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

Isabelle2018 arm: AInvs

This commit is contained in:
Gerwin Klein 2018-06-23 13:50:46 +02:00
parent 9850ae107c
commit 590b83ceb7
14 changed files with 51 additions and 61 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/invariant-abstract/ARM/ArchAcc_AI.thy
View File

@ -2947,8 +2947,6 @@ lemma unique_table_caps_pdE:
apply simp
done
lemmas unique_table_caps_pdE' = unique_table_caps_pdE[where cs="arch_caps_of x" for x, simplified]
lemma set_pd_table_caps [wp]:
"\<lbrace>valid_table_caps and (\<lambda>s.
(obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow>

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

@ -272,12 +272,10 @@ end
locale asid_update = Arch +
fixes ap asid s s'
assumes ko: "ko_at (ArchObj (ASIDPool empty)) ap s"
assumes ko: "ko_at (ArchObj (ASIDPool Map.empty)) ap s"
assumes empty: "arm_asid_table (arch_state s) asid = None"
defines "s' \<equiv> s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>"
context asid_update begin
begin
lemma vs_lookup1' [simp]:
"vs_lookup1 s' = vs_lookup1 s"
@ -416,7 +414,7 @@ lemma valid_arch_state_strg:
lemma valid_vs_lookup_at_upd_strg:
"valid_vs_lookup s \<and>
ko_at (ArchObj (ASIDPool empty)) ap s \<and>
ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and>
arm_asid_table (arch_state s) asid = None \<and>
(\<exists>ptr cap. caps_of_state s ptr = Some cap \<and> ap \<in> obj_refs cap \<and>
vs_cap_ref cap = Some [VSRef (ucast asid) None])
@ -435,7 +433,7 @@ lemma valid_vs_lookup_at_upd_strg:
lemma retype_region_ap:
"\<lbrace>\<top>\<rbrace>
retype_region ap 1 0 (ArchObject ASIDPoolObj) dev
\<lbrace>\<lambda>_. ko_at (ArchObj (arch_kernel_obj.ASIDPool empty)) ap\<rbrace>"
\<lbrace>\<lambda>_. ko_at (ArchObj (ASIDPool Map.empty)) ap\<rbrace>"
apply (rule hoare_post_imp)
prefer 2
apply (rule retype_region_obj_at)
@ -516,7 +514,7 @@ lemma cap_insert_simple_arch_caps_ap:
"\<lbrace>valid_arch_caps and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s)
and no_cap_to_obj_with_diff_ref cap {dest}
and (\<lambda>s. arm_asid_table (arch_state s) (asid_high_bits_of asid) = None)
and ko_at (ArchObj (ASIDPool empty)) ap
and ko_at (ArchObj (ASIDPool Map.empty)) ap
and K (cap = ArchObjectCap (ASIDPoolCap ap asid)) \<rbrace>
cap_insert cap src dest
\<lbrace>\<lambda>rv s. valid_arch_caps (s\<lparr>arch_state := arch_state s
@ -551,7 +549,7 @@ lemma cap_insert_simple_arch_caps_ap:
lemma valid_asid_map_asid_upd_strg:
"valid_asid_map s \<and>
ko_at (ArchObj (ASIDPool empty)) ap s \<and>
ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and>
arm_asid_table (arch_state s) asid = None \<longrightarrow>
valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>)"
apply clarsimp
@ -564,7 +562,7 @@ lemma valid_asid_map_asid_upd_strg:
lemma valid_vspace_objs_asid_upd_strg:
"valid_vspace_objs s \<and>
ko_at (ArchObj (ASIDPool empty)) ap s \<and>
ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and>
arm_asid_table (arch_state s) asid = None \<longrightarrow>
valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>)"
apply clarsimp
@ -577,7 +575,7 @@ lemma valid_vspace_objs_asid_upd_strg:
lemma valid_global_objs_asid_upd_strg:
"valid_global_objs s \<and>
ko_at (ArchObj (arch_kernel_obj.ASIDPool empty)) ap s \<and>
ko_at (ArchObj (arch_kernel_obj.ASIDPool Map.empty)) ap s \<and>
arm_asid_table (arch_state s) asid = None \<longrightarrow>
valid_global_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>)"
by clarsimp
@ -595,7 +593,7 @@ lemma cap_insert_ap_invs:
(\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and
K (cap = cap.ArchObjectCap (arch_cap.ASIDPoolCap ap asid)) and
(\<lambda>s. \<forall>irq \<in> cap_irqs cap. irq_issued irq s) and
ko_at (ArchObj (arch_kernel_obj.ASIDPool empty)) ap and
ko_at (ArchObj (arch_kernel_obj.ASIDPool Map.empty)) ap and
(\<lambda>s. ap \<notin> ran (arm_asid_table (arch_state s)) \<and>
arm_asid_table (arch_state s) (asid_high_bits_of asid) = None)\<rbrace>
cap_insert cap src dest

14
proof/invariant-abstract/ARM/ArchFinalise_AI.thy
View File

@ -372,7 +372,7 @@ lemma (* finalise_cap_cases1 *)[Finalise_AI_asms]:
| intro impI TrueI ext conjI)+)[11]
apply (simp add: arch_finalise_cap_def split del: if_split)
apply (rule hoare_pre)
apply (wpsimp simp: cap_cleanup_opt_def arch_cap_cleanup_opt_def simp_thms)+
apply (wpsimp simp: cap_cleanup_opt_def arch_cap_cleanup_opt_def)+
done
crunch typ_at_arch[wp,Finalise_AI_asms]: arch_finalise_cap,prepare_thread_delete "\<lambda>s. P (typ_at T p s)"
@ -1427,7 +1427,7 @@ lemma vs_lookup1_arch [simp]:
lemma vs_lookup_empty_table:
"(rs \<rhd> q)
(s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (ASIDPool empty)),
(s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (ASIDPool Map.empty)),
arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(x \<mapsto> p)\<rparr>\<rparr>) \<Longrightarrow>
(rs \<rhd> q) s \<or> (rs = [VSRef (ucast x) None] \<and> q = p)"
apply (erule vs_lookupE)
@ -1460,7 +1460,7 @@ lemma vs_lookup_empty_table:
lemma vs_lookup_pages_empty_table:
"(rs \<unrhd> q)
(s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (ASIDPool empty)),
(s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (ASIDPool Map.empty)),
arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(x \<mapsto> p)\<rparr>\<rparr>) \<Longrightarrow>
(rs \<unrhd> q) s \<or> (rs = [VSRef (ucast x) None] \<and> q = p)"
apply (subst (asm) vs_lookup_pages_def)
@ -1493,7 +1493,7 @@ lemma vs_lookup_pages_empty_table:
lemma set_asid_pool_empty_table_objs:
"\<lbrace>valid_vspace_objs and asid_pool_at p\<rbrace>
set_asid_pool p empty
set_asid_pool p Map.empty
\<lbrace>\<lambda>rv s. valid_vspace_objs
(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table :=
arm_asid_table (arch_state s)(asid_high_bits_of word2 \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
@ -1518,7 +1518,7 @@ lemma set_asid_pool_empty_table_objs:
lemma set_asid_pool_empty_table_lookup:
"\<lbrace>valid_vs_lookup and asid_pool_at p and
(\<lambda>s. \<exists>p'. caps_of_state s p' = Some (ArchObjectCap (ASIDPoolCap p base)))\<rbrace>
set_asid_pool p empty
set_asid_pool p Map.empty
\<lbrace>\<lambda>rv s. valid_vs_lookup
(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table :=
arm_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
@ -1541,7 +1541,7 @@ lemma set_asid_pool_empty_valid_asid_map:
"\<lbrace>\<lambda>s. valid_asid_map s \<and> asid_pool_at p s
\<and> (\<forall>asid'. \<not> ([VSRef asid' None] \<rhd> p) s)
\<and> (\<forall>p'. \<not> ([VSRef (ucast (asid_high_bits_of base)) None] \<rhd> p') s)\<rbrace>
set_asid_pool p empty
set_asid_pool p Map.empty
\<lbrace>\<lambda>rv s. valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table :=
arm_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def)
@ -1573,7 +1573,7 @@ lemma set_asid_pool_invs_table:
\<and> (\<exists>p'. caps_of_state s p' = Some (ArchObjectCap (ASIDPoolCap p base)))
\<and> (\<not> ([VSRef (ucast (asid_high_bits_of base)) None] \<rhd> p) s)
\<and> (\<forall>p'. \<not> ([VSRef (ucast (asid_high_bits_of base)) None] \<rhd> p') s)\<rbrace>
set_asid_pool p empty
set_asid_pool p Map.empty
\<lbrace>\<lambda>x s. invs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table :=
arm_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
apply (simp add: invs_def valid_state_def valid_pspace_def valid_arch_caps_def)

