feat(formal): F-5 render non-collision + real-lift R0 (RealWasm + plan)

.hypatia-ignore

@@ -71,3 +71,7 @@ cicd_rules/vlang_detected:formal/QttTyping.v
 cicd_rules/banned_language_file:formal/QttTyping.v
 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 — **14 files, 23 `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).
@@ -79,7 +79,8 @@ than the prose corpus suggests:
   in `P2_Progress.v` (first-order) + `P2_Stlc.v` (STLC with functions + the
   substitution lemma, funext-free) / `P3_BorrowSound.v` (single-bit) +
   `P3_BorrowGraph.v` (multi-resource loan graph) / `F3_PragmaDecidable.v` /
-  `F4_ErrorFaithful.v`. Affine/QTT layer: `QttSemiring.v` (`{0,1,ω}`) +
+  `F4_ErrorFaithful.v` / `F5_RenderFaithful.v` (render non-collision).
+  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>>.
@@ -220,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
@@ -302,8 +308,13 @@ cover them.
   renaming of canonical type names, and never collapses two distinct canonical
   types to one face string inside a single message (e.g. Js maps both `Unit` and
   `Option[T]` into "null"-shaped text — show this is unambiguous in context).
-| S | `absent`
-| new; `lib/face.ml` `render_ty`
+| S | `partial`
+| **mechanized** for the vocabulary model: `formal/F5_RenderFaithful.v` proves
+  every face's renaming is injective (`render_inj` — no two canonical types
+  collapse onto one string), incl. the Js/Cafe "null"/"?" overlap
+  (`js_no_collapse`, `cafe_no_collapse`, `option_never_atom`). Faithful to the
+  whole-string Unit/Bool match + canonical-inner Option rewrite; models the
+  name vocabulary, not raw OCaml strings. `lib/face.ml` `render_ty`
 
 | F-6
 | **Preview round-trip totality.** The `preview-{python,js,pseudocode,lucid,cafe}`
@@ -367,8 +378,9 @@ F-1 (full transformer preservation) is non-trivial rather than a formality.
 | **Done.** Grew the models toward the real language: **P-2 → STLC with functions
   + the substitution lemma** (`P2_Stlc.v`, funext-free); **P-3 → a multi-resource
   borrow graph** (`P3_BorrowGraph.v`: loan edges, liveness, move-locality,
-  multi-resource #554 rejected). *Leftover:* F-5 (small, self-contained
-  `render_ty` injectivity) and the K-4 `CAPABILITY-MATRIX` cross-link.
+  multi-resource #554 rejected); **F-5 → `render_ty` non-collision**
+  (`F5_RenderFaithful.v`: every face's renaming injective). *Leftover:* the K-4
+  `CAPABILITY-MATRIX` cross-link.
 | Wave 0
 
 | 2
@@ -382,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/F5_RenderFaithful.v

@@ -0,0 +1,135 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+
+(*
+   F5_RenderFaithful.v
+   ═══════════════════
+   F-5 (docs/PROOF-NEEDS.adoc): `render_ty` faithfulness / non-collision.
+
+   lib/face.ml's `render_ty` rewrites a small fixed vocabulary of canonical type
+   names per face — Unit, Bool, and Option[_] — leaving everything else
+   untouched. F-5 asks: is that renaming injective (it never collapses two
+   distinct canonical types onto one displayed string), even where face lexemes
+   overlap — Js renders Unit as "null" and Option[T] as "T | null", so both
+   mention "null"?
+
+   This models the canonical-type vocabulary render_ty branches on (`cty`), the
+   displayed-name lexemes (`name` — distinct constructors model distinct on-screen
+   tokens), and the rendered form (`rty`), then mirrors render_ty as
+   `render : face → cty → rty`. Two fidelity points carried over from the OCaml:
+
+   * Unit/Bool are special-cased only at the WHOLE-type level (`if s = "Unit"`),
+     never on a nested occurrence.
+   * Option's inner is rendered *canonically* — the OCaml `global_replace`
+     captures the canonical substring `\1` — so Js `Option[Option[Int]]` ⇒
+     "Option[Int] | null" (inner Option intact), exactly the greedy-regex result.
+
+   Theorems: `canon_inj`; `render_inj` (every face's renaming is injective — the
+   non-collapse guarantee); and the pointed `js_no_collapse` / `cafe_no_collapse`
+   / `option_never_atom` (Unit and Option[_] never read as the same type despite
+   the shared "null"/"?" lexeme). Axiom-free, no Admitted.
+
+   Scope (honest): models the displayed-name vocabulary, not raw OCaml strings;
+   assumes well-formed type strings (no adversarial text around `Option[...]`).
+
+   `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
+*)
+
+Require Import PeanoNat.
+
+(* The six faces (lib/face.ml `face`). *)
+Inductive face := Canonical | Python | Js | Pseudocode | Lucid | Cafe.
+
+(* Displayed atom lexemes. Distinct constructors ⇒ distinct on-screen names —
+   faithful, because the real renamings (None/null/nothing/bool/boolean/Boolean)
+   are genuinely distinct tokens and no canonical base name equals any of them. *)
+Inductive name :=
+| NUnit | NBool
+| NNone | NNothing | NNull
+| Nbool | NBoolean | NbooleanJs
+| NBase (n : nat).
+
+(* Rendered type forms. *)
+Inductive rty :=
+| RNm (x : name)
+| ROptBr (r : rty)    (* Option[ r ] *)
+| ROrNull (r : rty)   (* r | null    *)
+| RMaybe (r : rty)    (* Maybe r     *)
+| RQ (r : rty).       (* r ?         *)
+
+(* Canonical types: the vocabulary render_ty distinguishes. *)
+Inductive cty :=
+| CUnit | CBool | CBase (n : nat) | COption (a : cty).
+
+(* Canonical rendering — Option's inner stays canonical (matches the regex \1). *)
+Fixpoint canon (t : cty) : rty :=
+  match t with
+  | CUnit     => RNm NUnit
+  | CBool     => RNm NBool
+  | CBase n   => RNm (NBase n)
+  | COption a => ROptBr (canon a)
+  end.
+
+(* Per-face rendering, mirroring lib/face.ml render_ty: top-level special-case
+   for Unit/Bool; per-face Option wrapper with a canonical inner. *)
+Definition render (f : face) (t : cty) : rty :=
+  match t with
+  | CUnit =>
+    match f with
+    | Canonical | Lucid => RNm NUnit
+    | Python            => RNm NNone
+    | Js | Cafe         => RNm NNull
+    | Pseudocode        => RNm NNothing
+    end
+  | CBool =>
+    match f with
+    | Canonical                 => RNm NBool
+    | Python                    => RNm Nbool
+    | Js                        => RNm NbooleanJs
+    | Pseudocode | Lucid | Cafe => RNm NBoolean
+    end
+  | CBase n => RNm (NBase n)
+  | COption a =>
+    match f with
+    | Canonical | Python | Pseudocode => ROptBr (canon a)
+    | Js                              => ROrNull (canon a)
+    | Lucid                           => RMaybe  (canon a)
+    | Cafe                            => RQ      (canon a)
+    end
+  end.
+
+(* ── canonical rendering is injective ──────────────────────────────────── *)
+Lemma canon_inj : forall t1 t2, canon t1 = canon t2 -> t1 = t2.
+Proof.
+  induction t1; destruct t2; simpl; intro H;
+    try discriminate; try reflexivity.
+  - inversion H; reflexivity.                       (* CBase = CBase *)
+  - inversion H; f_equal; apply IHt1; assumption.   (* COption = COption *)
+Qed.
+
+(* ── every face's renaming is injective: the non-collapse guarantee ─────── *)
+Theorem render_inj : forall f t1 t2, render f t1 = render f t2 -> t1 = t2.
+Proof.
+  intros f t1 t2 H; destruct f, t1, t2; cbn in H;
+    solve [ discriminate
+          | reflexivity
+          | inversion H; subst; reflexivity
+          | inversion H; f_equal; apply canon_inj; assumption ].
+Qed.
+
+(* ── the pointed overlaps don't collapse ───────────────────────────────────
+   Js renders Unit as "null" and Option[T] as "T | null"; Cafe as "null"/"T?".
+   The shared lexeme never makes Unit and an Option read as the same type. *)
+Corollary js_no_collapse   : forall a, render Js   CUnit <> render Js   (COption a).
+Proof. intros a H; discriminate. Qed.
+
+Corollary cafe_no_collapse : forall a, render Cafe CUnit <> render Cafe (COption a).
+Proof. intros a H; discriminate. Qed.
+
+(* No Option ever collides with a base/Unit/Bool atom (different rendered shape). *)
+Corollary option_never_atom : forall f a x, render f (COption a) <> RNm x.
+Proof. intros f a x H; destruct f; cbn in H; discriminate. Qed.
+
+Print Assumptions render_inj.
+Print Assumptions js_no_collapse.
+Print Assumptions option_never_atom.

formal/README.adoc

@@ -89,6 +89,16 @@ cannot mistake it. Coq has no `v.mod` manifest, so `vmod_detected` never fires.
 | **P-4** (Wave 3) — the *dynamic* half: β-reduction preserves the usage profile;
   QTT scaling law; ties back to `usage_soundness`
 | **mechanized**, axiom-free
+
+| `F5_RenderFaithful.v`
+| **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
@@ -100,7 +110,7 @@ the obligation shapes as `Definition ... : Prop` over section `Variable`s
 each ending in a `*_discharged : Siblings_Stated.<name> … := <proof>` line that
 type-checks the concrete proof against the stated obligation.
 
-== Mechanized siblings (P-2, P-3, F-3, F-4)
+== Mechanized siblings (P-2, P-3, F-3, F-4, F-5)
 
 Each is proven for a deliberately small concrete model — enough to discharge
 the stated obligation and pin its meaning, not the full language:
@@ -133,6 +143,14 @@ the stated obligation and pin its meaning, not the full language:
 * **F-4** (`F4_ErrorFaithful.v`) — the face renderer preserves an error's
   *class* and *referent*, changing only vocabulary, so no face can make error
   X read as a different error Y.
+* **F-5** (`F5_RenderFaithful.v`) — `render_ty`'s per-face type-name renaming is
+  *injective*: distinct canonical types never collapse onto one displayed string.
+  Models the vocabulary it special-cases (`Unit`, `Bool`, `Option[_]`), faithful
+  to the whole-string Unit/Bool match and the canonical-inner Option rewrite
+  (Js `Option[Option[Int]]` ⇒ "Option[Int] | null"). Proves the pointed case the
+  obligation names — Js/Cafe render Unit as "null"/"?" *and* `Option[T]` with the
+  same lexeme, yet the two never read as one type (`js_no_collapse`,
+  `cafe_no_collapse`, `option_never_atom`).
 
 == Wave 2: the affine/QTT layer (P-4)
 
@@ -202,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