kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_AI

lemma ex_cte_cap_to_after_update:
  "\<lbrakk> ex_cte_cap_wp_to P p s; obj_at (same_caps val) p' s \<rbrakk>
     \<Longrightarrow> ex_cte_cap_wp_to P p (kheap_update (\<lambda>a b. if b = p' then Some val else kheap s b) s)" by (clarsimp simp: ex_cte_cap_wp_to_def cte_wp_at_after_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ex_cte_cap_wp_to P p s; obj_at (same_caps val) p' s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to P p (s\<lparr>kheap := \<lambda>b. if b = p' then Some val else kheap s b\<rparr>)
theory KHeap_AI

lemma set_object_iflive:
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap s \<and>
        (live val \<longrightarrow> ex_nonz_cap_to p s) \<and> obj_at (same_caps val) p s\<rbrace>
   set_object p val
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>" apply (wpsimp wp: set_object_wp) by (fastforce simp: if_live_then_nonz_cap_def obj_at_def elim!: ex_cap_to_after_update')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap s \<and> (live val \<longrightarrow> ex_nonz_cap_to p s) \<and> obj_at (same_caps val) p s\<rbrace> set_object p val \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>if_live_then_nonz_cap s; live val \<longrightarrow> ex_nonz_cap_to p s; obj_at (same_caps val) p s\<rbrakk> \<Longrightarrow> if_live_then_nonz_cap (s\<lparr>kheap := (kheap s)(p \<mapsto> val)\<rparr>)
theory KHeap_AI

lemma set_object_ifunsafe[wp]:
  "\<lbrace>if_unsafe_then_cap and obj_at (same_caps val) p\<rbrace>
     set_object p val \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>" apply (simp add: set_object_def) apply wp apply (clarsimp simp: if_unsafe_then_cap_def simp: cte_wp_at_after_update
                 dest!: caps_of_state_cteD) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (fastforce elim!: ex_cte_cap_to_after_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap and obj_at (same_caps val) p\<rbrace> set_object p val \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap and obj_at (same_caps val) p\<rbrace> do kobj <- get_object p;
y <- assert (a_type kobj = a_type val);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> val)\<rparr>)
od \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (if_unsafe_then_cap and obj_at (same_caps val) p) s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko = a_type val \<longrightarrow> if_unsafe_then_cap (s\<lparr>kheap := (kheap s)(p \<mapsto> val)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko a b cap. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) (a, b) s; obj_at (same_caps val) p s; ko_at ko p s; a_type ko = a_type val; cte_wp_at ((=) cap) (a, b) s; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a = p then Some val else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko a b cap. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) (a, b) s; obj_at (same_caps val) p s; ko_at ko p s; a_type ko = a_type val; caps_of_state s (a, b) = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a = p then Some val else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma set_object_zombies[wp]:
  "\<lbrace>zombies_final and obj_at (same_caps val) p\<rbrace>
      set_object p val \<lbrace>\<lambda>rv. zombies_final\<rbrace>" apply (simp add: set_object_def) apply wp apply (clarsimp simp: zombies_final_def is_final_cap'_def2
                        cte_wp_at_after_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final and obj_at (same_caps val) p\<rbrace> set_object p val \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final and obj_at (same_caps val) p\<rbrace> do kobj <- get_object p;
