impl_zero_copy_bytes_gen, det_cbor

src/cddl/pulse/CDDL.Pulse.Parse.Misc.fst

@@ -165,6 +165,73 @@ let impl_copyful_str_size
 : impl_copyful_parse vmatch (spec_str_size mt lo hi).parser (rel_vec_or_slice_of_seq true)
 = impl_copyful_bytes_gen cbor_destr_string _ ()
 
+inline_for_extraction noextract [@@noextract_to "krml"]
+```pulse
+fn impl_zero_copy_bytes_gen
+    (#ty: Type u#0)
+    (#vmatch: perm -> ty -> cbor -> slprop)
+    (cbor_destr_string: get_string_t vmatch)
+    (#t: Ghost.erased typ)
+    (#ser: Ghost.erased (Seq.seq U8.t -> bool))
+    (par: Ghost.erased (parser_spec t (Seq.seq U8.t) ser))
+    (sq: squash (
+      forall (x: cbor) . Ghost.reveal t x ==> (CString? (unpack x) /\ (Ghost.reveal par x <: Seq.seq U8.t) == CString?.v (unpack x))
+    ))
+: impl_zero_copy_parse #ty vmatch #(Ghost.reveal t) #(Seq.seq U8.t) #(Ghost.reveal ser) (Ghost.reveal par) #_ (rel_vec_or_slice_of_seq false)
+=
+    (c: ty)
+    (#p: perm)
+    (#v: Ghost.erased cbor)
+{
+  let s = cbor_destr_string c;
+  with ps vs . assert (pts_to s #ps vs);
+  let w : slice U8.t = {
+    p = ps;
+    s = s;
+  };
+  fold (rel_slice_of_seq false w vs);
+  let res : vec_or_slice U8.t = Slice w;
+  fold (rel_vec_or_slice_of_seq false res vs);
+  ghost fn aux (_: unit)
+  requires
+    (Trade.trade (pts_to s #ps vs) (vmatch p c v) ** rel_vec_or_slice_of_seq false res vs)
+  ensures vmatch p c v
+  {
+    unfold (rel_vec_or_slice_of_seq false res vs);
+    unfold (rel_slice_of_seq false w vs);
+    Trade.elim _ _
+  };
+  Trade.intro_trade _ _ _ aux;
+  res
+}
+```
+
+inline_for_extraction noextract [@@noextract_to "krml"]
+let impl_zero_copy_bytes
+    (#ty: Type u#0)
+    (#vmatch: perm -> ty -> cbor -> slprop)
+    (cbor_destr_string: get_string_t vmatch)
+: impl_zero_copy_parse #ty vmatch #bstr #(Seq.seq U8.t) #_ spec_bstr.parser #_ (rel_vec_or_slice_of_seq false )
+= impl_zero_copy_bytes_gen cbor_destr_string _ ()
+
+inline_for_extraction noextract [@@noextract_to "krml"]
+let impl_zero_copy_text
+    (#ty: Type u#0)
+    (#vmatch: perm -> ty -> cbor -> slprop)
+    (cbor_destr_string: get_string_t vmatch)
+: impl_zero_copy_parse #ty vmatch #tstr #(Seq.seq U8.t) #_ spec_tstr.parser #_ (rel_vec_or_slice_of_seq false )
+= impl_zero_copy_bytes_gen cbor_destr_string _ ()
+
+inline_for_extraction noextract [@@noextract_to "krml"]
+let impl_zero_copy_str_size
+    (#ty: Type u#0)
+    (#vmatch: perm -> ty -> cbor -> slprop)
+    (cbor_destr_string: get_string_t vmatch)
+    (mt: Ghost.erased major_type_byte_string_or_text_string)
+    (lo hi: Ghost.erased U64.t)
+: impl_zero_copy_parse vmatch (spec_str_size mt lo hi).parser (rel_vec_or_slice_of_seq false)
+= impl_zero_copy_bytes_gen cbor_destr_string _ ()
+
 inline_for_extraction noextract [@@noextract_to "krml"]
 ```pulse
 fn impl_copyful_simple
@@ -302,3 +369,46 @@ fn impl_copyful_det_cbor
   }
 }
 ```
+
+inline_for_extraction noextract [@@noextract_to "krml"]
+```pulse
+fn impl_zero_copy_det_cbor
+    (#ty: Type u#0)
+    (#vmatch: perm -> ty -> cbor -> slprop)
+    (#ty': Type0)
+    (#vmatch': perm -> ty -> cbor -> slprop)
+    (cbor_destr_string: get_string_t vmatch)
+    (cbor_det_parse: cbor_det_parse_t vmatch')
+    (#t: Ghost.erased typ)
+    (#tgt: Type0)
+    (sp: Ghost.erased (spec t tgt true))
+    (#implt: Type0)
+    (#r: rel implt tgt)
+    (ipl: impl_zero_copy_parse vmatch' (Ghost.reveal sp).parser r)
+: impl_zero_copy_parse #ty vmatch #(bstr_cbor_det (Ghost.reveal t)) #tgt #(spec_bstr_cbor_det (Ghost.reveal sp)).serializable (spec_bstr_cbor_det (Ghost.reveal sp)).parser #implt r
+=
+    (c: ty)
+    (#p: perm)
+    (#v: Ghost.erased cbor)
+{
+  let cs = cbor_destr_string c;
+  with ps s . assert (pts_to cs #ps s);
+  Seq.slice_length s;
+  let cp = cbor_det_parse cs;
+  match cp {
+    Some cp_ -> {
+      let cp = fst cp_;
+      let rem = Ghost.hide (snd cp_);
+      unfold (cbor_det_parse_post vmatch' cs ps s (Some (cp, Ghost.reveal rem)));
+      unfold (cbor_det_parse_post_some vmatch' cs ps s cp rem);
+      with ps vs . assert (vmatch' ps cp vs);
+      Trade.elim_hyp_r (vmatch' ps cp vs) _ _;
+      Trade.trans _ _ (vmatch p c v);
+      CBOR.Spec.API.Format.cbor_det_serialize_parse' vs (Seq.slice s (Seq.length (CBOR.Spec.API.Format.cbor_det_serialize vs)) (Seq.length s));
+      let res = ipl cp;
+      Trade.trans _ _ (vmatch p c v);
+      res
+    }
+  }
+}
+```

src/cddl/pulse/CDDL.Pulse.Types.fst

@@ -48,13 +48,19 @@ let rel_pure
 
 let rel_unit : rel unit unit = mk_rel (fun _ _ -> emp)
 
+noeq
+type slice (t: Type) = {
+  s: S.slice t;
+  p: perm;
+}
+
 let rel_slice_of_list
   (#low #high: Type)
   (r: rel low high)
   (freeable: bool)
-: rel (S.slice low) (list high)
+: rel (slice low) (list high)
 = mk_rel (fun x y ->
-    exists* s . pts_to x s ** seq_list_match s y r ** pure (freeable == false)
+    exists* s . pts_to x.s #x.p s ** seq_list_match s y r ** pure (freeable == false)
   )
 
 module U64 = FStar.UInt64
@@ -77,7 +83,7 @@ let rel_vec_of_list
 noeq
 type vec_or_slice (t: Type) =
 | Vec of vec t
-| Slice of S.slice t
+| Slice of slice t
 
 let rel_vec_or_slice_of_list
   (#low #high: Type)
@@ -196,8 +202,8 @@ let rel_bij_r
 let rel_slice_of_seq
   (#t: Type)
   (freeable: bool)
-: rel (S.slice t) (Seq.seq t)
-= mk_rel (fun x y -> pts_to x y ** pure (freeable == false))
+: rel (slice t) (Seq.seq t)
+= mk_rel (fun x y -> pts_to x.s #x.p y ** pure (freeable == false))
 
 let rel_vec_of_seq
   (#t: Type)