kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_AI

lemma get_simple_ko_valid_obj[wp]:
  "\<lbrace> valid_objs and obj_at (\<lambda>ko. bound (partial_inv f ko)) ep \<rbrace>
   get_simple_ko f ep
   \<lbrace> \<lambda>r. valid_obj ep (f r) \<rbrace>" apply (simp add: get_simple_ko_def) apply (rule hoare_seq_ext) prefer 2 apply (rule hoare_pre_imp [OF _ get_object_valid]) apply (simp add: invs_def valid_state_def valid_pspace_def) apply (wpsimp simp: partial_inv_def the_equality valid_obj_def
               split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and obj_at (\<lambda>ko. partial_inv f ko \<noteq> None) ep\<rbrace> get_simple_ko f ep \<lbrace>\<lambda>r. valid_obj ep (f r)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and obj_at (\<lambda>ko. \<exists>y. partial_inv f ko = Some y) ep\<rbrace> do kobj <- get_object ep;
y <- assert (a_type kobj = AEndpoint \<or> a_type kobj = ANTFN);
case partial_inv f kobj of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od \<lbrace>\<lambda>r. valid_obj ep (f r)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>kobj. \<lbrace>?B kobj\<rbrace> do y <- assert (a_type kobj = AEndpoint \<or> a_type kobj = ANTFN);
case partial_inv f kobj of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od \<lbrace>\<lambda>r. valid_obj ep (f r)\<rbrace>
 2. \<lbrace>valid_objs and obj_at (\<lambda>ko. \<exists>y. partial_inv f ko = Some y) ep\<rbrace> get_object ep \<lbrace>?B\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>valid_objs and obj_at (\<lambda>ko. \<exists>y. partial_inv f ko = Some y) ep\<rbrace> get_object ep \<lbrace>?B\<rbrace>
 2. \<And>kobj. \<lbrace>?B kobj\<rbrace> do y <- assert (a_type kobj = AEndpoint \<or> a_type kobj = ANTFN);
case partial_inv f kobj of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od \<lbrace>\<lambda>r. valid_obj ep (f r)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_objs and obj_at (\<lambda>ko. \<exists>y. partial_inv f ko = Some y) ep) s \<Longrightarrow> valid_objs s
 2. \<And>kobj. \<lbrace>valid_obj ep kobj\<rbrace> do y <- assert (a_type kobj = AEndpoint \<or> a_type kobj = ANTFN);
case partial_inv f kobj of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od \<lbrace>\<lambda>r. valid_obj ep (f r)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>kobj. \<lbrace>valid_obj ep kobj\<rbrace> do y <- assert (a_type kobj = AEndpoint \<or> a_type kobj = ANTFN);
case partial_inv f kobj of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od \<lbrace>\<lambda>r. valid_obj ep (f r)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma get_simple_ko_valid_simple_obj[wp]:
  notes valid_simple_obj_def[simp del]
  shows
  "\<lbrace> valid_objs and obj_at (\<lambda>ko. bound (partial_inv f ko)) ep \<rbrace>
   get_simple_ko f ep
   \<lbrace> \<lambda>r. valid_simple_obj (f r) \<rbrace>" apply (simp add: get_simple_ko_def) apply (rule hoare_seq_ext) prefer 2 apply (rule hoare_pre_imp [OF _ get_object_valid]) apply (simp add: invs_def valid_state_def valid_pspace_def) apply (wpsimp simp: partial_inv_def the_equality valid_obj_imp_valid_simple
              split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and obj_at (\<lambda>ko. partial_inv f ko \<noteq> None) ep\<rbrace> get_simple_ko f ep \<lbrace>\<lambda>r. valid_simple_obj (f r)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and obj_at (\<lambda>ko. \<exists>y. partial_inv f ko = Some y) ep\<rbrace> do kobj <- get_object ep;
