arch_split: invariants: split InterruptAcc_AI [VER-606]

proof/invariant-abstract/ARM/ArchInterruptAcc_AI.thy

@@ -0,0 +1,40 @@
+(*
+ * 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)
+ *)
+
+(*
+ Arch-specific retype invariants
+*)
+
+theory ArchInterruptAcc_AI
+imports "../InterruptAcc_AI"
+begin
+
+context Arch begin global_naming ARM
+
+named_theorems InterruptAcc_AI_assms
+
+lemma dmo_maskInterrupt_invs [InterruptAcc_AI_assms]:
+  "\<lbrace>all_invs_but_valid_irq_states_for irq and (\<lambda>s. state = interrupt_states s irq)\<rbrace> 
+   do_machine_op (maskInterrupt (state = IRQInactive) irq) 
+   \<lbrace>\<lambda>rv. invs\<rbrace>"
+   apply (simp add: do_machine_op_def split_def maskInterrupt_def)
+   apply wp
+   apply (clarsimp simp: in_monad invs_def valid_state_def all_invs_but_valid_irq_states_for_def valid_irq_states_but_def valid_irq_masks_but_def valid_machine_state_def cur_tcb_def valid_irq_states_def valid_irq_masks_def)
+  done
+
+end
+
+global_interpretation InterruptAcc_AI?: InterruptAcc_AI
+  proof goal_cases
+  interpret Arch .
+  case 1 show ?case by (unfold_locales; fact InterruptAcc_AI_assms)
+  qed
+
+end

proof/invariant-abstract/ARM/ArchVSpace_AI.thy

@@ -5033,4 +5033,4 @@ lemma invs_aligned_pdD:
   done
 
 end
-end
+end

proof/invariant-abstract/Finalise_AI.thy

@@ -11,7 +11,7 @@
 theory Finalise_AI
 imports
   "./$L4V_ARCH/ArchIpcCancel_AI"
-  InterruptAcc_AI
+  "./$L4V_ARCH/ArchInterruptAcc_AI"
   "./$L4V_ARCH/ArchRetype_AI"
 begin
 

proof/invariant-abstract/InterruptAcc_AI.thy

@@ -58,21 +58,23 @@ definition all_invs_but_valid_irq_states_for where
   pspace_in_kernel_window and
   cap_refs_in_kernel_window and cur_tcb"
 
-context begin interpretation Arch . (*FIXME: arch_split*)
-lemma dmo_maskInterrupt_invs:
-  "\<lbrace>all_invs_but_valid_irq_states_for irq and (\<lambda>s. state = interrupt_states s irq)\<rbrace> 
-   do_machine_op (maskInterrupt (state = IRQInactive) irq) 
-   \<lbrace>\<lambda>rv. invs\<rbrace>"
-   apply (simp add: do_machine_op_def split_def maskInterrupt_def)
-   apply wp
-   apply (clarsimp simp: in_monad invs_def valid_state_def all_invs_but_valid_irq_states_for_def valid_irq_states_but_def valid_irq_masks_but_def valid_machine_state_def cur_tcb_def valid_irq_states_def valid_irq_masks_def)
-  done
-end
+
+locale InterruptAcc_AI =
+  fixes state_ext_t :: "'state_ext::state_ext itself"
+  assumes dmo_maskInterrupt_invs:
+    "\<And>irq state.
+      \<lbrace>all_invs_but_valid_irq_states_for irq and (\<lambda>s. state = interrupt_states s irq)\<rbrace> 
+        do_machine_op (maskInterrupt (state = IRQInactive) irq) 
+      \<lbrace>\<lambda>rv. invs :: 'state_ext state \<Rightarrow> bool\<rbrace>"
+
+context InterruptAcc_AI begin
 
 lemma set_irq_state_invs[wp]:
-  "\<lbrace>\<lambda>s. invs s \<and> (state \<noteq> irq_state.IRQSignal \<longrightarrow> cap.IRQHandlerCap irq \<notin> ran (caps_of_state s))\<rbrace>
+  "\<And>state irq.
+    \<lbrace>\<lambda>s::'state_ext state. invs s
+          \<and> (state \<noteq> irq_state.IRQSignal \<longrightarrow> cap.IRQHandlerCap irq \<notin> ran (caps_of_state s))\<rbrace>
       set_irq_state state irq
-   \<lbrace>\<lambda>rv. invs\<rbrace>"
+    \<lbrace>\<lambda>rv. invs\<rbrace>"
   apply (simp add: set_irq_state_def)
   apply (wp dmo_maskInterrupt_invs)
   apply (clarsimp simp: invs_def valid_state_def cur_tcb_def valid_mdb_def all_invs_but_valid_irq_states_for_def)
@@ -84,6 +86,8 @@ lemma set_irq_state_invs[wp]:
   apply(clarsimp simp: valid_machine_state_def valid_irq_states_but_def valid_irq_masks_but_def, blast elim: valid_irq_statesE)
   done
 
+end
+
 lemmas ucast_ucast_mask8 = ucast_ucast_mask[where 'a=8, simplified, symmetric]
 
 end

proof/invariant-abstract/Retype_AI.thy

@@ -2474,11 +2474,11 @@ lemma pspace_no_overlap_typ_at_lift:
   apply (clarsimp simp: pspace_no_overlap_typ_at_def)
   apply (wp hoare_vcg_all_lift f)
   done
-context begin interpretation Arch . (*FIXME: arch_split*)
+
+
 lemma swp_clearMemoryVM [simp]:
   "swp clearMemoryVM x = (\<lambda>_. return ())"
   by (rule ext,simp)
-end
 
 
 (* FIXME: move *)

proof/invariant-abstract/VSpacePre_AI.thy

@@ -247,7 +247,4 @@ lemma set_mrs_ntfn_at[wp]:
   "\<lbrace> ntfn_at p \<rbrace> set_mrs receiver recv_buf mrs \<lbrace>\<lambda>rv. ntfn_at p \<rbrace>"
   by (simp add: ntfn_at_typ, wp)
 
-
-
-
-end
+end