-
Notifications
You must be signed in to change notification settings - Fork 0
/
VSpace_R.thy
3687 lines (3385 loc) · 165 KB
/
VSpace_R.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
(*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*)
(*
ARM VSpace refinement
*)
theory VSpace_R
imports TcbAcc_R
begin
crunch_ignore (add: throw_on_false)
definition
"pd_at_asid' pd asid \<equiv> \<lambda>s. \<exists>ap pool.
armKSASIDTable (ksArchState s) (ucast (asid_high_bits_of asid)) = Some ap \<and>
ko_at' (ASIDPool pool) ap s \<and> pool (asid && mask asid_low_bits) = Some pd \<and>
page_directory_at' pd s"
defs checkPDASIDMapMembership_def:
"checkPDASIDMapMembership pd asids
\<equiv> stateAssert (\<lambda>s. pd \<notin> ran ((option_map snd o armKSASIDMap (ksArchState s) |` (- set asids)))) []"
crunch inv[wp]:checkPDAt P
lemma findPDForASID_pd_at_wp:
"\<lbrace>\<lambda>s. \<forall>pd. (page_directory_at' pd s \<longrightarrow> pd_at_asid' pd asid s)
\<longrightarrow> P pd s\<rbrace> findPDForASID asid \<lbrace>P\<rbrace>,-"
apply (simp add: findPDForASID_def assertE_def
cong: option.case_cong
split del: split_if)
apply (rule hoare_pre)
apply (wp getASID_wp | wpc | simp add: o_def split del: split_if)+
apply (clarsimp simp: pd_at_asid'_def)
apply (case_tac ko, simp)
apply (subst(asm) inv_f_f)
apply (rule inj_onI, simp+)
apply fastforce
done
lemma findPDForASIDAssert_pd_at_wp:
"\<lbrace>(\<lambda>s. \<forall>pd. pd_at_asid' pd asid s
\<and> pd \<notin> ran ((option_map snd o armKSASIDMap (ksArchState s) |` (- {asid})))
\<longrightarrow> P pd s)\<rbrace>
findPDForASIDAssert asid \<lbrace>P\<rbrace>"
apply (simp add: findPDForASIDAssert_def const_def
checkPDAt_def checkPDUniqueToASID_def
checkPDASIDMapMembership_def)
apply (rule hoare_pre, wp getPDE_wp findPDForASID_pd_at_wp)
apply simp
done
crunch inv[wp]: findPDForASIDAssert "P"
(simp: const_def crunch_simps wp: loadObject_default_inv crunch_wps)
lemma pspace_relation_pd:
assumes p: "pspace_relation (kheap a) (ksPSpace c)"
assumes pa: "pspace_aligned a"
assumes pad: "pspace_aligned' c" "pspace_distinct' c"
assumes t: "page_directory_at p a"
shows "page_directory_at' p c" using assms pd_aligned [OF pa t]
apply (clarsimp simp: obj_at_def)
apply (drule(1) pspace_relation_absD)
apply (clarsimp simp: a_type_def
split: Structures_A.kernel_object.split_asm
split_if_asm arch_kernel_obj.split_asm)
apply (clarsimp simp: page_directory_at'_def pdBits_def pageBits_def
typ_at_to_obj_at_arches)
apply (drule_tac x="ucast y" in spec, clarsimp)
apply (simp add: ucast_ucast_mask iffD2 [OF mask_eq_iff_w2p] word_size)
apply (clarsimp simp add: pde_relation_def)
apply (drule(2) aligned_distinct_pde_atI')
apply (erule obj_at'_weakenE)
apply simp
done
lemma find_pd_for_asid_eq_helper:
"\<lbrakk> pd_at_asid asid pd s; valid_arch_objs s;
asid \<noteq> 0; pspace_aligned s \<rbrakk>
\<Longrightarrow> find_pd_for_asid asid s = returnOk pd s
\<and> page_directory_at pd s \<and> is_aligned pd pdBits"
apply (clarsimp simp: pd_at_asid_def valid_arch_objs_def)
apply (frule spec, drule mp, erule exI)
apply (clarsimp simp: vs_asid_refs_def graph_of_def
elim!: vs_lookupE)
apply (erule rtranclE)
apply simp
apply (clarsimp dest!: vs_lookup1D)
apply (erule rtranclE)
defer
apply (drule vs_lookup1_trans_is_append')
apply (clarsimp dest!: vs_lookup1D)
apply (clarsimp dest!: vs_lookup1D)
apply (drule spec, drule mp, rule exI,
rule vs_lookupI[unfolded vs_asid_refs_def])
apply (rule image_eqI[OF refl])
apply (erule graph_ofI)
apply clarsimp
apply (rule rtrancl.intros(1))
apply (clarsimp simp: vs_refs_def graph_of_def
split: Structures_A.kernel_object.splits
arch_kernel_obj.splits)
apply (clarsimp simp: obj_at_def)
apply (drule bspec, erule ranI)
apply clarsimp
apply (drule ucast_up_inj, simp)
apply (simp add: find_pd_for_asid_def bind_assoc
word_neq_0_conv[symmetric] liftE_bindE)
apply (simp add: exec_gets liftE_bindE bind_assoc
get_asid_pool_def get_object_def)
apply (simp add: mask_asid_low_bits_ucast_ucast)
apply (drule ucast_up_inj, simp)
apply (clarsimp simp: returnOk_def get_pde_def
get_pd_def get_object_def
bind_assoc)
apply (frule(1) pspace_alignedD[where p=pd])
apply (simp add: pdBits_def pageBits_def)
done
lemma find_pd_for_asid_assert_eq:
"\<lbrakk> pd_at_asid asid pd s; valid_arch_objs s;
asid \<noteq> 0; pspace_aligned s \<rbrakk>
\<Longrightarrow> find_pd_for_asid_assert asid s = return pd s"
apply (drule(3) find_pd_for_asid_eq_helper)
apply (simp add: find_pd_for_asid_assert_def
catch_def bind_assoc)
apply (clarsimp simp: returnOk_def obj_at_def
a_type_def
cong: bind_apply_cong)
apply (clarsimp split: Structures_A.kernel_object.splits
arch_kernel_obj.splits split_if_asm)
apply (simp add: get_pde_def get_pd_def get_object_def
bind_assoc is_aligned_neg_mask_eq
pd_bits_def pdBits_def)
apply (simp add: exec_gets)
done
lemma find_pd_for_asid_valids:
"\<lbrace> pd_at_asid asid pd and valid_arch_objs
and pspace_aligned and K (asid \<noteq> 0) \<rbrace>
find_pd_for_asid asid \<lbrace>\<lambda>rv s. pde_at rv s\<rbrace>,-"
"\<lbrace> pd_at_asid asid pd and valid_arch_objs
and pspace_aligned and K (asid \<noteq> 0)
and K (is_aligned pd pdBits \<longrightarrow> P pd) \<rbrace>
find_pd_for_asid asid \<lbrace>\<lambda>rv s. P rv\<rbrace>,-"
"\<lbrace> pd_at_asid asid pd and valid_arch_objs
and pspace_aligned and K (asid \<noteq> 0)
and pd_at_uniq asid pd \<rbrace>
find_pd_for_asid asid \<lbrace>\<lambda>rv s. pd_at_uniq asid rv s\<rbrace>,-"
"\<lbrace> pd_at_asid asid pd and valid_arch_objs
and pspace_aligned and K (asid \<noteq> 0) \<rbrace>
find_pd_for_asid asid -,\<lbrace>\<bottom>\<bottom>\<rbrace>"
apply (simp_all add: validE_def validE_R_def validE_E_def
valid_def split: sum.split)
apply (auto simp: returnOk_def return_def
pde_at_def pd_bits_def pdBits_def
pageBits_def is_aligned_neg_mask_eq
dest!: find_pd_for_asid_eq_helper
elim!: is_aligned_weaken)
done
lemma valid_asid_map_inj_map:
"\<lbrakk> valid_asid_map s; (s, s') \<in> state_relation;
unique_table_refs (caps_of_state s);
valid_vs_lookup s; valid_arch_objs s;
valid_arch_state s; valid_global_objs s \<rbrakk>
\<Longrightarrow> inj_on (option_map snd \<circ> armKSASIDMap (ksArchState s'))
(dom (armKSASIDMap (ksArchState s')))"
apply (rule inj_onI)
apply (clarsimp simp: valid_asid_map_def state_relation_def
arch_state_relation_def)
apply (frule_tac c=x in subsetD, erule domI)
apply (frule_tac c=y in subsetD, erule domI)
apply (drule(1) bspec [rotated, OF graph_ofI])+
apply clarsimp
apply (erule(6) pd_at_asid_unique)
apply (simp add: mask_def)+
done
lemma asidBits_asid_bits[simp]:
"asidBits = asid_bits"
by (simp add: asid_bits_def asidBits_def
asidHighBits_def asid_low_bits_def)
lemma find_pd_for_asid_assert_corres:
"corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd)
(K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits)
and pspace_aligned and pspace_distinct
and valid_arch_objs and valid_asid_map
and pd_at_asid asid pd and pd_at_uniq asid pd)
(pspace_aligned' and pspace_distinct' and no_0_obj')
(find_pd_for_asid_assert asid)
(findPDForASIDAssert asid)"
apply (simp add: find_pd_for_asid_assert_def const_def
findPDForASIDAssert_def liftM_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply (rule_tac F="is_aligned pda pdBits
\<and> pda = pd" in corres_gen_asm)
apply (clarsimp simp add: is_aligned_mask[symmetric])
apply (rule_tac P="pde_at pd and pd_at_uniq asid pd
and pspace_aligned and pspace_distinct
and pd_at_asid asid pd and valid_asid_map"
and P'="pspace_aligned' and pspace_distinct'"
in stronger_corres_guard_imp)
apply (rule corres_symb_exec_l[where P="pde_at pd and pd_at_uniq asid pd
and valid_asid_map and pd_at_asid asid pd"])
apply (rule corres_symb_exec_r[where P'="page_directory_at' pd"])
apply (simp add: checkPDUniqueToASID_def ran_option_map
checkPDASIDMapMembership_def)
apply (rule_tac P'="pd_at_uniq asid pd" in corres_stateAssert_implied)
apply (simp add: gets_def bind_assoc[symmetric]
stateAssert_def[symmetric, where L="[]"])
apply (rule_tac P'="valid_asid_map and pd_at_asid asid pd"
in corres_stateAssert_implied)
apply (rule corres_trivial, simp)
apply (clarsimp simp: state_relation_def arch_state_relation_def
valid_asid_map_def
split: option.split)
apply (drule bspec, erule graph_ofI)
apply clarsimp
apply (drule(1) pd_at_asid_unique2)
apply simp
apply (clarsimp simp: state_relation_def arch_state_relation_def
pd_at_uniq_def ran_option_map)
apply wp
apply (simp add: checkPDAt_def stateAssert_def)
apply (rule no_fail_pre, wp)
apply simp
apply (clarsimp simp: pde_at_def obj_at_def a_type_def)
apply (clarsimp split: Structures_A.kernel_object.splits
arch_kernel_obj.splits split_if_asm)
apply (simp add: get_pde_def exs_valid_def bind_def return_def
get_pd_def get_object_def simpler_gets_def)
apply wp
apply simp
apply (simp add: get_pde_def get_pd_def)
apply (rule no_fail_pre)
apply (wp get_object_wp | wpc)+
apply (clarsimp simp: pde_at_def obj_at_def a_type_def)
apply (clarsimp split: Structures_A.kernel_object.splits
arch_kernel_obj.splits split_if_asm)
apply simp
apply (clarsimp simp: state_relation_def)
apply (erule(3) pspace_relation_pd)
apply (simp add: pde_at_def pd_bits_def pdBits_def
is_aligned_neg_mask_eq)
apply (rule corres_split_catch [OF _ find_pd_for_asid_corres'[where pd=pd]])
apply (rule_tac P="\<bottom>" and P'="\<top>" in corres_inst)
apply (simp add: corres_fail)
apply (wp find_pd_for_asid_valids[where pd=pd])
apply (clarsimp simp: word_neq_0_conv)
apply simp
done
lemma findPDForASIDAssert_known_corres:
"corres r P P' f (g pd) \<Longrightarrow>
corres r (pd_at_asid asid pd and pd_at_uniq asid pd
and valid_arch_objs and valid_asid_map
and pspace_aligned and pspace_distinct
and K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits) and P)
(P' and pspace_aligned' and pspace_distinct' and no_0_obj')
f (findPDForASIDAssert asid >>= g)"
apply (subst return_bind[symmetric])
apply (subst corres_cong [OF refl refl _ refl refl])
apply (rule bind_apply_cong [OF _ refl])
apply clarsimp
apply (erule(3) find_pd_for_asid_assert_eq[symmetric])
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ find_pd_for_asid_assert_corres[where pd=pd]])
apply simp
apply wp
apply clarsimp
apply simp
done
lemma load_hw_asid_corres:
"corres op =
(valid_arch_objs and pspace_distinct
and pspace_aligned and valid_asid_map
and pd_at_asid a pd
and (\<lambda>s. \<forall>pd. pd_at_asid a pd s \<longrightarrow> pd_at_uniq a pd s)
and K (a \<noteq> 0 \<and> a \<le> mask asid_bits))
(pspace_aligned' and pspace_distinct' and no_0_obj')
(load_hw_asid a) (loadHWASID a)"
apply (simp add: load_hw_asid_def loadHWASID_def)
apply (rule_tac r'="op =" in corres_split' [OF _ _ gets_sp gets_sp])
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (case_tac "rv' a")
apply simp
apply (rule corres_guard_imp)
apply (rule_tac pd=pd in findPDForASIDAssert_known_corres)
apply (rule corres_trivial, simp)
apply clarsimp
apply clarsimp
apply clarsimp
apply (rule corres_guard_imp)
apply (rule_tac pd=b in findPDForASIDAssert_known_corres)
apply (rule corres_trivial, simp)
apply (clarsimp simp: valid_arch_state_def valid_asid_map_def)
apply (drule subsetD, erule domI)
apply (drule bspec, erule graph_ofI)
apply clarsimp
apply simp
done
crunch inv[wp]: loadHWASID "P"
(wp: crunch_wps)
lemma store_hw_asid_corres:
"corres dc
(pd_at_asid a pd and pd_at_uniq a pd
and valid_arch_objs and pspace_distinct
and pspace_aligned and K (a \<noteq> 0 \<and> a \<le> mask asid_bits)
and valid_asid_map)
(pspace_aligned' and pspace_distinct' and no_0_obj')
(store_hw_asid a h) (storeHWASID a h)"
apply (simp add: store_hw_asid_def storeHWASID_def)
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ find_pd_for_asid_assert_corres[where pd=pd]])
apply (rule corres_split_eqr)
apply (rule corres_split)
prefer 2
apply (rule corres_trivial, rule corres_modify)
apply (clarsimp simp: state_relation_def)
apply (simp add: arch_state_relation_def)
apply (rule ext)
apply simp
apply (rule corres_split_eqr)
apply (rule corres_trivial, rule corres_modify)
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (rule ext)
apply simp
apply (rule corres_trivial)
apply (clarsimp simp: corres_gets state_relation_def
arch_state_relation_def)
apply ((wp | simp)+)[4]
apply (rule corres_trivial)
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (wp | simp)+
done
lemma invalidate_asid_corres:
"corres dc
(valid_asid_map and valid_arch_objs
and pspace_aligned and pspace_distinct
and pd_at_asid a pd and pd_at_uniq a pd
and K (a \<noteq> 0 \<and> a \<le> mask asid_bits))
(pspace_aligned' and pspace_distinct' and no_0_obj')
(invalidate_asid a) (invalidateASID a)"
(is "corres dc ?P ?P' ?f ?f'")
apply (simp add: invalidate_asid_def invalidateASID_def)
apply (rule corres_guard_imp)
apply (rule_tac pd=pd in findPDForASIDAssert_known_corres)
apply (rule_tac P="?P" and P'="?P'" in corres_inst)
apply (rule_tac r'="op =" in corres_split' [OF _ _ gets_sp gets_sp])
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (rule corres_modify)
apply (simp add: state_relation_def arch_state_relation_def
fun_upd_def)
apply simp
apply simp
done
lemma invalidate_asid_ext_corres:
"corres dc
(\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_arch_objs s
\<and> pspace_aligned s \<and> pspace_distinct s
\<and> pd_at_asid a pd s \<and> pd_at_uniq a pd s
\<and> a \<noteq> 0 \<and> a \<le> mask asid_bits)
(pspace_aligned' and pspace_distinct' and no_0_obj')
(invalidate_asid a) (invalidateASID a)"
apply (insert invalidate_asid_corres)
apply (clarsimp simp: corres_underlying_def)
apply fastforce
done
lemma invalidate_hw_asid_entry_corres:
"corres dc \<top> \<top> (invalidate_hw_asid_entry a) (invalidateHWASIDEntry a)"
apply (simp add: invalidate_hw_asid_entry_def invalidateHWASIDEntry_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply (rule corres_trivial, rule corres_modify)
defer
apply (rule corres_trivial)
apply (wp | clarsimp simp: state_relation_def arch_state_relation_def)+
apply (rule ext)
apply simp
done
lemma find_free_hw_asid_corres:
"corres (op =)
(valid_asid_map and valid_arch_objs
and pspace_aligned and pspace_distinct
and (unique_table_refs o caps_of_state)
and valid_vs_lookup and valid_arch_state
and valid_global_objs)
(pspace_aligned' and pspace_distinct' and no_0_obj')
find_free_hw_asid findFreeHWASID"
apply (simp add: find_free_hw_asid_def findFreeHWASID_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr [OF _ corres_trivial])
apply (rule corres_split_eqr [OF _ corres_trivial])
apply (subgoal_tac "take (length [minBound .e. maxBound :: hardware_asid])
([next_asid .e. maxBound] @ [minBound .e. next_asid])
= [next_asid .e. maxBound] @ init [minBound .e. next_asid]")
apply (cut_tac v="find (\<lambda>a. hw_asid_table a = None)
([next_asid .e. maxBound] @ init [minBound .e. next_asid])"
in option.nchotomy[rule_format])
apply (erule corres_disj_division)
apply (clarsimp split del: if_splits)
apply (rule corres_split [OF _ invalidate_asid_ext_corres])
apply (rule corres_split' [where r'=dc])
apply (rule corres_trivial, rule corres_machine_op)
apply (rule corres_no_failI)
apply (rule no_fail_invalidateTLB_ASID)
apply fastforce
apply (rule corres_split)
prefer 2
apply (rule invalidate_hw_asid_entry_corres)
apply (rule corres_split)
apply (rule corres_trivial)
apply simp
apply (rule corres_trivial)
apply (rule corres_modify)
apply (simp add: minBound_word maxBound_word
state_relation_def arch_state_relation_def)
apply (wp | simp split del: split_if)+
apply (rule corres_trivial, clarsimp)
apply (cut_tac x=next_asid in leq_maxBound)
apply (simp only: word_le_nat_alt)
apply (simp add: init_def upto_enum_word
minBound_word
del: upt.simps)
apply (wp | clarsimp simp: arch_state_relation_def state_relation_def)+
apply (clarsimp dest!: findNoneD)
apply (drule bspec, rule UnI1, simp, rule order_refl)
apply (clarsimp simp: valid_arch_state_def)
apply (frule(1) is_inv_SomeD)
apply (clarsimp simp: valid_asid_map_def)
apply (frule bspec, erule graph_ofI, clarsimp)
apply (frule pd_at_asid_uniq, simp_all add: valid_asid_map_def valid_arch_state_def)[1]
apply (drule subsetD, erule domI)
apply simp
apply fastforce
apply clarsimp
done
crunch aligned'[wp]: findFreeHWASID "pspace_aligned'"
(simp: crunch_simps)
crunch distinct'[wp]: findFreeHWASID "pspace_distinct'"
(simp: crunch_simps)
crunch no_0_obj'[wp]: getHWASID "no_0_obj'"
lemma get_hw_asid_corres:
"corres op =
(pd_at_asid a pd and K (a \<noteq> 0 \<and> a \<le> mask asid_bits)
and unique_table_refs o caps_of_state
and valid_global_objs and valid_vs_lookup
and valid_asid_map and valid_arch_objs
and pspace_aligned and pspace_distinct
and valid_arch_state)
(pspace_aligned' and pspace_distinct' and no_0_obj')
(get_hw_asid a) (getHWASID a)"
apply (simp add: get_hw_asid_def getHWASID_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr [OF _ load_hw_asid_corres[where pd=pd]])
apply (case_tac maybe_hw_asid, simp_all)[1]
apply clarsimp
apply (rule corres_split_eqr [OF _ find_free_hw_asid_corres])
apply (rule corres_split [OF _ store_hw_asid_corres[where pd=pd]])
apply (rule corres_trivial, simp)
apply (wp load_hw_asid_wp | simp)+
apply (simp add: pd_at_asid_uniq)
apply simp
done
lemma set_current_asid_corres:
"corres dc
(pd_at_asid a pd and K (a \<noteq> 0 \<and> a \<le> mask asid_bits)
and unique_table_refs o caps_of_state
and valid_global_objs and valid_vs_lookup
and valid_asid_map and valid_arch_objs
and pspace_aligned and pspace_distinct
and valid_arch_state)
(pspace_aligned' and pspace_distinct' and no_0_obj')
(set_current_asid a) (setCurrentASID a)"
apply (simp add: set_current_asid_def setCurrentASID_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr [OF _ get_hw_asid_corres[where pd=pd]])
apply (rule corres_machine_op)
apply (rule corres_no_failI)
apply (rule no_fail_setHardwareASID)
apply fastforce
apply (wp | simp)+
done
lemma hv_corres:
"corres (fr \<oplus> dc) (tcb_at thread) (tcb_at' thread)
(handle_vm_fault thread fault) (handleVMFault thread fault)"
apply (simp add: handleVMFault_def ArchVSpace_H.handleVMFault_def)
apply (cases fault)
apply simp
apply (rule corres_guard_imp)
apply (rule corres_splitEE)
prefer 2
apply simp
apply (rule corres_machine_op [where r="op ="])
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_getFAR)
apply (rule corres_splitEE)
prefer 2
apply simp
apply (rule corres_machine_op [where r="op ="])
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_getDFSR)
apply (rule corres_trivial, simp)
apply wp
apply simp+
apply (rule corres_guard_imp)
apply (rule corres_splitEE)
prefer 2
apply simp
apply (rule corres_as_user')
apply (rule corres_no_failI [where R="op ="])
apply (rule no_fail_getRestartPC)
apply fastforce
apply (rule corres_splitEE)
prefer 2
apply simp
apply (rule corres_machine_op [where r="op ="])
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_getIFSR)
apply (rule corres_trivial, simp)
apply wp
apply simp+
done
lemma flush_space_corres:
"corres dc
(K (asid \<le> mask asid_bits \<and> asid \<noteq> 0)
and valid_asid_map and valid_arch_objs
and pspace_aligned and pspace_distinct
and unique_table_refs o caps_of_state
and valid_global_objs and valid_vs_lookup
and valid_arch_state and pd_at_asid asid pd)
(pspace_aligned' and pspace_distinct' and no_0_obj')
(flush_space asid) (flushSpace asid)"
apply (simp add: flushSpace_def flush_space_def)
apply (rule corres_guard_imp)
apply (rule corres_split)
prefer 2
apply (rule load_hw_asid_corres[where pd=pd])
apply (rule corres_split [where R="\<lambda>_. \<top>" and R'="\<lambda>_. \<top>"])
prefer 2
apply (rule corres_machine_op [where r=dc])
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_cleanCaches_PoU)
apply (case_tac maybe_hw_asid)
apply simp
apply clarsimp
apply (rule corres_machine_op)
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_invalidateTLB_ASID)
apply wp
apply clarsimp
apply (simp add: pd_at_asid_uniq)
apply simp
done
lemma invalidate_tlb_by_asid_corres:
"corres dc
(K (asid \<le> mask asid_bits \<and> asid \<noteq> 0)
and valid_asid_map and valid_arch_objs
and pspace_aligned and pspace_distinct
and unique_table_refs o caps_of_state
and valid_global_objs and valid_vs_lookup
and valid_arch_state and pd_at_asid asid pd)
(pspace_aligned' and pspace_distinct' and no_0_obj')
(invalidate_tlb_by_asid asid) (invalidateTLBByASID asid)"
apply (simp add: invalidate_tlb_by_asid_def invalidateTLBByASID_def)
apply (rule corres_guard_imp)
apply (rule corres_split [where R="\<lambda>_. \<top>" and R'="\<lambda>_. \<top>"])
prefer 2
apply (rule load_hw_asid_corres[where pd=pd])
apply (case_tac maybe_hw_asid)
apply simp
apply clarsimp
apply (rule corres_machine_op)
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_invalidateTLB_ASID)
apply wp
apply clarsimp
apply (simp add: pd_at_asid_uniq)
apply simp
done
lemma corres_name_pre:
"\<lbrakk> \<And>s s'. \<lbrakk> P s; P' s'; (s, s') \<in> state_relation \<rbrakk>
\<Longrightarrow> corres rvr (op = s) (op = s') f g \<rbrakk>
\<Longrightarrow> corres rvr P P' f g"
apply (simp add: corres_underlying_def split_def
Ball_def)
apply blast
done
lemma invalidate_tlb_by_asid_corres_ex:
"corres dc
(\<lambda>s. asid \<le> mask asid_bits \<and> asid \<noteq> 0
\<and> valid_asid_map s \<and> valid_arch_objs s
\<and> pspace_aligned s \<and> pspace_distinct s
\<and> unique_table_refs (caps_of_state s)
\<and> valid_global_objs s \<and> valid_vs_lookup s
\<and> valid_arch_state s \<and> (\<exists>pd. pd_at_asid asid pd s))
(pspace_aligned' and pspace_distinct' and no_0_obj')
(invalidate_tlb_by_asid asid) (invalidateTLBByASID asid)"
apply (rule corres_name_pre, clarsimp)
apply (rule corres_guard_imp)
apply (rule_tac pd=pd in invalidate_tlb_by_asid_corres)
apply simp+
done
crunch valid_global_objs[wp]: do_machine_op "valid_global_objs"
lemma state_relation_asid_map:
"(s, s') \<in> state_relation \<Longrightarrow> armKSASIDMap (ksArchState s') = arm_asid_map (arch_state s)"
by (simp add: state_relation_def arch_state_relation_def)
lemma find_pd_for_asid_pd_at_asid_again:
"\<lbrace>\<lambda>s. (\<forall>pd. pd_at_asid asid pd s \<longrightarrow> P pd s)
\<and> (\<forall>ex. (\<forall>pd. \<not> pd_at_asid asid pd s) \<longrightarrow> Q ex s)
\<and> valid_arch_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0\<rbrace>
find_pd_for_asid asid
\<lbrace>P\<rbrace>,\<lbrace>Q\<rbrace>"
apply (unfold validE_def, rule hoare_name_pre_state, fold validE_def)
apply (case_tac "\<exists>pd. pd_at_asid asid pd s")
apply clarsimp
apply (rule_tac Q="\<lambda>rv s'. s' = s \<and> rv = pd" and E="\<bottom>\<bottom>" in hoare_post_impErr)
apply (rule hoare_pre, wp find_pd_for_asid_valids)
apply fastforce
apply simp+
apply (rule_tac Q="\<lambda>rv s'. s' = s \<and> pd_at_asid asid rv s'"
and E="\<lambda>rv s'. s' = s" in hoare_post_impErr)
apply (rule hoare_pre, wp)
apply clarsimp+
done
lemma set_vm_root_corres:
"corres dc (tcb_at t and valid_arch_state and valid_objs and valid_asid_map
and unique_table_refs o caps_of_state and valid_vs_lookup
and valid_global_objs and pspace_aligned and pspace_distinct
and valid_arch_objs)
(pspace_aligned' and pspace_distinct'
and valid_arch_state' and tcb_at' t and no_0_obj')
(set_vm_root t) (setVMRoot t)"
proof -
have P: "corres dc \<top> \<top>
(do global_pd \<leftarrow> gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (Platform.addrFromPPtr global_pd))
od)
(do globalPD \<leftarrow> gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromPPtr globalPD))
od)"
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply (rule corres_machine_op)
apply (rule corres_rel_imp)
apply (rule corres_underlying_trivial)
apply (rule no_fail_setCurrentPD)
apply simp
apply (subst corres_gets)
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (wp | simp)+
done
have Q: "\<And>P P'. corres dc P P'
(throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch>
(\<lambda>_ . do global_pd \<leftarrow> gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ Platform.addrFromPPtr global_pd
od))
(throwError Fault_H.lookup_failure.InvalidRoot <catch>
(\<lambda>_ . do globalPD \<leftarrow> gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromPPtr globalPD
od))"
apply (rule corres_guard_imp)
apply (rule corres_split_catch [where f=lfr])
apply (simp, rule P)
apply (subst corres_throwError, simp add: lookup_failure_map_def)
apply (wp | simp)+
done
show ?thesis
unfolding set_vm_root_def setVMRoot_def locateSlot_def
getThreadVSpaceRoot_def armv_contextSwitch_def
apply (rule corres_guard_imp)
apply (rule corres_split' [where r'="op = \<circ> cte_map"])
apply (simp add: tcbVTableSlot_def cte_map_def objBits_def
objBitsKO_def tcb_cnode_index_def to_bl_1 of_bl_True)
apply (rule_tac R="\<lambda>thread_root. valid_arch_state and valid_asid_map and
valid_arch_objs and valid_vs_lookup and
unique_table_refs o caps_of_state and
valid_global_objs and valid_objs and
pspace_aligned and pspace_distinct and
cte_wp_at (op = thread_root) thread_root_slot"
and R'="\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'"
in corres_split [OF _ getSlotCap_corres])
apply (insert Q)
apply (case_tac rv, simp_all add: isCap_simps Q[simplified])[1]
apply (case_tac arch_cap, simp_all add: isCap_simps Q[simplified])[1]
apply (case_tac option, simp_all add: Q[simplified])[1]
apply (clarsimp simp: cap_asid_def)
apply (rule corres_guard_imp)
apply (rule corres_split_catch [where f=lfr])
apply (simp add: checkPDNotInASIDMap_def
checkPDASIDMapMembership_def)
apply (rule_tac P'="(Not \<circ> pd_at_asid aa word) and K (aa \<le> mask asid_bits)
and pd_at_uniq aa word
and valid_asid_map and valid_vs_lookup
and (unique_table_refs o caps_of_state)
and valid_arch_objs and valid_global_objs
and valid_arch_state"
in corres_stateAssert_implied)
apply (rule P)
apply (clarsimp simp: restrict_map_def state_relation_asid_map
elim!: ranE)
apply (frule(1) valid_asid_mapD)
apply (case_tac "x = aa")
apply clarsimp
apply (clarsimp simp: pd_at_uniq_def restrict_map_def)
apply (erule notE, rule_tac a=x in ranI)
apply simp
apply (rule corres_split_eqrE [OF _ find_pd_for_asid_corres])
apply (rule whenE_throwError_corres)
apply (simp add: lookup_failure_map_def)
apply simp
apply simp
apply (rule corres_split)
apply (rule_tac pd=pd' in set_current_asid_corres)
apply (rule corres_machine_op)
apply (rule corres_underlying_trivial)
apply (rule no_fail_setCurrentPD)
apply (wp | simp | wp_once hoare_drop_imps)+
apply (simp add: whenE_def split del: split_if, wp)[1]
apply (rule find_pd_for_asid_pd_at_asid_again)
apply wp
apply clarsimp
apply (frule page_directory_cap_pd_at_uniq, simp+)
apply (frule(1) cte_wp_at_valid_objs_valid_cap)
apply (clarsimp simp: valid_cap_def mask_def
word_neq_0_conv)
apply (drule(1) pd_at_asid_unique2, simp)
apply simp+
apply (wp get_cap_wp | simp)+
apply (clarsimp simp: tcb_at_cte_at_1 [simplified])
apply simp
done
qed
lemma invalidateTLBByASID_invs'[wp]:
"\<lbrace>invs'\<rbrace> invalidateTLBByASID param_a \<lbrace>\<lambda>_. invs'\<rbrace>"
apply (clarsimp simp: invalidateTLBByASID_def loadHWASID_def
| wp dmo_invs' no_irq_invalidateTLB_ASID | wpc)+
apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
in use_valid)
apply (clarsimp simp: invalidateTLB_ASID_def machine_op_lift_def
machine_rest_lift_def split_def | wp)+
done
crunch aligned' [wp]: flushSpace pspace_aligned' (ignore: getObject wp: getASID_wp)
crunch distinct' [wp]: flushSpace pspace_distinct' (ignore: getObject wp: getASID_wp)
crunch valid_arch' [wp]: flushSpace valid_arch_state' (ignore: getObject wp: getASID_wp)
crunch cur_tcb' [wp]: flushSpace cur_tcb' (ignore: getObject wp: getASID_wp)
lemma get_asid_pool_corres_inv':
"corres (\<lambda>p. (\<lambda>p'. p = p' o ucast) \<circ> inv ASIDPool)
(asid_pool_at p) (pspace_aligned' and pspace_distinct')
(get_asid_pool p) (getObject p)"
apply (rule corres_rel_imp)
apply (rule get_asid_pool_corres')
apply simp
done
lemma loadHWASID_wp [wp]:
"\<lbrace>\<lambda>s. P (option_map fst (armKSASIDMap (ksArchState s) asid)) s\<rbrace>
loadHWASID asid \<lbrace>P\<rbrace>"
apply (simp add: loadHWASID_def)
apply (wp findPDForASIDAssert_pd_at_wp
| wpc | simp | wp_once hoare_drop_imps)+
apply (auto split: option.split)
done
lemma invalidate_asid_entry_corres:
"corres dc (valid_arch_objs and valid_asid_map
and K (asid \<le> mask asid_bits \<and> asid \<noteq> 0)
and pd_at_asid asid pd and valid_vs_lookup
and unique_table_refs o caps_of_state
and valid_global_objs and valid_arch_state
and pspace_aligned and pspace_distinct)
(pspace_aligned' and pspace_distinct' and no_0_obj')
(invalidate_asid_entry asid) (invalidateASIDEntry asid)"
apply (simp add: invalidate_asid_entry_def invalidateASIDEntry_def)
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ load_hw_asid_corres[where pd=pd]])
apply (rule corres_split [OF _ corres_when])
apply (rule invalidate_asid_corres[where pd=pd])
apply simp
apply simp
apply (rule invalidate_hw_asid_entry_corres)
apply (wp load_hw_asid_wp
| clarsimp cong: if_cong)+
apply (simp add: pd_at_asid_uniq)
apply simp
done
crunch aligned'[wp]: invalidateASID "pspace_aligned'"
crunch distinct'[wp]: invalidateASID "pspace_distinct'"
lemma invalidateASID_cur' [wp]:
"\<lbrace>cur_tcb'\<rbrace> invalidateASID x \<lbrace>\<lambda>_. cur_tcb'\<rbrace>"
by (simp add: invalidateASID_def|wp)+
crunch aligned' [wp]: invalidateASIDEntry pspace_aligned'
crunch distinct' [wp]: invalidateASIDEntry pspace_distinct'
crunch cur' [wp]: invalidateASIDEntry cur_tcb'
lemma invalidateASID_valid_arch_state [wp]:
"\<lbrace>valid_arch_state'\<rbrace> invalidateASIDEntry x \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>"
apply (simp add: invalidateASID_def
invalidateASIDEntry_def invalidateHWASIDEntry_def)
apply (wp | simp)+
apply (clarsimp simp: valid_arch_state'_def simp del: fun_upd_apply)
apply (rule conjI)
apply (clarsimp simp: is_inv_None_upd fun_upd_def[symmetric]
comp_upd_simp inj_on_fun_upd_elsewhere
valid_asid_map'_def)
apply (auto elim!: subset_inj_on dest!: ran_del_subset)[1]
apply (clarsimp simp add: None_upd_eq fun_upd_def[symmetric])
done
crunch no_0_obj'[wp]: deleteASID "no_0_obj'"
(ignore: getObject simp: crunch_simps
wp: crunch_wps getObject_inv loadObject_default_inv)
lemma delete_asid_corres:
"corres dc
(invs and valid_etcbs and K (asid \<le> mask asid_bits \<and> asid \<noteq> 0))
(pspace_aligned' and pspace_distinct' and no_0_obj'
and valid_arch_state' and cur_tcb')
(delete_asid asid pd) (deleteASID asid pd)"
apply (simp add: delete_asid_def deleteASID_def)
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ corres_gets_asid])
apply (case_tac "asid_table (asid_high_bits_of asid)", simp)
apply clarsimp
apply (rule_tac P="\<lambda>s. asid_high_bits_of asid \<in> dom (asidTable o ucast) \<longrightarrow>
asid_pool_at (the ((asidTable o ucast) (asid_high_bits_of asid))) s" and
P'="pspace_aligned' and pspace_distinct'" and
Q="invs and valid_etcbs and K (asid \<le> mask asid_bits \<and> asid \<noteq> 0) and
(\<lambda>s. arm_asid_table (arch_state s) = asidTable \<circ> ucast)" in
corres_split)
prefer 2
apply (simp add: dom_def)
apply (rule get_asid_pool_corres_inv')
apply (rule corres_when, simp add: mask_asid_low_bits_ucast_ucast)
apply (rule corres_split [OF _ flush_space_corres[where pd=pd]])
apply (rule corres_split [OF _ invalidate_asid_entry_corres[where pd=pd]])
apply (rule_tac P="asid_pool_at (the (asidTable (ucast (asid_high_bits_of asid))))
and valid_etcbs"
and P'="pspace_aligned' and pspace_distinct'"
in corres_split)
prefer 2
apply (simp del: fun_upd_apply)
apply (rule set_asid_pool_corres')
apply (simp add: inv_def mask_asid_low_bits_ucast_ucast)
apply (rule ext)
apply (clarsimp simp: o_def)
apply (erule notE)
apply (erule ucast_ucast_eq, simp, simp)
apply (rule corres_split [OF _ gct_corres])
apply simp
apply (rule set_vm_root_corres)
apply wp
apply (simp del: fun_upd_apply)
apply (fold cur_tcb_def)
apply (wp set_asid_pool_asid_map_unmap
set_asid_pool_arch_objs_unmap_single
set_asid_pool_vs_lookup_unmap')
apply simp
apply (fold cur_tcb'_def)
apply (wp invalidate_asid_entry_invalidates)
apply (wp | clarsimp simp: o_def)+
apply (subgoal_tac "pd_at_asid asid pd s")
apply (auto simp: obj_at_def a_type_def graph_of_def
split: split_if_asm)[1]
apply (simp add: pd_at_asid_def)
apply (rule vs_lookupI)
apply (simp add: vs_asid_refs_def)
apply (rule image_eqI[OF refl])
apply (erule graph_ofI)
apply (rule r_into_rtrancl)
apply simp
apply (erule vs_lookup1I [OF _ _ refl])
apply (simp add: vs_refs_def)
apply (rule image_eqI[rotated], erule graph_ofI)
apply (simp add: mask_asid_low_bits_ucast_ucast)
apply wp
apply (simp add: o_def)
apply (wp getASID_wp)
apply clarsimp
apply assumption
apply wp
apply clarsimp
apply (clarsimp simp: valid_arch_state_def valid_asid_table_def
dest!: invs_arch_state)
apply blast
apply (clarsimp simp: valid_arch_state'_def valid_asid_table'_def)
done
lemma valid_arch_state_unmap_strg':
"valid_arch_state' s \<longrightarrow>
valid_arch_state' (s\<lparr>ksArchState :=
armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(ptr := None))
(ksArchState s)\<rparr>)"
apply (simp add: valid_arch_state'_def valid_asid_table'_def)
apply (auto simp: ran_def split: split_if_asm)
done
crunch armKSASIDTable_inv[wp]: invalidateASIDEntry
"\<lambda>s. P (armKSASIDTable (ksArchState s))"
crunch armKSASIDTable_inv[wp]: flushSpace
"\<lambda>s. P (armKSASIDTable (ksArchState s))"
lemma delete_asid_pool_corres:
"corres dc
(invs and K (is_aligned base asid_low_bits
\<and> base \<le> mask asid_bits)
and asid_pool_at ptr)
(pspace_aligned' and pspace_distinct' and no_0_obj'
and valid_arch_state' and cur_tcb')
(delete_asid_pool base ptr) (deleteASIDPool base ptr)"
apply (simp add: delete_asid_pool_def deleteASIDPool_def)
apply (rule corres_assume_pre, simp add: is_aligned_mask
cong: corres_weak_cong)
apply (thin_tac ?P)+
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ corres_gets_asid])
apply (rule corres_when)
apply simp
apply (simp add: liftM_def)
apply (rule corres_split [OF _ get_asid_pool_corres'])
apply (rule corres_split)
prefer 2
apply (rule corres_mapM [where r=dc and r'=dc], simp, simp)
prefer 5
apply (rule order_refl)
apply (drule_tac t="inv ?f ?x \<circ> ?g" in sym)
apply (rule_tac P="invs and
ko_at (ArchObj (arch_kernel_obj.ASIDPool pool)) ptr and
[VSRef (ucast (asid_high_bits_of base)) None] \<rhd> ptr and
K (is_aligned base asid_low_bits
\<and> base \<le> mask asid_bits)"
and P'="pspace_aligned' and pspace_distinct' and no_0_obj'"
in corres_guard_imp)
apply (rule corres_when)
apply (clarsimp simp: ucast_ucast_low_bits)
apply simp
apply (rule_tac pd1="the (pool (ucast xa))"
in corres_split [OF _ flush_space_corres])
apply (rule_tac pd="the (pool (ucast xa))"
in invalidate_asid_entry_corres)
apply wp
apply clarsimp
apply wp
apply (clarsimp simp: invs_def valid_state_def
valid_arch_caps_def valid_pspace_def
pd_at_asid_def cong: conj_cong)
apply (rule conjI)
apply (clarsimp simp: mask_def asid_low_bits_word_bits
elim!: is_alignedE)
apply (subgoal_tac "of_nat q < (2 ^ asid_high_bits :: word32)")
apply (subst mult_ac, rule word_add_offset_less)
apply assumption
apply assumption
apply (simp add: asid_bits_def word_bits_def)
apply (erule order_less_le_trans)
apply (simp add: word_bits_def asid_low_bits_def asid_high_bits_def)
apply (simp add: asid_bits_def asid_high_bits_def asid_low_bits_def)
apply (drule word_power_less_diff)
apply (drule of_nat_mono_maybe[where 'a=32, rotated])
apply (simp add: word_bits_def asid_low_bits_def)
apply (subst word_unat_power, simp)
apply (simp add: asid_bits_def word_bits_def)
apply (simp add: asid_low_bits_def word_bits_def)
apply (simp add: asid_bits_def asid_low_bits_def asid_high_bits_def)
apply (subst conj_commute, rule context_conjI)
apply (erule vs_lookup_trancl_step)