Ironwood $\leftarrow \text{Setup}(1^{\lambda })$

$\text{Ironwood}$ is a project to deploy a new shielded pool, built to restore confidence for all Zcash'rs in the supply integrity of Zcash.

A formal verification is in progress, which is intended to cover at least soundness of the Action circuit used by the Orchard and Ironwood pools, before the NU6.3 upgrade that activates the latter. An important part of this effort will be to clearly and accurately document the scope of what is and is not formally verified.

Documentation

• $\text{The Ironwood Book}$

License

Copyright 2026 Zcash Protocol Developers.

All code in this workspace is licensed under either of

• Apache License, Version 2.0, (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
• MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)

at your option.

Contribution

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.

Concepts

$\text{Ironwood}$ is the project to deploy a new shielded value pool for Zcash: the Ironwood pool. The Ironwood pool reuses the Orchard protocol —the Orchard action shape, keys, and proof system— while keeping its own state, separate from the Orchard pool, and using a new note plaintext format for quantum-recoverable notes.

At a high level, $\text{Ironwood}$ introduces:

• a new shielded value pool and value balance, the Ironwood pool, with its own note commitment tree and nullifier set but reusing the Orchard protocol;
• transaction version 6, which is version 5 with an Ironwood-pool bundle added;
• quantum-recoverable note plaintexts for Ironwood-pool notes;
• a rule that no funds can flow into the Orchard pool after NU6.3; and
• a circuit update that lets Orchard-pool notes be withdrawn or split into change notes, without allowing new value to enter that pool.

Relationship To Orchard

We distinguish the Orchard protocol —the shared action shape, keys, proof system, and note machinery— from the Orchard pool and the Ironwood pool, the two value pools that use it. Each pool has its own note commitment tree, nullifier set, and value balance.

The Ironwood pool reuses the Orchard protocol's action and zero-knowledge proof structure. This keeps the transition smaller than introducing an entirely new shielded protocol from first principles.

The important distinction is that the Ironwood pool is not "more Orchard-pool state". It has its own value balance, note commitment tree, and nullifier set. An Ironwood-pool note is represented with Orchard-protocol note machinery, but it is committed into the Ironwood pool's note commitment tree and spent against the Ironwood pool's nullifier set.

This lets the existing Orchard receiver and viewing-key infrastructure remain useful while creating a clean state boundary between legacy Orchard-pool funds and Ironwood-pool funds.

Quantum-Recoverable Notes

ZIP 2005 defines a new Orchard-protocol note plaintext format with lead byte $0x03$: the quantum-recoverable note plaintext format. The Ironwood pool adopts this format for its notes.

In wallet-facing code, Ironwood-pool notes are Orchard-shaped notes using the quantum-recoverable note plaintext format. The note plaintext format of Orchard-pool notes remains unchanged. Ironwood-pool notes use that pool's treestate when they are spent.

Value Movement After NU6.3

After NU6.3 activation, no funds can flow into the Orchard pool. Transactions can still spend Orchard-pool funds, and zero-balance Orchard-pool actions are still allowed, but the Orchard pool's value balance must not be negative.

Wallet-created payments and change that would previously have produced Orchard-pool outputs are routed to the Ironwood pool after NU6.3. This moves newly created shielded value into the Ironwood pool while still allowing legacy Orchard-pool notes to be spent.

Transaction Version 6

A new transaction format, version 6, is introduced in order to add an Ironwood-pool bundle. There are no other transaction format changes from v5 (there is a change to the signature hashing needed to support anchor update).

A version 6 transaction can contain:

• transparent inputs and outputs,
• bundles for each of the Sapling, Orchard, and Ironwood pools.

The Sapling-pool and transparent components are unchanged from version 5. The Orchard-pool and Ironwood-pool bundles follow the same Orchard-protocol bundle structure, but they are separate bundles in the transaction. The Ironwood-pool bundle uses different personalization strings for its transaction and authorization hashes.

Anchor update

NU6.3 introduces an additional change for v6 transactions, applying to all of the pools that version supports (Sapling, Orchard, and Ironwood), that allows a transaction to be signed and then have its anchor updated later. This can improve privacy by leaking less information about when the transaction was signed.

Preliminaries

Quantum Recoverability

