From b248562dbf3200d44b3175c087d0b35960dc8d5a Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 18 Jan 2024 17:16:51 -0800 Subject: [PATCH 1/2] Add high-level serializer for 3D types --- src/3d/InterpreterTarget.fst | 4 + src/3d/prelude/EverParse3d.Actions.Base.fst | 67 +++-- src/3d/prelude/EverParse3d.Actions.Base.fsti | 24 +- src/3d/prelude/EverParse3d.Interpreter.fst | 248 +++++++++---------- src/3d/prelude/EverParse3d.Prelude.fst | 100 ++++++-- src/3d/prelude/EverParse3d.Prelude.fsti | 98 +++++++- 6 files changed, 337 insertions(+), 204 deletions(-) diff --git a/src/3d/InterpreterTarget.fst b/src/3d/InterpreterTarget.fst index dd7e746e6..a43cafcf5 100644 --- a/src/3d/InterpreterTarget.fst +++ b/src/3d/InterpreterTarget.fst @@ -1020,6 +1020,7 @@ let print_binding mname (td:type_decl) %s\n\ (type_%s %s)\n\ (coerce (_ by (T.norm [delta_only [`%%type_%s]]; T.trefl())) (parser_%s %s))\n\ + (coerce (_ by (T.norm [delta_only [`%%type_%s]]; T.trefl())) (serializer_%s %s))\n\ %s\n\ %b\n\ (coerce (_ by %s) (validate_%s %s))\n\ @@ -1032,6 +1033,8 @@ let print_binding mname (td:type_decl) root_name args root_name root_name args + root_name + root_name args reader td.allow_reading coerce_validator root_name args @@ -1051,6 +1054,7 @@ let print_binding mname (td:type_decl) def'; (as_type_or_parser "type"); (as_type_or_parser "parser"); + (as_type_or_parser "serializer"); validate_binding; dtyp; enum_typ_of_binding] diff --git a/src/3d/prelude/EverParse3d.Actions.Base.fst b/src/3d/prelude/EverParse3d.Actions.Base.fst index 1965eaecc..051d18f56 100644 --- a/src/3d/prelude/EverParse3d.Actions.Base.fst +++ b/src/3d/prelude/EverParse3d.Actions.Base.fst @@ -1132,13 +1132,13 @@ noextract inline_for_extraction let validate_nlist (n:U32.t) - #wk - (#k:parser_kind true wk) + (#k:parser_kind true WeakKindStrongPrefix) #t (#p:parser k t) + (s:serializer p) #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) +: Tot (validate_with_action_t (parse_nlist n s) inv disj l 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)) @@ -1189,14 +1189,14 @@ let validate_total_constant_size_no_read inline_for_extraction noextract let validate_nlist_total_constant_size_mod_ok (n:U32.t) - #wk - (#k:parser_kind true wk) + (#k:parser_kind true WeakKindStrongPrefix) (#t: Type) (p:parser k t) + (s:serializer p) inv disj l - : Pure (validate_with_action_t (parse_nlist n p) inv disj l true) + : Pure (validate_with_action_t (parse_nlist n s) inv disj l true) (requires ( let open LP in k.parser_kind_subkind == Some ParserStrong /\ @@ -1208,22 +1208,22 @@ let validate_nlist_total_constant_size_mod_ok (ensures (fun _ -> True)) = [@inline_let] let _ = - parse_nlist_total_fixed_size_kind_correct n p + parse_nlist_total_fixed_size_kind_correct n p s in validate_total_constant_size_no_read' - (LP.strengthen (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n p)) + (LP.strengthen (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n s)) (Cast.uint32_to_uint64 n) () inv disj l inline_for_extraction noextract let validate_nlist_constant_size_mod_ko (n:U32.t) - (#wk: _) - (#k:parser_kind true wk) + (#k:parser_kind true WeakKindStrongPrefix) #t (p:parser k t) + (s:serializer p) inv disj l - : Pure (validate_with_action_t (parse_nlist n p) inv disj l true) + : Pure (validate_with_action_t (parse_nlist n s) inv disj l true) (requires ( let open LP in k.parser_kind_subkind == Some ParserStrong /\ @@ -1237,12 +1237,12 @@ let validate_nlist_constant_size_mod_ko let h = FStar.HyperStack.ST.get () in [@inline_let] let f () : Lemma - (requires (Some? (LP.parse (parse_nlist n p) (I.get_remaining input h)))) + (requires (Some? (LP.parse (parse_nlist n s) (I.get_remaining input h)))) (ensures False) = let sq = I.get_remaining input h in let sq' = Seq.slice sq 0 (U32.v n) in LowParse.Spec.List.list_length_constant_size_parser_correct p sq' ; - let Some (l, _) = LP.parse (parse_nlist n p) sq in + let Some (l, _) = LP.parse (parse_nlist n s) sq in assert (U32.v n == FStar.List.Tot.length l `Prims.op_Multiply` k.LP.parser_kind_low) ; FStar.Math.Lemmas.cancel_mul_mod (FStar.List.Tot.length l) k.LP.parser_kind_low ; assert (U32.v n % k.LP.parser_kind_low == 0) @@ -1255,12 +1255,12 @@ let validate_nlist_constant_size_mod_ko inline_for_extraction noextract let validate_nlist_total_constant_size' (n:U32.t) - #wk - (#k:parser_kind true wk) + (#k:parser_kind true WeakKindStrongPrefix) #t (p:parser k t) + (s:serializer p) inv disj l - : Pure (validate_with_action_t (parse_nlist n p) inv disj l true) + : Pure (validate_with_action_t (parse_nlist n s) inv disj l true) (requires ( let open LP in k.parser_kind_subkind == Some ParserStrong /\ @@ -1271,19 +1271,19 @@ let validate_nlist_total_constant_size' (ensures (fun _ -> True)) = fun ctxt error_handler_fn input start_position -> // n is not an integer constant, so we need to eta-expand and swap fun and if if n `U32.rem` U32.uint_to_t k.LP.parser_kind_low = 0ul - then validate_nlist_total_constant_size_mod_ok n p inv disj l ctxt error_handler_fn input start_position - else validate_nlist_constant_size_mod_ko n p inv disj l ctxt error_handler_fn input start_position + then validate_nlist_total_constant_size_mod_ok n p s inv disj l ctxt error_handler_fn input start_position + else validate_nlist_constant_size_mod_ko n p s inv disj l ctxt error_handler_fn input start_position inline_for_extraction noextract let validate_nlist_total_constant_size (n_is_const: bool) (n:U32.t) - #wk - (#k:parser_kind true wk) + (#k:parser_kind true WeakKindStrongPrefix) (#t: Type) (p:parser k t) + (s:serializer p) inv disj l -: Pure (validate_with_action_t (parse_nlist n p) inv disj l true) +: Pure (validate_with_action_t (parse_nlist n s) inv disj l true) (requires ( let open LP in k.parser_kind_subkind = Some ParserStrong /\ @@ -1300,26 +1300,25 @@ let validate_nlist_total_constant_size then U32.v n % k.LP.parser_kind_low = 0 else false then - validate_nlist_total_constant_size_mod_ok n p inv disj l + validate_nlist_total_constant_size_mod_ok n p s inv disj l else if if n_is_const then U32.v n % k.LP.parser_kind_low <> 0 else false then - validate_nlist_constant_size_mod_ko n p inv disj l + validate_nlist_constant_size_mod_ko n p s inv disj l else - validate_nlist_total_constant_size' n p inv disj l + validate_nlist_total_constant_size' n p s inv disj l noextract inline_for_extraction let validate_nlist_constant_size_without_actions (n_is_const: bool) (n:U32.t) - #wk - (#k:parser_kind true wk) - #t (#p:parser k t) #inv #disj #l #ar + (#k:parser_kind true WeakKindStrongPrefix) + #t (#p:parser k t) (s:serializer p) #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) +: Tot (validate_with_action_t (parse_nlist n s) inv disj l false) = if let open LP in @@ -1328,18 +1327,18 @@ let validate_nlist_constant_size_without_actions k.parser_kind_metadata = Some ParserKindMetadataTotal && k.parser_kind_low < 4294967296 then - validate_drop (validate_nlist_total_constant_size n_is_const n p inv disj l) + validate_drop (validate_nlist_total_constant_size n_is_const n p s inv disj l) else - validate_nlist n v + validate_nlist n s v #push-options "--z3rlimit_factor 16 --z3cliopt smt.arith.nl=false" #restart-solver noextract inline_for_extraction let validate_t_at_most - (n:U32.t) #nz #wk (#k:parser_kind nz wk) (#t:_) (#p:parser k t) + (n:U32.t) #nz (#k:parser_kind nz WeakKindStrongPrefix) (#t:_) (#p:parser k t) s #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) + : Tot (validate_with_action_t (parse_t_at_most n s) inv disj l false) = fun ctxt error_handler_fn input input_length start_position -> [@inline_let] let pos = start_position in let h = HST.get () in @@ -1377,10 +1376,10 @@ 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) + (n:U32.t) #nz (#k:parser_kind nz WeakKindStrongPrefix) (#t:_) (#p:parser k t) s #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 +: validate_with_action_t (parse_t_exact n s) inv disj l false = fun ctxt error_handler_fn input input_length start_position -> [@inline_let] let pos = start_position in let h = HST.get () in diff --git a/src/3d/prelude/EverParse3d.Actions.Base.fsti b/src/3d/prelude/EverParse3d.Actions.Base.fsti index 4c343e332..e4f18e197 100644 --- a/src/3d/prelude/EverParse3d.Actions.Base.fsti +++ b/src/3d/prelude/EverParse3d.Actions.Base.fsti @@ -526,61 +526,61 @@ val validate_ite noextract inline_for_extraction val validate_nlist (n:U32.t) - (#wk: _) - (#k:parser_kind true wk) + (#k:parser_kind true WeakKindStrongPrefix) (#[@@@erasable] t:Type) (#[@@@erasable] p:parser k t) + ((*[@@@erasable]*) s:serializer p) (#[@@@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 +: validate_with_action_t (parse_nlist n s) inv disj l false noextract inline_for_extraction val validate_nlist_constant_size_without_actions (n_is_const: bool) (n:U32.t) - (#wk: _) - (#k:parser_kind true wk) + (#k:parser_kind true WeakKindStrongPrefix) (#[@@@erasable] t:Type) (#[@@@erasable] p:parser k t) + ((*[@@@erasable]*) s:serializer p) (#[@@@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 (parse_nlist n p) inv disj l false) +: Tot (validate_with_action_t (parse_nlist n s) inv disj l false) noextract inline_for_extraction val validate_t_at_most (n:U32.t) (#nz: _) - (#wk: _) - (#k:parser_kind nz wk) + (#k:parser_kind nz WeakKindStrongPrefix) (#[@@@erasable] t:Type) (#[@@@erasable] p:parser k t) + ((*[@@@erasable]*) s:serializer p) (#[@@@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) + : Tot (validate_with_action_t (parse_t_at_most n s) inv disj l false) noextract inline_for_extraction val validate_t_exact (n:U32.t) (#nz:bool) - (#wk: _) - (#k:parser_kind nz wk) + (#k:parser_kind nz WeakKindStrongPrefix) (#[@@@erasable] t:Type) (#[@@@erasable] p:parser k t) + ((*[@@@erasable]*) s:serializer p) (#[@@@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) + : Tot (validate_with_action_t (parse_t_exact n s) inv disj l false) inline_for_extraction noextract val validate_with_comment diff --git a/src/3d/prelude/EverParse3d.Interpreter.fst b/src/3d/prelude/EverParse3d.Interpreter.fst index bcd38ccd5..aa1daa0c8 100644 --- a/src/3d/prelude/EverParse3d.Interpreter.fst +++ b/src/3d/prelude/EverParse3d.Interpreter.fst @@ -144,6 +144,22 @@ let itype_as_parser (i:itype) | AllBytes -> P.parse_all_bytes | AllZeros -> P.parse_all_zeros +(* Interpretation of an itype as a serializer *) +let itype_as_serializer (i:itype) + : P.serializer (itype_as_parser i) + = match i with + | UInt8 -> P.serialize____UINT8 + | UInt16 -> P.serialize____UINT16 + | UInt32 -> P.serialize____UINT32 + | UInt64 -> P.serialize____UINT64 + | UInt8BE -> P.serialize____UINT8BE + | UInt16BE -> P.serialize____UINT16BE + | UInt32BE -> P.serialize____UINT32BE + | UInt64BE -> P.serialize____UINT64BE + | Unit -> P.serialize_unit + | AllBytes -> P.serialize_all_bytes + | AllZeros -> P.serialize_all_zeros + [@@specialize] let allow_reader_of_itype (i:itype) : bool @@ -289,6 +305,8 @@ type global_binding = { p_t : Type0; //Its parser denotation p_p : P.parser parser_kind p_t; + //Its serializer denotation + p_s : P.serializer p_p; //Whether the type can be read -- to avoid double fetches p_reader: option (leaf_reader p_p); //Its validate-with-action denotationa @@ -309,6 +327,7 @@ let projector_names : list string = [ `%Mkglobal_binding?.loc; `%Mkglobal_binding?.p_t; `%Mkglobal_binding?.p_p; + `%Mkglobal_binding?.p_s; `%Mkglobal_binding?.p_reader; `%Mkglobal_binding?.p_v; ] @@ -321,6 +340,7 @@ let disj_of_bindng = Mkglobal_binding?.disj let loc_of_binding = Mkglobal_binding?.loc let type_of_binding = Mkglobal_binding?.p_t let parser_of_binding = Mkglobal_binding?.p_p +let serializer_of_binding = Mkglobal_binding?.p_s let leaf_reader_of_binding = Mkglobal_binding?.p_reader let validator_of_binding = Mkglobal_binding?.p_v @@ -428,6 +448,16 @@ let dtyp_as_parser #nz #wk (#pk:P.parser_kind nz wk) #hr #i #disj #l | DT_App _ _ _ _ _ b _ -> parser_of_binding b + +let dtyp_as_serializer #nz #wk (#pk:P.parser_kind nz wk) #hr #i #disj #l + (d:dtyp pk hr i disj l) + : P.serializer (dtyp_as_parser d) + = match d returns Tot (P.serializer (dtyp_as_parser d)) with + | DT_IType i -> + itype_as_serializer i + + | DT_App _ _ _ _ _ b _ -> + serializer_of_binding b [@@specialize] let dtyp_as_validator #nz #wk (#pk:P.parser_kind nz wk) @@ -891,7 +921,7 @@ type typ | T_nlist: fieldname:string -> - #wk:_ -> #pk:P.parser_kind true wk -> + #pk:P.parser_kind true P.WeakKindStrongPrefix -> #i:_ -> #l:_ -> #d:_ -> #b:_ -> n:U32.t -> t:typ pk i d l b -> @@ -899,7 +929,7 @@ type typ | T_at_most: fieldname:string -> - #nz:_ -> #wk:_ -> #pk:P.parser_kind nz wk -> + #nz:_ -> #pk:P.parser_kind nz P.WeakKindStrongPrefix -> #i:_ -> #d:_ -> #l:_ -> #b:_ -> n:U32.t -> t:typ pk i d l b -> @@ -907,7 +937,7 @@ type typ | T_exact: fieldname:string -> - #nz:_ -> #wk:_ -> #pk:P.parser_kind nz wk -> + #nz:_ -> #pk:P.parser_kind nz P.WeakKindStrongPrefix -> #i:_ -> #d:_ -> #l:_ -> #b:_ -> n:U32.t -> t:typ pk i d l b -> @@ -950,149 +980,115 @@ let t_probe_then_validate (fun src -> Atomic_action (Action_probe_then_validate td src len dest probe)) - -(* 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) - : Tot Type0 - (decreases t) - = match t with - | T_false _ -> False - - | T_denoted _ td -> - dtyp_as_type td - - | T_pair _ t1 t2 -> - as_type t1 & as_type t2 - - | T_dep_pair _ i t - | T_dep_pair_with_action _ i t _ -> - x:dtyp_as_type i & as_type (t x) - - | T_refine _ base refinement -> - P.refine (dtyp_as_type base) refinement - - | T_refine_with_action _ base refinement _ -> - P.refine (dtyp_as_type base) refinement - - | T_dep_pair_with_refinement _ base refinement t -> - x:P.refine (dtyp_as_type base) refinement & as_type (t x) - - | T_dep_pair_with_refinement_and_action _ base refinement t _ -> - x:P.refine (dtyp_as_type base) refinement & as_type (t x) - - | T_if_else b t0 t1 -> - P.t_ite b (fun _ -> as_type (t0())) - (fun _ -> as_type (t1())) - - | T_cases b t0 t1 -> - P.t_ite b (fun _ -> as_type t0) (fun _ -> as_type t1) - - | T_with_action _ t _ - | T_with_comment _ t _ -> - as_type t - - | T_with_dep_action _ i _ -> - dtyp_as_type i - - | T_nlist _ n t -> - P.nlist n (as_type t) - - | T_at_most _ n t -> - P.t_at_most n (as_type t) - - | T_exact _ n t -> - P.t_exact n (as_type t) - - | T_string _ elt_t terminator -> - P.cstring (dtyp_as_type elt_t) terminator - - -(* Parser denotation of `typ` *) -let rec as_parser +(* Type, parser and serializer denotation of `typ` *) +let rec denote #nz #wk (#pk:P.parser_kind nz wk) #l #i #d #b (t:typ pk l i d b) - : Tot (P.parser pk (as_type t)) + : Tot (t:Type0 & p:P.parser pk t & P.serializer p) (decreases t) - = match t returns Tot (P.parser pk (as_type t)) with + = match t returns Tot (t:Type0 & p:P.parser pk t & P.serializer p) with | T_false _ -> //assert_norm (as_type g T_false == False); - P.parse_impos() + (| False, P.parse_impos(), P.serialize_impos() |) | T_denoted _ d -> - dtyp_as_parser d + (| dtyp_as_type d, dtyp_as_parser d, dtyp_as_serializer d |) | T_pair _ t1 t2 -> //assert_norm (as_type g (T_pair t1 t2) == as_type g t1 * as_type g t2); - let p1 = as_parser t1 in - let p2 = as_parser t2 in - P.parse_pair p1 p2 + (| (denote t1)._1 & (denote t2)._1, + P.parse_pair (denote t1)._2 (denote t2)._2, + P.serialize_pair _ _ (denote t1)._3 (denote t2)._3 |) | T_dep_pair _ i t | T_dep_pair_with_action _ i t _ -> //assert_norm (as_type g (T_dep_pair i t) == x:itype_as_type i & as_type g (t x)); let pi = dtyp_as_parser i in - P.parse_dep_pair pi (fun (x:dtyp_as_type i) -> as_parser (t x)) + (| x:dtyp_as_type i & (denote (t x))._1, + P.parse_dep_pair pi (fun (x:dtyp_as_type i) -> (denote (t x))._2), + P.serialize_dep_pair _ _ (dtyp_as_serializer i) (fun x -> (denote (t x))._3) |) | T_refine _ base refinement | T_refine_with_action _ base refinement _ -> //assert_norm (as_type g (T_refine base refinement) == P.refine (itype_as_type base) refinement); - let pi = dtyp_as_parser base in - P.parse_filter pi refinement + (| P.refine (dtyp_as_type base) refinement, + P.parse_filter (dtyp_as_parser base) refinement, + P.serialize_filter _ _ (dtyp_as_serializer base) |) | T_dep_pair_with_refinement _ base refinement k -> - P.((dtyp_as_parser base `parse_filter` refinement) `parse_dep_pair` (fun x -> as_parser (k x))) - + (| x:P.refine (dtyp_as_type base) refinement & (denote (k x))._1, + P.((dtyp_as_parser base `parse_filter` refinement) `parse_dep_pair` (fun x -> (denote (k x))._2)), + P.serialize_dep_pair _ _ (P.serialize_filter _ _ (dtyp_as_serializer base)) (fun x -> (denote (k x))._3) |) | T_dep_pair_with_refinement_and_action _ base refinement k _ -> - P.((dtyp_as_parser base `parse_filter` refinement) `parse_dep_pair` (fun x -> as_parser (k x))) - - | T_if_else b t0 t1 -> - //assert_norm (as_type g (T_if_else b t0 t1) == P.t_ite b (as_type g t0) (as_type g t1)); - let p0 (_:squash b) = - P.parse_weaken_right (as_parser (t0())) _ - in - let p1 (_:squash (not b)) = - P.parse_weaken_left (as_parser (t1())) _ - in - P.parse_ite b p0 p1 + (| x:P.refine (dtyp_as_type base) refinement & (denote (k x))._1, + P.((dtyp_as_parser base `parse_filter` refinement) `parse_dep_pair` (fun x -> (denote (k x))._2)), + P.serialize_dep_pair _ _ (P.serialize_filter _ _ (dtyp_as_serializer base)) (fun x -> (denote (k x))._3) |) + + | T_if_else #nz1 #wk1 #pk1 #l1 #i1 #d1 #b1 #nz2 #wk2 #pk2 b t0 t1 -> + let p0 (_:squash b) = P.parse_weaken_right (denote (t0 ()))._2 pk2 in + let p1 (_:squash (not b)) = P.parse_weaken_left (denote (t1 ()))._2 pk1 in + let s0 (_:squash b) : P.serializer (p0 ()) = P.serialize_weaken_right (denote (t0 ()))._2 pk2 (denote (t0 ()))._3 in + let s1 (_:squash (not b)) : P.serializer (p1 ()) = P.serialize_weaken_left (denote (t1 ()))._2 pk1 (denote (t1 ()))._3 in + (| (if b then (denote (t0 ()))._1 else (denote (t1 ()))._1), + P.parse_ite b p0 p1, P.serialize_ite b p0 p1 s0 s1 |) | T_cases b t0 t1 -> //assert_norm (as_type g (T_if_else b t0 t1) == P.t_ite b (as_type g t0) (as_type g t1)); - let p0 (_:squash b) = - P.parse_weaken_right (as_parser t0) _ - in - let p1 (_:squash (not b)) = - P.parse_weaken_left (as_parser t1) _ - in - P.parse_ite b p0 p1 + let p0 (_:squash b) = P.parse_weaken_right (denote t0)._2 _ in + let p1 (_:squash (not b)) = P.parse_weaken_left (denote t1)._2 _ in + let s0 (_:squash b) : P.serializer (p0 ()) = P.serialize_weaken_right _ _ (denote t0)._3 in + let s1 (_:squash (not b)) : P.serializer (p1 ()) = P.serialize_weaken_left _ _ (denote t1)._3 in + (| (if b then (denote t0)._1 else (denote t1)._1), P.parse_ite b p0 p1, P.serialize_ite b p0 p1 s0 s1 |) | T_with_action _ t a -> //assert_norm (as_type g (T_with_action t a) == as_type g t); - as_parser t + denote t | T_with_dep_action _ i a -> //assert_norm (as_type g (T_with_dep_action i a) == itype_as_type i); - dtyp_as_parser i + (| dtyp_as_type i, dtyp_as_parser i, dtyp_as_serializer i |) | T_with_comment _ t c -> //assert_norm (as_type g (T_with_comment t c) == as_type g t); - as_parser t + denote t | T_nlist _ n t -> - P.parse_nlist n (as_parser t) + (| P.nlist n (denote t)._1 (denote t)._3, P.parse_nlist n (denote t)._3, P.serialize_nlist n (denote t)._3 |) | T_at_most _ n t -> - P.parse_t_at_most n (as_parser t) + (| P.t_at_most n _ (denote t)._3, P.parse_t_at_most n (denote t)._3, P.serialize_t_at_most n (denote t)._3 |) | T_exact _ n t -> - P.parse_t_exact n (as_parser t) + (| P.t_exact n _ (denote t)._3, P.parse_t_exact n (denote t)._3, P.serialize_t_exact n (denote t)._3 |) | T_string _ elt_t terminator -> - P.parse_string (dtyp_as_parser elt_t) terminator + (| P.cstring (dtyp_as_type elt_t) terminator, P.parse_string (dtyp_as_parser elt_t) terminator, P.serialize_string (dtyp_as_serializer elt_t) terminator |) + +(* Type denotation of `typ` *) +let as_type + #nz #wk (#pk:P.parser_kind nz wk) + #l #i #d #b + (t:typ pk l i d b) + : Tot Type0 = + (denote t)._1 + +(* Parser denotation of `typ` *) +let as_parser + #nz #wk (#pk:P.parser_kind nz wk) + #l #i #d #b + (t:typ pk l i d b) + : P.parser pk (as_type t) = + (denote t)._2 + +(* Serializer denotation of `typ` *) +let as_serializer + #nz #wk (#pk:P.parser_kind nz wk) + #l #i #d #b + (t:typ pk l i d b) + : Tot (P.serializer (as_parser t)) = + (denote t)._3 [@@specialize] let rec as_reader #nz (#pk:P.parser_kind nz P.WeakKindStrongPrefix) @@ -1234,31 +1230,31 @@ let rec as_validator (fun x -> as_validator typename (k x))) - | T_if_else b t0 t1 -> - assert_norm (as_type (T_if_else b t0 t1) == P.t_ite b (fun _ -> as_type (t0())) (fun _ -> as_type (t1 ()))); - let p0 (_:squash b) = P.parse_weaken_right (as_parser (t0())) _ in - let p1 (_:squash (not b)) = P.parse_weaken_left (as_parser (t1())) _ in + | T_if_else #nz1 #wk1 #pk1 #l1 #i1 #d1 #b1 #nz2 #wk2 #pk2 #l2 #i2 #d2 #b2 b t0 t1 -> + assert_norm (as_type (T_if_else b t0 t1) == (if b then as_type (t0()) else as_type (t1 ()))); + let p0 (_:squash b) = P.parse_weaken_right (as_parser (t0())) pk2 in + let p1 (_:squash (not b)) = P.parse_weaken_left (as_parser (t1())) pk1 in assert_norm (as_parser (T_if_else b t0 t1) == P.parse_ite b p0 p1); let v0 (_:squash b) = - A.validate_weaken_right (as_validator typename (t0())) _ + A.validate_weaken_right (as_validator typename (t0())) pk2 in let v1 (_:squash (not b)) = - A.validate_weaken_left (as_validator typename (t1())) _ + A.validate_weaken_left (as_validator typename (t1())) pk1 in - A.validate_ite b p0 v0 p1 v1 + coerce () (A.validate_ite b p0 v0 p1 v1) - | T_cases b t0 t1 -> + | T_cases #nz1 #wk1 #pk1 #l1 #i1 #d1 #b1 #nz2 #wk2 #pk2 #l2 #i2 #d2 #b2 b t0 t1 -> assert_norm (as_type (T_cases b t0 t1) == P.t_ite b (fun _ -> as_type t0) (fun _ -> as_type t1)); - let p0 (_:squash b) = P.parse_weaken_right (as_parser t0) _ in - let p1 (_:squash (not b)) = P.parse_weaken_left (as_parser t1) _ in + let p0 (_:squash b) = P.parse_weaken_right (as_parser t0) pk2 in + let p1 (_:squash (not b)) = P.parse_weaken_left (as_parser t1) pk1 in assert_norm (as_parser (T_cases b t0 t1) == P.parse_ite b p0 p1); let v0 (_:squash b) = - A.validate_weaken_right (as_validator typename t0) _ + A.validate_weaken_right (as_validator typename t0) pk2 in let v1 (_:squash (not b)) = - A.validate_weaken_left (as_validator typename t1) _ + A.validate_weaken_left (as_validator typename t1) pk1 in - A.validate_ite b p0 v0 p1 v1 + coerce () (A.validate_ite b p0 v0 p1 v1) | T_with_action fn t a -> assert_norm (as_type (T_with_action fn t a) == as_type t); @@ -1285,22 +1281,22 @@ let rec as_validator A.validate_with_comment c (as_validator typename t) | T_nlist fn n t -> - assert_norm (as_type (T_nlist fn n t) == P.nlist n (as_type t)); - assert_norm (as_parser (T_nlist fn n t) == P.parse_nlist n (as_parser t)); + assert_norm (as_type (T_nlist fn n t) == P.nlist n (as_type t) (as_serializer t)); + assert_norm (as_parser (T_nlist fn n t) == P.parse_nlist n (as_serializer t)); A.validate_with_error_handler typename fn - (A.validate_nlist n (as_validator typename t)) + (A.validate_nlist n (as_serializer t) (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)); - assert_norm (as_parser (T_at_most fn n t) == P.parse_t_at_most n (as_parser t)); + assert_norm (as_type (T_at_most fn n t) == P.t_at_most n (as_type t) (as_serializer t)); + assert_norm (as_parser (T_at_most fn n t) == P.parse_t_at_most n (as_serializer t)); A.validate_with_error_handler typename fn - (A.validate_t_at_most n (as_validator typename t)) + (A.validate_t_at_most n (as_serializer t) (as_validator typename t)) | T_exact fn n t -> - assert_norm (as_type (T_exact fn n t) == P.t_exact n (as_type t)); - assert_norm (as_parser (T_exact fn n t) == P.parse_t_exact n (as_parser t)); + assert_norm (as_type (T_exact fn n t) == P.t_exact n (as_type t) (as_serializer t)); + assert_norm (as_parser (T_exact fn n t) == P.parse_t_exact n (as_serializer t)); A.validate_with_error_handler typename fn - (A.validate_t_exact n (as_validator typename t)) + (A.validate_t_exact n (as_serializer t) (as_validator typename t)) | T_string fn elt_t terminator -> assert_norm (as_type (T_string fn elt_t terminator) == P.cstring (dtyp_as_type elt_t) terminator); @@ -1370,6 +1366,7 @@ let mk_global_binding #nz #wk ([@@@erasable] loc:loc_index) ([@@@erasable] p_t : Type0) ([@@@erasable] p_p : P.parser pk p_t) + ((*[@@@erasable]*) p_s : P.serializer p_p) (p_reader: option (leaf_reader p_p)) (b:bool) (p_v : A.validate_with_action_t p_p @@ -1387,6 +1384,7 @@ let mk_global_binding #nz #wk loc = loc; p_t = p_t; p_p = p_p; + p_s = p_s; p_reader = p_reader; p_v = p_v } @@ -1416,6 +1414,7 @@ let mk_dtyp_app #nz #wk ([@@@erasable] loc:loc_index) ([@@@erasable] p_t : Type0) ([@@@erasable] p_p : P.parser pk p_t) + ((*[@@@erasable]*) p_s : P.serializer p_p) (p_reader: option (leaf_reader p_p)) (b:bool) (p_v : A.validate_with_action_t p_p @@ -1434,6 +1433,7 @@ let mk_dtyp_app #nz #wk loc = loc; p_t = p_t; p_p = p_p; + p_s = p_s; p_reader = p_reader; p_v = p_v } in diff --git a/src/3d/prelude/EverParse3d.Prelude.fst b/src/3d/prelude/EverParse3d.Prelude.fst index f272142f5..1bf442eac 100755 --- a/src/3d/prelude/EverParse3d.Prelude.fst +++ b/src/3d/prelude/EverParse3d.Prelude.fst @@ -98,17 +98,40 @@ let parse_impos () let parse_ite e p1 p2 = if e then p1 () else p2 () -let nlist (n:U32.t) (t:Type) = list t +let serializer p = LP.serializer p + +let serialize_dep_pair p1 p2 s1 s2 = LPC.serialize_dtuple2 s1 s2 + +let serialize_pair p1 p2 s1 s2 = LPC.serialize_nondep_then s1 s2 + +let serialize_filter p f s = LPC.serialize_filter s f + +inline_for_extraction noextract +let serialize_weaken_left #nz #wk #k p k' s b = s b inline_for_extraction noextract -let parse_nlist n #wk #k #t p +let serialize_weaken_right #nz #wk #k p k' s b = s b + +let serialize_impos () (t:False) = Seq.empty + +let serialize_ite e p1 p2 s1 s2 = + if e then s1 () else s2 () + +let nlist (n:U32.t) t #k #p s = + LowParse.Spec.FLData.parse_fldata_strong_t (LowParse.Spec.List.serialize_list p s) (U32.v n) + +inline_for_extraction noextract +let parse_nlist n s = let open LowParse.Spec.FLData in let open LowParse.Spec.List in parse_weaken - #false #WeakKindStrongPrefix #(parse_fldata_kind (U32.v n) parse_list_kind) #(list t) - (LowParse.Spec.FLData.parse_fldata (LowParse.Spec.List.parse_list p) (U32.v n)) + #false #WeakKindStrongPrefix #_ #_ + (parse_fldata_strong (serialize_list _ s) (U32.v n)) #false kind_nlist +let serialize_nlist n s b = + LowParse.Spec.FLData.serialize_fldata_strong _ _ b + let all_bytes = Seq.seq LP.byte let parse_all_bytes' : LP.bare_parser all_bytes @@ -116,38 +139,49 @@ let parse_all_bytes' let parse_all_bytes = LP.parser_kind_prop_equiv kind_all_bytes parse_all_bytes'; parse_all_bytes' +let serialize_all_bytes b = b //////////////////////////////////////////////////////////////////////////////// module B32 = FStar.Bytes -let t_at_most (n:U32.t) (t:Type) = t & all_bytes +let t_at_most (n:U32.t) (t:Type) s = + LowParse.Spec.FLData.parse_fldata_strong_t + (LPC.serialize_nondep_then s serialize_all_bytes) (U32.v n) + inline_for_extraction noextract -let parse_t_at_most n #nz #wk #k #t p +let parse_t_at_most n #nz #k #t #p s = let open LowParse.Spec.FLData in let open LowParse.Spec.List in parse_weaken #false #WeakKindStrongPrefix - (LowParse.Spec.FLData.parse_fldata - (LPC.nondep_then p parse_all_bytes) + (LowParse.Spec.FLData.parse_fldata_strong + (LPC.serialize_nondep_then s serialize_all_bytes) (U32.v n)) #false kind_t_at_most +let serialize_t_at_most n s b = + LowParse.Spec.FLData.serialize_fldata_strong _ _ b + //////////////////////////////////////////////////////////////////////////////// -let t_exact (n:U32.t) (t:Type) = t +let t_exact n t s = + LowParse.Spec.FLData.parse_fldata_strong_t s (U32.v n) inline_for_extraction noextract -let parse_t_exact n #nz #wk #k #t p +let parse_t_exact n #nz #k #t #p s = let open LowParse.Spec.FLData in let open LowParse.Spec.List in parse_weaken #false #WeakKindStrongPrefix - (LowParse.Spec.FLData.parse_fldata - p + (LowParse.Spec.FLData.parse_fldata_strong + s (U32.v n)) #false kind_t_exact +let serialize_t_exact n s b = + LowParse.Spec.FLData.serialize_fldata_strong _ _ b + //////////////////////////////////////////////////////////////////////////////// // Readers //////////////////////////////////////////////////////////////////////////////// @@ -180,7 +214,7 @@ let validator_no_read #nz #wk (#k:parser_kind nz wk) (#t:Type) (p:parser k t) = LPL.validator_no_read #k #t p let parse_nlist_total_fixed_size_aux - (n:U32.t) (#wk: _) (#k:parser_kind true wk) #t (p:parser k t) + (n:U32.t) (#k:parser_kind true WeakKindStrongPrefix) #t (p:parser k t) (s:serializer p) (x: LP.bytes) : Lemma (requires ( @@ -192,7 +226,7 @@ let parse_nlist_total_fixed_size_aux Seq.length x >= U32.v n )) (ensures ( - Some? (LP.parse (parse_nlist n p) x) + Some? (LP.parse (parse_nlist n s) x) )) = let x' = Seq.slice x 0 (U32.v n) in let cnt = (U32.v n / k.LP.parser_kind_low) in @@ -202,7 +236,7 @@ let parse_nlist_total_fixed_size_aux LP.parser_kind_prop_equiv LowParse.Spec.List.parse_list_kind (LowParse.Spec.List.parse_list p) let parse_nlist_total_fixed_size_kind_correct - (n:U32.t) (#wk: _) (#k:parser_kind true wk) #t (p:parser k t) + (n:U32.t) (#k:parser_kind true WeakKindStrongPrefix) #t (p:parser k t) (s:serializer p) : Lemma (requires ( let open LP in @@ -212,15 +246,15 @@ let parse_nlist_total_fixed_size_kind_correct k.parser_kind_metadata == Some ParserKindMetadataTotal )) (ensures ( - LP.parser_kind_prop (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n p) + LP.parser_kind_prop (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n s) )) -= LP.parser_kind_prop_equiv (LowParse.Spec.FLData.parse_fldata_kind (U32.v n) LowParse.Spec.List.parse_list_kind) (parse_nlist n p); - LP.parser_kind_prop_equiv (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n p); - Classical.forall_intro (Classical.move_requires (parse_nlist_total_fixed_size_aux n p)) += LP.parser_kind_prop_equiv (LowParse.Spec.FLData.parse_fldata_kind (U32.v n) LowParse.Spec.List.parse_list_kind) (parse_nlist n s); + LP.parser_kind_prop_equiv (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n s); + Classical.forall_intro (Classical.move_requires (parse_nlist_total_fixed_size_aux n p s)) inline_for_extraction noextract -let validate_nlist_total_constant_size_mod_ok (n:U32.t) #wk (#k:parser_kind true wk) (#t: Type) (p:parser k t) - : Pure (validator_no_read (parse_nlist n p)) +let validate_nlist_total_constant_size_mod_ok (n:U32.t) (#k:parser_kind true WeakKindStrongPrefix) (#t: Type) (p:parser k t) (s:serializer p) + : Pure (validator_no_read (parse_nlist n s)) (requires ( let open LP in k.parser_kind_subkind == Some ParserStrong /\ @@ -235,11 +269,11 @@ let validate_nlist_total_constant_size_mod_ok (n:U32.t) #wk (#k:parser_kind true let h = FStar.HyperStack.ST.get () in [@inline_let] let _ = - parse_nlist_total_fixed_size_kind_correct n p; - LPL.valid_facts (parse_nlist n p) h sl (LPL.uint64_to_uint32 pos); - LPL.valid_facts (LP.strengthen (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n p)) h sl (LPL.uint64_to_uint32 pos) + parse_nlist_total_fixed_size_kind_correct n p s; + LPL.valid_facts (parse_nlist n s) h sl (LPL.uint64_to_uint32 pos); + LPL.valid_facts (LP.strengthen (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n s)) h sl (LPL.uint64_to_uint32 pos) in - LPL.validate_total_constant_size_no_read (LP.strengthen (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n p)) (FStar.Int.Cast.uint32_to_uint64 n) () sl len pos + LPL.validate_total_constant_size_no_read (LP.strengthen (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n s)) (FStar.Int.Cast.uint32_to_uint64 n) () sl len pos ) module LUT = LowParse.Spec.ListUpTo @@ -265,11 +299,17 @@ let parse_string LowParse.Spec.Base.parser_kind_prop_equiv k p; LP.weaken parse_string_kind (LUT.parse_list_up_to (cond_string_up_to terminator) p (fun _ _ _ -> ())) +let serialize_string #k #t #p s terminator = + LowParse.Spec.Base.parser_kind_prop_equiv k p; + let s = LUT.serialize_list_up_to (cond_string_up_to terminator) (fun _ _ _ -> ()) s in + fun b -> s b + inline_for_extraction noextract let is_zero (x: FStar.UInt8.t) : Tot bool = x = 0uy let all_zeros = list (LowParse.Spec.Combinators.parse_filter_refine is_zero) let parse_all_zeros = LowParse.Spec.List.parse_list (LowParse.Spec.Combinators.parse_filter LowParse.Spec.Int.parse_u8 is_zero) +let serialize_all_zeros = LowParse.Spec.List.serialize_list _ (LowParse.Spec.Combinators.serialize_filter LowParse.Spec.Int.serialize_u8 is_zero) //////////////////////////////////////////////////////////////////////////////// @@ -278,37 +318,47 @@ let parse_all_zeros = LowParse.Spec.List.parse_list (LowParse.Spec.Combinators.p /// UINT8 let parse____UINT8 = LowParse.Spec.Int.parse_u8 +let serialize____UINT8 = LowParse.Spec.Int.serialize_u8 let read____UINT8 = LowParse.Low.Int.read_u8 /// UINT8BE let parse____UINT8BE = LowParse.Spec.Int.parse_u8 +let serialize____UINT8BE = LowParse.Spec.Int.serialize_u8 let read____UINT8BE = LowParse.Low.Int.read_u8 /// UInt16BE let parse____UINT16BE = LowParse.Spec.Int.parse_u16 +let serialize____UINT16BE = LowParse.Spec.Int.serialize_u16 let read____UINT16BE = LowParse.Low.Int.read_u16 /// UInt32BE let parse____UINT32BE = LowParse.Spec.Int.parse_u32 +let serialize____UINT32BE = LowParse.Spec.Int.serialize_u32 let read____UINT32BE = LowParse.Low.Int.read_u32 /// UInt64BE let parse____UINT64BE = LowParse.Spec.Int.parse_u64 +let serialize____UINT64BE = LowParse.Spec.Int.serialize_u64 let read____UINT64BE = LowParse.Low.Int.read_u64 /// UInt16 let parse____UINT16 = LowParse.Spec.BoundedInt.parse_u16_le +let serialize____UINT16 = LowParse.Spec.BoundedInt.serialize_u16_le let read____UINT16 = LowParse.Low.BoundedInt.read_u16_le /// UInt32 let parse____UINT32 = LowParse.Spec.BoundedInt.parse_u32_le +let serialize____UINT32 = LowParse.Spec.BoundedInt.serialize_u32_le let read____UINT32 = LowParse.Low.BoundedInt.read_u32_le /// UInt64 let parse____UINT64 = LowParse.Spec.Int.parse_u64_le +let serialize____UINT64 = LowParse.Spec.Int.serialize_u64_le let read____UINT64 = LowParse.Low.Int.read_u64_le + +let serialize_unit () = Seq.empty inline_for_extraction noextract let read_unit diff --git a/src/3d/prelude/EverParse3d.Prelude.fsti b/src/3d/prelude/EverParse3d.Prelude.fsti index 3b37ffd18..6eef680de 100644 --- a/src/3d/prelude/EverParse3d.Prelude.fsti +++ b/src/3d/prelude/EverParse3d.Prelude.fsti @@ -107,14 +107,67 @@ val parse_ite (#nz:_) (#wk: _) (#k:parser_kind nz wk) (p2:squash (not e) -> parser k (b())) : Tot (parser k (t_ite e a b)) +//////////////////////////////////////////////////////////////////////////////// +// Serializers +//////////////////////////////////////////////////////////////////////////////// + +// [@@erasable] // TODO: why does this not work? +inline_for_extraction +noextract +val serializer (#nz:bool) (#wk: weak_kind) (#k:parser_kind nz wk) (#t:Type u#r) (p: parser k t) : Type u#r + +inline_for_extraction noextract +val serialize_dep_pair + #nz1 (#k1:parser_kind nz1 WeakKindStrongPrefix) #t1 (p1: parser k1 t1) + #nz2 #wk2 (#k2:parser_kind nz2 wk2) (#t2: t1 -> Tot Type) (p2: (x: t1) -> parser k2 (t2 x)) + (s1:serializer p1) (s2:(x: t1) -> serializer (p2 x)) + : Tot (serializer (parse_dep_pair p1 p2)) + +inline_for_extraction noextract +val serialize_pair + #nz1 (#k1:parser_kind nz1 WeakKindStrongPrefix) #t1 (p1:parser k1 t1) + #nz2 #wk2 (#k2:parser_kind nz2 wk2) #t2 (p2:parser k2 t2) + (s1:serializer p1) (s2:serializer p2) + : Tot (serializer (parse_pair p1 p2)) + +inline_for_extraction noextract +val serialize_filter #nz #wk (#k:parser_kind nz wk) #t (p:parser k t) (f:t -> bool) (s:serializer p) + : Tot (serializer (parse_filter p f)) + +inline_for_extraction noextract +val serialize_weaken_left (#nz:_) (#wk: _) (#k:parser_kind nz wk) (#t:_) (p:parser k t) + (#nz':_) (#wk': _) (k':parser_kind nz' wk') (s:serializer p) + : Tot (serializer (parse_weaken_left p k')) + +inline_for_extraction noextract +val serialize_weaken_right (#nz:_) (#wk: _) (#k:parser_kind nz wk) (#t:_) (p:parser k t) + (#nz':_) (#wk': _) (k':parser_kind nz' wk') (s:serializer p) + : Tot (serializer (parse_weaken_right p k')) + +val serialize_impos (_:unit) : serializer (parse_impos ()) + +val serialize_ite (#nz:_) (#wk: _) (#k:parser_kind nz wk) + (e:bool) + (#a:squash e -> Type) + (#b:squash (not e) -> Type) + (p1:squash e -> parser k (a())) + (p2:squash (not e) -> parser k (b())) + (s1:squash e -> serializer (p1())) + (s2:squash (not e) -> serializer (p2())) + : Tot (serializer (parse_ite e p1 p2)) + //////////////////////////////////////////////////////////////////////////////// // Variable-sized list whose size in bytes is exactly n //////////////////////////////////////////////////////////////////////////////// -val nlist (n:U32.t) (t:Type u#r) : Type u#r +val nlist (n:U32.t) (t:Type u#r) (#k:parser_kind true WeakKindStrongPrefix) (#p:parser k t) (s:serializer p) : Type u#r + +inline_for_extraction noextract +val parse_nlist (n:U32.t) (#k:parser_kind true WeakKindStrongPrefix) (#t:_) (#p:parser k t) (s:serializer p) + : Tot (parser kind_nlist (nlist n t s)) inline_for_extraction noextract -val parse_nlist (n:U32.t) (#wk: _) (#k:parser_kind true wk) (#t:_) (p:parser k t) - : Tot (parser kind_nlist (nlist n t)) +val serialize_nlist (n:U32.t) (#k:parser_kind true WeakKindStrongPrefix) (#t:_) (#p:parser k t) (s:serializer p) + : Tot (serializer (parse_nlist n s)) ///// // Parse all of the remaining bytes of the input buffer @@ -123,24 +176,33 @@ noextract val all_bytes: Type0 val parse_all_bytes: parser kind_all_bytes all_bytes +val serialize_all_bytes: serializer parse_all_bytes //////////////////////////////////////////////////////////////////////////////// // Variable-sized element whose size in bytes is at most n //////////////////////////////////////////////////////////////////////////////// -val t_at_most (n:U32.t) (t:Type u#r) : Type u#r +val t_at_most (n:U32.t) (t:Type u#r) #nz (#k:parser_kind nz WeakKindStrongPrefix) (#p:parser k t) (s:serializer p) : Type u#r inline_for_extraction noextract -val parse_t_at_most (n:U32.t) (#nz: _) (#wk: _) (#k:parser_kind nz wk) (#t:_) (p:parser k t) - : Tot (parser kind_t_at_most (t_at_most n t)) +val parse_t_at_most (n:U32.t) (#nz: _) (#k:parser_kind nz WeakKindStrongPrefix) (#t:_) (#p:parser k t) (s:serializer p) + : Tot (parser kind_t_at_most (t_at_most n t s)) + +inline_for_extraction noextract +val serialize_t_at_most (n:U32.t) (#nz: _) (#k:parser_kind nz WeakKindStrongPrefix) (#t:_) (#p:parser k t) (s:serializer p) + : Tot (serializer (parse_t_at_most n s)) //////////////////////////////////////////////////////////////////////////////// // Variable-sized element whose size in bytes is exactly n //////////////////////////////////////////////////////////////////////////////// -val t_exact (n:U32.t) (t:Type u#r) : Type u#r +val t_exact (n:U32.t) (t:Type u#r) #nz (#k:parser_kind nz WeakKindStrongPrefix) (#p:parser k t) (s:serializer p) : Type u#r + +inline_for_extraction noextract +val parse_t_exact (n:U32.t) (#nz:bool) (#k:parser_kind nz WeakKindStrongPrefix) (#t:_) (#p:parser k t) (s:serializer p) + : Tot (parser kind_t_exact (t_exact n t s)) inline_for_extraction noextract -val parse_t_exact (n:U32.t) (#nz:bool) (#wk: _) (#k:parser_kind nz wk) (#t:_) (p:parser k t) - : Tot (parser kind_t_exact (t_exact n t)) +val serialize_t_exact (n:U32.t) (#nz:bool) (#k:parser_kind nz WeakKindStrongPrefix) (#t:_) (#p:parser k t) (s:serializer p) + : Tot (serializer (parse_t_exact n s)) //////////////////////////////////////////////////////////////////////////////// // Readers @@ -176,10 +238,19 @@ val parse_string (terminator: t) : Tot (parser parse_string_kind (cstring t terminator)) +val serialize_string + (#k: parser_kind true WeakKindStrongPrefix) + (#t: eqtype) + (#p: parser k t) + (s: serializer p) + (terminator: t) +: Tot (serializer (parse_string p terminator)) + noextract val all_zeros: Type0 val parse_all_zeros: parser kind_all_zeros all_zeros +val serialize_all_zeros: serializer parse_all_zeros //////////////////////////////////////////////////////////////////////////////// // Base types @@ -191,6 +262,7 @@ let ___Bool = bool /// UINT8 let ___UINT8 : eqtype = FStar.UInt8.t val parse____UINT8 : parser kind____UINT8 ___UINT8 +val serialize____UINT8 : serializer parse____UINT8 val read____UINT8 : reader parse____UINT8 // Big-endian (or "network order") @@ -198,21 +270,25 @@ val read____UINT8 : reader parse____UINT8 /// UINT8BE let ___UINT8BE : eqtype = FStar.UInt8.t val parse____UINT8BE : parser kind____UINT8BE ___UINT8BE +val serialize____UINT8BE : serializer parse____UINT8BE val read____UINT8BE : reader parse____UINT8BE /// UInt16BE let ___UINT16BE : eqtype = U16.t val parse____UINT16BE : parser kind____UINT16BE ___UINT16BE +val serialize____UINT16BE : serializer parse____UINT16BE val read____UINT16BE : reader parse____UINT16BE /// UInt32BE let ___UINT32BE : eqtype = U32.t val parse____UINT32BE : parser kind____UINT32BE ___UINT32BE +val serialize____UINT32BE : serializer parse____UINT32BE val read____UINT32BE : reader parse____UINT32BE /// UInt64BE let ___UINT64BE : eqtype = U64.t val parse____UINT64BE : parser kind____UINT64BE ___UINT64BE +val serialize____UINT64BE : serializer parse____UINT64BE val read____UINT64BE : reader parse____UINT64BE // Little-endian @@ -220,21 +296,25 @@ val read____UINT64BE : reader parse____UINT64BE /// UInt16 let ___UINT16 : eqtype = U16.t val parse____UINT16 : parser kind____UINT16 ___UINT16 +val serialize____UINT16 : serializer parse____UINT16 val read____UINT16 : reader parse____UINT16 /// UInt32 let ___UINT32 : eqtype = U32.t val parse____UINT32 : parser kind____UINT32 ___UINT32 +val serialize____UINT32 : serializer parse____UINT32 val read____UINT32 : reader parse____UINT32 /// UInt64 let ___UINT64 : eqtype = U64.t val parse____UINT64 : parser kind____UINT64 ___UINT64 +val serialize____UINT64 : serializer parse____UINT64 val read____UINT64 : reader parse____UINT64 let parse_unit : parser kind_unit unit = parse_ret () +val serialize_unit : serializer parse_unit inline_for_extraction noextract val read_unit From 697c8802ecd7624f844044479299d481beb969fd Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 22 Jan 2024 14:38:02 -0800 Subject: [PATCH 2/2] Extract EverParse3d.Intepreter interface. --- src/3d/prelude/EverParse3d.Interpreter.fst | 915 --------------- src/3d/prelude/EverParse3d.Interpreter.fsti | 1104 +++++++++++++++++++ 2 files changed, 1104 insertions(+), 915 deletions(-) create mode 100644 src/3d/prelude/EverParse3d.Interpreter.fsti diff --git a/src/3d/prelude/EverParse3d.Interpreter.fst b/src/3d/prelude/EverParse3d.Interpreter.fst index aa1daa0c8..b07341de8 100644 --- a/src/3d/prelude/EverParse3d.Interpreter.fst +++ b/src/3d/prelude/EverParse3d.Interpreter.fst @@ -24,10 +24,6 @@ module T = FStar.Tactics module CP = EverParse3d.CopyBuffer open FStar.List.Tot -inline_for_extraction -noextract -let ___EVERPARSE_COPY_BUFFER_T = CP.copy_buffer_t - (* This module defines a strongly typed abstract syntax for an intermediate representation of 3D programs. This is the type `typ`. @@ -56,157 +52,9 @@ let ___EVERPARSE_COPY_BUFFER_T = CP.copy_buffer_t for t-validator is an instance of the 1st Futamura projection. *) -(* An attribute to control partial evaluation *) -let specialize = () - (** You can see the basic idea of the whole stack working at first on a very simple class of types---just the primitive types *) -(* Primitive types *) -type itype = - | UInt8 - | UInt16 - | UInt32 - | UInt64 - | UInt8BE - | UInt16BE - | UInt32BE - | UInt64BE - | Unit - | AllBytes - | AllZeros - -(* Interpretation of itype as an F* type *) -[@@specialize] -let itype_as_type (i:itype) - : Type - = match i with - | UInt8 -> P.___UINT8 - | UInt16 -> P.___UINT16 - | UInt32 -> P.___UINT32 - | UInt64 -> P.___UINT64 - | UInt8BE -> P.___UINT8BE - | UInt16BE -> P.___UINT16BE - | UInt32BE -> P.___UINT32BE - | UInt64BE -> P.___UINT64BE - | Unit -> unit - | AllBytes -> P.all_bytes - | AllZeros -> P.all_zeros - -[@@specialize] -let parser_kind_nz_of_itype (i:itype) - : bool - = match i with - | Unit - | AllBytes - | AllZeros -> false - | _ -> true - -[@@specialize] -let parser_weak_kind_of_itype (i:itype) - : P.weak_kind - = match i with - | AllBytes - | AllZeros -> P.WeakKindConsumesAll - | _ -> P.WeakKindStrongPrefix - -(* Interpretation of itype as a parser kind *) -[@@specialize] -let parser_kind_of_itype (i:itype) - : P.parser_kind (parser_kind_nz_of_itype i) - (parser_weak_kind_of_itype i) - = match i with - | UInt8 -> P.kind____UINT8 - | UInt16 -> P.kind____UINT16 - | UInt32 -> P.kind____UINT32 - | UInt64 -> P.kind____UINT64 - | UInt8BE -> P.kind____UINT8BE - | UInt16BE -> P.kind____UINT16BE - | UInt32BE -> P.kind____UINT32BE - | UInt64BE -> P.kind____UINT64BE - | Unit -> P.kind_unit - | AllBytes -> P.kind_all_bytes - | AllZeros -> P.kind_all_zeros - -(* Interpretation of an itype as a parser *) -let itype_as_parser (i:itype) - : P.parser (parser_kind_of_itype i) (itype_as_type i) - = match i with - | UInt8 -> P.parse____UINT8 - | UInt16 -> P.parse____UINT16 - | UInt32 -> P.parse____UINT32 - | UInt64 -> P.parse____UINT64 - | UInt8BE -> P.parse____UINT8BE - | UInt16BE -> P.parse____UINT16BE - | UInt32BE -> P.parse____UINT32BE - | UInt64BE -> P.parse____UINT64BE - | Unit -> P.parse_unit - | AllBytes -> P.parse_all_bytes - | AllZeros -> P.parse_all_zeros - -(* Interpretation of an itype as a serializer *) -let itype_as_serializer (i:itype) - : P.serializer (itype_as_parser i) - = match i with - | UInt8 -> P.serialize____UINT8 - | UInt16 -> P.serialize____UINT16 - | UInt32 -> P.serialize____UINT32 - | UInt64 -> P.serialize____UINT64 - | UInt8BE -> P.serialize____UINT8BE - | UInt16BE -> P.serialize____UINT16BE - | UInt32BE -> P.serialize____UINT32BE - | UInt64BE -> P.serialize____UINT64BE - | Unit -> P.serialize_unit - | AllBytes -> P.serialize_all_bytes - | AllZeros -> P.serialize_all_zeros - -[@@specialize] -let allow_reader_of_itype (i:itype) - : bool - = match i with - | AllBytes - | AllZeros -> false - | _ -> true - -(* Interpretation of an itype as a leaf reader *) -[@@specialize] -let itype_as_leaf_reader (i:itype { allow_reader_of_itype i }) - : A.leaf_reader (itype_as_parser i) - = match i with - | UInt8 -> A.read____UINT8 - | UInt16 -> A.read____UINT16 - | UInt32 -> A.read____UINT32 - | UInt64 -> A.read____UINT64 - | UInt8BE -> A.read____UINT8BE - | UInt16BE -> A.read____UINT16BE - | UInt32BE -> A.read____UINT32BE - | UInt64BE -> A.read____UINT64BE - | Unit -> A.read_unit - -(* Interpretation of an itype as a validator - -- Notice that the type shows that it is related to the parser *) -[@@specialize] -let itype_as_validator (i:itype) - : A.validate_with_action_t - (itype_as_parser i) - A.true_inv - A.disjointness_trivial - A.eloc_none - (allow_reader_of_itype i) - = match i with - | UInt8 -> A.validate____UINT8 - | UInt16 -> A.validate____UINT16 - | UInt32 -> A.validate____UINT32 - | UInt64 -> A.validate____UINT64 - | UInt8BE -> A.validate____UINT8BE - | UInt16BE -> A.validate____UINT16BE - | UInt32BE -> A.validate____UINT32BE - | UInt64BE -> A.validate____UINT64BE - | Unit -> A.validate_unit - | AllBytes -> A.validate_all_bytes - | AllZeros -> A.validate_all_zeros - - (* Our first order of business to scale this up to 3D is to set up definitions for type contexts. @@ -217,215 +65,9 @@ let itype_as_validator (i:itype) which are in scope. *) -let leaf_reader #nz #wk (#k: P.parser_kind nz wk) #t (p:P.parser k t) - = _:squash (wk == P.WeakKindStrongPrefix /\ hasEq t) & - A.leaf_reader p - (* Now, we can define the type of an environment *) module T = FStar.Tactics -[@@erasable] -noeq -type index (a:Type) = - | Trivial : index a - | NonTrivial : a -> index a - -[@@specialize] -let join_index (j:'a -> 'a -> 'a) (i0 i1:index 'a) -: index 'a -= match i0 with - | Trivial -> i1 - | _ -> ( - match i1 with - | Trivial -> i0 - | NonTrivial i1 -> - let NonTrivial i0 = i0 in - NonTrivial (j i0 i1) - ) -[@@specialize] -let interp_index (triv:'a) (i:index 'a) -: GTot 'a -= match i with - | Trivial -> triv - | NonTrivial i -> i - - -let inv_index = index A.slice_inv -[@@specialize] -let inv_none : inv_index = Trivial -[@@specialize] -let join_inv = join_index A.conj_inv -[@@specialize] -let interp_inv = interp_index A.true_inv - -let loc_index = index A.eloc -[@@specialize] -let loc_none : loc_index = Trivial -[@@specialize] -let join_loc = join_index A.eloc_union -[@@specialize] -let interp_loc = interp_index A.eloc_none - -let disj_index = index A.disjointness_pre -[@@specialize] -let disj_none : disj_index = Trivial -[@@specialize] -let join_disj = join_index A.conj_disjointness -[@@specialize] -let interp_disj = interp_index A.disjointness_trivial -[@@specialize] -let disjoint (e1 e2:loc_index) - : disj_index - = match e1, e2 with - | Trivial, _ - | _, 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: - - Represents the lifting of a fully applied a shallow F* - quadruple of {type, parser, validator, opt reader} -*) -noeq -type global_binding = { - //Parser metadata - 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; - //Memory invariant of any actions it contains - inv:inv_index; - //Disjointness precondition - disj:disj_index; - //Write footprint of any of its actions - loc:loc_index; - //Its type denotation - p_t : Type0; - //Its parser denotation - p_p : P.parser parser_kind p_t; - //Its serializer denotation - p_s : P.serializer p_p; - //Whether the type can be read -- to avoid double fetches - p_reader: option (leaf_reader p_p); - //Its validate-with-action denotationa - p_v : A.validate_with_action_t - p_p - (interp_inv inv) - (interp_disj disj) - (interp_loc loc) - (Some? p_reader); -} - -let projector_names : list string = [ - `%Mkglobal_binding?.parser_kind_nz; - `%Mkglobal_binding?.parser_weak_kind; - `%Mkglobal_binding?.parser_kind; - `%Mkglobal_binding?.inv; - `%Mkglobal_binding?.disj; - `%Mkglobal_binding?.loc; - `%Mkglobal_binding?.p_t; - `%Mkglobal_binding?.p_p; - `%Mkglobal_binding?.p_s; - `%Mkglobal_binding?.p_reader; - `%Mkglobal_binding?.p_v; -] - -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 inv_of_binding = Mkglobal_binding?.inv -let disj_of_bindng = Mkglobal_binding?.disj -let loc_of_binding = Mkglobal_binding?.loc -let type_of_binding = Mkglobal_binding?.p_t -let parser_of_binding = Mkglobal_binding?.p_p -let serializer_of_binding = Mkglobal_binding?.p_s -let leaf_reader_of_binding = Mkglobal_binding?.p_reader -let validator_of_binding = Mkglobal_binding?.p_v - -let has_reader (g:global_binding) = - match leaf_reader_of_binding g with - | Some _ -> true - | _ -> false - -let reader_binding = g:global_binding { has_reader g } - -[@@specialize] -let get_leaf_reader (r:reader_binding) - : leaf_reader (parser_of_binding r) - = Some?.v (leaf_reader_of_binding r) - - -(* The main type of 3D types. Some points to note: - - - The indexing structure determines the types of the - parser/validator etc. of its denotation - - - All top-level names mentioned in a typ must be bound in the - context. - - - Constructs that bind local names are represented using F* - functions that abstract over denotations of the underlying types. - - - Some elements of the source programs are "pre-denoted". Notably, - every refinement formula is represented in this AST already as a - boolean function, rather than in some embedded language of - expressions. This is because expressions are not necessarily - well-formed by syntax alone---they may give rise to verification - conditions when using bounded arithmetic functions. So, it's the - obligation of the `typ` generator (i.e., the 3D frontend) to - produce boolean functions for those expressions that can be - verified natively by F* for type correctness. -*) - -noeq -type dtyp - : #nz:bool -> #wk:P.weak_kind -> - P.parser_kind nz wk -> - has_reader:bool -> - inv_index -> - disj_index -> - loc_index -> - Type = - | DT_IType: - i:itype -> - dtyp (parser_kind_of_itype i) - (allow_reader_of_itype i) - inv_none disj_none loc_none - - | DT_App: - (* We give explicit names to the indices rather than - projecting them as a small optimization for the reduction - machinery ... it's no longer clear that the speedup is significant *) - #nz:bool -> - #wk:P.weak_kind -> - pk:P.parser_kind nz wk -> - hr:bool -> - inv:inv_index -> - disj:disj_index -> - loc:loc_index -> - x:global_binding -> - _:squash (nz == nz_of_binding x /\ - wk == wk_of_binding x /\ - pk == pk_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 - -[@@specialize] -let dtyp_as_type #nz #wk (#pk:P.parser_kind nz wk) #hr #i #disj #l - (d:dtyp pk hr i disj l) - : Type - = match d with - | DT_IType i -> - itype_as_type i - - | 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) : Lemma @@ -507,122 +149,6 @@ let dtyp_as_leaf_reader #nz (#pk:P.parser_kind nz P.WeakKindStrongPrefix) (** Actions *) -let action_binding - (inv:inv_index) - (l:loc_index) - (on_success:bool) - (a:Type) - : Type u#0 - = A.action (interp_inv inv) A.disjointness_trivial (interp_loc l) on_success a - -inline_for_extraction -let extern_action (l:loc_index) = A.external_action (interp_loc l) - -inline_for_extraction -let mk_extern_action (#l:loc_index) ($f:extern_action l) - = A.mk_external_action f - -[@@specialize] -let mk_action_binding - (#l:loc_index) - ($f:extern_action l) - : action_binding inv_none l false unit - = mk_extern_action f - -(* The type of atomic actions. - - `atomic_action l i b t`: is an atomic action that - - may modify locations `l` - - relies on a memory invariant `i` - - b, when set, indicates that the action can only run in a success handler - - t, is the result type of the action - - In comparison with with the 3D front-end's internal representation - of actions, some notable differences - - - The indexing structure tell us exactly the type to which these - will translate. It's also worth comparing these types to the - types of the action primitives in Actions.fsti---the indexing - structure is the same - - - The type is already partially interpreted, e.g., rather than - relying on an explicit representation of names (e.g., in - Action_deref), this representation directly uses a pointer - value. -*) -noeq -type atomic_action - : inv_index -> disj_index -> loc_index -> bool -> Type0 -> Type u#1 = - | Action_return: - #a:Type0 -> - x:a -> - atomic_action inv_none disj_none loc_none false a - - | Action_abort: - atomic_action inv_none disj_none loc_none false bool - - | Action_field_pos_64: - atomic_action inv_none disj_none loc_none false U64.t - - | Action_field_pos_32: - squash (EverParse3d.Actions.BackendFlag.backend_flag == A.BackendFlagBuffer) -> - atomic_action inv_none disj_none loc_none false U32.t - - | Action_field_ptr: - squash (EverParse3d.Actions.BackendFlag.backend_flag == A.BackendFlagBuffer) -> - atomic_action inv_none disj_none loc_none true A.___PUINT8 - - | Action_field_ptr_after: - squash (EverParse3d.Actions.BackendFlag.backend_flag == A.BackendFlagExtern) -> - (sz: FStar.UInt64.t) -> - write_to: A.bpointer A.___PUINT8 -> - atomic_action (NonTrivial (A.ptr_inv write_to)) disj_none (NonTrivial (A.ptr_loc write_to)) false bool - - | Action_field_ptr_after_with_setter: - squash (EverParse3d.Actions.BackendFlag.backend_flag == A.BackendFlagExtern) -> - sz: FStar.UInt64.t -> - #out_loc:loc_index -> - write_to: (A.___PUINT8 -> Tot (extern_action out_loc)) -> - atomic_action inv_none disj_none out_loc false bool - - | Action_deref: - #a:Type0 -> - x:A.bpointer a -> - atomic_action (NonTrivial (A.ptr_inv x)) disj_none loc_none false a - - | Action_assignment: - #a:Type0 -> - x:A.bpointer a -> - rhs:a -> - atomic_action (NonTrivial (A.ptr_inv x)) disj_none (NonTrivial (A.ptr_loc x)) false unit - - | Action_call: - #inv:inv_index -> - #loc:loc_index -> - #b:bool -> - #t:Type0 -> - action_binding inv loc b t -> - atomic_action inv disj_none loc b t - - | Action_probe_then_validate: - #nz:bool -> - #wk:_ -> - #k:P.parser_kind nz wk -> - #has_reader:bool -> - #inv:inv_index -> - #disj:disj_index -> - #l:loc_index -> - dt:dtyp k has_reader inv disj l -> - src:U64.t -> - len:U64.t -> - dest:CP.copy_buffer_t -> - probe:CP.probe_fn -> - atomic_action (join_inv inv (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 bool - - (* Denotation of atomic_actions as A.action *) [@@specialize] let atomic_action_as_action @@ -655,40 +181,6 @@ let atomic_action_as_action let v = dtyp_as_validator dt in A.probe_then_validate v src len dest probe -(* A sub-language of monadic actions. - - The indexing structure mirrors the indexes of the combinators in - Actions.fst -*) -noeq -type action - : inv_index -> disj_index -> loc_index -> bool -> Type0 -> Type u#1 = - | Atomic_action: - #i:_ -> #d:_ -> #l:_ -> #b:_ -> #t:_ -> - atomic_action i d l b t -> - action i d l b t - - | Action_seq: - #i0:_ -> #l0:_ -> #b0:_ -> hd:atomic_action i0 disj_none l0 b0 unit -> - #i1:_ -> #l1:_ -> #b1:_ -> #t:_ -> tl:action i1 disj_none l1 b1 t -> - action (join_inv i0 i1) disj_none (join_loc l0 l1) (b0 || b1) t - - | Action_ite : - hd:bool -> - #i0:_ -> #l0:_ -> #b0:_ -> #t:_ -> then_:(_:squash hd -> action i0 disj_none l0 b0 t) -> - #i1:_ -> #l1:_ -> #b1:_ -> else_:(_:squash (not hd) -> action i1 disj_none l1 b1 t) -> - action (join_inv i0 i1) disj_none (join_loc l0 l1) (b0 || b1) t - - | Action_let: - #i0:_ -> #l0:_ -> #b0:_ -> #t0:_ -> head:atomic_action i0 disj_none l0 b0 t0 -> - #i1:_ -> #l1:_ -> #b1:_ -> #t1:_ -> k:(t0 -> action i1 disj_none l1 b1 t1) -> - action (join_inv i0 i1) disj_none (join_loc l0 l1) (b0 || b1) t1 - - | Action_act: - #i0:_ -> #l0:_ -> #b0:_ -> act:action i0 disj_none l0 b0 unit -> - action i0 disj_none l0 b0 bool - - (* Denotation of action as A.action *) [@@specialize] let rec action_as_action @@ -722,244 +214,6 @@ let rec action_as_action #_ #(interp_loc l0) -(* Some AST nodes contain source comments that we propagate to the output *) -let comments = string - -[@@ no_auto_projectors] -noeq -type typ - : #nz:bool -> #wk:P.weak_kind -> - P.parser_kind nz wk -> - inv_index -> - disj_index -> - loc_index -> - bool -> - Type = - | T_false: - fieldname:string -> - typ P.impos_kind inv_none disj_none loc_none 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 - - | T_pair: - first_fieldname:string -> - #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> - #i1:_ -> #d1:_ -> #l1:_ -> #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 -> - typ (P.and_then_kind pk1 pk2) - (join_inv i1 i2) - (join_disj d1 d2) - (join_loc l1 l2) - false - - | T_dep_pair: - first_fieldname:string -> - #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> - #i1:_ -> #d1:_ -> #l1:_ -> - #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> - #i2:_ -> #d2:_ -> #l2:_ -> #b2:bool -> - //the first component is a pre-denoted type with a reader - t1:dtyp pk1 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) -> - typ (P.and_then_kind pk1 pk2) - (join_inv i1 i2) - (join_disj d1 d2) - (join_loc l1 l2) - false - - | T_refine: - fieldname:string -> - #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> - #i1:_ -> #d1:_ -> #l1:_ -> - //the first component is a pre-denoted type with a reader - base:dtyp pk1 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 - - | T_refine_with_action: - fieldname:string -> - #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> - #i1:_ -> #d1:_ -> #l1:_ -> - #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> - base:dtyp pk1 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) - false - - | T_dep_pair_with_refinement: - //This construct serves two purposes - // 1. To avoid double fetches, we fold the refinement - // and dependent pair into a single form - // 2. This allows the well-typedness of the continuation k - // to depend on the refinement of the first field - first_fieldname:string -> - #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> - #i1:_ -> #d1:_ -> #l1:_ -> - #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> - #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> - //the first component is a pre-denoted type with a reader - base:dtyp pk1 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) -> - typ (P.and_then_kind (P.filter_kind pk1) pk2) - (join_inv i1 i2) - (join_disj d1 d2) - (join_loc l1 l2) - false - - | T_dep_pair_with_action: - fieldname:string -> - #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> - #i1:_ -> #d1:_ -> #l1:_ -> - #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> - #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> - #i3:_ -> #d3:_ -> #l3:_ -> #b3:_ -> - base:dtyp pk1 true i1 d1 l1 -> - k:(x:dtyp_as_type base -> typ pk2 i2 d2 l2 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)) - false - - | T_dep_pair_with_refinement_and_action: - //This construct serves two purposes - // 1. To avoid double fetches, we fold the refinement - // and dependent pair and action into a single form - // 2. This allows the well-typedness of the continuation k - // to depend on the refinement of the first field - first_fieldname:string -> - #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> - #i1:_ -> #d1:_ -> #l1:_ -> - #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> - #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> - #i3:_ -> #d3:_ -> #l3:_ -> #b3:_ -> - //the first component is a pre-denoted type with a reader - base:dtyp pk1 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) -> - 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)) - false - - | T_if_else: - #nz1:_ -> #wk1:_ -> #pk1:P.parser_kind nz1 wk1 -> - #l1:_ -> #i1:_ -> #d1:_ -> #b1:_ -> - #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> - #l2:_ -> #i2:_ -> #d2:_ -> #b2:_ -> - 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) -> - typ (P.glb pk1 pk2) - (join_inv i1 i2) - (join_disj d1 d2) - (join_loc l1 l2) false - - | T_cases: - #nz1:_ -> #wk1:_ -> #pk1:P.parser_kind nz1 wk1 -> - #l1:_ -> #i1:_ -> #d1:_ -> #b1:_ -> - #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> - #l2:_ -> #i2:_ -> #d2:_ -> #b2:_ -> - b:bool -> //A bool, rather than an expression - t1:typ pk1 i1 d1 l1 b1 -> - t2:typ pk2 i2 d2 l2 b2 -> - typ (P.glb pk1 pk2) - (join_inv i1 i2) - (join_disj d1 d2) - (join_loc l1 l2) - false - - | T_with_action: - fieldname:string -> - #nz:_ -> #wk:_ -> #pk:P.parser_kind nz wk -> - #l1:_ -> #i1:_ -> #d1:_ -> #b1:_ -> - #l2:_ -> #i2:_ -> #d2:_ -> #b2:_ -> - base:typ pk i1 d1 l1 b1 -> - act:action i2 d2 l2 b2 bool -> - typ pk (join_inv i1 i2) (join_disj d1 d2) (join_loc l1 l2) false - - | T_with_dep_action: - fieldname:string -> - #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> - #i1:_ -> #d1: _ -> #l1:_ -> - #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> - head:dtyp pk1 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 - - | T_with_comment: - fieldname:string -> - #nz:_ -> #wk:_ -> #pk:P.parser_kind nz wk -> - #l:_ -> #i:_ -> #d:_ -> #b:_ -> - t:typ pk i d l b -> - c:comments -> - typ pk i d l b - - | T_nlist: - fieldname:string -> - #pk:P.parser_kind true P.WeakKindStrongPrefix -> - #i:_ -> #l:_ -> #d:_ -> #b:_ -> - n:U32.t -> - t:typ pk i d l b -> - typ P.kind_nlist i d l false - - | T_at_most: - fieldname:string -> - #nz:_ -> #pk:P.parser_kind nz P.WeakKindStrongPrefix -> - #i:_ -> #d:_ -> #l:_ -> #b:_ -> - n:U32.t -> - t:typ pk i d l b -> - typ P.kind_t_at_most i d l false - - | T_exact: - fieldname:string -> - #nz:_ -> #pk:P.parser_kind nz P.WeakKindStrongPrefix -> - #i:_ -> #d:_ -> #l:_ -> #b:_ -> - n:U32.t -> - t:typ pk i d l b -> - typ P.kind_t_exact i d l false - - | T_string: - fieldname:string -> - #pk1:P.parser_kind true P.WeakKindStrongPrefix -> - element_type:dtyp pk1 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 - - -[@@specialize] -inline_for_extraction -let coerce (#[@@@erasable]a:Type) - (#[@@@erasable]b:Type) - ( [@@@erasable]pf:squash (a == b)) - (x:a) - : b - = x - [@@specialize] let t_probe_then_validate (fieldname:string) @@ -1306,172 +560,3 @@ let rec as_validator (dtyp_as_leaf_reader elt_t) terminator) #pop-options -[@@noextract_to "krml"; specialize] -inline_for_extraction noextract -let validator_of #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) = - A.validate_with_action_t - (as_parser t) - (interp_inv i) - (interp_disj d) - (interp_loc l) - allow_reading - -[@@noextract_to "krml"; specialize] -inline_for_extraction noextract -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 - -let specialization_steps = - [nbe; - zeta; - primops; - iota; - delta_attr [`%specialize]; - delta_only ([`%Some?; - `%Some?.v; - `%as_validator; - `%nz_of_binding; - `%wk_of_binding; - `%pk_of_binding; - `%inv_of_binding; - `%loc_of_binding; - `%type_of_binding; - `%parser_of_binding; - `%validator_of_binding; - `%leaf_reader_of_binding; - `%fst; - `%snd; - `%Mktuple2?._1; - `%Mktuple2?._2]@projector_names)] - -let specialize_tac steps (_:unit) - : T.Tac unit - = let open FStar.List.Tot in - T.norm (steps@specialization_steps); - T.trefl() - -[@@specialize] -let mk_global_binding #nz #wk - (pk:P.parser_kind nz wk) - ([@@@erasable] inv:inv_index) - ([@@@erasable] disj:disj_index) - ([@@@erasable] loc:loc_index) - ([@@@erasable] p_t : Type0) - ([@@@erasable] p_p : P.parser pk p_t) - ((*[@@@erasable]*) p_s : P.serializer p_p) - (p_reader: option (leaf_reader p_p)) - (b:bool) - (p_v : A.validate_with_action_t p_p - (interp_inv inv) - (interp_disj disj) - (interp_loc loc) b) - ([@@@erasable] pf:squash (b == Some? p_reader)) - : global_binding - = { - parser_kind_nz = nz; - parser_weak_kind = wk; - parser_kind = pk; - inv = inv; - disj; - loc = loc; - p_t = p_t; - p_p = p_p; - p_s = p_s; - p_reader = p_reader; - p_v = p_v - } - -[@@specialize] -let mk_dt_app #nz #wk (pk:P.parser_kind nz wk) (b:bool) - ([@@@erasable] inv:inv_index) - ([@@@erasable] disj:disj_index) - ([@@@erasable] loc:loc_index) - (x:global_binding) - ([@@@erasable] pf:squash (nz == nz_of_binding x /\ - wk == wk_of_binding x /\ - pk == pk_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 - - -[@@specialize] -let mk_dtyp_app #nz #wk - (pk:P.parser_kind nz wk) - ([@@@erasable] inv:inv_index) - ([@@@erasable] disj:disj_index) - ([@@@erasable] loc:loc_index) - ([@@@erasable] p_t : Type0) - ([@@@erasable] p_p : P.parser pk p_t) - ((*[@@@erasable]*) p_s : P.serializer p_p) - (p_reader: option (leaf_reader p_p)) - (b:bool) - (p_v : A.validate_with_action_t p_p - (interp_inv inv) - (interp_disj disj) - (interp_loc loc) - b) - ([@@@erasable] pf:squash (b == Some? p_reader)) - : dtyp #nz #wk pk b inv disj loc - = let gb = { - parser_kind_nz = nz; - parser_weak_kind = wk; - parser_kind = pk; - inv = inv; - disj; - loc = loc; - p_t = p_t; - p_p = p_p; - p_s = p_s; - p_reader = p_reader; - p_v = p_v - } in - DT_App pk b inv disj loc gb () - -//attribute to tag disjointness indexes of type definitions -let specialize_disjointness = () -let coerce_validator steps : T.Tac unit = - let open FStar.List.Tot in - T.norm [delta_only (steps @ [`%parser_kind_of_itype; - `%parser_kind_nz_of_itype; - `%fst; - `%snd; - `%Mktuple2?._1; - `%Mktuple2?._2; - `%coerce; - `%validator_of; - `%dtyp_of; - `%join_disj; - ]); - delta_attr [`%specialize_disjointness]; - zeta; - iota; - primops]; - T.trefl() - - -let coerce_dt_app (steps:_) : T.Tac unit = - let open FStar.List.Tot in - T.norm [delta_only (steps@[`%nz_of_binding; - `%wk_of_binding; - `%pk_of_binding; - `%has_reader; - `%leaf_reader_of_binding; - `%inv_of_binding; - `%loc_of_binding; - `%mk_global_binding]@projector_names); - zeta; - iota; - simplify]; - T.trivial() diff --git a/src/3d/prelude/EverParse3d.Interpreter.fsti b/src/3d/prelude/EverParse3d.Interpreter.fsti new file mode 100644 index 000000000..df1a9697a --- /dev/null +++ b/src/3d/prelude/EverParse3d.Interpreter.fsti @@ -0,0 +1,1104 @@ +(* + Copyright 2021 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + + Authors: N. Swamy, ... +*) +module EverParse3d.Interpreter +module U32 = FStar.UInt32 +module U64 = FStar.UInt64 +module A = EverParse3d.Actions.All +module P = EverParse3d.Prelude +module T = FStar.Tactics +module CP = EverParse3d.CopyBuffer +open FStar.List.Tot + +inline_for_extraction +noextract +let ___EVERPARSE_COPY_BUFFER_T = CP.copy_buffer_t + +(* This module defines a strongly typed abstract syntax for an + intermediate representation of 3D programs. This is the type `typ`. + + The main idea of this module is to give `typ`s a threefold + denotation: + + 1. Type denotation: `as_type` interprets a `typ` as an F* type + + 2. Parser denotation: `as_parser` interprets a `t:typ` as a parser + of values of the type denotation of `t`. + + 3. Validate-with-action denotation: `as_validator` inteprets a + `t:typ` as a low-level validator corresponding to the parser + denotation of `t`. + + The 3rd denotation, validate-with-action, is the main operational + denotation. That is, given a 3D program `t:typ` we can interpret it + as validator to check that an input array of bytes conforms to the + format specified by `t`. But, what we want ultimately is a C + program for a `t`-validator. + + To achieve this, for any given concrete `t`, we partially evaluate + this interpreter to get an EverParse validator specialized to `t` + which can be extracted by F*/KaRaMeL as usual---this partial + evaluation of an interpreter to a compiler producing a C program + for t-validator is an instance of the 1st Futamura projection. + *) + +(* An attribute to control partial evaluation *) +let specialize = () + +(** You can see the basic idea of the whole stack working at first on + a very simple class of types---just the primitive types *) + +(* Primitive types *) +type itype = + | UInt8 + | UInt16 + | UInt32 + | UInt64 + | UInt8BE + | UInt16BE + | UInt32BE + | UInt64BE + | Unit + | AllBytes + | AllZeros + +(* Interpretation of itype as an F* type *) +[@@specialize] +let itype_as_type (i:itype) + : Type + = match i with + | UInt8 -> P.___UINT8 + | UInt16 -> P.___UINT16 + | UInt32 -> P.___UINT32 + | UInt64 -> P.___UINT64 + | UInt8BE -> P.___UINT8BE + | UInt16BE -> P.___UINT16BE + | UInt32BE -> P.___UINT32BE + | UInt64BE -> P.___UINT64BE + | Unit -> unit + | AllBytes -> P.all_bytes + | AllZeros -> P.all_zeros + +[@@specialize] +let parser_kind_nz_of_itype (i:itype) + : bool + = match i with + | Unit + | AllBytes + | AllZeros -> false + | _ -> true + +[@@specialize] +let parser_weak_kind_of_itype (i:itype) + : P.weak_kind + = match i with + | AllBytes + | AllZeros -> P.WeakKindConsumesAll + | _ -> P.WeakKindStrongPrefix + +(* Interpretation of itype as a parser kind *) +[@@specialize] +let parser_kind_of_itype (i:itype) + : P.parser_kind (parser_kind_nz_of_itype i) + (parser_weak_kind_of_itype i) + = match i with + | UInt8 -> P.kind____UINT8 + | UInt16 -> P.kind____UINT16 + | UInt32 -> P.kind____UINT32 + | UInt64 -> P.kind____UINT64 + | UInt8BE -> P.kind____UINT8BE + | UInt16BE -> P.kind____UINT16BE + | UInt32BE -> P.kind____UINT32BE + | UInt64BE -> P.kind____UINT64BE + | Unit -> P.kind_unit + | AllBytes -> P.kind_all_bytes + | AllZeros -> P.kind_all_zeros + +(* Interpretation of an itype as a parser *) +let itype_as_parser (i:itype) + : P.parser (parser_kind_of_itype i) (itype_as_type i) + = match i with + | UInt8 -> P.parse____UINT8 + | UInt16 -> P.parse____UINT16 + | UInt32 -> P.parse____UINT32 + | UInt64 -> P.parse____UINT64 + | UInt8BE -> P.parse____UINT8BE + | UInt16BE -> P.parse____UINT16BE + | UInt32BE -> P.parse____UINT32BE + | UInt64BE -> P.parse____UINT64BE + | Unit -> P.parse_unit + | AllBytes -> P.parse_all_bytes + | AllZeros -> P.parse_all_zeros + +(* Interpretation of an itype as a serializer *) +let itype_as_serializer (i:itype) + : P.serializer (itype_as_parser i) + = match i with + | UInt8 -> P.serialize____UINT8 + | UInt16 -> P.serialize____UINT16 + | UInt32 -> P.serialize____UINT32 + | UInt64 -> P.serialize____UINT64 + | UInt8BE -> P.serialize____UINT8BE + | UInt16BE -> P.serialize____UINT16BE + | UInt32BE -> P.serialize____UINT32BE + | UInt64BE -> P.serialize____UINT64BE + | Unit -> P.serialize_unit + | AllBytes -> P.serialize_all_bytes + | AllZeros -> P.serialize_all_zeros + +[@@specialize] +let allow_reader_of_itype (i:itype) + : bool + = match i with + | AllBytes + | AllZeros -> false + | _ -> true + +(* Interpretation of an itype as a leaf reader *) +[@@specialize] +let itype_as_leaf_reader (i:itype { allow_reader_of_itype i }) + : A.leaf_reader (itype_as_parser i) + = match i with + | UInt8 -> A.read____UINT8 + | UInt16 -> A.read____UINT16 + | UInt32 -> A.read____UINT32 + | UInt64 -> A.read____UINT64 + | UInt8BE -> A.read____UINT8BE + | UInt16BE -> A.read____UINT16BE + | UInt32BE -> A.read____UINT32BE + | UInt64BE -> A.read____UINT64BE + | Unit -> A.read_unit + +(* Interpretation of an itype as a validator + -- Notice that the type shows that it is related to the parser *) +[@@specialize] +let itype_as_validator (i:itype) + : A.validate_with_action_t + (itype_as_parser i) + A.true_inv + A.disjointness_trivial + A.eloc_none + (allow_reader_of_itype i) + = match i with + | UInt8 -> A.validate____UINT8 + | UInt16 -> A.validate____UINT16 + | UInt32 -> A.validate____UINT32 + | UInt64 -> A.validate____UINT64 + | UInt8BE -> A.validate____UINT8BE + | UInt16BE -> A.validate____UINT16BE + | UInt32BE -> A.validate____UINT32BE + | UInt64BE -> A.validate____UINT64BE + | Unit -> A.validate_unit + | AllBytes -> A.validate_all_bytes + | AllZeros -> A.validate_all_zeros + + +(* Our first order of business to scale this up to 3D is to set up + definitions for type contexts. + + A 3D program is a sequence of top-level definitions, where a given + definition may reference terms defined previously. To model this, + we'll given a denotation of programs in a _context_, where the + context provides denotations for all the names defined previously + which are in scope. +*) + +let leaf_reader #nz #wk (#k: P.parser_kind nz wk) #t (p:P.parser k t) + = _:squash (wk == P.WeakKindStrongPrefix /\ hasEq t) & + A.leaf_reader p + +(* Now, we can define the type of an environment *) +module T = FStar.Tactics + +[@@erasable] +noeq +type index (a:Type) = + | Trivial : index a + | NonTrivial : a -> index a + +[@@specialize] +let join_index (j:'a -> 'a -> 'a) (i0 i1:index 'a) +: index 'a += match i0 with + | Trivial -> i1 + | _ -> ( + match i1 with + | Trivial -> i0 + | NonTrivial i1 -> + let NonTrivial i0 = i0 in + NonTrivial (j i0 i1) + ) +[@@specialize] +let interp_index (triv:'a) (i:index 'a) +: GTot 'a += match i with + | Trivial -> triv + | NonTrivial i -> i + + +let inv_index = index A.slice_inv +[@@specialize] +let inv_none : inv_index = Trivial +[@@specialize] +let join_inv = join_index A.conj_inv +[@@specialize] +let interp_inv = interp_index A.true_inv + +let loc_index = index A.eloc +[@@specialize] +let loc_none : loc_index = Trivial +[@@specialize] +let join_loc = join_index A.eloc_union +[@@specialize] +let interp_loc = interp_index A.eloc_none + +let disj_index = index A.disjointness_pre +[@@specialize] +let disj_none : disj_index = Trivial +[@@specialize] +let join_disj = join_index A.conj_disjointness +[@@specialize] +let interp_disj = interp_index A.disjointness_trivial +[@@specialize] +let disjoint (e1 e2:loc_index) + : disj_index + = match e1, e2 with + | Trivial, _ + | _, 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: + + Represents the lifting of a fully applied a shallow F* + quadruple of {type, parser, validator, opt reader} +*) +noeq +type global_binding = { + //Parser metadata + 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; + //Memory invariant of any actions it contains + inv:inv_index; + //Disjointness precondition + disj:disj_index; + //Write footprint of any of its actions + loc:loc_index; + //Its type denotation + p_t : Type0; + //Its parser denotation + p_p : P.parser parser_kind p_t; + //Its serializer denotation + p_s : P.serializer p_p; + //Whether the type can be read -- to avoid double fetches + p_reader: option (leaf_reader p_p); + //Its validate-with-action denotationa + p_v : A.validate_with_action_t + p_p + (interp_inv inv) + (interp_disj disj) + (interp_loc loc) + (Some? p_reader); +} + +let projector_names : list string = [ + `%Mkglobal_binding?.parser_kind_nz; + `%Mkglobal_binding?.parser_weak_kind; + `%Mkglobal_binding?.parser_kind; + `%Mkglobal_binding?.inv; + `%Mkglobal_binding?.disj; + `%Mkglobal_binding?.loc; + `%Mkglobal_binding?.p_t; + `%Mkglobal_binding?.p_p; + `%Mkglobal_binding?.p_s; + `%Mkglobal_binding?.p_reader; + `%Mkglobal_binding?.p_v; +] + +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 inv_of_binding = Mkglobal_binding?.inv +let disj_of_bindng = Mkglobal_binding?.disj +let loc_of_binding = Mkglobal_binding?.loc +let type_of_binding = Mkglobal_binding?.p_t +let parser_of_binding = Mkglobal_binding?.p_p +let serializer_of_binding = Mkglobal_binding?.p_s +let leaf_reader_of_binding = Mkglobal_binding?.p_reader +let validator_of_binding = Mkglobal_binding?.p_v + +let has_reader (g:global_binding) = + match leaf_reader_of_binding g with + | Some _ -> true + | _ -> false + +let reader_binding = g:global_binding { has_reader g } + +[@@specialize] +let get_leaf_reader (r:reader_binding) + : leaf_reader (parser_of_binding r) + = Some?.v (leaf_reader_of_binding r) + + +(* The main type of 3D types. Some points to note: + + - The indexing structure determines the types of the + parser/validator etc. of its denotation + + - All top-level names mentioned in a typ must be bound in the + context. + + - Constructs that bind local names are represented using F* + functions that abstract over denotations of the underlying types. + + - Some elements of the source programs are "pre-denoted". Notably, + every refinement formula is represented in this AST already as a + boolean function, rather than in some embedded language of + expressions. This is because expressions are not necessarily + well-formed by syntax alone---they may give rise to verification + conditions when using bounded arithmetic functions. So, it's the + obligation of the `typ` generator (i.e., the 3D frontend) to + produce boolean functions for those expressions that can be + verified natively by F* for type correctness. +*) + +noeq +type dtyp + : #nz:bool -> #wk:P.weak_kind -> + P.parser_kind nz wk -> + has_reader:bool -> + inv_index -> + disj_index -> + loc_index -> + Type = + | DT_IType: + i:itype -> + dtyp (parser_kind_of_itype i) + (allow_reader_of_itype i) + inv_none disj_none loc_none + + | DT_App: + (* We give explicit names to the indices rather than + projecting them as a small optimization for the reduction + machinery ... it's no longer clear that the speedup is significant *) + #nz:bool -> + #wk:P.weak_kind -> + pk:P.parser_kind nz wk -> + hr:bool -> + inv:inv_index -> + disj:disj_index -> + loc:loc_index -> + x:global_binding -> + _:squash (nz == nz_of_binding x /\ + wk == wk_of_binding x /\ + pk == pk_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 + +[@@specialize] +let dtyp_as_type #nz #wk (#pk:P.parser_kind nz wk) #hr #i #disj #l + (d:dtyp pk hr i disj l) + : Type + = match d with + | DT_IType i -> + itype_as_type i + + | DT_App _ _ _ _ _ b _ -> + type_of_binding b + +val dtyp_as_eqtype_lemma #nz #wk (#pk:P.parser_kind nz wk) #i #disj #l + (d:dtyp pk true i disj l) + : Lemma + (ensures hasEq (dtyp_as_type d)) + [SMTPat (hasEq (dtyp_as_type d))] + + +val dtyp_as_parser #nz #wk (#pk:P.parser_kind nz wk) #hr #i #disj #l + (d:dtyp pk hr i disj l) + : P.parser pk (dtyp_as_type d) + +val dtyp_as_serializer #nz #wk (#pk:P.parser_kind nz wk) #hr #i #disj #l + (d:dtyp pk hr i disj l) + : P.serializer (dtyp_as_parser d) + +[@@specialize] +val dtyp_as_validator #nz #wk (#pk:P.parser_kind nz wk) + (#hr:_) + (#[@@@erasable] i:inv_index) + (#[@@@erasable] disj:disj_index) + (#[@@@erasable] l:loc_index) + (d:dtyp pk 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 + +[@@specialize] +val dtyp_as_leaf_reader #nz (#pk:P.parser_kind nz P.WeakKindStrongPrefix) + (#[@@@erasable] i:inv_index) + (#[@@@erasable] disj:disj_index) + (#[@@@erasable] l:loc_index) + (d:dtyp pk true i disj l) + : A.leaf_reader (dtyp_as_parser d) + +(** Actions *) + +let action_binding + (inv:inv_index) + (l:loc_index) + (on_success:bool) + (a:Type) + : Type u#0 + = A.action (interp_inv inv) A.disjointness_trivial (interp_loc l) on_success a + +inline_for_extraction +let extern_action (l:loc_index) = A.external_action (interp_loc l) + +inline_for_extraction +let mk_extern_action (#l:loc_index) ($f:extern_action l) + = A.mk_external_action f + +[@@specialize] +let mk_action_binding + (#l:loc_index) + ($f:extern_action l) + : action_binding inv_none l false unit + = mk_extern_action f + +(* The type of atomic actions. + + `atomic_action l i b t`: is an atomic action that + - may modify locations `l` + - relies on a memory invariant `i` + - b, when set, indicates that the action can only run in a success handler + - t, is the result type of the action + + In comparison with with the 3D front-end's internal representation + of actions, some notable differences + + - The indexing structure tell us exactly the type to which these + will translate. It's also worth comparing these types to the + types of the action primitives in Actions.fsti---the indexing + structure is the same + + - The type is already partially interpreted, e.g., rather than + relying on an explicit representation of names (e.g., in + Action_deref), this representation directly uses a pointer + value. +*) +noeq +type atomic_action + : inv_index -> disj_index -> loc_index -> bool -> Type0 -> Type u#1 = + | Action_return: + #a:Type0 -> + x:a -> + atomic_action inv_none disj_none loc_none false a + + | Action_abort: + atomic_action inv_none disj_none loc_none false bool + + | Action_field_pos_64: + atomic_action inv_none disj_none loc_none false U64.t + + | Action_field_pos_32: + squash (EverParse3d.Actions.BackendFlag.backend_flag == A.BackendFlagBuffer) -> + atomic_action inv_none disj_none loc_none false U32.t + + | Action_field_ptr: + squash (EverParse3d.Actions.BackendFlag.backend_flag == A.BackendFlagBuffer) -> + atomic_action inv_none disj_none loc_none true A.___PUINT8 + + | Action_field_ptr_after: + squash (EverParse3d.Actions.BackendFlag.backend_flag == A.BackendFlagExtern) -> + (sz: FStar.UInt64.t) -> + write_to: A.bpointer A.___PUINT8 -> + atomic_action (NonTrivial (A.ptr_inv write_to)) disj_none (NonTrivial (A.ptr_loc write_to)) false bool + + | Action_field_ptr_after_with_setter: + squash (EverParse3d.Actions.BackendFlag.backend_flag == A.BackendFlagExtern) -> + sz: FStar.UInt64.t -> + #out_loc:loc_index -> + write_to: (A.___PUINT8 -> Tot (extern_action out_loc)) -> + atomic_action inv_none disj_none out_loc false bool + + | Action_deref: + #a:Type0 -> + x:A.bpointer a -> + atomic_action (NonTrivial (A.ptr_inv x)) disj_none loc_none false a + + | Action_assignment: + #a:Type0 -> + x:A.bpointer a -> + rhs:a -> + atomic_action (NonTrivial (A.ptr_inv x)) disj_none (NonTrivial (A.ptr_loc x)) false unit + + | Action_call: + #inv:inv_index -> + #loc:loc_index -> + #b:bool -> + #t:Type0 -> + action_binding inv loc b t -> + atomic_action inv disj_none loc b t + + | Action_probe_then_validate: + #nz:bool -> + #wk:_ -> + #k:P.parser_kind nz wk -> + #has_reader:bool -> + #inv:inv_index -> + #disj:disj_index -> + #l:loc_index -> + dt:dtyp k has_reader inv disj l -> + src:U64.t -> + len:U64.t -> + dest:CP.copy_buffer_t -> + probe:CP.probe_fn -> + atomic_action (join_inv inv (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 bool + + +(* Denotation of atomic_actions as A.action *) +[@@specialize] +val atomic_action_as_action + (#i #d #l #b #t:_) + (a:atomic_action i d l b t) + : Tot (A.action (interp_inv i) (interp_disj d) (interp_loc l) b t) + +(* A sub-language of monadic actions. + + The indexing structure mirrors the indexes of the combinators in + Actions.fst +*) +noeq +type action + : inv_index -> disj_index -> loc_index -> bool -> Type0 -> Type u#1 = + | Atomic_action: + #i:_ -> #d:_ -> #l:_ -> #b:_ -> #t:_ -> + atomic_action i d l b t -> + action i d l b t + + | Action_seq: + #i0:_ -> #l0:_ -> #b0:_ -> hd:atomic_action i0 disj_none l0 b0 unit -> + #i1:_ -> #l1:_ -> #b1:_ -> #t:_ -> tl:action i1 disj_none l1 b1 t -> + action (join_inv i0 i1) disj_none (join_loc l0 l1) (b0 || b1) t + + | Action_ite : + hd:bool -> + #i0:_ -> #l0:_ -> #b0:_ -> #t:_ -> then_:(_:squash hd -> action i0 disj_none l0 b0 t) -> + #i1:_ -> #l1:_ -> #b1:_ -> else_:(_:squash (not hd) -> action i1 disj_none l1 b1 t) -> + action (join_inv i0 i1) disj_none (join_loc l0 l1) (b0 || b1) t + + | Action_let: + #i0:_ -> #l0:_ -> #b0:_ -> #t0:_ -> head:atomic_action i0 disj_none l0 b0 t0 -> + #i1:_ -> #l1:_ -> #b1:_ -> #t1:_ -> k:(t0 -> action i1 disj_none l1 b1 t1) -> + action (join_inv i0 i1) disj_none (join_loc l0 l1) (b0 || b1) t1 + + | Action_act: + #i0:_ -> #l0:_ -> #b0:_ -> act:action i0 disj_none l0 b0 unit -> + action i0 disj_none l0 b0 bool + + +(* Denotation of action as A.action *) +[@@specialize] +val action_as_action + (#i #d #l #b #t:_) + (a:action i d l b t) + : Tot (A.action (interp_inv i) (interp_disj d) (interp_loc l) b t) + +(* Some AST nodes contain source comments that we propagate to the output *) +let comments = string + +[@@ no_auto_projectors] +noeq +type typ + : #nz:bool -> #wk:P.weak_kind -> + P.parser_kind nz wk -> + inv_index -> + disj_index -> + loc_index -> + bool -> + Type = + | T_false: + fieldname:string -> + typ P.impos_kind inv_none disj_none loc_none 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 + + | T_pair: + first_fieldname:string -> + #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> + #i1:_ -> #d1:_ -> #l1:_ -> #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 -> + typ (P.and_then_kind pk1 pk2) + (join_inv i1 i2) + (join_disj d1 d2) + (join_loc l1 l2) + false + + | T_dep_pair: + first_fieldname:string -> + #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> + #i1:_ -> #d1:_ -> #l1:_ -> + #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> + #i2:_ -> #d2:_ -> #l2:_ -> #b2:bool -> + //the first component is a pre-denoted type with a reader + t1:dtyp pk1 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) -> + typ (P.and_then_kind pk1 pk2) + (join_inv i1 i2) + (join_disj d1 d2) + (join_loc l1 l2) + false + + | T_refine: + fieldname:string -> + #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> + #i1:_ -> #d1:_ -> #l1:_ -> + //the first component is a pre-denoted type with a reader + base:dtyp pk1 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 + + | T_refine_with_action: + fieldname:string -> + #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> + #i1:_ -> #d1:_ -> #l1:_ -> + #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> + base:dtyp pk1 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) + false + + | T_dep_pair_with_refinement: + //This construct serves two purposes + // 1. To avoid double fetches, we fold the refinement + // and dependent pair into a single form + // 2. This allows the well-typedness of the continuation k + // to depend on the refinement of the first field + first_fieldname:string -> + #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> + #i1:_ -> #d1:_ -> #l1:_ -> + #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> + #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> + //the first component is a pre-denoted type with a reader + base:dtyp pk1 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) -> + typ (P.and_then_kind (P.filter_kind pk1) pk2) + (join_inv i1 i2) + (join_disj d1 d2) + (join_loc l1 l2) + false + + | T_dep_pair_with_action: + fieldname:string -> + #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> + #i1:_ -> #d1:_ -> #l1:_ -> + #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> + #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> + #i3:_ -> #d3:_ -> #l3:_ -> #b3:_ -> + base:dtyp pk1 true i1 d1 l1 -> + k:(x:dtyp_as_type base -> typ pk2 i2 d2 l2 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)) + false + + | T_dep_pair_with_refinement_and_action: + //This construct serves two purposes + // 1. To avoid double fetches, we fold the refinement + // and dependent pair and action into a single form + // 2. This allows the well-typedness of the continuation k + // to depend on the refinement of the first field + first_fieldname:string -> + #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> + #i1:_ -> #d1:_ -> #l1:_ -> + #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> + #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> + #i3:_ -> #d3:_ -> #l3:_ -> #b3:_ -> + //the first component is a pre-denoted type with a reader + base:dtyp pk1 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) -> + 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)) + false + + | T_if_else: + #nz1:_ -> #wk1:_ -> #pk1:P.parser_kind nz1 wk1 -> + #l1:_ -> #i1:_ -> #d1:_ -> #b1:_ -> + #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> + #l2:_ -> #i2:_ -> #d2:_ -> #b2:_ -> + 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) -> + typ (P.glb pk1 pk2) + (join_inv i1 i2) + (join_disj d1 d2) + (join_loc l1 l2) false + + | T_cases: + #nz1:_ -> #wk1:_ -> #pk1:P.parser_kind nz1 wk1 -> + #l1:_ -> #i1:_ -> #d1:_ -> #b1:_ -> + #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> + #l2:_ -> #i2:_ -> #d2:_ -> #b2:_ -> + b:bool -> //A bool, rather than an expression + t1:typ pk1 i1 d1 l1 b1 -> + t2:typ pk2 i2 d2 l2 b2 -> + typ (P.glb pk1 pk2) + (join_inv i1 i2) + (join_disj d1 d2) + (join_loc l1 l2) + false + + | T_with_action: + fieldname:string -> + #nz:_ -> #wk:_ -> #pk:P.parser_kind nz wk -> + #l1:_ -> #i1:_ -> #d1:_ -> #b1:_ -> + #l2:_ -> #i2:_ -> #d2:_ -> #b2:_ -> + base:typ pk i1 d1 l1 b1 -> + act:action i2 d2 l2 b2 bool -> + typ pk (join_inv i1 i2) (join_disj d1 d2) (join_loc l1 l2) false + + | T_with_dep_action: + fieldname:string -> + #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> + #i1:_ -> #d1: _ -> #l1:_ -> + #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> + head:dtyp pk1 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 + + | T_with_comment: + fieldname:string -> + #nz:_ -> #wk:_ -> #pk:P.parser_kind nz wk -> + #l:_ -> #i:_ -> #d:_ -> #b:_ -> + t:typ pk i d l b -> + c:comments -> + typ pk i d l b + + | T_nlist: + fieldname:string -> + #pk:P.parser_kind true P.WeakKindStrongPrefix -> + #i:_ -> #l:_ -> #d:_ -> #b:_ -> + n:U32.t -> + t:typ pk i d l b -> + typ P.kind_nlist i d l false + + | T_at_most: + fieldname:string -> + #nz:_ -> #pk:P.parser_kind nz P.WeakKindStrongPrefix -> + #i:_ -> #d:_ -> #l:_ -> #b:_ -> + n:U32.t -> + t:typ pk i d l b -> + typ P.kind_t_at_most i d l false + + | T_exact: + fieldname:string -> + #nz:_ -> #pk:P.parser_kind nz P.WeakKindStrongPrefix -> + #i:_ -> #d:_ -> #l:_ -> #b:_ -> + n:U32.t -> + t:typ pk i d l b -> + typ P.kind_t_exact i d l false + + | T_string: + fieldname:string -> + #pk1:P.parser_kind true P.WeakKindStrongPrefix -> + element_type:dtyp pk1 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 + + +[@@specialize] +inline_for_extraction +let coerce (#[@@@erasable]a:Type) + (#[@@@erasable]b:Type) + ( [@@@erasable]pf:squash (a == b)) + (x:a) + : b + = x + +[@@specialize] +val t_probe_then_validate + (fieldname:string) + (probe:CP.probe_fn) + (len:U64.t) + (dest:CP.copy_buffer_t) + (#nz #wk:_) (#pk:P.parser_kind nz wk) + (#has_reader #i #disj:_) + (#l:_) + (td:dtyp pk 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))) + false + +(* Type denotation of `typ` *) +val as_type + #nz #wk (#pk:P.parser_kind nz wk) + #l #i #d #b + (t:typ pk l i d b) + : Tot Type0 + +(* Parser denotation of `typ` *) +val as_parser + #nz #wk (#pk:P.parser_kind nz wk) + #l #i #d #b + (t:typ pk l i d b) + : P.parser pk (as_type t) + +(* Serializer denotation of `typ` *) +val as_serializer + #nz #wk (#pk:P.parser_kind nz wk) + #l #i #d #b + (t:typ pk l i d b) + : Tot (P.serializer (as_parser t)) + +[@@specialize] +val as_reader #nz (#pk:P.parser_kind nz P.WeakKindStrongPrefix) + (#[@@@erasable] inv:inv_index) + (#[@@@erasable] d:disj_index) + (#[@@@erasable] loc:loc_index) + (t:typ pk inv d loc true) + : leaf_reader (as_parser t) + +(* The main result: + A validator denotation of `typ` + related by construction to the parser + and type denotations +*) +inline_for_extraction noextract +val as_validator + (typename:string) + #nz #wk (#pk:P.parser_kind nz wk) + (#[@@@erasable] inv:inv_index) + (#[@@@erasable] disj:disj_index) + (#[@@@erasable] loc:loc_index) + #b + (t:typ pk inv disj loc 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) + +[@@noextract_to "krml"; specialize] +inline_for_extraction noextract +let validator_of #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) = + A.validate_with_action_t + (as_parser t) + (interp_inv i) + (interp_disj d) + (interp_loc l) + allow_reading + +[@@noextract_to "krml"; specialize] +inline_for_extraction noextract +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 + +let specialization_steps = + [nbe; + zeta; + primops; + iota; + delta_attr [`%specialize]; + delta_only ([`%Some?; + `%Some?.v; + `%as_validator; + `%nz_of_binding; + `%wk_of_binding; + `%pk_of_binding; + `%inv_of_binding; + `%loc_of_binding; + `%type_of_binding; + `%parser_of_binding; + `%validator_of_binding; + `%leaf_reader_of_binding; + `%fst; + `%snd; + `%Mktuple2?._1; + `%Mktuple2?._2]@projector_names)] + +let specialize_tac steps (_:unit) + : T.Tac unit + = let open FStar.List.Tot in + T.norm (steps@specialization_steps); + T.trefl() + +[@@specialize] +let mk_global_binding #nz #wk + (pk:P.parser_kind nz wk) + ([@@@erasable] inv:inv_index) + ([@@@erasable] disj:disj_index) + ([@@@erasable] loc:loc_index) + ([@@@erasable] p_t : Type0) + ([@@@erasable] p_p : P.parser pk p_t) + ((*[@@@erasable]*) p_s : P.serializer p_p) + (p_reader: option (leaf_reader p_p)) + (b:bool) + (p_v : A.validate_with_action_t p_p + (interp_inv inv) + (interp_disj disj) + (interp_loc loc) b) + ([@@@erasable] pf:squash (b == Some? p_reader)) + : global_binding + = { + parser_kind_nz = nz; + parser_weak_kind = wk; + parser_kind = pk; + inv = inv; + disj; + loc = loc; + p_t = p_t; + p_p = p_p; + p_s = p_s; + p_reader = p_reader; + p_v = p_v + } + +[@@specialize] +let mk_dt_app #nz #wk (pk:P.parser_kind nz wk) (b:bool) + ([@@@erasable] inv:inv_index) + ([@@@erasable] disj:disj_index) + ([@@@erasable] loc:loc_index) + (x:global_binding) + ([@@@erasable] pf:squash (nz == nz_of_binding x /\ + wk == wk_of_binding x /\ + pk == pk_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 + + +[@@specialize] +let mk_dtyp_app #nz #wk + (pk:P.parser_kind nz wk) + ([@@@erasable] inv:inv_index) + ([@@@erasable] disj:disj_index) + ([@@@erasable] loc:loc_index) + ([@@@erasable] p_t : Type0) + ([@@@erasable] p_p : P.parser pk p_t) + ((*[@@@erasable]*) p_s : P.serializer p_p) + (p_reader: option (leaf_reader p_p)) + (b:bool) + (p_v : A.validate_with_action_t p_p + (interp_inv inv) + (interp_disj disj) + (interp_loc loc) + b) + ([@@@erasable] pf:squash (b == Some? p_reader)) + : dtyp #nz #wk pk b inv disj loc + = let gb = { + parser_kind_nz = nz; + parser_weak_kind = wk; + parser_kind = pk; + inv = inv; + disj; + loc = loc; + p_t = p_t; + p_p = p_p; + p_s = p_s; + p_reader = p_reader; + p_v = p_v + } in + DT_App pk b inv disj loc gb () + +//attribute to tag disjointness indexes of type definitions +let specialize_disjointness = () +let coerce_validator steps : T.Tac unit = + let open FStar.List.Tot in + T.norm [delta_only (steps @ [`%parser_kind_of_itype; + `%parser_kind_nz_of_itype; + `%fst; + `%snd; + `%Mktuple2?._1; + `%Mktuple2?._2; + `%coerce; + `%validator_of; + `%dtyp_of; + `%join_disj; + ]); + delta_attr [`%specialize_disjointness]; + zeta; + iota; + primops]; + T.trefl() + + +let coerce_dt_app (steps:_) : T.Tac unit = + let open FStar.List.Tot in + T.norm [delta_only (steps@[`%nz_of_binding; + `%wk_of_binding; + `%pk_of_binding; + `%has_reader; + `%leaf_reader_of_binding; + `%inv_of_binding; + `%loc_of_binding; + `%mk_global_binding]@projector_names); + zeta; + iota; + simplify]; + T.trivial()