Repository navigation
Expand file tree
/
Copy pathSupportedSpec.lean
More file actions
7068 lines (6561 loc) · 340 KB
/
Copy pathSupportedSpec.lean
File metadata and controls
7068 lines (6561 loc) · 340 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
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
import Compiler.Proofs.IRGeneration.SupportedFragment
import Compiler.Proofs.IRGeneration.IRInterpreter
import Compiler.CompilationModel.AbiHelpers
import Compiler.CompilationModel.Dispatch
import Compiler.CompilationModel.UsageAnalysis
import Compiler.CompilationModel.SelectorInteropHelpers
import Compiler.TypedIRCompilerCorrectness
set_option linter.deprecated false
set_option linter.unnecessarySimpa false
set_option linter.unusedSimpArgs false
set_option linter.unusedTactic false
set_option linter.unusedVariables false
namespace Compiler.Proofs.IRGeneration
open Compiler
open Compiler.CompilationModel
/-- ABI parameter types admitted by the first whole-contract Layer 2 fragment.
Only single-head-word scalars are included for the initial generic theorem. -/
def SupportedExternalScalarParamType : ParamType → Prop
| .uint256 | .int256 | .uint8 | .uint16 | .uintN _ | .intN _ | .bytesN _
| .address | .bytes32 | .bool => True
| _ => False
/-- Side condition on a dynamic array's element type: the stride literal the
loader divides the remaining tail by must be representable as an EVM word.
Below `2 ^ 256` the emitted `div` agrees with `Nat` division, so the generated
revert guard and `DynamicPayloadShape.fitsLength` accept exactly the same
lengths; at or above it the emitted `div` would saturate to `0` and the two
would diverge. `dynamicArrayElementStrideWords` is positive, so this also rules
out the EVM's division-by-zero convention. -/
def ExternalArrayStrideFitsWord (elemTy : ParamType) : Prop :=
32 * dynamicArrayElementStrideWords elemTy < Compiler.Constants.evmModulus
/-- ABI parameter types admitted by external dispatch, widened past the
single-head-word scalars to every dynamic parameter whose head contribution is a
single relative tail offset (verity#2085).
None of these is decodable by `decodeSupportedParamWord`: they have no
single-word value. Their head word is a relative tail offset, and the generated
calldata loader binds locals that `DynamicAbi.bindExternalParam` reproduces
semantically. Two shapes occur:
* Length-prefixed (`bytes`, `string`, `T[]`) — the offset points at a length
word, and the loader binds six locals (`_offset`, `_abs_offset`, `_length`,
`_tail_head_end`, `_tail_remaining`, `_data_offset`). `string` is encoded
byte-for-byte like `bytes`, so it reuses the same loader and binder lemmas.
Arrays additionally carry `ExternalArrayStrideFitsWord`.
* Length-word-free composites (a `tuple` with a dynamic member, or a
`fixedArray` of such) — the offset points straight at the composite's own head
area, and the loader binds three locals (`_offset`, `_abs_offset`,
`_data_offset`).
*Statically* sized composites are deliberately excluded: their head is wider
than one word, so they would break `supportedExternalParamType_headSize_eq_32`,
and `bindExternalParam` returns `none` for them anyway. `newtypeOf` is excluded
for a different reason: the emitter erases it to its base type while the binder
does not, so admitting it would relate two different loaders.
Consumers that need an actual scalar head word — the native-backend
static-scalar bridge and the legacy Yul compatibility witnesses — keep requiring
`SupportedExternalScalarParamType`. -/
def SupportedExternalParamType : ParamType → Prop
| .uint256 | .int256 | .uint8 | .uint16 | .uintN _ | .intN _ | .bytesN _
| .address | .bytes32 | .bool | .bytes | .string => True
| .array elemTy => ExternalArrayStrideFitsWord elemTy
| .fixedArray elemTy _ => isDynamicParamType elemTy = true
| .tuple elemTys => isDynamicParamTypeList elemTys = true
| _ => False
theorem SupportedExternalParamType_of_scalar {ty : ParamType}
(hscalar : SupportedExternalScalarParamType ty) :
SupportedExternalParamType ty := by
cases ty <;> simp [SupportedExternalScalarParamType] at hscalar <;>
simp [SupportedExternalParamType]
theorem SupportedExternalParamType_bytes :
SupportedExternalParamType ParamType.bytes := trivial
theorem SupportedExternalParamType_string :
SupportedExternalParamType ParamType.string := trivial
theorem SupportedExternalParamType_array {elemTy : ParamType}
(hstride : ExternalArrayStrideFitsWord elemTy) :
SupportedExternalParamType (ParamType.array elemTy) := hstride
/-- Every single-word element type has stride `1`, so word arrays — `uint256[]`,
`address[]`, `bytes32[]`, … — are admitted unconditionally. -/
theorem SupportedExternalParamType_wordArray {elemTy : ParamType}
(hword : isSingleWordStaticParamType elemTy = true) :
SupportedExternalParamType (ParamType.array elemTy) := by
show ExternalArrayStrideFitsWord elemTy
rw [ExternalArrayStrideFitsWord,
dynamicArrayElementStrideWords_eq_one_of_singleWordStatic hword]
simp [Compiler.Constants.evmModulus]
theorem SupportedExternalParamType_dynamicFixedArray {elemTy : ParamType} {n : Nat}
(hdynamic : isDynamicParamType elemTy = true) :
SupportedExternalParamType (ParamType.fixedArray elemTy n) := hdynamic
theorem SupportedExternalParamType_dynamicTuple {elemTys : List ParamType}
(hdynamic : isDynamicParamTypeList elemTys = true) :
SupportedExternalParamType (ParamType.tuple elemTys) := hdynamic
/-- The widened admission set, as the case split every downstream
calldata-loading execution lemma performs. The composite constructors are named
individually rather than folded into one `isLengthPrefixedDynamicShape = false`
disjunct because `genSingleParamLoad` dispatches on the constructor. -/
theorem supportedExternalParamType_cases {ty : ParamType}
(hsupported : SupportedExternalParamType ty) :
SupportedExternalScalarParamType ty ∨
ty = ParamType.bytes ∨
ty = ParamType.string ∨
(∃ elemTy, ty = ParamType.array elemTy ∧ ExternalArrayStrideFitsWord elemTy) ∨
(∃ elemTy n, ty = ParamType.fixedArray elemTy n ∧ isDynamicParamType elemTy = true) ∨
(∃ elemTys, ty = ParamType.tuple elemTys ∧ isDynamicParamTypeList elemTys = true) := by
cases ty <;> simp [SupportedExternalParamType] at hsupported <;>
simp_all [SupportedExternalScalarParamType]
/-- Widened parameter lists still have 32-byte ABI head words: every admitted
dynamic type contributes exactly one relative tail pointer to the head area. -/
theorem supportedExternalParamType_headSize_eq_32 {ty : ParamType}
(hsupported : SupportedExternalParamType ty) : paramHeadSize ty = 32 := by
cases ty <;> simp [SupportedExternalParamType] at hsupported <;>
simp [paramHeadSize, isDynamicParamType, hsupported]
/-- Return profiles admitted by the first whole-contract Layer 2 fragment.
The initial theorem only targets zero-return or single-head-word-return entrypoints. -/
def SupportedExternalReturnProfile : List ParamType → Prop
| [] => True
| [ty] => SupportedExternalScalarParamType ty
| _ => False
/-- Proof-side scalar-parameter predicate tied to the compiler's actual gating
function `isScalarParamType`. Mirrors the `eventParamScalarProofSupported` /
`eventParamScalarCompileSupported` pattern: instead of duplicating the case
list in the proof layer, the proof-side name delegates to the compile-side
Bool so the two cannot drift apart. The hand-restated `SupportedExternalScalarParamType`
Prop is retained for existing call sites; the agreement theorem
`SupportedExternalParamType_iff_externalParamScalarProofSupported` proves they
denote the same set of types. -/
def externalParamScalarProofSupported (ty : ParamType) : Bool :=
isScalarParamType ty
/-- Compile-driven decision procedure for the widened external-parameter
admission set. The scalar half still delegates to the compiler's
`isScalarParamType`; the dynamic constructors admitted on top of it are named
explicitly, and their side conditions are phrased with the compiler's own
`dynamicArrayElementStrideWords` / `isDynamicParamType`, so any future
compiler-side change to dynamic-parameter routing shows up at the agreement
oracle below rather than drifting silently. -/
def externalParamProofSupported : ParamType → Bool
| ParamType.bytes | ParamType.string => true
| ParamType.array elemTy =>
decide (32 * dynamicArrayElementStrideWords elemTy < Compiler.Constants.evmModulus)
| ParamType.fixedArray elemTy _ => isDynamicParamType elemTy
| ParamType.tuple elemTys => isDynamicParamTypeList elemTys
| ty => isScalarParamType ty
/-- Proof-side scalar-return-profile predicate tied to the compiler's scalar
gating function. Encodes the "zero or one single-word return" envelope of
`SupportedExternalReturnProfile` while delegating the per-type decision to
the compiler's `isScalarParamType`. -/
def externalReturnProfileProofSupported : List ParamType → Bool
| [] => true
| [ty] => isScalarParamType ty
| _ => false
def eventParamScalarProofSupported (ty : ParamType) : Bool :=
eventParamScalarCompileSupported ty
def eventDefScalarProofSupported (eventDef : EventDef) : Bool :=
eventDefScalarCompileSupported eventDef
/-- Proof-side catalog for source-shaped event declarations whose payloads are
handled by the compiler's ABI event encoder. This deliberately lives beside,
not inside, `eventEmissionProofSupported`: the existing semantic bridge still
requires scalar params because it proves exact word-by-word log execution.
All currently represented ABI `ParamType` constructors are source-shaped for
event declarations; per-statement validation still checks the stricter
argument-source requirements for dynamic payload copying/hashing. -/
def eventParamSourceShapeProofSupported (_ty : ParamType) : Bool := true
theorem eventParamSourceShapeProofSupported_of_scalar :
∀ {ty : ParamType},
eventParamScalarProofSupported ty = true →
eventParamSourceShapeProofSupported ty = true
| _ty, _hsupport => rfl
/-- Agreement oracle: the hand-restated `SupportedExternalScalarParamType` Prop holds
iff the compile-driven `externalParamScalarProofSupported` Bool is `true`.
This is the meaning-preservation lemma for the conversion pattern: any future
relaxation/tightening of `isScalarParamType` becomes visible at the proof
boundary, instead of silently drifting from a hand-written enumeration. -/
theorem SupportedExternalParamType_iff_externalParamScalarProofSupported
(ty : ParamType) :
SupportedExternalScalarParamType ty ↔ externalParamScalarProofSupported ty = true := by
cases ty <;>
simp [SupportedExternalScalarParamType, externalParamScalarProofSupported,
isScalarParamType]
/-- Agreement oracle for the widened admission set (verity#2085): the
hand-restated `SupportedExternalParamType` Prop holds iff the compile-driven
`externalParamProofSupported` Bool is `true`. -/
theorem SupportedExternalParamType_iff_externalParamProofSupported
(ty : ParamType) :
SupportedExternalParamType ty ↔ externalParamProofSupported ty = true := by
cases ty <;>
simp [SupportedExternalParamType, externalParamProofSupported, isScalarParamType,
ExternalArrayStrideFitsWord]
/-- Agreement oracle for the return-profile shape. -/
theorem SupportedExternalReturnProfile_iff_externalReturnProfileProofSupported
(returns : List ParamType) :
SupportedExternalReturnProfile returns ↔
externalReturnProfileProofSupported returns = true := by
rcases returns with _ | ⟨ty, tail⟩
· -- []
simp [SupportedExternalReturnProfile, externalReturnProfileProofSupported]
· rcases tail with _ | ⟨ty2, rest⟩
· -- [ty]
simp [SupportedExternalReturnProfile, externalReturnProfileProofSupported,
SupportedExternalParamType_iff_externalParamScalarProofSupported,
externalParamScalarProofSupported]
· -- ty :: ty2 :: rest
simp [SupportedExternalReturnProfile, externalReturnProfileProofSupported]
theorem eventDefScalarProofSupported_params_all
{eventDef : EventDef}
(hsupport : eventDefScalarProofSupported eventDef = true) :
eventDef.params.all (fun param => eventParamScalarProofSupported param.ty) = true := by
have hsplit :
(∀ param ∈ eventDef.params, eventParamScalarProofSupported param.ty = true) ∧
(eventDef.params.filter (fun param => param.kind == EventParamKind.indexed)).length ≤ 3 := by
simpa [eventDefScalarProofSupported, eventDefScalarCompileSupported,
eventParamScalarProofSupported, Bool.and_eq_true] using hsupport
simpa using hsplit.1
theorem eventDefScalarProofSupported_indexed_length_le_three
{eventDef : EventDef}
(hsupport : eventDefScalarProofSupported eventDef = true) :
(eventDef.params.filter (fun param => param.kind == EventParamKind.indexed)).length ≤ 3 := by
have hsplit :
(∀ param ∈ eventDef.params, eventParamScalarProofSupported param.ty = true) ∧
(eventDef.params.filter (fun param => param.kind == EventParamKind.indexed)).length ≤ 3 := by
simpa [eventDefScalarProofSupported, eventDefScalarCompileSupported,
eventParamScalarProofSupported, Bool.and_eq_true] using hsupport
exact hsplit.2
private theorem eventParamScalarProofSupported_eq_true_of_mem_all :
∀ {params : List EventParam} {param : EventParam},
params.all (fun param => eventParamScalarProofSupported param.ty) = true →
param ∈ params →
eventParamScalarProofSupported param.ty = true
| params, param, hall, hmem => by
have hforall :
∀ candidate ∈ params, eventParamScalarProofSupported candidate.ty = true := by
simpa using hall
exact hforall param hmem
theorem eventParamScalarProofSupported_eq_true_of_eventDefScalarProofSupported
{eventDef : EventDef}
{param : EventParam}
(hsupport : eventDefScalarProofSupported eventDef = true)
(hmem : param ∈ eventDef.params) :
eventParamScalarProofSupported param.ty = true :=
eventParamScalarProofSupported_eq_true_of_mem_all
(eventDefScalarProofSupported_params_all hsupport) hmem
theorem eventParamScalarProofSupported_eventIsDynamicType_eq_false :
∀ {ty : ParamType},
eventParamScalarProofSupported ty = true →
eventIsDynamicType ty = false
| ty, hsupport => by
cases ty <;>
simp [eventParamScalarProofSupported, eventParamScalarCompileSupported,
eventIsDynamicType, isDynamicParamType]
at hsupport ⊢
case newtypeOf name baseType =>
have hbase :=
eventParamScalarProofSupported_eventIsDynamicType_eq_false (ty := baseType) hsupport
simpa [eventIsDynamicType] using hbase
theorem eventParamScalarProofSupported_eventHeadWordSize_eq_thirty_two :
∀ {ty : ParamType},
eventParamScalarProofSupported ty = true →
eventHeadWordSize ty = 32
| ty, hsupport => by
cases ty <;>
simp [eventParamScalarProofSupported, eventParamScalarCompileSupported,
eventHeadWordSize, paramHeadSize]
at hsupport ⊢
case newtypeOf name baseType =>
have hbase :=
eventParamScalarProofSupported_eventHeadWordSize_eq_thirty_two (ty := baseType) hsupport
simpa [eventHeadWordSize] using hbase
theorem eventParamScalarProofSupported_ne_bytes
{ty : ParamType}
(hsupport : eventParamScalarProofSupported ty = true) :
ty ≠ ParamType.bytes := by
intro h; subst h; simp [eventParamScalarProofSupported,
eventParamScalarCompileSupported] at hsupport
theorem eventParamScalarProofSupported_ne_string
{ty : ParamType}
(hsupport : eventParamScalarProofSupported ty = true) :
ty ≠ ParamType.string := by
intro h; subst h; simp [eventParamScalarProofSupported,
eventParamScalarCompileSupported] at hsupport
theorem eventParamScalarProofSupported_ne_array
{ty elemTy : ParamType}
(hsupport : eventParamScalarProofSupported ty = true) :
ty ≠ ParamType.array elemTy := by
intro h; subst h; simp [eventParamScalarProofSupported,
eventParamScalarCompileSupported] at hsupport
theorem eventParamScalarProofSupported_ne_fixedArray
{ty elemTy : ParamType}
{len : Nat}
(hsupport : eventParamScalarProofSupported ty = true) :
ty ≠ ParamType.fixedArray elemTy len := by
intro h; subst h; simp [eventParamScalarProofSupported,
eventParamScalarCompileSupported] at hsupport
theorem eventParamScalarProofSupported_ne_tuple
{ty : ParamType}
{members : List ParamType}
(hsupport : eventParamScalarProofSupported ty = true) :
ty ≠ ParamType.tuple members := by
intro h; subst h; simp [eventParamScalarProofSupported,
eventParamScalarCompileSupported] at hsupport
/-- Generous size ceiling on event scratch geometry. The compiled emit block
addresses scratch words with the wrapping `add` builtin, so the semantic
bridge needs every scratch word offset `k * 32` to stay strictly below
`2^256`; bounding the signature byte length and parameter count by `2^32`
keeps all offsets distinct mod `2^256` while admitting every realistic event. -/
def eventScratchSizeLimit : Nat := 2 ^ 32
def eventDefScratchBounded (eventDef : EventDef) : Bool :=
decide ((bytesFromString (eventSignature eventDef)).length ≤ eventScratchSizeLimit) &&
decide (eventDef.params.length ≤ eventScratchSizeLimit)
def eventDefSourceShapeProofSupported (eventDef : EventDef) : Bool :=
eventDef.params.all (fun param => eventParamSourceShapeProofSupported param.ty) &&
decide ((eventDef.params.filter (fun param => param.kind == EventParamKind.indexed)).length ≤ 3) &&
eventDefScratchBounded eventDef
theorem eventDefSourceShapeProofSupported_of_scalar
{eventDef : EventDef}
(hscalar : eventDefScalarProofSupported eventDef = true)
(hscratch : eventDefScratchBounded eventDef = true) :
eventDefSourceShapeProofSupported eventDef = true := by
have hparams :
eventDef.params.all (fun param => eventParamSourceShapeProofSupported param.ty) = true := by
apply List.all_eq_true.mpr
intro param hmem
exact eventParamSourceShapeProofSupported_of_scalar
(eventParamScalarProofSupported_eq_true_of_eventDefScalarProofSupported hscalar hmem)
have hindexed := eventDefScalarProofSupported_indexed_length_le_three hscalar
simp [eventDefSourceShapeProofSupported, hparams, hscratch, hindexed]
private def dynamicTupleEventSmoke : EventDef :=
{ name := "CompositeEvent"
params := [
{ name := "id", ty := .bytes32, kind := .indexed },
{ name := "payload", ty := .tuple [.uint256, .bytes], kind := .unindexed },
{ name := "values", ty := .array .uint256, kind := .unindexed },
{ name := "note", ty := .bytes, kind := .unindexed }
] }
private def staticStructEventSmoke : EventDef :=
{ name := "CreateMarket"
params := [
{ name := "id", ty := .bytes32, kind := .indexed },
{ name := "market"
ty := .tuple [.address, .address, .address, .address, .uint256]
kind := .unindexed }
] }
private def indexedDynamicStructArrayEventSmoke : EventDef :=
{ name := "IndexedDynamicStructArray"
params := [
{ name := "payload"
ty := .array (.tuple [.uint256, .bytes])
kind := .indexed }
] }
private def fixedArrayAndAdtEventSmoke : EventDef :=
{ name := "FixedArrayAndAdt"
params := [
{ name := "fixed", ty := .fixedArray .address 2, kind := .indexed },
{ name := "choice", ty := .adt "Choice" 2, kind := .unindexed }
] }
example : eventDefSourceShapeProofSupported dynamicTupleEventSmoke = true := by
rfl
example : eventDefSourceShapeProofSupported staticStructEventSmoke = true := by
rfl
example :
eventDefSourceShapeProofSupported indexedDynamicStructArrayEventSmoke = true := by
rfl
example : eventDefSourceShapeProofSupported fixedArrayAndAdtEventSmoke = true := by
rfl
/-- Event arguments admitted by the semantic bridge: atomic word-pure
expressions (literals, scope variables, transaction context). The compiled
emit block evaluates argument expressions *after* the signature words have
been stored into scratch memory, while source semantics resolves arguments
*before* the emit takes effect; atomic arguments cannot observe memory (or
the block-local scratch bindings), so the two evaluation points agree. -/
def exprEventArgAtomic : Expr → Bool
| .literal _ | .param _ | .localVar _ | .caller | .contractAddress
| .txOrigin | .msgValue | .blockTimestamp | .blockNumber | .chainid
| .blobbasefee | .calldatasize => true
| .immutable _ => false
| _ => false
def eventEmissionProofSupported
(events : List EventDef) (eventName : String) (args : List Expr) : Bool :=
match events.find? (·.name == eventName) with
| none => false
| some eventDef =>
eventDefScalarProofSupported eventDef &&
decide (args.length = eventDef.params.length) &&
eventDefScratchBounded eventDef &&
args.all exprEventArgAtomic
theorem exists_eventDef_of_eventEmissionProofSupported
{events : List EventDef}
{eventName : String}
{args : List Expr}
(hsupport : eventEmissionProofSupported events eventName args = true) :
∃ eventDef,
events.find? (·.name == eventName) = some eventDef ∧
eventDefScalarProofSupported eventDef = true ∧
args.length = eventDef.params.length := by
unfold eventEmissionProofSupported at hsupport
cases hfind : events.find? (fun x => x.name == eventName) with
| none =>
simp [hfind] at hsupport
| some eventDef =>
simp [hfind, Bool.and_eq_true] at hsupport
exact ⟨eventDef, rfl, hsupport.1.1.1, hsupport.1.1.2⟩
theorem eventDefScratchBounded_of_eventEmissionProofSupported
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef) :
eventDefScratchBounded eventDef = true := by
unfold eventEmissionProofSupported at hsupport
rw [hfind] at hsupport
simp [Bool.and_eq_true] at hsupport
exact hsupport.1.2
theorem args_all_atomic_of_eventEmissionProofSupported
{events : List EventDef}
{eventName : String}
{args : List Expr}
(hsupport : eventEmissionProofSupported events eventName args = true) :
args.all exprEventArgAtomic = true := by
unfold eventEmissionProofSupported at hsupport
cases hfind : events.find? (fun x => x.name == eventName) with
| none => simp [hfind] at hsupport
| some eventDef =>
rw [hfind] at hsupport
simp [Bool.and_eq_true] at hsupport
simpa using hsupport.2
theorem eventEmissionProofSupported_find?_isSome
{events : List EventDef}
{eventName : String}
{args : List Expr}
(hsupport : eventEmissionProofSupported events eventName args = true) :
(events.find? (·.name == eventName)).isSome = true := by
rcases exists_eventDef_of_eventEmissionProofSupported hsupport with
⟨eventDef, hfind, _, _⟩
simp [hfind]
theorem eventDefScalarProofSupported_eq_true_of_eventEmissionProofSupported
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef) :
eventDefScalarProofSupported eventDef = true := by
rcases exists_eventDef_of_eventEmissionProofSupported hsupport with
⟨selected, hselected, hscalar, _⟩
rw [hfind] at hselected
injection hselected with heq
subst heq
exact hscalar
theorem eventParamScalarProofSupported_eq_true_of_eventEmissionProofSupported
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
{param : EventParam}
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef)
(hmem : param ∈ eventDef.params) :
eventParamScalarProofSupported param.ty = true :=
eventParamScalarProofSupported_eq_true_of_eventDefScalarProofSupported
(eventDefScalarProofSupported_eq_true_of_eventEmissionProofSupported hsupport hfind)
hmem
theorem eventEmissionProofSupported_indexed_length_le_three
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef) :
(eventDef.params.filter (fun param => param.kind == EventParamKind.indexed)).length ≤ 3 :=
eventDefScalarProofSupported_indexed_length_le_three
(eventDefScalarProofSupported_eq_true_of_eventEmissionProofSupported hsupport hfind)
theorem eventEmissionProofSupported_args_length
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef) :
args.length = eventDef.params.length := by
rcases exists_eventDef_of_eventEmissionProofSupported hsupport with
⟨selected, hselected, _, hlen⟩
rw [hfind] at hselected
injection hselected with heq
subst heq
exact hlen
theorem eventEmissionProofSupported_param_eventIsDynamicType_eq_false
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
{param : EventParam}
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef)
(hmem : param ∈ eventDef.params) :
eventIsDynamicType param.ty = false :=
eventParamScalarProofSupported_eventIsDynamicType_eq_false
(eventParamScalarProofSupported_eq_true_of_eventEmissionProofSupported
hsupport hfind hmem)
theorem eventEmissionProofSupported_param_eventHeadWordSize_eq_thirty_two
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
{param : EventParam}
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef)
(hmem : param ∈ eventDef.params) :
eventHeadWordSize param.ty = 32 :=
eventParamScalarProofSupported_eventHeadWordSize_eq_thirty_two
(eventParamScalarProofSupported_eq_true_of_eventEmissionProofSupported
hsupport hfind hmem)
theorem eventEmissionProofSupported_param_not_bytes
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
{param : EventParam}
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef)
(hmem : param ∈ eventDef.params) :
param.ty ≠ ParamType.bytes :=
eventParamScalarProofSupported_ne_bytes
(eventParamScalarProofSupported_eq_true_of_eventEmissionProofSupported
hsupport hfind hmem)
theorem eventEmissionProofSupported_param_not_string
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
{param : EventParam}
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef)
(hmem : param ∈ eventDef.params) :
param.ty ≠ ParamType.string :=
eventParamScalarProofSupported_ne_string
(eventParamScalarProofSupported_eq_true_of_eventEmissionProofSupported
hsupport hfind hmem)
theorem eventEmissionProofSupported_zippedWithSource_param_scalar
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
{α : Type}
{compiledArgs : List α}
{entry : EventParam × Expr × α}
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef)
(hmem :
entry ∈
((eventDef.params.zip args).zip compiledArgs |>.map
(fun ((p, srcExpr), argExpr) => (p, srcExpr, argExpr)))) :
eventParamScalarProofSupported entry.1.ty = true := by
rcases entry with ⟨param, srcExpr, argExpr⟩
simp only [List.mem_map] at hmem
rcases hmem with ⟨sourceEntry, hsourceMem, hentry⟩
rcases sourceEntry with ⟨paramArg, compiledArg⟩
rcases paramArg with ⟨sourceParam, sourceExpr⟩
cases hentry
have hparamArgMem : (sourceParam, sourceExpr) ∈ eventDef.params.zip args := by
exact (List.of_mem_zip hsourceMem).1
have hparamMem : sourceParam ∈ eventDef.params := by
exact (List.of_mem_zip hparamArgMem).1
exact eventParamScalarProofSupported_eq_true_of_eventEmissionProofSupported
hsupport hfind hparamMem
theorem eventEmissionProofSupported_zippedWithSource_eventIsDynamicType_eq_false
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
{α : Type}
{compiledArgs : List α}
{entry : EventParam × Expr × α}
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef)
(hmem :
entry ∈
((eventDef.params.zip args).zip compiledArgs |>.map
(fun ((p, srcExpr), argExpr) => (p, srcExpr, argExpr)))) :
eventIsDynamicType entry.1.ty = false :=
eventParamScalarProofSupported_eventIsDynamicType_eq_false
(eventEmissionProofSupported_zippedWithSource_param_scalar
hsupport hfind hmem)
theorem eventEmissionProofSupported_zippedWithSource_eventHeadWordSize_eq_thirty_two
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
{α : Type}
{compiledArgs : List α}
{entry : EventParam × Expr × α}
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef)
(hmem :
entry ∈
((eventDef.params.zip args).zip compiledArgs |>.map
(fun ((p, srcExpr), argExpr) => (p, srcExpr, argExpr)))) :
eventHeadWordSize entry.1.ty = 32 :=
eventParamScalarProofSupported_eventHeadWordSize_eq_thirty_two
(eventEmissionProofSupported_zippedWithSource_param_scalar
hsupport hfind hmem)
theorem eventEmissionProofSupported_zippedWithSource_unindexed_any_dynamic_false
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
{α : Type}
(compiledArgs : List α)
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef) :
((((eventDef.params.zip args).zip compiledArgs |>.map
(fun ((p, srcExpr), argExpr) => (p, srcExpr, argExpr))).filter
(fun (p, _, _) => p.kind == EventParamKind.unindexed)).any
(fun (p, _, _) => eventIsDynamicType p.ty)) = false := by
apply List.any_eq_false.mpr
intro entry hentry
have hstatic :
(match entry with
| (p, _, _) => eventIsDynamicType p.ty) = false :=
eventEmissionProofSupported_zippedWithSource_eventIsDynamicType_eq_false
hsupport hfind (List.mem_filter.mp hentry).1
simp [hstatic]
private theorem foldl_eventHeadWordSize_eq_thirty_two_mul_length
{α : Type}
{entries : List (EventParam × Expr × α)}
(acc : Nat)
(hhead :
∀ entry ∈ entries, eventHeadWordSize entry.1.ty = 32) :
(entries.map (fun entry => eventHeadWordSize entry.1.ty)).foldl (· + ·) acc =
acc + 32 * entries.length := by
induction entries generalizing acc with
| nil =>
simp
| cons entry rest ih =>
have hentry : eventHeadWordSize entry.1.ty = 32 := hhead entry (by simp)
have hrest :
∀ tailEntry ∈ rest, eventHeadWordSize tailEntry.1.ty = 32 := by
intro tailEntry hmem
exact hhead tailEntry (by simp [hmem])
calc
((entry :: rest).map (fun entry => eventHeadWordSize entry.1.ty)).foldl (· + ·) acc
= (rest.map (fun entry => eventHeadWordSize entry.1.ty)).foldl (· + ·)
(acc + 32) := by simp [hentry]
_ = (acc + 32) + 32 * rest.length := ih (acc + 32) hrest
_ = acc + 32 * (entry :: rest).length := by
simp [Nat.mul_succ, Nat.add_comm, Nat.add_assoc]
theorem eventEmissionProofSupported_zippedWithSource_unindexed_head_size
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
{α : Type}
(compiledArgs : List α)
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef) :
let zipped : List (EventParam × Expr × α) :=
(eventDef.params.zip args).zip compiledArgs |>.map
(fun ((p, srcExpr), argExpr) => (p, srcExpr, argExpr))
let unindexed := zipped.filter (fun (p, _, _) => p.kind == EventParamKind.unindexed)
(unindexed.map (fun (p, _, _) => eventHeadWordSize p.ty)).foldl (· + ·) 0 =
32 * unindexed.length := by
dsimp only
simpa using
foldl_eventHeadWordSize_eq_thirty_two_mul_length (α := α) (acc := 0)
(entries :=
(((eventDef.params.zip args).zip compiledArgs |>.map
(fun ((p, srcExpr), argExpr) => (p, srcExpr, argExpr))).filter
(fun (p, _, _) => p.kind == EventParamKind.unindexed)))
(by
intro entry hentry
exact eventEmissionProofSupported_zippedWithSource_eventHeadWordSize_eq_thirty_two
hsupport hfind (List.mem_filter.mp hentry).1)
theorem eventEmissionProofSupported_eventUnindexedHeadSize
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
(compiledArgs : List Compiler.Yul.YulExpr)
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef) :
eventUnindexedHeadSize
(eventUnindexedArgs (eventZippedWithSource eventDef args compiledArgs)) =
32 * (eventUnindexedArgs (eventZippedWithSource eventDef args compiledArgs)).length := by
simpa [eventUnindexedHeadSize, eventUnindexedArgs, eventZippedWithSource] using
eventEmissionProofSupported_zippedWithSource_unindexed_head_size
compiledArgs hsupport hfind
theorem eventEmissionProofSupported_eventHasUnindexedDynamicData_eq_false
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
(compiledArgs : List Compiler.Yul.YulExpr)
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef) :
eventHasUnindexedDynamicData
(eventUnindexedArgs (eventZippedWithSource eventDef args compiledArgs)) = false := by
simpa [eventHasUnindexedDynamicData, eventUnindexedArgs, eventZippedWithSource] using
eventEmissionProofSupported_zippedWithSource_unindexed_any_dynamic_false
compiledArgs hsupport hfind
private theorem eventCompiledArgs_filter_kind_length_le_params_filter_kind
{α : Type}
(params : List EventParam)
(args : List Expr)
(compiledArgs : List α)
(kind : EventParamKind) :
((List.filter
(fun entry : EventParam × Expr × α => entry.1.kind == kind)
(List.map
(fun entry : (EventParam × Expr) × α => (entry.1.1, entry.1.2, entry.2))
((List.zip params args).zip compiledArgs))).length) ≤
(params.filter (fun param => param.kind == kind)).length := by
induction params generalizing args compiledArgs with
| nil =>
simp
| cons param params ih =>
cases args with
| nil =>
simp
| cons arg args =>
cases compiledArgs with
| nil =>
simp
| cons compiledArg compiledArgs =>
by_cases hkind : param.kind == kind
· simp [hkind, ih args compiledArgs]
· have htail := ih args compiledArgs
simp [hkind]
exact htail
theorem eventEmissionProofSupported_zippedWithSource_indexed_length_le_three
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
{α : Type}
(compiledArgs : List α)
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef) :
((List.filter
(fun entry : EventParam × Expr × α => entry.1.kind == EventParamKind.indexed)
(List.map
(fun entry : (EventParam × Expr) × α => (entry.1.1, entry.1.2, entry.2))
((List.zip eventDef.params args).zip compiledArgs))).length) ≤ 3 := by
exact Nat.le_trans
(eventCompiledArgs_filter_kind_length_le_params_filter_kind
eventDef.params args compiledArgs EventParamKind.indexed)
(eventEmissionProofSupported_indexed_length_le_three hsupport hfind)
theorem eventEmissionProofSupported_eventIndexedArgs_length_le_three
{events : List EventDef}
{eventName : String}
{args : List Expr}
{eventDef : EventDef}
(compiledArgs : List Compiler.Yul.YulExpr)
(hsupport : eventEmissionProofSupported events eventName args = true)
(hfind : events.find? (·.name == eventName) = some eventDef) :
(eventIndexedArgs (eventZippedWithSource eventDef args compiledArgs)).length ≤ 3 := by
simpa [eventIndexedArgs, eventZippedWithSource] using
eventEmissionProofSupported_zippedWithSource_indexed_length_le_three
compiledArgs hsupport hfind
theorem eventLogFunction_mem_logBuiltins_of_le_three
{indexedLength : Nat}
(hle : indexedLength ≤ 3) :
eventLogFunction indexedLength ∈ ["log1", "log2", "log3", "log4"] := by
cases indexedLength with
| zero =>
simp [eventLogFunction]
| succ n =>
cases n with
| zero =>
simp [eventLogFunction]
| succ n =>
cases n with
| zero =>
simp [eventLogFunction]
| succ n =>
cases n with
| zero =>
simp [eventLogFunction]
| succ n =>
omega
theorem eventLogArgs_length
(dataSizeExpr : Compiler.Yul.YulExpr)
(indexedTopicParts : List (List Compiler.Yul.YulStmt × Compiler.Yul.YulExpr)) :
(eventLogArgs dataSizeExpr indexedTopicParts).length =
indexedTopicParts.length + 3 := by
simp [eventLogArgs]
mutual
/-- Constructor body proofs are intentionally staged after initcode argument
decoding. Raw constructor calldata observations therefore remain outside the
current body-level support interface until the deploy-wrapper proof exists. -/
def exprTouchesUnsupportedConstructorRawCalldataSurface : Expr → Bool
| .literal _ | .param _ | .immutable _ | .localVar _ | .caller | .contractAddress | .txOrigin
| .chainid | .msgValue | .selfBalance | .baseFee | .gasPrice | .blockTimestamp | .blockNumber
| .blobbasefee | .constructorArg _ | .returndataSize => false
| .calldatasize => true
| .storage _ | .storageAddr _ | .arrayLength _ | .memoryArrayLength _
| .storageArrayLength _ => false
| .logicalNot a | .bitNot a | .mload a | .tload a | .extcodesize a | .returndataOptionalBoolAt a =>
exprTouchesUnsupportedConstructorRawCalldataSurface a
| .calldataload _ =>
true
| .mapping _ a | .mappingWord _ a _ | .mappingPackedWord _ a _ _
| .mappingUint _ a | .structMember _ a _ | .arrayElement _ a
| .memoryArrayElement _ a
| .arrayElementWord _ a _ _
| .arrayElementDynamicWord _ a _
| .arrayElementDynamicDataOffset _ a
| .arrayElementDynamicMemberLength _ a _
| .arrayElementDynamicMemberDataOffset _ a _
| .storageArrayElement _ a =>
exprTouchesUnsupportedConstructorRawCalldataSurface a
| .paramDynamicMemberElement _ _ a =>
exprTouchesUnsupportedConstructorRawCalldataSurface a
| .arrayElementDynamicMemberElement _ a _ b =>
exprTouchesUnsupportedConstructorRawCalldataSurface a ||
exprTouchesUnsupportedConstructorRawCalldataSurface b
| .add a b | .sub a b | .mul a b | .div a b | .mod a b
| .eq a b | .ge a b | .gt a b | .lt a b | .le a b
| .logicalAnd a b | .logicalOr a b | .shl a b | .shr a b
| .bitAnd a b | .bitOr a b | .bitXor a b | .min a b | .max a b
| .wMulDown a b | .wDivUp a b | .ceilDiv a b | .slt a b | .sgt a b
| .sdiv a b | .smod a b | .sar a b | .byte a b | .signextend a b =>
exprTouchesUnsupportedConstructorRawCalldataSurface a ||
exprTouchesUnsupportedConstructorRawCalldataSurface b
| .mapping2 _ a b | .mapping2Word _ a b _ | .structMember2 _ a b _ =>
exprTouchesUnsupportedConstructorRawCalldataSurface a ||
exprTouchesUnsupportedConstructorRawCalldataSurface b
| .dynamicBytesEq _ _ => false
| .ite c t e | .mulDivDown c t e | .mulDivUp c t e
| .mulDiv512Down c t e | .mulDiv512Up c t e =>
exprTouchesUnsupportedConstructorRawCalldataSurface c ||
exprTouchesUnsupportedConstructorRawCalldataSurface t ||
exprTouchesUnsupportedConstructorRawCalldataSurface e
-- `paramDynamicHeadWord` reads the head section of an ABI-decoded
-- parameter; like `param _` it does not touch raw calldata, so the
-- constructor-arg precondition is unaffected.
| .paramDynamicHeadWord _ _ | .paramDynamicStaticComposite _ _
| .paramDynamicMemberLength _ _
| .paramDynamicMemberDataOffset _ _ => false
| .mappingChain _ keys | .internalCall _ keys | .externalCall _ keys =>
exprListTouchesUnsupportedConstructorRawCalldataSurface keys
| .intrinsic _ _ _ _ => true
| .forkIfAtLeast _ thenExpr elseExpr =>
exprTouchesUnsupportedConstructorRawCalldataSurface thenExpr ||
exprTouchesUnsupportedConstructorRawCalldataSurface elseExpr
| .keccak256 a b =>
exprTouchesUnsupportedConstructorRawCalldataSurface a ||
exprTouchesUnsupportedConstructorRawCalldataSurface b
| .call g t v io is oo os =>
exprTouchesUnsupportedConstructorRawCalldataSurface g ||
exprTouchesUnsupportedConstructorRawCalldataSurface t ||
exprTouchesUnsupportedConstructorRawCalldataSurface v ||
exprTouchesUnsupportedConstructorRawCalldataSurface io ||
exprTouchesUnsupportedConstructorRawCalldataSurface is ||
exprTouchesUnsupportedConstructorRawCalldataSurface oo ||
exprTouchesUnsupportedConstructorRawCalldataSurface os
| .staticcall g t io is oo os | .delegatecall g t io is oo os =>
exprTouchesUnsupportedConstructorRawCalldataSurface g ||
exprTouchesUnsupportedConstructorRawCalldataSurface t ||
exprTouchesUnsupportedConstructorRawCalldataSurface io ||
exprTouchesUnsupportedConstructorRawCalldataSurface is ||
exprTouchesUnsupportedConstructorRawCalldataSurface oo ||
exprTouchesUnsupportedConstructorRawCalldataSurface os
| .adtConstruct _ _ args =>
exprListTouchesUnsupportedConstructorRawCalldataSurface args
| .adtTag _ _ | .adtField _ _ _ _ _ => false
def exprListTouchesUnsupportedConstructorRawCalldataSurface : List Expr → Bool
| [] => false
| expr :: rest =>
exprTouchesUnsupportedConstructorRawCalldataSurface expr ||
exprListTouchesUnsupportedConstructorRawCalldataSurface rest
def stmtTouchesUnsupportedConstructorRawCalldataSurface : Stmt → Bool
| .panicCode _ => false
| .panic _ => false
| .letVar _ value | .assignVar _ value | .setStorage _ value
| .setStorageAddr _ value | .setImmutable _ value | .setStorageWord _ _ value
| .require value _ | .return value
| .storageArrayPush _ value =>
exprTouchesUnsupportedConstructorRawCalldataSurface value
| .returnCodeData pointer =>
exprTouchesUnsupportedConstructorRawCalldataSurface pointer
| .setMapping _ key value | .setMappingWord _ key _ value
| .setMappingPackedWord _ key _ _ value | .setMappingUint _ key value
| .setStructMember _ key _ value | .setStorageArrayElement _ key value
| .mstore key value | .tstore key value =>
exprTouchesUnsupportedConstructorRawCalldataSurface key ||
exprTouchesUnsupportedConstructorRawCalldataSurface value
| .setMappingChain _ keys value =>
exprListTouchesUnsupportedConstructorRawCalldataSurface keys ||
exprTouchesUnsupportedConstructorRawCalldataSurface value
| .setMapping2 _ key1 key2 value | .setMapping2Word _ key1 key2 _ value
| .setStructMember2 _ key1 key2 _ value =>
exprTouchesUnsupportedConstructorRawCalldataSurface key1 ||
exprTouchesUnsupportedConstructorRawCalldataSurface key2 ||
exprTouchesUnsupportedConstructorRawCalldataSurface value
| .emit _ args | .internalCallAssign _ _ args | .internalCall _ args
| .externalCallBind _ _ args | .tryExternalCallBind _ _ _ args =>
exprListTouchesUnsupportedConstructorRawCalldataSurface args
| .ite cond thenBranch elseBranch =>
exprTouchesUnsupportedConstructorRawCalldataSurface cond ||
stmtListTouchesUnsupportedConstructorRawCalldataSurface thenBranch ||
stmtListTouchesUnsupportedConstructorRawCalldataSurface elseBranch
| .forEach _ count body | .forEachSetBit _ count body =>
exprTouchesUnsupportedConstructorRawCalldataSurface count ||
stmtListTouchesUnsupportedConstructorRawCalldataSurface body
| .requireError cond _ args =>
exprTouchesUnsupportedConstructorRawCalldataSurface cond ||
exprListTouchesUnsupportedConstructorRawCalldataSurface args
| .revertError _ args =>
exprListTouchesUnsupportedConstructorRawCalldataSurface args
| .calldatacopy destOffset sourceOffset size
| .returndataCopy destOffset sourceOffset size =>
exprTouchesUnsupportedConstructorRawCalldataSurface destOffset ||
exprTouchesUnsupportedConstructorRawCalldataSurface sourceOffset ||
exprTouchesUnsupportedConstructorRawCalldataSurface size
| .stop | .storageArrayPop _
| .returnValues _ | .returnArray _ | .returnBytes _ | .returnStorageWords _
| .revertEmpty | .revertReturndata
| .rawLog _ _ _ | .ecm _ _ => false
| .unsafeBlock _ _ | .unsafeYul _ | .matchAdt _ _ _ => true
def stmtListTouchesUnsupportedConstructorRawCalldataSurface : List Stmt → Bool
| [] => false
| stmt :: rest =>