Skip to content

Commit

Permalink
impl_zero_copy_wf_array_group
Browse files Browse the repository at this point in the history
  • Loading branch information
tahina-pro committed Jan 31, 2025
1 parent fa30297 commit e5f644a
Show file tree
Hide file tree
Showing 6 changed files with 191 additions and 14 deletions.
4 changes: 4 additions & 0 deletions src/cddl/pulse/CDDL.Pulse.AST.Base.fst
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,11 @@ type cbor_impl
cbor_det_parse: cbor_det_parse_t vmatch; // TODO: support mixtures where non-deterministic CBOR objects contain .det-cbor deterministically serialized CBOR objects
cbor_array_iterator_init: array_iterator_start_t vmatch cbor_array_iterator_match;
cbor_array_iterator_is_done: array_iterator_is_empty_t cbor_array_iterator_match;
cbor_array_iterator_length: array_iterator_length_t cbor_array_iterator_match;
cbor_array_iterator_next: array_iterator_next_t vmatch cbor_array_iterator_match;
cbor_array_iterator_truncate: array_iterator_truncate_t cbor_array_iterator_match;
cbor_array_iterator_share: array_iterator_share_t cbor_array_iterator_match;
cbor_array_iterator_gather: array_iterator_gather_t cbor_array_iterator_match;
cbor_get_map_length: get_map_length_t vmatch;
cbor_map_get: map_get_t vmatch;
cbor_mk_int64: mk_int64_t vmatch;
Expand Down
4 changes: 4 additions & 0 deletions src/cddl/pulse/CDDL.Pulse.AST.Det.C.fst
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,11 @@ let cbor_det_impl : cbor_impl cbor_det_match cbor_det_map_entry_match cbor_det_a
cbor_det_parse = cbor_det_parse_full (); // TODO: support mixtures where non-deterministic CBOR objects contain .det-cbor deterministically serialized CBOR objects
cbor_array_iterator_init = cbor_det_array_iterator_start ();
cbor_array_iterator_is_done = cbor_det_array_iterator_is_empty ();
cbor_array_iterator_length = cbor_det_array_iterator_length ();
cbor_array_iterator_next = cbor_det_array_iterator_next ();
cbor_array_iterator_truncate = cbor_det_array_iterator_truncate ();
cbor_array_iterator_share = cbor_det_array_iterator_share ();
cbor_array_iterator_gather = cbor_det_array_iterator_gather ();
cbor_get_map_length = cbor_det_get_map_length ();
cbor_map_get = cbor_det_map_get_gen ();
cbor_mk_int64 = cbor_det_mk_int64 ();
Expand Down
143 changes: 135 additions & 8 deletions src/cddl/pulse/CDDL.Pulse.AST.Parse.fst
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
module CDDL.Pulse.AST.Parse
include CDDL.Pulse.AST.Base
include CDDL.Pulse.AST.Parse.ElemType
include CDDL.Pulse.Parse.ArrayGroup
include CDDL.Pulse.AST.Types
open Pulse.Lib.Pervasives
module Cbor = CBOR.Spec.API.Format
Expand Down Expand Up @@ -54,14 +55,66 @@ let ancillary_parse_env_extend
end
else None

