Meta-issue: Steel inference, framing, and selectors

[nikswamy]

• [x] Move all modules to use the PCM-based memory model (Nik)

• [x] Revise the formulation of frame preservation and remove the assume Steel.Effect.Atomic.witness_h_exists (Aseem)

• [ ] Add an interface to Steel.FramingEffect so that we can change its representation to use action trees directly rather than actions (once we have cumulativity)

• [ ] Remove the assumes in Steel.FramingEffect related to sl_implies

• [ ] Use Steel.FramingEffect to simplify existing modules, starting with Steel.HigherReference

• [ ] Extend SteelAtomic effect to support 2 additional indexes for requires/ensures

• [ ] Extend the multi-effect system to incorporate SteelAtomic

• [ ] Add an interface to Steel.Preorder so that its SMT patterns are hidden (Nik)

• [ ] Continue work on selectors and viewables (Aymeric)

Older typing glitches:

1. The post-hprop of a return is often not inferred

2. Trouble mixing refinement types. Not sure why the middle one (test_fails) fails.

assume
val t (n:nat) : Type0

noeq
type s (n:nat) =
  | MkS : st:t n -> s n

assume val ps (#n:nat) (x:t n) : hprop

let test_ok (n:nat) (x:t n) 
  : SteelT (y:s n{y.st == x}) (ps x) (fun _ -> ps x)
  = return #_ #(fun _ -> ps x)  (MkS x)

let test_fails (n:nat) (x:t n) 
  : SteelT (y:s n{y.st == x}) (ps x) (fun (y:s n{y.st == x}) -> ps y.st)
  = h_admit #(y:s n{y.st == x}) (ps x) (fun (y:s n{y.st == x}) -> ps y.st)

let ss #n (x: t n) = y:s n{y.st == x}
let test_ok_also (n:nat) (x:t n) 
  : SteelT (ss x) (ps x) (fun (y:ss x) -> ps y.st)
  = return #(ss x) #(fun (y:ss x) -> ps y.st) (MkS x)

[nikswamy]

Trying to use Steel.FramingEffect in the branch steel_framing ecafe7d43646b05403307d0e779dff6ce72a4781

1. Fails with Tot and SteelT not composable

let test (p:slprop) : SteelT unit p (fun _ -> p) = ()

2. Fails with "no tactic associated with deferred problem, F* may be in an inconsistent state.

assume val sl_admit (#a:Type) (#p:slprop) (#q:a -> slprop) (_:unit) : SteelT a p q
let test (p:slprop) : SteelT unit p (fun _ -> p) = sl_admit ()

3. Tactic seems to loop forever, needed to kill it

assume val sl_admit (#a:Type) (#[@@framing_implicit] p:slprop) (#[@@framing_implicit] q:a -> slprop) (_:unit) : SteelT a p q
let test (p:slprop) : SteelT unit p (fun _ -> p) = sl_admit ()

Now, some general scaffolding for the next few:

open Steel.FractionalPermission
open FStar.Ghost
assume val reference (a:Type0) : Type0
assume val pts_to (#a:Type0) (r:reference a) (p:perm) (v:erased a) : slprop u#1
assume val rread (#a:Type) (#p:perm) (#v:erased a) (r:reference a) : SteelT (x:a{x==Ghost.reveal v}) (pts_to r p v) (fun _ -> pts_to r p v)
assume val rwrite (#a:Type) (#v:erased a) (r:reference a) (v':a) : SteelT unit (pts_to r full_perm v) (fun _ -> pts_to r full_perm (Ghost.hide v'))

4. Fails with

(Error) user tactic failed: trefl: not a trivial equality ((fun _ -> pts_to r0 (MkPerm 1.0R) (hide u0)) vs ((*?u228*) _))

let read_write (#a:Type) (r0:reference a) (v0:erased a)
  : SteelT unit (pts_to r0 full_perm v0)
                (fun _ -> pts_to r0 full_perm v0)
  = let u0 = rread r0 in
    rwrite r0 u0

This could be a because of a discrepancy between hide u0 and v0.

5. So, I tried this variant, but the tactic loops

assume val rwrite_alt (#a:Type) (#v:erased a) (r:reference a) (v'':erased a) (v':a{v'==Ghost.reveal v''})
  : SteelT unit (pts_to r full_perm v) (fun _ -> pts_to r full_perm v'')

let read_write (#a:Type) (r0:reference a) (v0:erased a)
  : SteelT unit (pts_to r0 full_perm v0)
                (fun _ -> pts_to r0 full_perm v0)
  = let u0 = rread r0 in
    rwrite_alt r0 v0 u0

6. I also tried this swap example

let swap (#a:Type) (r0 r1:reference a) (v0 v1:erased a)
  : SteelT unit (pts_to r0 full_perm v0 `star` pts_to r1 full_perm v1)
                (fun _ -> pts_to r0 full_perm v1 `star` pts_to r1 full_perm v0)
  = let u0 = rread r0 in
    let u1 = rread r1 in
    rwrite_alt r0 v1 u1;
    rwrite_alt r1 v0 u0

This one doesn't loop, but it produces

(Error) user tactic failed: trefl: not a trivial equality ((fun _ -> star (pts_to r1 (MkPerm 1.0R) v0) (*?u74*) _) vs (fun _ -> star (star (pts_to r0 (MkPerm 1.0R) v1) (pts_to r1 (MkPerm 1.0R) v0)) emp))

suggesting a failure of the canonizer tactic.

7. Finally, this one also fails with what seems like the same issue with the canonizer.

(Error) user tactic failed: trefl: not a trivial equality ((fun _ -> star (pts_to r0 (MkPerm 1.0R) v1) (*?u106*) _) vs (fun _ -> star (star (pts_to r0 (MkPerm 1.0R) v1) (pts_to r1 (MkPerm 1.0R) v0)) emp))

assume
val rewrite_eq (#a:Type) (p:erased a -> slprop) (v0:erased a) (v1:erased a{v0 == v1})
  : SteelT unit (p v0) (fun _ -> p v1)

let swap (#a:Type) (r0 r1:reference a) (v0 v1:erased a)
  : SteelT unit (pts_to r0 full_perm v0 `star` pts_to r1 full_perm v1)
                (fun _ -> pts_to r0 full_perm v1 `star` pts_to r1 full_perm v0)
  = let u0 = rread r0 in
    let u1 = rread r1 in
    rwrite r1 u1;
    rwrite r1 u0;
    rewrite_eq (pts_to r1 full_perm) (Ghost.hide u0) v0;
    rewrite_eq (pts_to r0 full_perm) (Ghost.hide u1) v1

[R1kM]

Posting here several observations from ongoing work: Example 4 is indeed due to the discrepancy between hide u0 and v0. We might be able to apply an slprop canonicalization pass before running the tactic to solve this specific case.

Example 5, 6, 7 all suffer from program implicits that appear in the slprop indices (such as the permission, or the ghost value). In the current state, these implicits can only be inferred by unification on the slprop indices, but the tactic does not handle it correctly, since it considers for instance pts_to r0 full_perm v0 and pts_to r0 ?u1 ?u2 to be different terms. Passing these implicits explicitly in rread and rwrite (for instance rread #_ #full_perm #v0 r0) allows example 5 to verify.

In addition to requiring explicit program implicits, examples 6 and 7 also need their bodies to end with an explicit () to verify. When designing the framing tactic in our idealized calculus, we made the assumption that each body would terminate with a return, and hence a SteelF function. This invariant does not hold here, and that seems to be the cause for an slprop mismatch. I'm investigating some more.

Minor typo: In example 7, the first rwrite should have r0 as an argument

[R1kM]

More comments about why we currently require a return at the end of each function, and how we might avoid it. Let's consider the following code:

let read_write (#a:Type) (r0:reference a) (v0:erased a)
  : SteelT unit (pts_to r0 full_perm v0)
                (fun _ -> pts_to r0 full_perm v0)
  = let u0 = rread #_ #full_perm #v0 r0 in
    rwrite_alt #_ #v0 r0 v0 u0

As this is a bind between two annotated Steel functions, the inferred type for the body of the function would be of the shape SteelT unit (?u1 * ?u2) (?u3 * ?u4). But an extra indirection is added when performing subcomp, adding the following constraints:

?u5 == ?u3 * ?u4
?u6 == (fun _ -> pts_to r0 full_perm v0)
can_be_split_forall ?u5 ?u6

In the current state of framing, we first solve the trivial equalities (i.e. where one side contains no implicit, so ?u6 here, as well as ?u3 which corresponds to the postresource of rwrite), then the postresource of subcomp (i.e. can_be_split ?u5 ?u6 here) and then the rest of the constraints. But when solving ?u5, there is a chance we pick a term that will be equivalent to (fun _ -> pts_to r0 full_perm v0) * ?u4, but unfortunately not equal, leading to a failure when trying to solve the equality.

When the last command in the body is a return (or a lifted pure variable), and that the previous command was a Steel (which corresponds to almost all cases so far), we know the shape of the corresponding ?u3 * ?u4: ?u3 will be the complete postresource, and ?u4 will be an empty frame. Hence we can rig the solving of subcomp_post to make sure that the equality corresponding to ?u5 == ?u3 * ?u4 can be solved when finally encountered.

So what can we do in the general case? It seems that we need some knowledge of the shape of the inferred postcondition to correctly solve subcomp_post. A proposed solution is to solve all the equalities before solving subcomp_post, which will create new restricted uvars. In our example, this would give us the constraint can_be_split (fun _ -> pts_to r0 full_perm v0 star ?u7) (fun _ -> pts_to r0 full_perm v0) when solving subcomp_post.

How is it different from the previous naive solution which caused scoping issues? Here, we only solve the equalities, not the slprop equivalences which require calls to canon. Especially, given the cascaded structure of let-bindings, the only scope restriction that should happen is for the postcondition of the very last term, when restricting its scope to the top-level scope. All the other equalities should be restricted to inner constraints in binds, and should not leak outside these binds since they are then "blocked" by slprop equivalences.

One possible issue is that we are breaking the invariant that we have at most one slprop uvar when calling canon. We need to identify when we might have several uvars, and investigate how to tweak the tactic accordingly.

This approach could have several advantages. First, since the restriction of scopes will be performed when solving equalities, we might not need anymore to force backward inference. Second, reading and inspecting constraints after solving equalities is much easier. We don't have extra indirections, only the slprop equivalences.

[R1kM]

We also discussed how to typecheck the following example:

assume val p: slprop

let f (#a:Type) (r0:reference a) (v0:erased a) 
  : SteelT unit (p `star` pts_to r0 full_perm v0) (fun _ -> p `star` pts_to r0 full_perm v0)
  = rwrite_alt #_ #v0 r0 v0 (Ghost.reveal u0)

This only involves a subcomp from Steel to Steel. As Aseem remarked this morning, a subcomp from Steel to Steel only occurs when the body consists of a single function call. As soon as we have a bind, the inferred effect becomes SteelF. Furthermore, we also observed that having a refinement in the return type was also generating a bind (for instance if we were calling rread, and returning x:a{x == Ghost.reveal v0}). This seems to be due to an assert implicitly generated for the refinement.

To solve this, a solution might be to support framing inside of the Steel <: Steel subcomp: given a f : SteelT a pre_f post_f and an annotation SteelT a pre_g post_g, subcomp would succeed if we can solve pre_g <==> pre_f * frame and forall x. post_g x <==> post_f x * frame.

The subcomp for SteelF <: Steel would remain as it currently is.