Aymeric Fromherz

Better support for sladmit

1

Some uses of sladmit block progress in scheduling constraints, for instance when the post of the previous computation contains an unresolved frame. Proposed solution: Provide a special treatment for sladmit...

(reported by @nikswamy ) trefl fails on the following equality when removing indirection equalities in the first phase of the framing tactic ``` dlist_snoc left last cur right (List.Tot.Base.snoc ((*?u1592*)...

(proposed by @nikswamy ) We often use pure predicates when defining new slprops. Working with them can be inconvenient, for instance `pure p * pure q * s equiv pure...

In some cases, SMT verification of selectors VCs requires the global selector in the context. For instance: https://github.com/FStarLang/FStar/blob/c751ed5db01a24c13e334bab2c5762389a34791b/examples/steel/Selectors.LList.Derived.fst#L11 The most probable cause is that refinements on the types of selectors...

This issue often occurs when a program contains different branches, through if/then/else or pattern matching. For instance, ``` let test_if (r:ref int) : SteelSel unit (vptr r) (fun _ ->...

CheckNoUVars Failure in Steel

3

The following code snippet ``` val test (#a:Type0) (p:t a) : SteelSel (t a * t a) (llist p) (fun res -> llist (snd res)) (requires fun _ -> True)...