val validate_filter
       (name: string)
       (#nz:_)
       (#k:parser_kind nz WeakKindStrongPrefix)
       (#t:Type)
       (#[@@@erasable] p:parser k t)
       (#[@@@erasable] inv:slice_inv)
       (#[@@@erasable] l:eloc)
       (v:validate_with_action_t p inv l true)
       (r:leaf_reader p)
       (f:t -> bool)
       (cr:string)
       (cf:string)
  : validate_with_action_t (p `parse_filter` f) inv l false
let validate_filter (name: string) #nz (#k:parser_kind nz _) (#t:_) (#p:parser k t)
                    #inv #l (v:validate_with_action_t p inv l true)
                    (r:leaf_reader p) (f:t -> bool) (cr:string) (cf:string)
  : Tot (validate_with_action_t #nz #WeakKindStrongPrefix (p `LPC.parse_filter` f) inv l false)
  = fun ctxt error_handler_fn input input_length start_position ->
    [@inline_let] let pos = start_position in
    let h = HST.get () in
    LPC.parse_filter_eq p f (I.get_remaining input h);
    [@(rename_let ("positionAfter" ^ name))]
    let res = v ctxt error_handler_fn input input_length pos in
    let h1 = HST.get () in
    if LPE.is_error res
    then res
    else begin
      LowStar.Comment.comment cr;
      [@(rename_let ("" ^ name))]
      let field_value = r input pos in
      LowStar.Comment.comment (normalize_term ("start: " ^cf));
      [@(rename_let (name ^ "ConstraintIsOk"))]
      let ok = f field_value in
      LowStar.Comment.comment (normalize_term ("end: " ^ cf));
      LPE.check_constraint_ok ok res
    end
val validate_filter
       (name: string)
       (#nz:_)
       (#k:parser_kind nz WeakKindStrongPrefix)
       (#t:Type)
       (#[@@@erasable] p:parser k t)
       (#[@@@erasable] inv:slice_inv)
       (#[@@@erasable] l:eloc)
       (v:validate_with_action_t p inv l true)
       (r:leaf_reader p)
       (f:t -> bool)
       (cr:string)
       (cf:string)
  : validate_with_action_t (p `parse_filter` f) inv l false
let validate_filter
      (name: string)
      #nz
      (#k: parser_kind nz _)
      (#t: _)
      (#p: parser k t)
      #inv
      #l
      (v: validate_with_action_t p inv l true)
      (r: leaf_reader p)
      (f: (t -> bool))
      (cr: string)
      (cf: string)
    : Tot (validate_with_action_t #nz #WeakKindStrongPrefix (p `LPC.parse_filter` f) inv l false) =
fun ctxt error_handler_fn input input_length start_position ->
  [@@ inline_let ]let pos = start_position in
  let h = HST.get () in
  LPC.parse_filter_eq p f (I.get_remaining input h);
  [@@ (rename_let ("positionAfter" ^ name)) ]let res =
    v ctxt error_handler_fn input input_length pos
  in
  let h1 = HST.get () in
  if LPE.is_error res
  then res
  else
    (LowStar.Comment.comment cr;
      [@@ (rename_let ("" ^ name)) ]let field_value = r input pos in
      LowStar.Comment.comment (normalize_term ("start: " ^ cf));
      [@@ (rename_let (name ^ "ConstraintIsOk")) ]let ok = f field_value in
      LowStar.Comment.comment (normalize_term ("end: " ^ cf));
      LPE.check_constraint_ok ok res)
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.parser_kind EverParse3d.Kinds.WeakKindStrongPrefix EverParse3d.Prelude.parser EverParse3d.Actions.Base.slice_inv EverParse3d.Actions.Base.eloc EverParse3d.Actions.Base.validate_with_action_t EverParse3d.Actions.Base.leaf_reader 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 EverParse3d.ErrorCode.is_error FStar.UInt64.t EverParse3d.ErrorCode.check_constraint_ok Prims.unit LowStar.Comment.comment FStar.Pervasives.normalize_term Prims.op_Hat FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get LowParse.Spec.Combinators.parse_filter_eq EverParse3d.InputStream.Base.get_remaining LowParse.Spec.Combinators.parse_filter_kind LowParse.Spec.Combinators.parse_filter_refine LowParse.Spec.Combinators.parse_filter EverParse3d.Kinds.filter_kind EverParse3d.Prelude.refine EverParse3d.Prelude.parse_filter
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
  name v1 a
= validate_with_success_action' name (validate_drop v1) a

inline_for_extraction noextract
let validate_with_error_handler (typename:string) 
                                (fieldname:string)
                                #nz
                                #wk
                                (#k1:parser_kind nz wk)
                                 #t1
                                (#p1:parser k1 t1)
                                (#inv1:_)
                                (#l1:eloc)
                                (#ar:_)
                                (v1:validate_with_action_t p1 inv1 l1 ar)
  : validate_with_action_t p1 inv1 l1 ar
  = 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" ^ typename))]
    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 pos1
    else (
         error_handler_fn typename fieldname (LPE.error_reason_of_result pos1) (LPE.get_validator_error_kind pos1) ctxt input pos0;
         pos1
    )

inline_for_extraction noextract
let validate_ret
  : validate_with_action_t (parse_ret ()) true_inv eloc_none true
  = fun ctxt error_handler_fn input input_length start_position ->
    start_position

#push-options "--z3rlimit 32"

module LPC = LowParse.Spec.Combinators

inline_for_extraction noextract
let validate_pair
       (name1: string)
       #nz1 (#k1:parser_kind nz1 WeakKindStrongPrefix) #t1 (#p1:parser k1 t1)
       (#inv1:_) (#l1:eloc) (#ar1:_) (v1:validate_with_action_t p1 inv1 l1 ar1)
       #nz2 #wk2 (#k2:parser_kind nz2 wk2) #t2 (#p2:parser k2 t2)
       (#inv2:_) (#l2:eloc) (#ar2:_) (v2:validate_with_action_t p2 inv2 l2 ar2)
  : validate_with_action_t (p1 `parse_pair` p2) (conj_inv inv1 inv2) (l1 `eloc_union` l2) false
  = fun ctxt error_handler_fn input input_length start_position ->
    [@inline_let] let pos = start_position in
    let h = HST.get () in
    LPC.nondep_then_eq p1 p2 (I.get_remaining input h);
    [@(rename_let ("positionAfter" ^ name1))]
    let pos1 = validate_drop v1 ctxt error_handler_fn input input_length pos in
    let h1 = HST.get () in
    modifies_address_liveness_insensitive_unused_in h h1;
    if LPE.is_error pos1
    then
      pos1
    else
      validate_drop v2 ctxt error_handler_fn input input_length pos1

inline_for_extraction noextract
let validate_dep_pair
      (name1: string)
      #nz1 (#k1:parser_kind nz1 _) #t1 (#p1:parser k1 t1)
      #inv1 #l1 (v1:validate_with_action_t p1 inv1 l1 true) (r1: leaf_reader p1)
      #nz2 #wk2 (#k2:parser_kind nz2 wk2) (#t2:t1 -> Type) (#p2:(x:t1 -> parser k2 (t2 x)))
      #inv2 #l2 #ar2 (v2:(x:t1 -> validate_with_action_t (p2 x) inv2 l2 ar2))
  : Tot (validate_with_action_t (p1 `parse_dep_pair` p2) (conj_inv inv1 inv2) (l1 `eloc_union` l2) false)
  = fun ctxt error_handler_fn input input_length start_position ->
      [@inline_let] let pos = start_position in
      let h = HST.get () in
      LPC.parse_dtuple2_eq p1 p2 (I.get_remaining input h);
      [@(rename_let ("positionAfter" ^ name1))]
      let pos1 = v1 ctxt error_handler_fn input input_length pos in
      let h1 = HST.get() in
      if LPE.is_error pos1
      then begin
        pos1
      end
      else
        [@(rename_let ("" ^ name1))]
        let x = r1 input pos in
        let h15 = HST.get () in
        let _ = modifies_address_liveness_insensitive_unused_in h h15 in
        validate_drop (v2 x) ctxt error_handler_fn input input_length pos1

#pop-options

#push-options "--z3rlimit 64"
#restart-solver

inline_for_extraction noextract
let validate_dep_pair_with_refinement_and_action'
      (name1: string)
      (#nz1: _) (#k1:parser_kind nz1 _) (#t1: _) (#p1:parser k1 t1)
      (#inv1: _) (#l1: _) (v1:validate_with_action_t p1 inv1 l1 true) (r1: leaf_reader p1)
      (f: t1 -> bool)
      (#inv1': _) (#l1': _) (#b: _) (a:t1 -> action p1 inv1' l1' b bool)
      (#nz2: _) (#wk2: _) (#k2:parser_kind nz2 wk2) (#t2:refine _ f -> Type) (#p2:(x:refine _ f) -> parser k2 (t2 x))
      (#inv2: _) (#l2: _) (#ar2: _) (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 l2 ar2))
  : Tot (validate_with_action_t
             ((p1 `LPC.parse_filter` f) `(parse_dep_pair #nz1)` p2)
             (conj_inv inv1 (conj_inv inv1' inv2))
             (l1 `eloc_union` (l1' `eloc_union` l2))
             false)
  =
  fun ctxt error_handler_fn input input_length startPosition ->
      let h0 = HST.get () in
      LPC.parse_dtuple2_eq' #_ #_ (p1 `LPC.parse_filter` f) #_ #t2 p2 (I.get_remaining input h0);
      LPC.parse_filter_eq p1 f (I.get_remaining input h0);
      [@(rename_let ("positionAfter" ^ name1))]
      let res = v1 ctxt error_handler_fn input input_length startPosition in
      let h1 = HST.get() in
      modifies_address_liveness_insensitive_unused_in h0 h1;
      if LPE.is_error res
      then begin
        res
      end
      else begin
        assert (I.get_remaining input h1 == I.get_remaining input h0);
        [@(rename_let ("" ^ name1))]
        let field_value = r1 input startPosition in
        [@(rename_let (name1 ^ "ConstraintIsOk"))]
        let ok = f field_value in
        [@(rename_let ("positionAfter" ^ name1))]
        let res1 = LPE.check_constraint_ok ok res in
        let h2 = HST.get() in
        if LPE.is_error res1
        then
          res1
        else begin
             modifies_address_liveness_insensitive_unused_in h1 h2;
             if not (a field_value ctxt input startPosition res1)
             then LPE.set_validator_error_pos LPE.validator_error_action_failed res1 //action failed
             else begin
               let h15 = HST.get () in
               let _ = modifies_address_liveness_insensitive_unused_in h0 h15 in
               validate_drop (v2 field_value) ctxt error_handler_fn input input_length res1
             end
        end
      end

inline_for_extraction noextract
let validate_dep_pair_with_refinement_and_action_total_zero_parser'
      (name1: string)
      (#nz1: _) (#k1:parser_kind nz1 WeakKindStrongPrefix) (#t1: _) (#p1:parser k1 t1) (r1: leaf_reader p1)
      (inv1: _) (l1: _)
      (f: t1 -> bool)
      (#inv1': _) (#l1': _) (#b: _) (a:t1 -> action p1 inv1' l1' b bool)
      (#nz2: _) (#wk2: _) (#k2:parser_kind nz2 wk2) (#t2:refine _ f -> Type) (#p2:(x:refine _ f -> parser k2 (t2 x)))
      (#inv2: _) (#l2: _) (#ar2: _) (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 l2 ar2))
  : Pure (validate_with_action_t
             ((p1 `LPC.parse_filter` f) `(parse_dep_pair #nz1)` p2)
             (conj_inv inv1 (conj_inv inv1' inv2))
             (l1 `eloc_union` (l1' `eloc_union` l2))
             false)
         (requires (
           let open LP in
           k1.parser_kind_high == Some 0 /\
           k1.parser_kind_metadata == Some ParserKindMetadataTotal
         ))
         (ensures (fun _ -> True))
  = fun ctxt error_handler_fn input input_length startPosition ->
      let h0 = HST.get () in
      LPC.parse_dtuple2_eq' #_ #_ (p1 `LPC.parse_filter` f) #_ #t2 p2 (I.get_remaining input h0);
      LPC.parse_filter_eq p1 f (I.get_remaining input h0);
      [@inline_let] let _ = LP.parser_kind_prop_equiv k1 p1 in
      begin
        LowStar.Comment.comment ("Validating field " ^ name1);
        [@(rename_let ("" ^ name1))]
        let field_value = r1 input startPosition in
        [@(rename_let (name1 ^ "ConstraintIsOk"))]
        let ok = f field_value in
        [@(rename_let ("positionAfter" ^ name1))]
        let res1 = LPE.check_constraint_ok ok startPosition in
        if LPE.is_error res1
        then
             res1
        else let h2 = HST.get() in
             modifies_address_liveness_insensitive_unused_in h0 h2;
             if not (a field_value ctxt input startPosition res1)
             then LPE.set_validator_error_pos LPE.validator_error_action_failed startPosition //action failed
             else begin
               let h15 = HST.get () in
               let _ = modifies_address_liveness_insensitive_unused_in h0 h15 in
               validate_drop (v2 field_value) ctxt error_handler_fn input input_length res1
             end
        end

inline_for_extraction noextract
let validate_dep_pair_with_refinement_and_action
      (p1_is_constant_size_without_actions: bool)
      (name1: string)
      #nz1 (#k1:parser_kind nz1 _) #t1 (#p1:parser k1 t1)
      #inv1 #l1 (v1:validate_with_action_t p1 inv1 l1 true) (r1: leaf_reader p1)
      (f: t1 -> bool)
      #inv1' #l1' #b (a:t1 -> action p1 inv1' l1' b bool)
      #nz2 #wk2 (#k2:parser_kind nz2 wk2) (#t2:refine _ f -> Type) (#p2:(x:refine _ f -> parser k2 (t2 x)))
      #inv2 #l2 #ar2 (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 l2 ar2))
  : Tot (validate_with_action_t ((p1 `parse_filter` f) `parse_dep_pair` p2)
                                (conj_inv inv1 (conj_inv inv1' inv2))
                                (l1 `eloc_union` (l1' `eloc_union` l2))
                                false)
  = if
      p1_is_constant_size_without_actions `LP.bool_and`
      (k1.LP.parser_kind_high = Some 0) `LP.bool_and`
      (k1.LP.parser_kind_metadata = Some LP.ParserKindMetadataTotal)
    then
      validate_dep_pair_with_refinement_and_action_total_zero_parser' name1 r1 inv1 l1 f a v2
    else
      validate_dep_pair_with_refinement_and_action' name1 v1 r1 f a v2


inline_for_extraction noextract
let validate_dep_pair_with_action
      #nz1 (#k1:parser_kind nz1 _) #t1 (#p1:parser k1 t1)
      #inv1 #l1 (v1:validate_with_action_t p1 inv1 l1 true) (r1: leaf_reader p1)
      #inv1' #l1' #b (a:t1 -> action p1 inv1' l1' b bool)
      #nz2 #wk2 (#k2:parser_kind nz2 wk2) (#t2:t1 -> Type) (#p2:(x:t1 -> parser k2 (t2 x)))
      #inv2 #l2 #ar2 (v2:(x:t1 -> validate_with_action_t (p2 x) inv2 l2 ar2))
  : Tot (validate_with_action_t
             (p1 `(parse_dep_pair #nz1)` p2)
             (conj_inv inv1 (conj_inv inv1' inv2))
             (l1 `eloc_union` (l1' `eloc_union` l2))
             false)
  = fun ctxt error_handler_fn input input_length startPosition ->
      let h0 = HST.get () in
      LPC.parse_dtuple2_eq' #_ #_ p1 #_ #t2 p2 (I.get_remaining input h0);
      let res = v1 ctxt error_handler_fn input input_length startPosition in
      let h1 = HST.get() in
      modifies_address_liveness_insensitive_unused_in h0 h1;
      if LPE.is_error res
      then begin
        res
      end
      else begin
        let field_value = r1 input startPosition in
        let h2 = HST.get() in
        modifies_address_liveness_insensitive_unused_in h1 h2;
        let action_result = a field_value ctxt input startPosition res in
        let h3 = HST.get () in
        modifies_address_liveness_insensitive_unused_in h2 h3;
        if not action_result
        then LPE.set_validator_error_pos LPE.validator_error_action_failed res //action failed
        else
               validate_drop (v2 field_value) ctxt error_handler_fn input input_length res
      end

inline_for_extraction noextract
let validate_dep_pair_with_refinement'
      (name1: string)
      #nz1 (#k1:parser_kind nz1 _) #t1 (#p1:parser k1 t1)
      #inv1 #l1 (v1:validate_with_action_t p1 inv1 l1 true) (r1: leaf_reader p1)
      (f: t1 -> bool)
      #nz2 #wk2 (#k2:parser_kind nz2 wk2) (#t2:refine _ f -> Type) (#p2:(x:refine _ f -> parser k2 (t2 x)))
      #inv2 #l2 #ar2 (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 l2 ar2))
  : Tot (validate_with_action_t
             ((p1 `LPC.parse_filter` f) `(parse_dep_pair #nz1)` p2)
             (conj_inv inv1 inv2)
             (l1 `eloc_union` l2)
             false)
  = fun ctxt error_handler_fn input input_length startPosition ->
      let h0 = HST.get () in
      LPC.parse_dtuple2_eq' #_ #_ (p1 `LPC.parse_filter` f) #_ #t2 p2 (I.get_remaining input h0);
      LPC.parse_filter_eq p1 f (I.get_remaining input h0);
      [@(rename_let ("positionAfter" ^ name1))]
      let res = v1 ctxt error_handler_fn input input_length startPosition in
      let h1 = HST.get() in
      modifies_address_liveness_insensitive_unused_in h0 h1;
      if LPE.is_error res
      then begin
        res
      end
      else begin
        [@(rename_let ("" ^ name1))]
        let field_value = r1 input startPosition in
        [@(rename_let (name1 ^ "ConstraintIsOk"))]
        let ok = f field_value in
        [@(rename_let ("positionAfter" ^ name1))]
        let res1 = LPE.check_constraint_ok ok res in
        if LPE.is_error res1
        then
             res1
        else let h2 = HST.get() in
             // assert (B.modifies B.loc_none h1 h2);
             // assert (inv1' input.LPL.base h2);
             modifies_address_liveness_insensitive_unused_in h1 h2;
             // assert (loc_not_unused_in h2 `loc_includes` l1');
             // assert (valid_pos (p1 `(LPC.parse_filter #k1 #t1)` f) h0 input (uint64_to_uint32 pos) (uint64_to_uint32 res));
             let h15 = HST.get () in
             let _ = modifies_address_liveness_insensitive_unused_in h0 h15 in
             validate_drop (v2 field_value) ctxt error_handler_fn input input_length res1
        end

inline_for_extraction noextract
let validate_dep_pair_with_refinement_total_zero_parser'
      (name1: string)
      #nz1 (#k1:parser_kind nz1 _) #t1 (#p1:parser k1 t1)
      (inv1: _) (l1: _) (r1: leaf_reader p1)
      (f: t1 -> bool)
      #nz2 #wk2 (#k2:parser_kind nz2 wk2) (#t2:refine _ f -> Type) (#p2:(x:refine _ f -> parser k2 (t2 x)))
      #inv2 #l2 #ar2 (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 l2 ar2))
  : Pure (validate_with_action_t
             ((p1 `LPC.parse_filter` f) `(parse_dep_pair #nz1)` p2)
             (conj_inv inv1 inv2)
             (l1 `eloc_union` l2)
             false)
         (requires (
           let open LP in
           k1.parser_kind_high == Some 0 /\
           k1.parser_kind_metadata == Some ParserKindMetadataTotal
         ))
         (ensures (fun _ -> True))
  = fun ctxt error_handler_fn input input_length startPosition ->
      let h0 = HST.get () in
      LPC.parse_dtuple2_eq' #_ #_ (p1 `LPC.parse_filter` f) #_ #t2 p2 (I.get_remaining input h0);
      LPC.parse_filter_eq p1 f (I.get_remaining input h0);
      [@inline_let] let _ = LP.parser_kind_prop_equiv k1 p1 in
      begin
        LowStar.Comment.comment ("Validating field " ^ name1);
        [@(rename_let ("" ^ name1))]
        let field_value = r1 input startPosition in
        [@(rename_let (name1 ^ "ConstraintIsOk"))]
        let ok = f field_value in
        [@(rename_let ("positionAfter" ^ name1))]
        let res1 = LPE.check_constraint_ok ok startPosition in
        if LPE.is_error res1
        then res1
        else let h2 = HST.get() in
             // assert (B.modifies B.loc_none h1 h2);
             // assert (inv1' input.LPL.base h2);
             modifies_address_liveness_insensitive_unused_in h0 h2;
             // assert (loc_not_unused_in h2 `loc_includes` l1');
             // assert (valid_pos (p1 `(LPC.parse_filter #k1 #t1)` f) h0 input (uint64_to_uint32 pos) (uint64_to_uint32 res));
             let h15 = HST.get () in
             let _ = modifies_address_liveness_insensitive_unused_in h0 h15 in
             validate_drop (v2 field_value) ctxt error_handler_fn input input_length res1
        end

inline_for_extraction noextract
let validate_dep_pair_with_refinement
      (p1_is_constant_size_without_actions: bool)
      (name1: string)
      #nz1 (#k1:parser_kind nz1 _) #t1 (#p1:parser k1 t1)
      #inv1 #l1 (v1:validate_with_action_t p1 inv1 l1 true) (r1: leaf_reader p1)
      (f: t1 -> bool)
      #nz2 #wk2 (#k2:parser_kind nz2 wk2) (#t2:refine _ f -> Type) (#p2:(x:refine _ f -> parser k2 (t2 x)))
      #inv2 #l2 #ar2 (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 l2 ar2))
  : Tot (validate_with_action_t ((p1 `parse_filter` f) `parse_dep_pair` p2)
                                (conj_inv inv1 inv2)
                                (l1 `eloc_union` l2)
                                false)
  = if
      p1_is_constant_size_without_actions `LP.bool_and`
      (k1.LP.parser_kind_high = Some 0) `LP.bool_and`
      (k1.LP.parser_kind_metadata = Some LP.ParserKindMetadataTotal)
    then
      validate_dep_pair_with_refinement_total_zero_parser' name1 inv1 l1 r1 f v2
    else
      validate_dep_pair_with_refinement' name1 v1 r1 f v2

inline_for_extraction noextract
let validate_filter (name: string) #nz (#k:parser_kind nz _) (#t:_) (#p:parser k t)
                    #inv #l (v:validate_with_action_t p inv l true)
                    (r:leaf_reader p) (f:t -> bool) (cr:string) (cf:string)
val validate_filter
       (name: string)
       (#nz:_)
       (#k:parser_kind nz WeakKindStrongPrefix)
       (#t:Type)
       (#[@@@erasable] p:parser k t)
       (#[@@@erasable] inv:slice_inv)
       (#[@@@erasable] l:eloc)
       (v:validate_with_action_t p inv l true)
       (r:leaf_reader p)
       (f:t -> bool)
       (cr:string)
       (cf:string)
  : validate_with_action_t (p `parse_filter` f) inv l false

    name: Prims.string ->
    v: EverParse3d.Actions.Base.validate_with_action_t p inv l true ->
    r: EverParse3d.Actions.Base.leaf_reader p ->
    f: (_: t -> Prims.bool) ->
    cr: Prims.string ->
    cf: Prims.string
  -> EverParse3d.Actions.Base.validate_with_action_t (EverParse3d.Prelude.parse_filter p f)
      inv
      l
      false