kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_DR

lemma corres_dummy_set_notification:
  "dcorres dc \<top> \<top> (return a) (set_notification epptr b)" apply (simp add: set_simple_ko_def get_object_def bind_assoc gets_def) apply (rule dcorres_absorb_get_r) apply (clarsimp simp: corres_free_fail assert_def a_type_def
                  split: option.splits Structures_A.kernel_object.splits) apply (rule corres_free_set_object) apply (clarsimp simp:transform_def transform_current_thread_def) apply (subst transform_objects_update_kheap_same_caps) apply (simp add: transform_objects_update_same)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return a) (set_notification epptr b) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return a) (do x <- get;
y <- assert (\<exists>y. kheap x epptr = Some y);
y <- assert (a_type (the (kheap x epptr)) = AEndpoint \<or> a_type (the (kheap x epptr)) = ANTFN);
y <- assert (\<exists>y. kernel_object.Notification y = the (kheap x epptr));
KHeap_A.set_object epptr (kernel_object.Notification b)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return a) (do y <- assert (\<exists>y. kheap s' epptr = Some y);
y <- assert (a_type (the (kheap s' epptr)) = AEndpoint \<or> a_type (the (kheap s' epptr)) = ANTFN);
y <- assert (\<exists>y. kernel_object.Notification y = the (kheap s' epptr));
KHeap_A.set_object epptr (kernel_object.Notification b)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' x4. kheap s' epptr = Some (kernel_object.Notification x4) \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return a) (KHeap_A.set_object epptr (kernel_object.Notification b)) proof (prove)
goal (1 subgoal):
 1. \<And>s' x4. kheap s' epptr = Some (kernel_object.Notification x4) \<Longrightarrow> \<forall>s s'a. s = transform s'a \<and> transform s' = s \<and> s' = s'a \<longrightarrow> s = transform (update_kheap ((kheap s'a)(epptr \<mapsto> kernel_object.Notification b)) s'a) proof (prove)
goal (1 subgoal):
 1. \<And>s' x4. kheap s' epptr = Some (kernel_object.Notification x4) \<Longrightarrow> transform_objects s' = transform_objects (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification b)) s') proof (prove)
