[kani] Upgrade verifier to 0.67.0 - #3645
Conversation
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA). View this failed invocation of the CLA check for more information. For the most up to date status, view the checks section at the bottom of the pull request. |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #3645 +/- ##
=======================================
Coverage 91.89% 91.89%
=======================================
Files 20 20
Lines 6122 6122
=======================================
Hits 5626 5626
Misses 496 496 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
cef5c04 to
2c33905
Compare
|
@codex review Please review current head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
|
Security review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
![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: 2c3390532c
ℹ️ 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".
| - **Compiler and documentation compatibility:** Kani 0.67.0 bundles | ||
| `rustc 1.93.0-nightly (53732d5e0 2025-11-20)`. Current proof comments | ||
| cite the versioned Rust 1.93.0 Reference and standard-library | ||
| documentation only for guarantees that already applied to that compiler |
There was a problem hiding this comment.
This claims the proof comments cite versioned Rust 1.93.0 documentation, but the premises in prove_dst_layout_extend still link to the moving, unversioned https://doc.rust-lang.org/reference/... pages (layout.rs:2078 and layout.rs:2093). Those links can acquire guarantees newer than Kani's bundled compiler, so the recorded compatibility assertion is not auditable; pin these proof citations to an applicable version such as 1.93.0 before making this claim.
AGENTS.md reference: zerocopy/AGENTS.md:L37-L38
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. Both prove_dst_layout_extend citations are pinned to the Rust 1.93.0 Reference, and the validation guidance now treats the workflow Kani pin as the sole version record and explains how to inspect its bundled compiler before changing citations.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| - **Compiler and documentation compatibility:** Kani 0.67.0 bundles | ||
| `rustc 1.93.0-nightly (53732d5e0 2025-11-20)`. Current proof comments | ||
| cite the versioned Rust 1.93.0 Reference and standard-library | ||
| documentation only for guarantees that already applied to that compiler | ||
| snapshot. When changing the Kani pin, recheck both this recorded compiler | ||
| version and every proof premise that depends on versioned language or |
There was a problem hiding this comment.
When the scheduled roll_kani job runs, its update step changes only kani-version in .github/workflows/ci.yml (lines 201–214), leaving this hardcoded Kani and rustc version untouched. The next successful bot roll will therefore make these validation instructions stale despite explicitly requiring the recorded compiler version to be rechecked; extend that workflow to update and validate this metadata, or avoid duplicating the pinned version here.
AGENTS.md reference: zerocopy/AGENTS.md:L37-L38
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The duplicated Kani and rustc version strings were removed from the guidance. The workflow pin is now the sole Kani version record, and the document gives commands for inspecting that release and its bundled compiler when the pin changes.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| - **Domain:** Document whether a proof is universal, target-specific, | ||
| or bounded by a concrete allocation or collection size. State both | ||
| what is covered and what is not covered. |
There was a problem hiding this comment.
Target specificity and input bounds are simultaneous dimensions, not alternatives: for example, prove_dst_layout_extend is target/compiler-specific while its generator also silently excludes align == THEORETICAL_MAX_ALIGN via layout.rs:1964. The current “universal, target-specific, or bounded” wording permits documenting only one dimension and concealing exclusions like this boundary; require each harness to state its target/compiler/features and all bounds and assumptions independently.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The proof checklist now requires every harness to state each axis independently: target/toolchain, features, input bounds and assumptions, and layout/randomization scope. Existing proof-family comments and PR descriptions were updated with the exact shared CI configuration and their family-specific bounds.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| - **Oracles:** Prefer a safe Rust language or standard-library operation | ||
| as the source of expected behavior. If no such oracle exists, isolate | ||
| the manual oracle, state its normative basis, and explain both its | ||
| independence from the code under proof and its limitations. If the | ||
| predicate merely restates a zerocopy acceptance policy, label it as a | ||
| policy oracle rather than evidence of Rust-level validity. |
There was a problem hiding this comment.
The independence requirement is currently conditional on falling back to a manual oracle, so a proof may treat any safe or standard-library operation as authoritative even when it shares the implementation mechanism under test. This matters in the existing prove_split_at_unchecked harness: its expected mutable right pointer is computed with unsafe ptr.add(mid) (byte_slice.rs:402–403), the same primitive used by the implementation, instead of comparing against safe split_at_mut. Require independence for every oracle category and use the available safe slice operation here.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. Oracle independence is now required for every oracle category, not only manual predicates. The split proofs derive expected partitions and pointers with safe slice::split_at, and expected mutable effects with safe slice::split_at_mut; the same independent-oracle rule is documented across the proof families.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| - **Bit validity:** `kani::any::<T>()` produces only valid instances of | ||
| `T`. To verify a byte validator, generate arbitrary bytes and | ||
| construct `T` only after the validator accepts them. |
There was a problem hiding this comment.
When the validator has a bug and accepts bytes that are not a valid representation of T, treating that acceptance as permission to construct T can itself introduce undefined behavior into the proof harness; the following soundness-boundary paragraph explicitly acknowledges that Kani does not completely check invalid values. A validator proof should compare its decision with an independent language, safe-library, or explicitly labeled policy predicate, and should construct T only through an independently safe checked operation—not merely because the implementation under proof returned success.
AGENTS.md reference: zerocopy/AGENTS.md:L13-L17
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. validate_and_read_sized! now receives an Option<T> produced by an independent safe operation. It compares the raw validator over every candidate byte pattern, but invokes the public read only in the independently safe Some(T) branch; rejected/invalid public-read paths are explicitly outside these harnesses.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
2c33905 to
ca0e3c3
Compare
|
@codex review Please review current head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
|
Security review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ca0e3c3772
ℹ️ 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".
| - **Oracles:** Every oracle must be independent of the implementation | ||
| under proof. Prefer a safe Rust language or standard-library | ||
| operation whose documented contract directly supplies the expected | ||
| behavior. Do not call the target, reuse its zerocopy helper or policy, | ||
| or manually reconstruct the same unchecked operation. For every |
There was a problem hiding this comment.
The current head still contradicts this new requirement: prove_split_at_unchecked in src/byte_slice.rs derives the expected right pointer with unsafe ptr.add(mid) (lines 387–388 and 402–403), which is also the primitive used by the mutable implementation at lines 245–295, rather than obtaining the expected partitions from safe slice::split_at. Thus a shared pointer-arithmetic/modeling defect can affect both the target and its oracle. Fresh evidence relative to the resolved thread is that ca0e3c37 retains this unchanged harness; replace these expected values with the safe standard-library split before presenting this as the repository's oracle rule.
AGENTS.md reference: zerocopy/AGENTS.md:L37-L38
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the dependent split-proof revision. Checked and unchecked slice, Ref, and RefMut proofs now obtain result classification and expected partitions from safe Rust 1.93 split_at_checked, split_at, or split_at_mut; expected mutation frames also use safe slice operations. The oracle no longer reconstructs the expected right pointer with raw add.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| - **Domain:** Document every scope dimension independently: the | ||
| symbolic input domain; concrete size, allocation, loop, and unwind | ||
| bounds; assumptions and excluded boundary cases; Kani and bundled | ||
| compiler selection; target and data model; enabled features and | ||
| verifier flags; randomized-layout count or seed; the established | ||
| properties; and explicit non-goals. Shared configuration may be | ||
| factored into a nearby family or module scope only when every covered | ||
| harness refers to it unambiguously. |
There was a problem hiding this comment.
No existing proof family implements the scope documentation required here. For example, layout.rs silently excludes align == THEORETICAL_MAX_ALIGN at line 1964 and rejects branches via assume(false) plus diverging loops at lines 2019–2041, while the byte-order proof checks only one deterministic RNG iteration because RAND_ITERS == 1 under Kani (byteorder.rs:1287–1308). Fresh evidence relative to the resolved thread is that current head contains no claimed proof-family scope comments or kani::cover! witnesses, so reviewers still cannot distinguish these bounded checks from universal theorems; add the required per-family domain, exclusions, established properties, and non-goals alongside the harnesses.
AGENTS.md reference: zerocopy/AGENTS.md:L37-L38
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed across the dependent proof revisions. The layout family now documents each generator domain, pruning boundary, resource and unwind bound, oracle limitation, and harness theorem; common generation/checking is factored, covers witness the retained and excluded partitions, and the text explicitly excludes the custom/nested-DST algorithm issue in #3630 without inferring its failing partition.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
49c1349 to
7f2a7ba
Compare
|
@codex review Please review current head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 7f2a7ba668
ℹ️ 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".
| - **Recorded toolchain audit for the current workflow pin:** On 2026-09-08, | ||
| `kani-compiler --version --verbose` reported `rustc 1.93.0-nightly`, commit | ||
| `53732d5e076329a62f71d3c6901886ce8a71e812` dated 2025-11-20, LLVM 21.1.5, |
There was a problem hiding this comment.
The scheduled roll_kani job still changes only the kani-version field in .github/workflows/ci.yml, so its next successful roll will leave this newly added compiler/CBMC audit—and the Kani 0.67/Rust 1.93 scope recorded in layout.rs—describing the previous verifier while CI runs the new one, despite lines 149–151 requiring replacement and revalidation. Fresh evidence relative to the resolved thread is that the current head reintroduces explicit toolchain versions and audit metadata without extending the pin-only roller; either update all recorded metadata during rolls or avoid duplicating version-specific claims.
AGENTS.md reference: zerocopy/AGENTS.md:L37-L38
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The scheduled roller intentionally updates only the executable pin, while ci/check_actions.sh requires exactly one canonical workflow-pin candidate and one canonical audit label with equal SemVer values. Malformed, duplicate, or mismatched candidates fail closed; the roller PR body requires human revalidation before advancing the audit label.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| #[kani::unwind(1)] | ||
| fn prove_dst_layout_extend_dst_panics() { | ||
| let base: DstLayout = kani::any(); | ||
| let (base, _) = any_slice_dst_layout(); |
There was a problem hiding this comment.
For slice-DST bases, this harness obtains the expected result solely by calling DstLayout::extend under #[kani::should_panic]; it supplies neither an independent safe/language/standard-library oracle nor an explicitly labeled policy oracle. The newly added scope comment itself acknowledges that this proves only the existence of some assertion-class failure for some generated input, so a different assertion failure could keep the harness passing after the intended DST-base panic disappears. Since extend also makes no contract-level guarantees for fragments that cannot form a valid repr(C) type, treat this only as a clearly labeled implementation-policy regression or replace it with a discriminating oracle rather than presenting it as proof evidence.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The harness is renamed regression_dst_base_extend_has_some_assertion_failure and explicitly documented as only a coarse existential assertion-class signal. It is isolated as a negative implementation-policy regression and excluded from positive theorem or contract evidence.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
|
Security review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
7f2a7ba to
545c97a
Compare
|
@codex review Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
|
You have reached your Codex usage limits for security reviews. Please try again later. |
|
Codex Review: Didn't find any major issues. Nice work! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
There was a problem hiding this comment.
Did you miss #3645 (comment)? Make sure to check top-level comments too.
There was a problem hiding this comment.
Yes. That top-level request was implemented by splitting the mechanical Kani upgrade from the layout-proof change into #3645 and #3661, and it already has a disclosed top-level response. I have also changed the monitor to fetch each PR's complete top-level conversation on every pass, in addition to review bodies and inline comments, so older unchanged conversation comments cannot disappear behind an incremental cutoff.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
753348d to
973b5e5
Compare
|
Done. The current #3645 revision is limited to the Kani 0.67, CI, tooling, and validation-documentation changes; it contains no Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
|
@codex review Please review current head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
|
You have reached your Codex usage limits for security reviews. Please try again later. |
973b5e5 to
1cc864b
Compare
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 973b5e5cb8
ℹ️ 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".
| and inspect its data model with `--print cfg`. Proof premises must cite | ||
| versioned Rust Reference or standard-library documentation. When changing | ||
| the Kani pin, manually recheck every such premise against the new compiler | ||
| snapshot; mechanically changing citation versions does not establish that |
There was a problem hiding this comment.
The recorded Rust 1.93 compatibility proposition is still not auditable because prove_dst_layout_extend cites the moving, unversioned Rust Reference URLs at zerocopy/src/layout.rs:2078 and 2093, contrary to this requirement. Fresh evidence relative to the resolved thread is that those exact unversioned citations remain in 973b5e5c; pin them to the applicable Rust 1.93 documentation before claiming that the manual audit checked those contracts against the bundled compiler snapshot.
AGENTS.md reference: zerocopy/AGENTS.md:L37-L38
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
|
@codex review Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
|
You have reached your Codex usage limits for security reviews. Please try again later. |
|
Codex Review: Didn't find any major issues. Delightful! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
|
@codex review Please review exact head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
|
You have reached your Codex usage limits for security reviews. Please try again later. |
|
Codex Review: Didn't find any major issues. Nice work! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
1cc864b to
71b2944
Compare
|
You have reached your Codex usage limits for security reviews. Please try again later. |
|
Codex Review: Didn't find any major issues. Delightful! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
|
@googlebot rescan CLA rescan requested for exact head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
Remove verification flags that Kani 0.65 made implicit and then deleted. Teach cargo-zerocopy not to emit empty outer RUSTFLAGS tokens so Kani 0.67 can run through cargo.sh, and synchronize the executable pin with its documented toolchain audit. *Authored by an AI agent acting on Josh Liebow-Feeser's behalf.* gherrit-pr-id: Gfdfm7an47cyz2scdlmc6lpej7h2q5qlx
71b2944 to
d773c6c
Compare
|
You have reached your Codex usage limits for security reviews. Please try again later. |
|
Codex Review: Something went wrong. Try again later by commenting “@codex review”. ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
2 participants
Remove verification flags that Kani 0.65 made implicit and then deleted. Teach cargo-zerocopy not to emit empty outer RUSTFLAGS tokens so Kani 0.67 can run through cargo.sh, and synchronize the executable pin with its documented toolchain audit.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
Latest Update: v52 — Compare vs v51
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Gfdfm7an47cyz2scdlmc6lpej7h2q5qlx && git checkout -b pr-Gfdfm7an47cyz2scdlmc6lpej7h2q5qlx FETCH_HEADCheckout
git fetch origin refs/heads/Gfdfm7an47cyz2scdlmc6lpej7h2q5qlx && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gfdfm7an47cyz2scdlmc6lpej7h2q5qlx && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.