Steel work items

[nikswamy]

This issue elaborates on this wiki page https://github.com/FStarLang/FStar/wiki/Steel-(Outline) enumerating a breaking down of our current work items.

---

Semantics and effectful interface

• Revise semantics so that it uses pre/post directly instead of WP (Aseem)

• Define a Steel layered effect (Aseem):

• Define a preorder indexed generic monotonic state monad (Aseem)

• Revise semantics to layer it on top of the above-defined state monad + div, instead of on top of div alone (Aseem)

• Make the bind rule in the semantics more canonical, and provide an implicit weakening in the layered effect bind combinator (Aseem)

• Define combinators to build fp_props (Aymeric)

  • Figure out how to hook up a tactics to check that a requires/ensures with a particular footprint is included in the expects/provides foot print

• Try to prove the WP/pre-post equivalence lemma (Guido)

• Define another layer on top of the Steel layered effect where the pre- and postconditions are viewable predicates (instead of fp_prop predicates), provide a non-structural frame rule in this layer that uses viewable selectors for the frame prop in its pre- and postconditions (Aymeric/Aseem)

F* typechecker internal work

• Consider adding support for simplifying formulas that result from converting triples -> WPs -> triples, so that this round trip is almost the identity (Guido, Aseem, Nik?)

• Modify the return combinator for layered effects, so that it has type a:Type -> x:a -> <some binders> -> repr a is, instead of the current type a:Type -> <some binders> -> x:a -> repr a is. This is needed for the return combinator in the Steel effect (for parametricity of the lpost) (Aseem)

Memory model

• Add support for arrays (Denis)

  • Debug proof performance
  • Support for sharing and recombining arrays

• Consider adding support for other user-defined resources (e.g., provide a way for a user to define a struct)

Tactics

• Instantiate frame inference symbolic execution tactic with Steel.Memory (Denis)
• Add the frame rule optimization so that framing tactics that compute delta only run once at each application of frame (Denis, Aymeric) (you already had something like this working)
• Native compilation of all the tactics (Guido, already has something working)

Example programs

• Swapping with disjoint or equal pointers (Nik)
• See https://github.com/FStarLang/FStar/wiki/Steel-(Outline)#3-steel-in-action for more examples

Libraries

• Storable locks built abstractly from a ref (lock p)

Open ended stuff

• What do preorders on hprops look like? Can we revisit things like rgrefs, francois pottier's monotonic state, support for generic PCMs? (Danel, ...)

[nikswamy]

This is essentially done or superceded by all the work on the SteelCore paper. We'll track ongoing work on Steel in other issues.