Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
40 commits
Select commit Hold shift + click to select a range
42a4e36
removed ColMatrix dependency
Al-Kindi-0 Apr 20, 2025
08327ae
wip: working prover without randomized phase
Al-Kindi-0 Apr 29, 2025
ef3f65d
wip add aux to prover
Al-Kindi-0 Apr 29, 2025
2a1443a
add prove instrument
Al-Kindi-0 Apr 29, 2025
4d731ce
use folding factor 2
Al-Kindi-0 May 31, 2025
bd2c7b5
wip
Al-Kindi-0 Sep 8, 2025
36562ae
changed the structure of prover module
Al-Kindi-0 Sep 10, 2025
1fe8d01
changed the structure of prover module
Al-Kindi-0 Sep 10, 2025
9237942
wip
Al-Kindi-0 Sep 11, 2025
cb068fd
desactivate 9 deg constraint
Al-Kindi-0 Sep 11, 2025
33ab3b4
bump up p3 crate version
Al-Kindi-0 Sep 13, 2025
999449f
not rebased but with KECCAK
Al-Kindi-0 Sep 16, 2025
97b18d8
move in direction of Permutation support
Al-Kindi-0 Sep 16, 2025
f81c730
add missing modules
Al-Kindi-0 Sep 27, 2025
511a4e0
minor org work
Al-Kindi-0 Sep 27, 2025
b4c4602
update dep
Al-Kindi-0 Sep 29, 2025
09e1265
Merge remote-tracking branch 'origin/plonky3-migration-old' into zz/m…
zhenfeizhang Oct 4, 2025
e7ee755
cargo fmt
zhenfeizhang Oct 4, 2025
5032540
core compiles
zhenfeizhang Oct 4, 2025
bca5935
core tests pass
zhenfeizhang Oct 4, 2025
129e9fd
fixed air tests
zhenfeizhang Oct 4, 2025
46846aa
processor crate compiles
zhenfeizhang Oct 6, 2025
ce5515a
verifier repo fixed
zhenfeizhang Oct 6, 2025
8e058fa
fixed prover crate
zhenfeizhang Oct 6, 2025
46eea92
clean up
zhenfeizhang Oct 6, 2025
b573907
make exec compiles
zhenfeizhang Oct 6, 2025
12b5c85
clean up more errors
zhenfeizhang Oct 6, 2025
2842f8c
remove most of unused imports
zhenfeizhang Oct 7, 2025
920b712
update cargo lock
zhenfeizhang Oct 7, 2025
aeea60b
fix a few bugs
zhenfeizhang Oct 8, 2025
5407d30
fix issues with (de)serialization and fix tracing tree issues
Al-Kindi-0 Oct 9, 2025
e2b4f18
clean up
zhenfeizhang Oct 10, 2025
92eeb25
Merge remote-tracking branch 'origin/next' into zz/migrate-plonky3
zhenfeizhang Oct 10, 2025
2186419
fix some of the broken tests after merge
zhenfeizhang Oct 10, 2025
797f619
fix goldilocks test
zhenfeizhang Oct 10, 2025
5a50c83
Merge remote-tracking branch 'origin/next' into zz/migrate-plonky3
zhenfeizhang Dec 5, 2025
95c3f3a
wip
zhenfeizhang Dec 5, 2025
71295a8
wip
zhenfeizhang Dec 5, 2025
da23ba8
wip
zhenfeizhang Dec 5, 2025
fc7b6ec
fix core
zhenfeizhang Dec 5, 2025
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
530 changes: 489 additions & 41 deletions Cargo.lock

Large diffs are not rendered by default.

