kings-crown/FVELER_Isabelle huggingface dataset:
theory CNode_DR

lemma is_untyped_cap_transform_cap[simp]:
  "Types_D.is_untyped_cap (transform_cap src_cap)
  = is_untyped_cap src_cap" apply (case_tac src_cap) apply (simp_all add:transform_cap_def cap_type_simps) apply (clarsimp simp:cap_type_simps split:arch_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Types_D.is_untyped_cap (transform_cap src_cap) = Structures_A.is_untyped_cap src_cap proof (prove)
goal (12 subgoals):
 1. src_cap = cap.NullCap \<Longrightarrow> Types_D.is_untyped_cap (transform_cap src_cap) = Structures_A.is_untyped_cap src_cap
 2. \<And>x21 x22 x23 x24. src_cap = cap.UntypedCap x21 x22 x23 x24 \<Longrightarrow> Types_D.is_untyped_cap (transform_cap src_cap) = Structures_A.is_untyped_cap src_cap
 3. \<And>x31 x32 x33. src_cap = cap.EndpointCap x31 x32 x33 \<Longrightarrow> Types_D.is_untyped_cap (transform_cap src_cap) = Structures_A.is_untyped_cap src_cap
 4. \<And>x41 x42 x43. src_cap = cap.NotificationCap x41 x42 x43 \<Longrightarrow> Types_D.is_untyped_cap (transform_cap src_cap) = Structures_A.is_untyped_cap src_cap
 5. \<And>x51 x52 x53. src_cap = cap.ReplyCap x51 x52 x53 \<Longrightarrow> Types_D.is_untyped_cap (transform_cap src_cap) = Structures_A.is_untyped_cap src_cap
 6. \<And>x61 x62 x63. src_cap = cap.CNodeCap x61 x62 x63 \<Longrightarrow> Types_D.is_untyped_cap (transform_cap src_cap) = Structures_A.is_untyped_cap src_cap
 7. \<And>x7. src_cap = ThreadCap x7 \<Longrightarrow> Types_D.is_untyped_cap (transform_cap src_cap) = Structures_A.is_untyped_cap src_cap
 8. src_cap = cap.DomainCap \<Longrightarrow> Types_D.is_untyped_cap (transform_cap src_cap) = Structures_A.is_untyped_cap src_cap
 9. src_cap = IRQControlCap \<Longrightarrow> Types_D.is_untyped_cap (transform_cap src_cap) = Structures_A.is_untyped_cap src_cap
 10. \<And>x10. src_cap = IRQHandlerCap x10 \<Longrightarrow> Types_D.is_untyped_cap (transform_cap src_cap) = Structures_A.is_untyped_cap src_cap
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>x12. src_cap = ArchObjectCap x12 \<Longrightarrow> cap_type (case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)) \<noteq> Some UntypedType proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma is_untyped_cap_eqD:
  "Structures_A.is_untyped_cap src_cap
  \<Longrightarrow> \<exists>dev ptr sz idx. src_cap = cap.UntypedCap dev ptr sz idx" by (case_tac src_cap, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Structures_A.is_untyped_cap src_cap \<Longrightarrow> \<exists>dev ptr sz idx. src_cap = cap.UntypedCap dev ptr sz idx
theory CNode_DR

lemma p2_less_minus:
  "2 ^ sz - Suc 0 < 2 ^ sz" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 ^ sz - Suc 0 < 2 ^ sz
theory CNode_DR

