forked from seL4/l4v
-
Notifications
You must be signed in to change notification settings - Fork 0
/
CSpace_AI.thy
4775 lines (4000 loc) · 166 KB
/
CSpace_AI.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
*
* SPDX-License-Identifier: GPL-2.0-only
*)
(*
CSpace refinement
*)
theory CSpace_AI
imports ArchCSpacePre_AI
begin
context begin interpretation Arch .
requalify_consts
irq_state_update
irq_state
final_matters_arch
ups_of_heap
requalify_facts
is_derived_arch_non_arch
ups_of_heap_non_arch_upd
master_arch_cap_obj_refs
master_arch_cap_cap_class
same_aobject_as_commute
arch_derive_cap_inv
loadWord_inv
valid_global_refsD2
arch_derived_is_device
update_cnode_cap_data_def
safe_parent_for_arch_not_arch
safe_parent_cap_range_arch
valid_arch_mdb_simple
set_cap_update_free_index_valid_arch_mdb
set_untyped_cap_as_full_valid_arch_mdb
valid_arch_mdb_updates
safe_parent_arch_is_parent
safe_parent_for_arch_not_arch'
safe_parent_for_arch_no_obj_refs
valid_arch_mdb_same_master_cap
valid_arch_mdb_null_filter
valid_arch_mdb_untypeds
end
declare set_cap_update_free_index_valid_arch_mdb[wp]
(* Proofs don't want to see these details. *)
declare update_cnode_cap_data_def [simp]
lemma capBadge_ordefield_simps[simp]:
"(None, y) \<in> capBadge_ordering fb"
"((y, None) \<in> capBadge_ordering fb) = (y = None)"
"((y, y) \<in> capBadge_ordering fb) = (fb \<longrightarrow> (y = None \<or> y = Some 0))"
"((Some x, Some z) \<in> capBadge_ordering fb) = (x = 0 \<or> (\<not> fb \<and> x = z))"
"(y, Some 0) \<in> capBadge_ordering fb = (y = None \<or> y = Some 0)"
by (simp add: capBadge_ordering_def disj_ac
| simp add: eq_commute image_def
| fastforce)+
lemma capBadge_ordering_trans:
"\<lbrakk> (x, y) \<in> capBadge_ordering v; (y, z) \<in> capBadge_ordering v2 \<rbrakk>
\<Longrightarrow> (x, z) \<in> capBadge_ordering v2"
by (auto simp: capBadge_ordering_def split: if_split_asm)
definition "irq_state_independent_A (P :: 'z state \<Rightarrow> bool) \<equiv>
\<forall>(f :: nat \<Rightarrow> nat) (s :: 'z state). P s \<longrightarrow> P (s\<lparr>machine_state := machine_state s
\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>)"
lemma irq_state_independent_AI[intro!, simp]:
"\<lbrakk>\<And>s f. P (s\<lparr>machine_state := machine_state s
\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) = P s\<rbrakk>
\<Longrightarrow> irq_state_independent_A P"
by (simp add: irq_state_independent_A_def)
(* FIXME: Move. *)
lemma irq_state_independent_A_conjI[intro!]:
"\<lbrakk>irq_state_independent_A P; irq_state_independent_A Q\<rbrakk>
\<Longrightarrow> irq_state_independent_A (P and Q)"
"\<lbrakk>irq_state_independent_A P; irq_state_independent_A Q\<rbrakk>
\<Longrightarrow> irq_state_independent_A (\<lambda>s. P s \<and> Q s)"
by (auto simp: irq_state_independent_A_def)
(* FIXME: move *)
lemma gets_machine_state_modify:
"do x \<leftarrow> gets machine_state;
u \<leftarrow> modify (machine_state_update (\<lambda>y. x));
f x
od =
gets machine_state >>= f"
by (simp add: bind_def split_def simpler_gets_def simpler_modify_def)
locale CSpace_AI_getActiveIRQ_wp =
fixes state_ext_t :: "'state_ext::state_ext itself"
assumes getActiveIRQ_wp[wp]:
"\<And>P :: 'state_ext state \<Rightarrow> bool.
irq_state_independent_A P \<Longrightarrow> valid P (do_machine_op (getActiveIRQ in_kernel)) (\<lambda>_. P)"
lemma OR_choiceE_weak_wp:
"\<lbrace>P\<rbrace> f \<sqinter> g \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> OR_choiceE b f g \<lbrace>Q\<rbrace>"
apply (fastforce simp add: OR_choiceE_def alternative_def valid_def bind_def
select_f_def gets_def return_def get_def liftE_def lift_def bindE_def
split: option.splits if_split_asm)
done
context CSpace_AI_getActiveIRQ_wp begin
lemma preemption_point_inv:
fixes P :: "'state_ext state \<Rightarrow> bool"
shows
"\<lbrakk>irq_state_independent_A P; \<And>f s. P (trans_state f s) = P s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> preemption_point \<lbrace>\<lambda>_. P\<rbrace>"
apply (intro impI conjI | simp add: preemption_point_def o_def
| wp hoare_post_imp[OF _ getActiveIRQ_wp] OR_choiceE_weak_wp alternative_wp[where P=P]
| wpc)+
done
end
lemmas valid_cap_machine_state [iff]
= machine_state_update.valid_cap_update
lemma get_cap_valid [wp]:
"\<lbrace> valid_objs \<rbrace> get_cap addr \<lbrace> valid_cap \<rbrace>"
apply (wp get_cap_wp)
apply (auto dest: cte_wp_at_valid_objs_valid_cap)
done
lemma get_cap_wellformed:
"\<lbrace>valid_objs\<rbrace> get_cap slot \<lbrace>\<lambda>cap s. wellformed_cap cap\<rbrace>"
apply (rule hoare_strengthen_post, rule get_cap_valid)
apply (simp add: valid_cap_def2)
done
lemma update_cdt_cdt:
"\<lbrace>\<lambda>s. valid_mdb (cdt_update (\<lambda>_. (m (cdt s))) s)\<rbrace> update_cdt m \<lbrace>\<lambda>_. valid_mdb\<rbrace>"
by (simp add: update_cdt_def set_cdt_def) wp
(* FIXME: rename *)
lemma unpleasant_helper:
"(\<forall>a b. (\<exists>c. a = f c \<and> b = g c \<and> P c) \<longrightarrow> Q a b) = (\<forall>c. P c \<longrightarrow> Q (f c) (g c))"
by blast
lemma get_object_det:
"(r,s') \<in> fst (get_object p s) \<Longrightarrow> get_object p s = ({(r,s)}, False)"
by (auto simp: in_monad get_object_def bind_def gets_def get_def return_def)
lemma get_object_at_obj:
"\<lbrakk> (r,s') \<in> fst (get_object p s); P r \<rbrakk> \<Longrightarrow> obj_at P p s"
by (auto simp: get_object_def obj_at_def in_monad)
lemma get_cap_cte_at:
"(r,s') \<in> fst (get_cap p s) \<Longrightarrow> cte_at p s"
unfolding cte_at_def by (auto dest: get_cap_det)
lemma rab_cte_cap_to':
"s \<turnstile> \<lbrace>\<lambda>s. (is_cnode_cap (fst args) \<longrightarrow> (\<forall>r\<in>cte_refs (fst args) (interrupt_irq_node s). ex_cte_cap_wp_to P r s))
\<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace>
resolve_address_bits args
\<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>"
unfolding resolve_address_bits_def
proof (induct args arbitrary: s rule: resolve_address_bits'.induct)
case (1 z cap cref s')
have P:
"\<And>P' Q args adm s.
\<lbrakk> s \<turnstile> \<lbrace>P'\<rbrace> resolve_address_bits' z args \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>;
\<And>rv s. ex_cte_cap_wp_to P (fst rv) s \<Longrightarrow> Q rv s \<rbrakk> \<Longrightarrow>
s \<turnstile> \<lbrace>P'\<rbrace> resolve_address_bits' z args \<lbrace>Q\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>"
unfolding spec_validE_def
apply (fold validE_R_def)
apply (erule hoare_post_imp_R)
apply simp
done
show ?case
apply (subst resolve_address_bits'.simps)
apply (cases cap, simp_all split del: if_split)
defer 6 (* CNode *)
apply (wp+)[11]
apply (simp add: split_def cong: if_cong split del: if_split)
apply (rule hoare_pre_spec_validE)
apply (wp P [OF "1.hyps"], (simp add: in_monad | rule conjI refl)+)
apply (wp | simp | rule get_cap_wp)+
apply (fastforce simp: ex_cte_cap_wp_to_def elim!: cte_wp_at_weakenE)
done
qed
lemmas rab_cte_cap_to = use_spec(2) [OF rab_cte_cap_to']
lemma resolve_address_bits_real_cte_at:
"\<lbrace> valid_objs and valid_cap (fst args) \<rbrace>
resolve_address_bits args
\<lbrace>\<lambda>rv. real_cte_at (fst rv)\<rbrace>, -"
unfolding resolve_address_bits_def
proof (induct args rule: resolve_address_bits'.induct)
case (1 z cap cref)
show ?case
apply (clarsimp simp add: validE_R_def validE_def valid_def split: sum.split)
apply (subst (asm) resolve_address_bits'.simps)
apply (cases cap)
defer 6 (* cnode *)
apply (auto simp: in_monad)[11]
apply (rename_tac obj_ref nat list)
apply (simp only: cap.simps)
apply (case_tac "nat + length list = 0")
apply (simp add: fail_def)
apply (simp only: if_False)
apply (simp only: K_bind_def in_bindE_R)
apply (elim conjE exE)
apply (simp only: split: if_split_asm)
apply (clarsimp simp add: in_monad)
apply (clarsimp simp add: valid_cap_def)
apply (simp only: K_bind_def in_bindE_R)
apply (elim conjE exE)
apply (simp only: split: if_split_asm)
apply (frule (8) "1.hyps")
apply (clarsimp simp: in_monad validE_def validE_R_def valid_def)
apply (frule in_inv_by_hoareD [OF get_cap_inv])
apply simp
apply (frule (1) post_by_hoare [OF get_cap_valid])
apply (erule allE, erule impE, blast)
apply (clarsimp simp: in_monad split: cap.splits)
apply (drule (1) bspec, simp)+
apply (clarsimp simp: in_monad)
apply (frule in_inv_by_hoareD [OF get_cap_inv])
apply (clarsimp simp add: valid_cap_def)
done
qed
lemma resolve_address_bits_cte_at:
"\<lbrace> valid_objs and valid_cap (fst args) \<rbrace>
resolve_address_bits args
\<lbrace>\<lambda>rv. cte_at (fst rv)\<rbrace>, -"
apply (rule hoare_post_imp_R, rule resolve_address_bits_real_cte_at)
apply (erule real_cte_at_cte)
done
lemma lookup_slot_real_cte_at_wp [wp]:
"\<lbrace> valid_objs \<rbrace> lookup_slot_for_thread t addr \<lbrace>\<lambda>rv. real_cte_at (fst rv)\<rbrace>,-"
apply (simp add: lookup_slot_for_thread_def)
apply wp
apply (rule resolve_address_bits_real_cte_at)
apply simp
apply wp
apply clarsimp
apply (erule(1) objs_valid_tcb_ctable)
done
lemma lookup_slot_cte_at_wp[wp]:
"\<lbrace> valid_objs \<rbrace> lookup_slot_for_thread t addr \<lbrace>\<lambda>rv. cte_at (fst rv)\<rbrace>,-"
by (strengthen real_cte_at_cte, wp)
lemma get_cap_success:
fixes s cap ptr offset
defines "s' \<equiv> s\<lparr>kheap := [ptr \<mapsto> CNode (length offset) (\<lambda>x. if length x = length offset then Some cap else None)]\<rparr>"
shows "(cap, s') \<in> fst (get_cap (ptr, offset) s')"
by (simp add: get_cap_def get_object_def
in_monad s'_def well_formed_cnode_n_def length_set_helper dom_def
split: Structures_A.kernel_object.splits)
lemma len_drop_lemma:
assumes drop: "drop (n - length ys) xs = ys"
assumes l: "n = length xs"
shows "length ys \<le> n"
proof -
from drop
have "length (drop (n - length ys) xs) = length ys"
by simp
with l
have "length ys = n - (n - length ys)"
by simp
thus ?thesis by arith
qed
lemma drop_postfixD:
"(drop (length xs - length ys) xs = ys) \<Longrightarrow> (\<exists>zs. xs = zs @ ys)"
proof (induct xs arbitrary: ys)
case Nil thus ?case by simp
next
case (Cons x xs)
from Cons.prems
have "length ys \<le> length (x # xs)"
by (rule len_drop_lemma) simp
moreover
{ assume "length ys = length (x # xs)"
with Cons.prems
have ?case by simp
}
moreover {
assume "length ys < length (x # xs)"
hence "length ys \<le> length xs" by simp
hence "drop (length xs - length ys) xs =
drop (length (x # xs) - length ys) (x # xs)"
by (simp add: Suc_diff_le)
with Cons.prems
have ?case by (auto dest: Cons.hyps)
}
ultimately
show ?case by (auto simp: order_le_less)
qed
lemma drop_postfix_eq:
"n = length xs \<Longrightarrow> (drop (n - length ys) xs = ys) = (\<exists>zs. xs = zs @ ys)"
by (auto dest: drop_postfixD)
lemma postfix_dropD:
"xs = zs @ ys \<Longrightarrow> drop (length xs - length ys) xs = ys"
by simp
lemmas is_cap_defs = is_arch_cap_def is_zombie_def
lemma guard_mask_shift:
fixes cref' :: "'a::len word"
assumes postfix: "to_bl cref' = xs @ cref"
shows
"(length guard \<le> length cref \<and>
(cref' >> (length cref - length guard)) && mask (length guard) = of_bl guard)
= (guard \<le> cref)" (is "(_ \<and> ?l = ?r) = _ " is "(?len \<and> ?shift) = ?prefix")
proof
let ?w_len = "len_of TYPE('a)"
from postfix
have "length (to_bl cref') = length xs + length cref" by simp
hence w_len: "?w_len = \<dots>" by simp
assume "?len \<and> ?shift"
hence shift: ?shift and c_len: ?len by auto
from w_len c_len have "length guard \<le> ?w_len" by simp
with shift
have "(replicate (?w_len - length guard) False) @ guard = to_bl ?l"
by (simp add: word_rep_drop)
also
have "\<dots> = replicate (?w_len - length guard) False @
drop (?w_len - length guard) (to_bl (cref' >> (length cref - length guard)))"
by (simp add: bl_and_mask)
also
from c_len
have "\<dots> = replicate (?w_len - length guard) False @ take (length guard) cref"
by (simp add: bl_shiftr w_len word_size postfix)
finally
have "take (length guard) cref = guard" by simp
thus ?prefix by (simp add: take_prefix)
next
let ?w_len = "len_of TYPE('a)"
assume ?prefix
then obtain zs where cref: "cref = guard @ zs"
by (auto simp: prefix_def less_eq_list_def)
with postfix
have to_bl_c: "to_bl cref' = xs @ guard @ zs" by simp
hence "length (to_bl cref') = length \<dots>" by simp
hence w_len: "?w_len = \<dots>" by simp
from cref have c_len: "length guard \<le> length cref" by simp
from cref
have "length cref - length guard = length zs" by simp
hence "to_bl ?l = replicate (?w_len - length guard) False @
drop (?w_len - length guard) (to_bl (cref' >> (length zs)))"
by (simp add: bl_and_mask)
also
have "drop (?w_len - length guard) (to_bl (cref' >> (length zs))) = guard"
by (simp add: bl_shiftr word_size w_len to_bl_c)
finally
have "to_bl ?l = to_bl ?r"
by (simp add: word_rep_drop w_len)
with c_len
show "?len \<and> ?shift" by simp
qed
lemma of_bl_take:
"length xs < len_of TYPE('a) \<Longrightarrow> of_bl (take n xs) = ((of_bl xs) >> (length xs - n) :: ('a :: len) word)"
apply (clarsimp simp: bang_eq and_bang test_bit_of_bl
rev_take conj_comms nth_shiftr)
apply safe
apply simp_all
apply (clarsimp elim!: rsubst[where P="\<lambda>x. rev xs ! x"])+
done
lemma gets_the_tcb_get_cap:
"tcb_at t s \<Longrightarrow> liftM tcb_ctable (gets_the (get_tcb t)) s = get_cap (t, tcb_cnode_index 0) s"
apply (clarsimp simp add: tcb_at_def liftM_def bind_def assert_opt_def
gets_the_def simpler_gets_def return_def)
apply (clarsimp dest!: get_tcb_SomeD
simp add: get_cap_def tcb_cnode_map_def
get_object_def bind_def simpler_gets_def
return_def assert_def fail_def assert_opt_def)
done
lemma upd_other_cte_wp_at:
"\<lbrakk> cte_wp_at P p s; fst p \<noteq> ptr \<rbrakk> \<Longrightarrow>
cte_wp_at P p (kheap_update (\<lambda>ps. (kheap s)(ptr \<mapsto> ko)) s)"
by (auto elim!: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI)
lemma get_cap_cte_wp_at:
"\<lbrace>\<top>\<rbrace> get_cap p \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = rv) p\<rbrace>"
apply (wp get_cap_wp)
apply (clarsimp elim!: cte_wp_at_weakenE)
done
lemma get_cap_sp:
"\<lbrace>P\<rbrace> get_cap p \<lbrace>\<lambda>rv. P and cte_wp_at (\<lambda>c. c = rv) p\<rbrace>"
by (wp get_cap_cte_wp_at)
lemma wf_cs_nD:
"\<lbrakk> f x = Some y; well_formed_cnode_n n f \<rbrakk> \<Longrightarrow> length x = n"
unfolding well_formed_cnode_n_def by blast
lemma set_cdt_valid_pspace:
"\<lbrace>valid_pspace\<rbrace> set_cdt m \<lbrace>\<lambda>_. valid_pspace\<rbrace>"
unfolding set_cdt_def
apply simp
apply wp
apply (erule valid_pspace_eqI)
apply clarsimp
done
lemma cte_at_pspace:
"cte_wp_at P p s \<Longrightarrow> \<exists>ko. kheap s (fst p) = Some ko"
by (auto simp: cte_wp_at_cases)
lemma tcb_cap_cases_length:
"x \<in> dom tcb_cap_cases \<Longrightarrow> length x = 3"
by (auto simp add: tcb_cap_cases_def tcb_cnode_index_def to_bl_1)
lemma cte_at_cref_len:
"\<lbrakk>cte_at (p, c) s; cte_at (p, c') s\<rbrakk> \<Longrightarrow> length c = length c'"
apply (clarsimp simp: cte_at_cases)
apply (erule disjE)
prefer 2
apply (clarsimp simp: tcb_cap_cases_length)
apply clarsimp
apply (drule (1) wf_cs_nD)
apply (drule (1) wf_cs_nD)
apply simp
done
lemma well_formed_cnode_invsI:
"\<lbrakk> valid_objs s; kheap s x = Some (CNode sz cs) \<rbrakk>
\<Longrightarrow> well_formed_cnode_n sz cs"
apply (erule(1) valid_objsE)
apply (clarsimp simp: well_formed_cnode_n_def valid_obj_def valid_cs_def valid_cs_size_def
length_set_helper)
done
lemma set_cap_cte_eq:
"(x,t) \<in> fst (set_cap c p' s) \<Longrightarrow>
cte_at p' s \<and> cte_wp_at P p t = (if p = p' then P c else cte_wp_at P p s)"
apply (cases p)
apply (cases p')
apply (auto simp: set_cap_def2 split_def in_monad cte_wp_at_cases
get_object_def set_object_def wf_cs_upd
split: Structures_A.kernel_object.splits if_split_asm
option.splits,
auto simp: tcb_cap_cases_def split: if_split_asm)
done
lemma descendants_of_cte_at:
"\<lbrakk> p \<in> descendants_of x (cdt s); valid_mdb s \<rbrakk>
\<Longrightarrow> cte_at p s"
apply (simp add: descendants_of_def)
apply (drule tranclD2)
apply (clarsimp simp: cdt_parent_defs valid_mdb_def mdb_cte_at_def
simp del: split_paired_All)
apply (fastforce elim: cte_wp_at_weakenE)
done
lemma descendants_of_cte_at2:
"\<lbrakk> p \<in> descendants_of x (cdt s); valid_mdb s \<rbrakk>
\<Longrightarrow> cte_at x s"
apply (simp add: descendants_of_def)
apply (drule tranclD)
apply (clarsimp simp: cdt_parent_defs valid_mdb_def mdb_cte_at_def
simp del: split_paired_All)
apply (fastforce elim: cte_wp_at_weakenE)
done
lemma in_set_cap_cte_at:
"(x, s') \<in> fst (set_cap c p' s) \<Longrightarrow> cte_at p s' = cte_at p s"
by (fastforce simp: cte_at_cases set_cap_def split_def wf_cs_upd
in_monad get_object_def set_object_def
split: Structures_A.kernel_object.splits if_split_asm)
lemma in_set_cap_cte_at_swp:
"(x, s') \<in> fst (set_cap c p' s) \<Longrightarrow> swp cte_at s' = swp cte_at s"
by (simp add: swp_def in_set_cap_cte_at)
(* FIXME: move *)
lemma take_to_bl_len:
fixes a :: "'a::len word"
fixes b :: "'a::len word"
assumes t: "take x (to_bl a) = take y (to_bl b)"
assumes x: "x \<le> size a"
assumes y: "y \<le> size b"
shows "x = y"
proof -
from t
have "length (take x (to_bl a)) = length (take y (to_bl b))"
by simp
also
from x have "length (take x (to_bl a)) = x"
by (simp add: word_size)
also
from y have "length (take y (to_bl b)) = y"
by (simp add: word_size)
finally
show ?thesis .
qed
definition
final_matters :: "cap \<Rightarrow> bool"
where
"final_matters cap \<equiv> case cap of
Structures_A.NullCap \<Rightarrow> False
| Structures_A.UntypedCap dev p b f \<Rightarrow> False
| Structures_A.EndpointCap r badge rights \<Rightarrow> True
| Structures_A.NotificationCap r badge rights \<Rightarrow> True
| Structures_A.CNodeCap r bits guard \<Rightarrow> True
| Structures_A.ThreadCap r \<Rightarrow> True
| Structures_A.DomainCap \<Rightarrow> False
| Structures_A.ReplyCap r master rights \<Rightarrow> False
| Structures_A.IRQControlCap \<Rightarrow> False
| Structures_A.IRQHandlerCap irq \<Rightarrow> True
| Structures_A.Zombie r b n \<Rightarrow> True
| Structures_A.ArchObjectCap ac \<Rightarrow> final_matters_arch ac"
lemmas final_matters_simps[simp]
= final_matters_def[split_simps cap.split]
lemma no_True_set_nth:
"(True \<notin> set xs) = (\<forall>n < length xs. xs ! n = False)"
apply (induct xs)
apply simp
apply (case_tac a, simp_all)
apply (rule_tac x=0 in exI)
apply simp
apply safe
apply (case_tac n, simp_all)[1]
apply (case_tac na, simp_all)[1]
apply (erule_tac x="Suc n" in allE)
apply clarsimp
done
lemma set_cap_caps_of_state_monad:
"(v, s') \<in> fst (set_cap cap p s) \<Longrightarrow> caps_of_state s' = (caps_of_state s (p \<mapsto> cap))"
apply (drule use_valid)
apply (rule set_cap_caps_of_state [where P="(=) (caps_of_state s (p\<mapsto>cap))"])
apply (rule refl)
apply simp
done
lemma descendants_of_empty:
"(descendants_of d m = {}) = (\<forall>c. \<not>m \<turnstile> d cdt_parent_of c)"
apply (simp add: descendants_of_def)
apply (rule iffI)
apply clarsimp
apply (erule allE, erule allE)
apply (erule notE)
apply fastforce
apply clarsimp
apply (drule tranclD)
apply clarsimp
done
lemma descendants_of_None:
"(\<forall>c. d \<notin> descendants_of c m) = (m d = None)"
apply (simp add: descendants_of_def cdt_parent_defs)
apply (rule iffI)
prefer 2
apply clarsimp
apply (drule tranclD2)
apply clarsimp
apply (erule contrapos_pp)
apply fastforce
done
lemma not_should_be_parent_Null [simp]:
"should_be_parent_of cap.NullCap a b c = False"
by (simp add: should_be_parent_of_def)
lemma mdb_None_no_parent:
"m p = None \<Longrightarrow> m \<Turnstile> c \<leadsto> p = False"
by (clarsimp simp: cdt_parent_defs)
lemma descendants_of_self:
assumes "descendants_of dest m = {}"
shows "descendants_of x (m(dest \<mapsto> dest)) =
(if x = dest then {dest} else descendants_of x m - {dest})" using assms
apply (clarsimp simp: descendants_of_def cdt_parent_defs)
apply (rule conjI)
apply clarsimp
apply (fastforce split: if_split_asm elim: trancl_into_trancl trancl_induct)
apply clarsimp
apply (rule set_eqI)
apply clarsimp
apply (rule iffI)
apply (erule trancl_induct)
apply fastforce
apply clarsimp
apply (erule trancl_into_trancl)
apply clarsimp
apply clarsimp
apply (rule_tac P="(a,b) \<noteq> dest" in mp)
prefer 2
apply assumption
apply (thin_tac "(a,b) \<noteq> dest")
apply (erule trancl_induct)
apply fastforce
apply (fastforce split: if_split_asm elim: trancl_into_trancl)
done
lemma descendants_of_self_None:
assumes "descendants_of dest m = {}"
assumes n: "m dest = None"
shows "descendants_of x (m(dest \<mapsto> dest)) =
(if x = dest then {dest} else descendants_of x m)"
apply (subst descendants_of_self[OF assms(1)])
apply clarsimp
apply (subgoal_tac "dest \<notin> descendants_of x m")
apply simp
apply (insert n)
apply (simp add: descendants_of_None [symmetric] del: split_paired_All)
done
lemma descendants_insert_evil_trancl_induct:
assumes "src \<noteq> dest"
assumes d: "descendants_of dest m = {}"
assumes "src \<in> descendants_of x m"
shows "src \<in> descendants_of x (m (dest \<mapsto> src))"
proof -
have r: "\<And>t. \<lbrakk> src \<in> descendants_of x m; t = src \<rbrakk> \<Longrightarrow> src \<noteq> dest \<longrightarrow> src \<in> descendants_of x (m (dest \<mapsto> t))"
unfolding descendants_of_def cdt_parent_defs
apply (simp (no_asm_use) del: fun_upd_apply)
apply (erule trancl_induct)
apply clarsimp
apply (rule r_into_trancl)
apply clarsimp
apply (rule impI)
apply (erule impE)
apply (insert d)[1]
apply (clarsimp simp: descendants_of_def cdt_parent_defs)
apply fastforce
apply (simp del: fun_upd_apply)
apply (erule trancl_into_trancl)
apply clarsimp
done
show ?thesis using assms
apply -
apply (rule r [THEN mp])
apply assumption
apply (rule refl)
apply assumption
done
qed
lemma descendants_of_insert_child:
assumes d: "descendants_of dest m = {}"
assumes s: "src \<noteq> dest"
shows
"descendants_of x (m (dest \<mapsto> src)) =
(if src \<in> descendants_of x m \<or> x = src
then descendants_of x m \<union> {dest} else descendants_of x m - {dest})"
using assms
apply (simp add: descendants_of_def cdt_parent_defs del: fun_upd_apply)
apply (rule conjI)
apply clarify
apply (rule set_eqI)
apply (simp del: fun_upd_apply)
apply (rule iffI)
apply (simp only: disj_imp)
apply (erule_tac b="xa" in trancl_induct)
apply fastforce
apply clarsimp
apply (erule impE)
apply fastforce
apply (rule trancl_into_trancl)
prefer 2
apply simp
apply assumption
apply (erule disjE)
apply (drule descendants_insert_evil_trancl_induct [OF _ d])
apply (simp add: descendants_of_def cdt_parent_defs)
apply (simp add: descendants_of_def cdt_parent_defs del: fun_upd_apply)
apply (erule trancl_into_trancl)
apply fastforce
apply (case_tac "xa = dest")
apply (simp del: fun_upd_apply)
apply (drule descendants_insert_evil_trancl_induct [OF _ d])
apply (simp add: descendants_of_def cdt_parent_defs)
apply (simp add: descendants_of_def cdt_parent_defs del: fun_upd_apply)
apply (erule trancl_into_trancl)
apply fastforce
apply (rule_tac P="xa \<noteq> dest" in mp)
prefer 2
apply assumption
apply (erule_tac b=xa in trancl_induct)
apply fastforce
apply (clarsimp simp del: fun_upd_apply)
apply (erule impE)
apply fastforce
apply (fastforce elim: trancl_into_trancl)
apply (rule conjI)
apply (clarsimp simp del: fun_upd_apply)
apply (rule set_eqI)
apply (simp del: fun_upd_apply)
apply (rule iffI)
apply (simp only: disj_imp)
apply (erule_tac b="xa" in trancl_induct)
apply fastforce
apply clarsimp
apply (erule impE)
apply fastforce
apply (rule trancl_into_trancl)
prefer 2
apply simp
apply assumption
apply (erule disjE)
apply fastforce
apply (case_tac "xa = dest")
apply fastforce
apply (rule_tac P="xa \<noteq> dest" in mp)
prefer 2
apply assumption
apply (erule_tac b=xa in trancl_induct)
apply fastforce
apply (clarsimp simp del: fun_upd_apply)
apply (erule impE)
apply fastforce
apply (fastforce elim: trancl_into_trancl)
apply clarify
apply (rule set_eqI)
apply (simp del: fun_upd_apply)
apply (rule iffI)
apply (erule trancl_induct)
apply (fastforce split: if_split_asm)
apply (clarsimp split: if_split_asm)
apply (fastforce elim: trancl_into_trancl)
apply (elim conjE)
apply (rule_tac P="xa \<noteq> dest" in mp)
prefer 2
apply assumption
apply (erule_tac b=xa in trancl_induct)
apply fastforce
apply (clarsimp simp del: fun_upd_apply)
apply (erule impE)
apply fastforce
apply (erule trancl_into_trancl)
apply fastforce
done
lemma descendants_of_NoneD:
"\<lbrakk> m p = None; p \<in> descendants_of x m \<rbrakk> \<Longrightarrow> False"
by (simp add: descendants_of_None [symmetric] del: split_paired_All)
lemma descendants_of_insert_child':
assumes d: "descendants_of dest m = {}"
assumes s: "src \<noteq> dest"
assumes m: "m dest = None"
shows
"descendants_of x (m (dest \<mapsto> src)) =
(if src \<in> descendants_of x m \<or> x = src
then descendants_of x m \<union> {dest} else descendants_of x m)"
apply (subst descendants_of_insert_child [OF d s])
apply clarsimp
apply (subgoal_tac "dest \<notin> descendants_of x m")
apply clarsimp
apply (rule notI)
apply (rule descendants_of_NoneD, rule m, assumption)
done
locale vmdb_abs =
fixes s m cs
assumes valid_mdb: "valid_mdb s"
defines "m \<equiv> cdt s"
defines "cs \<equiv> caps_of_state s"
context vmdb_abs begin
lemma no_mloop [intro!]: "no_mloop m"
using valid_mdb by (simp add: valid_mdb_def m_def)
lemma no_loops [simp, intro!]: "\<not>m \<Turnstile> p \<rightarrow> p"
using no_mloop by (cases p) (simp add: no_mloop_def)
lemma no_mdb_loop [simp, intro!]: "m p \<noteq> Some p"
proof
assume "m p = Some p"
hence "m \<Turnstile> p \<leadsto> p" by (simp add: cdt_parent_of_def)
hence "m \<Turnstile> p \<rightarrow> p" ..
thus False by simp
qed
lemma untyped_inc:
"untyped_inc m cs"
using valid_mdb by (simp add: valid_mdb_def m_def cs_def)
lemma untyped_mdb:
"untyped_mdb m cs"
using valid_mdb by (simp add: valid_mdb_def m_def cs_def)
lemma null_no_mdb:
"cs p = Some cap.NullCap \<Longrightarrow> \<not> m \<Turnstile> p \<rightarrow> p' \<and> \<not> m \<Turnstile> p' \<rightarrow> p"
using valid_mdb_no_null [OF valid_mdb]
by (simp add: m_def cs_def)
end
lemma the_arch_cap_ArchObjectCap[simp]:
"the_arch_cap (cap.ArchObjectCap cap) = cap"
by (simp add: the_arch_cap_def)
lemma cap_master_cap_simps:
"cap_master_cap (cap.EndpointCap ref bdg rghts) = cap.EndpointCap ref 0 UNIV"
"cap_master_cap (cap.NotificationCap ref bdg rghts) = cap.NotificationCap ref 0 UNIV"
"cap_master_cap (cap.CNodeCap ref bits gd) = cap.CNodeCap ref bits []"
"cap_master_cap (cap.ThreadCap ref) = cap.ThreadCap ref"
"cap_master_cap (cap.NullCap) = cap.NullCap"
"cap_master_cap (cap.DomainCap) = cap.DomainCap"
"cap_master_cap (cap.UntypedCap dev r n f) = cap.UntypedCap dev r n 0"
"cap_master_cap (cap.ReplyCap r m rights) = cap.ReplyCap r True UNIV"
"cap_master_cap (cap.IRQControlCap) = cap.IRQControlCap"
"cap_master_cap (cap.IRQHandlerCap irq) = cap.IRQHandlerCap irq"
"cap_master_cap (cap.Zombie r a b) = cap.Zombie r a b"
"cap_master_cap (ArchObjectCap ac) = ArchObjectCap (cap_master_arch_cap ac)"
by (simp_all add: cap_master_cap_def)
lemma is_original_cap_set_cap:
"(x,s') \<in> fst (set_cap p c s) \<Longrightarrow> is_original_cap s' = is_original_cap s"
by (clarsimp simp: set_cap_def in_monad split_def get_object_def set_object_def
split: if_split_asm Structures_A.kernel_object.splits)
lemma mdb_set_cap:
"(x,s') \<in> fst (set_cap p c s) \<Longrightarrow> cdt s' = cdt s"
by (clarsimp simp: set_cap_def in_monad split_def get_object_def set_object_def
split: if_split_asm Structures_A.kernel_object.splits)
lemma master_cap_obj_refs:
"cap_master_cap c = cap_master_cap c' \<Longrightarrow> obj_refs c = obj_refs c'"
by (clarsimp simp add: cap_master_cap_def
intro!: master_arch_cap_obj_refs[THEN arg_cong[where f=set_option]]
split: cap.splits)
lemma master_cap_untyped_range:
"cap_master_cap c = cap_master_cap c' \<Longrightarrow> untyped_range c = untyped_range c'"
by (simp add: cap_master_cap_def split: cap.splits)
lemma master_cap_cap_range:
"cap_master_cap c = cap_master_cap c' \<Longrightarrow> cap_range c = cap_range c'"
by (simp add: cap_range_def cong: master_cap_untyped_range master_cap_obj_refs)
lemma master_cap_ep:
"cap_master_cap c = cap_master_cap c' \<Longrightarrow> is_ep_cap c = is_ep_cap c'"
by (simp add: cap_master_cap_def is_cap_simps split: cap.splits)
lemma master_cap_ntfn:
"cap_master_cap c = cap_master_cap c' \<Longrightarrow> is_ntfn_cap c = is_ntfn_cap c'"
by (simp add: cap_master_cap_def is_cap_simps split: cap.splits)
lemma cap_master_cap_zombie:
"cap_master_cap c = cap_master_cap c' \<Longrightarrow> is_zombie c = is_zombie c'"
by (simp add: cap_master_cap_def is_cap_simps split: cap.splits)
lemma zobj_refs_def2:
"zobj_refs c = (case c of Zombie _ _ _ \<Rightarrow> {} | _ \<Rightarrow> obj_refs c)"
by (cases c; simp)
lemma cap_master_cap_zobj_refs:
"cap_master_cap c = cap_master_cap c' \<Longrightarrow> zobj_refs c = zobj_refs c'"
by (clarsimp simp add: cap_master_cap_def
intro!: master_arch_cap_obj_refs[THEN arg_cong[where f=set_option]]
split: cap.splits)
lemma caps_of_state_obj_refs:
"\<lbrakk> caps_of_state s p = Some cap; r \<in> obj_refs cap; valid_objs s \<rbrakk>
\<Longrightarrow> \<exists>ko. kheap s r = Some ko"
apply (subgoal_tac "valid_cap cap s")
prefer 2
apply (rule cte_wp_valid_cap)
apply (erule caps_of_state_cteD)
apply assumption
apply (cases cap, auto simp: valid_cap_def obj_at_def
dest: obj_ref_is_arch
split: option.splits)
done
locale mdb_insert_abs =
fixes m src dest
assumes neq: "src \<noteq> dest"
assumes dest: "m dest = None"
assumes desc: "descendants_of dest m = {}"
locale mdb_insert_abs_sib = mdb_insert_abs +
fixes n
defines "n \<equiv> m(dest := m src)"
context mdb_insert_abs begin
lemma dest_no_parent_trancl [iff]:
"(m \<Turnstile> dest \<rightarrow> p) = False" using desc
by (simp add: descendants_of_def del: split_paired_All)
lemma dest_no_parent [iff]:
"(m \<Turnstile> dest \<leadsto> p) = False"
by (fastforce dest: r_into_trancl)
lemma dest_no_parent_d [iff]:
"(m p = Some dest) = False"
apply clarsimp
apply (fold cdt_parent_defs)
apply simp
done
lemma dest_no_child [iff]:
"(m \<Turnstile> p \<leadsto> dest) = False" using dest
by (simp add: cdt_parent_defs)
lemma dest_no_child_trancl [iff]:
"(m \<Turnstile> p \<rightarrow> dest) = False"
by (clarsimp dest!: tranclD2)
lemma descendants_child:
"descendants_of x (m(dest \<mapsto> src)) =
(if src \<in> descendants_of x m \<or> x = src
then descendants_of x m \<union> {dest} else descendants_of x m)"
apply (rule descendants_of_insert_child')
apply (rule desc)
apply (rule neq)
apply (rule dest)
done
lemma descendants_inc:
assumes dinc: "descendants_inc m cs"