Repository navigation
Conversation
A content transfer between dynamically sized referents needs the actual source and destination metadata. Equal byte widths cannot substitute a different count, especially for zero-sized or uninhabited elements. Derive each storage view's decoder and metadata from its installed model profile. Prove initialization, completeness, and transfer composition at one explicit pair, retaining the same intermediate view and metadata in both premises. Check wrapper metadata, empty domains, missing storage, and rejection of undef even with a trivial postcondition. These helpers do not change native TransmuteFrom promises or admit pointer execution, resource reasoning, or an assumed model of a local function. gherrit-pr-id: Gvxor5zd4poticd2jnomp3vuskfptpxar 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 introduces the IndexedReferent adapter and its corresponding tests in Lean 4, which compare byte domains at explicit metadata values to support content implications. It also updates the design and audit documentation to reflect these additions. The review feedback focuses on improving the robustness and readability of the Lean code by replacing positional underscores with named arguments in theorems like safe_to_initialized and initialized_to_safe, and making several parameters implicit in transfer_trans to simplify its usage in tests.
| theorem safe_to_initialized {source : RustModel Src} {destination : RustModel Dst} | ||
| (sourceView : StorageView source) (sm : sourceView.Metadata) | ||
| (destinationView : StorageView destination) (dm : destinationView.Metadata) | ||
| (law : sourceView.decoder.Initialized) : | ||
| transferAt sourceView sm destinationView dm .safe .initialized := | ||
| Rust.Referent.safe_to_initialized _ source.decode law sm _ _ |
There was a problem hiding this comment.
Using positional underscores (_) for explicit arguments can be fragile and hard to read. In Lean 4, it is more robust and idiomatic to use named arguments for parameters that cannot be automatically inferred, allowing Lean to implicitly synthesize the rest.
theorem safe_to_initialized {source : RustModel Src} {destination : RustModel Dst}
(sourceView : StorageView source) (sm : sourceView.Metadata)
(destinationView : StorageView destination) (dm : destinationView.Metadata)
(law : sourceView.decoder.Initialized) :
transferAt sourceView sm destinationView dm .safe .initialized :=
Rust.Referent.safe_to_initialized (decodeModel := source.decode) (initialized := law) (metadata := sm)
| theorem initialized_to_safe {source : RustModel Src} {destination : RustModel Dst} | ||
| (sourceView : StorageView source) (sm : sourceView.Metadata) | ||
| (destinationView : StorageView destination) (dm : destinationView.Metadata) | ||
| (law : destinationView.decoder.CompleteWith destination.decode) : | ||
| transferAt sourceView sm destinationView dm .initialized .safe := | ||
| Rust.Referent.initialized_to_safe _ destination.decode law dm _ _ |
There was a problem hiding this comment.
Similarly to safe_to_initialized, using named arguments here avoids fragile positional underscores and improves readability.
theorem initialized_to_safe {source : RustModel Src} {destination : RustModel Dst}
(sourceView : StorageView source) (sm : sourceView.Metadata)
(destinationView : StorageView destination) (dm : destinationView.Metadata)
(law : destinationView.decoder.CompleteWith destination.decode) :
transferAt sourceView sm destinationView dm .initialized .safe :=
Rust.Referent.initialized_to_safe (decodeModel := destination.decode) (complete := law) (metadata := dm)
| theorem transfer_trans {source : RustModel Src} {middle : RustModel Mid} | ||
| {destination : RustModel Dst} | ||
| (sourceView : StorageView source) (sm : sourceView.Metadata) | ||
| (middleView : StorageView middle) (mm : middleView.Metadata) | ||
| (destinationView : StorageView destination) (dm : destinationView.Metadata) | ||
| (firstState middleState lastState : Rust.Referent.State) | ||
| (first : transferAt sourceView sm middleView mm firstState middleState) | ||
| (second : transferAt middleView mm destinationView dm middleState lastState) | ||
| (width : sourceView.decoder.byteSize sm = middleView.decoder.byteSize mm) : | ||
| transferAt sourceView sm destinationView dm firstState lastState := | ||
| Rust.Referent.transfer_trans _ _ _ _ _ _ _ _ _ first second width |
There was a problem hiding this comment.
Many of the explicit parameters of transfer_trans (such as the views, metadata, and states) can be uniquely inferred by Lean's elaborator from the types of first, second, and width. Making these parameters implicit ({}) simplifies the theorem's usage significantly. Additionally, using named arguments for the call to Rust.Referent.transfer_trans avoids fragile positional underscores.
theorem transfer_trans {source : RustModel Src} {middle : RustModel Mid}
{destination : RustModel Dst}
{sourceView : StorageView source} {sm : sourceView.Metadata}
{middleView : StorageView middle} {mm : middleView.Metadata}
{destinationView : StorageView destination} {dm : destinationView.Metadata}
{firstState middleState lastState : Rust.Referent.State}
(first : transferAt sourceView sm middleView mm firstState middleState)
(second : transferAt middleView mm destinationView dm middleState lastState)
(width : sourceView.decoder.byteSize sm = middleView.decoder.byteSize mm) :
transferAt sourceView sm destinationView dm firstState lastState :=
Rust.Referent.transfer_trans (first := first) (second := second) (middleWidthAgrees := width)
| example : transferAt unitSliceView (0#usize) unitSliceView (2#usize) .safe .safe := | ||
| transfer_trans unitSliceView (0#usize) unitSliceView (1#usize) unitSliceView (2#usize) | ||
| .safe .safe .safe (unit_slice_transfer _ _) (unit_slice_transfer _ _) rfl |
There was a problem hiding this comment.
With the implicit parameter changes suggested for transfer_trans, this call can be simplified significantly, removing all the redundant explicit arguments.
example : transferAt unitSliceView (0#usize) unitSliceView (2#usize) .safe .safe :=
transfer_trans (unit_slice_transfer _ _) (unit_slice_transfer _ _) rfl
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## G5mwz4ieerzmvrwzsvsuahndzgsjmd53s #3895 +/- ##
==================================================================
Coverage 48.62% 48.62%
==================================================================
Files 35 35
Lines 4759 4759
==================================================================
Hits 2314 2314
Misses 2445 2445 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
A content transfer between dynamically sized referents needs the actual
source and destination metadata. Equal byte widths cannot substitute a
different count, especially for zero-sized or uninhabited elements.
Derive each storage view's decoder and metadata from its installed model
profile. Prove initialization, completeness, and transfer composition at
one explicit pair, retaining the same intermediate view and metadata in
both premises. Check wrapper metadata, empty domains, missing storage,
and rejection of undef even with a trivial postcondition.
These helpers do not change native TransmuteFrom promises or admit pointer
execution, resource reasoning, or an assumed model of a local function.
Authored by an AI agent acting on joshlf's behalf.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Gvxor5zd4poticd2jnomp3vuskfptpxar && git checkout -b pr-Gvxor5zd4poticd2jnomp3vuskfptpxar FETCH_HEADCheckout
git fetch origin refs/heads/Gvxor5zd4poticd2jnomp3vuskfptpxar && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gvxor5zd4poticd2jnomp3vuskfptpxar && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.