feat(formal): real-lift R1 — first real ⟦compile p⟧ = ⟦p⟧ (RealCompile.v)

.hypatia-ignore

@@ -82,3 +82,5 @@ cicd_rules/banned_language_file:formal/RealWasm.v
 # not a glob, so a new .v needs its own lines).
 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

docs/PROOF-NEEDS.adoc

@@ -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 — **16 files, 27 `Print
+  **exists** (Coq/Rocq 8.18), axiom-free throughout — **17 files, 29 `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).
@@ -83,7 +83,9 @@ than the prose corpus suggests:
   Affine/QTT layer: `QttSemiring.v` (`{0,1,ω}`) +
   `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). See <<outstanding>>, <<faces>>.
+  β-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⟧`). 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,
@@ -223,11 +225,14 @@ 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); its first stone is
-  **landed** — `formal/RealWasm.v` (R0) re-targets the *actual* `lib/wasm.ml`
-  `instr`/`value_type` with a stack-arity soundness theorem (checked code never
-  traps). R1 (real `RealAst`/`RealAstSem`/`RealCompile` for the int/bool/let
-  fragment) is the first real `⟦compile p⟧ = ⟦p⟧`.
+  `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.
 * **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
@@ -399,11 +404,14 @@ 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 landed**
-  (`formal/RealWasm.v` — real `lib/wasm.ml` IR, i32 core, arity soundness). 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) pending #553.
+  (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
+  #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)
+  pending #553.
 | Wave 2; #555; #553
 |===
 

formal/README.adoc

@@ -96,8 +96,14 @@ cannot mistake it. Coq has no `v.mod` manifest, so `vmod_detected` never fires.
 | **mechanized**, axiom-free
 
 | `RealWasm.v`
-| **Real lift R0** (`REAL-LIFT.adoc`) — the real `lib/wasm.ml` IR (i32 core):
-  `wexec` + arity checker + soundness (`wexec_sound`: checked code never traps)
+| **Real lift R0+R1** (`REAL-LIFT.adoc`) — the real `lib/wasm.ml` IR: i32 core +
+  locals (`LocalGet`/`LocalSet`) + comparisons; `wexec`, `wexec_sound`
+| **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)
 | **mechanized**, axiom-free
 |===
 
@@ -220,17 +226,28 @@ 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)
-
-`RealWasm.v` is the first foundation stone of the *real lift* — replacing the
-toy stack machine with the actual `lib/wasm.ml` IR. R0 covers the pure i32
-numeric core (real `instr` / `value_type` names), a stack-machine `wexec`, an
-arity checker `wcheck`, and the soundness theorem `wexec_sound`: arity-checked
-code never gets stuck — the target-side invariant the real K-1 preservation
-proof rests on. The full plan — the fragment ladder R0 → R1 → 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, linear memory, floats, the
-elaboration nodes, effects) — is `formal/REAL-LIFT.adoc`.
+== The real lift (R0 → R1)
+
+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:
+
+* **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.
+* **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`.
 
 == Scope (honest)
 

formal/REAL-LIFT.adoc

@@ -126,16 +126,19 @@ arity-checked code never gets stuck). That is the first real foundation stone.
 
 | `RealAst.v`
 | The real source `expr`/`stmt`/`program` inductives (faithful to `lib/ast.ml`),
-  per-fragment.
-| planned (S0)
+  per-fragment. (R1's `rexpr` core lives inline in `RealCompile.v`; split out as
+  the fragment grows.)
+| R1 inline
 
 | `RealAstSem.v`
 | The reference dynamic semantics (mirrors `lib/interp.ml`), per-fragment.
-| planned (S0)
+  (R1's `eval` lives inline in `RealCompile.v`.)
+| R1 inline
 
 | `RealCompile.v`
-| The real `compile` (port of `lib/codegen.ml`), per-fragment.
-| planned (K-1/R1)
+| The real `compile` (port of `lib/codegen.ml`) + (for R1) the source `rexpr`
+  core, reference `eval`, and the preservation theorem `compile_correct`.
+| **R1 landed**
 
 | `RealPreservation.v`
 | `⟦compile p⟧ = ⟦p⟧` — the real K-1, per-fragment; then re-chains
@@ -157,11 +160,14 @@ next. The rung names are stable references the `PROOF-NEEDS.adoc` rows will cite
   `wexec` + arity soundness. (`RealWasm.v`)
 | The toy stack machine's *target* — real names now.
 
-| **R1**
-| Source side S0+S1: `ExprLit`/`ExprVar`/`ExprLet`/`ExprBinary` (int/bool) →
-  `RealAst.v` + `RealAstSem.v`; `compile` for them (`RealCompile.v`); locals
-  (`LocalGet/Set/Tee`) + i64 in `RealWasm.v`. First real `⟦compile p⟧=⟦p⟧`.
-| Subsumes **K1** and **K1Let** on real objects.
+| **R1** ✅
+| Source `ExprLit`/`ExprVar`/`ExprLet`/`ExprBinary` (int/bool), resolved to
+  de Bruijn levels — `rexpr` + reference `eval` + `compile` + the preservation
+  theorem `compile_correct` (`RealCompile.v`); **locals** (`LocalGet`/`LocalSet`)
+  + comparison ops added to `RealWasm.v`. First real `⟦compile p⟧=⟦p⟧`, run from
+  the zero-initialised locals array (`compile_program_correct`). (`LocalTee`/i64
+  fold in with R2/R-wrap.)
+| **Subsumes K1 and K1Let on real objects.**
 
 | **R2**
 | Structured control: `Block/Loop/If/Br/BrIf/Return`; `ExprIf`/`ExprMatch`/
@@ -269,9 +275,15 @@ 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 code never traps), axiom-free.
-* Next: **R1** — stand up `RealAst.v` + `RealAstSem.v` + `RealCompile.v` for the
-  int/bool/let/binary fragment and prove the first real `⟦compile p⟧ = ⟦p⟧`,
-  adding locals + i64 to `RealWasm.v`.
+  `wcheck`, `wexec_sound` (arity-checked, local-free code never traps), 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.
 
 Tracked against `docs/PROOF-NEEDS.adoc` §6 Wave 3 and #513.

