-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathADT_C.thy
1469 lines (1332 loc) · 61 KB
/
ADT_C.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)
*)
theory ADT_C
imports
Schedule_C
"../refine/BCorres2_AI"
begin
definition
exec_C :: "(cstate, int, strictc_errortype) body \<Rightarrow>
(cstate, int, strictc_errortype) com \<Rightarrow>
(cstate,unit) nondet_monad"
where
"exec_C \<Gamma> c \<equiv> \<lambda>s. ({()} \<times> {s'. \<Gamma> \<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal s'},
\<exists>xs. xs \<notin> range Normal \<and> \<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> xs)"
definition
ct_running_C :: "cstate \<Rightarrow> bool"
where
"ct_running_C s \<equiv> let
g = globals s;
hp = clift (t_hrs_' g);
ct = ksCurThread_' g
in \<exists>tcb. hp ct = Some tcb \<and>
tsType_CL (thread_state_lift (tcbState_C tcb)) = scast ThreadState_Running"
context kernel_m
begin
definition
"callKernel_C e \<equiv> case e of
SyscallEvent n \<Rightarrow> exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall(syscall_from_H n))
| UnknownSyscall n \<Rightarrow> exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUnknownSyscall(of_nat n))
| UserLevelFault w1 w2 \<Rightarrow> exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault(w1,w2))
| Interrupt \<Rightarrow> exec_C \<Gamma> (Call handleInterruptEntry_'proc)
| VMFaultEvent t \<Rightarrow> exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent(vm_fault_type_from_H t))"
definition
"callKernel_withFastpath_C e \<equiv>
if e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyWait
then exec_C \<Gamma> (\<acute>cptr :== CALL getRegister(\<acute>ksCurThread, scast capRegister);;
\<acute>msgInfo :== CALL getRegister(\<acute>ksCurThread, scast msgInfoRegister);;
IF e = SyscallEvent syscall.SysCall
THEN CALL fastpath_call(\<acute>cptr, \<acute>msgInfo)
ELSE CALL fastpath_reply_wait(\<acute>cptr, \<acute>msgInfo) FI)
else callKernel_C e"
definition
setContext_C :: "user_context_C \<Rightarrow> tcb_C ptr \<Rightarrow> (cstate,unit) nondet_monad"
where
"setContext_C ct thread \<equiv>
exec_C \<Gamma> (\<acute>t_hrs :== hrs_mem_update (heap_update (Ptr &(thread\<rightarrow>[''tcbContext_C''])) ct) \<acute>t_hrs)"
lemma Basic_sem_eq:
"\<Gamma>\<turnstile>\<langle>Basic f,s\<rangle> \<Rightarrow> s' = ((\<exists>t. s = Normal t \<and> s' = Normal (f t)) \<or> (\<forall>t. s \<noteq> Normal t \<and> s' = s))"
apply (rule iffI)
apply (erule exec_elim_cases, simp_all)[1]
apply clarsimp
apply (erule disjE)
apply clarsimp
apply (rule exec.Basic)
apply clarsimp
apply (cases s, auto)
done
lemma setContext_C_corres:
"\<lbrakk> ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t \<rbrakk> \<Longrightarrow>
corres_underlying rf_sr nf dc (tcb_at' t) \<top>
(threadSet (\<lambda>tcb. tcb \<lparr> tcbContext := tc \<rparr>) t) (setContext_C tc' t')"
apply (simp add: setContext_C_def exec_C_def Basic_sem_eq corres_underlying_def)
apply clarsimp
apply (simp add: threadSet_def bind_assoc split_def exec_gets)
apply (drule (1) obj_at_cslift_tcb)
apply clarsimp
apply (frule getObject_eq [rotated -1], simp)
apply (simp add: objBits_simps)
apply (simp add: NonDetMonad.bind_def split_def)
apply (rule bexI)
prefer 2
apply assumption
apply simp
apply (frule setObject_eq [rotated -1], simp)
apply (simp add: objBits_simps)
apply (simp add: objBits_simps)
apply clarsimp
apply (rule bexI)
prefer 2
apply assumption
apply clarsimp
apply (clarsimp simp: typ_heap_simps')
apply (thin_tac "(?a,?b) \<in> fst ?t")+
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def
carch_state_relation_def cmachine_state_relation_def
typ_heap_simps' update_tcb_map_tos)
apply (simp add: map_to_ctes_upd_tcb_no_ctes map_to_tcbs_upd tcb_cte_cases_def)
apply (simp add: cep_relations_drop_fun_upd)
apply (rule conjI)
defer
apply (erule cready_queues_relation_not_queue_ptrs)
apply (rule ext, simp split: split_if)
apply (rule ext, simp split: split_if)
apply (drule ko_at_projectKO_opt)
apply (erule (2) cmap_relation_upd_relI)
apply (simp add: ctcb_relation_def)
apply assumption
apply simp
done
end
definition
"register_to_H \<equiv> inv register_from_H"
definition
to_user_context_C :: "user_context \<Rightarrow> user_context_C"
where
"to_user_context_C uc \<equiv> user_context_C (FCP (\<lambda>r. uc (register_to_H (of_nat r))))"
context kernel_m begin
lemma ccontext_rel_to_C:
"ccontext_relation uc (to_user_context_C uc)"
apply (clarsimp simp: ccontext_relation_def to_user_context_C_def fcp_beta)
apply (rule arg_cong [where f=uc])
apply (simp add: register_to_H_def inv_def)
done
end
definition
from_user_context_C :: "user_context_C \<Rightarrow> user_context"
where
"from_user_context_C uc \<equiv> \<lambda>r. index (registers_C uc) (unat (register_from_H r))"
definition
getContext_C :: "tcb_C ptr \<Rightarrow> cstate \<Rightarrow> user_context"
where
"getContext_C thread \<equiv>
\<lambda>s. from_user_context_C (the (clift (t_hrs_' (globals s)) (Ptr &(thread\<rightarrow>[''tcbContext_C'']))))"
lemma from_user_context_C:
"ccontext_relation uc uc' \<Longrightarrow> from_user_context_C uc' = uc"
by (auto simp: ccontext_relation_def from_user_context_C_def intro: ext)
context kernel_m begin
definition
kernelEntry_C ::
"bool \<Rightarrow> event \<Rightarrow> user_context \<Rightarrow> (cstate, user_context) nondet_monad"
where
"kernelEntry_C fp e tc \<equiv> do
t \<leftarrow> gets (ksCurThread_' o globals);
setContext_C (to_user_context_C tc) t;
if fp then callKernel_withFastpath_C e else callKernel_C e;
t \<leftarrow> gets (ksCurThread_' o globals);
gets $ getContext_C t
od"
definition
"kernel_call_C fp e \<equiv>
{(s, m, s'). s' \<in> fst (split (kernelEntry_C fp e) s) \<and>
m = (if ct_running_C (snd s') then UserMode else IdleMode)
\<or> snd (split (kernelEntry_C fp e) s)}"
definition
"getActiveIRQ_C \<equiv> exec_C \<Gamma> (Call getActiveIRQ_'proc)"
definition
checkActiveIRQ_C :: "(cstate, bool) nondet_monad"
where
"checkActiveIRQ_C \<equiv>
do getActiveIRQ_C;
irq \<leftarrow> gets ret__unsigned_long_';
return (irq \<noteq> scast irqInvalid)
od"
definition
check_active_irq_C :: "((user_context \<times> cstate) \<times> bool \<times> (user_context \<times> cstate)) set"
where
"check_active_irq_C \<equiv> {((tc, s), irq_raised, (tc, s')). (irq_raised, s') \<in> fst (checkActiveIRQ_C s)}"
end
(*Restrict our undefined initial state to only use the nondeterministic state*)
consts
Init_C' :: "unit observable \<Rightarrow> cstate global_state set"
definition "Init_C \<equiv> \<lambda>((tc,s),m,e). Init_C' ((tc, truncate_state s),m,e)"
definition
user_mem_C :: "globals \<Rightarrow> word32 \<Rightarrow> word8 option"
where
"user_mem_C s \<equiv> \<lambda>p.
case clift (t_hrs_' s) (Ptr (p && ~~mask pageBits)) of
Some v \<Rightarrow> let off = p && mask pageBits >> 2;
w = index (user_data_C.words_C v) (unat off);
i = 3 - unat (p && mask 2);
bs = (word_rsplit w :: word8 list)
in Some (bs!i)
| None \<Rightarrow> None"
(* FIXME: move to somewhere sensible *)
definition
"setUserMem_C um \<equiv>
modify (\<lambda>s. s\<lparr>globals := (globals s)\<lparr>t_hrs_' :=
(%p. case um p of None \<Rightarrow> fst (t_hrs_' (globals s)) p | Some x \<Rightarrow> x,
snd (t_hrs_' (globals s))) \<rparr>\<rparr>)"
lemma setUserMem_C_def_foldl:
"setUserMem_C um \<equiv>
modify (\<lambda>s. s\<lparr>globals := (globals s)\<lparr>t_hrs_' :=
(foldl (%f p. f(p := the (um p))) (fst (t_hrs_' (globals s)))
(filter (%p. p : dom um) enum),
snd (t_hrs_' (globals s))) \<rparr>\<rparr>)"
apply (rule eq_reflection)
apply (simp add: setUserMem_C_def)
apply (rule arg_cong[where f=modify])
apply (rule ext)
apply (rule_tac f=globals_update in arg_cong2)
apply (rule ext)
apply (rule_tac f=t_hrs_'_update in arg_cong2)
apply (rule ext)
apply simp_all
apply (rule ext)
apply (simp add: foldl_fun_upd_value)
apply (intro conjI impI)
apply clarsimp
apply (clarsimp split: option.splits)
done
(* FIXME: move *_to_H to StateRelation_C.thy? *)
definition
"cscheduler_action_to_H p \<equiv>
if p = NULL then ResumeCurrentThread
else if p = Ptr (~~ 0) then ChooseNewThread
else SwitchToThread (ctcb_ptr_to_tcb_ptr p)"
(* FIXME: move *)
lemma max_word_neq_0[simp]: "max_word \<noteq> 0"
apply (clarsimp simp: max_word_def)
apply (case_tac "len_of TYPE('a)")
apply clarsimp
apply (metis eq_iff_diff_eq_0 max_word_def max_word_eq word_pow_0 zero_neq_one)
done
lemma csch_act_rel_to_H:
"(\<forall>t. a = SwitchToThread t \<longrightarrow> is_aligned t 9) \<Longrightarrow>
cscheduler_action_relation a p \<longleftrightarrow> cscheduler_action_to_H p = a"
apply (cases a)
apply (simp_all add: cscheduler_action_relation_def
cscheduler_action_to_H_def)
apply safe
apply (simp_all add: tcb_ptr_to_ctcb_ptr_def ctcb_ptr_to_tcb_ptr_def
ctcb_offset_def is_aligned_mask mask_def max_word_def)
apply (word_bitwise, simp)
done
definition
cirqstate_to_H :: "word32 \<Rightarrow> irqstate"
where
"cirqstate_to_H w \<equiv>
if w = scast Kernel_C.IRQNotifyAEP then irqstate.IRQNotifyAEP
else if w = scast Kernel_C.IRQTimer then irqstate.IRQTimer
else irqstate.IRQInactive"
lemma cirqstate_cancel:
"cirqstate_to_H \<circ> irqstate_to_C = id"
apply (rule ext)
apply (case_tac x)
apply (auto simp: cirqstate_to_H_def Kernel_C.IRQInactive_def
Kernel_C.IRQTimer_def Kernel_C.IRQNotifyAEP_def)
done
definition
"cint_state_to_H cnode cirqs \<equiv>
InterruptState (ptr_val cnode)
(\<lambda>i::word8. if i \<le> scast Platform.maxIRQ then cirqstate_to_H (index cirqs (unat i))
else irqstate.IRQInactive)"
lemma cint_rel_to_H:
"irqs_masked' s \<Longrightarrow>
cinterrupt_relation (ksInterruptState s) n t \<Longrightarrow>
cint_state_to_H n t = (ksInterruptState s)"
apply (simp add: irqs_masked'_def)
apply (cases "ksInterruptState s")
apply (clarsimp simp: cinterrupt_relation_def cint_state_to_H_def
Platform.maxIRQ_def Kernel_C.maxIRQ_def)
apply (rule ext)
apply clarsimp
apply (drule spec, erule impE, assumption)
apply (drule_tac s="irqstate_to_C (fun i)" in sym,
simp add: cirqstate_cancel[THEN fun_cong, simplified])
done
definition
"cstate_to_machine_H s \<equiv>
(phantom_machine_state_' s)\<lparr>underlying_memory := option_to_0 \<circ> user_mem_C s\<rparr>"
lemma projectKO_opt_UserData [simp]:
"projectKO_opt KOUserData = Some UserData"
by (simp add: projectKO_opts_defs)
lemma ucast_ucast_mask_pageBits_shift:
"ucast (ucast (p && mask pageBits >> 2) :: 10 word) = p && mask pageBits >> 2"
apply (rule word_eqI)
apply (auto simp: word_size nth_ucast nth_shiftr pageBits_def)
done
lemma unat_ucast_mask_pageBits_shift:
"unat (ucast (p && mask pageBits >> 2) :: 10 word) = unat ((p::word32) && mask pageBits >> 2)"
apply (simp only: unat_ucast)
apply (rule mod_less)
apply (rule unat_less_power)
apply (simp add: word_bits_def)
apply (rule shiftr_less_t2n)
apply (rule order_le_less_trans [OF word_and_le1])
apply (simp add: pageBits_def mask_def)
done
lemma mask_pageBits_shift_sum:
"unat n = unat (p && mask 2) \<Longrightarrow>
(p && ~~ mask pageBits) + (p && mask pageBits >> 2) * 4 + n = (p::word32)"
apply (clarsimp simp: word32_shift_by_2)
apply (subst word_plus_and_or_coroll)
apply (rule word_eqI)
apply (clarsimp simp: word_size pageBits_def nth_shiftl nth_shiftr word_ops_nth_size)
apply arith
apply (subst word_plus_and_or_coroll)
apply (rule word_eqI)
apply (clarsimp simp: word_size pageBits_def nth_shiftl nth_shiftr word_ops_nth_size)
apply (rule word_eqI)
apply (clarsimp simp: word_size pageBits_def nth_shiftl nth_shiftr word_ops_nth_size)
apply (auto simp: linorder_not_less SucSucMinus)
done
lemma user_mem_C_relation:
"\<lbrakk>cpspace_user_data_relation (ksPSpace s')
(underlying_memory (ksMachineState s')) (t_hrs_' s);
pspace_distinct' s'\<rbrakk>
\<Longrightarrow> user_mem_C s = user_mem' s'"
apply (rule ext)
apply (rename_tac p)
apply (clarsimp simp: user_mem_C_def user_mem'_def
split: if_splits option.splits)
apply (rule conjI)
apply clarsimp
apply (clarsimp simp: pointerInUserData_def)
apply (drule user_data_at_ko)
apply (clarsimp simp: cmap_relation_def)
apply (subgoal_tac "(Ptr (p && ~~mask pageBits) :: user_data_C ptr) \<in>
Ptr ` dom (heap_to_page_data (ksPSpace s') (underlying_memory (ksMachineState s')))")
apply simp
apply clarsimp
apply (thin_tac "Ball ?A ?P")
apply (thin_tac "?t = dom (clift (t_hrs_' s))")
apply (rule imageI)
apply (clarsimp simp: dom_def heap_to_page_data_def obj_at'_def projectKOs)
apply (clarsimp simp: pointerInUserData_def)
apply (clarsimp simp: cmap_relation_def)
apply (drule equalityD2)
apply (drule subsetD)
apply (fastforce simp: dom_def)
apply clarsimp
apply (drule bspec)
apply (fastforce simp: dom_def)
apply (clarsimp simp: heap_to_page_data_def map_comp_def projectKOs
split: option.splits)
apply (rule conjI)
prefer 2
apply (clarsimp simp: typ_at'_def ko_wp_at'_def objBitsKO_def)
apply (drule pspace_distinctD')
apply fastforce
apply (clarsimp simp: objBitsKO_def)
apply clarsimp
apply (clarsimp simp: cuser_data_relation_def byte_to_word_heap_def Let_def)
apply (erule_tac x="ucast (p && mask pageBits >> 2)" in allE)
apply (simp add: ucast_ucast_mask_pageBits_shift unat_ucast_mask_pageBits_shift)
apply (rotate_tac -1)
apply (drule sym)
apply (simp add: word_rsplit_rcat_size word_size)
apply (case_tac "unat (p && mask 2)")
apply (simp add: mask_pageBits_shift_sum [where n=0, simplified])
apply (case_tac "nat")
apply (simp add: mask_pageBits_shift_sum [where n=1, simplified])
apply (case_tac "nata")
apply (simp add: mask_pageBits_shift_sum [where n=2, simplified])
apply (case_tac "natb")
apply (simp add: mask_pageBits_shift_sum [where n=3, simplified])
apply clarsimp
apply (subgoal_tac "unat (p && mask 2) < unat (2^2::word32)")
apply simp
apply (fold word_less_nat_alt)
apply (rule and_mask_less_size)
apply (clarsimp simp: word_size)
done
lemma
assumes vms': "valid_machine_state' a"
assumes mach_rel: "cmachine_state_relation (ksMachineState a) s"
assumes um_rel:
"cpspace_user_data_relation (ksPSpace a)
(underlying_memory (ksMachineState a)) (t_hrs_' s)"
"pspace_distinct' a"
shows cstate_to_machine_H_correct: "cstate_to_machine_H s = ksMachineState a"
proof -
have "underlying_memory (ksMachineState a) = option_to_0 \<circ> user_mem' a"
apply (rule ext)
using vms'[simplified valid_machine_state'_def]
by (auto simp: user_mem'_def option_to_0_def
split: option.splits split_if_asm)
with mach_rel[simplified cmachine_state_relation_def]
user_mem_C_relation[OF um_rel]
show ?thesis by (simp add: cstate_to_machine_H_def)
qed
definition
"array_to_map n c \<equiv> \<lambda>i. if i\<le>n then Some (index c (unat i)) else None"
lemma array_relation_to_map:
"array_relation r n a c \<Longrightarrow> \<forall>i\<le>n. r (a i) (the (array_to_map n c i))"
by (simp add: array_relation_def array_to_map_def)
lemma dom_array_to_map[simp]: "dom (array_to_map n c) = {i. i\<le>n}"
by (simp add: array_to_map_def dom_def)
lemma ran_array_to_map:
"ran (array_to_map n c) = {y. \<exists>i\<le>n. index c (unat i) = y}"
by (auto simp: array_to_map_def ran_def Collect_eq)
text {* Note: Sometimes, @{text array_map_conv} might be more convenient
in conjunction with @{const array_relation}. *}
definition "array_map_conv f n c \<equiv> map_comp f (array_to_map n c)"
lemma array_map_conv_def2:
"array_map_conv f n c \<equiv> \<lambda>i. if i\<le>n then f (index c (unat i)) else None"
by (rule eq_reflection, rule ext) (simp add: array_map_conv_def map_comp_def
array_to_map_def)
lemma array_relation_map_conv:
"array_relation r n a c \<Longrightarrow> \<forall>x y. r y x \<longrightarrow> (f x) = y \<Longrightarrow>
\<forall>i>n. a i = None \<Longrightarrow> array_map_conv f n c = a"
by (rule ext) (simp add: array_relation_def array_map_conv_def2)
lemma array_relation_map_conv2:
"array_relation r n a c \<Longrightarrow> \<forall>x. \<forall>y\<in>range a. r y x \<longrightarrow> (f x) = y \<Longrightarrow>
\<forall>i>n. a i = None \<Longrightarrow> array_map_conv f n c = a"
by (rule ext) (simp add: array_relation_def array_map_conv_def2)
lemma array_map_conv_Some[simp]: "array_map_conv Some n c = array_to_map n c"
by (simp add: array_map_conv_def map_comp_def)
lemma map_comp_array_map_conv_comm:
"map_comp f (array_map_conv g n c) = array_map_conv (map_comp f g) n c"
by (rule ext) (simp add: array_map_conv_def2 Option.map_def map_comp_def)
lemma ran_array_map_conv:
"ran (array_map_conv f n c) = {y. \<exists>i\<le>n. f (index c (unat i)) = Some y}"
by (auto simp add: array_map_conv_def2 ran_def Collect_eq)
(* FIXME: move to somewhere sensible >>> *)
text {* Map inversion (implicitly assuming injectivity). *}
definition
"the_inv_map m = (\<lambda>s. if s\<in>ran m then Some (THE x. m x = Some s) else None)"
text {* Map inversion can be expressed by function inversion. *}
lemma the_inv_map_def2:
"the_inv_map m = (Some \<circ> the_inv_into (dom m) (the \<circ> m)) |` (ran m)"
apply (rule ext)
apply (clarsimp simp: the_inv_map_def the_inv_into_def dom_def)
apply (rule_tac f=The in arg_cong)
apply (rule ext)
apply auto
done
text {* The domain of a function composition with Some is the universal set. *}
lemma dom_comp_Some[simp]: "dom (comp Some f) = UNIV" by (simp add: dom_def)
text {* Assuming injectivity, map inversion produces an inversive map. *}
lemma is_inv_the_inv_map:
"inj_on m (dom m) \<Longrightarrow> is_inv m (the_inv_map m)"
apply (simp add: is_inv_def)
apply (intro conjI allI impI)
apply (simp add: the_inv_map_def2)
apply (auto simp add: the_inv_map_def inj_on_def dom_def)
done
lemma the_the_inv_mapI:
"inj_on m (dom m) \<Longrightarrow> m x = Some y \<Longrightarrow> the (the_inv_map m y) = x"
by (auto simp: the_inv_map_def ran_def inj_on_def dom_def)
lemma eq_restrict_map_None[simp]:
"restrict_map m A x = None \<longleftrightarrow> x ~: (A \<inter> dom m)"
by (auto simp: restrict_map_def split: split_if_asm)
lemma eq_the_inv_map_None[simp]: "the_inv_map m x = None \<longleftrightarrow> x\<notin>ran m"
by (simp add: the_inv_map_def2)
lemma is_inv_unique:
"is_inv f g \<Longrightarrow> is_inv f h \<Longrightarrow> g=h"
apply (rule ext)
apply (clarsimp simp: is_inv_def dom_def Collect_eq ran_def)
apply (drule_tac x=x in spec)+
apply (case_tac "g x", clarsimp+)
done
lemma assumes A: "is_inv f g" shows the_inv_map_eq: "the_inv_map f = g"
by (simp add: is_inv_unique[OF A A[THEN is_inv_inj, THEN is_inv_the_inv_map]])
(*<<<*)
definition
casid_map_to_H
:: "(word32[256]) \<Rightarrow> (pde_C ptr \<rightharpoonup> pde_C) \<Rightarrow> asid \<rightharpoonup> hw_asid \<times> obj_ref"
where
"casid_map_to_H hw_asid_table pdes \<equiv>
(\<lambda>asid. Option.map
(\<lambda>hw_asid. (hw_asid,
the (the_inv_map (pde_stored_asid \<circ>\<^sub>m pdes \<circ>\<^sub>m
pd_pointer_to_asid_slot) hw_asid)))
(the_inv_map (array_map_conv (\<lambda>x. if x=0 then None else Some x)
0xFF hw_asid_table) asid))"
(* FIXME: move *)
lemma word_le_p2m1:
"(w::'a::len word) <= 2 ^ len_of TYPE('a) - 1" by (simp add: p2len)
(* FIXME: move *)
lemma ran_map_comp_subset: "ran (map_comp f g) <= (ran f)"
by (fastforce simp: map_comp_def ran_def split: option.splits)
(* FIXME: move *)(* NOTE: unused. *)
lemma inj_on_option_map:
"inj_on (Option.map f o m) (dom m) \<Longrightarrow> inj_on m (dom m)"
by (auto simp add: inj_on_def Option.map_def dom_def)
lemma eq_option_to_0_rev:
"Some 0 ~: A \<Longrightarrow> \<forall>x. \<forall>y\<in>A.
(op = \<circ> option_to_0) y x \<longrightarrow> (if x = 0 then None else Some x) = y"
by (clarsimp simp: option_to_0_def split: option.splits)
lemma inj_hwasidsI:
"asid_map_pd_to_hwasids m = Option.set \<circ> c \<Longrightarrow>
inj_on (Option.map snd \<circ> m) (dom m) \<Longrightarrow>
inj_on (Option.map fst \<circ> m) (dom m) \<Longrightarrow>
inj_on c (dom c)"
apply (clarsimp simp: asid_map_pd_to_hwasids_def inj_on_def)
apply (clarsimp simp: fun_eq_iff set_eq_iff)
apply (rename_tac x y z)
apply (frule_tac x=x in spec, drule_tac x=z in spec)
apply (drule_tac x=y in spec, drule_tac x=z in spec)
apply (fastforce simp: ran_def dom_def)
done
lemma (in kernel_m)
assumes valid: "valid_arch_state' astate"
assumes rel: "carch_state_relation (ksArchState astate) cstate"
shows casid_map_to_H_correct:
"casid_map_to_H (armKSHWASIDTable_' cstate) (clift (t_hrs_' cstate)) =
armKSASIDMap (ksArchState astate)"
apply (rule ext)
using valid rel
apply (clarsimp simp: valid_arch_state'_def carch_state_relation_def
casid_map_to_H_def)
apply (drule array_relation_map_conv2[OF _ eq_option_to_0_rev])
apply (fastforce simp: is_inv_def valid_asid_map'_def)
apply clarsimp
apply (cut_tac w=i in word_le_p2m1, simp add: minus_one_norm)
apply clarsimp
apply (case_tac "armKSASIDMap (ksArchState astate) x")
apply (clarsimp simp: ran_array_map_conv option_to_0_def split:option.splits)
apply (fastforce simp: is_inv_def)
apply clarsimp
apply (rule conjI)
apply (frule is_inv_inj)
apply (clarsimp simp: the_inv_map_def is_inv_def dom_option_map
split: split_if)
apply (intro conjI[rotated] impI domI, assumption)
apply (rule the_equality)
apply (clarsimp simp: ran_def dom_def Collect_eq)
apply (drule_tac x=x in spec)
apply (fastforce simp: inj_on_def)
apply (fastforce simp: inj_on_def)
apply (rule the_the_inv_mapI)
apply (frule inj_hwasidsI)
apply (simp add: valid_asid_map'_def)
apply (frule is_inv_inj2, simp add: dom_option_map)
apply simp
apply (thin_tac "array_map_conv ?f ?n ?c = ?a")
apply (clarsimp simp: asid_map_pd_to_hwasids_def ran_def)
apply (subst (asm) fun_eq_iff)
apply fastforce
done
definition (in state_rel)
"carch_state_to_H cstate \<equiv>
ARMKernelState
(symbol_table ''armKSGlobalsFrame'')
(array_map_conv (\<lambda>x. if x=NULL then None else Some (ptr_val x))
(2^asid_high_bits - 1) (armKSASIDTable_' cstate))
(array_map_conv (\<lambda>x. if x=0 then None else Some x) 0xFF
(armKSHWASIDTable_' cstate))
(armKSNextASID_' cstate)
(casid_map_to_H (armKSHWASIDTable_' cstate) (clift (t_hrs_' cstate)))
(symbol_table ''armKSGlobalPD'')
[symbol_table ''armKSGlobalPT'']
armKSKernelVSpace_C"
lemma eq_option_to_ptr_rev:
"Some 0 \<notin> A \<Longrightarrow>
\<forall>x. \<forall>y\<in>A. (op = \<circ> option_to_ptr) y x \<longrightarrow>
(if x=NULL then None else Some (ptr_val x)) = y"
by (auto simp: option_to_ptr_def option_to_0_def split: option.splits)
lemma (in kernel_m) carch_state_to_H_correct:
assumes valid: "valid_arch_state' astate"
assumes rel: "carch_state_relation (ksArchState astate) (cstate)"
assumes gpts: "armKSGlobalPTs (ksArchState astate) =
[symbol_table ''armKSGlobalPT'']"
shows "carch_state_to_H cstate = ksArchState astate"
apply (case_tac "ksArchState astate", simp)
apply (rename_tac v0 v1 v2 v3 v4 v5 v6 v7)
using gpts rel[simplified carch_state_relation_def carch_globals_def]
apply (clarsimp simp: carch_state_to_H_def
casid_map_to_H_correct[OF valid rel])
apply (rule conjI[rotated])
apply (rule array_relation_map_conv2[OF _ eq_option_to_0_rev])
apply assumption
using valid[simplified valid_arch_state'_def]
apply (fastforce simp: is_inv_def valid_asid_map'_def)
apply clarsimp
apply (cut_tac w=i in word_le_p2m1, simp add: minus_one_norm)
apply (rule array_relation_map_conv2[OF _ eq_option_to_ptr_rev])
apply assumption
using valid[simplified valid_arch_state'_def]
apply (fastforce simp: valid_asid_table'_def)
using valid[simplified valid_arch_state'_def]
apply (fastforce simp: valid_asid_table'_def)
done
lemma tcb_queue_rel_unique:
"hp NULL = None \<Longrightarrow>
tcb_queue_relation gn gp hp as pp cp \<Longrightarrow>
tcb_queue_relation gn gp hp as' pp cp \<Longrightarrow> as' = as"
proof (induct as arbitrary: as' pp cp)
case Nil thus ?case by (cases as', simp+)
next
case (Cons x xs) thus ?case
by (cases as') (clarsimp simp: tcb_ptr_to_ctcb_ptr_def)+
qed
lemma tcb_queue_rel'_unique:
"hp NULL = None \<Longrightarrow>
tcb_queue_relation' gn gp hp as pp cp \<Longrightarrow>
tcb_queue_relation' gn gp hp as' pp cp \<Longrightarrow> as' = as"
apply (clarsimp simp: tcb_queue_relation'_def split: split_if_asm)
apply (clarsimp simp: neq_Nil_conv)
apply (clarsimp simp: neq_Nil_conv)
apply (erule(2) tcb_queue_rel_unique)
done
lemma cqueues_unique:
"h_tcb NULL = None \<Longrightarrow>
cready_queues_relation h_tcb cs as \<Longrightarrow>
cready_queues_relation h_tcb cs as' \<Longrightarrow> as' = as"
oops (*
apply (clarsimp simp add: cready_queues_relation_def Let_def fun_eq_iff)
apply (rename_tac qdom prio)
apply (erule_tac x=qdom in allE)
apply (erule_tac x=qdom in allE)
apply (erule_tac x=prio in allE)+
apply clarsimp
apply (cut_tac w=qdom in word_le_p2m1)
apply (cut_tac w=prio in word_le_p2m1, simp add: seL4_MinPrio_def seL4_MaxPrio_def minus_one_norm)
apply (cut_tac w=prio in word_le_p2m1)
apply (simp add: seL4_MinPrio_def seL4_MaxPrio_def minDom_def maxDom_def minus_one_norm)
apply (clarsimp simp add: tcb_queue_relation'_def tcb_queue_rel_unique)
done
*)
definition
cready_queues_to_H
:: "(tcb_C ptr \<rightharpoonup> tcb_C) \<Rightarrow> (tcb_queue_C[4096]) \<Rightarrow> word8 \<times> word8 \<Rightarrow> word32 list"
where
"cready_queues_to_H h_tcb cs \<equiv> \<lambda>(qdom, prio). if ucast minDom \<le> qdom \<and> qdom \<le> ucast maxDom
\<and> ucast seL4_MinPrio \<le> prio \<and> prio \<le> ucast seL4_MaxPrio
then THE aq. let cqueue = index cs (cready_queues_index_to_C qdom prio)
in sched_queue_relation' h_tcb aq (head_C cqueue) (StateRelation_C.end_C cqueue)
else []"
lemma cready_queues_to_H_correct:
"cready_queues_relation (clift s) cs as \<Longrightarrow>
cready_queues_to_H (clift s) cs = as"
apply (clarsimp simp: cready_queues_to_H_def cready_queues_relation_def
fun_eq_iff)
apply (rule the_equality)
apply simp
apply (clarsimp simp: Let_def)
apply (rule_tac hp="clift s" in tcb_queue_rel'_unique, simp_all add: lift_t_NULL)
done
(* showing that cpspace_relation is actually unique >>>*)
(* FIXME: move *)
lemma inj_image_inv:
assumes inj_f: "inj f"
shows "f ` A = B \<Longrightarrow> inv f ` B = A"
by (drule sym) (simp add: inv_image_comp[OF inj_f])
lemma cmap_relation_unique:
assumes inj_f: "inj f"
assumes r: "\<And>x y z. r x z \<Longrightarrow> r y z \<Longrightarrow> x=y"
shows "cmap_relation a c f r \<Longrightarrow> cmap_relation a' c f r \<Longrightarrow> a' = a"
(is "PROP ?goal")
apply (clarsimp simp add: cmap_relation_def)
apply (drule inj_image_inv[OF inj_f])+
apply simp
apply (rule ext)
apply (case_tac "x:dom a")
apply (drule bspec, assumption)+
apply (simp add: dom_def Collect_eq, drule_tac x=x in spec)
apply (drule (1) r)
apply clarsimp
apply fastforce
done
lemma cpspace_cte_relation_unique:
assumes "cpspace_cte_relation ah ch" "cpspace_cte_relation ah' ch"
shows "map_to_ctes ah' = map_to_ctes ah"
apply (rule cmap_relation_unique[OF inj_Ptr _ assms])
by (clarsimp simp: ccte_relation_def Some_the[symmetric]) (drule sym, simp)
lemma inj_tcb_ptr_to_ctcb_ptr: "inj tcb_ptr_to_ctcb_ptr"
by (simp add: inj_on_def tcb_ptr_to_ctcb_ptr_def)
lemma ccontext_relation_imp_eq:
"ccontext_relation f x \<Longrightarrow> ccontext_relation g x \<Longrightarrow> f=g"
by (rule ext) (simp add: ccontext_relation_def)
(* FIXME: move *)
lemma ran_tcb_cte_cases:
"ran tcb_cte_cases =
{(Structures_H.tcbCTable, tcbCTable_update),
(Structures_H.tcbVTable, tcbVTable_update),
(Structures_H.tcbReply, tcbReply_update),
(Structures_H.tcbCaller, tcbCaller_update),
(tcbIPCBufferFrame, tcbIPCBufferFrame_update)}"
by (auto simp add: tcb_cte_cases_def split: split_if_asm)
(* FIXME: move *)
lemma ps_clear_is_aligned_ksPSpace_None:
"\<lbrakk>ps_clear p n s; is_aligned p n; 0<d; d \<le> mask n\<rbrakk>
\<Longrightarrow> ksPSpace s (p + d) = None"
apply (simp add: ps_clear_def add_diff_eq[symmetric] mask_2pm1[symmetric])
apply (drule equals0D[where a="p + d"])
apply (simp add: dom_def word_gt_0)
apply (drule mp)
apply (rule word_plus_mono_right)
apply simp
apply (simp add: mask_2pm1)
apply (erule is_aligned_no_overflow')
apply (drule mp)
apply (case_tac "(0\<Colon>word32)<2^n")
apply (frule le_m1_iff_lt[of "(2::word32)^n" d, THEN iffD1])
apply (simp add: mask_2pm1[symmetric])
apply (erule (1) is_aligned_no_wrap')
apply (simp add: is_aligned_mask mask_2pm1 not_less word_bits_def
power_overflow)
by assumption
(* FIXME: move *)
lemma ps_clear_32:
"\<lbrakk>ps_clear p 9 s; is_aligned p 9\<rbrakk> \<Longrightarrow> ksPSpace s (p + 0x20) = None"
by (rule ps_clear_is_aligned_ksPSpace_None) (simp add: mask_2pm1)+
lemma ps_clear_64:
"\<lbrakk>ps_clear p 9 s; is_aligned p 9\<rbrakk> \<Longrightarrow> ksPSpace s (p + 0x30) = None"
by (rule ps_clear_is_aligned_ksPSpace_None) (simp add: mask_2pm1)+
lemma ps_clear_128:
"\<lbrakk>ps_clear p 9 s; is_aligned p 9\<rbrakk> \<Longrightarrow> ksPSpace s (p + 0x40) = None"
by (rule ps_clear_is_aligned_ksPSpace_None) (simp add: mask_2pm1)+
lemma map_to_ctes_tcb_ctes:
notes if_cong[cong]
shows
"ctes_of s' = ctes_of s \<Longrightarrow>
ko_at' tcb p s \<Longrightarrow> ko_at' tcb' p s' \<Longrightarrow>
\<forall>x\<in>ran tcb_cte_cases. fst x tcb' = fst x tcb"
apply (clarsimp simp add: ran_tcb_cte_cases)
apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKO_opt_tcb
split: kernel_object.splits)
apply (case_tac ko, simp_all, clarsimp)
apply (clarsimp simp: objBits_type[of "KOTCB tcb" "KOTCB undefined"]
objBits_type[of "KOTCB tcb'" "KOTCB undefined"])
apply (rule conjI)
apply (drule ps_clear_def3[THEN iffD1,rotated 2],
assumption, simp add: objBitsKO_def)+
apply (clarsimp simp: map_to_ctes_def Let_def fun_eq_iff)
apply (drule_tac x=p in spec, simp)
apply (rule conjI)
apply (clarsimp simp: map_to_ctes_def Let_def fun_eq_iff)
apply (drule_tac x="p+0x10" in spec, simp add: objBitsKO_def)
apply (frule_tac s1=s in ps_clear_def3[THEN iffD1,rotated 2],
assumption, simp add: objBitsKO_def)
apply (frule_tac s1=s' in ps_clear_def3[THEN iffD1,rotated 2],
assumption, simp add: objBitsKO_def)
apply (drule (1) ps_clear_16)+
apply (simp add: is_aligned_add_helper[of _ 9 "0x10", simplified] split_def
objBitsKO_def)
apply (rule conjI)
apply (clarsimp simp: map_to_ctes_def Let_def fun_eq_iff)
apply (drule_tac x="p+0x20" in spec, simp add: objBitsKO_def)
apply (frule_tac s1=s in ps_clear_def3[THEN iffD1,rotated 2],
assumption, simp add: objBitsKO_def)
apply (frule_tac s1=s' in ps_clear_def3[THEN iffD1,rotated 2],
assumption, simp add: objBitsKO_def)
apply (drule (1) ps_clear_32)+
apply (simp add: is_aligned_add_helper[of _ 9 "0x20", simplified] split_def
objBitsKO_def)
apply (rule conjI)
apply (clarsimp simp: map_to_ctes_def Let_def fun_eq_iff)
apply (drule_tac x="p+0x30" in spec, simp add: objBitsKO_def)
apply (frule_tac s1=s in ps_clear_def3[THEN iffD1,rotated 2],
assumption, simp add: objBitsKO_def)
apply (frule_tac s1=s' in ps_clear_def3[THEN iffD1,rotated 2],
assumption, simp add: objBitsKO_def)
apply (drule (1) ps_clear_64)+
apply (simp add: is_aligned_add_helper[of _ 9 "0x30", simplified] split_def
objBitsKO_def)
apply (clarsimp simp: map_to_ctes_def Let_def fun_eq_iff)
apply (drule_tac x="p+0x40" in spec, simp add: objBitsKO_def)
apply (frule_tac s1=s in ps_clear_def3[THEN iffD1,rotated 2],
assumption, simp add: objBitsKO_def)
apply (frule_tac s1=s' in ps_clear_def3[THEN iffD1,rotated 2],
assumption, simp add: objBitsKO_def)
apply (drule (1) ps_clear_128)+
apply (simp add: is_aligned_add_helper[of _ 9 "0x40", simplified] split_def
objBitsKO_def)
done
lemma cfault_rel_imp_eq:
"cfault_rel x a b \<Longrightarrow> cfault_rel y a b \<Longrightarrow> x=y"
by (clarsimp simp: cfault_rel_def is_cap_fault_def
split: split_if_asm fault_CL.splits)
lemma cthread_state_rel_imp_eq:
"cthread_state_relation x z \<Longrightarrow> cthread_state_relation y z \<Longrightarrow> x=y"
apply (simp add: cthread_state_relation_def split_def)
apply (cases x)
apply (cases y, simp_all add: ThreadState_BlockedOnReceive_def
ThreadState_BlockedOnReply_def ThreadState_BlockedOnAsyncEvent_def
ThreadState_Running_def ThreadState_Inactive_def
ThreadState_IdleThreadState_def ThreadState_BlockedOnSend_def
ThreadState_Restart_def)+
done
lemma cpspace_tcb_relation_unique:
assumes tcbs: "cpspace_tcb_relation ah ch" "cpspace_tcb_relation ah' ch"
assumes ctes: " \<forall>tcb tcb'. (\<exists>p. map_to_tcbs ah p = Some tcb \<and>
map_to_tcbs ah' p = Some tcb') \<longrightarrow>
(\<forall>x\<in>ran tcb_cte_cases. fst x tcb' = fst x tcb)"
shows "map_to_tcbs ah' = map_to_tcbs ah"
using tcbs(2) tcbs(1)
apply (clarsimp simp add: cmap_relation_def)
apply (drule inj_image_inv[OF inj_tcb_ptr_to_ctcb_ptr])+
apply (simp add: tcb_ptr_to_ctcb_ptr_def[abs_def] ctcb_offset_def)
apply (rule ext)
apply (case_tac "x:dom (map_to_tcbs ah)")
apply (drule bspec, assumption)+
apply (simp add: dom_def Collect_eq, drule_tac x=x in spec)
apply clarsimp
apply (rename_tac p x y)
apply (cut_tac ctes)
apply (drule_tac x=x in spec, drule_tac x=y in spec, erule impE, fastforce)
apply (thin_tac "map_to_tcbs ?x ?y = Some ?z")+
apply (case_tac x, case_tac y, case_tac "the (clift ch (tcb_Ptr (p+0x100)))")
apply (clarsimp simp: ctcb_relation_def ran_tcb_cte_cases)
apply (drule up_ucast_inj_eq[THEN iffD1,rotated], simp+)
apply (auto simp: cfault_rel_imp_eq cthread_state_rel_imp_eq
ccontext_relation_imp_eq up_ucast_inj_eq)
done
lemma tcb_queue_rel_clift_unique:
"tcb_queue_relation gn gp (clift s) as pp cp \<Longrightarrow>
tcb_queue_relation gn gp (clift s) as' pp cp \<Longrightarrow> as' = as"
by (rule tcb_queue_rel_unique, rule lift_t_NULL)
lemma tcb_queue_rel'_clift_unique:
"tcb_queue_relation' gn gp (clift s) as pp cp \<Longrightarrow>
tcb_queue_relation' gn gp (clift s) as' pp cp \<Longrightarrow> as' = as"
by (clarsimp simp add: tcb_queue_relation'_def)
(rule tcb_queue_rel_clift_unique)
lemma cpspace_ep_relation_unique:
assumes "cpspace_ep_relation ah ch" "cpspace_ep_relation ah' ch"
shows "map_to_eps ah' = map_to_eps ah"
apply (rule cmap_relation_unique[OF inj_Ptr _ assms])
apply (clarsimp simp: EPState_Idle_def EPState_Recv_def EPState_Send_def
cendpoint_relation_def Let_def tcb_queue_rel'_clift_unique
split: endpoint.splits)
done
lemma cpspace_aep_relation_unique:
assumes "cpspace_aep_relation ah ch" "cpspace_aep_relation ah' ch"
shows "map_to_aeps ah' = map_to_aeps ah"
apply (rule cmap_relation_unique[OF inj_Ptr _ assms])
by (clarsimp simp: AEPState_Active_def AEPState_Idle_def AEPState_Waiting_def
casync_endpoint_relation_def Let_def tcb_queue_rel'_clift_unique
split: async_endpoint.splits)
(* FIXME: move *)
lemma of_bool_inject[iff]: "of_bool a = of_bool b \<longleftrightarrow> a=b"
by (cases a) (cases b, simp_all)+
(* FIXME: move *)
lemma ap_from_vm_rights_inject[iff]:
"(ap_from_vm_rights a::word32) = ap_from_vm_rights b \<longleftrightarrow> a=b"
by (simp add: ap_from_vm_rights_def split: vmrights.splits)
lemma cpspace_pde_relation_unique:
assumes "cpspace_pde_relation ah ch" "cpspace_pde_relation ah' ch"
shows "map_to_pdes ah' = map_to_pdes ah"
apply (rule cmap_relation_unique[OF inj_Ptr _ assms])
by (simp add: cpde_relation_def s_from_cacheable_def Let_def split: pde.splits bool.splits)
lemma cpspace_pte_relation_unique:
assumes "cpspace_pte_relation ah ch" "cpspace_pte_relation ah' ch"
shows "map_to_ptes ah' = map_to_ptes ah"
apply (rule cmap_relation_unique[OF inj_Ptr _ assms])
by (simp add: cpte_relation_def s_from_cacheable_def Let_def split: pte.splits bool.splits)
(* FIXME: move *)
lemma Collect_mono2: "Collect P \<subseteq> Collect Q \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q x)" by auto
(* FIXME: move to Wellformed, turn valid_asid_pool' into an abbreviation >>>*)
primrec
wf_asid_pool' :: "asidpool \<Rightarrow> bool"
where
"wf_asid_pool' (ASIDPool pool) =
(dom pool \<subseteq> {0 .. 2^asid_low_bits - 1} \<and>
0 \<notin> ran pool \<and> (\<forall>x \<in> ran pool. is_aligned x pdBits))"
lemma valid_eq_wf_asid_pool'[simp]:
"valid_asid_pool' pool = (\<lambda>s. wf_asid_pool' pool)"
by (case_tac pool) simp
declare valid_asid_pool'.simps[simp del]
(*<<<*)
lemma cpspace_asidpool_relation_unique:
assumes invs: "\<forall>x\<in>ran (map_to_asidpools ah). wf_asid_pool' x"
"\<forall>x\<in>ran (map_to_asidpools ah'). wf_asid_pool' x"
assumes rels: "cpspace_asidpool_relation ah ch"
"cpspace_asidpool_relation ah' ch"
shows "map_to_asidpools ah' = map_to_asidpools ah"
(* FIXME: Should we generalize cmap_relation_unique, instead? *)
using rels
apply (clarsimp simp add: cmap_relation_def)
apply (drule inj_image_inv[OF inj_Ptr])+
apply simp
apply (rule ext)
apply (case_tac "x:dom (map_to_asidpools ah)")
apply (drule bspec, assumption)+
apply (simp add: dom_def Collect_eq, drule_tac x=x in spec)
using invs
apply (clarsimp simp: casid_pool_relation_def Let_def
split: asidpool.splits asid_pool_C.splits)
apply (drule bspec, fastforce)+
apply (drule array_relation_to_map)+
apply (rule ext, rename_tac y)
apply (drule_tac x=y in spec)+
apply clarsimp
apply (case_tac "y\<le>2^asid_low_bits - 1", simp)
apply (drule_tac s="option_to_ptr (fun y)" in sym)
apply (simp add: option_to_ptr_def option_to_0_def ran_def
split: option.splits)
apply (simp add: atLeastAtMost_def atLeast_def atMost_def dom_def
Collect_mono2)
apply (drule_tac x=y in spec)+
apply auto
done
lemma valid_objs'_imp_wf_asid_pool':
"valid_objs' s \<Longrightarrow> \<forall>x\<in>ran (map_to_asidpools (ksPSpace s)). wf_asid_pool' x"
apply (clarsimp simp: valid_objs'_def ran_def)
apply (case_tac "ksPSpace s a", simp+)
apply (rename_tac y, drule_tac x=y in spec)
apply (case_tac y, simp_all add: projectKO_opt_asidpool)
apply (clarsimp simp: valid_obj'_def
split: arch_kernel_object.splits)
done
lemma cpspace_user_data_relation_unique:
"\<lbrakk>cmap_relation (heap_to_page_data ah bh) (clift ch) Ptr cuser_data_relation;
cmap_relation(heap_to_page_data ah' bh')(clift ch) Ptr cuser_data_relation\<rbrakk>
\<Longrightarrow> map_to_user_data ah' = map_to_user_data ah"
apply (clarsimp simp add: cmap_relation_def)
apply (drule inj_image_inv[OF inj_Ptr])+
apply simp
apply (rule ext)
apply (case_tac "x:dom (heap_to_page_data ah bh)")
apply (drule bspec, assumption)+
apply (simp add: dom_def Collect_eq, drule_tac x=x in spec)
apply (clarsimp simp add: cuser_data_relation_def heap_to_page_data_def)
apply (rule ccontr)
apply (case_tac z, case_tac za)
apply simp