Proof: progress + preservation for the surface type system

[hyperpolymath]

Parent: #513

Statement

For the surface AffineScript bidirectional type system, prove:

• Progress: a well-typed closed expression is either a value or can take a step.
• Preservation: a well-typed expression that takes a step remains well-typed at the same type.

Concretely

For the term language defined in lib/ast.ml + the bidirectional checking judgments in lib/typecheck.ml (synth / check mutually defined), and the call-by-value operational semantics encoded in lib/interp.ml:

Γ ⊢ e ⇒ τ      ⟹    e is a value  ∨  ∃ e'. e → e'             (Progress)
Γ ⊢ e ⇒ τ  ∧  e → e'   ⟹   Γ ⊢ e' ⇒ τ                          (Preservation)

Mechanisation

Lean 4 preferred (mature Mathlib, good inductive-type ergonomics) or Coq (sibling ephapax repo precedent). Target location: formal/Progress.lean + formal/Preservation.lean + formal/Semantics.lean (operational semantics) + formal/Syntax.lean (typed-syntax inductive). Mirror the ephapax-affine directory layout where it's already been done by hand.

Size

XL. Estimate: 3–4 weeks of focused work for someone fluent in the mechaniser. Can be broken into milestones: (1) syntax + values inductive; (2) operational-semantics relation; (3) typing judgments; (4) progress lemma; (5) preservation lemma; (6) congruence/substitution lemmas as needed.

Dependencies / out of scope

• Effect rows: defer to Proof: borrow-graph soundness (no use-after-move + no conflict + BorrowOutlivesOwner) #515 (effect-row well-formedness) — model with an opaque carrier or stub first.
• Borrow checker: separate workstream (Proof: progress + preservation for the surface type system #514); model the affine sublanguage's resource discipline without the full borrow graph first.
• Generics / row polymorphism: prove the monomorphic core first; polymorphism extension is a separate slice.

Status

NOT STARTED. Filed by 2026-06-01 audit.

🤖 Generated with Claude Code