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

riscv ainvs: more vs_lookup_target/table properties

This commit is contained in:
Rafal Kolanski 2019-05-03 07:47:45 +10:00
parent e46c7403fc
commit f443145e9c
2 changed files with 46 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -67,6 +67,18 @@ lemma vs_lookup_table_target:
apply (clarsimp simp: is_PageTablePTE_def pptr_from_pte_def split: if_split_asm)
done
lemma vs_lookup_table_targetD:
"\<lbrakk> vs_lookup_table level asid vref s = Some (level, p); level \<le> max_pt_level \<rbrakk>
\<Longrightarrow> \<exists>p'. vs_lookup_target (level+1) asid vref s = Some (level+1, p')"
apply (case_tac "level < max_pt_level")
apply (clarsimp dest!: vs_lookup_table_split_last_Some)
apply (clarsimp simp: vs_lookup_target_def vs_lookup_slot_def in_omonad pte_ref_def)
apply (fastforce dest: vm_level_less_plus_1_mono split: pte.splits)
apply (clarsimp simp: max_pt_level_plus_one vs_lookup_target_def vs_lookup_slot_def in_omonad
pte_ref_def pool_for_asid_vs_lookup)
apply (fastforce dest!: vs_lookup_table_max_pt_level_SomeD)
done
lemma valid_vs_lookupD:
"\<lbrakk> vs_lookup_target bot_level asid vref s = Some (level, p) ;
vref \<in> user_region; valid_vs_lookup s \<rbrakk>
@ -76,6 +88,12 @@ lemma valid_vs_lookupD:
unfolding valid_vs_lookup_def
by auto
lemma vs_lookup_table_asid_not_0:
"\<lbrakk> vs_lookup_table level asid vref s = Some (level, p); level \<le> max_pt_level;
vref \<in> user_region; valid_vs_lookup s \<rbrakk>
\<Longrightarrow> asid \<noteq> 0"
by (fastforce dest!: vs_lookup_table_targetD valid_vs_lookupD)
lemma vspace_for_asid_from_lookup_target:
"\<lbrakk> vs_lookup_target asid_pool_level asid vref s = Some (asid_pool_level, pt_ptr);
vref \<in> user_region; valid_vs_lookup s \<rbrakk>

28
proof/invariant-abstract/RISCV64/ArchInvariants_AI.thy
View File

@ -1774,6 +1774,11 @@ lemma pt_slot_offset_vref_for_level_eq:
"level < level' \<Longrightarrow> pt_slot_offset level pt_ptr (vref_for_level vref level') = pt_ptr"
by (simp add: vref_for_level_def pt_slot_offset_vref)
lemma vspace_for_pool_None_upd_idem:
"vspace_for_pool pool_ptr asid ((asid_pools_of s)(p := None)) = Some table_ptr
\<Longrightarrow> vspace_for_pool pool_ptr asid (asid_pools_of s) = Some table_ptr"
by (clarsimp simp: vspace_for_pool_def obind_def split: option.splits if_splits)
lemma vs_lookup_max_pt_levelD:
"vs_lookup_table max_pt_level asid vref s = Some (max_pt_level, root_pt)
\<Longrightarrow> \<exists>pool_ptr. pool_for_asid asid s = Some pool_ptr \<and>
@ -1786,6 +1791,11 @@ lemma vs_lookup_max_pt_levelI:
\<Longrightarrow> vs_lookup_table max_pt_level asid vref s = Some (max_pt_level, root_pt)"
by (clarsimp simp: vs_lookup_table_def in_omonad)
lemma vs_lookup_table_max_pt_level_SomeD:
"\<lbrakk> vs_lookup_table max_pt_level asid vref s = Some (level, p) \<rbrakk>
\<Longrightarrow> \<exists>pool. pool_for_asid asid s = Some pool \<and> vspace_for_pool pool asid (asid_pools_of s) = Some p"
by (clarsimp simp: vs_lookup_table_def in_omonad)
lemma vs_lookup_max_pt_valid:
"\<lbrakk> vs_lookup_table max_pt_level asid vref s = Some (max_pt_level, root_pt);
vref \<in> user_region;
@ -1800,6 +1810,11 @@ lemma aligned_vref_for_level_eq:
"is_aligned vref (pt_bits_left level) = (vref_for_level vref level = vref)"
unfolding vref_for_level_def using is_aligned_neg_mask_eq' by blast
lemma is_aligned_table_base_pte_bits[simp]:
"is_aligned (table_base p) pte_bits"
unfolding pte_bits_def
by (simp add: bit_simps is_aligned_neg_mask)
lemma pt_slot_offset_offset:
"is_aligned pt pt_bits \<Longrightarrow>
pt_slot_offset level pt vref && mask pt_bits >> pte_bits = pt_index level vref"
@ -1972,6 +1987,19 @@ lemma vs_lookup_split:
apply clarsimp
done
lemma vs_lookup_table_split_last_Some:
"\<lbrakk> vs_lookup_table level asid vref s = Some (level, p); level < max_pt_level \<rbrakk>
\<Longrightarrow> \<exists>p' pte. vs_lookup_table (level+1) asid vref s = Some (level+1, p')
\<and> ptes_of s (pt_slot_offset (level + 1) p' vref) = Some pte \<and> p = pptr_from_pte pte
\<and> is_PageTablePTE pte"
apply (clarsimp simp: vs_lookup_table_def in_omonad asid_pool_level_eq
vm_level_less_max_pt_level)
apply (subst (asm) pt_walk_split_Some[where level'="level+1"])
apply (clarsimp simp add: less_imp_le bit0.plus_one_leq)+
apply (subst (asm) (2) pt_walk.simps)
apply (clarsimp simp: in_omonad split: if_splits)
done
lemma vs_lookup_split_max_pt_level_Some:
"level \<le> max_pt_level \<Longrightarrow>
(vs_lookup_table level asid vref s = Some (level, p)) =