The whole verifier collapsed into one multi-scalar multiplication; the proof accepts exactly when that MSM is the group identity. Checked equal to the Rust verifier's captured MSM on four captures —two honest accepting runs and two match-only ones— for the specific circuit under analysis. The map's pinned to Rust node.

A capture of the deployed verifier run on a random proof string: deliberately non-accepting, it witnesses coefficient-for-coefficient agreement without an accepting run. Random inputs reach the proof slots that cannot be varied by honest proofs, so these captures carry the trust-boundary invariant.

The concrete verifier decision: the MSM assembled from the proof, instances, verifying key, and derived challenges evaluates to the group identity.

halo2's explicit IPA verifier equation, recovered from the compact MSM = 0 acceptance. This is the readable form that the IPA argument consumes.

An adaptive oracle-query computation with eager whole-table semantics, an explicit query bound, and a log of the points read on each execution. The straight-line reduction uses this model to price fresh-query and pinned-root events without constructing a transcript tree.

Replacing only a proof's IPA fields while preserving the pre-IPA proof data. The adaptive AGM hand-off uses this data operation when assembling the proof returned by its algebraic adversary; it is not a rewind extractor.

The transcript-ordering guarantee: each IPA round point sits in the transcript prefix before its challenge is drawn, so later messages cannot bend earlier challenges.

The security layer prices squeezes as exactly uniform; the deployed Challenge255 conversion instead reduces a 64-byte digest modulo $p$. With the digest idealized as uniform, an event's probability exceeds its uniform value by at most $r(p-r)/(p\cdot 2^{512})<2^{-260}$, where $2^{512}=qp+r$ — the exact constant, attained by the heavy residues, stated as the PMFEventBiasLE premise the transport theorem and the work-factor capstone's bias conjunct consume. Idealizing Blake2b as the uniform digest stays external.

The auxiliary generators the deployed verifier folds into the MSM alongside the main $g$ basis — the fold and blinding terms.

From one algebraically represented accepting proof, compute either the required opening data, an explicit relation over the augmented basis, or a pinned low-degree challenge event. No recursive transcript tree is constructed.

Folding the claimed value and synthetic blinder into the opened commitment: $P^{\prime }=P-[v]g_0+[\xi ]S$. The un-shift/un-blind lemmas move an opening of $P^{\prime }$ back to the actual multiopen commitment at its true value.

An adversary that supplies, with every group element it outputs, a representation: coefficients expressing that element over the elements it has received. Only the provenance of outputs is restricted — the computation choosing the coefficients may use any structure it can see. The restriction is part of the adversary's type, and every generic adversary is algebraic. See the algebraic-adversary restriction for what supports the heuristic.

Program every basis slot from the discrete-log challenge as $x•B+y•C$ with fresh uniform pairs (Jaeger–Tessaro, Lemma 3). The reduction restricts how the basis is sampled, not the adversary: it consumes relation coefficients from any source, so it carries no AGM scoping. A relation with nonzero challenge component yields the discrete log of the challenge; a miss retains the exact same returned relation and proves it annihilates the programming — a single $1/|\mathbb{F}|$ hyperplane, with no slot guess and no $|\mathrm{basis}|$ factor.

A modelling ingredient of the discrete-log endpoints: the reference-string generators are drawn from a programmable random oracle, so the programmed-basis reduction can embed its discrete-log challenge into the basis. Named with generatorRO wherever it applies, from the oracle setup and basis constructions to the capstones stated in this modelling.

A reference string of uniformly distributed group elements, with no hidden structure or trapdoor. The deployed protocol produces its URS once, by hashing public strings to the curve (GroupHash, spec §5.4.9.8), and the security statements sample it instead via the generator-RO. The gap between the two —including the protocol-lifetime caveat— is discussed under fixed bases, hash-to-curve, and the reference string.