y <- assert (a_type kobj = AEndpoint \<or> a_type kobj = ANTFN);
case partial_inv f kobj of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od \<lbrace>\<lambda>r. valid_simple_obj (f r)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>kobj. \<lbrace>?B kobj\<rbrace> do y <- assert (a_type kobj = AEndpoint \<or> a_type kobj = ANTFN);
case partial_inv f kobj of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od \<lbrace>\<lambda>r. valid_simple_obj (f r)\<rbrace>
 2. \<lbrace>valid_objs and obj_at (\<lambda>ko. \<exists>y. partial_inv f ko = Some y) ep\<rbrace> get_object ep \<lbrace>?B\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>valid_objs and obj_at (\<lambda>ko. \<exists>y. partial_inv f ko = Some y) ep\<rbrace> get_object ep \<lbrace>?B\<rbrace>
 2. \<And>kobj. \<lbrace>?B kobj\<rbrace> do y <- assert (a_type kobj = AEndpoint \<or> a_type kobj = ANTFN);
case partial_inv f kobj of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od \<lbrace>\<lambda>r. valid_simple_obj (f r)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_objs and obj_at (\<lambda>ko. \<exists>y. partial_inv f ko = Some y) ep) s \<Longrightarrow> valid_objs s
 2. \<And>kobj. \<lbrace>valid_obj ep kobj\<rbrace> do y <- assert (a_type kobj = AEndpoint \<or> a_type kobj = ANTFN);
case partial_inv f kobj of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od \<lbrace>\<lambda>r. valid_simple_obj (f r)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>kobj. \<lbrace>valid_obj ep kobj\<rbrace> do y <- assert (a_type kobj = AEndpoint \<or> a_type kobj = ANTFN);
case partial_inv f kobj of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od \<lbrace>\<lambda>r. valid_simple_obj (f r)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma get_ntfn_valid_ntfn[wp]:
  "\<lbrace> valid_objs and ntfn_at ntfn \<rbrace>
   get_notification ntfn
   \<lbrace> valid_ntfn \<rbrace>" by (wpsimp simp: ntfn_at_def2 valid_ntfn_def2 simp_del: valid_simple_obj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and ntfn_at ntfn\<rbrace> get_notification ntfn \<lbrace>valid_ntfn\<rbrace>
theory KHeap_AI

lemma get_ep_valid_ep[wp]:
  "\<lbrace> invs and ep_at ep \<rbrace>
   get_endpoint ep
   \<lbrace> valid_ep \<rbrace>" by (wpsimp simp: ep_at_def2 valid_ep_def2 simp_del: valid_simple_obj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ep_at ep\<rbrace> get_endpoint ep \<lbrace>valid_ep\<rbrace>
theory KHeap_AI

lemma set_simple_ko_valid_objs[wp]:
  "\<lbrace> valid_objs
     and valid_simple_obj (f v) and K (is_simple_type (f v))\<rbrace> set_simple_ko f ptr v \<lbrace>\<lambda>rv s. valid_objs s\<rbrace>" unfolding set_simple_ko_def by (wpsimp wp: set_object_valid_objs[THEN hoare_set_object_weaken_pre]
           simp: valid_obj_def obj_at_def a_type_def partial_inv_def valid_ntfn_def2 valid_ep_def2
          split: kernel_object.splits
       simp_del: valid_simple_obj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_simple_obj (f v) and K (is_simple_type (f v))\<rbrace> set_simple_ko f ptr v \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_simple_obj (f v) and K (is_simple_type (f v))\<rbrace> do obj <- get_object ptr;
assert (is_simple_type obj);
assert (partial_inv f obj \<noteq> None);
set_object ptr (f v)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace>
theory KHeap_AI

lemma set_simple_ko_aligned[wp]:
 "set_simple_ko f ptr v \<lbrace>pspace_aligned\<rbrace>" by (set_simple_ko_method wp_thm: set_object_aligned[THEN hoare_set_object_weaken_pre])

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

lemma set_simple_ko_typ_at [wp]:
  "set_simple_ko f p' ep \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace>" by (set_simple_ko_method wp_thm: set_object_typ_at)

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

lemma set_simple_ko_cte_wp_at [wp]:
  "set_simple_ko f p' ep \<lbrace>cte_wp_at P p\<rbrace>" by (set_simple_ko_method wp_thm: set_object_wp simp_thm: cte_wp_at_cases; fastforce)

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

lemma obj_set_prop_at:
  "\<lbrace>\<lambda>s. P obj \<rbrace> set_object p obj \<lbrace>\<lambda>rv. obj_at P p\<rbrace>" apply (simp add: set_object_def) apply wp apply (simp add: obj_at_def) done

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

