Skip to content

README.adoc

Latest commit

 

History

History
302 lines (254 loc) · 14.3 KB

README.adoc

File metadata and controls

302 lines (254 loc) · 14.3 KB
Raw

AffineScript formal/ — Mechanized Metatheory (Coq/Rocq)

Table of Contents

This directory is the machine-checked home for the proof obligations catalogued in docs/PROOF-NEEDS.adoc, and is the formal/ target directory issue #513 names for mechanized proofs. Prover: Coq/Rocq 8.18 — chosen for the codegen/K-1 track because the typed-WASM target semantics interoperate with typed-wasm and ephapax, both of which use Coq (Semantics.v).

Important
.v here is Coq, not V-lang

Coq proof scripts use the .v extension — shared with Verilog and the estate-banned V-lang. Everything in formal/ is Coq/Rocq, not V-lang and not Verilog. The estate language policy carves Coq proof scripts out of the cicd_rules/vlang_detected rule (path_allow_prefixes for "Coq proof scripts"); .hypatia-ignore makes that explicit for this directory so a sweep cannot mistake it. Coq has no v.mod manifest, so vmod_detected never fires.

Contents

File Obligation Status

K1_CodegenPreservation.v

K-1 — codegen → typed-WASM preservation (minimal fragment)

mechanized, axiom-free

K1Let_CodegenPreservation.v

K-1, grown — adds variables, let, and an environment

mechanized, axiom-free

F1_TransformerPreservation.v

F-1 — face transformer semantics-preservation (composes on K-1)

mechanized, axiom-free

Siblings_Stated.v

P-2, P-3, F-3, F-4 — the obligation statements (parametric propositions)

stated — and now discharged for concrete models below

P2_Progress.v

P-2 — progress + preservation (nat/bool/add/if, first-order)

mechanized, axiom-free

P2_Stlc.v

P-2, grown — STLC with functions + the substitution lemma; progress
preservation (funext-free)

mechanized, axiom-free

P3_BorrowSound.v

P-3 — borrow soundness + the #554 witness rejected (single-bit model)

mechanized, axiom-free

P3_BorrowGraph.v

P-3, grown — multi-resource borrow graph (loan edges + liveness); soundness, completeness, move-locality, multi-resource #554 rejected

mechanized, axiom-free

F3_PragmaDecidable.v

F-3 — pragma locality + alias-table functionality

mechanized, axiom-free

F4_ErrorFaithful.v

F-4 — error rendering preserves class + referent

mechanized, axiom-free

QttSemiring.v

P-4 (Wave 2) — the QTT quantity semiring {0,1,ω}: operations, semiring + order laws, occurrence-count homomorphism

mechanized, axiom-free

AffineUsage.v

P-4 (Wave 2) — affine usage over the semiring: λx.x affine, λx. x x not (variable totals ω)

mechanized, axiom-free

QttTyping.v

P-4 (Wave 3) — quantitative typing fusing all three: the typing context tracks usage, proven sound (usage x t = Γ x)

mechanized, axiom-free

QttDynamic.v

P-4 (Wave 3) — the dynamic half: β-reduction preserves the usage profile; QTT scaling law; ties back to usage_soundness

mechanized, axiom-free

F5_RenderFaithful.v

F-5 — render_ty per-face type renaming is injective (no two canonical types collapse onto one displayed string), incl. the Js/Cafe "null"/"?" overlap

mechanized, axiom-free

RealWasm.v

Real lift R0+R1+R2 (REAL-LIFT.adoc) — the real lib/wasm.ml IR: i32 core + locals + comparisons + structured control (IfElse); fuel-indexed wexec with monotonicity (wexec_mono) + additive sequencing (wexec_app_some)

mechanized, axiom-free

RealCompile.v

Real lift R1+R2 — the first real ⟦compile p⟧ = ⟦p⟧: resolved int/bool/let/binop/if source, reference eval, compile to real wasm, compile_correct (retires K1/K1Let on real objects)

mechanized, axiom-free

Rows.v

P-11 — record-row soundness: progress + preservation for STLC + extensible records (empty/extend/select/restrict over a lacks-checked row), funext-free

mechanized, axiom-free

All mechanized theorems report Closed under the global context under Print Assumptions — no Admitted, no axioms — honouring the estate rule that load-bearing proofs be constructive and complete. Siblings_Stated.v records the obligation shapes as Definition …​ : Prop over section Variable`s (discharged at `End into closed, universally-quantified props); the P2_/P3_/F3_/F4_ files give concrete models and prove those propositions hold, each ending in a *_discharged : Siblings_Stated.<name> … := <proof> line that type-checks the concrete proof against the stated obligation.