The deployed AGM route. Each IPA round exposes an executable pre-squeeze polynomial computation, proves that it has not queried that round's squeeze point, and connects its result to the final proof. One accepting transcript therefore yields a clean decode, explicit DLOG relation, or pinned quadratic event. The combined finder uses at most four prover invocations, so no expected-runs truncation or Markov tail appears anywhere in the bound. ofCovered packages the representation-carrying online prover with caller-supplied executable root, IPA, and constraint-$x$ stages plus freshness proofs; the captured endpoint applies existing verifier metadata without a new proof fixture. The representations exist only in the model —the algebraic adversary supplies them alongside its proof, and the extractor reads them— and are never Halo2 proof bytes; this is an AGM-and-random-oracle result. The verifying key, instance commitments, and initial transcript prefix are fixed per basis before oracle access. Only the adaptive-statement capstone permits online statement choice.

The group-work accounting language reifies as explicit syntax only the group operations a program writes as nodes. Everything else — the Lean terms building pure payloads, query arguments, and continuations — stays in the host language, where Lean has no operational cost semantics. That is what shallow means here, and the price of it is that the counter measures what was staged rather than what the host computes: group law performed inside an unreified callback would go uncharged. StagedGroupWorkFaithful is the judgement that no such work exists, which is why it is a named premiss carried into the endpoints rather than a theorem. A deep embedding — host computation reified as syntax too — would discharge it in Lean, at the cost of rewriting the reduction in that syntax.

The programmed-basis reduction turns a computed relation into either a discrete-log solution or one $1/|{\mathbb{F}}_p|$ miss hyperplane. The adaptive route uses a staged cost language whose erasure is the original algebraic adversary. One closed program constructs the charged basis, specializes the exact adversary path while retaining its annotation log and group nodes, builds a proof-carrying cache from that result, and feeds the same cache into charged verifier postprocessing. Lean proves that this program's counter is the adversary counter plus the reified reduction counter; no separate arithmetic join or second adversary execution remains. At $Q\le 2^{123}$, the endpoints bound failure by ${\mathrm{Adv}}_{\mathrm{DLOG}}(2^{124},2^{126})+2^{-83}$ for either a $2^{123}$ or $2^{125}$ adversary group-work budget; the latter's adversary-plus-reduction group work is at most $2^{126}$. Equality/list traversal, direct-coordinate work, and random-oracle queries are separate resources. The three-decode bound follows from a required family representation-length invariant; the generic theorem does not construct a concrete deployed family. Because the language is shallow, staging fidelity remains explicit both for the external adversary and for host computations inside the complete program, such as generic key construction, hashing, and fixed-representation callbacks. These numbers are coverage parameters, not a claim that Lean computes Vesta's DLOG advantage.

The decoded columns satisfy the verifier's full compressed constraint identity, including custom gates, permutation constraints, and lookups — the constraint half of SnarkRelation.

A family of explicit AGM-supplied openings in flat $x_4$-power form, with witness, $U$, and $W$ components carried as data. It is not constructed from an accept-measure rewind.

The $x_4$-level point-set aggregates recovered by applying the Vandermonde inverse componentwise to explicit opened-batch data.

The deployed $x_4$ fold is proved to have the flat power-batch shape. The AGM $x_1$ layer then supplies explicit openings for the individual queried member commitments.

The challenge values that fool the gate check — the roots of the constraint-difference polynomial; a uniform random-oracle challenge lands in it with probability ≤ $d/p$ (Schwartz–Zippel). A challenge outside it is the map's sound challenge.

The straight-line pricing of the constraint-evaluation challenge: the pre-$x$ constraint difference's root set is capped by the degree walk — ${\epsilon }_x=20470/|\mathbb{F}|$ at the captured key, consumed as $(Q+1)\cdot {\epsilon }_x$. Its causal half — the root set is fixed before the $x$ squeeze, and is unchanged when the run's own $x$ answer is reprogrammed — is discharged, not assumed: pinnedX derives it from the staged trace the computed family carries. What the caller supplies is that trace, with the per-stage freshness proofs ofCovered requires.