Quantum recoverability is the note-level change that defines Ironwood-pool notes. It does not make the current Orchard protocol post-quantum. Instead, it changes how new Ironwood-pool notes are created so they can be recovered into a future shielded protocol if the current elliptic-curve-based protocol ever has to be disabled.

The threat model is supply integrity. If an attacker can break discrete logarithms on the curves used by Zcash, then the existing Sapling-pool and Orchard-pool note commitments are not binding against that attacker. Even if Zcash later upgraded its proof system and rebuilt note commitments with a post-quantum hash, an attacker could otherwise try to forge a note that was not actually in the commitment tree.

Quantum-recoverable notes address this by changing how note commitment randomness is derived.

Ironwood-Pool Notes

ZIP 2005 defines a new Orchard-protocol note plaintext format with lead byte $0x03$: the quantum-recoverable note plaintext format. The Ironwood pool adopts this format for its notes. ZIP 2005 defines and analyses this new format and how it is used; it does not by itself define the Ironwood pool, or its note commitment tree or nullifier set. Those are layered on top of the ZIP 2005 note-level change.

Orchard-pool notes still use note plaintext lead byte $0x02$. For those notes, the note commitment randomness is derived only from $\mathsf{rseed}$ and $\text{ρ}$. $\mathsf{rseed}$ is the 32-byte random seed the sender picks for a note. When a note is created, its $\text{ρ}$ is set to $\mathsf{n}{\mathsf{f}}^{\mathsf{old}}$, the nullifier of the input note spent in the same action (the nullifier that action reveals).

For Ironwood-pool notes, the randomness is instead derived from the entire note contents. The derivation binds the randomness to:

• the diversifier-derived point,
• the recipient public key,
• the note value,
• $\text{ρ}$, and
• the note-specific $\text{φ}$ value.

In effect, the note contents become part of the randomness derivation.

flowchart LR
    subgraph V2["Orchard-pool note"]
        V2Inputs["$\mathsf{rseed},\text{ρ}$"] --> V2Rcm["$\mathsf{rcm}$"]
    end

    subgraph Ironwood["Ironwood-pool (QR) note"]
        IronwoodInputs["$\mathsf{rseed},{\mathsf{g}}_{\mathsf{d}},\mathsf{p}{\mathsf{k}}_{\mathsf{d}},\mathsf{v},\text{ρ},\text{φ}$"] --> IronwoodRcm["$\mathsf{rcm}$"]
    end

    IronwoodRcm --> Future["future recovery statement can check derivation"]

This makes it possible for a future recovery protocol to prove that a recovered note corresponds to a real note with fixed contents, rather than to a forged choice of note fields. Because $\mathsf{rcm}$ is now a hash of the note contents, the derivation can be recomputed from the recovered fields and checked against the on-chain commitment. The Ironwood-pool spend proof does not itself enforce this derivation; the check is instead carried out by a future, dedicated recovery statement that proves $\mathsf{rcm}$ was derived from the note contents.

Ironwood-pool outputs are Orchard-shaped notes using the quantum-recoverable note plaintext format. The Ironwood pool still uses Orchard-shaped actions, receivers, and note encryption. The distinction is that Ironwood-pool notes use the quantum-recoverable note plaintext format, are committed into the Ironwood pool's note commitment tree, and are spent against the Ironwood pool's nullifier set.

What This Does Not Do

Quantum recoverability is not a post-quantum shielded protocol by itself.

It does not:

• make current Orchard-protocol spends post-quantum secure,
• define the future recovery protocol in full,
• choose a future post-quantum proof system, or
• choose a future post-quantum note commitment tree.

It is a forward-compatibility change. The goal is to make funds created as recoverable notes usable by a later recovery protocol, without requiring Zcash to choose that future protocol today.

Why This Matters For Ironwood

The Ironwood pool is where newly created shielded value goes after NU6.3. Using Ironwood-pool notes means new Ironwood-pool funds are created in the recoverable format from the start.

This gives Zcash a migration path: existing value can be moved into the Ironwood pool, and Ironwood-pool notes are structured so that a future post-quantum transition has the information it needs to recover those funds.

Further reading:

• ZIP 2005: Ironwood Quantum Recoverability

User Documentation

Design

