Skip to content

Split Tree module in the F* Spec

Antonio Locascio requested to merge alocascio@tree-splitting into master

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 with Tree.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

Merge request reports