Redemption Circuit

The Redemption Circuit (redemption.circom, 174 LOC) is the specialized circuit for the GHOST token use case. It proves that a user committed a specific amount of tokens to the Merkle tree and is entitled to withdraw some or all of them — without revealing which commitment is being spent, how much was originally deposited, or who deposited it.

This circuit handles the full complexity of private token operations: commitment verification, nullifier derivation (double-spend prevention), amount conservation, partial withdrawals with change commitments, and policy binding.

Public Inputs

The Redemption Circuit has 8 public inputs — values that are visible on-chain and verified by the smart contract:

#	Input	Type	Description
0	root	Field element	The Merkle tree root being proven against. The contract checks this matches a known historical root.
1	nullifier	Field element	Unique identifier derived from the commitment. Recorded on-chain to prevent double-spending.
2	withdrawAmount	Field element	The amount of tokens being withdrawn in this transaction.
3	recipient	Field element	The recipient's address, bound to the proof to prevent front-running.
4	changeCommitment	Field element	A new commitment for any remaining funds (0 if full withdrawal).
5	tokenId	Field element	Hash identifying the token type (e.g., GHOST, gUSDC).
6	policyId	Field element	Policy contract address (0 for no policy).
7	policyParamsHash	Field element	Hash of the policy parameters (0 for no policy).

Private Inputs

The circuit has 7 private inputs — values known only to the prover that never appear on-chain:

Input	Type	Description
secret	Field element	The user's secret, part of the commitment preimage.
nullifierSecret	Field element	A separate secret used to derive the nullifier.
amount	Field element	The original deposit amount.
blinding	Field element	Random blinding factor that makes the commitment hiding.
pathElements[20]	Field element[20]	Sibling hashes along the Merkle proof path.
pathIndices[20]	Bit[20]	Left/right direction bits for each level of the tree.
newBlinding	Field element	Fresh blinding factor for the change commitment.

Constraint Walkthrough

The circuit enforces correctness through seven sequential steps, each adding constraints to the R1CS system.

Step 1: Compute Commitment from Preimage

The circuit computes the commitment as a 7-input Poseidon hash of all preimage fields:

$$\text{commitment} = \text{Poseidon}_7(\text{secret},\; \text{nullifierSecret},\; \text{tokenId},\; \text{amount},\; \text{blinding},\; \text{policyId},\; \text{policyParamsHash})$$

This uses the Commitment() sub-circuit. The 7-input structure ensures that the commitment is bound to the token type, amount, policy, and the user's secrets. Knowing the commitment hash alone reveals nothing about its preimage — the blinding factor provides computational hiding.

Step 2: Verify Merkle Tree Membership

The circuit uses MerkleTreeChecker(20) to verify that the computed commitment exists as a leaf in the Merkle tree with the claimed root. The proof walks 20 levels of the tree:

• At each level, a DualMux orders the current hash and the sibling (pathElements[i]) based on the direction bit (pathIndices[i]).
• A Poseidon2 hash computes the parent node.
• After 20 levels, the computed root must equal the public input root.

This proves membership without revealing which leaf the commitment occupies. The verifier sees only the root, not the leaf index or any intermediate hashes.

Step 3: Compute Leaf Index from Path Indices

The LeafIndex(20) sub-circuit reconstructs the leaf's position in the tree from the binary path indices:

$$\text{leafIndex} = \sum_{i=0}^{19} \text{pathIndices}[i] \cdot 2^i$$

This value is used in the next step for nullifier derivation. It ensures the nullifier is bound to a specific tree position, preventing certain classes of nullifier collision attacks.

Step 4: Derive and Verify Nullifier

The nullifier is derived as a nested Poseidon hash:

$$\text{nullifier} = \text{Poseidon}_2\!\big(\text{Poseidon}_2(\text{nullifierSecret},\; \text{commitment}),\; \text{leafIndex}\big)$$

The circuit computes this value and constrains it to equal the public input nullifier. This serves two purposes:

1. Double-spend prevention: once the nullifier is recorded on-chain, the same commitment cannot be spent again.
2. Unlinkability: the nullifier reveals nothing about the commitment or the user's secrets. An observer cannot determine which tree leaf was spent by examining the nullifier.

The nested hash structure (binding to both the commitment and the leaf index) prevents an attacker from constructing a different commitment at the same leaf position that yields the same nullifier.

Step 5: Range Check Amounts (252-bit)

The circuit enforces amount conservation through range checks:

changeAmount = amount - withdrawAmount

Three Num2Bits(252) decompositions enforce that:

• amount fits in 252 bits (non-negative, within field range)
• withdrawAmount fits in 252 bits (non-negative)
• changeAmount fits in 252 bits (non-negative, meaning withdrawAmount <= amount)

The 252-bit bound (rather than 256-bit) leaves headroom below the BN254 scalar field prime (~254 bits), preventing overflow attacks where an attacker could wrap around the field to create tokens from nothing.

Step 6: Compute Change Commitment

For partial withdrawals (when withdrawAmount < amount), the circuit computes a change commitment for the remaining funds:

$$\text{changeCommitment} = \text{Poseidon}_7(\text{secret},\; \text{nullifierSecret},\; \text{tokenId},\; \text{changeAmount},\; \text{newBlinding},\; \text{policyId},\; \text{policyParamsHash})$$

The circuit handles two cases:

Case	Condition	changeCommitment
Full withdrawal	changeAmount == 0	Must be 0
Partial withdrawal	changeAmount > 0	Must match computed Poseidon7(...)

An IsZero check on changeAmount selects between these cases. The change commitment is inserted into the Merkle tree by the contract, creating a new spendable UTXO for the remaining balance. Policy fields carry forward into the change commitment, ensuring that policy restrictions survive partial withdrawals.

Step 7: Bind Recipient and Policy

The final step creates dummy quadratic constraints that bind the recipient, policyId, and policyParamsHash public inputs to the proof:

recipientSquare = recipient * recipient
policyIdSquare = policyId * policyId
policyParamsHashSquare = policyParamsHash * policyParamsHash

These constraints do not perform logical checks — their purpose is to make the proof invalid if anyone changes these public inputs after proof generation. Without these constraints, an attacker could take a valid proof and substitute a different recipient address (front-running the reveal transaction). The quadratic form ensures the Groth16 prover commits to these values during proof generation.

Circuit Instantiation

The circuit is instantiated at the bottom of redemption.circom with a tree depth of 20 (supporting ~1 million commitments):

component main {public [root, nullifier, withdrawAmount, recipient,
                        changeCommitment, tokenId, policyId, policyParamsHash]}
    = GhostRedemption(20);

The {public [...]} declaration tells the Groth16 compiler which inputs are public (visible to the verifier) versus private (known only to the prover).

Relationship to the Broader Protocol

The Redemption Circuit is one of two circuits in Specter. It handles the token-specific use case: burning GHOST tokens into a commitment and later minting fresh tokens from a ZK proof. The Access Proof Circuit handles the general data access use case, which requires no nullifier, no amounts, and no recipient binding — just pure authentication against committed data.

Together, these two circuits cover the full spectrum of Specter's privacy operations: one-time value transfers (Redemption) and persistent data access (Access Proof).