forked from formalize/coq-vyper
-
Notifications
You must be signed in to change notification settings - Fork 1
/
ConstFold.v
1627 lines (1591 loc) · 71.9 KB
/
ConstFold.v
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
From Coq Require Import String ZArith Lia.
From Coq Require PropExtensionality.
From Vyper Require Import Config UInt256 Calldag.
From Vyper.L20 Require Import AST Callset Descend Expr Stmt.
(** Do constant folding in expressions.
(We don't have const declarations yet,
once we do, this will be somewhat more complicated.) *)
Fixpoint const_fold_expr {C: VyperConfig} (e: expr)
: string + expr
:= let fix const_fold_expr_list (l: list expr)
:= match l with
| nil => inr nil
| (h :: t)%list =>
match const_fold_expr h, const_fold_expr_list t with
| inl err, _ | _, inl err => inl err
| inr h', inr t' => inr (h' :: t')%list
end
end
in match e with
| Const _ | LocalVar _ | StorageVar _ => inr e
| UnOp op a =>
let a' := const_fold_expr a in
match a' with
| inl _ => a'
| inr (Const x) =>
match interpret_unop op x with
| Some val => inr (Const val)
| None => inl ("arithmetic error in unary " ++ L10.ToString.string_of_unop op)%string
end
| inr x => inr (UnOp op x)
end
| BinOp op a b =>
let a' := const_fold_expr a in
let b' := const_fold_expr b in
match a', b' with
| inl err, _ | _, inl err => inl err
| inr (Const x), inr (Const y) =>
match interpret_binop op x y with
| Some val => inr (Const val)
| None => inl ("arithmetic error in binary" ++ L10.ToString.string_of_binop op)%string
end
| inr x, inr y => inr (BinOp op x y)
end
| IfThenElse cond yes no =>
let yes' := const_fold_expr yes in
let no' := const_fold_expr no in
match const_fold_expr cond with
| inl err => inl err
| inr (Const x) => if (Z_of_uint256 x =? 0)%Z then no' else yes'
| inr cond' =>
match yes', no' with
| inl err, _ | _, inl err => inl err
| inr x, inr y => inr (IfThenElse cond' x y)
end
end
| LogicalAnd a b =>
match const_fold_expr a with
| inl err => inl err
| inr (Const x) => if (Z_of_uint256 x =? 0)%Z
then inr (Const x)
else const_fold_expr b
| inr a' => match const_fold_expr b with
| inl err => inl err
| inr b' => inr (LogicalAnd a' b')
end
end
| LogicalOr a b =>
match const_fold_expr a with
| inl err => inl err
| inr (Const x) => if (Z_of_uint256 x =? 0)%Z
then const_fold_expr b
else inr (Const x)
| inr a' => match const_fold_expr b with
| inl err => inl err
| inr b' => inr (LogicalOr a' b')
end
end
| PrivateCall name args => match const_fold_expr_list args with
| inl err => inl err
| inr args' => inr (PrivateCall name args')
end
| BuiltinCall name args => match const_fold_expr_list args with
| inl err => inl err
| inr args' => inr (BuiltinCall name args')
end
end.
(** Constant folding cannot add new calls. *)
Lemma callset_const_fold_expr {C: VyperConfig}
{e e': expr}
(ok: const_fold_expr e = inr e'):
let _ := string_set_impl in
FSet.is_subset (expr_callset e') (expr_callset e) = true.
Proof.
rewrite FSet.is_subset_ok. intro s.
enough (H: let _ := string_set_impl in
FSet.has (expr_callset e') s = true -> FSet.has (expr_callset e) s = true).
{
cbn in H.
destruct (FSet.has (expr_callset e) s); destruct (FSet.has (expr_callset e') s); try easy.
tauto.
}
cbn. revert e' ok. induction e using expr_ind'; intros; inversion ok; subst; cbn in *.
{ (* Const *) assumption. }
{ (* LocalVar *) assumption. }
{ (* StorageVar *) assumption. }
{ (* UnOp *)
destruct (const_fold_expr e). { discriminate. }
apply (IHe _ eq_refl).
destruct e0; cbn; inversion ok; try subst e'; try apply H. (* XXX: e0 *)
destruct (interpret_unop op val). 2:discriminate.
{ inversion ok. subst e'. apply H. }
}
{ (* BinOp *)
rewrite FSet.union_ok; apply Bool.orb_true_intro.
assert (D: forall A A' B B': Prop, (A -> A') -> (B -> B') -> (A \/ B) -> (A' \/ B')) by tauto.
destruct (const_fold_expr e1). discriminate.
destruct e; cbn.
{ (* e1 is Const *)
destruct (const_fold_expr e2). discriminate.
enough (E2: let _ := string_set_impl in FSet.has ((expr_callset e2)) s = true).
{ cbn in E2. rewrite E2. now right. }
cbn. apply (IHe2 _ eq_refl).
destruct e; cbn; inversion ok; try subst e'; cbn in H;
try rewrite FSet.union_ok in H;
try rewrite FSet.empty_ok in H;
try rewrite Bool.orb_false_l in H;
try easy.
(* e2 is Const *)
destruct (interpret_binop op val). 2:discriminate.
inversion ok. subst e'. cbn in H. now rewrite FSet.empty_ok in H.
}
1-9:destruct (const_fold_expr e2); try discriminate;
inversion ok; subst e'; cbn in H;
try rewrite FSet.union_ok in H;
try rewrite FSet.empty_ok in H;
try rewrite Bool.orb_false_l in H;
apply (D _ _ _ _ (IHe1 _ eq_refl) (IHe2 _ eq_refl));
cbn; try repeat rewrite FSet.union_ok;
try repeat rewrite FSet.union_ok in H;
try apply Bool.orb_prop in H; tauto.
}
{ (* IfThenElse *)
repeat rewrite FSet.union_ok. repeat rewrite Bool.orb_true_iff.
assert (D: forall A A' B B' C C': Prop, (A -> A') -> (B -> B') -> (C -> C')
-> (A \/ B \/ C) -> (A' \/ B' \/ C')) by tauto.
destruct (const_fold_expr e1). discriminate.
destruct e.
{ (* Const *)
destruct (Z_of_uint256 val =? 0)%Z.
{
destruct (const_fold_expr e3). discriminate.
inversion ok. subst e'.
repeat rewrite FSet.union_ok.
rewrite (IHe3 _ eq_refl H).
right. right. trivial.
}
(* same as in the previous branch but we dig into "yes" (e2) this time *)
destruct (const_fold_expr e2). discriminate.
inversion ok. subst e'.
repeat rewrite FSet.union_ok.
rewrite (IHe2 _ eq_refl H).
right. left. trivial.
}
1-9:destruct (const_fold_expr e2) as [v2|]; try discriminate;
destruct (const_fold_expr e3) as [v3|]; try discriminate;
inversion ok; subst e'; cbn in H;
repeat rewrite FSet.union_ok in H;
repeat rewrite FSet.empty_ok in H;
apply (D _ _ _ _ _ _ (IHe1 _ eq_refl) (IHe2 _ eq_refl) (IHe3 _ eq_refl));
repeat rewrite Bool.orb_true_iff in H; cbn; try rewrite FSet.empty_ok;
repeat rewrite FSet.union_ok; repeat rewrite Bool.orb_true_iff; tauto.
}
{ (* LogicalAnd *)
rewrite FSet.union_ok; apply Bool.orb_true_intro.
assert (D: forall A A' B B': Prop, (A -> A') -> (B -> B') -> (A \/ B) -> (A' \/ B')) by tauto.
destruct (const_fold_expr e1). discriminate.
destruct e; cbn.
{ (* e1 is Const *)
destruct (Z_of_uint256 val =? 0)%Z.
{ inversion ok. subst e'. cbn in H. rewrite FSet.empty_ok in H. discriminate. }
right. apply (IHe2 _ ok H).
}
1-9:destruct (const_fold_expr e2) as [v2|]; try discriminate;
inversion ok; subst e'; cbn in H;
repeat rewrite FSet.union_ok in H;
repeat rewrite FSet.empty_ok in H;
apply (D _ _ _ _ (IHe1 _ eq_refl) (IHe2 _ eq_refl));
repeat rewrite Bool.orb_true_iff in H; cbn; try rewrite FSet.empty_ok;
repeat rewrite FSet.union_ok; repeat rewrite Bool.orb_true_iff; tauto.
}
{ (* LogicalOr *)
rewrite FSet.union_ok; apply Bool.orb_true_intro.
assert (D: forall A A' B B': Prop, (A -> A') -> (B -> B') -> (A \/ B) -> (A' \/ B')) by tauto.
destruct (const_fold_expr e1). discriminate.
destruct e; cbn.
{ (* e1 is Const *)
destruct (Z_of_uint256 val =? 0)%Z.
right. apply (IHe2 _ ok H).
{ inversion ok. subst e'. cbn in H. rewrite FSet.empty_ok in H. discriminate. }
}
1-9:destruct (const_fold_expr e2) as [v2|]; try discriminate;
inversion ok; subst e'; cbn in H;
repeat rewrite FSet.union_ok in H;
repeat rewrite FSet.empty_ok in H;
apply (D _ _ _ _ (IHe1 _ eq_refl) (IHe2 _ eq_refl));
repeat rewrite Bool.orb_true_iff in H; cbn; try rewrite FSet.empty_ok;
repeat rewrite FSet.union_ok; repeat rewrite Bool.orb_true_iff; tauto.
}
{ (* PrivateCall *)
rewrite FSet.add_ok. destruct (string_dec name s) as [_|NE]. { trivial. }
clear H2. rename H into F. rename H0 into H. (* XXX *)
revert e' ok H. induction args as [|head]; intros.
{
inversion ok. subst e'. cbn in H.
rewrite FSet.add_ok in H.
destruct (string_dec name s). { contradiction. } exact H.
}
assert (FH := List.Forall_inv F). cbn in FH.
destruct (const_fold_expr head). discriminate.
assert (FHvalue := FH _ eq_refl). clear FH.
rewrite FSet.union_ok.
destruct (_ args). discriminate.
inversion ok. subst e'.
cbn in H. rewrite FSet.add_ok in H.
destruct (string_dec name s) as [|_]. { contradiction. }
rewrite FSet.union_ok in H.
rewrite Bool.orb_true_iff in H.
rewrite Bool.orb_true_iff.
assert (IH := IHargs (List.Forall_inv_tail F) _ eq_refl).
cbn in IH. rewrite FSet.add_ok in IH.
destruct (string_dec name s) as [|_]. { contradiction. }
tauto.
}
(* BuiltinCall *)
clear H2. rename H into F. rename H0 into H. (* XXX *)
revert e' ok H. induction args as [|head]; intros.
{ inversion ok. subst e'. cbn in H. exact H. }
assert (FH := List.Forall_inv F). cbn in FH.
destruct (const_fold_expr head). discriminate.
assert (FHvalue := FH _ eq_refl). clear FH.
rewrite FSet.union_ok.
destruct (_ args). discriminate.
inversion ok. subst e'.
cbn in H.
rewrite FSet.union_ok in H.
rewrite Bool.orb_true_iff in H.
rewrite Bool.orb_true_iff.
assert (IH := IHargs (List.Forall_inv_tail F) _ eq_refl).
cbn in IH.
tauto.
Qed.
Definition sum_map {C: VyperConfig} {Err A B} (f: A -> B) (e: Err + A)
: Err + B
:= match e with
| inl err => inl err
| inr a => inr (f a)
end.
Definition const_fold_small_stmt {C: VyperConfig} (ss: small_stmt)
: string + small_stmt
:= match ss with
| Pass | Abort _ => inr ss
| Return e => sum_map Return (const_fold_expr e)
| Raise e => sum_map Raise (const_fold_expr e)
| Assign lhs e => sum_map (Assign lhs) (const_fold_expr e)
| ExprStmt e => sum_map ExprStmt (const_fold_expr e)
end.
Lemma callset_const_fold_small_stmt {C: VyperConfig}
{ss ss': small_stmt}
(ok: const_fold_small_stmt ss = inr ss'):
let _ := string_set_impl in
FSet.is_subset (small_stmt_callset ss') (small_stmt_callset ss) = true.
Proof.
cbn. destruct ss; cbn in ok; unfold sum_map in *.
1-2: (* Pass, Abort *) inversion ok; subst ss'; apply FSet.is_subset_refl.
1-4:
remember (const_fold_expr _) as z; symmetry in Heqz; destruct z; try discriminate;
assert (E := callset_const_fold_expr Heqz); cbn in E;
inversion ok; subst ss'; apply E.
Qed.
Definition sum_ap {C: VyperConfig} {Err A B} (f: Err + (A -> B)) (e: Err + A)
: Err + B
:= match f with
| inr g => match e with
| inr a => inr (g a)
| inl err => inl err
end
| inl err => inl err
end.
Fixpoint const_fold_stmt {C: VyperConfig} (s: stmt)
: string + stmt
:= match s with
| SmallStmt ss => sum_map SmallStmt (const_fold_small_stmt ss)
| LocalVarDecl name init body =>
sum_ap (sum_map (LocalVarDecl name) (const_fold_expr init))
(const_fold_stmt body)
| IfElseStmt cond yes no =>
(* no attempt is made here to throw away the unused branch if [cond] is a constant. *)
sum_ap (sum_ap (sum_map IfElseStmt (const_fold_expr cond))
(const_fold_stmt yes))
(const_fold_stmt no)
| Loop name init count body =>
sum_ap (sum_map (fun f => f count)
(sum_map (Loop name) (const_fold_expr init)))
(const_fold_stmt body)
| Semicolon a b =>
sum_ap (sum_map Semicolon (const_fold_stmt a)) (const_fold_stmt b)
end.
Lemma callset_const_fold_stmt {C: VyperConfig}
{s s': stmt}
(ok: const_fold_stmt s = inr s'):
let _ := string_set_impl in
FSet.is_subset (stmt_callset s') (stmt_callset s) = true.
Proof.
cbn.
revert s' ok.
induction s; intros; cbn in ok; unfold sum_map in *; unfold sum_ap in *; cbn.
{ (* SmallStmt *)
remember (const_fold_small_stmt _) as z; symmetry in Heqz; destruct z; try discriminate.
inversion ok; subst s'.
apply (callset_const_fold_small_stmt Heqz).
}
{ (* LocalVarDecl *)
remember (const_fold_expr _) as init'; symmetry in Heqinit'; destruct init'; try discriminate.
remember (const_fold_stmt _) as body'; symmetry in Heqbody'; destruct body'; try discriminate.
assert (InitOk := callset_const_fold_expr Heqinit').
assert (BodyOk := IHs _ eq_refl).
inversion ok; subst s'.
cbn in *.
now apply FSet.union_monotonic.
}
{ (* IfElseStmt *)
rename s1 into yes. rename IHs1 into IHyes. rename s2 into no. rename IHs2 into IHno.
remember (const_fold_expr cond) as cond'; symmetry in Heqcond'; destruct cond'; try discriminate.
remember (const_fold_stmt yes) as yes'; symmetry in Heqyes'; destruct yes'; try discriminate.
remember (const_fold_stmt no) as no'; symmetry in Heqno'; destruct no'; try discriminate.
assert (CondOk := callset_const_fold_expr Heqcond').
assert (YesOk := IHyes _ eq_refl).
assert (NoOk := IHno _ eq_refl).
inversion ok; subst s'.
cbn in *.
apply FSet.union_monotonic. { assumption. }
now apply FSet.union_monotonic.
}
{ (* Loop *)
remember (const_fold_expr start) as start'; symmetry in Heqstart'; destruct start'; try discriminate.
remember (const_fold_stmt _) as body'; symmetry in Heqbody'; destruct body'; try discriminate.
assert (StartOk := callset_const_fold_expr Heqstart').
assert (BodyOk := IHs _ eq_refl).
inversion ok; subst s'.
cbn in *.
now apply FSet.union_monotonic.
}
(* Semicolon *)
remember (const_fold_stmt s1) as s1'; symmetry in Heqs1'; destruct s1'; try discriminate.
remember (const_fold_stmt s2) as s2'; symmetry in Heqs2'; destruct s2'; try discriminate.
assert (Ok1 := IHs1 _ eq_refl).
assert (Ok2 := IHs2 _ eq_refl).
inversion ok; subst s'.
cbn in *.
now apply FSet.union_monotonic.
Qed.
Definition const_fold_decl {C: VyperConfig} (d: decl)
: string + decl
:= match d with
| StorageVarDecl name => inr d
| FunDecl name arg_names body =>
sum_map (FunDecl name arg_names) (const_fold_stmt body)
end.
Lemma callset_const_fold_decl {C: VyperConfig}
{d d': decl}
(ok: const_fold_decl d = inr d'):
let _ := string_set_impl in
FSet.is_subset (decl_callset d') (decl_callset d) = true.
Proof.
destruct d; cbn in *.
{ inversion ok. subst d'. cbn. apply FSet.is_subset_refl. }
remember (const_fold_stmt body) as body'. symmetry in Heqbody'. destruct body'. { easy. }
cbn in ok. inversion ok. subst d'. cbn.
now apply callset_const_fold_stmt.
Qed.
Definition const_fold_calldag {C: VyperConfig} (cd: calldag)
:= calldag_maybe_map const_fold_decl (@callset_const_fold_decl C) cd.
Definition const_fold_fun_ctx {C: VyperConfig}
{bound: nat}
{cd cd': calldag}
(Ok: const_fold_calldag cd = inr cd')
: fun_ctx cd bound -> fun_ctx cd' bound
:= fun_ctx_maybe_map const_fold_decl (@callset_const_fold_decl C) Ok.
(*************************************************************************************)
Lemma weak_interpret_const_fold_expr_list
{C: VyperConfig}
{(*bigger_call_depth_bound*) smaller_call_depth_bound: nat}
(*(Ebound: bigger_call_depth_bound = S smaller_call_depth_bound)*)
(builtins: string -> option L10.Base.builtin)
{cd cd': calldag}
(ok: const_fold_calldag cd = inr cd')
(fc: fun_ctx cd (S smaller_call_depth_bound))
{do_call: forall
(smaller_fc: fun_ctx cd smaller_call_depth_bound)
(world: world_state)
(arg_values: list uint256),
world_state * L10.Base.expr_result uint256}
{do_call': forall
(smaller_fc: fun_ctx cd' smaller_call_depth_bound)
(world: world_state)
(arg_values: list uint256),
world_state * L10.Base.expr_result uint256}
(DoCallOk: forall smaller_fc world arg_values,
do_call' (const_fold_fun_ctx ok smaller_fc) world arg_values
=
do_call smaller_fc world arg_values)
(world: world_state)
(loc: string_map uint256)
{l l': list expr}
(ExprOk: (fix const_fold_expr_list (l: list expr)
:= match l with
| nil => inr nil
| (h :: t)%list =>
match const_fold_expr h, const_fold_expr_list t with
| inl err, _ | _, inl err => inl err
| inr h', inr t' => inr (h' :: t')%list
end
end) l = inr l')
(CallOk': let _ := string_set_impl in
FSet.is_subset (expr_list_callset l')
(decl_callset
(fun_decl
(const_fold_fun_ctx ok fc)))
= true)
(CallOk: let _ := string_set_impl in
FSet.is_subset (expr_list_callset l)
(decl_callset (fun_decl fc))
= true)
(ItemsOk: List.Forall
(fun e : expr =>
forall e' : expr,
const_fold_expr e = inr e' ->
forall
(CallOk : let H := string_set_impl in
FSet.is_subset (expr_callset e) (decl_callset (fun_decl fc)) = true)
(CallOk' : let H := string_set_impl in
FSet.is_subset (expr_callset e')
(decl_callset (fun_decl (const_fold_fun_ctx ok fc))) = true)
(world : world_state) (loc : string_map uint256),
interpret_expr eq_refl (const_fold_fun_ctx ok fc) do_call' builtins world loc e' CallOk' =
interpret_expr eq_refl fc do_call builtins world loc e CallOk) l):
interpret_expr_list eq_refl (const_fold_fun_ctx ok fc)
do_call' builtins
world loc l' CallOk'
=
interpret_expr_list eq_refl fc
do_call builtins
world loc l CallOk.
Proof.
revert l' ExprOk CallOk' world loc. induction l as [|lhead]; intros.
{ inversion ExprOk. now subst l'. }
remember (const_fold_expr lhead) as chead. symmetry in Heqchead.
destruct chead. { discriminate. }
assert (HeadItemOk := List.Forall_inv ItemsOk).
assert (TailItemsOk := List.Forall_inv_tail ItemsOk).
remember ((fix const_fold_expr_list (l : list expr) : string + list expr :=
match l with
| nil => inr nil
| (h :: t)%list =>
match const_fold_expr h with
| inl err => inl err
| inr h' =>
match const_fold_expr_list t with
| inl err => inl err
| inr t' => inr (h' :: t')%list
end
end
end) l) as c'.
symmetry in Heqc'.
destruct c'. { discriminate. }
inversion ExprOk. subst l'.
cbn.
rewrite (HeadItemOk _ Heqchead
(callset_descend_head eq_refl CallOk)
(callset_descend_head eq_refl CallOk')).
destruct interpret_expr as (world', result_h). destruct result_h. 2:{ trivial. }
now rewrite (IHl (callset_descend_tail eq_refl CallOk) TailItemsOk _ eq_refl
(callset_descend_tail eq_refl CallOk')).
Qed.
Lemma interpret_const_fold_expr {C: VyperConfig}
{bigger_call_depth_bound smaller_call_depth_bound: nat}
(Ebound: bigger_call_depth_bound = S smaller_call_depth_bound)
(builtins: string -> option L10.Base.builtin)
{cd cd': calldag}
(ok: const_fold_calldag cd = inr cd')
(fc: fun_ctx cd bigger_call_depth_bound)
{do_call: forall
(smaller_fc: fun_ctx cd smaller_call_depth_bound)
(world: world_state)
(arg_values: list uint256),
world_state * L10.Base.expr_result uint256}
{do_call': forall
(smaller_fc: fun_ctx cd' smaller_call_depth_bound)
(world: world_state)
(arg_values: list uint256),
world_state * L10.Base.expr_result uint256}
(DoCallOk: forall smaller_fc world arg_values,
do_call' (const_fold_fun_ctx ok smaller_fc) world arg_values
=
do_call smaller_fc world arg_values)
(world: world_state)
(loc: string_map uint256)
{e e': expr}
(ExprOk: const_fold_expr e = inr e')
(CallOk': let _ := string_set_impl in
FSet.is_subset (expr_callset e')
(decl_callset
(fun_decl
(const_fold_fun_ctx ok fc)))
= true)
(CallOk: let _ := string_set_impl in
FSet.is_subset (expr_callset e)
(decl_callset (fun_decl fc))
= true):
interpret_expr Ebound (const_fold_fun_ctx ok fc)
do_call' builtins
world loc e' CallOk'
=
interpret_expr Ebound fc
do_call builtins
world loc e CallOk.
Proof.
revert e' ExprOk CallOk CallOk' world loc. induction e using expr_ind'; intros;
cbn in ExprOk; inversion ExprOk; subst.
(* Const, LocalVar *) 1-2: reflexivity.
{ (* StorageVar *)
cbn.
unfold storage_var_is_declared.
assert (F := calldag_maybe_map_declmap const_fold_decl (@callset_const_fold_decl C) ok name).
destruct (cd_declmap cd name), (cd_declmap cd' name); try easy.
destruct d; cbn in F; inversion F. { now subst. }
remember (const_fold_stmt body) as body'.
destruct body'. { discriminate. }
inversion F. now subst.
}
{ (* UnOp *)
remember (const_fold_expr e) as ce.
destruct ce as [|arg]. { discriminate. }
destruct arg.
{ (* arg is const, so interpret immediately *)
remember (interpret_unop op val) as unop_result. destruct unop_result. 2:discriminate.
inversion ExprOk. subst e'. cbn.
rewrite<- (IHe _ eq_refl _ CallOk').
cbn. unfold Base.interpret_unop.
now rewrite<- Hequnop_result.
}
(* arg is not const *)
1-9: inversion ExprOk; subst e';
assert (IH := IHe _ eq_refl
(callset_descend_unop eq_refl CallOk)
(callset_descend_unop eq_refl CallOk')
world loc);
cbn; now rewrite<- IH.
}
{ (* BinOp *)
assert (BinOpOk:
forall (e1' e2': expr) CallOk' CallOk
(Left: interpret_expr eq_refl (const_fold_fun_ctx ok fc) do_call' builtins world loc
e1' (callset_descend_binop_left eq_refl CallOk')
=
interpret_expr eq_refl fc do_call builtins world loc e1
(callset_descend_binop_left eq_refl CallOk))
(Right: forall world loc,
interpret_expr eq_refl (const_fold_fun_ctx ok fc) do_call' builtins world loc e2'
(callset_descend_binop_right eq_refl CallOk')
=
interpret_expr eq_refl fc do_call builtins world loc e2
(callset_descend_binop_right eq_refl CallOk)),
interpret_expr eq_refl (const_fold_fun_ctx ok fc) do_call' builtins world loc
(BinOp op e1' e2') CallOk'
=
interpret_expr eq_refl fc do_call builtins world loc (BinOp op e1 e2) CallOk).
{
intros.
cbn. rewrite<- Left. cbn.
match goal with
|- (let (world', result_a) := ?x in _) = _ =>
destruct x as (world', result_a)
end.
destruct result_a. 2:reflexivity.
cbn. now rewrite Right.
}
remember (const_fold_expr e1) as ce1.
destruct ce1 as [|arg1]. { discriminate. }
destruct arg1; remember (const_fold_expr e2) as ce2; destruct ce2 as [|arg2]; try discriminate.
{ (* arg1 is const, so check out arg2 *)
destruct arg2.
{ (* arg2 is const, so interpret immediately *)
remember (interpret_binop op _ _) as binop_result. destruct binop_result. 2:discriminate.
inversion ExprOk. subst e'. cbn.
rewrite<- (IHe1 _ eq_refl _ CallOk').
cbn.
rewrite<- (IHe2 _ eq_refl _ CallOk').
unfold Base.interpret_binop. cbn.
now rewrite<- Heqbinop_result.
}
(* arg2 is not const *)
1-9: inversion ExprOk; subst e';
assert (IH1 := IHe1 _ eq_refl
(callset_descend_binop_left eq_refl CallOk)
(callset_descend_binop_left eq_refl CallOk')
world loc);
assert (IH2 := IHe2 _ eq_refl
(callset_descend_binop_right eq_refl CallOk)
(callset_descend_binop_right eq_refl CallOk')
world loc);
cbn; rewrite<- IH1; cbn; now rewrite<- IH2.
}
(* arg1 is not const *)
1-9: inversion ExprOk; subst e';
assert (IH1 := IHe1 _ eq_refl
(callset_descend_binop_left eq_refl CallOk)
(callset_descend_binop_left eq_refl CallOk')
world loc);
assert (IH2 := IHe2 _ eq_refl
(callset_descend_binop_right eq_refl CallOk)
(callset_descend_binop_right eq_refl CallOk'));
apply (BinOpOk _ _ CallOk' CallOk IH1 IH2).
}
{ (* IfThenElse *)
rename e1 into cond. rename IHe1 into IHcond.
rename e2 into yes. rename IHe2 into IHyes.
rename e3 into no. rename IHe3 into IHno.
remember (const_fold_expr cond) as cc. destruct cc as [|cc]. { discriminate. }
cbn.
destruct cc.
{ (* cond is a const *)
rewrite<- (IHcond _ eq_refl
(callset_descend_if_cond eq_refl CallOk)
FSet.empty_subset).
cbn.
destruct (Z_of_uint256 val =? 0)%Z.
{ now apply IHno. }
now apply IHyes.
}
(* cond is not const *)
1-9: remember (const_fold_expr yes) as cyes; destruct cyes as [|cyes]; try discriminate;
remember (const_fold_expr no) as cno; destruct cno as [|cno]; try discriminate;
inversion ExprOk; subst e';
try match goal with
| H: inr ?c = const_fold_expr _ |- _ => remember c as cond'
end;
rewrite<- (IHcond _ eq_refl
(callset_descend_if_cond eq_refl CallOk)
(callset_descend_if_cond eq_refl CallOk'));
cbn;
destruct interpret_expr;
rewrite (IHyes _ eq_refl
(callset_descend_if_then eq_refl CallOk)
(callset_descend_if_then eq_refl CallOk'));
rewrite (IHno _ eq_refl
(callset_descend_if_else eq_refl CallOk)
(callset_descend_if_else eq_refl CallOk'));
trivial.
}
{ (* LogicalAnd *)
remember (const_fold_expr e1) as c1. destruct c1 as [|c1]. { discriminate. }
cbn.
destruct c1.
{ (* left arg is a const *)
rewrite<- (IHe1 _ eq_refl
(callset_descend_and_left eq_refl CallOk)
FSet.empty_subset).
cbn.
destruct (Z_of_uint256 val =? 0)%Z.
{ inversion ExprOk. now subst e'. }
now apply IHe2.
}
(* left arg is not const *)
1-9: remember (const_fold_expr e2) as c2; destruct c2 as [|c2]; try discriminate;
inversion ExprOk; subst e';
try match goal with
| H: inr ?c = const_fold_expr _ |- _ => remember c as cond'
end;
rewrite<- (IHe1 _ eq_refl
(callset_descend_and_left eq_refl CallOk)
(callset_descend_and_left eq_refl CallOk'));
cbn;
destruct interpret_expr;
now rewrite (IHe2 _ eq_refl
(callset_descend_and_right eq_refl CallOk)
(callset_descend_and_right eq_refl CallOk')).
}
{ (* LogicalOr *)
remember (const_fold_expr e1) as c1. destruct c1 as [|c1]. { discriminate. }
cbn.
destruct c1.
{ (* left arg is a const *)
rewrite<- (IHe1 _ eq_refl
(callset_descend_or_left eq_refl CallOk)
FSet.empty_subset).
cbn.
destruct (Z_of_uint256 val =? 0)%Z.
{ now apply IHe2. }
inversion ExprOk. now subst e'.
}
(* left arg is not const *)
1-9: remember (const_fold_expr e2) as c2; destruct c2 as [|c2]; try discriminate;
inversion ExprOk; subst e';
try match goal with
| H: inr ?c = const_fold_expr _ |- _ => remember c as cond'
end;
rewrite<- (IHe1 _ eq_refl
(callset_descend_or_left eq_refl CallOk)
(callset_descend_or_left eq_refl CallOk'));
cbn;
destruct interpret_expr;
now rewrite (IHe2 _ eq_refl
(callset_descend_or_right eq_refl CallOk)
(callset_descend_or_right eq_refl CallOk')).
}
{ (* PrivateCall *)
remember ((fix const_fold_expr_list (l : list expr) : string + list expr :=
match l with
| nil => inr nil
| (h :: t)%list =>
match const_fold_expr h with
| inl err => inl err
| inr h' =>
match const_fold_expr_list t with
| inl err => inl err
| inr t' => inr (h' :: t')%list
end
end
end) args) as cargs. symmetry in Heqcargs. destruct cargs. { discriminate. }
inversion ExprOk. subst e'. cbn.
rename l into args'.
assert (R':
forall Ok' Ok, (* initially: (callset_descend_args eq_refl CallOk') etc *)
interpret_expr_list eq_refl (const_fold_fun_ctx ok fc) do_call' builtins world loc args' Ok'
=
(fix
interpret_expr_list (world0 : world_state) (loc0 : string_map uint256)
(e : list expr)
(CallOk0 : FSet.is_subset (expr_list_callset e)
(decl_callset (cached_maybe_mapped_decl const_fold_decl
(@callset_const_fold_decl C) ok fc)) = true) {struct
e} : world_state * Base.expr_result (list uint256) :=
match e as e' return (e = e' -> world_state * Base.expr_result (list uint256)) with
| nil => fun _ : e = nil => (world0, Base.ExprSuccess nil)
| (h :: t)%list =>
fun E : e = (h :: t)%list =>
let (world', result_h) :=
interpret_expr eq_refl (const_fold_fun_ctx ok fc) do_call' builtins world0 loc0 h
(callset_descend_head E CallOk0) in
match result_h with
| Base.ExprSuccess x =>
let (world'', result_t) :=
interpret_expr_list world' loc0 t (callset_descend_tail E CallOk0) in
(world'',
match result_t with
| Base.ExprSuccess y => Base.ExprSuccess (x :: y)%list
| Base.ExprAbort _ => result_t
end)
| Base.ExprAbort ab => (world', Base.ExprAbort ab)
end
end eq_refl) world loc args' Ok).
{
clear CallOk CallOk' Heqcargs ExprOk H1.
revert world loc. induction args'. { easy. }
intros. cbn.
assert (Irrel:
(@callset_descend_head C a args' (a :: args')
(@decl_callset C
(@cached_maybe_mapped_decl C (@decl C) (@decl C) (@decl_callset C) false
(@decl_callset C) (@const_fold_decl C) (@callset_const_fold_decl C) cd cd' ok
(S smaller_call_depth_bound) fc)) (@eq_refl (list (@expr C)) (a :: args')%list) Ok')
=
(@callset_descend_head C a args' (a :: args')
(@decl_callset C
(@cached_maybe_mapped_decl C (@decl C) (@decl C) (@decl_callset C) false
(@decl_callset C) (@const_fold_decl C) (@callset_const_fold_decl C) cd cd' ok
(S smaller_call_depth_bound) fc)) (@eq_refl (list (@expr C)) (a :: args')%list) Ok)).
{ apply PropExtensionality.proof_irrelevance. }
rewrite Irrel.
destruct interpret_expr. destruct e. 2:{ trivial. }
now rewrite (IHargs' w loc
(@callset_descend_tail C a args' (a :: args')
(@decl_callset C
(@cached_maybe_mapped_decl C (@decl C) (@decl C) (@decl_callset C) false
(@decl_callset C) (@const_fold_decl C) (@callset_const_fold_decl C) cd cd' ok
(S smaller_call_depth_bound) fc)) (@eq_refl (list (@expr C)) (a :: args')%list) Ok')
(@callset_descend_tail C a args' (a :: args')
(@decl_callset C
(@cached_maybe_mapped_decl C (@decl C) (@decl C) (@decl_callset C) false
(@decl_callset C) (@const_fold_decl C) (@callset_const_fold_decl C) cd cd' ok
(S smaller_call_depth_bound) fc)) (@eq_refl (list (@expr C)) (a :: args')%list) Ok) ).
}
rewrite<- (R' (callset_descend_args eq_refl CallOk')). clear R'.
assert (W := weak_interpret_const_fold_expr_list builtins ok fc DoCallOk world loc Heqcargs
(callset_descend_args eq_refl CallOk')
(callset_descend_args eq_refl CallOk)
H).
rewrite W.
assert (R:
forall Ok' Ok,
interpret_expr_list eq_refl fc do_call builtins world loc args Ok'
=
(fix
interpret_expr_list (world0 : world_state) (loc0 : string_map uint256)
(e : list expr)
(CallOk0 : FSet.is_subset (expr_list_callset e) (decl_callset (fun_decl fc)) =
true) {struct e} : world_state * Base.expr_result (list uint256) :=
match e as e' return (e = e' -> world_state * Base.expr_result (list uint256)) with
| nil => fun _ : e = nil => (world0, Base.ExprSuccess nil)
| (h :: t)%list =>
fun E : e = (h :: t)%list =>
let (world', result_h) :=
interpret_expr eq_refl fc do_call builtins world0 loc0 h (callset_descend_head E CallOk0) in
match result_h with
| Base.ExprSuccess x =>
let (world'', result_t) :=
interpret_expr_list world' loc0 t (callset_descend_tail E CallOk0) in
(world'',
match result_t with
| Base.ExprSuccess y => Base.ExprSuccess (x :: y)%list
| Base.ExprAbort _ => result_t
end)
| Base.ExprAbort ab => (world', Base.ExprAbort ab)
end
end eq_refl) world loc args Ok).
{
clear CallOk CallOk' Heqcargs args' W ExprOk H H1.
revert world loc. induction args. { easy. }
intros. cbn.
(* this is relatively horror-free this time: *)
assert (Irrel: callset_descend_head eq_refl Ok' = callset_descend_head eq_refl Ok).
{ apply PropExtensionality.proof_irrelevance. }
rewrite Irrel.
destruct interpret_expr. destruct e. 2:{ trivial. }
now rewrite (IHargs w loc
(callset_descend_tail eq_refl Ok')
(callset_descend_tail eq_refl Ok)).
}
rewrite<- (R (callset_descend_args eq_refl CallOk)). clear R.
remember (interpret_expr_list eq_refl fc do_call builtins world loc args
(callset_descend_args eq_refl CallOk)) as after_args. clear Heqafter_args.
destruct after_args as (world', result_args).
destruct result_args. 2:{ trivial. }
(* args computation has succeeded *)
enough (D: fun_ctx_descend (const_fold_fun_ctx ok fc)
CallOk' eq_refl eq_refl
=
match fun_ctx_descend fc CallOk eq_refl eq_refl with
| Some ctx => Some (const_fold_fun_ctx ok ctx)
| None => None
end).
{
rewrite D.
now destruct (fun_ctx_descend fc CallOk eq_refl eq_refl).
}
(* This follows the proof of D from From20To30/Expr.v, which in turn follows fun_ctx_descend_irrel. *)
unfold fun_ctx_descend.
assert (InnerOk: forall (d1 d2: decl)
(Edecl1: cd_declmap cd name = Some d1)
(Edecl2: cd_declmap cd' name = Some d2),
L20.Descend.fun_ctx_descend_inner (const_fold_fun_ctx ok fc) CallOk'
eq_refl eq_refl Edecl2
=
match L20.Descend.fun_ctx_descend_inner fc CallOk eq_refl eq_refl Edecl1 with
| Some ctx => Some (const_fold_fun_ctx ok ctx)
| None => None
end).
{
intros.
unfold Descend.fun_ctx_descend_inner.
remember (fun (depth: nat) (Edepth: cd_depthmap cd' name = Some depth) =>
Some
{|
fun_name := name;
fun_depth := depth;
fun_depth_ok := Edepth;
fun_decl := d2;
fun_decl_ok := Edecl2;
fun_bound_ok := Descend.call_descend' (const_fold_fun_ctx ok fc)
CallOk' eq_refl eq_refl
Edecl2 Edepth |})
as some_branch_l.
remember (fun Edepth : cd_depthmap cd' name = None =>
False_rect (option (fun_ctx cd' smaller_call_depth_bound))
(Descend.fun_ctx_descend_helper Edecl2 Edepth))
as none_branch_l.
remember (fun (depth: nat) (Edepth: cd_depthmap cd name = Some depth) =>
Some
{|
fun_name := name;
fun_depth := depth;
fun_depth_ok := Edepth;
fun_decl := d1;
fun_decl_ok := Edecl1;
fun_bound_ok := Descend.call_descend' fc CallOk eq_refl eq_refl Edecl1 Edepth |})
as some_branch_r.
remember (fun Edepth : cd_depthmap cd name = None =>
False_rect (option (fun_ctx cd smaller_call_depth_bound))
(L20.Descend.fun_ctx_descend_helper Edecl1 Edepth))
as none_branch_r.
assert (NoneOkL: forall (Edepth: cd_depthmap cd' name = None),
none_branch_l Edepth = None).
{ intro. exfalso. exact (Descend.fun_ctx_descend_helper Edecl2 Edepth). }
assert (NoneOkR: forall (Edepth: cd_depthmap cd name = None),
none_branch_r Edepth = None).
{ intro. exfalso. exact (Descend.fun_ctx_descend_helper Edecl1 Edepth). }
clear Heqnone_branch_l Heqnone_branch_r.
revert none_branch_l none_branch_r NoneOkL NoneOkR.
assert (SomeBranchOk: forall (depth: nat)
(Edepth1: cd_depthmap cd name = Some depth)
(Edepth2: cd_depthmap cd' name = Some depth),
some_branch_l depth Edepth2
=
match some_branch_r depth Edepth1 with
| Some ctx => Some (const_fold_fun_ctx ok ctx)
| None => None
end).
{
intros. subst. unfold const_fold_fun_ctx. cbn.
f_equal.
assert (D: d2 = cached_maybe_mapped_decl const_fold_decl (@callset_const_fold_decl C) ok
{|
fun_name := name;
fun_depth := depth;
fun_depth_ok := Edepth1;
fun_decl := d1;
fun_decl_ok := Edecl1;
fun_bound_ok := Descend.call_descend' fc CallOk eq_refl eq_refl Edecl1 Edepth1 |}).
{
unfold cached_maybe_mapped_decl. cbn.
remember (Calldag.calldag_maybe_map_fun_ctx_fun_decl_helper _ _ ok _) as Bad. clear HeqBad.
cbn in Bad. revert Bad.
destruct (cd_declmap cd' name). { now inversion Edecl2. }
intro Bad. discriminate.
}
subst. unfold fun_ctx_maybe_map. cbn.
f_equal; apply PropExtensionality.proof_irrelevance.
} (* SomeBranchOk *)
clear Heqsome_branch_l Heqsome_branch_r
CallOk CallOk' Edecl1 Edecl2 d1 d2 args value DoCallOk
do_call do_call' H Heqcargs W.
revert some_branch_l some_branch_r SomeBranchOk.
rewrite (calldag_maybe_map_depthmap_ok const_fold_decl _ ok name).
destruct (cd_depthmap cd' name), (cd_depthmap cd name); intros;
try apply SomeBranchOk; rewrite (NoneOkL eq_refl); rewrite (NoneOkR eq_refl); trivial.
} (* InnerOk *)
remember (@Descend.fun_ctx_descend_inner C (S smaller_call_depth_bound) smaller_call_depth_bound cd'
(@PrivateCall C name args') name args') as inner'.
remember (@Descend.fun_ctx_descend_inner C (S smaller_call_depth_bound) smaller_call_depth_bound cd
(@PrivateCall C name args) name args) as inner.
clear Heqinner' Heqinner.
subst.
remember (fun d (Edecl: cd_declmap cd' name = Some d) =>
inner' (const_fold_fun_ctx ok fc) CallOk' eq_refl eq_refl d Edecl)
as some_branch'.
remember (cd_declmap cd name) as maybe_d. destruct maybe_d.
{
assert (SomeBranchOk: forall (d': decl)
(Edecl: cd_declmap cd' name = Some d'),
some_branch' d' Edecl
=
match inner fc CallOk eq_refl eq_refl d eq_refl with
| Some ctx => Some (const_fold_fun_ctx ok ctx)
| None => None
end).
{ intros. apply InnerOk. }
clear Heqsome_branch'.
remember (cd_declmap cd' name) as maybe_d'.
destruct maybe_d'. { apply SomeBranchOk. }
assert (T := calldag_maybe_map_declmap const_fold_decl _ ok name).
rewrite<- Heqmaybe_d' in T.
rewrite<- Heqmaybe_d in T.
discriminate.
}
assert (SomeBranchOk: forall (d': decl)
(Edecl: cd_declmap cd' name = Some d'),
some_branch' d' Edecl
=