theory CNodeInv_R

lemma invokeCNode_invs' [wp]:
  "\<lbrace>invs' and sch_act_simple and valid_cnode_inv' cinv\<rbrace>
    invokeCNode cinv \<lbrace>\<lambda>y. invs'\<rbrace>" unfolding invokeCNode_def apply (wpsimp wp: cteRevoke_invs' cteInsert_invs cteMove_ex cteMove_cte_wp_at
getCTE_wp cteDelete_invs'
            simp: unless_def getSlotCap_def getThreadCallerSlot_def locateSlot_conv
         split_del: if_split) apply (cases cinv; clarsimp) apply (clarsimp simp: cte_wp_at_ctes_of is_derived'_def isCap_simps badge_derived'_def) apply (erule(1) valid_irq_handlers_ctes_ofD) apply (clarsimp simp: invs'_def valid_state'_def) apply (clarsimp simp: cte_wp_at_ctes_of) apply (intro conjI impI; clarsimp elim!: weak_derived_sym') apply (clarsimp simp: cte_wp_at_ctes_of elim!: weak_derived_sym') apply (clarsimp simp: cte_wp_at_ctes_of elim!: weak_derived_sym') apply (fastforce dest: ctes_of_valid') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and valid_cnode_inv' cinv\<rbrace> invokeCNode cinv \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and valid_cnode_inv' cinv\<rbrace> case cinv of Insert cap srcSlot destSlot \<Rightarrow> withoutPreemption $ cteInsert cap srcSlot destSlot | Rotate cap1 cap2 slot1 slot2 slot3 \<Rightarrow> withoutPreemption $ if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od | Revoke destSlot \<Rightarrow> cteRevoke destSlot | Move cap srcSlot destSlot \<Rightarrow> withoutPreemption $ cteMove cap srcSlot destSlot | CancelBadgedSends (capability.EndpointCap ptr b xa xaa xb xc) \<Rightarrow> withoutPreemption $ unless (b = 0) $ cancelBadgedSends ptr b | CancelBadgedSends _ \<Rightarrow> haskell_fail [] | SaveCaller destSlot \<Rightarrow> withoutPreemption $ do thread <- getCurThread;
