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(crate) 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.
145pub const 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.
150pub const 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 SpacedLeafImtProvider {
272    /// Create a new spaced-leaf IMT provider (K=2 punctured-range model).
273    ///
274    /// Builds the same sentinel layout as the production `prepare_nullifiers`
275    /// path: sorted, deduplicated, padded to odd count, then grouped into
276    /// punctured-range triples with strict ordering validation.
277    pub fn new() -> Self {
278        Self::with_extra_nullifiers(&[])
279    }
280
281    /// Create a spaced-leaf IMT provider after merging extra real nullifiers
282    /// into the sentinel skeleton.
283    ///
284    /// This mirrors the production `prepare_nullifiers` shape used by the
285    /// `imt-tree` reference adapter in integration tests.
286    pub fn with_extra_nullifiers(extra_nfs: &[pallas::Base]) -> Self {
287        let sorted_nfs = build_nullifier_list(extra_nfs);
288        let leaves = build_punctured_ranges_local(&sorted_nfs);
289        assert!(
290            leaves.len() <= 32,
291            "spaced-leaf fixture supports at most 32 leaves, got {}",
292            leaves.len()
293        );
294        let empty = empty_imt_hashes();
295
296        let empty_leaf_hash = poseidon_hash_3(
297            pallas::Base::zero(),
298            pallas::Base::zero(),
299            pallas::Base::zero(),
300        );
301        let mut level0 = vec![empty_leaf_hash; 32];
302        for (k, bounds) in leaves.iter().enumerate() {
303            level0[k] = poseidon_hash_3(bounds[0], bounds[1], bounds[2]);
304        }
305
306        let mut subtree_levels = vec![level0];
307        for _l in 1..=5 {
308            let prev = subtree_levels.last().unwrap();
309            let mut current = Vec::with_capacity(prev.len() / 2);
310            for j in 0..(prev.len() / 2) {
311                current.push(poseidon_hash_2(prev[2 * j], prev[2 * j + 1]));
312            }
313            subtree_levels.push(current);
314        }
315
316        let mut root = subtree_levels[5][0];
317        for l in 5..IMT_DEPTH {
318            root = poseidon_hash_2(root, empty[l]);
319        }
320
321        SpacedLeafImtProvider {
322            root,
323            leaves,
324            subtree_levels,
325        }
326    }
327}
328
329impl ImtProvider for SpacedLeafImtProvider {
330    fn root(&self) -> pallas::Base {
331        self.root
332    }
333
334    fn non_membership_proof(&self, nf: pallas::Base) -> Result<ImtProofData, ImtError> {
335        let k = find_range_for_value(&self.leaves, nf)
336            .ok_or_else(|| ImtError(format!("nullifier {nf:?} not in any punctured range")))?;
337
338        let nf_bounds = self.leaves[k];
339        let leaf_pos = k as u32;
340
341        let empty = empty_imt_hashes();
342        let mut path = [pallas::Base::zero(); IMT_DEPTH];
343
344        let mut idx = k;
345        for l in 0..5 {
346            let sibling_idx = idx ^ 1;
347            path[l] = self.subtree_levels[l][sibling_idx];
348            idx >>= 1;
349        }
350
351        for l in 5..IMT_DEPTH {
352            path[l] = empty[l];
353        }
354
355        Ok(ImtProofData {
356            root: self.root,
357            nf_bounds,
358            leaf_pos,
359            path,
360        })
361    }
362}
363
364#[cfg(test)]
365mod tests {
366    use super::*;
367    use ff::PrimeField;
368
369    fn base_from_repr(bytes: [u8; 32]) -> pallas::Base {
370        pallas::Base::from_repr(bytes).expect("frozen vector must be canonical")
371    }
372
373    #[test]
374    fn derive_nullifier_domain_frozen_vector() {
375        assert_eq!(
376            derive_nullifier_domain(pallas::Base::from(42u64)),
377            base_from_repr([
378                202, 12, 215, 224, 168, 199, 68, 160, 148, 160, 237, 250, 131, 157, 181, 207, 158,
379                105, 141, 50, 135, 245, 182, 83, 151, 198, 14, 254, 122, 79, 78, 23,
380            ])
381        );
382    }
383
384    #[test]
385    fn gov_null_hash_frozen_vector() {
386        assert_eq!(
387            gov_null_hash(
388                pallas::Base::from(1u64),
389                pallas::Base::from(2u64),
390                pallas::Base::from(3u64),
391            ),
392            base_from_repr([
393                234, 252, 225, 20, 190, 170, 130, 80, 54, 152, 212, 172, 198, 24, 120, 139, 100,
394                140, 198, 64, 152, 34, 38, 95, 158, 62, 234, 30, 198, 66, 171, 24,
395            ])
396        );
397    }
398
399    #[test]
400    fn find_range_for_value_rejects_punctured_interval_boundaries() {
401        let ranges = [
402            [
403                pallas::Base::from(10u64),
404                pallas::Base::from(15u64),
405                pallas::Base::from(20u64),
406            ],
407            [
408                pallas::Base::from(20u64),
409                pallas::Base::from(25u64),
410                pallas::Base::from(30u64),
411            ],
412        ];
413
414        for rejected in [9u64, 10, 15, 20, 25, 30, 31] {
415            assert_eq!(
416                find_range_for_value(&ranges, pallas::Base::from(rejected)),
417                None,
418                "boundary value {rejected} must not produce an IMT proof"
419            );
420        }
421
422        assert_eq!(
423            find_range_for_value(&ranges, pallas::Base::from(11u64)),
424            Some(0)
425        );
426        assert_eq!(
427            find_range_for_value(&ranges, pallas::Base::from(19u64)),
428            Some(0)
429        );
430        assert_eq!(
431            find_range_for_value(&ranges, pallas::Base::from(21u64)),
432            Some(1)
433        );
434        assert_eq!(
435            find_range_for_value(&ranges, pallas::Base::from(29u64)),
436            Some(1)
437        );
438    }
439}