arch-split Refine + EmptyFail_H, add Refine toplevel, clean up small theories

proof/ROOT

@@ -35,20 +35,11 @@ session Refine in "refine" = BaseRefine +
   directories
     "$L4V_ARCH"
   theories [condition = "REFINE_QUICK_AND_DIRTY", quick_and_dirty]
-    "$L4V_ARCH/Refine"
-    "$L4V_ARCH/RAB_FN"
-    "$L4V_ARCH/EmptyFail_H"
-    "$L4V_ARCH/ArchInit_R"
+    "RefineToplevel_R"
   theories [condition = "SKIP_REFINE_PROOFS", quick_and_dirty, skip_proofs]
-    "$L4V_ARCH/Refine"
-    "$L4V_ARCH/RAB_FN"
-    "$L4V_ARCH/EmptyFail_H"
-    "$L4V_ARCH/ArchInit_R"
-  theories
-    "$L4V_ARCH/Refine"
-    "$L4V_ARCH/RAB_FN"
-    "$L4V_ARCH/EmptyFail_H"
-    "$L4V_ARCH/ArchInit_R"
+    "RefineToplevel_R"
+  theories
+    "RefineToplevel_R"
 
 (*
  * This theory is in a separate session because the proofs currently

proof/crefine/AARCH64/Fastpath_Equiv.thy

@@ -1483,20 +1483,6 @@ crunch emptySlot
   for obj_at'_tcbIPCBuffer[wp]: "obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t"
   (wp: crunch_wps)
 
-(* FIXME AARCH64: this was removed since ARM in RAB_FN.thy back in refine *)
-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
-
 (* FIXME move *)
 crunch getBoundNotification
   for (no_fail) no_fail[intro!, wp, simp]

proof/crefine/Move_C.thy

@@ -8,7 +8,7 @@
 (* Arch generic lemmas that should be moved into theory files before CRefine *)
 
 theory Move_C
-imports Refine.Refine
+imports Refine.ArchRefine
 begin
 
 lemma dumb_bool_for_all: "(\<forall>x. x) = False"

proof/crefine/base/Include_C.thy

@@ -7,7 +7,7 @@
 theory Include_C
 imports
   "CSpec.KernelInc_C"
-  "Refine.Refine"
+  "Refine.ArchRefine"
 begin
 
 end

proof/infoflow/refine/ADT_IF_Refine.thy

@@ -5,7 +5,7 @@
  *)
 
 theory ADT_IF_Refine
-imports "InfoFlow.ArchADT_IF" "Refine.EmptyFail_H"
+imports "InfoFlow.ArchADT_IF" "Refine.ArchEmptyFail_H"
 begin
 
 definition kernelEntry_if where

proof/refine/AARCH64/ArchEmptyFail_H.thy

