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

SELFOUR-444: Finished InfoFlow and DRefine.

This commit is contained in:
Thomas Sewell 2016-05-26 17:51:53 +10:00
parent 69f7be9917
commit a96346e308
16 changed files with 1009 additions and 1186 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/EquivValid.thy
View File

@ -494,7 +494,7 @@ lemma liftME_ev:
lemma whenE_ev:
assumes a: "b \<Longrightarrow> equiv_valid_inv I A P m"
shows "equiv_valid_inv I A P (whenE b m)"
shows "equiv_valid_inv I A (\<lambda>s. b \<longrightarrow> P s) (whenE b m)"
unfolding whenE_def by (auto intro: a returnOk_ev_pre)
lemma whenE_throwError_bindE_ev:

36
proof/access-control/Access.thy
View File

@ -1596,41 +1596,7 @@ lemma cap_cur_auth_caps_of_state:
\<Longrightarrow> pas_cap_cur_auth aag cap"
by (metis cap_auth_caps_of_state)
lemma new_range_subset':
assumes al: "is_aligned (ptr :: 'a :: len word) sz" and al': "is_aligned x sz'"
and szv: "sz' \<le> sz" and xsz: "x < 2 ^ sz"
shows "{ptr + x .. (ptr + x) + 2 ^ sz' - 1} \<subseteq> {ptr .. ptr + 2 ^ sz - 1}"
using al
proof (rule is_aligned_get_word_bits)
assume p0: "ptr = 0" and szv': "len_of TYPE ('a) \<le> sz"
hence "(2 :: 'a word) ^ sz = 0" by simp
thus ?thesis using p0
apply -
apply (erule ssubst)
apply simp
done
next
assume szv': "sz < len_of TYPE('a)"
hence blah: "2 ^ (sz - sz') < (2 :: nat) ^ len_of TYPE('a)"
using szv
apply -
apply (rule power_strict_increasing, simp+)
done
show ?thesis using szv szv'
apply (intro range_subsetI)
apply (rule is_aligned_no_wrap' [OF al xsz])
apply (simp only: add_diff_eq[symmetric])
apply (subst add.assoc, rule word_plus_mono_right)
apply (subst iffD1 [OF le_m1_iff_lt])
apply (simp add: p2_gt_0 word_bits_conv)
apply (rule is_aligned_add_less_t2n[OF al' _ szv xsz])
apply simp
apply (simp add: field_simps szv al is_aligned_no_overflow)
done
qed
lemmas new_range_subset' = aligned_range_offset_subset
lemmas ptr_range_subset = new_range_subset' [folded ptr_range_def]
lemma pbfs_less_wb:

11
proof/drefine/Arch_DR.thy
View File

@ -1931,12 +1931,9 @@ proof -
set_cap_caps_no_overlap set_cap_no_overlap
set_cap_cte_wp_at set_cap_cte_cap_wp_to)
apply (simp add:region_in_kernel_window_def obj_bits_api_def default_arch_object_def)
apply (wp set_untyped_cap_caps_overlap_reserved get_cap_wp)
apply (rule hoare_strengthen_post)
apply (rule set_cap_device_and_range_aligned[where dev = False,simp])
apply simp
apply simp
apply (wp set_untyped_cap_caps_overlap_reserved get_cap_wp)
apply (wp set_untyped_cap_caps_overlap_reserved get_cap_wp
set_cap_no_overlap set_cap_cte_wp_at
| strengthen exI[where x=cref])+
apply clarsimp
apply clarsimp
apply (intro set_eqI)
@ -1948,7 +1945,7 @@ proof -
2 \<le> page_bits" in hoare_gen_asm)
apply (simp add: delete_objects_rewrite is_aligned_neg_mask_eq)
apply (rule_tac Q="\<lambda>_ s.
invs s \<and> valid_etcbs s \<and> pspace_no_overlap frame pageBits s \<and>
invs s \<and> valid_etcbs s \<and> pspace_no_overlap_range_cover frame pageBits s \<and>
descendants_range_in (untyped_range (cap.UntypedCap False frame pageBits idx)) cref s \<and>
cte_wp_at (op = (cap.UntypedCap False frame pageBits idx)) cref s \<and>
cte_wp_at (op = cap.NullCap) cnode_ref s \<and>

8
proof/drefine/Finalise_DR.thy
View File

@ -1842,12 +1842,12 @@ lemma dcorres_unmap_large_section:
apply (simp add:pd_bits_def pageBits_def)
apply (simp add:shiftr_shiftl1)
apply (subst (asm) is_aligned_neg_mask_eq[where n = 2])
apply (erule aligned_after_mask[OF aligned_add_aligned])
apply (erule is_aligned_andI1[OF aligned_add_aligned])
apply (simp add:shiftl_t2n[symmetric,where n =2,
simplified field_simps,simplified] is_aligned_shiftl_self)
apply simp
apply (subst (asm) is_aligned_neg_mask_eq[where n = 2])
apply (erule aligned_after_mask[OF is_aligned_weaken])
apply (erule is_aligned_andI1[OF is_aligned_weaken])
apply simp
apply (subst (asm) and_mask_plus)
apply (erule(1) lookup_pd_slot_aligned_6)
@ -1954,12 +1954,12 @@ lemma dcorres_unmap_large_page:
apply (simp add:pt_bits_def pageBits_def)
apply (simp add:shiftr_shiftl1)
apply (subst (asm) is_aligned_neg_mask_eq[where n = 2])
apply (erule aligned_after_mask[OF aligned_add_aligned])
apply (erule is_aligned_andI1[OF aligned_add_aligned])
apply (simp add:shiftl_t2n[symmetric,where n =2,
simplified field_simps,simplified] is_aligned_shiftl_self)
apply simp
apply (subst (asm) is_aligned_neg_mask_eq[where n = 2])
apply (erule aligned_after_mask[OF is_aligned_weaken])
apply (erule is_aligned_andI1[OF is_aligned_weaken])
apply simp
apply (subst (asm) and_mask_plus)
apply simp

9
proof/drefine/Syscall_DR.thy
View File

@ -689,12 +689,9 @@ lemma perform_invocation_corres:
apply (case_tac i')
apply (simp_all add: translate_invocation_def split: Invocations_A.invocation.splits)
(* untyped *)
apply (simp add:liftE_bindE)
apply (simp add:liftE_def returnOk_def)
apply (rule corres_guard_imp[OF corres_split'])
apply (rule invoke_untyped_corres)
apply (rule corres_trivial,simp)
apply wp
apply (simp add: liftME_def[symmetric])
apply (rule corres_guard_imp, rule invoke_untyped_corres)
apply clarsimp
apply clarsimp
(* send_ipc *)

928
proof/drefine/Untyped_DR.thy
View File

File diff suppressed because it is too large Load Diff

30
proof/infoflow/ADT_IF.thy
View File

@ -3047,6 +3047,34 @@ lemma irq_state_inv_trivE':
apply simp
done
crunch irq_state_of_state[wp]: init_arch_objects "\<lambda>s. P (irq_state_of_state s)"
(wp: crunch_wps dmo_wp ignore: do_machine_op)
lemma reset_untyped_cap_irq_state_inv:
"\<lbrace>irq_state_inv st and K (irq_is_recurring irq st)\<rbrace>
reset_untyped_cap slot \<lbrace>\<lambda>y. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>y. irq_state_next st\<rbrace>"
apply (cases "irq_is_recurring irq st", simp_all)
apply (simp add: reset_untyped_cap_def)
apply (rule hoare_pre)
apply (wp no_irq_clearMemory mapME_x_wp'
hoare_vcg_const_imp_lift
preemption_point_irq_state_inv'[where irq=irq]
| rule irq_state_inv_triv
| simp
| wp_once dmo_wp)+
done
lemma invoke_untyped_irq_state_inv:
"\<lbrace>irq_state_inv st and K (irq_is_recurring irq st)\<rbrace>
invoke_untyped ui \<lbrace>\<lambda>y. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>y. irq_state_next st\<rbrace>"
apply (cases ui, simp add: invoke_untyped_def mapM_x_def[symmetric])
apply (rule hoare_pre)
apply (wp mapM_x_wp' hoare_whenE_wp
reset_untyped_cap_irq_state_inv[where irq=irq]
| rule irq_state_inv_triv
| simp)+
done
lemma perform_invocation_irq_state_inv:
"\<lbrace>irq_state_inv st and
(\<lambda>s. \<forall>blah.
@ -3060,7 +3088,7 @@ lemma perform_invocation_irq_state_inv:
perform_invocation x y oper \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>"
apply(case_tac oper)
apply(simp | wp)+
apply((wp irq_state_inv_triv | simp)+)[4]
apply((wp invoke_untyped_irq_state_inv[where irq=irq] irq_state_inv_triv | simp)+)[4]
apply((wp invoke_tcb_irq_state_inv invoke_cnode_irq_state_inv[simplified validE_R_def] | simp add: invoke_domain_def |blast)+)[5]
apply (rule hoare_validE_cases)
apply(rule hoare_post_impErr[OF valid_validE])

26
proof/infoflow/Arch_IF.thy
View File

@ -70,9 +70,11 @@ lemma detype_irq_state_of_state[simp]:
apply(simp add: detype_def)
done
crunch irq_state_of_state[wp]: invoke_untyped "\<lambda>s. P (irq_state_of_state s)"
(wp: dmo_wp modify_wp hoare_unless_wp crunch_wps simp: crunch_simps
ignore: freeMemory simp: freeMemory_def storeWord_def clearMemory_def machine_op_lift_def machine_rest_lift_def mapM_x_defsym)
text {* Not true of invoke_untyped any more. *}
crunch irq_state_of_state[wp]: retype_region,create_cap,delete_objects "\<lambda>s. P (irq_state_of_state s)"
(wp: dmo_wp modify_wp crunch_wps
simp: crunch_simps ignore: freeMemory
simp: freeMemory_def storeWord_def clearMemory_def machine_op_lift_def machine_rest_lift_def mapM_x_defsym)
crunch irq_state_of_state[wp]: invoke_irq_control "\<lambda>s. P (irq_state_of_state s)"
@ -2184,7 +2186,7 @@ lemma perform_asid_control_invocation_globals_equiv:
word1 \<noteq> idle_thread b \<and>
(\<exists> idx. cte_wp_at (op = (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and>
descendants_of cslot_ptr2 (cdt b) = {} \<and>
pspace_no_overlap word1 pageBits b"
pspace_no_overlap_range_cover word1 pageBits b"
in hoare_strengthen_post)
prefer 2
apply (clarsimp simp: globals_equiv_def invs_valid_global_objs)
@ -2194,22 +2196,22 @@ lemma perform_asid_control_invocation_globals_equiv:
apply (rule conjI, fastforce simp: cte_wp_at_def)
apply (clarsimp simp: obj_bits_api_def default_arch_object_def)
apply (frule untyped_cap_aligned, simp add: invs_valid_objs)
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (strengthen refl caps_region_kernel_window_imp[mk_strg I E])
apply (simp add: invs_valid_objs invs_cap_refs_in_kernel_window
atLeastatMost_subset_iff word_and_le2
is_aligned_neg_mask_eq)
apply(rule conjI, rule descendants_range_caps_no_overlapI)
apply assumption
apply(simp add: is_aligned_neg_mask_eq)
apply(simp add: is_aligned_neg_mask_eq cte_wp_at_caps_of_state)
apply(simp add: is_aligned_neg_mask_eq empty_descendants_range_in)
apply(rule conjI, drule cap_refs_in_kernel_windowD2)
apply(simp add: invs_cap_refs_in_kernel_window)
apply(fastforce simp: cap_range_def is_aligned_neg_mask_eq)
apply(clarsimp simp: range_cover_def)
apply(subst is_aligned_neg_mask_eq[THEN sym], assumption)
apply(simp add: mask_neg_mask_is_zero pageBits_def)
apply (rule conjI)
apply (rule free_index_of_UntypedCap[symmetric])
apply (simp add: invs_valid_objs)
apply(wp delete_objects_invs_ex[where dev=False] delete_objects_pspace_no_overlap[where dev=False]
apply(wp add: delete_objects_invs_ex[where dev=False] delete_objects_pspace_no_overlap[where dev=False]
delete_objects_globals_equiv delete_objects_valid_ko_at_arm
hoare_vcg_ex_lift
del: Untyped_AI.delete_objects_pspace_no_overlap
| simp add: page_bits_def)+
apply (clarsimp simp: conj_comms invs_valid_ko_at_arm invs_psp_aligned invs_valid_objs valid_aci_def)
apply (clarsimp simp: cte_wp_at_caps_of_state)

16
proof/infoflow/Decode_IF.thy
View File

@ -25,8 +25,7 @@ lemma data_to_obj_type_rev:
lemma ensure_empty_rev:
"reads_equiv_valid_inv A aag (K (is_subject aag (fst slot))) (ensure_empty slot)"
unfolding ensure_empty_def fun_app_def
apply (wp get_cap_rev)
apply simp
apply (wp get_cap_rev | simp)+
done
@ -116,11 +115,14 @@ lemma decode_cnode_invocation_rev:
unfolding decode_cnode_invocation_def fun_app_def
apply (rule equiv_valid_guard_imp)
apply (simp add: unlessE_whenE)
apply (wp if_apply_ev derive_cap_rev whenE_inv hoare_vcg_imp_lift_R
apply wp
apply ((wp if_apply_ev derive_cap_rev whenE_inv hoare_vcg_imp_lift_R
lookup_slot_for_cnode_op_rev hoare_vcg_all_lift_R
lookup_slot_for_cnode_op_authorised ensure_empty_rev get_cap_rev
| simp add: split_def unlessE_whenE split del: split_if
| wpc)+
del: hoare_True_E_R
| wpc
| (wp_once hoare_drop_imps, wp_once lookup_slot_for_cnode_op_authorised))+)
apply(auto dest: bspec[where x="excaps ! 0"] bspec[where x="excaps ! Suc 0"]
intro: nth_mem elim: prop_of_obj_ref_of_cnode_cap
dest!: is_cnode_into_is_subject simp: expand_len_gr_Suc_0)
@ -129,7 +131,9 @@ lemma decode_cnode_invocation_rev:
lemma range_check_ev:
"equiv_valid_inv I A \<top> (range_check v v_min v_max)"
unfolding range_check_def fun_app_def unlessE_whenE
apply wp
apply (rule equiv_valid_guard_imp)
apply wp
apply simp
done
@ -202,7 +206,7 @@ lemma OR_choice_def2: "(\<And>P. \<lbrace>P\<rbrace> (c :: bool det_ext_monad) \
lemma check_prio_rev:
"reads_respects aag l (is_subject aag \<circ> cur_thread) (check_prio prio)"
apply (clarsimp simp: check_prio_def)
apply (wp thread_get_reads_respects)
apply (wp thread_get_reads_respects hoare_drop_imps)
by (clarsimp simp: reads_equiv_def)
lemma decode_set_priority_rev:

176
proof/infoflow/FinalCaps.thy
View File

@ -2088,80 +2088,114 @@ lemma delete_objects_silc_inv:
apply (wp detype_silc_inv | simp add: ptr_range_def)+
done
(* yet another horrendous invoke_untyped proof -- TODO: clean me up *)
lemma set_cap_silc_inv_simple:
"\<lbrace> silc_inv aag st and cte_wp_at (\<lambda>cp. cap_irqs cp = cap_irqs cap
\<and> Structures_A.obj_refs cp = Structures_A.obj_refs cap) slot
and K (is_subject aag (fst slot))\<rbrace>
set_cap cap slot
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply (wp set_cap_silc_inv)
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (rule conjI; clarsimp)
apply (drule caps_of_state_cteD)
apply (frule(1) silc_invD)
apply (clarsimp simp: intra_label_cap_def)
apply (rule exI, rule conjI, assumption)
apply (simp add: cap_points_to_label_def)
apply (simp add: slots_holding_overlapping_caps_def)
apply (simp add: silc_inv_def)
done
lemma reset_untyped_cap_silc_inv:
"\<lbrace> silc_inv aag st and cte_wp_at is_untyped_cap slot
and invs and pas_refined aag
and (\<lambda>s. descendants_of slot (cdt s) = {})
and K (is_subject aag (fst slot))\<rbrace>
reset_untyped_cap slot
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: reset_untyped_cap_def)
apply (wp set_cap_silc_inv_simple | simp add: unless_def)+
apply (rule valid_validE, rule_tac Q="\<lambda>_. cte_wp_at is_untyped_cap slot
and silc_inv aag st" in hoare_strengthen_post)
apply (rule validE_valid, rule mapME_x_inv_wp, rule hoare_pre)
apply (wp mapME_x_inv_wp preemption_point_inv set_cap_cte_wp_at
set_cap_silc_inv_simple | simp)+
apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps)
apply simp
apply (wp hoare_vcg_const_imp_lift delete_objects_silc_inv get_cap_wp | simp)+
apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def)
apply (frule(1) cap_auth_caps_of_state)
apply (clarsimp simp: aag_cap_auth_def aag_has_Control_iff_owns
ptr_range_def[symmetric])
apply (frule if_unsafe_then_capD[OF caps_of_state_cteD], clarsimp+)
apply (drule ex_cte_cap_protects[OF _ _ _ _ order_refl], erule caps_of_state_cteD)
apply (clarsimp simp: descendants_range_def2 empty_descendants_range_in)
apply clarsimp+
done
lemma reset_untyped_cap_untyped_cap:
"\<lbrace>cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> P True (untyped_range cp)) slot
and invs
and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>
reset_untyped_cap slot
\<lbrace>\<lambda>rv. cte_wp_at (\<lambda>cp. P (is_untyped_cap cp) (untyped_range cp)) slot\<rbrace>"
apply (simp add: reset_untyped_cap_def)
apply (rule hoare_pre)
apply (wp set_cap_cte_wp_at | simp add: unless_def)+
apply (rule valid_validE, rule_tac Q="\<lambda>rv. cte_wp_at (\<lambda>cp. is_untyped_cap cp
\<and> is_untyped_cap cap
\<and> untyped_range cp = untyped_range cap
\<and> P True (untyped_range cp)) slot"
in hoare_strengthen_post)
apply (wp mapME_x_inv_wp preemption_point_inv set_cap_cte_wp_at
| simp | clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def
ptr_range_def[symmetric])+
apply (wp get_cap_wp)
apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps ptr_range_def[symmetric])
apply (frule if_unsafe_then_capD[OF caps_of_state_cteD], clarsimp+)
apply (drule ex_cte_cap_protects[OF _ _ _ _ order_refl], erule caps_of_state_cteD)
apply (clarsimp simp: descendants_range_def2 empty_descendants_range_in)
apply clarsimp+
done
lemma invoke_untyped_silc_inv:
"\<lbrace> silc_inv aag st and authorised_untyped_inv_state aag ui and valid_untyped_inv ui and
K (authorised_untyped_inv aag ui)\<rbrace>
"\<lbrace> silc_inv aag st and invs and pas_refined aag
and ct_active and valid_untyped_inv ui
and K (authorised_untyped_inv aag ui)\<rbrace>
invoke_untyped ui
\<lbrace> \<lambda>_. silc_inv aag st \<rbrace>"
apply(rule hoare_gen_asm)
apply(case_tac ui, simp add: mapM_x_def[symmetric] authorised_untyped_inv_def)
apply(rename_tac word1 word2 apiobjt nat list dev)
apply wp
apply(rule_tac Q="\<lambda> r s. silc_inv aag st s \<and> (\<forall> x\<in>set list. is_subject aag (fst x)) \<and> (\<forall> oref\<in>set orefs. is_subject aag oref)" in hoare_strengthen_post)
apply (wp mapM_x_wp[OF _ subset_refl] create_cap_silc_inv retype_region_silc_inv
retype_region_ret_is_subject[simplified] set_cap_silc_inv
slots_holding_overlapping_caps_from_silc_inv[where aag=aag and st=st]
hoare_vcg_ex_lift delete_objects_silc_inv get_cap_wp static_imp_wp
| erule in_set_zipE
| clarsimp simp: split_paired_Ball
| blast )+
apply(intro allI impI conjI)
apply(simp add: valid_untyped_inv_def)
apply(drule (1) silc_invD)
apply(fastforce simp: intra_label_cap_def cap_points_to_label_def)
apply(elim exE, rename_tac lslot)
apply(rule_tac x="fst lslot" in exI, simp add: authorised_untyped_inv_state_def)
apply(rule_tac x="snd lslot" in exI)
apply(drule (1) cte_wp_at_eqD2)
apply(simp add: bits_of_def)
apply(elim conjE)
apply(rule subst[rotated, OF _ slots_holding_overlapping_caps_eq])
apply assumption
apply simp
apply simp
apply(fastforce simp: authorised_untyped_inv_state_def dest: cte_wp_at_eqD2)
apply(fastforce simp: silc_inv_def)
apply(drule (1) cte_wp_at_eqD2, simp)
apply(subst (asm) bits_of_UntypedCap[symmetric], assumption)
apply(drule (1) cte_wp_at_eqD2, clarsimp simp: authorised_untyped_inv_state_def bits_of_UntypedCap ptr_range_def cte_wp_at_sym p_assoc_help)
apply(drule (1) cte_wp_at_eqD2, simp)
apply(subst (asm) bits_of_UntypedCap[symmetric], assumption)
apply(drule (1) cte_wp_at_eqD2, clarsimp simp: authorised_untyped_inv_state_def bits_of_UntypedCap ptr_range_def cte_wp_at_sym p_assoc_help)
apply(drule (1) silc_invD)
apply(fastforce simp: intra_label_cap_def cap_points_to_label_def)
apply(elim exE, rename_tac lslot)
apply(rule_tac x="fst lslot" in exI, simp)
apply(rule_tac x="snd lslot" in exI)
apply(drule (1) cte_wp_at_eqD2)
apply(simp add: bits_of_def)
apply(elim conjE)
apply(rule subst[rotated, OF _ slots_holding_overlapping_caps_eq])
apply assumption
apply simp
apply simp
apply(fastforce simp: silc_inv_def)
apply(simp add: cte_wp_at_sym)
apply(drule (1) cte_wp_at_eqD2)
apply(simp add: bits_of_UntypedCap)
apply(simp add: cte_wp_at_sym)
apply(drule (1) cte_wp_at_eqD2)
apply(clarsimp simp: bits_of_UntypedCap ptr_range_def authorised_untyped_inv_state_def word_and_le2 p_assoc_help word_and_le1)
apply(drule spec, erule impE, assumption)
apply(simp add: bits_of_UntypedCap)
apply(drule_tac y=word2 in order_trans[rotated])
apply(rule word_and_le2)
apply fastforce
apply(drule (1) cte_wp_at_eqD2, simp)
apply(subst (asm) bits_of_UntypedCap[symmetric], assumption)
apply(simp add: cte_wp_at_sym)
apply(drule (1) cte_wp_at_eqD2)
apply(clarsimp simp: bits_of_UntypedCap ptr_range_def authorised_untyped_inv_state_def p_assoc_help)
apply(drule spec, erule impE, assumption)
apply(simp add: bits_of_UntypedCap)
apply(drule_tac y=word2 in order_trans[rotated])
apply(rule word_and_le2)
by fastforce
apply (rule hoare_pre)
apply (rule_tac Q="\<lambda>_. silc_inv aag st
and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x \<in> untyped_range cp.
is_subject aag x)) (case ui of Invocations_A.Retype src_slot _ _ _ _ _ _ _ \<Rightarrow>
src_slot)" in hoare_strengthen_post)
apply (rule invoke_untyped_Q)
apply (rule hoare_pre, wp create_cap_silc_inv create_cap_pas_refined)
apply (clarsimp simp: authorised_untyped_inv_def)
apply (auto simp: cte_wp_at_caps_of_state)[1]
apply ((wp | simp)+)[1]
apply (rule hoare_pre)
apply (wp retype_region_silc_inv retype_cte_wp_at | simp)+
apply clarsimp
apply (strengthen range_cover_le[mk_strg I E])
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (simp add: invs_valid_pspace)
apply (erule ball_subset)
apply (simp add: word_and_le2 field_simps)
apply (rule hoare_pre)
apply (wp set_cap_silc_inv_simple set_cap_cte_wp_at)
apply (cases ui, clarsimp simp: cte_wp_at_caps_of_state is_cap_simps
split del: split_if cong: if_cong)
apply (clarsimp simp: authorised_untyped_inv_def)
apply (wp reset_untyped_cap_silc_inv reset_untyped_cap_untyped_cap)
apply simp
apply (cases ui, clarsimp simp: cte_wp_at_caps_of_state
authorised_untyped_inv_def)
apply (frule(1) cap_auth_caps_of_state)
apply (clarsimp simp: aag_cap_auth_def aag_has_Control_iff_owns)
done
lemma perform_page_table_invocation_silc_ionv_get_cap_helper:
"\<lbrace>silc_inv aag st and cte_wp_at (is_pt_cap or is_pg_cap) xa\<rbrace>
@ -3166,4 +3200,4 @@ lemma call_kernel_silc_inv:
end
end
end

7
proof/infoflow/IRQMasks_IF.thy
View File

@ -40,10 +40,11 @@ lemma delete_objects_irq_masks[wp]:
apply(wp dmo_wp no_irq_mapM_x no_irq | simp add: freeMemory_def no_irq_storeWord)+
done
crunch irq_masks[wp]: invoke_untyped "\<lambda>s. P (irq_masks_of_state s)"
(ignore: delete_objects wp: hoare_unless_wp
crunch_wps dmo_wp no_irq simp: crunch_simps no_irq_clearMemory no_irq_cleanCacheRange_PoU mapM_x_def_bak)
(ignore: delete_objects wp: crunch_wps dmo_wp
wp: mapME_x_inv_wp preemption_point_inv
simp: crunch_simps no_irq_clearMemory no_irq_cleanCacheRange_PoU
mapM_x_def_bak unless_def)
crunch irq_masks[wp]: cap_insert "\<lambda>s. P (irq_masks_of_state s)"
(wp: crunch_wps)

7
proof/infoflow/PasUpdates.thy
View File

@ -60,9 +60,10 @@ lemma invoke_cnode_domain_fields[wp]: "\<lbrace>domain_fields P\<rbrace> invoke_
apply (wp | wpc | clarsimp simp: without_preemption_def crunch_simps | intro impI conjI | wp_once hoare_drop_imps hoare_vcg_all_lift)+
done
crunch domain_fields[wp]: set_domain,set_priority,switch_if_required_to,set_extra_badge,attempt_switch_to,handle_send,handle_recv,handle_reply "domain_fields P" (wp: syscall_valid crunch_wps rec_del_preservation cap_revoke_preservation transfer_caps_loop_pres simp: crunch_simps check_cap_at_def filterM_mapM unless_def detype_def detype_ext_def mapM_x_defsym ignore: without_preemption filterM rec_del check_cap_at cap_revoke resetTimer ackInterrupt getFAR getDFSR getIFSR getActiveIRQ const_on_failure freeMemory)
crunch domain_fields[wp]: set_domain,set_priority,switch_if_required_to,set_extra_badge,attempt_switch_to,handle_send,handle_recv,handle_reply "domain_fields P"
(wp: syscall_valid crunch_wps rec_del_preservation cap_revoke_preservation
transfer_caps_loop_pres mapME_x_inv_wp
simp: crunch_simps check_cap_at_def filterM_mapM unless_def detype_def detype_ext_def mapM_x_defsym ignore: without_preemption filterM rec_del check_cap_at cap_revoke resetTimer ackInterrupt getFAR getDFSR getIFSR getActiveIRQ const_on_failure freeMemory)
crunch cur_domain[wp]: transfer_caps_loop, ethread_set, thread_set_priority, set_priority, set_domain, invoke_domain, cap_move_ext, recycle_cap_ext,timer_tick,

870
proof/infoflow/Retype_IF.thy
View File

File diff suppressed because it is too large Load Diff

28
proof/infoflow/Syscall_IF.thy
View File

@ -1107,8 +1107,7 @@ crunch globals_equiv[wp]: invoke_domain "globals_equiv st"
lemma perform_invocation_globals_equiv:
"\<lbrace>invs and ct_active and valid_invocation oper and globals_equiv (st :: det_ext state) and
authorised_for_globals_inv oper
and K (case oper of (InvokeUntyped i) \<Rightarrow> (0::word32) < of_nat (length (slots_of_untyped_inv i)) | _ \<Rightarrow> True)\<rbrace>
authorised_for_globals_inv oper \<rbrace>
perform_invocation blocking calling oper
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
apply (subst pi_cases)
@ -1128,30 +1127,6 @@ lemma perform_invocation_globals_equiv:
authorised_for_globals_inv_def)
done
lemma dui_length_slots:
"\<lbrace>\<top>\<rbrace>
decode_untyped_invocation label args slot cap excaps
\<lbrace>\<lambda>rv s. (0::word32) < of_nat (length (slots_of_untyped_inv rv))\<rbrace>,-"
unfolding decode_untyped_invocation_def
apply(rule hoare_pre)
apply (simp add: unlessE_def[symmetric] whenE_def[symmetric] unlessE_whenE
split del: split_if)
apply(wp whenE_throwError_wp
|wpc
|simp add: nonzero_unat_simp split del: split_if add: split_def)+
apply(intro impI, rule TrueI)
done
lemma di_untyped_length_slots:
"\<lbrace>\<top>\<rbrace>
decode_invocation label args cap_index slot cap excaps
\<lbrace>\<lambda> rv s. (case rv of (InvokeUntyped ui) \<Rightarrow> (0::word32) < of_nat (length (slots_of_untyped_inv ui)) | _ \<Rightarrow> True)\<rbrace>,-"
unfolding decode_invocation_def
apply(rule hoare_pre)
apply(wp dui_length_slots | wpc | simp add: comp_def split_def uncurry_def)+
apply auto
done
lemma handle_invocation_globals_equiv:
"\<lbrace>invs and ct_active and globals_equiv st\<rbrace> handle_invocation calling blocking \<lbrace>\<lambda>_. globals_equiv (st::det_ext state)\<rbrace>"
apply (simp add: handle_invocation_def ts_Restart_case_helper split_def
@ -1167,7 +1142,6 @@ lemma handle_invocation_globals_equiv:
set_thread_state_ct_st' set_thread_state_globals_equiv
sts_authorised_for_globals_inv
decode_invocation_authorised_globals_inv
di_untyped_length_slots
| simp add: crunch_simps invs_imps)+
apply (auto intro: st_tcb_ex_cap simp: ct_active_not_idle ct_in_state_def)
done

5
proof/invariant-abstract/ARM/ArchArch_AI.thy
View File

@ -706,7 +706,8 @@ lemma perform_asid_control_invocation_st_tcb_at:
done
lemma set_cap_idx_up_aligned_area:
"\<lbrace>K (pcap = UntypedCap dev ptr pageBits idx) and cte_wp_at (op = pcap) slot and valid_objs\<rbrace> set_cap (max_free_index_update pcap) slot
"\<lbrace>K (\<exists>idx. pcap = UntypedCap dev ptr pageBits idx) and cte_wp_at (op = pcap) slot
and valid_objs\<rbrace> set_cap (max_free_index_update pcap) slot
\<lbrace>\<lambda>rv s. (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr pageBits \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s)\<rbrace>"
apply (rule hoare_pre)
apply (wp hoare_vcg_ex_lift set_cap_cte_wp_at)
@ -717,7 +718,7 @@ lemma set_cap_idx_up_aligned_area:
p_assoc_help valid_cap_def valid_untyped_def cap_aligned_def)
done
primrec get_untyped_cap_idx :: "cap \<Rightarrow> nat"
primrec(nonexhaustive) get_untyped_cap_idx :: "cap \<Rightarrow> nat"
where "get_untyped_cap_idx (UntypedCap dev ref sz idx) = idx"
lemma aci_invs':

36
proof/invariant-abstract/Retype_AI.thy
View File

@ -290,6 +290,42 @@ lemma aligned_ranges_subset_or_disjoint:
apply arith
done
lemma aligned_range_offset_subset:
assumes al: "is_aligned (ptr :: 'a :: len word) sz" and al': "is_aligned x sz'"
and szv: "sz' \<le> sz" and xsz: "x < 2 ^ sz"
shows "{ptr + x .. (ptr + x) + 2 ^ sz' - 1} \<subseteq> {ptr .. ptr + 2 ^ sz - 1}"
using al
proof (rule is_aligned_get_word_bits)
assume p0: "ptr = 0" and szv': "len_of TYPE ('a) \<le> sz"
hence "(2 :: 'a word) ^ sz = 0" by simp
thus ?thesis using p0
apply -
apply (erule ssubst)
apply simp
done
next
assume szv': "sz < len_of TYPE('a)"
hence blah: "2 ^ (sz - sz') < (2 :: nat) ^ len_of TYPE('a)"
using szv
apply -
apply (rule power_strict_increasing, simp+)
done
show ?thesis using szv szv'
apply (intro range_subsetI)
apply (rule is_aligned_no_wrap' [OF al xsz])
apply (simp only: add_diff_eq[symmetric])
apply (subst add.assoc, rule word_plus_mono_right)
apply (subst iffD1 [OF le_m1_iff_lt])
apply (simp add: p2_gt_0 word_bits_conv)
apply (rule is_aligned_add_less_t2n[OF al' _ szv xsz])
apply simp
apply (simp add: field_simps szv al is_aligned_no_overflow)
done
qed
lemma aligned_diff:
"\<lbrakk>is_aligned (dest :: 'a :: len word) bits; is_aligned (ptr :: 'a :: len word) sz; bits \<le> sz; sz < len_of TYPE('a);
dest < ptr\<rbrakk>