feat: faces same-cube verifier (invariant-path 'faces' profile)

DESIGN.md

@@ -47,3 +47,9 @@
 - Decision: make `scripts/install-desktop.sh` remove a destination `.desktop` file if it exists but is not writable, then reinstall with deterministic modes (`444` in app menu, `555` on Desktop/Shortcuts).
 - Tradeoff: replacement is explicit rather than in-place update, but content and permissions remain deterministic from template + destination policy.
 - Reasoning: GNU `install` can fail on existing read-only targets; KDE/Plasma desktop launchers also need execute bits to avoid launch aborts.
+
+## 2026-06-18 — Faces same-cube profile (`faces`)
+
+- Decision: add a `faces` profile (`profiles/faces.md`), a same-cube corpus (`examples/same-cube/`), and a verifier (`scripts/verify-same-cube.sh`) that grounds the AffineScript "different faces, same cube" invariant — every face's `preview-*` lowering must normalise to the same canonical text.
+- Tradeoff: v1 compares normalised canonical *text*, not ASTs, and SKIPs when no `affinescript` binary is reachable (grounding happens in CI). It can't yet catch two different canonical texts that typecheck to the same cube.
+- Reasoning: per-face snapshot tests (`affinescript/tests/faces/`) catch drift *within* a face but never compare face A's cube against face B's. The cross-face equality is the load-bearing claim; this profile is the claim-path debugger that locates which face breaks it. Doc-profile shape (markdown + script), so no change to the Rust core or CLI — consistent with the `pmpl` / `standards-docs` profiles.

Justfile

@@ -15,6 +15,10 @@ build:
 run-cli:
     cargo run --release --bin invariant-path-cli
 
+# Ground the AffineScript "different faces, same cube" invariant (faces profile)
+same-cube corpus="examples/same-cube/greet":
+    ./scripts/verify-same-cube.sh {{corpus}} --out .machine_readable/audits/same-cube.jsonl
+
 # Run the TUI
 run-tui:
     ./invariant-path-launcher --auto

README.adoc

@@ -21,8 +21,9 @@ It is a claim-path debugger, not a truth engine.
 * `schemas/annotation.schema.json` — JSON schema for persisted annotations
 * `docs/ARCHITECTURE.md` — minimal architecture proposal
 * `docs/EXTENDING.md` — extension guide for invariant types and heuristics
-* `examples/` — seeded and realistic examples
-* `profiles/` — profile notes for `echidna`, `panll`, and `hypatia`
+* `examples/` — seeded and realistic examples (incl. `examples/same-cube/` — the AffineScript faces corpus)
+* `profiles/` — profile notes for `echidna`, `panll`, `hypatia`, `pmpl`, and `faces` (AffineScript "different faces, same cube")
+* `scripts/verify-same-cube.sh` — grounds the faces same-cube invariant (see `profiles/faces.md`)
 
 == Quick Start
 

examples/same-cube/README.md

@@ -0,0 +1,47 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+
+# Same-cube corpus
+
+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**.
+
+```
+greet/
+  canonical.affine   face: canonical      (the reference cube)
+  rattle.affine      face: rattlescript   -> preview-python
+  jaffa.affine       face: jaffascript    -> preview-js
+  pseudo.affine      face: pseudoscript   -> preview-pseudocode
+  lucid.affine       face: lucidscript    -> preview-lucid
+  cafe.affine        face: cafescripto    -> preview-cafe
+```
+
+## Ground the invariant
+
+```sh
+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`).
+
+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.
+
+## 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.

examples/same-cube/greet/cafe.affine

@@ -0,0 +1,14 @@
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+#
+# Same-cube corpus "greet" — CafeScripto (CoffeeScript) face.
+# Lowers via `preview-cafe` to the canonical cube in ./canonical.affine.
+# face: cafescripto
+
+effect IO {
+  fn println(s: String) -> ();
+}
+
+fn main() -{IO}-> () {
+  println("Hello, faces!");
+}

examples/same-cube/greet/canonical.affine

@@ -0,0 +1,16 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+//
+// Same-cube corpus "greet" — the reference (canonical) face.
+// Every sibling file in this directory is the SAME program written in a
+// different face. Each face's `preview-*` lowering must normalise to the
+// canonical text below ("different faces, same cube").
+// face: canonical
+
+effect IO {
+  fn println(s: String) -> ();
+}
+
+fn main() -{IO}-> () {
+  println("Hello, faces!");
+}

examples/same-cube/greet/jaffa.affine

