[kani] Strengthen SplitByteSlice proofs - #3649
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 @@
## G4pavaeiw7kliymw4ujvmg43vcwah5v5p #3649 +/- ##
==================================================================
Coverage 91.89% 91.89%
==================================================================
Files 20 20
Lines 6118 6118
==================================================================
Hits 5622 5622
Misses 496 496 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
![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: 3b10359346
ℹ️ 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: The assertion above establishes the method's sole caller | ||
| // precondition using the address-stable dereference observed above. |
There was a problem hiding this comment.
The new safety comment only refers to the local assertion and dereference stability, but the repository's mandatory unsafe-code review requires every unsafe block's justification to quote and cite a versioned Rust Reference or standard-library guarantee. Expand this comment with the required authoritative citation and quoted guarantees so the block can pass the project's safety audit.
AGENTS.md reference: zerocopy/AGENTS.md:L19-L23
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The unchecked helper now cites and quotes the Rust 1.93.0 slice::split_at_unchecked bound, and the proof establishes that bound from a length-stable safe dereference immediately before the call. Expected partitions and mutations come from safe slice operations.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
f22e083 to
503d7a8
Compare
316d409 to
5e971ad
Compare
9719a71 to
e6b583c
Compare
5e971ad to
ae91fc4
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: ae91fc4d1a
ℹ️ 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 bytes = kani::any::<[u8; BUFFER_LEN]>(); | ||
| let original = bytes; | ||
| let len = any_len(); | ||
| let _ = check_split_at(&bytes[..len], kani::any(), &original[..len]); |
There was a problem hiding this comment.
When the input is an interior view such as &bytes[1..3], none of these proofs exercises it: every slice harness uses &bytes[..len], and the Ref/RefMut harnesses likewise map only [..len]. Consequently, the documented domain does not cover every subslice view, and the mutable frame checks never test bytes preceding the view, so an implementation that miscomputes addresses or writes before a non-prefix view could still pass. Make both the view start and end symbolic and derive the independent oracle from the corresponding range of original.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. A shared View { start, end } generator now covers every contiguous view of the four-byte backing array, including every empty prefix/interior/suffix view. All slice, Ref, and RefMut harnesses use it, and mutable expected results plus the whole-buffer frame come from safe slice operations.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
ae91fc4 to
aba94a1
Compare
e6b583c to
60f0d48
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: aba94a1f58
ℹ️ 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_checked` supplies result classification | ||
| // and expected partitions; safe `slice::split_at_mut` supplies expected | ||
| // mutations. |
There was a problem hiding this comment.
The oracle inventory omits operations that supply expected behavior: check_split_at_unchecked derives pointer shape with slice::split_at, assert_split derives expected contents with another split_at, and the mutation checks depend on get_mut. The repository's proof protocol requires every oracle to state its versioned normative basis, independence from the target, and limitations, so add those operations and citations rather than documenting only split_at_checked and split_at_mut.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L71
Useful? React with 👍 / 👎.
| // Domain: Every `[u8; 4]`, every contiguous view (including empty prefix, | ||
| // interior, and suffix views), and every `usize` midpoint for the safe | ||
| // operation or every valid midpoint for the unchecked operation, for | ||
| // `&[u8]`, `&mut [u8]`, `Ref<[u8]>`, and `RefMut<[u8]>`. |
There was a problem hiding this comment.
The documented domain identifies the four-byte input but never records that each harness uses one fixed stack-backed allocation, has no explicit proof loops, and applies #[kani::unwind(5)]. These are independent proof-scope dimensions required by the repository's validation protocol; without them, readers cannot tell whether the bound is a deliberate part of the assurance or an incidental verifier setting. Add those concrete bounds to this domain statement.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L71
Useful? React with 👍 / 👎.
171b12a to
eae4632
Compare
274a10a to
6037ae9
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. |
|
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". |
eae4632 to
b2efd47
Compare
6037ae9 to
2f73227
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". |
2f73227 to
9aebc12
Compare
b2efd47 to
25a6c2f
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. 🎉 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". |
9aebc12 to
6350696
Compare
25a6c2f to
2d20df4
Compare
|
You have reached your Codex usage limits for security reviews. Please try again later. |
|
Codex Review: Didn't find any major issues. What shall we delve into next? 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". |
*Authored by an AI agent acting on Josh Liebow-Feeser's behalf.* gherrit-pr-id: G3hsfirdl7ux7wqc5tmzkwycqmjxflxa2
6350696 to
867d9c2
Compare
2d20df4 to
225b02c
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
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/G3hsfirdl7ux7wqc5tmzkwycqmjxflxa2 && git checkout -b pr-G3hsfirdl7ux7wqc5tmzkwycqmjxflxa2 FETCH_HEADCheckout
git fetch origin refs/heads/G3hsfirdl7ux7wqc5tmzkwycqmjxflxa2 && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/G3hsfirdl7ux7wqc5tmzkwycqmjxflxa2 && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.