kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchKHeap_AI

lemma valid_ioports_lift:
  assumes x: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>"
  assumes y: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>rv s. P (arch_state s)\<rbrace>"
  shows      "\<lbrace>valid_ioports\<rbrace> f \<lbrace>\<lambda>rv. valid_ioports\<rbrace>" apply simp 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_ioports\<rbrace> f \<lbrace>\<lambda>rv. valid_ioports\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. True\<rbrace> f \<lbrace>\<lambda>rv s. True\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma valid_arch_mdb_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>"
  assumes r: "\<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> f \<lbrace>\<lambda>r s. P (is_original_cap s)\<rbrace>"
  shows "\<lbrace>\<lambda>s. valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>r s. valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace>" apply (clarsimp simp: valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>r s. valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma get_simple_ko_wp:
  "\<lbrace>\<lambda>s. \<forall>ntfn. ko_at (f ntfn) ntfnptr s \<longrightarrow> P ntfn s\<rbrace> get_simple_ko f ntfnptr \<lbrace>P\<rbrace>" by get_simple_ko_method

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ntfn. ko_at (f ntfn) ntfnptr s \<longrightarrow> P ntfn s\<rbrace> get_simple_ko f ntfnptr \<lbrace>P\<rbrace>
theory KHeap_AI

lemma get_object_inv [wp]: "\<lbrace>P\<rbrace> get_object t \<lbrace>\<lambda>rv. P\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_object t \<lbrace>\<lambda>rv. P\<rbrace>
theory KHeap_AI

lemma get_tcb_rev:
  "kheap s p = Some (TCB t)\<Longrightarrow> get_tcb p s = Some t" by (clarsimp simp:get_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s p = Some (TCB t) \<Longrightarrow> get_tcb p s = Some t
theory KHeap_AI

lemma get_tcb_obj_atE[elim!]:
  "\<lbrakk> get_tcb t s = Some tcb; get_tcb t s = Some tcb \<Longrightarrow> P (TCB tcb) \<rbrakk> \<Longrightarrow> obj_at P t s" by (clarsimp dest!: get_tcb_SomeD simp: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_tcb t s = Some tcb; get_tcb t s = Some tcb \<Longrightarrow> P (TCB tcb)\<rbrakk> \<Longrightarrow> obj_at P t s
theory KHeap_AI

lemma a_type_TCB[simp]:
  "a_type (TCB x) = ATCB" by (simp add: a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a_type (TCB x) = ATCB
theory KHeap_AI

lemma pspace_aligned_obj_update:
  assumes obj: "obj_at P t s"
  assumes pa: "pspace_aligned s"
  assumes R: "\<And>k. P k \<Longrightarrow> a_type k = a_type k'"
  shows "pspace_aligned (s\<lparr>kheap := (kheap s)(t \<mapsto> k')\<rparr>)" using pa obj apply (simp add: pspace_aligned_def cong: conj_cong) apply (clarsimp simp: obj_at_def obj_bits_T dest!: R) apply (fastforce dest: bspec [OF _ domI]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_aligned (s\<lparr>kheap := (kheap s)(t \<mapsto> k')\<rparr>) proof (prove)
using this:
pspace_aligned s
obj_at P t s

goal (1 subgoal):
 1. pspace_aligned (s\<lparr>kheap := (kheap s)(t \<mapsto> k')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); obj_at P t s\<rbrakk> \<Longrightarrow> is_aligned t (obj_bits k') proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>\<forall>x\<in>dom (kheap s). is_aligned x (obj_bits_type (a_type (the (kheap s x)))); kheap s t = Some ko; a_type ko = a_type k'\<rbrakk> \<Longrightarrow> is_aligned t (obj_bits_type (a_type k')) proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma cte_at_same_type:
  "\<lbrakk>cte_at t s; a_type k = a_type ko; kheap s p = Some ko\<rbrakk>
  \<Longrightarrow> cte_at t (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)" apply (clarsimp simp: cte_at_cases del: disjCI) apply (elim exE disjE) apply (clarsimp simp: a_type_def well_formed_cnode_n_def length_set_helper
                  split: Structures_A.kernel_object.split_asm
                         if_split_asm) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) t s; a_type k = a_type ko; kheap s p = Some ko\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) t (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<exists>sz fun. ko = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> snd t \<in> dom fun) \<or> (\<exists>tcb. ko = TCB tcb) \<and> snd t \<in> dom tcb_cap_cases; a_type k = a_type ko; kheap s (fst t) = Some ko; p = fst t\<rbrakk> \<Longrightarrow> (\<exists>sz fun. k = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> snd t \<in> dom fun) \<or> (\<exists>tcb. k = TCB tcb) \<and> snd t \<in> dom tcb_cap_cases proof (prove)
goal (2 subgoals):
 1. \<And>sz fun. \<lbrakk>a_type k = a_type ko; kheap s (fst t) = Some ko; p = fst t; ko = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> snd t \<in> dom fun\<rbrakk> \<Longrightarrow> (\<exists>sz fun. k = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> snd t \<in> dom fun) \<or> (\<exists>tcb. k = TCB tcb) \<and> snd t \<in> dom tcb_cap_cases
 2. \<lbrakk>a_type k = a_type ko; kheap s (fst t) = Some ko; p = fst t; (\<exists>tcb. ko = TCB tcb) \<and> snd t \<in> dom tcb_cap_cases\<rbrakk> \<Longrightarrow> (\<exists>sz fun. k = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> snd t \<in> dom fun) \<or> (\<exists>tcb. k = TCB tcb) \<and> snd t \<in> dom tcb_cap_cases proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a_type k = a_type ko; kheap s (fst t) = Some ko; p = fst t; (\<exists>tcb. ko = TCB tcb) \<and> snd t \<in> dom tcb_cap_cases\<rbrakk> \<Longrightarrow> (\<exists>sz fun. k = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> snd t \<in> dom fun) \<or> (\<exists>tcb. k = TCB tcb) \<and> snd t \<in> dom tcb_cap_cases proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma untyped_same_type:
  "\<lbrakk>valid_untyped (cap.UntypedCap dev r n f) s; a_type k = a_type ko; kheap s p = Some ko\<rbrakk>
  \<Longrightarrow> valid_untyped (cap.UntypedCap dev r n f) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)" unfolding valid_untyped_def by (clarsimp simp: obj_range_def obj_bits_T)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_untyped (UntypedCap dev r n f) s; a_type k = a_type ko; kheap s p = Some ko\<rbrakk> \<Longrightarrow> valid_untyped (UntypedCap dev r n f) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> untyped_range (UntypedCap dev r n f) \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> untyped_range (UntypedCap dev r n f) \<and> usable_untyped_range (UntypedCap dev r n f) \<inter> obj_range p obj = {}; a_type k = a_type ko; kheap s p = Some ko\<rbrakk> \<Longrightarrow> \<forall>pa obj. kheap (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) pa = Some obj \<longrightarrow> obj_range pa obj \<inter> untyped_range (UntypedCap dev r n f) \<noteq> {} \<longrightarrow> obj_range pa obj \<subseteq> untyped_range (UntypedCap dev r n f) \<and> usable_untyped_range (UntypedCap dev r n f) \<inter> obj_range pa obj = {}
theory KHeap_AI

lemma set_object_valid_objs[wp]:
  "\<lbrace>valid_objs and valid_obj p k\<rbrace>
  set_object p k
  \<lbrace>\<lambda>r. valid_objs\<rbrace>" apply (wpsimp wp: set_object_wp_strong simp: obj_at_def) apply (clarsimp simp: valid_objs_def dom_def) apply (intro conjI impI; fastforce intro: valid_obj_same_type) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_obj p k\<rbrace> set_object p k \<lbrace>\<lambda>r. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>valid_objs s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow> valid_objs (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko ptr. \<lbrakk>\<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow> (ptr = p \<longrightarrow> valid_obj p k (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)) \<and> (ptr \<noteq> p \<longrightarrow> (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>))) proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma set_object_aligned[wp]:
  "set_object p k \<lbrace>pspace_aligned\<rbrace>" apply (wpsimp wp: set_object_wp_strong) apply (clarsimp elim!: pspace_aligned_obj_update) done

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

lemma assert_get_tcb:
  "\<lbrace> P \<rbrace> gets_the (get_tcb t) \<lbrace> \<lambda>r. P and tcb_at t \<rbrace>" by (clarsimp simp: valid_def in_monad gets_the_def tcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>r. P and tcb_at t\<rbrace>
theory KHeap_AI

lemma dxo_wp_weak[wp]:
  assumes xopv: "\<And>s f. P (trans_state f s) = P s"
  shows "\<lbrace>P\<rbrace> do_extended_op x \<lbrace>\<lambda>_. P\<rbrace>" unfolding do_extended_op_def apply (simp add: split_def) apply wp apply (clarsimp simp: mk_ef_def) apply (simp add: xopv[simplified trans_state_update']) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do_extended_op x \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do ex <- get;
(uu_, es') <- select_f (mk_ef (wrap_ext_op x ex));
modify (exst_update (\<lambda>_. exst es'))
od \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do ex <- get;
p <- select_f (mk_ef (wrap_ext_op x ex));
modify (exst_update (\<lambda>_. exst (snd p)))
od \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> \<forall>x\<in>fst (mk_ef (wrap_ext_op x s)). P (s\<lparr>exst := exst (snd x)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>P s; ((), b) \<in> fst (wrap_ext_op x s)\<rbrakk> \<Longrightarrow> P (s\<lparr>exst := exst b\<rparr>) proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma sts_ep_at_inv[wp]:
  "\<lbrace> ep_at ep \<rbrace> set_thread_state t s \<lbrace> \<lambda>rv. ep_at ep \<rbrace>" apply (simp add: set_thread_state_def) apply (wp | simp add: set_object_def)+ apply (clarsimp simp: obj_at_def is_ep is_tcb get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ep_at ep\<rbrace> set_thread_state t s \<lbrace>\<lambda>rv. ep_at ep\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ep_at ep\<rbrace> do tcb <- gets_the (get_tcb t);
y <- set_object t (TCB (tcb\<lparr>tcb_state := s\<rparr>));
do_extended_op (set_thread_state_ext t)
od \<lbrace>\<lambda>rv. ep_at ep\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. ep_at ep sa \<Longrightarrow> (\<exists>y. get_tcb t sa = Some y) \<longrightarrow> (\<forall>ko. ko_at ko t sa \<longrightarrow> a_type ko = ATCB \<longrightarrow> ep_at ep (sa\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t sa)\<lparr>tcb_state := s\<rparr>)) else kheap sa a\<rparr>)) proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma sts_ntfn_at_inv[wp]:
  "\<lbrace> ntfn_at ep \<rbrace> set_thread_state t s \<lbrace> \<lambda>rv. ntfn_at ep \<rbrace>" apply (simp add: set_thread_state_def) apply (wp | simp add: set_object_def)+ apply (clarsimp simp: obj_at_def is_ntfn is_tcb get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ntfn_at ep\<rbrace> set_thread_state t s \<lbrace>\<lambda>rv. ntfn_at ep\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ntfn_at ep\<rbrace> do tcb <- gets_the (get_tcb t);
y <- set_object t (TCB (tcb\<lparr>tcb_state := s\<rparr>));
do_extended_op (set_thread_state_ext t)
od \<lbrace>\<lambda>rv. ntfn_at ep\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. ntfn_at ep sa \<Longrightarrow> (\<exists>y. get_tcb t sa = Some y) \<longrightarrow> (\<forall>ko. ko_at ko t sa \<longrightarrow> a_type ko = ATCB \<longrightarrow> ntfn_at ep (sa\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t sa)\<lparr>tcb_state := s\<rparr>)) else kheap sa a\<rparr>)) proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma sbn_ep_at_inv[wp]:
  "\<lbrace> ep_at ep \<rbrace> set_bound_notification t ntfn \<lbrace> \<lambda>rv. ep_at ep \<rbrace>" apply (simp add: set_bound_notification_def) apply (wp | simp add: set_object_def)+ apply (clarsimp simp: obj_at_def is_ep is_tcb get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ep_at ep\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. ep_at ep\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ep_at ep\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od \<lbrace>\<lambda>rv. ep_at ep\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ep_at ep s \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<forall>ko. ko_at ko t s \<longrightarrow> a_type ko = ATCB \<longrightarrow> ep_at ep (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_bound_notification := ntfn\<rparr>)) else kheap s a\<rparr>)) proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma sbn_ntfn_at_inv[wp]:
  "\<lbrace> ntfn_at ep \<rbrace> set_bound_notification t ntfn \<lbrace> \<lambda>rv. ntfn_at ep \<rbrace>" apply (simp add: set_bound_notification_def) apply (wp | simp add: set_object_def)+ apply (clarsimp simp: obj_at_def is_ntfn is_tcb get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ntfn_at ep\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. ntfn_at ep\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ntfn_at ep\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od \<lbrace>\<lambda>rv. ntfn_at ep\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ntfn_at ep s \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<forall>ko. ko_at ko t s \<longrightarrow> a_type ko = ATCB \<longrightarrow> ntfn_at ep (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_bound_notification := ntfn\<rparr>)) else kheap s a\<rparr>)) proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma set_cdt_inv:
  assumes P: "\<And>s. P s \<Longrightarrow> P (cdt_update (\<lambda>_. m) s)"
  shows "\<lbrace>P\<rbrace> set_cdt m \<lbrace>\<lambda>_. P\<rbrace>" apply (simp add: set_cdt_def) apply wp apply (erule P) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> set_cdt m \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do s <- get;
put (s\<lparr>cdt := m\<rparr>)
od \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> P (s\<lparr>cdt := m\<rparr>) proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma set_object_at_obj3:
  "\<lbrace>K (P obj)\<rbrace> set_object p obj \<lbrace>\<lambda>rv. obj_at P p\<rbrace>" by (clarsimp simp: set_object_def obj_at_def valid_def in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (P obj)\<rbrace> set_object p obj \<lbrace>\<lambda>rv. obj_at P p\<rbrace>
theory KHeap_AI

lemma set_object_valid_cap:
  "set_object p ko \<lbrace>valid_cap c\<rbrace>" by (wpsimp wp: set_object_wp_strong simp: obj_at_def valid_cap_same_type)

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

lemma set_object_cte_at:
  "set_object p ko \<lbrace>cte_at c\<rbrace>" by (wpsimp wp: set_object_wp_strong simp: obj_at_def cte_at_same_type)

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

lemma obj_at_ko_atD:
  "obj_at P x s \<Longrightarrow> \<exists>k. ko_at k x s \<and> P k" by (clarsimp simp: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at P x s \<Longrightarrow> \<exists>k. ko_at k x s \<and> P k
theory KHeap_AI

lemma set_object_ko:
  "\<lbrace>ko_at obj ptr and K (x \<noteq> ptr)\<rbrace> set_object x ko \<lbrace>\<lambda>rv. ko_at obj ptr\<rbrace>" by (clarsimp simp add: valid_def set_object_def get_object_def in_monad obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_at obj ptr and K (x \<noteq> ptr)\<rbrace> set_object x ko \<lbrace>\<lambda>rv. ko_at obj ptr\<rbrace>
theory KHeap_AI

lemma set_object_ko_at:
  "\<lbrace>\<top>\<rbrace> set_object p ko \<lbrace>\<lambda>_. ko_at ko p\<rbrace>" by (wpsimp wp: set_object_wp simp: obj_at_def)

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

lemma get_simple_ko_sp:
  "\<lbrace>P\<rbrace> get_simple_ko f p \<lbrace>\<lambda>ep. ko_at (f ep) p and P\<rbrace>" by get_simple_ko_method

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_simple_ko f p \<lbrace>\<lambda>ep. ko_at (f ep) p and P\<rbrace>
theory KHeap_AI

lemma get_simple_ko_inv[wp]: "\<lbrace>P\<rbrace> get_simple_ko f ep \<lbrace>\<lambda>rv. P\<rbrace>" by get_simple_ko_method

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_simple_ko f ep \<lbrace>\<lambda>rv. P\<rbrace>
theory KHeap_AI

lemma get_simple_ko_actual_ko[wp]:
  "\<lbrace> obj_at (\<lambda>ko. bound (partial_inv f ko)) ep \<rbrace>
   get_simple_ko f ep
   \<lbrace> \<lambda>rv. obj_at (\<lambda>k. k = f rv) ep \<rbrace>" by (fastforce simp: get_simple_ko_def get_object_def bind_def partial_inv_def
                             valid_def gets_def get_def return_def in_fail
                             assert_def obj_at_def split_def the_equality
                   split: kernel_object.splits option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at (\<lambda>ko. partial_inv f ko \<noteq> None) ep\<rbrace> get_simple_ko f ep \<lbrace>\<lambda>rv. obj_at (\<lambda>k. k = f rv) ep\<rbrace>
theory KHeap_AI

lemma get_object_valid [wp]:
  "\<lbrace>valid_objs\<rbrace> get_object oref \<lbrace> valid_obj oref \<rbrace>" apply (simp add: get_object_def) apply wp apply (clarsimp simp add: valid_pspace_def valid_objs_def dom_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> get_object oref \<lbrace>valid_obj oref\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> do kh <- gets kheap;
y <- assert (\<exists>y. kh oref = Some y);
return (the (kh oref))
od \<lbrace>valid_obj oref\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs s \<Longrightarrow> (\<exists>y. kheap s oref = Some y) \<longrightarrow> valid_obj oref (the (kheap s oref)) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s oref = Some y\<rbrakk> \<Longrightarrow> valid_obj oref y s proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma get_object_valid_obj_simple [wp]:
  notes valid_simple_obj_def[simp del]
  shows
  "\<lbrace>valid_objs\<rbrace> get_object oref \<lbrace> valid_simple_obj \<rbrace>" apply (simp add: get_object_def) apply wp apply (clarsimp simp: valid_pspace_def valid_objs_def dom_def
                 intro!: valid_obj_imp_valid_simple) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> get_object oref \<lbrace>valid_simple_obj\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> do kh <- gets kheap;
y <- assert (\<exists>y. kh oref = Some y);
return (the (kh oref))
od \<lbrace>valid_simple_obj\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs s \<Longrightarrow> (\<exists>y. kheap s oref = Some y) \<longrightarrow> valid_simple_obj (the (kheap s oref)) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s oref = Some y\<rbrakk> \<Longrightarrow> valid_obj (?p9 s) y s proof (prove)
goal:
No subgoals!
theory KHeap_AI

lemma get_object_valid_simple [wp]:
  "\<lbrace>valid_simple_objs\<rbrace> get_object oref \<lbrace> valid_simple_obj \<rbrace>" apply (simp add: get_object_def) apply wp apply (clarsimp simp add: valid_pspace_def valid_simple_objs_def dom_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_simple_objs\<rbrace> get_object oref \<lbrace>valid_simple_obj\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_simple_objs\<rbrace> do kh <- gets kheap;
y <- assert (\<exists>y. kh oref = Some y);
return (the (kh oref))
od \<lbrace>valid_simple_obj\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_simple_objs s \<Longrightarrow> (\<exists>y. kheap s oref = Some y) \<longrightarrow> valid_simple_obj (the (kheap s oref)) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> (case obj of Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s | _ \<Rightarrow> True)); kheap s oref = Some y\<rbrakk> \<Longrightarrow> case y of Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s | _ \<Rightarrow> True proof (prove)
goal:
No subgoals!