theory CSpace_RAB_C

lemma ccorres_locateSlotCap_push:
  "ccorres_underlying sr \<Gamma> r xf ar axf P P' hs
    (a >>=E (\<lambda>x. locateSlotCap cp n >>= (\<lambda>p. b p x))) c
    \<Longrightarrow> (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, - )
    \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf P P' hs
    (locateSlotCap cp n >>= (\<lambda>p. a >>=E (\<lambda>x. b p x))) c" apply (simp add: locateSlot_conv) apply (rule ccorres_guard_imp2) apply (rule ccorres_stateAssert) apply (erule monadic_rewrite_ccorres_assemble) apply (rule monadic_rewrite_bindE[OF monadic_rewrite_refl]) apply (rule monadic_rewrite_transverse) apply (rule monadic_rewrite_bind_head) apply (rule monadic_rewrite_stateAssert[where f="return", simplified]) apply (rule monadic_rewrite_refl) apply simp apply (rule monadic_rewrite_refl) apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres_underlying sr \<Gamma> r xf ar axf P P' hs (doE x <- a;
do p <- locateSlotCap cp n;
b p x
od
odE) c; \<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf P P' hs (do p <- locateSlotCap cp n;
a >>=E b p
od) c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres_underlying sr \<Gamma> r xf ar axf P P' hs (doE x <- a;
do xa <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od
odE) c; \<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf P P' hs (do x <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
a >>=E b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n)
od) c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccorres_underlying sr \<Gamma> r xf ar axf P P' hs (doE x <- a;
do xa <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od
odE) c; \<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf ?Q6 ?Q'6 hs (do x <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
a >>=E b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n)
od) c
 2. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf ar axf P P' hs (doE x <- a;
do xa <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od
odE) c; \<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -; (s, s') \<in> sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ?Q6 s \<and> s' \<in> ?Q'6 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccorres_underlying sr \<Gamma> r xf ar axf P P' hs (doE x <- a;
do xa <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od
odE) c; \<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf ?P9 ?Q'6 hs (a >>=E b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n)) c
 2. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf ar axf P P' hs (doE x <- a;
do xa <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od
odE) c; \<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -; (s, s') \<in> sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ((isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB \<longrightarrow> ?P9 s) \<and> s' \<in> ?Q'6 proof (prove)
goal (2 subgoals):
 1. (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -) \<Longrightarrow> monadic_rewrite ?F11 ?E11 ?Q11 (a >>=E b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n)) (doE x <- a;
do xa <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od
odE)
 2. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf ar axf P P' hs (doE x <- a;
do xa <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od
odE) c; \<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -; (s, s') \<in> sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ((isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB \<longrightarrow> (P and ?Q11) s) \<and> s' \<in> P' proof (prove)
goal (3 subgoals):
 1. \<And>x. (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -) \<Longrightarrow> monadic_rewrite ?F11 ?E11 (?Q13 x) (b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x) (do xa <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od)
 2. (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -) \<Longrightarrow> \<lbrace>?R13\<rbrace> a \<lbrace>?Q13\<rbrace>, -
 3. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf ar axf P P' hs (doE x <- a;
do xa <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od
odE) c; \<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -; (s, s') \<in> sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ((isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB \<longrightarrow> (P and ((\<lambda>_. True) and ?R13)) s) \<and> s' \<in> P' proof (prove)
goal (4 subgoals):
 1. \<And>x. (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -) \<Longrightarrow> monadic_rewrite False True (?Q17 x) (do xa <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od) (?b17 x)
 2. \<And>x. (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -) \<Longrightarrow> monadic_rewrite ?F11 ?E11 (?P17 x) (b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x) (?b17 x)
 3. (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -) \<Longrightarrow> \<lbrace>?R13\<rbrace> a \<lbrace>\<lambda>x. ?P17 x and ?Q17 x\<rbrace>, -
 4. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf ar axf P P' hs (doE x <- a;
do xa <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od
odE) c; \<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -; (s, s') \<in> sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ((isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB \<longrightarrow> (P and ((\<lambda>_. True) and ?R13)) s) \<and> s' \<in> P' proof (prove)
goal (4 subgoals):
 1. \<And>x. (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -) \<Longrightarrow> monadic_rewrite False True (?Q17 x) (stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) []) (?g20 x)
 2. \<And>x. (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -) \<Longrightarrow> monadic_rewrite ?F11 ?E11 (?P17 x) (b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x) (do xa <- ?g20 x;
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od)
 3. (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -) \<Longrightarrow> \<lbrace>?R13\<rbrace> a \<lbrace>\<lambda>x. ?P17 x and ?Q17 x\<rbrace>, -
 4. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf ar axf P P' hs (doE x <- a;
