[kani] Prove bounded UTF-8 validation - #3654
Conversation
|
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. |
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 @@
## Gyiyzmayequ5ugyjdxzkhyjwnp6pggabj #3654 +/- ##
==================================================================
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:
|
bd1ccdb to
5bdc725
Compare
17ccb01 to
e985ff7
Compare
5bdc725 to
a802f42
Compare
e985ff7 to
5a84428
Compare
a802f42 to
170146b
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: 5a8442871d
ℹ️ 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".
| // Excludes: Empty and longer strings, properties outside Kani's model, and | ||
| // an independent proof of UTF-8 validity itself. |
There was a problem hiding this comment.
BLOCKING: For &[], the empty string is valid UTF-8 and exercises the zero-length slice/DST boundary, but every harness starts at N = 1 and this line explicitly excludes that case. Consequently, the bounded result does not cover every length through four and leaves the pointer metadata and public conversion behavior at the lower boundary unverified. Add a dedicated N = 0 harness that calls check_str_try_ref_from_bytes([]) without the invalid-input coverage assertion.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. A dedicated zero-length harness now checks [] against core::str::from_utf8 and exercises the public borrowed conversion without requiring an impossible invalid-input cover. The family domain is now lengths 0 through 4.
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. |
5a84428 to
658451e
Compare
170146b to
017f40b
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: 658451eef0
ℹ️ 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".
| // Oracle: `core::str::from_utf8` is the authoritative safe Rust oracle. | ||
| // Consequently, these harnesses prove zerocopy's validator/cast plumbing, | ||
| // not the standard library's UTF-8 algorithm. |
There was a problem hiding this comment.
BLOCKING: core::str::from_utf8 is also the operation used by the TryFromBytes for str implementation at lines 175–178, so it is independent for checking the surrounding cast/API plumbing but not for independently checking the validator's UTF-8 decision. This paragraph should cite the versioned standard-library contract and explicitly delimit that dependency, or use a genuinely independent UTF-8 oracle; otherwise the documented claim that the validator agrees with an independent oracle is unsupported.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L71
Useful? React with 👍 / 👎.
| // Excludes: Longer strings, properties outside Kani's model, an independent | ||
| // proof of UTF-8 validity itself, and the public borrowed API's | ||
| // invalid-input path. The latter is not invoked because a bug which | ||
| // materialized invalid `str` would be undefined before its `Result` could | ||
| // safely be inspected, and Kani does not completely check invalid values. |
There was a problem hiding this comment.
BLOCKING: The generic exclusion of “properties outside Kani's model” omits the concrete loop/allocation bounds and the harnesses' #[kani::unwind(5)] limit, and it does not explicitly identify Kani's incomplete reference-aliasing, pointer-provenance, or uninitialized-memory checking. The provenance limitation is especially material because this family claims input-address retention; document these bounds and non-goals explicitly so the stated proof domain is not broader than the verifier's coverage.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L71
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The UTF-8 family now records fixed stack inputs of lengths 0..=4, no allocation, no kani::assume, no explicit proof loop, and #[kani::unwind(5)]. It also limits pointer equality to an address observation in Kani’s model and explicitly leaves aliasing, provenance, invalid-value, and uninitialized-memory obligations in the tool/TCB boundary.
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. 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". |
7930a08 to
e2010a6
Compare
4caa07f to
eec7b6f
Compare
e2010a6 to
7930a08
Compare
eec7b6f to
4caa07f
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. 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". |
7930a08 to
d72291e
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. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 35cb45d881
ℹ️ 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".
| // https://doc.rust-lang.org/1.93.0/reference/type-layout.html#the-transparent-representation | ||
|
|
||
| fn utf8_oracle(bytes: &[u8]) -> (Result<&str, core::str::Utf8Error>, bool) { | ||
| let expected = core::str::from_utf8(bytes); |
There was a problem hiding this comment.
BLOCKING: Fresh evidence after the earlier thread was marked addressed is that current head 35cb45d again defines the oracle with core::str::from_utf8, while the TryFromBytes for str implementation under proof calls that same function at line 178. Thus the validator harness can check the surrounding pointer/cast plumbing, but its expected validity classification is not independent and cannot substantiate the documented validator-equivalence proof under the repository's oracle rules. Restore an independent safe Rust or language-derived UTF-8 classifier (or an explicitly labeled policy oracle), or drop the validator-equivalence claim.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L71
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed. The oracle no longer calls core::str::from_utf8; it is an independent bounded classifier over Unicode 17 Table 3-7's nine well-formed UTF-8 sequence rows. The proof labels the Rust-to-Unicode bridge and manual table transcription as EXTERNAL-SPEC/TCB, documents the loop invariant, and keeps the claim limited to lengths 0 through 4.
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. 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". |
|
@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. Can't wait for the next one! 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. Hooray! 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: Gti2px6v6qyolz34c5rkfkgsrcirhtxpe
|
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: 727f9f8719
ℹ️ 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 expected_valid = utf8_oracle(&bytes); | ||
| assert_same_bool(expected_valid, true); |
There was a problem hiding this comment.
BLOCKING: When either zero-length proof is selected by itself through ci/run_kani.sh, it emits no cover summary, so the wrapper's fail-closed check_cover_summaries rejects the otherwise successful run with “Kani emitted no recognized cover summary.” This makes both prove_empty_str_validators and prove_empty_str_try_ref_from_bytes unusable as independently selected harnesses; add a reachable valid-partition cover such as kani::cover!(expected_valid, "empty input is accepted") to each.
AGENTS.md reference: AGENTS.md:L67-L71
Useful? React with 👍 / 👎.
2 participants
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
Latest Update: v50 — Compare vs v49
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Gti2px6v6qyolz34c5rkfkgsrcirhtxpe && git checkout -b pr-Gti2px6v6qyolz34c5rkfkgsrcirhtxpe FETCH_HEADCheckout
git fetch origin refs/heads/Gti2px6v6qyolz34c5rkfkgsrcirhtxpe && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gti2px6v6qyolz34c5rkfkgsrcirhtxpe && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.