This page summarizes the main design decisions behind $\text{Ironwood}$.

Overview

Goals

$\text{Ironwood}$ introduces a new shielded pool without discarding the parts of the Orchard protocol that are still useful. The design therefore separates consensus state while reusing Orchard-shaped actions, proofs, receivers, and wallet infrastructure where possible.

The result is the Ironwood pool, with a smaller implementation and deployment surface than a fully independent shielded protocol.

New Shielded Pool

The Ironwood pool is a new shielded value pool and value balance, based on the Orchard protocol. This is consensus-relevant: transactions account for Ironwood-pool value separately from the Sapling and Orchard pools.

Version 6 transactions support the following pools:

• transparent,
• Sapling,
• Orchard, and
• Ironwood.

Transaction version 6 is based on transaction version 5 and adds an Ironwood-pool bundle. The transparent and Sapling-pool components are unchanged from version 5. The Orchard-pool component is the same bundle as in version 5, but version 6 changes how it is hashed and verified; see Orchard-Pool Bundle Changes in Version 6.

Pool State

Separate State

The Ironwood pool has a separate note commitment tree and a separate nullifier set.

This is the main boundary between the Orchard and Ironwood pools. Even though an Ironwood-pool action has the Orchard action shape, its note commitments are appended to the Ironwood pool's tree, and its nullifiers are checked against the Ironwood pool's nullifier set.

This prevents the Orchard and Ironwood pools from sharing anonymity-set state by accident, and gives a clean migration path away from legacy Orchard-pool state.

Chain History Tree

The chain history tree (the FlyClient MMR introduced in ZIP 221) gains Ironwood-pool metadata. From NU6.3 onward, history nodes use a new node-data version that, in addition to the existing Sapling-pool and Orchard-pool fields, commits to:

• the Ironwood pool's note commitment tree root at the start of the node's block range,
• the Ironwood pool's note commitment tree root at the end of the node's block range, and
• the number of transactions in the range that contain an Ironwood-pool bundle.

The effect is that, from NU6.3 onward, the chain history commitment binds the Ironwood pool's tree state and Ironwood-pool activity of every block range, just as it already binds the Sapling and Orchard pools.

Actions and Notes

Ironwood-Pool Bundle

The Ironwood-pool bundle reuses the Orchard-protocol action and bundle structure. In the implementation this appears as a second Orchard-shaped bundle in the transaction encoding.

This means the Ironwood pool inherits, from the Orchard protocol:

• the Orchard-protocol action layout;
• the Orchard-protocol authorization structure;
• the Orchard-protocol note encryption, modified for quantum recoverability;
• Orchard-protocol proof construction; and
• Orchard-protocol bundle padding behavior.

Quantum recoverability is the only note-level change for new Ironwood-pool outputs. The rest of the bundle structure follows the Orchard protocol.

Orchard Circuit Constraint

After NU6.3, the Orchard pool is constrained so that it can only remove value from the Orchard pool or split existing Orchard-pool notes into change notes. It must not allow new value to enter the Orchard pool.

This means the Orchard pool remains usable for legacy note handling:

• an Orchard-pool note can be withdrawn out of the Orchard pool;
• an Orchard-pool note can be split into multiple Orchard-pool change notes; and
• zero-balance Orchard-pool actions remain possible.

But transactions cannot use the Orchard pool as a destination for newly created value. New shielded outputs that would previously have been Orchard-pool outputs are routed to the Ironwood pool instead.

The "split into change notes" half of this constraint (requiring each retained output to return to the address it was spent from) is enforced in the Action circuit as the cross-address restriction. The "no new value" half is the value-balance rule below. See Action Circuit for the exact circuit mechanism.

Quantum-Recoverable Ironwood-Pool Notes

ZIP 2005 defines a new Orchard-protocol note plaintext format with lead byte $0x03$: the quantum-recoverable note plaintext format. The Ironwood pool adopts this format for its notes.

This gives the Ironwood pool a concrete note-level distinction while preserving the Orchard keys and receiver handling. Wallet code can therefore model Ironwood-pool notes as Orchard-shaped notes, but classify them by note plaintext format:

• Orchard-pool notes use the existing note plaintext format, and
• Ironwood-pool notes use the quantum-recoverable note plaintext format.

