theory Invariants_H

lemma locateSlot_conv:
  "locateSlotBasic A B = return (A + 2 ^ cte_level_bits * B)"
  "locateSlotTCB = locateSlotBasic"
  "locateSlotCNode A bits B = (do
    x \<leftarrow> stateAssert (\<lambda>s. case (gsCNodes s A) of None \<Rightarrow> False | Some n \<Rightarrow> n = bits \<and> B < 2 ^ n) [];
    locateSlotBasic A B od)"
  "locateSlotCap c B = (do
    x \<leftarrow> stateAssert (\<lambda>s. ((isCNodeCap c \<or> (isZombie c \<and> capZombieType c \<noteq> ZombieTCB))
            \<and> (case gsCNodes s (capUntypedPtr c) of None \<Rightarrow> False
                | Some n \<Rightarrow> (isCNodeCap c \<and> n = capCNodeBits c
                    \<or> isZombie c \<and> n = zombieCTEBits (capZombieType c)) \<and> B < 2 ^ n))
        \<or> isThreadCap c \<or> (isZombie c \<and> capZombieType c = ZombieTCB)) [];
    locateSlotBasic (capUntypedPtr c) B od)" apply (simp_all add: locateSlotCap_def locateSlotTCB_def fun_eq_iff) apply (simp add: locateSlotBasic_def objBits_simps cte_level_bits_def objBits_defs) apply (simp add: locateSlotCNode_def stateAssert_def) apply (cases c, simp_all add: locateSlotCNode_def isZombie_def isThreadCap_def
                                isCNodeCap_def capUntypedPtr_def stateAssert_def
                                bind_assoc exec_get locateSlotTCB_def
                                objBits_simps'
                           split: zombie_type.split
                           cong: option.case_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (locateSlotBasic A B = return (A + 2 ^ cte_level_bits * B) &&& locateSlotTCB = locateSlotBasic) &&& locateSlotCNode A bits B = do x <- stateAssert (\<lambda>s. case gsCNodes s A of None \<Rightarrow> False | Some n \<Rightarrow> n = bits \<and> B < 2 ^ n) [];
