From ae28570090954f94a7fefc4b98db4ddd9859a393 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 17 Oct 2024 17:16:15 -0700 Subject: [PATCH] track whether or not a validator has actions in an index; do no optimize array validation when the payload has an action --- src/3d/InterpreterTarget.fst | 68 +++-- src/3d/InterpreterTarget.fsti | 9 +- src/3d/Z3TestGen.fst | 4 +- src/3d/prelude/EverParse3d.Actions.Base.fst | 166 ++++++------ src/3d/prelude/EverParse3d.Actions.Base.fsti | 154 +++++++----- src/3d/prelude/EverParse3d.Interpreter.fst | 252 +++++++++++-------- 6 files changed, 381 insertions(+), 272 deletions(-) diff --git a/src/3d/InterpreterTarget.fst b/src/3d/InterpreterTarget.fst index 7df44508..823b8cd2 100644 --- a/src/3d/InterpreterTarget.fst +++ b/src/3d/InterpreterTarget.fst @@ -212,11 +212,11 @@ let dtyp_of_app (en: env) (hd:A.ident) (args:list T.index) DT_IType i | _ -> - let readable = match H.try_find en hd.v with + let has_action, readable = match H.try_find en hd.v with | None -> failwith "type not found" - | Some td -> td.allow_reading + | Some td -> td.has_action, td.allow_reading in - DT_App readable hd + DT_App has_action readable hd (List.map (function Inl _ -> failwith "Unexpected type application" | Inr e -> e) @@ -317,7 +317,7 @@ let rec typ_indexes_of_parser (en:env) (p:T.parser) match dt with | DT_IType _ -> typ_indexes_nil - | DT_App _ hd args -> + | DT_App _ _ hd args -> let td = match H.try_find en hd.v with | Some td -> td @@ -537,10 +537,43 @@ let rec allow_reading_of_typ (t:typ) begin match dt with | DT_IType i -> allow_reader_of_itype i - | DT_App readable _ _ -> readable + | DT_App has_action readable _ _ -> readable end - | _ -> false + | _ -> + false + +let rec has_action_of_typ (t:typ) + : Tot bool + = + match t with + | T_false _ -> false + | T_with_comment _ t _ -> has_action_of_typ t + | T_denoted _ dt -> + begin + match dt with + | DT_IType i -> false + | DT_App has_action readable _ _ -> has_action + end + | T_pair _ t1 t2 -> + has_action_of_typ t1 || has_action_of_typ t2 + | T_dep_pair _ t1 (_, t2) -> + has_action_of_dtyp t1 || has_action_of_typ t2 + | T_refine _ t _ -> has_action_of_dtyp t + | T_refine_with_action _ _ _ _ -> true + | T_dep_pair_with_refinement _ t _ (_, t2) -> has_action_of_dtyp t || has_action_of_typ t2 + | T_dep_pair_with_action _ _ _ _ -> true + | T_dep_pair_with_refinement_and_action _ _ _ _ _ -> true + | T_if_else _ t1 t2 -> has_action_of_typ t1 || has_action_of_typ t2 + | T_with_action _ _ _ -> true + | T_with_dep_action _ _ _ -> true + | T_drop t -> has_action_of_typ t + | T_with_comment _ t _ -> has_action_of_typ t + | T_nlist _ _ _ t -> has_action_of_typ t + | T_at_most _ _ t -> has_action_of_typ t + | T_exact _ _ t -> has_action_of_typ t + | T_string _ t _ -> has_action_of_dtyp t + | T_probe_then_validate _ t _ _ _ -> true let check_validity_of_typ_indexes (td:T.type_decl) indexes = let rec atomic_locs_of l = @@ -610,6 +643,7 @@ let translate_decls (en:env) (ds:T.decls) typ = typ; kind = td.decl_parser.p_kind; typ_indexes; + has_action = has_action_of_typ typ; allow_reading = ar; attrs = attrs; enum_typ = refined @@ -649,7 +683,7 @@ let print_dtyp (mname:string) (dt:dtyp) = | DT_IType i -> Printf.sprintf "(DT_IType %s)" (print_ityp i) - | DT_App _ hd args -> + | DT_App _ _ hd args -> Printf.sprintf "(%s %s)" (print_derived_name mname "dtyp" hd) (List.map (T.print_expr mname) args |> String.concat " ") @@ -893,7 +927,7 @@ let print_type_decl mname (td:type_decl) = FStar.Printf.sprintf "[@@specialize; noextract_to \"krml\"]\n\ noextract\n\ - let def_%s = ( %s <: Tot (typ _ _ _ _ _) by (T.norm [delta_attr [`%%specialize]; zeta; iota; primops]; T.smt()))\n" + let def_%s = ( %s <: Tot (typ _ _ _ _ _ _) by (T.norm [delta_attr [`%%specialize]; zeta; iota; primops]; T.smt()))\n" (print_typedef_name mname td.name) (print_typ mname td.typ) @@ -929,7 +963,7 @@ let rec print_disj' mname (d:disj) let print_disj mname = print_index (print_disj' mname) let print_td_iface is_entrypoint mname root_name binders args - inv eloc disj ar pk_wk pk_nz = + inv eloc disj ha ar pk_wk pk_nz = let ar = if is_entrypoint then false else ar in let kind_t = Printf.sprintf "[@@noextract_to \"krml\"]\n\ @@ -943,11 +977,12 @@ let print_td_iface is_entrypoint mname root_name binders args let def'_t = Printf.sprintf "[@@noextract_to \"krml\"]\n\ noextract\n\ - val def'_%s %s: typ kind_%s %s %s %s %b" + val def'_%s %s: typ kind_%s %s %s %s %b %b" root_name binders root_name inv disj eloc + ha ar in let validator_t = @@ -1006,13 +1041,14 @@ let print_binding mname (td:type_decl) "[@@specialize; noextract_to \"krml\"]\n\ noextract\n\ let def'_%s %s\n\ - : typ kind_%s %s %s %s %s\n\ + : typ kind_%s %s %s %s %b %b\n\ = coerce (_ by (coerce_validator [`%%kind_%s])) (def_%s %s)" root_name binders root_name inv disj eloc - (string_of_bool td.allow_reading) + td.has_action + td.allow_reading root_name root_name args @@ -1060,7 +1096,7 @@ let print_binding mname (td:type_decl) Printf.sprintf "[@@specialize; noextract_to \"krml\"]\n\ noextract\n\ let dtyp_%s %s\n\ - : dtyp kind_%s %b %s %s %s\n\ + : dtyp kind_%s %b %b %s %s %s\n\ = mk_dtyp_app\n\ kind_%s\n\ %s\n\ @@ -1070,10 +1106,11 @@ let print_binding mname (td:type_decl) (coerce (_ by (T.norm [delta_only [`%%type_%s]]; T.trefl())) (parser_%s %s))\n\ %s\n\ %b\n\ + %b\n\ (coerce (_ by %s) (validate_%s %s))\n\ (_ by (T.norm [delta_only [`%%Some?]; iota]; T.trefl()))\n" root_name binders - root_name td.allow_reading + root_name td.has_action td.allow_reading inv disj eloc root_name inv disj eloc @@ -1081,6 +1118,7 @@ let print_binding mname (td:type_decl) root_name root_name args reader + td.has_action td.allow_reading coerce_validator root_name args in @@ -1113,7 +1151,7 @@ let print_binding mname (td:type_decl) let iface = print_td_iface td.name.td_entrypoint mname root_name binders args - inv eloc disj td.allow_reading + inv eloc disj td.has_action td.allow_reading weak_kind k.pk_nz in impl, iface diff --git a/src/3d/InterpreterTarget.fsti b/src/3d/InterpreterTarget.fsti index 194c1289..c04b0a44 100644 --- a/src/3d/InterpreterTarget.fsti +++ b/src/3d/InterpreterTarget.fsti @@ -50,6 +50,7 @@ type dtyp : Type = i:itype -> dtyp | DT_App: + has_action:bool -> readable: bool -> hd:A.ident -> args:list expr -> @@ -58,8 +59,13 @@ type dtyp : Type = let allow_reader_of_dtyp (d: dtyp) : Tot bool = match d with | DT_IType i -> allow_reader_of_itype i - | DT_App readable _ _ -> readable + | DT_App _ readable _ _ -> readable +let has_action_of_dtyp d : Tot bool = + match d with + | DT_IType _ -> false + | DT_App has_action _ _ _ -> has_action + let readable_dtyp = (d: dtyp { allow_reader_of_dtyp d == true }) let non_empty_string = s:string { s <> "" } @@ -194,6 +200,7 @@ type type_decl = { typ : typ; kind : T.parser_kind; typ_indexes : typ_indexes; + has_action: bool; allow_reading: bool; attrs : (attrs: T.decl_attributes { attrs.is_entrypoint ==> ~ allow_reading }); enum_typ: option (t:T.typ {T.T_refine? t }) diff --git a/src/3d/Z3TestGen.fst b/src/3d/Z3TestGen.fst index b212a213..7e0fb34b 100644 --- a/src/3d/Z3TestGen.fst +++ b/src/3d/Z3TestGen.fst @@ -516,7 +516,7 @@ let parse_readable_dtyp : Tot (parser reading) = match d with | I.DT_IType i -> parse_readable_itype i - | I.DT_App _ hd args -> parse_readable_app hd args + | I.DT_App _ _ hd args -> parse_readable_app hd args let parse_not_readable_app' (hd: string) @@ -537,7 +537,7 @@ let parse_dtyp then wrap_parser (parse_readable_dtyp d) else match d with | I.DT_IType i -> parse_itype i - | I.DT_App _ hd args -> parse_not_readable_app hd args + | I.DT_App _ _ hd args -> parse_not_readable_app hd args let parse_false : parser not_reading = maybe_toplevel_parser (fun _ _ _ _ -> { call = "parse-false" }) diff --git a/src/3d/prelude/EverParse3d.Actions.Base.fst b/src/3d/prelude/EverParse3d.Actions.Base.fst index e44aad8c..8a76e2ea 100644 --- a/src/3d/prelude/EverParse3d.Actions.Base.fst +++ b/src/3d/prelude/EverParse3d.Actions.Base.fst @@ -237,6 +237,7 @@ let validate_with_action_t' (inv:slice_inv) (disj:disjointness_pre) (l:eloc) + (_has_action:bool) (allow_reading:bool) : Type = (# [EverParse3d.Util.solve_from_ctx ()] I.extra_t #input_buffer_t) -> @@ -277,7 +278,7 @@ let validate_with_action_t' end ) -let validate_with_action_t p inv disj l allow_reading = validate_with_action_t' p inv disj l allow_reading +let validate_with_action_t p inv disj l has_action allow_reading = validate_with_action_t' p inv disj l has_action allow_reading let validate_eta v = fun ctxt error_handler_fn sl pos -> v ctxt error_handler_fn sl pos @@ -324,15 +325,15 @@ let validate_with_success_action' (name: string) #nz #wk (#k1:parser_kind nz wk) #t1 (#p1:parser k1 t1) - (#inv1:_) (#disj1:_) (#l1:eloc) - (v1:validate_with_action_t p1 inv1 disj1 l1 false) + (#inv1:_) (#disj1:_) (#l1:eloc) #ha + (v1:validate_with_action_t p1 inv1 disj1 l1 ha false) (#inv2:_) (#disj2:_) (#l2:eloc) #b (a:action inv2 disj2 l2 b bool) : validate_with_action_t p1 (conj_inv inv1 inv2) (conj_disjointness disj1 disj2) (l1 `eloc_union` l2) - false + true false = fun ctxt error_handler_fn input input_length start_position -> [@inline_let] let pos0 = start_position in let h0 = HST.get () in @@ -360,9 +361,9 @@ let validate_drop_true (#p:LP.parser k t) (#inv:slice_inv) (#disj:disjointness_pre) - (#l:eloc) - (v: validate_with_action_t' p inv disj l true) -: Tot (validate_with_action_t' p inv disj l false) + (#l:eloc) #ha + (v: validate_with_action_t' p inv disj l ha true) +: Tot (validate_with_action_t' p inv disj l ha 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 @@ -378,9 +379,9 @@ let validate_drop (#inv:slice_inv) (#disj:disjointness_pre) (#l:eloc) - #allow_reading - (v: validate_with_action_t' p inv disj l allow_reading) -: Tot (validate_with_action_t' p inv disj l false) + #ha #allow_reading + (v: validate_with_action_t' p inv disj l ha allow_reading) +: Tot (validate_with_action_t' p inv disj l ha false) = if allow_reading then validate_drop_true v else v @@ -402,9 +403,9 @@ let validate_with_error_handler (#p1:parser k1 t1) (#inv1 #disj1:_) (#l1:eloc) - (#ar:_) - (v1:validate_with_action_t p1 inv1 disj1 l1 ar) - : validate_with_action_t p1 inv1 disj1 l1 ar + (#ha #ar:_) + (v1:validate_with_action_t p1 inv1 disj1 l1 ha ar) + : validate_with_action_t p1 inv1 disj1 l1 ha ar = fun ctxt error_handler_fn input input_length start_position -> [@inline_let] let pos0 = start_position in let h0 = HST.get () in @@ -421,7 +422,7 @@ let validate_with_error_handler inline_for_extraction noextract let validate_ret - : validate_with_action_t (parse_ret ()) true_inv disjointness_trivial eloc_none true + : validate_with_action_t (parse_ret ()) true_inv disjointness_trivial eloc_none false true = fun ctxt error_handler_fn input input_length start_position -> start_position @@ -433,9 +434,9 @@ inline_for_extraction noextract let validate_pair (name1: string) #nz1 (#k1:parser_kind nz1 WeakKindStrongPrefix) #t1 (#p1:parser k1 t1) - (#inv1 #disj1:_) (#l1:eloc) (#ar1:_) (v1:validate_with_action_t p1 inv1 disj1 l1 ar1) + (#inv1 #disj1:_) (#l1:eloc) (#ha1 #ar1:_) (v1:validate_with_action_t p1 inv1 disj1 l1 ha1 ar1) #nz2 #wk2 (#k2:parser_kind nz2 wk2) #t2 (#p2:parser k2 t2) - (#inv2 #disj2:_) (#l2:eloc) (#ar2:_) (v2:validate_with_action_t p2 inv2 disj2 l2 ar2) + (#inv2 #disj2:_) (#l2:eloc) (#ha2 #ar2:_) (v2:validate_with_action_t p2 inv2 disj2 l2 ha2 ar2) = fun ctxt error_handler_fn input input_length start_position -> [@inline_let] let pos = start_position in let h = HST.get () in @@ -454,9 +455,9 @@ inline_for_extraction noextract let validate_dep_pair (name1: string) #nz1 (#k1:parser_kind nz1 _) #t1 (#p1:parser k1 t1) - #inv1 #disj1 #l1 (v1:validate_with_action_t p1 inv1 disj1 l1 true) (r1: leaf_reader p1) + #inv1 #disj1 #l1 #ha1 (v1:validate_with_action_t p1 inv1 disj1 l1 ha1 true) (r1: leaf_reader p1) #nz2 #wk2 (#k2:parser_kind nz2 wk2) (#t2:t1 -> Type) (#p2:(x:t1 -> parser k2 (t2 x))) - #inv2 #disj2 #l2 #ar2 (v2:(x:t1 -> validate_with_action_t (p2 x) inv2 disj2 l2 ar2)) + #inv2 #disj2 #l2 #ha2 #ar2 (v2:(x:t1 -> validate_with_action_t (p2 x) inv2 disj2 l2 ha2 ar2)) = fun ctxt error_handler_fn input input_length start_position -> [@inline_let] let pos = start_position in let h = HST.get () in @@ -484,18 +485,19 @@ 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 #disj1 #l1: _) (v1:validate_with_action_t p1 inv1 disj1 l1 true) (r1: leaf_reader p1) + (#inv1 #disj1 #l1 #ha1: _) (v1:validate_with_action_t p1 inv1 disj1 l1 ha1 true) (r1: leaf_reader p1) (f: t1 -> bool) (#inv1' #disj1' #l1' #b: _) (a:t1 -> action inv1' disj1' l1' b bool) (#nz2 #wk2: _) (#k2:parser_kind nz2 wk2) (#t2:refine _ f -> Type) (#p2:(x:refine _ f) -> parser k2 (t2 x)) - (#inv2 #disj2 #l2 #ar2: _) (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 disj2 l2 ar2)) + (#inv2 #disj2 #l2 #ha2 #ar2: _) (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 disj2 l2 ha2 ar2)) : validate_with_action_t ((p1 `LPC.parse_filter` f) `(parse_dep_pair #nz1)` p2) (conj_inv inv1 (conj_inv inv1' inv2)) (conj_disjointness disj1 (conj_disjointness disj1' disj2)) (l1 `eloc_union` (l1' `eloc_union` l2)) + true false = fun ctxt error_handler_fn input input_length startPosition -> let h0 = HST.get () in @@ -543,12 +545,13 @@ let validate_dep_pair_with_refinement_and_action_total_zero_parser' (#inv1' #disj1' #l1' #b: _) (a:t1 -> action inv1' disj1' l1' b bool) (#nz2 #wk2: _) (#k2:parser_kind nz2 wk2) (#t2:refine _ f -> Type) (#p2:(x:refine _ f -> parser k2 (t2 x))) - (#inv2 #disj2 #l2 #ar2: _) (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 disj2 l2 ar2)) + (#inv2 #disj2 #l2 #ha2 #ar2: _) (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 disj2 l2 ha2 ar2)) : Pure (validate_with_action_t ((p1 `LPC.parse_filter` f) `(parse_dep_pair #nz1)` p2) (conj_inv inv1 (conj_inv inv1' inv2)) (conj_disjointness disj1 (conj_disjointness disj1' disj2)) (l1 `eloc_union` (l1' `eloc_union` l2)) + true false) (requires ( let open LP in @@ -588,12 +591,12 @@ 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 #disj1 #l1 (v1:validate_with_action_t p1 inv1 disj1 l1 true) + #inv1 #disj1 #l1 #ha1 (v1:validate_with_action_t p1 inv1 disj1 l1 ha1 true) (r1: leaf_reader p1) (f: t1 -> bool) #inv1' #disj1' #l1' #b (a:t1 -> action inv1' disj1' l1' b bool) #nz2 #wk2 (#k2:parser_kind nz2 wk2) (#t2:refine _ f -> Type) (#p2:(x:refine _ f -> parser k2 (t2 x))) - #inv2 #disj2 #l2 #ar2 (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 disj2 l2 ar2)) + #inv2 #disj2 #l2 #ha2 #ar2 (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 disj2 l2 ha2 ar2)) = if p1_is_constant_size_without_actions `LP.bool_and` (k1.LP.parser_kind_high = Some 0) `LP.bool_and` @@ -607,10 +610,10 @@ let validate_dep_pair_with_refinement_and_action inline_for_extraction noextract let validate_dep_pair_with_action #nz1 (#k1:parser_kind nz1 _) #t1 (#p1:parser k1 t1) - #inv1 #disj1 #l1 (v1:validate_with_action_t p1 inv1 disj1 l1 true) (r1: leaf_reader p1) + #inv1 #disj1 #l1 #ha1 (v1:validate_with_action_t p1 inv1 disj1 l1 ha1 true) (r1: leaf_reader p1) #inv1' #disj1' #l1' #b (a:t1 -> action inv1' disj1' l1' b bool) #nz2 #wk2 (#k2:parser_kind nz2 wk2) (#t2:t1 -> Type) (#p2:(x:t1 -> parser k2 (t2 x))) - #inv2 #disj2 #l2 #ar2 (v2:(x:t1 -> validate_with_action_t (p2 x) inv2 disj2 l2 ar2)) + #inv2 #disj2 #l2 #ha2 #ar2 (v2:(x:t1 -> validate_with_action_t (p2 x) inv2 disj2 l2 ha2 ar2)) = 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); @@ -638,15 +641,16 @@ inline_for_extraction noextract let validate_dep_pair_with_refinement' (name1: string) #nz1 (#k1:parser_kind nz1 _) #t1 (#p1:parser k1 t1) - #inv1 #disj1 #l1 (v1:validate_with_action_t p1 inv1 disj1 l1 true) (r1: leaf_reader p1) + #inv1 #disj1 #l1 #ha1 (v1:validate_with_action_t p1 inv1 disj1 l1 ha1 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 #disj2 #l2 #ar2 (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 disj2 l2 ar2)) + #inv2 #disj2 #l2 #ha2 #ar2 (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 disj2 l2 ha2 ar2)) : Tot (validate_with_action_t ((p1 `LPC.parse_filter` f) `(parse_dep_pair #nz1)` p2) (conj_inv inv1 inv2) (conj_disjointness disj1 disj2) (l1 `eloc_union` l2) + (ha1||ha2) false) = fun ctxt error_handler_fn input input_length startPosition -> let h0 = HST.get () in @@ -690,13 +694,14 @@ let validate_dep_pair_with_refinement_total_zero_parser' #nz2 #wk2 (#k2:parser_kind nz2 wk2) (#t2:refine _ f -> Type) (#p2:(x:refine _ f -> parser k2 (t2 x))) - #inv2 #disj2 #l2 #ar2 - (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 disj2 l2 ar2)) + #inv2 #disj2 #l2 #ha2 #ar2 + ha1 (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 disj2 l2 ha2 ar2)) : Pure (validate_with_action_t ((p1 `LPC.parse_filter` f) `(parse_dep_pair #nz1)` p2) (conj_inv inv1 inv2) (conj_disjointness disj1 disj2) (l1 `eloc_union` l2) + (ha1 || ha2) false) (requires ( let open LP in @@ -735,19 +740,19 @@ 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 #disj1 #l1 (v1:validate_with_action_t p1 inv1 disj1 l1 true) (r1: leaf_reader p1) + #inv1 #disj1 #l1 #ha1 (v1:validate_with_action_t p1 inv1 disj1 l1 ha1 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 #disj2 #l2 #ar2 - (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 disj2 l2 ar2)) + #inv2 #disj2 #l2 #ar2 #ha2 + (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 disj2 l2 ha2 ar2)) = 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 disj1 l1 r1 f v2 + validate_dep_pair_with_refinement_total_zero_parser' name1 inv1 disj1 l1 r1 f ha1 v2 else validate_dep_pair_with_refinement' name1 v1 r1 f v2 @@ -755,7 +760,7 @@ inline_for_extraction noextract let validate_filter (name: string) #nz (#k:parser_kind nz _) (#t:_) (#p:parser k t) - #inv #disj #l (v:validate_with_action_t p inv disj l true) + #inv #disj #l #ha (v:validate_with_action_t p inv disj l ha true) (r:leaf_reader p) (f:t -> bool) (cr:string) (cf:string) = fun ctxt error_handler_fn input input_length start_position -> [@inline_let] let pos = start_position in @@ -781,7 +786,7 @@ inline_for_extraction noextract let validate_filter_with_action (name: string) #nz (#k:parser_kind nz _) (#t:_) (#p:parser k t) - #inv #disj #l (v:validate_with_action_t p inv disj l true) + #inv #disj #l #ha (v:validate_with_action_t p inv disj l ha true) (r:leaf_reader p) (f:t -> bool) (cr:string) (cf:string) (#b:bool) #inva #disja (#la:eloc) (a: t -> action inva disja la b bool) @@ -815,8 +820,8 @@ inline_for_extraction noextract let validate_with_dep_action (name: string) #nz (#k:parser_kind nz _) (#t:_) (#p:parser k t) - #inv #disj #l - (v:validate_with_action_t p inv disj l true) + #inv #disj #l #ha + (v:validate_with_action_t p inv disj l ha true) (r:leaf_reader p) (#b:bool) #inva #disja (#la:eloc) (a: t -> action inva disja la b bool) @@ -841,9 +846,9 @@ let validate_with_dep_action inline_for_extraction noextract let validate_weaken #nz #wk (#k:parser_kind nz wk) #t (#p:parser k t) - #inv #disj #l #ar (v:validate_with_action_t p inv disj l ar) + #inv #disj #l #ha #ar (v:validate_with_action_t p inv disj l ha ar) #nz' #wk' (k':parser_kind nz' wk'{k' `is_weaker_than` k}) -: validate_with_action_t (parse_weaken p k') inv disj l ar +: validate_with_action_t (parse_weaken p k') inv disj l ha ar = fun ctxt error_handler_fn input input_length start_position -> v ctxt error_handler_fn input input_length start_position @@ -853,7 +858,7 @@ let validate_weaken inline_for_extraction noextract let validate_weaken_left #nz #wk (#k:parser_kind nz wk) (#t:_) (#p:parser k t) - #inv #disj #l #ar (v:validate_with_action_t p inv disj l ar) + #inv #disj #l #ar #ha (v:validate_with_action_t p inv disj l ha ar) #nz' #wk' (k':parser_kind nz' wk') = validate_weaken v (glb k' k) @@ -862,7 +867,7 @@ let validate_weaken_left inline_for_extraction noextract let validate_weaken_right #nz #wk (#k:parser_kind nz wk) (#t:_) (#p:parser k t) - #inv #disj #l #ar (v:validate_with_action_t p inv disj l ar) + #inv #disj #l #ar #ha (v:validate_with_action_t p inv disj l ha ar) #nz' #wk' (k':parser_kind nz' wk') = validate_weaken v (glb k k') @@ -939,8 +944,8 @@ let validate_list_body (#k:LP.parser_kind) #t (#p:LP.parser k t) - #inv #disj #l #ar - (v: validate_with_action_t' p inv disj l ar) + #inv #disj #l #ha #ar + (v: validate_with_action_t' p inv disj l ha ar) (g0 g1: Ghost.erased HS.mem) (ctxt:app_ctxt) (error_handler_fn:error_handler) @@ -974,8 +979,8 @@ let validate_list' (#k:LP.parser_kind) #t (#p:LP.parser k t) - #inv #disj #l #ar - (v: validate_with_action_t' p inv disj l ar) + #inv #disj #l #ha #ar + (v: validate_with_action_t' p inv disj l ha ar) (ctxt: app_ctxt) (error_handler_fn: error_handler) (sl: input_buffer_t) @@ -1039,9 +1044,9 @@ let validate_list (#k:LP.parser_kind) #t (#p:LP.parser k t) - #inv #disj #l #ar - (v: validate_with_action_t' p inv disj l ar) -: validate_with_action_t' (LowParse.Spec.List.parse_list p) inv disj l false + #inv #disj #l #ha #ar + (v: validate_with_action_t' p inv disj l ha ar) +: validate_with_action_t' (LowParse.Spec.List.parse_list p) inv disj l ha false = fun ctxt error_handler_fn input input_length start_position -> validate_list' v ctxt error_handler_fn input input_length start_position @@ -1057,9 +1062,9 @@ let validate_fldata_consumes_all (#k: LP.parser_kind) #t (#p: LP.parser k t) - #inv #disj #l #ar - (v: validate_with_action_t' p inv disj l ar { k.LP.parser_kind_subkind == Some LP.ParserConsumesAll }) -: validate_with_action_t' (LowParse.Spec.FLData.parse_fldata p (U32.v n)) inv disj l false + #inv #disj #l #ha #ar + (v: validate_with_action_t' p inv disj l ha ar { k.LP.parser_kind_subkind == Some LP.ParserConsumesAll }) +: validate_with_action_t' (LowParse.Spec.FLData.parse_fldata p (U32.v n)) inv disj l ha false = fun ctxt error_handler_fn input input_length start_position -> [@inline_let] let pos = start_position in let h = HST.get () in @@ -1094,9 +1099,9 @@ let validate_fldata (#k: LP.parser_kind) #t (#p: LP.parser k t) - #inv #disj #l #ar - (v: validate_with_action_t' p inv disj l ar) -: validate_with_action_t' (LowParse.Spec.FLData.parse_fldata p (U32.v n)) inv disj l false + #inv #disj #l #ha #ar + (v: validate_with_action_t' p inv disj l ha ar) +: validate_with_action_t' (LowParse.Spec.FLData.parse_fldata p (U32.v n)) inv disj l ha false = fun ctxt error_handler_fn input input_length start_position -> [@inline_let] let pos = start_position in let h = HST.get () in @@ -1138,9 +1143,9 @@ let validate_nlist (#k:parser_kind true wk) #t (#p:parser k t) - #inv #disj #l #ar - (v: validate_with_action_t p inv disj l ar) -: Tot (validate_with_action_t (parse_nlist n p) inv disj l false) + #inv #disj #l #ha #ar + (v: validate_with_action_t p inv disj l ha ar) +: Tot (validate_with_action_t (parse_nlist n p) inv disj l ha false) = validate_weaken #false #WeakKindStrongPrefix #(LowParse.Spec.FLData.parse_fldata_kind (U32.v n) LowParse.Spec.List.parse_list_kind) #(list t) (validate_fldata_consumes_all n (validate_list v)) @@ -1159,7 +1164,7 @@ let validate_total_constant_size_no_read' k.LP.parser_kind_metadata == Some LP.ParserKindMetadataTotal }) inv disj l -: validate_with_action_t' p inv disj l true +: validate_with_action_t' p inv disj l false true = fun ctxt error_handler_fn input input_length start_position -> [@inline_let] let pos = start_position in let h = HST.get () in @@ -1185,7 +1190,7 @@ let validate_total_constant_size_no_read k.LP.parser_kind_metadata == Some LP.ParserKindMetadataTotal }) inv disj l -: Tot (validate_with_action_t p inv disj l true) +: Tot (validate_with_action_t p inv disj l false true) = validate_total_constant_size_no_read' p sz u inv disj l inline_for_extraction noextract @@ -1198,7 +1203,7 @@ let validate_nlist_total_constant_size_mod_ok inv disj l - : Pure (validate_with_action_t (parse_nlist n p) inv disj l true) + : Pure (validate_with_action_t (parse_nlist n p) inv disj l false true) (requires ( let open LP in k.parser_kind_subkind == Some ParserStrong /\ @@ -1225,7 +1230,7 @@ let validate_nlist_constant_size_mod_ko #t (p:parser k t) inv disj l - : Pure (validate_with_action_t (parse_nlist n p) inv disj l true) + : Pure (validate_with_action_t (parse_nlist n p) inv disj l false true) (requires ( let open LP in k.parser_kind_subkind == Some ParserStrong /\ @@ -1262,7 +1267,7 @@ let validate_nlist_total_constant_size' #t (p:parser k t) inv disj l - : Pure (validate_with_action_t (parse_nlist n p) inv disj l true) + : Pure (validate_with_action_t (parse_nlist n p) inv disj l false true) (requires ( let open LP in k.parser_kind_subkind == Some ParserStrong /\ @@ -1285,7 +1290,7 @@ let validate_nlist_total_constant_size (#t: Type) (p:parser k t) inv disj l -: Pure (validate_with_action_t (parse_nlist n p) inv disj l true) +: Pure (validate_with_action_t (parse_nlist n p) inv disj l false true) (requires ( let open LP in k.parser_kind_subkind = Some ParserStrong /\ @@ -1321,8 +1326,8 @@ let validate_nlist_constant_size_without_actions #wk (#k:parser_kind true wk) #t (#p:parser k t) #inv #disj #l #ar - (v: validate_with_action_t p inv disj l ar) -: Tot (validate_with_action_t (parse_nlist n p) inv disj l false) + (v: validate_with_action_t p inv disj l false ar) +: Tot (validate_with_action_t (parse_nlist n p) inv disj l false false) = if payload_is_constant_size then ( @@ -1346,8 +1351,8 @@ let validate_nlist_constant_size_without_actions noextract inline_for_extraction let validate_t_at_most (n:U32.t) #nz #wk (#k:parser_kind nz wk) (#t:_) (#p:parser k t) - #inv #disj #l #ar (v:validate_with_action_t p inv disj l ar) - : Tot (validate_with_action_t (parse_t_at_most n p) inv disj l false) + #inv #disj #l #ha #ar (v:validate_with_action_t p inv disj l ha ar) + : Tot (validate_with_action_t (parse_t_at_most n p) inv disj l ha false) = fun ctxt error_handler_fn input input_length start_position -> [@inline_let] let pos = start_position in let h = HST.get () in @@ -1386,9 +1391,9 @@ let validate_t_at_most noextract inline_for_extraction let validate_t_exact (n:U32.t) #nz #wk (#k:parser_kind nz wk) (#t:_) (#p:parser k t) - #inv #disj #l #ar - (v:validate_with_action_t p inv disj l ar) -: validate_with_action_t (parse_t_exact n p) inv disj l false + #inv #disj #l #ha #ar + (v:validate_with_action_t p inv disj l ha ar) +: validate_with_action_t (parse_t_exact n p) inv disj l ha false = fun ctxt error_handler_fn input input_length start_position -> [@inline_let] let pos = start_position in let h = HST.get () in @@ -1427,8 +1432,8 @@ inline_for_extraction noextract let validate_with_comment (c:string) #nz #wk (#k:parser_kind nz wk) #t (#p:parser k t) - #inv #disj #l #ar (v:validate_with_action_t p inv disj l ar) -: validate_with_action_t p inv disj l ar + #inv #disj #l #ha #ar (v:validate_with_action_t p inv disj l ha ar) +: validate_with_action_t p inv disj l ha ar = fun ctxt error_handler_fn input input_length start_position -> LowParse.Low.Base.comment c; v ctxt error_handler_fn input input_length start_position @@ -1436,12 +1441,12 @@ let validate_with_comment inline_for_extraction noextract let validate_weaken_inv_loc #nz #wk (#k:parser_kind nz wk) #t (#p:parser k t) - #inv #disj (#l:eloc) #ar + #inv #disj (#l:eloc) #ha #ar (inv':slice_inv{inv' `inv_implies` inv}) (disj':_{ disj' `imp_disjointness` disj}) (l':eloc{l' `eloc_includes` l}) - (v:validate_with_action_t p inv disj l ar) - : Tot (validate_with_action_t p inv' disj' l' ar) + (v:validate_with_action_t p inv disj l ha ar) + : Tot (validate_with_action_t p inv' disj' l' ha ar) = v @@ -1710,7 +1715,7 @@ let validate_list_up_to (prf: LUT.consumes_if_not_cond (cond_string_up_to terminator) p) : validate_with_action_t #true #WeakKindStrongPrefix (LUT.parse_list_up_to (cond_string_up_to terminator) p prf) - true_inv disjointness_trivial eloc_none false + true_inv disjointness_trivial eloc_none false false = fun ctxt error_handler_fn sl sl_len pos -> let h0 = HST.get () in HST.push_frame (); @@ -1731,11 +1736,12 @@ let validate_string (#k: parser_kind true WeakKindStrongPrefix) (#t: eqtype) (#[@@@erasable] p: parser k t) - (v: validator p) + (#ha:_) + (v: validator_maybe_action p ha) (r: leaf_reader p) (terminator: t) = LP.parser_kind_prop_equiv k p; - validate_weaken (validate_list_up_to v r terminator (fun _ _ _ -> ())) _ + validate_list_up_to v r terminator (fun _ _ _ -> ()) let validate_all_bytes = fun _ _ input input_length start_position -> I.empty input input_length start_position @@ -1869,8 +1875,8 @@ let probe_then_validate (#inv:slice_inv) (#disj:_) (#l:eloc) - (#allow_reading:bool) - (v:validate_with_action_t p inv disj l allow_reading) + (#ha #allow_reading:bool) + (v:validate_with_action_t p inv disj l ha allow_reading) (src:U64.t) (len:U64.t) (dest:CP.copy_buffer_t) diff --git a/src/3d/prelude/EverParse3d.Actions.Base.fsti b/src/3d/prelude/EverParse3d.Actions.Base.fsti index c28aa203..a23cc3db 100644 --- a/src/3d/prelude/EverParse3d.Actions.Base.fsti +++ b/src/3d/prelude/EverParse3d.Actions.Base.fsti @@ -154,6 +154,7 @@ val validate_with_action_t (liveness_inv:slice_inv) (disj:disjointness_pre) (l:eloc) + (has_action:bool) (allow_reading:bool) : Type0 @@ -167,9 +168,9 @@ val validate_eta (#[@@@erasable] inv:slice_inv) (#[@@@erasable] disj:disjointness_pre) (#[@@@erasable] l:eloc) - (#allow_reading:bool) - (v: validate_with_action_t p inv disj l allow_reading) -: Tot (validate_with_action_t p inv disj l allow_reading) + (#has_action #allow_reading:bool) + (v: validate_with_action_t p inv disj l has_action allow_reading) +: Tot (validate_with_action_t p inv disj l has_action allow_reading) inline_for_extraction noextract val act_with_comment @@ -200,9 +201,9 @@ val validate_without_reading (#[@@@erasable] inv:slice_inv) (#[@@@erasable] disj:disjointness_pre) (#[@@@erasable] l:eloc) - (#allow_reading:bool) - (v: validate_with_action_t p inv disj l allow_reading) -: Tot (validate_with_action_t p inv disj l false) + (#has_action #allow_reading:bool) + (v: validate_with_action_t p inv disj l has_action allow_reading) +: Tot (validate_with_action_t p inv disj l has_action false) inline_for_extraction noextract val validate_with_success_action @@ -215,14 +216,14 @@ val validate_with_success_action (#[@@@erasable] inv1:slice_inv) (#[@@@erasable] disj1:disjointness_pre) (#[@@@erasable] l1:eloc) - (#allow_reading:bool) - (v1:validate_with_action_t p1 inv1 disj1 l1 allow_reading) + (#has_action #allow_reading:bool) + (v1:validate_with_action_t p1 inv1 disj1 l1 has_action allow_reading) (#[@@@erasable] inv2:slice_inv) (#[@@@erasable] disj2:disjointness_pre) (#[@@@erasable] l2:eloc) (#b:bool) (a:action inv2 disj2 l2 b bool) - : validate_with_action_t p1 (conj_inv inv1 inv2) (conj_disjointness disj1 disj2) (l1 `eloc_union` l2) false + : validate_with_action_t p1 (conj_inv inv1 inv2) (conj_disjointness disj1 disj2) (l1 `eloc_union` l2) true false inline_for_extraction noextract val validate_with_error_handler @@ -236,13 +237,13 @@ val validate_with_error_handler (#[@@@erasable] inv1:slice_inv) (#[@@@erasable] disj:disjointness_pre) (#[@@@erasable] l1:eloc) - (#ar:_) - (v1:validate_with_action_t p1 inv1 disj l1 ar) - : validate_with_action_t p1 inv1 disj l1 ar + (#has_action #ar:_) + (v1:validate_with_action_t p1 inv1 disj l1 has_action ar) + : validate_with_action_t p1 inv1 disj l1 has_action ar inline_for_extraction noextract val validate_ret - : validate_with_action_t (parse_ret ()) true_inv disjointness_trivial eloc_none true + : validate_with_action_t (parse_ret ()) true_inv disjointness_trivial eloc_none false true inline_for_extraction noextract val validate_pair @@ -254,8 +255,8 @@ val validate_pair (#[@@@erasable] inv1:slice_inv) (#[@@@erasable] disj1:disjointness_pre) (#[@@@erasable] l1:eloc) - (#allow_reading1:bool) - (v1:validate_with_action_t p1 inv1 disj1 l1 allow_reading1) + (#has_action1 #allow_reading1:bool) + (v1:validate_with_action_t p1 inv1 disj1 l1 has_action1 allow_reading1) (#nz2:_) (#wk2: _) (#k2:parser_kind nz2 wk2) @@ -264,13 +265,14 @@ val validate_pair (#[@@@erasable] inv2:slice_inv) (#[@@@erasable] disj2:disjointness_pre) (#[@@@erasable] l2:eloc) - (#allow_reading2:bool) - (v2:validate_with_action_t p2 inv2 disj2 l2 allow_reading2) + (#has_action2 #allow_reading2:bool) + (v2:validate_with_action_t p2 inv2 disj2 l2 has_action2 allow_reading2) : validate_with_action_t (p1 `parse_pair` p2) (conj_inv inv1 inv2) (conj_disjointness disj1 disj2) (l1 `eloc_union` l2) + (has_action1 || has_action2) false inline_for_extraction noextract @@ -283,7 +285,8 @@ val validate_dep_pair (#[@@@erasable] inv1:slice_inv) (#[@@@erasable] disj1:disjointness_pre) (#[@@@erasable] l1:eloc) - (v1:validate_with_action_t p1 inv1 disj1 l1 true) + (#has_action1:_) + (v1:validate_with_action_t p1 inv1 disj1 l1 has_action1 true) (r1: leaf_reader p1) (#nz2:_) (#wk2: _) @@ -293,13 +296,14 @@ val validate_dep_pair (#[@@@erasable] inv2:slice_inv) (#[@@@erasable] disj2:disjointness_pre) (#[@@@erasable] l2:eloc) - (#allow_reading2:bool) - (v2:(x:t1 -> validate_with_action_t (p2 x) inv2 disj2 l2 allow_reading2)) + (#has_action2 #allow_reading2:bool) + (v2:(x:t1 -> validate_with_action_t (p2 x) inv2 disj2 l2 has_action2 allow_reading2)) : validate_with_action_t (p1 `parse_dep_pair` p2) (conj_inv inv1 inv2) (conj_disjointness disj1 disj2) (l1 `eloc_union` l2) + (has_action1 || has_action2) false inline_for_extraction noextract @@ -313,7 +317,8 @@ val validate_dep_pair_with_refinement_and_action (#[@@@erasable] inv1:slice_inv) (#[@@@erasable] disj1:disjointness_pre) (#[@@@erasable] l1:eloc) - (v1:validate_with_action_t p1 inv1 disj1 l1 true) + (#has_action1:bool) + (v1:validate_with_action_t p1 inv1 disj1 l1 has_action1 true) (r1: leaf_reader p1) (f: t1 -> bool) (#[@@@erasable] inv1':slice_inv) @@ -329,13 +334,14 @@ val validate_dep_pair_with_refinement_and_action (#[@@@erasable] inv2:slice_inv) (#[@@@erasable] disj2:disjointness_pre) (#[@@@erasable] l2:eloc) - (#allow_reading2:bool) - (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 disj2 l2 allow_reading2)) + (#has_action2 #allow_reading2:bool) + (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 disj2 l2 has_action2 allow_reading2)) : validate_with_action_t ((p1 `parse_filter` f) `parse_dep_pair` p2) (conj_inv inv1 (conj_inv inv1' inv2)) (conj_disjointness disj1 (conj_disjointness disj1' disj2)) (l1 `eloc_union` (l1' `eloc_union` l2)) + true false inline_for_extraction noextract @@ -347,7 +353,8 @@ val validate_dep_pair_with_action (#[@@@erasable] inv1:slice_inv) (#[@@@erasable] disj1:disjointness_pre) (#[@@@erasable] l1:eloc) - (v1:validate_with_action_t p1 inv1 disj1 l1 true) + (#has_action1:_) + (v1:validate_with_action_t p1 inv1 disj1 l1 has_action1 true) (r1: leaf_reader p1) (#[@@@erasable] inv1':slice_inv) (#[@@@erasable] disj1':disjointness_pre) @@ -362,13 +369,14 @@ val validate_dep_pair_with_action (#[@@@erasable] inv2:slice_inv) (#[@@@erasable] disj2:disjointness_pre) (#[@@@erasable] l2:eloc) - (#allow_reading2:_) - (v2:(x:t1 -> validate_with_action_t (p2 x) inv2 disj2 l2 allow_reading2)) + (#has_action2 #allow_reading2:_) + (v2:(x:t1 -> validate_with_action_t (p2 x) inv2 disj2 l2 has_action2 allow_reading2)) : validate_with_action_t (p1 `(parse_dep_pair #nz1)` p2) (conj_inv inv1 (conj_inv inv1' inv2)) (conj_disjointness disj1 (conj_disjointness disj1' disj2)) (l1 `eloc_union` (l1' `eloc_union` l2)) + true false inline_for_extraction noextract @@ -382,7 +390,8 @@ val validate_dep_pair_with_refinement (#[@@@erasable] inv1:slice_inv) (#[@@@erasable] disj1:disjointness_pre) (#[@@@erasable] l1:eloc) - (v1:validate_with_action_t p1 inv1 disj1 l1 true) + (#has_action1:_) + (v1:validate_with_action_t p1 inv1 disj1 l1 has_action1 true) (r1: leaf_reader p1) (f: t1 -> bool) (#nz2:_) @@ -394,12 +403,14 @@ val validate_dep_pair_with_refinement (#[@@@erasable] disj2:disjointness_pre) (#[@@@erasable] l2:eloc) (#allow_reading2:bool) - (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 disj2 l2 allow_reading2)) + (#has_action2:_) + (v2:(x:refine _ f -> validate_with_action_t (p2 x) inv2 disj2 l2 has_action2 allow_reading2)) : validate_with_action_t ((p1 `parse_filter` f) `parse_dep_pair` p2) (conj_inv inv1 inv2) (conj_disjointness disj1 disj2) (l1 `eloc_union` l2) + (has_action1 || has_action2) false inline_for_extraction noextract @@ -412,12 +423,13 @@ val validate_filter (#[@@@erasable] inv:slice_inv) (#[@@@erasable] disj:disjointness_pre) (#[@@@erasable] l:eloc) - (v:validate_with_action_t p inv disj l true) + (#has_action:_) + (v:validate_with_action_t p inv disj l has_action true) (r:leaf_reader p) (f:t -> bool) (cr:string) (cf:string) - : validate_with_action_t (p `parse_filter` f) inv disj l false + : validate_with_action_t (p `parse_filter` f) inv disj l has_action false inline_for_extraction noextract val validate_filter_with_action @@ -429,7 +441,8 @@ val validate_filter_with_action (#[@@@erasable] inv:slice_inv) (#[@@@erasable] disj:disjointness_pre) (#[@@@erasable] l:eloc) - (v:validate_with_action_t p inv disj l true) + (#has_action:_) + (v:validate_with_action_t p inv disj l has_action true) (r:leaf_reader p) (f:t -> bool) (cr:string) @@ -444,6 +457,7 @@ val validate_filter_with_action (conj_inv inv inva) (conj_disjointness disj disja) (eloc_union l la) + true false inline_for_extraction noextract @@ -456,7 +470,8 @@ val validate_with_dep_action (#[@@@erasable] inv:slice_inv) (#[@@@erasable] disj:disjointness_pre) (#[@@@erasable] l:eloc) - (v:validate_with_action_t p inv disj l true) + (#has_action:_) + (v:validate_with_action_t p inv disj l has_action true) (r:leaf_reader p) (#b:bool) (#[@@@erasable] inva:slice_inv) @@ -468,6 +483,7 @@ val validate_with_dep_action (conj_inv inv inva) (conj_disjointness disj disja) (eloc_union l la) + true false inline_for_extraction noextract @@ -481,11 +497,12 @@ val validate_weaken_left (#[@@@erasable] disj:disjointness_pre) (#[@@@erasable] l:eloc) (#allow_reading:bool) - (v:validate_with_action_t p inv disj l allow_reading) + (#has_action:_) + (v:validate_with_action_t p inv disj l has_action allow_reading) (#nz':_) (#wk': _) (k':parser_kind nz' wk') - : validate_with_action_t (parse_weaken_left p k') inv disj l allow_reading + : validate_with_action_t (parse_weaken_left p k') inv disj l has_action allow_reading inline_for_extraction noextract val validate_weaken_right @@ -498,16 +515,17 @@ val validate_weaken_right (#[@@@erasable] disj:disjointness_pre) (#[@@@erasable] l:eloc) (#allow_reading:bool) - (v:validate_with_action_t p inv disj l allow_reading) + (#has_action:_) + (v:validate_with_action_t p inv disj l has_action allow_reading) (#nz':_) (#wk': _) (k':parser_kind nz' wk') - : validate_with_action_t (parse_weaken_right p k') inv disj l allow_reading + : validate_with_action_t (parse_weaken_right p k') inv disj l has_action allow_reading inline_for_extraction noextract val validate_impos (_:unit) - : validate_with_action_t (parse_impos ()) true_inv disjointness_trivial eloc_none true + : validate_with_action_t (parse_impos ()) true_inv disjointness_trivial eloc_none false true noextract inline_for_extraction val validate_ite @@ -520,20 +538,21 @@ val validate_ite (#[@@@erasable] inv1:slice_inv) (#[@@@erasable] disj1:disjointness_pre) (#[@@@erasable] l1:eloc) - (#ar1:_) + (#ha1 #ar1:_) (#[@@@erasable] inv2:slice_inv) (#[@@@erasable] disj2:disjointness_pre) (#[@@@erasable] l2:eloc) - (#ar2:_) + (#ha2 #ar2:_) ([@@@erasable] p1:squash e -> parser k (a())) - (v1:(squash e -> validate_with_action_t (p1()) inv1 disj1 l1 ar1)) + (v1:(squash e -> validate_with_action_t (p1()) inv1 disj1 l1 ha1 ar1)) ([@@@erasable] p2:squash (not e) -> parser k (b())) - (v2:(squash (not e) -> validate_with_action_t (p2()) inv2 disj2 l2 ar2)) + (v2:(squash (not e) -> validate_with_action_t (p2()) inv2 disj2 l2 ha2 ar2)) : validate_with_action_t (parse_ite e p1 p2) (conj_inv inv1 inv2) (conj_disjointness disj1 disj2) (l1 `eloc_union` l2) + (ha1 || ha2) false noextract inline_for_extraction @@ -546,9 +565,9 @@ val validate_nlist (#[@@@erasable] inv:slice_inv) (#[@@@erasable] disj:disjointness_pre) (#[@@@erasable] l:eloc) - (#allow_reading:bool) - (v: validate_with_action_t p inv disj l allow_reading) -: validate_with_action_t (parse_nlist n p) inv disj l false + (#ha #allow_reading:bool) + (v: validate_with_action_t p inv disj l ha allow_reading) +: validate_with_action_t (parse_nlist n p) inv disj l ha false noextract inline_for_extraction val validate_nlist_constant_size_without_actions @@ -563,8 +582,8 @@ val validate_nlist_constant_size_without_actions (#[@@@erasable] disj:disjointness_pre) (#[@@@erasable] l:eloc) (#allow_reading:bool) - (v: validate_with_action_t p inv disj l allow_reading) -: Tot (validate_with_action_t (parse_nlist n p) inv disj l false) + (v: validate_with_action_t p inv disj l false allow_reading) +: Tot (validate_with_action_t (parse_nlist n p) inv disj l false false) noextract inline_for_extraction val validate_t_at_most @@ -577,9 +596,9 @@ val validate_t_at_most (#[@@@erasable] inv:slice_inv) (#[@@@erasable] disj:disjointness_pre) (#[@@@erasable] l:eloc) - (#ar:_) - (v:validate_with_action_t p inv disj l ar) - : Tot (validate_with_action_t (parse_t_at_most n p) inv disj l false) + (#ha #ar:_) + (v:validate_with_action_t p inv disj l ha ar) + : Tot (validate_with_action_t (parse_t_at_most n p) inv disj l ha false) noextract inline_for_extraction val validate_t_exact @@ -592,9 +611,9 @@ val validate_t_exact (#[@@@erasable] inv:slice_inv) (#[@@@erasable] disj:disjointness_pre) (#[@@@erasable] l:eloc) - (#ar:_) - (v:validate_with_action_t p inv disj l ar) - : Tot (validate_with_action_t (parse_t_exact n p) inv disj l false) + (#ha #ar:_) + (v:validate_with_action_t p inv disj l ha ar) + : Tot (validate_with_action_t (parse_t_exact n p) inv disj l ha false) inline_for_extraction noextract val validate_with_comment @@ -607,9 +626,9 @@ val validate_with_comment (#[@@@erasable] inv:slice_inv) (#[@@@erasable] disj:disjointness_pre) (#[@@@erasable] l:eloc) - (#allow_reading:bool) - (v:validate_with_action_t p inv disj l allow_reading) - : validate_with_action_t p inv disj l allow_reading + (#ha #allow_reading:bool) + (v:validate_with_action_t p inv disj l ha allow_reading) + : validate_with_action_t p inv disj l ha allow_reading inline_for_extraction noextract val validate_weaken_inv_loc @@ -621,12 +640,12 @@ val validate_weaken_inv_loc (#[@@@erasable] inv:slice_inv) (#[@@@erasable] disj:disjointness_pre) (#[@@@erasable] l:eloc) - (#allow_reading:bool) + (#ha #allow_reading:bool) ([@@@erasable] inv':slice_inv{inv' `inv_implies` inv}) ([@@@erasable] disj':disjointness_pre { disj' `imp_disjointness` disj }) ([@@@erasable] l':eloc{l' `eloc_includes` l}) - (v:validate_with_action_t p inv disj l allow_reading) - : Tot (validate_with_action_t p inv' disj' l' allow_reading) + (v:validate_with_action_t p inv disj l ha allow_reading) + : Tot (validate_with_action_t p inv' disj' l' ha allow_reading) inline_for_extraction noextract val read_filter @@ -644,7 +663,11 @@ val read_impos inline_for_extraction let validator #nz #wk (#k:parser_kind nz wk) (#t:Type) (p:parser k t) - = validate_with_action_t p true_inv disjointness_trivial eloc_none true + = validate_with_action_t p true_inv disjointness_trivial eloc_none false true + +inline_for_extraction +let validator_maybe_action #nz #wk (#k:parser_kind nz wk) (#t:Type) (p:parser k t) (has_action:bool) + = validate_with_action_t p true_inv disjointness_trivial eloc_none has_action true inline_for_extraction noextract val validate____UINT8 @@ -727,18 +750,19 @@ val validate_string (#k: parser_kind true WeakKindStrongPrefix) (#t: eqtype) (#[@@@erasable] p: parser k t) - (v: validator p) + (#ha:_) + (v: validator_maybe_action p ha) (r: leaf_reader p) (terminator: t) - : Tot (validate_with_action_t (parse_string p terminator) true_inv disjointness_trivial eloc_none false) + : Tot (validate_with_action_t (parse_string p terminator) true_inv disjointness_trivial eloc_none ha false) inline_for_extraction noextract val validate_all_bytes - : validate_with_action_t parse_all_bytes true_inv disjointness_trivial eloc_none false // could be true + : validate_with_action_t parse_all_bytes true_inv disjointness_trivial eloc_none false false // could be true inline_for_extraction noextract val validate_all_zeros - : validate_with_action_t parse_all_zeros true_inv disjointness_trivial eloc_none false + : validate_with_action_t parse_all_zeros true_inv disjointness_trivial eloc_none false false //////////////////////////////////////////////////////////////////////////////// @@ -880,8 +904,8 @@ val probe_then_validate (#inv:slice_inv) (#disj:disjointness_pre) (#l:eloc) - (#allow_reading:bool) - (v:validate_with_action_t p inv disj l allow_reading) + (#ha #allow_reading:bool) + (v:validate_with_action_t p inv disj l ha allow_reading) (src:U64.t) (len:U64.t) (dest:CP.copy_buffer_t) diff --git a/src/3d/prelude/EverParse3d.Interpreter.fst b/src/3d/prelude/EverParse3d.Interpreter.fst index 9e6dc347..a6d4ae26 100644 --- a/src/3d/prelude/EverParse3d.Interpreter.fst +++ b/src/3d/prelude/EverParse3d.Interpreter.fst @@ -176,6 +176,7 @@ let itype_as_validator (i:itype) A.true_inv A.disjointness_trivial A.eloc_none + false (allow_reader_of_itype i) = match i with | UInt8 -> A.validate____UINT8 @@ -265,7 +266,6 @@ let disjoint (e1 e2:loc_index) | _, Trivial -> disj_none | NonTrivial e1, NonTrivial e2 -> NonTrivial (A.disjoint e1 e2) - (* A context is a list of bindings, where each binding is a pair of a name and a denotation of the name. *) (* global_binding: @@ -279,6 +279,7 @@ type global_binding = { parser_kind_nz:bool; // Does it consume non-zero bytes? parser_weak_kind: P.weak_kind; parser_kind: P.parser_kind parser_kind_nz parser_weak_kind; + parser_has_action: bool; //Memory invariant of any actions it contains inv:inv_index; //Disjointness precondition @@ -297,6 +298,7 @@ type global_binding = { (interp_inv inv) (interp_disj disj) (interp_loc loc) + parser_has_action (Some? p_reader); } @@ -304,6 +306,7 @@ let projector_names : list string = [ `%Mkglobal_binding?.parser_kind_nz; `%Mkglobal_binding?.parser_weak_kind; `%Mkglobal_binding?.parser_kind; + `%Mkglobal_binding?.parser_has_action; `%Mkglobal_binding?.inv; `%Mkglobal_binding?.disj; `%Mkglobal_binding?.loc; @@ -316,6 +319,7 @@ let projector_names : list string = [ let nz_of_binding = Mkglobal_binding?.parser_kind_nz let wk_of_binding = Mkglobal_binding?.parser_weak_kind let pk_of_binding = Mkglobal_binding?.parser_kind +let has_action_of_binding = Mkglobal_binding?.parser_has_action let inv_of_binding = Mkglobal_binding?.inv let disj_of_bindng = Mkglobal_binding?.disj let loc_of_binding = Mkglobal_binding?.loc @@ -363,6 +367,7 @@ noeq type dtyp : #nz:bool -> #wk:P.weak_kind -> P.parser_kind nz wk -> + has_action:bool -> has_reader:bool -> inv_index -> disj_index -> @@ -371,6 +376,7 @@ type dtyp | DT_IType: i:itype -> dtyp (parser_kind_of_itype i) + false (allow_reader_of_itype i) inv_none disj_none loc_none @@ -381,6 +387,7 @@ type dtyp #nz:bool -> #wk:P.weak_kind -> pk:P.parser_kind nz wk -> + ha:bool -> hr:bool -> inv:inv_index -> disj:disj_index -> @@ -389,25 +396,26 @@ type dtyp _:squash (nz == nz_of_binding x /\ wk == wk_of_binding x /\ pk == pk_of_binding x /\ + ha == has_action_of_binding x /\ hr == has_reader x /\ inv == inv_of_binding x /\ disj == disj_of_bindng x /\ loc == loc_of_binding x) -> - dtyp #nz #wk pk hr inv disj loc + dtyp #nz #wk pk ha hr inv disj loc [@@specialize] -let dtyp_as_type #nz #wk (#pk:P.parser_kind nz wk) #hr #i #disj #l - (d:dtyp pk hr i disj l) +let dtyp_as_type #nz #wk (#pk:P.parser_kind nz wk) #ha #hr #i #disj #l + (d:dtyp pk ha hr i disj l) : Type = match d with | DT_IType i -> itype_as_type i - | DT_App _ _ _ _ _ b _ -> + | DT_App _ _ _ _ _ _ b _ -> type_of_binding b -let dtyp_as_eqtype_lemma #nz #wk (#pk:P.parser_kind nz wk) #i #disj #l - (d:dtyp pk true i disj l) +let dtyp_as_eqtype_lemma #nz #wk (#pk:P.parser_kind nz wk) #ha #i #disj #l + (d:dtyp pk ha true i disj l) : Lemma (ensures hasEq (dtyp_as_type d)) [SMTPat (hasEq (dtyp_as_type d))] @@ -415,33 +423,33 @@ let dtyp_as_eqtype_lemma #nz #wk (#pk:P.parser_kind nz wk) #i #disj #l | DT_IType i -> () - | DT_App _ _ _ _ _ b _ -> + | DT_App _ _ _ _ _ _ b _ -> let (| _, _ |) = get_leaf_reader b in () -let dtyp_as_parser #nz #wk (#pk:P.parser_kind nz wk) #hr #i #disj #l - (d:dtyp pk hr i disj l) +let dtyp_as_parser #nz #wk (#pk:P.parser_kind nz wk) #ha #hr #i #disj #l + (d:dtyp pk ha hr i disj l) : P.parser pk (dtyp_as_type d) = match d returns Tot (P.parser pk (dtyp_as_type d)) with | DT_IType i -> itype_as_parser i - | DT_App _ _ _ _ _ b _ -> + | DT_App _ _ _ _ _ _ b _ -> parser_of_binding b [@@specialize] let dtyp_as_validator #nz #wk (#pk:P.parser_kind nz wk) - (#hr:_) + (#ha #hr:_) (#[@@@erasable] i:inv_index) (#[@@@erasable] disj:disj_index) (#[@@@erasable] l:loc_index) - (d:dtyp pk hr i disj l) + (d:dtyp pk ha hr i disj l) : A.validate_with_action_t #nz #wk #pk #(dtyp_as_type d) (dtyp_as_parser d) (interp_inv i) (interp_disj disj) (interp_loc l) - hr + ha hr = match d returns A.validate_with_action_t #nz #wk #pk #(dtyp_as_type d) @@ -449,29 +457,29 @@ let dtyp_as_validator #nz #wk (#pk:P.parser_kind nz wk) (interp_inv i) (interp_disj disj) (interp_loc l) - hr + ha hr with | DT_IType i -> itype_as_validator i - | DT_App _ _ _ _ _ b _ -> + | DT_App _ _ _ _ _ _ b _ -> // assert_norm (dtyp_as_type (DT_App_Alt ps b args) == (type_of_binding_alt (apply_arrow b args))); // assert_norm (dtyp_as_parser (DT_App_Alt ps b args) == parser_of_binding_alt (apply_arrow b args)); validator_of_binding b [@@specialize] -let dtyp_as_leaf_reader #nz (#pk:P.parser_kind nz P.WeakKindStrongPrefix) +let dtyp_as_leaf_reader #nz (#pk:P.parser_kind nz P.WeakKindStrongPrefix) #ha (#[@@@erasable] i:inv_index) (#[@@@erasable] disj:disj_index) (#[@@@erasable] l:loc_index) - (d:dtyp pk true i disj l) + (d:dtyp pk ha true i disj l) : A.leaf_reader (dtyp_as_parser d) = match d with | DT_IType i -> itype_as_leaf_reader i - | DT_App _ _ _ _ _ b _ -> + | DT_App _ _ _ _ _ _ b _ -> let (| _, lr |) = get_leaf_reader b in lr @@ -579,11 +587,12 @@ type atomic_action #nz:bool -> #wk:_ -> #k:P.parser_kind nz wk -> + #ha:bool -> #has_reader:bool -> #inv:inv_index -> #disj:disj_index -> #l:loc_index -> - dt:dtyp k has_reader inv disj l -> + dt:dtyp k ha has_reader inv disj l -> src:U64.t -> len:U64.t -> dest:CP.copy_buffer_t -> @@ -706,76 +715,80 @@ type typ disj_index -> loc_index -> bool -> + bool -> Type = | T_false: fieldname:string -> - typ P.impos_kind inv_none disj_none loc_none true + typ P.impos_kind inv_none disj_none loc_none false true | T_denoted : fieldname:string -> #nz:_ -> #wk:_ -> #pk:P.parser_kind nz wk -> - #has_reader:_ -> #i:_ -> #disj:_ -> #l:_ -> - td:dtyp pk has_reader i disj l -> - typ pk i disj l has_reader + #ha:_ -> #has_reader:_ -> #i:_ -> #disj:_ -> #l:_ -> + td:dtyp pk ha has_reader i disj l -> + typ pk i disj l ha has_reader | T_pair: first_fieldname:string -> #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> - #i1:_ -> #d1:_ -> #l1:_ -> #b1:_ -> + #i1:_ -> #d1:_ -> #l1:_ -> #ha1:_ -> #b1:_ -> #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> - #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> - t1:typ pk1 i1 d1 l1 b1 -> - t2:typ pk2 i2 d2 l2 b2 -> + #i2:_ -> #d2:_ -> #l2:_ -> #ha2:_ -> #b2:_ -> + t1:typ pk1 i1 d1 l1 ha1 b1 -> + t2:typ pk2 i2 d2 l2 ha2 b2 -> typ (P.and_then_kind pk1 pk2) (join_inv i1 i2) (join_disj d1 d2) (join_loc l1 l2) - false + (ha1 || ha2) + false | T_dep_pair: first_fieldname:string -> #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> - #i1:_ -> #d1:_ -> #l1:_ -> + #i1:_ -> #d1:_ -> #l1:_ -> #ha1:_ -> #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> - #i2:_ -> #d2:_ -> #l2:_ -> #b2:bool -> + #i2:_ -> #d2:_ -> #l2:_ -> #ha2:_ -> #b2:bool -> //the first component is a pre-denoted type with a reader - t1:dtyp pk1 true i1 d1 l1 -> + t1:dtyp pk1 ha1 true i1 d1 l1 -> //the second component is a function from denotations of t1 //that's why it's a small type, so that we can speak about its //denotation here - t2:(dtyp_as_type t1 -> typ pk2 i2 d2 l2 b2) -> + t2:(dtyp_as_type t1 -> typ pk2 i2 d2 l2 ha2 b2) -> typ (P.and_then_kind pk1 pk2) (join_inv i1 i2) (join_disj d1 d2) (join_loc l1 l2) + (ha1 || ha2) false | T_refine: fieldname:string -> #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> - #i1:_ -> #d1:_ -> #l1:_ -> + #i1:_ -> #d1:_ -> #l1:_ -> #ha1:_ -> //the first component is a pre-denoted type with a reader - base:dtyp pk1 true i1 d1 l1 -> + base:dtyp pk1 ha1 true i1 d1 l1 -> //the second component is a function from denotations of base //but notice that its codomain is bool, rather than expr //That's to ensure that the refinement is already well-typed refinement:(dtyp_as_type base -> bool) -> - typ (P.filter_kind pk1) i1 d1 l1 false + typ (P.filter_kind pk1) i1 d1 l1 ha1 false | T_refine_with_action: fieldname:string -> #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> - #i1:_ -> #d1:_ -> #l1:_ -> + #i1:_ -> #d1:_ -> #l1:_ -> #ha1:_ -> #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> - base:dtyp pk1 true i1 d1 l1 -> + base:dtyp pk1 ha1 true i1 d1 l1 -> refinement:(dtyp_as_type base -> bool) -> act:(dtyp_as_type base -> action i2 d2 l2 b2 bool) -> typ (P.filter_kind pk1) (join_inv i1 i2) (join_disj d1 d2) (join_loc l1 l2) + true false - + | T_dep_pair_with_refinement: //This construct serves two purposes // 1. To avoid double fetches, we fold the refinement @@ -784,34 +797,36 @@ type typ // to depend on the refinement of the first field first_fieldname:string -> #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> - #i1:_ -> #d1:_ -> #l1:_ -> + #i1:_ -> #d1:_ -> #l1:_ -> #ha1:_ -> #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> - #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> + #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> #ha2:_ -> //the first component is a pre-denoted type with a reader - base:dtyp pk1 true i1 d1 l1 -> + base:dtyp pk1 ha1 true i1 d1 l1 -> //the second component is a function from denotations of base refinement:(dtyp_as_type base -> bool) -> - k:(x:dtyp_as_type base { refinement x } -> typ pk2 i2 d2 l2 b2) -> + k:(x:dtyp_as_type base { refinement x } -> typ pk2 i2 d2 l2 ha2 b2) -> typ (P.and_then_kind (P.filter_kind pk1) pk2) (join_inv i1 i2) (join_disj d1 d2) (join_loc l1 l2) + (ha1 || ha2) false | T_dep_pair_with_action: fieldname:string -> #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> - #i1:_ -> #d1:_ -> #l1:_ -> + #i1:_ -> #d1:_ -> #l1:_ -> #ha1:_ -> #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> - #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> + #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> #ha2:_ -> #i3:_ -> #d3:_ -> #l3:_ -> #b3:_ -> - base:dtyp pk1 true i1 d1 l1 -> - k:(x:dtyp_as_type base -> typ pk2 i2 d2 l2 b2) -> + base:dtyp pk1 ha1 true i1 d1 l1 -> + k:(x:dtyp_as_type base -> typ pk2 i2 d2 l2 ha2 b2) -> act:(dtyp_as_type base -> action i3 d3 l3 b3 bool) -> typ (P.and_then_kind pk1 pk2) (join_inv i1 (join_inv i3 i2)) (join_disj d1 (join_disj d3 d2)) (join_loc l1 (join_loc l3 l2)) + true false | T_dep_pair_with_refinement_and_action: @@ -822,113 +837,118 @@ type typ // to depend on the refinement of the first field first_fieldname:string -> #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> - #i1:_ -> #d1:_ -> #l1:_ -> + #i1:_ -> #d1:_ -> #l1:_ -> #ha1:_ -> #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> - #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> + #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> #ha2:_ -> #i3:_ -> #d3:_ -> #l3:_ -> #b3:_ -> //the first component is a pre-denoted type with a reader - base:dtyp pk1 true i1 d1 l1 -> + base:dtyp pk1 ha1 true i1 d1 l1 -> //the second component is a function from denotations of base refinement:(dtyp_as_type base -> bool) -> - k:(x:dtyp_as_type base { refinement x } -> typ pk2 i2 d2 l2 b2) -> + k:(x:dtyp_as_type base { refinement x } -> typ pk2 i2 d2 l2 ha2 b2) -> act:(dtyp_as_type base -> action i3 d3 l3 b3 bool) -> typ (P.and_then_kind (P.filter_kind pk1) pk2) (join_inv i1 (join_inv i3 i2)) (join_disj d1 (join_disj d3 d2)) (join_loc l1 (join_loc l3 l2)) + true false | T_if_else: #nz1:_ -> #wk1:_ -> #pk1:P.parser_kind nz1 wk1 -> - #l1:_ -> #i1:_ -> #d1:_ -> #b1:_ -> + #l1:_ -> #i1:_ -> #d1:_ -> #b1:_ -> #ha1:_ -> #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> - #l2:_ -> #i2:_ -> #d2:_ -> #b2:_ -> + #l2:_ -> #i2:_ -> #d2:_ -> #b2:_ -> #ha2:_ -> b:bool -> //A bool, rather than an expression - t1:(squash b -> typ pk1 i1 d1 l1 b1) -> - t2:(squash (not b) -> typ pk2 i2 d2 l2 b2) -> + t1:(squash b -> typ pk1 i1 d1 l1 ha1 b1) -> + t2:(squash (not b) -> typ pk2 i2 d2 l2 ha2 b2) -> typ (P.glb pk1 pk2) (join_inv i1 i2) (join_disj d1 d2) - (join_loc l1 l2) false + (join_loc l1 l2) + (ha1 || ha2) + false | T_cases: #nz1:_ -> #wk1:_ -> #pk1:P.parser_kind nz1 wk1 -> - #l1:_ -> #i1:_ -> #d1:_ -> #b1:_ -> + #l1:_ -> #i1:_ -> #d1:_ -> #b1:_ -> #ha1:_ -> #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> - #l2:_ -> #i2:_ -> #d2:_ -> #b2:_ -> + #l2:_ -> #i2:_ -> #d2:_ -> #b2:_ -> #ha2:_ -> b:bool -> //A bool, rather than an expression - t1:typ pk1 i1 d1 l1 b1 -> - t2:typ pk2 i2 d2 l2 b2 -> + t1:typ pk1 i1 d1 l1 ha1 b1 -> + t2:typ pk2 i2 d2 l2 ha2 b2 -> typ (P.glb pk1 pk2) (join_inv i1 i2) (join_disj d1 d2) (join_loc l1 l2) + (ha1 || ha2) false | T_with_action: fieldname:string -> #nz:_ -> #wk:_ -> #pk:P.parser_kind nz wk -> - #l1:_ -> #i1:_ -> #d1:_ -> #b1:_ -> + #l1:_ -> #i1:_ -> #d1:_ -> #b1:_ -> #ha1:_ -> #l2:_ -> #i2:_ -> #d2:_ -> #b2:_ -> - base:typ pk i1 d1 l1 b1 -> + base:typ pk i1 d1 l1 ha1 b1 -> act:action i2 d2 l2 b2 bool -> - typ pk (join_inv i1 i2) (join_disj d1 d2) (join_loc l1 l2) false + typ pk (join_inv i1 i2) (join_disj d1 d2) (join_loc l1 l2) true false | T_with_dep_action: fieldname:string -> #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> - #i1:_ -> #d1: _ -> #l1:_ -> + #i1:_ -> #d1: _ -> #l1:_ -> #ha1:_ -> #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> - head:dtyp pk1 true i1 d1 l1 -> + head:dtyp pk1 ha1 true i1 d1 l1 -> act:(dtyp_as_type head -> action i2 d2 l2 b2 bool) -> - typ pk1 (join_inv i1 i2) (join_disj d1 d2) (join_loc l1 l2) false + typ pk1 (join_inv i1 i2) (join_disj d1 d2) (join_loc l1 l2) true false | T_drop: #nz:_ -> #wk:_ -> #pk:P.parser_kind nz wk -> - #l:_ -> #i:_ -> #d:_ -> #b:_ -> - t:typ pk i d l b -> - typ pk i d l false + #l:_ -> #i:_ -> #d:_ -> #b:_ -> #ha:_ -> + t:typ pk i d l ha b -> + typ pk i d l ha false | T_with_comment: fieldname:string -> #nz:_ -> #wk:_ -> #pk:P.parser_kind nz wk -> - #l:_ -> #i:_ -> #d:_ -> #b:_ -> - t:typ pk i d l b -> + #l:_ -> #i:_ -> #d:_ -> #b:_ -> #ha:_ -> + t:typ pk i d l ha b -> c:comments -> - typ pk i d l b + typ pk i d l ha b | T_nlist: fieldname:string -> #wk:_ -> #pk:P.parser_kind true wk -> - #i:_ -> #l:_ -> #d:_ -> #b:_ -> + #i:_ -> #l:_ -> #d:_ -> #b:_ -> #ha:_ -> n_is_constant:bool -> payload_is_constant_size:bool -> n:U32.t -> - t:typ pk i d l b -> - typ P.kind_nlist i d l false + t:typ pk i d l ha b -> + typ P.kind_nlist i d l ha false | T_at_most: fieldname:string -> #nz:_ -> #wk:_ -> #pk:P.parser_kind nz wk -> - #i:_ -> #d:_ -> #l:_ -> #b:_ -> + #i:_ -> #d:_ -> #l:_ -> #b:_ -> #ha:_ -> n:U32.t -> - t:typ pk i d l b -> - typ P.kind_t_at_most i d l false + t:typ pk i d l ha b -> + typ P.kind_t_at_most i d l ha false | T_exact: fieldname:string -> #nz:_ -> #wk:_ -> #pk:P.parser_kind nz wk -> - #i:_ -> #d:_ -> #l:_ -> #b:_ -> + #i:_ -> #d:_ -> #l:_ -> #b:_ -> #ha:_ -> n:U32.t -> - t:typ pk i d l b -> - typ P.kind_t_exact i d l false + t:typ pk i d l ha b -> + typ P.kind_t_exact i d l ha false | T_string: fieldname:string -> #pk1:P.parser_kind true P.WeakKindStrongPrefix -> - element_type:dtyp pk1 true inv_none disj_none loc_none -> + #ha:_ -> + element_type:dtyp pk1 ha true inv_none disj_none loc_none -> terminator:dtyp_as_type element_type -> - typ P.parse_string_kind inv_none disj_none loc_none false + typ P.parse_string_kind inv_none disj_none loc_none ha false [@@specialize] @@ -947,13 +967,14 @@ let t_probe_then_validate (len:U64.t) (dest:CP.copy_buffer_t) (#nz #wk:_) (#pk:P.parser_kind nz wk) - (#has_reader #i #disj:_) + (#ha #has_reader #i #disj:_) (#l:_) - (td:dtyp pk has_reader i disj l) + (td:dtyp pk ha has_reader i disj l) : typ (parser_kind_of_itype UInt64) (join_inv i (NonTrivial (A.copy_buffer_inv dest))) (join_disj disj (disjoint (NonTrivial (A.copy_buffer_loc dest)) l)) (join_loc l (NonTrivial (A.copy_buffer_loc dest))) + true false = T_with_dep_action fieldname (DT_IType UInt64) @@ -964,8 +985,8 @@ let t_probe_then_validate (* Type denotation of `typ` *) let rec as_type #nz #wk (#pk:P.parser_kind nz wk) - #l #i #d #b - (t:typ pk l i d b) + #l #i #d #ha #b + (t:typ pk l i d ha b) : Tot Type0 (decreases t) = match t with @@ -1024,8 +1045,8 @@ let rec as_type (* Parser denotation of `typ` *) let rec as_parser #nz #wk (#pk:P.parser_kind nz wk) - #l #i #d #b - (t:typ pk l i d b) + #l #i #d #ha #b + (t:typ pk l i d ha b) : Tot (P.parser pk (as_type t)) (decreases t) = match t returns Tot (P.parser pk (as_type t)) with @@ -1110,11 +1131,11 @@ let rec as_parser P.parse_string (dtyp_as_parser elt_t) terminator [@@specialize] -let rec as_reader #nz (#pk:P.parser_kind nz P.WeakKindStrongPrefix) +let rec as_reader #nz (#pk:P.parser_kind nz P.WeakKindStrongPrefix) #ha (#[@@@erasable] inv:inv_index) (#[@@@erasable] d:disj_index) (#[@@@erasable] loc:loc_index) - (t:typ pk inv d loc true) + (t:typ pk inv d loc ha true) : leaf_reader (as_parser t) = match t with | T_denoted _n dt -> @@ -1143,14 +1164,14 @@ let rec as_validator (#[@@@erasable] inv:inv_index) (#[@@@erasable] disj:disj_index) (#[@@@erasable] loc:loc_index) - #b - (t:typ pk inv disj loc b) + #ha #b + (t:typ pk inv disj loc ha b) : Tot (A.validate_with_action_t #nz #wk #pk #(as_type t) (as_parser t) (interp_inv inv) (interp_disj disj) (interp_loc loc) - b) + ha b) (decreases t) = A.index_equations(); match t @@ -1160,7 +1181,7 @@ let rec as_validator (interp_inv inv) (interp_disj disj) (interp_loc loc) - b + ha b ) with | T_false fn -> @@ -1306,8 +1327,15 @@ let rec as_validator | T_nlist fn n_is_const payload_is_constant_size n t -> assert_norm (as_type (T_nlist fn n_is_const payload_is_constant_size n t) == P.nlist n (as_type t)); assert_norm (as_parser (T_nlist fn n_is_const payload_is_constant_size n t) == P.parse_nlist n (as_parser t)); - A.validate_with_error_handler typename fn - (A.validate_nlist_constant_size_without_actions n_is_const payload_is_constant_size n (as_validator typename t)) + if ha + then ( + A.validate_with_error_handler typename fn + (A.validate_nlist n (as_validator typename t)) + ) + else ( + A.validate_with_error_handler typename fn + (A.validate_nlist_constant_size_without_actions n_is_const payload_is_constant_size n (as_validator typename t)) + ) | T_at_most fn n t -> assert_norm (as_type (T_at_most fn n t) == P.t_at_most n (as_type t)); @@ -1331,16 +1359,17 @@ let rec as_validator #pop-options [@@noextract_to "krml"; specialize] inline_for_extraction noextract -let validator_of #allow_reading #nz #wk (#k:P.parser_kind nz wk) +let validator_of #ha #allow_reading #nz #wk (#k:P.parser_kind nz wk) (#[@@@erasable] i:inv_index) (#[@@@erasable] d:disj_index) (#[@@@erasable] l:loc_index) - (t:typ k i d l allow_reading) = + (t:typ k i d l ha allow_reading) = A.validate_with_action_t (as_parser t) (interp_inv i) (interp_disj d) (interp_loc l) + ha allow_reading [@@noextract_to "krml"; specialize] @@ -1349,8 +1378,8 @@ let dtyp_of #nz #wk (#k:P.parser_kind nz wk) (#[@@@erasable] i:inv_index) (#[@@@erasable] d:disj_index) (#[@@@erasable] l:loc_index) - #b (t:typ k i d l b) = - dtyp k b i d l + #ha #b (t:typ k i d l ha b) = + dtyp k ha b i d l let specialization_steps = [nbe; @@ -1364,6 +1393,7 @@ let specialization_steps = `%nz_of_binding; `%wk_of_binding; `%pk_of_binding; + `%has_action_of_binding; `%inv_of_binding; `%loc_of_binding; `%type_of_binding; @@ -1390,17 +1420,18 @@ let mk_global_binding #nz #wk ([@@@erasable] p_t : Type0) ([@@@erasable] p_p : P.parser pk p_t) (p_reader: option (leaf_reader p_p)) - (b:bool) + (#ha b:bool) (p_v : A.validate_with_action_t p_p (interp_inv inv) (interp_disj disj) - (interp_loc loc) b) + (interp_loc loc) ha b) ([@@@erasable] pf:squash (b == Some? p_reader)) : global_binding = { parser_kind_nz = nz; parser_weak_kind = wk; parser_kind = pk; + parser_has_action = ha; inv = inv; disj; loc = loc; @@ -1411,7 +1442,7 @@ let mk_global_binding #nz #wk } [@@specialize] -let mk_dt_app #nz #wk (pk:P.parser_kind nz wk) (b:bool) +let mk_dt_app #nz #wk (pk:P.parser_kind nz wk) (ha b:bool) ([@@@erasable] inv:inv_index) ([@@@erasable] disj:disj_index) ([@@@erasable] loc:loc_index) @@ -1419,12 +1450,13 @@ let mk_dt_app #nz #wk (pk:P.parser_kind nz wk) (b:bool) ([@@@erasable] pf:squash (nz == nz_of_binding x /\ wk == wk_of_binding x /\ pk == pk_of_binding x /\ + ha == has_action_of_binding x /\ b == has_reader x /\ inv == inv_of_binding x /\ disj == disj_of_bindng x /\ loc == loc_of_binding x)) - : dtyp #nz #wk pk b inv disj loc - = DT_App pk b inv disj loc x pf + : dtyp #nz #wk pk ha b inv disj loc + = DT_App pk ha b inv disj loc x pf [@@specialize] @@ -1436,18 +1468,20 @@ let mk_dtyp_app #nz #wk ([@@@erasable] p_t : Type0) ([@@@erasable] p_p : P.parser pk p_t) (p_reader: option (leaf_reader p_p)) - (b:bool) + (ha b:bool) (p_v : A.validate_with_action_t p_p (interp_inv inv) (interp_disj disj) (interp_loc loc) + ha b) ([@@@erasable] pf:squash (b == Some? p_reader)) - : dtyp #nz #wk pk b inv disj loc + : dtyp #nz #wk pk ha b inv disj loc = let gb = { parser_kind_nz = nz; parser_weak_kind = wk; parser_kind = pk; + parser_has_action = ha; inv = inv; disj; loc = loc; @@ -1456,7 +1490,7 @@ let mk_dtyp_app #nz #wk p_reader = p_reader; p_v = p_v } in - DT_App pk b inv disj loc gb () + DT_App pk ha b inv disj loc gb () //attribute to tag disjointness indexes of type definitions let specialize_disjointness = ()