Repository navigation
docs(proofs): align README, AFFIRMATION and EXPLAINME with the proof ledger; Agda-first convergence plan - #1030
Conversation
…ledger; Agda-first convergence plan
Second PR of the proof-ledger stack (owner decisions 2026-11-09).
- EXPLAINME.adoc moves back to the repository root, as README-EXPLAINME
requires. Every claim in it was re-checked against the tree.
- Removed: "Idris2 proofs verify recipe correctness"; "Haskell Liquid
types"; a nonexistent proofs/agda/ row.
- Corrected: 5 networks is now 8; 7 Zig exports is now 18.
- Volatile metrics give way to the mix tasks that compute them.
- The safety systems are now described as built but not wired.
- It gains [[proof-ledger]], which cites the canonical ledger.
- README's own overclaims are recorded under Known gaps; fixing them is
a follow-up.
- README's proof bullet now describes what is proved, over models not the
runtime, and quotes the ledger census. AFFIRMATION drops "blocked only on
Mathlib network access" (PROOF-POLICY forbids Mathlib) and fixes a dead
.md link.
- scripts/proof-ledger.sh claims: every census README, AFFIRMATION or
EXPLAINME quotes must equal the ledger's computed census. It runs in CI,
with 4 contracts built from the ledger itself.
- The neural-convergence handover is rewritten: Agda first (2.8.0.2,
--safe --without-K --cubical-compatible) over constructive Bishop reals
built on agda-stdlib v2.3 (8326c74), milestones M0-M5, no Mathlib. The
stdlib feasibility was spiked locally under the profile. The ESN is
framed in the induced infinity-norm the runtime actually uses.
- docs/proofs/needs.adoc becomes a pointer to the ledger; its own list had
drifted ("Agda retired", Mathlib).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CYR5bf5FBLS7cXQK72aVNM
|
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 55 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. |
…ger-wright-zwwbe2-proof-claims # Conflicts: # tests/proof-ledger-test.sh
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. |
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3a483e99e7
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| [ -f "$doc" ] || continue | ||
| found=$(tr '\n' ' ' < "$doc" | tr -s ' ' | grep -oE '[0-9]+ proven of [0-9]+(; [0-9]+ proven-with-postulates, [0-9]+ tested-only, [0-9]+ argued, [0-9]+ open\.?)?' || true) |
There was a problem hiding this comment.
The new proof-status workflow invokes claims with the default document list, but missing files are silently skipped and there is no assertion that each file contributed a census. Consequently, deleting or renaming EXPLAINME.adoc, or merely removing/reformatting all census text in any designated document, still exits successfully—even PROOF_CLAIM_DOCS=/nonexistent reports that zero censuses agree. Require every configured document to exist and yield the expected census before this CI gate passes.
Useful? React with 👍 / 👎.
| * The runtime uses IEEE floats. The theorems are about reals; the link from | ||
| them to `+lib/neural/*.ex+` is the `+models-runtime-refinement+` row, and | ||
| `+test/neural_test.exs+` is that row's evidence, which is `+tested-only+`. |
There was a problem hiding this comment.
At this commit, the canonical models-runtime-refinement ledger row has status open, file -, and no evidence names; test/neural_test.exs belongs to no such row. Calling that test this row's evidence and labeling the row tested-only directly contradicts the ledger this documentation tells implementers to follow, and can make the outstanding model-to-runtime correspondence work appear complete.
Useful? React with 👍 / 👎.
| `/api/*` needs a bearer token only when `HYPATIA_API_BEARER_TOKEN` is set; | ||
| otherwise it is loopback-only. |
There was a problem hiding this comment.
When HYPATIA_API_BEARER_TOKEN is unset but HYPATIA_API_ALLOW_NONLOCAL=true, Hypatia.Web.ApiRouter.legacy_loopback_only/2 explicitly permits non-loopback requests without a token. Therefore the API is not always loopback-only in the stated “otherwise” case; omitting this exception can lead operators to expose operational endpoints while believing the documented IP restriction still applies.
Useful? React with 👍 / 👎.
| M3 — PageRank (`+PageRank.agda+`):: | ||
| `+G(x) = α·P·x + (1 - α)·v+` with `+P+` column-stochastic (non-negative | ||
| rational entries, columns summing to 1) and a rational `+0 ≤ α < 1+`. | ||
| `+G+` is an ℓ¹ contraction with modulus `+α+`, because a column-stochastic | ||
| `+P+` gives `+‖P x‖₁ ≤ ‖x‖₁+`. Then M2. *Ledger:* `+pagerank-convergence+` |
There was a problem hiding this comment.
For repeated successful outcomes between the same identities, build_edges/1 emits parallel edges, while iterate_trust/4 adds every duplicate to out_weight_sum but uses Enum.find to include only one matching edge in each target's numerator. The resulting runtime transition matrix can therefore be sub-stochastic rather than column-stochastic, so the proposed M3 theorem's exact-column-sum premise excludes a normal runtime input and cannot establish the stated obligation for graph_of_trust.ex; either model the sub-stochastic case or deduplicate the runtime edges.
Useful? React with 👍 / 👎.
Merges b2b23e5 (computed grades, PROOF-POLICY pin, check hardening). The one conflict is in scripts/proof-ledger.sh, where both branches added a function: claims() here and markers_ok() there. Both are kept. It also fixes Codex's four findings on 3a483e9: - `claims`: a claim document that does not exist, or quotes no census, now fails. It was skipped silently, so a renamed EXPLAINME passed. Two new contracts; 40/40 pass. - HANDOVER M3 is stated for a column-sub-stochastic P (each column sums to at most 1). ||Px||_1 <= ||x||_1 still holds, so the contraction argument is unchanged, and it covers the matrices the runtime builds: - dangling nodes give zero columns; - iterate_trust/4 sums parallel edges into the out-weight but takes one of them into each target, so repeated outcomes leak mass. The leak is named as a runtime defect to fix in the runtime. - HANDOVER: models-runtime-refinement is open and names no evidence; test/neural_test.exs is a candidate, not that row's recorded evidence. - EXPLAINME: /api needs a bearer token when HYPATIA_API_BEARER_TOKEN is set and not empty. Otherwise only loopback clients are answered, unless HYPATIA_API_ALLOW_NONLOCAL=true. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CYR5bf5FBLS7cXQK72aVNM
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
|
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: fd96af78ef
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| ∞-norm, *not* the spectral radius: the runtime has scaled by the induced | ||
| ∞-norm (`+@reservoir_norm+` = 0.95) since 2026-10, and `+test/neural_test.exs+` | ||
| checks both that bound and the convergence of two initial states. | ||
| *Ledger:* `+esn-echo-state+` becomes `+proven+` at PWG-3. |
There was a problem hiding this comment.
If the milestones land independently as prescribed, M4 proves only a theorem parameterized by an activation already known to be 1-Lipschitz and bounded, while M5 explicitly defers proving those premises for the runtime's :math.tanh activation. Marking esn-echo-state proven after M4 would therefore overstate the current unconditional ledger obligation; either keep the row open until M5 lands or change the obligation to record the activation premises and track the runtime instantiation separately.
Useful? React with 👍 / 👎.
| Safety systems are built but not wired. `Safety.RateLimiter` and | ||
| `Safety.Quarantine` have no caller in `lib/`. `BatchRollback.rollback/2` is |
There was a problem hiding this comment.
In the inspected tree, lib/hypatia/web/api_router.ex:90-92 and lib/hypatia/web/graphql.ex:191-193 call the Quarantine GenServer, so the new claim that it has no caller in lib/ is false. It is still not consulted by scan or dispatch enforcement, which is the actual gap; state that narrower condition so maintainers do not overlook the existing API and GraphQL integration.
Useful? React with 👍 / 👎.
| [cols="1,2", options="header"] | ||
| |=== | ||
| | README row | Tree | ||
| | `lib/`: 133 | 154 `.ex` files (`+ls lib/**/*.ex \| wc -l+`), 180 `defmodule` |
There was a problem hiding this comment.
With Bash's default globstar setting disabled, the shown ls lib/**/*.ex | wc -l command expands only files exactly one directory below lib/ and reports 101 here, not the stated 154; it omits both top-level files and deeper subdirectories. Because this section says its counts are reproducible with the commands shown, use find lib -name '*.ex' (or explicitly enable globstar) so future audits do not derive a false module count.
Useful? React with 👍 / 👎.
…dger rows now proven (#1031) ## Summary This is the third PR of the proof-ledger stack, based on #1030 (which is based on #1029). The owner decided on 2026-11-09 to **re-home the Lean engineering proofs to Idris2 now** (PROOF-POLICY §3), rather than record Lean's kernel axioms as necessary. - **New Idris2 files:** `verification/proofs/idris2/` gains `RateLimiting`, `BayesianUpdate`, `ParserTotality`, `PageRankInvariants` and `ESNSpectralScaling`. - They port the Lean files theorem for theorem, with names in camelCase. - Every file is under `%default total`, with no `believe_me`, `assert_total` or holes. - The existing per-file `idris2 --check` loop picks them up; no new CI is needed. - **Why the axioms go away:** four of the Lean files rested on `propext`, or on `propext` + `Quot.sound` (from `Lean.collectAxioms`, see #1029). Idris2 has neither. - **Ledger rows renamed:** | Old id | New id | |---|---| | `lean-rate-limiting` | `rate-limiting` | | `lean-bayesian-update` | `bayesian-update` | | `lean-parser-totality` | `parser-totality` | | `lean-pagerank-preconditions` | `pagerank-preconditions` | | `lean-esn-preconditions` | `esn-preconditions` | All five are **`proven`**. **Census: 22 proven of 42; 0 proven-with-postulates, 11 tested-only, 2 argued, 7 open.** - **Lean project removed:** `verification/proofs/lean4/` is deleted. The `lake build` job becomes **`Lean hole re-check (HYP-01 control)`**: the pinned Lean stays for the verdict fixture only. The job is not a required check (rules on `main` require `abi-codegen-drift`, `zig build test`, `Escript packaging soundness`, `scan / gitleaks`). - **Claims updated:** README, AFFIRMATION, EXPLAINME, PROOF-STATUS and `needs.adoc` describe the move. The `claims` gate from #1030 caught all four stale census quotes first, so the derived-claims check works end to end. - **Contract fix:** the ledger contracts now refuse a mutant whose target row is missing. I hit this in practice: the old axiom contracts targeted the renamed `lean-*` ids, so they would have mutated nothing and still passed. ## How has this been verified? Local receipt, Idris2 **0.7.0** built from source with Chez Scheme (the same version CI pins): | Check | Result | |---|---| | `idris2 --check` on all 12 `verification/proofs/idris2/*.idr` | 12/12 ok | | `idris2 --build src/abi/hypatia-abi.ipkg`, `verify/hypatia-verify.ipkg` | exit 0, exit 0 | | `scripts/check-verdicts.sh` | PASS: 2 positive controls, 5 expected rejections | | `scripts/check-trusted-base.sh` | OK | | `proof-ledger.sh check` / `render --check` / `claims` | valid / current / 4 censuses agree | | `tests/proof-ledger-test.sh` | 19 passed, 0 failed; a planted missing target makes it fail | | `actionlint` | only the pre-existing SC2005 note `main` has | ## Notes - **Not a recheck leg:** this re-homes engineering statements. It is not a recheck leg of any theory theorem. The convergence theorems remain `open` (Agda-first plan in #1030). - **Removed files:** the removed Lean files' statements are the Idris2 files' statements. Git history keeps the Lean versions. --- _Generated by [Claude Code](https://claude.ai/code/session_01CYR5bf5FBLS7cXQK72aVNM)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
Summary
This is the second PR of the proof-ledger stack and is based on #1029; review it after that. It follows the owner's decisions of 2026-11-09: move EXPLAINME to the root with a full refresh, and use constructive reals for the convergence theorems.
EXPLAINME.adoc moves back to the repository root, as README-EXPLAINME requires. Every claim in it was re-checked against the tree.
proofs/agda/safety-triangle row for a directory that doesn't exist.Gen.idris a generator, not a spec;Verdict/Retractionare added.mix hypatia.*tasks that compute them.lib/, recipe, CLI-command and Mix-task counts,just build-all,guix.scm, and two dead links. Fixing README itself is a follow-up PR.[[proof-ledger]]section citesverification/proof-ledger.jsonland quotes its census.README / AFFIRMATION
.mdlink.Derived claims:
scripts/proof-ledger.sh claimsfails when a census quoted in README, AFFIRMATION or EXPLAINME differs from the ledger's. It runs in CI and has 4 contracts, built from the ledger so they survive count changes.Convergence handover, rewritten Agda-first:
--safe --without-K --cubical-compatible, over constructive Bishop reals built on agda-stdlib v2.3 (8326c74), with no Mathlib.echo_state_network.exactually uses.docs/proofs/needs.adocbecomes a pointer to the ledger; its own list had drifted ("Agda retired", Mathlib).How has this been verified?
Data.Rationaland checks a Bishop-real record under the §2.1 profile, with rc=0.proof-ledger.sh check/render --check/claimsall pass (4 quoted censuses agree).tests/proof-ledger-test.sh: 19 passed, 0 failed.check-proof-status.sh: OK..exfiles, 16 Mix tasks,RateLimiter/Safety.Quarantinehaving no callers, thedispatch_guard.exnovelty lines, and the missingguix.scm.shellcheckis clean; the invisible-character scan is clean.Notes
CC-BY-SA-4.0, the repo's docs licence. The standard's MPL example reads "or applicable licence"..audittraining/datasets still namedocs/EXPLAINME.adoc. They are a frozen training corpus and are left as they are.Generated by Claude Code