Fixed what was broken, or so it seems

Sandbox.fst

module Sandbox

open FStar
open LowStar.Buffer
open LowStar.BufferOps
open FStar.HyperStack.ST

module Buffer = LowStar.Buffer

unfold let test_pre (b r: buffer UInt32.t) (h: FStar.HyperStack.mem): Type0 =
  live h b /\ live h r /\
  length r = 1 /\ length b = 3 /\
  UInt32.v (Buffer.get h r 0) < Buffer.length b /\
  UInt32.v (Buffer.get h r 0) >= 0

unfold let test_post (b r: buffer UInt32.t) (test: bool) (h: FStar.HyperStack.mem): Type0 =
  test_pre b r h /\ (test = true ==>
    UInt32.v (Buffer.get h r 0) < Buffer.length b - 1)



module HS = FStar.HyperStack 

val while:
  #test_pre: (HS.mem -> GTot Type0) ->
  #test_post: (bool -> HS.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))
let rec while #test_pre #test_post test body =
  if test () then begin
    body ();
    while #test_pre #test_post test body
  end

module H = FStar.HyperStack
module HA = FStar.HyperStack.All

module U32 = FStar.UInt32

module B = LowStar.Buffer

module M = LowStar.Monotonic.Buffer

open LowStar.BufferOps

#push-options "--z3rlimit 151 --ifuel 4 --fuel 4"
let square_while ()
  : HA.Stack unit (fun _ -> true) (fun h0 _ h1 -> true) =
  //let open C.Nullity in
  let open FStar.UInt32 in
  HA.push_frame ();
  let b = B.alloca_of_list [ 0ul; 1ul; 2ul ] in
  
  // JP: createL doesn't work here!
  let r = B.alloca 0ul 1ul in
  // JP: eta-expansions seem necessary for the pre/post
  let test (): HA.Stack bool (requires (fun h -> test_pre b r h)) (ensures (fun _ ret h1 -> test_post b r ret h1)) =
    (!*r) <> 2ul
  in
  let body (): HA.Stack unit (requires (fun h -> test_post b r true h)) (ensures (fun _ _ h1 -> test_pre b r h1)) =
    let h = HA.get () in 
    assert (B.live h r /\ B.length r = 1);
    b.(!*r) <- b.(!*r) *%^ b.(!*r);
    r.(0ul) <- !*r +%^ 1ul
  in
  let h = HA.get () in
  assert (
    UInt32.v (B.get h r 0) < B.length b /\
    UInt32.v (B.get h r 0) >= 0
  );
  while #(test_pre b r) #(test_post b r) test body;
  HA.pop_frame ()

let square_while_2 ()
          : HA.Stack unit (fun _ -> true) (fun h0 _ h1 -> true) =
  //let open C.Nullity in
  let open FStar.UInt32 in
  HA.push_frame ();
  let b = B.alloca_of_list [ 0ul; 1ul; 2ul ] in
  
  // JP: createL doesn't work here!
  let r = B.alloca 0ul 1ul in
  // JP: eta-expansions seem necessary for the pre/post
  let test (): HA.Stack bool (requires (fun h -> test_pre b r h)) (ensures (fun _ ret h1 -> test_post b r ret h1)) =
    (!*r) <> 2ul
  in
  let body (): HA.Stack unit (requires (fun h -> test_post b r true h)) (ensures (fun _ _ h1 -> test_pre b r h1)) =
    let h = HA.get () in
    assert (B.live h r /\ B.length r = 1);
    b.(!*r) <- b.(!*r) *%^ b.(!*r);
    r.(0ul) <- !*r +%^ 1ul
  in
  let h = HA.get () in
  assert (
    UInt32.v (B.get h r 0) < B.length b /\
    UInt32.v (B.get h r 0) >= 0
  );
  while #(test_pre b r) #(test_post b r) test body;
  HA.pop_frame ()