locateSlotBasic A B
od &&& locateSlotCap c B = do x <- stateAssert (\<lambda>s. (isCNodeCap c \<or> isZombie c \<and> capZombieType c \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr c) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap c \<and> n = capCNodeBits c \<or> isZombie c \<and> n = zombieCTEBits (capZombieType c)) \<and> B < 2 ^ n) \<or> isThreadCap c \<or> isZombie c \<and> capZombieType c = ZombieTCB) [];
locateSlotBasic (global.capUntypedPtr c) B
od proof (prove)
goal (3 subgoals):
 1. \<forall>x. locateSlotBasic A B x = return (A + 2 ^ cte_level_bits * B) x
 2. \<forall>x. locateSlotCNode A bits B x = (do x <- stateAssert (\<lambda>s. case gsCNodes s A of None \<Rightarrow> False | Some n \<Rightarrow> n = bits \<and> B < 2 ^ n) [];
locateSlotBasic A B
od) x
 3. (isZombie c \<longrightarrow> (isThreadCap c \<longrightarrow> (isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotCNode (capCNodePtr c) (capCNodeBits c) B x = locateSlotBasic (global.capUntypedPtr c) B x)) \<and> (\<not> isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotBasic (capTCBPtr c) B x = locateSlotBasic (global.capUntypedPtr c) B x))) \<and> (\<not> isThreadCap c \<longrightarrow> (isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotCNode (capCNodePtr c) (capCNodeBits c) B x = (do x <- stateAssert (\<lambda>s. (case gsCNodes s (global.capUntypedPtr c) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap c \<and> n = capCNodeBits c \<or> isZombie c \<and> n = zombieCTEBits (capZombieType c)) \<and> B < 2 ^ n) \<or> capZombieType c = ZombieTCB) [];
locateSlotBasic (global.capUntypedPtr c) B
od) x)) \<and> (\<not> isCNodeCap c \<longrightarrow> (\<forall>x. (case capZombieType c of ZombieTCB \<Rightarrow> locateSlotTCB (PPtr $ fromPPtr $ capZombiePtr c) B | ZombieCNode bits \<Rightarrow> locateSlotCNode (capZombiePtr c) bits B) x = (do x <- stateAssert (\<lambda>s. capZombieType c \<noteq> ZombieTCB \<and> (case gsCNodes s (global.capUntypedPtr c) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap c \<and> n = capCNodeBits c \<or> isZombie c \<and> n = zombieCTEBits (capZombieType c)) \<and> B < 2 ^ n) \<or> capZombieType c = ZombieTCB) [];
locateSlotBasic (global.capUntypedPtr c) B
od) x)))) \<and> (\<not> isZombie c \<longrightarrow> (isThreadCap c \<longrightarrow> (isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotCNode (capCNodePtr c) (capCNodeBits c) B x = locateSlotBasic (global.capUntypedPtr c) B x)) \<and> (\<not> isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotBasic (capTCBPtr c) B x = locateSlotBasic (global.capUntypedPtr c) B x))) \<and> (\<not> isThreadCap c \<longrightarrow> (isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotCNode (capCNodePtr c) (capCNodeBits c) B x = (do x <- stateAssert (\<lambda>s. case gsCNodes s (global.capUntypedPtr c) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap c \<and> n = capCNodeBits c \<or> isZombie c \<and> n = zombieCTEBits (capZombieType c)) \<and> B < 2 ^ n) [];
locateSlotBasic (global.capUntypedPtr c) B
od) x)) \<and> (\<not> isCNodeCap c \<longrightarrow> (\<forall>x. fail x = (do x <- stateAssert (\<lambda>s. False) [];
locateSlotBasic (global.capUntypedPtr c) B
od) x)))) proof (prove)
goal (2 subgoals):
 1. \<forall>x. locateSlotCNode A bits B x = (do x <- stateAssert (\<lambda>s. case gsCNodes s A of None \<Rightarrow> False | Some n \<Rightarrow> n = bits \<and> B < 2 ^ n) [];
locateSlotBasic A B
od) x
 2. (isZombie c \<longrightarrow> (isThreadCap c \<longrightarrow> (isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotCNode (capCNodePtr c) (capCNodeBits c) B x = locateSlotBasic (global.capUntypedPtr c) B x)) \<and> (\<not> isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotBasic (capTCBPtr c) B x = locateSlotBasic (global.capUntypedPtr c) B x))) \<and> (\<not> isThreadCap c \<longrightarrow> (isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotCNode (capCNodePtr c) (capCNodeBits c) B x = (do x <- stateAssert (\<lambda>s. (case gsCNodes s (global.capUntypedPtr c) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap c \<and> n = capCNodeBits c \<or> isZombie c \<and> n = zombieCTEBits (capZombieType c)) \<and> B < 2 ^ n) \<or> capZombieType c = ZombieTCB) [];
locateSlotBasic (global.capUntypedPtr c) B
od) x)) \<and> (\<not> isCNodeCap c \<longrightarrow> (\<forall>x. (case capZombieType c of ZombieTCB \<Rightarrow> locateSlotTCB (PPtr $ fromPPtr $ capZombiePtr c) B | ZombieCNode bits \<Rightarrow> locateSlotCNode (capZombiePtr c) bits B) x = (do x <- stateAssert (\<lambda>s. capZombieType c \<noteq> ZombieTCB \<and> (case gsCNodes s (global.capUntypedPtr c) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap c \<and> n = capCNodeBits c \<or> isZombie c \<and> n = zombieCTEBits (capZombieType c)) \<and> B < 2 ^ n) \<or> capZombieType c = ZombieTCB) [];
locateSlotBasic (global.capUntypedPtr c) B
od) x)))) \<and> (\<not> isZombie c \<longrightarrow> (isThreadCap c \<longrightarrow> (isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotCNode (capCNodePtr c) (capCNodeBits c) B x = locateSlotBasic (global.capUntypedPtr c) B x)) \<and> (\<not> isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotBasic (capTCBPtr c) B x = locateSlotBasic (global.capUntypedPtr c) B x))) \<and> (\<not> isThreadCap c \<longrightarrow> (isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotCNode (capCNodePtr c) (capCNodeBits c) B x = (do x <- stateAssert (\<lambda>s. case gsCNodes s (global.capUntypedPtr c) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap c \<and> n = capCNodeBits c \<or> isZombie c \<and> n = zombieCTEBits (capZombieType c)) \<and> B < 2 ^ n) [];
locateSlotBasic (global.capUntypedPtr c) B
od) x)) \<and> (\<not> isCNodeCap c \<longrightarrow> (\<forall>x. fail x = (do x <- stateAssert (\<lambda>s. False) [];
locateSlotBasic (global.capUntypedPtr c) B
od) x)))) proof (prove)
goal (1 subgoal):
 1. (isZombie c \<longrightarrow> (isThreadCap c \<longrightarrow> (isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotCNode (capCNodePtr c) (capCNodeBits c) B x = locateSlotBasic (global.capUntypedPtr c) B x)) \<and> (\<not> isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotBasic (capTCBPtr c) B x = locateSlotBasic (global.capUntypedPtr c) B x))) \<and> (\<not> isThreadCap c \<longrightarrow> (isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotCNode (capCNodePtr c) (capCNodeBits c) B x = (do x <- stateAssert (\<lambda>s. (case gsCNodes s (global.capUntypedPtr c) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap c \<and> n = capCNodeBits c \<or> isZombie c \<and> n = zombieCTEBits (capZombieType c)) \<and> B < 2 ^ n) \<or> capZombieType c = ZombieTCB) [];
locateSlotBasic (global.capUntypedPtr c) B
od) x)) \<and> (\<not> isCNodeCap c \<longrightarrow> (\<forall>x. (case capZombieType c of ZombieTCB \<Rightarrow> locateSlotTCB (PPtr $ fromPPtr $ capZombiePtr c) B | ZombieCNode bits \<Rightarrow> locateSlotCNode (capZombiePtr c) bits B) x = (do x <- stateAssert (\<lambda>s. capZombieType c \<noteq> ZombieTCB \<and> (case gsCNodes s (global.capUntypedPtr c) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap c \<and> n = capCNodeBits c \<or> isZombie c \<and> n = zombieCTEBits (capZombieType c)) \<and> B < 2 ^ n) \<or> capZombieType c = ZombieTCB) [];
locateSlotBasic (global.capUntypedPtr c) B
od) x)))) \<and> (\<not> isZombie c \<longrightarrow> (isThreadCap c \<longrightarrow> (isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotCNode (capCNodePtr c) (capCNodeBits c) B x = locateSlotBasic (global.capUntypedPtr c) B x)) \<and> (\<not> isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotBasic (capTCBPtr c) B x = locateSlotBasic (global.capUntypedPtr c) B x))) \<and> (\<not> isThreadCap c \<longrightarrow> (isCNodeCap c \<longrightarrow> (\<forall>x. locateSlotCNode (capCNodePtr c) (capCNodeBits c) B x = (do x <- stateAssert (\<lambda>s. case gsCNodes s (global.capUntypedPtr c) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap c \<and> n = capCNodeBits c \<or> isZombie c \<and> n = zombieCTEBits (capZombieType c)) \<and> B < 2 ^ n) [];
locateSlotBasic (global.capUntypedPtr c) B
od) x)) \<and> (\<not> isCNodeCap c \<longrightarrow> (\<forall>x. fail x = (do x <- stateAssert (\<lambda>s. False) [];
locateSlotBasic (global.capUntypedPtr c) B
od) x)))) proof (prove)
goal:
No subgoals!