[kani] Prove primitive byte validation - #3647
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 @@
## Gk2g4l26m6qo5bi7nwt5p7s4lbskrcsk4 #3647 +/- ##
==================================================================
Coverage 91.89% 91.89%
==================================================================
Files 20 20
Lines 6122 6122
==================================================================
Hits 5626 5626
Misses 496 496 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
| // types, they exhaust every byte pattern on Kani's target. They do not | ||
| // establish that Kani detects invalid typed values after construction. | ||
|
|
||
| // Evaluate the validator directly on initialized source bytes. This check |
There was a problem hiding this comment.
| // Evaluate the validator directly on initialized source bytes. This check | |
| // Evaluates the validator directly on initialized source bytes. This check |
There was a problem hiding this comment.
Addressed while factoring this setup. The direct-validator plumbing moved to the shared validator_accepts_sized! helper, whose comment now explains that it evaluates the validator on initialized source bytes before the end-to-end API may materialize T.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| } | ||
|
|
||
| #[cfg(kani)] | ||
| mod proofs { |
There was a problem hiding this comment.
Can you think of a way to more exhaustively generate every possible bit pattern and then categorize each bit pattern as bit valid or not?
For example, perhaps, for a given T: Sized + IntoBytes, we could do:
- Generate
kani::any::<T>() - Confirm that the bytes are accepted as a valid
TbyTryFromBytes - Somehow generate every
[u8; size_of::<T>()]that's not a validT - Confirm that these bytes are rejected by
TryFromBytes
Ideally we could do this in a way that doesn't require manually encoding validity and instead relies on Rust itself to give us an oracle for validity.
There was a problem hiding this comment.
Implemented the byte-first form of this idea in the current revision. Each selected fixed-size type starts from kani::any::<[u8; N]>(), so Kani ranges over every byte pattern without first creating a possibly-invalid T. The proofs compare both the raw validator and public read API against safe checked oracles (char::from_u32, NonZeroU16::new, and native-byte APIs); the only residual manual rule is bool, centralized once and tied to versioned language documentation.
There is no fully generic safe negative oracle: generating kani::any::<T>() witnesses only valid values, while materializing arbitrary bytes as T before checking them is already undefined behavior when the bytes are invalid. That limitation is now documented in proof_support.rs and the PR scope.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
1cf4212 to
b721246
Compare
2753765 to
49e0f09
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. |
![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: 49e0f0915d
ℹ️ 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".
| // Domain: Every initialized source byte sequence for `bool`, `char`, | ||
| // `NonZeroU16`, `Option<NonZeroU16>`, and `[bool; 4]` on Kani's target. |
There was a problem hiding this comment.
For calls where try_read_from_bytes receives a slice whose length differs from size_of::<T>(), these harnesses exercise neither acceptance nor the documented size-error behavior: each bytes value is a fixed-size array and validator_accepts_sized! explicitly uses CastSizedExact. Thus “Every initialized source byte sequence” overstates the public-API domain. Either state that only exactly sized byte representations are covered and exclude size mismatches, or add arbitrary-length harnesses with an independent expected size-error oracle.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The domain is now explicitly every exactly sized initialized representation for the listed types. Size-mismatched sources and size-error classification by the public API are explicitly excluded.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| // Excludes: Other types and array lengths, non-native byte order, and | ||
| // validity or provenance behavior not modeled by Kani. Starting from bytes | ||
| // ensures that no invalid destination value exists before validation. |
There was a problem hiding this comment.
When this theorem is interpreted beyond the exact CI compilation, the stated exclusions are incomplete: the Kani job in .github/workflows/ci.yml:719-743 enables only __internal_use_only_features_that_work_on_stable and uses --randomize-layout, which checks one randomized layout per run rather than every layout for the target. Nothing in these harnesses quantifies over feature configurations or layout seeds, yet the comment excludes only non-native byte order and model limitations. Explicitly restrict the result to the sampled layout and enabled feature set, or add the configurations needed to support a broader claim.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The family comment and PR scope now bound the result to the exact shared Kani CI configuration, including its bundled target/compiler, stable-compatible feature bundle, function-contract flag, and one randomized layout per invocation.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
b721246 to
8c2ad1a
Compare
49e0f09 to
4c05617
Compare
|
@codex review Please review current head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 4c056173b4
ℹ️ 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::proof] | ||
| #[kani::unwind(5)] | ||
| fn prove_bool_array_try_read_from_bytes() { |
There was a problem hiding this comment.
When this module comment is used as the theorem’s proof scope, it omits the concrete loop bound on the [bool; 4] harness: #[kani::unwind(5)] limits every loop reached from this harness, but neither the documented domain nor its exclusions mentions that limitation. The current revision documents exact source sizes and the shared CI configuration, but this is a distinct remaining bound; state the five-step unwind limit and which array iteration it is intended to cover so the claimed domain remains accurate if the implementation’s looping behavior changes.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The family scope now states that every harness has #[kani::unwind(5)], permitting the [bool; 4] validator and any other reached bytewise operation to examine four bytes or elements and terminate, with unwinding assertions enforcing that bound.
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. |
4c05617 to
fdb1983
Compare
8c2ad1a to
99ced13
Compare
4636641 to
4e93d0f
Compare
dc3f69d to
69aa306
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. |
4e93d0f to
d2506e1
Compare
69aa306 to
7485956
Compare
|
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. 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". |
7485956 to
5e538bb
Compare
d2506e1 to
145f683
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. Another round soon, 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". |
145f683 to
8fc739c
Compare
5e538bb to
72bf299
Compare
|
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". |
Drive bool, char, NonZeroU16, its niche-optimized Option, and bool arrays from every concrete-size byte sequence. Compare both internal validators and public reads against safe checked standard-library constructors where available and one centralized Reference-backed bool oracle; verify accepted values and valid/invalid reachability. *Authored by an AI agent acting on Josh Liebow-Feeser's behalf.* gherrit-pr-id: Gcmpgic3rdonowgrcxzylfnswfrlxt6lm
8fc739c to
59a2396
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
Drive bool, char, NonZeroU16, its niche-optimized Option, and bool arrays from every concrete-size byte sequence. Compare both internal validators and public reads against safe checked standard-library constructors where available and one centralized Reference-backed bool oracle; verify accepted values and valid/invalid reachability.
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/Gcmpgic3rdonowgrcxzylfnswfrlxt6lm && git checkout -b pr-Gcmpgic3rdonowgrcxzylfnswfrlxt6lm FETCH_HEADCheckout
git fetch origin refs/heads/Gcmpgic3rdonowgrcxzylfnswfrlxt6lm && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gcmpgic3rdonowgrcxzylfnswfrlxt6lm && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.