Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

make ARM+ARM_HYP proofs work for smaller irq_len #820

Merged
merged 2 commits into from
Dec 19, 2024
Merged

make ARM+ARM_HYP proofs work for smaller irq_len #820

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c60d1c0
sys-init: make example work for small irq_len
lsf37 Sep 26, 2024
222d65f
crefine arm+arm-hyp: deal with smaller irq_len
lsf37 Sep 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion proof/crefine/ARM/Ctac_lemmas_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -183,7 +183,7 @@ lemmas ccorres_move_c_guard_ap = ccorres_move_c_guards [OF move_c_guard_ap]

lemma array_assertion_abs_irq:
"\<forall>s s'. (s, s') \<in> rf_sr \<and> True
\<and> (n s' \<le> 256 \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
\<and> (n s' \<le> 2^LENGTH(irq_len) \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
\<longrightarrow> (x s' = 0 \<or> 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)
Expand Down
4 changes: 3 additions & 1 deletion proof/crefine/ARM/Interrupt_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Comment on lines +302 to +304
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, this is a clever way to handle this. Thanks for the comment, it would have been very confusing without it

done

lemma invokeIRQControl_ccorres:
Expand Down
2 changes: 1 addition & 1 deletion proof/crefine/ARM/Refine_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 \<noteq> irqInvalid" for irq::irq
Expand Down
2 changes: 1 addition & 1 deletion proof/crefine/ARM_HYP/Ctac_lemmas_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -186,7 +186,7 @@ lemmas ccorres_move_c_guard_ap = ccorres_move_c_guards [OF move_c_guard_ap]

lemma array_assertion_abs_irq:
"\<forall>s s'. (s, s') \<in> rf_sr \<and> True
\<and> (n s' \<le> 256 \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
\<and> (n s' \<le> 2^LENGTH(irq_len) \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
\<longrightarrow> (x s' = 0 \<or> 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)
Expand Down
4 changes: 3 additions & 1 deletion proof/crefine/ARM_HYP/Interrupt_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
2 changes: 1 addition & 1 deletion proof/crefine/ARM_HYP/Refine_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 \<noteq> irqInvalid" for irq::irq
Expand Down
28 changes: 15 additions & 13 deletions sys-init/examples/ExampleSpecIRQ_SI.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,7 @@ definition
4 \<mapsto> EndpointCap ep_id 0 {Read},
7 \<mapsto> PageDirectoryCap pd_b_id Real None,
8 \<mapsto> FrameCap False frame_b_id {AllowRead, AllowWrite} small_section_size Real None,
254 \<mapsto> IrqHandlerCap 254]"
0x3F \<mapsto> IrqHandlerCap 0x3F]"

definition
"cnode_extra \<equiv>
Expand Down Expand Up @@ -160,14 +160,16 @@ definition
irq_objects :: cdl_heap
where
"irq_objects \<equiv>
\<lambda>obj_id. if obj_id = 0x104 then Some (IRQNode (new_irq_node ntfn_id))
else if 0x100 \<le> obj_id \<and> obj_id < 0x200 then (Some (IRQNode empty_irq_node))
\<lambda>obj_id. if obj_id = 0x104
then Some (IRQNode (new_irq_node ntfn_id))
else if 0x100 \<le> obj_id \<and> obj_id \<le> 0x100 + mask LENGTH(irq_len)
then (Some (IRQNode empty_irq_node))
else None"


lemma
"irq_objects =
(\<lambda>obj_id. if 0x100 \<le> obj_id \<and> obj_id < 0x200
(\<lambda>obj_id. if 0x100 \<le> obj_id \<and> obj_id \<le> 0x100 + mask LENGTH(irq_len)
then (Some (IRQNode empty_irq_node))
else None) ++
(\<lambda>obj_id. if obj_id = 0x104 then Some (IRQNode (new_irq_node ntfn_id))
Expand All @@ -193,9 +195,9 @@ definition
frame_a2_id \<mapsto> Frame empty_frame,
frame_b_id \<mapsto> Frame empty_section,
ep_id \<mapsto> Endpoint,
ntfn_id \<mapsto> Notification,
ntfn_id \<mapsto> Notification,
0x104 \<mapsto> IRQNode (new_irq_node ntfn_id),
0x1FE \<mapsto> IRQNode empty_irq_node],
0x13F \<mapsto> IRQNode empty_irq_node],
cdl_cdt = [(cnode_a2_id, 0) \<mapsto> (cnode_extra_id, 1),
(cnode_b_id, 4) \<mapsto> (cnode_extra_id, 1),
(cnode_a2_id, 10) \<mapsto> (cnode_extra_id, 2)], \<comment> \<open>All caps are orig caps,
Expand Down Expand Up @@ -349,7 +351,7 @@ lemma range_example_irq_node:
done

lemma irq_nodes_example_spec:
"irq_nodes example_spec = {obj_id. obj_id = 0x104 \<or> obj_id = 0x1FE}"
"irq_nodes example_spec = {obj_id. obj_id = 0x104 \<or> obj_id = 0x13F}"
by (auto simp: irq_nodes_def example_spec_def object_at_def is_irq_node_def)

(*************************
Expand Down Expand Up @@ -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]:
Expand Down Expand Up @@ -473,7 +475,7 @@ lemma slots_of_example_spec_obj_ids:
lemma irq_handler_cap_example_spec:
"\<lbrakk>is_irqhandler_cap cap; opt_cap (obj_id, slot) example_spec = Some cap\<rbrakk>
\<Longrightarrow> (obj_id = cnode_a2_id \<and> slot = 12) \<or>
(obj_id = cnode_b_id \<and> slot = 254)"
(obj_id = cnode_b_id \<and> 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
Expand All @@ -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 \<and> slot = 12) \<or>
(obj_id = cnode_b_id \<and> slot = 254))"
(obj_id = cnode_b_id \<and> slot = 0x3F))"
apply (clarsimp simp: cap_at_def)
apply (rule iffI)
apply clarsimp
Expand Down Expand Up @@ -678,13 +680,13 @@ lemma real_object_at_example_spec_simp [simp]:
"real_object_at 0xC example_spec"
"real_object_at 0xD example_spec"
"\<not>real_object_at 0x104 example_spec"
"\<not>real_object_at 0x1FE example_spec"
"\<not>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:
Expand Down Expand Up @@ -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)
Expand Down
Loading