UROP project @ Programming Languages & Verification @ MIT CSAIL
GenerUtil.v
: basic general utilitiesKeyUtil.v
: utilities specific to the trees' keys (list bool
)SeqAccess.v
: more general utilies for working with lists and zero-extended sequencesPrefixCritical.v
: utilities for working with prefixes oflist bool
and with critical bits of pairs of tree keysFront.v
: (roughly) the definition of crit-bit trees and the unverified operations on themMain.v
: (roughly) the proof internals + a basic explanation attemptTheorem.v
: (roughly) the key theorems specifying the behavior of the definitions inFront
> "(roughly)" because the boundaries between Front
, Main
, and Theorem
are not very sharp.
The dependencies between the files are contained in the transitive closure of this: