val read_with_perm
  (#k: parser_kind)
  (#t: Type u#0)
  (#p: parser k t)
  (r: leaf_reader p)
  (#len: Ghost.erased U32.t)
  (sl: input_buffer_t len)
  (pos: U32.t)
  (n: U32.t)
  (perm_of: R.perm (slice_of sl).base)
: HST.Stack t
  (requires (fun h ->
    valid_input_buffer p h sl perm_of pos /\
    k.LPL.parser_kind_subkind == Some LPL.ParserStrong /\
    k.LPL.parser_kind_high == Some k.LPL.parser_kind_low /\
    k.LPL.parser_kind_low == U32.v n /\
    R.readable h perm_of pos (get_valid_pos p h (slice_of sl) pos)
  ))
  (ensures (fun h res h' ->
    let pos' = get_valid_pos p h (slice_of sl) pos in
    B.modifies (R.loc_perm perm_of) h h' /\
    R.preserved perm_of 0ul pos h h' /\
    R.preserved perm_of pos' (B.len (slice_of sl).LPL.base) h h' /\
    R.unreadable h' perm_of pos pos' /\
    live_input_buffer h' sl perm_of /\
    res == contents p h (slice_of sl) pos
  ))
let read_with_perm #k #t #p r #len base pos n perm_of =
  let h0 = HST.get () in
  LPL.valid_facts p h0 (slice_of base) pos;
  LPL.parser_kind_prop_equiv k p;
  [@inline_let] let sl' : LPL.slice triv triv = { LPL.base = base; LPL.len = pos `U32.add` n } in
  LPL.parse_strong_prefix p (LPL.bytes_of_slice_from h0 (slice_of base) pos) (LPL.bytes_of_slice_from h0 sl' pos);
  LPL.valid_facts p h0 sl' pos;
  let pos' = Ghost.hide (LPL.get_valid_pos p h0 sl' pos) in
  drop base pos pos' perm_of ;
  let h1 = HST.get () in
  let prf (h2: HS.mem) : Lemma
    (requires (B.modifies B.loc_none h1 h2))
    (ensures (
      R.preserved perm_of 0ul pos h0 h2 /\
      R.preserved perm_of pos' (B.len (slice_of base).LPL.base) h0 h2 /\
      R.unreadable h2 perm_of pos pos' /\
      live_input_buffer h2 base perm_of
    ))
    [SMTPat (B.modifies B.loc_none h1 h2)] // this lemma *with SMT pattern* allows tail call to the leaf reader, thus removing spurious temporary assignments in the generated C code
  =
    R.valid_perm_frame h1 perm_of B.loc_none h2;
    R.preserved_split perm_of 0ul pos (B.len base) h1 h2;
    R.preserved_split perm_of pos pos' (B.len base) h1 h2;
    R.preserved_trans perm_of 0ul pos h0 h1 h2;
    R.preserved_trans perm_of pos' (B.len base) h0 h1 h2
  in
  r sl' pos
val read_with_perm
  (#k: parser_kind)
  (#t: Type u#0)
  (#p: parser k t)
  (r: leaf_reader p)
  (#len: Ghost.erased U32.t)
  (sl: input_buffer_t len)
  (pos: U32.t)
  (n: U32.t)
  (perm_of: R.perm (slice_of sl).base)
: HST.Stack t
  (requires (fun h ->
    valid_input_buffer p h sl perm_of pos /\
    k.LPL.parser_kind_subkind == Some LPL.ParserStrong /\
    k.LPL.parser_kind_high == Some k.LPL.parser_kind_low /\
    k.LPL.parser_kind_low == U32.v n /\
    R.readable h perm_of pos (get_valid_pos p h (slice_of sl) pos)
  ))
  (ensures (fun h res h' ->
    let pos' = get_valid_pos p h (slice_of sl) pos in
    B.modifies (R.loc_perm perm_of) h h' /\
    R.preserved perm_of 0ul pos h h' /\
    R.preserved perm_of pos' (B.len (slice_of sl).LPL.base) h h' /\
    R.unreadable h' perm_of pos pos' /\
    live_input_buffer h' sl perm_of /\
    res == contents p h (slice_of sl) pos
  ))
let read_with_perm #k #t #p r #len base pos n perm_of =
let h0 = HST.get () in
LPL.valid_facts p h0 (slice_of base) pos;
LPL.parser_kind_prop_equiv k p;
[@@ inline_let ]let sl':LPL.slice triv triv = { LPL.base = base; LPL.len = pos `U32.add` n } in
LPL.parse_strong_prefix p
  (LPL.bytes_of_slice_from h0 (slice_of base) pos)
  (LPL.bytes_of_slice_from h0 sl' pos);
LPL.valid_facts p h0 sl' pos;
let pos' = Ghost.hide (LPL.get_valid_pos p h0 sl' pos) in
drop base pos pos' perm_of;
let h1 = HST.get () in
let prf (h2: HS.mem)
    : Lemma (requires (B.modifies B.loc_none h1 h2))
      (ensures
        (R.preserved perm_of 0ul pos h0 h2 /\
          R.preserved perm_of pos' (B.len (slice_of base).LPL.base) h0 h2 /\
          R.unreadable h2 perm_of pos pos' /\ live_input_buffer h2 base perm_of))
      [SMTPat (B.modifies B.loc_none h1 h2)] =
  R.valid_perm_frame h1 perm_of B.loc_none h2;
  R.preserved_split perm_of 0ul pos (B.len base) h1 h2;
  R.preserved_split perm_of pos pos' (B.len base) h1 h2;
  R.preserved_trans perm_of 0ul pos h0 h1 h2;
  R.preserved_trans perm_of pos' (B.len base) h0 h1 h2
in
r sl' pos
EverParse3d.InputBuffer.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Low.Base.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverParse3d.Readable.fsti.checked
EverParse3d.InputBuffer.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Low.Base.leaf_reader FStar.Ghost.erased FStar.UInt32.t EverParse3d.InputBuffer.input_buffer_t FStar.Ghost.reveal EverParse3d.Readable.perm LowParse.Bytes.byte LowParse.Slice.__proj__Mkslice__item__base EverParse3d.InputBuffer.triv EverParse3d.InputBuffer.slice_of FStar.Monotonic.HyperStack.mem Prims.unit LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_none Prims.squash Prims.l_and EverParse3d.Readable.preserved FStar.UInt32.uint_to_t LowStar.Monotonic.Buffer.len LowParse.Slice.buffer_srel_of_srel EverParse3d.Readable.unreadable EverParse3d.InputBuffer.live_input_buffer Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil EverParse3d.Readable.preserved_trans LowStar.Buffer.trivial_preorder FStar.UInt32.__uint_to_t EverParse3d.Readable.preserved_split EverParse3d.Readable.valid_perm_frame FStar.HyperStack.ST.get EverParse3d.InputBuffer.drop FStar.Ghost.hide LowParse.Low.Base.Spec.get_valid_pos LowParse.Low.Base.Spec.valid_facts LowParse.Spec.Base.parse_strong_prefix LowParse.Slice.bytes_of_slice_from LowParse.Slice.slice LowParse.Slice.Mkslice FStar.UInt32.add LowParse.Spec.Base.parser_kind_prop_equiv
module EverParse3d.InputBuffer

module B = LowStar.Buffer
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module U32 = FStar.UInt32
module LPL = LowParse.Low.Base
module R = EverParse3d.Readable
module G = FStar.Ghost

open LowParse.Low.Base

let input_buffer_t len =
  (base: B.buffer LPL.byte { U32.v len <= B.length base })

let slice_of #len x =
  { LPL.base = x; LPL.len = len }

let drop #len base from to perm_of =
    R.drop #byte #base perm_of from to
val read_with_perm
  (#k: parser_kind)
  (#t: Type u#0)
  (#p: parser k t)
  (r: leaf_reader p)
  (#len: Ghost.erased U32.t)
  (sl: input_buffer_t len)
  (pos: U32.t)
  (n: U32.t)
  (perm_of: R.perm (slice_of sl).base)
: HST.Stack t
  (requires (fun h ->
    valid_input_buffer p h sl perm_of pos /\
    k.LPL.parser_kind_subkind == Some LPL.ParserStrong /\
    k.LPL.parser_kind_high == Some k.LPL.parser_kind_low /\
    k.LPL.parser_kind_low == U32.v n /\
    R.readable h perm_of pos (get_valid_pos p h (slice_of sl) pos)
  ))
  (ensures (fun h res h' ->
    let pos' = get_valid_pos p h (slice_of sl) pos in
    B.modifies (R.loc_perm perm_of) h h' /\
    R.preserved perm_of 0ul pos h h' /\
    R.preserved perm_of pos' (B.len (slice_of sl).LPL.base) h h' /\
    R.unreadable h' perm_of pos pos' /\
    live_input_buffer h' sl perm_of /\
    res == contents p h (slice_of sl) pos
  ))

    r: LowParse.Low.Base.leaf_reader p ->
    sl: EverParse3d.InputBuffer.input_buffer_t (FStar.Ghost.reveal len) ->
    pos: FStar.UInt32.t ->
    n: FStar.UInt32.t ->
    perm_of: EverParse3d.Readable.perm (Mkslice?.base (EverParse3d.InputBuffer.slice_of sl))
  -> FStar.HyperStack.ST.Stack t