diff --git a/proof/crefine/X64/ADT_C.thy b/proof/crefine/X64/ADT_C.thy index 049d7689c0..82672f5287 100644 --- a/proof/crefine/X64/ADT_C.thy +++ b/proof/crefine/X64/ADT_C.thy @@ -539,6 +539,10 @@ end context state_rel begin +definition + "ioapic_nirqs_to_H cstate \ + \x. if x \ of_nat maxNumIOAPIC then ioapic_nirqs_' cstate.[unat x] else 0" + definition "carch_state_to_H cstate \ 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) \ \Map IRQ states to their Haskell equivalent, and out-of-bounds entries to X64IRQFree\ (case_option X64IRQFree id \ (array_map_conv @@ -582,6 +587,8 @@ 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 \clarsimp simp: global_ioport_bitmap_relation_def\) apply (rule conjI) prefer 2 apply (rule ext) @@ -589,7 +596,10 @@ lemma carch_state_to_H_correct: array_to_map_def) using valid[simplified valid_arch_state'_def valid_x64_irq_state'_def] apply (case_tac "x \ 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 diff --git a/proof/crefine/X64/Interrupt_C.thy b/proof/crefine/X64/Interrupt_C.thy index 4f21490401..cb5bced472 100644 --- a/proof/crefine/X64/Interrupt_C.thy +++ b/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: "\rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" + shows "ccorres r xf + (\s. (\rv. x64KSIOAPICnIRQs (ksArchState s) = rv \ P rv s)) + {s. \rv. s \ P' rv } hs + (gets (x64KSIOAPICnIRQs \ ksArchState) >>= (\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: + "\ (s,s') \ rf_sr; i < of_nat maxNumIOAPIC \ \ + 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 \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') - \ - (UNIV - \ {s. ioapic___unsigned_long_' s = ioapic} - \ {s. pin___unsigned_long_' s = pin} - \ {s. level___unsigned_long_' s = level} - \ {s. polarity_' s = polarity}) + valid_ioapic + (\\ioapic___unsigned_long = ioapic\ \ + \\pin___unsigned_long = pin\ \ + \\level___unsigned_long = level\ \ + \\polarity = polarity\) hs (doE numIOAPICs <- liftE (gets (x64KSNumIOAPICs \ ksArchState)); + ioapic_nirqs <- liftE (gets (x64KSIOAPICnIRQs \ 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="\s. x64KSNumIOAPICs (ksArchState s) = numIOAPICs" and Q'=\ 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 \ of_nat maxNumIOAPIC" in ccorres_gen_asm) + apply (clarsimp simp: not_less word_le_def[symmetric]) + apply (prop_tac "ioapic < of_nat maxNumIOAPIC", + solves \simp add: le_m1_iff_lt[THEN iffD1] word_neq_0_conv\) + apply (rule ccorres_prove_guard) + (* array guard where array dimension is maxNumIOAPIC *) + apply (solves \simp add: Kernel_Config.maxNumIOAPIC_def\) + apply ccorres_rewrite + apply (rename_tac ioapic_nirqs) + apply (rule_tac Q="\s. ioapic_nirqs = x64KSIOAPICnIRQs (ksArchState s) \ + 0 < x64KSIOAPICnIRQs (ksArchState s) ioapic" and + Q'=\ + 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="\s. ioapic_nirqs = x64KSIOAPICnIRQs (ksArchState s) \ + numIOAPICs \ of_nat maxNumIOAPIC \ + 0 < x64KSIOAPICnIRQs (ksArchState s) ioapic \ + x64KSIOAPICnIRQs (ksArchState s) ioapic \ 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 \simp add: Kernel_Config.maxNumIOAPIC_def\) apply (rule_tac Q=\ and Q'=\ 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=\ and Q'=\ in ccorres_split_when_throwError_cond) + apply (rule_tac Q=\ and Q'=\ + 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=\ and Q'=\ - 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) diff --git a/proof/crefine/X64/SR_lemmas_C.thy b/proof/crefine/X64/SR_lemmas_C.thy index e5103dbdf9..8b00610a92 100644 --- a/proof/crefine/X64/SR_lemmas_C.thy +++ b/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 \ \ 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) \ rf_sr) = ((a, y) \ 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)) \ rf_sr) = ((a, y) \ 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 \ *) lemma valid_mdb_cslift_next: diff --git a/proof/crefine/X64/StateRelation_C.thy b/proof/crefine/X64/StateRelation_C.thy index 0701acd80b..0f17b0fbc4 100644 --- a/proof/crefine/X64/StateRelation_C.thy +++ b/proof/crefine/X64/StateRelation_C.thy @@ -191,6 +191,7 @@ where global_ioport_bitmap_relation (clift (t_hrs_' cstate)) (x64KSAllocatedIOPorts astate) \ fpu_null_state_relation (t_hrs_' cstate) \ x64KSNumIOAPICs astate = UCAST (32 \ 64) (num_ioapics_' cstate) \ + array_relation (=) (of_nat Kernel_Config.maxNumIOAPIC) (x64KSIOAPICnIRQs astate) (ioapic_nirqs_' cstate) \ array_relation x64_irq_state_relation maxIRQ (x64KSIRQState astate) (x86KSIRQState_' cstate) \ carch_globals astate" diff --git a/proof/crefine/lib/Ctac.thy b/proof/crefine/lib/Ctac.thy index f07db59f25..e5b71f8994 100644 --- a/proof/crefine/lib/Ctac.thy +++ b/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: + "\ G; ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m (c) \ \ + ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m (Guard F \G\ c)" + by (rule ccorres_guard_imp, erule ccorres_move_const_guard; simp) + +lemma ccorres_prove_guard_seq: + "\ G; ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m (c;; d) \ \ + ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m (Guard F \G\ 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: "\P\ m \\\rv. Q (f rv)\ \ \P\ liftM f m \\Q\" unfolding liftM_def exs_valid_def