kings-crown/FVELER_Isabelle huggingface dataset:
theory Intent_DR

lemma empty_when_fail_lookup_ipc_buffer:
  "empty_when_fail (lookup_ipc_buffer a b)" apply (simp add:lookup_ipc_buffer_def) apply (rule empty_when_fail_compose)+ apply (simp_all add: empty_when_fail_simps empty_when_fail_get_cap empty_when_fail_thread_get
                           weak_det_spec_simps weak_det_spec_thread_get weak_det_spec_get_cap) apply (case_tac ra; simp add:empty_when_fail_simps) apply (rename_tac arch_cap) apply (case_tac arch_cap; simp add:empty_when_fail_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_when_fail (lookup_ipc_buffer a b) proof (prove)
goal (1 subgoal):
 1. empty_when_fail (do buffer_ptr <- thread_get tcb_ipc_buffer b;
CSpaceAcc_A.get_cap (b, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> a then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))
od) proof (prove)
goal (5 subgoals):
 1. \<And>r ra. empty_when_fail (case ra of ArchObjectCap (PageCap xa p R vms xaa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> a then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)
 2. \<And>r. empty_when_fail (CSpaceAcc_A.get_cap (b, tcb_cnode_index 4))
 3. \<And>r P. weak_det_spec P (CSpaceAcc_A.get_cap (b, tcb_cnode_index 4))
 4. empty_when_fail (thread_get tcb_ipc_buffer b)
 5. \<And>P. weak_det_spec P (thread_get tcb_ipc_buffer b) proof (prove)
goal (1 subgoal):
 1. \<And>r ra. empty_when_fail (case ra of ArchObjectCap (PageCap xa p R vms xaa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> a then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None) proof (prove)
goal (1 subgoal):
 1. \<And>r ra x12. ra = ArchObjectCap x12 \<Longrightarrow> empty_when_fail (case x12 of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> a then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) proof (prove)
goal (1 subgoal):
 1. \<And>r ra arch_cap. ra = ArchObjectCap arch_cap \<Longrightarrow> empty_when_fail (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> a then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma mab_le_pbfs [simp]:
  "msg_align_bits \<le> pageBitsForSize sz" by (cases sz, simp_all add: msg_align_bits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msg_align_bits \<le> pageBitsForSize sz
theory Intent_DR

lemma two_le_pbfs[simp]:
  "2 \<le> pageBitsForSize sz" by (cases sz,simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 \<le> pageBitsForSize sz
theory Intent_DR

lemma two_le_msg_align_bits[simp]:
  "2 \<le> msg_align_bits" by(simp add:msg_align_bits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 \<le> msg_align_bits
theory Intent_DR

lemma is_aligned_word_size[simp]:
  "is_aligned (of_nat r * of_nat word_size) 2" apply (simp add:word_size_def) apply (rule is_aligned_mult_triv2[where n = 2,simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned (word_of_nat r * word_of_nat word_size) 2 proof (prove)
goal (1 subgoal):
 1. is_aligned (word_of_nat r * 4) 2 proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma ipc_frame_wp_at_cte_at:
  "ipc_frame_wp_at P a s\<Longrightarrow> \<exists>buf sz rs. ipc_frame_cte_at a buf sz rs s" by (clarsimp simp:ipc_frame_wp_at_def obj_at_def cte_wp_at_cases
    ,simp add: split:cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ipc_frame_wp_at P a s \<Longrightarrow> \<exists>buf sz rs. ipc_frame_cte_at a buf sz rs s
theory Intent_DR

lemma get_ipc_frame_words_no_ipc_buffer:
  "\<not> (is_arch_page_cap (tcb_ipcframe tcb)) \<Longrightarrow> get_ipc_buffer_words ms tcb ns = []" unfolding get_ipc_buffer_words_def by (clarsimp simp: evalMonad_def Let_def return_def
    split:if_splits cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_arch_page_cap (tcb_ipcframe tcb) \<Longrightarrow> get_ipc_buffer_words ms tcb ns = [] proof (prove)
goal (1 subgoal):
 1. \<not> is_arch_page_cap (tcb_ipcframe tcb) \<Longrightarrow> (let p = tcb_ipc_buffer tcb; cap = tcb_ipcframe tcb; wordsM = case cap of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then mapM loadWord (map (\<lambda>n. buf + (p && mask (pageBitsForSize sz)) + word_of_nat (n * word_size)) ns) else return [] | ArchObjectCap _ \<Rightarrow> return [] | _ \<Rightarrow> return [] in the (evalMonad wordsM ms)) = []
theory Intent_DR

lemma get_ipc_buffer_words_empty_list[simp]:
  "get_ipc_buffer_words x tcb_type [] = [] " by (clarsimp simp:get_ipc_buffer_words_def split:cap.splits arch_cap.splits
    simp:mapM_def sequence_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_ipc_buffer_words x tcb_type [] = []
theory Intent_DR

lemma mask_neg_mask_cancel:
  "a&& mask n && ~~ mask n = 0 " by (simp add:mask_out_sub_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a && mask n && ~~ mask n = 0
theory Intent_DR

lemma mask_inj_if:
  "\<lbrakk>a && mask n = a; b && mask n = b; a && mask n = b && mask n\<rbrakk>\<Longrightarrow> a = b" by (rule box_equals)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a && mask n = a; b && mask n = b; a && mask n = b && mask n\<rbrakk> \<Longrightarrow> a = b
theory Intent_DR

lemma eq_sym_helper: "(A = B)  \<Longrightarrow> (B = A)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A = B \<Longrightarrow> B = A
theory Intent_DR

lemma select_f_store_word:
  "(select_f (storeWord p w ms)) = (do assert (p && mask 2 = 0);
    return ((),storeWord_ms p w ms) od)" apply (clarsimp simp: assert_def select_f_def storeWord_def bind_def fail_def simpler_modify_def
                        storeWord_ms_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. select_f (storeWord p w ms) = do assert (p && mask 2 = 0);
return ((), storeWord_ms p w ms)
od proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma store_word_offs_ipc_frame_wp:
  "\<lbrace>ipc_frame_wp_at P s_id\<rbrace> store_word_offs base a aa \<lbrace>\<lambda>rv. ipc_frame_wp_at P s_id\<rbrace>" by (wp | simp add: ipc_frame_wp_at_def store_word_offs_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ipc_frame_wp_at P s_id\<rbrace> store_word_offs base a aa \<lbrace>\<lambda>rv. ipc_frame_wp_at P s_id\<rbrace>
theory Intent_DR

lemma pspace_aligned_set_cxt_mrs[wp]:
  "\<lbrace>ko_at (TCB tcb) thread and pspace_aligned\<rbrace>
     KHeap_A.set_object thread (TCB (tcb_arch_update (arch_tcb_context_set t) tcb))
   \<lbrace>\<lambda>rv. pspace_aligned\<rbrace>" apply (wp set_object_aligned) apply (clarsimp simp:obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_at (TCB tcb) thread and pspace_aligned\<rbrace> KHeap_A.set_object thread (TCB (tcb_arch_update (arch_tcb_context_set t) tcb)) \<lbrace>\<lambda>rv. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (ko_at (TCB tcb) thread and pspace_aligned) s \<Longrightarrow> pspace_aligned s proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma pspace_distinct_set_cxt_mrs[wp]:
  "\<lbrace>ko_at (TCB tcb) thread and pspace_distinct\<rbrace>
     KHeap_A.set_object thread (TCB (tcb_arch_update (arch_tcb_context_set t) tcb))
   \<lbrace>\<lambda>rv. pspace_distinct\<rbrace>" apply (wp set_object_distinct) apply (clarsimp simp:obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_at (TCB tcb) thread and pspace_distinct\<rbrace> KHeap_A.set_object thread (TCB (tcb_arch_update (arch_tcb_context_set t) tcb)) \<lbrace>\<lambda>rv. pspace_distinct\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (ko_at (TCB tcb) thread and pspace_distinct) s \<Longrightarrow> pspace_distinct s proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma ipc_buffer_set_cxt_mrs[wp]:
  "\<lbrace>ko_at (TCB tcb) thread and ipc_buffer_wp_at P a\<rbrace>
     KHeap_A.set_object thread (TCB (tcb_arch_update (arch_tcb_context_set t) tcb))
   \<lbrace>\<lambda>rv. ipc_buffer_wp_at P a\<rbrace>" by (clarsimp simp: KHeap_A.set_object_def get_object_def get_def put_def bind_def valid_def
                       return_def obj_at_def ipc_buffer_wp_at_def in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_at (TCB tcb) thread and ipc_buffer_wp_at P a\<rbrace> KHeap_A.set_object thread (TCB (tcb_arch_update (arch_tcb_context_set t) tcb)) \<lbrace>\<lambda>rv. ipc_buffer_wp_at P a\<rbrace>
theory Intent_DR

lemma set_object_valid_etcbs: "\<lbrace>valid_etcbs and (\<lambda>s. kheap s ptr = Some (TCB tcba))\<rbrace>
                KHeap_A.set_object ptr (TCB tcbb)
              \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>" apply (clarsimp simp: set_object_def get_object_def) apply wp apply (auto simp: valid_etcbs_def st_tcb_at_def obj_at_def is_etcb_at_def st_tcb_at_kh_def obj_at_kh_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs and (\<lambda>s. kheap s ptr = Some (TCB tcba))\<rbrace> KHeap_A.set_object ptr (TCB tcbb) \<lbrace>\<lambda>rv. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs and (\<lambda>s. kheap s ptr = Some (TCB tcba))\<rbrace> do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh ptr = Some y);
return (the (kh ptr))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (update_kheap ((kheap s)(ptr \<mapsto> TCB tcbb)) s)
od \<lbrace>\<lambda>rv. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_etcbs and (\<lambda>s. kheap s ptr = Some (TCB tcba))) s \<Longrightarrow> (\<exists>y. kheap s ptr = Some y) \<longrightarrow> a_type (the (kheap s ptr)) = ATCB \<longrightarrow> valid_etcbs (update_kheap ((kheap s)(ptr \<mapsto> TCB tcbb)) s) proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma set_registers_ipc_frame_ptr_at[wp]:
  "\<lbrace>ipc_frame_wp_at buf y\<rbrace>as_user thread (setRegister r rv) \<lbrace>%x. ipc_frame_wp_at buf y\<rbrace>" apply (clarsimp simp: as_user_def select_f_def
                        arch_tcb_update_aux3
                        setRegister_def simpler_modify_def) apply wp apply clarsimp apply wp apply (clarsimp simp:valid_def) apply (assumption) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ipc_frame_wp_at buf y\<rbrace> as_user thread (setRegister r rv) \<lbrace>\<lambda>x. ipc_frame_wp_at buf y\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ipc_frame_wp_at buf y\<rbrace> do tcb <- gets_the (get_tcb thread);
(a, uc') <- \<lambda>s. ({(((), (arch_tcb_context_get (tcb_arch tcb))(r := rv)), s)}, False);
KHeap_A.set_object thread (TCB (tcb_arch_update (arch_tcb_context_set uc') tcb))
od \<lbrace>\<lambda>x. ipc_frame_wp_at buf y\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>tcb x. \<lbrace>?B2 tcb x\<rbrace> case x of (a, uc') \<Rightarrow> KHeap_A.set_object thread (TCB (tcb_arch_update (arch_tcb_context_set uc') tcb)) \<lbrace>\<lambda>x. ipc_frame_wp_at buf y\<rbrace>
 2. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> \<lambda>s. ({(((), (arch_tcb_context_get (tcb_arch tcb))(r := rv)), s)}, False) \<lbrace>?B2 tcb\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 4. \<And>s. ipc_frame_wp_at buf y s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>tcb b. \<lbrace>?B2 tcb ((), b)\<rbrace> KHeap_A.set_object thread (TCB (tcb_arch_update (arch_tcb_context_set b) tcb)) \<lbrace>\<lambda>x. ipc_frame_wp_at buf y\<rbrace>
 2. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> \<lambda>s. ({(((), (arch_tcb_context_get (tcb_arch tcb))(r := rv)), s)}, False) \<lbrace>?B2 tcb\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 4. \<And>s. ipc_frame_wp_at buf y s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> \<lambda>s. ({(((), (arch_tcb_context_get (tcb_arch tcb))(r := rv)), s)}, False) \<lbrace>\<lambda>x2. ko_at (TCB tcb) thread and ipc_frame_wp_at buf y\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 3. \<And>s. ipc_frame_wp_at buf y s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>tcb s. ?B1 tcb s \<Longrightarrow> ko_at (TCB tcb) thread s \<and> ipc_frame_wp_at buf y s
 2. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 3. \<And>s. ipc_frame_wp_at buf y s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>tcb s. ko_at (TCB tcb) thread s \<and> ipc_frame_wp_at buf y s\<rbrace>
 2. \<And>s. ipc_frame_wp_at buf y s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ipc_frame_wp_at buf y s \<Longrightarrow> get_tcb thread s \<noteq> None \<longrightarrow> ko_at (TCB (the (get_tcb thread s))) thread s \<and> ipc_frame_wp_at buf y s proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma set_registers_ipc_buffer_ptr_at[wp]:
  "\<lbrace>ipc_buffer_wp_at buf y\<rbrace>as_user thread (setRegister r rv) \<lbrace>%x. ipc_buffer_wp_at buf y\<rbrace>" apply (clarsimp simp: as_user_def
                        select_f_def
                        setRegister_def
                        arch_tcb_update_aux3
                        simpler_modify_def) apply wp apply clarsimp apply wp apply (clarsimp simp:valid_def) apply (assumption) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ipc_buffer_wp_at buf y\<rbrace> as_user thread (setRegister r rv) \<lbrace>\<lambda>x. ipc_buffer_wp_at buf y\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ipc_buffer_wp_at buf y\<rbrace> do tcb <- gets_the (get_tcb thread);
(a, uc') <- \<lambda>s. ({(((), (arch_tcb_context_get (tcb_arch tcb))(r := rv)), s)}, False);
KHeap_A.set_object thread (TCB (tcb_arch_update (arch_tcb_context_set uc') tcb))
od \<lbrace>\<lambda>x. ipc_buffer_wp_at buf y\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>tcb x. \<lbrace>?B2 tcb x\<rbrace> case x of (a, uc') \<Rightarrow> KHeap_A.set_object thread (TCB (tcb_arch_update (arch_tcb_context_set uc') tcb)) \<lbrace>\<lambda>x. ipc_buffer_wp_at buf y\<rbrace>
 2. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> \<lambda>s. ({(((), (arch_tcb_context_get (tcb_arch tcb))(r := rv)), s)}, False) \<lbrace>?B2 tcb\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 4. \<And>s. ipc_buffer_wp_at buf y s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>tcb b. \<lbrace>?B2 tcb ((), b)\<rbrace> KHeap_A.set_object thread (TCB (tcb_arch_update (arch_tcb_context_set b) tcb)) \<lbrace>\<lambda>x. ipc_buffer_wp_at buf y\<rbrace>
 2. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> \<lambda>s. ({(((), (arch_tcb_context_get (tcb_arch tcb))(r := rv)), s)}, False) \<lbrace>?B2 tcb\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 4. \<And>s. ipc_buffer_wp_at buf y s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> \<lambda>s. ({(((), (arch_tcb_context_get (tcb_arch tcb))(r := rv)), s)}, False) \<lbrace>\<lambda>x2. ko_at (TCB tcb) thread and ipc_buffer_wp_at buf y\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 3. \<And>s. ipc_buffer_wp_at buf y s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>tcb s. ?B1 tcb s \<Longrightarrow> ko_at (TCB tcb) thread s \<and> ipc_buffer_wp_at buf y s
 2. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 3. \<And>s. ipc_buffer_wp_at buf y s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>tcb s. ko_at (TCB tcb) thread s \<and> ipc_buffer_wp_at buf y s\<rbrace>
 2. \<And>s. ipc_buffer_wp_at buf y s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ipc_buffer_wp_at buf y s \<Longrightarrow> get_tcb thread s \<noteq> None \<longrightarrow> ko_at (TCB (the (get_tcb thread s))) thread s \<and> ipc_buffer_wp_at buf y s proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma dcorres_set_mrs:
  "dcorres dc \<top>
   (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y
     and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs)
   (corrupt_frame buf)
             (set_mrs y (Some (buf + (bptr && mask (pageBitsForSize sz)))) b)" apply (rule corrupt_frame_include_self) apply (rule corres_guard_imp[OF set_mrs_corres]) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) (corrupt_frame buf) (set_mrs y (Some (buf + (bptr && mask (pageBitsForSize sz)))) b) proof (prove)
goal (2 subgoals):
 1. dcorres dc (\<lambda>_. True) (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) (do corrupt_tcb_intent ?y;
corrupt_frame buf
od) (set_mrs y (Some (buf + (bptr && mask (pageBitsForSize sz)))) b)
 2. \<And>s. (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s \<Longrightarrow> ipc_frame_ptr_at buf ?y s \<and> not_idle_thread ?y s \<and> valid_etcbs s proof (prove)
goal (3 subgoals):
 1. \<And>s. True \<Longrightarrow> True
 2. \<And>s. (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s \<Longrightarrow> (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s
 3. \<And>s. (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s \<Longrightarrow> ipc_frame_ptr_at buf y s \<and> not_idle_thread y s \<and> valid_etcbs s proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma dcorres_copy_mrs:
  "valid_message_info mi \<Longrightarrow>
   dcorres dc \<top> ((valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y
     and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs))
    (corrupt_frame buf)
    (copy_mrs thread rv y (Some (buf + (bptr && mask (pageBitsForSize sz))))
               (mi_length mi))" apply (rule corrupt_frame_include_self) apply (rule corres_guard_imp[OF copy_mrs_corres]) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_message_info mi \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) (corrupt_frame buf) (copy_mrs thread rv y (Some (buf + (bptr && mask (pageBitsForSize sz)))) (mi_length mi)) proof (prove)
goal (2 subgoals):
 1. valid_message_info mi \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) (do corrupt_tcb_intent ?y;
corrupt_frame buf
od) (copy_mrs thread rv y (Some (buf + (bptr && mask (pageBitsForSize sz)))) (mi_length mi))
 2. \<And>s. \<lbrakk>valid_message_info mi; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at buf ?y s \<and> not_idle_thread ?y s \<and> valid_etcbs s proof (prove)
goal (4 subgoals):
 1. valid_message_info mi \<Longrightarrow> valid_message_info mi
 2. \<And>s. \<lbrakk>valid_message_info mi; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s. \<lbrakk>valid_message_info mi; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s
 4. \<And>s. \<lbrakk>valid_message_info mi; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at buf y s \<and> not_idle_thread y s \<and> valid_etcbs s proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma nat_bl_to_bin_surj:
  "\<exists>bl. n = nat (bl_to_bin bl)" using n_less_equal_power_2[where n=n, folded of_nat_less_iff, simplified] apply (rule_tac x="bin_to_bl n (int n)" in exI) apply (simp only: bin_bl_bin bintrunc_mod2p) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>bl. n = nat (bl_to_bin bl) proof (prove)
using this:
True

goal (1 subgoal):
 1. \<exists>bl. n = nat (bl_to_bin bl) proof (prove)
goal (1 subgoal):
 1. True \<Longrightarrow> n = nat (bl_to_bin (bin_to_bl n (int n))) proof (prove)
goal (1 subgoal):
 1. True \<Longrightarrow> n = nat (int n mod 2 ^ n) proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma transform_tcb_slot_1:
  "transform_cslot_ptr (a,tcb_cnode_index 1) = (a,tcb_vspace_slot)" apply (clarsimp simp:transform_cslot_ptr_def) apply (unfold tcb_vspace_slot_def) apply (simp add: tcb_cnode_index_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_cslot_ptr (a, tcb_cnode_index 1) = (a, tcb_vspace_slot) proof (prove)
goal (1 subgoal):
 1. nat (bl_to_bin (tcb_cnode_index (Suc 0))) = tcb_vspace_slot proof (prove)
goal (1 subgoal):
 1. nat (bl_to_bin (tcb_cnode_index (Suc 0))) = 1 proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma transform_tcb_slot_2:
  "transform_cslot_ptr (a,tcb_cnode_index 2) = (a,tcb_replycap_slot)" apply (clarsimp simp:transform_cslot_ptr_def) apply (unfold tcb_replycap_slot_def) apply (simp add: tcb_cnode_index_def) apply (simp add:bl_to_bin_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_cslot_ptr (a, tcb_cnode_index 2) = (a, tcb_replycap_slot) proof (prove)
goal (1 subgoal):
 1. nat (bl_to_bin (tcb_cnode_index 2)) = tcb_replycap_slot proof (prove)
goal (1 subgoal):
 1. nat (bl_to_bin (tcb_cnode_index 2)) = 2 proof (prove)
goal (1 subgoal):
 1. nat (bl_to_bin [True, False]) = 2 proof (prove)
goal:
No subgoals!