[kani] Split byteorder proofs by monomorphization - #3650
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 @@
## G3hsfirdl7ux7wqc5tmzkwycqmjxflxa2 #3650 +/- ##
==================================================================
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:
|
36c9262 to
c81636b
Compare
316d409 to
5e971ad
Compare
c81636b to
0cb495c
Compare
5e971ad to
ae91fc4
Compare
0cb495c to
20446e2
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: 20446e2e37
ℹ️ 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".
| // The native/non-native pair exercises both `ByteOrder::ORDER` branches | ||
| // on Kani's target. It does not directly instantiate the big-, little-, | ||
| // or network-endian marker types, prove constant evaluation or |
There was a problem hiding this comment.
On Kani's target, NativeEndian aliases one of BigEndian/LittleEndian and NonNativeEndian aliases the other, so these harnesses actually monomorphize every wrapper with both concrete marker types; NetworkEndian is likewise just an alias for BigEndian and has no distinct implementation to exclude. Describing all three marker types as uninstantiated materially understates the proof domain, so clarify that only the alias names are not explicitly spelled while their concrete behavior is covered.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L71
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The scope now explains that NativeEndian, NonNativeEndian, and NetworkEndian are aliases on this target: their concrete big- or little-endian implementations are covered even though the alias names are not separately instantiated.
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. |
20446e2 to
c73ced0
Compare
ae91fc4 to
aba94a1
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: c73ced01c0
ℹ️ 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".
| // covered rather than a distinct implementation. These proofs do not | ||
| // separately spell every alias name, prove constant evaluation or | ||
| // arithmetic/operator implementations, or establish behavior on other | ||
| // targets, pointer widths, or outside Kani's floating-point model. |
There was a problem hiding this comment.
The scope paragraph lists the target and several non-goals, but it does not independently state the concrete size/allocation/unwind bounds, the absence of assumptions and excluded boundary cases, or the remaining Kani soundness limitations. Without those dimensions, readers can overgeneralize these harnesses beyond their modeled state space; explicitly record the zero allocation/loop bounds, unwind behavior, assumptions/boundaries, and applicable Kani soundness boundary for this proof family.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L71
Useful? React with 👍 / 👎.
| // wrappers, `MAX_VALUE`. The oracle is the corresponding primitive's | ||
| // inherent `to_ne_bytes` operation plus safe byte reversal. |
There was a problem hiding this comment.
When this proof is audited or the pinned compiler is rolled, merely naming to_ne_bytes plus byte reversal does not establish why that composition is an independent oracle for the expected big- and little-endian representation. Add versioned standard-library or language references for those semantics, explain that the target uses distinct to_be_bytes/to_le_bytes paths (including the separate float helpers), and state the oracle's limitations so the assertions are not justified only by an undocumented manual invert policy.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L71
Useful? React with 👍 / 👎.
| #[kani::proof] | ||
| fn $proof() { | ||
| $prove::<$ty>($invert); | ||
| } |
There was a problem hiding this comment.
Each generated harness still invokes one aggregate helper that proves new, get, set, the inherent byte methods, and both array conversion contracts together. If one entry point introduces an unsupported operation, timeout, or failed assertion, Kani cannot produce an independent result for the otherwise unrelated contracts, despite the repository guidance to keep distinct harnesses for different entry points; generate separate constructor, accessor/mutator, and conversion harnesses while sharing the symbolic inputs and oracle helpers.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L71
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The 24 concrete endian monomorphizations now each produce six independently selectable Kani results—constants, constructors, accessors, native conversions, byte conversions, and mutation—for 144 harnesses total. Shared helpers retain the oracle mechanics without coupling failures across those six contract groups.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
d76a656 to
9291e56
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. 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". |
171b12a to
eae4632
Compare
9291e56 to
413256b
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. Breezy! 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
413256b to
0bc43a2
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. Keep them coming! 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". |
0bc43a2 to
a2b512a
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". |
*Authored by an AI agent acting on Josh Liebow-Feeser's behalf.* gherrit-pr-id: G7impma2ko2k767ryccrfbsdxo4a2m3s2
25a6c2f to
2d20df4
Compare
a2b512a to
0160cfa
Compare
|
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". |
|
@googlebot rescan CLA rescan requested for exact head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
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/G7impma2ko2k767ryccrfbsdxo4a2m3s2 && git checkout -b pr-G7impma2ko2k767ryccrfbsdxo4a2m3s2 FETCH_HEADCheckout
git fetch origin refs/heads/G7impma2ko2k767ryccrfbsdxo4a2m3s2 && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/G7impma2ko2k767ryccrfbsdxo4a2m3s2 && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.