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❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## Gdtlvwakxpzsmcwa7vhtmv7d5h63sbw3l #3884 +/- ##
=====================================================================
+ Coverage 48.80% 48.89% +0.08%
=====================================================================
Files 33 34 +1
Lines 4725 4733 +8
=====================================================================
+ Hits 2306 2314 +8
Misses 2419 2419 ☔ 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 generic owned conversions through transmute_copy in zerocopy along with formal verification models, proofs, and audits in Lean and Python (Aeneas) to verify their safety. The review feedback highlights three key issues in the Aeneas admission checker (admission.py): a crash when processing on_unwind in unstructured control flow blocks due to unhandled variant options, a false positive in the transmute-copy closure audit caused by duplicate recording of global constant initializers, and potential runtime overhead/dependency issues from using re.fullmatch instead of basic string operations for type variable validation.
| elif tag in {'Call', 'Drop', 'Assert'}: | ||
| children = [term['target'], term['on_unwind']] |
There was a problem hiding this comment.
In Charon, on_unwind is an Option<BlockId> represented as a variant (e.g., {"None": []} or {"Some": block_id}). Passing it directly to children causes type(child) is not int to evaluate to True, which raises a ValueError and crashes the audit for any unstructured function containing a Call, Drop, or Assert terminator. Unpack the on_unwind option using variant to extract the actual block index when it is Some.
| elif tag in {'Call', 'Drop', 'Assert'}: | |
| children = [term['target'], term['on_unwind']] | |
| elif tag in {'Call', 'Drop', 'Assert'}: | |
| children = [term['target']] | |
| if term.get('on_unwind'): | |
| unwind_tag, unwind_val = variant(term['on_unwind']) | |
| if unwind_tag == 'Some': | |
| children.append(unwind_val) |
| if tag == 'Call': | ||
| function, _ = producer | ||
| kind, callee = variant(function['kind']) | ||
| if kind != 'Fun': | ||
| raise ValueError('Unresolved global initializer') | ||
| self.record_native_call(callee, arguments, kind='global') |
There was a problem hiding this comment.
When a global constant is referenced multiple times within the same function, global_value is called multiple times. Since record_native_call is called before checking if index in self.globals:, it records duplicate calls from the current function to the global's initializer. This causes duplicate edges in edges, which leads count(owner) to sum the same child multiple times and falsely raise ValueError('Transmute-copy closure contains multiple byte choices'). Prevent duplicate recording by checking if the call has already been recorded for the current caller.
| if tag == 'Call': | |
| function, _ = producer | |
| kind, callee = variant(function['kind']) | |
| if kind != 'Fun': | |
| raise ValueError('Unresolved global initializer') | |
| self.record_native_call(callee, arguments, kind='global') | |
| if tag == 'Call': | |
| function, _ = producer | |
| kind, callee = variant(function['kind']) | |
| if kind != 'Fun': | |
| raise ValueError('Unresolved global initializer') | |
| if not any(row.get('caller_def_id') == self.current_function['def_id'] and | |
| row.get('callee_def_id') == callee and | |
| row.get('kind') == 'global' | |
| for row in self.calls): | |
| self.record_native_call(callee, arguments, kind='global') |
| if not isinstance(arguments, list) or not arguments or any( | ||
| not isinstance(argument, str) or | ||
| (match := re.fullmatch(r'T(0|[1-9][0-9]*)', argument)) is None or | ||
| int(match[1]) not in source_indices for argument in arguments): |
There was a problem hiding this comment.
Using re.fullmatch introduces regex overhead and a potential runtime dependency on the re module if it is not imported in admission.py. Since Charon type variables are always named T0, T1, etc., we can simplify this check using basic string operations (startswith and isdigit), which is both safer and more efficient.
| if not isinstance(arguments, list) or not arguments or any( | |
| not isinstance(argument, str) or | |
| (match := re.fullmatch(r'T(0|[1-9][0-9]*)', argument)) is None or | |
| int(match[1]) not in source_indices for argument in arguments): | |
| if not isinstance(arguments, list) or not arguments or any( | |
| not isinstance(argument, str) or | |
| not argument.startswith('T') or | |
| not argument[1:].isdigit() or | |
| int(argument[1:]) not in source_indices for argument in arguments): |
f2aa9ee to
a11d390
Compare
Add a trait-bounded const helper that consumes Src: IntoBytes and returns Dst: FromBytes after an equal-size post-monomorphization assertion. Use ManuallyDrop and the standard transmute_copy operation. Their Lean interpretations retain the original extracted arguments before adding semantic providers. The helper requires Rust 1.83 to borrow a generic source that may have interior mutability in const evaluation. The production transmute macro remains unchanged. Interpret the copy through both physical decoders and destination model admission. Quantify generic proofs over a checked representation preference, then prove coverage of every represented output while fixing the decoders. This preserves ambiguous source encodings. Admission limits the fragment to one conversion with polymorphic forwarding; independent choices across repeated operations require a richer effect model. Audit original compiler endpoints, constant initializers, exact retained providers, and complete primitive interpretations. Preserve the ordinary ABI size queries and state physical-width correspondence explicitly. The existing ownership checker proves the erased conditional drops empty. Prove the actual helper and a caller that reuses its theorem. Add independent contract expectations and compiled mutation controls for substituted providers, altered primitive models, missing call witnesses, and the size guard. Physical profiles and standard-library semantics remain explicit Rust correspondence premises; this adds no general pointer/resource model. Regenerate UI snapshots on all three pinned compilers for the shifted source line numbers. Their diagnostic text is unchanged. gherrit-pr-id: Gmhd5pbk4jan7lwabm442fdhchwui6nnr Agent-authored-by: AI agent acting on joshlf's behalf
633fe56 to
dec2c00
Compare
a11d390 to
394b6d6
Compare
Add a trait-bounded const helper that consumes Src: IntoBytes and returns
Dst: FromBytes after an equal-size post-monomorphization assertion. Use
ManuallyDrop and the standard transmute_copy operation. Their Lean
interpretations retain the original extracted arguments before adding
semantic providers. The helper requires Rust 1.83 to borrow a generic
source that may have interior mutability in const evaluation. The production
transmute macro remains unchanged.
Interpret the copy through both physical decoders and destination model
admission. Quantify generic proofs over a checked representation preference,
then prove coverage of every represented output while fixing the decoders.
This preserves ambiguous source encodings. Admission limits the fragment
to one conversion with polymorphic forwarding; independent choices across
repeated operations require a richer effect model.
Audit original compiler endpoints, constant initializers, exact retained
providers, and complete primitive interpretations. Preserve the ordinary
ABI size queries and state physical-width correspondence explicitly. The
existing ownership checker proves the erased conditional drops empty.
Prove the actual helper and a caller that reuses its theorem. Add independent
contract expectations and compiled mutation controls for substituted
providers, altered primitive models, missing call witnesses, and the size
guard. Physical profiles and standard-library semantics remain explicit
Rust correspondence premises; this adds no general pointer/resource model.
Regenerate UI snapshots on all three pinned compilers for the shifted
source line numbers. Their diagnostic text is unchanged.
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/Gmhd5pbk4jan7lwabm442fdhchwui6nnr && git checkout -b pr-Gmhd5pbk4jan7lwabm442fdhchwui6nnr FETCH_HEADCheckout
git fetch origin refs/heads/Gmhd5pbk4jan7lwabm442fdhchwui6nnr && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gmhd5pbk4jan7lwabm442fdhchwui6nnr && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.