When an Ironwood-pool note is spent, the witness is obtained from the Ironwood pool's note commitment tree, not the Orchard pool's tree.

Transaction Format and Hashing

Version 6 Transaction Format

Transaction version 6 adds the Ironwood-pool bundle to the transaction format. The bundle order is:

1. transparent bundle,
2. Sapling-pool bundle,
3. Orchard-pool bundle,
4. Ironwood-pool bundle.

The Ironwood-pool bundle uses the same Orchard-protocol bundle serialization as the Orchard-pool bundle, but is interpreted in the Ironwood-pool context.

Version 6 is the default transaction version that wallets SHOULD use from NU6.3 activation. Transaction versions 4 and 5 remain valid.

Orchard-Pool Bundle Changes in Version 6

The Orchard-pool bundle keeps its version 5 layout, but version 6 changes it in three consensus-visible ways. Together these wind the Orchard pool down so that it only supports transactions that take value out of the pool or that send it to one of the expanded receivers spent from in the same transaction.

• Flag encoding. The flags byte gains a new enableCrossAddress flag (bit 2). After NU6.3 an Orchard-pool bundle must not set it: consensus rejects a version 6 Orchard-pool bundle that does, restricting Orchard-pool actions to change or withdrawal. An Ironwood-pool bundle, by contrast, may set it. See Action Circuit.
• Anchor placement. For every supported pool (Sapling, Orchard, and Ironwood), the anchor is excluded from the version 6 txid and signature hash and is committed in the authorization digest instead. See Transaction Hashing.
• Verifying key. From NU6.3, Orchard-pool actions are verified with the post-NU6.3 circuit verifying key, which is selected by block height (not by transaction version), so that the cross-address restriction is enforceable on them. This binds Orchard-pool actions in version 5 transactions as well as version 6.

The Orchard-protocol action machinery is otherwise reused.

Transaction Hashing

The Ironwood-pool bundle uses Orchard-protocol bundle and action hashing, but with Ironwood-pool-specific personalization strings.

This applies to:

• Ironwood-pool bundle hashing,
• Ironwood-pool action compact hashing,
• Ironwood-pool action memo hashing,
• Ironwood-pool action non-compact hashing, and
• Ironwood-pool authorization hashing.

The version 6 transaction ID tree includes an Ironwood-pool component digest after the Orchard-pool one. An empty Ironwood-pool bundle is represented by its own empty-bundle digest, not by reusing the Orchard-pool empty-bundle digest.

Version 6 signature hashing uses the version 6 transaction hash path. This ensures signatures bind to the Ironwood-pool bundle when it is present.

The bundle anchor is excluded from version 6 txid and signature hashing, and is committed in the authorization digest instead. Because the signature no longer binds the anchor, a spend can be pre-signed before the anchor it is finalized against exists. The anchor is still bound at the consensus layer, through the block's authorizing-data commitment.

Consensus Value Rules

Post-NU6.3 Orchard-Pool Value Rule

After NU6.3 activation, no funds can flow into the Orchard pool. Transactions must not have a negative Orchard-pool value balance.

The rule still permits:

• spending existing Orchard-pool value,
• positive Orchard-pool value balances, where value exits the Orchard pool, and
• zero-balance Orchard-pool actions.

This lets wallets spend existing Orchard-pool funds while preventing newly created shielded value from being placed back into the Orchard pool.

Coinbase After NU6.3

Because new value may not enter the Orchard pool after NU6.3, coinbase rules change so that block rewards are never paid into it:

• Empty Orchard component. A coinbase transaction must contain no Orchard-pool actions at all. Coinbase reward outputs are routed to the Sapling pool or transparent receivers; the Orchard receiver is no longer a reward destination after NU6.3, and a miner address whose unified address contains only an Orchard receiver is rejected for coinbase use.
• Coinbase value balance. The coinbase balance check accounts for the Ironwood-pool value balance alongside the Sapling and Orchard pools, and Ironwood-pool coinbase outputs must be recoverable, as already required for the Sapling and Orchard pools, so that coinbase funds are not burned.
• No coinbase spends. A coinbase transaction must not enable spends in its Ironwood-pool bundle, mirroring the existing rule for the Orchard pool.

Wallet and Tooling

