Repository navigation
census: see proofs written in Rust (Creusot/Pearlite, Verus), rank status docs - #31
Open
hyperpolymath wants to merge 3 commits into
Open
hyperpolymath wants to merge 3 commits into
hyperpolymath wants to merge 3 commits into
Conversation
…atus docs The census found proof files by prover extension only, so every Creusot and Verus proof in the estate (PROOF-POLICY §1.2 makes both the default for first-party Rust) was invisible: catachresis-colloquium/IDApTIK, with a CI-proved Creusot kernel, read as "idris2 9". - census-repo.sh: a crate is found by its [package] Cargo.toml depending on creusot-std / creusot-contracts / vstd / verus_builtin; only that crate's .rs files are read, and a file is kept when it carries a contract or proof marker. Files are labelled rs-creusot or rs-verus. Contract-carrying functions (and Verus proof/spec fns) count as declarations. MATHESIS_GIT_BASE lets the tests use a local forge. - proof-holes.sh: #[trusted] is recognised in the cfg_attr(creusot, ...) form too; Verus admit(), assume(...) and external_body are escapes. (This is proof-craft's script; the rules need carrying upstream.) - build-rows.sh: creusot and verus count as engineering provers. A repo with several status docs is listed under PROOF-STATUS, else PROOF-NEEDS, else a proof-debt ledger (now any name containing proof-debt, e.g. CREUSOT-PROOF-DEBT.tsv). Also fixes a latent bug: an empty template list made the NR==FNR idiom drop every row. - tests/census_rust_test.sh: an offline fixture repository (a Creusot crate, a Verus crate, an unverified crate, both kinds of status doc) through census-repo.sh and build-rows.sh. It fails on the previous scripts; wired into `just census-test` and proven-tests.yml. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDgrTtpKguSWPmrtoJd Signed-off-by: Claude <noreply@anthropic.com>
|
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 34 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. |
estate-rules failed on 7b1e096 with "committed REPOSITORY-MAP.adoc is stale": the map lists every path and this PR added a test. Regenerated with `just repo-map`; tests/shape/repo_map_determinism_test.sh now passes locally (it failed the same way before). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDgrTtpKguSWPmrtoJd Signed-off-by: Claude <noreply@anthropic.com>
Re-ran the full census (scripts/census/run-census.sh) over the committed 476-repository input on 2026-11-09 and regenerated the rows, catalogue and atlas. 276 repositories have proof files, 244 once template files are set aside (239 before); five carry Creusot or Verus proofs the first pass could not see: catachresis-colloquium/IDApTIK (idris2 9, creusot 3, two #[trusted] escapes), hyperpolymath/Axiom.jl, cicd-squabbler, cicd-suite and metadatastician/vordr (creusot 2, verus 1). Comparing every repo's status doc with the first pass found one ranking regression: developer-ecosystem moved from its root PROOF-NEEDS.adoc to a sub-project's PROOF-STATUS.adoc. A document two or more directories deep (outside docs/status/ and .machine_readable/compliance/) now ranks after any shallower one; standards' 3-practice/ layout keeps its needs list. Both shapes are new cases in census_rust_test.sh, which failed on the earlier rule. Every other change of status doc is a PROOF-STATUS page now preferred over a needs list or debt ledger beside it. The atlas tests pin the snapshot size, so 239 becomes 244 there and in docs/atlas/README.adoc. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDgrTtpKguSWPmrtoJd Signed-off-by: Claude <noreply@anthropic.com>
|
hyperpolymath
marked this pull request as ready for review
November 9, 2026 15:37
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
added a commit
to catachresis-colloquium/IDApTIK
that referenced
this pull request
Nov 9, 2026
… proof ledger (#222) ## Summary Closes out the brand thread (#206, #207, #220) against the estate PROOF-POLICY (`metadatastician/standards` at `9bdf864`), using the owner decisions of 2026-11-09. Four commits: ### 1. `a62cc9f`: the contrast kernel's contract holds for its callers, and has teeth | Gap | Fix | |---|---| | `meets` required `num, den <= 1000` while its doc capped the *ratio*, and two tests called it with `2101/100`: unverified callers outside the proved domain. | The bound is now `num, den <= 10^6`; products stay below `~1.05·10^16`. It is exported as `THRESHOLD_TERM_MAX`. A corner test evaluates every extreme with overflow checks on, and a planted bound of `4e9` makes it panic. | | `srgb::meets`, the unverified caller, never checked the kernel's precondition. | It now refuses an out-of-range threshold. Two `should_panic` tests cover that, plus an exhaustive check of all 256 channel values against the kernel's bound. | | The Creusot job's only mutant was in `trace.rs`. | Two contrast mutants must translate and then fail the **proof**: `Goal Coma.vc_luminance: ✘` and `Goal Coma.vc_meets: ✘` in CI run 42621975151, with `Proved (24 files)` on the clean tree. | `AGENTS.md` now points at PROOF-POLICY: Creusot with Pearlite, plus Verus; Idris2 for interfaces; Agda for theory. ### 2. `28beede`: the contrast proof sessions are committed in `verif/`, from that CI run ### 3. `ec1f89a`: the four live contrast failures are closed (owner decisions) 1. The `LOCKED` / `NO POWER` / `GUARD` labels are now `bone` (16.83:1). The threat stays as the alarm-red square and ring, which are glyphs at 4.27:1. 2. The OT button stays `phosphor`, and OT is marked by a 2 px `alarm` border (3.16:1 or better against both sides). The verb never sits on red. 3. The not-ready button stays pressable, and its verb is `phosphor` on the faint fill, 10.04:1 (it was 1.35:1). `dust` was offered at 5.89:1, but that figure was measured on bare glass. On the faint fill it is 4.37:1 and fails, so the owner chose `phosphor`. 4. The meter track is `pitch`. `cobalt`, the lowest fill, is 3.34:1 (it was 2.58:1 on `slate`). The colours come from `deck::verb_style` and `hud::METER_TRACK`, and the tests read those. Planted regressions fail: a slate track gives 2.58:1, and a glass verb on the not-ready button gives 1.36:1. ### 4. `c6b519d`: a machine proof ledger, `config/proof-ledger.ncl`, rendered to `docs/status/PROOF-STATUS.adoc` - 29 obligations. *14 proven of 29; 0 proven-with-postulates, 8 tested-only, 2 argued, 5 open.* - Every row is an engineering obligation, so no Proof Witness Grade applies. - The two Verus legs are `open`: the agent session's permission classifier refused to run the toolchain's install script. - The schema rejects: - a status word outside the closed set; - a proven row without a receipt; - an open row without a next action; - a dangling or duplicate id; - a proven row resting on an unproven step; - a proven Creusot row with no Verus leg; - a PWG field. - There are ten bad fixtures, and each must fail *for the reason its `# expect:` line names*. - `just proof-ledger-check` runs in CI's `config-scenario-check` job and fails on drift. ## Verification - Every commit passed the repo's local gates: `test-ghost` crates, `brand-check`, `proof-ledger-check`, clippy `-D warnings`, fmt, `creusot_ledger_check`, `must_check`, `doc_claims_check` and `cargo deny`. - The full `idaptik-bevy` package tests pass, including the schedule-initialisation smoke that catches query conflicts. - The Creusot proof and its mutants are receipted in CI. ## For the owner - `docs/PROJECT-ASSURANCE-PROFILE.adoc` still says "no Creusot obligations discharged yet". That is stale, but `AGENTS.md` forbids changing its labels as a side effect, so it is left for an evidence review. - The census-side counterpart is hyperpolymath/mathesis#31. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01J4QvDgrTtpKguSWPmrtoJd <!-- This is an auto-generated comment: release notes by coderabbit.ai --> <!-- coderabbit-ai-generated:v1 --> ## Summary by CodeRabbit * **New Features** * Added a proof-status page summarizing completed, in-progress, and tested obligations, with verifier details, dependencies, and follow-up actions. * **Bug Fixes** * Improved visual contrast across screen labels, deck buttons, and HUD meters. Threat labels now use bone text, OT buttons use an alarm border, and meters use a pitch-colored track. * Updated ready and not-ready button colors to improve readability while preserving their existing interaction behavior. <!-- end of auto-generated comment: release notes by coderabbit.ai --> --------- Signed-off-by: Claude <noreply@anthropic.com> 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
The census found proof files by prover extension only, so no Creusot or Verus proof in the estate appeared in the catalogue, although PROOF-POLICY §1.2 makes both the default for first-party Rust. For example,
catachresis-colloquium/IDApTIKhas a CI-proved Creusot kernel, yet read asidris2 9with no status doc.This PR teaches the census to find proofs written in Rust and to rank a repository's proof-status documents. It also carries a full second census run with the new scripts.
Changes
scripts/census/census-repo.sh: finds Rust proofs.[package]Cargo.tomldepending oncreusot-std,creusot-contracts,vstdorverus_builtin. Only that crate's.rsfiles are read, and only files carrying a contract or proof marker are kept.rs-creusotorrs-verus.proof fnandspec fn.MATHESIS_GIT_BASElets the tests point the census at a local forge.scripts/census/proof-holes.sh: new escape rules.#[trusted]is now recognised in thecfg_attr(creusot, creusot_std::macros::trusted)form too.admit(),assume(…)and#[verifier::external_body]count as escapes.scripts/census/build-rows.sh: provers and status docs.creusotandveruscount as engineering provers.docs/status/and.machine_readable/compliance/) comes after any shallower one. Then aPROOF-STATUSpage beats aPROOF-NEEDSlist, which beats a proof-debt ledger. A debt ledger is now any name containingproof-debt, such asCREUSOT-PROOF-DEBT.tsv.NR==FNRidiom drop every row.summarise.sh,render-catalogue.sh,README.adoc: prover names, the method, and second-pass numbers.tests/census_rust_test.sh: an offline fixture repository throughcensus-repo.shandbuild-rows.sh.build-rows.sh-only ranking cases cover a monorepo's nested sub-project page andstandards' one-level3-practice/layout.just census-testandproven-tests.yml.#[trusted]), Axiom.jl, cicd-squabbler, cicd-suite, and vordr (creusot 2, verus 1).Status-doc changes, checked repo by repo against the first pass
Most changes are a
PROOF-STATUSpage now preferred over aPROOF-NEEDSlist or debt ledger beside it, which is the point. The rest:vcl-ut: debt → needs.jtv-lang: a status page found for the first time.IDApTIK: its debt ledger; itsPROOF-STATUS.adocarrives with proof + brand: contrast kernel contract, live contrast fixes, machine proof ledger catachresis-colloquium/IDApTIK#222.An earlier draft of the ranking moved
developer-ecosystemonto a sub-project's page. The depth rule fixes that, and it is now a test case.RSR Quality Checklist
Required
tests/census_rust_test.sh, which failed on the previous scripts;just catalogue-check;checkandbun test, 10 pass;repo_map_determinism_test.sh;check-root-shape.sh.census-repo.share the same set as before.As Applicable
Testing
Not covered:
repos.jsonwas not refreshed, so repos created after the first listing are absent, as before.🤖 Generated with Claude Code
https://claude.ai/code/session_01J4QvDgrTtpKguSWPmrtoJd