[kani] Prove Unalign update write-back - #3651
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 @@
## G7impma2ko2k767ryccrfbsdxo4a2m3s2 #3651 +/- ##
==================================================================
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:
|
36c9262 to
c81636b
Compare
0e35235 to
61ff28d
Compare
0cb495c to
20446e2
Compare
61ff28d to
2d90423
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. 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". |
|
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. |
2d90423 to
cc19271
Compare
20446e2 to
c73ced0
Compare
|
@codex review Please review current head 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: cc19271442
ℹ️ 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".
| // These normal-return harnesses are universal over the old and new byte | ||
| // values on Kani's target. One uses a one-byte, alignment-one value; the | ||
| // other uses a greater-than-one-aligned value with a destructor. Together, | ||
| // they exercise both branches of `Unalign::update`, including | ||
| // closure-result forwarding, mutation write-back, and one observable final |
There was a problem hiding this comment.
This scope describes the symbolic bytes and two type shapes, but it never independently records the concrete object/allocation bounds, that there are no loops or recursion requiring an unwind bound, that there are no assumptions, or that the only modeled callback/destructor is non-panicking and mutates one u8 field rather than replacing the whole T. These omissions make it easy to overread the harness as covering ownership and write-back cases it does not model; enumerate each required bound and excluded boundary case explicitly.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
Useful? React with 👍 / 👎.
| assert_eq!(returned, old); | ||
| // Destructuring is a language operation independent of `into_inner`, | ||
| // which exercises the same representation-sensitive path as `update`. | ||
| let Unalign(restored) = value; |
There was a problem hiding this comment.
Calling destructuring a “language operation” establishes independence from into_inner, but it does not provide the required normative basis or limitations for the oracle. The proof also relies on safe field assignment, closure-result forwarding, moving a field from a packed wrapper, and drop(restored) invoking the destructor exactly once; cite the versioned Rust Reference or standard-library contracts that supply those expectations and identify which assertions each oracle supports.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The proof now maps each assertion to exact Rust 1.93 contracts for tuple-struct construction and destructuring, default move bindings, closure/block evaluation, assignment, function return, move deinitialization, mem::drop, and destructor execution. It explains both update return paths and why moving the sole field and then restored yields exactly one observed Drop::drop call.
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: 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". |
3879072 to
ed4cbd6
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. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ed4cbd6697
ℹ️ 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 returned = value.update(|value| { | ||
| assert_eq!(value.0, old); | ||
| value.0 = new; | ||
| old |
There was a problem hiding this comment.
When these closures use the surrounding old and new bindings as expected inputs, assigned values, and return values, the proof depends on closure capture and captured-path evaluation preserving those bytes. References [4] and [5] establish parameter mapping and block ordering, but the proof account never cites or maps the Rust 1.93 capture/path contracts for either closure, so these expected-result oracles remain partly grounded in modeled compiler behavior; cite those contracts and map both captured bindings through both closures.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed. The account now cites Rust 1.93 closure capture inference, capture modes, captured-place expressions, and u8: Copy, then explicitly maps both old and new through both non-move closures into the assertion, assignment, and returned result.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
ed4cbd6 to
bdccd1c
Compare
0bc43a2 to
a2b512a
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. 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". |
bdccd1c to
269250c
Compare
a2b512a to
0160cfa
Compare
|
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: 269250c0e1
ℹ️ 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".
| kani::cover!(result != old); | ||
| kani::cover!(result == new); | ||
| kani::cover!(result != new); | ||
| kani::cover!(result != old && result != new); |
There was a problem hiding this comment.
When this cover is used to establish that the independent closure result can differ from both field values, references [27] and [32] cover byte inequality and Kani's cover mechanism, but none of [1]–[38] establishes the && operator's conjunction and short-circuit semantics; [30] covers only unary negation. Cite the Rust 1.93 lazy-Boolean-operator contract and map it to this distinct-from-both partition so the claimed non-vacuity result has a documented independent basis.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
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 20091159752fa7f84cc7ed4f93f8633965f26a9a. The oracle inventory now cites the Rust 1.93 lazy Boolean operator contract and maps a && b to conjunction with left-to-right short-circuit evaluation. That basis is applied specifically to the cover requiring the independent closure result to differ from both the old and new field values. The exact full Kani suite verified all 332 harnesses and all covers, and the repository pre-push hook passed.
|
@googlebot rescan CLA rescan requested for exact head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
269250c to
2009115
Compare
|
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: 2009115975
ℹ️ 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".
| assert_same_usize(mem::size_of::<Byte>(), 1); | ||
| assert_same_usize(mem::size_of::<Unalign<Byte>>(), 1); | ||
| assert_same_usize(mem::align_of::<Byte>(), 1); |
There was a problem hiding this comment.
When these fail-closed layout checks are used as expected-result oracles, every expected 1, 16, and 24—including the later alignment comparison and offset checks—is an unsuffixed integer literal whose value and usize type depend on contextual literal typing. Reference [33] is mapped only to the explicitly suffixed u8 counter literals, while [27] supplies only equality mechanics, so these size, alignment, branch-selection, and placement expectations still lack the required versioned normative basis. Suffix the layout constants with usize and map their literal semantics, or cite and map contextual typing for each affected assertion.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
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 3580b1d52e3fb5373f7a480e8e79efde29fbf8d6. The layout expectations and alignment threshold now use explicitly typed usize literals. The adjacent argument spells out the decimal/suffix conversion and representability of the expected values, with the specific Rust 1.93 literal rules linked as premise [33]. Language-derived layout facts remain separate from the pinned compiler/target layout assumptions.
*Authored by an AI agent acting on Josh Liebow-Feeser's behalf.* gherrit-pr-id: G56sp4dsuukjpe3trlzhqbkuvl6f53jkg
0160cfa to
91fb011
Compare
2009115 to
3580b1d
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/G56sp4dsuukjpe3trlzhqbkuvl6f53jkg && git checkout -b pr-G56sp4dsuukjpe3trlzhqbkuvl6f53jkg FETCH_HEADCheckout
git fetch origin refs/heads/G56sp4dsuukjpe3trlzhqbkuvl6f53jkg && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/G56sp4dsuukjpe3trlzhqbkuvl6f53jkg && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.