-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathcompaux.thy
1850 lines (1641 loc) · 55.7 KB
/
compaux.thy
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
chapter {* Generated by Lem from compile.lem. *}
theory "compaux"
imports
Main "~~/src/HOL/Library/Code_Target_Numeral"
"Lem_pervasives"
"Evm"
"Word8"
"Rlp"
"Compile"
begin
(****************************************************)
(* *)
(* Termination Proofs *)
(* *)
(****************************************************)
(*
termination big_step by lexicographic_order
*)
termination get_expr by lexicographic_order
termination compile_expr by lexicographic_order
(****************************************************)
(* *)
(* Lemmata *)
(* *)
(****************************************************)
declare respond_to_call_correctly_def [simp]
declare respond_to_return_correctly_def [simp]
declare respond_to_fail_correctly_def [simp]
declare build_cenv_def [simp]
declare program_of_lst_def [simp]
declare build_venv_called.simps [simp]
declare eval_annotation_def [simp]
text {* The following lemma is just for controlling the Isabelle/HOL simplifier. *}
value "program_content_of_lst 0 always_fail_code"
(*
declare program_annotation_of_lst_def [simp]
*)
(*
declare store_byte_list_in_program.simps [simp]
*)
lemma foo [cong] : "100 = Suc 99"
apply(auto)
done
declare program_sem.psimps [simp]
(*
declare program_sem.simps [simp]
*)
declare program_iter.simps [simp]
declare program_step.simps [simp]
theorem iter_return [simp] :
"program_iter c (Return st) steps = Return st"
apply(induction steps)
apply(auto)
done
theorem iter_tinystep [simp] :
" program_iter c (Continue v 0 (Suc k)) (Suc steps) =
Return (program_sem v c 0 (Suc k))"
apply(subst program_sem.simps)
apply(auto)
done
theorem iter_annot [simp] :
" \<not> check_annotations v c \<Longrightarrow>
program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return (program_sem v c (Suc n) (Suc k))"
apply(subst program_sem.simps)
apply(auto)
done
theorem iter_no_next [simp] :
"\<lbrakk> check_annotations v c; venv_next_instruction v c = None \<rbrakk> \<Longrightarrow>
program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return (program_sem v c (Suc n) (Suc k))"
apply(subst program_sem.simps)
apply(auto)
done
theorem iter_inst_annotation [simp] :
"\<lbrakk> check_annotations v c; venv_next_instruction v c = Some i;
instruction_sem v c i = InstructionAnnotationFailure \<rbrakk> \<Longrightarrow>
program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return (program_sem v c (Suc n) (Suc k))"
apply(subst program_sem.simps)
apply(auto)
done
theorem iter_inst_to_world [simp] :
"\<lbrakk> check_annotations v c; venv_next_instruction v c = Some i;
instruction_sem v c i = InstructionToWorld a st bal pushed_v \<rbrakk> \<Longrightarrow>
program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return (program_sem v c (Suc n) (Suc k))"
apply(subst program_sem.simps)
apply(auto)
done
theorem iter_inst_continue1 [simp] :
"\<lbrakk> check_annotations v c; venv_next_instruction v c = Some i;
instruction_sem v c i = InstructionContinue new_v;
venv_pc v < venv_pc new_v;
\<forall>vv xx. (program_iter c (Continue vv n (Suc k)) steps =
Return xx \<longrightarrow>
program_iter c (Continue vv n (Suc k)) steps =
Return (program_sem vv c n (Suc k)));
program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return x \<rbrakk> \<Longrightarrow>
program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return (program_sem v c (Suc n) (Suc k))"
apply(subst program_sem.simps)
apply(auto)
apply(simp add: strict_if_def)
done
theorem iter_inst_continue2 [simp] :
"\<lbrakk> check_annotations v c; venv_next_instruction v c = Some i;
instruction_sem v c i = InstructionContinue new_v;
venv_pc v \<ge> venv_pc new_v;
\<forall>nn vv xx. (
program_iter c (Continue vv nn k) steps = Return xx \<longrightarrow>
program_iter c (Continue vv nn k) steps =
Return (program_sem vv c nn k));
program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) = Return x
\<rbrakk> \<Longrightarrow>
program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return (program_sem v c (Suc n) (Suc k))"
apply(subst program_sem.simps)
apply(auto)
apply(simp add: strict_if_def)
done
theorem iter_runout [simp] :
"program_iter c (Continue v n 0) (Suc steps) =
Return (program_sem v c n 0)"
apply(auto simp:program_sem.simps)
done
theorem step_foo : "\<exists>steps.
program_iter c s1 (Suc steps) = s2 \<Longrightarrow>
\<exists>steps. program_iter c s1 steps = s2"
apply(blast)
done
theorem iter2_inst_continue1 [simp] :
"\<lbrakk> check_annotations v c; venv_next_instruction v c = Some i;
instruction_sem v c i = InstructionContinue new_v;
venv_pc v < venv_pc new_v;
\<forall>vv. \<exists>steps. program_iter c (Continue vv n (Suc k)) steps =
Return (program_sem vv c n (Suc k))\<rbrakk> \<Longrightarrow>
\<exists>steps. program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return (program_sem v c (Suc n) (Suc k))"
apply(subst program_sem.simps)
apply(auto)
apply(simp add: strict_if_def)
done
theorem iter2_inst_continue2 [simp] :
"\<lbrakk> check_annotations v c; venv_next_instruction v c = Some i;
instruction_sem v c i = InstructionContinue new_v;
venv_pc v \<ge> venv_pc new_v;
\<forall>vv nn. \<exists>steps. program_iter c (Continue vv nn k) steps =
Return (program_sem vv c nn k)\<rbrakk> \<Longrightarrow>
\<exists>steps. program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return (program_sem v c (Suc n) (Suc k))"
apply(subst program_sem.simps)
apply(auto)
apply(simp add: strict_if_def)
done
theorem iter2_inst_continue [simp] :
"\<lbrakk> check_annotations v c; venv_next_instruction v c = Some i;
instruction_sem v c i = InstructionContinue new_v;
\<forall>vv. \<exists>steps. program_iter c (Continue vv n (Suc k)) steps =
Return (program_sem vv c n (Suc k));
\<forall>vv nn. \<exists>steps. program_iter c (Continue vv nn k) steps =
Return (program_sem vv c nn k)\<rbrakk> \<Longrightarrow>
\<exists>steps. program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return (program_sem v c (Suc n) (Suc k))"
apply(cases " venv_pc v < venv_pc new_v")
apply(rule iter2_inst_continue1)
apply(clarify)
apply(blast)
apply(blast)
apply(blast)
apply(blast)
apply(rule iter2_inst_continue2)
apply(blast)
apply(blast)
apply(blast)
apply(arith)
apply(blast)
done
declare program_iter.simps [simp del]
declare program_step.simps [simp del]
theorem iter_inst_continue :
"\<lbrakk> check_annotations v c; venv_next_instruction v c = Some i;
instruction_sem v c i = InstructionContinue new_v;
\<forall>vv xx. (program_iter c (Continue vv n (Suc k)) steps = Return xx \<longrightarrow>
program_iter c (Continue vv n (Suc k)) steps =
Return (program_sem vv c n (Suc k)));
\<forall>vv nn xx.
( program_iter c (Continue vv nn k) steps = Return xx \<longrightarrow>
program_iter c (Continue vv nn k) steps =
Return (program_sem vv c nn k) );
program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) = Return x\<rbrakk> \<Longrightarrow>
program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return (program_sem v c (Suc n) (Suc k))"
apply(cases " venv_pc v < venv_pc new_v")
apply(rule iter_inst_continue1)
apply(clarify)
apply(blast)
apply(blast)
apply(blast)
apply(blast)
apply(blast)
apply(rule iter_inst_continue2)
apply(blast)
apply(blast)
apply(blast)
apply(arith)
apply(blast)
apply(blast)
done
theorem iter_aux1 :
"\<lbrakk> check_annotations v c; venv_next_instruction v c = Some i;
\<forall>vv xx. (program_iter c (Continue vv n (Suc k)) steps = Return xx \<longrightarrow>
program_iter c (Continue vv n (Suc k)) steps =
Return (program_sem vv c n (Suc k)));
\<forall>vv nn xx.
( program_iter c (Continue vv nn k) steps = Return xx \<longrightarrow>
program_iter c (Continue vv nn k) steps =
Return (program_sem vv c nn k) );
program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) = Return x\<rbrakk> \<Longrightarrow>
program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return (program_sem v c (Suc n) (Suc k))"
apply(cases "instruction_sem v c i")
apply(rule iter_inst_continue)
apply(blast)
apply(blast)
apply(blast)
apply(blast)
apply(blast)
apply(blast)
apply(auto)
done
theorem iter2_aux1 [simp] :
"\<lbrakk> check_annotations v c; venv_next_instruction v c = Some i;
\<forall>vv. \<exists>steps. program_iter c (Continue vv n (Suc k)) steps =
Return (program_sem vv c n (Suc k));
\<forall>vv nn. \<exists>steps. program_iter c (Continue vv nn k) steps =
Return (program_sem vv c nn k)\<rbrakk> \<Longrightarrow>
\<exists>steps. program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return (program_sem v c (Suc n) (Suc k))"
apply(cases "instruction_sem v c i")
apply(rule iter2_inst_continue)
apply(blast)
apply(blast)
apply(blast)
apply(blast)
apply(blast)
apply(auto)
done
theorem iter_aux2 :
"\<lbrakk> check_annotations v c;
\<forall>vv xx. (program_iter c (Continue vv n (Suc k)) steps = Return xx \<longrightarrow>
program_iter c (Continue vv n (Suc k)) steps =
Return (program_sem vv c n (Suc k)));
\<forall>vv nn xx.
( program_iter c (Continue vv nn k) steps = Return xx \<longrightarrow>
program_iter c (Continue vv nn k) steps =
Return (program_sem vv c nn k) );
program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) = Return x\<rbrakk> \<Longrightarrow>
program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return (program_sem v c (Suc n) (Suc k))"
apply(cases "venv_next_instruction v c")
defer
apply(rule iter_aux1)
apply(auto)
done
theorem iter2_aux2 [simp] :
"\<lbrakk> check_annotations v c;
\<forall>vv. \<exists>steps. program_iter c (Continue vv n (Suc k)) steps =
Return (program_sem vv c n (Suc k));
\<forall>vv nn. \<exists>steps. program_iter c (Continue vv nn k) steps =
Return (program_sem vv c nn k)\<rbrakk> \<Longrightarrow>
\<exists>steps. program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return (program_sem v c (Suc n) (Suc k))"
apply(cases "venv_next_instruction v c")
defer
apply(rule iter2_aux1)
apply(auto)
done
theorem iter_aux3 :
"\<lbrakk> \<forall>vv xx. (program_iter c (Continue vv n (Suc k)) steps = Return xx \<longrightarrow>
program_iter c (Continue vv n (Suc k)) steps =
Return (program_sem vv c n (Suc k)));
\<forall>vv nn xx.
( program_iter c (Continue vv nn k) steps = Return xx \<longrightarrow>
program_iter c (Continue vv nn k) steps =
Return (program_sem vv c nn k) );
program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) = Return x\<rbrakk> \<Longrightarrow>
program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return (program_sem v c (Suc n) (Suc k))"
apply(cases "check_annotations v c")
apply(rule iter_aux2)
apply(auto)
done
theorem iter2_aux3 [simp] :
"\<lbrakk> \<forall>vv. \<exists>steps. program_iter c (Continue vv n (Suc k)) steps =
Return (program_sem vv c n (Suc k));
\<forall>vv nn. \<exists>steps. program_iter c (Continue vv nn k) steps =
Return (program_sem vv c nn k)\<rbrakk> \<Longrightarrow>
\<exists>steps. program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return (program_sem v c (Suc n) (Suc k))"
apply(cases "check_annotations v c")
apply(rule iter2_aux2)
apply(auto)
done
theorem iter2_aux4 [simp] :
"\<lbrakk> \<forall>vv. \<exists>steps. program_iter c (Continue vv n (Suc k)) steps =
Return (program_sem vv c n (Suc k));
\<forall>vv nn. \<exists>steps. program_iter c (Continue vv nn k) steps =
Return (program_sem vv c nn k)\<rbrakk> \<Longrightarrow>
\<exists>steps. program_iter c (Continue v (Suc n) (Suc k)) steps =
Return (program_sem v c (Suc n) (Suc k))"
apply(rule step_foo)
apply(rule iter2_aux3)
apply(auto)
done
definition iter_correct ::
"variable_env \<Rightarrow> constant_env \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
"iter_correct v c n k steps = (
\<forall> x. Return x = program_iter c (Continue v n k) steps \<longrightarrow>
x = program_sem v c n k)"
definition iter_correct2 ::
"variable_env \<Rightarrow> constant_env \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
"iter_correct2 v c n k steps = (
\<forall> x. program_iter c (Continue v n k) steps = Return x \<longrightarrow>
program_iter c (Continue v n k) steps =
Return (program_sem v c n k))"
theorem correct_same : "iter_correct v c n k steps = iter_correct2 v c n k steps"
apply(auto simp:iter_correct_def simp:iter_correct2_def)
done
theorem ummm :
"\<forall>vv. iter_correct2 vv c n (Suc k) steps \<Longrightarrow>
\<forall>vv nn. iter_correct2 vv c nn k steps \<Longrightarrow>
\<forall>x. program_iter c
(Continue v (Suc n) (Suc k))
(Suc steps) =
Return x \<Longrightarrow>
program_iter c
(Continue v (Suc n) (Suc k))
(Suc steps) =
Return (program_sem v c (Suc n) (Suc k))"
apply(rule iter_aux3)
apply(auto)
done
theorem lame : "Return x = Return y \<Longrightarrow> x = y"
apply(auto)
done
theorem lame2 :
"program_iter c
(Continue v (Suc n) (Suc k))
(Suc steps) =
Return x \<Longrightarrow>
program_iter c (Continue v (Suc n) (Suc k)) (Suc steps) =
Return (program_sem v c (Suc n) (Suc k)) \<Longrightarrow>
x = program_sem v c (Suc n) (Suc k)"
apply(auto)
done
theorem iter_aux4 :
"\<lbrakk> \<forall>vv. iter_correct vv c n (Suc k) steps;
\<forall>vv nn. iter_correct vv c nn k steps \<rbrakk> \<Longrightarrow>
iter_correct v c (Suc n) (Suc k) (Suc steps)"
apply(auto simp:correct_same)
apply(auto simp:iter_correct2_def)
apply(rule_tac steps = "steps" in lame2)
apply(blast)
apply(rule iter_aux3)
apply(auto)
done
theorem iter_nothing [simp] : "program_iter c st 0 = st"
apply(auto simp:program_iter.simps)
done
theorem blah1 [simp] : "Return x =
program_iter c (Continue v n 0) steps \<Longrightarrow>
program_sem v c n 0 = x"
apply(induction steps)
apply(auto)
done
theorem blah3 [simp] :
"(\<And>v n.
iter_correct v c n (Suc k) steps) \<Longrightarrow>
(\<And>v n x. iter_correct v c n k x) \<Longrightarrow>
iter_correct v c n (Suc k) (Suc steps)"
apply(induction n arbitrary: v)
apply(subst iter_correct_def)
apply(auto)
apply(rule iter_aux4)
apply(auto)
done
theorem blah2 [simp] :
"(\<And>v n x. iter_correct v c n k x) \<Longrightarrow>
iter_correct v c n (Suc k) steps"
apply(induction steps arbitrary: v n)
apply(subst iter_correct_def)
apply(auto)
done
theorem program_iter_bigstep :
"iter_correct v c n k steps"
(* Theorem: program_iter_bigstep*)(* try *)
apply(induction k arbitrary: v n steps)
apply(subst iter_correct_def)
apply(auto)
done
theorem iter_exists_aux [simp] :
"(\<And>v n.
\<exists>steps.
program_iter c (Continue v n k) steps =
Return (program_sem v c n k)) \<Longrightarrow>
\<exists>steps.
program_iter c (Continue v n (Suc k)) steps =
Return (program_sem v c n (Suc k))"
apply(induction n arbitrary:v k)
apply(rule_tac x = 1 in exI)
apply(simp add:program_iter.simps program_sem.simps program_step.simps)
apply(rule iter2_aux4)
defer
apply(blast)
apply(auto)
done
theorem iter_exists :
"\<exists>steps. program_iter c (Continue v n k) steps = Return (program_sem v c n k)"
apply(induction k arbitrary:v n)
apply(rule_tac x = 1 in exI)
apply(auto)
done
(*
value "size (0::256 word)"
definition zurp :: "256 word \<Rightarrow> 256 word" where
"zurp k = k"
theorem foo3 [simp] : "size (w::256 word) = 256"
apply (auto simp:word_size)
done
*)
lemma strict_if_True [simp] :
"strict_if True a b = a True"
apply(simp add: strict_if_def)
done
text {* When the if-condition is known to be False, the simplifier
can proceed into the else-clause. *}
lemma strict_if_False [simp] :
"strict_if False a b = b True"
apply(simp add: strict_if_def)
done
text {* When the if-condition is not known to be either True or False,
the simplifier is allowed to perform computation on the if-condition. *}
lemma strict_if_cong [cong] :
"b0 = b1 \<Longrightarrow> strict_if b0 x y = strict_if b1 x y"
apply(auto)
done
lemma unblock_program_sem [simp] : "blocked_program_sem v c l p True = program_sem v c l p"
apply(simp add: blocked_program_sem.psimps)
done
lemma program_sem_unblock :
"program_sem_blocked v c internal external True = program_sem v c internal external"
apply(simp add: program_sem_blocked_def)
done
theorem foo2 : "length ((word_rsplit (w::256 word)) :: 8 word list) = 32"
apply(rule length_word_rsplit_even_size)
apply(auto simp:word_size)
done
theorem list_elems : "length lst = Suc x \<Longrightarrow>
\<exists>b1 tl. lst = Cons b1 tl"
apply(induction lst)
apply(auto)
done
theorem list_elems1 : "length lst = 1 \<Longrightarrow> \<exists>b1. lst = [b1]"
apply(rule exE)
apply(rule list_elems)
apply(auto)
done
theorem list_elems2 : "length lst = 2 \<Longrightarrow> \<exists>b1 b2. lst = [b1,b2]"
apply(insert list_elems [of lst 1])
apply(auto)
apply(rule exE)
apply(rule list_elems)
apply(auto)
done
theorem list_elems3 : "length lst = 3 \<Longrightarrow> \<exists>b1 b2 b3. lst = [b1,b2,b3]"
apply(insert list_elems [of lst 2])
apply(auto)
apply(insert list_elems [of "drop 1 lst" 1])
apply(auto)
apply(insert list_elems [of "drop 2 lst" 0])
apply(auto)
done
theorem list_elems32 : "length lst = 32 \<Longrightarrow>
\<exists>b1 b2 b3 b4 b5 b6 b7 b8 b9 b10
b11 b12 b13 b14 b15 b16 b17 b18 b19 b20
b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 b32.
lst = [b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,
b11,b12,b13,b14,b15,b16,b17,b18,b19,b20,
b21,b22,b23,b24,b25,b26,b27,b28,b29,b30,b31,b32]"
apply(insert list_elems [of lst 31])
apply(auto)
apply(insert list_elems [of "drop 1 lst" 30])
apply(auto)
apply(insert list_elems [of "drop 2 lst" 29])
apply(auto)
apply(insert list_elems [of "drop 3 lst" 28])
apply(auto)
apply(insert list_elems [of "drop 4 lst" 27])
apply(auto)
apply(insert list_elems [of "drop 5 lst" 26])
apply(auto)
apply(insert list_elems [of "drop 6 lst" 25])
apply(auto)
apply(insert list_elems [of "drop 7 lst" 24])
apply(auto)
apply(insert list_elems [of "drop 8 lst" 23])
apply(auto)
apply(insert list_elems [of "drop 9 lst" 22])
apply(auto)
apply(insert list_elems [of "drop 10 lst" 21])
apply(auto)
apply(insert list_elems [of "drop 11 lst" 20])
apply(auto)
apply(insert list_elems [of "drop 12 lst" 19])
apply(auto)
apply(insert list_elems [of "drop 13 lst" 18])
apply(auto)
apply(insert list_elems [of "drop 14 lst" 17])
apply(auto)
apply(insert list_elems [of "drop 15 lst" 16])
apply(auto)
apply(insert list_elems [of "drop 16 lst" 15])
apply(auto)
apply(insert list_elems [of "drop 17 lst" 14])
apply(auto)
apply(insert list_elems [of "drop 18 lst" 13])
apply(auto)
apply(insert list_elems [of "drop 19 lst" 12])
apply(auto)
apply(insert list_elems [of "drop 20 lst" 11])
apply(auto)
apply(insert list_elems [of "drop 21 lst" 10])
apply(auto)
apply(insert list_elems [of "drop 22 lst" 9])
apply(auto)
apply(insert list_elems [of "drop 23 lst" 8])
apply(auto)
apply(insert list_elems [of "drop 24 lst" 7])
apply(auto)
apply(insert list_elems [of "drop 25 lst" 6])
apply(auto)
apply(insert list_elems [of "drop 26 lst" 5])
apply(auto)
apply(insert list_elems [of "drop 27 lst" 4])
apply(auto)
apply(insert list_elems [of "drop 28 lst" 3])
apply(auto)
apply(insert list_elems [of "drop 29 lst" 2])
apply(auto)
apply(insert list_elems [of "drop 30 lst" 1])
apply(auto)
apply(insert list_elems [of "drop 31 lst" 0])
apply(auto)
done
theorem word_elems32 : "\<exists>b1 b2 b3 b4 b5 b6 b7 b8 b9 b10
b11 b12 b13 b14 b15 b16 b17 b18 b19 b20
b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 b32.
(word_rsplit (w::256 word) :: 8 word list) =
[b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,
b11,b12,b13,b14,b15,b16,b17,b18,b19,b20,
b21,b22,b23,b24,b25,b26,b27,b28,b29,b30,b31,b32]"
apply(rule list_elems32)
apply(rule foo2)
done
fun get_foo :: "simple \<Rightarrow> 256 word" where
"get_foo (Compile.ImmedV x) = x"
| "get_foo (Compile.MemoryV x) = x"
| "get_foo (Compile.StorageV x) = x"
declare check_annotations_def [simp]
declare program_content_of_lst.simps [simp]
declare store_byte_list_in_program.simps [simp]
declare program_annotation_of_lst.simps [simp]
declare prepend_annotation_def [simp]
declare inst_size_def [simp]
declare inst_code.simps [simp]
declare stack_inst_code.simps [simp]
declare venv_next_instruction_def [simp]
declare instruction_sem.simps [simp]
declare stack_0_1_op_def [simp]
declare venv_advance_pc_def [simp]
declare build_aenv_def [simp]
declare jump_def [simp]
(* declare word_of_bytes_def [simp] *)
declare instruction_failure_result_def [simp]
declare build_venv_returned.simps [simp]
declare build_venv_failed_def [simp]
declare compile_simple.simps [simp]
declare get_simple.simps [simp]
declare get_stack_top.simps [simp]
declare eval_expr_def [simp]
declare stop_def [simp]
declare mload_def [simp]
declare general_dup_def [simp]
declare stack_1_1_op_def [simp]
theorem simple_correct :
"( eval_expr v addr (compile_simple expr) = get_simple v expr)"
(* Theorem: simple_correct*)(* try *)
apply(insert word_elems32 [of "get_foo expr"])
apply(induction expr)
apply(auto)
apply(subst foo)
apply(subst foo)
apply(subst program_sem.simps)
apply(auto simp:foo2)
apply(subst foo)
apply(subst program_sem.simps)
apply(auto simp:foo2)
apply (metis word_rcat_rsplit)
apply(subst foo)
apply(subst foo)
apply(subst program_sem.simps)
apply(auto simp:foo2)
apply(subst foo)
apply(subst program_sem.simps)
apply(auto simp:foo2)
apply(subst foo)
apply(subst program_sem.simps)
apply(auto simp:foo2)
apply (metis word_rcat_rsplit)
apply(subst foo)
apply(subst foo)
apply(subst program_sem.simps)
apply(auto simp:foo2)
apply(subst foo)
apply(subst program_sem.simps)
apply(auto simp:foo2)
apply(subst foo)
apply(subst program_sem.simps)
apply(auto simp:foo2)
apply (metis word_rcat_rsplit)
done
fun get_stack_top2 :: " program_state \<Rightarrow>( 256 word)option " where
" get_stack_top2 (Continue s _ _) = ( None )"
| " get_stack_top2 (Return a) = get_stack_top a"
definition make_prog :: "inst list \<Rightarrow> address \<Rightarrow> constant_env" where
"make_prog prog addr = (|
cenv_program = (program_of_lst (prog @ [Misc STOP])),
cenv_this = addr |)"
definition iter_expr :: "nat \<Rightarrow> variable_env \<Rightarrow> 160 word \<Rightarrow>(inst)list \<Rightarrow>( 256 word)option " where
"iter_expr x v addr prog =
get_stack_top2 (program_iter
(make_prog prog addr)
(Continue ( v (| venv_pc :=(( 0 :: nat)) |)) 0 0)
x)"
theorem iter_add :
"program_iter c (program_iter c st y) x = program_iter c st (x+y)"
apply(induction y arbitrary: st x)
apply(auto simp:program_iter.simps)
done
theorem iter_suc :
"program_iter c st (Suc x) = program_step c (program_iter c st x)"
apply(induction x arbitrary: st)
apply(auto simp:program_iter.simps)
done
theorem iter_return_stable :
"program_iter c st x = Return rt \<Longrightarrow>
program_iter c st (Suc x) = Return rt"
apply(induction x arbitrary:st)
apply(auto simp:program_iter.simps program_step.simps)
done
theorem last_iter_aux :
"(\<And>v a1 a2.
program_iter c (Continue v a1 a2) x =
Return rt \<Longrightarrow>
\<exists>y nv e1 e2.
program_iter c (Continue v a1 a2)
y =
Continue nv e1 e2 \<and>
program_step c
(Continue nv e1 e2) =
Return rt) \<Longrightarrow>
program_iter c (Continue v a1 a2)
(Suc x) =
Return rt \<Longrightarrow>
\<exists>y nv e1 e2.
program_iter c (Continue v a1 a2) y =
Continue nv e1 e2 \<and>
program_step c (Continue nv e1 e2) =
Return rt"
apply(cases " program_iter c (Continue v a1 a2) x")
apply(simp add:iter_suc)
apply(blast)
apply(simp add:iter_return_stable)
done
theorem last_iter :
"program_iter c (Continue v a1 a2) x = Return rt \<Longrightarrow>
\<exists>y nv e1 e2. program_iter c (Continue v a1 a2) y = Continue nv e1 e2 \<and>
program_step c (Continue nv e1 e2) = Return rt"
apply(induction x arbitrary: v a1 a2 )
apply(auto)
apply(rule last_iter_aux)
apply(auto)
done
fun maybe_eq :: "'a option \<Rightarrow> 'a option \<Rightarrow> bool" where
"maybe_eq (Some a) (Some b) = (a = b)"
| "maybe_eq _ _ = True"
theorem expr_stop_aux2 :
"program_sem (v\<lparr>venv_pc:=0\<rparr>) c 100 100 =
ProgramStepRunOut \<Longrightarrow>
get_stack_top (program_sem (v\<lparr>venv_pc:=0\<rparr>) c 100 100) = None"
apply(auto simp:make_prog_def)
done
declare program_sem.psimps [simp del]
theorem expr_stop_foo :
"\<lbrakk> program_sem (v\<lparr>venv_pc:=0\<rparr>) c 100 100 =
ProgramStepRunOut;
get_stack_top (program_sem (v\<lparr>venv_pc:=0\<rparr>) c 100 100) = Some x
\<rbrakk> \<Longrightarrow>
False"
apply(auto)
done
theorem expr_stop_aux3 :
"get_stack_top (ProgramToWorld x21 x22 x23 t) = Some x \<Longrightarrow>
\<exists>nv n k. t = Some (nv,n,k)"
apply(cases t)
apply(auto)
done
theorem expr_stop_aux :
"eval_expr v addr code = Some res \<Longrightarrow>
\<exists>act stor bal nv n k. program_sem (v\<lparr> venv_pc := 0\<rparr>) (make_prog code addr) 100 100 =
ProgramToWorld act stor bal (Some (nv, n, k))"
apply(simp add:make_prog_def)
apply(cases " program_sem (v\<lparr> venv_pc := 0\<rparr>) \<lparr>cenv_program =
\<lparr>program_content =
program_content_of_lst 0
(code @ [Misc STOP]),
program_length = Suc (length code),
program_annotation =
program_annotation_of_lst 0
(code @ [Misc STOP])\<rparr>,
cenv_this = addr\<rparr> 100 100")
apply(auto)
apply(auto simp:expr_stop_aux3)
done
theorem expr_stop_aux11 :
"\<exists>act stor bal nv n k. (eval_expr v addr code = Some res \<longrightarrow>
program_sem (v\<lparr> venv_pc := 0\<rparr>) (make_prog code addr) 100 100 =
ProgramToWorld act stor bal (Some (nv, n, k)))"
apply(auto simp:expr_stop_aux)
done
theorem iter_exists_foo :
"program_sem v c n k = rt \<Longrightarrow>
\<exists>x. program_iter c (Continue v n k) x = Return rt"
apply(auto simp:iter_exists)
done
theorem iter_exists_foo2 :
"program_sem v c n k =
ProgramToWorld act stor bal (Some (nv, n2, k2)) \<Longrightarrow>
\<exists>x. program_iter c (Continue v n k) x =
Return (ProgramToWorld act stor bal (Some (nv, n2, k2)))"
apply(auto simp:iter_exists_foo)
done
theorem iter_exists_foo3 :
"\<exists>x. program_iter c (Continue v n k) x =
Return (ProgramToWorld act stor bal (Some (nv, n2, k2)))
\<Longrightarrow> \<exists>act stor bal nv n2 k2 x. program_iter c (Continue v n k) x =
Return (ProgramToWorld act stor bal (Some (nv, n2, k2)))"
apply(blast)
done
theorem iter_exists_foo4 :
"program_sem v c n k =
ProgramToWorld act stor bal (Some (nv, n2, k2)) \<Longrightarrow>
\<exists>act stor bal nv n2 k2 x. program_iter c (Continue v n k) x =
Return (ProgramToWorld act stor bal (Some (nv, n2, k2)))"
apply(rule iter_exists_foo3)
apply(rule iter_exists_foo2)
apply(blast)
done
theorem iter_exists_foo5 :
"(\<exists>act stor bal nv n2 k2 x. program_sem v c n k =
ProgramToWorld act stor bal (Some (nv, n2, k2))) \<longrightarrow>
(\<exists>act stor bal nv n2 k2 x. program_iter c (Continue v n k) x =
Return (ProgramToWorld act stor bal (Some (nv, n2, k2))))"
apply(auto simp:iter_exists_foo4)
done
declare expr_stop_aux [simp]
theorem expr_stop_aux4 :
"eval_expr v addr (compile_expr expr) = Some res \<Longrightarrow>
\<exists>act stor bal nv n k x.
program_iter (make_prog (compile_expr expr) addr)
(Continue (v\<lparr>venv_pc:=0\<rparr>) 100 100) x =
Return (ProgramToWorld act stor bal (Some (nv, n, k)))"
apply(auto simp:iter_exists_foo5)
done
fun simple_inst :: "inst \<Rightarrow> bool" where
"simple_inst (Misc STOP) = False"
| "simple_inst (Misc RETURN) = False"
| "simple_inst (Misc CALL) = False"
| "simple_inst (Misc CREATE) = False"
| "simple_inst (Misc CALLCODE) = False"
| "simple_inst (Misc SUICIDE) = False"
| "simple_inst (Misc DELEGATECALL) = False"
| "simple_inst _ = True"
theorem compiled_simple_aux1 :
"xa \<in> set (compile_simple x) \<Longrightarrow> simple_inst xa"
apply(cases x)
apply(auto)
done
theorem compiled_simple_aux2 :
"x \<in> set (binop_inst x1a) \<Longrightarrow> simple_inst x"
apply(cases x1a)
apply(auto simp:binop_inst.simps)
done
theorem compiled_simple_aux3 :
"x \<in> set (unop_inst x1a) \<Longrightarrow> simple_inst x"
apply(cases x1a)
apply(auto simp:unop_inst.simps)
done
(* Compiled instructions are simple *)
theorem compiled_simple :
"x \<in> set (compile_expr expr) \<Longrightarrow> simple_inst x"
apply(induction expr arbitrary:x)
apply(auto simp: compiled_simple_aux1 compiled_simple_aux2 compiled_simple_aux3)
done
(* Simple instructions do not return normally *)
fun will_return :: "inst option \<Rightarrow> bool" where
"will_return (Some x) = (\<not> simple_inst x)"
| "will_return None = False"
theorem no_inst_error : "venv_next_instruction v c = None \<Longrightarrow>
program_step c (Continue v n k) \<noteq>
Return (ProgramToWorld act stor bal (Some (nv, e1, e2)))"
apply(auto simp:program_step.simps)
apply(cases k)
apply(auto)
apply(cases n)
apply(simp)
apply(cases "\<not> check_annotations v c")
apply(simp)
apply(cases "check_annotations v c")
defer
apply(blast)
apply (metis lame nat.distinct(1) option.simps(4) program_result.distinct(1) venv_next_instruction_def)
done
theorem name_1 :
"check_annotations v c \<Longrightarrow> (\<not> check_annotations v c) = False"
apply(blast)
done
declare check_annotations_def [simp del]
theorem blahblah [simp] :
"stack_2_1_op v c x \<noteq>
InstructionToWorld act stor bal (Some (nv, n, k))"
apply(auto simp:stack_2_1_op_def)
apply(cases "venv_stack v")
apply(auto)
apply(cases "tl (venv_stack v)")
apply(auto)
done
theorem blahblah2 [simp] :
"stack_1_1_op v c x \<noteq>
InstructionToWorld act stor bal (Some (nv, n, k))"
apply(auto simp:stack_2_1_op_def)
apply(cases "venv_stack v")
apply(auto)
done
theorem blahblah3 [simp] :
"stack_3_1_op v c x \<noteq>
InstructionToWorld act stor bal (Some (nv, n, k))"
apply(auto simp:stack_3_1_op_def)
apply(cases "venv_stack v")
apply(auto)
apply(cases "tl (venv_stack v)")
apply(auto)
apply(cases "tl (tl (venv_stack v))")
apply(auto)
done
theorem no_return_bits :
"instruction_sem v c (Bits x2) \<noteq>
InstructionToWorld act stor bal (Some (nv,n,k))"
apply(cases x2)
apply(auto)
apply(cases "venv_stack v")
apply(auto)
done
theorem no_return_sarith :
"instruction_sem v c (Sarith x2) \<noteq>
InstructionToWorld act stor bal (Some (nv,n,k))"
apply(cases x2)
apply(auto)