lemma set_simple_ko_refs_of[wp]:
 "\<lbrace>\<lambda>s. P ((state_refs_of s) (ep := refs_of (f val)))\<rbrace>
    set_simple_ko f ep val
  \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>" apply (set_simple_ko_method  wp_thm: set_object_wp simp_thm: set_object_def) by (fastforce simp: state_refs_of_def elim!: rsubst[where P=P])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of s)(ep := refs_of (f val)))\<rbrace> set_simple_ko f ep val \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. P ((state_refs_of s)(ep := refs_of (f val))) \<Longrightarrow> (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> kheap s ep = Some (Endpoint x3) \<longrightarrow> P (state_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> f val)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> kheap s ep = Some (Notification x4) \<longrightarrow> P (state_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> f val)\<rparr>)))
theory KHeap_AI

lemma set_ep_refs_of[wp]:
 "\<lbrace>\<lambda>s. P ((state_refs_of s) (ep := ep_q_refs_of val))\<rbrace>
    set_endpoint ep val
  \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>" by (wp; fastforce simp: state_refs_of_def elim!: rsubst[where P=P])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of s)(ep := ep_q_refs_of val))\<rbrace> set_endpoint ep val \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>
theory KHeap_AI

lemma set_ntfn_refs_of[wp]:
  "\<lbrace>\<lambda>s. P ((state_refs_of s) (ntfnptr := ntfn_q_refs_of (ntfn_obj ntfn) \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)))\<rbrace>
     set_notification ntfnptr ntfn
   \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>" by (wp; fastforce simp: state_refs_of_def elim!: rsubst[where P=P])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of s)(ntfnptr := ntfn_q_refs_of (ntfn_obj ntfn) \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)))\<rbrace> set_notification ntfnptr ntfn \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>
theory KHeap_AI

lemma pspace_distinct_same_type:
  "\<lbrakk> kheap s t = Some ko; a_type ko = a_type ko';  pspace_distinct s\<rbrakk>
    \<Longrightarrow> pspace_distinct (s\<lparr>kheap := (kheap s)(t \<mapsto> ko')\<rparr>)" apply (clarsimp simp add: pspace_distinct_def obj_bits_T) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s t = Some ko; a_type ko = a_type ko'; pspace_distinct s\<rbrakk> \<Longrightarrow> pspace_distinct (s\<lparr>kheap := (kheap s)(t \<mapsto> ko')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>kheap s t = Some ko; a_type ko = a_type ko'; \<forall>x y ko ko'. kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y \<longrightarrow> x \<le> y + (2 ^ obj_bits_type (a_type ko') - 1) \<longrightarrow> y \<le> x + (2 ^ obj_bits_type (a_type ko) - 1) \<longrightarrow> x \<le> x + (2 ^ obj_bits_type (a_type ko) - 1) \<longrightarrow> \<not> y \<le> y + (2 ^ obj_bits_type (a_type ko') - 1)\<rbrakk> \<Longrightarrow> (x = t \<longrightarrow> (\<forall>y. y \<noteq> t \<longrightarrow> (\<forall>ko'a. kheap s y = Some ko'a \<longrightarrow> t \<le> y + (2 ^ obj_bits_type (a_type ko'a) - 1) \<longrightarrow> y \<le> t + (2 ^ obj_bits_type (a_type ko') - 1) \<longrightarrow> t \<le> t + (2 ^ obj_bits_type (a_type ko') - 1) \<longrightarrow> \<not> y \<le> y + (2 ^ obj_bits_type (a_type ko'a) - 1)))) \<and> (x \<noteq> t \<longrightarrow> (\<forall>y. (y = t \<longrightarrow> (\<forall>ko. kheap s x = Some ko \<longrightarrow> x \<le> t + (2 ^ obj_bits_type (a_type ko') - 1) \<longrightarrow> t \<le> x + (2 ^ obj_bits_type (a_type ko) - 1) \<longrightarrow> x \<le> x + (2 ^ obj_bits_type (a_type ko) - 1) \<longrightarrow> \<not> t \<le> t + (2 ^ obj_bits_type (a_type ko') - 1))) \<and> (y \<noteq> t \<longrightarrow> (\<forall>ko ko'. kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y \<longrightarrow> x \<le> y + (2 ^ obj_bits_type (a_type ko') - 1) \<longrightarrow> y \<le> x + (2 ^ obj_bits_type (a_type ko) - 1) \<longrightarrow> x \<le> x + (2 ^ obj_bits_type (a_type ko) - 1) \<longrightarrow> \<not> y \<le> y + (2 ^ obj_bits_type (a_type ko') - 1))))) proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma set_object_distinct[wp]:
  "set_object p ko' \<lbrace>pspace_distinct\<rbrace>" by (wpsimp wp: set_object_wp_strong simp: obj_at_def pspace_distinct_same_type)

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

