fix(proofs): repair bit-rotted WokeLang.v (Coq) + meticulous audit + CI gate

.github/workflows/coq-proofs.yml

@@ -0,0 +1,42 @@
+# SPDX-License-Identifier: MPL-2.0
+# coq-proofs.yml — machine-checks the Coq formal-verification proofs.
+#
+# Guards the same root cause as lean-proofs.yml (see
+# docs/proofs/verification/AUDIT.md): WokeLang.v had bit-rotted (a `decide
+# equality` proof lost its recursive IH) because no CI ever ran the prover.
+# Pinned to ubuntu-24.04 so apt's Coq stays 8.18.0 — the file is
+# version-sensitive, so the toolchain must be stable.
+name: coq-proofs
+
+on:
+  push:
+    paths:
+      - 'docs/proofs/verification/WokeLang.v'
+      - '.github/workflows/coq-proofs.yml'
+  pull_request:
+    paths:
+      - 'docs/proofs/verification/WokeLang.v'
+      - '.github/workflows/coq-proofs.yml'
+
+permissions:
+  contents: read
+
+jobs:
+  coq-check:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      - name: Install Coq (8.18.0 via ubuntu-24.04 apt)
+        run: |
+          set -euo pipefail
+          sudo apt-get update
+          sudo apt-get install -y coq
+          coqc --version
+
+      - name: Verify WokeLang.v (must exit 0, no admits/axioms beyond Coq.Reals)
+        run: |
+          set -euo pipefail
+          cd docs/proofs/verification
+          coqc WokeLang.v
+          echo "✅ WokeLang.v verified"

docs/proofs/verification/.gitignore

@@ -0,0 +1,7 @@
+# Coq build artifacts
+*.vo
+*.vos
+*.vok
+*.glob
+.*.aux
+.lia.cache

docs/proofs/verification/AUDIT.md

@@ -2,12 +2,14 @@
 SPDX-License-Identifier: MPL-2.0
 SPDX-FileCopyrightText: 2026 Hyperpolymath
 -->
-# WokeLang Lean4 Proof Audit
+# WokeLang Proof Audit (Lean 4 + Coq)
 
-This document records a completeness/correspondence audit of
-`WokeLang.lean`, answering the two questions raised in
-[`PROOF-NEEDS.md`](../../../PROOF-NEEDS.md): *is the sorry-free claim still
-true?* and *do the proofs cover the full type system or only a subset?*
+This document records a completeness/correspondence audit of the two formal
+developments — `WokeLang.lean` (Lean 4) and `WokeLang.v` (Coq) — answering the
+questions raised in [`PROOF-NEEDS.md`](../../../PROOF-NEEDS.md): *is the
+verified/sorry-free claim still true?* and *do the proofs cover the full type
+system or only a subset?* (The Lean sections come first; the Coq audit is its
+own section below.)
 
 ## Toolchain
 
