What can we do to get automated framing in specifications?

[nikswamy]

When writing Steel specifications in selector style, the specifications themselves need to be framed.

Consider this:

First some general scaffolding for a test case, defining an abstract indexed vprop p x n.

module AbstractVProp
open Steel.Memory
open Steel.Effect
open Steel.Effect.Atomic

val t : Type0
val ty : Type0
val p (x:t) (n:nat) : vprop
val q : vprop
val type_of_p (x:t) (n:nat) 
  : Lemma (ensures normal (t_of (p x n)) == ty)

let coerce_eq (#a:Type) (#b:Type) (_:squash (a == b)) (x:a) : b = x

let value_of (x:t) (#n:nat) (r:rmem (p x n)) 
  : GTot ty
  = type_of_p x n;
    coerce_eq () (r (p x n ))

Now, if I want to write a spec involving p, I need to explicitly focus the memory on the p-footprint when selecting from it. For that, a combinator like this is useful:

let focus (#r:vprop)
          (#r0:vprop{
            FStar.Tactics.with_tactic
              selector_tactic
                   (r `can_be_split` r0 /\ True)
          })
          (h:rmem r)
  : Tot (rmem r0)
  = focus_rmem h r0

focus triggers the use of the selector tactic, which is helpful.

Now, when writing a spec for bar, I have to write:

val bar (x:t) (y:ty)
  : Steel unit 
    (p x 0 `star` q)
    (fun _ -> emp)
    (requires fun h -> 
      let v = value_of x (focus h) in
      v == y)
    (ensures fun h0 _ h1 -> True)

making an explicit invocation of focus.

But, actually, in this case it doesn't work, because the system is unable to infer the implicit argument instantiation of value_of x #0. I tried revising focus and value_of as below, to defer solving them

let focus (#r:vprop)
          (#[@@@framing_implicit] r0:vprop{
            FStar.Tactics.with_tactic
              selector_tactic
                   (r `can_be_split` r0 /\ True)
          })
          (h:rmem r)
  : Tot (rmem r0)
  = focus_rmem h r0
  
 let value_of (x:t) (#[@@@framing_implicit] n:nat) (r:rmem (p x n)) 
  : GTot ty
  = type_of_p x n;
    coerce_eq () (r (p x n )) 

But, that didn't work either.

So, two questions:

1. How can we rig the selector_tactic so that it too can work like the framing tactic used in the effect and solve deferred constraints, while resolving implicits

2. Going further, is there a way to even automate away the placement of focus?