Split Tree module in the F* Spec
TO BE MERGED AFTER !23 (closed)
This MR splits the Tree
module from the F* Sapling Spec into the following sub-modules:
-
Tree.Data.fst
: Data structures used by the spec. -
Tree.Properties.fst
: Predicates and proofs used in the specification that shouldn't be part of the extracted implementation. This module is extracted for use in tests. -
Tree.Methods.fst
: Functions and proofs that, along withTree.Data
, make up the certified extracted implementation.
The Tree.fst
file just includes all of the previous sub-modules, following the style used in F*'s standard library.
Edited by Antonio Locascio