refactor(air): remove tagging, apply uniform constraint description, and optimize evaluation

.github/workflows/test.yml

@@ -81,6 +81,21 @@ jobs:
             echo "No documentation changes in crates/lib/core/docs/ - OK"
           fi
 
+  check-constraints:
+    name: check recursive constraint artifacts
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Cleanup large tools for build space
+        uses: ./.github/actions/cleanup-runner
+      - uses: Swatinem/rust-cache@v2
+        with:
+          save-if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/next' }}
+      - name: Install rust
+        run: rustup update --no-self-update
+      - name: Check recursive constraint artifacts for drift
+        run: make check-constraints
+
   run-examples:
     name: run masm examples
     runs-on: warp-ubuntu-latest-x64-4x

.gitignore

@@ -24,3 +24,7 @@ crates/lib/core/assets/core.masl
 
 # mdBook
 book/
+
+# Constraint analysis tooling
+.constraint-tooling/
+scripts/__pycache__/

CHANGELOG.md

@@ -28,6 +28,8 @@
 - Documented non-overlap requirement for `memcopy_words`, `memcopy_elements`, and AEAD encrypt/decrypt procedures ([#2941](https://github.com/0xMiden/miden-vm/pull/2941)).
 - Added chainable `Test` builders for common test setup in `miden-utils-testing` ([#2957](https://github.com/0xMiden/miden-vm/pull/2957)).
 - Speed-up AUX range check trace generation by changing divisors to a flat Vec layout ([#2966](https://github.com/0xMiden/miden-vm/pull/2966)).
+- Removed AIR constraint tagging instrumentation, applied a uniform constraint description style across components, and optimized constraint evaluation ([#2856](https://github.com/0xMiden/miden-vm/pull/2856)).
+
 ## 0.22.1
 
 #### Enhancements

Makefile

@@ -19,6 +19,8 @@ help:
 	@printf "  make test-prover                 # Test prover crate\n"
 	@printf "  make test-core-lib               # Test core-lib crate\n"
 	@printf "  make test-verifier               # Test verifier crate\n"
+	@printf "  make check-constraints          # Check core-lib constraint artifacts\n"
+	@printf "  make regenerate-constraints      # Regenerate core-lib constraint artifacts\n"
 	@printf "\nExamples:\n"
 	@printf "  make test-air test=\"some_test\" # Test specific function\n"
 	@printf "  make test-fast                   # Fast tests (no proptests/CLI)\n"
@@ -220,6 +222,14 @@ exec-avx2: ## Builds an executable with AVX2 acceleration enabled
 exec-sve: ## Builds an executable with SVE acceleration enabled
 	RUSTFLAGS="-C target-feature=+sve" cargo build --profile optimized $(FEATURES_CONCURRENT_EXEC)
 
+.PHONY: regenerate-constraints
+regenerate-constraints: ## Regenerate core-lib constraint artifacts
+	cargo run --package miden-core-lib --features constraints-tools --bin regenerate-constraints -- --write
+
+.PHONY: check-constraints
+check-constraints: ## Check core-lib constraint artifacts for drift
+	cargo run --package miden-core-lib --features constraints-tools --bin regenerate-constraints -- --check
+
 .PHONY: exec-info
 exec-info: ## Builds an executable with log tree enabled
 	cargo build --profile optimized $(FEATURES_LOG_TREE)

air/Cargo.toml

@@ -35,5 +35,6 @@ thiserror.workspace = true
 tracing.workspace = true
 
 [dev-dependencies]
+insta.workspace = true
 miden-ace-codegen = { workspace = true, features = ["testing"] }
 proptest.workspace = true

air/src/ace.rs

@@ -49,8 +49,9 @@ pub enum MessageElement {
 pub enum ProductFactor {
     /// Claimed final value of an auxiliary trace column, by column index.
     BusBoundary(usize),
-    /// A bus message computed from its elements as `alpha + sum(beta^i * elements[i])`.
-    Message(Vec<MessageElement>),
+    /// A bus message computed from its elements as `bus_prefix[bus] + sum(beta^i * elements[i])`.
+    /// The first field is the bus type index (see `trace::bus_types`).
+    Message(usize, Vec<MessageElement>),
     /// Multiset product reduced from variable-length public inputs, by group index.
     Vlpi(usize),
 }
@@ -131,7 +132,7 @@ where
     for factor in factors {
         let node = match factor {
             ProductFactor::BusBoundary(idx) => builder.input(InputKey::AuxBusBoundary(*idx)),
-            ProductFactor::Message(elements) => encode_bus_message(builder, elements),
+            ProductFactor::Message(bus, elements) => encode_bus_message(builder, *bus, elements),
             ProductFactor::Vlpi(idx) => builder.input(InputKey::VlpiReduction(*idx)),
         };
         acc = builder.mul(acc, node);
@@ -154,20 +155,38 @@ where
     sum
 }
 
-/// Encode a bus message as `alpha + sum(beta^i * elements[i])`.
-fn encode_bus_message<EF>(builder: &mut DagBuilder<EF>, elements: &[MessageElement]) -> NodeId
+/// Encode a bus message as `bus_prefix[bus] + sum(beta^i * elements[i])`.
+///
+/// The bus prefix provides domain separation: `bus_prefix[bus] = alpha + (bus+1) * gamma`
+/// where `gamma = beta^MAX_MESSAGE_WIDTH`. This matches [`trace::Challenges::encode`].
+fn encode_bus_message<EF>(
+    builder: &mut DagBuilder<EF>,
+    bus: usize,
+    elements: &[MessageElement],
+) -> NodeId
 where
     EF: ExtensionField<Felt>,
 {
     let alpha = builder.input(InputKey::AuxRandAlpha);
     let beta = builder.input(InputKey::AuxRandBeta);
 
-    // acc = alpha + sum(beta^i * elem_i)
+    // Compute gamma = beta^MAX_MESSAGE_WIDTH.
+    let mut gamma = builder.constant(EF::ONE);
+    for _ in 0..trace::MAX_MESSAGE_WIDTH {
+        gamma = builder.mul(gamma, beta);
+    }
+
+    // bus_prefix = alpha + (bus + 1) * gamma
+    let scale = builder.constant(EF::from(Felt::from_u32((bus as u32) + 1)));
+    let offset = builder.mul(gamma, scale);
+    let bus_prefix = builder.add(alpha, offset);
+
+    // acc = bus_prefix + sum(beta^i * elem_i)
     //
     // Beta powers are built incrementally. The DagBuilder is hash-consed, so
     // identical beta^i nodes across multiple message encodings are shared
     // automatically.
-    let mut acc = alpha;
+    let mut acc = bus_prefix;
     let mut beta_power = builder.constant(EF::ONE);
     for elem in elements {
         let node = match elem {
@@ -190,6 +209,7 @@ where
 pub fn reduced_aux_batch_config() -> ReducedAuxBatchConfig {
     use MessageElement::{Constant, PublicInput};
     use ProductFactor::{BusBoundary, Message, Vlpi};
+    use trace::bus_types;
 
     // Aux boundary column indices.
     let p1 = trace::DECODER_AUX_TRACE_OFFSET;
@@ -251,10 +271,10 @@ pub fn reduced_aux_batch_config() -> ReducedAuxBatchConfig {
             BusBoundary(s_aux),
             BusBoundary(b_hash_kernel),
             BusBoundary(b_chiplets),
-            Message(ph_msg),
-            Message(default_msg),
+            Message(bus_types::BLOCK_HASH_TABLE, ph_msg),
+            Message(bus_types::LOG_PRECOMPILE_TRANSCRIPT, default_msg),
         ],
-        denominator: vec![Message(final_msg), Vlpi(0)],
+        denominator: vec![Message(bus_types::LOG_PRECOMPILE_TRANSCRIPT, final_msg), Vlpi(0)],
         sum_columns: vec![b_range, v_wiring],
     }
 }

air/src/config.rs

@@ -85,10 +85,10 @@ pub fn pcs_params() -> PcsParams {
 /// Compile-time constant binding the Fiat-Shamir transcript to the Miden VM AIR.
 /// Must match the constants in `crates/lib/core/asm/sys/vm/mod.masm`.
 pub const RELATION_DIGEST: [Felt; 4] = [
-    Felt::new(14932224741264950205),
-    Felt::new(13231194489255299102),
-    Felt::new(9539190039789656767),
-    Felt::new(16072183680659208914),
+    Felt::new(789474107508207355),
+    Felt::new(6700560344624007800),
+    Felt::new(10413623302183279352),
+    Felt::new(1269032160905630127),
 ];
 
 /// Observes PCS protocol parameters and per-proof trace height into the challenger.
@@ -293,3 +293,59 @@ pub fn keccak_config(params: PcsParams) -> MidenStarkConfig<KeccakLmcs, KeccakCh
     challenger.observe_slice(&RELATION_DIGEST);
     GenericStarkConfig::new(params, lmcs, Radix2DitParallel::default(), challenger)
 }
+
+#[cfg(test)]
+mod tests {
+    extern crate alloc;
+    use alloc::vec::Vec;
+
+    use miden_ace_codegen::{AceConfig, LayoutKind};
+    use miden_core::{Felt, crypto::hash::Poseidon2, field::QuadFelt};
+
+    use crate::{ProcessorAir, ace};
+
+    const PROTOCOL_ID: u64 = 0;
+    const REGEN_HINT: &str = "cargo run -p miden-core-lib --features constraints-tools --bin regenerate-constraints -- --write";
+
+    /// Snapshot test: catches any AIR change that alters the constraint circuit.
+    ///
+    /// If this test fails, regenerate with:
+    ///   cargo run -p miden-core-lib --features constraints-tools --bin regenerate-constraints --
+    /// --write
+    #[test]
+    fn relation_digest_matches_current_air() {
+        let config = AceConfig {
+            num_quotient_chunks: 8,
+            num_vlpi_groups: 1,
+            layout: LayoutKind::Masm,
+        };
+        let air = ProcessorAir;
+        let batch_config = ace::reduced_aux_batch_config();
+        let circuit =
+            ace::build_batched_ace_circuit::<_, QuadFelt>(&air, config, &batch_config).unwrap();
+        let encoded = circuit.to_ace().unwrap();
+        let circuit_commitment: [Felt; 4] = encoded.circuit_hash().into();
+
+        let input: Vec<Felt> = core::iter::once(Felt::new(PROTOCOL_ID))
+            .chain(circuit_commitment.iter().copied())
+            .collect();
+        let digest = Poseidon2::hash_elements(&input);
+        let expected: Vec<u64> =
+            digest.as_elements().iter().map(|f| f.as_canonical_u64()).collect();
+
+        let snapshot = format!(
+            "num_inputs: {}\nnum_eval_gates: {}\nrelation_digest: {:?}",
+            encoded.num_vars(),
+            encoded.num_eval_rows(),
+            expected,
+        );
+        insta::assert_snapshot!(snapshot);
+
+        let actual: Vec<u64> =
+            super::RELATION_DIGEST.iter().map(|f| f.as_canonical_u64()).collect();
+        assert_eq!(
+            actual, expected,
+            "RELATION_DIGEST in config.rs is stale. Regenerate with: {REGEN_HINT}"
+        );
+    }
+}

air/src/constraints/bus.rs

@@ -10,7 +10,6 @@
 //! - v_wiring (ACE wiring LogUp)
 
 /// Auxiliary trace column indices.
-#[allow(dead_code)]
 pub mod indices {
     /// Block stack table (decoder control flow)
     pub const P1_BLOCK_STACK: usize = 0;