-
Notifications
You must be signed in to change notification settings - Fork 17
Expand file tree
/
Copy pathExpressionCompile.lean
More file actions
754 lines (732 loc) · 44.4 KB
/
Copy pathExpressionCompile.lean
File metadata and controls
754 lines (732 loc) · 44.4 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
import Compiler.CompilationModel.Types
import Compiler.CompilationModel.AdtStorageLayout
import Compiler.CompilationModel.DynamicData
import Compiler.CompilationModel.InternalArgs
import Compiler.CompilationModel.InternalNaming
import Compiler.CompilationModel.ValidationHelpers
namespace Compiler.CompilationModel
open Compiler
open Compiler.Yul
-- Helpers for building common Yul patterns (defined outside mutual block for termination).
-- Exposed (non-private) so that bridge/closure proofs in `Compiler.Proofs.*` can
-- reference their definitional shape via `simp`/`unfold`.
def yulBinOp (op : String) (a b : YulExpr) : YulExpr :=
YulExpr.call op [a, b]
def yulNegatedBinOp (op : String) (a b : YulExpr) : YulExpr :=
YulExpr.call "iszero" [YulExpr.call op [a, b]]
def yulToBool (e : YulExpr) : YulExpr :=
YulExpr.call "iszero" [YulExpr.call "iszero" [e]]
-- Exposed so proof modules can name the exact mapping-read lowering shape.
def compileMappingSlotRead (fields : List Field) (field : String) (keyExpr : YulExpr)
(label : String) (wordOffset : Nat := 0) : Except String YulExpr :=
if !isMapping fields field then
throw s!"Compilation error: field '{field}' is not a mapping"
else
match findFieldWithResolvedSlot fields field with
| some (f, slot) =>
let mappingBase := YulExpr.call "mappingSlot" [YulExpr.lit slot, keyExpr]
let finalSlot := if wordOffset == 0 then mappingBase else YulExpr.call "add" [mappingBase, YulExpr.lit wordOffset]
let loadBuiltin := if f.isTransient then "tload" else "sload"
pure (YulExpr.call loadBuiltin [finalSlot])
| none => throw s!"Compilation error: unknown mapping field '{field}' in {label}"
-- Exposed so proof modules can name the exact nested mapping-chain lowering shape.
def compileMappingSlotChain (baseSlot : YulExpr) (keys : List YulExpr) : YulExpr :=
keys.foldl (fun slotExpr keyExpr => YulExpr.call "mappingSlot" [slotExpr, keyExpr]) baseSlot
def findInternalFunctionForCall? (functions : List FunctionSpec) (name : String) : Option FunctionSpec :=
match functions.filter (fun fn => fn.isInternal && fn.name == name) with
| [fn] => some fn
| _ => none
-- Compile expression to Yul (using mutual recursion for lists)
set_option maxHeartbeats 800000 in
mutual
def compileExprListWithInternals (fields : List Field)
(dynamicSource : DynamicDataSource := .calldata)
(internalFunctions : List FunctionSpec := []) :
List Expr → Except String (List YulExpr)
| [] => pure []
| e :: es => do
let head ← compileExprWithInternals fields dynamicSource internalFunctions e
let tail ← compileExprListWithInternals fields dynamicSource internalFunctions es
pure (head :: tail)
def compileInternalCallArg (fields : List Field) (dynamicSource : DynamicDataSource)
(internalFunctions : List FunctionSpec) (calleeName : String) (param : Param) (arg : Expr) :
Except String (List YulExpr) := do
if isExpandedInternalParamType param.ty then
match directForwardedInternalArgName? arg with
| some name =>
pure ((internalCallYulArgNamesForParam name param).map YulExpr.ident)
| none =>
throw s!"Compilation error: internal call '{calleeName}' argument for parameter '{param.name}' with type {repr param.ty} must be a direct parameter forwarding expression (issue #1889)."
else
pure [← compileExprWithInternals fields dynamicSource internalFunctions arg]
def compileInternalCallArgsWithParams (fields : List Field) (dynamicSource : DynamicDataSource)
(internalFunctions : List FunctionSpec) (calleeName : String) : List Param → List Expr →
Except String (List YulExpr)
| [], [] => pure []
| param :: params, arg :: args => do
let head ← compileInternalCallArg fields dynamicSource internalFunctions calleeName param arg
let tail ← compileInternalCallArgsWithParams fields dynamicSource internalFunctions calleeName params args
pure (head ++ tail)
| params, args =>
throw s!"Compilation error: internal call '{calleeName}' received {args.length} source arg(s), expected {params.length} (issue #1889)."
def compileExpandedInternalCallArgsWithParams
(fields : List Field) (dynamicSource : DynamicDataSource)
(internalFunctions : List FunctionSpec) (calleeName : String) : List Param → List Expr →
Except String (List YulExpr)
| [], [] => pure []
| param :: params, args => do
let expectedNames := internalFunctionYulParamNames [param]
let head := args.take expectedNames.length
let tail := args.drop expectedNames.length
let compileForwardedIndex : Expr → Except String YulExpr
| Expr.param name => pure (YulExpr.ident name)
| Expr.localVar name => pure (YulExpr.ident name)
| Expr.literal n => pure (YulExpr.lit (n % uint256Modulus))
| _ =>
throw s!"Compilation error: internal call '{calleeName}' checked dynamic-member projection uses an unsupported computed index (issue #1889)."
let dynamicMemberHelperNames
(lengthCalldata lengthMemory offsetCalldata offsetMemory : String)
(isLength : Bool) : String :=
match dynamicSource with
| .calldata => if isLength then lengthCalldata else offsetCalldata
| .memory => if isLength then lengthMemory else offsetMemory
let compileProjection : Expr → Except String YulExpr
| Expr.paramDynamicMemberDataOffset name wordOffset =>
pure (YulExpr.call
(dynamicMemberHelperNames
checkedParamDynamicMemberLengthCalldataHelperName
checkedParamDynamicMemberLengthMemoryHelperName
checkedParamDynamicMemberDataOffsetCalldataHelperName
checkedParamDynamicMemberDataOffsetMemoryHelperName
false)
[YulExpr.ident s!"{name}_data_offset", YulExpr.lit wordOffset])
| Expr.paramDynamicMemberLength name wordOffset =>
pure (YulExpr.call
(dynamicMemberHelperNames
checkedParamDynamicMemberLengthCalldataHelperName
checkedParamDynamicMemberLengthMemoryHelperName
checkedParamDynamicMemberDataOffsetCalldataHelperName
checkedParamDynamicMemberDataOffsetMemoryHelperName
true)
[YulExpr.ident s!"{name}_data_offset", YulExpr.lit wordOffset])
| Expr.arrayElementDynamicMemberDataOffset name index wordOffset => do
let indexExpr ← compileForwardedIndex index
pure (YulExpr.call
(dynamicMemberHelperNames
checkedArrayElementDynamicMemberLengthCalldataHelperName
checkedArrayElementDynamicMemberLengthMemoryHelperName
checkedArrayElementDynamicMemberDataOffsetCalldataHelperName
checkedArrayElementDynamicMemberDataOffsetMemoryHelperName
false)
[YulExpr.ident s!"{name}_data_offset", YulExpr.ident s!"{name}_length", indexExpr, YulExpr.lit wordOffset])
| Expr.arrayElementDynamicMemberLength name index wordOffset => do
let indexExpr ← compileForwardedIndex index
pure (YulExpr.call
(dynamicMemberHelperNames
checkedArrayElementDynamicMemberLengthCalldataHelperName
checkedArrayElementDynamicMemberLengthMemoryHelperName
checkedArrayElementDynamicMemberDataOffsetCalldataHelperName
checkedArrayElementDynamicMemberDataOffsetMemoryHelperName
true)
[YulExpr.ident s!"{name}_data_offset", YulExpr.ident s!"{name}_length", indexExpr, YulExpr.lit wordOffset])
| _ =>
throw s!"Compilation error: internal call '{calleeName}' expanded arguments must be direct parameters or checked dynamic-member projections (issue #1889)."
let rec compileExpanded : List Expr → Except String (List YulExpr)
| [] => pure []
| Expr.param argName :: rest => do
let compiledRest ← compileExpanded rest
pure (YulExpr.ident argName :: compiledRest)
| e@(Expr.paramDynamicMemberDataOffset _ _) :: rest
| e@(Expr.paramDynamicMemberLength _ _) :: rest
| e@(Expr.arrayElementDynamicMemberDataOffset _ _ _) :: rest
| e@(Expr.arrayElementDynamicMemberLength _ _ _) :: rest => do
let compiledHead ← compileProjection e
let compiledRest ← compileExpanded rest
pure (compiledHead :: compiledRest)
| _ :: _ =>
throw s!"Compilation error: internal call '{calleeName}' expanded arguments must be direct parameters or checked dynamic-member projections (issue #1889)."
let headExprs ← compileExpanded head
let tailExprs ← compileExpandedInternalCallArgsWithParams fields dynamicSource internalFunctions calleeName params tail
pure (headExprs ++ tailExprs)
| [], _ :: _ =>
throw s!"Compilation error: internal call '{calleeName}' received extra expanded argument(s) (issue #1889)."
def compileInternalCallArgs (fields : List Field) (dynamicSource : DynamicDataSource)
(internalFunctions : List FunctionSpec) (calleeName : String) (args : List Expr) :
Except String (List YulExpr) :=
match findInternalFunctionForCall? internalFunctions calleeName with
| some callee =>
let expandedArgCount :=
callee.params.foldl (fun acc param => acc + (internalFunctionYulParamNames [param]).length) 0
if args.length == callee.params.length then
compileInternalCallArgsWithParams fields dynamicSource internalFunctions calleeName callee.params args
else if args.length == expandedArgCount then
compileExpandedInternalCallArgsWithParams fields dynamicSource internalFunctions calleeName callee.params args
else
compileInternalCallArgsWithParams fields dynamicSource internalFunctions calleeName callee.params args
| none => compileExprListWithInternals fields dynamicSource internalFunctions args
def compileExprWithInternals (fields : List Field)
(dynamicSource : DynamicDataSource := .calldata)
(internalFunctions : List FunctionSpec := []) :
Expr → Except String YulExpr
| Expr.literal n => pure (YulExpr.lit (n % uint256Modulus))
| Expr.param name => pure (YulExpr.ident name)
| Expr.constructorArg idx => pure (YulExpr.ident s!"arg{idx}")
| Expr.immutable name => pure (YulExpr.call "loadimmutable" [YulExpr.str name])
| Expr.storage field =>
if isMapping fields field then
throw s!"Compilation error: field '{field}' is a mapping; use Expr.mapping, Expr.mappingWord, or Expr.mappingPackedWord"
else
match findFieldWithResolvedSlot fields field with
| some (f, slot) =>
let loadBuiltin := if f.isTransient then "tload" else "sload"
match f.packedBits with
| none =>
pure (YulExpr.call loadBuiltin [YulExpr.lit slot])
| some packed =>
pure (YulExpr.call "and" [
YulExpr.call "shr" [YulExpr.lit packed.offset, YulExpr.call loadBuiltin [YulExpr.lit slot]],
YulExpr.lit (packedMaskNat packed)
])
| none => throw s!"Compilation error: unknown storage field '{field}'"
| Expr.storageAddr field =>
if isMapping fields field then
throw s!"Compilation error: field '{field}' is a mapping; use Expr.mapping, Expr.mappingWord, or Expr.mappingPackedWord"
else
match findFieldWithResolvedSlot fields field with
| some (f, slot) =>
let loadBuiltin := if f.isTransient then "tload" else "sload"
match f.ty with
| .address =>
match f.packedBits with
| none =>
pure (YulExpr.call loadBuiltin [YulExpr.lit slot])
| some packed =>
pure (YulExpr.call "and" [
YulExpr.call "shr" [YulExpr.lit packed.offset, YulExpr.call loadBuiltin [YulExpr.lit slot]],
YulExpr.lit (packedMaskNat packed)
])
| _ =>
throw s!"Compilation error: field '{field}' is not address-typed; use Expr.storage instead"
| none => throw s!"Compilation error: unknown storage field '{field}'"
| Expr.mapping field key => do
compileMappingSlotRead fields field (← compileExprWithInternals fields dynamicSource internalFunctions key) "mapping"
| Expr.mappingWord field key wordOffset => do
compileMappingSlotRead fields field (← compileExprWithInternals fields dynamicSource internalFunctions key) "mappingWord" wordOffset
| Expr.mappingPackedWord field key wordOffset packed => do
if !packedBitsValid packed then
throw s!"Compilation error: Expr.mappingPackedWord for field '{field}' has invalid packed range offset={packed.offset} width={packed.width}. Require 0 < width <= 256, offset < 256, and offset + width <= 256."
else do
let slotWord ← compileMappingSlotRead fields field (← compileExprWithInternals fields dynamicSource internalFunctions key) "mappingPackedWord" wordOffset
pure (YulExpr.call "and" [
YulExpr.call "shr" [YulExpr.lit packed.offset, slotWord],
YulExpr.lit (packedMaskNat packed)
])
| Expr.mapping2 field key1 key2 =>
if !isMapping2 fields field then
throw s!"Compilation error: field '{field}' is not a double mapping"
else
match findFieldWithResolvedSlot fields field with
| some (f, slot) => do
let loadBuiltin := if f.isTransient then "tload" else "sload"
let key1Expr ← compileExprWithInternals fields dynamicSource internalFunctions key1
let key2Expr ← compileExprWithInternals fields dynamicSource internalFunctions key2
let innerSlot := YulExpr.call "mappingSlot" [YulExpr.lit slot, key1Expr]
pure (YulExpr.call loadBuiltin [YulExpr.call "mappingSlot" [innerSlot, key2Expr]])
| none => throw s!"Compilation error: unknown mapping field '{field}'"
| Expr.mapping2Word field key1 key2 wordOffset =>
if !isMapping2 fields field then
throw s!"Compilation error: field '{field}' is not a double mapping"
else
match findFieldWithResolvedSlot fields field with
| some (f, slot) => do
let loadBuiltin := if f.isTransient then "tload" else "sload"
let key1Expr ← compileExprWithInternals fields dynamicSource internalFunctions key1
let key2Expr ← compileExprWithInternals fields dynamicSource internalFunctions key2
let innerSlot := YulExpr.call "mappingSlot" [YulExpr.lit slot, key1Expr]
let outerSlot := YulExpr.call "mappingSlot" [innerSlot, key2Expr]
let finalSlot := if wordOffset == 0 then outerSlot else YulExpr.call "add" [outerSlot, YulExpr.lit wordOffset]
pure (YulExpr.call loadBuiltin [finalSlot])
| none => throw s!"Compilation error: unknown mapping field '{field}'"
| Expr.mappingUint field key => do
compileMappingSlotRead fields field (← compileExprWithInternals fields dynamicSource internalFunctions key) "mappingUint"
| Expr.mappingChain field keys =>
if !isMapping fields field then
throw s!"Compilation error: field '{field}' is not a mapping"
else
match findFieldWithResolvedSlot fields field with
| some (f, slot) => do
let keyExprs ← compileExprListWithInternals fields dynamicSource internalFunctions keys
let loadBuiltin := if f.isTransient then "tload" else "sload"
pure (YulExpr.call loadBuiltin [compileMappingSlotChain (YulExpr.lit slot) keyExprs])
| none => throw s!"Compilation error: unknown mapping field '{field}'"
| Expr.structMember field key memberName => do
if isMapping2 fields field then
throw s!"Compilation error: field '{field}' is a double mapping; use Expr.structMember2 instead of Expr.structMember"
match findStructMembers fields field with
| none => throw s!"Compilation error: field '{field}' is not a mappingStruct"
| some members =>
match findStructMember members memberName with
| none => throw s!"Compilation error: struct field '{field}' has no member '{memberName}'"
| some member =>
match member.packed with
| none =>
compileMappingSlotRead fields field (← compileExprWithInternals fields dynamicSource internalFunctions key) s!"structMember.{memberName}" member.wordOffset
| some packed =>
let slotWord ← compileMappingSlotRead fields field (← compileExprWithInternals fields dynamicSource internalFunctions key) s!"structMember.{memberName}" member.wordOffset
pure (YulExpr.call "and" [
YulExpr.call "shr" [YulExpr.lit packed.offset, slotWord],
YulExpr.lit (packedMaskNat packed)
])
| Expr.structMember2 field key1 key2 memberName =>
if !isMapping2 fields field then
throw s!"Compilation error: field '{field}' is not a double mapping; use Expr.structMember instead of Expr.structMember2"
else
match findStructMembers fields field with
| none => throw s!"Compilation error: field '{field}' is not a mappingStruct"
| some members =>
match findStructMember members memberName with
| none => throw s!"Compilation error: struct field '{field}' has no member '{memberName}'"
| some member =>
match findFieldWithResolvedSlot fields field with
| some (f, slot) => do
let loadBuiltin := if f.isTransient then "tload" else "sload"
let key1Expr ← compileExprWithInternals fields dynamicSource internalFunctions key1
let key2Expr ← compileExprWithInternals fields dynamicSource internalFunctions key2
let innerSlot := YulExpr.call "mappingSlot" [YulExpr.lit slot, key1Expr]
let outerSlot := YulExpr.call "mappingSlot" [innerSlot, key2Expr]
let finalSlot := if member.wordOffset == 0 then outerSlot else YulExpr.call "add" [outerSlot, YulExpr.lit member.wordOffset]
match member.packed with
| none =>
pure (YulExpr.call loadBuiltin [finalSlot])
| some packed =>
pure (YulExpr.call "and" [
YulExpr.call "shr" [YulExpr.lit packed.offset, YulExpr.call loadBuiltin [finalSlot]],
YulExpr.lit (packedMaskNat packed)
])
| none => throw s!"Compilation error: unknown mapping field '{field}'"
| Expr.caller => pure (YulExpr.call "caller" [])
| Expr.contractAddress => pure (YulExpr.call "address" [])
| Expr.txOrigin => pure (YulExpr.call "origin" [])
| Expr.chainid => pure (YulExpr.call "chainid" [])
| Expr.extcodesize addr => do
pure (YulExpr.call "extcodesize" [← compileExprWithInternals fields dynamicSource internalFunctions addr])
| Expr.msgValue => pure (YulExpr.call "callvalue" [])
| Expr.selfBalance => pure (YulExpr.call "selfbalance" [])
| Expr.blockTimestamp => pure (YulExpr.call "timestamp" [])
| Expr.blockNumber => pure (YulExpr.call "number" [])
| Expr.blobbasefee => pure (YulExpr.call "blobbasefee" [])
| Expr.mload offset => do
pure (YulExpr.call "mload" [← compileExprWithInternals fields dynamicSource internalFunctions offset])
| Expr.tload offset => do
pure (YulExpr.call "tload" [← compileExprWithInternals fields dynamicSource internalFunctions offset])
| Expr.keccak256 offset size => do
pure (YulExpr.call "keccak256" [
← compileExprWithInternals fields dynamicSource internalFunctions offset,
← compileExprWithInternals fields dynamicSource internalFunctions size
])
| Expr.call gas target value inOffset inSize outOffset outSize => do
pure (YulExpr.call "call" [
← compileExprWithInternals fields dynamicSource internalFunctions gas,
← compileExprWithInternals fields dynamicSource internalFunctions target,
← compileExprWithInternals fields dynamicSource internalFunctions value,
← compileExprWithInternals fields dynamicSource internalFunctions inOffset,
← compileExprWithInternals fields dynamicSource internalFunctions inSize,
← compileExprWithInternals fields dynamicSource internalFunctions outOffset,
← compileExprWithInternals fields dynamicSource internalFunctions outSize
])
| Expr.staticcall gas target inOffset inSize outOffset outSize => do
pure (YulExpr.call "staticcall" [
← compileExprWithInternals fields dynamicSource internalFunctions gas,
← compileExprWithInternals fields dynamicSource internalFunctions target,
← compileExprWithInternals fields dynamicSource internalFunctions inOffset,
← compileExprWithInternals fields dynamicSource internalFunctions inSize,
← compileExprWithInternals fields dynamicSource internalFunctions outOffset,
← compileExprWithInternals fields dynamicSource internalFunctions outSize
])
| Expr.delegatecall gas target inOffset inSize outOffset outSize => do
pure (YulExpr.call "delegatecall" [
← compileExprWithInternals fields dynamicSource internalFunctions gas,
← compileExprWithInternals fields dynamicSource internalFunctions target,
← compileExprWithInternals fields dynamicSource internalFunctions inOffset,
← compileExprWithInternals fields dynamicSource internalFunctions inSize,
← compileExprWithInternals fields dynamicSource internalFunctions outOffset,
← compileExprWithInternals fields dynamicSource internalFunctions outSize
])
| Expr.calldatasize => pure (YulExpr.call "calldatasize" [])
| Expr.calldataload offset => do
pure (YulExpr.call "calldataload" [← compileExprWithInternals fields dynamicSource internalFunctions offset])
| Expr.returndataSize => pure (YulExpr.call "returndatasize" [])
| Expr.returndataOptionalBoolAt outOffset => do
let outOffsetExpr ← compileExprWithInternals fields dynamicSource internalFunctions outOffset
let rdSize := YulExpr.call "returndatasize" []
pure (YulExpr.call "or" [
YulExpr.call "eq" [rdSize, YulExpr.lit 0],
YulExpr.call "and" [
YulExpr.call "eq" [rdSize, YulExpr.lit 32],
YulExpr.call "eq" [YulExpr.call "mload" [outOffsetExpr], YulExpr.lit 1]
]
])
| Expr.localVar name => pure (YulExpr.ident name)
| Expr.externalCall name args => do
let argExprs ← compileExprListWithInternals fields dynamicSource internalFunctions args
if name == builtinExpName then
match argExprs with
| [base, exponent] => pure (YulExpr.call "exp" [base, exponent])
| _ => throw s!"Compilation error: builtin exp expects 2 args, got {argExprs.length}"
else
pure (YulExpr.call name argExprs)
| Expr.internalCall functionName args => do
let argExprs ← compileInternalCallArgs fields dynamicSource internalFunctions functionName args
pure (YulExpr.call (internalFunctionYulName functionName) argExprs)
| Expr.arrayLength name => pure (YulExpr.ident s!"{name}_length")
| Expr.memoryArrayLength name => pure (YulExpr.ident s!"{name}_length")
| Expr.arrayElement name index => do
let indexExpr ← compileExprWithInternals fields dynamicSource internalFunctions index
let helperName := match dynamicSource with
| .calldata => checkedArrayElementCalldataHelperName
| .memory => checkedArrayElementMemoryHelperName
pure (YulExpr.call helperName [
YulExpr.ident s!"{name}_data_offset",
YulExpr.ident s!"{name}_length",
indexExpr
])
| Expr.memoryArrayElement name index => do
let indexExpr ← compileExprWithInternals fields dynamicSource internalFunctions index
pure (YulExpr.call checkedArrayElementMemoryHelperName [
YulExpr.ident s!"{name}_data_offset",
YulExpr.ident s!"{name}_length",
indexExpr
])
| Expr.arrayElementWord name index elementWords wordOffset => do
if elementWords == 0 then
throw s!"Compilation error: Expr.arrayElementWord '{name}' requires elementWords > 0"
else if wordOffset >= elementWords then
throw s!"Compilation error: Expr.arrayElementWord '{name}' wordOffset {wordOffset} is outside element width {elementWords}"
else
let indexExpr ← compileExprWithInternals fields dynamicSource internalFunctions index
let helperName := match dynamicSource with
| .calldata => checkedArrayElementWordCalldataHelperName
| .memory => checkedArrayElementWordMemoryHelperName
pure (YulExpr.call helperName [
YulExpr.ident s!"{name}_data_offset",
YulExpr.ident s!"{name}_length",
indexExpr,
YulExpr.lit elementWords,
YulExpr.lit wordOffset
])
| Expr.arrayElementDynamicWord name index wordOffset => do
let indexExpr ← compileExprWithInternals fields dynamicSource internalFunctions index
let helperName := match dynamicSource with
| .calldata => checkedArrayElementDynamicWordCalldataHelperName
| .memory => checkedArrayElementDynamicWordMemoryHelperName
pure (YulExpr.call helperName [
YulExpr.ident s!"{name}_data_offset",
YulExpr.ident s!"{name}_length",
indexExpr,
YulExpr.lit wordOffset
])
| Expr.arrayElementDynamicDataOffset name index => do
let indexExpr ← compileExprWithInternals fields dynamicSource internalFunctions index
let helperName := match dynamicSource with
| .calldata => checkedArrayElementDynamicDataOffsetCalldataHelperName
| .memory => checkedArrayElementDynamicDataOffsetMemoryHelperName
pure (YulExpr.call helperName [
YulExpr.ident s!"{name}_data_offset",
YulExpr.ident s!"{name}_length",
indexExpr
])
| Expr.paramDynamicHeadWord name wordOffset => do
let helperName := match dynamicSource with
| .calldata => checkedParamDynamicHeadWordCalldataHelperName
| .memory => checkedParamDynamicHeadWordMemoryHelperName
pure (YulExpr.call helperName [
YulExpr.ident s!"{name}_data_offset",
YulExpr.lit wordOffset
])
| Expr.paramDynamicMemberLength name wordOffset => do
let helperName := match dynamicSource with
| .calldata => checkedParamDynamicMemberLengthCalldataHelperName
| .memory => checkedParamDynamicMemberLengthMemoryHelperName
pure (YulExpr.call helperName [
YulExpr.ident s!"{name}_data_offset",
YulExpr.lit wordOffset
])
| Expr.paramDynamicMemberDataOffset name wordOffset => do
let helperName := match dynamicSource with
| .calldata => checkedParamDynamicMemberDataOffsetCalldataHelperName
| .memory => checkedParamDynamicMemberDataOffsetMemoryHelperName
pure (YulExpr.call helperName [
YulExpr.ident s!"{name}_data_offset",
YulExpr.lit wordOffset
])
| Expr.paramDynamicMemberElement name wordOffset innerIndex => do
let innerIndexExpr ← compileExprWithInternals fields dynamicSource internalFunctions innerIndex
let helperName := match dynamicSource with
| .calldata => checkedParamDynamicMemberElementCalldataHelperName
| .memory => checkedParamDynamicMemberElementMemoryHelperName
pure (YulExpr.call helperName [
YulExpr.ident s!"{name}_data_offset",
YulExpr.lit wordOffset,
innerIndexExpr
])
| Expr.paramDynamicStaticComposite name wordOffset =>
pure (YulExpr.call "add" [
YulExpr.ident s!"{name}_data_offset",
YulExpr.lit (wordOffset * 32)
])
| Expr.arrayElementDynamicMemberLength name index wordOffset => do
let indexExpr ← compileExprWithInternals fields dynamicSource internalFunctions index
let helperName := match dynamicSource with
| .calldata => checkedArrayElementDynamicMemberLengthCalldataHelperName
| .memory => checkedArrayElementDynamicMemberLengthMemoryHelperName
pure (YulExpr.call helperName [
YulExpr.ident s!"{name}_data_offset",
YulExpr.ident s!"{name}_length",
indexExpr,
YulExpr.lit wordOffset
])
| Expr.arrayElementDynamicMemberDataOffset name index wordOffset => do
let indexExpr ← compileExprWithInternals fields dynamicSource internalFunctions index
let helperName := match dynamicSource with
| .calldata => checkedArrayElementDynamicMemberDataOffsetCalldataHelperName
| .memory => checkedArrayElementDynamicMemberDataOffsetMemoryHelperName
pure (YulExpr.call helperName [
YulExpr.ident s!"{name}_data_offset",
YulExpr.ident s!"{name}_length",
indexExpr,
YulExpr.lit wordOffset
])
| Expr.arrayElementDynamicMemberElement name index wordOffset innerIndex => do
let indexExpr ← compileExprWithInternals fields dynamicSource internalFunctions index
let innerIndexExpr ← compileExprWithInternals fields dynamicSource internalFunctions innerIndex
let helperName := match dynamicSource with
| .calldata => checkedArrayElementDynamicMemberElementCalldataHelperName
| .memory => checkedArrayElementDynamicMemberElementMemoryHelperName
pure (YulExpr.call helperName [
YulExpr.ident s!"{name}_data_offset",
YulExpr.ident s!"{name}_length",
indexExpr,
YulExpr.lit wordOffset,
innerIndexExpr
])
| Expr.storageArrayLength field =>
match findFieldWithResolvedSlot fields field with
| some (f, slot) =>
match f.ty with
| .dynamicArray _ =>
pure (YulExpr.call "sload" [YulExpr.lit slot])
| _ =>
throw s!"Compilation error: field '{field}' is not a storage dynamic array; use Expr.storageArrayLength only with FieldType.dynamicArray"
| none =>
throw s!"Compilation error: unknown storage field '{field}'"
| Expr.storageArrayElement field index =>
match findFieldWithResolvedSlot fields field with
| some (f, slot) =>
match f.ty with
| .dynamicArray _ => do
pure (YulExpr.call checkedStorageArrayElementHelperName [
YulExpr.lit slot,
← compileExprWithInternals fields dynamicSource internalFunctions index
])
| _ =>
throw s!"Compilation error: field '{field}' is not a storage dynamic array; use Expr.storageArrayElement only with FieldType.dynamicArray"
| none =>
throw s!"Compilation error: unknown storage field '{field}'"
| Expr.dynamicBytesEq lhsName rhsName =>
let helperName := match dynamicSource with
| .calldata => dynamicBytesEqCalldataHelperName
| .memory => dynamicBytesEqMemoryHelperName
pure (YulExpr.call helperName [
YulExpr.ident s!"{lhsName}_data_offset",
YulExpr.ident s!"{lhsName}_length",
YulExpr.ident s!"{rhsName}_data_offset",
YulExpr.ident s!"{rhsName}_length"
])
| Expr.add a b => return yulBinOp "add" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.sub a b => return yulBinOp "sub" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.mul a b => return yulBinOp "mul" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.div a b => return yulBinOp "div" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.sdiv a b => return yulBinOp "sdiv" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.mod a b => return yulBinOp "mod" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.smod a b => return yulBinOp "smod" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.bitAnd a b => return yulBinOp "and" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.bitOr a b => return yulBinOp "or" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.bitXor a b => return yulBinOp "xor" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.bitNot a => return YulExpr.call "not" [← compileExprWithInternals fields dynamicSource internalFunctions a]
| Expr.shl s v => return yulBinOp "shl" (← compileExprWithInternals fields dynamicSource internalFunctions s) (← compileExprWithInternals fields dynamicSource internalFunctions v)
| Expr.shr s v => return yulBinOp "shr" (← compileExprWithInternals fields dynamicSource internalFunctions s) (← compileExprWithInternals fields dynamicSource internalFunctions v)
| Expr.sar s v => return yulBinOp "sar" (← compileExprWithInternals fields dynamicSource internalFunctions s) (← compileExprWithInternals fields dynamicSource internalFunctions v)
| Expr.byte i v => return yulBinOp "byte" (← compileExprWithInternals fields dynamicSource internalFunctions i) (← compileExprWithInternals fields dynamicSource internalFunctions v)
| Expr.signextend b v =>
return yulBinOp "signextend" (← compileExprWithInternals fields dynamicSource internalFunctions b) (← compileExprWithInternals fields dynamicSource internalFunctions v)
| Expr.intrinsic name lowering _minFork args => do
let argExprs ← compileExprListWithInternals fields dynamicSource internalFunctions args
match lowering with
| .verbatim inArity outArity opcodeHex =>
if outArity != 1 then
throw s!"Compilation error: intrinsic {name} must produce exactly 1 output, got {outArity}"
if args.length != inArity then
throw s!"Compilation error: intrinsic {name} expects {inArity} arg(s), got {args.length}"
pure (YulExpr.call (Verity.Core.Intrinsics.YulLowering.callName lowering)
(YulExpr.verbatimHex opcodeHex :: argExprs))
| .builtin builtinName =>
let some (inArity, outArity) := Verity.Core.Intrinsics.yulBuiltinArity? builtinName
| throw s!"Compilation error: intrinsic {name} targets unknown Yul builtin '{builtinName}'"
if outArity != 1 then
throw s!"Compilation error: intrinsic {name} builtin {builtinName} must produce exactly 1 output, got {outArity}"
if args.length != inArity then
throw s!"Compilation error: intrinsic {name} builtin {builtinName} expects {inArity} arg(s), got {args.length}"
pure (YulExpr.call builtinName argExprs)
| Expr.forkIfAtLeast required _thenExpr _elseExpr =>
throw s!"Compilation error: unresolved fork_if_at_least {required}; compile through compileSpecsWithOptions so the branch can be selected from --target-fork before Yul emission"
| Expr.eq a b => return yulBinOp "eq" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.gt a b => return yulBinOp "gt" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.sgt a b => return yulBinOp "sgt" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.lt a b => return yulBinOp "lt" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.slt a b => return yulBinOp "slt" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.ge a b => return yulNegatedBinOp "lt" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.le a b => return yulNegatedBinOp "gt" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.logicalAnd a b => return yulBinOp "and" (yulToBool (← compileExprWithInternals fields dynamicSource internalFunctions a)) (yulToBool (← compileExprWithInternals fields dynamicSource internalFunctions b))
| Expr.logicalOr a b => return yulBinOp "or" (yulToBool (← compileExprWithInternals fields dynamicSource internalFunctions a)) (yulToBool (← compileExprWithInternals fields dynamicSource internalFunctions b))
| Expr.logicalNot a => return YulExpr.call "iszero" [← compileExprWithInternals fields dynamicSource internalFunctions a]
| Expr.ceilDiv a b => do
let ca ← compileExprWithInternals fields dynamicSource internalFunctions a
let cb ← compileExprWithInternals fields dynamicSource internalFunctions b
-- mul(iszero(iszero(a)), add(div(sub(a, 1), b), 1))
-- When a == 0: iszero(iszero(0)) = 0, so result = 0
-- When a > 0: iszero(iszero(a)) = 1, so result = (a-1)/b + 1
pure (YulExpr.call "mul" [
YulExpr.call "iszero" [YulExpr.call "iszero" [ca]],
YulExpr.call "add" [
YulExpr.call "div" [YulExpr.call "sub" [ca, YulExpr.lit 1], cb],
YulExpr.lit 1
]
])
| Expr.mulDivDown a b c => do
let ca ← compileExprWithInternals fields dynamicSource internalFunctions a
let cb ← compileExprWithInternals fields dynamicSource internalFunctions b
let cc ← compileExprWithInternals fields dynamicSource internalFunctions c
-- div(mul(a, b), c)
pure (YulExpr.call "div" [YulExpr.call "mul" [ca, cb], cc])
| Expr.mulDivUp a b c => do
let ca ← compileExprWithInternals fields dynamicSource internalFunctions a
let cb ← compileExprWithInternals fields dynamicSource internalFunctions b
let cc ← compileExprWithInternals fields dynamicSource internalFunctions c
-- div(add(mul(a, b), sub(c, 1)), c)
pure (YulExpr.call "div" [
YulExpr.call "add" [
YulExpr.call "mul" [ca, cb],
YulExpr.call "sub" [cc, YulExpr.lit 1]
],
cc
])
-- verity#1761: full-precision `a * b / c` using the OpenZeppelin /
-- Solmate `FullMath.mulDiv` algorithm. The intermediate product is
-- handled at 512-bit precision; the helper reverts on zero divisor
-- or when the quotient does not fit in `uint256`.
| Expr.mulDiv512Down a b c => do
let ca ← compileExprWithInternals fields dynamicSource internalFunctions a
let cb ← compileExprWithInternals fields dynamicSource internalFunctions b
let cc ← compileExprWithInternals fields dynamicSource internalFunctions c
pure (YulExpr.call fullMulDivHelperName [ca, cb, cc])
| Expr.mulDiv512Up a b c => do
let ca ← compileExprWithInternals fields dynamicSource internalFunctions a
let cb ← compileExprWithInternals fields dynamicSource internalFunctions b
let cc ← compileExprWithInternals fields dynamicSource internalFunctions c
pure (YulExpr.call fullMulDivUpHelperName [ca, cb, cc])
| Expr.wMulDown a b => do
let ca ← compileExprWithInternals fields dynamicSource internalFunctions a
let cb ← compileExprWithInternals fields dynamicSource internalFunctions b
-- div(mul(a, b), 1000000000000000000)
pure (YulExpr.call "div" [YulExpr.call "mul" [ca, cb], YulExpr.lit 1000000000000000000])
| Expr.wDivUp a b => do
let ca ← compileExprWithInternals fields dynamicSource internalFunctions a
let cb ← compileExprWithInternals fields dynamicSource internalFunctions b
-- div(add(mul(a, 1000000000000000000), sub(b, 1)), b)
pure (YulExpr.call "div" [
YulExpr.call "add" [
YulExpr.call "mul" [ca, YulExpr.lit 1000000000000000000],
YulExpr.call "sub" [cb, YulExpr.lit 1]
],
cb
])
| Expr.min a b => do
let ca ← compileExprWithInternals fields dynamicSource internalFunctions a
let cb ← compileExprWithInternals fields dynamicSource internalFunctions b
-- sub(a, mul(sub(a, b), gt(a, b)))
pure (YulExpr.call "sub" [ca,
YulExpr.call "mul" [
YulExpr.call "sub" [ca, cb],
YulExpr.call "gt" [ca, cb]
]
])
| Expr.max a b => do
let ca ← compileExprWithInternals fields dynamicSource internalFunctions a
let cb ← compileExprWithInternals fields dynamicSource internalFunctions b
-- add(a, mul(sub(b, a), gt(b, a)))
pure (YulExpr.call "add" [ca,
YulExpr.call "mul" [
YulExpr.call "sub" [cb, ca],
YulExpr.call "gt" [cb, ca]
]
])
| Expr.ite cond thenVal elseVal => do
let condExpr ← compileExprWithInternals fields dynamicSource internalFunctions cond
let thenExpr ← compileExprWithInternals fields dynamicSource internalFunctions thenVal
let elseExpr ← compileExprWithInternals fields dynamicSource internalFunctions elseVal
-- Branchless ternary: add(mul(iszero(iszero(cond)), thenVal), mul(iszero(cond), elseVal))
let condBool := YulExpr.call "iszero" [YulExpr.call "iszero" [condExpr]]
let condNeg := YulExpr.call "iszero" [condExpr]
pure (YulExpr.call "add" [
YulExpr.call "mul" [condBool, thenExpr],
YulExpr.call "mul" [condNeg, elseExpr]
])
-- ADT expressions: storage-backed tagged unions (#1727 Steps 5c/5d)
| Expr.adtConstruct adtName variantName _args =>
throw s!"Compilation error: ADT construct '{adtName}.{variantName}' cannot be used in expression position. ADT construction expands to multiple sstores and must be compiled at the statement level."
| Expr.adtTag _adtName storageField =>
-- Tag byte: sload(baseSlot) & 0xFF
match findFieldSlot fields storageField with
| some baseSlot =>
pure (compileAdtTagRead (YulExpr.lit baseSlot))
| none => throw s!"Compilation error: unknown storage field '{storageField}' for ADT tag read"
| Expr.adtField _adtName _variantName _fieldName fieldIndex storageField =>
-- Field read: sload(baseSlot + fieldIndex + 1)
match findFieldSlot fields storageField with
| some baseSlot =>
pure (compileAdtFieldRead (YulExpr.lit baseSlot) fieldIndex)
| none => throw s!"Compilation error: unknown storage field '{storageField}' for ADT field read"
end
def compileExprList (fields : List Field)
(dynamicSource : DynamicDataSource := .calldata) (exprs : List Expr) :
Except String (List YulExpr) :=
compileExprListWithInternals fields dynamicSource [] exprs
def compileExpr (fields : List Field)
(dynamicSource : DynamicDataSource := .calldata) (expr : Expr) :
Except String YulExpr :=
compileExprWithInternals fields dynamicSource [] expr
-- Compile require condition to a "failure" predicate to avoid double-negation.
def compileRequireFailCondWithInternals (fields : List Field)
(dynamicSource : DynamicDataSource := .calldata)
(internalFunctions : List FunctionSpec := []) :
Expr → Except String YulExpr
| Expr.ge a b => return yulBinOp "lt" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| Expr.le a b => return yulBinOp "gt" (← compileExprWithInternals fields dynamicSource internalFunctions a) (← compileExprWithInternals fields dynamicSource internalFunctions b)
| cond => return YulExpr.call "iszero" [← compileExprWithInternals fields dynamicSource internalFunctions cond]
def compileRequireFailCond (fields : List Field)
(dynamicSource : DynamicDataSource := .calldata) (cond : Expr) :
Except String YulExpr :=
compileRequireFailCondWithInternals fields dynamicSource [] cond
theorem compileExprWithInternals_nil_eq
(fields : List Field) (dynamicSource : DynamicDataSource) (expr : Expr) :
compileExprWithInternals fields dynamicSource [] expr =
compileExpr fields dynamicSource expr := rfl
theorem compileExprListWithInternals_nil_eq
(fields : List Field) (dynamicSource : DynamicDataSource) (exprs : List Expr) :
compileExprListWithInternals fields dynamicSource [] exprs =
compileExprList fields dynamicSource exprs := rfl
theorem compileRequireFailCondWithInternals_nil_eq
(fields : List Field) (dynamicSource : DynamicDataSource) (cond : Expr) :
compileRequireFailCondWithInternals fields dynamicSource [] cond =
compileRequireFailCond fields dynamicSource cond := rfl
end Compiler.CompilationModel