formal/RealCompile.v

@@ -0,0 +1,206 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+
+(*
+   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.
+
+   `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
+*)
+
+Require Import List.
+Require Import ZArith.
+Require Import PeanoNat.
+Require Import Lia.
+Require Import ASFormal.RealWasm.
+Import ListNotations.
+
+(* ── source: the resolved R1 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).
+
+Definition lit_val (l : lit) : Z :=
+  match l with LInt z => z | LBool b => if b then 1 else 0 end.
+
+Definition bop_val (b : bop) (a c : Z) : Z :=
+  match b with
+  | BAdd => Z.add a c | BSub => Z.sub a c | BMul => Z.mul a c
+  | BAnd => Z.land a c | BOr => Z.lor a c
+  | BEq  => if Z.eqb a c then 1 else 0
+  | BLt  => if Z.ltb a c then 1 else 0
+  end.
+
+(* ── reference semantics (mirrors lib/interp.ml): env = level-indexed list ── *)
+Fixpoint eval (env : list Z) (e : rexpr) : option Z :=
+  match e with
+  | 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
+  | RBin b e1 e2 =>
+      match eval env e1, eval env e2 with
+      | Some a, Some c => Some (bop_val b a c)
+      | _, _ => None
+      end
+  end.
+
+(* ── compiler (mirrors lib/codegen.ml): d = binding depth = next free slot ── *)
+Definition bop_instr (b : bop) : instr :=
+  match b with
+  | BAdd => I32Add | BSub => I32Sub | BMul => I32Mul
+  | BAnd => I32And | BOr => I32Or
+  | BEq  => I32Eq  | BLt => I32LtS
+  end.
+
+Fixpoint compile (d : nat) (e : rexpr) : list instr :=
+  match e with
+  | RLit l => [I32Const (lit_val l)]
+  | 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]
+  end.
+
+(* max extra local slots e needs above its starting depth. *)
+Fixpoint depth (e : rexpr) : nat :=
+  match e with
+  | RLit _ | RVar _ => 0
+  | RLet e1 e2 => Nat.max (depth e1) (S (depth e2))
+  | RBin _ e1 e2 => Nat.max (depth e1) (depth e2)
+  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).
+Proof. destruct b; reflexivity. Qed.
+
+(* ── agreement: locals' first |env| slots hold env ────────────────────────── *)
+Definition agree (env locals : list Z) : Prop :=
+  forall i, i < length env -> nth_error locals i = nth_error env i.
+
+(* ── the preservation theorem ─────────────────────────────────────────────── *)
+Lemma compile_correct : forall e env d locals st v,
+  eval env e = Some v ->
+  length env = d ->
+  agree env locals ->
+  d + depth e <= length locals ->
+  exists locals',
+    wexec (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 ];
+    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].
+    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].
+    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]]].
+    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.
+      destruct (Nat.eq_dec j d) as [->|Hjd].
+      - rewrite set_nth_eq by lia.
+        rewrite nth_error_app2 by lia. rewrite Hlen, Nat.sub_diag. reflexivity.
+      - rewrite set_nth_neq by lia. rewrite Hlow1 by lia.
+        rewrite (Hagree j) by lia. rewrite nth_error_app1 by lia. reflexivity. }
+    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].
+      assert (Hltb : Nat.ltb d (length locals1) = true) by (apply Nat.ltb_lt; lia).
+      rewrite Hltb. reflexivity.
+    + rewrite Hlen2, set_nth_length. exact Hlen1.
+    + intros j Hj. rewrite Hlow2 by lia. rewrite set_nth_neq by lia. apply Hlow1; lia.
+  - (* RBin b e1 e2 *)
+    cbn in Heval.
+    destruct (eval env e1) as [v1|] eqn:Hev1; cbn in Heval; [| discriminate].
+    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]]].
+    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.
+    + rewrite Hlen2. exact Hlen1.
+    + intros j Hj. rewrite Hlow2 by lia. apply Hlow1; 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]).
+Proof.
+  intros e v Heval.
+  destruct (compile_correct e [] 0 (repeat 0%Z (depth e)) [] v Heval)
+    as [locals' [Hw _]].
+  - reflexivity.
+  - intros i Hi; cbn in Hi; lia.
+  - rewrite repeat_length; lia.
+  - exists locals'; exact Hw.
+Qed.
+
+(* concrete: let x = 2+3 in x*4  ⇒  20, end-to-end. *)
+Example r1_eval_demo :
+  eval [] (RLet (RBin BAdd (RLit (LInt 2)) (RLit (LInt 3)))
+                (RBin BMul (RVar 0) (RLit (LInt 4)))) = Some 20%Z.
+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] []
+  = Some ([5%Z], [20%Z]).
+Proof. reflexivity. Qed.
+
+Print Assumptions compile_correct.
+Print Assumptions compile_program_correct.