The additive deployed extraction bound at the captured key for the represented straight-line algebraic adversary, with Fiat–Shamir and generator derivation modelled as random oracles. The endpoint uses staged representations and a fixed four-call finder, adding the $2k$ IPA-root term and no expected-runs or Markov term. It includes the DLOG term, the shape's root budget, and the concrete $(Q+1)\cdot 20470/|\mathbb{F}|$ constraint-root term. It is a compressed-identity statement; row-level gate, permutation, and lookup semantics carry the four explicitly priced $y$/$\beta$/$\gamma$/$\theta$ budgets through the matching semantic promotion. Concrete hash identification and the caller-supplied staged computations remain outside this theorem.

The adaptive-statement capstones prove a knowledge-failure bound for the deployed Action verifier against represented online algebraic adversaries, with Fiat–Shamir challenge derivation modelled as a random oracle. The adversary chooses the public statement and proof together, and the selected instance prefix is bound before $\theta$. For every consensus-valid Action count, a faithfully staged adversary bounded by either $2^{123}$ or $2^{125}$ group operations has failure probability at most ${\mathrm{Adv}}_{\mathrm{DLOG}}(2^{124},2^{126})+2^{-83}$, provided $Q\le 2^{123}$. Erasure preserves the original game; one composed program value-threads the exact adversary path and cache through the reduction; and Lean checks the counter decomposition and $2\times$ arithmetic. The result remains conditional on two explicit shallow-language fidelity obligations: the supplied adversary program and the complete program's host callbacks must perform no hidden Vesta group work. Its three-decode bound is conditional on the family's required representation-length invariant, which is not a concrete deployment instance constructed here. The quoted powers are resource coverage —not a universal failure ceiling— and the result does not cover arbitrary non-algebraic adversaries or concrete Blake2b. The random oracle ranges over bounded transcripts of the deployed schedule; AGM representations accompany every query but are erased before the oracle answers. The family fixes its key digest and verifier representations per basis before oracle access, and bundle size is public, universally quantified up to the consensus maximum.

The event that the deployed Action verifier accepts but the executable extractor does not return private witnesses for the entire bundle. The capstone bounds this event directly.

The explicitly priced $y$, $\beta$, $\gamma$, and $\theta$ challenge surfaces needed to promote the compressed constraint identity to row-level gate, permutation, and lookup semantics.

The composed capstone returns the deployed Action circuit's private witnesses and satisfaction proofs. The remaining output-side floor is the bridge from that compiled circuit specification to the abstract Orchard ledger relation. On the input side, Lean derives the verifying key and checks it against the capture; identifying that capture with Orchard's canonical deployed artifact and byte serialization remains external.

No transaction creates or destroys value (spec §4.13 Sapling / §4.14 Orchard). Value commitments are cv v rcv $=v•\mathcal{V}+\mathsf{rcv}•\mathcal{R}$; a bundle's binding verification key collects to $\mathsf{bvk}=A•\mathcal{V}+B•\mathcal{R}$ with $A$ the net value imbalance. The property is not "no discrete-log relation between $\mathcal{V}$ and $\mathcal{R}$ exists" —one always does in a prime-order group— but the reduction in the NontrivialRelation card below.

The break, as computed data: a nontrivial $\mathbb{F}$-linear relation between the value base Vbase ($\mathcal{V}$) and randomness base Rbase ($\mathcal{R}$), with its coefficients explicit — equivalently the discrete log dlog_Rbase Vbase (imbalance_yields_discrete_log). One always exists at prime order, so an ∃-closed Prop version (or a disjunction branch concluding it) is vacuous as a statement. The reductions compute one from a non-balancing verifying bundle with no cryptographic hypothesis (ofImbalance, and the bundle forms ofBundleModImbalance, ofOrchardImbalance, ofSaplingImbalance); the force is the computational assumption that no efficient adversary can find one.

