kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_DP

lemma throw_on_none_wp:
  "\<lbrace>\<lambda>s. case x of None \<Rightarrow> Q s | Some y \<Rightarrow> P y s\<rbrace> throw_on_none x \<lbrace>P\<rbrace>, \<lbrace>\<lambda>r s. Q s\<rbrace>" apply (rule hoare_pre) apply (clarsimp simp:throw_on_none_def) apply (wp | wpc | simp)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case x of None \<Rightarrow> Q s | Some y \<Rightarrow> P y s\<rbrace> throw_on_none x \<lbrace>P\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> throw_on_none x \<lbrace>P\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace>
 2. \<And>s. case x of None \<Rightarrow> Q s | Some y \<Rightarrow> P y s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case x of None \<Rightarrow> throw | Some y \<Rightarrow> returnOk y \<lbrace>P\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace>
 2. \<And>s. case x of None \<Rightarrow> Q s | Some y \<Rightarrow> P y s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. case x of None \<Rightarrow> Q s | Some y \<Rightarrow> P y s \<Longrightarrow> (x = None \<longrightarrow> Q s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> P xa s) proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma throw_opt_wp:
  "\<lbrace>\<lambda>s. case x of None \<Rightarrow> Q s | Some y \<Rightarrow> P y s\<rbrace> throw_opt err x \<lbrace>P\<rbrace>, \<lbrace>\<lambda>r s. Q s\<rbrace>" apply (rule hoare_pre) apply (clarsimp simp:throw_opt_def) apply (wp | wpc | simp)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case x of None \<Rightarrow> Q s | Some y \<Rightarrow> P y s\<rbrace> throw_opt err x \<lbrace>P\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> throw_opt err x \<lbrace>P\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace>
 2. \<And>s. case x of None \<Rightarrow> Q s | Some y \<Rightarrow> P y s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case x of None \<Rightarrow> throwError err | Some v \<Rightarrow> returnOk v \<lbrace>P\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace>
 2. \<And>s. case x of None \<Rightarrow> Q s | Some y \<Rightarrow> P y s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. case x of None \<Rightarrow> Q s | Some y \<Rightarrow> P y s \<Longrightarrow> (x = None \<longrightarrow> Q s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> P xa s) proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma do_notification_transfer_sep_wp:
  "\<lbrace> cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c - \<and>* P)\<rbrace> do_notification_transfer thread
    \<lbrace>\<lambda>rv. cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c - \<and>* P)\<rbrace>" apply (simp add: do_notification_transfer_def) apply (rule hoare_pre) apply wp apply (rule hoare_post_imp[rotated]) apply (rule set_cap_wp) apply sep_solve apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c - \<and>* P)\<rbrace> do_notification_transfer thread \<lbrace>\<lambda>rv. cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c - \<and>* P)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c - \<and>* P)\<rbrace> do y <- set_cap (thread, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent thread
