theory Invoke_C

lemma invokeCNodeRotate_ccorres:
  "ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (\<lambda>s. cte_at' slot1 s \<and> cte_at' slot2 s \<and> slot1 \<noteq> slot2
            \<and> valid_pspace' s \<and> valid_cap' cap2 s
            \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s
            \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> (cteCap c) = cap2) slot2 s
            \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> NullCap) slot2 s
            \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s))
       (UNIV \<inter> {s. slot1_' s = Ptr slot1} \<inter>
               {s. slot2_' s = Ptr slot2} \<inter>
               {s. slot3_' s = Ptr slot3} \<inter>
               {s. ccap_relation cap1 (cap1_' s)} \<inter>
               {s. ccap_relation cap2 (cap2_' s)}) []
       (invokeCNode (Rotate cap1 cap2 slot1 slot2 slot3))
  (Call invokeCNodeRotate_'proc)" apply (cinit lift: slot1_' slot2_' slot3_' cap1_' cap2_' simp del: return_bind cong:call_ignore_cong) apply (simp split del: if_split del: Collect_const) apply (simp only: liftE_def) apply (rule_tac r'="dc" and xf'="xfdc" in ccorres_split_nothrow_novcg) apply (rule ccorres_cond [where R = \<top>]) apply (clarsimp simp: Collect_const_mem) apply (ctac (no_vcg) add: cteSwap_ccorres) apply (ctac (no_vcg) add: cteMove_ccorres) apply (simp only: K_bind_def) apply (ctac (no_vcg) add: cteMove_ccorres) apply (rule hoare_strengthen_post) apply (rule cteMove_valid_pspace') apply (simp add: valid_pspace'_def) apply ceqv apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) apply (rule allI, rule conseqPre,vcg) apply clarsimp apply (simp add: return_def) apply wp apply (simp add: guard_is_UNIV_def) apply (clarsimp simp: valid_pspace'_def) apply (rule conjI, clarsimp) apply (clarsimp simp:cte_wp_at_ctes_of) apply (clarsimp simp: weak_derived'_def isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (\<lambda>s. cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s)) (UNIV \<inter> \<lbrace>\<acute>slot1 = cte_Ptr slot1\<rbrace> \<inter> \<lbrace>\<acute>slot2 = cte_Ptr slot2\<rbrace> \<inter> \<lbrace>\<acute>slot3 = cte_Ptr slot3\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>cap1\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>cap2\<rbrace>) [] (invokeCNode (Rotate cap1 cap2 slot1 slot2 slot3)) (Call invokeCNodeRotate_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q529 cap2a cap1a slot3a slot2a slot1a) (?Q'529 cap2a cap1a slot3a slot2a slot1a) [SKIP] (liftE (if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od)) (IF slot1a = slot3a THEN
  CALL cteSwap_'proc(cap1a,slot1a,cap2a,slot2a)
ELSE
  CALL cteMove_'proc(cap2a,slot2a,slot3a);;
CALL cteMove_'proc(cap1a,slot1a,slot2a)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q529 cap2a cap1a slot3a slot2a slot1a s \<and> s' \<in> ?Q'529 cap2a cap1a slot3a slot2a slot1a proof (prove)
goal (2 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q529 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)) (?Q'529 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)) [SKIP] (liftE (if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od)) (IF slot1 = slot3 THEN
  CALL cteSwap_'proc(cap1a,cte_Ptr slot1,cap2a,cte_Ptr slot2)
ELSE
  CALL cteMove_'proc(cap2a,cte_Ptr slot2,cte_Ptr slot3);;
CALL cteMove_'proc(cap1a,cte_Ptr slot1,cte_Ptr slot2)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q529 cap2a cap1a slot3a slot2a slot1a s \<and> s' \<in> ?Q'529 cap2a cap1a slot3a slot2a slot1a proof (prove)
goal (2 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q529 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)) (?Q'529 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)) [SKIP] (do r <- if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od;
return (Inr r)
od) (IF slot1 = slot3 THEN
  CALL cteSwap_'proc(cap1a,cte_Ptr slot1,cap2a,cte_Ptr slot2)
ELSE
  CALL cteMove_'proc(cap2a,cte_Ptr slot2,cte_Ptr slot3);;
CALL cteMove_'proc(cap1a,cte_Ptr slot1,cte_Ptr slot2)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q529 cap2a cap1a slot3a slot2a slot1a s \<and> s' \<in> ?Q'529 cap2a cap1a slot3a slot2a slot1a proof (prove)
goal (6 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P544 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)) (?Q'529 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)) [] (if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od) (IF slot1 = slot3 THEN
  CALL cteSwap_'proc(cap1a,cte_Ptr slot1,cap2a,cte_Ptr slot2)
ELSE
  CALL cteMove_'proc(cap2a,cte_Ptr slot2,cte_Ptr slot3);;
CALL cteMove_'proc(cap1a,cte_Ptr slot1,cte_Ptr slot2)
FI)
 2. \<And>cap2a cap1a slot3a slot2a slot1a rv' t t'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 3. \<And>cap2a cap1a slot3a slot2a slot1a rv rv'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q536 cap2a cap1a slot3a slot2a slot1a rv) (?Q'536 cap2a cap1a slot3a slot2a slot1a rv rv') [SKIP] (return (Inr rv)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 4. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R542 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od \<lbrace>?Q536 cap2a cap1a slot3a slot2a slot1a\<rbrace>
 5. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'536 cap2a cap1a slot3a slot2a slot1a)
 6. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P544 cap2a cap1a slot3a slot2a slot1a and ?R542 cap2a cap1a slot3a slot2a slot1a) s \<and> s' \<in> ?Q'529 cap2a cap1a slot3a slot2a slot1a proof (prove)
goal (8 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<longrightarrow> (slot1 = slot3) = (s' \<in> \<lbrace>slot1 = slot3\<rbrace>)
 2. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt555 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)) (?Rt548 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)) [] (cteSwap cap1 slot1 cap2 slot2) (CALL cteSwap_'proc(cap1a,cte_Ptr slot1,cap2a,cte_Ptr slot2))
 3. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf553 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)) (?Rf547 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)) [] (do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od) (CALL cteMove_'proc(cap2a,cte_Ptr slot2,cte_Ptr slot3);;
CALL cteMove_'proc(cap1a,cte_Ptr slot1,cte_Ptr slot2))
 4. \<And>cap2a cap1a slot3a slot2a slot1a rv' t t'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 5. \<And>cap2a cap1a slot3a slot2a slot1a rv rv'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q536 cap2a cap1a slot3a slot2a slot1a rv) (?Q'536 cap2a cap1a slot3a slot2a slot1a rv rv') [SKIP] (return (Inr rv)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 6. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R542 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od \<lbrace>?Q536 cap2a cap1a slot3a slot2a slot1a\<rbrace>
 7. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'536 cap2a cap1a slot3a slot2a slot1a)
 8. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. slot1 = slot3 \<longrightarrow> ?Pt555 cap2a cap1a slot3a slot2a slot1a s) and (\<lambda>s. slot1 \<noteq> slot3 \<longrightarrow> ?Pf553 cap2a cap1a slot3a slot2a slot1a s) and ?R542 cap2a cap1a slot3a slot2a slot1a) s \<and> s' \<in> ?Rt548 cap2a cap1a slot3a slot2a slot1a \<inter> \<lbrace>slot1 = slot3\<rbrace> \<union> ?Rf547 cap2a cap1a slot3a slot2a slot1a \<inter> - \<lbrace>slot1 = slot3\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt555 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)) (?Rt548 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)) [] (cteSwap cap1 slot1 cap2 slot2) (CALL cteSwap_'proc(cap1a,cte_Ptr slot1,cap2a,cte_Ptr slot2))
 2. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf553 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)) (?Rf547 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)) [] (do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od) (CALL cteMove_'proc(cap2a,cte_Ptr slot2,cte_Ptr slot3);;
CALL cteMove_'proc(cap1a,cte_Ptr slot1,cte_Ptr slot2))
 3. \<And>cap2a cap1a slot3a slot2a slot1a rv' t t'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 4. \<And>cap2a cap1a slot3a slot2a slot1a rv rv'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q536 cap2a cap1a slot3a slot2a slot1a rv) (?Q'536 cap2a cap1a slot3a slot2a slot1a rv rv') [SKIP] (return (Inr rv)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 5. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R542 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od \<lbrace>?Q536 cap2a cap1a slot3a slot2a slot1a\<rbrace>
 6. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'536 cap2a cap1a slot3a slot2a slot1a)
 7. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. slot1 = slot3 \<longrightarrow> ?Pt555 cap2a cap1a slot3a slot2a slot1a s) and (\<lambda>s. slot1 \<noteq> slot3 \<longrightarrow> ?Pf553 cap2a cap1a slot3a slot2a slot1a s) and ?R542 cap2a cap1a slot3a slot2a slot1a) s \<and> s' \<in> ?Rt548 cap2a cap1a slot3a slot2a slot1a \<inter> \<lbrace>slot1 = slot3\<rbrace> \<union> ?Rf547 cap2a cap1a slot3a slot2a slot1a \<inter> - \<lbrace>slot1 = slot3\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf553 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)) (?Rf547 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)) [] (do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od) (CALL cteMove_'proc(cap2a,cte_Ptr slot2,cte_Ptr slot3);;
