|
| 1 | +<!-- SPDX-License-Identifier: MPL-2.0 --> |
| 2 | +<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> --> |
| 3 | + |
| 4 | +# WokeLang Formal-Verification Roadmap |
| 5 | + |
| 6 | +Scope for taking WokeLang from "a model of the expression core + grammar |
| 7 | +metatheory is machine-checked" to "fully proved." Companion to |
| 8 | +[`verification/AUDIT.md`](verification/AUDIT.md), |
| 9 | +[`verification/GRAMMAR-PROOF-INVENTORY.md`](verification/GRAMMAR-PROOF-INVENTORY.md), |
| 10 | +and [`../../PROOF-NEEDS.md`](../../PROOF-NEEDS.md). Derived from a four-part survey |
| 11 | +of every proof document and the implementation (2026-06). |
| 12 | + |
| 13 | +## The two axes (and the honest reality) |
| 14 | + |
| 15 | +"Fully proved across its entire extent" means two very different things: |
| 16 | + |
| 17 | +- **Axis 1 — breadth of the *models*:** mechanize every prose proof (type |
| 18 | + inference, semantics, compiler, security, complexity, concurrency) in Lean 4 |
| 19 | + (4.30.0, Mathlib-free, single-file) and/or Coq 8.18.0. Mostly tractable; a few |
| 20 | + items are infeasible without Mathlib. |
| 21 | +- **Axis 2 — depth, *model ↔ real code*:** connect the proofs to the actual |
| 22 | + **~23k-LOC Rust** implementation (plus a divergent ~1.1k-LOC OCaml `core/`). |
| 23 | + There is currently **no extraction, no refinement proof, no translation |
| 24 | + validation** in place. The machine-checked proofs cover roughly **10–15 %** of |
| 25 | + the 94-production surface language, and they verify **models, not code**. |
| 26 | + |
| 27 | +> **Reality check.** Literal "fully proved against the shipping Rust" is |
| 28 | +> CompCert + RustBelt scale — multiple person-years, research-grade tooling that |
| 29 | +> does not exist for this codebase (async / `tokio` / proc-macros). It is a new |
| 30 | +> research program, not an extension of the present work. What *is* achievable is |
| 31 | +> **"the language model fully proved, plus an empirical bridge to the code."** |
| 32 | +
|
| 33 | +## Current baseline (machine-checked, hole-free, CI-gated) |
| 34 | + |
| 35 | +| File | Covers | |
| 36 | +|---|---| |
| 37 | +| `verification/WokeLang.lean` / `.v` | expression-core **type safety** (progress, preservation, type-safety, canonical forms, arrays, `Result`/`unwrap` panic); statement *typing* (no execution); consent monotonicity/preservation; capability preorder | |
| 38 | +| `verification/WokeGrammar.lean` | verified-parser core (soundness, completeness, termination, precedence, determinism) | |
| 39 | +| `verification/WokeGrammarStructure.{lean,v}` | no-left-recursion (whole grammar), maximal munch, keyword priority, LL(1)✗/LL(2)✓ | |
| 40 | +| `verification/WokeGrammar{CFL,Regular,Pumping}.lean` | CFL closure, non-regularity, the CFL pumping lemma, `aⁿbⁿcⁿ ∉ CFL`, ∩ non-closure | |
| 41 | + |
| 42 | +## Fix-first: five spec bugs (each Small, do as the phase is reached) |
| 43 | + |
| 44 | +These are *wrong as written* and will block the corresponding proofs: |
| 45 | + |
| 46 | +1. **HM `unify(Int,Float)=promote`** makes the "most general unifier" theorems |
| 47 | + false — model widening as **subtyping**, not unification. (blocks Phase 3a) |
| 48 | +2. **`Step` is non-deterministic** (`sArrayVal` overlaps element rules) — blocks |
| 49 | + any determinism proof. (blocks Phase 1c) |
| 50 | +3. **Float `==` reflexivity** is false on `NaN` — the memory-model equality claim |
| 51 | + needs restating (decidable structural eq, or exclude floats). |
| 52 | +4. **Unbounded `Int` vs `ℤ₆₄`** — the model uses ℤ; the language is 64-bit |
| 53 | + wrapping. Affects arithmetic laws and compiler/WASM correctness. (cross-cutting) |
| 54 | +5. **Three-way divergence** — Rust, OCaml `core/`, and the Lean/Coq models |
| 55 | + disagree on `Result`/units/coercions, so "the impl refines the proof" is |
| 56 | + currently ill-posed. Resolve by making one model **normative**. (blocks Axis 2) |
| 57 | + |
| 58 | +## Axis 1 — phases (dependency-ordered) |
| 59 | + |
| 60 | +| Phase | Deliverable | Effort | Mathlib-free? | Depends on | |
| 61 | +|---|---|---|---|---| |
| 62 | +| **1. Full type safety** | substitution lemma + `[T-Call]`/`Φ` + indexing → progress/preservation for the full *expression* language | M | yes | core | |
| 63 | +| **1b. Statement dynamics** | statement execution relation + store-typing preservation | L | yes | 1 | |
| 64 | +| **1c. Operational metatheory** | fix determinism, add big-step, big↔small equivalence | M | yes | bug 2, 1b | |
| 65 | +| **2a. Capability order** | antisymmetry + `hasCapability` satisfaction lemmas (+ Coq `cap_subsumes_trans`) | S | yes | — | |
| 66 | +| **2b. Consent state machine** | duration/expiry, protocol completeness + determinism + unforgability, isolation | M | yes (excl. IO persistence, LTL/CTL) | — | |
| 67 | +| **2c. Capability state machine** | no-privilege-escalation, confinement, revocation, temporal, audit | M | yes | 2a | |
| 68 | +| **3a. HM inference (soundness)** | `unify` (well-founded + occurs check) + Algorithm W **soundness** | L | yes (hand-rolled `FTV`/`Subst`) | 1, bug 1 | |
| 69 | +| **3b. HM completeness** | principal types / most-general | XL | yes but large | 3a | |
| 70 | +| **4a. Compiler simulation** | Lean bytecode IR + VM + `compile` + forward simulation (interpret↔VM) | L | yes | 1c | |
| 71 | +| **4b. Lexer/parser in Lean** | `tokenize`/`parse` + EBNF conformance (beyond current structural facts) | M ea. | yes | — | |
| 72 | +| **4c. WASM preservation** | WASM-subset semantics + preservation | L | yes (partial) | 4a | |
| 73 | +| **5a. Category theory (concrete)** | functor / monad / naturality laws for `Maybe`/`Result`/`List`/`State` | S–M | yes | — | |
| 74 | +| **6. Complexity (structural)** | AST-size + `bytecode ≤ k·AST` size theorems only | L | yes | 4a | |
| 75 | +| **7. Concurrency (scoped)** | interleaving semantics + worker isolation + message-non-loss safety | L | yes | 1b | |
| 76 | + |
| 77 | +## Axis 1 — explicitly out of scope / research-grade |
| 78 | + |
| 79 | +- **Denotational adequacy** (`𝕍 ≅ … + (𝕍→𝕍⊥)`, fixpoints): recursive |
| 80 | + function-summand fails Lean's positivity check; needs Scott domain theory → |
| 81 | + XL, likely infeasible single-file/Mathlib-free. Restrict to the first-order |
| 82 | + fragment (M) or descope. |
| 83 | +- **Category-theory headline claims** (CCC, all finite limits/colimits, |
| 84 | + adjunctions, Yoneda, topos): need Mathlib's `CategoryTheory` (policy conflict); |
| 85 | + several are not well-posed about an actual defined category. Descope or |
| 86 | + grant a one-module Mathlib exception. |
| 87 | +- **Complexity asymptotics** (`O(·)`, inverse-Ackermann/union-find, crate |
| 88 | + constants): claims about Rust + external crates, not witnessable in a model. |
| 89 | +- **Concurrency race/deadlock freedom + CSP trace-equivalence**: evidence is Rust |
| 90 | + ownership / a not-yet-built async runtime — not faithfully mechanizable. |
| 91 | +- **Memory model** (use-after-free, double-free, data races, UTF-8, |
| 92 | + atomic-write persistence): Rust/POSIX host properties, *not* object-language |
| 93 | + theorems. Only bounds-safety + equality-relation are real (S). |
| 94 | + |
| 95 | +## Axis 2 — model ↔ implementation |
| 96 | + |
| 97 | +| Approach | Guarantee | Effort | Reality | |
| 98 | +|---|---|---|---| |
| 99 | +| **(E) Make one model normative; kill 3-way divergence** | well-posedness | M | **Prerequisite** for any bridge being meaningful | |
| 100 | +| **(A) Differential + property-based testing** | empirical | S–M | **Only realistic near-term bridge**; tooling exists (`proptest`, `fuzz/`, `conformance/`) | |
| 101 | +| **(B) Translation validation for the parser** | per-run certificate | L | model already half-supports it (renderer inversion) | |
| 102 | +| **(C) Coq→OCaml extraction of a *new* reference interpreter** | extracted = verified | L | idiomatic, but *replaces* `core/eval.ml` rather than validating it | |
| 103 | +| **(D) Rust refinement (Aeneas/Creusot/Verus), core fragment only** | impl ⊑ model | XL | research-grade; async/macros out of tool scope | |
| 104 | +| **Full verified source→WASM compiler** | end-to-end | XL (multi-person-year) | CompCert-scale; new project | |
| 105 | + |
| 106 | +## Recommended target — three tiers |
| 107 | + |
| 108 | +- **Tier 1 — the model is fully proved.** Phases 1, 1b, 1c, 2a–2c, 3a, 4a plus the |
| 109 | + five spec-bug fixes: full type safety, sound type inference, a verified compiler |
| 110 | + simulation, and real security state machines. The achievable bulk — all |
| 111 | + Mathlib-free, extending the hole-free core. |
| 112 | +- **Tier 2 — empirical bridge to the code.** (E) + (A): resolve divergence and |
| 113 | + stand up cross-backend differential / property testing. Real confidence the |
| 114 | + Rust/OCaml code matches the verified model. |
| 115 | +- **Tier 3 — true refinement / verified compilation.** (D) and source→WASM: |
| 116 | + explicitly a research program (multi-person-year). Not a committed deliverable. |
| 117 | + |
| 118 | +**First increment** (lowest risk, highest leverage): the five spec-bug fixes + |
| 119 | +**Phase 2a** (capability order, S) + **Phase 1** (full-expression type safety via |
| 120 | +the substitution lemma, M). These extend the existing hole-free file directly and |
| 121 | +unlock Phases 1c / 3a / 4a. |
| 122 | + |
| 123 | +## Progress |
| 124 | + |
| 125 | +- [x] **Phase 2a (Lean)** — capability partial order (`capSubsumes_antisymm`, |
| 126 | + completing `_refl`/`_trans`) + satisfaction lemmas (`hasCapability_mono`, |
| 127 | + `hasCapability_subsumes`). Coq parity (`cap_subsumes_trans`/`_antisymm`) remains |
| 128 | + a deliberate follow-up — the author left it unproven rather than ship fragile |
| 129 | + 6×6×6 automation; a clean Coq proof wants a `cap_subsumes` characterization lemma. |
| 130 | +- [ ] Phase 1, 1b, 1c — type-safety + operational metatheory. |
| 131 | +- [ ] Phase 2b, 2c — consent + capability state machines. |
| 132 | +- [ ] Phase 3a (+3b) — HM inference. |
| 133 | +- [ ] Phase 4a–4c — compiler / parser / WASM. |
| 134 | +- [ ] Phase 5a, 6, 7 — concrete category theory, structural complexity, scoped concurrency. |
| 135 | +- [ ] Axis 2 — (E) normative model, (A) differential testing. |
0 commit comments