Repository navigation
Integrate accepted RMQ extensions and repair Linux verification - #2
Merged
Merged
Conversation
The 2026-08-09 fresh-blind audit returned NOT_ACCEPTABLE. Every blocking finding was reproduced here before being fixed. 210 is an upper budget, not exact cost: the theorem is _cost_le_, and a guarded invalid query is Costed.pure none with cost 0. Corrected on PAPER_CLAIM_CORRESPONDENCE.md:7 - which said cost 210 while citing an alias named ...Le210 - and on artifact/CLAIMS.md:82, which the audit did not cite. The defect originated in this project's own commissioning prompt, whose section 2 stated exact cost and handed that to the auditor as the target. Corrected, and it now names the _cost_le_ theorem and the zero-cost invalid query. Four gates had demonstrated false negatives, two of them gates this project wrote and claimed to have injection-verified. Both failed the same way: the injection tested the shape the author imagined, not the space of failures. hub_closure_lint parsed ^import only, so an indented import was invisible; constant_sync_check asked only whether the numeral appeared anywhere, so corrupting one of five 427s passed; claim_drift_scan exited 0 on a missing scan root; check_paper missed conventional-RAM phrasings. gate.ps1 also never invoked check_paper at all. Each fix is verified against the auditor's own mutation. Extending the paper patterns initially broke on RELATED_WORK_LEDGER describing Fischer and Heun correctly; the fix taught the attribution allowance that markdown ledgers cite with a bib key in backticks, matched against keys parsed from references.bib. RC-02 is not discharged as commissioned, so WDD-20260807-014 is void by its own terms; the corrected wording restores it without any Lean change. DD-20260809-095, WDD-20260809-028. Co-Authored-By: Claude Fable 5 <[email protected]>
The audit's P1-2/RC-10 finding, reproduced before fixing. rmq.tex said in the abstract that Stage A has been accepted and later that it is under a feasibility gate and neither accepted nor rejected. Three passages asserted the result is stated nowhere else than Section 9, while the allocated-bits entry of Section 3 states the capacity bound outright. Now one status throughout - accepted in the repository, not yet absorbed into a theorem environment - and a containment claim that is accurate rather than aspirational: stated in exactly two places, the allocated-bits entry and Section 9, with all three assertions corrected to match. THEOREM_LEDGER called the packed 210 logical fuel (charged trace events), which describes the other quantity. It now names the packed one as a structural countdown and records that independence holds at declaration and proof-term level, not module-closure level. EVIDENCE_MATRIX's frozen requirement asserts the invariant Section 3 falsifies. The text is frozen so an appended entry records that it does not hold, and why: the violation was created by the same commit that retracted the earlier false denial. Repairing one claim contradicted another. check_paper -SelfTest PASS; latexmk exit 0, zero undefined refs, 15 pages; git diff --check clean; strict claim-drift unchanged. Edits made through exact-string replacement, not Python str.replace - writing \ref in a Python replacement emits a carriage return and silently corrupts LaTeX cross-references. DD-20260809-096. Co-Authored-By: Claude Fable 5 <[email protected]>
The remaining item - promoting the packed result into RMQPaper - changes the Lean import graph and needs a full build. Starting it at the end of a long stretch is how the union-find cordon was corrupted and reverted earlier today. RC1_CORRECTION_HANDOFF.md records what a resumer would otherwise rediscover: which auditor items are closed and how each was verified; that WDD-20260807-014 is currently void by its own terms; that RMQPaper's closure contains zero PackedCellProbe modules; the import chain making module-level 210-independence false while declaration-level holds; that the base repin goes last; and that the next tag must not begin with v. Two items are left explicitly unresolved rather than papered over: promoting the packed result grows the reviewer surface the owner wants reduced, which needs a design decision rather than a silent mid-edit choice; and one claim in the parallel review is wrong - it reports no print axioms for the packed capstone, which exists at scripts/axiom_check.lean:1232. WDD-20260809-029. Co-Authored-By: Claude Fable 5 <[email protected]>
RMQPaper's closure was 153 files with zero PackedCellProbe modules, so the paper artifact root exported the charged-trace 210 story while the claim map named the packed theorem as the accepted claim. A reviewer asking which import yields the paper's theorem got two answers. Adds two aliases to RMQ/Headlines/RMQ.lean following its existing convention, and points the claim map at the public alias so the documented and importable identities are the same string. The alias is added to headline_axiom_check too - it was already audited from axiom_check.lean:1232, but it is the paper's headline claim and now paper-exported, so its trust story belongs in the inventory a reviewer runs. It depends on propext, Classical.choice, Quot.sound and nothing else. The docstring carries the three rules this result is repeatedly over-read without: 427 bounds attempted probes and is an upper bound; the result is cell-probe, not word-RAM time; and its 210 is the controller's structural countdown, not the charged-trace 210 exported a few lines above. Escalated rather than absorbed: this grows the closure 153 -> 204 files and 139,054 -> 190,529 lines, a 37% increase in the reviewer surface the owner wants reduced. Correctness first - a paper root advertising the wrong theorem is a defect, a large closure is a cost - but the resolution is likely a separate minimal paper root, which is an owner decision. DD-20260809-097. Co-Authored-By: Claude Fable 5 <[email protected]>
Touching a gate script requires a workflow-log entry; the promotion commit added a #print axioms line to headline_axiom_check.lean without one. Records why the duplicate audit is deliberate: axiom_check.lean is the exhaustive inventory, headline_axiom_check.lean is the short one covering the claims the paper actually makes. The packed capstone became a paper-exported headline claim in DD-20260809-097, so its absence there was a gap of the same class as the RMQPaper closure defect. Also records that the parallel review's claim that no #print axioms existed for it was wrong. Co-Authored-By: Claude Fable 5 <[email protected]>
Marks 4.1 done with the measured closure growth (+51 files, +51,475 lines, +37%) and states plainly that the separate-minimal-root resolution is an owner decision that was not settled in the promotion commit. Co-Authored-By: Claude Fable 5 <[email protected]>
The ledger's claim that the packed 210 references neither queryCost nor nonSyntheticWeight was prose about a proof term. scripts/independence_check.lean now walks the transitive constant closure of the countdown theorem's type and value and fails if either appears: 1855 constants, neither present. Wired as gate step 3b. Scope matches the ledger deliberately - the property is declaration- and proof-term-level, not module-closure-level, since the packed module's compilation closure does reach the charged declaration. Three vacuity guards, two of which exist because injection broke the first version. Skipping proof terms left the type-reachable control green while the target closure collapsed 1855 -> 16 and still passed; making the walk non-transitive left both controls green because both are shallow, and only the closure floor caught it at 74 < 500. WDD-20260809-017. Co-Authored-By: Claude Fable 5 <[email protected]>
Notes the two things a future script needs: RMQ modules shadow Lean.Name so metaprogramming identifiers must be fully qualified, and import Lean is safe in scripts/ but must not enter a library module. Also records that the walker is reusable for any future 'X does not depend on Y' claim. Co-Authored-By: Claude Fable 5 <[email protected]>
Co-Authored-By: Claude Fable 5 <[email protected]>
P3-1a: bpChunkedCrossBlockCloseCostedWithRankSeed_cost_le_principled accepted an unused close-position premise. Removing it exposed that the identical premise on canonicalLcaCloseCostedWithRankSeed_cost_le and _cost_le_principled existed only to feed it - one decorative hypothesis chain across three theorems, now stated without it. Strengthening: conclusions and quantifiers untouched, so every frozen row citing them still discharges. Disclosed in each docstring the way B6 REQ-B6-09 disclosed its hsameBlock addition. Checked that B6_SAMEBLOCK_ACCEPTANCE_MATRIX and PAPER_MODEL_ADEQUACY cite the conclusion rather than the hypothesis list. Also corrects a docstring the audit did not catch: the cap was said to require 'the genuine close-position bounds', plural. It requires exactly one. P3-1b: the cost-algebra comment called the component caps 'tight'. They are <= bounds, and the aggregate 210 has no attainment witness - only the interior 33 does. The comment now says so and says not to reintroduce 'tight' without a theorem exhibiting an attaining execution. Also strips a trailing blank line at EOF in DESIGN_DECISIONS.md that failed the Artifact Reproducibility whitespace check on c140d68. That run reached GATE PASS, including the new independence check, and failed only on this. DD-20260809-099. Co-Authored-By: Claude Fable 5 <[email protected]>
68 is cited across three result documents and the manuscript as 'the fixture run issues 68 attempted probes', but lived only as a local have inside one proof - nothing outside it would have broken had it drifted. Now egcpFixtureTraceLength, derived from egcpFixtureTraceAddresses so the length cannot disagree with the literal address list, with the former local have routed through it. Added to axiom_check; propext and Quot.sound only. Both the docstring and the inventory comment state what the number is not: it is = for one pinned fixture and is NOT an attainment witness for 427, which remains an upper bound with no execution known to attain it. Field 32 is an eta equation closed by rfl, whose content is entirely in the elaboration - it pins the controller's arity and argument types, so the controller cannot take xs, a shape, or an oracle. The audit's point was that it reads like the semantic no-hidden-input theorem. The field is sound; the way it invited being cited was not. Its docstring now says what it does not establish and points at fields 33 and 34, which carry the semantic content. Proof note: simpa exhausts the isDefEq heartbeat budget by trying to evaluate the run term; raising maxRecDepth misdiagnoses it. DD-20260809-100. Co-Authored-By: Claude Fable 5 <[email protected]>
Follows the B6 REQ-B6-08 precedent of making trust evidence durable in the inventories. Kept out of headline_axiom_check deliberately: that list is the claims the paper makes, and diluting it would cost the one-screenful property that makes it worth running. WDD-20260809-018. Co-Authored-By: Claude Fable 5 <[email protected]>
Co-Authored-By: Claude Fable 5 <[email protected]>
All nine :NNN citations in THEOREM_LEDGER.md resolved against the tree. Seven correct. L-PACK-01's producer :702 drifted to :723 from this round's field-32 docstring. L-UB-06's :9349 was already wrong at the pinned base commit e3362d4, where the theorem sat at :8261 - about 1,090 lines off, not introduced by any recent change and not caught by the fresh-blind audit. Recorded in EVIDENCE_MATRIX rather than quietly fixed, because the second case shows a pinned base commit does not make a citation right: a reviewer following :9349 at the exact commit the ledger names lands in unrelated code. Nothing checks these; they are prose shaped like references. Also rewrites the handoff's base-repin section, which understated the task. The pin has two roles - a substrate statement that must move, and 31 per-row ACCEPTED_BASE records that assert verification against a tree. Restamping the latter without re-verifying is this project's recurring defect class. Co-Authored-By: Claude Fable 5 <[email protected]>
RC1_CORRECTION_HANDOFF.md is workflow-classified, so every commit touching it must also update WORKFLOW_DESIGN_DECISIONS.md. Commits 2bd03d8 and 9389655 did not, and CI failed on both. Local verification missed it because it used -Base HEAD~2/HEAD~3, spanning the whole batch just committed - and some commit in that range did update the file, so the range looked compliant. CI uses -Base HEAD~1: each commit against its own parent. A range that is collectively compliant can contain commits that are not. Same shape as the gate defects the audit found: a verification that resembles the real check closely enough to feel conclusive while testing something weaker. WDD-20260809-019. Co-Authored-By: Claude Fable 5 <[email protected]>
The first sweep matched :NNN only on lines also naming a .lean path, but the File: line comes after Declaration: in every row, so 18 of 27 citations were invisible. A second sweep attributed citations to the nearest preceding .lean mention and manufactured three past-EOF defects that did not exist. The third parses rows and resolves each citation against every file named in the row. 24 resolve. Three were wrong: L-PACK-01 and L-ARCH-01 both cite the capstone producer at :702, displaced to :723 by this round's field-32 docstring, and L-UB-06's :9349 was already wrong at the pinned base commit by ~1,090 lines. L-ARCH-01 was missed by both earlier sweeps. Records the rule: a grep over a structured document is sampling with an unknown miss rate, not verification. Fine for locating things, not as the basis for a universal claim, because the miss rate is invisible in a clean result. WDD-20260809-020. Co-Authored-By: Claude Fable 5 <[email protected]>
DD-20260809-101. Companion to WDD-20260809-020: that entry records how the audit method failed twice, this one records what changed on the paper surfaces. Three citations corrected, 24 unchanged. No proposition, declaration name, or status changed. Notes the consequence for the pending repin: ACCEPTED_BASE is defined as 'kernel-checked declaration present on the base commit', so repinning does require moving the per-row Commit: fields - but the basis is a green build plus axiom inventories confirming each named declaration still exists, not a licence to trust line numbers, which no build checks. Co-Authored-By: Claude Fable 5 <[email protected]>
Moves the substrate from e3362d4 to 688c54a, the last commit of the RC-1 correction round with both CI workflows green. Reading the ledger header settled a question this round had got wrong: ACCEPTED_BASE is defined as 'kernel-checked declaration present on the base commit' - a claim about the pinned tree, not a historical acceptance date. So the 29 per-row Commit: fields move with the substrate pin, and each move restates a claim. Restating a claim is not done on faith, so at 688c54a: lake build RMQ exit 0; axiom_check exit 0 with no sorryAx or ofReduceBool; the new ledger_decl_check confirms all 53 cited declaration names are present; all 27 line citations resolve after three corrections. Deliberately not moved: three mentions of the old base in EVIDENCE_MATRIX and one in THEOREM_LEDGER, which state what was true at the previous pin. A blanket replace would have rewritten history to say the old audit happened at a commit that did not exist yet. All 38 occurrences were classified individually. L-ARCH-01 gains an Amended line rather than a silent restamp: this round retracted its 'logical fuel' gloss on the packed 210. The proposition was not re-audited and the row now says so. Adds scripts/ledger_decl_check.lean as gate step 3c with a count floor, a negative control, and deliberately wide imports - the last because its first run reported two phantom absences that were really RMQ/Headlines.lean being outside every artifact root's closure. DD-20260809-102, WDD-20260809-021. Co-Authored-By: Claude Fable 5 <[email protected]>
Nine tag references retargeted. Adds RC-11, artifact-root correspondence: take the theorem PAPER_CLAIM_CORRESPONDENCE names as the accepted claim and check that importing the paper artifact root actually gives you it. That is the defect this round fixed - RMQPaper's closure held zero PackedCellProbe modules while the claim map named the packed theorem - and no existing row would have caught it, since RC-10 compares the manuscript to the theorems rather than asking which import yields them. Report section updated to RC-01..RC-11. Co-Authored-By: Claude Fable 5 <[email protected]>
Writes the 2026-08-09 round-log entry, which was owed by the standing default that every audit round is logged. Records the three findings worth carrying: the exact-cost defect originated in this project's own commissioning prompt; two of the four broken gates were ones this project wrote and claimed to have injection-verified; and the sharpest finding came from the non-blind review rather than the blind audit, which is why RC-11 now exists. Also records the round's own recurring defect - three verifications that stood in for weaker properties than claimed, all after an audit whose subject was exactly that - and the L-UB-06 citation that was wrong at the pinned base commit itself by ~1,090 lines. Rewrites the handoff as a short resume card: the RC-2 audit is uncommissioned, WDD-20260807-014 stays void until RC-02 discharges in its corrected form, and the minimal-paper-root question is an open owner decision. Co-Authored-By: Claude Fable 5 <[email protected]>
Every finding independently reproduced first; none were wrong. P1-01 claim honesty: PAPER_THEOREM_MAP said the charged-trace cost 'is exactly 210' while the same file disclaimed attainment; RELATED_WORK_AND_LIMITATIONS and paper/THEOREM_LEDGER claimed a 'tight component-wise cap' when only the interior 33 has an attainment witness. This was our own incomplete fix - DD-20260809-099 retracted exactly this in the source comment three days earlier and never synced the surfaces repeating it, including a file edited in that same commit. P1-02: README and PUBLICATION_STRATEGY said payload construction 'is accounted separately', asserting an accounting that does not exist. Now stated as unproved and excluded from the bound, matching ledger row L-OPEN-01. P1-03: the Windows ownership path closed the kill-on-close job and waited on the root alone, while POSIX waits for the whole group - so a grandchild could outlive the assertion that the tree was dead. Adds a real descendant barrier that enumerates job members before closing and waits for them. Every CI job ran ubuntu, so this path had no coverage at all; two standalone ownership jobs now run on windows-2022 and ubuntu-24.04 without needing a Lean build. An inconclusive barrier run exits nonzero rather than reporting a pass. P1-04: applied the novelty log's repairs, which documented each defect with an exact replacement and had never been applied - the Tanaka conflation, the priority overreach, Fischer-Heun mislabelled systematic, the cell-probe convention mis-sourced to a self-declared word-RAM paper, and the invented /HOL title fragment. Four load-bearing bib entries added; ledger rows corrected. One deviation: the log's priority paraphrase trips our own priority-claim detector, correctly, so the sentence reports their belief instead of restating 'the first'. P2-01: the independence forbidden set held the two names the ledger sentence uses; a proof could reach the charged cost through the algebra or its equalities and pass. All eight now listed. The three original injections tested the collector, never whether the set was the right set. P2-02/P3-01: field 27's 'never a stored numeral' is not entailed by its extensional equalities - scoped to what it proves; field 15 said 'both decoded header fields' when the header stores one. Prevention: a claim-drift term for exact/tight formulations of 210 and 427, injection-verified against the audited wording rather than an imagined one. DD-20260812-103, WDD-20260812-024/025/026. Co-Authored-By: Claude Fable 5 <[email protected]>
The first Windows barrier introduced a second defect. Stop-RMQWindowsOwnedJob closes the handle then throws on survivors; the callers zeroed their handle AFTER the call, so a throw left a non-zero handle and finally invoked the barrier again, failing CloseHandle on an already-closed handle. The surfaced error became 'The handle is invalid', replacing the true survived-cleanup diagnosis. The first full-gate run failed exactly this way, at CLEAN-BASELINE/PORTABILITY rather than the deadline control. Callers now zero their own copy before invoking the barrier, so a throw cannot cause a second close and the real error survives. WDD-20260812-027. Co-Authored-By: Claude Fable 5 <[email protected]>
The second gate run failed with "The property 'Count' cannot be found on this object". A PowerShell pipeline matching nothing yields $null, not an empty array, and $null.Count throws - so the wait loop failed whenever NO member survived, i.e. on the healthy path. A barrier written to detect survivors crashed precisely when there were none. Adds Get-RMQAliveProcessIds, wrapped in @(...) at every call site, and pins the edge cases in Invoke-RMQOwnedProcessCollectionSelfTest: null, empty, all-dead, one-live, mixed, zero-handle barrier, and a live job with no survivors. The standalone -SelfTest entry runs them, so the new Windows and POSIX CI jobs cover them in about a minute. Three defects in this one function across two days - the missing wait, the handle released after the throw, and this. All three found by running it, two of them only by a 90-minute aggregate gate. WDD-20260813-028. Co-Authored-By: Claude Fable 5 <[email protected]>
Pre-existing defect, newly visible. With the M1 deadline control repaired the gate reached the topology regression for the first time and failed with 'sleeper child PID receipt was not written'. That harness bounded its sleeper at 5s while the identical M1 control uses 20s; the sleeper must complete two sequential PowerShell startups - its own, then the grandchild it spawns - before writing the receipt the assertion requires. git log shows no commit from this round touched that file. It was hidden because M1 failed first and aborted the gate, so nothing downstream of M1 had ever run to completion on Windows. Two divergent implementations of the same control with a 4x budget difference and no comment is the shape that hides this. WDD-20260813-029. Co-Authored-By: Claude Fable 5 <[email protected]>
Writes the 2026-08-12/13 round-log entry and RC2_CORRECTION_HANDOFF.md. Corrects a claim committed earlier in this round: WDD-20260813-029 said the aggregate gate had never run to completion on Windows. The repository's own records contradict it - a Windows deadline-control PASS at 98.3s, and a full gate exit 0 in 3101.473s across all 16 topology cases. The claim was inferred from two consecutive failures, which does not license 'never'. The accurate account: the missing barrier made the control a race that usually wins, since closing a kill-on-close job kills the tree almost at once and the assertion ran after WaitForExit on the root. So Windows receipts mostly said PASS and a real defect looked like a flake. What made that survivable is the CI gap, which is separately verifiable - every job ran ubuntu-24.04. WDD-20260813-030. Co-Authored-By: Claude Fable 5 <[email protected]>
Nine tag references. Adds owned_process_tree.ps1 -SelfTest to the gate table - it was unlisted, so an auditor enumerating gates would not have found the layer whose defect produced P1-03 - and a note that gate.ps1 must be run to completion with the platform named, that its ownership layer has two implementations of which only one runs per host, and that an INCONCLUSIVE self-test is uncovered rather than passing. Discloses the sequencing: the Windows GATE PASS was captured on 60c81ae and this commit changes one docs/internal markdown file, so the tagged tree differs from the gate-verified tree by that file. CI re-runs the full gate and both ownership jobs on the tagged commit. WDD-20260813-031. Co-Authored-By: Claude Fable 5 <[email protected]>
Answers P1-2, P1-3, P2-1, P2-3, P2-4, P3-1 of the 2026-08-15 fresh-blind audit. Every finding reproduced before repair. P1-2: gate.ps1 ran the M1 registry and NEITHER EG-CP replay, so the required gate's mutation coverage excluded the release headline. Both now run from the aggregate with propagated exit codes. This survived two prior audits because every individual piece was green - nobody asked whether the gate contained the suites. P1-3: six topology fixtures timed out at 300s on the auditor's runner, with a measured slow path of 298.145s. The topology pair moves to 900s with the derivation recorded beside it; M1 stays at 300s and now states why. Second deadline defect in that file - fixing the sleeper bound without asking what else was chosen rather than derived is what left this one. P2-1: the independence checker targeted the structural equality while the published derived_cap_le_427 is fed by packedReviewerRunAgainstMemory_trace_ length_le_427. Now checks all three cap suppliers. Third defect in that file: collector, then forbidden set, now target. P2-3: RunAxiomCheck is a whitelist, not a two-name blacklist. P2-4: the strict scanner suppresses allowed hits - it leaked ~1,579 lines of prior audit reports to a blind auditor after being identified last round. P3-1: ledger counts corrected and now derived by check_paper, which also stopped REQUIRING the pending marker it should have been catching. WDD-20260816-032. Co-Authored-By: Claude Opus 5 <[email protected]>
Answers P1-1, the finding that drove the NOT_ACCEPTABLE verdict. At the release tag, import RMQPaper gave a kernel-exported 427-probe capstone while rmq.tex pinned to an ancestor, titled Section 9 provisional, stated an unspecified constant C, and carried an ARCHITECTURE_RESULT_PENDING marker. Section 9 is now 'A packed cell-probe architecture' with a theorem environment stating the result at 427, replacing the targetstmt. Four further assertions that the result was unabsorbed - header comment, abstract, contributions, conclusion - became false once the theorem landed and are fixed. The theorem carries its three non-licensed readings inline: 427 bounds ATTEMPTED probes and is an upper bound (fixture issues 68); cell-probe, so not word-RAM or preprocessing time; and its 210 is the structural countdown, independent of the charged budget. This was on the coordinator's known-open list rated as editorial. That was wrong - at a release candidate it is a release-blocking mismatch. DD-20260816-105. Co-Authored-By: Claude Opus 5 <[email protected]>
The 2026-08-15 fresh-blind audit failed RC-10 because this substrate was pinned to an ancestor of the release tag: at the release commit `import RMQPaper` supplied the 427-probe capstone while the manuscript still called it a future editorial insertion. The paper and the artifact did not identify the same claim. The theorem absorption landed in the previous commit. This moves all 38 full-SHA pins across the substrate from `688c54a3...` to `0665b494...` so the 29 ACCEPTED_BASE rows -- whose status is DEFINED as "kernel-checked declaration present on the base commit" -- restate their claim about the tree that actually carries it. Mentions of `688c54a3` and `e3362d4` that survive are deliberate: they record what was true at earlier pins. Co-Authored-By: Claude Opus 5 <[email protected]>
…816-033) The P2-4 entry claiming this leak was closed was false when written. Two attempts had failed, both exiting 0: 1. Suppressing `allowed` output -- the leaking hits are labelled `review`, so 104 lines of prior audit reports still printed. 2. A `Get-ScanFiles` filter using `-like "*\audit_reports\*"` -- backslash is not an escape character in a -like pattern so it matched nothing, and that function feeds only the required-attribution pass, never the term scan that produces the leak. The measurement after attempt two was byte-identical to before it. A filter that matches nothing is indistinguishable from one that works, except by count. Fixed in both enumerations: rg globs for the term scan, the PowerShell predicate for the attribution pass. 1,579 -> 1,160 hits; 339 -> 0 process-record citations; -IncludeProcessRecords reproduces 1,579 exactly. `-SelfTest` now asserts both that no emitted line's PATH FIELD cites a process record, and that the exclusion removes a nonzero number of hits -- the second being the only signal that would have caught attempt two. Verified by injection. gate.ps1 runs it before the strict scan, since this gate's output is the contamination channel and blind auditors are required to run it. Co-Authored-By: Claude Opus 5 <[email protected]>
Reproduced the aggregate-gate claim-scan failure on the unchanged NATIVE-1 candidate 4edb1e1 with the unchanged scanner and policy: the strict default-root scan exits 1 with 17 unapproved matches (14 in commands/final-static-command.json, 3 in commands/final-claims-public.json) and the self-test exits 1 because it cannot read a hit count from both runs. Freeze the repair matrix before any receipt, manifest, verifier or attribute change: the four repair rows and the three restated replay rows are copied verbatim from the governing prompt (byte-checked), the 31 inherited rows and 4 continuation obligations are referenced by their frozen sources with preservation checks, and the verification ledger is fixed. Record the decision to archive scanner-output receipts as exact gzip blobs in WDD-20260913-NATIVE1-R1-001. Co-Authored-By: Claude Opus 5 <[email protected]>
…ip blobs Replace the twelve receipts under docs/internal/extensions/native1/commands/ whose base blobs contain claim-scanner result lines with single-member gzip archives at the same path plus .gz. Each archive decompresses to the exact Git blob bytes at 4edb1e1 (8,785,885 bytes, 4,571 result lines, 1,206,228 archive bytes). The scanner, claim policy, globs, allowlists and exclusions are unchanged; ripgrep skips the binary archives while traversing the scan roots, so the historical output leaves the scanned text corpus. Add repair-r1/RECEIPT_ARCHIVES.json (per-file original path, base blob id, blob SHA-256 and length, result-line count, archive path, archive SHA-256 and length, decompressed length, referring files), verify_receipt_archives.py (recomputes every value from the archives and git cat-file on the base and rejects missing, duplicate, extra and mismatching entries), and the versioned 19-case control runner with its mutation/hold helper. Mark each archive binary with an exact .gitattributes line. Existing references to the original names are not rewritten; the manifest resolves them. Co-Authored-By: Claude Opus 5 <[email protected]>
On the repaired commit d0b4cef the unchanged strict default-root claim scan exits 0 (1907 hits, 0 strict failures) and the scanner self-test exits 0 (exclusion removed 431 hits), after the same mutex session reproduced the base failure. The 19-case receipt-archive control runner passes under Windows PowerShell 5.1 with restoration digests equal; the preservation checks, diff checks, strict design checks and trust hygiene scans pass. Add the worker report (Status: INCOMPLETE, awaiting coordinator certification), the committed controls receipt, an evidence appendix after the byte-preserved frozen matrix, and a WDD verification note. No gate result or acceptance is claimed. Co-Authored-By: Claude Opus 5 <[email protected]>
Merge of 3832502 (codex/bv-1-fully-charged-rank-select), accepted at the lane rung by the coordinator. Acceptance record: extension-coordination-20260911/claude-coordinator-20260912/BV1_COORDINATOR_ACCEPTANCE.md Aggregate gate on the exact lane tip: bv1-gate (PASS, 13,568.9 s). Audit: BV-1-A1 fresh blind audit (63,613 B, SHA-256 BBA6ED82...). Conflicts in the append-only ledgers (docs/DIGESTION_LOG.md, docs/FAMILY_SUMMARY.md, docs/internal/DESIGN_DECISIONS.md, docs/internal/WORKFLOW_DESIGN_DECISIONS.md) and lakefile.toml are resolved as the current bytes followed by this lane's appended bytes, in lane order; each lane's change to those files is a pure append to the base blob (checked before resolution). The BV-1 lakefile bytes stay as the prefix; the line-ending decision INT-D1 is left to the owner. Integration candidate composed under owner approval of 2026-09-18 (step 1 of INTEGRATION_PLAN_DRAFT.md), with LB-1 and OPT-1 squashed instead of merged for the per-commit design check; not merged to main, not pushed. Co-Authored-By: Claude Opus 5 <[email protected]>
…(squash of 7f21dc8) Squash of 7f21dc8fa843a0f63025624fb3ad05a3bef234ae (codex/lb-1-variable-payload), accepted at the lane rung by the coordinator. Lane history (kept on the lane branches): codex/lb-1-variable-payload (0bbbe8c matrix freeze, d6dabbe, 5033ce5, 7f21dc8). Squash-merged, following the PRE-1 precedent (ruling R-S7-3), because lane commits 5033ce5 and 7f21dc8 fail the per-commit design check on their own under the checker main will carry, and main certifies every non-merge commit (WDD-20260817-079; the retrospective record is pinned to eight pre-policy commits). The squashed change carries every ledger entry of the lane and passes the check. Acceptance record: extension-coordination-20260911/claude-coordinator-20260912/LB1_COORDINATOR_ACCEPTANCE.md Aggregate gate on the exact lane tip: lb1-gate (PASS, 12,037.7 s). Audit: LB-1-A1 fresh blind audit (80,118 B, SHA-256 F08544F2...). Conflicts in the append-only ledgers (docs/DIGESTION_LOG.md, docs/FAMILY_SUMMARY.md, docs/internal/DESIGN_DECISIONS.md, docs/internal/WORKFLOW_DESIGN_DECISIONS.md) and lakefile.toml are resolved as the current bytes followed by this lane's appended bytes, in lane order; each lane's change to those files is a pure append to the base blob (checked before resolution). The BV-1 lakefile bytes stay as the prefix; the line-ending decision INT-D1 is left to the owner. Integration candidate composed under owner approval of 2026-09-18 (step 1 of INTEGRATION_PLAN_DRAFT.md), with LB-1 and OPT-1 squashed instead of merged for the per-commit design check; not merged to main, not pushed. Co-Authored-By: Claude Opus 5 <[email protected]>
Merge of e80da1a (codex/native-1-r1-claim-receipts), accepted at the lane rung by the coordinator. Acceptance record: extension-coordination-20260911/claude-coordinator-20260912/NATIVE1_COORDINATOR_ACCEPTANCE.md Aggregate gate on the exact lane tip: native1-gate-r1 (PASS, 16,568.3 s). Audit: NATIVE-1-A1 fresh blind audit (91,524 B, SHA-256 5CF155B5...) on 4edb1e1, carried by the evidence-only repair NATIVE-1-R1. Conflicts in the append-only ledgers (docs/DIGESTION_LOG.md, docs/FAMILY_SUMMARY.md, docs/internal/DESIGN_DECISIONS.md, docs/internal/WORKFLOW_DESIGN_DECISIONS.md) and lakefile.toml are resolved as the current bytes followed by this lane's appended bytes, in lane order; each lane's change to those files is a pure append to the base blob (checked before resolution). The BV-1 lakefile bytes stay as the prefix; the line-ending decision INT-D1 is left to the owner. Integration candidate composed under owner approval of 2026-09-18 (step 1 of INTEGRATION_PLAN_DRAFT.md), with LB-1 and OPT-1 squashed instead of merged for the per-commit design check; not merged to main, not pushed. Co-Authored-By: Claude Opus 5 <[email protected]>
…f183dba) Squash of f183dbafb5afd66cdfd855eb2a025613e59e48ae (codex/opt-1-r2-claim-receipts), accepted at the lane rung by the coordinator. Lane history (kept on the lane branches): codex/opt-1-packed-compiler (aecf4a5) -> codex/opt-1-r1-replay-certification (4cc9501) -> codex/opt-1-r2-claim-receipts (f183dba). Squash-merged, following the PRE-1 precedent (ruling R-S7-3), because lane commits 3b82967 and f183dba fail the per-commit design check on their own under the checker main will carry, and main certifies every non-merge commit (WDD-20260817-079; the retrospective record is pinned to eight pre-policy commits). The squashed change carries every ledger entry of the lane and passes the check. Acceptance record: extension-coordination-20260911/claude-coordinator-20260912/OPT1_COORDINATOR_ACCEPTANCE.md Aggregate gate on the exact lane tip: opt1-gate-r2 (PASS, 11,016.1 s). Audit: OPT-1-A2 fresh blind audit (85,760 B, SHA-256 0B783074...) on 4cc9501, carried by the evidence-only repair OPT-1-R2. Conflicts in the append-only ledgers (docs/DIGESTION_LOG.md, docs/FAMILY_SUMMARY.md, docs/internal/DESIGN_DECISIONS.md, docs/internal/WORKFLOW_DESIGN_DECISIONS.md) and lakefile.toml are resolved as the current bytes followed by this lane's appended bytes, in lane order; each lane's change to those files is a pure append to the base blob (checked before resolution). The BV-1 lakefile bytes stay as the prefix; the line-ending decision INT-D1 is left to the owner. Integration candidate composed under owner approval of 2026-09-18 (step 1 of INTEGRATION_PLAN_DRAFT.md), with LB-1 and OPT-1 squashed instead of merged for the per-commit design check; not merged to main, not pushed. Co-Authored-By: Claude Opus 5 <[email protected]>
…544cd) Squash of 74544cd24b476f72765caebdff6ea155514e5bb4 (codex/pre-1-r2-consumer-markers), accepted at the lane rung by the coordinator. Lane history: codex/pre-1-packed-preprocessing (contract phase, builder stages S1-S8, final candidate 84ae12f) -> codex/pre-1-r1-claim-receipts (a0c93e9, claim-scan evidence archives) -> codex/pre-1-r2-consumer-markers (74544cd, fail-closed consumer markers, halts and Run.Safe controls). Squash-merged per coordinator ruling R-S7-3 because single lane commits (75a6301, 6ccfb5c, fa8e34e, 02aa945, 3ce9b89) fail the per-commit design check on their own; the squashed change passes it. Acceptance record: extension-coordination-20260911/claude-coordinator-20260912/PRE1_COORDINATOR_ACCEPTANCE.md Aggregate gate on the exact lane tip: pre1-gate-r2 (PASS, 13,939.8 s). Audit: PRE-1-A2 fresh blind audit (53,979 B, SHA-256 bda5f414...) on 84ae12f and PRE-1-A2C continuation audit (66,433 B, SHA-256 a5a40ecf...) on 74544cd. Conflicts in the append-only ledgers (docs/DIGESTION_LOG.md, docs/FAMILY_SUMMARY.md, docs/internal/DESIGN_DECISIONS.md, docs/internal/WORKFLOW_DESIGN_DECISIONS.md) and lakefile.toml are resolved as the current bytes followed by this lane's appended bytes, in lane order; each lane's change to those files is a pure append to the base blob (checked before resolution). The BV-1 lakefile bytes stay as the prefix; the line-ending decision INT-D1 is left to the owner. Integration candidate composed under owner approval of 2026-09-18 (step 1 of INTEGRATION_PLAN_DRAFT.md), with LB-1 and OPT-1 squashed instead of merged for the per-commit design check; not merged to main, not pushed. Co-Authored-By: Claude Opus 5 <[email protected]>
…ule for it Owner decision INT-D1 (2026-09-19): the integrated build manifest uses LF line endings like main. BV-1 had committed the file with CRLF on most lines and pinned those bytes with `lakefile.toml -text` for its whole-file replay hash; that identity cannot survive any integration, because the combined manifest must carry every lane's [[lean_exe]] stanza. The attribute line and its comment are removed; all other BV-1 byte-preservation rules stay. Parsed TOML content is unchanged (tomllib before/after: same package, libraries and the same seven ordered executable targets). Design record: DD-20260919-INT-001. Co-Authored-By: Claude Fable 5.1 <[email protected]>
The topology lint skips files whose whole text holds neither the snapshot marker nor a removed spelling (verdicts unchanged; one run fell from about 1,590 s to seconds), and the PRE-1 builder gate checker builds the replay's prerequisites under its own deadline before the replay starts, so a cold tree (CI, a fresh worktree) no longer fails as inconclusive. WDD-20260919-INT-001. Co-Authored-By: Claude Fable 5.1 <[email protected]>
The packed-query replay runs fixtures with `lean --run`; on Linux the
interpreter overflowed the default 8 MiB main-thread stack ("deep recursion
was detected at 'interpreter'"), failing both required checks on the first CI
run of any PQ1-era commit. Windows reserves a larger stack, so local gates
never saw it. ci.yml and reproduce_artifact.sh now set a 1 GiB limit first
(measured to work under WSL). WDD-20260920-INT-002.
Co-Authored-By: Claude Fable 5.1 <[email protected]>
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.
Promote the accepted post-PQ1 integration checkpoint after its required Linux checks pass. This brings the reviewed PRE, native execution, lower-bound, bitvector and compiler work already on
claude/integrate-post-pq1-extensionsonto main. The separate, unaccepted lifecycle campaign is excluded.The integration at bf31f98 failed Linux compilation of Construction.Proof.Constants. A clean Ubuntu 24.04 reproduction on pinned Lean 4.22.0 identified a worker-thread stack overflow even with the existing 1 GiB OS stack setup. The new repair commit c9e26d2 sets Lake's worker stack to 64 MiB and retains the full bounded PRE warm-up output on failure. Theorem sources, trust settings, mutation registries and acceptance predicates are unchanged.
Validation so far: all 121 incoming non-merge commits and the new repair commit pass strict per-commit design certification; TOML parsing, PowerShell syntax and whitespace checks pass. The earlier accepted checkpoint has a recorded Windows aggregate pass. The new candidate's Linux
Lean gateandReproduce artifactchecks remain required and pending; this PR must not bypass protection. The local focused stack experiment is queued behind the shared native build slot. No new Linux success is claimed before those results.