[codex] Add polyglot bug zoo link exhibit#487
Conversation
|
Warning Rate limit exceeded
You’ve run out of usage credits. Purchase more in the billing tab. ⌛ 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)
WalkthroughThis pull request introduces BZ-SHAPE-007, a polyglot link-obligation specimen demonstrating cross-language verification between Go and Rust via ChangesPolyglot Link Obligation & LinkBundle Integration
Estimated code review effort🎯 4 (Complex) | ⏱️ ~45 minutes Possibly related PRs
Poem
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ 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. Comment |
|
@coderabbitai review |
✅ Actions performedReview triggered.
|
![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: db3c93fa5a
ℹ️ 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".
| Name: sig.Name, | ||
| OutBinding: ir.DefaultOutBinding, | ||
| Post: ir.And(), // true placeholder | ||
| Post: wrapFormulaForParams(parseContractPost(trimmed), sig.Params), |
There was a problem hiding this comment.
Changing //provekit:contract to emit post: nil (instead of the previous true placeholder) introduces false link failures for callers that omit post=... but call unconstrained callees. In discharge_obligation, the linker returns unprovable-obligation as soon as source post is absent, before it checks whether the target precondition is absent (vacuous case), so previously-clean edges now fail solely due to this serialization change.
Useful? React with 👍 / 👎.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 6
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
docs/contributing/build.md (1)
16-17:⚠️ Potential issue | 🟡 Minor | ⚡ Quick winInline comment for
cargo run --manifest-path bug-zoo/...is stale.Line 17 still reads
# Bug Zoo specimen/exposure/dropper checks, but line 90 has been updated to drop dropper closure receipts from the scope. The inline comment in the Make targets listing should be updated for consistency.✏️ Proposed fix
cargo run --manifest-path bug-zoo/Cargo.toml -- --all - # Bug Zoo specimen/exposure/dropper checks + # Bug Zoo specimen/exhibit/link-bundle/fixed-pair checks🤖 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 `@docs/contributing/build.md` around lines 16 - 17, Update the stale inline comment that follows the cargo invocation in the Make targets listing: change the comment text currently reading "# Bug Zoo specimen/exposure/dropper checks" to reflect the new scope (dropper closure receipts were removed); locate the line with the cargo command (cargo run --manifest-path bug-zoo/Cargo.toml -- --all) and replace the comment to correctly describe the remaining checks (e.g., "Bug Zoo specimen/exposure checks") so the comment matches the updated behavior described later in the file.
🧹 Nitpick comments (7)
examples/polyglot-rust-go/fixture-fail/go-caller/rust_callee.h (1)
1-1: 💤 Low valueConsider adding an include guard.
The header has no
#pragma onceor#ifndefguard. While the current cgo usage is single-inclusion, adding a guard is standard defensive practice.🛡️ Proposed fix
+#pragma once + int process(int n);🤖 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 `@examples/polyglot-rust-go/fixture-fail/go-caller/rust_callee.h` at line 1, The header rust_callee.h is missing an include guard; wrap its contents (the declaration of int process(int n);) with either a traditional `#ifndef/`#define/#endif pair using a unique macro (e.g., RUST_CALLEE_H) or add `#pragma` once at the top to prevent multiple inclusion; update the file to include one of these guards so the process(int) declaration is protected against double inclusion.examples/polyglot-rust-go/fixture-ok/go-caller/rust_callee.h (1)
1-1: 💤 Low valueConsider using
int32_tto match the Rusti32type exactly.
intis guaranteed ≥16 bits in C; on all real cgo targets it is 32 bits, but usingint32_t(from<stdint.h>) makes the correspondence with the Rusti32callee explicit and portable by contract.🔧 Proposed change
+#include <stdint.h> + -int process(int n); +int32_t process(int32_t n);🤖 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 `@examples/polyglot-rust-go/fixture-ok/go-caller/rust_callee.h` at line 1, The header currently declares the function as int process(int n) which can be ambiguous versus Rust's i32; change the signature to use fixed-width types by including <stdint.h> and declaring int32_t process(int32_t n) so the C prototype for function process and parameter n exactly matches the Rust i32 callee; update any callers to use int32_t as needed.examples/polyglot-rust-go/fixture-fail/go-caller/caller_fail.go (1)
13-17: 💤 Low valueRedundant
extern int process(int n);after the header include.
rust_callee.halready declaresprocess; the explicitexternre-declaration is a harmless but unnecessary duplicate. The same pattern appears incaller_ok.go.♻️ Proposed cleanup
/* `#include` "rust_callee.h" `#include` <stdint.h> -extern int process(int n); */🤖 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 `@examples/polyglot-rust-go/fixture-fail/go-caller/caller_fail.go` around lines 13 - 17, Remove the redundant explicit declaration "extern int process(int n);" that follows the `#include` "rust_callee.h" in caller_fail.go (and mirror the same change in caller_ok.go); rust_callee.h already declares process, so keep the `#include` "rust_callee.h" line and delete the duplicate extern declaration to avoid the unnecessary re-declaration.implementations/rust/provekit-cli/src/cmd_link.rs (1)
363-368: ⚡ Quick win
child.wait()result is discarded — non-zero subprocess exits aren't surfaced.If
provekit-lsp-gocrashes after sending some parse responses, the linker proceeds with whatever was collected and the user sees a "successful" (or partial-failure) link bundle with no indication that the lifter exited abnormally. Capture and check the exit status, and propagate as agather_and_linkerror when it's non-zero.🤖 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 `@implementations/rust/provekit-cli/src/cmd_link.rs` around lines 363 - 368, The code currently drops the child process exit value (child.wait()) after sending the shutdown request; capture the ExitStatus, check whether status.success() is true, and if not return or propagate an error from gather_and_link indicating the lifter exited non‑zero (include the ExitStatus or its code in the message). Update the block around shutdown_req/child.wait() to map wait errors into a gather_and_link error and to convert a non-success ExitStatus into a gather_and_link error so abnormal exits of provekit-lsp-go are surfaced to the caller (refer to the child variable, child.wait(), shutdown_req, and the gather_and_link caller).implementations/go/cmd/provekit-lsp-go/main.go (2)
732-764: ⚡ Quick win
findAheadFnSignaturereturns the first matching func in declaration order, not the nearest one to the annotation.The loop iterates
file.Declsin source/declaration order and returns on the first*ast.FuncDeclwhoselinefalls in the lookahead window(startLine+1, startLine+11]. If two annotations are within 10 lines of each other (e.g., adjacent contract annotations, or a contract followed by a small helper), the parameter scope of the wrong function could be selected. Tighten the match to "the next FuncDecl afterstartLine" — e.g., track the minimumline > startLinerather than first hit.♻️ Proposed tightening
- if file != nil { - for _, decl := range file.Decls { - fn, ok := decl.(*ast.FuncDecl) - if !ok || fn.Name == nil { - continue - } - line := fset.Position(fn.Pos()).Line - if line <= start || line > end+1 { - continue - } - return functionSignature{ - Name: fn.Name.Name, - Params: funcParams(fn.Type.Params), - }, true - } - } + if file != nil { + var best *ast.FuncDecl + bestLine := end + 2 + for _, decl := range file.Decls { + fn, ok := decl.(*ast.FuncDecl) + if !ok || fn.Name == nil { + continue + } + line := fset.Position(fn.Pos()).Line + if line <= start || line > end+1 { + continue + } + if line < bestLine { + bestLine = line + best = fn + } + } + if best != nil { + return functionSignature{ + Name: best.Name.Name, + Params: funcParams(best.Type.Params), + }, true + } + }🤖 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 `@implementations/go/cmd/provekit-lsp-go/main.go` around lines 732 - 764, findAheadFnSignature currently returns the first FuncDecl in file.Decls that falls in the lookahead window, which can pick the wrong function; change the loop to select the FuncDecl with the smallest fset.Position(fn.Pos()).Line that is > startLine (and <= end) instead of returning on first match — track a bestLine and bestFn during iteration, skip nil names as done now, and after the loop if bestFn != nil return functionSignature{Name: bestFn.Name.Name, Params: funcParams(bestFn.Type.Params)}, true; keep the fallback to findAheadFn(lines, startLine) unchanged.
645-647: 💤 Low valueSilent swallow of
parser.ParseFileerrors degrades parameter-scope quantification.When
parser.ParseFilefails (e.g., the source is partially edited inside an LSP session),fileisniland the fallbackfindAheadFnis taken infindAheadFnSignature, which returns no parameters — sowrapFormulaForParamsno longer wraps in anyForAllNamedand the parsedpostbecomes a formula with free variables. That contradicts the new test's expectation that contracts with annotations are always quantified. Consider at least logging/surfacing the parse error (or signaling a warning back through the existingwarningschannel) so callers can detect this degradation.🤖 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 `@implementations/go/cmd/provekit-lsp-go/main.go` around lines 645 - 647, Capture the error returned by parser.ParseFile (change "file, _ := parser.ParseFile(...)" to "file, err := parser.ParseFile(...)" ), and if err != nil send a descriptive warning into the existing warnings channel (or log it if warnings is unavailable) including the path and err; keep the rest of the logic but ensure callers are informed so findAheadFnSignature/wrapFormulaForParams can avoid silent degradation (reference token.NewFileSet, parser.ParseFile, findAheadFnSignature, wrapFormulaForParams, ForAllNamed and the warnings channel).bug-zoo/src/lib.rs (1)
129-151: ⚡ Quick winReject unknown keys in the new link-exhibit manifest blocks.
LinkExposureandFixedLinkExposurecurrently accept unknown YAML keys silently. BecausegoLspBinis optional and defaulted, a typo here degrades into a late setup/link failure instead of a parse-time error. Adding#[serde(deny_unknown_fields)]to these new structs would make specimen mistakes fail fast.🤖 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 `@bug-zoo/src/lib.rs` around lines 129 - 151, Add strict deserialization to the new manifest structs so typos are caught at parse time: annotate the LinkExposure and FixedLinkExposure structs with #[serde(deny_unknown_fields)] (in addition to the existing #[serde(rename_all = "camelCase")]) so unknown YAML keys cause a parse error rather than silently being ignored; update both struct declarations (LinkExposure and FixedLinkExposure) accordingly.
🤖 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.
Inline comments:
In
`@bug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/exhibit/cgo-rust-callee/harness/go-caller/caller_fail.go`:
- Line 3: Update the stale top-of-file comment that incorrectly states "calls
C.process(-1)" to accurately describe the actual behavior: the Go caller
forwards the supplied variable n to the C function via C.process(C.int(n));
either remove the misleading comment or replace it with a concise line such as
"Calls C.process with the provided n (C.process(C.int(n)))" so it matches the
inline comment near the C.process call and the variable n usage.
In
`@bug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/exhibit/cgo-rust-callee/harness/go-caller/go.mod`:
- Around line 1-3: The module path in go.mod is incorrect; replace the declared
module string so it reflects this harness's actual repository location rather
than the examples/ fixture. Edit the module declaration in go.mod (the single
"module ..." line) to a harness-scoped path such as
"bugzoo/species/bz-shape-007-polyglot-link-obligation/rust-go/exhibit/cgo-rust-callee/harness/go-caller"
(all-lowercase) so tooling like go list and repo-wide dependency resolution see
a unique, accurate module root.
In
`@bug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/fixed/cgo-rust-callee/harness/rust-callee/Cargo.toml`:
- Around line 1-7: The crate declares and uses the bare attribute
#[requires(...)] in src/lib.rs but Cargo.toml has no proc-macro dependency
providing that attribute, so compilation will fail; either add a proc-macro
contract crate that exports #[requires] (e.g., add a dependency that provides
the attribute to [dependencies]) or implement a shim stripping mechanism (e.g.,
a build script or attribute macro that replaces/removes #[requires]) and/or add
#[allow(dead_code)] where needed; update Cargo.toml to include the chosen
proc-macro crate and ensure the attribute macro name matches #[requires] used in
the source (or remove/replace the attribute in lib.rs).
In `@bug-zoo/src/lib.rs`:
- Around line 1417-1462: The helper mutates the checked-in file at bundle_path
and then restores it, causing race conditions; instead copy the project
directory to a unique temp directory (e.g., using tempfile::TempDir) and run the
provekit CLI against that temp copy (update where you build cmd and set
current_dir to the temp copy, not repo_root/project_path), then read the
produced link-bundle.json from the temp copy and remove any use of
restore_original_bundle/original_bundle for this run; keep references to
provekit_cli_command, cmd.arg("link"), bundle_path (use a temp_bundle_path
derived from the temp copy) and read_json(bundle_path.clone()) so the rest of
the logic reads from the temp output and the checked-in fixture is never
mutated.
In `@implementations/rust/provekit-cli/src/cmd_link.rs`:
- Around line 131-144: The function build_plan_and_registry currently treats
errors from SolversConfig::load the same as a missing config; change it so
build_plan_and_registry distinguishes Err(_) from Ok(None): call
SolversConfig::load(project_root) and match on the Result, returning Err up to
gather_and_link (or at minimum logging a clear warning with the error) when load
returns Err(e), only falling back to default z3 on Ok(None). Update callers
(e.g., gather_and_link) to accept a Result return from build_plan_and_registry
(or handle the propagated error) so malformed .provekit/config.toml is surfaced
instead of silently using registry::build_default_z3("z3").
- Around line 307-311: The fallback to contract_cid_from_go_decl is dead and
returns an empty string, so replace the unwrap_or_else(...) that uses
contract_cid_from_go_decl(decl) with explicit failure handling: when
contract_cids.and_then(...).and_then(...).map(...) yields None, either
return/propagate an Err from the surrounding function or log a warning and skip
with a clear message including the contract name; remove or disable
contract_cid_from_go_decl usage for CID lookup. Locate the expression using
contract_cids and the contract_cid_from_go_decl function to implement this
change (symbols: contract_cids, contract_cid_from_go_decl, decl, name) and
ensure the caller receives an error/notice instead of silently getting "" so
downstream filtering cannot drop contracts silently.
---
Outside diff comments:
In `@docs/contributing/build.md`:
- Around line 16-17: Update the stale inline comment that follows the cargo
invocation in the Make targets listing: change the comment text currently
reading "# Bug Zoo specimen/exposure/dropper checks" to reflect the new scope
(dropper closure receipts were removed); locate the line with the cargo command
(cargo run --manifest-path bug-zoo/Cargo.toml -- --all) and replace the comment
to correctly describe the remaining checks (e.g., "Bug Zoo specimen/exposure
checks") so the comment matches the updated behavior described later in the
file.
---
Nitpick comments:
In `@bug-zoo/src/lib.rs`:
- Around line 129-151: Add strict deserialization to the new manifest structs so
typos are caught at parse time: annotate the LinkExposure and FixedLinkExposure
structs with #[serde(deny_unknown_fields)] (in addition to the existing
#[serde(rename_all = "camelCase")]) so unknown YAML keys cause a parse error
rather than silently being ignored; update both struct declarations
(LinkExposure and FixedLinkExposure) accordingly.
In `@examples/polyglot-rust-go/fixture-fail/go-caller/caller_fail.go`:
- Around line 13-17: Remove the redundant explicit declaration "extern int
process(int n);" that follows the `#include` "rust_callee.h" in caller_fail.go
(and mirror the same change in caller_ok.go); rust_callee.h already declares
process, so keep the `#include` "rust_callee.h" line and delete the duplicate
extern declaration to avoid the unnecessary re-declaration.
In `@examples/polyglot-rust-go/fixture-fail/go-caller/rust_callee.h`:
- Line 1: The header rust_callee.h is missing an include guard; wrap its
contents (the declaration of int process(int n);) with either a traditional
`#ifndef/`#define/#endif pair using a unique macro (e.g., RUST_CALLEE_H) or add
`#pragma` once at the top to prevent multiple inclusion; update the file to
include one of these guards so the process(int) declaration is protected against
double inclusion.
In `@examples/polyglot-rust-go/fixture-ok/go-caller/rust_callee.h`:
- Line 1: The header currently declares the function as int process(int n) which
can be ambiguous versus Rust's i32; change the signature to use fixed-width
types by including <stdint.h> and declaring int32_t process(int32_t n) so the C
prototype for function process and parameter n exactly matches the Rust i32
callee; update any callers to use int32_t as needed.
In `@implementations/go/cmd/provekit-lsp-go/main.go`:
- Around line 732-764: findAheadFnSignature currently returns the first FuncDecl
in file.Decls that falls in the lookahead window, which can pick the wrong
function; change the loop to select the FuncDecl with the smallest
fset.Position(fn.Pos()).Line that is > startLine (and <= end) instead of
returning on first match — track a bestLine and bestFn during iteration, skip
nil names as done now, and after the loop if bestFn != nil return
functionSignature{Name: bestFn.Name.Name, Params:
funcParams(bestFn.Type.Params)}, true; keep the fallback to findAheadFn(lines,
startLine) unchanged.
- Around line 645-647: Capture the error returned by parser.ParseFile (change
"file, _ := parser.ParseFile(...)" to "file, err := parser.ParseFile(...)" ),
and if err != nil send a descriptive warning into the existing warnings channel
(or log it if warnings is unavailable) including the path and err; keep the rest
of the logic but ensure callers are informed so
findAheadFnSignature/wrapFormulaForParams can avoid silent degradation
(reference token.NewFileSet, parser.ParseFile, findAheadFnSignature,
wrapFormulaForParams, ForAllNamed and the warnings channel).
In `@implementations/rust/provekit-cli/src/cmd_link.rs`:
- Around line 363-368: The code currently drops the child process exit value
(child.wait()) after sending the shutdown request; capture the ExitStatus, check
whether status.success() is true, and if not return or propagate an error from
gather_and_link indicating the lifter exited non‑zero (include the ExitStatus or
its code in the message). Update the block around shutdown_req/child.wait() to
map wait errors into a gather_and_link error and to convert a non-success
ExitStatus into a gather_and_link error so abnormal exits of provekit-lsp-go are
surfaced to the caller (refer to the child variable, child.wait(), shutdown_req,
and the gather_and_link caller).
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro
Run ID: 5f7bda6f-b247-4988-92d1-f0cdb2fa13ec
📒 Files selected for processing (49)
.provekit/ci/accepted/go/blake3-512:3bc39a0377fbd0cef8da644fb97fd6b48f6f3468c8bee8ca7b94f45ff2e6aacaa3fcad1b3d5e2b3a7fff297cb4bcc3bdaf0e7d9bf733da42c591f405021f205b.job-result.json.provekit/ci/accepted/java/blake3-512:d647ecccb0831c607db377b7e096eb78e7b39dcbe4b1a44cc633c946d9605afb6bf56597cf266e41ec344a7bfc662f7c6d1ed790e05d3945beabe06da9b75298.job-result.json.provekit/ci/accepted/rust/blake3-512:b9698db898dc694764d694835837b9d1266eaf0d63c72a667aba21478d333d61ef140f3152b21692c0e2db7a7a3b03e7e90d4cd84c6aa7bc4d71a29af2cd7a74.job-result.jsonREADME.mdbug-zoo/README.mdbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/README.mdbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/exhibit/cgo-rust-callee/expected-diagnostic.txtbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/exhibit/cgo-rust-callee/harness/go-caller/caller_fail.gobug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/exhibit/cgo-rust-callee/harness/go-caller/go.modbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/exhibit/cgo-rust-callee/harness/go-caller/rust_callee.hbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/exhibit/cgo-rust-callee/harness/link-bundle.jsonbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/exhibit/cgo-rust-callee/harness/rust-callee/Cargo.tomlbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/exhibit/cgo-rust-callee/harness/rust-callee/src/lib.rsbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/exhibit/sat-witness.jsonbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/fixed/cgo-rust-callee/expected-diagnostic.txtbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/fixed/cgo-rust-callee/harness/go-caller/caller_ok.gobug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/fixed/cgo-rust-callee/harness/go-caller/go.modbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/fixed/cgo-rust-callee/harness/go-caller/rust_callee.hbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/fixed/cgo-rust-callee/harness/link-bundle.jsonbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/fixed/cgo-rust-callee/harness/rust-callee/Cargo.tomlbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/fixed/cgo-rust-callee/harness/rust-callee/src/lib.rsbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/kit-rpc/run-go-lsp.shbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/lab/harness/caller_test.gobug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/lab/harness/go.modbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/lab/harness/run.shbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/lab/library/README.mdbug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/specimen.yamlbug-zoo/src/lib.rsbug-zoo/tests/smoke.rsdocs/contributing/build.mddocs/explanation/bug-zoo.mddocs/explanation/use-cases.mddocs/how-to/bug-zoo.mddocs/reference/per-language-status.mddocs/reference/protocol-extensions.mdexamples/polyglot-rust-go/README.mdexamples/polyglot-rust-go/fixture-fail/go-caller/caller_fail.goexamples/polyglot-rust-go/fixture-fail/go-caller/rust_callee.hexamples/polyglot-rust-go/fixture-fail/link-bundle.jsonexamples/polyglot-rust-go/fixture-ok/go-caller/caller_ok.goexamples/polyglot-rust-go/fixture-ok/go-caller/rust_callee.hexamples/polyglot-rust-go/fixture-ok/link-bundle.jsonexamples/polyglot-rust-go/fixture-ok/rust-callee/src/lib.rsimplementations/go/cmd/provekit-lsp-go/cross_kit_call_edges_test.goimplementations/go/cmd/provekit-lsp-go/main.goimplementations/go/cmd/provekit-lsp-go/main_test.goimplementations/rust/provekit-cli/src/cmd_link.rsimplementations/rust/provekit-linker/src/lib.rsimplementations/rust/provekit-linker/tests/discharge_obligation.rs
| @@ -0,0 +1,26 @@ | |||
| // caller_fail.go - FAILURE CASE | |||
| // | |||
| // This Go file calls C.process(-1) without any guard. | |||
There was a problem hiding this comment.
Stale comment claims C.process(-1) but the code passes n directly.
Line 3 states "calls C.process(-1)" while the actual call at line 25 is C.process(C.int(n)) — the function forwards whatever n was supplied. The accurate description is already in the inline comment at line 22.
📝 Proposed fix
-// This Go file calls C.process(-1) without any guard.
+// This Go file calls C.process(n) without guarding that n > 0.📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| // This Go file calls C.process(-1) without any guard. | |
| // This Go file calls C.process(n) without guarding that n > 0. |
🤖 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
`@bug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/exhibit/cgo-rust-callee/harness/go-caller/caller_fail.go`
at line 3, Update the stale top-of-file comment that incorrectly states "calls
C.process(-1)" to accurately describe the actual behavior: the Go caller
forwards the supplied variable n to the C function via C.process(C.int(n));
either remove the misleading comment or replace it with a concise line such as
"Calls C.process with the provided n (C.process(C.int(n)))" so it matches the
inline comment near the C.process call and the variable n usage.
| module github.com/tsavo/provekit/examples/polyglot-rust-go/fixture-fail/go-caller | ||
|
|
||
| go 1.22 |
There was a problem hiding this comment.
Module path is mismatched with the physical location.
The declared module path github.com/tsavo/provekit/examples/polyglot-rust-go/fixture-fail/go-caller refers to the examples/ fixture directory, but this go.mod lives under the bug-zoo/ exhibit harness. This creates a naming conflict with the actual examples/polyglot-rust-go/fixture-fail/go-caller module, and can confuse go list, dependency resolution, and repo-wide tooling that traverses module roots.
The module path should reflect the actual exhibit location, similarly to how the lab harness uses bugzoo/polyglot-link-lab.
🐛 Proposed fix
-module github.com/tsavo/provekit/examples/polyglot-rust-go/fixture-fail/go-caller
+module bugzoo/polyglot-link-obligation/exhibit/go-caller
go 1.22📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| module github.com/tsavo/provekit/examples/polyglot-rust-go/fixture-fail/go-caller | |
| go 1.22 | |
| module bugzoo/polyglot-link-obligation/exhibit/go-caller | |
| go 1.22 |
🤖 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
`@bug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/exhibit/cgo-rust-callee/harness/go-caller/go.mod`
around lines 1 - 3, The module path in go.mod is incorrect; replace the declared
module string so it reflects this harness's actual repository location rather
than the examples/ fixture. Edit the module declaration in go.mod (the single
"module ..." line) to a harness-scoped path such as
"bugzoo/species/bz-shape-007-polyglot-link-obligation/rust-go/exhibit/cgo-rust-callee/harness/go-caller"
(all-lowercase) so tooling like go list and repo-wide dependency resolution see
a unique, accurate module root.
| [package] | ||
| name = "rust-callee" | ||
| version = "0.1.0" | ||
| edition = "2021" | ||
|
|
||
| [lib] | ||
| crate-type = ["cdylib"] |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# 1. Find any Cargo.toml files in ancestor directories of the new crate
fd "Cargo.toml" bug-zoo --max-depth 8 | sort
# 2. Check for workspace membership or [workspace] sections
rg -l '\[workspace\]' bug-zoo/
# 3. Search for any dependency providing the `requires` proc-macro
rg -n 'requires|contracts|prusti' bug-zoo/ --include="*.toml"
# 4. Also check how the fixture-ok callee resolves it
rg -n 'requires|contracts|prusti' examples/polyglot-rust-go/ --include="*.toml"Repository: TSavo/provekit
Length of output: 1211
🏁 Script executed:
#!/bin/bash
# 1. Check root bug-zoo Cargo.toml for workspace
echo "=== ROOT CARGO.TOML ==="
cat bug-zoo/Cargo.toml
echo -e "\n=== REVIEWED CRATE CARGO.TOML ==="
cat bug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/fixed/cgo-rust-callee/harness/rust-callee/Cargo.toml
# 2. Check paired lib.rs to confirm #[requires] usage
echo -e "\n=== PAIRED LIB.RS ==="
cat bug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/fixed/cgo-rust-callee/harness/rust-callee/src/lib.rs 2>/dev/null || echo "lib.rs not found"
# 3. Search for proc-macro deps using correct rg syntax
echo -e "\n=== SEARCHING FOR REQUIRES/CONTRACTS IN TOML FILES ==="
rg 'requires|contracts|prusti' bug-zoo/ -t toml -A 2
echo -e "\n=== CHECKING EXAMPLES FIXTURE ==="
rg 'requires|contracts|prusti' examples/polyglot-rust-go/ -t toml -A 2 2>/dev/null || echo "examples directory search completed"Repository: TSavo/provekit
Length of output: 1570
🏁 Script executed:
#!/bin/bash
# Check parent workspace structure
echo "=== PARENT WORKSPACE (implementations/rust) ==="
cat implementations/rust/Cargo.toml 2>/dev/null | head -100
echo -e "\n=== SEARCH FOR PROC-MACRO IN PARENT WORKSPACE ==="
rg 'requires|contracts|prusti' implementations/rust/ -t toml -A 2 2>/dev/null | head -50
# Also check if there's a Cargo.lock at any level that might provide transitive deps
echo -e "\n=== CHECKING FOR CARGO.LOCK FILES ==="
fd "Cargo.lock" . --max-depth 5Repository: TSavo/provekit
Length of output: 6635
🏁 Script executed:
#!/bin/bash
# Check provekit-macros structure
echo "=== PROVEKIT-MACROS CARGO.TOML ==="
cat implementations/rust/provekit-macros/Cargo.toml 2>/dev/null
echo -e "\n=== PROVEKIT-MACROS LIB.RS (first 100 lines) ==="
head -100 implementations/rust/provekit-macros/lib.rs 2>/dev/null || echo "Not found"
# Check if reviewed crate has build.rs
echo -e "\n=== BUILD.RS IN REVIEWED CRATE ==="
cat bug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/fixed/cgo-rust-callee/harness/rust-callee/build.rs 2>/dev/null || echo "No build.rs found"
# Check directory contents of reviewed crate
echo -e "\n=== FILES IN REVIEWED CRATE ==="
find bug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/fixed/cgo-rust-callee/harness/rust-callee -type f
# Check if the parent crate (bug-zoo itself) might have build logic
echo -e "\n=== BUILD.RS IN BUG-ZOO ROOT ==="
cat bug-zoo/build.rs 2>/dev/null || echo "No build.rs in bug-zoo root"Repository: TSavo/provekit
Length of output: 1214
#[requires] attribute lacks a proc-macro dependency — crate will fail to compile.
The paired src/lib.rs uses #[requires(n > 0)], a bare attribute not provided by any declared dependency. The provekit-macros crate is a proc-macro, but it only exports #[provekit::contract], #[provekit::implement], and #[provekit::verify] — not #[requires]. No proc-macro dependency is listed in [dependencies], and the parent workspace (implementations/rust) does not provide one either. Rust compilation will fail with cannot find attribute 'requires'.
If the intent is to defer the attribute to a post-build lifter (never compiling it with rustc), a #[allow(dead_code)] shim or explicit stripping mechanism must be implemented. Otherwise, add the required dependency (e.g., contracts, prusti-contracts, or custom) to [dependencies].
🤖 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
`@bug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation/rust-go/fixed/cgo-rust-callee/harness/rust-callee/Cargo.toml`
around lines 1 - 7, The crate declares and uses the bare attribute
#[requires(...)] in src/lib.rs but Cargo.toml has no proc-macro dependency
providing that attribute, so compilation will fail; either add a proc-macro
contract crate that exports #[requires] (e.g., add a dependency that provides
the attribute to [dependencies]) or implement a shim stripping mechanism (e.g.,
a build script or attribute macro that replaces/removes #[requires]) and/or add
#[allow(dead_code)] where needed; update Cargo.toml to include the chosen
proc-macro crate and ensure the attribute macro name matches #[requires] used in
the source (or remove/replace the attribute in lib.rs).
| let bundle_path = project_path.join("link-bundle.json"); | ||
| let original_bundle = std::fs::read(&bundle_path).ok(); | ||
|
|
||
| let mut cmd = provekit_cli_command(&repo_root)?; | ||
| if trace_enabled() { | ||
| cmd.env("PROVEKIT_CLI_TRACE", "1"); | ||
| cmd.stderr(Stdio::inherit()); | ||
| } | ||
| cmd.arg("link").arg(&project_arg).current_dir(&repo_root); | ||
| if let Some(go_lsp_bin) = go_lsp_bin { | ||
| let go_lsp_path = specimen_dir.join(go_lsp_bin); | ||
| let go_lsp_path = go_lsp_path.canonicalize().unwrap_or(go_lsp_path); | ||
| cmd.arg("--go-lsp-bin").arg(go_lsp_path); | ||
| } | ||
|
|
||
| let started = Instant::now(); | ||
| trace_log(format!( | ||
| "provekit link start id={id} project={}", | ||
| project_arg.display() | ||
| )); | ||
| let output = cmd | ||
| .output() | ||
| .map_err(|e| format!("spawn provekit link for `{id}`: {e}"))?; | ||
| trace_log(format!( | ||
| "provekit link exit id={id} status={} elapsed={:?}", | ||
| output.status, | ||
| started.elapsed() | ||
| )); | ||
|
|
||
| let stdout = String::from_utf8_lossy(&output.stdout); | ||
| let stderr = String::from_utf8_lossy(&output.stderr); | ||
| let exit_code = output.status.code().unwrap_or(EXIT_USER_ERROR as i32); | ||
| if !matches!(exit_code, 0 | 1) { | ||
| restore_original_bundle(&bundle_path, original_bundle.as_deref()); | ||
| return Err(format!( | ||
| "provekit link returned unexpected exit {exit_code} for `{id}`\nstdout:\n{stdout}\nstderr:\n{stderr}" | ||
| )); | ||
| } | ||
|
|
||
| let bundle = read_json(bundle_path.clone()).map_err(|error| { | ||
| restore_original_bundle(&bundle_path, original_bundle.as_deref()); | ||
| format!( | ||
| "read provekit link bundle for `{id}`: {error}\nstdout:\n{stdout}\nstderr:\n{stderr}" | ||
| ) | ||
| })?; | ||
| restore_original_bundle(&bundle_path, original_bundle.as_deref()); |
There was a problem hiding this comment.
Avoid using the checked-in link-bundle.json as temporary output.
This helper overwrites project/link-bundle.json, reads it back, and then restores whatever bytes were there before the run. That makes the zoo non-reentrant: overlapping runs can save/restore each other’s bundle, compare against transient output, or leave the fixture dirty. The new smoke test that reads the fixed bundle is also exposed to this race under parallel test execution. Please run provekit link in a temp project copy, or teach it to emit to a unique temp path instead of mutating the checked-in fixture in place.
Also applies to: 1489-1495
🤖 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 `@bug-zoo/src/lib.rs` around lines 1417 - 1462, The helper mutates the
checked-in file at bundle_path and then restores it, causing race conditions;
instead copy the project directory to a unique temp directory (e.g., using
tempfile::TempDir) and run the provekit CLI against that temp copy (update where
you build cmd and set current_dir to the temp copy, not repo_root/project_path),
then read the produced link-bundle.json from the temp copy and remove any use of
restore_original_bundle/original_bundle for this run; keep references to
provekit_cli_command, cmd.arg("link"), bundle_path (use a temp_bundle_path
derived from the temp copy) and read_json(bundle_path.clone()) so the rest of
the logic reads from the temp output and the checked-in fixture is never
mutated.
| fn build_plan_and_registry(project_root: &Path) -> (SolverPlan, Registry) { | ||
| if let Ok(Some(sc)) = SolversConfig::load(project_root) { | ||
| trace_log(format!( | ||
| "solver config loaded from {}/.provekit/config.toml", | ||
| project_root.display() | ||
| )); | ||
| return (SolverPlan::from_config(&sc), registry::build(&sc)); | ||
| } | ||
| trace_log("solver config not found; using default z3 registry"); | ||
| ( | ||
| SolverPlan::Single("z3".into()), | ||
| registry::build_default_z3("z3"), | ||
| ) | ||
| } |
There was a problem hiding this comment.
Silent fallback on SolversConfig::load errors masks malformed config.
if let Ok(Some(sc)) = SolversConfig::load(project_root) collapses the Err(_) and Ok(None) arms into the same default-z3 path, but they have very different meanings — a malformed .provekit/config.toml would now silently behave as if it didn't exist, potentially masking user intent (custom solver plan) and producing confusing link verdicts. Surface the error explicitly (as a Result returned from gather_and_link) or at least emit a clearly labeled warning so it isn't conflated with the legitimate "no config present" case.
🛡️ Proposed change
-fn build_plan_and_registry(project_root: &Path) -> (SolverPlan, Registry) {
- if let Ok(Some(sc)) = SolversConfig::load(project_root) {
- trace_log(format!(
- "solver config loaded from {}/.provekit/config.toml",
- project_root.display()
- ));
- return (SolverPlan::from_config(&sc), registry::build(&sc));
- }
- trace_log("solver config not found; using default z3 registry");
- (
- SolverPlan::Single("z3".into()),
- registry::build_default_z3("z3"),
- )
-}
+fn build_plan_and_registry(project_root: &Path) -> Result<(SolverPlan, Registry), String> {
+ match SolversConfig::load(project_root) {
+ Ok(Some(sc)) => {
+ trace_log(format!(
+ "solver config loaded from {}/.provekit/config.toml",
+ project_root.display()
+ ));
+ Ok((SolverPlan::from_config(&sc), registry::build(&sc)))
+ }
+ Ok(None) => {
+ trace_log("solver config not found; using default z3 registry");
+ Ok((
+ SolverPlan::Single("z3".into()),
+ registry::build_default_z3("z3"),
+ ))
+ }
+ Err(e) => Err(format!("load solver config: {e}")),
+ }
+}🤖 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 `@implementations/rust/provekit-cli/src/cmd_link.rs` around lines 131 - 144,
The function build_plan_and_registry currently treats errors from
SolversConfig::load the same as a missing config; change it so
build_plan_and_registry distinguishes Err(_) from Ok(None): call
SolversConfig::load(project_root) and match on the Result, returning Err up to
gather_and_link (or at minimum logging a clear warning with the error) when load
returns Err(e), only falling back to default z3 on Ok(None). Update callers
(e.g., gather_and_link) to accept a Result return from build_plan_and_registry
(or handle the propagated error) so malformed .provekit/config.toml is surfaced
instead of silently using registry::build_default_z3("z3").
| let cid = contract_cids | ||
| .and_then(|cids| cids.get(&name)) | ||
| .and_then(|cid| cid.as_str()) | ||
| .map(str::to_string) | ||
| .unwrap_or_else(|| contract_cid_from_go_decl(decl)); |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Look for any "cid" field emitted on Go declarations from ir.MarshalDeclarations
# in the symbolic IR package, and check the test fixtures for declaration.cid usage.
rg -nP --type=go -C3 '"cid"'
rg -nP --type=go -C3 '\bMarshalDeclarations\b'
ast-grep --pattern $'type ContractDeclaration struct {
$$$
}'Repository: TSavo/provekit
Length of output: 15196
🏁 Script executed:
#!/bin/bash
# Examine the Rust implementation of contract_cid_from_go_decl
cat -n implementations/rust/provekit-cli/src/cmd_link.rs | sed -n '385,405p'Repository: TSavo/provekit
Length of output: 643
🏁 Script executed:
#!/bin/bash
# Get context around lines 307-311 to understand the fallback logic
cat -n implementations/rust/provekit-cli/src/cmd_link.rs | sed -n '300,320p'Repository: TSavo/provekit
Length of output: 1139
🏁 Script executed:
#!/bin/bash
# Look at the Declaration struct definition in Rust to see what fields it has
rg -A 20 'struct.*Declaration' implementations/rust/provekit-cli/src/cmd_link.rsRepository: TSavo/provekit
Length of output: 40
🏁 Script executed:
#!/bin/bash
# Check if there's a cid field being added to the Go JSON during serialization
rg -n 'cid' implementations/go/provekit-ir-symbolic/ir/canonicalize.go -C 5Repository: TSavo/provekit
Length of output: 40
🏁 Script executed:
#!/bin/bash
# Check the Declaration type definition in the Go IR to see if cid is added during marshaling
rg -B 5 -A 15 'type Declaration struct' implementations/go/provekit-ir-symbolic/ir/Repository: TSavo/provekit
Length of output: 40
The fallback contract_cid_from_go_decl is dead code: it will always return an empty string.
Go declarations emitted via ir.MarshalDeclarations do not include a per-declaration cid field. The Go ContractDeclaration struct (property.go) contains only Name, OutBinding, Pre, Post, Inv, and Evidence—no cid. The fallback at line 311 attempts to read decl.get("cid"), but this key will never exist in the JSON output, so the function always returns "". This causes silent contract drops via downstream filtering.
Either remove the fallback and require all contracts to be present in the contractCids map, or surface an error/warning when the map lookup fails instead of silently using an empty CID.
🤖 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 `@implementations/rust/provekit-cli/src/cmd_link.rs` around lines 307 - 311,
The fallback to contract_cid_from_go_decl is dead and returns an empty string,
so replace the unwrap_or_else(...) that uses contract_cid_from_go_decl(decl)
with explicit failure handling: when
contract_cids.and_then(...).and_then(...).map(...) yields None, either
return/propagate an Err from the surrounding function or log a warning and skip
with a clear message including the contract name; remove or disable
contract_cid_from_go_decl usage for CID lookup. Locate the expression using
contract_cids and the contract_cid_from_go_decl function to implement this
change (symbols: contract_cids, contract_cid_from_go_decl, decl, name) and
ensure the caller receives an error/notice instead of silently getting "" so
downstream filtering cannot drop contracts silently.
Summary
provekit link.linkExhibits, LinkBundle red/green checks, and separateproofIrCidsvsreceiptCidsreporting.Why
The zoo story should be honest: lab shows the bug shape with no ProvekIt workflow, exhibit proves ProvekIt catches the missing cross-kit edge, and fixed proves the positive is not false by closing the same edge rather than deleting it.
Validation
go test ./cmd/provekit-lsp-go -count=1cargo check --manifest-path implementations/rust/provekit-cli/Cargo.tomlcargo test --manifest-path implementations/rust/provekit-cli/Cargo.toml --test polyglot_smokecargo test --manifest-path implementations/rust/provekit-linker/Cargo.tomlcargo run --manifest-path bug-zoo/Cargo.toml -- bug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation --jsonPROVEKIT_BUG_ZOO_TRACE=1 cargo run --manifest-path bug-zoo/Cargo.toml -- bug-zoo/species/BZ-SHAPE-007-polyglot-link-obligation --jsoncargo test --manifest-path bug-zoo/Cargo.tomlgit diff --checkgit diff --cached --checkSummary by CodeRabbit
New Features
provekit linkDocumentation
Tests