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".
| \n### CI Failure Hints\n\nFailed jobs: `build`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 20e7b900ca
ℹ️ 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: 20e7b900ca
ℹ️ 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: f85598c41a
ℹ️ 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".
| $(← translatePureExprWithTypes fields constDecls immutableDecls params locals offset)) | ||
| | _ => | ||
| match matchLocalFunctionApp? functions rhs with | ||
| match ← resolveLocalFunctionApp? fields constDecls immutableDecls #[] functions params locals rhs with |
There was a problem hiding this comment.
resolveLocalFunctionApp? infers argument types via inferPureExprType, but this translation path passes #[] as externalDecls. When a local helper call in a bind source includes an externalCall argument (which is valid and can pass earlier type validation), this second inference run cannot resolve the external and fails during translation with an unsupported/unknown external error. That creates a compile-time regression for contracts that wrap externals inside internal helper calls; the resolver here needs the actual external declarations (and the same fix at the other #[] call sites).
Useful? React with 👍 / 👎.
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
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 e01b323. Configure here.
| match firstDuplicateName (spec.functions.map functionSignature) with | ||
| | some dup => | ||
| throw s!"Compilation error: duplicate function name '{dup}' in {spec.name}" | ||
| throw s!"Compilation error: duplicate function signature '{dup}' in {spec.name}" |
There was a problem hiding this comment.
Signature-based duplicate check misses same-name internal functions
Medium Severity
The duplicate function check changed from comparing names (·.name) to comparing full signatures (functionSignature). This means two functions sharing the same name but with different parameter types now pass validation. For internal functions, this is unsafe — compileInternalFunction emits Yul funcDef statements keyed by name, so same-name internal functions would produce duplicate Yul function definitions regardless of their parameter types.
Reviewed by Cursor Bugbot for commit e01b323. Configure here.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e01b323750
ℹ️ 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".
| exprs := exprs.push (← `(Compiler.CompilationModel.Expr.arrayElementWord | ||
| $(strTerm paramName) | ||
| $indexExpr | ||
| $(natTerm elementWords) |
There was a problem hiding this comment.
Tuple destructuring for arrayElement expands into one Expr.arrayElementWord per member, each reusing $indexExpr directly, so the index expression is re-evaluated for every field. If the index contains call-like operations (e.g., call, delegatecall, externalCall), this duplicates side effects and can even read different tuple elements across fields, which diverges from the source-level arrayElement semantics that should evaluate the index once before destructuring.
Useful? React with 👍 / 👎.
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
Touches compiler IR, validation, and Yul codegen helpers around storage writes and ABI array bounds, which can affect generated contract semantics. Native harness additions are mostly additive but increase coupling to EVMYulLean execution/projection behavior.
Overview
Adds a new executable native EVMYulLean runtime target (
Native.interpretIRRuntimeNative) built onEvmYul.Yul.callDispatcher, including a much more complete state/result projection that preserves prior events and a largenative_decidesmoke-test suite to validate lowering, dispatch, environment/storage/log semantics, and failure-closed behavior.Extends the compilation model/IR with packed-word capabilities:
Expr.arrayElementWord(checked word access inside static-width array elements) andStmt.setStorageWord(write tofield.slot + offset), plus new Yul helpers for word-indexed array loads, updated array-length bounds checks for multi-word elements, and updated validation/usage/trust-surface tracking for the new constructors.Tightens ABI/dispatch correctness by deduping external functions by full
functionSignature(not just name), and updates docs + the fork conformance workflow to include building the new native harness/smoke tests. Contract-side support is adjusted with new packed/struct slot helpers (setPackedStorage,structMemberAt/setStructMemberAt, etc.) and minor API cleanup (environment builtins now returnContractvalues;toparams renamed totoAddr).Reviewed by Cursor Bugbot for commit e01b323. Bugbot is set up for automated code reviews on this repo. Configure here.