feat(formal): real-lift R2-loops — backward jumps (Loop/Br/BrIf) + while simulation (settles #601)

.hypatia-ignore

@@ -83,3 +83,7 @@ cicd_rules/vlang_detected:formal/Rows.v
 cicd_rules/banned_language_file:formal/Rows.v
 cicd_rules/vlang_detected:formal/RealCompile.v
 cicd_rules/banned_language_file:formal/RealCompile.v
+# RealLoop.v — REAL-LIFT rung R2-loops (Loop/Br/BrIf + source while). Coq proof
+# script, wired into formal/_CoqProject; exempt from the V-lang ban.
+cicd_rules/vlang_detected:formal/RealLoop.v
+cicd_rules/banned_language_file:formal/RealLoop.v

docs/PROOF-NEEDS.adoc

@@ -12,7 +12,7 @@ This is the single document that enumerates *what AffineScript must prove*, at
 gap between the soundness *arguments* the project relies on (prose in
 `docs/academic/proofs/`, the borrow-checker comments in `lib/borrow.ml`,
 `docs/CAPABILITY-MATRIX.adoc`) and the soundness *proofs* that are actually
-mechanized today: a growing axiom-free Coq core (18 files) that pins each
+mechanized today: a growing axiom-free Coq core (19 files) that pins each
 obligation on a deliberately *small model* — no full-language theorem is
 discharged yet (see <<status>>).
 
@@ -70,7 +70,7 @@ than the prose corpus suggests:
   `TypeSafety.v` is example lemmas about list length, not AffineScript. Not
   core-metatheory.
 * **`formal/`** — the directory #513 names as the mechanized-proof target now
-  **exists** (Coq/Rocq 8.18), axiom-free throughout — **18 files, 31 `Print
+  **exists** (Coq/Rocq 8.18), axiom-free throughout — **19 files, 33 `Print
   Assumptions` closure reports**, all "Closed under the global context". Codegen
   keystone: `K1_CodegenPreservation.v` (K-1 minimal) +
   `K1Let_CodegenPreservation.v` (K-1 grown with variables/`let`/environment).
@@ -84,10 +84,15 @@ than the prose corpus suggests:
   `AffineUsage.v` (`λx.x` affine, `λx. x x` not) + `QttTyping.v` (quantitative
   typing, `usage x t = Γ x` sound) + `QttDynamic.v` (the dynamic half:
   β-reduction preserves the usage profile). Real lift (`REAL-LIFT.adoc`):
-  `RealWasm.v` (real `lib/wasm.ml` IR — i32 core + locals + structured `IfElse`,
-  fuel-indexed `wexec`) + `RealCompile.v` (R1+R2: the first real
-  `⟦compile p⟧ = ⟦p⟧`, incl. `if`). Record rows: `Rows.v` (P-11 — progress +
-  preservation for extensible records). See <<outstanding>>, <<faces>>.
+  `RealWasm.v` (real `lib/wasm.ml` IR — i32 core + locals + structured `IfElse`
+  + `Block`/`Loop`/`Br`/`BrIf`, fuel-indexed `wexec`) + `RealCompile.v` (R1+R2:
+  the first real `⟦compile p⟧ = ⟦p⟧`, incl. `if`) + `RealLoop.v` (R2-loops: a
+  branch-aware executor `cexec` over backward jumps, a source `while`/`seq`/`set`
+  statement language, and `compile_stmt_correct` — the lowered terminating
+  `while` simulates the reference run, settling the #601 value-returning-tail
+  question concretely: the statement tail leaves an empty value stack).
+  Record rows: `Rows.v` (P-11 — progress + preservation for extensible records).
+  See <<outstanding>>, <<faces>>.
 * **Research tracks** (not core soundness): `docs/academic/tropical-session-types/`
   (Lean), `proposals/echo-types/EchoEncodingFaithfulness.agda`,
   `proposals/idaptik/migrated/**/*Boundary.agda` (echo-types loss-with-residue,

formal/README.adoc

@@ -107,6 +107,13 @@ cannot mistake it. Coq has no `v.mod` manifest, so `vmod_detected` never fires.
   `compile_correct` (retires K1/K1Let on real objects)
 | **mechanized**, axiom-free
 
+| `RealLoop.v`
+| **Real lift R2-loops** — `Block`/`Loop`/`Br`/`BrIf` + a branch-aware executor
+  `cexec`; source `while`/`seq`/`set` statements; `compile_stmt_correct` (a
+  terminating `while`'s `Block[Loop[…]]` lowering simulates `run_stmt`,
+  empty-stack unit tail — settles #601)
+| **mechanized**, axiom-free
+
 | `Rows.v`
 | **P-11** — record-row soundness: progress + preservation for STLC + extensible
   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
 trailing-statement/tail split is mechanized separately in
 `invariant-path/proofs/SameCube.agda` (F-2).
 
-== The real lift (R0 → R2)
+== The real lift (R0 → R2-loops)
 
 The *real lift* replaces the toy stack machine with the actual `lib/wasm.ml` IR
 and the toy source with the real (resolved) AST, climbing a strict-superset
-fragment ladder. Three rungs are down:
+fragment ladder. Four rungs are down:
 
 * **R0** (`RealWasm.v`) — the pure i32 numeric core (real `instr` / `value_type`
   names) and a stack-machine `wexec`.
@@ -254,11 +261,21 @@ fragment ladder. Three rungs are down:
   (more fuel never loses a result) + `wexec_app_some` (additive sequencing). The
   preservation theorem is stated **existentially in the fuel**; the branch taken
   by `if` is run with monotonically-padded fuel.
-
-The full plan — the rest of the ladder (R2-loops → R-mem → R-float → R-str →
-R-call → R-wrap → R-eff), the Coq module structure, and the strategy for each
-hard part (backward jumps `Loop`/`Br` reuse the fuel device; linear memory,
-floats, the elaboration nodes, effects) — is `formal/REAL-LIFT.adoc`.
+* **R2-loops** (`RealWasm.v` grown with `Block`/`Loop`/`Br`/`BrIf`; `RealLoop.v`)
+  — backward jumps. The R2 `wexec` can't express "branched to label k", so a
+  branch-aware executor `cexec` (outcome `ONormal`/`OBranch k`/`OTrap`) handles
+  the structured control: a `Loop` consumed by `Br 0` re-enters with decremented
+  fuel, staying a structural `Fixpoint`. The R2 expression compiler is re-proved
+  into `cexec` (`cexec_compile`), and a source `while`/`seq`/`set` statement
+  language is lowered to `Block[Loop[…;BrIf 1;…;Br 0]]`; `compile_stmt_correct`
+  proves a terminating `while` simulates the reference `run_stmt`, ending with an
+  **empty value stack** — settling the #601 value-returning-tail question
+  (statement tail = unit) concretely.
+
+The full plan — the rest of the ladder (R-mem → R-float → R-str → R-call →
+R-wrap → R-eff), the Coq module structure, and the strategy for each hard part
+(linear memory, floats, the elaboration nodes, effects) — is
+`formal/REAL-LIFT.adoc`.
 
 == Record rows (P-11)
 

formal/REAL-LIFT.adoc

@@ -169,18 +169,24 @@ next. The rung names are stable references the `PROOF-NEEDS.adoc` rows will cite
   fold in with R2/R-wrap.)
 | **Subsumes K1 and K1Let on real objects.**
 
-| **R2** ✅ (conditionals)
-| Structured control. **Done:** the `IfElse` instruction (lib/wasm.ml's `If`) +
-  `RIf` source (`ExprIf`), value-returning. Because `instr` now nests
-  `list instr`, the structural `wexec` is guard-rejected, so `wexec` became
-  **fuel-indexed** (`wexec_mono` + `wexec_app_some` replace the clean
-  `wexec_seq`; the theorem is existential in the fuel). **Remaining (R2-loops):**
-  `Loop`/`Br`/`BrIf` + `while`/`for`/`break`/`continue` — backward jumps reuse
-  the same fuel device, plus a source divergence model.
-| Closed the toy K-1's "`if`/control is the next increment" gap. The remaining
-  value-returning-tail story lets **F-2** (#601) be settled *concretely*: the
-  statement-tail vs expression-tail lowerings become two real `instr` sequences
-  whose `wexec` agreement (unit) / divergence (value-returning) is a theorem.
+| **R2** ✅ (conditionals + loops)
+| Structured control. **Done (conditionals):** the `IfElse` instruction
+  (lib/wasm.ml's `If`) + `RIf` source (`ExprIf`), value-returning. Because
+  `instr` now nests `list instr`, the structural `wexec` is guard-rejected, so
+  `wexec` became **fuel-indexed** (`wexec_mono` + `wexec_app_some` replace the
+  clean `wexec_seq`; the theorem is existential in the fuel). **Done (R2-loops,
+  `RealLoop.v`):** the `Block`/`Loop`/`Br`/`BrIf` instructions + a *branch-aware*
+  executor `cexec` (outcome = Normal / Branch k / Trap) that handles the
+  backward jump (a `Loop` consumed by `Br 0` re-enters, reusing the same fuel
+  device), the R2 expression compiler lifted into it (`cexec_compile`), a source
+  `while`/`seq`/`set` statement language, and `compile_stmt_correct` — a
+  terminating `while`'s lowering (`Block[Loop[…;BrIf 1;…;Br 0]]`) simulates the
+  reference `run_stmt`. (`for`/`break`/`continue` reuse the same machinery; an
+  RLet-scratch / general source divergence model is the residual.)
+| Closed the toy K-1's "`if`/control is the next increment" gap, then the loop
+  gap. **F-2** (#601) is now settled *concretely*: a `while` is a *statement*,
+  and its lowering's `cexec` ends with an **empty value stack** (the unit tail) —
+  a theorem — versus the expression tail, which keeps its value on the stack.
 
 | **R-mem**
 | Linear memory: load/store family, `MemorySize/Grow`, a byte-addressed memory
@@ -222,14 +228,25 @@ proven against).
 
 == 5. Hard parts and the strategy for each
 
-* **Nested control & termination — DONE for conditionals (R2).** Because `instr`
-  nests `list instr` (the `IfElse` branches), even *forward* structured control
-  defeats Coq's structural guard checker — so `wexec` is already **fuel-indexed**
-  as of R2 (`wexec : nat → …`), with the standard monotonicity lemma
-  (`wexec_mono`: more fuel never changes a `Some` result) and an additive
-  sequencing lemma (`wexec_app_some`) replacing the structural `wexec_seq`;
-  preservation is stated existentially in the fuel. Backward jumps (`Loop`/`Br`,
-  and the source `while`/`for`) reuse the very same device — that is R2-loops.
+* **Nested control & termination — DONE for conditionals *and* loops (R2 +
+  R2-loops).** Because `instr` nests `list instr` (the `IfElse`/`Block`/`Loop`
+  branches), even *forward* structured control defeats Coq's structural guard
+  checker — so `wexec` is **fuel-indexed** as of R2 (`wexec : nat → …`), with the
+  standard monotonicity lemma (`wexec_mono`) and additive sequencing
+  (`wexec_app_some`) replacing the structural `wexec_seq`; preservation is
+  existential in the fuel. Backward jumps (`Loop`/`Br`, and the source
+  `while`/`for`) reuse the very same device — that is R2-loops (`RealLoop.v`),
+  **done**: a `Loop` consumed by `Br 0` recurses with decremented fuel, so the
+  loop stays a structural `Fixpoint`. Because the R2 `wexec` returns
+  `option (locals×stack)` and so cannot express "branched to label k", R2-loops
+  introduces a branch-aware `cexec` (outcome = `ONormal`/`OBranch k`/`OTrap`)
+  with its own `cexec_mono` + `cexec_app_normal`; the R2 expression compiler is
+  re-proved into it (`cexec_compile`), and `compile_stmt_correct` shows a
+  terminating source `while` simulates its `Block[Loop[…]]` lowering. The
+  guard-checker also rejects a *mutual* `instr`/`list instr` "branch-free"
+  predicate (list recursion only decreases on the spine), which is why the
+  bridge is the direct `cexec_compile` re-proof rather than a `wexec`→`cexec`
+  lift over a `branchfree` flag.
 * **Linear memory.** Model memory as `Z → byte` (or a finite map) + a bound;
   load/store mirror `lib/wasm.ml`'s align/offset. The allocator
   (`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`,
   in the fuel. (The R1 arity lemma `wexec_sound`/`wcheck` was retired in the fuel
   refactor; it can be restated over fuel later, but is not load-bearing —
   `compile_correct` is.) Axiom-free.
-* Next: **R2-loops** — `Loop`/`Br` + source `while`/`for` on the same fuel
-  device; this is the rung that settles #601 concretely.
+* **R2-loops landed** — `RealWasm.v` grown with `Block`/`Loop`/`Br`/`BrIf`
+  (faithful lib/wasm.ml structured control), zero blast radius on the proven
+  `wexec`. `RealLoop.v` adds the branch-aware executor `cexec` (outcome
+  `ONormal`/`OBranch k`/`OTrap`; a `Br 0` to a `Loop` re-enters via decremented
+  fuel) with `cexec_mono` + `cexec_app_normal`, lifts the R2 expression compiler
+  into it (`cexec_compile`), defines a source `while`/`seq`/`set` statement
+  language (`run_stmt`/`compile_stmt`), and proves `compile_stmt_correct`: a
+  terminating `while` lowered to `Block[Loop[…;BrIf 1;…;Br 0]]` simulates the
+  reference run, ending with an **empty value stack** — the unit/statement tail,
+  settling **#601** concretely. Axiom-free; 19 files / 33 closure reports.
+* Next: **R-mem** — linear memory (load/store, byte model) for tuples/arrays/
+  records; then R-float / R-str / R-call per the ladder. (`for`/`break`/
+  `continue` and a general source-divergence model reuse the R2-loops `cexec`.)
 
 Tracked against `docs/PROOF-NEEDS.adoc` §6 Wave 3 and #513.