Umbrella: 8 must-have + 12 high-priority proof obligations for the AffineScript compiler

[hyperpolymath]

Summary

Umbrella tracking the 8 must-have + 12 high-priority proof obligations for the AffineScript compiler, surfaced by the 2026-06-01 proof-obligation catalogue audit (142 total obligations identified). This is the spine of the "AffineScript will be the subject of almost everything" programme.

The 8 must-haves (each filed as a child issue below)

#	Area	Obligation	Mechanisation	Size
1	Type system	Progress + preservation for the surface language (bidirectional checker)	Lean 4 / Coq	XL
2	Borrow checker	Borrow-graph soundness: no use-after-move + no conflicting borrows + BorrowOutlivesOwner	Lean 4	XL
3	Affine discipline	QTT semiring: every @linear binding consumed exactly once (Scaled-Let ADR-002)	Lean 4 / Coq	L
4	Type inference	Hindley-Milner soundness + decidability of unification over TyVar/TyApp/effect rows	Coq	L
5	Effects	Effect-row well-formedness + unification + subsumption	Lean 4	M
6	Name resolution	Determinism: no two symbols at the same qualified path, import cycles rejected, module shadowing rules (ADR-014 / #228)	TLA+ / property tests	M
7	Codegen (WASM)	Semantic preservation: compiled WASM's observable behaviour matches source semantics (reference backend)	Why3	XL
8	Parser	Conformance: grammar accepts exactly the spec examples; Menhir conflict resolution stated (ADR-009 / ADR-012)	property tests	M

12 high-priority follow-ons (filed as child issues at lower urgency)

Trait coherence; row polymorphism transitivity; NLL last-use; return-escape; CFG-join in try/catch; effect-site closure (ADR-016 / #234); typed-WASM L7/L10/L13 emission; FFI ABI conformance (Zig C-ABI / #19 + wasm_export_call / #467); stdlib algebraic laws (umbrella); codegen-deno string escape + int division regressions; res-to-affine migration correctness (#488); formatter idempotence + linter determinism.

Conventions

• Each child issue carries the obligation statement, the mechanisation suggestion, the size estimate, and the upstream dependencies.
• Property-test obligations ship as Alcotest cases via the existing test/test_*.ml machinery — first batch landed in PR test(stdlib): batch 1 of algebraic-law property tests (6 cases) — stacked on #511 #512 (test/test_stdlib_laws.ml).
• Mechanised proofs target a new formal/ directory at the repo root following the ephapax / typed-wasm convention.

Out of scope here

• The 110 medium / marginal / ecosystem / cross-cutting obligations from the catalogue (filed separately when work picks them up).

🤖 Generated with Claude Code

[hyperpolymath]

Filed 2026-06-01 (this session):

• Proof: progress + preservation for the surface type system #514 — Progress + preservation (Lean 4 / Coq, XL)
• Proof: borrow-graph soundness (no use-after-move + no conflict + BorrowOutlivesOwner) #515 — Borrow-graph soundness: no-use-after-move / no-conflict / BorrowOutlivesOwner (Lean 4, XL)
• Proof: affine discipline soundness — @linear consumed exactly once (QTT semiring + Scaled-Let) #516 — Affine discipline: QTT semiring soundness (Lean 4 / Coq, L)
• Proof: Hindley-Milner soundness + principal types + decidability of unification #517 — Hindley-Milner soundness + principal types + decidable unification (Coq, L)
• Proof: effect-row well-formedness + soundness against ADR-016 walker + subsumption #518 — Effect-row well-formedness + ADR-016 walker soundness + subsumption (Lean 4, M)
• Proof / property: resolver determinism + import-cycle rejection + qualified-path canonicality (ADR-014) #519 — Resolver determinism + import-cycle rejection + ADR-014 canonicality (property tests, M)
• Proof: WebAssembly backend semantic preservation (source ⇓ v ⟹ wasm ⇓ encode(v)) #520 — WASM backend semantic preservation (Why3 / Coq, XL)
• Proof / property: parser conformance to spec + Menhir conflict-resolution stability (ADR-009 / ADR-012) #521 — Parser conformance + Menhir conflict stability (property tests, M)

Companion shipping:

• PR test(stdlib): batch 1 of algebraic-law property tests (6 cases) — stacked on #511 #512 — first batch of algebraic-law property tests (6 cases: string ++ semigroup + monoid, int / truncation codegen: integer / lowers to floating-point division on the JS-family backends #478 source-level, int + associativity). Stacked on fix(ci): foundational CI/CD audit — bytesLength + STEP 4-B stdlib decls + governance allowlist + Pages precheck + Scorecard caller perms #511 (foundational CI/CD fix).

Next slices of the catalogue's high-priority follow-ons + 110 medium / marginal items remain unfiled — will be created when work picks them up so the backlog stays signal-rich.