// SPDX-License-Identifier: CC-BY-SA-4.0
// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
= AffineScript — Proof-Needs Inventory
Jonathan D.A. Jewell
:toc: left
:toclevels: 3
:sectnums:
:sectnumlevels: 2

This is the single document that enumerates *what AffineScript must prove*, at
*what rigour*, with *what current status*. It is deliberately honest about the
gap between the soundness *arguments* the project relies on (prose in
`docs/academic/proofs/`, the borrow-checker comments in `lib/borrow.ml`,
`docs/CAPABILITY-MATRIX.adoc`) and the soundness *proofs* that are actually
mechanized today: a growing axiom-free Coq core (20 files) that pins each
obligation on a deliberately *small model* — no full-language theorem is
discharged yet (see <<status>>).

It supersedes the previous near-empty `PROOF-NEEDS.md`, which recorded only the
2026-03-29 template-ABI cleanup (preserved in <<history>>).

[IMPORTANT]
====
This inventory is a *catalogue of obligations*, not a relicensing or a code
change. Filing it does not assert any obligation is discharged. Each row's
*Status* column is the ground truth; "stated", "prose", and "absent" all mean
**not proven**.
====

[#vocab]
== Status & rigour vocabulary

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

| `absent`     | No artifact exists. Not even a statement.
| `stated`     | The theorem is written as a type/lemma signature, but the body is a hole (`?todo`, `Admitted`, `sorry`). Proves nothing.
| `prose`      | A paper argument exists (markdown). Convincing-to-a-human, machine-unchecked.
| `partial`    | A restricted case is machine-checked; the general theorem is not.
| `mechanized` | Fully machine-checked under a `--safe`-equivalent discipline (no postulates/axioms/`Admitted`).
|===

Rigour tiers (effort, mirroring the umbrella issue #513): `S` small ·
`M` medium · `L` large · `XL` extra-large.

[#status]
== 1. Current mechanization status — the "afresh" baseline

A fresh sweep of the repo (2026-06-20) finds the mechanized core is *thinner*
than the prose corpus suggests:

* **`docs/academic/formal-verification/solo-core/`** — the only core-language
  formalisation. Covers the *Solo* fragment only: STLC + Unit + Product + Sum +
  `let` + QTT quantities `{0, 1, ω}`. `Syntax/Context/Quantity/Typing` are
  populated; **`Soundness.idr` is statements-only** — `data Step` has *no
  constructors* ("intentionally omitted until week 3"), and
  `progress = ?todo_progress`, `preservation = ?todo_preservation`. Status:
  `stated`. It proves nothing yet. Solo *excludes* traits, effects, rows,
  refinements, dependent types, ownership/borrowing, records, arrays, modules,
  and `unsafe`.
* **`docs/academic/proofs/*.md`** — seven prose proofs (type-soundness,
  ownership-soundness, effect-soundness, quantitative-types, dependent-types,
  row-polymorphism, coherence-parametricity) plus DB-theory notes. Status:
  `prose`. None mechanized.
* **`docs/academic/mechanized/{agda,coq,lean}/README.md`** — explicit
  *"Status: Stub / Planned"* placeholders. No proof content.
* **`affinescript-vite/verification/proofs/{agda,coq,lean4,idris2}/`** — RSR
  *templates* ("Replace with your project's domain-specific proofs"); the Coq
  `TypeSafety.v` is example lemmas about list length, not AffineScript. Not
  core-metatheory.
* **`formal/`** — the directory #513 names as the mechanized-proof target now
  **exists** (Coq/Rocq 8.18), axiom-free throughout — **20 files, 35 `Print
  Assumptions` closure reports**, all "Closed under the global context". Codegen
  keystone: `K1_CodegenPreservation.v` (K-1 minimal) +
  `K1Let_CodegenPreservation.v` (K-1 grown with variables/`let`/environment).
  Faces front-end: `F1_TransformerPreservation.v` (F-1, composing on K-1).
  `Siblings_Stated.v` states P-2/P-3/F-3/F-4, **discharged for concrete models**
  in `P2_Progress.v` (first-order) + `P2_Stlc.v` (STLC with functions + the
  substitution lemma, funext-free) / `P3_BorrowSound.v` (single-bit) +
  `P3_BorrowGraph.v` (multi-resource loan graph) / `F3_PragmaDecidable.v` /
  `F4_ErrorFaithful.v` / `F5_RenderFaithful.v` (render non-collision).
  Affine/QTT layer: `QttSemiring.v` (`{0,1,ω}`) +
  `AffineUsage.v` (`λx.x` affine, `λx. x x` not) + `QttTyping.v` (quantitative
  typing, `usage x t = Γ x` sound) + `QttDynamic.v` (the dynamic half:
  β-reduction preserves the usage profile). Real lift (`REAL-LIFT.adoc`):
  `RealWasm.v` (real `lib/wasm.ml` IR — i32 core + locals + structured `IfElse`
  + `Block`/`Loop`/`Br`/`BrIf`, fuel-indexed `wexec`) + `RealCompile.v` (R1+R2:
  the first real `⟦compile p⟧ = ⟦p⟧`, incl. `if`) + `RealLoop.v` (R2-loops: a
  branch-aware executor `cexec` over backward jumps, a source `while`/`seq`/`set`
  statement language, and `compile_stmt_correct` — the lowered terminating
  `while` simulates the reference run, settling the #601 value-returning-tail
  question concretely: the statement tail leaves an empty value stack) +
  `RealMem.v` (R-mem: word-addressed linear memory with `I32Load`/`I32Store`, a
  structural memory executor `mexec`, a bump allocator, and the store→load /
  2-cell tuple-layout round-trips — `field i at base+i` proved via `set_nth`'s
  get-after-set; the heap precondition for arrays/records/strings/floats).
  Record rows: `Rows.v` (P-11 — progress + preservation for extensible records).
  See <<outstanding>>, <<faces>>.
* **Research tracks** (not core soundness): `docs/academic/tropical-session-types/`
  (Lean), `proposals/echo-types/EchoEncodingFaithfulness.agda`,
  `proposals/idaptik/migrated/**/*Boundary.agda` (echo-types loss-with-residue,
  a *different* project living in `proposals/`).

[WARNING]
====
**Known soundness *holes* (execution-verified, open).** These are bugs that
*falsify* the corresponding prose proof's assumptions. Each is tracked as a
defect but **none has a stated proof obligation** whose discharge would have
caught it or would prevent regression — that linkage is itself a gap (see
<<missed>>).

These were the execution-verified *implementation* holes. As of 2026-06 their
implementation status is closed and now tracked, test-anchored, in
link:SOUNDNESS.adoc[docs/SOUNDNESS.adoc] — #554 *fixed* (UAM via callee-returned
borrow rejected), #555 *fenced loud* on every compiled backend (one pinned
interpreter residual), #556 *fixed*, #558 *removed* (refinements withdrawn, not
left unenforced), #559 *fixed* for concrete overlaps, #553 Polonius M1–M3 but
test-only/unwired. **That does not discharge the proof obligations below.**
Closing a hole means the implementation no longer exhibits the counterexample;
it does *not* mean the property is mechanically proven. The obligations these
holes motivate — most pointedly that the borrow proof must now be *stated to
reject the (now-fixed) #554 program* as a negative test — remain `prose` or
`absent`. Implementation truth: SOUNDNESS.adoc. Proof truth: this file.

