kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_AI

lemma get_mrs_inv[wp]:
  "\<lbrace>P\<rbrace> get_mrs t buf info \<lbrace>\<lambda>rv. P\<rbrace>" by (wpsimp simp: get_mrs_def load_word_offs_def wp: dmo_inv loadWord_inv mapM_wp')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_mrs t buf info \<lbrace>\<lambda>rv. P\<rbrace>
theory Ipc_AI

lemma copy_mrs_typ_at[wp]:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> copy_mrs s sb r rb n \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" apply (simp add: copy_mrs_def load_word_offs_def
                   store_word_offs_def set_object_def
              cong: option.case_cong
              split del: if_split) apply (wp hoare_vcg_split_case_option mapM_wp') apply (wp hoare_drop_imps mapM_wp')+ apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> copy_mrs s sb r rb n \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
buf_mrs <- case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. do v <- do_machine_op (loadWord (sb_ptr + word_of_nat x * word_of_nat word_size));
s <- get;
y <- assert (in_user_frame (rb_ptr + word_of_nat x * word_of_nat word_size) s);
do_machine_op (storeWord (rb_ptr + word_of_nat x * word_of_nat word_size) v)
od) (if Suc (length msg_registers) \<le> unat n then [Suc (length msg_registers)..<unat n] @ [unat n] else []);
return (min n (nat_to_len (min (length msg_registers) (unat n) + length buf_mrs)))
od \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x xa sb_ptr xb y xc. \<lbrakk>xa = Some sb_ptr; xb = Some y; xc \<in> set (if Suc (length msg_registers) \<le> unat n then [Suc (length msg_registers)..<unat n] @ [unat n] else [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. P (typ_at T p a)\<rbrace> do_machine_op (loadWord (sb_ptr + word_of_nat xc * word_of_nat word_size)) \<lbrace>\<lambda>xd s. in_user_frame (y + word_of_nat xc * word_of_nat word_size) s \<longrightarrow> P (typ_at T p s)\<rbrace>
 2. \<lbrace>?Q6\<rbrace> mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers) \<lbrace>\<lambda>x s. (sb = None \<longrightarrow> P (typ_at T p s)) \<and> (\<forall>y. sb = Some y \<longrightarrow> (rb = None \<longrightarrow> P (typ_at T p s)) \<and> (\<forall>y. rb = Some y \<longrightarrow> P (typ_at T p s)))\<rbrace>
 3. \<And>s. P (typ_at T p s) \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. P (typ_at T p s) \<Longrightarrow> P (typ_at T p s) \<and> (\<forall>y. sb = Some y \<longrightarrow> (rb = None \<longrightarrow> P (typ_at T p s)) \<and> (\<forall>y. rb = Some y \<longrightarrow> P (typ_at T p s))) proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma copy_mrs_tcb[wp]:
  "\<lbrace> tcb_at t \<rbrace> copy_mrs s sb r rb n \<lbrace>\<lambda>rv. tcb_at t \<rbrace>" by (simp add: tcb_at_typ, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t\<rbrace> copy_mrs s sb r rb n \<lbrace>\<lambda>rv. tcb_at t\<rbrace>
theory Ipc_AI

lemma copy_mrs_ntfn_at[wp]:
  "\<lbrace> ntfn_at p \<rbrace> copy_mrs s sb r rb n \<lbrace>\<lambda>rv. ntfn_at p \<rbrace>" by (simp add: ntfn_at_typ, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ntfn_at p\<rbrace> copy_mrs s sb r rb n \<lbrace>\<lambda>rv. ntfn_at p\<rbrace>
theory Ipc_AI

lemma store_word_offs_invs[wp]:
  "\<lbrace>invs\<rbrace> store_word_offs p x w \<lbrace>\<lambda>_. invs\<rbrace>" by (wp | simp add: store_word_offs_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> store_word_offs p x w \<lbrace>\<lambda>_. invs\<rbrace>
theory Ipc_AI

lemma set_mrs_aligned [wp]:
  "\<lbrace>pspace_aligned\<rbrace>  set_mrs t a msgs \<lbrace>\<lambda>rv. pspace_aligned\<rbrace>" apply (simp add: set_mrs_redux zipWithM_x_mapM split_def
                   store_word_offs_def
             cong: option.case_cong
              del: upt.simps) apply (wp mapM_wp' | wpcw | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> set_mrs t a msgs \<lbrace>\<lambda>rv. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> do y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>) t;
case a of None \<Rightarrow> return (nat_to_len (min (length msg_registers) (length msgs))) | Some pptr \<Rightarrow> do _ <- mapM (\<lambda>p. do y <- do s <- get;
assert (in_user_frame (pptr + word_of_nat (fst p) * word_of_nat word_size) s)
od;
do_machine_op (storeWord (pptr + word_of_nat (fst p) * word_of_nat word_size) (snd p))
od) (zip [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) msgs));
return (nat_to_len (min (length msgs) msg_max_length))
od
od \<lbrace>\<lambda>rv. pspace_aligned\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma copy_mrs_valid_objs [wp]:
  "\<lbrace>valid_objs\<rbrace> copy_mrs s sb r rb n \<lbrace>\<lambda>rv. valid_objs\<rbrace>" apply (simp add: copy_mrs_redux) apply (wp mapM_wp' | wpc
       | simp add: store_word_offs_def load_word_offs_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> copy_mrs s sb r rb n \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> do buf_mrs <- do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [length msg_registers + 1..<Suc (unat n)]
od;
return (min n (nat_to_len (min (length msg_registers) (unat n) + length buf_mrs)))
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma copy_mrs_aligned [wp]:
  "\<lbrace>pspace_aligned\<rbrace> copy_mrs s sb r rb n \<lbrace>\<lambda>rv. pspace_aligned\<rbrace>" apply (simp add: copy_mrs_redux) apply (wp mapM_wp' | wpc
       | simp add: store_word_offs_def load_word_offs_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> copy_mrs s sb r rb n \<lbrace>\<lambda>rv. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> do buf_mrs <- do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [length msg_registers + 1..<Suc (unat n)]
od;
return (min n (nat_to_len (min (length msg_registers) (unat n) + length buf_mrs)))
od \<lbrace>\<lambda>rv. pspace_aligned\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma get_tcb_ko_at:
  "(get_tcb t s = Some tcb) = ko_at (TCB tcb) t s" by (auto simp: obj_at_def get_tcb_def
           split: option.splits Structures_A.kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (get_tcb t s = Some tcb) = ko_at (TCB tcb) t s
theory Ipc_AI

lemma set_mrs_caps_of_state[wp]:
  "\<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_mrs t b m \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>" apply (simp add: set_mrs_redux zipWithM_x_mapM split_def
             cong: option.case_cong
                split del: if_split) apply (wp mapM_wp' | wpc)+ apply (wp thread_set_caps_of_state_trivial2 | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_mrs t b m \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length m) msg_registers) then m ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>) t;
case b of None \<Rightarrow> return (nat_to_len (min (length msg_registers) (length m))) | Some pptr \<Rightarrow> do _ <- mapM (\<lambda>p. store_word_offs pptr (fst p) (snd p)) (zip (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) (drop (length msg_registers) m));
return (nat_to_len (min (length m) msg_max_length))
od
od \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length m) msg_registers) then m ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>) t \<lbrace>\<lambda>y s. (b = None \<longrightarrow> P (caps_of_state s)) \<and> (\<forall>x. b = Some x \<longrightarrow> P (caps_of_state s))\<rbrace>
 2. \<And>s. P (caps_of_state s) \<Longrightarrow> ?Q4 s proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma set_mrs_mdb [wp]:
  "\<lbrace>valid_mdb\<rbrace> set_mrs t b m \<lbrace>\<lambda>_. valid_mdb\<rbrace>" by (rule valid_mdb_lift; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb\<rbrace> set_mrs t b m \<lbrace>\<lambda>_. valid_mdb\<rbrace>
theory Ipc_AI

lemma set_mrs_ep_at[wp]:
  "\<lbrace>ep_at x\<rbrace> set_mrs tcb buf msg \<lbrace>\<lambda>rv. ep_at x\<rbrace>" by (simp add: ep_at_typ, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ep_at x\<rbrace> set_mrs tcb buf msg \<lbrace>\<lambda>rv. ep_at x\<rbrace>
theory Ipc_AI

lemma copy_mrs_ep_at[wp]:
  "\<lbrace>ep_at x\<rbrace> copy_mrs s sb r rb n \<lbrace>\<lambda>rv. ep_at x\<rbrace>" by (simp add: ep_at_typ, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ep_at x\<rbrace> copy_mrs s sb r rb n \<lbrace>\<lambda>rv. ep_at x\<rbrace>
theory Ipc_AI

lemma lookup_extra_caps_srcs[wp]:
  "\<lbrace>valid_objs\<rbrace> lookup_extra_caps thread buf info \<lbrace>transfer_caps_srcs\<rbrace>,-" apply (simp add: lookup_extra_caps_def lookup_cap_and_slot_def
                   split_def lookup_slot_for_thread_def) apply (wp mapME_set[where R=valid_objs] get_cap_wp resolve_address_bits_real_cte_at
             | simp add: cte_wp_at_caps_of_state
             | wp (once) hoare_drop_imps
             | clarsimp simp: objs_valid_tcb_ctable)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_extra_caps thread buf info \<lbrace>\<lambda>caps s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> liftE (get_extra_cptrs buf info) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (doE p <- doE tcb <- liftE (gets_the (get_tcb thread));
resolve_address_bits (tcb_ctable tcb, cptr)
odE;
cap <- liftE (get_cap (fst p));
returnOk (cap, fst p)
odE)) \<lbrace>\<lambda>caps s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s\<rbrace>, - proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma do_normal_tcb[wp]:
  "\<And>t sender send_buf ep badge can_grant receiver recv_buf.
    \<lbrace>tcb_at t :: 'state_ext state \<Rightarrow> bool\<rbrace>
      do_normal_transfer sender send_buf ep badge
                         can_grant receiver recv_buf
    \<lbrace>\<lambda>rv. tcb_at t\<rbrace>" by (simp add: tcb_at_typ, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>t sender send_buf ep badge can_grant receiver recv_buf. \<lbrace>tcb_at t\<rbrace> do_normal_transfer sender send_buf ep badge can_grant receiver recv_buf \<lbrace>\<lambda>rv. tcb_at t\<rbrace>
theory Ipc_AI

lemma valid_recv_ep_tcb:
  "\<lbrakk> valid_ep (RecvEP (a # lista)) s \<rbrakk> \<Longrightarrow> tcb_at a s" by (simp add: valid_ep_def tcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ep (RecvEP (a # lista)) s \<Longrightarrow> tcb_at a s
theory Ipc_AI

lemma copy_mrs_thread_set_dmo:
  assumes ts: "\<And>c. \<lbrace>Q\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set (c tcb) (tcb_arch tcb)\<rparr>) r \<lbrace>\<lambda>rv. Q\<rbrace>"
  assumes dmo: "\<And>x y. \<lbrace>Q\<rbrace> do_machine_op (storeWord x y) \<lbrace>\<lambda>rv. Q\<rbrace>"
               "\<And>x. \<lbrace>Q\<rbrace> do_machine_op (loadWord x) \<lbrace>\<lambda>rv. Q\<rbrace>"
  shows "\<lbrace>Q\<rbrace> copy_mrs s sb r rb n \<lbrace>\<lambda>rv. Q\<rbrace>" apply (simp add: copy_mrs_redux) apply (wp mapM_wp [where S=UNIV, simplified] dmo ts | wpc
       | simp add: store_word_offs_def load_word_offs_def
       | rule as_user_wp_thread_set_helper hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> copy_mrs s sb r rb n \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> do buf_mrs <- do y <- mapM (\<lambda>ra. do v <- as_user s (getRegister ra);
as_user r (setRegister ra v)
od) (take (unat n) msg_registers);
case sb of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [length msg_registers + 1..<Suc (unat n)]
od;
return (min n (nat_to_len (min (length msg_registers) (unat n) + length buf_mrs)))
od \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma set_mrs_refs_of[wp]:
  "\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace>
     set_mrs a b c
   \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>" by (wp set_mrs_thread_set_dmo thread_set_refs_trivial | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> set_mrs a b c \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>
theory Ipc_AI

lemma set_mrs_cte_wp_at [wp]:
  "\<lbrace>cte_wp_at P c\<rbrace> set_mrs p' b m \<lbrace>\<lambda>rv. cte_wp_at P c\<rbrace>" by (wp set_mrs_thread_set_dmo thread_set_cte_wp_at_trivial
         ball_tcb_cap_casesI | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P c\<rbrace> set_mrs p' b m \<lbrace>\<lambda>rv. cte_wp_at P c\<rbrace>
theory Ipc_AI

lemma set_mrs_ex_nonz_cap_to[wp]:
  "\<lbrace>ex_nonz_cap_to p\<rbrace> set_mrs a b c \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>" by (wp ex_nonz_cap_to_pres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to p\<rbrace> set_mrs a b c \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>
theory Ipc_AI

lemma set_mrs_iflive[wp]:
  "\<lbrace>if_live_then_nonz_cap\<rbrace> set_mrs a b c \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>" by (wp set_mrs_thread_set_dmo thread_set_iflive_trivial
         ball_tcb_cap_casesI | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap\<rbrace> set_mrs a b c \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>
theory Ipc_AI

lemma set_mrs_ifunsafe[wp]:
  "\<lbrace>if_unsafe_then_cap\<rbrace> set_mrs a b c \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>" by (wp set_mrs_thread_set_dmo thread_set_ifunsafe_trivial
         ball_tcb_cap_casesI | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> set_mrs a b c \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>
theory Ipc_AI

lemma set_mrs_zombies[wp]:
  "\<lbrace>zombies_final\<rbrace> set_mrs a b c \<lbrace>\<lambda>rv. zombies_final\<rbrace>" by (wp set_mrs_thread_set_dmo thread_set_zombies_trivial
         ball_tcb_cap_casesI | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> set_mrs a b c \<lbrace>\<lambda>rv. zombies_final\<rbrace>
theory Ipc_AI

lemma set_mrs_valid_globals[wp]:
  "\<lbrace>valid_global_refs\<rbrace> set_mrs a b c \<lbrace>\<lambda>rv. valid_global_refs\<rbrace>" by (wp set_mrs_thread_set_dmo thread_set_global_refs_triv
         ball_tcb_cap_casesI valid_global_refs_cte_lift | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs\<rbrace> set_mrs a b c \<lbrace>\<lambda>rv. valid_global_refs\<rbrace>
theory Ipc_AI

lemma set_mrs_idle[wp]:
  "\<lbrace>valid_idle\<rbrace> set_mrs param_a param_b param_c \<lbrace>\<lambda>_. valid_idle\<rbrace>" by (wp set_mrs_thread_set_dmo thread_set_valid_idle_trivial
         ball_tcb_cap_casesI | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> set_mrs param_a param_b param_c \<lbrace>\<lambda>_. valid_idle\<rbrace>
theory Ipc_AI

lemma set_mrs_reply[wp]:
  "\<lbrace>valid_reply_caps\<rbrace> set_mrs a b c \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>" by (wp set_mrs_thread_set_dmo thread_set_valid_reply_caps_trivial
         ball_tcb_cap_casesI | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps\<rbrace> set_mrs a b c \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>
theory Ipc_AI

lemma set_mrs_reply_masters[wp]:
  "\<lbrace>valid_reply_masters\<rbrace> set_mrs a b c \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>" by (wp set_mrs_thread_set_dmo thread_set_valid_reply_masters_trivial
         ball_tcb_cap_casesI | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters\<rbrace> set_mrs a b c \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>
theory Ipc_AI

lemma do_ipc_transfer_valid_arch[wp]:
  "\<lbrace>valid_arch_state\<rbrace>
    do_ipc_transfer s ep bg grt r \<lbrace>\<lambda>rv. valid_arch_state :: 'state_ext state \<Rightarrow> bool\<rbrace>" by (rule valid_arch_state_lift_aobj_at; wp do_ipc_transfer_aobj_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<rbrace> do_ipc_transfer s ep bg grt r \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>
theory Ipc_AI

lemma copy_mrs_irq_handlers[wp]:
  "\<lbrace>valid_irq_handlers\<rbrace> copy_mrs s sb r rb n \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace>" apply (rule copy_mrs_thread_set_dmo) apply ((wp valid_irq_handlers_lift thread_set_caps_of_state_trivial
              ball_tcb_cap_casesI | simp)+)[1] apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers\<rbrace> copy_mrs s sb r rb n \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>c. \<lbrace>valid_irq_handlers\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set (c tcb) (tcb_arch tcb)\<rparr>) r \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace>
 2. \<And>x y. \<lbrace>valid_irq_handlers\<rbrace> do_machine_op (storeWord x y) \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace>
 3. \<And>x. \<lbrace>valid_irq_handlers\<rbrace> do_machine_op (loadWord x) \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrace>valid_irq_handlers\<rbrace> do_machine_op (storeWord x y) \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace>
 2. \<And>x. \<lbrace>valid_irq_handlers\<rbrace> do_machine_op (loadWord x) \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma as_user_cap_refs_in_kernel_window[wp]:
  "\<lbrace>cap_refs_in_kernel_window\<rbrace> as_user t m \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" by (wp as_user_wp_thread_set_helper ball_tcb_cap_casesI
            thread_set_cap_refs_in_kernel_window
            | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window\<rbrace> as_user t m \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>
theory Ipc_AI

lemma as_user_cap_refs_respects_device_region[wp]:
  "\<lbrace>cap_refs_respects_device_region\<rbrace> as_user t m \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" by (wp as_user_wp_thread_set_helper ball_tcb_cap_casesI
            thread_set_cap_refs_respects_device_region
            | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region\<rbrace> as_user t m \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>
theory Ipc_AI

lemma as_user_valid_ioc[wp]:
  "\<lbrace>valid_ioc\<rbrace> as_user r f \<lbrace>\<lambda>_. valid_ioc\<rbrace>" apply (simp add: as_user_def split_def) apply (wp set_object_valid_ioc_caps) apply (clarsimp simp: valid_ioc_def obj_at_def get_tcb_def
                  split: option.splits Structures_A.kernel_object.splits) apply (drule spec, drule spec, erule impE, assumption) apply (clarsimp simp: cap_of_def tcb_cnode_map_tcb_cap_cases
                        cte_wp_at_cases null_filter_def) apply (simp add: tcb_cap_cases_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> as_user r f \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> do tcb <- gets_the (get_tcb r);
p <- select_f (f (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object r (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_ioc s \<Longrightarrow> get_tcb r s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb r s))))). valid_ioc s \<and> typ_at (a_type (TCB (the (get_tcb r s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb r s)))\<rparr>))) r s \<and> (\<forall>b. is_original_cap s (r, b) \<longrightarrow> null_filter (cap_of (TCB (the (get_tcb r s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb r s)))\<rparr>))) b \<noteq> None)) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 a b ba. \<lbrakk>\<forall>a b. is_original_cap s (a, b) \<longrightarrow> cte_wp_at (\<lambda>x. x \<noteq> NullCap) (a, b) s; kheap s r = Some (TCB x2); (a, b) \<in> fst (f (arch_tcb_context_get (tcb_arch x2))); is_original_cap s (r, ba)\<rbrakk> \<Longrightarrow> \<exists>y. null_filter (cap_of (TCB (x2\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch x2)\<rparr>))) ba = Some y proof (prove)
goal (1 subgoal):
 1. \<And>s x2 a b ba. \<lbrakk>kheap s r = Some (TCB x2); (a, b) \<in> fst (f (arch_tcb_context_get (tcb_arch x2))); is_original_cap s (r, ba); cte_wp_at (\<lambda>x. x \<noteq> NullCap) (r, ba) s\<rbrakk> \<Longrightarrow> \<exists>y. null_filter (cap_of (TCB (x2\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch x2)\<rparr>))) ba = Some y proof (prove)
goal (1 subgoal):
 1. \<And>s x2 a b ba get set restr. \<lbrakk>kheap s r = Some (TCB x2); (a, b) \<in> fst (f (arch_tcb_context_get (tcb_arch x2))); is_original_cap s (r, ba); get x2 \<noteq> NullCap; tcb_cap_cases ba = Some (get, set, restr); get (x2\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch x2)\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma as_user_machine_state[wp]:
  "\<lbrace>\<lambda>s. P(machine_state s)\<rbrace> as_user r f \<lbrace>\<lambda>_. \<lambda>s. P(machine_state s)\<rbrace>" by (wp | simp add: as_user_def split_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (machine_state s)\<rbrace> as_user r f \<lbrace>\<lambda>_ s. P (machine_state s)\<rbrace>