Mechanized siblings (P-2, P-3, F-3, F-4, F-5)

Each is proven for a deliberately small concrete model — enough to discharge the stated obligation and pin its meaning, not the full language:

  • P-2 (P2_Progress.v) — a simply-typed first-order calculus (nat/bool/add/if), small-step, call-by-value, with the standard canonical-forms / progress / preservation development.

  • P-2, grown (P2_Stlc.v) — the Wave-1 increment: the simply-typed lambda calculus with functions, binders, and the substitution lemma (the thing the first-order version lacked). Full progress + preservation, funext-free — contexts are compared only on a term’s free variables (context_invariance), so it uses no functional_extensionality and stays axiom-free. The QTT/affine quantities (substructural context splitting) are the next increment.

  • P-3 (P3_BorrowSound.v) — a one-resource borrow calculus; proves the precise validity checker is sound and rejects the #554 witness ([OBorrow; OMove; OUseRef]), matching `lib/borrow.ml’s post-#554-fix behaviour.

  • P-3, grown (P3_BorrowGraph.v) — the Wave-1 increment: a multi-resource borrow graph with explicit loan edges (reference ↦ borrowed resource) and per-resource liveness; a deref is valid iff its loan target is still live (the Polonius-style, #553, reading). Proves soundness, completeness, and move-locality — moving resource b cannot change the validity of a deref borrowing some a ≠ b (the genuine borrow-graph property) — and rejects the multi-resource #554 program. Still needs the real lib/borrow.ml CFG / mutable borrows / aliasing for full P-3.

  • F-3 (F3_PragmaDecidable.v) — the alias table is a function, and detection factors through the scanned region, so it cannot depend on bytes past the pragma.

  • F-4 (F4_ErrorFaithful.v) — the face renderer preserves an error’s class and referent, changing only vocabulary, so no face can make error X read as a different error Y.

  • F-5 (F5_RenderFaithful.v) — render_ty’s per-face type-name renaming is injective: distinct canonical types never collapse onto one displayed string. Models the vocabulary it special-cases (`Unit, Bool, Option[_]), faithful to the whole-string Unit/Bool match and the canonical-inner Option rewrite (Js Option[Option[Int]] ⇒ "Option[Int] | null"). Proves the pointed case the obligation names — Js/Cafe render Unit as "null"/"?" and Option[T] with the same lexeme, yet the two never read as one type (js_no_collapse, cafe_no_collapse, option_never_atom).

Wave 2: the affine/QTT layer (P-4)

The quantities {0,1,ω} and their algebra are what make AffineScript affine:

  • QttSemiring.v — the multiplicity semiring: qplus (context addition, with 1 + 1 = ω) and qmult (scaling), all semiring + order laws by exhaustive case analysis, and the homomorphism qof (m + n) = qplus (qof m) (qof n) (occurrence counts add under QTT addition).

  • AffineUsage.v — reads a variable’s multiplicity as qof (count x t), proves usage composes under the semiring through application (usage x (app f a) = qplus (usage x f) (usage x a)), and defines affine well-formedness. Payoff: λx.x is affine; λx. x x is not — its variable totals ω, exceeding the affine bound. The mechanized statement of "a linear value may not be duplicated".

  • QttTyping.v (Wave 3 capstone) — a quantitative type system fusing all three: qtt Γ t A where the usage context Γ tracks quantities (Q_App adds Γ₁ + Γ₂, Q_Lam binds at the used multiplicity). The capstone theorem usage_soundness : qtt Γ t A → ∀x, usage x t = Γ x proves the typing context records exactly the QTT usage — the static quantity discipline is sound against occurrence counts. Corollary: a term typed in a singleton context uses that variable exactly once.

  • QttDynamic.v (Wave 3) — the dynamic half. A small-step β-reduction on the QTT terms with the headline step_preserves_usage: t → t' implies usage z t' = usage z t for every z, so the quantity accounting is a dynamic invariant. Adds the QTT scaling law usage z (subst x v b) = usage z b + usage x b · usage z v (via the new qof_mult ×-homomorphism), an affine-no-increase corollary, and qtt_context_preserved, which composes the dynamic invariant with usage_soundness so a well-typed term’s QTT context stays valid across a step. β substitutes a closed value (the closed-program convention P2_Stlc.v also uses), so it is capture-/axiom-free.

The remaining step is the full operational development on the real AST: the quantity-preserving substitution lemma generalised past the binder-free fragment and the closed-value convention.

K-1 and its growth

K1_CodegenPreservation.v proves, for a minimal two-type fragment (nat + bool, add + and) compiled to a small stack machine:

Definition K1_preservation : Prop :=
  forall e v, seval e = Some v -> wexec (compile e) [] = Some [obs v].
Theorem k1_preservation_holds : K1_preservation.        (* proven *)

K1Let_CodegenPreservation.v re-proves the same shape for a grown fragment with de Bruijn variables and let, evaluated under an environment; the target machine gains a locals register and compilation balances IBind/IUnbind. if/structured control is the next increment (it needs a target control construct + a termination measure, deliberately out of scope here).

F-1 composes on K-1

F1_TransformerPreservation.v models a face surface fexp with parser sugar, a transform elaborate : fexp → sexp (the T_F of ADR-010), and the face’s own semantics feval. It proves the transform preserves meaning (feval f = seval (elaborate f)) and then chains K-1 to get end-to-end codegen preservation, plus the cross-face same-cube corollary (faces landing on the same canonical AST emit identical code). The observational version for the trailing-statement/tail split is mechanized separately in invariant-path/proofs/SameCube.agda (F-2).

The real lift (R0 → R2)

The real lift replaces the toy stack machine with the actual lib/wasm.ml IR and the toy source with the real (resolved) AST, climbing a strict-superset fragment ladder. Three rungs are down:

  • R0 (RealWasm.v) — the pure i32 numeric core (real instr / value_type names) and a stack-machine wexec.

  • R1 (RealWasm.v grown with locals + comparisons; RealCompile.v) — the first real ⟦compile p⟧ = ⟦p⟧. The source is the resolved (de Bruijn-level) int/bool/let/binary core of lib/ast.ml; eval is the reference semantics; compile lowers let to LocalSet into a pre-sized locals array. compile_correct carries an env↔locals agreement invariant with fresh-slot allocation and low-slot preservation through the induction. This retires K1/K1Let on real objects.

  • R2 (RealWasm.v grown with structured control IfElse; RealCompile.v grown with RIf) — conditionals. Because instr now nests list instr, the structural wexec is rejected by the guard checker, so wexec is now fuel-indexed; the clean wexec_seq is replaced by wexec_mono (more fuel never loses a result) + wexec_app_some (additive sequencing). The preservation theorem is stated existentially in the fuel; the branch taken by if is run with monotonically-padded fuel.

The full plan — the rest of the ladder (R2-loops → R-mem → R-float → R-str → R-call → R-wrap → R-eff), the Coq module structure, and the strategy for each hard part (backward jumps Loop/Br reuse the fuel device; linear memory, floats, the elaboration nodes, effects) — is formal/REAL-LIFT.adoc.

Record rows (P-11)

Rows.v is the seed for AffineScript’s row-polymorphic records. It extends the P2_Stlc.v STLC with extensible records — {} (empty), { l = e | e' } (extension), e.l (selection), and e \ l (restriction) — typed over a row carrying a lacks side-condition (no duplicate labels), and proves full progress + preservation. The soundness payload is canonical-forms for records: a well-typed selection of a present label never gets stuck. Record terms use explicit rempty/rext constructors (so the standard term induction covers fields) while record types are list (id * ty) (so the row helpers are ordinary list fixpoints — no mutual-induction scheme); this is the Software-Foundations Records.v idiom, kept funext-free like P2_Stlc.v. This is Wave W0 (monomorphic rows); row variables + the lacks judgment (true row polymorphism, e.g. {name : String | ρ} → String) are the W1 increment, deferred exactly as P2_Stlc.v defers the QTT/affine layer.

Scope (honest)

These are Wave-0/1 seeds, not the discharged obligations. The fragments are deliberately small; the full theorems need the real AffineScript AST and the real typed-WASM operational semantics, expanded the way solo-core’s Duet/Ensemble tracks expand Solo. That expansion has begun — see the real lift above (RealWasm.v / RealCompile.v, R0→R2) and the plan in formal/REAL-LIFT.adoc. Tracked in docs/PROOF-NEEDS.adoc and #513.

Checking

just -f formal/justfile check
# or, by hand (F-1 Requires K-1, so compile K-1 first):
cd formal
for f in K1_CodegenPreservation K1Let_CodegenPreservation \
         F1_TransformerPreservation Siblings_Stated; do
  coqc -Q . ASFormal "$f.v"
done

Requires Coq 8.18+ (apt install coq, or opam coq). The check recipe fails if any proof depends on an axiom or Admitted.