theory KHeap_DR

lemma set_parent_corres:
  "\<lbrakk>slot = transform_cslot_ptr slot';pslot = transform_cslot_ptr pslot'\<rbrakk>
    \<Longrightarrow>dcorres dc \<top> ((cte_wp_at ((\<noteq>)cap.NullCap) slot') and
             weak_valid_mdb and (cte_wp_at ((\<noteq>)cap.NullCap) pslot')
             and (\<lambda>s. cdt s slot' = None))
             (set_parent slot pslot)
             (update_cdt (\<lambda>cdt a. if a = slot' then Some pslot' else cdt a))" supply if_cong[cong] apply (clarsimp simp:set_parent_def update_cdt_def gets_def) apply (rule dcorres_absorb_get_l) apply (rule dcorres_absorb_get_r) apply clarsimp apply (frule transform_cdt_none[OF cte_wp_at_weakenE]) apply simp apply (simp add:weak_valid_mdb_def) apply simp apply (clarsimp simp:corres_underlying_def cdl_cdt_transform
    fail_def assert_def simpler_modify_def put_def gets_def
    get_def set_cdt_def return_def bind_def) apply (simp add:transform_current_thread_def weak_valid_mdb_def) apply (rename_tac s') apply (subgoal_tac "transform s'\<lparr>cdl_cdt:=(cdl_cdt(transform s'))
    (transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr>
    = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot')") apply (clarsimp simp:cdl_cdt_transform) apply (subgoal_tac "s'\<lparr>cdt := \<lambda>a. if a = slot' then Some pslot' else cdt s' a\<rparr> = abs_cdt_single_update s' slot' pslot'") apply simp apply (rule sym, rule transform_cdt_single_update_helper,simp) apply (rule cdt_single_update_eq,simp) apply (clarsimp simp:cte_wp_at_cte_at)+ apply (clarsimp simp:abs_cdt_single_update_def) apply (clarsimp simp:cdl_cdt_single_update_def cdl_cdt_transform) apply (case_tac "transform s'") apply (clarsimp simp:cdl_cdt_transform) apply (rule ext) apply (clarsimp split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (cte_wp_at ((\<noteq>) cap.NullCap) slot' and weak_valid_mdb and cte_wp_at ((\<noteq>) cap.NullCap) pslot' and (\<lambda>s. cdt s slot' = None)) (set_parent slot pslot) (update_cdt (\<lambda>cdt a. if a = slot' then Some pslot' else cdt a)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (cte_wp_at ((\<noteq>) cap.NullCap) slot' and weak_valid_mdb and cte_wp_at ((\<noteq>) cap.NullCap) pslot' and (\<lambda>s. cdt s slot' = None)) (set_parent slot pslot) (update_cdt (\<lambda>cdt a. if a = slot' then Some pslot' else cdt a)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (cte_wp_at ((\<noteq>) cap.NullCap) slot' and weak_valid_mdb and cte_wp_at ((\<noteq>) cap.NullCap) pslot' and (\<lambda>s. cdt s slot' = None)) (do s <- get;
y <- assert (cdl_cdt s (transform_cslot_ptr slot') = None);
modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr>)
od) (do s <- get;
set_cdt (\<lambda>a. if a = slot' then Some pslot' else cdt s a)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; True; (cte_wp_at ((\<noteq>) cap.NullCap) slot' and weak_valid_mdb and cte_wp_at ((\<noteq>) cap.NullCap) pslot' and (\<lambda>s. cdt s slot' = None)) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- assert (cdl_cdt (transform s') (transform_cslot_ptr slot') = None);
modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr>)
od) (do s <- get;
set_cdt (\<lambda>a. if a = slot' then Some pslot' else cdt s a)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' s'a. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; True; (cte_wp_at ((\<noteq>) cap.NullCap) slot' and weak_valid_mdb and cte_wp_at ((\<noteq>) cap.NullCap) pslot' and (\<lambda>s. cdt s slot' = None)) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- assert (cdl_cdt (transform s') (transform_cslot_ptr slot') = None);
modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr>)
od) (set_cdt (\<lambda>a. if a = slot' then Some pslot' else cdt s'a a)) proof (prove)
goal (1 subgoal):
 1. \<And>s'a. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'a; weak_valid_mdb s'a; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'a; cdt s'a slot' = None\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- assert (cdl_cdt (transform s'a) (transform_cslot_ptr slot') = None);
modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr>)
od) (set_cdt (\<lambda>a. if a = slot' then Some pslot' else cdt s'a a)) proof (prove)
goal (4 subgoals):
 1. \<And>s'a c. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'a; weak_valid_mdb s'a; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'a; cdt s'a slot' = None; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> True
 2. \<And>s'a. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'a; weak_valid_mdb s'a; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'a; cdt s'a slot' = None\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a)
 3. \<And>s'a. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'a; weak_valid_mdb s'a; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'a; cdt s'a slot' = None\<rbrakk> \<Longrightarrow> cdt s'a slot' = None
 4. \<And>s'a. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'a; weak_valid_mdb s'a; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'a; cdt s'a slot' = None; transform_cdt s'a (transform_cslot_ptr slot') = None\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- assert (cdl_cdt (transform s'a) (transform_cslot_ptr slot') = None);
modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr>)
od) (set_cdt (\<lambda>a. if a = slot' then Some pslot' else cdt s'a a)) proof (prove)
goal (3 subgoals):
 1. \<And>s'a. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'a; weak_valid_mdb s'a; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'a; cdt s'a slot' = None\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a)
 2. \<And>s'a. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'a; weak_valid_mdb s'a; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'a; cdt s'a slot' = None\<rbrakk> \<Longrightarrow> cdt s'a slot' = None
 3. \<And>s'a. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'a; weak_valid_mdb s'a; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'a; cdt s'a slot' = None; transform_cdt s'a (transform_cslot_ptr slot') = None\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- assert (cdl_cdt (transform s'a) (transform_cslot_ptr slot') = None);
modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr>)
od) (set_cdt (\<lambda>a. if a = slot' then Some pslot' else cdt s'a a)) proof (prove)
goal (2 subgoals):
 1. \<And>s'a. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'a; weak_valid_mdb s'a; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'a; cdt s'a slot' = None\<rbrakk> \<Longrightarrow> cdt s'a slot' = None
 2. \<And>s'a. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'a; weak_valid_mdb s'a; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'a; cdt s'a slot' = None; transform_cdt s'a (transform_cslot_ptr slot') = None\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- assert (cdl_cdt (transform s'a) (transform_cslot_ptr slot') = None);
modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr>)
od) (set_cdt (\<lambda>a. if a = slot' then Some pslot' else cdt s'a a)) proof (prove)
goal (1 subgoal):
 1. \<And>s'a. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'a; weak_valid_mdb s'a; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'a; cdt s'a slot' = None; transform_cdt s'a (transform_cslot_ptr slot') = None\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- assert (cdl_cdt (transform s'a) (transform_cslot_ptr slot') = None);
modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr>)
od) (set_cdt (\<lambda>a. if a = slot' then Some pslot' else cdt s'a a)) proof (prove)
goal (1 subgoal):
 1. \<And>s'a. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'a; weak_valid_mdb s'a; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'a; cdt s'a slot' = None; transform_cdt s'a (transform_cslot_ptr slot') = None\<rbrakk> \<Longrightarrow> transform (s'a\<lparr>cdt := \<lambda>a. if a = slot' then Some pslot' else cdt s'a a\<rparr>) = transform s'a\<lparr>cdl_cdt := (transform_cdt s'a)(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s'a. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a) \<and> no_mloop (cdt s'a); cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'a; cdt s'a slot' = None; transform_cdt s'a (transform_cslot_ptr slot') = None\<rbrakk> \<Longrightarrow> transform (s'a\<lparr>cdt := \<lambda>a. if a = slot' then Some pslot' else cdt s'a a\<rparr>) = transform s'a\<lparr>cdl_cdt := (transform_cdt s'a)(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s') \<and> no_mloop (cdt s'); cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None\<rbrakk> \<Longrightarrow> transform (s'\<lparr>cdt := \<lambda>a. if a = slot' then Some pslot' else cdt s' a\<rparr>) = transform s'\<lparr>cdl_cdt := (transform_cdt s')(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s') \<and> no_mloop (cdt s'); cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None; transform s'\<lparr>cdl_cdt := (cdl_cdt (transform s'))(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot')\<rbrakk> \<Longrightarrow> transform (s'\<lparr>cdt := \<lambda>a. if a = slot' then Some pslot' else cdt s' a\<rparr>) = transform s'\<lparr>cdl_cdt := (transform_cdt s')(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr>
 2. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s') \<and> no_mloop (cdt s'); cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None\<rbrakk> \<Longrightarrow> transform s'\<lparr>cdl_cdt := (cdl_cdt (transform s'))(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot') proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None; transform s'\<lparr>cdl_cdt := (transform_cdt s')(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> transform (s'\<lparr>cdt := \<lambda>a. if a = slot' then Some pslot' else cdt s' a\<rparr>) = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot')
 2. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s') \<and> no_mloop (cdt s'); cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None\<rbrakk> \<Longrightarrow> transform s'\<lparr>cdl_cdt := (cdl_cdt (transform s'))(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot') proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None; transform s'\<lparr>cdl_cdt := (transform_cdt s')(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); no_mloop (cdt s'); s'\<lparr>cdt := \<lambda>a. if a = slot' then Some pslot' else cdt s' a\<rparr> = abs_cdt_single_update s' slot' pslot'\<rbrakk> \<Longrightarrow> transform (s'\<lparr>cdt := \<lambda>a. if a = slot' then Some pslot' else cdt s' a\<rparr>) = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot')
 2. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None; transform s'\<lparr>cdl_cdt := (transform_cdt s')(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> s'\<lparr>cdt := \<lambda>a. if a = slot' then Some pslot' else cdt s' a\<rparr> = abs_cdt_single_update s' slot' pslot'
 3. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s') \<and> no_mloop (cdt s'); cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None\<rbrakk> \<Longrightarrow> transform s'\<lparr>cdl_cdt := (cdl_cdt (transform s'))(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot') proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None; transform s'\<lparr>cdl_cdt := (transform_cdt s')(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); no_mloop (cdt s'); s'\<lparr>cdt := \<lambda>a. if a = slot' then Some pslot' else cdt s' a\<rparr> = abs_cdt_single_update s' slot' pslot'\<rbrakk> \<Longrightarrow> transform (abs_cdt_single_update s' slot' pslot') = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot')
 2. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None; transform s'\<lparr>cdl_cdt := (transform_cdt s')(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> s'\<lparr>cdt := \<lambda>a. if a = slot' then Some pslot' else cdt s' a\<rparr> = abs_cdt_single_update s' slot' pslot'
 3. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s') \<and> no_mloop (cdt s'); cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None\<rbrakk> \<Longrightarrow> transform s'\<lparr>cdl_cdt := (cdl_cdt (transform s'))(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot') proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None; transform s'\<lparr>cdl_cdt := (transform_cdt s')(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); no_mloop (cdt s'); s'\<lparr>cdt := \<lambda>a. if a = slot' then Some pslot' else cdt s' a\<rparr> = abs_cdt_single_update s' slot' pslot'\<rbrakk> \<Longrightarrow> cdl_cdt (cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot')) = transform_cdt (abs_cdt_single_update s' slot' pslot')
 2. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None; transform s'\<lparr>cdl_cdt := (transform_cdt s')(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> s'\<lparr>cdt := \<lambda>a. if a = slot' then Some pslot' else cdt s' a\<rparr> = abs_cdt_single_update s' slot' pslot'
 3. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s') \<and> no_mloop (cdt s'); cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None\<rbrakk> \<Longrightarrow> transform s'\<lparr>cdl_cdt := (cdl_cdt (transform s'))(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot') proof (prove)
goal (4 subgoals):
 1. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None; transform s'\<lparr>cdl_cdt := (transform_cdt s')(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); no_mloop (cdt s'); s'\<lparr>cdt := \<lambda>a. if a = slot' then Some pslot' else cdt s' a\<rparr> = abs_cdt_single_update s' slot' pslot'\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) pslot' s'
 2. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None; transform s'\<lparr>cdl_cdt := (transform_cdt s')(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); no_mloop (cdt s'); s'\<lparr>cdt := \<lambda>a. if a = slot' then Some pslot' else cdt s' a\<rparr> = abs_cdt_single_update s' slot' pslot'\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot' s'
 3. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None; transform s'\<lparr>cdl_cdt := (transform_cdt s')(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> s'\<lparr>cdt := \<lambda>a. if a = slot' then Some pslot' else cdt s' a\<rparr> = abs_cdt_single_update s' slot' pslot'
 4. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s') \<and> no_mloop (cdt s'); cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None\<rbrakk> \<Longrightarrow> transform s'\<lparr>cdl_cdt := (cdl_cdt (transform s'))(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot') proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None; transform s'\<lparr>cdl_cdt := (transform_cdt s')(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> s'\<lparr>cdt := \<lambda>a. if a = slot' then Some pslot' else cdt s' a\<rparr> = abs_cdt_single_update s' slot' pslot'
 2. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s') \<and> no_mloop (cdt s'); cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None\<rbrakk> \<Longrightarrow> transform s'\<lparr>cdl_cdt := (cdl_cdt (transform s'))(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot') proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s') \<and> no_mloop (cdt s'); cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None\<rbrakk> \<Longrightarrow> transform s'\<lparr>cdl_cdt := (cdl_cdt (transform s'))(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = cdl_cdt_single_update (transform s') (transform_cslot_ptr slot') (transform_cslot_ptr pslot') proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> transform s'\<lparr>cdl_cdt := (transform_cdt s')(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = transform s'\<lparr>cdl_cdt := \<lambda>x. if x = transform_cslot_ptr slot' then Some (transform_cslot_ptr pslot') else transform_cdt s' x\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s' cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); no_mloop (cdt s'); transform s' = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>\<rbrakk> \<Longrightarrow> transform s'\<lparr>cdl_cdt := (transform_cdt s')(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')\<rparr> = transform s'\<lparr>cdl_cdt := \<lambda>x. if x = transform_cslot_ptr slot' then Some (transform_cslot_ptr pslot') else transform_cdt s' x\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s' cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); no_mloop (cdt s'); transform s' = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>\<rbrakk> \<Longrightarrow> (transform_cdt s')(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot') = (\<lambda>x. if x = transform_cslot_ptr slot' then Some (transform_cslot_ptr pslot') else transform_cdt s' x) proof (prove)
goal (1 subgoal):
 1. \<And>s' cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x. \<lbrakk>slot = transform_cslot_ptr slot'; pslot = transform_cslot_ptr pslot'; cte_wp_at ((\<noteq>) cap.NullCap) slot' s'; cte_wp_at ((\<noteq>) cap.NullCap) pslot' s'; cdt s' slot' = None; transform_cdt s' (transform_cslot_ptr slot') = None; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); no_mloop (cdt s'); transform s' = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>\<rbrakk> \<Longrightarrow> ((transform_cdt s')(transform_cslot_ptr slot' \<mapsto> transform_cslot_ptr pslot')) x = (if x = transform_cslot_ptr slot' then Some (transform_cslot_ptr pslot') else transform_cdt s' x) proof (prove)
goal:
No subgoals!