Formal Verification (Lean 4)

Interactive visual explorer, step-by-step memory & borrow simulator, Lean Blueprint dependency graph, and full Lean 4 proof browser for NURL's ownership model.

NURL's single-owner memory model (Memory and Ownership, docs/MEMORY.md) is backed by a mechanized Lean 4 soundness and leak-freedom proof in formal/ — over 30,200 lines of Lean 4 across 50 modules and 1,369 proven theorems, with zero sorrys and only Lean's three standard axioms (propext, Classical.choice, Quot.sound).

Use the interactive explorer below to inspect the proof at two levels:

For Everyone (Tab 1 — Visual Story & Simulator): Step through concrete NURL programs to see how the compile-time context $\Gamma$ (Typing.lean) and runtime memory store Mem (Semantics.lean) interact, why vec_push kills Slice views while preserving element borrows (Eff.kills), and how panic unwinding (panic_unwind) frees every owned allocation via the drop journal.
For Mathematicians & PL Researchers (Tabs 2–4 — Lean Blueprint DAG, Code Browser & 303 Hole Corpus): Explore the interactive Lean Blueprint theorem/module dependency graphs, browse all 1,766 Lean 4 declarations with cross-referenced dependencies, and inspect all 303 soundness hole probes (h01–h315).

Lean 4 -koneistettu todistus · A1 & A2 todistettu (0 sorrya)

NURLin muistimallin visuaalinen ja interaktiivinen todistusselain

Tutki sekä visuaalisesti ("tavalliselle ihmiselle") että matemaattisen tarkasti (Lean Blueprint -riippuvuusverkko ja kaikki 1 766 Lean 4 -määritelmää), miten NURL todistaa muistiturvallisuuden (A2.memory_safe) ja vuodottomuuden (A2.no_leak_end, A2.no_leak_panic).

30,328

riviä Lean 4 -todistusta

1,375

todistettua lausetta (0 sorry)

Lean-moduulia (A1 + A2)

307

reikäkoetta (h01–h298)

v4.35.0

Vain standardiaksioomat

Mitä Lean 4 -todistus oikeasti todistaa? (Kansantajuinen kokonaiskuva)

Ohjelmointikielissä, joissa ei ole roskienkerääjää (GC), on viisi klassista tapaa rikkoa muisti: (1) luku vapautuksen jälkeen (Use-After-Free), (2) saman muistin vapautus kahdesti (Double-Free), (3) luku vanhentuneen näkymän läpi kun puskuri kasvaa (Iterator/View Invalidation), (4) jaetun arvon muokkaus lainan aikana, ja (5) muistivuoto (Memory Leak) normaalin poistumisen tai paniikin yhteydessä. Lean-todistus rakentaa matemaattisen koneen, jossa jokainen näistä virheistä pysäyttäisi koneen Stuck-tilaan — ja todistaa sitten, ettei yksikään tyyppitarkistuksen läpäissyt ohjelma voi koskaan päätyä Stuck-tilaan tai jättää muistia vapauttamatta.

A2.memory_safe

1. Ei koskaan muistivirhettä (¬ Stuck)

Jokainen muistiluku tarkistaa, että keko-osoite on varattu (m.alloc c = true) ja indeksit ovat rajoissa. Jos ohjelma yrittäisi lukea vapautettua muistia tai vanhentunutta Slice-näkymää, sääntöä ei ole (Stuck). Lause todistaa, että jokainen saavutettava tila on joko valmis (.skip), panikoi turvallisesti tai ottaa laillisen askeleen.

A2.no_leak_end

2. Ei muistivuotoja valmistuessa

