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 alloc::string::String;
13use ff::PrimeField;
14use halo2_gadgets::poseidon::primitives::{self as poseidon, ConstantLength};
15use pasta_curves::pallas;
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) fn gov_auth_domain_tag() -> pallas::Base {
24 let mut bytes = [0u8; 32];
25 bytes[..24].copy_from_slice(b"governance authorization");
26 pallas::Base::from_repr(bytes).unwrap()
27}
28
29/// Compute Poseidon hash of two field elements (out of circuit).
30pub(crate) fn poseidon_hash_2(a: pallas::Base, b: pallas::Base) -> pallas::Base {
31 poseidon::Hash::<_, poseidon::P128Pow5T3, ConstantLength<2>, 3, 2>::init().hash([a, b])
32}
33
34/// Compute Poseidon hash of three field elements (out of circuit).
35/// Uses `ConstantLength<3>` (width-3 sponge, 2 absorption blocks).
36pub(crate) fn poseidon_hash_3(a: pallas::Base, b: pallas::Base, c: pallas::Base) -> pallas::Base {
37 poseidon::Hash::<_, poseidon::P128Pow5T3, ConstantLength<3>, 3, 2>::init().hash([a, b, c])
38}
39
40/// Derive the nullifier domain for a voting round (out of circuit).
41///
42/// `dom = Poseidon("governance authorization", vote_round_id)`
43///
44/// The nullifier domain scopes alternate nullifiers to a specific application
45/// instance (ZIP §Nullifier Domains). This application hashes its protocol
46/// identifier with the vote round ID to produce a unique domain per round.
47pub fn derive_nullifier_domain(vote_round_id: pallas::Base) -> pallas::Base {
48 poseidon_hash_2(gov_auth_domain_tag(), vote_round_id)
49}
50
51/// Compute alternate nullifier out-of-circuit (ZIP §Alternate Nullifier Derivation).
52///
53/// `nf_dom = Poseidon(nk, dom, nf^old)`
54///
55/// where `dom` is the nullifier domain (see [`derive_nullifier_domain`]).
56/// Single ConstantLength<3> call (2 permutations at rate=2).
57pub(crate) fn gov_null_hash(
58 nk: pallas::Base,
59 dom: pallas::Base,
60 real_nf: pallas::Base,
61) -> pallas::Base {
62 poseidon_hash_3(nk, dom, real_nf)
63}
64
65/// IMT non-membership proof data (K=2 punctured-range leaf model).
66///
67/// Each leaf stores three sorted nullifier boundaries `[nf_lo, nf_mid, nf_hi]`.
68/// The leaf hash is `Poseidon3(nf_lo, nf_mid, nf_hi)`, followed by a standard
69/// 29-level Merkle path to the root. Non-membership is proven by showing:
70/// 1. `nf_lo < value < nf_hi` (strict interval)
71/// 2. `value != nf_mid` (non-equality with interior nullifier)
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
94#[cfg(feature = "std")]
95impl std::error::Error for ImtError {}
96
97/// Trait for providing IMT non-membership proofs.
98///
99/// Implementations must return proofs against a consistent root — all proofs
100/// from the same provider must share the same `root()` value.
101pub trait ImtProvider {
102 /// The current IMT root.
103 fn root(&self) -> pallas::Base;
104 /// Generate a non-membership proof for the given nullifier.
105 fn non_membership_proof(&self, nf: pallas::Base) -> Result<ImtProofData, ImtError>;
106}
107
108// ================================================================
109// SpacedLeafImtProvider (available for proof generation and tests)
110// ================================================================
111
112use alloc::vec::Vec;
113use ff::Field;
114
115/// Precomputed empty subtree hashes for the IMT (Poseidon-based).
116///
117/// `empty[0] = Poseidon3(0, 0, 0)` (hash of an all-zero punctured-range leaf),
118/// `empty[i] = Poseidon(empty[i-1], empty[i-1])` for i >= 1.
119pub fn empty_imt_hashes() -> Vec<pallas::Base> {
120 let empty_leaf = poseidon_hash_3(pallas::Base::zero(), pallas::Base::zero(), pallas::Base::zero());
121 let mut hashes = vec![empty_leaf];
122 for _ in 1..=IMT_DEPTH {
123 let prev = *hashes.last().unwrap();
124 hashes.push(poseidon_hash_2(prev, prev));
125 }
126 hashes
127}
128
129/// Sentinel spacing exponent: sentinels are placed at `k * 2^249`.
130/// With K=2 punctured ranges each leaf spans two consecutive intervals,
131/// giving outer span `2 * 2^249 = 2^250` — matching the circuit's 250-bit
132/// range check.
133const SENTINEL_EXPONENT: u64 = 249;
134
135/// Number of sentinel multiples: `0, 1*step, 2*step, ..., 32*step`.
136/// `32 * 2^249 = 2^254` covers the Pallas field (p ≈ 2^254.9).
137const SENTINEL_COUNT: u64 = 32;
138
139/// Build the sorted, deduplicated, odd-count sentinel list used by both
140/// [`SpacedLeafImtProvider`] and the production `prepare_nullifiers` path.
141///
142/// Sentinels: `k * 2^249` for `k = 0..=32`, plus `p - 1` to close the tail.
143/// If the count is even after dedup, `Fp::from(2)` is inserted after sentinel 0
144/// to make it odd (collision probability ≈ 2^{-254}).
145fn build_sentinel_list() -> Vec<pallas::Base> {
146 let step = pallas::Base::from(2u64).pow([SENTINEL_EXPONENT, 0, 0, 0]);
147 let mut nfs: Vec<pallas::Base> = (0u64..=SENTINEL_COUNT)
148 .map(|k| step * pallas::Base::from(k))
149 .collect();
150 nfs.push(-pallas::Base::one()); // p - 1
151 nfs.sort();
152 nfs.dedup();
153 if nfs.len() % 2 == 0 {
154 debug_assert_eq!(nfs[0], pallas::Base::zero(), "sentinel 0 must be first");
155 nfs.insert(1, pallas::Base::from(2u64));
156 }
157 nfs
158}
159
160/// Build punctured-range triples from a sorted, deduplicated, odd-count
161/// nullifier list. Mirrors `imt_tree::tree::build_punctured_ranges` so the
162/// test fixture is protected by the same ordering invariant as production.
163fn build_punctured_ranges_local(sorted_nfs: &[pallas::Base]) -> Vec<[pallas::Base; 3]> {
164 let n = sorted_nfs.len();
165 assert!(n >= 3, "need at least 3 sorted nullifiers, got {n}");
166 assert!(n % 2 == 1, "sorted nullifier count must be odd (got {n})");
167
168 let num_leaves = (n - 1) / 2;
169 (0..num_leaves)
170 .map(|i| {
171 let base = i * 2;
172 let (lo, mid, hi) = (sorted_nfs[base], sorted_nfs[base + 1], sorted_nfs[base + 2]);
173 assert!(
174 lo < mid && mid < hi,
175 "punctured range {i} violates strict ordering: \
176 nf_lo={lo:?}, nf_mid={mid:?}, nf_hi={hi:?}"
177 );
178 [lo, mid, hi]
179 })
180 .collect()
181}
182
183/// Find the punctured-range index containing `value`. Mirrors
184/// `imt_tree::tree::find_punctured_range_for_value`.
185fn find_range_for_value(ranges: &[[pallas::Base; 3]], value: pallas::Base) -> Option<usize> {
186 let i = ranges.partition_point(|[nf_lo, _, _]| *nf_lo < value);
187 if i == 0 {
188 return None;
189 }
190 let idx = i - 1;
191 let [nf_lo, nf_mid, nf_hi] = ranges[idx];
192 let offset = value - nf_lo;
193 let span = nf_hi - nf_lo;
194 if offset == pallas::Base::zero() || offset >= span {
195 return None;
196 }
197 if value == nf_mid {
198 return None;
199 }
200 Some(idx)
201}
202
203/// IMT provider with evenly-spaced K=2 punctured-range brackets.
204///
205/// Mirrors the production sentinel injection path: sentinels at `k * 2^249`
206/// for `k = 0..=32`, plus `p - 1`, sorted, deduplicated, and padded to odd
207/// count with `Fp::from(2)`. Each interior leaf spans exactly `2^250`,
208/// satisfying the circuit's 250-bit range check. The tail leaf covers
209/// `[32*step, p-1]` with span `≈ 2^126`, well under the bound.
210///
211/// Used for proof generation (fixture generators) and testing.
212#[derive(Debug)]
213pub struct SpacedLeafImtProvider {
214 /// The root of the IMT.
215 root: pallas::Base,
216 /// Punctured-range triples: `[nf_lo, nf_mid, nf_hi]` for each leaf.
217 leaves: Vec<[pallas::Base; 3]>,
218 /// Bottom levels of the subtree (32-leaf subtree → 5 levels).
219 /// `subtree_levels[0]` has 32 leaf hashes Poseidon3(nf_lo, nf_mid, nf_hi),
220 /// `subtree_levels[5]` has 1 subtree root.
221 subtree_levels: Vec<Vec<pallas::Base>>,
222}
223
224impl SpacedLeafImtProvider {
225 /// Create a new spaced-leaf IMT provider (K=2 punctured-range model).
226 ///
227 /// Builds the same sentinel layout as the production `prepare_nullifiers`
228 /// path: sorted, deduplicated, padded to odd count, then grouped into
229 /// punctured-range triples with strict ordering validation.
230 pub fn new() -> Self {
231 let sorted_nfs = build_sentinel_list();
232 let leaves = build_punctured_ranges_local(&sorted_nfs);
233 let empty = empty_imt_hashes();
234
235 let empty_leaf_hash = poseidon_hash_3(
236 pallas::Base::zero(),
237 pallas::Base::zero(),
238 pallas::Base::zero(),
239 );
240 let mut level0 = vec![empty_leaf_hash; 32];
241 for (k, bounds) in leaves.iter().enumerate() {
242 level0[k] = poseidon_hash_3(bounds[0], bounds[1], bounds[2]);
243 }
244
245 let mut subtree_levels = vec![level0];
246 for _l in 1..=5 {
247 let prev = subtree_levels.last().unwrap();
248 let mut current = Vec::with_capacity(prev.len() / 2);
249 for j in 0..(prev.len() / 2) {
250 current.push(poseidon_hash_2(prev[2 * j], prev[2 * j + 1]));
251 }
252 subtree_levels.push(current);
253 }
254
255 let mut root = subtree_levels[5][0];
256 for l in 5..IMT_DEPTH {
257 root = poseidon_hash_2(root, empty[l]);
258 }
259
260 SpacedLeafImtProvider {
261 root,
262 leaves,
263 subtree_levels,
264 }
265 }
266}
267
268impl ImtProvider for SpacedLeafImtProvider {
269 fn root(&self) -> pallas::Base {
270 self.root
271 }
272
273 fn non_membership_proof(&self, nf: pallas::Base) -> Result<ImtProofData, ImtError> {
274 let k = find_range_for_value(&self.leaves, nf).ok_or_else(|| {
275 ImtError(alloc::format!(
276 "nullifier {nf:?} not in any punctured range"
277 ))
278 })?;
279
280 let nf_bounds = self.leaves[k];
281 let leaf_pos = k as u32;
282
283 let empty = empty_imt_hashes();
284 let mut path = [pallas::Base::zero(); IMT_DEPTH];
285
286 let mut idx = k;
287 for l in 0..5 {
288 let sibling_idx = idx ^ 1;
289 path[l] = self.subtree_levels[l][sibling_idx];
290 idx >>= 1;
291 }
292
293 for l in 5..IMT_DEPTH {
294 path[l] = empty[l];
295 }
296
297 Ok(ImtProofData {
298 root: self.root,
299 nf_bounds,
300 leaf_pos,
301 path,
302 })
303 }
304}