riscv aspec/ainvs: resolve FIXMEs, reduce warnings
Mostly moved lemmas and definitions to more suitable locations. Removed unused lemmas and commented-out code. Resolved simple Isabelle warnings.
This commit is contained in:
Gerwin Klein
Rafal Kolanski
parent
f8dc660baf
commit
a1dca67543
|
|
@ -45,7 +45,6 @@ lemma shiftl_inj:
|
|||
context non_vspace_op
|
||||
begin
|
||||
|
||||
(* FIXME RISCV: arch split/move to arch (level) *)
|
||||
lemma valid_vso_at[wp]:"\<lbrace>valid_vso_at level p\<rbrace> f \<lbrace>\<lambda>_. valid_vso_at level p\<rbrace>"
|
||||
by (rule valid_vso_at_lift_aobj_at; wp vsobj_at; simp)
|
||||
|
||||
|
|
@ -53,8 +52,6 @@ end
|
|||
|
||||
context Arch begin global_naming RISCV64
|
||||
|
||||
|
||||
(* FIXME RISCV: move up *)
|
||||
(* Is there a lookup that leads to a page table at (level, p)? *)
|
||||
locale_abbrev ex_vs_lookup_table ::
|
||||
"vm_level \<Rightarrow> obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" ("\<exists>\<rhd> '(_, _')" [0,0] 1000) where
|
||||
|
|
@ -72,6 +69,17 @@ bundle unfold_objects_asm =
|
|||
kernel_object.split_asm[split]
|
||||
arch_kernel_obj.split_asm[split]
|
||||
|
||||
lemma invs_valid_asid_table [elim!]:
|
||||
"invs s \<Longrightarrow> valid_asid_table s"
|
||||
by (simp add: invs_def valid_state_def valid_arch_state_def)
|
||||
|
||||
lemma ptes_of_wellformed_pte:
|
||||
"\<lbrakk> ptes_of s p = Some pte; valid_objs s \<rbrakk> \<Longrightarrow> wellformed_pte pte"
|
||||
apply (clarsimp simp: ptes_of_def in_omonad)
|
||||
apply (erule (1) valid_objsE)
|
||||
apply (clarsimp simp: valid_obj_def)
|
||||
done
|
||||
|
||||
lemma vs_lookup_table_target:
|
||||
"\<lbrakk> vs_lookup_table level asid vref s = Some (level, p); level \<le> max_pt_level \<rbrakk> \<Longrightarrow>
|
||||
vs_lookup_target (level + 1) asid (vref_for_level vref level) s = Some (level + 1, p)"
|
||||
|
|
@ -189,7 +197,6 @@ lemma cap_to_pt_is_pt_cap:
|
|||
valid_cap_def obj_at_def is_ko_to_discs is_cap_table_def
|
||||
split: if_splits arch_cap.split cap.splits option.splits)
|
||||
|
||||
(* FIXME RISCV: probably need extra lemma for asid_pool_level *)
|
||||
lemma unique_vs_lookup_table:
|
||||
"\<lbrakk> vs_lookup_table level asid vref s = Some (level, p);
|
||||
vs_lookup_table level' asid' vref' s = Some (level', p');
|
||||
|
|
@ -490,10 +497,6 @@ lemma valid_objs_caps:
|
|||
apply (erule (1) caps_of_state_valid_cap)
|
||||
done
|
||||
|
||||
lemma invs_valid_asid_table [elim!]:
|
||||
"invs s \<Longrightarrow> valid_asid_table s"
|
||||
by (simp add: invs_def valid_state_def valid_arch_state_def)
|
||||
|
||||
(* invs could be relaxed; lemma so far only needed when invs is present *)
|
||||
lemma vs_lookup_table_unique_level:
|
||||
"\<lbrakk> vs_lookup_table level asid vref s = Some (level, p);
|
||||
|
|
@ -677,7 +680,6 @@ definition
|
|||
definition
|
||||
"invalid_pte_at p \<equiv> \<lambda>s. ptes_of s p = Some InvalidPTE"
|
||||
|
||||
(* FIXME RISCV: \<forall>level might not be quite right, we'll have to see *)
|
||||
definition
|
||||
"valid_slots \<equiv> \<lambda>(pte, p) s. wellformed_pte pte \<and>
|
||||
(\<forall>level. \<exists>\<rhd>(level, p && ~~ mask pt_bits) s \<longrightarrow> pte_at p s \<and> valid_pte level pte s)"
|
||||
|
|
@ -1013,11 +1015,10 @@ lemma unique_table_caps_ptD:
|
|||
\<Longrightarrow> p = p'"
|
||||
unfolding unique_table_caps_2_def by fastforce
|
||||
|
||||
lemma set_pt_table_caps:
|
||||
lemma set_pt_table_caps[wp]:
|
||||
"\<lbrace>valid_table_caps and (\<lambda>s. valid_caps (caps_of_state s) s) and
|
||||
(\<lambda>s. ((\<exists>slot. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow>
|
||||
pt = empty_pt) \<or>
|
||||
(\<forall>slot. \<exists>asid. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p (Some asid)))))\<rbrace>
|
||||
(\<lambda>s. (\<forall>slot asidopt. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p asidopt))
|
||||
\<longrightarrow> asidopt = None \<longrightarrow> pt = empty_pt)) \<rbrace>
|
||||
set_pt p pt
|
||||
\<lbrace>\<lambda>rv. valid_table_caps\<rbrace>"
|
||||
unfolding valid_table_caps_def set_pt_def
|
||||
|
|
@ -1028,20 +1029,6 @@ lemma set_pt_table_caps:
|
|||
apply (clarsimp simp: obj_at_def)
|
||||
apply (drule_tac x=r in spec, erule impE, fastforce)
|
||||
apply (clarsimp simp: opt_map_def fun_upd_apply split: option.splits)
|
||||
apply (erule impE, fastforce)
|
||||
apply clarsimp
|
||||
apply (erule_tac x=ref in allE, erule_tac x=slot in allE, fastforce)
|
||||
done
|
||||
|
||||
(* FIXME RISCV this is a much cleaner phrasing, should supersede the one above *)
|
||||
lemma set_pt_table_caps'[wp]:
|
||||
"\<lbrace>valid_table_caps and (\<lambda>s. valid_caps (caps_of_state s) s) and
|
||||
(\<lambda>s. (\<forall>slot asidopt. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p asidopt))
|
||||
\<longrightarrow> asidopt = None \<longrightarrow> pt = empty_pt)) \<rbrace>
|
||||
set_pt p pt
|
||||
\<lbrace>\<lambda>rv. valid_table_caps\<rbrace>"
|
||||
apply (wp set_pt_table_caps)
|
||||
apply fastforce
|
||||
done
|
||||
|
||||
lemma store_pte_valid_table_caps:
|
||||
|
|
@ -1313,7 +1300,7 @@ lemma pte_of_pt_slot_offset_upd_idem:
|
|||
\<Longrightarrow> pte_of (pt_slot_offset level pt_ptr vptr) (pts(obj_ref := pt'))
|
||||
= pte_of (pt_slot_offset level pt_ptr vptr) pts"
|
||||
unfolding pte_of_def
|
||||
by (rule obind_eqI; clarsimp simp: in_omonad pt_slot_offset_id)+
|
||||
by (rule obind_eqI; clarsimp simp: in_omonad)+
|
||||
|
||||
lemma pt_lookup_target_pt_eqI:
|
||||
"\<lbrakk> \<forall>level' pt_ptr'.
|
||||
|
|
@ -1724,7 +1711,6 @@ lemma vs_lookup_table_unreachable_upd_idem:
|
|||
apply (subst vs_lookup_table_upd_idem; fastforce)
|
||||
done
|
||||
|
||||
(* FIXME RISCV: simplified form of this may be preferable *)
|
||||
lemma vs_lookup_table_unreachable_upd_idem':
|
||||
"\<lbrakk> \<not>(\<exists>level. \<exists>\<rhd> (level, obj_ref) s);
|
||||
vref \<in> user_region; pspace_aligned s; valid_vspace_objs s; valid_asid_table s \<rbrakk>
|
||||
|
|
@ -1767,7 +1753,6 @@ lemma vs_lookup_target_unreachable_upd_idem:
|
|||
apply (clarsimp simp: fun_upd_def opt_map_def split: option.splits)
|
||||
done
|
||||
|
||||
(* FIXME RISCV: simplified form of this may be preferable *)
|
||||
lemma vs_lookup_target_unreachable_upd_idem':
|
||||
"\<lbrakk> \<not>(\<exists>level. \<exists>\<rhd> (level, obj_ref) s);
|
||||
vref \<in> user_region; pspace_aligned s; valid_vspace_objs s; valid_asid_table s \<rbrakk>
|
||||
|
|
@ -1935,7 +1920,7 @@ lemma set_asid_pool_vs_lookup_unmap':
|
|||
apply (rename_tac root pool_ptr)
|
||||
apply (subgoal_tac "vs_lookup_target asid_pool_level asid vref s = Some (asid_pool_level, root)"
|
||||
, fastforce)
|
||||
apply (erule vs_lookup_target_asid_pool_level_upd_helper; assumption)
|
||||
apply (erule vs_lookup_target_asid_pool_level_upd_helper; simp)
|
||||
apply clarsimp
|
||||
apply (subgoal_tac "vs_lookup_target level asid vref s = Some (level, target)", fastforce)
|
||||
apply (erule vs_lookup_target_None_upd_helper; simp)
|
||||
|
|
@ -1971,25 +1956,6 @@ lemma set_asid_pool_only_idle [wp]:
|
|||
"\<lbrace>only_idle\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. only_idle\<rbrace>"
|
||||
by (wp only_idle_lift set_asid_pool_typ_at)
|
||||
|
||||
(* FIXME RISCV move up *)
|
||||
lemma vspace_for_asid_SomeD:
|
||||
"vspace_for_asid asid s = Some pt_ptr
|
||||
\<Longrightarrow> \<exists>pool_ptr pool. asid_table s (asid_high_bits_of asid) = Some pool_ptr
|
||||
\<and> asid_pools_of s pool_ptr = Some pool
|
||||
\<and> pool (asid_low_bits_of asid) = Some pt_ptr
|
||||
\<and> asid > 0"
|
||||
unfolding vspace_for_asid_def
|
||||
by (clarsimp simp: pool_for_asid_def vspace_for_pool_def)
|
||||
|
||||
(* FIXME RISCV move up *)
|
||||
lemma vspace_for_asid_SomeI:
|
||||
"\<lbrakk> asid_table s (asid_high_bits_of asid) = Some pool_ptr;
|
||||
asid_pools_of s pool_ptr = Some pool;
|
||||
pool (asid_low_bits_of asid) = Some pt_ptr;
|
||||
asid > 0 \<rbrakk>
|
||||
\<Longrightarrow> vspace_for_asid asid s = Some pt_ptr"
|
||||
by (clarsimp simp: vspace_for_asid_def vspace_for_pool_def pool_for_asid_def obind_def)
|
||||
|
||||
lemma set_asid_pool_equal_mappings[wp]:
|
||||
"\<lbrace>equal_kernel_mappings and
|
||||
(\<lambda>s. \<forall>p pt. p \<in> ran ap \<longrightarrow> pts_of s p = Some pt \<longrightarrow> has_kernel_mappings pt s)\<rbrace>
|
||||
|
|
@ -2012,21 +1978,13 @@ lemma set_asid_pool_equal_mappings[wp]:
|
|||
apply (fastforce elim: vspace_for_asid_SomeI simp: opt_map_def)+
|
||||
done
|
||||
|
||||
(* FIXME RISCV RAF: this expansion is ugly but is in simp normal form *)
|
||||
|
||||
lemma pts_of_asid_pool_upd:
|
||||
"pts_of s p = None
|
||||
\<Longrightarrow> ((kheap s(p \<mapsto> ArchObj (ASIDPool ap)) |> aobj_of |> pt_of)) = pts_of s"
|
||||
by (rule ext, fastforce simp: opt_map_def split: option.splits)
|
||||
|
||||
lemma translate_address_asid_pool_upd:
|
||||
"pts_of s p = None
|
||||
\<Longrightarrow> translate_address pt_ptr vref
|
||||
(\<lambda>pa. pte_of pa (kheap s(p \<mapsto> ArchObj (ASIDPool ap)) |> aobj_of |> pt_of))
|
||||
= translate_address pt_ptr vref (ptes_of s)"
|
||||
by (subst pts_of_asid_pool_upd, simp+)
|
||||
by simp
|
||||
|
||||
(* FIXME RISCV move up and generalise to others, should be useful *)
|
||||
lemma ko_atasid_pool_pts_None:
|
||||
"ako_at (ASIDPool pool) p s \<Longrightarrow> pts_of s p = None"
|
||||
by (clarsimp simp: opt_map_def obj_at_def split: option.splits)
|
||||
|
|
@ -2213,9 +2171,6 @@ lemma set_pt_has_kernel_mappings:
|
|||
apply (wpsimp wp: set_pt_pts_of)+
|
||||
done
|
||||
|
||||
(* FIXME RISCV currently unused
|
||||
FIXME RISCV the not-global-pt requirement is a bit left field, we don't have a convenient
|
||||
way to go from vspace_for_asid to "not a global pt" *)
|
||||
lemma set_pt_equal_kernel_mappings:
|
||||
"\<lbrace>\<lambda>s. equal_kernel_mappings s
|
||||
\<and> ((\<exists>asid. vspace_for_asid asid s = Some p) \<longrightarrow> has_kernel_mappings pt s)
|
||||
|
|
@ -2250,19 +2205,19 @@ lemma store_pte_equal_kernel_mappings_no_kernel_slots:
|
|||
done
|
||||
|
||||
lemma store_pte_state_refs_of[wp]:
|
||||
"\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> store_pte ptr val \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>"
|
||||
apply (simp add: store_pte_def set_pt_def)
|
||||
"store_pte ptr val \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace>"
|
||||
unfolding store_pte_def set_pt_def
|
||||
apply (wp get_object_wp set_object_wp)
|
||||
apply (clarsimp elim!: rsubst[where P=P] intro!: ext)
|
||||
apply (clarsimp simp: state_refs_of_def obj_at_def)
|
||||
apply (clarsimp elim!: rsubst[where P=P])
|
||||
apply (rule ext, clarsimp simp: state_refs_of_def obj_at_def)
|
||||
done
|
||||
|
||||
lemma store_pte_state_hyp_refs_of[wp]:
|
||||
"\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> store_pte ptr val \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>"
|
||||
apply (simp add: store_pte_def set_pt_def)
|
||||
"store_pte ptr val \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>"
|
||||
unfolding store_pte_def set_pt_def
|
||||
apply (wp get_object_wp set_object_wp)
|
||||
apply (clarsimp elim!: rsubst[where P=P] intro!: ext)
|
||||
apply (clarsimp simp: state_hyp_refs_of_def obj_at_def)
|
||||
apply (clarsimp elim!: rsubst[where P=P])
|
||||
apply (rule ext, clarsimp simp: state_hyp_refs_of_def obj_at_def)
|
||||
done
|
||||
|
||||
lemma asid_pools_of_pt_None_upd_idem:
|
||||
|
|
@ -2925,6 +2880,23 @@ lemma store_pte_invs_unmap:
|
|||
by (wpsimp wp: store_pte_invs simp: wellformed_pte_def)
|
||||
|
||||
|
||||
lemma vs_lookup_table_vspace:
|
||||
"\<lbrakk> vs_lookup_table level asid vptr s = Some (level, pt_ptr);
|
||||
vspace_for_asid asid' s = Some pt_ptr; vptr \<in> user_region; invs s \<rbrakk>
|
||||
\<Longrightarrow> asid' = asid \<and> level = max_pt_level"
|
||||
apply (cases "level = asid_pool_level"; clarsimp)
|
||||
apply (clarsimp simp: vs_lookup_table_def)
|
||||
apply (drule pool_for_asid_validD; clarsimp)
|
||||
apply (drule vspace_for_asid_valid_pt; clarsimp)
|
||||
apply (fastforce simp: in_omonad)
|
||||
apply (drule vspace_for_asid_vs_lookup)
|
||||
apply (frule_tac level=level and level'=max_pt_level in unique_vs_lookup_table, assumption; clarsimp?)
|
||||
apply (fastforce intro: valid_objs_caps)
|
||||
apply (drule (1) no_loop_vs_lookup_table; clarsimp?)
|
||||
apply (rule vref_for_level_eq_max_mono[symmetric], simp)
|
||||
apply (fastforce intro: valid_objs_caps)
|
||||
done
|
||||
|
||||
lemma pspace_respects_device_region_dmo:
|
||||
assumes valid_f: "\<And>P. f \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace>"
|
||||
shows "do_machine_op f \<lbrace>pspace_respects_device_region\<rbrace>"
|
||||
|
|
|
|||
|
|
@ -990,46 +990,6 @@ lemma shiftr_irrelevant:
|
|||
apply simp
|
||||
done
|
||||
|
||||
(* FIXME RISCV: probably translate
|
||||
lemma lookup_pt_slot_cap_to:
|
||||
"\<lbrace>invs and \<exists>\<rhd>pm and K (is_aligned pm pml4_bits \<and> vptr < pptr_base \<and> canonical_address vptr)\<rbrace>
|
||||
lookup_pt_slot pm vptr
|
||||
\<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap
|
||||
\<and> rv && ~~ mask pt_bits \<in> obj_refs cap
|
||||
\<and> s \<turnstile> cap \<and> cap_asid cap \<noteq> None\<rbrace>, -"
|
||||
apply (rule hoare_gen_asmE)
|
||||
apply (wp lookup_pt_slot_wp)
|
||||
apply clarsimp
|
||||
apply (drule_tac x=ref in spec)
|
||||
apply (erule impE, fastforce, clarsimp)
|
||||
apply (thin_tac "(_ \<rhd> pm) _")
|
||||
apply (frule valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI]; clarsimp)
|
||||
apply (intro exI, rule conjI, assumption)
|
||||
apply (frule (1) caps_of_state_valid)
|
||||
apply (clarsimp simp: pte_at_def)
|
||||
apply (frule (2) valid_cap_to_pt_cap')
|
||||
by (auto simp: vs_cap_ref_def is_pt_cap_def
|
||||
split: cap.splits arch_cap.splits option.splits)
|
||||
*)
|
||||
|
||||
|
||||
(* FIXME RISCV: needed?
|
||||
lemma find_vspace_for_asid_ref_offset_voodoo:
|
||||
"\<lbrace>pspace_aligned and valid_vspace_objs and
|
||||
K (ref = [VSRef (ucast (asid_low_bits_of asid)) (Some AASIDPool),
|
||||
VSRef (ucast (asid_high_bits_of asid)) None])\<rbrace>
|
||||
find_vspace_for_asid asid
|
||||
\<lbrace>\<lambda>rv. (ref \<rhd> (rv + (get_pml4_index v << word_size_bits) && ~~ mask pml4_bits))\<rbrace>,-"
|
||||
apply (rule hoare_gen_asmE)
|
||||
apply (rule_tac Q'="\<lambda>rv s. is_aligned rv pml4_bits \<and> (ref \<rhd> rv) s"
|
||||
in hoare_post_imp_R)
|
||||
apply simp
|
||||
apply (rule hoare_pre, wp find_vspace_for_asid_lookup_ref)
|
||||
apply simp
|
||||
apply (simp add: pml4_shifting)
|
||||
done
|
||||
*)
|
||||
|
||||
|
||||
declare mask_shift [simp]
|
||||
declare word_less_sub_le [simp del]
|
||||
|
|
@ -1041,21 +1001,6 @@ lemma valid_mask_vm_rights[simp]:
|
|||
"mask_vm_rights V R \<in> valid_vm_rights"
|
||||
by (simp add: mask_vm_rights_def)
|
||||
|
||||
(* FIXME RISCV: looks duplicate-ish
|
||||
lemma vs_lookup_and_unique_refs:
|
||||
"\<lbrakk>(ref \<rhd> p) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref';
|
||||
p \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s)\<rbrakk>
|
||||
\<Longrightarrow> ref = ref'"
|
||||
apply (frule_tac ref=ref in valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI], assumption)
|
||||
apply clarsimp
|
||||
apply (frule_tac cap'=capa in unique_table_refsD)
|
||||
apply simp+
|
||||
apply (case_tac capa, simp_all)
|
||||
apply ((case_tac cap, simp_all)+)[6]
|
||||
apply (clarsimp simp add: table_cap_ref_def vs_cap_ref_def split: cap.splits arch_cap.splits option.splits)
|
||||
done
|
||||
*)
|
||||
|
||||
lemma cte_wp_at_page_cap_weaken:
|
||||
"cte_wp_at (diminished (ArchObjectCap (FrameCap word seta vmpage_size dev None))) slot s \<Longrightarrow>
|
||||
cte_wp_at (\<lambda>a. \<exists>p R sz dev m. a = ArchObjectCap (FrameCap p R sz dev m)) slot s"
|
||||
|
|
@ -1063,37 +1008,12 @@ lemma cte_wp_at_page_cap_weaken:
|
|||
apply (clarsimp simp: acap_rights_update_def split: cap.splits arch_cap.splits)
|
||||
done
|
||||
|
||||
(* FIXME RISCV: no longer the case for huge pages after kernel_base update
|
||||
lemma aligned_sum_less_kernel_base:
|
||||
"vmsz_aligned p sz \<Longrightarrow> (p + 2 ^ pageBitsForSize sz - 1 < kernel_base) = (p < kernel_base)"
|
||||
apply (rule iffI)
|
||||
apply (rule le_less_trans)
|
||||
apply (rule is_aligned_no_overflow)
|
||||
apply (simp add: vmsz_aligned_def)
|
||||
apply simp
|
||||
apply (simp add:field_simps[symmetric])
|
||||
apply (erule gap_between_aligned)
|
||||
apply (simp add: vmsz_aligned_def)+
|
||||
apply (case_tac sz; simp add: kernel_base_def bit_simps is_aligned_def)
|
||||
done
|
||||
*)
|
||||
|
||||
lemma le_user_vtop_less_pptr_base[simp]:
|
||||
"x \<le> user_vtop \<Longrightarrow> x < pptr_base"
|
||||
using dual_order.strict_trans2 by blast
|
||||
|
||||
lemmas le_user_vtop_canonical_address = below_user_vtop_canonical[simp]
|
||||
|
||||
(* FIXME RISCV: move to ArchInvariants *)
|
||||
lemma pte_at_eq:
|
||||
"pte_at p s = (ptes_of s p \<noteq> None)"
|
||||
by (auto simp: obj_at_def pte_at_def in_omonad pte_of_def)
|
||||
|
||||
(* FIXME RISCV: move to ArchInvariants *)
|
||||
lemma user_vtop_canonical_user:
|
||||
"vref < user_vtop \<Longrightarrow> vref \<le> canonical_user"
|
||||
using user_vtop_canonical_user by simp
|
||||
|
||||
lemma ptrFromPAddr_addr_from_ppn:
|
||||
"is_aligned pt_ptr table_size \<Longrightarrow>
|
||||
ptrFromPAddr (addr_from_ppn (ucast (addrFromPPtr pt_ptr >> pageBits))) = pt_ptr"
|
||||
|
|
@ -1102,23 +1022,6 @@ lemma ptrFromPAddr_addr_from_ppn:
|
|||
apply (simp add: aligned_shiftr_mask_shiftl mask_len_id[where 'a=machine_word_len, simplified])
|
||||
done
|
||||
|
||||
(* FIXME RISCV: move to ArchInvariants *)
|
||||
lemma pt_bits_left_0[simp]:
|
||||
"(pt_bits_left level = pageBits) = (level = 0)"
|
||||
by (auto simp: pt_bits_left_def bit_simps)
|
||||
|
||||
(* FIXME RISCV: move to ArchInvariants *)
|
||||
lemma pt_lookup_slot_vs_lookup_slotI:
|
||||
"\<lbrakk> vspace_for_asid asid s = Some pt_ptr;
|
||||
pt_lookup_slot pt_ptr vref (ptes_of s) = Some (level, slot) \<rbrakk>
|
||||
\<Longrightarrow> vs_lookup_slot level asid vref s = Some (level, slot) \<and> level \<le> max_pt_level"
|
||||
unfolding pt_lookup_slot_def pt_lookup_slot_from_level_def vs_lookup_slot_def
|
||||
apply (clarsimp simp: in_omonad)
|
||||
apply (drule (1) pt_lookup_vs_lookupI, simp)
|
||||
apply (drule vs_lookup_level)
|
||||
apply (fastforce dest: pt_walk_max_level)
|
||||
done
|
||||
|
||||
lemma is_aligned_pageBitsForSize_table_size:
|
||||
"is_aligned p (pageBitsForSize vmpage_size) \<Longrightarrow> is_aligned p table_size"
|
||||
apply (erule is_aligned_weaken)
|
||||
|
|
@ -1144,15 +1047,6 @@ lemma vs_lookup_slot_pte_at:
|
|||
apply (rule is_aligned_add; simp add: is_aligned_shift)
|
||||
done
|
||||
|
||||
(* FIXME RISCV: move up *)
|
||||
lemma size_level1[simp]:
|
||||
"(size level = Suc 0) = (level = (1 :: vm_level))"
|
||||
proof
|
||||
assume "size level = Suc 0"
|
||||
hence "size level = size (1::vm_level)" by simp
|
||||
thus "level = 1" by (subst (asm) bit0.size_inj)
|
||||
qed auto
|
||||
|
||||
lemma vmpage_size_of_level_pt_bits_left:
|
||||
"\<lbrakk> pt_bits_left level = pageBitsForSize vmpage_size; level \<le> max_pt_level \<rbrakk> \<Longrightarrow>
|
||||
vmpage_size_of_level level = vmpage_size"
|
||||
|
|
@ -1282,11 +1176,6 @@ lemma decode_frame_invocation_wf[wp]:
|
|||
split: option.split)
|
||||
done
|
||||
|
||||
(* FIXME RISCV: move to ArchInvariants *)
|
||||
lemma minus_one_max_pt_level[simp]:
|
||||
"(level - 1 = max_pt_level) = (level = asid_pool_level)"
|
||||
by (simp add: level_defs bit0.minus_1_eq)
|
||||
|
||||
lemma decode_pt_inv_map_wf[wp]:
|
||||
"arch_cap = PageTableCap pt_ptr pt_map_data \<Longrightarrow>
|
||||
\<lbrace>invs and valid_cap (ArchObjectCap arch_cap) and
|
||||
|
|
|
|||
|
|
@ -69,32 +69,32 @@ definition
|
|||
replaceable_final_arch_cap :: "'z::state_ext state \<Rightarrow> cslot_ptr \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool"
|
||||
where
|
||||
"replaceable_final_arch_cap s sl newcap \<equiv> \<lambda>cap.
|
||||
(* Don't leave dangling vspace references. That is, if cap points to a mapped vspace object, *)
|
||||
\<comment> \<open>Don't leave dangling vspace references. That is, if cap points to a mapped vspace object,\<close>
|
||||
(\<forall>ref. vs_cap_ref cap = Some ref
|
||||
(* then either newcap maintains the same vs_refs *)
|
||||
\<comment> \<open> then either newcap maintains the same vs_refs \<close>
|
||||
\<longrightarrow> (vs_cap_ref newcap = Some ref \<and> obj_refs newcap = obj_refs cap)
|
||||
(* or the object pointed to by cap is not currently mapped. *)
|
||||
\<comment> \<open> or the object pointed to by cap is not currently mapped. \<close>
|
||||
\<or> (\<forall>oref \<in> obj_refs cap. \<not> reachable_target ref oref s))
|
||||
(* Don't introduce duplicate caps to vspace table objects with different vs_refs. *)
|
||||
\<comment> \<open> Don't introduce duplicate caps to vspace table objects with different vs_refs. \<close>
|
||||
\<and> no_cap_to_obj_with_diff_ref newcap {sl} s
|
||||
(* Don't introduce non-empty unmapped table objects. *)
|
||||
\<comment> \<open> Don't introduce non-empty unmapped table objects. \<close>
|
||||
\<and> (is_pt_cap newcap
|
||||
\<longrightarrow> cap_asid newcap = None
|
||||
\<longrightarrow> (\<forall>r \<in> obj_refs newcap. pts_of s r = Some empty_pt))
|
||||
(* If newcap is vspace table cap such that either:
|
||||
\<comment> \<open> If newcap is vspace table cap such that either:
|
||||
- newcap and cap have different types or different obj_refs, or
|
||||
- newcap is unmapped while cap is mapped, *)
|
||||
- newcap is unmapped while cap is mapped, \<close>
|
||||
\<and> (is_pt_cap newcap
|
||||
\<longrightarrow> (is_pt_cap cap
|
||||
\<longrightarrow> (cap_asid newcap = None \<longrightarrow> cap_asid cap = None)
|
||||
\<longrightarrow> obj_refs cap \<noteq> obj_refs newcap)
|
||||
(* then, aside from sl, there is no other slot with a cap that
|
||||
\<comment> \<open>then, aside from sl, there is no other slot with a cap that
|
||||
- has the same obj_refs and type as newcap, and
|
||||
- is unmapped if newcap is mapped. *)
|
||||
- is unmapped if newcap is mapped. \<close>
|
||||
\<longrightarrow> (\<forall>sl'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs newcap
|
||||
\<and> is_pt_cap cap'
|
||||
\<and> (cap_asid newcap = None \<or> cap_asid cap' = None)) sl' s \<longrightarrow> sl' = sl))
|
||||
(* Don't replace with an ASID pool. *)
|
||||
\<comment> \<open>Don't replace with an ASID pool. \<close>
|
||||
\<and> \<not>is_ap_cap newcap"
|
||||
|
||||
definition
|
||||
|
|
@ -116,7 +116,8 @@ lemma unique_table_refsD:
|
|||
lemma table_cap_ref_vs_cap_ref_Some:
|
||||
"table_cap_ref x = Some y \<Longrightarrow> vs_cap_ref x = Some y"
|
||||
by (clarsimp simp: table_cap_ref_def vs_cap_ref_def table_cap_ref_arch_def vs_cap_ref_arch_def
|
||||
split: cap.splits arch_cap.splits)
|
||||
simp del: arch_cap_fun_lift_Some
|
||||
split: cap.splits arch_cap.splits)
|
||||
|
||||
lemma set_cap_aobjs_of[wp]:
|
||||
"set_cap cap ptr \<lbrace>\<lambda>s. P (aobjs_of s)\<rbrace>"
|
||||
|
|
@ -129,30 +130,6 @@ lemma set_cap_pool_for_asid[wp]:
|
|||
"set_cap cap ptr \<lbrace>\<lambda>s. P (pool_for_asid asid s)\<rbrace>"
|
||||
unfolding pool_for_asid_def by wpsimp
|
||||
|
||||
(* FIXME RISCV: move to ArchInvariants *)
|
||||
lemmas vs_lookup_slot_vref_for_level_eq[simp] = vs_lookup_slot_vref_for_level[OF order_refl]
|
||||
|
||||
(* FIXME RISCV: move to ArchInvariants *)
|
||||
lemmas vs_lookup_target_vref_for_level_eq[simp] = vs_lookup_target_vref_for_level[OF order_refl]
|
||||
|
||||
(* FIXME RISCV: move to ArchInvariants *)
|
||||
lemma pool_for_asid_asid_for_level[simp]:
|
||||
"pool_for_asid (asid_for_level asid level) = pool_for_asid asid"
|
||||
by (clarsimp simp: pool_for_asid_def asid_for_level_def asid_high_bits_of_def mask_shift)
|
||||
|
||||
(* FIXME RISCV: move to ArchInvariants *)
|
||||
lemma vs_lookup_asid_for_level[simp]:
|
||||
"vs_lookup_table level (asid_for_level asid level) vref = vs_lookup_table level asid vref"
|
||||
apply (simp add: vs_lookup_table_def)
|
||||
apply (rule ext, rule obind_eqI, rule refl)
|
||||
apply (clarsimp simp: asid_for_level_def)
|
||||
done
|
||||
|
||||
(* FIXME RISCV: move to ArchInvariants *)
|
||||
lemma vs_lookup_slot_asid_for_level[simp]:
|
||||
"vs_lookup_slot level (asid_for_level asid level) vref = vs_lookup_slot level asid vref"
|
||||
by (simp add: vs_lookup_slot_def)
|
||||
|
||||
lemma set_cap_valid_vs_lookup:
|
||||
"\<lbrace>\<lambda>s. valid_vs_lookup s
|
||||
\<and> (\<forall>vref cap'. caps_of_state s ptr = Some cap'
|
||||
|
|
@ -412,11 +389,9 @@ lemma set_cap_hyp_refs_of [wp]:
|
|||
\<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>"
|
||||
apply (simp add: set_cap_def set_object_def split_def)
|
||||
apply (wp get_object_wp | wpc)+
|
||||
apply (auto elim!: rsubst[where P=P]
|
||||
simp: state_hyp_refs_of_def obj_at_def
|
||||
intro!: ext
|
||||
split: if_split_asm)
|
||||
done
|
||||
by (force elim!: rsubst[where P=P]
|
||||
simp: state_hyp_refs_of_def obj_at_def
|
||||
split: if_split_asm)
|
||||
|
||||
lemma state_hyp_refs_of_revokable[simp]:
|
||||
"state_hyp_refs_of (s \<lparr> is_original_cap := m \<rparr>) = state_hyp_refs_of s"
|
||||
|
|
|
|||
|
|
@ -210,27 +210,6 @@ lemma is_derived_is_cap:
|
|||
by (clarsimp simp: cap_master_cap_def is_cap_simps
|
||||
split: cap.splits arch_cap.splits)+
|
||||
|
||||
(* FIXME RISCV: move up *)
|
||||
lemma vs_lookup_table_eq_lift:
|
||||
"\<lbrakk> pts_of s' = pts_of s;
|
||||
asid_pools_of s' = asid_pools_of s;
|
||||
pool_for_asid asid s' = pool_for_asid asid s \<rbrakk>
|
||||
\<Longrightarrow> vs_lookup_table level asid vref s' = vs_lookup_table level asid vref s"
|
||||
unfolding vs_lookup_table_def
|
||||
by (auto simp: obind_def split: option.splits)
|
||||
|
||||
(* FIXME RISCV: move up *)
|
||||
lemma aobjs_of_non_aobj_upd:
|
||||
"\<lbrakk> kheap s p = Some ko; \<not> is_ArchObj ko; \<not> is_ArchObj ko' \<rbrakk>
|
||||
\<Longrightarrow> kheap s(p \<mapsto> ko') |> aobj_of = aobjs_of s"
|
||||
by (rule ext)
|
||||
(auto simp: opt_map_def is_ArchObj_def aobj_of_def split: kernel_object.splits if_split_asm)
|
||||
|
||||
(* FIXME RISCV: move up *)
|
||||
lemma pool_for_asid_kheap_upd[simp]:
|
||||
"pool_for_asid asid (s\<lparr>kheap := kheap'\<rparr>) = pool_for_asid asid s"
|
||||
by (simp add: pool_for_asid_def)
|
||||
|
||||
lemma vs_lookup_pages_non_aobj_upd:
|
||||
"\<lbrakk> kheap s p = Some ko; \<not> is_ArchObj ko; \<not> is_ArchObj ko' \<rbrakk>
|
||||
\<Longrightarrow> vs_lookup_pages (s\<lparr>kheap := kheap s(p \<mapsto> ko')\<rparr>) = vs_lookup_pages s"
|
||||
|
|
@ -246,7 +225,6 @@ lemma vs_lookup_pages_non_aobj_upd:
|
|||
apply (rule obind_eqI; clarsimp)
|
||||
done
|
||||
|
||||
(* FIXME RISCV: which do we want, the lookup_target or lookup_pages version? *)
|
||||
lemma vs_lookup_target_non_aobj_upd:
|
||||
"\<lbrakk> kheap s p = Some ko; \<not> is_ArchObj ko; \<not> is_ArchObj ko' \<rbrakk>
|
||||
\<Longrightarrow> vs_lookup_target level asid vref (s\<lparr>kheap := kheap s(p \<mapsto> ko')\<rparr>)
|
||||
|
|
|
|||
|
|
@ -819,41 +819,6 @@ lemma arch_finalise_cap_replaceable:
|
|||
apply (rule conjI; clarsimp)
|
||||
apply (clarsimp simp: valid_cap_def wellformed_mapdata_def cap_aligned_def)
|
||||
done
|
||||
(*
|
||||
apply (fastforce simp: valid_cap_def wellformed_mapdata_def cap_aligned_def)
|
||||
done *)
|
||||
(*
|
||||
apply (rule conjI, clarsimp)
|
||||
apply (clarsimp simp: valid_cap_def)
|
||||
apply (rule conjI; clarsimp)
|
||||
apply (rule conjI; clarsimp)
|
||||
apply (rule conjI; clarsimp)
|
||||
apply (clarsimp simp: valid_cap_def wellformed_mapdata_def cap_aligned_def)
|
||||
done
|
||||
*)
|
||||
(* FIXME RISCV
|
||||
apply (rule hoare_pre)
|
||||
apply (simp add: simps split: option.splits vmpage_size.splits)
|
||||
apply (wp wps
|
||||
| strengthen strg
|
||||
| simp add: simps reachable_frame_cap_def live_def
|
||||
| wpc)+
|
||||
(* unmap_page case is a bit unpleasant *)
|
||||
apply (strengthen cases_conj_strg[where P="\<not> is_final_cap' cap s" for cap s, simplified])
|
||||
apply (rule hoare_post_imp, clarsimp split: vmpage_size.split, assumption)
|
||||
apply (simp add: vspace_bits_defs)
|
||||
apply (wp hoare_vcg_disj_lift hoare_vcg_all_lift hoare_vcg_const_imp_lift
|
||||
unmap_page_tcb_cap_valid unmap_page_page_unmapped
|
||||
unmap_page_section_unmapped)[1]
|
||||
apply (wp wps
|
||||
| strengthen strg imp_and_strg tcb_cap_valid_imp_NullCap
|
||||
| simp add: simps is_master_reply_cap_def reachable_pg_cap_def
|
||||
| wpc)+
|
||||
apply (intro conjI; clarsimp split: cap.splits arch_cap.splits vmpage_size.splits)
|
||||
by (auto simp: valid_cap_def obj_at_def simps is_master_reply_cap_def
|
||||
a_type_def data_at_def vspace_bits_defs X
|
||||
elim!: tcb_cap_valid_imp_NullCap[rule_format, rotated]
|
||||
split: cap.splits arch_cap.splits vmpage_size.splits) *)
|
||||
|
||||
|
||||
global_naming Arch
|
||||
|
|
@ -1070,25 +1035,8 @@ crunch pred_tcb_at[wp]:
|
|||
crunch pred_tcb_at[wp_unsafe]: arch_finalise_cap "pred_tcb_at proj P t"
|
||||
(simp: crunch_simps wp: crunch_wps)
|
||||
|
||||
lemma store_pte_unmap_empty: (* FIXME RISCV: check usage *)
|
||||
"\<lbrace>\<lambda>s. obj_at (empty_table S) word s\<rbrace>
|
||||
store_pte xa InvalidPTE
|
||||
\<lbrace>\<lambda>rv s. obj_at (empty_table S) word s\<rbrace>"
|
||||
apply (wp get_object_wp | simp add: store_pte_def set_pt_def set_object_def)+
|
||||
apply (clarsimp simp: obj_at_def empty_table_def)
|
||||
done
|
||||
|
||||
lemma unmap_page_table_empty: (* FIXME RISCV: check usage *)
|
||||
"\<lbrace>\<lambda>s. obj_at (empty_table S) word s\<rbrace>
|
||||
unmap_page_table aa b word
|
||||
\<lbrace>\<lambda>rv s. obj_at (empty_table S) word s\<rbrace>"
|
||||
apply (simp add: unmap_page_table_def)
|
||||
apply (wp store_pte_unmap_empty | simp | wpc)+
|
||||
done
|
||||
|
||||
definition
|
||||
replaceable_or_arch_update
|
||||
where
|
||||
replaceable_or_arch_update :: "'z::state_ext state \<Rightarrow> cslot_ptr \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool" where
|
||||
"replaceable_or_arch_update \<equiv> \<lambda>s slot cap cap'.
|
||||
if is_frame_cap cap
|
||||
then is_arch_update cap cap' \<and>
|
||||
|
|
@ -1187,14 +1135,6 @@ lemma invs_valid_arch_capsI:
|
|||
|
||||
context Arch begin global_naming RISCV64 (*FIXME: arch_split*)
|
||||
|
||||
lemma arch_finalise_pt_empty:
|
||||
"\<lbrace>(\<lambda>s. obj_at (empty_table {}) ptr s) and valid_cap (ArchObjectCap acap) and
|
||||
K (is_pt_cap (ArchObjectCap acap) \<and> aobj_ref acap = Some ptr)\<rbrace>
|
||||
arch_finalise_cap acap final
|
||||
\<lbrace>\<lambda>rv s. obj_at (empty_table {}) ptr s\<rbrace>"
|
||||
by (rule hoare_gen_asm)
|
||||
(wpsimp simp: is_cap_simps arch_finalise_cap_def wp: unmap_page_table_empty)
|
||||
|
||||
lemma do_machine_op_reachable_pg_cap[wp]:
|
||||
"\<lbrace>\<lambda>s. P (reachable_frame_cap cap s)\<rbrace>
|
||||
do_machine_op mo
|
||||
|
|
|
|||
|
|
@ -64,6 +64,10 @@ lemma arch_cap_fun_lift_expand[simp]:
|
|||
| _ \<Rightarrow> F)"
|
||||
unfolding arch_cap_fun_lift_def by fastforce
|
||||
|
||||
lemma arch_cap_fun_lift_Some[simp]:
|
||||
"(arch_cap_fun_lift f None cap = Some x) = (\<exists>acap. cap = ArchObjectCap acap \<and> f acap = Some x)"
|
||||
by (cases cap; simp)
|
||||
|
||||
lemma arch_obj_fun_lift_expand[simp]:
|
||||
"arch_obj_fun_lift (\<lambda>ako. case ako of
|
||||
ASIDPool pool \<Rightarrow> P_ASIDPool pool
|
||||
|
|
@ -313,10 +317,6 @@ definition wellformed_vspace_obj :: "arch_kernel_obj \<Rightarrow> bool" where
|
|||
|
||||
lemmas wellformed_aobj_simps[simp] = wellformed_aobj_def[split_simps arch_kernel_obj.split]
|
||||
|
||||
(* FIXME RISCV: move to spec? *)
|
||||
locale_abbrev global_pt :: "'z state \<Rightarrow> obj_ref" where
|
||||
"global_pt s \<equiv> riscv_global_pt (arch_state s)"
|
||||
|
||||
definition has_kernel_mappings :: "pt \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" where
|
||||
"has_kernel_mappings pt \<equiv> \<lambda>s.
|
||||
\<forall>pt'. pts_of s (global_pt s) = Some pt' \<longrightarrow>
|
||||
|
|
@ -841,6 +841,18 @@ lemma max_pt_level_less_Suc[iff]:
|
|||
apply (simp add: bit0.no_overflow_eq_max_bound max_pt_level_def flip: asid_pool_level_minus)
|
||||
by (metis asid_pool_level_max asid_pool_level_neq max_pt_level_def antisym_conv2)
|
||||
|
||||
lemma size_level1[simp]:
|
||||
"(size level = Suc 0) = (level = (1 :: vm_level))"
|
||||
proof
|
||||
assume "size level = Suc 0"
|
||||
hence "size level = size (1::vm_level)" by simp
|
||||
thus "level = 1" by (subst (asm) bit0.size_inj)
|
||||
qed auto
|
||||
|
||||
lemma minus_one_max_pt_level[simp]:
|
||||
"(level - 1 = max_pt_level) = (level = asid_pool_level)"
|
||||
by (simp add: level_defs bit0.minus_1_eq)
|
||||
|
||||
lemma max_inc_pt_level[simp]:
|
||||
"level \<le> max_pt_level \<Longrightarrow> max (level + 1) level = level + 1"
|
||||
by (simp add: dual_order.strict_implies_order max.commute max_def)
|
||||
|
|
@ -1275,7 +1287,7 @@ lemma user_vtop_pptr_base[intro!,simp]:
|
|||
"user_vtop < pptr_base"
|
||||
by (simp add: user_vtop_def pptrUserTop_def pptr_base_def pptrBase_def canonical_bit_def mask_def)
|
||||
|
||||
lemma user_vtop_canonical_user:
|
||||
lemma user_vtop_leq_canonical_user:
|
||||
"user_vtop \<le> canonical_user"
|
||||
by (simp add: user_vtop_def pptrUserTop_def canonical_user_def canonical_bit_def mask_def)
|
||||
|
||||
|
|
@ -1297,7 +1309,11 @@ lemma canonical_user_canonical:
|
|||
|
||||
lemma below_user_vtop_canonical:
|
||||
"p \<le> user_vtop \<Longrightarrow> canonical_address p"
|
||||
by (drule order_trans, rule user_vtop_canonical_user) (erule canonical_user_canonical)
|
||||
by (drule order_trans, rule user_vtop_leq_canonical_user) (erule canonical_user_canonical)
|
||||
|
||||
lemma user_vtop_canonical_user:
|
||||
"vref < user_vtop \<Longrightarrow> vref \<le> canonical_user"
|
||||
using user_vtop_leq_canonical_user by simp
|
||||
|
||||
lemmas window_defs =
|
||||
kernel_window_def not_kernel_window_def kernel_elf_window_def kernel_regions_def
|
||||
|
|
@ -1418,6 +1434,10 @@ lemma vs_lookup_min_level:
|
|||
"vs_lookup_table bot_level asid vref s = Some (level, p) \<Longrightarrow> bot_level \<le> level"
|
||||
by (auto simp: vs_lookup_table_def in_omonad not_le split: if_split_asm dest!: pt_walk_min_level)
|
||||
|
||||
lemma pt_bits_left_0[simp]:
|
||||
"(pt_bits_left level = pageBits) = (level = 0)"
|
||||
by (auto simp: pt_bits_left_def bit_simps)
|
||||
|
||||
lemma pt_bits_left_mono:
|
||||
"level \<le> level' \<Longrightarrow> pt_bits_left level \<le> pt_bits_left level'"
|
||||
by (simp add: pt_bits_left_def)
|
||||
|
|
@ -1510,6 +1530,10 @@ lemma vs_lookup_vref_for_level:
|
|||
vs_lookup_table bot_level asid (vref_for_level vref level) = vs_lookup_table bot_level asid vref"
|
||||
by (force simp: vs_lookup_table_def pt_walk_vref_for_level obind_def split: option.splits)
|
||||
|
||||
lemma riscv_global_pts_global_ref:
|
||||
"pt \<in> riscv_global_pts (arch_state s) level \<Longrightarrow> pt \<in> global_refs s"
|
||||
by (auto simp: global_refs_def)
|
||||
|
||||
lemma valid_global_vspace_mappings_kwD:
|
||||
"\<lbrakk> valid_global_vspace_mappings s; vref \<in> kernel_window s \<rbrakk>
|
||||
\<Longrightarrow> translate_address (global_pt s) vref (ptes_of s) = Some (addrFromPPtr vref)"
|
||||
|
|
@ -1519,6 +1543,24 @@ lemma valid_global_vspace_mappings_aligned[simp]:
|
|||
"valid_global_vspace_mappings s \<Longrightarrow> is_aligned (global_pt s) pt_bits"
|
||||
by (simp add: valid_global_vspace_mappings_def Let_def)
|
||||
|
||||
|
||||
lemma vspace_for_asid_SomeD:
|
||||
"vspace_for_asid asid s = Some pt_ptr
|
||||
\<Longrightarrow> \<exists>pool_ptr pool. asid_table s (asid_high_bits_of asid) = Some pool_ptr
|
||||
\<and> asid_pools_of s pool_ptr = Some pool
|
||||
\<and> pool (asid_low_bits_of asid) = Some pt_ptr
|
||||
\<and> asid > 0"
|
||||
unfolding vspace_for_asid_def
|
||||
by (clarsimp simp: pool_for_asid_def vspace_for_pool_def)
|
||||
|
||||
lemma vspace_for_asid_SomeI:
|
||||
"\<lbrakk> asid_table s (asid_high_bits_of asid) = Some pool_ptr;
|
||||
asid_pools_of s pool_ptr = Some pool;
|
||||
pool (asid_low_bits_of asid) = Some pt_ptr;
|
||||
asid > 0 \<rbrakk>
|
||||
\<Longrightarrow> vspace_for_asid asid s = Some pt_ptr"
|
||||
by (clarsimp simp: vspace_for_asid_def vspace_for_pool_def pool_for_asid_def obind_def)
|
||||
|
||||
lemmas ptes_of_def = pte_of_def
|
||||
|
||||
lemma ptes_of_pts_of:
|
||||
|
|
@ -1666,6 +1708,17 @@ lemma pt_lookup_vs_lookupI:
|
|||
vs_lookup_table bot_level asid vref s = Some (level, p)"
|
||||
by (frule vspace_for_asid_0) (auto simp: pt_lookup_vs_lookup_eq obind_def)
|
||||
|
||||
lemma pt_lookup_slot_vs_lookup_slotI:
|
||||
"\<lbrakk> vspace_for_asid asid s = Some pt_ptr;
|
||||
pt_lookup_slot pt_ptr vref (ptes_of s) = Some (level, slot) \<rbrakk>
|
||||
\<Longrightarrow> vs_lookup_slot level asid vref s = Some (level, slot) \<and> level \<le> max_pt_level"
|
||||
unfolding pt_lookup_slot_def pt_lookup_slot_from_level_def vs_lookup_slot_def
|
||||
apply (clarsimp simp: in_omonad)
|
||||
apply (drule (1) pt_lookup_vs_lookupI, simp)
|
||||
apply (drule vs_lookup_level)
|
||||
apply (fastforce dest: pt_walk_max_level)
|
||||
done
|
||||
|
||||
lemma vspace_for_asid_vs_lookup:
|
||||
"vspace_for_asid asid s = Some pt \<Longrightarrow>
|
||||
vs_lookup_table max_pt_level asid 0 s = Some (max_pt_level, pt)"
|
||||
|
|
@ -1680,6 +1733,10 @@ proof -
|
|||
with p show ?thesis by (auto dest!: ptes_of_pts_of)
|
||||
qed
|
||||
|
||||
lemma pte_at_eq:
|
||||
"pte_at p s = (ptes_of s p \<noteq> None)"
|
||||
by (auto simp: obj_at_def pte_at_def in_omonad pte_of_def)
|
||||
|
||||
lemma valid_vspace_objsI [intro?]:
|
||||
"(\<And>p ao asid vref level.
|
||||
\<lbrakk> vs_lookup_table level asid (vref_for_level vref (level+1)) s = Some (level, p);
|
||||
|
|
@ -2467,6 +2524,90 @@ lemma vs_lookup_slot_table:
|
|||
pt_slot = pt_slot_offset level pt_ptr vref)"
|
||||
by (clarsimp simp: vs_lookup_slot_def in_omonad) fastforce
|
||||
|
||||
lemmas vs_lookup_slot_vref_for_level_eq[simp] = vs_lookup_slot_vref_for_level[OF order_refl]
|
||||
lemmas vs_lookup_target_vref_for_level_eq[simp] = vs_lookup_target_vref_for_level[OF order_refl]
|
||||
|
||||
lemma pool_for_asid_asid_for_level[simp]:
|
||||
"pool_for_asid (asid_for_level asid level) = pool_for_asid asid"
|
||||
by (clarsimp simp: pool_for_asid_def asid_for_level_def asid_high_bits_of_def mask_shift)
|
||||
|
||||
lemma vs_lookup_asid_for_level[simp]:
|
||||
"vs_lookup_table level (asid_for_level asid level) vref = vs_lookup_table level asid vref"
|
||||
apply (simp add: vs_lookup_table_def)
|
||||
apply (rule ext, rule obind_eqI, rule refl)
|
||||
apply (clarsimp simp: asid_for_level_def)
|
||||
done
|
||||
|
||||
lemma vs_lookup_slot_asid_for_level[simp]:
|
||||
"vs_lookup_slot level (asid_for_level asid level) vref = vs_lookup_slot level asid vref"
|
||||
by (simp add: vs_lookup_slot_def)
|
||||
|
||||
lemma vs_lookup_table_eq_lift:
|
||||
"\<lbrakk> pts_of s' = pts_of s;
|
||||
asid_pools_of s' = asid_pools_of s;
|
||||
pool_for_asid asid s' = pool_for_asid asid s \<rbrakk>
|
||||
\<Longrightarrow> vs_lookup_table level asid vref s' = vs_lookup_table level asid vref s"
|
||||
unfolding vs_lookup_table_def
|
||||
by (auto simp: obind_def split: option.splits)
|
||||
|
||||
lemma aobjs_of_non_aobj_upd:
|
||||
"\<lbrakk> kheap s p = Some ko; \<not> is_ArchObj ko; \<not> is_ArchObj ko' \<rbrakk>
|
||||
\<Longrightarrow> kheap s(p \<mapsto> ko') |> aobj_of = aobjs_of s"
|
||||
by (rule ext)
|
||||
(auto simp: opt_map_def is_ArchObj_def aobj_of_def split: kernel_object.splits if_split_asm)
|
||||
|
||||
lemma pool_for_asid_kheap_upd[simp]:
|
||||
"pool_for_asid asid (s\<lparr>kheap := kheap'\<rparr>) = pool_for_asid asid s"
|
||||
by (simp add: pool_for_asid_def)
|
||||
|
||||
lemma table_index_max_level_slots:
|
||||
"\<lbrakk> vref \<in> user_region; is_aligned pt pt_bits \<rbrakk>
|
||||
\<Longrightarrow> table_index (pt_slot_offset max_pt_level pt vref) \<notin> kernel_mapping_slots"
|
||||
apply (simp add: kernel_mapping_slots_def table_index_offset_max_pt_level not_le user_region_def)
|
||||
apply (simp add: pt_bits_left_def level_defs bit_simps canonical_user_def)
|
||||
apply word_bitwise
|
||||
apply (simp add: word_size canonical_bit_def word_bits_def)
|
||||
done
|
||||
|
||||
lemma valid_vspace_objs_strong_slotD:
|
||||
"\<lbrakk> vs_lookup_slot level asid vref s = Some (level, slot); vref \<in> user_region;
|
||||
level \<le> max_pt_level; valid_vspace_objs s; valid_asid_table s; pspace_aligned s\<rbrakk>
|
||||
\<Longrightarrow> \<exists>pte. ptes_of s slot = Some pte \<and> valid_pte level pte s"
|
||||
apply (clarsimp simp: vs_lookup_slot_def split: if_split_asm)
|
||||
apply (rename_tac pt_ptr)
|
||||
apply (drule (5) valid_vspace_objs_strongD)
|
||||
apply (clarsimp simp: in_omonad ptes_of_def)
|
||||
apply (frule (1) pspace_alignedD, clarsimp)
|
||||
apply (prop_tac "table_size = pt_bits", simp add: bit_simps)
|
||||
apply (clarsimp simp: is_aligned_pt_slot_offset_pte)
|
||||
apply (drule_tac x="table_index (pt_slot_offset level pt_ptr vref)" in bspec; clarsimp)
|
||||
apply (drule (1) table_index_max_level_slots)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma pt_bits_left_inj[simp]:
|
||||
"(pt_bits_left level' = pt_bits_left level) = (level' = level)"
|
||||
by (simp add: pt_bits_left_def bit_simps)
|
||||
|
||||
lemma pt_walk_stopped:
|
||||
"\<lbrakk> pt_walk top_level level top_ptr vref (ptes_of s) = Some (level', pt_ptr);
|
||||
level < level'; level \<le> max_pt_level \<rbrakk>
|
||||
\<Longrightarrow> \<exists>pte. ptes_of s (pt_slot_offset level' pt_ptr vref) = Some pte \<and> \<not> is_PageTablePTE pte"
|
||||
apply (induct top_level arbitrary: top_ptr; clarsimp)
|
||||
apply (subst (asm) (2) pt_walk.simps)
|
||||
apply (clarsimp split: if_split_asm)
|
||||
done
|
||||
|
||||
lemma vs_lookup_table_stopped:
|
||||
"\<lbrakk> vs_lookup_table level asid vref s = Some (level', pt_ptr); level' \<noteq> level;
|
||||
level \<le> max_pt_level \<rbrakk> \<Longrightarrow>
|
||||
\<exists>pte. ptes_of s (pt_slot_offset level' pt_ptr vref) = Some pte \<and> \<not>is_PageTablePTE pte"
|
||||
apply (clarsimp simp: vs_lookup_table_def split: if_split_asm)
|
||||
apply (frule pt_walk_min_level)
|
||||
apply (clarsimp simp: min_def split: if_split_asm)
|
||||
apply (fastforce dest: pt_walk_stopped)
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
context Arch_pspace_update_eq begin
|
||||
|
|
|
|||
|
|
@ -18,11 +18,6 @@ begin
|
|||
|
||||
context Arch begin global_naming RISCV64
|
||||
|
||||
(* FIXME RISCV: move up *)
|
||||
lemma riscv_global_pts_global_ref:
|
||||
"pt \<in> riscv_global_pts (arch_state s) level \<Longrightarrow> pt \<in> global_refs s"
|
||||
by (auto simp: global_refs_def)
|
||||
|
||||
named_theorems Retype_AI_assms
|
||||
|
||||
lemma arch_kobj_size_cong[Retype_AI_assms]:
|
||||
|
|
@ -160,64 +155,6 @@ crunch pspace_respects_device_region[wp]: copy_global_mappings "pspace_respects_
|
|||
crunch cap_refs_respects_device_region[wp]: copy_global_mappings "cap_refs_respects_device_region"
|
||||
(wp: crunch_wps)
|
||||
|
||||
(* FIXME RISCV: these should go to where something is assigned to an ASIDPool
|
||||
lemma copy_global_equal_kernel_mappings_restricted:
|
||||
"is_aligned pt pt_bits \<Longrightarrow>
|
||||
\<lbrace>\<lambda>s. equal_kernel_mappings (s \<lparr> kheap := restrict_map (kheap s) (- (insert pt S)) \<rparr>)
|
||||
\<and> pspace_aligned s \<and> valid_arch_state s\<rbrace>
|
||||
copy_global_mappings pt
|
||||
\<lbrace>\<lambda>rv s. equal_kernel_mappings (s \<lparr> kheap := restrict_map (kheap s) (- S) \<rparr>)\<rbrace>"
|
||||
apply (simp add: copy_global_mappings_def equal_kernel_mappings_def, wp)
|
||||
done
|
||||
|
||||
lemma copy_global_invs_mappings_restricted:
|
||||
"\<lbrace>(\<lambda>s. all_invs_but_equal_kernel_mappings_restricted (insert pd S) s)
|
||||
and (\<lambda>s. insert pd S \<inter> global_refs s = {})
|
||||
and K (is_aligned pd pd_bits)\<rbrace>
|
||||
copy_global_mappings pd
|
||||
\<lbrace>\<lambda>rv. all_invs_but_equal_kernel_mappings_restricted S\<rbrace>"
|
||||
apply (simp add: copy_global_mappings_def equal_kernel_mappings_def, wp, auto)
|
||||
done
|
||||
|
||||
lemma copy_global_mappings_valid_ioc[wp]:
|
||||
"\<lbrace>valid_ioc\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>_. valid_ioc\<rbrace>"
|
||||
by (simp add: copy_global_mappings_def)
|
||||
|
||||
lemma copy_global_mappings_vms[wp]:
|
||||
"\<lbrace>valid_machine_state\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>_. valid_machine_state\<rbrace>"
|
||||
by (simp add: copy_global_mappings_def)
|
||||
|
||||
lemma copy_global_mappings_invs:
|
||||
"\<lbrace>invs and (\<lambda>s. pd \<notin> global_refs s)
|
||||
and K (is_aligned pd pd_bits)\<rbrace>
|
||||
copy_global_mappings pd \<lbrace>\<lambda>rv. invs\<rbrace>"
|
||||
apply (fold all_invs_but_equal_kernel_mappings_restricted_eq)
|
||||
apply (rule hoare_pre, rule copy_global_invs_mappings_restricted)
|
||||
apply (clarsimp simp: equal_kernel_mappings_def obj_at_def
|
||||
restrict_map_def)
|
||||
done
|
||||
|
||||
crunch global_refs_inv[wp]: copy_global_mappings "\<lambda>s. P (global_refs s)"
|
||||
(wp: crunch_wps)
|
||||
|
||||
lemma mapM_copy_global_invs_mappings_restricted:
|
||||
"\<lbrace>\<lambda>s. all_invs_but_equal_kernel_mappings_restricted (set pds) s
|
||||
\<and> (set pds \<inter> global_refs s = {})
|
||||
\<and> (\<forall>pd \<in> set pds. is_aligned pd pd_bits)\<rbrace>
|
||||
mapM_x copy_global_mappings pds
|
||||
\<lbrace>\<lambda>rv. invs\<rbrace>"
|
||||
apply (fold all_invs_but_equal_kernel_mappings_restricted_eq)
|
||||
apply (induct pds, simp_all only: mapM_x_Nil mapM_x_Cons K_bind_def)
|
||||
apply (wp, simp)
|
||||
apply (rule hoare_seq_ext, assumption, thin_tac "P" for P)
|
||||
apply (rule hoare_conjI)
|
||||
apply (rule hoare_pre, rule copy_global_invs_mappings_restricted)
|
||||
apply clarsimp
|
||||
apply (rule hoare_pre, wp)
|
||||
apply clarsimp
|
||||
done
|
||||
*)
|
||||
|
||||
lemma dmo_eq_kernel_restricted [wp, Retype_AI_assms]:
|
||||
"\<lbrace>\<lambda>s. equal_kernel_mappings (kheap_update (f (kheap s)) s)\<rbrace>
|
||||
do_machine_op m
|
||||
|
|
@ -803,7 +740,7 @@ lemma valid_table_caps:
|
|||
|
||||
lemma caps_of_state':
|
||||
"caps_of_state s p = Some cap \<Longrightarrow> caps_of_state s' p = Some cap"
|
||||
by (fastforce simp: F cte_wp_at_cases s'_def ps_def orthr) (* FIXME RISCV: F? *)
|
||||
by (fastforce simp: F cte_wp_at_cases s'_def ps_def orthr)
|
||||
|
||||
lemma valid_vs_lookup:
|
||||
"valid_vs_lookup s \<Longrightarrow> valid_vs_lookup s'"
|
||||
|
|
|
|||
|
|
@ -116,42 +116,17 @@ proof -
|
|||
show ?thesis by auto
|
||||
qed
|
||||
|
||||
(* FIXME RISCV: move to lib *)
|
||||
(* FIXME: move to lib *)
|
||||
lemma throw_opt_wp[wp]:
|
||||
"\<lbrace>if v = None then E ex else Q (the v)\<rbrace> throw_opt ex v \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
|
||||
unfolding throw_opt_def by wpsimp auto
|
||||
|
||||
(* FIXME RISCV: move to ArchInvariants *)
|
||||
lemma arch_cap_fun_lift_Some[simp]:
|
||||
"(arch_cap_fun_lift f None cap = Some x) = (\<exists>acap. cap = ArchObjectCap acap \<and> f acap = Some x)"
|
||||
by (cases cap; simp)
|
||||
|
||||
context Arch begin global_naming RISCV64
|
||||
|
||||
(* FIXME RISCV: move up? *)
|
||||
(* this is what copy_global_mappings needs to establish from an empty_pt *)
|
||||
definition
|
||||
definition kernel_mappings_only :: "(pt_index \<Rightarrow> pte) \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" where
|
||||
"kernel_mappings_only pt s \<equiv>
|
||||
has_kernel_mappings pt s \<and> (\<forall>idx. idx \<notin> kernel_mapping_slots \<longrightarrow> pt idx = InvalidPTE)"
|
||||
|
||||
(* FIXME RISCV: move *)
|
||||
lemma vs_lookup_table_vspace:
|
||||
"\<lbrakk> vs_lookup_table level asid vptr s = Some (level, pt_ptr);
|
||||
vspace_for_asid asid' s = Some pt_ptr; vptr \<in> user_region; invs s \<rbrakk>
|
||||
\<Longrightarrow> asid' = asid \<and> level = max_pt_level"
|
||||
apply (cases "level = asid_pool_level"; clarsimp)
|
||||
apply (clarsimp simp: vs_lookup_table_def)
|
||||
apply (drule pool_for_asid_validD; clarsimp)
|
||||
apply (drule vspace_for_asid_valid_pt; clarsimp)
|
||||
apply (fastforce simp: in_omonad)
|
||||
apply (drule vspace_for_asid_vs_lookup)
|
||||
apply (frule_tac level=level and level'=max_pt_level in unique_vs_lookup_table, assumption; clarsimp?)
|
||||
apply (fastforce intro: valid_objs_caps)
|
||||
apply (drule (1) no_loop_vs_lookup_table; clarsimp?)
|
||||
apply (rule vref_for_level_eq_max_mono[symmetric], simp)
|
||||
apply (fastforce intro: valid_objs_caps)
|
||||
done
|
||||
|
||||
lemma find_vspace_for_asid_wp[wp]:
|
||||
"\<lbrace>\<lambda>s. (vspace_for_asid asid s = None \<longrightarrow> E InvalidRoot s) \<and>
|
||||
(\<forall>pt. vspace_for_asid asid s = Some pt \<longrightarrow> Q pt s) \<rbrace>
|
||||
|
|
@ -785,16 +760,6 @@ lemma pts_of_Some_alignedD:
|
|||
"\<lbrakk> pts_of s p = Some pt; pspace_aligned s \<rbrakk> \<Longrightarrow> is_aligned p pt_bits"
|
||||
by (drule pspace_aligned_pts_ofD; simp)
|
||||
|
||||
(* FIXME RISCV: move *)
|
||||
lemma table_index_max_level_slots:
|
||||
"\<lbrakk> vref \<in> user_region; is_aligned pt pt_bits \<rbrakk>
|
||||
\<Longrightarrow> table_index (pt_slot_offset max_pt_level pt vref) \<notin> kernel_mapping_slots"
|
||||
apply (simp add: kernel_mapping_slots_def table_index_offset_max_pt_level not_le user_region_def)
|
||||
apply (simp add: pt_bits_left_def level_defs bit_simps canonical_user_def)
|
||||
apply word_bitwise
|
||||
apply (simp add: word_size canonical_bit_def word_bits_def)
|
||||
done
|
||||
|
||||
lemma vs_lookup_target_not_global:
|
||||
"\<lbrakk> vs_lookup_target level asid vref s = Some (level, pt); vref \<in> user_region; invs s \<rbrakk>
|
||||
\<Longrightarrow> pt \<notin> global_refs s"
|
||||
|
|
@ -880,23 +845,6 @@ lemma mapM_x_swp_store_pte_invs_unmap:
|
|||
mapM_x (swp store_pte pte) slots \<lbrace>\<lambda>_. invs\<rbrace>"
|
||||
by (simp add: mapM_x_mapM | wp mapM_swp_store_pte_invs_unmap)+
|
||||
|
||||
(* FIXME RISCV: move *)
|
||||
lemma valid_vspace_objs_strong_slotD:
|
||||
"\<lbrakk> vs_lookup_slot level asid vref s = Some (level, slot); vref \<in> user_region;
|
||||
level \<le> max_pt_level; valid_vspace_objs s; valid_asid_table s; pspace_aligned s\<rbrakk>
|
||||
\<Longrightarrow> \<exists>pte. ptes_of s slot = Some pte \<and> valid_pte level pte s"
|
||||
apply (clarsimp simp: vs_lookup_slot_def split: if_split_asm)
|
||||
apply (rename_tac pt_ptr)
|
||||
apply (drule (5) valid_vspace_objs_strongD)
|
||||
apply (clarsimp simp: in_omonad ptes_of_def)
|
||||
apply (frule (1) pspace_alignedD, clarsimp)
|
||||
apply (prop_tac "table_size = pt_bits", simp add: bit_simps)
|
||||
apply (clarsimp simp: is_aligned_pt_slot_offset_pte)
|
||||
apply (drule_tac x="table_index (pt_slot_offset level pt_ptr vref)" in bspec; clarsimp)
|
||||
apply (drule (1) table_index_max_level_slots)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma vs_lookup_table_step:
|
||||
"\<lbrakk> vs_lookup_table level asid vref s = Some (level, pt'); level \<le> max_pt_level; 0 < level;
|
||||
ptes_of s (pt_slot_offset level pt' vref) = Some pte; is_PageTablePTE pte;
|
||||
|
|
@ -953,8 +901,6 @@ lemma store_pte_invalid_vs_lookup_target_unmap:
|
|||
apply (clarsimp simp flip: bit0.neq_0_conv simp: is_PageTablePTE_def)
|
||||
apply (fastforce simp: pte_ref_Some_cases)
|
||||
apply (drule (1) no_loop_vs_lookup_table; simp?)
|
||||
apply (drule max_pt_level_eq_minus_one)
|
||||
apply simp
|
||||
(* PagePTE *)
|
||||
apply (prop_tac "\<exists>sz. data_at sz p' s")
|
||||
apply (fastforce simp: is_PagePTE_def pptr_from_pte_def)
|
||||
|
|
@ -1475,38 +1421,12 @@ lemma unmap_page_pool_for_asid[wp]:
|
|||
"unmap_page pgsz asid vref pt \<lbrace>\<lambda>s. P (pool_for_asid asid s)\<rbrace>"
|
||||
unfolding unmap_page_def by (wpsimp simp: pool_for_asid_def)
|
||||
|
||||
(* FIXME RISCV: move to ArchInvariants *)
|
||||
lemma pt_bits_left_inj[simp]:
|
||||
"(pt_bits_left level' = pt_bits_left level) = (level' = level)"
|
||||
by (simp add: pt_bits_left_def bit_simps)
|
||||
|
||||
lemma data_at_level:
|
||||
"\<lbrakk> data_at pgsz p s; data_at (vmpage_size_of_level level) p s;
|
||||
pt_bits_left level' = pageBitsForSize pgsz; level \<le> max_pt_level \<rbrakk> \<Longrightarrow>
|
||||
level = level'"
|
||||
by (fastforce simp: data_at_def obj_at_def)
|
||||
|
||||
(* FIXME RISCV: move to ArchInvariants *)
|
||||
lemma pt_walk_stopped:
|
||||
"\<lbrakk> pt_walk top_level level top_ptr vref (ptes_of s) = Some (level', pt_ptr);
|
||||
level < level'; level \<le> max_pt_level \<rbrakk>
|
||||
\<Longrightarrow> \<exists>pte. ptes_of s (pt_slot_offset level' pt_ptr vref) = Some pte \<and> \<not> is_PageTablePTE pte"
|
||||
apply (induct top_level arbitrary: top_ptr; clarsimp)
|
||||
apply (subst (asm) (2) pt_walk.simps)
|
||||
apply (clarsimp split: if_split_asm)
|
||||
done
|
||||
|
||||
(* FIXME RISCV: move to ArchInvariants *)
|
||||
lemma vs_lookup_table_stopped:
|
||||
"\<lbrakk> vs_lookup_table level asid vref s = Some (level', pt_ptr); level' \<noteq> level;
|
||||
level \<le> max_pt_level \<rbrakk> \<Longrightarrow>
|
||||
\<exists>pte. ptes_of s (pt_slot_offset level' pt_ptr vref) = Some pte \<and> \<not>is_PageTablePTE pte"
|
||||
apply (clarsimp simp: vs_lookup_table_def split: if_split_asm)
|
||||
apply (frule pt_walk_min_level)
|
||||
apply (clarsimp simp: min_def split: if_split_asm)
|
||||
apply (fastforce dest: pt_walk_stopped)
|
||||
done
|
||||
|
||||
lemma unmap_page_not_target:
|
||||
"\<lbrace> data_at pgsz pptr and valid_asid_table and valid_vspace_objs and pspace_aligned
|
||||
and unique_table_refs and valid_vs_lookup and (\<lambda>s. valid_caps (caps_of_state s) s)
|
||||
|
|
@ -2137,14 +2057,6 @@ lemma copy_global_mappings_copies[wp]:
|
|||
riscv_global_pt_in_global_refs valid_global_vspace_mappings_aligned)
|
||||
done
|
||||
|
||||
(* FIXME RISCV: move *)
|
||||
lemma ptes_of_wellformed_pte:
|
||||
"\<lbrakk> ptes_of s p = Some pte; valid_objs s \<rbrakk> \<Longrightarrow> wellformed_pte pte"
|
||||
apply (clarsimp simp: ptes_of_def in_omonad)
|
||||
apply (erule (1) valid_objsE)
|
||||
apply (clarsimp simp: valid_obj_def)
|
||||
done
|
||||
|
||||
lemma copy_global_mappings_invs:
|
||||
"\<lbrace> invs and K (is_aligned pt_ptr pt_bits) and
|
||||
(\<lambda>s. \<forall>level. \<not> \<exists>\<rhd> (level, pt_ptr) s) and
|
||||
|
|
|
|||
|
|
@ -134,6 +134,10 @@ definition riscv_global_pt :: "arch_state \<Rightarrow> obj_ref"
|
|||
where
|
||||
"riscv_global_pt s = the_elem (riscv_global_pts s max_pt_level)"
|
||||
|
||||
locale_abbrev global_pt :: "'z state \<Rightarrow> obj_ref"
|
||||
where
|
||||
"global_pt s \<equiv> riscv_global_pt (arch_state s)"
|
||||
|
||||
text \<open>
|
||||
The kernel window is mapped into every virtual address space from the @{term pptr_base}
|
||||
pointer upwards. This function copies the mappings which create the kernel window into a new
|
||||
|
|
@ -142,7 +146,7 @@ text \<open>
|
|||
definition copy_global_mappings :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
|
||||
where
|
||||
"copy_global_mappings new_pm \<equiv> do
|
||||
global_pt \<leftarrow> gets (riscv_global_pt \<circ> arch_state);
|
||||
global_pt \<leftarrow> gets global_pt;
|
||||
base \<leftarrow> return $ pt_index max_pt_level pptr_base;
|
||||
pt_size \<leftarrow> return $ 1 << ptTranslationBits;
|
||||
mapM_x (\<lambda>index. do
|
||||
|
|
|
|||
|
|
@ -99,7 +99,7 @@ definition set_vm_root :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
|
|||
odE
|
||||
| _ \<Rightarrow> throwError InvalidRoot) <catch>
|
||||
(\<lambda>_. do
|
||||
global_pt \<leftarrow> gets (riscv_global_pt \<circ> arch_state);
|
||||
global_pt \<leftarrow> gets global_pt;
|
||||
do_machine_op $ setVSpaceRoot (addrFromPPtr global_pt) 0
|
||||
od)
|
||||
od"
|
||||
|
|
|
|||
Loading…
Reference in New Issue