Skip to content

Commit 146e06a

Browse files
e6que6qu
authored
Merge pull request #3 from e6qu/docs/status-and-gap-analysis
Add project status, gap analysis, and next steps docs
2 parents b1a2a6a + 4886a68 commit 146e06a

6 files changed

Lines changed: 379 additions & 1 deletion

File tree

‎DO_NEXT.md‎

Lines changed: 122 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,122 @@
1+
# What To Do Next
2+
3+
## Immediate: Tutorial 01 End-to-End Verification
4+
5+
Prove the concept works by fully verifying tutorial 01:
6+
7+
### Step 1: Restructure Lean project
8+
```
9+
tutorials/01-setup-hello-proof/lean/
10+
├── lakefile.lean # require aeneas from git @ "main" / "backends" / "lean"
11+
├── lean-toolchain # match Aeneas's toolchain (v4.28.0-rc1)
12+
├── HelloProof.lean # REAL Aeneas output (copy from generated/)
13+
└── HelloProof/
14+
└── Proofs.lean # Real proofs against real generated code
15+
```
16+
17+
### Step 2: Write real proofs for tutorial 01
18+
Using patterns from the Aeneas ICFP tutorial:
19+
20+
```lean
21+
import HelloProof
22+
open Aeneas Aeneas.Std Result hello_proof
23+
24+
-- clamp never panics and result is in [lo, hi]
25+
@[pspec]
26+
theorem clamp_spec (x lo hi : Std.I32) (h : lo ≤ hi) :
27+
∃ r, clamp x lo hi = ok r ∧ lo ≤ r ∧ r ≤ hi := by
28+
rw [clamp]
29+
split <;> split <;> simp_all
30+
all_goals (constructor <;> scalar_tac)
31+
32+
-- safe_divide by zero returns Err
33+
@[pspec]
34+
theorem safe_divide_zero (x : Std.I64) :
35+
safe_divide x 0#i64 = ok (core.result.Result.Err ()) := by
36+
rw [safe_divide]; simp
37+
38+
-- checked_add never panics
39+
@[pspec]
40+
theorem checked_add_no_panic (x y : Std.U32) :
41+
∃ r, checked_add x y = ok r := by
42+
rw [checked_add]
43+
progress as ⟨i⟩ -- U32.MAX - x
44+
split
45+
· progress as ⟨i1⟩ -- x + y
46+
exact ⟨some i1, rfl⟩
47+
· exact ⟨none, rfl⟩
48+
```
49+
50+
### Step 3: Verify locally
51+
```bash
52+
cd tutorials/01-setup-hello-proof/lean
53+
lake build # Must succeed — this IS the formal verification
54+
```
55+
56+
### Step 4: Update CI
57+
Change Lean CI jobs to use real Aeneas library. Cache the Aeneas build (~1600 modules).
58+
59+
## Then: Fix Rust and Write Proofs for Tutorials 02-06
60+
61+
For each tutorial:
62+
1. Fix any Rust patterns that Aeneas can't translate
63+
2. Re-run `charon` + `aeneas` to get clean generated Lean
64+
3. Set up lakefile with real Aeneas dependency
65+
4. Write real proofs using `step`/`progress`/`scalar_tac`
66+
5. Verify with `lake build`
67+
68+
## Then: Fix Tutorials 07-11
69+
70+
These need Rust refactoring to avoid unsupported Aeneas patterns (see GAP_ANALYSIS.md Gap 5).
71+
72+
## Key Aeneas Proof Patterns to Use
73+
74+
From the ICFP tutorial solutions:
75+
76+
```lean
77+
-- Pattern 1: Unfold + progress through monadic steps
78+
theorem foo_spec (x : U32) (h : ↑x + 1 ≤ U32.max) :
79+
∃ y, foo x = ok y ∧ ↑y = ↑x + 1 := by
80+
rw [foo]
81+
progress as ⟨y⟩
82+
scalar_tac
83+
84+
-- Pattern 2: Branching (if/match)
85+
theorem bar_spec (x : I32) :
86+
∃ r, bar x = ok r := by
87+
rw [bar]
88+
split -- case split on if-then-else
89+
· simp_all -- true branch
90+
· simp_all -- false branch
91+
92+
-- Pattern 3: Loop invariant
93+
@[pspec]
94+
theorem loop_spec (x : Vec U32) (i : Usize) (h : i ≤ x.length) :
95+
∃ x', loop x i = ok x' ∧ x'.length = x.length := by
96+
rw [loop]
97+
split
98+
· progress as ⟨...⟩ -- loop body
99+
progress as ⟨x', hx'⟩ -- recursive call (uses this theorem via @[pspec])
100+
simp_all
101+
· simp_all
102+
termination_by (x.length - i.val).toNat
103+
decreasing_by scalar_decr_tac
104+
105+
-- Pattern 4: Composing specs
106+
-- If foo has @[pspec], then `progress` automatically uses it:
107+
theorem baz_spec (x : U32) (h : ...) :
108+
∃ y, baz x = ok y ∧ ... := by
109+
rw [baz]
110+
progress as ⟨y, hy⟩ -- auto-applies foo_spec
111+
scalar_tac
112+
```
113+
114+
## Definition of Done
115+
116+
A tutorial is "formally verified" when:
117+
1. Rust code compiles and passes tests
118+
2. `charon cargo --preset=aeneas` produces clean LLBC (no errors)
119+
3. `aeneas -backend lean *.llbc` produces clean Lean (no errors)
120+
4. Proof file contains real `theorem` (not `axiom`) with real tactic proofs (not `sorry`)
121+
5. `lake build` with real Aeneas library succeeds
122+
6. CI enforces all of the above

