Auxiliary materials for Recalling a Witness
back to paper page
# 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