[RESOLVED] How to use sub to create a live sub buffer - Assertion failure - understood the usage

[sheeraSearch82]

I am getting assertion failure at sub. Could someone please help?
`module Test

module B = LowStar.Buffer
module U32 = FStar.UInt32
module H = FStar.HyperStack

open LowStar.BufferOps

type lbuffer (l:nat) = b:B.buffer U32.t {B.length b == l}

let test (h:H.mem)
(l:lbuffer 1024 {B.live h l })
(len:UInt32.t{U32.v len > 1 /\ U32.v len < B.length l})=
assert (0 + U32.v len < B.length l);
assert (U32.v len < B.length l);
let l1 = B.sub l 0ul U32.(len -^ 1ul) in
admit()
`

[R1kM]

The problem seems to be that you try to use an effectful function (sub) in the Tot effect. If you look at the definition of sub, it is defined with the Stack effect.
For instance, the following code works:

let test (h:H.mem)
(l:lbuffer 1024 {B.live h l })
(len:UInt32.t{U32.v len > 1 /\ U32.v len < B.length l}) : 
  ST.Stack unit (requires fun h -> B.live h l) (ensures fun _ _ _ -> True)
=
assert (0 + U32.v len < B.length l);
assert (U32.v len < B.length l);
let l1 = B.gsub l 0ul U32.(len -^ 1ul) in
admit()

Alternatively, if you want to define a sub-buffer for specification and proof purposes only, you can use gsub, which is Ghost and will not be extracted.