‎GAP_ANALYSIS.md‎

Lines changed: 115 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,115 @@
1+
# Gap Analysis: What's Missing for Real Formal Verification
2+
3+
## The Goal
4+
5+
**Prove Rust programs correct** by:
6+
1. Translating Rust → pure Lean via Aeneas
7+
2. Writing Lean proofs about the generated code
8+
3. Lean typechecker verifies the proofs → Rust code is proven correct
9+
10+
## Gap 1: No Real Proofs
11+
12+
**Current:** All theorems are `axiom` — unproven assertions. Lean accepts them but verifies nothing.
13+
14+
**Needed:** Real proofs using Aeneas tactics (`step`/`progress`, `scalar_tac`, `simp_all`).
15+
16+
**How to close:** Write proofs following the ICFP tutorial patterns:
17+
```lean
18+
-- Current (BROKEN — proves nothing):
19+
axiom clamp_in_bounds (x lo hi : Std.I32) (h : lo ≤ hi) :
20+
∃ r, clamp x lo hi = ok r ∧ lo ≤ r ∧ r ≤ hi
21+
22+
-- Needed (REAL — Lean verifies this):
23+
@[pspec]
24+
theorem clamp_in_bounds (x lo hi : Std.I32) (h : lo ≤ hi) :
25+
∃ r, clamp x lo hi = ok r ∧ lo ≤ r ∧ r ≤ hi := by
26+
rw [clamp]
27+
split <;> split <;> simp_all <;> constructor <;> scalar_tac
28+
```
29+
30+
**Effort:** Medium per theorem. Start with tutorials 01-03 (simplest), then 04-06.
31+
32+
## Gap 2: Proof Files Use Fake Prelude Instead of Real Aeneas Library
33+
34+
**Current:** Each tutorial has a standalone `Aeneas.lean` with simplified types (`U32` as bare `Nat` wrapper). Proof files import this fake prelude.
35+
36+
**Needed:** Lakefiles that `require aeneas from git` and proof files that import the real generated code.
37+
38+
**How to close:**
39+
1. Change each tutorial's `lakefile.lean` to depend on the real Aeneas library
40+
2. Replace hand-written `Funs.lean` with the real generated code from `lean/generated/`
41+
3. Rewrite proof files to work against real Aeneas types
42+
43+
**Effort:** Small per tutorial (lakefile change + file reorganization). The proofs themselves are Gap 1.
44+
45+
## Gap 3: Proof Files Don't Reference the Real Generated Code
46+
47+
**Current:** Hand-written `Funs.lean` files approximate what Aeneas generates. The real output is in `lean/generated/` but unused.
48+
49+
**Needed:** Proof files that `import` the real generated code and prove properties about the real generated functions.
50+
51+
**How to close:** For each tutorial:
52+
```
53+
lean/
54+
├── lakefile.lean # requires aeneas from git
55+
├── lean-toolchain # matches Aeneas's toolchain
56+
├── HelloProof.lean # REAL Aeneas output (was in generated/)
57+
└── HelloProof/
58+
└── Proofs.lean # Hand-written proofs importing HelloProof
59+
```
60+
61+
## Gap 4: CI Doesn't Verify Proofs Against Real Aeneas
62+
63+
**Current:** Lean CI builds against standalone prelude. Axioms always pass.
64+
65+
**Needed:** Lean CI builds against real Aeneas library. Real proofs must typecheck.
66+
67+
**How to close:**
68+
1. Change lakefiles to use real Aeneas dependency
69+
2. CI installs elan + runs `lake build` (Aeneas library is cached)
70+
3. Build time: ~5 min first run, ~30s cached
71+
72+
**Effort:** Small (lakefile changes + CI cache configuration).
73+
74+
## Gap 5: Some Rust Code Can't Be Translated by Aeneas
75+
76+
**Current:** Tutorials 04, 07, 08, 09, 10, 11 have Aeneas translation errors.
77+
78+
| Tutorial | Error | Root Cause |
79+
|----------|-------|------------|
80+
| 04 | `type_var_id` | Generic `run_machine<M: StateMachine>` |
81+
| 07 | `Unreachable` | `vec![]` macro in `AppModel::new`, modular focus cycling |
82+
| 08 | `shallow-init-box` | `Conversation::new` with `vec![msg]` |
83+
| 09 | `break to outer loop` | Nested loop in `validate_tool_call` |
84+
| 10 | Missing `filter`/`collect` | Iterator combinators |
85+
| 11 | `nested borrows` | Borrow in `render_conversation` |
86+
87+
**Needed:** Refactor Rust code to avoid unsupported patterns.
88+
89+
**How to close:**
90+
- Replace `vec![x]` with `Vec::new()` + `push(x)` (Aeneas doesn't support `vec![]` macro)
91+
- Replace `break` in nested loops with flag variable
92+
- Replace iterator chains with explicit `while` loops
93+
- Simplify generic trait usage
94+
- Avoid nested borrows
95+
96+
**Effort:** Medium. Each fix is small but needs retesting with Aeneas.
97+
98+
## Gap 6: Tutorial 07 Completely Fails Translation
99+
100+
**Current:** Tutorial 07 (TUI Core) fails Aeneas translation entirely.
101+
102+
**Needed:** Rewrite to avoid `Unreachable` patterns.
103+
104+
**How to close:** Rewrite `AppModel::new` to build widget list incrementally instead of using `vec![]`. Rewrite `focus_next`/`focus_prev` to avoid patterns that cause `Unreachable`.
105+
106+
**Effort:** Medium.
107+
108+
## Priority Order
109+
110+
1. **Gap 2 + Gap 3** — Switch to real Aeneas library and real generated code (structural change)
111+
2. **Gap 1** — Write real proofs for tutorial 01 first (easiest, proof of concept)
112+
3. **Gap 5** — Fix Rust code for tutorials with translation errors
113+
4. **Gap 4** — Update CI to build against real Aeneas
114+
5. **Gap 1 continued** — Write real proofs for remaining tutorials
115+
6. **Gap 6** — Fix tutorial 07

‎PLAN.md‎

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,32 @@
11
# Rust + Lean 4 Formal Verification via Aeneas: Master Plan
22

33
> This is the master implementation plan. For the project overview, see [README.md](README.md).
4+
> For current status, see [STATUS.md](STATUS.md). For gap analysis, see [GAP_ANALYSIS.md](GAP_ANALYSIS.md).
5+
6+
## Purpose
7+
8+
**Formally verify Rust programs using Lean 4 and Aeneas.**
9+
10+
The verification pipeline:
11+
1. Write Rust code
12+
2. Translate to pure Lean via Aeneas (`charon` + `aeneas`)
13+
3. Write Lean proofs about the generated code
14+
4. `lake build` typechecks proofs → Rust code is mathematically proven correct
415

516
## Context
617

7-
Build a comprehensive, beginner-friendly tutorial series that teaches formal verification of Rust programs using Lean 4 and Aeneas. The series culminates in a verified TUI multi-agent LLM harness. Each tutorial includes actual working Rust code, Aeneas-generated Lean code, and deep hand-written Lean proofs proving functional correctness.
18+
Build a comprehensive, beginner-friendly tutorial series that teaches formal verification of Rust programs using Lean 4 and Aeneas. The series culminates in a verified TUI multi-agent LLM harness. Each tutorial includes actual working Rust code, **real** Aeneas-generated Lean code, and Lean proofs verified by the Lean typechecker.
819

920
Target audience: total beginners (basic algorithm knowledge only).
1021
Architecture: "Functional Core, Imperative Shell" throughout.
1122

23+
## Related Documents
24+
25+
- [STATUS.md](STATUS.md) — Current project status
26+
- [WHAT_WE_DID.md](WHAT_WE_DID.md) — History of what was built
27+
- [GAP_ANALYSIS.md](GAP_ANALYSIS.md) — What's missing for real verification
28+
- [DO_NEXT.md](DO_NEXT.md) — Immediate next steps
29+
1230
## Project Structure
1331

1432
```

‎README.md‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -142,6 +142,14 @@ See [Tutorial 01: Setup and Hello Proof](tutorials/01-setup-hello-proof/README.m
142142
- [LEAN.md](LEAN.md) — Everything you need to know about Lean 4
143143
- [AENEAS.md](AENEAS.md) — Everything you need to know about Aeneas
144144

145+
## Project Documents
146+
147+
- [STATUS.md](STATUS.md) — Current project status and what works/doesn't
148+
- [PLAN.md](PLAN.md) — Master implementation plan
149+
- [GAP_ANALYSIS.md](GAP_ANALYSIS.md) — What's missing for real formal verification
150+
- [DO_NEXT.md](DO_NEXT.md) — Immediate next steps
151+
- [WHAT_WE_DID.md](WHAT_WE_DID.md) — History of what was built
152+
145153
## How Each Tutorial Works
146154

147155
Every tutorial (02 and above) has the same structure:

‎STATUS.md‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
# Project Status
2+
3+
**Last updated:** 2026-03-23
4+
5+
## Purpose
6+
7+
**Formally verify Rust programs using Lean 4 and Aeneas.**
8+
9+
This means: mathematically prove that Rust code is correct — not just that it compiles or passes tests, but that it satisfies precise specifications for ALL possible inputs. The proof is checked by the Lean 4 type checker, which is a small trusted kernel. If `lake build` succeeds, the code is verified.
10+
11+
## Current State
12+
13+
### What Works
14+
15+
| Component | Status | Details |
16+
|-----------|--------|---------|
17+
| Rust code | **Working** | 11 tutorials, 297 tests passing, all linted (clippy + fmt) |
18+
| Aeneas translation | **Working** | 10/11 tutorials successfully translated via `charon` + `aeneas` (Nix) |
19+
| Generated Lean code | **Working** | Real Aeneas output in `lean/generated/` — typechecks against real Aeneas library |
20+
| CI (Rust) | **Working** | 11 individual jobs: fmt, clippy, build, test |
21+
| CI (Lean) | **Partially working** | Builds against standalone prelude (not real Aeneas library) |
22+
| Formal proofs | **NOT working** | Theorem statements exist as `axiom` (unproven). No actual verification happening. |
23+
24+
### What Does NOT Work
25+
26+
1. **No real proofs exist.** All theorems are `axiom` declarations — they assert properties without proof. Lean accepts them but verifies nothing about correctness.
27+
28+
2. **The standalone Aeneas prelude is a fake.** Our `Aeneas.lean` defines simplified types (`U32` as bare `Nat` wrapper) without the real bounds guarantees. Proofs against this prelude would not constitute real verification.
29+
30+
3. **The tutorial Lean files don't use the real generated code.** The hand-written `Funs.lean` files are approximations of what Aeneas generates. The real output lives in `lean/generated/` but isn't used by the proof files.
31+
32+
4. **CI doesn't verify proofs.** The Lean CI jobs build against the standalone prelude, which has no proof obligations. They pass trivially.
33+
34+
### Tutorial Translation Results
35+
36+
| Tutorial | Charon | Aeneas | Notes |
37+
|----------|--------|--------|-------|
38+
| 01 Setup | OK | OK | Clean translation |
39+
| 02 RPN Calculator | OK | OK | Clean (lib only, binary had extern error) |
40+
| 03 Infix Calculator | OK | OK | Clean |
41+
| 04 State Machines | OK | Partial | `type_var_id` errors in generic `run_machine` |
42+
| 05 Message Protocol | OK | OK | Clean |
43+
| 06 Buffer Management | OK | OK | Clean |
44+
| 07 TUI Core | OK | **Failed** | `Unreachable` in `focus_next`/`focus_prev`/`new` |
45+
| 08 LLM Client Core | OK | Partial | `shallow-init-box` error in `Conversation::new` |
46+
| 09 Agent Reasoning | OK | Partial | `break to outer loop` in `validate_tool_call` |
47+
| 10 Multi-Agent | OK | Partial | Missing `filter`/`collect` iterator support |
48+
| 11 Full Integration | OK | Partial | `nested borrows` in `render_conversation` |
49+
50+
### Infrastructure
51+
52+
- **GitHub:** https://github.com/e6qu/rust-lean-aeneas
53+
- **CI:** GitHub Actions — 11 Rust jobs + 11 Lean jobs + gate
54+
- **Rust:** Edition 2024, rustc 1.94.0
55+
- **Lean:** v4.28.0 via elan
56+
- **Aeneas:** Latest from `github:aeneasverif/aeneas` via Nix
57+
- **Charon:** Latest from `github:aeneasverif/aeneas#charon` via Nix

0 commit comments

Comments
 (0)