diff --git a/.github/workflows/coq-proofs.yml b/.github/workflows/coq-proofs.yml new file mode 100644 index 0000000..c3ed939 --- /dev/null +++ b/.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" diff --git a/docs/proofs/verification/.gitignore b/docs/proofs/verification/.gitignore new file mode 100644 index 0000000..044f776 --- /dev/null +++ b/docs/proofs/verification/.gitignore @@ -0,0 +1,7 @@ +# Coq build artifacts +*.vo +*.vos +*.vok +*.glob +.*.aux +.lia.cache diff --git a/docs/proofs/verification/AUDIT.md b/docs/proofs/verification/AUDIT.md index 70e0ede..8ff6b13 100644 --- a/docs/proofs/verification/AUDIT.md +++ b/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. diff --git a/docs/proofs/verification/WokeLang.v b/docs/proofs/verification/WokeLang.v index d33c010..af1ad60 100644 --- a/docs/proofs/verification/WokeLang.v +++ b/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) *)