Skip to main content

voting_circuits/delegation/
imt.rs

1//! IMT (Indexed Merkle Tree) utilities for the delegation proof system.
2//!
3//! Provides out-of-circuit helpers for building and verifying Poseidon-based
4//! Indexed Merkle Tree non-membership proofs using K=2 punctured-range leaves.
5//! Each leaf stores three sorted nullifier boundaries `[nf_lo, nf_mid, nf_hi]`
6//! and the leaf hash is `Poseidon3(nf_lo, nf_mid, nf_hi)`, followed by a
7//! standard Merkle path authenticating the leaf.
8//! A non-membership proof shows that a nullifier falls strictly inside
9//! `(nf_lo, nf_hi)` and is not equal to `nf_mid`.
10//! Used by the delegation circuit and builder.
11
12use pasta_curves::pallas;
13use std::string::String;
14
15use crate::protocol_hash::{poseidon_hash, poseidon_hash_2, poseidon_hash_3};
16
17/// Depth of the nullifier Indexed Merkle Tree Merkle path (Poseidon-based).
18/// Total Poseidon calls per proof = 2 (leaf hash, ConstantLength<3>) + 29 (path) = 31.
19pub const IMT_DEPTH: usize = 29;
20
21/// Protocol identifier for governance authorization, encoded as a little-endian
22/// Pallas field element. Used to derive the nullifier domain for this application.
23pub(crate) use crate::domain_tags::governance_authorization as gov_auth_domain_tag;
24
25/// Domain tag for governance alternate nullifiers.
26pub(crate) use crate::domain_tags::governance_nullifier as gov_null_domain_tag;
27
28/// Derive the nullifier domain for a voting round (out of circuit).
29///
30/// `dom = Poseidon("governance authorization", vote_round_id)`
31///
32/// The nullifier domain scopes alternate nullifiers to a specific application
33/// instance (ZIP §Nullifier Domains). This application hashes its protocol
34/// identifier with the vote round ID to produce a unique domain per round.
35pub fn derive_nullifier_domain(vote_round_id: pallas::Base) -> pallas::Base {
36    poseidon_hash_2(gov_auth_domain_tag(), vote_round_id)
37}
38
39/// Compute alternate nullifier out-of-circuit (ZIP §Alternate Nullifier Derivation).
40///
41/// `nf_dom = Poseidon("governance nullifier", nk, dom, nf^old)`
42///
43/// where `dom` is the nullifier domain (see [`derive_nullifier_domain`]).
44/// Single ConstantLength<4> call (2 permutations at rate=2).
45pub(crate) fn gov_null_hash(
46    nk: pallas::Base,
47    dom: pallas::Base,
48    real_nf: pallas::Base,
49) -> pallas::Base {
50    poseidon_hash([gov_null_domain_tag(), nk, dom, real_nf])
51}
52
53/// IMT non-membership proof data (K=2 punctured-range leaf model).
54///
55/// Each leaf stores three sorted nullifier boundaries `[nf_lo, nf_mid, nf_hi]`.
56/// The leaf hash is `Poseidon3(nf_lo, nf_mid, nf_hi)`, followed by a standard
57/// 29-level Merkle path to the root. Non-membership is proven by showing:
58///   1. `nf_lo < value < nf_hi` (strict interval)
59///   2. `value != nf_mid` (non-equality with interior nullifier)
60///
61/// # Tree contract
62///
63/// Proof soundness depends on the authenticated leaves forming the canonical
64/// K=2 punctured-range tree for the nullifier set. The nullifier list must be
65/// sorted, deduplicated, padded to an odd count, and include sentinels so that
66/// adjacent leaves share only boundary nullifiers and cover every value the
67/// circuit may rule out.
68///
69/// Every returned leaf must also have outer span `nf_hi - nf_lo <= 2^250` in
70/// canonical Pallas base-field ordering. This keeps each canonical bracket
71/// within the 250-bit offset checks used by the circuit.
72#[derive(Clone, Debug)]
73pub struct ImtProofData {
74    /// The Merkle root of the IMT.
75    pub root: pallas::Base,
76    /// Three sorted nullifier boundaries: `[nf_lo, nf_mid, nf_hi]`.
77    pub nf_bounds: [pallas::Base; 3],
78    /// Position of the leaf in the tree.
79    pub leaf_pos: u32,
80    /// Sibling hashes along the 29-level Merkle path (pure siblings).
81    pub path: [pallas::Base; IMT_DEPTH],
82}
83
84/// Error type for IMT proof fetching failures.
85#[derive(Clone, Debug)]
86pub struct ImtError(pub String);
87
88impl core::fmt::Display for ImtError {
89    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
90        write!(f, "IMT error: {}", self.0)
91    }
92}
93
94impl std::error::Error for ImtError {}
95
96/// Trait for providing IMT non-membership proofs.
97///
98/// # Invariants
99///
100/// Implementations must return proofs against a consistent root. Every proof
101/// returned by [`ImtProvider::non_membership_proof`] must authenticate to the
102/// same root returned by [`ImtProvider::root`].
103///
104/// Implementations must also satisfy the [`ImtProofData`] tree contract. The
105/// leaves committed under the root must be a non-overlapping partition of the
106/// nullifier domain covered by the circuit. A provider must not return a proof
107/// against one leaf for a value that appears as `nf_mid` in another leaf, since
108/// the circuit cannot detect overlap between authenticated leaves.
109///
110/// [`SpacedLeafImtProvider`] is the in-crate implementation for proof
111/// generation and tests.
112pub trait ImtProvider {
113    /// The current IMT root.
114    fn root(&self) -> pallas::Base;
115    /// Generate a non-membership proof for the given nullifier.
116    fn non_membership_proof(&self, nf: pallas::Base) -> Result<ImtProofData, ImtError>;
117}
118
119// ================================================================
120// SpacedLeafImtProvider (available for proof generation and tests)
121// ================================================================
122
123use ff::Field;
124use std::vec::Vec;
125
126/// Precomputed empty subtree hashes for the IMT (Poseidon-based).
127///
128/// `empty[0] = Poseidon3(0, 0, 0)` (hash of an all-zero punctured-range leaf),
129/// `empty[i] = Poseidon(empty[i-1], empty[i-1])` for i >= 1.
130fn empty_imt_hashes() -> Vec<pallas::Base> {
131    let empty_leaf = poseidon_hash_3(
132        pallas::Base::zero(),
133        pallas::Base::zero(),
134        pallas::Base::zero(),
135    );
136    let mut hashes = vec![empty_leaf];
137    for _ in 1..=IMT_DEPTH {
138        let prev = *hashes.last().unwrap();
139        hashes.push(poseidon_hash_2(prev, prev));
140    }
141    hashes
142}
143
144/// Sentinel spacing exponent: sentinels are placed at `k * 2^249`.
145/// With K=2 punctured ranges each leaf spans two consecutive intervals,
146/// giving outer span `2 * 2^249 = 2^250` — matching the circuit's 250-bit
147/// range check.
148pub const SENTINEL_EXPONENT: u64 = 249;
149
150/// Number of sentinel multiples: `0, 1*step, 2*step, ..., 32*step`.
151/// `32 * 2^249 = 2^254` reaches the main high bit of the Pallas base field,
152/// and the final `p - 1` sentinel closes the remaining tail.
153pub const SENTINEL_COUNT: u64 = 32;
154
155/// Build the sorted, deduplicated, odd-count sentinel list used by both
156/// [`SpacedLeafImtProvider`] and the production `prepare_nullifiers` path.
157///
158/// Sentinels: `k * 2^249` for `k = 0..=32`, plus `p - 1` to close the tail.
159/// If the count is even after dedup, `Fp::from(2)` is inserted after sentinel 0
160/// to make it odd (collision probability ≈ 2^{-254}).
161pub fn build_sentinel_list() -> Vec<pallas::Base> {
162    let step = pallas::Base::from(2u64).pow([SENTINEL_EXPONENT, 0, 0, 0]);
163    let mut nfs: Vec<pallas::Base> = (0u64..=SENTINEL_COUNT)
164        .map(|k| step * pallas::Base::from(k))
165        .collect();
166    nfs.push(-pallas::Base::one()); // p - 1
167    nfs.sort();
168    nfs.dedup();
169    if nfs.len() % 2 == 0 {
170        debug_assert_eq!(nfs[0], pallas::Base::zero(), "sentinel 0 must be first");
171        nfs.insert(1, pallas::Base::from(2u64));
172    }
173    nfs
174}
175
176/// Build the sorted, deduplicated, odd-count nullifier list after merging
177/// real nullifiers into the sentinel skeleton.
178///
179/// This is the shared input-preparation step for the in-tree fixture provider
180/// and the `imt-tree` reference adapter used by integration tests.
181pub fn build_nullifier_list(extra_nfs: &[pallas::Base]) -> Vec<pallas::Base> {
182    let mut nfs = build_sentinel_list();
183    nfs.extend_from_slice(extra_nfs);
184    nfs.sort();
185    nfs.dedup();
186    if nfs.len() % 2 == 0 {
187        let padding = std::iter::once(2u64)
188            .chain(1u64..)
189            .map(pallas::Base::from)
190            .find(|candidate| nfs.binary_search(candidate).is_err())
191            .expect("small field-element padding candidate should exist");
192        let insert_at = nfs.binary_search(&padding).unwrap_err();
193        nfs.insert(insert_at, padding);
194    }
195    nfs
196}
197
198/// Build punctured-range triples from a sorted, deduplicated, odd-count
199/// nullifier list. Mirrors `imt_tree::tree::build_punctured_ranges` so the
200/// test fixture is protected by the same ordering invariant as production.
201/// See `imt_circuit_integration::spaced_leaf_and_production_sentinel_providers_agree`
202/// for the runtime cross-check against the `imt-tree` reference path.
203fn build_punctured_ranges_local(sorted_nfs: &[pallas::Base]) -> Vec<[pallas::Base; 3]> {
204    let n = sorted_nfs.len();
205    assert!(n >= 3, "need at least 3 sorted nullifiers, got {n}");
206    assert!(n % 2 == 1, "sorted nullifier count must be odd (got {n})");
207
208    let num_leaves = (n - 1) / 2;
209    (0..num_leaves)
210        .map(|i| {
211            let base = i * 2;
212            let (lo, mid, hi) = (sorted_nfs[base], sorted_nfs[base + 1], sorted_nfs[base + 2]);
213            assert!(
214                lo < mid && mid < hi,
215                "punctured range {i} violates strict ordering: \
216                 nf_lo={lo:?}, nf_mid={mid:?}, nf_hi={hi:?}"
217            );
218            [lo, mid, hi]
219        })
220        .collect()
221}
222
223/// Find the punctured range whose open interval can witness `value`.
224///
225/// This is the provider side of the same contract enforced by
226/// `PuncturedIntervalGate`. It returns `None` for values below the first range,
227/// values equal to a leaf boundary (`nf_lo` or `nf_hi`), values past `nf_hi`,
228/// and values equal to `nf_mid`. The boundary cases correspond to the gate's
229/// strict `x_lo = real_nf - nf_lo - 1` and `x_hi = nf_hi - real_nf - 1` range
230/// checks. The `nf_mid` case corresponds to the inverse witness non-equality gate.
231///
232/// Mirrors `imt_tree::tree::find_punctured_range_for_value`; the integration
233/// tests cross-check both implementations on the same roots and proof
234/// witnesses.
235fn find_range_for_value(ranges: &[[pallas::Base; 3]], value: pallas::Base) -> Option<usize> {
236    let i = ranges.partition_point(|[nf_lo, _, _]| *nf_lo < value);
237    if i == 0 {
238        return None;
239    }
240    let idx = i - 1;
241    let [nf_lo, nf_mid, nf_hi] = ranges[idx];
242    let offset = value - nf_lo;
243    let span = nf_hi - nf_lo;
244    if offset == pallas::Base::zero() || offset >= span {
245        return None;
246    }
247    if value == nf_mid {
248        return None;
249    }
250    Some(idx)
251}
252
253/// IMT provider with evenly-spaced K=2 punctured-range brackets.
254///
255/// Mirrors the production sentinel injection path: sentinels at `k * 2^249`
256/// for `k = 0..=32`, plus `p - 1`, sorted, deduplicated, and padded to odd
257/// count with `Fp::from(2)`. Each interior leaf spans exactly `2^250`,
258/// satisfying the circuit's 250-bit range check. The final leaf is
259/// `[31*step, 32*step, p-1]`, also within the bound.
260///
261/// Used for proof generation (fixture generators) and testing.
262#[derive(Debug)]
263pub struct SpacedLeafImtProvider {
264    /// The root of the IMT.
265    root: pallas::Base,
266    /// Punctured-range triples: `[nf_lo, nf_mid, nf_hi]` for each leaf.
267    leaves: Vec<[pallas::Base; 3]>,
268    /// Bottom levels of the subtree (32-leaf subtree → 5 levels).
269    /// `subtree_levels[0]` has 32 leaf hashes Poseidon3(nf_lo, nf_mid, nf_hi),
270    /// `subtree_levels[5]` has 1 subtree root.
271    subtree_levels: Vec<Vec<pallas::Base>>,
272}
273
274impl SpacedLeafImtProvider {
275    /// Create a new spaced-leaf IMT provider (K=2 punctured-range model).
276    ///
277    /// Builds the same sentinel layout as the production `prepare_nullifiers`
278    /// path: sorted, deduplicated, padded to odd count, then grouped into
279    /// punctured-range triples with strict ordering validation.
280    pub fn new() -> Self {
281        Self::with_extra_nullifiers(&[])
282    }
283
284    /// Create a spaced-leaf IMT provider after merging extra real nullifiers
285    /// into the sentinel skeleton.
286    ///
287    /// This mirrors the production `prepare_nullifiers` shape used by the
288    /// `imt-tree` reference adapter in integration tests.
289    pub fn with_extra_nullifiers(extra_nfs: &[pallas::Base]) -> Self {
290        let sorted_nfs = build_nullifier_list(extra_nfs);
291        let leaves = build_punctured_ranges_local(&sorted_nfs);
292        assert!(
293            leaves.len() <= 32,
294            "spaced-leaf fixture supports at most 32 leaves, got {}",
295            leaves.len()
296        );
297        let empty = empty_imt_hashes();
298
299        let empty_leaf_hash = poseidon_hash_3(
300            pallas::Base::zero(),
301            pallas::Base::zero(),
302            pallas::Base::zero(),
303        );
304        let mut level0 = vec![empty_leaf_hash; 32];
305        for (k, bounds) in leaves.iter().enumerate() {
306            level0[k] = poseidon_hash_3(bounds[0], bounds[1], bounds[2]);
307        }
308
309        let mut subtree_levels = vec![level0];
310        for _l in 1..=5 {
311            let prev = subtree_levels.last().unwrap();
312            let mut current = Vec::with_capacity(prev.len() / 2);
313            for j in 0..(prev.len() / 2) {
314                current.push(poseidon_hash_2(prev[2 * j], prev[2 * j + 1]));
315            }
316            subtree_levels.push(current);
317        }
318
319        let mut root = subtree_levels[5][0];
320        for l in 5..IMT_DEPTH {
321            root = poseidon_hash_2(root, empty[l]);
322        }
323
324        SpacedLeafImtProvider {
325            root,
326            leaves,
327            subtree_levels,
328        }
329    }
330}
331
332impl ImtProvider for SpacedLeafImtProvider {
333    fn root(&self) -> pallas::Base {
334        self.root
335    }
336
337    fn non_membership_proof(&self, nf: pallas::Base) -> Result<ImtProofData, ImtError> {
338        let k = find_range_for_value(&self.leaves, nf)
339            .ok_or_else(|| ImtError(format!("nullifier {nf:?} not in any punctured range")))?;
340
341        let nf_bounds = self.leaves[k];
342        let leaf_pos = k as u32;
343
344        let empty = empty_imt_hashes();
345        let mut path = [pallas::Base::zero(); IMT_DEPTH];
346
347        let mut idx = k;
348        for l in 0..5 {
349            let sibling_idx = idx ^ 1;
350            path[l] = self.subtree_levels[l][sibling_idx];
351            idx >>= 1;
352        }
353
354        for l in 5..IMT_DEPTH {
355            path[l] = empty[l];
356        }
357
358        Ok(ImtProofData {
359            root: self.root,
360            nf_bounds,
361            leaf_pos,
362            path,
363        })
364    }
365}
366
367#[cfg(test)]
368mod tests {
369    use super::*;
370    use ff::PrimeField;
371
372    fn base_from_repr(bytes: [u8; 32]) -> pallas::Base {
373        pallas::Base::from_repr(bytes).expect("frozen vector must be canonical")
374    }
375
376    #[test]
377    fn gov_null_hash_is_domain_separated_from_imt_leaf_hash() {
378        let a = pallas::Base::from(0u64);
379        let b = pallas::Base::from(1u64);
380        let c = pallas::Base::from(2u64);
381
382        assert_ne!(
383            gov_null_hash(a, b, c),
384            poseidon_hash_3(a, b, c),
385            "governance nullifiers must not share the raw Poseidon3 preimage with IMT leaves"
386        );
387    }
388
389    #[test]
390    fn derive_nullifier_domain_frozen_vector() {
391        assert_eq!(
392            derive_nullifier_domain(pallas::Base::from(42u64)),
393            base_from_repr([
394                202, 12, 215, 224, 168, 199, 68, 160, 148, 160, 237, 250, 131, 157, 181, 207, 158,
395                105, 141, 50, 135, 245, 182, 83, 151, 198, 14, 254, 122, 79, 78, 23,
396            ])
397        );
398    }
399
400    #[test]
401    fn gov_null_hash_frozen_vector() {
402        assert_eq!(
403            gov_null_hash(
404                pallas::Base::from(1u64),
405                pallas::Base::from(2u64),
406                pallas::Base::from(3u64),
407            ),
408            base_from_repr([
409                33, 58, 71, 28, 174, 217, 192, 215, 38, 189, 209, 38, 27, 71, 135, 247, 157, 111,
410                146, 254, 20, 25, 211, 204, 191, 4, 120, 54, 134, 218, 195, 29,
411            ])
412        );
413    }
414
415    #[test]
416    fn find_range_for_value_rejects_punctured_interval_boundaries() {
417        let ranges = [
418            [
419                pallas::Base::from(10u64),
420                pallas::Base::from(15u64),
421                pallas::Base::from(20u64),
422            ],
423            [
424                pallas::Base::from(20u64),
425                pallas::Base::from(25u64),
426                pallas::Base::from(30u64),
427            ],
428        ];
429
430        for rejected in [9u64, 10, 15, 20, 25, 30, 31] {
431            assert_eq!(
432                find_range_for_value(&ranges, pallas::Base::from(rejected)),
433                None,
434                "boundary value {rejected} must not produce an IMT proof"
435            );
436        }
437
438        assert_eq!(
439            find_range_for_value(&ranges, pallas::Base::from(11u64)),
440            Some(0)
441        );
442        assert_eq!(
443            find_range_for_value(&ranges, pallas::Base::from(19u64)),
444            Some(0)
445        );
446        assert_eq!(
447            find_range_for_value(&ranges, pallas::Base::from(21u64)),
448            Some(1)
449        );
450        assert_eq!(
451            find_range_for_value(&ranges, pallas::Base::from(29u64)),
452            Some(1)
453        );
454    }
455}