[kani] Prove utility memory operations - #3648
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 @@
## Gcmpgic3rdonowgrcxzylfnswfrlxt6lm #3648 +/- ##
====================================================================
Coverage ? 91.85%
====================================================================
Files ? 20
Lines ? 6093
Branches ? 0
====================================================================
Hits ? 5597
Misses ? 496
Partials ? 0 ☔ 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: f22e083f02
ℹ️ 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 assumptions above establish that the source subslice is | ||
| // no longer than the destination subslice. | ||
| unsafe { copy_unchecked(&src[..src_len], &mut dst[..dst_len]) }; |
There was a problem hiding this comment.
The safety comment here—and each of the other newly added unsafe call sites in this proof module—only restates the callee's preconditions. The repository's mandatory reviewing protocol requires every unsafe block's justification to cite and quote a versioned Rust Reference or standard-library guarantee, so these comments must be expanded with the relevant documentation citations and excerpts before merging.
AGENTS.md reference: zerocopy/AGENTS.md:L21-L23
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The unsafe calls now cite and quote the exact versioned guarantees they consume: copy_nonoverlapping validity/alignment/non-overlap, numeric bit validity for transmutation, and the allocator contracts for the modeled allocation paths. Expected values are derived from safe copying, native-byte conversions, Wrapping, and safe dereferencing.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
f22e083 to
503d7a8
Compare
e2d0662 to
2753765
Compare
503d7a8 to
9719a71
Compare
2753765 to
49e0f09
Compare
9719a71 to
e6b583c
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: e6b583c20b
ℹ️ 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".
| // Note that even if the effectively copied size | ||
| // (`count * size_of::<T>()`) is 0, the pointers must be non-null | ||
| // and properly aligned. | ||
| unsafe { copy_unchecked(&src[..src_len], &mut dst[..dst_len]) }; |
There was a problem hiding this comment.
The current revision's [1] excerpt only lists copy_nonoverlapping's preconditions; it does not support the safety comment's claims that the subslices are live and aligned or that regions belonging to distinct local arrays cannot overlap. This is fresh evidence relative to the prior thread because the newly added citation still leaves those essential claims based on intuition rather than quoted, versioned Reference or standard-library guarantees; add citations establishing reference validity/alignment and exclusivity/non-overlap. zerocopy/agent_docs/unsafe_code.mdL56-L65
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The safety rationale now cites the Rust 1.93.0 reference guarantees for reference alignment, non-nullness, validity, slice-buffer pointers, and exclusive-reference access, and connects those guarantees to every copy_nonoverlapping precondition, including non-overlap.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
e6b583c to
60f0d48
Compare
49e0f09 to
4c05617
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: 60f0d48bc9
ℹ️ 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 `u32::to_ne_bytes`, `u32::from_ne_bytes`, and `Wrapping` | ||
| // construction. |
There was a problem hiding this comment.
For the two reference-transmute harnesses, Wrapping construction supplies an expected value but cannot establish the separately claimed address preservation. The assertions merely designate the original pointer as the expected address without citing a Rust or standard-library rule that requires this result, explaining why that rule is independent of transmute_ref/transmute_mut, or labeling its limitations. Cite the normative pointer/reference rule used to derive the expected address (or stop claiming this property); otherwise these assertions do not satisfy the repository's oracle requirements. zerocopy/agent_docs/validation.mdL74-L83
Useful? React with 👍 / 👎.
| // 12. | ||
| // Establishes: The copied prefix and every destination frame byte exactly | ||
| // match a safe copy. | ||
| // Oracle: `slice::copy_from_slice` applied to a separate destination copy. |
There was a problem hiding this comment.
When this harness is used as evidence for copy_unchecked's copy and frame behavior, the expected buffer is derived entirely through slice::copy_from_slice, but the scope comment only names that API and never cites its documented guarantee that the receiver elements are replaced by the source elements. Add a versioned standard-library citation for that semantic contract and explicitly state why using it on the separate destination is independent of copy_unchecked; otherwise the asserted expected result lacks the normative basis required for every proof oracle. zerocopy/agent_docs/validation.mdL74-L83
Useful? React with 👍 / 👎.
|
You have reached your Codex usage limits for security reviews. Please try again later. |
dc3f69d to
69aa306
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. More of your lovely PRs please. 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". |
69aa306 to
7485956
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. |
2f73227 to
9aebc12
Compare
7485956 to
5e538bb
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. 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". |
5e538bb to
72bf299
Compare
9aebc12 to
6350696
Compare
|
You have reached your Codex usage limits for security reviews. Please try again later. |
|
Codex Review: Didn't find any major issues. Keep it up! 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". |
Replace the private raw copy helper with safe `copy_prefix`, prove its bounded frame behavior, and remove three caller unsafe blocks. Add concrete representation and mutation proofs for transmute helpers, plus sized, ZST, and plain-slice `new_box` smoke proofs. Document the remaining aliasing, provenance, allocator, and nested-DST limits. *Authored by an AI agent acting on Josh Liebow-Feeser's behalf.* gherrit-pr-id: G4pavaeiw7kliymw4ujvmg43vcwah5v5p
6350696 to
867d9c2
Compare
72bf299 to
1961311
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
Replace the private raw copy helper with safe
copy_prefix, prove its boundedframe behavior, and remove three caller unsafe blocks. Add concrete
representation and mutation proofs for transmute helpers, plus sized, ZST, and
plain-slice
new_boxsmoke proofs. Document the remaining aliasing, provenance,allocator, and nested-DST limits.
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/G4pavaeiw7kliymw4ujvmg43vcwah5v5p && git checkout -b pr-G4pavaeiw7kliymw4ujvmg43vcwah5v5p FETCH_HEADCheckout
git fetch origin refs/heads/G4pavaeiw7kliymw4ujvmg43vcwah5v5p && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/G4pavaeiw7kliymw4ujvmg43vcwah5v5p && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.