Need at least one unit of fuel to reason with abstract vprops

[nikswamy]

This may be related to the unfolding behavior of vprops. Could it be remedied by using strict_on_arguments?

module AVP
open FStar.Ghost
open Steel.FractionalPermission
open Steel.Memory
open Steel.Effect.Atomic
open Steel.Effect
open Steel.Reference
#push-options "--ide_id_info_off"

assume
val s : Type0
assume
val vs (x:s) : vprop

noeq
type t = {
  g : ghost_ref nat;
  something_else : s;
}

[@@__reduce__]
let vt (x:t) =
  ghost_vptr x.g `star`
  vs x.something_else

let value_of (x:t) (r:rmem (vt x))
  : GTot nat
  = ghost_sel x.g r

//If you're not using an abstract vprop, then this code goes through without fuel
#push-options "--fuel 0 --ifuel 0"
let foo (#o:_) (x:t)
  : SteelGhost unit o
    (vt x)
    (fun _ -> vt x)
    (requires fun _ -> True)
    (ensures fun h0 _ h1 ->
      value_of x (focus_rmem h0 _) ==
      value_of x (focus_rmem h1 _))
  = noop(); ()
#pop-options

//Now let's try it in abstract style
let type_of_vt (x:t) :
  Lemma (ensures (t_of (vt x) == nat & t_of (vs x.something_else)))
        [SMTPat (t_of (vt x))]
  = ()

let coerce_eq (#a:Type) (#b:Type) (_:squash (a == b)) (x:a) : b = x
let value_of_alt (x:t)
                 (r:rmem (vt x))
  : GTot nat
  = type_of_vt x;
    fst (coerce_eq #_ #(nat & t_of (vs x.something_else)) () (r (vt x)))

//this works
let foo_alt (#o:_) (x:t)
  : SteelGhost unit o
    (vt x)
    (fun _ -> vt x)
    (requires fun _ -> True)
    (ensures fun h0 _ h1 ->
      value_of_alt x (focus_rmem h0 _) ==
      value_of_alt x (focus_rmem h1 _))
  = noop(); ()

//But, setting the fuel to 0 makes it fail
#push-options "--fuel 0 --ifuel 0"
[@@expect_failure]
let foo_alt' (#o:_) (x:t)
  : SteelGhost unit o
    (vt x)
    (fun _ -> vt x)
    (requires fun _ -> True)
    (ensures fun h0 _ h1 ->
      value_of_alt x (focus_rmem h0 _) ==
      value_of_alt x (focus_rmem h1 _))
  = noop(); ()
#pop-options