Repository navigation
docs(proofs): record the CI receipts of THY-1; it derives PWG-1 (WO 1.4) - #66
Conversation
The proof lanes passed on main for the first time: run 42896264290, job 130110238086, commit 3367689, inside the pinned Guix (8edb9da). For each THY-1 witness the log records the checker and its version (Agda 2.7.0.1, Rocq 8.18.0, Lean 4.29.0), the invocation, the SHA-256 of the file (equal to the recorded digests), the result (PASS) and the axioms reported (none; the Agda cone is Agda.Primitive and FeatureReachability). The planted controls failed the gate in the same run. - verification/receipts/theory_praxis.deed: the three CI receipts are current at source commit 3367689; the local runs of 2026-11-09 stay as superseded receipts with their reasons. The canon reader (standards be39f90) derives PWG-1, and refuses PWG-1 when one receipt names another commit. Agda 2.7.0.1 postulates the same four Agda.Primitive names, so the trusted base is unchanged. - PROOF-STATUS.adoc: each leg names its CI receipt; the grade row reads PWG-1 since 2026-11-10, and says the grade drops when a later commit breaks a leg (PROOF-POLICY 8.4). - ROADMAP.adoc: the lanes pass, with the run, the toolchain time (22 to 35 minutes) and the third finding, the Guix agda store defect. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZnDRsCLfZcFcEzvPcM
|
Caution Review failedThe pull request is closed. Walkthrough
Merge Risk:
 |
|
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
Summary
The last step of work order 1.4. The proof lanes passed on
mainfor the first time: run 42896264290 (job 130110238086), commit336768958d01, inside the pinned Guix (8edb9da). That run gives THY-1 a CI receipt for each witness, and the canon reader now derivesPWG-1.What the run recorded, per THY-1 witness
4e39d6ae…(= recorded)Agda.Primitive,FeatureReachabilitye2f90043…(= recorded)absent_under_all_featuresclosed under the global context4158e54f…(= recorded)The planted controls failed the gate in the same run.
Changes
verification/receipts/theory_praxis.deed: the three CI receipts are current at source commit336768958d01. The local runs of 2026-11-09 stay as superseded receipts, with reasons.be39f90) derivesPWG-1.PWG-1when one receipt names another commit; I tested that tamper case.Agda.Primitivenames, so the trusted base is unchanged.docs/status/PROOF-STATUS.adoc: each leg names its CI receipt. The grade row readsPWG-1since 2026-11-10, and says that the grade drops when a later commit breaks a leg (§8.4).docs/status/ROADMAP.adoc: the lanes pass. It records the run, the toolchain time (22 to 35 minutes) and the third finding, the Guixagdastore defect.Testing
PWG-1.asciidoctor --failure-level=WARNon both documents: no warnings.just validate-repo-map: up to date.Generated by Claude Code
Summary by CodeRabbit
PWG-1grade, replacing the previousPWG-2iistatus for current CI receipts.mainCI run passed the Agda, Rocq, and Lean proof checks, with unchanged file digests and clean axiom reports.