theory KHeap_DR

lemma set_cap_null_cap_corres:
  "dcorres dc \<top> (valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s) and valid_etcbs)
    (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap)
    (do set_original slot False;
        CSpaceAcc_A.set_cap cap.NullCap slot
    od)" apply (rule corres_dummy_return_pl) apply (rule corres_guard_imp) apply (rule corres_split[where r'="dc"]) apply (rule set_original_dummy_corres) apply clarsimp apply (rule set_cap_corres) apply (clarsimp simp:transform_cap_def) apply (rule refl) apply wp+ apply clarsimp apply (clarsimp simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s) and valid_etcbs) (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) (do set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s) and valid_etcbs) (do return ?b;
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (do set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot
od) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q2 ?Q'2 (do return ?b;
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (do set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot
od)
 2. \<And>s. True \<Longrightarrow> ?Q2 s
 3. \<And>s. (valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s) and valid_etcbs) s \<Longrightarrow> ?Q'2 s proof (prove)
goal (6 subgoals):
 1. dcorres dc ?P6 ?P'6 (return ?b) (set_original slot False)
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 rv') (K_bind (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) rv) (K_bind (CSpaceAcc_A.set_cap cap.NullCap slot) rv')
 3. \<lbrace>?Q6\<rbrace> return ?b \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> set_original slot False \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> (?P6 and ?Q6) s
 6. \<And>s. (valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s) and valid_etcbs) s \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 rv') (K_bind (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) rv) (K_bind (CSpaceAcc_A.set_cap cap.NullCap slot) rv')
 2. \<lbrace>?Q6\<rbrace> return ?b \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> set_original slot False \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>rv. dcorres dc (?R6 rv) (?R'6 ()) (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) (CSpaceAcc_A.set_cap cap.NullCap slot)
 2. \<lbrace>?Q6\<rbrace> return ?b \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> set_original slot False \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>rv. cdl_cap.NullCap = transform_cap cap.NullCap
 2. \<And>rv. transform_cslot_ptr slot = transform_cslot_ptr slot
 3. \<lbrace>?Q6\<rbrace> return ?b \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> set_original slot False \<lbrace>\<lambda>a b. valid_idle b \<and> fst slot \<noteq> idle_thread b \<and> valid_etcbs b\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>rv. transform_cslot_ptr slot = transform_cslot_ptr slot
 2. \<lbrace>?Q6\<rbrace> return ?b \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> set_original slot False \<lbrace>\<lambda>a b. valid_idle b \<and> fst slot \<noteq> idle_thread b \<and> valid_etcbs b\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q6\<rbrace> return ?b \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<lbrace>?Q'6\<rbrace> set_original slot False \<lbrace>\<lambda>a b. valid_idle b \<and> fst slot \<noteq> idle_thread b \<and> valid_etcbs b\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 4. \<And>s. (valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s
 2. \<And>s. (valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. valid_idle (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>) \<and> fst slot \<noteq> idle_thread (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>) \<and> valid_etcbs (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. valid_idle (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>) \<and> fst slot \<noteq> idle_thread (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>) \<and> valid_etcbs (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>))) s proof (prove)
goal:
No subgoals!