diff --git a/proof/crefine/ARM/Ctac_lemmas_C.thy b/proof/crefine/ARM/Ctac_lemmas_C.thy index 2b42ab3a0c..c6e7f407ed 100644 --- a/proof/crefine/ARM/Ctac_lemmas_C.thy +++ b/proof/crefine/ARM/Ctac_lemmas_C.thy @@ -183,7 +183,7 @@ lemmas ccorres_move_c_guard_ap = ccorres_move_c_guards [OF move_c_guard_ap] lemma array_assertion_abs_irq: "\s s'. (s, s') \ rf_sr \ True - \ (n s' \ 256 \ (x s' \ 0 \ n s' \ 0)) + \ (n s' \ 2^LENGTH(irq_len) \ (x s' \ 0 \ n s' \ 0)) \ (x s' = 0 \ array_assertion intStateIRQNode_Ptr (n s') (hrs_htd (t_hrs_' (globals s'))))" apply (intro allI impI disjCI2) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) diff --git a/proof/crefine/ARM/Interrupt_C.thy b/proof/crefine/ARM/Interrupt_C.thy index 9432a06011..58bc21d17d 100644 --- a/proof/crefine/ARM/Interrupt_C.thy +++ b/proof/crefine/ARM/Interrupt_C.thy @@ -299,7 +299,9 @@ lemma invokeIRQControl_expanded_ccorres: apply (rule conjI, fastforce)+ apply (clarsimp simp: Collect_const_mem ccap_relation_def cap_irq_handler_cap_lift cap_to_H_def c_valid_cap_def cl_valid_cap_def irq_len_val ucast_and_mask) - apply word_eqI + (* if irq_len < 8, there may be an additional term in the goal *) + apply (rule conjI, word_eqI_solve)? + apply (word_eqI_solve dest: bit_imp_le_length) done lemma invokeIRQControl_ccorres: diff --git a/proof/crefine/ARM/Refine_C.thy b/proof/crefine/ARM/Refine_C.thy index f072174c0c..563f15f7a2 100644 --- a/proof/crefine/ARM/Refine_C.thy +++ b/proof/crefine/ARM/Refine_C.thy @@ -36,7 +36,7 @@ lemma schedule_sch_act_wf: apply (rule schedule_invs') done -(* On GICv2 and GICv3, irqInvalid is picked such it is outside the range of possible IRQs +(* On Arm, irqInvalid is picked such it is outside the range of possible IRQs by type alone. *) lemma irq_type_never_invalid_left: "ucast irq \ irqInvalid" for irq::irq diff --git a/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy b/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy index e099909f4e..f79b929cc6 100644 --- a/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy +++ b/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy @@ -186,7 +186,7 @@ lemmas ccorres_move_c_guard_ap = ccorres_move_c_guards [OF move_c_guard_ap] lemma array_assertion_abs_irq: "\s s'. (s, s') \ rf_sr \ True - \ (n s' \ 256 \ (x s' \ 0 \ n s' \ 0)) + \ (n s' \ 2^LENGTH(irq_len) \ (x s' \ 0 \ n s' \ 0)) \ (x s' = 0 \ array_assertion intStateIRQNode_Ptr (n s') (hrs_htd (t_hrs_' (globals s'))))" apply (intro allI impI disjCI2) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) diff --git a/proof/crefine/ARM_HYP/Interrupt_C.thy b/proof/crefine/ARM_HYP/Interrupt_C.thy index 88046147c6..8c8d9e1ac2 100644 --- a/proof/crefine/ARM_HYP/Interrupt_C.thy +++ b/proof/crefine/ARM_HYP/Interrupt_C.thy @@ -309,7 +309,9 @@ lemma invokeIRQControl_expanded_ccorres: apply (clarsimp simp: Collect_const_mem ccap_relation_def cap_irq_handler_cap_lift cap_to_H_def c_valid_cap_def cl_valid_cap_def irq_len_val word_bw_assocs mask_twice) - apply word_eqI + (* if irq_len < 8, there may be an additional term in the goal *) + apply (rule conjI, word_eqI_solve)? + apply (word_eqI_solve dest: bit_imp_le_length) done lemma invokeIRQControl_ccorres: diff --git a/proof/crefine/ARM_HYP/Refine_C.thy b/proof/crefine/ARM_HYP/Refine_C.thy index 1c73871530..d6c0182dfb 100644 --- a/proof/crefine/ARM_HYP/Refine_C.thy +++ b/proof/crefine/ARM_HYP/Refine_C.thy @@ -30,7 +30,7 @@ lemma schedule_sch_act_wf: apply (rule schedule_invs') done -(* On GICv2 and GICv3, irqInvalid is picked such it is outside the range of possible IRQs +(* On Arm, irqInvalid is picked such it is outside the range of possible IRQs by type alone. *) lemma irq_type_never_invalid_left: "ucast irq \ irqInvalid" for irq::irq diff --git a/sys-init/examples/ExampleSpecIRQ_SI.thy b/sys-init/examples/ExampleSpecIRQ_SI.thy index 8a8c133bd9..a197456d0b 100644 --- a/sys-init/examples/ExampleSpecIRQ_SI.thy +++ b/sys-init/examples/ExampleSpecIRQ_SI.thy @@ -119,7 +119,7 @@ definition 4 \ EndpointCap ep_id 0 {Read}, 7 \ PageDirectoryCap pd_b_id Real None, 8 \ FrameCap False frame_b_id {AllowRead, AllowWrite} small_section_size Real None, - 254 \ IrqHandlerCap 254]" + 0x3F \ IrqHandlerCap 0x3F]" definition "cnode_extra \ @@ -160,14 +160,16 @@ definition irq_objects :: cdl_heap where "irq_objects \ - \obj_id. if obj_id = 0x104 then Some (IRQNode (new_irq_node ntfn_id)) - else if 0x100 \ obj_id \ obj_id < 0x200 then (Some (IRQNode empty_irq_node)) + \obj_id. if obj_id = 0x104 + then Some (IRQNode (new_irq_node ntfn_id)) + else if 0x100 \ obj_id \ obj_id \ 0x100 + mask LENGTH(irq_len) + then (Some (IRQNode empty_irq_node)) else None" lemma "irq_objects = - (\obj_id. if 0x100 \ obj_id \ obj_id < 0x200 + (\obj_id. if 0x100 \ obj_id \ obj_id \ 0x100 + mask LENGTH(irq_len) then (Some (IRQNode empty_irq_node)) else None) ++ (\obj_id. if obj_id = 0x104 then Some (IRQNode (new_irq_node ntfn_id)) @@ -193,9 +195,9 @@ definition frame_a2_id \ Frame empty_frame, frame_b_id \ Frame empty_section, ep_id \ Endpoint, - ntfn_id \ Notification, + ntfn_id \ Notification, 0x104 \ IRQNode (new_irq_node ntfn_id), - 0x1FE \ IRQNode empty_irq_node], + 0x13F \ IRQNode empty_irq_node], cdl_cdt = [(cnode_a2_id, 0) \ (cnode_extra_id, 1), (cnode_b_id, 4) \ (cnode_extra_id, 1), (cnode_a2_id, 10) \ (cnode_extra_id, 2)], \ \All caps are orig caps, @@ -349,7 +351,7 @@ lemma range_example_irq_node: done lemma irq_nodes_example_spec: - "irq_nodes example_spec = {obj_id. obj_id = 0x104 \ obj_id = 0x1FE}" + "irq_nodes example_spec = {obj_id. obj_id = 0x104 \ obj_id = 0x13F}" by (auto simp: irq_nodes_def example_spec_def object_at_def is_irq_node_def) (************************* @@ -386,7 +388,7 @@ lemma cap_irq_simp [simp]: lemma example_irq_node_simps [simp]: "example_irq_node 4 = 0x104" - "example_irq_node 0xFE = 0x1FE" + "example_irq_node 0x3F = 0x13F" by (simp add: example_irq_node_def)+ lemma irq_objects_simps [simp]: @@ -473,7 +475,7 @@ lemma slots_of_example_spec_obj_ids: lemma irq_handler_cap_example_spec: "\is_irqhandler_cap cap; opt_cap (obj_id, slot) example_spec = Some cap\ \ (obj_id = cnode_a2_id \ slot = 12) \ - (obj_id = cnode_b_id \ slot = 254)" + (obj_id = cnode_b_id \ slot = 0x3F)" by (clarsimp simp: example_spec_def opt_cap_def slots_of_def object_slots_def empty_irq_node_def new_irq_node_def new_cnode_def obj_defs new_cap_map_def empty_cap_map_def @@ -483,7 +485,7 @@ lemma irq_handler_cap_example_spec: lemma irqhandler_cap_at_example_spec: "irqhandler_cap_at (obj_id, slot) example_spec = ((obj_id = cnode_a2_id \ slot = 12) \ - (obj_id = cnode_b_id \ slot = 254))" + (obj_id = cnode_b_id \ slot = 0x3F))" apply (clarsimp simp: cap_at_def) apply (rule iffI) apply clarsimp @@ -678,13 +680,13 @@ lemma real_object_at_example_spec_simp [simp]: "real_object_at 0xC example_spec" "real_object_at 0xD example_spec" "\real_object_at 0x104 example_spec" - "\real_object_at 0x1FE example_spec" + "\real_object_at 0x13F example_spec" by (clarsimp simp: real_object_at_example_spec)+ lemma cdl_objects_example_spec_simps [simp]: "cdl_objects example_spec 4 = Some (Frame empty_frame)" "cdl_objects example_spec 0xD = Some Notification" - "cdl_objects example_spec 0x1FE = Some (IRQNode empty_irq_node)" + "cdl_objects example_spec 0x13F = Some (IRQNode empty_irq_node)" by (clarsimp simp: example_spec_def map_add_def)+ lemma well_formed_cap_to_object_example: @@ -728,7 +730,7 @@ lemma well_formed_cap_to_object_example: apply (rule_tac x=12 in exI) (* Not sure why fastforce gives up here. *) apply (fastforce simp: cnode_at_example_spec cnode_a2_def object_slots_def new_cnode_def new_cap_map_def) - apply (case_tac "obj_id = 0x1FE") + apply (case_tac "obj_id = 0x13F") apply (rule_tac x=cnode_b_id in exI) apply (fastforce simp: cnode_at_example_spec cnode_b_def object_slots_def new_cnode_def new_cap_map_def)