kings-crown/FVELER_Isabelle huggingface dataset:
theory Ctac_lemmas_C

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> rf_sr \<and> cte_wp_at' (\<lambda>_. True) (ptr_val p) s \<and> True \<longrightarrow> s' \<Turnstile>\<^sub>c p proof (prove)
goal (1 subgoal):
 1. \<And>x. p = cte_Ptr x \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> cte_wp_at' (\<lambda>_. True) (ptr_val p) s \<and> True \<longrightarrow> s' \<Turnstile>\<^sub>c p proof (prove)
goal (1 subgoal):
 1. \<And>x s s' cte. \<lbrakk>p = cte_Ptr x; (s, s') \<in> rf_sr; ctes_of s x = Some cte\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c cte_Ptr x proof (prove)
goal (1 subgoal):
 1. \<And>x s s' cte cte' ctel'. \<lbrakk>p = cte_Ptr x; (s, s') \<in> rf_sr; ctes_of s x = Some (cte_to_H ctel'); cslift s' (cte_Ptr x) = Some cte'; cte_lift cte' = Some ctel'; cte = cte_to_H ctel'; cl_valid_cte ctel'\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c cte_Ptr x proof (prove)
goal:
No subgoals!
theory Ctac_lemmas_C

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>gsCNodes s p = Some n; cte_array_relation s cstate\<rbrakk> \<Longrightarrow> array_assertion (cte_Ptr p) (2 ^ n) (hrs_htd (t_hrs_' cstate)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>gsCNodes s p = Some n; cte_array_relation s cstate\<rbrakk> \<Longrightarrow> h_t_array_valid (hrs_htd (t_hrs_' cstate)) (cte_Ptr p) (2 ^ n)
 2. \<lbrakk>gsCNodes s p = Some n; cte_array_relation s cstate\<rbrakk> \<Longrightarrow> 0 < 2 ^ n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>gsCNodes s p = Some n; cte_array_relation s cstate\<rbrakk> \<Longrightarrow> 0 < 2 ^ n proof (prove)
goal:
No subgoals!
theory Ctac_lemmas_C

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' tcb s; array_assertion (cte_Ptr (ptr_val (tcb_ptr_to_ctcb_ptr tcb) && 0xFFFFFE00)) (unat tcbCNodeEntries) (hrs_htd (t_hrs_' (globals s')))\<rbrakk> \<Longrightarrow> array_assertion (cte_Ptr tcb) (unat tcbCNodeEntries) (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal:
No subgoals!
theory Ctac_lemmas_C

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') && ~~mask tcbBlockSizeBits)) (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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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::'a) \<or> array_assertion (cte_Ptr (ptr_val (tcb s') && ~~ mask tcbBlockSizeBits)) (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::'a) \<or> array_assertion (cte_Ptr tcb') (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>x s' \<noteq> (0::'a); (s, s') \<in> rf_sr; tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s; n s' \<le> unat tcbCNodeEntries\<rbrakk> \<Longrightarrow> array_assertion (cte_Ptr (ptr_val (tcb s') && ~~ mask tcbBlockSizeBits)) (n s') (hrs_htd (t_hrs_' (globals s')))
 2. \<And>s s'. \<lbrakk>x s' \<noteq> (0::'a); (s, s') \<in> rf_sr; tcb_at' tcb' s; n s' \<le> unat tcbCNodeEntries\<rbrakk> \<Longrightarrow> array_assertion (cte_Ptr tcb') (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal:
No subgoals!
theory Ctac_lemmas_C

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') && ~~mask tcbBlockSizeBits)) (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 del: nat_uint_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> rf_sr \<and> tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s \<and> 0 \<le> n s' \<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') && ~~ mask tcbBlockSizeBits)) (n s') strong (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s; 0 \<le> n s'; (case strong of True \<Rightarrow> n s' + 1 | False \<Rightarrow> n s') \<le> uint tcbCNodeEntries; array_assertion (cte_Ptr (ptr_val (tcb s') && ~~ mask tcbBlockSizeBits)) (unat tcbCNodeEntries) (hrs_htd (t_hrs_' (globals s')))\<rbrakk> \<Longrightarrow> ptr_add_assertion (cte_Ptr (ptr_val (tcb s') && ~~ mask tcbBlockSizeBits)) (n s') strong (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s; 0 \<le> n s'; (case strong of True \<Rightarrow> n s' + 1 | False \<Rightarrow> n s') \<le> uint tcbCNodeEntries; array_assertion (cte_Ptr (ptr_val (tcb s') && ~~ mask tcbBlockSizeBits)) (unat tcbCNodeEntries) (hrs_htd (t_hrs_' (globals s'))); n s' \<noteq> 0\<rbrakk> \<Longrightarrow> array_assertion (cte_Ptr (ptr_val (tcb s') && ~~ mask tcbBlockSizeBits)) (case strong of True \<Rightarrow> Suc (nat (n s')) | False \<Rightarrow> nat (n s')) (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s; 0 \<le> n s'; (case strong of True \<Rightarrow> n s' + 1 | False \<Rightarrow> n s') \<le> uint tcbCNodeEntries; n s' \<noteq> 0\<rbrakk> \<Longrightarrow> (case strong of True \<Rightarrow> Suc (nat (n s')) | False \<Rightarrow> nat (n s')) \<le> unat tcbCNodeEntries proof (prove)
goal:
No subgoals!
theory Ctac_lemmas_C

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: pd_bits_def pt_bits_def ptBits_def pteBits_def) apply (rule_tac x=0 in exI, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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::'a) \<longrightarrow> n s' \<noteq> 0) \<longrightarrow> x s' = (0::'a) \<or> array_assertion (pte_Ptr pd) (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>x s' \<noteq> (0::'a); (s, s') \<in> rf_sr; page_table_at' pd s; n s' \<le> 2 ^ (ptBits - 2); 0 < n s'\<rbrakk> \<Longrightarrow> array_assertion (pte_Ptr pd) (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' y. \<lbrakk>x s' \<noteq> (0::'a); (s, s') \<in> rf_sr; n s' \<le> 2 ^ (ptBits - 2); 0 < n s'; cslift s' (pt_Ptr pd) = Some y\<rbrakk> \<Longrightarrow> array_assertion (pte_Ptr pd) (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>x s' \<noteq> (0::'a); (s, s') \<in> rf_sr; n s' \<le> 256; 0 < n s'\<rbrakk> \<Longrightarrow> \<exists>i. word_of_nat i * 4 = 0 \<and> i + n s' \<le> 256 proof (prove)
goal:
No subgoals!
theory Ctac_lemmas_C

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> rf_sr \<and> pde_at' (ptr_val p) s \<and> True \<longrightarrow> s' \<Turnstile>\<^sub>c p proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; obj_at' (\<lambda>_. True) (ptr_val p) s\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p proof (prove)
goal (1 subgoal):
 1. \<And>s s' ko. \<lbrakk>(s, s') \<in> rf_sr; ko_at' ko (ptr_val p) s\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p proof (prove)
goal (2 subgoals):
 1. \<And>s s' ko. ko_at' ko (ptr_val p) s \<Longrightarrow> map_to_pdes (ksPSpace s) (?x10 s s' ko) = Some (?y10 s s' ko)
 2. \<And>s s' ko y'. \<lbrakk>ko_at' ko (ptr_val p) s; map_to_pdes (ksPSpace s) (?x10 s s' ko) = Some (?y10 s s' ko); cpde_relation (?y10 s s' ko) y'; cslift s' (pde_Ptr (?x10 s s' ko)) = Some y'\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p proof (prove)
goal (1 subgoal):
 1. \<And>s s' ko y'. \<lbrakk>ko_at' ko (ptr_val p) s; map_to_pdes (ksPSpace s) (ptr_val p) = Some ko; cpde_relation ko y'; cslift s' (pde_Ptr (ptr_val p)) = Some y'\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p proof (prove)
goal:
No subgoals!
theory Ctac_lemmas_C

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 pdeBits_def) apply (rule_tac x=0 in exI, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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::'a) \<longrightarrow> n s' \<noteq> 0) \<longrightarrow> x s' = (0::'a) \<or> array_assertion (pde_Ptr pd) (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>x s' \<noteq> (0::'a); (s, s') \<in> rf_sr; page_directory_at' pd s; n s' \<le> 2 ^ (pdBits - 2); 0 < n s'\<rbrakk> \<Longrightarrow> array_assertion (pde_Ptr pd) (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' y. \<lbrakk>x s' \<noteq> (0::'a); (s, s') \<in> rf_sr; n s' \<le> 2 ^ (pdBits - 2); 0 < n s'; cslift s' (pd_Ptr pd) = Some y\<rbrakk> \<Longrightarrow> array_assertion (pde_Ptr pd) (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>x s' \<noteq> (0::'a); (s, s') \<in> rf_sr; n s' \<le> 4096; 0 < n s'\<rbrakk> \<Longrightarrow> \<exists>i. word_of_nat i * 4 = 0 \<and> i + n s' \<le> 4096 proof (prove)
goal:
No subgoals!
theory Ctac_lemmas_C

lemma ccorres_Guard_intStateIRQNode_array_Ptr_Seq:
  assumes "ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C hs a (c;; d)"
  shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C hs a (Guard F {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} c;; d)" by (rule ccorres_guard_imp2[OF ccorres_move_Guard_Seq[where P=\<top> and P'=\<top>, OF _ assms]]
      ; simp add: rf_sr_def cstate_relation_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C hs a (Guard F {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} c;;
d)
theory Ctac_lemmas_C

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>gsCNodes s p = Some n; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> array_assertion (cte_Ptr p) (2 ^ n) (hrs_htd (t_hrs_' (globals s')))
theory CSpaceAcc_C

lemma getCurThread_sp:
  "\<lbrace>P\<rbrace> getCurThread \<lbrace>\<lambda>rv s. ksCurThread s = rv \<and> P s\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getCurThread \<lbrace>\<lambda>rv s. ksCurThread s = rv \<and> P s\<rbrace>
theory CSpaceAcc_C

lemma rf_sr_ksCurThread:
  "(s, s') \<in> rf_sr \<Longrightarrow> ksCurThread_' (globals s')
                       = tcb_ptr_to_ctcb_ptr (ksCurThread s)" by (clarsimp simp: rf_sr_def cstate_relation_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> rf_sr \<Longrightarrow> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s)
theory CSpaceAcc_C

lemma getSchedulerAction_sp:
  "\<lbrace>P\<rbrace> getSchedulerAction \<lbrace>\<lambda>rv s. ksSchedulerAction s = rv \<and> P s\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getSchedulerAction \<lbrace>\<lambda>rv s. ksSchedulerAction s = rv \<and> P s\<rbrace>
theory CSpaceAcc_C

lemma rf_sr_ksDomainTime:
  "(s, s') \<in> rf_sr \<Longrightarrow> ksDomainTime_' (globals s') = ksDomainTime s" by (clarsimp simp: rf_sr_def cstate_relation_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> rf_sr \<Longrightarrow> ksDomainTime_' (globals s') = ksDomainTime s
theory CSpaceAcc_C

lemma rf_sr_ksIdleThread:
  "(s, s') \<in> rf_sr \<Longrightarrow> ksIdleThread_' (globals s')
                       = tcb_ptr_to_ctcb_ptr (ksIdleThread s)" by (clarsimp simp: rf_sr_def cstate_relation_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> rf_sr \<Longrightarrow> ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s)
theory CSpaceAcc_C

lemma curDomain_sp:
  "\<lbrace>P\<rbrace> curDomain \<lbrace>\<lambda>rv s. ksCurDomain s = rv \<and> P s\<rbrace>" apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> curDomain \<lbrace>\<lambda>rv s. ksCurDomain s = rv \<and> P s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> ksCurDomain s = ksCurDomain s \<and> P s proof (prove)
goal:
No subgoals!
theory CSpaceAcc_C

lemma getSlotCap_pre_cte_at:
  "\<lbrace>\<lambda>s. \<not> cte_at' p s \<rbrace> getSlotCap p \<lbrace> \<lambda>_ _. False \<rbrace>" unfolding getSlotCap_def apply simp apply (wp getCTE_wp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at' (\<lambda>_. True) p s\<rbrace> getSlotCap p \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at' (\<lambda>_. True) p s\<rbrace> do cte <- getCTE p;
return $ cteCap cte
od \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at' (\<lambda>_. True) p s\<rbrace> do cte <- getCTE p;
return (cteCap cte)
od \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> cte_wp_at' (\<lambda>_. True) p s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p s \<and> False) proof (prove)
goal:
No subgoals!
theory CSpaceAcc_C

lemma array_assertion_abs_cnode_ctes:
  "\<forall>s s'. (s, s') \<in> rf_sr \<and> (\<exists>n. gsCNodes s p = Some n \<and> n' \<le> 2 ^ n) \<and> True
    \<longrightarrow> (x s' = 0 \<or> array_assertion (cte_Ptr p) n' (hrs_htd (t_hrs_' (globals s'))))" apply (clarsimp, drule(1) rf_sr_gsCNodes_array_assertion) apply (metis array_assertion_shrink_right) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> rf_sr \<and> (\<exists>n. gsCNodes s p = Some n \<and> n' \<le> 2 ^ n) \<and> True \<longrightarrow> x s' = (0::'a) \<or> array_assertion (cte_Ptr p) n' (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' n. \<lbrakk>(s, s') \<in> rf_sr; n' \<le> 2 ^ n; \<not> array_assertion (cte_Ptr p) n' (hrs_htd (t_hrs_' (globals s'))); array_assertion (cte_Ptr p) (2 ^ n) (hrs_htd (t_hrs_' (globals s')))\<rbrakk> \<Longrightarrow> x s' = (0::'a) proof (prove)
goal:
No subgoals!
theory CSpace_RAB_C

lemma not_snd_bindE_I1:
  "\<not> snd ((a >>=E b) s) \<Longrightarrow> \<not> snd (a s)" unfolding bindE_def by (erule not_snd_bindI1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> snd ((a >>=E b) s) \<Longrightarrow> \<not> snd (a s) proof (prove)
goal (1 subgoal):
 1. \<not> snd ((a >>= Nondet_Monad.lift b) s) \<Longrightarrow> \<not> snd (a s)
theory CSpace_RAB_C

lemma ccorres_gen_asm_state:
  assumes rl: "\<And>s. P s \<Longrightarrow> ccorres r xf G G' hs a c"
  shows "ccorres r xf (G and P) G' hs a c" proof (rule ccorres_guard_imp2) show "ccorres r xf (G and (\<lambda>_. \<exists>s. P s)) G' hs a c" apply (rule ccorres_gen_asm) apply (erule exE) apply (erule rl) done next fix s s' assume "(s, s') \<in> rf_sr" and "(G and P) s" and "s' \<in> G'" thus "(G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G'" by (clarsimp elim!: exI) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf (G and P) G' hs a c proof (state)
goal (2 subgoals):
 1. ccorres r xf ?Q ?Q' hs a c
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (G and P) s; s' \<in> G'\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (1 subgoal):
 1. ccorres r xf (G and (\<lambda>_. \<exists>s. P s)) G' hs a c proof (prove)
goal (1 subgoal):
 1. \<exists>s. P s \<Longrightarrow> ccorres r xf G G' hs a c proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> ccorres r xf G G' hs a c proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres r xf (G and (\<lambda>_. \<exists>s. P s)) G' hs a c

goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (G and P) s; s' \<in> G'\<rbrakk> \<Longrightarrow> (G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G' proof (state)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (G and P) s; s' \<in> G'\<rbrakk> \<Longrightarrow> (G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G' proof (state)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (G and P) s; s' \<in> G'\<rbrakk> \<Longrightarrow> (G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G' proof (state)
this:
(s, s') \<in> rf_sr
(G and P) s
s' \<in> G'

goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (G and P) s; s' \<in> G'\<rbrakk> \<Longrightarrow> (G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G' proof (prove)
using this:
(s, s') \<in> rf_sr
(G and P) s
s' \<in> G'

goal (1 subgoal):
 1. (G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G' proof (state)
this:
(G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G'

goal:
No subgoals!
theory CSpace_RAB_C

lemma rightsFromWord_wordFromRights:
  "rightsFromWord (wordFromRights rghts) = rghts" apply (cases rghts) apply (simp add: wordFromRights_def rightsFromWord_def
            split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rightsFromWord (wordFromRights rghts) = rghts proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. rghts = CapRights x1 x2 x3 x4 \<Longrightarrow> rightsFromWord (wordFromRights rghts) = rghts proof (prove)
goal:
No subgoals!
theory CSpace_RAB_C

lemma wordFromRights_inj:
  "inj wordFromRights" by (rule inj_on_inverseI, rule rightsFromWord_wordFromRights)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj wordFromRights
theory CSpace_RAB_C

lemma rightsFromWord_spec:
  shows "\<forall>s. \<Gamma> \<turnstile> {s} \<acute>ret__struct_seL4_CapRights_C :== PROC rightsFromWord(\<acute>w)
  \<lbrace>seL4_CapRights_lift \<acute>ret__struct_seL4_CapRights_C = cap_rights_from_word_canon \<^bsup>s\<^esup>w \<rbrace>" apply vcg apply (simp add: seL4_CapRights_lift_def nth_shiftr mask_shift_simps nth_shiftr
                   cap_rights_from_word_canon_def word_and_1 eval_nat_numeral
                   word_sless_def word_sle_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call rightsFromWord_'proc \<lbrace>seL4_CapRights_lift \<acute>ret__struct_seL4_CapRights_C = cap_rights_from_word_canon \<^bsup>s\<^esup>w\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>w. \<forall>v. 0 <s 1 \<and> 0 \<le>s 0 \<and> seL4_CapRights_lift (seL4_CapRights_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (UCAST(32 \<rightarrow> 32) w)) v) = cap_rights_from_word_canon w proof (prove)
goal:
No subgoals!
theory CSpace_RAB_C

lemma cap_rights_to_H_from_word_canon [simp]:
  "cap_rights_to_H (cap_rights_from_word_canon wd) = rightsFromWord wd" unfolding cap_rights_from_word_def rightsFromWord_def apply (simp add: cap_rights_from_word_canon_def) apply (simp add: cap_rights_to_H_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_rights_to_H (cap_rights_from_word_canon wd) = rightsFromWord wd proof (prove)
goal (1 subgoal):
 1. cap_rights_to_H (cap_rights_from_word_canon wd) = CapRights (wd !! 0) (wd !! 1) (wd !! 2) (wd !! 3) proof (prove)
goal (1 subgoal):
 1. cap_rights_to_H \<lparr>capAllowGrantReply_CL = from_bool (wd !! 3), capAllowGrant_CL = from_bool (wd !! 2), capAllowRead_CL = from_bool (wd !! Suc 0), capAllowWrite_CL = from_bool (wd !! 0)\<rparr> = CapRights (wd !! 0) (wd !! Suc 0) (wd !! 2) (wd !! 3) proof (prove)
goal:
No subgoals!