IMTs Verification & Validation Meta-Issue
Functional Verification of IMTs
Coq Implementation
IMT model
-
Model of Commitments, Trees (!7 (merged)) #2 (closed) -
Incremental Specs (!7 (merged)) #2 (closed) -
Internal/External API for single insertion (!7 (merged)) #2 (closed) -
Internal/External API for iterated insertion (!7 (merged))
Client Library Implementations
-
WIP Overflow Insert #4 (closed) -
Position-based insert (!7 (merged)) #3 (closed) -
WIP Batching/List Optimization #5 (closed)
PBT with QuickChick
-
?
!6 (closed))
Property Based Testing in Ocaml (-
Qcheck model for properties -
Extracted Code from Coq/Fstar -
Plug PBT tests into protocol/client code
Misc
-
Add coqdoc support
Report
-
TR/Submission -
Blog Post
Edited by Germán Delbianco