feat(formal): real-lift R2 — structured conditionals (fuel-indexed wexec)

docs/PROOF-NEEDS.adoc

@@ -84,9 +84,10 @@ 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) + `RealCompile.v`
-  (R1: the first real `⟦compile p⟧ = ⟦p⟧`). 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`,
+  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>>.
 * **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,
@@ -236,14 +237,15 @@ The work in flight changes which obligations are *load-bearing* and which are
   fragment compiled to a stack machine — `K1Let_CodegenPreservation.v` grows it
   with de Bruijn variables, `let`, and an environment. The **real lift** onto the
   real AffineScript AST + real typed-WASM semantics is scoped in
-  `formal/REAL-LIFT.adoc` (fragment ladder R0→R-eff); **R0 + R1 landed**.
-  `formal/RealWasm.v` (R0) re-targets the *actual* `lib/wasm.ml`
-  `instr`/`value_type` (i32 core + locals) with a stack-arity soundness theorem;
-  `formal/RealCompile.v` (R1) gives the **first real `⟦compile p⟧ = ⟦p⟧`** —
-  resolved int/bool/`let`/binary source, reference `eval`, `compile` to real
-  wasm, `compile_correct` (env↔locals agreement) + `compile_program_correct`,
-  retiring `K1`/`K1Let` on real objects. R2 (structured control, fuel-indexed) is
-  next, and is the rung that settles #601 concretely.
+  `formal/REAL-LIFT.adoc` (fragment ladder R0→R-eff); **R0 + R1 + R2 landed**.
+  `formal/RealWasm.v` re-targets the *actual* `lib/wasm.ml` `instr`/`value_type`
+  (i32 core + locals + structured `IfElse`); `formal/RealCompile.v` gives the
+  **first real `⟦compile p⟧ = ⟦p⟧`** — resolved int/bool/`let`/binary/**if**
+  source, reference `eval`, `compile` to real wasm, `compile_correct` (env↔locals
+  agreement, existential-fuel) + `compile_program_correct`, retiring `K1`/`K1Let`
+  on real objects. R2's conditionals forced `wexec` to become **fuel-indexed**
+  (nested `list instr` defeats the structural guard checker); R2-loops
+  (`Loop`/`Br`, value-returning tails) is next and settles #601 concretely.
 * **K-2 — Effect-soundness is *blocked*, not merely unproven.** P-6 cannot be
   honestly *stated against the current backend* because #555 drops handler arms
   on three of the codegen targets. The obligation must be split: (a) prove
@@ -415,10 +417,11 @@ F-1 (full transformer preservation) is non-trivial rather than a formality.
   the **real typed-WASM operational semantics**, then re-prove K-1/F-1/F-2 against
   them (this is what makes K-1/F-1 `XL`, and what actually resolves #601). Planned
   as a strict-superset *fragment ladder* in `formal/REAL-LIFT.adoc`
-  (R0→R1→R2→R-mem→R-float→R-str→R-call→R-wrap→R-eff); **R0 + R1 landed**
-  (`formal/RealWasm.v` — real `lib/wasm.ml` IR, i32 core + locals;
-  `formal/RealCompile.v` — the first real `⟦compile p⟧ = ⟦p⟧`, retiring K1/K1Let
-  on real objects). **R2** (structured control, fuel-indexed) is next and settles
+  (R0→R1→R2→R-mem→R-float→R-str→R-call→R-wrap→R-eff); **R0 + R1 + R2 landed**
+  (`formal/RealWasm.v` — real `lib/wasm.ml` IR, i32 core + locals + structured
+  `IfElse`, fuel-indexed `wexec`; `formal/RealCompile.v` — the first real
+  `⟦compile p⟧ = ⟦p⟧` incl. value-returning `if`, retiring K1/K1Let on real
+  objects). **R2-loops** (`Loop`/`Br`, value-returning tails) is next and settles
   #601 concretely. Then the still-`prose`/`absent` obligations: P-5 (inference),
   P-6 (effects — blocked on #555/K-2, = rung R-eff), P-7 (resolution), P-8
   (parser), P-10 (coherence); faces F-6/F-7; full-language borrowing (P-3)

formal/README.adoc

@@ -96,14 +96,15 @@ cannot mistake it. Coq has no `v.mod` manifest, so `vmod_detected` never fires.
 | **mechanized**, axiom-free
 
 | `RealWasm.v`
-| **Real lift R0+R1** (`REAL-LIFT.adoc`) — the real `lib/wasm.ml` IR: i32 core +
-  locals (`LocalGet`/`LocalSet`) + comparisons; `wexec`, `wexec_sound`
+| **Real lift R0+R1+R2** (`REAL-LIFT.adoc`) — the real `lib/wasm.ml` IR: i32 core
+  + locals + comparisons + structured control (`IfElse`); fuel-indexed `wexec`
+  with monotonicity (`wexec_mono`) + additive sequencing (`wexec_app_some`)
 | **mechanized**, axiom-free
 
 | `RealCompile.v`
-| **Real lift R1** — the first *real* `⟦compile p⟧ = ⟦p⟧`: resolved int/bool/`let`
-  source, reference `eval`, `compile` to real wasm, `compile_correct` (retires
-  K1/K1Let on real objects)
+| **Real lift R1+R2** — the first *real* `⟦compile p⟧ = ⟦p⟧`: resolved
+  int/bool/`let`/binop/**if** source, reference `eval`, `compile` to real wasm,
+  `compile_correct` (retires K1/K1Let on real objects)
 | **mechanized**, axiom-free
 
 | `Rows.v`
@@ -231,28 +232,33 @@ 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 → R1)
+== The real lift (R0 → R2)
 
 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. Two rungs are down:
+fragment ladder. Three rungs are down:
 
 * **R0** (`RealWasm.v`) — the pure i32 numeric core (real `instr` / `value_type`
-  names), a stack-machine `wexec`, an arity checker `wcheck`, and `wexec_sound`:
-  arity-checked, local-free code never gets stuck.
+  names) and a stack-machine `wexec`.
 * **R1** (`RealWasm.v` grown with **locals** + comparisons; `RealCompile.v`) —
   the **first real `⟦compile p⟧ = ⟦p⟧`**. The source is the resolved
   (de Bruijn-level) int/bool/`let`/binary core of `lib/ast.ml`; `eval` is the
   reference semantics; `compile` lowers `let` to `LocalSet` into a pre-sized
   locals array. `compile_correct` carries an env↔locals *agreement* invariant
-  with fresh-slot allocation and low-slot preservation through the induction;
-  `compile_program_correct` runs a closed program from the zero-initialised
-  array. This **retires `K1`/`K1Let` on real objects**.
-
-The full plan — the rest of the ladder (R2 → R-mem → R-float → R-str → R-call →
-R-wrap → R-eff), the Coq module structure, and the strategy for each hard part
-(loops/termination via fuel, linear memory, floats, the elaboration nodes,
-effects) — is `formal/REAL-LIFT.adoc`.
+  with fresh-slot allocation and low-slot preservation through the induction.
+  This **retires `K1`/`K1Let` on real objects**.
+* **R2** (`RealWasm.v` grown with structured control `IfElse`; `RealCompile.v`
+  grown with `RIf`) — conditionals. Because `instr` now nests `list instr`, the
+  structural `wexec` is rejected by the guard checker, so `wexec` is now
+  **fuel-indexed**; the clean `wexec_seq` is replaced by `wexec_mono`
+  (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`.
 
 == Record rows (P-11)
 