v1 readiness ledger: #563. Proof programme umbrella: #513.
====

[#missed]
== 2. Proof obligations missed before (pre-faces, uncatalogued)

These predate the faces work; they were simply never written down as
obligations. They are the "we might have missed" half of the brief.

[cols="1,3,1,1,2"]
|===
| ID | Obligation | Rigour | Status | Notes / issue

| P-1
| **The inventory itself.** No document enumerated proof needs; `PROOF-NEEDS.md`
  held only a cleanup note. (Closed by *this* file.)
| S | `mechanized`
| —

| P-2
| **Solo progress + preservation.** Discharge the two holes in `Soundness.idr`:
  give `Step` its constructors and prove
  `progress`/`preservation`/`affinePreservation`.
| XL | `partial`
| #513 must-have 1; solo-core (Idris2) `stated`; **progress + preservation
  mechanized** for a first-order fragment (`formal/P2_Progress.v`) AND for the
  **STLC with functions + the substitution lemma** (`formal/P2_Stlc.v`,
  funext-free). QTT/affine quantities are the remaining increment

| P-3
| **Borrow-graph soundness.** A well-typed program never observes a moved/aliased
  value. Must *exclude* the #554 counterexample (callee-returned borrow).
| XL | `partial`
| #513 must-have 2; **mechanized** for a single-bit model
  (`formal/P3_BorrowSound.v`) and a *multi-resource borrow graph* with loan
  edges + liveness (`formal/P3_BorrowGraph.v`: soundness, completeness,
  move-locality, multi-resource #554 rejected). #554 fixed (SOUNDNESS.adoc);
  full P-3 needs `lib/borrow.ml`'s CFG + Polonius #553

| P-4
| **QTT affine usage.** Quantities `{0,1,ω}` are respected: `1`-vars used exactly
  once, `0`-vars erased, semiring laws hold.
| L | `partial`
| #513 must-have 3; **mechanized** across four files: `formal/QttSemiring.v`
  (`{0,1,ω}` laws + occurrence homomorphism), `formal/AffineUsage.v` (`λx.x`
  affine, `λx. x x` not), `formal/QttTyping.v` — a quantitative type system whose
  usage context Γ is proven to track usage exactly (`usage x t = Γ x`) — and
  `formal/QttDynamic.v`, the *dynamic* half: β-reduction **preserves the usage
  profile** (`t → t' ⇒ ∀z, usage z t' = usage z t`), with the QTT scaling law
  (`qof_mult`) and `qtt_context_preserved` composing it with `usage_soundness`.
  The full operational development on the *real* AST (substitution lemma past the
  binder-free / closed-value fragment) is the remaining lift; prose
  `quantitative-types.md`

| P-5
| **HM inference soundness + principality.** Inferred types are well-typed and
  principal.
| L | `prose`
| #513 must-have 4; prose `inference-algorithm.md`

| P-6
| **Effect-row soundness.** A function performs no effect outside its row; row
  unification is sound. *Blocked* — the backend (#555) does not implement the
  semantics this proof would assume (see <<outstanding>>).
| M | `prose`
| #513 must-have 5; blocked on #555

| P-7
| **Name-resolution determinism.** Resolution is a deterministic total function
  of the program.
| M | `absent`
| #513 must-have 6

| P-8
| **Parser conformance.** The grammar accepts exactly the documented language
  (property-tested).
| M | `absent`
| #513 must-have 8

| P-9
| **Refinement enforcement = proof obligation.** #558 was simultaneously a bug
  *and* the missing obligation "refinement predicates are checked." *Withdrawn:*
  the refinement/dependent surface was *removed* in v1, so there is no unenforced
  predicate left to prove about (see link:SOUNDNESS.adoc[SOUNDNESS.adoc]).
  Retained for history; reopen only if refinements return.
| L | `absent` (withdrawn)
| #558

| P-10
| **Trait coherence.** At most one instance resolves per (trait, type). The
  *implementation* now rejects concrete overlaps (#559, see
  link:SOUNDNESS.adoc[SOUNDNESS.adoc]); generic-subsumption overlap is the open
  follow-up. The *proof* that resolution is unique remains unwritten.
| L | `absent`
| #559; #513 high-priority

| P-11
| **Record-row soundness.** Well-typed record operations never get stuck: a
  selection of a present label always reduces, and extension/restriction
  preserve typing over a `lacks`-checked row (no duplicate labels). Distinct
  from P-6 *effect*-row soundness.
| M | `mechanized`
| `formal/Rows.v` — progress + preservation for STLC + extensible records
  (empty/extend/select/restrict), funext-free, axiom-free. Wave W0
  (monomorphic rows); row-*variable* polymorphism is the W1 increment
|===

[#outstanding]
== 3. Additional needs arising from outstanding work

The work in flight changes which obligations are *load-bearing* and which are
*blocked*.

* **K-1 — Codegen WASM semantic-preservation is the keystone (#513 must-have 7).**
  `⟦compile(p)⟧_wasm = ⟦p⟧_source` for the operational semantics. This is the
  single obligation every *face* and every *aLib conformer* ultimately rests on:
  prove the backend preserves meaning once, and front-end face theorems
  (<<faces>>) compose into end-to-end correctness. Rigour `XL`. Status `partial`
  (was `prose`): a Wave-0 mechanized seed — `formal/K1_CodegenPreservation.v`
  (Coq, no axioms) — proves preservation for a minimal nat/bool · add/and
  fragment compiled to a stack machine — `K1Let_CodegenPreservation.v` grows it
  with de Bruijn variables, `let`, and an environment. The **real lift** onto the
  real AffineScript AST + real typed-WASM semantics is scoped in
  `formal/REAL-LIFT.adoc` (fragment ladder R0→R-eff); **R0 + R1 + R2 landed**.
  `formal/RealWasm.v` re-targets the *actual* `lib/wasm.ml` `instr`/`value_type`
  (i32 core + locals + structured `IfElse`); `formal/RealCompile.v` gives the
  **first real `⟦compile p⟧ = ⟦p⟧`** — resolved int/bool/`let`/binary/**if**
  source, reference `eval`, `compile` to real wasm, `compile_correct` (env↔locals
  agreement, existential-fuel) + `compile_program_correct`, retiring `K1`/`K1Let`
  on real objects. R2's conditionals forced `wexec` to become **fuel-indexed**
  (nested `list instr` defeats the structural guard checker); R2-loops
  (`Loop`/`Br`, value-returning tails) is next and settles #601 concretely.
* **K-2 — Effect-soundness is *blocked*, not merely unproven.** P-6 cannot be
  honestly *stated against the current backend* because #555 drops handler arms
  on three of the codegen targets. The obligation must be split: (a) prove
  soundness against the *interpreter's intended* handler semantics, then (b)
  prove the lowered targets refine that semantics — which (b) currently *fails*.
  This makes #555 a proof-blocking defect, not just a runtime bug.
* **K-3 — Borrow soundness must be stated to *reject* #554.** Any mechanized P-3
  must take the #554 program as a *negative* test (must not typecheck). *Done in
  the model:* `P3_BorrowSound.v` and `P3_BorrowGraph.v` reject the #554 witness
  (`[OBorrow; OMove; OUseRef]`); the full-language negative test still waits on
  Polonius (#553), which the real-checker statement needs to reject it in general.
* **K-4 — `CAPABILITY-MATRIX.adoc` rows are latent obligations.** Every row not
  marked `enforced` (effects `partial`, refinements `declared-but-unwired`, …)
  is a place where a prose proof presumes behaviour the implementation does not
  deliver. The matrix should cross-link each such row to its P-/F- obligation
  here.

[#faces]
== 4. New proof needs from the *faces* work

The faces architecture (ADR-010: surface transformers `lib/<face>_face.ml` +
error-vocabulary formatter `lib/face.ml` + pragma detector `lib/face_pragma.ml`;
"different faces, same cube") introduces obligations that are **entirely absent
from #513's 8 must-haves and 12 high-priority items.** This is the core
discovery of the review: the proof programme predates faces and never grew to
cover them.

[cols="1,3,1,1,2"]
|===
| ID | Obligation | Rigour | Status | Seed / issue

| F-1
| **Transformer semantics-preservation — the *real* same-cube theorem.** For
  each face `F` with surface→canonical transform `T_F`, the typed-wasm
  denotation is preserved: `⟦T_F(p)⟧_wasm = ⟦T_canonical(canon(p))⟧_wasm` for all
  well-typed face-`F` programs `p`. This is the *front-end* analogue of the
  backend keystone K-1; together they give end-to-end "same cube". Needs the
  AffineScript AST + wasm semantics formalised.
| XL | `partial`
| mechanized fragment: `formal/F1_TransformerPreservation.v` (composes on K-1)

| F-2
| **Same-cube cross-face agreement (observational).** Any two faces compiling
  the same abstract program emit observationally-equivalent wasm (same effect
  trace, same return). *Partially mechanized*: `invariant-path/proofs/SameCube.agda`
  (`--safe`) proves the unit-returning-tail case, which is exactly where the two
  lowering classes the verifier found still agree.
| L | `partial`
| `SameCube.agda` (inv-path #33); **divergence instance #601**

| F-3
| **Face pragma detection is total + deterministic + confluent.**
  `Face_pragma.detect_in_source` returns exactly one face (or falls through to
  the canonical default) for every input; it is independent of bytes past the
  first code token; the alias table (`parse_face_name`: rattle→Python,
  jaffa→Js, pseudo→Pseudocode, lucid→Lucid, cafe→Cafe, +brand names) is a
  *function* (no name maps to two faces); and dispatch `--face` > pragma >
  extension is confluent (same source ⇒ same face). Face analogue of P-7.
| M | `partial`
| **mechanized** for a model: `formal/F3_PragmaDecidable.v` (discharges the
  Siblings_Stated F3 statements); `lib/face_pragma.ml`

| F-4
| **Error-vocabulary faithfulness (simulation).** Each `Face.format_*_for_face`
  preserves the *referent* of the canonical error: same error class, same
  offending identifier, same fix-direction. Formally: the per-face translation
  is a total simulation of the canonical error algebra (exhaustiveness is
  OCaml-checked; *semantic* faithfulness is not), so a face can never make error
  *X* read as a different error *Y*.
| M | `partial`
| **mechanized** for a model: `formal/F4_ErrorFaithful.v` (discharges the
  Siblings_Stated F4 statement); `lib/face.ml`

| F-5
| **`render_ty` faithfulness / non-collision.** The per-face type renaming
  (`Option[T]`→`Maybe T` (Lucid), `→ T?` (Cafe), `→ T \| null` (Js);
  `Unit`→`None`/`null`/`nothing`; `Bool`→…) is an *injective, invertible*
  renaming of canonical type names, and never collapses two distinct canonical
  types to one face string inside a single message (e.g. Js maps both `Unit` and
  `Option[T]` into "null"-shaped text — show this is unambiguous in context).
| S | `partial`
| **mechanized** for the vocabulary model: `formal/F5_RenderFaithful.v` proves
  every face's renaming is injective (`render_inj` — no two canonical types
  collapse onto one string), incl. the Js/Cafe "null"/"?" overlap
  (`js_no_collapse`, `cafe_no_collapse`, `option_never_atom`). Faithful to the
  whole-string Unit/Bool match + canonical-inner Option rewrite; models the
  name vocabulary, not raw OCaml strings. `lib/face.ml` `render_ty`

| F-6
| **Preview round-trip totality.** The `preview-{python,js,pseudocode,lucid,cafe}`
  subcommands are total, and parsing the preview of `p` under face `F` yields a
  program denotationally equal to `p` (`parse_F ∘ preview_F ≈ id` up to
  denotation). If faces are "the same cube", the preview path must round-trip.
| M | `absent`
| new

| F-7
| **Face confluence with canonicalisation.** An explicit pragma is never
  silently overridden in a way that changes denotation; resolving a face and
  then canonicalising commutes (`canon ∘ T_F = canon ∘ T_canonical ∘ surface_F`).
  Ties F-1 and F-3 together.
| M | `absent`
| new
|===

[NOTE]
====
**Why F-2 is `partial`, not done.** Grounding `examples/same-cube/greet`
against a real build split the six faces into *two* wasm classes —
`{canonical, jaffa, cafe}` emit a trailing call as a *statement* (`{ a; }`),
`{rattle, pseudo, lucid}` as a *tail expression* (`{ a }`). For a
unit-returning action these are observationally identical (proven in
`SameCube.agda`); for a *value-returning* tail they genuinely diverge in result
type. That concrete divergence is filed as **#601** and is the precise reason
F-1 (full transformer preservation) is non-trivial rather than a formality.
====

== 5. Adjacent repositories (same cube, wider lens)

* **aggregate-library (aLib) — cross-*cube* conformance, not cross-*face*.**
  Faces unify *syntax* over one cube; aLib unifies a *library API* over *many*
  cubes. Its YAML conformance vectors are a property-test obligation (each
  conformer satisfies every vector — the aLib analogue of P-8), and its spec
  "Properties" sections (commutativity, associativity, identity, …) are exactly
  the *stdlib algebraic-law* obligations #513 lists as high-priority. The
  AffineScript reference conformer (`aggregate-library/src/affinescript/ALib.affine`)
  is where those laws become AffineScript proof obligations.
* **invariant-path — the same-cube *harness*.** `proofs/SameCube.agda` is the
  first mechanized faces proof (seed of F-2); `scripts/verify-same-cube.sh`
  compiles every face to wasm and sha256-compares as the empirical (test-tier)
  companion. Treat these as the F-2 home until a `formal/` faces track exists in
  this repo.

== 6. Recommended sequencing

[cols="1,4,1"]
|===
| Wave | Items | Gates

| 0
| **Done.** `formal/` stood up (Coq); **K-1 mechanized**; **F-1 mechanized**
  (composes on K-1); **P-2/P-3/F-3/F-4 mechanized** for concrete models
  (small-step progress+preservation; borrow soundness rejecting #554; pragma
  locality + alias functionality; error faithfulness). The axiom-free seed.
| —

| 1
| **Done.** Grew the models toward the real language: **P-2 → STLC with functions
  + the substitution lemma** (`P2_Stlc.v`, funext-free); **P-3 → a multi-resource
  borrow graph** (`P3_BorrowGraph.v`: loan edges, liveness, move-locality,
  multi-resource #554 rejected); **F-5 → `render_ty` non-collision**
  (`F5_RenderFaithful.v`: every face's renaming injective). *Leftover:* the K-4
  `CAPABILITY-MATRIX` cross-link.
| Wave 0

| 2
| **Done.** The affine/QTT layer — **`QttSemiring.v`** (`{0,1,ω}` laws +
  occurrence homomorphism), **`AffineUsage.v`** (`λx.x` affine, `λx. x x` not),
  **`QttTyping.v`** (static quantitative typing, `usage x t = Γ x` sound), and
  **`QttDynamic.v`** — the *dynamic* half: β-reduction preserves the usage
  profile (`step_preserves_usage`), the QTT scaling law, and `qtt_context_preserved`
  tying it back to `usage_soundness`. *Leftover:* generalise the dynamic
  development past the binder-free / closed-value fragment onto the real AST.
| Wave 1

| 3
| **The real lift (the bulk of the remaining work) — scoped + started.** Replace
  the toy objects with the real ones: formalise the **real AffineScript AST** and
  the **real typed-WASM operational semantics**, then re-prove K-1/F-1/F-2 against
  them (this is what makes K-1/F-1 `XL`, and what actually resolves #601). Planned
  as a strict-superset *fragment ladder* in `formal/REAL-LIFT.adoc`
  (R0→R1→R2→R-mem→R-float→R-str→R-call→R-wrap→R-eff); **R0 + R1 + R2 landed**
  (`formal/RealWasm.v` — real `lib/wasm.ml` IR, i32 core + locals + structured
  `IfElse`, fuel-indexed `wexec`; `formal/RealCompile.v` — the first real
  `⟦compile p⟧ = ⟦p⟧` incl. value-returning `if`, retiring K1/K1Let on real
  objects). **R2-loops** (`Loop`/`Br`, value-returning tails) is next and settles
  #601 concretely. Then the still-`prose`/`absent` obligations: P-5 (inference),
  P-6 (effects — blocked on #555/K-2, = rung R-eff), P-7 (resolution), P-8
  (parser), P-10 (coherence); faces F-6/F-7; full-language borrowing (P-3)
  pending #553.
| Wave 2; #555; #553
|===

[#xref]
== Appendix A — relationship to #513 / #563

* **#513** (proof-programme umbrella) supplies P-2…P-10 and K-1. This document
  *adds* the faces obligations F-1…F-7 and the aLib law-conformance obligation,
  which #513 does not mention, and links the open soundness holes
  (#554/#555/#556/#558/#559) to the obligations they falsify.
* **#563** (v1 readiness ledger) tracks the holes as release blockers; the
  `Status` column here should stay consistent with that ledger.
* When `formal/` lands, each `P-`/`F-` ID should become a module name or lemma
  label so the catalogue and the mechanization share one namespace.

[#history]
== Appendix B — historical note (preserved)

*Template ABI Cleanup (2026-03-29).* The template ABI was removed — it was
creating a false impression of formal verification. The removed files
(`Types.idr`, `Layout.idr`, `Foreign.idr`) contained only RSR template
scaffolding with unresolved `{{PROJECT}}`/`{{AUTHOR}}` placeholders and no
domain-specific proofs. When this project needs formal ABI verification, create
domain-specific Idris2 proofs following the pattern in repos like `typed-wasm`,
`proven`, `echidna`, or `boj-server`. (The same caution applies to the
`affinescript-vite/verification/proofs/` *templates* surveyed in <<status>>:
they are scaffolding, not metatheory.)
