-
Notifications
You must be signed in to change notification settings - Fork 0
/
CHERI_Instantiation.thy
6287 lines (5438 loc) · 265 KB
/
CHERI_Instantiation.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
theory CHERI_Instantiation
imports
"Sail-Morello.Morello_lemmas"
"Sail-T-CHERI.Cheri_axioms_lemmas"
"Sail.Sail2_operators_mwords_lemmas"
"Sail.Sail2_values_lemmas"
"HOL-Library.Monad_Syntax"
"Sail-T-CHERI.Word_Extra"
"Sail-T-CHERI.Recognising_Automata"
"Word_Lib.Norm_Words"
"Sail-T-CHERI.BW2"
"New_CVC4"
"State_Invariants"
begin
no_notation Sail2_prompt_monad.bind (infixr "\<bind>" 54)
no_notation Sail2_prompt_monad_lemmas.seq (infixr "\<then>" 54)
adhoc_overloading bind Sail2_prompt_monad.bind
section \<open>General lemmas\<close>
lemma pow2_power[simp]: "pow2 n = 2 ^ nat n"
by (auto simp: pow2_def pow_def)
lemma un_ui_lt:
"(unat x < unat y) \<longleftrightarrow> (uint x < uint y)"
unfolding unat_def nat_less_eq_zless[OF uint_ge_0] ..
declare unat_add_lem[THEN iffD1, simp]
declare unat_mult_lem[THEN iffD1, simp]
lemma bitU_of_bool_simps[simp]:
"bitU_of_bool True = B1"
"bitU_of_bool False = B0"
by (auto simp: bitU_of_bool_def)
lemma of_bits_method_vec_of_bits_maybe[simp]:
"of_bits_method BC_mword = vec_of_bits_maybe"
by (auto simp: BC_mword_defs vec_of_bits_maybe_def)
lemma or_boolM_return_True[simp]: "or_boolM (return True) m = return True"
by (auto simp: or_boolM_def)
lemma and_boolM_assoc:
"and_boolM (and_boolM m1 m2) m3 = and_boolM m1 (and_boolM m2 m3)"
by (auto intro: bind_cong simp: and_boolM_def)
lemma or_boolM_assoc:
"or_boolM (or_boolM m1 m2) m3 = or_boolM m1 (or_boolM m2 m3)"
by (auto intro: bind_cong simp: or_boolM_def)
lemma if_then_let_unfold[simp]:
"(if c then let x = y in f x else z) = (if c then f y else z)"
by auto
lemma Run_if_then_return[simp]:
"Run (if c then return x else m) t a \<longleftrightarrow> (c \<and> t = [] \<and> a = x \<or> \<not>c \<and> Run m t a)"
by auto
lemma Run_bind_return[simp]:
"Run (m \<bind> (\<lambda>a. return (f a))) t a \<longleftrightarrow> (\<exists>a'. Run m t a' \<and> a = f a')"
by (auto elim!: Run_bindE intro: Traces_bindI[of m t _ _ "[]", simplified])
lemma Run_bind_iff:
"Run (m \<bind> f) t a \<longleftrightarrow> (\<exists>t1 t2 a1. t = t1 @ t2 \<and> Run m t1 a1 \<and> Run (f a1) t2 a)"
by (auto elim!: Run_bindE intro: Traces_bindI)
lemma Run_and_boolM_True_iff:
"Run (and_boolM m1 m2) t True \<longleftrightarrow> (\<exists>t1 t2. t = t1 @ t2 \<and> Run m1 t1 True \<and> Run m2 t2 True)"
by (auto simp: and_boolM_def Run_bind_iff)
lemma Run_if_iff:
"Run (if c then m1 else m2) t a \<longleftrightarrow> (c \<and> Run m1 t a \<or> \<not>c \<and> Run m2 t a)"
by auto
lemma Run_if_then_throw_iff[simp]:
"Run (if c then throw e else m) t a \<longleftrightarrow> \<not>c \<and> Run m t a"
by auto
lemma Run_bind_assert_exp_iff[simp]:
"Run (assert_exp c msg \<bind> f) t a \<longleftrightarrow> c \<and> Run (f ()) t a"
by (auto elim: Run_bindE)
lemma Run_write_regE:
assumes "Run (write_reg r v) t a"
obtains "t = [E_write_reg (name r) (regval_of r v)]"
using assms
by (auto simp: write_reg_def elim: Traces_cases)
lemma concat_take_chunks_eq:
"n > 0 \<Longrightarrow> List.concat (take_chunks n xs) = xs"
by (induction n xs rule: take_chunks.induct) auto
lemma bits_of_mem_bytes_of_word_to_bl:
"bits_of_mem_bytes (mem_bytes_of_word w) = map bitU_of_bool (to_bl w)"
unfolding bits_of_mem_bytes_def mem_bytes_of_word_def bits_of_bytes_def
by (auto simp add: concat_take_chunks_eq simp del: take_chunks.simps)
lemma uint_leq2pm1[intro]:
fixes w :: "'a::len word"
assumes "n \<ge> 2^LENGTH('a) - 1"
shows "uint w \<le> n"
using assms dual_order.trans zle_diff1_eq by blast
lemma test_bit_of_bl_append:
fixes x y :: "bool list"
defines "w \<equiv> of_bl (x @ y) :: 'a::len word"
shows "w !! n =
(if n \<ge> LENGTH('a) \<or> n \<ge> length x + length y then False else
if n < length y then rev y ! n else
rev x ! (n - length y))"
unfolding w_def
by (auto simp: test_bit_of_bl nth_append)
lemma update_subrange_vec_dec_test_bit:
fixes w :: "'a::len word" and w' :: "'b::len word"
assumes "0 \<le> j" and "j \<le> i" and "nat i < LENGTH('a)" and "LENGTH('b) = nat (i - j + 1)"
shows "update_subrange_vec_dec w i j w' !! n =
(if nat j > n \<or> n > nat i then w !! n else w' !! (n - nat j))"
(is "?lhs = ?rhs")
proof -
note [simp] = update_subrange_vec_dec_update_subrange_list_dec
update_subrange_list_dec_drop_take
nat_add_distrib nat_diff_distrib
consider (Low) "nat j > n" | (Mid) "nat j \<le> n \<and> n \<le> nat i" | (High) "n > nat i"
by linarith
then show ?thesis
proof cases
case Low
then show ?thesis
using assms
by (auto simp: test_bit_of_bl nth_append rev_nth test_bit_bl)
next
case Mid
then show ?thesis
using assms
by (auto simp: test_bit_of_bl_append nth_append less_diff_conv2 test_bit_bl[of w' "n - nat j"])
next
case High
then show ?thesis
using assms
by (auto simp: test_bit_of_bl_append nth_rev test_bit_bl[of w n])
qed
qed
lemma slice_update_subrange_vec_dec_above:
fixes w :: "'a::len word" and w' :: "'b::len word"
assumes "0 \<le> j" and "j \<le> i" and "nat i < LENGTH('a)" and "LENGTH('b) = nat (i - j + 1)"
and "nat j \<ge> n + LENGTH('c)"
shows "Word.slice n (update_subrange_vec_dec w i j w') = (Word.slice n w :: 'c::len word)"
using assms
by (intro word_eqI)
(auto simp: update_subrange_vec_dec_update_subrange_list_dec update_subrange_list_dec_drop_take
nth_slice test_bit_of_bl nat_add_distrib nat_diff_distrib nth_append rev_nth to_bl_nth)
lemma slice_update_subrange_vec_dec_below:
fixes w :: "'a::len word" and w' :: "'b::len word"
assumes "0 \<le> j" and "j \<le> i" and "nat i < LENGTH('a)" and "LENGTH('b) = nat (i - j + 1)"
and "n > nat i"
shows "Word.slice n (update_subrange_vec_dec w i j w') = (Word.slice n w :: 'c::len word)"
using assms
by (intro word_eqI)
(auto simp: update_subrange_vec_dec_update_subrange_list_dec update_subrange_list_dec_drop_take
nth_slice test_bit_of_bl_append nth_rev nat_add_distrib nat_diff_distrib test_bit_bl[of w "n' + n" for n'])
lemma update_subrange_vec_dec_word_cat_cap_pair:
fixes tmp :: "256 word" and c1 c2 :: "128 word"
shows "update_subrange_vec_dec (update_subrange_vec_dec tmp 127 0 c2) 255 128 c1 = (word_cat c1 c2 :: 256 word)"
by (intro word_eqI) (auto simp: test_bit_cat update_subrange_vec_dec_test_bit)
lemmas slice_128_cat_cap_pair = slice_cat1[where a = c1 and b = c2 for c1 c2 :: "128 word", simplified]
lemma slice_set_bit_above:
assumes "n' \<ge> n + LENGTH('a)"
shows "Word.slice n (set_bit w n' b) = (Word.slice n w :: 'a::len word)"
using assms
by (intro word_eqI) (auto simp: nth_slice test_bit_set_gen)
lemma slice_set_bit_below:
assumes "n' < n"
shows "Word.slice n (set_bit w n' b) = (Word.slice n w :: 'a::len word)"
using assms
by (intro word_eqI) (auto simp: nth_slice test_bit_set_gen)
lemma of_bl_0th[simp]: "(of_bl [b] :: 1 word) !! 0 = b"
by (auto simp: test_bit_of_bl)
definition aligned :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
"aligned addr sz \<equiv> sz dvd addr"
lemma aligned_dvd_trans:
assumes "aligned addr sz" and "sz' dvd sz"
shows "aligned addr sz'"
using assms
by (auto simp: aligned_def)
lemma aligned32_16[intro, simp]:
"aligned addr 32 \<Longrightarrow> aligned addr 16"
by (simp add: aligned_dvd_trans)
lemma aligned_add_size_iff[simp]:
"aligned (addr + sz) sz \<longleftrightarrow> aligned addr sz"
by (auto simp: aligned_def)
lemma unat_le_unat_add_iff:
fixes x y :: "'a::len word"
shows "unat x \<le> unat (x + y) \<longleftrightarrow> unat x + unat y < 2^LENGTH('a)"
using no_olen_add_nat word_le_nat_alt by blast
lemmas unat_lt2p64[simp, intro] = unat_lt2p[of w for w :: "64 word", simplified]
lemma aligned_unat_plus_distrib:
fixes addr offset :: "'a::len word"
assumes "aligned (unat addr) sz" and "unat offset < sz" and "sz dvd 2^LENGTH('a)"
shows "unat (addr + offset) = unat addr + unat offset"
proof -
obtain k k' where k: "unat addr = sz * k" and k': "2^LENGTH('a) = sz * k'"
using assms
by (auto simp: dvd_def aligned_def)
then have "k < k'" and "k' > 0"
using unat_lt2p[of addr]
by auto
have "sz * k + unat offset < sz * (Suc k)"
using \<open>unat offset < sz\<close>
by auto
also have "\<dots> \<le> sz * k'"
using \<open>k < k'\<close>
unfolding less_eq_Suc_le
by (intro mult_le_mono2)
finally show ?thesis
unfolding unat_plus_if' k k'
by auto
qed
lemma integer_subrange_word_of_int[simp]:
assumes "sz \<ge> 0" and "LENGTH('a) = Suc (nat sz)"
shows "(integer_subrange i sz 0 :: 'a::len word) = word_of_int i"
using assms
by (auto simp: integer_subrange_def of_bl_bin_word_of_int)
lemma unat_word_of_int[simp]:
"unat (word_of_int i :: 'a::len word) = nat (i mod 2^LENGTH('a))"
by (auto simp: unat_def uint_word_of_int)
lemma unat_add_word_of_int_l2p_distrib:
fixes w :: "'a::len word"
assumes "uint w + i < 2^LENGTH('a)" and "i \<ge> 0"
shows "unat (w + word_of_int i) = unat w + nat i"
using assms
by (metis add_increasing nat_add_distrib uint_ge_0 unat_def wi_hom_add word_of_int_inverse word_uint.Rep_inverse)
lemma unat_add_l2p_distrib:
fixes w :: "'a::len word"
assumes "uint w + uint i < 2^LENGTH('a)"
shows "unat (w + i) = unat w + unat i"
using assms
using no_olen_add unat_plus_simple
by auto
lemma leq_bools_to_bl_iff:
fixes x y :: "'a::len word"
shows "leq_bools (to_bl x) (to_bl y) \<longleftrightarrow> (\<forall>n. x !! n \<longrightarrow> y !! n)"
proof
assume leq: "leq_bools (to_bl x) (to_bl y)"
show "\<forall>n. x !! n \<longrightarrow> y !! n"
proof
fix n
have "to_bl x ! (size x - Suc n) \<longrightarrow> to_bl y ! (size y - Suc n)"
using leq
unfolding leq_bools_iff
by auto
then show "x !! n \<longrightarrow> y !! n"
by (cases "n < LENGTH('a)") (auto simp: to_bl_nth dest: test_bit_len)
qed
next
assume "\<forall>n. x !! n \<longrightarrow> y !! n"
then show "leq_bools (to_bl x) (to_bl y)"
unfolding leq_bools_iff
by (auto simp: to_bl_nth)
qed
lemma AND_NOT_eq_0_iff:
fixes x y :: "'a::len word"
shows "(x AND NOT y = 0) \<longleftrightarrow> (\<forall>n. x !! n \<longrightarrow> y !! n)"
by (auto simp: word_eq_iff word_ops_nth_size intro: test_bit_len)
context Cap_Axiom_Automaton
begin
lemma read_memt_bytes_accessed_mem_cap:
assumes "Run (read_memt_bytes BCa BCb rk addr sz) t (bytes, tag)"
and "cap_of_mem_bytes_method CC bytes tag = Some c"
and "\<forall>addr'. nat_of_bv BCa addr = Some addr' \<longrightarrow> \<not>is_translation_event ISA (E_read_memt rk addr' (nat sz) (bytes, tag))"
shows "accessed_mem_cap_of_trace_if_tagged c t"
using assms
unfolding read_memt_bytes_def accessed_mem_cap_of_trace_if_tagged_def
by (auto simp: derivable_caps_def maybe_fail_def accessed_caps_def
split: option.splits intro: derivable.Copy
elim!: Run_bindE Traces_cases[of "Read_memt _ _ _ _"])
lemma Run_bindE':
fixes m :: "('rv, 'b, 'e) monad" and a :: 'a
assumes "Run (bind m f) t a"
and "\<And>tm am tf. t = tm @ tf \<Longrightarrow> Run m tm am \<Longrightarrow> Run (f am) tf a \<Longrightarrow> P (tm @ tf)"
shows "P t"
using assms
by (auto elim: Run_bindE)
lemmas Run_case_prodE = case_prodE2[where Q = "\<lambda>m. Run m t a" and R = thesis for t a thesis]
declare Run_case_prodE[where thesis = "c \<in> derivable_caps s" and a = c for c s, derivable_caps_combinators]
declare Run_case_prodE[where thesis = "fst a \<in> derivable_caps s" and a = a for a s, derivable_caps_combinators]
declare Run_case_prodE[where thesis = "snd a \<in> derivable_caps s" and a = a for a s, derivable_caps_combinators]
lemma prod_snd_derivable_caps[derivable_capsE]:
assumes "a = (x, y)"
and "snd a \<in> derivable_caps s"
shows "y \<in> derivable_caps s"
using assms
by auto
lemma prod_fst_derivable_caps[derivable_capsE]:
assumes "a = (x, y)"
and "fst a \<in> derivable_caps s"
shows "x \<in> derivable_caps s"
using assms
by auto
lemma return_prod_snd_derivable_caps[derivable_capsE]:
assumes "Run (return (x, y)) t a"
and "y \<in> derivable_caps s"
shows "snd a \<in> derivable_caps s"
using assms
by auto
lemma return_prod_fst_derivable_caps[derivable_capsE]:
assumes "Run (return (x, y)) t a"
and "x \<in> derivable_caps s"
shows "fst a \<in> derivable_caps s"
using assms
by auto
text \<open>For the proofs of some of the decode clauses, some fairly simple side conditions need to be
proved, but the auto proof method struggles in some cases due to the nesting of blocks and use
of mutable variables, so we declare some custom proof rules so that these conditions can be
handled efficiently by the @{method derivable_capsI} proof method.\<close>
lemma member_fst_snd_prod_elims[derivable_capsE]:
"\<And>a x y xs. a = (x, y) \<Longrightarrow> fst a \<in> xs \<Longrightarrow> x \<in> xs"
"\<And>a x y xs. a = (x, y) \<Longrightarrow> snd a \<in> xs \<Longrightarrow> y \<in> xs"
"\<And>a x y xs. a = (x, y) \<Longrightarrow> fst (snd a) \<in> xs \<Longrightarrow> fst y \<in> xs"
"\<And>a x y xs. a = (x, y) \<Longrightarrow> fst (snd (snd a)) \<in> xs \<Longrightarrow> fst (snd y) \<in> xs"
"\<And>a x y xs. a = (x, y) \<Longrightarrow> fst (snd (snd (snd a))) \<in> xs \<Longrightarrow> fst (snd (snd y)) \<in> xs"
"\<And>a x y xs. a = (x, y) \<Longrightarrow> snd (snd a) \<in> xs \<Longrightarrow> snd y \<in> xs"
"\<And>a x y xs. a = (x, y) \<Longrightarrow> snd (snd (snd a)) \<in> xs \<Longrightarrow> snd (snd y) \<in> xs"
"\<And>a x y xs. a = (x, y) \<Longrightarrow> snd (snd (snd (snd a))) \<in> xs \<Longrightarrow> snd (snd (snd y)) \<in> xs"
by auto
lemma return_prods_derivable[derivable_capsE]:
"\<And>a b x xs. Run (return (a, b)) t x \<Longrightarrow> a \<in> xs \<Longrightarrow> fst x \<in> xs"
"\<And>a b x xs. Run (return (a, b)) t x \<Longrightarrow> b \<in> xs \<Longrightarrow> snd x \<in> xs"
"\<And>a b c x xs. Run (return (a, b, c)) t x \<Longrightarrow> b \<in> xs \<Longrightarrow> fst (snd x) \<in> xs"
"\<And>a b c x xs. Run (return (a, b, c)) t x \<Longrightarrow> c \<in> xs \<Longrightarrow> snd (snd x) \<in> xs"
"\<And>a b c d e x xs. Run (return (a, b, c, d, e)) t x \<Longrightarrow> d \<in> xs \<Longrightarrow> fst (snd (snd (snd x))) \<in> xs"
by auto
declare Run_bindE[where thesis = "fst (snd (snd (snd a))) \<in> xs" and a = a for a xs, derivable_caps_combinators]
declare Run_bindE[where thesis = "snd (snd a) \<in> xs" and a = a for a xs, derivable_caps_combinators]
declare Run_ifE[where thesis = "fst (snd (snd (snd a))) \<in> xs" and a = a for a xs, derivable_caps_combinators]
declare Run_ifE[where thesis = "snd (snd a) \<in> xs" and a = a for a xs, derivable_caps_combinators]
declare Run_letE[where thesis = "fst (snd (snd (snd a))) \<in> xs" and a = a for a xs, derivable_caps_combinators]
declare Run_letE[where thesis = "snd (snd a) \<in> xs" and a = a for a xs, derivable_caps_combinators]
declare Run_case_prodE[where thesis = "fst (snd (snd (snd a))) \<in> xs" and a = a for a xs, derivable_caps_combinators]
declare Run_case_prodE[where thesis = "snd (snd a) \<in> xs" and a = a for a xs, derivable_caps_combinators]
lemmas Run_int_set_member_combinators[derivable_caps_combinators] =
Run_bindE[where thesis = "a \<in> insert x xs" and a = a for a x :: int and xs :: "int set"]
Run_ifE[where thesis = "a \<in> insert x xs" and a = a for a x :: int and xs :: "int set"]
Run_letE[where thesis = "a \<in> insert x xs" and a = a for a x :: int and xs :: "int set"]
lemma Run_return_resultE:
assumes "Run (return x) t a"
and "a = x \<Longrightarrow> P x"
shows "P a"
using assms
by auto
declare Run_return_resultE[where P = "\<lambda>a. a \<in> xs" for xs, derivable_capsE]
end
section \<open>Simplification rules\<close>
lemma Zeros_0[simp]:
"Zeros n = 0"
by (auto simp: Zeros_def zeros_def)
lemma Ones_max_word[simp]:
"Ones n = max_word"
by (auto simp: Ones_def sail_ones_def zeros_def)
declare id0_def[simp]
declare eq_bits_int_def[simp]
declare CAPABILITY_DBITS_def[simp]
declare CAPABILITY_DBYTES_def[simp]
declare zero_extend_def[simp]
lemmas cap_bit_index_defs[simp] =
CAP_TAG_BIT_def CAP_IE_BIT_def
CAP_VALUE_HI_BIT_def CAP_VALUE_LO_BIT_def
CAP_PERMS_LO_BIT_def CAP_PERMS_HI_BIT_def
CAP_OTYPE_LO_BIT_def CAP_OTYPE_HI_BIT_def
CAP_BASE_LO_BIT_def CAP_BASE_HI_BIT_def
CAP_LIMIT_LO_BIT_def CAP_LIMIT_HI_BIT_def
CAP_BASE_MANTISSA_LO_BIT_def CAP_LIMIT_MANTISSA_LO_BIT_def
CAP_FLAGS_HI_BIT_def CAP_FLAGS_LO_BIT_def
lemmas special_otype_defs[simp] =
CAP_SEAL_TYPE_RB_def CAP_SEAL_TYPE_LPB_def CAP_SEAL_TYPE_LB_def
CAP_MAX_FIXED_SEAL_TYPE_def
lemma ZeroExtend1_ucast[simp]:
"ZeroExtend1 n w = ucast w"
by (auto simp: ZeroExtend1_def)
lemma DataFromCapability_tag_ucast[simp]:
"DataFromCapability 128 c = (of_bl [c !! 128], ucast c)"
by (auto simp: DataFromCapability_def)
definition Capability_of_tag_word :: "bool \<Rightarrow> 128 word \<Rightarrow> Capability" where
"Capability_of_tag_word tag word =
(let tag = (of_bl [tag] :: 1 word) in
word_cat tag word)"
lemma Capability_of_tag_word_id[simp]:
fixes c :: Capability
shows "Capability_of_tag_word (c !! 128) (ucast c) = c" (is "?c' = c")
proof (intro word_eqI impI)
fix n
assume "n < size ?c'"
then show "?c' !! n = c !! n"
unfolding Capability_of_tag_word_def
by (cases "n = 128") (auto simp: nth_word_cat nth_ucast test_bit_of_bl)
qed
lemma Capability_of_tag_word_128th[simp]:
"Capability_of_tag_word tag data !! 128 = tag"
by (auto simp: Capability_of_tag_word_def nth_word_cat test_bit_of_bl)
lemma update_bits_tag_Capability_from_tag_word[simp]:
"update_vec_dec (update_subrange_vec_dec c 127 0 cap_bits) 128 (bitU_of_bool tag)
= Capability_of_tag_word tag cap_bits"
unfolding Capability_of_tag_word_def
by (cases tag; intro word_eqI)
(auto simp: test_bit_set_gen update_subrange_vec_dec_test_bit nth_word_cat nth_ucast
dest: test_bit_len)
lemma nat_of_bv_mword_unat[simp]: "nat_of_bv BC_mword w = Some (unat w)"
by (auto simp: nat_of_bv_def unat_def)
lemma Bit_bitU_of_bool[simp]: "Morello.Bit w = bitU_of_bool (w !! 0)"
by (auto simp: Morello.Bit_def)
lemma CapIsTagSet_128th[simp]:
"CapIsTagSet c \<longleftrightarrow> c !! 128"
by (auto simp: CapIsTagSet_def CapGetTag_def nth_ucast test_bit_of_bl)
lemma CapSetTag_set_128th[simp]:
"CapSetTag c t = set_bit c 128 (t !! 0)"
by (cases "t !! 0") (auto simp: CapSetTag_def)
lemma CapIsTagSet_CapSetTag_iff[simp]:
"CapIsTagSet (CapSetTag c t) \<longleftrightarrow> (t !! 0)"
by (auto simp: test_bit_set)
lemma CapWithTagClear_128th[simp]:
"CapWithTagClear c !! 128 = False"
by (auto simp: CapWithTagClear_def test_bit_set)
lemma CapIsTagSet_CapWithTagSet_eq:
assumes "CapIsTagSet c"
shows "CapWithTagSet c = c"
using assms
by (intro word_eqI) (auto simp: CapWithTagSet_def test_bit_set_gen)
lemma CapIsTagClear_iff_not_128th[simp]:
"CapIsTagClear c \<longleftrightarrow> \<not>CapIsTagSet c"
by (auto simp: CapIsTagClear_def CapGetTag_def nth_ucast test_bit_of_bl)
lemma CapGetPermissions_set_0th[simp]:
"CapGetPermissions (set_bit c 0 b) = CapGetPermissions c"
by (intro word_eqI) (auto simp: CapGetPermissions_def nth_slice test_bit_set_gen)
lemma CapGetPermissions_CapSetFlags_eq[simp]:
"CapGetPermissions (CapSetFlags c flags) = CapGetPermissions c"
by (intro word_eqI)
(auto simp: CapGetPermissions_def CapSetFlags_def nth_slice slice_update_subrange_vec_dec_below)
lemma CapGetObjectType_CapSetObjectType_and_mask:
"CapGetObjectType (CapSetObjectType c otype) = (otype AND mask (nat CAP_OTYPE_HI_BIT - nat CAP_OTYPE_LO_BIT + 1))"
unfolding CapGetObjectType_def CapSetObjectType_def
by (intro word_eqI)
(auto simp: word_ao_nth nth_slice nth_ucast update_subrange_vec_dec_test_bit)
lemma CapGetObjectType_CapUnseal_0[simp]:
"CapGetObjectType (CapUnseal c) = 0"
by (auto simp: CapUnseal_def CapGetObjectType_CapSetObjectType_and_mask)
lemma CapSetObjectType_128th_iff[simp]:
"CapSetObjectType c otype !! 128 \<longleftrightarrow> c !! 128"
unfolding CapSetObjectType_def
by (auto simp: update_subrange_vec_dec_test_bit)
lemma CapUnseal_128th_iff[simp]:
"CapUnseal c !! 128 = c !! 128"
by (auto simp: CapUnseal_def)
lemma clear_perms_128th_iff[simp]:
"CapClearPerms c perms !! 128 \<longleftrightarrow> c !! 128"
by (auto simp: CapClearPerms_def update_subrange_vec_dec_test_bit)
lemma CapGetObjectType_CapClearPerms[simp]:
"CapGetObjectType (CapClearPerms c perms) = CapGetObjectType c"
by (auto simp: CapClearPerms_def CapGetObjectType_def slice_update_subrange_vec_dec_above)
lemma CapIsSealed_CapClearPerms_iff[simp]:
"CapIsSealed (CapClearPerms c perms) \<longleftrightarrow> CapIsSealed c"
by (auto simp: CapIsSealed_def)
lemma CapSetFlags_128th_iff[simp]:
"CapSetFlags c flags !! 128 = c !! 128"
by (auto simp: CapSetFlags_def update_subrange_vec_dec_test_bit)
lemma CapUnseal_not_sealed[simp]:
"\<not>CapIsSealed (CapUnseal c)"
by (auto simp: CapIsSealed_def CapUnseal_def CapGetObjectType_CapSetObjectType_and_mask)
lemma CMAX_not_sealed[simp]: "\<not>CapIsSealed CMAX"
by (auto simp: CMAX_def CapIsSealed_def CapGetObjectType_def)
lemma CapUnsignedGreaterThan_iff_unat_gt[simp]:
"CapUnsignedGreaterThan x y \<longleftrightarrow> unat x > unat y"
unfolding unat_def nat_less_eq_zless[OF uint_ge_0]
by (auto simp: CapUnsignedGreaterThan_def)
lemma CapUnsignedGreaterThanOrEqual_iff_unat_geq[simp]:
"CapUnsignedGreaterThanOrEqual x y \<longleftrightarrow> unat x \<ge> unat y"
by (auto simp: CapUnsignedGreaterThanOrEqual_def unat_def nat_le_eq_zle)
lemma CapUnsignedLessThan_iff_unat_lt[simp]:
"CapUnsignedLessThan x y \<longleftrightarrow> unat x < unat y"
unfolding unat_def nat_less_eq_zless[OF uint_ge_0]
by (auto simp: CapUnsignedLessThan_def)
lemma CapUnsignedLessThanOrEqual_iff_unat_leq[simp]:
"CapUnsignedLessThanOrEqual x y \<longleftrightarrow> unat x \<le> unat y"
by (auto simp: CapUnsignedLessThanOrEqual_def unat_def nat_le_eq_zle)
lemma CapGetObjectType_set_bit_128_eq[simp]:
"CapGetObjectType (set_bit c 128 tag) = CapGetObjectType c"
unfolding CapGetObjectType_def CAP_OTYPE_LO_BIT_def
by (intro word_eqI) (auto simp: word_ao_nth nth_slice test_bit_set_gen)
lemma CapGetObjectType_update_address[simp]:
fixes addr :: "64 word"
shows "CapGetObjectType (update_subrange_vec_dec c 63 0 addr) = CapGetObjectType c"
unfolding CapGetObjectType_def
by (intro word_eqI) (auto simp: word_ao_nth nth_slice update_subrange_vec_dec_test_bit)
lemma CapAdd_GetObjectType_eq:
assumes "Run (CapAdd c increment) t c'"
shows "CapGetObjectType c' = CapGetObjectType c"
using assms
unfolding CapAdd_def
by (auto elim!: Run_letE Run_bindE)
lemma CapAdd_CapIsSealed_iff[simp]:
assumes "Run (CapAdd c increment) t c'"
shows "CapIsSealed c' \<longleftrightarrow> CapIsSealed c"
using assms
by (auto simp: CapIsSealed_def CapAdd_GetObjectType_eq)
lemma CapAdd__1_CapIsSealed_iff[simp]:
assumes "Run (CapAdd__1 c increment) t c'"
shows "CapIsSealed c' \<longleftrightarrow> CapIsSealed c"
using assms
by (auto simp: CapAdd__1_def)
lemma Run_CapAdd_tag_imp:
assumes "Run (CapAdd c offset) t c'"
and "c' !! 128"
shows "c !! 128"
using assms
unfolding CapAdd_def CAP_VALUE_HI_BIT_def CAP_VALUE_LO_BIT_def
by (auto simp: test_bit_set update_subrange_vec_dec_test_bit
elim!: Run_bindE Run_letE split: if_splits)
lemma CapGetPermissions_CapWithTagSet_eq[simp]:
"CapGetPermissions (CapWithTagSet c) = CapGetPermissions c"
unfolding CapGetPermissions_def CapWithTagSet_def
by (intro word_eqI) (auto simp: nth_slice test_bit_set_gen)
lemma CapGetObjectType_CapWithTagSet_eq[simp]:
"CapGetObjectType (CapWithTagSet c) = CapGetObjectType c"
unfolding CapGetObjectType_def CapWithTagSet_def CapGetObjectType_def
by (intro word_eqI) (auto simp: word_ao_nth nth_slice test_bit_set_gen)
lemma CapIsSealed_CapWithTagSet_iff[simp]:
"CapIsSealed (CapWithTagSet c) \<longleftrightarrow> CapIsSealed c"
unfolding CapIsSealed_def
by auto
lemma CapGetObjectType_CapSetFlags_eq[simp]:
"CapGetObjectType (CapSetFlags c flags) = CapGetObjectType c"
by (intro word_eqI)
(auto simp: CapGetObjectType_def CapSetFlags_def word_ao_nth slice_update_subrange_vec_dec_below)
lemma CapIsSealed_CapSetFlags_iff[simp]:
"CapIsSealed (CapSetFlags c flags) = CapIsSealed c"
by (auto simp: CapIsSealed_def)
lemma Run_BranchAddr_not_CapIsSealed_if:
assumes "Run (BranchAddr c el) t c'"
and "CapIsTagSet c'"
shows "\<not>CapIsSealed c'"
using assms
unfolding BranchAddr_def
by (auto elim!: Run_bindE Run_letE Run_ifE split: if_splits)
lemma CapGetObjectType_set_bit_0_eq[simp]:
"CapGetObjectType (set_bit c 0 b) = CapGetObjectType c"
by (intro word_eqI)
(auto simp: CapGetObjectType_def word_ao_nth nth_slice test_bit_set_gen)
lemma CapIsSealed_set_bit_0_iff[simp]:
"CapIsSealed (set_bit c 0 b) = CapIsSealed c"
by (auto simp: CapIsSealed_def)
(*lemma no_Run_EndOfInstruction[simp]:
"Run (EndOfInstruction u) t a \<longleftrightarrow> False"
by (auto simp: EndOfInstruction_def)
lemma no_Run_AArch64_TakeException[simp]:
"Run (AArch64_TakeException target_el exception preferred_exception_return vect_offset) t a \<longleftrightarrow> False"
unfolding AArch64_TakeException_def bind_assoc
by (auto elim!: Run_bindE)
lemma no_Run_AArch64_DataAbort[simp]:
"Run (AArch64_DataAbort vaddress fault) t a \<longleftrightarrow> False"
by (auto simp: AArch64_DataAbort_def elim!: Run_bindE Run_ifE)
lemma no_Run_AArch64_InstructionAbort[simp]:
"Run (AArch64_InstructionAbort vaddress fault) t a \<longleftrightarrow> False"
by (auto simp: AArch64_InstructionAbort_def elim!: Run_bindE Run_ifE)
lemma no_Run_AArch64_WatchpointException[simp]:
"Run (AArch64_WatchpointException vaddress fault) t a \<longleftrightarrow> False"
by (auto simp: AArch64_WatchpointException_def elim!: Run_bindE Run_ifE)
lemma no_Run_AArch64_BreakpointException[simp]:
"Run (AArch64_BreakpointException fault) t a \<longleftrightarrow> False"
by (auto simp: AArch64_BreakpointException_def elim!: Run_bindE Run_ifE)
lemma no_Run_AArch64_Abort[simp]:
"Run (AArch64_Abort vaddress fault) t a \<longleftrightarrow> False"
by (auto simp: AArch64_Abort_def elim!: Run_bindE Run_ifE)
lemma no_Run_AArch64_SystemAccessTrap[simp]:
"Run (AArch64_SystemAccessTrap target_el ec) t a \<longleftrightarrow> False"
by (auto simp: AArch64_SystemAccessTrap_def elim!: Run_bindE Run_ifE)
lemma no_Run_CapabilityAccessTrap[simp]:
"Run (CapabilityAccessTrap target_el) t a \<longleftrightarrow> False"
by (auto simp: CapabilityAccessTrap_def elim!: Run_bindE Run_ifE)
lemma no_Run_Unreachable[simp]:
"Run (Unreachable u) t a \<longleftrightarrow> False"
by (auto simp: Unreachable_def elim!: Run_bindE)*)
lemma EL_exhaust_disj:
fixes el :: "2 word"
shows "el = EL0 \<or> el = EL1 \<or> el = EL2 \<or> el = EL3"
by (cases el rule: exhaustive_2_word) (auto simp: EL0_def EL1_def EL2_def EL3_def)
lemma Run_if_ELs_cases:
assumes "Run (if el = EL0 then m0 else if el = EL1 then m1 else if el = EL2 then m2 else if el = EL3 then m3 else mu) t a"
obtains (EL0) "el = EL0" and "Run m0 t a"
| (EL1) "el = EL1" and "Run m1 t a"
| (EL2) "el = EL2" and "Run m2 t a"
| (EL3) "el = EL3" and "Run m3 t a"
using assms
by (cases el rule: exhaustive_2_word; auto simp: EL0_def EL1_def EL2_def EL3_def)
lemma unat_paddress_plus_distrib[simp]:
fixes w :: "48 word"
assumes offset: "unat offset < 2^63"
shows "unat (ucast w + offset :: 64 word) = unat w + unat offset"
proof -
have "unat w + unat offset < 2^64"
using add_strict_mono[OF unat_lt2p[of w] offset]
by auto
then show ?thesis
by (auto simp: unat_plus_if_size)
qed
declare HaveAArch32EL_def[simp]
(*lemma HaveAArch32EL_False[simp]:
"HaveAArch32EL el = False"
unfolding HaveAArch32EL_def HaveAnyAArch32_def HaveEL_def
unfolding EL0_def EL1_def EL2_def EL3_def
by (cases el rule: exhaustive_2_word) (auto elim: Run_bindE)*)
lemma ELUsingAArch32_False:
shows "\<not>Run (ELUsingAArch32 el) t True"
unfolding ELUsingAArch32_def ELStateUsingAArch32_def ELStateUsingAArch32K_def
by (auto elim!: Run_bindE)
lemma UsingAArch32_False[simp]:
shows "\<not>Run (UsingAArch32 ()) t True"
by (auto simp: UsingAArch32_def HaveAnyAArch32_def elim!: Run_elims)
lemma AddrTop_63_or_55:
assumes "Run (AddrTop address el) t b"
shows "b = 63 \<or> b = 55"
using assms
unfolding AddrTop_def
by (auto elim!: Run_bindE simp: ELUsingAArch32_False)
lemmas datatype_splits =
ArchVersion.split Constraint.split Unpredictable.split Exception.split InstrEnc.split
BranchType.split Fault.split AccType.split DeviceType.split MemType.split
MBReqDomain.split MBReqTypes.split PrefetchHint.split
FPExc.split FPRounding.split FPType.split
CountOp.split ExtendType.split FPMaxMinOp.split FPUnaryOp.split FPConvOp.split
MoveWideOp.split ShiftType.split LogicalOp.split MemOp.split MemAtomicOp.split
SystemHintOp.split PSTATEField.split VBitOp.split
CompareOp.split ImmediateOp.split ReduceOp.split
section \<open>Capabilities\<close>
definition is_sentry :: "Capability \<Rightarrow> bool" where
"is_sentry c \<equiv> CapGetObjectType c = CAP_SEAL_TYPE_RB"
definition is_indirect_sentry :: "Capability \<Rightarrow> bool" where
"is_indirect_sentry c \<equiv> CapGetObjectType c \<in> {CAP_SEAL_TYPE_LB, CAP_SEAL_TYPE_LPB}"
definition get_base :: "Capability \<Rightarrow> nat" where
"get_base c \<equiv> unat (THE b. \<exists>t. Run (CapGetBase c) t b)"
definition get_limit :: "Capability \<Rightarrow> nat" where
"get_limit c \<equiv> unat (THE l. \<exists>t b v. Run (CapGetBounds c) t (b, l, v))"
definition get_perms :: "Capability \<Rightarrow> perms" where
"get_perms c = to_bl (CapGetPermissions c)"
definition set_tag :: "Capability \<Rightarrow> bool \<Rightarrow> Capability" where
"set_tag c tag = CapSetTag c (if tag then 1 else 0)"
definition seal :: "Capability \<Rightarrow> nat \<Rightarrow> Capability" where
"seal c obj_type = CapSetObjectType c (of_nat obj_type)"
definition cap_of_mem_bytes :: "memory_byte list \<Rightarrow> bitU \<Rightarrow> Capability option" where
"cap_of_mem_bytes bytes tag =
do {
(bytes' :: 128 word) \<leftarrow> vec_of_bits_maybe (bits_of_mem_bytes bytes);
(tag' :: bool) \<leftarrow> bool_of_bitU tag;
let (tag'' :: 1 word) = of_bl [tag'];
Some (word_cat tag'' bytes')
}"
abbreviation "cap_permits p c \<equiv> CapCheckPermissions c p"
abbreviation "clear_perm p c \<equiv> CapClearPerms c p"
definition "CC \<equiv>
\<lparr>is_tagged_method = CapIsTagSet,
is_sealed_method = CapIsSealed,
is_sentry_method = is_sentry,
is_indirect_sentry_method = is_indirect_sentry,
get_base_method = get_base,
get_top_method = get_limit,
get_obj_type_method = (\<lambda>c. unat (CapGetObjectType c)),
get_perms_method = get_perms,
get_cursor_method = (\<lambda>c. unat (CapGetValue c)),
is_global_method = (\<lambda>c. \<not>(CapIsLocal c)),
seal_method = seal,
unseal_method = CapUnseal,
clear_global_method = (clear_perm CAP_PERM_GLOBAL),
cap_of_mem_bytes_method = cap_of_mem_bytes,
permits_execute_method = CapIsExecutePermitted,
permits_ccall_method = (cap_permits CAP_PERM_BRANCH_SEALED_PAIR),
permits_load_method = (cap_permits CAP_PERM_LOAD),
permits_load_cap_method = (cap_permits CAP_PERM_LOAD_CAP),
permits_seal_method = (cap_permits CAP_PERM_SEAL),
permits_store_method = (cap_permits CAP_PERM_STORE),
permits_store_cap_method = (cap_permits CAP_PERM_STORE_CAP),
permits_store_local_cap_method = (cap_permits CAP_PERM_STORE_LOCAL),
permits_system_access_method = CapIsSystemAccessPermitted,
permits_unseal_method = (cap_permits CAP_PERM_UNSEAL)\<rparr>"
interpretation Capabilities CC
proof
fix c obj_type
show "is_tagged_method CC (seal_method CC c obj_type) = is_tagged_method CC c"
by (auto simp: CC_def seal_def)
next
fix c tag
show "is_tagged_method CC (unseal_method CC c) = is_tagged_method CC c"
by (auto simp: CC_def set_tag_def test_bit_set)
show "is_tagged_method CC (clear_global_method CC c) = is_tagged_method CC c"
by (auto simp: CC_def set_tag_def test_bit_set)
next
fix c bytes tag
have test_128_128: "w !! 128 \<longleftrightarrow> False" for w :: "128 word"
by (auto dest: test_bit_len)
assume "cap_of_mem_bytes_method CC bytes tag = Some c"
then show "is_tagged_method CC c = (tag = B1)"
by (cases tag)
(auto simp: CC_def cap_of_mem_bytes_def bind_eq_Some_conv nth_ucast test_bit_cat test_128_128)
qed
lemma CC_simps[simp]:
"is_tagged_method CC c = CapIsTagSet c"
"is_sealed_method CC c = CapIsSealed c"
"is_sentry_method CC c = is_sentry c"
"is_indirect_sentry_method CC c = is_indirect_sentry c"
"seal_method CC c otype = seal c otype"
"unseal_method CC c = CapUnseal c"
"get_cursor_method CC c = unat (CapGetValue c)"
"get_base_method CC c = get_base c"
"get_top_method CC c = get_limit c"
"get_obj_type_method CC c = unat (CapGetObjectType c)"
"cap_of_mem_bytes_method CC = cap_of_mem_bytes"
"permits_execute_method CC c = cap_permits CAP_PERM_EXECUTE c"
"permits_ccall_method CC c = cap_permits CAP_PERM_BRANCH_SEALED_PAIR c"
"permits_load_method CC c = cap_permits CAP_PERM_LOAD c"
"permits_load_cap_method CC c = cap_permits CAP_PERM_LOAD_CAP c"
"permits_seal_method CC c = cap_permits CAP_PERM_SEAL c"
"permits_store_method CC c = cap_permits CAP_PERM_STORE c"
"permits_store_cap_method CC c = cap_permits CAP_PERM_STORE_CAP c"
"permits_store_local_cap_method CC c = cap_permits CAP_PERM_STORE_LOCAL c"
"permits_unseal_method CC c = cap_permits CAP_PERM_UNSEAL c"
"permits_system_access_method CC c = CapIsSystemAccessPermitted c"
"get_perms_method CC c = to_bl (CapGetPermissions c)"
"is_global_method CC c = cap_permits CAP_PERM_GLOBAL c"
"clear_global_method CC c = clear_perm CAP_PERM_GLOBAL c"
by (auto simp: CC_def CapIsExecutePermitted_def get_perms_def CapIsLocal_def)
abbreviation "RV_class \<equiv> instance_Sail2_values_Register_Value_Morello_types_register_value_dict"
lemmas RV_class_def = instance_Sail2_values_Register_Value_Morello_types_register_value_dict_def
lemma cap_of_mem_bytes_of_word_Capability_of_tag_word:
fixes data :: "'a::len word"
assumes "LENGTH('a) = 128"
shows "cap_of_mem_bytes (mem_bytes_of_word data) (bitU_of_bool tag) = Some (Capability_of_tag_word tag (ucast data))"
unfolding Capability_of_tag_word_def cap_of_mem_bytes_def
by (auto simp: bind_eq_Some_conv bits_of_mem_bytes_of_word_to_bl ucast_bl)
lemma cap_of_mem_bytes_of_word_B1_Capability_of_tag_word:
fixes data :: "'a::len word"
assumes "LENGTH('a) = 128"
shows "cap_of_mem_bytes (mem_bytes_of_word data) B1 = Some (Capability_of_tag_word True (ucast data))"
using cap_of_mem_bytes_of_word_Capability_of_tag_word[of data True, OF assms]
by (auto simp: CC_def)
text \<open>Proofs that a monadic function essentially encodes a pure function\<close>
definition
monad_return_rel :: "('rv, 'a, 'e) monad \<Rightarrow> ('rv, 'a, 'e) monad \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
where
"monad_return_rel m m' P = (\<forall> t t' x x'. Run m t x \<and> Run m' t' x' \<longrightarrow> P x x')"
lemmas monad_return_relD = monad_return_rel_def[THEN iffD1, unfolded imp_conjL, rule_format]
definition
monad_result_of :: "('rv, 'a, 'e) monad \<Rightarrow> 'a"
where
"monad_result_of m = (THE v. \<exists>t. Run m t v)"
lemma monad_result_of_eq:
"monad_return_rel m m (=) \<Longrightarrow> Run m t x \<Longrightarrow> monad_result_of m = x"
apply (simp add: monad_result_of_def)
apply (rule the_equality)
apply (auto elim: monad_return_relD)
done
lemma monad_return_rel_bind:
"monad_return_rel f f' P \<Longrightarrow> (\<And>x x'. P x x' \<Longrightarrow> monad_return_rel (g x) (g' x') Q)
\<Longrightarrow> monad_return_rel (bind f g) (bind f' g') Q"
apply (subst monad_return_rel_def, clarsimp elim!: Run_bindE)
apply (drule(2) monad_return_relD)
apply (elim meta_allE, drule(1) meta_mp)
apply (erule(2) monad_return_relD)
done
lemma monad_return_rel_if:
"G = G' \<Longrightarrow> monad_return_rel f f' P \<Longrightarrow> monad_return_rel g g' P
\<Longrightarrow> monad_return_rel (If G f g) (If G' f' g') P"
by simp
lemma monad_return_rel_return:
"P x y \<Longrightarrow> monad_return_rel (return x) (return y) P"
by (clarsimp simp: monad_return_rel_def)
lemma monad_return_rel_triv:
"monad_return_rel f g (\<lambda> x x'. True)"
by (clarsimp simp: monad_return_rel_def)
definition
eq_at_bits :: "nat set \<Rightarrow> ('a :: len0) word \<Rightarrow> 'a word \<Rightarrow> bool"
where
"eq_at_bits ns x y = (\<forall>i \<in> ns. i < size x \<longrightarrow> test_bit x i = test_bit y i)"
lemma monad_return_rel_undefined:
"monad_return_rel (undefined_bitvector BC RV i) (undefined_bitvector BC RV j) (eq_at_bits {})"
by (simp add: monad_return_rel_def eq_at_bits_def)
lemmas monad_return_rel_assert_exp_triv =
monad_return_rel_triv[where f="assert_exp P str" and g="assert_exp Q str'" for str str' P Q]
lemma monad_return_rel_assert_exp_P:
"monad_return_rel (assert_exp P str) (assert_exp P str') (\<lambda>_ _. P)"
by (clarsimp simp: monad_return_rel_def)
lemma monad_return_rel_let_same_forget:
"(\<And>x. monad_return_rel (g x) (g' x) Q)
\<Longrightarrow> monad_return_rel (Let x g) (Let x g') Q"
by simp
lemma monad_return_rel_let_rel:
"P x x' \<Longrightarrow> (\<And>x x'. P x x' \<Longrightarrow> monad_return_rel (g x) (g' x') Q)
\<Longrightarrow> monad_return_rel (Let x g) (Let x' g') Q"
by simp
lemma test_bit_word_update:
"j = i + size y - 1 \<Longrightarrow> j < size x \<Longrightarrow> 0 < size y \<Longrightarrow>
test_bit (word_update x i j y) k = (if i \<le> k \<and> k \<le> j then test_bit y (k - i) else test_bit x k)"
using test_bit_size[of x k] test_bit_size[of y "k - i"]
apply (simp add: word_update_def Let_def test_bit_of_bl nth_append)
apply (intro conjI impI iffI, simp_all add: nth_rev to_bl_nth rev_take)
apply (simp_all add: Suc_leI le_diff_conv2)
apply (auto simp: nth_rev to_bl_nth)
done
lemma test_bit_slice_mask:
"n = int (LENGTH ('a)) \<Longrightarrow> 0 \<le> i \<Longrightarrow> 0 \<le> l \<Longrightarrow>
test_bit (slice_mask n i l :: ('a :: len) word) j = (nat i \<le> j \<and> (j - nat i) < nat l \<and> j < nat n)"
apply (simp add: slice_mask_def word_ops_nth_size nth_shiftl sail_ones_def zeros_def)
apply (simp add: sail_mask_def nth_shiftl mask_def[simplified, symmetric])
apply (safe, simp_all)
done
lemma test_bit_above_size:
"n \<ge> size (x :: ('a :: len) word) \<Longrightarrow> \<not> test_bit x n"
by (auto dest!: test_bit_size)
lemma test_bit_vector_update_subrange_from_subrange:
assumes cs: "e1 \<le> s1 \<and> 0 \<le> e1 \<and> e2 \<le> s2 \<and> 0 \<le> e2"
shows "test_bit (vector_update_subrange_from_subrange n v1 s1 e1 v2 s2 e2) i
= (i < size v1 \<and> (nat e1 \<le> i \<and>
v2 !! (i - nat e1 + nat e2) \<and> i - nat e1 < nat (s2 - e2 + 1) \<and> i - nat e1 + nat e2 < size v2 \<and> i - nat e1 < size v1 \<or>
v1 !! i \<and> (nat e1 \<le> i \<longrightarrow> \<not> i - nat e1 < nat (s1 - e1 + 1))))"
using cs
apply (simp add: vector_update_subrange_from_subrange_def)
apply (cases "i < size v1", simp_all add: test_bit_above_size)
apply (simp add: word_ao_nth nth_shiftr nth_shiftl nth_ucast test_bit_slice_mask
word_ops_nth_size)
done
lemma CapGetTop_monad_return_rel:
"monad_return_rel (CapGetTop c) (CapGetTop c) (=)"
apply (clarsimp simp add: CapGetTop_def Let_def split del: if_split)
apply (intro monad_return_rel_if monad_return_rel_return
monad_return_rel_bind[OF monad_return_rel_undefined])
apply simp
done
lemma CapGetExponent_range:
"0 \<le> CapGetExponent c \<and> CapGetExponent c < 64"
by (clarsimp simp add: CapGetExponent_def uint_lt2p[THEN order_less_le_trans])
lemma eq_at_bits_set_slice_zeros_lemma:
assumes eq: "eq_at_bits S x x'"
and imp: "\<And>y y'. eq_at_bits (S \<union> {nat i ..< nat j}) y y' \<Longrightarrow> monad_return_rel (g y) (g' y') Q"
and extra: "n = int (size x)" "0 \<le> i" "0 \<le> j"
shows "monad_return_rel (Let (set_slice_zeros n x i j) g) (Let (set_slice_zeros n x' i j) g') Q"
using eq extra
apply simp
apply (rule imp)
apply (clarsimp simp: eq_at_bits_def set_slice_zeros_def word_ops_nth_size
test_bit_slice_mask)
apply auto
done
lemma eq_at_bits_word_update_lemma:
assumes eq: "eq_at_bits S x x'"
and imp: "\<And>y y'. eq_at_bits (S \<union> {nat i ..< nat j + 1}) y y' \<Longrightarrow> monad_return_rel (g y) (g' y') Q"
and extra: "j = i + size y - 1" "j < size x" "0 < size y"
shows "monad_return_rel (Let (word_update x i j y) g) (Let (word_update x' i j y) g') Q"
using eq extra