P1-0 (B): claims ledger — run every TESTED row, reconcile test/proof counts - #146
Merged
Merged
Conversation
…y/fmt - e2e.yml: `toolchain: v1` is not a toolchain name (rustup: "invalid toolchain name: 'v1'"), so "Rust Build + Unit Tests" died before building. Use `stable` with clippy + rustfmt components. - e2e.yml: drop `|| true` from the Clippy and Format steps; they could never fail. - cargo fmt over attestation.rs / keys_cli.rs (rust-ci's first red step). - Clear every `clippy --all-targets -D warnings` lint (each target's errors masked the next): rand 0.9 thread_rng -> rng, needless mut / borrow / parens, &PathBuf -> &Path, dead `root_path` field, dead store in the transactions bench. - jk-keys imported `attestation` and `keys` via `mod`, compiling a second private copy of each: the lib's public API read as dead code there and 10 unit tests ran twice. Import them from the lib crate instead. Unique test count is unchanged (107; was 117 listed with the 10 duplicates). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VxcAoyMQe7CjQwCKL18Mm4
….adoc
- dtolnay/rust-toolchain@v1 needs a `toolchain` input; the Criterion,
E2E Lifecycle and Panic Attack jobs had none ("'toolchain' is a required
input"). Set `stable`.
- tests/aspect: SECURITY/ARCHITECTURE/PROOF-NEEDS/TOPOLOGY were migrated
to .adoc, so the .md-only existence checks failed 4/29. Accept either,
as README already did. Negative control: removing TOPOLOGY.adoc makes
the check FAIL.
- attestation: propagate HMAC new_from_slice's error instead of expect()
(Hypatia expect_in_hot_path; the fn already returns io::Result).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VxcAoyMQe7CjQwCKL18Mm4
… counts ULTRAPLAN P1-0, first of three stacked PRs. PROOF-NEEDS.adoc gains a `=== Claims ledger` table, one row per line: claim | status | artefact | command, status one of PROVEN / TESTED / ASSUMED / DESIGNED / OPEN. dashboard-check now: - rejects a wrapped row, an unknown status, a missing table, naming the line; - for TESTED rows, requires the artefact file to name the test, the command to exit 0, and an output line showing that test passing, so `true` or a filter that runs 0 tests fails; - for PROVEN rows, requires the theorem name and a passing checker command; - for ASSUMED / DESIGNED / OPEN, requires command `-` and an existing file or #N artefact; - measures tests with `cargo test --workspace --locked -- --list` and fails when README / EXPLAINME / TOPOLOGY / READINESS print a different test count, or a proof count different from the number of PROVEN rows. The ledger has 7 TESTED rows and 2 OPEN rows (#145); 0 PROVEN, because the Idris2 ABI does not typecheck. The dashboards claimed 67 tests and 30 proofs; they now say 119 tests and 0 checked proofs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VxcAoyMQe7CjQwCKL18Mm4
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 38 minutes. View limit detailsLimit details: You’ve used the included review currently available. Review configuration: ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: 📒 Files selected for processing (22)
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. Comment |
`cargo test -- --list` counts declared tests; an #[ignore] would keep the count while "pass" became false. rust-ci is what runs them. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VxcAoyMQe7CjQwCKL18Mm4
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
1 participant
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.
ULTRAPLAN P1-0, PR B of three (B: ledger + counts; C: escape-hatch counter; D:
workflow_call).What it does
PROOF-NEEDS.adocgains a=== Claims ledgertable. Each row isclaim | status | artefact | command, with status PROVEN / TESTED / ASSUMED / DESIGNED / OPEN, and each row fits on one line.dashboard-check --check .(already run bydashboard-check.yml) now does the following:file::testmust exist and name the test. The command must exit 0, and some output line must show that test passing (ok/PASS). That rejectstrueand a filter that runs 0 tests.-. The artefact must be an existing file or#N.Dashboard counts. On README / EXPLAINME / TOPOLOGY / READINESS, a number followed within two words by test(s) must equal
cargo test --workspace --locked -- --list(lines ending: test). A number followed by proof(s)/theorem(s) must equal the number of PROVEN rows. Percentages are excluded, and so are numbers in another table cell.Ledger contents: 7 TESTED rows (obliteration ×3, execute∘undo, content-store round-trip, rollback, audit-chain verify) and 2 OPEN rows (#145). 0 PROVEN, because the Idris2 ABI does not typecheck.
Doc corrections the checker forced
TOPOLOGY "Last updated" → 2026-10-02.
Scope limits (stated, not implied)
N%figures on TOPOLOGY are not checked.Verification (local, rust 1.97.1)
cargo fmt --all -- --check✓;cargo clippy --workspace --all-targets --locked -- -D warnings✓;cargo test --workspace --locked: 119 passed, 0 failed.cargo run -p dashboard-check -- --check .→ rc=0:✓ 119 tests measured, 0 PROVEN claims, all 7 TESTED rows ran and passed.claims 118 but there are 119on three lines with rc=1. It was green again after the update.claims.rs):lying_verifier_fails(exit 0, no output),unchecked_skip_fails(running 0 tests),inflated_counts_fail_and_true_counts_pass,wrapped_row_is_rejected,proven_row_needs_theorem_and_passing_checker,open_rows_run_nothing_and_need_a_real_artefact.✓ Testedrows, both✓ Openrows and✓ 119 tests measured, 0 PROVEN claims.Red checks: inherited from #144 (e6fee67), deferred, not introduced here
The red set on this head equals #144's, which equals main 539e6f9's. The ledger commit adds none.
lint-workflows: deferred to main is red on 7 of 12 workflows; four e2e jobs die atdtolnay/rust-toolchain@v1, so the unit tests have no CI measurement #135 (acceptance item 5)governance / Workflow security linter: deferred to main is red on 7 of 12 workflows; four e2e jobs die atdtolnay/rust-toolchain@v1, so the unit tests have no CI measurement #135 (acceptance item 5)governance / Allowlist Preflight: deferred to main is red on 7 of 12 workflows; four e2e jobs die atdtolnay/rust-toolchain@v1, so the unit tests have no CI measurement #135 (acceptance item 6,Check live Actions policy)Validate DEED manifests: deferred to main is red on 7 of 12 workflows; four e2e jobs die atdtolnay/rust-toolchain@v1, so the unit tests have no CI measurement #135 (acceptance item 6)estate-audit: deferred to main is red on 7 of 12 workflows; four e2e jobs die atdtolnay/rust-toolchain@v1, so the unit tests have no CI measurement #135 (acceptance item 6,Code Hygiene Gate)idris-abi (expected red until J1-3): expected red by design (docs(security): placeholder key ids so required gitleaks passes #142) until J1-3: make the Idris2 ABI typecheck; delete or honestly restate the six unproved security claims #145 (ULTRAPLAN J1-3) makes Types.idr typecheck.CodeRabbit posted the status "Review rate limited" on 6f31e89 and has not reviewed this PR yet. Its review will be read before this PR is marked ready.
🤖 Generated with Claude Code
https://claude.ai/code/session_01VxcAoyMQe7CjQwCKL18Mm4