kings-crown/FVELER_Isabelle huggingface dataset:
theory CNode_DR

lemma cnode_decode_rotate_throw:
  "length caps \<le> 1 \<Longrightarrow>
  CNode_D.decode_cnode_invocation target target_ref caps
                                  (CNodeRotateIntent a b c d e f g h) =
  Monads_D.throw" apply (cases caps) apply (simp add: CNode_D.decode_cnode_invocation_def)[1] apply (case_tac list) apply (auto simp: CNode_D.decode_cnode_invocation_def get_index_def throw_on_none_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length caps \<le> 1 \<Longrightarrow> CNode_D.decode_cnode_invocation target target_ref caps (CNodeRotateIntent a b c d e f g h) = throw proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length caps \<le> 1; caps = []\<rbrakk> \<Longrightarrow> CNode_D.decode_cnode_invocation target target_ref caps (CNodeRotateIntent a b c d e f g h) = throw
 2. \<And>aa list. \<lbrakk>length caps \<le> 1; caps = aa # list\<rbrakk> \<Longrightarrow> CNode_D.decode_cnode_invocation target target_ref caps (CNodeRotateIntent a b c d e f g h) = throw proof (prove)
goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>length caps \<le> 1; caps = aa # list\<rbrakk> \<Longrightarrow> CNode_D.decode_cnode_invocation target target_ref caps (CNodeRotateIntent a b c d e f g h) = throw proof (prove)
goal (2 subgoals):
 1. \<And>aa list. \<lbrakk>length caps \<le> 1; caps = aa # list; list = []\<rbrakk> \<Longrightarrow> CNode_D.decode_cnode_invocation target target_ref caps (CNodeRotateIntent a b c d e f g h) = throw
 2. \<And>aa list aaa lista. \<lbrakk>length caps \<le> 1; caps = aa # list; list = aaa # lista\<rbrakk> \<Longrightarrow> CNode_D.decode_cnode_invocation target target_ref caps (CNodeRotateIntent a b c d e f g h) = throw proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma set_object_cur_thread_idle_thread:
  "\<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> KHeap_A.set_object word x
         \<lbrace>\<lambda>yb s. P (cur_thread s) (idle_thread s)\<rbrace>" by (wpsimp wp: set_object_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> KHeap_A.set_object word x \<lbrace>\<lambda>yb s. P (cur_thread s) (idle_thread s)\<rbrace>
theory Ipc_DR