Wallet Routing

Wallet-created Orchard-receiver outputs are routed to the Ironwood pool after NU6.3.

Before NU6.3, an Orchard receiver produces an Orchard-pool output. After NU6.3, the same receiver produces an Ironwood-pool output using the quantum-recoverable note plaintext format. Change follows the same rule: Orchard-pool change after NU6.3 is emitted as Ironwood-pool change.

This allows legacy Orchard-pool notes to migrate out through ordinary spends while ensuring new outputs land in the Ironwood pool.

Wallets must keep track of which pool a note is in (as they already need to do for notes in the Sapling and Orchard pools), and use the appropriate anchor and witness path when spending them.

Wallet Storage And APIs

The Ironwood pool is exposed as a distinct pool in wallet-facing state, while reusing Orchard-protocol note data internally.

Wallet storage tracks:

• Ironwood-pool note commitment tree metadata,
• Ironwood-pool shardtree state,
• Ironwood-pool nullifier observations,
• Ironwood-pool balances,
• Ironwood-pool Orchard-protocol received notes, and
• pool distinctions for sent and received outputs.

Compact block and lightwallet protocol data also grow Ironwood-pool fields:

• Ironwood-pool action data,
• Ironwood-pool note commitment tree size,
• Ironwood-pool tree state, and
• Ironwood-pool subtree roots.

This gives light clients enough information to maintain the Ironwood pool's note commitment tree and detect Ironwood-pool spends and outputs independently of the Orchard pool.

PCZT

Partially-created Zcash transactions include an Ironwood-pool bundle in the updated PCZT format.

PCZT version 2 can carry:

• transparent data,
• Sapling-pool data,
• Orchard-pool data, and
• Ironwood-pool data.

The PCZT action fields also include the note plaintext version, because verifiers and provers need it to reconstruct note commitments.

Status

Open Placeholders

The current design still has placeholders that should be finalized before a production protocol specification:

• final activation heights and deployment rules.

The circuit and proof-system changes, previously open here, are now specified in Action Circuit. From NU6.3 a single Action circuit version —the Orchard-protocol Action circuit plus one new constraint, the cross-address restriction— is used for both the Orchard and Ironwood pools, with its own proving and verifying keys.

Transaction Format

Version 6 follows the version 5 transaction format, with an Ironwood-pool bundle added after the Orchard-pool bundle. Within version 6, the Orchard-pool bundle keeps its version 5 layout but gains a new enableCrossAddress flag. See Orchard-Pool Bundle Changes in Version 6.

At the transaction ID layer, the Ironwood-pool bundle is another child in the transaction hash tree:

flowchart TD
    TxId["txid<br/>ZcashTxHash_ || consensusBranchId"]

    Header["header digest<br/>version, branch ID, lock time, expiry height"]
    Transparent["transparent digest"]
    Sapling["Sapling-pool digest"]
    Orchard["Orchard-pool bundle digest"]
    Ironwood["Ironwood-pool bundle digest"]

    TxId --> Header
    TxId --> Transparent
    TxId --> Sapling
    TxId --> Orchard
    TxId --> Ironwood

The Orchard-pool and Ironwood-pool bundle digests have the same structure. The difference is that the Ironwood-pool bundle uses its own personalization strings at each bundle-hash node:

flowchart TD
    OrchardBundle["Orchard-pool bundle digest<br/>ZTxIdOrchardH_v6"]
    IronwoodBundle["Ironwood-pool bundle digest<br/>ZTxIdIronwd_H_v6"]

    subgraph Shape["Same Orchard-protocol bundle hash shape"]
        Compact["actions compact hash<br/>nf, cmx, epk, compact ciphertext"]
        Memos["actions memo hash<br/>memo ciphertext"]
        NonCompact["actions non-compact hash<br/>cv, rk, remaining enc ciphertext, out ciphertext"]
        Flags["bundle flags"]
        Value["value balance"]
    end

    OrchardBundle --> Compact
    OrchardBundle --> Memos
    OrchardBundle --> NonCompact
    OrchardBundle --> Flags
    OrchardBundle --> Value

    IronwoodBundle -. same fields .-> Compact
    IronwoodBundle -. same fields .-> Memos
    IronwoodBundle -. same fields .-> NonCompact
    IronwoodBundle -. same fields .-> Flags
    IronwoodBundle -. same fields .-> Value

