All missions

The claim

The HTLC mission proved which witnesses spend a received HTLC output under the script interpreter, and that its timeout path runs through OP_CHECKLOCKTIMEVERIFY <cltv_expiry>. That is a statement about one script evaluation. The claim Lightning actually needs is one block higher: no block can contain a non-revocation spend of a received HTLC by the timeout path before the expiry height. This mission composes the script result with the block mission's finality rule (IsFinalTx, required by ContextualCheckBlock for every transaction in a block) to state exactly that, and the same bound for a pre-signed HTLC-timeout transaction whose lock time is the expiry.

What is proved

• Finality of height-locked transactions (isFinalTx_height): with a nonzero lock time below the threshold and an input that is not SEQUENCE_FINAL, a transaction is final at height $h$ iff its lock time is below $h$.
• Pre-signed HTLC-timeout transactions (presigned_timeout_height): lock time cltv_expiry means acceptance only in a block above the expiry.
• Received HTLC, timeout path (received_spend_height, the goal): a two-element witness accepted by VerifyScript for a received HTLC output, in a transaction final at height $h$, is a revocation spend or has cltv_expiry < h.

What this rests on and what it does not say

The composition uses only published theorems: received_p2wsh_spend, cltv_concrete, checkLockTime_iff (HTLC mission) and the block mission's isFinalTx. It does not say that a transaction final at a height is in a block at that height, which is the block mission's ContextualCheckBlock characterization, nor anything about the offered HTLC's timeout path beyond the pre-signed transaction's own lock time (there the bound rests on the remote node signing only a transaction with that lock time, a key-level fact outside the script). Time-based expiries (lock times at or above the threshold) are excluded by hypothesis; BOLT #3 uses heights. (BOLT #3, tx_verify.cpp)

The claim

A Lightning channel's funds sit in the funding transaction's output, a pay-to-witness-script-hash of the 2-of-2 script 2 <pubkey1> <pubkey2> 2 OP_CHECKMULTISIG. Everything else in the protocol (commitment transactions, penalties, HTLCs) rests on one fact about this output: it moves only with both parties' signatures. This mission proves that fact against the script interpreter as transcribed from Bitcoin Core, and completes the on-chain script set of a channel begun by the to_local, HTLC and anchor missions.

What is proved

• The script on its witness (funding_witness): the 2-of-2 loop's verdict, with the NULLDUMMY condition on the dummy element.
• The spending condition, for any witness (funding_spends_iff): the witness-v0 success condition holds iff the stack is exactly [sig2, sig1, dummy] with each signature valid for its key in order; no other shape succeeds.
• The output under VerifyScript (parseScript_funding, funding_p2wsh_spend, the goal): the byte form parses as intended, and VerifyScript accepts a witness for the P2WSH output exactly when it is dummy sig1 sig2 with both signatures valid for the spending transaction's own checker.

What this rests on and what it does not say

