// SPDX-License-Identifier: CC-BY-SA-4.0
// SPDX-FileCopyrightText: 2024-2026 hyperpolymath (Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>)
= AffineScript Soundness Ledger
// Freshness stamp — a real main-ancestor commit (survives squash-merge); advance
// it (and --reseal) in any change that touches a soundness path. See "Keeping
// this honest" and tools/check-soundness-ledger.sh (property 4).
:ground-truth-sha: 65c2ae3
:ground-truth-date: 2026-06-21
:stamp-verified-by: tools/check-soundness-ledger.sh
:toc: macro
:toclevels: 2
:icons: font

[IMPORTANT]
====
*This document is the single source of truth for the status of AffineScript's
known soundness holes.* If any other document — `README.adoc`,
`docs/CAPABILITY-MATRIX.adoc`, `docs/PROOF-NEEDS.adoc`, `.claude/CLAUDE.md`, a
dated `STATE-*.adoc` snapshot, the wiki — disagrees with this ledger about
whether a hole is open, fixed, fenced, or removed, *this ledger wins and the
other document is drift to be corrected*.
====

This ledger is *test-anchored* and *content-bound*: every row names the fixture
or test that proves its claim, and `tools/check-soundness-ledger.sh` (wired into
`just check` + CI) fails the build if any named anchor goes missing, if a status
surface stops pointing here, if a named anchor's *content hash* drifts from the
digest manifest (`tools/soundness-anchors.sha256`), if a soundness path moved
since the freshness stamp without the stamp being advanced, or if a
`residual (pinned)` / `open (tracked)` row lacks a live, currently-failing pin.
Those bindings are what stop the ledger going stale silently — including in the
one direction the name-only design could not catch: a fixture that survives but
has its assertion quietly weakened underneath it.

Ground-truthed at `{ground-truth-sha}` on {ground-truth-date} by source
inspection at the cited `file:line` anchors, with `dune build` and
`dune runtest` green, and the anchor-digest manifest regenerated
(`tools/check-soundness-ledger.sh --reseal`) in the same change. The status
words below are deliberate; read them precisely.

toc::[]

== Why this file exists

Soundness status used to live in ~6 places that drifted independently — the
capability matrix, a survey block in `.claude/CLAUDE.md`, dated `STATE-*`
snapshots, session handoffs, the wiki. A reader (human or agent) who happened to
open the stale one got a stale answer, in the *dangerous* direction: "this hole
is still open" long after it was fixed, or — worse in principle — the reverse.
This file is the structural fix, resting on four mechanisms, *each enforced by
the gate rather than asserted in prose*:

[horizontal]
One surface:: Soundness-hole status is stated here and nowhere else. Other docs
may summarise and link here; they may not maintain a competing per-issue ledger.
The gate enforces the back-link.

Anchored to tests:: Each claim cites the executable artefact that proves it. The
gate verifies the artefact *exists*.

Content-bound:: The gate also verifies the artefact still *says what it said*:
each anchor — fixture, pinned-test body, and suite file — is pinned to a content
digest in `tools/soundness-anchors.sha256`, so an anchor cannot have its assertion
eroded — weakened, re-baselined, or silently re-scoped — without the digest
mismatching and the build failing. Prose nailed to a fixture *by name only* can
still rot if the fixture's meaning drifts; prose nailed *by content* cannot.

Stamped, and the stamp is enforced:: The freshness attribute records the
main-ancestor commit this was last reconciled against. The gate fails if `HEAD`
has touched any anchored fixture, any cited `lib/*.ml` soundness path, or this
ledger's table since `:ground-truth-sha:` without the stamp being advanced in the
same change. The stamp records when the file last *actually matched* the
compiler, not merely when someone last claimed to check.

== Status vocabulary

[cols="1,4",options="header"]
|===
| Term | Meaning

| `fixed`
| The previously-unsound behaviour is gone. The program that used to be wrongly
accepted is now rejected, or the wrong result is now the right one.

| `loud-fail`
| The construct is not implementable on this path, but it errors at compile-time
or run-time — it never silently emits a plausible-wrong value. "Fail loud, never
silent" is the governing rule.

| `removed`
| The feature whose surface could not be honestly enforced was withdrawn from the
language, so there is no unenforced surface left to mislead anyone.

| `residual (pinned)`
| A known-incorrect behaviour still exists, but an *xfail* test pins it: the test
asserts the *desired* behaviour, currently fails (the bug is present), and is
caught by the xfail harness as a tolerated expected-failure. It flips to an
*unexpected pass* — failing the build with a distinct "is the hole fixed?"
message — the day the hole is fixed.

| `open (tracked)`
| A known gap with no fix yet, tracked by an issue. Stated here so it cannot be
mistaken for a guarantee. Pinned the same way as `residual (pinned)`.