4
proof/invariant-abstract/ARM/ArchKernelInit_AI.thy
View File

@ -55,14 +55,14 @@ lemma init_cdt [simp]:
by (simp add: state_defs)
lemma mdp_parent_empty [simp]:
"\<not>empty \<Turnstile> x \<rightarrow> y"
"\<not>Map.empty \<Turnstile> x \<rightarrow> y"
apply clarsimp
apply (drule tranclD)
apply (clarsimp simp: cdt_parent_of_def)
done
lemma descendants_empty [simp]:
"descendants_of x empty = {}"
"descendants_of x Map.empty = {}"
by (clarsimp simp: descendants_of_def)
lemma [simp]: "\<not>is_reply_cap Structures_A.NullCap"

2
proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy
View File

@ -2877,8 +2877,6 @@ lemma unique_table_caps_pdE:
apply simp
done
lemmas unique_table_caps_pdE' = unique_table_caps_pdE[where cs="arch_caps_of x" for x, simplified]
lemma set_pd_table_caps [wp]:
"\<lbrace>valid_table_caps and (\<lambda>s.
(obj_at (empty_table {}) p s \<longrightarrow>

14
proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy
View File

@ -296,7 +296,7 @@ end
locale asid_update = Arch +
fixes ap asid s s'
assumes ko: "ko_at (ArchObj (ASIDPool empty)) ap s"
assumes ko: "ko_at (ArchObj (ASIDPool Map.empty)) ap s"
assumes empty: "arm_asid_table (arch_state s) asid = None"
defines "s' \<equiv> s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>"
@ -431,7 +431,7 @@ lemma valid_arch_state_strg:
lemma valid_vs_lookup_at_upd_strg:
"valid_vs_lookup s \<and>
ko_at (ArchObj (ASIDPool empty)) ap s \<and>
ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and>
arm_asid_table (arch_state s) asid = None \<and>
(\<exists>ptr cap. caps_of_state s ptr = Some cap \<and> ap \<in> obj_refs cap \<and>
vs_cap_ref cap = Some [VSRef (ucast asid) None])
@ -450,7 +450,7 @@ lemma valid_vs_lookup_at_upd_strg:
lemma retype_region_ap:
"\<lbrace>\<top>\<rbrace>
retype_region ap 1 0 (ArchObject ASIDPoolObj) dev
\<lbrace>\<lambda>_. ko_at (ArchObj (arch_kernel_obj.ASIDPool empty)) ap\<rbrace>"
\<lbrace>\<lambda>_. ko_at (ArchObj (arch_kernel_obj.ASIDPool Map.empty)) ap\<rbrace>"
apply (rule hoare_post_imp)
prefer 2
apply (rule retype_region_obj_at)
@ -531,7 +531,7 @@ lemma cap_insert_simple_arch_caps_ap:
"\<lbrace>valid_arch_caps and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s)
and no_cap_to_obj_with_diff_ref cap {dest}
and (\<lambda>s. arm_asid_table (arch_state s) (asid_high_bits_of asid) = None)
and ko_at (ArchObj (ASIDPool empty)) ap
and ko_at (ArchObj (ASIDPool Map.empty)) ap
and K (cap = ArchObjectCap (ASIDPoolCap ap asid)) \<rbrace>
cap_insert cap src dest
\<lbrace>\<lambda>rv s. valid_arch_caps (s\<lparr>arch_state := arch_state s
@ -566,7 +566,7 @@ lemma cap_insert_simple_arch_caps_ap:
lemma valid_asid_map_asid_upd_strg:
"valid_asid_map s \<and>
ko_at (ArchObj (ASIDPool empty)) ap s \<and>
ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and>
arm_asid_table (arch_state s) asid = None \<longrightarrow>
valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>)"
apply clarsimp
@ -579,7 +579,7 @@ lemma valid_asid_map_asid_upd_strg:
lemma valid_vspace_objs_asid_upd_strg:
"valid_vspace_objs s \<and>
ko_at (ArchObj (ASIDPool empty)) ap s \<and>
ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and>
arm_asid_table (arch_state s) asid = None \<longrightarrow>
valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>)"
apply clarsimp
@ -602,7 +602,7 @@ lemma cap_insert_ap_invs:
(\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and
K (cap = ArchObjectCap (ASIDPoolCap ap asid)) and
(\<lambda>s. \<forall>irq \<in> cap_irqs cap. irq_issued irq s) and
ko_at (ArchObj (ASIDPool empty)) ap and
ko_at (ArchObj (ASIDPool Map.empty)) ap and
(\<lambda>s. ap \<notin> ran (arm_asid_table (arch_state s)) \<and>
arm_asid_table (arch_state s) (asid_high_bits_of asid) = None)\<rbrace>
cap_insert cap src dest

12
proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy
View File

@ -2165,7 +2165,7 @@ lemma vs_lookup1_arch [simp]:
lemma vs_lookup_empty_table:
"(rs \<rhd> q)
(s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (ASIDPool empty)),
(s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (ASIDPool Map.empty)),
arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(x \<mapsto> p)\<rparr>\<rparr>) \<Longrightarrow>
(rs \<rhd> q) s \<or> (rs = [VSRef (ucast x) None] \<and> q = p)"
apply (erule vs_lookupE)
@ -2198,7 +2198,7 @@ lemma vs_lookup_empty_table:
lemma vs_lookup_pages_empty_table:
"(rs \<unrhd> q)
(s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (ASIDPool empty)),
(s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (ASIDPool Map.empty)),
arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(x \<mapsto> p)\<rparr>\<rparr>) \<Longrightarrow>
(rs \<unrhd> q) s \<or> (rs = [VSRef (ucast x) None] \<and> q = p)"
apply (subst (asm) vs_lookup_pages_def)
@ -2231,7 +2231,7 @@ lemma vs_lookup_pages_empty_table:
lemma set_asid_pool_empty_table_objs:
"\<lbrace>valid_vspace_objs and asid_pool_at p\<rbrace>
set_asid_pool p empty
set_asid_pool p Map.empty
\<lbrace>\<lambda>rv s. valid_vspace_objs
(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table :=
arm_asid_table (arch_state s)(asid_high_bits_of word2 \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
@ -2256,7 +2256,7 @@ lemma set_asid_pool_empty_table_objs:
lemma set_asid_pool_empty_table_lookup:
"\<lbrace>valid_vs_lookup and asid_pool_at p and
(\<lambda>s. \<exists>p'. caps_of_state s p' = Some (ArchObjectCap (ASIDPoolCap p base)))\<rbrace>
set_asid_pool p empty
set_asid_pool p Map.empty
\<lbrace>\<lambda>rv s. valid_vs_lookup
(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table :=
arm_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
@ -2279,7 +2279,7 @@ lemma set_asid_pool_empty_valid_asid_map:
"\<lbrace>\<lambda>s. valid_asid_map s \<and> asid_pool_at p s
\<and> (\<forall>asid'. \<not> ([VSRef asid' None] \<rhd> p) s)
\<and> (\<forall>p'. \<not> ([VSRef (ucast (asid_high_bits_of base)) None] \<rhd> p') s)\<rbrace>
set_asid_pool p empty
set_asid_pool p Map.empty
\<lbrace>\<lambda>rv s. valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table :=
arm_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def)
@ -2311,7 +2311,7 @@ lemma set_asid_pool_invs_table:
\<and> (\<exists>p'. caps_of_state s p' = Some (ArchObjectCap (ASIDPoolCap p base)))
\<and> (\<not> ([VSRef (ucast (asid_high_bits_of base)) None] \<rhd> p) s)
\<and> (\<forall>p'. \<not> ([VSRef (ucast (asid_high_bits_of base)) None] \<rhd> p') s)\<rbrace>
set_asid_pool p empty
set_asid_pool p Map.empty
\<lbrace>\<lambda>x s. invs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table :=
arm_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
apply (simp add: invs_def valid_state_def valid_pspace_def valid_arch_caps_def)

