Repository navigation
Conversation
Byte-set inclusion puts no bound on an empty destination's address. State Project's postcondition with a nonnegative bounded offset, carry that contract through HasField, and use it in the NonNull and transitive projection safety arguments. Add shared mathematical Projection, Cast, and CastExact laws for explicit extents and opaque provenance. Prove composition, empty and one-past bounds, non-null propagation, slice splitting, and no-wrap consequences under explicit word bounds. Keep native pointer carriers rejected: the unchanged Aeneas pin does not retain their geometry. Exercise that boundary with well-formed native pointer shapes. Audit every imported shared Rust module and test root, including referent laws, so adding a library module cannot silently omit its assumptions. gherrit-pr-id: Gsul3w4vydc4wowguwwscielqttbpeytg 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. |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## Gsrhkadysza6axfyzqxp4iamxj6iko5ex #3891 +/- ##
==================================================================
Coverage 48.67% 48.67%
==================================================================
Files 35 35
Lines 4754 4754
==================================================================
Hits 2314 2314
Misses 2440 2440 ☔ 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 Rust.Pointer.Geometry module in Lean, which defines and proves numerical byte-range relations (such as Projection, Cast, and CastExact) between raw pointer values, including handling of empty referents and address bounds. It also updates the Lean test auditing mechanism to dynamically select submodules, documents the extraction boundaries in LOWERING_AUDIT.md, expands Python admission tests for raw pointer carriers, and refines safety documentation/comments in the zerocopy Rust crate to align with these geometric definitions. I have no feedback to provide as there are no review comments.
This branch has not been deployed
2 participants
Byte-set inclusion puts no bound on an empty destination's address. State
Project's postcondition with a nonnegative bounded offset, carry that
contract through HasField, and use it in the NonNull and transitive
projection safety arguments.
Add shared mathematical Projection, Cast, and CastExact laws for explicit
extents and opaque provenance. Prove composition, empty and one-past bounds,
non-null propagation, slice splitting, and no-wrap consequences under
explicit word bounds. Keep native pointer carriers rejected: the unchanged
Aeneas pin does not retain their geometry. Exercise that boundary with
well-formed native pointer shapes.
Audit every imported shared Rust module and test root, including referent
laws, so adding a library module cannot silently omit its assumptions.
Authored by an AI agent acting on joshlf's behalf.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Gsul3w4vydc4wowguwwscielqttbpeytg && git checkout -b pr-Gsul3w4vydc4wowguwwscielqttbpeytg FETCH_HEADCheckout
git fetch origin refs/heads/Gsul3w4vydc4wowguwwscielqttbpeytg && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gsul3w4vydc4wowguwwscielqttbpeytg && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.