# Lean 4 Proofs

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](https://github.com/AeneasVerif/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

```lean
-- 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 `axiom`s** — 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.