feat(formal): real-lift R0 + scoping plan (RealWasm.v + REAL-LIFT.adoc)

Begins the "real lift" (PROOF-NEEDS.adoc section 6 Wave 3): replacing the toy
proof models with the real AffineScript AST + real typed-WASM semantics.

- formal/REAL-LIFT.adoc: the engineering plan, grounded in lib/ast.ml (the real
  ~30-constructor expr) and lib/wasm.ml (the real WebAssembly-1.0 IR). Defines
  the Coq module structure (RealWasm / RealWasmSem / RealAst / RealAstSem /
  RealCompile / RealPreservation) and a strict-superset fragment ladder
  R0->R1->R2->R-mem->R-float->R-str->R-call->R-wrap->R-eff, each axiom-free
  before the next, with the strategy for each hard part (loops/termination via
  fuel, linear memory, abstract floats, the post-typecheck elaboration nodes,
  effects gated on #555).

- formal/RealWasm.v: R0, the first stone. Re-targets the ACTUAL lib/wasm.ml
  instr/value_type names (vs the toy K-1's ad-hoc machine) for the pure i32
  numeric core, with a stack-machine wexec, an arity checker wcheck, and
  wexec_sound: arity-checked code never gets stuck — the target-side invariant
  the real K-1 preservation proof rests on. i32 modelled as Z (wrap deferred to
  rung R-wrap). Axiom-free.

Wired into _CoqProject / justfile / .hypatia-ignore / README.adoc.
PROOF-NEEDS.adoc: K-1 row + section 6 Wave 3 note R0 landed; formal/ now 16
files, 27 axiom-free closure reports.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr

Author: hyperpolymath

.hypatia-ignore

@@ -73,3 +73,5 @@ cicd_rules/vlang_detected:formal/QttDynamic.v
 cicd_rules/banned_language_file:formal/QttDynamic.v
 cicd_rules/vlang_detected:formal/F5_RenderFaithful.v
 cicd_rules/banned_language_file:formal/F5_RenderFaithful.v
+cicd_rules/vlang_detected:formal/RealWasm.v
+cicd_rules/banned_language_file:formal/RealWasm.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 — **15 files, 26 `Print
+  **exists** (Coq/Rocq 8.18), axiom-free throughout — **16 files, 27 `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).
@@ -221,8 +221,13 @@ The work in flight changes which obligations are *load-bearing* and which are
   (was `prose`): a Wave-0 mechanized seed — `formal/K1_CodegenPreservation.v`
   (Coq, no axioms) — proves preservation for a minimal nat/bool · add/and
   fragment compiled to a stack machine — `K1Let_CodegenPreservation.v` grows it
-  with de Bruijn variables, `let`, and an environment; the real AffineScript AST
-  + real typed-WASM operational semantics remain the open obligation.
+  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⟧`.
 * **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
@@ -389,13 +394,16 @@ F-1 (full transformer preservation) is non-trivial rather than a formality.
 | Wave 1
 
 | 3
-| **The real lift (open — the bulk of the remaining work).** Replace the toy
-  objects with the real ones: formalise the **real AffineScript AST** and 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). Then
+| **The real lift (the bulk of the remaining work) — scoped + started.** Replace
+  the toy objects with the real ones: formalise the **real AffineScript AST** and
+  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), P-7 (resolution), P-8 (parser), P-10 (coherence); faces F-6/F-7;
-  full-language borrowing (P-3) pending #553.
+  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

@@ -94,6 +94,11 @@ cannot mistake it. Coq has no `v.mod` manifest, so `vmod_detected` never fires.
 | **F-5** — `render_ty` per-face type renaming is injective (no two canonical
   types collapse onto one displayed string), incl. the Js/Cafe "null"/"?" overlap
 | **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)
+| **mechanized**, axiom-free
 |===
 
 All mechanized theorems report *Closed under the global context* under `Print
@@ -215,12 +220,26 @@ 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`.
+
 == Scope (honest)
 
-These are Wave-0 seeds, not the discharged obligations. The fragments are
+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. Tracked in `docs/PROOF-NEEDS.adoc` and #513.
+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.
 
 == Checking
 

formal/REAL-LIFT.adoc

@@ -0,0 +1,277 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
+= The Real Lift — from toy seeds to the real AffineScript AST + typed-WASM
+Jonathan D.A. Jewell
+:toc: left
+:toclevels: 3
+:sectnums:
+:sectnumlevels: 2
+
+This is the engineering plan for the single largest remaining body of proof work
+in `docs/PROOF-NEEDS.adoc` §6 Wave 3: replacing the deliberately-small models the
+`formal/` track proves today with the *real* objects, so that K-1 / F-1 / F-2 and
+the dynamic halves of P-2 / P-4 become discharged obligations rather than
+meaning-pinning seeds.
+
+It is grounded in the actual compiler: the source AST is `lib/ast.ml`, the target
+IR is `lib/wasm.ml`, the compiler is `lib/codegen.ml` (+ `lib/codegen_gc.ml`),
+and the reference dynamic semantics is `lib/interp.ml`.
+
+[IMPORTANT]
+====
+The lift is **XL** (CompCert-scale for a substantial language). It is delivered
+as a *ladder* of strict-superset fragments, each fully mechanized and axiom-free
+before the next — the way `K1 → K1Let` already grew, and the way solo-core's
+`Solo → Duet → Ensemble` is meant to expand. No milestone lands with an
+`Admitted`.
+====
+
+== 1. The theorem
+
+For the real compiler `compile : Ast.program → Wasm.wasm_module` and the real
+operational semantics on each side:
+
+[source]
+----
+⟦ compile(p) ⟧_wasm  =  ⟦ p ⟧_source          (for every well-typed p)
+----
+
+K-1 is the backend half; F-1 (`⟦T_F(p)⟧ = ⟦T_canonical(canon(p))⟧`) composes the
+face transformers on top of it; F-2 (#601) is the observational corollary across
+faces. All three collapse to "grow K-1 onto the real objects, then re-chain the
+existing F-1/F-2 scaffolding."
+
+== 2. The two real objects (what we are formalising)
+
+=== 2.1 Source — `lib/ast.ml`
+
+The real `expr` has ~30 constructors. Grouped by the order the ladder tackles
+them:
+
+[cols="1,3"]
+|===
+| Group | Constructors
+
+| Core values/binding
+| `ExprLit` (Int/Float/Bool/Char/String/Unit), `ExprVar`, `ExprLet`
+  (carries `el_quantity : quantity option` — the QTT multiplicity), `ExprBlock`,
+  `stmt` (`StmtLet`/`StmtExpr`/`StmtAssign`/`StmtWhile`/`StmtFor`)
+
+| Control
+| `ExprIf`, `ExprMatch` (+ `match_arm`, guards), `ExprReturn`, `ExprBreak`,
+  `ExprContinue`
+
+| Functions
+| `ExprLambda` (+ `param` with `p_quantity`/`p_ownership`), `ExprApp`,
+  top-level `fn_decl` (`FnBlock`/`FnExpr`/`FnExtern`)
+
+| Aggregates (heap)
+| `ExprTuple`/`ExprTupleIndex`, `ExprArray`/`ExprIndex`, `ExprRecord`/`ExprField`/`ExprRowRestrict`
+
+| Operators
+| `ExprBinary` (`binary_op`), `ExprUnary` (`unary_op`, incl. `OpRef`/`OpMutRef`/`OpDeref`)
+
+| Elaboration nodes (post-typecheck, backend-only — `Typecheck.elaborate_string_concat`)
+| `ExprStringConcat`/`ExprStringEq`/`ExprStringRel` (the "string wall"),
+  `ExprFloatBinary`/`ExprFloatArray`/`ExprFloatIndex` (the "float wall"),
+  `ExprCellTuple`/`ExprCellTupleIndex`/`ExprCellRecord`/`ExprCellField`
+  (uniform-8 float-bearing layout)
+
+| Effects
+| `ExprHandle` (+ `handler_arm`), `ExprResume`, `ExprTry`, effect rows on
+  `TyArrow`
+
+| Unsafe
+| `ExprUnsafe` (`UnsafeRead`/`Write`/`Offset`/`Transmute`/`Forget`)
+|===
+
+The type layer (`type_expr`) carries the substructural data the proofs care
+about: `quantity` `{QZero,QOne,QOmega}` (→ already mechanized in `QttSemiring.v`),
+`ownership` `{Own,Ref,Mut}`, `origin_var` (ADR-022 Polonius regions, → P-3 /
+`P3_BorrowGraph.v`), effect rows (→ P-6, blocked on #555), and record rows.
+
+=== 2.2 Target — `lib/wasm.ml`
+
+A faithful WebAssembly-1.0 IR: `value_type {I32,I64,F32,F64}`, ~150 `instr`
+constructors (numeric i32/i64/f32/f64, `LocalGet/Set/Tee`, `GlobalGet/Set`, the
+load/store family with align+offset, `Block/Loop/If/Br/BrIf/Return/Call/CallIndirect`,
+`MemorySize/Grow`), and a `wasm_module` with `funcs`/`mems`/`tables`/`globals`/
+`exports`/`imports`/`elems`/`datas`/`custom_sections`. The
+`typedwasm.ownership` custom section carries `TyOwn/TyRef/TyMut` to the binary
+for typed-wasm Level-7/10 verification — the seam where P-3 (borrow soundness)
+connects to the target.
+
+=== 2.3 The gap from the toy K-1
+
+`K1_CodegenPreservation.v` invents an ad-hoc stack machine; `RealWasm.v`
+(this directory, milestone **R0**, below) re-targets the *actual* `instr` /
+`value_type` names with a stack-arity soundness theorem (`wexec_sound`:
+arity-checked code never gets stuck). That is the first real foundation stone.
+
+== 3. Coq module structure
+
+[cols="1,3,1"]
+|===
+| Module | Contents | Status
+
+| `RealWasm.v`
+| Target IR (real `instr`/`value_type` names) + stack-machine `wexec` +
+  arity checker `wcheck` + soundness `wexec_sound`.
+| **R0 landed**
+
+| `RealWasmSem.v`
+| The full target operational semantics as the ladder reaches control/memory:
+  fuel-indexed step relation, linear-memory model, frame/locals.
+| planned (R2+)
+
+| `RealAst.v`
+| The real source `expr`/`stmt`/`program` inductives (faithful to `lib/ast.ml`),
+  per-fragment.
+| planned (S0)
+
+| `RealAstSem.v`
+| The reference dynamic semantics (mirrors `lib/interp.ml`), per-fragment.
+| planned (S0)
+
+| `RealCompile.v`
+| The real `compile` (port of `lib/codegen.ml`), per-fragment.
+| planned (K-1/R1)
+
+| `RealPreservation.v`
+| `⟦compile p⟧ = ⟦p⟧` — the real K-1, per-fragment; then re-chains
+  `F1_TransformerPreservation.v` and the `SameCube` F-2 story.
+| planned
+|===
+
+== 4. The fragment ladder
+
+Each rung is a strict superset; each is fully proven (axiom-free) before the
+next. The rung names are stable references the `PROOF-NEEDS.adoc` rows will cite.
+
+[cols="1,3,2"]
+|===
+| Rung | Adds | Retires / advances
+
+| **R0** ✅
+| Pure i32 numeric stack core (`I32Const`, add/sub/mul/and/or/xor, `eqz`, drop);
+  `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.
+
+| **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.
+
+| **R-mem**
+| Linear memory: load/store family, `MemorySize/Grow`, a byte-addressed memory
+  model; `ExprTuple`/`ExprArray`/`ExprRecord` + indexing/field access.
+| Heap layout — the precondition for strings and the "cell" elaboration nodes.
+
+| **R-float**
+| `F64` (then `F32`) lane; the float-wall elaboration nodes
+  (`ExprFloatBinary`/`FloatArray`/`FloatIndex`, `ExprCellTuple`/`CellRecord`/`CellField`,
+  uniform-8 layout). Float model: an abstract IEEE carrier with deterministic ops
+  first (defer Flocq/NaN-bit fidelity to R-float-exact).
+| The "float wall" / "float heap wall" become preservation lemmas.
+
+| **R-str**
+| The string wall: `ExprStringConcat`/`StringEq`/`StringRel` over the
+  `[len][utf8]` byte layout (lengths-prefixed compare/concat).
+| String-wall slices 8b/9/10 (#458) as preservation lemmas.
+
+| **R-call**
+| `Call`/`CallIndirect` + `tables`/`elems`; multi-function `program`; `ExprApp`
+  to top-level `fn_decl`; closures (the indirect-dispatch path).
+| Whole-program K-1.
+
+| **R-wrap**
+| Replace `Z` i32 with mod-2^32 semantics (normalise at each op); i64 mod-2^64.
+| Bit-exact integer fidelity.
+
+| **R-eff**
+| Effects/handlers (`ExprHandle`/`Resume`/`Try`, effect rows) via CPS lowering.
+  **Gated on #555 / K-2**: prove against the interpreter's *intended* handler
+  semantics, then show the lowered targets refine it (the part that currently
+  fails on three backends).
+| **P-6** effect-row soundness; the #555 proof-blocking defect.
+|===
+
+The source-side rungs S0…Sn track the target rungs one-for-one (each `RealAst`/
+`RealAstSem` increment matches the `RealWasm`/`RealCompile` increment it is
+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.)
+* **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) —
+  enough for the deterministic layout the elaboration nodes assume.
+* **Floats.** Start with an *abstract* IEEE carrier: opaque `f64` with the
+  arithmetic/compare ops as deterministic uninterpreted functions, so R-float
+  proves *layout/dispatch* preservation without a NaN-bit model. A later
+  R-float-exact swaps in Flocq if bit-fidelity is ever load-bearing.
+* **The elaboration nodes.** `ExprStringConcat`/`Float*`/`Cell*` are introduced
+  by `Typecheck.elaborate_string_concat` *after* typing. The proof must include
+  that elaboration as part of `compile` (source semantics is on the
+  pre-elaboration AST; the elaboration must be shown meaning-preserving — itself
+  a clean lemma per node).
+* **Borrowing / QTT at the seam.** `origin_var` + the `typedwasm.ownership`
+  custom section connect to typed-wasm Level-7/10. P-3 (`P3_BorrowGraph.v`) and
+  P-4 (`QttTyping.v`/`QttDynamic.v`) are the *static+dynamic* discipline; the
+  lift shows `compile` preserves the multiplicity/ownership facts into the custom
+  section (a refinement, not a re-proof).
+* **Effects.** The genuinely hardest, and *blocked*: do it last (R-eff), only
+  after #555 is resolved per K-2.
+
+== 6. Reuse: typed-WASM, don't reinvent
+
+`hyperpolymath/typed-wasm` and `ephapax` both have Coq (`Semantics.v`). The
+target operational semantics (`RealWasmSem.v`) and `value_type`/`instr` encoding
+should be *imported or aligned* with typed-wasm's, not independently reinvented —
+the compile target is the one genuinely shared surface across the estate
+(per `.claude/CLAUDE.md`'s disambiguation table). The `typedwasm.ownership`
+custom section is the contracted hand-off point; the `crates/typed-wasm-verify/`
+verifier crate is the executable companion to the Coq semantics.
+
+== 7. Sequencing & effort
+
+[cols="1,3,1"]
+|===
+| Phase | Rungs | Size
+
+| First-order K-1 | R0 ✅ → R1 → R2 | M (multi-week)
+| Heap & data | R-mem → R-float → R-str | M–L
+| Whole program | R-call → R-wrap | M
+| The long tail | R-eff (after #555), generics/traits, `unsafe` | L–XL
+|===
+
+"First-order K-1" (R0→R2) is the natural first *publishable* milestone: it
+discharges K-1 for the nat/bool/let/if/control fragment on the **real** AST and
+**real** wasm IR, retires `K1`/`K1Let`, and settles #601 concretely. The estate
+already has the front-end scaffolding (`F1_TransformerPreservation.v`,
+`SameCube.agda`) waiting to re-chain onto it.
+
+== 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`.
+
+Tracked against `docs/PROOF-NEEDS.adoc` §6 Wave 3 and #513.