-
Notifications
You must be signed in to change notification settings - Fork 0
/
Retype_C.thy
7251 lines (6736 loc) · 320 KB
/
Retype_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 Retype_C
imports
Detype_C
CSpace_All
StoreWord_C
begin
declare word_neq_0_conv [simp del]
lemma sint_eq_uintI:
"uint (a::word32) < 2^ (word_bits - 1) \<Longrightarrow> sint a = uint a"
apply (rule word_sint.Abs_inverse')
apply (subst word_bits_def[symmetric])
apply (simp add:sints_def)
apply (simp add:range_sbintrunc)
apply (simp add:word_bits_def)
apply (rule order_trans[where y =0])
apply simp
apply simp
apply simp
done
lemma sint_eq_uint:
"unat (a::word32) < 2^ 31 \<Longrightarrow> sint a = uint a"
apply (rule sint_eq_uintI)
apply (clarsimp simp:uint_nat word_bits_def
zless_nat_eq_int_zless[symmetric])
done
lemma sle_positive: "\<lbrakk> b < 0x80000000; (a :: word32) \<le> b \<rbrakk> \<Longrightarrow> a <=s b"
apply (simp add:word_sle_def)
apply (subst sint_eq_uint)
apply (rule unat_less_helper)
apply simp
apply (subst sint_eq_uint)
apply (rule unat_less_helper)
apply simp
apply (clarsimp simp:word_le_def)
done
lemma sless_positive: "\<lbrakk> b < 0x80000000; (a :: word32) < b \<rbrakk> \<Longrightarrow> a <s b"
apply (clarsimp simp: word_sless_def)
apply (rule conjI)
apply (erule sle_positive)
apply simp
apply simp
done
lemma zero_le_sint: "\<lbrakk> 0 \<le> (a :: word32); a < 0x80000000 \<rbrakk> \<Longrightarrow> 0 \<le> sint a"
apply (subst sint_eq_uint)
apply (simp add:unat_less_helper)
apply simp
done
context kernel_m
begin
(* Ensure that the given region of memory does not contain any typed memory. *)
definition
region_is_typeless :: "word32 \<Rightarrow> nat \<Rightarrow> ('a globals_scheme, 'b) StateSpace.state_scheme \<Rightarrow> bool"
where
"region_is_typeless ptr sz s \<equiv>
\<forall>z\<in>{ptr ..+ sz}. snd (snd (t_hrs_' (globals s)) z) = empty"
lemma c_guard_word8:
"c_guard (p :: word8 ptr) = (ptr_val p \<noteq> 0)"
unfolding c_guard_def ptr_aligned_def c_null_guard_def
apply simp
apply (rule iffI)
apply (drule intvlD)
apply clarsimp
apply simp
apply (rule intvl_self)
apply simp
done
lemma
"(x \<in> {x ..+ n}) = (n \<noteq> 0)"
apply (rule iffI)
apply (drule intvlD)
apply clarsimp
apply (rule intvl_self)
apply simp
done
lemma aligned_add_aligned_simple:
"\<lbrakk> is_aligned a n; is_aligned b n; n < word_bits \<rbrakk> \<Longrightarrow> is_aligned (a + b) n"
apply (rule aligned_add_aligned [where n=n], auto)
done
lemma aligned_sub_aligned_simple:
"\<lbrakk> is_aligned a n; is_aligned b n; n < word_bits \<rbrakk> \<Longrightarrow> is_aligned (a - b) n"
apply (rule aligned_sub_aligned [where n=n], auto)
done
lemma heap_update_list_append3:
"\<lbrakk> s' = s + of_nat (length xs) \<rbrakk> \<Longrightarrow> heap_update_list s (xs @ ys) H = heap_update_list s' ys (heap_update_list s xs H)"
apply simp
apply (subst heap_update_list_append [symmetric])
apply clarsimp
done
lemma ptr_aligned_word32:
"\<lbrakk> is_aligned p 2 \<rbrakk> \<Longrightarrow> ptr_aligned ((Ptr p) :: word32 ptr)"
apply (clarsimp simp: is_aligned_def ptr_aligned_def)
done
lemma c_guard_word32:
"\<lbrakk> is_aligned (ptr_val p) 2; p \<noteq> NULL \<rbrakk> \<Longrightarrow> c_guard (p :: (word32 ptr))"
apply (clarsimp simp: c_guard_def)
apply (rule conjI)
apply (case_tac p, clarsimp simp: ptr_aligned_word32)
apply (case_tac p, simp add: c_null_guard_def)
apply (subst intvl_aligned_bottom_eq [where n=2 and bits=2], auto simp: word_bits_def)
done
lemma is_aligned_and_not_zero: "\<lbrakk> is_aligned n k; n \<noteq> 0 \<rbrakk> \<Longrightarrow> 2^k \<le> n"
apply (metis aligned_small_is_0 word_not_le)
done
lemma replicate_append [rule_format]: "\<forall>xs. replicate n x @ (x # xs) = replicate (n + 1) x @ xs"
apply (induct n)
apply clarsimp
apply clarsimp
done
lemmas unat_add_simple =
iffD1 [OF unat_add_lem [where 'a = 32, folded word_bits_def]]
lemma replicate_append_list [rule_format]:
"\<forall>n. set L \<subseteq> {0::word8} \<longrightarrow> (replicate n 0 @ L = replicate (n + length L) 0)"
apply (rule rev_induct)
apply clarsimp
apply (rule allI)
apply (erule_tac x="n+1" in allE)
apply clarsimp
apply (subst append_assoc[symmetric])
apply clarsimp
apply (subgoal_tac "\<And>n. (replicate n 0 @ [0]) = (0 # replicate n (0 :: word8))")
apply clarsimp
apply (induct_tac na)
apply clarsimp
apply clarsimp
done
lemma heap_update_list_replicate:
"\<lbrakk> set L = {0}; n' = n + length L \<rbrakk> \<Longrightarrow> heap_update_list s ((replicate n 0) @ L) H = heap_update_list s (replicate n' 0) H"
apply (subst replicate_append_list)
apply clarsimp
apply clarsimp
done
lemma heap_update_word32_is_heap_update_list:
"heap_update p (x :: word32) = heap_update_list (ptr_val p) (to_bytes x a)"
apply (rule ext)+
apply (clarsimp simp: heap_update_def)
apply (clarsimp simp: to_bytes_def typ_info_word)
done
lemma to_bytes_word32_0:
"to_bytes (0 :: word32) xs = [0, 0, 0, 0 :: word8]"
apply (simp add: to_bytes_def typ_info_word word_rsplit_same word_rsplit_0)
done
lemma const_less_word: "\<lbrakk> (a :: word32) - 1 < b; a \<noteq> b \<rbrakk> \<Longrightarrow> a < b"
apply (metis less_1_simp word_le_less_eq)
done
lemma const_le_unat_word: "\<lbrakk> b < 2 ^ word_bits; of_nat b \<le> a \<rbrakk> \<Longrightarrow> b \<le> unat (a :: word32)"
apply (clarsimp simp: word_le_def uint_nat)
apply (subst (asm) unat_of_nat32)
apply (clarsimp simp: word_bits_def size)
apply clarsimp
done
lemma globals_list_distinct_subset:
"\<lbrakk> globals_list_distinct D symtab xs; D' \<subseteq> D \<rbrakk>
\<Longrightarrow> globals_list_distinct D' symtab xs"
by (simp add: globals_list_distinct_def disjoint_subset)
lemma fst_s_footprint:
"(fst ` s_footprint p) = {ptr_val (p :: 'a ptr)
..+ size_of TYPE('a :: c_type)}"
apply (simp add: s_footprint_def s_footprint_untyped_def)
apply (auto simp: intvl_def size_of_def image_def)
done
lemma memzero_spec:
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. ptr_val \<acute>s \<noteq> 0 \<and> ptr_val \<acute>s \<le> ptr_val \<acute>s + (\<acute>n - 1)
\<and> (is_aligned (ptr_val \<acute>s) 2) \<and> (is_aligned (\<acute>n) 2)
\<and> {ptr_val \<acute>s ..+ unat \<acute>n} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd \<acute>t_hrs)\<rbrace>
Call memzero_'proc {t.
t_hrs_' (globals t) = hrs_mem_update (heap_update_list (ptr_val (s_' s))
(replicate (unat (n_' s)) (ucast (0)))) (t_hrs_' (globals s))}"
apply (hoare_rule HoarePartial.ProcNoRec1)
apply (clarsimp simp: whileAnno_def)
apply (rule_tac I1="{t. (ptr_val (s_' s) \<le> ptr_val (s_' s) + ((n_' s) - 1) \<and> ptr_val (s_' s) \<noteq> 0) \<and>
ptr_val (s_' s) + (n_' s - n_' t) = ptr_val (p___ptr_to_unsigned_char_' t) \<and>
n_' t \<le> n_' s \<and>
(is_aligned (n_' t) 2) \<and>
(is_aligned (n_' s) 2) \<and>
(is_aligned (ptr_val (s_' t)) 2) \<and>
(is_aligned (ptr_val (s_' s)) 2) \<and>
(is_aligned (ptr_val (p___ptr_to_unsigned_char_' t)) 2) \<and>
{ptr_val (p___ptr_to_unsigned_char_' t) ..+ unat (n_' t)} \<times> {SIndexVal, SIndexTyp 0}
\<subseteq> dom_s (hrs_htd (t_hrs_' (globals t))) \<and>
globals t = (globals s)\<lparr> t_hrs_' :=
hrs_mem_update (heap_update_list (ptr_val (s_' s))
(replicate (unat (n_' s - n_' t)) 0))
(t_hrs_' (globals s))\<rparr> }"
and V1=undefined in subst [OF whileAnno_def])
apply vcg
apply (clarsimp simp add: hrs_mem_update_def)
apply clarsimp
apply (case_tac s, case_tac p___ptr_to_unsigned_char)
apply (subgoal_tac "4 \<le> unat na")
apply (intro conjI)
apply (simp add: ptr_safe_def s_footprint_def s_footprint_untyped_def
typ_uinfo_t_def typ_info_word)
apply (erule order_trans[rotated])
apply (auto intro!: intvlI)[1]
apply (subst c_guard_word32, simp_all)[1]
apply (clarsimp simp: field_simps)
apply (metis le_minus' minus_one_helper5 olen_add_eqv diff_self word_le_0_iff word_le_less_eq)
apply (clarsimp simp: field_simps)
apply (frule is_aligned_and_not_zero)
apply clarsimp
apply (rule word_le_imp_diff_le, auto)[1]
apply clarsimp
apply (rule aligned_sub_aligned [where n=2], simp_all add: is_aligned_def word_bits_def)[1]
apply clarsimp
apply (rule aligned_add_aligned_simple, simp_all add: is_aligned_def word_bits_def)[1]
apply (erule order_trans[rotated])
apply (clarsimp simp: subset_iff)
apply (erule subsetD[OF intvl_sub_offset, rotated])
apply (simp add: unat_sub word_le_nat_alt)
apply (clarsimp simp: word_bits_def hrs_mem_update_def)
apply (subst heap_update_word32_is_heap_update_list [where a="[]"])
apply (subst heap_update_list_append3[symmetric])
apply clarsimp
apply (subst to_bytes_word32_0)
apply (rule heap_update_list_replicate)
apply clarsimp
apply (rule_tac s="unat ((n - na) + 4)" in trans)
apply (simp add: field_simps)
apply (subst Word.unat_plus_simple[THEN iffD1])
apply (rule is_aligned_no_overflow''[where n=2, simplified])
apply (erule(1) aligned_sub_aligned, simp)
apply (clarsimp simp: field_simps)
apply (frule_tac x=n in is_aligned_no_overflow'', simp)
apply simp
apply simp
apply (rule dvd_imp_le)
apply (simp add: is_aligned_def)
apply (simp add: unat_eq_0[symmetric])
apply clarsimp
done
lemma is_aligned_and_2_to_k:
assumes mask_2_k: "(n && 2 ^ k - 1) = 0"
shows "is_aligned (n :: word32) k"
proof (subst is_aligned_mask)
have "mask k = (2 :: word32) ^ k - 1"
by (clarsimp simp: mask_def)
thus "n && mask k = 0" using mask_2_k
by simp
qed
lemma memset_spec:
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. ptr_val \<acute>s \<noteq> 0 \<and> ptr_val \<acute>s \<le> ptr_val \<acute>s + (\<acute>n - 1)
\<and> {ptr_val \<acute>s ..+ unat \<acute>n} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd \<acute>t_hrs)\<rbrace>
Call memset_'proc
{t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list (ptr_val (s_' s))
(replicate (unat (n_' s)) (ucast (c_' s)))) (t_hrs_' (globals s))}"
apply (hoare_rule HoarePartial.ProcNoRec1)
apply (clarsimp simp: whileAnno_def)
apply (rule_tac I1="{t. (ptr_val (s_' s) \<le> ptr_val (s_' s) + ((n_' s) - 1) \<and> ptr_val (s_' s) \<noteq> 0) \<and>
c_' t = c_' s \<and>
ptr_val (s_' s) + (n_' s - n_' t) = ptr_val (p___ptr_to_unsigned_char_' t) \<and>
n_' t \<le> n_' s \<and>
{ptr_val (p___ptr_to_unsigned_char_' t) ..+ unat (n_' t)} \<times> {SIndexVal, SIndexTyp 0}
\<subseteq> dom_s (hrs_htd (t_hrs_' (globals t))) \<and>
globals t = (globals s)\<lparr> t_hrs_' :=
hrs_mem_update (heap_update_list (ptr_val (s_' s))
(replicate (unat (n_' s - n_' t)) (ucast (c_' t))))
(t_hrs_' (globals s))\<rparr>}"
and V1=undefined in subst [OF whileAnno_def])
apply vcg
apply (clarsimp simp add: hrs_mem_update_def split: split_if_asm)
apply (subst (asm) word_mod_2p_is_mask [where n=2, simplified], simp)
apply (subst (asm) word_mod_2p_is_mask [where n=2, simplified], simp)
apply (rule conjI)
apply (rule is_aligned_and_2_to_k, clarsimp simp: mask_def)
apply (rule is_aligned_and_2_to_k, clarsimp simp: mask_def)
apply clarsimp
apply (intro conjI)
apply (simp add: ptr_safe_def s_footprint_def s_footprint_untyped_def
typ_uinfo_t_def typ_info_word)
apply (erule order_trans[rotated])
apply (auto simp: intvl_self unat_gt_0 intro!: intvlI)[1]
apply (simp add: c_guard_word8)
apply (erule subst)
apply (subst lt1_neq0 [symmetric])
apply (rule order_trans)
apply (subst lt1_neq0, assumption)
apply (erule word_random)
apply (rule word_le_minus_mono_right)
apply (simp add: lt1_neq0)
apply assumption
apply (erule order_trans [rotated])
apply (simp add: lt1_neq0)
apply (case_tac p___ptr_to_unsigned_char, simp add: CTypesDefs.ptr_add_def unat_minus_one field_simps)
apply (metis word_must_wrap word_not_simps(1) linear)
apply (erule order_trans[rotated])
apply (clarsimp simp: ptr_val_case split: ptr.splits)
apply (erule subsetD[OF intvl_sub_offset, rotated])
apply (simp add: unat_sub word_le_nat_alt word_less_nat_alt)
apply (clarsimp simp: ptr_val_case unat_minus_one hrs_mem_update_def split: ptr.splits)
apply (subgoal_tac "unat (n - (na - 1)) = Suc (unat (n - na))")
apply (erule ssubst, subst replicate_Suc_append)
apply (subst heap_update_list_append)
apply (simp add: heap_update_word8)
apply (subst unatSuc [symmetric])
apply (subst add.commute)
apply (metis word_neq_0_conv word_sub_plus_one_nonzero)
apply (simp add: field_simps)
apply (clarsimp)
apply (metis diff_0_right word_gt_0)
done
lemma is_aligned_power2: "b \<le> a \<Longrightarrow> is_aligned (2 ^ a) b"
apply (metis WordLemmaBucket.is_aligned_0' is_aligned_triv
is_aligned_weaken le_def power_overflow)
done
declare snd_get[simp]
declare snd_gets[simp]
lemma snd_when_aligneError[simp]:
shows "(snd ((when P (alignError sz)) s)) = P"
by (simp add: when_def alignError_def fail_def split: split_if)
lemma snd_unless_aligneError[simp]:
shows "(snd ((unless P (alignError sz)) s)) = (\<not> P)"
by (simp add: unless_def)
lemma lift_t_retyp_heap_same:
fixes p :: "'a :: mem_type ptr"
assumes gp: "g p"
shows "lift_t g (hp, ptr_retyp p td) p = Some (from_bytes (heap_list hp (size_of TYPE('a)) (ptr_val p)))"
apply (simp add: lift_t_def lift_typ_heap_if s_valid_def hrs_htd_def)
apply (subst ptr_retyp_h_t_valid)
apply (rule gp)
apply simp
apply (subst heap_list_s_heap_list_dom)
apply (clarsimp simp: s_footprint_intvl)
apply simp
done
lemma lift_t_retyp_heap_same_rep0:
fixes p :: "'a :: mem_type ptr"
assumes gp: "g p"
shows "lift_t g (heap_update_list (ptr_val p) (replicate (size_of TYPE('a)) 0) hp, ptr_retyp p td) p =
Some (from_bytes (replicate (size_of TYPE('a)) 0))"
apply (subst lift_t_retyp_heap_same)
apply (rule gp)
apply (subst heap_list_update [where v = "replicate (size_of TYPE('a)) 0", simplified])
apply (rule order_less_imp_le)
apply simp
apply simp
done
lemma ptr_retyp_valid_footprint_disjoint2:
"\<lbrakk>valid_footprint (ptr_retyp (q::'b::mem_type ptr) d) p s; {p..+size_td s} \<inter> {ptr_val q..+size_of TYPE('b)} = {} \<rbrakk>
\<Longrightarrow> valid_footprint d p s"
apply(clarsimp simp: valid_footprint_def Let_def)
apply (drule spec, drule (1) mp)
apply(subgoal_tac "p + of_nat y \<in> {p..+size_td s}")
apply (subst (asm) ptr_retyp_d)
apply clarsimp
apply fast
apply (clarsimp simp add: ptr_retyp_d_eq_fst split: split_if_asm)
apply fast
apply (erule intvlI)
done
lemma ptr_retyp_disjoint2:
"\<lbrakk>ptr_retyp (p::'a::mem_type ptr) d,g \<Turnstile>\<^sub>t q;
{ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val q..+size_of TYPE('b)} = {} \<rbrakk>
\<Longrightarrow> d,g \<Turnstile>\<^sub>t (q::'b::mem_type ptr)"
apply(clarsimp simp: h_t_valid_def)
apply(erule ptr_retyp_valid_footprint_disjoint2)
apply(simp add: size_of_def)
apply fast
done
lemma ptr_retyp_disjoint_iff:
"{ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val q..+size_of TYPE('b)} = {}
\<Longrightarrow> ptr_retyp (p::'a::mem_type ptr) d,g \<Turnstile>\<^sub>t q = d,g \<Turnstile>\<^sub>t (q::'b::mem_type ptr)"
apply rule
apply (erule (1) ptr_retyp_disjoint2)
apply (erule (1) ptr_retyp_disjoint)
done
lemma lift_t_retyp_heap_other2:
fixes p :: "'a :: mem_type ptr" and p' :: "'b :: mem_type ptr"
assumes orth: "{ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val p'..+size_of TYPE('b)} = {}"
shows "lift_t g (hp, ptr_retyp p td) p' = lift_t g (hp, td) p'"
apply (simp add: lift_t_def lift_typ_heap_if s_valid_def hrs_htd_def ptr_retyp_disjoint_iff [OF orth])
apply (cases "td, g \<Turnstile>\<^sub>t p'")
apply simp
apply (simp add: h_t_valid_taut heap_list_s_heap_list heap_list_update_disjoint_same
ptr_retyp_disjoint_iff orth)
apply (simp add: h_t_valid_taut heap_list_s_heap_list heap_list_update_disjoint_same
ptr_retyp_disjoint_iff orth)
done
lemma dom_s_SindexValD:
"(x, SIndexVal) \<in> dom_s td \<Longrightarrow> fst (td x)"
unfolding dom_s_def by clarsimp
lemma typ_slice_t_self_nth:
"\<exists>n < length (typ_slice_t td m). \<exists>b. typ_slice_t td m ! n = (td, b)"
using typ_slice_t_self [where td = td and m = m]
by (fastforce simp add: in_set_conv_nth)
lemma ptr_retyp_other_cleared_region:
fixes p :: "'a :: mem_type ptr" and p' :: "'b :: mem_type ptr"
assumes ht: "ptr_retyp p td, g \<Turnstile>\<^sub>t p'"
and tdisj: "typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b :: mem_type)"
and clear: "\<forall>x \<in> {ptr_val p ..+ size_of TYPE('a)}. \<forall>n b. snd (td x) n \<noteq> Some (typ_uinfo_t TYPE('b), b)"
shows "{ptr_val p'..+ size_of TYPE('b)} \<inter> {ptr_val p ..+ size_of TYPE('a)} = {}"
proof (rule classical)
assume asm: "{ptr_val p'..+ size_of TYPE('b)} \<inter> {ptr_val p ..+ size_of TYPE('a)} \<noteq> {}"
then obtain mv where mvp: "mv \<in> {ptr_val p..+size_of TYPE('a)}"
and mvp': "mv \<in> {ptr_val p'..+size_of TYPE('b)}"
by blast
then obtain k' where mv: "mv = ptr_val p' + of_nat k'" and klt: "k' < size_td (typ_info_t TYPE('b))"
by (clarsimp dest!: intvlD simp: size_of_def typ_uinfo_size)
let ?mv = "ptr_val p' + of_nat k'"
obtain n b where nl: "n < length (typ_slice_t (typ_uinfo_t TYPE('b)) k')"
and tseq: "typ_slice_t (typ_uinfo_t TYPE('b)) k' ! n = (typ_uinfo_t TYPE('b), b)"
using typ_slice_t_self_nth [where td = "typ_uinfo_t TYPE('b)" and m = k']
by clarsimp
with ht have "snd (ptr_retyp p td ?mv) n = Some (typ_uinfo_t TYPE('b), b)"
unfolding h_t_valid_def
apply -
apply (clarsimp simp: valid_footprint_def Let_def)
apply (drule spec, drule mp [OF _ klt])
apply (clarsimp simp: map_le_def)
apply (drule bspec)
apply simp
apply simp
done
moreover {
assume "snd (ptr_retyp p empty_htd ?mv) n = Some (typ_uinfo_t TYPE('b), b)"
hence "(typ_uinfo_t TYPE('b)) \<in> fst ` set (typ_slice_t (typ_uinfo_t TYPE('a))
(unat (ptr_val p' + of_nat k' - ptr_val p)))"
using asm mv mvp
apply -
apply (rule_tac x = "(typ_uinfo_t TYPE('b), b)" in image_eqI)
apply simp
apply (fastforce simp add: ptr_retyp_footprint list_map_eq in_set_conv_nth split: split_if_asm)
done
with typ_slice_set have "(typ_uinfo_t TYPE('b)) \<in> fst ` td_set (typ_uinfo_t TYPE('a)) 0"
by (rule subsetD)
hence False using tdisj by (clarsimp simp: tag_disj_def typ_tag_le_def)
} ultimately show ?thesis using mvp mvp' mv unfolding h_t_valid_def valid_footprint_def
apply -
apply (subst (asm) ptr_retyp_d_eq_snd)
apply (auto simp add: map_add_Some_iff clear)
done
qed
lemma h_t_valid_not_empty:
fixes p :: "'a :: c_type ptr"
shows "\<lbrakk> d,g \<Turnstile>\<^sub>t p; x \<in> {ptr_val p..+size_of TYPE('a)} \<rbrakk> \<Longrightarrow> snd (d x) \<noteq> empty"
apply (drule intvlD)
apply (clarsimp simp: h_t_valid_def size_of_def)
apply (drule valid_footprintD)
apply (simp add: typ_uinfo_size)
apply clarsimp
done
lemma ptr_retyps_out:
fixes p :: "'a :: mem_type ptr"
shows "x \<notin> {ptr_val p..+n * size_of TYPE('a)} \<Longrightarrow> ptr_retyps n p td x = td x"
proof (induct n arbitrary: p)
case 0 thus ?case by simp
next
case (Suc m)
have ih: "ptr_retyps m (CTypesDefs.ptr_add p 1) td x = td x"
proof (rule Suc.hyps)
from Suc.prems show "x \<notin> {ptr_val (CTypesDefs.ptr_add p 1)..+m * size_of TYPE('a)}"
apply (rule contrapos_nn)
apply (erule subsetD [rotated])
apply (simp add: CTypesDefs.ptr_add_def)
apply (rule intvl_sub_offset)
apply (simp add: unat_of_nat)
done
qed
from Suc.prems have "x \<notin> {ptr_val p..+size_of TYPE('a)}"
apply (rule contrapos_nn)
apply (erule subsetD [rotated])
apply (rule intvl_start_le)
apply simp
done
thus ?case
by (simp add: ptr_retyp_d ih)
qed
lemma lift_t_retyp_heap_other_orth:
fixes p :: "'a :: mem_type ptr" and p' :: "'b :: mem_type ptr"
assumes orth: "{ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val p'..+size_of TYPE('b)} = {}"
and lbs: "length bs = size_of TYPE('a)"
shows "lift_t g (heap_update_list (ptr_val p) bs hp, ptr_retyp p td) p' = lift_t g (hp, td) p'"
using lbs
apply (simp add: lift_t_def lift_typ_heap_if s_valid_def hrs_htd_def ptr_retyp_disjoint_iff [OF orth])
apply (cases "td, g \<Turnstile>\<^sub>t p'")
apply (simp add: h_t_valid_taut heap_list_s_heap_list heap_update_def heap_list_update_disjoint_same
ptr_retyp_disjoint_iff orth typ_heap_simps)
apply (simp add: h_t_valid_taut heap_list_s_heap_list heap_list_update_disjoint_same
ptr_retyp_disjoint_iff orth)
done
lemma lift_t_retyp_heap_other_rep0:
fixes p :: "'a :: mem_type ptr" and p' :: "'b :: mem_type ptr"
assumes orth: "{ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val p'..+size_of TYPE('b)} = {}"
shows "lift_t g (heap_update_list (ptr_val p) (replicate (size_of TYPE('a)) 0) hp, ptr_retyp p td) p' = lift_t g (hp, td) p'"
apply (simp add: lift_t_def lift_typ_heap_if s_valid_def hrs_htd_def ptr_retyp_disjoint_iff [OF orth])
apply (cases "td, g \<Turnstile>\<^sub>t p'")
apply simp
apply (simp add: h_t_valid_taut heap_list_s_heap_list heap_list_update_disjoint_same
ptr_retyp_disjoint_iff orth)
apply (simp add: h_t_valid_taut heap_list_s_heap_list heap_list_update_disjoint_same
ptr_retyp_disjoint_iff orth)
done
lemma map_leD:
"\<lbrakk> map_le m m'; m x = Some y \<rbrakk> \<Longrightarrow> m' x = Some y"
by (simp add: map_le_def dom_def)
lemma h_t_valid_intvl_htd_contains_uinfo_t:
"h_t_valid d g (p :: ('a :: c_type) ptr) \<Longrightarrow> x \<in> {ptr_val p ..+ size_of TYPE('a)} \<Longrightarrow>
(\<exists>n. snd (d x) n \<noteq> None \<and> fst (the (snd (d x) n)) = typ_uinfo_t TYPE ('a))"
apply (clarsimp simp: h_t_valid_def valid_footprint_def Let_def intvl_def size_of_def)
apply (drule spec, drule(1) mp)
apply (cut_tac m=k in typ_slice_t_self[where td="typ_uinfo_t TYPE ('a)"])
apply (clarsimp simp: in_set_conv_nth)
apply (drule_tac x=i in map_leD)
apply simp
apply fastforce
done
lemma lift_t_retyp_heap_other0:
fixes p :: "'a :: mem_type ptr" and p' :: "'b :: mem_type ptr"
assumes clear: "\<forall>x \<in> {ptr_val p ..+ size_of TYPE('a)}. \<forall>n b. snd (td x) n \<noteq> Some (typ_uinfo_t TYPE('b), b)"
and lbs: "length bs = size_of TYPE('a)"
and tdisj: "typ_uinfo_t TYPE('a :: mem_type) \<bottom>\<^sub>t typ_uinfo_t TYPE('b :: mem_type)"
shows "lift_t g (heap_update_list (ptr_val p) bs hp, ptr_retyp p td) p' = lift_t g (hp, td) p'"
proof (cases "{ptr_val p ..+ size_of TYPE('a)} \<inter> {ptr_val p' ..+ size_of TYPE('b)} = {}")
case True
thus ?thesis using lbs
by (rule lift_t_retyp_heap_other_orth)
next
case False
then obtain mv where mvp: "mv \<in> {ptr_val p..+size_of TYPE('a)}"
and mvp': "mv \<in> {ptr_val p'..+size_of TYPE('b)}" by blast
have "\<not> td, g \<Turnstile>\<^sub>t p'" using mvp mvp'
apply clarsimp
apply (drule(1) h_t_valid_intvl_htd_contains_uinfo_t)
apply (clarsimp simp: clear)
done
thus ?thesis
using False
apply (simp add: liftt_if split: split_if_asm split_if)
apply (rule notI)
apply (drule ptr_retyp_other_cleared_region [OF _ tdisj clear])
apply (simp add: Int_ac)
done
qed
lemma lift_t_retyp_no_heap_other0:
fixes p :: "'a :: mem_type ptr" and p' :: "'b :: mem_type ptr"
assumes clear: "\<forall>x \<in> {ptr_val p ..+ size_of TYPE('a)}. \<forall>n b. snd (td x) n \<noteq> Some (typ_uinfo_t TYPE('b), b)"
and tdisj: "typ_uinfo_t TYPE('a :: mem_type) \<bottom>\<^sub>t typ_uinfo_t TYPE('b :: mem_type)"
shows "lift_t g (hp, ptr_retyp p td) p' = lift_t g (hp, td) p'"
proof (cases "{ptr_val p ..+ size_of TYPE('a)} \<inter> {ptr_val p' ..+ size_of TYPE('b)} = {}")
case True
thus ?thesis
by (rule lift_t_retyp_heap_other2)
next
case False
then obtain mv where mvp: "mv \<in> {ptr_val p..+size_of TYPE('a)}"
and mvp': "mv \<in> {ptr_val p'..+size_of TYPE('b)}" by blast
hence "\<not> td, g \<Turnstile>\<^sub>t p'" using mvp'
apply clarsimp
apply (drule(1) h_t_valid_intvl_htd_contains_uinfo_t)
apply (clarsimp simp: clear)
done
thus ?thesis
using False
apply (simp add: liftt_if split: split_if_asm split_if)
apply (rule notI)
apply (drule ptr_retyp_other_cleared_region [OF _ tdisj clear])
apply (simp add: Int_ac)
done
qed
lemma lift_t_retyp_heap_other:
fixes p :: "'a :: mem_type ptr"
assumes clear: "\<forall>x \<in> {ptr_val p ..+ size_of TYPE('a)}. \<forall>n b. snd (td x) n \<noteq> Some (typ_uinfo_t TYPE('b), b)"
and lbs: "length bs = size_of TYPE('a)"
and tdisj: "typ_uinfo_t TYPE('a :: mem_type) \<bottom>\<^sub>t typ_uinfo_t TYPE('b :: mem_type)"
shows "lift_t g (heap_update_list (ptr_val p) bs hp, ptr_retyp p td) = (lift_t g (hp, td) :: 'b :: mem_type typ_heap)"
by (rule ext, rule lift_t_retyp_heap_other0 [OF clear lbs tdisj])
lemma lift_t_retyp_no_heap_other:
fixes p :: "'a :: mem_type ptr"
assumes clear: "\<forall>x \<in> {ptr_val p ..+ size_of TYPE('a)}. \<forall>n b. snd (td x) n \<noteq> Some (typ_uinfo_t TYPE('b), b)"
and tdisj: "typ_uinfo_t TYPE('a :: mem_type) \<bottom>\<^sub>t typ_uinfo_t TYPE('b :: mem_type)"
shows "lift_t g (hp, ptr_retyp p td) = (lift_t g (hp, td) :: 'b :: mem_type typ_heap)"
by (rule ext, rule lift_t_retyp_no_heap_other0 [OF clear tdisj])
lemma cslift_ptr_retyps_memset_other:
fixes p :: "'a :: mem_type ptr"
assumes clear: "\<forall>z \<in> {ptr_val p ..+ nptrs * size_of TYPE('a)}.
\<forall>n b. snd ((hrs_htd (t_hrs_' (globals x))) z) n \<noteq> Some (typ_uinfo_t TYPE('b), b)"
and tdisj: "typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b :: mem_type)"
and sz: "nptrs * size_of TYPE('a) < 2 ^ word_bits"
shows "(clift (hrs_htd_update (ptr_retyps nptrs p)
(hrs_mem_update (heap_update_list (ptr_val p) (replicate (nptrs * size_of TYPE('a)) 0))
(t_hrs_' (globals x)))) :: 'b :: mem_type typ_heap)
= cslift x" (is "?LHS nptrs p = ?RHS nptrs p" )
using clear sz
proof (induct nptrs arbitrary: p)
case 0
show ?case by (simp add: hrs_mem_update_def hrs_htd_update_def)
next
case (Suc n)
have pa:
"(ptr_val p + of_nat (size_of TYPE('a))) = ptr_val (CTypesDefs.ptr_add p 1)"
by (simp add: CTypesDefs.ptr_add_def)
let ?td = "snd (t_hrs_' (globals x))"
have rl: "\<And>x. x \<in> {ptr_val p..+ size_of TYPE('a)} \<Longrightarrow> x \<in> {ptr_val p..+Suc n * size_of TYPE('a)}"
apply (erule subsetD [rotated])
apply (rule intvl_start_le)
apply simp
done
have ih': "?LHS n (CTypesDefs.ptr_add p 1) = ?RHS n (CTypesDefs.ptr_add p 1)"
using Suc.prems
apply -
apply (rule Suc.hyps[rotated])
apply simp
apply clarsimp
apply (subgoal_tac "z \<in> {ptr_val p..+Suc n * size_of TYPE('a)}")
prefer 2
apply (rule subsetD [rotated])
apply (simp add: CTypesDefs.ptr_add_def)
apply (rule intvl_sub_offset)
apply (simp add: unat_of_nat)
apply simp
done
show ?case
proof (rule ext)
fix p' :: "'b ptr"
have "size_of TYPE('a) + n * size_of TYPE('a) < 2 ^ word_bits" using Suc.prems by simp
thus "?LHS (Suc n) p p' = ?RHS (Suc n) p p'"
apply (simp add: replicate_add)
apply (simp add: heap_update_list_append2 hrs_mem_update_def hrs_htd_update_def split_beta)
apply (subst lift_t_retyp_heap_other0)
apply (clarsimp simp: CTypesDefs.ptr_add_def)
apply (subst(asm) ptr_retyps_out)
apply clarsimp
apply (drule orthD2 [rotated])
apply (rule init_intvl_disj [where z = "n * size_of TYPE('a)"])
apply (simp add: word_bits_conv addr_card)
apply simp
apply (simp add: Suc.prems(1)[rule_format, OF rl, unfolded hrs_htd_def])
apply simp
apply (rule tdisj)
apply (subst pa)
apply (subst ih' [simplified hrs_mem_update_def hrs_htd_update_def split_beta, simplified])
apply (rule refl)
done
qed
qed
(* Clag *)
lemma cslift_ptr_retyps_no_heap_other:
fixes p :: "'a :: mem_type ptr"
assumes clear: "\<forall>z \<in> {ptr_val p ..+ nptrs * size_of TYPE('a)}.
\<forall>n b. snd (td z) n \<noteq> Some (typ_uinfo_t TYPE('b), b)"
and tdisj: "typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b :: mem_type)"
and sz: "nptrs * size_of TYPE('a) < 2 ^ word_bits"
shows "(clift (hp, ptr_retyps nptrs p td) :: 'b :: mem_type typ_heap)
= clift (hp, td)" (is "?LHS nptrs p = ?RHS nptrs p" )
using clear sz
proof (induct nptrs arbitrary: p)
case 0
show ?case by (simp add: hrs_mem_update_def hrs_htd_update_def)
next
case (Suc n)
have pa:
"(ptr_val p + of_nat (size_of TYPE('a))) = ptr_val (CTypesDefs.ptr_add p 1)"
by (simp add: CTypesDefs.ptr_add_def)
have rl: "\<And>x. x \<in> {ptr_val p..+ size_of TYPE('a)} \<Longrightarrow> x \<in> {ptr_val p..+Suc n * size_of TYPE('a)}"
apply (erule subsetD [rotated])
apply (rule intvl_start_le)
apply simp
done
have ih': "?LHS n (CTypesDefs.ptr_add p 1) = ?RHS n (CTypesDefs.ptr_add p 1)"
proof (rule Suc.hyps, rule ballI)
fix z
assume zin: "z \<in> {ptr_val (CTypesDefs.ptr_add p 1)..+n * size_of TYPE('a)}"
hence "z \<in> {ptr_val p..+Suc n * size_of TYPE('a)}"
apply (rule subsetD [rotated])
apply (simp add: CTypesDefs.ptr_add_def)
apply (rule intvl_sub_offset)
apply (simp add: unat_of_nat)
done
thus "\<forall>n b. snd (td z) n \<noteq> Some (typ_uinfo_t TYPE('b), b)" using Suc.prems by simp
next
from Suc.prems show "n * size_of TYPE('a) < 2 ^ word_bits" by simp
qed
show ?case
proof (rule ext)
fix p' :: "'b ptr"
have "size_of TYPE('a) + n * size_of TYPE('a) < 2 ^ word_bits" using Suc.prems by simp
thus "?LHS (Suc n) p p' = ?RHS (Suc n) p p'"
apply simp
apply (subst lift_t_retyp_no_heap_other0)
apply (clarsimp simp: CTypesDefs.ptr_add_def)
apply (subst(asm) ptr_retyps_out)
apply clarsimp
apply (drule orthD2 [rotated])
apply (rule init_intvl_disj [where z = "n * size_of TYPE('a)"])
apply (simp add: word_bits_conv addr_card)
apply simp
apply (simp add: Suc.prems(1)[rule_format, OF rl])
apply (rule tdisj)
apply (subst ih' [simplified hrs_mem_update_def hrs_htd_update_def split_beta, simplified])
apply (rule refl)
done
qed
qed
lemma list_map_length_is_None [simp]:
"list_map xs (length xs) = None"
apply (induct xs)
apply (simp add: list_map_def)
apply (simp add: list_map_def)
done
find_theorems h_t_valid intvl
lemma list_map_append_one:
"list_map (xs @ [x]) = [length xs \<mapsto> x] ++ list_map xs"
by (simp add: list_map_def)
lemma field_of_t_refl:
"field_of_t p p' = (p = p')"
apply (safe, simp_all add: field_of_t_def field_of_self)
apply (simp add: field_of_def)
apply (drule td_set_size_lte)
apply (simp add: unat_eq_0)
done
lemma ptr_retyp_same_cleared_region:
fixes p :: "'a :: mem_type ptr" and p' :: "'a :: mem_type ptr"
assumes ht: "ptr_retyp p td, g \<Turnstile>\<^sub>t p'"
shows "p = p' \<or> {ptr_val p..+ size_of TYPE('a)} \<inter> {ptr_val p' ..+ size_of TYPE('a)} = {}"
apply (rule disjCI2)
apply (rule h_t_valid_neq_disjoint[OF ptr_retyp_h_t_valid ht, OF TrueI])
apply simp
apply (simp add: field_of_t_refl)
done
lemma h_t_valid_ptr_retyp_inside_eq:
fixes p :: "'a :: mem_type ptr" and p' :: "'a :: mem_type ptr"
assumes inside: "ptr_val p' \<in> {ptr_val p ..+ size_of TYPE('a)}"
and ht: "ptr_retyp p td, g \<Turnstile>\<^sub>t p'"
shows "p = p'"
using ptr_retyp_same_cleared_region[OF ht] inside mem_type_self[where p=p']
by blast
lemma h_t_valid_ptr_retyp_outside:
fixes p :: "'a :: mem_type ptr" and p' :: "'a :: mem_type ptr"
assumes nin: "ptr_val p' \<notin> {ptr_val p..+size_of TYPE('a)}"
and disj: "\<forall>x \<in> dom (lift_t g (hp, td)) \<union> {p}. \<forall>y \<in> dom (lift_t g (hp, td)).
{ptr_val x ..+ size_of TYPE('a)} \<inter> {ptr_val y ..+ size_of TYPE('a)} \<noteq> {} \<longrightarrow> x = y"
shows "ptr_retyp p td, g \<Turnstile>\<^sub>t p' = td, g \<Turnstile>\<^sub>t p'"
proof
assume ht: "td,g \<Turnstile>\<^sub>t p'"
have "p \<in> dom (lift_t g (hp, td) :: 'a typ_heap) \<union> {p}" by simp
moreover from ht have "p' \<in> dom (lift_t g (hp, td))"
by (simp add: liftt_if dom_def)
ultimately have "{ptr_val p ..+ size_of TYPE('a)} \<inter> {ptr_val p' ..+ size_of TYPE('a)} = {} \<or> p = p'" using disj
by auto
thus "ptr_retyp p td,g \<Turnstile>\<^sub>t p'"
proof
assume "{ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val p'..+size_of TYPE('a)} = {}"
thus ?thesis using ht by (simp add: ptr_retyp_disjoint_iff)
next
assume "p = p'" thus ?thesis using nin by simp
qed
next
assume ht: "ptr_retyp p td,g \<Turnstile>\<^sub>t p'"
thus "td,g \<Turnstile>\<^sub>t p'" using nin ptr_retyp_same_cleared_region[OF ht]
mem_type_self ptr_retyp_disjoint_iff
by blast
qed
lemma lift_t_retyp_heap_same_nptr:
fixes p :: "'a :: mem_type ptr" and p' :: "'a :: mem_type ptr"
-- "more or less pspace_aligned, slightly different for tcbs"
assumes disj: "\<forall>x \<in> dom (lift_t g (hp, td) :: 'a typ_heap) \<union> {p}. \<forall>y \<in> dom (lift_t g (hp, td) :: 'a typ_heap).
{ptr_val x ..+ size_of TYPE('a)} \<inter> {ptr_val y ..+ size_of TYPE('a)} \<noteq> {} \<longrightarrow> x = y"
and diff: "p' \<noteq> p"
and lbs: "length bs = size_of TYPE('a)"
shows "lift_t g (heap_update_list (ptr_val p) bs hp, ptr_retyp p td) p' =
lift_t g (hp, td) p'" (is "lift_t g (?hp, ?td) p' = lift_t g (hp, td) p'")
proof (cases "ptr_val p' \<in> {ptr_val p ..+ size_of TYPE('a)}")
case True
hence "{ptr_val p ..+ size_of TYPE('a)} \<inter> {ptr_val p' ..+ size_of TYPE('a)} \<noteq> {}"
apply clarsimp
apply (drule (1) orthD1)
apply simp
done
hence "p' \<notin> dom (lift_t g (hp, td))" using disj diff
apply -
apply (rule notI)
apply (drule bspec [where x = p])
apply simp
apply (drule (1) bspec, drule (1) mp)
apply simp
done
hence "\<not> td, g \<Turnstile>\<^sub>t p'"
apply (rule contrapos_nn)
apply (clarsimp simp: liftt_if)
done
with diff show ?thesis
apply -
apply (simp add: lift_typ_heap_if lift_t_def lift_state_ptr_retyp_d_empty [OF True] s_valid_def hrs_htd_def)
apply (erule contrapos_np)
apply (clarsimp split: split_if_asm)
apply (erule h_t_valid_ptr_retyp_inside_eq [OF True, symmetric])
done
next
case False
note ht_eq = h_t_valid_ptr_retyp_outside [OF False disj]
show ?thesis using False
apply (simp add: lift_t_def lift_typ_heap_if h_t_s_valid)
apply (clarsimp simp add: ht_eq [symmetric] split: split_if)
apply (frule ptr_retyp_same_cleared_region)
apply (erule disjE)
apply simp
apply (simp add: heap_list_s_def ht_eq)
apply (subgoal_tac "{ptr_val p'..+size_of TYPE('a)} \<subseteq> {x. fst (td x)}")
apply (subst heap_list_proj_h_lift_state)
apply (fastforce simp add: ptr_retyp_d_eq_fst split: split_if)
apply (simp add: heap_list_update_disjoint_same heap_list_proj_h_lift_state lbs)
apply clarsimp
apply (drule intvlD)
apply clarsimp
apply (erule (1) h_t_valid_Some)
done
qed
lemma lift_t_retyp_heap_same_nptr':
fixes p :: "'a :: mem_type ptr" and p' :: "'a :: mem_type ptr"
-- "more or less pspace_aligned, slightly different for tcbs"
assumes disj: "\<forall>x \<in> dom (lift_t g (hp, td) :: 'a typ_heap) \<union> {p}. \<forall>y \<in> dom (lift_t g (hp, td) :: 'a typ_heap).
{ptr_val x ..+ size_of TYPE('a)} \<inter> {ptr_val y ..+ size_of TYPE('a)} \<noteq> {} \<longrightarrow> x = y"
and diff: "p' \<noteq> p"
shows "lift_t g (hp, ptr_retyp p td) p' =
lift_t g (hp, td) p'" (is "lift_t g (hp, ?td) p' = lift_t g (hp, td) p'")
proof (cases "ptr_val p' \<in> {ptr_val p ..+ size_of TYPE('a)}")
case True
hence "{ptr_val p ..+ size_of TYPE('a)} \<inter> {ptr_val p' ..+ size_of TYPE('a)} \<noteq> {}"
apply clarsimp
apply (drule (1) orthD1)
apply simp
done
hence "p' \<notin> dom (lift_t g (hp, td))" using disj diff
apply -
apply (rule notI)
apply (drule bspec [where x = p])
apply simp
apply (drule (1) bspec, drule (1) mp)
apply simp
done
hence "\<not> td, g \<Turnstile>\<^sub>t p'"
apply (rule contrapos_nn)
apply (clarsimp simp: liftt_if)
done
with diff show ?thesis
apply -
apply (simp add: lift_typ_heap_if lift_t_def lift_state_ptr_retyp_d_empty [OF True] s_valid_def hrs_htd_def)
apply (erule contrapos_np)
apply (clarsimp split: split_if_asm)
apply (erule h_t_valid_ptr_retyp_inside_eq [OF True, symmetric])
done
next
case False
note ht_eq = h_t_valid_ptr_retyp_outside [OF False disj]
show ?thesis using False
apply (simp add: lift_t_def lift_typ_heap_if h_t_s_valid)
apply (clarsimp simp add: ht_eq [symmetric] split: split_if)
apply (frule ptr_retyp_same_cleared_region)
apply (erule disjE)
apply simp
apply (simp add: heap_list_s_def ht_eq)
apply (subgoal_tac "{ptr_val p'..+size_of TYPE('a)} \<subseteq> {x. fst (td x)}")
apply (subst heap_list_proj_h_lift_state)
apply (fastforce simp add: ptr_retyp_d_eq_fst split: split_if)
apply (simp add: heap_list_update_disjoint_same heap_list_proj_h_lift_state)
apply clarsimp
apply (drule intvlD)
apply clarsimp
apply (erule (1) h_t_valid_Some)
done
qed
lemma ptr_add_orth:
fixes p :: "'a :: mem_type ptr"
assumes lt: "Suc n * size_of TYPE('a) < 2 ^ word_bits"
shows "{ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val (CTypesDefs.ptr_add p 1)..+n * size_of TYPE('a)} = {}"
using lt
apply -
apply (rule disjointI)
apply clarsimp
apply (drule intvlD)+
apply (clarsimp simp: CTypesDefs.ptr_add_def)
apply (simp only: Abs_fnat_hom_add)
apply (drule unat_cong)
apply (simp only: unat_of_nat)
apply (unfold word_bits_len_of)
apply (subst (asm) mod_less)
apply (erule order_less_trans)
apply (simp add: addr_card_wb [symmetric])
apply (subst (asm) mod_less)
apply simp
apply simp
done
lemma cslift_ptr_retyp_memset_same:
fixes p :: "'a :: mem_type ptr"
assumes guard: "\<forall>n < nptrs. c_guard (CTypesDefs.ptr_add p (of_nat n))"
assumes clear: "\<forall>z \<in> {ptr_val p ..+ nptrs * size_of TYPE('a)}.
\<forall>n b. snd ((hrs_htd hp) z) n \<noteq> Some (typ_uinfo_t TYPE('a), b)"
and size_of_m: "size_of TYPE('a) = 2 ^ m"
and al: "is_aligned (ptr_val p) m"
and clift_al: "\<forall>x \<in> dom (clift hp :: 'a typ_heap). is_aligned (ptr_val x) m"
and sz: "nptrs * size_of TYPE('a) < 2 ^ word_bits"
shows "(clift (hrs_htd_update (ptr_retyps nptrs p) hp) :: 'a :: mem_type typ_heap)
= (\<lambda>y. if y \<in> (CTypesDefs.ptr_add p o of_nat) ` {k. k < nptrs}
then Some (from_bytes (heap_list (hrs_mem hp) (size_of TYPE('a)) (ptr_val y)))
else clift hp y)"
(is "?LHS nptrs p = ?RHS nptrs p" )
using guard clear sz al