|
7 | 7 |
|
8 | 8 | use alloc::vec::Vec; |
9 | 9 |
|
10 | | -use miden_ace_codegen::{AceCircuit, AceConfig, AceError, build_multi_air_ace_circuit}; |
11 | | -use miden_core::field::QuadFelt; |
| 10 | +use miden_ace_codegen::{AceCircuit, AceConfig, AceError, LayoutKind, build_multi_air_ace_circuit}; |
| 11 | +use miden_core::{Felt, field::QuadFelt}; |
12 | 12 |
|
13 | | -use crate::session::ChipletAir; |
| 13 | +use crate::session::{ChipletAir, NUM_CHIPLETS}; |
14 | 14 |
|
15 | 15 | // MULTI-AIR ACE CIRCUIT |
16 | 16 | // ================================================================================================ |
17 | 17 |
|
| 18 | +/// Per-AIR trace regions are padded to this width before concatenation, matching the LMCS wire |
| 19 | +/// alignment used by the commitment scheme. |
| 20 | +const LMCS_ALIGNMENT: usize = 8; |
| 21 | + |
| 22 | +/// Number of quotient chunks the precompile relation commits to. |
| 23 | +/// |
| 24 | +/// The lifted STARK verifier derives this quantity symbolically from the AIRs. Deriving it through |
| 25 | +/// the same implementation keeps the ACE circuit's READ layout coupled to the proof protocol. |
| 26 | +fn num_quotient_chunks() -> usize { |
| 27 | + let max_log_quotient_degree = ChipletAir::all() |
| 28 | + .iter() |
| 29 | + .map(miden_lifted_stark::log_quotient_degree::<Felt, QuadFelt, ChipletAir>) |
| 30 | + .max() |
| 31 | + .expect("the chiplet stack is non-empty"); |
| 32 | + 1usize << max_log_quotient_degree |
| 33 | +} |
| 34 | + |
| 35 | +/// ACE codegen settings for the precompile chiplet relation. |
| 36 | +fn precompile_ace_config() -> AceConfig { |
| 37 | + AceConfig { |
| 38 | + num_quotient_chunks: num_quotient_chunks(), |
| 39 | + layout: LayoutKind::Masm, |
| 40 | + num_airs: NUM_CHIPLETS, |
| 41 | + } |
| 42 | +} |
| 43 | + |
18 | 44 | /// Builds the ACE circuit for the precompile chiplet multi-AIR relation. |
19 | 45 | /// |
20 | 46 | /// The circuit uses the stable [`ChipletAir::all`] instance order as its canonical ACE fold order |
21 | 47 | /// and aligns trace regions to eight base-field elements. These choices define the committed ACE |
22 | 48 | /// encoding; they do not prescribe the lifted STARK proof order. The cross-chiplet LogUp identity |
23 | 49 | /// is checked separately by `ChipletMultiAir::eval_external`. |
24 | | -pub fn build_precompile_multi_air_ace_circuit( |
25 | | - config: AceConfig, |
26 | | -) -> Result<AceCircuit<QuadFelt>, AceError> { |
27 | | - const LMCS_ALIGNMENT: usize = 8; |
28 | | - |
| 50 | +pub fn build_precompile_multi_air_ace_circuit() -> Result<AceCircuit<QuadFelt>, AceError> { |
29 | 51 | let airs = ChipletAir::all(); |
30 | 52 | let proof_order: Vec<_> = (0..airs.len()).collect(); |
31 | 53 |
|
32 | | - build_multi_air_ace_circuit(&airs, &proof_order, config, LMCS_ALIGNMENT) |
| 54 | + build_multi_air_ace_circuit::<ChipletAir>( |
| 55 | + &airs, |
| 56 | + &proof_order, |
| 57 | + precompile_ace_config(), |
| 58 | + LMCS_ALIGNMENT, |
| 59 | + ) |
33 | 60 | } |
34 | 61 |
|
35 | 62 | #[cfg(test)] |
36 | 63 | mod tests { |
37 | | - use miden_ace_codegen::{AceConfig, LayoutKind}; |
| 64 | + use alloc::{format, string::String, vec::Vec}; |
| 65 | + |
| 66 | + use miden_core::{Felt, field::QuadFelt}; |
38 | 67 |
|
39 | | - use super::build_precompile_multi_air_ace_circuit; |
40 | | - use crate::session::NUM_CHIPLETS; |
| 68 | + use super::{build_precompile_multi_air_ace_circuit, precompile_ace_config}; |
| 69 | + use crate::session::{ChipletAir, NUM_CHIPLETS}; |
41 | 70 |
|
42 | 71 | #[test] |
43 | 72 | fn precompile_multi_air_ace_circuit_builds() { |
44 | | - let config = AceConfig { |
45 | | - num_quotient_chunks: 8, |
46 | | - layout: LayoutKind::Masm, |
47 | | - num_airs: NUM_CHIPLETS, |
48 | | - }; |
49 | | - |
50 | | - let circuit = build_precompile_multi_air_ace_circuit(config) |
51 | | - .expect("precompile multi-AIR ACE circuit"); |
| 73 | + let circuit = |
| 74 | + build_precompile_multi_air_ace_circuit().expect("precompile multi-AIR ACE circuit"); |
52 | 75 | assert_eq!(circuit.layout().counts.num_public, crate::logup::NUM_PUBLIC_VALUES); |
53 | 76 | assert_eq!(circuit.layout().counts.num_aux_boundary, NUM_CHIPLETS); |
54 | 77 | assert!(circuit.layout().counts.preprocessed_width >= 8); |
55 | 78 | } |
| 79 | + |
| 80 | + /// Pin the complete quotient-degree vector, not merely its maximum: otherwise a chiplet could |
| 81 | + /// drift between degrees while another chiplet kept the relation-wide maximum unchanged. |
| 82 | + #[test] |
| 83 | + fn quotient_chunks_match_the_symbolic_derivation() { |
| 84 | + const EXPECTED: [(&str, u8); NUM_CHIPLETS] = [ |
| 85 | + ("ChunkNodeSponge", 2), |
| 86 | + ("Poseidon2", 2), |
| 87 | + ("KeccakRound", 2), |
| 88 | + ("BytePairLut", 1), |
| 89 | + ("TranscriptEval", 1), |
| 90 | + ("UintStoreMul", 1), |
| 91 | + ("UintAdd", 1), |
| 92 | + ("EcPointStoreGroups", 1), |
| 93 | + ("EcGroupAdd", 1), |
| 94 | + ("EcMsm", 1), |
| 95 | + ]; |
| 96 | + |
| 97 | + let derived: Vec<(String, u8)> = ChipletAir::all() |
| 98 | + .iter() |
| 99 | + .map(|air| { |
| 100 | + ( |
| 101 | + format!("{air:?}"), |
| 102 | + miden_lifted_stark::log_quotient_degree::<Felt, QuadFelt, ChipletAir>(air), |
| 103 | + ) |
| 104 | + }) |
| 105 | + .collect(); |
| 106 | + let expected: Vec<(String, u8)> = |
| 107 | + EXPECTED.iter().map(|(name, degree)| ((*name).into(), *degree)).collect(); |
| 108 | + assert_eq!( |
| 109 | + derived, expected, |
| 110 | + "a chiplet's quotient degree moved; if intended, re-mint the relation digest" |
| 111 | + ); |
| 112 | + |
| 113 | + let max = derived.iter().map(|(_, degree)| *degree).max().expect("non-empty stack"); |
| 114 | + let expected_chunks = 1usize << max; |
| 115 | + assert_eq!( |
| 116 | + precompile_ace_config().num_quotient_chunks, |
| 117 | + expected_chunks, |
| 118 | + "the ACE circuit must read exactly the quotient chunks the proof carries" |
| 119 | + ); |
| 120 | + let circuit = |
| 121 | + build_precompile_multi_air_ace_circuit().expect("precompile multi-AIR ACE circuit"); |
| 122 | + assert_eq!( |
| 123 | + circuit.layout().counts.num_quotient_chunks, |
| 124 | + expected_chunks, |
| 125 | + "the built circuit must preserve the derived quotient arity" |
| 126 | + ); |
| 127 | + } |
56 | 128 | } |
0 commit comments