@@ -0,0 +1,14 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+//
+// Same-cube corpus "greet" — JaffaScript (JavaScript / TypeScript) face.
+// Lowers via `preview-js` to the canonical cube in ./canonical.affine.
+// face: jaffascript
+
+effect IO {
+  fn println(s: String) -> ();
+}
+
+function main() -{IO}-> () {
+  println("Hello, faces!");
+}

examples/same-cube/greet/lucid.affine

@@ -0,0 +1,15 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+--
+-- Same-cube corpus "greet" — LucidScript (PureScript / Haskell) face.
+-- Lowers via `preview-lucid` to the canonical cube in ./canonical.affine.
+-- face: lucidscript
+
+module Greet where
+
+effect IO {
+  fn println(s: String) -> ();
+}
+
+main :: -{IO}-> ()
+main () = println("Hello, faces!")

examples/same-cube/greet/pseudo.affine

@@ -0,0 +1,14 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+--
+-- Same-cube corpus "greet" — PseudoScript (pseudocode) face.
+-- Lowers via `preview-pseudocode` to the canonical cube in ./canonical.affine.
+-- face: pseudoscript
+
+effect IO {
+  fn println(s: String) -> ();
+}
+
+function main() -{IO}-> () do
+    output "Hello, faces!"
+end

examples/same-cube/greet/rattle.affine

@@ -0,0 +1,12 @@
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+#
+# Same-cube corpus "greet" — RattleScript (Python) face.
+# Lowers via `preview-python` to the canonical cube in ./canonical.affine.
+# face: rattlescript
+
+effect IO:
+    fn println(s: String) -> ();
+
+def main() -{IO}-> ():
+    println("Hello, faces!")

profiles/faces.md

@@ -0,0 +1,83 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+
+# Profile: faces
+
+**Target corpus:** the AffineScript face family —
+`affinescript/examples/faces/`, the `examples/same-cube/` corpus in this
+repo, and the face brand-surface repos (`rattlescript`, `jaffascript`,
+`pseudoscript`, `lucidscript`, `cafescripto`).
+**Mode:** invariant-grounding (behavioural equality, not doc-claims)
+**Purpose:** Keep the load-bearing AffineScript claim — *"different faces,
+same cube"* — grounded in the actual behaviour of the face transformers.
+
+## Why this profile exists
+
+AffineScript is one canonical language (the "cube"). Each *face* (ADR-010)
+is an alternative surface syntax — RattleScript (Python), JaffaScript
+(JS/TS), PseudoScript (pseudocode), LucidScript (PureScript/Haskell),
+CafeScripto (CoffeeScript) — lowered to canonical AffineScript by a pure
+text transformer (`lib/<name>_face.ml`) and previewed with `preview-*`.
+
+The whole architecture rests on one invariant:
+
+> For a given program, **every face lowers to the same canonical cube**
+> (modulo whitespace and comment placement), and therefore to the same
+> typed-wasm output.
+
+That is a *claim*. Like any claim, it can rot: a transformer edit can
+silently make one face diverge while the others still pass their own
+round-trip tests. Per-face snapshot tests (`affinescript/tests/faces/`)
+catch *drift within a face* but not *divergence between faces* — they
+never compare face A's cube against face B's. This profile grounds the
+cross-face equality directly: it is a claim-path debugger for the
+same-cube invariant, locating *which* face breaks the cube and *where*.
+
+## The claim path
+
+```
+face source (greet/rattle.affine, …)         ← evidence / specification
+        │  preview-<face>                     ← transition (transformer T)
+        ▼
+canonical text (normalised)                   ← intermediate target
+        │  byte-equality vs canonical.affine  ← grounding check
+        ▼
+"same cube" holds for this program            ← conclusion (Grounded | Ungrounded)
+```
+
+## Invocation
+
+```sh
+# Ground the bundled same-cube corpus (needs an `affinescript` binary on
+# PATH, or a dune build of it — see the script's resolver).
+scripts/verify-same-cube.sh examples/same-cube/greet \
+  --out .machine_readable/audits/same-cube.jsonl
+
+# Any directory of sibling face files for ONE program works:
+scripts/verify-same-cube.sh path/to/<program>-faces/
+```
+
+A face brand-surface repo grounds its own examples by pointing the shared
+workspace at its corpus (the `tools/invariant-path/` hook), e.g.:
+
+```sh
+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.
+- Effect-handler lowering soundness (tracked in affinescript #555); a
+  face that exercises `handle` may converge in text yet diverge at runtime.