miden-ace-codegen 0.22.1

ACE circuit codegen for Plonky3-based Miden AIRs.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89

//! Synthetic OOD tests derived from the air-script ACE test strategy.
//!
//! The air-script tests correct a random quotient so the ACE circuit evaluates
//! to zero. Here we apply the same idea to the Miden VM quotient recomposition
//! (barycentric chunk kernel) and keep the tests independent of the prover.

use miden_air::ProcessorAir;
use miden_core::{Felt, field::QuadFelt};
use miden_crypto::field::Field;

use super::common::{eval_quotient, fill_inputs, zps_for_chunk};
use crate::{
    AceConfig, EXT_DEGREE, InputKey, LayoutKind, circuit::emit_circuit,
    pipeline::build_ace_dag_for_air,
};

#[test]
fn synthetic_ood_adjusts_quotient_to_zero() {
    let config = AceConfig {
        num_quotient_chunks: 8,
        num_aux_inputs: 14,
        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 = fill_inputs(&artifacts.layout);
    let root = circuit.eval(&inputs).expect("circuit eval");

    let zps_0 = zps_for_chunk(&artifacts.layout, &inputs, 0);
    let delta = root * zps_0.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");

    // Sanity check: recomposition is well-defined and stable.
    let quotient = eval_quotient(&artifacts.layout, &inputs);
    assert_eq!(quotient, eval_quotient(&artifacts.layout, &inputs));
}

#[test]
fn quotient_next_inputs_do_not_affect_eval() {
    let config = AceConfig {
        num_quotient_chunks: 8,
        num_aux_inputs: 14,
        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 = fill_inputs(&artifacts.layout);

    let root = circuit.eval(&inputs).expect("circuit eval");
    let zps_0 = zps_for_chunk(&artifacts.layout, &inputs, 0);
    let delta = root * zps_0.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"
    );

    // Mutate all quotient_next inputs; evaluation should remain zero.
    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");
}