Skip to content
Merged
Show file tree
Hide file tree
Changes from all 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
2 changes: 2 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,8 @@
#### Bug Fixes

- Reverted `InvokeKind::ProcRef` back to `InvokeKind::Exec` in `visit_mut_procref` and added an explanatory comment (#2893).
- Fixed the release dry-run publish cycle between `miden-air` and `miden-ace-codegen`, and preserved leaf-only DAG imports with explicit snapshots ([#2931](https://github.com/0xMiden/miden-vm/pull/2931)).

#### Changes

- Documented that enum variants are module-level constants and must be unique within a module (#2932).
Expand Down
1 change: 0 additions & 1 deletion Cargo.lock

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

1 change: 1 addition & 0 deletions air/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -35,4 +35,5 @@ thiserror.workspace = true
tracing.workspace = true

[dev-dependencies]
miden-ace-codegen = { workspace = true, features = ["testing"] }
proptest.workspace = true
4 changes: 2 additions & 2 deletions air/src/ace.rs
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ where
EF: ExtensionField<Felt>,
{
let constraint_root = constraint_dag.root;
let mut builder = DagBuilder::from_nodes(constraint_dag.nodes);
let mut builder = DagBuilder::from_dag(constraint_dag);

// Build product_check.
let product_check = build_product_check(&mut builder, config);
Expand All @@ -109,7 +109,7 @@ where
let partial = builder.add(constraint_root, term2);
let root = builder.add(partial, term3);

AceDag { nodes: builder.into_nodes(), root }
builder.build(root)
}

/// Build the running-product identity check.
Expand Down
185 changes: 185 additions & 0 deletions air/tests/ace_codegen.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,185 @@
use miden_ace_codegen::{
AceConfig, AceError, EXT_DEGREE, InputKey, LayoutKind, build_ace_circuit_for_air,
build_ace_dag_for_air, emit_circuit,
testing::{
eval_dag, eval_folded_constraints, eval_periodic_values, eval_quotient, fill_inputs,
zps_for_chunk,
},
};
use miden_air::{LiftedAir, ProcessorAir};
use miden_core::{Felt, field::QuadFelt};
use miden_crypto::{
field::{Field, PrimeCharacteristicRing},
stark::air::symbolic::{AirLayout, SymbolicAirBuilder},
};

#[test]
fn processor_air_dag_matches_manual_eval() {
let air = ProcessorAir;
let config = AceConfig {
num_quotient_chunks: 2,
num_vlpi_groups: 0,
layout: LayoutKind::Native,
};
let artifacts = build_ace_dag_for_air::<_, Felt, QuadFelt>(&air, config).unwrap();
let layout = artifacts.layout.clone();
let inputs: Vec<QuadFelt> = fill_inputs(&layout);
let z_k = inputs[layout.index(InputKey::ZK).unwrap()];
let periodic_values = eval_periodic_values::<Felt, QuadFelt>(
&LiftedAir::<Felt, QuadFelt>::periodic_columns(&air),
z_k,
);

let air_layout = AirLayout {
preprocessed_width: 0,
main_width: layout.counts.width,
num_public_values: layout.counts.num_public,
permutation_width: layout.counts.aux_width,
num_permutation_challenges: layout.counts.num_randomness,
num_permutation_values: LiftedAir::<Felt, QuadFelt>::num_aux_values(&air),
num_periodic_columns: layout.counts.num_periodic,
};
let mut builder = SymbolicAirBuilder::<Felt, QuadFelt>::new(air_layout);
LiftedAir::<Felt, QuadFelt>::eval(&air, &mut builder);

let acc = eval_folded_constraints(
&builder.base_constraints(),
&builder.extension_constraints(),
&builder.constraint_layout(),
&inputs,
&layout,
&periodic_values,
);
let z_pow_n = inputs[layout.index(InputKey::ZPowN).unwrap()];
let vanishing = z_pow_n - QuadFelt::ONE;
let expected = acc - eval_quotient::<Felt, QuadFelt>(&layout, &inputs) * vanishing;

let actual = eval_dag(&artifacts.dag, &inputs, &layout).unwrap();
assert_eq!(actual, expected);
}

#[test]
fn processor_air_dag_rejects_mismatched_layout() {
let air = ProcessorAir;
let dag_config = AceConfig {
num_quotient_chunks: 8,
num_vlpi_groups: 0,
layout: LayoutKind::Native,
};
let layout_config = AceConfig {
num_quotient_chunks: 1,
num_vlpi_groups: 0,
layout: LayoutKind::Native,
};

let dag = build_ace_dag_for_air::<_, Felt, QuadFelt>(&air, dag_config).unwrap().dag;
let wrong_layout =
build_ace_dag_for_air::<_, Felt, QuadFelt>(&air, layout_config).unwrap().layout;
let inputs: Vec<QuadFelt> = fill_inputs(&wrong_layout);

let err = eval_dag(&dag, &inputs, &wrong_layout).unwrap_err();
assert!(
matches!(err, AceError::InvalidInputLayout { .. }),
"expected InvalidInputLayout, got {err:?}"
);
}

#[test]
#[allow(clippy::print_stdout)]
fn processor_air_chiplet_rows() {
let air = ProcessorAir;
let config = AceConfig {
num_quotient_chunks: 8,
num_vlpi_groups: 1,
layout: LayoutKind::Masm,
};

let circuit = build_ace_circuit_for_air::<_, Felt, QuadFelt>(&air, config).unwrap();
let encoded = circuit.to_ace().unwrap();
let read_rows = encoded.num_read_rows();
let eval_rows = encoded.num_eval_rows();
let total_rows = read_rows + eval_rows;

println!(
"ACE chiplet rows (ProcessorAir): read={}, eval={}, total={}, inputs={}, constants={}, nodes={}",
read_rows,
eval_rows,
total_rows,
encoded.num_inputs(),
encoded.num_constants(),
encoded.num_nodes()
);
}

#[test]
fn synthetic_ood_adjusts_quotient_to_zero() {
let config = AceConfig {
num_quotient_chunks: 8,
num_vlpi_groups: 0,
layout: LayoutKind::Masm,
};

let artifacts =
build_ace_dag_for_air::<_, Felt, QuadFelt>(&ProcessorAir, config).expect("ace dag");
let circuit = emit_circuit(&artifacts.dag, artifacts.layout.clone()).expect("ace circuit");

let mut inputs: Vec<QuadFelt> = fill_inputs(&artifacts.layout);
let root = circuit.eval(&inputs).expect("circuit eval");

let z_pow_n = inputs[artifacts.layout.index(InputKey::ZPowN).unwrap()];
let vanishing = z_pow_n - QuadFelt::ONE;
let zps_0 = zps_for_chunk::<Felt, QuadFelt>(&artifacts.layout, &inputs, 0);
let delta = root * (zps_0 * vanishing).inverse();

let idx = artifacts
.layout
.index(InputKey::QuotientChunkCoord { offset: 0, chunk: 0, coord: 0 })
.unwrap();
inputs[idx] += delta;

let result = circuit.eval(&inputs).expect("circuit eval");
assert!(result.is_zero(), "ACE circuit must evaluate to zero");
}

#[test]
fn quotient_next_inputs_do_not_affect_eval() {
let config = AceConfig {
num_quotient_chunks: 8,
num_vlpi_groups: 0,
layout: LayoutKind::Masm,
};

let artifacts =
build_ace_dag_for_air::<_, Felt, QuadFelt>(&ProcessorAir, config).expect("ace dag");
let circuit = emit_circuit(&artifacts.dag, artifacts.layout.clone()).expect("ace circuit");

let mut inputs: Vec<QuadFelt> = fill_inputs(&artifacts.layout);

let root = circuit.eval(&inputs).expect("circuit eval");
let z_pow_n = inputs[artifacts.layout.index(InputKey::ZPowN).unwrap()];
let vanishing = z_pow_n - QuadFelt::ONE;
let zps_0 = zps_for_chunk::<Felt, QuadFelt>(&artifacts.layout, &inputs, 0);
let delta = root * (zps_0 * vanishing).inverse();
let idx = artifacts
.layout
.index(InputKey::QuotientChunkCoord { offset: 0, chunk: 0, coord: 0 })
.unwrap();
inputs[idx] += delta;
assert!(
circuit.eval(&inputs).expect("circuit eval").is_zero(),
"precondition: zero root"
);

for chunk in 0..artifacts.layout.counts.num_quotient_chunks {
for coord in 0..EXT_DEGREE {
let idx = artifacts
.layout
.index(InputKey::QuotientChunkCoord { offset: 1, chunk, coord })
.unwrap();
inputs[idx] += QuadFelt::from(Felt::new(123 + (chunk * 7 + coord) as u64));
}
}

let result = circuit.eval(&inputs).expect("circuit eval");
assert!(result.is_zero(), "quotient_next should not affect ACE eval");
}
4 changes: 3 additions & 1 deletion crates/ace-codegen/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -13,11 +13,13 @@ repository.workspace = true
rust-version.workspace = true
edition.workspace = true

[features]
testing = []

[dependencies]
miden-core = { workspace = true }
miden-crypto = { workspace = true }
thiserror = { workspace = true }

[dev-dependencies]
miden-air = { workspace = true, features = ["std"] }
miden-core = { workspace = true, features = ["std"] }
10 changes: 6 additions & 4 deletions crates/ace-codegen/src/circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -96,12 +96,14 @@ where
let mut constants = Vec::new();
let mut constant_map = HashMap::<EF, usize>::new();
let mut operations = Vec::new();
let mut node_map: Vec<Option<AceNode>> = vec![None; dag.nodes.len()];
let mut node_map: Vec<Option<AceNode>> = vec![None; dag.nodes().len()];

for (idx, node) in dag.nodes.iter().enumerate() {
for (idx, node) in dag.nodes().iter().enumerate() {
let ace_node = match node {
NodeKind::Input(key) => {
let input_idx = layout.index(*key).expect("input key must be present in layout");
let input_idx = layout.index(*key).ok_or_else(|| AceError::InvalidInputLayout {
message: format!("missing input key in layout: {key:?}"),
})?;
AceNode::Input(input_idx)
},
NodeKind::Constant(value) => {
Expand Down Expand Up @@ -150,7 +152,7 @@ where
node_map[idx] = Some(ace_node);
}

let root = lookup_node(&node_map, dag.root);
let root = lookup_node(&node_map, dag.root());
Ok(AceCircuit { layout, constants, operations, root })
}

Expand Down
Loading
Loading