kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_AI

lemma ep_redux_simps:
  "valid_ep (case xs of [] \<Rightarrow> Structures_A.IdleEP | y # ys \<Rightarrow> Structures_A.SendEP (y # ys))
        = (\<lambda>s. distinct xs \<and> (\<forall>t\<in>set xs. tcb_at t s))"
  "valid_ep (case xs of [] \<Rightarrow> Structures_A.IdleEP | y # ys \<Rightarrow> Structures_A.RecvEP (y # ys))
        = (\<lambda>s. distinct xs \<and> (\<forall>t\<in>set xs. tcb_at t s))"
  "valid_ntfn (ntfn\<lparr>ntfn_obj := (case xs of [] \<Rightarrow> Structures_A.IdleNtfn | y # ys \<Rightarrow> Structures_A.WaitingNtfn (y # ys))\<rparr>)
        = (\<lambda>s. distinct xs \<and> (\<forall>t\<in>set xs. tcb_at t s)
             \<and> (case ntfn_bound_tcb ntfn of
                 Some t \<Rightarrow> tcb_at t s \<and> (case xs of y # ys \<Rightarrow> xs = [t] | _ \<Rightarrow> True)
               | _ \<Rightarrow> True))"
  "ep_q_refs_of (case xs of [] \<Rightarrow> Structures_A.IdleEP | y # ys \<Rightarrow> Structures_A.SendEP (y # ys))
        = (set xs \<times> {EPSend})"
  "ep_q_refs_of (case xs of [] \<Rightarrow> Structures_A.IdleEP | y # ys \<Rightarrow> Structures_A.RecvEP (y # ys))
        = (set xs \<times> {EPRecv})"
  "ntfn_q_refs_of (case xs of [] \<Rightarrow> Structures_A.IdleNtfn | y # ys \<Rightarrow> Structures_A.WaitingNtfn (y # ys))
        = (set xs \<times> {NTFNSignal})" by (fastforce split: list.splits option.splits
                 simp: valid_ep_def valid_ntfn_def valid_bound_tcb_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (valid_ep (case xs of [] \<Rightarrow> IdleEP | y # ys \<Rightarrow> SendEP (y # ys)) = (\<lambda>s. distinct xs \<and> (\<forall>t\<in>set xs. tcb_at t s)) &&& valid_ep (case xs of [] \<Rightarrow> IdleEP | y # ys \<Rightarrow> RecvEP (y # ys)) = (\<lambda>s. distinct xs \<and> (\<forall>t\<in>set xs. tcb_at t s)) &&& valid_ntfn (ntfn_set_obj ntfn (case xs of [] \<Rightarrow> IdleNtfn | y # ys \<Rightarrow> WaitingNtfn (y # ys))) = (\<lambda>s. distinct xs \<and> (\<forall>t\<in>set xs. tcb_at t s) \<and> (case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some t \<Rightarrow> tcb_at t s \<and> (case xs of [] \<Rightarrow> True | y # ys \<Rightarrow> xs = [t])))) &&& ep_q_refs_of (case xs of [] \<Rightarrow> IdleEP | y # ys \<Rightarrow> SendEP (y # ys)) = set xs \<times> {EPSend} &&& ep_q_refs_of (case xs of [] \<Rightarrow> IdleEP | y # ys \<Rightarrow> RecvEP (y # ys)) = set xs \<times> {EPRecv} &&& ntfn_q_refs_of (case xs of [] \<Rightarrow> IdleNtfn | y # ys \<Rightarrow> WaitingNtfn (y # ys)) = set xs \<times> {NTFNSignal}
theory KHeap_AI

lemma set_simple_ko_global_refs [wp]:
  "set_simple_ko f ntfn p \<lbrace>valid_global_refs\<rbrace>" by (rule valid_global_refs_cte_lift; wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs\<rbrace> set_simple_ko f ntfn p \<lbrace>\<lambda>_. valid_global_refs\<rbrace>
theory KHeap_AI

lemma set_simple_ko_reply[wp]:
  "set_simple_ko f p ep \<lbrace>valid_reply_caps\<rbrace>" by (wp valid_reply_caps_st_cte_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps\<rbrace> set_simple_ko f p ep \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>
theory KHeap_AI

lemma obj_at_ko_atE:
  "\<lbrakk> obj_at P ptr s; ko_at k ptr s; P k \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q" by (clarsimp simp: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at P ptr s; ko_at k ptr s; P k \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
theory KHeap_AI

lemma set_object_non_pagetable:
  "vspace_obj_pred P' \<Longrightarrow>
   \<lbrace>(\<lambda>s. P (obj_at P' p' s)) and K(non_vspace_obj ko) and obj_at non_vspace_obj p \<rbrace>
    set_object p ko
   \<lbrace>\<lambda>r s. P (obj_at P' p' s)\<rbrace>" unfolding set_object_def apply wp apply clarsimp apply (erule_tac P=P in rsubst) apply (clarsimp simp: obj_at_def) by (rule vspace_obj_predE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vspace_obj_pred P' \<Longrightarrow> \<lbrace>(\<lambda>s. P (obj_at P' p' s)) and K (non_vspace_obj ko) and obj_at non_vspace_obj p\<rbrace> set_object p ko \<lbrace>\<lambda>r s. P (obj_at P' p' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. vspace_obj_pred P' \<Longrightarrow> \<lbrace>(\<lambda>s. P (obj_at P' p' s)) and K (non_vspace_obj ko) and obj_at non_vspace_obj p\<rbrace> do kobj <- get_object p;
assert (a_type kobj = a_type ko);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)
od \<lbrace>\<lambda>r s. P (obj_at P' p' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vspace_obj_pred P'; ((\<lambda>s. P (obj_at P' p' s)) and K (non_vspace_obj ko) and obj_at non_vspace_obj p) s\<rbrakk> \<Longrightarrow> \<forall>koa. ko_at koa p s \<longrightarrow> a_type koa = a_type ko \<longrightarrow> P (obj_at P' p' (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s koa. \<lbrakk>vspace_obj_pred P'; P (obj_at P' p' s); non_vspace_obj ko; obj_at non_vspace_obj p s; ko_at koa p s; a_type koa = a_type ko\<rbrakk> \<Longrightarrow> P (obj_at P' p' (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s koa. \<lbrakk>vspace_obj_pred P'; non_vspace_obj ko; obj_at non_vspace_obj p s; ko_at koa p s; a_type koa = a_type ko\<rbrakk> \<Longrightarrow> obj_at P' p' s = obj_at P' p' (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s koa. \<lbrakk>vspace_obj_pred P'; non_vspace_obj ko; non_vspace_obj koa; kheap s p = Some koa; a_type koa = a_type ko; p' = p\<rbrakk> \<Longrightarrow> P' koa = P' ko
theory KHeap_AI

lemma set_object_memory[wp]:
  "\<lbrace>\<lambda>s. P (underlying_memory (machine_state s))\<rbrace>
    set_object p ko
   \<lbrace>\<lambda>_ s. P (underlying_memory (machine_state s))\<rbrace>" unfolding set_object_def apply wp by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (underlying_memory (machine_state s))\<rbrace> set_object p ko \<lbrace>\<lambda>_ s. P (underlying_memory (machine_state s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (underlying_memory (machine_state s))\<rbrace> do kobj <- get_object p;
assert (a_type kobj = a_type ko);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)
od \<lbrace>\<lambda>_ s. P (underlying_memory (machine_state s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (underlying_memory (machine_state s)) \<Longrightarrow> \<forall>koa. ko_at koa p s \<longrightarrow> a_type koa = a_type ko \<longrightarrow> P (underlying_memory (machine_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)))
theory KHeap_AI

lemma do_machine_op_result[wp]:
  "\<lbrace>P\<rbrace> mop \<lbrace>\<lambda>rv s. Q rv\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P (machine_state s)\<rbrace> do_machine_op mop \<lbrace>\<lambda>rv s. Q rv\<rbrace>" unfolding do_machine_op_def by wpsimp (erule(2) use_valid)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> mop \<lbrace>\<lambda>rv s. Q rv\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P (machine_state s)\<rbrace> do_machine_op mop \<lbrace>\<lambda>rv s. Q rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> mop \<lbrace>\<lambda>rv s. Q rv\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P (machine_state s)\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f (mop ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od \<lbrace>\<lambda>rv s. Q rv\<rbrace>
theory KHeap_AI

lemma dmo_inv:
  assumes "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
  shows "\<lbrace>P\<rbrace> do_machine_op f \<lbrace>\<lambda>_. P\<rbrace>" unfolding do_machine_op_def by wpsimp
     (fastforce dest: in_inv_by_hoareD [OF assms])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do_machine_op f \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f (f ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od \<lbrace>\<lambda>_. P\<rbrace>
theory KHeap_AI

lemma dmo_inv_prop_lift:
  assumes "\<And>P. f \<lbrace>\<lambda>ms. P (g ms)\<rbrace>"
  shows "do_machine_op f \<lbrace>\<lambda>s. P (g (machine_state s))\<rbrace>" unfolding do_machine_op_def by wpsimp
     (erule (1) use_valid[OF _ assms])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (g (machine_state s))\<rbrace> do_machine_op f \<lbrace>\<lambda>_ s. P (g (machine_state s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (g (machine_state s))\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f (f ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od \<lbrace>\<lambda>_ s. P (g (machine_state s))\<rbrace>
theory KHeap_AI

lemma valid_arch_state[wp]:"\<lbrace>valid_arch_state\<rbrace> f \<lbrace>\<lambda>_. valid_arch_state\<rbrace>" by (rule valid_arch_state_lift_aobj_at; wp aobj_at; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<rbrace> f \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
theory KHeap_AI

lemma valid_vspace_obj[wp]:"f \<lbrace>valid_vspace_objs\<rbrace>" by (rule valid_vspace_objs_lift_weak; wp vsobj_at; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs\<rbrace> f \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>
theory KHeap_AI

lemma vs_lookup[wp]: "f \<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace>" by (rule vs_lookup_vspace_obj_at_lift; wp vsobj_at; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup s)\<rbrace>
theory KHeap_AI

lemma vs_lookup_pages[wp]: "f \<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace>" by (rule vs_lookup_pages_vspace_obj_at_lift; wp vsobj_at; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup_pages s)\<rbrace>
theory KHeap_AI

lemma valid_global_objs[wp]: "f \<lbrace>valid_global_objs\<rbrace>" by (rule valid_global_objs_lift_weak, (wp vsobj_at)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_objs\<rbrace> f \<lbrace>\<lambda>_. valid_global_objs\<rbrace>
theory KHeap_AI

lemma valid_global_vspace_mappings[wp]:
  "f \<lbrace>valid_global_vspace_mappings\<rbrace>" by (rule valid_global_vspace_mappings_lift, (wp vsobj_at)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_vspace_mappings\<rbrace> f \<lbrace>\<lambda>_. valid_global_vspace_mappings\<rbrace>
theory KHeap_AI

lemma valid_asid_map[wp]: "f \<lbrace>valid_asid_map\<rbrace>" by (rule valid_asid_map_lift, (wp vsobj_at)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> f \<lbrace>\<lambda>_. valid_asid_map\<rbrace>
theory KHeap_AI

lemma valid_kernel_mappings[wp]: "f \<lbrace>valid_kernel_mappings\<rbrace>" by (rule valid_kernel_mappings_lift, (wp vsobj_at)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_kernel_mappings\<rbrace> f \<lbrace>\<lambda>_. valid_kernel_mappings\<rbrace>
theory KHeap_AI

lemma in_user_frame[wp]:"f \<lbrace>in_user_frame p\<rbrace>" by (rule in_user_frame_obj_pred_lift; wp vsobj_at; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>in_user_frame p\<rbrace> f \<lbrace>\<lambda>_. in_user_frame p\<rbrace>
theory KHeap_AI

lemma valid_machine_state[wp]: "\<lbrace>valid_machine_state\<rbrace> f \<lbrace>\<lambda>rv. valid_machine_state\<rbrace>" unfolding valid_machine_state_def by (wp hoare_vcg_disj_lift hoare_vcg_all_lift vsobj_at memory)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> f \<lbrace>\<lambda>rv. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0\<rbrace>
theory KHeap_AI

lemma valid_arch_caps[wp]: "\<lbrace>valid_arch_caps\<rbrace> f \<lbrace>\<lambda>_. valid_arch_caps\<rbrace>" by (rule valid_arch_caps_lift_weak[OF arch_state' vsobj_at caps])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps\<rbrace> f \<lbrace>\<lambda>_. valid_arch_caps\<rbrace>
theory KHeap_AI

lemma store_word_offs_obj_at_P[wp]:
  "store_word_offs a b c \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace>" unfolding store_word_offs_def by (wp | fastforce)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> store_word_offs a b c \<lbrace>\<lambda>_ s. P (obj_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> do s <- get;
assert (in_user_frame (a + word_of_nat (b * word_size)) s);
do_machine_op $ storeWord (a + word_of_nat (b * word_size)) c
od \<lbrace>\<lambda>_ s. P (obj_at P' p s)\<rbrace>
theory KHeap_AI

lemma valid_irq_handlers_lift:
  assumes x: "\<And>P. f \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace>"
  assumes y: "\<And>P. f \<lbrace>\<lambda>s. P (interrupt_states s)\<rbrace>"
  shows      "f \<lbrace>valid_irq_handlers\<rbrace>" apply (simp add: valid_irq_handlers_def irq_issued_def) apply (rule hoare_use_eq [where f=caps_of_state, OF x y]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers\<rbrace> f \<lbrace>\<lambda>_. valid_irq_handlers\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal\<rbrace> f \<lbrace>\<lambda>_ s. \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma set_simple_ko_only_idle [wp]:
  "set_simple_ko f p ntfn \<lbrace>only_idle\<rbrace>" by (wp only_idle_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_idle\<rbrace> set_simple_ko f p ntfn \<lbrace>\<lambda>_. only_idle\<rbrace>
theory KHeap_AI

lemma set_simple_ko_valid_ioc[wp]:
  "set_simple_ko f ptr val \<lbrace>valid_ioc\<rbrace>" by (set_simple_ko_method wp_thm: set_object_valid_ioc_no_caps[THEN hoare_set_object_weaken_pre]
                                   get_object_wp
                           simp_thm: is_tcb_def is_cap_table_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> set_simple_ko f ptr val \<lbrace>\<lambda>_. valid_ioc\<rbrace>
theory KHeap_AI

lemma set_object_machine_state[wp]:
  "set_object p ko \<lbrace>\<lambda>s. P (machine_state s)\<rbrace>" by (wpsimp wp: set_object_wp_strong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (machine_state s)\<rbrace> set_object p ko \<lbrace>\<lambda>_ s. P (machine_state s)\<rbrace>
theory KHeap_AI

lemma tcb_cap_valid_caps_of_stateD:
  "\<lbrakk> caps_of_state s p = Some cap; valid_objs s \<rbrakk> \<Longrightarrow> tcb_cap_valid cap p s" apply (rule cte_wp_tcb_cap_valid) apply (simp add: cte_wp_at_caps_of_state) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; valid_objs s\<rbrakk> \<Longrightarrow> tcb_cap_valid cap p s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s p = Some cap; valid_objs s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) p s
 2. \<lbrakk>caps_of_state s p = Some cap; valid_objs s\<rbrakk> \<Longrightarrow> valid_objs s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; valid_objs s\<rbrakk> \<Longrightarrow> valid_objs s proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma add_mask_eq:
  "\<lbrakk>is_aligned (w::'a::len word) n; x \<le> 2 ^ n - 1; n < len_of TYPE('a)\<rbrakk>
   \<Longrightarrow> (w + x) && mask n = x" by (drule is_aligned_add_helper) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned w n; x \<le> 2 ^ n - 1; n < LENGTH('a)\<rbrakk> \<Longrightarrow> w + x && mask n = x
theory KHeap_AI

lemma thread_get_wp':
  "\<lbrace>\<lambda>s. \<forall>tcb. ko_at (TCB tcb) ptr s \<longrightarrow> P (f tcb) s\<rbrace> thread_get f ptr \<lbrace>P\<rbrace>" apply (simp add: thread_get_def) apply wp apply clarsimp apply (clarsimp simp: obj_at_def dest!: get_tcb_SomeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>tcb. ko_at (TCB tcb) ptr s \<longrightarrow> P (f tcb) s\<rbrace> thread_get f ptr \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>tcb. ko_at (TCB tcb) ptr s \<longrightarrow> P (f tcb) s\<rbrace> do tcb <- gets_the (get_tcb ptr);
return (f tcb)
od \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>tcb. ko_at (TCB tcb) ptr s \<longrightarrow> P (f tcb) s \<Longrightarrow> get_tcb ptr s \<noteq> None \<longrightarrow> P (f (the (get_tcb ptr s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<forall>tcb. ko_at (TCB tcb) ptr s \<longrightarrow> P (f tcb) s; get_tcb ptr s = Some y\<rbrakk> \<Longrightarrow> P (f y) s proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma set_object_dom_shrink[wp]:
  "set_object pt obj \<lbrace>\<lambda>s. p \<notin> dom (kheap s)\<rbrace>" apply (wp set_object_typ_at get_object_wp | simp add: set_object_def)+ apply (clarsimp simp: obj_at_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. p \<notin> dom (kheap s)\<rbrace> set_object pt obj \<lbrace>\<lambda>_ s. p \<notin> dom (kheap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. p \<notin> dom (kheap s) \<Longrightarrow> \<forall>ko. ko_at ko pt s \<longrightarrow> a_type ko = a_type obj \<longrightarrow> p \<notin> dom (\<lambda>a. if a = pt then Some obj else kheap s a) proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma set_aobject_zombies[wp]:
  "set_object ptr (ArchObj obj) \<lbrace>\<lambda>s. zombies_final s\<rbrace>" apply (wp set_object_zombies[THEN hoare_set_object_weaken_pre]) apply (clarsimp simp: obj_at_def same_caps_def a_type_def
                 split: kernel_object.split_asm if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. zombies_final s \<Longrightarrow> \<forall>ko. ko_at ko ptr s \<longrightarrow> a_type (ArchObj obj) = a_type ko \<longrightarrow> (zombies_final and obj_at (same_caps (ArchObj obj)) ptr) s proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma set_aobject_state_refs[wp]:
  "set_object p (ArchObj obj) \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace>" apply (wpsimp wp: set_object_wp_strong
              simp: obj_at_def a_type_def
             split: kernel_object.split_asm if_split_asm) apply (erule rsubst [where P=P]) apply (rule ext) by (clarsimp simp: state_refs_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> set_object p (ArchObj obj) \<lbrace>\<lambda>_ s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x5. \<lbrakk>P (state_refs_of s); kheap s p = Some (ArchObj x5); aa_type obj = aa_type x5\<rbrakk> \<Longrightarrow> P (state_refs_of (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj obj)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s x5. \<lbrakk>kheap s p = Some (ArchObj x5); aa_type obj = aa_type x5\<rbrakk> \<Longrightarrow> state_refs_of s = state_refs_of (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj obj)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x5 x. \<lbrakk>kheap s p = Some (ArchObj x5); aa_type obj = aa_type x5\<rbrakk> \<Longrightarrow> state_refs_of s x = state_refs_of (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj obj)\<rparr>) x
theory KHeap_AI

lemma set_aobject_cte_wp_at:
  "set_object ptr (ArchObj obj) \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace>" apply (simp add: cte_wp_at_caps_of_state) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (\<exists>cap. caps_of_state s p = Some cap \<and> P' cap)\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_ s. P (\<exists>cap. caps_of_state s p = Some cap \<and> P' cap)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma set_object_is_original_cap[wp]:
  "set_object a b \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace>" by (wpsimp wp: get_object_wp simp: set_object_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> set_object a b \<lbrace>\<lambda>_ s. P (is_original_cap s)\<rbrace>
theory KHeap_AI

lemma set_aobject_valid_mdb[wp]:
  "set_object ptr (ArchObj obj) \<lbrace>\<lambda>s. valid_mdb s\<rbrace>" apply (rule valid_mdb_lift) apply (wp set_object_no_cdt) apply (clarsimp simp: set_object_def) apply (wp get_object_wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_. valid_mdb\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_ s. P (is_original_cap s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_ s. P (is_original_cap s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do kobj <- get_object ptr;
y <- assert (a_type kobj = a_type (ArchObj obj));
s <- get;
put (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj obj)\<rparr>)
od \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_ s. P (is_original_cap s)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma set_aobject_pred_tcb_at[wp]:
  "set_object ptr (ArchObj obj) \<lbrace>pred_tcb_at proj P t\<rbrace>" apply (simp add: set_object_def) apply (wp get_object_wp) apply (clarsimp simp: pred_tcb_at_def obj_at_def a_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t\<rbrace> do kobj <- get_object ptr;
y <- assert (a_type kobj = a_type (ArchObj obj));
s <- get;
put (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj obj)\<rparr>)
od \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pred_tcb_at proj P t s \<Longrightarrow> \<forall>ko. ko_at ko ptr s \<longrightarrow> a_type ko = a_type (ArchObj obj) \<longrightarrow> pred_tcb_at proj P t (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj obj)\<rparr>) proof (prove)
goal:
No subgoals!