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

riscv refine: prove new Haskell assertions 

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein 2020-04-18 11:42:21 +08:00
parent 7b9249fe2a
commit 14206e2536
4 changed files with 67 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
proof/refine/RISCV64/ArchAcc_R.thy
View File

@ -515,7 +515,7 @@ lemma lookupPTSlotFromLevel_inv:
apply (subst lookupPTSlotFromLevel.simps)
apply (wpsimp simp: pteAtIndex_def wp: getPTE_wp)
apply (subst lookupPTSlotFromLevel.simps)
apply (wpsimp simp: pteAtIndex_def wp: getPTE_wp|assumption)+
apply (wpsimp simp: pteAtIndex_def checkPTAt_def wp: getPTE_wp|assumption)+
done
declare lookupPTSlotFromLevel_inv[wp]
@ -524,11 +524,11 @@ lemma lookupPTFromLevel_inv[wp]:
"lookupPTFromLevel level pt vptr target_pt \<lbrace>P\<rbrace>"
proof (induct level arbitrary: pt)
case 0 show ?case
by (subst lookupPTFromLevel.simps, simp, wp)
by (subst lookupPTFromLevel.simps, simp add: checkPTAt_def, wp)
next
case (Suc level)
show ?case
by (subst lookupPTFromLevel.simps, simp)
by (subst lookupPTFromLevel.simps, simp add: checkPTAt_def)
(wpsimp wp: Suc getPTE_wp simp: pteAtIndex_def)
qed
@ -630,7 +630,13 @@ next
show ?case
apply (subst pt_lookup_slot_from_level_rec)
apply (simp add: lookupPTSlotFromLevel.simps Let_def obind_comp_dist if_comp_dist
gets_the_if_distrib)
gets_the_if_distrib checkPTAt_def)
apply (rule corres_stateAssert_implied[where P'="\<lambda>_. True", simplified, rotated])
apply clarsimp
apply (rule page_table_at_cross; assumption?)
apply (drule (5) valid_vspace_objs_strongD)
apply (clarsimp simp: pt_at_eq in_omonad)
apply (simp add: state_relation_def)
apply (rule corres_guard_imp, rule corres_split[where r'=pte_relation'])
apply (rule corres_if3)
apply (rename_tac pte pte', case_tac pte; (simp add: isPageTablePTE_def))
@ -690,7 +696,13 @@ proof (induct level arbitrary: level' pt pt')
case 0
then show ?case
apply (subst lookupPTFromLevel.simps, subst pt_lookup_from_level_simps)
apply (clarsimp simp: lookup_failure_map_def)
apply (clarsimp simp: checkPTAt_def liftE_bindE)
apply (rule corres_stateAssert_implied[where P'="\<lambda>_. True", simplified, rotated])
apply clarsimp
apply (rule page_table_at_cross; assumption?)
apply (drule vs_lookup_table_pt_at; simp?)
apply (simp add: state_relation_def)
apply (simp add: lookup_failure_map_def)
done
next
case (minus level)
@ -745,6 +757,13 @@ next
from minus.prems
show ?case
apply (subst lookupPTFromLevel.simps, subst pt_lookup_from_level_simps)
apply (clarsimp simp: checkPTAt_def)
apply (subst liftE_bindE,
rule corres_stateAssert_implied[where P'="\<lambda>_. True", simplified, rotated])
apply clarsimp
apply (rule page_table_at_cross; assumption?)
apply (drule vs_lookup_table_pt_at; simp?)
apply (simp add: state_relation_def)
apply (simp add: unlessE_whenE not_less)
apply (rule corres_initial_splitE[where r'=dc])
apply (corressimp simp: lookup_failure_map_def)

2
proof/refine/RISCV64/EmptyFail_H.thy
View File

@ -150,7 +150,7 @@ proof (induct level arbitrary: pt)
next
case (Suc level)
then show ?case
by (subst lookupPTSlotFromLevel.simps) (wpsimp simp: pteAtIndex_def)
by (subst lookupPTSlotFromLevel.simps) (wpsimp simp: checkPTAt_def pteAtIndex_def)
qed
lemma empty_fail_arch_cap_exhausted:

47
proof/refine/RISCV64/Retype_R.thy
View File

@ -12,6 +12,10 @@ theory Retype_R
imports VSpace_R
begin
(* FIXME RISCV: move way up somewhere *)
text \<open>To ensure that the proof state is in a certain case of a case distinction:\<close>
method in_case for x::'a = match premises in "t = x" for t \<Rightarrow> succeed
context begin interpretation Arch . (*FIXME: arch_split*)
definition
@ -2191,28 +2195,29 @@ proof -
using cover
apply (clarsimp simp: RISCV64_H.toAPIType_def APIType_capBits_def
split: RISCV64_H.object_type.splits)
\<comment> \<open>SmallPageObject\<close>
apply (in_case "HugePageObject")
apply wp
apply (simp add: valid_cap'_def capAligned_def n_less_word_bits ball_conj_distrib)
apply (wp createObjects_aligned2 createObjects_nonzero'
cwo_ret'[where bs=0, simplified]
cwo_ret'[where bs="ptTranslationBits + ptTranslationBits", simplified]
| simp add: objBits_if_dev pageBits_def ptr range_cover_n_wb)+
apply (simp add:pageBits_def ptr word_bits_def)
\<comment> \<open>LargePageObject\<close>
apply (in_case "SmallPageObject")
apply wp
apply (simp add: valid_cap'_def capAligned_def n_less_word_bits ball_conj_distrib)
apply (wp createObjects_aligned2 createObjects_nonzero'
cwo_ret'[where bs=ptTranslationBits, simplified]
cwo_ret'[where bs=0, simplified]
| simp add: objBits_if_dev pageBits_def ptr range_cover_n_wb)+
apply (simp add:pageBits_def ptr word_bits_def)
\<comment> \<open>HugePageObject\<close>
apply (in_case \<open>LargePageObject\<close>)
apply wp
apply (simp add: valid_cap'_def capAligned_def n_less_word_bits ball_conj_distrib)
apply (wp createObjects_aligned2 createObjects_nonzero'
cwo_ret'[where bs="ptTranslationBits + ptTranslationBits", simplified]
cwo_ret'[where bs=ptTranslationBits, simplified]
| simp add: objBits_if_dev pageBits_def ptr range_cover_n_wb)+
apply (simp add:pageBits_def ptr word_bits_def)
\<comment> \<open>PageTableObject\<close>
apply (in_case \<open>PageTableObject\<close>)
apply wp
apply (simp add: valid_cap'_def capAligned_def n_less_word_bits)
apply (rule hoare_chain)
@ -2231,7 +2236,7 @@ proof -
apply (rule ucast_less[where 'b="pt_index_len" and 'a="machine_word_len", simplified])
apply simp
apply clarsimp
done
done
next
case (Some a) thus ?thesis
proof(cases a)
@ -5181,7 +5186,7 @@ lemma corres_retype_region_createNewCaps:
apply (clarsimp simp: list_all2_same list_all2_map1 list_all2_map2 objBits_simps
allRights_def APIType_map2_def
split del: if_split)
\<comment> \<open>SmallPageObject\<close>
apply (in_case \<open>HugePageObject\<close>)
apply (subst retype_region2_extra_ext_trivial)
apply (simp add: APIType_map2_def)
apply (simp add: corres_liftM2_simp[unfolded liftM_def] split del: if_split)
@ -5191,13 +5196,13 @@ lemma corres_retype_region_createNewCaps:
apply (rule corres_retype_update_gsI;
clarsimp simp: obj_bits_api_def3 APIType_map2_def objBits_simps ext
default_object_def default_arch_object_def makeObjectKO_def
data_page_relation_retype
data_page_relation_retype bit_simps
elim!: range_cover.aligned;
assumption)
apply fastforce+
apply (simp add: APIType_map2_def arch_default_cap_def vm_read_write_def vmrights_map_def
list_all2_map1 list_all2_map2 list_all2_same)
\<comment> \<open>LargePageObject\<close>
apply (simp add: APIType_map2_def arch_default_cap_def vm_read_write_def vmrights_map_def
list_all2_map1 list_all2_map2 list_all2_same)
apply (in_case \<open>SmallPageObject\<close>)
apply (subst retype_region2_extra_ext_trivial)
apply (simp add: APIType_map2_def)
apply (simp add: corres_liftM2_simp[unfolded liftM_def] split del: if_split)
@ -5211,9 +5216,9 @@ lemma corres_retype_region_createNewCaps:
elim!: range_cover.aligned;
assumption)
apply fastforce+
apply (simp add: APIType_map2_def arch_default_cap_def vm_read_write_def vmrights_map_def
list_all2_map1 list_all2_map2 list_all2_same)
\<comment> \<open>HugePageObject\<close>
apply (simp add: APIType_map2_def arch_default_cap_def vm_read_write_def vmrights_map_def
list_all2_map1 list_all2_map2 list_all2_same)
apply (in_case \<open>LargePageObject\<close>)
apply (subst retype_region2_extra_ext_trivial)
apply (simp add: APIType_map2_def)
apply (simp add: corres_liftM2_simp[unfolded liftM_def] split del: if_split)
@ -5223,13 +5228,13 @@ lemma corres_retype_region_createNewCaps:
apply (rule corres_retype_update_gsI;
clarsimp simp: obj_bits_api_def3 APIType_map2_def objBits_simps ext
default_object_def default_arch_object_def makeObjectKO_def
data_page_relation_retype bit_simps
data_page_relation_retype
elim!: range_cover.aligned;
assumption)
apply fastforce+
apply (simp add: APIType_map2_def arch_default_cap_def vm_read_write_def vmrights_map_def
list_all2_map1 list_all2_map2 list_all2_same)
\<comment> \<open>PageTable\<close>
apply (simp add: APIType_map2_def arch_default_cap_def vm_read_write_def vmrights_map_def
list_all2_map1 list_all2_map2 list_all2_same)
apply (in_case \<open>PageTableObject\<close>)
apply (subst retype_region2_extra_ext_trivial)
apply (simp add: APIType_map2_def)
apply (simp_all add: corres_liftM2_simp[unfolded liftM_def])
@ -5244,7 +5249,7 @@ lemma corres_retype_region_createNewCaps:
apply (clarsimp simp: list_all2_map1 list_all2_map2 list_all2_same
APIType_map2_def arch_default_cap_def)
apply fastforce+
done
done
end
end

16
proof/refine/RISCV64/Untyped_R.thy
View File

@ -4625,6 +4625,16 @@ lemma (in range_cover) funky_aligned:
apply simp
done
(* FIXME RISCV: move to Corres_UL *)
lemma corres_assert_gen_asm_cross:
"\<lbrakk> \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; Q' s'\<rbrakk> \<Longrightarrow> A;
A \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g ()) \<rbrakk>
\<Longrightarrow> corres_underlying sr nf nf' r (P and P') (Q and Q') f (assert A >>= g)"
by (metis corres_assert_assume corres_cases corres_name_pre)
defs canonicalAddressAssert_def:
"canonicalAddressAssert p \<equiv> RISCV64.canonical_address p"
context begin interpretation Arch . (*FIXME: arch_split*)
lemma inv_untyped_corres':
@ -4863,6 +4873,11 @@ lemma inv_untyped_corres':
have sz_limit[simp]: "sz \<le> maxUntypedSizeBits"
using vc' unfolding valid_cap'_def by clarsimp
have canonical_ptr[simp]: "canonical_address ptr"
using ptr_cn sz_limit
unfolding canonical_address_range maxUntypedSizeBits_def canonical_bit_def
by word_bitwise (simp add: word_size)
note set_cap_free_index_invs_spec = set_free_index_invs[where cap = "cap.UntypedCap
dev (ptr && ~~ mask sz) sz (if reset then 0 else idx)"
,unfolded free_index_update_def free_index_of_def,simplified]
@ -4887,6 +4902,7 @@ lemma inv_untyped_corres':
sz (if reset then 0 else idx)" in corres_gen_asm)
apply (rule corres_add_noop_lhs)
apply (rule corres_split_nor[OF _ cNodeNoOverlap return_wp stateAssert_wp])
apply (clarsimp simp: canonicalAddressAssert_def)
apply (rule corres_split[OF _ updateFreeIndex_corres,rotated])
apply (simp add:isCap_simps)+
apply (clarsimp simp:getFreeIndex_def bits_of_def shiftL_nat shiftl_t2n