x64 crefine: ioapic_nirqs proof updates

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

proof/crefine/X64/ADT_C.thy

@@ -539,6 +539,10 @@ end
 
 context state_rel begin
 
+definition
+  "ioapic_nirqs_to_H cstate \<equiv>
+     \<lambda>x. if x \<le> of_nat maxNumIOAPIC then ioapic_nirqs_' cstate.[unat x] else 0"
+
 definition
   "carch_state_to_H cstate \<equiv>
    X64KernelState
@@ -553,6 +557,7 @@ definition
       x64KSKernelVSpace_C
       (cioport_bitmap_to_H (the (clift (t_hrs_' cstate) (Ptr (symbol_table ''x86KSAllocatedIOPorts'')))))
       (ucast (num_ioapics_' cstate))
+      (ioapic_nirqs_to_H cstate)
       \<comment> \<open>Map IRQ states to their Haskell equivalent, and out-of-bounds entries to X64IRQFree\<close>
       (case_option X64IRQFree id \<circ>
           (array_map_conv
@@ -582,14 +587,19 @@ lemma carch_state_to_H_correct:
   using valid[simplified valid_arch_state'_def]
   apply (fastforce simp: valid_asid_table'_def)
   apply (simp add: ccr3_relation_def split: cr3.splits)
+  apply (rule conjI)
+   apply (solves \<open>clarsimp simp: global_ioport_bitmap_relation_def\<close>)
   apply (rule conjI)
    prefer 2
    apply (rule ext)
    apply (clarsimp simp: x64_irq_state_relation_def array_relation_def array_map_conv_def
                          array_to_map_def)
    using valid[simplified valid_arch_state'_def valid_x64_irq_state'_def]
    apply (case_tac "x \<le> maxIRQ"; fastforce split: option.split)
-  apply (clarsimp simp: global_ioport_bitmap_relation_def)
+  apply (clarsimp simp: array_relation_def ioapic_nirqs_to_H_def)
+  apply (rule ext)
+  using valid[simplified valid_arch_state'_def valid_ioapic_def]
+  apply (clarsimp simp: not_le)
   done
 
 end

proof/crefine/X64/Interrupt_C.thy

@@ -530,32 +530,61 @@ lemma ccorres_pre_gets_x64KSNumIOAPICs_ksArchState:
   apply clarsimp
   done
 
+lemma ccorres_pre_gets_x64KSIOAPICnIRQs_ksArchState:
+  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
+  shows   "ccorres r xf
+                   (\<lambda>s. (\<forall>rv. x64KSIOAPICnIRQs (ksArchState s) = rv  \<longrightarrow> P rv s))
+                   {s. \<forall>rv. s \<in> P' rv } hs
+                   (gets (x64KSIOAPICnIRQs \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c"
+  apply (rule ccorres_guard_imp)
+    apply (rule ccorres_symb_exec_l)
+       defer
+       apply wp[1]
+      apply (rule gets_sp)
+     apply (clarsimp simp: empty_fail_def simpler_gets_def)
+    apply assumption
+   apply clarsimp
+   defer
+   apply (rule ccorres_guard_imp)
+     apply (rule cc)
+    apply clarsimp
+   apply assumption
+  apply clarsimp
+  done
+
+lemma rf_sr_x64KSIOAPICnIRQs:
+  "\<lbrakk> (s,s') \<in> rf_sr; i < of_nat maxNumIOAPIC \<rbrakk> \<Longrightarrow>
+   ioapic_nirqs_' (globals s').[unat i] = x64KSIOAPICnIRQs (ksArchState s) i"
+  by (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def Let_def
+                     array_relation_def)
+
 lemma ioapic_decode_map_pin_to_vector_ccorres:
   "ccorres (intr_and_se_rel \<currency> dc)
      (liftxf errstate id (K ()) ret__unsigned_long_')
-     \<top>
-     (UNIV
-           \<inter> {s. ioapic___unsigned_long_' s = ioapic}
-           \<inter> {s. pin___unsigned_long_' s = pin}
-           \<inter> {s. level___unsigned_long_' s = level}
-           \<inter> {s. polarity_' s = polarity})
+     valid_ioapic
+     (\<lbrace>\<acute>ioapic___unsigned_long = ioapic\<rbrace> \<inter>
+      \<lbrace>\<acute>pin___unsigned_long = pin\<rbrace> \<inter>
+      \<lbrace>\<acute>level___unsigned_long = level\<rbrace> \<inter>
+      \<lbrace>\<acute>polarity = polarity\<rbrace>)
      hs
      (doE numIOAPICs <- liftE (gets (x64KSNumIOAPICs \<circ> ksArchState));
+          ioapic_nirqs <- liftE (gets (x64KSIOAPICnIRQs \<circ> ksArchState));
           whenE (numIOAPICs = 0) (throwError (Inl IllegalOperation));
           whenE (uint (numIOAPICs - 1) < uint ioapic)
-                     (throwError (Inl (RangeError 0 (numIOAPICs - 1))));
-          whenE (uint (ioapicIRQLines - 1) < uint pin)
-                     (throwError (Inl (RangeError 0 (ioapicIRQLines - 1))));
+                (throwError (Inl (RangeError 0 (numIOAPICs - 1))));
+          whenE (uint (ucast (ioapic_nirqs ioapic - 1) :: machine_word) < uint pin)
+                (throwError (Inl (RangeError 0 (ucast (ioapic_nirqs ioapic - 1)))));
           whenE (1 < uint level) (throwError (Inl (RangeError 0 1)));
           whenE (1 < uint polarity) (throwError (Inl (RangeError 0 1)))
        odE)
-    (Call ioapic_decode_map_pin_to_vector_'proc)"
-  supply Collect_const[simp del]
+     (Call ioapic_decode_map_pin_to_vector_'proc)"
+  supply Collect_const[simp del] word_less_1[simp del] (* for uniform array guard on ioapic_nirqs *)
   apply (cinit' lift: ioapic___unsigned_long_' pin___unsigned_long_' level___unsigned_long_'
                       polarity_')
    apply (simp add: ioapicIRQLines_def cong: StateSpace.state.fold_congs globals.fold_congs)
    apply (clarsimp simp: liftE_bindE)
    apply (rule ccorres_pre_gets_x64KSNumIOAPICs_ksArchState)
+   apply (rule ccorres_pre_gets_x64KSIOAPICnIRQs_ksArchState)
    apply (rule_tac Q="\<lambda>s. x64KSNumIOAPICs (ksArchState s) = numIOAPICs" and Q'=\<top>
                    in ccorres_split_when_throwError_cond)
       apply (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def Let_def)
@@ -573,23 +602,55 @@ lemma ioapic_decode_map_pin_to_vector_ccorres:
                             EXCEPTION_SYSCALL_ERROR_def EXCEPTION_NONE_def syscall_error_rel_def)
       apply (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def Let_def)
       apply (subst ucast_sub_ucast; fastforce simp: lt1_neq0)
+     apply (rule_tac P="numIOAPICs \<le> of_nat maxNumIOAPIC" in ccorres_gen_asm)
+     apply (clarsimp simp: not_less word_le_def[symmetric])
+     apply (prop_tac "ioapic < of_nat maxNumIOAPIC",
+            solves \<open>simp add: le_m1_iff_lt[THEN iffD1] word_neq_0_conv\<close>)
+     apply (rule ccorres_prove_guard)
+      (* array guard where array dimension is maxNumIOAPIC *)
+      apply (solves \<open>simp add: Kernel_Config.maxNumIOAPIC_def\<close>)
+     apply ccorres_rewrite
+     apply (rename_tac ioapic_nirqs)
+     apply (rule_tac Q="\<lambda>s. ioapic_nirqs = x64KSIOAPICnIRQs (ksArchState s) \<and>
+                            0 < x64KSIOAPICnIRQs (ksArchState s) ioapic" and
+                     Q'=\<top>
+                     in ccorres_split_when_throwError_cond)
+        apply (fastforce simp: word_le_def scast_ucast_up_eq_ucast uint_up_ucast is_up
+                               rf_sr_x64KSIOAPICnIRQs
+                               uint_minus_1_less_le_eq)
+      (* Need to VCG it as the range error depends on the global state *)
+      apply (rule_tac P="\<lambda>s. ioapic_nirqs = x64KSIOAPICnIRQs (ksArchState s) \<and>
+                             numIOAPICs \<le> of_nat maxNumIOAPIC \<and>
+                             0 < x64KSIOAPICnIRQs (ksArchState s) ioapic \<and>
+                             x64KSIOAPICnIRQs (ksArchState s) ioapic \<le> ucast ioapicIRQLines"
+                  and P'="UNIV" in ccorres_from_vcg_throws)
+      apply (rule allI, rule conseqPre, vcg)
+      apply (clarsimp simp: fst_throwError_returnOk syscall_error_to_H_cases
+                            EXCEPTION_SYSCALL_ERROR_def EXCEPTION_NONE_def syscall_error_rel_def)
+      apply (simp add: rf_sr_x64KSIOAPICnIRQs
+                       scast_ucast_up_eq_ucast ioapicIRQLines_def sint_ucast_eq_uint is_down
+                       scast_ucast_up_minus_1_ucast)
+      apply (rule conjI, uint_arith)
+      apply (rule conjI, uint_arith)
+      (* array guard where array dimension is maxNumIOAPIC *)
+      apply (solves \<open>simp add: Kernel_Config.maxNumIOAPIC_def\<close>)
      apply (rule_tac Q=\<top> and Q'=\<top> in ccorres_split_when_throwError_cond)
-        apply (fastforce simp: word_le_def add1_zle_eq[symmetric])
+        apply clarsimp
+        apply (metis arith_special(21) diff_eq_diff_eq uint_1 word_less_def word_less_sub1
+                     word_neq_0_conv word_sub_less_iff)
        apply (fastforce simp: syscall_error_to_H_cases intro: syscall_error_throwError_ccorres_n)
-      apply (rule_tac Q=\<top> and Q'=\<top> in ccorres_split_when_throwError_cond)
+      apply (rule_tac Q=\<top> and Q'=\<top>
+                      in ccorres_split_when_throwError_cond[where b="returnOk ()", simplified])
          apply clarsimp
          apply (metis arith_special(21) diff_eq_diff_eq uint_1 word_less_def word_less_sub1
                       word_neq_0_conv word_sub_less_iff)
         apply (fastforce simp: syscall_error_to_H_cases intro: syscall_error_throwError_ccorres_n)
-       apply (rule_tac Q=\<top> and Q'=\<top>
-                       in ccorres_split_when_throwError_cond[where b="returnOk ()", simplified])
-          apply clarsimp
-          apply (metis arith_special(21) diff_eq_diff_eq uint_1 word_less_def word_less_sub1
-                       word_neq_0_conv word_sub_less_iff)
-         apply (fastforce simp: syscall_error_to_H_cases intro: syscall_error_throwError_ccorres_n)
-        apply (ctac add: ccorres_return_CE)
-       apply vcg+
-  apply fastforce
+       apply (ctac add: ccorres_return_CE)
+      apply vcg+
+  apply (clarsimp simp: not_less)
+  apply (prop_tac "ioapic < x64KSNumIOAPICs (ksArchState s)")
+   apply (meson word_leq_minus_one_le word_less_eq_iff_unsigned)
+  apply (fastforce simp: valid_ioapic_def)
   done
 
 (* Bundle of definitions for minIRQ, maxIRQ, minUserIRQ, etc *)
@@ -867,11 +928,8 @@ from assms show ?thesis
                                     invs_sch_act_wf' ct_in_state'_def cte_wp_at_weakenE'
                                     pred_tcb'_weakenE invs_pspace_aligned' invs_pspace_distinct')
               apply (subst pred_tcb'_weakenE, assumption, fastforce)+
-              apply (rule conjI)
-               apply (rule TrueI)
-              apply (rule conjI)
-               apply (rule impI)
-               apply (rule TrueI)
+              apply (rule conjI, fastforce)
+              apply clarsimp
               apply (rule_tac irq1="yf" in irq64_helper_two)
               apply (simp only: unat_def)
              apply (vcg exspec=isIRQActive_modifies)

proof/crefine/X64/SR_lemmas_C.thy

@@ -1065,7 +1065,6 @@ lemma cstate_relation_only_t_hrs:
   ksCurThread_' s = ksCurThread_' t;
   ksIdleThread_' s = ksIdleThread_' t;
   ksWorkUnitsCompleted_' s = ksWorkUnitsCompleted_' t;
-  intStateIRQNode_' s = intStateIRQNode_' t;
   intStateIRQTable_' s = intStateIRQTable_' t;
   x86KSASIDTable_' s = x86KSASIDTable_' t;
   x64KSCurrentUserCR3_' s = x64KSCurrentUserCR3_' t;
@@ -1075,6 +1074,7 @@ lemma cstate_relation_only_t_hrs:
   ksCurDomain_' s = ksCurDomain_' t;
   ksDomainTime_' s = ksDomainTime_' t;
   num_ioapics_' s = num_ioapics_' t;
+  ioapic_nirqs_' s = ioapic_nirqs_' t;
   x86KSIRQState_' s = x86KSIRQState_' t
   \<rbrakk>
   \<Longrightarrow> cstate_relation a s = cstate_relation a t"
@@ -1091,7 +1091,6 @@ lemma rf_sr_upd:
     "(ksCurThread_' (globals x)) = (ksCurThread_' (globals y))"
     "(ksIdleThread_' (globals x)) = (ksIdleThread_' (globals y))"
     "(ksWorkUnitsCompleted_' (globals x)) = (ksWorkUnitsCompleted_' (globals y))"
-    "intStateIRQNode_'(globals x) = intStateIRQNode_' (globals y)"
     "intStateIRQTable_'(globals x) = intStateIRQTable_' (globals y)"
     "x86KSASIDTable_' (globals x) = x86KSASIDTable_' (globals y)"
     "x64KSCurrentUserCR3_' (globals x) = x64KSCurrentUserCR3_' (globals y)"
@@ -1101,6 +1100,7 @@ lemma rf_sr_upd:
     "ksCurDomain_' (globals x) = ksCurDomain_' (globals y)"
     "ksDomainTime_' (globals x) = ksDomainTime_' (globals y)"
     "num_ioapics_' (globals x) = num_ioapics_' (globals y)"
+    "ioapic_nirqs_' (globals x) = ioapic_nirqs_' (globals y)"
     "x86KSIRQState_' (globals x) = x86KSIRQState_' (globals y)"
   shows "((a, x) \<in> rf_sr) = ((a, y) \<in> rf_sr)"
   unfolding rf_sr_def using assms
@@ -1114,7 +1114,6 @@ lemma rf_sr_upd_safe[simp]:
   and     sa: "(ksSchedulerAction_' (globals (g y))) = (ksSchedulerAction_' (globals y))"
   and     ct: "(ksCurThread_' (globals (g y))) = (ksCurThread_' (globals y))"
   and     it: "(ksIdleThread_' (globals (g y))) = (ksIdleThread_' (globals y))"
-  and     isn: "intStateIRQNode_'(globals (g y)) = intStateIRQNode_' (globals y)"
   and     ist: "intStateIRQTable_'(globals (g y)) = intStateIRQTable_' (globals y)"
   and     dsi: "ksDomScheduleIdx_' (globals (g y)) = ksDomScheduleIdx_' (globals y)"
   and     cdom: "ksCurDomain_' (globals (g y)) = ksCurDomain_' (globals y)"
@@ -1124,11 +1123,12 @@ lemma rf_sr_upd_safe[simp]:
     "x64KSCurrentUserCR3_' (globals (g y)) = x64KSCurrentUserCR3_' (globals y)"
     "phantom_machine_state_' (globals (g y)) = phantom_machine_state_' (globals y)"
     "num_ioapics_' (globals (g y)) = num_ioapics_' (globals y)"
+    "ioapic_nirqs_' (globals (g y)) = ioapic_nirqs_' (globals y)"
     "x86KSIRQState_' (globals (g y)) = x86KSIRQState_' (globals y)"
   and    gs: "ghost'state_' (globals (g y)) = ghost'state_' (globals y)"
   and     wu:  "(ksWorkUnitsCompleted_' (globals (g y))) = (ksWorkUnitsCompleted_' (globals y))"
   shows "((a, (g y)) \<in> rf_sr) = ((a, y) \<in> rf_sr)"
-  using rl rq rqL1 rqL2 sa ct it isn ist arch wu gs dsi cdom dt by - (rule rf_sr_upd)
+  using assms by - (rule rf_sr_upd)
 
 (* More of a well-formed lemma, but \<dots> *)
 lemma valid_mdb_cslift_next:

proof/crefine/X64/StateRelation_C.thy

@@ -191,6 +191,7 @@ where
     global_ioport_bitmap_relation (clift (t_hrs_' cstate)) (x64KSAllocatedIOPorts astate) \<and>
     fpu_null_state_relation (t_hrs_' cstate) \<and>
     x64KSNumIOAPICs astate = UCAST (32 \<rightarrow> 64) (num_ioapics_' cstate) \<and>
+    array_relation (=) (of_nat Kernel_Config.maxNumIOAPIC) (x64KSIOAPICnIRQs astate) (ioapic_nirqs_' cstate) \<and>
     array_relation x64_irq_state_relation maxIRQ (x64KSIRQState astate) (x86KSIRQState_' cstate) \<and>
     carch_globals astate"
 

proof/crefine/lib/Ctac.thy

@@ -1949,6 +1949,18 @@ lemmas ccorres_move_const_guards
     = ccorres_move_const_guard
       ccorres_move_const_guard[unfolded Collect_const]
 
+lemma ccorres_prove_guard_direct:
+  "\<lbrakk> G; ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m (c) \<rbrakk> \<Longrightarrow>
+   ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m (Guard F \<lbrace>G\<rbrace> c)"
+  by (rule ccorres_guard_imp, erule ccorres_move_const_guard; simp)
+
+lemma ccorres_prove_guard_seq:
+  "\<lbrakk> G; ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m (c;; d) \<rbrakk> \<Longrightarrow>
+   ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m (Guard F \<lbrace>G\<rbrace> c;; d)"
+  by (rule ccorres_guard_imp, erule ccorres_move_const_guard; simp)
+
+lemmas ccorres_prove_guard = ccorres_prove_guard_direct ccorres_prove_guard_seq
+
 lemma liftM_exs_valid:
   "\<lbrace>P\<rbrace> m \<exists>\<lbrace>\<lambda>rv. Q (f rv)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> liftM f m \<exists>\<lbrace>Q\<rbrace>"
   unfolding liftM_def exs_valid_def