Steel work items

[R1kM]

Recapping here the list of Steel work items

Code Refactoring

• Replace SteelAtomic unobservable and SteelAtomic observable by SteelGhost and SteelAtomic
• Remove the quantification on invariant_names for each SteelAtomic signature
• Use Set.equal instead of == for invariant_names relations, so as to trigger SMT automatically
• Add smt_fallback to SteelSel
• Add an Atomic version of SteelSel
• Replace all uses of Steel by SteelSel, and rename SteelSel (and variants) into Steel
• Unify tactics in SteelSel.Common and Steel.Common
• Add refinement in post-memory to include validity of precondition, so as to avoid repeating it
• Use selectors in Queue/DoublyLinkedList
• Move stable libraries to ulib/experimental
• Wrap up Steel.Array library (@tahina-pro , PR Pointer arithmetics for C arrays in Steel (attempt 2) FStar#2319 )
• Clean up the different versions of SteelSel.change_slprop
• Split Steel.Effect into different submodules, with a top-level empty module including them all
• Rename DisposableInvariant into CancellableInvariant, to reduce confusion with Iris
• Change the value argument in Steel.Reference, Steel.MonotonicHigherReference and Steel.HigherReference to a non-erased value
• Combine selectors with permissions for references (#2297 )

(Layered) Effects improvements

• Add SMT fallback prop to all pre and post (similar to paper calculus)
• Allow the use of unconstrained implicits in subcomp and if_then_else for framing and SMT rewrites (#2234)
• Improve composition between different effects in if/then/else (#2220)
• (related to previous) Revisit effect hierarchy to use lifts instead of a myriad of polymonadic binds
• Dependent pattern matching (#2256)
• Use computation trees as repr for Steel effect
• Figure out SteelGhost and erased interaction
• Linear generation of equalities (#2280)
• Solve (un)observable preconditions in effect combinators by tactic

Framing tactic improvements

• Do not use fst/snd/pairs for internal constructs and normalization
• Add special support for sladmit (#2239)
• Add special support for pure predicates (#2235)
• Make code more resistant when SMT fallback is called while being disabled (i.e. with the predicate already resolved to True)
• Provide better error message when unification fails (should not happen, please report)
• Brainstorm about "irrelevant_if_duplicated" attribute for slprops (for instance, pts_to r 0.5 v1 * pts_to r 0.5 v2)

IDE support

• Remove spurious warnings about implicit not resolved when they are resolved by tactic
• Fix ranges (and underscored code snippet) when an assertion fails
• Provide meaningful error message and range when the SMT query in smt_fallback fails
• Only open fstar:goals buffer in a debug mode when tactic fails.
• Provide information about the current slprop context from Emacs

Other

• Allow native extraction to C
• How do we remove "reifiable" from the Steel effect for extraction to OCaml?
• Inspect SMT queries (especially the large number of small queries generated)
  • prop subtyping
  • unobservable vs observable queries
  • All the rest
• Documentation and Steel tutorial
• Provide more combinators for vprops (@tahina-pro, PR Some SteelSel combinators: vrefine, vrewrite, vdep FStar#2277)

F* issues

• Fix CheckNoUvars error in IDE ( CheckNoUVars Failure in Steel #217 )
• Fix segfaults when calling the tactic (#2209)
• Correctly propagate implicit arg qualifiers in Rel.imitate_app (PR Rel: Propagate arg qualifiers in imitate_app FStar#2238 )
• Allow the generation of SMT guards when calling the unifier through a variant of trefl (PR Allow full SMT guard generation in trefl_with_guards tactic FStar#2240 )

[aseemr]

See FStarLang/FStar#2256 for dependent pattern matching