Recalling a Witness

Software artifacts (evaluated by the POPL AEC)

The examples and case studies described in Sections 2, 3, and 4 of this paper have been implemented in F⭑ (master branch). F⭑ is open source software, it is available on Github, and it is known to work well on Windows, Mac, and Linux. Instructions for building from source are available at INSTALL.md.

The AEC evaluated these examples and case studies as they were presented in F⭑ release v0.9.5.0. These artifacts were subsequently polished further to better match the text in the final version of the paper, see this commit in the master branch of the F⭑ repository. However, as F⭑ is a language that is actively developed, the contents of the files listed below might have changed since this paper was published.

The examples and the supporting library code are in the following files in the F⭑ master branch
(as of this commit; the given filepaths are relative to the top-level fstar directory):

Section 2 of the paper

ulib/FStar.Monotonic.Heap.fsti
Basic heap model interface with support for monotonic references

ulib/FStar.Monotonic.Heap.fst
Implementation of the basic heap model interface

ulib/FStar.Heap.fst
Plain heap model where all the references have trivial preorder

ulib/FStar.ST.fst
Implementation of the STATE effect using the heap model

ulib/FStar.MRef.fst
Utility functions for monotonic references

examples/preorders/SnapshotST.fst
An example of temporarily escaping the preorder

ulib/FStar.Monotonic.HyperHeap.fst
Region-based hyperheap model with support for monotonic references

ulib/FStar.Monotonic.HyperStack.fst
Region-based hyperstack model with support for monotonic references

ulib/FStar.Monotonic.RRef.fst
Utility functions for hyperstack monotonic references

Section 3 of the paper

examples/preorders/MonotonicArray.fst
The monotonic array library

examples/preorders/Protocol.fst
The file transfer case study

Section 4 of the paper

examples/preorders/Ariadne.fst
The Ariadne protocol case study

back to paper page