Steel work items

[R1kM]

Recapping here the list of Steel work items

Code Refactoring

• [x] 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
• [x] Add smt_fallback to SteelSel
• [x] Add an Atomic version of SteelSel
• [x] Replace all uses of Steel by SteelSel, and rename SteelSel (and variants) into Steel
• [x] 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 #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
• [x] Combine selectors with permissions for references (#2297 )

(Layered) Effects improvements

• [ ] Add SMT fallback prop to all pre and post (similar to paper calculus)
• [x] 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)
• [x] (related to previous) Revisit effect hierarchy to use lifts instead of a myriad of polymonadic binds
• [x] Dependent pattern matching (#2256)
• [ ] Use computation trees as repr for Steel effect
• [x] Figure out SteelGhost and erased interaction
• [x] Linear generation of equalities (#2280)
• [x] Solve (un)observable preconditions in effect combinators by tactic

Framing tactic improvements

• [ ] Do not use fst/snd/pairs for internal constructs and normalization
• [x] Add special support for sladmit (#2239)
• [ ] Add special support for pure predicates (#2235)
• [x] 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
• [x] 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
• [x] Provide more combinators for vprops (@tahina-pro, PR #2277)

F* issues

• [ ] Fix CheckNoUvars error in IDE ( #2213 )
• [ ] Fix segfaults when calling the tactic (#2209)
• [x] Correctly propagate implicit arg qualifiers in Rel.imitate_app (PR #2238 )
• [x] Allow the generation of SMT guards when calling the unifier through a variant of trefl (PR #2240 )

[aseemr]

See https://github.com/FStarLang/FStar/pull/2256 for dependent pattern matching