# lean-dag — Equivocation, growth, and denial of service > **Provenance.** Code and prose in this project were co-written with > heavy LLM assistance. The Lean proofs are machine-checked — the kernel > verifies every theorem against its stated form — but whether the > definitions and theorem statements capture their *intended* meaning, > and whether the surrounding prose is faithful to what is proved, has > only human-plus-LLM review behind it. Read critically. The denial-of-service extension of the development. Safety and liveness (`spec.md`, `liveness.md`) already hold under equivocation — `no_equivocation` constrains correct validators only, and every result is stated against a universe in which Byzantine validators may publish as many blocks per round as they like. What they do not address is **storage**: Byzantine validators flood the DAG, and correct validators must fetch, validate and retain a view that grows without bound. This document describes the machinery that rules that out: a validity condition (`DoSValid`), exact bounds on the size of a block's causal history, and an acceptance-layer budget (the *novelty budget*) under which liveness and linear storage hold simultaneously — from round 0, under full asynchrony, from hypotheses a validator can enforce without ever knowing who is Byzantine. The headline results, each developed below and mapped to Lean in §8: - **Theorem A** (§5). Under the DoS validity condition, every valid block's causal history is **linear in its round**: `|H(b)| ≤ (n + (n−1)·f^f)·(r+1)` — and the constant's exponential shape is optimal in the bare model: a lower-bound family exists whose doubling step is machine-checked. - **Theorem B** (§6). Validators that cap the download per acceptance (the novelty budget) and reference only what they accepted get **liveness and linear storage simultaneously**, from round 0, under full asynchrony — and every rule involved is author-blind. - **B5** (§6). Under both conditions together, the Byzantine share of storage **stops growing** once every equivocator has been exposed. - **No amplification** (§4, §6). A correct validator's relay duty is its own blocks plus their budget-priced cones, and nothing else — floods die at the acceptance gate. > **Status.** Everything below is proved in Lean — no `sorry`, axioms > `propext`, `Classical.choice`, `Quot.sound` only — and witnessed on > concrete models by `decide`. §8 is the index, mapping every result to its > Lean name and file. Result labels (D…, B…, C…, S…) are stable identifiers > cited by the Lean sources. ## Overview — the two conditions, and the two main theorems A self-contained summary. Everything used here is defined from scratch; §1–§7 develop it, and §8 maps every result to its Lean name. **The setting.** There are `n ≥ 3f+1` **validators**, of which at most `f` are **Byzantine**; the rest are **correct**. (The concrete witnesses all instantiate the boundary `n = 3f+1`, where every constant below takes its familiar form.) The protocol proceeds in numbered **rounds**. A **block** `b` carries an author (its *creator*), a round, and a finite set of **references** to earlier blocks. A block is **valid** when 1. every reference points to a block of the round exactly below; 2. its references carry pairwise distinct authors; 3. they carry at least `n − f` distinct authors — a **quorum** (at `n = 3f+1`, the familiar `2f+1`); and 4. one of them is by `b`'s own author — the **self-parent** — so every author's blocks chain back to round 0. Correct validators author at most one block per round; a Byzantine validator may **equivocate** — author several blocks at one round. The universe `U` is every block some correct validator ever held, so `|U|` is the storage burden on the correct population; blocks revealed to nobody impose none. From what arrives, each validator **accepts** at most one block per author per round — its *accepted set* — and builds its next block by referencing its latest acceptances. The central quantity is a block's **cone** (causal history): `H(b)` is `b` together with everything reachable from it through references, and `|H(b)|` is what a validator must fetch and validate in order to accept `b`. A validator's **view** `V` is the union of the cones of the blocks it accepted, so views reduce to cones: `|V| ≤ n · max |H(b)|` (D2). Absent any further condition, `|H(b)|` can grow *exponentially* in the round: each block may name `f` fresh Byzantine blocks one round down, and the branching compounds level by level. **Notation**, fixed for the whole document. `n` — the number of validators, `n ≥ 3f+1`; `f` — the fault bound; quorum threshold `n − f`; `r` — a block's round; `t` — a schedule round, at which a validator's state is measured; `H(b)` — the cone of block `b`; `V_v(t)` — validator `v`'s retained view at round `t` (Lean `viewUpto`); `U` — the universe of blocks correct validators held; `e` — the number of exposed authors in a cone; `R` — the eventual-synchrony stabilization round; `T` — the enforced acceptance budget, `κ` its analysis-side counterpart (every theorem composes with `κ := T`), and `Κ = f·κ + 1` — the derived threshold at which correct blocks always lie within the budget. `|S|` is the size of a finite set. **Condition 1 — DoS validity.** Say author `X` is **exposed** in `H(b)` when the cone contains two `X`-blocks at one round — an equivocation made visible. The condition: > a block may not reference an author who is exposed in its own cone. Exposure is objective (any two validators compute it alike, D13), permanent along references (D12), and *is* the damage rather than a report of it (D11): an author's equivocation either inflates nobody's cone, or exposes the author — and then exclusion is automatic and forever. A correct author is never exposed (D15), so the condition never blocks a correct validator. **Theorem A — the bare-model bound** (§5; `card_history_le'` with `card_history_ge`). Under validity and DoS validity, every block `b` at round `r` satisfies > `(n−f)·r + 1 ≤ |H(b)| ≤ (n + (n−1)·f^f) · (r+1)`. Linear in `r` at every fault budget — the compounding is gone — with a per-round, per-author constant `1 + (n−1)·f^(f−1)` (C1′); at `n = 3f+1`, `f = 1` the ceiling is exactly `7(r+1)`. The constant's exponential shape is **final, not slack**: with `e` exposed authors, an author can lawfully run `2^(e−2)` chains through one cone — a family constructed against every proved constraint, its doubling step machine-checked (`Udouble`, §5) — against a proved ceiling of `(n−e)·e^(e−1)`. Exponential in `e` from both sides, so no rule keyed on the *shape* of cones can bring the constant down to a polynomial in `f` — which is what forces Condition 2 to price something an adversary cannot shape away. **Condition 2 — the novelty budget.** Measure an arriving block not by its cone but by what its cone would *newly* bring. Against a validator's current store `V`, the **novelty** of `b` is `H(b) \ V` — precisely the download performed to validate `b`, so the measurement is the work itself. It is antitone in `V`: as the store grows, every block's novelty only shrinks. The enforced rule (`UniformBudget T`, for a parameter `T`): > never accept a block whose novelty exceeds `T` blocks; defer it instead > — the store grows, and the block is re-priced later. together with the **reference discipline** (`RefsAccepted`): a block references exactly what its author accepted. Real DAG protocols do both. The rule is **author-blind** — nothing in it consults who is Byzantine — and once the network delivers reliably (after the stabilization round `R`) it never defers a correct block: a correct block's cone is a complete record of its author's acceptances (the DAG is its own repair channel, C3′), so a correct block can then never cost another correct validator more than `f·T + 1` (C3″) — a *derived* threshold, not an assumed one. **Theorem B — DoS resistance** (§6; `dos_resistance`). Assume correct validators build once they hold a quorum (`Live`), the network eventually puts a quorum in every correct validator's hands whenever one exists (`DeliversQuorum`), and correct validators enforce the budget and the reference discipline. Then, simultaneously: > **liveness** — no correct validator ever stalls: each has a block at > every round, to the horizon of the growth assumption; and > **linear storage** — every correct validator's view at round `t` obeys > `|V_v(t)| ≤ |Correct|·(t+1) + |Correct|·f·(1 + t·T)`, from round 0, under full asynchrony — no global stabilization time appears in either hypothesis or conclusion, and no rule a validator runs consults an identity. The proof's engine: every Byzantine block in any correct view entered through *some* correct validator's budgeted acceptance, so the global Byzantine pool grows by at most `|Correct|·f·T` per round (B4). The adversary's hidden mass is thereby repriced rather than forbidden: a `2^e`-block reveal must trickle through `T`-sized acceptances, taking exponentially many rounds to place, while correct storage grows linearly throughout. **No amplification.** A consequence worth stating on its own: a correct validator's entire outbound obligation is to publish its own block and serve that block's cone — which is, transitively, exactly its accepted set. Liveness consumes nothing else: no theorem ever requires a Byzantine block that no correct validator accepted to move anywhere, and everything held-but-never-accepted may be dropped with no effect. Since acceptance is budget-priced, the obligation is bounded — at most `f·T + 1` blocks per peer when a new block lands post-`R` (C3″), linear cumulatively (B4, no synchrony needed) — so correct validators **dampen floods rather than relay them**: the acceptance decision is the amplification gate (§4, §6). Theorem B does not assume Condition 1 — the budget is a standalone defense — but the two compose (**B5**, §6): the budget alone bounds the Byzantine share of a view by a *rate*, `|Correct|·f·T` per round, sustained forever; under both conditions that term **stops growing** the moment every Byzantine author has been exposed, and the view bound's slope decays to the correct-production rate `|Correct|` per round, the Byzantine part frozen at `|Correct|·f·(1 + (m+1)·T)` for `m` the round exposure completed. Read together: exclusion makes Byzantine damage **one-shot per author** (C2), Theorem A bounds what one shot can weigh inside the DAG, Theorem B bounds what any schedule of shots can cost a correct validator, and B5 says the cost *ends* once the authors are caught — all from conditions each validator can enforce alone, without ever knowing who is Byzantine. ## 1. The threat, and the two measures `liveness.md` §4.2 fixes `U` as *every block some correct validator ever held* — not every block anyone ever wrote. So `|U.ids|` is the storage burden imposed on the correct population, and a block revealed to nobody adds nothing to it. Two quantities measure the burden: - **View size.** `V.ids` is a `Finset`; `|V.ids|` is what a validator stores. Views are downward closed, so a view with maximum round `r` spans rounds `0…r`. - **History size.** `H(b) := {c | Reaches U b c}` — the causal cone of `b`. `|H(b)|` is what a validator must fetch and validate in order to accept `b`, and it is the quantity the attack inflates. §2 reduces the first to the second; §5 bounds the second; §6 bounds both at the point of acceptance. A third quantity, **bandwidth** — blocks received, inspected and discarded — is invisible to the model: `U` records what was *held*, and there is no notion of a message. Every bound here is about storage; the wire-level cap on candidates held is the one piece that lives at the network layer (§9). ## 2. The acceptance rule, and view size from history size The rule: *a correct validator accepts at most one block per author at its latest round, and its view is the causal history of what it accepts.* ```lean structure Accepted (U) (A : Finset BlockId) (n : ℕ) : Prop where subset_ids : A ⊆ U.ids round_eq : ∀ i ∈ A, (U.block i).round = n -- one round: the frontier inj : ∀ i ∈ A, ∀ j ∈ A, creator i = creator j → i = j ``` `A` is the **frontier**; earlier rounds enter the view inside the histories, which is what makes `|A| ≤ n` rather than `n(r+1)`. The set is not invented for the size bound: the delivery layer needs it independently (`Delivery.accepted`, §7 S2/S5), and `accepted_inj` there is exactly the injectivity D2 consumes. - **D1 — a generated view is a view.** `A.biUnion (history U)` is downward closed, because a union of causal histories is. No closure obligation is discharged by hand. - **D2 — the bridge.** `|V| ≤ n · max_{b ∈ A} |H(b)|`. Unconditional: no DoS condition, no synchrony, no correctness hypothesis. - **D3 — the sharp form.** When the validator references everything it accepted, `H(b) = {b} ∪ V`, so `|V| = |H(b)| − 1`. The exposure clause of §3 can make `refs` a proper subset; then D2 is the operative bound. - **D4 — generated views grow**, provided each block references its own previous one — which validity now demands of every block (S10). The principle that keeps both D3's failure mode and D4 harmless: **exclusion governs what you reference, not what you retain** (§7 S1). What the rule must *not* be read as claiming: `V ≤ n(r+1)` "by construction". A round-`r` block by `w` may reference the other half of an equivocation than the one this validator accepted, so `V` holds both. The rule gives the reduction to `|H(b)|`, not the bound — the bound is §5 and §6. ## 3. The DoS validity condition > If a block's history contains an equivocation by validator `X`, then `X` > may not be used as one of that block's references. ```lean /-- `X` is exposed in `b`'s history: two distinct blocks by `X`, one round. -/ def ExposedIn (U) (b : BlockId) (X : Validator) : Prop := ∃ i j, Reaches U b i ∧ Reaches U b j ∧ i ≠ j ∧ creator i = X ∧ creator j = X ∧ round i = round j def DoSValid (U) : Prop := ∀ b ∈ U.ids, ∀ i ∈ (U.block b).refs, ¬ ExposedIn U b (U.block i).creator ``` **A predicate on the universe, not a field of `ValidWrt`.** As a separate predicate, every safety and liveness theorem applies verbatim, and the DoS results take `(hdos : DoSValid U)` as an extra hypothesis — the condition is available in both regimes at no migration cost. **Well founded**: the condition on `b` depends only on the histories of `b`'s references, since `b` is the only block of `H(b)` at its own round. **Constructible**: as a building rule it converges — drop references naming exposed authors, recompute; dropping only shrinks the history, exposure is monotone, so the iteration terminates within `f` rounds and always retains every correct reference (a correct author is never exposed, D15). A correct validator can always build. The three facts that make it a *validity* condition: - **D11 — inflation is exposure.** For every block `b` and author `X`, either `H(b)` holds at most one `X`-block per round — the equivocation gained `X` nothing — or `X` is exposed in `H(b)` and `b` may not reference `X`. The two are the same sentence read twice: the mechanism does not need to *catch* equivocators, because exclusion is automatic exactly where damage occurs. In particular the tie-break policy for accepting halves is not a security parameter. - **D12 — exposure is permanent.** `Reaches U c b → ExposedIn U b X → ExposedIn U c X`. Exclusion, once earned, is inherited by everything downstream. - **D13 — exposure is view-independent.** The test computed inside any view agrees with the test inside `U`, so two correct validators never disagree about whether a block is DoS-valid. The division of labour: the acceptance rule (§2) bounds what a flood can make you *keep*; `DoSValid` bounds what a reference can make you *fetch*; bandwidth stays outside (§1). ## 4. Safety and liveness under the condition **D14 — safety is untouched.** Literally: `DoSValid` is an extra hypothesis, and no safety result mentions it. Checked mechanically (`LeanDagTest/DoS/SafetyUnderDoS.lean`). **Exclusion is sound, and priced correctly.** - **D15.** `ExposedIn U b X → X ∉ Correct` — a correct validator is never excluded, by anyone, ever. - **D15a.** With `k` authors exposed in `H(b)`, `b`'s references must come from the other `n−k` validators: each caught equivocator costs exactly one unit of fault-tolerance margin, and at `k = f` a block must reference every correct block of the round below. This is the intended report, not a defect (§7 S8): redundancy falls in exact proportion to *proved* misbehaviour. - **D15b.** The correct set alone always meets the quorum: exclusion can never make the threshold unreachable. The pool shrinks; the threshold does not — which is what `|Correct| ≥ n−f` was always for. **Liveness.** The delivery layer separates `held` (what arrived — never deduplicated, §7 S5) from `accepted` (what the validator builds on — one block per author, forced by `distinct_creators`, §7 S2). `R` is the eventual-synchrony stabilization round: `EventuallyDelivers R` says that from round `R` on, every correct-authored block reaches every correct validator in time to be built on — the network assumption, nothing more. Under the condition, L1 (*no stall*) holds from `R` rather than from round 0 — before `R` the adversary controls delivery and can hand a validator a quorum of authors it has just excluded — and after `R` nothing changes: L4 and L6 are untouched, a correct leader still commits, commits still recur. The chain that matters end to end: exclusion bites → the correct set still meets the quorum (D15b) → blocks keep being produced → a post-`R` slot with a correct leader commits. Witnessed in full on `Uexcl` (§8). **What the network must move.** The chain above consumes only correct-authored blocks — `EventuallyDelivers` guards on the author being correct — together with their cones, which by the reference discipline are exactly the authors' accepted sets. No theorem assumes a Byzantine-authored block is ever delivered to anyone: Byzantine delivery is entirely the adversary's choice, and a block delivered to nobody is not in `U` and imposes no burden (§1). Both extremes are witnessed: `ugrowHonest` (`LeanDagTest/Mysticeti/Partial.lean`) discharges the liveness definitions with the Byzantine validator publishing nothing at all, and `Dtwin` (§8) has Byzantine blocks reaching some correct validators and not others. The consequence for relaying — a correct validator's outbound duty is its own block plus that block's cone, budget-bounded, and nothing else — is developed in §6 (*no amplification*). **Exclusion after `R` is total.** - **D16 — agree, or be exposed.** Post-`R` synchrony puts every correct round-`n` block into every correct round-`(n+1)` block's references, so correct validators either jointly hold one `X`-block per round — `X` gained nothing (D11) — or every correct round-`(n+1)` block is exposed to `X`. - **D17 — total and permanent.** Once every correct block of a round is exposed to `X`, *no valid block* of any later round may reference `X` — Byzantine blocks included, since every valid block leans on `f+1` correct blocks of the round below. - **D18 — pinning.** An author that publishes a round-`j` block to all but at most `f` correct validators loses the freedom to disagree about that round later. - **C2 — the rate guarantee.** Every author contributes at most one block per round to any history until it is exposed, and nothing afterwards (D11 + D19b + D17). The residual damage is **one reveal per Byzantine author** (§7 S4): a history built out of sight and delivered by getting a single block accepted — the last block ever accepted from that author. Bounding the *size* of that reveal is §5; repricing its *delivery* is §6. ## 5. The size of a reveal — the bare-model bounds The question S4 prices the residual damage by: what is the biggest `|H(b)|` a round-`r` block can have and stay valid? Without any condition, nothing better than the layer recurrence `m_s ≤ n + f·m_{s+1}` holds (writing `m_s` for the number of blocks of `H(b)` at round `s`) — each block may reference up to `f` fresh Byzantine blocks per level, and the recurrence compounds exponentially. Under `DoSValid` and validity the answer is **linear in `r` at every `f`**, with a per-round constant that is exponential in the number of exposed authors — from both sides, so the bare model's answer is final. **The per-block facts.** - **D5 / D6 — the baseline.** Without equivocation `|V| ≤ n(r+1)` (D5); and `(n−f)·r + 1 ≤ |U|` always, since equivocation only adds blocks (D6). Both ends attained. - **D7.** A history's top layer below the block is exactly its reference set, and carries distinct authors (`distinct_creators`). - **D8 / D8a.** An equivocation is visible only at a merge, two rounds up — the reference graph cannot *report* one earlier — and merges are not luck: a validator whose accepted set spans both halves exposes the author in its own next block as a matter of course. - **D19a.** A history containing no equivocation is linear: `|H(b)| ≤ n(r+1)`. - **D19b.** A block is clean about every author it references, so the blow-up can only come from authors a block does *not* name. **The self-parent condition (S10).** `ValidWrt` requires every non-genesis block to reference *some* block by its own creator: ```lean self_parent : 0 < b.round → ∃ i ∈ b.refs, (blk i).creator = b.creator ``` Real DAG protocols do this anyway, and without it the linear bound is false: an author that sheds its own past can launder chains through single-block *carriers*, giving `Θ(r^{⌊f/2⌋+1})` histories at `f ≥ 3` with every block valid and `DoSValid`. With it (all in `LeanDag/DoS/SelfParent.lean`): - **D20 — chains reach the ground**: a history holds a block by its own author at every round below it. - **D21 — no self-laundering**: no block is exposed to its own author — an author whose equivocation is visible in a history can never build on that history again. - **D22 / D23 — exact prices**: a block's own author contributes exactly `r+1` blocks to its history; naming another author costs exactly that author's chain, `r` blocks. - **D24 — the floor**: pure validity forces `(n−f)·r + 1 ≤ |H(b)|`, so the question is two-sided and the ceiling below matches the floor's shape. **The ceiling — C1′, proved at every `f`.** An author's contribution to a history is `chains × rounds`, and chains are counted by **tops** — the author's blocks with no same-author child in the cone (`topsOf`, `LeanDag/DoS/Adoption.lean`). An unexposed author has one chain; a namer's history has room for only one chain of the named author, so distinct tops need distinct adopting authors (*the adoption collapse*); and iterating "who adopted the adopter" climbs strictly nested cones — a **pedigree** (`LeanDag/DoS/Pedigree.lean`) — whose author list is duplicate-free and determines its top. Anchored at the first unexposed adopter, with `e := |exposedTo U b| ≤ f` exposed authors: > per exposed author `|topsOf U b X| ≤ (n−e)·e^(e−1)` > (`card_topsOf_le_of_exposed`); > per author per round **`c(f) = 1 + (n−1)·f^(f−1)`** > (`card_historyBlocksOf_le'`); > in total **`|H(b)| ≤ (n + (n−1)·f^f)·(r+1)`** (`card_history_le'`) — at > `n = 3f+1`: exactly `7(r+1)` at `f = 1`, constant `31` at `f = 2` > against a floor of `5r+1`. Under at most one exposed author the constant is `2n−1` (**B1**), and at `f ≤ 1` the bound is unconditional. Linear in `r` at every fault budget: no compounding, which is all C1′ ever demanded. **The exponential in `e` is real — polynomial `c(f)` is impossible.** Two proved constraints cut the count and pin its shape: - **D25 — density** (`LeanDag/DoS/Density.lean`): a valid block's history contains a block by all but at most `f` of the correct validators, at every round below it. Cones cannot be selectively blind; the miss budget is exactly `f`. - **Freshness**: a chain may adopt an author only while no chain of that author sits anywhere in what it has already gathered. With `e` exposed authors to adopt among, this prunes the pedigree tree to `G(e) = e + Σ_{d