diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc
index b424dd77..1a699a37 100644
--- a/docs/PROOF-NEEDS.adoc
+++ b/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)
diff --git a/formal/README.adoc b/formal/README.adoc
index bee60935..16c51457 100644
--- a/formal/README.adoc
+++ b/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
 
diff --git a/formal/REAL-LIFT.adoc b/formal/REAL-LIFT.adoc
index 5c44bd56..dee7a923 100644
--- a/formal/REAL-LIFT.adoc
+++ b/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.
diff --git a/formal/RealCompile.v b/formal/RealCompile.v
index e97ad61b..884f5591 100644
--- a/formal/RealCompile.v
+++ b/formal/RealCompile.v
@@ -4,28 +4,29 @@
 (*
    RealCompile.v
    ═════════════
-   REAL-LIFT rung R1 (see formal/REAL-LIFT.adoc): the first **real**
-   ⟦compile p⟧ = ⟦p⟧, on the real RealWasm.v target IR.
-
-   Source: the resolved (de Bruijn LEVEL) core of lib/ast.ml — integer/bool
-   literals (ExprLit), variables (ExprVar), let (ExprLet), and binary operators
-   (ExprBinary: + - * & | == <). de Bruijn levels are how lib/codegen.ml sees the
-   AST after lib/resolve.ml — name resolution itself is obligation P-7. Bool ≔
-   0/1, Int ≔ Z, so the single observable is Z.
-
-   `eval` (mirrors lib/interp.ml) is the reference dynamic semantics. `compile`
-   (mirrors lib/codegen.ml) lowers `let` to `LocalSet d` into a pre-sized locals
-   array (slot = binding depth d; siblings reuse slots). The theorem
-   `compile_correct`:
-
-       eval env e = Some v  →  agree env locals  →  d = |env|  →  enough slots →
-         wexec (compile d e) locals st = Some (locals', v :: st)
-         ∧ |locals'| = |locals| ∧ (low slots < d unchanged)
-
-   and the closed-program corollary `compile_program_correct` runs it from the
-   zero-initialised locals array. This RETIRES the toy K1 / K1Let on REAL objects
-   — the target is RealWasm's actual lib/wasm.ml instruction names with mutable
-   locals, not an ad-hoc machine. Axiom-free, no Admitted.
+   REAL-LIFT rungs R1 + R2 (see formal/REAL-LIFT.adoc): the first **real**
+   ⟦compile p⟧ = ⟦p⟧, on the real RealWasm.v target IR, now with **structured
+   conditionals**.
+
+   Source: the resolved (de Bruijn LEVEL) core of lib/ast.ml — int/bool literals
+   (ExprLit), variables (ExprVar), let (ExprLet), binary operators (ExprBinary:
+   + - * & | == <), and **if/else** (ExprIf, value-returning). de Bruijn levels
+   are how lib/codegen.ml sees the AST after lib/resolve.ml (name resolution is
+   obligation P-7). Bool ≔ 0/1, Int ≔ Z, one observable Z.
+
+   `eval` (mirrors lib/interp.ml) is the reference semantics; `compile` (mirrors
+   lib/codegen.ml) lowers `let` to `LocalSet` into a pre-sized locals array and
+   `if` to the structured `IfElse` instruction. Because R2's `wexec` is
+   fuel-indexed, the theorem is stated **existentially in the fuel**:
+
+       eval env e = Some v  →  agree env locals  →  |env| = d  →  enough slots →
+         ∃ fuel locals', wexec fuel (compile d e) locals st = Some (locals', v :: st)
+           ∧ |locals'| = |locals| ∧ (low slots < d unchanged)
+
+   The fuel of a compound is the *sum* of its parts' fuels (via wexec_app_some),
+   and the branch taken by `if` is run with monotonically-padded fuel
+   (wexec_le_S). Closed-program corollary runs it from the zero-init array.
+   Retires the toy K1/K1Let on REAL objects. Axiom-free, no Admitted.
 
    `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
 *)
@@ -37,14 +38,15 @@ Require Import Lia.
 Require Import ASFormal.RealWasm.
 Import ListNotations.
 
-(* ── source: the resolved R1 core of lib/ast.ml ───────────────────────────── *)
+(* ── source: the resolved R1+R2 core of lib/ast.ml ────────────────────────── *)
 Inductive lit := LInt (z : Z) | LBool (b : bool).
 Inductive bop := BAdd | BSub | BMul | BAnd | BOr | BEq | BLt.
 Inductive rexpr :=
 | RLit (l : lit)
-| RVar (i : nat)              (* de Bruijn LEVEL: outermost binder = 0 *)
-| RLet (e1 e2 : rexpr)        (* let _ = e1 in e2 *)
-| RBin (b : bop) (e1 e2 : rexpr).
+| RVar (i : nat)                    (* de Bruijn LEVEL: outermost binder = 0 *)
+| RLet (e1 e2 : rexpr)              (* let _ = e1 in e2 *)
+| RBin (b : bop) (e1 e2 : rexpr)
+| RIf (c thn els : rexpr).          (* if c then thn else els (value-returning) *)
 
 Definition lit_val (l : lit) : Z :=
   match l with LInt z => z | LBool b => if b then 1 else 0 end.
@@ -63,14 +65,14 @@ Fixpoint eval (env : list Z) (e : rexpr) : option Z :=
   | RLit l => Some (lit_val l)
   | RVar i => nth_error env i
   | RLet e1 e2 =>
-      match eval env e1 with
-      | Some v1 => eval (env ++ [v1]) e2
-      | None => None
-      end
+      match eval env e1 with Some v1 => eval (env ++ [v1]) e2 | None => None end
   | RBin b e1 e2 =>
       match eval env e1, eval env e2 with
-      | Some a, Some c => Some (bop_val b a c)
-      | _, _ => None
+      | Some a, Some c => Some (bop_val b a c) | _, _ => None end
+  | RIf c thn els =>
+      match eval env c with
+      | Some vc => if Z.eqb vc 0 then eval env els else eval env thn
+      | None => None
       end
   end.
 
@@ -88,6 +90,7 @@ Fixpoint compile (d : nat) (e : rexpr) : list instr :=
   | RVar i => [LocalGet i]
   | RLet e1 e2 => compile d e1 ++ [LocalSet d] ++ compile (S d) e2
   | RBin b e1 e2 => compile d e1 ++ compile d e2 ++ [bop_instr b]
+  | RIf c thn els => compile d c ++ [IfElse (compile d thn) (compile d els)]
   end.
 
 (* max extra local slots e needs above its starting depth. *)
@@ -96,11 +99,12 @@ Fixpoint depth (e : rexpr) : nat :=
   | RLit _ | RVar _ => 0
   | RLet e1 e2 => Nat.max (depth e1) (S (depth e2))
   | RBin _ e1 e2 => Nat.max (depth e1) (depth e2)
+  | RIf c thn els => Nat.max (depth c) (Nat.max (depth thn) (depth els))
   end.
 
 (* the binop instruction realises bop_val on the (reversed) operand stack. *)
-Lemma step1_bop : forall b lo v1 v2 t,
-  step1 (bop_instr b) lo (v2 :: v1 :: t) = Some (lo, bop_val b v1 v2 :: t).
+Lemma wexec_bop : forall b lo v1 v2 t,
+  wexec 2 [bop_instr b] lo (v2 :: v1 :: t) = Some (lo, bop_val b v1 v2 :: t).
 Proof. destruct b; reflexivity. Qed.
 
 (* ── agreement: locals' first |env| slots hold env ────────────────────────── *)
@@ -113,28 +117,28 @@ Lemma compile_correct : forall e env d locals st v,
   length env = d ->
   agree env locals ->
   d + depth e <= length locals ->
-  exists locals',
-    wexec (compile d e) locals st = Some (locals', v :: st) /\
+  exists fuel locals',
+    wexec fuel (compile d e) locals st = Some (locals', v :: st) /\
     length locals' = length locals /\
     (forall i, i < d -> nth_error locals' i = nth_error locals i).
 Proof.
-  induction e as [ l | i | e1 IH1 e2 IH2 | b e1 IH1 e2 IH2 ];
+  induction e as [ l | i | e1 IH1 e2 IH2 | b e1 IH1 e2 IH2 | c IHc thn IHthn els IHels ];
     intros env d locals st v Heval Hlen Hagree Hbound; cbn [depth] in Hbound.
   - (* RLit *)
     cbn in Heval. injection Heval as Hv; subst v.
-    exists locals. cbn [compile wexec step1].
+    exists 2, locals.
     split; [reflexivity | split; [reflexivity | intros; reflexivity]].
   - (* RVar i *)
     cbn in Heval.
     assert (Hi : i < length env) by (apply nth_error_Some; rewrite Heval; discriminate).
-    exists locals. cbn [compile wexec step1].
+    exists 2, locals. cbn [compile wexec step1].
     rewrite (Hagree i Hi), Heval. cbn.
     split; [reflexivity | split; [reflexivity | intros; reflexivity]].
   - (* RLet e1 e2 *)
     cbn in Heval.
     destruct (eval env e1) as [v1|] eqn:Hev1; cbn in Heval; [| discriminate].
     destruct (IH1 env d locals st v1 Hev1 Hlen Hagree ltac:(lia))
-      as [locals1 [Hw1 [Hlen1 Hlow1]]].
+      as [f1 [locals1 [Hw1 [Hlen1 Hlow1]]]].
     assert (Hd : d < length locals1) by lia.
     assert (Hag2 : agree (env ++ [v1]) (set_nth d v1 locals1)).
     { intros j Hj. rewrite app_length in Hj; cbn in Hj.
@@ -146,11 +150,11 @@ Proof.
     destruct (IH2 (env ++ [v1]) (S d) (set_nth d v1 locals1) st v Heval
                   ltac:(rewrite app_length; cbn; lia) Hag2
                   ltac:(rewrite set_nth_length; lia))
-      as [locals2 [Hw2 [Hlen2 Hlow2]]].
-    exists locals2. split; [| split].
-    + apply wexec_seq with (lo1:=locals1) (st1:=v1::st); [exact Hw1|].
-      apply wexec_seq with (lo1:=set_nth d v1 locals1) (st1:=st); [| exact Hw2].
-      cbn [wexec step1].
+      as [f2 [locals2 [Hw2 [Hlen2 Hlow2]]]].
+    exists (f1 + (2 + f2)), locals2. split; [| split].
+    + apply wexec_app_some with (lo1:=locals1) (st1:=v1::st); [exact Hw1|].
+      apply wexec_app_some with (lo1:=set_nth d v1 locals1) (st1:=st); [| exact Hw2].
+      rewrite wexec_S_cons. cbn [step1].
       assert (Hltb : Nat.ltb d (length locals1) = true) by (apply Nat.ltb_lt; lia).
       rewrite Hltb. reflexivity.
     + rewrite Hlen2, set_nth_length. exact Hlen1.
@@ -161,33 +165,60 @@ Proof.
     destruct (eval env e2) as [v2|] eqn:Hev2; cbn in Heval; [| discriminate].
     injection Heval as Hv; subst v.
     destruct (IH1 env d locals st v1 Hev1 Hlen Hagree ltac:(lia))
-      as [locals1 [Hw1 [Hlen1 Hlow1]]].
+      as [f1 [locals1 [Hw1 [Hlen1 Hlow1]]]].
     assert (Hag1 : agree env locals1).
     { intros j Hj. rewrite Hlow1 by lia. apply Hagree; lia. }
-    destruct (IH2 env d locals1 (v1 :: st) v2 Hev2 Hlen Hag1
-                  ltac:(rewrite Hlen1; lia))
-      as [locals2 [Hw2 [Hlen2 Hlow2]]].
-    exists locals2. split; [| split].
-    + apply wexec_seq with (lo1:=locals1) (st1:=v1::st); [exact Hw1|].
-      apply wexec_seq with (lo1:=locals2) (st1:=v2::v1::st); [exact Hw2|].
-      cbn [wexec]. rewrite step1_bop. reflexivity.
+    destruct (IH2 env d locals1 (v1 :: st) v2 Hev2 Hlen Hag1 ltac:(rewrite Hlen1; lia))
+      as [f2 [locals2 [Hw2 [Hlen2 Hlow2]]]].
+    exists (f1 + (f2 + 2)), locals2. split; [| split].
+    + apply wexec_app_some with (lo1:=locals1) (st1:=v1::st); [exact Hw1|].
+      apply wexec_app_some with (lo1:=locals2) (st1:=v2::v1::st); [exact Hw2|].
+      exact (wexec_bop b locals2 v1 v2 st).
     + rewrite Hlen2. exact Hlen1.
     + intros j Hj. rewrite Hlow2 by lia. apply Hlow1; lia.
+  - (* RIf c thn els *)
+    change (compile d (RIf c thn els))
+      with (compile d c ++ [IfElse (compile d thn) (compile d els)]).
+    cbn in Heval.
+    destruct (eval env c) as [vc|] eqn:Hevc; cbn in Heval; [| discriminate].
+    destruct (IHc env d locals st vc Hevc Hlen Hagree ltac:(lia))
+      as [fc [lc [Hwc [Hlenc Hlowc]]]].
+    assert (Hagc : agree env lc).
+    { intros j Hj. rewrite Hlowc by lia. apply Hagree; lia. }
+    destruct (Z.eqb vc 0) eqn:Hvc; cbn in Heval.
+    + (* vc = 0 → els *)
+      destruct (IHels env d lc st v Heval Hlen Hagc ltac:(lia))
+        as [fe [le [Hwe [Hlene Hlowe]]]].
+      exists (fc + S (S fe)), le. split; [| split].
+      * apply wexec_app_some with (lo1:=lc) (st1:=vc::st); [exact Hwc|].
+        rewrite wexec_ifelse, Hvc; cbn [step1].
+        rewrite (wexec_le_S _ _ _ _ _ Hwe); reflexivity.
+      * rewrite Hlene. exact Hlenc.
+      * intros j Hj. rewrite Hlowe by lia. apply Hlowc; lia.
+    + (* vc <> 0 → thn *)
+      destruct (IHthn env d lc st v Heval Hlen Hagc ltac:(lia))
+        as [ft [lt [Hwt [Hlent Hlowt]]]].
+      exists (fc + S (S ft)), lt. split; [| split].
+      * apply wexec_app_some with (lo1:=lc) (st1:=vc::st); [exact Hwc|].
+        rewrite wexec_ifelse, Hvc; cbn [step1].
+        rewrite (wexec_le_S _ _ _ _ _ Hwt); reflexivity.
+      * rewrite Hlent. exact Hlenc.
+      * intros j Hj. rewrite Hlowt by lia. apply Hlowc; lia.
 Qed.
 
 (* ── closed-program corollary ─────────────────────────────────────────────── *)
 Corollary compile_program_correct : forall e v,
   eval [] e = Some v ->
-  exists locals',
-    wexec (compile 0 e) (repeat 0%Z (depth e)) [] = Some (locals', [v]).
+  exists fuel locals',
+    wexec fuel (compile 0 e) (repeat 0%Z (depth e)) [] = Some (locals', [v]).
 Proof.
   intros e v Heval.
   destruct (compile_correct e [] 0 (repeat 0%Z (depth e)) [] v Heval)
-    as [locals' [Hw _]].
+    as [fuel [locals' [Hw _]]].
   - reflexivity.
   - intros i Hi; cbn in Hi; lia.
   - rewrite repeat_length; lia.
-  - exists locals'; exact Hw.
+  - exists fuel, locals'; exact Hw.
 Qed.
 
 (* concrete: let x = 2+3 in x*4  ⇒  20, end-to-end. *)
@@ -197,10 +228,17 @@ Example r1_eval_demo :
 Proof. reflexivity. Qed.
 
 Example r1_exec_demo :
-  wexec (compile 0 (RLet (RBin BAdd (RLit (LInt 2)) (RLit (LInt 3)))
-                         (RBin BMul (RVar 0) (RLit (LInt 4))))) [0%Z] []
+  wexec 20 (compile 0 (RLet (RBin BAdd (RLit (LInt 2)) (RLit (LInt 3)))
+                            (RBin BMul (RVar 0) (RLit (LInt 4))))) [0%Z] []
   = Some ([5%Z], [20%Z]).
 Proof. reflexivity. Qed.
 
+(* R2: if (1 < 2) then 11 else 22  ⇒  11, end-to-end. *)
+Example r2_if_demo :
+  wexec 20 (compile 0 (RIf (RBin BLt (RLit (LInt 1)) (RLit (LInt 2)))
+                           (RLit (LInt 11)) (RLit (LInt 22)))) [] []
+  = Some ([], [11%Z]).
+Proof. reflexivity. Qed.
+
 Print Assumptions compile_correct.
 Print Assumptions compile_program_correct.
diff --git a/formal/RealWasm.v b/formal/RealWasm.v
index 6f256b36..6113cd3e 100644
--- a/formal/RealWasm.v
+++ b/formal/RealWasm.v
@@ -6,15 +6,17 @@
    ══════════
    The REAL-LIFT target IR (see formal/REAL-LIFT.adoc). Grows across rungs.
 
-   R0 — pure i32 numeric stack core (real lib/wasm.ml instr/value_type names),
-        stack-machine wexec, arity checker wcheck, soundness wexec_sound.
-   R1 — adds **locals** (LocalGet/LocalSet) and the comparison ops I32Eq/I32LtS,
-        threading a mutable locals store through wexec. wexec is refactored
-        through a per-instruction `step1`, so the append lemma `wexec_app`
-        (the sequencing lemma RealCompile.v's preservation proof composes with)
-        is one line. wexec_sound is retained for the **pure** (`no_local`)
-        fragment: arity-checked local-free code never traps and never touches
-        the locals.
+   R0 — pure i32 numeric stack core (real lib/wasm.ml instr/value_type names).
+   R1 — adds **locals** (LocalGet/LocalSet) + comparison ops I32Eq/I32LtS.
+   R2 — adds **structured control**: `IfElse thn els` (lib/wasm.ml's `If`, minus
+        the block_type validation annotation). Because `instr` now nests
+        `list instr`, a *structural* `wexec` is rejected by Coq's guard checker —
+        so `wexec` becomes **fuel-indexed** (decreasing on the `nat` fuel), as
+        REAL-LIFT.adoc anticipated for R2. Fuel keeps definitional computation
+        (`cbn`/`reflexivity` still work), at the cost of the old one-line
+        `wexec_seq`: composition is recovered via monotonicity (`wexec_mono`:
+        more fuel preserves a `Some` result) + the additive sequencing lemma
+        `wexec_app_some`. (Backward jumps — `Loop`/`Br` — are the next sub-rung.)
 
    i32 ≔ Z (wrap deferred to rung R-wrap). Axiom-free, no Admitted.
    `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
@@ -29,7 +31,7 @@ Import ListNotations.
 (* lib/wasm.ml `value_type` — full, faithful. *)
 Inductive value_type := I32 | I64 | F32 | F64.
 
-(* R0 i32 core + R1 (comparisons + locals), real lib/wasm.ml names. *)
+(* R0 i32 core + R1 (comparisons + locals) + R2 (structured control). *)
 Inductive instr :=
 | I32Const (z : Z)
 | I32Add | I32Sub | I32Mul
@@ -38,7 +40,8 @@ Inductive instr :=
 | I32Eqz
 | Drop
 | LocalGet (i : nat)             (* R1: locals *)
-| LocalSet (i : nat).
+| LocalSet (i : nat)
+| IfElse (thn els : list instr). (* R2: lib/wasm.ml `If` (sans block_type) *)
 
 Definition stack  := list Z.
 Definition locals := list Z.
@@ -68,7 +71,8 @@ Proof.
   - apply IHi; lia.
 Qed.
 
-(* one-instruction step over (locals, stack). None = trap (underflow / oob). *)
+(* one straight-line instruction step. IfElse is handled by wexec (it recurses
+   into a sub-list), so step1 never sees it — the dead arm returns None. *)
 Definition step1 (i : instr) (lo : locals) (st : stack) : option (locals * stack) :=
   match i with
   | I32Const z => Some (lo, z :: st)
@@ -87,100 +91,117 @@ Definition step1 (i : instr) (lo : locals) (st : stack) : option (locals * stack
                   | v :: t => if Nat.ltb k (length lo) then Some (set_nth k v lo, t) else None
                   | [] => None
                   end
+  | IfElse _ _ => None
   end.
 
-Fixpoint wexec (is : list instr) (lo : locals) (st : stack) : option (locals * stack) :=
-  match is with
-  | [] => Some (lo, st)
-  | i :: r => match step1 i lo st with
-              | Some (lo', st') => wexec r lo' st'
-              | None => None
-              end
+(* fuel-indexed executor. None = trap OR out of fuel. *)
+Fixpoint wexec (fuel : nat) (is : list instr) (lo : locals) (st : stack)
+  : option (locals * stack) :=
+  match fuel with
+  | O => None
+  | S f =>
+    match is with
+    | [] => Some (lo, st)
+    | IfElse thn els :: r =>
+        match st with
+        | c :: t =>
+            match wexec f (if Z.eqb c 0 then els else thn) lo t with
+            | Some (lo', st') => wexec f r lo' st'
+            | None => None
+            end
+        | [] => None
+        end
+    | i :: r =>
+        match step1 i lo st with
+        | Some (lo', st') => wexec f r lo' st'
+        | None => None
+        end
+    end
   end.
 
-(* sequencing — the lemma the preservation proof composes with. *)
-Lemma wexec_app : forall is1 is2 lo st,
-  wexec (is1 ++ is2) lo st =
-  match wexec is1 lo st with Some (lo', st') => wexec is2 lo' st' | None => None end.
-Proof.
-  induction is1 as [| i r IH]; intros is2 lo st; simpl.
-  - reflexivity.
-  - destruct (step1 i lo st) as [[lo' st']|]; [apply IH | reflexivity].
-Qed.
-
-(* the run-then-run composition, in the shape the preservation proof applies. *)
-Lemma wexec_seq : forall is1 is2 lo st lo1 st1 lo2 st2,
-  wexec is1 lo st = Some (lo1, st1) ->
-  wexec is2 lo1 st1 = Some (lo2, st2) ->
-  wexec (is1 ++ is2) lo st = Some (lo2, st2).
-Proof. intros. rewrite wexec_app, H. exact H0. Qed.
-
-(* ── arity discipline (degenerate validation: i32 stack height) ──────────── *)
-Definition consumes (i : instr) : nat :=
+(* one-step unfolding (avoids cbn over-reducing the IfElse branch run). *)
+Lemma wexec_S_cons : forall f i r lo st,
+  wexec (S f) (i :: r) lo st =
   match i with
-  | I32Const _ => 0
-  | LocalGet _ => 0
-  | I32Add | I32Sub | I32Mul | I32And | I32Or | I32Xor | I32Eq | I32LtS => 2
-  | I32Eqz => 1
-  | Drop => 1
-  | LocalSet _ => 1
+  | IfElse thn els =>
+      match st with
+      | c :: t =>
+          match wexec f (if Z.eqb c 0 then els else thn) lo t with
+          | Some (lo', st') => wexec f r lo' st' | None => None end
+      | [] => None end
+  | _ => match step1 i lo st with Some (lo', st') => wexec f r lo' st' | None => None end
   end.
+Proof. intros; destruct i; reflexivity. Qed.
 
-Definition produces (i : instr) : nat :=
-  match i with
-  | Drop => 0
-  | LocalSet _ => 0
-  | _ => 1
-  end.
+(* one-step unfolding of a single structured conditional. *)
+Lemma wexec_ifelse : forall f c tcode ecode lo st,
+  wexec (S f) [IfElse tcode ecode] lo (c :: st) =
+  match wexec f (if Z.eqb c 0 then ecode else tcode) lo st with
+  | Some (lo', st') => wexec f [] lo' st' | None => None end.
+Proof. reflexivity. Qed.
 
-Fixpoint wcheck (is : list instr) (n : nat) : option nat :=
-  match is with
-  | [] => Some n
-  | i :: r =>
-      if Nat.leb (consumes i) n
-      then wcheck r (n - consumes i + produces i)
-      else None
-  end.
+(* ── monotonicity: more fuel never loses a Some result ────────────────────── *)
+Lemma wexec_le_S : forall f is lo st r,
+  wexec f is lo st = Some r -> wexec (S f) is lo st = Some r.
+Proof.
+  induction f as [| f IHf]; intros is lo st r Hw; [discriminate Hw|].
+  destruct is as [| i r0]; [exact Hw|].
+  rewrite wexec_S_cons in Hw; rewrite wexec_S_cons; destruct i;
+    try (destruct (step1 _ lo st) as [[lo' st']|];
+         [ apply IHf; exact Hw | discriminate Hw ]).
+  (* IfElse *)
+  destruct st as [| c t]; [discriminate Hw|].
+  destruct (wexec f (if Z.eqb c 0 then els else thn) lo t) as [[lo' st']|] eqn:Hb;
+    [| discriminate Hw].
+  apply IHf in Hb; rewrite Hb; apply IHf; exact Hw.
+Qed.
 
-(* the pure (local-free) fragment. *)
-Fixpoint no_local (is : list instr) : Prop :=
-  match is with
-  | [] => True
-  | LocalGet _ :: _ => False
-  | LocalSet _ :: _ => False
-  | _ :: r => no_local r
-  end.
+Lemma wexec_mono : forall f f' is lo st r,
+  f <= f' -> wexec f is lo st = Some r -> wexec f' is lo st = Some r.
+Proof.
+  intros f f' is lo st r Hle; induction Hle; intros Hw.
+  - exact Hw.
+  - apply wexec_le_S, IHHle, Hw.
+Qed.
 
-(* ── soundness: arity-checked, local-free code never traps ─────────────────
-   (and never touches the locals). The target invariant for the pure core; the
-   locals-using case is covered operationally + by RealCompile.v's preservation. *)
-Theorem wexec_sound : forall is n m lo st,
-  wcheck is n = Some m -> length st = n -> no_local is ->
-  exists st', wexec is lo st = Some (lo, st') /\ length st' = m.
+(* ── additive sequencing: run is1 with f1, then is2 with f2 ⇒ is1++is2 with
+   f1+f2. The fuel-world replacement for R1's wexec_seq. ─────────────────────── *)
+Lemma wexec_app_some : forall f1 is1 lo st lo1 st1,
+  wexec f1 is1 lo st = Some (lo1, st1) ->
+  forall f2 is2 lo2 st2,
+  wexec f2 is2 lo1 st1 = Some (lo2, st2) ->
+  wexec (f1 + f2) (is1 ++ is2) lo st = Some (lo2, st2).
 Proof.
-  induction is as [| i r IH]; intros n m lo st Hchk Hlen Hnl; cbn in Hchk.
-  - injection Hchk as <-. exists st. split; [reflexivity | exact Hlen].
-  - destruct (Nat.leb (consumes i) n) eqn:Hle; [| discriminate].
-    apply Nat.leb_le in Hle.
-    destruct i; cbn in Hchk, Hle, Hnl |- *;
-      try contradiction;
-      try (eapply IH; [exact Hchk | cbn; lia | exact Hnl]).
-    all: destruct st as [| a [| b t]]; cbn in Hlen |- *;
-         try (exfalso; lia);
-         (eapply IH; [exact Hchk | cbn in Hlen |- *; lia | exact Hnl]).
+  induction f1 as [| f1 IHf1];
+    intros is1 lo st lo1 st1 Hw1 f2 is2 lo2 st2 Hw2; [discriminate Hw1|].
+  destruct is1 as [| i r0].
+  - cbn [wexec] in Hw1. injection Hw1 as Hlo Hst; subst lo1 st1.
+    cbn [app]. apply wexec_mono with (f := f2); [lia | exact Hw2].
+  - rewrite wexec_S_cons in Hw1.
+    cbn [app]; rewrite Nat.add_succ_l, wexec_S_cons; destruct i;
+      try (destruct (step1 _ lo st) as [[lo' st']|];
+           [ exact (IHf1 r0 lo' st' lo1 st1 Hw1 f2 is2 lo2 st2 Hw2)
+           | discriminate Hw1 ]).
+    (* IfElse *)
+    destruct st as [| c t]; [discriminate Hw1|].
+    destruct (wexec f1 (if Z.eqb c 0 then els else thn) lo t) as [[lo' st']|] eqn:Hb;
+      [| discriminate Hw1].
+    rewrite (wexec_mono f1 (f1 + f2) _ lo t _ ltac:(lia) Hb).
+    exact (IHf1 r0 lo' st' lo1 st1 Hw1 f2 is2 lo2 st2 Hw2).
 Qed.
 
-(* concrete sanity checks. *)
+(* concrete sanity checks (generous fuel; monotonic). *)
 Example wexec_demo :
-  wexec [I32Const 2; I32Const 3; I32Add; I32Const 4; I32Mul] [] [] = Some ([], [20%Z]).
+  wexec 10 [I32Const 2; I32Const 3; I32Add; I32Const 4; I32Mul] [] [] = Some ([], [20%Z]).
 Proof. reflexivity. Qed.
 
 Example wexec_local_demo :
-  wexec [I32Const 7; LocalSet 0; LocalGet 0] [0%Z] [] = Some ([7%Z], [7%Z]).
+  wexec 10 [I32Const 7; LocalSet 0; LocalGet 0] [0%Z] [] = Some ([7%Z], [7%Z]).
 Proof. reflexivity. Qed.
 
-Example wcheck_demo :
-  wcheck [I32Const 2; I32Const 3; I32Add; I32Const 4; I32Mul] 0 = Some 1.
+(* if 0 then 11 else 22  ⇒  22  (condition 0 takes the else branch). *)
+Example wexec_if_demo :
+  wexec 10 [I32Const 0; IfElse [I32Const 11] [I32Const 22]] [] [] = Some ([], [22%Z]).
 Proof. reflexivity. Qed.
 
-Print Assumptions wexec_sound.
+Print Assumptions wexec_app_some.