Skip to main content

miden_air/
proof_order.rs

1use alloc::{string::String, vec::Vec};
2
3use crate::MidenAir;
4
5/// Supported AIRs in instance order.
6///
7/// This order is used for per-AIR inputs and breaks proof-order ties when trace heights are equal.
8pub const AIRS: [MidenAir; 3] =
9    [MidenAir::Core, MidenAir::Chiplets, MidenAir::Poseidon2Permutation];
10
11pub const MIDEN_AIR_COUNT: usize = AIRS.len();
12
13/// Number of possible proof-order permutations.
14pub const PROOF_ORDER_COUNT: usize = factorial(MIDEN_AIR_COUNT);
15const _: () = assert!(PROOF_ORDER_COUNT <= u32::MAX as usize, "proof-order tags must fit in u32");
16
17/// Smallest Merkle tree depth covering every proof-order tag.
18pub const PROOF_ORDER_REGISTRY_DEPTH: usize = ceil_log2(PROOF_ORDER_COUNT);
19
20/// Proof-order AIR permutation.
21///
22/// The proof stores AIR commitments in ascending `(log_trace_height, instance_index)` order. That
23/// order can vary by statement, so the recursive verifier selects one ACE circuit from a small
24/// registry. The registry key is `tag`, the Lehmer rank of the AIR permutation relative to
25/// [`AIRS`].
26#[derive(Clone, Debug, Eq, PartialEq)]
27pub struct ProofOrder {
28    airs: [MidenAir; MIDEN_AIR_COUNT],
29    tag: u32,
30}
31
32impl ProofOrder {
33    /// Construct a proof order from an explicit AIR permutation.
34    ///
35    /// Panics if an AIR is missing or duplicated.
36    pub fn new(airs: [MidenAir; MIDEN_AIR_COUNT]) -> Self {
37        assert_is_air_permutation(airs);
38        let tag = lehmer_rank(airs);
39        Self { airs, tag }
40    }
41
42    /// Construct a proof order from a slice containing every supported AIR exactly once.
43    pub fn from_airs(airs: &[MidenAir]) -> Self {
44        let Ok(airs) = airs.try_into() else {
45            panic!("proof order must include every AIR exactly once");
46        };
47        Self::new(airs)
48    }
49
50    /// Return the canonical instance order from [`AIRS`].
51    pub fn instance_order() -> Self {
52        Self::new(AIRS)
53    }
54
55    /// Return every supported proof order, sorted by tag.
56    pub fn variants() -> Vec<Self> {
57        (0..PROOF_ORDER_COUNT).map(Self::from_rank).collect()
58    }
59
60    /// Decode a registry tag into a proof order.
61    pub fn from_tag(tag: u32) -> Option<Self> {
62        let rank = tag as usize;
63        (rank < PROOF_ORDER_COUNT).then(|| Self::from_rank(rank))
64    }
65
66    /// Sort AIRs by trace height, using instance order as the tie-breaker.
67    ///
68    /// `log_heights` must be in [`AIRS`] order.
69    pub fn from_instance_log_heights(log_heights: &[u8]) -> Self {
70        assert_eq!(log_heights.len(), AIRS.len(), "one log height is required per AIR");
71
72        let mut ordered: Vec<(MidenAir, u8)> =
73            AIRS.iter().copied().zip(log_heights.iter().copied()).collect();
74        ordered.sort_by_key(|(air, height)| (*height, air.instance_index()));
75
76        let mut airs = [AIRS[0]; MIDEN_AIR_COUNT];
77        for (dst, (air, _)) in airs.iter_mut().zip(ordered) {
78            *dst = air;
79        }
80        Self::new(airs)
81    }
82
83    /// AIRs in the order used by the proof.
84    pub fn airs(&self) -> &[MidenAir] {
85        &self.airs
86    }
87
88    /// Registry tag for this proof order.
89    pub fn tag(&self) -> u32 {
90        self.tag
91    }
92
93    /// File stem for the generated ACE circuit for this order.
94    pub fn file_stem(&self) -> String {
95        let mut stem = String::from("constraints_eval_");
96        for (i, air) in self.airs.iter().copied().enumerate() {
97            if i > 0 {
98                stem.push_str("_then_");
99            }
100            stem.push_str(air.file_token());
101        }
102        stem
103    }
104
105    /// Decode a Lehmer rank into its AIR permutation.
106    fn from_rank(rank: usize) -> Self {
107        debug_assert!(rank < PROOF_ORDER_COUNT);
108        debug_assert!(rank <= u32::MAX as usize);
109
110        let tag = rank as u32;
111        let mut rank = rank;
112        let mut remaining = AIRS.to_vec();
113        let mut airs = [AIRS[0]; MIDEN_AIR_COUNT];
114
115        for (i, slot) in airs.iter_mut().enumerate() {
116            let factor = factorial(MIDEN_AIR_COUNT - 1 - i);
117            // The next Lehmer digit selects an AIR from the remaining ordered list.
118            let index = rank / factor;
119            rank %= factor;
120            *slot = remaining.remove(index);
121        }
122
123        Self { airs, tag }
124    }
125}
126
127/// Compute `n!`.
128const fn factorial(n: usize) -> usize {
129    let mut result = 1;
130    let mut factor = 2;
131    while factor <= n {
132        result *= factor;
133        factor += 1;
134    }
135    result
136}
137
138/// Return the smallest `d` such that `2^d >= value`.
139const fn ceil_log2(value: usize) -> usize {
140    assert!(value > 0, "ceil_log2 is undefined for zero");
141
142    let mut value = value - 1;
143    let mut result = 0;
144    while value > 0 {
145        value >>= 1;
146        result += 1;
147    }
148    result
149}
150
151/// Assert that `airs` contains every supported AIR exactly once.
152fn assert_is_air_permutation(airs: [MidenAir; MIDEN_AIR_COUNT]) {
153    let mut seen = [false; MIDEN_AIR_COUNT];
154    for air in &airs {
155        let index = air.instance_index();
156        assert!(!seen[index], "proof order contains duplicate AIR: {air:?}");
157        seen[index] = true;
158    }
159}
160
161/// Return the Lehmer rank of an AIR permutation relative to [`AIRS`].
162fn lehmer_rank(airs: [MidenAir; MIDEN_AIR_COUNT]) -> u32 {
163    let mut rank = 0;
164    for i in 0..airs.len() {
165        // Lehmer digit: number of smaller instance indices to the right of position `i`.
166        let smaller_after = airs[i + 1..]
167            .iter()
168            .filter(|air| air.instance_index() < airs[i].instance_index())
169            .count();
170        rank += smaller_after as u32 * factorial(airs.len() - 1 - i) as u32;
171    }
172    rank
173}
174
175#[cfg(test)]
176mod tests {
177    use super::*;
178
179    #[test]
180    fn air_registry_order_matches_instance_indices() {
181        for (index, air) in AIRS.iter().copied().enumerate() {
182            assert_eq!(air.instance_index(), index);
183        }
184    }
185
186    #[test]
187    fn proof_order_constants_derive_from_air_count() {
188        assert_eq!(PROOF_ORDER_COUNT, ProofOrder::variants().len());
189        assert_eq!(PROOF_ORDER_REGISTRY_DEPTH, ceil_log2(PROOF_ORDER_COUNT));
190    }
191
192    #[test]
193    fn proof_order_count_is_factorial() {
194        assert_eq!(factorial(0), 1);
195        assert_eq!(factorial(1), 1);
196        assert_eq!(factorial(2), 2);
197        assert_eq!(factorial(3), 6);
198        assert_eq!(factorial(4), 24);
199    }
200
201    #[test]
202    fn registry_depth_is_ceil_log2() {
203        assert_eq!(ceil_log2(1), 0);
204        assert_eq!(ceil_log2(2), 1);
205        assert_eq!(ceil_log2(3), 2);
206        assert_eq!(ceil_log2(6), 3);
207        assert_eq!(ceil_log2(24), 5);
208    }
209
210    #[test]
211    fn proof_order_tags_use_lehmer_rank() {
212        let variants = ProofOrder::variants();
213
214        assert_eq!(variants.len(), PROOF_ORDER_COUNT);
215        assert_eq!(variants[0], ProofOrder::instance_order());
216        for (tag, order) in variants.into_iter().enumerate() {
217            assert_eq!(order.tag(), tag as u32);
218            assert_eq!(ProofOrder::from_tag(tag as u32), Some(order));
219        }
220        assert_eq!(ProofOrder::from_tag(PROOF_ORDER_COUNT as u32), None);
221    }
222
223    #[test]
224    fn proof_order_sorts_by_height_then_instance_index() {
225        assert_eq!(
226            ProofOrder::from_instance_log_heights(&[8, 9, 10]),
227            ProofOrder::from_airs(&[
228                MidenAir::Core,
229                MidenAir::Chiplets,
230                MidenAir::Poseidon2Permutation,
231            ])
232        );
233        assert_eq!(
234            ProofOrder::from_instance_log_heights(&[9, 8, 10]),
235            ProofOrder::from_airs(&[
236                MidenAir::Chiplets,
237                MidenAir::Core,
238                MidenAir::Poseidon2Permutation,
239            ])
240        );
241        assert_eq!(
242            ProofOrder::from_instance_log_heights(&[8, 8, 8]),
243            ProofOrder::from_airs(&[
244                MidenAir::Core,
245                MidenAir::Chiplets,
246                MidenAir::Poseidon2Permutation,
247            ])
248        );
249    }
250}