srcSlot <- getThreadCallerSlot thread;
cap <- getSlotCap srcSlot;
case cap of capability.NullCap \<Rightarrow> return () | capability.ReplyCap x True xa \<Rightarrow> haskell_fail [] | capability.ReplyCap x False xa \<Rightarrow> cteMove cap srcSlot destSlot | _ \<Rightarrow> haskell_fail []
od | Delete destSlot \<Rightarrow> cteDelete destSlot True \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; sch_act_simple s; valid_cnode_inv' cinv s\<rbrakk> \<Longrightarrow> (\<forall>x xa xb. cinv = Insert x xa xb \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) xb s \<and> valid_cap' x s \<and> xa \<noteq> xb \<and> cte_wp_at' (is_derived' (ctes_of s) xa x \<circ> cteCap) xa s \<and> cte_wp_at' (untyped_derived_eq x \<circ> cteCap) xa s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) xb s \<and> (\<forall>irq. x = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s)) \<and> (\<forall>x xa xb xc xd. cinv = Rotate x xa xb xc xd \<longrightarrow> (xb = xd \<longrightarrow> valid_cap' x s \<and> valid_cap' xa s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) xd s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) xc s \<and> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = x) xd s \<and> cte_wp_at' (weak_derived' xa \<circ> cteCap) xc s \<and> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = xa) xc s \<and> cte_wp_at' (weak_derived' x \<circ> cteCap) xd s \<and> xd \<noteq> xc) \<and> (xb \<noteq> xd \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) xd s \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) xa) xc s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> xa = cteCap c) xc s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) xc s \<and> valid_cap' xa s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) xd s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) xc s \<and> cte_wp_at' (weak_derived' xa \<circ> cteCap) xc s \<and> cte_wp_at' ((=) capability.NullCap \<circ> cteCap) xd s \<and> xc \<noteq> xd \<and> cte_wp_at' (\<lambda>_. True) xb s \<and> (if xc = xb then x = capability.NullCap else cte_wp_at' ((\<lambda>a. weak_derived' a x) \<circ> cteCap) xb s) \<and> cte_wp_at' (\<lambda>_. True) xb s \<and> (if xc = xb then True else cte_wp_at' ((\<lambda>a. isUntypedCap a \<longrightarrow> x = a) \<circ> cteCap) xb s) \<and> cte_wp_at' (\<lambda>_. True) xb s \<and> (if xc = xb then False else cte_wp_at' ((\<lambda>a. a \<noteq> capability.NullCap) \<circ> cteCap) xb s) \<and> valid_cap' x s \<and> cte_wp_at' (\<lambda>_. True) xc s)) \<and> (\<forall>x xa xb. cinv = Move x xa xb \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) xb s \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) x) xa s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> x = cteCap c) xa s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) xa s \<and> valid_cap' x s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) xb s) \<and> (\<forall>x. cinv = SaveCaller x \<longrightarrow> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s)) \<and> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (\<forall>xa xb xc. cteCap cte = capability.ReplyCap xa xb xc \<longrightarrow> \<not> xb \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) (capability.ReplyCap xa False xc)) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability.ReplyCap xa False xc = cteCap c) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> valid_cap' (capability.ReplyCap xa False xc) s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s)))) proof (prove)
goal (4 subgoals):
 1. \<And>s x12 x13 irq. \<lbrakk>invs' s; sch_act_simple s; cinv = Insert (capability.IRQHandlerCap irq) x12 x13; valid_cap' (capability.IRQHandlerCap irq) s; cte_wp_at' (is_derived' (ctes_of s) x12 (capability.IRQHandlerCap irq) \<circ> cteCap) x12 s; cte_wp_at' (untyped_derived_eq (capability.IRQHandlerCap irq) \<circ> cteCap) x12 s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x13 s; x12 \<noteq> x13; ex_cte_cap_wp_to' (\<lambda>_. True) x13 s\<rbrakk> \<Longrightarrow> irq_issued' irq s
 2. \<And>s x21 x22 x23 x24 x25. \<lbrakk>invs' s; sch_act_simple s; cinv = Rotate x21 x22 x23 x24 x25; valid_cap' x21 s; valid_cap' x22 s; cte_wp_at' (\<lambda>c. weak_derived' x21 (cteCap c)) x23 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x21) x23 s; cte_wp_at' (\<lambda>c. weak_derived' x22 (cteCap c)) x24 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x22) x24 s; x23 \<noteq> x24; x24 \<noteq> x25; x21 \<noteq> capability.NullCap; x22 \<noteq> capability.NullCap; x23 \<noteq> x25 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x25 s; ex_cte_cap_wp_to' (\<lambda>_. True) x24 s; ex_cte_cap_wp_to' (\<lambda>_. True) x25 s\<rbrakk> \<Longrightarrow> (x23 = x25 \<longrightarrow> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = x21) x25 s \<and> cte_wp_at' (weak_derived' x22 \<circ> cteCap) x24 s \<and> cte_wp_at' (weak_derived' x21 \<circ> cteCap) x25 s) \<and> (x23 \<noteq> x25 \<longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) x22) x24 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> x22 = cteCap c) x24 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) x24 s \<and> cte_wp_at' (weak_derived' x22 \<circ> cteCap) x24 s \<and> cte_wp_at' ((=) capability.NullCap \<circ> cteCap) x25 s \<and> cte_wp_at' (\<lambda>_. True) x23 s \<and> cte_wp_at' ((\<lambda>a. weak_derived' a x21) \<circ> cteCap) x23 s \<and> cte_wp_at' (\<lambda>_. True) x23 s \<and> cte_wp_at' ((\<lambda>a. isUntypedCap a \<longrightarrow> x21 = a) \<circ> cteCap) x23 s \<and> cte_wp_at' (\<lambda>_. True) x23 s \<and> cte_wp_at' ((\<lambda>a. a \<noteq> capability.NullCap) \<circ> cteCap) x23 s \<and> cte_wp_at' (\<lambda>_. True) x24 s)
 3. \<And>s x41 x42 x43. \<lbrakk>invs' s; sch_act_simple s; cinv = Move x41 x42 x43; cte_wp_at' (\<lambda>c. weak_derived' x41 (cteCap c)) x42 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x41) x42 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) x42 s; valid_cap' x41 s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x43 s; ex_cte_cap_wp_to' (\<lambda>_. True) x43 s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) x41) x42 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> x41 = cteCap c) x42 s
 4. \<And>s x6. \<lbrakk>invs' s; sch_act_simple s; cinv = SaveCaller x6; ex_cte_cap_wp_to' (\<lambda>_. True) x6 s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x6 s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s)) \<and> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (\<forall>x xa xb. cteCap cte = capability.ReplyCap x xa xb \<longrightarrow> \<not> xa \<longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) (capability.ReplyCap x False xb)) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability.ReplyCap x False xb = cteCap c) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> valid_cap' (capability.ReplyCap x False xb) s))) proof (prove)
goal (4 subgoals):
 1. \<And>s x12 x13 irq cte cteb. \<lbrakk>invs' s; sch_act_simple s; cinv = Insert (capability.IRQHandlerCap irq) x12 x13; valid_cap' (capability.IRQHandlerCap irq) s; x12 \<noteq> x13; ex_cte_cap_wp_to' (\<lambda>_. True) x13 s; ctes_of s x12 = Some cte; untyped_derived_eq (capability.IRQHandlerCap irq) (capability.IRQHandlerCap irq); ctes_of s x13 = Some cteb; cteCap cteb = capability.NullCap; cteCap cte = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> irq_issued' irq s
 2. \<And>s x21 x22 x23 x24 x25. \<lbrakk>invs' s; sch_act_simple s; cinv = Rotate x21 x22 x23 x24 x25; valid_cap' x21 s; valid_cap' x22 s; cte_wp_at' (\<lambda>c. weak_derived' x21 (cteCap c)) x23 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x21) x23 s; cte_wp_at' (\<lambda>c. weak_derived' x22 (cteCap c)) x24 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x22) x24 s; x23 \<noteq> x24; x24 \<noteq> x25; x21 \<noteq> capability.NullCap; x22 \<noteq> capability.NullCap; x23 \<noteq> x25 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x25 s; ex_cte_cap_wp_to' (\<lambda>_. True) x24 s; ex_cte_cap_wp_to' (\<lambda>_. True) x25 s\<rbrakk> \<Longrightarrow> (x23 = x25 \<longrightarrow> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = x21) x25 s \<and> cte_wp_at' (weak_derived' x22 \<circ> cteCap) x24 s \<and> cte_wp_at' (weak_derived' x21 \<circ> cteCap) x25 s) \<and> (x23 \<noteq> x25 \<longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) x22) x24 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> x22 = cteCap c) x24 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) x24 s \<and> cte_wp_at' (weak_derived' x22 \<circ> cteCap) x24 s \<and> cte_wp_at' ((=) capability.NullCap \<circ> cteCap) x25 s \<and> cte_wp_at' (\<lambda>_. True) x23 s \<and> cte_wp_at' ((\<lambda>a. weak_derived' a x21) \<circ> cteCap) x23 s \<and> cte_wp_at' (\<lambda>_. True) x23 s \<and> cte_wp_at' ((\<lambda>a. isUntypedCap a \<longrightarrow> x21 = a) \<circ> cteCap) x23 s \<and> cte_wp_at' (\<lambda>_. True) x23 s \<and> cte_wp_at' ((\<lambda>a. a \<noteq> capability.NullCap) \<circ> cteCap) x23 s \<and> cte_wp_at' (\<lambda>_. True) x24 s)
 3. \<And>s x41 x42 x43. \<lbrakk>invs' s; sch_act_simple s; cinv = Move x41 x42 x43; cte_wp_at' (\<lambda>c. weak_derived' x41 (cteCap c)) x42 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x41) x42 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) x42 s; valid_cap' x41 s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x43 s; ex_cte_cap_wp_to' (\<lambda>_. True) x43 s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) x41) x42 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> x41 = cteCap c) x42 s
 4. \<And>s x6. \<lbrakk>invs' s; sch_act_simple s; cinv = SaveCaller x6; ex_cte_cap_wp_to' (\<lambda>_. True) x6 s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x6 s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s)) \<and> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (\<forall>x xa xb. cteCap cte = capability.ReplyCap x xa xb \<longrightarrow> \<not> xa \<longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) (capability.ReplyCap x False xb)) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability.ReplyCap x False xb = cteCap c) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> valid_cap' (capability.ReplyCap x False xb) s))) proof (prove)
goal (4 subgoals):
 1. \<And>s x12 x13 irq cte cteb. \<lbrakk>invs' s; sch_act_simple s; cinv = Insert (capability.IRQHandlerCap irq) x12 x13; valid_cap' (capability.IRQHandlerCap irq) s; x12 \<noteq> x13; ex_cte_cap_wp_to' (\<lambda>_. True) x13 s; untyped_derived_eq (capability.IRQHandlerCap irq) (capability.IRQHandlerCap irq); ctes_of s x13 = Some cteb; cteCap cteb = capability.NullCap; cteCap cte = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> valid_irq_handlers' s
 2. \<And>s x21 x22 x23 x24 x25. \<lbrakk>invs' s; sch_act_simple s; cinv = Rotate x21 x22 x23 x24 x25; valid_cap' x21 s; valid_cap' x22 s; cte_wp_at' (\<lambda>c. weak_derived' x21 (cteCap c)) x23 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x21) x23 s; cte_wp_at' (\<lambda>c. weak_derived' x22 (cteCap c)) x24 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x22) x24 s; x23 \<noteq> x24; x24 \<noteq> x25; x21 \<noteq> capability.NullCap; x22 \<noteq> capability.NullCap; x23 \<noteq> x25 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x25 s; ex_cte_cap_wp_to' (\<lambda>_. True) x24 s; ex_cte_cap_wp_to' (\<lambda>_. True) x25 s\<rbrakk> \<Longrightarrow> (x23 = x25 \<longrightarrow> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = x21) x25 s \<and> cte_wp_at' (weak_derived' x22 \<circ> cteCap) x24 s \<and> cte_wp_at' (weak_derived' x21 \<circ> cteCap) x25 s) \<and> (x23 \<noteq> x25 \<longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) x22) x24 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> x22 = cteCap c) x24 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) x24 s \<and> cte_wp_at' (weak_derived' x22 \<circ> cteCap) x24 s \<and> cte_wp_at' ((=) capability.NullCap \<circ> cteCap) x25 s \<and> cte_wp_at' (\<lambda>_. True) x23 s \<and> cte_wp_at' ((\<lambda>a. weak_derived' a x21) \<circ> cteCap) x23 s \<and> cte_wp_at' (\<lambda>_. True) x23 s \<and> cte_wp_at' ((\<lambda>a. isUntypedCap a \<longrightarrow> x21 = a) \<circ> cteCap) x23 s \<and> cte_wp_at' (\<lambda>_. True) x23 s \<and> cte_wp_at' ((\<lambda>a. a \<noteq> capability.NullCap) \<circ> cteCap) x23 s \<and> cte_wp_at' (\<lambda>_. True) x24 s)
 3. \<And>s x41 x42 x43. \<lbrakk>invs' s; sch_act_simple s; cinv = Move x41 x42 x43; cte_wp_at' (\<lambda>c. weak_derived' x41 (cteCap c)) x42 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x41) x42 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) x42 s; valid_cap' x41 s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x43 s; ex_cte_cap_wp_to' (\<lambda>_. True) x43 s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) x41) x42 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> x41 = cteCap c) x42 s
 4. \<And>s x6. \<lbrakk>invs' s; sch_act_simple s; cinv = SaveCaller x6; ex_cte_cap_wp_to' (\<lambda>_. True) x6 s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x6 s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s)) \<and> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (\<forall>x xa xb. cteCap cte = capability.ReplyCap x xa xb \<longrightarrow> \<not> xa \<longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) (capability.ReplyCap x False xb)) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability.ReplyCap x False xb = cteCap c) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> valid_cap' (capability.ReplyCap x False xb) s))) proof (prove)
goal (3 subgoals):
 1. \<And>s x21 x22 x23 x24 x25. \<lbrakk>invs' s; sch_act_simple s; cinv = Rotate x21 x22 x23 x24 x25; valid_cap' x21 s; valid_cap' x22 s; cte_wp_at' (\<lambda>c. weak_derived' x21 (cteCap c)) x23 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x21) x23 s; cte_wp_at' (\<lambda>c. weak_derived' x22 (cteCap c)) x24 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x22) x24 s; x23 \<noteq> x24; x24 \<noteq> x25; x21 \<noteq> capability.NullCap; x22 \<noteq> capability.NullCap; x23 \<noteq> x25 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x25 s; ex_cte_cap_wp_to' (\<lambda>_. True) x24 s; ex_cte_cap_wp_to' (\<lambda>_. True) x25 s\<rbrakk> \<Longrightarrow> (x23 = x25 \<longrightarrow> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = x21) x25 s \<and> cte_wp_at' (weak_derived' x22 \<circ> cteCap) x24 s \<and> cte_wp_at' (weak_derived' x21 \<circ> cteCap) x25 s) \<and> (x23 \<noteq> x25 \<longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) x22) x24 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> x22 = cteCap c) x24 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) x24 s \<and> cte_wp_at' (weak_derived' x22 \<circ> cteCap) x24 s \<and> cte_wp_at' ((=) capability.NullCap \<circ> cteCap) x25 s \<and> cte_wp_at' (\<lambda>_. True) x23 s \<and> cte_wp_at' ((\<lambda>a. weak_derived' a x21) \<circ> cteCap) x23 s \<and> cte_wp_at' (\<lambda>_. True) x23 s \<and> cte_wp_at' ((\<lambda>a. isUntypedCap a \<longrightarrow> x21 = a) \<circ> cteCap) x23 s \<and> cte_wp_at' (\<lambda>_. True) x23 s \<and> cte_wp_at' ((\<lambda>a. a \<noteq> capability.NullCap) \<circ> cteCap) x23 s \<and> cte_wp_at' (\<lambda>_. True) x24 s)
 2. \<And>s x41 x42 x43. \<lbrakk>invs' s; sch_act_simple s; cinv = Move x41 x42 x43; cte_wp_at' (\<lambda>c. weak_derived' x41 (cteCap c)) x42 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x41) x42 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) x42 s; valid_cap' x41 s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x43 s; ex_cte_cap_wp_to' (\<lambda>_. True) x43 s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) x41) x42 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> x41 = cteCap c) x42 s
 3. \<And>s x6. \<lbrakk>invs' s; sch_act_simple s; cinv = SaveCaller x6; ex_cte_cap_wp_to' (\<lambda>_. True) x6 s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x6 s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s)) \<and> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (\<forall>x xa xb. cteCap cte = capability.ReplyCap x xa xb \<longrightarrow> \<not> xa \<longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) (capability.ReplyCap x False xb)) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability.ReplyCap x False xb = cteCap c) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> valid_cap' (capability.ReplyCap x False xb) s))) proof (prove)
goal (3 subgoals):
 1. \<And>s x21 x22 x23 x24 x25 cte cteb. \<lbrakk>invs' s; sch_act_simple s; cinv = Rotate x21 x22 x23 x24 x25; valid_cap' x21 s; valid_cap' x22 s; x23 \<noteq> x24; x24 \<noteq> x25; x21 \<noteq> capability.NullCap; x22 \<noteq> capability.NullCap; x23 \<noteq> x25 \<longrightarrow> (\<exists>cte. ctes_of s x25 = Some cte \<and> cteCap cte = capability.NullCap); ex_cte_cap_wp_to' (\<lambda>_. True) x24 s; ex_cte_cap_wp_to' (\<lambda>_. True) x25 s; weak_derived' x21 (cteCap cte); ctes_of s x23 = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = x21; weak_derived' x22 (cteCap cteb); ctes_of s x24 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = x22\<rbrakk> \<Longrightarrow> (x23 = x25 \<longrightarrow> (\<exists>cte. ctes_of s x25 = Some cte \<and> (isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = x21)) \<and> (\<exists>cte. ctes_of s x25 = Some cte \<and> weak_derived' x21 (cteCap cte))) \<and> (x23 \<noteq> x25 \<longrightarrow> weak_derived' (cteCap cteb) x22 \<and> cteCap cteb \<noteq> capability.NullCap \<and> (\<exists>cte. ctes_of s x25 = Some cte \<and> capability.NullCap = cteCap cte) \<and> weak_derived' (cteCap cte) x21 \<and> cteCap cte \<noteq> capability.NullCap)
 2. \<And>s x41 x42 x43. \<lbrakk>invs' s; sch_act_simple s; cinv = Move x41 x42 x43; cte_wp_at' (\<lambda>c. weak_derived' x41 (cteCap c)) x42 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x41) x42 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) x42 s; valid_cap' x41 s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x43 s; ex_cte_cap_wp_to' (\<lambda>_. True) x43 s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) x41) x42 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> x41 = cteCap c) x42 s
 3. \<And>s x6. \<lbrakk>invs' s; sch_act_simple s; cinv = SaveCaller x6; ex_cte_cap_wp_to' (\<lambda>_. True) x6 s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x6 s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s)) \<and> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (\<forall>x xa xb. cteCap cte = capability.ReplyCap x xa xb \<longrightarrow> \<not> xa \<longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) (capability.ReplyCap x False xb)) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability.ReplyCap x False xb = cteCap c) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> valid_cap' (capability.ReplyCap x False xb) s))) proof (prove)
goal (2 subgoals):
 1. \<And>s x41 x42 x43. \<lbrakk>invs' s; sch_act_simple s; cinv = Move x41 x42 x43; cte_wp_at' (\<lambda>c. weak_derived' x41 (cteCap c)) x42 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x41) x42 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) x42 s; valid_cap' x41 s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x43 s; ex_cte_cap_wp_to' (\<lambda>_. True) x43 s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) x41) x42 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> x41 = cteCap c) x42 s
 2. \<And>s x6. \<lbrakk>invs' s; sch_act_simple s; cinv = SaveCaller x6; ex_cte_cap_wp_to' (\<lambda>_. True) x6 s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x6 s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s)) \<and> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (\<forall>x xa xb. cteCap cte = capability.ReplyCap x xa xb \<longrightarrow> \<not> xa \<longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) (capability.ReplyCap x False xb)) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability.ReplyCap x False xb = cteCap c) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> valid_cap' (capability.ReplyCap x False xb) s))) proof (prove)
goal (1 subgoal):
 1. \<And>s x6. \<lbrakk>invs' s; sch_act_simple s; cinv = SaveCaller x6; ex_cte_cap_wp_to' (\<lambda>_. True) x6 s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x6 s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s)) \<and> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (\<forall>x xa xb. cteCap cte = capability.ReplyCap x xa xb \<longrightarrow> \<not> xa \<longrightarrow> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) (capability.ReplyCap x False xb)) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability.ReplyCap x False xb = cteCap c) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> valid_cap' (capability.ReplyCap x False xb) s))) proof (prove)
goal (1 subgoal):
 1. \<And>s x6 cte ctea x xa xb. \<lbrakk>invs' s; sch_act_simple s; cinv = SaveCaller x6; ex_cte_cap_wp_to' (\<lambda>_. True) x6 s; ctes_of s x6 = Some cte; cteCap cte = capability.NullCap; ctes_of s (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) = Some ctea; cteCap ctea = capability.ReplyCap x False xb; \<not> xa\<rbrakk> \<Longrightarrow> valid_cap' (capability.ReplyCap x False xb) s proof (prove)
goal:
No subgoals!