axiom-crypto · jonathanpwang · Aug 22, 2023 · Aug 22, 2023
diff --git a/halo2-base/src/safe_types/bytes.rs b/halo2-base/src/safe_types/bytes.rs
@@ -55,11 +55,11 @@ impl<F: ScalarField> VarLenBytesVec<F> {
     // VarLenBytesVec can be only created by SafeChip.
     pub(super) fn new(bytes: Vec<SafeByte<F>>, len: AssignedValue<F>, max_len: usize) -> Self {
         assert!(
-            len.value().le(&F::from_u128(max_len as u128)),
+            len.value().le(&F::from(max_len as u64)),
             "Invalid length which exceeds MAX_LEN {}",
             max_len
         );
-        assert!(bytes.len() == max_len, "bytes is not padded correctly");
+        assert_eq!(bytes.len(), max_len, "bytes is not padded correctly");
         Self { bytes, len }
     }
 

diff --git a/halo2-base/src/safe_types/mod.rs b/halo2-base/src/safe_types/mod.rs
@@ -231,23 +231,23 @@ impl<'a, F: ScalarField> SafeTypeChip<'a, F> {
     ///
     /// * ctx: Circuit [Context]<F> to assign witnesses to.
     /// * inputs: Slice representing the byte array.
-    /// * len: [AssignedValue]<F> witness representing the variable elements within the byte array from 0..=len.
+    /// * len: [AssignedValue]<F> witness representing the variable length of the byte array. Constrained to be `<= MAX_LEN`.
     /// * MAX_LEN: [usize] representing the maximum length of the byte array and the number of elements it must contain.
     pub fn raw_to_var_len_bytes<const MAX_LEN: usize>(
         &self,
         ctx: &mut Context<F>,
         inputs: [AssignedValue<F>; MAX_LEN],
         len: AssignedValue<F>,
     ) -> VarLenBytes<F, MAX_LEN> {
-        self.range_chip.check_less_than_safe(ctx, len, MAX_LEN as u64);
+        self.range_chip.check_less_than_safe(ctx, len, MAX_LEN as u64 + 1);
         VarLenBytes::<F, MAX_LEN>::new(inputs.map(|input| self.assert_byte(ctx, input)), len)
     }
 
-    /// Converts a vector of AssignedValue(treated as little-endian) to VarLenBytesVec. Not encourged to use because `MAX_LEN` cannot be verified at compile time.
+    /// Converts a vector of AssignedValue to [VarLenBytesVec]. Not encouraged to use because `MAX_LEN` cannot be verified at compile time.
     ///
     /// * ctx: Circuit [Context]<F> to assign witnesses to.
-    /// * inputs: Vector representing the byte array.
-    /// * len: [AssignedValue]<F> witness representing the variable elements within the byte array from 0..=len.
+    /// * inputs: Vector representing the byte array, right padded to `max_len`. See [VarLenBytesVec] for details about padding.
+    /// * len: [AssignedValue]<F> witness representing the variable length of the byte array. Constrained to be `<= max_len`.
     /// * max_len: [usize] representing the maximum length of the byte array and the number of elements it must contain.
     pub fn raw_to_var_len_bytes_vec(
         &self,
@@ -256,7 +256,7 @@ impl<'a, F: ScalarField> SafeTypeChip<'a, F> {
         len: AssignedValue<F>,
         max_len: usize,
     ) -> VarLenBytesVec<F> {
-        self.range_chip.check_less_than_safe(ctx, len, max_len as u64);
+        self.range_chip.check_less_than_safe(ctx, len, max_len as u64 + 1);
         VarLenBytesVec::<F>::new(
             inputs.iter().map(|input| self.assert_byte(ctx, *input)).collect_vec(),
             len,

diff --git a/halo2-base/src/safe_types/tests/bytes.rs b/halo2-base/src/safe_types/tests/bytes.rs
@@ -36,11 +36,15 @@ fn mock_circuit_test<FM: FnMut(&mut Context<Fr>, SafeTypeChip<'_, Fr>)>(mut f: F
 fn pos_var_len_bytes() {
     base_test().k(10).lookup_bits(8).run(|ctx, range| {
         let safe = SafeTypeChip::new(range);
-        let fake_bytes = ctx.assign_witnesses(
+        let bytes = ctx.assign_witnesses(
             vec![255u64, 255u64, 255u64, 255u64].into_iter().map(Fr::from).collect::<Vec<_>>(),
         );
         let len = ctx.load_witness(Fr::from(3u64));
-        safe.raw_to_var_len_bytes::<4>(ctx, fake_bytes.try_into().unwrap(), len);
+        safe.raw_to_var_len_bytes::<4>(ctx, bytes.clone().try_into().unwrap(), len);
+
+        // check edge case len == MAX_LEN
+        let len = ctx.load_witness(Fr::from(4u64));
+        safe.raw_to_var_len_bytes::<4>(ctx, bytes.try_into().unwrap(), len);
     });
 }
 
@@ -57,7 +61,7 @@ fn neg_var_len_bytes_witness_values_not_bytes() {
     });
 }
 
-//Checks assertion len < max_len
+// Checks assertion len <= max_len
 #[test]
 #[should_panic]
 fn neg_var_len_bytes_len_less_than_max_len() {
@@ -75,11 +79,15 @@ fn neg_var_len_bytes_len_less_than_max_len() {
 fn pos_var_len_bytes_vec() {
     base_test().k(10).lookup_bits(8).run(|ctx, range| {
         let safe = SafeTypeChip::new(range);
-        let fake_bytes = ctx.assign_witnesses(
+        let bytes = ctx.assign_witnesses(
             vec![255u64, 255u64, 255u64, 255u64].into_iter().map(Fr::from).collect::<Vec<_>>(),
         );
         let len = ctx.load_witness(Fr::from(3u64));
-        safe.raw_to_var_len_bytes_vec(ctx, fake_bytes, len, 4);
+        safe.raw_to_var_len_bytes_vec(ctx, bytes.clone(), len, 4);
+
+        // check edge case len == MAX_LEN
+        let len = ctx.load_witness(Fr::from(4u64));
+        safe.raw_to_var_len_bytes_vec(ctx, bytes, len, 4);
     });
 }
 
@@ -97,7 +105,7 @@ fn neg_var_len_bytes_vec_witness_values_not_bytes() {
     });
 }
 
-//Checks assertion len != max_len
+// Checks assertion len <= max_len
 #[test]
 #[should_panic]
 fn neg_var_len_bytes_vec_len_less_than_max_len() {
@@ -106,7 +114,7 @@ fn neg_var_len_bytes_vec_len_less_than_max_len() {
         let fake_bytes = ctx.assign_witnesses(
             vec![500u64, 500u64, 500u64, 500u64].into_iter().map(Fr::from).collect::<Vec<_>>(),
         );
-        let max_len = 5;
+        let max_len = 4;
         safe.raw_to_var_len_bytes_vec(ctx, fake_bytes, len, max_len);
     });
 }