Skip to content

Commit

Permalink
remove diminished (VER-1158)
Browse files Browse the repository at this point in the history 
diminished takes two caps and asserts that one is equal to the other
except that one may have fewer rights. We remove this definition and all
references to it, replacing diminished with equality.
  • Loading branch information
Victor Phan authored and Victor Phan committed Nov 15, 2019
1 parent 1970ed0 commit b9c2854
Show file tree
Hide file tree
Showing 71 changed files with 1,088 additions and 2,048 deletions.
29 changes: 9 additions & 20 deletions proof/access-control/Arch_AC.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -267,8 +267,7 @@ lemma perform_page_table_invocation_pas_refined [wp]:
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (frule (1) cap_cur_auth_caps_of_state)
apply simp
apply (clarsimp simp: valid_pti_def cte_wp_at_caps_of_state
is_arch_diminished_def diminished_def mask_PTCap_eq)
apply (clarsimp simp: valid_pti_def cte_wp_at_caps_of_state mask_PTCap_eq)
apply (clarsimp simp: cap_auth_conferred_def update_map_data_def is_page_cap_def
cap_links_asid_slot_def cap_links_irq_def aag_cap_auth_def)
done
Expand Down Expand Up @@ -478,13 +477,6 @@ lemma kernel_base_aligned_20:
apply(simp add: kernel_base_def is_aligned_def)
done

lemma diminished_PageCapD:
"diminished (ArchObjectCap (PageCap dev p R sz m)) cap
\<Longrightarrow> \<exists>R'. cap = ArchObjectCap (PageCap dev p R' sz m)"
apply (clarsimp simp: diminished_def mask_cap_def cap_rights_update_def)
apply (fastforce simp: acap_rights_update_def split: cap.splits arch_cap.splits bool.splits)
done

