tag some byte arrays with maxbits

Author: alinush

circuit/templates/helpers/base64url/Base64UrlDecode.circom

@@ -34,7 +34,9 @@ template Base64UrlDecode(N) {
     // (We implement this as: \floor{(4*N + 2) / 3}.)
     var M = (4*N + 2) \ 3;
     signal input in[M];
-    signal output out[N];
+    signal output {maxbits} out[N];
+    // TODO(Soundness): Make sure this is actually enforced by this template.
+    out.maxbits = 8;
 
     component bits_in[M \ 4][4];
     component bits_out[M \ 4][3];

circuit/templates/helpers/hashtofield/HashBytesToFieldWithLen.circom

@@ -14,19 +14,13 @@ include "HashElemsToField.circom";
  * We hash the length `len` of the input as well to prevent collisions.
  *
  * Currently, does not work for inputs larger than $64 \times 31 = 1984$ bytes.
- * TODO(Comment): Why?
- *
- * TODO(Buses): If `in` is `Bytes(MAX_LEN)` bus, then we can remove the `AssertIsBytes`
- * constraint here, since it may be unnecessarily repeated if this gets called for the
- * same byte sub-sequence repeatedly.
+ * because `HashElemsToField` only handles <= 64 field elements (but can be extended).
  *
  * Parameters:
- *   NUM_BYTES       the max number of bytes this can handle; is > 0 and <= 1984 (64 * 31)
+ *   NUM_BYTES      the max number of bytes this can handle; is > 0 and <= 1984 (64 * 31)
  *
  * Input signals:
- *   in[NUM_BYTES]  array to be hashed, although only in[0], in[1], ..., in[len-1];
- *                  constrained to ensure elements are actually bytes
- *                  are actually hashed
+ *   in[NUM_BYTES]  array to be hashed, but only in[0], in[1], ..., in[len-1] prefix is actually hashed
  *   len            the number of bytes that will be actually hashed;
  *                  bytes `in[len], in[len+1]..., in[NUM_BYTES-1]` are ignored
  *
@@ -35,15 +29,15 @@ include "HashElemsToField.circom";
  *
  * Notes:
  *   There is no way to meaningfully ensure that `len` is the actual length of the bytes in `in`.
- *   TODO(Buses): Some type-safety via a `Bytes(MAX_LEN)` bus may be useful here?
  */
 template HashBytesToFieldWithLen(NUM_BYTES) {
     assert(NUM_BYTES > 0);
-    signal input in[NUM_BYTES];
+    assert(NUM_BYTES <= 1984);
+    signal input {maxbits} in[NUM_BYTES];
     signal input len;
     signal output hash;
 
-    AssertIsBytes(NUM_BYTES)(in);
+    assert(in.maxbits <= 8);
 
     var NUM_ELEMS = NUM_BYTES % 31 == 0 ? NUM_BYTES\31 : NUM_BYTES\31 + 1;
 
@@ -54,14 +48,13 @@ template HashBytesToFieldWithLen(NUM_BYTES) {
         8           // bitsPerChunk
     )(in);
 
-    // TODO(Cleanup): Can't we use a var here? We are simply re-assigning signals, it seems.
-    signal input_with_len[NUM_ELEMS + 1];
+    var elems[NUM_ELEMS + 1];
     for (var i = 0; i < NUM_ELEMS; i++) {
-        input_with_len[i] <== input_packed[i];
+        elems[i] = input_packed[i];
     }
-    input_with_len[NUM_ELEMS] <== len;
+    elems[NUM_ELEMS] = len;
 
-    PoseidonBN254Hash() poseidonHash <== HashElemsToField(NUM_ELEMS + 1)(input_with_len);
+    PoseidonBN254Hash() poseidonHash <== HashElemsToField(NUM_ELEMS + 1)(elems);
 
     hash <== poseidonHash.value;
 }

circuit/templates/helpers/jwt/ParseEmailVerifiedField.circom

@@ -24,9 +24,9 @@ include "circomlib/circuits/gates.circom";
 // This template exists specifically for the email_verified JWT field, as some providers
 // do not follow the OIDC spec and instead enclose the value of this field in quotes
 template ParseEmailVerifiedField(MAX_KV_PAIR_LEN, MAX_NAME_LEN, MAX_VALUE_LEN) {
-    signal input field[MAX_KV_PAIR_LEN]; // ASCII
-    signal input name[MAX_NAME_LEN];
-    signal input value[MAX_VALUE_LEN];
+    signal input {maxbits} field[MAX_KV_PAIR_LEN]; // ASCII
+    signal input {maxbits} name[MAX_NAME_LEN];
+    signal input {maxbits} value[MAX_VALUE_LEN];
     signal input field_len; // ASCII
     signal input name_len;
     signal input value_index; // index of value within `field`

circuit/templates/helpers/jwt/ParseJWTFieldSharedLogic.circom

@@ -23,9 +23,9 @@ include "circomlib/circuits/gates.circom";
 // Note that this template is NOT secure on its own, but must be called from
 // `ParseJWTFieldWithQuotedValue` or `ParseJWTFieldWithUnquotedValue`
 template ParseJWTFieldSharedLogic(MAX_KV_PAIR_LEN, MAX_NAME_LEN, MAX_VALUE_LEN) {
-    signal input field[MAX_KV_PAIR_LEN]; // ASCII
-    signal input name[MAX_NAME_LEN]; // ASCII
-    signal input value[MAX_VALUE_LEN]; // ASCII
+    signal input {maxbits} field[MAX_KV_PAIR_LEN]; // ASCII
+    signal input {maxbits} name[MAX_NAME_LEN]; // ASCII
+    signal input {maxbits} value[MAX_VALUE_LEN]; // ASCII
     signal input field_len;
     signal input name_len;
     signal input value_index; // index of value within `field`
@@ -68,4 +68,4 @@ template ParseJWTFieldSharedLogic(MAX_KV_PAIR_LEN, MAX_NAME_LEN, MAX_VALUE_LEN)
     signal checks_pass <== MultiAND(9)(checks);
     signal success <== OR()(checks_pass, skip_checks);
     success === 1;
-}
+}

circuit/templates/helpers/jwt/ParseJWTFieldWithQuotedValue.circom

@@ -22,9 +22,9 @@ include "circomlib/circuits/gates.circom";
 // checks enforced by this template will be skipped, and it will function as
 // a no-op. If it is set to 0, failing one check will fail proof generation
 template ParseJWTFieldWithQuotedValue(MAX_KV_PAIR_LEN, MAX_NAME_LEN, MAX_VALUE_LEN) {
-    signal input field[MAX_KV_PAIR_LEN]; // ASCII
-    signal input name[MAX_NAME_LEN]; // ASCII
-    signal input value[MAX_VALUE_LEN]; // ASCII
+    signal input {maxbits} field[MAX_KV_PAIR_LEN]; // ASCII
+    signal input {maxbits} name[MAX_NAME_LEN]; // ASCII
+    signal input {maxbits} value[MAX_VALUE_LEN]; // ASCII
     signal input field_string_bodies[MAX_KV_PAIR_LEN];
     signal input field_len;
     signal input name_len;
@@ -70,4 +70,4 @@ template ParseJWTFieldWithQuotedValue(MAX_KV_PAIR_LEN, MAX_NAME_LEN, MAX_VALUE_L
     signal checks_pass <== MultiAND(3)(checks);
     signal succeed <== OR()(checks_pass, skip_checks);
     succeed === 1;
-}
+}

circuit/templates/helpers/jwt/ParseJWTFieldWithUnquotedValue.circom

@@ -22,9 +22,9 @@ include "circomlib/circuits/gates.circom";
 // checks enforced by this template will be skipped, and it will function as
 // a no-op. If it is set to 0, failing one check will fail proof generation
 template ParseJWTFieldWithUnquotedValue(MAX_KV_PAIR_LEN, MAX_NAME_LEN, MAX_VALUE_LEN) {
-    signal input field[MAX_KV_PAIR_LEN]; // ASCII
-    signal input name[MAX_NAME_LEN];
-    signal input value[MAX_VALUE_LEN];
+    signal input {maxbits} field[MAX_KV_PAIR_LEN]; // ASCII
+    signal input {maxbits} name[MAX_NAME_LEN];
+    signal input {maxbits} value[MAX_VALUE_LEN];
     signal input field_len; // ASCII
     signal input name_len;
     signal input value_index; // index of value within `field`
@@ -65,4 +65,4 @@ template ParseJWTFieldWithUnquotedValue(MAX_KV_PAIR_LEN, MAX_NAME_LEN, MAX_VALUE
     signal checks_pass <== AND()(checks[0], checks[1]);
     signal success <== OR()(checks_pass, skip_checks);
     success === 1;
-}
+}

circuit/templates/helpers/sha/SHA2_256_PaddingVerify.circom

@@ -9,16 +9,20 @@ include "circomlib/circuits/bitify.circom";
 
 // Verifies SHA2_256 input padding according to https://www.rfc-editor.org/rfc/rfc4634.html#section-4.1
 template SHA2_256_PaddingVerify(MAX_INPUT_LEN) {
-    signal input in[MAX_INPUT_LEN]; // byte array
+    signal input {maxbits} in[MAX_INPUT_LEN]; // byte array
     signal input num_blocks; // Number of 512-bit blocks in `in` including sha padding
     signal input padding_start; // equivalent to L/8, where L is the length of the unpadded message in bits as specified in RFC4634
-    signal input L_byte_encoded[8]; // 64-bit encoding of L
-    signal input padding_without_len[64]; // padding_without_len[0] = 1, followed by K 0s. Length K+1, max length 512 bits. Does not include the 64-bit encoding of L
+    signal input {maxbits} L_byte_encoded[8]; // byte-array; 64-bit encoding of L
+    signal input {maxbits} padding_without_len[64]; // byte-array; padding_without_len[0] = 1, followed by K 0s. Length K+1, max length 512 bits. Does not include the 64-bit encoding of L
 
     var len_bits = num_blocks * 512;
     var padding_start_bits = padding_start * 8;
     var K = len_bits - padding_start_bits - 1 - 64; 
 
+    assert(in.maxbits == 8);
+    assert(L_byte_encoded.maxbits == 8);
+    assert(padding_without_len.maxbits == 8);
+
     // Ensure K is 9-bits (i.e., < 2^9 = 512)
     _ <== Num2Bits(9)(K);
 

circuit/templates/helpers/strings/IsSubstring.circom

@@ -40,12 +40,15 @@ template IsSubstring(MAX_STR_LEN, MAX_SUBSTR_LEN) {
     // length
     assert(MAX_SUBSTR_LEN <= MAX_STR_LEN);
 
-    signal input str[MAX_STR_LEN];
+    signal input {maxbits} str[MAX_STR_LEN];
     signal input str_hash;
 
-    signal input substr[MAX_SUBSTR_LEN];
+    signal input {maxbits} substr[MAX_SUBSTR_LEN];
     signal input substr_len;
 
+    assert(str.maxbits <= 8);
+    assert(substr.maxbits <= 8);
+
     // The index of `substr` in `str`:
     //
     //   str[start_index]                    = substr[0]
@@ -126,9 +129,9 @@ template IsSubstring(MAX_STR_LEN, MAX_SUBSTR_LEN) {
 // Enforces that:
 // - `str[start_index:substr_len]` = `substr[0:substr_len]`
 template AssertIsSubstring(MAX_STR_LEN, MAX_SUBSTR_LEN) {
-    signal input str[MAX_STR_LEN];
+    signal input {maxbits} str[MAX_STR_LEN];
     signal input str_hash;
-    signal input substr[MAX_SUBSTR_LEN];
+    signal input {maxbits} substr[MAX_SUBSTR_LEN];
     signal input substr_len;
     signal input start_index;