cbordet snap

project-everest · Jan 30, 2025 · 1a26d7f · 1a26d7f
1 parent 46e3e27
commit 1a26d7f
Show file tree

Hide file tree

Showing 3 changed files with 83 additions and 0 deletions.
diff --git a/src/cbor/pulse/det/c/CBORDet.c b/src/cbor/pulse/det/c/CBORDet.c
@@ -1387,6 +1387,14 @@ cbor_serialized_array_iterator_is_empty(
   return c.len == 0ULL;
 }
 
+static uint64_t
+cbor_serialized_array_iterator_length(
+  CBOR_Pulse_Raw_Iterator_Base_cbor_raw_serialized_iterator c
+)
+{
+  return c.len;
+}
+
 static cbor_raw
 cbor_serialized_array_iterator_next(
   CBOR_Pulse_Raw_Iterator_cbor_raw_iterator__CBOR_Pulse_Raw_Type_cbor_raw *pi,
@@ -1633,6 +1641,35 @@ cbor_array_iterator_is_empty(
   }
 }
 
+static uint64_t
+cbor_array_iterator_length(
+  CBOR_Pulse_Raw_Iterator_cbor_raw_iterator__CBOR_Pulse_Raw_Type_cbor_raw c
+)
+{
+  if (c.tag == CBOR_Pulse_Raw_Iterator_CBOR_Raw_Iterator_Slice)
+  {
+    Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw c_ = c.case_CBOR_Raw_Iterator_Slice;
+    uint64_t res = (uint64_t)len__CBOR_Pulse_Raw_Type_cbor_raw(c_);
+    uint64_t res0 = res;
+    return res0;
+  }
+  else if (c.tag == CBOR_Pulse_Raw_Iterator_CBOR_Raw_Iterator_Serialized)
+  {
+    CBOR_Pulse_Raw_Iterator_Base_cbor_raw_serialized_iterator
+    c_ = c.case_CBOR_Raw_Iterator_Serialized;
+    uint64_t res = cbor_serialized_array_iterator_length(c_);
+    return res;
+  }
+  else
+  {
+    KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
+      __FILE__,
+      __LINE__,
+      "unreachable (pattern matches are exhaustive in F*)");
+    KRML_HOST_EXIT(255U);
+  }
+}
+
 typedef struct
 __Pulse_Lib_Slice_slice_CBOR_Pulse_Raw_Type_cbor_raw_Pulse_Lib_Slice_slice_CBOR_Pulse_Raw_Type_cbor_raw_s
 {
@@ -5204,6 +5241,15 @@ cbor_det_array_iterator_is_empty(
   return res;
 }
 
+uint64_t
+cbor_det_array_iterator_length(
+  CBOR_Pulse_Raw_Iterator_cbor_raw_iterator__CBOR_Pulse_Raw_Type_cbor_raw x
+)
+{
+  uint64_t res = cbor_array_iterator_length(x);
+  return res;
+}
+
 cbor_raw
 cbor_det_array_iterator_next(
   CBOR_Pulse_Raw_Iterator_cbor_raw_iterator__CBOR_Pulse_Raw_Type_cbor_raw *x

diff --git a/src/cbor/pulse/det/c/CBORDet.h b/src/cbor/pulse/det/c/CBORDet.h
@@ -292,6 +292,11 @@ cbor_det_array_iterator_is_empty(
   CBOR_Pulse_Raw_Iterator_cbor_raw_iterator__CBOR_Pulse_Raw_Type_cbor_raw x
 );
 
+uint64_t
+cbor_det_array_iterator_length(
+  CBOR_Pulse_Raw_Iterator_cbor_raw_iterator__CBOR_Pulse_Raw_Type_cbor_raw x
+);
+
 cbor_raw
 cbor_det_array_iterator_next(
   CBOR_Pulse_Raw_Iterator_cbor_raw_iterator__CBOR_Pulse_Raw_Type_cbor_raw *x

diff --git a/src/cbor/pulse/det/rust/src/cbordetveraux.rs b/src/cbor/pulse/det/rust/src/cbordetveraux.rs
@@ -1380,6 +1380,9 @@ fn cbor_serialized_array_iterator_init <'a>(c: cbor_serialized <'a>) ->
 fn cbor_serialized_array_iterator_is_empty <'a>(c: cbor_raw_serialized_iterator <'a>) -> bool
 { c.len == 0u64 }
 
+fn cbor_serialized_array_iterator_length <'a>(c: cbor_raw_serialized_iterator <'a>) -> u64
+{ c.len }
+
 #[derive(PartialEq, Clone, Copy)]
 enum cbor_raw_iterator__CBOR_Pulse_Raw_Type_cbor_raw_tags
 {
@@ -1593,6 +1596,26 @@ fn cbor_array_iterator_is_empty <'a>(c: cbor_raw_iterator__CBOR_Pulse_Raw_Type_c
     }
 }
 
+fn cbor_array_iterator_length <'a>(c: cbor_raw_iterator__CBOR_Pulse_Raw_Type_cbor_raw <'a>) ->
+    u64
+{
+    match c
+    {
+        cbor_raw_iterator__CBOR_Pulse_Raw_Type_cbor_raw::CBOR_Raw_Iterator_Slice { _0: c· } =>
+          {
+              let res: u64 = c·.len() as u64;
+              let res0: u64 = res;
+              res0
+          },
+        cbor_raw_iterator__CBOR_Pulse_Raw_Type_cbor_raw::CBOR_Raw_Iterator_Serialized { _0: c· } =>
+          {
+              let res: u64 = cbor_serialized_array_iterator_length(c·);
+              res
+          },
+        _ => panic!("Incomplete pattern matching")
+    }
+}
+
 fn cbor_array_iterator_next <'b, 'a>(
     pi: &'b mut [cbor_raw_iterator__CBOR_Pulse_Raw_Type_cbor_raw <'a>]
 ) ->
@@ -4524,6 +4547,15 @@ pub fn cbor_det_array_iterator_is_empty <'a>(
     res
 }
 
+pub fn cbor_det_array_iterator_length <'a>(
+    x: cbor_raw_iterator__CBOR_Pulse_Raw_Type_cbor_raw <'a>
+) ->
+    u64
+{
+    let res: u64 = cbor_array_iterator_length(x);
+    res
+}
+
 pub fn cbor_det_array_iterator_next <'b, 'a>(
     x: &'b mut [cbor_raw_iterator__CBOR_Pulse_Raw_Type_cbor_raw <'a>]
 ) ->