val validate_with_success_action
      (name: string)
      (#nz:bool)
      (#wk: _)
      (#k1:parser_kind nz wk)
      (#[@@@erasable] t1:Type)
      (#[@@@erasable] p1:parser k1 t1)
      (#[@@@erasable] inv1:slice_inv)
      (#[@@@erasable] l1:eloc)
      (#allow_reading:bool)
      (v1:validate_with_action_t p1 inv1 l1 allow_reading)
      (#[@@@erasable] inv2:slice_inv)
      (#[@@@erasable] l2:eloc)
      (#b:bool)
      (a:action p1 inv2 l2 b bool)
  : validate_with_action_t p1 (conj_inv inv1 inv2) (l1 `eloc_union` l2) false
let validate_with_success_action
  name v1 a
= validate_with_success_action' name (validate_drop v1) a
val validate_with_success_action
      (name: string)
      (#nz:bool)
      (#wk: _)
      (#k1:parser_kind nz wk)
      (#[@@@erasable] t1:Type)
      (#[@@@erasable] p1:parser k1 t1)
      (#[@@@erasable] inv1:slice_inv)
      (#[@@@erasable] l1:eloc)
      (#allow_reading:bool)
      (v1:validate_with_action_t p1 inv1 l1 allow_reading)
      (#[@@@erasable] inv2:slice_inv)
      (#[@@@erasable] l2:eloc)
      (#b:bool)
      (a:action p1 inv2 l2 b bool)
  : validate_with_action_t p1 (conj_inv inv1 inv2) (l1 `eloc_union` l2) false
let validate_with_success_action name v1 a =
validate_with_success_action' name (validate_drop v1) a
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.string Prims.bool EverParse3d.Kinds.weak_kind EverParse3d.Kinds.parser_kind EverParse3d.Prelude.parser EverParse3d.Actions.Base.slice_inv EverParse3d.Actions.Base.eloc EverParse3d.Actions.Base.validate_with_action_t EverParse3d.Actions.Base.action EverParse3d.Actions.Base.validate_with_success_action' EverParse3d.Actions.Base.validate_drop EverParse3d.Actions.Base.conj_inv EverParse3d.Actions.Base.eloc_union
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
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 p inv l allow_reading = validate_with_action_t' p inv l allow_reading

let validate_eta v =
  fun ctxt error_handler_fn sl pos -> v ctxt error_handler_fn sl pos

let act_with_comment
  s res a
=
  fun ctxt sl pos posf ->
  LPL.comment s;
  a ctxt sl pos posf

let leaf_reader
  #nz
  #k
  (#t: Type)
  (p: parser k t)
: Tot Type
=
  (# [FStar.Tactics.Typeclasses.tcresolve ()] _extra_t : I.extra_t #input_buffer_t ) ->
  (sl: input_buffer_t) ->
  (pos: LPE.pos_t) ->
  Stack t
  (requires (fun h ->
    valid p h sl /\
    U64.v pos == Seq.length (I.get_read sl h)
  ))
  (ensures (fun h res h' ->
    let s = I.get_remaining sl h in
    I.live sl h' /\
    modifies (I.perm_footprint sl) h h' /\
    begin match LP.parse p s with
    | None -> False
    | Some (y, len) ->
      res == y /\
      I.get_remaining sl h' == Seq.slice s len (Seq.length s)
    end
  ))

#push-options "--z3rlimit 32"

inline_for_extraction
noextract
let validate_with_success_action' (name: string) #nz #wk (#k1:parser_kind nz wk) #t1 (#p1:parser k1 t1) (#inv1:_) (#l1:eloc)
                         (v1:validate_with_action_t p1 inv1 l1 false)
                         (#inv2:_) (#l2:eloc) #b (a:action p1 inv2 l2 b bool)
  : validate_with_action_t p1 (conj_inv inv1 inv2) (l1 `eloc_union` l2) false
  = fun ctxt error_handler_fn input input_length start_position ->
    [@inline_let] let pos0 = start_position in
    let h0 = HST.get () in
    [@(rename_let ("positionAfter" ^ name))]
    let pos1 = v1 ctxt error_handler_fn input input_length pos0 in
    let h1 = HST.get () in
    modifies_address_liveness_insensitive_unused_in h0 h1;
    if LPE.is_success pos1
    then
         [@(rename_let ("action_success_" ^ name))]
         let b = a ctxt input pos0 pos1 in
         let h2 = HST.get () in
         modifies_address_liveness_insensitive_unused_in h1 h2;
         if not b
         then LPE.set_validator_error_pos LPE.validator_error_action_failed pos1
         else pos1
    else
         pos1

inline_for_extraction
noextract
let validate_drop_true
   (#k:LP.parser_kind) (#t:Type) (#p:LP.parser k t) (#inv:slice_inv) (#l:eloc) (v: validate_with_action_t' p inv l true)
: Tot (validate_with_action_t' p inv l false)
= fun ctxt error_handler_fn input input_length start_position ->
  [@inline_let] let pos = start_position in
  let res = v ctxt error_handler_fn input input_length pos in
  I.skip_if_success input pos res;
  res

inline_for_extraction
noextract
let validate_drop
   (#k:LP.parser_kind) (#t:Type) (#p:LP.parser k t) (#inv:slice_inv) (#l:eloc) #allow_reading (v: validate_with_action_t' p inv l allow_reading)
: Tot (validate_with_action_t' p inv l false)
= if allow_reading
  then validate_drop_true v
  else v

let validate_with_success_action
val validate_with_success_action
      (name: string)
      (#nz:bool)
      (#wk: _)
      (#k1:parser_kind nz wk)
      (#[@@@erasable] t1:Type)
      (#[@@@erasable] p1:parser k1 t1)
      (#[@@@erasable] inv1:slice_inv)
      (#[@@@erasable] l1:eloc)
      (#allow_reading:bool)
      (v1:validate_with_action_t p1 inv1 l1 allow_reading)
      (#[@@@erasable] inv2:slice_inv)
      (#[@@@erasable] l2:eloc)
      (#b:bool)
      (a:action p1 inv2 l2 b bool)
  : validate_with_action_t p1 (conj_inv inv1 inv2) (l1 `eloc_union` l2) false

    name: Prims.string ->
    v1: EverParse3d.Actions.Base.validate_with_action_t p1 inv1 l1 allow_reading ->
    a: EverParse3d.Actions.Base.action p1 inv2 l2 b Prims.bool
  -> EverParse3d.Actions.Base.validate_with_action_t p1
      (EverParse3d.Actions.Base.conj_inv inv1 inv2)
      (EverParse3d.Actions.Base.eloc_union l1 l2)
      false