kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_DR

lemma set_cap_noop_dcorres1:
  "dcorres dc
           (\<lambda>s. opt_cap (transform_cslot_ptr ptr) s = Some (transform_cap cap))
           (valid_idle and not_idle_thread (fst ptr) and valid_etcbs)
    (return ()) (set_cap cap ptr)" apply (rule corres_cong[OF refl refl _ refl refl, THEN iffD1]) apply (erule set_cap_is_noop_opt_cap) apply (rule corres_guard_imp, rule set_cap_corres, simp_all add: not_idle_thread_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>s. opt_cap (transform_cslot_ptr ptr) s = Some (transform_cap cap)) (valid_idle and not_idle_thread (fst ptr) and valid_etcbs) (return ()) (CSpaceAcc_A.set_cap cap ptr) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> {ss'. transform (snd ss') = fst ss'}; opt_cap (transform_cslot_ptr ptr) s = Some (transform_cap cap); (valid_idle and not_idle_thread (fst ptr) and valid_etcbs) s'\<rbrakk> \<Longrightarrow> ?f1 s = return () s
 2. dcorres dc (\<lambda>s. opt_cap (transform_cslot_ptr ptr) s = Some (transform_cap cap)) (valid_idle and not_idle_thread (fst ptr) and valid_etcbs) ?f1 (CSpaceAcc_A.set_cap cap ptr) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>s. opt_cap (transform_cslot_ptr ptr) s = Some (transform_cap cap)) (valid_idle and not_idle_thread (fst ptr) and valid_etcbs) (KHeap_D.set_cap (transform_cslot_ptr ptr) (transform_cap cap)) (CSpaceAcc_A.set_cap cap ptr) proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma set_cap_noop_dcorres2:
  "dcorres dc \<top> (cte_wp_at (\<lambda>cap'. transform_cap cap = transform_cap cap') ptr
                     and not_idle_thread (fst ptr)
                     and valid_idle and valid_etcbs)
    (return ()) (set_cap cap ptr)" apply (rule stronger_corres_guard_imp, rule set_cap_noop_dcorres1, simp_all) apply (clarsimp simp: cte_wp_at_caps_of_state not_idle_thread_def
                        caps_of_state_transform_opt_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (cte_wp_at (\<lambda>cap'. transform_cap cap = transform_cap cap') ptr and not_idle_thread (fst ptr) and valid_idle and valid_etcbs) (return ()) (CSpaceAcc_A.set_cap cap ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>cte_wp_at (\<lambda>cap'. transform_cap cap = transform_cap cap') ptr s' \<and> not_idle_thread (fst ptr) s' \<and> valid_idle s' \<and> valid_etcbs s'; transform s' = s\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr ptr) s = Some (transform_cap cap) proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma descendants_exist_in_cdt:
  "\<lbrakk> a \<in> descendants_of p (cdt s) \<rbrakk>
        \<Longrightarrow> cdt s a \<noteq> None" apply (simp add: descendants_of_def cdt_parent_rel_def) apply (frule RangeI[THEN eqset_imp_iff[OF trancl_range, THEN iffD1]]) apply (clarsimp simp: is_cdt_parent_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<in> CSpaceAcc_A.descendants_of p (cdt s) \<Longrightarrow> cdt s a \<noteq> None proof (prove)
goal (1 subgoal):
 1. (p, a) \<in> {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<^sup>+ \<Longrightarrow> \<exists>aa b. cdt s a = Some (aa, b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(p, a) \<in> {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<^sup>+; a \<in> Range {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<rbrakk> \<Longrightarrow> \<exists>aa b. cdt s a = Some (aa, b) proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma descendants_exist_in_cdl_cdt:
  "\<lbrakk> a \<in> KHeap_D.descendants_of p (transform s) \<rbrakk>
        \<Longrightarrow> cdl_cdt (transform s) a \<noteq> None" apply (simp add: KHeap_D.descendants_of_def KHeap_D.cdt_parent_rel_def) apply (frule RangeI) apply (frule DomainI) apply (clarsimp simp: KHeap_D.is_cdt_parent_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<in> KHeap_D.descendants_of p (transform s) \<Longrightarrow> cdl_cdt (transform s) a \<noteq> None proof (prove)
goal (1 subgoal):
 1. (p, a) \<in> {(x, y). KHeap_D.is_cdt_parent (transform s) x y}\<^sup>+ \<Longrightarrow> \<exists>aa b. cdl_cdt (transform s) a = Some (aa, b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(p, a) \<in> {(x, y). KHeap_D.is_cdt_parent (transform s) x y}\<^sup>+; a \<in> Range ({(x, y). KHeap_D.is_cdt_parent (transform s) x y}\<^sup>+)\<rbrakk> \<Longrightarrow> \<exists>aa b. cdl_cdt (transform s) a = Some (aa, b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(p, a) \<in> {(x, y). KHeap_D.is_cdt_parent (transform s) x y}\<^sup>+; a \<in> Range ({(x, y). KHeap_D.is_cdt_parent (transform s) x y}\<^sup>+); p \<in> Domain ({(x, y). KHeap_D.is_cdt_parent (transform s) x y}\<^sup>+)\<rbrakk> \<Longrightarrow> \<exists>aa b. cdl_cdt (transform s) a = Some (aa, b) proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma descendants_not_null_cap:
  "\<lbrakk> a \<in> descendants_of p (cdt s); mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<rbrakk>
        \<Longrightarrow> cte_wp_at P a s" apply (drule descendants_exist_in_cdt) apply clarsimp apply (drule(1) mdb_cte_atD) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> CSpaceAcc_A.descendants_of p (cdt s); mdb_cte_at (swp (cte_wp_at P) s) (cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at P a s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); cdt s a \<noteq> None\<rbrakk> \<Longrightarrow> cte_wp_at P a s proof (prove)
goal (1 subgoal):
 1. \<And>aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); cdt s a = Some (aa, b)\<rbrakk> \<Longrightarrow> cte_wp_at P a s proof (prove)
goal (1 subgoal):
 1. \<And>aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); swp (cte_wp_at P) s (aa, b) \<and> swp (cte_wp_at P) s a\<rbrakk> \<Longrightarrow> cte_wp_at P a s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma descendants_in_cte_wp_set:
  "mdb_cte_at (swp (cte_wp_at P ) s) (cdt s)
  \<Longrightarrow> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> Collect (\<lambda>x. cte_wp_at (P) x s)" by (auto simp:descendants_not_null_cap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<Longrightarrow> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> {x. cte_wp_at P x s}
theory Finalise_DR

lemma ex_in_none_empty_set:
  "a\<noteq>{} \<Longrightarrow> \<exists>x. x\<in>a" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> a
theory Finalise_DR

lemma delete_cdt_slot_shrink_descendants:
  "\<lbrace>\<lambda>s. valid_mdb s \<and> x = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p x \<and> x = y \<rbrace>
    set_cdt ((\<lambda>p. if x p = Some slot then x slot else x p)(slot := None))
    \<lbrace>\<lambda>r s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and>
    CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p y \<rbrace>" apply (clarsimp simp:set_cdt_def get_def put_def bind_def valid_def) apply (rule conjI) apply (subgoal_tac "mdb_empty_abs s") apply (clarsimp simp:mdb_empty_abs.descendants mdb_empty_abs_def vmdb_abs_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_mdb s \<and> x = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p x \<and> x = y\<rbrace> set_cdt ((\<lambda>p. if x p = Some slot then x slot else x p)(slot := None)) \<lbrace>\<lambda>r s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p y\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_mdb s; x = cdt s; slot \<in> CSpaceAcc_A.descendants_of p (cdt s); y = cdt s\<rbrakk> \<Longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)) \<and> CSpaceAcc_A.descendants_of p ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)) \<subseteq> CSpaceAcc_A.descendants_of p (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_mdb s; x = cdt s; slot \<in> CSpaceAcc_A.descendants_of p (cdt s); y = cdt s\<rbrakk> \<Longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None))
 2. \<And>s. \<lbrakk>valid_mdb s; x = cdt s; slot \<in> CSpaceAcc_A.descendants_of p (cdt s); y = cdt s\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of p ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)) \<subseteq> CSpaceAcc_A.descendants_of p (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>valid_mdb s; x = cdt s; slot \<in> CSpaceAcc_A.descendants_of p (cdt s); y = cdt s; mdb_empty_abs s\<rbrakk> \<Longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None))
 2. \<And>s. \<lbrakk>valid_mdb s; x = cdt s; slot \<in> CSpaceAcc_A.descendants_of p (cdt s); y = cdt s\<rbrakk> \<Longrightarrow> mdb_empty_abs s
 3. \<And>s. \<lbrakk>valid_mdb s; x = cdt s; slot \<in> CSpaceAcc_A.descendants_of p (cdt s); y = cdt s\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of p ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)) \<subseteq> CSpaceAcc_A.descendants_of p (cdt s) proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma invs_emptyable_descendants:
  "\<lbrakk>invs s;CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}\<rbrakk>
              \<Longrightarrow> emptyable (a, b) s" apply (clarsimp simp:emptyable_def) apply (frule reply_slot_not_descendant) apply simp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}\<rbrakk> \<Longrightarrow> emptyable (a, b) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, tcb_cnode_index 2)}; tcb_at a s; b = tcb_cnode_index 2\<rbrakk> \<Longrightarrow> st_tcb_at halted a s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, tcb_cnode_index 2)}; tcb_at a s; b = tcb_cnode_index 2\<rbrakk> \<Longrightarrow> tcb_at ?t7 s
 2. \<lbrakk>invs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, tcb_cnode_index 2)}; tcb_at a s; b = tcb_cnode_index 2; (?t7, tcb_cnode_index 2) \<notin> CSpaceAcc_A.descendants_of ?ptr7 (cdt s)\<rbrakk> \<Longrightarrow> st_tcb_at halted a s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, tcb_cnode_index 2)}; tcb_at a s; b = tcb_cnode_index 2; (a, tcb_cnode_index 2) \<notin> CSpaceAcc_A.descendants_of ?ptr7 (cdt s)\<rbrakk> \<Longrightarrow> st_tcb_at halted a s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma cap_delete_one_cte_at:
  "\<lbrace>invs and emptyable sl and cte_at x\<rbrace> cap_delete_one sl \<lbrace>\<lambda>_. cte_at x\<rbrace>" apply (simp add:cap_delete_one_def) apply wp apply (clarsimp simp:unless_def when_def | rule conjI)+ apply (wp|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable sl and cte_wp_at (\<lambda>_. True) x\<rbrace> cap_delete_one sl \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable sl and cte_wp_at (\<lambda>_. True) x\<rbrace> do cap <- CSpaceAcc_A.get_cap sl;
unless (cap = cap.NullCap) (do final <- IpcCancel_A.is_final_cap cap;
y <- IpcCancel_A.fast_finalise cap final;
IpcCancel_A.empty_slot sl cap.NullCap
od)
od \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap sl \<lbrace>\<lambda>cap. if cap = cap.NullCap then cte_wp_at (\<lambda>_. True) x else cte_wp_at (\<lambda>_. True) x\<rbrace>
 2. \<And>s. (invs and emptyable sl and cte_wp_at (\<lambda>_. True) x) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap sl \<lbrace>\<lambda>cap. cte_wp_at (\<lambda>_. True) x\<rbrace>
 2. \<And>s. (invs and emptyable sl and cte_wp_at (\<lambda>_. True) x) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma nat_to_bl_zero_zero:
  "(nat_to_bl 0 0) = (Some [])" by (clarsimp simp: nat_to_bl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. nat_to_bl 0 0 = Some []
theory Finalise_DR

lemma transform_cap_Null [simp]:
  "(transform_cap cap = cdl_cap.NullCap) = (cap = cap.NullCap)" apply (cases cap, simp_all) apply (rename_tac arch_cap) apply (case_tac arch_cap, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (transform_cap cap = cdl_cap.NullCap) = (cap = cap.NullCap) proof (prove)
goal (1 subgoal):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> transform_cap (ArchObjectCap x12) \<noteq> cdl_cap.NullCap proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap. cap = ArchObjectCap arch_cap \<Longrightarrow> transform_cap (ArchObjectCap arch_cap) \<noteq> cdl_cap.NullCap proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma valid_ntfn_after_remove_slot:
  "\<lbrakk>valid_ntfn ntfn s'; ntfn_obj ntfn = (Structures_A.ntfn.WaitingNtfn list)\<rbrakk>
   \<Longrightarrow> valid_ntfn (ntfn_set_obj ntfn
           (case remove1 ptr list of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn
                            | a # lista \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 ptr list))) s'" apply (clarsimp simp: valid_ntfn_def
                 split: ntfn.splits list.split_asm list.splits option.splits) by (metis (mono_tags) distinct.simps(2) distinct_length_2_or_more distinct_remove1 set_remove1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_ntfn ntfn s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_obj ntfn (case remove1 ptr list of [] \<Rightarrow> IdleNtfn | a # lista \<Rightarrow> WaitingNtfn (remove1 ptr list))) s' proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; ntfn_bound_tcb ntfn = None; list \<noteq> []; \<forall>t\<in>set list. tcb_at t s'; distinct list; remove1 ptr list = x21 # x22\<rbrakk> \<Longrightarrow> tcb_at x21 s' \<and> (\<forall>t\<in>set x22. tcb_at t s') \<and> x21 \<notin> set x22 \<and> distinct x22
theory Finalise_DR

lemma dcorres_get_irq_slot:
  "dcorres (\<lambda>r r'. r = transform_cslot_ptr r') \<top> \<top> (gets (CSpace_D.get_irq_slot x)) (KHeap_A.get_irq_slot x)" apply (simp add:gets_def CSpace_D.get_irq_slot_def KHeap_A.get_irq_slot_def) apply (rule dcorres_absorb_get_l) apply (rule dcorres_absorb_get_r) apply (clarsimp simp: return_def transform_def corres_underlying_def transform_cslot_ptr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>r r'. r = transform_cslot_ptr r') (\<lambda>_. True) (\<lambda>_. True) (gets (CSpace_D.get_irq_slot x)) (KHeap_A.get_irq_slot x) proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>r r'. r = transform_cslot_ptr r') (\<lambda>_. True) (\<lambda>_. True) (do s <- get;
return (cdl_irq_node s x, 0)
od) (do s <- get;
return (interrupt_irq_node s x, [])
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = transform_cslot_ptr r') ((=) (transform s')) ((=) s') (return (cdl_irq_node (transform s') x, 0)) (do s <- get;
return (interrupt_irq_node s x, [])
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' s'a. \<lbrakk>True; True; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = transform_cslot_ptr r') ((=) (transform s'a)) ((=) s'a) (return (cdl_irq_node (transform s') x, 0)) (return (interrupt_irq_node s'a x, [])) proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma machine_op_lift[wp]:
  "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> machine_op_lift x \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" apply (clarsimp simp:machine_rest_lift_def ignore_failure_def machine_op_lift_def) apply (wpsimp simp:simpler_modify_def valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> machine_op_lift x \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> do mr <- gets machine_state_rest;
(r, mr') <- select_f (if fst (x mr) = {} then ({((), mr)}, False) else (fst (x mr), False));
modify (machine_state_rest_update (\<lambda>_. mr'))
od \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma invalidateLocalTLB_ASID_underlying_memory[wp]:
  "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateLocalTLB_ASID a \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" apply (clarsimp simp: invalidateLocalTLB_ASID_def, wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateLocalTLB_ASID a \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma dsb_underlying_memory[wp]: "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> dsb \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" apply (clarsimp simp: dsb_def, wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> dsb \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma invalidate_I_PoU_underlying_memory[wp]: "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidate_I_PoU \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" apply (clarsimp simp: invalidate_I_PoU_def , wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidate_I_PoU \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma cleanCachesPoU_underlying_memory[wp]:
  "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanCaches_PoU \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" apply (clarsimp simp: cleanCaches_PoU_def, wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanCaches_PoU \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma invalidate_asid_dwp[wp]:
  "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>\<lambda>x ps. transform ps = cs\<rbrace>" apply (clarsimp simp:invalidate_asid_def) apply wp apply (clarsimp simp:transform_def transform_objects_def2 transform_current_thread_def transform_cdt_def transform_asid_table_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>\<lambda>x ps. transform ps = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do asid_map <- gets (arm_asid_map \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(the (hw_asid_table next_asid) := None)\<rparr>\<rparr>)
od \<lbrace>\<lambda>x ps. transform ps = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. transform s = cs \<Longrightarrow> transform (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the (hw_asid_table next_asid) := None)\<rparr>\<rparr>) = cs proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma invalidate_hw_asid_entry_dwp[wp]:
  "\<lbrace>\<lambda>s. transform s = cs\<rbrace> invalidate_hw_asid_entry next_asid \<lbrace>\<lambda>xb a. transform a = cs\<rbrace>" apply (clarsimp simp:invalidate_hw_asid_entry_def) apply wp apply (clarsimp simp:transform_def transform_objects_def2 transform_current_thread_def transform_cdt_def transform_asid_table_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. transform s = cs\<rbrace> invalidate_hw_asid_entry next_asid \<lbrace>\<lambda>xb a. transform a = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. transform s = cs\<rbrace> do hw_asid_map <- gets (arm_hwasid_table \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(next_asid := None)\<rparr>\<rparr>)
od \<lbrace>\<lambda>xb a. transform a = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. transform s = cs \<Longrightarrow> transform (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) s)(next_asid := None)\<rparr>\<rparr>) = cs proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma set_hardware_asid_dwp[wp]:
  " \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> setHardwareASID hw_asid \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" by (clarsimp simp:setHardwareASID_def,wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> setHardwareASID hw_asid \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
theory Finalise_DR

lemma  transform_arch_state:
  "\<lbrakk> arm_globals_frame (arch_state a) = arm_globals_frame x;
       arm_asid_table (arch_state a) = arm_asid_table x \<rbrakk>
    \<Longrightarrow> transform (a\<lparr>arch_state := x \<rparr>) = transform a" by (clarsimp simp:transform_def transform_objects_def2 transform_cdt_def
    transform_current_thread_def transform_asid_table_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arm_globals_frame (arch_state a) = arm_globals_frame x; asid_table a = arm_asid_table x\<rbrakk> \<Longrightarrow> transform (a\<lparr>arch_state := x\<rparr>) = transform a
theory Finalise_DR

lemma arch_obj_not_idle:
  "\<lbrakk>valid_idle s;kheap s ptr = Some (ArchObj x )\<rbrakk> \<Longrightarrow> not_idle_thread ptr s" by (clarsimp simp:not_idle_thread_def valid_idle_def obj_at_def pred_tcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s ptr = Some (ArchObj x)\<rbrakk> \<Longrightarrow> not_idle_thread ptr s
theory Finalise_DR

lemma asid_pool_at_rev:
  "\<lbrakk> kheap s a = Some (ArchObj (arch_kernel_obj.ASIDPool fun)) \<rbrakk> \<Longrightarrow> asid_pool_at a s" apply (clarsimp simp: obj_at_def valid_idle_def st_tcb_at_def) apply (clarsimp simp: a_type_def
                 split: arch_kernel_obj.splits Structures_A.kernel_object.split_asm if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s a = Some (ArchObj (ASIDPool fun)) \<Longrightarrow> typ_at (AArch AASIDPool) a s proof (prove)
goal (1 subgoal):
 1. kheap s a = Some (ArchObj (ASIDPool fun)) \<Longrightarrow> a_type (ArchObj (ASIDPool fun)) = AArch AASIDPool proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma asid_pool_not_idle:
  "\<lbrakk> valid_idle s; asid_pool_at a s \<rbrakk> \<Longrightarrow> not_idle_thread a s" apply (clarsimp simp:obj_at_def valid_idle_def pred_tcb_at_def) apply (clarsimp simp: not_idle_thread_def
                 split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; typ_at (AArch AASIDPool) a s\<rbrakk> \<Longrightarrow> not_idle_thread a s proof (prove)
goal (1 subgoal):
 1. \<And>ap tcb. \<lbrakk>idle_thread s = idle_thread_ptr; kheap s a = Some (ArchObj (ASIDPool ap)); kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb)\<rbrakk> \<Longrightarrow> not_idle_thread a s proof (prove)
goal:
No subgoals!