do xa <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od
odE) c; \<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -; (s, s') \<in> sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ((isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB \<longrightarrow> (P and ((\<lambda>_. True) and ?R13)) s) \<and> s' \<in> P' proof (prove)
goal (4 subgoals):
 1. \<And>x. (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -) \<Longrightarrow> monadic_rewrite False True (?P22 x) (return ()) (?g20 x)
 2. \<And>x. (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -) \<Longrightarrow> monadic_rewrite ?F11 ?E11 (?P17 x) (b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x) (do xa <- ?g20 x;
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od)
 3. (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -) \<Longrightarrow> \<lbrace>?R13\<rbrace> a \<lbrace>\<lambda>x. ?P17 x and (\<lambda>s. (False \<longrightarrow> (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB \<longrightarrow> ?P22 x s) \<and> (\<not> False \<longrightarrow> ?P22 x s \<and> ((isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB)))\<rbrace>, -
 4. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf ar axf P P' hs (doE x <- a;
do xa <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od
odE) c; \<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -; (s, s') \<in> sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ((isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB \<longrightarrow> (P and ((\<lambda>_. True) and ?R13)) s) \<and> s' \<in> P' proof (prove)
goal (3 subgoals):
 1. \<And>x. (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -) \<Longrightarrow> monadic_rewrite ?F11 ?E11 (?P17 x) (b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x) (do xa <- return ();
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od)
 2. (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -) \<Longrightarrow> \<lbrace>?R13\<rbrace> a \<lbrace>\<lambda>x. ?P17 x and (\<lambda>s. (False \<longrightarrow> (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB \<longrightarrow> True) \<and> (\<not> False \<longrightarrow> True \<and> ((isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB)))\<rbrace>, -
 3. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf ar axf P P' hs (doE x <- a;
do xa <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od
odE) c; \<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -; (s, s') \<in> sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ((isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB \<longrightarrow> (P and ((\<lambda>_. True) and ?R13)) s) \<and> s' \<in> P' proof (prove)
goal (3 subgoals):
 1. \<And>x. (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -) \<Longrightarrow> monadic_rewrite ?F11 ?E11 (?P17 x) (b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x) (b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x)
 2. (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -) \<Longrightarrow> \<lbrace>?R13\<rbrace> a \<lbrace>\<lambda>x. ?P17 x and (\<lambda>s. (False \<longrightarrow> (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB \<longrightarrow> True) \<and> (\<not> False \<longrightarrow> True \<and> ((isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB)))\<rbrace>, -
 3. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf ar axf P P' hs (doE x <- a;
do xa <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od
odE) c; \<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -; (s, s') \<in> sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ((isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB \<longrightarrow> (P and ((\<lambda>_. True) and ?R13)) s) \<and> s' \<in> P' proof (prove)
goal (2 subgoals):
 1. (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -) \<Longrightarrow> \<lbrace>?R13\<rbrace> a \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>s. (False \<longrightarrow> (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB \<longrightarrow> True) \<and> (\<not> False \<longrightarrow> True \<and> ((isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB)))\<rbrace>, -
 2. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf ar axf P P' hs (doE x <- a;
do xa <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od
odE) c; \<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -; (s, s') \<in> sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ((isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB \<longrightarrow> (P and ((\<lambda>_. True) and ?R13)) s) \<and> s' \<in> P' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf ar axf P P' hs (doE x <- a;
do xa <- stateAssert (\<lambda>s. (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB) [];
b (global.capUntypedPtr cp + 2 ^ cte_level_bits * n) x
od
odE) c; \<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, -; (s, s') \<in> sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ((isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB \<longrightarrow> (P and ((\<lambda>_. True) and ((\<lambda>_. True) and (\<lambda>s. (False \<longrightarrow> (isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB \<longrightarrow> True) \<and> (\<not> False \<longrightarrow> True \<and> ((isCNodeCap cp \<or> isZombie cp \<and> capZombieType cp \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cp) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cp \<and> na = capCNodeBits cp \<or> isZombie cp \<and> na = zombieCTEBits (capZombieType cp)) \<and> n < 2 ^ na) \<or> isThreadCap cp \<or> isZombie cp \<and> capZombieType cp = ZombieTCB)))))) s) \<and> s' \<in> P' proof (prove)
goal:
No subgoals!