feat(baseline): rust-std-baseline-v1 pilot (closes #257)#292
Conversation
… builtins (closes #257) First-mover pilot validating the per-language foundation-baseline workflow locked by #254 (rubric), #255 (federation), #256 (DSL survey). Adds: - `implementations/rust/provekit-baseline-rust-std/` — orchestrator crate with seven slabs (string, vec, option, result, slice, hashmap, iter) authoring 157 ContractDecls across 58 distinct std::* builtins. Each builtin meets the rubric's 2-predicate floor (type signature + determinism); aspirational structural predicates added where the current DSL surface (forall/eq/gte/ctor/num/strConst) reaches. - `src/bin/mint-rust-std-baseline.rs` — orchestrator binary signs with foundation v0 ed25519 seed, asserts byte-determinism, enforces rubric §"Compliance checklist" floors before exit. - Disclaimer ships as a `kind=disclaimer` v1.2 layered memento member of the proof envelope; envelope metadata pins disclaimer_cid + baseline.{version,language,language_version,kit_version} per §3. - `.provekit/baselines/rust-std-baseline-v1.proof` — the signed catalog (275 KB; bundle CID `blake3-512:60dc813e…14ec`, contractSetCid `blake3-512:76c278af…d5e4`). - `docs/baselines/README.md` + `docs/baselines/rust.md` — per-rubric index + per-language addendum (steward: rust-lang team; signature available: no; gaps: G6 effect tracking, G7 aliasing). - Regression tests pin contractSetCid + disclaimer_cid; substrate-load test asserts the verifier round-trips every member with zero load errors (the AC "substrate verifies the bytes" gate). DSL surface honored: only forall/eq/gte/ctor/num/strConst per #285's pre-launch lock. G1-G4 (lt/lte/between/member_of/or/not) land in a follow-up PR after the cross-kit DSL extension. G5-G10 are research-grade and explicitly deferred in the rust addendum. Foundation v0 seed unchanged ([0x42; 32]); other kits untouched; catalog CIDs unchanged. Workspace gains one new member. 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 ignored due to path filters (1)
📒 Files selected for processing (16)
✨ 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 54 seconds.Comment |
Two `tempdir()` calls within the same test (e.g. `mint_baseline_is_deterministic`'s dir1 + dir2) could resolve to the same nanosecond and collide on path. Add an AtomicU64 sequence number suffix so back-to-back invocations always produce distinct paths. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Captures institutional knowledge per-kit agents need before authoring
their baseline:
- Disclaimer must ship as kind=disclaimer v1.2 layered memento member
(NOT raw bytes — verifier rule-2 fails on raw-blob members)
- Foundation v0 seed: redeclare locally per kit, don't depend on cli
- claim-envelope::assemble_layered/build_header private; baselines
inline-replicate until public helper lands (follow-up filed)
- .gitignore needs allowlist line !.provekit/baselines/*.proof
Plus empirical validation from the pilot:
- 2-predicate floor reached on every one of 58 builtins WITHOUT G1-G4
- G1-G4 would have lifted ~70% to aspirational 3+ density (lt/lte for
numeric bounds, or/not for nullable returns)
The 12 per-kit agents (#258-#270) read this rubric first; institutional
notes belong here, not in scattered comments.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
Pull request overview
Introduces the first Rust std::* “foundation baseline” catalog as a new Rust workspace crate that mints a deterministic, signed .proof bundle (plus pin/verification tests) and adds the accompanying baseline documentation.
Changes:
- Added
provekit-baseline-rust-stdcrate with slab-authored ContractDecls and a minting orchestrator binary. - Added regression/pin tests for
contractSetCidanddisclaimer_cid, plus a substrate load verification test. - Added baseline docs + checked-in baseline
.proof, and updated workspace membership +.gitignoreallowlist.
Reviewed changes
Copilot reviewed 14 out of 17 changed files in this pull request and generated 8 comments.
Show a summary per file
| File | Description |
|---|---|
| implementations/rust/provekit-baseline-rust-std/Cargo.toml | New crate manifest for the Rust std baseline mint/orchestrator. |
| implementations/rust/provekit-baseline-rust-std/src/lib.rs | Core orchestrator: disclaimer member minting, contract minting, proof envelope build, and unit tests. |
| implementations/rust/provekit-baseline-rust-std/src/bin/mint-rust-std-baseline.rs | CLI mint driver: deterministic double-mint check + compliance gate output. |
| implementations/rust/provekit-baseline-rust-std/src/std_string_slab.rs | String/str baseline invariants slab. |
| implementations/rust/provekit-baseline-rust-std/src/std_vec_slab.rs | Vec baseline invariants slab. |
| implementations/rust/provekit-baseline-rust-std/src/std_option_slab.rs | Option baseline invariants slab. |
| implementations/rust/provekit-baseline-rust-std/src/std_result_slab.rs | Result baseline invariants slab. |
| implementations/rust/provekit-baseline-rust-std/src/std_slice_slab.rs | Slice baseline invariants slab. |
| implementations/rust/provekit-baseline-rust-std/src/std_hashmap_slab.rs | HashMap/BTreeMap baseline invariants slab. |
| implementations/rust/provekit-baseline-rust-std/src/std_iter_slab.rs | Iterator baseline invariants slab. |
| implementations/rust/provekit-baseline-rust-std/tests/baseline_pin.rs | Pin tests for CIDs + substrate load smoke test + floor checks. |
| implementations/rust/Cargo.toml | Adds the new baseline crate to the Rust workspace members. |
| implementations/rust/Cargo.lock | Locks dependency graph including the new baseline crate. |
| .provekit/baselines/rust-std-baseline-v1.proof | Checked-in signed baseline catalog artifact. |
| docs/baselines/README.md | Baseline catalog overview + index entry for rust baseline. |
| docs/baselines/rust.md | Rust baseline-specific disclaimer, coverage summary, and minting instructions. |
| .gitignore | Allowlists .provekit/baselines/*.proof for committing baseline catalogs. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| /// Mint the disclaimer as a layered memento. Returns the canonical | ||
| /// bytes plus the attestation CID (key under which it goes into the | ||
| /// proof envelope's `members` map). |
| /// baseline.{version,language,language_version,kit_version,disclaimer_cid}. | ||
| #[test] | ||
| fn envelope_metadata_carries_required_fields() { | ||
| let dir = tempdir(); | ||
| let m = mint_baseline(&dir).expect("mint"); | ||
| let _ = std::fs::remove_dir_all(&dir); | ||
|
|
||
| // Re-decode the catalog to pull metadata out of the on-disk bytes. | ||
| // We don't ship a full CBOR decoder reader here; the assertion | ||
| // is structural — the mint pipeline ALWAYS sets these keys, so |
| assert!( | ||
| pool.mementos.len() >= 100, | ||
| "verifier indexed only {} mementos; expected >= 100", |
| DSL predicates G1-G4 (`lt`, `lte`, `between`, `member_of`, `or`, `not`) | ||
| are tracked in [`dsl-extension-survey.md`](../contributing/dsl-extension-survey.md) | ||
| for the post-launch DSL extension PR; using them here would diverge | ||
| from sibling kits' surfaces during the parallel #258-#268 mint push. |
|
|
||
| - [`docs/contributing/baseline-catalog-rubric.md`](../contributing/baseline-catalog-rubric.md) (#254) | ||
| - [`docs/contributing/signing-your-own-catalog.md`](../contributing/signing-your-own-catalog.md) (#255) | ||
| - [`docs/contributing/dsl-extension-survey.md`](../contributing/dsl-extension-survey.md) (#256) |
| Foundation v1 advisory catalog of hidden predicates about Rust's | ||
| `std::*` builtins. Authored against `rustc 1.81.0`. | ||
|
|
||
| Catalog file: [`.provekit/baselines/rust-std-baseline-v1.proof`](../../.provekit/baselines/rust-std-baseline-v1.proof). |
| | Language | Catalog | Status | Authored against | | ||
| |----------|---------|--------|------------------| | ||
| | rust | [`.provekit/baselines/rust-std-baseline-v1.proof`](../../.provekit/baselines/rust-std-baseline-v1.proof) | v1 (foundation-baseline, advisory) | rustc 1.81.0 | | ||
| | go | _pending #258_ | not yet minted | — | |
| provekit-claim-envelope = { path = "../provekit-claim-envelope" } | ||
| provekit-ir-symbolic = { path = "../provekit-ir-symbolic" } | ||
| provekit-proof-envelope = { path = "../provekit-proof-envelope" } | ||
| serde_json = { workspace = true } |
…exclusion - Rename ctorN -> ctor_n (snake_case, fixes non_snake_case warning) - Add #[allow(dead_code)] to ctor0/ctor2 with explanatory comment; they are scaffolding for future N-ary predicate kinds, not bugs - Add comment to configs/rust.toml explaining it is intentionally excluded from the mint_all_baselines langs list — Rust baselines are owned by provekit-baseline-rust-std (#292) to avoid duplicate rust-std-baseline-v1 Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…366) (#387) * fix(baselines): resolve P1 review concerns from #293/#326 inline Closes #366 partial (generator + BridgeV14 kit work). P1 concerns addressed: #1 Critical (CodeRabbit) — apply_builtin dead ctor0 branch: removed the unreachable `a == 0` guard introduced by `let a = if arity == 0 { 1 }`. Now arity=0 (serde default) correctly means unary; the ctor0 path is gone. #5 Major (Copilot) — gte double-wrap: the old gte arm applied ctor1(left, ctor1(sig, s)) in both branches of a dead if/else. Fixed to ctor1(left, s) — the property applied directly to the input variable, not to the builtin result. #9 + #11 (CodeRabbit Major) — rust in lang list causes duplicate rust-std-baseline-v1: removed "rust" from the hard-coded langs array. rust is already minted by provekit-baseline-rust-std (#292). rust.toml kept as reference but is not read by this binary. #13 (Copilot) — silent skip on missing config changed to panic: a missing config is always a repo error, not a runtime skip. #14 (Copilot) — unknown predicate kind silently skipped changed to panic: unknown kinds indicate a stale config or missing handler, not a soft warning. #15 (Copilot Major) — missing gte.args.left defaulting to signature changed to panic: malformed configs must not silently produce wrong-but-passing baselines. #19 (CodeRabbit Major) — PHP Minter.php mintBridgeV14 now validates and normalizes the tagged-union target before signing. Extra keys are stripped; missing kind or cid fails with InvalidArgumentException. #20 (CodeRabbit Critical) — Python bridge_v14.py missing `import base64` added. The base64 module is used at line 101 but was not imported. BridgeV14 kit work (from #326, unique to that branch): - C kit: bridge_v14.c + self_contracts.h header - PHP kit: Minter.php (+ validation fix above) - Per-kit BridgeV14 in cpp, csharp, go, python, ruby, swift, ts, zig Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * chore(baselines): regenerate 11 per-kit std baseline catalogs Baselines minted by `mint-all-baselines` against the corrected orchestrator (P1 fixes from previous commit). Rust excluded from this binary — handled by provekit-baseline-rust-std. 11 kits minted: c, cpp, csharp, go, java, php, python, ruby, swift, typescript, zig. CIDs: c blake3-512:6a30a452... cpp blake3-512:64fc0845... csharp blake3-512:e221722e... go blake3-512:efa64a6c... java blake3-512:22a41119... php blake3-512:93028afd... python blake3-512:224e0cbe... ruby blake3-512:1c52edaf... swift blake3-512:313ab922... typescript blake3-512:9da2bdff... zig blake3-512:5f7e1f73... These are byte-deterministic: same seed (FOUNDATION_V0_SEED = [0x42; 32]), same configs, same produced_at timestamp. Regeneration on any platform with the corrected binary must produce identical CIDs. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * chore(baseline-std): silence dead-code warnings + document rust.toml exclusion - Rename ctorN -> ctor_n (snake_case, fixes non_snake_case warning) - Add #[allow(dead_code)] to ctor0/ctor2 with explanatory comment; they are scaffolding for future N-ary predicate kinds, not bugs - Add comment to configs/rust.toml explaining it is intentionally excluded from the mint_all_baselines langs list — Rust baselines are owned by provekit-baseline-rust-std (#292) to avoid duplicate rust-std-baseline-v1 Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
Summary
First-mover validation of the per-language foundation-baseline workflow locked by #254 (rubric), #255 (federation), #256 (DSL survey). Mints
rust-std-baseline-v1.proofcovering 58 std::* builtins across 7 slabs, signed with the foundation v0 ed25519 seed.kind=disclaimermember; envelope metadata pinsdisclaimer_cid+baseline.{version, language, language_version, kit_version}per rubric §3.forall/eq/gte/ctor/num/strConstper docs(spec): formula DSL extension survey — predicate gaps + decisions (closes #256) #285's pre-launch lock. G1-G4 (lt/lte/between/member_of/or/not) defer to a follow-up PR after the cross-kit DSL extension.blake3-512:60dc813e…14ecblake3-512:76c278af…d5e4blake3-512:dae426aa…9bca1Files changed:
implementations/rust/provekit-baseline-rust-std/(new crate: lib + 7 slabs + mint binary + pin tests)implementations/rust/Cargo.toml(workspace member edit).provekit/baselines/rust-std-baseline-v1.proof(the signed catalog, 275 KB)docs/baselines/README.md+docs/baselines/rust.md.gitignore(allowlist.provekit/baselines/*.proof)AC checklist (per issue #257)
pinned_thresholds_mettest + mint binary exit-3 gate)signer_role: "foundation-baseline"baseline.version,baseline.language,baseline.language_version,baseline.kit_version,baseline.disclaimer_ciddisclaimer_base_starts_with_advisory_onlytest)docs/baselines/rust.mdexists with disclaimer + change logsubstrate_loads_baseline_with_no_errors— verifier round-trips every member with zero load errors)rust-std-baseline-v1.proofat.provekit/baselines/make conformancestill passes (rust pieces: catalog-verify OK, test-self-contracts 61/61, mint-rust round-trips to its existing pinned CID)provekit verify --baseline=rustCLI verb — deferred (substrate verifies the bytes; thin alias is a follow-up)Test plan
cargo test -p provekit-baseline-rust-std— 9/9 passing (6 lib + 3 pin + 1 substrate-load)cargo run -p provekit-baseline-rust-std --bin mint-rust-std-baseline— mints, byte-deterministic across two runs, compliance gate greenmake catalog-verify— passesmake test-self-contracts— 61/61 passing (no regression in existing rust self-contracts)make mint-rust— passes (existing self-contracts CID unchanged)DSL feedback for #256
The pilot did not hit any blockers on the locked surface. Where I'd have reached for G1-G4 (deferred):
lt/lteforVec::push's "len <= capacity" tightening — currently expressed asgte(capacity, len).or/notfor nullable returns (Map::get,Vec::pop,slice::first/last) — currently expressed as type-signature predicates returningOption.The 2-predicate floor was reachable on every one of the 58 builtins without G1-G4. Aspirational 3+ density was reachable on ~40 of them. G5/G7 (structural typing, aliasing) are explicitly deferred per the rubric and noted in the rust addendum.
🤖 Generated with Claude Code