Skip to content

feat(Codegen): factor solidityPanicPayload for Panic(uint256) emission (#1999)#2030

Merged
Th0rgal merged 1 commit into
task/1993a-checked-arithfrom
task/1999-panic
Jun 18, 2026
Merged

feat(Codegen): factor solidityPanicPayload for Panic(uint256) emission (#1999)#2030
Th0rgal merged 1 commit into
task/1993a-checked-arithfrom
task/1999-panic

Conversation

@Th0rgal

@Th0rgal Th0rgal commented Jun 13, 2026

Copy link
Copy Markdown
Member

Summary

  • Factor the Panic(uint256) ABI payload into a reusable solidityPanicPayload builder in Compiler/CompilationModel/DynamicData.lean; panicErrorHelper now delegates to it. Behavior-preserving emission refactor (emitted Yul unchanged).
  • Strengthen the arithmetic-panic smoke test to assert the exact mstore(4, 17) / mstore(4, 18) panic-code stores.
  • No new axioms or theorems; refresh artifacts unchanged.

Notes

Verification

  • lake build Verity Contracts Compiler PrintAxioms → Build completed successfully
  • scripts/refresh_verification_artifacts.sh[refresh] PASS
  • make check → All checks passed (607 tests)

Note

Low Risk
Refactor-only codegen with strengthened compile-to-Yul assertions; emitted panic shape is unchanged.

Overview
Extracts Solidity Panic(uint256) revert emission into a reusable solidityPanicPayload builder in DynamicData.lean; panicErrorHelper now wraps that list in a Yul function definition instead of inlining the same mstore / revert(0, 36) sequence.

The arithmetic-panic compile smoke test now also checks that panic helpers store codes 17 and 18 at word offset 4 (mstore(4, 17) / mstore(4, 18)), alongside the existing selector and revert(0, 36) assertions. Intended as a behavior-preserving refactor for reuse (e.g. downstream panic module work).

Reviewed by Cursor Bugbot for commit 17cba05. Bugbot is set up for automated code reviews on this repo. Configure here.

#1999)

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.
@vercel

vercel Bot commented Jun 13, 2026

Copy link
Copy Markdown

The latest updates on your projects. Learn more about Vercel for GitHub.

Project Deployment Actions Updated (UTC)
verity Building Building Preview, Comment Jun 13, 2026 12:57pm

Request Review

@Th0rgal Th0rgal merged commit 3b28770 into task/1993a-checked-arith Jun 18, 2026
21 checks passed
Th0rgal added a commit that referenced this pull request Jun 19, 2026
* Support dynamic internal helper args

* feat: allow runtime scalar custom error args

* feat: add source-shaped dynamic event proof surface

* Emit checked arithmetic helpers

* feat(Codegen): factor solidityPanicPayload for Panic(uint256) emission (#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.

* feat: self-delegate multicall helper (#1997) (#2029)

* feat: add self-delegate multicall helper

* fix(verity): multicall offset-wrap bound check + documented trusted ECM (#2029)

* fix(merge): drop duplicate internal-call helpers from Compile.lean

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.

* fix(proofs): set noCheckedArithmetic on scalarEventSmoke supported spec

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.

* fix(merge): restore CompilationModelFeatureTest content dropped by botched 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant