array iterator share, gather

src/cbor/pulse/CBOR.Pulse.API.Det.Common.fsti

@@ -258,6 +258,10 @@ val cbor_det_array_iterator_next () : array_iterator_next_t cbor_det_match cbor_
 
 val cbor_det_array_iterator_truncate () : array_iterator_truncate_t cbor_det_array_iterator_match
 
+val cbor_det_array_iterator_share () : array_iterator_share_t cbor_det_array_iterator_match
+
+val cbor_det_array_iterator_gather () : array_iterator_gather_t cbor_det_array_iterator_match
+
 val cbor_det_get_array_item () : get_array_item_t cbor_det_match
 
 val cbor_det_get_map_length () : get_map_length_t cbor_det_match

src/cbor/pulse/raw/CBOR.Pulse.API.Det.Common.fst

@@ -1053,6 +1053,36 @@ fn cbor_det_array_iterator_truncate (_: unit) : array_iterator_truncate_t u#0 #_
 }
 ```
 
+```pulse
+ghost
+fn cbor_det_array_iterator_share (_: unit) : array_iterator_share_t u#0 #_ cbor_det_array_iterator_match
+= (x: _)
+  (#py: _)
+  (#z: _)
+{
+  unfold (cbor_det_array_iterator_match py x z);
+  Read.cbor_array_iterator_share x;
+  fold (cbor_det_array_iterator_match (py /. 2.0R) x z);
+  fold (cbor_det_array_iterator_match (py /. 2.0R) x z);
+}
+```
+
+```pulse
+ghost
+fn cbor_det_array_iterator_gather (_: unit) : array_iterator_gather_t u#0 #_ cbor_det_array_iterator_match
+= (x: _)
+  (#py1: _)
+  (#z1: _)
+  (#py2: _)
+  (#z2: _)
+{
+  unfold (cbor_det_array_iterator_match py1 x z1);
+  unfold (cbor_det_array_iterator_match py2 x z2);
+  Read.cbor_array_iterator_gather x #py1 #_ #py2 #_;
+  fold (cbor_det_array_iterator_match (py1 +. py2) x z1);
+}
+```
+
 let rec list_index_map
   (#t1 #t2: Type)
   (f: (t1 -> t2))

src/cbor/pulse/raw/CBOR.Pulse.Raw.Format.Serialized.fsti

@@ -71,6 +71,10 @@ val cbor_serialized_array_iterator_next (_: squash SZ.fits_u64) : cbor_raw_seria
 
 val cbor_serialized_array_iterator_truncate : cbor_raw_serialized_iterator_truncate_t cbor_serialized_array_iterator_match
 
+val cbor_serialized_array_iterator_share : cbor_raw_serialized_iterator_share_t cbor_serialized_array_iterator_match
+
+val cbor_serialized_array_iterator_gather : cbor_raw_serialized_iterator_gather_t cbor_serialized_array_iterator_match
+
 val cbor_serialized_map_iterator_match
   (p: perm)
   (i: cbor_raw_serialized_iterator)

src/cbor/pulse/raw/CBOR.Pulse.Raw.Iterator.fst

@@ -663,6 +663,205 @@ decreases r
 }
 ```
 
+inline_for_extraction
+let cbor_raw_serialized_iterator_share_t
+  (#elt_high: Type0)
+  (ser_match: perm -> cbor_raw_serialized_iterator -> list elt_high -> slprop)
+=
+  (c: cbor_raw_serialized_iterator) ->
+  (#pm: perm) ->
+  (#r: (list elt_high)) ->
+  stt_ghost unit emp_inames
+    (ser_match pm c r)
+    (fun _ ->
+      ser_match (pm /. 2.0R) c r **
+      ser_match (pm /. 2.0R) c r
+    )
+
+```pulse
+ghost
+fn cbor_raw_iterator_share
+  (#elt_low #elt_high: Type0)
+  (elt_match: perm -> elt_low -> elt_high -> slprop)
+  (elt_share: (
+    (p': perm) ->
+    (c': elt_low) ->
+    (r': elt_high) ->
+    stt_ghost unit emp_inames
+      (elt_match p' c' r')
+      (fun _ -> elt_match (p' /. 2.0R) c' r' **
+        elt_match (p' /. 2.0R) c' r'
+      )
+  ))
+  (#ser_match: perm -> cbor_raw_serialized_iterator -> list elt_high -> slprop)
+  (phi: cbor_raw_serialized_iterator_share_t ser_match)
+  (c: cbor_raw_iterator elt_low)
+  (#pm: perm)
+  (#r: (list elt_high))
+requires
+    cbor_raw_iterator_match elt_match ser_match pm c r
+ensures
+    cbor_raw_iterator_match elt_match ser_match (pm /. 2.0R) c r **
+    cbor_raw_iterator_match elt_match ser_match (pm /. 2.0R) c r
+{
+  match c {
+    CBOR_Raw_Iterator_Slice c' -> {
+      rewrite (cbor_raw_iterator_match elt_match ser_match pm c r)
+        as (cbor_raw_slice_iterator_match elt_match pm c' r);
+      unfold (cbor_raw_slice_iterator_match elt_match pm c' r);
+      with cs . assert (pts_to c'.s #(pm *. c'.slice_perm) cs);
+      S.share c'.s;
+      cbor_raw_share_slice elt_match (pm *. c'.payload_perm) cs r elt_share ();
+      half_mul_l pm c'.slice_perm;
+      half_mul_l pm c'.payload_perm;
+      fold (cbor_raw_slice_iterator_match elt_match (pm /. 2.0R) c' r);
+      rewrite (cbor_raw_slice_iterator_match elt_match (pm /. 2.0R) c' r)
+        as (cbor_raw_iterator_match elt_match ser_match (pm /. 2.0R) c r);
+      fold (cbor_raw_slice_iterator_match elt_match (pm /. 2.0R) c' r);
+      rewrite (cbor_raw_slice_iterator_match elt_match (pm /. 2.0R) c' r)
+        as (cbor_raw_iterator_match elt_match ser_match (pm /. 2.0R) c r);
+    }
+    CBOR_Raw_Iterator_Serialized c' -> {
+      rewrite (cbor_raw_iterator_match elt_match ser_match pm c r)
+        as (ser_match pm c' r);
+      phi c';
+      rewrite (ser_match (pm /. 2.0R) c' r)
+        as (cbor_raw_iterator_match elt_match ser_match (pm /. 2.0R) c r);
+      rewrite (ser_match (pm /. 2.0R) c' r)
+        as (cbor_raw_iterator_match elt_match ser_match (pm /. 2.0R) c r);
+    }
+  }
+}
+```
+
+```pulse
+ghost
+fn rec cbor_raw_gather_slice
+  (#elt_low #elt_high: Type0)
+  (elt_match: perm -> elt_low -> elt_high -> slprop)
+  (p1: perm)
+  (c: Seq.seq elt_low)
+  (r1: list elt_high)
+  (p2: perm)
+  (r2: list elt_high)
+  (elt_gather: (
+    (p1': perm) ->
+    (c': elt_low) ->
+    (r1': elt_high) ->
+    (p2': perm) ->
+    (r2': elt_high { r1' << r1 }) ->
+    stt_ghost unit emp_inames
+      (elt_match p1' c' r1' ** elt_match p2' c' r2')
+      (fun _ -> elt_match (p1' +. p2') c' r1' **
+        pure (r1' == r2')
+      )
+  ))
+  (_: unit)
+requires
+  PM.seq_list_match c r1 (elt_match p1) **
+  PM.seq_list_match c r2 (elt_match p2)
+ensures
+  PM.seq_list_match c r1 (elt_match (p1 +. p2)) **
+  pure (r1 == r2)
+decreases r1
+{
+  PM.seq_list_match_length (elt_match p1) c r1;
+  PM.seq_list_match_length (elt_match p2) c r2;
+  match r1 {
+    Nil -> {
+      PM.seq_list_match_nil_elim c r1 (elt_match p1);
+      PM.seq_list_match_nil_elim c r2 (elt_match p2);
+      PM.seq_list_match_nil_intro c r1 (elt_match (p1 +. p2));
+    }
+    a :: q -> {
+      PM.seq_list_match_cons_elim c r1 (elt_match p1);
+      PM.seq_list_match_cons_elim c r2 (elt_match p2);
+      elt_gather p1 (Seq.head c) (List.Tot.hd r1) p2 (List.Tot.hd r2);
+      cbor_raw_gather_slice elt_match p1 (Seq.tail c) q p2 (List.Tot.tl r2) elt_gather ();
+      PM.seq_list_match_cons_intro (Seq.head c) (List.Tot.hd r1) (Seq.tail c) q (elt_match (p1 +. p2));
+    }
+  }
+}
+```
+
+inline_for_extraction
+let cbor_raw_serialized_iterator_gather_t
+  (#elt_high: Type0)
+  (ser_match: perm -> cbor_raw_serialized_iterator -> list elt_high -> slprop)
+=
+  (c: cbor_raw_serialized_iterator) ->
+  (#pm1: perm) ->
+  (#r1: (list elt_high)) ->
+  (#pm2: perm) ->
+  (#r2: (list elt_high)) ->
+  stt_ghost unit emp_inames
+    (ser_match pm1 c r1 ** ser_match pm2 c r2)
+    (fun _ ->
+      ser_match (pm1 +. pm2) c r1 **
+      pure (r1 == r2)
+    )
+
+```pulse
+ghost
+fn cbor_raw_iterator_gather
+  (#elt_low #elt_high: Type0)
+  (elt_match: perm -> elt_low -> elt_high -> slprop)
+  (elt_gather: (
+    (p1': perm) ->
+    (c': elt_low) ->
+    (r1': elt_high) ->
+    (p2': perm) ->
+    (r2': elt_high) ->
+    stt_ghost unit emp_inames
+      (elt_match p1' c' r1' ** elt_match p2' c' r2')
+      (fun _ -> elt_match (p1' +. p2') c' r1' **
+        pure (r1' == r2')
+      )
+  ))
+  (#ser_match: perm -> cbor_raw_serialized_iterator -> list elt_high -> slprop)
+  (phi: cbor_raw_serialized_iterator_gather_t ser_match)
+  (c: cbor_raw_iterator elt_low)
+  (#pm1: perm)
+  (#r1: (list elt_high))
+  (#pm2: perm)
+  (#r2: (list elt_high))
+requires
+    cbor_raw_iterator_match elt_match ser_match pm1 c r1 **
+    cbor_raw_iterator_match elt_match ser_match pm2 c r2
+ensures
+    cbor_raw_iterator_match elt_match ser_match (pm1 +. pm2) c r1 **
+    pure (r1 == r2)
+{
+  match c {
+    CBOR_Raw_Iterator_Slice c' -> {
+      rewrite (cbor_raw_iterator_match elt_match ser_match pm1 c r1)
+        as (cbor_raw_slice_iterator_match elt_match pm1 c' r1);
+      unfold (cbor_raw_slice_iterator_match elt_match pm1 c' r1);
+      rewrite (cbor_raw_iterator_match elt_match ser_match pm2 c r2)
+        as (cbor_raw_slice_iterator_match elt_match pm2 c' r2);
+      unfold (cbor_raw_slice_iterator_match elt_match pm2 c' r2);
+      S.gather c'.s;
+      perm_mul_add_l pm1 pm2 c'.slice_perm;
+      with cs . assert (pts_to c'.s #((pm1 +. pm2) *. c'.slice_perm) cs);
+      cbor_raw_gather_slice elt_match (pm1 *. c'.payload_perm) cs r1 (pm2 *. c'.payload_perm) r2 elt_gather ();
+      perm_mul_add_l pm1 pm2 c'.payload_perm;
+      fold (cbor_raw_slice_iterator_match elt_match (pm1 +. pm2) c' r1);
+      rewrite (cbor_raw_slice_iterator_match elt_match (pm1 +. pm2) c' r1)
+        as (cbor_raw_iterator_match elt_match ser_match (pm1 +. pm2) c r1);
+    }
+    CBOR_Raw_Iterator_Serialized c' -> {
+      rewrite (cbor_raw_iterator_match elt_match ser_match pm1 c r1)
+        as (ser_match pm1 c' r1);
+      rewrite (cbor_raw_iterator_match elt_match ser_match pm2 c r2)
+        as (ser_match pm2 c' r2);
+      phi c' #pm1 #r1 #pm2 #r2;
+      rewrite (ser_match (pm1 +. pm2) c' r1)
+        as (cbor_raw_iterator_match elt_match ser_match (pm1 +. pm2) c r1);
+    }
+  }
+}
+```
+
 let rec seq_of_list_splitAt
   (#t: Type)
   (l: list t)

src/cbor/pulse/raw/CBOR.Pulse.Raw.Read.fst

@@ -287,6 +287,58 @@ ensures
 }
 ```
 
+module Perm = CBOR.Pulse.Raw.Match.Perm
+
+```pulse
+ghost
+fn cbor_array_iterator_share
+  (c: cbor_array_iterator)
+  (#pm: perm)
+  (#r: (list raw_data_item))
+requires
+    cbor_array_iterator_match pm c r
+ensures
+    cbor_array_iterator_match (pm /. 2.0R) c r **
+    cbor_array_iterator_match (pm /. 2.0R) c r
+{
+  unfold (cbor_array_iterator_match pm c r);
+  cbor_raw_iterator_share
+    cbor_match
+    Perm.cbor_raw_share
+    cbor_serialized_array_iterator_share
+    c;
+  fold (cbor_array_iterator_match (pm /. 2.0R) c r);
+  fold (cbor_array_iterator_match (pm /. 2.0R) c r);
+}
+```
+
+```pulse
+ghost
+fn cbor_array_iterator_gather
+  (c: cbor_array_iterator)
+  (#pm1: perm)
+  (#r1: (list raw_data_item))
+  (#pm2: perm)
+  (#r2: (list raw_data_item))
+requires
+    cbor_array_iterator_match pm1 c r1 **
+    cbor_array_iterator_match pm2 c r2
+ensures
+    cbor_array_iterator_match (pm1 +. pm2) c r1 **
+    pure (r1 == r2)
+{
+  unfold (cbor_array_iterator_match pm1 c r1);
+  unfold (cbor_array_iterator_match pm2 c r2);
+  cbor_raw_iterator_gather
+    cbor_match
+    Perm.cbor_raw_gather
+    cbor_serialized_array_iterator_gather
+    c
+    #pm1 #r1 #pm2 #r2;
+  fold (cbor_array_iterator_match (pm1 +. pm2) c r1);
+}
+```
+
 ```pulse
 ghost
 fn cbor_match_map_elim

src/cbor/pulse/raw/everparse/CBOR.Pulse.Raw.EverParse.Iterator.fst

@@ -327,3 +327,46 @@ fn cbor_raw_serialized_iterator_truncate
   c'
 }
 ```
+
+```pulse
+ghost
+fn cbor_raw_serialized_iterator_share
+  (#elt_high: Type0)
+  (#k: LP.parser_kind)
+  (#p: LP.parser k elt_high)
+  (s: LP.serializer p { (k).parser_kind_subkind == Some LP.ParserStrong /\ (k).parser_kind_low > 0 })
+: cbor_raw_serialized_iterator_share_t #elt_high (cbor_raw_serialized_iterator_match s)
+=
+  (c: _)
+  (#pm: perm)
+  (#l: (list elt_high))
+{
+  unfold (cbor_raw_serialized_iterator_match s pm c l);
+  LP.pts_to_serialized_share (LP.serialize_nlist (c.glen) s) c.s;
+  fold (cbor_raw_serialized_iterator_match s (pm /. 2.0R) c l);
+  fold (cbor_raw_serialized_iterator_match s (pm /. 2.0R) c l);
+}
+```
+
+```pulse
+ghost
+fn cbor_raw_serialized_iterator_gather
+  (#elt_high: Type0)
+  (#k: LP.parser_kind)
+  (#p: LP.parser k elt_high)
+  (s: LP.serializer p { (k).parser_kind_subkind == Some LP.ParserStrong /\ (k).parser_kind_low > 0 })
+: cbor_raw_serialized_iterator_gather_t #elt_high (cbor_raw_serialized_iterator_match s)
+=
+  (c: _)
+  (#pm1: perm)
+  (#l1: (list elt_high))
+  (#pm2: perm)
+  (#l2: (list elt_high))
+{
+  unfold (cbor_raw_serialized_iterator_match s pm1 c l1);
+  unfold (cbor_raw_serialized_iterator_match s pm2 c l2);
+  LP.pts_to_serialized_gather (LP.serialize_nlist (c.glen) s) c.s;
+  perm_mul_add_l pm1 pm2 c.p;
+  fold (cbor_raw_serialized_iterator_match s (pm1 +. pm2) c l1);
+}
+```

src/cbor/pulse/raw/everparse/CBOR.Pulse.Raw.Format.Serialized.fst

@@ -193,6 +193,10 @@ let cbor_serialized_array_iterator_next sq = cbor_raw_serialized_iterator_next _
 
 let cbor_serialized_array_iterator_truncate = cbor_raw_serialized_iterator_truncate serialize_raw_data_item
 
+let cbor_serialized_array_iterator_share = cbor_raw_serialized_iterator_share serialize_raw_data_item
+
+let cbor_serialized_array_iterator_gather = cbor_raw_serialized_iterator_gather serialize_raw_data_item
+
 let cbor_serialized_map_iterator_match = cbor_raw_serialized_iterator_match (serialize_nondep_then serialize_raw_data_item serialize_raw_data_item)
 
 module LP = LowParse.Pulse.VCList