Repository navigation
Conversation
|
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. |
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. |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## G44fd7b86a51e9f6cabdcddc13cebc2f0 #3646 +/- ##
====================================================================
Coverage ? 91.89%
====================================================================
Files ? 20
Lines ? 6122
Branches ? 0
====================================================================
Hits ? 5626
Misses ? 496
Partials ? 0 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
|
|
||
| #[kani::proof] | ||
| #[kani::unwind(9)] | ||
| fn prove_slice_split_at_unchecked() { |
There was a problem hiding this comment.
See if you can deduplicate some between these two tests? Lots of repetition.
There was a problem hiding this comment.
Addressed in the current revision. The shared and mutable harnesses now reuse any_slice_split_case, ExpectedSplit, expected_split, and assert_slice_split; only the mutation-specific setup and assertions remain local. The module and PR descriptions also spell out the exact common proof domain and exclusions.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
![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: 1cf4212f5e
ℹ️ 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".
| // SAFETY: `split <= source.len()`, and slices have no trailing | ||
| // padding, so the left and right portions do not overlap. | ||
| let (left, right) = unsafe { SplitAt::split_at_unchecked(source, split).via_unchecked() }; |
There was a problem hiding this comment.
BLOCKING: This new safety comment does not satisfy the repository's mandatory unsafe-code standard because it neither cites versioned Rust Reference/standard-library documentation nor quotes the guarantees used to justify the two unsafe calls; the analogous block at lines 1025–1028 has the same omission. Expand each rationale with citations and supporting quotations, for example starting with // [1] Per https://doc.rust-lang.org/1.91.0/std/primitive.slice.html#method.split_at_unchecked: and quoting the relevant contract.
AGENTS.md reference: zerocopy/AGENTS.md:L21-L23
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. Each unsafe operation now has a separate safety rationale. The unchecked split cites and quotes the Rust 1.93.0 slice contract, while via_unchecked cites and quotes the versioned array/slice layout guarantees that establish non-overlap.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| // These bounded harnesses establish byte-range and data-flow properties | ||
| // for the slice instantiation of `SplitAt` over a fixed live allocation. |
There was a problem hiding this comment.
BLOCKING: The module comment describes these harnesses as establishing properties for the slice instantiation of SplitAt, but both harnesses instantiate only [u32], so they do not cover ZSTs or elements with different size and alignment even though the formal-verification rules require target-specific proof domains to be documented. Either narrow this text explicitly to the [u32] instantiation with CAPACITY = 8 or add representative harnesses before presenting the result as slice-wide.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L72
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The proof comment now states the domain as every initialized [u32; 8], logical length 0..=8, and valid split point for shared and mutable slices. It explicitly excludes other element types (including ZSTs), custom DSTs, other layouts, and a generic SplitAt theorem.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| let source_end = source[source_len..].as_ptr(); | ||
| // SAFETY: `split <= source.len()`, and slices have no trailing | ||
| // padding, so the left and right portions do not overlap. | ||
| let (left, right) = unsafe { SplitAt::split_at_unchecked(source, split).via_unchecked() }; |
There was a problem hiding this comment.
BLOCKING: This block performs both the unsafe SplitAt::split_at_unchecked call and the unsafe via_unchecked call, violating the crate-level deny(clippy::multiple_unsafe_ops_per_block) policy; the mutable block at line 1028 has the same problem. Split each expression into two statements such as let split = unsafe { SplitAt::split_at_unchecked(source, split) }; let (left, right) = unsafe { split.via_unchecked() };, with a separate safety rationale for each operation.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L72
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. SplitAt::split_at_unchecked and Split::via_unchecked are now separate statements and separate unsafe blocks, each with its own contract-specific safety comment and citation; the mutable harness follows the same structure.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
1cf4212 to
b721246
Compare
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. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b721246249
ℹ️ 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".
| // Excludes: Other element types (including ZSTs), larger slices, custom | ||
| // slice DSTs and their padding (see #3630), other targets/layouts, and the | ||
| // aliasing, provenance, and reference-validity obligations that Kani does |
There was a problem hiding this comment.
BLOCKING: In the inspected .github/workflows/ci.yml Kani job, Kani 0.67.0 runs with the stable-only feature set and --randomize-layout, which verifies only one randomized layout per invocation; saying merely that “other targets/layouts” are excluded does not identify the target, feature configuration, or sampled-layout scope that was actually verified. Fresh evidence beyond the prior bounded-[u32] comment is this new but still unnamed target/layout exclusion. Spell out the CI target/toolchain/features and the one-layout-per-run limitation in this proof-domain block.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L72
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The proof-domain block and PR scope now identify the CI-pinned Kani release and bundled x86_64-unknown-linux-gnu compiler, the stable-compatible feature bundle, -Zfunction-contracts, and the fact that each invocation checks one layout selected by --randomize-layout.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| // SAFETY: The array and slice layout guarantees [1] place each element | ||
| // immediately after the last, so the two portions have no overlapping | ||
| // padding. This satisfies `Split::via_unchecked`'s conditional | ||
| // no-overlap precondition. |
There was a problem hiding this comment.
BLOCKING: For both via_unchecked calls, the fresh rationale quotes only element offsets and the fact that slices share array-section layout. Those premises locate the first right-hand element but do not explicitly establish the byte extent or absence of trailing padding in the left slice, which is precisely the unsafe precondition being discharged. Quote the Reference guarantee that [T; N] has size size_of::<T>() * N, connect it to the slice-layout guarantee, and make the same correction in the mutable block.
AGENTS.md reference: zerocopy/AGENTS.md:L21-L23
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. Both shared and mutable via_unchecked rationales now quote the array size formula, element-offset rule, and slice-section layout guarantee from the Rust 1.93.0 Reference, and connect them explicitly to the absence of padding overlap.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
2c33905 to
ca0e3c3
Compare
b721246 to
8c2ad1a
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: 8c2ad1a936
ℹ️ 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".
| // Oracle: Safe `slice::split_at` supplies the expected partitions and | ||
| // addresses; safe `slice::split_at_mut` supplies the expected mutations. |
There was a problem hiding this comment.
BLOCKING: Although these are genuinely independent standard-library calls, merely naming them does not state their normative postconditions, explain their independence from the zerocopy implementation, or delimit their evidentiary limitations. The versioned citations below cover the unsafe variants' preconditions and layout, but none establishes that safe split_at returns the [..mid] and [mid..] partitions or that split_at_mut plus fill supplies the expected write/frame result. Cite those safe API contracts and explicitly state the independence and limitations of each oracle.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L72
Useful? React with 👍 / 👎.
| // Domain: Every initialized `[u32; 8]`, source length from 0 through 8, | ||
| // and valid split point from 0 through the source length, for shared and | ||
| // mutable slices. |
There was a problem hiding this comment.
BLOCKING: The current domain identifies [u32; 8] and the symbolic index ranges, but it still leaves required scope dimensions implicit: the local backing-array allocations, the at-most-eight-element mutation/oracle/assertion loops, and the 33 unwind bound used by both harnesses. Without stating these bounds and why 33 covers every exercised loop, the documented proof domain does not fully describe the modeled state space; add them to this block explicitly.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L72
Useful? React with 👍 / 👎.
ca0e3c3 to
49c1349
Compare
8c2ad1a to
99ced13
Compare
753348d to
973b5e5
Compare
4636641 to
4e93d0f
Compare
|
@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. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 4e93d0f614
ℹ️ 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 values = kani::any(); | ||
| let source_len: usize = kani::any(); |
There was a problem hiding this comment.
BLOCKING: The claim that these harnesses cover every initialized array, length, split point, and mutation value depends on kani::any() ranging over every valid value of each requested type, but the proof account neither cites Kani 0.67's any contract nor labels its translation as a TOOL/TCB premise. The documented assume semantics only explain how generated values are filtered, not which values are generated initially, so add the version-pinned kani::any basis and its valid-value/model limitations for these calls.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L72
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed. The proof account now cites Kani 0.67's any/any_raw path, its AnyRawHook -> Nondet registration, and CBMC 6.8.0's nondeterministic-input model. It explicitly records the Kani/translation/model correspondence as TOOL/TCB, limits the claim to valid values of the requested types, and keeps the cover results as non-vacuity evidence rather than using them to prove exhaustiveness.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
a0a14a5 to
e7ef4f3
Compare
4e93d0f to
d2506e1
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. 👍 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". |
d2506e1 to
145f683
Compare
|
@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. Chef's kiss. 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". |
e7ef4f3 to
757a961
Compare
145f683 to
8fc739c
Compare
|
You have reached your Codex usage limits for security reviews. Please try again later. |
|
Codex Review: Didn't find any major issues. Chef's kiss. 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". |
Verify immutable and mutable SplitAt core behavior over a fixed live allocation with symbolic source and split lengths. Check exact extents, boundary pointers, contents, mutations, untouched suffixes, and reachable empty/interior/end partitions. *Authored by an AI agent acting on Josh Liebow-Feeser's behalf.* gherrit-pr-id: Gk2g4l26m6qo5bi7nwt5p7s4lbskrcsk4
8fc739c to
59a2396
Compare
757a961 to
6843138
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". |
Verify immutable and mutable SplitAt core behavior over a fixed live allocation with symbolic source and split lengths. Check exact extents, boundary pointers, contents, mutations, untouched suffixes, and reachable empty/interior/end partitions.
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/Gk2g4l26m6qo5bi7nwt5p7s4lbskrcsk4 && git checkout -b pr-Gk2g4l26m6qo5bi7nwt5p7s4lbskrcsk4 FETCH_HEADCheckout
git fetch origin refs/heads/Gk2g4l26m6qo5bi7nwt5p7s4lbskrcsk4 && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gk2g4l26m6qo5bi7nwt5p7s4lbskrcsk4 && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.