kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_DR

lemma set_to_option_Option_set:
  "set_to_option (set_option x) = x" by (auto simp: set_to_option_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_to_option (set_option x) = x
theory KHeap_DR

lemma unbind_notification_valid_idle[wp]:
  "\<lbrace>valid_idle\<rbrace> IpcCancel_A.unbind_notification t \<lbrace>\<lambda>rv. valid_idle\<rbrace>" apply (simp add: unbind_notification_def) apply (rule hoare_seq_ext[OF _ gbn_sp]) apply (case_tac ntfnptr, clarsimp, wp, simp) apply clarsimp apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) apply (wp | clarsimp)+ apply (auto simp: obj_at_def is_ntfn_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> IpcCancel_A.unbind_notification t \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> do ntfnptr <- get_bound_notification t;
case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
IpcCancel_A.do_unbind_notification ntfnptr' ntfn t
od
od \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptr. \<lbrace>bound_tcb_at ((=) ntfnptr) t and valid_idle\<rbrace> case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
IpcCancel_A.do_unbind_notification ntfnptr' ntfn t
od \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptr a. ntfnptr = Some a \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and valid_idle\<rbrace> case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
IpcCancel_A.do_unbind_notification ntfnptr' ntfn t
od \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrace>bound_tcb_at ((=) (Some a)) t and valid_idle\<rbrace> do ntfn <- get_notification a;
y <- set_notification a (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn. \<lbrace>ko_at (kernel_object.Notification ntfn) a and (bound_tcb_at ((=) (Some a)) t and valid_idle)\<rbrace> do y <- set_notification a (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn s. \<lbrakk>ko_at (kernel_object.Notification ntfn) a s; bound_tcb_at ((=) (Some a)) t s; valid_idle s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. kernel_object.Notification y = ko) a s proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma unbind_maybe_notification_valid_idle[wp]:
  "\<lbrace>valid_idle\<rbrace> IpcCancel_A.unbind_maybe_notification a \<lbrace>\<lambda>rv. valid_idle\<rbrace>" apply (simp add: unbind_maybe_notification_def) apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) apply (case_tac "ntfn_bound_tcb ntfn", clarsimp, wp, simp) apply clarsimp apply (wp | clarsimp)+ apply (auto simp: obj_at_def is_ntfn_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> IpcCancel_A.unbind_maybe_notification a \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> do ntfn <- get_notification a;
case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> IpcCancel_A.do_unbind_notification a ntfn t
od \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>ko_at (kernel_object.Notification ntfn) a and valid_idle\<rbrace> case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> IpcCancel_A.do_unbind_notification a ntfn t \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn aa. ntfn_bound_tcb ntfn = Some aa \<Longrightarrow> \<lbrace>ko_at (kernel_object.Notification ntfn) a and valid_idle\<rbrace> case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> IpcCancel_A.do_unbind_notification a ntfn t \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn aa. ntfn_bound_tcb ntfn = Some aa \<Longrightarrow> \<lbrace>ko_at (kernel_object.Notification ntfn) a and valid_idle\<rbrace> do y <- set_notification a (ntfn_set_bound_tcb ntfn None);
set_bound_notification aa None
od \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn aa s. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; ko_at (kernel_object.Notification ntfn) a s; valid_idle s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. kernel_object.Notification y = ko) a s proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma cdl_cdt_transform:
  "cdl_cdt (transform s) = transform_cdt s" by (simp add:transform_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_cdt (transform s) = transform_cdt s
theory KHeap_DR

lemma set_tcb_capslot_weak_valid_mdb:
  "\<lbrace>weak_valid_mdb and cte_wp_at ((=) cap.NullCap) slot\<rbrace> set_cap cap slot \<lbrace>\<lambda>r s. weak_valid_mdb s\<rbrace> " apply (simp add: weak_valid_mdb_def cte_wp_at_caps_of_state swp_def) apply (wp set_cap_caps_of_state2) apply (case_tac slot) apply (clarsimp simp: valid_def set_cap_def cte_wp_at_caps_of_state weak_valid_mdb_def swp_def) apply (simp only: mdb_cte_at_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>weak_valid_mdb and cte_wp_at ((=) cap.NullCap) slot\<rbrace> CSpaceAcc_A.set_cap cap slot \<lbrace>\<lambda>r. weak_valid_mdb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>weak_valid_mdb and cte_wp_at ((=) cap.NullCap) slot\<rbrace> CSpaceAcc_A.set_cap cap slot \<lbrace>\<lambda>r s. mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap) (cdt s) \<and> no_mloop (cdt s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (weak_valid_mdb and cte_wp_at ((=) cap.NullCap) slot) s \<Longrightarrow> mdb_cte_at (\<lambda>y. \<exists>capa. ((caps_of_state s)(slot \<mapsto> cap)) y = Some capa \<and> cap.NullCap \<noteq> capa) (cdt s) \<and> no_mloop (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(weak_valid_mdb and cte_wp_at ((=) cap.NullCap) slot) s; slot = (a, b)\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>y. \<exists>capa. ((caps_of_state s)(slot \<mapsto> cap)) y = Some capa \<and> cap.NullCap \<noteq> capa) (cdt s) \<and> no_mloop (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>slot = (a, b); mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap) (cdt s); no_mloop (cdt s); caps_of_state s (a, b) = Some cap.NullCap\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>y. (y = (a, b) \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>slot = (a, b); \<forall>p c. cdt s c = Some p \<longrightarrow> (\<exists>cap. caps_of_state s p = Some cap \<and> cap.NullCap \<noteq> cap) \<and> (\<exists>cap. caps_of_state s c = Some cap \<and> cap.NullCap \<noteq> cap); no_mloop (cdt s); caps_of_state s (a, b) = Some cap.NullCap\<rbrakk> \<Longrightarrow> \<forall>p c. cdt s c = Some p \<longrightarrow> ((p = (a, b) \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (p \<noteq> (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s p = Some cap \<and> cap.NullCap \<noteq> cap))) \<and> (c = (a, b) \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (c \<noteq> (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s c = Some cap \<and> cap.NullCap \<noteq> cap)) proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma tcb_reply_cap_cte_wp_at:
  "\<lbrakk>valid_objs s;st_tcb_at (\<lambda>r. \<not> inactive r \<and> \<not> idle r) sid s\<rbrakk>
     \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) s" apply (clarsimp simp:valid_objs_def) apply (drule_tac x = sid in bspec) apply (clarsimp simp:st_tcb_at_def obj_at_def) apply (clarsimp simp:cte_wp_at_cases st_tcb_at_def obj_at_def valid_obj_def valid_tcb_def) apply (clarsimp simp:tcb_cap_cases_def split:Structures_A.thread_state.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) s proof (prove)
goal (2 subgoals):
 1. st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s \<Longrightarrow> sid \<in> dom (kheap s)
 2. \<lbrakk>st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; \<exists>obj. kheap s sid = Some obj \<and> valid_obj sid obj s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; \<exists>obj. kheap s sid = Some obj \<and> valid_obj sid obj s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>kheap s sid = Some (TCB tcb); tcb_state tcb \<noteq> Inactive; tcb_state tcb \<noteq> IdleThreadState; cap.NullCap = tcb_reply tcb; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr sid (tcb_state tcb) (getF tcb)); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma opt_cap_objects_cong:
  "cdl_objects s = cdl_objects s' \<Longrightarrow> opt_cap slot s = opt_cap slot s'" apply (cases slot) apply (clarsimp simp: opt_cap_def slots_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_objects s = cdl_objects s' \<Longrightarrow> opt_cap slot s = opt_cap slot s' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cdl_objects s = cdl_objects s'; slot = (a, b)\<rbrakk> \<Longrightarrow> opt_cap slot s = opt_cap slot s' proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma cap_delete_one_valid_mdb[wp]:
  "\<lbrace>invs and emptyable slot\<rbrace> cap_delete_one slot \<lbrace>\<lambda>yc. valid_mdb\<rbrace>" apply (rule hoare_post_imp [where Q="%x. invs"]) apply (simp add:invs_def valid_state_def valid_pspace_def) apply (rule delete_one_invs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable slot\<rbrace> cap_delete_one slot \<lbrace>\<lambda>yc. valid_mdb\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. invs s \<Longrightarrow> valid_mdb s
 2. \<lbrace>invs and emptyable slot\<rbrace> cap_delete_one slot \<lbrace>\<lambda>x. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable slot\<rbrace> cap_delete_one slot \<lbrace>\<lambda>x. invs\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma thread_get_corresE:
  "\<lbrakk>did = thread; dcorres rv \<top> P' (f tcb) (g (t tcb')) \<rbrakk>
  \<Longrightarrow> dcorres rv \<top>
    (P' and not_idle_thread thread and valid_irq_node and (\<lambda>s. transform_tcb (machine_state s) thread tcb' etcb' = Tcb tcb)
     and ko_at (TCB tcb') thread
     and (\<lambda>s. get_etcb thread s = Some etcb'))
    (liftE (get_thread did) >>=E f) (liftE(thread_get t thread) >>=E g)" apply (simp add:liftE_def bindE_def lift_def) apply (rule thread_get_corres) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>did = thread; dcorres rv (\<lambda>_. True) P' (f tcb) (g (t tcb'))\<rbrakk> \<Longrightarrow> dcorres rv (\<lambda>_. True) (P' and not_idle_thread thread and valid_irq_node and (\<lambda>s. transform_tcb (machine_state s) thread tcb' etcb' = Tcb tcb) and ko_at (TCB tcb') thread and (\<lambda>s. get_etcb thread s = Some etcb')) (liftE (get_thread did) >>=E f) (liftE (thread_get t thread) >>=E g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>did = thread; dcorres rv (\<lambda>_. True) P' (f tcb) (g (t tcb'))\<rbrakk> \<Longrightarrow> dcorres rv (\<lambda>_. True) (P' and not_idle_thread thread and valid_irq_node and (\<lambda>s. transform_tcb (machine_state s) thread tcb' etcb' = Tcb tcb) and ko_at (TCB tcb') thread and (\<lambda>s. get_etcb thread s = Some etcb')) (get_thread thread >>= f) (thread_get t thread >>= g) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>did = thread; dcorres rv (\<lambda>_. True) P' (f tcb) (g (t tcb'))\<rbrakk> \<Longrightarrow> thread = thread
 2. \<lbrakk>did = thread; dcorres rv (\<lambda>_. True) P' (f tcb) (g (t tcb'))\<rbrakk> \<Longrightarrow> dcorres rv (\<lambda>_. True) P' (f tcb) (g (t tcb')) proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma resolve_address_bits_error_branch1:
  " \<not> is_cnode_cap cap \<Longrightarrow> resolve_address_bits (cap,cref) = throwError ExceptionTypes_A.lookup_failure.InvalidRoot" unfolding resolve_address_bits_def apply (clarsimp simp:is_cap_simps) apply (case_tac cap) apply (clarsimp simp:CSpace_A.resolve_address_bits'.simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> Structures_A.is_cnode_cap cap \<Longrightarrow> CSpace_A.resolve_address_bits (cap, cref) = throwError InvalidRoot proof (prove)
goal (1 subgoal):
 1. \<not> Structures_A.is_cnode_cap cap \<Longrightarrow> resolve_address_bits' TYPE('a) (cap, cref) = throwError InvalidRoot proof (prove)
goal (1 subgoal):
 1. \<forall>r bits g. cap \<noteq> cap.CNodeCap r bits g \<Longrightarrow> resolve_address_bits' TYPE('a) (cap, cref) = throwError InvalidRoot proof (prove)
goal (12 subgoals):
 1. \<lbrakk>\<forall>r bits g. cap \<noteq> cap.CNodeCap r bits g; cap = cap.NullCap\<rbrakk> \<Longrightarrow> resolve_address_bits' TYPE('a) (cap, cref) = throwError InvalidRoot
 2. \<And>x21 x22 x23 x24. \<lbrakk>\<forall>r bits g. cap \<noteq> cap.CNodeCap r bits g; cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> resolve_address_bits' TYPE('a) (cap, cref) = throwError InvalidRoot
 3. \<And>x31 x32 x33. \<lbrakk>\<forall>r bits g. cap \<noteq> cap.CNodeCap r bits g; cap = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> resolve_address_bits' TYPE('a) (cap, cref) = throwError InvalidRoot
 4. \<And>x41 x42 x43. \<lbrakk>\<forall>r bits g. cap \<noteq> cap.CNodeCap r bits g; cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> resolve_address_bits' TYPE('a) (cap, cref) = throwError InvalidRoot
 5. \<And>x51 x52 x53. \<lbrakk>\<forall>r bits g. cap \<noteq> cap.CNodeCap r bits g; cap = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> resolve_address_bits' TYPE('a) (cap, cref) = throwError InvalidRoot
 6. \<And>x61 x62 x63. \<lbrakk>\<forall>r bits g. cap \<noteq> cap.CNodeCap r bits g; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> resolve_address_bits' TYPE('a) (cap, cref) = throwError InvalidRoot
 7. \<And>x7. \<lbrakk>\<forall>r bits g. cap \<noteq> cap.CNodeCap r bits g; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> resolve_address_bits' TYPE('a) (cap, cref) = throwError InvalidRoot
 8. \<lbrakk>\<forall>r bits g. cap \<noteq> cap.CNodeCap r bits g; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> resolve_address_bits' TYPE('a) (cap, cref) = throwError InvalidRoot
 9. \<lbrakk>\<forall>r bits g. cap \<noteq> cap.CNodeCap r bits g; cap = IRQControlCap\<rbrakk> \<Longrightarrow> resolve_address_bits' TYPE('a) (cap, cref) = throwError InvalidRoot
 10. \<And>x10. \<lbrakk>\<forall>r bits g. cap \<noteq> cap.CNodeCap r bits g; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> resolve_address_bits' TYPE('a) (cap, cref) = throwError InvalidRoot
