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}