Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update and sync-up the recursive verifier #1575

Open
wants to merge 5 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 4 commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
- Debug instructions can be enabled in the cli `run` command using `--debug` flag (#1502).
- Added support for procedure annotation (attribute) syntax to Miden Assembly (#1510).
- Make `miden-prover::prove()` method conditionally asynchronous (#1563).
- Update and sync the recursive verifier (#1575).

#### Changes

Expand Down
67 changes: 33 additions & 34 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion assembly/src/library/namespace.rs
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ impl LibraryNamespace {
if matches!(source, Self::KERNEL_PATH | Self::EXEC_PATH | Self::ANON_PATH) {
return Ok(());
}
if source.as_bytes().len() > Self::MAX_LENGTH {
if source.len() > Self::MAX_LENGTH {
return Err(LibraryNamespaceError::Length);
}
if !source.starts_with(|c: char| c.is_ascii_lowercase() && c.is_ascii_alphabetic()) {
Expand Down
4 changes: 2 additions & 2 deletions assembly/src/library/path.rs
Original file line number Diff line number Diff line change
Expand Up @@ -192,8 +192,8 @@ impl LibraryPath {

/// Return the size in bytes of this path when displayed as a string
pub fn byte_len(&self) -> usize {
self.inner.components.iter().map(|c| c.as_bytes().len()).sum::<usize>()
+ self.inner.ns.as_str().as_bytes().len()
self.inner.components.iter().map(|c| c.len()).sum::<usize>()
+ self.inner.ns.as_str().len()
+ (self.inner.components.len() * 2)
}

Expand Down
2 changes: 1 addition & 1 deletion assembly/src/parser/scanner.rs
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ pub struct Scanner<'input> {
impl<'input> Scanner<'input> {
/// Construct a new [Scanner] for the given `source`.
pub fn new(input: &'input str) -> Self {
let end = input.as_bytes().len();
let end = input.len();
assert!(end < u32::MAX as usize, "file too large");

let mut chars = input.char_indices().peekable();
Expand Down
2 changes: 1 addition & 1 deletion assembly/src/parser/token.rs
Original file line number Diff line number Diff line change
Expand Up @@ -860,7 +860,7 @@ impl<'input> Token<'input> {
// No match, it's an ident
None => Token::Ident(s),
// If the match is not exact, it's an ident
Some(matched) if matched.len() != s.as_bytes().len() => Token::Ident(s),
Some(matched) if matched.len() != s.len() => Token::Ident(s),
// Otherwise clone the Token corresponding to the keyword that was matched
Some(matched) => Self::KEYWORDS[matched.pattern().as_usize()].1.clone(),
}
Expand Down
3 changes: 2 additions & 1 deletion core/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,8 @@ std = [
lock_api = { version = "0.4", features = ["arc_lock"] }
math = { package = "winter-math", version = "0.10", default-features = false }
memchr = { version = "2.7", default-features = false }
miden-crypto = { version = "0.12", default-features = false }
#miden-crypto = { version = "0.12", default-features = false }
miden-crypto = { git = "https://github.com/0xPolygonMiden/crypto/", branch ="al-fix-rpo-randcoin", default-features = false }
miden-formatting = { version = "0.1", default-features = false }
miette = { package = "miden-miette", version = "7.1", default-features = false, optional = true, features = [
"fancy-no-syscall",
Expand Down
18 changes: 9 additions & 9 deletions processor/src/operations/comb_ops.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,8 @@ where
/// \frac{T_i(x) - T_i(g \cdot z)}{x - g \cdot z} \right)}
///
/// The instruction computes the numerators $\alpha_i \cdot (T_i(x) - T_i(z))$ and
/// $\alpha_i \cdot (T_i(x) - T_i(g \cdot z))$ and stores the values in two accumulators $p$
/// and $r$, respectively. This instruction is specialized to main trace columns i.e.
/// $\alpha_i \cdot (T_i(x) - T_i(g \cdot z))$ and stores the values in two accumulators $r$
/// and $p$, respectively. This instruction is specialized to main trace columns i.e.
/// the values $T_i(x)$ are base field elements.
///
/// The instruction is used in the context of STARK proof verification in order to compute
Expand Down Expand Up @@ -47,9 +47,9 @@ where
/// 1. Ti for i in 0..=7 stands for the the value of the i-th trace polynomial for the current
/// query i.e. T_i(x).
/// 2. (p0, p1) stands for an extension field element accumulating the values for the quotients
/// with common denominator (x - z).
/// 3. (r0, r1) stands for an extension field element accumulating the values for the quotients
/// with common denominator (x - gz).
/// 3. (r0, r1) stands for an extension field element accumulating the values for the quotients
/// with common denominator (x - z).
/// 4. x_addr is the memory address from which we are loading the Ti's using the MSTREAM
/// instruction.
/// 5. z_addr is the memory address to the i-th OOD evaluations at z and gz i.e. T_i(z):=
Expand All @@ -75,7 +75,7 @@ where
// --- compute the updated accumulator values ---------------------------------------------
let v0 = self.stack.get(7);
let tx = QuadFelt::new(v0, ZERO);
let [p_new, r_new] = [p + alpha * (tx - tz), r + alpha * (tx - tgz)];
let [r_new, p_new] = [r + alpha * (tx - tz), p + alpha * (tx - tgz)];
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: can we swap the order to [p_new, r_new] so that it's consistent with line 73 above?

I think the ideal would be to put r before p on the stack (so that the order is always consistent), but just this small swap is probably fine

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Makes sense, done!


// --- rotate the top 8 elements of the stack ---------------------------------------------
self.stack.set(0, t0);
Expand Down Expand Up @@ -252,8 +252,8 @@ mod tests {
let a1 = a[1];
let alpha = QuadFelt::new(a0, a1);

let p_new = p + alpha * (tx - tz);
let r_new = r + alpha * (tx - tgz);
let p_new = p + alpha * (tx - tgz);
let r_new = r + alpha * (tx - tz);

assert_eq!(p_new.to_base_elements()[1], stack_state[8]);
assert_eq!(p_new.to_base_elements()[0], stack_state[9]);
Expand Down Expand Up @@ -356,10 +356,10 @@ mod tests {
expected.extend_from_slice(&[ZERO, Felt::from(18_u8), Felt::from(10_u8), Felt::from(2_u8)]);
// updated accumulators
expected.extend_from_slice(&[
r.to_base_elements()[0],
r.to_base_elements()[1],
p.to_base_elements()[0],
p.to_base_elements()[1],
r.to_base_elements()[0],
r.to_base_elements()[1],
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Lines 334 and 335 are still incorrect (i.e. p should use tgz and r should use tz). Then I think the diff here should be reverted (since the stack is being built from bottom to top, so r comes before p)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed

]);
// the top 8 stack elements should equal tx since 8 calls to `rcomb_base` implies 8 circular
// shifts of the top 8 elements i.e., the identity map on the top 8 element.
Expand Down
19 changes: 7 additions & 12 deletions stdlib/asm/crypto/stark/constants.masm
Original file line number Diff line number Diff line change
Expand Up @@ -17,15 +17,15 @@ const.TRACE_DOMAIN_GENERATOR_PTR=4294799999
const.PUBLIC_INPUTS_PTR=4294800000

# OOD Frames
# (72 + 9 + 8) * 2 * 2 Felt for current and next trace rows and 8 * 2 Felt for constraint composition
# polynomials. Total memory slots required: ((72 + 9 + 8) * 2 * 2 + 8 * 2) / 4 = 93
# (70 + 7) * 2 * 2 Felt for current and next trace rows and 8 * 2 Felt for constraint composition
# polynomials. Total memory slots required: ((70 + 7) * 2 * 2 + 8 * 2) / 4 = 81
const.OOD_TRACE_PTR=4294900000
const.OOD_CONSTRAINT_EVALS_PTR=4294900081
const.OOD_CONSTRAINT_EVALS_PTR=4294900077
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there an assumption in the code that OOD_TRACE_PTR is right next to OOD_CONSTRAINT_EVALS_PTR? If not, we could put them far away enough such that we don't need to come fix this value everytime we make a change to the shape of the trace.

Similar comment applies to all constants in this file

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The reason for this is so that we avoid having to update the pointers in between the different steps of computing the random linear combination for the DEEP queries. This is the hottest loop of the recursive verifier and any savings we can make are worth the little extra effort.


# Current trace row
# 72 Felt for main portion of trace, 9 * 2 Felt for auxiliary portion of trace and 8 * 2 Felt for
# 70 Felt for main portion of trace, 7 * 2 Felt for auxiliary portion of trace and 8 * 2 Felt for
# constraint composition polynomials. Since we store these with the padding to make each of the
# three portions a multiple of 8, the number of slots required is (80 + 24 + 16) / 4 = 30
# three portions a multiple of 8, the number of slots required is (72 + 16 + 16) / 4 = 26
const.CURRENT_TRACE_ROW_PTR=4294900100

# Random elements
Expand All @@ -36,7 +36,7 @@ const.AUX_RAND_ELEM_PTR=4294900150
const.COMPOSITION_COEF_PTR=4294900200

# We need 2 Felt for each trace column and each of the 8 constraint composition columns. We thus need
# (72 + 9 + 8) * 2 Felt i.e. 44 memory slots.
# (70 + 7 + 8) * 2 Felt i.e. 43 memory slots.
const.DEEP_RAND_CC_PTR=4294903000

# FRI
Expand Down Expand Up @@ -80,7 +80,6 @@ const.GRINDING_FACTOR_PTR=4294903308

# RPO capacity initialization words
const.ZERO_WORD_PTR=4294903309
const.ZERO_ZERO_ZERO_ONE_PTR=4294903310

# State of RPO-based random coin
const.C_PTR=4294903311
Expand All @@ -106,7 +105,7 @@ const.TMP8=4294903322
# | TRACE_DOMAIN_GENERATOR_PTR | 4294799999 |
# | PUBLIC_INPUTS_PTR | 4294800000 |
# | OOD_TRACE_PTR | 4294900000 |
# | OOD_CONSTRAINT_EVALS_PTR | 4294900081 |
# | OOD_CONSTRAINT_EVALS_PTR | 4294900077 |
# | CURRENT_TRACE_ROW_PTR | 4294900100 |
# | AUX_RAND_ELEM_PTR | 4294900150 |
# | COMPOSITION_COEF_PTR | 4294900200 |
Expand Down Expand Up @@ -238,10 +237,6 @@ export.zero_word
push.ZERO_WORD_PTR
end

export.zero_zero_zero_one_word
push.ZERO_ZERO_ZERO_ONE_PTR
end

#! Returns the pointer to the capacity word of the random coin.
#!
#! Note: The random coin is implemented using a hash function, this returns the
Expand Down
Loading
Loading