Repository navigation
docs(proofs): record what the active Agda CNO/OND terms actually state - #197
Open
hyperpolymath wants to merge 1 commit into
Open
hyperpolymath wants to merge 1 commit into
hyperpolymath wants to merge 1 commit into
Conversation
A statement-level review (2026-11-09) found that several claims in the ledger and docs say more than the active Agda proves. This commit changes labels and prose only; no proof term changes. - IsCNO is degenerate: state-eq includes the program counter, which every instruction except Halt moves, so cno-identity holds only for Halt-only programs. The archived Coq fixed this on 2026-05-18; the Agda did not. - terminates and thermodynamically-reversible hold by construction for every program (eval is total; energy-dissipated is constantly zero). - The Agda OND-5 (under O-out) and the archived Coq/Lean OND-5 (under O_all) are different propositions; correspondence is unassessed. - The OND-3 anchoring to is_CNO exists only in the archived Coq. - Grades now follow PROOF-POLICY §8 (PWG). The Agda proofs are `proven` but `ungraded` until a PWG-3 receipt is recorded; the superseded "Grade 3" label is removed. - Flags the unverified "z3 5.3.3" receipt version and corrects EXPLAINME's description of the active prover stack. All four modules recheck cold under `agda --safe --without-K --cubical-compatible` (Agda 2.6.3, stdlib 2.3, local, not a CI receipt). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
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 51 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. |
This was referenced Nov 9, 2026
hyperpolymath
marked this pull request as ready for review
November 9, 2026 15:52
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 23:31
hyperpolymath
added a commit
that referenced
this pull request
Nov 10, 2026
Stacked on #197 (the claims audit). Merge that first; this PR then shows only its own commit, `d8abb02`. ## Why The 2026-11-09 design audit found the active Agda `IsCNO` degenerate: - `state-eq` compares the program counter, and `step` advances it, so only `Halt`-only programs were CNOs. - `terminates` held for every program because `eval` is a total fold over the list. `Jump` did not change control flow. - `energy-dissipated` was constantly zero, so `cno-reversible` held for every program. ## What changes in `proofs/agda/CNO.agda` - **A pc-driven machine.** The big-step relation `_⊢_⇓_` stops when the pc runs off the end or hits `Halt`. The fuel interpreter `run` agrees with it in both directions (`run-sound`, `run-complete`). A Store or Add on a missing register faults: no normal stop. The machine is deterministic (`⇓-det`). - **`obs-eq`.** Memory, registers and I/O. `state-eq` is kept as full equality. - **`IsCNO p`.** From every state, started at pc 0, the machine stops normally, and every normal stop is `obs-eq` to the start. Purity (`cno-pure-thm`) and observational reversibility (`cno-left-inverse`) are derived, not assumed. The constant energy model and the unused `reversible` are removed; nothing thermodynamic is claimed here. - **Composition.** `seq-comp` relocates the second program's jumps. `cno-composition` needs `Closed p₁` (no jump past `p₁`'s end). `closedness-needed` is a checked counterexample showing the condition cannot be dropped. - **Witnesses for and against.** - `nop-is-cno`, `jump-exit-is-cno` and `nop-nop-is-cno`: the class is not Halt-only. - `load-not-cno`: the class is not everything. - `jump-self-diverges`: termination is not automatic. `EchoBridgeCNO.agda` is restated over `cno-result` and `obs-eq`. The `≡` form is on the observable projection `observe`, and `program-state-model` is a `CNOModel` over observable states. ## Strict flags All four modules now declare `--safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness`. The CI job runs each module with the PROOF-POLICY §2.1 invocation plus `--double-check -W error -W noUnsupportedIndexedMatch`. The earlier `Add` overlap that `--exact-split` rejected is gone, because Store and Add now dispatch through `store-at` and `add-at`. ## Checks run locally | Toolchain | CNO | OND | EchoBridgeScaffold | EchoBridgeCNO | |---|---|---|---|---| | Agda 2.6.3 + stdlib v1.7.3 (as CI) | pass | pass | pass | pass | | Agda 2.7.0.1 + stdlib 2.3, cold (`--ignore-interfaces`) | pass | pass | pass | pass | `scripts/check-proof-patterns.sh`, `tests/check-proof-patterns.sh` and `scripts/check-adoc-tables.sh` on the edited docs all pass. No postulates, no escape pragmas. ## Docs The `PROOF-STATUS.adoc` audit rows are marked resolved, with the original findings kept as history. README, EXPLAINME, GLOSSARY, TWO-PILLARS and `proofs/agda/README.adoc` are updated to match. ## Downstream hyperpolymath/echo-types pins absolute-zero at `f486c29`, so nothing breaks now. Its CNO modules (`EchoCNOBridge`, `EchoCNOSemantics`, `EchoCNOPackaging`, `EchoThermodynamicsArbitrary`) will need adapting when it repins. ## Not touched The `CNO.agda` header still says `License: AGPL-3.0 / Palimpsest 0.5`. AGPL is on the estate deny list, but licence edits are owner-only, so it is left as it is. --- _Generated by [Claude Code](https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV)_ <!-- This is an auto-generated comment: release notes by coderabbit.ai --> <!-- coderabbit-ai-generated:v1 --> ## Summary by CodeRabbit * **Formalization Updates** * The active Agda proofs now model program-counter-driven execution, normal termination, and observable state preservation. The documented CNO claims no longer include a thermodynamic guarantee. * Added examples covering sequential composition and programs that fail to meet CNO conditions. * **Verification** * Agda checks now apply stricter validation. Z3 checks remain bounded and are marked tested-only. * **Documentation** * Proof statuses now use Proof Witness Grades: active Agda proofs are ungraded pending a receipt, and OND-6 remains open. Archived prover work is distinguished from active checks. <!-- end of auto-generated comment: release notes by coderabbit.ai --> --------- Co-authored-by: Claude <noreply@anthropic.com> Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
hyperpolymath
added a commit
to hyperpolymath/echo-types
that referenced
this pull request
Nov 10, 2026
## Summary A statement-level review (2026-11-09) compared PROOF-STATUS, the `Smoke.agda` comments and module headers with the Agda statements they describe. This PR changes **comments, ledger text and labels only**. No proof term changes, and every theorem name and Smoke pin is kept. Strengthening the thin results is a separate follow-up. **Vacuous or hypothesis-restating results, now labelled as such:** | Result | What it states | |---|---| | `bennett-reversible-arbitrary` | The `inj` hypothesis is unused; the cost is 0 for **every** `f`, because occupancy is 0 or 1 and ⌊log₂⌋ of either is 0. | | `partial-deniable-restricted` | `= const`: the theorem restates its hypothesis. | | `measure-not-injective` | Conditional on the measure already agreeing on two distinct echoes; it does not show every measure is lossy. | **Overclaims corrected:** - PROOF-STATUS "Pillars A–D COMPLETE" restated claims that R-2026-05-18 withdrew: graded-comonad laws, the terminal-cone universal property, model-independence, and the conservativity metatheorem. - `EchoAbstractionBarrier` claimed a guarantee, but there is no enforced barrier: `Echo` is a transparent Σ. - `EchoEntropy`'s "blind" results hold by construction (the shadow is constant). - `EchoLLEncoding` holds only for encodings whose linear carrier is a proposition. - F5 proves that a comparison iso exists, not that it is unique, and its lifting uses only that one leg is an equivalence. - The EchoVariance/F1 Smoke comments overclaimed: there is no graded monad and no adjunction, and F1 is a lossless writer that does not mention Echo. - `EchoProvenance`'s Echo-vs-Σ clearance claim does not hold. - `ImageFactorizationProp` is conditional on a `TruncInterface` that the `--safe` build does not supply. **Stale text fixed:** - the nonexistent names `const-fibre-↔-domain` and `aggregate-non-injective`; - "F5-3 remains the final open slice"; - the "scaffold" labels in `All.agda`; - σ–π "set equality", which is actually ⇔; - the CNO module list in MAP.adoc. PROOF-STATUS gains a "Design audit (2026-11-09)" table. It also records that every theorem is `ungraded` under PROOF-POLICY §8: no PWG-3 receipt is in the repo and no Rocq/Lean leg exists. ## Verification (local, not CI receipts) Run with the pinned toolchain from `scripts/setup-agda.sh`: Agda 2.7.0.1, stdlib `8326c74`, absolute-zero `f486c29`. - `All`, `Smoke` and `AuditSmoke` compile under `--safe --without-K --cubical-compatible`. - `kernel-guard.sh`, `check-agda-invocations.sh`, `check-no-unsafe.sh` and `tools/check-guardrails.sh` pass. - Earlier today, all eight CI entrypoints of `main` passed cold on the same toolchain. ## Related hyperpolymath/absolute-zero#197 records that the active Agda `IsCNO` is degenerate. That affects every CNO-facing result here (`EchoCNOBridge`, `EchoCNOSemantics`, `EchoCNOPackaging`, `EchoThermodynamicsArbitrary`). --- _Generated by [Claude Code](https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV)_ Co-authored-by: Claude <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
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
A statement-level review of
proofs/agda/(2026-11-09) found that the ledger and docs claim more than the active Agda proves. This PR corrects the labels and prose only. No proof term changes. The redesign of the CNO definition is a separate follow-up.IsCNOstate-eqincludesstate-pc, and every instruction exceptHaltmoves the PC, socno-identityholds only forHalt-only programs. The archived Coq fixed this on 2026-05-18; the active Agda did not.provenabout that class only.terminates∃ s′. eval p s ≡ s′, inhabited by(eval p s , refl)thermodynamically-reversibleenergy-dissipated _ _ _ = zeroO-out, Coq/Lean underO_allunassessedis_CNOOND.agdanever importsCNOproven,ungradeduntil a PWG-3 receipt is recordedAlso:
z3 5.3.3receipt version as unverified, since the file also records 4.16.0 elsewhere;IsCNOdefinition (comment only).Verification
All four modules recheck cold under
agda --safe --without-K --cubical-compatible, using Agda 2.6.3 with agda-stdlib 2.3. This was a local run, not a CI receipt.Follow-ups (not in this PR)
state-eqwithout the PC.IsCNO.--cubical-compatible.Generated by Claude Code