riscv access: add proofs for Arch_AC
Signed-off-by: Ryan Barry <ryan.barry@unsw.edu.au>
This commit is contained in:
parent
cc5014240d
commit
ed8971a269
|
@ -67,12 +67,25 @@ lemma mapM_set'':
|
||||||
apply (auto simp: neq_Nil_conv)
|
apply (auto simp: neq_Nil_conv)
|
||||||
done
|
done
|
||||||
|
|
||||||
|
lemma as_user_state_vrefs:
|
||||||
|
"\<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace>
|
||||||
|
as_user t f
|
||||||
|
\<lbrace>\<lambda>_ s :: det_ext state. P (state_vrefs s)\<rbrace>"
|
||||||
|
apply (simp add: as_user_def)
|
||||||
|
apply (wpsimp wp: set_object_wp)
|
||||||
|
apply (clarsimp simp: state_vrefs_tcb_upd obj_at_def is_obj_defs
|
||||||
|
elim!: rsubst[where P=P, OF _ ext]
|
||||||
|
dest!: get_tcb_SomeD)
|
||||||
|
done
|
||||||
|
|
||||||
lemma as_user_pas_refined[wp]:
|
lemma as_user_pas_refined[wp]:
|
||||||
"as_user t f \<lbrace>pas_refined aag\<rbrace>"
|
"\<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and pas_refined aag\<rbrace>
|
||||||
|
as_user t f
|
||||||
|
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
|
||||||
apply (simp add: pas_refined_def state_objs_to_policy_def)
|
apply (simp add: pas_refined_def state_objs_to_policy_def)
|
||||||
apply (rule hoare_pre)
|
apply (rule hoare_pre)
|
||||||
apply wps
|
apply wps
|
||||||
apply wp
|
apply (wp as_user_state_vrefs)
|
||||||
apply simp
|
apply simp
|
||||||
done
|
done
|
||||||
|
|
||||||
|
@ -137,11 +150,16 @@ lemma is_subject_asid_into_loas:
|
||||||
|
|
||||||
locale Arch_AC_1 =
|
locale Arch_AC_1 =
|
||||||
assumes set_mrs_state_vrefs[wp]:
|
assumes set_mrs_state_vrefs[wp]:
|
||||||
"set_mrs thread buf msgs \<lbrace>\<lambda>s :: det_ext state. P (state_vrefs s)\<rbrace>"
|
"\<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace>
|
||||||
|
set_mrs thread buf msgs
|
||||||
|
\<lbrace>\<lambda>_ s :: det_ext state. P (state_vrefs s)\<rbrace>"
|
||||||
and mul_add_word_size_lt_msg_align_bits_ofnat:
|
and mul_add_word_size_lt_msg_align_bits_ofnat:
|
||||||
"\<lbrakk> p < 2 ^ (msg_align_bits - word_size_bits); k < 4 \<rbrakk>
|
"\<lbrakk> p < 2 ^ (msg_align_bits - word_size_bits); k < word_size \<rbrakk>
|
||||||
\<Longrightarrow> of_nat p * of_nat word_size + k < (2 :: obj_ref) ^ msg_align_bits"
|
\<Longrightarrow> of_nat p * of_nat word_size + k < (2 :: obj_ref) ^ msg_align_bits"
|
||||||
begin
|
and zero_less_word_size[simp]:
|
||||||
|
"0 < (word_size :: obj_ref)"
|
||||||
|
|
||||||
|
context Arch_AC_1 begin
|
||||||
|
|
||||||
lemmas mul_word_size_lt_msg_align_bits_ofnat =
|
lemmas mul_word_size_lt_msg_align_bits_ofnat =
|
||||||
mul_add_word_size_lt_msg_align_bits_ofnat[where k=0, simplified]
|
mul_add_word_size_lt_msg_align_bits_ofnat[where k=0, simplified]
|
||||||
|
@ -177,7 +195,9 @@ lemma store_word_offs_integrity_autarch:
|
||||||
done
|
done
|
||||||
|
|
||||||
lemma set_mrs_pas_refined[wp]:
|
lemma set_mrs_pas_refined[wp]:
|
||||||
"set_mrs thread buf msgs \<lbrace>pas_refined aag\<rbrace>"
|
"\<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and pas_refined aag\<rbrace>
|
||||||
|
set_mrs thread buf msgs
|
||||||
|
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
|
||||||
apply (simp add: pas_refined_def state_objs_to_policy_def)
|
apply (simp add: pas_refined_def state_objs_to_policy_def)
|
||||||
apply (rule hoare_pre)
|
apply (rule hoare_pre)
|
||||||
apply (wp | wps)+
|
apply (wp | wps)+
|
||||||
|
|
File diff suppressed because it is too large
Load Diff
Loading…
Reference in New Issue