fix(proofs): repair WokeLang.lean to verify under Lean 4.30.0 + add CI gate#79
Merged
Merged
Conversation
…I gate
The Lean4 verification file claimed "sorry-free, verified" but had bit-rotted:
it did not compile under current Lean, because no CI ever ran the prover.
Restore sorry-free compilation under Lean 4.30.0 with NO weakened statements
(only proof bodies + 2 deriving clauses + 1 abbrev changed; every theorem
signature and inductive is byte-identical), and add the missing CI gate.
Root causes fixed:
- DecidableEq no longer derives for Value/WokeType (Float has none; nested
List blocks the handler) -> drop to `deriving Repr`; equality decisions use
classical `by_cases` (no instance needed).
- induction/cases on the concrete emptyTypeEnv/emptyEnv indices + Lean binder
arity drift; preservation made type-polymorphic via `induction hs
generalizing t`; `cases ... with | inr ⟨..⟩` -> `obtain`; type-mismatched
reduction siblings discharged with `nomatch`.
- BEq Permission: make Permission a reducible `abbrev`.
Verified: `lean docs/proofs/verification/WokeLang.lean` exits 0, zero
sorry/admit/axiom. progress, preservation, type_safety,
consent_{monotonicity,preservation} all machine-checked.
Adds:
- docs/proofs/verification/lean-toolchain (pin Lean v4.30.0)
- docs/proofs/verification/AUDIT.md (coverage/correspondence audit)
- .github/workflows/lean-proofs.yml (CI gate so it cannot rot again)
https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7
hyperpolymath
marked this pull request as ready for review
June 14, 2026 04:02
hyperpolymath
added a commit
that referenced
this pull request
Jun 14, 2026
…preorder (#80) ## Summary Builds on the now-verified `WokeLang.lean` (#79) by **extending the type-safety proofs** — Tier 1 (base operators) + Tier 3 (capability lattice) from `AUDIT.md`. Every addition is machine-checked under Lean 4.30.0 by the `lean-proofs` CI gate, **still sorry-free, no axioms**. ## Tier 1 — base operators Each adds a `HasType` rule + `Step` rule and full `progress` / `preservation` coverage (including the congruence and error-propagation cases): - **`or`** (logical) — mirrors the proven `and`. - **`sub`, `mul`** (integer) — mirror the proven `add`. ## Tier 3 — capability lattice - **`capSubsumes_refl`**, **`capSubsumes_trans`** — capability subsumption is a **preorder**. This is deliberately the order shape echo-types' `DecorationStructure` requires (`≤-refl`/`≤-trans`), keeping WokeLang's capability lattice on-path for a future echo/loss layer. ## Echo-types design compatibility Per your request, I checked echo-types `main` before extending, and documented it in `AUDIT.md`. The precedent is `EchoEphapaxBridge`: **Ephapax** (a linear-typed language) ports `EchoLinear` + `EchoResidue` into its prover as a separate **L3 layer**. So the echo/loss layer is a `Mode`-indexed decoration *on top of* the base type system — these base-operator extensions are **orthogonal and compatible**, and the capability preorder is a stepping stone toward it. ## Verification ``` $ lean docs/proofs/verification/WokeLang.lean # exit 0, sorry-free ``` ## Still open in Tier 1 (next increment) Ordering comparisons (`lt`/`gt`/`le`/`ge`), `div`/`mod` (divide-by-zero → `error` panic, reusing the proven panic fragment), float variants, and `array` typing. https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7 --- _Generated by [Claude Code](https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7)_ Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jun 15, 2026
…ation state (#83) ## Why The Lean + Coq proof repair/extension landed in **#79–#82 (all merged)** but was **invisible to the estate's bot-coordination layer**. The machine-readable state still described a pre-proof-work world: - `STATE.a2ml [frontier]` named only an aspirational Isabelle narrative and **omitted the existing, now-verified Lean+Coq type-safety track** entirely; `last-shepherd` stopped at #77. - `debt.a2ml` carried **zero** real items — so the documented proof follow-ups would not reach the next session's Phase 0. - `coverage.a2ml` had no record that `docs/proofs/verification/` was visited. - `methodology.a2ml`'s divergent-mode invariants were generic template stubs — one example literally read *"Idris2 only … no Lean4, Coq"*, the **opposite** of reality, a real footgun for a divergent-mode bot. ## What (all additive; no curated content overwritten) Surfaced through the channels whose own contracts say *"updated by agents at session end"*: | File | Change | |---|---| | `bot_directives/debt.a2ml` | Carry-forward follow-ups as Phase-0 input: **should** — Coq binop parity, Lean array typing (Coq's is a ready template), `cap_subsumes_trans`; **could** — Coq `preservation` clean rewrite, Lean float binops, echo-types L3 integration blueprint. | | `bot_directives/coverage.a2ml` | `docs/proofs/verification/` recorded as a visited component (PRs #79–#82). | | `bot_directives/methodology.a2ml` | `divergent-invariants`: provers are **Lean 4 + Coq** (not Idris2/Isabelle); admit/sorry stay **zero**; the `Coq.Reals` axioms are **permitted, not escape hatches** (don't let an Axiom-scanner flag them). `known-constraints`: CI-gated + toolchain-pinned (Coq is version-sensitive); Lean/Coq cover **complementary** subsets; PROOF-NEEDS #2 is **ill-posed** pending a maintainer (a)/(b) decision. | | `6a2/STATE.a2ml` | Added `type-safety-proofs` to `[frontier]`; added `proof-gates` + `last-proof-shepherd` to `[ci]`. Existing lines preserved. | Source of truth for every claim: [`docs/proofs/verification/AUDIT.md`](../blob/main/docs/proofs/verification/AUDIT.md). ## Notes for review - **Draft on purpose** — `.machine_readable/` is maintainer-curated (`gitbot-fleet`/`hypatia` are both barred from it), so this goes through human review rather than direct-to-`main`. - The only deletions are replaced **generic template-example comments** in `methodology.a2ml` (incl. the misleading "Idris2 only" stub). No real data removed. - `coverage.a2ml`'s `total/visited` summary counters were left untouched — I won't fabricate a component denominator. - Stacked on the merged #82; the net diff is the four files above. https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7 --- _Generated by [Claude Code](https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
The Lean 4 formal-verification file
docs/proofs/verification/WokeLang.leanclaimed "all 12sorryeliminated / verified" — but it had silently bit-rotted and did not compile under a current Lean toolchain (~100 errors). Root cause: no CI ever ran the prover (workflows only covered the OCaml core + e2e), so the headline correctness claim was never machine-enforced.This PR restores sorry-free compilation under Lean 4.30.0, adds the missing CI gate, and documents a coverage/correspondence audit.
What changed
Only proof bodies + 2
derivingclauses + 1abbrev— every theorem signature and every inductive is byte-identical (verified by diff). No statement was weakened; nosorry/admit/axiomintroduced.Root causes fixed:
DecidableEqno longer derives forValue/WokeType(Floathas none — NaN; and nestedList Selfblocks the deriving handler) → reduced toderiving Repr; equality decisions use Lean's classicalby_cases(no instance needed).induction/caseson concrete indices (emptyTypeEnv,emptyEnv) + binder-arity drift across Lean versions.preservationmade type-polymorphic viainduction hs generalizing t(its congruence cases need the IH at the operand type, not the result type).cases … with | inr ⟨..⟩anonymous-constructor patterns →obtain(no longer supported incases). Type-mismatched reduction siblings discharged withnomatch.BEq Permission: madePermissiona reducibleabbrevso theStringinstance transfers.Verification
Machine-checked:
progress,preservation,type_safety(multi-step),consent_monotonicity,consent_preservation— for the expression core (incl. the Result/unwrap/errorpanic-propagation fragment).Added
docs/proofs/verification/lean-toolchain— pins Lean v4.30.0.docs/proofs/verification/AUDIT.md— answers PROOF-NEEDS.md WokeLang EBNF grammar specification #1 & Implement WokeLang interpreter in Rust #2: the proofs cover a clean expression core (a strict, honestly-scoped subset), the Lean type system corresponds to the Rust typechecker (not the OCamlcore/eval.ml, which models a different language), and the consent theorems correspond to the spec's Hoare logic..github/workflows/lean-proofs.yml— installs the pinned toolchain and runs the check on every push to the proof dir, so this can't bit-rot again. SHA-pinned action, pure-bash install (matches estate governance).Note on scope
This repairs and re-verifies the existing proofs and makes them durable. It does not yet extend coverage (more binops/comparisons, statements, arrays, compiler/VM correctness) — those remain per PROOF-NEEDS.md and are tabulated in AUDIT.md.
https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7
Generated by Claude Code