A total of 12 subgoals... proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma resolve_address_bits_terminate_branch:
  "\<lbrakk>in_terminate_branch ref cap; cap = cap.CNodeCap oref radix_bits guard\<rbrakk>
      \<Longrightarrow> CSpace_A.resolve_address_bits (cap,ref) = returnOk ((oref, drop (length guard) ref), [])" unfolding resolve_address_bits_def by (clarsimp simp: CSpace_A.resolve_address_bits'.simps in_terminate_branch_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>in_terminate_branch ref cap; cap = cap.CNodeCap oref radix_bits guard\<rbrakk> \<Longrightarrow> CSpace_A.resolve_address_bits (cap, ref) = returnOk ((oref, drop (length guard) ref), []) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>in_terminate_branch ref cap; cap = cap.CNodeCap oref radix_bits guard\<rbrakk> \<Longrightarrow> resolve_address_bits' TYPE('a) (cap, ref) = returnOk ((oref, drop (length guard) ref), [])
theory KHeap_DR

lemma resolve_address_bits_recursive_branch:
  "\<lbrakk>in_recursive_branch ref cap;cap = cap.CNodeCap oref radix_bits guard\<rbrakk>
   \<Longrightarrow> CSpace_A.resolve_address_bits (cap,ref ) =
         doE next_cap \<leftarrow> liftE (CSpaceAcc_A.get_cap (oref, take radix_bits (drop (length guard) ref)));
             if Structures_A.is_cnode_cap next_cap then CSpace_A.resolve_address_bits (next_cap, drop (radix_bits + length guard) ref)
             else returnOk ((oref, take radix_bits (drop (length guard) ref)), drop (radix_bits + length guard) ref)
         odE" unfolding resolve_address_bits_def by (clarsimp simp: in_recursive_branch_def CSpace_A.resolve_address_bits'.simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard\<rbrakk> \<Longrightarrow> CSpace_A.resolve_address_bits (cap, ref) = doE next_cap <- liftE (CSpaceAcc_A.get_cap (oref, take radix_bits (drop (length guard) ref)));
