[kani] Prove IntoBytes views and write frames - #3656
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. |
93cdb98 to
efa1180
Compare
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## Gsgjodecq7t42k3eelvsqemhatlt2or2u #3656 +/- ##
==================================================================
Coverage 91.85% 91.85%
==================================================================
Files 20 20
Lines 6093 6093
==================================================================
Hits 5597 5597
Misses 496 496 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
7dd9138 to
89a8bf3
Compare
efa1180 to
d41363c
Compare
89a8bf3 to
dda6a78
Compare
d41363c to
9742a70
Compare
dda6a78 to
edac273
Compare
9742a70 to
3f9d1cf
Compare
|
@codex review Please review current head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
|
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". |
|
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. |
edac273 to
94bc86b
Compare
3f9d1cf to
243a7c5
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. |
|
You have reached your Codex usage limits for security reviews. Please try again later. |
|
@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. Swish! 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 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". |
|
@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. Already looking forward to the next diff. 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 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. Swish! 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. You're on a roll. 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". |
|
You have reached your Codex usage limits for security reviews. Please try again later. |
![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: aa2e710216
ℹ️ 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".
| ) -> [u8; MAX_DST_LEN] { | ||
| let mut expected = copy_snapshot(destination); | ||
| let selected = &mut expected[range]; | ||
| selected.copy_from_slice(source); |
There was a problem hiding this comment.
When this helper constructs the expected frame, source: &[u8; VALUE_SIZE] is implicitly coerced to &[u8] for copy_from_slice; the cited copy contract only specifies what happens after that slice has been formed, and the oracle inventory never establishes that the coercion preserves all four array elements in order and with the expected length. The same unstated premise is used by the suffix helper, so add the pinned Rust array-to-slice unsizing/coercion basis and its limitations to make the expected-byte oracle independently auditable.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L71
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
Addressed on exact head 623c6096a308f9f0bd792502e7772475324e5e56. Every fixed-array-to-slice step used by these expected-value and frame oracles is now explicit through array::as_slice(), including the source copies, split observations, and source-length observations. The proof text cites the exact Rust 1.93 whole-array slice contract and states its limits: it establishes the ordered full-array view, not distinct storage, provenance, aliasing, or allocation identity. The exact full Kani suite verified all 332 harnesses and all covers, and the repository pre-push hook passed.
|
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". |
*Authored by an AI agent acting on Josh Liebow-Feeser's behalf.* gherrit-pr-id: G3ehtgm3rda6i5wi6h6gwkvlmzeh4sn46
|
You have reached your Codex usage limits for security reviews. Please try again later. |
|
Codex Review: Didn't find any major issues. Bravo. 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". |
2 participants
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
Latest Update: v51 — Compare vs v50
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/G3ehtgm3rda6i5wi6h6gwkvlmzeh4sn46 && git checkout -b pr-G3ehtgm3rda6i5wi6h6gwkvlmzeh4sn46 FETCH_HEADCheckout
git fetch origin refs/heads/G3ehtgm3rda6i5wi6h6gwkvlmzeh4sn46 && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/G3ehtgm3rda6i5wi6h6gwkvlmzeh4sn46 && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.