Variable not found when calling function involving $

[danelahman]

The following minimised example (calling into KreMLin's loops library, where the first argument of CL.while is marked with $.)

module Test

module B = LowStar.Buffer
module U32 = FStar.UInt32
module CL = C.Loops

open FStar.HyperStack.ST

let const_cond (p:B.pointer U32.t) 
: Stack bool 
    (requires (fun h0 -> B.live h0 p)) 
    (ensures  (fun h0 x h1 -> True))
= true

let foo (p:B.pointer U32.t)
: ST unit 
    (requires (fun h0 -> B.live h0 p))
    (ensures  (fun h0 x h1 -> True))
= CL.while
    (fun () -> const_cond p)
    (fun () -> ())

fails with

(Error) Variable "h0#450644" not found

and points to the h0 in (ensures (fun h0 x h1 -> True)) in the type of const_cond.

[mtzguido]

Looking at this, here's a slight minimization:

open FStar.HyperStack.ST

// copied from C.Loops
assume val while:
  #test_pre: (HyperStack.mem -> GTot Type0) ->
  #test_post: (bool -> HyperStack.mem -> GTot Type0) ->
  $test: (unit -> Stack bool
    (requires (fun h -> test_pre h))
    (ensures (fun h0 x h1 -> test_post x h1))) ->
  body: (unit -> Stack unit
    (requires (fun h -> test_post true h))
    (ensures (fun h0 _ h1 -> test_pre h1))) ->
  Stack unit
    (requires (fun h -> test_pre h))
    (ensures (fun h0 _ h1 -> test_post false h1))

// just to mention m
val memok : HyperStack.mem -> Type0
let memok m = True

let foo ()
: ST unit 
    (requires (fun h0 -> True))
    (ensures  (fun h0 x h1 -> True))
= let ff () : Stack bool
                    (requires memok)
                    (ensures (fun the_bad_guy x h1 -> True))
            = true
  in
  while ff (fun () -> ())

Bug.fst(28,34-28,45): (Error 230) Variable "the_bad_guy#489" not found

The problem is that (after #57), the type of h1 in postconditions is refined with an assumption of the precondition, which then confuses F* at some point. Here, the type of the last h1 is m:mem{memok the_bad_guy} (with the_bad_guy in scope!), which at some point becomes ill-scoped. Annotating it as (h1:HyperStack.mem) makes the problem go away. Having a constantly True precondition also avoids mentioning h0 and hence succeeds, I'm forcing it to appear via memok to trigger the bug here.

[mtzguido]

Smaller:

open FStar.HyperStack.ST

assume val while:
  #post: (bool -> HyperStack.mem -> GTot Type0) ->
  $f: (unit -> Stack bool
    (requires (fun h -> True))
    (ensures (fun h0 x h1 -> post x h1))) ->
  Stack unit
    (requires (fun h -> True))
    (ensures (fun h0 _ h1 -> True))

// bogus
val memok : HyperStack.mem -> Type0
let memok m = True

let foo ()
: STATE unit (fun _ _ -> False) // false precondition, anything goes
= let ff () : Stack bool
                    (requires memok)
                    (ensures (fun the_bad_guy x h1 -> True))
            = true
  in
  while //#(fun x h1 -> True)
        ff

I believe the problem is F not tracking that the_bad_guy is free in the a flex pattern, see this excerpt from a log where I made F abort on an unbound variable (--defensive abort which I'm about to mainline). Notice FV(lhs) does not mention the_bad_guy.

Attempting 125 (Tm_app::(*?u20*) _ x2353 h12354 vs Tm_fvar: Prims.l_True::Prims.l_True); rel = (=)
solve_t_flex_rigid_eq
it's a pattern
lhs         = (* Instantiating implicit argument in application *)
((uu___1679: Prims.unit), (ff2021:
(uu___2409: Prims.unit
    -> FStar.HyperStack.ST.Stack Prims.bool
        Danel.memok
        (fun
            (_: FStar.Monotonic.HyperStack.mem)
            (_: Prims.bool)
            (_: (uu___02413: FStar.Monotonic.HyperStack.mem{Danel.memok the_bad_guy2410}))
            ->
            Prims.l_True))) |- ?20 : uu___2414: Prims.bool -> uu___2415: FStar.Monotonic.HyperStack.mem -> Prims.GTot Type0) [x2353 h12354]
FV(lhs)         = uu___#1679, ff#2021, x#2353, h1#2354
rhs         = Prims.l_True
FV(rhs)         = 
Solving 125: with [TERM 20 <- fun
  (_: Prims.bool)
  (_: (uu___02424: FStar.Monotonic.HyperStack.mem{Danel.memok the_bad_guy2352}))
  ->
  Prims.l_True]
Solving 125 ((* mk_problem: logical guard for lambda co-domain *)
((uu___1679: Prims.unit), (ff2021:
(uu___2425: Prims.unit
    -> FStar.HyperStack.ST.Stack Prims.bool
        Danel.memok
        (fun
            (_: FStar.Monotonic.HyperStack.mem)
            (_: Prims.bool)
            (_: (uu___02429: FStar.Monotonic.HyperStack.mem{Danel.memok the_bad_guy2426}))
            ->
            Prims.l_True))), (uu___2175: Prims.unit), (the_bad_guy2352: FStar.Monotonic.HyperStack.mem), (x2353: Prims.bool), (h12354: uu___02430: FStar.Monotonic.HyperStack.mem{Danel.memok the_bad_guy2352}) |- ?33 : Type0)) with formula Prims.l_True
Danel.fst(26,8-26,10): (Warning 290) Internal: term is not closed (commit).
t = (fun
  (_: Prims.bool)
  (_: (uu___02433: FStar.Monotonic.HyperStack.mem{Danel.memok the_bad_guy2352}))
  ->
  Prims.l_True)
FVs = ((the_bad_guy2352: FStar.Monotonic.HyperStack.mem))
 (see also Danel.fst(22,54-22,58))
Unexpected error
Failure("Aborting due to '--defensive abort'")