Repository navigation
proofs: scope vacuous Agda CNO fields, fix archived PROOF-STATUS paths, pin stdlib, make OND-3 writer Z3 check real - #198
Open
hyperpolymath wants to merge 2 commits into
Open
hyperpolymath wants to merge 2 commits into
hyperpolymath wants to merge 2 commits into
Conversation
…dlib, make OND-3 writer check real - CNO.agda (comments only): `terminates` is definitional (eval is total over a finite list, so every program "terminates") and `energy-dissipated` is the constant 0, so `thermodynamically-reversible` holds for every program. Say what they do and do not establish beside the definitions and on IsCNO. - PROOF-STATUS.adoc: new "Scope of the Agda CNO fields" section; rows and sections that pointed at proofs/coq, proofs/lean4, proofs/isabelle, proofs/mizar and proofs/verify-all-provers.sh now point at archive/proofs/ and are marked ARCHIVED instead of VERIFIED; 2026-11-09 receipts (z3 4.8.12, Agda 2.6.3 incl. --cubical-compatible); escape the `|` that split a table row. - scripts/provision-agda-stdlib.sh: register agda-stdlib v1.7.3 pinned to commit 0817da68 (fails if the tag moves); used by CI's agda job, the Justfile (`just provision-agda-stdlib`) and named in verify-active-provers.sh. - OND_checks.smt2: the OND-3 dir 2 block asserted (not (and (= 0 0) (= 1 1))), unsat for any program. It now computes the writer's O_all observable from a modelled writer_step/inj (per OND.v), plus a leaking-writer control (sat) and a writer_not_null witness (sat). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY
Contributor
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 58 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. |
…ive gate
Follow-up to the PROOF-STATUS.adoc reconciliation in this PR. Docs that state
current facts now cite archive/proofs/{coq,lean4,isabelle,mizar}/... and
archive/proofs/verify-all-provers.six-prover.sh instead of the removed
proofs/... paths, and say "archived" / past tense where they claimed those
provers are currently built, verified or CI-gated. The active gate is named as
proofs/verify-active-provers.sh (Agda + Z3 bounded + Idris 2 ABI).
- README, EXPLAINME, ROADMAP: layout rows, evidence pointers, "what verifies"
receipts and the CI row.
- docs/proof-debt.adoc: ledger file pointers moved to archive/proofs/, with an
archive note in the status banner.
- docs/COOKBOOK.adoc, ECHIDNA.adoc: archive notice; input paths moved.
- docs/JUSTFILE-COOKBOOK.adoc: build-all matches the Justfile; build-coq,
build-lean and verify-coq marked historical; clean-coq/clean-lean paths
match the Justfile.
- docs/OND-PILLAR-STRUCTURE.adoc, OND-ROADMAP, ECOSYSTEM-CONNECTIONS,
MACHINE_VERIFICATION, VERIFICATION_RESULTS: status text and commands.
- docs/wiki: Architecture data flow, Verification, Proof-Systems, Home,
Roadmap, Audit-Trail.
Dated records (CHANGELOG, AUDIT resolved items, docs/archive/*, session notes,
historical plans) are left as written. No proof file changed.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY
hyperpolymath
marked this pull request as ready for review
November 9, 2026 15:45
Codex Review Summary: ❌ FailedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
hyperpolymath
enabled auto-merge (squash)
November 9, 2026 22:53
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
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
This PR acts on the absolute-zero items in the ephapax v2 survey's cross-repo action list, plus one Z3 finding.
proofs/agda/CNO.agda,terminatesholds by definition:evalis total over a finite list, so(eval p s , refl)inhabits it for every program.energy-dissipated _ _ _ = zero, sothermodynamically-reversibleholds for every program byrefl. The notes beside the definitions and onIsCNOnow say what these fields establish and what they do not. They also record thatIsCNOnever uses the non-trivialreversiblepredicate, and thatcno-identityis the only field that constrains a program. PROOF-STATUS gains a new section, "Scope of the Agda CNO fields".proofs/coqandproofs/verify-all-provers.shno longer exist. Rows and sections now point atarchive/proofs/{coq,lean4,isabelle,mizar}andarchive/proofs/verify-all-provers.six-prover.sh. The Coq, Lean 4, Isabelle/HOL and Mizar headings change from "VERIFIED (this environment)" to "ARCHIVED (historical receipt)", and claims that they are CI-gated now read as past tense. A pre-existing unescaped|in the Z3 table row (sat|unsat) split the canonical table:scripts/check-adoc-tables.shfailed onmainand now passes.scripts/provision-agda-stdlib.shclones agda-stdlibv1.7.3. It fails unless the tag resolves to the pinned commit0817da6877aa045932221134913d8511caa78d97. It then renames the manifest tostandard-libraryand writes$AGDA_DIR/{libraries,defaults}. The CIagdajob now runs this script in place of its inline steps. The script is also thejust provision-agda-stdlibrecipe and is named inverify-active-provers.sh.(not (and (= 0 0) (= 1 1))), which is unsat for any program. It now modelswriter_opperOND.v: memory as an array,inj,writer_step = store m 0 7, time 1, with theO_allobservable computed from them. That check returnsunsat. A control with a leaking writer returnssat, and awriter_not_nullwitness returnssat. Ifwriter_stepis mutated to leak, the main verdict flips tosat.Checks run (actual output)
z3 proofs/z3/ond/OND_checks.smt2(Z3 4.8.12):sat unsat sat sat sat, exit 0.bash proofs/z3/verify.sh:Z3-CHECK OK(5 verdicts match).AGDA_DIR:--safe --without-K: CNO, OND, EchoBridgeScaffold and EchoBridgeCNO each exit 0.--safe --without-K --cubical-compatible: all four exit 0.bash proofs/tests/gate-selftest.sh:GATE-SELFTEST OK: 27/27.bash scripts/check-proof-patterns.sh: OK.bash scripts/check-adoc-tables.sh PROOF-STATUS.adoc: OK.Not done (follow-ups)
docs/*,docs/wiki/*) still citeproofs/coqandverify-all-provers.sh. This PR fixes PROOF-STATUS only.--cubical-compatible.License:line in theCNO.agdaheader comment was left untouched (licence edits are owner-only).Follow-up commit 37c792a: archived-path sweep in the other docs
This commit picks up the "many other docs" follow-up above. It changes documentation only: no proof file, script or workflow.
Docs that state current facts now cite
archive/proofs/{coq,lean4,isabelle,mizar}/…andarchive/proofs/verify-all-provers.six-prover.shin place of the removedproofs/…paths. Where a doc claimed those provers are built, verified or CI-gated now, it says "archived" or uses the past tense, worded the way PROOF-STATUS is. The active gate is named asproofs/verify-active-provers.sh(Agda + Z3 bounded + Idris 2 ABI). CI is described as theagda,z3andidrisjobs inproofs.yml.Files changed (18):
README.adoc,EXPLAINME.adoc,ROADMAP.adoc: layout rows, evidence pointers, the "What genuinely verifies" receipts (now labelled as 2026-07-07 receipts) and the CI row.docs/proof-debt.adoc: ledger file pointers now go toarchive/proofs/, and the status banner has an archive note.docs/COOKBOOK.adoc,ECHIDNA.adoc: archive notice added; input paths moved.docs/JUSTFILE-COOKBOOK.adoc:build-allnow matches the Justfile (Agda + Idris).build-coq,build-leanandverify-coqare marked historical because the Justfile no longer has them. Theclean-coq/clean-leanpaths now match the Justfile.docs/OND-PILLAR-STRUCTURE.adoc,docs/OND-ROADMAP.adoc,docs/ECOSYSTEM-CONNECTIONS.adoc,docs/MACHINE_VERIFICATION.adoc,docs/VERIFICATION_RESULTS.adoc: status text and commands.docs/wiki/{Architecture,Verification,Proof-Systems,Home,Roadmap,Audit-Trail}.md.References left on purpose:
CHANGELOG.adoc, the resolved items inAUDIT.adoc,docs/archive/*,docs/PROOF-INSIGHTS.adoc(session note, 2026-02-05),docs/PROOF-COMPLETION-PLAN.adoc(historical plan),docs/proof-debt-triage.adoc(self-described historical triage),docs/PROOF-CLASSIFICATION.adoc(pre-completion classification) and the historical sample output in the two cookbooks.docs/OND-PILLAR-STRUCTURE.adoclayout tables: these are the original design sketch, and several of their paths exist in neitherproofs/norarchive/proofs/. The status banner now says this rather than rewriting the tables.docs/CLAUDE.adoc: itsproofs/coqreferences describe the separate GitLab repository.docs/COOKBOOK.adoc"Adding a New Language" (proofs/coq/mylang/…), and the ECHIDNA plan's output paths (proofs/coq-completed/,proofs/lean4/CNO_translated.lean).proofs/verify-all-provers.sh(now archived asarchive/proofs/verify-all-provers.six-prover.sh)".Checks (actual output):
test -e). The only old paths left in added lines are the "old name → new name" phrasings.bash scripts/check-adoc-tables.shon the 12 touched.adocfiles: 11 OK.EXPLAINME.adoc:134: unterminated table blockalso fails on the base commit: the file ends in|===abc def ghi …. That line is not touched here.asciidoctor -won the 12 touched.adocfiles: the same 6 warnings/errors before and after the change (identical once line numbers are normalised). They are the EXPLAINME table above, two "table missing leading separator" errors in README, and the missingpygments.rbgem.Found but not changed (outside a docs-only sweep):
verification/run-local-verification.shandverification/setup-and-verify.shstill runcoqc,lakeandisabelleagainstproofs/coq,proofs/lean4andproofs/isabelle.proofs/z3/cno_properties.smt2. That file was not moved to the archive; it no longer exists (proofs/z3/verify.shnotes it was dropped on 2026-09-23).Generated by Claude Code
🤖 Generated with Claude Code
https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY