clib: remove seL4-related lemmas from Ctac.thy
This commit is contained in:
Rafal Kolanski
Alejandro Gomez-Londono
parent
dd62b49ee4
commit
9dbb5e4e2e
|
|
@ -12,8 +12,8 @@
|
|||
|
||||
theory Ctac
|
||||
imports
|
||||
Corres_C
|
||||
"../XPres"
|
||||
Corres_C
|
||||
"../XPres"
|
||||
begin
|
||||
|
||||
(* This file includes theorems associated with ctac and friends *)
|
||||
|
|
@ -1699,27 +1699,6 @@ lemmas ccorres_move_c_guards =
|
|||
ccorres_move_Guard[OF abs_c_guard_from_abs_h_t_valid]
|
||||
ccorres_move_Guard
|
||||
|
||||
lemma c_guard_abs_cte:
|
||||
fixes p :: "cte_C ptr"
|
||||
shows "\<forall>s s'. (s, s') \<in> rf_sr \<and> cte_at' (ptr_val p) s \<and> True \<longrightarrow> s' \<Turnstile>\<^sub>c p"
|
||||
apply (cases p)
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of)
|
||||
apply (erule (1) rf_sr_ctes_of_cliftE)
|
||||
apply (simp add: typ_heap_simps')
|
||||
done
|
||||
|
||||
lemmas ccorres_move_c_guard_cte [corres_pre] = ccorres_move_c_guards [OF c_guard_abs_cte]
|
||||
|
||||
lemma c_guard_abs_tcb:
|
||||
fixes p :: "tcb_C ptr"
|
||||
shows "\<forall>s s'. (s, s') \<in> rf_sr \<and> tcb_at' (ctcb_ptr_to_tcb_ptr p) s \<and> True \<longrightarrow> s' \<Turnstile>\<^sub>c p"
|
||||
apply clarsimp
|
||||
apply (drule (1) tcb_at_h_t_valid)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemmas ccorres_move_c_guard_tcb [corres_pre] = ccorres_move_c_guards [OF c_guard_abs_tcb]
|
||||
|
||||
lemma h_t_array_valid_array_assertion:
|
||||
"h_t_array_valid htd ptr n \<Longrightarrow> 0 < n
|
||||
\<Longrightarrow> array_assertion ptr n htd"
|
||||
|
|
@ -1727,64 +1706,6 @@ lemma h_t_array_valid_array_assertion:
|
|||
apply (fastforce intro: exI[where x=0])
|
||||
done
|
||||
|
||||
lemma cte_array_relation_array_assertion:
|
||||
"gsCNodes s p = Some n \<Longrightarrow> cte_array_relation s cstate
|
||||
\<Longrightarrow> array_assertion (cte_Ptr p) (2 ^ n) (hrs_htd (t_hrs_' cstate))"
|
||||
apply (rule h_t_array_valid_array_assertion)
|
||||
apply (clarsimp simp: cvariable_array_map_relation_def)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma rf_sr_gsCNodes_array_assertion:
|
||||
"gsCNodes s p = Some n \<Longrightarrow> (s, s') \<in> rf_sr
|
||||
\<Longrightarrow> array_assertion (cte_Ptr p) (2 ^ n) (hrs_htd (t_hrs_' (globals s')))"
|
||||
by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
|
||||
cte_array_relation_array_assertion)
|
||||
|
||||
lemma rf_sr_tcb_ctes_array_assertion:
|
||||
"\<lbrakk> (s, s') \<in> rf_sr; tcb_at' (ctcb_ptr_to_tcb_ptr tcb) s \<rbrakk>
|
||||
\<Longrightarrow> array_assertion (cte_Ptr (ptr_val tcb && 0xFFFFFE00))
|
||||
(unat tcbCNodeEntries) (hrs_htd (t_hrs_' (globals s')))"
|
||||
apply (rule h_t_array_valid_array_assertion, simp_all add: tcbCNodeEntries_def)
|
||||
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
|
||||
cvariable_array_map_relation_def
|
||||
cpspace_relation_def)
|
||||
apply (drule obj_at_ko_at', clarsimp)
|
||||
apply (drule spec, drule mp, rule exI, erule ko_at_projectKO_opt)
|
||||
apply (frule ptr_val_tcb_ptr_mask)
|
||||
apply (simp add: mask_def)
|
||||
done
|
||||
|
||||
lemma rf_sr_tcb_ctes_array_assertion2:
|
||||
"\<lbrakk> (s, s') \<in> rf_sr; tcb_at' tcb s \<rbrakk>
|
||||
\<Longrightarrow> array_assertion (cte_Ptr tcb)
|
||||
(unat tcbCNodeEntries) (hrs_htd (t_hrs_' (globals s')))"
|
||||
apply (frule(1) rf_sr_tcb_ctes_array_assertion[where
|
||||
tcb="tcb_ptr_to_ctcb_ptr t" for t, simplified])
|
||||
apply (simp add: ptr_val_tcb_ptr_mask')
|
||||
done
|
||||
|
||||
lemma array_assertion_abs_tcb_ctes:
|
||||
"\<forall>s s'. (s, s') \<in> rf_sr \<and> tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s \<and> (n s' \<le> unat tcbCNodeEntries)
|
||||
\<longrightarrow> (x s' = 0 \<or> array_assertion (cte_Ptr (ptr_val (tcb s') && 0xFFFFFE00)) (n s') (hrs_htd (t_hrs_' (globals s'))))"
|
||||
"\<forall>s s'. (s, s') \<in> rf_sr \<and> tcb_at' tcb' s \<and> (n s' \<le> unat tcbCNodeEntries)
|
||||
\<longrightarrow> (x s' = 0 \<or> array_assertion (cte_Ptr tcb') (n s') (hrs_htd (t_hrs_' (globals s'))))"
|
||||
apply (safe intro!: disjCI2)
|
||||
apply (drule(1) rf_sr_tcb_ctes_array_assertion rf_sr_tcb_ctes_array_assertion2
|
||||
| erule array_assertion_shrink_right | simp)+
|
||||
done
|
||||
|
||||
lemma array_assertion_abs_tcb_ctes_add:
|
||||
"\<forall>s s'. (s, s') \<in> rf_sr \<and> tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s
|
||||
\<and> (n s' \<ge> 0 \<and> (case strong of True \<Rightarrow> n s' + 1 | False \<Rightarrow> n s') \<le> uint tcbCNodeEntries)
|
||||
\<longrightarrow> ptr_add_assertion (cte_Ptr (ptr_val (tcb s') && 0xFFFFFE00)) (n s')
|
||||
strong (hrs_htd (t_hrs_' (globals s')))"
|
||||
apply (clarsimp, drule(1) rf_sr_tcb_ctes_array_assertion)
|
||||
apply (simp add: ptr_add_assertion_positive, rule disjCI2)
|
||||
apply (erule array_assertion_shrink_right)
|
||||
apply (cases strong, simp_all add: unat_def)
|
||||
done
|
||||
|
||||
lemma array_assertion_abs_to_const:
|
||||
"\<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s'
|
||||
\<longrightarrow> (Suc 0 = 0 \<or> array_assertion (ptr s s') (n s s') (htd s s'))
|
||||
|
|
@ -1797,115 +1718,15 @@ lemmas ccorres_move_array_assertions
|
|||
ccorres_move_Guard_Seq[OF array_assertion_abs_to_const]
|
||||
ccorres_move_Guard[OF array_assertion_abs_to_const]
|
||||
|
||||
lemmas ccorres_move_array_assertion_tcb_ctes [corres_pre]
|
||||
= ccorres_move_array_assertions [OF array_assertion_abs_tcb_ctes(1)]
|
||||
ccorres_move_array_assertions [OF array_assertion_abs_tcb_ctes(2)]
|
||||
ccorres_move_Guard_Seq[OF array_assertion_abs_tcb_ctes_add]
|
||||
ccorres_move_Guard[OF array_assertion_abs_tcb_ctes_add]
|
||||
|
||||
lemma ptr_add_assertion_positive_helper:
|
||||
"n == m \<Longrightarrow> 0 \<le> sint m \<Longrightarrow> 0 \<le> sint n"
|
||||
by simp
|
||||
|
||||
lemma c_guard_abs_tcb_ctes:
|
||||
fixes p :: "cte_C ptr"
|
||||
shows "\<forall>s s'. (s, s') \<in> rf_sr \<and> tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s
|
||||
\<and> (n < ucast tcbCNodeEntries) \<longrightarrow> s' \<Turnstile>\<^sub>c cte_Ptr (((ptr_val (tcb s') && 0xFFFFFE00)
|
||||
+ n * 0x10))"
|
||||
apply (clarsimp)
|
||||
apply (rule c_guard_abs_cte[rule_format], intro conjI, simp_all)
|
||||
apply (simp add: cte_at'_obj_at', rule disjI2)
|
||||
apply (frule ptr_val_tcb_ptr_mask)
|
||||
apply (rule_tac x="n * 0x10" in bexI)
|
||||
apply (simp add: mask_def)
|
||||
apply (simp add: word_less_nat_alt tcbCNodeEntries_def tcb_cte_cases_def)
|
||||
apply (case_tac "unat n", simp_all add: unat_eq_of_nat, rename_tac n_rem)
|
||||
apply (case_tac "n_rem", simp_all add: unat_eq_of_nat, (rename_tac n_rem)?)+
|
||||
done
|
||||
|
||||
lemmas ccorres_move_c_guard_tcb_ctes [corres_pre] = ccorres_move_c_guards [OF c_guard_abs_tcb_ctes]
|
||||
|
||||
lemma cvariable_array_map_const_add_map_option:
|
||||
"cvariable_array_map_relation m (\<lambda>_. n)
|
||||
= cvariable_array_map_relation (map_option f o m) (\<lambda>_. n)"
|
||||
by (simp add: cvariable_array_map_relation_def fun_eq_iff)
|
||||
|
||||
lemma c_guard_abs_pte:
|
||||
"\<forall>s s'. (s, s') \<in> rf_sr \<and> pte_at' (ptr_val p) s \<and> True
|
||||
\<longrightarrow> s' \<Turnstile>\<^sub>c (p :: pte_C ptr)"
|
||||
apply (clarsimp simp: typ_at_to_obj_at_arches)
|
||||
apply (drule obj_at_ko_at', clarsimp)
|
||||
apply (erule cmap_relationE1[OF rf_sr_cpte_relation])
|
||||
apply (erule ko_at_projectKO_opt)
|
||||
apply (fastforce intro: typ_heap_simps)
|
||||
done
|
||||
|
||||
lemmas ccorres_move_c_guard_pte = ccorres_move_c_guards [OF c_guard_abs_pte]
|
||||
|
||||
lemma array_assertion_abs_pt:
|
||||
"\<forall>s s'. (s, s') \<in> rf_sr \<and> (page_table_at' pd s)
|
||||
\<and> (n s' \<le> 2 ^ (ptBits - 2) \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
|
||||
\<longrightarrow> (x s' = 0 \<or> array_assertion (pte_Ptr pd) (n s') (hrs_htd (t_hrs_' (globals s'))))"
|
||||
apply (intro allI impI disjCI2, clarsimp)
|
||||
apply (drule(1) page_table_at_rf_sr, clarsimp)
|
||||
apply (erule clift_array_assertion_imp, simp_all add: ptBits_def pageBits_def)
|
||||
apply (rule_tac x=0 in exI, simp)
|
||||
done
|
||||
|
||||
lemmas ccorres_move_array_assertion_pt
|
||||
= ccorres_move_array_assertions[OF array_assertion_abs_pt]
|
||||
|
||||
lemma c_guard_abs_pde:
|
||||
"\<forall>s s'. (s, s') \<in> rf_sr \<and> pde_at' (ptr_val p) s \<and> True
|
||||
\<longrightarrow> s' \<Turnstile>\<^sub>c (p :: pde_C ptr)"
|
||||
apply (clarsimp simp: typ_at_to_obj_at_arches)
|
||||
apply (drule obj_at_ko_at', clarsimp)
|
||||
apply (erule cmap_relationE1[OF rf_sr_cpde_relation])
|
||||
apply (erule ko_at_projectKO_opt)
|
||||
apply (fastforce intro: typ_heap_simps)
|
||||
done
|
||||
|
||||
lemmas ccorres_move_c_guard_pde = ccorres_move_c_guards [OF c_guard_abs_pde]
|
||||
|
||||
lemma array_assertion_abs_pd:
|
||||
"\<forall>s s'. (s, s') \<in> rf_sr \<and> (page_directory_at' pd s)
|
||||
\<and> (n s' \<le> 2 ^ (pdBits - 2) \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
|
||||
\<longrightarrow> (x s' = 0 \<or> array_assertion (pde_Ptr pd) (n s') (hrs_htd (t_hrs_' (globals s'))))"
|
||||
apply (intro allI impI disjCI2, clarsimp)
|
||||
apply (drule(1) page_directory_at_rf_sr, clarsimp)
|
||||
apply (erule clift_array_assertion_imp, simp_all add: pdBits_def pageBits_def)
|
||||
apply (rule_tac x=0 in exI, simp)
|
||||
done
|
||||
|
||||
lemmas ccorres_move_array_assertion_pd
|
||||
= ccorres_move_array_assertions[OF array_assertion_abs_pd]
|
||||
|
||||
lemma move_c_guard_ap:
|
||||
"\<forall>s s'. (s, s') \<in> rf_sr \<and> asid_pool_at' (ptr_val p) s \<and> True
|
||||
\<longrightarrow> s' \<Turnstile>\<^sub>c (p :: asid_pool_C ptr)"
|
||||
apply (clarsimp simp: typ_at_to_obj_at_arches)
|
||||
apply (drule obj_at_ko_at', clarsimp)
|
||||
apply (erule cmap_relationE1 [OF rf_sr_cpspace_asidpool_relation])
|
||||
apply (erule ko_at_projectKO_opt)
|
||||
apply (fastforce intro: typ_heap_simps)
|
||||
done
|
||||
|
||||
lemmas ccorres_move_c_guard_ap = ccorres_move_c_guards [OF move_c_guard_ap]
|
||||
|
||||
lemma array_assertion_abs_irq:
|
||||
"\<forall>s s'. (s, s') \<in> rf_sr \<and> True
|
||||
\<and> (n s' \<le> 256 \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
|
||||
\<longrightarrow> (x s' = 0 \<or> array_assertion (intStateIRQNode_' (globals s'))
|
||||
(n s') (hrs_htd (t_hrs_' (globals s'))))"
|
||||
apply (intro allI impI disjCI2)
|
||||
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
|
||||
apply (clarsimp simp: h_t_valid_clift_Some_iff)
|
||||
apply (erule clift_array_assertion_imp, (simp add: exI[where x=0])+)
|
||||
done
|
||||
|
||||
lemmas ccorres_move_array_assertion_irq
|
||||
= ccorres_move_array_assertions [OF array_assertion_abs_irq]
|
||||
|
||||
lemma ccorres_move_const_guard:
|
||||
"ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m c
|
||||
\<Longrightarrow> ccorres_underlying rf_sr Gamm rrel xf arrel axf
|
||||
|
|
|
|||
Loading…
Reference in New Issue