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

x64 ainvs: rename wellformed_arch_obj to arch_valid_obj

This commit is contained in:
Miki Tanaka 2017-08-18 10:03:49 +10:00
parent 55d50c7ba9
commit 71d1d4143b
4 changed files with 27 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
proof/invariant-abstract/X64/ArchAcc_AI.thy
View File

@ -377,7 +377,7 @@ lemma update_object_valid_objs:
apply (simp add: update_object_def)
apply (wp get_object_wp set_object_valid_objs)
including unfold_objects
apply (clarsimp simp: wellformed_arch_obj_def a_type_def valid_obj_def)
apply (clarsimp simp: arch_valid_obj_def a_type_def valid_obj_def)
done
lemma update_object_iflive[wp]:
@ -521,12 +521,12 @@ lemma update_aobj_valid_arch [wp]:
by (wp valid_arch_state_lift)
lemma update_aobj_valid_objs [wp]:
"\<lbrace>valid_objs and wellformed_arch_obj obj\<rbrace> update_object ptr (ArchObj obj) \<lbrace>\<lambda>_. valid_objs\<rbrace>"
"\<lbrace>valid_objs and arch_valid_obj obj\<rbrace> update_object ptr (ArchObj obj) \<lbrace>\<lambda>_. valid_objs\<rbrace>"
apply (simp add: update_object_def)
apply (wp set_object_valid_objs get_object_wp)
apply (clarsimp simp: a_type_def split: kernel_object.split_asm if_split_asm)
including unfold_objects
by (clarsimp simp: a_type_def valid_obj_def wellformed_arch_obj_def)
by (clarsimp simp: a_type_def valid_obj_def arch_valid_obj_def)
lemma update_aobj_valid_idle[wp]:
"\<lbrace>\<lambda>s. valid_idle s\<rbrace>
@ -1362,7 +1362,7 @@ lemma store_pte_valid_objs [wp]:
apply (wp|wpc)+
apply (clarsimp simp: valid_objs_def dom_def simp del: fun_upd_apply)
apply (erule allE, erule impE, blast)
apply (clarsimp simp: valid_obj_def wellformed_arch_obj_def)
apply (clarsimp simp: valid_obj_def arch_valid_obj_def)
done
lemma store_pde_valid_objs [wp]:
@ -1372,7 +1372,7 @@ lemma store_pde_valid_objs [wp]:
apply (wp|wpc)+
apply (clarsimp simp: valid_objs_def dom_def simp del: fun_upd_apply)
apply (erule allE, erule impE, blast)
apply (clarsimp simp: valid_obj_def wellformed_arch_obj_def)
apply (clarsimp simp: valid_obj_def arch_valid_obj_def)
done
lemma store_pdpte_valid_objs [wp]:
@ -1382,7 +1382,7 @@ lemma store_pdpte_valid_objs [wp]:
apply (wp|wpc)+
apply (clarsimp simp: valid_objs_def dom_def simp del: fun_upd_apply)
apply (erule allE, erule impE, blast)
apply (clarsimp simp: valid_obj_def wellformed_arch_obj_def)
apply (clarsimp simp: valid_obj_def arch_valid_obj_def)
done
lemma store_pml4e_arch [wp]:
@ -1885,7 +1885,7 @@ lemma update_object_invs[wp]:
\<and> obj_at (\<lambda>ko. case obj of PageMapL4 pm \<Rightarrow> \<exists>pm'. ko = ArchObj (PageMapL4 pm') \<and> (\<forall>x\<in>kernel_mapping_slots. pm x = pm' x) | _ \<Rightarrow> True) ptr s
\<and> valid_kernel_mappings_if_pm (set (second_level_tables (arch_state s))) (ArchObj obj)
\<and> valid_global_objs_upd ptr obj (arch_state s)
\<and> ((\<exists>\<rhd> ptr) s \<longrightarrow> (valid_vspace_obj obj s)) \<and> (wellformed_arch_obj obj s)
\<and> ((\<exists>\<rhd> ptr) s \<longrightarrow> (valid_vspace_obj obj s)) \<and> (arch_valid_obj obj s)
(* Lattice Preserving *)
\<and> (\<forall>nref np nq stepref. ((nref, np) \<in> (vs_lookup1 s)\<^sup>* `` refs_diff vs_lookup1_on_heap_obj obj ptr s
@ -2659,7 +2659,7 @@ lemma valid_vspace_obj_from_invs:
done
lemma valid_obj_from_invs:
"\<lbrakk>kheap s p = Some (ArchObj ao); invs s\<rbrakk> \<Longrightarrow> wellformed_arch_obj ao s"
"\<lbrakk>kheap s p = Some (ArchObj ao); invs s\<rbrakk> \<Longrightarrow> arch_valid_obj ao s"
by (auto simp: valid_obj_def valid_objs_def obj_at_def dom_def dest!:invs_valid_objs)
lemmas vs_ref_lvl_obj_simps[simp] = vs_ref_lvl_def[split_simps kernel_object.split option.split]
@ -2888,7 +2888,7 @@ lemma set_asid_pool_valid_objs [wp]:
apply (simp add: set_asid_pool_def)
apply (wp set_object_valid_objs get_object_wp)
including unfold_objects
by (clarsimp simp: a_type_def valid_obj_def wellformed_arch_obj_def)
by (clarsimp simp: a_type_def valid_obj_def arch_valid_obj_def)
lemma set_asid_pool_global_objs [wp]:
"\<lbrace>valid_global_objs and valid_arch_state\<rbrace>

8
proof/invariant-abstract/X64/ArchDetype_AI.thy
View File

@ -176,11 +176,11 @@ lemma hyp_refsym : "sym_refs (state_hyp_refs_of s)"
lemma hyp_refs_of: "\<And>obj p. \<lbrakk> ko_at obj p s \<rbrakk> \<Longrightarrow> hyp_refs_of obj \<subseteq> (UNIV - untyped_range cap \<times> UNIV)"
by (fastforce intro: hyp_refs_of_live dest!: hyp_sym_refs_ko_atD[OF _ hyp_refsym] live_okE)
lemma wellformed_arch_obj[detype_invs_proofs]:
"\<And>p ao. \<lbrakk>ko_at (ArchObj ao) p s; wellformed_arch_obj ao s\<rbrakk>
\<Longrightarrow> wellformed_arch_obj ao (detype (untyped_range cap) s)"
lemma arch_valid_obj[detype_invs_proofs]:
"\<And>p ao. \<lbrakk>ko_at (ArchObj ao) p s; arch_valid_obj ao s\<rbrakk>
\<Longrightarrow> arch_valid_obj ao (detype (untyped_range cap) s)"
apply (frule hyp_refs_of)
apply (auto simp: wellformed_arch_obj_def split: arch_kernel_obj.splits option.splits)
apply (auto simp: arch_valid_obj_def split: arch_kernel_obj.splits option.splits)
done
lemma sym_hyp_refs_detype[detype_invs_proofs]:

22
proof/invariant-abstract/X64/ArchInvariants_AI.thy
View File

@ -435,9 +435,9 @@ where
| _ \<Rightarrow> True"
definition
wellformed_arch_obj :: "arch_kernel_obj \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
arch_valid_obj :: "arch_kernel_obj \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where
"wellformed_arch_obj ao s \<equiv> wellformed_vspace_obj ao"
"arch_valid_obj ao s \<equiv> wellformed_vspace_obj ao"
lemmas
wellformed_pte_simps[simp] =
@ -456,15 +456,15 @@ lemmas
wellformed_pml4e_def[split_simps pml4e.split]
lemmas
wellformed_arch_obj_simps[simp] =
wellformed_arch_obj_def[split_simps arch_kernel_obj.split]
arch_valid_obj_simps[simp] =
arch_valid_obj_def[split_simps arch_kernel_obj.split]
lemmas
wellformed_vspace_obj_simps[simp] =
wellformed_vspace_obj_def[split_simps arch_kernel_obj.split]
lemma wellformed_arch_pspace: "\<And>ao. \<lbrakk>wellformed_arch_obj ao s; kheap s = kheap s'\<rbrakk>
\<Longrightarrow> wellformed_arch_obj ao s'" by simp
lemma wellformed_arch_pspace: "\<And>ao. \<lbrakk>arch_valid_obj ao s; kheap s = kheap s'\<rbrakk>
\<Longrightarrow> arch_valid_obj ao s'" by simp
section "Virtual Memory"
@ -1445,7 +1445,7 @@ lemmas aa_type_elims[elim!] =
lemma wellformed_arch_typ:
assumes P: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
shows "\<lbrace>\<lambda>s. wellformed_arch_obj ao s\<rbrace> f \<lbrace>\<lambda>rv s. wellformed_arch_obj ao s\<rbrace>"
shows "\<lbrace>\<lambda>s. arch_valid_obj ao s\<rbrace> f \<lbrace>\<lambda>rv s. arch_valid_obj ao s\<rbrace>"
by (cases ao; clarsimp; wp)
lemma valid_vspace_obj_pspaceI:
@ -1601,8 +1601,8 @@ lemma caps_of_state_update [iff]:
"caps_of_state (f s) = caps_of_state s"
by (rule ext) (auto simp: caps_of_state_def)
lemma wellformed_arch_obj_update:
"\<And>ao. b = ArchObj ao \<Longrightarrow> wellformed_arch_obj ao (f s) = wellformed_arch_obj ao s"
lemma arch_valid_obj_update:
"\<And>ao. b = ArchObj ao \<Longrightarrow> arch_valid_obj ao (f s) = arch_valid_obj ao s"
by clarsimp
end
@ -3008,8 +3008,8 @@ lemma in_user_frame_lift:
by (wp hoare_vcg_ex_lift typ_at)
lemma wellformed_arch_default:
"wellformed_arch_obj (default_arch_object aobject_type dev us) s"
unfolding wellformed_arch_obj_def default_arch_object_def
"arch_valid_obj (default_arch_object aobject_type dev us) s"
unfolding arch_valid_obj_def default_arch_object_def
by (cases aobject_type; simp)
lemma valid_vspace_obj_default':

6
proof/invariant-abstract/X64/ArchKHeap_AI.thy
View File

@ -895,9 +895,9 @@ lemma state_hyp_refs_of_tcb_state_update:
apply (clarsimp simp add: state_hyp_refs_of_def obj_at_def split: option.splits)
done
lemma wellformed_arch_obj_same_type:
"\<lbrakk> wellformed_arch_obj ao s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk>
\<Longrightarrow> wellformed_arch_obj ao (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
lemma arch_valid_obj_same_type:
"\<lbrakk> arch_valid_obj ao s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk>
\<Longrightarrow> arch_valid_obj ao (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
by (induction ao rule: arch_kernel_obj.induct;
clarsimp simp: typ_at_same_type)