(* FIXME: CLAG *)
lemmas do_machine_op_bind =
submonad_bind [OF submonad_do_machine_op submonad_do_machine_op
Expand Down Expand Up @@ -669,11 +661,10 @@ proof -
| elim conjE hd_valid_slots[THEN bspec[rotated]]
| clarsimp dest!:set_tl_subset_mp
| wpc )+
apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_diminished_def
cap_auth_conferred_def cap_rights_update_def
acap_rights_update_def update_map_data_def is_pg_cap_def
valid_page_inv_def valid_cap_simps
dest!: diminished_PageCapD cap_master_cap_eqDs)
apply (clarsimp simp: cte_wp_at_caps_of_state cap_auth_conferred_def cap_rights_update_def
acap_rights_update_def update_map_data_def is_pg_cap_def
valid_page_inv_def valid_cap_simps
dest!: cap_master_cap_eqDs)
apply (drule (1) clas_caps_of_state)
apply (simp add: cap_links_asid_slot_def label_owns_asid_slot_def)
apply (auto dest: pas_refined_Control)[1]
Expand Down Expand Up @@ -710,9 +701,7 @@ lemma perform_page_invocation_pas_refined [wp]:
pde_ref2_def auth_graph_map_mem pas_refined_refl
split: sum.splits)+)[2]
apply (clarsimp simp: cte_wp_at_caps_of_state is_transferable_is_arch_update[symmetric]
is_arch_diminished_def pte_ref_def pde_ref2_def
is_cap_simps is_pg_cap_def cap_auth_conferred_def
dest!: diminished_PageCapD)
pte_ref_def pde_ref2_def is_cap_simps is_pg_cap_def cap_auth_conferred_def)
apply (frule(1) cap_cur_auth_caps_of_state, simp)
apply (intro impI conjI;
clarsimp; (* NB: for speed *)
Expand Down Expand Up @@ -1134,8 +1123,8 @@ lemmas vmsz_aligned_t2n_neg_mask

lemma decode_arch_invocation_authorised:
"\<lbrace>invs and pas_refined aag
and cte_wp_at (diminished (cap.ArchObjectCap cap)) slot
and (\<lambda>s. \<forall>(cap, slot) \<in> set excaps. cte_wp_at (diminished cap) slot s)
and cte_wp_at ((=) (cap.ArchObjectCap cap)) slot
and (\<lambda>s. \<forall>(cap, slot) \<in> set excaps. cte_wp_at ((=) cap) slot s)
and K (\<forall>(cap, slot) \<in> {(cap.ArchObjectCap cap, slot)} \<union> set excaps.
aag_cap_auth aag (pasObjectAbs aag (fst slot)) cap \<and> is_subject aag (fst slot)
\<and> (\<forall>v \<in> cap_asid' cap. is_subject_asid aag v))\<rbrace>
Expand All @@ -1155,7 +1144,7 @@ lemma decode_arch_invocation_authorised:
split del: if_split)+
apply (clarsimp simp: authorised_asid_pool_inv_def authorised_page_table_inv_def
neq_Nil_conv invs_psp_aligned invs_vspace_objs cli_no_irqs)
apply (drule diminished_cte_wp_at_valid_cap, clarsimp+)
apply (drule cte_wp_valid_cap, clarsimp+)
apply (cases cap; simp)
\<comment> \<open>asid pool\<close>
apply (find_goal \<open>match premises in "cap = ASIDPoolCap _ _" \<Rightarrow> succeed\<close>)
Expand Down
27 changes: 7 additions & 20 deletions proof/access-control/Syscall_AC.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -113,18 +113,6 @@ lemma perform_invocation_respects:

declare AllowSend_def[simp] AllowRecv_def[simp]

lemma diminshed_IRQControlCap_eq:
"diminished IRQControlCap = ((=) IRQControlCap)"
apply (rule ext)
apply (case_tac x, auto simp: diminished_def mask_cap_def cap_rights_update_def split:bool.splits)
done

lemma diminished_DomainCap_eq:
"diminished DomainCap = ((=) DomainCap)"
apply (rule ext)
apply (case_tac x, auto simp: diminished_def mask_cap_def cap_rights_update_def split:bool.splits)
done

lemma hoare_conjunct1_R:
"\<lbrace> P \<rbrace> f \<lbrace> \<lambda> r s. Q r s \<and> Q' r s\<rbrace>,- \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,-"
apply(auto intro: hoare_post_imp_R)
Expand All @@ -136,14 +124,14 @@ lemma hoare_conjunct2_R:
done

lemma decode_invocation_authorised:
"\<lbrace>pas_refined aag and valid_cap cap and invs and ct_active and cte_wp_at (diminished cap) slot
"\<lbrace>pas_refined aag and valid_cap cap and invs and ct_active and cte_wp_at ((=) cap) slot
and ex_cte_cap_to slot
and (\<lambda>s. \<forall>r\<in>zobj_refs cap. ex_nonz_cap_to r s)
and (\<lambda>s. \<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_to r s)
and (\<lambda>s. \<forall>cap \<in> set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_to r s)
and (\<lambda>s. \<forall>x \<in> set excaps. s \<turnstile> (fst x))
and (\<lambda>s. \<forall>x \<in> set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s)
and (\<lambda>s. \<forall>x \<in> set excaps. cte_wp_at (diminished (fst x)) (snd x) s)
and (\<lambda>s. \<forall>x \<in> set excaps. cte_wp_at ((=) (fst x)) (snd x) s)
and (\<lambda>s. \<forall>x \<in> set excaps. real_cte_at (snd x) s)
and (\<lambda>s. \<forall>x \<in> set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s)
and (\<lambda>s. \<forall>x \<in> set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s)
Expand All @@ -161,7 +149,7 @@ lemma decode_invocation_authorised:
decode_cnode_inv_authorised
decode_tcb_invocation_authorised decode_tcb_inv_wf
decode_arch_invocation_authorised
| strengthen cnode_diminished_strg
| strengthen cnode_eq_strg
| wpc | simp add: comp_def authorised_invocation_def decode_invocation_def
split del: if_split del: hoare_True_E_R
| wp (once) hoare_FalseE_R)+
Expand All @@ -178,17 +166,16 @@ lemma decode_invocation_authorised:
apply (clarsimp simp: cap_auth_conferred_def cap_rights_to_auth_def
pas_refined_Control[symmetric] reply_cap_rights_to_auth_def)

apply ((clarsimp simp: valid_cap_def cte_wp_at_eq_simp
is_cap_simps pas_refined_all_auth_is_owns
apply ((clarsimp simp: valid_cap_def is_cap_simps pas_refined_all_auth_is_owns
ex_cte_cap_wp_to_weakenE[OF _ TrueI]
cap_auth_conferred_def cap_rights_to_auth_def
| rule conjI | (subst split_paired_Ex[symmetric], erule exI)
| erule cte_wp_at_weakenE
| drule(1) bspec
| erule diminished_no_cap_to_obj_with_diff_ref)+)[1]
apply (simp only: domain_sep_inv_def diminished_DomainCap_eq)
| erule eq_no_cap_to_obj_with_diff_ref)+)[1]
apply (simp only: domain_sep_inv_def)
apply (rule impI, erule subst, rule pas_refined_sita_mem [OF sita_controlled],
auto simp: cte_wp_at_caps_of_state diminshed_IRQControlCap_eq)[1]
auto simp: cte_wp_at_caps_of_state)[1]

apply (clarsimp simp add: cap_links_irq_def )
apply (drule (1) pas_refined_Control, simp)
Expand Down
Loading

0 comments on commit b9c2854

Please sign in to comment.