You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
docs(machine-readable): surface PRs #79-#82 proof work to bot-coordination 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>
type-safety-proofs = "docs/proofs/verification/ — WokeLang.lean (Lean 4.30.0) + WokeLang.v (Coq 8.18.0): both compile sorry/admit/axiom-free (Coq only the unavoidable Coq.Reals classical+funext axioms from modelling float as the reals) and are CI-gated (lean-proofs.yml, coq-proofs.yml). Proven for the expression core: canonical_forms, progress, preservation, type_safety (multi-step), consent_{monotonicity,preservation}. Strict subset of the surface language; Lean/Coq cover complementary fragments. Repaired from bit-rot + extended 2026-06-14/15 (PRs #79-#82, merged). Full audit: docs/proofs/verification/AUDIT.md"
30
31
31
32
[ci]
32
33
workflows = "20 GitHub Actions; thin-wrapper reusables from hyperpolymath/standards"
proof-gates = "lean-proofs.yml + coq-proofs.yml (added 2026-06-14): machine-check the Lean/Coq developments on every push. Before this NO CI ran a prover, so the 'verified/sorry-free' claim had silently rotted."
notes = "docs/proofs/verification/. Repaired bit-rotted WokeLang.lean (Lean 4.30.0) + WokeLang.v (Coq 8.18.0) to compile sorry/admit/axiom-free; extended the Lean type-safety core (or, sub/mul/div/mod with zero-divisor panic, lt/gt/le/ge, capability preorder); fixed Coq cap_subsumes reflexivity (proved cap_subsumes_refl); added lean-proofs + coq-proofs CI gates (no prover had ever run in CI); wrote AUDIT.md. PRs #79-#82, all merged. Carry-forward recorded in debt.a2ml."
issue = "Binops behind the Lean file: only add/eq/and have rules. Bring Coq up to parity with the extended Lean set — sub/mul/div/mod (div/mod panic to error on zero divisor), comparisons lt/gt/le/ge, and or."
issue = "Array typing/evaluation not modelled (tArray + an array congruence/value rule). The Coq file already has this (T_Array/T_Lit_Array + S_Array_step/S_Array_val + well-founded expr_size induction) and is a ready template."
issue = "cap_subsumes_trans not yet proven (cap_subsumes_refl is). The relation IS transitive; a robust proof needs explicit per-kind case analysis, not the brittle 6x6x6 automation."
issue = "preservation is a large brute-force `try solve [...]` pile ending in a literal 'Nuclear option' — it compiles and is axiom-honest but is fragile/unreviewable. Rewrite per-case in the style of the Lean preservation."
issue = "Echo-types L3 integration blueprint not started: a Lean port of EchoLinear + EchoResidue as WokeLang/Echo.lean (a Mode-indexed decoration on top of the base type system, leaving progress/preservation intact), modelled on Ephapax's formal/Echo.v Coq port. Connects to the STATE [frontier] echo-types goal."
# If parallel → stop. Note as cross-project insight.
71
71
72
72
[methodology.divergent-invariants]
73
+
# Real invariants for wokelang's formal-verification strength (populated
74
+
# 2026-06-15 from PRs #79-#82). The generic template examples below are
75
+
# DELIBERATELY NOT used — wokelang's provers are Lean 4 + Coq, not Idris2.
73
76
rules = [
74
-
# Customise per project. Examples:
75
-
# "Idris2 only for formal verification — no Lean4, Coq, Agda",
76
-
# "believe_me count must remain zero",
77
-
# "FFI architecture: Idris2 → RefC → Zig → C ABI (no shortcuts)",
77
+
"Verification provers for docs/proofs/verification/ are Lean 4 and Coq — deepen these two; do NOT switch to Idris2/Isabelle or add a third prover for the type-safety track (the STATE [frontier] echo-types narrative is a separate, additive layer, not a prover swap)",
78
+
"sorry / admit / Admitted count in WokeLang.lean and WokeLang.v must remain zero; the ONLY permitted axioms are Coq.Reals' ClassicalDedekindReals.sig_forall_dec + functional_extensionality (unavoidable from modelling float as the reals R) — these are NOT escape hatches, and an Axiom-scanner must not flag them",
79
+
"The proofs are a deliberate strict SUBSET of the surface language (the expression core) — broaden along the existing Step/HasType + progress/preservation pattern; do not claim full-language verification",
78
80
]
79
81
80
82
# Optional: language invariant for the core strength
@@ -88,10 +90,12 @@ rules = [
88
90
# Updated at session end with newly discovered constraints.
89
91
90
92
[methodology.known-constraints]
93
+
# Discovered 2026-06-14/15 (PRs #79-#82). See docs/proofs/verification/AUDIT.md.
91
94
constraints = [
92
-
# Customise per project. Examples:
93
-
# "End-to-end build has never been verified",
94
-
# "libproject.so does not exist yet — all bindings call stubs",
95
+
"Formal proofs live in docs/proofs/verification/: WokeLang.lean (Lean 4, pinned v4.30.0 via lean-toolchain) + WokeLang.v (Coq 8.18.0, ubuntu-24.04), both now CI-gated (lean-proofs.yml, coq-proofs.yml)",
96
+
"Both proof files had silently bit-rotted because no CI ever ran a prover; the toolchain pins are load-bearing and WokeLang.v is version-sensitive — do not bump Coq blindly",
97
+
"Lean and Coq cover COMPLEMENTARY subsets: Coq is ahead on arrays (T_Array + well-founded expr_size induction); Lean is ahead on binops (sub/mul/div/mod, lt/gt/le/ge, or). Neither is full-language",
98
+
"PROOF-NEEDS #2 (eval matches the Lean spec) is NOT a well-posed single theorem: core/eval.ml models a different language (units-of-measure, to_bool coercions, no Result) than the Lean/Coq Step relation. Needs a maintainer decision — (a) treat WokeLang.lean as normative and converge implementations, or (b) build a second model faithful to core/eval.ml — before attempting it",
0 commit comments