|
| 1 | +// SPDX-License-Identifier: CC-BY-SA-4.0 |
| 2 | +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) |
| 3 | += AffineScript — Proof-Needs Inventory |
| 4 | +Jonathan D.A. Jewell |
| 5 | +:toc: left |
| 6 | +:toclevels: 3 |
| 7 | +:sectnums: |
| 8 | +:sectnumlevels: 2 |
| 9 | + |
| 10 | +This is the single document that enumerates *what AffineScript must prove*, at |
| 11 | +*what rigour*, with *what current status*. It is deliberately honest about the |
| 12 | +gap between the soundness *arguments* the project relies on (prose in |
| 13 | +`docs/academic/proofs/`, the borrow-checker comments in `lib/borrow.ml`, |
| 14 | +`docs/CAPABILITY-MATRIX.adoc`) and the soundness *proofs* that are actually |
| 15 | +mechanized today (almost none — see <<status>>). |
| 16 | + |
| 17 | +It supersedes the previous near-empty `PROOF-NEEDS.md`, which recorded only the |
| 18 | +2026-03-29 template-ABI cleanup (preserved in <<history>>). |
| 19 | + |
| 20 | +[IMPORTANT] |
| 21 | +==== |
| 22 | +This inventory is a *catalogue of obligations*, not a relicensing or a code |
| 23 | +change. Filing it does not assert any obligation is discharged. Each row's |
| 24 | +*Status* column is the ground truth; "stated", "prose", and "absent" all mean |
| 25 | +**not proven**. |
| 26 | +==== |
| 27 | + |
| 28 | +[#vocab] |
| 29 | +== Status & rigour vocabulary |
| 30 | + |
| 31 | +[cols="1,4"] |
| 32 | +|=== |
| 33 | +| Term | Meaning |
| 34 | + |
| 35 | +| `absent` | No artifact exists. Not even a statement. |
| 36 | +| `stated` | The theorem is written as a type/lemma signature, but the body is a hole (`?todo`, `Admitted`, `sorry`). Proves nothing. |
| 37 | +| `prose` | A paper argument exists (markdown). Convincing-to-a-human, machine-unchecked. |
| 38 | +| `partial` | A restricted case is machine-checked; the general theorem is not. |
| 39 | +| `mechanized` | Fully machine-checked under a `--safe`-equivalent discipline (no postulates/axioms/`Admitted`). |
| 40 | +|=== |
| 41 | + |
| 42 | +Rigour tiers (effort, mirroring the umbrella issue #513): `S` small · |
| 43 | +`M` medium · `L` large · `XL` extra-large. |
| 44 | + |
| 45 | +[#status] |
| 46 | +== 1. Current mechanization status — the "afresh" baseline |
| 47 | + |
| 48 | +A fresh sweep of the repo (2026-06-20) finds the mechanized core is *thinner* |
| 49 | +than the prose corpus suggests: |
| 50 | + |
| 51 | +* **`docs/academic/formal-verification/solo-core/`** — the only core-language |
| 52 | + formalisation. Covers the *Solo* fragment only: STLC + Unit + Product + Sum + |
| 53 | + `let` + QTT quantities `{0, 1, ω}`. `Syntax/Context/Quantity/Typing` are |
| 54 | + populated; **`Soundness.idr` is statements-only** — `data Step` has *no |
| 55 | + constructors* ("intentionally omitted until week 3"), and |
| 56 | + `progress = ?todo_progress`, `preservation = ?todo_preservation`. Status: |
| 57 | + `stated`. It proves nothing yet. Solo *excludes* traits, effects, rows, |
| 58 | + refinements, dependent types, ownership/borrowing, records, arrays, modules, |
| 59 | + and `unsafe`. |
| 60 | +* **`docs/academic/proofs/*.md`** — seven prose proofs (type-soundness, |
| 61 | + ownership-soundness, effect-soundness, quantitative-types, dependent-types, |
| 62 | + row-polymorphism, coherence-parametricity) plus DB-theory notes. Status: |
| 63 | + `prose`. None mechanized. |
| 64 | +* **`docs/academic/mechanized/{agda,coq,lean}/README.md`** — explicit |
| 65 | + *"Status: Stub / Planned"* placeholders. No proof content. |
| 66 | +* **`affinescript-vite/verification/proofs/{agda,coq,lean4,idris2}/`** — RSR |
| 67 | + *templates* ("Replace with your project's domain-specific proofs"); the Coq |
| 68 | + `TypeSafety.v` is example lemmas about list length, not AffineScript. Not |
| 69 | + core-metatheory. |
| 70 | +* **`formal/`** — the directory #513 names as the mechanized-proof target |
| 71 | + **does not exist**. |
| 72 | +* **Research tracks** (not core soundness): `docs/academic/tropical-session-types/` |
| 73 | + (Lean), `proposals/echo-types/EchoEncodingFaithfulness.agda`, |
| 74 | + `proposals/idaptik/migrated/**/*Boundary.agda` (echo-types loss-with-residue, |
| 75 | + a *different* project living in `proposals/`). |
| 76 | + |
| 77 | +[WARNING] |
| 78 | +==== |
| 79 | +**Known soundness *holes* (execution-verified, open).** These are bugs that |
| 80 | +*falsify* the corresponding prose proof's assumptions. Each is tracked as a |
| 81 | +defect but **none has a stated proof obligation** whose discharge would have |
| 82 | +caught it or would prevent regression — that linkage is itself a gap (see |
| 83 | +<<missed>>). |
| 84 | +
|
| 85 | +* **#554** — borrow checker *accepts* use-after-move through a callee-returned |
| 86 | + borrow (`let r = pick(a); consume(a); *r` typechecks). Polonius residual: #553 |
| 87 | + (ADR-022, 0% implemented). CORE-01/#177 closed 2026-05-30 did **not** close this. |
| 88 | +* **#555** — `handle` is mis-lowered on core-WASM / JS-text / Deno-ESM (effect |
| 89 | + arms dropped); interpreter dispatch is shallow single-shot tail-resume only. |
| 90 | +* **#556** — async CPS table-miss silently lowers synchronously. |
| 91 | +* **#558** — refinement-type predicates parse but are silently *not enforced*. |
| 92 | +* **#559** — trait coherence is *not checked*. |
| 93 | +
|
| 94 | +v1 readiness ledger: #563. Proof programme umbrella: #513. |
| 95 | +==== |
| 96 | + |
| 97 | +[#missed] |
| 98 | +== 2. Proof obligations missed before (pre-faces, uncatalogued) |
| 99 | + |
| 100 | +These predate the faces work; they were simply never written down as |
| 101 | +obligations. They are the "we might have missed" half of the brief. |
| 102 | + |
| 103 | +[cols="1,3,1,1,2"] |
| 104 | +|=== |
| 105 | +| ID | Obligation | Rigour | Status | Notes / issue |
| 106 | + |
| 107 | +| P-1 |
| 108 | +| **The inventory itself.** No document enumerated proof needs; `PROOF-NEEDS.md` |
| 109 | + held only a cleanup note. (Closed by *this* file.) |
| 110 | +| S | `mechanized` |
| 111 | +| — |
| 112 | + |
| 113 | +| P-2 |
| 114 | +| **Solo progress + preservation.** Discharge the two holes in `Soundness.idr`: |
| 115 | + give `Step` its constructors and prove |
| 116 | + `progress`/`preservation`/`affinePreservation`. |
| 117 | +| XL | `stated` |
| 118 | +| #513 must-have 1; solo-core Track F1 wks 3–12 |
| 119 | + |
| 120 | +| P-3 |
| 121 | +| **Borrow-graph soundness.** A well-typed program never observes a moved/aliased |
| 122 | + value. Must *exclude* the #554 counterexample (callee-returned borrow). |
| 123 | +| XL | `prose` |
| 124 | +| #513 must-have 2; counterexample #554; #553 |
| 125 | + |
| 126 | +| P-4 |
| 127 | +| **QTT affine usage.** Quantities `{0,1,ω}` are respected: `1`-vars used exactly |
| 128 | + once, `0`-vars erased, semiring laws hold. |
| 129 | +| L | `prose` |
| 130 | +| #513 must-have 3; prose `quantitative-types.md` |
| 131 | + |
| 132 | +| P-5 |
| 133 | +| **HM inference soundness + principality.** Inferred types are well-typed and |
| 134 | + principal. |
| 135 | +| L | `prose` |
| 136 | +| #513 must-have 4; prose `inference-algorithm.md` |
| 137 | + |
| 138 | +| P-6 |
| 139 | +| **Effect-row soundness.** A function performs no effect outside its row; row |
| 140 | + unification is sound. *Blocked* — the backend (#555) does not implement the |
| 141 | + semantics this proof would assume (see <<outstanding>>). |
| 142 | +| M | `prose` |
| 143 | +| #513 must-have 5; blocked on #555 |
| 144 | + |
| 145 | +| P-7 |
| 146 | +| **Name-resolution determinism.** Resolution is a deterministic total function |
| 147 | + of the program. |
| 148 | +| M | `absent` |
| 149 | +| #513 must-have 6 |
| 150 | + |
| 151 | +| P-8 |
| 152 | +| **Parser conformance.** The grammar accepts exactly the documented language |
| 153 | + (property-tested). |
| 154 | +| M | `absent` |
| 155 | +| #513 must-have 8 |
| 156 | + |
| 157 | +| P-9 |
| 158 | +| **Refinement enforcement = proof obligation.** #558 is simultaneously a bug |
| 159 | + *and* the missing obligation "refinement predicates are checked." Drawing that |
| 160 | + equivalence is itself the catalogue gap. |
| 161 | +| L | `absent` |
| 162 | +| #558 |
| 163 | + |
| 164 | +| P-10 |
| 165 | +| **Trait coherence.** At most one instance resolves per (trait, type); #559 is |
| 166 | + the open counterexample. |
| 167 | +| L | `absent` |
| 168 | +| #559; #513 high-priority |
| 169 | +|=== |
| 170 | + |
| 171 | +[#outstanding] |
| 172 | +== 3. Additional needs arising from outstanding work |
| 173 | + |
| 174 | +The work in flight changes which obligations are *load-bearing* and which are |
| 175 | +*blocked*. |
| 176 | + |
| 177 | +* **K-1 — Codegen WASM semantic-preservation is the keystone (#513 must-have 7).** |
| 178 | + `⟦compile(p)⟧_wasm = ⟦p⟧_source` for the operational semantics. This is the |
| 179 | + single obligation every *face* and every *aLib conformer* ultimately rests on: |
| 180 | + prove the backend preserves meaning once, and front-end face theorems |
| 181 | + (<<faces>>) compose into end-to-end correctness. Rigour `XL`. Status `prose` |
| 182 | + (`operational-semantics.md` / `denotational-semantics.md` are the inputs). |
| 183 | +* **K-2 — Effect-soundness is *blocked*, not merely unproven.** P-6 cannot be |
| 184 | + honestly *stated against the current backend* because #555 drops handler arms |
| 185 | + on three of the codegen targets. The obligation must be split: (a) prove |
| 186 | + soundness against the *interpreter's intended* handler semantics, then (b) |
| 187 | + prove the lowered targets refine that semantics — which (b) currently *fails*. |
| 188 | + This makes #555 a proof-blocking defect, not just a runtime bug. |
| 189 | +* **K-3 — Borrow soundness must be stated to *reject* #554.** Any mechanized P-3 |
| 190 | + must take the #554 program as a *negative* test (must not typecheck). Without |
| 191 | + Polonius (#553) the current checker cannot; so P-3's statement should be |
| 192 | + written now even though its proof waits on #553. |
| 193 | +* **K-4 — `CAPABILITY-MATRIX.adoc` rows are latent obligations.** Every row not |
| 194 | + marked `enforced` (effects `partial`, refinements `declared-but-unwired`, …) |
| 195 | + is a place where a prose proof presumes behaviour the implementation does not |
| 196 | + deliver. The matrix should cross-link each such row to its P-/F- obligation |
| 197 | + here. |
| 198 | + |
| 199 | +[#faces] |
| 200 | +== 4. New proof needs from the *faces* work |
| 201 | + |
| 202 | +The faces architecture (ADR-010: surface transformers `lib/<face>_face.ml` + |
| 203 | +error-vocabulary formatter `lib/face.ml` + pragma detector `lib/face_pragma.ml`; |
| 204 | +"different faces, same cube") introduces obligations that are **entirely absent |
| 205 | +from #513's 8 must-haves and 12 high-priority items.** This is the core |
| 206 | +discovery of the review: the proof programme predates faces and never grew to |
| 207 | +cover them. |
| 208 | + |
| 209 | +[cols="1,3,1,1,2"] |
| 210 | +|=== |
| 211 | +| ID | Obligation | Rigour | Status | Seed / issue |
| 212 | + |
| 213 | +| F-1 |
| 214 | +| **Transformer semantics-preservation — the *real* same-cube theorem.** For |
| 215 | + each face `F` with surface→canonical transform `T_F`, the typed-wasm |
| 216 | + denotation is preserved: `⟦T_F(p)⟧_wasm = ⟦T_canonical(canon(p))⟧_wasm` for all |
| 217 | + well-typed face-`F` programs `p`. This is the *front-end* analogue of the |
| 218 | + backend keystone K-1; together they give end-to-end "same cube". Needs the |
| 219 | + AffineScript AST + wasm semantics formalised. |
| 220 | +| XL | `absent` |
| 221 | +| new |
| 222 | + |
| 223 | +| F-2 |
| 224 | +| **Same-cube cross-face agreement (observational).** Any two faces compiling |
| 225 | + the same abstract program emit observationally-equivalent wasm (same effect |
| 226 | + trace, same return). *Partially mechanized*: `invariant-path/proofs/SameCube.agda` |
| 227 | + (`--safe`) proves the unit-returning-tail case, which is exactly where the two |
| 228 | + lowering classes the verifier found still agree. |
| 229 | +| L | `partial` |
| 230 | +| `SameCube.agda` (inv-path #33); **divergence instance #601** |
| 231 | + |
| 232 | +| F-3 |
| 233 | +| **Face pragma detection is total + deterministic + confluent.** |
| 234 | + `Face_pragma.detect_in_source` returns exactly one face (or falls through to |
| 235 | + the canonical default) for every input; it is independent of bytes past the |
| 236 | + first code token; the alias table (`parse_face_name`: rattle→Python, |
| 237 | + jaffa→Js, pseudo→Pseudocode, lucid→Lucid, cafe→Cafe, +brand names) is a |
| 238 | + *function* (no name maps to two faces); and dispatch `--face` > pragma > |
| 239 | + extension is confluent (same source ⇒ same face). Face analogue of P-7. |
| 240 | +| M | `absent` |
| 241 | +| new; `lib/face_pragma.ml` |
| 242 | + |
| 243 | +| F-4 |
| 244 | +| **Error-vocabulary faithfulness (simulation).** Each `Face.format_*_for_face` |
| 245 | + preserves the *referent* of the canonical error: same error class, same |
| 246 | + offending identifier, same fix-direction. Formally: the per-face translation |
| 247 | + is a total simulation of the canonical error algebra (exhaustiveness is |
| 248 | + OCaml-checked; *semantic* faithfulness is not), so a face can never make error |
| 249 | + *X* read as a different error *Y*. |
| 250 | +| M | `absent` |
| 251 | +| new; `lib/face.ml` |
| 252 | + |
| 253 | +| F-5 |
| 254 | +| **`render_ty` faithfulness / non-collision.** The per-face type renaming |
| 255 | + (`Option[T]`→`Maybe T` (Lucid), `→ T?` (Cafe), `→ T \| null` (Js); |
| 256 | + `Unit`→`None`/`null`/`nothing`; `Bool`→…) is an *injective, invertible* |
| 257 | + renaming of canonical type names, and never collapses two distinct canonical |
| 258 | + types to one face string inside a single message (e.g. Js maps both `Unit` and |
| 259 | + `Option[T]` into "null"-shaped text — show this is unambiguous in context). |
| 260 | +| S | `absent` |
| 261 | +| new; `lib/face.ml` `render_ty` |
| 262 | + |
| 263 | +| F-6 |
| 264 | +| **Preview round-trip totality.** The `preview-{python,js,pseudocode,lucid,cafe}` |
| 265 | + subcommands are total, and parsing the preview of `p` under face `F` yields a |
| 266 | + program denotationally equal to `p` (`parse_F ∘ preview_F ≈ id` up to |
| 267 | + denotation). If faces are "the same cube", the preview path must round-trip. |
| 268 | +| M | `absent` |
| 269 | +| new |
| 270 | + |
| 271 | +| F-7 |
| 272 | +| **Face confluence with canonicalisation.** An explicit pragma is never |
| 273 | + silently overridden in a way that changes denotation; resolving a face and |
| 274 | + then canonicalising commutes (`canon ∘ T_F = canon ∘ T_canonical ∘ surface_F`). |
| 275 | + Ties F-1 and F-3 together. |
| 276 | +| M | `absent` |
| 277 | +| new |
| 278 | +|=== |
| 279 | + |
| 280 | +[NOTE] |
| 281 | +==== |
| 282 | +**Why F-2 is `partial`, not done.** Grounding `examples/same-cube/greet` |
| 283 | +against a real build split the six faces into *two* wasm classes — |
| 284 | +`{canonical, jaffa, cafe}` emit a trailing call as a *statement* (`{ a; }`), |
| 285 | +`{rattle, pseudo, lucid}` as a *tail expression* (`{ a }`). For a |
| 286 | +unit-returning action these are observationally identical (proven in |
| 287 | +`SameCube.agda`); for a *value-returning* tail they genuinely diverge in result |
| 288 | +type. That concrete divergence is filed as **#601** and is the precise reason |
| 289 | +F-1 (full transformer preservation) is non-trivial rather than a formality. |
| 290 | +==== |
| 291 | + |
| 292 | +== 5. Adjacent repositories (same cube, wider lens) |
| 293 | + |
| 294 | +* **aggregate-library (aLib) — cross-*cube* conformance, not cross-*face*.** |
| 295 | + Faces unify *syntax* over one cube; aLib unifies a *library API* over *many* |
| 296 | + cubes. Its YAML conformance vectors are a property-test obligation (each |
| 297 | + conformer satisfies every vector — the aLib analogue of P-8), and its spec |
| 298 | + "Properties" sections (commutativity, associativity, identity, …) are exactly |
| 299 | + the *stdlib algebraic-law* obligations #513 lists as high-priority. The |
| 300 | + AffineScript reference conformer (`aggregate-library/src/affinescript/ALib.affine`) |
| 301 | + is where those laws become AffineScript proof obligations. |
| 302 | +* **invariant-path — the same-cube *harness*.** `proofs/SameCube.agda` is the |
| 303 | + first mechanized faces proof (seed of F-2); `scripts/verify-same-cube.sh` |
| 304 | + compiles every face to wasm and sha256-compares as the empirical (test-tier) |
| 305 | + companion. Treat these as the F-2 home until a `formal/` faces track exists in |
| 306 | + this repo. |
| 307 | + |
| 308 | +== 6. Recommended sequencing |
| 309 | + |
| 310 | +[cols="1,4,1"] |
| 311 | +|=== |
| 312 | +| Wave | Items | Gates |
| 313 | + |
| 314 | +| 0 (now) |
| 315 | +| Stand up `formal/` (the #513 target dir). *State* — without proving — P-2, |
| 316 | + P-3 (rejecting #554), F-1, F-3, F-4 as signatures/holes, mirroring the |
| 317 | + solo-core skeleton style. Cross-link `CAPABILITY-MATRIX.adoc` rows (K-4). |
| 318 | +| — |
| 319 | + |
| 320 | +| 1 |
| 321 | +| Discharge solo-core P-2 (progress+preservation). Mechanize F-3/F-5 (small, |
| 322 | + self-contained OCaml-property obligations; no semantics needed). |
| 323 | +| Wave 0 |
| 324 | + |
| 325 | +| 2 |
| 326 | +| K-1 codegen preservation skeleton → unblocks F-1, F-2-full, F-6. Split P-6 per |
| 327 | + K-2 and surface #555 as proof-blocking. |
| 328 | +| Wave 1; #555 |
| 329 | + |
| 330 | +| 3 |
| 331 | +| Extend solo-core to Duet (traits+effects: P-6, P-10) then Ensemble (P-4 full, |
| 332 | + refinements P-9, borrowing P-3-full pending #553). |
| 333 | +| Wave 2; #553 |
| 334 | +|=== |
| 335 | + |
| 336 | +[#xref] |
| 337 | +== Appendix A — relationship to #513 / #563 |
| 338 | + |
| 339 | +* **#513** (proof-programme umbrella) supplies P-2…P-10 and K-1. This document |
| 340 | + *adds* the faces obligations F-1…F-7 and the aLib law-conformance obligation, |
| 341 | + which #513 does not mention, and links the open soundness holes |
| 342 | + (#554/#555/#556/#558/#559) to the obligations they falsify. |
| 343 | +* **#563** (v1 readiness ledger) tracks the holes as release blockers; the |
| 344 | + `Status` column here should stay consistent with that ledger. |
| 345 | +* When `formal/` lands, each `P-`/`F-` ID should become a module name or lemma |
| 346 | + label so the catalogue and the mechanization share one namespace. |
| 347 | + |
| 348 | +[#history] |
| 349 | +== Appendix B — historical note (preserved) |
| 350 | + |
| 351 | +*Template ABI Cleanup (2026-03-29).* The template ABI was removed — it was |
| 352 | +creating a false impression of formal verification. The removed files |
| 353 | +(`Types.idr`, `Layout.idr`, `Foreign.idr`) contained only RSR template |
| 354 | +scaffolding with unresolved `{{PROJECT}}`/`{{AUTHOR}}` placeholders and no |
| 355 | +domain-specific proofs. When this project needs formal ABI verification, create |
| 356 | +domain-specific Idris2 proofs following the pattern in repos like `typed-wasm`, |
| 357 | +`proven`, `echidna`, or `boj-server`. (The same caution applies to the |
| 358 | +`affinescript-vite/verification/proofs/` *templates* surveyed in <<status>>: |
| 359 | +they are scaffolding, not metatheory.) |
0 commit comments