From fb323b9e7851201be15592a0e7e5bcc90bf920f4 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Fri, 1 Sep 2023 16:34:18 -0700
Subject: [PATCH] WIP CDDL impl

---
 src/cbor/CBOR.SteelST.Array.fst |  158 +++++
 src/cbor/CBOR.SteelST.fst       |    2 +
 src/cbor/CDDL.Spec.fst          |   34 +-
 src/cbor/CDDL.SteelST.fst       | 1081 +++++++++++++++++++++++++++++++
 4 files changed, 1265 insertions(+), 10 deletions(-)
 create mode 100644 src/cbor/CBOR.SteelST.Array.fst
 create mode 100644 src/cbor/CDDL.SteelST.fst

diff --git a/src/cbor/CBOR.SteelST.Array.fst b/src/cbor/CBOR.SteelST.Array.fst
new file mode 100644
index 000000000..0cdc0698f
--- /dev/null
+++ b/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
diff --git a/src/cbor/CBOR.SteelST.fst b/src/cbor/CBOR.SteelST.fst
index 2e884fe00..0aad9bb4b 100644
--- a/src/cbor/CBOR.SteelST.fst
+++ b/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
diff --git a/src/cbor/CDDL.Spec.fst b/src/cbor/CDDL.Spec.fst
index efbb04e1c..a88444b61 100644
--- a/src/cbor/CDDL.Spec.fst
+++ b/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
diff --git a/src/cbor/CDDL.SteelST.fst b/src/cbor/CDDL.SteelST.fst
new file mode 100644
index 000000000..fa7caefdf
--- /dev/null
+++ b/src/cbor/CDDL.SteelST.fst
@@ -0,0 +1,1081 @@
+module CDDL.SteelST
+include CDDL.Spec
+open LowParse.SteelST.Combinators
+module Cbor = CBOR.SteelST
+module SZ = FStar.SizeT
+open Steel.ST.GenElim
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_typ (t: typ) =
+  (#va: v Cbor.parse_raw_data_item_kind Cbor.raw_data_item) ->
+  (a: byte_array) ->
+  ST bool
+    (aparse Cbor.parse_raw_data_item a va)
+    (fun _ -> aparse Cbor.parse_raw_data_item a va)
+    True
+    (fun res -> res == t va.contents)
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_typ_with_size (t: typ) =
+  (#va: v Cbor.parse_raw_data_item_kind Cbor.raw_data_item) ->
+  (a: byte_array) ->
+  (sz: SZ.t) ->
+  ST bool
+    (aparse Cbor.parse_raw_data_item a va)
+    (fun _ -> aparse Cbor.parse_raw_data_item a va)
+    (SZ.v sz == Seq.length (Cbor.serialize_raw_data_item va.contents))
+    (fun res -> res == t va.contents)
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_typ_with_size_of_impl_typ
+  (#t: typ)
+  (i: impl_typ t)
+: Tot (impl_typ_with_size t)
+= fun a _ -> i a
+
+module AP = LowParse.SteelST.ArrayPtr
+
+inline_for_extraction [@@noextract_to "krml"]
+let get_serialized_size
+  (#k: Ghost.erased parser_kind)
+  (#t: Type)
+  (#p: parser k t)
+  (#vp: v k t)
+  (s: serializer p)
+  (j: jumper p)
+  (a: byte_array)
+: ST SZ.t
+    (aparse p a vp)
+    (fun res -> aparse p a vp)
+    True
+    (fun res ->
+      SZ.v res == AP.length (array_of vp) /\
+      SZ.v res == Seq.length (serialize s vp.contents)
+    )
+=
+  let vb = elim_aparse p a in
+  parsed_data_is_serialize s (AP.contents_of vb);
+  let res = j a in
+  let _ = intro_aparse p a in
+  return res
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_typ_of_impl_typ_with_size
+  (#t: typ)
+  (i: impl_typ_with_size t)
+: Tot (impl_typ t)
+= fun a ->
+    let sz = get_serialized_size Cbor.serialize_raw_data_item CBOR.SteelST.Validate.jump_raw_data_item a in
+    i a sz
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_t_choice
+  (#t1 #t2: typ)
+  (i1: impl_typ t1)
+  (i2: impl_typ t2)
+: Tot (impl_typ (t1 `t_choice` t2))
+= fun a ->
+    if i1 a
+    then return true
+    else i2 a
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_t_always_false : impl_typ t_always_false
+= fun _ -> return false
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_rec_typ_body
+  (f: (typ -> typ))
+  (impl_f: (t: typ) -> impl_typ_with_size t -> impl_typ_with_size (f t))
+  (impl_rec_typ: impl_typ_with_size (rec_typ f))
+: Tot (impl_typ_with_size (rec_typ f))
+= fun #va a sz ->
+    [@@inline_let]
+    let _ = assert (rec_typ f va.contents == f (rec_typ'_rec f va.contents (rec_typ f)) va.contents) by (FStar.Tactics.trefl ()) in
+    impl_f
+      (rec_typ'_rec f va.contents (rec_typ f))
+      (fun #va' a' sz' -> if sz' `SZ.lt` sz then impl_rec_typ a' sz' else return false)
+      #va a sz
+
+[@@noextract_to "krml"] let rec impl_rec_typ_template // this cannot extract because I cannot use inline_for_extraction on recursive functions. This function only provides a template to create implementations for recursive types.
+  (f: (typ -> typ))
+  (impl_f: (t: typ) -> impl_typ_with_size t -> impl_typ_with_size (f t))
+: Tot (impl_typ_with_size (rec_typ f))
+= fun a sz -> impl_rec_typ_body f impl_f (impl_rec_typ_template f impl_f) a sz
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_any: impl_typ any = (fun _ -> return true)
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_uint : impl_typ uint
+= fun a ->
+    let mt = CBOR.SteelST.Validate.read_major_type a in
+    return (mt = Cbor.major_type_uint64)
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_nint : impl_typ nint
+= fun a ->
+    let mt = CBOR.SteelST.Validate.read_major_type a in
+    return (mt = Cbor.major_type_neg_int64)
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_t_int : impl_typ t_int
+= impl_uint `impl_t_choice` impl_nint
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_bstr : impl_typ bstr
+= fun a ->
+    let mt = CBOR.SteelST.Validate.read_major_type a in
+    return (mt = Cbor.major_type_byte_string)
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_bytes : impl_typ CDDL.Spec.bytes = impl_bstr
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_tstr : impl_typ tstr
+= fun a ->
+    let mt = CBOR.SteelST.Validate.read_major_type a in
+    return (mt = Cbor.major_type_text_string)
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_text : impl_typ text = impl_tstr
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_t_simple_value_literal (s: Cbor.simple_value) : impl_typ (t_simple_value_literal s)
+= fun a ->
+    let mt = CBOR.SteelST.Validate.read_major_type a in
+    if mt = Cbor.major_type_simple_value
+    then begin
+      let sv = CBOR.SteelST.Read.read_simple_value a in
+      return (sv = s)
+    end else begin
+      return false
+    end
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_t_false : impl_typ t_false
+= impl_t_simple_value_literal simple_value_false
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_t_true : impl_typ t_true
+= impl_t_simple_value_literal simple_value_true
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_t_bool : impl_typ t_bool
+= impl_t_false `impl_t_choice` impl_t_true
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_t_nil : impl_typ t_nil
+= impl_t_simple_value_literal simple_value_nil
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_t_null : impl_typ t_null
+= impl_t_nil
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_t_undefined : impl_typ t_undefined
+= impl_t_simple_value_literal simple_value_undefined
+
+module U64 = FStar.UInt64
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_t_uint_literal (s: U64.t) : impl_typ (t_uint_literal s)
+= fun a ->
+    let mt = CBOR.SteelST.Validate.read_major_type a in
+    if mt = Cbor.major_type_uint64
+    then begin
+      let sv = CBOR.SteelST.Read.read_int64 a in
+      return (sv = s)
+    end else begin
+      return false
+    end
+
+module VC = LowParse.SteelST.VCList
+module R = Steel.ST.Reference
+
+[@@noextract_to "krml"]
+let impl_array_group3_post
+  (g: array_group3)
+  (l l': list Cbor.raw_data_item)
+  (res: bool)
+: Tot prop
+= res == Some? (g l) /\
+  (res == true ==> g l == Some l')
+
+[@@erasable]
+noeq
+type impl_array_group3_res
+= {
+    n: U64.t;
+    al: byte_array;
+    l: v (VC.parse_nlist_kind (U64.v n) Cbor.parse_raw_data_item_kind) (VC.nlist (U64.v n) Cbor.raw_data_item);
+    res: bool;
+  }
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_array_group3
+  (g: array_group3)
+: Tot Type
+= (#n: Ghost.erased U64.t) ->
+  (#al: Ghost.erased byte_array) ->
+  (#l: v (VC.parse_nlist_kind (U64.v n) Cbor.parse_raw_data_item_kind) (VC.nlist (U64.v n) Cbor.raw_data_item)) ->
+  (#res: Ghost.erased bool) ->
+  (pn: R.ref U64.t) ->
+  (pl: R.ref byte_array) ->
+  (pres: R.ref bool) ->
+  ST impl_array_group3_res
+    (
+      R.pts_to pn full_perm n `star`
+      R.pts_to pl full_perm al `star`
+      R.pts_to pres full_perm res `star`
+      aparse (VC.parse_nlist (U64.v n) Cbor.parse_raw_data_item) al l
+    )
+    (fun res ->
+      R.pts_to pn full_perm res.n `star`
+      R.pts_to pl full_perm res.al `star`
+      R.pts_to pres full_perm res.res `star`
+      aparse (VC.parse_nlist (U64.v res.n) Cbor.parse_raw_data_item) res.al res.l `star`
+      (aparse (VC.parse_nlist (U64.v res.n) Cbor.parse_raw_data_item) res.al res.l `implies_`
+        aparse (VC.parse_nlist (U64.v n) Cbor.parse_raw_data_item) al l
+      )
+    )
+    True
+    (fun res ->
+        impl_array_group3_post g l.contents res.l.contents res.res
+    )
+
+let rewrite_with_implies
+  (#opened: _)
+  (p q: vprop)
+: STGhost unit opened
+    p (fun _ -> q `star` (q `implies_` p))
+    (p == q)
+    (fun _ -> True)
+= rewrite p q;
+  intro_implies q p emp (fun _ -> rewrite q p)
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_array_group3_always_false : impl_array_group3 array_group3_always_false
+= fun #gn #ga #gl pn pl pres ->
+    let w = {
+      n = gn;
+      al = ga;
+      l = gl;
+      res = false;
+    }
+    in
+    R.write pres false;
+    rewrite_with_implies
+      (aparse (VC.parse_nlist (U64.v gn) Cbor.parse_raw_data_item) ga gl)
+      (aparse (VC.parse_nlist (U64.v w.n) Cbor.parse_raw_data_item) w.al w.l);
+    return w
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_array_group3_empty : impl_array_group3 array_group3_empty
+= fun #gn #ga #gl pn pl pres ->
+    let w = {
+      n = gn;
+      al = ga;
+      l = gl;
+      res = true;
+    }
+    in
+    R.write pres true;
+    rewrite_with_implies
+      (aparse (VC.parse_nlist (U64.v gn) Cbor.parse_raw_data_item) ga gl)
+      (aparse (VC.parse_nlist (U64.v w.n) Cbor.parse_raw_data_item) w.al w.l);
+    return w
+
+#push-options "--z3rlimit 16"
+#restart-solver
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_array_group3_concat
+  (#g1 #g2: array_group3)
+  (i1: impl_array_group3 g1)
+  (i2: impl_array_group3 g2)
+: impl_array_group3 (array_group3_concat g1 g2)
+= fun #gn #ga #gl pn pl pres ->
+    let w1 = i1 pn pl pres in
+    let res1 = R.read pres in
+    if res1
+    then begin
+      let w2 = i2 pn pl pres in
+      implies_trans
+        (aparse (VC.parse_nlist (U64.v w2.n) Cbor.parse_raw_data_item) w2.al w2.l)
+        (aparse (VC.parse_nlist (U64.v w1.n) Cbor.parse_raw_data_item) w1.al w1.l)
+        (aparse (VC.parse_nlist (U64.v gn) Cbor.parse_raw_data_item) ga gl);
+      return w2
+    end else begin
+      noop ();
+      return w1
+    end
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_array_group3_choice
+  (#g1 #g2: array_group3)
+  (i1: impl_array_group3 g1)
+  (i2: impl_array_group3 g2)
+: Tot (impl_array_group3 (array_group3_choice g1 g2))
+= fun #gn #ga #gl pn pl pres ->
+    let n = R.read pn in
+    let a = R.read pl in
+    let w1 = i1 pn pl pres in
+    let res1 = R.read pres in
+    if res1
+    then begin
+      noop ();
+      return w1
+    end else begin
+      R.write pn n;
+      R.write pl a;
+      elim_implies
+        (aparse (VC.parse_nlist (U64.v w1.n) Cbor.parse_raw_data_item) w1.al w1.l)
+        (aparse (VC.parse_nlist (U64.v gn) Cbor.parse_raw_data_item) ga gl);
+      i2 #gn #ga #gl pn pl pres
+    end
+
+let impl_array_group3_res_strong
+  (g: array_group3)
+  (l: list Cbor.raw_data_item)
+: Tot Type0
+= (res: impl_array_group3_res { impl_array_group3_post g l res.l.contents res.res })
+
+module GR = Steel.ST.GhostReference
+
+unfold
+let impl_array_group3_zero_or_more_inv_prop_gen
+  (g: array_group3)
+  (gn: Ghost.erased U64.t)
+  (gl: list Cbor.raw_data_item)
+  (wres: bool)
+  (wl: list Cbor.raw_data_item)
+  (cont: bool)
+: Tot prop
+= cont = not wres /\
+  begin if cont
+  then array_group3_zero_or_more g gl == array_group3_zero_or_more' g wl 
+  else impl_array_group3_post (array_group3_zero_or_more g) gl wl wres
+  end
+
+let impl_array_group3_zero_or_more_inv_prop
+  (g: array_group3)
+  (gn: Ghost.erased U64.t)
+  (gl: v (VC.parse_nlist_kind (U64.v gn) Cbor.parse_raw_data_item_kind) (VC.nlist (U64.v gn) Cbor.raw_data_item))
+  (w: impl_array_group3_res)
+  (cont: bool)
+: Tot prop
+= impl_array_group3_zero_or_more_inv_prop_gen g gn gl.contents w.res w.l.contents cont
+
+[@@__reduce__]
+let impl_array_group3_zero_or_more_inv_body
+  (g: array_group3)
+  (gn: Ghost.erased U64.t)
+  (ga: Ghost.erased byte_array)
+  (gl: v (VC.parse_nlist_kind (U64.v gn) Cbor.parse_raw_data_item_kind) (VC.nlist (U64.v gn) Cbor.raw_data_item))
+  (pn: R.ref U64.t)
+  (pl: R.ref byte_array)
+  (pres: R.ref bool)
+  (wn: U64.t)
+  (wal: byte_array)
+  (wl: v (VC.parse_nlist_kind (U64.v wn) Cbor.parse_raw_data_item_kind) (VC.nlist (U64.v wn) Cbor.raw_data_item))
+  (wres: bool)
+: Tot vprop
+= 
+  R.pts_to pn full_perm wn `star`
+  R.pts_to pl full_perm wal `star`
+  R.pts_to pres full_perm wres `star`
+  aparse (VC.parse_nlist (U64.v wn) Cbor.parse_raw_data_item) wal wl `star`
+  (aparse (VC.parse_nlist (U64.v wn) Cbor.parse_raw_data_item) wal wl `implies_`
+    aparse (VC.parse_nlist (U64.v gn) Cbor.parse_raw_data_item) ga gl
+  )
+
+[@@__reduce__]
+let impl_array_group3_zero_or_more_inv0
+  (g: array_group3)
+  (gn: Ghost.erased U64.t)
+  (ga: Ghost.erased byte_array)
+  (gl: v (VC.parse_nlist_kind (U64.v gn) Cbor.parse_raw_data_item_kind) (VC.nlist (U64.v gn) Cbor.raw_data_item))
+  (pn: R.ref U64.t)
+  (pl: R.ref byte_array)
+  (pres: R.ref bool)
+  (pw: GR.ref impl_array_group3_res)
+  (cont: bool)
+: Tot vprop
+= exists_ (fun w ->
+    GR.pts_to pw full_perm w `star`
+    impl_array_group3_zero_or_more_inv_body g gn ga gl pn pl pres w.n w.al w.l w.res `star`
+    pure (impl_array_group3_zero_or_more_inv_prop g gn gl w cont)
+  )
+
+let impl_array_group3_zero_or_more_inv
+  (g: array_group3)
+  (gn: Ghost.erased U64.t)
+  (ga: Ghost.erased byte_array)
+  (gl: v (VC.parse_nlist_kind (U64.v gn) Cbor.parse_raw_data_item_kind) (VC.nlist (U64.v gn) Cbor.raw_data_item))
+  (pn: R.ref U64.t)
+  (pl: R.ref byte_array)
+  (pres: R.ref bool)
+  (pw: GR.ref impl_array_group3_res)
+  (cont: bool)
+: Tot vprop
+= impl_array_group3_zero_or_more_inv0 g gn ga gl pn pl pres pw cont
+
+let intro_impl_array_group3_zero_or_more_inv
+  (#opened: _)
+  (#w': impl_array_group3_res)
+  (g: array_group3)
+  (gn: Ghost.erased U64.t)
+  (ga: Ghost.erased byte_array)
+  (gl: v (VC.parse_nlist_kind (U64.v gn) Cbor.parse_raw_data_item_kind) (VC.nlist (U64.v gn) Cbor.raw_data_item))
+  (pn: R.ref U64.t)
+  (pl: R.ref byte_array)
+  (pres: R.ref bool)
+  (pw: GR.ref impl_array_group3_res)
+  (wn: U64.t)
+  (wal: byte_array)
+  (wl: v (VC.parse_nlist_kind (U64.v wn) Cbor.parse_raw_data_item_kind) (VC.nlist (U64.v wn) Cbor.raw_data_item))
+  (wres: bool)
+  (cont: bool)
+: STGhost unit opened
+    (impl_array_group3_zero_or_more_inv_body g gn ga gl pn pl pres wn wal wl wres `star`
+      GR.pts_to pw full_perm w'
+    )
+    (fun _ -> impl_array_group3_zero_or_more_inv g gn ga gl pn pl pres pw cont)
+    (impl_array_group3_zero_or_more_inv_prop_gen g gn gl.contents wres wl.contents cont)
+    (fun _ -> True)
+= let w = {
+    al = wal;
+    n = wn;
+    l = wl;
+    res = wres;
+  }
+  in
+  rewrite
+    (impl_array_group3_zero_or_more_inv_body g gn ga gl pn pl pres wn wal wl wres)
+    (impl_array_group3_zero_or_more_inv_body g gn ga gl pn pl pres w.n w.al w.l w.res);
+  GR.write pw w;
+  rewrite
+    (impl_array_group3_zero_or_more_inv0 g gn ga gl pn pl pres pw cont)
+    (impl_array_group3_zero_or_more_inv g gn ga gl pn pl pres pw cont)
+
+let elim_impl_array_group3_zero_or_more_inv
+  (#opened: _)
+  (g: array_group3)
+  (gn: Ghost.erased U64.t)
+  (ga: Ghost.erased byte_array)
+  (gl: v (VC.parse_nlist_kind (U64.v gn) Cbor.parse_raw_data_item_kind) (VC.nlist (U64.v gn) Cbor.raw_data_item))
+  (pn: R.ref U64.t)
+  (pl: R.ref byte_array)
+  (pres: R.ref bool)
+  (pw: GR.ref impl_array_group3_res)
+  (cont: bool)
+: STGhost impl_array_group3_res opened
+    (impl_array_group3_zero_or_more_inv g gn ga gl pn pl pres pw cont)
+    (fun w -> impl_array_group3_zero_or_more_inv_body g gn ga gl pn pl pres w.n w.al w.l w.res `star`
+      GR.pts_to pw full_perm w
+    )
+    True
+    (fun w -> impl_array_group3_zero_or_more_inv_prop g gn gl w cont)
+= rewrite
+    (impl_array_group3_zero_or_more_inv g gn ga gl pn pl pres pw cont)
+    (impl_array_group3_zero_or_more_inv0 g gn ga gl pn pl pres pw cont);
+  let _ = gen_elim () in
+  let w = vpattern_replace (GR.pts_to pw full_perm) in
+  rewrite
+    (impl_array_group3_zero_or_more_inv_body g gn ga gl pn pl pres _ _ _ _)
+    (impl_array_group3_zero_or_more_inv_body g gn ga gl pn pl pres w.n w.al w.l w.res);
+  w
+
+let implies_refl
+  (#opened: _)
+  (p: vprop)
+: STGhostT unit opened
+    emp
+    (fun _ -> p `implies_` p)
+= intro_implies p p emp (fun _ -> noop ())
+
+#pop-options
+
+#push-options "--z3rlimit 32"
+#restart-solver
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_array_group3_zero_or_more
+  (#g: array_group3)
+  (i: impl_array_group3 g)
+: Tot (impl_array_group3 (array_group3_zero_or_more g))
+= fun #gn #ga #gl pn pl pres ->
+    R.write pres false;
+    implies_refl (aparse (VC.parse_nlist (U64.v gn) Cbor.parse_raw_data_item) ga gl);
+    let w0 = {
+      n = gn;
+      al = ga;
+      l = gl;
+      res = false;
+    }
+    in
+    let pw = GR.alloc w0 in
+    intro_impl_array_group3_zero_or_more_inv g gn ga gl pn pl pres pw _ _ _ _ true;
+    Steel.ST.Loops.while_loop
+      (impl_array_group3_zero_or_more_inv g gn ga gl pn pl pres pw)
+      (fun _ ->
+        let gcont = elim_exists #_ #_ #(impl_array_group3_zero_or_more_inv g gn ga gl pn pl pres pw) () in
+        let _ = elim_impl_array_group3_zero_or_more_inv g gn ga gl pn pl pres pw gcont in
+        let res = R.read pres in
+        [@@inline_let]
+        let cont = not res in
+        intro_impl_array_group3_zero_or_more_inv g gn ga gl pn pl pres pw _ _ _ _ cont;
+        return cont
+      )
+      (fun _ ->
+        let w0 = elim_impl_array_group3_zero_or_more_inv g gn ga gl pn pl pres pw true in
+        let al = R.read pl in
+        let n = R.read pn in
+        let w = i pn pl pres in
+        let res = R.read pres in
+        let n' = R.read pn in
+        let res = res && (n' `U64.lt` n) in
+        R.write pres (not res);
+        if res
+        then begin
+          implies_trans
+            (aparse (VC.parse_nlist (U64.v w.n) Cbor.parse_raw_data_item) w.al w.l)
+            (aparse (VC.parse_nlist (U64.v w0.n) Cbor.parse_raw_data_item) w0.al w0.l)
+            (aparse (VC.parse_nlist (U64.v gn) Cbor.parse_raw_data_item) ga gl);
+          intro_impl_array_group3_zero_or_more_inv g gn ga gl pn pl pres pw _ _ _ _ true;
+          noop ()
+        end else begin
+          elim_implies
+            (aparse (VC.parse_nlist (U64.v w.n) Cbor.parse_raw_data_item) w.al w.l)
+            (aparse (VC.parse_nlist (U64.v w0.n) Cbor.parse_raw_data_item) w0.al w0.l);
+          R.write pn n;
+          R.write pl al;
+          vpattern_rewrite (R.pts_to pn full_perm) w0.n;
+          vpattern_rewrite (R.pts_to pl full_perm) w0.al;
+          intro_impl_array_group3_zero_or_more_inv g gn ga gl pn pl pres pw _ _ _ _ false;
+          noop ()
+        end
+      );
+    let w = elim_impl_array_group3_zero_or_more_inv g gn ga gl pn pl pres pw false in
+    GR.free pw;
+    return w
+
+#pop-options
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_array_group3_one_or_more
+  (#g: array_group3)
+  (i: impl_array_group3 g)
+: Tot (impl_array_group3 (array_group3_one_or_more g))
+= i `impl_array_group3_concat` impl_array_group3_zero_or_more i
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_array_group3_zero_or_one
+  (#g: array_group3)
+  (i: impl_array_group3 g)
+: Tot (impl_array_group3 (array_group3_zero_or_one g))
+= i `impl_array_group3_choice` impl_array_group3_empty
+
+[@@erasable]
+noeq
+type ghost_focus_nlist_res (k: parser_kind) (t: Type0) = {
+  n: nat;
+  a2: byte_array;
+  va1: v k t;
+  va2: v (VC.parse_nlist_kind n k) (VC.nlist n t);
+}
+
+#push-options "--z3rlimit 32"
+#restart-solver
+
+let ghost_focus_nlist
+  (#opened: _)
+  (#k: parser_kind)
+  (#t: Type0)
+  (p: parser k t)
+  (n: nat)
+  (#va: v _ _)
+  (a: byte_array)
+: STGhost (ghost_focus_nlist_res k t) opened
+    (aparse (VC.parse_nlist n p) a va)
+    (fun w ->
+      aparse p a w.va1 `star`
+      aparse (VC.parse_nlist w.n p) w.a2 w.va2 `star`
+      ((aparse p a w.va1 `star`
+        aparse (VC.parse_nlist w.n p) w.a2 w.va2) `implies_`
+        aparse (VC.parse_nlist n p) a va
+    ))
+    (Cons? va.contents /\
+      n > 0 /\
+      k.parser_kind_subkind == Some ParserStrong
+    )
+    (fun w ->
+      n == w.n + 1 /\
+      va.contents == w.va1.contents :: w.va2.contents /\
+      AP.merge_into (array_of w.va1) (array_of w.va2) (array_of va)
+    )
+= let n_pred : nat = n - 1 in
+  let a2 = VC.elim_nlist_cons p n n_pred a in
+  let _ = gen_elim () in
+  let va1 = vpattern_replace (aparse p a) in
+  let va2 = vpattern_replace (aparse (VC.parse_nlist n_pred p) a2) in
+  let w = {
+    n = n_pred;
+    a2 = Ghost.reveal a2;
+    va1 = va1;
+    va2 = va2;
+  }
+  in
+  vpattern_rewrite (aparse p a) w.va1;
+  rewrite (aparse _ a2 _) (aparse (VC.parse_nlist w.n p) w.a2 w.va2);
+  intro_implies
+    (aparse p a w.va1 `star`
+      aparse (VC.parse_nlist w.n p) w.a2 w.va2)
+    (aparse (VC.parse_nlist n p) a va)
+    emp
+    (fun _ ->
+      let _ = VC.intro_nlist_cons n p w.n a w.a2 in
+      vpattern_rewrite (aparse _ a) va
+    );
+  w
+
+#pop-options
+
+let vpattern_rewrite_with_implies
+  (#opened: _)
+  (#a: Type)
+  (#x1: a)
+  (p: a -> vprop)
+  (x2: a)
+: STGhost unit opened
+    (p x1)
+    (fun _ -> p x2 `star` (p x2 `implies_` p x1))
+    (x1 == x2)
+    (fun _ -> True)
+= rewrite_with_implies (p x1) (p x2)
+
+inline_for_extraction
+let hop_aparse_aparse_with_implies
+  (#k1: Ghost.erased parser_kind)
+  (#t1: Type)
+  (#p1: parser k1 t1)
+  (j1: jumper p1)
+  (#k2: Ghost.erased parser_kind)
+  (#t2: _)
+  (p2: parser k2 t2)
+  (#va1: _)
+  (#va2: _)
+  (a1: byte_array)
+  (a2: Ghost.erased byte_array)
+: ST byte_array
+    (aparse p1 a1 va1 `star` aparse p2 a2 va2)
+    (fun res -> aparse p1 a1 va1 `star` aparse p2 res va2 `star` (aparse p2 res va2 `implies_` aparse p2 a2 va2))
+    (AP.adjacent (array_of va1) (array_of va2))
+    (fun res -> res == Ghost.reveal a2)
+= let res = hop_aparse_aparse j1 p2 a1 a2 in
+  intro_implies
+    (aparse p2 res va2)
+    (aparse p2 a2 va2)
+    emp
+    (fun _ -> vpattern_rewrite (fun res -> aparse _ res _) a2);
+  return res
+
+let rewrite_aparse_with_implies
+  (#opened: _)
+  (#k1: parser_kind)
+  (#t1: Type)
+  (#p1: parser k1 t1)
+  (#y1: v k1 t1)
+  (a: byte_array)
+  (#k2: parser_kind)
+  (#t2: Type)
+  (p2: parser k2 t2)
+: STGhost (v k2 t2) opened
+    (aparse p1 a y1)
+    (fun y2 -> aparse p2 a y2 `star` (aparse p2 a y2 `implies_` aparse p1 a y1))
+    (t1 == t2 /\ (forall bytes . parse p1 bytes == parse p2 bytes))
+    (fun y2 ->
+      t1 == t2 /\
+      array_of' y1 == array_of' y2 /\
+      y1.contents == y2.contents
+    )
+= let y2 = rewrite_aparse a p2 in
+  intro_implies
+    (aparse p2 a y2)
+    (aparse p1 a y1)
+    emp
+    (fun _ ->
+      let _ = rewrite_aparse a p1 in
+      vpattern_rewrite (aparse _ a) y1
+    );
+  y2
+
+#push-options "--z3rlimit 32"
+#restart-solver
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_array_group3_item
+  (#t: typ)
+  (i: impl_typ t)
+: Tot (impl_array_group3 (array_group3_item t))
+= fun #gn #ga #gl pn pl pres ->
+    let n = R.read pn in
+    if n = 0uL
+    then begin
+      noop ();
+      impl_array_group3_always_false pn pl pres
+    end else begin
+      let wcons = ghost_focus_nlist Cbor.parse_raw_data_item _ ga in
+      let a = R.read pl in
+      vpattern_rewrite_with_implies #_ #_ #(Ghost.reveal ga) (fun a -> aparse _ a _) a;
+      if i a
+      then begin
+        let a2 = hop_aparse_aparse_with_implies Cbor.jump_raw_data_item _ a _ in
+        [@@inline_let]
+        let n' : U64.t = n `U64.sub` 1uL in
+        let gl' = rewrite_aparse_with_implies a2 (VC.parse_nlist (U64.v n') Cbor.parse_raw_data_item) in
+        R.write pn n';
+        R.write pl a2;
+        R.write pres true;
+        let w : impl_array_group3_res = {
+          al = a2; 
+          n = n `U64.sub` 1uL;
+          l = gl';
+          res = true;
+        }
+        in
+        rewrite_with_implies (aparse _ a2 _) (aparse (VC.parse_nlist (U64.v w.n) Cbor.parse_raw_data_item) w.al w.l);
+        implies_trans (aparse _ w.al _) (aparse _ a2 _) (aparse _ a2 _);
+        implies_trans (aparse _ w.al _) (aparse _ a2 _) (aparse _ wcons.a2 _);
+        implies_join
+          (aparse _ a _) (aparse _ ga _)
+          (aparse _ w.al _) (aparse _ wcons.a2 _);
+        implies_trans
+          (aparse _ a _ `star` aparse _ w.al _)
+          (aparse _ ga _ `star` aparse _ wcons.a2 _)
+          (aparse _ ga _);
+        implies_curry (aparse _ a _) (aparse _ w.al _) (aparse _ ga _);
+        elim_implies (aparse _ a _) (aparse _ w.al _ `implies_` aparse _ ga _);
+        return w
+      end else begin
+        elim_implies (aparse _ a _) (aparse _ ga _);
+        elim_implies (aparse _ ga _ `star` aparse _ _ _) (aparse _ ga _);
+        impl_array_group3_always_false pn pl pres
+      end
+    end
+
+#pop-options
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_t_array3_res
+  (g: array_group3)
+  (va: v Cbor.parse_raw_data_item_kind Cbor.raw_data_item)
+: Tot Type0
+= (res: bool { res == t_array3 g va.contents })
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_t_array3
+  (#g: array_group3)
+  (i: impl_array_group3 g)
+: Tot (impl_typ (t_array3 g))
+= fun #va a ->
+    let mt = CBOR.SteelST.Validate.read_major_type a in
+    if mt = Cbor.major_type_array
+    then begin
+      noop ();
+      let res : impl_t_array3_res g va =
+        R.with_local 0uL (fun pn ->
+        R.with_local a (fun pa ->
+        R.with_local false (fun pres ->
+          let wl = CBOR.SteelST.Array.focus_array pn pa a in
+          let wi = i pn pa pres in
+          let res0 = R.read pres in
+          let n = R.read pn in
+          let res : impl_t_array3_res g va = res0 && (n = 0uL) in
+          elim_implies
+            (aparse (VC.parse_nlist (U64.v wi.n) Cbor.parse_raw_data_item) wi.al wi.l)
+            (aparse (VC.parse_nlist (U64.v wl.n) Cbor.parse_raw_data_item) wl.a wl.l);
+          elim_implies
+            (aparse (VC.parse_nlist (U64.v wl.n) Cbor.parse_raw_data_item) wl.a wl.l)
+            (aparse Cbor.parse_raw_data_item a va);
+          return res
+        )))
+      in
+      return (res <: bool)
+    end else begin
+      return false
+    end
+
+let rec sieve_list
+  (l: list map_group_entry)
+  (l': list bool { List.Tot.length l' == List.Tot.length l })
+: Tot (list map_group_entry)
+  (decreases l)
+= match l, l' with
+  | a :: q, true :: q' -> a :: sieve_list q q'
+  | _ :: q, false :: q' -> sieve_list q q'
+  | _ -> []
+
+let rec sieve_list_append
+  (l1: list map_group_entry)
+  (l1': list bool { List.Tot.length l1' == List.Tot.length l1 })
+  (l2: list map_group_entry)
+  (l2': list bool { List.Tot.length l2' == List.Tot.length l2 })
+: Lemma
+  (ensures (
+    List.Tot.length (l1 `List.Tot.append` l2) == List.Tot.length (l1' `List.Tot.append` l2') /\
+    sieve_list (l1 `List.Tot.append` l2) (l1' `List.Tot.append` l2') == sieve_list l1 l1' `List.Tot.append` sieve_list l2 l2'
+  ))
+  (decreases l1)
+= List.Tot.append_length l1 l2;
+  List.Tot.append_length l1' l2';
+  match l1, l1' with
+  | _ :: q, _ :: q' -> sieve_list_append q q' l2 l2'
+  | _ -> ()
+
+let list_rev_eq
+  (#t: Type)
+  (a: t)
+  (q: list t)
+: Lemma
+  (List.Tot.rev (a :: q) == List.Tot.rev q `List.Tot.append` [a])
+= List.Tot.rev_rev' (a :: q);
+  List.Tot.rev_rev' q
+
+let rec sieve_list_rev
+  (l1: list map_group_entry)
+  (l1': list bool { List.Tot.length l1' == List.Tot.length l1 })
+: Lemma
+  (ensures (
+    List.Tot.length (List.Tot.rev l1) == List.Tot.length (List.Tot.rev l1') /\
+    sieve_list (List.Tot.rev l1) (List.Tot.rev l1') == List.Tot.rev (sieve_list l1 l1')
+  ))
+  (decreases (List.Tot.length l1))
+= List.Tot.rev_length l1;
+  List.Tot.rev_length l1';
+  match l1, l1' with
+  | a :: q, a' :: q' ->
+    list_rev_eq a q;
+    list_rev_eq a' q';
+    sieve_list_rev q q';
+    sieve_list_append (List.Tot.rev q) (List.Tot.rev q') [a] [a'];
+    List.Tot.rev_append (sieve_list [a] [a']) (sieve_list q q')
+  | _ -> ()
+
+let rec matches_list_map_group_entry2'
+  (x: (Cbor.raw_data_item & Cbor.raw_data_item))
+  (unmatched: list bool)
+  (l: list map_group_entry)
+  (l': list bool { List.Tot.length l' == List.Tot.length l })
+: GTot (option (list bool))
+    (decreases l)
+= match l, l' with
+  | a :: q, true :: q' ->
+    if matches_map_group_entry a x
+    then Some (List.Tot.rev_acc (false :: unmatched) q')
+    else matches_list_map_group_entry2' x (true :: unmatched) q q'
+  | a :: q, false :: q' ->
+    matches_list_map_group_entry2' x (false :: unmatched) q q'
+  | _ -> None
+
+let rec matches_list_map_group_entry2'_correct
+  (x: (Cbor.raw_data_item & Cbor.raw_data_item))
+  (unmatched0: list map_group_entry)
+  (unmatched: list map_group_entry)
+  (unmatched': list bool)
+  (l0: list map_group_entry)
+  (l: list map_group_entry)
+  (l': list bool)
+: Lemma
+  (requires (
+    List.Tot.length unmatched' == List.Tot.length unmatched0 /\
+    unmatched == sieve_list unmatched0 unmatched' /\
+    List.Tot.length l' == List.Tot.length l0 /\
+    l == sieve_list l0 l'
+  ))
+  (ensures (
+    match matches_list_map_group_entry' x unmatched l, matches_list_map_group_entry2' x unmatched' l0 l' with
+    | None, None -> True
+    | Some q, Some q' ->
+      List.Tot.length q' == List.Tot.length (List.Tot.rev_acc unmatched0 l0) /\
+      q == sieve_list (List.Tot.rev_acc unmatched0 l0) q'
+    | _ -> False
+  ))
+  (decreases l0)
+= admit ()
+
+let matches_list_map_group_entry2
+  (x: (Cbor.raw_data_item & Cbor.raw_data_item))
+  (l: list map_group_entry)
+  (l': list bool { List.Tot.length l' == List.Tot.length l })
+: GTot (option (list bool))
+= matches_list_map_group_entry2' x [] l l'
+
+let matches_list_map_group_entry2_correct
+  (x: (Cbor.raw_data_item & Cbor.raw_data_item))
+  (l0: list map_group_entry)
+  (l: list map_group_entry)
+  (l': list bool)
+: Lemma
+  (requires (
+    List.Tot.length l' == List.Tot.length l0 /\
+    l == sieve_list l0 l'
+  ))
+  (ensures (
+    match matches_list_map_group_entry x l, matches_list_map_group_entry2 x l0 l' with
+    | None, None -> True
+    | Some q, Some q' ->
+      List.Tot.length q' == List.Tot.length l0 /\
+      q == sieve_list l0 q'
+    | _ -> False
+  ))
+= matches_list_map_group_entry2'_correct x [] [] [] l0 l l'
+
+let rec pts_to_list
+  (#t: Type)
+  (lr: list (R.ref t))
+  (lv: list t)
+: Tot vprop
+= match lr, lv with
+  | [], [] -> emp
+  | r :: lr', v :: lv' -> R.pts_to r full_perm v `star` pts_to_list lr' lv'
+  | _ -> pure (squash False)
+
+let rec pts_to_list_length
+  (#opened: _)
+  (#t: Type)
+  (lr: list (R.ref t))
+  (lv: list t)
+: STGhost unit opened
+    (pts_to_list lr lv)
+    (fun _ -> pts_to_list lr lv)
+    True
+    (fun _ -> List.Tot.length lr == List.Tot.length lv)
+    (decreases lr)
+= match lr, lv with
+  | [], [] -> noop ()
+  | r :: lr', v :: lv' ->
+    rewrite (pts_to_list lr lv) (R.pts_to r full_perm v `star` pts_to_list lr' lv');
+    pts_to_list_length lr' lv';
+    rewrite (R.pts_to r full_perm v `star` pts_to_list lr' lv') (pts_to_list lr lv)
+  | _ ->
+    rewrite (pts_to_list lr lv) (pure (squash False));
+    elim_pure (squash False);
+    rewrite emp (pts_to_list lr lv) // by contradiction
+
+let rec intro_pts_to_list_append
+  (#opened: _)
+  (#t: Type)
+  (lr1: list (R.ref t))
+  (lv1: list t)
+  (lr2: list (R.ref t))
+  (lv2: list t)
+: STGhostT unit opened
+    (pts_to_list lr1 lv1 `star` pts_to_list lr2 lv2)
+    (fun _ -> pts_to_list (lr1 `List.Tot.append` lr2) (lv1 `List.Tot.append` lv2))
+    (decreases lr1)
+= match lr1, lv1 with
+  | [], [] ->
+    rewrite (pts_to_list lr1 lv1) emp;
+    rewrite (pts_to_list lr2 lv2) (pts_to_list (lr1 `List.Tot.append` lr2) (lv1 `List.Tot.append` lv2))
+  | r :: lr', v :: lv' ->
+    rewrite (pts_to_list lr1 lv1) (R.pts_to r full_perm v `star` pts_to_list lr' lv');
+    intro_pts_to_list_append lr' lv' lr2 lv2;
+    rewrite
+      (R.pts_to r full_perm v `star` pts_to_list (lr' `List.Tot.append` lr2) (lv' `List.Tot.append` lv2))
+      (pts_to_list (lr1 `List.Tot.append` lr2) (lv1 `List.Tot.append` lv2))
+  | _ ->
+    rewrite (pts_to_list lr1 lv1) (pure (squash False));
+    elim_pure (squash False);
+    rewrite (pts_to_list lr2 lv2) (pts_to_list (lr1 `List.Tot.append` lr2) (lv1 `List.Tot.append` lv2)) // by contradiction
+
+let rec intro_pts_to_list_rev
+  (#opened: _)
+  (#t: Type)
+  (lr: list (R.ref t))
+  (lv: list t)
+: STGhostT unit opened
+    (pts_to_list lr lv)
+    (fun _ -> pts_to_list (List.Tot.rev lr) (List.Tot.rev lv))
+    (decreases lr)
+= match lr, lv with
+  | [], [] ->
+    rewrite (pts_to_list lr lv) (pts_to_list (List.Tot.rev lr) (List.Tot.rev lv))
+  | r :: lr', v :: lv' ->
+    rewrite (pts_to_list lr lv) (R.pts_to r full_perm v `star` pts_to_list lr' lv');
+    intro_pts_to_list_rev lr' lv';
+    List.Tot.rev_append [r] lr';
+    List.Tot.rev_append [v] lv';
+    rewrite (R.pts_to r full_perm v `star` emp) (pts_to_list (List.Tot.rev [r]) (List.Tot.rev [v]));
+    intro_pts_to_list_append (List.Tot.rev lr') (List.Tot.rev lv') (List.Tot.rev [r]) (List.Tot.rev [v]);
+    rewrite (pts_to_list _ _) (pts_to_list (List.Tot.rev lr) (List.Tot.rev lv))
+  | _ ->
+    rewrite (pts_to_list lr lv) (pure (squash False));
+    elim_pure (squash False);
+    rewrite emp (pts_to_list (List.Tot.rev lr) (List.Tot.rev lv)) // by contradiction
+
+let rec elim_pts_to_list_append
+  (#opened: _)
+  (#t: Type)
+  (lr1: list (R.ref t))
+  (lv1: list t)
+  (lr2: list (R.ref t))
+  (lv2: list t)
+: STGhost unit opened
+    (pts_to_list (lr1 `List.Tot.append` lr2) (lv1 `List.Tot.append` lv2))
+    (fun _ -> pts_to_list lr1 lv1 `star` pts_to_list lr2 lv2)
+    (List.Tot.length lr1 == List.Tot.length lv1)
+    (fun _ -> True)
+    (decreases lr1)
+= match lr1, lv1 with
+  | [], [] ->
+    rewrite (pts_to_list (lr1 `List.Tot.append` lr2) (lv1 `List.Tot.append` lv2)) (pts_to_list lr2 lv2);
+    rewrite emp (pts_to_list lr1 lv1)
+  | r :: lr', v :: lv' ->
+    rewrite (pts_to_list (lr1 `List.Tot.append` lr2) (lv1 `List.Tot.append` lv2))
+      (R.pts_to r full_perm v `star` pts_to_list (lr' `List.Tot.append` lr2) (lv' `List.Tot.append` lv2));
+    elim_pts_to_list_append lr' lv' lr2 lv2;
+    rewrite
+      (R.pts_to r full_perm v `star` pts_to_list lr' lv')
+      (pts_to_list lr1 lv1)
+
+inline_for_extraction [@@noextract_to "krml"]
+let impl_matches_list_map_group_entry2'_t
+  (l: list map_group_entry)
+  (lr: list (R.ref bool))
+: Tot Type
+= (gx1: v Cbor.parse_raw_data_item_kind Cbor.raw_data_item) ->
+  (gx2: v Cbor.parse_raw_data_item_kind Cbor.raw_data_item) ->
+  (x1: byte_array) ->
+  (x2: byte_array) ->
+  (unmatched_r: Ghost.erased (list (R.ref bool))) ->
+  (unmatched: Ghost.erased (list bool)) ->
+  (l': Ghost.erased (list bool) { List.Tot.length l' == List.Tot.length l }) ->
+  STT (option (R.ref bool))
+    (pts_to_list unmatched_r unmatched `star`
+      pts_to_list lr l' `star`
+      aparse Cbor.parse_raw_data_item x1 gx1 `star`
+      aparse Cbor.parse_raw_data_item x2 gx2
+    )
+    (fun res ->
+      aparse Cbor.parse_raw_data_item x1 gx1 `star`
+      aparse Cbor.parse_raw_data_item x2 gx2 `star`
+      begin match res with
+      | None ->
+        pts_to_list unmatched_r unmatched `star`
+        pts_to_list lr l' `star`
+        pure (matches_list_map_group_entry2' (gx1.contents, gx2.contents) unmatched l l' == None)
+      | Some r' ->
+        exists_ (fun lrl -> exists_ (fun lrr -> exists_ (fun lvl -> exists_ (fun lvr ->
+          pts_to_list lrl lvl `star`
+          pts_to_list lrr lvr `star`
+          R.pts_to r' full_perm false `star`
+          pure (
+            matches_list_map_group_entry2' (gx1.contents, gx2.contents) unmatched l l' == Some (lvl `List.Tot.append` (false :: lvr)) /\
+            Ghost.reveal unmatched `List.Tot.append` Ghost.reveal l' == lvl `List.Tot.append` (true :: lvr)
+          )
+        ))))
+      end
+    )
+