kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_DR

lemma evalMonad_bind_functional:
  "\<lbrakk> functional f; det f \<rbrakk> \<Longrightarrow> evalMonad (f >>= g) s = evalMonad (g (the (evalMonad f s))) s " unfolding evalMonad_def apply (erule detE [where s = s]) apply (clarsimp simp: bind_def) apply (drule in_inv_by_hoareD [OF _ in_singleton, rotated]) apply (clarsimp simp: functional_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>functional f; det f\<rbrakk> \<Longrightarrow> evalMonad (f >>= g) s = evalMonad (g (the (evalMonad f s))) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>functional f; det f\<rbrakk> \<Longrightarrow> (if fst ((f >>= g) s) = {} then None else Some (pick (fst ` fst ((f >>= g) s)))) = (if fst (g (the (if fst (f s) = {} then None else Some (pick (fst ` fst (f s))))) s) = {} then None else Some (pick (fst ` fst (g (the (if fst (f s) = {} then None else Some (pick (fst ` fst (f s))))) s)))) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>functional f; fst (f s) = {(a, b)}\<rbrakk> \<Longrightarrow> (if fst ((f >>= g) s) = {} then None else Some (pick (fst ` fst ((f >>= g) s)))) = (if fst (g (the (if fst (f s) = {} then None else Some (pick (fst ` fst (f s))))) s) = {} then None else Some (pick (fst ` fst (g (the (if fst (f s) = {} then None else Some (pick (fst ` fst (f s))))) s)))) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>functional f; fst (f s) = {(a, b)}\<rbrakk> \<Longrightarrow> (fst (g a b) = {} \<longrightarrow> fst (g a s) = {}) \<and> (fst (g a b) \<noteq> {} \<longrightarrow> fst (g a s) \<noteq> {} \<and> (fst (g a s) \<noteq> {} \<longrightarrow> pick (fst ` fst (g a b)) = pick (fst ` fst (g a s)))) proof (prove)
goal (2 subgoals):
 1. \<And>a b P. functional f \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>a b. \<lbrakk>functional f; b = s\<rbrakk> \<Longrightarrow> (fst (g a b) = {} \<longrightarrow> fst (g a s) = {}) \<and> (fst (g a b) \<noteq> {} \<longrightarrow> fst (g a s) \<noteq> {} \<and> (fst (g a s) \<noteq> {} \<longrightarrow> pick (fst ` fst (g a b)) = pick (fst ` fst (g a s)))) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>functional f; b = s\<rbrakk> \<Longrightarrow> (fst (g a b) = {} \<longrightarrow> fst (g a s) = {}) \<and> (fst (g a b) \<noteq> {} \<longrightarrow> fst (g a s) \<noteq> {} \<and> (fst (g a s) \<noteq> {} \<longrightarrow> pick (fst ` fst (g a b)) = pick (fst ` fst (g a s)))) proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma mapM_functional:
  assumes fn: "\<And>n. functional (f n)"
  shows   "functional (mapM f ns)" apply (rule functional_from_wp) apply (wp mapM_wp') apply (rule fn [unfolded functional_def, THEN spec]) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. functional (mapM f ns) proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>P\<rbrace> mapM f ns \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P x. x \<in> set ns \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>P s. P s \<Longrightarrow> P s proof (prove)
goal (1 subgoal):
 1. \<And>P s. P s \<Longrightarrow> P s proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma loadWord_functional [simp]:
  "functional (loadWord n)" unfolding loadWord_def apply (rule functional_from_wp) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. functional (loadWord n) proof (prove)
goal (1 subgoal):
 1. functional (do m <- gets underlying_memory;
assert (n && mask 2 = 0);
return (word_rcat [m (n + 3), m (n + 2), m (n + 1), m n])
od) proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>P\<rbrace> do m <- gets underlying_memory;
assert (n && mask 2 = 0);
return (word_rcat [m (n + 3), m (n + 2), m (n + 1), m n])
od \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P s. P s \<Longrightarrow> n && mask 2 = 0 \<longrightarrow> P s proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma is_aligned_buffer_offset:
  "\<lbrakk> is_aligned buf (pageBitsForSize sz); is_aligned p msg_align_bits \<rbrakk> \<Longrightarrow>
  is_aligned (buf + (p && mask (pageBitsForSize sz)) + of_nat n * of_nat word_size) 2" apply (rule aligned_add_aligned) apply (erule aligned_add_aligned) apply (erule is_aligned_andI1) apply simp apply simp apply (simp add: word_size_def is_aligned_mult_triv2[where n = 2, simplified]
                     word_bits_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned buf (pageBitsForSize sz); is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> is_aligned (buf + (p && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size) 2 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned buf (pageBitsForSize sz); is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> is_aligned (buf + (p && mask (pageBitsForSize sz))) ?n
 2. \<lbrakk>is_aligned buf (pageBitsForSize sz); is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat n * word_of_nat word_size) 2
 3. \<lbrakk>is_aligned buf (pageBitsForSize sz); is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> 2 \<le> ?n proof (prove)
goal (4 subgoals):
 1. is_aligned p msg_align_bits \<Longrightarrow> is_aligned (p && mask (pageBitsForSize sz)) ?n
 2. is_aligned p msg_align_bits \<Longrightarrow> ?n \<le> pageBitsForSize sz
 3. \<lbrakk>is_aligned buf (pageBitsForSize sz); is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat n * word_of_nat word_size) 2
 4. \<lbrakk>is_aligned buf (pageBitsForSize sz); is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> 2 \<le> ?n proof (prove)