4
proof/invariant-abstract/ARM_HYP/ArchKernelInit_AI.thy
View File

@ -55,14 +55,14 @@ lemma init_cdt [simp]:
by (simp add: state_defs)
lemma mdp_parent_empty [simp]:
"\<not>empty \<Turnstile> x \<rightarrow> y"
"\<not>Map.empty \<Turnstile> x \<rightarrow> y"
apply clarsimp
apply (drule tranclD)
apply (clarsimp simp: cdt_parent_of_def)
done
lemma descendants_empty [simp]:
"descendants_of x empty = {}"
"descendants_of x Map.empty = {}"
by (clarsimp simp: descendants_of_def)
lemma [simp]: "\<not>is_reply_cap Structures_A.NullCap"

4
proof/invariant-abstract/CSpace_AI.thy
View File

@ -2605,7 +2605,7 @@ qed
lemmas parency_m_n' =
parency_m_n [where p="s_d_swp p" and p'="s_d_swp p'", simplified, folded s_d_swp_def]
parency_m_n [where p="s_d_swp p" and p'="s_d_swp p'" for p p', simplified, folded s_d_swp_def]
lemma parency:
@ -4415,7 +4415,7 @@ lemma of_nat_ucast:
apply (rule nat_int.Rep_eqD)
apply (simp only: zmod_int)
apply (rule mod_mod_cancel)
apply (subst zdvd_int[symmetric])
apply (simp add: dvd_power_same)
apply (rule le_imp_power_dvd)
apply (simp add: is_down_def target_size_def source_size_def word_size)
done

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

@ -800,7 +800,7 @@ lemma caps_of_state_foldr:
(\<lambda>(oref,cref). if oref \<in> set addrs
then (case ty of Structures_A.CapTableObject \<Rightarrow> empty_cnode us
| Structures_A.TCBObject \<Rightarrow> option_map (\<lambda>x. cap.NullCap) \<circ> tcb_cap_cases
| _ \<Rightarrow> empty) cref
| _ \<Rightarrow> Map.empty) cref
else caps_of_state s (oref,cref))"
apply (rule ext)+
apply (case_tac x)

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

@ -2178,10 +2178,6 @@ lemma unique_table_caps_pdE:
apply simp
done
lemmas unique_table_caps_pml4E' = unique_table_caps_pml4E[where cs="arch_caps_of x" for x, simplified]
lemmas unique_table_caps_pdptE' = unique_table_caps_pdptE[where cs="arch_caps_of x" for x, simplified]
lemmas unique_table_caps_pdE' = unique_table_caps_pdE[where cs="arch_caps_of x" for x, simplified]
(* FIXME: valid_globals_refsD is used here, so it might be still useful *)
lemma eq_ucast_word9[simp]:

16
proof/invariant-abstract/X64/ArchArch_AI.thy
View File

@ -287,7 +287,7 @@ end
locale asid_update = Arch +
fixes ap asid s s'
assumes ko: "ko_at (ArchObj (ASIDPool empty)) ap s"
assumes ko: "ko_at (ArchObj (ASIDPool Map.empty)) ap s"
assumes empty: "x64_asid_table (arch_state s) asid = None"
defines "s' \<equiv> s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table := x64_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>"
@ -414,7 +414,7 @@ lemma valid_arch_state_strg:
lemma valid_vs_lookup_at_upd_strg:
"valid_vs_lookup s \<and>
ko_at (ArchObj (ASIDPool empty)) ap s \<and>
ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and>
x64_asid_table (arch_state s) asid = None \<and>
(\<exists>ptr cap. caps_of_state s ptr = Some cap \<and> ap \<in> obj_refs cap \<and>
vs_cap_ref cap = Some [VSRef (ucast asid) None])
@ -433,7 +433,7 @@ lemma valid_vs_lookup_at_upd_strg:
lemma retype_region_ap:
"\<lbrace>\<top>\<rbrace>
retype_region ap 1 0 (ArchObject ASIDPoolObj) dev
\<lbrace>\<lambda>_. ko_at (ArchObj (ASIDPool empty)) ap\<rbrace>"
\<lbrace>\<lambda>_. ko_at (ArchObj (ASIDPool Map.empty)) ap\<rbrace>"
apply (rule hoare_post_imp)
prefer 2
apply (rule retype_region_obj_at)
@ -513,7 +513,7 @@ lemma cap_insert_simple_arch_caps_ap:
"\<lbrace>valid_arch_caps and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s)
and no_cap_to_obj_with_diff_ref cap {dest}
and (\<lambda>s. x64_asid_table (arch_state s) (asid_high_bits_of asid) = None)
and ko_at (ArchObj (ASIDPool empty)) ap
and ko_at (ArchObj (ASIDPool Map.empty)) ap
and K (cap = ArchObjectCap (ASIDPoolCap ap asid)) \<rbrace>
cap_insert cap src dest
\<lbrace>\<lambda>rv s. valid_arch_caps (s\<lparr>arch_state := arch_state s
@ -548,7 +548,7 @@ lemma cap_insert_simple_arch_caps_ap:
lemma valid_asid_map_asid_upd_strg:
"valid_asid_map s \<and>
ko_at (ArchObj (ASIDPool empty)) ap s \<and>
ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and>
x64_asid_table (arch_state s) asid = None \<longrightarrow>
valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table := x64_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>)"
apply clarsimp
@ -561,7 +561,7 @@ lemma valid_asid_map_asid_upd_strg:
lemma valid_vspace_objs_asid_upd_strg:
"valid_vspace_objs s \<and>
ko_at (ArchObj (ASIDPool empty)) ap s \<and>
ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and>
x64_asid_table (arch_state s) asid = None \<longrightarrow>
valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table := x64_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>)"
apply clarsimp
@ -574,7 +574,7 @@ lemma valid_vspace_objs_asid_upd_strg:
lemma valid_global_objs_asid_upd_strg:
"valid_global_objs s \<and>
ko_at (ArchObj (arch_kernel_obj.ASIDPool empty)) ap s \<and>
ko_at (ArchObj (arch_kernel_obj.ASIDPool Map.empty)) ap s \<and>
x64_asid_table (arch_state s) asid = None \<longrightarrow>
valid_global_objs (s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table := x64_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>)"
by clarsimp
@ -602,7 +602,7 @@ lemma cap_insert_ap_invs:
(\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and
K (cap = ArchObjectCap (ASIDPoolCap ap asid)) and
(\<lambda>s. \<forall>irq \<in> cap_irqs cap. irq_issued irq s) and
ko_at (ArchObj (ASIDPool empty)) ap and
ko_at (ArchObj (ASIDPool Map.empty)) ap and
(\<lambda>s. ap \<notin> ran (x64_asid_table (arch_state s)) \<and>
x64_asid_table (arch_state s) (asid_high_bits_of asid) = None)\<rbrace>
cap_insert cap src dest

10
proof/invariant-abstract/X64/ArchFinalise_AI.thy
View File

@ -1447,7 +1447,7 @@ lemma vs_lookup1_arch [simp]:
lemma vs_lookup_empty_table:
"(rs \<rhd> q)
(s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (ASIDPool empty)),
(s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (ASIDPool Map.empty)),
arch_state := arch_state s\<lparr>x64_asid_table := x64_asid_table (arch_state s)(x \<mapsto> p)\<rparr>\<rparr>) \<Longrightarrow>
(rs \<rhd> q) s \<or> (rs = [VSRef (ucast x) None] \<and> q = p)"
apply (erule vs_lookupE)
@ -1480,7 +1480,7 @@ lemma vs_lookup_empty_table:
lemma vs_lookup_pages_empty_table:
"(rs \<unrhd> q)
(s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (ASIDPool empty)),
(s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (ASIDPool Map.empty)),
arch_state := arch_state s\<lparr>x64_asid_table := x64_asid_table (arch_state s)(x \<mapsto> p)\<rparr>\<rparr>) \<Longrightarrow>
(rs \<unrhd> q) s \<or> (rs = [VSRef (ucast x) None] \<and> q = p)"
apply (subst (asm) vs_lookup_pages_def)
@ -1513,7 +1513,7 @@ lemma vs_lookup_pages_empty_table:
lemma set_asid_pool_empty_table_objs:
"\<lbrace>valid_vspace_objs and asid_pool_at p\<rbrace>
set_asid_pool p empty
set_asid_pool p Map.empty
\<lbrace>\<lambda>rv s. valid_vspace_objs
(s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table :=
x64_asid_table (arch_state s)(asid_high_bits_of word2 \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
@ -1538,7 +1538,7 @@ lemma set_asid_pool_empty_table_objs:
lemma set_asid_pool_empty_table_lookup:
"\<lbrace>valid_vs_lookup and asid_pool_at p and
(\<lambda>s. \<exists>p'. caps_of_state s p' = Some (ArchObjectCap (ASIDPoolCap p base)))\<rbrace>
set_asid_pool p empty
set_asid_pool p Map.empty
\<lbrace>\<lambda>rv s. valid_vs_lookup
(s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table :=
x64_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
@ -1569,7 +1569,7 @@ lemma set_asid_pool_invs_table:
\<and> (\<exists>p'. caps_of_state s p' = Some (ArchObjectCap (ASIDPoolCap p base)))
\<and> (\<not> ([VSRef (ucast (asid_high_bits_of base)) None] \<rhd> p) s)
\<and> (\<forall>p'. \<not> ([VSRef (ucast (asid_high_bits_of base)) None] \<rhd> p') s)\<rbrace>
set_asid_pool p empty
set_asid_pool p Map.empty
\<lbrace>\<lambda>x s. invs (s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table :=
x64_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
apply (simp add: invs_def valid_state_def valid_pspace_def valid_arch_caps_def valid_asid_map_def

4
proof/invariant-abstract/X64/ArchKernelInit_AI.thy
View File

@ -52,14 +52,14 @@ lemma init_cdt [simp]:
by (simp add: state_defs)
lemma mdp_parent_empty [simp]:
"\<not>empty \<Turnstile> x \<rightarrow> y"
"\<not>Map.empty \<Turnstile> x \<rightarrow> y"
apply clarsimp
apply (drule tranclD)
apply (clarsimp simp: cdt_parent_of_def)
done
lemma descendants_empty [simp]:
"descendants_of x empty = {}"
"descendants_of x Map.empty = {}"
by (clarsimp simp: descendants_of_def)
lemma [simp]: "\<not>is_reply_cap Structures_A.NullCap"