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

[hyperpolymath]

Makes docs/SOUNDNESS.adoc keep every promise it makes. The ledger on main is "prose ahead of mechanism" (it claims content-binding / stamp-enforcement / pinned xfails, but the gate enforced only 2 of those). This builds the missing mechanism, and folds in the closed-#625 capability-matrix anchoring.

The five properties (each maps to a function in the gate)

#	Property	Function	Provenance
1	Anchors exist	check_anchors_exist	Jonathan's #622 design (kept)
2	Back-links	check_backlinks	Jonathan's #622 design (kept)
3	Content-binding	check_content_binding + tools/soundness-anchors.sha256 + --reseal	new
4	Stamp-enforcement	check_stamp	new
5	Pin-liveness (xfail)	check_pins + test/xfail/test_xfail_pins.ml	new

## What this gate enforces is documented at the top of the script. Everything fails closed.

Ground-truth correction (compiler wins)

Running the compiler showed #559 generic-subsumption is already detected/rejected (impl[T] Greet for Box[T] vs impl Greet for Box[Int] → "Trait coherence violation"). So the ledger's open (tracked) "not yet detected" was stale in the dangerous direction. Corrected to fixed with a positive test; the stale test_e2e.ml comment fixed. → one fewer xfail pin than the spec assumed.

Also: the stub-return row uses #624 (the real tracker); #560 is variable-string wasm ops, unrelated — this change supplies the pin #628 couldn't (the fixture/test now exist). Stamp re-pointed to dd6c19e (a real main-ancestor; the old d55e22c was squash-orphaned). Metatheory note updated for the new formal/ proofs (#620–#627).

Self-tests — each new check watched failing

SELF-TEST 1 — Property 3 (mutate a fixture by one token):
  ERROR (property 3): anchor content drift vs tools/soundness-anchors.sha256 ...

SELF-TEST 2 — Property 4 (un-advanced/orphaned stamp + soundness change):
  ERROR (property 4): stamp d55e22c is not an ancestor of HEAD; re-point :ground-truth-sha: ...

SELF-TEST (5a) — Property 5 (pinned row names a missing pin):
  ERROR (property 1): test anchor not defined: test_stub_backend_return_DELETED
  FATAL: anchor test:test_stub_backend_return_DELETED: expected exactly one defining file, found 0 (fail closed)

SELF-TEST (5b) — Property 5 (an xfail pin flips to XPASS):
  ALARM (property 5): pin test_resume_nontail_xfail is PASSING — the hole may be fixed.
  Open docs/SOUNDNESS.adoc and update the row to 'fixed' (do NOT just silence the pin).

Full suite green (534 tests; xfail harness reports both pins XFAIL-OK), all four guard gates green, dune build/dune runtest green at dd6c19e.

Claims I could not make fully mechanical (named, not silently softened)

1. Content-binding scope. Fixtures + pinned-test bodies are digest-bound (11/12 anchors); the one SUITE-file anchor (#553 → test/test_borrow_polonius.ml) is existence+stamp-checked only — a whole-file hash is too coarse. The ledger sentence was tightened to say exactly this.
2. Stamp "advanced-in-this-change" detection is robust for the normal branch-off-fresh-main workflow (and the orphaned-stamp case fails closed, self-test 2). It has a known edge in a multi-commit-since-stamp history (stamp bumped in an earlier commit, soundness changed again later without re-bump could read as "advanced"); decision-2's full "diff-on-main" freshness check is not separately implemented. Flagged for your call.

CI

build job now checks out fetch-depth: 0 so property 4 can resolve the stamp; the xfail harness is in .ocamlformat-ignore (authored without ocamlformat available).

🤖 Generated with Claude Code

https://claude.ai/code/session_01BbxKhXQwTvVgkYDgBMLJoa

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 41 issues detected

Severity	Count
🔴 Critical	2
🟠 High	23
🟡 Medium	16

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action denoland/setup-deno@v2 needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "secret_action_without_presence_gate",
    "file": "instant-sync.yml",
    "action": "peter-evans/repository-dispatch",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
    "type": "js_exec_sync",
    "file": "/home/runner/work/affinescript/affinescript/packages/affinescript-cli/mod.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Shell execution -- validate input before passing to shell (2 occurrences, CWE-78)",
    "type": "js_exec_sync",
    "file": "/home/runner/work/affinescript/affinescript/packages/affine-vscode/mod.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
    "type": "js_exec_sync",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-vite/src/affine-plugin-improved.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "expect() in hot path (32 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/wasm_gen.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "expect() in hot path (29 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/affine_gen.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unsafe block -- requires SAFETY comment (2 occurrences, CWE-676)",
    "type": "unsafe_block",
    "file": "/home/runner/work/affinescript/affinescript/runtime/src/panic.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unsafe block -- requires SAFETY comment (1 occurrences, CWE-676)",
    "type": "unsafe_block",
    "file": "/home/runner/work/affinescript/affinescript/runtime/src/alloc.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unsafe block -- requires SAFETY comment (3 occurrences, CWE-676)",
    "type": "unsafe_block",
    "file": "/home/runner/work/affinescript/affinescript/runtime/src/ffi.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence