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.

Verifying the proofs

The formalization is a Lean 4 development over Mathlib, and building it re-elaborates every proof — a successful build is the verification. The single command is lake build, with two one-time prerequisites: install elan (the Lean toolchain manager, which reads lean-toolchain and installs the pinned toolchain automatically), then, from the repository root, fetch Mathlib's prebuilt artifacts so it need not be recompiled from source:

lake exe cache get   # one-time: download prebuilt Mathlib artifacts
lake build           # verify everything (exactly what CI runs)

Documentation

• 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 — and where the model idealizes the deployed verifier.

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 — for example a discrete-log relation, a hash collision, or 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) rest, in their abstract form over an arbitrary Fp-module, only on the standard classical axioms propext, Classical.choice, and Quot.sound — no sorry, no additional axioms, no compiler trust. Instantiated at a concrete Pasta curve they additionally inherit one compiler-trust axiom: CompElliptic's curve point-count, a closed computational fact discharged by native_decide (below). This applies to both the SNARK soundness endpoints (Vesta) and the Action circuit soundness (Pallas). The +native flag on the corresponding build-time checks records exactly which endpoints carry it.

@[csimp] replacement lemmas get their own assert_axioms entries in Zcash/TrustBoundary.lean, enforced by scripts/check_csimp_census.sh in CI: the compiler applies a csimp substitution in all downstream compiled code, but the axioms of the lemma's own proof are not propagated into downstream native_decide axiom tracking ( lean4#7463), so the check must sit on the lemma itself. The underlying mechanism study — what native_decide, the interpreter, and precompiled native code actually trust — is design/lean-native-trust-research.md in the CompElliptic repository.

