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 integrates support for the standard transmute primitive (core::intrinsics::transmute) into the Aeneas verification pipeline. It introduces a new private Rust module owned_transmute.rs for little-endian targets to perform owned conversions, alongside corresponding Lean specifications, proofs, and audit mechanisms to verify their correctness. Additionally, the compiler admission logic is updated to reject unsupported target overrides. The review feedback suggests a minor optimization in admission.py to avoid redundant evaluations of the variant function within a set comprehension.
| stages = {variant(f['body'])[0] for f in self.functions.values() | ||
| if f['body'] != 'Opaque'} | ||
| if f['body'] != 'Opaque' and variant(f['body'])[0] != 'Intrinsic'} |
There was a problem hiding this comment.
The variant(f['body'])[0] expression is evaluated twice for each function in the set comprehension. We can optimize this and improve readability by using a standard loop to build the set.
| stages = {variant(f['body'])[0] for f in self.functions.values() | |
| if f['body'] != 'Opaque'} | |
| if f['body'] != 'Opaque' and variant(f['body'])[0] != 'Intrinsic'} | |
| stages = set() | |
| for f in self.functions.values(): | |
| if f['body'] != 'Opaque': | |
| stage, _ = variant(f['body']) | |
| if stage != 'Intrinsic': | |
| stages.add(stage) |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## G4s3r4gpuxvvnoxoizjjgoy3b2rwmgi7g #3877 +/- ##
=====================================================================
- Coverage 60.00% 59.70% -0.30%
=====================================================================
Files 22 23 +1
Lines 3808 3827 +19
=====================================================================
Hits 2285 2285
- Misses 1523 1542 +19 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
d445ff7 to
24172ac
Compare
24172ac to
d6cac2b
Compare
4981be2 to
4f6d829
Compare
Verify the native standard transmute calls for u32 -> [u8; 4], [u8; 4] -> u32, and u8 -> bool. Retain the original ordered Rust endpoint types, require their canonical closed providers, and audit whole primitive and provider definitions plus every reached call, including calls inside unannotated helpers. Scope the numeric interpretation to the original little-endian 64-bit compiler target. The fixed unsigned scalars and initialized byte arrays have no padding or pointers. Boolean decoding accepts exactly zero and one and returns undef before constructing a Boolean for any invalid byte. Prove the Rust round-trip assertion root and independent arbitrary-outcome contracts for both integer conversions and the guarded Boolean conversion. The production transmute macro, pointer semantics, and generic FromBytes support remain deferred. gherrit-pr-id: Gwz22aqvb6z6qe2dmsgncsa6phc6jlxbf Agent-authored-by: AI agent acting on joshlf's behalf
4f6d829 to
ef5452c
Compare
d6cac2b to
1719318
Compare
Verify the native standard transmute calls for u32 -> [u8; 4],
[u8; 4] -> u32, and u8 -> bool. Retain the original ordered Rust
endpoint types, require their canonical closed providers, and audit
whole primitive and provider definitions plus every reached call,
including calls inside unannotated helpers.
Scope the numeric interpretation to the original little-endian 64-bit
compiler target. The fixed unsigned scalars and initialized byte arrays
have no padding or pointers. Boolean decoding accepts exactly zero and
one and returns undef before constructing a Boolean for any invalid byte.
Prove the Rust round-trip assertion root and independent arbitrary-outcome
contracts for both integer conversions and the guarded Boolean conversion.
The production transmute macro, pointer semantics, and generic FromBytes
support remain deferred.
Authored by an AI agent acting on joshlf's behalf.
Latest Update: v11 — Compare vs v10
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Gwz22aqvb6z6qe2dmsgncsa6phc6jlxbf && git checkout -b pr-Gwz22aqvb6z6qe2dmsgncsa6phc6jlxbf FETCH_HEADCheckout
git fetch origin refs/heads/Gwz22aqvb6z6qe2dmsgncsa6phc6jlxbf && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gwz22aqvb6z6qe2dmsgncsa6phc6jlxbf && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.