Invariantti Covers m takaa jokaisella askeleella, että jokainen varattu osoite (m.alloc i = true) kuuluu täsmälleen yhdelle aktiivisen lohkon omistajalle. Kun ohjelma päättyy (.ok m' .skip), kaikki lohkot ovat poistuneet, joten ∀ i, m'.alloc i = false.

A2.no_leak_panic

3. Ei muistivuotoja edes paniikissa

Kun rajatarkistus tai panic laukeaa, ajonaikainen pino purkautuu (panic_unwind) sisimmästä kehyksestä ulompaan (drop journal). Jokainen poistuva kehys vapauttaa omistamansa puut (DropSlot), joten lopputilassa ∀ i, m'.alloc i = false.

Interaktiivinen muisti- ja lainantarkistussimulaattori

Valitse skenaario ja astu eteenpäin nähdäksesi rinnakkain käännösaikaisen kontekstin Γ (Typing.lean) ja ajonaikaisen muistin Mem (Semantics.lean).

1. Miksi vec_push mitätöi Slice-näkymän (mutta säilyttää alkiolainan)?

Havainnollistaa sääntöä StmtT.push, efektihilaa Eff.kills .realloc ja reikäkokeita h07 / h33.

1 / 4

Stmt.letv v (Rhs.new .int) …Vaihe 1: Luodaan omistettu Vec v

Muuttuja v saa omistavan paikan Slot⟨own: true, some(node c=0 d=1 [])⟩. Kekoon varataan ohjaussolmu #0 ja datapuskuri #1.

1. NURL Source Codeline 1

1: ( Vec i ) v ( vec_new [i] )
2( vec_push [i] v 42 )
3: ( Slice i ) s ( slice_from_vec [i] v )
4( vec_push [i] v 99 )   // reallocates buffer d=1 → d=2!
5: i x ( slice_get [i] s 0 ) // COMPILE ERROR: s is dead

2. Käännösaikainen konteksti ΓA2/Typing.lean

vmode: .own Ty.vec .int

live = true

Ainoa omistaja puulle (#0, #1)

3. Ajonaikainen muisti MemA2/Semantics.lean

Pinopaikat (m.st : Var → Option Slot):

vown=true

node(c=#0, d=#1, [42])

Keko-osoitteet (m.alloc : Nat → Bool):

Vec header c=#0alloc=true (owner: v)

Buffer d=#1 [42]alloc=true (owner: v)

Interaktiivinen efektihila (Eff.kills): Mitkä lainat säilyvät ja mitkä kuolevat?

Kokeile mitä tahansa operaatiota säiliölle v (A2/Syntax.lean: Eff.kills e hv k) ja katso mitkä v:stä riippuvat sidonnat pysyvät elossa.

Säiliön alkiot sisältävät näkymiä (Ty.holdsView = true)

Kind.viewKILLED (live := false)

Näkymä puskuriin (.view)

: ( Slice i ) s ( slice_from_vec [i] v )

Puskuri voi siirtyä uuteen osoitteeseen tai vapautua → näkymä osoittaisi vanhaan puskuriin.

Kind.innerSÄILYY (live = true)

Alkiolaina (.inner)

: ~ ( Vec i ) elem ( vec_at v 0 )

Ulomman Vecin puskurin siirto (realloc) säilyttää alkioiden omat ohjaussolmut ehjinä!

Kind.selfSÄILYY (live = true)

Kahvalaina (.self)

: ~ ( Vec i ) cur v

Kahva osoittaa samaan ohjaussolmuun c, joka pysyy voimassa.

Proof Roadmap & Scope (`formal/CLAIM.md`)

The mechanization is organized into phases:

Phase	Scope	Key Theorems	Status
A1	Core single-threaded calculus: owned `Vec` trees (a `String` is a `Vec` of bytes), moves and drop flags, `in` / `inout` / `sink`, borrows and `Slice` views, buffer reallocation (`Eff.realloc`), element drop (`Eff.drop`), function summaries (`CallT`, `FnOK`).	`A1.soundness`, `A1.memory_safe`	Proven (22 modules, 9,571 lines, 449 theorems)
A2	Full single-threaded calculus: A1 + inline structs (`Ty.prod`) and enums/options (`Ty.sum`) with field-precise paths, closures and trait objects as packages (`Val.pkg`, `Rhs.pack`, `Stmt.callc`) with captures by handle and by name (`Kind.name`), panics with unwinding and `recover` (`Stmt.catchR`), the drop journal, and complete leak freedom.	`A2.soundness`, `A2.memory_safe`, `A2.no_leak_end`, `A2.no_leak_panic`	Proven (28 modules, 20,693 lines, 920 theorems)
A3	Concurrency: `Send` / `Sync`, `Arc`, `Mutex`, `Locked [T]`, `RwLocked [T]` and `% Frozen`, `Atomic`, channels, M:N fibers — data-race freedom against the LLVM / C11 memory model.	—	Planned
B	Semantic soundness of the standard library's `unsafe` foundation (`Vec`, `String`, `HashMap`, `Rc` + cycle collector, `Arc`, channels).	—	Planned
C	Compiler verification: `nurlc` emits proof certificates for accepted programs, checked by a small verified validator.	—	Planned
D	Codegen translation validation: drop insertion, drop flags, and the panic drop journal preserve the formal operational semantics.	—	Planned

Verifying the Proof Locally

The Lean 4 proof uses toolchain leanprover/lean4:v4.35.0 with zero external library dependencies (Lean 4 core library only). To build all 50 modules and verify that the crown theorems depend only on standard axioms:

cd formal
./check.sh

check.sh runs lake build, rejects any occurrence of sorry, admit, or custom axiom across A1/ and A2/, and executes lake env lean Check.lean (#print axioms A1.memory_safe, A2.memory_safe, A2.no_leak_end).