array iterator length

src/cbor/pulse/CBOR.Pulse.API.Base.fst

@@ -338,6 +338,17 @@ let array_iterator_is_empty_t
     (iter p x y)
     (fun res -> iter p x y ** pure (res == Nil? y))
 
+inline_for_extraction
+let array_iterator_length_t
+  (#t': Type)
+  (iter: perm -> t' -> list cbor -> slprop)
+= (x: t') ->
+  (#p: perm) ->
+  (#y: Ghost.erased (list cbor)) ->
+  stt U64.t
+    (iter p x y)
+    (fun res -> iter p x y ** pure (U64.v res == List.Tot.length y))
+
 inline_for_extraction
 let array_iterator_next_t
   (#t #t': Type)

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

@@ -254,6 +254,8 @@ val cbor_det_array_iterator_start () : array_iterator_start_t cbor_det_match cbo
 
 val cbor_det_array_iterator_is_empty () : array_iterator_is_empty_t cbor_det_array_iterator_match
 
+val cbor_det_array_iterator_length () : array_iterator_length_t cbor_det_array_iterator_match
+
 val cbor_det_array_iterator_next () : array_iterator_next_t cbor_det_match cbor_det_array_iterator_match
 
 val cbor_det_array_iterator_truncate () : array_iterator_truncate_t cbor_det_array_iterator_match

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

@@ -993,6 +993,19 @@ fn cbor_det_array_iterator_is_empty (_: unit) : array_iterator_is_empty_t u#0 #_
 }
 ```
 
+```pulse
+fn cbor_det_array_iterator_length (_: unit) : array_iterator_length_t u#0 #_ cbor_det_array_iterator_match
+= (x: _)
+  (#p: _)
+  (#v: _)
+{
+  unfold (cbor_det_array_iterator_match p x v);
+  let res = Read.cbor_array_iterator_length x;
+  fold (cbor_det_array_iterator_match p x v);
+  res
+}
+```
+
 ```pulse
 fn cbor_det_array_iterator_next (_: unit) : array_iterator_next_t u#0 #_ #_ cbor_det_match cbor_det_array_iterator_match
 = (x: _)

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

@@ -67,6 +67,8 @@ val cbor_serialized_array_iterator_init
 
 val cbor_serialized_array_iterator_is_empty : cbor_raw_serialized_iterator_is_empty_t cbor_serialized_array_iterator_match
 
+val cbor_serialized_array_iterator_length : cbor_raw_serialized_iterator_length_t cbor_serialized_array_iterator_match
+
 val cbor_serialized_array_iterator_next (_: squash SZ.fits_u64) : cbor_raw_serialized_iterator_next_t cbor_match cbor_serialized_array_iterator_match
 
 val cbor_serialized_array_iterator_truncate : cbor_raw_serialized_iterator_truncate_t cbor_serialized_array_iterator_match

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

@@ -15,6 +15,7 @@ module U64 = FStar.UInt64
 noeq
 type cbor_raw_slice_iterator (elt: Type0) = {
   s: Pulse.Lib.Slice.slice elt;
+  sq: squash (SZ.v (S.len s) < pow2 64);
   slice_perm: perm;
   payload_perm: perm;
 }
@@ -131,6 +132,7 @@ ensures exists* p .
 {
   let c : cbor_raw_slice_iterator elt_low = {
     s = a;
+    sq = ();
     slice_perm = 1.0R;
     payload_perm = pm' `perm_div` pm;
   };
@@ -174,6 +176,30 @@ ensures
 }
 ```
 
+inline_for_extraction
+```pulse
+fn cbor_raw_slice_iterator_length
+  (#elt_low #elt_high: Type0)
+  (elt_match: perm -> elt_low -> elt_high -> slprop)
+  (c: cbor_raw_slice_iterator elt_low)
+  (#pm: perm)
+  (#r: Ghost.erased (list elt_high))
+requires
+    cbor_raw_slice_iterator_match elt_match pm c r
+returns res: U64.t
+ensures
+    cbor_raw_slice_iterator_match elt_match pm c r **
+    pure (List.Tot.length r == U64.v res)
+{
+  unfold (cbor_raw_slice_iterator_match elt_match pm c r);
+  PM.seq_list_match_length (elt_match (pm `perm_mul` c.payload_perm)) _ _;
+  Pulse.Lib.Slice.pts_to_len c.s;
+  let res = (SZ.sizet_to_uint64 (S.len c.s));
+  fold (cbor_raw_slice_iterator_match elt_match pm c r);
+  res
+}
+```
+
 noeq
 type cbor_raw_iterator (elt: Type0) =
 | CBOR_Raw_Iterator_Slice of cbor_raw_slice_iterator elt
@@ -278,11 +304,13 @@ ensures
 {
   cbor_raw_slice_iterator_match_unfold elt_match pm i l; // 1: (pts_to i.s _ ** PM.seq_list_match _ l _) @==> cbor_raw_slice_iterator_match elt_match pm i l
   with sq . assert (pts_to i.s #(pm `perm_mul` i.slice_perm) sq);
+  S.pts_to_len i.s;
   PM.seq_list_match_length (elt_match (pm `perm_mul` i.payload_perm)) _ _;
   let res = Pulse.Lib.Slice.op_Array_Access i.s 0sz;
   PM.seq_list_match_cons_elim_trade _ l (elt_match (pm `perm_mul` i.payload_perm)); // 2: (elt_match _ (List.Tot.hd l) ** PM.seq_list_match _ (List.Tot.tl l) _) @==> PM.seq_list_match _ l _
 //  assert (elt_match (pm `perm_mul` i.payload_perm) res (List.Tot.hd l)); // FIXME: make this work, without the need for `rewrite ... sq`, see below
   let s' = slice_split_right i.s 1sz; // 3: pts_to s' _ @==> pts_to i.s _
+  S.pts_to_len s';
   let i1 = { i with s = s' };
   let i' = { i1 with slice_perm = i.slice_perm /. 2.0R };
   pi := CBOR_Raw_Iterator_Slice i';
@@ -409,6 +437,58 @@ ensures
 }
 ```
 
+inline_for_extraction
+let cbor_raw_serialized_iterator_length_t
+  (#elt_high: Type0)
+  (ser_match: perm -> cbor_raw_serialized_iterator -> list elt_high -> slprop)
+=
+  (c: cbor_raw_serialized_iterator) ->
+  (#pm: perm) ->
+  (#r: Ghost.erased (list elt_high)) ->
+  stt U64.t
+    (ser_match pm c r)
+    (fun res -> ser_match pm c r **
+      pure ((U64.v res <: nat) == List.Tot.length r)
+    )
+
+inline_for_extraction
+```pulse
+fn cbor_raw_iterator_length
+  (#elt_low #elt_high: Type0)
+  (elt_match: perm -> elt_low -> elt_high -> slprop)
+  (ser_match: perm -> cbor_raw_serialized_iterator -> list elt_high -> slprop)
+  (phi: cbor_raw_serialized_iterator_length_t ser_match)
+  (c: cbor_raw_iterator elt_low)
+  (#pm: perm)
+  (#r: Ghost.erased (list elt_high))
+requires
+    cbor_raw_iterator_match elt_match ser_match pm c r
+returns res: U64.t
+ensures
+    cbor_raw_iterator_match elt_match ser_match pm c r **
+    pure ((U64.v res <: nat) == List.Tot.length 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);
+      let res = cbor_raw_slice_iterator_length elt_match c';
+      rewrite (cbor_raw_slice_iterator_match elt_match pm c' r)
+        as (cbor_raw_iterator_match elt_match ser_match pm c r);
+      res
+    }
+    CBOR_Raw_Iterator_Serialized c' -> {
+      rewrite (cbor_raw_iterator_match elt_match ser_match pm c r)
+        as (ser_match pm c' r);
+      let res = phi c';
+      rewrite (ser_match pm c' r)
+        as (cbor_raw_iterator_match elt_match ser_match pm c r);
+      res
+    }
+  }
+}
+```
+
 inline_for_extraction
 let cbor_raw_serialized_iterator_next_t
   (#elt_low #elt_high: Type0)
@@ -585,10 +665,12 @@ ensures
       Trade.trans_hyp_r _ _ _ (cbor_raw_iterator_match elt_match ser_match pm c r);
       assume (pure (SZ.fits_u64));
       let Mktuple2 sl1 sl2 = S.split_trade c'.s (SZ.uint64_to_sizet len);
+      S.pts_to_len sl1;
       Trade.elim_hyp_r _ _ (pts_to c'.s #(pm `perm_mul` c'.slice_perm) s);
       Trade.trans_hyp_l _ _ _ (cbor_raw_iterator_match elt_match ser_match pm c r);
       let c1 = {
         s = sl1;
+        sq = ();
         slice_perm = pm `perm_mul` c'.slice_perm;
         payload_perm = pm `perm_mul` c'.payload_perm;
       };

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

@@ -226,6 +226,29 @@ ensures
 }
 ```
 
+```pulse
+fn cbor_array_iterator_length
+  (c: cbor_array_iterator)
+  (#pm: perm)
+  (#r: Ghost.erased (list raw_data_item))
+requires
+    cbor_array_iterator_match pm c r
+returns res: U64.t
+ensures
+    cbor_array_iterator_match pm c r **
+    pure ((U64.v res <: nat) == List.Tot.length r)
+{
+  unfold (cbor_array_iterator_match pm c r);
+  let res = cbor_raw_iterator_length
+    cbor_match
+    cbor_serialized_array_iterator_match
+    cbor_serialized_array_iterator_length
+    c;
+  fold (cbor_array_iterator_match pm c r);
+  res
+}
+```
+
 ```pulse
 fn cbor_array_iterator_next
   (sq: squash SZ.fits_u64)

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

@@ -181,6 +181,26 @@ fn cbor_raw_serialized_iterator_is_empty
 }
 ```
 
+inline_for_extraction
+```pulse
+fn cbor_raw_serialized_iterator_length
+  (#elt_high: Type0)
+  (#k: Ghost.erased LP.parser_kind)
+  (#p: LP.parser k elt_high)
+  (s: LP.serializer p { (Ghost.reveal k).parser_kind_subkind == Some LP.ParserStrong /\ (Ghost.reveal k).parser_kind_low > 0 })
+: cbor_raw_serialized_iterator_length_t #elt_high (cbor_raw_serialized_iterator_match s)
+= (c: cbor_raw_serialized_iterator)
+  (#pm: perm)
+  (#l: Ghost.erased (list elt_high))
+{
+  cbor_raw_serialized_iterator_unfold s pm c l;
+  with l' . assert (LP.pts_to_serialized (LP.serialize_nlist c.glen s) c.s #(pm *. c.p) l');
+  CBOR.Spec.Util.list_splitAt_length (U64.v c.len) l';
+  Trade.elim _ _;
+  c.len
+}
+```
+
 let cbor_raw_serialized_iterator_next_cont
   (#elt_low #elt_high: Type0)
   (#k: LP.parser_kind)

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

@@ -180,6 +180,8 @@ ensures
 
 let cbor_serialized_array_iterator_is_empty = cbor_raw_serialized_iterator_is_empty _
 
+let cbor_serialized_array_iterator_length = cbor_raw_serialized_iterator_length _
+
 inline_for_extraction
 ```pulse
 fn cbor_serialized_array_iterator_next_cont (_: unit)