Repository navigation
Create receipt-bound publication proof authority - #36
Conversation
📝 WalkthroughWalkthroughAdds receipt-bound publication authority promotion across evidence contracts, SQLite storage, application, CLI, MCP, scripts, tests, and trust documentation. The new flow replays staged artifacts, requires a passed publication report, and atomically persists authoritative proof or refutation evidence. ChangesPublication authority promotion
Estimated code review effort: 5 (Critical) | ~120 minutes Possibly related PRs
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
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 |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
There was a problem hiding this comment.
🧹 Nitpick comments (1)
src/app.rs (1)
5602-5620: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winExtend the gate test to the enforcement-flag paths.
validate_publication_authority_reportalso rejects aPassedreport when any ofclean_checkout,dependency_closure_complete,network_isolation_enforced,memory_limit_enforcedis false, or whenauthoritativeis true. This test only flipsclassification, so those fail-closed branches are unverified. Consider adding cases that keepclassification == Passedwhile individually clearing each flag (and settingauthoritative = true) and assertingMCL_PUBLICATION_AUTHORITY_REPORT_NOT_PASSED.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@src/app.rs` around lines 5602 - 5620, Extend publication_authority_requires_an_explicit_passed_report to retain classification as Passed while individually setting clean_checkout, dependency_closure_complete, network_isolation_enforced, and memory_limit_enforced to false, plus authoritative to true. For each case, assert validate_publication_authority_report returns MCL_PUBLICATION_AUTHORITY_REPORT_NOT_PASSED, preserving the existing classification checks.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Nitpick comments:
In `@src/app.rs`:
- Around line 5602-5620: Extend
publication_authority_requires_an_explicit_passed_report to retain
classification as Passed while individually setting clean_checkout,
dependency_closure_complete, network_isolation_enforced, and
memory_limit_enforced to false, plus authoritative to true. For each case,
assert validate_publication_authority_report returns
MCL_PUBLICATION_AUTHORITY_REPORT_NOT_PASSED, preserving the existing
classification checks.
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro
Run ID: 5d488c4c-a3cb-4903-a6e4-eac5d9c3220f
📒 Files selected for processing (18)
.github/workflows/publication.ymldocs/decisions/ADR-0007-atomic-receipt-bound-publication-authority.mddocs/dev-diary/0035-a-witness-must-name-the-exact-thing.mddocs/dev-diary/README.mddocs/implementation/RELEASE_CHECKLIST.mddocs/implementation/STATUS.mddocs/trust/PUBLICATION_AUTHORITY.mdmigrations/0011_publication_authority.sqlschemas/evidence/evidence-2.schema.jsonscripts/publication-ingest.shsrc/app.rssrc/cli/mod.rssrc/domain/evidence.rssrc/domain/mod.rssrc/mcp/mod.rssrc/store/mod.rstests/mcp_stdio.rstests/phase1_cli.rs
|
Addressed the final CodeRabbit test-coverage finding in
Every case fails closed with Local validation on the exact commit:
|
Exact merged-main publication-authority evidencePR #36 merged as Post-merge evidence:
Downloaded byte audit:
The audit checked exactly 72 regular files with no symbolic links, all 25 fixed retained roles by canonical path/identity/byte hash, 24 sorted unique final artifact hashes after content deduplication, all eight empty stderr files, and 18 explicitly false The final payload names formalization The certificate and SLSA statement bind immutable repository/owner IDs, the protected workflow, This completes issue #21's receipt-bound formal proof-authority boundary. It does not create source-claim |
Summary
evidence/2andpublication_authority_binding/1contracts without changing anyevidence/1byte identity.Change class
Select one:
Affected trust boundary: the protected-publication boundary that may create authoritative formal proof/refutation evidence. The receipt is only a locator; authority is derived from exact replay inside the application and Store transaction.
TDD evidence
Red evidence: issue #21 and the existing publication contracts denied this authority path before implementation. Independent review then produced concrete failing regressions for cross-subject receipt substitution and post-ingestion failure retention; both were fixed at the boundary. The final review added individual fail-closed enforcement-flag cases.
Green evidence: exact receipt/request subject binding now holds at ingestion, Store promotion, SQL insertion, retry, and evidence read. Promotion covers dry-run, persist, exact retry, missing CAS, altered staged content, forbidden caller inputs, and every protected-report pass condition.
Commands and results:
cargo fmt --all -- --checkcargo clippy --workspace --all-targets --all-features -- -D warningscargo test --workspace --all-targets— 112 library, 1 Lean-worker, 3 MCP, and 10 CLI tests on the initial head; the review follow-up adds one case group without changing production codeMCL_RUN_LEAN_INTEGRATION=1 cargo test --test lean_worker -- --nocapture— real pinned Lean 4.32.0PYTHONPATH=src PYTHONWARNINGS=error::ResourceWarning python -m unittest discover -s tests -v— 39 passedgit diff --checkmcl health/mcl doctor, and unknown receipt rejected asMCL_PUBLICATION_RECEIPT_NOT_FOUNDMathematical verification
Verifier and result: real Lean 4.32.0 integration passed locally and in required CI. The exact merged-main protected-publication run remains a post-merge acceptance condition and will be independently audited before issue #21 is closed. This change creates authority only for the exact Lean formalization named by the request; it does not derive source-claim truth.
Provenance and licensing
Provenance references: ADR-0007,
docs/trust/PUBLICATION_AUTHORITY.md, the retained closure and attestation contracts, and issue #21.Risk and recovery
Known limitations: this is formalization authority only. SPEC section 11 still requires a later read combining current formal authority with current verified statement fidelity and all other derived-truth preconditions. Docstring coverage remains advisory; the public trust contract is documented in the ADR, schema, trust guide, CLI help, and tests.
Rollback or recovery plan: revert the merge commit. Migration 11 is additive; legacy
evidence/1identities and reads remain unchanged. A failed promotion retains the exact raw and canonical receipt CAS bytes for replay and diagnosis.Follow-up work: independently audit the protected-main artifact, record exact hashes/run metadata, close issue #21 only if every criterion passes, then implement the separate fidelity-bound source-truth read.
Review readiness
Review-driven hardening
Passed.Advances #21. Do not close #21 until the exact merged tree produces and retains a protected-main authority record and that artifact is independently audited.