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}