lemma revokable_cap_insert_dest_original:
  "is_cap_revocable capa cap = cap_insert_dest_original capa cap" by (clarsimp simp: is_cap_revocable_def arch_is_cap_revocable_def cap_insert_dest_original_def split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_cap_revocable capa cap = cap_insert_dest_original capa cap
theory CNode_DR

lemma cap_move_swap_ext_def:
  "(cap_move new_cap src_slot dest_slot :: (unit, unit) s_monad)=
    do CSpaceAcc_A.set_cap new_cap dest_slot;
   CSpaceAcc_A.set_cap cap.NullCap src_slot;
   src_p \<leftarrow> gets (\<lambda>s. cdt s src_slot);
   dest_p \<leftarrow> gets (\<lambda>s. cdt s dest_slot);
   cdt \<leftarrow> gets cdt;
   parent \<leftarrow> return $ cdt src_slot;
   cdt' \<leftarrow> return $ cdt(dest_slot := parent, src_slot := None);
   set_cdt
    (\<lambda>r. if cdt' r = Some src_slot then Some dest_slot
         else cdt' r);
   is_original \<leftarrow> gets is_original_cap;
   set_original dest_slot (is_original src_slot);
   set_original src_slot False;
      do_extended_op
    (cap_move_ext src_slot dest_slot src_p dest_p)
od" unfolding cap_move_def apply (simp add: set_original_def gets_fold_into_modify) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_move new_cap src_slot dest_slot = do CSpaceAcc_A.set_cap new_cap dest_slot;
CSpaceAcc_A.set_cap cap.NullCap src_slot;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
cdt <- gets cdt;
parent <- return $ cdt src_slot;
cdt' <- return $ cdt(dest_slot := parent, src_slot := None);
set_cdt (\<lambda>r. if cdt' r = Some src_slot then Some dest_slot else cdt' r);
is_original <- gets is_original_cap;
set_original dest_slot (is_original src_slot);
set_original src_slot False;
do_extended_op (cap_move_ext src_slot dest_slot src_p dest_p)
od proof (prove)
goal (1 subgoal):
 1. do CSpaceAcc_A.set_cap new_cap dest_slot;
CSpaceAcc_A.set_cap cap.NullCap src_slot;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
cdt <- gets cdt;
parent <- return $ cdt src_slot;
cdt' <- return $ cdt(dest_slot := parent, src_slot := None);
set_cdt (\<lambda>r. if cdt' r = Some src_slot then Some dest_slot else cdt' r);
do_extended_op (cap_move_ext src_slot dest_slot src_p dest_p);
is_original <- gets is_original_cap;
set_original dest_slot (is_original src_slot);
set_original src_slot False
od = do CSpaceAcc_A.set_cap new_cap dest_slot;
CSpaceAcc_A.set_cap cap.NullCap src_slot;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
cdt <- gets cdt;
parent <- return $ cdt src_slot;
cdt' <- return $ cdt(dest_slot := parent, src_slot := None);
set_cdt (\<lambda>r. if cdt' r = Some src_slot then Some dest_slot else cdt' r);
is_original <- gets is_original_cap;
set_original dest_slot (is_original src_slot);
set_original src_slot False;
do_extended_op (cap_move_ext src_slot dest_slot src_p dest_p)
od proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma cap_null_reply_case_If:
  "(case cap of cap.ReplyCap t b R \<Rightarrow> f t b R | cap.NullCap \<Rightarrow> g | _ \<Rightarrow> h)
        = (if cap = cap.NullCap then g
           else if is_reply_cap cap \<or> is_master_reply_cap cap
           then f (obj_ref_of cap) (is_master_reply_cap cap) (cap_rights cap)
           else h)" by (simp add: is_reply_cap_def is_master_reply_cap_def split: cap.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case cap of cap.NullCap \<Rightarrow> g | cap.ReplyCap t b R \<Rightarrow> f t b R | _ \<Rightarrow> h) = (if cap = cap.NullCap then g else if is_reply_cap cap \<or> is_master_reply_cap cap then f (obj_ref_of cap) (is_master_reply_cap cap) (Structures_A.cap_rights cap) else h)
theory CNode_DR

lemma corres_if_rhs2:
  "\<lbrakk> G \<Longrightarrow> corres_underlying sr nf nf' rvr P Q a b;
      \<not> G \<Longrightarrow> corres_underlying sr nf nf' rvr P' Q' a c \<rbrakk>
     \<Longrightarrow> corres_underlying sr nf nf' rvr (P and P') (\<lambda>s. (G \<longrightarrow> Q s) \<and> (\<not> G \<longrightarrow> Q' s))
        a (if G then b else c)" by (rule corres_guard_imp, rule corres_if_rhs, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<Longrightarrow> corres_underlying sr nf nf' rvr P Q a b; \<not> G \<Longrightarrow> corres_underlying sr nf nf' rvr P' Q' a c\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' rvr (P and P') (\<lambda>s. (G \<longrightarrow> Q s) \<and> (\<not> G \<longrightarrow> Q' s)) a (if G then b else c)
theory CNode_DR

lemma transform_cap_is_Null:
  "(transform_cap cap = cdl_cap.NullCap) = (cap = cap.NullCap)" by (simp add: transform_cap_def split: cap.split arch_cap.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (transform_cap cap = cdl_cap.NullCap) = (cap = cap.NullCap)
theory CNode_DR

lemma cdl_Null_descendants:
  "\<lbrakk>cte_wp_at ((=) cap.NullCap) slot' s';valid_mdb s'\<rbrakk>
   \<Longrightarrow> KHeap_D.descendants_of (transform_cslot_ptr slot') (transform s') = {}" apply (subst descendants_of_eqv,clarsimp simp:valid_mdb_def,simp) apply (erule cte_wp_at_weakenE,simp_all) apply (erule mdb_Null_descendants,simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) cap.NullCap) slot' s'; valid_mdb s'\<rbrakk> \<Longrightarrow> KHeap_D.descendants_of (transform_cslot_ptr slot') (transform s') = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at ((=) cap.NullCap) slot' s'; valid_mdb s'\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot' s'
 2. \<lbrakk>cte_wp_at ((=) cap.NullCap) slot' s'; valid_mdb s'\<rbrakk> \<Longrightarrow> transform_cslot_ptr ` CSpaceAcc_A.descendants_of slot' (cdt s') = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) cap.NullCap) slot' s'; valid_mdb s'\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of slot' (cdt s') = {} proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma empty_set_eq: "{x. False} = {}" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {x. False} = {}
theory CNode_DR

lemma preemption_corres:
  "dcorres (dc \<oplus> dc) P P'
       (Monads_D.throw \<sqinter> returnOk x)
       preemption_point" apply (simp add: preemption_point_def) apply (auto simp: preemption_point_def o_def gets_def liftE_def whenE_def getActiveIRQ_def
                    corres_underlying_def select_def bind_def get_def bindE_def select_f_def modify_def
                    alternative_def throwError_def returnOk_def return_def lift_def
                    put_def do_machine_op_def
                    update_work_units_def wrap_ext_bool_det_ext_ext_def work_units_limit_def
                    work_units_limit_reached_def OR_choiceE_def reset_work_units_def mk_ef_def
           split: option.splits kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) P P' (throw \<sqinter> returnOk x) Exceptions_A.preemption_point proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) P P' (throw \<sqinter> returnOk x) (doE y <- liftE update_work_units;
OR_choiceE work_units_limit_reached (doE y <- liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (\<lambda>y. throwError ())
odE) (returnOk ())
odE) proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma valid_pdpt_objs_irq_state_independent[intro!, simp]:
  "valid_pdpt_objs (s \<lparr> machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr> \<rparr> )
   = valid_pdpt_objs s" by (simp add: obj_valid_pdpt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>ran (kheap (update_machine (machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>) s)). obj_valid_pdpt x) = (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)
theory CNode_DR

lemma cdt_machine_state_independent[intro!, simp]:
  "cdt (update_machine x s) = cdt s" by (simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdt (update_machine x s) = cdt s
theory CNode_DR

lemma cte_wp_at_machine_state[simp]:
  "update_machine z s = s' \<Longrightarrow> cte_wp_at x y s' = cte_wp_at x y s" by (drule sym, simp add: cte_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_machine z s = s' \<Longrightarrow> cte_wp_at x y s' = cte_wp_at x y s
theory CNode_DR

lemma valid_mdb_machine_state[simp]:
  "update_machine z s = s' \<Longrightarrow> valid_mdb s' = valid_mdb s" by (drule sym, simp add: valid_mdb_def swp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_machine z s = s' \<Longrightarrow> valid_mdb s' = valid_mdb s
theory CNode_DR

lemma valid_idle_machine_state[simp]:
  "update_machine z s = s' \<Longrightarrow> valid_idle s' = valid_idle s" by (drule sym, simp add: valid_idle_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_machine z s = s' \<Longrightarrow> valid_idle s' = valid_idle s
theory CNode_DR

lemma not_idle_thread_machine_state[simp]:
  "update_machine z s  = s'\<Longrightarrow> not_idle_thread x s' = not_idle_thread x s" by (drule sym, simp add: not_idle_thread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_machine z s = s' \<Longrightarrow> not_idle_thread x s' = not_idle_thread x s
theory CNode_DR

lemma dcorres_select_select_ext:
  "\<forall>s'\<in>S'. \<exists>s\<in>S. rvr s s' \<Longrightarrow>
    dcorres rvr \<top> \<top> (select S) (select_ext a S')" by (clarsimp simp: select_def select_ext_def get_def bind_def return_def assert_def fail_def corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s'\<in>S'. \<exists>s\<in>S. rvr s s' \<Longrightarrow> dcorres rvr (\<lambda>_. True) (\<lambda>_. True) (select S) (select_ext a S')
theory CNode_DR

lemma revoke_cap_spec_corres:
  "dcorres (dc \<oplus> dc) \<top> ((=) s' and invs and valid_pdpt_objs and valid_etcbs)
       (revoke_cap (transform_cslot_ptr slot')) (cap_revoke slot')" apply (subst revoke_cap_def) apply (rule boolean_exception_corres) unfolding K_def apply (clarsimp simp: liftE_bindE cong: if_cong) apply (rule cap_revoke_corres_helper) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) (\<lambda>_. True) ((=) s' and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (revoke_cap (transform_cslot_ptr slot')) (cap_revoke slot') proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) (\<lambda>_. True) ((=) s' and invs and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_etcbs) (doE fin <- monadic_trancl_preemptible (K (doE S <- liftE $ gets $ KHeap_D.descendants_of (transform_cslot_ptr slot');
if S = {} then returnOk True else doE child <- liftE $ select S;
cap <- liftE $ KHeap_D.get_cap child;
assertE (cap \<noteq> cdl_cap.NullCap);
delete_cap child;
throw \<sqinter> returnOk False
odE
odE)) False;
unlessE fin throw
odE) (cap_revoke slot') proof (prove)
goal (1 subgoal):
 1. dcorres boolean_exception (\<lambda>_. True) ((=) s' and invs and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_etcbs) (monadic_trancl_preemptible (K (doE S <- liftE $ gets $ KHeap_D.descendants_of (transform_cslot_ptr slot');
if S = {} then returnOk True else doE child <- liftE $ select S;
cap <- liftE $ KHeap_D.get_cap child;
assertE (cap \<noteq> cdl_cap.NullCap);
delete_cap child;
throw \<sqinter> returnOk False
odE
odE)) False) (cap_revoke slot') proof (prove)
goal (1 subgoal):
 1. dcorres boolean_exception (\<lambda>_. True) ((=) s' and invs and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_etcbs) (monadic_trancl_preemptible (\<lambda>y. doE S <- liftE $ gets $ KHeap_D.descendants_of (transform_cslot_ptr slot');
if S = {} then returnOk True else doE child <- liftE $ select S;
cap <- liftE $ KHeap_D.get_cap child;
assertE (cap \<noteq> cdl_cap.NullCap);
delete_cap child;
throw \<sqinter> returnOk False
odE
odE) False) (cap_revoke slot') proof (prove)
goal (1 subgoal):
 1. dcorres boolean_exception (\<lambda>_. True) ((=) s' and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (monadic_trancl_preemptible (\<lambda>y. do S <- gets (KHeap_D.descendants_of (transform_cslot_ptr slot'));
if S = {} then returnOk True else do child <- select S;
cap <- KHeap_D.get_cap child;
doE y <- assertE (cap \<noteq> cdl_cap.NullCap);
y <- delete_cap child;
throw \<sqinter> returnOk False
odE
od
od) False) (cap_revoke slot') proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma revoke_cap_corres:
  "slot = transform_cslot_ptr slot'
  \<Longrightarrow> dcorres (dc\<oplus>dc) \<top> (invs and valid_pdpt_objs and valid_etcbs)
       (revoke_cap (slot)) (cap_revoke (slot'))" apply (rule dcorres_expand_pfx) apply clarsimp apply (rule corres_guard_imp[OF revoke_cap_spec_corres]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slot = transform_cslot_ptr slot' \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (revoke_cap slot) (cap_revoke slot') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>slot = transform_cslot_ptr slot'; s = transform s'; True; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) s) ((=) s') (revoke_cap slot) (cap_revoke slot') proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; invs s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (revoke_cap (transform_cslot_ptr slot')) (cap_revoke slot') proof (prove)
goal (2 subgoals):
 1. \<And>s' s. \<lbrakk>slot = transform_cslot_ptr slot'; invs s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; transform s' = s\<rbrakk> \<Longrightarrow> True
 2. \<And>s' s. \<lbrakk>slot = transform_cslot_ptr slot'; invs s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; s' = s\<rbrakk> \<Longrightarrow> ((=) (?s'11 s') and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma corres_mapM_to_mapM_x:
  "corres_underlying sr fl fl' dc P P' f (mapM_x g xs)
     \<Longrightarrow> corres_underlying sr fl fl' dc P P' f (mapM g xs)" by (simp add: mapM_x_mapM liftM_def[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr fl fl' dc P P' f (mapM_x g xs) \<Longrightarrow> corres_underlying sr fl fl' dc P P' f (mapM g xs)
theory CNode_DR

lemma ep_waiting_set_recv_upd_kh:
  "ep_at epptr s \<Longrightarrow> (ep_waiting_set_recv epptr (update_kheap ((kheap s)(epptr \<mapsto> kernel_object.Endpoint X)) s))
    = (ep_waiting_set_recv epptr s)" apply (rule set_eqI) apply (clarsimp simp:ep_waiting_set_recv_def obj_at_def is_ep_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep_at epptr s \<Longrightarrow> ep_waiting_set_recv epptr (update_kheap ((kheap s)(epptr \<mapsto> kernel_object.Endpoint X)) s) = ep_waiting_set_recv epptr s proof (prove)
goal (1 subgoal):
 1. \<And>x. ep_at epptr s \<Longrightarrow> (x \<in> ep_waiting_set_recv epptr (update_kheap ((kheap s)(epptr \<mapsto> kernel_object.Endpoint X)) s)) = (x \<in> ep_waiting_set_recv epptr s) proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma ep_waiting_set_send_upd_kh:
  "ep_at epptr s \<Longrightarrow> (ep_waiting_set_send epptr (update_kheap ((kheap s)(epptr \<mapsto> kernel_object.Endpoint X)) s))
    = (ep_waiting_set_send epptr s)" apply (rule set_eqI) apply (clarsimp simp:ep_waiting_set_send_def obj_at_def is_ep_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep_at epptr s \<Longrightarrow> ep_waiting_set_send epptr (update_kheap ((kheap s)(epptr \<mapsto> kernel_object.Endpoint X)) s) = ep_waiting_set_send epptr s proof (prove)
goal (1 subgoal):
 1. \<And>x. ep_at epptr s \<Longrightarrow> (x \<in> ep_waiting_set_send epptr (update_kheap ((kheap s)(epptr \<mapsto> kernel_object.Endpoint X)) s)) = (x \<in> ep_waiting_set_send epptr s) proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma ntfn_waiting_set_upd_kh:
  "ep_at epptr s \<Longrightarrow> (ntfn_waiting_set epptr (update_kheap ((kheap s)(epptr \<mapsto> kernel_object.Endpoint X)) s))
    = (ntfn_waiting_set epptr s)" apply (rule set_eqI) apply (clarsimp simp:ntfn_waiting_set_def obj_at_def is_ep_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep_at epptr s \<Longrightarrow> ntfn_waiting_set epptr (update_kheap ((kheap s)(epptr \<mapsto> kernel_object.Endpoint X)) s) = ntfn_waiting_set epptr s proof (prove)
goal (1 subgoal):
 1. \<And>x. ep_at epptr s \<Longrightarrow> (x \<in> ntfn_waiting_set epptr (update_kheap ((kheap s)(epptr \<mapsto> kernel_object.Endpoint X)) s)) = (x \<in> ntfn_waiting_set epptr s) proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma neq_CPSR:
  "msg_info_register \<noteq> CPSR \<and> cap_register \<noteq> CPSR" by (clarsimp simp: msg_info_register_def cap_register_def capRegister_def msgInfoRegister_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msg_info_register \<noteq> CPSR \<and> cap_register \<noteq> CPSR
theory CNode_DR

lemma empty_pool:
  "(\<lambda>x. if x \<le> 2 ^ ARM_A.asid_low_bits - 1 then None else (ap :: 10 word \<rightharpoonup> word32) x) = Map.empty" apply (rule ext) apply (cut_tac ptr=x and 'a=10 in word_up_bound) apply (simp add:asid_low_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if x \<le> 2 ^ local.asid_low_bits - 1 then None else ap x) = (\<lambda>x. None) proof (prove)
goal (1 subgoal):
 1. \<And>x. (if x \<le> 2 ^ local.asid_low_bits - 1 then None else ap x) = None proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<le> 2 ^ LENGTH(10) - 1 \<Longrightarrow> (if x \<le> 2 ^ local.asid_low_bits - 1 then None else ap x) = None proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma opt_cap_asid_pool_Some:
  "\<lbrakk> valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.ASIDPool pool)) \<rbrakk>
         \<Longrightarrow>  (opt_cap (a, snd (transform_asid asid)) (transform s))
    = Some (transform_asid_pool_entry (pool (ucast asid)))" apply (clarsimp simp:opt_cap_def transform_def slots_of_def object_slots_def
                       transform_objects_def map_add_def restrict_map_def not_idle_thread_def) apply (frule arch_obj_not_idle,simp) apply (clarsimp simp:transform_asid_pool_contents_def unat_map_def not_idle_thread_def
                       transform_asid_def) apply (rule unat_lt2p[where 'a="10", simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s a = Some (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> opt_cap (a, snd (transform_asid asid)) (transform s) = Some (transform_asid_pool_entry (pool (UCAST(32 \<rightarrow> 10) asid))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s a = Some (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> (a \<noteq> idle_thread s \<longrightarrow> transform_asid_pool_contents pool (snd (transform_asid asid)) = Some (transform_asid_pool_entry (pool (UCAST(32 \<rightarrow> 10) asid)))) \<and> a \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s a = Some (ArchObj (ASIDPool pool)); not_idle_thread a s\<rbrakk> \<Longrightarrow> (a \<noteq> idle_thread s \<longrightarrow> transform_asid_pool_contents pool (snd (transform_asid asid)) = Some (transform_asid_pool_entry (pool (UCAST(32 \<rightarrow> 10) asid)))) \<and> a \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s a = Some (ArchObj (ASIDPool pool)); a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> unat (UCAST(32 \<rightarrow> 10) asid) < 1024 proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma opt_cap_asid_pool_not_None:
  "\<lbrakk> ko_at (ArchObj (arch_kernel_obj.ASIDPool pool)) w s'; valid_idle s';
     ba < 2 ^ asid_low_bits \<rbrakk>
   \<Longrightarrow> \<exists>y. opt_cap (w, ba) (transform s') = Some y" by (clarsimp simp: opt_object_asid_pool obj_at_def slots_of_def unat_map_def
      opt_cap_def invs_def valid_state_def object_slots_def transform_asid_pool_contents_def
      asid_low_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ako_at (ASIDPool pool) w s'; valid_idle s'; ba < 2 ^ local.asid_low_bits\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (w, ba) (transform s') = Some y