| `partial`
| Implemented and load-bearing for common cases; the named residual is the gap.
|===

== The ledger

Every row in this table is in scope for the gate. There are no soundness-relevant
holes outside this table; the "still open" prose below is a reader's digest *of
these rows*, not a separately-maintained list.

[cols="1,4,1,3",options="header"]
|===
| Issue | Soundness claim (current behaviour) | Status | Proven in code

| #554 / #177
| Use-after-move through a callee-returned borrow is rejected.
`let r = pick(a); consume(a); *r` no longer type-checks — it is reported as
`MoveWhileBorrowed`. CORE-01 (#177) closed; this was its last execution-verified
hole.
| `fixed`
| `test/e2e/fixtures/borrow_callee_returned_borrow_uam.affine` (+ the
`borrow_callee_returned_borrow_aggregate.affine`,
`borrow_callee_returned_borrow_interproc.affine`,
`borrow_callee_returned_borrow_match_arm.affine`,
`borrow_callee_returned_borrow_return_stmt.affine` hardening variants and
`borrow_callee_value_return_ok.affine` anti-over-rejection)

| #555 (codegen)
| `handle` / `resume` on every compiled backend (core-WASM, WasmGC, Deno-ESM,
JS-text, C) fails loud with `UnsupportedFeature` instead of silently dropping
handler arms. The old failure — compile the body, drop the arms, lower `resume`
as a pass-through (42 in the interpreter vs 41 in wasm) — is gone.
| `loud-fail`
| `test/e2e/fixtures/handle_return_arm.affine`; `lib/codegen.ml` `ExprHandle` /
`ExprResume` arms; `lib/codegen_deno.ml`

| #555 (interp, multi-shot)
| Calling `resume` more than once in a handler fails loud (it cannot be expressed
without reified continuations, and previously returned a silently-wrong value).
| `loud-fail`
| `test/e2e/fixtures/handle_resume_multishot.affine`; `lib/interp.ml` resume
invocation counter

|*#555* (interp, non-tail single-shot)
|`let x = op(); x + 100` resuming to `5` returns `5`, not `105`: the shallow
 tree-walking continuation has already unwound the bind chain. This is the one
 genuinely-still-silent shape, on the *interpreter* path only. It needs a CPS
 rewrite of `eval` (blocked: OCaml 4.14 has no native effect handlers and the
 interpreter must stay `js_of_ocaml`-compatible — owner-steer item). Tracked: #623.
|*residual (pinned)*
|`test/e2e/fixtures/handle_resume_nontail.affine` +
 `test_resume_nontail_known_shallow` (asserts the wrong-but-known value; flips
 to failing the day delimited continuations land)

| #556
| Async CPS table-miss fails loud instead of silently lowering synchronously.
| `loud-fail`
| `test/e2e/fixtures/async_sync_fallback.affine` (+ `async_no_boundary.affine`,
`async_passthrough_thenable.affine`)

| #558
| Refinement / dependent types were removed in v1 (2026-04-10). There is no
`TRefined` node for the checker to silently ignore; `assume(…)` is rejected at
parse and `T where (P)` is a parse error. You cannot write an unenforced
predicate.
| `removed`
| `test/e2e/fixtures/assume_rejected.affine` + `test_parse_assume_rejected`

| #559 (concrete)
| Overlapping trait impls whose self types unify are rejected as a coherence
violation, before the check pass, so an ambiguous instance base is reported up
front.
| `fixed`
| `lib/typecheck.ml` `check_all_coherence` call; `lib/trait.ml` `check_coherence`
/ `check_all_coherence`; `test_coherence_duplicate_rejected`

| #559 (generic subsumption)
| Generic-subsumption overlap — `impl[T] Greet for Box[T]` overlapping
`impl Greet for Box[Int]` — *is* detected and rejected as a coherence violation
(the unification-based check instantiates the generic head: `Box[T]` unifies with
`Box[Int]`). Ground-truthed 2026-06-21 against the running compiler — this row
was previously, wrongly, marked "not yet detected".
| `fixed`
| `test_coherence_generic_subsumption_rejected`

| #553 (Polonius)
| The Polonius extractor (ADR-022) is implemented through M3 but is
TEST-ONLY / unwired — it gates no production verdict. The lexical `lib/borrow.ml`
is the production checker; the extractor is diffed against it over the fixture
corpus with a shrinking allowlist (7 known divergences).
| `partial`
| `test/test_borrow_polonius.ml` (parallel-run diff gate + `known_divergences`,
count pinned at 7)

| #555-stub / #624
| The Lean and Why3 experimental backends now FAIL LOUD on an early `return`
instead of silently dropping it. Previously `gen_block` skipped the `return`
statements, so `fn f(){ return 1; … }` lowered to `:= ()`; now a
`Ast.fn_body_contains_return` fence makes `codegen_lean` / `codegen_why3` return
`Error`. Fixed via #624. (NB: #628 tracked this as "#560"; that issue is actually
variable-string wasm ops — #624 is the correct tracker. This change supplies the
loud fence #628 could not, so the row is now `loud-fail` (it was previously a
pinned residual).)
| `loud-fail`
| `test/e2e/fixtures/stub_backend_return_dropped.affine` +
`test_stub_backend_return_fenced` (positive check: asserts
`Lean_codegen.codegen_lean` returns `Error` on the early-`return` program — it was
`Ok`; the check would fail if the silent drop regressed).
|===

