Harden the soundness-ledger gate: content-binding, stamp-enforcement, xfail pin-liveness

.github/workflows/ci.yml

@@ -35,6 +35,11 @@ jobs:
     steps:
       - name: Checkout code
         uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        with:
+          # Full history so the soundness-ledger gate (property 4) can resolve
+          # :ground-truth-sha: and diff soundness paths against it. A shallow
+          # clone makes property 4 fail closed ("stamp not present").
+          fetch-depth: 0
       - name: Set up OCaml toolchain (self-hosted; replaces ocaml/setup-ocaml)
         run: |
           sudo apt-get update
@@ -97,6 +102,13 @@ jobs:
         # PROOF-NEEDS / NAVIGATION / CLAUDE.md) stops linking back to it.
         # See tools/check-soundness-ledger.sh.
         run: ./tools/check-soundness-ledger.sh
+      - name: Capability-matrix test-anchor gate
+        # docs/CAPABILITY-MATRIX.adoc anchors each feature-readiness claim to an
+        # executable test ("== Test anchors"). This gate fails if that section
+        # disappears or if any test it names goes missing — so a "works" status
+        # row cannot outlive the test that backs it.
+        # See tools/check-capability-anchors.sh.
+        run: ./tools/check-capability-anchors.sh
       - name: Check formatting
         run: opam exec -- dune build @fmt
   lint:

.ocamlformat-ignore

@@ -0,0 +1,7 @@
+# The standalone soundness xfail-pin harness was authored in an environment
+# without ocamlformat available, so its formatting could not be verified at
+# authoring time. Excluded from `dune build @fmt` until it is run through
+# ocamlformat 0.26.2 and this entry removed. It is a self-contained test
+# executable (see docs/SOUNDNESS.adoc, property 5); nothing depends on its
+# formatting.
+test/xfail/test_xfail_pins.ml

docs/CAPABILITY-MATRIX.adoc

@@ -225,6 +225,38 @@ db-theory triplet — `Sqlite.affine` (#522 / #524 / #525), `Transaction.affine`
 group-by + aggregation primitives) — are the current authoring frontier.
 A few primitives remain `extern` builtins.
 
+== Test anchors
+
+Every enforcement claim in the tables above is anchored to an executable test,
+mirroring the link:SOUNDNESS.adoc[soundness ledger]. This makes the claims
+*falsifiable*: `tools/check-capability-anchors.sh` (wired into `just check` +
+CI) extracts every `test/…` path named below and fails the build if any has
+gone missing — so a `works` / `enforced` row cannot keep its status after its
+test is deleted or renamed without this section (and CI) noticing.
+
+[cols="2,4",options="header"]
+|===
+|Component (row above) |Anchoring test(s)
+
+|Lexer |`test/test_lexer.ml`
+|Parser / AST / Name resolution |`test/test_e2e.ml`, `test/test_qualified_paths.ml`
+|Type checker |`test/test_e2e.ml`, `test/test_slash_effect_row.ml`
+|Effect system |`test/test_effects.ml`, `test/test_effect_sites.ml`; fixtures `test/e2e/fixtures/handle_return_arm.affine`, `test/e2e/fixtures/handle_resume_tail.affine`
+|Borrow checker |`test/test_borrow_polonius.ml`; fixtures `test/e2e/fixtures/borrow_callee_returned_borrow_uam.affine`, `test/e2e/fixtures/borrow_callee_value_return_ok.affine`
+|Quantity / affine (QTT) |`test/test_e2e.ml`; fixtures `test/e2e/fixtures/linear_arrow_violation.affine`, `test/e2e/fixtures/affine_violation.affine`, `test/e2e/fixtures/erased_violation.affine`
+|Interpreter |`test/test_e2e.ml`, `test/test_solo_cesk.ml`, `test/test_module_mut.ml`
+|Traits (incl. #559 coherence) |`test/test_e2e.ml` (Trait-Coherence suite)
+|Stdlib (AOT + laws) |`test/test_stdlib_aot.ml`, `test/test_stdlib_laws.ml`
+|typed-wasm isolation |`test/test_tw_isolation.ml`
+|Codegen (golden snapshots) |`test/test_golden.ml`
+|Deno / JS host backends |`test/test_deno_builtins_consistency.ml`, `test/test_int_div_js.ml`
+|Solo core (executable metatheory) |`test/test_solo_cesk.ml`
+|===
+
+NOTE: this anchors *feature-readiness* claims. *Soundness-hole* anchors live in
+their own ledger (link:SOUNDNESS.adoc[SOUNDNESS.adoc]), gated by
+`tools/check-soundness-ledger.sh`.
+
 == What AffineScript is NOT (anti-over-claim)
 
 * Not "production-ready". Alpha. CORE-01 (#177) closed 2026-05-30. The

justfile

@@ -99,6 +99,7 @@ guard:
     ./tools/check-no-extension-ts.sh
     ./tools/check-doc-truthing.sh
     ./tools/check-soundness-ledger.sh
+    ./tools/check-capability-anchors.sh
 
 # Re-baseline the doc-truthing over-claim ledger after a deliberate, legitimate
 # change (e.g. a new dated roadmap milestone). Commit the .allow diff.

test/e2e/fixtures/stub_backend_return_dropped.affine

@@ -0,0 +1,12 @@
+// Early (non-tail) `return`. The experimental Lean/Why3 backends drop it:
+// lean_codegen.ml `gen_block` skips `StmtReturn`, lowering this body to `:= ()`
+// (both returns vanish). Pinned by `test_stub_backend_return_xfail` (Refs #624).
+// The desired end-state is a loud failure on this shape; until then the pin
+// fails-as-expected. Do not "fix" this fixture to make a pin pass — read
+// docs/SOUNDNESS.adoc first.
+fn early(x: Int) -> Int {
+  return 1;
+  return 2;
+}
+
+fn main() -> Int = early(0);

test/test_e2e.ml

@@ -2382,22 +2382,35 @@ fn main() -> Int = 0;
       Alcotest.failf "#559: impls for Pair[Int,Bool] vs Pair[Bool,Int] do not \
                       overlap and must be accepted, got error: %s" msg
 
-(* KNOWN LIMITATION (#559): generic-subsumption overlap — a blanket/generic
-   impl `impl[T] Greet for Box[T]` overlapping a specific `impl Greet for
-   Box[Int]` — is NOT yet detected. The coherence check itself instantiates
-   impl type params and would catch it, but generic *impl* handling has its
-   own separate immaturities (e.g. `impl[T] ... for Box[T]` currently trips a
-   spurious "Trait not found" before coherence runs), so this case rides on a
-   prerequisite that is not yet solid. The soundness-critical hole #559 named
-   — silently accepting overlapping *concrete* impls — IS fixed and covered by
-   the rejected/accepted tests above. Generic-subsumption coherence is tracked
-   as follow-up, not pinned here as an executable accept (it would mis-document
-   a moving target). *)
+(* #559 generic-subsumption: a blanket impl `impl[T] Greet for Box[T]`
+   overlapping a specific `impl Greet for Box[Int]` IS detected and rejected.
+   The unification-based coherence check instantiates the generic head — Box[T]
+   unifies with Box[Int] — so the overlap is caught by the same machinery as the
+   concrete case. (Ground-truthed 2026-06-21 against the running compiler; an
+   earlier note here wrongly claimed this was undetected — corrected per the
+   docs/SOUNDNESS.adoc "compiler is ground truth" rule.) *)
+let test_coherence_generic_subsumption_rejected () =
+  let src = {|
+trait Greet { fn greet() -> Int; }
+enum Box[T] { Mk(T) }
+impl[T] Greet for Box[T] { fn greet() -> Int = 1; }
+impl Greet for Box[Int] { fn greet() -> Int = 2; }
+fn main() -> Int = 0;
+|} in
+  match tc_source src with
+  | Ok () ->
+      Alcotest.fail "#559 generic subsumption: impl[T] Box[T] overlapping \
+                     Box[Int] must be rejected as overlapping; the checker \
+                     accepted them — the hole has regressed"
+  | Error msg ->
+      Alcotest.(check bool) "error names trait coherence" true
+        (contains_str "coherence" msg)
 
 let coherence_tests = [
   Alcotest.test_case "duplicate impl (same self type) → rejected"    `Quick test_coherence_duplicate_rejected;
   Alcotest.test_case "impls for distinct types → accepted"           `Quick test_coherence_distinct_types_ok;
   Alcotest.test_case "distinct generic args → accepted (no over-reject)" `Quick test_coherence_distinct_generic_args_ok;
+  Alcotest.test_case "generic subsumption (impl[T] Box[T] vs Box[Int]) → rejected" `Quick test_coherence_generic_subsumption_rejected;
 ]
 
 (* ============================================================================
@@ -2490,23 +2503,16 @@ let test_resume_multishot_loud_fail () =
       Alcotest.(check bool) "error names the multi-shot resume limit" true
         (contains_str "multi-shot resume" msg)
 
-let test_resume_nontail_known_shallow () =
-  (* KNOWN shallow-resume incompleteness: the correct result is 105; the
-     shallow interpreter returns the resumed value 5. Flip to VInt 105 when
-     delimited continuations land (Refs #555). *)
-  match interp_main (fixture "handle_resume_nontail.affine") with
-  | Ok (Value.VInt 5) -> ()
-  | Ok (Value.VInt 105) ->
-      Alcotest.fail
-        "non-tail resume now returns 105 — delimited continuations appear to \
-         have landed; update this pin and the #555 CAPABILITY-MATRIX note"
-  | Ok v -> Alcotest.failf "non-tail resume: expected VInt 5 (known shallow), got %s" (Value.show_value v)
-  | Error msg -> Alcotest.failf "non-tail resume should evaluate (shallow), got error: %s" msg
+(* The non-tail single-shot resume residual (#555 / #623) is pinned as an xfail
+   in test/xfail/test_xfail_pins.ml (test_resume_nontail_xfail): it asserts the
+   CORRECT result (105) and fails-as-expected while the shallow interpreter
+   returns 5, flipping to a loud XPASS the day delimited continuations land.
+   Anchored from docs/SOUNDNESS.adoc. Kept out of this passing suite so there is
+   one pin convention, not two. *)
 
 let resume_soundness_tests = [
   Alcotest.test_case "interp: single-shot tail-resume evaluates to 5"   `Quick test_resume_single_shot_tail;
   Alcotest.test_case "interp: multi-shot resume → loud failure"         `Quick test_resume_multishot_loud_fail;
-  Alcotest.test_case "interp: non-tail resume → 5 (KNOWN shallow #555)" `Quick test_resume_nontail_known_shallow;
 ]
 
 (* ============================================================================

test/xfail/dune

@@ -0,0 +1,5 @@
+(test
+ (name test_xfail_pins)
+ (libraries affinescript)
+ (deps
+  (source_tree ../e2e)))

test/xfail/test_xfail_pins.ml

@@ -0,0 +1,121 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2024-2026 hyperpolymath (Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>) *)
+
+(** xfail pin harness for the soundness ledger (docs/SOUNDNESS.adoc, property 5).
+
+    Each pin asserts the DESIRED behaviour of a known soundness hole. Because the
+    hole is still present, the assertion currently FAILS — which is the expected
+    state, reported as [XFAIL-OK]. The day the hole is fixed, the assertion
+    PASSES, which is unexpected and reported as [XPASS]: the process exits
+    non-zero (so [dune runtest] and the gate both go red) with a message telling
+    the engineer to update the ledger row rather than silence the pin.
+
+    Polarity / fail-closed contract:
+      - pin body raises [Xfail] when the desired behaviour is NOT met (hole
+        present)         -> XFAIL-OK (exit 0 contribution)
+      - pin body returns normally (desired behaviour met, hole gone)
+                          -> XPASS    (exit 1)
+      - pin body raises ANY OTHER exception (parse error, missing fixture, …)
+                          -> XERROR   (exit 1) — pin infrastructure is broken,
+                             so we fail closed rather than mistake it for an
+                             expected failure.
+
+    The shell gate (tools/check-soundness-ledger.sh, property 5) runs this
+    executable, asserts every pin named by a `residual (pinned)` / `open
+    (tracked)` ledger row reports XFAIL-OK, and surfaces XPASS as the distinct
+    "is the hole fixed?" alarm. *)
+
+open Affinescript
+
+exception Xfail of string
+
+(* Locate test/e2e/fixtures across the run contexts we care about:
+   AFFINE_FIXTURES override (the gate sets this), the dune-test sandbox
+   (cwd = _build/default/test/xfail, fixtures at ../e2e/fixtures via the
+   source_tree dep), cwd = test/, and cwd = repo root. Fail closed if none. *)
+let fixtures_dir =
+  let cands =
+    (match Sys.getenv_opt "AFFINE_FIXTURES" with Some d -> [ d ] | None -> [])
+    @ [ "../e2e/fixtures"; "e2e/fixtures"; "test/e2e/fixtures" ]
+  in
+  match List.find_opt Sys.file_exists cands with
+  | Some d -> d
+  | None ->
+    failwith
+      "xfail: cannot locate test/e2e/fixtures (set AFFINE_FIXTURES to its path)"
+
+let fixture name = Filename.concat fixtures_dir name
+
+let parse path =
+  try Parse_driver.parse_file path
+  with e -> failwith ("parse " ^ path ^ ": " ^ Printexc.to_string e)
+
+let resolve_symbols prog =
+  let loader = Module_loader.create (Module_loader.default_config ()) in
+  match Resolve.resolve_program_with_loader prog loader with
+  | Ok (rctx, _) -> rctx.symbols
+  | Error (e, _) -> failwith ("resolve: " ^ Resolve.show_resolve_error e)
+
+(* ---- Pin: #555 / #623 — interpreter non-tail single-shot resume ----------
+   `let x = op(); x + 100` with `op() => resume(5)` should yield 105 once the
+   continuation is reified; the shallow tree-walking interpreter yields 5. *)
+let test_resume_nontail_xfail () =
+  let path = fixture "handle_resume_nontail.affine" in
+  let prog = parse path in
+  let _ = resolve_symbols prog in
+  let v =
+    match Interp.eval_program prog with
+    | Error e -> failwith ("eval: " ^ Value.show_eval_error e)
+    | Ok env -> (
+      match Value.lookup_env "main" env with
+      | Error _ -> failwith "no `main` binding"
+      | Ok f -> (
+        match Interp.apply_function f [] with
+        | Ok v -> v
+        | Error e -> failwith ("apply main: " ^ Value.show_eval_error e)))
+  in
+  match v with
+  | Value.VInt 105 -> () (* desired met -> XPASS: the hole is fixed *)
+  | Value.VInt 5 ->
+    raise (Xfail "non-tail resume returns 5, not 105 (shallow continuation)")
+  | other ->
+    raise
+      (Xfail ("non-tail resume returned " ^ Value.show_value other ^ ", not 105"))
+
+(* ---- Pin: #555-stub / #624 — Lean backend drops `return` ------------------
+   The agreed remedy (#624) is to fail loud on early `return`; today
+   `codegen_lean` returns Ok and silently lowers the body to `:= ()`. *)
+let test_stub_backend_return_xfail () =
+  let path = fixture "stub_backend_return_dropped.affine" in
+  let prog = parse path in
+  let symbols = resolve_symbols prog in
+  match Lean_codegen.codegen_lean prog symbols with
+  | Error _ -> () (* desired met -> XPASS: the backend now fails loud *)
+  | Ok _ ->
+    raise
+      (Xfail
+         "Lean_codegen.codegen_lean returned Ok; early `return` silently dropped")
+
+let pins =
+  [ ("test_resume_nontail_xfail",
+     "#555/#623 interp non-tail resume -> 5 not 105", test_resume_nontail_xfail);
+    ("test_stub_backend_return_xfail",
+     "#555-stub/#624 Lean drops `return`", test_stub_backend_return_xfail) ]
+
+let () =
+  let bad = ref false in
+  List.iter
+    (fun (name, reason, body) ->
+      match try `Ok (body ()) with Xfail m -> `Xfail m | e -> `Err (Printexc.to_string e) with
+      | `Xfail _ -> Printf.printf "XFAIL-OK %s -- %s\n" name reason
+      | `Ok () ->
+        bad := true;
+        Printf.printf
+          "XPASS %s -- pin passed; is the hole fixed? update docs/SOUNDNESS.adoc\n"
+          name
+      | `Err m ->
+        bad := true;
+        Printf.printf "XERROR %s -- pin infrastructure failed: %s\n" name m)
+    pins;
+  flush stdout;
+  if !bad then exit 1 else exit 0

tools/check-capability-anchors.sh

@@ -0,0 +1,73 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Anti-staleness gate for the capability matrix's test anchors
+# (docs/CAPABILITY-MATRIX.adoc "== Test anchors").
+#
+# The matrix is the authoritative feature-readiness doc. Its "Test anchors"
+# section pins each enforcement claim ("works" / "enforced" / "partial") to the
+# executable test(s) that exercise it — the same test-anchoring discipline the
+# soundness ledger uses (tools/check-soundness-ledger.sh). This gate makes those
+# anchors falsifiable: it extracts every test path the matrix names and fails the
+# build if any has gone missing, so a feature cannot keep a green status row
+# after its test is deleted or renamed without this section (and CI) noticing.
+#
+# Checks:
+#   1. The matrix exists and carries a "== Test anchors" section.
+#   2. Every test/*.ml and test/e2e/fixtures/*.affine path named anywhere in the
+#      matrix actually exists on disk.
+#
+# Usage:  ./tools/check-capability-anchors.sh
+# Wired into:  just check (via the `guard` recipe) and CI (.github/workflows/ci.yml).
+# Run from anywhere; it cd's to the repo root itself.
+
+set -euo pipefail
+
+cd "$(dirname "$0")/.."
+
+MATRIX="docs/CAPABILITY-MATRIX.adoc"
+
+fail=0
+note() { printf '%s\n' "$*" >&2; }
+
+# --- 1. The matrix exists and carries its Test-anchors section ---------------
+if [ ! -f "$MATRIX" ]; then
+  note "ERROR: the capability matrix is missing: $MATRIX"
+  exit 1
+fi
+if ! grep -q "^== Test anchors" "$MATRIX"; then
+  note "ERROR: $MATRIX lost its '== Test anchors' section."
+  note "       That section anchors each feature-readiness claim to an"
+  note "       executable test. Restore it (see the soundness ledger for the"
+  note "       same pattern: docs/SOUNDNESS.adoc)."
+  fail=1
+fi
+
+# --- 2. Every test path the matrix names actually exists ---------------------
+missing=0
+while IFS= read -r path; do
+  [ -z "$path" ] && continue
+  if [ ! -f "$path" ]; then
+    if [ "$missing" -eq 0 ]; then
+      note "ERROR: $MATRIX names test anchors that no longer exist:"
+      missing=1
+      fail=1
+    fi
+    note "         - $path"
+  fi
+done < <(grep -oE 'test/[A-Za-z0-9_./-]+\.(ml|affine)' "$MATRIX" | LC_ALL=C sort -u)
+if [ "$missing" -eq 1 ]; then
+  note "       Either restore the test or update the matrix to its new anchor"
+  note "       in the same change. A renamed/deleted test must not leave a"
+  note "       feature-readiness claim unmoored."
+fi
+
+if [ "$fail" -ne 0 ]; then
+  note ""
+  note "Capability-anchor guard failed. Feature-readiness claims in"
+  note "$MATRIX are drifting from the tests that back them."
+  exit 1
+fi
+
+echo "OK: capability anchors intact — Test-anchors section present + every named test exists."