Native-executing checks are temporary, and opt-in until they go. Executing a check through locally compiled native code (a precompileModules dylib — ours, or the CompElliptic pin's) trusts the C emitter, the local C toolchain, and the loader, coarse-grained and with no axiom trace. That is a real extension of the trusted base, and the performance it buys does not justify it: these checks are slated for removal rather than for permanent accommodation, and the discipline below is what contains them in the meantime, not a settled design. Loading a lane's dylib is inseparable from elaborating modules that import it, so the enforced invariant sits at the level of checks: no module whose import closure reaches a lane module may contain an evaluation-based check (#eval, #guard, native_decide) unless explicitly opted in — a documented review discipline; nothing in CI enforces it today. Appendix C of the research document linked above records the observed Lake behaviour behind this rule.

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 facts in this repository are the four derived-form fingerprint boundary theorems nonInteractiveFingerprint_matches_derived (the generated per-capture fingerprint_matches are their raw forms): numeric checks that the Lean verifier's assembled multi-scalar multiplication equals the Rust verifier's on each captured proof — two honest, two at random inputs. 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.TrustBoundary is the top-level census for reusable library claims — the key-binding, birthday, ledger, and binding-signature break reductions together with the fixture-free SNARK binding/knowledge-soundness stack (the executable extractors, the endpoints across the modeled adversaries, and the DL capstones). Zcash.lean imports it directly, so lake build Zcash enforces that census. Concrete capstones stay with their captures in the fixture-local trust-boundary modules and are enforced by FixtureCheck. The obligations use two commands from Zcash.Meta.AxiomCheck:

• assert_axioms d fails the build unless d rests only on the standard classical axioms (propext, Classical.choice, Quot.sound) — in particular no sorry and no native_decide; assert_axioms d +native additionally permits the toolchain-dependent native_decide compiler-trust axiom that the curve-instantiated endpoints carry. Unlike a #guard_msgs-pinned #print axioms, it states the expected tier in one line and stays green across toolchain bumps that rename the native_decide axiom, while still failing the moment a declaration reaches beyond its tier. It covers the general soundness theorems, probability bounds, and run-time/query-charge lemmas.
• assert_computable d additionally requires d to be a plain def — not noncomputable — so it guards the breaks-as-computed-data discipline: the data-producing reductions (a collision, fold, peel, or fork turned into a discrete-log relation) stay genuinely computable, closing the gap where a reduction could silently become noncomputable and still build. Classical.choice is admitted only through erased Prop certificate fields (+choice); the relation coefficients are direct terms of the inputs, so the break data cannot have been conjured from mere propositional existence. +native covers the Vesta producers.

The boundaries kept as literal pins are the four fixture censuses — Zcash.Snark.Fixtures.SingleAction.Honest.TrustBoundary, …MultiAction.Honest.TrustBoundary, and their two …Random.TrustBoundary siblings — which belong to the FixtureCheck target (kept out of lake build Zcash because the captures are large and slow). Each states its tier with assert_axioms like the rest of the development, and additionally retains #guard_msgs-pinned #print axioms checks on fingerprint_matches and the derived boundary theorems, documenting 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 — because for a captured fingerprint match the exact axiom set is the claim, the case Zcash.Meta.AxiomCheck reserves the pinned form for. CI builds all five default targets — Zcash, FixtureCheck, CircuitCheck, MetaCheck, and SecurityCheck — and each fingerprint_matches's native_decide compiles and runs the verifier, so anything noncomputable on the assembled-verifier path fails the build.

What the fixture captures actually check is the statement of record in each family's Boundary.lean — nonInteractiveFingerprint_matches_derived — with the quantified match and its ε in Snark/Fingerprint/Epsilon.lean and the per-capture headliners in Fixtures/*/Random/Epsilon.lean. Capture lineage, seeds, and the reproducibility pipeline are in Zcash/Snark/Fixtures/PROVENANCE.md. Together, the captures and ε theorems support the typed, post-decoding Rust↔Lean boundary, not universal byte-level refinement. Byte encoding, transcript domain-prefix bytes, and Blake2b remain external; Snark/Fingerprint/Match.lean enumerates this boundary, tracked in #66.

The circuit-side layout fixtures are pinned, not regenerated. The CS and layout dumps behind CircuitCheck's TestVk* comparisons (Zcash/Circuits/Fixtures/*.json) were emitted by one-off instrumentation of halo2/orchard that was never published, so unlike the verifier-fingerprint captures they have no regenerate-and-diff pipeline: CI pins their bytes (SHA256SUMS, with a set-equality check so an unpinned dump cannot be added), and those pins live in the same repository they guard. Independent anchoring exists at verifying-key granularity — Keygen/Certificate.lean checks the key derived from the ported circuit against the release-regenerated capture — but the row-level layout content below the key, and the base-circuit dump (actionBaseLayout.json), which has no capture-side anchor at all, rest on the pinned bytes plus review. Lineage, and the follow-up to regenerate these from released sources, are recorded in Zcash/Circuits/Fixtures/PROVENANCE.md.

Modelling boundaries

The trust discipline above bounds what the proofs rest on. One boundary sits outside it, in what the statements model: it is neither an axiom nor a compiler-trust question, so no census sees it.

Fiat–Shamir is idealized. The deployed verifier derives each challenge by hashing the transcript so far with Blake2b and reducing 64 bytes to a field element. The development models that as an abstract squeeze (Verifier/FiatShamir.lean) and, in the security layer, as a uniform random oracle — the assumption that carries interactive soundness to the deployed non-interactive check. Identifying the deployed hash with that oracle is external, over and above the byte-level boundary noted above: the fixtures check challenge schedules against typed captures, not against transcript bytes.

Coined terms and shorthand for the development are collected on the Definitions page.

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 Definitions.

Security Models

The ledger security games under Zcash/Security/ and the verifier-soundness capstones under Zcash/Snark/ traced by the proof map share one methodology. This page describes it: the shape every argument follows, the adversary models the theorems are stated in, and where hardness judgements actually live.

Every argument has the same shape, the development-wide breaks as computed data convention:

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

So each definition sits on a three-layer stack:

• Layer A — vocabulary. The break events, as structures carrying their data (RandomOracle.Collision, NontrivialRelation, NoteCommitBreak). Deterministic; no probability.
• Layer B — reduction. A computable def that turns a property violation into a Layer-A break (NontrivialRelation.ofImbalance, Merkle.collisionOfWrongLeaf, noteCommitBreakOfNe). Deterministic; no hardness assumption.
• Layer C — probability. The bound that producing the break is hard: the birthday bound $q\cdot (q-1)/|\mathbb{F}|$, or the discrete-log advantage. The only layer that consumes an assumption.

What a reduction in these models says

The capstones are reductions in idealized models: the challenge hash is modelled as a random oracle, and on the generator-RO endpoints the adversary is restricted to be algebraic. A theorem of this kind says: an algebraic adversary in the random-oracle model that wins the protocol game, under the stated conditions, would need to be able to compute a nontrivial discrete-log relation —tightly equivalent to computing a discrete log (Jaeger–Tessaro, Expected-Time Cryptography: Generic Techniques and Applications to Concrete Soundness, Lemma 3)— with an advantage and resource cost that is related in terms of concrete efficiency. The same content is sometimes stated as: an adversary that wins the game either exhibits a discrete-log break or falls outside the modelled class — an inclusive or, since an adversary that wins the game by non-algebraic means could potentially do so by breaking the underlying problem.

What such a theorem does not say is "assuming (among other things) that discrete log is hard, the protocol is secure". Discrete-log hardness is not a premiss of the theorem, and it could not be one. Zcash is defined over fixed curves and hash sizes; it is not a family of protocols indexed by a security parameter. Even if it were, what we care about is the security of the concrete deployed system. Defining concrete efficiency is not the obstacle — resources can be counted directly, with no need for polynomial time as a proxy. The obstacle is that the relations among the deployed bases are fixed constants: an adversary that hard-codes, say, the discrete log of $\mathcal{R}$ base $\mathcal{V}$ is concretely tiny, so "no efficient adversary finds a nontrivial relation among the deployed bases" is false as stated, even though we conjecture that nobody can exhibit such an adversary. More subtly, there are also adversaries that hard-code the results of an infeasibly expensive precomputation, allowing discrete logarithms to be computed cheaply even at targets not fixed in advance (Bernstein–Lange, section 3 of Non-uniform cracks in the concrete: the power of free precomputation, Asiacrypt 2013).

Restricting the adversary's access until such bounds become provable is exactly the generic-group model — but the resulting theorem would then be restricted to generic adversaries (Shoup, Lower bounds for discrete logarithms and related problems, Eurocrypt 1997), and would not say anything about the protocol's security for its instantiated curves such as Pallas and Vesta.

There are two different techniques that can help to overcome this problem in a concrete-security development:

1. We can present an explicit computable reduction, with exact resource accounting, from winning the game to an exhibited discrete-log solver.
2. We can consider the adversary's advantage against a family of protocols ranging over the choices of random bases, modelling hash functions as random oracles where necessary. These bases can be on the actual curves, and the random oracles can have the same input and output types as in the actual protocol.

At least one of the two is needed to defuse the hard-coded adversary, and either would technically suffice:

• Under 2, the bases are sampled inside the experiment; the adversary does not know them when it starts, and so a hard-coded constant is useless.
• Under 1, no hardness claim is stated at all, and the reduction returning a nontrivial relation is a meaningful security argument whether or not a winning adversary hard-coded its discrete log.

Our approach is to use 1 for all reductions, and 2 when it allows obtaining a tighter reduction. We always use 1 because it is essentially free: in a development where we take the effort to make some reductions computable, it is consistent to make all of them computable. We sometimes additionally use 2 because, using 1 alone, there is sometimes no known way to obtain a tightly efficient reduction: against fixed bases the reduction has no randomness into which to embed its discrete-log challenge, so extraction must rewind the adversary — the forking route, with the tightness losses that brings. Sampling the bases, on the other hand, lets the reduction embed the challenge into the basis randomness and extract straight-line, with no multiplicative loss.

Embedding the challenge into the basis randomness is legitimate because it does not change the game. Given a discrete-log challenge $(B,C)$ —seeking the $z$ with $C=z•B$— the reduction sets each base to $x•B+y•C$ with its own fresh uniform pair $(x,y)$ per base. Such bases are exactly uniform: the adversary's view is identical to the honestly sampled game, so its success probability is unchanged, and the challenge is hidden perfectly rather than computationally. What the reduction gains is private knowledge of the pairs. A returned relation among the bases then becomes a linear equation in $z$, solvable unless the relation's coefficients land on the single $1/|\mathbb{F}|$ hyperplane where the $y$ component cancels — the form of reduction the definitions page calls programmed-basis. The argument is Jaeger–Tessaro's proof of their Lemma 3, presented there as a careful use of self-reducibility techniques.

The judgement that the exhibited solver is beyond reach is a statement about the current state of cryptanalytic knowledge, supplied by the reader rather than by the mathematics — Rogaway's "human ignorance" approach (Formalizing Human Ignorance, Vietcrypt 2006). Even outside formalization, time-bounded universal hardness claims for a fixed primitive are subtle: free precomputation converts memory into online speed at a quantified exchange rate (Corrigan-Gibbs–Kogan, The Discrete-Logarithm Problem with Preprocessing, Eurocrypt 2018: generic preprocessing attacks with advice $S$ and online time $T$ achieve success $\epsilon$ with $S\cdot T^2$ on the order of $\epsilon \cdot N$, and this is tight); non-uniform definitions admit unrealistic counterexample algorithms, as discussed above (Bernstein–Lange); and whether the non-uniform model is the right one at all is itself debated (Koblitz–Menezes, Another look at non-uniformity).

The Lean interface encodes this division of labour — the mathematics exhibits the reduction, and the reader supplies the hardness judgement. TextbookDLAdvantageLE and its coin-carrying variant bound the winning-coins measure of one named algorithm —the relation finder the reduction constructs— and the finite-security profiles instantiate that bound with a caller-supplied advantage function, evaluated at the finder's accounted resources. The advantage function is arbitrary, and the theorems are generic in it: nothing about the difficulty of discrete log is assumed anywhere in the development. A capstone converts a belief about achievable discrete-log advantage at a given cost into a bound on the protocol game; it does not certify the belief.

The resource numbers are coverage parameters

The Snark-side capstones quote concrete numbers: the covered adversary's random-oracle queries are bounded by $2^{123}$ and its group work by $2^{123}$ —or $2^{125}$ in a staged-certified variant— with a statistical remainder ($2^{-83}$ for the consensus-generic Action capstone) proved for every workload up to the full covered budget. The instantiated formula endpoint quotes an eight-fold finder envelope —a three-bit overhead, since the finder replays a bounded number of traversals— evaluating the advantage at $2^{126}$ oracle queries and group operations. The staged-certified endpoints instead count the reduction's work additively, by a proved counter composition, and evaluate it at $2^{124}$ queries and $2^{126}$ group operations — the group work including the adversary's own at the larger budget. It is easy to misread the envelope as an estimate of Vesta's discrete-log cost; it is in fact a coverage parameter. The target is as large as is useful —past roughly $2^{126}$ group operations an adversary can compute Vesta discrete logs directly, voiding every binding property here (see the lifetime caveat below)— and no smaller, so that no adversary with a meaningful guarantee is excluded.

The near-coincidence with Pollard rho's estimated cost on Vesta (about $2^{126}$, using the curve's automorphisms) is therefore a stopping rationale, not a dependence: a revised attack estimate would change the interpretation, not the theorem. And the quoted bound is the worst covered point: the theorems evaluate the advantage function at the finder's exact accounted counts, and substituting the larger envelope numbers can only increase it. Since generic-attack success falls off steeply below its threshold, an adversary far below the target gets a far stronger interpreted bound. Reading resource-parameterized claims this way —as attack-cost curves rather than single thresholds— follows Bernstein, Understanding brute force, 2005.

The algebraic-adversary restriction

An algebraic adversary is one that, whenever it outputs a group element, also supplies a representation: coefficients expressing that element over the elements it has received (Fuchsbauer–Kiltz–Loss, The Algebraic Group Model and its Applications, Crypto 2018). Only the provenance of output group elements is restricted. The computation deciding the coefficients is unrestricted — the adversary may inspect encodings, branch on bits, and use any structure it can see. In this development the restriction is part of the adversary's type in the online-AGM layer, not a named hypothesis on any capstone — which is why this page states it: conditions carried by the quantifier domain are as load-bearing as named hypotheses, and less visible in theorem statements.

Like the random-oracle model, this is a heuristic restriction of the adversary's strategy class, not an assumption that could be true or false of Pallas or Vesta. Random-oracle non-instantiability (Canetti–Goldreich–Halevi, The Random Oracle Methodology, Revisited) is the standing warning against reading in-model theorems as instantiated guarantees. The heuristic earns its keep only if two supporting claims hold. First, re-expression: an adversary that is only incidentally non-algebraic must be re-expressible as an algebraic one at similar cost. Every generic adversary is algebraic —it only ever combines the elements it received— so the algebraic-adversary restriction is strictly weaker than the generic-group one; the substance is the claim that the concrete curves offer no useful operations that are neither generic nor algebraic. Second, the known deviations of the curves from generic must not obstruct the re-expression. Pasta's efficient endomorphism is the sharp example: it acts as scalar multiplication by a known cube root of unity, so an adversary using it remains algebraic — its outputs still carry representations. The same structure genuinely cheapens the best generic attacks (the automorphism-class rho walk behind the $2^{126}$ figure above), which the coverage parameters absorb. Deviating from generic and obstructing algebraicity are different failures, and the endomorphism is the first (since it can reduce the number of group operations required) without being the second.

The remaining supporting claim is that the modelled basis covers everything a realistic adversary can obtain. That is a claim about hash-to-curve, and it belongs with the reference-string discussion below.

Fixed bases, hash-to-curve, and the reference string

Several reductions bottom out at discrete log by treating a set of group elements as independent — for example the value-commitment bases $\mathcal{V}$ and $\mathcal{R}$, the Sinsemilla generators, and the proof system's inner-product reference string. Independence is what turns "find a nontrivial relation among these elements" into the discrete-log game: the reduction models each base as a random multiple of one generator and embeds its discrete-log challenge into that randomness.

In the deployed protocol, though, these bases are fixed. Each is produced once, by hashing public strings to the curve with GroupHash (spec §5.4.9.8), and the resulting outputs are baked into the protocol as a Uniform Reference String. The gap between the two is the standard gap for protocols with a URS. We prove security for the family of protocols that sample the bases at random, over the distribution of that randomness. Then we argue heuristically that the deployed protocol, which fixes them via hash-to-curve, inherits it — provided that the hash-to-curve scheme admits no attack more efficient than the algebraic ones bounded by the proven reductions. No Lean theorem instantiates the soundness endpoints at the deployed bases; identifying Halo2's hash-to-curve outputs with the sampled basis is the heuristic step (Zcash/TrustBoundary.lean records this scope). The same heuristic underlies every fixed-base use of hash-to-curve here, including the value and note commitments, the Merkle hash, and the proof system's reference string. The same primitive also produces bases on demand: DiversifyHash derives each diversified address base from GroupHash at key generation.

This heuristic comes with an important caveat: an adversary has the protocol's entire lifetime to attack that one specific reference string — for example, to search for a discrete log relating the value-commitment bases $\mathcal{V}$ and $\mathcal{R}$. Such an attack could have started as soon as Orchard was designed, long before any particular transaction it would compromise. A bound that holds for random bases does not preclude an attack tuned to the deployed bases, and the cost of finding one is amortized over every transaction ever made against them. The caveat is not speculative: a rational adversary would certainly prefer this strategy, since it dominates all others based on breaking discrete logs — it does not provide free precomputation, but it gives the adversary more time over which to pay the cost. That is a known, acknowledged limitation of this development.

This sharpens the potential threat from quantum computers or other discrete-log attacks: a single discrete-log computation is catastrophic to the protocol as a whole, rather than localized to a specific user or key. Against these fixed bases, one discrete-log computation is sufficient to break binding/knowledge-soundness properties for the entire protocol, not just for a single transaction or user. That includes Balance properties, Spendability, and Spend authority, although not privacy. Migrating away from reliance on discrete-log binding/knowledge-soundness is therefore a whole-protocol concern, not a per-transaction one. See ZIP 2005 for further discussion.

What makes a hash-to-curve output a good base is that it comes with no known representation over previously received elements. The same property cuts the other way for the adversary model. A realistic adversary can evaluate GroupHash directly on inputs of its choice, and every output it obtains is a group element held with no representation over a fixed basis — so an adversary with that access is not algebraic over any fixed finite basis. The faithful modelling makes hash-to-curve itself an oracle of the game: the adversary may query it, each fresh output joins the AGM basis as a new independent element, and the reduction may embed its challenge in programmed outputs. The development does not currently model that access. Each game fixes an enumerated basis of the generators its honest algorithms use, and its theorems quantify over adversaries algebraic over that basis. Two consequences should be stated plainly. For games whose honest parties themselves call DiversifyHash —Spendability and Spend Authority, where key generation derives the diversified base— the modelled adversary cannot express strategies a realistic adversary performs routinely, so those games need the oracle in the adversary's interface before their capstones carry their intended weight. And enumerating, per game, the generators judged relevant leaves out fixed bases from other protocol components that a deployed adversary can obtain; nothing known suggests they help, but "nothing known suggests" is itself a heuristic judgement, and it should be visible rather than implicit. Both are known limitations of the current modelling (#188).

These models and their limitations are part of every statement in the development: a capstone's bound is no stronger than the adversary class it quantifies over. For the property statements the models scope, see the Ledger Security Games; for the verifier-soundness half, the Proof Map; for the coined terms, the Definitions.

Ledger Security Games

The proof map traces verifier knowledge soundness — the deployed Halo 2 verifier under Zcash/Snark/. This page is its companion for the other half of the development: the protocol security properties under Zcash/Security/. It covers:

• the top-level capstones — the ledger-model security games of Balance integrity, Spendability, and Spend authority;
• how each capstone connects, by reduction via intermediate security properties such as binding-signature balance, key binding, and verifier knowledge soundness, to an exhibited break of a cryptographic primitive in a specified adversary model.

Every argument here follows the breaks as computed data convention and the three-layer stack described in Security Models.

One connected picture

%%{init: {"flowchart": {"nodeSpacing": 20, "rankSpacing": 50, "padding": 6, "diagramPadding": 4, "subGraphTitleMargin": {"top": 4, "bottom": 18}}, "themeCSS": ".cluster-label { font-weight: 700; font-size: 1.1em; font-family: raleway, sans-serif; } marker { overflow: visible !important; } marker path { transform-box: fill-box !important; transform-origin: center !important; transform: scale(1.25) !important; }"}}%%
flowchart TD
  subgraph GAMES["Ledger capstones"]
    BAL["Balance integrity<br/>orchardBalanceIntegrity_measure_le"]
    SPEND["Spendability<br/>faerieGoldCore<br/>validLedger_append"]
    SPENDAUTH["Spend authority<br/>orchardSpendAuthority_measure_le"]
  end

  BAL --> BS["Binding-signature<br/>balance"]
  BAL --> NCB["Note-commitment<br/>binding"]
  BAL --> MERK["Merkle-path<br/>binding"]
  BAL --> KB["Key binding<br/>ZIP 2005"]
  SPEND --> BAL
  SPEND ---> NCB
  SPEND ---> MERK
  SPEND ---> KB
  SPEND ---> NFB["Nullifier binding"]
  SPEND ---> SPENDAUTH
  SPENDAUTH --> KB

  subgraph ASSUMPTIONS["Hardness assumptions"]
    DL[("Discrete log")]
  end

  subgraph MODELS["Heuristic adversary models"]
    ROM[("Random oracle")]
  end

  BS --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/BindingSignature/Balance.lean'>non-balancing<br/>bundle computes</a>"| NDLR["NontrivialRelation<br/>(<span class='katex'><span class='mord mathcal'>V</span></span>,&nbsp;<span class='katex'><span class='mord mathcal'>R</span></span>) discrete-log<br/>relation"]
  BS --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/ExtractionArm.lean'>verifying signature<br/>the extractor misses</a>"| KERR["RedDSA<br/>extractability"]
  BS --> STMT["Witness or replay<br/>evidence<br/>ActionSatisfied<br/>§4.17.4"]
  NCB --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Statement.lean'>wrong note<br/>opening computes</a>"| NCBK["NoteCommitBreak"]
  NCB --> STMT
  MERK --> STMT
  MERK --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Merkle.lean'>wrong Merkle<br/>path computes</a>"| MC["DefinedCollision<br/>one height,<br/>encoding domain"]
  KB --> STMT
  KB --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/KeyBindingDLR.lean'>Orchard-protocol<br/>CommitIvkCollision<br/>computes</a>"| SDLR
  KB --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/KeyBinding/Basic.lean'>conflicting ivk<br/>witnesses compute</a>"| CUS["CollisionUpToSign<br/>shifted oracle,<br/>distinct queries"]
  NFB --> STMT
  NFB --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Spendability.lean'>distinct derive-inputs +<br/>equal nullifier<br/>computes</a>"| NFC["NullifierCollision"]
  SPENDAUTH --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/SpendAuthority.lean'>verified signature over<br/>unsigned sighash computes</a>"| SAF["SpendAuthForgery<br/>(randomization<br/>of ±ak)"]

  STMT STMTtoKS@-. "<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Snark/Soundness/Composition/Bridge.lean'>justified by<br/>the extractor</a>" .-> KS["Knowledge soundness:<br/>accepting proof yields<br/>witness or break data"]
  NCBK --> SDLR["Sinsemilla<br/>discrete-log<br/>relation"]

  KERR KERRtoNDLR@==>|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/RedDSA/Extraction.lean'>good challenge<br/>computes</a>"| NDLR
  KERR --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/RedDSA/KnowledgeError.lean'>challenge hash as random<br/>oracle; query-time labels<br/>pin the bad challenge</a>"| ROM
  NDLR -->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/BindingSignature/DiscreteLog.lean'>independent<br/>hash-to-curve bases</a>"| DL
  SDLR -->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/BindingSignature/DiscreteLog.lean'>independent<br/>hash-to-curve bases</a>"| DL
  KS KStoDL@===>|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Snark/Soundness/Action/AdaptiveStatementKnowledge.lean'>independent<br/>hash-to-curve bases</a>"| DL
  KS -->|"<a target='_blank' href='https://github.com/zcash/ironwood/tree/main/Zcash/Snark/Soundness/FiatShamir'>Fiat–Shamir<br/>heuristic</a>"| ROM
  MC --> SDLR
  CUS --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/Common/Birthday.lean'>birthday counting<br/>q(q-1)/|𝔽|,<br/>no assumption</a>"| ROM
  NFC -->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Nullifier.lean'>distinct-note openings<br/>compute</a>"| SDLR
  SAF ---> RDSA["RedDSA unforgeability,<br/>±-randomized keys"]
  RDSA RDSAtoDL@==>|"re-rand reduction<br/><a target='_blank' href='https://eprint.iacr.org/2015/395'>[FKMSSS2016]</a> +<br/><a target='_blank' href='https://eprint.iacr.org/2019/877'>straight-line AGM extraction</a>"| DL
  RDSA -->|"challenge hash<br/>as random oracle"| ROM

  click BAL "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Balance.lean" _blank
  click SPEND "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Spendability.lean" _blank
  click SPENDAUTH "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/SpendAuthority.lean" _blank
  click BS "https://github.com/zcash/ironwood/blob/main/Zcash/Security/BindingSignature/Balance.lean" _blank
  click NCB "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Statement.lean" _blank
  click MERK "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Merkle.lean" _blank
  click KB "https://github.com/zcash/ironwood/blob/main/Zcash/Security/KeyBinding/Basic.lean" _blank
  click NFB "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Spendability.lean" _blank
  click STMT "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Statement.lean" _blank
  click NCBK "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Statement.lean" _blank
  click MC "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Merkle.lean" _blank
  click CUS "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Common/RandomOracle.lean" _blank
  click NFC "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Spendability.lean" _blank
  click SAF "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/SpendAuthority.lean" _blank
  click NDLR "https://github.com/zcash/ironwood/blob/main/Zcash/Common/DiscreteLogRelation.lean" _blank
  click SDLR "https://github.com/zcash/ironwood/blob/main/Zcash/Common/DiscreteLogRelation.lean" _blank
  click KS "https://github.com/zcash/ironwood/blob/main/Zcash/Snark/Soundness/Relation/KnowledgeSoundness.lean" _blank
  click DL "https://github.com/zcash/ironwood/blob/main/Zcash/Common/DiscreteLogRelation.lean" _blank
  click ROM "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Common/RandomOracle.lean" _blank
  click KERR "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/ExtractionKappaArm.lean" _blank
  click RDSA "https://github.com/zcash/ironwood/issues/121" _blank

  classDef proven fill:#1a7f37,stroke:#116329,color:#ffffff
  classDef checked fill:#0969da,stroke:#0550ae,color:#ffffff
  classDef partial fill:#9a6700,stroke:#7d4e00,color:#ffffff
  classDef hyp fill:#cf222e,stroke:#a40e26,color:#ffffff
  classDef assumed fill:#57606a,stroke:#424a53,color:#ffffff
  class BAL,SPEND,SPENDAUTH,KS partial
  class NCB,BS,KB,MERK,NFB,STMT,NDLR,CUS,NCBK,MC,NFC,SAF,SDLR,KERR checked
  class RDSA hyp
  class DL,ROM assumed
  classDef agmEdge stroke:#8858c8,stroke-width:4.2px
  classDef agmBridge stroke:#8858c8,stroke-width:3.5px,stroke-dasharray: 7.5 3.2
  class KERRtoNDLR,KStoDL,RDSAtoDL agmEdge
  class STMTtoKS agmBridge

➞ heavy purple edge: a reduction (or intended reduction) in the online-AGM — both endpoint games are algebraic
⇢ dashed purple edge: an AGM-scoped justification crossing named side conditions — a semantic bridge rather than a proved implication
➝ thin edge: depends on (a reduction, assumption, or model)
 ■  fully proven — nothing here yet
 ■  stated and machine-checked in Lean, over abstract primitives
 ■  partly machine-checked; remainder tracked (discharging the capstones' named ε's end to end: composing the per-arm oracle-model discharges into one experiment, RedDSA unforgeability; knowledge soundness's circuit-correctness conditions)
 ■  named hypothesis; formalization deferred
 ■  assumption or heuristic model; terminal by design

This picture is a deliberate approximation, and is likely to change as the formalization proceeds. The RedDSA node is a named hypothesis rather than a terminal assumption: its discharge edge names the reduction for security of signatures with re-randomizable keys (Efficient Unlinkable Sanitizable Signatures from Signatures with Re-Randomizable Keys, section 3), adapted to the ±-randomized variant, together with the same straight-line AGM+ROM extraction of Fuchsbauer–Plouviez–Seurin (Blind Schnorr Signatures and Signed ElGamal Encryption in the Algebraic Group Model, Theorem 1) that discharges the binding-signature extractability node at $(q_H+2)/|\mathbb{F}|+{\epsilon }_{\mathrm{DL}}$. The two arms differ in the signing oracle: the binding-signature extraction has none to simulate, because the signature extracted from is the adversary's own, while the RedDSA unforgeability game has one. The planned discharge is to simulate the signing oracle by programming the challenge oracle at the re-randomized key; the randomizer, carried by the forgery, enters the extraction as a known coefficient.

Every solid arrow reads "rests on"; where an edge carries a label, the label names the computed break object flowing along it, or the side condition under which the reduction holds (base independence from hash-to-curve, the birthday count). Heavy purple arrows mark reductions (or intended reductions) stated for algebraic adversaries: both the source and the target of such an edge are interpreted as games against online-AGM adversaries, so the model scopes the whole reduction rather than being one more assumption it rests on — see Security Models. The random-oracle node remains a terminal because some error terms genuinely bottom out there: they are counting arguments over the oracle table, with no computational assumption. The games are the top-level capstones. The ledger model requires the adversary to supply, along with any accepting proof, a witness or replay evidence for the Action statement (ActionSatisfied) — in the replay case the ledger oracle can produce the previously supplied witness. Each component argument consumes the statement's satisfaction on that witness. Knowledge soundness is what justifies the modelling: whenever the ledger layer needs a witness, the extractor computes one —or computes break data— from the accepting proof. The justification is AGM-scoped —the extractor consumes the adversary's representations— so its edge is heavy purple; the dashing marks that it crosses the remaining semantic bridge: the Clean/Ironwood circuit-correctness conditions (TopLevelCircuitCorrectness) — named component conditions rather than a proved implication. Discharging them is the subject of the circuit soundness proof.

New to the shorthand? See the Definitions.  ·  For the methodology, Security Models.  ·  For the verifier-soundness half, the Proof Map.

Definitions

Coined terms and shorthand used across the proof map, the ledger security games, and the Lean development. Anchors point to definitions under Zcash/, linked to their source files.

Source Map

A directory-by-directory index of the Lean development under Zcash/: what each subtree contains and where to start reading. It is the source-tree companion to the proof map (which traces how the results connect), the ledger security games (which state the properties being proven), the security models page (which describes the methodology), and the definitions page (which defines the coined terms).

The development has four tiers. Zcash/Arithmetic/ holds the objects the other three are stated over — the scalar field, the verifier group and its reference string, the fingerprint multiscalar multiplication, and the transform machinery and fast kernels behind them. Zcash/Snark/ is verifier soundness for the deployed Halo 2 verifier — an accepting proof is bound to a witness satisfying the circuit, or else an explicit break of a hardness assumption is computed. Zcash/Circuits/ is the circuit layer — a port of the Orchard Action circuit onto Clean's Halo 2 formalization, saying what satisfying that circuit means in protocol terms, with Integration/ carrying the Clean-to-Ironwood boundary. Zcash/Security/ is the protocol security-property layer — the binding-signature balance, key-binding, and ledger-model games built on top. A small set of shared leaves (Zcash/Common/, Zcash/Meta/) and a library-wide trust census (Zcash/TrustBoundary.lean) support all four.

Each .lean file carries a module docstring with the details; this page stays at the directory level, naming the notable modules as entry points.

Top level — Zcash/

• Common/ — shared leaves that two tiers need and neither should import the other for. DiscreteLogRelation carries a nontrivial F-linear (discrete-log) relation among a family of generators as computed data — the coefficients — so the reduction-style security arguments can produce a break rather than merely assert one exists (see breaks as computed data on the Formal Verification page). AlgebraicRelation carries the same relation over an arbitrary indexed basis (AlgebraicRelationWitness) and turns one into a discrete log, either against known slot logs or against a basis programmed from the DL challenge (Jaeger–Tessaro, Expected-Time Cryptography: Generic Techniques and Applications to Concrete Soundness, Lemma 3); RelationProbability and RelationProbabilityCoins price that reduction's single miss hyperplane at 1/|F|, and UniformMeasure holds the distribution facts they count with. None of these restrict the adversary — they consume relation coefficients from any source, and what scopes them is how the basis is sampled — so they sit here rather than under Snark/Soundness/AGM/. Expr is the gate-polynomial AST exactly as halo2 evaluates it, produced by the circuit-side VK-match projection and consumed by the verifier stack. RelationWitness supplies the combinators for sequencing a computed break branch: a conclusion A ⊕' R cannot be case-split classically, so composing such reductions — and commuting a family of them past ∀ — needs explicit searches rather than by_cases. ParMap is List.map on the task runtime, proven equal to List.map definitionally.
• Meta/ — build-time metaprogramming. AxiomCheck provides assert_axioms, a sibling of Mathlib's assert_no_sorry that asserts an upper bound on a declaration's trusted base without hard-coding the pretty-printed axiom list, so the trust pins stay green across toolchain bumps that rename the native_decide axiom, and assert_computable, which additionally requires the declaration to be a plain def. EndpointCensus enforces the endpoint census a second time from the elaborated environment: both census commands record every pin they elaborate, and assert_endpoint_census — run by Zcash/CensusCheck.lean, the CensusCheck target, whose imports span every census file — fails the build on an endpoint-named declaration with no recorded pin, closing the surface-syntax evasions a source-text scan cannot see.
• Arithmetic.lean — the tier's root module, and the only place in the repository that earns root vocabulary: Fp and URS are re-exported at Zcash so every module finds them by the enclosing-namespace walk.
• TrustBoundary.lean — the library-wide census that makes the trust claims build-time checks rather than prose: a change that widens any checked declaration's trusted base — a reachable sorry, an unexpected axiom, or native_decide where none was permitted — fails the build here. Computed break reductions are pinned with assert_computable, theorems with assert_axioms. The SNARK-side censuses were consolidated into this one file, so apart from the two per-capture fixture boundaries below it is the single place the trust claims are pinned.

Arithmetic — Zcash/Arithmetic/

The objects every other tier is stated over, and the evaluation lanes that make the concrete computations affordable. Most of these names stay qualified; a module that wants one opens Zcash.Arithmetic for exactly that name.

Field fixes the scalar field F_p (Vesta's scalar = Pallas base) and its cardinality, which appears in every Schwartz–Zippel bound; Group fixes the verifier group E_q (Vesta) and the uniform reference string as an F-module, with the concrete instantiation unconditional — CompElliptic's Vesta curve is a proven AddCommGroup and its order is pinned with no assumption — and VestaModule supplies that module instance as a plain def. Msm is the fingerprint multiscalar multiplication the verifier collapses its whole check into, mirroring halo2's MSM<C>, and FastMsm gives it a windowed Pippenger evaluation path registered with @[csimp], so the fixtures' native_decide auxiliaries run fast while the statement surface is untouched.

The transform stack is what the verifying-key derivation is built from: Domain (halo2's domain scalars — omegaOf, DELTA, the primitive-root facts, bridged to CompElliptic's certified Pasta root), Fft (bestFftG, halo2's best_fft over an arbitrary Fp-module, so the scalar and group instances share one definition), FftSpec (its full DFT specification, bestFftG_dft), InvDft and ScalarInvDft, LagrangeBasis (the closed coefficient form ℓ_i = n⁻¹ · Σ_t ω^{-i·t} Xᵗ), and CommitLagrange (the per-column committer, which inverse-DFTs the coefficients as scalars and commits against the monomial basis, so no group FFT is ever evaluated). NatKernel and NatKernelEquiv are the dictionary-free evaluation lane underneath — projective Vesta points as canonical-ℕ triples dispatching to GMP under the interpreter, proven equal to the statement-surface functions.

Verifier soundness — Zcash/Snark/

Core/ — the verifier's proof-side objects

ProofString is the proof as opaque field and group elements after canonical decoding; Challenges records the verifier's challenges in squeeze order (θ, β, γ, y, x, the multiopen x₁…x₄, and the IPA ξ, z and round challenges uⱼ). The field, group, and MSM these are read against live in Zcash/Arithmetic/; Core.lean is a one-line compatibility shim re-exporting Msm at Zcash.Snark for the generated captures, to be deleted when they are next regenerated.

Verifier/ — the MSM assembly

The pure function that assembles the fingerprint MSM in the exact order of halo2's plonk/verifier.rs — the Lean image of the interactive verifier.

• Assemble and Checks compose the building blocks.
• Queries builds the per-argument opening queries; QueryCommitment resolves each assembled query back to the canonical group element it references.
• Expressions recomputes the vanishing argument's expected_h_eval.
• Ipa is the inner-product-argument opening (compute_s / compute_b).
• FiatShamir models halo2's Blake2b challenge schedule as an abstract squeeze.
• AssembleSpec says what the rejecting assemble? returns when it does not reject — exactly the total assembly's value — the operational interface both the fingerprint walk and the deployed soundness layer consume.
• OrchardShape specializes the verifier shape to the captured Orchard column and query dimensions while leaving the action count free; every consensus-valid action count instantiates it.
• Parametric proves the assembly and schedule traverse every sub-proof for an arbitrary proof count; every consensus-valid Orchard action count is one such count. At zero, this describes the transaction-level absence of an Orchard bundle, not a verifier call with an empty bundle. Actual Action-verifier invocations have a positive proof count and the deployed domain exponent k = 11. The generic Lean functions remain total at k = 0, while halo2's IPA implementation requires a nonempty challenge vector, so behavioral correspondence is scoped to the deployed positive domain.

Keygen/ — the verifying key, derived rather than assumed

The circuit-side half of halo2's keygen_vk. Pipeline is the single generic route from a closed TopLevelCircuit and a monomial URS to a full VerifyingKey: Clean's Halo2.Keygen supplies the pinned constraint system, domain exponent and selector map, and this module adds the group side. Derivation instantiates it at the closed Orchard Action circuit — every definition there is a TopLevelCircuit method applied to actionCircuit — and is what ordinary clients consume. Lagrange relates the two directions of the Lagrange basis: the verifier-side commitment keys are built from the closed coefficient rows, and conversely the derived basis's i-th entry is the monomial commitment to that same closed row. Certificate holds the one slow check — a single bundled native_decide comparing every field of the derived key against the capture, which dominates the elaboration time of the lane — and so is built only in the fixture lane. InstanceCapture joins the fixture's captured instance commitments to the circuit-derived family the deployed capstone consumes: the Lagrange commitment key is identified with the certified monomial derivation, and the captured public-input column is read back as the circuit's own PublicInputs record.

Fingerprint/ — the cross-check and its soundness

Match is the fingerprint match: running the deployed Rust verifier and the Lean assemble on the same proof and challenges and comparing the assembled MSMs coefficient-for-coefficient — the cross-check that validates the Lean assembly in place of a line-by-line translation proof; the per-family Boundary modules under Fixtures/ restate it at the Lean-derived key and schedule as the statements of record. SchwartzZippel supplies the abstract random-evaluation bound: a fingerprint agrees with a random evaluation only with negligible probability. Outer batching of separate proof blobs by Halo2's optional BatchVerifier is outside this formalization's scope.

SampleSpace encodes the proof-string scalars and challenges as one product sample space (ScalarSlot, with the deployed read schedule's lastEval shape baked into the type). Rational/ instantiates the Schwartz–Zippel bound at assemble's own coefficients — the quantified random match. GoodEvent enumerates the challenge-only denominator factors whose joint nonvanishing is the good event; Representation is the representation toolkit (cleared num/den identities on the event, with challenge folds costing one degree unit per element); Family holds RationalCoeffFamily, the object the walk constructs and the ε theorem consumes. ConstraintWalk, GroupingTable (with Verifier/GroupingRef), OpeningWalk, IpaWalk, OtherCoefficients, and Capstone walk the whole assembly — grouping stability through a fixed reference table, the opening value, the IPA scalars, and the positional other coefficient stream — into assembleCoeffFamily: every MSM coefficient as a polynomial numerator over enumerated denominators with one degree budget. Epsilon then prices the match. For bounded-degree polynomial numerators over the walk's enumerated challenge denominators, a family that differs from Lean's agrees at a uniform point with probability at most (D + B)/p. The random fixtures state the concrete ε values; Fingerprint/Match.lean lists the premisses, including class membership and sample uniformity.

Fixtures/ — captured proofs and boundary checks

Concrete Orchard captures that exercise the assembly end-to-end and make the Rust/Lean boundary less silent. This subtree is the FixtureCheck lake target, kept out of lake build Zcash (the captures are large, generated, and slow) but built by CI. Shared/ScheduleMarker re-encodes captured Fiat–Shamir schedules into the model's marker form; Shared/TamperSweep is the shared mutation vocabulary of the per-slot negative sweeps; PostNu63 pins the canonical post-NU 6.3 verifying key and URS so fixture drift is visible here, and PostNu63Random extends the same point equalities to the random captures — kept separate so the honest lane does not depend on compiling the random data modules. (The join between the captured instance commitments and the circuit-derived family lives in Keygen/InstanceCapture.)

SingleAction/Honest/ and MultiAction/Honest/ hold the captured honest single- and multi-action proofs, each with its Fiat–Shamir schedule check, its Boundary statement of record at the Lean-derived key and schedule, its per-slot tamper sweep (Negative/Sweep), and its checked TrustBoundary turning the fingerprint match into build-time obligations; SingleAction/Honest/VkMatch computes the capture's constraint-system fields equal to the ones derived end to end from the ported configure. The multi-action capture additionally carries the shape/VK faithfulness checks, the adversarial negative fixtures, the degree, schedule and static-check modules, the adaptive-statement knowledge-failure endpoints — its 2^123 work-factor instantiation and the conditionally staged-certified 2^123 and 2^125 adversary-work ones — data-coupled programmed-basis and verifier-commitment accounting, explicit adversary and complete-program staging-fidelity obligations, mechanically composed reduction work, a direct-decode bound derived from a required family invariant, and a separate oracle-query budget, and CapturedZeroFamily — the shape-generic zero prover instantiated at the captured key's own scalar data, so the staged IPA trace carries eleven live rounds.

Each family's Random/ subfolder holds the random match-only captures — the deployed verifier run on random proof strings, deliberately non-accepting. Each has the same schedule checks and Faithfulness, a VkCertificate transporting the single-action keygen certificate along PostNu63Random's point equalities, its Boundary statement of record, aliveness guards in Negative (the model assembles at the random point, the capture is genuinely non-accepting, and one tamper canary), and its own TrustBoundary census. What the four families jointly check is that Lean's assembled MSM equals the deployed one coefficient-for-coefficient at each captured proof; the two Random/ families additionally carry the per-capture ε modules that price the quantified match (Fingerprint/Epsilon.lean, Fixtures/*/Random/Epsilon.lean). Capture lineage and seeds live in Fixtures/PROVENANCE.md, and Fixtures/MANIFEST.tsv binds each committed capture to its digest, generator, and invocation — scripts/check_fixture_manifest.sh verifies the binding on every CI run and rejects any generated-looking artifact without an entry.

Soundness/ — the soundness argument

The core argument that an accepting proof yields a witness or a computed break. The top-level modules cover the argument end to end: Main (the deployed-acceptance predicate and explicit verifier-equation correspondence), KnowledgeSoundness (the SnarkRelation knowledge-soundness relation), Constraints (Schwartz–Zippel soundness of the vanishing check) with FoldSplit (recovering the individual constraints from the verifier's y-fold), ConstraintCore and ConstraintRouting (the rewind-free deterministic identities the algebraic decoder consumes), ConstraintRelations (the row-level results the capstone's satisfaction predicate yields — the permutation argument's copy constraints and the lookup argument's inclusion), DegreeWalk (an explicit degree bound D for the combined constraint difference, hence εx = D / |𝔽|), and GoodChallenge/ChallengePricing (deriving the good-challenge exclusions from challenge uniformity rather than assuming them). The permutation/lookup stack is GrandProduct — the shared grand-product-to-multiset kernel — with RunningProduct (telescoping the running product), GrandProductBridge (the two Schwartz–Zippel steps from the verifier's evaluated check to the multiset identity), Permutation, PermutationConstruction, PermutationRows, Lookup, and LookupAssembly. The IPA algebra is InnerProduct, Halves, IpaSoundness, Consistency, and CommitFold; the executable extraction route itself lives in AGM/StraightLineIpa. InstanceBinding closes the public-instance gap: a decoded instance column is the polynomial halo2 committed from its instances argument, or a (g, U, W) relation is computed. ZeroData supplies the zero-data multiopen keystone the constant prover families are built on. Vesta pins the abstract group to the actual Vesta curve. TopLevelTerminal connects canonical constraint satisfaction to the Spec of an arbitrary top-level circuit using that circuit's derived verifier key and public inputs. Action/StraightLineTerminal and Action/StraightLineEvent connect the one-run computed decode to the concrete Action statement and carry a failure as explicit relation data. Action/AdaptiveStatement* is the adaptive-statement stack, the strongest Action notion: one online-AGM adversary returns the public inputs and proof together. DeploymentRecord states the machine-readable deployment-instantiation record — one identification field per model floor (challenge law, basis law, key digest, typed acceptance, discrete-log advantage) — that a deployed interpretation of the capstones supplies. AdaptiveStatementModel defines the game and binds the verifying key and selected instance commitments before theta; Accounting, Terminal, and Surfaces decode arbitrary statement prefixes and price the root, IPA, and semantic surfaces under the single (Q + 1) query factor; Provenance, Semantic, and Complete identify the selected statement's decoded polynomials with the executable resolver stages; Event unions the priced events and Capstone discharges the statistical residual against them; Knowledge ends at the executable knowledge extractor and its failure bound; Cached proves that one retained execution gives the same finder and extraction event; and Cost constructs the programmed basis through reified Vesta operations, feeds those computed points into the adversary, threads reified canonical commitments into verifier assembly, and derives the conditional staged 2× group-operation bound. Its private composition carries one closed program that constructs the charged basis, specializes the exact adversary path with its annotations and group nodes, constructs a proof-carrying cache from that result, and consumes that same cache in reified postprocessing. Lean proves the resulting counter equals adversary work plus reduction work. Since the cost language is shallow, fidelity of the supplied adversary and of generic host callbacks inside the complete program remains external and is stated separately. The modeled three-decode inequality is derived from the family's required fixed-representation cap rather than retained as a free certified-profile number; this generic development does not construct the concrete deployment family that must satisfy the cap. Profile retains the older declared-resource compatibility theorem. The shared AdaptiveSurfaces and AdaptiveTerminal supply the per-commitment activity predicates, challenge surfaces, and pointwise semantic terminal both Action routes consume.

Six subtrees carry the heavier machinery:

• AGM/ — the algebraic-group-model layer: what it adds is the restriction on the prover, namely that it emits a representation alongside every group element (Fuchsbauer–Kiltz–Loss, The Algebraic Group Model and its Applications). The relation-to-discrete-log machinery itself is model-free and lives in Common/AlgebraicRelation; Adapter supplies only the view of the deployed URS as an augmented basis (g, U, W). This subtree adds the algebraic coefficients to the online prover interfaces (OnlineMembers, OnlineMultiopen), reifies erasable group-work events for adaptive programs (CostedOracle), and evaluates the reduction's probability loss at Vesta (ProbabilityVesta) — programming every basis slot from the DL challenge rather than guessing which slot the relation will hit, so the loss is an additive 1/|F| with no multiplicative factor. The bulk of the subtree is the rewind-free deployed decoder, consisting of the unbatching chain (AlgebraicUnbatch, DeployedX1, DeployedMultiopen, ValueUnbatch, DeployedValueUnbatch, ShiftRecovery), the direct coordinate decode (DirectX4Columns, DirectConstraintFamily), the explicit root sets it must avoid (DeployedRootSets, DeployedRootDecode, DeployedPinnedRoots, PinnedRootWitness), the retained-provenance route (OnlineMembers, OnlineMultiopen, OnlineConstraint, DeployedConstraintSupply), and the adapters back onto the opened-batch interfaces (SyntheticOpened, DeployedSyntheticOpened, DecodeToOpened). StraightLineIpa and StraightLinePinnedRoots classify one accepting algebraic transcript as a clean opening, an explicit relation, or a squeeze-pinned bad-challenge event, from a single execution with no rewinding; AdaptiveOnline, AdaptiveRootCore, AdaptiveDecode, AdaptiveIpaSurfaces, and the AdaptiveStatement* modules extend the same rewind-free machinery to adversaries that choose their statement online, decoding accepting prefixes and pricing the per-round IPA surfaces; StraightLineFiniteSecurity records group work, random-oracle queries and direct-decode field work as distinct quantities and asserts no generic-group DLOG formula. ZeroFamily and ZeroFamilyRoots are the constant zero-data prover at an arbitrary shape, whose multiopen obligation reduces to 0 = 0.
• Canonical/ — the verifier-native constraint model the circuit layer is handed. It installs the fixed selector triple into the commitment-ID resolver (ConstraintModel, DomainSelectors), recovers the three constraint families from the flat y-folded list (ConstraintSatisfaction), interpolates rows on the ω domain (PolynomialEnvironment), joins halo2's Lagrange-basis instance commitments to the extractor's monomial coefficient vectors (InstanceCommitment), and instantiates the permutation and lookup arguments at routed decoded polynomials (PermutationInstantiation, PermutationSemantics, LookupInstantiation, LookupSemantics, LookupRows), ending at Terminal.
• Composition/ — joining the two halves the architecture keeps apart and bounding the probability loss the join costs. Bridge identifies the algebraic extraction's aggregate witness with the deployed decoded terminal's opened commitment. DeployedAcceptance and DeployedRuntime name the deployed decision on one oracle table; DeployedRootContainment and DeployedConstraintContainment replace the four-level joint-event coupling with a finite union of explicit bad-root events, each fixed before its own squeeze, so the residual is additive and has no fourth root. Quotient reconstructs a genuinely pre-x quotient, PrefixedSqueeze and ScheduleBudget bound the probability loss at the x squeeze, and ActionBudget and AlgebraicRootBudget cap the action-dependent counts at the consensus maximum, with OrchardConsensusBounds (and its straight-line sibling under AGM/) evaluating the composite bounds at the captured Orchard shape up to that maximum. The straight-line route is StraightLineDeployed (the primary deployed path), StraightLineConstraint, StraightLineDecodeSupply, and the two inhabitants of its interface — StraightLineWitness at the degenerate shape and ZeroStraightLine with eleven live IPA rounds. ZeroBasisAcceptance proves the computation-free steps toward an accepting run of the adaptive knowledge machinery: representations and algebraic points vanish at the all-zero basis, MSM evaluation reduces to its base terms, and assembly success plus vanishing bases give DeployedAccepts; assembly success at a guard-passing oracle and the base-provenance walk remain open. SemanticChallengeRemainder bounds the probability loss from the bundle-wide y/β/γ/θ exclusions the Action-level statement needs, and DirectPathCost bounds the direct-coordinate postprocessing's field operations and data traversal by a shape polynomial with no |F| term.
• Deployed/ — algebra for halo2's actual deployed IPA. Fold rewrites the flattened verifier MSM's generator term into the closed-form fold consumed by the straight-line extractor; Verification exposes halo2's explicit IPA verifier equation; and Binding supplies the augmented-generator collision reductions shared by the computed AGM path.
• FiatShamir/ — the reusable Fiat–Shamir random-oracle kernel: random-oracle primitives (Oracle), the deployed squeeze ordering (Ordering), random-oracle execution and IPA-field splicing (Execution), closed-form IPA assembly algebra (Assembly), the one-level pinned-squeeze bound and the additive union of pinned root events (PinnedSqueeze, PinnedRoots), and the wrapper that returns a run's own oracle reads with its output (WithReads). FiatShamir/Adversary/ builds the querying-adversary reduction on top: the Q-query adaptive adversary model (OracleComp), the Fiat–Shamir-to-AGM handoff (Algebraic), oracle-domain reduction to finite support (DomainReduction), and the adaptive interface and pre-IPA query accounting (Adaptive, PreIpa, Provenance). These components use the bounded querying-adversary model to price straight-line pinned-root events.
• Oracle/ — the squeeze idealization and its deployed gap. Model models squeezes as a reprogrammable random function with the exactly uniform challenge law and the PMFEventBiasLE transport interface; Challenge255 prices the deployed conversion against that ideal — a uniform 512-bit digest reduced modulo p overshoots uniform by exactly r(p−r)/(p·2^512) < 2^-260, stated as the PMFEventBiasLE premise the work-factor capstone's bias conjunct consumes, with Blake2b's idealization as the uniform digest remaining external.
• Multiopen/ — the multiopen argument's value binding. Decode supplies the coefficient and Vandermonde primitives; Opened defines the augmented opened-batch and member-decode interfaces populated by explicit AGM representations; and Deployed proves that halo2's x₄ fold has the required flat power-batch shape. Compat is the MSM evaluation spine; RPoly supplies the interpolation core (Mathlib's Lagrange.interpolate, plus the bridge to the deployed foldl); ValueCheck, ValueCheckDeployed, and NodeBinding provide the deployed algebra consumed by the AGM unbatching chain; and ConstraintResolver, CanonicalSelection and CanonicalRelation route the decoded members into the canonical constraint model, which is the semantic handoff to the formal circuit.

Capstones/ — the advertised endpoints

Where the deployed Action circuit's own statements are stated. ActionEvents carries the shape identification the rest of the chain is stated over, ActionChecks carries the captured key's scalars and static checks, ActionBudgets discharges the semantic surfaces, and Action states the endpoints — knowledge-soundness bounds for every consensus-valid bundle size, in compositional error-formula form, in resource-accounted finite-security form at the 2^123 work factor, and in the staged-certified forms carrying their group-work accounting at 2^123 and 2^125 adversary work. Knowledge soundness is the only property advertised: it implies the plain-soundness statement, so that is not stated separately. Legacy fixed-statement endpoints and their events are retired.

Endpoints about the verifier's algebra rather than the circuit statement live with the layer that proves them: the captured straight-line knowledge errors in Fixtures/MultiAction/Honest/StraightLineKnowledgeError, and the consensus-maximum work factors in Soundness/AGM/StraightLineOrchardConsensusBounds. Every endpoint, wherever it sits, is a top-level leaf that nothing else depends on, which is why each must be named directly in a TrustBoundary.lean census entry — see scripts/check_endpoint_census.sh, enforced a second time from the elaborated environment by the CensusCheck target (Zcash/Meta/EndpointCensus.lean).

Circuit layer — Zcash/Circuits/

A port of the Orchard Action circuit onto Clean's Halo 2 formalization, with elliptic-curve arithmetic from CompElliptic. Each chip is ported from the actual Rust (orchard@0.14.0, halo2_gadgets-0.5.0) rather than from memory, and the module docstrings cite the source lines. Where the Sinsemilla incomplete-addition escapes can fire, the statements carry them as data (SpecOrBreak) rather than assuming them away.

• Specs/ — the value-level protocol specifications the circuits are proven against: Orchard data shapes (Types), the Pallas curve and its certified arithmetic (Pallas, PallasCert, CompEllipticExtras), bit-range arithmetic (Bitrange), and the Sinsemilla hash with its generators and break structure (Sinsemilla, SinsemillaGenerators, SinsemillaBreak).
• Utilities/ — the shared gadgets: LookupRangeCheck (the first lookup-consuming gadget ported, generic over K), RunningSum/DecomposeRunningSum, CondSwap, and AddChip.
• Ecc/ — the ECC chip. Point witnessing (WitnessPoint), complete and incomplete addition (Add, AddIncomplete), variable-base multiplication in its incomplete/complete/overflow phases (Mul, MulIncomplete, MulIncompleteRound, MulComplete, MulOverflow, DoubleAndAdd), and fixed-base multiplication (MulFixed/, with full-width, short, and base-field-element variants). MulFixed/Certs/ holds the six deployed fixed bases with their window-table certificates, checked through CertCheck's ℕ-literal evaluator.
• Sinsemilla/ — the Sinsemilla chip: the 2^K generator table (Basic), one hash piece and its rounds (HashPiece, HashPieceRound), the ⊥-propagating chain (Chain, HashToPoint), the commit domain (CommitDomain), and the fixed-depth Merkle path (Merkle).
• Poseidon/ — the Poseidon chip: the pow5 S-box and round structure (Pow5, Rounds, Constants), the permutation (Permute), and the sponge/hash at ConstantLength<2> (Hash).
• NoteCommit/ and CommitIvk/ — the two commitment circuits, each as pieces and decompositions, the gate set, the canonicity checks, and the assembled Main/MainBundle contract at the extracted window scalar.
• Action/ — the top-level Orchard Action circuit. Circuit is the ironwood configure and synthesize in exact region-creation order; CircuitPreIronwood is the post-NU 6.2 circuit without the cross-address region (both share configure); RealBases instantiates everything at the actual deployed constants; PublicInput declares the public instance-cell layout and splits the semantic witness into public and private halves; SelectorCoherence certifies that every selector reference the configure program registers was allocated by that same program; the per-check modules are ValueCommit, DeriveNullifier, SpendAuthority, and AddressIntegrity; Bundle is the end-to-end statement against protocol spec §4.17.4; and TopLevel presents the whole thing as a closed TopLevelCircuit.
• Integration/ — the Clean-to-Ironwood boundary, and the largest directory in the tree. Only modules that translate belong here; pure verifier-native constraint, permutation and lookup mathematics stays in Zcash/Snark/. It compiles the circuit's declared structure into what the verifier's soundness model quantifies over: gates and lookups from the operation stream (OperationGates, OperationLookups, OperationFixed, OperationCopies), the permutation round trip (PermutationCompiler, PermutationReplay, CopyListMembership), the layout and selector compilers (FixedLayout, SelectorCoherence, LookupSelectorRows, QueryLayouts), the commitment provenance of the fixed, σ and instance columns (FixedColumns, PermutationColumns, InstanceColumns), the resolver-backed environments (ResolverGates, ResolverQueryEnvironment, PolynomialEnvironment, ExprRich), and the reassembly of full circuit satisfaction (CircuitSatisfaction, CircuitIntegration). The Action* modules specialize all of that to the deployed Action circuit and land at ActionTerminal; the TopLevel* modules are the circuit-generic versions. StraightLineActionTerminal reaches that same terminal from one accepting execution instead of a rewinding one, and StraightLineActionEvent bounds the probability loss from the challenge exclusions it leaves open — the probability that an accepting run carries neither the bundle statement nor a nontrivial relation.
• Fixtures/ and Tests/ — the VK cross-check against Rust. Fixtures/ reconstructs, purely and computably, the layout products a keygen-view dump pins (the ordered copy list, the permutation σ, the fixed assignments) from a circuit's Operations, with the dumps carried as JSON data files (Json) and their SHA-256 pins as Lean data (Stamp, generated, the module that carries a fixture change into Lake's import graph); Tests/ checks that the ported configure is equal to those dumps' post-compress_selectors, and is the CircuitCheck lake target — like FixtureCheck, kept out of lake build Zcash but compiled by CI, with the glob covering the whole directory so a newly added test cannot land in no target at all.

Protocol security — Zcash/Security/

The security-property games layered on the verifier, all in the reduction style: a property violation exhibits a concrete break (a hash collision or a discrete-log relation), carried as computed data.

• Common/ — the classical random-oracle foundation shared by the games. RandomOracle is the collision vocabulary (the Collision / CollisionUpToSign structures); Birthday is the birthday-bound counting for random-oracle ±-collisions, in the counting-fraction style used throughout (no probability monad).
• Concrete/ — PallasGroup, the Pallas group behind a small protocol-facing wrapper over CompElliptic's affine SWPoint, carrying the transported group laws and the scalar-module structure the deployed pool's primitives are stated over.
• BindingSignature/ — the binding-signature balance argument (spec §4.13 Sapling / §4.14 Orchard). Balance is the shared algebraic core over an arbitrary F-module; Orchard and Sapling add the per-pool no-overflow bounds that keep the value sums below the scalar-field order. DiscreteLog carries the computed relation the rest of the way, to the discrete log of Vbase base Rbase: if you can unbalance, you can solve DL. It is scoped by the sampling of the two bases, not by any restriction on the adversary, which is why it sits here rather than under Snark/Soundness/AGM/.
• KeyBinding/ — the key-binding theorem (ZIP 2005, ROM). Basic is the deterministic layer: a verifying Recovery-Statement witness pins the key components (ak up to y-sign, nk, and the qk/sk branch) to ivk unless an explicit break is computed. Instance bridges that concrete development to the games' KeyBindingInterface, Pool states it at the Orchard Action, and Probability adds the whole-table random-oracle model that turns the counting facts into a probability bound.
• Ledger/ — the ledger-model games. Statement transcribes the games-relevant conjuncts of an Orchard-shaped Action statement over abstract primitives — the interface the games consume — and Model is the witness-annotated ledger they quantify over, with Effects reading off the outputs, spends, and shielded-pool balance. Bridge is deliberately the only place that translates an extracted Action circuit witness into that statement, and the only place Sinsemilla escapes become break statements, with BridgeTests guarding the protocol distinctions a type-correct refinement can silently erase and SinsemillaDLR carrying a classified escape onward as a relation. The games themselves: Balance (every nonzero spend is a committed output of a strictly earlier transaction, or a Merkle/note-commitment break is computed), Spendability (the Faerie-Gold core — nullifiers pin note tuples — plus persistence), and SpendAuthority (an unsigned spend yields a signature forgery or a key-binding break), with Merkle proving fixed-depth Merkle trees position-binding up to an exhibited tree-hash collision and Nullifier reducing a nullifier collision to a discrete-log relation. Pool instantiates the abstract primitives at the deployed pool, Value discharges the transaction-balance premiss against the binding-signature layer, KeyBindingArm discharges the key-binding ε in the oracle model, Capstone lifts the deterministic layer to a distribution over valid annotated ledgers, and Completeness checks the other direction — that an honest wallet's spend actually verifies.