The same rule applies to authorization hashing: the Ironwood-pool bundle follows the Orchard-pool bundle authorization structure, but uses Ironwood-pool-specific personalization strings.

In version 6 the bundle anchor is excluded from the txid bundle digest shown above, and is instead committed in the authorization digest. This keeps both the txid and the signature sighash independent of the anchor, so that a spend can be signed before the anchor it is finalized against —the note-commitment-tree root— exists.

Action Circuit

From NU6.3, both the Orchard and Ironwood pools use a single Action circuit version (OrchardCircuitVersion::PostNU6_3). It inherits the proof system, curves, gadgets, and action statement from the Orchard protocol unchanged, and adds exactly one circuit-level constraint: a configurable cross-address restriction that, when active, forces an action's output note to be addressed to the same expanded receiver (${\mathsf{g}}_{\mathsf{d}}$ and $\mathsf{p}{\mathsf{k}}_{\mathsf{d}}$) as the note it spends.

What Ironwood Reuses

A post-NU6.3 action, in either pool, proves the Action Statement (Orchard) plus the cross-address restriction below, reusing the same machinery: the same Halo 2 proof system and gadgets.

The post-NU6.3 circuit keeps the same advice columns, the same custom gates, and the same circuit size as the pre-NU6.3 one. Post-NU6.3 proofs are therefore the same size as pre-NU6.3 proofs. They are also the same size between the Orchard-pool and Ironwood-pool bundles.

The Cross-Address Restriction

The one new circuit constraint enforces a same-receiver property. A note is addressed to an expanded receiver, represented in the circuit by the diversified base ${\mathsf{g}}_{\mathsf{d}}$ and the diversified transmission key $\mathsf{p}{\mathsf{k}}_{\mathsf{d}}$. When the restriction is active, an action's output note and spent note must share that expanded receiver:

$({\mathsf{g}}_{\mathsf{d}},\mathsf{p}{\mathsf{k}}_{\mathsf{d}})$ of the output note must equal $({\mathsf{g}}_{\mathsf{d}},\mathsf{p}{\mathsf{k}}_{\mathsf{d}})$ of the spent note.