lemma set_thread_state_cur_thread_idle_thread:
  "\<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s) \<rbrace> set_thread_state thread x \<lbrace>\<lambda>rv s. P (cur_thread s)  (idle_thread s)\<rbrace>" apply (simp add: set_thread_state_def) apply (wp set_object_cur_thread_idle_thread dxo_wp_weak | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> set_thread_state thread x \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- KHeap_A.set_object thread (TCB (update_tcb_state x tcb));
do_extended_op (set_thread_state_ext thread)
od \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma thread_set_cur_thread_idle_thread:
  " \<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> thread_set (tcb_fault_update Map.empty) word  \<lbrace>\<lambda>xg s. P (cur_thread s) (idle_thread s)\<rbrace>" apply (simp add:thread_set_def) apply (wp set_object_cur_thread_idle_thread) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> thread_set (tcb_fault_update (\<lambda>x. None)) word \<lbrace>\<lambda>xg s. P (cur_thread s) (idle_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> do tcb <- gets_the (get_tcb word);
KHeap_A.set_object word (TCB (tcb\<lparr>tcb_fault := None\<rparr>))
od \<lbrace>\<lambda>xg s. P (cur_thread s) (idle_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (cur_thread s) (idle_thread s) \<Longrightarrow> get_tcb word s \<noteq> None \<longrightarrow> P (cur_thread s) (idle_thread s) proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma do_fault_transfer_cur_thread_idle_thread:
  "\<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> do_fault_transfer c a e recv_buffer \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>" apply (simp add:do_fault_transfer_def set_message_info_def) apply (wp as_user_cur_thread_idle_thread |wpc|clarsimp)+ apply (wps | wp transfer_caps_it copy_mrs_it | simp)+ apply wpc apply (wp | simp add:thread_get_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> do_fault_transfer c a e recv_buffer \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> do fault <- thread_get tcb_fault a;
f <- case fault of None \<Rightarrow> fail | Some f \<Rightarrow> return f;
(label, msg) <- make_fault_msg f a;
sent <- set_mrs e recv_buffer msg;
y <- as_user e (setRegister msg_info_register ((label << 12) || sent));
as_user e (setRegister badge_register c)
od \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>fault f x1 x2. \<lbrace>?R11 fault f (x1, x2) x1 x2\<rbrace> set_mrs e recv_buffer x2 \<lbrace>\<lambda>sent s. P (cur_thread s) (idle_thread s)\<rbrace>
 2. \<And>fault f. \<lbrace>?B2 fault f\<rbrace> make_fault_msg f a \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> ?R11 fault f x xa xb s\<rbrace>
 3. \<And>fault. \<lbrace>?B1 fault\<rbrace> case fault of None \<Rightarrow> fail | Some f \<Rightarrow> return f \<lbrace>?B2 fault\<rbrace>
 4. \<lbrace>?Q\<rbrace> thread_get tcb_fault a \<lbrace>?B1\<rbrace>
 5. \<And>s. P (cur_thread s) (idle_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>fault. \<lbrace>?B1 fault\<rbrace> case fault of None \<Rightarrow> fail | Some f \<Rightarrow> return f \<lbrace>\<lambda>f s. P (cur_thread s) (idle_thread s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> thread_get tcb_fault a \<lbrace>?B1\<rbrace>
 3. \<And>s. P (cur_thread s) (idle_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>fault. fault = None \<Longrightarrow> \<lbrace>?R52 fault\<rbrace> fail \<lbrace>\<lambda>f s. P (cur_thread s) (idle_thread s)\<rbrace>
 2. \<And>fault x2. fault = Some x2 \<Longrightarrow> \<lbrace>?R53 fault x2\<rbrace> return x2 \<lbrace>\<lambda>f s. P (cur_thread s) (idle_thread s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> thread_get tcb_fault a \<lbrace>\<lambda>fault s. (fault = None \<longrightarrow> ?R52 fault s) \<and> (\<forall>x. fault = Some x \<longrightarrow> ?R53 fault x s)\<rbrace>
 4. \<And>s. P (cur_thread s) (idle_thread s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma do_normal_transfer_cur_thread_idle_thread:
  "\<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s) \<rbrace> Ipc_A.do_normal_transfer a b c d e f g \<lbrace>\<lambda>rv s. P (cur_thread s)  (idle_thread s)\<rbrace>" apply (simp add:do_normal_transfer_def set_message_info_def cong: if_cong) apply (wp as_user_cur_thread_idle_thread |wpc|clarsimp)+ apply (wps | wp transfer_caps_it copy_mrs_it)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> do_normal_transfer a b c d e f g \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> do mi <- get_message_info a;
caps <- if e then Ipc_A.lookup_extra_caps a b mi <catch> (\<lambda>y. return []) else return [];
mrs_transferred <- copy_mrs a b f g (mi_length mi);
mi' <- Ipc_A.transfer_caps mi caps c f g;
y <- as_user f (setRegister msg_info_register ((mi_label mi << 12) || (mi_extra_caps mi' << 7) || (mi_caps_unwrapped mi' << 9) || mrs_transferred));
as_user f (setRegister badge_register d)
od \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>mi caps mrs_transferred. \<lbrace>?B7 mi caps mrs_transferred\<rbrace> Ipc_A.transfer_caps mi caps c f g \<lbrace>\<lambda>mi' s. P (cur_thread s) (idle_thread s)\<rbrace>
 2. \<And>mi caps. \<lbrace>?B6 mi caps\<rbrace> copy_mrs a b f g (mi_length mi) \<lbrace>?B7 mi caps\<rbrace>
 3. \<And>mi. \<lbrace>?B5 mi\<rbrace> if e then Ipc_A.lookup_extra_caps a b mi <catch> (\<lambda>y. return []) else return [] \<lbrace>?B6 mi\<rbrace>
 4. \<lbrace>?Q4\<rbrace> get_message_info a \<lbrace>?B5\<rbrace>
 5. \<And>s. P (cur_thread s) (idle_thread s) \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. P (cur_thread s) (idle_thread s) \<Longrightarrow> P (cur_thread s) (idle_thread s) proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma do_ipc_transfer_cur_thread_idle_thread:
  "\<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s) \<rbrace> Ipc_A.do_ipc_transfer a b c d e \<lbrace>\<lambda>rv s. P (cur_thread s)  (idle_thread s)\<rbrace>" apply (simp add:do_ipc_transfer_def) apply (wp do_fault_transfer_cur_thread_idle_thread do_normal_transfer_cur_thread_idle_thread|wpc)+ apply (wp | simp add:thread_get_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> Ipc_A.do_ipc_transfer a b c d e \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> do recv_buffer <- lookup_ipc_buffer True e;
fault <- thread_get tcb_fault a;
case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False a;
do_normal_transfer a send_buffer b c d e recv_buffer
od | Some f \<Rightarrow> do_fault_transfer c a e recv_buffer
od \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>recv_buffer. \<lbrace>?B1 recv_buffer\<rbrace> thread_get tcb_fault a \<lbrace>\<lambda>fault s. (fault = None \<longrightarrow> P (cur_thread s) (idle_thread s)) \<and> (\<forall>x. fault = Some x \<longrightarrow> P (cur_thread s) (idle_thread s))\<rbrace>
 2. \<lbrace>?Q\<rbrace> lookup_ipc_buffer True e \<lbrace>?B1\<rbrace>
 3. \<And>s. P (cur_thread s) (idle_thread s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma dcorres_move_guard:
  "dcorres r P P' a c \<Longrightarrow> dcorres r \<top> (P' and (P o transform)) a c" apply (rule corres_underlyingI) apply (erule (1) corres_underlyingE, simp_all)[1] apply (fastforce intro: bexI [rotated]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres r P P' a c \<Longrightarrow> dcorres r (\<lambda>_. True) (P' and P \<circ> transform) a c proof (prove)
goal (2 subgoals):
 1. \<And>s t rv' t'. \<lbrakk>dcorres r P P' a c; (s, t) \<in> {ss'. transform (snd ss') = fst ss'}; True; (P' and P \<circ> transform) t; (rv', t') \<in> fst (c t)\<rbrakk> \<Longrightarrow> \<exists>(rv, s')\<in>fst (a s). (s', t') \<in> {ss'. transform (snd ss') = fst ss'} \<and> r rv rv'
 2. \<And>s t. \<lbrakk>dcorres r P P' a c; (s, t) \<in> {ss'. transform (snd ss') = fst ss'}; True; (P' and P \<circ> transform) t; False\<rbrakk> \<Longrightarrow> \<not> snd (c t) proof (prove)
goal (2 subgoals):
 1. \<And>s t rv' t' s' rv. \<lbrakk>transform t = s; P' t \<and> P s; (rv', t') \<in> fst (c t); (rv, s') \<in> fst (a s); transform t' = s'; r rv rv'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (rv, s') \<Rightarrow> transform t' = s' \<and> r rv rv'
 2. \<And>s t. \<lbrakk>dcorres r P P' a c; (s, t) \<in> {ss'. transform (snd ss') = fst ss'}; True; (P' and P \<circ> transform) t; False\<rbrakk> \<Longrightarrow> \<not> snd (c t) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>dcorres r P P' a c; (s, t) \<in> {ss'. transform (snd ss') = fst ss'}; True; (P' and P \<circ> transform) t; False\<rbrakk> \<Longrightarrow> \<not> snd (c t) proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma dcorres_move_guard_back:
  "dcorres r \<top> (P' and (P o transform)) a c \<Longrightarrow> dcorres r P P' a c" apply (rule corres_underlyingI) apply (erule (1) corres_underlyingE, rule TrueI) apply (fastforce intro: bexI [rotated])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres r (\<lambda>_. True) (P' and P \<circ> transform) a c \<Longrightarrow> dcorres r P P' a c proof (prove)
goal (2 subgoals):
 1. \<And>s t rv' t'. \<lbrakk>dcorres r (\<lambda>_. True) (P' and P \<circ> transform) a c; (s, t) \<in> {ss'. transform (snd ss') = fst ss'}; P s; P' t; (rv', t') \<in> fst (c t)\<rbrakk> \<Longrightarrow> \<exists>(rv, s')\<in>fst (a s). (s', t') \<in> {ss'. transform (snd ss') = fst ss'} \<and> r rv rv'
 2. \<And>s t. \<lbrakk>dcorres r (\<lambda>_. True) (P' and P \<circ> transform) a c; (s, t) \<in> {ss'. transform (snd ss') = fst ss'}; P s; P' t; False\<rbrakk> \<Longrightarrow> \<not> snd (c t) proof (prove)
goal (5 subgoals):
 1. \<And>s t rv' t'. \<lbrakk>(s, t) \<in> {ss'. transform (snd ss') = fst ss'}; P s; P' t; (rv', t') \<in> fst (c t)\<rbrakk> \<Longrightarrow> (P' and P \<circ> transform) t
 2. \<And>s t rv' t'. \<lbrakk>(s, t) \<in> {ss'. transform (snd ss') = fst ss'}; P s; P' t; (rv', t') \<in> fst (c t)\<rbrakk> \<Longrightarrow> (?rv'3 s t rv' t', ?t'3 s t rv' t') \<in> fst (c t)
 3. \<And>s t rv' t' s' rv. \<lbrakk>(s, t) \<in> {ss'. transform (snd ss') = fst ss'}; P s; P' t; (rv', t') \<in> fst (c t); False \<longrightarrow> \<not> snd (c t); (rv, s') \<in> fst (a s); (s', ?t'3 s t rv' t') \<in> {ss'. transform (snd ss') = fst ss'}; r rv (?rv'3 s t rv' t')\<rbrakk> \<Longrightarrow> \<exists>(rv, s')\<in>fst (a s). (s', t') \<in> {ss'. transform (snd ss') = fst ss'} \<and> r rv rv'
 4. \<And>s t rv' t'. \<lbrakk>(s, t) \<in> {ss'. transform (snd ss') = fst ss'}; P s; P' t; (rv', t') \<in> fst (c t)\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd (a s)
 5. \<And>s t. \<lbrakk>dcorres r (\<lambda>_. True) (P' and P \<circ> transform) a c; (s, t) \<in> {ss'. transform (snd ss') = fst ss'}; P s; P' t; False\<rbrakk> \<Longrightarrow> \<not> snd (c t) proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma dcorres_move_guard_iff:
  "dcorres r P P' a c = dcorres r \<top> (P' and (P o transform)) a c" apply (rule iffI) apply (erule dcorres_move_guard) apply (erule dcorres_move_guard_back) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres r P P' a c = dcorres r (\<lambda>_. True) (P' and P \<circ> transform) a c proof (prove)
goal (2 subgoals):
 1. dcorres r P P' a c \<Longrightarrow> dcorres r (\<lambda>_. True) (P' and P \<circ> transform) a c
 2. dcorres r (\<lambda>_. True) (P' and P \<circ> transform) a c \<Longrightarrow> dcorres r P P' a c proof (prove)
goal (1 subgoal):
 1. dcorres r (\<lambda>_. True) (P' and P \<circ> transform) a c \<Longrightarrow> dcorres r P P' a c proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma transform_cdt_cong:
  "\<lbrakk> cdt s = cdt s'; interrupt_irq_node s = interrupt_irq_node s' \<rbrakk> \<Longrightarrow> transform_cdt s = transform_cdt s'" unfolding transform_cdt_def by (simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdt s = cdt s'; interrupt_irq_node s = interrupt_irq_node s'\<rbrakk> \<Longrightarrow> transform_cdt s = transform_cdt s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdt s = cdt s'; interrupt_irq_node s = interrupt_irq_node s'\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s) = map_lift_over transform_cslot_ptr (cdt s')
theory Ipc_DR

lemma transform_current_thread_cong:
  "\<lbrakk> cur_thread s = cur_thread s'; idle_thread s = idle_thread s' \<rbrakk> \<Longrightarrow> transform_current_thread s = transform_current_thread s'" unfolding transform_current_thread_def by (simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cur_thread s = cur_thread s'; idle_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> transform_current_thread s = transform_current_thread s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cur_thread s = cur_thread s'; idle_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> (if cur_thread s \<noteq> idle_thread s then Some (cur_thread s) else None) = (if cur_thread s' \<noteq> idle_thread s' then Some (cur_thread s') else None)
theory Ipc_DR

lemma cap_installed_at_irq_weak_cong:
  "\<lbrakk> w = w'; caps_of_state s = caps_of_state s'; interrupt_irq_node s = interrupt_irq_node s' \<rbrakk> \<Longrightarrow> cap_installed_at_irq w s = cap_installed_at_irq w' s'" unfolding cap_installed_at_irq_def by (simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w = w'; caps_of_state s = caps_of_state s'; interrupt_irq_node s = interrupt_irq_node s'\<rbrakk> \<Longrightarrow> cap_installed_at_irq w s = cap_installed_at_irq w' s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w = w'; caps_of_state s = caps_of_state s'; interrupt_irq_node s = interrupt_irq_node s'\<rbrakk> \<Longrightarrow> caps_of_state s (interrupt_irq_node s w, []) = caps_of_state s' (interrupt_irq_node s' w', [])
theory Ipc_DR

lemma is_arch_page_capE:
  assumes ispc: "is_arch_page_cap cap"
  and     rl:   "\<And>buf rights sz mapdata dev. \<lbrakk> cap = cap.ArchObjectCap (arch_cap.PageCap dev buf rights sz mapdata)\<rbrakk> \<Longrightarrow> R"
  shows   "R" using ispc unfolding is_arch_page_cap_def apply (simp split:  cap.splits arch_cap.splits) apply (erule rl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R proof (prove)
using this:
is_arch_page_cap cap

goal (1 subgoal):
 1. R proof (prove)
using this:
case cap of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> True | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False

goal (1 subgoal):
 1. R proof (prove)
goal (1 subgoal):
 1. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); x12 = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> R proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma get_ipc_buffer_words_Nil:
  "get_ipc_buffer_words ms tcb [] = []" unfolding get_ipc_buffer_words_def by (auto simp: mapM_Nil split: cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_ipc_buffer_words ms tcb [] = [] proof (prove)
goal (1 subgoal):
 1. (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)) []) else return [] | ArchObjectCap _ \<Rightarrow> return [] | _ \<Rightarrow> return [] in the (evalMonad wordsM ms)) = []
theory Ipc_DR

lemma det_loadWord:
  "is_aligned x 2 \<Longrightarrow> det (loadWord x)" unfolding loadWord_def by (simp add: is_aligned_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned x 2 \<Longrightarrow> det (loadWord x) proof (prove)
goal (1 subgoal):
 1. is_aligned x 2 \<Longrightarrow> det (do m <- gets underlying_memory;
assert (x && mask 2 = 0);
return (word_rcat [m (x + 3), m (x + 2), m (x + 1), m x])
od)
theory Ipc_DR

lemma functional_from_wp:
  "(\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>) \<Longrightarrow> functional f" unfolding functional_def by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>) \<Longrightarrow> functional f proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>) \<Longrightarrow> \<forall>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>
theory Ipc_DR

lemma detE:
  "\<lbrakk> det f; \<And>a b. fst (f s) = {(a, b)} \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" unfolding det_def apply (drule spec [where x = s]) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>det f; \<And>a b. fst (f s) = {(a, b)} \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. \<exists>r. f s = ({r}, False); \<And>a b. fst (f s) = {(a, b)} \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a b. fst (f s) = {(a, b)} \<Longrightarrow> R; \<exists>r. f s = ({r}, False)\<rbrakk> \<Longrightarrow> R proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma evalMonad_from_wp:
  "\<lbrakk> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv _. P rv\<rbrace>; det f \<rbrakk> \<Longrightarrow> P (the (evalMonad f s))" apply (erule detE [where s = s]) apply (drule use_valid [rotated]) apply (rule refl) apply (erule in_singleton) apply (clarsimp simp: evalMonad_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv _. P rv\<rbrace>; det f\<rbrakk> \<Longrightarrow> P (the (evalMonad f s)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv _. P rv\<rbrace>; fst (f s) = {(a, b)}\<rbrakk> \<Longrightarrow> P (the (evalMonad f s)) proof (prove)
goal (3 subgoals):
 1. \<And>a b. fst (f s) = {(a, b)} \<Longrightarrow> s = ?s2 a b
 2. \<And>a b. fst (f s) = {(a, b)} \<Longrightarrow> (?r2 a b, ?s'2 a b) \<in> fst (f (?s2 a b))
 3. \<And>a b. \<lbrakk>fst (f s) = {(a, b)}; P (?r2 a b)\<rbrakk> \<Longrightarrow> P (the (evalMonad f s)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. fst (f s) = {(a, b)} \<Longrightarrow> (?r2 a b, ?s'2 a b) \<in> fst (f s)
 2. \<And>a b. \<lbrakk>fst (f s) = {(a, b)}; P (?r2 a b)\<rbrakk> \<Longrightarrow> P (the (evalMonad f s)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>fst (f s) = {(a, b)}; P a\<rbrakk> \<Longrightarrow> P (the (evalMonad f s)) proof (prove)
goal:
No subgoals!