// 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. (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.
  (R1's `eval` lives inline in `RealCompile.v`.)
| R1 inline

| `RealCompile.v`
| 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
  `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 `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** ✅ (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** ⏳ (kernel landed)
| Linear memory. **Done (`RealMem.v`):** `I32Load`/`I32Store` added to the real
  `instr` (zero blast radius); a **word-addressed** memory (`mem := list Z`, cell
  = i32) with a structural memory executor `mexec` (straight-line ⇒ no fuel) +
  `mexec_app`; a bump allocator (`base = current size`); and the heap round-trips
  — store→load (`mexec_store_then_load`) and a 2-cell **tuple build+project**
  (`mexec_pair_build_proj`: `field i at base+i`, both projections) — reusing
  `set_nth`'s get-after-set. **Remaining:** `MemorySize`/`Grow` as a runtime
  allocator instruction, byte-granular layout, control-bearing field
  expressions (combine `mexec` with the R2-loops `cexec`), and the full source
  `ExprTuple`/`ExprArray`/`ExprRecord` + indexing/field-access compile-correctness.
| 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

* **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) —
  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 + 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`. 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.
* **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.
* **R-mem kernel landed** — `RealWasm.v` grown with `I32Load`/`I32Store` (zero
  blast radius). `RealMem.v` gives a word-addressed memory (`mem := list Z`), a
  *structural* memory executor `mexec` (straight-line ⇒ no fuel) + `mexec_app`, a
  bump allocator, and the heap round-trips: store→load (`mexec_store_then_load`)
  and the 2-cell tuple build+project (`mexec_pair_build_proj`, `field i at
  base+i`), reusing `set_nth`'s get-after-set. Axiom-free; 20 files / 35 closure
  reports. **Remaining R-mem:** runtime `MemorySize`/`Grow`, byte layout,
  control-bearing fields (fuse `mexec` with `cexec`), full source
  tuple/array/record compile-correctness.
* Next: finish R-mem (above), then **R-float** / **R-str** / **R-call** per the
  ladder.

Tracked against `docs/PROOF-NEEDS.adoc` §6 Wave 3 and #513.
