kings-crown/FVELER_Isabelle huggingface dataset:
theory EmptyFail

lemma empty_fail_getNotification [intro!, wp, simp]:
  "empty_fail (getNotification ep)" by (simp add: getNotification_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (getNotification ep)
theory EmptyFail

lemma empty_fail_lookupIPCBuffer [intro!, wp, simp]:
  "empty_fail (lookupIPCBuffer a b)" by (clarsimp simp: lookupIPCBuffer_def
                     Let_def getThreadBufferSlot_def locateSlot_conv
              split: capability.splits arch_capability.splits | wp | wpc | safe)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (lookupIPCBuffer a b)
theory EmptyFail

lemma empty_fail_updateObject_default [intro!, wp, simp]:
  "empty_fail (updateObject_default v ko a b c)" by (fastforce simp: updateObject_default_def typeError_def unless_def split: kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (updateObject_default v ko a b c)
theory EmptyFail

lemma empty_fail_threadSet [intro!, wp, simp]:
  "empty_fail (threadSet f p)" by (fastforce simp: threadSet_def getObject_def setObject_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (threadSet f p)
theory EmptyFail

lemma empty_fail_getThreadState[iff]:
  "empty_fail (getThreadState t)" by (simp add: getThreadState_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (getThreadState t)
theory EmptyFail

lemma empty_fail_getSchedulerAction [intro!, wp, simp]:
  "empty_fail getSchedulerAction" by (simp add: getSchedulerAction_def getObject_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail getSchedulerAction
theory EmptyFail

lemma empty_fail_scheduleSwitchThreadFastfail [intro!, wp, simp]:
  "empty_fail (scheduleSwitchThreadFastfail a b c d)" by (simp add: scheduleSwitchThreadFastfail_def split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (scheduleSwitchThreadFastfail a b c d)
theory EmptyFail

lemma empty_fail_curDomain [intro!, wp, simp]:
  "empty_fail curDomain" by (simp add: curDomain_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail curDomain
theory SubMonad_R

lemma submonad_doMachineOp:
  "submonad ksMachineState (ksMachineState_update \<circ> K) \<top> doMachineOp" apply (unfold_locales) apply (clarsimp simp: ext stateAssert_def doMachineOp_def o_def gets_def
                             get_def bind_def return_def submonad_fn_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. submonad ksMachineState (ksMachineState_update \<circ> K) (\<lambda>_. True) doMachineOp proof (prove)
goal (5 subgoals):
 1. \<forall>x s. True \<longrightarrow> ksMachineState ((ksMachineState_update \<circ> K) x s) = x
 2. \<forall>x y s. (ksMachineState_update \<circ> K) x ((ksMachineState_update \<circ> K) y s) = (ksMachineState_update \<circ> K) x s
 3. \<forall>s. (ksMachineState_update \<circ> K) (ksMachineState s) s = s
 4. \<And>s x. True = True
 5. doMachineOp = submonad_fn ksMachineState (ksMachineState_update \<circ> K) (\<lambda>_. True) proof (prove)
goal:
No subgoals!
theory SubMonad_R

lemma corres_machine_op:
  assumes P: "corres_underlying Id False True r \<top> \<top> x x'"
  shows      "corres r \<top> \<top> (do_machine_op x) (doMachineOp x')" apply (rule corres_submonad [OF submonad_do_machine_op submonad_doMachineOp _ _ P]) apply (simp_all add: state_relation_def swp_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres r (\<lambda>_. True) (\<lambda>_. True) (do_machine_op x) (doMachineOp x') proof (prove)
goal (2 subgoals):
 1. \<forall>s s'. (s, s') \<in> state_relation \<and> True \<and> True \<longrightarrow> (machine_state s, ksMachineState s') \<in> Id
 2. \<forall>s s' ss ss'. (s, s') \<in> state_relation \<and> (ss, ss') \<in> Id \<longrightarrow> ((machine_state_update \<circ> K) ss s, (ksMachineState_update \<circ> K) ss' s') \<in> state_relation proof (prove)
goal:
No subgoals!
theory SubMonad_R

lemma doMachineOp_mapM:
  assumes "\<And>x. empty_fail (m x)"
  shows "doMachineOp (mapM m l) = mapM (doMachineOp \<circ> m) l" apply (rule submonad_mapM [OF submonad_doMachineOp submonad_doMachineOp,
                                simplified]) apply (rule assms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doMachineOp (mapM m l) = mapM (doMachineOp \<circ> m) l proof (prove)
goal (1 subgoal):
 1. \<And>x. empty_fail (m x) proof (prove)
goal:
No subgoals!
theory SubMonad_R

lemma doMachineOp_mapM_x:
  assumes "\<And>x. empty_fail (m x)"
  shows "doMachineOp (mapM_x m l) = mapM_x (doMachineOp \<circ> m) l" apply (rule submonad_mapM_x [OF submonad_doMachineOp submonad_doMachineOp,
                                simplified]) apply (rule assms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doMachineOp (mapM_x m l) = mapM_x (doMachineOp \<circ> m) l proof (prove)
goal (1 subgoal):
 1. \<And>x. empty_fail (m x) proof (prove)
goal:
No subgoals!
theory SubMonad_R

lemma threadGet_stateAssert_gets_asUser:
  "threadGet (atcbContextGet o tcbArch) t = do stateAssert (tcb_at' t) []; gets (asUser_fetch t) od" apply (rule is_stateAssert_gets [OF _ _ empty_fail_threadGet no_fail_threadGet]) apply (clarsimp simp: threadGet_def liftM_def, wp) apply (simp add: threadGet_def liftM_def, wp getObject_tcb_at') apply (simp add: threadGet_def liftM_def, wp) apply (rule hoare_strengthen_post, rule getObject_obj_at') apply (simp add: objBits_simps')+ apply (clarsimp simp: obj_at'_def asUser_fetch_def projectKOs atcbContextGet_def o_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. threadGet (atcbContextGet \<circ> tcbArch) t = do stateAssert (tcb_at' t) [];
gets (asUser_fetch t)
od proof (prove)
goal (3 subgoals):
 1. \<forall>s. \<lbrace>(=) s\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>\<lambda>_. (=) s\<rbrace>
 2. \<lbrace>\<lambda>_. True\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>\<lambda>_. tcb_at' t\<rbrace>
 3. \<lbrace>tcb_at' t\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>\<lambda>rv s. asUser_fetch t s = rv\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>_. True\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>\<lambda>_. tcb_at' t\<rbrace>
 2. \<lbrace>tcb_at' t\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>\<lambda>rv s. asUser_fetch t s = rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>\<lambda>rv s. asUser_fetch t s = rv\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q23\<rbrace> getObject t \<lbrace>\<lambda>x a. asUser_fetch t a = atcbContextGet (tcbArch x)\<rbrace>
 2. \<And>s. tcb_at' t s \<Longrightarrow> ?Q23 s proof (prove)
goal (4 subgoals):
 1. \<And>q n ko. loadObject t q n ko = loadObject_default t q n ko
 2. \<And>v. 1 < 2 ^ objBits v
 3. \<And>rv s. obj_at' ((=) rv) t s \<Longrightarrow> asUser_fetch t s = atcbContextGet (tcbArch rv)
 4. \<And>s. tcb_at' t s \<Longrightarrow> True proof (prove)
goal (2 subgoals):
 1. \<And>rv s. obj_at' ((=) rv) t s \<Longrightarrow> asUser_fetch t s = atcbContextGet (tcbArch rv)
 2. \<And>s. tcb_at' t s \<Longrightarrow> True proof (prove)
goal:
No subgoals!
theory SubMonad_R

lemma atcbContext_get_eq[simp] : "atcbContextGet (atcbContextSet x atcb) = x" by(simp add: atcbContextGet_def atcbContextSet_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. atcbContextGet (atcbContextSet x atcb) = x
theory SubMonad_R

lemma atcbContext_set_eq[simp] : "atcbContextSet (atcbContextGet t) t = t" by (cases t, simp add: atcbContextGet_def atcbContextSet_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. atcbContextSet (atcbContextGet t) t = t
theory ArchAcc_R

lemma fun_all: "f = f' \<Longrightarrow> (\<forall>s. f s \<longrightarrow> f' s)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f = f' \<Longrightarrow> \<forall>s. f s \<longrightarrow> f' s
theory ArchAcc_R

lemma distrib_imp:
  "P \<longrightarrow> Q \<and> Q' \<Longrightarrow> ((P \<longrightarrow> Q) \<Longrightarrow> (P \<longrightarrow> Q') \<Longrightarrow> R) \<Longrightarrow> R" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<longrightarrow> Q \<and> Q'; \<lbrakk>P \<longrightarrow> Q; P \<longrightarrow> Q'\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory ArchAcc_R

lemma no_0_obj'_abstract:
  "(s, s') \<in> state_relation \<Longrightarrow> no_0_obj' s' \<Longrightarrow> kheap s 0 = None" by (auto intro: pspace_relation_None simp add: no_0_obj'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; no_0_obj' s'\<rbrakk> \<Longrightarrow> kheap s 0 = None
theory ArchAcc_R

lemma corres_gets_asid [corres]:
  "corres (\<lambda>a c. a = c o ucast) \<top> \<top> (gets (arm_asid_table \<circ> arch_state)) (gets (armKSASIDTable \<circ> ksArchState))" by (simp add: state_relation_def arch_state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>a c. a = c \<circ> UCAST(7 \<rightarrow> 32)) (\<lambda>_. True) (\<lambda>_. True) (gets (arm_asid_table \<circ> arch_state)) (gets (armKSASIDTable \<circ> ksArchState))
theory ArchAcc_R

lemma asid_low_bits [simp]:
  "asidLowBits = asid_low_bits" by (simp add: asid_low_bits_def asidLowBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asidLowBits = local.asid_low_bits
theory ArchAcc_R

lemma aligned_distinct_obj_atI':
  "\<lbrakk> ksPSpace s x = Some ko; pspace_aligned' s;
      pspace_distinct' s; ko = injectKO v \<rbrakk>
      \<Longrightarrow> ko_at' v x s" apply (simp add: obj_at'_def projectKOs project_inject
                   pspace_distinct'_def pspace_aligned'_def) apply (drule bspec, erule domI)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s x = Some ko; pspace_aligned' s; pspace_distinct' s; ko = injectKO v\<rbrakk> \<Longrightarrow> ko_at' v x s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s x = Some (injectKO v); \<forall>x\<in>dom (ksPSpace s). is_aligned x (objBitsKO (the (ksPSpace s x))); \<forall>x\<in>dom (ksPSpace s). ps_clear x (objBitsKO (the (ksPSpace s x))) s; ko = injectKO v\<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO (injectKO v)) \<and> ps_clear x (objBitsKO (injectKO v)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s x = Some (injectKO v); ko = injectKO v; is_aligned x (objBitsKO (the (ksPSpace s x))); ps_clear x (objBitsKO (the (ksPSpace s x))) s\<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO (injectKO v)) \<and> ps_clear x (objBitsKO (injectKO v)) s proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma aligned_distinct_relation_asid_pool_atI'[elim]:
  "\<lbrakk> asid_pool_at p s; pspace_relation (kheap s) (ksPSpace s');
     pspace_aligned' s'; pspace_distinct' s' \<rbrakk>
        \<Longrightarrow> asid_pool_at' p s'" apply (drule asid_pool_at_ko) apply (clarsimp simp add: obj_at_def) apply (drule(1) pspace_relation_absD) apply (clarsimp simp: other_obj_relation_def) apply (simp split: Structures_H.kernel_object.split_asm
                     arch_kernel_object.split_asm) apply (drule(2) aligned_distinct_asid_pool_atI') apply (clarsimp simp: obj_at'_def typ_at'_def ko_wp_at'_def
                        projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch AASIDPool) p s; pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'\<rbrakk> \<Longrightarrow> asid_pool_at' p s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; \<exists>pool. ako_at (arch_kernel_obj.ASIDPool pool) p s\<rbrakk> \<Longrightarrow> asid_pool_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>pool. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; kheap s p = Some (ArchObj (arch_kernel_obj.ASIDPool pool))\<rbrakk> \<Longrightarrow> asid_pool_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>pool. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; \<forall>(x', P)\<in>obj_relation_cuts (ArchObj (arch_kernel_obj.ASIDPool pool)) p. \<exists>z. ksPSpace s' x' = Some z \<and> P (ArchObj (arch_kernel_obj.ASIDPool pool)) z\<rbrakk> \<Longrightarrow> asid_pool_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>pool z. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; ksPSpace s' p = Some z; case z of KOArch (KOASIDPool xa) \<Rightarrow> asid_pool_relation pool xa | KOArch _ \<Rightarrow> False | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> asid_pool_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>pool z x8 x1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; ksPSpace s' p = Some (KOArch (KOASIDPool x1)); z = KOArch (KOASIDPool x1); x8 = KOASIDPool x1; asid_pool_relation pool x1\<rbrakk> \<Longrightarrow> asid_pool_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>pool z x8 x1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; z = KOArch (KOASIDPool x1); x8 = KOASIDPool x1; asid_pool_relation pool x1; ko_at' x1 p s'\<rbrakk> \<Longrightarrow> asid_pool_at' p s' proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma getObject_ASIDPool_corres':
  "corres (\<lambda>p p'. p = inv ASIDPool p' o ucast)
          (asid_pool_at p) (pspace_aligned' and pspace_distinct')
          (get_asid_pool p) (getObject p)" apply (rule stronger_corres_guard_imp,
         rule getObject_ASIDPool_corres) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>p p'. p = inv asidpool.ASIDPool p' \<circ> UCAST(10 \<rightarrow> 32)) (typ_at (AArch AASIDPool) p) (pspace_aligned' and pspace_distinct') (get_asid_pool p) (getObject p) proof (prove)
goal (3 subgoals):
 1. p = p
 2. \<And>s s'. \<lbrakk>typ_at (AArch AASIDPool) p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> typ_at (AArch AASIDPool) p s
 3. \<And>s s'. \<lbrakk>typ_at (AArch AASIDPool) p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> asid_pool_at' p s' proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma storePDE_cte_wp_at'[wp]:
  "\<lbrace>\<lambda>s. P (cte_wp_at' P' p s)\<rbrace>
     storePDE ptr val
   \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>" apply (simp add: storePDE_def) apply (wp setObject_cte_wp_at2'[where Q="\<top>"]) apply (clarsimp simp: updateObject_default_def in_monad
                          projectKO_opts_defs projectKOs) apply (rule equals0I) apply (clarsimp simp: updateObject_default_def in_monad
                         projectKOs projectKO_opts_defs) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at' P' p s)\<rbrace> storePDE ptr val \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at' P' p s)\<rbrace> setObject ptr val \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject val (KOTCB tcb) ptr x n s); True; lookupAround2 ptr (ksPSpace s) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> \<exists>tcb'. t = (KOTCB tcb', s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb' = getF tcb)
 2. \<And>x n cte s. fst (updateObject val (KOCTE cte) ptr x n s) = {}
 3. \<And>s. P (cte_wp_at' P' p s) \<Longrightarrow> P (cte_wp_at' P' p s) \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>x n cte s. fst (updateObject val (KOCTE cte) ptr x n s) = {}
 2. \<And>s. P (cte_wp_at' P' p s) \<Longrightarrow> P (cte_wp_at' P' p s) \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>x n cte s y. y \<in> fst (updateObject val (KOCTE cte) ptr x n s) \<Longrightarrow> False
 2. \<And>s. P (cte_wp_at' P' p s) \<Longrightarrow> P (cte_wp_at' P' p s) \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s. P (cte_wp_at' P' p s) \<Longrightarrow> P (cte_wp_at' P' p s) \<and> True proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma storePTE_cte_wp_at'[wp]:
  "\<lbrace>\<lambda>s. P (cte_wp_at' P' p s)\<rbrace>
     storePTE ptr val
   \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>" apply (simp add: storePTE_def) apply (wp setObject_cte_wp_at2'[where Q="\<top>"]) apply (clarsimp simp: updateObject_default_def in_monad
                          projectKO_opts_defs projectKOs) apply (rule equals0I) apply (clarsimp simp: updateObject_default_def in_monad
                         projectKOs projectKO_opts_defs) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at' P' p s)\<rbrace> storePTE ptr val \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at' P' p s)\<rbrace> setObject ptr val \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject val (KOTCB tcb) ptr x n s); True; lookupAround2 ptr (ksPSpace s) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> \<exists>tcb'. t = (KOTCB tcb', s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb' = getF tcb)
 2. \<And>x n cte s. fst (updateObject val (KOCTE cte) ptr x n s) = {}
 3. \<And>s. P (cte_wp_at' P' p s) \<Longrightarrow> P (cte_wp_at' P' p s) \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>x n cte s. fst (updateObject val (KOCTE cte) ptr x n s) = {}
 2. \<And>s. P (cte_wp_at' P' p s) \<Longrightarrow> P (cte_wp_at' P' p s) \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>x n cte s y. y \<in> fst (updateObject val (KOCTE cte) ptr x n s) \<Longrightarrow> False
 2. \<And>s. P (cte_wp_at' P' p s) \<Longrightarrow> P (cte_wp_at' P' p s) \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s. P (cte_wp_at' P' p s) \<Longrightarrow> P (cte_wp_at' P' p s) \<and> True proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma setObject_ASIDPool_corres':
  "a = inv ASIDPool a' o ucast \<Longrightarrow>
  corres dc (asid_pool_at p and valid_etcbs) (pspace_aligned' and pspace_distinct')
            (set_asid_pool p a) (setObject p a')" apply (rule stronger_corres_guard_imp[OF setObject_ASIDPool_corres]) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a = inv asidpool.ASIDPool a' \<circ> UCAST(10 \<rightarrow> 32) \<Longrightarrow> corres dc (typ_at (AArch AASIDPool) p and valid_etcbs) (pspace_aligned' and pspace_distinct') (set_asid_pool p a) (setObject p a') proof (prove)
goal (4 subgoals):
 1. a = inv asidpool.ASIDPool a' \<circ> UCAST(10 \<rightarrow> 32) \<Longrightarrow> p = p
 2. a = inv asidpool.ASIDPool a' \<circ> UCAST(10 \<rightarrow> 32) \<Longrightarrow> a = inv asidpool.ASIDPool a' \<circ> UCAST(10 \<rightarrow> 32)
 3. \<And>s s'. \<lbrakk>a = inv asidpool.ASIDPool a' \<circ> UCAST(10 \<rightarrow> 32); (typ_at (AArch AASIDPool) p and valid_etcbs) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (typ_at (AArch AASIDPool) p and valid_etcbs) s
 4. \<And>s s'. \<lbrakk>a = inv asidpool.ASIDPool a' \<circ> UCAST(10 \<rightarrow> 32); (typ_at (AArch AASIDPool) p and valid_etcbs) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> asid_pool_at' p s' proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma pde_relation_aligned_simp:
  "pde_relation_aligned (ucast (p && mask pd_bits >> 2)::12 word) pde pde'
       = pde_relation_aligned ((p::word32) >> 2) pde pde'" by (clarsimp simp: pde_relation_aligned_def
              split: ARM_H.pde.splits if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pde_relation_aligned (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) pde pde' = pde_relation_aligned (p >> 2) pde pde'
theory ArchAcc_R

lemma pde_relation_alignedD:
  "\<lbrakk> kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd));
     pspace_relation (kheap s) (ksPSpace s');
     ksPSpace s' ((p && ~~ mask pd_bits) + (ucast x << 2)) = Some (KOArch (KOPDE pde))\<rbrakk>
     \<Longrightarrow> pde_relation_aligned x (pd x) pde" apply (clarsimp simp:pspace_relation_def) apply (drule bspec,blast) apply (clarsimp simp:pde_relation_def) apply (drule_tac x = x in spec) apply (clarsimp simp:pde_relation_aligned_def
     split:ARM_H.pde.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) x << 2)) = Some (KOArch (KOPDE pde))\<rbrakk> \<Longrightarrow> pde_relation_aligned x (pd x) pde proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); ksPSpace s' ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) x << 2)) = Some (KOArch (KOPDE pde)); pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))\<rbrakk> \<Longrightarrow> pde_relation_aligned x (pd x) pde proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); ksPSpace s' ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) x << 2)) = Some (KOArch (KOPDE pde)); pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>obj_relation_cuts (the (kheap s (p && ~~ mask pd_bits))) (p && ~~ mask pd_bits). case x of (y, P) \<Rightarrow> P (the (kheap s (p && ~~ mask pd_bits))) (the (ksPSpace s' y))\<rbrakk> \<Longrightarrow> pde_relation_aligned x (pd x) pde proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); ksPSpace s' ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) x << 2)) = Some (KOArch (KOPDE pde)); pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x. \<exists>pde. the (ksPSpace s' ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) x << 2))) = KOArch (KOPDE pde) \<and> pde_relation_aligned x (pd x) pde\<rbrakk> \<Longrightarrow> pde_relation_aligned x (pd x) pde proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); ksPSpace s' ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) x << 2)) = Some (KOArch (KOPDE pde)); pspace_dom (kheap s) = dom (ksPSpace s'); \<exists>pde. the (ksPSpace s' ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) x << 2))) = KOArch (KOPDE pde) \<and> pde_relation_aligned x (pd x) pde\<rbrakk> \<Longrightarrow> pde_relation_aligned x (pd x) pde proof (prove)
goal:
No subgoals!