Repository navigation
Conversation
Mark the existing unsafe impl for [T] and prove its invariant from the actual element dictionary and retained model. Initialization covers all accepted language representations; realizability supplies bytes at each admitted slice's actual element count. Preserve native slice identity in trait binding and associated-type lifting. Reject changed elements and reference lookalikes. Add a Rust client that exercises slice and unsized-wrapper dictionary selection, and check its specification against independent count-indexed expectations. Refresh the complete extraction goldens and annotation snapshots. gherrit-pr-id: G5mwz4ieerzmvrwzsvsuahndzgsjmd53s Agent-authored-by: AI agent acting on joshlf's behalf
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 implements and verifies the native slice [T]: IntoBytes implementation in the Aeneas verification framework. It adds the invariant_proof marker to the slice IntoBytes implementation in zerocopy, updates the lowering audit and design documentation, and introduces the corresponding Lean specifications, proofs, and python test cases to verify slice initialization and realizability. I have no feedback to provide.
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## Gqvy7wjamomt5ju5ujyh4bgdxfluqkdr3 #3894 +/- ##
=====================================================================
- Coverage 48.67% 48.62% -0.06%
=====================================================================
Files 35 35
Lines 4754 4759 +5
=====================================================================
Hits 2314 2314
- Misses 2440 2445 +5 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
Mark the existing unsafe impl for [T] and prove its invariant from the
actual element dictionary and retained model. Initialization covers all
accepted language representations; realizability supplies bytes at each
admitted slice's actual element count.
Preserve native slice identity in trait binding and associated-type
lifting. Reject changed elements and reference lookalikes. Add a Rust
client that exercises slice and unsized-wrapper dictionary selection, and
check its specification against independent count-indexed expectations.
Refresh the complete extraction goldens and annotation snapshots.
Authored by an AI agent acting on joshlf's behalf.
⬇️ Download this PR
Branch
git fetch origin refs/heads/G5mwz4ieerzmvrwzsvsuahndzgsjmd53s && git checkout -b pr-G5mwz4ieerzmvrwzsvsuahndzgsjmd53s FETCH_HEADCheckout
git fetch origin refs/heads/G5mwz4ieerzmvrwzsvsuahndzgsjmd53s && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/G5mwz4ieerzmvrwzsvsuahndzgsjmd53s && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.