[@@sem_attr]
let ancillary_parse_array_group_env
(#cbor_t: Type)
(vmatch: perm -> cbor_t -> Cbor.cbor -> slprop)
(#cbor_array_iterator_t: Type0)
(cbor_array_iterator_match: perm -> cbor_array_iterator_t -> list Cbor.cbor -> slprop)
(#se: sem_env)
(#s_env: target_type_env se.se_bound)
(r_env: rel_env s_env)
(sp_env: spec_env se s_env.te_type)
= (t: group) -> (t_wf: ast0_wf_array_group t { spec_wf_array_group se t t_wf }) -> option (impl_array_group cbor_array_iterator_match (array_group_sem se t) & impl_zero_copy_array_group cbor_array_iterator_match (spec_of_wf_array_group sp_env t_wf).ag_parser (impl_type_sem vmatch cbor_array_iterator_match r_env (target_type_of_wf_array_group t_wf)).sem_rel)

[@@sem_attr]
let ancillary_parse_array_group_env_extend
(#cbor_t: Type)
(#vmatch: perm -> cbor_t -> Cbor.cbor -> slprop)
(#cbor_array_iterator_t: Type0)
(#cbor_array_iterator_match: perm -> cbor_array_iterator_t -> list Cbor.cbor -> slprop)
(#se: sem_env)
(#s_env: target_type_env se.se_bound)
(#r_env: rel_env s_env)
(#sp_env: spec_env se s_env.te_type)
(env1: ancillary_parse_array_group_env vmatch cbor_array_iterator_match r_env sp_env)
(#se2: sem_env)
(#s_env2: target_type_env se2.se_bound)
(r_env2: rel_env s_env2 {
rel_env_included r_env r_env2
})
(sp_env2: spec_env se2 s_env2.te_type {
spec_env_included sp_env sp_env2
})
: Tot (ancillary_parse_array_group_env vmatch cbor_array_iterator_match r_env2 sp_env2)
= fun t t_wf ->
if bounded_wf_array_group se.se_bound t t_wf
then begin
(env1 t t_wf)
end
else None

module U64 = FStar.UInt64
module U8 = FStar.UInt8
module I64 = FStar.Int64
module V = CDDL.Pulse.AST.Validate
module SZ = FStar.SizeT

noeq
type ask_for =
| AskForType: t: typ -> ast0_wf_typ t -> ask_for
| AskForArrayGroup: t: group -> ast0_wf_array_group t -> ask_for

let ask_for_spec
(se: sem_env)
(a: ask_for)
: Tot prop
= match a with
| AskForType t t_wf -> spec_wf_typ se true t t_wf
| AskForArrayGroup t t_wf -> spec_wf_array_group se t t_wf

[@@sem_attr]
let rec impl_zero_copy_type
let rec impl_zero_copy_wf_type
(#cbor_t #t2 #t_arr #t_map: Type0)
(#vmatch: (perm -> cbor_t -> Cbor.cbor -> slprop))
(#vmatch2: (perm -> t2 -> (Cbor.cbor & Cbor.cbor) -> slprop))
Expand All @@ -75,22 +128,23 @@ let rec impl_zero_copy_type
(sp_env: spec_env se s_env.te_type)
(p_env: parse_env vmatch r_env sp_env)
(ancillary: ancillary_parse_env vmatch cbor_array_iterator_match r_env sp_env)
(ancillary_ag: ancillary_parse_array_group_env vmatch cbor_array_iterator_match r_env sp_env)
(#t: typ)
(t_wf: ast0_wf_typ t {
spec_wf_typ se true t t_wf /\ SZ.fits_u64
})
: Pure (either (impl_zero_copy_parse vmatch (spec_of_wf_typ sp_env t_wf).parser (impl_type_sem vmatch cbor_array_iterator_match r_env (target_type_of_wf_typ t_wf)).sem_rel) (t': typ & ast0_wf_typ t'))
: Pure (either (impl_zero_copy_parse vmatch (spec_of_wf_typ sp_env t_wf).parser (impl_type_sem vmatch cbor_array_iterator_match r_env (target_type_of_wf_typ t_wf)).sem_rel) (ask_for))
(requires True)
(ensures (fun res -> match res with
| Inl _ -> True
| Inr (| t', t_wf' |) -> spec_wf_typ se true t' t_wf'
| Inr a -> ask_for_spec se a
))
(decreases t_wf)
= match t_wf with
| WfTRewrite _ _ s ->
impl_zero_copy_type impl v_env r_env sp_env p_env ancillary s
impl_zero_copy_wf_type impl v_env r_env sp_env p_env ancillary ancillary_ag s
| WfTTagged tg _ s ->
begin match impl_zero_copy_type impl v_env r_env sp_env p_env ancillary s with
begin match impl_zero_copy_wf_type impl v_env r_env sp_env p_env ancillary ancillary_ag s with
| Inr ask -> Inr ask
| Inl p ->
begin match tg with
Expand All @@ -99,17 +153,17 @@ let rec impl_zero_copy_type
end
end
| WfTChoice _ _ s1 s2 ->
begin match impl_zero_copy_type impl v_env r_env sp_env p_env ancillary s1 with
begin match impl_zero_copy_wf_type impl v_env r_env sp_env p_env ancillary ancillary_ag s1 with
| Inr ask -> Inr ask
| Inl p1 ->
begin match impl_zero_copy_type impl v_env r_env sp_env p_env ancillary s2 with
begin match impl_zero_copy_wf_type impl v_env r_env sp_env p_env ancillary ancillary_ag s2 with
| Inr ask -> Inr ask
| Inl p2 -> Inl (impl_zero_copy_choice (V.validate_typ impl v_env true _ s1) p1 p2)
end
end
| WfTElem e -> Inl (impl_zero_copy_elem_type vmatch impl.cbor_get_major_type impl.cbor_destr_int64 impl.cbor_get_string impl.cbor_destr_simple e)
| WfTDetCbor _ _ s ->
begin match impl_zero_copy_type impl v_env r_env sp_env p_env ancillary s with
begin match impl_zero_copy_wf_type impl v_env r_env sp_env p_env ancillary ancillary_ag s with
| Inr ask -> Inr ask
| Inl p ->
Inl (impl_zero_copy_det_cbor impl.cbor_get_string impl.cbor_det_parse _ p)
Expand All @@ -125,3 +179,76 @@ let rec impl_zero_copy_type
| WfTDef n -> Inl (p_env n)
| WfTArray _ _ -> admit ()
| WfTMap _ _ _ -> admit ()

[@@sem_attr]
let rec impl_zero_copy_wf_array_group
(#cbor_t #t2 #t_arr #t_map: Type0)
(#vmatch: (perm -> cbor_t -> Cbor.cbor -> slprop))
(#vmatch2: (perm -> t2 -> (Cbor.cbor & Cbor.cbor) -> slprop))
(#cbor_array_iterator_match: (perm -> t_arr -> list Cbor.cbor -> slprop))
(#cbor_map_iterator_match: (perm -> t_map -> list (Cbor.cbor & Cbor.cbor) -> slprop))
(impl: cbor_impl vmatch vmatch2 cbor_array_iterator_match cbor_map_iterator_match)
(#se: sem_env)
(v_env: V.validator_env vmatch se)
(#s_env: target_type_env se.se_bound)
(r_env: rel_env s_env)
(sp_env: spec_env se s_env.te_type)
(p_env: parse_env vmatch r_env sp_env)
(ancillary: ancillary_parse_env vmatch cbor_array_iterator_match r_env sp_env)
(ancillary_ag: ancillary_parse_array_group_env vmatch cbor_array_iterator_match r_env sp_env)
(#t: group)
(t_wf: ast0_wf_array_group t {
spec_wf_array_group se t t_wf /\ SZ.fits_u64
})
: Pure (either (impl_zero_copy_array_group cbor_array_iterator_match (spec_of_wf_array_group sp_env t_wf).ag_parser (impl_type_sem vmatch cbor_array_iterator_match r_env (target_type_of_wf_array_group t_wf)).sem_rel) (ask_for))
(requires True)
(ensures (fun res -> match res with
| Inl _ -> True
| Inr a -> ask_for_spec se a
))
(decreases t_wf)
= match t_wf with
| WfAElem _ _ _ t_wf' ->
begin match impl_zero_copy_wf_type impl v_env r_env sp_env p_env ancillary ancillary_ag t_wf' with
| Inl pt ->
Inl (impl_zero_copy_array_group_item impl.cbor_array_iterator_next pt)
| Inr ask -> Inr ask
end
| WfAZeroOrOne _ t_wf' ->
begin match impl_zero_copy_wf_array_group impl v_env r_env sp_env p_env ancillary ancillary_ag t_wf' with
| Inr ask -> Inr ask
| Inl pe ->
Inl (impl_zero_copy_array_group_zero_or_one pe (V.validate_array_group impl v_env _ t_wf'))
end
| WfAZeroOrOneOrMore _ t_wf' g' ->
// HERE I need function pointers, so I MUST NOT do a recursive call
begin match ancillary_ag _ t_wf' with
| None -> Inr (AskForArrayGroup _ t_wf')
| Some (ve, pe) ->
begin match g' with
| GZeroOrMore _ ->
Inl (impl_zero_copy_array_group_zero_or_more impl.cbor_array_iterator_share impl.cbor_array_iterator_gather ve pe ())
| _ ->
Inl (impl_zero_copy_array_group_one_or_more impl.cbor_array_iterator_share impl.cbor_array_iterator_gather ve pe ())
end
end
| WfAConcat _ _ t_wf1 t_wf2 ->
begin match impl_zero_copy_wf_array_group impl v_env r_env sp_env p_env ancillary ancillary_ag t_wf1 with
| Inr ask -> Inr ask
| Inl pg1 ->
begin match impl_zero_copy_wf_array_group impl v_env r_env sp_env p_env ancillary ancillary_ag t_wf2 with
| Inr ask -> Inr ask
| Inl pg2 -> Inl (impl_zero_copy_array_group_concat impl.cbor_array_iterator_length impl.cbor_array_iterator_share impl.cbor_array_iterator_gather impl.cbor_array_iterator_truncate pg1 (V.validate_array_group impl v_env _ t_wf1) pg2 ())
end
end
| WfAChoice _ _ t_wf1 t_wf2 ->
begin match impl_zero_copy_wf_array_group impl v_env r_env sp_env p_env ancillary ancillary_ag t_wf1 with
| Inr ask -> Inr ask
| Inl pg1 ->
begin match impl_zero_copy_wf_array_group impl v_env r_env sp_env p_env ancillary ancillary_ag t_wf2 with
| Inr ask -> Inr ask
| Inl pg2 -> Inl (impl_zero_copy_array_group_choice pg1 (V.validate_array_group impl v_env _ t_wf1) pg2)
end
end
| WfARewrite _ _ t_wf2 ->
impl_zero_copy_wf_array_group impl v_env r_env sp_env p_env ancillary ancillary_ag t_wf2
8 changes: 4 additions & 4 deletions src/cddl/pulse/CDDL.Pulse.AST.Types.fst
Original file line number Diff line number Diff line change
Expand Up @@ -97,20 +97,20 @@ let rec impl_type_sem
let it = impl_type_sem vmatch cbor_array_iterator_match env t in {
sem_impl_type =
either
(slice it.sem_impl_type)
(vec_or_slice it.sem_impl_type)
(array_iterator_t cbor_array_iterator_match it.sem_impl_type (Iterator.mk_spec it.sem_rel)) // HERE the relation on the element types is used in the implementation array type
;
sem_rel =
rel_either_left
(rel_slice_of_list it.sem_rel false)
(rel_vec_or_slice_of_list it.sem_rel false)
(rel_array_iterator cbor_array_iterator_match (Iterator.mk_spec it.sem_rel))
;
}
| TTTable t1 t2 ->
let it1 = impl_type_sem vmatch cbor_array_iterator_match env t1 in
let it2 = impl_type_sem vmatch cbor_array_iterator_match env t2 in {
sem_impl_type = slice (it1.sem_impl_type & it2.sem_impl_type); // HERE we will plug support for iterable CBOR maps whose elements will be parsed wrt. it1.sem_rel, it2.sem_rel
sem_rel = rel_slice_of_table (target_type_eq s_env t1) it1.sem_rel it2.sem_rel
sem_impl_type = vec_or_slice (it1.sem_impl_type & it2.sem_impl_type); // HERE we will plug support for iterable CBOR maps whose elements will be parsed wrt. it1.sem_rel, it2.sem_rel
sem_rel = rel_vec_or_slice_of_table (target_type_eq s_env t1) it1.sem_rel it2.sem_rel false
}

let rel_env_included
Expand Down
42 changes: 40 additions & 2 deletions src/cddl/pulse/CDDL.Pulse.Parse.ArrayGroup.fst
Original file line number Diff line number Diff line change
Expand Up @@ -694,7 +694,7 @@ fn cddl_array_iterator_next

inline_for_extraction noextract [@@noextract_to "krml"]
```pulse
fn impl_zero_copy_array_group_zero_or_more
fn impl_zero_copy_array_group_zero_or_more'
(#cbor_array_iterator_t: Type)
(#cbor_array_iterator_match: perm -> cbor_array_iterator_t -> list cbor -> slprop)
(share: array_iterator_share_t cbor_array_iterator_match)
Expand Down Expand Up @@ -745,6 +745,44 @@ fn impl_zero_copy_array_group_zero_or_more
}
```

inline_for_extraction noextract [@@noextract_to "krml"]
```pulse
fn impl_zero_copy_array_group_zero_or_more
(#cbor_array_iterator_t: Type)
(#cbor_array_iterator_match: perm -> cbor_array_iterator_t -> list cbor -> slprop)
(share: array_iterator_share_t cbor_array_iterator_match)
(gather: array_iterator_gather_t cbor_array_iterator_match)
(#t1: Ghost.erased (array_group None))
(#tgt1: Type0)
(#tgt_size1: Ghost.erased (tgt1 -> nat))
(#tgt_serializable1: Ghost.erased (tgt1 -> bool))
(#ps1: Ghost.erased (array_group_parser_spec t1 tgt_size1 tgt_serializable1))
(#impl_tgt1: Type0)
(#r1: rel impl_tgt1 tgt1)
(va1: impl_array_group cbor_array_iterator_match (Ghost.reveal t1)) // MUST be a function pointer
(pa1: impl_zero_copy_array_group cbor_array_iterator_match ps1 r1) // MUST be a function pointer
(sq: squash (
array_group_concat_unique_strong t1 t1
))
: impl_zero_copy_array_group #cbor_array_iterator_t cbor_array_iterator_match #(array_group_zero_or_more (Ghost.reveal t1)) #(list tgt1) #(ag_spec_zero_or_more_size (Ghost.reveal tgt_size1)) #(ag_spec_zero_or_more_serializable (Ghost.reveal tgt_serializable1))
(array_group_parser_spec_zero_or_more0 (Ghost.reveal ps1) ())
#(either (vec_or_slice impl_tgt1) (array_iterator_t cbor_array_iterator_match impl_tgt1 (Iterator.mk_spec r1))) (rel_either_left (rel_vec_or_slice_of_list r1 false) (rel_array_iterator cbor_array_iterator_match (Iterator.mk_spec r1)))
=
(c: _)
(#p: _)
(#l: _)
{
let i = impl_zero_copy_array_group_zero_or_more' share gather va1 pa1 sq c;
with v . assert (rel_array_iterator cbor_array_iterator_match (Iterator.mk_spec r1) i v);
let res : either (vec_or_slice impl_tgt1) (array_iterator_t cbor_array_iterator_match impl_tgt1 (Iterator.mk_spec r1)) = Inr i;
Trade.rewrite_with_trade
(rel_array_iterator cbor_array_iterator_match (Iterator.mk_spec r1) i v)
(rel_either_left (rel_vec_or_slice_of_list r1 false) (rel_array_iterator cbor_array_iterator_match (Iterator.mk_spec r1)) res v);
Trade.trans _ _ (cbor_array_iterator_match p c l);
res
}
```

inline_for_extraction noextract [@@noextract_to "krml"]
let impl_zero_copy_array_group_one_or_more
(#cbor_array_iterator_t: Type)
Expand All @@ -765,7 +803,7 @@ let impl_zero_copy_array_group_one_or_more
array_group_is_nonempty t1
))
: impl_zero_copy_array_group cbor_array_iterator_match (array_group_parser_spec_one_or_more0 (Ghost.reveal ps1) ())
(rel_array_iterator cbor_array_iterator_match (Iterator.mk_spec r1))
(rel_either_left (rel_vec_or_slice_of_list r1 false) (rel_array_iterator cbor_array_iterator_match (Iterator.mk_spec r1)))
= impl_zero_copy_array_group_ext
(impl_zero_copy_array_group_zero_or_more share gather va1 pa1 ())
_
Expand Down
4 changes: 4 additions & 0 deletions src/cddl/spec/CDDL.Spec.AST.Base.fst
Original file line number Diff line number Diff line change
Expand Up @@ -3003,6 +3003,10 @@ and spec_of_wf_array_group_incr
spec_of_wf_array_group env wf == spec_of_wf_array_group env' wf
))
(decreases wf)
[SMTPatOr [
[SMTPat (spec_env_included env env'); SMTPat (spec_of_wf_array_group env wf)];
[SMTPat (spec_env_included env env'); SMTPat (spec_of_wf_array_group env' wf)];
]]
= match wf with
| WfAElem _ _ _ s ->
spec_of_wf_typ_incr env env' s
Expand Down

0 comments on commit e5f644a

Please sign in to comment.