Skip to content

Commit b699e30

Browse files
Th0rgalgithub-actions[bot]
Th0rgal
and
github-actions[bot]
authored
Add typed router ABI surface support (#1933)
* Add typed router ABI surface support * chore: auto-refresh derived artifacts * Fix structMembers typed destructuring --------- Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com>
1 parent 92e26a7 commit b699e30

32 files changed

Lines changed: 655 additions & 215 deletions

‎Compiler/ABI.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ private def abiTypeString : ParamType → String
1414
| .uint256 => "uint256"
1515
| .int256 => "int256"
1616
| .uint8 => "uint8"
17+
| .uint16 => "uint16"
1718
| .address => "address"
1819
| .bool => "bool"
1920
| .bytes32 => "bytes32"

‎Compiler/CompilationModel/AbiEncoding.lean‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@ def encodeStaticCustomErrorArg (errorName : String) (ty : ParamType) (argExpr :
1717
pure argExpr
1818
| ParamType.uint8 =>
1919
pure (YulExpr.call "and" [argExpr, YulExpr.lit 255])
20+
| ParamType.uint16 =>
21+
pure (YulExpr.call "and" [argExpr, YulExpr.lit 65535])
2022
| ParamType.address =>
2123
pure (YulExpr.call "and" [argExpr, YulExpr.hex addressMask])
2224
| ParamType.bool =>
@@ -37,7 +39,7 @@ partial def compileUnindexedAbiEncode
3739
(srcBase dstBase : YulExpr) (stem : String) :
3840
Except String (List YulStmt × YulExpr) := do
3941
match ty with
40-
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
42+
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.uint16 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
4143
let loaded := dynamicWordLoad dynamicSource srcBase
4244
pure ([
4345
YulStmt.expr (YulExpr.call "mstore" [dstBase, normalizeEventWord ty loaded])
@@ -298,7 +300,7 @@ def revertWithCustomError (dynamicSource : DynamicDataSource)
298300
let argsWithHeadOffsets := attachOffsets argsWithSources 4
299301
let argStores ← argsWithHeadOffsets.zipIdx.mapM fun ((ty, srcExpr, argExpr, headOffset), idx) => do
300302
match ty with
301-
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
303+
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.uint16 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
302304
let encoded ← encodeStaticCustomErrorArg errorDef.name ty argExpr
303305
pure [YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit headOffset, encoded])]
304306
| ParamType.adt _ maxFields =>

‎Compiler/CompilationModel/AbiHelpers.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,7 @@ mutual
4747
| ParamType.uint256 => "uint256"
4848
| ParamType.int256 => "int256"
4949
| ParamType.uint8 => "uint8"
50+
| ParamType.uint16 => "uint16"
5051
| ParamType.address => "address"
5152
| ParamType.bool => "bool"
5253
| ParamType.bytes32 => "bytes32"

‎Compiler/CompilationModel/AbiTypeLayout.lean‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ mutual
99
| ParamType.uint256 => false
1010
| ParamType.int256 => false
1111
| ParamType.uint8 => false
12+
| ParamType.uint16 => false
1213
| ParamType.address => false
1314
| ParamType.bool => false
1415
| ParamType.bytes32 => false
@@ -35,6 +36,7 @@ mutual
3536
| ParamType.uint256 => 32
3637
| ParamType.int256 => 32
3738
| ParamType.uint8 => 32
39+
| ParamType.uint16 => 32
3840
| ParamType.address => 32
3941
| ParamType.bool => 32
4042
| ParamType.bytes32 => 32
@@ -69,14 +71,14 @@ mutual
6971
| ParamType.fixedArray elemTy n =>
7072
if isDynamicParamType (ParamType.fixedArray elemTy n) then 1 else n * paramParentHeadWords elemTy
7173
| ParamType.newtypeOf _ baseType => paramParentHeadWords baseType
72-
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.address
74+
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.uint16 | ParamType.address
7375
| ParamType.bool | ParamType.bytes32 => 1
7476
| ParamType.adt _ maxFields => 1 + maxFields
7577

7678
/-- Number of 32-byte words in the local head of an ABI value once its dynamic
7779
tail has been entered. Dynamic children occupy one offset word in that head. -/
7880
partial def paramLocalHeadWords : ParamType → Nat
79-
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.address
81+
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.uint16 | ParamType.address
8082
| ParamType.bool | ParamType.bytes32 | ParamType.string | ParamType.bytes
8183
| ParamType.array _ => 1
8284
| ParamType.fixedArray elemTy n => n * paramParentHeadWords elemTy

‎Compiler/CompilationModel/EventAbiHelpers.lean‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ def indexedDynamicArrayElemSupported (elemTy : ParamType) : Bool :=
1616
def normalizeEventWord (ty : ParamType) (expr : YulExpr) : YulExpr :=
1717
match ty with
1818
| ParamType.uint8 => YulExpr.call "and" [expr, YulExpr.lit 255]
19+
| ParamType.uint16 => YulExpr.call "and" [expr, YulExpr.lit 65535]
1920
| ParamType.address => YulExpr.call "and" [expr, YulExpr.hex addressMask]
2021
| ParamType.bool => yulToBool expr
2122
| ParamType.newtypeOf _ baseType => normalizeEventWord baseType expr
@@ -24,7 +25,7 @@ def normalizeEventWord (ty : ParamType) (expr : YulExpr) : YulExpr :=
2425
partial def staticCompositeLeaves (baseName : String) (ty : ParamType) :
2526
List (ParamType × YulExpr) :=
2627
match ty with
27-
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
28+
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.uint16 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
2829
[(ty, YulExpr.ident baseName)]
2930
| ParamType.fixedArray elemTy n =>
3031
(List.range n).flatMap fun i =>
@@ -41,7 +42,7 @@ partial def staticCompositeLeaves (baseName : String) (ty : ParamType) :
4142
partial def staticCompositeLeafTypeOffsets
4243
(baseOffset : Nat) (ty : ParamType) : List (Nat × ParamType) :=
4344
match ty with
44-
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
45+
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.uint16 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
4546
[(baseOffset, ty)]
4647
| ParamType.fixedArray elemTy n =>
4748
(List.range n).flatMap fun i =>
@@ -66,7 +67,7 @@ partial def compileIndexedInPlaceEncoding
6667
(srcBase dstBase : YulExpr) (stem : String) :
6768
Except String (List YulStmt × YulExpr) := do
6869
match ty with
69-
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
70+
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.uint16 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
7071
let loaded := dynamicWordLoad dynamicSource srcBase
7172
pure ([
7273
YulStmt.expr (YulExpr.call "mstore" [dstBase, normalizeEventWord ty loaded])

‎Compiler/CompilationModel/EventEmission.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,7 @@ def eventDynamicArraySource?
8181

8282
def eventParamScalarCompileSupported (ty : ParamType) : Bool :=
8383
match ty with
84-
| .uint256 | .int256 | .uint8 | .address | .bool | .bytes32 => true
84+
| .uint256 | .int256 | .uint8 | .uint16 | .address | .bool | .bytes32 => true
8585
| .string | .tuple _ | .array _ | .fixedArray _ _ | .bytes => false
8686
| .adt _ _ => false
8787
| .newtypeOf _ baseType => eventParamScalarCompileSupported baseType

‎Compiler/CompilationModel/LayoutCompatibilityReport.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ private def jsonOption (render : α → String) : Option α → String
1919
private def mappingKeyTypeString : MappingKeyType → String
2020
| .address => "address"
2121
| .uint256 => "uint256"
22+
| .bytes32 => "bytes32"
2223

2324
private def mappingKeyChainString (keys : List MappingKeyType) : String :=
2425
String.intercalate "=>" (keys.map mappingKeyTypeString)

‎Compiler/CompilationModel/LayoutReport.lean‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,14 @@ private def jsonOption (render : α → String) : Option α → String
1717
private def mappingKeyTypeString : MappingKeyType → String
1818
| .address => "address"
1919
| .uint256 => "uint256"
20+
| .bytes32 => "bytes32"
21+
22+
private def structMemberTypeString : StructMemberType → String
23+
| .uint256 => "uint256"
24+
| .uint16 => "uint16"
25+
| .address => "address"
26+
| .bool => "bool"
27+
| .bytes32 => "bytes32"
2028

2129
private def mappingKeysJson (keys : List MappingKeyType) : String :=
2230
jsonArray (keys.map (fun keyType => jsonString (mappingKeyTypeString keyType)))
@@ -30,6 +38,7 @@ private def packedBitsJson (packed : PackedBits) : String :=
3038
private def structMemberJson (member : StructMember) : String :=
3139
jsonObject [
3240
("name", jsonString member.name),
41+
("type", jsonString (structMemberTypeString member.ty)),
3342
("wordOffset", jsonNat member.wordOffset),
3443
("packedBits", jsonOption packedBitsJson member.packed)
3544
]

‎Compiler/CompilationModel/ParamLoading.lean‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ open Compiler
1212
open Compiler.Yul
1313

1414
def isScalarParamType : ParamType → Bool
15-
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.address | ParamType.bool | ParamType.bytes32 => true
15+
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.uint16 | ParamType.address | ParamType.bool | ParamType.bytes32 => true
1616
| _ => false
1717

1818
private def dynamicArrayElementStrideWords (elemTy : ParamType) : Nat :=
@@ -108,6 +108,8 @@ def genScalarLoad
108108
[YulStmt.let_ name load]
109109
| ParamType.uint8 =>
110110
[YulStmt.let_ name (YulExpr.call "and" [load, YulExpr.lit 255])]
111+
| ParamType.uint16 =>
112+
[YulStmt.let_ name (YulExpr.call "and" [load, YulExpr.lit 65535])]
111113
| ParamType.bytes32 =>
112114
[YulStmt.let_ name load]
113115
| ParamType.address =>
@@ -123,7 +125,7 @@ def genStaticTypeLoads
123125
(loadWord : YulExpr → YulExpr) (name : String) (ty : ParamType) (offset : Nat) :
124126
List YulStmt :=
125127
match ty with
126-
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
128+
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.uint16 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
127129
genScalarLoad loadWord name ty offset
128130
| ParamType.fixedArray elemTy n =>
129131
(List.range n).flatMap fun i =>
@@ -147,7 +149,7 @@ def genSingleParamLoad
147149
(headSize : Nat) (baseOffset : Nat) (name : String) (ty : ParamType) (headOffset : Nat) :
148150
List YulStmt :=
149151
match ty with
150-
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
152+
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.uint16 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
151153
genScalarLoad loadWord name ty headOffset
152154
| ParamType.tuple elemTypes =>
153155
if isDynamicParamType ty then
@@ -223,7 +225,7 @@ private def constructorArgAliases (params : List Param) : List YulStmt :=
223225
YulExpr.ident s!"{param.name}_offset"
224226
else
225227
match param.ty with
226-
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
228+
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.uint16 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
227229
YulExpr.ident param.name
228230
| _ =>
229231
YulExpr.call "mload" [YulExpr.lit headOffset]

‎Compiler/CompilationModel/ScopeValidation.lean‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ def findParamType (params : List Param) (name : String) : Option ParamType :=
1313

1414
partial def staticParamBindingNames (name : String) (ty : ParamType) : List String :=
1515
match ty with
16-
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
16+
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.uint16 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
1717
[name]
1818
| ParamType.fixedArray elemTy n =>
1919
(List.range n).flatMap (fun i => staticParamBindingNames s!"{name}_{i}" elemTy)
@@ -38,6 +38,7 @@ mutual
3838
| ParamType.uint256 => false
3939
| ParamType.int256 => false
4040
| ParamType.uint8 => false
41+
| ParamType.uint16 => false
4142
| ParamType.address => false
4243
| ParamType.bool => false
4344
| ParamType.bytes32 => false
@@ -59,7 +60,7 @@ decreasing_by all_goals simp_wf; all_goals omega
5960
end
6061

6162
def isScalarParamTypeForScope : ParamType → Bool
62-
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.address | ParamType.bool | ParamType.bytes32 => true
63+
| ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.uint16 | ParamType.address | ParamType.bool | ParamType.bytes32 => true
6364
| _ => false
6465

6566
def paramBindingNames (param : Param) : List String :=

0 commit comments

Comments
 (0)