lemma set_simple_ko_distinct[wp]:
  "set_simple_ko f ep v \<lbrace>pspace_distinct\<rbrace>" by (set_simple_ko_method wp_thm: set_object_distinct[THEN hoare_set_object_weaken_pre])

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

lemma set_simple_ko_cur_tcb[wp]:
  "set_simple_ko f ep v \<lbrace>cur_tcb\<rbrace>" by (set_simple_ko_method wp_thm: set_object_wp simp_thm: cur_tcb_def is_tcb is_ep; fastforce)

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

lemma assert_pre:
  "\<lbrace>P\<rbrace> do s <- get; assert (P s); f od \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" by (simp add: valid_def assert_def get_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do s <- get;
assert (P s);
f
od \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>
theory KHeap_AI

lemma set_object_pspace_in_kernel_window:
  "set_object p k \<lbrace>pspace_in_kernel_window\<rbrace>" unfolding set_object_def apply (rule assert_pre) apply (rule hoare_pre) apply (rule pspace_in_kernel_window_atyp_lift) apply (wp; clarsimp simp add: obj_at_def)+ by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> set_object p k \<lbrace>\<lambda>_. pspace_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> do kobj <- get_object p;
assert (a_type kobj = a_type k);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
od \<lbrace>\<lambda>_. pspace_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> do s <- get;
assert (pspace_in_kernel_window s);
kobj <- get_object p;
assert (a_type kobj = a_type k);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
od \<lbrace>\<lambda>_. pspace_in_kernel_window\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> do s <- get;
assert (pspace_in_kernel_window s);
kobj <- get_object p;
assert (a_type kobj = a_type k);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
od \<lbrace>\<lambda>_. pspace_in_kernel_window\<rbrace>
 2. \<And>s. pspace_in_kernel_window s \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>P pa T. \<lbrace>\<lambda>s. P (typ_at T pa s)\<rbrace> do s <- get;
assert (pspace_in_kernel_window s);
kobj <- get_object p;
assert (a_type kobj = a_type k);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
od \<lbrace>\<lambda>_ s. P (typ_at T pa s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> do s <- get;
assert (pspace_in_kernel_window s);
kobj <- get_object p;
assert (a_type kobj = a_type k);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
od \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>
 3. \<And>s. pspace_in_kernel_window s \<Longrightarrow> pspace_in_kernel_window s proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_in_kernel_window s \<Longrightarrow> pspace_in_kernel_window s
theory KHeap_AI

lemma set_object_pspace_respects_device_region:
  "set_object p k \<lbrace>pspace_respects_device_region\<rbrace>" apply (simp add: set_object_def, wp) apply (clarsimp simp: pspace_respects_device_region_def
                        device_mem_obj_upd_dom user_mem_obj_upd_dom
                        obj_at_def in_user_frame_obj_upd in_device_frame_obj_upd
                 split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_respects_device_region\<rbrace> set_object p k \<lbrace>\<lambda>_. pspace_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_respects_device_region s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko = a_type k \<longrightarrow> pspace_respects_device_region (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma set_simple_ko_kernel_window[wp]:
  "set_simple_ko f ptr val \<lbrace>pspace_in_kernel_window\<rbrace>" by (set_simple_ko_method
        wp_thm: set_object_pspace_in_kernel_window[THEN hoare_set_object_weaken_pre])

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

lemma set_simple_ko_respect_device_region[wp]:
  "set_simple_ko f ptr val \<lbrace>pspace_respects_device_region\<rbrace>" by (set_simple_ko_method
        wp_thm: set_object_pspace_respects_device_region[THEN hoare_set_object_weaken_pre])

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

lemma swp_apply [simp]:
  "swp f x y = f y x" by (simp add: swp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. swp f x y = f y x
theory KHeap_AI

lemma hoare_cte_wp_caps_of_state_lift:
  assumes c: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (caps_of_state s)\<rbrace>"
  shows "\<lbrace>\<lambda>s. cte_wp_at P p s\<rbrace> f \<lbrace>\<lambda>r s. cte_wp_at P p s\<rbrace>" apply (simp add: cte_wp_at_caps_of_state) apply (rule c) done

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

lemma set_simple_ko_caps_of_state [wp]:
  "set_simple_ko f p ep \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace>" apply (set_simple_ko_method simp_thm: bind_assoc wp_thm: set_object_wp_strong) apply (rule conjI; clarsimp split: if_splits; subst cte_wp_caps_of_lift; assumption?) apply (auto simp: cte_wp_at_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_simple_ko f p ep \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (caps_of_state s) \<Longrightarrow> (\<forall>x3. f ep = Endpoint x3 \<longrightarrow> (\<forall>x3a. (\<exists>!y. f y = Endpoint x3a) \<longrightarrow> kheap s p = Some (Endpoint x3a) \<longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> Endpoint x3)\<rparr>)))) \<and> (\<forall>x4. f ep = Notification x4 \<longrightarrow> (\<forall>x4a. (\<exists>!y. f y = Notification x4a) \<longrightarrow> kheap s p = Some (Notification x4a) \<longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> Notification x4)\<rparr>)))) proof (prove)
goal (2 subgoals):
 1. \<And>s x3 x3a y pa Pa. \<lbrakk>P (caps_of_state s); f ep = Endpoint x3; f y = Endpoint x3a; \<forall>y y'. f y = Endpoint x3a \<and> f y' = Endpoint x3a \<longrightarrow> y = y'; kheap s p = Some (Endpoint x3a)\<rbrakk> \<Longrightarrow> cte_wp_at Pa pa (s\<lparr>kheap := (kheap s)(p \<mapsto> Endpoint x3)\<rparr>) = cte_wp_at Pa pa s
 2. \<And>s x4 x4a y pa Pa. \<lbrakk>P (caps_of_state s); f ep = Notification x4; f y = Notification x4a; \<forall>y y'. f y = Notification x4a \<and> f y' = Notification x4a \<longrightarrow> y = y'; kheap s p = Some (Notification x4a)\<rbrakk> \<Longrightarrow> cte_wp_at Pa pa (s\<lparr>kheap := (kheap s)(p \<mapsto> Notification x4)\<rparr>) = cte_wp_at Pa pa s proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma set_simple_ko_revokable [wp]:
  "set_simple_ko f p ep \<lbrace>\<lambda> s. P (is_original_cap s)\<rbrace>" by (set_simple_ko_method wp_thm: set_object_wp)

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

lemma set_ep_mdb [wp]:
  "set_simple_ko f p ep \<lbrace>valid_mdb\<rbrace>" by (wp valid_mdb_lift)

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

lemma cte_wp_at_after_update:
  "\<lbrakk> obj_at (same_caps val) p' s \<rbrakk>
    \<Longrightarrow> cte_wp_at P p (kheap_update (\<lambda>a b. if b = p' then Some val else kheap s b) s)
         = cte_wp_at P p s" by (fastforce simp: obj_at_def cte_wp_at_cases split: if_split_asm dest: bspec [OF _ ranI])

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

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

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

lemma ex_cap_to_after_update':
  "\<lbrakk> ex_nonz_cap_to p s; obj_at (same_caps val) p' s \<rbrakk>
     \<Longrightarrow> ex_nonz_cap_to p (s\<lparr>kheap := (kheap s)(p' \<mapsto> val)\<rparr>)" by (clarsimp simp: ex_nonz_cap_to_def cte_wp_at_after_update')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ex_nonz_cap_to p s; obj_at (same_caps val) p' s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to p (s\<lparr>kheap := (kheap s)(p' \<mapsto> val)\<rparr>)