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. |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## Gcwyaqhevirytq5t6oazk3klcbcycuwnn #3883 +/- ##
====================================================================
Coverage ? 48.80%
====================================================================
Files ? 33
Lines ? 4725
Branches ? 0
====================================================================
Hits ? 2306
Misses ? 2419
Partials ? 0 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
![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 introduces the concept of "source realizability" to the formal verification of the IntoBytes trait within the Aeneas verification framework. It updates the into_bytes_initialized trait invariant to require that every mathematically admitted raw value has at least one physical byte representation. To support this, new Lean files (RustRealizability.lean, RustRealizabilityModels.lean, and RustRealizabilityTests.lean) are added to provide and test realizability proofs for primitives, arrays, and various wrapper types. Existing proofs and trait declarations are updated accordingly to incorporate these new realizability obligations. There are no review comments to address, and I have no feedback to provide.
An initialized physical decoder can reject every byte string. Its initialization law then holds without supplying any bytes for an admitted source value, so that law alone cannot justify a conversion out of the value. Require each mathematically admitted source value to have a physical representation. Prove this stronger IntoBytes invariant for the existing primitive, array, and wrapper implementations. Keep initialization over the full physical decoding domain, independently of library admission. The existence requirement permits multiple representations of one value and remains vacuous for uninhabited sources. Regression examples cover both cases, empty arrays, and an initialized decoder that cannot represent one of its admitted values. gherrit-pr-id: Gdtlvwakxpzsmcwa7vhtmv7d5h63sbw3l Agent-authored-by: AI agent acting on joshlf's behalf
633fe56 to
dec2c00
Compare
This branch has not been deployed
2 participants
An initialized physical decoder can reject every byte string. Its
initialization law then holds without supplying any bytes for an admitted
source value, so that law alone cannot justify a conversion out of the
value.
Require each mathematically admitted source value to have a physical
representation. Prove this stronger IntoBytes invariant for the existing
primitive, array, and wrapper implementations. Keep initialization over
the full physical decoding domain, independently of library admission.
The existence requirement permits multiple representations of one value
and remains vacuous for uninhabited sources. Regression examples cover
both cases, empty arrays, and an initialized decoder that cannot represent
one of its admitted values.
Authored by an AI agent acting on joshlf's behalf.
Latest Update: v6 — Compare vs v5
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Gdtlvwakxpzsmcwa7vhtmv7d5h63sbw3l && git checkout -b pr-Gdtlvwakxpzsmcwa7vhtmv7d5h63sbw3l FETCH_HEADCheckout
git fetch origin refs/heads/Gdtlvwakxpzsmcwa7vhtmv7d5h63sbw3l && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gdtlvwakxpzsmcwa7vhtmv7d5h63sbw3l && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.