Skip to content

LeaTTa 0.5.0

Choose a tag to compare

View all tags
@MesTTo MesTTo released this 20 Jun 08:16
· 40 commits to metatheory since this release
v0.5.0
99419ef

LeaTTa 0.5.0: I machine-checked the safety of Cordial Miners

I formalized PoR-weighted Cordial Miners, a leaderless DAG-based consensus protocol, in Lean 4 and proved it safe. It is the next LeaTTa iteration, after MeTTaIL.

Run it:

#eval simulate demo
-- [1, 2, 3]

I hand it a committee, some blocks, and the approvals each block got. It folds the approvals through the weighted certificate collector, keeps the finalized blocks, and orders them with a verified topological sort. The ordering is a proved pure function, so every honest node computes the same list.

The safety I care about: two honest nodes never publish conflicting orders. It is a theorem, and here is everything it leans on:

#print axioms cm_end_to_end_safety_permanent
-- propext, Classical.choice, Quot.sound

The three standard axioms, nothing else. No sorry, admit, native_decide, partial, or unsafe, CI-enforced.

The theorem: under three assumptions, no two conflicting values ever finalize, correct nodes never disagree on a published position, and the blocklace stays well formed. The assumptions are the usual BFT ones:

  • a Byzantine-weight bound,
  • honest non-equivocation,
  • finality permanence (a final wave stays final).

The hard part is that the published order only grows and never reorders. I did not assume that, I derived it:

  • the order lists each finalized leader's history in turn,
  • so it grows when the finalized-leader sequence grows at the end,
  • which happens when the count of finalized waves goes up,
  • which happens when finality is permanent.

It all comes down to those three facts.

In the library:

  • the weighted quorum-overlap lemma, the arithmetic core of the safety,
  • self-enforcing threshold finality, and no two conflicting final leaders,
  • a verified, executable, total topological-sort ordering (no partial),
  • a coarse and a fine theory, tied by a forward simulation,
  • lossless extraction of protocol facts to MeTTa-IL atoms,
  • the end-to-end simulation above.

I proved safety, not liveness. Liveness (delivery, no scheduler starvation) holds only under fairness assumptions I state explicitly; I did the structural cores, the temporal argument is next. Finality permanence is an assumption, not derived from a network model.

The protocol is by Keidar, Naor, Poupko and Shapiro; the PoR-weighted variant and the plan are Ben Goertzel's. There is a Cordial Miners chapter in the LeaTTa book and an overview in the repo. Build it with lake build CordialMiners.

Assets 8
Loading