feat: checked-arithmetic helper emission (#1993 emission half)#2028
Merged
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
#1999) (#2030) Extract the Panic(uint256) revert payload (selector 0x4e487b71 + one ABI word holding the panic code) into a reusable solidityPanicPayload builder so panic emission is compiler-owned and reusable for checked-arithmetic paths; assert the encoded code words (mstore(4, 17/18)) in the arithmetic-panic smoke test.
Contributor
| \n### CI Failure Hints\n\nFailed jobs: `compiler-regressions`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
Resolve #1997 internal-functions refactor vs checked-arithmetic feature: - compileExpr -> compileExprWithInternals threading (main) - internalParamYulNamesForType single source of truth + directForwardedInternalArgName? (main) - preserve checkedArithmeticHelpers reserved-names + Dispatch helpers (feature) - regenerate PrintAxioms.lean (5266 thms, 0 sorry)
The #1997 refactor moved findInternalFunctionForCall?, compileInternalCallArg, compileInternalCallArgsWithParams, and compileInternalCallArgs into ExpressionCompile.lean. The merge of origin/main kept the stale copies in Compile.lean too, producing "already been declared" errors. Remove the stale copies; ExpressionCompile.lean is the single source.
The merge brought in main's scalar-events supported-spec smoke test, which the SupportedSpecSurfaceWithScalarEvents struct now requires to discharge the noCheckedArithmetic obligation added in this PR. Prove it by simp over the spec definitions.
…tched origin/main merge The eb9fadb merge of origin/main into task/1993a-checked-arith dropped ~3385 lines of origin/main test content and left the namespace structure broken (InternalHelperDynamicArgs never closed), causing the compiler-regressions CI job to fail with a parse error. Restore origin/main's full feature-test file and re-graft task/1993a's unique checked-arithmetic helper assertions on top, so the union of both sides' test cases is preserved.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Implements the emission half of issue #1993 — Solidity-0.8-style overflow-checked arithmetic. (The proof-obligation /
LocalNoOverflowForaxiom-discharge half is tracked separately in #1993b → PR #2013.)checked_add_t_uint256,checked_sub_t_uint256,checked_mul_t_uint256,checked_div_t_uint256, pluspanic_error_0x11/panic_error_0x12.Compiler.emitYulWithOptionsfacade while keepingCodegenCommon.emitYulproof-stable.SupportedSpec*.noCheckedArithmeticsurface exclusions so checked arithmetic stays outside the existing helper-free proof theorems (kept axiom-clean) pending the #1993b discharge.Stacking
Based on
task/2000-dynamic-events(#2020), the tip of the Tier-1 dynamic-ABI stack.Test plan
lake build Verity Contracts Compiler PrintAxioms→ "Build completed successfully."scripts/refresh_verification_artifacts.sh→ "[refresh] PASS"make check→ "All checks passed."Note
Medium Risk
Changes compiler Yul for arithmetic and panic behavior on contracts that trigger the new path; proof theorems explicitly exclude that fragment until follow-up work, but mis-detection or a bad fold could affect generated runtime code.
Overview
Adds Solidity 0.8-style checked
uint256arithmetic to the compiler: when contracts use panic guards for overflow, underflow, or division by zero, the pipeline emits on-demand Yul helpers (checked_add/sub/mul/div_t_uint256pluspanic_error_0x11/0x12with the standardPanic(uint256)selector) and reserves those symbol names so user code cannot collide.After normal Yul emission (via
emitYulWithOptions), a peephole pass folds matchingifrevert guards plus rawadd/sub/mul/divinto calls to those helpers, while plainCodegenCommon.emitYulstays unchanged for existing proofs.Proof surface:
SupportedSpec*gainsnoCheckedArithmetic, keeping checked-arithmetic contracts outside current helper-free IR-generation theorems until the separate discharge work lands.The same diff also introduces
Calls.selfDelegateMulticallBytes(self-delegatecallmulticall(bytes[])with offset checks and revert bubbling, documented as an ECM assumption) and expands event source-shape proof scaffolding for dynamic ABI events—likely from the stacked branch, not the core #1993 emission story.Reviewed by Cursor Bugbot for commit 87afe71. Bugbot is set up for automated code reviews on this repo. Configure here.