harden(missions): close the false-proved paths, and audit the registry end to end - #579
Open
DrMurphyIsIn wants to merge 8 commits into
Open
DrMurphyIsIn wants to merge 8 commits into
DrMurphyIsIn wants to merge 8 commits into
Conversation
…ompiles
THE STRUCTURAL HOLE. The grant gate asked whether an artifact EXISTS, whether it
CONTAINS the node's statement, and (since 2026-09-18) whether it carries a `sorry`.
It never asked the question that makes those mean anything: is this file compiled by
anything? Twice in two days that gap produced granted nodes resting on Lean no build
had ever elaborated:
* ZeroFreePolylog / ZeroFreeElementary -- artifacts of two proved rh nodes, imported
by nothing, outside every guard's closure, no .olean in any built worktree. Fixed
2026-09-18 by giving them a guard and a build target.
* The ENTIRE zeta_reflection island -- home of ALL SIX proved anduril node artifacts,
granted 2026-09-18, referenced by NO workflow at all. Found by this change.
NEW MODULE missions/coverage.py answers one narrow decidable question: does some CI job
run `lake build` inside the island an artifact lives in? It parses every workflow, honours
step `working-directory`, job-level `defaults.run.working-directory`, and `cd .../lean`
inside a `run:` block (three jobs in this repo address their island that way, and missing
them would manufacture false orphans).
WIRED IN TWO PLACES:
* `grant_status` refuses to flip a node whose artifact is in an unbuilt island.
* `verify_campaign` reports the same as an ERROR for every already-proved node, so the
required `unit` job catches drift rather than only new grants.
Deliberately NOT checked: that the build passes (CI reports that on the commit) and that
the module is inside defaultTargets (Lake closures are not statically decidable from the
manifest; the islands express coverage through guard-lib import closures). This is a floor
-- it makes "granted against Lean nothing compiles" impossible and leaves the rest to the
island's own axiom guard.
ORPHAN ISLANDS are a WARNING, not an error: 12 islands carry Lean no workflow builds, but
an island with no node attached is scratch or in-flight work, and erroring on it would turn
this check into an allowlist that rots. Surfacing it is what stops one quietly acquiring
six granted nodes, which is precisely what happened.
ENABLING WORK: new `zeta-reflection-compiles` job builds the five axiom guards that import
exactly the six anduril artifacts, then asserts the exact axiom set over all 67 anchors.
None of the six is in that lakefile's defaultTargets, so a bare `lake build` does not cover
them; they are named explicitly. With the job present all four campaigns verify clean.
Four new tests. conjecture1_proved = False.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… answer CI caught my own version of the failure mode this module was written to find. WHAT BROKE. `_workflow_docs` swallowed a missing PyYAML and returned `[]`. The required `unit` job does not install PyYAML, so there `ci_built_islands` answered "no island is built by CI" -- and every proved node in every campaign failed the coverage check at once. The output read like a registry catastrophe; the cause was a missing dependency. A checker that degrades into a confident wrong answer is worse than one that admits it cannot parse. THREE FIXES, because any one alone would leave the class open: 1. `_workflow_docs` now returns None (not []) when PyYAML is absent, and the caller falls back to `_scan_islands_without_yaml`, a line-oriented parser with no dependencies. On this repo the two agree exactly (82 islands), and a test asserts that equality against the real workflows so the fallback cannot silently drift from the precise path. 2. `_assert_parser_sane` refuses the specific shape of a broken parse: reporting zero built islands while a workflow plainly contains `lake build` now raises CoverageParseError. One loud error beats N confident false ones. A repo that genuinely builds nothing is still fine. 3. pyyaml added to the `unit` job, so the precise path is the one that actually runs there. Two regression tests, both named for what they prevent rather than what they call. conjecture1_proved = False. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… wall islands in CI TWO DEFECTS, both instances of rules this branch is already enforcing elsewhere. 1. THE MEMO SHIPPED UNAMENDED ALONGSIDE ITS OWN REFUTATION. PR #572 landed RH_BARRIER_FE_UNIFORMITY_DESIGN_2026-09-18.md, whose headline is "no FE-uniform argument can prove any route's wall clause, and one witness refutes all four routes at once", together with wall_adversary/BarrierScopeXR.lean, which refutes exactly that. The refutation was written up only in the separate ascent-plan document, so a reader opening the memo got the unrefuted claim, and section 5 still instructed registering the node. Retraction banners added to the memo and to wall_barrier/README.md, naming the three kernel results that do the refuting (barrier_silent, transfer_to_member_fails, uniform_refutation_decides_nothing) and striking OP 3 / OP 4. Neither proposed node is on main, so nothing downstream is affected. The barrier is SOUND BUT EMPTY: its theorems refute only the universal over the bundle, while every route's wall clause is about ONE member, the completed zeta. The memo's own poly_refutes_poor_bundle shows s*(s-1) already refutes the bundle unconditionally, so the Davenport-Heilbronn witness contributes nothing at current bundle strength. The transfer theorems remain valid; what is withdrawn is their force as a barrier. The separate WallBarrierAM orientation-only result is unaffected and stands. 2. NEITHER WALL ISLAND WAS BUILT BY ANYTHING. No workflow referenced either, and wall_adversary had no lakefile at all -- a loose .lean file no project could build -- while the ascent plan cited its contents as "kernel-checked". Added a lakefile there and a wall-analysis-compiles job that builds both islands and asserts the exact axiom set over all 19 anchors. Leaving the refutation unbuilt would have left the retraction above resting on the same kind of claim it corrects. Orphan islands fall 13 -> 10. The remaining ten are older scratch dirs with no lakefile and no node attached, which is why the coverage checker reports them as a warning rather than an error. KNOWN GAP, recorded not fixed: neither wall island pins mathlib (no lake-manifest.json), so these builds are verified-at-run rather than reproducible. conjecture1_proved = False. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…by the gate audit An execution-based audit drove the real gate with throwaway campaigns and confirmed nine ways to reach `proved` without proving anything. None is exploited: all 47 proved nodes and the one refuted node were scanned and are clean. These are latent holes, closed now. ONE OF THEM WAS MY OWN, SHIPPED HOURS EARLIER. `island_of` regexed the UNRESOLVED artifact string, so `../../examples/wired/lean/../../unbuilt/lean/U.lean` was credited to the built island while the file sat in the unbuilt one. Attribution now uses the resolved path. SUFFIX EXTENSION was the sharpest. The normalized statement ends at the conclusion, so containment was a prefix match: an artifact proving `NoZero s ∨ True` satisfied a node claiming `NoZero s`, and `RH → RH` satisfied `RH`. `statement_matches` now requires the text immediately after a match to begin the proof body (`:=` or `by`), which is exactly where the statement ends. All 47 live proved nodes still match, so the tightening costs nothing real. ALSO CLOSED: * Self-supplied axioms and name shadowing. `axiom` and `unsafe` in DECLARATION position are now incompleteness markers (declaration-position, so the guards' own `#print axioms` idiom does not trip). This is the same mechanism as the 17 proved nodes that rely on definitions their artifact declares locally. * The statement hidden in a string literal. `_strip_lean_comments` preserves string contents on purpose; for CONTAINMENT they are caller-controlled, so they are blanked. * The refutation branch paid NONE of the checks the proof branch gained: a node could flip to `refuted` against an artifact carrying `sorry` in an island CI never builds. Both checks are hoisted above the branch, so either outcome pays them. A false `refuted` on an RH node is as loud a claim as a false `proved`. * Statement drift at grant. `regen_diff` was checked only by the read-only battery, so a hand-edited statement with a re-forged header hash was grantable. The gate calls it now. * No readback at grant. `promote_to_open` requires one; `grant_status` never re-checked, so a node set `open` by hand could be granted with no read-back on record. * A `lake build` under a literal-false `if:` vouched for an island it never builds. * DATA LOSS: `save_node` dropped `proof.fidelity_note`, so granting a node DESTROYED the note recording where it was actually verified. One live node carries it. Now modelled. STILL OPEN, deliberately: vacuity. Nothing checks that a registered statement is non-trivial -- `theorem p : True` is grantable. That is a judgement the machine cannot make, and it is what the read-back ceremony is for; see the audit document for the identity gap there. The parser-sanity guard now keys on "walked no steps" rather than "found nothing", because a repo whose build steps are all disabled is an empty answer that is CORRECT -- the earlier version raised on exactly that, which is the same over-eager failure it exists to prevent. Test fixtures updated where they modelled states the registry cannot reach: `open` nodes without a readback, and hand-written statement files with no generated header. Five new regression tests, each named for the attack it blocks. conjecture1_proved = False. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
What `status = "proved"` means, mechanically, link by link, and where it could be wrong. Execution-based: every attack was driven against the real gate in throwaway campaigns. HEADLINE: the live corpus is clean. All 47 proved nodes and the one refuted node were scanned against every mechanism found; no false claim exists today. Records the seven-link trust chain and what enforces each; the nine false-`proved` paths (eight now closed, vacuity deliberately not); the two self-inflicted bugs in the checker itself and why the pattern is the lesson; the seams that remain open (guard coverage is island-level not theorem-level, with two nodes guarded by nothing; 17 of 47 nodes rely on locally mirrored definitions with no drift today; non-Lean artifacts skip content checks; the reduction machinery has never run on a real node); and the operational findings. The central finding is not a code hole. Vacuity cannot be closed by code -- nothing can decide whether a registered statement says what its title claims -- so the strongest link in the chain is the read-back, and that is the one with no mechanism behind it: promote_to_open checks only that a readback EXISTS, --auditor is free text, and the independence requirement lives only in prose. In a project where authors, auditors and integrators are all autonomous sessions, that is the thing to decide next. conjecture1_proved = False. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
DrMurphyIsIn
changed the title
proved paths, and audit the registry end to end
…p destroying evidence A data-integrity audit drove the registry with real concurrent processes. Three holes could corrupt the live registry TODAY; all are closed here. 1. WRITES WERE NOT ATOMIC, AND A TORN FILE COULD READ BACK AS A VALID NODE. `save_node` truncated in place. Under two writers and two readers, 1325 of 8000 reads saw an EMPTY file and 399 saw torn TOML. Most torn reads fail loudly -- but an exhaustive byte-prefix scan of all 66 live node files found 201 truncation points that load as a VALID Node with a field silently missing, `readback` among them in 64 of the 66 files. Because the registry reads, replaces one field and writes back, a session that read a torn file mid-write PERMANENTLY erased the read-back, which is the record gating promote_to_open. All seven writers (nodes, manifests, claims, statements, toolchain, lakefile, root module) now go through `atomic_write_text`: temp file, fsync, os.replace. 2. CLAIMS DID NOT EXCLUDE. Six racing processes each returned a Claim naming themselves in one of thirty trials, and a racing stale-steal left a torn claim file that broke every claim operation in the campaign. The claim file is now created O_CREAT|O_EXCL; EEXIST is treated as contention and only then re-read for staleness. Re-probed with 8 processes x 12 trials: exactly one winner every time. 3. GRANTING DESTROYED HAND-WRITTEN EVIDENCE. `_node_to_doc` rebuilt the document from the dataclass, so any key the schema did not model was dropped. A live node carries a `[nonvacuity]` table and a `proof.fidelity_note` -- the latter recording that its proof is kernel-verified LOCALLY and NOT on main CI -- and any audit, link or grant erased 1978 characters of it without a word. Unmodelled keys are now retained on `Node.extra` and re-emitted; the round trip on that file is byte-identical. ALSO: * REAL TOML EVERYWHERE. `loads_toml` fell back to a hand-rolled subset parser when `tomllib` was absent, so CI (3.11+) and an older developer machine could read the same file differently, silently: extra spaces around `=` produced a key with a trailing space so the field VANISHED; a dotted key became a top-level key so the proof was ABSENT; a duplicate `[proof]` table from a botched merge was last-wins locally while CI rejected the file outright. `tomli` is now a dependency under 3.11 and is preferred over the fallback, which additionally refuses duplicate and dotted keys rather than guessing. All 74 live TOML files parse under the real parser. * `open-leaves` no longer KeyErrors on the cross-campaign dependency form introduced this week. It was the command the how-to tells every session to run first, and the first qualified reference would have broken it. * `link` required neither that the artifact exists nor that the node is not already proved; a bogus link stayed invisible to CI until someone ran `grant`. Both now checked, with `--force` for a deliberate repoint. * `mission audit` refused nothing: `--text "" --auditor ""` promoted a draft. Both must now be non-empty. * The attempts ledger silently swallowed malformed lines anywhere in the file, so recorded work vanished from every digest. Skipped lines are counted and surfaced as a warning. Three new regression tests, each named for what it prevents. conjecture1_proved = False. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Adds three sections to the 2026-09-19 architectural audit. 4b, the data layer: writes were not atomic and 201 byte-prefixes of live node files load as a VALID node with a field missing (readback in 64 of 66); claims did not exclude, with six racing processes each believing they won; granting destroyed hand-written evidence including the note recording that a proof is verified locally and NOT on main CI; and two TOML parsers meant two truths, silently, between a developer machine and CI. All closed. 4c, the operator surface: the table of seven mutating subcommands and what validates each. The MCP surface is read-only and is the one surface with no finding against it. 4d, the measurement behind the self-certification finding: 37 of 47 proved nodes carry a read-back whose auditor is the same session that registered them; ten have a blind-auditor read-back backed by testimony. The likely cause is a documentation gap rather than shortcutting -- the independence rule is in the design document but not in the how-to a session reads first, so a session auditing its own node has followed its instructions. Corrected section 4, which had wrongly said the how-to carries the rule. conjecture1_proved = False. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…actually read it The rule that the renderer must not be the statement's author lives in MISSIONS_DESIGN_2026-09-11.md section 8. The document a session reads first is MISSIONS_HOWTO.md, whose entire treatment of the ceremony never mentioned independence or blindness. A session that read the how-to and audited its own node had followed the instructions it was given -- which is why 37 of 47 proved nodes carry a read-back whose declared auditor is the session that registered them. This is the cheapest repair for the measured cause, and it names the reason: nothing in code enforces independence, and grant is containment against the very statement the author wrote, so the read-back is the only thing between a wrong or vacuous statement and a proved node. conjecture1_proved = False. Co-Authored-By: Claude Opus 5 (1M context) <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
1 participant
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.
Started as one fix and became the hardening pass plus the architectural audit. Full findings:
telperion/docs/MISSIONS_ARCHITECTURE_AUDIT_2026-09-19.md.The live corpus is clean. All 47 proved nodes and the one refuted node were scanned against every mechanism found. No false claim exists today. Everything below is about what was possible.
The structural hole
The gate asked whether an artifact exists, whether it contains the node's statement, and (since #569) whether it carries a
sorry. It never asked whether anything compiles the file. That produced two incidents in two days: two rh nodes proved against modules no build had ever compiled, and all six proved anduril nodes in thezeta_reflectionisland, which no workflow built at all.missions/coverage.pynow answers that question and is wired into both the gate and the battery in the requiredunitjob. A newzeta-reflection-compilesjob builds the five guards covering exactly those six artifacts, asserting the exact axiom set over 67 anchors.Nine false-
provedpaths, eight closedAn execution-based audit drove the real gate. Confirmed, ranked:
NoZero s ∨ TruesatisfiedNoZero s, andRH → RHsatisfiedRH. A match must now be followed by the proof body. All 47 live nodes still match.axiom/unsafein declaration position are now markers, without tripping the guards' own#print axiomsidiom.refutedon an RH node is as loud as a falseproved.regen_diffran only in the battery.save_nodedroppedproof.fidelity_note, the field recording where a node was actually verified.lake buildvouched for an island.Two self-inflicted bugs, kept in the record
The checker shipped briefly with a worse defect than any it was written to find: it swallowed a missing YAML dependency and answered "nothing is built", failing every proved node at once. Fixed with a dependency-free fallback a test holds equal to the precise path, plus a guard that raises rather than reporting a catastrophe. That guard's first version then misfired on a repo whose build steps are all legitimately disabled. Same over-eagerness, opposite direction.
Also here
The finding that is not a code hole
Vacuity cannot be closed by code. Nothing can decide whether a registered statement says what its title claims. The project's answer is the read-back, and that is the link with no mechanism:
promote_to_openchecks only that a readback exists,--auditoris free text, and the independence requirement lives only in prose. In a project where authors, auditors and integrators are all autonomous sessions, that is the decision to make next. Section 4 of the audit proposes recording grant provenance and statement authorship so self-certification becomes visible rather than impossible.conjecture1_proved = False.🤖 Generated with Claude Code