Lean 4 Proofs

View as Markdown

The lean4/ directory contains machine-checked proofs of Nucleus's core algorithms, written in the Lean 4 proof assistant. Each proof targets a Lean model of an algorithm — a precise, hand-written translation of the Rust design — and shows the model holds for every input, not just tested cases. This gives mathematical confidence in the algorithm designs Nucleus implements; it is a proof about the models, not about the compiled Rust binary itself.

What's Verified

MVCC (Multi-Version Concurrency Control)

  • Snapshot isolation — Transactions see a consistent snapshot
  • No dirty reads — Uncommitted writes are invisible
  • Visibility correctness — Version chains resolve correctly

Page Allocator

  • No double-free — A freed page cannot be freed again
  • Conservation — allocated + free = total (no page leaks)
  • Allocation validity — Only free pages can be allocated

Buffer Pool

  • Capacity bounds — Pool never exceeds max size
  • Pin safety — Pinned pages are never evicted
  • Eviction correctness — Only unpinned pages are evictable

Cryptographic Primitives

  • HMAC-SHA256 — Output length, determinism, PRF security
  • Constant-time comparison — Timing-attack resistance (examines all bytes)
  • PKCE (RFC 7636) — Roundtrip correctness, determinism, collision resistance

Data Structures

  • LRU Cache — Capacity bounds, set/get consistency, no duplicates
  • Bloom Filter — No false negatives, insert monotonicity, bit array invariants
  • Sliding Window — Non-negative estimates, accurate counting, rollover correctness

Project Structure

lean4/Nucleus/
├── lakefile.lean           # Build configuration
├── lean-toolchain          # Lean version pin
└── Nucleus/
    ├── Aeneas/             # Rust → Lean translations
    │   ├── Primitives.lean
    │   ├── StorageModel.lean
    │   ├── MvccModel.lean
    │   └── PageModel.lean
    ├── Spec/               # Formal specifications
    │   ├── MvccSpec.lean
    │   ├── PageSpec.lean
    │   ├── BufferSpec.lean
    │   └── TupleSpec.lean
    ├── Proofs/             # Machine-checked proofs
    │   ├── MvccProofs.lean
    │   ├── PageProofs.lean
    │   ├── BufferProofs.lean
    │   └── TupleProofs.lean
    ├── Helpers/            # Shared tactics & lemmas
    ├── Crypto/             # HMAC, PKCE, constant-time proofs
    └── Structures/         # LRU, Bloom, sliding window proofs

How It Works

  1. Models capture each algorithm's Rust types and functions as Lean 4 definitions. These are hand-written to mirror nucleus/src. (The Aeneas/ naming reflects the long-term goal of auto-generating them with Aeneas; today they are maintained by hand.)
  2. Specs state the properties to prove as Lean theorems
  3. Proofs provide machine-checked evidence that the properties hold
  4. Lean's type checker verifies every proof step — no human trust required

Example: Empty WAL Recovery

-- Proofs/WalProofs.lean — proven with `simp`, no `sorry`, no axioms
/-- An empty WAL has no recovery records. -/
theorem empty_wal_no_recovery :
    (WAL.mk [] 0 0).recoveryRecords = [] := by
  simp [WAL.recoveryRecords]

This holds for the model by construction — Lean checks it for every case, not just the ones a test would try.

Axioms and Assumptions

The suite compiles with zero sorry, but it declares 28 explicit axioms — facts assumed rather than derived from Lean's core. Being explicit about them is the point: what is assumed is stated in the open and can be audited. They fall into three groups:

  • Foundational identities — e.g. n ^^^ n = 0. True and mechanical; axiomatized to avoid pulling in heavy Nat/bitwise libraries.
  • Standard cryptographic assumptions — e.g. SHA-256 collision resistance (sha256_collision_resistant), HMAC PRF security. These are unprovable by nature; every crypto proof assumes them.
  • Open proof obligations — a few structural lemmas (notably in Structures/BloomSpec.lean and Structures/LruSpec.lean) are currently assumed rather than fully discharged. Discharging these is tracked work.

So the guarantees are modulo these axioms. The MVCC, WAL, and Raft models are proven without any load-bearing assumptions of their own.

Status

All 26 files compile with 0 sorry across 70 theorems. The proofs cover Lean models of the algorithms listed above; they do not (yet) prove properties of the production Rust directly. The open threads are discharging the remaining structural axioms and moving from hand-written models toward Aeneas-generated ones.