28 changes: 27 additions & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,10 @@ miden-utils-testing = { path = "./crates/test-utils", package = "miden-test-util
miden-verifier = { path = "./verifier", version = "0.20", default-features = false }

# Miden crates
miden-crypto = { version = "0.19", default-features = false }
# miden-crypto = { version = "0.17", default-features = false }

miden-crypto = { git = "https://github.com/0xMiden/crypto", branch = "zz/migrate-plonky3" }

miden-formatting = { version = "0.1", default-features = false }
midenc-hir-type = { version = "0.4", default-features = false }

Expand Down Expand Up @@ -89,3 +92,26 @@ winter-prover = { version = "0.13", default-features = false }
winter-rand-utils = "0.13"
winter-utils = { version = "0.13", default-features = false }
winter-verifier = { version = "0.13", default-features = false }

# Plonky3 dependencies
p3-air = { branch = "zz/migrate-plonky3", default-features = false, git = "https://github.com/0xMiden/Plonky3/" }
p3-blake3= { branch = "zz/migrate-plonky3", default-features = false, git = "https://github.com/0xMiden/Plonky3/" }
p3-challenger = { branch = "zz/migrate-plonky3", default-features = false, git = "https://github.com/0xMiden/Plonky3/" }
p3-commit = { branch = "zz/migrate-plonky3", default-features = false, git = "https://github.com/0xMiden/Plonky3/" }
p3-dft= { branch = "zz/migrate-plonky3", default-features = false, git = "https://github.com/0xMiden/Plonky3/" }
p3-field = { branch = "zz/migrate-plonky3", default-features = false, git = "https://github.com/0xMiden/Plonky3/" }
p3-fri = { branch = "zz/migrate-plonky3", default-features = false, git = "https://github.com/0xMiden/Plonky3/" }
p3-goldilocks = { branch = "zz/migrate-plonky3", default-features = false, git = "https://github.com/0xMiden/Plonky3/" }
p3-keccak = { branch = "zz/migrate-plonky3", default-features = false, git = "https://github.com/0xMiden/Plonky3/" }
p3-matrix= { branch = "zz/migrate-plonky3", default-features = false, git = "https://github.com/0xMiden/Plonky3/" }
p3-maybe-rayon= { branch = "zz/migrate-plonky3", default-features = false, git = "https://github.com/0xMiden/Plonky3/" }
p3-merkle-tree = { branch = "zz/migrate-plonky3", default-features = false, git = "https://github.com/0xMiden/Plonky3/" }
p3-poseidon2 = { branch = "zz/migrate-plonky3", default-features = false, git = "https://github.com/0xMiden/Plonky3/" }
p3-symmetric = { branch = "zz/migrate-plonky3", default-features = false, git = "https://github.com/0xMiden/Plonky3/" }
p3-uni-stark = { branch = "zz/migrate-plonky3", default-features = false, git = "https://github.com/0xMiden/Plonky3/" }
p3-util = { branch = "zz/migrate-plonky3", default-features = false, git = "https://github.com/0xMiden/Plonky3/" }


rand = { version = "0.9", default-features = false }
# [patch.crates-io]
# miden-crypto = { git = "https://github.com/0xMiden/crypto", branch = "zz/migrate-plonky3" }
9 changes: 9 additions & 0 deletions air/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,15 @@ winter-air.workspace = true
winter-prover.workspace = true
miden-utils-indexing.workspace = true

p3-air.workspace = true
p3-commit.workspace = true
p3-field.workspace = true
p3-matrix.workspace = true
p3-uni-stark.workspace = true

serde = { version = "1.0", features = ["derive"] }
bincode = "1.3"

[dev-dependencies]
criterion.workspace = true
proptest.workspace = true
Expand Down
8 changes: 4 additions & 4 deletions air/benches/enforce_stack_constraint.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,14 @@ use std::time::Duration;

use criterion::{Criterion, criterion_group, criterion_main};
use miden_air::{
Felt, FieldElement,
Felt,
stack::{
NUM_GENERAL_CONSTRAINTS, enforce_constraints, field_ops, io_ops,
op_flags::generate_evaluation_frame, overflow, stack_manipulation, system_ops, u32_ops,
},
trace::STACK_TRACE_OFFSET,
};
use miden_core::{Operation, ZERO};
use miden_core::{Operation, PrimeCharacteristicRing, ZERO};

fn enforce_stack_constraint(c: &mut Criterion) {
let mut group = c.benchmark_group("enforce_stack_constraint");
Expand All @@ -25,8 +25,8 @@ fn enforce_stack_constraint(c: &mut Criterion) {
+ NUM_GENERAL_CONSTRAINTS;

let mut frame = generate_evaluation_frame(Operation::Inv.op_code() as usize);
frame.current_mut()[STACK_TRACE_OFFSET] = Felt::new(89u64);
frame.next_mut()[STACK_TRACE_OFFSET] = Felt::new(89u64).inv();
frame.current_mut()[STACK_TRACE_OFFSET] = Felt::from_u64(89u64);
frame.next_mut()[STACK_TRACE_OFFSET] = Felt::from_u64(89u64).inverse_unwrap_zero();

let mut result = [ZERO; NUM_CONSTRAINTS];

Expand Down
2 changes: 1 addition & 1 deletion air/src/constraints/chiplets/bitwise/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ use crate::{
};

#[cfg(test)]
pub mod tests;
//pub mod tests;

// CONSTANTS
// ================================================================================================
Expand Down
6 changes: 3 additions & 3 deletions air/src/constraints/chiplets/hasher/mod.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
use alloc::vec::Vec;

use super::{EvaluationFrame, Felt, FieldElement, TransitionConstraintDegree};
use super::{EvaluationFrame, Felt, TransitionConstraintDegree};
use crate::{
ONE, ZERO,
trace::chiplets::{
Expand All @@ -14,7 +14,7 @@ use crate::{
};

#[cfg(test)]
mod tests;
//mod tests;

// CONSTANTs
// ================================================================================================
Expand Down Expand Up @@ -105,7 +105,7 @@ pub fn get_transition_constraint_count() -> usize {
/// by the caller and set to `Felt::ONE`
/// - The `transition_flag` indicates whether this is the last row this chiplet's execution trace,
/// and therefore the constraints should not be enforced.
pub fn enforce_constraints<E: FieldElement<BaseField = Felt>>(
pub fn enforce_constraints<E: ExtensionField<Felt>>(
frame: &EvaluationFrame<E>,
periodic_values: &[E],
result: &mut [E],
Expand Down
2 changes: 1 addition & 1 deletion air/src/constraints/chiplets/memory/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ use crate::{
};

#[cfg(test)]
mod tests;
//mod tests;

// CONSTANTS
// ================================================================================================
Expand Down
4 changes: 2 additions & 2 deletions air/src/constraints/chiplets/memory/tests.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
use alloc::vec::Vec;

use miden_core::{Felt, FieldElement, WORD_SIZE};
use miden_core::{Felt, WORD_SIZE};
use winter_rand_utils::rand_value;

use super::{
Expand Down Expand Up @@ -171,7 +171,7 @@ fn get_test_frame(
};
next[MEMORY_D0_COL_IDX] = Felt::new(delta as u16 as u64);
next[MEMORY_D1_COL_IDX] = Felt::new(delta >> 16);
next[MEMORY_D_INV_COL_IDX] = (Felt::new(delta)).inv();
next[MEMORY_D_INV_COL_IDX] = (Felt::new(delta)).inverse_unwrap_zero();

// since we're always writing a word, the idx0 and idx1 columns should be zero
next[MEMORY_IDX0_COL_IDX] = ZERO;
Expand Down
12 changes: 6 additions & 6 deletions air/src/constraints/chiplets/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ use alloc::vec::Vec;
use miden_core::{Word, precompile::PrecompileTranscriptState};

use super::super::{
CHIPLETS_OFFSET, EvaluationFrame, Felt, FieldElement, TransitionConstraintDegree,
CHIPLETS_OFFSET, EvaluationFrame, Felt, TransitionConstraintDegree,
};
use crate::{
Assertion, AuxRandElements,
Expand Down Expand Up @@ -50,13 +50,13 @@ pub fn get_aux_assertions_first_step<E>(
aux_rand_elements: &AuxRandElements<E>,
pc_transcript_state: PrecompileTranscriptState,
) where
E: FieldElement<BaseField = Felt>,
E: ExtensionField<Felt>,
{
let reduced_kernel_digests = reduce_kernel_digests(kernel_digests, aux_rand_elements);
result.push(Assertion::single(
CHIPLETS_BUS_AUX_TRACE_OFFSET,
0,
reduced_kernel_digests.inv(),
reduced_kernel_digests.inverse_unwrap_zero(),
));

// Anchor hasher vtable init against PI-provided transcript state (empty/final).
Expand Down Expand Up @@ -100,7 +100,7 @@ pub fn get_transition_constraint_count() -> usize {
}

/// Enforces constraints for the chiplets module and all chiplet components.
pub fn enforce_constraints<E: FieldElement<BaseField = Felt>>(
pub fn enforce_constraints<E: ExtensionField<Felt>>(
frame: &EvaluationFrame<E>,
periodic_values: &[E],
result: &mut [E],
Expand Down Expand Up @@ -274,7 +274,7 @@ impl<E: FieldElement> ChipletsFrameExt<E> for &EvaluationFrame<E> {
/// Reduces kernel procedures digests using auxiliary randomness.
fn reduce_kernel_digests<E>(kernel_digests: &[Word], aux_rand_elements: &AuxRandElements<E>) -> E
where
E: FieldElement<BaseField = Felt>,
E: ExtensionField<Felt>,
{
let alphas = aux_rand_elements.rand_elements();
kernel_digests.iter().fold(E::ONE, |acc, digest: &Word| {
Expand All @@ -284,7 +284,7 @@ where
.iter()
.skip(2)
.zip(digest.iter())
.map(|(alpha, coef)| alpha.mul_base(*coef))
.map(|(alpha, coef)| alpha.mul(*coef))
.fold(affine_term, |acc, term| acc + term);

acc * cur
Expand Down
10 changes: 6 additions & 4 deletions air/src/constraints/mod.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
/*
use super::{EvaluationFrame, ExtensionOf, Felt, FieldElement};
use crate::{
trace::{
Expand All @@ -17,8 +18,8 @@ pub mod stack;
/// calculations.
pub trait MainFrameExt<F, E>
where
F: FieldElement<BaseField = Felt>,
E: FieldElement<BaseField = Felt> + ExtensionOf<F>,
F: ExtensionField<Felt>,
E: ExtensionField<Felt> + ExtensionOf<F>,
{
/// Returns true when a u32 stack operation that requires range checks is being performed.
fn u32_rc_op(&self) -> F;
Expand Down Expand Up @@ -61,8 +62,8 @@ where

impl<F, E> MainFrameExt<F, E> for EvaluationFrame<F>
where
F: FieldElement<BaseField = Felt>,
E: FieldElement<BaseField = Felt> + ExtensionOf<F>,
F: ExtensionField<Felt>,
E: ExtensionField<Felt> + ExtensionOf<F>,
{
/// Returns true when the stack operation is a u32 operation that requires range checks.
/// TODO: this is also defined in the op flags. It's redefined here to avoid computing all of
Expand Down Expand Up @@ -106,3 +107,4 @@ where
alpha + self.current()[DECODER_USER_OP_HELPERS_OFFSET + 3].into()
}
}
*/
19 changes: 10 additions & 9 deletions air/src/constraints/range.rs
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
use alloc::vec::Vec;

/*
use miden_core::{ExtensionOf, ZERO};

use crate::{
Assertion, EvaluationFrame, Felt, FieldElement, TransitionConstraintDegree,
Assertion, EvaluationFrame, Felt, TransitionConstraintDegree,
chiplets::ChipletsFrameExt,
constraints::MainFrameExt,
trace::range::{B_RANGE_COL_IDX, M_COL_IDX, V_COL_IDX},
Expand Down Expand Up @@ -113,8 +113,8 @@ pub fn enforce_aux_constraints<F, E>(
aux_rand_elements: &[E],
result: &mut [E],
) where
F: FieldElement<BaseField = Felt>,
E: FieldElement<BaseField = Felt> + ExtensionOf<F>,
F: ExtensionField<Felt>,
E: ExtensionField<Felt> + ExtensionOf<F>,
{
// Get the first random element for this segment.
let alpha = aux_rand_elements[0];
Expand Down Expand Up @@ -159,8 +159,8 @@ fn enforce_b_range<E, F>(
alpha: E,
result: &mut [E],
) where
F: FieldElement<BaseField = Felt>,
E: FieldElement<BaseField = Felt> + ExtensionOf<F>,
F: ExtensionField<Felt>,
E: ExtensionField<Felt> + ExtensionOf<F>,
{
// The denominator values for the LogUp lookup.
let mv0: E = main_frame.lookup_mv0(alpha);
Expand All @@ -178,16 +178,16 @@ fn enforce_b_range<E, F>(
// operation with range checks. This value has degree 6.
let sflag_rc_mem: E = range_check
.mul(memory_lookups)
.mul_base(<EvaluationFrame<F> as MainFrameExt<F, E>>::u32_rc_op(main_frame));
.mul(<EvaluationFrame<F> as MainFrameExt<F, E>>::u32_rc_op(main_frame));
// An intermediate value required by all memory terms that includes the flag indicating the
// memory portion of the chiplets trace. This value has degree 8.
let mflag_rc_stack: E =
range_check.mul(stack_lookups).mul_base(main_frame.chiplets_memory_flag());
range_check.mul(stack_lookups).mul(main_frame.chiplets_memory_flag());

// The terms for the LogUp check after all denominators have been multiplied in.
let b_next_term = aux_frame.b_range_next().mul(lookups); // degree 8
let b_term = aux_frame.b_range().mul(lookups); // degree 8
let rc_term = stack_lookups.mul(memory_lookups).mul_base(main_frame.multiplicity()); // degree 7
let rc_term = stack_lookups.mul(memory_lookups).mul(main_frame.multiplicity()); // degree 7
let s0_term = sflag_rc_mem.mul(sv1).mul(sv2).mul(sv3); // degree 9
let s1_term = sflag_rc_mem.mul(sv0).mul(sv2).mul(sv3); // degree 9
let s2_term = sflag_rc_mem.mul(sv0).mul(sv1).mul(sv3); // degree 9
Expand Down Expand Up @@ -255,3 +255,4 @@ impl<E: FieldElement> EvaluationFrameExt<E> for &EvaluationFrame<E> {
self.next()[column] - self.current()[column]
}
}
*/
6 changes: 3 additions & 3 deletions air/src/constraints/stack/field_ops/mod.rs
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
use alloc::vec::Vec;

use super::{EvaluationFrame, FieldElement, TransitionConstraintDegree, op_flags::OpFlags};
use super::{EvaluationFrame, TransitionConstraintDegree, op_flags::OpFlags};
use crate::{
stack::EvaluationFrameExt,
utils::{are_equal, is_binary},
};

#[cfg(test)]
pub mod tests;
//pub mod tests;

// CONSTANTS
// ================================================================================================
Expand Down Expand Up @@ -67,7 +67,7 @@ pub fn enforce_constraints<E: FieldElement>(
index += enforce_mul_constraints(frame, &mut result[index..], op_flag.mul());

// Enforce constaints of the INV operation.
index += enforce_inv_constraints(frame, &mut result[index..], op_flag.inv());
index += enforce_inv_constraints(frame, &mut result[index..], op_flag.inverse_unwrap_zero());

// Enforce constaints of the INCR operation.
index += enforce_incr_constraints(frame, &mut result[index..], op_flag.incr());
Expand Down
8 changes: 4 additions & 4 deletions air/src/constraints/stack/field_ops/tests.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
use core::ops::Neg;

use miden_core::{Felt, FieldElement, ONE, Operation, ZERO};
use miden_core::{Felt, ONE, Operation, ZERO};
use proptest::prelude::*;
use winter_rand_utils::rand_value;

Expand Down Expand Up @@ -260,7 +260,7 @@ pub fn get_eqz_test_frame(a: u64) -> EvaluationFrame<Felt> {
},
_ => {
frame.current_mut()[STACK_TRACE_OFFSET] = Felt::new(a);
frame.current_mut()[DECODER_TRACE_OFFSET + USER_OP_HELPERS_OFFSET] = Felt::new(a).inv();
frame.current_mut()[DECODER_TRACE_OFFSET + USER_OP_HELPERS_OFFSET] = Felt::new(a).inverse_unwrap_zero();
frame.next_mut()[STACK_TRACE_OFFSET] = ZERO;
},
}
Expand Down Expand Up @@ -291,7 +291,7 @@ pub fn get_inv_test_frame(a: u64) -> EvaluationFrame<Felt> {
// Set the output. First element in the next frame should be the inverse of
// the first element of the current frame.
frame.current_mut()[STACK_TRACE_OFFSET] = Felt::new(a);
frame.next_mut()[STACK_TRACE_OFFSET] = Felt::new(a).inv();
frame.next_mut()[STACK_TRACE_OFFSET] = Felt::new(a).inverse_unwrap_zero();

frame
}
Expand Down Expand Up @@ -360,7 +360,7 @@ pub fn get_eq_test_frame(a: u64, b: u64) -> EvaluationFrame<Felt> {
frame.current_mut()[STACK_TRACE_OFFSET] = Felt::new(a);
frame.current_mut()[STACK_TRACE_OFFSET + 1] = Felt::new(b);
frame.current_mut()[DECODER_TRACE_OFFSET + USER_OP_HELPERS_OFFSET] =
(Felt::new(a) - Felt::new(b)).inv();
(Felt::new(a) - Felt::new(b)).inverse_unwrap_zero();
frame.next_mut()[STACK_TRACE_OFFSET] = ZERO;
}

Expand Down
4 changes: 2 additions & 2 deletions air/src/constraints/stack/io_ops/mod.rs
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
use alloc::vec::Vec;

use super::{EvaluationFrame, FieldElement, TransitionConstraintDegree, op_flags::OpFlags};
use super::{EvaluationFrame, TransitionConstraintDegree, op_flags::OpFlags};
use crate::{stack::EvaluationFrameExt, utils::are_equal};

#[cfg(test)]
pub mod tests;
//pub mod tests;

// CONSTANTS
// ================================================================================================
Expand Down
Loading
Loading