When active, the restriction limits each action to change (the output returns to the spent note's address) or withdrawal (value leaves the pool through a positive value balance), rather than a cross-address transfer. Its purpose is to discourage economic activity within the pool.

This is the circuit mechanism behind the Orchard Circuit Constraint: after NU6.3, legacy Orchard-pool actions disable cross-address transfers and the Orchard pool is wound down, while pools that accept new payments (the Ironwood pool) keep cross-address transfers enabled.

The companion rule that no new value may enter the Orchard pool after NU6.3 (that the Orchard pool's value balance must not be negative) is not enforced by this circuit. The per-action circuit only ties ${\mathsf{v}}^{\mathsf{old}}-{\mathsf{v}}^{\mathsf{new}}$ to the action's value commitment $\mathsf{c}{\mathsf{v}}^{\mathsf{net}}$; the sign of the bundle's value balance is a transaction-level concern outside the orchard crate. See Post-NU6.3 Orchard-Pool Value Rule.

A new public input

The public-input layout is unified across all circuit versions: every version's instance carries the same ten public inputs, with disableCrossAddress added after the existing Orchard-protocol action inputs.

The bundle-level flag is enableCrossAddress (the NU6.3 flag, bit 2); the circuit-level public input is its negation, $\mathsf{disableCrossAddress}$. The post-NU6.3 circuit constrains it: $0$ imposes no extra constraint, and $1$ enforces the same-expanded-receiver property above. Older circuit versions carry and commit the input but leave it unconstrained, relying on the proving and verification API to reject a set flag they cannot enforce. Because instance columns are zero-padded over the evaluation domain, an unrestricted statement ($\mathsf{disableCrossAddress}=0$) commits identically to the pre-NU6.3 nine-input instance encoding.

How the constraint is enforced

The post-NU6.3 circuit adds the constraint without adding a gate or a column. The existing "Orchard circuit checks" gate (which checks value balance, the computed Merkle root against the anchor, and the enable flags) already contains a product constraint of the form ${\mathsf{v}}^{\mathsf{old}}\cdot (\mathsf{root}-\mathsf{anchor})=0$, exactly the shape needed for $\mathsf{disableCrossAddress}\cdot (\mathsf{coor}{\mathsf{d}}^{\mathsf{old}}-\mathsf{coor}{\mathsf{d}}^{\mathsf{new}})=0$.

The circuit reuses that gate on four extra rows, one per affine coordinate of ${\mathsf{g}}_{\mathsf{d}}$ and $\mathsf{p}{\mathsf{k}}_{\mathsf{d}}$. Copy constraints place $\mathsf{disableCrossAddress}$ and the spent and output coordinates into the gate, and its selector is enabled on those rows; with the gate's other terms neutralized, the surviving constraint is:

$$\mathsf{disableCrossAddress}\cdot (\mathsf{coor}{\mathsf{d}}^{\mathsf{old}}-\mathsf{coor}{\mathsf{d}}^{\mathsf{new}})=0$$

Any nonzero $\mathsf{disableCrossAddress}$ forces each coordinate of the output address to equal the spent address; a zero leaves them free. The check is conditional on the flag and does not rely on the flag being boolean.

Keys And Enforcement

The post-NU6.3 circuit (OrchardCircuitVersion::PostNU6_3) is a new circuit version in the orchard crate that extends the fixed post-NU6.2 circuit with the cross-address constraint. It ships with its own proving and verifying keys.

• The verifying key differs. Enabling the shared gate on the four extra rows changes the circuit's fixed (selector) columns, so the post-NU6.3 verifying key is distinct from the fixed-circuit verifying key, even though the proof size and verification cost are unchanged.
• Restricted statements require the post-NU6.3 keys. Because older versions cannot constrain $\mathsf{disableCrossAddress}$, it is incorrect to use those versions with an instance that includes the $\mathsf{disableCrossAddress}$ instance variable.

The circuit is the cryptographic enforcement point: a prover cannot satisfy a restricted statement with a cross-address output. The builder, PCZT, and signer layers add a same-receiver structural check so that honest participants do not construct a restricted bundle that would fail to prove.

Orchard- to Ironwood-pool Migration

Moving existing Orchard-pool funds into the Ironwood pool is an ordinary version 6 transaction rather than a special protocol operation: it spends Orchard-pool notes and creates Ironwood-pool outputs. It is the case where the post-NU6.3 rules compose. The Orchard-pool side has a positive value balance (value leaves the Orchard pool, which the value rule permits), and the Ironwood-pool side has a negative value balance (value enters the Ironwood pool); the two net to the fee.

Exact wallet migration mechanics to be described.

Formal Verification

Ironwood's formal verification is a Lean 4 development (over Mathlib) in this repository: verifier soundness for the deployed Halo 2 verifier under Zcash/Snark/, and the protocol security-property layers (binding-signature balance, key binding, and the ledger-model security games) under Zcash/Security/. This page documents two development-wide conventions: how security breaks are represented, and what the development is allowed to trust.

Breaks as computed data

The security arguments are reduction-style: a theorem shows that a violation of a protocol property exhibits a concrete break of an underlying primitive — a discrete-log relation, a hash collision, a commitment-opening collision. Hardness assumptions are consumed only at the computational layer, against the exhibited break.

Care is needed in how "exhibits" is stated. In a prime-order group, a nontrivial discrete-log relation between any two elements always exists; for any compressing hash, collisions always exist by pigeonhole. So a Prop that existentially quantifies over the break data ("there exist distinct inputs with equal outputs") is simply true at every instantiation of interest. A theorem concluding property ∨ ∃-break is then vacuous, and a hypothesis ¬ ∃-break is unsatisfiable. Proof irrelevance makes this unrecoverable: even when a proof constructs the break honestly, a consumer of the statement cannot extract it.

The convention:

• Break events are structures carrying the breaking data (the colliding queries, the relation coefficients), with Prop certificates attached. Examples: RandomOracle.Collision and RandomOracle.CollisionUpToSign (the ±-collision shape produced by coordinate-extractor arguments — and the Merkle tree-hash collision computed by Merkle.collisionOfWrongLeaf is a Collision directly), Ledger.NoteCommitBreak, and BindingSignature.NontrivialRelation (the discrete-log relation computed from a non-balancing verifying bundle).
• Reductions are plain computable defs producing them, such as Merkle.collisionOfWrongLeaf, noteCommitBreakOfNe, and the NontrivialRelation.ofImbalance family (through to the per-pool Orchard and Sapling bundle capstones, whose balance statements are the contrapositives under discrete-log relation hardness). A structure with data fields cannot be inhabited by proof-irrelevant existence, and a plain def cannot conjure the data from mere existence via choice — the compiler enforces this, so noncomputable is not permitted for these definitions.
• Efficiency of a reduction is the one property Lean cannot express; it is established by inspection. The constructions here are straight-line manipulations of their inputs.
• Predicates over named witnesses (for example, a key-binding break of two specific witnesses) keep their content as Props: the breaking pair is bound in the statement rather than existentially closed.

The principle's scope is computational reductions: it applies wherever the argument is that an efficient adversary achieving some effect would thereby violate a computational assumption. For that argument to have content, the reduction must be the kind of object an adversary's output can be fed through — a computable function producing the break the assumption forbids. It is not a constructivism requirement on the development at large. Classical.choice is used throughout Mathlib and throughout the Prop-valued reasoning here, and Lean is not intended to support purely constructive proofs. The point is that choice must not be what produces the break data: a noncomputable reduction could satisfy its type by using classical choice to "find" the break, proving nothing about efficient adversaries. Ordinary theorems, and the Prop certificate fields inside break structures, remain freely classical.

Trust discipline

Following the pattern of CompElliptic's trust discipline, the development distinguishes general theorems from concrete, closed computational facts, and holds them to different trust standards.

General, quantified theorems (the soundness statements and security reductions) must rest only on the standard classical axioms propext, Classical.choice, and Quot.sound. No sorry, no additional axioms, no compiler trust.

Concrete, closed facts with no free variables may additionally use native_decide (which discharges a goal by running compiled native code, adding a compiler-trust axiom) and the kernel's GMP-backed bignum arithmetic. The principal such fact in this repository is the captured fingerprint match fingerprint_matches: a single numeric check that the Lean verifier's assembled multi-scalar multiplication equals the Rust verifier's on a captured proof. The CompElliptic dependency applies the same discipline to its concrete curve-arithmetic facts (cardinalities, primality certificates). Such facts are independently re-checkable (another implementation, or hand computation, would compute the same result), so a miscompiled or buggy oracle could in principle be caught by disagreement.

These boundaries are checked at build time, not merely documented:

• Zcash.Snark.Fingerprint.TrustBoundary pins the fingerprint match: assert_no_sorry walks the elaborated dependency graph, so a sorry hidden in any transitive dependency fails the build; and a #guard_msgs-pinned #print axioms freezes the exact axiom set, so a newly introduced axiom fails the build. The pin also documents precisely which compiler-trust axiom native_decide adds — on this toolchain a per-declaration axiom (…_native.native_decide.ax_1_1), where older Lean versions used the global Lean.ofReduceBool. Pinning it keeps that claim verified rather than remembered, which is the point of the discipline: unpinned claims about the trusted base drift silently as toolchains change.
• Zcash.Security.Ledger.TrustBoundary and Zcash.Security.BindingSignature.TrustBoundary pin the break reductions the same way. The ledger reductions rest on propext and Quot.sound only; the binding-signature relation reductions additionally record Classical.choice, entering only through erased Prop certificate fields — in both cases the definitions compile as plain defs, so the break data cannot have been conjured from mere propositional existence.
• CI builds both as part of the default targets, and fingerprint_matches's native_decide compiles and runs the verifier, so anything noncomputable on the assembled-verifier path fails the build.

Coined terms and shorthand for the development, including the two conventions above, are collected in the glossary.

Proof Journey

Follow the verifier-soundness argument in logical order, with the stacked and parallel PR provenance attached to the stage where each mechanized layer enters.

Explore the complete map

Proof Map

One connected picture of the verifier-soundness proof.

Watch the Proof Journey.  ·  New to the terms? See the Glossary.

Glossary

Coined terms and shorthand used across the proof map and the Lean development. Anchors point to a module + name under Zcash/.