CALL cteMove_'proc(cap1a,cte_Ptr slot1,cte_Ptr slot2))
 2. \<And>cap2a cap1a slot3a slot2a slot1a rv' t t'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 3. \<And>cap2a cap1a slot3a slot2a slot1a rv rv'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q536 cap2a cap1a slot3a slot2a slot1a rv) (?Q'536 cap2a cap1a slot3a slot2a slot1a rv rv') [SKIP] (return (Inr rv)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 4. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R542 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od \<lbrace>?Q536 cap2a cap1a slot3a slot2a slot1a\<rbrace>
 5. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'536 cap2a cap1a slot3a slot2a slot1a)
 6. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. slot1 = slot3 \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2)) s) and (\<lambda>s. slot1 \<noteq> slot3 \<longrightarrow> ?Pf553 cap2a cap1a slot3a slot2a slot1a s) and ?R542 cap2a cap1a slot3a slot2a slot1a) s \<and> s' \<in> {s. slot2_'_update (\<lambda>_. slot2a) (cap2_'_update (\<lambda>_. cap2a) (slot1_'_update (\<lambda>_. slot1a) (cap1_'_update (\<lambda>_. cap1a) s))) \<in> UNIV \<inter> \<lbrace>\<acute>slot1 = slot1a\<rbrace> \<inter> \<lbrace>\<acute>slot2 = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>cap1\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>cap2\<rbrace>} \<inter> \<lbrace>slot1 = slot3\<rbrace> \<union> ?Rf547 cap2a cap1a slot3a slot2a slot1a \<inter> - \<lbrace>slot1 = slot3\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a rv xfdca. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q576 cap2a cap1a slot3a slot2a slot1a rv) (?Q'590 cap2a cap1a rv xfdca) [] (K_bind (cteMove cap1 slot1 slot2) rv) (CALL cteMove_'proc(cap1a,cte_Ptr slot1,cte_Ptr slot2))
 2. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R584 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> cteMove cap2 slot2 slot3 \<lbrace>?Q576 cap2a cap1a slot3a slot2a slot1a\<rbrace>
 3. \<And>cap2a cap1a slot3a slot2a slot1a rv' t t'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 4. \<And>cap2a cap1a slot3a slot2a slot1a rv rv'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q536 cap2a cap1a slot3a slot2a slot1a rv) (?Q'536 cap2a cap1a slot3a slot2a slot1a rv rv') [SKIP] (return (Inr rv)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 5. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R542 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od \<lbrace>?Q536 cap2a cap1a slot3a slot2a slot1a\<rbrace>
 6. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'536 cap2a cap1a slot3a slot2a slot1a)
 7. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. slot1 = slot3 \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2)) s) and (\<lambda>s. slot1 \<noteq> slot3 \<longrightarrow> (valid_mdb' and pspace_aligned' and ?R584 cap2a cap1a slot3a slot2a slot1a) s) and ?R542 cap2a cap1a slot3a slot2a slot1a) s \<and> s' \<in> {s. slot2_'_update (\<lambda>_. slot2a) (cap2_'_update (\<lambda>_. cap2a) (slot1_'_update (\<lambda>_. slot1a) (cap1_'_update (\<lambda>_. cap1a) s))) \<in> UNIV \<inter> \<lbrace>\<acute>slot1 = slot1a\<rbrace> \<inter> \<lbrace>\<acute>slot2 = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>cap1\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>cap2\<rbrace>} \<inter> \<lbrace>slot1 = slot3\<rbrace> \<union> {s. destSlot_'_update (\<lambda>_. slot3a) (srcSlot_'_update (\<lambda>_. slot2a) (newCap_'_update (\<lambda>_. cap2a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot3a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'589 cap2a cap1a slot3a slot2a slot1a t rv} \<inter> - \<lbrace>slot1 = slot3\<rbrace>
flex-flex pairs:
\<lambda>cap2a cap1a t rv. ?Q'590 cap2a cap1a rv (xfdc t) \<equiv>\<^sup>? \<lambda>cap2a cap1a. ?Q'589 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1) proof (prove)
goal (7 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a rv xfdca. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q576 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1) rv) (?Q'590 cap2a cap1a rv xfdca) [] (cteMove cap1 slot1 slot2) (CALL cteMove_'proc(cap1a,cte_Ptr slot1,cte_Ptr slot2))
 2. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R584 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> cteMove cap2 slot2 slot3 \<lbrace>?Q576 cap2a cap1a slot3a slot2a slot1a\<rbrace>
 3. \<And>cap2a cap1a slot3a slot2a slot1a rv' t t'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 4. \<And>cap2a cap1a slot3a slot2a slot1a rv rv'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q536 cap2a cap1a slot3a slot2a slot1a rv) (?Q'536 cap2a cap1a slot3a slot2a slot1a rv rv') [SKIP] (return (Inr rv)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 5. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R542 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od \<lbrace>?Q536 cap2a cap1a slot3a slot2a slot1a\<rbrace>
 6. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'536 cap2a cap1a slot3a slot2a slot1a)
 7. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. slot1 = slot3 \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2)) s) and (\<lambda>s. slot1 \<noteq> slot3 \<longrightarrow> (valid_mdb' and pspace_aligned' and ?R584 cap2a cap1a slot3a slot2a slot1a) s) and ?R542 cap2a cap1a slot3a slot2a slot1a) s \<and> s' \<in> {s. slot2_'_update (\<lambda>_. slot2a) (cap2_'_update (\<lambda>_. cap2a) (slot1_'_update (\<lambda>_. slot1a) (cap1_'_update (\<lambda>_. cap1a) s))) \<in> UNIV \<inter> \<lbrace>\<acute>slot1 = slot1a\<rbrace> \<inter> \<lbrace>\<acute>slot2 = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>cap1\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>cap2\<rbrace>} \<inter> \<lbrace>slot1 = slot3\<rbrace> \<union> {s. destSlot_'_update (\<lambda>_. slot3a) (srcSlot_'_update (\<lambda>_. slot2a) (newCap_'_update (\<lambda>_. cap2a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot3a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'589 cap2a cap1a slot3a slot2a slot1a t rv} \<inter> - \<lbrace>slot1 = slot3\<rbrace>
flex-flex pairs:
\<lambda>cap2a cap1a t rv. ?Q'590 cap2a cap1a rv (xfdc t) \<equiv>\<^sup>? \<lambda>cap2a cap1a. ?Q'589 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1) proof (prove)
goal (6 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R584 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> cteMove cap2 slot2 slot3 \<lbrace>\<lambda>a. valid_mdb' and pspace_aligned'\<rbrace>
 2. \<And>cap2a cap1a slot3a slot2a slot1a rv' t t'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 3. \<And>cap2a cap1a slot3a slot2a slot1a rv rv'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q536 cap2a cap1a slot3a slot2a slot1a rv) (?Q'536 cap2a cap1a slot3a slot2a slot1a rv rv') [SKIP] (return (Inr rv)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 4. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R542 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od \<lbrace>?Q536 cap2a cap1a slot3a slot2a slot1a\<rbrace>
 5. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'536 cap2a cap1a slot3a slot2a slot1a)
 6. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. slot1 = slot3 \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2)) s) and (\<lambda>s. slot1 \<noteq> slot3 \<longrightarrow> (valid_mdb' and pspace_aligned' and ?R584 cap2a cap1a slot3a slot2a slot1a) s) and ?R542 cap2a cap1a slot3a slot2a slot1a) s \<and> s' \<in> {s. slot2_'_update (\<lambda>_. slot2a) (cap2_'_update (\<lambda>_. cap2a) (slot1_'_update (\<lambda>_. slot1a) (cap1_'_update (\<lambda>_. cap1a) s))) \<in> UNIV \<inter> \<lbrace>\<acute>slot1 = slot1a\<rbrace> \<inter> \<lbrace>\<acute>slot2 = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>cap1\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>cap2\<rbrace>} \<inter> \<lbrace>slot1 = slot3\<rbrace> \<union> {s. destSlot_'_update (\<lambda>_. slot3a) (srcSlot_'_update (\<lambda>_. slot2a) (newCap_'_update (\<lambda>_. cap2a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot3a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. slot2a) (srcSlot_'_update (\<lambda>_. slot1a) (newCap_'_update (\<lambda>_. cap1a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot2a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot1a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>newCap\<rbrace>}} \<inter> - \<lbrace>slot1 = slot3\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R584 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> cteMove cap2 slot2 slot3 \<lbrace>?Q634 cap2a cap1a slot3a slot2a slot1a\<rbrace>
 2. \<And>cap2a cap1a slot3a slot2a slot1a rv s. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; ?Q634 cap2a cap1a slot3a slot2a slot1a rv s\<rbrakk> \<Longrightarrow> (valid_mdb' and pspace_aligned') s
 3. \<And>cap2a cap1a slot3a slot2a slot1a rv' t t'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 4. \<And>cap2a cap1a slot3a slot2a slot1a rv rv'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q536 cap2a cap1a slot3a slot2a slot1a rv) (?Q'536 cap2a cap1a slot3a slot2a slot1a rv rv') [SKIP] (return (Inr rv)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 5. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R542 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od \<lbrace>?Q536 cap2a cap1a slot3a slot2a slot1a\<rbrace>
 6. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'536 cap2a cap1a slot3a slot2a slot1a)
 7. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. slot1 = slot3 \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2)) s) and (\<lambda>s. slot1 \<noteq> slot3 \<longrightarrow> (valid_mdb' and pspace_aligned' and ?R584 cap2a cap1a slot3a slot2a slot1a) s) and ?R542 cap2a cap1a slot3a slot2a slot1a) s \<and> s' \<in> {s. slot2_'_update (\<lambda>_. slot2a) (cap2_'_update (\<lambda>_. cap2a) (slot1_'_update (\<lambda>_. slot1a) (cap1_'_update (\<lambda>_. cap1a) s))) \<in> UNIV \<inter> \<lbrace>\<acute>slot1 = slot1a\<rbrace> \<inter> \<lbrace>\<acute>slot2 = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>cap1\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>cap2\<rbrace>} \<inter> \<lbrace>slot1 = slot3\<rbrace> \<union> {s. destSlot_'_update (\<lambda>_. slot3a) (srcSlot_'_update (\<lambda>_. slot2a) (newCap_'_update (\<lambda>_. cap2a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot3a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. slot2a) (srcSlot_'_update (\<lambda>_. slot1a) (newCap_'_update (\<lambda>_. cap1a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot2a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot1a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>newCap\<rbrace>}} \<inter> - \<lbrace>slot1 = slot3\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a rv s. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; valid_pspace' s\<rbrakk> \<Longrightarrow> (valid_mdb' and pspace_aligned') s
 2. \<And>cap2a cap1a slot3a slot2a slot1a rv' t t'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 3. \<And>cap2a cap1a slot3a slot2a slot1a rv rv'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q536 cap2a cap1a slot3a slot2a slot1a rv) (?Q'536 cap2a cap1a slot3a slot2a slot1a rv rv') [SKIP] (return (Inr rv)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 4. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R542 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od \<lbrace>?Q536 cap2a cap1a slot3a slot2a slot1a\<rbrace>
 5. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'536 cap2a cap1a slot3a slot2a slot1a)
 6. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. slot1 = slot3 \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2)) s) and (\<lambda>s. slot1 \<noteq> slot3 \<longrightarrow> (valid_mdb' and pspace_aligned' and (\<lambda>a. valid_pspace' a \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap2) slot2 a \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cap2 = cteCap c) slot2 a \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 a \<and> valid_cap' cap2 a \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 a)) s) and ?R542 cap2a cap1a slot3a slot2a slot1a) s \<and> s' \<in> {s. slot2_'_update (\<lambda>_. slot2a) (cap2_'_update (\<lambda>_. cap2a) (slot1_'_update (\<lambda>_. slot1a) (cap1_'_update (\<lambda>_. cap1a) s))) \<in> UNIV \<inter> \<lbrace>\<acute>slot1 = slot1a\<rbrace> \<inter> \<lbrace>\<acute>slot2 = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>cap1\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>cap2\<rbrace>} \<inter> \<lbrace>slot1 = slot3\<rbrace> \<union> {s. destSlot_'_update (\<lambda>_. slot3a) (srcSlot_'_update (\<lambda>_. slot2a) (newCap_'_update (\<lambda>_. cap2a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot3a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. slot2a) (srcSlot_'_update (\<lambda>_. slot1a) (newCap_'_update (\<lambda>_. cap1a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot2a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot1a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>newCap\<rbrace>}} \<inter> - \<lbrace>slot1 = slot3\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a rv' t t'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 2. \<And>cap2a cap1a slot3a slot2a slot1a rv rv'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q536 cap2a cap1a slot3a slot2a slot1a rv) (?Q'536 cap2a cap1a slot3a slot2a slot1a rv rv') [SKIP] (return (Inr rv)) (?d'536 cap2a cap1a slot3a slot2a slot1a rv')
 3. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R542 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od \<lbrace>?Q536 cap2a cap1a slot3a slot2a slot1a\<rbrace>
 4. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'536 cap2a cap1a slot3a slot2a slot1a)
 5. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. slot1 = slot3 \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2)) s) and (\<lambda>s. slot1 \<noteq> slot3 \<longrightarrow> (valid_mdb' and pspace_aligned' and (\<lambda>a. valid_pspace' a \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap2) slot2 a \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cap2 = cteCap c) slot2 a \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 a \<and> valid_cap' cap2 a \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 a)) s) and ?R542 cap2a cap1a slot3a slot2a slot1a) s \<and> s' \<in> {s. slot2_'_update (\<lambda>_. slot2a) (cap2_'_update (\<lambda>_. cap2a) (slot1_'_update (\<lambda>_. slot1a) (cap1_'_update (\<lambda>_. cap1a) s))) \<in> UNIV \<inter> \<lbrace>\<acute>slot1 = slot1a\<rbrace> \<inter> \<lbrace>\<acute>slot2 = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>cap1\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>cap2\<rbrace>} \<inter> \<lbrace>slot1 = slot3\<rbrace> \<union> {s. destSlot_'_update (\<lambda>_. slot3a) (srcSlot_'_update (\<lambda>_. slot2a) (newCap_'_update (\<lambda>_. cap2a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot3a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. slot2a) (srcSlot_'_update (\<lambda>_. slot1a) (newCap_'_update (\<lambda>_. cap1a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot2a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot1a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>newCap\<rbrace>}} \<inter> - \<lbrace>slot1 = slot3\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a rv rv'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q536 cap2a cap1a slot3a slot2a slot1a rv) (?Q'536 cap2a cap1a slot3a slot2a slot1a rv rv') [SKIP] (return (Inr rv)) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R542 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od \<lbrace>?Q536 cap2a cap1a slot3a slot2a slot1a\<rbrace>
 3. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'536 cap2a cap1a slot3a slot2a slot1a)
 4. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. slot1 = slot3 \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2)) s) and (\<lambda>s. slot1 \<noteq> slot3 \<longrightarrow> (valid_mdb' and pspace_aligned' and (\<lambda>a. valid_pspace' a \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap2) slot2 a \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cap2 = cteCap c) slot2 a \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 a \<and> valid_cap' cap2 a \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 a)) s) and ?R542 cap2a cap1a slot3a slot2a slot1a) s \<and> s' \<in> {s. slot2_'_update (\<lambda>_. slot2a) (cap2_'_update (\<lambda>_. cap2a) (slot1_'_update (\<lambda>_. slot1a) (cap1_'_update (\<lambda>_. cap1a) s))) \<in> UNIV \<inter> \<lbrace>\<acute>slot1 = slot1a\<rbrace> \<inter> \<lbrace>\<acute>slot2 = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>cap1\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>cap2\<rbrace>} \<inter> \<lbrace>slot1 = slot3\<rbrace> \<union> {s. destSlot_'_update (\<lambda>_. slot3a) (srcSlot_'_update (\<lambda>_. slot2a) (newCap_'_update (\<lambda>_. cap2a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot3a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. slot2a) (srcSlot_'_update (\<lambda>_. slot1a) (newCap_'_update (\<lambda>_. cap1a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot2a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot1a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>newCap\<rbrace>}} \<inter> - \<lbrace>slot1 = slot3\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a rv rv'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; dc rv rv'\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return (Inr rv) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R542 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV)
 4. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. slot1 = slot3 \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2)) s) and (\<lambda>s. slot1 \<noteq> slot3 \<longrightarrow> (valid_mdb' and pspace_aligned' and (\<lambda>a. valid_pspace' a \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap2) slot2 a \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cap2 = cteCap c) slot2 a \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 a \<and> valid_cap' cap2 a \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 a)) s) and ?R542 cap2a cap1a slot3a slot2a slot1a) s \<and> s' \<in> {s. slot2_'_update (\<lambda>_. slot2a) (cap2_'_update (\<lambda>_. cap2a) (slot1_'_update (\<lambda>_. slot1a) (cap1_'_update (\<lambda>_. cap1a) s))) \<in> UNIV \<inter> \<lbrace>\<acute>slot1 = slot1a\<rbrace> \<inter> \<lbrace>\<acute>slot2 = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>cap1\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>cap2\<rbrace>} \<inter> \<lbrace>slot1 = slot3\<rbrace> \<union> {s. destSlot_'_update (\<lambda>_. slot3a) (srcSlot_'_update (\<lambda>_. slot2a) (newCap_'_update (\<lambda>_. cap2a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot3a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. slot2a) (srcSlot_'_update (\<lambda>_. slot1a) (newCap_'_update (\<lambda>_. cap1a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot2a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot1a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>newCap\<rbrace>}} \<inter> - \<lbrace>slot1 = slot3\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a rv rv' \<sigma>. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; dc rv rv'\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return (Inr rv) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))}
 2. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R542 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV)
 4. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. slot1 = slot3 \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2)) s) and (\<lambda>s. slot1 \<noteq> slot3 \<longrightarrow> (valid_mdb' and pspace_aligned' and (\<lambda>a. valid_pspace' a \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap2) slot2 a \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cap2 = cteCap c) slot2 a \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 a \<and> valid_cap' cap2 a \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 a)) s) and ?R542 cap2a cap1a slot3a slot2a slot1a) s \<and> s' \<in> {s. slot2_'_update (\<lambda>_. slot2a) (cap2_'_update (\<lambda>_. cap2a) (slot1_'_update (\<lambda>_. slot1a) (cap1_'_update (\<lambda>_. cap1a) s))) \<in> UNIV \<inter> \<lbrace>\<acute>slot1 = slot1a\<rbrace> \<inter> \<lbrace>\<acute>slot2 = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>cap1\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>cap2\<rbrace>} \<inter> \<lbrace>slot1 = slot3\<rbrace> \<union> {s. destSlot_'_update (\<lambda>_. slot3a) (srcSlot_'_update (\<lambda>_. slot2a) (newCap_'_update (\<lambda>_. cap2a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot3a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. slot2a) (srcSlot_'_update (\<lambda>_. slot1a) (newCap_'_update (\<lambda>_. cap1a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot2a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot1a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>newCap\<rbrace>}} \<inter> - \<lbrace>slot1 = slot3\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cap2a cap1a \<sigma> x. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (return (Inr ()) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (\<lambda>y. ()) ret__unsigned_long_' (x\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))
 2. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R542 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV)
 4. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. slot1 = slot3 \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2)) s) and (\<lambda>s. slot1 \<noteq> slot3 \<longrightarrow> (valid_mdb' and pspace_aligned' and (\<lambda>a. valid_pspace' a \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap2) slot2 a \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cap2 = cteCap c) slot2 a \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 a \<and> valid_cap' cap2 a \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 a)) s) and ?R542 cap2a cap1a slot3a slot2a slot1a) s \<and> s' \<in> {s. slot2_'_update (\<lambda>_. slot2a) (cap2_'_update (\<lambda>_. cap2a) (slot1_'_update (\<lambda>_. slot1a) (cap1_'_update (\<lambda>_. cap1a) s))) \<in> UNIV \<inter> \<lbrace>\<acute>slot1 = slot1a\<rbrace> \<inter> \<lbrace>\<acute>slot2 = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>cap1\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>cap2\<rbrace>} \<inter> \<lbrace>slot1 = slot3\<rbrace> \<union> {s. destSlot_'_update (\<lambda>_. slot3a) (srcSlot_'_update (\<lambda>_. slot2a) (newCap_'_update (\<lambda>_. cap2a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot3a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. slot2a) (srcSlot_'_update (\<lambda>_. slot1a) (newCap_'_update (\<lambda>_. cap1a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot2a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot1a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>newCap\<rbrace>}} \<inter> - \<lbrace>slot1 = slot3\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<lbrace>?R542 cap2a cap1a (cte_Ptr slot3) (cte_Ptr slot2) (cte_Ptr slot1)\<rbrace> if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV)
 3. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. slot1 = slot3 \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2)) s) and (\<lambda>s. slot1 \<noteq> slot3 \<longrightarrow> (valid_mdb' and pspace_aligned' and (\<lambda>a. valid_pspace' a \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap2) slot2 a \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cap2 = cteCap c) slot2 a \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 a \<and> valid_cap' cap2 a \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 a)) s) and ?R542 cap2a cap1a slot3a slot2a slot1a) s \<and> s' \<in> {s. slot2_'_update (\<lambda>_. slot2a) (cap2_'_update (\<lambda>_. cap2a) (slot1_'_update (\<lambda>_. slot1a) (cap1_'_update (\<lambda>_. cap1a) s))) \<in> UNIV \<inter> \<lbrace>\<acute>slot1 = slot1a\<rbrace> \<inter> \<lbrace>\<acute>slot2 = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>cap1\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>cap2\<rbrace>} \<inter> \<lbrace>slot1 = slot3\<rbrace> \<union> {s. destSlot_'_update (\<lambda>_. slot3a) (srcSlot_'_update (\<lambda>_. slot2a) (newCap_'_update (\<lambda>_. cap2a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot3a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. slot2a) (srcSlot_'_update (\<lambda>_. slot1a) (newCap_'_update (\<lambda>_. cap1a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot2a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot1a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>newCap\<rbrace>}} \<inter> - \<lbrace>slot1 = slot3\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cap2a cap1a slot3a slot2a slot1a. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV)
 2. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. slot1 = slot3 \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2)) s) and (\<lambda>s. slot1 \<noteq> slot3 \<longrightarrow> (valid_mdb' and pspace_aligned' and (\<lambda>a. valid_pspace' a \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap2) slot2 a \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cap2 = cteCap c) slot2 a \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 a \<and> valid_cap' cap2 a \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 a)) s) and (\<lambda>a. True)) s \<and> s' \<in> {s. slot2_'_update (\<lambda>_. slot2a) (cap2_'_update (\<lambda>_. cap2a) (slot1_'_update (\<lambda>_. slot1a) (cap1_'_update (\<lambda>_. cap1a) s))) \<in> UNIV \<inter> \<lbrace>\<acute>slot1 = slot1a\<rbrace> \<inter> \<lbrace>\<acute>slot2 = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>cap1\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>cap2\<rbrace>} \<inter> \<lbrace>slot1 = slot3\<rbrace> \<union> {s. destSlot_'_update (\<lambda>_. slot3a) (srcSlot_'_update (\<lambda>_. slot2a) (newCap_'_update (\<lambda>_. cap2a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot3a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. slot2a) (srcSlot_'_update (\<lambda>_. slot1a) (newCap_'_update (\<lambda>_. cap1a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot2a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot1a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>newCap\<rbrace>}} \<inter> - \<lbrace>slot1 = slot3\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap2a cap1a slot3a slot2a slot1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; slot3a = cte_Ptr slot3; slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> slot1 \<noteq> slot2 \<and> valid_pspace' s \<and> valid_cap' cap2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. slot1 = slot3 \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2)) s) and (\<lambda>s. slot1 \<noteq> slot3 \<longrightarrow> (valid_mdb' and pspace_aligned' and (\<lambda>a. valid_pspace' a \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap2) slot2 a \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cap2 = cteCap c) slot2 a \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 a \<and> valid_cap' cap2 a \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 a)) s) and (\<lambda>a. True)) s \<and> s' \<in> {s. slot2_'_update (\<lambda>_. slot2a) (cap2_'_update (\<lambda>_. cap2a) (slot1_'_update (\<lambda>_. slot1a) (cap1_'_update (\<lambda>_. cap1a) s))) \<in> UNIV \<inter> \<lbrace>\<acute>slot1 = slot1a\<rbrace> \<inter> \<lbrace>\<acute>slot2 = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>cap1\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>cap2\<rbrace>} \<inter> \<lbrace>slot1 = slot3\<rbrace> \<union> {s. destSlot_'_update (\<lambda>_. slot3a) (srcSlot_'_update (\<lambda>_. slot2a) (newCap_'_update (\<lambda>_. cap2a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot3a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot2a\<rbrace> \<inter> \<lbrace>ccap_relation cap2 \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. slot2a) (srcSlot_'_update (\<lambda>_. slot1a) (newCap_'_update (\<lambda>_. cap1a) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = slot2a\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = slot1a\<rbrace> \<inter> \<lbrace>ccap_relation cap1 \<acute>newCap\<rbrace>}} \<inter> - \<lbrace>slot1 = slot3\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap2a cap1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s; cte_wp_at' (\<lambda>_. True) slot2 s; slot1 \<noteq> slot2; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; valid_cap' cap2 s; cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s; slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s\<rbrakk> \<Longrightarrow> (slot1 = slot3 \<longrightarrow> cte_wp_at' (\<lambda>_. True) slot3 s \<and> slot3 \<noteq> slot2) \<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cap2 = cteCap c) slot2 s) proof (prove)
goal (1 subgoal):
 1. \<And>cap2a cap1a s s'. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; (s, s') \<in> rf_sr; cte_wp_at' (\<lambda>_. True) slot1 s; cte_wp_at' (\<lambda>_. True) slot2 s; slot1 \<noteq> slot2; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; valid_cap' cap2 s; cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = cap2) slot2 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) slot2 s; slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s\<rbrakk> \<Longrightarrow> slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap2) slot2 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cap2 = cteCap c) slot2 s proof (prove)
goal (1 subgoal):
 1. \<And>cap2a cap1a s s' cte ctea ctee. \<lbrakk>ccap_relation cap2 cap2a; ccap_relation cap1 cap1a; (s, s') \<in> rf_sr; slot1 \<noteq> slot2; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; valid_cap' cap2 s; ctes_of s slot1 = Some cte; weak_derived' cap2 (cteCap ctea); isUntypedCap (cteCap ctea) \<longrightarrow> cteCap ctea = cap2; ctes_of s slot2 = Some ctea; cteCap ctea \<noteq> capability.NullCap; slot1 \<noteq> slot3; ctes_of s slot3 = Some ctee; cteCap ctee = capability.NullCap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap ctea) cap2 proof (prove)
goal:
No subgoals!