od \<lbrace>\<lambda>rv. cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c - \<and>* P)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do y <- set_cap (thread, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent thread
od \<lbrace>\<lambda>rv. cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c - \<and>* P)\<rbrace>
 2. \<And>s. cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c - \<and>* P) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_cap (thread, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>y. cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c - \<and>* P)\<rbrace>
 2. \<And>s. cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c - \<and>* P) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> set_cap (thread, tcb_pending_op_slot) RunningCap \<lbrace>?Q7\<rbrace>
 2. \<And>rv s. ?Q7 rv s \<Longrightarrow> cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c - \<and>* P) s
 3. \<And>s. cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c - \<and>* P) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* ?R10) s \<Longrightarrow> cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c - \<and>* P) s
 2. \<And>s. cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c - \<and>* P) s \<Longrightarrow> cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c - \<and>* ?R10) s proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c - \<and>* P) s \<Longrightarrow> cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c - \<and>* P) s proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma update_thread_tcb_at:
  "\<lbrace>K(\<forall>x. P (t x))\<rbrace>
    update_thread thread_ptr t \<lbrace>\<lambda>rv. tcb_at' P thread_ptr\<rbrace>" apply (rule hoare_pre) apply (simp add: update_thread_def set_object_def | wp modify_wp | wpc)+ apply (auto simp: no_pending_def object_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (\<forall>x. P (t x))\<rbrace> update_thread thread_ptr t \<lbrace>\<lambda>rv. tcb_at' P thread_ptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> update_thread thread_ptr t \<lbrace>\<lambda>rv. tcb_at' P thread_ptr\<rbrace>
 2. \<And>s. K (\<forall>x. P (t x)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>x. P (t x) \<Longrightarrow> (\<exists>y. cdl_objects s thread_ptr = Some y) \<longrightarrow> (the (cdl_objects s thread_ptr) = Endpoint \<longrightarrow> ?R36 (ds_id Endpoint) s) \<and> (the (cdl_objects s thread_ptr) = Notification \<longrightarrow> ?R37 (ds_id Notification) s) \<and> (\<forall>x. the (cdl_objects s thread_ptr) = Tcb x \<longrightarrow> tcb_at' P thread_ptr (s\<lparr>cdl_objects := \<lambda>a. if a = thread_ptr then Some (Tcb (t x)) else cdl_objects s a\<rparr>)) \<and> (\<forall>x. the (cdl_objects s thread_ptr) = CNode x \<longrightarrow> ?R39 (CNode x) x s) \<and> (\<forall>x. the (cdl_objects s thread_ptr) = AsidPool x \<longrightarrow> ?R40 (AsidPool x) x s) \<and> (\<forall>x. the (cdl_objects s thread_ptr) = PageTable x \<longrightarrow> ?R41 (PageTable x) x s) \<and> (\<forall>x. the (cdl_objects s thread_ptr) = PageDirectory x \<longrightarrow> ?R42 (PageDirectory x) x s) \<and> (\<forall>x. the (cdl_objects s thread_ptr) = Frame x \<longrightarrow> ?R43 (Frame x) x s) \<and> (the (cdl_objects s thread_ptr) = Untyped \<longrightarrow> ?R44 (ds_id Untyped) s) \<and> (\<forall>x. the (cdl_objects s thread_ptr) = IRQNode x \<longrightarrow> ?R45 (IRQNode x) x s) proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma corrupt_intents_no_pending:
  "no_pending s \<Longrightarrow> no_pending (corrupt_intents a b s)" apply (clarsimp simp: no_pending_def corrupt_intents_def opt_cap_def slots_of_def) apply (drule_tac x = oid in spec) apply (auto split: option.splits cdl_object.splits if_splits
              simp: object_slots_def option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_pending s \<Longrightarrow> no_pending (corrupt_intents a b s) proof (prove)
goal (1 subgoal):
 1. \<And>oid cap. \<lbrakk>\<forall>oid cap. (case cdl_objects s oid of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap; (case (cdl_objects s ++ (\<lambda>ptr. case cdl_objects s ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some b then Some (Tcb (tcb\<lparr>cdl_tcb_intent := a ptr\<rparr>)) else None | Some _ \<Rightarrow> None)) oid of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) tcb_pending_op_slot = Some cap; is_pending_cap cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>oid cap. \<lbrakk>(case (cdl_objects s ++ (\<lambda>ptr. case cdl_objects s ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some b then Some (Tcb (tcb\<lparr>cdl_tcb_intent := a ptr\<rparr>)) else None | Some _ \<Rightarrow> None)) oid of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) tcb_pending_op_slot = Some cap; is_pending_cap cap; \<forall>cap. (case cdl_objects s oid of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma detype_insert:
  "detype (insert a A) s = detype {a} (detype A s)" by (cases s, simp add: detype_def fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. detype (insert a A) s = detype {a} (detype A s)
theory Retype_DP

lemma detype_set_wp:
  "finite S \<Longrightarrow>
   \<lbrace><(\<And>* x\<in> S. x \<mapsto>o -) \<and>* R>\<rbrace>
    modify (detype S)
   \<lbrace>\<lambda>_. <(\<And>* x \<in> S. x \<mapsto>o Untyped) \<and>* R>\<rbrace>" apply (clarsimp simp: modify_def) apply wp apply (rule detype_set_sep_helper) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite S \<Longrightarrow> \<lbrace>cdl.lift (sep_map_set_conj sep_any_map_o S \<and>* R)\<rbrace> modify (detype S) \<lbrace>\<lambda>_. cdl.lift ((SETSEPCONJ x:S. x \<mapsto>o Untyped) \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (sep_map_set_conj sep_any_map_o S \<and>* R)\<rbrace> do s <- get;
put (detype S s)
od \<lbrace>\<lambda>_. cdl.lift ((SETSEPCONJ x:S. x \<mapsto>o Untyped) \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (sep_map_set_conj sep_any_map_o S \<and>* R) s \<Longrightarrow> cdl.lift ((SETSEPCONJ x:S. x \<mapsto>o Untyped) \<and>* R) (detype S s) proof (prove)
goal (2 subgoals):
 1. \<And>s. cdl.lift (sep_map_set_conj sep_any_map_o S \<and>* R) s \<Longrightarrow> finite S
 2. \<And>s. cdl.lift (sep_map_set_conj sep_any_map_o S \<and>* R) s \<Longrightarrow> cdl.lift (sep_map_set_conj sep_any_map_o S \<and>* R) s proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma set_parent_cdt_parent:
  "\<lbrace>\<lambda>s. cdl_cdt s slot = Some parent\<rbrace> set_parent param_a param_b \<lbrace>\<lambda>_ s. cdl_cdt s slot = Some parent\<rbrace>" apply (simp add: set_parent_def) apply wp apply (clarsimp simp add: ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl_cdt s slot = Some parent\<rbrace> set_parent param_a param_b \<lbrace>\<lambda>_ s. cdl_cdt s slot = Some parent\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl_cdt s slot = Some parent\<rbrace> do cdt <- gets cdl_cdt;
y <- assert (cdt param_a = None);
modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(param_a \<mapsto> param_b)\<rparr>)
od \<lbrace>\<lambda>_ s. cdl_cdt s slot = Some parent\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl_cdt s slot = Some parent \<Longrightarrow> cdl_cdt s param_a = None \<longrightarrow> cdl_cdt (s\<lparr>cdl_cdt := (cdl_cdt s)(param_a \<mapsto> param_b)\<rparr>) slot = Some parent proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma set_parent_cdl_parent:
   "\<lbrace>\<lambda>s. cdl_cdt s slot = Some parent\<rbrace>
     set_parent slot' parent'
   \<lbrace>\<lambda>_ s. cdl_cdt s slot = Some parent\<rbrace>" apply (simp add: set_parent_def) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl_cdt s slot = Some parent\<rbrace> set_parent slot' parent' \<lbrace>\<lambda>_ s. cdl_cdt s slot = Some parent\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl_cdt s slot = Some parent\<rbrace> do cdt <- gets cdl_cdt;
y <- assert (cdt slot' = None);
modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(slot' \<mapsto> parent')\<rparr>)
od \<lbrace>\<lambda>_ s. cdl_cdt s slot = Some parent\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl_cdt s slot = Some parent \<Longrightarrow> cdl_cdt s slot' = None \<longrightarrow> cdl_cdt (s\<lparr>cdl_cdt := (cdl_cdt s)(slot' \<mapsto> parent')\<rparr>) slot = Some parent proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma transfer_caps_loop_cdl_parent:
   "\<lbrace>\<lambda>s. cdl_cdt s slot = Some parent\<rbrace>
     transfer_caps_loop ep rcvr caps dest
   \<lbrace>\<lambda>_ s. cdl_cdt s slot = Some parent\<rbrace>" apply (induct caps arbitrary: dest; clarsimp split del: if_split) apply (rule hoare_pre) apply (wp crunch_wps | assumption
      | simp add: crunch_simps split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl_cdt s slot = Some parent\<rbrace> transfer_caps_loop ep rcvr caps dest \<lbrace>\<lambda>_ s. cdl_cdt s slot = Some parent\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a aa b caps dest. (\<And>dest. \<lbrace>\<lambda>s. cdl_cdt s slot = Some parent\<rbrace> transfer_caps_loop ep rcvr caps dest \<lbrace>\<lambda>_ s. cdl_cdt s slot = Some parent\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. cdl_cdt s slot = Some parent\<rbrace> if is_ep_cap a \<and> ep = Some (cap_object a) then do corrupt_ipc_buffer rcvr True;
transfer_caps_loop ep rcvr caps dest
od else if dest \<noteq> None then doE new_cap <- returnOk (update_cap_rights (cap_rights a - {AllowWrite}) a) \<sqinter> returnOk a;
target_cap <- derive_cap (aa, b) new_cap;
whenE (target_cap = NullCap) throw;
liftE (insert_cap_child target_cap (aa, b) (the dest) \<sqinter> insert_cap_sibling target_cap (aa, b) (the dest));
liftE $ transfer_caps_loop ep rcvr caps None
odE <catch> (\<lambda>_. return ()) else return () \<lbrace>\<lambda>_ s. cdl_cdt s slot = Some parent\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a aa b caps dest. (\<And>dest. \<lbrace>\<lambda>s. cdl_cdt s slot = Some parent\<rbrace> transfer_caps_loop ep rcvr caps dest \<lbrace>\<lambda>_ s. cdl_cdt s slot = Some parent\<rbrace>) \<Longrightarrow> \<lbrace>?Q7 a aa b caps dest\<rbrace> if is_ep_cap a \<and> ep = Some (cap_object a) then do corrupt_ipc_buffer rcvr True;
transfer_caps_loop ep rcvr caps dest
od else if dest \<noteq> None then doE new_cap <- returnOk (update_cap_rights (cap_rights a - {AllowWrite}) a) \<sqinter> returnOk a;
target_cap <- derive_cap (aa, b) new_cap;
whenE (target_cap = NullCap) throw;
liftE (insert_cap_child target_cap (aa, b) (the dest) \<sqinter> insert_cap_sibling target_cap (aa, b) (the dest));
liftE $ transfer_caps_loop ep rcvr caps None
odE <catch> (\<lambda>_. return ()) else return () \<lbrace>\<lambda>_ s. cdl_cdt s slot = Some parent\<rbrace>
 2. \<And>a aa b caps dest s. \<lbrakk>\<And>dest. \<lbrace>\<lambda>s. cdl_cdt s slot = Some parent\<rbrace> transfer_caps_loop ep rcvr caps dest \<lbrace>\<lambda>_ s. cdl_cdt s slot = Some parent\<rbrace>; cdl_cdt s slot = Some parent\<rbrakk> \<Longrightarrow> ?Q7 a aa b caps dest s proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma set_object_no_pending:
  "\<lbrace>no_pending and K(\<forall>cap. object_slots x tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)\<rbrace> set_object a x \<lbrace>\<lambda>rv. no_pending\<rbrace>" apply (clarsimp simp: set_object_def simpler_modify_def valid_def no_pending_def) apply (drule_tac x=oid in spec) apply (fastforce simp: opt_cap_def slots_of_def ran_def
                   split: option.split_asm if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_pending and K (\<forall>cap. object_slots x tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)\<rbrace> set_object a x \<lbrace>\<lambda>rv. no_pending\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s oid cap. \<lbrakk>\<forall>oid cap. opt_cap (oid, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; \<forall>cap. object_slots x tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap; opt_cap (oid, tcb_pending_op_slot) (s\<lparr>cdl_objects := (cdl_objects s)(a \<mapsto> x)\<rparr>) = Some cap; is_pending_cap cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s oid cap. \<lbrakk>\<forall>cap. object_slots x tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap; opt_cap (oid, tcb_pending_op_slot) (s\<lparr>cdl_objects := (cdl_objects s)(a \<mapsto> x)\<rparr>) = Some cap; is_pending_cap cap; \<forall>cap. opt_cap (oid, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma object_slots_upd_intent[simp]:
  "object_slots (Tcb (x\<lparr>cdl_tcb_intent := intent\<rparr>)) = object_slots (Tcb x)" by (clarsimp simp: object_slots_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_slots (Tcb (x\<lparr>cdl_tcb_intent := intent\<rparr>)) = object_slots (Tcb x)
theory Retype_DP

lemma no_pending_cong[cong]:
  "cdl_objects s = cdl_objects b \<Longrightarrow> no_pending s = no_pending b" by (clarsimp simp: no_pending_def opt_cap_def slots_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_objects s = cdl_objects b \<Longrightarrow> no_pending s = no_pending b
theory Retype_DP

lemma default_cap_not_pending[simp]:
  "\<not> is_pending_cap (default_cap a b c d)" by (simp add: default_cap_def is_pending_cap_def split: cdl_object_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_pending_cap (default_cap a b c d)
theory Retype_DP

lemma default_object_no_pending_cap:
  "\<lbrakk> default_object b c d = Some x2; object_slots x2 tcb_pending_op_slot = Some cap\<rbrakk>
    \<Longrightarrow> \<not> is_pending_cap cap" apply (case_tac b) apply (clarsimp simp: default_object_def object_slots_def default_tcb_def is_pending_cap_def
                        empty_cnode_def empty_cap_map_def empty_irq_node_def
                 split: if_split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>default_object b c d = Some x2; object_slots x2 tcb_pending_op_slot = Some cap\<rbrakk> \<Longrightarrow> \<not> is_pending_cap cap proof (prove)
goal (10 subgoals):
 1. \<lbrakk>default_object b c d = Some x2; object_slots x2 tcb_pending_op_slot = Some cap; b = EndpointType\<rbrakk> \<Longrightarrow> \<not> is_pending_cap cap
 2. \<lbrakk>default_object b c d = Some x2; object_slots x2 tcb_pending_op_slot = Some cap; b = NotificationType\<rbrakk> \<Longrightarrow> \<not> is_pending_cap cap
 3. \<lbrakk>default_object b c d = Some x2; object_slots x2 tcb_pending_op_slot = Some cap; b = TcbType\<rbrakk> \<Longrightarrow> \<not> is_pending_cap cap
 4. \<lbrakk>default_object b c d = Some x2; object_slots x2 tcb_pending_op_slot = Some cap; b = CNodeType\<rbrakk> \<Longrightarrow> \<not> is_pending_cap cap
 5. \<lbrakk>default_object b c d = Some x2; object_slots x2 tcb_pending_op_slot = Some cap; b = IRQNodeType\<rbrakk> \<Longrightarrow> \<not> is_pending_cap cap
 6. \<lbrakk>default_object b c d = Some x2; object_slots x2 tcb_pending_op_slot = Some cap; b = UntypedType\<rbrakk> \<Longrightarrow> \<not> is_pending_cap cap
 7. \<lbrakk>default_object b c d = Some x2; object_slots x2 tcb_pending_op_slot = Some cap; b = AsidPoolType\<rbrakk> \<Longrightarrow> \<not> is_pending_cap cap
 8. \<lbrakk>default_object b c d = Some x2; object_slots x2 tcb_pending_op_slot = Some cap; b = PageTableType\<rbrakk> \<Longrightarrow> \<not> is_pending_cap cap
 9. \<lbrakk>default_object b c d = Some x2; object_slots x2 tcb_pending_op_slot = Some cap; b = PageDirectoryType\<rbrakk> \<Longrightarrow> \<not> is_pending_cap cap
 10. \<And>x10. \<lbrakk>default_object b c d = Some x2; object_slots x2 tcb_pending_op_slot = Some cap; b = FrameType x10\<rbrakk> \<Longrightarrow> \<not> is_pending_cap cap proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma create_objects_no_pending[wp]:
  "\<lbrace>no_pending\<rbrace> create_objects a (default_object b c d) \<lbrace>\<lambda>rv. no_pending\<rbrace>" apply (simp add: create_objects_def, wp) apply (clarsimp simp: no_pending_def) apply (drule_tac x = oid in spec) apply (clarsimp simp: opt_cap_def default_object_no_pending_cap slots_of_def
                 split: if_splits option.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_pending\<rbrace> create_objects a (default_object b c d) \<lbrace>\<lambda>rv. no_pending\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. no_pending s \<Longrightarrow> no_pending (s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> set a then default_object b c d else cdl_objects s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s oid cap. \<lbrakk>\<forall>oid cap. opt_cap (oid, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; opt_cap (oid, tcb_pending_op_slot) (s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> set a then default_object b c d else cdl_objects s x\<rparr>) = Some cap; is_pending_cap cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s oid cap. \<lbrakk>opt_cap (oid, tcb_pending_op_slot) (s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> set a then default_object b c d else cdl_objects s x\<rparr>) = Some cap; is_pending_cap cap; \<forall>cap. opt_cap (oid, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma detype_no_pending:
  "no_pending s \<Longrightarrow> no_pending (detype S s)" apply (clarsimp simp: detype_def no_pending_def) apply (drule_tac x = oid in spec) apply (clarsimp simp: opt_cap_def slots_of_def object_slots_def split: if_splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_pending s \<Longrightarrow> no_pending (detype S s) proof (prove)
goal (1 subgoal):
 1. \<And>oid cap. \<lbrakk>\<forall>oid cap. opt_cap (oid, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; opt_cap (oid, tcb_pending_op_slot) (s\<lparr>cdl_objects := \<lambda>x. if x \<in> S then Some Untyped else cdl_objects s x\<rparr>) = Some cap; is_pending_cap cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>oid cap. \<lbrakk>opt_cap (oid, tcb_pending_op_slot) (s\<lparr>cdl_objects := \<lambda>x. if x \<in> S then Some Untyped else cdl_objects s x\<rparr>) = Some cap; is_pending_cap cap; \<forall>cap. opt_cap (oid, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma set_cap_no_pending_asm_in_pre:
  "\<lbrace>no_pending and K (snd slot = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap cap)\<rbrace>
    set_cap slot cap \<lbrace>\<lambda>rv s. no_pending s\<rbrace>" by (rule hoare_gen_asm, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_pending and K (snd slot = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap cap)\<rbrace> set_cap slot cap \<lbrace>\<lambda>rv. no_pending\<rbrace>