[ALL] DOCS: refresh NEXT_SESSION handoff — verified baseline, Rocq 9.1.1 fix, corpus-gap pickup - #54
Draft
ib823 wants to merge 1 commit into
Draft
[ALL] DOCS: refresh NEXT_SESSION handoff — verified baseline, Rocq 9.1.1 fix, corpus-gap pickup#54ib823 wants to merge 1 commit into
ib823 wants to merge 1 commit into
Conversation
…1.1 fix, corpus-gap pickup Makes the session bootstrap actually usable after the 2026-08-02 audit, and fixes the drift the audit found in this very file. STEP 2 — corrected Rocq 9.2 -> 9.1.1 (FINDING 3). The old block was wrong in three ways: version, switch package (ocaml-system.4.14.1 -> ocaml-base-compiler .4.14.2), and it omitted --disable-sandboxing, without which opam init fails in an unprivileged container. Replaced with the exact sequence run and verified end-to-end this session (built all 328 files). Records the ~25 min provisioning cost against a ~2m15s build, since that ratio is the main reason to prefer a persistent environment. STEP 3 — replaced the unverifiable baseline with measured values at a5ee2ce: 2912/0 proto, 304/0 tooling, 328/328 Coq files, Qed 12,626 / 0 / 0 / 0 / 30, corpus 64 pass of 165, 4 (not 2) expected audit-docs warnings. Flags that `--all-targets` clippy is NOT clean (FINDING 2) so the next session does not trust a claim this file used to make. Notes the 180 "Closed under the global context" reports as the strongest evidence in the repo. Adds the SBOM drift check, which was missing. STEP 4 — leads with the audit's structural conclusion: Gate C is budget-blocked on the owner-deferred REQ-28, and every other gate's remaining blocker is external too, so "close the gates" is not a viable plan. Points instead at the corpus gap with the measured failure-class breakdown (70% parse-level, 15% REQ-44(b) forward references, together 85%) and records that the forward-ref half is Rust-only, not Coq-blocked. Also notes CI is green as of a5ee2ce and that no in-repo gate checks CI status -- the blind spot that let it stay red for 8+ pushes. audit-docs.sh: exit 0, 0 discrepancies, 4 expected warnings. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016qQCunxB3dDkhDzdmKoEmU
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
Follow-up to #53 (merged as
a5ee2ce). MakesNEXT_SESSION.mdusable for a fresh session, and fixes the drift the audit found in this very file.Docs only — no code, no workflow, no proof changes.
Changes
STEP 2 — Rocq provisioning corrected (FINDING 3). The old block was wrong in three ways: it said 9.2 (the Makefile header, CLAUDE.md and the CI job name all say 9.1.1), it used
ocaml-system.4.14.1instead ofocaml-base-compiler.4.14.2, and it omitted--disable-sandboxing, without whichopam initfails in an unprivileged container. Replaced with the exact sequence run end-to-end this session — the one that built all 328 files. Also records the ~25 min provisioning cost against a ~2m15s build, since that ratio is the main argument for a persistent environment.STEP 3 — baseline replaced with measured values at
a5ee2ce: 2912/0 proto, 304/0 tooling, 328/328 Coq files, Qed 12,626 / Admitted 0 / Abort 0 / Axiom 0 / Parameter 30, corpus 64 of 165 passing, and 4 (not 2) expectedaudit-docs.shwarnings. Adds the SBOM drift check, which was missing entirely.Two corrections that matter for the next session's trust:
cargo clippy --all-targetsis NOT clean (FINDING 2) — this file previously asserted it was. The enforced form is plaincargo clippy, which does pass.Print Assumptionsreports, all "Closed under the global context" as the strongest evidence in the repo — kernel-level axiom-freedom, not a grep.STEP 4 — leads with the audit's structural conclusion. Gate C's only open exit criterion is REQ-28, the external crypto audit, deferred by the owner on 2026-06-10. Every other gate's remaining blocker is external too. So a plan framed as "close the gates" stalls immediately. Points instead at the corpus gap with the measured failure-class breakdown — 70% parse-level, 15% REQ-44(b) forward references, 85% together — and records that the forward-ref half is Rust-only, not Coq-blocked, because the core Coq calculus has no recursion constructor to widen and
foundations/RecursionSafety.valready mechanizes the rule.Also notes CI is green as of
a5ee2ce, and that no in-repo gate checks CI status — the blind spot that let it stay red for 8+ pushes.Type
.riifileTesting
scripts/audit-docs.sh→ exit 0, 0 discrepancies, 4 expected warningscargo test --all— n/a, no code changedcargo clippy -- -D warnings— n/a, no code changedChecklist
unsafewithout justification — no code changedAdmittedin Coq proofs — no proofs changedNote
The branch was restarted from
mainafter #53 merged, per the merged-PR protocol, so this is a new PR rather than a reopen. The force-with-lease push replaced only already-merged history.Generated by Claude Code