> For the complete documentation index, see [llms.txt](https://valargroup.gitbook.io/shielded-vote-docs/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://valargroup.gitbook.io/shielded-vote-docs/circuit-components/imt-non-membership.md).

# IMT Non-Membership

**Used in:** ZKP #1 (condition 13)

## What it does

Proves that a note's real nullifier is **not** in the nullifier Indexed Merkle Tree (IMT) at the snapshot height. This establishes that the note was unspent at snapshot time.

## Background: the (low, width) leaf model

The nullifier exclusion tree is built by taking all known nullifiers, sorting them, and converting them into **exclusion intervals**. Each leaf stores a `(low, width)` pair where `width = high - low` is pre-computed during tree construction, defining a gap between consecutive known nullifiers. If a value falls within some leaf's interval (`value - low <= width`), it is guaranteed not to be an existing nullifier.

The leaf hash is `Poseidon(low, width)`, and a standard Poseidon Merkle path authenticates the leaf against the public root.

The IMT is initialized with \~17 sentinel nullifiers at multiples of `2^250`, covering the full Pallas field. This guarantees every bracket has width < `2^250`, which is required for the range checks to be sound. Inserting a real nullifier only splits a bracket into two smaller ones, so this invariant holds permanently.

## Circuit

The prover witnesses:

* `low` — interval start (low bound of the bracketing leaf)
* `width` — interval width (`high - low`, pre-computed during tree construction)
* `leaf_pos` — position of the leaf in the tree
* `path[0..29]` — sibling hashes along the 29-level Merkle path

The circuit performs three steps:

### 1. Leaf hash + Merkle path (29 levels)

```
leaf_hash = Poseidon(low, width)
```

At each level, an `ImtSwapGate` places `(current, sibling)` into `(left, right)` based on the position bit, then computes `parent = Poseidon(left, right)`. After 29 levels, the computed root is constrained to equal the public `nullifier_imt_root`.

Total Poseidon calls: 1 (leaf hash) + 29 (path) = 30 per note.

### 2. Interval check

The `IntervalGate` proves `low <= real_nf <= low + width` using 2 constraints:

```
x = real_nf - low                      (offset from low bound)
x_shifted = 2^250 - width + x - 1      (upper bound check)
```

The `width = high - low` subtraction is pre-computed during tree construction, reducing the in-circuit constraint count from 3 to 2.

### 3. Range checks

Both `x` and `x_shifted` are range-checked to `[0, 2^250)` using 25 limbs of the 10-bit lookup table:

* **`x` in `[0, 2^250)`** proves `real_nf >= low` — if `real_nf < low`, the subtraction wraps to a value ≥ `2^250` and fails.
* **`x_shifted` in `[0, 2^250)`** proves `real_nf <= low + width` — if `real_nf > low + width` then `x > width`, so `x_shifted >= 2^250` and fails.

These two checks together enforce `low <= real_nf <= low + width`.

## Why this matters

In ZCash, a note is "spent" when its nullifier appears on-chain. To prove you own an unspent note, you must prove your nullifier is **not** in the set of all published nullifiers. The IMT structure makes this efficient — exclusion proofs are logarithmic in the number of nullifiers.

## Client-side considerations

The full set of Orchard nullifiers is \~2GB. Rather than downloading this, the client uses PIR (Private Information Retrieval) to fetch exclusion proofs without revealing which nullifier it is querying. See [Design Principles — PIR](/shielded-vote-docs/overview/design-principles.md).

## Capacity

The tree depth is 29, giving 2^29 ≈ 537 million leaf slots. Each nullifier insertion splits one bracket into two (adding one leaf), so the tree supports \~537M nullifiers without any circuit change. Today Zcash has \~50M Orchard nullifiers — over 10x headroom. If the tree ever fills, increasing the depth by 1 doubles capacity at the cost of one additional Poseidon hash per proof.

## Note on padded notes

Padded notes have randomly-generated nullifiers that won't appear in the IMT. The non-membership check is still performed for circuit uniformity — it will always pass for random nullifiers.

## See also

* [`imt.rs`](https://github.com/valargroup/voting-circuits/blob/main/voting-circuits/src/delegation/imt.rs) — out-of-circuit IMT utilities and `SpacedLeafImtProvider`
* [`imt_circuit.rs`](https://github.com/valargroup/voting-circuits/blob/main/voting-circuits/src/delegation/imt_circuit.rs) — `ImtSwapGate`, `IntervalGate`, and `synthesize_imt_non_membership`