proofs: expose native EVMYulLean transition target#1743
proofs: expose native EVMYulLean transition target#1743
Conversation
![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: fc6b2b9c8a
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 19edb78f49
ℹ️ 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".
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?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: c61a0a8e5c
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 070a5f855f
ℹ️ 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".
| let matchedFns := candidates.filter (fun fn => | ||
| fn.params.map (fun param => param.ty) == argTypes) |
There was a problem hiding this comment.
This overload resolver requires exact type equality (fn.params ... == argTypes), but inferPureExprType classifies numeric literals as uint256. As a result, helper calls like foo(1) stop resolving when the only matching overload expects int256 (or other non-uint256 numeric types), even though the prior name/arity path accepted them and arithmetic typing already has signed-literal compatibility logic. This introduces a compile-time regression for contracts that pass literals to typed internal helper calls; the resolver should apply literal-compatible matching rather than strict equality.
Useful? React with 👍 / 👎.
|
Pushed What this commit actually adds:
What is still left to do:
Advice to complete this PR cleanly: Plan A:
Plan B:
Plan C:
My recommendation is Plan A first. The current tree is already structured around a concrete Validation on this branch remains green:
|
Th0rgal
force-pushed
the
codex/native-evmyullean-transition
branch
from
0672929 to
39ae307
Compare
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 39ae307375
ℹ️ 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".
| let valueExpr ← compileExpr fields dynamicSource value | ||
| let slotExpr := | ||
| if wordOffset == 0 then YulExpr.lit slot | ||
| else YulExpr.call "add" [YulExpr.lit slot, YulExpr.lit wordOffset] | ||
| pure [YulStmt.expr (YulExpr.call "sstore" [slotExpr, valueExpr])] |
There was a problem hiding this comment.
Stmt.setStorageWord currently emits exactly one sstore at the resolved base slot, but fields can carry aliasSlots (from slot-alias compatibility) that are intentionally kept in sync by other write paths like setStorage. With the current lowering, setPackedStorage/setStorageWord on an aliased field updates only the primary slot and leaves aliases stale, so contracts relying on alias mirroring for migration/back-compat can observe inconsistent state depending on which slot is read.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit 4f58dad. Configure here.
| let slots := slot :: f.aliasSlots | ||
| match slots with | ||
| | [] => | ||
| throw s!"Compilation error: internal invariant failure: no write slots for field '{field}' in setStorageWord" |
There was a problem hiding this comment.
Unreachable match arm on always-nonempty list
Low Severity
slots is defined as slot :: f.aliasSlots, which is always a cons cell, making the | [] => match arm at line 138 unreachable dead code. The throw will never execute because a list constructed with :: can never match []. The remaining two arms ([singleSlot] and _) already cover all possible shapes of a nonempty list, so the dead branch adds misleading noise about an "internal invariant failure" that structurally cannot occur.
Reviewed by Cursor Bugbot for commit 4f58dad. Configure here.
2 participants
Summary
Native.interpretIRRuntimeNativeas the executable native EVMYulLean target for emitted IR runtime YulYulResultEvmYul.Yul.callDispatcherFixed issues
Closes #1738.
Closes #1739.
Closes #1740.
Closes #1741.
Closes #1742.
Closes #1744.
Closes #1745.
Refs #1737.
Refs #1722.
Why
PR #1735 was only a docs/sync cleanup and did not close the native-runtime work from #1722. The current public theorem target still runs through
interpretYulRuntimeWithBackend .evmYulLean, which uses Verity's custom Yul statement interpreter with EVMYulLean-backed builtins. That bridge is useful, but it is not the simpler final architecture requested in #1737.This PR is now the native transition foundation plus the reported frontend/executable parity fixes needed before the remaining work can focus on the native public theorem target.
What changed
Native.interpretIRRuntimeNativeoverEvmYul.Yul.callDispatcher.verity_contractenvironment reads such asblockTimestamp,blockNumber,chainid,blobbasefee,contractAddress,msgSender, andmsgValue, including executable.runstate reads.internalCall/internalCallAssignremain only lower-level compilation-model IR.setPackedStorage root offset word, lowering toStmt.setStorageWord/sstore(root.slot + offset, word).arrayLength/arrayElement; dynamic element arrays such asArray StringandArray Bytesstill fail closed.Remaining work for #1737
Native.interpretIRRuntimeNativeor a total wrapper around itexecYulFuel/execYulFuelWithBackendto reference-oracle status and update trust-boundary docs accordinglyValidation
lake build Contracts.Smokelake build Contracts.MacroTranslateInvariantTestlake build Contracts.MacroTranslateRoundTripFuzzlake build Compiler.Proofs.YulGeneration.Backends.EvmYulLeanNativeHarness Compiler.Proofs.YulGeneration.Backends.EvmYulLeanNativeSmokeTestpython3 scripts/check_selectors.pypython3 -m unittest scripts/test_native_transition_api.py scripts/test_check_native_transition_doc.py scripts/test_check_selectors.py -vpython3 -m unittest scripts/test_generate_macro_property_tests.py -vpython3 scripts/check_macro_property_test_generation.pypython3 scripts/check_lean_hygiene.pypython3 scripts/check_verification_status_doc.pypython3 scripts/check_layer2_boundary_sync.pypython3 scripts/check_layer2_boundary_catalog_sync.pypython3 scripts/check_docs_workflow_sync.pygit diff --checkmake checkNote
Medium Risk
Expands the compiler IR surface (new array/Storage ops and overload handling) and adds a large native-execution proof seam; mistakes could change generated Yul or validation behavior for contracts relying on these features.
Overview
Adds a native EVMYulLean execution seam by introducing result-comparison predicates and end-to-end theorems in
Compiler/Proofs/EndToEnd.leanthat relateNative.interpretIRRuntimeNative(viacallDispatcher) to the existing EVMYulLean-backed interpreter, parameterized by an explicit observable storage-slot projection.Extends the compilation model and lowering to support packed full-word storage writes (
Stmt.setStorageWord) and dynamic array element word access (Expr.arrayElementWord), including new checked helper functions, param-loading bounds/stride fixes for arrays of multi-word static tuples, and usage analysis so only the required helpers become reserved/emitted.Tightens validation and determinism: external overloads are now de-duplicated by function signature (while internal helpers remain keyed by name), internal/external name collisions are rejected, and new smoke/tests cover the added IR forms and updated macro behaviors. CI/docs are updated so the weekly EVMYulLean fork conformance probe also builds the native harness and related oracle/smoke tests.
Reviewed by Cursor Bugbot for commit 4f58dad. Bugbot is set up for automated code reviews on this repo. Configure here.