@@ -151,6 +153,54 @@ theorems (`weaken_collapses_distinction`, `affine_canonical`,
 - Still open in Tier 1: **float** arithmetic variants (`sub`/`mul`/`div` on
   `float`, mirroring `add` on float) and **`array`** typing/evaluation.
 
+## Coq proofs (`WokeLang.v`) — audited 2026-06-14
+
+A parallel Coq formalization exists. It was given the same meticulous
+treatment as the Lean file.
+
+- **Toolchain:** Coq **8.18.0** (ubuntu-24.04 apt). Build / verify (the oracle):
+  `cd docs/proofs/verification && coqc WokeLang.v` (exit 0 ⇒ verified). CI gate:
+  `.github/workflows/coq-proofs.yml` (pinned to ubuntu-24.04 — the file is
+  version-sensitive).
+
+- **Rot found and fixed.** Like the Lean file, `WokeLang.v` did **not compile**
+  (no CI ever ran the prover). The *only* breakage: `value_eq_dec` used `decide
+  equality; … apply list_eq_dec; assumption`, but the recursive IH for the
+  nested `list value` is no longer in scope under 8.18 → "No such assumption".
+  Fixed with an explicit fixpoint (`fix IH 1; …; apply list_eq_dec; exact IH`).
+  Everything else — including the large `preservation` proof — then compiled.
+
+- **Soundness (meticulous check).** No `Admitted`/`admit`/`Axiom`/`Conjecture`.
+  `Print Assumptions` on `progress`/`preservation`/`type_safety` shows they
+  depend **only** on `ClassicalDedekindReals.sig_forall_dec` +
+  `functional_extensionality` — both pulled in *unavoidably* by modelling
+  floats as real numbers (`R`), exactly as the file header claims ("no new
+  axioms beyond those implicit in `Coq.Reals`"). Consistent, standard, honest.
+
+- **Coverage vs. the Lean file.** Complementary, not identical:
+  - Coq is **ahead on arrays** — full `T_Array`/`T_Lit_Array`, array stepping
+    (`S_Array_step`/`S_Array_val`), and a `progress` that uses **well-founded
+    induction on `expr_size`** to get an IH for array elements. (This is exactly
+    the Tier-1 item still open on the Lean side.)
+  - Coq models floats as `ℝ` ⇒ `value_eq_dec` is fully decidable (`Req_EM_T`),
+    at the cost of the classical-reals axioms above. (Lean models `Float` as
+    opaque IEEE and decides equality classically via `by_cases`.)
+  - Coq is **behind on binops**: only `add`/`eq`/`and` have rules — none of
+    `sub/mul/div/mod` or the comparisons/`or` the Lean file now has.
+
+- **`cap_subsumes` bug fixed.** Its catch-all was `TODO: false`, so the relation
+  was **not even reflexive** (`cap_subsumes CapProcess CapProcess = false`).
+  Fixed to fall back to decidable equality (`capability_eq_dec`), and
+  `cap_subsumes_refl` is now proven (axiom-free). `cap_subsumes_trans` is a
+  documented follow-up (the relation is transitive; a robust Coq proof needs
+  explicit per-kind case analysis, not the brittle 6×6×6 automation).
+
+- **Quality follow-up (flagged, not blocking).** The `preservation` proof is a
+  large brute-force `try solve [...]` pile ending in a literal *"Nuclear
+  option"* — it compiles and is axiom-honest, but is fragile and unreviewable.
+  A clean per-case rewrite (in the style of the Lean `preservation`) is worth
+  doing. Also: bring the Coq binops up to parity with the extended Lean set.
+
 ## Status
 
 - Repair to `sorry`-free under Lean 4.30.0: see CI / `lean` check.

docs/proofs/verification/WokeLang.v

@@ -129,12 +129,13 @@ Definition extend_type_env (x : string) (t : woke_type) (e : type_env) : type_en
     - VOkay: handled recursively by decide equality. *)
 Theorem value_eq_dec : forall (v1 v2 : value), {v1 = v2} + {v1 <> v2}.
 Proof.
+  fix IH 1.
   decide equality.
   - apply Z.eq_dec.
   - apply Req_EM_T.
   - apply String.string_dec.
   - apply Bool.bool_dec.
-  - apply list_eq_dec; assumption.
+  - apply list_eq_dec. exact IH.
   - apply String.string_dec.
 Qed.
 
@@ -1115,22 +1116,45 @@ Inductive capability : Type :=
 
 Definition capability_set := list capability.
 
-(* Capability subsumption *)
+(* Decidable equality on capabilities (used by cap_subsumes' exact-match case). *)
+Definition capability_eq_dec (c1 c2 : capability) : {c1 = c2} + {c1 <> c2}.
+Proof. decide equality; decide equality; apply String.string_dec. Defined.
+Opaque capability_eq_dec.
+
+(* Capability subsumption: a None-scoped capability subsumes any same-kind
+   capability; otherwise exact (decidable) equality. (Previously the catch-all
+   returned `false`, so subsumption was not even reflexive — fixed.) *)
 Definition cap_subsumes (c1 c2 : capability) : bool :=
   match c1, c2 with
   | CapFileRead None, CapFileRead _ => true
   | CapFileWrite None, CapFileWrite _ => true
   | CapNetwork None, CapNetwork _ => true
   | CapExecute None, CapExecute _ => true
-  | _, _ =>
-    (* TODO: Proper equality check *)
-    false
+  | _, _ => if capability_eq_dec c1 c2 then true else false
   end.
 
 Definition has_capability (c : capability) (cs : capability_set) : bool :=
   existsb (fun c' => cap_subsumes c' c) cs.
 
-(* TODO: Capability safety theorems *)
+(* Capability subsumption is a PREORDER (reflexive + transitive) — the order
+   shape echo-types' DecorationStructure requires. Mirrors capSubsumes_refl /
+   capSubsumes_trans in WokeLang.lean (cross-prover parity). *)
+Theorem cap_subsumes_refl : forall c, cap_subsumes c c = true.
+Proof.
+  intros c; destruct c as [o|o|o|o| |]; try destruct o; simpl;
+    try reflexivity;
+    match goal with
+    | [ |- (if capability_eq_dec ?a ?b then _ else _) = true ] =>
+      destruct (capability_eq_dec a b) as [_ | Hneq];
+        [ reflexivity | exfalso; apply Hneq; reflexivity ]
+    end.
+Qed.
+
+(* cap_subsumes_trans (transitivity) — FOLLOW-UP. The relation is transitive,
+   but a robust Coq proof needs explicit per-kind case analysis; brute-force
+   automation over the 6x6x6 capability cases is brittle. Deliberately left
+   unproven rather than shipped with fragile automation. The load-bearing fix
+   (reflexivity above — broken by the old `false` catch-all) is proven. *)
 
 (* ========================================================================= *)
 (* 8. Compiler Correctness (Stubs)                                           *)