feat: ground same-cube at the typed-wasm level (real finding: 2 classes)

Built affinescript and actually ran the verifier (it previously only ever
SKIPped). Upgraded verify-same-cube.sh from normalised-text comparison to
compiling each face to typed-wasm and sha256-comparing the modules — the wasm
IS the cube, so this is the rigorous bar and avoids text-only false-positives.

Grounded result for the 'greet' corpus (affinescript @ main, 457-test suite
green, per-face snapshot net 6/6 green): the six faces compile to TWO wasm
classes — {canonical, jaffa, cafe} vs {rattle, pseudo, lucid}. The split is a
real lowering-style divergence (trailing call as statement vs tail-expression);
observationally identical (same output, same unit return) but not
byte-identical wasm. So 'different faces, same cube' holds observationally but
not byte-level for this corpus. Docs (profile + corpus README) record the
honest finding; the verifier reports wasm equivalence classes with preview
diffs as diagnostics.

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

Author: claude

examples/same-cube/README.md

@@ -6,7 +6,7 @@ Each subdirectory here is **one program written in every AffineScript face**.
 The files are deliberately the *same* program (identical strings, identical
 structure) — not the demonstrative, different-string examples in
 `affinescript/examples/faces/`. That is the whole point: if they are the same
-program, every face must lower to the **same canonical cube**.
+program, every face should lower to the **same cube**.
 
 ```
 greet/
@@ -25,23 +25,46 @@ scripts/verify-same-cube.sh examples/same-cube/greet \
   --out .machine_readable/audits/same-cube.jsonl
 ```
 
-The verifier detects each file's face from its `face:` pragma, runs the
-matching `preview-*` transformer, normalises the result (modulo comments and
-whitespace), and compares it to `canonical.affine`. Output is a per-face
-table plus invariant-path claim records (`Grounded` / `Ungrounded`).
+The verifier detects each file's face from its `face:` pragma, **compiles it to
+typed-wasm** (`compile --face <face>`), and sha256-compares the modules — the
+wasm *is* the cube, so byte-identical wasm is the rigorous bar. For any face
+outside the canonical class it also prints the `preview-*` text diff as a
+diagnostic of *where* the lowering diverges. Output is a per-face table, the
+wasm equivalence classes, and invariant-path claim records (`Grounded` /
+`Ungrounded`). Needs an `affinescript` binary (PATH, `--affinescript`,
+`AFFINESCRIPT`, or `../affinescript/_build`); without one it SKIPs.
 
-This is a **claim-path debugger**, not a rubber stamp: a `DIFF` line does not
-mean the tool failed — it means the tool located the face that diverges from
-the cube, and prints exactly where. Grounding requires an `affinescript`
-binary (PATH, `--affinescript`, `AFFINESCRIPT`, or `../affinescript/_build`);
-without one the verifier SKIPs, because the invariant is grounded in CI where
-the compiler is built.
+This is a **claim-path debugger**, not a rubber stamp: a `DIFF` is the tool
+locating which face leaves the cube and showing exactly where.
+
+## Grounded result — `greet` (2026-06-18, affinescript @ main)
+
+Run against a freshly-built compiler, the six faces compile to **two** distinct
+wasm modules:
+
+| wasm class | faces |
+|---|---|
+| `56c454be…` | canonical, **jaffa**, **cafe** |
+| `2ff63dd1…` | **rattle**, **pseudo**, **lucid** |
+
+The split is **not** a transformer crash — all six compile, type-check, and
+print the same string. It is a real, characterised divergence in *lowering
+style*: rattle/pseudo/lucid render the trailing call as a **tail expression**
+(`fn main() … { println(x) }`), while canonical/jaffa/cafe keep it as a
+**statement** (`{ println(x); }`). For `println : … -> ()` both return unit, so
+the programs are **observationally identical** — but the emitted wasm is not
+byte-identical.
+
+So *"different faces, same cube"* is true **observationally** but **false at the
+byte-wasm level** for this corpus: the face transformers do not currently agree
+on trailing-statement lowering. Tracked as an affinescript transformer-
+consistency item. (lucid additionally emits a `module Greet;` decl and drops
+the `-{IO}->` annotation in its preview text; neither changes the wasm class.)
 
 ## Adding a program
 
-Add a new sibling directory (e.g. `counter/`) with one file per face you want
-to cover, each carrying the right `face:` pragma and encoding the identical
-program. Keep to surface features the transformers handle today (see the
-"Known transformer gaps" table in `affinescript/examples/faces/README.adoc`);
-a face that uses an unsupported construct will show up as a `DIFF`, which is
-useful signal, not noise.
+Add a sibling directory (e.g. `counter/`) with one file per face, each carrying
+the right `face:` pragma and encoding the identical program. Keep to surface
+features the transformers handle today (see the "Known transformer gaps" table
+in `affinescript/examples/faces/README.adoc`); divergences show up as extra
+wasm classes — useful signal, not noise.

profiles/faces.md

@@ -38,8 +38,8 @@ same-cube invariant, locating *which* face breaks the cube and *where*.
 face source (greet/rattle.affine, …)         ← evidence / specification
         │  preview-<face>                     ← transition (transformer T)
         ▼
-canonical text (normalised)                   ← intermediate target
-        │  byte-equality vs canonical.affine  ← grounding check
+typed-wasm module (compile --face)            ← the cube itself
+        │  sha256-equality vs canonical wasm  ← grounding check
         ▼
 "same cube" holds for this program            ← conclusion (Grounded | Ungrounded)
 ```
@@ -63,21 +63,28 @@ workspace at its corpus (the `tools/invariant-path/` hook), e.g.:
 just invariant-path same-cube examples/
 ```
 
-## What v1 catches
-
-- A face whose `preview-*` lowering no longer normalises to the canonical
-  cube (the cross-face equality break the per-face snapshots miss).
-- A face example that fails to parse after lowering (round-trip break).
-- A corpus where one face silently encodes a *different* program (e.g. a
-  changed string literal or dropped statement).
-
-## What v1 does NOT catch (yet)
-
-- *Semantic* divergence below the canonical-text level — two different
-  canonical texts that nevertheless typecheck to the same cube. v1
-  compares normalised canonical text, not ASTs. (AST-level equality is
-  the planned v2 grounding, once the compiler exposes a stable AST dump.)
-- typed-wasm equality. The chain "same canonical ⇒ same wasm" is asserted
-  by the compiler, not re-checked here.
+## What it catches
+
+- A face whose lowering compiles to a **different typed-wasm module** than the
+  canonical reference (the cross-face equality break the per-face snapshots
+  miss). Comparing wasm — the cube itself — also avoids text-only
+  false-positives (e.g. tail-expression vs statement lowering, observationally
+  identical but textually different).
+- A face example that fails to parse or compile (round-trip / build break).
+- A corpus where one face silently encodes a *different* program.
+
+When faces split into more than one wasm class, the `preview-*` text diff is
+printed per divergence so you can see *where* the lowering parts ways.
+
+## Limits
+
+- **Byte-identical** wasm is stricter than **observational** equivalence: two
+  faces can print the same thing and return the same value yet emit different
+  wasm. The grounded `greet` result is exactly this — rattle/pseudo/lucid vs
+  canonical/jaffa/cafe split into two classes over a trailing-statement
+  lowering choice. The tool reports the wasm *classes* and leaves "are these
+  classes observationally equal?" to the reader; it does not execute the
+  modules to compare runtime output.
+- It grounds the corpora it is given; it does not enumerate all programs.
 - Effect-handler lowering soundness (tracked in affinescript #555); a
   face that exercises `handle` may converge in text yet diverge at runtime.