Skip to content

Commit ea496bd

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
feat(formal): real-lift R2-loops — backward jumps (Loop/Br/BrIf) + while simulation (settles #601) (#665)
Fourth rung of the real lift (`formal/REAL-LIFT.adoc`): **structured control with backward jumps**, and a source `while` whose lowering is proved correct — settling the **#601** value-returning-tail question concretely. Axiom-free throughout. > Branch note: pushed to `claude/lucid-cray-4a22dp-r2loops` rather than `claude/lucid-cray-4a22dp` — the latter is still present at the merged #664 tip and is now protected against direct pushes (force/ff/delete all blocked), so a fresh branch was the only push path. Diff is against current `main` (post-#664), so it shows **only** the R2-loops changes. ## What landed **Target IR (`RealWasm.v`)** - Adds the faithful `lib/wasm.ml` structured-control instructions `Block`, `Loop`, `Br k`, `BrIf k` to `instr` (+ dead `step1` arms). **Zero blast radius** — the proven `wexec` and `RealCompile.compile_correct` still compile unchanged. **R2-loops (new file `RealLoop.v`)** - The R2 executor `wexec : … → option (locals×stack)` can't express *"this code branched to label k"*, so it cannot run `Br`. R2-loops introduces a **branch-aware** executor `cexec` returning an `outcome` (`ONormal` / `OBranch k` / `OTrap`). It reuses the *same fuel device* R2 used for forward control: a `Loop` consumed by `Br 0` re-enters by recursing with decremented fuel, so `cexec` stays a structural `Fixpoint` — definitional, so `cbn`/`reflexivity`/demos still compute (a real countdown `while` evaluates by `reflexivity`). - `cexec_le_S` / `cexec_mono` (more fuel never changes a `Some`) + `cexec_app_normal` (additive sequencing when the prefix ends `Normal`). - A *mutual* `instr`/`list instr` `branchfree` predicate is **rejected by Coq's guard checker** (list recursion only decreases on the spine), so instead of a `wexec→cexec` bridge over a flag, the R2 expression compiler is re-proved directly into `cexec`: **`cexec_compile`** (the `cexec` analogue of `compile_correct`). - Source statements `SSkip` / `SSeq` / `SSet` / `SWhile` with a fuel-indexed reference `run_stmt` (+ `run_stmt_mono`, `run_stmt_length`), and a lowering `compile_stmt` taking `while` to `Block[Loop[<cond>; I32Eqz; BrIf 1; <body>; Br 0]]`. - **`cexec_loop`** — the loop-simulation lemma (induction on the while's fuel: cond-false unwinds with `OBranch 1`, caught by the `Block`; cond-true runs the body and re-enters via `OBranch 0`). - **`compile_stmt_correct`** — a terminating statement's lowering runs to the same locals, leaving the value stack **empty** (`cexec … = Some (ONormal lo' [])`). A `while` is a *statement* (unit tail); this is **#601 settled concretely** — the expression tail would instead keep its value on the stack. ## Verification `coqc` 8.18, whole `formal/` track re-audited against current `main`: - **19 files compile**, **33 `Print Assumptions` reports**, every one *"Closed under the global context"* — **zero axioms, no `Admitted`**. ## Docs `formal/REAL-LIFT.adoc` (R2 row + §5 hard-parts + §8 status), `formal/README.adoc` (RealLoop row + "real lift R0 → R2-loops"), `docs/PROOF-NEEDS.adoc` (counts 18→19 / 31→33, K-1 row). `_CoqProject` / `justfile` / `.hypatia-ignore` wire `RealLoop.v` in. ## Next Rung **R-mem** (linear memory: load/store, tuples/arrays/records). `for`/`break`/`continue` and a general source-divergence model reuse this `cexec`. Refs `REAL-LIFT.adoc`, `docs/PROOF-NEEDS.adoc` (K-1 row), #601. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr --- _Generated by [Claude Code](https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent bfa3c70 commit ea496bd

8 files changed

Lines changed: 802 additions & 37 deletions

File tree

‎.hypatia-ignore‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -83,3 +83,7 @@ cicd_rules/vlang_detected:formal/Rows.v
8383
cicd_rules/banned_language_file:formal/Rows.v
8484
cicd_rules/vlang_detected:formal/RealCompile.v
8585
cicd_rules/banned_language_file:formal/RealCompile.v
86+
# RealLoop.v — REAL-LIFT rung R2-loops (Loop/Br/BrIf + source while). Coq proof
87+
# script, wired into formal/_CoqProject; exempt from the V-lang ban.
88+
cicd_rules/vlang_detected:formal/RealLoop.v
89+
cicd_rules/banned_language_file:formal/RealLoop.v

‎docs/PROOF-NEEDS.adoc‎

Lines changed: 11 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ This is the single document that enumerates *what AffineScript must prove*, at
1212
gap between the soundness *arguments* the project relies on (prose in
1313
`docs/academic/proofs/`, the borrow-checker comments in `lib/borrow.ml`,
1414
`docs/CAPABILITY-MATRIX.adoc`) and the soundness *proofs* that are actually
15-
mechanized today: a growing axiom-free Coq core (18 files) that pins each
15+
mechanized today: a growing axiom-free Coq core (19 files) that pins each
1616
obligation on a deliberately *small model* — no full-language theorem is
1717
discharged yet (see <<status>>).
1818

@@ -70,7 +70,7 @@ than the prose corpus suggests:
7070
`TypeSafety.v` is example lemmas about list length, not AffineScript. Not
7171
core-metatheory.
7272
* **`formal/`** — the directory #513 names as the mechanized-proof target now
73-
**exists** (Coq/Rocq 8.18), axiom-free throughout — **18 files, 31 `Print
73+
**exists** (Coq/Rocq 8.18), axiom-free throughout — **19 files, 33 `Print
7474
Assumptions` closure reports**, all "Closed under the global context". Codegen
7575
keystone: `K1_CodegenPreservation.v` (K-1 minimal) +
7676
`K1Let_CodegenPreservation.v` (K-1 grown with variables/`let`/environment).
@@ -84,10 +84,15 @@ than the prose corpus suggests:
8484
`AffineUsage.v` (`λx.x` affine, `λx. x x` not) + `QttTyping.v` (quantitative
8585
typing, `usage x t = Γ x` sound) + `QttDynamic.v` (the dynamic half:
8686
β-reduction preserves the usage profile). Real lift (`REAL-LIFT.adoc`):
87-
`RealWasm.v` (real `lib/wasm.ml` IR — i32 core + locals + structured `IfElse`,
88-
fuel-indexed `wexec`) + `RealCompile.v` (R1+R2: the first real
89-
`⟦compile p⟧ = ⟦p⟧`, incl. `if`). Record rows: `Rows.v` (P-11 — progress +
90-
preservation for extensible records). See <<outstanding>>, <<faces>>.
87+
`RealWasm.v` (real `lib/wasm.ml` IR — i32 core + locals + structured `IfElse`
88+
+ `Block`/`Loop`/`Br`/`BrIf`, fuel-indexed `wexec`) + `RealCompile.v` (R1+R2:
89+
the first real `⟦compile p⟧ = ⟦p⟧`, incl. `if`) + `RealLoop.v` (R2-loops: a
90+
branch-aware executor `cexec` over backward jumps, a source `while`/`seq`/`set`
91+
statement language, and `compile_stmt_correct` — the lowered terminating
92+
`while` simulates the reference run, settling the #601 value-returning-tail
93+
question concretely: the statement tail leaves an empty value stack).
94+
Record rows: `Rows.v` (P-11 — progress + preservation for extensible records).
95+
See <<outstanding>>, <<faces>>.
9196
* **Research tracks** (not core soundness): `docs/academic/tropical-session-types/`
9297
(Lean), `proposals/echo-types/EchoEncodingFaithfulness.agda`,
9398
`proposals/idaptik/migrated/**/*Boundary.agda` (echo-types loss-with-residue,

‎formal/README.adoc‎

Lines changed: 24 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -107,6 +107,13 @@ cannot mistake it. Coq has no `v.mod` manifest, so `vmod_detected` never fires.
107107
`compile_correct` (retires K1/K1Let on real objects)
108108
| **mechanized**, axiom-free
109109

110+
| `RealLoop.v`
111+
| **Real lift R2-loops** — `Block`/`Loop`/`Br`/`BrIf` + a branch-aware executor
112+
`cexec`; source `while`/`seq`/`set` statements; `compile_stmt_correct` (a
113+
terminating `while`'s `Block[Loop[…]]` lowering simulates `run_stmt`,
114+
empty-stack unit tail — settles #601)
115+
| **mechanized**, axiom-free
116+
110117
| `Rows.v`
111118
| **P-11** — record-row soundness: progress + preservation for STLC + extensible
112119
records (empty/extend/select/restrict over a `lacks`-checked row), funext-free
@@ -232,11 +239,11 @@ the same canonical AST emit identical code). The observational version for the
232239
trailing-statement/tail split is mechanized separately in
233240
`invariant-path/proofs/SameCube.agda` (F-2).
234241

235-
== The real lift (R0 → R2)
242+
== The real lift (R0 → R2-loops)
236243

237244
The *real lift* replaces the toy stack machine with the actual `lib/wasm.ml` IR
238245
and the toy source with the real (resolved) AST, climbing a strict-superset
239-
fragment ladder. Three rungs are down:
246+
fragment ladder. Four rungs are down:
240247

241248
* **R0** (`RealWasm.v`) — the pure i32 numeric core (real `instr` / `value_type`
242249
names) and a stack-machine `wexec`.
@@ -254,11 +261,21 @@ fragment ladder. Three rungs are down:
254261
(more fuel never loses a result) + `wexec_app_some` (additive sequencing). The
255262
preservation theorem is stated **existentially in the fuel**; the branch taken
256263
by `if` is run with monotonically-padded fuel.
257-
258-
The full plan — the rest of the ladder (R2-loops → R-mem → R-float → R-str →
259-
R-call → R-wrap → R-eff), the Coq module structure, and the strategy for each
260-
hard part (backward jumps `Loop`/`Br` reuse the fuel device; linear memory,
261-
floats, the elaboration nodes, effects) — is `formal/REAL-LIFT.adoc`.
264+
* **R2-loops** (`RealWasm.v` grown with `Block`/`Loop`/`Br`/`BrIf`; `RealLoop.v`)
265+
— backward jumps. The R2 `wexec` can't express "branched to label k", so a
266+
branch-aware executor `cexec` (outcome `ONormal`/`OBranch k`/`OTrap`) handles
267+
the structured control: a `Loop` consumed by `Br 0` re-enters with decremented
268+
fuel, staying a structural `Fixpoint`. The R2 expression compiler is re-proved
269+
into `cexec` (`cexec_compile`), and a source `while`/`seq`/`set` statement
270+
language is lowered to `Block[Loop[…;BrIf 1;…;Br 0]]`; `compile_stmt_correct`
271+
proves a terminating `while` simulates the reference `run_stmt`, ending with an
272+
**empty value stack** — settling the #601 value-returning-tail question
273+
(statement tail = unit) concretely.
274+
275+
The full plan — the rest of the ladder (R-mem → R-float → R-str → R-call →
276+
R-wrap → R-eff), the Coq module structure, and the strategy for each hard part
277+
(linear memory, floats, the elaboration nodes, effects) — is
278+
`formal/REAL-LIFT.adoc`.
262279

263280
== Record rows (P-11)
264281

‎formal/REAL-LIFT.adoc‎

Lines changed: 50 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -169,18 +169,24 @@ next. The rung names are stable references the `PROOF-NEEDS.adoc` rows will cite
169169
fold in with R2/R-wrap.)
170170
| **Subsumes K1 and K1Let on real objects.**
171171

172-
| **R2** ✅ (conditionals)
173-
| Structured control. **Done:** the `IfElse` instruction (lib/wasm.ml's `If`) +
174-
`RIf` source (`ExprIf`), value-returning. Because `instr` now nests
175-
`list instr`, the structural `wexec` is guard-rejected, so `wexec` became
176-
**fuel-indexed** (`wexec_mono` + `wexec_app_some` replace the clean
177-
`wexec_seq`; the theorem is existential in the fuel). **Remaining (R2-loops):**
178-
`Loop`/`Br`/`BrIf` + `while`/`for`/`break`/`continue` — backward jumps reuse
179-
the same fuel device, plus a source divergence model.
180-
| Closed the toy K-1's "`if`/control is the next increment" gap. The remaining
181-
value-returning-tail story lets **F-2** (#601) be settled *concretely*: the
182-
statement-tail vs expression-tail lowerings become two real `instr` sequences
183-
whose `wexec` agreement (unit) / divergence (value-returning) is a theorem.
172+
| **R2** ✅ (conditionals + loops)
173+
| Structured control. **Done (conditionals):** the `IfElse` instruction
174+
(lib/wasm.ml's `If`) + `RIf` source (`ExprIf`), value-returning. Because
175+
`instr` now nests `list instr`, the structural `wexec` is guard-rejected, so
176+
`wexec` became **fuel-indexed** (`wexec_mono` + `wexec_app_some` replace the
177+
clean `wexec_seq`; the theorem is existential in the fuel). **Done (R2-loops,
178+
`RealLoop.v`):** the `Block`/`Loop`/`Br`/`BrIf` instructions + a *branch-aware*
179+
executor `cexec` (outcome = Normal / Branch k / Trap) that handles the
180+
backward jump (a `Loop` consumed by `Br 0` re-enters, reusing the same fuel
181+
device), the R2 expression compiler lifted into it (`cexec_compile`), a source
182+
`while`/`seq`/`set` statement language, and `compile_stmt_correct` — a
183+
terminating `while`'s lowering (`Block[Loop[…;BrIf 1;…;Br 0]]`) simulates the
184+
reference `run_stmt`. (`for`/`break`/`continue` reuse the same machinery; an
185+
RLet-scratch / general source divergence model is the residual.)
186+
| Closed the toy K-1's "`if`/control is the next increment" gap, then the loop
187+
gap. **F-2** (#601) is now settled *concretely*: a `while` is a *statement*,
188+
and its lowering's `cexec` ends with an **empty value stack** (the unit tail) —
189+
a theorem — versus the expression tail, which keeps its value on the stack.
184190

185191
| **R-mem**
186192
| Linear memory: load/store family, `MemorySize/Grow`, a byte-addressed memory
@@ -222,14 +228,25 @@ proven against).
222228

223229
== 5. Hard parts and the strategy for each
224230

225-
* **Nested control & termination — DONE for conditionals (R2).** Because `instr`
226-
nests `list instr` (the `IfElse` branches), even *forward* structured control
227-
defeats Coq's structural guard checker — so `wexec` is already **fuel-indexed**
228-
as of R2 (`wexec : nat → …`), with the standard monotonicity lemma
229-
(`wexec_mono`: more fuel never changes a `Some` result) and an additive
230-
sequencing lemma (`wexec_app_some`) replacing the structural `wexec_seq`;
231-
preservation is stated existentially in the fuel. Backward jumps (`Loop`/`Br`,
232-
and the source `while`/`for`) reuse the very same device — that is R2-loops.
231+
* **Nested control & termination — DONE for conditionals *and* loops (R2 +
232+
R2-loops).** Because `instr` nests `list instr` (the `IfElse`/`Block`/`Loop`
233+
branches), even *forward* structured control defeats Coq's structural guard
234+
checker — so `wexec` is **fuel-indexed** as of R2 (`wexec : nat → …`), with the
235+
standard monotonicity lemma (`wexec_mono`) and additive sequencing
236+
(`wexec_app_some`) replacing the structural `wexec_seq`; preservation is
237+
existential in the fuel. Backward jumps (`Loop`/`Br`, and the source
238+
`while`/`for`) reuse the very same device — that is R2-loops (`RealLoop.v`),
239+
**done**: a `Loop` consumed by `Br 0` recurses with decremented fuel, so the
240+
loop stays a structural `Fixpoint`. Because the R2 `wexec` returns
241+
`option (locals×stack)` and so cannot express "branched to label k", R2-loops
242+
introduces a branch-aware `cexec` (outcome = `ONormal`/`OBranch k`/`OTrap`)
243+
with its own `cexec_mono` + `cexec_app_normal`; the R2 expression compiler is
244+
re-proved into it (`cexec_compile`), and `compile_stmt_correct` shows a
245+
terminating source `while` simulates its `Block[Loop[…]]` lowering. The
246+
guard-checker also rejects a *mutual* `instr`/`list instr` "branch-free"
247+
predicate (list recursion only decreases on the spine), which is why the
248+
bridge is the direct `cexec_compile` re-proof rather than a `wexec`→`cexec`
249+
lift over a `branchfree` flag.
233250
* **Linear memory.** Model memory as `Z → byte` (or a finite map) + a bound;
234251
load/store mirror `lib/wasm.ml`'s align/offset. The allocator
235252
(`runtime/src/alloc.rs`) is modelled abstractly (a bump pointer in a global) —
@@ -297,7 +314,18 @@ already has the front-end scaffolding (`F1_TransformerPreservation.v`,
297314
in the fuel. (The R1 arity lemma `wexec_sound`/`wcheck` was retired in the fuel
298315
refactor; it can be restated over fuel later, but is not load-bearing —
299316
`compile_correct` is.) Axiom-free.
300-
* Next: **R2-loops** — `Loop`/`Br` + source `while`/`for` on the same fuel
301-
device; this is the rung that settles #601 concretely.
317+
* **R2-loops landed** — `RealWasm.v` grown with `Block`/`Loop`/`Br`/`BrIf`
318+
(faithful lib/wasm.ml structured control), zero blast radius on the proven
319+
`wexec`. `RealLoop.v` adds the branch-aware executor `cexec` (outcome
320+
`ONormal`/`OBranch k`/`OTrap`; a `Br 0` to a `Loop` re-enters via decremented
321+
fuel) with `cexec_mono` + `cexec_app_normal`, lifts the R2 expression compiler
322+
into it (`cexec_compile`), defines a source `while`/`seq`/`set` statement
323+
language (`run_stmt`/`compile_stmt`), and proves `compile_stmt_correct`: a
324+
terminating `while` lowered to `Block[Loop[…;BrIf 1;…;Br 0]]` simulates the
325+
reference run, ending with an **empty value stack** — the unit/statement tail,
326+
settling **#601** concretely. Axiom-free; 19 files / 33 closure reports.
327+
* Next: **R-mem** — linear memory (load/store, byte model) for tuples/arrays/
328+
records; then R-float / R-str / R-call per the ladder. (`for`/`break`/
329+
`continue` and a general source-divergence model reuse the R2-loops `cexec`.)
302330

303331
Tracked against `docs/PROOF-NEEDS.adoc` §6 Wave 3 and #513.

0 commit comments

Comments
 (0)