Lifts field balance ($A=0$ in ZMod r) to integer balance: with per-action 64-bit value ranges and a bounded action count, $|A|<r$, so the residue being zero forces the integer to be zero. Discharged per pool from the value-type subranges.

Turns the computed Orchard/Sapling relations into plain discrete-log solutions: if you can unbalance, you can solve DL. DLR and DL are tightly equivalent (Jaeger–Tessaro, Expected-Time Cryptography: Generic Techniques and Applications to Concrete Soundness, Lemma 3), so this assumes no more than DL hardness, given the independence of the hash-to-curve bases.

A verifying Recovery-Statement witness pins its key components —$\mathsf{ak}$ (up to sign), $\mathsf{nk}$, and the $\mathsf{qk}$/$\mathsf{sk}$ branch with its key— to $\mathsf{ivk}$, unless a break is exhibited (ZIP 2005 key-binding theorem). Factors as KB = KBOpening ∧ KBDerivation: the ${\mathsf{Commit}}^{\mathsf{ivk}}$ opening and the derivation constraints.

Algebraic core: two openings of the same ${\mathsf{Commit}}^{\mathsf{ivk}}$ value force their Pedersen scalars equal or negated. An OpeningBreak (two valid openings differing in the opening data) is the break structure the games layer produces.

The reduction computes a $\pm$-collision of the $\mathsf{rivk}$-derivation random oracle at distinct derivation queries from a break (Layer B). Producing that collision within $q$ queries is bounded by the birthday bound ${\epsilon }_{\mathrm{kb}}\le q\cdot (q-1)/|\mathsf{RIVK}|$, which is $q\cdot (q-1)/r_{\mathbb{P}}$ at the intended Pallas instantiation (Layer C).

The games-relevant conjuncts of an Orchard-shaped Action statement (spec §4.17.4) over abstract primitives: commitment integrity, Merkle-path validity, nullifier integrity, the key-binding condition, address integrity, value-commitment integrity. This is the interface the games consume, and the target the verifier-soundness proof is meant to deliver.

The deterministic steps of the Balance argument: an address $(g_d,{\mathsf{pk}}_d)$ determines $\mathsf{ivk}$ (needs only $g_d\ne 0$ and torsion-freeness), hence $\mathsf{nk}$ is determined up to an exhibited key-binding break, and spends of the same note tuple reveal the same nullifier up to a break.

A note-commitment opening collision, as data. noteCommitBreakOfNe computes one when an extract-equal commitment fails to pin the note tuple $(\mathsf{rcm},\mathsf{note})$. Prequantumly, note-commitment binding reduces to a Sinsemilla / discrete-log-relation break.

Fixed-depth Merkle trees are position-binding up to a hash collision: a validating authentication path for a leaf that is not the committed one, against a defined tree, computes a DefinedCollision of one height’s compression — escaped (⊥) evaluations never count as collisions. The vector-commitment property the Balance and Spendability arguments require of the note-commitment tree. Prequantumly, the Sinsemilla compression’s collision resistance reduces to a discrete-log-relation break (SDLR) — the same terminal as note-commitment binding — so BLAKE2b collision resistance does not enter the pre-quantum Balance argument.

The shielded pool is non-negative and the pools sum to the minted issuance. The deterministic balanceIntegrityOrBreak proves it up to a computed break; the probabilistic violation events mirror its conclusion (the transparent conjunct cannot fail on the valid sample space). The interval consequence $\mathsf{pool}\in [0,\mathsf{issuanceTotal}]$ is weaker, and is stated separately as the shielded-balance-cap capstones.

An adversary is a PMF over valid annotated ledgers; each event is "the computed reduction lands in this branch on this sample", so no choice is needed to extract break data. Violation events are contained in unions of break events, and each break event's probability is a named ε hypothesis.

