feat: add paramter check to recursive verifier

chore: changelog update

chore: add back file and update it

Revert "refactor: remove file"

This reverts commit 384a5af.

CHANGELOG.md

@@ -13,6 +13,7 @@
 #### Enhancements
 - Added `miden_core::mast::MastForest::advice_map` to load it into the advice provider before the `MastForest` execution (#1574).
 - Optimized the computation of the DEEP queries in the recursive verifier (#1594).
+- Added validity checks for the inputs to the recursive verifier (#1596).
 
 ## 0.11.0 (2024-11-04)
 

stdlib/asm/crypto/stark/constants.masm

@@ -39,11 +39,15 @@ const.COMPOSITION_COEF_PTR=4294900200
 
 # We need 2 Felt for each trace column and each of the 8 constraint composition columns. We thus need
 # (70 + 7 + 8) * 2 Felt i.e. 43 memory slots.
+# Note that there is a cap on the number of such coefficients so that the memory region allocated for
+# these coefficients does not overlap with the memory region storing the FRI queries.
+# This cap is of a 100 coefficients which is equivalent to 50 memory slots. This gives 150 memory
+# slots for all of the FRI queries i.e., 150 FRI queries.
 const.DEEP_RAND_CC_PTR=4294903000
 
 # FRI
 #
-#       (FRI_COM_PTR - 100)    ---|
+#       (FRI_COM_PTR - 150)    ---|
 #              .
 #              .                  | <- FRI queries
 #              .

stdlib/asm/crypto/stark/mod.masm

@@ -0,0 +1,27 @@
+use.std::crypto::stark::verifier
+
+#!   Verify a STARK proof attesting to the correct execution of a program in the Miden VM.
+#!   The following simplifying assumptions are currently made:
+#!   - The blowup is set to 8.
+#!   - The maximal allowed degree of the remainder polynomial is 7.
+#!   - The public inputs are composed of the input and output stacks, of fixed size equal to 16.
+#!   - There are two trace segments, main and auxiliary. It is assumed that the main trace segment
+#!   is 70 columns wide while the auxiliary trace segment is 7 columns wide.
+#!   - The OOD evaluation frame is composed of two interleaved rows, current and next, each composed
+#!    of 70 elements representing the main trace portion and 7 elements for the auxiliary trace one.
+#!   - To boost soundness, the protocol is run on a quadratic extension field and this means that
+#!    the OOD evaluation frame is composed of elements in a quadratic extension field i.e. tuples.
+#!    Similarly, elements of the auxiliary trace are quadratic extension field elements. The random
+#!    values for computing random linear combinations are also in this extension field.
+#!   - The following procedure makes use of global memory address beyond 3 * 2^30 and these are
+#!    defined in `constants.masm`.
+#!
+#! Input: [log(trace_length), num_queries, log(blowup), grinding, ...]
+#! Output: [...]
+#!
+#! Cycles:
+#!  1- Remainder codeword size 32:
+#!   5013 + num_queries * (40 + num_fri_layers * 76 + 26 + 445) + 83 * num_fri_layers + 10 * log(trace_length) + 1633
+#!  2- Remainder codeword size 64:
+#!   5013 + num_queries * (40 + num_fri_layers * 76 + 26 + 445) + 83 * num_fri_layers + 10 * log(trace_length) + 3109
+export.verifier::verify

stdlib/asm/crypto/stark/utils.masm

@@ -16,3 +16,35 @@ export.compute_lde_generator
     exp.u32
     # => [domain_gen, ..]
 end
+
+#! Validates the inputs to the recursive verifier.
+#!
+#! Input: [log(trace_length), num_queries, log(blowup), grinding, ...]
+#! Output: [log(trace_length), num_queries, log(blowup), grinding, ...]
+#!
+#! Cycles: 28
+export.validate_inputs
+    # 1) Assert that all inputs are u32 so that we can use u32 operations in what follows
+    dupw
+    u32assertw
+    # => [log(trace_length), num_queries, log(blowup), grinding, ...]
+
+    # 2) Assert that the trace length is at most 29. The 2-adicity of our field is 32 and since
+    #    the blowup factor is 8, we need to make sure that the LDE size is at most 2^32.
+    #    We also check that the trace length is greater than the minimal length supported i.e., 2^6.
+    dup u32lt.30 assert
+    u32gt.5 assert
+
+    # 3) Assert that the number of FRI queries is at most 150. This restriction is a soft one
+    #    and is due to the memory layout in the `constants.masm` files but can be updated
+    #    therein.
+    #    We also make sure that there is at least one FRI query.
+    dup u32lt.151 assert
+    u32gt.0 assert
+
+    # 4) Assert that the the log(blowup) is 3
+    eq.3 assert
+
+    # 5) Assert that the grinding factor is at most 31
+    u32lt.32 assert
+end

stdlib/asm/crypto/stark/verifier.masm

@@ -6,7 +6,7 @@ use.std::crypto::stark::random_coin
 use.std::crypto::stark::ood_frames
 use.std::crypto::stark::public_inputs
 use.std::crypto::stark::constants
-
+use.std::crypto::stark::utils
 
 #!   Verify a STARK proof attesting to the correct execution of a program in the Miden VM.
 #!   The following simplifying assumptions are currently made:
@@ -25,18 +25,25 @@ use.std::crypto::stark::constants
 #!    defined in `constants.masm`.
 #!
 #! Input: [log(trace_length), num_queries, log(blowup), grinding, ...]
-#! Output: []
+#! Output: [...]
+#!
 #! Cycles:
 #!  1- Remainder codeword size 32:
-#!   4985 + num_queries * (40 + num_fri_layers * 76 + 26 + 445) + 83 * num_fri_layers + 10 * log(trace_length) + 1633
+#!   5013 + num_queries * (40 + num_fri_layers * 76 + 26 + 445) + 83 * num_fri_layers + 10 * log(trace_length) + 1633
 #!  2- Remainder codeword size 64:
-#!   4985 + num_queries * (40 + num_fri_layers * 76 + 26 + 445) + 83 * num_fri_layers + 10 * log(trace_length) + 3109
+#!   5013 + num_queries * (40 + num_fri_layers * 76 + 26 + 445) + 83 * num_fri_layers + 10 * log(trace_length) + 3109
 export.verify
 
     #==============================================================================================
     #       I)  Hash proof context and hash-&-load public inputs
     #==============================================================================================
 
+    # Validate inputs
+    #
+    # Cycles: 28
+    exec.utils::validate_inputs
+    # => [log(trace_length), num_queries, log(blowup), grinding, ...]
+
     # Initialize the seed using proof context
     #
     # Cycles: 82