Repository navigation
Umbrella: 8 must-have + 12 high-priority proof obligations for the AffineScript compiler #513
Description
Activity
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.
- added a commit that references this issue
on Jul 28, 2026
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)
@linearbinding consumed exactly once (Scaled-LetADR-002)TyVar/TyApp/effect rows12 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
test/test_*.mlmachinery — 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).formal/directory at the repo root following the ephapax / typed-wasm convention.Out of scope here
🤖 Generated with Claude Code