diff --git a/CHANGELOG.md b/CHANGELOG.md index fbe9376eae..b932392e44 100644 --- a/CHANGELOG.md +++ b/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) diff --git a/stdlib/asm/crypto/stark/constants.masm b/stdlib/asm/crypto/stark/constants.masm index ed00ac9bcd..8529917593 100644 --- a/stdlib/asm/crypto/stark/constants.masm +++ b/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 # . diff --git a/stdlib/asm/crypto/stark/mod.masm b/stdlib/asm/crypto/stark/mod.masm new file mode 100644 index 0000000000..776b802297 --- /dev/null +++ b/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 diff --git a/stdlib/asm/crypto/stark/utils.masm b/stdlib/asm/crypto/stark/utils.masm index 27553f0dde..5f701da93c 100644 --- a/stdlib/asm/crypto/stark/utils.masm +++ b/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 diff --git a/stdlib/asm/crypto/stark/verifier.masm b/stdlib/asm/crypto/stark/verifier.masm index 15bf4f84fa..0183fe2a78 100644 --- a/stdlib/asm/crypto/stark/verifier.masm +++ b/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