feat(formal): stand up Coq formal/ track + mechanize the K-1 Wave-0 seed

.claude/CLAUDE.md

@@ -139,6 +139,27 @@ The "no Node.js / no Bun" rules in the language policy table have two approved e
 
 Browsers and Cloudflare Workers are NOT supported and never will be (the shim's purpose — fetch, save to disk, exec a native binary — cannot be done in a sandboxed JS runtime). The JSR runtime-compatibility checkboxes for this package should be: Deno ✅, Bun ✅, Node ✅, Workers ❌, Browsers ❌.
 
+### Formal-methods Coq `.v` (NOT V-lang)
+
+The `formal/` directory holds **Coq/Rocq 8.18** proof scripts — mechanized
+metatheory for the obligations in `docs/PROOF-NEEDS.adoc` (Wave-0 seed: K-1
+codegen→typed-WASM preservation, `formal/K1_CodegenPreservation.v`). Coq uses
+the `.v` extension, **shared with Verilog and the estate-banned V-lang** (→
+Zig). Coq `.v` is **not** V-lang and is **not** a policy violation:
+
+- The estate vlang ban (`cicd_rules/vlang_detected`, matches `*.v`) carries an
+  estate-wide `path_allow_prefixes` carve-out for "Coq proof scripts"; V-lang's
+  `v.mod` manifest (`cicd_rules/vmod_detected`) does not exist for Coq.
+- `formal/*.v` is exempted explicitly in `.hypatia-ignore` so a future sweep
+  cannot conflate the two `.v`. Prover choice is Coq (typed-wasm / ephapax
+  interop, both Coq); solo-core's separate skeleton stays Idris2.
+- Load-bearing proofs here must be **complete**: no `Admitted`, no axioms
+  (`Print Assumptions` must report "Closed under the global context"),
+  paralleling the Agda "no postulates in load-bearing tracks" rule;
+  `formal/justfile`'s `check` recipe enforces it.
+
+Do not "migrate", rewrite, or delete `formal/*.v` as if it were V-lang.
+
 ### Package Management
 
 - **Primary**: Guix (guix.scm)

.hypatia-ignore

@@ -32,3 +32,16 @@ cicd_rules/banned_language_file:tools/res-to-affine/test/fixtures/partial1.res
 cicd_rules/banned_language_file:tools/res-to-affine/test/fixtures/phase3.res
 cicd_rules/banned_language_file:tools/res-to-affine/test/fixtures/phase3b.res
 cicd_rules/banned_language_file:tools/res-to-affine/test/fixtures/phase3c.res
+#
+# ─── Coq/Rocq proof scripts (.v is NOT V-lang) ──────────────────────
+#
+# `.v` is shared by Coq, Verilog and the estate-banned V-lang (→ Zig).
+# The vlang ban is detected on `*.v` via cicd_rules/vlang_detected, with an
+# estate-wide path_allow_prefixes carve-out for "Coq proof scripts". The
+# AffineScript `formal/` track (obligation K-1, see docs/PROOF-NEEDS.adoc)
+# is Coq 8.18 — not V-lang, not Verilog. Exempt it explicitly so a future
+# sweep cannot mis-flag it. (Coq ships no `v.mod`, so vmod_detected never
+# fires.) Both rule names are listed for robustness; the non-matching one is
+# an inert no-op under the scanner's `grep -qxF` whole-line match.
+cicd_rules/vlang_detected:formal/K1_CodegenPreservation.v
+cicd_rules/banned_language_file:formal/K1_CodegenPreservation.v

docs/PROOF-NEEDS.adoc

@@ -67,8 +67,10 @@ than the prose corpus suggests:
   *templates* ("Replace with your project's domain-specific proofs"); the Coq
   `TypeSafety.v` is example lemmas about list length, not AffineScript. Not
   core-metatheory.
-* **`formal/`** — the directory #513 names as the mechanized-proof target
-  **does not exist**.
+* **`formal/`** — the directory #513 names as the mechanized-proof target now
+  **exists** (Coq/Rocq 8.18). It holds the Wave-0 **K-1 seed**
+  (`formal/K1_CodegenPreservation.v`) — a complete, axiom-free
+  codegen-preservation proof for a minimal nat/bool fragment (see <<outstanding>>).
 * **Research tracks** (not core soundness): `docs/academic/tropical-session-types/`
   (Lean), `proposals/echo-types/EchoEncodingFaithfulness.agda`,
   `proposals/idaptik/migrated/**/*Boundary.agda` (echo-types loss-with-residue,
@@ -178,8 +180,11 @@ The work in flight changes which obligations are *load-bearing* and which are
   `⟦compile(p)⟧_wasm = ⟦p⟧_source` for the operational semantics. This is the
   single obligation every *face* and every *aLib conformer* ultimately rests on:
   prove the backend preserves meaning once, and front-end face theorems
-  (<<faces>>) compose into end-to-end correctness. Rigour `XL`. Status `prose`
-  (`operational-semantics.md` / `denotational-semantics.md` are the inputs).
+  (<<faces>>) compose into end-to-end correctness. Rigour `XL`. Status `partial`
+  (was `prose`): a Wave-0 mechanized seed — `formal/K1_CodegenPreservation.v`
+  (Coq, no axioms) — proves preservation for a minimal nat/bool · add/and
+  fragment compiled to a stack machine; the real AffineScript AST + real
+  typed-WASM operational semantics remain the open obligation.
 * **K-2 — Effect-soundness is *blocked*, not merely unproven.** P-6 cannot be
   honestly *stated against the current backend* because #555 drops handler arms
   on three of the codegen targets. The obligation must be split: (a) prove
@@ -311,10 +316,11 @@ F-1 (full transformer preservation) is non-trivial rather than a formality.
 |===
 | Wave | Items | Gates
 
-| 0 (now)
-| Stand up `formal/` (the #513 target dir). *State* — without proving — P-2,
-  P-3 (rejecting #554), F-1, F-3, F-4 as signatures/holes, mirroring the
-  solo-core skeleton style. Cross-link `CAPABILITY-MATRIX.adoc` rows (K-4).
+| 0
+| *In progress.* DONE: `formal/` stood up (Coq/Rocq); **K-1 seed mechanized**
+  (`K1_CodegenPreservation.v`, axiom-free). NEXT: *state* P-2, P-3 (rejecting
+  #554), F-1, F-3, F-4 as signatures, mirroring solo-core; cross-link
+  `CAPABILITY-MATRIX.adoc` rows (K-4).
 | —
 
 | 1

formal/.gitignore

@@ -0,0 +1,9 @@
+# Coq/Rocq build artifacts
+*.vo
+*.vok
+*.vos
+*.glob
+.*.aux
+.lia.cache
+.nia.cache
+.coqdeps.d

formal/K1_CodegenPreservation.v

@@ -0,0 +1,160 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+
+(*
+   K1_CodegenPreservation.v
+   ════════════════════════
+   Wave-0 seed of obligation **K-1** from docs/PROOF-NEEDS.adoc:
+   "codegen → typed-WASM semantic-preservation" — the keystone every face
+   (via F-1) and every aLib conformer ultimately composes through.
+
+   This file is a Coq/Rocq PROOF SCRIPT. It is NOT V-lang and NOT Verilog —
+   the `.v` extension is shared between Coq, Verilog and V-lang. The estate
+   language policy bans *V-lang* (→ Zig) and carves Coq proof scripts out of
+   the `cicd_rules/vlang_detected` rule via `path_allow_prefixes`; this repo
+   makes that explicit for `formal/` in `.hypatia-ignore`.
+
+   SCOPE (honest). This discharges K-1 for a deliberately minimal fragment:
+   a two-type (nat, bool) expression language with `add` and `and`, compiled
+   to a little stack machine that stands in for typed-WASM. The full
+   obligation — the real AffineScript AST and the real typed-WASM operational
+   semantics — is future work that *expands* this core, exactly the way
+   solo-core's Duet/Ensemble tracks expand the Solo fragment. What is proven
+   here is the genuine article for the fragment: a complete, machine-checked
+   compiler-correctness theorem with NO `Admitted`, NO `Axiom`, NO `postulate`
+   (estate rule: load-bearing proofs must be constructive and complete).
+
+   Check it:  coqc formal/K1_CodegenPreservation.v   (or: just -f formal/justfile check)
+*)
+
+Require Import List.
+Import ListNotations.
+
+(* ══════════════════ Source: a minimal AffineScript fragment ══════════════ *)
+
+Inductive sval : Type :=
+| VNat  (n : nat)
+| VBool (b : bool).
+
+Inductive sexp : Type :=
+| SNat  (n : nat)
+| SBool (b : bool)
+| SAdd  (e1 e2 : sexp)
+| SAnd  (e1 e2 : sexp).
+
+(* Big-step source evaluator. Partial: `add` on bools (or `and` on nats) is
+   stuck (None), so `seval e = Some v` is a real, non-trivial hypothesis. *)
+Fixpoint seval (e : sexp) : option sval :=
+  match e with
+  | SNat n  => Some (VNat n)
+  | SBool b => Some (VBool b)
+  | SAdd e1 e2 =>
+      match seval e1, seval e2 with
+      | Some (VNat a), Some (VNat b) => Some (VNat (a + b))
+      | _, _ => None
+      end
+  | SAnd e1 e2 =>
+      match seval e1, seval e2 with
+      | Some (VBool a), Some (VBool b) => Some (VBool (andb a b))
+      | _, _ => None
+      end
+  end.
+
+(* ══════════════ Target: a minimal typed-WASM-style stack machine ═════════ *)
+
+Inductive wval : Type :=
+| WNat  (n : nat)
+| WBool (b : bool).
+
+Inductive instr : Type :=
+| IPushN (n : nat)
+| IPushB (b : bool)
+| IAdd
+| IAnd.
+
+Definition code  := list instr.
+Definition stack := list wval.
+
+(* One instruction over the stack. None = trap (ill-typed operand stack),
+   the analogue of a typed-WASM validation failure. *)
+Definition wstep (i : instr) (s : stack) : option stack :=
+  match i, s with
+  | IPushN n, s                        => Some (WNat n :: s)
+  | IPushB b, s                        => Some (WBool b :: s)
+  | IAdd, WNat b :: WNat a :: s'       => Some (WNat (a + b) :: s')
+  | IAnd, WBool b :: WBool a :: s'     => Some (WBool (andb a b) :: s')
+  | _, _                               => None
+  end.
+
+Fixpoint wexec (c : code) (s : stack) : option stack :=
+  match c with
+  | []        => Some s
+  | i :: rest =>
+      match wstep i s with
+      | Some s' => wexec rest s'
+      | None    => None
+      end
+  end.
+
+(* ══════════════════════ Compiler: source → stack code ════════════════════ *)
+
+Fixpoint compile (e : sexp) : code :=
+  match e with
+  | SNat n     => [IPushN n]
+  | SBool b    => [IPushB b]
+  | SAdd e1 e2 => compile e1 ++ compile e2 ++ [IAdd]
+  | SAnd e1 e2 => compile e1 ++ compile e2 ++ [IAnd]
+  end.
+
+(* Value correspondence: a source value and the wasm value it denotes. *)
+Definition obs (v : sval) : wval :=
+  match v with
+  | VNat n  => WNat n
+  | VBool b => WBool b
+  end.
+
+(* ════════════════ The K-1 obligation, for this fragment ══════════════════ *)
+
+(* Codegen preserves meaning: if the source evaluates to v, then running the
+   compiled code on the empty operand stack yields exactly [obs v]. *)
+Definition K1_preservation : Prop :=
+  forall (e : sexp) (v : sval),
+    seval e = Some v ->
+    wexec (compile e) [] = Some [obs v].
+
+(* ───────────────────────── discharge (no Admitted) ──────────────────────── *)
+
+(* Correctness in continuation-passing form: running `compile e` followed by
+   any continuation `k`, from any stack `s`, is the same as running `k` with
+   the source value `v` pushed. Threading `k` is exactly the induction
+   strength needed (and avoids reasoning about a residual `match`). *)
+Lemma compile_correct : forall e v s k,
+  seval e = Some v ->
+  wexec (compile e ++ k) s = wexec k (obs v :: s).
+Proof.
+  induction e as [n | b | e1 IH1 e2 IH2 | e1 IH1 e2 IH2];
+    intros v s k Hev; simpl in Hev.
+  - (* SNat *)  inversion Hev; subst; reflexivity.
+  - (* SBool *) inversion Hev; subst; reflexivity.
+  - (* SAdd *)
+    destruct (seval e1) as [[a | ab] |]; try discriminate;
+    destruct (seval e2) as [[b | bb] |]; try discriminate;
+    inversion Hev; subst; clear Hev; simpl; rewrite <- !app_assoc;
+    rewrite (IH1 _ s _ eq_refl), (IH2 _ _ _ eq_refl); reflexivity.
+  - (* SAnd *)
+    destruct (seval e1) as [[na | a] |]; try discriminate;
+    destruct (seval e2) as [[nb | b] |]; try discriminate;
+    inversion Hev; subst; clear Hev; simpl; rewrite <- !app_assoc;
+    rewrite (IH1 _ s _ eq_refl), (IH2 _ _ _ eq_refl); reflexivity.
+Qed.
+
+Theorem k1_preservation_holds : K1_preservation.
+Proof.
+  unfold K1_preservation; intros e v Hev.
+  pose proof (compile_correct e v [] [] Hev) as H.
+  rewrite app_nil_r in H; simpl in H; exact H.
+Qed.
+
+(* `Print Assumptions` must report "Closed under the global context" — i.e.
+   the theorem rests on no axioms. CI greps for exactly that string. *)
+Print Assumptions k1_preservation_holds.

formal/README.adoc

@@ -0,0 +1,82 @@
+// SPDX-License-Identifier: MPL-2.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
+K-1 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
+
+[cols="2,2,3"]
+|===
+| File | Obligation | Status
+
+| `K1_CodegenPreservation.v`
+| **K-1** — codegen → typed-WASM semantic-preservation
+| **mechanized** for a minimal fragment (no `Admitted`, no axioms). The full
+  obligation remains open — see <<scope>>.
+|===
+
+== What `K1_CodegenPreservation.v` proves
+
+A complete, axiom-free compiler-correctness theorem for a minimal two-type
+AffineScript fragment (nat + bool, with `add` and `and`) compiled to a small
+stack machine that stands in for typed-WASM:
+
+[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 *)
+----
+
+i.e. whenever the source big-step evaluates to a value `v`, the compiled code
+run on the empty operand stack yields exactly the corresponding wasm value
+`[obs v]`. `Print Assumptions k1_preservation_holds` reports *Closed under the
+global context* — the proof rests on no axioms, honouring the estate rule that
+load-bearing proofs be constructive and complete (no `Admitted`, no
+`postulate`). This mirrors how `invariant-path/proofs/SameCube.agda` grounds
+F-2 with a real `--safe` proof rather than a stated hole.
+
+[#scope]
+== Scope (honest)
+
+This is the **Wave-0 seed** of K-1, not the discharged obligation. The fragment
+is deliberately tiny: no functions, binders, effects, ownership, traits, or
+the real instruction set. The full theorem needs the real AffineScript AST and
+the real typed-WASM operational semantics; expanding this core is the analogue
+of solo-core's Duet/Ensemble tracks expanding the Solo fragment. Tracked in
+`docs/PROOF-NEEDS.adoc` (K-1) and #513 (must-have 7).
+
+The faces twin **F-1** (transformer semantics-preservation) composes *on top
+of* K-1: prove the backend preserves meaning once here, and each
+`lib/<face>_face.ml` front-end transform need only preserve the canonical AST
+denotation for the same-cube result to follow end-to-end.
+
+== Checking
+
+[source,sh]
+----
+just -f formal/justfile check        # or:  cd formal && coqc K1_CodegenPreservation.v
+----
+
+Requires Coq 8.18+ (`apt install coq`, or opam `coq`). The `check` recipe fails
+if the proof ever starts depending on an axiom or `Admitted`.

formal/_CoqProject

@@ -0,0 +1,2 @@
+-Q . ASFormal
+K1_CodegenPreservation.v

formal/justfile

@@ -0,0 +1,17 @@
+# SPDX-License-Identifier: MPL-2.0
+# Coq/Rocq proof checks for the AffineScript `formal/` track.
+# (Mustfile/justfile per estate policy — no Makefiles.)
+
+# Type-check every proof and assert it closes under no axioms.
+check:
+    #!/usr/bin/env bash
+    set -euo pipefail
+    out="$(coqc K1_CodegenPreservation.v)"
+    printf '%s\n' "$out"
+    grep -q "Closed under the global context" <<<"$out" \
+      || { echo "::error:: K-1 proof depends on an axiom / Admitted"; exit 1; }
+    echo "OK: K-1 fragment mechanized, no axioms."
+
+# Remove Coq build artifacts.
+clean:
+    rm -f *.vo *.vok *.vos *.glob .*.aux .coqdeps.d

spec/FRG-PROFILE.adoc

@@ -167,7 +167,9 @@ For AffineScript, the following FRG tightening applies:
 
 == What is NOT yet met (honest gaps)
 
-* No formalisation directory.
+* `formal/` now exists *(met 2026-06-21)* — Coq/Rocq 8.18, holding the
+  mechanized K-1 codegen-preservation seed. (The *typing-judgment* encoding and
+  *type*-preservation/progress below remain open.)
 * No qualifying-prover encoding of the AST or typing judgment.
 * No preservation or progress statement.
 * (PROOF-NEEDS: met 2026-06-20.) `docs/PROOF-NEEDS.adoc` now enumerates the
@@ -178,7 +180,8 @@ For AffineScript, the following FRG tightening applies:
 
 == Path to next grade (D — preservation stated)
 
-* Create `formal/` directory.
+* [DONE 2026-06-21] Create `formal/` directory (Coq/Rocq; holds the K-1
+  codegen-preservation seed).
 * Encode AST in a qualifying prover (Rocq is the natural choice
   for compatibility with ephapax / typed-wasm).
 * Encode typing judgment.
@@ -219,6 +222,7 @@ dependent/refinement aspirations).
 
 | 2026-05-28 | E (pragmatic) | Initial FRG assessment. Strict reading = X (no formal/). Pragmatic E based on conformance corpus + operational typechecker + honest README status block. Recommend adopting strict X until qualifying-prover mechanisation lands.
 | 2026-06-20 | E (pragmatic) | `docs/PROOF-NEEDS.adoc` authored — open obligations enumerated (P-/F-/K- series), closing the "no PROOF-NEEDS" honest gap and completing path-to-D step 6. Grade unchanged (still no `formal/` prover encoding). Faces obligations F-1…F-7 newly catalogued.
+| 2026-06-21 | E (pragmatic) | `formal/` stood up (Coq/Rocq 8.18) with the mechanized **K-1 codegen-preservation seed** (`K1_CodegenPreservation.v`, axiom-free; `Print Assumptions` closed) — closes the "no formalisation directory" gap. Grade still E: D needs *type*-preservation/progress stated for the affine calculus itself (K-1 is codegen-preservation for a minimal fragment, a distinct theorem).
 |===
 
 == Review cycle