if Structures_A.is_cnode_cap next_cap then CSpace_A.resolve_address_bits (next_cap, drop (radix_bits + length guard) ref) else returnOk ((oref, take radix_bits (drop (length guard) ref)), drop (radix_bits + length guard) ref)
odE proof (prove)
goal (1 subgoal):
 1. \<lbrakk>in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard\<rbrakk> \<Longrightarrow> resolve_address_bits' TYPE('a) (cap, ref) = doE next_cap <- liftE (CSpaceAcc_A.get_cap (oref, take radix_bits (drop (length guard) ref)));
if Structures_A.is_cnode_cap next_cap then resolve_address_bits' TYPE('a) (next_cap, drop (radix_bits + length guard) ref) else returnOk ((oref, take radix_bits (drop (length guard) ref)), drop (radix_bits + length guard) ref)
odE
theory KHeap_DR

lemma is_cnode_cap_transform_cap:
  "Types_D.is_cnode_cap (transform_cap cap) = is_cnode_cap cap" apply (case_tac cap) apply (simp_all add:transform_cap_def cap_type_simps split:cdl_cap.splits arch_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Types_D.is_cnode_cap (transform_cap cap) = Structures_A.is_cnode_cap cap proof (prove)
goal (12 subgoals):
 1. cap = cap.NullCap \<Longrightarrow> Types_D.is_cnode_cap (transform_cap cap) = Structures_A.is_cnode_cap cap
 2. \<And>x21 x22 x23 x24. cap = cap.UntypedCap x21 x22 x23 x24 \<Longrightarrow> Types_D.is_cnode_cap (transform_cap cap) = Structures_A.is_cnode_cap cap
 3. \<And>x31 x32 x33. cap = cap.EndpointCap x31 x32 x33 \<Longrightarrow> Types_D.is_cnode_cap (transform_cap cap) = Structures_A.is_cnode_cap cap
 4. \<And>x41 x42 x43. cap = cap.NotificationCap x41 x42 x43 \<Longrightarrow> Types_D.is_cnode_cap (transform_cap cap) = Structures_A.is_cnode_cap cap
 5. \<And>x51 x52 x53. cap = cap.ReplyCap x51 x52 x53 \<Longrightarrow> Types_D.is_cnode_cap (transform_cap cap) = Structures_A.is_cnode_cap cap
 6. \<And>x61 x62 x63. cap = cap.CNodeCap x61 x62 x63 \<Longrightarrow> Types_D.is_cnode_cap (transform_cap cap) = Structures_A.is_cnode_cap cap
 7. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> Types_D.is_cnode_cap (transform_cap cap) = Structures_A.is_cnode_cap cap
 8. cap = cap.DomainCap \<Longrightarrow> Types_D.is_cnode_cap (transform_cap cap) = Structures_A.is_cnode_cap cap
 9. cap = IRQControlCap \<Longrightarrow> Types_D.is_cnode_cap (transform_cap cap) = Structures_A.is_cnode_cap cap
 10. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> Types_D.is_cnode_cap (transform_cap cap) = Structures_A.is_cnode_cap cap
A total of 12 subgoals... proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma cdl_resolve_address_bits_error_branch1:
  "\<not> is_cnode_cap cap\<Longrightarrow> CSpace_D.resolve_address_bits (transform_cap cap) cap_ptr remaining_size = Monads_D.throw" apply (subst KHeap_DR.resolve_address_bits.simps) apply (simp add:unlessE_def is_cnode_cap_transform_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> Structures_A.is_cnode_cap cap \<Longrightarrow> CSpace_D.resolve_address_bits (transform_cap cap) cap_ptr remaining_size = throw proof (prove)
goal (1 subgoal):
 1. \<not> Structures_A.is_cnode_cap cap \<Longrightarrow> doE unlessE (Types_D.is_cnode_cap (transform_cap cap)) $ throw;
cnode <- liftE $ get_cnode $ cap_object (transform_cap cap);
radix_size <- returnOk $ cdl_cnode_size_bits cnode;
guard_size <- returnOk $ cap_guard_size (transform_cap cap);
cap_guard <- returnOk $ cap_guard (transform_cap cap);
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (cap_ptr >> remaining_size - guard_size) && mask guard_size;
unlessE (guard_size \<le> remaining_size \<and> guard = cap_guard) $ throw;
whenE (remaining_size < level_size) $ throw;
offset <- returnOk $ (cap_ptr >> remaining_size - level_size) && mask radix_size;
slot <- returnOk (cap_object (transform_cap cap), unat offset);
size_left <- returnOk (remaining_size - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap cap_ptr size_left else returnOk (slot, size_left)
odE
odE = throw proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma take_drop:
  "replicate n k @ a = (replicate n k @ (take s a)) @ (drop s a)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. replicate n k @ a = (replicate n k @ take s a) @ drop s a
theory KHeap_DR

lemma length_drop:
  "length cref - a = length (drop a cref)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length cref - a = length (drop a cref)
theory KHeap_DR

lemma nat_case_split:
  "0 < n \<Longrightarrow> (case n of 0 \<Rightarrow> a | Suc nat' \<Rightarrow> f nat') = f (n - 1)"
  "0 < n \<Longrightarrow> (case (case n of 0 \<Rightarrow> a' | Suc sz' \<Rightarrow> cdl_object.CNode (f' sz')) of
                 cdl_object.CNode x \<Rightarrow> return x
               | _ \<Rightarrow> fail) = return  (f' (n - 1))" by (auto split: nat.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0 < n \<Longrightarrow> (case n of 0 \<Rightarrow> a | Suc nat' \<Rightarrow> f nat') = f (n - 1)) &&& (0 < n \<Longrightarrow> (case case n of 0 \<Rightarrow> a' | Suc sz' \<Rightarrow> cdl_object.CNode (f' sz') of cdl_object.CNode x \<Rightarrow> return x | _ \<Rightarrow> fail) = return (f' (n - 1)))
theory KHeap_DR

lemma cdl_current_thread:
  "(cdl_current_thread (transform s')) = transform_current_thread s'" by (clarsimp simp:transform_def )

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_current_thread (transform s') = transform_current_thread s'