Strange interaction between framing, preconditions, and conditionals

[nikswamy]

test4 fails and the only difference with test2 is that it contains an irrelevant framed assertion ff xx

module MemCpy
open Steel.Memory
open Steel.Effect
open Steel.Effect.Atomic
module U32 = FStar.UInt32


#push-options "--ide_id_info_off"
#push-options "--max_fuel 0 --max_ifuel 0"

let fst = fst
let snd = snd
assume
val array (t:Type0) : Type0
let contents (t:Type0) = Seq.seq t
let length #t (c:contents t) = Seq.length c
assume
val is_array (#t:_) (x:array t) (c:contents t) : slprop u#1

assume
val split (#t:Type) (#r:contents t) (a:array t) (i:U32.t { U32.v i <= length r})
  : SteelT (array t & array t)
           (is_array a r)
           (fun lr ->
              let s = Seq.split r (U32.v i) in
              is_array (fst lr) (fst s) `star` is_array (snd lr) (snd s))

let test1 (a:Type) (len:U32.t { U32.v len > 0 })
          (v0:contents a { length v0 == U32.v len })
          (src:array a)
    : SteelT unit
      (is_array src v0)
      (fun _ -> emp)
    = let x = split src 1ul in
      sladmit()

let test2 (a:Type) (len:U32.t)
          (v0:contents a { length v0 == U32.v len })
          (src:array a)
    : SteelT unit
      (is_array src v0)
      (fun _ -> emp)
    = if len = 0ul
      then (noop(); sladmit())
      else (
        let x = split src 1ul in
        sladmit()
      )

assume
val t : Type0
assume
val ff (x:t) : slprop u#1

let test3 (a:Type) (len:U32.t { U32.v len > 0 })
          (v0:contents a { length v0 == U32.v len })
          (src:array a)  (xx:t)
    : SteelT unit
      (is_array src v0 `star` ff xx)
      (fun _ -> emp)
    = let x = split src 1ul in
      sladmit()

let test4 (a:Type) (len:U32.t)
          (v0:contents a { length v0 == U32.v len })
          (src:array a) (xx:t)
    : SteelT unit
      (is_array src v0 `star` ff xx)
      (fun _ -> emp)
    = if len = 0ul
      then (noop(); sladmit())
      else (let x = split src 1ul in
            sladmit())

[R1kM]

Minimizing further, the following test4 fails:

let test4 (a:Type) (len:U32.t)
          (v0:contents a { length v0 == U32.v len })
          (src:array a) (xx:t)
    : SteelT unit
      (is_array src v0 `star` ff xx)
      (fun _ -> emp)
    = assume (length v0 > 0);
      let x = split src 1ul in
      sladmit()

[aseemr]

I am unable to verify even test2 in the master branch (Edit: works after I merged steel to master).

[aseemr]

Here is a small repro:

module Test

open Steel.Memory
open Steel.Effect
#push-options "--ide_id_info_off"
#push-options "--max_fuel 0 --max_ifuel 0"

assume
val is_elt (_:Seq.seq ℤ & Seq.seq ℤ) : slprop u#1

assume
val split (r:Seq.seq ℤ) (i:ℕ {i ≤ Seq.length r})
  : SteelT unit
           emp
           (λ _ → is_elt (Seq.split r i))

assume val drop (p:slprop u#1) : SteelF unit p (λ _ → emp) (λ _ → ⊤) (λ _ _ _ → ⊤)

let test4 (v0:Seq.seq ℤ)
    : Steel unit
        emp
        (λ _ → emp)
        (λ _ → Seq.length v0 == 2)
        (λ _ _ _ → ⊤)
    = split v0 1; drop (is_elt (Seq.split v0 1))

Move the requires to a refinement on v0, and it works.

[aseemr]

This also works:

let test4 (v0:Seq.seq ℤ)
    : Steel unit
        emp
        (λ _ → emp)
        (λ _ → Seq.length v0 == 2)
        (λ _ _ _ → ⊤)
    = let _ : squash (Seq.length v0 == 2) = () in
      let x = split v0 1 in
      drop (is_elt (Seq.split v0 1))

and so does this in the original example:

let test4 (a:Type) (len:U32.t)
          (v0:contents a { length v0 == U32.v len })
          (src:array a) (xx:t)
    : SteelT unit
      (is_array src v0 `star` ff xx)
      (λ _ → emp)
    = if len = 0ul
      then (noop(); sladmit())
      else (let _ : squash (U32.v len > 0) = () in
            let x = split src 1ul in
            sladmit())

The reason is the logical part of the tactics environment not being precise enough.

[R1kM]

We discussed this issue during today's Steel meeting. As mentioned by Aseem, the problem is that the tactic context does not contain the logical context. As such, when some SMT goals for refinements are generated during the tactic run, verification fails because of missing facts. This is why adding a bound squash variable with the right facts is a workaround.

We discussed the following two solutions:
1/ When an SMT goal is generated during the tactic, add it to the equality abduction variable. This will ensure it will have the correct facts in the context, and we already have most of the machinery in place. The problem is that we do not currently have this variable in all separation logic VCs because of limitations in subcomp.
2/ Add a mechanism similar to assert by tactic, (called collect by tactic) to encode SL goals inside the logical context, while deferring them to a tactic.

We agreed to try 1/ first, as 2/ might be a more involved change.