feat(self-contracts): encode 5-7 catalog-format spec rules as contract mementos#16
Conversation
…mementos Adds `provekit-self-contracts/src/catalog_format.rs` plus six broken-fixture JSON files. The module mirrors the per-file `.invariant.rs` pattern: an `invariants()` function authors one IR contract per spec rule, and a `verify_catalog()` runtime checker discharges them against a real catalog. Rules encoded against `protocol/specs/2026-04-30-protocol-catalog-format.md` (spec CID blake3-512:6d610d40...): R1 (kind literal "catalog"), R5 (every properties value is a self-identifying CID), R6 (declaredAt is ISO-8601 UTC), R7 (underscore-prefixed fields participate in JCS canonicalization), R14 (no truncated digests; 128-hex-char), R15 (every CID carries blake3-512: prefix). Each rule has a positive test against the real v1.3.0 catalog and a negative fixture that fails closed. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Warning Rate limit exceeded
To keep reviews running without waiting, you can enable usage-based add-on for your organization. This allows additional reviews beyond the hourly cap. Account admins can enable it under billing. ⌛ How to resolve this issue?After the wait time has elapsed, a review can be triggered using the We recommend that you space out your commits to avoid hitting the rate limit. 🚦 How do rate limits work?CodeRabbit enforces hourly rate limits for each developer per organization. Our paid plans have higher rate limits than the trial, open-source and free plans. In all cases, we re-allow further reviews after a brief timeout. Please see our FAQ for further information. ℹ️ Review info⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Pro Run ID: 📒 Files selected for processing (7)
✨ Finishing Touches🧪 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. Review rate limit: 0/1 reviews remaining, refill in 47 minutes and 9 seconds.Comment |
![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: bed31fa56c
ℹ️ 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".
| r5_problems.push(format!( | ||
| "properties[`{}`] is not a self-identifying CID", | ||
| key | ||
| )); | ||
| continue; |
There was a problem hiding this comment.
When a properties value has a non-blake3-512: prefix (for example sha256:<64-hex>), this branch pushes R15/R5 errors and then continues, so the R14 length check is skipped and r14_no_truncated_digests can incorrectly remain Holds. That breaks the stated per-rule independence of CatalogReport and produces a false negative for truncated-digest detection on malformed CIDs.
Useful? React with 👍 / 👎.
| r5_problems.push(format!( | ||
| "properties[`{}`] is {}, expected string", | ||
| key, | ||
| value_type(other) | ||
| )); |
There was a problem hiding this comment.
In the non-string branch, only r5_problems is updated before continuing, leaving r14_problems and r15_problems untouched. As a result, catalogs with non-string properties values can report R14 and R15 as Holds, even though no valid CID exists to satisfy prefix/length rules. This under-reports violations for malformed catalogs.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Pull request overview
This PR adds a new catalog_format module under provekit-self-contracts to encode a subset of the protocol-catalog-format spec as authored IR contracts plus a runtime JSON verifier. It extends the self-contracts crate with catalog-specific rule checking and fixture-backed tests, aiming to make selected catalog-format rules machine-checkable alongside the rest of the repository’s self-verification tooling.
Changes:
- Added
src/catalog_format.rswith six authored catalog-format rules, averify_catalogruntime checker, and in-module tests. - Exposed the new module from
provekit-self-contracts/src/lib.rs. - Added negative JSON fixtures for R1, R5, R6, R14, and R15.
Reviewed changes
Copilot reviewed 7 out of 7 changed files in this pull request and generated 7 comments.
Show a summary per file
| File | Description |
|---|---|
implementations/rust/provekit-self-contracts/tests/fixtures/catalog-format/r6-declared-at-local-time.json |
Negative fixture for non-UTC declaredAt. |
implementations/rust/provekit-self-contracts/tests/fixtures/catalog-format/r5-property-value-not-string.json |
Negative fixture for non-string properties value. |
implementations/rust/provekit-self-contracts/tests/fixtures/catalog-format/r15-sha256-prefix.json |
Negative fixture for wrong CID prefix. |
implementations/rust/provekit-self-contracts/tests/fixtures/catalog-format/r14-truncated-digest.json |
Negative fixture for truncated digest length. |
implementations/rust/provekit-self-contracts/tests/fixtures/catalog-format/r1-bad-kind.json |
Negative fixture for wrong top-level kind. |
implementations/rust/provekit-self-contracts/src/lib.rs |
Exposes the new catalog-format module from the self-contracts crate. |
implementations/rust/provekit-self-contracts/src/catalog_format.rs |
Implements catalog-format contract authoring, runtime verification, and tests. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| post: Some(eq( | ||
| ctor1("is_self_identifying_cid", ctor1("properties_value", str_const("any"))), | ||
| ctor1("true_const", str_const("")), | ||
| )), |
| contract( | ||
| "catalog_format_r6_declaredAt_is_iso8601_utc", | ||
| ContractArgs { | ||
| post: Some(eq( | ||
| ctor1("iso8601_utc", ctor1("declaredAt_of", str_const("c"))), | ||
| ctor1("true_const", str_const("")), | ||
| )), | ||
| ..Default::default() | ||
| }, |
| fn invariants_mints_one_contract_per_rule() { | ||
| reset_collector(); | ||
| begin_collecting(); | ||
| invariants(); | ||
| let decls = finish(); | ||
| assert_eq!( | ||
| decls.len(), | ||
| 6, | ||
| "expected 6 catalog-format contracts, got {}", | ||
| decls.len() | ||
| ); | ||
| let names: Vec<&str> = decls.iter().map(|d| d.name.as_str()).collect(); | ||
| assert!(names.iter().all(|n| n.starts_with("catalog_format_r"))); | ||
| // All distinct. | ||
| let mut sorted = names.clone(); | ||
| sorted.sort(); | ||
| let original = sorted.len(); | ||
| sorted.dedup(); | ||
| assert_eq!(sorted.len(), original, "duplicate contract names"); |
| // -- Aggregate sanity: every rule has both a positive and a negative | ||
| // coverage path. ----------------------------- | ||
| #[test] | ||
| fn coverage_summary_every_rule_has_positive_and_negative() { | ||
| // Positive: all_hold() on real catalog (covered by | ||
| // real_catalog_satisfies_all_encoded_rules). | ||
| // Negative: each fixture-based test above. This test simply | ||
| // sanity-checks that all six fixtures parse and run end-to-end. | ||
| let names = [ | ||
| "r1-bad-kind.json", | ||
| "r5-property-value-not-string.json", | ||
| "r6-declared-at-local-time.json", | ||
| "r14-truncated-digest.json", | ||
| "r15-sha256-prefix.json", | ||
| ]; |
| // catalog-format spec rules as machine-enforceable contracts. Independent | ||
| // of the per-Rust-file orchestrator below; lives in its own module so | ||
| // the file/test layout matches its origin (`protocol/specs/2026-04-30-protocol-catalog-format.md`). | ||
| pub mod catalog_format; |
| /// JCS-encode a JSON value via the canonicalizer crate. We round-trip | ||
| /// `serde_json::Value` -> `provekit_canonicalizer::Value` to stay on the | ||
| /// same bytes the rest of the protocol uses. | ||
| fn jcs_encode(j: &JsonValue) -> Result<String, String> { | ||
| use provekit_canonicalizer::{encode_jcs, Value}; | ||
| use std::sync::Arc; | ||
| fn to_canonical(j: &JsonValue) -> Result<Arc<Value>, String> { | ||
| Ok(match j { | ||
| JsonValue::Null => Value::null(), | ||
| JsonValue::Bool(b) => Value::boolean(*b), | ||
| JsonValue::Number(n) => { | ||
| let i = n | ||
| .as_i64() | ||
| .ok_or_else(|| format!("non-i64 number `{}` not supported", n))?; | ||
| Value::integer(i) | ||
| } | ||
| JsonValue::String(s) => Value::string(s.clone()), | ||
| JsonValue::Array(items) => { | ||
| let mut converted: Vec<Arc<Value>> = Vec::with_capacity(items.len()); | ||
| for it in items { | ||
| converted.push(to_canonical(it)?); | ||
| } | ||
| Value::array(converted) | ||
| } | ||
| JsonValue::Object(map) => { | ||
| let mut entries: Vec<(String, Arc<Value>)> = Vec::with_capacity(map.len()); | ||
| for (k, v) in map { | ||
| entries.push((k.clone(), to_canonical(v)?)); | ||
| } | ||
| Value::object(entries) | ||
| } | ||
| }) | ||
| } | ||
| let v = to_canonical(j)?; | ||
| Ok(encode_jcs(&v)) |
| post: Some(eq( | ||
| ctor1( | ||
| "starts_with", | ||
| ctor1("any_cid_in_catalog", str_const("c")), | ||
| ), | ||
| str_const("blake3-512:"), |
Summary
Closes the catalog-format meta-loop in task #177: the rules of
protocol/specs/2026-04-30-protocol-catalog-format.mdare now encoded as machine-enforceable contract mementos inimplementations/rust/provekit-self-contracts/. Each catalog can now ship with a discharge proof against the catalog-format spec.The encoding is a two-layer mirror of the kit's existing
.invariant.rspattern (seeprovekit-canonicalizer/src/jcs.invariant.rsfor the precedent). Layer 1:pub fn invariants()mints one declarative IR contract per rule via the kit'smust/contractcollector; the formula names the rule. Layer 2:pub fn verify_catalog(json) -> CatalogReportis the runtime discharge that walks a catalog JSON and answers per-rule whether it holds.The new module is
provekit-self-contracts/src/catalog_format.rs. It is independent of the existingauthor_all_invariants()orchestrator (which bundles.invariant.rsfiles for each Rust source); the catalog-format rules are not about a Rust function, so retrofitting them into that flow would have been wrong.Rules in the catalog-format spec (numbered checkboxes)
Read against
2026-04-30-protocol-catalog-format.mdat sha25601a880343b303b4a3ffdf68481bd9b187487b440c7c2e17f9033d6623d3a5010, 92 lines, full read.§1 (catalog file structure):
kindMUST be the literal string"catalog"nameMUST be present (string) — deferred (low value: shape check, no value-level discriminator beyond presence)versionMUST be present (string) — deferred (spec marksversionas informational only; the CID is the identity)algorithmsMUST be present (object, role -> array of self-identifying tags) — deferred (structure of role keys not value-level enough to discriminate; defer to a successor PR that wires the algorithm-tag whitelist)propertiesis a self-identifying CID stringdeclaredAtis ISO-8601 UTC_*) fields participate in JCS canonicalization (NOT stripped before hashing)§2 (hashing rules):
blake3-512:|| hex(BLAKE3-512(spec_file_bytes)) (raw bytes; no canonicalization) — deferred (mechanical equivalence to recompute-spec-cids step 2; encoding here would duplicate)blake3-512:|| hex(BLAKE3-512(JCS(catalog_json))) — deferred (mechanical equivalence to recompute-spec-cids step 5; same reason as R8)§5 (conformance test):
propertiesexists at expected path — deferred (already enforced by recompute-spec-cids; pure dup)properties[key]— deferred (already enforced by recompute-spec-cids; pure dup)§6 (forbidden patterns):
blake3-512:prefix (self-identifying)This PR encodes 6 of 15 rules (R1, R5, R6, R7, R14, R15). The deferred set falls into two buckets: shape checks with low discriminative value (R2, R3, R4) and rules already enforced verbatim by
tools/recompute-spec-cids(R8, R9, R10, R11, R12, R13).Test coverage summary
real_catalog_satisfies_all_encoded_rulesr1_violation_kind_not_catalog_is_caught(fixture:r1-bad-kind.json)real_catalog_satisfies_all_encoded_rulesr5_violation_property_value_not_string_is_caught(fixture:r5-property-value-not-string.json)real_catalog_satisfies_all_encoded_rulesr6_violation_declared_at_local_time_is_caught(fixture:r6-declared-at-local-time.json)r7_underscore_fields_change_jcs_bytes(asserts JCS bytes differ when_*keys removed)real_catalog_satisfies_all_encoded_rulesr14_violation_truncated_digest_is_caught(fixture:r14-truncated-digest.json)real_catalog_satisfies_all_encoded_rulesr15_violation_wrong_prefix_is_caught(fixture:r15-sha256-prefix.json)Plus aggregate tests:
invariants_mints_one_contract_per_rule—invariants()produces exactly 6 distinct-named contracts.coverage_summary_every_rule_has_positive_and_negative— every fixture parses and runs end-to-end without panic.19/19 tests pass under
cargo test --release --manifest-path implementations/rust/Cargo.toml -p provekit-self-contracts.Spec CID anchor
The spec this PR conforms to is
protocol-catalog-formatat:(value taken from
protocol/specs/2026-04-30-protocol-catalog.jsonv1.3.0)What this PR does NOT do (and why)
protocol/specs/. The catalog CID is unchanged; no drift introduced.tools/recompute-spec-cidsorprovekit-ir-symbolic/src/invariants.rs. Other agents own those.author_all_invariants(). The orchestrator there bundles per-Rust-file.invariant.rsmodules; the catalog isn't a Rust file, and trying to thread it in would tangle the orchestrator. The new module stays independent; minting a.prooffor these contracts would be a successor PR if/when needed.Test plan
cargo build --release --manifest-path implementations/rust/Cargo.toml -p provekit-self-contractssucceedscargo test --release --manifest-path implementations/rust/Cargo.toml -p provekit-self-contractsreports 19/19 passprovekit-self-contractsitself (existing pre-PR warnings come fromprovekit-ir-symbolic/src/invariants.rs, owned by another agent, untouched here)