adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

CRefine adjustments for ASM translation. 

With analysis of ASM statements included, some previous modifies
proofs get weakened. This has in particular consequences for proofs
about a cache clean done during retype. Make a weak assumption here
(bytes which actually have a type are unchanged), and strengthen some
logic to fit with this.
This commit is contained in:
Thomas Sewell 2016-11-29 12:59:18 +11:00
parent 8e7c55c1a5
commit 422347cd89
11 changed files with 149 additions and 92 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
proof/crefine/Arch_C.thy
View File

@ -564,7 +564,7 @@ shows
apply simp+
apply (clarsimp simp:typ_heap_simps' region_is_bytes'_def[where sz=0])
apply (frule ccte_relation_ccap_relation)
apply (clarsimp simp: cap_get_tag_isCap)
apply (clarsimp simp: cap_get_tag_isCap hrs_htd_update)
apply (clarsimp simp: hrs_htd_update_def split_def
pageBits_def
split: split_if)
@ -575,18 +575,17 @@ shows
apply (simp add: ghost_assertion_data_get_gs_clear_region[unfolded o_def])
apply (drule valid_global_refsD_with_objSize, clarsimp)+
apply (clarsimp simp: isCap_simps dest!: ccte_relation_ccap_relation)
apply (cut_tac ptr=frame and bits=12 and s="globals_update (t_hrs_'_update (hrs_htd_update
(typ_region_bytes frame 12))) s'" in typ_region_bytes_actually_is_bytes)
apply (cut_tac ptr=frame and bits=12
and htd="typ_region_bytes frame 12 (hrs_htd (t_hrs_' (globals s')))" in typ_region_bytes_actually_is_bytes)
apply (simp add: hrs_htd_update)
apply clarsimp
apply (clarsimp simp: region_actually_is_bytes'_def[where len=0])
apply (intro conjI)
apply (clarsimp elim!:is_aligned_weaken)
apply (simp add:is_aligned_def)
apply (erule is_aligned_no_wrap',simp)
apply (drule region_actually_is_bytes_dom_s[OF _ order_refl])
apply (simp add: hrs_htd_update_def split_def)
apply (clarsimp simp: region_actually_is_bytes_def hrs_htd_update)
apply (simp add: hrs_htd_def hrs_htd_update_def split_def)
apply (simp add: hrs_htd_def)
apply (erule is_aligned_no_wrap',simp)
apply (drule region_actually_is_bytes_dom_s[OF _ order_refl])
apply (simp add: hrs_htd_def split_def)
apply (clarsimp simp: ccap_relation_def)
apply (clarsimp simp: cap_asid_pool_cap_lift)
apply (clarsimp simp: cap_to_H_def)

18
proof/crefine/CSpace_C.thy
View File

@ -2332,6 +2332,12 @@ lemma region_is_bytes_subset:
\<Longrightarrow> region_is_bytes' ptr' sz' htd"
by (auto simp: region_is_bytes'_def)
lemma region_actually_is_bytes_subset:
"region_actually_is_bytes' ptr sz htd
\<Longrightarrow> {ptr' ..+ sz'} \<subseteq> {ptr ..+ sz}
\<Longrightarrow> region_actually_is_bytes' ptr' sz' htd"
by (auto simp: region_actually_is_bytes'_def)
lemma intvl_both_le:
"\<lbrakk> a \<le> x; unat x + y \<le> unat a + b \<rbrakk>
\<Longrightarrow> {x ..+ y} \<le> {a ..+ b}"
@ -2420,7 +2426,7 @@ lemma ctes_of_untyped_zero_rf_sr_case:
untyped_ranges_zero' s \<rbrakk>
\<Longrightarrow> case untypedZeroRange (cteCap cte)
of None \<Rightarrow> True
| Some (start, end) \<Rightarrow> region_is_zero_bytes start (unat ((end + 1) - start)) s'"
| Some (start, end) \<Rightarrow> region_actually_is_zero_bytes start (unat ((end + 1) - start)) s'"
by (simp split: option.split add: ctes_of_untyped_zero_rf_sr)
lemma gsUntypedZeroRanges_update_helper:
@ -2449,7 +2455,7 @@ lemma updateTrackedFreeIndex_noop_ccorres:
\<and> idx \<le> 2 ^ capBlockSize cap
\<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) o cteCap) slot
and valid_objs' and untyped_ranges_zero')
{s. \<not> capIsDevice cap' \<longrightarrow> region_is_zero_bytes (capPtr cap' + of_nat idx) (capFreeIndex cap' - idx) s} hs
{s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_zero_bytes (capPtr cap' + of_nat idx) (capFreeIndex cap' - idx) s} hs
(updateTrackedFreeIndex slot idx) Skip"
(is "ccorres dc xfdc ?P ?P' _ _ _")
apply (simp add: updateTrackedFreeIndex_def getSlotCap_def)
@ -2478,16 +2484,16 @@ lemma updateTrackedFreeIndex_noop_ccorres:
apply clarsimp
apply (thin_tac "\<not> capIsDevice cap' \<longrightarrow> P" for P)
apply (clarsimp split: option.split_asm)
apply (subst region_is_bytes_subset, simp+)
apply (subst region_actually_is_bytes_subset, simp+)
apply (subst heap_list_is_zero_mono2, simp+)
apply (frule untypedZeroRange_idx_backward_helper[where idx=idx],
simp+)
apply (clarsimp simp: isCap_simps valid_cap_simps')
apply (clarsimp split: option.split_asm)
apply (clarsimp dest!: untypedZeroRange_not_device)
apply (subst region_is_bytes_subset, simp+)
apply (subst region_actually_is_bytes_subset, simp+)
apply (subst heap_list_is_zero_mono2, simp+)
apply (simp add: region_is_bytes'_def heap_list_zero_Ball_intvl)
apply (simp add: region_actually_is_bytes'_def heap_list_zero_Ball_intvl)
apply (clarsimp dest!: untypedZeroRange_not_device)
apply blast
apply (clarsimp simp: cte_wp_at_ctes_of)
@ -2503,7 +2509,7 @@ lemma updateTrackedFreeIndex_forward_noop_ccorres:
apply (rule ccorres_name_pre)
apply (rule ccorres_guard_imp2,
rule_tac cap'="cteCap (the (ctes_of s slot))" in updateTrackedFreeIndex_noop_ccorres)
apply (clarsimp simp: cte_wp_at_ctes_of region_is_bytes'_def)
apply (clarsimp simp: cte_wp_at_ctes_of region_actually_is_bytes'_def)
done
lemma clearUntypedFreeIndex_noop_ccorres:

2
proof/crefine/Detype_C.thy
View File

@ -1618,7 +1618,7 @@ lemma zero_ranges_are_zero_typ_region_bytes:
\<Longrightarrow> zero_ranges_are_zero rs (hrs_htd_update (typ_region_bytes ptr bits) hrs)"
apply (clarsimp simp: zero_ranges_are_zero_def)
apply (drule(1) bspec)
apply (clarsimp simp: region_is_bytes'_def typ_region_bytes_def hrs_htd_update)
apply (clarsimp simp: region_actually_is_bytes'_def typ_region_bytes_def hrs_htd_update)
done
lemma deleteObjects_ccorres':

47
proof/crefine/Invoke_C.thy
View File

@ -1942,6 +1942,21 @@ lemma eq_UntypedCap_helper:
\<Longrightarrow> cap = UntypedCap dev ptr sz idx"
by (clarsimp simp: isCap_simps)
lemma byte_regions_unmodified_actually_heap_list:
"byte_regions_unmodified hrs hrs'
\<Longrightarrow> region_actually_is_bytes' p' n' htd
\<Longrightarrow> htd = (hrs_htd hrs)
\<Longrightarrow> heap_list (hrs_mem hrs) n p = v
\<Longrightarrow> {p ..+ n} \<subseteq> {p' ..+ n'}
\<Longrightarrow> heap_list (hrs_mem hrs') n p = v"
apply (erule trans[rotated], rule heap_list_h_eq2)
apply (simp add: byte_regions_unmodified_def region_actually_is_bytes_def)
apply (drule_tac x=x in spec)
apply (drule_tac x=x in bspec)
apply blast
apply (clarsimp split: split_if_asm)
done
lemma resetUntypedCap_ccorres:
notes upt.simps[simp del] Collect_const[simp del] replicate_numeral[simp del]
shows
@ -2021,7 +2036,7 @@ lemma resetUntypedCap_ccorres:
apply (simp add: guard_is_UNIV_def)
apply wp
apply simp
apply (vcg exspec=cleanCacheRange_PoU_modifies)
apply (vcg exspec=cleanCacheRange_PoU_preserves_bytes)
apply (rule_tac P="reset_chunk_bits \<le> capBlockSize (cteCap cte)
\<and> of_nat (capFreeIndex (cteCap cte)) - 1
< (2 ^ capBlockSize (cteCap cte) :: addr)"
@ -2115,7 +2130,7 @@ lemma resetUntypedCap_ccorres:
apply (simp add: guard_is_UNIV_def)
apply (wp hoare_vcg_ex_lift doMachineOp_psp_no_overlap)
apply clarsimp
apply (vcg exspec=cleanCacheRange_PoU_modifies)
apply (vcg exspec=cleanCacheRange_PoU_preserves_bytes)
apply clarify
apply (rule conjI)
apply (clarsimp simp: invs_valid_objs' cte_wp_at_ctes_of
@ -2158,21 +2173,26 @@ lemma resetUntypedCap_ccorres:
is_aligned_mult_triv2[THEN is_aligned_weaken]
region_actually_is_bytes_subset_t_hrs[mk_strg I E]
| simp)+
apply (clarsimp simp: capAligned_def
apply (clarsimp simp: capAligned_def imp_conjL
aligned_offset_non_zero
is_aligned_add_multI conj_comms
is_aligned_mask_out_add_eq_sub[OF is_aligned_weaken])
apply (strengthen region_is_bytes_subset[OF region_actually_is_bytes, mk_strg I E]
apply (strengthen region_actually_is_bytes_subset[mk_strg I E]
heap_list_is_zero_mono[OF heap_list_update_eq]
order_trans [OF intvl_start_le
aligned_intvl_offset_subset[where sz'=reset_chunk_bits]]
| simp add: is_aligned_mult_triv2)+
byte_regions_unmodified_actually_heap_list[mk_strg I E E]
| simp add: is_aligned_mult_triv2 hrs_mem_update)+
apply (simp add: unat_sub word_le_nat_alt unat_sub[OF word_and_le2]
mask_out_sub_mask word_and_le2
unat_of_nat32[OF order_le_less_trans, rotated,
OF power_strict_increasing])
apply (case_tac idx')
(* must be contradictory *)
apply clarsimp
apply (simp add: is_aligned_def addr_card_def card_word
reset_chunk_bits_def)
apply clarsimp
apply (simp add: is_aligned_def addr_card_def card_word
reset_chunk_bits_def)
apply (simp add: unat_of_nat32[OF order_le_less_trans, rotated,
@ -2181,9 +2201,9 @@ lemma resetUntypedCap_ccorres:
unat_mod unat_of_nat mod_mod_cancel)
apply (strengthen nat_le_Suc_less_imp[OF mod_less_divisor, THEN order_trans])
apply (simp add: is_aligned_def addr_card_def card_word)
apply clarsimp
apply clarsimp
apply (rule conseqPre, vcg exspec=cleanCacheRange_PoU_modifies
apply (rule conseqPre, vcg exspec=cleanCacheRange_PoU_preserves_bytes
exspec=preemptionPoint_modifies)
apply (clarsimp simp: in_set_conv_nth isCap_simps
length_upto_enum_step upto_enum_step_nth
@ -2318,7 +2338,10 @@ lemma resetUntypedCap_ccorres:
region_is_bytes_typ_region_bytes
intvl_start_le is_aligned_power2
heap_list_is_zero_mono[OF heap_list_update_eq]
| simp add: unat_of_nat)+
byte_regions_unmodified_actually_heap_list[OF _ _ refl, mk_strg I E]
typ_region_bytes_actually_is_bytes[OF refl]
region_actually_is_bytes_subset[OF typ_region_bytes_actually_is_bytes[OF refl]]
| simp add: unat_of_nat imp_conjL hrs_mem_update hrs_htd_update)+
apply (clarsimp simp: order_trans[OF power_increasing[where a=2]]
addr_card_def card_word
is_aligned_weaken from_bool_0)
@ -2331,7 +2354,7 @@ lemma ccorres_cross_retype_zero_bytes_over_guard:
((\<lambda>s. invs' s
\<and> cte_wp_at' (\<lambda>cte. \<exists>idx. cteCap cte = UntypedCap dev (ptr && ~~ mask sz) sz idx
\<and> idx \<le> unat (ptr && mask sz)) p s) and P')
{s'. (\<not> dev \<longrightarrow> region_is_zero_bytes ptr
{s'. (\<not> dev \<longrightarrow> region_actually_is_zero_bytes ptr
(num_ret * 2 ^ APIType_capBits newType userSize) s')
\<and> (\<exists>cte cte' idx. cslift s' (cte_Ptr p) = Some cte'
\<and> ccte_relation cte cte' \<and> cteCap cte = UntypedCap dev (ptr && ~~ mask sz) sz idx)
@ -2342,7 +2365,7 @@ lemma ccorres_cross_retype_zero_bytes_over_guard:
apply (frule(2) rf_sr_cte_relation)
apply (case_tac dev)
apply fastforce
apply (frule(1) retype_offs_region_is_zero_bytes, (simp | clarsimp)+)
apply (frule(1) retype_offs_region_actually_is_zero_bytes, (simp | clarsimp)+)
apply fastforce
done
@ -2637,13 +2660,15 @@ lemma invokeUntyped_Retype_ccorres:
apply (clarsimp simp: ccHoarePost_def hrs_mem_update
object_type_from_H_bound
typ_heap_simps' word_sle_def
word_of_nat_less zero_bytes_heap_update)
word_of_nat_less zero_bytes_heap_update
region_actually_is_bytes)
apply (frule ccte_relation_ccap_relation)
apply (cut_tac vui)
apply (clarsimp simp: cap_get_tag_isCap getFreeIndex_def
cte_wp_at_ctes_of shiftL_nat
split: split_if)
apply (simp add: mask_out_sub_mask field_simps region_is_bytes'_def)
apply (clarsimp elim!: region_actually_is_bytes_subset)
apply (rule order_refl)
apply (cut_tac misc us_misc' proofs us_misc bits_low

6
proof/crefine/Machine_C.thy
View File

@ -74,6 +74,12 @@ assumes cleanByVA_PoU_ccorres:
(doMachineOp (cleanByVA_PoU w1 w2))
(Call cleanByVA_PoU_'proc)"
assumes cleanByVA_PoU_preserves_kernel_bytes:
"\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call cleanByVA_PoU_'proc
{t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))
\<and> (\<forall>x. snd (hrs_htd (t_hrs_' (globals s)) x) 0 \<noteq> None
\<longrightarrow> hrs_mem (t_hrs_' (globals t)) x = hrs_mem (t_hrs_' (globals s)) x)}"
assumes invalidateByVA_ccorres:
"ccorres dc xfdc \<top> (\<lbrace>\<acute>vaddr = w1\<rbrace> \<inter> \<lbrace>\<acute>paddr = w2\<rbrace>) []
(doMachineOp (invalidateByVA w1 w2))

2
proof/crefine/Recycle_C.thy
View File

@ -1289,7 +1289,7 @@ lemma updateFreeIndex_ccorres:
and untyped_ranges_zero'
and (\<lambda>_. is_aligned (of_nat idx' :: word32) 4 \<and> idx' \<le> 2 ^ (capBlockSize cap')))
{s. \<not> capIsDevice cap'
\<longrightarrow> region_is_zero_bytes (capPtr cap' + of_nat idx') (capFreeIndex cap' - idx') s} hs
\<longrightarrow> region_actually_is_zero_bytes (capPtr cap' + of_nat idx') (capFreeIndex cap' - idx') s} hs
(updateFreeIndex srcSlot idx') c"
(is "_ \<Longrightarrow> ccorres dc xfdc (valid_objs' and ?cte_wp_at' and _ and _) ?P' hs ?a c")
apply (rule ccorres_gen_asm)

109
proof/crefine/Retype_C.thy
View File

@ -1497,11 +1497,11 @@ lemma region_is_bytes_typ_region_bytes:
apply (simp add: subsetD split: split_if_asm)
done
lemma region_is_bytes_retyp_disjoint:
lemma region_actually_is_bytes_retyp_disjoint:
"{ptr ..+ sz} \<inter> {ptr_val (p :: 'a ptr)..+n * size_of TYPE('a :: mem_type)} = {}
\<Longrightarrow> region_is_bytes' ptr sz htd
\<Longrightarrow> region_is_bytes' ptr sz (ptr_retyps_gen n p arr htd)"
apply (clarsimp simp: region_is_bytes'_def del: impI)
\<Longrightarrow> region_actually_is_bytes' ptr sz htd
\<Longrightarrow> region_actually_is_bytes' ptr sz (ptr_retyps_gen n p arr htd)"
apply (clarsimp simp: region_actually_is_bytes'_def del: impI)
apply (subst ptr_retyps_gen_out)
apply blast
apply simp
@ -1524,7 +1524,7 @@ lemma zero_ranges_ptr_retyps:
apply (clarsimp simp: zero_ranges_are_zero_def untyped_ranges_zero_inv_def
hrs_htd_update)
apply (drule(1) bspec, clarsimp)
apply (rule region_is_bytes_retyp_disjoint, simp_all)
apply (rule region_actually_is_bytes_retyp_disjoint, simp_all)
apply (clarsimp simp: map_comp_Some_iff cteCaps_of_def
elim!: ranE)
apply (frule(1) ctes_of_valid')
@ -2638,6 +2638,7 @@ definition
where
"byte_regions_unmodified hrs hrs' \<equiv> \<forall>x. (\<forall>n td b. snd (hrs_htd hrs x) n = Some (td, b)
\<longrightarrow> td = typ_uinfo_t TYPE (word8))
\<longrightarrow> snd (hrs_htd hrs x) 0 \<noteq> None
\<longrightarrow> hrs_mem hrs' x = hrs_mem hrs x"
abbreviation
@ -2736,7 +2737,7 @@ lemma mdb_node_ptr_set_mdbNext_preserves_bytes:
lemma updateNewFreeIndex_noop_ccorres:
"ccorres dc xfdc (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)
{s. (case untypedZeroRange cap of None \<Rightarrow> True
| Some (a, b) \<Rightarrow> region_is_zero_bytes a (unat ((b + 1) - a)) s)} hs
| Some (a, b) \<Rightarrow> region_actually_is_zero_bytes a (unat ((b + 1) - a)) s)} hs
(updateNewFreeIndex slot) Skip"
(is "ccorres _ _ ?P ?P' hs _ _")
apply (simp add: updateNewFreeIndex_def getSlotCap_def)
@ -2765,19 +2766,19 @@ lemma updateNewFreeIndex_noop_ccorres:
lemma byte_regions_unmodified_region_is_bytes:
"byte_regions_unmodified hrs hrs'
\<Longrightarrow> region_is_bytes' y n (hrs_htd hrs)
\<Longrightarrow> region_actually_is_bytes' y n (hrs_htd hrs)
\<Longrightarrow> x \<in> {y ..+ n}
\<Longrightarrow> hrs_mem hrs' x = hrs_mem hrs x"
apply (clarsimp simp: byte_regions_unmodified_def)
apply (clarsimp simp: byte_regions_unmodified_def imp_conjL[symmetric])
apply (drule spec, erule mp)
apply (clarsimp simp: region_is_bytes'_def)
apply metis
apply (clarsimp simp: region_actually_is_bytes'_def)
apply (drule(1) bspec, simp split: split_if_asm)
done
lemma insertNewCap_ccorres1:
"ccorres dc xfdc (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap)
({s. (case untypedZeroRange cap of None \<Rightarrow> True
| Some (a, b) \<Rightarrow> region_is_zero_bytes a (unat ((b + 1) - a)) s)}
| Some (a, b) \<Rightarrow> region_actually_is_zero_bytes a (unat ((b + 1) - a)) s)}
\<inter> {s. ccap_relation cap (cap_' s)} \<inter> {s. parent_' s = Ptr parent}
\<inter> {s. slot_' s = Ptr slot}) []
(insertNewCap parent slot cap)
@ -2813,7 +2814,7 @@ lemma insertNewCap_ccorres1:
apply (rule conjI)
apply (clarsimp simp: cte_wp_at_ctes_of is_aligned_3_next)
apply (clarsimp split: option.split)
apply (intro allI conjI impI; simp; clarsimp)
apply (intro allI conjI impI; simp; clarsimp simp: region_actually_is_bytes)
apply (erule trans[OF heap_list_h_eq2, rotated])
apply (rule byte_regions_unmodified_region_is_bytes)
apply (erule byte_regions_unmodified_trans[rotated]
@ -4693,34 +4694,18 @@ lemma rf_sr_htd_safe:
"(s, s') \<in> rf_sr \<Longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s')))"
by (simp add: rf_sr_def cstate_relation_def Let_def)
definition
"region_actually_is_bytes ptr len s
= (\<forall>x \<in> {ptr ..+ len}. hrs_htd (t_hrs_' (globals s)) x
= (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]))"
abbreviation
"region_actually_is_zero_bytes ptr len s
\<equiv> region_actually_is_bytes ptr len s
\<and> heap_list_is_zero (hrs_mem (t_hrs_' (globals s))) ptr len"
lemma region_actually_is_bytes_dom_s:
"region_actually_is_bytes ptr len s
"region_actually_is_bytes' ptr len htd
\<Longrightarrow> S \<subseteq> {ptr ..+ len}
\<Longrightarrow> S \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s)))"
apply (clarsimp simp: region_actually_is_bytes_def dom_s_def)
\<Longrightarrow> S \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s htd"
apply (clarsimp simp: region_actually_is_bytes'_def dom_s_def)
apply fastforce
done
lemma region_actually_is_bytes:
"region_actually_is_bytes ptr len s
\<Longrightarrow> region_is_bytes ptr len s"
by (simp add: region_is_bytes'_def region_actually_is_bytes_def
split: split_if)
lemma typ_region_bytes_actually_is_bytes:
"hrs_htd (t_hrs_' (globals s)) = typ_region_bytes ptr bits htd
\<Longrightarrow> region_actually_is_bytes ptr (2 ^ bits) s"
by (clarsimp simp: region_actually_is_bytes_def typ_region_bytes_def)
"htd = typ_region_bytes ptr bits htd'
\<Longrightarrow> region_actually_is_bytes' ptr (2 ^ bits) htd"
by (clarsimp simp: region_actually_is_bytes'_def typ_region_bytes_def)
(* FIXME: need a way to avoid overruling the parser on this, it's ugly *)
lemma memzero_modifies:
@ -7622,6 +7607,16 @@ lemma copyGlobalMappings_preserves_bytes:
(simp_all add: h_t_valid_field)+)
done
lemma cleanByVA_PoU_preserves_bytes:
"\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call cleanByVA_PoU_'proc
{t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))
\<and> byte_regions_unmodified' s t}"
apply (rule allI, rule conseqPost,
rule cleanByVA_PoU_preserves_kernel_bytes[rule_format])
apply simp_all
apply (clarsimp simp: byte_regions_unmodified_def)
done
lemma cleanCacheRange_PoU_preserves_bytes:
"\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call cleanCacheRange_PoU_'proc
{t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))
@ -7631,7 +7626,7 @@ lemma cleanCacheRange_PoU_preserves_bytes:
apply (subst whileAnno_def[symmetric, where V=undefined
and I="{t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))
\<and> byte_regions_unmodified' s t}" for s])
apply (rule conseqPre, vcg)
apply (rule conseqPre, vcg exspec=cleanByVA_PoU_preserves_bytes)
apply (safe intro!: byte_regions_unmodified_hrs_mem_update
elim!: byte_regions_unmodified_trans byte_regions_unmodified_trans[rotated],
(simp_all add: h_t_valid_field)+)
@ -7661,8 +7656,9 @@ lemma Arch_createObject_preserves_bytes:
apply (safe intro!: ptr_retyp_d ptr_retyps_out)
apply (simp_all add: object_type_from_H_def Kernel_C_defs APIType_capBits_def
split: object_type.split_asm ArchTypes_H.apiobject_type.split_asm)
apply (rule byte_regions_unmodified_flip,
simp add: hrs_htd_update hrs_htd_update_canon)
apply (rule byte_regions_unmodified_flip, simp)
apply (rule byte_regions_unmodified_trans[rotated],
assumption, simp_all add: hrs_htd_update_canon hrs_htd_update)
done
lemma ptr_arr_retyps_eq_outside_dom:
@ -7670,8 +7666,6 @@ lemma ptr_arr_retyps_eq_outside_dom:
\<Longrightarrow> ptr_arr_retyps n p htd x = htd x"
by (simp add: ptr_arr_retyps_def htd_update_list_same2)
text {* NOTE: FIXME: need a way to show that
createObject will preserve a zero heap list. *}
lemma createObject_preserves_bytes:
"\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call createObject_'proc
{t. \<forall>nt. t_' s = object_type_from_H nt
@ -7758,12 +7752,12 @@ lemma offset_intvl_first_chunk_subsets_unat:
apply (simp add: word_le_nat_alt word_less_nat_alt unat_of_nat)
done
lemma retype_offs_region_is_zero_bytes:
lemma retype_offs_region_actually_is_zero_bytes:
"\<lbrakk> ctes_of s p = Some cte; (s, s') \<in> rf_sr; untyped_ranges_zero' s;
cteCap cte = UntypedCap False (ptr &&~~ mask sz) sz idx;
idx \<le> unat (ptr && mask sz);
range_cover ptr sz (getObjectSize newType userSize) num_ret \<rbrakk>
\<Longrightarrow> region_is_zero_bytes ptr
\<Longrightarrow> region_actually_is_zero_bytes ptr
(num_ret * 2 ^ APIType_capBits newType userSize) s'"
using word_unat_mask_lt[where w=ptr and m=sz]
apply -
@ -7772,7 +7766,7 @@ lemma retype_offs_region_is_zero_bytes:
apply (simp add: untypedZeroRange_def max_free_index_def word_size)
apply clarify
apply (strengthen heap_list_is_zero_mono2[mk_strg I E]
region_is_bytes_subset[mk_strg I E])
region_actually_is_bytes_subset[mk_strg I E])
apply (simp add: getFreeRef_def word_size)
apply (rule intvl_both_le)
apply (rule order_trans, rule word_plus_mono_right, erule word_of_nat_le)
@ -7815,7 +7809,7 @@ lemma insertNewCap_ccorres:
and valid_objs' and valid_cap' cap)
({s. cap_get_tag (cap_' s) = scast cap_untyped_cap
\<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (cap_' s)))) of None \<Rightarrow> True
| Some (a, b) \<Rightarrow> region_is_zero_bytes a (unat ((b + 1) - a)) s)}
| Some (a, b) \<Rightarrow> region_actually_is_zero_bytes a (unat ((b + 1) - a)) s)}
\<inter> {s. ccap_relation cap (cap_' s)} \<inter> {s. parent_' s = Ptr parent}
\<inter> {s. slot_' s = Ptr slot}) []
(insertNewCap parent slot cap)
@ -7826,18 +7820,19 @@ lemma insertNewCap_ccorres:
apply (clarsimp simp: ccap_relation_def map_option_Some_eq2)
apply (simp add: untypedZeroRange_def Let_def)
done
find_theorems untypedZeroRange
term zero_ranges_are_zero
lemma createObject_untyped_region_is_zero_bytes:
"\<forall>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s. let tp = (object_type_to_H (t_' s));
sz = APIType_capBits tp (unat (userSize_' s))
in (\<not> to_bool (deviceMemory_' s)
\<longrightarrow> region_is_zero_bytes (ptr_val (regionBase_' s)) (2 ^ sz) s)
\<longrightarrow> region_actually_is_zero_bytes (ptr_val (regionBase_' s)) (2 ^ sz) s)
\<and> is_aligned (ptr_val (regionBase_' s)) sz
\<and> sz < 32 \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> sz \<ge> 4)}
Call createObject_'proc
{t. cap_get_tag (ret__struct_cap_C_' t) = scast cap_untyped_cap
\<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True
| Some (a, b) \<Rightarrow> region_is_zero_bytes a (unat ((b + 1) - a)) t)}"
| Some (a, b) \<Rightarrow> region_actually_is_zero_bytes a (unat ((b + 1) - a)) t)}"
apply (rule allI, rule conseqPre, vcg exspec=copyGlobalMappings_modifies
exspec=Arch_initContext_modifies
exspec=cleanCacheRange_PoU_modifies)
@ -7885,7 +7880,7 @@ shows "ccorres dc xfdc
isFrameType newType)
\<and> (unat num = length destSlots)
)))
({s. (\<not> isdev \<longrightarrow> region_is_zero_bytes ptr
({s. (\<not> isdev \<longrightarrow> region_actually_is_zero_bytes ptr
(length destSlots * 2 ^ APIType_capBits newType userSize) s)}
\<inter> {s. t_' s = object_type_from_H newType}
\<inter> {s. parent_' s = cte_Ptr srcSlot}
@ -7925,7 +7920,7 @@ shows "ccorres dc xfdc
apply simp
apply (clarsimp simp: whileAnno_def)
apply (rule ccorres_rel_imp)
apply (rule_tac Q="{s. \<not> isdev \<longrightarrow> region_is_zero_bytes
apply (rule_tac Q="{s. \<not> isdev \<longrightarrow> region_actually_is_zero_bytes
(ptr + (i_' s << APIType_capBits newType userSize))
(unat (num - i_' s) * 2 ^ APIType_capBits newType userSize) s}"
in ccorres_zipWithM_x_while_genQ[where j=1, OF _ _ _ _ _ i_xf_for_sequence, simplified])
@ -8051,21 +8046,17 @@ shows "ccorres dc xfdc
apply (simp add: unat_eq_def)
apply (drule range_cover_sz')
apply (simp add: unat_eq_def word_less_nat_alt)
apply clarsimp
apply (erule heap_list_is_zero_mono)
apply (subgoal_tac "unat (num - of_nat n) \<noteq> 0")
apply simp
apply (simp only: unat_eq_0, clarsimp simp: unat_of_nat)
apply (simp add: hrs_htd_update typ_region_bytes_actually_is_bytes)
apply (simp add: hrs_htd_update typ_region_bytes_actually_is_bytes)
apply clarsimp
apply (erule heap_list_is_zero_mono)
apply (subgoal_tac "unat (num - of_nat n) \<noteq> 0")
apply simp
apply (simp only: unat_eq_0, clarsimp simp: unat_of_nat)
apply (frule range_cover_sz')
apply (clarsimp simp: Let_def hrs_htd_update
APIType_capBits_def[where ty="APIObjectType ArchTypes_H.apiobject_type.Untyped"])
apply (subst is_aligned_add, erule range_cover.aligned)
apply (simp add: is_aligned_shiftl)+
apply clarsimp
apply (rule region_is_bytes_typ_region_bytes)
apply simp
apply clarsimp
apply (subst range_cover.unat_of_nat_n)
apply (erule range_cover_le)
subgoal by simp
@ -8083,7 +8074,7 @@ shows "ccorres dc xfdc
apply clarsimp
apply (rule context_conjI)
apply (simp add: hrs_htd_update)
apply (simp add: region_is_bytes'_def, rule ballI)
apply (simp add: region_actually_is_bytes'_def, rule ballI)
apply (drule bspec, erule(1) subsetD)
apply (drule(1) orthD2)
apply (simp add: Ball_def unat_eq_def typ_bytes_region_out)

11
proof/crefine/SR_lemmas_C.thy
View File

@ -1686,6 +1686,12 @@ lemma region_is_bytes_disjoint:
apply (simp add: cleared[unfolded region_is_bytes'_def] not_byte size_of_def)
done
lemma region_actually_is_bytes:
"region_actually_is_bytes' ptr len htd
\<Longrightarrow> region_is_bytes' ptr len htd"
by (simp add: region_is_bytes'_def region_actually_is_bytes'_def
split: split_if)
lemma zero_ranges_are_zero_update[simp]:
"h_t_valid (hrs_htd hrs) c_guard (ptr :: 'a ptr)
\<Longrightarrow> typ_uinfo_t TYPE('a :: wf_type) \<noteq> typ_uinfo_t TYPE(word8)
@ -1693,6 +1699,7 @@ lemma zero_ranges_are_zero_update[simp]:
= zero_ranges_are_zero rs hrs"
apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update
intro!: ball_cong[OF refl] conj_cong[OF refl])
apply (drule region_actually_is_bytes)
apply (drule(2) region_is_bytes_disjoint)
apply (simp add: heap_update_def heap_list_update_disjoint_same Int_commute)
done
@ -2228,7 +2235,7 @@ lemma page_table_at_rf_sr:
lemma gsUntypedZeroRanges_rf_sr:
"\<lbrakk> (start, end) \<in> gsUntypedZeroRanges s; (s, s') \<in> rf_sr \<rbrakk>
\<Longrightarrow> region_is_zero_bytes start (unat ((end + 1) - start)) s'"
\<Longrightarrow> region_actually_is_zero_bytes start (unat ((end + 1) - start)) s'"
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
zero_ranges_are_zero_def)
apply (drule(1) bspec)
@ -2239,7 +2246,7 @@ lemma ctes_of_untyped_zero_rf_sr:
"\<lbrakk> ctes_of s p = Some cte; (s, s') \<in> rf_sr;
untyped_ranges_zero' s;
untypedZeroRange (cteCap cte) = Some (start, end) \<rbrakk>
\<Longrightarrow> region_is_zero_bytes start (unat ((end + 1) - start)) s'"
\<Longrightarrow> region_actually_is_zero_bytes start (unat ((end + 1) - start)) s'"
apply (erule gsUntypedZeroRanges_rf_sr[rotated])
apply (clarsimp simp: untyped_ranges_zero_inv_def)
apply (rule_tac a=p in ranI)

20
proof/crefine/StateRelation_C.thy
View File

@ -696,11 +696,29 @@ abbreviation
"region_is_zero_bytes ptr n x \<equiv> region_is_bytes ptr n x
\<and> heap_list_is_zero (hrs_mem (t_hrs_' (globals x))) ptr n"
definition
region_actually_is_bytes' :: "addr \<Rightarrow> nat \<Rightarrow> heap_typ_desc \<Rightarrow> bool"
where
"region_actually_is_bytes' ptr len htd
= (\<forall>x \<in> {ptr ..+ len}. htd x
= (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]))"
abbreviation
"region_actually_is_bytes ptr len s
\<equiv> region_actually_is_bytes' ptr len (hrs_htd (t_hrs_' (globals s)))"
lemmas region_actually_is_bytes_def = region_actually_is_bytes'_def
abbreviation
"region_actually_is_zero_bytes ptr len s
\<equiv> region_actually_is_bytes ptr len s
\<and> heap_list_is_zero (hrs_mem (t_hrs_' (globals s))) ptr len"
definition
zero_ranges_are_zero
where
"zero_ranges_are_zero rs hrs
= (\<forall>(start, end) \<in> rs. region_is_bytes' start (unat ((end + 1) - start)) (hrs_htd hrs)
= (\<forall>(start, end) \<in> rs. region_actually_is_bytes' start (unat ((end + 1) - start)) (hrs_htd hrs)
\<and> heap_list_is_zero (hrs_mem hrs) start (unat ((end + 1) - start)))"
definition (in state_rel)

2
proof/crefine/StoreWord_C.thy
View File

@ -641,6 +641,7 @@ proof (intro allI impI)
apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update base_def
heap_update_def
intro!: ball_cong[OF refl] conj_cong[OF refl])
apply (drule region_actually_is_bytes)
apply (frule(1) region_is_bytes_disjoint[rotated 2, OF h_t_valid_clift])
apply simp
apply (subst heap_list_update_disjoint_same, simp_all)
@ -949,6 +950,7 @@ proof (intro allI impI)
apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update base_def
heap_update_def
intro!: ball_cong[OF refl] conj_cong[OF refl])
apply (drule region_actually_is_bytes)
apply (frule(1) region_is_bytes_disjoint[rotated 2, OF h_t_valid_clift])
apply simp
apply (subst heap_list_update_disjoint_same, simp_all)

7
proof/crefine/Syscall_C.thy
View File

@ -1363,11 +1363,13 @@ lemma handleRecv_ccorres:
apply (simp add: liftE_bind)
apply (ctac)
apply (rule_tac P="\<lambda>s. ksCurThread s = rv" in ccorres_cross_over_guard)
apply (ctac add: receiveIPC_ccorres[unfolded dc_def])
apply (wp deleteCallerCap_ksQ_ct' hoare_vcg_all_lift)
apply clarsimp
apply (vcg exspec=deleteCallerCap_modifies)
apply (rule conseqPost[where Q'=UNIV and A'="{}"], vcg exspec=deleteCallerCap_modifies)
apply (clarsimp dest!: rf_sr_ksCurThread)
apply simp
apply clarsimp
apply (vcg exspec=handleFault_modifies)
@ -1499,6 +1501,7 @@ lemma handleRecv_ccorres:
apply (vcg exspec=isBlocked_modifies exspec=lookupCap_modifies)
apply wp
apply clarsimp
apply vcg
apply (clarsimp simp add: sch_act_sane_def)