fix(verifier): enforce ConsequentBundlePinned via targetProofCid lookup#13
Conversation
Closes the shim-poisoning vector promoted to a normative example in PR #10 (protocol/specs/2026-04-30-ir-formal-grammar.md, "Bridge target pinning"). Without this gate, an attacker can mint a poisoned `.proof` bundle whose contract member is byte-equal to the bridge's `targetContractCid`; the verifier accepts the substitution because syntactically the obligation looks discharged. With the gate, a bridge is bound not just to a contract shape but to a specific consequent bundle, and substitution is rejected before any discharge logic runs. Changes: - `MementoPool` gains `bundle_members: BTreeMap<String, BTreeSet<String>>` mapping `.proof` bundle CID to the set of member CIDs it contained. Multi-valued because the same member CID can legitimately appear in more than one bundle; last-writer-wins would silently swap honest for poisoned. `load_all_proofs` populates the map keyed by the bundle's content hash (`derived_full`). - `CallSite` gains `bridge_target_proof_cid: Option<String>`. `enumerate_callsites` reads it from `body.targetProofCid`; absent / empty maps to `None` for back-compat with bridges minted before the field was normative. - `resolve_target::run` gates the resolution on `BridgeDeclaration.ConsequentBundlePinned`. If `bridge_target_proof_cid = Some(expected)`, the resolved contract must be a member of `pool.bundle_members[expected]` or the bridge is rejected with `BridgeTargetProofCidMismatch`. A pinned bundle that isn't loaded at all is also a mismatch (fail-closed). If `bridge_target_proof_cid = None`, the bridge is accepted with a soft warning to stderr (matches existing `eprintln!("warning: ...")` pattern in `runner.rs` and `solvers/plan.rs`); back-compat path for pre-grammar bridges, but operators see what isn't being checked. Tests added in `tests/resolve_target.rs`: - `rejects_when_target_proof_cid_does_not_match_bundle`: shim-poisoning scenario A from the spec; member resolves but its bundle CID differs from the bridge's pin. Must reject. - `rejects_when_pinned_bundle_is_not_loaded`: pin references a bundle not present in the pool. Must reject. - `accepts_when_target_proof_cid_matches_bundle`: scenario B; pin matches. Must accept. - `accepts_when_target_proof_cid_is_none_back_compat`: legacy bridge with no field. Must accept (with stderr warning). Sanity-checked the tests are meaningful by reverting just `resolve_target.rs` and confirming the two reject-tests fail while the accept-tests still pass. 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 (5)
✨ 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 52 minutes and 26 seconds.Comment |
There was a problem hiding this comment.
Pull request overview
This PR updates the Rust verifier to enforce the bridge's forward pin (targetProofCid) when resolving a consequent contract, closing the shim-poisoning substitution path described in the spec. It fits into the verifier pipeline by carrying bundle-pin metadata from callsite enumeration through proof loading into resolve_target, where the actual gate is applied.
Changes:
- Added bundle membership tracking to
MementoPooland populated it while loading.prooffiles. - Extended
CallSiteto carrybridge_target_proof_cidand extractedtargetProofCidfrom bridge bodies. - Added
resolve_targetchecks and new tests for accept/reject cases around pinned bundles and back-compat behavior.
Reviewed changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
implementations/rust/provekit-verifier/tests/resolve_target.rs |
Adds unit tests for forward-pin enforcement, missing bundle rejection, matching bundle acceptance, and legacy fallback. |
implementations/rust/provekit-verifier/src/types.rs |
Extends verifier pipeline data structures with bundle-membership indexing and optional bridge proof-pin metadata. |
implementations/rust/provekit-verifier/src/resolve_target.rs |
Enforces that resolved target contracts come from the bridge-pinned .proof bundle, with a legacy warning path. |
implementations/rust/provekit-verifier/src/load_all_proofs.rs |
Records per-bundle member CIDs while loading proofs so resolve_target can validate pinned-bundle membership. |
implementations/rust/provekit-verifier/src/enumerate_callsites.rs |
Extracts targetProofCid from bridge JSON and carries it into generated CallSites. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| // bridges without this field are tolerated at load time but | ||
| // can't have ConsequentBundlePinned enforced; resolve_target | ||
| // emits a soft warning in that case. | ||
| let bridge_target_proof_cid = bbody | ||
| .get("targetProofCid") | ||
| .and_then(|v| v.as_str()) | ||
| .filter(|s| !s.is_empty()) | ||
| .map(|s| s.to_string()); |
| None => { | ||
| // Back-compat: legacy bridges that pre-date `targetProofCid` | ||
| // are loadable but cannot have ConsequentBundlePinned | ||
| // enforced. New bridges MUST set the field; flag the gap so | ||
| // operators can see what isn't being checked. | ||
| eprintln!( | ||
| "warning: bridge {} has no targetProofCid; \ | ||
| ConsequentBundlePinned not enforced (back-compat path)", | ||
| cs.bridge_ir_name | ||
| ); |
| pool.bundle_members | ||
| .entry(derived_full.clone()) | ||
| .or_default() | ||
| .insert(cid.clone()); |
![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: ae2c68c990
ℹ️ 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".
| let bridge_target_proof_cid = bbody | ||
| .get("targetProofCid") | ||
| .and_then(|v| v.as_str()) | ||
| .filter(|s| !s.is_empty()) |
There was a problem hiding this comment.
Filtering out empty targetProofCid values converts "" into None, which sends the callsite down the back-compat branch in resolve_target and skips ConsequentBundlePinned enforcement. This creates an easy bypass for the new pinning check whenever a bridge envelope is malformed-but-loadable with an empty string (field present but not usable), because the verifier will accept it with only a warning rather than fail closed.
Useful? React with 👍 / 👎.
…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
Closes the shim-poisoning vector promoted to a normative example in #10
(
protocol/specs/2026-04-30-ir-formal-grammar.md, § "Bridge targetpinning: the shim-poisoning vector"). The Rust verifier now enforces
INVARIANT BridgeDeclaration.ConsequentBundlePinned:The vector this closes
A bridge carries two outbound CIDs into the target side: the antecedent
(
targetContractCid) and the consequent (targetProofCid). Withoutenforcing the second pin, the verifier accepts any
.proofbundle thathappens to contain a contract member matching
targetContractCid,regardless of which binary the bundle was minted for. An attacker can
mint a poisoned bundle whose contract member is byte-equal to the
bridge's pin; syntactically the discharge looks fine, semantically the
guarantee is broken.
This PR adds the one CID-equality check the spec calls "the entire
mitigation": after resolving the consequent contract, the verifier
checks that the contract is a member of the bundle the bridge pinned,
and refuses any other bundle as a substitute.
What changed
MementoPooltracksbundle_members: BTreeMap<bundle_cid, set<member_cid>>.Multi-valued because the same member can legitimately appear in two
bundles (one honest, one poisoned); last-writer-wins would silently
swap them.
load_all_proofspopulates this from the.prooffile'scontent hash.
CallSitegainsbridge_target_proof_cid: Option<String>.enumerate_callsitesextracts it frombody.targetProofCid.resolve_target::rungates resolution on the pin: mismatch -> rejectwith
BridgeTargetProofCidMismatch { expected, actual }-shapederror.
Behavior on missing field
targetProofCidis REQUIRED by the current grammar, but bridges mintedbefore the field was normative MAY lack it. To preserve back-compat:
bridge_target_proof_cid = None-> bridge is accepted with a softwarning to stderr (
warning: bridge X has no targetProofCid; ConsequentBundlePinned not enforced). Matches the existingeprintln!("warning: ...")pattern inrunner.rs/solvers/plan.rs.bridge_target_proof_cid = Some(_)-> ConsequentBundlePinned isenforced fully. Mismatch is fail-closed.
New bridges from the current producer MUST set the field; the warning
makes the gap visible to operators rather than hiding it.
Test coverage added
In
implementations/rust/provekit-verifier/tests/resolve_target.rs:rejects_when_target_proof_cid_does_not_match_bundle-- specscenario A, the shim-poisoning case. Member resolves but its bundle
CID differs from the pin. Must reject.
rejects_when_pinned_bundle_is_not_loaded-- pin references abundle not in the pool. Must reject (fail-closed).
accepts_when_target_proof_cid_matches_bundle-- spec scenario B.Pin matches. Must accept.
accepts_when_target_proof_cid_is_none_back_compat-- legacybridge, no field. Must accept (soft-warning path).
Sanity-checked by reverting just the
resolve_target.rsgate andconfirming the two reject-tests fail while the two accept-tests still
pass.
Test plan
cargo test --release --manifest-path implementations/rust/Cargo.toml -p provekit-verifier --test resolve_target-- 12/12 passresolve_target.rs, confirm reject-tests now fail, restoresmt_emitter::var_with_empty_name_returns_err, fails onmaintoo)Related
targetProofCidattack to a normative example)2026-05-02-binary-attestation-protocol.mdadds the backpin (
binaryCid); together they close the two-pin loop documented inthe spec's "Two-pin closure" subsection.