WIP CDDL impl

src/cbor/CBOR.SteelST.Array.fst

@@ -0,0 +1,158 @@
+module CBOR.SteelST.Array
+include CBOR.SteelST.Base
+open CBOR.SteelST.Validate
+open LowParse.SteelST.Combinators
+open LowParse.SteelST.Recursive
+open LowParse.SteelST.BitSum
+open LowParse.SteelST.ValidateAndRead
+open Steel.ST.GenElim
+
+module AP = LowParse.SteelST.ArrayPtr
+module SZ = FStar.SizeT
+module R = Steel.ST.Reference
+module NL = LowParse.SteelST.VCList.Sorted
+module U8 = FStar.UInt8
+module U64 = FStar.UInt64
+
+#restart-solver
+unfold
+let get_raw_data_item_payload_array_post
+  (va: v parse_raw_data_item_kind raw_data_item)
+  (vh: v (get_parser_kind parse_header) header)
+  (n: nat)
+  (vc: v (NL.parse_nlist_kind n parse_raw_data_item_kind) (NL.nlist n raw_data_item))
+: GTot prop
+=
+        let (| h, c |) = synth_raw_data_item_recip va.contents in
+        let (| b, x |) = h in
+        // order of the following conjuncts matters for typechecking
+        vh.contents == h /\
+        n == UInt64.v (argument_as_uint64 b x) /\
+        va.contents == Array vc.contents /\
+        vc.contents == c /\
+        AP.merge_into (array_of' vh) (array_of' vc) (array_of va)
+
+let get_raw_data_item_payload_array
+  (#opened: _)
+  (#va: v parse_raw_data_item_kind raw_data_item)
+  (a: byte_array)
+: STGhost (Ghost.erased byte_array) opened
+    (aparse parse_raw_data_item a va)
+    (fun a' -> exists_ (fun vh -> exists_ (fun (n: nat) -> exists_ (fun vc ->
+      aparse parse_header a vh `star`
+      aparse (NL.parse_nlist n parse_raw_data_item) a' vc `star`
+      pure (get_raw_data_item_payload_array_post va vh n vc)
+    ))))
+    (Array? va.contents)
+    (fun _ -> True)
+= Classical.forall_intro parse_raw_data_item_eq;
+  let _ = rewrite_aparse a (parse_dtuple2 parse_header (parse_content parse_raw_data_item) `parse_synth` synth_raw_data_item) in
+  let va1 = elim_synth' _ _ synth_raw_data_item_recip a () in // (parse_dtuple2 parse_header (parse_content parse_raw_data_item)) synth_raw_data_item a () in
+  let a' = ghost_split_dtuple2_full _ _ a in // parse_header (parse_content parse_raw_data_item) a in
+  let _ = gen_elim () in
+  let vh = vpattern_replace (aparse _ a) in
+  let (| b, x |) = vh.contents in
+  let n = UInt64.v (argument_as_uint64 b x) in
+  let vc = rewrite_aparse a' (NL.parse_nlist n parse_raw_data_item) in
+  assert (get_raw_data_item_payload_array_post va vh n vc);
+  noop ();
+  a'
+
+#push-options "--z3rlimit 32"
+
+#restart-solver
+let intro_raw_data_item_array
+  (#opened: _)
+  (#vh: v (get_parser_kind parse_header) header)
+  (h: byte_array)
+  (#n: nat)
+  (#vc: v (NL.parse_nlist_kind n parse_raw_data_item_kind) (NL.nlist n raw_data_item))
+  (c: byte_array)
+: STGhost (v parse_raw_data_item_kind raw_data_item) opened
+    (aparse parse_header h vh `star`
+      aparse (NL.parse_nlist n parse_raw_data_item) c vc
+    )
+    (fun va -> aparse parse_raw_data_item h va)
+    (
+      let (| b, x |) = vh.contents in
+      let (major_type, _) = b in
+      n == UInt64.v (argument_as_uint64 b x) /\
+      major_type == get_major_type (Array vc.contents) /\
+      AP.adjacent (array_of' vh) (array_of' vc)
+    )
+    (fun va ->
+      get_raw_data_item_payload_array_post va vh n vc
+    )
+= Classical.forall_intro parse_raw_data_item_eq;
+  let h' = uint64_as_argument (get_major_type (Array vc.contents)) (UInt64.uint_to_t n) in
+  assert (vh.contents == h');
+  noop ();
+  let _ = rewrite_aparse c (parse_content parse_raw_data_item vh.contents) in
+  let _ = intro_dtuple2 parse_header (parse_content parse_raw_data_item) h c in
+  let _ = intro_synth (parse_dtuple2 parse_header (parse_content parse_raw_data_item)) synth_raw_data_item h () in 
+  rewrite_aparse h parse_raw_data_item
+
+#pop-options
+
+[@@erasable]
+noeq
+type focus_array_res = {
+  n: U64.t;
+  l: v (NL.parse_nlist_kind (U64.v n) parse_raw_data_item_kind) (NL.nlist (U64.v n) raw_data_item);
+  a: byte_array;
+}
+
+#push-options "--z3rlimit 16"
+
+#restart-solver
+
+let focus_array
+  (#n': Ghost.erased U64.t)
+  (#a': Ghost.erased byte_array)
+  (#va: v parse_raw_data_item_kind raw_data_item)
+  (pn: R.ref U64.t)
+  (pa: R.ref byte_array)
+  (a: byte_array)
+: ST focus_array_res
+    (aparse parse_raw_data_item a va `star`
+      R.pts_to pn full_perm n' `star`
+      R.pts_to pa full_perm a'
+    )
+    (fun res ->
+      R.pts_to pn full_perm res.n `star`
+      R.pts_to pa full_perm res.a `star`
+      aparse (NL.parse_nlist (U64.v res.n) parse_raw_data_item) res.a res.l `star`
+      (aparse (NL.parse_nlist (U64.v res.n) parse_raw_data_item) res.a res.l `implies_`
+        aparse parse_raw_data_item a va
+      )
+    )
+    (Array? va.contents)
+    (fun res ->
+      va.contents == Array res.l.contents
+    )
+= let gn : Ghost.erased U64.t = Ghost.hide (U64.uint_to_t (List.Tot.length (Array?.v va.contents))) in
+  let ga' = get_raw_data_item_payload_array a in
+  let _ = gen_elim () in
+  let gl = rewrite_aparse ga' (NL.parse_nlist (U64.v gn) parse_raw_data_item) in
+  let a' = hop_aparse_aparse jump_header _ a ga' in
+  let n = read_header_argument_as_uint64 a in
+  let res = {
+    n = n;
+    l = gl;
+    a = a';
+  }
+  in
+  R.write pn n;
+  R.write pa a';
+  rewrite (aparse _ a' _) (aparse (NL.parse_nlist (U64.v res.n) parse_raw_data_item) res.a res.l);
+  intro_implies
+    (aparse (NL.parse_nlist (U64.v res.n) parse_raw_data_item) res.a res.l)
+    (aparse parse_raw_data_item a va)
+    (aparse parse_header a _)
+    (fun _ ->
+      let _ = intro_raw_data_item_array a res.a in
+      vpattern_rewrite (aparse parse_raw_data_item a) va
+    );
+  return res
+
+#pop-options

src/cbor/CBOR.SteelST.fst

@@ -1,6 +1,8 @@
 module CBOR.SteelST
 include CBOR.Spec
 
+module DummyArray = CBOR.SteelST.Array // for dependencies only
+
 let validate_raw_data_item = CBOR.SteelST.Validate.validate_raw_data_item
 let jump_raw_data_item = CBOR.SteelST.Validate.jump_raw_data_item
 let jump_header = CBOR.SteelST.Validate.jump_header

src/cbor/CDDL.Spec.fst

@@ -10,8 +10,16 @@ let t_choice (t1 t2: typ) : typ = (fun x -> t1 x || t2 x)
 let t_always_false = (fun _ -> false)
 
 // Recursive type (needed by COSE Section 5.1 "Recipient")
-let rec rec_typ' (f: (typ -> typ)) (t: Cbor.raw_data_item) : GTot bool (decreases t) =
-  f (fun t' -> if FStar.StrongExcludedMiddle.strong_excluded_middle (t' << t) then rec_typ' f t' else false) t
+
+let rec_typ'_rec
+  (f: (typ -> typ)) (t: Cbor.raw_data_item)
+  (rec_typ': ((t': Cbor.raw_data_item { Seq.length (Cbor.serialize_raw_data_item t') < Seq.length (Cbor.serialize_raw_data_item t) }) -> GTot bool))
+  (t': Cbor.raw_data_item)
+: GTot bool
+= if Seq.length (Cbor.serialize_raw_data_item t') < Seq.length (Cbor.serialize_raw_data_item t) then rec_typ' t' else false
+
+let rec rec_typ' (f: (typ -> typ)) (t: Cbor.raw_data_item) : GTot bool (decreases (Seq.length (Cbor.serialize_raw_data_item t))) =
+  f (rec_typ'_rec f t (rec_typ' f)) t
 
 let rec_typ : (typ -> typ) -> typ = rec_typ'
 
@@ -27,12 +35,20 @@ let bytes = bstr
 let tstr : typ = (fun x -> Cbor.String? x && Cbor.String?.typ x = Cbor.major_type_text_string)
 let text = tstr
 
-let t_false : typ = (fun x -> Cbor.Simple? x && Cbor.Simple?.v x = 20uy)
-let t_true : typ = (fun x -> Cbor.Simple? x && Cbor.Simple?.v x = 21uy)
+let simple_value_false : Cbor.simple_value = 20uy
+let simple_value_true : Cbor.simple_value = 21uy
+let simple_value_nil : Cbor.simple_value = 22uy
+let simple_value_undefined : Cbor.simple_value = 23uy
+
+let t_simple_value_literal (s: Cbor.simple_value) : typ =
+  (fun x -> Cbor.Simple? x && Cbor.Simple?.v x = s)
+
+let t_false : typ = t_simple_value_literal simple_value_false
+let t_true : typ = t_simple_value_literal simple_value_true
 let t_bool : typ = t_choice t_false t_true
-let t_nil : typ = (fun x -> Cbor.Simple? x && Cbor.Simple?.v x = 22uy)
+let t_nil : typ = t_simple_value_literal simple_value_nil
 let t_null : typ = t_nil
-let t_undefined : typ = (fun x -> Cbor.Simple? x && Cbor.Simple?.v x = 23uy)
+let t_undefined : typ = t_simple_value_literal simple_value_undefined
 
 let t_uint_literal (v: U64.t) : typ = (fun x ->
   uint x &&
@@ -137,10 +153,8 @@ let array_group3_zero_or_more : array_group3 -> array_group3 = array_group3_zero
 let array_group3_one_or_more (a: array_group3) : array_group3 =
   a `array_group3_concat` array_group3_zero_or_more a
 
-let array_group3_zero_or_one (a: array_group3) : Tot array_group3 = fun l ->
-  match a l with
-  | None -> Some l
-  | Some l' -> Some l'
+let array_group3_zero_or_one (a: array_group3) : Tot array_group3 =
+  a `array_group3_choice` array_group3_empty
 
 let array_group3_item (t: typ) : array_group3 = fun l ->
   match l with