@@ -0,0 +1,132 @@
+(*
+ * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+ * Copyright 2023, Proofcraft Pty Ltd
+ *
+ * SPDX-License-Identifier: GPL-2.0-only
+ *)
+
+theory ArchEmptyFail_H
+imports EmptyFail_H
+begin
+
+context Arch begin arch_global_naming
+
+named_theorems EmptyFail_H_assms
+
+lemma arch_deriveCap_empty_fail[EmptyFail_H_assms, intro!, wp, simp]:
+  "empty_fail (Arch.deriveCap x y)"
+  unfolding AARCH64_H.deriveCap_def
+  by (cases y, auto simp: isCap_simps cong: if_cong)
+
+lemma empty_fail_getObject_ap[intro!, wp, simp]:
+  "empty_fail (getObject p :: asidpool 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)
+
+lemma empty_fail_getObject_vcpu[intro!, wp, simp]:
+  "empty_fail (getObject p :: vcpu kernel)"
+  by (simp add: empty_fail_getObject)
+
+lemma empty_fail_lookupPTSlotFromLevel[intro!, wp, simp]:
+  "empty_fail (lookupPTSlotFromLevel level pt vPtr)"
+proof (induct level arbitrary: pt)
+  case 0
+  then show ?case by (subst lookupPTSlotFromLevel.simps, simp)
+next
+  case (Suc level)
+  then show ?case
+    by (subst lookupPTSlotFromLevel.simps) (wpsimp simp: checkPTAt_def pteAtIndex_def)
+qed
+
+(* FIXME AARCH64 this and empty_fail_pt_type_exhausted are needed to effectively crunch decodeARMMMUInvocation,
+   so should be moved much higher and then deployed to other crunches of decodeARMMMUInvocation,
+   which are hand-held at present  *)
+lemma empty_fail_arch_cap_exhausted:
+  "\<lbrakk>\<not> isFrameCap cap; \<not> isPageTableCap cap; \<not> isASIDControlCap cap; \<not> isASIDPoolCap cap;
+    \<not> isVCPUCap cap; \<not> isSGISignalCap cap; \<not> isSMCCap cap\<rbrakk>
+   \<Longrightarrow> empty_fail undefined"
+  by (cases cap; simp add: isCap_simps)
+
+(* FIXME AARCH64 move somewhere high up, see empty_fail_arch_cap_exhausted *)
+lemma empty_fail_pt_type_exhausted:
+  "\<lbrakk> pt_t \<noteq> NormalPT_T; pt_t \<noteq> VSRootPT_T \<rbrakk>
+   \<Longrightarrow> False"
+  by (case_tac pt_t; simp)
+
+crunch decodeARMMMUInvocation, Arch_postCapDeletion, setRegister, prepareThreadDelete
+  for (empty_fail) empty_fail[EmptyFail_H_assms, intro!, wp, simp]
+  (simp: Let_def pteAtIndex_def
+   wp: empty_fail_catch empty_fail_pt_type_exhausted empty_fail_arch_cap_exhausted
+   rule: AARCH64_H.postCapDeletion_def)
+
+crunch vcpuEnable, vcpuRestore
+  for (empty_fail) empty_fail[intro!, wp, simp]
+  (simp: uncurry_def)
+
+lemma empty_fail_lookupPTFromLevel[intro!, wp, simp]:
+  "empty_fail (lookupPTFromLevel level ptPtr vPtr target)"
+  by (induct level arbitrary: ptPtr; subst lookupPTFromLevel.simps; simp; wpsimp)
+
+crunch
+  Arch_finaliseCap, Arch.switchToThread, Arch.switchToIdleThread, prepareNextDomain, getRestartPC,
+  makeArchFaultMessage
+  for (empty_fail) empty_fail[EmptyFail_H_assms, intro!, wp, simp]
+  (rule: AARCH64_H.finaliseCap_def)
+
+crunch
+  decodeVCPUInjectIRQ, decodeVCPUWriteReg, decodeVCPUReadReg, doFlush, decodeVCPUAckVPPI,
+  decodeTransfer, checkValidIPCBuffer, Arch.decodeIRQControlInvocation, Arch.decodeInvocation,
+  deleteGhost, Arch.createObject, getSanitiseRegisterInfo,
+  handleArchFaultReply, prepareSetDomain, postModifyRegisters, postSetFlags,
+  Arch.performIRQControl, Arch.invokeIRQHandler, Arch.performInvocation, handleSpuriousIRQ,
+  maskIrqSignal, handleVMFault, checkIRQ, prepareThreadDelete, Arch.postCapDeletion
+  for (empty_fail) empty_fail[EmptyFail_H_assms, intro!, wp, simp]
+  (simp: Let_def)
+
+end (* Arch *)
+
+interpretation EmptyFail_H?: EmptyFail_H
+proof goal_cases
+  interpret Arch  .
+  case 1 show ?case by (intro_locales; (unfold_locales; (fact EmptyFail_H_assms)?)?)
+qed
+
+context Arch begin arch_global_naming
+
+named_theorems EmptyFail_H_2_assms
+
+crunch
+  handleReservedIRQ, handleHypervisorFault
+  for (empty_fail) empty_fail[EmptyFail_H_2_assms, intro!, wp, simp]
+  (simp: Let_def)
+
+end (* Arch *)
+
+interpretation EmptyFail_H_2?: EmptyFail_H_2
+proof goal_cases
+  interpret Arch  .
+  case 1 show ?case by (intro_locales; (unfold_locales; (fact EmptyFail_H_2_assms)?)?)
+qed
+
+crunch callKernel
+  for (empty_fail) empty_fail
+  (wp: empty_fail_catch)
+
+theorem call_kernel_serial:
+  "\<lbrakk> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and
+      schact_is_rct and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) 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