kings-crown/FVELER_Isabelle huggingface dataset:
theory Arch_DR

lemma select_ret_or_throw_twiceE:
  "(doE _ \<leftarrow> select_ret_or_throw S X; select_ret_or_throw S X odE)
    = select_ret_or_throw S X" apply (simp add: select_ret_or_throw_def alternative_def returnOk_def return_def
                       select_def bind_def throwError_def Sigma_def
                       bindE_def) apply (rule ext, auto simp: throwError_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doE _ <- select_ret_or_throw S X;
select_ret_or_throw S X
odE = select_ret_or_throw S X proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. ((if S = {} then {} else (\<Union>x\<in>S. {(Inr x, s)}) \<union> (\<Union>x\<in>S. \<Union>x\<in>X. {(Inl x, s)})) \<union> (\<Union>x\<in>X. {(Inl x, s)}), \<exists>x\<in>(\<Union>x\<in>S. {(Inr x, s)}) \<union> (\<Union>x\<in>X. {(Inl x, s)}). snd (case x of (x, xa) \<Rightarrow> lift (\<lambda>_ s. ((\<Union>x\<in>S. {(Inr x, s)}) \<union> (\<Union>x\<in>X. {(Inl x, s)}), False)) x xa))) = (\<lambda>s. ((\<Union>x\<in>S. {(Inr x, s)}) \<union> (\<Union>x\<in>X. {(Inl x, s)}), False)) proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma corres_initial_bindE_rdonly_select_ret_or_throw:
  assumes y: "\<And>rv'. corres_underlying sr nf nf' (e \<oplus> r) P P' (select_ret_or_throw S X) (d rv')"
  assumes x: "corres_underlying sr nf nf' (e \<oplus> dc) P P' (select_ret_or_throw S X) c"
  assumes z: "\<lbrace>P'\<rbrace> c \<lbrace>\<lambda>_. P'\<rbrace>,-"
  shows      "corres_underlying sr nf nf' (e \<oplus> r) P P' (select_ret_or_throw S X) (c >>=E (\<lambda>rv'. d rv'))" apply (subst select_ret_or_throw_twiceE[symmetric]) apply (rule corres_initial_splitE[OF x y]) apply wp apply (wp z) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (e \<oplus> r) P P' (select_ret_or_throw S X) (c >>=E d) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (e \<oplus> r) P P' (doE _ <- select_ret_or_throw S X;
select_ret_or_throw S X
odE) (c >>=E d) proof (prove)
goal (2 subgoals):
 1. \<lbrace>P\<rbrace> select_ret_or_throw S X \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 2. \<lbrace>P'\<rbrace> c \<lbrace>\<lambda>rv'. P'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P'\<rbrace> c \<lbrace>\<lambda>rv'. P'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma corres_select_ret_or_throw:
  "\<forall>v \<in> S'. \<exists>v' \<in> S. r v' v
    \<Longrightarrow> \<forall>x \<in> X'. \<exists>x' \<in> X. e x' x
    \<Longrightarrow> corres_underlying sr nf nf' (e \<oplus> r) \<top> \<top>
        (select_ret_or_throw S X) (select_ret_or_throw S' X')" apply (simp add: select_ret_or_throw_def) apply (rule corres_alternate_match) apply (simp add: returnOk_def liftM_def[symmetric] o_def) apply (rule corres_select, simp) apply (simp add: throwError_def liftM_def[symmetric] o_def) apply (rule corres_select, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>v\<in>S'. \<exists>v'\<in>S. r v' v; \<forall>x\<in>X'. \<exists>x'\<in>X. e x' x\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (e \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (select_ret_or_throw S X) (select_ret_or_throw S' X') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>v\<in>S'. \<exists>v'\<in>S. r v' v; \<forall>x\<in>X'. \<exists>x'\<in>X. e x' x\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (e \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (select S >>= returnOk \<sqinter> select X >>= throwError) (select S' >>= returnOk \<sqinter> select X' >>= throwError) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>v\<in>S'. \<exists>v'\<in>S. r v' v; \<forall>x\<in>X'. \<exists>x'\<in>X. e x' x\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (e \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (select S >>= returnOk) (select S' >>= returnOk)
 2. \<lbrakk>\<forall>v\<in>S'. \<exists>v'\<in>S. r v' v; \<forall>x\<in>X'. \<exists>x'\<in>X. e x' x\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (e \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (select X >>= throwError) (select X' >>= throwError) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>v\<in>S'. \<exists>v'\<in>S. r v' v; \<forall>x\<in>X'. \<exists>x'\<in>X. e x' x\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>_. True) (\<lambda>_. True) (select S) (select S')
 2. \<lbrakk>\<forall>v\<in>S'. \<exists>v'\<in>S. r v' v; \<forall>x\<in>X'. \<exists>x'\<in>X. e x' x\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (e \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (select X >>= throwError) (select X' >>= throwError) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>v\<in>S'. \<exists>v'\<in>S. r v' v; \<forall>x\<in>X'. \<exists>x'\<in>X. e x' x\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (e \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (select X >>= throwError) (select X' >>= throwError) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>v\<in>S'. \<exists>v'\<in>S. r v' v; \<forall>x\<in>X'. \<exists>x'\<in>X. e x' x\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' e (\<lambda>_. True) (\<lambda>_. True) (select X) (select X') proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma pde_unat_less_helper[simplified]:
  "unat ((p && mask pd_bits >> 2) :: word32) < 2 ^ 12" apply (rule unat_less_helper, simp only: word_unat_power[symmetric],
         rule shiftr_less_t2n) apply (rule order_less_le_trans, rule and_mask_less_size,
         simp_all add: pd_bits_def pageBits_def word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (p && mask pd_bits >> 2) < 2 ^ 12 proof (prove)
goal (1 subgoal):
 1. p && mask pd_bits < 2 ^ (2 + 12) proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma pde_opt_cap_eq:
  "\<lbrakk> ko_at (ArchObj (arch_kernel_obj.PageDirectory pd)) (x && ~~ mask pd_bits) s;
         valid_idle s \<rbrakk>
       \<Longrightarrow> opt_cap (transform_pd_slot_ref x) (transform s)
         = Some (transform_pde ((kernel_pde_mask pd) (ucast (x && mask pd_bits >> 2))))" apply (simp add: opt_cap_def transform_pd_slot_ref_def
                   slots_of_def transform_def
                   obj_at_def object_slots_def restrict_map_def map_add_def
                   transform_page_directory_contents_def transform_objects_def
                   unat_map_def ucast_nat_def
                   pde_unat_less_helper) apply (clarsimp simp: valid_idle_def st_tcb_at_def obj_at_def pred_tcb_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ako_at (arch_kernel_obj.PageDirectory pd) (x && ~~ mask pd_bits) s; valid_idle s\<rbrakk> \<Longrightarrow> opt_cap (transform_pd_slot_ref x) (transform s) = Some (transform_pde (kernel_pde_mask pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s (x && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); valid_idle s\<rbrakk> \<Longrightarrow> x && ~~ mask pd_bits \<noteq> idle_thread s proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma corres_add_noop_rhs:
  "corres_underlying sr fl fl' r P P' f (do _ \<leftarrow> return (); g od)
    \<Longrightarrow> corres_underlying sr fl fl' r P P' f g" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr fl fl' r P P' f (do _ <- return ();
g
od) \<Longrightarrow> corres_underlying sr fl fl' r P P' f g
theory Arch_DR

lemma gets_the_noop_dcorres:
  "dcorres dc (\<lambda>s. f s \<noteq> None) \<top> (gets_the f) (return x)" by (clarsimp simp: gets_the_def corres_underlying_def exec_gets
                     assert_opt_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>s. f s \<noteq> None) (\<lambda>_. True) (gets_the f) (return x)
theory Arch_DR

lemma dget_object_sp:
  "\<lbrace>P\<rbrace> KHeap_D.get_object p \<lbrace>\<lambda>r s. P s \<and> cdl_objects s p = Some r\<rbrace>" apply wp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> KHeap_D.get_object p \<lbrace>\<lambda>r s. P s \<and> cdl_objects s p = Some r\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> cdl_objects s p \<noteq> None \<longrightarrow> P s \<and> cdl_objects s p = Some (the (cdl_objects s p)) proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma set_cap_opt_cap:
  "\<lbrace>\<lambda>s. if slot = slot' then P (Some cap) else P (opt_cap slot s)\<rbrace>
  KHeap_D.set_cap slot' cap
  \<lbrace>\<lambda>uu s. P (opt_cap slot s)\<rbrace>" apply (wp set_cap_opt_cap') apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if slot = slot' then P (Some cap) else P (opt_cap slot s)\<rbrace> KHeap_D.set_cap slot' cap \<lbrace>\<lambda>uu s. P (opt_cap slot s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. if slot = slot' then P (Some cap) else P (opt_cap slot s) \<Longrightarrow> P (((\<lambda>p. opt_cap p s)(slot' \<mapsto> cap)) slot) proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma case_sum_eq: "case_sum a a x = a (case x of Inl a \<Rightarrow> a | Inr a \<Rightarrow> a)" apply (case_tac x) apply (clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case x of Inl x \<Rightarrow> a x | Inr x \<Rightarrow> a x) = a (case x of Inl a \<Rightarrow> a | Inr a \<Rightarrow> a) proof (prove)
goal (2 subgoals):
 1. \<And>aa. x = Inl aa \<Longrightarrow> (case x of Inl x \<Rightarrow> a x | Inr x \<Rightarrow> a x) = a (case x of Inl a \<Rightarrow> a | Inr a \<Rightarrow> a)
 2. \<And>b. x = Inr b \<Longrightarrow> (case x of Inl x \<Rightarrow> a x | Inr x \<Rightarrow> a x) = a (case x of Inl a \<Rightarrow> a | Inr a \<Rightarrow> a) proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma ucast_add:
  " len_of TYPE('a) \<le> len_of TYPE('b)
   \<Longrightarrow> (ucast (a + b) :: (('a::len)word)) = ucast (a :: (('b ::len) word)) + (ucast b)" apply (rule word_unat.Rep_eqD) apply (simp add:unat_ucast unat_word_ariths mod_mod_power min_def mod_add_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> UCAST('b \<rightarrow> 'a) (a + b) = UCAST('b \<rightarrow> 'a) a + UCAST('b \<rightarrow> 'a) b proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> unat (UCAST('b \<rightarrow> 'a) (a + b)) = unat (UCAST('b \<rightarrow> 'a) a + UCAST('b \<rightarrow> 'a) b) proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma cleanL2Range_underlying_memory[wp]:
  "cleanL2Range word3 w \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace>" by (clarsimp simp: cleanL2Range_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanL2Range word3 w \<lbrace>\<lambda>_ ms. underlying_memory ms = m\<rbrace>
theory Arch_DR

lemma invalidateL2Range_underlying_memory[wp]:
  "invalidateL2Range word3 w \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace>" by (clarsimp simp: invalidateL2Range_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateL2Range word3 w \<lbrace>\<lambda>_ ms. underlying_memory ms = m\<rbrace>
theory Arch_DR

lemma cleanInvalidateL2Range_underlying_memory[wp]:
  "cleanInvalidateL2Range word3 w \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace>" by (clarsimp simp: cleanInvalidateL2Range_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanInvalidateL2Range word3 w \<lbrace>\<lambda>_ ms. underlying_memory ms = m\<rbrace>
theory Arch_DR

lemma cleanByVA_underlying_memory[wp]:
  "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanByVA a b \<lbrace>\<lambda>y ms. underlying_memory ms = m\<rbrace>" by (clarsimp simp: cleanByVA_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanByVA a b \<lbrace>\<lambda>y ms. underlying_memory ms = m\<rbrace>
theory Arch_DR

lemma invalidateByVA_underlying_memory[wp]:
  "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateByVA a b \<lbrace>\<lambda>y ms. underlying_memory ms = m\<rbrace>" by (clarsimp simp: invalidateByVA_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateByVA a b \<lbrace>\<lambda>y ms. underlying_memory ms = m\<rbrace>
theory Arch_DR

lemma invalidateByVA_I_underlying_memory[wp]:
  "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateByVA_I a b \<lbrace>\<lambda>y ms. underlying_memory ms = m\<rbrace>" by (clarsimp simp: invalidateByVA_I_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateByVA_I a b \<lbrace>\<lambda>y ms. underlying_memory ms = m\<rbrace>
theory Arch_DR

lemma cleanInvalByVA_underlying_memory[wp]:
  "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanInvalByVA a b \<lbrace>\<lambda>y ms. underlying_memory ms = m\<rbrace>" by (clarsimp simp: cleanInvalByVA_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanInvalByVA a b \<lbrace>\<lambda>y ms. underlying_memory ms = m\<rbrace>
theory Arch_DR

lemma cleanCacheRange_PoC_underlying_memory[wp]:
  "cleanCacheRange_PoC word1 word2 word3 \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace>" by (clarsimp simp: cleanCacheRange_PoC_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanCacheRange_PoC word1 word2 word3 \<lbrace>\<lambda>_ ms. underlying_memory ms = m\<rbrace>
theory Arch_DR

lemma cleanCacheRange_RAM_underlying_memory[wp]:
  "cleanCacheRange_RAM word1 word2 word3 \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace>" by (clarsimp simp: cleanCacheRange_RAM_def,wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanCacheRange_RAM word1 word2 word3 \<lbrace>\<lambda>_ ms. underlying_memory ms = m\<rbrace>
theory Arch_DR

lemma branchFlush_underlying_memory[wp]:
  "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> branchFlush a b \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" by (clarsimp simp: branchFlush_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> branchFlush a b \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
theory Arch_DR

lemma branchFlushRange_underlying_memory[wp]:
  "branchFlushRange word1 word2 word3 \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace>" by (clarsimp simp: branchFlushRange_def,wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> branchFlushRange word1 word2 word3 \<lbrace>\<lambda>_ ms. underlying_memory ms = m\<rbrace>
theory Arch_DR

lemma invalidateCacheRange_RAM_underlying_memory[wp]:
  "invalidateCacheRange_RAM word1 word2 word3 \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace>" by (clarsimp simp: invalidateCacheRange_RAM_def, wp, clarsimp, wp, clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateCacheRange_RAM word1 word2 word3 \<lbrace>\<lambda>_ ms. underlying_memory ms = m\<rbrace>
theory Arch_DR

lemma invalidateCacheRange_I_underlying_memory[wp]:
  "invalidateCacheRange_I word1 word2 word3 \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace>" by (clarsimp simp: invalidateCacheRange_I_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateCacheRange_I word1 word2 word3 \<lbrace>\<lambda>_ ms. underlying_memory ms = m\<rbrace>
theory Arch_DR

lemma cleanInvalidateCacheRange_RAM_underlying_memory[wp]:
  "cleanInvalidateCacheRange_RAM word1 word2 word3 \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace>" by (clarsimp simp: cleanInvalidateCacheRange_RAM_def,wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanInvalidateCacheRange_RAM word1 word2 word3 \<lbrace>\<lambda>_ ms. underlying_memory ms = m\<rbrace>
theory Arch_DR

lemma isb_underlying_memory[wp]:
  "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> isb \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" by (clarsimp simp: isb_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> isb \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
theory Arch_DR

lemma do_flush_underlying_memory[wp]:
  "do_flush flush_type word1 word2 word3 \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace>" unfolding do_flush_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> do_flush flush_type word1 word2 word3 \<lbrace>\<lambda>_ ms. underlying_memory ms = m\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> case flush_type of flush_type.Clean \<Rightarrow> cleanCacheRange_RAM word1 word2 word3 | flush_type.Invalidate \<Rightarrow> invalidateCacheRange_RAM word1 word2 word3 | flush_type.CleanInvalidate \<Rightarrow> cleanInvalidateCacheRange_RAM word1 word2 word3 | flush_type.Unify \<Rightarrow> do cleanCacheRange_PoU word1 word2 word3;
dsb;
invalidateCacheRange_I word1 word2 word3;
branchFlushRange word1 word2 word3;
isb
od \<lbrace>\<lambda>_ ms. underlying_memory ms = m\<rbrace>
theory Arch_DR

lemma pte_check_if_mapped_corres:
  "dcorres dc \<top> \<top> (return a) (pte_check_if_mapped pte)" apply (clarsimp simp add: pte_check_if_mapped_def get_master_pte_def get_pte_def get_pt_def
                            bind_assoc in_monad get_object_def corres_underlying_def return_def) apply (case_tac y; simp add: in_monad) by (simp add: get_pte_def get_pt_def get_object_def in_monad bind_assoc
         split: pte.splits kernel_object.splits arch_kernel_obj.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return a) (pte_check_if_mapped pte) proof (prove)
goal (1 subgoal):
 1. \<And>b ba y s'' x pt. \<lbrakk>kheap b ((pte && ~~ mask 6) && ~~ mask pt_bits) = Some y; (x, s'') \<in> fst ((case y of ArchObj (arch_kernel_obj.PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) b); (pt, ba) \<in> fst ((case x (UCAST(32 \<rightarrow> 8) ((pte && ~~ mask 6) && mask pt_bits >> 2)) of LargePagePTE xa xaa xb \<Rightarrow> return (x (UCAST(32 \<rightarrow> 8) ((pte && ~~ mask 6) && mask pt_bits >> 2))) | _ \<Rightarrow> get_pte pte) s'')\<rbrakk> \<Longrightarrow> transform ba = transform b proof (prove)
goal (1 subgoal):
 1. \<And>b ba y s'' x pt x5. \<lbrakk>kheap b ((pte && ~~ mask 6) && ~~ mask pt_bits) = Some (ArchObj x5); (x, s'') \<in> fst ((case x5 of arch_kernel_obj.PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) b); (pt, ba) \<in> fst ((case x (UCAST(32 \<rightarrow> 8) ((pte && ~~ mask 6) && mask pt_bits >> 2)) of LargePagePTE xa xaa xb \<Rightarrow> return (x (UCAST(32 \<rightarrow> 8) ((pte && ~~ mask 6) && mask pt_bits >> 2))) | _ \<Rightarrow> get_pte pte) s''); y = ArchObj x5\<rbrakk> \<Longrightarrow> transform ba = transform b
theory Arch_DR

lemma pde_check_if_mapped_corres:
  "dcorres dc \<top> \<top> (return a) (pde_check_if_mapped pde)" apply (clarsimp simp add: pde_check_if_mapped_def get_master_pde_def get_pde_def get_pd_def
                            in_monad get_object_def corres_underlying_def return_def) apply (case_tac y; simp add: in_monad) by (simp add: get_pde_def get_pd_def get_object_def in_monad bind_assoc
         split: pde.splits kernel_object.splits arch_kernel_obj.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return a) (pde_check_if_mapped pde) proof (prove)
goal (1 subgoal):
 1. \<And>b ba y pd s'' pda. \<lbrakk>kheap b ((pde && ~~ mask 6) && ~~ mask pd_bits) = Some y; (pd, ba) \<in> fst ((case pda (UCAST(32 \<rightarrow> 12) ((pde && ~~ mask 6) && mask pd_bits >> 2)) of SuperSectionPDE x xa xb \<Rightarrow> return (pda (UCAST(32 \<rightarrow> 12) ((pde && ~~ mask 6) && mask pd_bits >> 2))) | _ \<Rightarrow> get_pde pde) s''); (pda, s'') \<in> fst ((case y of ArchObj (arch_kernel_obj.PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) b)\<rbrakk> \<Longrightarrow> transform ba = transform b proof (prove)
goal (1 subgoal):
 1. \<And>b ba y pd s'' pda x5. \<lbrakk>kheap b ((pde && ~~ mask 6) && ~~ mask pd_bits) = Some (ArchObj x5); (pd, ba) \<in> fst ((case pda (UCAST(32 \<rightarrow> 12) ((pde && ~~ mask 6) && mask pd_bits >> 2)) of SuperSectionPDE x xa xb \<Rightarrow> return (pda (UCAST(32 \<rightarrow> 12) ((pde && ~~ mask 6) && mask pd_bits >> 2))) | _ \<Rightarrow> get_pde pde) s''); (pda, s'') \<in> fst ((case x5 of arch_kernel_obj.PageDirectory x \<Rightarrow> return x | _ \<Rightarrow> fail) b); y = ArchObj x5\<rbrakk> \<Longrightarrow> transform ba = transform b
theory Arch_DR

lemma if_invalidate_equiv_return:
  "dcorres dc \<top> \<top> (return a) (if b then invalidate_tlb_by_asid asid else return ())" apply (cases b, simp_all) apply (rule wp_to_dcorres) apply (wp invalidate_tlb_by_asid_dwp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return a) (if b then invalidate_tlb_by_asid asid else return ()) proof (prove)
goal (1 subgoal):
 1. b \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return a) (invalidate_tlb_by_asid asid) proof (prove)
goal (1 subgoal):
 1. \<And>cs. b \<Longrightarrow> \<lbrace>\<lambda>s. True \<and> transform s = cs\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cs s. \<lbrakk>b; True \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma ct_active_not_idle_etc:
  "\<lbrakk> invs s; ct_active s \<rbrakk> \<Longrightarrow> not_idle_thread (cur_thread s) s" apply (simp add: not_idle_thread_def ct_in_state_def) apply (subgoal_tac "valid_idle s") apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def) apply (clarsimp simp: invs_def valid_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; ct_active s\<rbrakk> \<Longrightarrow> not_idle_thread (cur_thread s) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; st_tcb_at active (cur_thread s) s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> idle_thread s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; st_tcb_at active (cur_thread s) s; valid_idle s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> idle_thread s
 2. \<lbrakk>invs s; st_tcb_at active (cur_thread s) s\<rbrakk> \<Longrightarrow> valid_idle s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; st_tcb_at active (cur_thread s) s\<rbrakk> \<Longrightarrow> valid_idle s proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma valid_etcbs_clear_um_detype:
  "\<lbrakk> valid_etcbs s \<rbrakk> \<Longrightarrow> valid_etcbs (clear_um {frame..frame + 2 ^ pageBits - 1} (Retype_A.detype {frame..frame + 2 ^ pageBits - 1} s))" by (clarsimp simp: valid_etcbs_def st_tcb_at_def is_etcb_at_def st_tcb_at_kh_def
                     obj_at_kh_def obj_at_def detype_def detype_ext_def clear_um_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_etcbs s \<Longrightarrow> valid_etcbs (clear_um {frame..frame + 2 ^ pageBits - 1} (Retype_A.detype {frame..frame + 2 ^ pageBits - 1} s))