goal (3 subgoals):
 1. is_aligned p msg_align_bits \<Longrightarrow> msg_align_bits \<le> pageBitsForSize sz
 2. \<lbrakk>is_aligned buf (pageBitsForSize sz); is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat n * word_of_nat word_size) 2
 3. \<lbrakk>is_aligned buf (pageBitsForSize sz); is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> 2 \<le> msg_align_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned buf (pageBitsForSize sz); is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat n * word_of_nat word_size) 2
 2. \<lbrakk>is_aligned buf (pageBitsForSize sz); is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> 2 \<le> msg_align_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned buf (pageBitsForSize sz); is_aligned p msg_align_bits\<rbrakk> \<Longrightarrow> 2 \<le> msg_align_bits proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma evalMonad_singleton [simp]:
  "evalMonad (\<lambda>s. ({(f s, g s)}, b)) s = Some (f s)" unfolding evalMonad_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. evalMonad (\<lambda>s. ({(f s, g s)}, b)) s = Some (f s) proof (prove)
goal (1 subgoal):
 1. (if fst ({(f s, g s)}, b) = {} then None else Some (pick (fst ` fst ({(f s, g s)}, b)))) = Some (f s)
theory Ipc_DR

lemma mi_length_dest : "of_nat (unat (mi_length rva)) = mi_length rva" by (rule word_unat.Rep_inverse)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_of_nat (unat (mi_length rva)) = mi_length rva
theory Ipc_DR

lemma dummy_finalise_wp[wp]:
  "is_pending_cap obj
         \<Longrightarrow> \<lbrace>(=) s\<rbrace> PageTableUnmap_D.fast_finalise obj (PageTableUnmap_D.is_final_cap' obj s) \<lbrace>\<lambda>x. (=) s\<rbrace>" by (clarsimp simp:is_pending_cap_def split:cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_pending_cap obj \<Longrightarrow> \<lbrace>(=) s\<rbrace> PageTableUnmap_D.fast_finalise obj (PageTableUnmap_D.is_final_cap' obj s) \<lbrace>\<lambda>x. (=) s\<rbrace>
theory Ipc_DR

lemma cte_at_into_opt_cap:
  "cte_at p s = (\<exists>cap. cte_wp_at ((=) cap) p s
        \<and> (fst p \<noteq> idle_thread s \<and> valid_etcbs s \<longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap)))" apply (clarsimp simp: cte_wp_at_caps_of_state) apply (safe, simp_all) apply (clarsimp simp: caps_of_state_transform_opt_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>_. True) p s = (\<exists>cap. cte_wp_at ((=) cap) p s \<and> (fst p \<noteq> idle_thread s \<and> valid_etcbs s \<longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap))) proof (prove)
goal (1 subgoal):
 1. (\<exists>cap. caps_of_state s p = Some cap) = (\<exists>cap. caps_of_state s p = Some cap \<and> (fst p \<noteq> idle_thread s \<and> valid_etcbs s \<longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap))) proof (prove)
goal (1 subgoal):
 1. \<And>cap. caps_of_state s p = Some cap \<Longrightarrow> fst p \<noteq> idle_thread s \<and> valid_etcbs s \<longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma object_slots_has_slots [simp]:
  "object_slots obj p = Some v \<Longrightarrow> has_slots obj" unfolding object_slots_def has_slots_def by (simp split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_slots obj p = Some v \<Longrightarrow> has_slots obj proof (prove)
goal (1 subgoal):
 1. (case obj of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) p = Some v \<Longrightarrow> case obj of cdl_object.Endpoint \<Rightarrow> False | cdl_object.Notification \<Rightarrow> False | Frame cdl_frame_ext \<Rightarrow> False | cdl_object.Untyped \<Rightarrow> False | _ \<Rightarrow> True
theory Ipc_DR

lemma corres_guard_from_wp_bind_r:
  assumes ac: "corres_underlying sr False False r G G' a (c >>= d)"
  and     rl: "\<lbrace>\<lambda>s. \<not> P s\<rbrace> c \<lbrace>\<lambda>_ _. False\<rbrace>"
  shows "corres_underlying sr False False r G (\<lambda>s. P s \<longrightarrow> G' s) a (c >>= d)" apply (rule corres_guard_from_wp_r) apply (rule ac) apply (wp rl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr False False r G (\<lambda>s. P s \<longrightarrow> G' s) a (c >>= d) proof (prove)
goal (2 subgoals):
 1. corres_underlying sr False False r G G' a (c >>= d)
 2. \<lbrace>\<lambda>s. \<not> P s\<rbrace> c >>= d \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> P s\<rbrace> c >>= d \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma thread_set_gwp:
  "dcorres dc P P' a (thread_set f p)
  \<Longrightarrow> dcorres dc P (\<lambda>s. tcb_at p s \<longrightarrow> P' s) a (thread_set f p)" unfolding thread_set_def apply (erule corres_guard_from_wp_r) apply (wp gets_the_wp) apply (simp add: tcb_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' a (thread_set f p) \<Longrightarrow> dcorres dc P (\<lambda>s. tcb_at p s \<longrightarrow> P' s) a (thread_set f p) proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' a (do tcb <- gets_the $ get_tcb p;
KHeap_A.set_object p $ TCB $ f tcb
od) \<Longrightarrow> dcorres dc P (\<lambda>s. tcb_at p s \<longrightarrow> P' s) a (do tcb <- gets_the $ get_tcb p;
KHeap_A.set_object p $ TCB $ f tcb
od) proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> tcb_at p s\<rbrace> do tcb <- gets_the $ get_tcb p;
KHeap_A.set_object p $ TCB $ f tcb
od \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> tcb_at p s \<Longrightarrow> get_tcb p s \<noteq> None \<longrightarrow> False proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma sts_gwp:
  "dcorres dc P P' a (set_thread_state p st)
  \<Longrightarrow> dcorres dc P (\<lambda>s. tcb_at p s \<longrightarrow> P' s) a (set_thread_state p st)" apply (simp add: set_thread_state_thread_set thread_set_def) apply (erule corres_guard_from_wp_r) apply (wp gets_the_wp) apply (simp add: tcb_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' a (set_thread_state p st) \<Longrightarrow> dcorres dc P (\<lambda>s. tcb_at p s \<longrightarrow> P' s) a (set_thread_state p st) proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' a (do y <- do tcb <- gets_the (get_tcb p);
KHeap_A.set_object p (TCB (update_tcb_state st tcb))
od;
set_thread_state_ext p
od) \<Longrightarrow> dcorres dc P (\<lambda>s. tcb_at p s \<longrightarrow> P' s) a (do y <- do tcb <- gets_the (get_tcb p);
KHeap_A.set_object p (TCB (update_tcb_state st tcb))
od;
set_thread_state_ext p
od) proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> tcb_at p s\<rbrace> do y <- do tcb <- gets_the (get_tcb p);
KHeap_A.set_object p (TCB (update_tcb_state st tcb))
od;
set_thread_state_ext p
od \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> tcb_at p s \<Longrightarrow> get_tcb p s \<noteq> None \<longrightarrow> False proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma corres_ignore_ret_lhs: "dcorres rv P P' (do f;g od) f' \<Longrightarrow> dcorres rv P P' (do a\<leftarrow>f;g od) f'" by (clarsimp simp:corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres rv P P' (do f;
g
od) f' \<Longrightarrow> dcorres rv P P' (do a <- f;
g
od) f'
theory Ipc_DR

lemma set_scheduler_action_dcorres:
  "dcorres dc P P' (return ()) (set_scheduler_action sa)" by (clarsimp simp: set_scheduler_action_def modify_def get_def put_def bind_def return_def  corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' (return ()) (set_scheduler_action sa)
theory Ipc_DR

lemma tcb_sched_action_transform_inv: "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> tcb_sched_action tcb_sched_enqueue t \<lbrace>\<lambda>r s. transform s = cs\<rbrace>" apply (clarsimp simp: tcb_sched_action_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> tcb_sched_action tcb_sched_enqueue t \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma set_scheduler_action_transform_inv:
  "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_scheduler_action act \<lbrace>\<lambda>r s. transform s = cs\<rbrace>" by (wpsimp simp: set_scheduler_action_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_scheduler_action act \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
theory Ipc_DR

lemma ntfn_waiting_set_spec:
  "\<lbrakk>y\<in> ntfn_waiting_set epptr s\<rbrakk>\<Longrightarrow> st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification epptr)) y s" by (clarsimp simp: ntfn_waiting_set_def st_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y \<in> ntfn_waiting_set epptr s \<Longrightarrow> st_tcb_at ((=) (BlockedOnNotification epptr)) y s
theory Ipc_DR

lemma not_empty_list_not_empty_set:
  "a \<noteq> [] \<Longrightarrow> \<exists>x. x \<in> (set a)" apply (case_tac a) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<noteq> [] \<Longrightarrow> \<exists>x. x \<in> set a proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> []; a = []\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> set a
 2. \<And>aa list. \<lbrakk>a \<noteq> []; a = aa # list\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> set a proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma insert_contr:
  "\<lbrakk>\<forall>x. x \<notin> insert y Q\<rbrakk> \<Longrightarrow> P" apply (drule_tac x = y in spec) apply (clarsimp simp:insertI1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x. x \<notin> insert y Q \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. y \<notin> insert y Q \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma bound_tcb_fold:
  "\<lbrakk>kheap s x = Some (TCB tcb); tcb_bound_notification tcb = Some ntfnptr\<rbrakk> \<Longrightarrow> bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) x s" by (auto simp: pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = Some (TCB tcb); tcb_bound_notification tcb = Some ntfnptr\<rbrakk> \<Longrightarrow> bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) x s
theory Ipc_DR

lemma valid_idle_set_thread_state:
  "\<lbrace>not_idle_thread xa and valid_idle :: det_state \<Rightarrow> bool\<rbrace> set_thread_state xa Structures_A.thread_state.Restart \<lbrace>\<lambda>xa. valid_idle\<rbrace>" apply (simp add: set_thread_state_def not_idle_thread_def) apply (simp add: set_object_def get_object_def) apply wp apply (clarsimp simp: not_idle_thread_def) apply (clarsimp simp: obj_at_def dest!:get_tcb_SomeD) apply (auto simp: valid_idle_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_idle_thread xa and valid_idle\<rbrace> set_thread_state xa Restart \<lbrace>\<lambda>xa. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. xa \<noteq> idle_thread s) and valid_idle\<rbrace> do tcb <- gets_the (get_tcb xa);
y <- KHeap_A.set_object xa (TCB (update_tcb_state Restart tcb));
set_thread_state_ext xa
od \<lbrace>\<lambda>xa. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. xa \<noteq> idle_thread s) and valid_idle\<rbrace> do tcb <- gets_the (get_tcb xa);
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh xa = Some y);
return (the (kh xa))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (update_kheap ((kheap s)(xa \<mapsto> TCB (update_tcb_state Restart tcb))) s)
od;
set_thread_state_ext xa
od \<lbrace>\<lambda>xa. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. xa \<noteq> idle_thread s) and valid_idle) s \<Longrightarrow> get_tcb xa s \<noteq> None \<longrightarrow> (\<exists>y. kheap s xa = Some y) \<longrightarrow> a_type (the (kheap s xa)) = ATCB \<longrightarrow> valid_idle (update_kheap ((kheap s)(xa \<mapsto> TCB (update_tcb_state Restart (the (get_tcb xa s))))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>xa \<noteq> idle_thread s; valid_idle s; get_tcb xa s = Some y; kheap s xa = Some (TCB tcb)\<rbrakk> \<Longrightarrow> valid_idle (update_kheap (\<lambda>a. if a = xa then Some (TCB (update_tcb_state Restart (the (get_tcb xa s)))) else kheap s a) s) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>xa \<noteq> idle_thread s; valid_idle s; kheap s xa = Some (TCB tcb)\<rbrakk> \<Longrightarrow> valid_idle (update_kheap (\<lambda>a. if a = xa then Some (TCB (update_tcb_state Restart (the (get_tcb xa s)))) else kheap s a) s) proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma tcb_sched_action_tcb_at_not_idle[wp]:
  "\<lbrace>\<lambda>s. \<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s\<rbrace> tcb_sched_action a b
   \<lbrace>\<lambda>x s. \<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s\<rbrace>" by (wp hoare_Ball_helper)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s\<rbrace> tcb_sched_action a b \<lbrace>\<lambda>x s. \<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s\<rbrace>
theory Ipc_DR

lemma not_idle_thread_cancel_signal:
  "\<lbrace>not_idle_thread obj_id' and valid_idle\<rbrace> cancel_signal obj_id' word \<lbrace>\<lambda>r. valid_idle\<rbrace>" including no_pre apply (simp add:cancel_signal_def) apply (wp valid_idle_set_thread_state|wpc)+ apply (rule hoare_strengthen_post[OF get_simple_ko_sp]) apply (clarsimp simp:not_idle_thread_def obj_at_def is_ntfn_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_idle_thread obj_id' and valid_idle\<rbrace> cancel_signal obj_id' word \<lbrace>\<lambda>r. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_idle_thread obj_id' and valid_idle\<rbrace> cancel_signal obj_id' word \<lbrace>\<lambda>r. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_idle_thread obj_id' and valid_idle\<rbrace> do ntfn <- get_notification word;
queue <- case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification word (ntfn_set_obj ntfn (case remove1 obj_id' queue of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 obj_id' queue)));
set_thread_state obj_id' Inactive
od \<lbrace>\<lambda>r. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_idle_thread obj_id' and valid_idle\<rbrace> get_notification word \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> True) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> obj_at (\<lambda>ko. partial_inv kernel_object.Notification ko \<noteq> None) word s \<and> valid_idle s \<and> (obj_id' = idle_thread s \<longrightarrow> idle Inactive)) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> True)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (ko_at (kernel_object.Notification rv) word and (not_idle_thread obj_id' and valid_idle)) s \<Longrightarrow> (ntfn_obj rv = IdleNtfn \<longrightarrow> True) \<and> (\<forall>x. ntfn_obj rv = WaitingNtfn x \<longrightarrow> obj_at (\<lambda>ko. partial_inv kernel_object.Notification ko \<noteq> None) word s \<and> valid_idle s \<and> (obj_id' = idle_thread s \<longrightarrow> idle Inactive)) \<and> (\<forall>x. ntfn_obj rv = ActiveNtfn x \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma set_thread_state_block_on_send_corres:
    "dcorres dc \<top>
     (not_idle_thread thread and valid_etcbs)
     (block_thread_on_ipc thread
       (PendingSyncSendCap epptr badge call can_grant can_grant_reply False))
     (set_thread_state thread
       (Structures_A.thread_state.BlockedOnSend epptr
         \<lparr>sender_badge = badge, sender_can_grant = can_grant,
          sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))" by (simp add:block_thread_on_ipc_def,rule block_thread_on_send_corres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (not_idle_thread thread and valid_etcbs) (block_thread_on_ipc thread (PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) (set_thread_state thread (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))
theory Ipc_DR

lemma set_thread_state_block_on_receive_corres:
  "dcorres dc \<top> (not_idle_thread thread and valid_etcbs)
      (block_thread_on_ipc thread (PendingSyncRecvCap epptr False can_grant))
      (set_thread_state thread
        (Structures_A.thread_state.BlockedOnReceive epptr \<lparr>receiver_can_grant = can_grant\<rparr>))" apply (simp add:block_thread_on_ipc_def) apply (rule block_thread_on_recv_corres) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (not_idle_thread thread and valid_etcbs) (block_thread_on_ipc thread (PendingSyncRecvCap epptr False can_grant)) (set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = can_grant\<rparr>)) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (not_idle_thread thread and valid_etcbs) (KHeap_D.set_cap (thread, tcb_pending_op_slot) (PendingSyncRecvCap epptr False can_grant)) (set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = can_grant\<rparr>)) proof (prove)
goal:
No subgoals!