y <- assert (a_type kobj = a_type val);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> val)\<rparr>)
od \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (zombies_final and obj_at (same_caps val) p) s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko = a_type val \<longrightarrow> zombies_final (s\<lparr>kheap := (kheap s)(p \<mapsto> val)\<rparr>) proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma set_simple_ko_iflive[wp]:
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap s \<and> (live (f ep) \<longrightarrow> ex_nonz_cap_to p s)\<rbrace>
     set_simple_ko f p ep \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>" apply (set_simple_ko_method wp_thm: set_object_iflive[THEN hoare_set_object_weaken_pre]) apply (rule conjI; clarsimp elim!: obj_at_weakenE
                              split: Structures_A.kernel_object.splits
                               simp: is_ep_def is_ntfn_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap s \<and> (live (f ep) \<longrightarrow> ex_nonz_cap_to p s)\<rbrace> set_simple_ko f p ep \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>if_live_then_nonz_cap s; live (f ep) \<longrightarrow> ex_nonz_cap_to p s\<rbrakk> \<Longrightarrow> ((\<exists>x3. f ep = Endpoint x3) \<longrightarrow> (\<forall>x3. (\<exists>!y. f y = Endpoint x3) \<longrightarrow> kheap s p = Some (Endpoint x3) \<longrightarrow> is_ep (Endpoint x3))) \<and> ((\<exists>x4. f ep = Notification x4) \<longrightarrow> (\<forall>x4. (\<exists>!y. f y = Notification x4) \<longrightarrow> kheap s p = Some (Notification x4) \<longrightarrow> is_ntfn (Notification x4))) proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma set_simple_ko_ifunsafe[wp]:
  "\<lbrace>if_unsafe_then_cap\<rbrace> set_simple_ko f p val \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>" apply (set_simple_ko_method wp_thm: set_object_ifunsafe[THEN hoare_set_object_weaken_pre]) by (clarsimp elim!: obj_at_weakenE
                simp: is_ep_def is_ntfn_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> set_simple_ko f p val \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. if_unsafe_then_cap s \<Longrightarrow> ((\<exists>x3. f val = Endpoint x3) \<longrightarrow> (\<forall>x3. (\<exists>!y. f y = Endpoint x3) \<longrightarrow> kheap s p = Some (Endpoint x3) \<longrightarrow> is_ep (Endpoint x3))) \<and> ((\<exists>x4. f val = Notification x4) \<longrightarrow> (\<forall>x4. (\<exists>!y. f y = Notification x4) \<longrightarrow> kheap s p = Some (Notification x4) \<longrightarrow> is_ntfn (Notification x4)))
theory KHeap_AI

lemma set_simple_ko_zombies[wp]:
  "\<lbrace>zombies_final\<rbrace> set_simple_ko f p val \<lbrace>\<lambda>rv. zombies_final\<rbrace>" apply (set_simple_ko_method wp_thm: set_object_zombies[THEN hoare_set_object_weaken_pre]) by (clarsimp elim!: obj_at_weakenE
                simp: is_ep_def is_ntfn_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> set_simple_ko f p val \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. zombies_final s \<Longrightarrow> ((\<exists>x3. f val = Endpoint x3) \<longrightarrow> (\<forall>x3. (\<exists>!y. f y = Endpoint x3) \<longrightarrow> kheap s p = Some (Endpoint x3) \<longrightarrow> is_ep (Endpoint x3))) \<and> ((\<exists>x4. f val = Notification x4) \<longrightarrow> (\<forall>x4. (\<exists>!y. f y = Notification x4) \<longrightarrow> kheap s p = Some (Notification x4) \<longrightarrow> is_ntfn (Notification x4)))
theory KHeap_AI

lemma set_object_cap_refs_in_kernel_window:
  "\<lbrace>cap_refs_in_kernel_window and obj_at (same_caps ko) p\<rbrace>
  set_object p ko
  \<lbrace>\<lambda>r. cap_refs_in_kernel_window\<rbrace>" apply (simp add: set_object_def, wp) apply (clarsimp simp: cap_refs_in_kernel_window_def) apply (clarsimp simp: valid_refs_def cte_wp_at_after_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window and obj_at (same_caps ko) p\<rbrace> set_object p ko \<lbrace>\<lambda>r. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cap_refs_in_kernel_window and obj_at (same_caps ko) p) s \<Longrightarrow> \<forall>koa. ko_at koa p s \<longrightarrow> a_type koa = a_type ko \<longrightarrow> cap_refs_in_kernel_window (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s koa. \<lbrakk>valid_refs (ARM.not_kernel_window_arch (arch_state s)) s; obj_at (same_caps ko) p s; ko_at koa p s; a_type koa = a_type ko\<rbrakk> \<Longrightarrow> valid_refs (ARM.not_kernel_window_arch (arch_state s)) (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma get_object_ret:
  "\<lbrace>obj_at P addr\<rbrace> get_object addr \<lbrace>\<lambda>r s. P r\<rbrace>" unfolding get_object_def by (wp, clarsimp elim!: obj_atE)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at P addr\<rbrace> get_object addr \<lbrace>\<lambda>r s. P r\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at P addr\<rbrace> do kh <- gets kheap;
assert (kh addr \<noteq> None);
return $ the $ kh addr
od \<lbrace>\<lambda>r s. P r\<rbrace>
theory KHeap_AI

lemma captable_case_helper:
  "\<lbrakk> \<forall>sz cs. ob \<noteq> CNode sz cs \<rbrakk> \<Longrightarrow> (case ob of CNode sz cs \<Rightarrow> P sz cs | _ \<Rightarrow> Q) = Q" by (case_tac ob, simp_all add: not_ex[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>sz cs. ob \<noteq> CNode sz cs \<Longrightarrow> (case ob of CNode sz cs \<Rightarrow> P sz cs | _ \<Rightarrow> Q) = Q
theory KHeap_AI

lemma null_filter_caps_of_stateD:
  "null_filter (caps_of_state s) p = Some c \<Longrightarrow>
  cte_wp_at (\<lambda>c'. c' = c \<and> c' \<noteq> cap.NullCap) p s" apply (simp add: null_filter_def split: if_split_asm) apply (drule caps_of_state_cteD) apply (simp add: cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. null_filter (caps_of_state s) p = Some c \<Longrightarrow> cte_wp_at (\<lambda>c'. c' = c \<and> c' \<noteq> NullCap) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<noteq> NullCap; caps_of_state s p = Some c\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c'. c' = c \<and> c' \<noteq> NullCap) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<noteq> NullCap; cte_wp_at ((=) c) p s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c'. c' = c \<and> c' \<noteq> NullCap) p s proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma caps_of_state_after_update:
  "obj_at (same_caps val) p s \<Longrightarrow>
     (caps_of_state (kheap_update (\<lambda>a b. if b = p then Some val else kheap s b) s))
       = caps_of_state s" by (simp add: caps_of_state_cte_wp_at cte_wp_at_after_update
          cong: if_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at (same_caps val) p s \<Longrightarrow> caps_of_state (s\<lparr>kheap := \<lambda>b. if b = p then Some val else kheap s b\<rparr>) = caps_of_state s
theory KHeap_AI

lemma elim_CNode_case:
  "\<lbrakk> (case x of CNode sz ct \<Rightarrow> False | _ \<Rightarrow> True) \<rbrakk>
     \<Longrightarrow> (case x of CNode sz ct \<Rightarrow> f sz ct | _ \<Rightarrow> k) = k" by (simp split: Structures_A.kernel_object.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. case x of CNode sz ct \<Rightarrow> False | _ \<Rightarrow> True \<Longrightarrow> (case x of CNode sz ct \<Rightarrow> f sz ct | _ \<Rightarrow> k) = k
theory KHeap_AI

lemma no_fail_obj_at [wp]:
  "no_fail (obj_at \<top> ptr) (get_object ptr)" apply (simp add: get_object_def) apply (rule no_fail_pre, wp) apply (fastforce simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (obj_at (\<lambda>_. True) ptr) (get_object ptr) proof (prove)
goal (1 subgoal):
 1. no_fail (obj_at (\<lambda>_. True) ptr) (do kh <- gets kheap;
y <- assert (\<exists>y. kh ptr = Some y);
return (the (kh ptr))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at (\<lambda>_. True) ptr s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. \<exists>y. kheap s ptr = Some y) and (\<lambda>sa. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> True)) s)) s proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma valid_irq_states_machine_state_updateI:
  "(\<And>irq. interrupt_states s irq = IRQInactive \<Longrightarrow> irq_masks m irq) \<Longrightarrow>
   valid_irq_states (s\<lparr>machine_state := m\<rparr>)" apply(simp add: valid_irq_states_def valid_irq_masks_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>irq. interrupt_states s irq = IRQInactive \<Longrightarrow> irq_masks m irq) \<Longrightarrow> valid_irq_states (s\<lparr>machine_state := m\<rparr>) proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma valid_irq_statesE:
  "\<lbrakk>valid_irq_states s; (\<And> irq. interrupt_states s irq = IRQInactive \<Longrightarrow> irq_masks (machine_state s) irq) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" by(auto simp: valid_irq_states_def valid_irq_masks_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_irq_states s; (\<And>irq. interrupt_states s irq = IRQInactive \<Longrightarrow> irq_masks (machine_state s) irq) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory KHeap_AI

lemma cap_refs_respects_region_cong:
  "\<lbrakk> caps_of_state a  = caps_of_state b;
     device_state (machine_state a) = device_state (machine_state b) \<rbrakk>
  \<Longrightarrow> cap_refs_respects_device_region a = cap_refs_respects_device_region b" by (simp add: cap_refs_respects_device_region_def cte_wp_at_caps_of_state dom_def
                cap_range_respects_device_region_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state a = caps_of_state b; device_state (machine_state a) = device_state (machine_state b)\<rbrakk> \<Longrightarrow> cap_refs_respects_device_region a = cap_refs_respects_device_region b
theory KHeap_AI

lemma dmo_invs:
  "(\<And>P. f \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace>) \<Longrightarrow>
   \<lbrace>\<lambda>s. \<forall>m. \<forall>(r,m')\<in>fst (f m).
              (\<forall>p. in_user_frame p s  \<or> underlying_memory m' p = underlying_memory m p) \<and>
              (\<forall>irq. m = machine_state s \<longrightarrow>
                      (interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq) \<or>
                      irq_masks m' irq = irq_masks m irq) \<and>
              invs s\<rbrace>
   do_machine_op f
   \<lbrace>\<lambda>_. invs\<rbrace>" by (wpsimp wp: dmo_invs1) fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (f m). (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (\<forall>irq. m = machine_state s \<longrightarrow> (interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq) \<or> irq_masks m' irq = irq_masks m irq) \<and> invs s\<rbrace> do_machine_op f \<lbrace>\<lambda>_. invs\<rbrace>
theory KHeap_AI

lemma as_user_typ_at[wp]:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> as_user t m \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" unfolding as_user_def apply (wpsimp wp: set_object_wp_strong) apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> as_user t m \<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 tcb <- gets_the $ get_tcb t;
uc <- return $ arch_tcb_context_get (tcb_arch tcb);
(a, uc') <- select_f $ m uc;
new_tcb <- return $ tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>;
set_object t (TCB new_tcb);
return a
od \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y x xa ko. \<lbrakk>P (typ_at T p s); (x, xa) \<in> fst (m (arch_tcb_context_get (tcb_arch y))); get_tcb t s = Some y; ko_at ko t s; ATCB = a_type ko\<rbrakk> \<Longrightarrow> P (typ_at T p (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch y)\<rparr>))\<rparr>)) proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma as_user_no_del_ntfn[wp]:
  "\<lbrace>ntfn_at p\<rbrace> as_user t m \<lbrace>\<lambda>rv. ntfn_at p\<rbrace>" by (simp add: ntfn_at_typ, rule as_user_typ_at)

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

lemma as_user_no_del_ep[wp]:
  "\<lbrace>ep_at p\<rbrace> as_user t m \<lbrace>\<lambda>rv. ep_at p\<rbrace>" by (simp add: ep_at_typ, rule as_user_typ_at)

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

lemma set_simple_ko_tcb[wp]:
  "set_simple_ko f ep v \<lbrace> 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> set_simple_ko f ep v \<lbrace>\<lambda>_. tcb_at t\<rbrace>
theory KHeap_AI

lemma set_simple_ko_pred_tcb_at [wp]:
  "set_simple_ko g ep v \<lbrace> pred_tcb_at proj f t \<rbrace>" by(set_simple_ko_method wp_thm: set_object_at_obj2 simp_thm: pred_tcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj f t\<rbrace> set_simple_ko g ep v \<lbrace>\<lambda>_. pred_tcb_at proj f t\<rbrace>
theory KHeap_AI

lemma set_endpoint_ep_at[wp]:
  "set_endpoint ptr val \<lbrace>ep_at ptr'\<rbrace>" by (simp add: ep_at_typ, wp)

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

lemma set_notification_ntfn_at[wp]:
  "set_notification ptr val \<lbrace>ntfn_at ptr'\<rbrace>" by (simp add: ntfn_at_typ, wp)

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

lemma cte_wp_at_neg2:
  "(\<not> cte_wp_at P p s) = (cte_at p s \<longrightarrow> cte_wp_at (\<lambda>cap. \<not> P cap) p s)" by (fastforce simp: cte_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> cte_wp_at P p s) = (cte_wp_at (\<lambda>_. True) p s \<longrightarrow> cte_wp_at (\<lambda>cap. \<not> P cap) p s)
theory KHeap_AI

lemma cte_wp_at_neg:
  "cte_wp_at (\<lambda>cap. \<not> P cap) p s = (cte_at p s \<and> \<not> cte_wp_at P p s)" by (fastforce simp: cte_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>cap. \<not> P cap) p s = (cte_wp_at (\<lambda>_. True) p s \<and> \<not> cte_wp_at P p s)
theory KHeap_AI

lemma valid_cte_at_neg_typ:
  assumes x: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
  shows "\<lbrace>\<lambda>s. \<not> cte_at p s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> cte_at p s\<rbrace>" apply (simp add: cte_at_typ) apply (rule hoare_vcg_conj_lift [OF x]) apply (simp only: imp_conv_disj) apply (rule hoare_vcg_disj_lift [OF x]) apply (rule hoare_vcg_prop) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at (\<lambda>_. True) p s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> cte_wp_at (\<lambda>_. True) p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> typ_at (ACapTable (length (snd p))) (fst p) s \<and> (typ_at ATCB (fst p) s \<longrightarrow> snd p \<notin> dom tcb_cap_cases)\<rbrace> f \<lbrace>\<lambda>rv s. \<not> typ_at (ACapTable (length (snd p))) (fst p) s \<and> (typ_at ATCB (fst p) s \<longrightarrow> snd p \<notin> dom tcb_cap_cases)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. typ_at ATCB (fst p) s \<longrightarrow> snd p \<notin> dom tcb_cap_cases\<rbrace> f \<lbrace>\<lambda>rv s. typ_at ATCB (fst p) s \<longrightarrow> snd p \<notin> dom tcb_cap_cases\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> typ_at ATCB (fst p) s \<or> snd p \<notin> dom tcb_cap_cases\<rbrace> f \<lbrace>\<lambda>rv s. \<not> typ_at ATCB (fst p) s \<or> snd p \<notin> dom tcb_cap_cases\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. snd p \<notin> dom tcb_cap_cases\<rbrace> f \<lbrace>\<lambda>rv s. snd p \<notin> dom tcb_cap_cases\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma ex_nonz_cap_to_pres:
  assumes y: "\<And>P p. \<lbrace>cte_wp_at P p\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace>"
  shows      "\<lbrace>ex_nonz_cap_to p\<rbrace> f \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>" apply (simp only: ex_nonz_cap_to_def not_ex) apply (intro hoare_vcg_disj_lift hoare_vcg_ex_lift
               y hoare_vcg_all_lift valid_cte_at_neg_typ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to p\<rbrace> f \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>cref. cte_wp_at (\<lambda>c. p \<in> zobj_refs c) cref s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at (\<lambda>c. p \<in> zobj_refs c) cref s\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma set_simple_ko_ex_cap[wp]:
  "set_simple_ko f p' v \<lbrace>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_simple_ko f p' v \<lbrace>\<lambda>_. ex_nonz_cap_to p\<rbrace>
theory KHeap_AI

lemma set_simple_ko_idle[wp]:
  "\<lbrace>obj_at (\<lambda>ko. partial_inv f ko \<noteq> None) ptr and valid_idle\<rbrace>
   set_simple_ko f ptr ep \<lbrace>\<lambda>_. valid_idle\<rbrace>" by (set_simple_ko_method simp_thm: obj_at_def valid_idle_def pred_tcb_at_def
                             wp_thm: set_object_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at (\<lambda>ko. partial_inv f ko \<noteq> None) ptr and valid_idle\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>_. valid_idle\<rbrace>