// SPDX-License-Identifier: CC-BY-SA-4.0
// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
= AffineScript `formal/` — Mechanized Metatheory (Coq/Rocq)
Jonathan D.A. Jewell
:toc: left
:toclevels: 2

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`).

[NOTE]
.CI gates on 8.20.1, not 8.18
====
Since 2026-07-29 these proofs are gated in CI by
`.github/workflows/coq-proof-gate.yml`, whose pinned container provides
**Coq 8.20.1**. The whole corpus was verified to check clean on 8.20.1; the
only friction is a deprecation warning (`app_length` -> `length_app`, deprecated
since 8.20) from `RealCompile.v`, `RealLoop.v` and `RealMem.v`. No errors.

Reconciling this documented 8.18 pin with the 8.20 gating version is
outstanding. See `docs/ci/COQ-PROOF-GATE.adoc`.
====

[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

[cols="2,2,3"]
|===
| 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

| `RealLoop.v`
| **Real lift R2-loops** — `Block`/`Loop`/`Br`/`BrIf` + a branch-aware executor
  `cexec`; source `while`/`seq`/`set` statements; `compile_stmt_correct` (a
  terminating `while`'s `Block[Loop[…]]` lowering simulates `run_stmt`,
  empty-stack unit tail — settles #601)
| **mechanized**, axiom-free

| `RealMem.v`
| **Real lift R-mem (kernel)** — `I32Load`/`I32Store`; word-addressed memory +
  structural executor `mexec`; bump allocator; store→load and 2-cell
  tuple build+project round-trips (`field i at base+i`)
| **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:

[source,coq]
----
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 → R-mem)

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. Five rungs are down (R-mem in kernel form):

* **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.
* **R2-loops** (`RealWasm.v` grown with `Block`/`Loop`/`Br`/`BrIf`; `RealLoop.v`)
  — backward jumps. The R2 `wexec` can't express "branched to label k", so a
  branch-aware executor `cexec` (outcome `ONormal`/`OBranch k`/`OTrap`) handles
  the structured control: a `Loop` consumed by `Br 0` re-enters with decremented
  fuel, staying a structural `Fixpoint`. The R2 expression compiler is re-proved
  into `cexec` (`cexec_compile`), and a source `while`/`seq`/`set` statement
  language is lowered to `Block[Loop[…;BrIf 1;…;Br 0]]`; `compile_stmt_correct`
  proves a terminating `while` simulates the reference `run_stmt`, ending with an
  **empty value stack** — settling the #601 value-returning-tail question
  (statement tail = unit) concretely.
* **R-mem** (kernel) (`RealWasm.v` grown with `I32Load`/`I32Store`; `RealMem.v`)
  — linear memory. A **word-addressed** heap (`mem := list Z`, cell = i32) with a
  *structural* executor `mexec` (memory ops are straight-line, so no fuel) +
  `mexec_app`, a bump allocator (`base = current size`), and the heap round-trips:
  store→load (`mexec_store_then_load`) and a 2-cell tuple build+project
  (`mexec_pair_build_proj` — `field i at base+i`, both projections), all reusing
  `set_nth`'s get-after-set. Remaining R-mem: runtime `memory.grow`, byte layout,
  control-bearing fields (fuse `mexec` with `cexec`), and the full source
  tuple/array/record compile-correctness.

The full plan — the rest of the ladder (finish R-mem → R-float → R-str → R-call →
R-wrap → R-eff), the Coq module structure, and the strategy for each hard part
(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

[source,sh]
----
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`.