The signature checks are the signature mission's checker with the witness-v0 sighash; which transaction the signatures commit to (a commitment transaction, a mutual close) is a matter of what was signed, outside the script. BOLT #3's lexicographic ordering of the two keys is not a script-level condition and is not stated. (BOLT #3, interpreter.cpp)

The claim

Modern Lightning channels use option_anchors: the remote balance and both HTLC kinds carry a one-block OP_CHECKSEQUENCEVERIFY so that a commitment transaction's outputs cannot be spent in the same block it confirms in, and each side gets an anchor output that it can spend at any time to bump the fee, and that anyone can sweep after 16 blocks so that anchors do not litter the UTXO set. This mission proves what those scripts enforce, against the script interpreter as transcribed from Bitcoin Core, completing the BOLT #3 commitment-transaction script set begun by the to_local and HTLC missions.

What is proved

• to_remote (to_remote_eval, to_remote_spends_iff, parseScript_toRemote, to_remote_p2wsh_spend): spendable by the remote key, only after the one-block delay, and by nothing else.
• Anchor (anchor_eval, anchor_holder, anchor_anyone, anchor_spends_iff, parseScript_anchor, anchor_p2wsh_spend, anchor_anyone_concrete, anchor_anyone_delay): the funding-key holder spends at any time; a clean-false signature (the empty signature) spends exactly after the 16-block delay; under the concrete checker, the empty-signature witness verifies iff the spending transaction is version 2 or later with nSequence ≥ 16. A signature the checker rejects outright fails the script.
• HTLCs with anchors (the six path theorems, the two spends_iff, the two parse theorems, the two p2wsh_spend): the HTLC mission's three paths each, with the one-block delay added to every non-revocation path and the revocation path unchanged.

What this rests on and what it does not say

The signature checks stay at the level of the signature mission's checker; the 20-byte hashes are parameters. anchor_anyone_concrete holds under consensus flags: under the policy flag WITNESS_PUBKEYTYPE an uncompressed funding key would make the empty-signature path fail, which is not modelled. With the CHECKSEQUENCEVERIFY flag off (pre-BIP112 blocks) the anchor is spendable by anyone at once; the activation mission fixes the flag on for every current height. The HTLC-success and HTLC-timeout second-stage transactions pay to the to_local script, already covered. (BOLT #3, interpreter.cpp)

The claim

A Lightning commitment transaction carries one output per in-flight payment: an offered HTLC (the local node pays if the remote reveals the preimage, or recovers the funds after the timeout) or a received HTLC (the local node claims with the preimage before expiry, else the remote takes the funds back). BOLT #3 gives each a witness script with three branches (revocation, preimage, timeout), and the channel's security rests on those three being the only ways to spend. The to_local mission proved this for the balance output; this mission proves it for both HTLC scripts, against the script interpreter as transcribed from Bitcoin Core.

What is proved

• The opcodes (cltv_step, multisig_two): OP_CHECKLOCKTIMEVERIFY passes exactly under CltvPasses; a 2-of-2 OP_CHECKMULTISIG passes iff each signature verifies for its key in order.
• Each path in closed form (offered_revocation, offered_preimage, offered_timeout, received_revocation, received_success, received_timeout): on the BOLT #3 witness shapes the interpreter leaves exactly the expected check, including the NULLDUMMY condition on the multisig dummy.
• The spending conditions, for any witness (offered_spends_iff, received_spends_iff): over an arbitrary stack, the witness-v0 success condition holds iff one of the three paths' conditions holds. Two facts the interpreter forces that the BOLT text leaves implicit: the inner selector is "is the top element 32 bytes long", not "is it empty"; and every non-revocation path requires the top element not to hash to the revocation hash, because OP_DUP OP_HASH160 … OP_EQUAL hashes whatever is on top.
• The outputs under VerifyScript (parseScript_offered, parseScript_received, offered_p2wsh_spend, received_p2wsh_spend, the goal): the byte forms parse as intended, and the pay-to-witness-script-hash outputs are spent exactly by the three paths, with the spending transaction's own signature checker and lock-time check.
• The lock time (cltv_concrete, checkLockTime_iff): with the CLTV flag active the check is Core's CheckLockTime, which for a block-height expiry is "nLockTime is a height at least the expiry and the input is not final".

What this rests on and what it does not say

The two 20-byte hashes are parameters, not tied to any key or preimage; signature checks stay at the level of the signature mission's checker. The HTLC-success and HTLC-timeout transactions themselves (second-stage, with their own to_local-style scripts) and the anchor-output variants of the scripts are not modelled, nor is the protocol-level argument about who holds which key when. (BOLT #3, interpreter.cpp)

The claim

A Lightning commitment transaction pays the local node's balance to a to_local output whose witness script (BOLT #3) reads

OP_IF <revocationpubkey> OP_ELSE <to_self_delay> OP_CHECKSEQUENCEVERIFY OP_DROP <local_delayedpubkey> OP_ENDIF OP_CHECKSIG

The channel's security rests on two claims about this script: the counterparty can spend it at any time with the revocation key, and the local node can spend it with its delayed key only after to_self_delay blocks, and nobody can spend it any other way. This mission proves both, and the "no other way", against the script interpreter as the script, signature and verification missions transcribed it from Bitcoin Core.

What is proved

• The interpreter run (eval_cons, csv_step, serialize_length): the script on any stack b :: tl of admissible size fails unless tl is a single element, and otherwise leaves the result of the selected signature check; the OP_CHECKSEQUENCEVERIFY step passes exactly under CsvPasses.
• The spending conditions (spends_iff): for any stack whatsoever, the witness-v0 success condition (one element left, and true) holds iff the stack is [b, sig] and either b is true and sig verifies for the revocation key, or b is false, the sequence check passes, and sig verifies for the delayed key.
• The output (parseScript_toLocal, p2wsh_spend, the goal): the byte form of the script parses as intended, and VerifyScript accepts a witness for the pay-to-witness-script-hash output exactly when the witness is [sig, b, script] and the selected branch's conditions hold for the spending transaction's own signature checker and sequence check.
• The delay (csv_concrete, checkSequence_iff, lightning_delay): with the CHECKSEQUENCEVERIFY flag active, the sequence check is Core's CheckSequence, which for a 16-bit delay and a flag-free nSequence (as Lightning sets it) is exactly "version ≥ 2 and nSequence ≥ to_self_delay".

What this rests on and what it does not say

The signature checks are the signature mission's checkSigPreTapscript with the witness-v0 sighash; nothing here says who holds the keys or how they are derived (BOLT #3's key derivation and the revocation secret are outside the script). The P2WSH program must be a true value, which VerifyScript requires of every witness program and which is a fact about one SHA-256 output the model cannot evaluate symbolically. MINIMALIF is policy, so under consensus any true selector opens the revocation branch; the relative lock time itself (whether the spending transaction may enter a block) is the block mission's BIP68 check, not the script's. (BOLT #3, interpreter.cpp)

The claim

"Bitcoin is secure as long as honest miners hold the majority of the hashrate" is the informal reading of Garay, Kiayias and Leonardos's backbone analysis: in a synchronous network, if the adversary finds fewer blocks than there are uniquely successful honest rounds over every long enough window, then honest chains grow (chain growth), agree on all but their last blocks (common prefix), and contain honest blocks regularly (chain quality). This mission states the synchronous model and proves these three properties from that combinatorial hypothesis.

What is proved

• The model: executions with honest parties, a rushing adversary, maxvalid adoption, and valid chains in which every block sits on exactly the chain its creator extended (the hash-chain abstraction).
• Chain growth (chain_growth, chain_growth_self): between rounds $r$ and $s$ every honest chain grows by at least the number of successful rounds in between.
• Common prefix (uniquely_successful_height, common_prefix_private, common_prefix_rounds, common_prefix, the goal): a uniquely successful round pins the honest block at its height; a private fork that stays adversarial for a window loses; hence the chains of any two honest parties agree once the last $2λ$ blocks are dropped.
• Chain quality (chain_quality): any $λ$ consecutive blocks of an honest chain contain an honest block.
• The bridge to Core (chainWork_const_bits): at constant difficulty the block mission's chainWork is the block count times one block's proof, so "longest" and "most work" coincide in this regime.

What this rests on and what it does not say

Nothing probabilistic is proved: Typical (adversarial blocks in every window of length $≥ λ$ strictly fewer than the uniquely successful rounds strictly inside it) is assumed, where the paper derives it from Chernoff bounds and honest majority. The constants are $k = 2λ$ and $ℓ = λ$ rather than the paper's $2λf$; only the weak form of chain quality is proved. The model is synchronous with one honest block per party per round, no explicit message layer, and static difficulty. (ePrint 2014/765)

Motivation

Philippe Flajolet and Robert Sedgewick's Analytic Combinatorics is the standard reference for counting discrete structures exactly and asymptotically. Its methods are used throughout the analysis of algorithms, random structures and enumerative combinatorics. This mission collects formally verified versions of the book's chapter-level results in one connected development.

Setting

A combinatorial class is a set of objects with a size such that each size has finitely many objects. Its generating function records how many objects have each size: the ordinary generating function $C(z)=\sum_n c_n z^n$ for unlabelled classes and the exponential generating function $\sum_n c_n z^n/n!$ for labelled ones. The symbolic method translates constructions on classes (disjoint union, product, sequence, set, cycle, pointing) into equations between generating functions. For example, if a class has counting series $C(z)$ and no size-zero objects, the series $S(z)$ for ordered sequences of its objects satisfies

Lagrange inversion recovers the coefficients of implicitly defined series. Singularity analysis and the saddle-point method turn the analytic behaviour of a generating function into asymptotic estimates for its coefficients, and the same machinery gives limit laws for parameters of random structures.

Formalization targets

Goal

The goal is the ordered-sequence identity above for a class with finitely many objects of each size and none of size zero, stated for formal power series over $\mathbb Q$. The sequence class includes the empty sequence of size zero.

Milestones

The 132 milestones are the remaining results, listed in the order of the book's chapters. Counts per chapter, goal included:

The total is 133 results.

Significance

The results are classical; the book proves them. This mission adds machine-checked proofs: every listed result has a Lean 4 proof accepted on the platform against a fixed Mathlib revision. Formalizing them pins down hypotheses that informal statements leave implicit: which objects a series counts, which convergence and nonvanishing conditions an estimate needs, and which limits are taken.

Difficulty

Informal treatments identify a generating function with "the" counting sequence of a construction; a formal statement must fix the finite type of objects being counted and the exact construction, so the symbolic-method results here are stated against explicit finite object types. Analytic estimates cannot be read off formal series: they need the analyticity domain, the behaviour near the dominant singularity and explicit error terms. Several saddle-point estimates require uniform local and tail bounds that informal arguments state only loosely; where the source assumes such bounds, the statements here keep them as hypotheses.

Formalization scope

Formal power-series identities are stated coefficientwise and do not require analytic convergence. Analytic estimates and probability limits keep their convergence, nonvanishing, parameter and measurability conditions. Results that the source proves under explicit assumptions remain conditional on those assumptions. Some results import supporting lemmas that are proved as separate theorems of the mission.

The mission covers 133 chapter-level results of the source development. It does not claim that every theorem of the book is formalized; coverage is exactly the verified declarations in the mission. Further results, sharper variants and alternative proofs are welcome as additional theorems.

Selected references

• Philippe Flajolet and Robert Sedgewick, Analytic Combinatorics, Cambridge University Press, 2009. Author-hosted book.
• AnalyticCombinatorics source repository, the immutable source revision formalized here.

Motivation

Atlases I–IV certified four-dimensional vacuum and Einstein–Maxwell metrics on a registered coordinate definition layer. Atlas VI extends the certificate notion to total dimension $5=4+1$ and asks two concrete questions: inside one explicit static ansatz, exactly when is the five-dimensional Einstein–Maxwell certificate satisfied; and for the cohomogeneity-one equal-spin ansatz, is the full system of field equations equivalent to a finite set of radial equations.

Setting

Total dimension $5$, signature $(-,+,+,+,+)$, $\Lambda=0$, coupling $G_{ab}=2S_{ab}$ with $E_{ab}=R_{ab}-\tfrac12 g_{ab}R-2S_{ab}$. VI-01: $g=-f\,dv^2+2\,dv\,dr+r^2[du^2/(4u(1-u))+u\,d\varphi^2+(1-u)\,d\psi^2]$, $f=1-\mu/r^2+\beta/r^4$, $A=-Q/(2r^2)\,dv$, on $\{r>0,\ 0<u<1\}$ for all real $\mu,\beta,Q$. VI-02: $g=-B\,dt^2+D\,dr^2+A[du^2/(4u(1-u))+u(1-u)(d\varphi-d\psi)^2]+H(\sigma-W\,dt)^2$, $\sigma=u\,d\varphi+(1-u)\,d\psi$, $\mathcal A=\Phi\,dt+\Psi\,\sigma$, $F=d\mathcal A$, radial data $C^\infty$ on an open $R$ with $B,D,A,H\neq0$ (ESData).

Formalization targets

• Goal: under ESData, $R\neq\emptyset$ and $A>0$, $H>0$, $BD>0$ on $R$, the Einstein–Maxwell certificate on $\{x_1\in R,\ 0<u<1\}$ holds iff the five reduced Einstein and two reduced Maxwell radial equations hold on $R$.
• VI-01: certificate iff $3\beta=Q^2$; Ricci-flat certificate iff $\beta=0$; explicit counterexample at $(1,1,1)$.
• VI-02: pointwise completeness of the seven reduced equations; fixed certified instances MP01 (VacuumCertificate, and EMCertificateD with $F=0$), MP02 (EMCertificateD with $F=0$ only, via the reduced system; no VacuumCertificate statement) and ST03 (static charged EMCertificateD); refutations NW01 ($\neg$ VacuumCertificate) and NQ14 ($\neg$ EMCertificateD).

Significance

A machine-checked reduction of a five-dimensional Einstein–Maxwell system to seven radial equations, with explicit domains and hypotheses, usable as a certificate checker for equal-spin candidates; the VI-01 criterion derives the charge normalisation.

Difficulty

All curvature data are explicit closed forms generated as CAS hints and re-proved in Lean component by component (Christoffel, derivative, Ricci and Einstein–Maxwell tables); the reduction needs frame reconstruction lemmas for every residual component.

Formalization scope (what is NOT claimed)

• EF5 is one fixed explicit static ansatz (f = 1 − μ/r² + β/r⁴, A = −Q/(2r²) dv); cert_iff (3β = Q²) is a criterion inside that ansatz, not a classification of five-dimensional black holes.
• EF5.vacuum_cert and EF5.vacuum_cert_iff conclude EMCertificateD with F = faraday5 0 (= 0); the literal VacuumCertificate (Ricci-flat) iff is EF5.vacuumCertificate_iff.
• ESData asks only: R open, the seven radial functions C^∞ on R, and B, D, A, H nonvanishing on R — no field equation. The Goal additionally assumes R.Nonempty and A > 0, H > 0, B·D > 0 on R. No B > 0, D > 0, connectedness, exterior-only or q ≠ 0 hypothesis is assumed or claimed.
• ReducedSystem consists of FIVE Einstein (redE_tt, redE_tσ, redE_rr, redE_uu, redE_σσ) and TWO Maxwell (redJ_t, redJ_σ) radial equations; F = d𝒜 by definition supplies closedness. It is not the VI-03 six-state CAS system.
• MP01 and MP02 are two specified certified parameter instances (μ = 3, a = 1/2 and μ = 5 with rotation constant −2/3), not a certified arbitrary-parameter Myers–Perry theorem. ST03 is one fixed static charged instance (μ = 2, Q = 1, β = 1/3).
• Each candidate domain is exactly esDomain {r | 0 < r ∧ rX r ≠ 0} with the listed exclusion polynomial rX; no horizon or axis (u ∈ {0,1}) regularity is claimed.
• NW01 refutes VacuumCertificate (¬ Ricci-flat certificate); NQ14 refutes EMCertificateD. They are ordinary theorems with negated conclusions, not disproofs of positive targets.
• B3 coordinate certificates on the registered local layer (PHYSICS_BOUNDARY §N, §O), not Mathlib-only or manifold results. No new exact charged-rotating solution, global event horizon, uniqueness, gauge equivalence or static ↔ EF coordinate bridge is claimed.
• Supplementary Python/CAS/search evidence (VI-01 per-run instances, PS00/PS02 pilot replays, VI-03 CAS) is outside this release and is not a formally verified search algorithm. EF5/Certificate.lean conditional assemblers are excluded.

Selected references

• R. C. Myers, M. J. Perry, Ann. Phys. 172 (1986) 304 — family name of MP01/MP02/NW01 (not accessed; see LITERATURE_CHECK.md).
• F. R. Tangherlini, Nuovo Cimento 27 (1963) 636 — family name of EF5/ST03 (not accessed; normalisation derived in Lean).
• Exact Vacuum / Spacetime Atlas I, II, IV (the author's earlier releases; bundles and nodes reused unchanged).

The claim

A transaction's identifier is the hash of its serialization without witnesses, and that serialization still contains every scriptSig. Before SegWit, anyone could take a valid transaction, re-encode a signature inside a scriptSig (a different DER length byte, a negated S value, an extra push), and broadcast a transaction that was equally valid and had a different txid. Any protocol that referred to an unconfirmed transaction by its txid — a refund signed against a funding transaction, which is how payment channels start — could be broken this way. BIP141 fixed it by moving signatures into the witness, which the txid does not hash, and by requiring the scriptSig of a native witness spend to be empty.

This mission proves that the fix does what it claims, against the published VerifyScript and CheckInputScripts: for a transaction whose inputs spend native witness programs and whose scripts verify, the txid is a function of the sender's intent — version, prevouts, sequence numbers, outputs, lock time — and of nothing else.

What is proved

• native_scriptSig_empty — under CheckInputScripts with WITNESS, every input spending a native witness program has an empty scriptSig (SCRIPT_ERR_WITNESS_MALLEATED, lifted from the VerifyScript mission's native_witness_malleated).
• txid_of_intent — for such a transaction, txid tx = txid (ofIntent (intentOf tx)): the identifier of the canonical transaction with empty scriptSigs and witnesses.
• txid_determined (goal) — two transactions with the same intent, both verifying against the same ledger, with native witness-program inputs, have the same txid.
• p2sh_wrapped_scriptSig — for a P2SH output spent with witness data, VerifyScript succeeds only if the scriptSig is exactly the single push of the witness program it evaluates to (SCRIPT_ERR_WITNESS_MALLEATED_P2SH); the scriptSig of a wrapped spend is determined by the redeem script.

What this rests on

The serialization mission's txid_strip (the txid ignores witnesses), the VerifyScript mission's native_witness_malleated, and the block mission's CheckInputScripts. The statements are about the executable VerifyScript; no assumption about hash functions or signatures is needed, because the theorems say nothing about whether a valid spend exists, only that its identifier is fixed once it does. (interpreter.cpp, transaction.h, BIP141)

The claim

"There will only ever be 21 million bitcoin" is the most repeated statement about the system, and it is usually justified by the subsidy schedule alone: fifty coins, halved every 210,000 blocks, summing to just under 21 million. The schedule is proved in the subsidy mission (BitcoinSubsidy.issuance_total). But the schedule is a bound on what a coinbase may create; whether the chain's spendable supply stays within it depends on the whole validation path — that every non-coinbase transaction spends at least what it creates, that no input is spent twice, that the coinbase is bounded by the subsidy plus the fees actually collected, and that these checks run against the right ledger at every step. The inflation bug CVE-2018-17144 was a failure of exactly this composition, not of the schedule.

This mission states the bound as a property of every chain state reachable from the genesis under the block mission's validate, and proves it.

What is proved

With totalValue u the sum of the values of the coins of a ledger and issued n the subsidy GetBlockSubsidy has issued to a chain of n blocks:

• update_bound — UpdateCoins raises the total by at most the value created and lowers it by the value spent (ledger arithmetic on a distinct-key ledger).
• values_in_range — every coin of a reachable state has a value in [0, MAX_MONEY], because coins only enter as outputs that passed CheckTransaction.
• block_supply — one accepted block raises the total by at most GetBlockSubsidy(height): the coinbase bound of ConnectBlock against the fees, through the acceptance theorem and ApplySpec of the block mission.
• supply_bound (goal) — on every reachable state, totalValue S.utxo + genesisSubsidy ≤ issued S.nextHeight.
• supply_lt_maxMoney — hence totalValue S.utxo < MAX_MONEY on every reachable state.

The genesis subsidy appears on the left because the source never adds the genesis coinbase to the UTXO set (ConnectBlock's genesis shortcut), so it is issued but unspendable; the inequality is exact at the genesis state.

What this rests on

The block mission's acceptance (the executable validation accepts iff the declarative specification holds), apply_spec (the resulting state is ApplySpec), reachable_wellFormed (distinct ledger keys), and the subsidy mission's core_eq_spec and issuance_bound. Nothing about the rules is re-transcribed here; the mission adds the quantities and the induction. (validation.cpp, tx_verify.cpp, coins.cpp)

Why the script interpreter is the heart of consensus

Every Bitcoin transaction input is authorized by running a small stack program: the input's scriptSig followed by the spent output's scriptPubKey, on the same stack, and the spend is valid when the program leaves a true value on top. Nearly every historical consensus failure in Bitcoin touched this interpreter — the disabled opcodes (CVE-2010-5137), the concatenation bug that let any output be spent (CVE-2010-5141), the overflow in numeric opcodes that prompted the four-byte limit, the CHECKMULTISIG off-by-one that consumes an extra element. Bitcoin Core's EvalScript is 800 lines of C++ with a switch over a hundred opcodes, and VerifyScript wraps it with the pay-to-script-hash and witness-program rules. (interpreter.cpp, script.h)

This mission transcribes the legacy execution path (SigVersion::BASE) — the number representation CScriptNum, the truth test CastToBool, the full non-push opcode table of EvalScript with its resource limits, and VerifyScript for output scripts that are neither pay-to-script-hash nor witness programs — and proves the properties the rest of validation relies on: that script numbers round-trip and are minimal, that truth is "nonzero as a number", that the resource limits and the disabled-opcode rule behave as stated, and that the two classic payment templates do exactly what they are meant to.

Numbers, truth, and the machine

A byte is an 8-bit word and a stack element is a list of bytes. A script number is a little-endian magnitude whose last byte's top bit is the sign: $\mathrm{setVch}(v)$ reads it, $\mathrm{serialize}(n)$ writes the shortest such encoding (appending a sign byte when the magnitude's top bit is already set), and the CScriptNum constructor rejects encodings longer than four bytes (five for the lock-time opcodes) and, under MINIMALDATA, non-minimal ones. $\mathrm{castToBool}(v)$ is true when some byte is nonzero, except that a negative zero (0x80 after zero bytes) is false.

A script is the sequence of instructions GetOp yields: a data push carrying its bytes, or a non-push opcode. The interpreter's state is the main stack, the alt stack, the condition stack vfExec, and nOpCount; stacks are lists with the top first. One step on a push checks the 520-byte element limit and pushes when all conditions are true; on an opcode it counts it against the 201-operation limit (only opcodes above OP_16 count, as in the source: OP_1NEGATE, OP_RESERVED and the small-integer pushes are exempt), rejects the fifteen disabled opcodes regardless of execution state, and when executing (or for IF/NOTIF/ELSE/ENDIF always) runs the opcode's case — pushes of small integers, flow control, the stack-manipulation family, EQUAL, the numeric family on four-byte operands, WITHIN, the hash opcodes, CODESEPARATOR, CHECKSIG, CHECKMULTISIG with its key-count accounting, the NOPs, and CHECKLOCKTIMEVERIFY/CHECKSEQUENCEVERIFY when their flags are set — then checks the 1000-element stack limit. Hashes, the lock-time checks, and the signature check (with its encoding rules and FindAndDelete) are an abstract oracle, exactly the role of BaseSignatureChecker and the hash primitives in the source. Running a script steps through it and fails on an unbalanced conditional; verifying evaluates scriptSig then scriptPubKey and requires a non-empty stack with a true top.

Formalization targets

Goal — pay-to-public-key-hash does what it says

for all signatures, keys and hashes within the 520-byte element limit, every flag setting and every oracle. This is BitcoinScript.p2pkh_correct: the template that carries most of Bitcoin's history is correct against the transcribed interpreter, in both directions, with the signature check and hash left abstract. It is the weakest stable statement, since it fixes nothing about the oracle.

Supporting milestones

1. Round-trip (serialize_roundtrip): $\mathrm{setVch}(\mathrm{serialize}(n)) = n$ for every integer.
2. Minimality (serialize_minimal): the serializer's output always passes the minimal-encoding test; (toNum_serialize): a serialized number of at most four bytes is accepted by the strict constructor and reads back as itself.
3. Truth is nonzero (castToBool_iff): $\mathrm{castToBool}(v) \iff \mathrm{setVch}(v) \ne 0$, for every byte string, including both encodings of zero.
4. Pushes (eval_pushes): a push-only script within the element and stack limits leaves exactly its pushes, top-first.
5. Disabled opcodes (disabled_fails): a script containing any of the fifteen disabled opcodes fails from every state, executed or not.
6. Operation limit (op_count_fails): a script with more than 201 counted opcodes (non-push opcodes above OP_16) never succeeds.
7. Pay-to-public-key (p2pk_correct): $\langle sig\rangle$ against $\langle pk\rangle\ \mathtt{CHECKSIG}$ succeeds iff the oracle accepts the signature.

What the result establishes

The goal and milestones give kernel-checked semantics for the pieces of the legacy interpreter that every later layer consumes. The number theorems fix what CScriptNum means on the wire and show the interpreter's own outputs are always minimal — which is why MINIMALDATA can be a policy rule. The truth theorem is what makes VERIFY, IF and the final check well-defined on arbitrary byte strings. The limit and disabled-opcode theorems are the denial-of-service and CVE-2010-5137 defences, stated as universal properties of the transcription rather than of test cases. And the template theorems are the first end-to-end statements that a real Bitcoin spending condition is enforced by the code, modulo the cryptography.

What is deliberately abstract: hash functions, the signature check with its DER/strict-encoding rules and FindAndDelete, and the lock-time checks. These are oracle fields, so every theorem holds for every oracle; instantiating them is the work of the hash, sighash and signature layers. Not modeled: byte-level script parsing (GetOp, MAX_SCRIPT_SIZE), pay-to-script-hash and witness programs in VerifyScript, SegWit v0 and Tapscript execution, and the policy flags (MINIMALDATA, NULLFAIL, CONST_SCRIPTCODE, DISCOURAGE_UPGRADABLE_NOPS, MINIMALIF), which are fixed to off as in block validation.

Status: all statements are open with intentional placeholder proofs. The opcode table has been checked by evaluation against the source's documented stack effects (x1 x2 x3 -- x2 x3 x1 and the like) and the CVE-2010-5137 and limit behaviours; nothing about compiled Bitcoin Core is claimed.

Where the obvious argument fails

The number round-trip looks like bookkeeping until the sign byte: when the magnitude's top byte already has bit 7 set, the serializer appends a whole byte for the sign, and the reader must then see a cleared top bit on that extra byte while the magnitude is unchanged. The proof splits on this case and on the sign, and needs the precise effect of |= 0x80 and & 0x7f on bytes below 128. Minimality has the matching trap: the serializer never emits a trailing zero magnitude byte, which is what makes its output pass the test.

For the templates, the naive approach is to compute. It works, but only after the interpreter's resource checks are discharged on every step — the element size on each push, the op count on each opcode, the stack size after each step — which is why the template theorems carry element-size hypotheses and why the push lemma is stated with its limits. For the op-count theorem the trap is CHECKMULTISIG, which adds its key count to nOpCount mid-execution; the invariant has to allow that increase while keeping it under the limit.

Formalization scope

Bytes are BitVec 8; numbers are Int with natAbs for the magnitude; bit tests are the source's masks (& 0x80, & 0x7f, | 0x80) read through toNat. Stacks are Lists, top first; the stacktop(-k) indexing of the source becomes position $k-1$. Scripts are List Instr. execOp is one if-chain mirroring the switch; step performs the per-iteration checks in the source's order; run is the loop plus the final conditional check; evalScript returns the main stack. Flags carries CHECKLOCKTIMEVERIFY, CHECKSEQUENCEVERIFY and NULLDUMMY; fRequireMinimal is false. The oracle's checkSig returns none where an encoding check fails the whole script and some b for the signature verdict.

A trivializing formalization would define verifyScriptPlain on the two templates directly, or let the oracle see the script; the interpreter is the full opcode table and the oracle sees only the stack elements it is handed. Restricting the templates to canonical sizes beyond the 520-byte limit is out of scope.

No Mathlib is required; the development imports only Std. Proofs in any order are welcome; lemmas about individual opcodes' stack effects are reusable for every later script theorem.

Selected references

• Bitcoin Core contributors. EvalScript, VerifyScript, CastToBool, EvalChecksigPreTapscript, src/script/interpreter.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. Source
• Bitcoin Core contributors. CScriptNum, opcode table, MAX_SCRIPT_ELEMENT_SIZE, MAX_OPS_PER_SCRIPT, MAX_STACK_SIZE, MAX_PUBKEYS_PER_MULTISIG, src/script/script.h, and GetScriptOp, src/script/script.cpp, same revision. Source
• Pieter Wuille. BIP62: Dealing with malleability (rules 3–6, minimal data and numbers), 2014. Specification
• Satoshi Nakamoto. Bitcoin: A Peer-to-Peer Electronic Cash System, 2008, section 2. Paper

Why the header clock matters

Bitcoin has no trusted clock. A block's timestamp is chosen by its miner, so the consensus rules constrain it from two sides: it must exceed the median time past of the previous eleven blocks (time-too-old), and it must not run more than two hours ahead of the validating node's own clock (time-too-new). The median, rather than the previous block's time, is what makes the rule robust to a few manipulated timestamps, and since BIP113 the same median is the clock against which time-based lock-times are evaluated. The remaining contextual header rules fix the required difficulty bits and refuse block versions that predate the BIP34, BIP66 and BIP65 soft forks once those are active. (GetMedianTimePast, ContextualCheckBlockHeader, CMainParams)

One property of this design is used everywhere but stated nowhere in the code: along any chain that obeys time-too-old, the median time past never decreases. It is what makes a time-based lock, once satisfied, stay satisfied. This mission transcribes the median and the contextual rules and proves that property.

The median, the window, and the rules

A chain of ancestors is represented by the list of its block times, most recent first. The window is the first eleven entries (nMedianTimeSpan), or all of them for a shorter chain. The median time past sorts the window and takes the element at index $\lfloor |w| / 2 \rfloor$; for an even-length window this is the upper of the two middle elements, as the source's pbegin[(pend - pbegin) / 2]. For an empty chain the model returns $0$, a case the source never queries.

A header carries a version, a time and nBits. For a buried deployment, DeploymentActiveAfter(prev) holds when $\mathrm{prev.height} + 1$ reaches the activation height: $227{,}931$ for BIP34, $363{,}725$ for BIP66, $388{,}381$ for BIP65. The version floor rejects a version below 2, 3 or 4 when the corresponding deployment is active. The contextual check of a header against its predecessor requires: nBits equals the required work (supplied by the caller, as GetNextWorkRequired computes it in the proof-of-work development); the time strictly exceeds the predecessor's median time past; the time is at most the local clock plus $7{,}200$ seconds; and the version is not outdated. Mainnet has enforce_BIP94 = false, so the testnet timewarp rule is absent.

Formalization targets

Goal — median time past is non-decreasing along a valid chain

For a chain of block times $t_0, t_1, \dots$ (most recent first) in which every block satisfies time-too-old against its predecessor — $\mathrm{MTP}(t_{i+1}, t_{i+2}, \dots) < t_i$ for every $i$ — the median time past of every suffix is at most that of every shorter suffix:

This is BitcoinHeader.mtp_mono_chain. It is the clock-monotonicity that BIP113 and BIP68 time locks rely on.

Supporting milestones

1. Window membership (mtp_mem_window, mtp_mem): for a non-empty chain the median is one of the window's times, hence one of the chain's.
2. Bounds (mtp_bounds): the median lies between any lower and upper bound of the window.
3. Only eleven matter (mtp_take): the median of a chain equals the median of its first eleven times.
4. One step (mtp_mono): if $\mathrm{MTP}(c) < t$ then $\mathrm{MTP}(c) \le \mathrm{MTP}(t :: c)$. The heart of the goal, by a counting argument on the sorted window.
5. Version floor (versionOutdated_iff): the rejection condition as a disjunction of height thresholds.
6. The contextual check (contextualCheck_iff): acceptance as a conjunction of the four rules.
7. Floors after activation (version_floor): an accepted header has version at least 2, 3, 4 after the respective heights.

What the result establishes

The goal is a kernel-checked statement about the transcribed median: appending blocks that pass time-too-old can only move the median forward. Together with the characterization of the contextual check it gives the exact semantics of Bitcoin's block clock: bounded from below by a non-decreasing median, from above by local time plus two hours.

Formalizing adds the general proof of a fact usually argued by example. The argument is a counting one: the median of a window of $n$ sorted times is the smallest value with at least $n - \lfloor n/2 \rfloor$ window elements at or above it; appending a time above the old median and dropping at most one old element keeps that count high enough, including when the window is still growing in the first ten blocks of a chain.

Not in scope, and stated as such: the computation of the required nBits (the proof-of-work mission), the local-clock model behind NodeClock::now(), checkpoints, minimum chain work, and the CheckBlockHeader proof-of-work test itself. Status: all statements are open with intentional placeholder proofs.

Where the obvious argument fails

The naive argument — "the new time is larger than the median, so the median cannot fall" — overlooks that the window also loses its oldest element, which may have been one of the elements above the median. The proof must show that losing one such element and gaining one keeps at least $n - \lfloor n/2 \rfloor$ elements at or above the old median. A second subtlety is the growing window: for the first ten blocks the window length increases by one and the median index may move, so the count required changes from $n - \lfloor n/2 \rfloor$ to $(n+1) - \lfloor (n+1)/2 \rfloor$; the two cases are not the same inequality. The even-length convention (upper middle) is what makes the bookkeeping close.

Formalization scope

Times are Int, as int64_t block times. The window is List.take 11, the sort is List.mergeSort on ≤, and the median is getD (length / 2) 0. The required nBits is a parameter of the check. Heights are Nat. enforce_BIP94, checkpoints and minimum chain work are not modeled.

A trivializing formalization would define the median as the previous block's time, or sort with a different index convention; the definitions follow the source's sort-and-index. Assuming the chain's times are themselves sorted is ruled out: the goal assumes only the time-too-old rule.

No Mathlib is required; the development imports only Std. The counting lemmas on sorted lists are reusable for any later median-based rule.

Selected references

• Bitcoin Core contributors. CBlockIndex::GetMedianTimePast, src/chain.h at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. Source
• Bitcoin Core contributors. ContextualCheckBlockHeader, src/validation.cpp, same revision. Source
• Bitcoin Core contributors. DeploymentActiveAfter, src/deploymentstatus.h, and CMainParams activation heights, src/kernel/chainparams.cpp, same revision. Source
• Thomas Kerin, Mark Friedenbach. BIP113: Median time-past as endpoint for lock-time calculations, 2015. Specification
• Gavin Andresen. BIP34: Block v2, Height in Coinbase, 2012; Pieter Wuille. BIP66: Strict DER signatures, 2015; Peter Todd. BIP65: OP_CHECKLOCKTIMEVERIFY, 2014. BIPs

Why relative lock-time matters

Bitcoin nodes must agree on whether a transaction may spend its inputs yet. Since 2016 that decision includes relative lock-time: an input may declare that the output it spends must have been confirmed for a minimum number of blocks or a minimum elapsed time before it becomes spendable. The rule is defined by BIP68 and enforced on mainnet by three helper functions in Bitcoin Core: CalculateSequenceLocks, EvaluateSequenceLocks, and SequenceLocks (pinned source). Payment channels, atomic swaps, and vault constructions depend on this rule to enforce dispute windows; a node that decodes a sequence word differently from its peers can accept or reject a block the rest of the network treats the other way.

The specification is short and the implementation is about seventy lines, yet the two are written in different languages. BIP68 speaks of bits, masks, and elapsed delays; the implementation folds inputs into two signed thresholds compared against the candidate height and its ancestor's median time. Whether these agree, for every 32-bit sequence word and every input list, is the question this mission settles. Absolute lock-time (nLockTime) already has a Lean treatment in btc-verified, whose consensus documentation lists BIP68 as outstanding work.

Sequence words, inputs, and contexts

An input is a pair $(s, c)$: an unsigned 32-bit sequence word $s$ and the coin height $c \in \mathbb N$ of the output being spent. A context is a pair $(H, M)$: the candidate block height $H \in \mathbb N$ and a total function $M : \mathbb N \to \mathbb N$ giving the median time past of each ancestor height. Write $h^- = \max(h-1, 0)$; natural-number subtraction in Lean truncates at zero and realizes this directly.

Three fields of $s$ matter. The disable bit $D$ is bit 31. The type bit $T$ is bit 22: set means a time-based lock, clear means a height-based lock. The delay $d = s \bmod 65536$ is the low sixteen bits; for a time lock it denotes $512d$ seconds. Enforcement $E$ holds when the transaction version is at least 2 and bit 0 of the validation flags is set.

The declarative model (BIP68_Model) expresses these as arithmetic on $s$ viewed as a natural number: $D \iff \lfloor s / 2^{31} \rfloor = 1$, $T \iff \lfloor s / 2^{22} \rfloor \bmod 2 = 1$. A single input is satisfied when

A transaction satisfies BIP68 when $\neg E$ or every input is satisfied. The model also fixes the expected height list: each input's coin height, replaced by $0$ exactly when $E$ holds and $D$ is set.

The Core transcription (BIP68_Core) uses bit-vector masks 0x80000000, 0x00400000, 0x0000ffff and a left shift by 9. An accumulator holds two signed thresholds $(a, b)$ and a reversed height list, starting at $(-1, -1, [\,])$. Each enabled, non-disabled input updates $b \leftarrow \max(b,\ M(c^-) + 512d - 1)$ for a time lock or $a \leftarrow \max(a,\ c + d - 1)$ for a height lock. Evaluation succeeds when $a < H$ and $b < M(H^-)$. When $E$ is false, the fold is skipped and the original heights are returned.

Formalization targets

Goal — helper correctness

Under the admissible domain ($0 < H \le 2^{31}-1$, every $c \le H$, every $M(h) \le 2^{63}-1$ for $h \le H$) and the no-overflow condition (for every enforced, non-disabled input, the sum selected by $T$ fits its signed destination before the subtraction of one),

and the height list returned by the fold equals the expected height list. This is BitcoinBIP68.core_correct.

Supporting milestones

1. Decoding (decode_sequence): for every 32-bit word, the mask tests agree with the quotient-and-remainder tests, the masked delay equals $d$, and the shifted seconds equal $512d$. No hypothesis on unused bits.
2. Fold acceptance (fold_acceptance): for any starting accumulator, evaluating the fold succeeds iff evaluating the starting accumulator succeeds and every input is satisfied. No range or monotonicity assumptions.
3. Height vector (height_vector): the returned list has the original length and order, with zeroes exactly at enforced, disabled inputs, including repeated entries and the empty list.
4. Threshold bounds (calculated_bounds): under admissibility and no-overflow, $-1 \le a \le 2^{31}-1$ and $-1 \le b \le 2^{63}-1$, preserving the $-1$ sentinel.

What the result establishes

The goal is a kernel-checked statement that a Lean transcription of the pinned Core helpers decides exactly the BIP68 spending condition on the admissible domain, and that its side effect on the per-input height list is the one BIP68 describes. Both directions matter: a lock the implementation accepts is one the specification accepts, and a lock the specification accepts is one the implementation accepts.

Formalizing it adds three things beyond the prose specification. It makes the overflow preconditions explicit, which BIP68 leaves implicit and Core leaves to callers. It separates the bit-level decoding (a bv_decide-style fact) from the aggregation logic (an induction over the input list), so each can be audited on its own. And it produces reusable definitions — Input, Context, the admissibility and overflow predicates — for a later whole-block validation development in which the caller obligations (supplying coin heights, ancestor clocks, activation flags, and coinbase exclusion) are discharged.

Status: the statements compile with intentional sorry placeholders and have independent read-backs. Differential checks ran 2,014 cases against extracted Core helper bodies; these test the transcription, not the theorems. No proof of any statement is claimed.

Where the obvious argument fails

The natural first idea is to prove core_correct by unfolding everything and calling a decision procedure. It fails because the two sides live in different arithmetic. The implementation computes thresholds in signed integers after subtracting one; the specification compares unsigned sums with $\le$. The equivalence $a < H \iff \max_i (c_i + d_i - 1) < H$ holds only because the $-1$ sentinel is below every admissible height and because each $c_i + d_i - 1$ is formed without wrap-around. Both facts need the admissibility and no-overflow hypotheses, and the proof must thread them through the fold.

A second trap is the disabled input. In the model, a disabled input is satisfied unconditionally; in the fold, it leaves both thresholds unchanged but still appends $0$ to the height list only when enforcement is on. height_vector records this asymmetry; a proof that treats disabled inputs as absent gets the height list wrong.

A third is the median-time function. $M$ is arbitrary: not monotone, not bounded outside $[0, H]$. The theorems are stated for this weaker model deliberately, so any proof that assumes a well-formed chain is proving a different statement.

Formalization scope

The development commits to the following conventions, all fixed in BIP68_Model and BIP68_Core. Sequence words, versions, and flags are BitVec 32. Heights and times are Nat in the model and Int in the accumulator. $h - 1$ on Nat truncates at zero, matching max(h-1, 0) in the source. Input lists are finite Lists; the empty list is in scope. The predicates specEnabled, specDisabled, and specTimeBased are Prop with decidability instances; the Core-side tests are Bool. Admissibility and no-overflow are the only hypotheses on core_correct; fold_acceptance and height_vector carry none.

A trivializing formalization would define satisfiesBIP68 by calling sequenceLocks; the model is written independently from the BIP text and must stay that way. Weakening the no-overflow hypothesis to a vacuous one, or restricting to nonempty lists, is out of scope.

Dependencies: Lean 4 core and Std only; no Mathlib. The two definitions are published first and imported by every theorem. Proofs of the four milestones in any order are welcome, as are lemmas on coreStep reusable by the goal. Out of scope: the C++-to-Lean correspondence (documented, not proved), coinbase exclusion, activation selection, and block-level composition, which belong to a separate whole-consensus mission that will import these results.

Selected references

• Mark Friedenbach, BtcDrak, Nicolas Dorier, kinoshitajona. BIP68: Relative lock-time using consensus-enforced sequence numbers, Bitcoin Improvement Proposals, 2015. Specification
• Bitcoin Core contributors. CalculateSequenceLocks, EvaluateSequenceLocks, SequenceLocks, src/consensus/tx_verify.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. Source
• Bitcoin Core contributors. Mainnet validation and parameters, same revision. validation.cpp, chainparams.cpp
• ProofOfKeags contributors. btc-verified: absolute lock-time in Lean 4, revision 2fdeb40c. LockTime.lean, consensus coverage
• Lean FRO. Bitvectors, Lean Language Reference. Documentation

Why the Merkle root and its mutation check matter

A Bitcoin block header commits to its transactions through a single 32-byte Merkle root: the transaction hashes are paired and hashed, the results paired and hashed again, until one hash remains. Every node recomputes this root from the block body and rejects the block if it does not match the header. Bitcoin's construction has a quirk that later became a vulnerability: when a level has an odd number of hashes, the last one is duplicated before pairing. Consequently the transaction lists $[1,2,3,4,5,6]$ and $[1,2,3,4,5,6,5,6]$ have the same root, and an attacker could relay the second, invalid, block with the first block's header; a node that marked that header permanently invalid would then reject the genuine block (CVE-2012-2459). Bitcoin Core defends by detecting, at every level, two equal adjacent hashes in an aligned pair and treating the block as having a bad root. (ComputeMerkleRoot and the comment above it.)

This mission transcribes that loop and proves that the defence does what its comment claims for the general form of the construction: duplicating any aligned block of $2^k$ trailing leaves preserves the root and is detected, at the level where that block has collapsed to one node.

The loop, as a function on lists

Hashes are an arbitrary type $H$ with decidable equality; the pairwise hash is an abstract $c : H \times H \to H$ (in the source, SHA256D64 on the two concatenated hashes), and the zero hash returned for an empty list is an abstract $z$. The three operations are, for a list of hashes $\ell$:

• pairUp$(\ell)$: $c$ applied to successive aligned pairs; an odd trailing element $a$ contributes $c(a, a)$. This is hashes.push_back(hashes.back()) followed by the pairwise hashing.
• hasEqualPair$(\ell)$: true when some aligned pair $(\ell_{2i}, \ell_{2i+1})$ with $2i + 1 < |\ell|$ consists of equal hashes. The duplicated trailing element is not tested: the check runs before the duplication.
• rootLoop$(\ell, m)$: while $|\ell| > 1$, replace $m$ by $m \lor \mathrm{hasEqualPair}(\ell)$ and $\ell$ by $\mathrm{pairUp}(\ell)$; on exit return the single remaining hash (or $z$ if the list is empty) together with $m$.

computeMerkleRoot$(\ell) = \mathrm{rootLoop}(\ell, \mathtt{false})$ returns the pair (root, mutated), exactly as ComputeMerkleRoot(hashes, &mutated).

Formalization targets

Goal — duplication of an aligned block is root-preserving and detected

For every $k$, every non-empty prefix $\ell$ whose length is a multiple of $2^{k+1}$, and every block $t$ of exactly $2^k$ hashes,

This is BitcoinMerkle.dup_block. The alignment hypotheses are what make $t$ collapse to a single node at level $k$, where the duplicate then sits in an aligned pair; $\ell \ne [\,]$ is needed because a list of one hash is its own root while a list of two is not. With $k = 0$ it is the classic duplicated-last-transaction case; with $k = 1$ it is the $[1,\dots,6,5,6]$ example of the source comment.

Supporting milestones

1. Base cases (root_nil, root_single, root_pair): the empty list gives $(z, \mathtt{false})$; one hash gives $(a, \mathtt{false})$; two give $(c(a,b),\ a = b)$.
2. Flag independence (rootLoop_fst): the root does not depend on the incoming flag.
3. Flag is sticky (rootLoop_sticky): once set, the flag stays set through the remaining levels.
4. One level distributes over an even split (pairUp_append_even, hasEqualPair_append_even): for $|\ell|$ even, $\mathrm{pairUp}(\ell \mathbin{+\!\!+} r) = \mathrm{pairUp}(\ell) \mathbin{+\!\!+} \mathrm{pairUp}(r)$ and likewise for the pair test.
5. Leaf-level case (dup_leaf): the goal at $k = 0$, stated directly.

What the result establishes

The goal is a kernel-checked statement about the transcribed loop: for the entire family of duplications that CVE-2012-2459 is built on, the root is unchanged and the mutation flag is raised. Together with the base cases it fixes the exact semantics of the odd-level rule and of the check, including the fact that the self-pairing of a duplicated trailing element is never itself flagged.

What the result does not say is also worth stating. It does not claim that every root collision is detected; that would require assumptions on the hash function (the source comment says "assuming no double-SHA256 collisions"), and $c$ is here an arbitrary function. Nor does it claim anything about the byte-level SHA256D64 or about transaction serialization; those belong to the hash and serialization layer. What formalizing adds is the general $k$ statement with its precise alignment conditions, which the source states only by example.

Status: all statements are open with intentional placeholder proofs. Nothing about compiled Bitcoin Core is claimed.

Where the obvious argument fails

The natural first attempt is to compute both sides for small lists and generalize. It fails on the $k$-level statement because the two lists differ in length by $2^k$ and go through $k$ levels before the duplicate appears as a pair. The argument has to track two facts through the loop at once: that the root is insensitive to the flag (so the two runs can be compared level by level with different flags), and that the flag, once raised at level $k$, survives to the end. Both are separate milestones for that reason.

The alignment hypotheses are the second trap. Without $2^{k+1} \mid |\ell|$ the block $t$ straddles a pair boundary and its two copies do not collapse to equal nodes; without $|t| = 2^k$ the copies collapse at different levels. The theorem is false without them, and the base case $\ell = [\,]$ shows that non-emptiness is needed too.

Formalization scope

$H$ is a type parameter with DecidableEq; $c$ and $z$ are parameters. Lists are Lean Lists, so pairUp and hasEqualPair are structurally recursive, and rootLoop is defined by well-founded recursion on the list length with the lemma $|\mathrm{pairUp}(\ell)| = \lceil |\ell| / 2 \rceil$ supplied in the definition file to justify termination. Equality in hasEqualPair is decide (a = b) on $H$, matching hashes[pos] == hashes[pos + 1] on uint256. The mutated pointer being null in the source (as in BlockWitnessMerkleRoot) only suppresses the output; the model always computes the flag.

A trivializing formalization would restrict $H$ to a type with a trivial hash or define the root by a different, non-duplicating rule; the definitions are fixed to the source's loop. Out of scope: MerkleComputation (Merkle branches), BlockMerkleRoot's leaf extraction, the witness root's zero coinbase leaf, and any collision-resistance assumption on $c$.

No Mathlib is required; the development imports only Std. Proofs of milestones in any order are welcome, and the distribution lemmas are reusable by any later Merkle-branch work.

Selected references

• Bitcoin Core contributors. ComputeMerkleRoot, src/consensus/merkle.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48, lines 16–73 including the CVE-2012-2459 comment. Source
• Forrest Voight. CVE-2012-2459: Bitcoin block Merkle root duplication, 2012. Advisory
• Satoshi Nakamoto. Bitcoin: A Peer-to-Peer Electronic Cash System, 2008, section 7. Paper

Why the issuance schedule matters

Every Bitcoin block may create new coins through its coinbase transaction, and the amount it may create is fixed by consensus: a block subsidy that starts at fifty bitcoin and halves every 210,000 blocks, plus the fees of the block's other transactions. The schedule is the mechanism behind the often-quoted cap of twenty-one million bitcoin, yet the cap appears nowhere in the code as a rule. What the code enforces is the per-block subsidy, computed by GetBlockSubsidy in validation.cpp, and the check in ConnectBlock that the coinbase pays no more than fees plus subsidy. The cap is a consequence, and the only place a number near it appears is MAX_MONEY, a sanity bound on individual amounts whose comment says explicitly that it is "not the total money supply". (GetBlockSubsidy, amount.h, CMainParams)

This mission makes the consequence a theorem about the pinned implementation: the sum of the subsidies of all blocks, at every height the chain can reach, is strictly below MAX_MONEY, and in fact equals a specific constant once the subsidy reaches zero. It is the arithmetic core of the ledger-supply results that a whole-consensus development will need, and it is small enough to be verified completely.

The subsidy function and its schedule

Amounts are counted in satoshi. One bitcoin is $\mathrm{COIN} = 10^8$ satoshi and $\mathrm{MAX\_MONEY} = 21{,}000{,}000 \cdot \mathrm{COIN}$. The mainnet halving interval is $I = 210{,}000$ blocks.

The Core subsidy at height $h \in \mathbb N$ is the transcription of GetBlockSubsidy: with $k = \lfloor h / I \rfloor$ the number of halvings, the subsidy is $0$ if $k \ge 64$, and otherwise $(50 \cdot \mathrm{COIN}) \gg k$, the right shift of the initial subsidy by $k$ bits. Heights are nonnegative integers in the source, and the shift acts on the nonnegative value $50 \cdot \mathrm{COIN}$, so natural numbers represent both exactly. The explicit halvings >= 64 branch exists because a shift by 64 or more is undefined in C++.

The declarative schedule is $\mathrm{specSubsidy}(h) = \lfloor 50 \cdot \mathrm{COIN} \,/\, 2^{\lfloor h/I \rfloor} \rfloor$: fifty bitcoin, halved once per interval with the remainder discarded.

Issuance below height $n$ is the running sum of Core subsidies, $\mathrm{issuedBelow}(0) = 0$ and $\mathrm{issuedBelow}(n+1) = \mathrm{issuedBelow}(n) + \mathrm{coreSubsidy}(n)$. The interval sum $\mathrm{intervalSum}(m) = \sum_{j < m} \lfloor 50 \cdot \mathrm{COIN} / 2^j \rfloor$ collects one subsidy per interval. The zero height is $33 I = 6{,}930{,}000$.