goal (4 subgoals):
 1. \<And>s' x4. kheap s' epptr = Some (kernel_object.Notification x4) \<Longrightarrow> kheap s' epptr = Some (?ko28 s' x4)
 2. \<And>s' x4. kheap s' epptr = Some (kernel_object.Notification x4) \<Longrightarrow> caps_of_object (kernel_object.Notification b) = caps_of_object (?ko28 s' x4)
 3. \<And>s' x4. kheap s' epptr = Some (kernel_object.Notification x4) \<Longrightarrow> a_type (kernel_object.Notification b) = a_type (?ko28 s' x4)
 4. \<And>s' x4. kheap s' epptr = Some (kernel_object.Notification x4) \<Longrightarrow> transform_objects s' = (if epptr = idle_thread s' then transform_objects (update_kheap (kheap s') s') else (transform_objects (update_kheap (kheap s') s'))(epptr \<mapsto> transform_object (machine_state s') epptr (ekheap s' epptr) (kernel_object.Notification b))) proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma corres_dummy_set_sync_ep:
  "dcorres dc \<top> \<top> (return a) (set_endpoint epptr b)" apply (simp add: set_simple_ko_def get_object_def bind_assoc gets_def) apply (rule dcorres_absorb_get_r) apply (clarsimp simp: corres_free_fail assert_def a_type_def partial_inv_def
                  split: option.splits Structures_A.kernel_object.splits) apply (rule corres_free_set_object) apply (clarsimp simp:transform_def transform_current_thread_def) apply (subst transform_objects_update_kheap_same_caps) apply (simp add: transform_objects_update_same)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return a) (set_endpoint epptr b) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return a) (do x <- get;
y <- assert (\<exists>y. kheap x epptr = Some y);
y <- assert (a_type (the (kheap x epptr)) = AEndpoint \<or> a_type (the (kheap x epptr)) = ANTFN);
y <- assert (\<exists>y. kernel_object.Endpoint y = the (kheap x epptr));
KHeap_A.set_object epptr (kernel_object.Endpoint b)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return a) (do y <- assert (\<exists>y. kheap s' epptr = Some y);
y <- assert (a_type (the (kheap s' epptr)) = AEndpoint \<or> a_type (the (kheap s' epptr)) = ANTFN);
y <- assert (\<exists>y. kernel_object.Endpoint y = the (kheap s' epptr));
KHeap_A.set_object epptr (kernel_object.Endpoint b)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3. kheap s' epptr = Some (kernel_object.Endpoint x3) \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return a) (KHeap_A.set_object epptr (kernel_object.Endpoint b)) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3. kheap s' epptr = Some (kernel_object.Endpoint x3) \<Longrightarrow> \<forall>s s'a. s = transform s'a \<and> transform s' = s \<and> s' = s'a \<longrightarrow> s = transform (update_kheap ((kheap s'a)(epptr \<mapsto> kernel_object.Endpoint b)) s'a) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3. kheap s' epptr = Some (kernel_object.Endpoint x3) \<Longrightarrow> transform_objects s' = transform_objects (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint b)) s') proof (prove)
goal (4 subgoals):
 1. \<And>s' x3. kheap s' epptr = Some (kernel_object.Endpoint x3) \<Longrightarrow> kheap s' epptr = Some (?ko28 s' x3)
 2. \<And>s' x3. kheap s' epptr = Some (kernel_object.Endpoint x3) \<Longrightarrow> caps_of_object (kernel_object.Endpoint b) = caps_of_object (?ko28 s' x3)
 3. \<And>s' x3. kheap s' epptr = Some (kernel_object.Endpoint x3) \<Longrightarrow> a_type (kernel_object.Endpoint b) = a_type (?ko28 s' x3)
 4. \<And>s' x3. kheap s' epptr = Some (kernel_object.Endpoint x3) \<Longrightarrow> transform_objects s' = (if epptr = idle_thread s' then transform_objects (update_kheap (kheap s') s') else (transform_objects (update_kheap (kheap s') s'))(epptr \<mapsto> transform_object (machine_state s') epptr (ekheap s' epptr) (kernel_object.Endpoint b))) proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma nat_to_bl_id2:
  shows "nat_to_bl (length p) (nat (bl_to_bin p)) = Some p" unfolding nat_to_bl_def by (simp add: not_le bl_to_bin_ge0 bl_to_bin_lt2p nat_less_iff del: bin_to_bl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. nat_to_bl (length p) (nat (bl_to_bin p)) = Some p proof (prove)
goal (1 subgoal):
 1. (if 2 ^ length p \<le> nat (bl_to_bin p) then None else Some $ bin_to_bl (length p) (int (nat (bl_to_bin p)))) = Some p
theory KHeap_DR

lemma xf_cnode_contents:
  "\<lbrakk> well_formed_cnode_n sz cn; cn p = Some cap \<rbrakk> \<Longrightarrow>
  transform_cnode_contents sz cn (nat (bl_to_bin p)) = Some (transform_cap cap)" unfolding transform_cnode_contents_def apply clarsimp apply (frule (1) wf_cs_nD [symmetric], simp) apply (simp add: nat_to_bl_id2 word_bits_conv option_map_join_simps option_map_join_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_formed_cnode_n sz cn; cn p = Some cap\<rbrakk> \<Longrightarrow> transform_cnode_contents sz cn (nat (bl_to_bin p)) = Some (transform_cap cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_formed_cnode_n sz cn; cn p = Some cap\<rbrakk> \<Longrightarrow> map_option transform_cap (option_map_join cn (nat_to_bl sz (nat (bl_to_bin p)))) = Some (transform_cap cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_formed_cnode_n sz cn; cn p = Some cap\<rbrakk> \<Longrightarrow> \<exists>z. option_map_join cn (nat_to_bl sz (nat (bl_to_bin p))) = Some z \<and> transform_cap z = transform_cap cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_formed_cnode_n (length p) cn; cn p = Some cap; sz = length p\<rbrakk> \<Longrightarrow> \<exists>z. option_map_join cn (nat_to_bl (length p) (nat (bl_to_bin p))) = Some z \<and> transform_cap z = transform_cap cap proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma caps_of_state_cnode_upd:
  "\<lbrakk> kheap s p' = Some (CNode sz cn); well_formed_cnode_n sz cn;
     cn sl' = Some ocap' \<rbrakk> \<Longrightarrow>
  caps_of_state (update_kheap ((kheap s)(p' \<mapsto> CNode sz (cn(sl' \<mapsto> cap')))) s) =
   (caps_of_state s) ((p',sl') \<mapsto> cap')" apply (rule ext) apply (auto simp: caps_of_state_cte_wp_at cte_wp_at_cases wf_cs_upd) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p' = Some (kernel_object.CNode sz cn); well_formed_cnode_n sz cn; cn sl' = Some ocap'\<rbrakk> \<Longrightarrow> caps_of_state (update_kheap ((kheap s)(p' \<mapsto> kernel_object.CNode sz (cn(sl' \<mapsto> cap')))) s) = (caps_of_state s)((p', sl') \<mapsto> cap') proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>kheap s p' = Some (kernel_object.CNode sz cn); well_formed_cnode_n sz cn; cn sl' = Some ocap'\<rbrakk> \<Longrightarrow> caps_of_state (update_kheap ((kheap s)(p' \<mapsto> kernel_object.CNode sz (cn(sl' \<mapsto> cap')))) s) x = ((caps_of_state s)((p', sl') \<mapsto> cap')) x proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma caps_of_state_cnode:
  "\<lbrakk> kheap s p = Some (CNode sz cn); well_formed_cnode_n sz cn; cn sl = Some cap \<rbrakk> \<Longrightarrow>
  caps_of_state s (p, sl) = Some cap" by (simp add: caps_of_state_cte_wp_at cte_wp_at_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (kernel_object.CNode sz cn); well_formed_cnode_n sz cn; cn sl = Some cap\<rbrakk> \<Longrightarrow> caps_of_state s (p, sl) = Some cap
theory KHeap_DR

lemma cdl_objects_tcb:
  "\<lbrakk>kheap s' p = Some (TCB tcb); ekheap s' p = Some etcb; p \<noteq> idle_thread s'\<rbrakk>
\<Longrightarrow> cdl_objects (transform s') p =
   Some (Tcb \<lparr>cdl_tcb_caps =
              [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb),
               tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb),
               tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb),
               tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb),
               tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb),
               tcb_pending_op_slot \<mapsto> infer_tcb_pending_op p (tcb_state tcb),
               tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)],
              cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb),
              cdl_tcb_intent = transform_full_intent (machine_state s') p tcb,
              cdl_tcb_has_fault = (tcb_has_fault tcb),
              cdl_tcb_domain = tcb_domain etcb
            \<rparr>)" apply (simp add: transform_def transform_objects_def) apply (clarsimp simp: transform_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s' p = Some (TCB tcb); ekheap s' p = Some etcb; p \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> cdl_objects (transform s') p = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op p (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') p tcb, cdl_tcb_has_fault = tcb_has_fault tcb, cdl_tcb_domain = tcb_domain etcb\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s' p = Some (TCB tcb); ekheap s' p = Some etcb; p \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> transform_tcb (machine_state s') p tcb etcb = Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op p (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') p tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr> proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma get_ipc_buffer_words_caps_cong:
  "\<lbrakk> tcb_ipc_buffer tcb = tcb_ipc_buffer tcb';
     is_pg_cap (tcb_ipcframe tcb) = is_pg_cap (tcb_ipcframe tcb');
     \<lbrakk> is_pg_cap (tcb_ipcframe tcb); is_pg_cap (tcb_ipcframe tcb') \<rbrakk>
     \<Longrightarrow> obj_ref_of (tcb_ipcframe tcb) = obj_ref_of (tcb_ipcframe tcb') \<and>
        cap_bits (tcb_ipcframe tcb) = cap_bits (tcb_ipcframe tcb') \<and>
        cap_rights (tcb_ipcframe tcb) = cap_rights (tcb_ipcframe tcb')\<rbrakk>
  \<Longrightarrow> get_ipc_buffer_words ms tcb ns = get_ipc_buffer_words ms tcb' ns" apply (clarsimp simp: get_ipc_buffer_words_def is_cap_simps) by (auto split: cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_ipc_buffer tcb = tcb_ipc_buffer tcb'; is_pg_cap (tcb_ipcframe tcb) = is_pg_cap (tcb_ipcframe tcb'); \<lbrakk>is_pg_cap (tcb_ipcframe tcb); is_pg_cap (tcb_ipcframe tcb')\<rbrakk> \<Longrightarrow> obj_ref_of (tcb_ipcframe tcb) = obj_ref_of (tcb_ipcframe tcb') \<and> cap_bits (tcb_ipcframe tcb) = cap_bits (tcb_ipcframe tcb') \<and> Structures_A.cap_rights (tcb_ipcframe tcb) = Structures_A.cap_rights (tcb_ipcframe tcb')\<rbrakk> \<Longrightarrow> get_ipc_buffer_words ms tcb ns = get_ipc_buffer_words ms tcb' ns proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_ipc_buffer tcb = tcb_ipc_buffer tcb'; (\<exists>dev p R sz m. tcb_ipcframe tcb = ArchObjectCap (PageCap dev p R sz m)) = (\<exists>dev p R sz m. tcb_ipcframe tcb' = ArchObjectCap (PageCap dev p R sz m)); \<exists>dev p R sz m. tcb_ipcframe tcb' = ArchObjectCap (PageCap dev p R sz m) \<Longrightarrow> obj_ref_of (tcb_ipcframe tcb) = obj_ref_of (tcb_ipcframe tcb') \<and> cap_bits (tcb_ipcframe tcb) = cap_bits (tcb_ipcframe tcb') \<and> Structures_A.cap_rights (tcb_ipcframe tcb) = Structures_A.cap_rights (tcb_ipcframe tcb')\<rbrakk> \<Longrightarrow> the (evalMonad (case tcb_ipcframe tcb of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then mapM loadWord (map (\<lambda>n. buf + (tcb_ipc_buffer tcb' && mask (pageBitsForSize sz)) + word_of_nat (n * word_size)) ns) else return [] | ArchObjectCap _ \<Rightarrow> return [] | _ \<Rightarrow> return []) ms) = the (evalMonad (case tcb_ipcframe tcb' of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then mapM loadWord (map (\<lambda>n. buf + (tcb_ipc_buffer tcb' && mask (pageBitsForSize sz)) + word_of_nat (n * word_size)) ns) else return [] | ArchObjectCap _ \<Rightarrow> return [] | _ \<Rightarrow> return []) ms)
theory KHeap_DR

lemma transform_full_intent_caps_cong:
  "\<lbrakk> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb');
     tcb_ipc_buffer tcb = tcb_ipc_buffer tcb';
     is_pg_cap (tcb_ipcframe tcb) = is_pg_cap (tcb_ipcframe tcb');
     \<lbrakk> is_pg_cap (tcb_ipcframe tcb); is_pg_cap (tcb_ipcframe tcb') \<rbrakk>
     \<Longrightarrow> obj_ref_of (tcb_ipcframe tcb) = obj_ref_of (tcb_ipcframe tcb') \<and>
        cap_bits (tcb_ipcframe tcb) = cap_bits (tcb_ipcframe tcb') \<and>
        cap_rights (tcb_ipcframe tcb) = cap_rights (tcb_ipcframe tcb')
        \<rbrakk> \<Longrightarrow>
  transform_full_intent ms p tcb = transform_full_intent ms p tcb'" apply (clarsimp simp: transform_full_intent_def Let_def get_tcb_mrs_def
                        get_tcb_message_info_def
                  cong: get_ipc_buffer_words_caps_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'); tcb_ipc_buffer tcb = tcb_ipc_buffer tcb'; is_pg_cap (tcb_ipcframe tcb) = is_pg_cap (tcb_ipcframe tcb'); \<lbrakk>is_pg_cap (tcb_ipcframe tcb); is_pg_cap (tcb_ipcframe tcb')\<rbrakk> \<Longrightarrow> obj_ref_of (tcb_ipcframe tcb) = obj_ref_of (tcb_ipcframe tcb') \<and> cap_bits (tcb_ipcframe tcb) = cap_bits (tcb_ipcframe tcb') \<and> Structures_A.cap_rights (tcb_ipcframe tcb) = Structures_A.cap_rights (tcb_ipcframe tcb')\<rbrakk> \<Longrightarrow> transform_full_intent ms p tcb = transform_full_intent ms p tcb' proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma transform_full_intent_caps_cong_weak:
  "\<lbrakk> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb');
     tcb_ipc_buffer tcb = tcb_ipc_buffer tcb';
     tcb_ipcframe tcb = tcb_ipcframe tcb' \<rbrakk> \<Longrightarrow>
  transform_full_intent ms p tcb = transform_full_intent ms p tcb'" by (rule transform_full_intent_caps_cong) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'); tcb_ipc_buffer tcb = tcb_ipc_buffer tcb'; tcb_ipcframe tcb = tcb_ipcframe tcb'\<rbrakk> \<Longrightarrow> transform_full_intent ms p tcb = transform_full_intent ms p tcb'
theory KHeap_DR

lemma tcb_slot_pending_ipc_neq [simp]:
  "tcb_pending_op_slot \<noteq> tcb_ipcbuffer_slot" by (simp add: tcb_pending_op_slot_def tcb_ipcbuffer_slot_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_pending_op_slot \<noteq> tcb_ipcbuffer_slot
theory KHeap_DR

lemma transform_scheduler_action_update[simp]: "transform (s\<lparr> scheduler_action := a \<rparr>) = transform s" by (auto simp: transform_def transform_cdt_def transform_current_thread_def transform_asid_table_def transform_objects_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform (scheduler_action_update (\<lambda>_. a) s) = transform s
theory KHeap_DR

lemma transform_cdt_list_update[simp]: "transform (s\<lparr> cdt_list := a \<rparr>) = transform s" by (auto simp: transform_def transform_cdt_def transform_current_thread_def transform_asid_table_def transform_objects_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform (cdt_list_update (\<lambda>_. a) s) = transform s
theory KHeap_DR

lemma transform_ready_queues_update[simp]: "transform (s\<lparr> ready_queues := a \<rparr>) = transform s" by (auto simp: transform_def transform_cdt_def transform_current_thread_def transform_asid_table_def transform_objects_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform (ready_queues_update (\<lambda>_. a) s) = transform s
theory KHeap_DR

lemma mdb_cte_at_cte_wp_at:
  "\<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt s slot = Some slot'\<rbrakk>
    \<Longrightarrow> (cte_wp_at ((\<noteq>) cap.NullCap) slot s)" apply (clarsimp simp:mdb_cte_at_def) apply (case_tac slot,case_tac slot') apply (drule spec)+ apply (auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt s slot = Some slot'\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) slot s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) cap.NullCap) (aa, ba) s; cdt s slot = Some slot'\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) slot s proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) cap.NullCap) (aa, ba) s; cdt s slot = Some slot'; slot = (a, b); slot' = (aa, ba)\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) slot s proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cdt s slot = Some slot'; slot = (a, b); slot' = (aa, ba); cdt s (?a9 a b aa ba, ?b11 a b aa ba) = Some (?a5 a b aa ba, ?b7 a b aa ba) \<longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (?a5 a b aa ba, ?b7 a b aa ba) s \<and> cte_wp_at ((\<noteq>) cap.NullCap) (?a9 a b aa ba, ?b11 a b aa ba) s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) slot s proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma mdb_cte_at_cte_wp_at':
  "\<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt s slot = Some slot'\<rbrakk>
   \<Longrightarrow>(cte_wp_at ((\<noteq>) cap.NullCap) slot' s)" apply (case_tac slot,case_tac slot') apply (clarsimp simp:mdb_cte_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt s slot = Some slot'\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) slot' s proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt s slot = Some slot'; slot = (a, b); slot' = (aa, ba)\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) slot' s proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma transform_cdt_slot_inj_on_mdb_cte_at:
  "\<lbrakk> mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<rbrakk> \<Longrightarrow>
       inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s))" apply (rule transform_cdt_slot_inj_on_cte_at[where P=P and s=s], simp_all) apply (safe elim!: ranE) apply (drule(1) mdb_cte_atD | clarsimp simp: cte_wp_at_caps_of_state)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<Longrightarrow> inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); x \<in> dom (cdt s) \<or> x \<in> ran (cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at P x s proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); cdt s (a, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> cte_wp_at P (a, b) s
 2. \<And>a b aa ba. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); cdt s (aa, ba) = Some (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at P (a, b) s proof (prove)
goal:
No subgoals!