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✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## G5ql2xwdsnzdupc5d4auj6l5vgi5okgrc #3848 +/- ##
====================================================================
Coverage ? 61.30%
====================================================================
Files ? 20
Lines ? 3727
Branches ? 0
====================================================================
Hits ? 2285
Misses ? 1442
Partials ? 0 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: dccb7830a6
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| body = {'call': body['call'], 'on_unwind': | ||
| {'span': term['span'], 'id': 0, 'statements': []}} |
There was a problem hiding this comment.
When an unstructured Call has an on_unwind target, this replaces it with an empty block; cfg() later scans the referenced block independently with unwind=False. Consequently, cleanup blocks containing supported-looking Assign or Call effects bypass the restricted unwind-effect check. If Charon subsequently removes that ignored cleanup path, the final LLBC stage cannot catch the omitted effect, so admission can certify execution that Aeneas does not model. Traverse blocks according to their unwind edges, or otherwise mark every cleanup target and apply the unwind restrictions to it.
Useful? React with 👍 / 👎.
| if value and (name in {'RUSTFLAGS', 'CARGO_ENCODED_RUSTFLAGS', | ||
| 'CARGO_BUILD_RUSTFLAGS', 'RUSTC', 'RUSTC_WRAPPER', | ||
| 'RUSTC_WORKSPACE_WRAPPER', 'CHARON_ARGS'} or | ||
| re.fullmatch(r'CARGO_TARGET_.*_RUSTFLAGS', name)): |
There was a problem hiding this comment.
The override check omits Cargo's configuration-derived environment variables such as CARGO_BUILD_RUSTC, CARGO_BUILD_RUSTC_WRAPPER, and CARGO_BUILD_RUSTC_WORKSPACE_WRAPPER. In particular, a workspace wrapper composes with Charon's own RUSTC_WRAPPER, so setting it allows an additional executable to participate in compilation while both pre- and post-extraction identities remain unchanged because the variable is neither rejected nor hashed. Reject these aliases alongside their direct RUSTC* equivalents before treating the MIR pipeline as controlled.
Useful? React with 👍 / 👎.
| if (not isinstance(evidence, dict) or evidence.get('version') != 1 or | ||
| evidence.get('sources') != manifest.get('sources') or | ||
| evidence.get('registry') != admission.digest(root / 'verification/aeneas/external.json') or | ||
| evidence.get('inputs') != admission.input_identity(root) or | ||
| set(evidence.get('stages', {})) != {'before', 'llbc'} or | ||
| any(stage.get('roots') != roots for stage in evidence['stages'].values())): |
There was a problem hiding this comment.
For a verified-live project, this validates Rust sources, registry, toolchain inputs, stages, and roots but never compares manifest["model"] with the current Zerocopy/Funs.lean and Types.lean. If either generated model is edited after assembly— including during the proof-check window—lake clean rebuilds and audits that edited model while stale admission evidence is still accepted; an altered pure definition can therefore make the proofs pass without corresponding to the inspected LLBC. Recompute the model fingerprint before and after proof checking, just as the Rust input identity is checked.
Useful? React with 👍 / 👎.
| if tag == 'Call': | ||
| function, args = body | ||
| if variant(function['kind'])[0] != 'Fun': | ||
| raise ValueError('Unresolved constant producer') | ||
| for arg in args: | ||
| self.constant(arg) | ||
| self.visit(function['kind']['Fun']) |
There was a problem hiding this comment.
For a ConstantExpr::Call, this visits only the generic function declaration and ignores the concrete generics stored on the function operand. A constant or promoted call to the opaque transmute_unchecked can therefore match its generic registry prototype with an instantiation other than the sole admitted u8 → bool case, bypassing the explicit instantiation check used for ordinary calls. Apply the same concrete type/const/dictionary validation and boundary recording to constant calls before accepting their producer.
Useful? React with 👍 / 👎.
| leaf = 'core::num::{usize}::unchecked_' + op.lower() | ||
| if not any(row['rust'] == leaf for row in self.registry): | ||
| raise ValueError(f'No reviewed interpretation for {leaf}') | ||
| self.calls.append({'caller': self.current, 'callee': leaf, | ||
| 'implicit': True}) |
There was a problem hiding this comment.
This branch records an implicit unchecked_add or unchecked_mul only in calls, while check_translation() validates failure-capable signatures exclusively for entries in the executions list. Thus, when the primitive appears only as the expected UB-mode BinaryOp, its generated Lean signature is never checked; an infallible translation that erases the unsafe precondition can pass admission unless the same leaf happens to be visited independently. Record the selected registry interpretation in executions, or make the translation check consume these implicit call records directly.
Useful? React with 👍 / 👎.
| for path in sorted(paths): | ||
| combined.update(str(path.relative_to(root)).encode()) | ||
| combined.update(path.read_bytes()) | ||
| tools = Path(os.environ['AENEAS_TOOLCHAIN_DIR']) |
There was a problem hiding this comment.
run.sh supports an unset AENEAS_TOOLCHAIN_DIR by assigning tools_dir to target/aeneas/toolchain, but neither that assignment nor toolchain.sh exports the variable. On the normal CI invocation (bash verification/aeneas/run.sh with no override), the first admission.py inputs call therefore reaches this direct environment lookup and raises KeyError before extraction starts. Use the same repository-relative default here or explicitly export the resolved directory in the driver.
Useful? React with 👍 / 👎.
| name = rust_identity(file, owner['path']) | ||
| annotations.source_body_digests.setdefault(name, []).append( | ||
| hashlib.sha256(encoded[owner['open']:owner['close']]).hexdigest()) |
There was a problem hiding this comment.
The trust check hashes only the lexical bytes between each function's body braces. transmute_unchecked, for example, invokes the crate-local static_assert! macro, so changing that macro—or the implementation of any local helper called by an opaque boundary—changes the compiled execution without changing this digest. Although the project identity records that some source changed, it is not compared with a reviewed expected project identity, so the unchanged registry entry still selects the old trusted interpretation. Hash the expanded/MIR body or include all transitive local dependencies in the registered boundary identity.
Useful? React with 👍 / 👎.
| if current == `Aeneas.Std.Option.ofResult then | ||
| throwError "Extracted execution depends on unsupported failure erasure: {current}" | ||
| if let some owner := env.getModuleIdxFor? current then | ||
| let moduleName := env.allImportedModuleNames[owner.toNat]! | ||
| if moduleName.getRoot == `Aeneas && !auditModules.contains owner then continue |
There was a problem hiding this comment.
This dependency walk only rejects the exact Aeneas.Std.Option.ofResult adapter; it never compares the registered transmute_unchecked, copy_unchecked, or unchecked-arithmetic implementations with their required guards and bad-input behavior. An axiom-free Lean definition that returns .ok for an invalid Boolean, oversized copy, or overflowing arithmetic therefore passes both this walk and the axiom audit, and the generated-template check establishes only a Result-typed signature. Add compiled definitional or theorem checks covering each registered primitive's complete input domain before accepting its interpretation.
Useful? React with 👍 / 👎.
7846f80 to
6bd1390
Compare
f9211b5 to
9f142e4
Compare
c678614 to
3c4fe9b
Compare
9f142e4 to
b03b22f
Compare
3c4fe9b to
556d864
Compare
b03b22f to
f561c6e
Compare
556d864 to
5345d5d
Compare
An extracted proof cannot account for an effect that translation erased. Preserve Charon's imported promoted MIR before its transformation passes and inspect both that snapshot and final LLBC from every discovered function specification, following callees and unwind paths. Admit only the reviewed value-and-borrow fragment or an exact registered external interpretation. Reject unknown operations, unsupported instantiations and extraction options, missing snapshots, and lost guarded calls. Refuse optimized-MIR fallback for stolen local bodies. Preserve compiler-owned doc attributes and their literal source origins before item selection. This gives later annotation binding evidence from macro expansion without guessing an impl from its textual header. Treat only the compiler's exact tuple/unit constructor aliases as the parent struct's attributes; fields, variants and statements remain distinct. Omit unused provided-method signatures before they import unrelated trait dependencies. Reject resolved calls to omitted methods, including inherited and overridden methods; required slots retain their identities. Native controls check both omission and annotation-origin behavior. Bind the report to compiler inputs, source bodies and the patched runtime. Audit downstream Lean dependencies for failure-erasing adapters, including uses hidden behind opaque helpers. The checker constrains the trusted translation boundary; it is not a proof of rustc or Charon's semantics. gherrit-pr-id: Glga77guruqohhu34sv7kfiu3slnotqyv Agent-authored-by: AI agent acting on joshlf's behalf
5345d5d to
716ef6d
Compare
f561c6e to
1fd4064
Compare
An extracted proof cannot account for an effect that translation erased.
Preserve Charon's imported promoted MIR before its transformation passes
and inspect both that snapshot and final LLBC from every discovered
function specification, following callees and unwind paths.
Admit only the reviewed value-and-borrow fragment or an exact registered
external interpretation. Reject unknown operations, unsupported
instantiations and extraction options, missing snapshots, and lost guarded
calls. Refuse optimized-MIR fallback for stolen local bodies.
Preserve compiler-owned doc attributes and their literal source origins
before item selection. This gives later annotation binding evidence from
macro expansion without guessing an impl from its textual header. Treat
only the compiler's exact tuple/unit constructor aliases as the parent
struct's attributes; fields, variants and statements remain distinct.
Omit unused provided-method signatures before they import unrelated
trait dependencies. Reject resolved calls to omitted methods, including
inherited and overridden methods; required slots retain their identities.
Native controls check both omission and annotation-origin behavior.
Bind the report to compiler inputs, source bodies and the patched runtime.
Audit downstream Lean dependencies for failure-erasing adapters, including
uses hidden behind opaque helpers. The checker constrains the trusted
translation boundary; it is not a proof of rustc or Charon's semantics.
Authored by an AI agent acting on joshlf's behalf.
Latest Update: v26 — Compare vs v25
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Glga77guruqohhu34sv7kfiu3slnotqyv && git checkout -b pr-Glga77guruqohhu34sv7kfiu3slnotqyv FETCH_HEADCheckout
git fetch origin refs/heads/Glga77guruqohhu34sv7kfiu3slnotqyv && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Glga77guruqohhu34sv7kfiu3slnotqyv && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.