[kani] Prove representative derived validators - #3655
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. |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## Gti2px6v6qyolz34c5rkfkgsrcirhtxpe #3655 +/- ##
==================================================================
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:
|
7dd9138 to
89a8bf3
Compare
17ccb01 to
e985ff7
Compare
dda6a78 to
edac273
Compare
e985ff7 to
5a84428
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. 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". |
|
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
5a84428 to
658451e
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. |
94bc86b to
c7ae9cf
Compare
![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: 94bc86bb95
ℹ️ 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 candidate representation is valid. Each theorem covers one fixed, | ||
| //! sized derive input and every byte pattern for that input on Kani's target. | ||
| //! This is not a generator theorem: it does not cover other derive inputs, | ||
| //! configurations, targets, or properties absent from Kani's memory model. The | ||
| //! sized inputs also deliberately avoid the nested-DST layout issue tracked in | ||
| //! #3630. |
There was a problem hiding this comment.
The family scope does not state the concrete byte sizes, that there are no assumptions or dynamic allocations, whether loops/unwind bounds are absent or applicable, or the specific Kani blind spots around aliasing, provenance, invalid values, and uninitialized memory. Saying only “fixed, sized” and “properties absent from Kani's memory model” leaves several required scope dimensions implicit, so readers cannot audit what “every byte pattern” establishes; add an explicit scope ledger covering those dimensions and the public invalid-input-path exclusion.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
Useful? React with 👍 / 👎.
| fn char_from_bytes(bytes: &[u8], offset: usize) -> Option<char> { | ||
| let representation: [u8; 4] = bytes[offset..offset + 4].try_into().unwrap(); | ||
| char::from_u32(u32::from_ne_bytes(representation)) |
There was a problem hiding this comment.
Both struct proofs treat four candidate bytes as the native-endian object representation of char, but char::from_u32 only supplies checked scalar construction; it does not by itself establish that u32::from_ne_bytes(representation) describes the candidate char bytes. The existing primitive proof cites the versioned Reference guarantee that char is represented as a 32-bit unsigned word, but this new oracle neither cites nor unambiguously refers to that premise. Add the same versioned representation basis and explain the native-endian mapping so the expected result is independent of the validator under proof.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
Useful? React with 👍 / 👎.
| // Domain: all initialized representations of this fixed `repr(C)` type. | ||
| // Establishes: the generated validator accepts exactly when both fields | ||
| // do. On those independently valid inputs, the public value-reading API | ||
| // succeeds and returns the oracle's field values. | ||
| // Oracle: actual field offsets plus safe checked `char` construction and the | ||
| // shared `bool` language-validity oracle. This is not a derive-generator or | ||
| // generic struct-layout theorem. |
There was a problem hiding this comment.
For BoolAndChar, the symbolic representation includes arbitrary padding between the one-byte bool and four-byte char, while the safely constructed witness can contain different padding. Field offsets and safe field constructors therefore do not alone establish validity of the exact candidate bytes, despite the shared macro explicitly requiring each caller to explain that step. Cite the independent aggregate-validity/padding rule and state that padding bytes impose no additional validity condition before using expected.is_some() as the exact acceptance oracle.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The aggregate oracle now cites Rust 1.93’s field-validity rule and MaybeUninit padding contract, and explains that initialized padding bytes impose no additional validity condition. Compiler offset_of! values select the exact field bytes, so safely constructed matching fields witness validity even when their padding differs from the candidate.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
|
@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. 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". |
|
@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 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". |
|
@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. 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". |
|
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". |
|
@googlebot rescan CLA rescan requested for 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. 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". |
|
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". |
*Authored by an AI agent acting on Josh Liebow-Feeser's behalf.* gherrit-pr-id: Gsgjodecq7t42k3eelvsqemhatlt2or2u
|
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/Gsgjodecq7t42k3eelvsqemhatlt2or2u && git checkout -b pr-Gsgjodecq7t42k3eelvsqemhatlt2or2u FETCH_HEADCheckout
git fetch origin refs/heads/Gsgjodecq7t42k3eelvsqemhatlt2or2u && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gsgjodecq7t42k3eelvsqemhatlt2or2u && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.