x64: add refine files, copied from ARM

proof/refine/X64/Bits_R.thy

@@ -0,0 +1,571 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+theory Bits_R
+imports Corres
+begin
+
+
+
+
+
+crunch_ignore (add:
+  bind return "when" get gets fail
+  assert put modify unless select
+  alternative assert_opt gets_the
+  returnOk throwError lift bindE
+  liftE whenE unlessE throw_opt
+  assertE liftM liftME sequence_x
+  zipWithM_x mapM_x sequence mapM sequenceE_x
+  sequenceE mapME mapME_x catch select_f
+  handleE' handleE handle_elseE forM forM_x
+  zipWithM filterM forME_x)
+
+crunch_ignore (add:
+  withoutFailure throw catchFailure rethrowFailure
+  capFaultOnFailure lookupErrorOnFailure
+  nullCapOnFailure nothingOnFailure
+  without_preemption withoutPreemption preemptionPoint
+  cap_fault_on_failure lookup_error_on_failure
+  const_on_failure ignore_failure ignoreFailure
+  empty_on_failure emptyOnFailure unifyFailure
+  unify_failure throw_on_false
+)
+
+context Arch begin (*FIXME: arch_split*)
+
+crunch_ignore (add:
+  invalidateTLB_ASID invalidateTLB_VAASID
+  cleanByVA cleanByVA_PoU invalidateByVA invalidateByVA_I invalidate_I_PoU
+  cleanInvalByVA branchFlush clean_D_PoU cleanInvalidate_D_PoC cleanInvalidateL2Range
+  invalidateL2Range cleanL2Range flushBTAC writeContextID isb dsb dmb
+  setHardwareASID setCurrentPD)
+
+end
+
+crunch_ignore (add:
+  storeWordVM loadWord setRegister getRegister getRestartPC
+  debugPrint set_register get_register
+  setNextPC maskInterrupt clearMemory throw_on_false)
+
+crunch_ignore (add: unifyFailure ignoreFailure)
+
+crunch_ignore (add: empty_on_failure)
+crunch_ignore (add: emptyOnFailure)
+
+context begin interpretation Arch . (*FIXME: arch_split*)
+
+lemma throwE_R: "\<lbrace>\<top>\<rbrace> throw f \<lbrace>P\<rbrace>,-"
+  by (simp add: validE_R_def) wp
+
+lemma withoutFailure_wp [wp]:
+  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> withoutFailure f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> withoutFailure f \<lbrace>Q\<rbrace>,-"
+  "\<lbrace>\<top>\<rbrace> withoutFailure f -,\<lbrace>E\<rbrace>"
+  by (auto simp: validE_R_def validE_E_def valid_def)
+
+lemma no_fail_alignError [simp, wp]:
+  "no_fail \<bottom> (alignError x)"
+  by (simp add: alignError_def)
+
+lemma no_fail_typeError [simp, wp]:
+  "no_fail \<bottom> (typeError xs ko)"
+  by (simp add: typeError_def)
+
+lemma isCap_simps:
+  "isZombie v = (\<exists>v0 v1 v2. v = Zombie v0 v1 v2)"
+  "isArchObjectCap v = (\<exists>v0. v = ArchObjectCap v0)"
+  "isThreadCap v = (\<exists>v0. v = ThreadCap v0)"
+  "isCNodeCap v = (\<exists>v0 v1 v2 v3. v = CNodeCap v0 v1 v2 v3)"
+  "isNotificationCap v = (\<exists>v0 v1 v2 v3. v = NotificationCap v0 v1 v2 v3)"
+  "isEndpointCap v = (\<exists>v0 v1 v2 v3 v4. v = EndpointCap v0 v1 v2 v3 v4)"
+  "isUntypedCap v = (\<exists>d v0 v1 f. v = UntypedCap d v0 v1 f)"
+  "isReplyCap v = (\<exists>v0 v1. v = ReplyCap v0 v1)"
+  "isIRQControlCap v = (v = IRQControlCap)"
+  "isIRQHandlerCap v = (\<exists>v0. v = IRQHandlerCap v0)"
+  "isNullCap v = (v = NullCap)"
+  "isDomainCap v = (v = DomainCap)"
+  "isPageCap w = (\<exists>d v0 v1 v2 v3. w = PageCap d v0 v1 v2 v3)"
+  "isPageTableCap w = (\<exists>v0 v1. w = PageTableCap v0 v1)"
+  "isPageDirectoryCap w = (\<exists>v0 v1. w = PageDirectoryCap v0 v1)"
+  "isASIDControlCap w = (w = ASIDControlCap)"
+  "isASIDPoolCap w = (\<exists>v0 v1. w = ASIDPoolCap v0 v1)"
+  "isArchPageCap cap = (\<exists>d ref rghts sz data. cap = ArchObjectCap (PageCap d ref rghts sz data))"
+  by (auto simp: isCap_defs split: capability.splits arch_capability.splits)
+
+lemma untyped_not_null [simp]:
+  "\<not> isUntypedCap NullCap" by (simp add: isCap_simps)
+
+text {* Miscellaneous facts about low level constructs *}
+
+lemma projectKO_tcb:
+  "(projectKO_opt ko = Some t) = (ko = KOTCB t)"
+  by (cases ko) (auto simp: projectKO_opts_defs)
+
+lemma projectKO_cte:
+  "(projectKO_opt ko = Some t) = (ko = KOCTE t)"
+  by (cases ko) (auto simp: projectKO_opts_defs)
+
+lemma projectKO_ep:
+  "(projectKO_opt ko = Some t) = (ko = KOEndpoint t)"
+  by (cases ko) (auto simp: projectKO_opts_defs)
+
+lemma projectKO_ntfn:
+  "(projectKO_opt ko = Some t) = (ko = KONotification t)"
+  by (cases ko) (auto simp: projectKO_opts_defs)
+
+lemma projectKO_ASID:
+  "(projectKO_opt ko = Some t) = (ko = KOArch (KOASIDPool t))"
+  by (cases ko)
+     (auto simp: projectKO_opts_defs split: arch_kernel_object.splits)
+
+lemma projectKO_PTE:
+  "(projectKO_opt ko = Some t) = (ko = KOArch (KOPTE t))"
+  by (cases ko)
+     (auto simp: projectKO_opts_defs split: arch_kernel_object.splits)
+
+lemma projectKO_PDE:
+  "(projectKO_opt ko = Some t) = (ko = KOArch (KOPDE t))"
+  by (cases ko)
+     (auto simp: projectKO_opts_defs split: arch_kernel_object.splits)
+
+lemma projectKO_user_data:
+  "(projectKO_opt ko = Some (t :: user_data)) = (ko = KOUserData)"
+  by (cases ko)
+     (auto simp: projectKO_opts_defs split: arch_kernel_object.splits)
+
+lemma projectKO_user_data_device:
+  "(projectKO_opt ko = Some (t :: user_data_device)) = (ko = KOUserDataDevice)"
+  by (cases ko)
+     (auto simp: projectKO_opts_defs split: arch_kernel_object.splits)
+
+
+lemmas projectKOs =
+  projectKO_ntfn projectKO_ep projectKO_cte projectKO_tcb
+  projectKO_ASID projectKO_PTE projectKO_PDE projectKO_user_data projectKO_user_data_device
+  projectKO_eq projectKO_eq2
+
+lemma capAligned_epI:
+  "ep_at' p s \<Longrightarrow> capAligned (EndpointCap p a b c d)"
+  apply (clarsimp simp: obj_at'_real_def capAligned_def
+                        objBits_simps word_bits_def)
+  apply (drule ko_wp_at_norm)
+  apply clarsimp
+  apply (drule ko_wp_at_aligned)
+  apply (simp add: objBits_simps projectKOs capUntypedPtr_def isCap_simps)
+  done
+
+lemma capAligned_ntfnI:
+  "ntfn_at' p s \<Longrightarrow> capAligned (NotificationCap p a b c)"
+  apply (clarsimp simp: obj_at'_real_def capAligned_def
+                        objBits_simps word_bits_def capUntypedPtr_def isCap_simps)
+  apply (fastforce dest: ko_wp_at_norm
+                  dest!: ko_wp_at_aligned simp: objBits_simps projectKOs)
+  done
+
+lemma capAligned_tcbI:
+  "tcb_at' p s \<Longrightarrow> capAligned (ThreadCap p)"
+  apply (clarsimp simp: obj_at'_real_def capAligned_def
+                        objBits_simps word_bits_def capUntypedPtr_def isCap_simps)
+  apply (fastforce dest: ko_wp_at_norm
+                  dest!: ko_wp_at_aligned simp: objBits_simps projectKOs)
+  done
+
+lemma capAligned_reply_tcbI:
+  "tcb_at' p s \<Longrightarrow> capAligned (ReplyCap p m)"
+  apply (clarsimp simp: obj_at'_real_def capAligned_def
+                        objBits_simps word_bits_def capUntypedPtr_def isCap_simps)
+  apply (fastforce dest: ko_wp_at_norm
+                  dest!: ko_wp_at_aligned simp: objBits_simps projectKOs)
+  done
+
+lemma ko_at_valid_objs':
+  assumes ko: "ko_at' k p s"
+  assumes vo: "valid_objs' s"
+  assumes k: "\<And>ko. projectKO_opt ko = Some k \<Longrightarrow> injectKO k = ko"
+  shows "valid_obj' (injectKO k) s" using ko vo
+  by (clarsimp simp: valid_objs'_def obj_at'_def projectKOs
+                     project_inject ranI)
+
+lemma obj_at_valid_objs':
+  "\<lbrakk> obj_at' P p s; valid_objs' s \<rbrakk> \<Longrightarrow>
+  \<exists>k. P k \<and>
+      ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko)
+       \<longrightarrow> valid_obj' (injectKO k) s)"
+  apply (drule obj_at_ko_at')
+  apply clarsimp
+  apply (rule_tac x=ko in exI)
+  apply clarsimp
+  apply (erule (1) ko_at_valid_objs')
+  apply simp
+  done
+
+lemma tcb_in_valid_state':
+  "\<lbrakk> st_tcb_at' P t s; valid_objs' s \<rbrakk> \<Longrightarrow> \<exists>st. P st \<and> valid_tcb_state' st s"
+  apply (clarsimp simp: pred_tcb_at'_def)
+  apply (drule obj_at_valid_objs')
+   apply fastforce
+  apply (clarsimp simp: projectKOs)
+  apply (fastforce simp add: valid_obj'_def valid_tcb'_def)
+  done
+
+lemma gct_corres: "corres op = \<top> \<top> (gets cur_thread) getCurThread"
+  by (simp add: getCurThread_def curthread_relation)
+
+lemma gct_wp [wp]: "\<lbrace>\<lambda>s. P (ksCurThread s) s\<rbrace> getCurThread \<lbrace>P\<rbrace>"
+  by (unfold getCurThread_def, wp)
+
+lemma git_corres:
+  "corres op = \<top> \<top> (gets idle_thread) getIdleThread"
+  by (simp add: getIdleThread_def state_relation_def)
+
+lemma git_wp [wp]: "\<lbrace>\<lambda>s. P (ksIdleThread s) s\<rbrace> getIdleThread \<lbrace>P\<rbrace>"
+  by (unfold getIdleThread_def, wp)
+
+lemma gsa_wp [wp]: "\<lbrace>\<lambda>s. P (ksSchedulerAction s) s\<rbrace> getSchedulerAction \<lbrace>P\<rbrace>"
+  by (unfold getSchedulerAction_def, wp)
+
+text {* Shorthand names for the relations between faults, errors and failures *}
+
+definition
+  fr :: "ExceptionTypes_A.fault \<Rightarrow> Fault_H.fault \<Rightarrow> bool"
+where
+  fr_def[simp]:
+ "fr x y \<equiv> (y = fault_map x)"
+
+definition
+  ser :: "ExceptionTypes_A.syscall_error \<Rightarrow> Fault_H.syscall_error \<Rightarrow> bool"
+where
+  ser_def[simp]:
+ "ser x y \<equiv> (y = syscall_error_map x)"
+
+definition
+  lfr :: "ExceptionTypes_A.lookup_failure \<Rightarrow> Fault_H.lookup_failure \<Rightarrow> bool"
+where
+  lfr_def[simp]:
+ "lfr x y \<equiv> (y = lookup_failure_map x)"
+
+text {* Correspondence and weakest precondition
+        rules for the "on failure" transformers *}
+
+lemma corres_injection:
+  assumes x: "t = injection_handler fn"
+  assumes y: "t' = injection_handler fn'"
+  assumes z: "\<And>ft ft'. f' ft ft' \<Longrightarrow> f (fn ft) (fn' ft')"
+  shows      "corres (f' \<oplus> r) P P' m m'
+     \<Longrightarrow> corres (f \<oplus> r) P P' (t m) (t' m')"
+  apply (simp add: injection_handler_def handleE'_def x y)
+  apply (rule corres_guard_imp)
+    apply (rule corres_split)
+       defer
+       apply assumption
+      apply (rule wp_post_taut)
+     apply (rule wp_post_taut)
+    apply simp
+   apply simp
+  apply (case_tac v, (clarsimp simp: z)+)
+  done
+
+lemma corres_gets_pspace:
+  "corres pspace_relation \<top> \<top> (gets kheap) (gets ksPSpace)"
+  by (subst corres_gets, clarsimp)
+
+lemma rethrowFailure_injection:
+  "rethrowFailure = injection_handler"
+  by (intro ext, simp add: rethrowFailure_def injection_handler_def o_def)
+
+lemma capFault_injection:
+ "capFaultOnFailure addr b = injection_handler (Fault_H.CapFault addr b)"
+  apply (rule ext)
+  apply (simp add: capFaultOnFailure_def rethrowFailure_injection)
+  done
+
+lemma lookupError_injection:
+ "lookupErrorOnFailure b = injection_handler (Fault_H.FailedLookup b)"
+  apply (rule ext)
+  apply (simp add: lookupErrorOnFailure_def rethrowFailure_injection)
+  done
+
+lemma corres_cap_fault:
+  "corres (lfr \<oplus> r) P P' f g \<Longrightarrow>
+   corres (fr \<oplus> r) P P' (cap_fault_on_failure addr b f)
+                        (capFaultOnFailure addr b g)"
+  by (fastforce intro: corres_injection[where f'=lfr]
+         simp: cap_fault_injection capFault_injection)
+
+lemmas capFault_wp[wp] = injection_wp[OF capFault_injection]
+lemmas capFault_wp_E[wp] = injection_wp_E[OF capFault_injection]
+
+lemmas capFault_bindE = injection_bindE[OF capFault_injection capFault_injection]
+
+lemmas capFault_liftE[simp] = injection_liftE[OF capFault_injection]
+
+lemma corres_lookup_error:
+  "\<lbrakk> corres (lfr \<oplus> r) P P' f g \<rbrakk>
+     \<Longrightarrow> corres (ser \<oplus> r) P P' (lookup_error_on_failure b f) (lookupErrorOnFailure b g)"
+  by (fastforce intro: corres_injection[where f'=lfr]
+         simp: lookup_error_injection lookupError_injection)
+
+lemmas lookupError_wp[wp] = injection_wp[OF lookupError_injection]
+lemmas lookupError_wp_E[wp] = injection_wp_E[OF lookupError_injection]
+
+lemmas lookupError_bindE = injection_bindE[OF lookupError_injection lookupError_injection]
+
+lemmas lookupError_liftE[simp] = injection_liftE[OF lookupError_injection]
+
+
+lemma unifyFailure_injection:
+  "unifyFailure = injection_handler (\<lambda>x. ())"
+  by (rule ext,
+      simp add: unifyFailure_def injection_handler_def
+                rethrowFailure_def o_def)
+
+lemmas unifyFailure_injection_corres
+   = corres_injection [where f=dc, simplified, OF _ unifyFailure_injection]
+
+lemmas unifyFailure_discard
+   = unifyFailure_injection_corres [OF id_injection, simplified]
+
+lemmas unifyFailure_wp = injection_wp [OF unifyFailure_injection]
+
+lemmas unifyFailure_wp_E[wp] = injection_wp_E [OF unifyFailure_injection]
+
+lemmas corres_unify_failure =
+    corres_injection [OF unify_failure_injection unifyFailure_injection, rotated]
+
+lemma ignoreFailure_wp[wp_split]:
+  "\<lbrace>P\<rbrace> v \<lbrace>\<lambda>rv. Q ()\<rbrace>,\<lbrace>\<lambda>rv. Q ()\<rbrace> \<Longrightarrow>
+    \<lbrace>P\<rbrace> ignoreFailure v \<lbrace>Q\<rbrace>"
+  by (simp add: ignoreFailure_def const_def) wp
+
+lemma ep'_cases_weak_wp:
+  assumes "\<lbrace>P_A\<rbrace> a \<lbrace>Q\<rbrace>"
+  assumes "\<And>q. \<lbrace>P_B\<rbrace> b q \<lbrace>Q\<rbrace>"
+  assumes "\<And>q. \<lbrace>P_C\<rbrace> c q \<lbrace>Q\<rbrace>"
+  shows
+  "\<lbrace>P_A and P_B and P_C\<rbrace>
+    case ts of
+      IdleEP \<Rightarrow> a
+    | SendEP q \<Rightarrow> b q
+    | RecvEP q \<Rightarrow> c q \<lbrace>Q\<rbrace>"
+  apply (cases ts)
+  apply (simp, rule hoare_weaken_pre, rule assms, simp)+
+  done
+
+lemma ntfn'_cases_weak_wp:
+  assumes "\<lbrace>P_A\<rbrace> a \<lbrace>Q\<rbrace>"
+  assumes "\<And>q. \<lbrace>P_B\<rbrace> b q \<lbrace>Q\<rbrace>"
+  assumes "\<And>bdg. \<lbrace>P_C\<rbrace> c bdg \<lbrace>Q\<rbrace>"
+  shows
+  "\<lbrace>P_A and P_B and P_C\<rbrace>
+    case ts of
+      IdleNtfn \<Rightarrow> a
+    | WaitingNtfn q \<Rightarrow> b q
+    | ActiveNtfn bdg \<Rightarrow> c bdg \<lbrace>Q\<rbrace>"
+  apply (cases ts)
+  apply (simp, rule hoare_weaken_pre, rule assms, simp)+
+  done
+
+lemma ko_at_cte_ctable:
+  fixes ko :: tcb
+  shows "\<lbrakk> ko_at' tcb p s \<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>x. x = tcbCTable tcb) p s"
+  unfolding obj_at'_def
+  apply (clarsimp simp: projectKOs objBits_simps)
+  apply (erule(2) cte_wp_at_tcbI')
+   apply fastforce
+  apply simp
+  done
+
+lemma ko_at_cte_vtable:
+  fixes ko :: tcb
+  shows "\<lbrakk> ko_at' tcb p s \<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>x. x = tcbVTable tcb) (p + 16) s"
+  apply (clarsimp simp: obj_at'_def objBits_simps projectKOs)
+  apply (erule(2) cte_wp_at_tcbI')
+   apply fastforce
+  apply simp
+  done
+
+lemma ko_at_imp_cte_wp_at':
+  fixes x :: cte
+  shows "\<lbrakk> ko_at' x ptr s \<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cte = x) ptr s"
+  apply (erule obj_atE')
+  apply (clarsimp simp: projectKOs objBits_simps)
+  apply (erule cte_wp_at_cteI')
+    apply (simp add: cte_level_bits_def)+
+  done
+
+lemma modify_map_casesD:
+  "modify_map m p f p' = Some cte \<Longrightarrow>
+  (p \<noteq> p' \<longrightarrow> m p' = Some cte) \<and>
+  (p = p' \<longrightarrow> (\<exists>cap node. m p = Some (CTE cap node) \<and> f (CTE cap node) = cte))"
+  apply (simp add: modify_map_def split: if_split_asm)
+  apply clarsimp
+  apply (case_tac z)
+  apply auto
+  done
+
+lemma modify_map_casesE:
+  "\<lbrakk> modify_map m p f p' = Some cte;
+     \<lbrakk> p \<noteq> p'; m p' = Some cte \<rbrakk> \<Longrightarrow> P;
+     \<And>cap node. \<lbrakk> p = p'; m p = Some (CTE cap node); cte = f (CTE cap node) \<rbrakk> \<Longrightarrow> P
+  \<rbrakk> \<Longrightarrow> P"
+  by (auto dest: modify_map_casesD)
+
+
+lemma modify_map_cases:
+  "(modify_map m p f p' = Some cte) =
+  ((p \<noteq> p' \<longrightarrow> m p' = Some cte) \<and>
+   (p = p' \<longrightarrow> (\<exists>cap node. m p = Some (CTE cap node) \<and> f (CTE cap node) = cte)))"
+  apply (rule iffI)
+   apply (erule modify_map_casesD)
+  apply (clarsimp simp: modify_map_def)
+  done
+
+
+lemma no_0_modify_map [simp]:
+  "no_0 (modify_map m p f) = no_0 m"
+  by (simp add: no_0_def modify_map_def)
+
+
+lemma modify_map_0 [simp]:
+  "no_0 m \<Longrightarrow> modify_map m 0 f = m"
+  by (rule ext) (auto simp add: modify_map_def no_0_def)
+
+
+lemma modify_map_exists:
+  "\<exists>cap node. m p = Some (CTE cap node) \<Longrightarrow> \<exists>cap' node'. modify_map m q f p = Some (CTE cap' node')"
+  apply clarsimp
+  apply (case_tac "f (CTE cap node)")
+  apply (cases "q=p")
+   apply (auto simp add: modify_map_cases)
+  done
+
+
+lemma modify_map_exists_rev:
+  "modify_map m q f p = Some (CTE cap node) \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node')"
+  apply (case_tac "f (CTE cap node)")
+  apply (cases "q=p")
+   apply (auto simp add: modify_map_cases)
+  done
+
+
+lemma modify_map_if:
+  "(modify_map m p f p' = Some cte) =
+   (if p = p'
+    then \<exists>cap node. m p = Some (CTE cap node) \<and> f (CTE cap node) = cte
+    else \<exists>cap node. m p' = Some (CTE cap node) \<and> cte = CTE cap node)"
+  apply (cases cte)
+  apply (rule iffI)
+   apply (drule modify_map_casesD)
+   apply auto[1]
+  apply (auto simp: modify_map_def)
+  done
+
+lemma nothingOnFailure_wp [wp]:
+  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>rv. Q None\<rbrace>"
+  shows      "\<lbrace>P\<rbrace> nothingOnFailure f \<lbrace>Q\<rbrace>"
+  apply (simp add: nothingOnFailure_def)
+  apply (wp x)
+  done
+
+lemma corres_empty_on_failure:
+  "corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m' \<Longrightarrow>
+   corres r P P' (empty_on_failure m) (emptyOnFailure m')"
+  apply (simp add: empty_on_failure_def emptyOnFailure_def)
+  apply (rule corres_guard_imp)
+    apply (rule corres_split_catch)
+       apply (rule corres_trivial, simp)
+      apply (erule corres_rel_imp)
+      apply (case_tac x; simp)
+     apply wp+
+   apply simp+
+  done
+
+
+
+lemma emptyOnFailure_wp[wp]:
+  "\<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>rv. Q []\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> emptyOnFailure m \<lbrace>Q\<rbrace>"
+  by (simp add: emptyOnFailure_def) wp
+
+lemma withoutPreemption_lift:
+  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> withoutPreemption f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
+  by simp
+
+lemma withoutPreemption_R:
+  "\<lbrace>\<top>\<rbrace> withoutPreemption f -, \<lbrace>Q\<rbrace>"
+  by (wp withoutPreemption_lift)
+
+lemma ko_at_cte_ipcbuffer:
+  "ko_at' tcb p s \<Longrightarrow> cte_wp_at' (\<lambda>x. x = tcbIPCBufferFrame tcb) (p + tcbIPCBufferSlot * 0x10) s"
+  apply (clarsimp simp: obj_at'_def projectKOs objBits_simps)
+  apply (erule (2) cte_wp_at_tcbI')
+   apply (fastforce simp add: tcb_cte_cases_def tcbIPCBufferSlot_def)
+  apply simp
+  done
+
+lemma tcb_at_cte_offset_unique:
+  assumes tat: "tcb_at' t s"
+  and      vo: "valid_objs' s"
+  and     pal: "pspace_aligned' s"
+  and     csx: "x \<in> dom tcb_cte_cases"
+  and     csy: "y \<in> dom tcb_cte_cases"
+  shows "(tcb_at' (t + x - y) s) = (x = y)"
+proof (rule iffI)
+  assume "tcb_at' (t + x - y) s"
+  hence "is_aligned (t + x - y) 9" using pal
+    apply -
+    apply (erule obj_atE')
+    apply (simp add: projectKOs objBits_simps)
+    done
+  moreover from tat pal have "is_aligned t 9"
+    apply -
+    apply (erule obj_atE')
+    apply (simp add: projectKOs objBits_simps)
+    done
+  ultimately show "x = y" using csx csy
+    apply -
+    apply (drule (1) is_aligned_addD1 [where y = "x - y", simplified add_diff_eq])
+    apply (simp add: tcb_cte_cases_def)
+    apply (auto simp: is_aligned_def dvd_def)
+    apply arith+
+    done
+next
+  assume "x = y"
+  thus "tcb_at' (t + x - y) s" using tat by simp
+qed
+
+lemma set_ep_arch':  "\<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setEndpoint ntfn p \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace>"
+  apply (simp add: setEndpoint_def setObject_def split_def)
+  apply (wp updateObject_default_inv|simp)+
+  done
+
+lemma corres_const_on_failure:
+  "corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m' \<Longrightarrow>
+   corres r P P' (const_on_failure x m) (constOnFailure y m')"
+  apply (simp add: const_on_failure_def constOnFailure_def)
+  apply (rule corres_guard_imp)
+    apply (rule corres_split_catch)
+       apply (rule corres_trivial, simp)
+      apply (erule corres_rel_imp)
+      apply (case_tac xa)
+       apply (clarsimp simp: const_def)
+      apply simp
+     apply wp+
+   apply simp+
+  done
+
+lemma constOnFailure_wp :
+  "\<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv. Q n\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> constOnFailure n m \<lbrace>Q\<rbrace>"
+  apply (simp add: constOnFailure_def const_def)
+  apply (wp|simp)+
+  done
+
+end
+end

proof/refine/X64/BuildRefineCache.thy

@@ -0,0 +1,44 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+theory BuildRefineCache
+imports "~~/src/HOL/Main"
+begin
+
+ML {*
+
+(* needed to generate a proof cache *)
+proofs := 1;
+DupSkip.record_proofs := true;
+quick_and_dirty := true;
+
+tracing "Building refinement image using ROOT.ML";
+
+use "ROOT.ML";
+
+*}
+
+ML {*
+
+tracing "Synching proof cache";
+
+DupSkip.sync_cache @{theory Refine};
+
+tracing "Dumping proof cache";
+
+let
+  val xml = XML_Syntax.xml_forest_of_cache (! DupSkip.the_cache);
+in
+  File.open_output (XML_Syntax.output_forest xml) (Path.basic "proof_cache.xml")
+end;
+
+*}
+
+end

proof/refine/X64/Cache.thy

@@ -0,0 +1,41 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+theory Cache
+imports "~~/src/HOL/Main"
+begin
+
+text {* Enable the proof cache, both skipping from it
+        and recording to it. *}
+ML {* DupSkip.record_proofs := true *}
+ML {* proofs := 1 *}
+
+ML {* DupSkip.skip_dup_proofs := true *}
+
+text {* If executed in reverse order, save the cache *}
+ML {* val cache_thy_save_cache = ref false; *}
+ML {*
+if (! cache_thy_save_cache)
+then File.open_output (XML_Syntax.output_forest
+           (XML_Syntax.xml_forest_of_cache (! DupSkip.the_cache)))
+       (Path.basic "proof_cache.xml")
+else () *}
+ML {* cache_thy_save_cache := true *}
+ML {* cache_thy_save_cache := false *}
+
+text {* Load the proof cache
+           - can take up to a minute *}
+
+ML {*
+DupSkip.the_cache := XML_Syntax.cache_of_xml_forest (
+    File.open_input (XML_Syntax.input_forest)
+           (Path.basic "proof_cache.xml")) *}
+
+end

proof/refine/X64/Corres.thy

@@ -0,0 +1,19 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+theory Corres
+imports StateRelation "../../../lib/Corres_Method"
+begin
+
+text {* Instantiating the corres framework to this particular state relation. *}
+abbreviation
+ "corres \<equiv> corres_underlying state_relation False True"
+
+end

proof/refine/X64/DomainTime_R.thy

@@ -0,0 +1,346 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+theory DomainTime_R
+imports
+  ADT_H
+begin
+
+text {* Preservation of domain time remaining over kernel invocations;
+        invariance of domain list validity
+*}
+
+context begin interpretation Arch . (*FIXME: arch_split*)
+
+(* FIXME move to DetSchedDomainTime_AI *)
+crunch domain_list_inv[wp]: do_user_op "\<lambda>s. P (domain_list s)"
+  (wp: select_wp)
+
+(* abstract and haskell have identical domain list fields *)
+abbreviation
+  valid_domain_list' :: "'a kernel_state_scheme \<Rightarrow> bool"
+where
+  "valid_domain_list' \<equiv> \<lambda>s. valid_domain_list_2 (ksDomSchedule s)"
+
+lemmas valid_domain_list'_def = valid_domain_list_2_def
+
+(* first, crunching valid_domain_list' over the kernel - it is never changed *)
+
+crunch ksDomSchedule_inv[wp]:
+  sendFaultIPC, handleFault, replyFromKernel
+  "\<lambda>s. P (ksDomSchedule s)"
+
+crunch ksDomSchedule_inv[wp]: setDomain "\<lambda>s. P (ksDomSchedule s)"
+  (wp: crunch_wps simp: if_apply_def2)
+
+crunch ksDomSchedule_inv[wp]: sendSignal "\<lambda>s. P (ksDomSchedule s)"
+  (wp: crunch_wps simp: crunch_simps simp: unless_def)
+
+crunch ksDomSchedule_inv[wp]: finaliseCap "\<lambda>s. P (ksDomSchedule s)"
+  (simp: crunch_simps assertE_def unless_def
+ ignore: getObject setObject forM ignoreFailure
+     wp: getObject_inv loadObject_default_inv crunch_wps)
+
+crunch ksDomSchedule_inv[wp]: finaliseCap, capSwapForDelete "\<lambda>s. P (ksDomSchedule s)"
+  (simp: crunch_simps simp: unless_def)
+
+lemma finaliseSlot_ksDomSchedule_inv[wp]:
+  "\<lbrace>\<lambda>s. P (ksDomSchedule s) \<rbrace> finaliseSlot param_a param_b \<lbrace>\<lambda>_ s. P (ksDomSchedule s)\<rbrace>"
+  by (wp finaliseSlot_preservation | clarsimp)+
+
+crunch ksDomSchedule_inv[wp]: invokeTCB "\<lambda>s. P (ksDomSchedule s)"
+  (wp: crunch_wps checkCap_inv finaliseSlot'_preservation simp: if_apply_def2 crunch_simps)
+
+crunch ksDomSchedule_inv[wp]: doReplyTransfer "\<lambda>s. P (ksDomSchedule s)"
+  (wp: crunch_wps transferCapsToSlots_pres1 setObject_ep_ct
+       setObject_ntfn_ct
+        simp: unless_def crunch_simps
+      ignore: transferCapsToSlots setObject getObject)
+
+lemma cteRevoke_ksDomSchedule_inv[wp]:
+  "\<lbrace>\<lambda>s. P (ksDomSchedule s) \<rbrace> cteRevoke param_a \<lbrace>\<lambda>_ s. P (ksDomSchedule s)\<rbrace>"
+  by (wp cteRevoke_preservation | clarsimp)+
+
+crunch ksDomSchedule_inv[wp]: finaliseCap "\<lambda>s. P (ksDomSchedule s)"
+  (simp: crunch_simps assertE_def unless_def
+ ignore: getObject setObject forM ignoreFailure
+     wp: getObject_inv loadObject_default_inv crunch_wps)
+
+crunch ksDomSchedule_inv[wp]: cancelBadgedSends "\<lambda>s. P (ksDomSchedule s)"
+  (ignore: filterM setObject getObject
+     simp: filterM_mapM crunch_simps
+       wp: crunch_wps hoare_unless_wp)
+
+crunch ksDomSchedule_inv[wp]: createNewObjects "\<lambda>s. P (ksDomSchedule s)"
+  (simp: crunch_simps zipWithM_x_mapM wp: crunch_wps hoare_unless_wp)
+
+crunch ksDomSchedule_inv[wp]: preemptionPoint "\<lambda>s. P (ksDomSchedule s)"
+  (simp: whenE_def)
+
+crunch ksDomSchedule_inv[wp]: performARMMMUInvocation "\<lambda>s. P (ksDomSchedule s)"
+  (ignore: getObject setObject
+   wp: crunch_wps getObject_cte_inv getASID_wp
+   simp: unless_def)
+
+crunch ksDomSchedule_inv[wp]: performInvocation "\<lambda>s. P (ksDomSchedule s)"
+  (wp: crunch_wps zipWithM_x_inv cteRevoke_preservation mapME_x_inv_wp
+   simp: unless_def crunch_simps filterM_mapM)
+
+crunch ksDomSchedule_inv[wp]: schedule "\<lambda>s. P (ksDomSchedule s)"
+  (ignore: setNextPC threadSet simp:crunch_simps wp:findM_inv)
+
+crunch ksDomSchedule_inv[wp]: activateThread "\<lambda>s. P (ksDomSchedule s)"
+
+crunch ksDomSchedule_inv[wp]:
+  receiveSignal, getNotification, receiveIPC, deleteCallerCap "\<lambda>s. P (ksDomSchedule s)"
+  (wp: hoare_drop_imps simp: crunch_simps)
+
+lemma handleRecv_ksDomSchedule_inv[wp]:
+  "\<lbrace>\<lambda>s. P (ksDomSchedule s) \<rbrace> handleRecv e \<lbrace>\<lambda>_ s. P (ksDomSchedule s) \<rbrace>"
+  unfolding handleRecv_def
+  by (rule hoare_pre)
+     (wp hoare_drop_imps | simp add: crunch_simps | wpc)+
+
+crunch ksDomSchedule_inv[wp]: handleEvent "\<lambda>s. P (ksDomSchedule s)"
+  (wp: hoare_drop_imps hv_inv' syscall_valid' throwError_wp withoutPreemption_lift
+   simp: runErrorT_def
+   ignore: setThreadState)
+
+lemma callKernel_ksDomSchedule_inv[wp]:
+  "\<lbrace>\<lambda>s. P (ksDomSchedule s) \<rbrace> callKernel e \<lbrace>\<lambda>_ s. P (ksDomSchedule s) \<rbrace>"
+  unfolding callKernel_def
+  by (rule hoare_pre)
+     (wp | simp add: if_apply_def2)+
+
+
+(* now we handle preservation of domain time remaining, which most of the kernel does not change *)
+
+crunch ksDomainTime[wp]: setExtraBadge, cteInsert "\<lambda>s. P (ksDomainTime s)"
+  (wp: crunch_wps)
+
+crunch ksDomainTime[wp]: transferCapsToSlots "\<lambda>s. P (ksDomainTime s)"
+
+crunch ksDomainTime[wp]: setupCallerCap, switchIfRequiredTo, doIPCTransfer, attemptSwitchTo "\<lambda>s. P (ksDomainTime s)"
+  (wp: crunch_wps simp: zipWithM_x_mapM ignore: constOnFailure)
+
+crunch ksDomainTime_inv[wp]: setEndpoint, setNotification, storePTE, storePDE
+  "\<lambda>s. P (ksDomainTime s)"
+  (wp: crunch_wps setObject_ksPSpace_only updateObject_default_inv
+   ignore: setObject)
+
+crunch ksDomainTime_inv[wp]: sendFaultIPC, handleFault, replyFromKernel "\<lambda>s. P (ksDomainTime s)"
+
+crunch ksDomainTime_inv[wp]: setDomain "\<lambda>s. P (ksDomainTime s)"
+  (wp: crunch_wps simp: if_apply_def2)
+
+crunch ksDomainTime_inv[wp]: sendSignal "\<lambda>s. P (ksDomainTime s)"
+  (wp: crunch_wps simp: crunch_simps simp: unless_def)
+
+crunch ksDomainTime_inv[wp]: deleteASID "\<lambda>s. P (ksDomainTime s)"
+  (wp: crunch_wps setObject_ksPSpace_only getObject_inv loadObject_default_inv
+       updateObject_default_inv
+   ignore: setObject getObject simp: whenE_def)
+
+crunch ksDomainTime_inv[wp]: finaliseCap "\<lambda>s. P (ksDomainTime s)"
+  (simp: crunch_simps assertE_def unless_def
+ ignore: getObject setObject forM ignoreFailure
+     wp: setObject_ksPSpace_only getObject_inv loadObject_default_inv crunch_wps)
+
+crunch ksDomainTime_inv[wp]: cancelBadgedSends "\<lambda>s. P (ksDomainTime s)"
+  (wp: crunch_wps setObject_ksPSpace_only getObject_inv loadObject_default_inv
+       updateObject_default_inv hoare_unless_wp
+   ignore: setObject getObject filterM
+   simp: whenE_def filterM_mapM crunch_simps)
+
+crunch ksDomainTime_inv[wp]: capSwapForDelete "\<lambda>s. P (ksDomainTime s)"
+  (simp: crunch_simps simp: unless_def)
+
+lemma finaliseSlot_ksDomainTime_inv[wp]:
+  "\<lbrace>\<lambda>s. P (ksDomainTime s) \<rbrace> finaliseSlot param_a param_b \<lbrace>\<lambda>_ s. P (ksDomainTime s)\<rbrace>"
+  by (wp finaliseSlot_preservation | clarsimp)+
+
+crunch ksDomainTime_inv[wp]: invokeTCB "\<lambda>s. P (ksDomainTime s)"
+  (wp: crunch_wps checkCap_inv finaliseSlot'_preservation simp: if_apply_def2 crunch_simps)
+
+crunch ksDomainTime_inv[wp]: doReplyTransfer "\<lambda>s. P (ksDomainTime s)"
+  (wp: crunch_wps transferCapsToSlots_pres1 setObject_ep_ct
+       setObject_ntfn_ct
+        simp: unless_def crunch_simps
+      ignore: transferCapsToSlots setObject getObject)
+
+lemma cteRevoke_ksDomainTime_inv[wp]:
+  "\<lbrace>\<lambda>s. P (ksDomainTime s) \<rbrace> cteRevoke param_a \<lbrace>\<lambda>_ s. P (ksDomainTime s)\<rbrace>"
+  by (wp cteRevoke_preservation | clarsimp)+
+
+crunch ksDomainTime_inv[wp]: finaliseCap "\<lambda>s. P (ksDomainTime s)"
+  (simp: crunch_simps assertE_def unless_def
+ ignore: getObject setObject forM ignoreFailure
+     wp: getObject_inv loadObject_default_inv crunch_wps)
+
+crunch ksDomainTime_inv[wp]: cancelBadgedSends "\<lambda>s. P (ksDomainTime s)"
+  (ignore: filterM setObject getObject
+     simp: filterM_mapM crunch_simps
+       wp: crunch_wps)
+
+crunch ksDomainTime_inv[wp]: createNewObjects "\<lambda>s. P (ksDomainTime s)"
+  (simp: crunch_simps zipWithM_x_mapM
+   wp: crunch_wps hoare_unless_wp
+   ignore: getObject setObject)
+
+crunch ksDomainTime_inv[wp]: performARMMMUInvocation "\<lambda>s. P (ksDomainTime s)"
+  (ignore: getObject setObject
+   wp: crunch_wps getObject_cte_inv getASID_wp setObject_ksPSpace_only updateObject_default_inv
+   simp: unless_def)
+
+crunch ksDomainTime_inv[wp]: preemptionPoint "\<lambda>s. P (ksDomainTime s)"
+  (simp: whenE_def)
+
+crunch ksDomainTime_inv[wp]: performInvocation "\<lambda>s. P (ksDomainTime s)"
+  (wp: crunch_wps zipWithM_x_inv cteRevoke_preservation mapME_x_inv_wp
+   simp: unless_def crunch_simps filterM_mapM)
+
+crunch ksDomainTime_inv[wp]: activateThread "\<lambda>s. P (ksDomainTime s)"
+
+crunch ksDomainTime_inv[wp]:
+  receiveSignal, getNotification, receiveIPC, deleteCallerCap "\<lambda>s. P (ksDomainTime s)"
+  (wp: hoare_drop_imps simp: crunch_simps)
+
+lemma handleRecv_ksDomainTime_inv[wp]:
+  "\<lbrace>\<lambda>s. P (ksDomainTime s) \<rbrace> handleRecv e \<lbrace>\<lambda>_ s. P (ksDomainTime s) \<rbrace>"
+  unfolding handleRecv_def
+  by (rule hoare_pre)
+     (wp hoare_drop_imps | simp add: crunch_simps | wpc)+
+
+crunch ksDomainTime_inv[wp]: doUserOp "(\<lambda>s. P (ksDomainTime s))"
+  (wp: select_wp)
+
+crunch ksDomainTime_inv[wp]: getIRQState, chooseThread, handleYield "(\<lambda>s. P (ksDomainTime s))"
+
+crunch ksDomainTime_inv[wp]: handleSend, handleReply "(\<lambda>s. P (ksDomainTime s))"
+  (wp: hoare_drop_imps hv_inv' syscall_valid' throwError_wp withoutPreemption_lift
+   simp: runErrorT_def
+   ignore: setThreadState)
+
+crunch ksDomainTime_inv[wp]: handleInvocation "(\<lambda>s. P (ksDomainTime s))"
+  (wp: hoare_drop_imps hv_inv' syscall_valid' throwError_wp withoutPreemption_lift
+   simp: runErrorT_def
+   ignore: setThreadState)
+
+crunch ksDomainTime_inv[wp]: handleCall "(\<lambda>s. P (ksDomainTime s))"
+  (wp: crunch_wps setObject_ksPSpace_only updateObject_default_inv cteRevoke_preservation
+   simp: crunch_simps unless_def
+   ignore: syscall setObject loadObject getObject constOnFailure )
+
+crunch domain_time'_inv[wp]: activateThread,handleHypervisorFault "\<lambda>s. P (ksDomainTime s)"
+  (wp: hoare_drop_imps)
+
+lemma nextDomain_domain_time_left'[wp]:
+  "\<lbrace> valid_domain_list' \<rbrace>
+   nextDomain
+   \<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<rbrace>"
+   unfolding nextDomain_def Let_def
+   apply (clarsimp simp: valid_domain_list'_def dschLength_def)
+   apply (simp only: all_set_conv_all_nth)
+   apply (erule_tac x="Suc (ksDomScheduleIdx s) mod length (ksDomSchedule s)" in allE)
+   apply fastforce
+   done
+
+lemma rescheduleRequired_ksSchedulerAction[wp]:
+  "\<lbrace>\<top>\<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. ksSchedulerAction s = ChooseNewThread \<rbrace>"
+  unfolding rescheduleRequired_def
+  by (wp setSchedulerAction_direct)
+
+lemma timerTick_valid_domain_time:
+  "\<lbrace>\<lambda>s. 0 < ksDomainTime s\<rbrace>
+   timerTick
+   \<lbrace>\<lambda>_ s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread\<rbrace>"
+  apply (simp add: timerTick_def numDomains_def)
+  apply wp
+       apply (rule_tac Q="\<lambda>_ s. ksSchedulerAction s = ChooseNewThread" in hoare_strengthen_post)
+        apply (wp | clarsimp simp: if_apply_def2)+
+  done
+
+lemma handleInterrupt_valid_domain_time:
+  "\<lbrace>\<lambda>s.  0 < ksDomainTime s \<rbrace>
+   handleInterrupt i
+   \<lbrace>\<lambda>rv s.  ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread\<rbrace>"
+   apply (simp add: handleInterrupt_def)
+   apply (case_tac "maxIRQ < i"; simp)
+    subgoal by (wp hoare_false_imp) simp
+   apply (rule_tac B="\<lambda>_ s. 0 < ksDomainTime s" in hoare_seq_ext[rotated])
+    apply (rule hoare_pre, wp, simp)
+   apply (rename_tac st)
+   apply (case_tac st, simp_all)
+    (* IRQSignal : no timer tick, trivial preservation of ksDomainTime *)
+    apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s" in hoare_post_imp, clarsimp)
+    apply (rule hoare_pre, (wp | wpc)+)
+     apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s" in hoare_post_imp, clarsimp)
+     apply wp
+    (* IRQTimer : tick occurs *) (* IRQReserved : trivial *)
+    apply (wp timerTick_valid_domain_time
+          | clarsimp simp: handleReservedIRQ_def
+          | wp_once hoare_vcg_imp_lift)+
+  done
+
+lemma schedule_domain_time_left':
+  "\<lbrace> valid_domain_list' and
+     (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<rbrace>
+   ThreadDecls_H.schedule
+   \<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<rbrace>"
+  unfolding schedule_def
+  supply word_neq_0_conv[simp]
+  apply (wp | wpc)+
+      apply (rule_tac Q="\<lambda>_. valid_domain_list'" in hoare_post_imp, clarsimp)
+      apply (wp | clarsimp)+
+  done
+
+lemma handleEvent_ksDomainTime_inv:
+  "\<lbrace>\<lambda>s. P (ksDomainTime  s) \<and> e \<noteq> Interrupt \<rbrace>
+   handleEvent e
+   \<lbrace>\<lambda>_ s. P (ksDomainTime s) \<rbrace>"
+  apply (cases e, simp_all)
+      apply (rename_tac syscall)
+      apply (case_tac syscall, simp_all add: handle_send_def)
+             apply (wp hv_inv'|simp add: handleEvent_def |wpc)+
+  done
+
+lemma callKernel_domain_time_left:
+  "\<lbrace> (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) \<rbrace>
+   callKernel e
+   \<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<rbrace>"
+  including no_pre
+  unfolding callKernel_def
+  supply word_neq_0_conv[simp]
+  apply (case_tac "e = Interrupt")
+   apply (simp add: handleEvent_def)
+   apply (rule hoare_pre)
+   apply ((wp schedule_domain_time_left' handleInterrupt_valid_domain_time
+          | wpc | simp)+)[1]
+    apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s \<and> valid_domain_list' s" in hoare_post_imp)
+     apply fastforce
+    apply wp
+   apply simp
+  (* non-interrupt case; may throw but does not touch ksDomainTime in handleEvent *)
+  apply simp
+  apply ((wp schedule_domain_time_left' handleInterrupt_valid_domain_time
+          | simp add: if_apply_def2)+)[1]
+   apply (rule_tac Q="\<lambda>_ s. valid_domain_list' s \<and> 0 < ksDomainTime s" in hoare_post_imp)
+    apply fastforce
+   apply wp
+  apply simp
+  apply (rule hoare_pre)
+   apply (rule_tac Q="\<lambda>_ s. valid_domain_list' s \<and> 0 < ksDomainTime s"
+            in NonDetMonadVCG.hoare_post_impErr[rotated 2], assumption)
+    apply (wp handleEvent_ksDomainTime_inv | clarsimp)+
+  done
+
+end
+
+end

proof/refine/X64/EmptyFail.thy

@@ -0,0 +1,132 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+theory EmptyFail
+imports Bits_R
+begin
+
+(* Collect empty_fail lemmas here. naming convention is emtpy_fail_NAME.
+   Unless there is a good reason, they should all be [intro!, wp, simp] *)
+
+lemma empty_fail_projectKO [simp, intro!]:
+  "empty_fail (projectKO v)"
+  unfolding empty_fail_def projectKO_def
+  by (simp add: return_def fail_def split: option.splits)
+
+lemma empty_fail_alignCheck [intro!, wp, simp]:
+  "empty_fail (alignCheck a b)"
+  unfolding alignCheck_def
+  by (simp add: alignError_def)
+
+lemma empty_fail_magnitudeCheck [intro!, wp, simp]:
+  "empty_fail (magnitudeCheck a b c)"
+  unfolding magnitudeCheck_def
+  by (simp split: option.splits)
+
+lemma empty_fail_loadObject_default [intro!, wp, simp]:
+  shows "empty_fail (loadObject_default x b c d)"
+  by (auto simp: loadObject_default_def
+           split: option.splits)
+
+lemma empty_fail_threadGet [intro!, wp, simp]:
+  "empty_fail (threadGet f p)"
+  by (simp add: threadGet_def getObject_def split_def)
+
+lemma empty_fail_getCTE [intro!, wp, simp]:
+  "empty_fail (getCTE slot)"
+  apply (simp add: getCTE_def getObject_def split_def)
+  apply (intro empty_fail_bind, simp_all)
+  apply (simp add: loadObject_cte typeError_def alignCheck_def alignError_def
+                   magnitudeCheck_def
+            split: Structures_H.kernel_object.split)
+  apply (auto split: option.split)
+  done
+
+lemma empty_fail_updateObject_cte [intro!, wp, simp]:
+  "empty_fail (updateObject (v :: cte) ko a b c)"
+  by (simp add: updateObject_cte typeError_def unless_def split: kernel_object.splits )
+
+lemma empty_fail_setCTE [intro!, wp, simp]:
+  "empty_fail (setCTE p cte)"
+  unfolding setCTE_def
+  by (simp add: setObject_def split_def)
+
+lemma empty_fail_updateMDB [intro!, wp, simp]:
+  "empty_fail (updateMDB a b)"
+  unfolding updateMDB_def Let_def by auto
+
+lemma empty_fail_getSlotCap [intro!, wp, simp]:
+  "empty_fail (getSlotCap a)"
+  unfolding getSlotCap_def by simp
+
+context begin interpretation Arch . (*FIXME: arch_split*)
+
+lemma empty_fail_getObject:
+  assumes x: "(\<And>b c d. empty_fail (loadObject x b c d::'a :: pspace_storable kernel))"
+  shows "empty_fail (getObject x :: 'a :: pspace_storable kernel)"
+  apply (simp add: getObject_def split_def)
+  apply (safe intro!: empty_fail_bind empty_fail_gets empty_fail_assert_opt)
+  apply (rule x)
+  done
+
+lemma empty_fail_getObject_tcb [intro!, wp, simp]:
+  shows "empty_fail (getObject x :: tcb kernel)"
+  by (auto intro: empty_fail_getObject)
+
+lemma empty_fail_updateTrackedFreeIndex [intro!, wp, simp]:
+  shows "empty_fail (updateTrackedFreeIndex p idx)"
+  by (simp add: updateTrackedFreeIndex_def)
+
+lemma empty_fail_updateNewFreeIndex [intro!, wp, simp]:
+  shows "empty_fail (updateNewFreeIndex p)"
+  apply (simp add: updateNewFreeIndex_def)
+  apply (safe intro!: empty_fail_bind)
+  apply (simp split: capability.split)
+  done
+
+lemma empty_fail_insertNewCap [intro!, wp, simp]:
+  "empty_fail (insertNewCap p p' cap)"
+  unfolding insertNewCap_def by simp
+
+lemma empty_fail_getIRQSlot [intro!, wp, simp]:
+  "empty_fail (getIRQSlot irq)"
+  by (simp add: getIRQSlot_def getInterruptState_def locateSlot_conv)
+
+lemma empty_fail_getObject_ntfn [intro!, wp, simp]:
+  "empty_fail (getObject p :: Structures_H.notification kernel)"
+  by (simp add: empty_fail_getObject)
+
+lemma empty_fail_getNotification [intro!, wp, simp]:
+  "empty_fail (getNotification ep)"
+  by (simp add: getNotification_def)
+
+lemma empty_fail_lookupIPCBuffer [intro!, wp, simp]:
+  "empty_fail (lookupIPCBuffer a b)"
+  by (clarsimp simp: lookupIPCBuffer_def ARM_H.lookupIPCBuffer_def
+                     Let_def getThreadBufferSlot_def locateSlot_conv
+              split: capability.splits arch_capability.splits | wp | wpc)+
+
+lemma empty_fail_updateObject_default [intro!, wp, simp]:
+  "empty_fail (updateObject_default v ko a b c)"
+  by (simp add: updateObject_default_def typeError_def unless_def split: kernel_object.splits )
+
+lemma empty_fail_threadSet [intro!, wp, simp]:
+  "empty_fail (threadSet f p)"
+  by (simp add: threadSet_def getObject_def setObject_def split_def)
+
+lemma empty_fail_getThreadState[iff]:
+  "empty_fail (getThreadState t)"
+  by (simp add: getThreadState_def)
+
+declare empty_fail_stateAssert [wp]
+declare setRegister_empty_fail [intro!, simp]
+
+end
+end

proof/refine/X64/EmptyFail_H.thy

@@ -0,0 +1,315 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+theory EmptyFail_H
+imports Refine
+begin
+
+lemma wpc_helper_empty_fail:
+  "empty_fail f \<Longrightarrow> wpc_helper (P, P') (Q, Q') (empty_fail f)"
+  by (clarsimp simp: wpc_helper_def)
+
+wpc_setup "\<lambda>m. empty_fail m" wpc_helper_empty_fail
+
+crunch_ignore (empty_fail)
+  (add: handleE' getCTE getObject updateObject
+        CSpaceDecls_H.resolveAddressBits
+        doMachineOp
+        suspend restart
+        schedule)
+
+context begin interpretation Arch . (*FIXME: arch_split*)
+
+lemmas forM_empty_fail[intro!, wp, simp] = empty_fail_mapM[simplified forM_def[symmetric]]
+lemmas forM_x_empty_fail[intro!, wp, simp] = empty_fail_mapM_x[simplified forM_x_def[symmetric]]
+lemmas forME_x_empty_fail[intro!, wp, simp] = mapME_x_empty_fail[simplified forME_x_def[symmetric]]
+
+lemma withoutPreemption_empty_fail[intro!, wp, simp]:
+  "empty_fail m \<Longrightarrow> empty_fail (withoutPreemption m)"
+  by (simp add: withoutPreemption_def)
+
+lemma withoutFailure_empty_fail[intro!, wp, simp]:
+  "empty_fail m \<Longrightarrow> empty_fail (withoutFailure m)"
+  by (simp add: withoutFailure_def)
+
+lemma catchFailure_empty_fail[intro!, wp, simp]:
+  "\<lbrakk> empty_fail f; \<And>x. empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail (catchFailure f g)"
+  by (simp add: catchFailure_def empty_fail_catch)
+
+lemma emptyOnFailure_empty_fail[intro!, wp, simp]:
+  "empty_fail m \<Longrightarrow> empty_fail (emptyOnFailure m)"
+  by (simp add: emptyOnFailure_def empty_fail_catch)
+
+lemma rethrowFailure_empty_fail [intro!, wp, simp]:
+  "empty_fail m \<Longrightarrow> empty_fail (rethrowFailure f m)"
+  apply (simp add:rethrowFailure_def o_def)
+  apply (wp | simp)+
+  done
+
+lemma unifyFailure_empty_fail [intro!, wp, simp]:
+  "empty_fail f \<Longrightarrow> empty_fail (unifyFailure f)"
+  by (simp add: unifyFailure_def)
+
+lemma lookupErrorOnFailure_empty_fail [intro!, wp, simp]:
+  "empty_fail f \<Longrightarrow> empty_fail (lookupErrorOnFailure isSource f)"
+  by (simp add: lookupErrorOnFailure_def)
+
+lemma setObject_empty_fail [intro!, wp, simp]:
+  assumes x: "(\<And>a b c. empty_fail (updateObject v a x b c))"
+  shows "empty_fail (setObject x v)"
+  apply (simp add: setObject_def split_def)
+  apply (wp x | simp)+
+  done
+
+lemma asUser_empty_fail [intro!, wp, simp]:
+  "empty_fail f \<Longrightarrow> empty_fail (asUser t f)"
+  apply (simp add:asUser_def)
+  apply (wp | wpc | simp | simp add: empty_fail_def)+
+  done
+
+lemma capFaultOnFailure_empty_fail [intro!, wp, simp]:
+  "empty_fail m \<Longrightarrow> empty_fail (capFaultOnFailure cptr rp m)"
+  apply (simp add: capFaultOnFailure_def)
+  done
+
+crunch (empty_fail) empty_fail[intro!, wp, simp]: locateSlotCap
+
+lemma resolveAddressBits_spec_empty_fail:
+  notes spec_empty_fail_bindE'[wp_split]
+  shows
+  "spec_empty_fail (CSpace_H.resolveAddressBits a b c) s"
+proof (induct arbitrary: s rule: resolveAddressBits.induct)
+  case (1 a b c s)
+  show ?case
+    apply (simp add: resolveAddressBits.simps)
+    apply (wp | simp | wpc | intro impI conjI | rule drop_spec_empty_fail)+
+      apply (rule use_spec_empty_fail)
+      apply (rule 1 | simp add: in_monad | rule drop_spec_empty_fail | force)+
+    done
+ qed
+
+lemmas resolveAddressBits_empty_fail[intro!, wp, simp] =
+       resolveAddressBits_spec_empty_fail[THEN use_spec_empty_fail]
+
+crunch (empty_fail) empty_fail[intro!, wp, simp]: lookupIPCBuffer
+(simp:Let_def)
+
+declare ef_dmo'[intro!, wp, simp]
+
+lemma empty_fail_getObject_ep [intro!, wp, simp]:
+  "empty_fail (getObject p :: endpoint kernel)"
+  by (simp add: empty_fail_getObject)
+
+lemma getEndpoint_empty_fail [intro!, wp, simp]:
+  "empty_fail (getEndpoint ep)"
+  by (simp add: getEndpoint_def)
+
+lemma constOnFailure_empty_fail[intro!, wp, simp]:
+  "empty_fail m \<Longrightarrow> empty_fail (constOnFailure x m)"
+  by (simp add: constOnFailure_def const_def empty_fail_catch)
+
+lemma ArchRetypeDecls_H_deriveCap_empty_fail[intro!, wp, simp]:
+  "isPageTableCap y \<or> isPageDirectoryCap y \<or> isPageCap y
+   \<or> isASIDControlCap y \<or> isASIDPoolCap y
+   \<Longrightarrow> empty_fail (Arch.deriveCap x y)"
+  apply (simp add: ARM_H.deriveCap_def)
+  by auto
+
+crunch (empty_fail) empty_fail[intro!, wp, simp]: ensureNoChildren
+
+lemma deriveCap_empty_fail[intro!, wp, simp]:
+  "empty_fail (RetypeDecls_H.deriveCap slot y)"
+  apply (simp add: Retype_H.deriveCap_def)
+  apply (clarsimp simp: empty_fail_bindE)
+  apply (case_tac "capCap y")
+      apply (simp_all add: isPageTableCap_def isPageDirectoryCap_def
+                           isPageCap_def isASIDPoolCap_def isASIDControlCap_def)
+  done
+
+crunch (empty_fail) empty_fail[intro!, wp, simp]: setExtraBadge, cteInsert
+
+lemma transferCapsToSlots_empty_fail[intro!, wp, simp]:
+  "empty_fail (transferCapsToSlots ep buffer n caps slots mi)"
+  apply (induct caps arbitrary: slots n mi)
+   apply simp
+  apply (simp add: Let_def split_def
+             split del: if_split)
+  apply (simp | wp | wpc | safe)+
+  done
+
+crunch (empty_fail) empty_fail[intro!, wp, simp]: lookupTargetSlot, ensureEmptySlot, lookupSourceSlot, lookupPivotSlot
+
+lemma decodeCNodeInvocation_empty_fail[intro!, wp, simp]:
+  "empty_fail (decodeCNodeInvocation label args cap exs)"
+  apply (rule_tac label=label and args=args and exs=exs in decode_cnode_cases2)
+         apply (simp_all add: decodeCNodeInvocation_def
+                         split_def cnode_invok_case_cleanup unlessE_whenE
+                   cong: if_cong bool.case_cong list.case_cong)
+         apply (simp | wp | wpc | safe)+
+  done
+
+lemma empty_fail_getObject_ap [intro!, wp, simp]:
+  "empty_fail (getObject p :: asidpool kernel)"
+  by (simp add: empty_fail_getObject)
+
+lemma empty_fail_getObject_pde [intro!, wp, simp]:
+  "empty_fail (getObject p :: pde kernel)"
+  by (simp add: empty_fail_getObject)
+
+lemma empty_fail_getObject_pte [intro!, wp, simp]:
+  "empty_fail (getObject p :: pte kernel)"
+  by (simp add: empty_fail_getObject)
+
+crunch (empty_fail) empty_fail[intro!, wp, simp]: decodeARMMMUInvocation
+(simp: Let_def ARMMMU_improve_cases)
+
+lemma ignoreFailure_empty_fail[intro!, wp, simp]:
+  "empty_fail x \<Longrightarrow> empty_fail (ignoreFailure x)"
+  by (simp add: ignoreFailure_def empty_fail_catch)
+
+crunch (empty_fail) empty_fail[intro!, wp, simp]: cancelIPC, setThreadState, tcbSchedDequeue, setupReplyMaster, isBlocked, switchIfRequiredTo
+(simp: Let_def)
+
+crunch (empty_fail) "_H_empty_fail": "ThreadDecls_H.suspend"
+lemma ThreadDecls_H_suspend_empty_fail[intro!, wp, simp]:
+  "empty_fail (ThreadDecls_H.suspend target)"
+  by (simp add:suspend_def)
+
+lemma ThreadDecls_H_restart_empty_fail[intro!, wp, simp]:
+  "empty_fail (ThreadDecls_H.restart target)"
+  by (simp add:restart_def)
+
+crunch (empty_fail) empty_fail[intro!, wp, simp]: finaliseCap, preemptionPoint, capSwapForDelete
+(wp: empty_fail_catch simp:  Let_def ignore: cacheRangeOp)
+
+lemmas finalise_spec_empty_fail_induct = finaliseSlot'.induct[where P=
+    "\<lambda>sl exp s. spec_empty_fail (finaliseSlot' sl exp) s"]
+
+lemma spec_empty_fail_If:
+  "\<lbrakk> P \<Longrightarrow> spec_empty_fail f s; \<not> P \<Longrightarrow> spec_empty_fail g s \<rbrakk>
+   \<Longrightarrow> spec_empty_fail (if P then f else g) s"
+  by (simp split: if_split)
+
+lemma spec_empty_whenE':
+  "\<lbrakk> P \<Longrightarrow> spec_empty_fail f s \<rbrakk> \<Longrightarrow> spec_empty_fail (whenE P f) s"
+  by (simp add: whenE_def spec_empty_returnOk)
+
+lemma finaliseSlot_spec_empty_fail:
+  notes spec_empty_fail_bindE'[rotated, wp_split]
+  shows "spec_empty_fail (finaliseSlot x b) s"
+unfolding finaliseSlot_def
+proof (induct rule: finalise_spec_empty_fail_induct)
+  case (1 x b s)
+  show ?case
+  apply (subst finaliseSlot'_simps_ext)
+  apply (simp only: split_def Let_def K_bind_def fun_app_def)
+  apply (wp spec_empty_whenE' spec_empty_fail_If | wpc
+         | rule 1[unfolded Let_def K_bind_def split_def fun_app_def,
+                  simplified], (simp | intro conjI)+
+         | rule drop_spec_empty_fail | simp)+
+  done
+qed
+
+lemmas finaliseSlot_empty_fail[intro!, wp, simp] =
+       finaliseSlot_spec_empty_fail[THEN use_spec_empty_fail]
+
+lemma checkCapAt_empty_fail[intro!, wp, simp]:
+  "empty_fail action \<Longrightarrow> empty_fail (checkCapAt cap ptr action)"
+  by (simp add: checkCapAt_def)
+
+lemma assertDerived_empty_fail[intro!, wp, simp]:
+  "empty_fail f \<Longrightarrow> empty_fail (assertDerived src cap f)"
+  by (simp add: assertDerived_def)
+
+crunch (empty_fail) empty_fail[intro!, wp, simp]: cteDelete
+
+lemma liftE_empty_fail[intro!, wp, simp]:
+  "empty_fail f \<Longrightarrow> empty_fail (liftE f)"
+  by simp
+
+lemma spec_empty_fail_unlessE':
+  "\<lbrakk> \<not> P \<Longrightarrow> spec_empty_fail f s \<rbrakk> \<Longrightarrow> spec_empty_fail (unlessE P f) s"
+  by (simp add:unlessE_def spec_empty_returnOk)
+
+lemma cteRevoke_spec_empty_fail:
+  notes spec_empty_fail_bindE'[wp_split]
+  shows "spec_empty_fail (cteRevoke p) s"
+proof (induct rule: cteRevoke.induct)
+  case (1 p s)
+  show ?case
+  apply (simp add: cteRevoke.simps)
+  apply (wp spec_empty_whenE' spec_empty_fail_unlessE' | rule drop_spec_empty_fail, wp)+
+  apply (rule 1, auto simp add: in_monad)
+  done
+qed
+
+lemmas cteRevoke_empty_fail[intro!, wp, simp] =
+       cteRevoke_spec_empty_fail[THEN use_spec_empty_fail]
+
+lemma Syscall_H_syscall_empty_fail[intro!, wp, simp]:
+  "\<lbrakk>empty_fail a; \<And>x. empty_fail (b x); \<And>x. empty_fail (c x);
+    \<And>x. empty_fail (d x); \<And>x. empty_fail (e x)\<rbrakk>
+   \<Longrightarrow> empty_fail (syscall a b c d e)"
+  apply (simp add:syscall_def)
+  apply (wp | wpc | simp)+
+  done
+
+lemma catchError_empty_fail[intro!, wp, simp]:
+  "\<lbrakk> empty_fail f; \<And>x. empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail (catchError f g)"
+  by (simp add: catchError_def handle_empty_fail)
+
+lemma findM_empty_fail [intro!, wp, simp]:
+  assumes m: "\<And>x. empty_fail (f x)"
+  shows "empty_fail (findM f xs)"
+proof (induct xs)
+  case Nil
+  thus ?case by (simp add: findM_def)
+next
+  case Cons
+  from Cons
+  show ?case by (simp add: m)
+qed
+
+crunch (empty_fail) empty_fail[intro!, wp, simp]: chooseThread
+(wp: empty_fail_catch simp: const_def Let_def)
+
+crunch (empty_fail) empty_fail[intro!, wp, simp]: getDomainTime
+crunch (empty_fail) empty_fail[intro!, wp, simp]: nextDomain
+
+
+lemma ThreadDecls_H_schedule_empty_fail[intro!, wp, simp]:
+  "empty_fail schedule"
+  apply (simp add: schedule_def)
+  apply (simp | wp | wpc)+
+  done
+
+lemma empty_fail_resetTimer[wp]: "empty_fail resetTimer"
+  by (simp add: resetTimer_def)
+
+crunch (empty_fail) empty_fail: callKernel
+(wp: empty_fail_catch simp: const_def Let_def ignore: cacheRangeOp)
+
+lemma call_kernel_serial:
+  " \<lbrakk> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and
+              (\<lambda>s. scheduler_action s = resume_cur_thread)) s;
+       \<exists>s'. (s, s') \<in> state_relation \<and>
+            (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and
+              (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
+              (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s' \<rbrakk>
+    \<Longrightarrow> fst (call_kernel event s) \<noteq> {}"
+  apply (cut_tac m = "call_kernel event" in corres_underlying_serial)
+    apply (rule kernel_corres)
+   apply (rule callKernel_empty_fail)
+  apply auto
+  done
+
+end
+
+end

proof/refine/X64/IncKernelInit.thy

@@ -0,0 +1,17 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+theory IncKernelInit
+imports ADT_H Tcb_R Arch_R
+begin
+
+(* Dummy include file for kernel init *)
+
+end

proof/refine/X64/Include.thy

@@ -0,0 +1,20 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+theory Include
+imports
+  "../../../spec/abstract/Syscall_A"
+  "../../../spec/design/API_H"
+  "../../../spec/design/$L4V_ARCH/ArchIntermediate_H"
+begin
+
+no_notation bind_drop (infixl ">>" 60)
+
+end

proof/refine/X64/InitLemmas.thy

@@ -0,0 +1,32 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+(* General lemmas removed from KernelInit *)
+
+theory InitLemmas
+imports IncKernelInit
+begin
+
+declare headM_tailM_Cons[simp]
+
+declare cart_singletons[simp]
+
+declare  less_1_simp[simp]
+
+declare  is_aligned_no_overflow[simp]
+
+declare unless_True[simp]
+
+declare maybe_fail_bind_fail[simp]
+
+crunch cte_wp_at'[wp]: setPriority "cte_wp_at' P p" (simp: crunch_simps)
+crunch irq_node'[wp]: setPriority "\<lambda>s. P (irq_node' s)" (simp: crunch_simps)
+
+end

proof/refine/X64/InterruptAcc_R.thy

@@ -0,0 +1,180 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+theory InterruptAcc_R
+imports TcbAcc_R
+begin
+
+lemma get_irq_slot_corres:
+  "corres (\<lambda>sl sl'. sl' = cte_map sl) \<top> \<top> (get_irq_slot irq) (getIRQSlot irq)"
+  apply (simp add: getIRQSlot_def get_irq_slot_def locateSlot_conv
+                   liftM_def[symmetric])
+  apply (simp add: getInterruptState_def)
+  apply (clarsimp simp: state_relation_def interrupt_state_relation_def)
+  apply (simp add: cte_map_def cte_level_bits_def
+                   ucast_nat_def shiftl_t2n)
+  done
+
+crunch inv[wp]: get_irq_slot "P"
+crunch inv[wp]: getIRQSlot "P"
+
+context begin interpretation Arch . (*FIXME: arch_split*)
+
+lemma set_irq_state_corres:
+  "irq_state_relation state state' \<Longrightarrow>
+   corres dc \<top> \<top> (set_irq_state state irq) (setIRQState state' irq)"
+  apply (simp add: set_irq_state_def setIRQState_def
+                   bind_assoc[symmetric])
+  apply (subgoal_tac "(state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)")
+   apply (rule corres_guard_imp)
+     apply (rule corres_split_nor)
+        apply (rule corres_machine_op)
+        apply (rule corres_Id | simp)+
+        apply (rule no_fail_maskInterrupt)
+       apply (simp add: getInterruptState_def setInterruptState_def
+                        simpler_gets_def simpler_modify_def bind_def)
+       apply (simp add: simpler_modify_def[symmetric])
+       apply (rule corres_trivial, rule corres_modify)
+       apply (simp add: state_relation_def swp_def)
+       apply (clarsimp simp: interrupt_state_relation_def)
+      apply (wp | simp)+
+  apply (clarsimp simp: irq_state_relation_def
+                 split: irq_state.split_asm irqstate.split_asm)
+  done
+
+lemma setIRQState_invs[wp]:
+  "\<lbrace>\<lambda>s. invs' s \<and> (state \<noteq> IRQSignal \<longrightarrow> IRQHandlerCap irq \<notin> ran (cteCaps_of s)) \<and> (state \<noteq> IRQInactive \<longrightarrow> irq \<le> maxIRQ)\<rbrace>
+      setIRQState state irq
+   \<lbrace>\<lambda>rv. invs'\<rbrace>"
+  apply (simp add: setIRQState_def setInterruptState_def getInterruptState_def)
+  apply (wp dmo_maskInterrupt)
+  apply (clarsimp simp: invs'_def valid_state'_def cur_tcb'_def
+                        Invariants_H.valid_queues_def valid_queues'_def
+                        valid_idle'_def valid_irq_node'_def
+                        valid_arch_state'_def valid_global_refs'_def
+                        global_refs'_def valid_machine_state'_def
+                        if_unsafe_then_cap'_def ex_cte_cap_to'_def
+                        valid_irq_handlers'_def irq_issued'_def
+                        cteCaps_of_def valid_irq_masks'_def
+                        bitmapQ_defs valid_queues_no_bitmap_def)
+  apply (rule conjI, clarsimp)
+  apply (clarsimp simp: irqs_masked'_def ct_not_inQ_def)
+  apply (rule conjI)
+   apply fastforce
+  apply (simp add: ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
+  done
+
+lemma getIRQSlot_real_cte[wp]:
+  "\<lbrace>invs'\<rbrace> getIRQSlot irq \<lbrace>real_cte_at'\<rbrace>"
+  apply (simp add: getIRQSlot_def getInterruptState_def locateSlot_conv)
+  apply wp
+  apply (clarsimp simp: invs'_def valid_state'_def valid_irq_node'_def
+                        cte_level_bits_def ucast_nat_def)
+  done
+
+lemma getIRQSlot_cte_at[wp]:
+  "\<lbrace>invs'\<rbrace> getIRQSlot irq \<lbrace>cte_at'\<rbrace>"
+  apply (rule hoare_strengthen_post [OF getIRQSlot_real_cte])
+  apply (clarsimp simp: real_cte_at')
+  done
+
+lemma work_units_updated_state_relationI[intro!]:
+  "(s,s') \<in> state_relation \<Longrightarrow>
+   (work_units_completed_update (\<lambda>_. work_units_completed s + 1) s, s'\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s' + 1\<rparr>) \<in> state_relation"
+  apply (simp add: state_relation_def)
+  done
+
+lemma work_units_and_irq_state_state_relationI [intro!]:
+  "(s, s') \<in> state_relation \<Longrightarrow>
+   (s \<lparr> work_units_completed := n,  machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr>\<rparr>,
+    s' \<lparr> ksWorkUnitsCompleted := n, ksMachineState := ksMachineState s' \<lparr> irq_state := f (irq_state (ksMachineState s')) \<rparr>\<rparr>)
+   \<in> state_relation"
+  by (simp add: state_relation_def swp_def)
+
+lemma preemption_corres:
+  "corres (intr \<oplus> dc) \<top> \<top> preemption_point preemptionPoint"
+  apply (simp add: preemption_point_def preemptionPoint_def)
+  by (auto simp: preemption_point_def preemptionPoint_def o_def gets_def liftE_def whenE_def getActiveIRQ_def
+                 corres_underlying_def select_def bind_def get_def bindE_def select_f_def modify_def
+                 alternative_def throwError_def returnOk_def return_def lift_def doMachineOp_def split_def
+                 put_def getWorkUnits_def setWorkUnits_def modifyWorkUnits_def do_machine_op_def
+
+                 update_work_units_def wrap_ext_bool_det_ext_ext_def work_units_limit_def workUnitsLimit_def
+                 work_units_limit_reached_def OR_choiceE_def reset_work_units_def mk_ef_def
+           elim: state_relationE)
+  (* what? *)
+  (* who says our proofs are not automatic.. *)
+
+lemma preemptionPoint_inv:
+  assumes "(\<And>f s. P (ksWorkUnitsCompleted_update f s) = P s)"
+          "irq_state_independent_H P"
+  shows "\<lbrace>P\<rbrace> preemptionPoint \<lbrace>\<lambda>_. P\<rbrace>" using assms
+  apply (simp add: preemptionPoint_def setWorkUnits_def getWorkUnits_def modifyWorkUnits_def)
+  apply (wpc
+          | wp hoare_whenE_wp hoare_seq_ext [OF _ select_inv] alternative_valid hoare_drop_imps
+          | simp)+
+  done
+
+lemma invs'_wu [simp, intro!]:
+  "invs' (ksWorkUnitsCompleted_update f s) = invs' s"
+  apply (simp add: invs'_def cur_tcb'_def valid_state'_def Invariants_H.valid_queues_def
+                   valid_queues'_def valid_irq_node'_def valid_machine_state'_def
+                   ct_not_inQ_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def
+                   bitmapQ_defs valid_queues_no_bitmap_def)
+  done
+
+lemma ct_in_state'_irq_state_independent [simp, intro!]:
+  "ct_in_state' x (s\<lparr>ksMachineState := ksMachineState s
+                          \<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) =
+   ct_in_state' x s"
+  by (simp add: ct_in_state'_def irq_state_independent_H_def)+
+
+lemma ex_cte_cap_wp_to'_irq_state_independent [simp, intro!]:
+  "ex_cte_cap_wp_to' x y (s\<lparr>ksMachineState := ksMachineState s
+                          \<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) =
+   ex_cte_cap_wp_to' x y s"
+  by (simp add: ex_cte_cap_wp_to'_def irq_state_independent_H_def)+
+
+lemma ps_clear_irq_state_independent [simp, intro!]:
+  "ps_clear a b (s\<lparr>ksMachineState := ksMachineState s
+                    \<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) =
+   ps_clear a b s"
+  by (simp add: ps_clear_def)
+
+lemma invs'_irq_state_independent [simp, intro!]:
+  "invs' (s\<lparr>ksMachineState := ksMachineState s
+                 \<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) =
+   invs' s"
+  apply (clarsimp simp: irq_state_independent_H_def invs'_def valid_state'_def
+          valid_pspace'_def sch_act_wf_def
+          valid_queues_def sym_refs_def state_refs_of'_def
+          if_live_then_nonz_cap'_def if_unsafe_then_cap'_def
+          valid_idle'_def valid_global_refs'_def
+          valid_arch_state'_def valid_irq_node'_def
+          valid_irq_handlers'_def valid_irq_states'_def
+          irqs_masked'_def bitmapQ_defs valid_queues_no_bitmap_def
+          valid_queues'_def valid_pde_mappings'_def
+          pspace_domain_valid_def cur_tcb'_def
+          valid_machine_state'_def tcb_in_cur_domain'_def
+          ct_not_inQ_def ct_idle_or_in_cur_domain'_def
+          cong: if_cong option.case_cong)
+  apply (rule iffI[rotated])
+   apply (clarsimp)
+   apply (case_tac "ksSchedulerAction s", simp_all)
+  apply clarsimp
+  apply (case_tac "ksSchedulerAction s", simp_all)
+  done
+
+lemma preemptionPoint_invs [wp]:
+  "\<lbrace>invs'\<rbrace> preemptionPoint \<lbrace>\<lambda>_. invs'\<rbrace>"
+  by (wp preemptionPoint_inv | clarsimp)+
+
+end
+end

proof/refine/X64/Interrupt_R.thy

@@ -0,0 +1,901 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+(*
+   Refinement for interrupt controller operations
+*)
+
+theory Interrupt_R
+imports Ipc_R Invocations_R
+begin
+
+context Arch begin
+
+(*FIXME: arch_split: move up *)
+requalify_types
+  irqcontrol_invocation
+
+lemmas [crunch_def] = decodeIRQControlInvocation_def performIRQControl_def
+
+context begin global_naming global
+
+(*FIXME: arch_split: move up *)
+requalify_types
+  Invocations_H.irqcontrol_invocation
+
+(*FIXME: arch_split*)
+requalify_facts
+  Interrupt_H.decodeIRQControlInvocation_def
+  Interrupt_H.performIRQControl_def
+
+end
+end
+
+primrec
+  irq_handler_inv_relation :: "irq_handler_invocation \<Rightarrow> irqhandler_invocation \<Rightarrow> bool"
+where
+  "irq_handler_inv_relation (Invocations_A.ACKIrq irq) x = (x = AckIRQ irq)"
+| "irq_handler_inv_relation (Invocations_A.ClearIRQHandler irq) x = (x = ClearIRQHandler irq)"
+| "irq_handler_inv_relation (Invocations_A.SetIRQHandler irq cap ptr) x =
+       (\<exists>cap'. x = SetIRQHandler irq cap' (cte_map ptr) \<and> cap_relation cap cap')"
+
+consts
+  interrupt_control_relation :: "arch_irq_control_invocation \<Rightarrow> Arch.irqcontrol_invocation \<Rightarrow> bool"
+
+primrec
+  irq_control_inv_relation :: "irq_control_invocation \<Rightarrow> irqcontrol_invocation \<Rightarrow> bool"
+where
+  "irq_control_inv_relation (Invocations_A.IRQControl irq slot slot') x
+       = (x = IssueIRQHandler irq (cte_map slot) (cte_map slot'))"
+| "irq_control_inv_relation (Invocations_A.ArchIRQControl ivk) x
+       = (\<exists>ivk'. x = ArchIRQControl ivk' \<and> interrupt_control_relation ivk ivk')"
+
+primrec
+  irq_handler_inv_valid' :: "irqhandler_invocation \<Rightarrow> kernel_state \<Rightarrow> bool"
+where
+  "irq_handler_inv_valid' (AckIRQ irq) = (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> IRQInactive)"
+| "irq_handler_inv_valid' (ClearIRQHandler irq) = \<top>"
+| "irq_handler_inv_valid' (SetIRQHandler irq cap cte_ptr)
+     = (valid_cap' cap and valid_cap' (IRQHandlerCap irq)
+           and K (isNotificationCap cap)
+           and cte_wp_at' (badge_derived' cap \<circ> cteCap) cte_ptr
+           and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = IRQHandlerCap irq) ptr' s)
+           and ex_cte_cap_wp_to' isCNodeCap cte_ptr)"
+
+primrec
+  irq_control_inv_valid' :: "irqcontrol_invocation \<Rightarrow> kernel_state \<Rightarrow> bool"
+where
+  "irq_control_inv_valid' (ArchIRQControl ivk) = \<bottom>"
+| "irq_control_inv_valid' (IssueIRQHandler irq ptr ptr') =
+       (cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) ptr and
+        cte_wp_at' (\<lambda>cte. cteCap cte = IRQControlCap) ptr' and
+        ex_cte_cap_to' ptr and real_cte_at' ptr and
+        (Not o irq_issued' irq) and K (irq \<le> maxIRQ))"
+
+context begin interpretation Arch . (*FIXME: arch_split*)
+
+lemma data_to_bool_toBool[simp]:
+  "data_to_bool dat = toBool dat"
+  by (auto simp: data_to_bool_def toBool_def)
+
+lemma decode_irq_handler_corres:
+  "\<lbrakk> list_all2 cap_relation (map fst caps) (map fst caps');
+    list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) caps caps' \<rbrakk> \<Longrightarrow>
+   corres (ser \<oplus> irq_handler_inv_relation) invs invs'
+     (decode_irq_handler_invocation label irq caps)
+     (decodeIRQHandlerInvocation label irq caps')"
+  apply (simp add: decode_irq_handler_invocation_def decodeIRQHandlerInvocation_def
+                 split del: if_split)
+  apply (cases caps)
+   apply (simp add: returnOk_def split: invocation_label.split list.splits split del: if_split)
+  apply (clarsimp simp: list_all2_Cons1 split del: if_split)
+  apply (simp add: returnOk_def split: invocation_label.split list.splits)
+  apply (clarsimp split: cap_relation_split_asm arch_cap.split_asm simp: returnOk_def)
+  done
+
+crunch inv[wp]: decodeIRQHandlerInvocation "P"
+  (simp: crunch_simps)
+
+lemma decode_irq_handler_valid'[wp]:
+  "\<lbrace>\<lambda>s. invs' s \<and> (\<forall>cap \<in> set caps. s \<turnstile>' fst cap)
+        \<and> (\<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = IRQHandlerCap irq) ptr' s)
+        \<and> (\<forall>cap \<in> set caps. \<forall>r \<in> cte_refs' (fst cap) (irq_node' s). ex_cte_cap_to' r s)
+        \<and> (\<forall>cap \<in> set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s)
+        \<and> (\<forall>cap \<in> set caps. cte_wp_at' (badge_derived' (fst cap) \<circ> cteCap) (snd cap) s)
+        \<and> s \<turnstile>' IRQHandlerCap irq\<rbrace>
+     decodeIRQHandlerInvocation label irq caps
+   \<lbrace>irq_handler_inv_valid'\<rbrace>,-"
+  apply (simp add: decodeIRQHandlerInvocation_def Let_def split_def
+               split del: if_split)
+  apply (rule hoare_pre)
+   apply (wp | wpc | simp)+
+  apply (clarsimp simp: neq_Nil_conv isCap_simps)
+  apply (rule conjI)
+   apply (clarsimp simp: cte_wp_at_ctes_of)
+   apply (drule (1) valid_irq_handlers_ctes_ofD)
+    apply (simp add: invs'_def valid_state'_def)
+   apply (simp add: irq_issued'_def)
+  apply clarsimp
+  done
+
+lemma is_irq_active_corres:
+  "corres op = \<top> \<top> (is_irq_active irq) (isIRQActive irq)"
+  apply (simp add: is_irq_active_def isIRQActive_def get_irq_state_def
+                   getIRQState_def getInterruptState_def)
+  apply (clarsimp simp: state_relation_def interrupt_state_relation_def)
+  apply (drule_tac x=irq in spec)+
+  apply (simp add: irq_state_relation_def
+            split: irqstate.split_asm irq_state.split_asm)
+  done
+
+crunch inv: isIRQActive "P"
+
+lemma isIRQActive_wp:
+  "\<lbrace>\<lambda>s. \<forall>rv. (irq_issued' irq s \<longrightarrow> rv) \<longrightarrow> Q rv s\<rbrace> isIRQActive irq \<lbrace>Q\<rbrace>"
+  apply (simp add: isIRQActive_def getIRQState_def
+                   getInterruptState_def)
+  apply wp
+  apply (clarsimp simp: irq_issued'_def)
+  done
+
+lemma whenE_rangeCheck_eq:
+  "(rangeCheck (x :: 'a :: {linorder, integral}) y z) =
+    (whenE (x < fromIntegral y \<or> fromIntegral z < x)
+      (throwError (RangeError (fromIntegral y) (fromIntegral z))))"
+  by (simp add: rangeCheck_def unlessE_whenE ucast_id linorder_not_le[symmetric])
+
+lemma decode_irq_control_corres:
+  "list_all2 cap_relation caps caps' \<Longrightarrow>
+   corres (ser \<oplus> irq_control_inv_relation)
+     (invs and (\<lambda>s. \<forall>cp \<in> set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp \<in> set caps'. s \<turnstile>' cp))
+     (decode_irq_control_invocation label args slot caps)
+     (decodeIRQControlInvocation label args (cte_map slot) caps')"
+  apply (clarsimp simp: decode_irq_control_invocation_def decodeIRQControlInvocation_def
+                        arch_check_irq_def ARM_H.checkIRQ_def
+                        ARM_H.decodeIRQControlInvocation_def arch_decode_irq_control_invocation_def
+             split del: if_split cong: if_cong
+                 split: invocation_label.split)
+
+  apply (cases caps, simp split: list.split)
+  apply (case_tac "\<exists>n. length args = Suc (Suc (Suc n))")
+   apply (clarsimp simp: list_all2_Cons1 Let_def split_def liftE_bindE
+                         whenE_rangeCheck_eq length_Suc_conv checkIRQ_def)
+   apply (rule corres_guard_imp)
+     apply (rule whenE_throwError_corres)
+       apply (simp add: minIRQ_def maxIRQ_def)
+      apply (simp add: minIRQ_def ucast_nat_def)
+     apply (simp add: linorder_not_less)
+     apply (simp add: maxIRQ_def word_le_nat_alt)
+     apply (simp add: ucast_nat_def)
+     apply (rule corres_split_eqr [OF _ is_irq_active_corres])
+       apply (rule whenE_throwError_corres, simp, simp)
+       apply (rule corres_splitEE [OF _ lsfc_corres])
+           apply (rule corres_splitEE [OF _ ensure_empty_corres])
+              apply (rule corres_trivial, clarsimp simp: returnOk_def)
+             apply clarsimp
+            apply (wp isIRQActive_inv | simp only: simp_thms | wp_once hoare_drop_imps)+
+    apply fastforce
+   apply fastforce
+  apply (subgoal_tac "length args \<le> 2", clarsimp split: list.split)
+  apply arith
+  done
+
+crunch inv[wp]: "InterruptDecls_H.decodeIRQControlInvocation"  "P"
+  (simp: crunch_simps)
+
+
+(* Levity: added (20090201 10:50:27) *)
+declare ensureEmptySlot_stronger [wp]
+
+lemma lsfco_real_cte_at'[wp]:
+  "\<lbrace>valid_objs' and valid_cap' croot\<rbrace>
+     lookupSlotForCNodeOp is_src croot ptr depth
+   \<lbrace>\<lambda>rv s. real_cte_at' rv s\<rbrace>,-"
+  apply (simp add: lookupSlotForCNodeOp_def split_def unlessE_def
+                   whenE_def
+               split del: if_split
+             cong: if_cong list.case_cong capability.case_cong)
+  apply (rule hoare_pre)
+   apply (wp resolveAddressBits_real_cte_at'
+            | simp
+            | wpc | wp_once hoare_drop_imps)+
+  done
+
+lemma decode_irq_control_valid'[wp]:
+  "\<lbrace>\<lambda>s. invs' s \<and> (\<forall>cap \<in> set caps. s \<turnstile>' cap)
+        \<and> (\<forall>cap \<in> set caps. \<forall>r \<in> cte_refs' cap (irq_node' s). ex_cte_cap_to' r s)
+        \<and> cte_wp_at' (\<lambda>cte. cteCap cte = IRQControlCap) slot s\<rbrace>
+     decodeIRQControlInvocation label args slot caps
+   \<lbrace>irq_control_inv_valid'\<rbrace>,-"
+  apply (simp add: decodeIRQControlInvocation_def Let_def split_def checkIRQ_def
+                   rangeCheck_def unlessE_whenE
+                split del: if_split cong: if_cong list.case_cong
+                                          invocation_label.case_cong)
+  apply (rule hoare_pre)
+   apply (wp ensureEmptySlot_stronger isIRQActive_wp
+             whenE_throwError_wp
+                | simp add: ARM_H.decodeIRQControlInvocation_def | wpc
+                | wp_once hoare_drop_imps)+
+  apply (clarsimp simp: minIRQ_def maxIRQ_def word_le_nat_alt unat_of_nat)
+  done
+
+lemma irq_nodes_global_refs:
+  "irq_node' s + (ucast (irq:: 10 word)) * 0x10 \<in> global_refs' s"
+  by (simp add: global_refs'_def mult.commute mult.left_commute)
+
+lemma valid_globals_ex_cte_cap_irq:
+  "\<lbrakk> ex_cte_cap_wp_to' isCNodeCap ptr s; valid_global_refs' s;
+         valid_objs' s \<rbrakk>
+       \<Longrightarrow> ptr \<noteq> intStateIRQNode (ksInterruptState s) + 2 ^ cte_level_bits * ucast (irq :: 10 word)"
+  apply (clarsimp simp: cte_wp_at_ctes_of ex_cte_cap_wp_to'_def)
+  apply (drule(1) ctes_of_valid'[rotated])
+  apply (drule(1) valid_global_refsD')
+  apply (drule subsetD[rotated], erule cte_refs_capRange)
+   apply (clarsimp simp: isCap_simps)
+  apply (subgoal_tac "irq_node' s + 2 ^ cte_level_bits * ucast irq \<in> global_refs' s")
+   apply blast
+  apply (simp add: global_refs'_def cte_level_bits_def
+    mult.commute mult.left_commute)
+  done
+
+lemma invoke_irq_handler_corres:
+  "irq_handler_inv_relation i i' \<Longrightarrow>
+   corres dc (einvs and irq_handler_inv_valid i)
+             (invs' and irq_handler_inv_valid' i')
+     (invoke_irq_handler i)
+     (invokeIRQHandler i')"
+  apply (cases i, simp_all add: invokeIRQHandler_def)
+    apply (rule corres_guard_imp, rule corres_machine_op)
+      apply (rule corres_Id, simp_all)
+    apply (rule no_fail_maskInterrupt)
+   apply (rename_tac word cap prod)
+   apply clarsimp
+   apply (rule corres_guard_imp)
+     apply (rule corres_split [OF _ get_irq_slot_corres])
+       apply simp
+       apply (rule corres_split_nor [OF _ cap_delete_one_corres])
+         apply (rule cins_corres, simp+)
+        apply (rule_tac Q="\<lambda>rv s. einvs s \<and> cte_wp_at (\<lambda>c. c = cap.NullCap) irq_slot s
+                                  \<and> (a, b) \<noteq> irq_slot
+                                  \<and> cte_wp_at (is_derived (cdt s) (a, b) cap) (a, b) s"
+                      in hoare_post_imp)
+         apply fastforce
+        apply (wp cap_delete_one_still_derived)+
+       apply (strengthen invs_mdb_strengthen')
+       apply wp+
+      apply (simp add: conj_comms eq_commute)
+      apply (wp get_irq_slot_different hoare_drop_imps)+
+    apply (clarsimp simp: valid_state_def invs_def)
+    apply (erule cte_wp_at_weakenE, simp add: is_derived_use_interrupt)
+   apply fastforce
+  apply (rule corres_guard_imp)
+    apply (rule corres_split [OF _ get_irq_slot_corres])
+      apply simp
+      apply (rule cap_delete_one_corres)
+     apply wp+
+   apply simp+
+  done
+
+lemma ntfn_badge_derived_enough_strg:
+  "cte_wp_at' (\<lambda>cte. isNotificationCap cap \<and> badge_derived' cap (cteCap cte)) ptr s
+        \<longrightarrow> cte_wp_at' (is_derived' ctes ptr cap \<circ> cteCap) ptr s"
+  by (clarsimp simp: cte_wp_at_ctes_of isCap_simps
+                     badge_derived'_def is_derived'_def vsCapRef_def)
+
+lemma cteDeleteOne_ex_cte_cap_to'[wp]:
+  "\<lbrace>ex_cte_cap_wp_to' P p\<rbrace> cteDeleteOne ptr \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P p\<rbrace>"
+  apply (simp add: ex_cte_cap_to'_def)
+  apply (rule hoare_pre)
+   apply (rule hoare_use_eq_irq_node' [OF cteDeleteOne_irq_node'])
+   apply (wp hoare_vcg_ex_lift cteDeleteOne_cte_wp_at_preserved)
+   apply (case_tac cap, simp_all add: finaliseCap_def isCap_simps)
+  done
+
+lemma cteDeleteOne_other_cap:
+  "\<lbrace>(\<lambda>s. cte_wp_at' (P o cteCap) p s) and K (p \<noteq> p')\<rbrace>
+     cteDeleteOne p'
+   \<lbrace>\<lambda>rv s. cte_wp_at' (P o cteCap) p s\<rbrace>"
+  apply (rule hoare_gen_asm)
+  apply (simp add: tree_cte_cteCap_eq)
+  apply (wp cteDeleteOne_cteCaps_of)
+  apply simp
+  done
+
+lemma isnt_irq_handler_strg:
+  "(\<not> isIRQHandlerCap cap) \<longrightarrow> (\<forall>irq. cap = IRQHandlerCap irq \<longrightarrow> P irq)"
+  by (clarsimp simp: isCap_simps)
+
+lemma ct_in_current_domain_ksMachineState:
+  "ct_idle_or_in_cur_domain' (ksMachineState_update p s) = ct_idle_or_in_cur_domain' s"
+  apply (simp add:ct_idle_or_in_cur_domain'_def)
+  apply (simp add:tcb_in_cur_domain'_def)
+  done
+
+lemma invoke_irq_handler_invs'[wp]:
+  "\<lbrace>invs' and irq_handler_inv_valid' i\<rbrace>
+    invokeIRQHandler i \<lbrace>\<lambda>rv. invs'\<rbrace>"
+  apply (cases i, simp_all add: invokeIRQHandler_def)
+    apply (wp dmo_maskInterrupt)
+    apply (clarsimp simp add: invs'_def valid_state'_def valid_irq_masks'_def
+      valid_machine_state'_def ct_not_inQ_def
+      ct_in_current_domain_ksMachineState)
+   apply (wp cteInsert_invs)+
+   apply (strengthen ntfn_badge_derived_enough_strg isnt_irq_handler_strg)
+   apply (wp cteDeleteOne_other_cap cteDeleteOne_other_cap[unfolded o_def])
+  apply (rename_tac word1 cap word2)
+  apply (simp add: getInterruptState_def getIRQSlot_def locateSlot_conv)
+  apply wp
+  apply (rename_tac word1 cap word2 s)
+  apply (clarsimp simp: ucast_nat_def)
+  apply (drule_tac irq=word1 in valid_globals_ex_cte_cap_irq)
+    apply clarsimp+
+  apply (clarsimp simp: cte_wp_at_ctes_of ex_cte_cap_to'_def
+                        isCap_simps untyped_derived_eq_def)
+  apply (fastforce simp: cte_level_bits_def badge_derived'_def)+
+  done
+
+lemma IRQHandler_valid':
+  "(s' \<turnstile>' IRQHandlerCap irq) = (irq \<le> maxIRQ)"
+  by (simp add: valid_cap'_def capAligned_def word_bits_conv)
+
+lemma valid_mdb_interrupts'[simp]:
+  "valid_mdb' (ksInterruptState_update f s) = valid_mdb' s"
+  by (simp add: valid_mdb'_def)
+crunch valid_mdb'[wp]: setIRQState "valid_mdb'"
+crunch cte_wp_at[wp]: setIRQState "cte_wp_at' P p"
+
+lemma invoke_irq_control_corres:
+  "irq_control_inv_relation i i' \<Longrightarrow>
+   corres (intr \<oplus> dc) (einvs and irq_control_inv_valid i)
+             (invs' and irq_control_inv_valid' i')
+     (invoke_irq_control i)
+     (performIRQControl i')"
+  apply (cases i, simp_all add: performIRQControl_def)
+   apply (rule corres_guard_imp)
+     apply (rule corres_split_nor [OF _ set_irq_state_corres])
+        apply (rule cins_corres_simple)
+          apply (wp | simp add: irq_state_relation_def
+                                IRQHandler_valid IRQHandler_valid')+
+    apply (clarsimp simp: invs_def valid_state_def valid_pspace_def
+                          cte_wp_at_caps_of_state is_simple_cap_def
+                          is_cap_simps safe_parent_for_def)
+   apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def
+                         IRQHandler_valid  IRQHandler_valid' is_simple_cap'_def
+                         isCap_simps)
+   apply (clarsimp simp: safe_parent_for'_def cte_wp_at_ctes_of)
+   apply (case_tac ctea)
+   apply (clarsimp simp: isCap_simps sameRegionAs_def3)
+   apply (auto dest: valid_irq_handlers_ctes_ofD)[1]
+  apply (clarsimp simp: arch_invoke_irq_control_def ARM_H.performIRQControl_def)
+  done
+
+crunch valid_cap'[wp]: setIRQState "valid_cap' cap"
+
+lemma setIRQState_cte_cap_to'[wp]:
+  "\<lbrace>ex_cte_cap_to' p\<rbrace> setIRQState st irq \<lbrace>\<lambda>_. ex_cte_cap_to' p\<rbrace>"
+  apply (simp add: setIRQState_def doMachineOp_def
+                   split_def setInterruptState_def getInterruptState_def)
+  apply wp
+  apply (clarsimp simp: ex_cte_cap_to'_def)
+  done
+
+lemma setIRQState_issued[wp]:
+  "\<lbrace>K (st = IRQSignal)\<rbrace> setIRQState st irq \<lbrace>\<lambda>rv. irq_issued' irq\<rbrace>"
+  apply (simp add: setIRQState_def irq_issued'_def setInterruptState_def
+                   getInterruptState_def)
+  apply wp
+  apply clarsimp
+  done
+
+lemma invoke_irq_control_invs'[wp]:
+  "\<lbrace>invs' and irq_control_inv_valid' i\<rbrace> performIRQControl i \<lbrace>\<lambda>rv. invs'\<rbrace>"
+  apply (cases i, simp_all add: performIRQControl_def)
+  apply (rule hoare_pre)
+   apply (wp cteInsert_simple_invs | simp add: cte_wp_at_ctes_of)+
+  apply (clarsimp simp: cte_wp_at_ctes_of IRQHandler_valid'
+                        is_simple_cap'_def isCap_simps
+                        safe_parent_for'_def sameRegionAs_def3)
+  apply (case_tac ctea)
+  apply (auto dest: valid_irq_handlers_ctes_ofD
+              simp: invs'_def valid_state'_def)
+  done
+
+lemma get_irq_state_corres:
+  "corres irq_state_relation \<top> \<top>
+       (get_irq_state irq) (getIRQState irq)"
+  apply (simp add: get_irq_state_def getIRQState_def getInterruptState_def)
+  apply (clarsimp simp: state_relation_def interrupt_state_relation_def)
+  done
+
+lemma getIRQState_prop:
+  "\<lbrace>\<lambda>s. P (intStateIRQTable (ksInterruptState s) irq)\<rbrace>
+     getIRQState irq
+   \<lbrace>\<lambda>rv s. P rv\<rbrace>"
+  apply (simp add: getIRQState_def getInterruptState_def)
+  apply wp
+  apply simp
+  done
+
+lemma num_domains[simp]:
+  "num_domains = numDomains"
+  apply(simp add: num_domains_def numDomains_def)
+  done
+
+lemma dec_domain_time_corres:
+  "corres dc \<top> \<top> dec_domain_time decDomainTime"
+  apply (simp add:dec_domain_time_def corres_underlying_def
+    decDomainTime_def simpler_modify_def)
+  apply (clarsimp simp:state_relation_def)
+  done
+
+lemma weak_sch_act_wf_updateDomainTime[simp]:
+  "weak_sch_act_wf m (s\<lparr>ksDomainTime := t\<rparr>)
+   = weak_sch_act_wf m s"
+  by (simp add:weak_sch_act_wf_def tcb_in_cur_domain'_def )
+
+lemma tcbSchedAppend_valid_objs':
+  "\<lbrace>valid_objs'\<rbrace>tcbSchedAppend t \<lbrace>\<lambda>r. valid_objs'\<rbrace>"
+  apply (simp add:tcbSchedAppend_def)
+  apply (wp hoare_unless_wp
+    threadSet_valid_objs' threadGet_wp
+    | simp add:valid_tcb_tcbQueued)+
+  apply (clarsimp simp add:obj_at'_def typ_at'_def)
+  done
+
+lemma tcbSchedAppend_sch_act_wf:
+  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> tcbSchedAppend thread
+  \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
+  apply (simp add:tcbSchedAppend_def bitmap_fun_defs)
+  apply (wp hoare_unless_wp setQueue_sch_act threadGet_wp|simp)+
+  apply (fastforce simp:typ_at'_def obj_at'_def)
+  done
+
+lemma valid_tcb_tcbTimeSlice_update[simp]:
+  "valid_tcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) s = valid_tcb' tcb s"
+  by (simp add:valid_tcb'_def tcb_cte_cases_def)
+
+lemma thread_state_case_if:
+ "(case state of Structures_A.thread_state.Running \<Rightarrow> f | _ \<Rightarrow> g) =
+  (if state = Structures_A.thread_state.Running then f else g)"
+  by (case_tac state,auto)
+
+lemma threadState_case_if:
+ "(case state of Structures_H.thread_state.Running \<Rightarrow> f | _ \<Rightarrow> g) =
+  (if state = Structures_H.thread_state.Running then f else g)"
+  by (case_tac state,auto)
+
+lemma tcbSchedAppend_invs_but_ct_not_inQ':
+  "\<lbrace>invs' and st_tcb_at' runnable' t \<rbrace>
+   tcbSchedAppend t \<lbrace>\<lambda>_. all_invs_but_ct_not_inQ'\<rbrace>"
+  apply (simp add: invs'_def valid_state'_def)
+  apply (rule hoare_pre)
+   apply (wp sch_act_wf_lift valid_irq_node_lift irqs_masked_lift
+             valid_irq_handlers_lift' cur_tcb_lift ct_idle_or_in_cur_domain'_lift2
+             untyped_ranges_zero_lift
+        | simp add: cteCaps_of_def o_def
+        | fastforce elim!: st_tcb_ex_cap'' split: thread_state.split_asm)+
+  done
+
+lemma timerTick_corres:
+  "corres dc (cur_tcb and valid_sched)
+             invs'
+             timer_tick timerTick"
+  apply (simp add: timerTick_def timer_tick_def)
+  apply (simp add:thread_state_case_if threadState_case_if)
+  apply (rule_tac Q="\<top> and (cur_tcb and valid_sched)" and Q'="\<top> and invs'" in corres_guard_imp)
+  apply (rule corres_guard_imp)
+  apply (rule corres_split [OF _ gct_corres])
+      apply simp
+      apply (rule corres_split [OF _ gts_corres])
+        apply (rename_tac state state')
+        apply (rule corres_split[where r' = dc ])
+           apply simp
+           apply (rule corres_when,simp)
+           apply (rule corres_split[OF _ dec_domain_time_corres])
+             apply (rule corres_split[OF _ domain_time_corres])
+               apply (rule corres_when,simp)
+               apply (rule rescheduleRequired_corres)
+              apply (wp hoare_drop_imp)+
+            apply (simp add:dec_domain_time_def)
+            apply wp+
+           apply (simp add:decDomainTime_def)
+          apply wp
+          apply (rule corres_if[where Q = \<top> and Q' = \<top>])
+            apply (case_tac state,simp_all)[1]
+          apply (simp add: Let_def)
+          apply (rule_tac r'="op =" in corres_split [OF _ ethreadget_corres])
+             apply (rename_tac ts ts')
+             apply (rule_tac R="1 < ts" in corres_cases)
+              apply (simp)
+              apply (unfold thread_set_time_slice_def)
+              apply (fold dc_def)
+              apply (rule ethread_set_corres, simp+)
+              apply (clarsimp simp: etcb_relation_def)
+             apply simp
+             apply (rule corres_split [OF _ ethread_set_corres])
+                      apply (rule corres_split [OF _ tcbSchedAppend_corres])
+                        apply (fold dc_def)
+                        apply (rule rescheduleRequired_corres)
+                       apply (wp)[1]
+                      apply (rule hoare_strengthen_post)
+                       apply (wp tcbSchedAppend_invs_but_ct_not_inQ', clarsimp simp: sch_act_wf_weak)
+                     apply (simp add: sch_act_wf_weak etcb_relation_def
+                       time_slice_def timeSlice_def pred_conj_def)+
+                 apply (wp threadSet_timeslice_invs threadSet_valid_queues
+                           threadSet_valid_queues' threadSet_pred_tcb_at_state)+
+               apply (simp add:etcb_relation_def)
+              apply (wp threadSet_timeslice_invs threadSet_valid_queues
+                        threadSet_valid_queues' threadSet_pred_tcb_at_state)
+             apply simp
+            apply (wp|wpc|unfold Let_def|simp)+
+            apply (wp static_imp_wp threadSet_timeslice_invs threadSet_valid_queues  threadSet_valid_queues'
+               threadSet_pred_tcb_at_state threadSet_weak_sch_act_wf tcbSchedAppend_valid_objs'
+               rescheduleRequired_weak_sch_act_wf tcbSchedAppend_valid_queues| simp)+
+            apply (strengthen sch_act_wf_weak)
+            apply (clarsimp simp:conj_comms)
+            apply (wp tcbSchedAppend_valid_queues tcbSchedAppend_sch_act_wf)
+           apply simp
+           apply (wp threadSet_valid_queues threadSet_pred_tcb_at_state threadSet_sch_act
+            threadSet_tcbDomain_triv threadSet_valid_queues' threadSet_valid_objs'| simp)+
+         apply (wp threadGet_wp gts_wp gts_wp')+
+       apply (clarsimp simp: cur_tcb_def tcb_at_is_etcb_at valid_sched_def valid_sched_action_def)
+       apply (subgoal_tac "is_etcb_at thread s \<and> tcb_at thread s \<and> valid_etcbs s \<and> weak_valid_sched_action s")
+        prefer 2
+        apply assumption
+       apply clarsimp
+      apply (wp gts_wp')+
+     apply (clarsimp simp add:cur_tcb_def valid_sched_def
+         valid_sched_action_def valid_etcbs_def is_tcb_def
+         is_etcb_at_def st_tcb_at_def obj_at_def
+         dest!:get_tcb_SomeD)
+     apply (simp split:Structures_A.kernel_object.splits)
+     apply (drule_tac x = "cur_thread s" in spec)
+     apply clarsimp
+    apply (clarsimp simp: invs'_def valid_state'_def
+    sch_act_wf_weak
+    cur_tcb'_def inQ_def
+    ct_in_state'_def obj_at'_def)
+    apply (clarsimp simp:st_tcb_at'_def
+       valid_idle'_def ct_idle_or_in_cur_domain'_def
+       obj_at'_def projectKO_eq)
+   apply simp
+  apply simp
+  done
+
+lemmas corres_eq_trivial = corres_Id[where f = h and g = h for h, simplified]
+thm corres_Id
+
+lemma handle_interrupt_corres:
+  "corres dc
+     (einvs) (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> IRQInactive))
+     (handle_interrupt irq) (handleInterrupt irq)"
+  (is "corres dc (einvs) ?P' ?f ?g")
+  apply (simp add: handle_interrupt_def handleInterrupt_def )
+  apply (rule conjI[rotated]; rule impI)
+
+  apply (rule corres_guard_imp)
+    apply (rule corres_split [OF _ get_irq_state_corres,
+                              where R="\<lambda>rv. einvs"
+                                and R'="\<lambda>rv. invs' and (\<lambda>s. rv \<noteq> IRQInactive)"])
+      defer
+      apply (wp getIRQState_prop getIRQState_inv do_machine_op_bind doMachineOp_bind | simp add: do_machine_op_bind doMachineOp_bind )+
+      apply (rule corres_guard_imp)
+apply (rule corres_split)
+    apply (rule corres_machine_op, rule corres_eq_trivial ; (simp add: dc_def no_fail_maskInterrupt no_fail_bind no_fail_ackInterrupt)+)+
+    apply ((wp | simp)+)[4]
+    apply (rule corres_gen_asm2)
+
+  apply (case_tac st, simp_all add: irq_state_relation_def split: irqstate.split_asm)
+   apply (simp add: getSlotCap_def bind_assoc)
+   apply (rule corres_guard_imp)
+     apply (rule corres_split [OF _ get_irq_slot_corres])
+       apply simp
+       apply (rule corres_split [OF _ get_cap_corres,
+                                 where R="\<lambda>rv. einvs and valid_cap rv"
+                                  and R'="\<lambda>rv. invs' and valid_cap' (cteCap rv)"])
+         apply (rule corres_split'[where r'=dc])
+            apply (case_tac xb, simp_all add: doMachineOp_return)[1]
+             apply (clarsimp simp add: when_def doMachineOp_return)
+             apply (rule corres_guard_imp, rule send_signal_corres)
+              apply (clarsimp simp: valid_cap_def valid_cap'_def do_machine_op_bind doMachineOp_bind)+
+              apply ( rule corres_split)
+              apply (rule corres_machine_op, rule corres_eq_trivial ; (simp add:  no_fail_maskInterrupt no_fail_bind no_fail_ackInterrupt)+)+
+            apply ((wp |simp)+)
+            apply clarsimp
+   apply fastforce
+   apply (rule corres_guard_imp)
+   apply (rule corres_split)
+   apply simp
+     apply (rule corres_split [OF corres_machine_op timerTick_corres])
+       apply (rule corres_eq_trivial, simp+)
+       apply (rule corres_machine_op)
+       apply (rule corres_eq_trivial, (simp add: no_fail_ackInterrupt)+)
+       apply wp+
+    apply clarsimp
+   apply clarsimp
+  done
+
+lemma invs_ChooseNewThread:
+  "invs' s \<Longrightarrow> invs' (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)"
+  by (rule invs'_update_cnt)
+
+lemma ksDomainTime_invs[simp]:
+  "invs' (a\<lparr>ksDomainTime := t\<rparr>) = invs' a"
+  by (simp add:invs'_def valid_state'_def
+    cur_tcb'_def ct_not_inQ_def ct_idle_or_in_cur_domain'_def
+    tcb_in_cur_domain'_def valid_machine_state'_def)
+
+lemma valid_machine_state'_ksDomainTime[simp]:
+  "valid_machine_state' (a\<lparr>ksDomainTime := t\<rparr>) = valid_machine_state' a"
+  by (simp add:valid_machine_state'_def)
+
+lemma cur_tcb'_ksDomainTime[simp]:
+  "cur_tcb' (a\<lparr>ksDomainTime := 0\<rparr>) = cur_tcb' a"
+  by (simp add:cur_tcb'_def)
+
+lemma ct_idle_or_in_cur_domain'_ksDomainTime[simp]:
+  "ct_idle_or_in_cur_domain' (a\<lparr>ksDomainTime := t \<rparr>) = ct_idle_or_in_cur_domain' a"
+  by (simp add:ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
+
+lemma threadSet_ksDomainTime[wp]:
+  "\<lbrace>\<lambda>s. P (ksDomainTime s)\<rbrace> threadSet f ptr \<lbrace>\<lambda>rv s. P (ksDomainTime s)\<rbrace>"
+  apply (simp add: threadSet_def setObject_def split_def)
+  apply (wp crunch_wps | simp add:updateObject_default_def)+
+  done
+
+crunch ksDomainTime[wp]: rescheduleRequired "\<lambda>s. P (ksDomainTime s)"
+(simp:tcbSchedEnqueue_def wp:hoare_unless_wp)
+
+crunch ksDomainTime[wp]: tcbSchedAppend "\<lambda>s. P (ksDomainTime s)"
+(simp:tcbSchedEnqueue_def wp:hoare_unless_wp)
+
+lemma updateTimeSlice_valid_pspace[wp]:
+  "\<lbrace>valid_pspace'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread
+  \<lbrace>\<lambda>r. valid_pspace'\<rbrace>"
+  apply (wp threadSet_valid_pspace'T)
+  apply (auto simp:tcb_cte_cases_def)
+  done
+
+lemma updateTimeSlice_sch_act_wf[wp]:
+  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<rbrace>
+   threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread
+   \<lbrace>\<lambda>r s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
+  by (wp threadSet_sch_act,simp)
+
+
+lemma updateTimeSlice_valid_queues[wp]:
+  "\<lbrace>\<lambda>s. Invariants_H.valid_queues s \<rbrace>
+   threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread
+   \<lbrace>\<lambda>r s. Invariants_H.valid_queues s\<rbrace>"
+  apply (wp threadSet_valid_queues,simp)
+  apply (clarsimp simp:obj_at'_def inQ_def)
+  done
+
+
+lemma updateTimeSlice_sym_refs[wp]:
+  "\<lbrace>\<lambda>s. sym_refs (state_refs_of' s)\<rbrace>
+   threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread
+  \<lbrace>\<lambda>r s. sym_refs (state_refs_of' s)\<rbrace>"
+  apply (simp add: threadSet_def setObject_def split_def)
+  apply (wp crunch_wps getObject_tcb_wp
+    | simp add: updateObject_default_def loadObject_default_def
+    | wpc)+
+   apply (clarsimp simp:state_refs_of'_def
+     obj_at'_def lookupAround2_known1)
+  apply (subst lookupAround2_known1)
+   apply simp
+  apply (erule_tac f1 = sym_refs in arg_cong[THEN iffD1,rotated])
+  apply (rule ext)
+  apply (subst option.sel)
+  apply (subst fst_conv)+
+  apply (clarsimp simp:projectKO_eq projectKO_opt_tcb split:Structures_H.kernel_object.splits)
+  apply (simp add:objBits_simps)
+  apply (frule_tac s' = s and
+    v' = "(KOTCB (tcbTimeSlice_update (\<lambda>_. ts') obj))" in ps_clear_updE)
+   apply simp
+  apply (clarsimp simp:fun_upd_def)
+  apply (rule set_eqI)
+  apply (rule iffI)
+   apply (clarsimp split:option.splits if_split_asm)
+   apply (intro conjI impI)
+    apply simp
+   apply clarsimp
+   apply (drule_tac s' = s and y = thread and x = x and
+    v' = "(KOTCB (tcbTimeSlice_update (\<lambda>_. ts') obj))"
+     in ps_clear_updE[rotated])
+    apply simp
+   apply (clarsimp simp:fun_upd_def)
+  apply (clarsimp split:option.splits if_split_asm)
+  apply (intro conjI impI)
+   apply simp
+  apply clarsimp
+   apply (drule_tac y = thread and x = x and s' = s and
+    v' = "KOTCB obj"
+     in ps_clear_updE)
+    apply simp
+  apply (simp add:fun_upd_def[symmetric])
+  apply (subgoal_tac "s\<lparr>ksPSpace := ksPSpace s(thread \<mapsto> KOTCB obj)\<rparr> = s")
+   apply simp
+  apply (case_tac s)
+   apply simp
+  apply (rule ext,simp)
+  done
+
+lemma updateTimeSlice_if_live_then_nonz_cap'[wp]:
+  "\<lbrace>\<lambda>s. if_live_then_nonz_cap' s\<rbrace>
+   threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread
+  \<lbrace>\<lambda>r s. if_live_then_nonz_cap' s\<rbrace>"
+  apply (wp threadSet_iflive'T)
+   apply (simp add:tcb_cte_cases_def)
+  apply (clarsimp simp:if_live_then_nonz_cap'_def
+   ko_wp_at'_def)
+  apply (intro conjI)
+   apply (clarsimp simp:obj_at'_real_def)+
+  done
+
+lemma updateTimeSlice_if_unsafe_then_cap'[wp]:
+  "\<lbrace>\<lambda>s. if_unsafe_then_cap' s\<rbrace>
+   threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread
+  \<lbrace>\<lambda>r s. if_unsafe_then_cap' s\<rbrace>"
+  apply (wp threadSet_ifunsafe'T)
+   apply (simp add:tcb_cte_cases_def)+
+  done
+
+lemma updateTimeSlice_valid_idle'[wp]:
+  "\<lbrace>\<lambda>s. valid_idle' s\<rbrace>
+   threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread
+  \<lbrace>\<lambda>r s. valid_idle' s\<rbrace>"
+  apply (wp threadSet_idle'T)
+  apply (simp add:tcb_cte_cases_def)
+  apply (clarsimp simp:valid_idle'_def)
+  done
+
+lemma updateTimeSlice_valid_global_refs'[wp]:
+  "\<lbrace>\<lambda>s. valid_global_refs' s\<rbrace>
+   threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread
+  \<lbrace>\<lambda>r s. valid_global_refs' s\<rbrace>"
+  apply (wp threadSet_idle'T)
+  apply (simp add:tcb_cte_cases_def)+
+  done
+
+lemma updateTimeSlice_valid_irq_node'[wp]:
+  "\<lbrace>\<lambda>s. valid_irq_node' (irq_node' s) s\<rbrace>
+   threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread
+  \<lbrace>\<lambda>r s. valid_irq_node' (irq_node' s) s\<rbrace>"
+  apply (rule hoare_pre)
+  apply wps
+  apply (simp add: valid_irq_node'_def
+    | wp hoare_vcg_all_lift)+
+  done
+
+lemma updateTimeSlice_irq_handlers'[wp]:
+  "\<lbrace>\<lambda>s. valid_irq_handlers' s\<rbrace>
+   threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread
+  \<lbrace>\<lambda>r s. valid_irq_handlers' s\<rbrace>"
+  apply (rule hoare_pre)
+  apply (wp threadSet_irq_handlers' |
+   simp add: tcb_cte_cases_def)+
+  done
+
+
+lemma updateTimeSlice_valid_queues'[wp]:
+  "\<lbrace>\<lambda>s. valid_queues' s \<rbrace>
+  threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread
+  \<lbrace>\<lambda>r s. valid_queues' s\<rbrace>"
+  apply (wp threadSet_valid_queues')
+  apply (auto simp:inQ_def)
+  done
+
+lemma rescheduleRequired_valid_irq_node'[wp]:
+  "\<lbrace>\<lambda>s. valid_irq_node' (irq_node' s) s\<rbrace> rescheduleRequired
+  \<lbrace>\<lambda>rv s. valid_irq_node' (irq_node' s) s \<rbrace>"
+  apply (simp add:rescheduleRequired_def valid_irq_node'_def)
+  apply (wp hoare_vcg_all_lift | wpc |simp)+
+   apply (simp add:tcbSchedEnqueue_def)
+   apply (wp hoare_unless_wp)
+   apply (wp threadSet_typ_at_lifts | wps)+
+  apply simp
+  done
+
+lemma rescheduleRequired_cur_tcb'[wp]:
+  "\<lbrace>\<lambda>s. cur_tcb' s\<rbrace> rescheduleRequired
+  \<lbrace>\<lambda>rv s. cur_tcb' s \<rbrace>"
+  apply (simp add:rescheduleRequired_def)
+  apply wp
+    apply (simp add:cur_tcb'_def)
+   apply (wp|wpc)+
+  apply simp
+  done
+
+
+lemma timerTick_invs'[wp]:
+  "\<lbrace>invs'\<rbrace> timerTick \<lbrace>\<lambda>rv. invs'\<rbrace>"
+  apply (simp add: numDomains_def timerTick_def)
+  apply (wp threadSet_invs_trivial threadSet_pred_tcb_no_state
+            rescheduleRequired_all_invs_but_ct_not_inQ
+            tcbSchedAppend_invs_but_ct_not_inQ'
+       | simp add: tcb_cte_cases_def numDomains_def invs_ChooseNewThread
+       | wpc)+
+     apply (simp add:decDomainTime_def)
+     apply wp
+    apply simp
+    apply (rule_tac Q="\<lambda>rv. invs'"
+      in hoare_post_imp)
+     apply (clarsimp simp add:invs'_def valid_state'_def)
+    apply (wp threadGet_wp threadSet_cur threadSet_timeslice_invs
+      rescheduleRequired_all_invs_but_ct_not_inQ
+      hoare_vcg_imp_lift threadSet_ct_idle_or_in_cur_domain'
+      |wpc | simp)+
+             apply (rule hoare_strengthen_post[OF tcbSchedAppend_invs_but_ct_not_inQ'])
+             apply (clarsimp simp:valid_pspace'_def sch_act_wf_weak)
+            apply wp
+           apply (wp threadSet_pred_tcb_no_state threadSet_tcbDomain_triv
+             threadSet_valid_objs' threadSet_timeslice_invs
+             | simp)+
+          apply (wp threadGet_wp)
+   apply (wp gts_wp')+
+  apply (clarsimp simp:invs'_def st_tcb_at'_def obj_at'_def
+    valid_state'_def numDomains_def)
+  done
+
+lemma resetTimer_invs'[wp]:
+  "\<lbrace>invs'\<rbrace> doMachineOp resetTimer \<lbrace>\<lambda>_. invs'\<rbrace>"
+  apply (wp dmo_invs' no_irq no_irq_resetTimer)
+  apply clarsimp
+  apply (drule_tac Q="%_ b. underlying_memory b p = underlying_memory m p"
+                in use_valid)
+    apply (simp add: resetTimer_def
+                     machine_op_lift_def machine_rest_lift_def split_def)
+    apply wp
+   apply clarsimp+
+  done
+
+lemma dmo_ackInterrupt[wp]:
+"\<lbrace>invs'\<rbrace> doMachineOp (ackInterrupt irq) \<lbrace>\<lambda>y. invs'\<rbrace>"
+  apply (wp dmo_invs' no_irq no_irq_ackInterrupt)
+  apply safe
+   apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
+          in use_valid)
+     apply ((clarsimp simp: ackInterrupt_def machine_op_lift_def
+                           machine_rest_lift_def split_def | wp)+)[3]
+  done
+
+lemma hint_invs[wp]:
+  "\<lbrace>invs'\<rbrace> handleInterrupt irq \<lbrace>\<lambda>rv. invs'\<rbrace>"
+  apply (simp add: handleInterrupt_def getSlotCap_def
+  cong: irqstate.case_cong)
+  apply (rule conjI; rule impI)
+
+   apply (wp dmo_maskInterrupt_True getCTE_wp'
+    | wpc | simp add: doMachineOp_bind )+
+    apply (rule_tac Q="\<lambda>rv. invs'" in hoare_post_imp)
+     apply (clarsimp simp: cte_wp_at_ctes_of ex_nonz_cap_to'_def)
+     apply fastforce
+    apply (wp threadSet_invs_trivial | simp add: inQ_def handleReservedIRQ_def)+
+  apply (wp hoare_post_comb_imp_conj hoare_drop_imp getIRQState_inv)
+  apply (assumption)+
+  done
+
+
+crunch st_tcb_at'[wp]: timerTick "st_tcb_at' P t"
+  (wp: threadSet_pred_tcb_no_state)
+
+lemma handleInterrupt_runnable:
+  "\<lbrace>st_tcb_at' runnable' t\<rbrace> handleInterrupt irq \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace>"
+  apply (simp add: handleInterrupt_def)
+  apply (rule conjI; rule impI)
+   apply (wp sai_st_tcb' hoare_vcg_all_lift hoare_drop_imps
+             threadSet_pred_tcb_no_state getIRQState_inv haskell_fail_wp
+          |wpc|simp add: handleReservedIRQ_def)+
+  done
+
+end
+
+end

proof/refine/X64/Invocations_R.thy

@@ -0,0 +1,28 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+theory Invocations_R
+imports Invariants_H
+begin
+context begin interpretation Arch . (*FIXME: arch_split*)
+lemma invocation_type_eq[simp]:
+  "invocationType = invocation_type"
+  apply (rule ext)
+  apply (simp add: invocationType_def invocation_type_def Let_def)
+  apply safe
+   apply (frule from_to_enum)
+   apply blast
+  apply (cut_tac x=v in maxBound_is_bound)
+  apply simp
+  done
+end
+declare resolveAddressBits.simps[simp del]
+
+end

proof/refine/X64/KernelInit_R.thy

@@ -0,0 +1,49 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+(* Kernel init refinement. Currently axiomatised.
+*)
+
+theory KernelInit_R
+imports
+  IncKernelInit
+  "../../invariant-abstract/KernelInit_AI"
+begin
+
+(* Axiomatisation of the rest of the initialisation code *)
+axiomatization where
+  init_refinement:
+  "Init_H \<subseteq> lift_state_relation state_relation `` Init_A"
+
+axiomatization where
+  ckernel_init_valid_duplicates':
+  "\<forall>((tc,s),x) \<in> Init_H. vs_valid_duplicates' (ksPSpace s)"
+
+axiomatization where
+  ckernel_init_invs:
+  "\<forall>((tc,s),x) \<in> Init_H. invs' s"
+
+axiomatization where
+  ckernel_init_sch_norm:
+  "((tc,s),x) \<in> Init_H \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread"
+
+axiomatization where
+  ckernel_init_ctr:
+  "((tc,s),x) \<in> Init_H \<Longrightarrow> ct_running' s"
+
+axiomatization where
+  ckernel_init_domain_time:
+  "((tc,s),x) \<in> Init_H \<Longrightarrow> ksDomainTime s \<noteq> 0"
+
+axiomatization where
+  ckernel_init_domain_list:
+  "((tc,s),x) \<in> Init_H \<Longrightarrow> length (ksDomSchedule s) > 0 \<and> (\<forall>(d,time) \<in> set (ksDomSchedule s). time > 0)"
+
+end

proof/refine/X64/LevityCatch.thy

@@ -0,0 +1,81 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+theory LevityCatch
+imports
+  Include
+  "../../../lib/LemmaBucket"
+begin
+
+(* Try again, clagged from Include *)
+no_notation bind_drop (infixl ">>" 60)
+
+lemma no_fail_getCurThread:
+  "no_fail \<top> getCurThread"
+  by (clarsimp simp: getCurThread_def no_fail_def gets_def
+                     bind_def return_def get_def)
+
+lemma no_fail_getSchedulerAction:
+  "no_fail \<top> getSchedulerAction"
+  by (auto simp: getSchedulerAction_def)
+
+lemma projectKO_def2:
+  "projectKO x = assert_opt (projectKO_opt x)"
+  by (simp add: assert_opt_def projectKO_def)
+
+lemma magnitudeCheck_assert:
+  "magnitudeCheck x y n = assert (case y of None \<Rightarrow> True | Some z \<Rightarrow> 1 << n \<le> z - x)"
+  apply (simp add: magnitudeCheck_def assert_def when_def
+            split: option.split)
+  apply fastforce
+  done
+context begin interpretation Arch . (*FIXME: arch_split*)
+lemmas makeObject_simps =
+  makeObject_endpoint makeObject_notification makeObject_cte
+  makeObject_tcb makeObject_user_data makeObject_pde makeObject_pte
+  makeObject_asidpool
+end
+definition
+  "diminished' cap cap' \<equiv> \<exists>R. cap = maskCapRights R cap'"
+
+lemma projectKO_inv : "\<lbrace>P\<rbrace> projectKO ko \<lbrace>\<lambda>rv. P\<rbrace>"
+  by (simp add: projectKO_def fail_def valid_def return_def
+           split: option.splits)
+
+(****** From GeneralLib *******)
+
+lemma alignCheck_assert:
+  "alignCheck ptr n = assert (is_aligned ptr n)"
+  by (simp add: is_aligned_mask alignCheck_def assert_def
+                alignError_def unless_def when_def)
+
+lemma magnitudeCheck_inv:   "\<lbrace>P\<rbrace> magnitudeCheck x y n \<lbrace>\<lambda>rv. P\<rbrace>"
+  apply (clarsimp simp add: magnitudeCheck_def split: option.splits)
+  apply (wp hoare_when_wp)
+  apply simp
+  done
+
+lemma alignCheck_inv:
+  "\<lbrace>P\<rbrace> alignCheck x n \<lbrace>\<lambda>rv. P\<rbrace>"
+  apply (simp add: alignCheck_def unless_def alignError_def)
+  apply (wp hoare_when_wp)
+  apply simp
+  done
+
+lemma updateObject_default_inv:
+  "\<lbrace>P\<rbrace> updateObject_default obj ko x y n \<lbrace>\<lambda>rv. P\<rbrace>"
+  unfolding updateObject_default_def
+  by (simp, wp magnitudeCheck_inv alignCheck_inv projectKO_inv, simp)
+context begin interpretation Arch . (*FIXME: arch_split*)
+lemma to_from_apiType [simp]: "toAPIType (fromAPIType x) = Some x"
+  by (cases x) (auto simp add: fromAPIType_def ARM_H.fromAPIType_def
+    toAPIType_def ARM_H.toAPIType_def)
+end
+end

proof/refine/X64/Machine_R.thy

@@ -0,0 +1,111 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+(*
+    Properties of machine operations.
+*)
+
+theory Machine_R
+imports Bits_R
+begin
+
+definition "irq_state_independent_H (P :: kernel_state \<Rightarrow> bool)\<equiv>
+              \<forall>(f :: nat \<Rightarrow> nat) (s :: kernel_state). P s \<longrightarrow> P (s\<lparr>ksMachineState := ksMachineState s
+                                \<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>)"
+
+lemma irq_state_independent_HI[intro!, simp]:
+  "\<lbrakk>\<And>s f. P (s\<lparr>ksMachineState := ksMachineState s
+              \<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) = P s\<rbrakk>
+   \<Longrightarrow> irq_state_independent_H P"
+  by (simp add: irq_state_independent_H_def)
+
+lemma irq_state_independent_H_conjI[intro!]:
+  "\<lbrakk>irq_state_independent_H P; irq_state_independent_H Q\<rbrakk>
+   \<Longrightarrow> irq_state_independent_H (P and Q)"
+  "\<lbrakk>irq_state_independent_H P; irq_state_independent_H Q\<rbrakk>
+   \<Longrightarrow> irq_state_independent_H (\<lambda>s. P s \<and> Q s)"
+  by (simp add: irq_state_independent_H_def)+
+
+lemma irq_state_independent_H_disjI[intro]:
+  "\<lbrakk>irq_state_independent_H P; irq_state_independent_H Q\<rbrakk>
+   \<Longrightarrow> irq_state_independent_H (P or Q)"
+  "\<lbrakk>irq_state_independent_H P; irq_state_independent_H Q\<rbrakk>
+   \<Longrightarrow> irq_state_independent_H (\<lambda>s. P s \<or> Q s)"
+  by (simp add: irq_state_independent_H_def)+
+
+context begin interpretation Arch . (*FIXME: arch_split*)
+
+lemma dmo_getirq_inv[wp]:
+  "irq_state_independent_H P \<Longrightarrow> \<lbrace>P\<rbrace> doMachineOp getActiveIRQ \<lbrace>\<lambda>rv. P\<rbrace>"
+  apply (simp add: getActiveIRQ_def doMachineOp_def split_def exec_gets
+                   select_f_select[simplified liftM_def]
+                   select_modify_comm gets_machine_state_modify)
+  apply wp
+  apply (clarsimp simp: irq_state_independent_H_def in_monad return_def split: if_splits)
+  done
+
+lemma getActiveIRQ_masked:
+  "\<lbrace>\<lambda>s. valid_irq_masks' table (irq_masks s)\<rbrace> getActiveIRQ
+  \<lbrace>\<lambda>rv s. \<forall>irq. rv = Some irq \<longrightarrow> table irq \<noteq> IRQInactive\<rbrace>"
+  apply (simp add: getActiveIRQ_def)
+  apply wp
+  apply (clarsimp simp: valid_irq_masks'_def)
+  done
+
+lemma dmo_maskInterrupt:
+  "\<lbrace>\<lambda>s. P (ksMachineState_update (irq_masks_update (\<lambda>t. t (irq := m))) s)\<rbrace>
+  doMachineOp (maskInterrupt m irq) \<lbrace>\<lambda>_. P\<rbrace>"
+  apply (simp add: doMachineOp_def split_def)
+  apply wp
+  apply (clarsimp simp: maskInterrupt_def in_monad)
+  apply (erule rsubst [where P=P])
+  apply simp
+  done
+
+lemma dmo_maskInterrupt_True:
+  "\<lbrace>invs'\<rbrace> doMachineOp (maskInterrupt True irq) \<lbrace>\<lambda>_. invs'\<rbrace>"
+  apply (wp dmo_maskInterrupt)
+  apply (clarsimp simp: invs'_def valid_state'_def)
+  apply (simp add: valid_irq_masks'_def valid_machine_state'_def
+                   ct_not_inQ_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
+  done
+
+lemma setIRQState_irq_states':
+  "\<lbrace>valid_irq_states'\<rbrace>
+      setIRQState state irq
+   \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace>"
+  apply (simp add: setIRQState_def setInterruptState_def getInterruptState_def)
+  apply (wp dmo_maskInterrupt)
+  apply (simp add: valid_irq_masks'_def)
+  done
+
+lemma getActiveIRQ_le_maxIRQ:
+  "\<lbrace>irqs_masked' and valid_irq_states'\<rbrace> doMachineOp getActiveIRQ \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace>"
+  apply (simp add: doMachineOp_def split_def)
+  apply wp
+  apply clarsimp
+  apply (drule use_valid, rule getActiveIRQ_le_maxIRQ')
+   prefer 2
+   apply simp
+  apply (simp add: irqs_masked'_def valid_irq_states'_def)
+  done
+
+(* FIXME: follows already from getActiveIRQ_le_maxIRQ *)
+lemma getActiveIRQ_neq_Some0xFF:
+  "\<lbrace>\<top>\<rbrace> doMachineOp getActiveIRQ \<lbrace>\<lambda>rv s. rv \<noteq> Some 0x3FF\<rbrace>"
+  apply (simp add: doMachineOp_def split_def)
+  apply wp
+  apply clarsimp
+  apply (drule use_valid, rule getActiveIRQ_neq_Some0xFF')
+   apply auto
+  done
+
+end
+end

proof/refine/X64/RAB_FN.thy

@@ -0,0 +1,166 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+theory RAB_FN
+
+imports
+  "CSpace1_R"
+  "../../../lib/MonadicRewrite"
+
+begin
+
+definition
+ "only_cnode_caps ctes =
+    option_map ((\<lambda>x. if isCNodeCap x then x else NullCap) o cteCap) o ctes"
+
+definition locateSlotFun_def:
+"locateSlotFun cnode offset \<equiv> cnode + 2 ^ cte_level_bits * offset"
+
+definition
+  "cnode_caps_gsCNodes cts cns
+    = (\<forall>cap \<in> ran cts. isCNodeCap cap
+    \<longrightarrow> cns (capCNodePtr cap) = Some (capCNodeBits cap))"
+
+abbreviation (input)
+  "cnode_caps_gsCNodes' s \<equiv> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)"
+
+function
+  resolveAddressBitsFn ::
+  "capability \<Rightarrow> cptr \<Rightarrow> nat \<Rightarrow> (word32 \<Rightarrow> capability option)
+    \<Rightarrow> (lookup_failure + (machine_word * nat))"
+where
+ "resolveAddressBitsFn a b c =
+(\<lambda>x0 capptr bits caps. (let nodeCap = x0 in
+  if isCNodeCap nodeCap
+  then (let
+        radixBits = capCNodeBits nodeCap;
+        guardBits = capCNodeGuardSize nodeCap;
+        levelBits = radixBits + guardBits;
+        offset = (fromCPtr capptr `~shiftR~` (bits-levelBits)) &&
+                   (mask radixBits);
+        guard = (fromCPtr capptr `~shiftR~` (bits-guardBits)) &&
+                   (mask guardBits);
+        bitsLeft = bits - levelBits;
+        slot = locateSlotFun (capCNodePtr nodeCap) offset
+    in
+      if levelBits = 0 then Inr (0, 0)
+      else if \<not> (guardBits \<le> bits \<and> guard = capCNodeGuard nodeCap)
+            then Inl $ GuardMismatch_ \<lparr>
+                guardMismatchBitsLeft= bits,
+                guardMismatchGuardFound= capCNodeGuard nodeCap,
+                guardMismatchGuardSize= guardBits \<rparr>
+      else if (levelBits > bits) then Inl $ DepthMismatch_ \<lparr>
+            depthMismatchBitsLeft= bits,
+            depthMismatchBitsFound= levelBits \<rparr>
+      else if (bitsLeft = 0)
+          then Inr (slot, 0)
+      else (case caps slot of Some NullCap
+        \<Rightarrow> Inr (slot, bitsLeft)
+      | Some nextCap
+        \<Rightarrow> resolveAddressBitsFn nextCap capptr bitsLeft caps
+      | None \<Rightarrow> Inr (0, 0))
+    )
+  else Inl InvalidRoot
+  ))
+
+a b c"
+  by auto
+
+termination
+  apply (relation "measure (snd o snd)")
+  apply (auto split: if_split_asm)
+  done
+
+declare resolveAddressBitsFn.simps[simp del]
+
+lemma isCNodeCap_capUntypedPtr_capCNodePtr:
+  "isCNodeCap c \<Longrightarrow> capUntypedPtr c = capCNodePtr c"
+  by (clarsimp simp: isCap_simps)
+
+lemma resolveAddressBitsFn_eq:
+  "monadic_rewrite F E (\<lambda>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s))
+        \<and> valid_objs' s \<and> cnode_caps_gsCNodes' s)
+    (resolveAddressBits cap capptr bits)
+    (gets (resolveAddressBitsFn cap capptr bits o only_cnode_caps o ctes_of))"
+  (is "monadic_rewrite F E (?P cap) (?f cap bits) (?g cap capptr bits)")
+proof (induct cap capptr bits rule: resolveAddressBits.induct)
+  case (1 cap cref depth)
+  note resolveAddressBits.simps[simp del] resolveAddressBitsFn.simps[simp del]
+
+  show ?case
+    apply (subst resolveAddressBits.simps, subst resolveAddressBitsFn.simps)
+    apply (simp only: Let_def haskell_assertE_def K_bind_def)
+    apply (rule monadic_rewrite_name_pre)
+    apply (rule monadic_rewrite_imp)
+     apply (rule_tac P="op = s" in monadic_rewrite_trans)
+      (* step 1, apply the induction hypothesis on the lhs *)
+      apply (rule monadic_rewrite_named_if monadic_rewrite_named_bindE
+                  monadic_rewrite_refl[THEN monadic_rewrite_imp, where f="returnOk y" for y]
+                  monadic_rewrite_refl[THEN monadic_rewrite_imp, where f="x $ y" for x y]
+                  monadic_rewrite_refl[THEN monadic_rewrite_imp, where f="assertE P" for P s]
+                  TrueI)+
+       apply (rule_tac g="case nextCap of CNodeCap a b c d
+            \<Rightarrow> ?g nextCap cref bitsLeft
+            | _ \<Rightarrow> returnOk (slot, bitsLeft)" in monadic_rewrite_imp)
+        apply (wpc | rule monadic_rewrite_refl "1.hyps"
+           | simp only: capability.case haskell_assertE_def simp_thms)+
+       apply (clarsimp simp: in_monad locateSlot_conv getSlotCap_def
+                      dest!: in_getCTE fst_stateAssertD)
+       apply (fastforce elim: cte_wp_at_weakenE')
+      apply (rule monadic_rewrite_refl[THEN monadic_rewrite_imp], simp)
+     (* step 2, split and match based on the lhs structure *)
+     apply (simp add: locateSlot_conv liftE_bindE unlessE_def whenE_def
+                      if_to_top_of_bindE assertE_def stateAssert_def bind_assoc
+                      assert_def if_to_top_of_bind getSlotCap_def
+               split del: if_split cong: if_cong)
+     apply (rule monadic_rewrite_if_lhs monadic_rewrite_symb_exec_l'[OF get_wp]
+                 empty_fail_get no_fail_get impI
+                 monadic_rewrite_refl get_wp
+       | simp add: throwError_def returnOk_def locateSlotFun_def if_not_P
+                   isCNodeCap_capUntypedPtr_capCNodePtr
+             cong: if_cong split del: if_split)+
+          apply (rule monadic_rewrite_symb_exec_l'[OF getCTE_inv _ _ _ getCTE_cte_wp_at])
+            apply simp
+           apply (rule impI, rule no_fail_getCTE)
+          apply (simp add: monadic_rewrite_def simpler_gets_def return_def returnOk_def
+                           only_cnode_caps_def cte_wp_at_ctes_of isCap_simps
+                           locateSlotFun_def isCNodeCap_capUntypedPtr_capCNodePtr
+                    split: capability.split)
+         apply (rule monadic_rewrite_name_pre[where P="\<lambda>_. False" and f=fail]
+                     monadic_rewrite_refl get_wp
+           | simp add: throwError_def returnOk_def locateSlotFun_def if_not_P
+                       isCNodeCap_capUntypedPtr_capCNodePtr
+             cong: if_cong split del: if_split)+
+  (* step 3, prove the non-failure conditions *)
+  apply (clarsimp simp: isCap_simps)
+  apply (frule(1) cte_wp_at_valid_objs_valid_cap')
+  apply (clarsimp simp: cte_level_bits_def valid_cap_simps'
+                        real_cte_at' isCap_simps)
+  apply (clarsimp simp: cte_wp_at_ctes_of only_cnode_caps_def ball_Un
+                        cnode_caps_gsCNodes_def ran_map_option o_def)
+  apply (drule bspec, rule IntI, erule ranI, simp add: isCap_simps)
+  apply (simp add: isCap_simps capAligned_def word_bits_def and_mask_less')
+  done
+qed
+
+lemma resolveAddressBitsFn_real_cte_at':
+  "resolveAddressBitsFn cap addr depth (only_cnode_caps (ctes_of s)) = Inr rv
+    \<Longrightarrow> (isCNodeCap cap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)
+    \<Longrightarrow> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)
+    \<Longrightarrow> valid_objs' s \<Longrightarrow> valid_cap' cap s
+    \<Longrightarrow> real_cte_at' (fst rv) s"
+  using monadic_rewrite_refine_validE_R[where F=False and P''=\<top>,
+    OF resolveAddressBitsFn_eq resolveAddressBits_real_cte_at']
+  apply (clarsimp simp: valid_def validE_R_def validE_def simpler_gets_def)
+  apply (cases rv, clarsimp)
+  apply metis
+  done
+
+end

proof/refine/X64/StateRelation.thy

@@ -0,0 +1,764 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+(*
+   The refinement relation between abstract and concrete states
+*)
+
+theory StateRelation
+imports Invariants_H
+begin
+
+context begin interpretation Arch . (*FIXME: arch_split*)
+definition
+  cte_map :: "cslot_ptr \<Rightarrow> word32"
+where
+ "cte_map \<equiv> \<lambda>(oref, cref). oref + (of_bl cref * 16)"
+
+definition
+  lookup_failure_map :: "ExceptionTypes_A.lookup_failure \<Rightarrow> Fault_H.lookup_failure"
+where
+ "lookup_failure_map \<equiv> \<lambda>lf. case lf of
+    ExceptionTypes_A.InvalidRoot            \<Rightarrow> Fault_H.InvalidRoot
+  | ExceptionTypes_A.MissingCapability n    \<Rightarrow> Fault_H.MissingCapability n
+  | ExceptionTypes_A.DepthMismatch n m      \<Rightarrow> Fault_H.DepthMismatch n m
+  | ExceptionTypes_A.GuardMismatch n g      \<Rightarrow> Fault_H.GuardMismatch n (of_bl g) (length g)"
+
+primrec
+  arch_fault_map :: "Machine_A.ARM_A.arch_fault \<Rightarrow> ArchFault_H.ARM_H.arch_fault"
+where
+ "arch_fault_map (Machine_A.ARM_A.VMFault ptr msg) = ArchFault_H.ARM_H.VMFault ptr msg"
+
+primrec
+  fault_map :: "ExceptionTypes_A.fault \<Rightarrow> Fault_H.fault"
+where
+  "fault_map (ExceptionTypes_A.CapFault ref bool failure) =
+   Fault_H.CapFault ref bool (lookup_failure_map failure)"
+| "fault_map (ExceptionTypes_A.ArchFault  arch_fault) =
+   Fault_H.ArchFault  (arch_fault_map arch_fault)"
+| "fault_map (ExceptionTypes_A.UnknownSyscallException n) =
+   Fault_H.UnknownSyscallException n"
+| "fault_map (ExceptionTypes_A.UserException x y) =
+   Fault_H.UserException x y"
+
+
+text {*
+  A pspace and a tree are related if every object in the pspace
+  corresponds to an object in the tree. Some abstract objects
+  like CapTables correspond to multiple concrete ones, thus we
+  have to make cuts.
+*}
+
+type_synonym obj_relation_cut = "Structures_A.kernel_object \<Rightarrow> Structures_H.kernel_object \<Rightarrow> bool"
+type_synonym obj_relation_cuts = "(word32 \<times> obj_relation_cut) set"
+
+definition
+  vmrights_map :: "rights set \<Rightarrow> vmrights"
+where
+ "vmrights_map S \<equiv> if AllowRead \<in> S
+                   then (if AllowWrite \<in> S then VMReadWrite else VMReadOnly)
+                   else VMKernelOnly"
+
+definition
+  zbits_map :: "nat option \<Rightarrow> zombie_type"
+where
+ "zbits_map N \<equiv> case N of Some n \<Rightarrow> ZombieCNode n
+                        | None \<Rightarrow> ZombieTCB"
+
+primrec
+  acap_relation :: "arch_cap \<Rightarrow> arch_capability \<Rightarrow> bool"
+where
+  "acap_relation (arch_cap.ASIDPoolCap x y) c             = (c =
+        arch_capability.ASIDPoolCap x y)"
+| "acap_relation (arch_cap.ASIDControlCap) c              = (c =
+        arch_capability.ASIDControlCap)"
+| "acap_relation (arch_cap.PageCap dev word rghts sz data) c  = (c =
+        arch_capability.PageCap dev word (vmrights_map rghts) sz data)"
+| "acap_relation (arch_cap.PageTableCap word data) c      = (c =
+        arch_capability.PageTableCap word data)"
+| "acap_relation (arch_cap.PageDirectoryCap word data) c  = (c =
+        arch_capability.PageDirectoryCap word data)"
+
+primrec
+  cap_relation :: "cap \<Rightarrow> capability \<Rightarrow> bool"
+where
+  "cap_relation Structures_A.NullCap c                    = (c =
+           Structures_H.NullCap)"
+| "cap_relation Structures_A.DomainCap c                  = (c =
+           Structures_H.DomainCap)"
+| "cap_relation (Structures_A.UntypedCap dev ref n f) c       = (c =
+           Structures_H.UntypedCap dev ref n f)"
+| "cap_relation (Structures_A.EndpointCap ref b r) c      = (c =
+           Structures_H.EndpointCap ref b (AllowSend \<in> r)
+             (AllowRecv \<in> r) (AllowGrant \<in> r))"
+| "cap_relation (Structures_A.NotificationCap ref b r) c = (c =
+           Structures_H.NotificationCap ref b (AllowSend \<in> r) (AllowRecv \<in> r))"
+| "cap_relation (Structures_A.CNodeCap ref n L) c    = (c =
+           Structures_H.CNodeCap ref n (of_bl L) (length L))"
+| "cap_relation (Structures_A.ThreadCap ref) c            = (c =
+           Structures_H.ThreadCap ref)"
+| "cap_relation (Structures_A.ReplyCap ref master) c      = (c =
+           Structures_H.ReplyCap ref master)"
+| "cap_relation (Structures_A.IRQControlCap) c            = (c =
+           Structures_H.IRQControlCap)"
+| "cap_relation (Structures_A.IRQHandlerCap irq) c        = (c =
+           Structures_H.IRQHandlerCap irq)"
+| "cap_relation (Structures_A.ArchObjectCap a) c          = (\<exists>a'.
+           acap_relation a a' \<and> c = Structures_H.ArchObjectCap a')"
+| "cap_relation (Structures_A.Zombie p b n) c             = (c =
+           Structures_H.Zombie p (zbits_map b) n)"
+
+
+definition
+  cte_relation :: "cap_ref \<Rightarrow> obj_relation_cut"
+where
+ "cte_relation y \<equiv> \<lambda>ko ko'. \<exists>sz cs cte cap. ko = CNode sz cs \<and> ko' = KOCTE cte
+                               \<and> cs y = Some cap \<and> cap_relation cap (cteCap cte)"
+
+definition
+  asid_pool_relation :: "(10 word \<rightharpoonup> word32) \<Rightarrow> asidpool \<Rightarrow> bool"
+where
+  "asid_pool_relation \<equiv> \<lambda>p p'. p = inv ASIDPool p' o ucast"
+
+definition
+  ntfn_relation :: "Structures_A.notification \<Rightarrow> Structures_H.notification \<Rightarrow> bool"
+where
+ "ntfn_relation \<equiv> \<lambda>ntfn ntfn'.
+    (case ntfn_obj ntfn of
+      Structures_A.IdleNtfn       \<Rightarrow> ntfnObj ntfn' = Structures_H.IdleNtfn
+    | Structures_A.WaitingNtfn q  \<Rightarrow> ntfnObj ntfn' = Structures_H.WaitingNtfn q
+    | Structures_A.ActiveNtfn b \<Rightarrow> ntfnObj ntfn' = Structures_H.ActiveNtfn b)
+  \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfn'"
+
+definition
+  ep_relation :: "Structures_A.endpoint \<Rightarrow> Structures_H.endpoint \<Rightarrow> bool"
+where
+ "ep_relation \<equiv> \<lambda>ep ep'. case ep of
+    Structures_A.IdleEP   \<Rightarrow> ep' = Structures_H.IdleEP
+  | Structures_A.RecvEP q \<Rightarrow> ep' = Structures_H.RecvEP q
+  | Structures_A.SendEP q \<Rightarrow> ep' = Structures_H.SendEP q"
+
+definition
+  fault_rel_optionation :: "ExceptionTypes_A.fault option \<Rightarrow> Fault_H.fault option \<Rightarrow> bool"
+where
+ "fault_rel_optionation \<equiv> \<lambda>f f'. f' = option_map fault_map f"
+
+primrec
+  thread_state_relation :: "Structures_A.thread_state \<Rightarrow> Structures_H.thread_state \<Rightarrow> bool"
+where
+  "thread_state_relation (Structures_A.Running) ts'
+     = (ts' = Structures_H.Running)"
+| "thread_state_relation (Structures_A.Restart) ts'
+     = (ts' = Structures_H.Restart)"
+| "thread_state_relation (Structures_A.Inactive) ts'
+     = (ts' = Structures_H.Inactive)"
+| "thread_state_relation (Structures_A.IdleThreadState) ts'
+     = (ts' = Structures_H.IdleThreadState)"
+| "thread_state_relation (Structures_A.BlockedOnReply) ts'
+     = (ts' = Structures_H.BlockedOnReply)"
+| "thread_state_relation (Structures_A.BlockedOnReceive oref) ts'
+     = (ts' = Structures_H.BlockedOnReceive oref)"
+| "thread_state_relation (Structures_A.BlockedOnSend oref sp) ts'
+     = (ts' = Structures_H.BlockedOnSend oref (sender_badge sp)
+                   (sender_can_grant sp) (sender_is_call sp))"
+| "thread_state_relation (Structures_A.BlockedOnNotification oref) ts'
+     = (ts' = Structures_H.BlockedOnNotification oref)"
+
+definition
+  arch_tcb_relation :: "Structures_A.arch_tcb \<Rightarrow> Structures_H.arch_tcb \<Rightarrow> bool"
+where
+ "arch_tcb_relation \<equiv> \<lambda>atcb atcb'.
+   tcb_context atcb = atcbContext atcb'"
+
+definition
+  tcb_relation :: "Structures_A.tcb \<Rightarrow> Structures_H.tcb \<Rightarrow> bool"
+where
+ "tcb_relation \<equiv> \<lambda>tcb tcb'.
+    tcb_fault_handler tcb = to_bl (tcbFaultHandler tcb')
+  \<and> tcb_ipc_buffer tcb = tcbIPCBuffer tcb'
+  \<and> arch_tcb_relation (tcb_arch tcb) (tcbArch tcb')
+  \<and> thread_state_relation (tcb_state tcb) (tcbState tcb')
+  \<and> fault_rel_optionation (tcb_fault tcb) (tcbFault tcb')
+  \<and> cap_relation (tcb_ctable tcb) (cteCap (tcbCTable tcb'))
+  \<and> cap_relation (tcb_vtable tcb) (cteCap (tcbVTable tcb'))
+  \<and> cap_relation (tcb_reply tcb) (cteCap (tcbReply tcb'))
+  \<and> cap_relation (tcb_caller tcb) (cteCap (tcbCaller tcb'))
+  \<and> cap_relation (tcb_ipcframe tcb) (cteCap (tcbIPCBufferFrame tcb'))
+  \<and> tcb_bound_notification tcb = tcbBoundNotification tcb'
+  \<and> tcb_mcpriority tcb = tcbMCP tcb'"
+
+definition
+  other_obj_relation :: "Structures_A.kernel_object \<Rightarrow> Structures_H.kernel_object \<Rightarrow> bool"
+where
+  "other_obj_relation obj obj' \<equiv>
+  (case (obj, obj') of
+        (TCB tcb, KOTCB tcb') \<Rightarrow> tcb_relation tcb tcb'
+      | (Endpoint ep, KOEndpoint ep') \<Rightarrow> ep_relation ep ep'
+      | (Notification ntfn, KONotification ntfn') \<Rightarrow> ntfn_relation ntfn ntfn'
+      | (ArchObj (ARM_A.ASIDPool pool), KOArch (KOASIDPool pool'))
+             \<Rightarrow> asid_pool_relation pool pool'
+      | _ \<Rightarrow> False)"
+
+primrec
+   pde_relation' :: "ARM_A.pde \<Rightarrow> ARM_H.pde \<Rightarrow> bool"
+where
+  "pde_relation'  ARM_A.InvalidPDE x = (x = ARM_H.InvalidPDE)"
+| "pde_relation' (ARM_A.PageTablePDE ptr atts domain) x
+      = (x = ARM_H.PageTablePDE ptr (ParityEnabled \<in> atts) domain)"
+| "pde_relation' (ARM_A.SectionPDE ptr atts domain rghts) x
+      = (x = ARM_H.SectionPDE ptr (ParityEnabled \<in> atts) domain
+               (PageCacheable \<in> atts) (Global \<in> atts) (XNever \<in> atts) (vmrights_map rghts))"
+| "pde_relation' (ARM_A.SuperSectionPDE ptr atts rghts) x
+      = (x = ARM_H.SuperSectionPDE ptr (ParityEnabled \<in> atts)
+               (PageCacheable \<in> atts) (Global \<in> atts) (XNever \<in> atts) (vmrights_map rghts))"
+
+
+primrec
+   pte_relation' :: "ARM_A.pte \<Rightarrow> ARM_H.pte \<Rightarrow> bool"
+where
+  "pte_relation'  ARM_A.InvalidPTE x = (x = ARM_H.InvalidPTE)"
+| "pte_relation' (ARM_A.LargePagePTE ptr atts rghts) x
+      = (x = ARM_H.LargePagePTE ptr (PageCacheable \<in> atts) (Global \<in> atts)
+                                         (XNever \<in> atts) (vmrights_map rghts))"
+| "pte_relation' (ARM_A.SmallPagePTE ptr atts rghts) x
+      = (x = ARM_H.SmallPagePTE ptr (PageCacheable \<in> atts) (Global \<in> atts)
+                                         (XNever \<in> atts) (vmrights_map rghts))"
+
+
+definition
+  pde_align' :: "ARM_H.pde \<Rightarrow> nat"
+where
+ "pde_align' pde \<equiv>
+  case pde of ARM_H.pde.SuperSectionPDE _ _ _ _ _ _ \<Rightarrow> 4 | _ \<Rightarrow> 0"
+
+lemmas pde_align_simps[simp] =
+  pde_align'_def[split_simps ARM_A.pde.split]
+
+definition
+  pte_align' :: "ARM_H.pte \<Rightarrow> nat"
+where
+ "pte_align' pte \<equiv> case pte of ARM_H.pte.LargePagePTE _ _ _ _ _ \<Rightarrow> 4 | _ \<Rightarrow> 0"
+
+lemmas pte_align_simps[simp] =
+  pte_align'_def[split_simps ARM_A.pte.split]
+
+definition
+  "pde_relation_aligned y pde pde' \<equiv>
+   if is_aligned y (pde_align' pde') then pde_relation' pde pde'
+   else pde = ARM_A.InvalidPDE"
+
+definition
+  "pte_relation_aligned y pte pte' \<equiv>
+   if is_aligned y (pte_align' pte') then pte_relation' pte pte'
+   else pte = ARM_A.InvalidPTE"
+
+definition
+ "pte_relation y \<equiv> \<lambda>ko ko'. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> ko' = KOArch (KOPTE pte)
+                              \<and> pte_relation_aligned y (pt y) pte"
+
+definition
+ "pde_relation y \<equiv> \<lambda>ko ko'. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> ko' = KOArch (KOPDE pde)
+                              \<and> pde_relation_aligned y (pd y) pde"
+
+primrec
+ aobj_relation_cuts :: "ARM_A.arch_kernel_obj \<Rightarrow> word32 \<Rightarrow> obj_relation_cuts"
+where
+  "aobj_relation_cuts (DataPage dev sz) x =
+      {(x + n * 2 ^ pageBits, \<lambda>_ obj. obj = (if dev then KOUserDataDevice else KOUserData) ) | n . n < 2 ^ (pageBitsForSize sz - pageBits) }"
+| "aobj_relation_cuts (ARM_A.ASIDPool pool) x =
+     {(x, other_obj_relation)}"
+| "aobj_relation_cuts (PageTable pt) x =
+     (\<lambda>y. (x + (ucast y << 2), pte_relation y)) ` UNIV"
+| "aobj_relation_cuts (PageDirectory pd) x =
+     (\<lambda>y. (x + (ucast y << 2), pde_relation y)) ` UNIV"
+
+primrec
+  obj_relation_cuts :: "Structures_A.kernel_object \<Rightarrow> word32 \<Rightarrow> obj_relation_cuts"
+where
+  "obj_relation_cuts (CNode sz cs) x =
+     (if well_formed_cnode_n sz cs
+      then {(cte_map (x, y), cte_relation y) | y. y \<in> dom cs}
+      else {(x, \<bottom>\<bottom>)})"
+| "obj_relation_cuts (TCB tcb) x = {(x, other_obj_relation)}"
+| "obj_relation_cuts (Endpoint ep) x = {(x, other_obj_relation)}"
+| "obj_relation_cuts (Notification ntfn) x = {(x, other_obj_relation)}"
+| "obj_relation_cuts (ArchObj ao) x = aobj_relation_cuts ao x"
+
+
+lemma obj_relation_cuts_def2:
+  "obj_relation_cuts ko x =
+   (case ko of CNode sz cs \<Rightarrow> if well_formed_cnode_n sz cs
+                             then {(cte_map (x, y), cte_relation y) | y. y \<in> dom cs}
+                             else {(x, \<bottom>\<bottom>)}
+             | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>y. (x + (ucast y << 2), pte_relation y))
+                                           ` (UNIV :: word8 set)
+             | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>y. (x + (ucast y << 2), pde_relation y))
+                                           ` (UNIV :: 12 word set)
+             | ArchObj (DataPage dev sz)      \<Rightarrow>
+                 {(x + n * 2 ^ pageBits,  \<lambda>_ obj. obj =(if dev then KOUserDataDevice else KOUserData)) | n . n < 2 ^ (pageBitsForSize sz - pageBits) }
+             | _ \<Rightarrow> {(x, other_obj_relation)})"
+  by (simp split: Structures_A.kernel_object.split
+                  ARM_A.arch_kernel_obj.split)
+
+lemma obj_relation_cuts_def3:
+  "obj_relation_cuts ko x =
+  (case (a_type ko) of
+     ACapTable n \<Rightarrow> {(cte_map (x, y), cte_relation y) | y. length y = n}
+   | AArch APageTable \<Rightarrow> (\<lambda>y. (x + (ucast y << 2), pte_relation y))
+                            ` (UNIV :: word8 set)
+   | AArch APageDirectory \<Rightarrow> (\<lambda>y. (x + (ucast y << 2), pde_relation y))
+                            ` (UNIV :: 12 word set)
+   | AArch (AUserData sz)  \<Rightarrow> {(x + n * 2 ^ pageBits, \<lambda>_ obj. obj = KOUserData) | n . n < 2 ^ (pageBitsForSize sz - pageBits) }
+   | AArch (ADeviceData sz)  \<Rightarrow> {(x + n * 2 ^ pageBits, \<lambda>_ obj. obj = KOUserDataDevice ) | n . n < 2 ^ (pageBitsForSize sz - pageBits) }
+   | AGarbage _ \<Rightarrow> {(x, \<bottom>\<bottom>)}
+   | _ \<Rightarrow> {(x, other_obj_relation)})"
+  apply (simp add: obj_relation_cuts_def2 a_type_def
+            split: Structures_A.kernel_object.split
+                  ARM_A.arch_kernel_obj.split)
+  apply (clarsimp simp: well_formed_cnode_n_def length_set_helper)
+  done
+
+definition
+ "is_other_obj_relation_type tp \<equiv>
+  case tp of
+     ACapTable n \<Rightarrow> False
+   | AArch APageTable \<Rightarrow> False
+   | AArch APageDirectory \<Rightarrow> False
+   | AArch (AUserData _)   \<Rightarrow> False
+   | AArch (ADeviceData _)   \<Rightarrow> False
+   | AGarbage _ \<Rightarrow> False
+   | _ \<Rightarrow> True"
+
+lemma is_other_obj_relation_type_CapTable:
+  "\<not> is_other_obj_relation_type (ACapTable n)"
+  by (simp add: is_other_obj_relation_type_def)
+
+lemma is_other_obj_relation_type_UserData:
+  "\<not> is_other_obj_relation_type (AArch (AUserData sz))"
+  unfolding is_other_obj_relation_type_def by simp
+
+lemma is_other_obj_relation_type_DeviceData:
+  "\<not> is_other_obj_relation_type (AArch (ADeviceData sz))"
+  unfolding is_other_obj_relation_type_def by simp
+
+lemma is_other_obj_relation_type:
+  "is_other_obj_relation_type (a_type ko) \<Longrightarrow>
+   obj_relation_cuts ko x = {(x, other_obj_relation)}"
+  by (simp add: obj_relation_cuts_def3 is_other_obj_relation_type_def
+         split: a_type.splits aa_type.splits)
+
+definition
+  pspace_dom :: "Structures_A.kheap \<Rightarrow> word32 set"
+where
+  "pspace_dom ps \<equiv> \<Union>x\<in>dom ps. fst ` (obj_relation_cuts (the (ps x)) x)"
+
+definition
+  pspace_relation :: "Structures_A.kheap \<Rightarrow> (word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> bool"
+where
+ "pspace_relation ab con \<equiv>
+  (pspace_dom ab = dom con) \<and>
+  (\<forall>x \<in> dom ab. \<forall>(y, P) \<in> obj_relation_cuts (the (ab x)) x.
+       P (the (ab x)) (the (con y)))"
+
+definition etcb_relation :: "etcb \<Rightarrow> Structures_H.tcb \<Rightarrow> bool"
+where
+ "etcb_relation \<equiv> \<lambda>etcb tcb'.
+    tcb_priority etcb = tcbPriority tcb'
+  \<and> tcb_time_slice etcb = tcbTimeSlice tcb'
+  \<and> tcb_domain etcb = tcbDomain tcb'"
+
+definition
+ ekheap_relation :: "(obj_ref \<Rightarrow> etcb option) \<Rightarrow> (word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> bool"
+where
+ "ekheap_relation ab con \<equiv>
+    \<forall>x \<in> dom ab. \<exists>tcb'. con x = Some (KOTCB tcb') \<and> etcb_relation (the (ab x)) tcb'"
+
+primrec
+  sched_act_relation :: "Deterministic_A.scheduler_action \<Rightarrow> Structures_H.scheduler_action \<Rightarrow> bool"
+where
+  "sched_act_relation resume_cur_thread a' = (a' = ResumeCurrentThread)" |
+  "sched_act_relation choose_new_thread a' = (a' = ChooseNewThread)" |
+  "sched_act_relation (switch_thread x) a' = (a' = SwitchToThread x)"
+
+definition
+  ready_queues_relation :: "(Deterministic_A.domain \<Rightarrow> Structures_A.priority \<Rightarrow> Deterministic_A.ready_queue)
+                         \<Rightarrow> (domain \<times> priority \<Rightarrow> KernelStateData_H.ready_queue) \<Rightarrow> bool"
+where
+  "ready_queues_relation qs qs' \<equiv> \<forall>d p. (qs d p = qs' (d, p))"
+
+definition
+  ghost_relation :: "Structures_A.kheap \<Rightarrow> (word32 \<rightharpoonup> vmpage_size) \<Rightarrow> (word32 \<rightharpoonup> nat) \<Rightarrow> bool"
+where
+  "ghost_relation h ups cns \<equiv>
+   (\<forall>a sz. (\<exists>dev. h a = Some (ArchObj (DataPage dev sz))) \<longleftrightarrow> ups a = Some sz) \<and>
+   (\<forall>a n. (\<exists>cs. h a = Some (CNode n cs) \<and> well_formed_cnode_n n cs) \<longleftrightarrow>
+          cns a = Some n)"
+
+definition
+  cdt_relation :: "(cslot_ptr \<Rightarrow> bool) \<Rightarrow> cdt \<Rightarrow> cte_heap \<Rightarrow> bool"
+where
+  "cdt_relation \<equiv> \<lambda>cte_at m m'.
+  \<forall>c. cte_at c \<longrightarrow> cte_map ` descendants_of c m = descendants_of' (cte_map c) m'"
+
+definition
+  cdt_list_relation :: "cdt_list \<Rightarrow> cdt \<Rightarrow> cte_heap \<Rightarrow> bool"
+where
+ "cdt_list_relation \<equiv> \<lambda>t m m'.
+    \<forall>c cap node. m' (cte_map c) = Some (CTE cap node)
+        \<longrightarrow> (case next_slot c t m of None \<Rightarrow> True
+            | Some next \<Rightarrow> mdbNext node = cte_map next)"
+
+definition
+  revokable_relation :: "(cslot_ptr \<Rightarrow> bool) \<Rightarrow> (cslot_ptr \<Rightarrow> cap option) \<Rightarrow> cte_heap \<Rightarrow> bool"
+where
+  "revokable_relation revo cs m' \<equiv>
+  \<forall>c cap node. cs c \<noteq> None \<longrightarrow>
+               m' (cte_map c) = Some (CTE cap node) \<longrightarrow>
+               revo c = mdbRevocable node"
+
+definition
+  irq_state_relation :: "irq_state \<Rightarrow> irqstate \<Rightarrow> bool"
+where
+  "irq_state_relation irq irq' \<equiv> case (irq, irq') of
+     (irq_state.IRQInactive, irqstate.IRQInactive) \<Rightarrow> True
+   | (irq_state.IRQSignal, irqstate.IRQSignal) \<Rightarrow> True
+   | (irq_state.IRQTimer, irqstate.IRQTimer) \<Rightarrow> True
+   | _ \<Rightarrow> False"
+
+definition
+  interrupt_state_relation :: "(irq \<Rightarrow> obj_ref) \<Rightarrow> (irq \<Rightarrow> irq_state) \<Rightarrow> interrupt_state \<Rightarrow> bool"
+where
+  "interrupt_state_relation node_map irqs is \<equiv>
+    (\<exists>node irqs'. is = InterruptState node irqs'
+              \<and> (\<forall>irq. node_map irq = node + (ucast irq << cte_level_bits))
+              \<and> (\<forall>irq. irq_state_relation (irqs irq) (irqs' irq)))"
+
+definition
+  arch_state_relation :: "(arch_state \<times> ARM_H.kernel_state) set"
+where
+  "arch_state_relation \<equiv> {(s, s') .
+         arm_asid_table s = armKSASIDTable s' o ucast
+       \<and> arm_global_pd s = armKSGlobalPD s'
+       \<and> arm_hwasid_table s = armKSHWASIDTable s'
+       \<and> arm_global_pts s = armKSGlobalPTs s'
+       \<and> arm_next_asid s = armKSNextASID s'
+       \<and> arm_asid_map s = armKSASIDMap s'
+       \<and> arm_kernel_vspace s = armKSKernelVSpace s'}"
+
+
+definition
+  (* NOTE: this map discards the Ident right, needed on endpoints only *)
+  rights_mask_map :: "rights set \<Rightarrow> Types_H.cap_rights"
+where
+ "rights_mask_map \<equiv> \<lambda>rs. CapRights (AllowWrite \<in> rs) (AllowRead \<in> rs) (AllowGrant \<in> rs)"
+
+
+lemma obj_relation_cutsE:
+  "\<lbrakk> (y, P) \<in> obj_relation_cuts ko x; P ko ko';
+     \<And>sz cs z cap cte. \<lbrakk> ko = CNode sz cs; well_formed_cnode_n sz cs; y = cte_map (x, z);
+                      ko' = KOCTE cte; cs z = Some cap; cap_relation cap (cteCap cte) \<rbrakk>
+              \<Longrightarrow> R;
+     \<And>pt (z :: word8) pte'. \<lbrakk> ko = ArchObj (PageTable pt); y = x + (ucast z << 2);
+                              ko' = KOArch (KOPTE pte'); pte_relation_aligned z (pt z) pte' \<rbrakk>
+              \<Longrightarrow> R;
+     \<And>pd (z :: 12 word) pde'. \<lbrakk> ko = ArchObj (PageDirectory pd); y = x + (ucast z << 2);
+                              ko' = KOArch (KOPDE pde'); pde_relation_aligned z (pd z) pde' \<rbrakk>
+              \<Longrightarrow> R;
+     \<And>sz dev n. \<lbrakk> ko = ArchObj (DataPage dev sz); ko' = (if dev then KOUserDataDevice else KOUserData);
+              y = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize sz - pageBits) \<rbrakk> \<Longrightarrow> R;
+            \<lbrakk> y = x; other_obj_relation ko ko'; is_other_obj_relation_type (a_type ko) \<rbrakk> \<Longrightarrow> R
+    \<rbrakk> \<Longrightarrow> R"
+  apply (simp add: obj_relation_cuts_def2 is_other_obj_relation_type_def
+                   a_type_def
+            split: Structures_A.kernel_object.split_asm if_split_asm
+                   ARM_A.arch_kernel_obj.split_asm)
+    apply ((clarsimp split: if_splits,
+                force simp: cte_relation_def pte_relation_def pde_relation_def)+)[5]
+  done
+
+lemma eq_trans_helper:
+  "\<lbrakk> x = y; P y = Q \<rbrakk> \<Longrightarrow> P x = Q"
+  by simp
+
+lemma cap_relation_case':
+  "cap_relation cap cap'
+     = (case cap of cap.ArchObjectCap arch_cap.ASIDControlCap \<Rightarrow> cap_relation cap cap'
+            | _ \<Rightarrow> cap_relation cap cap')"
+  by (simp split: cap.split arch_cap.split)
+
+schematic_goal cap_relation_case:
+  "cap_relation cap cap' = ?P"
+  apply (subst cap_relation_case')
+  apply (clarsimp cong: cap.case_cong arch_cap.case_cong)
+  apply (rule refl)
+  done
+
+lemmas cap_relation_split =
+  eq_trans_helper [where P=P, OF cap_relation_case cap.split[where P=P]] for P
+lemmas cap_relation_split_asm =
+  eq_trans_helper [where P=P, OF cap_relation_case cap.split_asm[where P=P]] for P
+
+
+
+text {* Relations on other data types that aren't stored but
+        used as intermediate values in the specs. *}
+
+primrec
+  message_info_map :: "Structures_A.message_info \<Rightarrow> Types_H.message_info"
+where
+ "message_info_map (Structures_A.MI a b c d) = (Types_H.MI a b c d)"
+
+lemma mi_map_label[simp]: "msgLabel (message_info_map mi) = mi_label mi"
+  by (cases mi, simp)
+
+primrec
+  syscall_error_map :: "ExceptionTypes_A.syscall_error \<Rightarrow> Fault_H.syscall_error"
+where
+  "syscall_error_map (ExceptionTypes_A.InvalidArgument n)     = Fault_H.InvalidArgument n"
+| "syscall_error_map (ExceptionTypes_A.InvalidCapability n)   = (Fault_H.InvalidCapability n)"
+| "syscall_error_map ExceptionTypes_A.IllegalOperation        = Fault_H.IllegalOperation"
+| "syscall_error_map (ExceptionTypes_A.RangeError n m)        = Fault_H.RangeError n m"
+| "syscall_error_map ExceptionTypes_A.AlignmentError          = Fault_H.AlignmentError"
+| "syscall_error_map (ExceptionTypes_A.FailedLookup b lf)     = Fault_H.FailedLookup b (lookup_failure_map lf)"
+| "syscall_error_map ExceptionTypes_A.TruncatedMessage        = Fault_H.TruncatedMessage"
+| "syscall_error_map ExceptionTypes_A.DeleteFirst             = Fault_H.DeleteFirst"
+| "syscall_error_map ExceptionTypes_A.RevokeFirst             = Fault_H.RevokeFirst"
+| "syscall_error_map (ExceptionTypes_A.NotEnoughMemory n)       = Fault_H.syscall_error.NotEnoughMemory n"
+
+definition
+  APIType_map :: "Structures_A.apiobject_type \<Rightarrow> ARM_H.object_type"
+where
+  "APIType_map ty \<equiv> case ty of
+                    Structures_A.Untyped \<Rightarrow> APIObjectType ArchTypes_H.Untyped
+                  | Structures_A.TCBObject \<Rightarrow> APIObjectType ArchTypes_H.TCBObject
+                  | Structures_A.EndpointObject \<Rightarrow> APIObjectType ArchTypes_H.EndpointObject
+                  | Structures_A.NotificationObject \<Rightarrow> APIObjectType ArchTypes_H.NotificationObject
+                  | Structures_A.CapTableObject \<Rightarrow> APIObjectType ArchTypes_H.CapTableObject
+                  | ArchObject ao \<Rightarrow> (case ao of
+         SmallPageObj     \<Rightarrow> SmallPageObject
+       | LargePageObj     \<Rightarrow> LargePageObject
+       | SectionObj       \<Rightarrow> SectionObject
+       | SuperSectionObj  \<Rightarrow> SuperSectionObject
+       | PageTableObj     \<Rightarrow> PageTableObject
+       | PageDirectoryObj \<Rightarrow> PageDirectoryObject)"
+
+lemma get_tcb_at: "tcb_at t s \<Longrightarrow> (\<exists>tcb. get_tcb t s = Some tcb)"
+  by (simp add: tcb_at_def)
+
+
+definition
+  state_relation :: "(det_state \<times> kernel_state) set"
+where
+ "state_relation \<equiv> {(s, s').
+         pspace_relation (kheap s) (ksPSpace s')
+       \<and> ekheap_relation (ekheap s) (ksPSpace s')
+       \<and> sched_act_relation (scheduler_action s) (ksSchedulerAction s')
+       \<and> ready_queues_relation (ready_queues s) (ksReadyQueues s')
+       \<and> ghost_relation (kheap s) (gsUserPages s') (gsCNodes s')
+       \<and> cdt_relation (swp cte_at s) (cdt s) (ctes_of s')
+       \<and> cdt_list_relation (cdt_list s) (cdt s) (ctes_of s')
+       \<and> revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s')
+       \<and> (arch_state s, ksArchState s') \<in> arch_state_relation
+       \<and> interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s')
+       \<and> (cur_thread s = ksCurThread s')
+       \<and> (idle_thread s = ksIdleThread s')
+       \<and> (machine_state s = ksMachineState s')
+       \<and> (work_units_completed s = ksWorkUnitsCompleted s')
+       \<and> (domain_index s = ksDomScheduleIdx s')
+       \<and> (domain_list s = ksDomSchedule s')
+       \<and> (cur_domain s = ksCurDomain s')
+       \<and> (domain_time s = ksDomainTime s')}"
+
+text {* Rules for using states in the relation. *}
+
+lemma curthread_relation:
+  "(a, b) \<in> state_relation \<Longrightarrow> ksCurThread b = cur_thread a"
+  by (simp add: state_relation_def)
+
+lemma workunitscompleted_relation:
+  "(a, b) \<in> state_relation \<Longrightarrow> ksWorkUnitsCompleted b = work_units_completed a"
+  by (simp add: state_relation_def)
+
+lemma state_relation_pspace_relation[elim!]:
+  "(s,s') \<in> state_relation \<Longrightarrow> pspace_relation (kheap s) (ksPSpace s')"
+  by (simp add: state_relation_def)
+
+lemma state_relation_ekheap_relation[elim!]:
+  "(s,s') \<in> state_relation \<Longrightarrow> ekheap_relation (ekheap s) (ksPSpace s')"
+  by (simp add: state_relation_def)
+
+(* intro/dest/elim for state_relation *)
+lemma state_relationI [intro?]:
+  "\<And>s s'. \<lbrakk> pspace_relation (kheap s) (ksPSpace s');
+  ekheap_relation (ekheap s) (ksPSpace s');
+  sched_act_relation (scheduler_action s) (ksSchedulerAction s');
+  ready_queues_relation (ready_queues s) (ksReadyQueues s');
+  ghost_relation (kheap s) (gsUserPages s') (gsCNodes s');
+  cdt_relation (swp cte_at s) (cdt s) (ctes_of s');
+  cdt_list_relation (cdt_list s) (cdt s) (ctes_of s');
+  revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s');
+  (arch_state s, ksArchState s') \<in> arch_state_relation;
+  interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s');
+  cur_thread s = ksCurThread s';
+  idle_thread s = ksIdleThread s';
+  machine_state s = ksMachineState s';
+  work_units_completed s = ksWorkUnitsCompleted s';
+  domain_index s = ksDomScheduleIdx s';
+  domain_list s = ksDomSchedule s';
+  cur_domain s = ksCurDomain s';
+  domain_time s = ksDomainTime s' \<rbrakk> \<Longrightarrow>
+  (s, s') \<in> state_relation"
+  unfolding state_relation_def by blast
+
+lemma state_relationD:
+  assumes sr:  "(s, s') \<in> state_relation"
+  shows "pspace_relation (kheap s) (ksPSpace s') \<and>
+  ekheap_relation (ekheap s) (ksPSpace s') \<and>
+  sched_act_relation (scheduler_action s) (ksSchedulerAction s') \<and>
+  ready_queues_relation (ready_queues s) (ksReadyQueues s') \<and>
+  ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') \<and>
+  cdt_relation (swp cte_at s) (cdt s) (ctes_of s') \<and>
+  cdt_list_relation (cdt_list s) (cdt s) (ctes_of s') \<and>
+  revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and>
+  (arch_state s, ksArchState s') \<in> arch_state_relation \<and>
+  interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s') \<and>
+  cur_thread s = ksCurThread s' \<and>
+  idle_thread s = ksIdleThread s' \<and>
+  machine_state s = ksMachineState s' \<and>
+  work_units_completed s = ksWorkUnitsCompleted s' \<and>
+  domain_index s = ksDomScheduleIdx s' \<and>
+  domain_list s = ksDomSchedule s' \<and>
+  cur_domain s = ksCurDomain s' \<and>
+  domain_time s = ksDomainTime s'"
+  using sr unfolding state_relation_def by simp
+
+lemma state_relationE [elim?]:
+  assumes sr:  "(s, s') \<in> state_relation"
+  and rl: "\<lbrakk>pspace_relation (kheap s) (ksPSpace s');
+  ekheap_relation (ekheap s) (ksPSpace s');
+  sched_act_relation (scheduler_action s) (ksSchedulerAction s');
+  ready_queues_relation (ready_queues s) (ksReadyQueues s');
+  ghost_relation (kheap s) (gsUserPages s') (gsCNodes s');
+  cdt_relation (swp cte_at s) (cdt s) (ctes_of s') \<and>
+  revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s');
+  cdt_list_relation (cdt_list s) (cdt s) (ctes_of s');
+  (arch_state s, ksArchState s') \<in> arch_state_relation;
+  interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s');
+  cur_thread s = ksCurThread s';
+  idle_thread s = ksIdleThread s';
+  machine_state s = ksMachineState s';
+  work_units_completed s = ksWorkUnitsCompleted s';
+  domain_index s = ksDomScheduleIdx s';
+  domain_list s = ksDomSchedule s';
+  cur_domain s = ksCurDomain s';
+  domain_time s = ksDomainTime s' \<rbrakk> \<Longrightarrow> R"
+  shows "R"
+  using sr by (blast intro!: rl dest: state_relationD)
+
+text {* This isn't defined for arch objects *}
+
+lemma objBits_obj_bits:
+  assumes rel: "other_obj_relation obj obj'"
+  shows   "obj_bits obj = objBitsKO obj'"
+  using rel
+  by (simp add: other_obj_relation_def objBitsKO_simps pageBits_def
+                archObjSize_def
+         split: Structures_A.kernel_object.split_asm
+                ARM_A.arch_kernel_obj.split_asm
+                Structures_H.kernel_object.split_asm
+                ARM_H.arch_kernel_object.split_asm)
+
+lemma replicate_length_cong:
+  "x = y \<Longrightarrow> replicate x n = replicate y n" by simp
+
+lemmas isCap_defs =
+  isZombie_def isArchObjectCap_def
+  isThreadCap_def isCNodeCap_def isNotificationCap_def
+  isEndpointCap_def isUntypedCap_def isNullCap_def
+  isIRQHandlerCap_def isIRQControlCap_def isReplyCap_def
+  isPageCap_def isPageTableCap_def isPageDirectoryCap_def
+  isASIDControlCap_def isASIDPoolCap_def isArchPageCap_def
+  isDomainCap_def
+
+lemma isCNodeCap_cap_map [simp]:
+  "cap_relation c c' \<Longrightarrow> isCNodeCap c' = is_cnode_cap c"
+  apply (cases c, simp_all add: isCap_defs split: sum.splits)
+   apply clarsimp+
+  done
+
+lemma isNullCap_cap_map [simp]:
+  "cap_relation c c' \<Longrightarrow> isNullCap c' = (c = cap.NullCap)"
+  apply (cases c, simp_all add: isCap_defs split: sum.splits)
+   apply clarsimp+
+  done
+
+lemma revokable_relation_eqI:
+  assumes r: "revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) m"
+  assumes c: "\<And>P p. cte_wp_at P p s'' \<Longrightarrow> cte_wp_at P p s"
+  assumes m: "\<And>p. is_original_cap s' p = is_original_cap s p"
+  shows "revokable_relation (is_original_cap s') (null_filter (caps_of_state s'')) m" using r
+  apply (clarsimp simp add: m revokable_relation_def null_filter_def)
+  apply (drule caps_of_state_cteD)
+  apply (drule c)
+  apply (simp add: cte_wp_at_caps_of_state)
+  done
+
+lemma sts_rel_idle :
+  "thread_state_relation st IdleThreadState = (st = Structures_A.IdleThreadState)"
+  by (cases st, auto)
+
+lemma pspace_relation_absD:
+  "\<lbrakk> ab x = Some y; pspace_relation ab con \<rbrakk>
+      \<Longrightarrow> \<forall>(x', P) \<in> obj_relation_cuts y x. \<exists>z. con x' = Some z \<and> P y z"
+  apply (clarsimp simp add: pspace_relation_def)
+  apply (drule bspec, erule domI)
+  apply simp
+  apply (drule(1) bspec)
+  apply (subgoal_tac "a \<in> pspace_dom ab")
+   apply clarsimp
+  apply (simp(no_asm) add: pspace_dom_def)
+  apply (rule rev_bexI, erule domI)
+  apply (simp add: image_def rev_bexI)
+  done
+
+lemma ekheap_relation_absD:
+  "\<lbrakk> ab x = Some y; ekheap_relation ab con \<rbrakk>
+      \<Longrightarrow> \<exists>tcb'. con x = Some (KOTCB tcb') \<and> etcb_relation y tcb'"
+  by (force simp add: ekheap_relation_def)
+
+lemma in_related_pspace_dom:
+  "\<lbrakk> s' x = Some y; pspace_relation s s' \<rbrakk> \<Longrightarrow> x \<in> pspace_dom s"
+  by (clarsimp simp add: pspace_relation_def)
+
+lemma pspace_dom_revE:
+  "\<lbrakk> x \<in> pspace_dom ps; \<And>ko y P. \<lbrakk> ps y = Some ko; (x, P) \<in> obj_relation_cuts ko y \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
+  by (clarsimp simp add: pspace_dom_def)
+
+lemma pspace_dom_relatedE:
+  "\<lbrakk> s' x = Some ko'; pspace_relation s s';
+     \<And>y ko P. \<lbrakk> s y = Some ko; (x, P) \<in> obj_relation_cuts ko y; P ko ko' \<rbrakk> \<Longrightarrow> R
+        \<rbrakk> \<Longrightarrow> R"
+  apply (rule pspace_dom_revE [OF in_related_pspace_dom],
+         assumption+)
+  apply (frule(1) pspace_relation_absD)
+  apply fastforce
+  done
+
+lemma ghost_relation_typ_at:
+  "ghost_relation (kheap s) ups cns \<equiv>
+   (\<forall>a sz. data_at sz a s = (ups a = Some sz)) \<and>
+   (\<forall>a n. typ_at (ACapTable n) a s = (cns a = Some n))"
+   apply (rule eq_reflection)
+   apply (clarsimp simp: ghost_relation_def typ_at_eq_kheap_obj data_at_def)
+   apply (intro conjI impI iffI allI,simp_all)
+    apply (auto elim!: allE)
+   done
+end
+end

proof/refine/X64/SubMonad_R.thy

@@ -0,0 +1,160 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+theory SubMonad_R
+imports KHeap_R EmptyFail
+begin
+
+(* SubMonadLib *)
+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
+
+interpretation submonad_doMachineOp:
+  submonad ksMachineState "(ksMachineState_update \<circ> K)" \<top> doMachineOp
+  by (rule submonad_doMachineOp)
+
+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
+
+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
+
+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
+
+
+lemma submonad_args_ksPSpace:
+  "submonad_args ksPSpace (ksPSpace_update o (\<lambda>x _. x)) \<top>"
+  by (simp add: submonad_args_def)
+
+context begin interpretation Arch . (*FIXME: arch_split*)
+definition
+  "asUser_fetch \<equiv> \<lambda>t s. case (ksPSpace s t) of
+      Some (KOTCB tcb) \<Rightarrow> (atcbContextGet o tcbArch) tcb
+    | None \<Rightarrow> undefined"
+
+definition
+  "asUser_replace \<equiv> \<lambda>t uc s.
+      let obj = case (ksPSpace s t) of
+                   Some (KOTCB tcb) \<Rightarrow> Some (KOTCB (tcb \<lparr>tcbArch := atcbContextSet uc (tcbArch tcb)\<rparr>))
+                 | obj \<Rightarrow> obj
+      in s \<lparr> ksPSpace := (ksPSpace s) (t := obj) \<rparr>"
+
+
+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, wp getObject_obj_at')
+     apply (simp add: objBits_def objBitsKO_def)+
+   apply (clarsimp simp: obj_at'_def asUser_fetch_def projectKOs atcbContextGet_def)+
+  done
+
+lemma threadSet_modify_asUser:
+  "tcb_at' t st \<Longrightarrow>
+   threadSet (\<lambda>tcb. tcb\<lparr> tcbArch := atcbContextSet uc (tcbArch tcb)\<rparr>) t st = modify (asUser_replace t uc) st"
+  apply (rule is_modify [OF _ empty_fail_threadSet no_fail_threadSet])
+   apply (clarsimp simp: threadSet_def setObject_def split_def
+                         updateObject_default_def)
+   apply wp
+   apply (rule_tac Q="\<lambda>rv. obj_at' (op = rv) t and (op = st)" in hoare_post_imp)
+    apply (clarsimp simp: asUser_replace_def Let_def obj_at'_def
+                          projectKOs fun_upd_def
+                   split: option.split kernel_object.split)
+   apply (wp getObject_obj_at' | clarsimp simp: objBits_def objBitsKO_def atcbContextSet_def)+
+  done
+
+lemma atcbContext_get_eq[simp] : "atcbContextGet (atcbContextSet x atcb) = x"
+  by(simp add: atcbContextGet_def atcbContextSet_def)
+
+lemma atcbContext_set_eq[simp] : "atcbContextSet (atcbContextGet t) t = t"
+  by (cases t, simp add: atcbContextGet_def atcbContextSet_def)
+
+
+lemma atcbContext_set_set[simp] : "atcbContextSet x (atcbContextSet y atcb) = atcbContextSet x atcb"
+  by (cases atcb ,simp add: atcbContextSet_def)
+
+lemma submonad_asUser:
+  "submonad (asUser_fetch t) (asUser_replace t) (tcb_at' t) (asUser t)"
+  apply (unfold_locales)
+      apply (clarsimp simp: asUser_fetch_def asUser_replace_def
+                            Let_def obj_at'_def projectKOs
+                     split: kernel_object.split option.split)
+     apply (clarsimp simp: asUser_replace_def Let_def
+                    split: kernel_object.split option.split)
+     apply (rename_tac tcb)
+     apply (case_tac tcb, simp)
+    apply (clarsimp simp: asUser_fetch_def asUser_replace_def Let_def
+                          fun_upd_idem
+                   split: kernel_object.splits option.splits)
+    apply (rename_tac tcb)
+    apply (case_tac tcb, simp add: map_upd_triv atcbContextSet_def)
+   apply (clarsimp simp: obj_at'_def asUser_replace_def
+                         Let_def projectKOs atcbContextSet_def
+                  split: kernel_object.splits option.splits)
+   apply (rename_tac tcb)
+   apply (case_tac tcb, simp add: objBitsKO_def ps_clear_def)
+  apply (rule ext)
+  apply (clarsimp simp: submonad_fn_def asUser_def bind_assoc split_def)
+  apply (subst threadGet_stateAssert_gets_asUser, simp add: bind_assoc, rule ext)
+  apply (rule bind_apply_cong [OF refl])+
+  apply (rule bind_apply_cong [OF threadSet_modify_asUser])
+   apply (clarsimp simp: in_monad stateAssert_def select_f_def)
+  apply (rule refl)
+  done
+
+end
+
+global_interpretation submonad_asUser:
+  submonad "asUser_fetch t" "asUser_replace t" "tcb_at' t" "asUser t"
+  by (rule submonad_asUser)
+
+lemma asUser_doMachineOp_comm:
+  "\<lbrakk> empty_fail m; empty_fail m' \<rbrakk> \<Longrightarrow>
+   do x \<leftarrow> asUser t m; y \<leftarrow> doMachineOp m'; n x y od =
+   do y \<leftarrow> doMachineOp m'; x \<leftarrow> asUser t m; n x y od"
+  apply (rule submonad_comm [OF submonad.axioms(1) [OF submonad_asUser]
+                                submonad.axioms(1) [OF submonad_doMachineOp]])
+        apply (simp add: submonad.fn_is_sm [OF submonad_asUser])
+       apply (simp add: submonad.fn_is_sm [OF submonad_doMachineOp])
+      apply (simp add: asUser_replace_def Let_def)
+     apply simp
+    apply (rule refl)
+   apply assumption+
+  done
+
+lemma doMachineOp_nosch [wp]:
+  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> doMachineOp m \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
+  apply (simp add: doMachineOp_def split_def)
+  apply (wp select_f_wp)
+  apply simp
+  done
+
+end