let validate_with_action_t' (#k:LP.parser_kind) (#t:Type) (p:LP.parser k t) (inv:slice_inv) (l:eloc) (allow_reading:bool) =
  (# [tcresolve ()] I.extra_t #input_buffer_t) ->
  (ctxt: app_ctxt) ->
  (error_handler_fn : error_handler) ->
  (sl: input_buffer_t) ->
  (len: I.tlen sl) ->
  (pos: LPE.pos_t) ->
  Stack U64.t
  (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 /\
    U64.v pos == Seq.length (I.get_read sl h) /\
    app_loc ctxt l `loc_disjoint` I.footprint sl
  )
  (ensures fun h res h' ->
    I.live sl h' /\
    modifies (app_loc ctxt l `loc_union` I.perm_footprint sl) h h' /\
    inv (I.footprint sl) h' /\
    B.live h' ctxt /\
    (((~ allow_reading) \/ LPE.is_error res) ==> U64.v (LPE.get_validator_error_pos res) == Seq.length (I.get_read sl h')) /\
    begin let s = I.get_remaining sl h in
    if LPE.is_success res
    then
      begin if allow_reading
      then U64.v res >= U64.v pos /\ valid_length p h sl (U64.v res - U64.v pos) /\ I.get_remaining sl h' == s
      else valid_consumed p h h' sl
      end
    else
      let s' = I.get_remaining sl h' in
      (LPE.get_validator_error_kind res <> LPE.get_validator_error_kind LPE.validator_error_action_failed ==> None? (LP.parse p s)) /\
      Seq.length s' <= Seq.length s /\
      s' `Seq.equal` Seq.slice s (Seq.length s - Seq.length s') (Seq.length s)
    end
    )
let validate_with_action_t'
      (#k: LP.parser_kind)
      (#t: Type)
      (p: LP.parser k t)
      (inv: slice_inv)
      (l: eloc)
      (allow_reading: bool)
     =

    #[tcresolve ()]
      I.extra_t #input_buffer_t ->
    ctxt: app_ctxt ->
    error_handler_fn: error_handler ->
    sl: input_buffer_t ->
    len: I.tlen sl ->
    pos: LPE.pos_t
  -> Stack U64.t
      (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) /\
          U64.v pos == Seq.length (I.get_read sl h) /\
          (app_loc ctxt l) `loc_disjoint` (I.footprint sl))
      (ensures
        fun h res h' ->
          I.live sl h' /\ modifies ((app_loc ctxt l) `loc_union` (I.perm_footprint sl)) h h' /\
          inv (I.footprint sl) h' /\ B.live h' ctxt /\
          (((~allow_reading) \/ LPE.is_error res) ==>
            U64.v (LPE.get_validator_error_pos res) == Seq.length (I.get_read sl h')) /\
          (let s = I.get_remaining sl h in
            if LPE.is_success res
            then
              if allow_reading
              then
                U64.v res >= U64.v pos /\ valid_length p h sl (U64.v res - U64.v pos) /\
                I.get_remaining sl h' == s
              else valid_consumed p h h' sl
            else
              let s' = I.get_remaining sl h' in
              (LPE.get_validator_error_kind res <>
                LPE.get_validator_error_kind LPE.validator_error_action_failed ==>
                None? (LP.parse p s)) /\ Seq.length s' <= Seq.length s /\
              s' `Seq.equal` (Seq.slice s (Seq.length s - Seq.length s') (Seq.length s))))
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
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser EverParse3d.Actions.Base.slice_inv EverParse3d.Actions.Base.eloc Prims.bool EverParse3d.InputStream.Base.extra_t EverParse3d.Actions.Base.input_buffer_t EverParse3d.InputStream.All.inst EverParse3d.Actions.Base.app_ctxt EverParse3d.Actions.Base.error_handler EverParse3d.InputStream.Base.tlen EverParse3d.ErrorCode.pos_t FStar.UInt64.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 Prims.eq2 Prims.int Prims.l_or Prims.b2t Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt64.n FStar.UInt64.v FStar.Seq.Base.length EverParse3d.InputStream.Base.get_read LowStar.Monotonic.Buffer.loc_disjoint LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_union EverParse3d.InputStream.Base.perm_footprint Prims.l_imp Prims.l_not EverParse3d.ErrorCode.is_error EverParse3d.ErrorCode.get_validator_error_pos EverParse3d.ErrorCode.is_success EverParse3d.Actions.Base.valid_length Prims.op_Subtraction FStar.Seq.Base.seq EverParse3d.InputStream.Base.get_remaining EverParse3d.Actions.Base.valid_consumed Prims.logical Prims.op_disEquality Prims.op_LessThanOrEqual Prims.op_LessThan EverParse3d.ErrorCode.get_validator_error_kind EverParse3d.ErrorCode.validator_error_action_failed FStar.Pervasives.Native.uu___is_None FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.consumed_length LowParse.Spec.Base.parse FStar.Seq.Base.equal FStar.Seq.Base.slice
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
=
    (# [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)

module LP = LowParse.Spec.Base
module LPL = LowParse.Low.Base

unfold
let valid_consumed
  (#input_buffer_t: Type0)
  (# [tcresolve ()] inst : I.input_stream_inst input_buffer_t)
  (#k: LP.parser_kind)
  (#t: Type)
  (p: LP.parser k t)
  (h: HS.mem)
  (h': HS.mem)
  (sl: input_buffer_t)
: Tot prop
= I.live sl h /\
  I.live sl h' /\
  begin
    let s = I.get_remaining sl h in
    begin match LP.parse p s with
    | None -> False
    | Some (_, len) -> I.get_remaining sl h' `Seq.equal` Seq.slice s len (Seq.length s)
    end
  end

unfold
let valid_length
  (#input_buffer_t: Type0)
  (# [tcresolve ()] inst : I.input_stream_inst input_buffer_t)
  (#k: LP.parser_kind)
  (#t: Type)
  (p: LP.parser k t)
  (h: HS.mem)
  (sl: input_buffer_t)
  (len: int)
: Tot prop
= I.live sl h /\
  begin
    let s = I.get_remaining sl h in
    begin match LP.parse p s with
    | None -> False
    | Some (_, len') -> len == len'
    end
  end

let valid
  (#input_buffer_t: Type0)
  (# [tcresolve ()] inst : I.input_stream_inst input_buffer_t)
  (#k: LP.parser_kind)
  (#t: Type)
  (p: LP.parser k t)
  (h: HS.mem)
  (sl: input_buffer_t)
: Tot prop
= I.live sl h /\
  Some? (LP.parse p (I.get_remaining sl h))

inline_for_extraction
let error_handler = 
    typename:string ->
    fieldname:string ->
    error_reason:string ->
    error_code:U64.t ->
    ctxt: app_ctxt ->
    sl: input_buffer_t ->
    pos: LPE.pos_t ->
    Stack unit
      (requires fun h ->
        I.live sl h /\
        true_inv (I.footprint sl) h /\
        B.live h ctxt /\
        loc_not_unused_in h `loc_includes` app_loc ctxt eloc_none /\
        address_liveness_insensitive_locs `loc_includes` app_loc ctxt eloc_none /\
        app_loc ctxt eloc_none `loc_disjoint` I.footprint sl /\
        U64.v pos <= Seq.length (I.get_read sl h)
      )
      (ensures fun h0 _ h1 ->
        let sl = Ghost.reveal sl in
        modifies (app_loc ctxt eloc_none) h0 h1 /\
        B.live h1 ctxt /\
        true_inv (I.footprint sl) h1)

inline_for_extraction noextract
val validate_with_action_t' : p: LowParse.Spec.Base.parser k t ->
    inv: EverParse3d.Actions.Base.slice_inv ->
    l: EverParse3d.Actions.Base.eloc ->
    allow_reading: Prims.bool
  -> Type0

    p: LowParse.Spec.Base.parser k t ->
    inv: EverParse3d.Actions.Base.slice_inv ->
    l: EverParse3d.Actions.Base.eloc ->
    allow_reading: Prims.bool
  -> Type0