Proof: affine discipline soundness — @linear consumed exactly once (QTT semiring + Scaled-Let) #516

Parent: #513

Statement

For the quantity checker in lib/quantity.ml, prove the QTT-semiring soundness of affine consumption:

If quantity_ok(prog) accepts a program under the (0, 1, ω) semiring with Scaled-Let (ADR-002) and the Mut quantity policy, then every @linear binding is consumed exactly once on every execution trace.

Concretely

quantity_ok(prog)  ⟹  ∀ trace t of prog. ∀ binding b : QOne.  uses_in_trace(b, t) = 1

Plus the dual:

• QZero bindings consumed = 0 times
• QOmega bindings consumed 0..∞ times

Mechanisation

Lean 4 or Coq. Target: formal/Quantity/{Semiring.lean, ScaledLet.lean, Soundness.lean}. The (0, 1, ω) semiring is well-studied (Atkey 2018 "Syntax and Semantics of Quantitative Type Theory") — mathlib has rough scaffolding.

Recent landings:

• Scaled-Let (ADR-002): BUG-001 / BUG-002 fixed in stdlib Http: typed-wasm target (convergence ABI; shared with Ephapax) #225 (?) — verify which PR
• Omitted-binder scaling (BUG-004): same line of work

Size

L. Estimate: 2–3 weeks. The semiring laws are mechanical; the soundness proof against the operational semantics is the work.

Status

NOT STARTED.

🤖 Generated with Claude Code