One ε per shared break event bounds the violation at every prefix below a bound, where a naive union bound would pay $k\cdot \epsilon$. Prefix-indexed value events are named *Before and step-indexed Balance-subset events *UpTo (EWD 831 half-open ranges, exclusive bound as the parameter); the one step/prefix crossing is confined to _succ-marked lemmas.

At the Orchard-protocol bases, every Balance-subset arm's break computes a nontrivial discrete-log relation among the fixed Sinsemilla bases, so one ${\epsilon }_{\mathrm{sinsemilladlr}}$ replaces the three per-arm ε's — and every prefix lands in the same relation event, so the all-prefixes bounds cost no factor of $k$. ${\epsilon }_{\mathrm{sinsemilladlr}}$ reduces tightly to discrete-log hardness (Jaeger–Tessaro, Expected-Time Cryptography: Generic Techniques and Applications to Concrete Soundness, Lemma 3, re-proved as relation_prob_le_of_textbookDL); the witness-level model abstracts away Halo 2 knowledge soundness, a separate, lossy reduction on the different Halo 2 bases. ${\epsilon }_{\mathrm{bindsig}}$ names the bound on the conservation side; the extractor-plus-knowledge-error forms and the κ discharge below replace it with named bounds further down the reduction (#107 tracks the remaining glue).

The binding signature is a signature of knowledge of $\mathsf{bsk}$, the discrete log of $\mathsf{bvk}$ base $\mathcal{R}$; the conservation reduction's extraction-failure arm is bounded at $(q_H+2)/|\mathbb{F}|+{\epsilon }_{\mathrm{DL}}$ for any query-bounded algebraic ledger adversary. This is the straight-line AGM+ROM extraction of Fuchsbauer–Plouviez–Seurin (Blind Schnorr Signatures and Signed ElGamal Encryption in the Algebraic Group Model, Theorem 1), in the key-only setting — no signing oracle, because the signature extracted from is the adversary's own. The DL premiss is uniform over challenge tables: one ε bounds the finder for every table. A reduction that samples the table internally would need only its overall advantage. Challenge queries carry the adversary's representations as labels the oracle never sees. The representation in effect at the output's query point —the run's first annotation there, or the announced output representation when the run never queried the point— pins the query's one bad challenge before the answer is drawn. Away from it the verification equation computes a relation over the presented basis. The extractor reads the key's $\mathcal{R}$-coefficient off that effective representation, and the reference-string heuristic carries the random-basis game to the deployed bases.

Layer-A break events for the classical ROM: a Collision is two distinct queries with equal outputs; a CollisionUpToSign ($a=\pm b$) is the shape produced by arguments passing through the Extract coordinate extractor, whose fibres are $\{P,-P\}$. Key binding bottoms out here, as does the nullifier (Faerie-Gold) argument for the Recovery Statement; the deployed nullifier argument bottoms out in the Sinsemilla discrete-log relation instead.

A $q$-bounded query log has a shifted $\pm$-collision with probability at most $q\cdot (q-1)/|\mathbb{F}|$, by union-bounding $2/|\mathbb{F}|$ per pair. queries_pair_collision_measure_le proves this in the random-oracle model without a hardness assumption; birthday_closed_form supplies the arithmetic identity (#73).

Break events are structures carrying the breaking data (colliding queries, relation coefficients); the reductions producing them are plain computable defs. An ∃-closed break Prop is vacuously true at the instantiations of interest (relations always exist at prime order; compressing hashes always have collisions), so the content lives in the data, protected by compiler-checked computability and pinned axiom sets. See Breaks as computed data.

Build-time pins on what a theorem may rest on: assert_axioms asserts a bound on the axioms used by a definition, so that a stray sorry or a new axiom fails the build instead of silently widening the trusted base. assert_computable additionally asserts that the definition is a plain def, ensuring constructivity of security reductions. Some of the TrustBoundary modules also use #guard_msgs-pinned #print axioms checks, e.g. to pin specific native axioms. See Trust discipline; what the fixture boundaries check is each family's Boundary.lean statement of record.