Repository navigation
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. |
![gemini-code-assist[bot]](https://avatars.githubusercontent.com/in/956858?s=60&v=4){kind=small}
There was a problem hiding this comment.
Code Review
This pull request formalizes and verifies referent validity implications within the Aeneas verification framework for zerocopy. It updates design documentation, adds Lean models and proofs for validity markers and transparent wrappers, and introduces verification clients in zerocopy/src/pointer/referent_checks.rs. The feedback suggests a minor refactoring in the newly added referent_checks.rs to move the Dst: ?Sized bounds from the where clauses to the generic parameter lists for consistency with Src: ?Sized.
| fn require_transfer<Src: ?Sized, Dst, SV, DV>() | ||
| where | ||
| Dst: TransmuteFrom<Src, SV, DV> + ?Sized, | ||
| { | ||
| } |
There was a problem hiding this comment.
For consistency with Src: ?Sized in the generic parameter list, it is more idiomatic to declare Dst: ?Sized in the generic parameter list as well, rather than relaxing the bound in the where clause.
| fn require_transfer<Src: ?Sized, Dst, SV, DV>() | |
| where | |
| Dst: TransmuteFrom<Src, SV, DV> + ?Sized, | |
| { | |
| } | |
| fn require_transfer<Src: ?Sized, Dst: ?Sized, SV, DV>() | |
| where | |
| Dst: TransmuteFrom<Src, SV, DV>, | |
| { | |
| } |
| fn require_type_independent<Src: ?Sized, Dst, SV, DV>() | ||
| where | ||
| Dst: CastableFrom<Src, SV, DV> + ?Sized, | ||
| { | ||
| } |
There was a problem hiding this comment.
For consistency with Src: ?Sized in the generic parameter list, it is more idiomatic to declare Dst: ?Sized in the generic parameter list as well, rather than relaxing the bound in the where clause.
| fn require_type_independent<Src: ?Sized, Dst, SV, DV>() | |
| where | |
| Dst: CastableFrom<Src, SV, DV> + ?Sized, | |
| { | |
| } | |
| fn require_type_independent<Src: ?Sized, Dst: ?Sized, SV, DV>() | |
| where | |
| Dst: CastableFrom<Src, SV, DV>, | |
| { | |
| } |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## Gd7mcbq7u5yus3mis4yyvjdxx6qo4trg6 #3890 +/- ##
====================================================================
Coverage ? 48.67%
====================================================================
Files ? 35
Lines ? 4754
Branches ? 0
====================================================================
Hits ? 2314
Misses ? 2440
Partials ? 0 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
![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: 3c48caa912
ℹ️ 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".
| contentTransfer modelBool boolDecoder (modelUScalar .U8) u8BitDecoder .safe .initialized ∧ | ||
| contentTransfer (modelUScalar .U8) u8BitDecoder modelBool boolDecoder .initialized .uninit ∧ |
There was a problem hiding this comment.
The concrete client invokes six dictionaries, but this independent contract observes only the bool → u8 and u8 → bool transfers and one type-independent pair. In particular, the [u8; 4] → u32 initialized-to-safe call and the ManuallyDrop<u8> → u8 wrapper call on lines 74 and 76 of referent_checks.rs are absent, so their calls can be removed or replaced while concrete_transfers_spec and its required-contract proof still pass. Add postconditions for those transfers (and the omitted Uninit pair) so this harness actually checks every concrete implementation it claims to select.
Useful? React with 👍 / 👎.
8473f05 to
508e3b3
Compare
3c48caa to
21b16c4
Compare
Annotate Validity, TransmuteFrom, and CastableFrom, and prove 24 native implementation laws: the four validity markers, four blanket transfers, twelve wrapper directions, two Cell/UnsafeCell chains, and the two permitted type-independent state pairs. Safe contents must pass the retained physical and mathematical decoders. Empty safe domains remain valid without constructing an inhabitant. Attach optional state codes to the existing generated providers for the four empty marker types, and check each against its actual Validity::KIND. Keep the original Rust trait signatures. Missing metadata cannot silently select a weaker state, and missing physical support supplies no decoder view from which to apply a content law. Add generic and concrete Rust clients that consume the actual dictionaries. Check their proofs against independent byte-content expectations, retaining all original inputs and model providers. Add negative controls for invalid boolean bytes, extra proof premises, replaced providers, missing support, and forbidden results even outside the interpreted state cases. Refresh the golden models and generated annotation snapshots. These are conditional referent-content claims, not pointer access or resource proofs. AsInitialized contents and opaque MaybeUninit storage remain deferred. gherrit-pr-id: Gsrhkadysza6axfyzqxp4iamxj6iko5ex Agent-authored-by: AI agent acting on joshlf's behalf
21b16c4 to
5d3a57a
Compare
508e3b3 to
3abac09
Compare
Annotate Validity, TransmuteFrom, and CastableFrom, and prove 24 native
implementation laws: the four validity markers, four blanket transfers,
twelve wrapper directions, two Cell/UnsafeCell chains, and the two
permitted type-independent state pairs. Safe contents must pass the
retained physical and mathematical decoders. Empty safe domains remain
valid without constructing an inhabitant.
Attach optional state codes to the existing generated providers for the
four empty marker types, and check each against its actual Validity::KIND.
Keep the original Rust trait signatures. Missing metadata cannot silently
select a weaker state, and missing physical support supplies no decoder
view from which to apply a content law.
Add generic and concrete Rust clients that consume the actual dictionaries.
Check their proofs against independent byte-content expectations, retaining
all original inputs and model providers. Add negative controls for invalid
boolean bytes, extra proof premises, replaced providers, missing support,
and forbidden results even outside the interpreted state cases. Refresh
the golden models and generated annotation snapshots.
These are conditional referent-content claims, not pointer access or
resource proofs. AsInitialized contents and opaque MaybeUninit storage
remain deferred.
Authored by an AI agent acting on joshlf's behalf.
Latest Update: v4 — Compare vs v3
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Gsrhkadysza6axfyzqxp4iamxj6iko5ex && git checkout -b pr-Gsrhkadysza6axfyzqxp4iamxj6iko5ex FETCH_HEADCheckout
git fetch origin refs/heads/Gsrhkadysza6axfyzqxp4iamxj6iko5ex && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gsrhkadysza6axfyzqxp4iamxj6iko5ex && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.