@@ -276,8 +282,8 @@ These are Wave-0/1 seeds, not the discharged obligations. The fragments are
 deliberately small; the full theorems need the real AffineScript AST and the
 real typed-WASM operational semantics, expanded the way solo-core's
 Duet/Ensemble tracks expand Solo. That expansion has **begun** — see the real
-lift above (`RealWasm.v`, R0) and the plan in `formal/REAL-LIFT.adoc`. Tracked
-in `docs/PROOF-NEEDS.adoc` and #513.
+lift above (`RealWasm.v` / `RealCompile.v`, R0→R2) and the plan in
+`formal/REAL-LIFT.adoc`. Tracked in `docs/PROOF-NEEDS.adoc` and #513.
 
 == Checking
 

formal/REAL-LIFT.adoc

@@ -169,14 +169,18 @@ 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**
-| Structured control: `Block/Loop/If/Br/BrIf/Return`; `ExprIf`/`ExprMatch`/
-  `while`/`for`/`break`/`continue`. Needs a **fuel-indexed** `wexec` (loops may
-  diverge) and the matching source semantics.
-| Closes the toy K-1's "`if`/control is the next increment" gap. 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, not a prose observation.
+| **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.
 
 | **R-mem**
 | Linear memory: load/store family, `MemorySize/Grow`, a byte-addressed memory
@@ -218,11 +222,14 @@ proven against).
 
 == 5. Hard parts and the strategy for each
 
-* **Loops & termination.** Wasm `Loop` can diverge, so `wexec` cannot stay a
-  structural fixpoint past R1. Strategy: **fuel-indexed** big-step
-  (`wexec : nat → …`) with the standard "more fuel never changes a `Some`
-  result" monotonicity lemma; preservation is stated up to fuel. (Same device
-  the source `while`/`for` semantics will use.)
+* **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.
 * **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) —
@@ -274,16 +281,23 @@ already has the front-end scaffolding (`F1_TransformerPreservation.v`,
 
 == 8. Status
 
-* **R0 landed** — `RealWasm.v`: real `instr`/`value_type` names, `wexec`,
-  `wcheck`, `wexec_sound` (arity-checked, local-free code never traps), axiom-free.
+* **R0 landed** — `RealWasm.v`: real `instr`/`value_type` names + a stack-machine
+  `wexec`, axiom-free.
 * **R1 landed** — `RealWasm.v` grown with **locals** (`LocalGet`/`LocalSet`) +
   comparison ops; `RealCompile.v` gives the resolved int/bool/`let`/binary source
   `rexpr`, the reference `eval`, the `compile` to real wasm, and the **first real
   `⟦compile p⟧ = ⟦p⟧`** — `compile_correct` (env↔locals agreement, fresh-slot
-  allocation, low-slot preservation) + `compile_program_correct`. Axiom-free.
-  Retires `K1`/`K1Let` on real objects.
-* Next: **R2** — structured control (`Block`/`Loop`/`If`/`Br`/`Return`,
-  `ExprIf`/`ExprMatch`/`while`) on a fuel-indexed `wexec`; this is the rung that
-  settles #601 concretely.
+  allocation, low-slot preservation) + `compile_program_correct`. Retires
+  `K1`/`K1Let` on real objects.
+* **R2 landed (conditionals)** — `RealWasm.v` grown with the structured `IfElse`
+  instruction; this forced `wexec` to become **fuel-indexed** (the nested
+  `list instr` defeats the structural guard checker), with `wexec_mono` +
+  `wexec_app_some` replacing `wexec_seq`. `RealCompile.v` grows `compile` with
+  `RIf`; `compile_correct` now covers value-returning `if`, stated existentially
+  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.
 
 Tracked against `docs/PROOF-NEEDS.adoc` §6 Wave 3 and #513.