Formalizing Ironwood

$\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 --wfail, 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 --wfail   # verify every proof; --wfail makes warnings fail, as CI does

CI runs the same build plus source-level consistency checks — census coverage, fixture digests, and regeneration diffs — documented in Build and CI Checks.

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.

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

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.

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

The Guide to the Ironwood Formalization is the reader-facing overview of what is proved and what a reader of the theorems is trusting; Security Models develops the adversary models and where hardness judgements live. This page documents two development-wide conventions — how security breaks are represented, and how what the development trusts is checked at build time.

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 the concrete Pasta curves they may inherit CompElliptic's closed native_decide arithmetic facts: the Pallas or Vesta point-count witness and, where Pallas square-root data enters, its Tonelli–Shanks root-of-unity certificate. The reusable census also contains Ironwood's closed NU6.3 cross-address separation check. The +native flag on each build-time check names exactly which owners that endpoint reaches.

@[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 axioms of the named owning declarations, which 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 the default lake targets (scripts/check_build_coverage.sh checks that CI and the lakefile agree on that list, and that every Lean module is reachable from it), 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. The boundaries in what the statements model —the random-oracle treatment of the challenge hash, the algebraic-adversary restriction, the abstract types standing in for byte-level encodings, and the sampled bases standing in for the deployed fixed ones— are neither axioms nor compiler-trust questions, so no census sees them. The Guide's What you are trusting states each of these boundaries and collects the whole set; Security Models develops the adversary models they define and where the hardness judgements live.

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

Guide to the Ironwood Formalization

This page is for anyone deciding what to conclude, and what not to conclude, from this formalization. This section is general; later sections of the page focus on the verifier knowledge-soundness proof.

The place of formalization in security assurance

A protocol formalization such as this one is not a "proof of security". It is a set of claims that constrain the difficulty of various classes of attacks, relative to breaking the cryptographic problems on which the protocol's security was intended to rest. The classes of attacks it rules out are not exhaustive; they are relative to a particular model of what adversaries are able to do.

Sometimes a formalization is presented as something that has to be complete in order to be valuable. This idea might come from the fact that the formal logic in which it is grounded has a "principle of explosion", such that if we make a mistake then it is possible to prove "false". In that case, it would be possible to prove that a protocol is secure when it is not. But this does not take into account how protocol formalization actually works. How it works is that we progressively extend the model to cover ways in which the protocol could be vulnerable. If a flaw lies in a particular piece, and we try to formalize that piece within the framework we've set, then we won't be able to do it, and then we are very likely to find the flaw. This can only really give confidence once the framework is mostly complete —which it is— because we need to know that we are proving the right kinds of thing, that will eventually be composable.

Formalization cannot replace other forms of security assurance: informal security arguments; conservative cryptographic design; detailed and complete specification; incident response processes; careful software engineering practices; unoptimized reference implementations; thorough code reviews; internal and third party audits; automated and manual testing; supply chain integrity checks, etc. On the contrary, it should be interwoven with them, for instance by checking that the formalized objects are consistent with the specification and (where possible) that they match the same test vectors as the production implementation and the unoptimized reference.

So, modelling gaps and the long-term task of closing them, gaining more and more confidence as we go —and then maintaining the formalization in sync with the spec as the protocol evolves— are not a side-issue; that process is the entire point. It is a process that finds bugs just like any other assurance technique, but it is deeply more thorough than conventional auditing or testing. If, as a protocol designer, you're having sleepless nights about a class of potential security problems in a specific part of the protocol, then competently formalizing that part gives you a very meaningful improvement in assurance. And it is feasible to be thorough enough in coverage to approach what we might naively expect from "proven security" more closely than by other methods.

On the flip side, there have been cases where formalization was used as an excuse to skip other forms of assurance, which is positively harmful. See for example Nadim Kobeissi's paper Verification Theatre: False Assurance in Formally Verified Cryptographic Libraries. Even when we don't make the kind of mistakes described in Kobeissi's paper, it's easy to be speaking in good faith and still end up overclaiming — as we have seen a number of times during this formalization effort. It takes substantial labour to educate readers about what they should not conclude from a formalization, and that is as much a matter of good technical writing and teaching as of proof.

In particular, it turns out that AIs are very good at writing a lot of Lean code (and comments) quickly. That is what made this development possible, but it also presents a huge challenge to reining in complexity, verbosity, and overclaims. The path of least resistance is to let the AI produce more output than is humanly reviewable. Using a proof-oriented language like Lean makes this less terrible than it could be, but it is still terrible: not only does it hide the wood for the trees; it introduces some biases in the direction of "it's complicated, but trust us" that we need to actively resist. If this formalization oversimplifies or fails to properly explain something, that's a deficiency and needs to be fixed. We are still in the process of removing a lot of redundancy and rewriting excessively jargon-laden documentation. This page aims to help by focussing attention on the things most important for a human reader to assess.

Scope

There are three foci for this formalization effort: the Action circuit, the Halo 2 SNARK, and the ledger layer (the high-level protocol security properties). Ideally they should fit together. They don't quite do so yet.

Scope at the ledger layer

The formalization of Spendability and Spend authority properties is not yet finished. It needs significant attention to the way honest parties are modelled: the properties need to be strengthened by giving the adversary oracles that allow it to control how the honest parties create transactions, generate keys (without telling the adversary those keys), etc. That is how these properties were originally defined at Zcon3 in Understanding the Security of Zcash.

The formalization of Balance integrity is in better shape (modelling honest parties is not an issue for Balance properties; the adversary merely has to exhibit an unbalanced consensus-valid ledger). All the important pieces have been completed, but they have not yet been connected up. The remaining significant gap is that ledger security arguments are not yet tied into the Action circuit knowledge soundness proof at all: the games state their circuit premiss over their own abstract types, and no definition is currently shared between the two developments (#147 and #155). Additional caveats are stated on the Ledger Security Games page.

For tractability, the modelled ledger also abstracts away from the real protocol in several directions:

• The real protocol has, at the time of writing, six chain value pools: the transparent pool; the lockbox (also transparent), and four shielded pools for Sprout, Sapling, Orchard, and Ironwood. The modelled ledger has one transparent pool, and one Orchard-protocol shielded pool (similar to either Orchard or Ironwood). We argue that this simplification is enough to capture realistic attacks, because the interaction of all other pools with a given shielded pool is as though the other pools are transparent. (It is a bit of an oversimplification for Orchard and Ironwood because they share addresses and key material; we may decide to either model this explicitly or justify more rigorously why that isn't needed.)
• Modelling of the hash-to-curve in the ledger games is not complete. This also particularly affects the formalization of the Spendability and Spend authority properties, because they depend on diversified address generation using $\mathsf{DiversifyHash}$, and so a realistic adversary has to be able to invoke the hash-to-curve. The first step is delivered: the deployed hash-to-curve is proven indifferentiable from a random oracle onto the group, with a concrete advantage bound, modelling the underlying field-element hash as a random oracle — see Group-Hash Indifferentiability. What remains is to give the games' adversaries oracle access to it (#188).

Circuit and SNARK layers

Guide to the Circuit and SNARK Theorems

The verifier knowledge-soundness proof for the Orchard protocol (and therefore the Ironwood pool) can be followed with one idea from cryptography — that a proof system lets someone convince you of a claim without showing you the data behind it. Understanding that idea needs no Lean, no Halo 2, and no background in formal or succinct proof systems. The rest of this page tries to explain the modelling assumptions and heuristics the verifier soundness claim rests on that are not established by a formal theorem, and therefore have to be assessed by other means.

It is not a walkthrough of the proofs. The proof map shows how the results connect, the source map indexes the tree, definitions covers the coined terms, Security Models states the models in full, and the Knowledge-Soundness Contract reads the theorem field by field. From here on, the subject is the Action circuit; for the protocol properties built on top of it, see Ledger Security Games.

The claim

If the deployed verifier accepts a proof, then whoever produced that proof could have handed you the secret data it is a proof about — unless they solved a problem that most cryptographers believe has been infeasibly difficult (although quantum computers could change this in a few years), or hit an event the theorem shows is vanishingly unlikely.

Two phrases are worth pinning down.

The secret data means numbers satisfying the circuit's equations. That satisfying them amounts to a legitimate Orchard action — well-formed note, balanced value, correctly derived nullifier, authorized spend — is itself proven.

The deployed verifier means the verifier as Lean models it: checked against a circuit description Lean derives itself and compares against a captured copy, reading a proof already decoded from bytes into points and numbers. That the captured copy is what Zcash ships, and that the bytes on the wire decode to what the model is handed, are checked outside Lean.

What you need to know first

Circuit and witness. The Action circuit is a large system of equations. The secret data — which note is spent, its value, the key authorizing the spend — assigns numbers to its variables. An assignment making every equation true is a witness.

Commitments. A commitment is a short value pinning down a much longer one: publishing it fixes your choice without revealing it, and opening it means producing the long value and convincing everyone it is what you committed to. Ironwood's commitments are weighted sums of curve points from a fixed public list agreed in advance.

Accepting. Halo 2 lets a witness-holder produce a short proof the verifier checks without seeing the witness. Ironwood runs it over the Vesta curve, and the verifier's work collapses into one arithmetic test: combine the proof, the public inputs, and the circuit description into a single weighted sum of curve points, and check it comes out to zero.

Challenges. Underneath, the protocol is a conversation — the prover sends something, the verifier picks a random number and sends it back, for several rounds. Those numbers are challenges, and they stop a cheating prover preparing everything in advance. The deployed verifier is not interactive, so the conversation is simulated: each challenge is computed by hashing everything sent so far, the Fiat–Shamir transform. The prover can compute them too, but only after fixing the earlier messages they derive from.

Knowing, not merely existing. A weaker claim would say a witness exists. Not enough for a payment system: the statement behind an Orchard action can be true while the person proving it is not entitled to spend — the note is real and somebody holds the key, just not them. So the claim is that this prover holds a witness, made precise by demanding an extractor, a procedure that produces the witness given access to the prover.

It is vanishingly unlikely that the hardness of the problems on which Orchard's security depends could be proven outright. What can be proven is a trade: any prover that cheats can be turned, cheaply and mechanically, into a solver for a problem believed (for now) infeasible. That trade is a reduction, and every theorem here has that shape. Within the algebraic-adversary model that we consider, the assumed-infeasible problem is always the same — given the fixed list of curve points, find multipliers, not all zero, that cancel them to zero: a nontrivial discrete-log relation.

What Lean actually proves

The acceptance test

Lean assembles the weighted sum in the same order Halo 2's Rust verifier does. Acceptance means the assembly succeeds, the structural checks pass, and the sum is zero. A first proof step rewrites that compact test into the explicit equation the rest of the argument consumes.

Classifying one accepting proof

An equation holding says nothing about who knew what. What closes the gap in this formalization is the algebraic-adversary assumption below: the prover must show its work. For every curve point it sends, it must declare a recipe of how to build it from points that it was given. Read against those recipes, the equation forces one of three things.

• The recipes describe a genuine opening — the prover holds data satisfying the circuit, and the argument writes it down.
• The recipes cancel for the wrong reason: the prover found a relation among the fixed points. The argument writes the relation down instead.
• Neither, meaning the challenge fell in the small set of values that can mask a false equation. The bound below covers how often that happens.

Nothing is re-run with different answers: the prover runs once, and the classification reads what that single run declared. That matters, because an extractor's cost is a count of prover runs, and a count growing with the size of the field would be worth nothing in practice. The adversary also picks its own target, producing the public inputs and the proof together; everything identifying that statement is hashed in before the first challenge, so it cannot be chosen after the fact.

What comes out is computed data, not an assertion that something exists — load-bearing, because on this curve a relation always exists, so a theorem merely claiming one existed would say nothing at all (the breaks as computed data convention rules that out). And the witness satisfies the whole constraint system: not just the equations, but the constraints forcing the same value into cells the circuit declares equal, and the table lookups. Equations alone would be close to meaningless, since they do not force the circuit's wiring to be respected.

The probability bound

The two parts above are deterministic. The third branch is not, and it exists because the verifier compresses its work: rather than checking far too many equations one at a time, it checks a single weighted combination, the weights drawn from the challenges. If one equation fails, the combination fails too — unless the weights land in the set that makes the failure cancel. Lean bounds the size of that set, tiny against the field it is drawn from, and charges the adversary for it once per hash query it is allowed.

A second, similar cost pays for reading the combination backwards, since knowing it holds is not knowing that a particular equation holds in a particular row. Recovering those row-level facts draws further challenges, each with its own priced chance of hiding a failure. None is waved through as an assumption.

Together they bound the probability that the verifier accepts while extraction fails, for every bundle size consensus allows. The bound splits in two: a discrete-log term, whose size is the reader's premiss rather than the theorem's, and a statistical leftover the theorem establishes outright. A reviewer judges the first term and simply reads the second.

What you are trusting

A hardness assumption on each curve

Finding a discrete-log relation on each of Pallas and Vesta is infeasible — for each curve, no efficient adversary finds multipliers, not all zero, cancelling the points output by the group hash to zero. This discharges every branch where the argument computes a relation instead of a witness.

Pallas is relied on for security of the application protocol, both inside and outside the Action circuit. Vesta is relied on for knowledge soundness of the SNARK, via the binding property of the verifier's commitments.

In all cases, Lean proves the arithmetic of the cost — how many hash queries and how much group work the reduction spends, each against an explicit ceiling. It falls on readers of these proofs, outside the formalization, to interpret consequences for Zcash's security properties according to their assessment of discrete-log hardness of Pallas and Vesta. The latter is not a binary property; a reader might reasonably come to different conclusions for different timescales based on their assessment of the timeline for quantum computer development, for example.

Three idealizations

These are not hardness assumptions; instead, they swap the real world for a more convenient one. They are choices we took to make this formalization more tractable, with the trade-off that attacks depending on the differences between the real world and the idealized one could be missed.

• The hash behaves like a truly random function — the random-oracle model. This covers BLAKE2b, the conversion of hash output into numbers, and the derivation of the public point list. BLAKE2b is not formalized anywhere: the model treats it as an opaque box and assumes the box is random.
• The attacker is algebraic — assumed to declare, for every curve point it outputs, a recipe building it from points it was given. Real attackers owe no such explanation. This is what lets the reduction read a relation off the adversary's own output. Note where it sits: built into what counts as an adversary at all, rather than appearing as a hypothesis you can read off a theorem. An attacker that does not play along is outside the claim entirely — not covered with a weaker bound.
• Attacks do not depend on specific encodings. The formalization does not cover the concrete, byte-level encodings used to represent curve points, field elements, etc., either in transmitted protocol messages or in the Fiat–Shamir transcript. Instead, the formalization is expressed in terms of the abstract types used in the specification. This is a potentially significant category of gap, because (despite substantial attention to this area in audits and code review) Zcash implementations have had quite a few significant security bugs due to unintentionally non-canonical encodings, mishandling of exceptional cases in decoding, etc. It is a longer-term goal to extend the formalization to cover the byte-level encodings.

The fixed list of curve points

The reduction treats the public list as independent, which is what turns "find a relation among these points" into the discrete-log problem. The deployed protocol does not sample them: it produces the list once by hashing public strings onto the curve and bakes the result in. So security is proved for the family of protocols that sample the list, and the deployed protocol is argued to inherit it — no theorem is ever instantiated at the real points.

The caveat is not the usual asymptotic hand-wave. An adversary has the protocol's entire lifetime to attack one specific list, and the cost is amortized over every transaction ever made against it. One such computation breaks the whole protocol at once, rather than one transaction or one user. Security Models develops this at length.

How Fiat–Shamir is modelled

Lean models the hashing schedule exactly — what gets hashed, in what order, matching Halo 2's verifier. The order is load-bearing and it is checked: each round's message is hashed in before the challenge derived from it is drawn, so a later message cannot bend an earlier challenge, which is what makes it harmless that the prover can compute challenges too. Lean proves this of its own model, and captured fixtures check that model against real transcripts.

The byte layer beneath is not modelled. The sequence of things hashed is verified; how they become bytes, and BLAKE2b itself, are not. Modelling the encoding would narrow the gap without closing it, since the hash would remain outside the proof.

Facts checked by running code, not by the kernel

A few closed numeric facts are established by compiling a program and running it rather than by checking them inside Lean's kernel. Each records an axiom noting the compiler was trusted, and the trust discipline pins every one at build time. Alongside facts about the Vesta curve, the fingerprint match is the one tying the model to the shipped code: it confirms Lean's assembled sum is identical to the Rust verifier's — for the captured proofs in the repository, not for the verifier in general.

The programs those evaluations run are not small. They include the whole fast native arithmetic: field operations, curve group operations, and the multi-scalar multiplication the fingerprint match assembles. The algorithms themselves are proven correct against the group law, inside the kernel, and every proof-carrying replacement of a slow definition by a fast one is checked and censused. What the axiom records as trusted is the compiler's translation of that proven code into the code that actually ran.

These facts are rigorously established; what is not established is that they hold on the kernel alone. Being closed and re-checkable, they fail loudly rather than silently — the curve facts were computed by an entirely different method when the Pasta curves were designed, so a compiler bug would have to arrive at exactly the same wrong answer to slip through.

The whole set, in one place

Everything above, collected.

1. Discrete log is hard for considered adversaries on both Pasta curves — Vesta carries the verifier's knowledge soundness; Pallas carries the Action circuit and the ledger properties built on it. Discrete log hardness is not a binary property; the feasibility of attacks may vary over time and according to the capabilities of an adversary.
2. The hash behaves like a random oracle. BLAKE2b is treated as fresh randomness with no exploitable structure, and is not formalized anywhere.
3. The attacker is algebraic — it shows its work for every curve point it outputs. One that does not is outside the claim rather than covered by it.
4. Attacks do not depend on specific encodings. The formalization speaks the specification's abstract types; how curve points and field elements become bytes, in protocol messages or in the transcript, is not covered.
5. The deployed list of curve points is as good as a sampled one. Security is proved for protocols that sample it; the real one is hashed into existence and baked in.
6. The byte layer under the hashing schedule. What gets hashed, and in what order, is checked; how those things become bytes is not.
7. Facts established by running code trust the compiler. Each is pinned to its owning declaration at build time, and each is independently re-checkable — but the compiled code they run is the whole fast native arithmetic, proven correct in the kernel and executed as the compiler translated it.

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)/\text{\#}\mathbb{F}$, or the discrete-log advantage. The only layer that consumes an assumption.

How the layers compose

A capstone is assembled from several sub-reductions, called "arms", each with its own bound. The composition happens at the reduction layer (Layer B), not the probability layer (Layer C).

We use that approach for two reasons:

• Probability statements over different sample spaces don't combine straightforwardly — conditioning on a sub-event reweights the measure, and product measures and marginals get in the way.
• Directly combining results expressed in terms of probability often results in an unnecessarily loose reduction. The issue is that giving an adversary $n$ problems in parallel, of which they only have to find one solution, may or may not fundamentally help them depending on the detail of those problems. Black-box reasoning using the probability bounds for the individual problems has to assume the worst case, which loses a factor of $n$ in tightness (via a union bound).

Composing at the level of computable reductions makes it easier to handle both issues. A reduction is a total function from the adversary's output to a break, and so "run the adversary, then run the reduction" is just another machine (algebraic if both its components are) at an unchanged query count. Reductions compose by ordinary function composition — the path of least resistance that Lean's proof tactics handle well. And the reduction has the actual break data from the adversary's solution to one of the source problems. The tightness loss, if any, that the reduction incurs to solve the target problem will depend on the particular case, but this approach avoids throwing away information that is likely to be needed to get the best available reduction. The overall probability bound is then taken once at the end.

Three pieces of structure make that last step essentially mechanical:

• The event sets form a Boolean algebra, ordered by inclusion $\subseteq$ and combined by union $\cup$.
• The probability measure, $\mu$, of an event set is monotone and finitely subadditive. Monotone means that if $A\subseteq B$ then $\mu (A)\le \mu (B)$ (a subset of events has no greater probability than the original set). Finitely subadditive means that $\mu (A\cup B)\le \mu (A)+\mu (B)$ (the probability of a union is at most the sum of the probabilities of its parts). That's all we need: no independence and no inclusion–exclusion principle.
• The lift that carries a per-parameter event into the sample space is a monotone join-homomorphism — it preserves both $\subseteq$ and $\cup$. The lift is "there is a valid run, at the sampled parameters, whose output lands in the event"; it preserves unions because $\exists$ distributes over $\vee$.

So a composed bound is proved like this:

• First, a distribution-independent set-level containment: the bad event is contained in a union of per-arm events. This involves no probability over multiple sample spaces, so it is easily reusable.
• At this point it might be possible to collapse together either multiple possibilities for the same kind of event, or different events that rest on the same or closely related cryptographic problems.
• Finally, lift to a probability, and sum:
  • monotonicity carries the containment into the sample space;
  • the join-homomorphism distributes it over the union;
  • subadditivity turns the union into the sum of the per-arm bounds.

The Balance integrity argument as a worked example

Balance integrity has exactly this shape. Its set of violation events —the shielded pool going negative, or the pools failing to sum to the minted issuance— is contained in the union of the three Balance-subset break arms (Merkle, note-commitment, key-binding) and the Balance conservation violation. That containment is balanceIntegrityViolationBefore_subset_conservation; it mentions no probabilities and holds at every ledger prefix at once.

Lifting it to the sample space through the join-homomorphism sampledLedgerEvent and applying subadditivity, gives the integrity experiment's bound as the sum of the non-negativity side and the conservation side. The conservation side is reused wholesale — the conservation experiment is one arm dropped in as a black box. And at the Orchard instantiation, the three non-negativity arms, at all possible prefixes at which they could occur, collapse onto a single advantage — that of finding a nontrivial discrete-log relation among the fixed Sinsemilla bases. That is, each arm's break is routed through its deterministic reducer, so all three land in one event and are bounded once. This gives a reduction for the _idealizedks capstones that is almost optimally tight — losing only a factor of $2$ in tightness, without any factor of the number of ledger prefixes.

Naming the Boolean algebra, the subadditive measure, and the join-homomorphism is what turns per-composition plumbing into three reusable lemmas. This is an instance of a widely applicable principle — looking for the algebraic structure in a problem often drastically simplifies and clarifies it.

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/\text{\#}\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, for several reasons:

• 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$. This result is tight.
• Non-uniform definitions admit unrealistic counterexample algorithms, as discussed above (Bernstein–Lange).
• 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 makes at most $2^{123}$ random-oracle queries and performs at most $2^{125}$ group operations, the latter certified by a staged cost program. The statistical remainder ($2^{-83}$ for the consensus-generic Action capstone) is proved for every workload up to the full covered budget. The endpoints count the reduction's work additively, by a proved counter composition: the reduction adds at most $2^{123}$ group operations and 22 oracle queries to the adversary's own, and the advantage is evaluated at $2^{124}$ queries and $2^{126}$ group operations after rounding up to powers of two. The accounting overhead is a fraction of a bit of group work: before rounding, $2^{125}$ becomes at most $2^{125}+2^{123}\approx 2^{125.32}$.

It is easy to misread the $2^{126}$ target 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 rounded budgets 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 three supporting claims hold:

1. Re-expression: an adversary that is only incidentally non-algebraic must be re-expressible as an algebraic one at similar cost.
2. Structural compatibility: an adversary must not be able to make essential use of known structure of a curve that is unavailable within the algebraic model we are using.
3. Basis sufficiency: the basis of group elements provided to the adversary is sufficient to model realistic attacks.

The first claim says that our formalization of the algebraic model faithfully captures only the intended semantic restrictions; that is, if we write down some algorithm for a semantically algebraic attack, we will always be able to meet the syntactic requirements of the formalization.

The second claim is about the reasonableness of applying the AGM (in our variant) to the particular curves used by our protocol, Pallas and Vesta. That is, do they have known structure (or structure that an adversary might know) allowing for attacks outside the model that we need to be worried about in practice?

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. An example of structure that separates them is Pasta's efficient endomorphism: 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 third supporting claim is that the modelled basis covers all group elements that may be useful to an adversary in realistic attacks. The next section covers that issue.

Fixed bases, the group hash, 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 the group hash, inherits it — provided that the group hash scheme admits no attack more efficient than the algebraic ones bounded by the proven reductions. The group-hash indifferentiability development supplies the formal half of that judgement: the deployed group hash is indifferentiable from a random oracle into the group, under a named Weil-bound hypothesis, with the simulator exhibited as an algorithm.

No Lean theorem instantiates the soundness endpoints at the deployed bases; identifying Halo2's group hash outputs with the sampled basis is a heuristic step (Zcash/TrustBoundary.lean records this scope). The same heuristic underlies every fixed-base use of the group hash 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 group-hash 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 the group hash 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. The indifferentiability result is what licenses giving them that oracle as a random oracle.
• 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.

Reading the Security Bound

Bottom line: within the formal model, breaking the knowledge soundness of the deployed Action verifier is —up to a small statistical error— at least as hard as solving Vesta discrete log: the reduction turns every covered attack into a DLOG solver with comparable resources. The benchmark therefore remains Vesta DLOG, whose best known classical attacks have an expected-work scale of about $2^{126}$ group operations. This is conventionally summarized as a 126-bit headline security level for Vesta DLOG. At the certified profile, the constructed solver uses less than twice the attacker's group-work budget, giving this claim a conservative 125-bit computational-work headline; the advantage function below is the precise statement.

Here “knowledge soundness” means that whoever produced an accepted proof must know a valid witness: the private data that justifies the proved statement. The extractor computes the witness from the prover's declared group-element representations, not from the proof alone. “Covered” means inside the theorem's scope: an adversary that stays within the resource budgets below, supplies a representation for every group element it outputs, and faces Fiat–Shamir challenges modelled as a random oracle. The game also samples the verifier's fixed bases; the deployed, baked-in list inherits the result through the fixed-bases argument in Security Models.

For experts

For a bundle containing $n$ Actions and an adversary $A$ making at most $q$ random-oracle queries and performing at most $g$ Vesta group operations, the reduction gives

$$\mathrm{Pr}[\text{verifier accepts but extraction fails}]\le {\mathrm{Adv}}_{\mathrm{DLOG}}(q+22,g+R(n))+{\epsilon }_{\mathrm{stat}}(q,n).$$

${\mathrm{Adv}}_{\mathrm{DLOG}}(q,g)$ is the advantage function: for query budget $q$ and group-operation budget $g$, the externally supplied upper bound on the success probability of a Vesta DLOG solver.

${\epsilon }_{\mathrm{stat}}(q,n)$ is the statistical soundness error: it collects the non-DLOG statistical terms, including exceptional random challenges that prevent extraction and the random-URS binding term, for an adversary making at most $q$ oracle queries against a bundle containing $n$ Actions.

Direction of the reduction:

Action attacker $A$ using $q$ queries and $g$ group operations $⟶$ reduction adds 22 queries and $R(n)$ group operations $⟶$ Vesta DLOG solver using $q+22$ queries and $g+R(n)$ group operations.

The reduction constructs the DLOG solver by running the Action attacker and processing its output. $R(n)$ is the extra Vesta group work it performs for a bundle containing $n$ Actions — reduction overhead, not attacker work or a probability loss. For the deployed Action specialization, the reduction also makes 22 oracle queries beyond those made by the attacker.

For the certified consensus profile, $q\le 2^{123}$, $g\le 2^{125}$, $R(n)\le 2^{123}$, and ${\epsilon }_{\mathrm{stat}}(q,n)\le 2^{-83}$. The exact bound is

$$\mathrm{Pr}[\text{failure}]\le {\mathrm{Adv}}_{\mathrm{DLOG}}(2^{123}+22,2^{125}+2^{123})+2^{-83}.$$

Rounding the solver budgets up to powers of two gives the simpler endpoint

$$\mathrm{Pr}[\text{failure}]\le {\mathrm{Adv}}_{\mathrm{DLOG}}(2^{124},2^{126})+2^{-83}.$$

Here $2^{125}$ is the covered Action-attacker work budget. The reduction turns it into at most $2^{125}+2^{123}\approx 2^{125.32}$ solver work, giving Action a conservative 125-bit computational-work headline. The $2^{126}$ in the endpoint is only its rounded ceiling. Separately, Vesta itself has a headline 126-bit DLOG security level; the matching number has a different origin. Security Models gives the full coverage-parameter interpretation.

In plain language

Outside the statistical soundness error, a covered knowledge-soundness attack would imply a DLOG break with the resources shown above. No easier protocol-specific computational term remains in the bound.

The advantage function says more than any single “security-bit target” could: for any query and work budgets, it tells experts exactly where to evaluate their preferred Vesta DLOG estimate.

Reading the work curve

Choose an amount of Action-attacker group work on the horizontal axis, trace upward to the orange curve, and then read the corresponding computational-success scale on the vertical axis. The curve shifts the idealized Vesta DLOG reference by the reduction's conservative one-bit work loss. Its marked scale is therefore the headline for this claim: about $2^{125}$ group operations, derived from Vesta's 126-bit DLOG headline.

The graph shows only group work. The oracle-query budget $q$ remains a separate input in the equation above, and the statistical term is not plotted. The exact advantage function, not this illustration, is the security claim.

Lean proves the adversary-to-DLOG reduction, its resource transformation, and the statistical soundness error. The numerical DLOG estimate comes from external cryptanalysis.

Proof Journey

Follow the verifier-soundness argument in logical order, with the PR that landed each mechanized layer attached to the stage where it enters. Every anchor below is pinned at the current main, so the stages describe the tree as it stands rather than the stack that built it.

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.

The Knowledge-Soundness Contract

The Action circuit's knowledge-soundness result is one theorem, orchard_action_adaptiveStatement_knowledge_error_bound. Reading it tells you a probability is bounded — not what is bounded, what a successful extraction hands back, or what that thing certifies. Those live in the layers that prove it.

Zcash/Snark/Contract/ gathers them: KnowledgeContract is a record with one field per question an auditor must answer, and actionKnowledgeContract is its instance for the deployed circuit. The layer proves nothing new — it re-exports the definitions the theorem is stated in and applies the theorem itself unchanged, which is why its census pin carries exactly the endpoint's axiom footprint. The one substantive demand the record makes of an instance is the witness_statement field, discussed below. This page reads the instance in order.

The six questions

1. What is a run?

A generator random-oracle table and one Fiat–Shamir transcript, drawn independently. The URS basis is read from the table by orchardGeneratorROBasis, modelling halo2's parameter derivation ($g_i=H(0\Vert i)$, $W=H(1)$, $U=H(2)$) — a modelling assumption, not a theorem.

The adversary is adaptive in the statement: it outputs the public inputs and the proof together, and both the canonical verifying key and every selected instance commitment enter the transcript before the first challenge, so the statement cannot be chosen after seeing it. The adversary is also algebraic: its output type requires every emitted group element to carry a representation over the basis. That is a restriction on which adversaries the bound covers at all, not an assumption that can be discharged.

2. When does the verifier accept?

ComputedAdaptiveActionStatementFSFamily.accepts: halo2's checked acceptance at the adversary's own selected inputs and proof, over the URS read from the oracle table. This is DeployedAccepts, the verifier's entire check collapsed into one multiscalar multiplication — acceptance means the assembly succeeds and that MSM evaluates to zero. It is the deployed verifier's own condition, not a reformulation chosen to be convenient.

3. What does extraction return?

An ActionTerminal.ActionBundleWitness: the private witnesses of every Action in the bundle, packaged with proofs that they satisfy ActionSpec at the public inputs the adversary selected. It lives in Type — data a program can hold and inspect, not a proposition that a witness exists somewhere. The extractor is a total function; returning none is what extraction failure means, and that failure is the only event the bound is about.

("Executable" describes the extractor where the proving layer defines and checks it. The contract record is noncomputable — its law is a PMF, which Lean cannot run — and neither adds nor needs a computability check of its own.)

4. What does a returned witness certify?

BundleStatement: every Action in the bundle satisfies the circuit's statement at the public inputs the adversary selected. This field carries the weight — a bound on "accepted but extraction returned nothing" is worthless if extraction may return junk. witness_statement forecloses that: a returned witness entails the statement, and stating it as a field means no instance can quietly omit it.

5. What is the failure event?

Accepted, yet extraction returned nothing. Both conjuncts matter: a rejected run is not a failure, and neither is an accepted run that yielded a witness.

6. What is the error?

The endpoint's compositional formula: the adversary's discrete-log advantage at its query and group-work counts, plus $1/\text{\#}\mathbb{F}$, plus a per-query term collecting the Schwartz–Zippel budgets of each challenge surface. At the $2^{123}$ work-factor target it lands on ${\mathrm{Adv}}_{\mathrm{DLOG}}(2^{126},2^{126})+2^{-83}$, whose two arguments are the random-oracle query count and the group-operation count.

What the contract does not say

Completeness is not implied. That some run accepts, or that an honest prover's proof extracts, is a separate property. Nothing here rules out the vacuous case: a contract whose acceptance predicate holds nowhere satisfies every field. Read the contract as a bound on the adversary, never as evidence that the circuit works.

Ordinary soundness is not advertised separately — because it is free. On a false statement the extractor must have returned none, since a returned witness would have entailed it. So acceptFalseStatement_le gives the soundness bound at the same error for every contract, and no separate endpoint is advertised for it.

The ledger security capstones do not follow from it. The contract ends at ActionBundleWitness. The formal continuation begins, per Action, at Zcash.Security.Ledger.Bridge.actionSpec_to_ledger, which consumes the public input, private witness, and ActionSpec proof — and returns an ActionBreak or an existentially witnessed ledger statement in Prop, not an executable ledger witness. The ledger security capstones build on that handoff, and they depend on knowledge soundness rather than settle for less: they are stated in the witness-level model, over ledger actions that already carry witnesses, and extraction is what supplies those for a merely proof-carrying bundle. What this contract does not do is discharge that step for the deployed circuit — the witness-level model abstracts Halo 2 knowledge soundness away, and relating the two is a separate reduction on the different Halo 2 bases.

The assumptions are not fields of the record. They are the arguments of actionKnowledgeContract: a nonzero generator, an injective oracle-parameter query, the family-construction obligations, and the generic AdaptiveStatementDlogProfile, whose proverGroupWork and reductionGroupWork are caller-supplied labels with finderAdvantageLE the corresponding DLOG advantage bound. (The operationally accounted route is separate: AdaptiveStatementAdversaryCostCertificate and CertifiedAdaptiveStatementDlogProfile feed orchard_action_adaptiveStatement_certified_knowledge_error_bound.) Two more conditions are structural, carried by the adversary's type: the algebraic restriction above and the random-oracle modelling of the challenge schedule. What trusting each of these means is the subject of Security Models, and the Guide to the Ironwood Formalization states them in plain language.

Why the record is not Action-specific

KnowledgeContract is stated for any circuit. Action is its only instance because it is the only circuit carrying an advertised capstone — the other circuits are components composed into its specification. And the shape already recurs: the ledger security games pair a break event, a containment showing the event covers the property, and a bound — the same three moves as failure, witness_statement, and knowledge_sound. Keeping the record generic is what stops the second circuit's contract from becoming a second bespoke tree.

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 and key binding, to an exhibited break of a cryptographic primitive in a specified adversary model — and where the intended hand-off to verifier knowledge soundness remains open.

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

One picture, not yet connected

%%{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/issues/147'>intended hand-off:<br/>not yet formalized<br/>(#147, #155)</a>" .-> KS["Knowledge soundness:<br/>accepting proof yields<br/>witness or break data<br/>(separate development)"]
  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/ExtractionKnowledgeError.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 gapEdge stroke:#cf222e,stroke-width:3.5px,stroke-dasharray: 7.5 3.2
  class KERRtoNDLR,KStoDL,RDSAtoDL agmEdge
  class STMTtoKS gapEdge

➞ heavy purple edge: a reduction (or intended reduction) in the online-AGM — both endpoint games are algebraic
⇢ dashed red edge: an intended hand-off that is not yet formalized — the endpoints share no definition (#147, #155)
➝ 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

What the Balance capstones assume

The Balance capstones are stated for a Knowledge-Soundness-idealized adversary (IdealizedKSBalanceAdversary): one that outputs a witness-annotated ledger, every Action carrying the witness for the Action statement. The annotation is where knowledge soundness of the Action circuit enters: nothing yet connects an accepting Halo 2 proof to those witnesses, so the idealizedks in the capstones' names marks results that are complete over this idealized ledger model but not yet composed with the circuit layer. That composition is the dashed red edge above (#147); until it lands, the Balance integrity node stays amber even though every ledger-side arm is machine-checked. This is an incompleteness of the proof, not an accepted modelling trade-off. The capstones' accepted trade-offs —the binding challenge hash as a random oracle, the programmed value and binding bases carried to the deployed ones by the reference-string heuristic, elided byte encodings— are documented at IdealizedKSBalanceAdversary.violationEvent.

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)/\text{\#}\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.

As stated above, the KS-idealized 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 is intended to justify that modelling: whenever the ledger layer needs a witness, the extractor would compute one —or compute break data— from the accepting proof. That hand-off is not yet formalized in any form: the games state ActionSatisfied over their own abstract types, and no definition is shared with the SNARK development. The dashed red edge marks exactly this gap (#147, #155). Until it lands, the witness-supply requirement is a modelling assumption of the ledger games, not a consequence of verifier knowledge soundness.

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

Group-Hash Indifferentiability

The Zcash security arguments model the Pasta group hashes as random oracles into the curve groups. This page explains what justifies that modelling, and what the formalization does and does not establish. It is written for a reader who has not seen an indifferentiability proof before; no prior acquaintance with the notion is assumed.

The counting that the argument rests on lives in CompElliptic (Hashing/TwoTermUniformity.lean, Hashing/PastaSSWU.lean); the probabilistic argument on this page lives under Zcash/Security/GroupHash/.

The deployed hash

Let $\mathbb{G}$ be an elliptic curve group, $\mathbb{F}$ its field of definition (base field), and $M$ a convenient input domain. The deployed group hash $H⦂M\to \mathbb{G}$ is

$$H(m)=f(u_0)+f(u_1),(u_0,u_1)=hash\_to\_field(m,2),$$

where $f=\mathsf{mapToCurve}⦂\mathbb{F}\to \mathbb{G}$ sends a field element to a curve point, and the sum is the group law.

We model $hash\_to\_field(\cdot ,2)⦂M\to \mathbb{F}\times \mathbb{F}$ as a random oracle: an idealized hash whose output on each new input is a fresh uniform pair. The question is whether $H$ itself may then be modelled as a random oracle into the group $\mathbb{G}$. But first, we'll try to explain why a simpler construction does not suffice.

Mapping to a curve

How can we map from a field to an elliptic curve group? In the case of short Weierstrass curves, each non-identity point has coordinates $(x,y)⦂\mathbb{F}\times \mathbb{F}$ satisfying the curve equation:

$$y^2=x^3+a\cdot x+b$$

An obvious candidate for a map from a field element $u$ to a curve element would be to choose one of the points with $x=u$ using a deterministic square root function ${}^{+}\sqrt{\cdot }$, i.e. $(u,{}^{+}\sqrt{u^3+a\cdot u+b})$.

Sapling used twisted Edwards curves which have a different equation, but that is essentially what it did — pick one of the coordinates, and then the equation in the other is quadratic. It's easy to construct a hash into the field with low bias using a conventional hash function with a large enough output size, by taking its output as an integer modulo the field size. Then the mapping above is bijective, so its output points will be approximately evenly distributed, although only among half of the curve points — the half chosen by the deterministic ${}^{+}\sqrt{\cdot }$.

The problem is that then not all $x$-coordinates, and therefore not all inputs to the hash, map to a point. For each $x$-coordinate, we have 0, 1, or 2 solutions for $y$ depending on the number of square roots of $x^3+a\cdot x+b$. Heuristically, roughly half of the $x$-coordinates should have no solutions for $y$, roughly half of them should have two solutions, and a negligible proportion (only the case $y^2=0=x^3+a\cdot x+b$, which may not happen at all for a particular curve) have one solution. That is in fact what happens in practice. If the curve has $N$ points, and $N$ is odd —as it is for Pallas and Vesta— then the number of $x$-coordinates that correspond to a point on the curve is exactly $(N-1)/2$. The proportion that correspond to a point is $(N-1)/(2\cdot \text{\#}\mathbb{F})$, writing $\text{\#}\mathbb{F}$ for the number of elements of $\mathbb{F}$. The Hasse bound, $|N-(\text{\#}\mathbb{F}+1)|\le 2\sqrt{\text{\#}\mathbb{F}}$, makes the heuristic precise: $(N-1)/(2\cdot \text{\#}\mathbb{F})$ is within $1/\sqrt{\text{\#}\mathbb{F}}$ of ${}^1/{}_2$.

For fixed generators, having a group hash that is not a total function is not so much of a problem: we can extend it to a total function by repeated hashing with an index. Since there are only a fixed set of generators and they are found off-line, non-constant timing due to the variable number of iterations is not an issue. But Sapling had introduced diversified addresses, which require on-line use of the group hash in order to derive an address from a diversifier. We avoided timing attacks in Sapling by not doing repeated hashing, and accepting that only half of all diversifiers would be valid. But we had encountered complications in the application protocol (ZIP 32 and its usage) due to this abstraction leak from the underlying cryptography. We wanted to avoid that when designing Orchard.

Fortunately, an Informational RFC for deterministic, constant-time Hashing to Elliptic Curves was close enough to ready (it was in a late draft, and in fact did not change significantly before the final version, RFC 9380). The scheme we analyse here is that standard, specialized to Pallas and Vesta.

What 𝑓 looks like

So how does $f$, or as RFC 9380 calls it map_to_curve, work? A naive approach would be to try to "fill in" the other half of the curve points that were missed by the deterministic square root, using the other half of the $x$-coordinates. But there is no known way of doing so (in fact, if there were then it would indicate undesired structure and potential cryptographic weaknesses in the curve).

The basic idea of having two different cases depending on whether a given input yields solutions for a square root, however, is exactly what RFC 9380's "Simplified SWU" construction does. For now we will ignore a complication that arises for short Weierstrass curves with $a=0$, like Pallas and Vesta; we'll get to that in its own section. Then, ignoring negligible cases we have:

$$f(u)=\{\begin{array}{ll}{f}_1(u),& \text{for half of the }u\\ f_2(u),& \text{for the other half.}\end{array}$$

The Simplified SWU construction arranges that the two candidate curve-equation values differ by a nonsquare factor, so exactly one of the two branches is available for each input $u$. The precise formulas —including how $u$ is transformed before it becomes an $x$-coordinate— are in CompElliptic's Hashing/SimplifiedSWU.lean, the formalization of the construction.

The actual construction also fixes the sign at the end: the output's $y$-coordinate is negated if necessary so that its sign matches the sign of the input, in the convention that RFC 9380 calls sgn0. This makes $f$ odd, that is, $f(-u)=-f(u)$ for $u\ne 0$. Oddness carries weight below: it is what splits an input pair $\{u,-u\}$ across a point and its negation, and the character-sum analysis relies on it too.

The images of $f_1$ and $f_2$ are not disjoint; for Simplified SWU they in fact coincide, apart from a negligible proportion of exceptional points. To see why, fix a target point $P$. Whether any input reaches $P$ via $f_1$ comes down to a quadratic equation in $t=Z\cdot u^2$; the equation depends only on the $x$-coordinate of $P$, which $P$ shares with $-P$. A solution $t$ yields inputs precisely when $t/Z$ is a square —that is, when $t$ really is $Z\cdot u^2$ for some input $u$— and then, since $f$ is odd, the input pair $\{u,-u\}$ has one member mapping to $P$ and the other to $-P$. So each realizable solution contributes exactly one preimage of $P$. Reaching $P$ via $f_2$ comes down to a second quadratic in $t$, in the same way. Now, two facts connect the branches:

• $t$ solves the $f_1$-equation exactly when $1/t$ solves the $f_2$-equation;
• $t/Z$ is a square iff $(1/t)/Z$ is, because their product is the square $1/Z^2$.

So input $u$ reaching $P$ via $f_1$ corresponds to the inputs $\pm 1/(Z\cdot u)$ reaching $P$ via $f_2$ and vice versa. Hence $P$ is reached via $f_1$ iff it is reached via $f_2$.

This coexists with the exact halves above because those partition the inputs, not the outputs. The correspondence $u\mapsto \pm 1/(Z\cdot u)$ carries the $f_1$-half of the inputs into the $f_2$-half and back, preserving the point reached. About ${}^3/{}_8$ of the output space is reached —with 2 or 4 preimages per reached point excluding exceptional cases— and the remaining ${}^5/{}_8$ by neither map. (These proportions are heuristic; we confirmed them by exact computation on small curves, and they can be proven with error $O(1/\sqrt{\text{\#}\mathbb{F}})$ by counting points on the branch varieties — Lang–Weil, "Number of Points of Varieties in Finite Fields", Amer. J. Math. 76(4), 1954, doi:10.2307/2372655. A modern exposition of that paper is Tao, The Lang-Weil bound, 2012.)

It turns out, for the Pasta curves, that we cannot do much better than this ${}^3/{}_8$ coverage by mapping directly from a single field element (or at least, trying to do so would not lead to a less complicated scheme overall, given other constraints like the desire for a constant-time group hash).

Particular application protocols might actually be perfectly fine with this kind of non-uniform mapping. However, it can easily be distinguished from a uniform one, and each of our security arguments would then need to take the non-uniformity into account separately. That need does not go away entirely; what we can do is pay for it once, with a concrete figure. So we would like a mapping that, applied to $hash\_to\_field$ outputs, can be distinguished from a uniform mapping onto the whole group only with a concretely bounded advantage. As we will see, modelling $hash\_to\_field$ as a random oracle, that advantage is at most $q/2^{120}$ after $q$ queries for the mapping we chose.

The detour through an isogenous curve

Now for the complication we deferred. The formulas of Simplified SWU require the curve coefficients to satisfy $a\ne 0$ and $b\ne 0$. Pallas and Vesta both have the curve equation $y^2=x^3+5$, i.e. $a=0$. This is not by coincidence; the same Complex Multiplication structure that allows us to find a cycle of curves is what blocks Simplified SWU from working.

RFC 9380 (section 6.6.3) resolves this with a detour: run Simplified SWU on an auxiliary curve with $a\ne 0$ that is isogenous to the target. An isogeny is a mapping from one curve to another, given by rational maps on the coordinates, that preserves the identity point. In general it need not be invertible; over the algebraic closure, a degree-$3$ isogeny is $3$-to-$1$. For Pallas and Vesta, the auxiliary curves are the ones that the protocol specification and the pasta_curves crate call iso-Pallas and iso-Vesta respectively. Having used Simplified SWU to obtain a point on the auxiliary curve, we apply the isogeny (here of degree 3; the Pasta curves were chosen to make the degree as low as possible), in order to land on the intended curve.

For the analysis on this page the detour is short, at least conceptually. An isogeny is always a group homomorphism, and for these particular curve pairs it is a bijection on the rational points. (Isogenous curves have equally many rational points, and the kernels of these particular isogenies contain no rational point other than the identity.) A bijective relabelling of the outputs neither merges nor splits fibres, so the branch structure, the preimage counts, and the oddness that the character-sum analysis below relies on, all transport across unchanged. The formalization defines $f$ (mapToCurve) as the composition and states the counting theorems directly on that mapping.

Because the isogeny is a homomorphism, there are two equivalent ways to compute $f(u_0)+f(u_1)$: either by adding the two Simplified SWU outputs on the auxiliary curve and applying the isogeny once, or by mapping each point across the isogeny and then adding. The former method is used by RFC 9380 and hashtocurve.sage; the latter by pasta_curves. The two orders agree exactly (mapHashOutputsToCurve_eq), so nothing depends on the choice.

Although a correctly constructed isogeny is always a homomorphism (Silverman, The Arithmetic of Elliptic Curves, Theorem III.4.8), Mathlib does not prove that or have the necessary machinery to do so in general. Instead we prove that the particular rational maps given in the protocol specification (§5.4.9.8) and hashtocurve.sage are bijective (iso_map_bijective) and are homomorphisms (iso_map_add). The latter turns out to be quite involved, requiring a careful choice of coordinates to make it feasible to prove the necessary identities using Mathlib's linear_combination tactic. The details are explained in Homomorphism.lean.

We've now described the deployed construction in full, and established the motivation for using $H(m)=f(u_0)+f(u_1)$ instead of a mapping from a single field element. The rest of this page is about why that construction works, specifically why it can reasonably be modelled as a random oracle.

Uniformity is not enough

A first guess is that it would suffice for $H$'s outputs to be close to uniform on $\mathbb{G}$. We will see from the regularity analysis below that this holds. It does not suffice, because $H$ is not a black box. The function $hash\_to\_field$ is public: anyone can compute the intermediate pair $(u_0,u_1)$ and check that $H(m)$ really equals $f(u_0)+f(u_1)$. A security argument that replaces $H$ by an ideal random oracle $R$ must survive an adversary that does exactly that. So the question is not "do $H$'s outputs look uniform?" but "can the pair of oracles $(hash\_to\_field,H)$ be faked consistently, given only $R$ ?".

Indifferentiability

Indifferentiability (Maurer–Renner–Holenstein, Indifferentiability, Impossibility Results on Reductions, and Applications to the Random Oracle Methodology) makes that question precise. A simulator $\mathcal{S}$ is given oracle access to the ideal random oracle $R$, and must answer $hash\_to\_field$ queries. A distinguisher $\mathcal{D}$ talks to two oracles and tries to tell which of two worlds it is in:

• the real world $(hash\_to\_field,H)$ — the genuine intermediate oracle and the genuine construction built on top of it;
• the ideal world $({\mathcal{S}}^R,R)$ — the ideal random oracle $R$ into the group, and the simulator faking the intermediate hash consistently with it.

The construction is $(q,\epsilon )$-indifferentiable if some simulator makes every distinguisher's advantage at most $\epsilon$ after $q$ queries. The point of establishing this is the Maurer–Renner–Holenstein composition theorem: any^† protocol proven secure with an ideal $R$ in place of the group hash stays secure with the real $H$ — provided one is content to model $hash\_to\_field$ as a random oracle. So indifferentiability is what lets the rest of the security development treat the group hash as a random oracle without having to reason about $hash\_to\_field$ again.

The simulator is forced

The consistency check above pins down what the simulator must do. On a query $m$ it learns $Q=R(m)$, a uniform group element, and it must return a pair $(u_0,u_1)$ with

$$f(u_0)+f(u_1)=Q,$$

because the distinguisher can and will check that equation. Moreover the pair must look like a fresh $hash\_to\_field$ output, i.e. uniform — so the simulator must return a preimage of $Q$ that is close enough to uniform under the two-term sum. Following the proof of Theorem 1 of Brier–Coron–Icart–Madore–Randriam–Tibouchi (Efficient Indifferentiable Hashing into Ordinary Elliptic Curves), specialized to this construction, two ingredients make this possible.

The first ingredient: regularity

For uniform $(u_0,u_1)$, the distribution of $f(u_0)+f(u_1)$ is close to uniform on $\mathbb{G}$. CompElliptic's TwoTermUniformity proves this from a Weil bound on the character sums of $f$.

A character of $\mathbb{G}$ is a homomorphism $\psi ⦂\mathbb{G}\to {\mathbb{C}}^{\times }$ into the nonzero complex numbers: it turns the group operation into ordinary multiplication, $\psi (P+Q)=\psi (P)\cdot \psi (Q)$, and its values lie on the unit circle. The character sum of $f$ at $\psi$ is

$$S(\psi )=\sum _{u\in \mathbb{F}}\psi (f(u)),$$

the character added up over all outputs of $f$. The trivial character $\psi \equiv 1$ gives $S(\psi )=\text{\#}\mathbb{F}$; a Weil bound bounds the absolute value $|S(\psi )|$ at the nontrivial characters, from which such character-sum bounds follow. The name "Weil bound" is from André Weil's proof of the Riemann hypothesis for algebraic curves over finite fields (Sur les courbes algébriques et les variétés qui s'en déduisent, 1948). A modern presentation of the elliptic-curve case is Kohel–Shparlinski, On Exponential Sums and Group Generators for Elliptic Curves over Finite Fields, ANTS-IV, LNCS 1838, 2000.

Character sums measure uniformity because a distribution on $\mathbb{G}$ is uniform exactly when all its nontrivial character sums vanish — so small nontrivial character sums mean close to uniform. That is what lets a Weil bound control the regularity distance

$$\sum _Q\left|\frac{\mathsf{pairCount}fQ}{(\text{\#}\mathbb{F}{)}^2}-\frac{1}{\text{\#}\mathbb{G}}\right|\le \beta ,$$

where $\mathsf{pairCount}fQ$ counts the pairs $(u_0,u_1)$ with $f(u_0)+f(u_1)=Q$ — the size of the fibre of $Q$. Dividing by $(\text{\#}\mathbb{F}{)}^2$ turns the count into the probability that the two-term sum lands on $Q$, so the sum is the $L^1$ distance between that output distribution and the uniform distribution on $\mathbb{G}$. The $L^1$ distance between two distributions $\mu$ and $\nu$ on a finite set is ${\sum }_x|\mu (x)-\nu (x)|$, the total of the absolute differences of the probabilities they assign. $\beta$ will be calculated in the next section.

Calculating the Weil constant

The regularity distance is proved relative to the named hypothesis WeilBounded. That hypothesis is parameterized: it asserts a constant $C$ with every nontrivial character sum of the zero-repaired mapping at most $C\cdot \sqrt{\text{\#}\mathbb{F}}$, and the final advantage scales with $C^2$.

The formalization (sum_abs_prob_dev_le) bounds the regularity distance of the previous section by any budget $\beta$ whose square dominates $\frac{(\text{\#}\mathbb{G}-1)\cdot C^4}{(\text{\#}\mathbb{F}{)}^2}$ — that is, any $\beta$ just above $\frac{C^2\cdot \sqrt{\text{\#}\mathbb{G}}}{\text{\#}\mathbb{F}}$.

That expression is the aside's pipeline, made quantitative. The two-term spectrum at $\psi$ is $S(\psi {)}^2$, so each of the $\text{\#}\mathbb{G}-1$ nontrivial frequencies has spectral energy at most $(C^2\cdot \text{\#}\mathbb{F}{)}^2$. Parseval turns total spectral energy into the summed squared deviation of the pair counts, divided by $\text{\#}\mathbb{G}$; Cauchy–Schwarz bounds the square of an $L^1$ sum by $\text{\#}\mathbb{G}$ times the sum of squares, cancelling the $\text{\#}\mathbb{G}$ quotient; and normalizing counts to probabilities divides by $(\text{\#}\mathbb{F}{)}^4$ — leaving $\frac{(\text{\#}\mathbb{G}-1)\cdot C^4}{(\text{\#}\mathbb{F}{)}^2}$.

At the deployed sizes $\text{\#}\mathbb{F}\approx \text{\#}\mathbb{G}\approx 2^{254}$ and $C=21/2$ (see below), yielding $\beta \approx 2^{-120}$.

The Weil bound places a bound on character sums along covering curves of the encoding, once $C$ is calculated via a per-encoding genus computation. Proving this result in general requires machinery that is not yet in Mathlib, which is why the hypothesis is named rather than discharged; that is where the deep number theory lives.

The calculation of the constant $C$ for a specific encoding and curves, on the other hand, is relatively straightforward. For example, Farashahi–Fouque–Shparlinski–Tibouchi–Voloch carry out this calculation for a sibling of the deployed encoding —simplified SWU with $Z=-1$, over fields of size $\equiv 3(\mathrm{mod}4)$, with a quadratic-residue sign rule— and obtain $|S(\chi )|\le 52\cdot \sqrt{\text{\#}\mathbb{F}}+151$ from genus-8 coverings.

The deployed variant differs in all three parameters. The Weil bound for both Pallas and Vesta has been calculated as $|S(\chi )|\le 10\sqrt{\text{\#}\mathbb{F}}+1$ from genus-6 coverings (see zcash/pasta's weilbound.sage). This is where the deployed $C=21/2$ comes from: the hypothesis wants $|S(\chi )|\le C\cdot \sqrt{\text{\#}\mathbb{F}}$, and the extra half over the $10$ absorbs the trailing $+1$. In square-root-free form this is $(10\sqrt{\text{\#}\mathbb{F}}+1{)}^2\le (21/2{)}^2\cdot \text{\#}\mathbb{F}$, which holds at the deployed sizes with margin about $2^{126}$.

The calculation of $C$ is proven on paper in CompElliptic's design/weil-constant-derivation.md, modulo results cited as established mathematics. It is also formalized, down to Weil's theorem at the two branch covers, in CompElliptic's Hashing/BranchCovers.lean and Hashing/WeilInstance.lean. The per-cover inputs are $|S_{C_j}(\chi )|\le (2\cdot 6-2)\cdot \sqrt{\text{\#}\mathbb{F}}$ — the analogous sums over the rational points of the two branch coverings, stated in square-root-free form. Everything between those inputs and the deployed WeilBounded instances is machine-checked. The paper proof's own checkable inputs are also machine-checked (CompElliptic's Hashing/WeilSupport.lean), and the design doc cites each proven fact at its point of use, with CI keeping the references exact. Weil's theorem itself stays the cited input: even stating it needs vocabulary (genus, places, covers of curves) that Mathlib does not yet have. That vocabulary is tracked at CompElliptic#30.

The second ingredient: preimage sampling

For each $Q$, the simulator must sample a pair uniformly from the fibre $\{(u_0,u_1)\mid f(u_0)+f(u_1)=Q\}$. Sampling one coordinate is easy: draw $u_0$ uniformly. Then the second coordinate must satisfy $f(u_1)=Q-f(u_0)$, so $u_1$ ranges over the preimages of $Q-f(u_0)$ under the single map $f$. That single-term fibre has at most a constant number of elements — we saw in the "Where the ⅜ comes from" note above that each point has at most $4$ nonzero preimages under $f$, and CompElliptic's card_mapToCurve_fibre_le proves the weaker but sufficient bound of $10$, again counting nonzero preimages.

Care is needed to make the pair uniform on the fibre. Drawing $u_1$ uniformly from the preimages of $Q-f(u_0)$ would over-weight the pairs whose preimage set is small: the pair's probability would be $\frac{1}{\text{\#}\mathbb{F}\cdot c}$ with $c$ the size of its preimage set, and $c$ varies across the fibre. So the simulator instead fixes a bound $d$ on the preimage counts and draws a slot index $0\le j<d$ uniformly, alongside $u_0$. If the preimage set of $Q-f(u_0)$ has an element with index $j$, the round accepts the pair $(u_0,u_1)$ with $u_1$ that element; otherwise it rejects, and the simulator redraws both $u_0$ and $j$. In particular an empty preimage set always rejects. Now every pair of the fibre consistent with $u_0$ is accepted in a round with the same probability $\frac{1}{\text{\#}\mathbb{F}\cdot d}$, whatever the size of its preimage set, so conditional on acceptance the pair is exactly uniform on the fibre. The bound $d$ also controls the cost: a round accepts with probability $\frac{\mathsf{pairCount}fQ}{\text{\#}\mathbb{F}\cdot d}$, about $1/d$ for typical $Q$, so few rounds are needed. This is the rejection sampler whose costs and output law Simulator.lean proves, instantiated at the deployed mappings at the constant deployedFibreBound = 11 — the bound of $10$ for nonzero preimages, plus one for the input $0$.

The single-query bias, in detail

This is the part the formalization currently establishes, in Zcash/Security/GroupHash/Sampler.lean, and it is the technical heart of the argument. It compares the two worlds on a single fresh query, before worrying about how queries compose.

Two per-query laws

On a fresh query, the distinguisher observes a pair in $\mathbb{F}\times \mathbb{F}$ (from which the group element is a fixed function). Each world draws that pair from a distribution:

• real: the pair is uniform on $\mathbb{F}\times \mathbb{F}$ — this is $hash\_to\_field$ answering honestly (PMF.uniformOfFintype);
• ideal: draw a uniform group element $Q$, then draw a pair uniformly from the fibre of $Q$ (idealLaw, the bind of the uniform law on $\mathbb{G}$ with the fibre sampler).

The fibre sampler and its fallback

fibreSampler f Q samples a pair uniformly from the fibre of $Q$. One subtlety: the two-term sum need not be surjective, so some $Q$ have an empty fibre, with no pair to return. On those, the sampler falls back to a uniform pair on $\mathbb{F}\times \mathbb{F}$, which keeps it a genuine distribution. The fallback's only effect is on the bias, where it is accounted for exactly.

The bias reduces to the regularity distance

The claim, in each direction, is that the law in each world overshoots that of the other world by at most $\beta$: for every test $w$ valued in $[0,1]$, ${\sum }_x\mu (x)w(x)\le {\sum }_x\nu (x)w(x)+\beta$. This one-sided form (PMFWeightedBiasLE) is what the query-composition step needs.

To bound it, regroup the per-pair difference by the group element $Q=f(u_0)+f(u_1)$. Take a nonempty fibre of $Q$, with $k=\mathsf{pairCount}fQ\ge 1$ pairs. Every pair in it looks identical in both worlds:

• the ideal world puts $\frac{1}{\text{\#}\mathbb{G}\cdot k}$ on each pair — it spreads the $\frac{1}{\text{\#}\mathbb{G}}$ that $R$ gives to $Q$ uniformly over the $k$ pairs;
• the real world puts $\frac{1}{(\text{\#}\mathbb{F}{)}^2}$ on each pair.

So the absolute difference is one constant across all $k$ pairs of the fibre, and summed over the fibre it is

$$k\cdot \left|\frac{1}{\text{\#}\mathbb{G}\cdot k}-\frac{1}{(\text{\#}\mathbb{F}{)}^2}\right|=\left|\frac{1}{\text{\#}\mathbb{G}}-\frac{k}{(\text{\#}\mathbb{F}{)}^2}\right|,$$

a single term of the regularity distance. The $k$ cancels inside the first fraction. The fibre size enters only as $\mathsf{pairCount}fQ$ in that term, which is identical for every nonempty fibre — the ideal-world law is uniform within the fibre whatever its size, so all $k$ pairs share one probability. Summing over the nonempty fibres gives the part of the regularity distance with $\mathsf{pairCount}fQ>0$.

Why both directions come out at the same $\beta$

The empty fibres require our attention in one direction only.

When the real law overshoots the ideal one, the fallback only raises the ideal law's probabilities, which shrinks $\text{real}-\text{ideal}$. So this direction is bounded by the nonempty part of the regularity distance alone.

When the ideal law overshoots the real one, the fallback contributes a fallback mass $\frac{e}{\text{\#}\mathbb{G}}$, spread over all pairs, where $e$ is the number of group elements the two-term sum misses — the mass $R$ sends to those missed elements. That mass is exactly the empty-fibre part of the same regularity distance: an empty fibre has $\mathsf{pairCount}fQ=0$, so its term is $\left|0-\frac{1}{\text{\#}\mathbb{G}}\right|=\frac{1}{\text{\#}\mathbb{G}}$, and there are $e$ of them, totalling $\frac{e}{\text{\#}\mathbb{G}}$. So the nonempty part and the fallback mass together are the whole regularity distance ${\sum }_Q\left|\frac{\mathsf{pairCount}fQ}{(\text{\#}\mathbb{F}{)}^2}-\frac{1}{\text{\#}\mathbb{G}}\right|\le \beta$. The fallback fills in the terms the nonempty part left out, and the bound stays at $\beta$.

From one query to many

A single-query bound does not immediately bound a distinguisher that makes many adaptive queries — later queries may depend on earlier answers. The adaptive hybrid runFreshPMF_eventBiasLE (in Zcash/Common/Oracle/) bridges the gap: it charges the one-squeeze bias once per query node, so a $q$-query tree turns a single-query bias $\beta$ into an overall bias of at most $q\cdot \beta$, even when the query tree is fully adaptive. Repeated queries to the same point are first collapsed by dedup, so a point asked twice keeps one answer rather than drawing a fresh one.

What is proved, and what is modelled

It's important to be precise about the status of each part.

• Formalized and machine-checked. The regularity distance (TwoTermUniformity, conditional on the Weil bound), the single-term fibre bound (card_mapToCurve_fibre_le), the single-query bias in both directions (Sampler.lean), its composition into the full distinguisher-advantage bound at the deployed mappings (Indiff.lean), the collapse of the two-oracle game onto that one-oracle form (TwoOracle.lean), and the rejection-sampling simulator — its round-count laws, its output law's distance to the fibre sampler, and the composition with the simulator as the exhibited ideal-world witness (Simulator.lean and the capped section of Indiff.lean).
• An unformalized mathematical input. The regularity distance rests on Weil's theorem at the two branch covers — the CharSumBounded inputs discussed in Calculating the Weil constant. The bound calculation between those inputs and the endpoints is machine-checked; the inputs themselves are cited — stating them needs function-field vocabulary that Mathlib does not yet have (CompElliptic#30).
• A modelling choice, not a theorem. That $hash\_to\_field$ behaves like a random oracle is a heuristic (see the note above). The indifferentiability argument is what makes that heuristic transfer from $hash\_to\_field$ to the group hash $H$; it does not remove it.

Conclusion

The question this page set out to answer is: "can we formally justify modelling the deployed group hash as a random oracle into the curve group, given that $hash\_to\_field$ is so modelled?" The formalization now carries the whole argument, machine-checked at the deployed Pallas and Vesta instances.

A distinguisher that makes $q$ queries, and sees both the field-element hash and the group hash built from it, can tell the real construction from a random oracle with advantage at most $q/2^{120}$ (pallas_indiffFromRO, vesta_indiffFromRO, via the two-oracle collapse twoOracleIndiffFromRO). The only unformalized mathematical input is Weil's theorem at the two branch covers, discussed above. The $2^{-120}$ budget absorbs the regularity distance, about $2^{-120.2}$ (the arithmetic is at the end of the regularity section), and the zero-repair transport $4/\text{\#}\mathbb{F}$, roughly $2^{-252}$.

The ideal world in that statement is played by a simulator, and the simulator is a real algorithm, not just a distribution: it hashes once, then rejection-samples a preimage pair, giving up after $K$ rounds. Its cost is pinned down exactly — the chance that it is still running after $k$ rounds decays geometrically. The answers it returns differ from the idealized ones by at most $(1-\mathsf{acceptProb}{)}^K$ per query, where $\mathsf{acceptProb}$ is a round's chance of accepting, so the cap $K$ makes that difference as small as desired. The indifferentiability statement holds with this algorithmic simulator in place of the idealized one, at the cost of that same per-query term (pallas_indiffFromROCapped, vesta_indiffFromROCapped), conditional on the Weil bound hypothesis.

Two things remain, both tracked in issues:

• The Weil bound rests on a cited input: Weil's theorem at the two branch covers. The calculation from that input to the deployed constant is formalized, and so are the paper proof's supporting facts (CompElliptic's Hashing/WeilSupport.lean) — the delivered scope of CompElliptic#28. The input's own statement needs function-field vocabulary (genus, places, covers) that Mathlib does not yet have, tracked at CompElliptic#30.
• The security games that want to use this result need the group hash added to their adversary's interface first (#188). The composition requirement for multi-stage games (the † note above) applies at each consumption site.

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. The Oracle/ subtree holds the generic oracle-computation machinery shared by the Fiat–Shamir soundness reductions and the group-hash indifferentiability argument, so neither tier owns it: OracleComp is the bounded querying-adversary model — an adaptive oracle-query computation with eager whole-table semantics, an explicit query bound, and a per-run read log, plus dedup, domain restriction, query-charge accounting, and escape bounds; Model holds the one-sided PMFEventBiasLE/PMFWeightedBiasLE bias-transport interfaces; Hybrid is the adaptive fresh-answer hybrid that turns a single-query bias into the Q·ε bound; LabeledOracleComp adds labeled query trees and the first-label bad-set bounds; and WithReads returns a run's own reads with its output, growing the query bound only by the re-queried family's size.
• 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 four 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-NU6.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 as a standalone diagnostic, not a soundness or fixture-trust input. 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 — the conditionally staged-certified 2^125 adversary-work one and the deployed 2^123 one, with the declared-profile 2^123 instantiation pinned as the latter's rung — 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), plus a certified ceiling on the failure observer's query budget, without which the joint Challenge255 charge would be a free multiple — 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. ChallengeUniform gives the exactly-uniform challenge law over Fp; 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 premiss the work-factor capstone's bias conjunct consumes, with BLAKE2b's idealization as the uniform digest remaining external. (The generic oracle-computation machinery — OracleComp, the adaptive hybrid, and the PMFEventBiasLE transport interface — are in Common/Oracle/.)
• 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. Action.lean states the endpoints — knowledge-soundness bounds for every consensus-valid bundle size, in compositional error-formula form with declared and with staged-certified group-work accounting, in the staged-certified finite-security form at 2^125 adversary work, and in the deployed form that consumes an ActionDeploymentInstantiation, charges the joint Challenge255 bias once for the whole transcript, and prices that charge at 2^-136 against the record's certified query ceiling. 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.

Action.lean is the only endpoint file here. The Action/ subdirectory below it holds what discharges those endpoints at the captured key: Base carries the shape identification the chain is stated over, Checks the captured key's scalars and static checks, and Budgets the semantic surfaces. Those three are instance-level — stated at the capture and reaching it through their imports — which is why they sit here rather than under Soundness/, a subtree that imports no fixture so that the captures stay off lake build Zcash's path.

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

Contract/ — what the endpoints promise

The auditor-facing layer over Capstones/. Knowledge defines KnowledgeContract, a record of the runs a knowledge claim quantifies over, their law, what acceptance means, what an extraction returns, what a returned witness certifies, the failure event, and the concrete error — together with the generic consequence that accepting a false statement is bounded by the same error. Action instantiates it at the deployed Action circuit, reusing orchard_action_adaptiveStatement_knowledge_error_bound unchanged as the claim.

The record is deliberately not circuit-specific. Action is its only instance today because it is the only circuit carrying an advertised capstone; CommitIvk, NoteCommit, Ecc, Sinsemilla, and Poseidon are components composed into its specification rather than independent surfaces.

Nothing here proves anything new, so the layer adds no trust: both declarations are pinned in Fixtures/MultiAction/Honest/TrustBoundary.lean with the same axiom footprint as the endpoint they re-export. The prose counterpart is The knowledge-soundness contract.

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), 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, kernel-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; CircuitPreNU63 is the post-NU6.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. Soundness/Action/StraightLineTerminal reaches that same terminal from one accepting execution, and Soundness/Action/StraightLineEvent 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.

Build and CI checks

Building the Lean development re-elaborates every proof reachable from the build targets — a successful build is the verification. This page lists what CI runs on top of that build, and what each additional check guards. The workflow files under .github/workflows/ are the mechanism; the substance of what they do is described here.

The build

CI builds with

lake build --wfail Zcash FixtureCheck CircuitCheck MetaCheck SecurityCheck CensusCheck

The named targets are exactly the lakefile's default set, so lake build --wfail is equivalent. The --wfail treats warnings as errors. sorry elaborates with a warning, so among other things this causes any use of sorry to fail CI even where no census entry reaches it.

The targets:

• Zcash — the library: everything reachable from Zcash.lean, which imports Zcash.TrustBoundary, the library-wide axiom census. Building this target enforces every census entry in that file.
• FixtureCheck — the captured fixtures, the knowledge soundness capstones, and the keygen certificate. The fixture-local trust boundaries and the native_decide fingerprint faithfulness checks run here; this target is separate because the captures are large and slow.
• CircuitCheck — Zcash.Circuits.Tests: comparisons of the pinned verifying-key and layout dumps against the Lean circuit model.
• MetaCheck — tests of Zcash.Meta.AxiomCheck itself: forged axioms exercising its rejection paths, kept out of the production import graph.
• SecurityCheck — Zcash.Security.Ledger.BridgeTests: regression checks guarding the protocol distinctions a type-correct refinement could silently erase.
• CensusCheck — the endpoint census enforced a second time, from the elaborated environment: every endpoint-named declaration in the census files' import closure must carry a direct pin.

The build also re-elaborates proofs in the CompElliptic library that it depends on, but not necessarily every proof in that library, and not CompElliptic's additional CI checks.

Source-level checks

Each of these is a standalone script under scripts/, run by CI on every Lean-relevant change. All of them can be run locally from the repository root.

• check_build_coverage.sh — CI and the lakefile agree on the target list, and every Lean module is reachable from it. A module no target reaches is not elaborated at all: its sorrys, its axiom drift, and even a failure to compile would be invisible to a green build.
• check_endpoint_census.sh — every deliverable soundness endpoint is named in a census pin. The census commands traverse a declaration's dependencies, so an endpoint that nothing pinned depends on would otherwise be invisible to every census entry.
• check_csimp_census.sh — every @[csimp] replacement lemma has its own assert_axioms entry. The compiler applies a csimp substitution in all downstream compiled code, but the lemma's own axioms are not propagated into downstream native_decide axiom tracking (lean4#7463).
• check_costed_group_work_census.sh — the staged Vesta work model's host callbacks (pure/map payloads) carry non-group computation at no charge to the group-work counter. The cost language is shallow, so Lean cannot check that an opaque payload performs no Vesta group law; each such definition is therefore pinned, and a new one must join the census to be reviewed against that condition.
• check_no_umbrella_imports.sh — no Lean file imports a Mathlib umbrella module. import Mathlib pulls in all of Mathlib, and several such processes in a parallel build create severe memory pressure.
• check_fixture_manifest.sh — every machine-generated capture artifact matches its recorded digest and provenance entry in Zcash/Snark/Fixtures/MANIFEST.tsv. This binds the committed artifacts to their provenance on every run, with no Rust toolchain needed.

Fixture regeneration

scripts/regenerate-fingerprint-fixtures.sh proves the committed captures regenerate byte-for-byte from their sources: it clones the pinned Orchard release, asserts the tag and its published lockfile checksums, regenerates every capture family plus the proof-byte siblings, and diffs each committed artifact. CI runs the full regeneration when a fixture-relevant path changes; on every other run, the manifest check above still binds the artifacts to their recorded digests.

The circuit-side layout dumps have no regeneration pipeline: their generator is unpublished one-off instrumentation in local halo2/orchard checkouts (Zcash/Circuits/Fixtures/PROVENANCE.md records the lineage). This should not be confused with the verifier-fingerprint exporter above, which is published and pinned. Publishing the layout instrumentation is #207. CI instead pins the bytes of the layout dumps: SHA256SUMS must list exactly the committed dumps, each digest must match, and the Stamp.lean rendering of those pins —which carries a fixture change into Lake's import graph— must be current.

Book checks

The book workflow validates the proof-journey page's graph data before building: book/validate-proof-journey.py checks the recorded edges against the checked-out Lean tree, so a renamed or deleted anchor fails CI rather than silently pointing at nothing. The book itself is then built with mdbook, which resolves every included file and internal link.

Working Notes

The pages in this section are development-facing notes: normative rules for how the codebase is organized, and specifications of refactoring arcs. They are kept with the book so that they render and stay discoverable, but their register differs from the rest of this chapter: they describe the development as it stands, and they are refreshed as refactoring arcs complete rather than kept continuously current.

• The Clean Boundary is the normative rule for how Clean-originated concepts appear in ironwood.

The Clean boundary: architecture rule

This note is normative for how Clean-originated concepts appear in the ironwood codebase. It exists so that the work converges on one structure, instead of each workstream growing local bridge plumbing.

The principle

Ironwood is the host, Clean is a guest. Ironwood has its own first-class vocabulary — VerifyingKey, Expr, Shape, its satisfaction notions, its polynomial environments — and the guest must not scatter its vocabulary (Halo2.ConstraintSystem, Operations, Gate, Expression F Query, RichExpression, …) through the host's rooms.

Everything Clean produces is funneled through one concept: TopLevelCircuit, which carries everything downstream needs and is instantiated once per concrete circuit (actionCircuit).

TopLevelCircuit is deliberately two-sided:

• It is a Clean-native core concept (it may well migrate into Clean itself — TopLevelKeygen already consumes only Clean and could follow). Its Clean-typed methods (constraintSystem, operations, config, …) are legitimate and public — for the boundary implementation.
• Ironwood defines an ironwood-native interface on top of it, and that interface is the only thing non-boundary ironwood code may consume. Its outputs are ironwood-typed; a reader never needs to know Clean exists to use it.

The canonical example of the pattern is

TopLevelCircuit.toVerifierKey : TopLevelCircuit → ProofParams → URS G → VerifyingKey …

— the core Clean concept bridged to a core ironwood concept in one method, with every Clean internal invisible in the signature.

The ironwood-native interface (target surface)

On TopLevelCircuit, defined ironwood-side in the designated boundary modules:

• toVerifierKey (pp : ProofParams) (urs : URS G) : VerifyingKey (pp.mergeDerived top) … — keygen, with the derived Shape in the return type (no lawfulness side condition).
• Shape/domain data as needed by consumers (ProofParams.mergeDerived, domain scalars).
• An Expr-typed pinned-constraint-system view (the boundary applies RichExpression.toExpr internally, exactly as toVerifierKey already does for the VK's gates).
• A satisfaction contract in ironwood terms: an ironwood-decoded assignment satisfying the circuit's derived key implies the circuit's public statement. The internal generic proof may pass through top.Statement over a reconstructed Clean environment, but that environment and the whole satisfaction-integration cluster are implementation details rather than a public seam.

The rule (enforceable, greppable)

Clean identifiers may appear only under Zcash/Circuits/ and inside the designated boundary modules. Every other Zcash/Snark/ (and Common/, Security/) signature mentions only TopLevelCircuit and ironwood types.

Review test: would a reader of this file need to know Clean exists to understand it? If yes and it is not a boundary module, it is misplaced.

Worked example of the anti-pattern

Zcash/Common/ExprRich.lean. RichExpression exists precisely because ripping ironwood's Expr out of ironwood for Clean's use would have been rude in the other direction — the type was deliberately duplicated so the clone stays on the guest's side of the wall. Installing its conversion (ofExpr/toExpr/eval_ofExpr) in the host's Common/ un-quarantines it: it presents a Clean-side clone as a core ironwood concept. (Contrast Common/Expr.lean in the same folder — ironwood's own shared AST — which is exactly what Common is for.) The conversion belongs inside the boundary as private plumbing; with an Expr-typed pinned view on the interface, nothing outside the boundary mentions RichExpression at all.

Current state of the boundary

Checked against the tree as of dc421aa0 (2026-08-21):

• Zcash/Bridge/ is dissolved; Snark/VkCommit/ became the designated boundary family Snark/Keygen/; and the RichExpression conversion lives inside the boundary (Circuits/Integration/ExprRich.lean).
• The cross-language satisfaction seam lives under Zcash/Circuits/Integration/.
• Clean imports are otherwise confined to Zcash/Circuits/ and Snark/Keygen/. One violation of the greppable rule remains: Snark/Fixtures/SingleAction/Honest/VkMatch.lean imports Clean, declares definitions with Halo2.SelCompressMap and Halo2.AnyColumn in their types, and applies RichExpression.ofExpr. It should be restated over the interface, in the style that Snark/Keygen/Certificate.lean demonstrates.
• The cross-repo migrations — Circuits/Fixtures/Layout.lean's keygen semantics into Clean's Halo2/Keygen, and eventually Circuits/TopLevel{,Keygen}.lean themselves into Clean core — ride Clean pin cycles and have not happened.

Drawing the boundary precisely

The directory boundary is a dependency boundary, not merely a collection of files created during the circuit-integration work.

What stays verifier-native

The following concepts speak only the ironwood verifier's language and remain under Zcash/Snark/Soundness/:

• ConstraintSatisfaction and ConstraintPolyModel;
• CanonicalConstraintModel and the canonical domain-selector mathematics;
• permutation and lookup instantiation and semantics;
• the decoded multiopen constraint resolver.

In particular, CanonicalConstraintModel takes a VerifyingKey, challenges, and an ironwood CommitmentId → Polynomial resolver and produces an ironwood ConstraintPolyModel. It does not know about a Clean circuit and is an input to the boundary, not part of its implementation.

Some existing files need splitting rather than moving wholesale. For example, PolynomialEnvironment currently contains both the verifier-native interpolation construction (rowPolynomial and its algebraic facts) and the Clean-facing constructor of a Halo2.Environment. The former stays in Snark/Soundness; only the latter moves into Circuits/Integration.

What lives in Zcash/Circuits/Integration

This directory contains the implementation that is forced to understand both sides:

• extracting the gate, copy, lookup, and fixed-data obligations of Clean operations;
• interpreting ironwood resolver polynomials as a placed Clean environment;
• connecting selector compression and query layouts to Clean gate evaluation;
• reassembling those families as Clean's authoritative Halo2.Constraints;
• applying TopLevelCircuit.soundness;
• specializing the generic result to a concrete circuit statement such as Orchard Action.

Pure Clean compiler semantics should instead live in Zcash/Circuits/ or, preferably when reusable, upstream in Clean itself. Pure ironwood soundness stays in Zcash/Snark/Soundness/.

Deployed specializations stay with soundness

A theorem that relies on the large captured VK artifacts—Fixture.shape, Fixture.vk, capturedURS, or the certificate equating those values with circuit-derived keygen output—belongs under Zcash/Snark/Soundness/Deployed/, not in this directory. Such a theorem may import the boundary's public circuit-derived terminal, but it should not re-establish Clean semantics itself. Conversely, Circuits/Integration should not import the fixture dumps merely to advertise the final deployed capstone.

The public satisfaction contract has two levels

TopLevelCircuit declares a PublicInput type and an injective layout of its encoded elements in instance cells. That one layout derives both extraction from a Clean environment and the cell/value assignments consumed by verifier integration. The top-level circuit separately extracts a private witness, recombines public and private data into its formal-circuit witness, and proves that this factorization agrees with the formal circuit's native extractor. Its Spec receives public and private data explicitly; only Statement public existentially hides the private witness.

The boundary therefore exposes two theorem levels:

1. a boundary-internal generic theorem taking satisfaction of the circuit-derived key to top.Statement at the public input extracted through the declared layout;
2. a public theorem phrased only in ironwood-decoded data and the concrete circuit's public statement, for example the structured Orchard Action public inputs.

No caller of the public theorem should construct a Clean environment or mention Operations, ConstraintSystem, selector compression, placement, or RichExpression.

Consequence of circuit-derived key generation

For vk := top.toVerifierKey pp urs, the gate and lookup expressions, query layouts, shape counts, domain parameters, permutation chunks, and commitment families are outputs of the same circuit-owned keygen pipeline. Their correspondence must not be reintroduced as an arbitrary caller-supplied coherence record.

Gate and lookup registration plus selector allocation now come from packaged Clean lawfulness. The remaining TopLevelConstraintBounds contains only supported-domain and polynomial-degree bounds; it is not a gate-coherence sidecar. Gate well-formedness remains intrinsic to Gate.