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