== Still open — read before claiming "sound"

The implementation holes marked `fixed` / `loud-fail` / `removed` above are
closed. Honesty requires naming what is *not* a guarantee. Each item here is a
row in the table above, restated for the hurried reader — not a separate list:

* *Interpreter non-tail resume* (#555 residual, pinned; tracked as #623) — see
  the ledger row.
* *Stub backends drop `return`.* The Lean and Why3 *experimental* code
  generators drop `return` statements wholesale — a broader codegen-honesty gap
  than #555, flagged but not yet fenced (tracked as #624). Treat all
  non-reference backends as experimental (see `docs/CAPABILITY-MATRIX.adoc`).
* *Generic-subsumption coherence* (#559 follow-up) — see the ledger row.

== Closed holes are not proofs

Closing an *implementation* hole is not the same as having *metatheory*. The
soundness *arguments* for the holes above (`docs/academic/proofs/*.adoc`, the
comments in `lib/borrow.ml`) remain `prose`, and the `Solo` core fragment's
`progress` / `preservation` are still `?todo`. Mechanisation has *started* — an
axiom-free Coq/Rocq `formal/` track (codegen-preservation: K-1
`K1_CodegenPreservation.v`, K-1-with-`let` `K1Let_CodegenPreservation.v`, and
the F-1 transformer-preservation composition; #620/#621) — but it does not yet
cover any hole in this ledger. The proof obligations, their rigour tiers, and
their (mostly `prose` / `absent`) status are catalogued in
`docs/PROOF-NEEDS.adoc` (umbrella issue #513). The one-line distinction:

The one distinction to carry away, stated so the polish of *this ledger* is not
mistaken for the rigour of the *metatheory*:

[NOTE]
====
The compiler now fails loud on these shapes and the residuals are pinned by
tests — so the *bookkeeping* about soundness is mechanically enforced and
current. The soundness *arguments* for the holes in this ledger are still paper
proofs or fragment proofs, not a machine-checked guarantee about the whole
language. A green gate here means "the status table is honest and the fixtures
still say what they said," *not* "AffineScript is proven sound".
====

The v1 release-readiness ledger is issue #563.

== Keeping this honest (how to update)

[arabic]
. *Ground-truth by running the tool.* Reproduce the behaviour against the built
compiler (`dune build && dune runtest`, `dune exec affinescript -- …`). Never
edit a status here from another doc — that is how drift starts. If the compiler
disagrees with a row, *the compiler wins* and the row is corrected (that is how
the #559-generic row above was fixed).
. *Change the row, change the anchor, change the digest.* If you fix or break a
hole, update the status word, its anchoring fixture/test, *and* regenerate
`tools/soundness-anchors.sha256` (`tools/check-soundness-ledger.sh --reseal`) in
the same change. The gate fails if a named anchor no longer exists *or* if its
content digest drifts from the manifest without a reseal.
. *Bump the stamp, in the same change.* Update `:ground-truth-sha:` (to a real
main-ancestor commit you verified against) and `:ground-truth-date:`. The gate
fails if a soundness path moved since the stamp without the stamp advancing.
. *Do not fork the ledger.* If another doc needs to mention soundness status, it
links here; it does not copy the table. The gate checks the back-links from
`README.adoc`, `docs/CAPABILITY-MATRIX.adoc`, `docs/PROOF-NEEDS.adoc`,
`docs/NAVIGATION.adoc`, and `.claude/CLAUDE.md`.

== See also

* link:CAPABILITY-MATRIX.adoc[CAPABILITY-MATRIX.adoc] — authoritative feature
readiness (this ledger owns soundness-hole status; the matrix links here).
* link:PROOF-NEEDS.adoc[PROOF-NEEDS.adoc] — what must be proven, at what rigour,
with what status (now including the mechanized Wave-0 `formal/` track).
* link:reports/HANDOFF-2026-06-17-soundness.adoc[reports/HANDOFF-2026-06-17-soundness.adoc],
link:reports/TIDY-UP-LEDGER-2026-06-16.adoc[reports/TIDY-UP-LEDGER-2026-06-16.adoc]
— the dated session reports this ledger consolidates (historical inputs).
