val action
      (#nz:bool)
      (#wk: _)
      (#k:parser_kind nz wk)
      (#t:Type)
      (p:parser k t)
      (inv:slice_inv)
      (l:eloc)
      (on_success:bool)
      (a:Type)
    : Type0
let action
  p inv l on_success a
=
    (# [tcresolve ()] I.extra_t #input_buffer_t) ->
    ctxt: app_ctxt ->
    sl: input_buffer_t ->
    pos: LPE.pos_t ->
    posf: LPE.pos_t ->
    Stack a
      (requires fun h ->
        I.live sl h /\
        inv (I.footprint sl) h /\
        B.live h ctxt /\
        loc_not_unused_in h `loc_includes` app_loc ctxt l /\
        address_liveness_insensitive_locs `loc_includes` app_loc ctxt l /\
        app_loc ctxt l `loc_disjoint` I.footprint sl /\
        U64.v pos <= U64.v posf /\
        U64.v posf == Seq.length (I.get_read sl h)
      )
      (ensures fun h0 _ h1 ->
        let sl = Ghost.reveal sl in
        modifies (app_loc ctxt l) h0 h1 /\
        B.live h1 ctxt /\
        inv (I.footprint sl) h1)
val action
      (#nz:bool)
      (#wk: _)
      (#k:parser_kind nz wk)
      (#t:Type)
      (p:parser k t)
      (inv:slice_inv)
      (l:eloc)
      (on_success:bool)
      (a:Type)
    : Type0
let action p inv l on_success a =

    #[tcresolve ()]
      I.extra_t #input_buffer_t ->
    ctxt: app_ctxt ->
    sl: input_buffer_t ->
    pos: LPE.pos_t ->
    posf: LPE.pos_t
  -> Stack a
      (requires
        fun h ->
          I.live sl h /\ inv (I.footprint sl) h /\ B.live h ctxt /\
          (loc_not_unused_in h) `loc_includes` (app_loc ctxt l) /\
          address_liveness_insensitive_locs `loc_includes` (app_loc ctxt l) /\
          (app_loc ctxt l) `loc_disjoint` (I.footprint sl) /\ U64.v pos <= U64.v posf /\
          U64.v posf == Seq.length (I.get_read sl h))
      (ensures
        fun h0 _ h1 ->
          let sl = Ghost.reveal sl in
          modifies (app_loc ctxt l) h0 h1 /\ B.live h1 ctxt /\ inv (I.footprint sl) h1)
EverParse3d.Actions.Base.fst.checked
prims.fst.checked LowStar.Comment.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.List.fsti.checked LowParse.Spec.FLData.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked LowParse.Low.ListUpTo.fst.checked LowParse.Low.Int.fsti.checked LowParse.Low.FLData.fst.checked LowParse.Low.BoundedInt.fsti.checked LowParse.Low.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Tactics.Typeclasses.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked EverParse3d.Prelude.fst.checked EverParse3d.Kinds.fst.checked EverParse3d.InputStream.Base.fst.checked EverParse3d.InputStream.All.fsti.checked EverParse3d.ErrorCode.fst.checked C.Loops.fst.checked
EverParse3d.Actions.Base.fst
Prims.bool EverParse3d.Kinds.weak_kind EverParse3d.Kinds.parser_kind EverParse3d.Prelude.parser EverParse3d.Actions.Base.slice_inv EverParse3d.Actions.Base.eloc EverParse3d.InputStream.Base.extra_t EverParse3d.Actions.Base.input_buffer_t EverParse3d.InputStream.All.inst EverParse3d.Actions.Base.app_ctxt EverParse3d.ErrorCode.pos_t FStar.Monotonic.HyperStack.mem Prims.l_and EverParse3d.InputStream.Base.live EverParse3d.InputStream.Base.footprint LowStar.Monotonic.Buffer.live FStar.UInt8.t LowStar.Buffer.trivial_preorder LowStar.Monotonic.Buffer.loc_includes LowStar.Monotonic.Buffer.loc_not_unused_in FStar.Ghost.reveal LowStar.Monotonic.Buffer.loc EverParse3d.Actions.Base.app_loc LowStar.Monotonic.Buffer.address_liveness_insensitive_locs LowStar.Monotonic.Buffer.loc_disjoint Prims.b2t Prims.op_LessThanOrEqual FStar.UInt64.v Prims.eq2 Prims.int Prims.l_or Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt64.n FStar.Seq.Base.length EverParse3d.InputStream.Base.get_read LowStar.Monotonic.Buffer.modifies FStar.Ghost.hide
module EverParse3d.Actions.Base
friend EverParse3d.Kinds
friend EverParse3d.Prelude
open FStar.HyperStack.ST
open LowStar.Buffer
open LowStar.BufferOps
module B = LowStar.Buffer
module I = EverParse3d.InputStream.Base
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

module LPE = EverParse3d.ErrorCode
open FStar.Tactics.Typeclasses

module B = LowStar.Buffer
module U8 = FStar.UInt8
module P = EverParse3d.Prelude

let hinv = HS.mem -> Tot Type0
let liveness_inv = i:hinv {
  forall l h0 h1. {:pattern (i h1); (modifies l h0 h1)}  i h0 /\ modifies l h0 h1 /\ address_liveness_insensitive_locs `loc_includes` l ==> i h1
}
let mem_inv  = liveness_inv
let slice_inv = loc -> mem_inv
let inv_implies (inv0 inv1:slice_inv) =
  forall i h.
    inv0 i h ==> inv1 i h
let true_inv : slice_inv = fun _ _ -> True
let conj_inv (i0 i1:slice_inv) : slice_inv = fun sl h -> i0 sl h /\ i1 sl h
let eloc = (l: FStar.Ghost.erased B.loc { B.address_liveness_insensitive_locs `B.loc_includes` l })
let eloc_union (l1 l2:eloc) : Tot eloc = B.loc_union l1 l2
let eloc_none : eloc = B.loc_none
let eloc_includes (l1 l2:eloc) = B.loc_includes l1 l2 /\ True

let inv_implies_refl inv = ()
let inv_implies_true inv0 = ()
let inv_implies_conj inv0 inv1 inv2 h01 h02 = ()

let eloc_includes_none l = ()
let eloc_includes_union l0 l1 l2 h01 h02 = ()
let eloc_includes_refl l = ()

let bpointer a = B.pointer a
let ptr_loc #a (x:B.pointer a) : Tot eloc = B.loc_buffer x
let ptr_inv #a (x:B.pointer a) : slice_inv = fun (sl:_) h -> B.live h x


let app_ctxt = B.pointer U8.t
let app_loc (x:app_ctxt) (l:eloc) : eloc = B.loc_buffer x `loc_union` l

inline_for_extraction
noextract
let input_buffer_t = EverParse3d.InputStream.All.t

let action
  p inv l on_success a
val action
      (#nz:bool)
      (#wk: _)
      (#k:parser_kind nz wk)
      (#t:Type)
      (p:parser k t)
      (inv:slice_inv)
      (l:eloc)
      (on_success:bool)
      (a:Type)
    : Type0

    p: EverParse3d.Prelude.parser k t ->
    inv: EverParse3d.Actions.Base.slice_inv ->
    l: EverParse3d.Actions.Base.eloc ->
    on_success: Prims.bool ->
    a: Type
  -> Type0