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 ff::PrimeField;
13use halo2_gadgets::poseidon::primitives::{self as poseidon, ConstantLength};
14use pasta_curves::pallas;
15use std::string::String;
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
94impl std::error::Error for ImtError {}
95
96/// Trait for providing IMT non-membership proofs.
97///
98/// Implementations must return proofs against a consistent root — all proofs
99/// from the same provider must share the same `root()` value.
100pub trait ImtProvider {
101    /// The current IMT root.
102    fn root(&self) -> pallas::Base;
103    /// Generate a non-membership proof for the given nullifier.
104    fn non_membership_proof(&self, nf: pallas::Base) -> Result<ImtProofData, ImtError>;
105}
106
107// ================================================================
108// SpacedLeafImtProvider (available for proof generation and tests)
109// ================================================================
110
111use ff::Field;
112use std::vec::Vec;
113
114/// Precomputed empty subtree hashes for the IMT (Poseidon-based).
115///
116/// `empty[0] = Poseidon3(0, 0, 0)` (hash of an all-zero punctured-range leaf),
117/// `empty[i] = Poseidon(empty[i-1], empty[i-1])` for i >= 1.
118pub fn empty_imt_hashes() -> Vec<pallas::Base> {
119    let empty_leaf = poseidon_hash_3(
120        pallas::Base::zero(),
121        pallas::Base::zero(),
122        pallas::Base::zero(),
123    );
124    let mut hashes = vec![empty_leaf];
125    for _ in 1..=IMT_DEPTH {
126        let prev = *hashes.last().unwrap();
127        hashes.push(poseidon_hash_2(prev, prev));
128    }
129    hashes
130}
131
132/// Sentinel spacing exponent: sentinels are placed at `k * 2^249`.
133/// With K=2 punctured ranges each leaf spans two consecutive intervals,
134/// giving outer span `2 * 2^249 = 2^250` — matching the circuit's 250-bit
135/// range check.
136const SENTINEL_EXPONENT: u64 = 249;
137
138/// Number of sentinel multiples: `0, 1*step, 2*step, ..., 32*step`.
139/// `32 * 2^249 = 2^254` covers the Pallas field (p ≈ 2^254.9).
140const SENTINEL_COUNT: u64 = 32;
141
142/// Build the sorted, deduplicated, odd-count sentinel list used by both
143/// [`SpacedLeafImtProvider`] and the production `prepare_nullifiers` path.
144///
145/// Sentinels: `k * 2^249` for `k = 0..=32`, plus `p - 1` to close the tail.
146/// If the count is even after dedup, `Fp::from(2)` is inserted after sentinel 0
147/// to make it odd (collision probability ≈ 2^{-254}).
148fn build_sentinel_list() -> Vec<pallas::Base> {
149    let step = pallas::Base::from(2u64).pow([SENTINEL_EXPONENT, 0, 0, 0]);
150    let mut nfs: Vec<pallas::Base> = (0u64..=SENTINEL_COUNT)
151        .map(|k| step * pallas::Base::from(k))
152        .collect();
153    nfs.push(-pallas::Base::one()); // p - 1
154    nfs.sort();
155    nfs.dedup();
156    if nfs.len() % 2 == 0 {
157        debug_assert_eq!(nfs[0], pallas::Base::zero(), "sentinel 0 must be first");
158        nfs.insert(1, pallas::Base::from(2u64));
159    }
160    nfs
161}
162
163/// Build punctured-range triples from a sorted, deduplicated, odd-count
164/// nullifier list. Mirrors `imt_tree::tree::build_punctured_ranges` so the
165/// test fixture is protected by the same ordering invariant as production.
166fn build_punctured_ranges_local(sorted_nfs: &[pallas::Base]) -> Vec<[pallas::Base; 3]> {
167    let n = sorted_nfs.len();
168    assert!(n >= 3, "need at least 3 sorted nullifiers, got {n}");
169    assert!(n % 2 == 1, "sorted nullifier count must be odd (got {n})");
170
171    let num_leaves = (n - 1) / 2;
172    (0..num_leaves)
173        .map(|i| {
174            let base = i * 2;
175            let (lo, mid, hi) = (sorted_nfs[base], sorted_nfs[base + 1], sorted_nfs[base + 2]);
176            assert!(
177                lo < mid && mid < hi,
178                "punctured range {i} violates strict ordering: \
179                 nf_lo={lo:?}, nf_mid={mid:?}, nf_hi={hi:?}"
180            );
181            [lo, mid, hi]
182        })
183        .collect()
184}
185
186/// Find the punctured-range index containing `value`. Mirrors
187/// `imt_tree::tree::find_punctured_range_for_value`.
188fn find_range_for_value(ranges: &[[pallas::Base; 3]], value: pallas::Base) -> Option<usize> {
189    let i = ranges.partition_point(|[nf_lo, _, _]| *nf_lo < value);
190    if i == 0 {
191        return None;
192    }
193    let idx = i - 1;
194    let [nf_lo, nf_mid, nf_hi] = ranges[idx];
195    let offset = value - nf_lo;
196    let span = nf_hi - nf_lo;
197    if offset == pallas::Base::zero() || offset >= span {
198        return None;
199    }
200    if value == nf_mid {
201        return None;
202    }
203    Some(idx)
204}
205
206/// IMT provider with evenly-spaced K=2 punctured-range brackets.
207///
208/// Mirrors the production sentinel injection path: sentinels at `k * 2^249`
209/// for `k = 0..=32`, plus `p - 1`, sorted, deduplicated, and padded to odd
210/// count with `Fp::from(2)`. Each interior leaf spans exactly `2^250`,
211/// satisfying the circuit's 250-bit range check. The tail leaf covers
212/// `[32*step, p-1]` with span `≈ 2^126`, well under the bound.
213///
214/// Used for proof generation (fixture generators) and testing.
215#[derive(Debug)]
216pub struct SpacedLeafImtProvider {
217    /// The root of the IMT.
218    root: pallas::Base,
219    /// Punctured-range triples: `[nf_lo, nf_mid, nf_hi]` for each leaf.
220    leaves: Vec<[pallas::Base; 3]>,
221    /// Bottom levels of the subtree (32-leaf subtree → 5 levels).
222    /// `subtree_levels[0]` has 32 leaf hashes Poseidon3(nf_lo, nf_mid, nf_hi),
223    /// `subtree_levels[5]` has 1 subtree root.
224    subtree_levels: Vec<Vec<pallas::Base>>,
225}
226
227impl SpacedLeafImtProvider {
228    /// Create a new spaced-leaf IMT provider (K=2 punctured-range model).
229    ///
230    /// Builds the same sentinel layout as the production `prepare_nullifiers`
231    /// path: sorted, deduplicated, padded to odd count, then grouped into
232    /// punctured-range triples with strict ordering validation.
233    pub fn new() -> Self {
234        let sorted_nfs = build_sentinel_list();
235        let leaves = build_punctured_ranges_local(&sorted_nfs);
236        let empty = empty_imt_hashes();
237
238        let empty_leaf_hash = poseidon_hash_3(
239            pallas::Base::zero(),
240            pallas::Base::zero(),
241            pallas::Base::zero(),
242        );
243        let mut level0 = vec![empty_leaf_hash; 32];
244        for (k, bounds) in leaves.iter().enumerate() {
245            level0[k] = poseidon_hash_3(bounds[0], bounds[1], bounds[2]);
246        }
247
248        let mut subtree_levels = vec![level0];
249        for _l in 1..=5 {
250            let prev = subtree_levels.last().unwrap();
251            let mut current = Vec::with_capacity(prev.len() / 2);
252            for j in 0..(prev.len() / 2) {
253                current.push(poseidon_hash_2(prev[2 * j], prev[2 * j + 1]));
254            }
255            subtree_levels.push(current);
256        }
257
258        let mut root = subtree_levels[5][0];
259        for l in 5..IMT_DEPTH {
260            root = poseidon_hash_2(root, empty[l]);
261        }
262
263        SpacedLeafImtProvider {
264            root,
265            leaves,
266            subtree_levels,
267        }
268    }
269}
270
271impl ImtProvider for SpacedLeafImtProvider {
272    fn root(&self) -> pallas::Base {
273        self.root
274    }
275
276    fn non_membership_proof(&self, nf: pallas::Base) -> Result<ImtProofData, ImtError> {
277        let k = find_range_for_value(&self.leaves, nf)
278            .ok_or_else(|| ImtError(format!("nullifier {nf:?} not in any punctured range")))?;
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}