Skip to content

Commit

Permalink
capDL-api: seplogic lemmas for ARMIssueSGISignal
Browse files Browse the repository at this point in the history
Add separation logic specification lemmas for the new SGISignalCap API
for later use in sys-init.

Signed-off-by: Gerwin Klein <[email protected]>
  • Loading branch information
lsf37 committed Mar 15, 2024
1 parent 39666e4 commit 5b40e6f
Show file tree
Hide file tree
Showing 2 changed files with 169 additions and 0 deletions.
157 changes: 157 additions & 0 deletions proof/capDL-api/IRQ_DP.thy
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,29 @@ lemma decode_irq_control_issue_irq_rv:
apply sep_solve
done

lemma invoke_irq_control_issue_sgi_wp:
"\<lbrace> <dest_slot \<mapsto>c cap \<and>* R> \<rbrace>
invoke_irq_control (ArchIssueIrqHandler (ARMIssueSGISignal irq targets control_slot dest_slot))
\<lbrace>\<lambda>_. <dest_slot \<mapsto>c SGISignalCap irq targets \<and>* R> \<rbrace>"
by (clarsimp simp: invoke_irq_control_def arch_invoke_irq_control_def cap_type_def |
wp sep_wp: insert_cap_child_wp | sep_solve)+

lemma decode_irq_control_issue_sgi_rv:
"\<lbrace>\<lambda>s. P (ArchIssueIrqHandler
(ARMIssueSGISignal (ucast irq) (ucast cpus) target_ref
(cap_object root_cap, offset index r))) s \<and>
caps = (root_cap, root_ptr) # xs \<and> unat depth \<le> word_bits \<and> 0 < unat depth \<and>
<\<box> (r, (unat depth)) : root_cap index \<mapsto>u cap \<and>* R> s\<rbrace>
decode_irq_control_invocation target target_ref caps
(ArchIrqControlIssueIrqHandlerIntent
(ARMIssueSGISignalIntent irq cpus index depth))
\<lbrace>P\<rbrace>, -"
apply (clarsimp simp: decode_irq_control_invocation_def arch_decode_irq_control_invocation_def)
apply (wp lookup_slot_for_cnode_op_rvu'[where cap=cap and r=r] throw_on_none_rv)
apply (clarsimp simp: get_index_def)
apply sep_solve
done

schematic_goal lookup_extra_caps_once_wp:
"\<lbrace>?P\<rbrace> lookup_extra_caps root_tcb_id [endpoint_cptr] \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace>"
apply (clarsimp simp: lookup_extra_caps_def mapME_def sequenceE_def, wp)
Expand Down Expand Up @@ -256,6 +279,140 @@ lemma seL4_IRQHandler_IRQControl_Get:
apply (clarsimp simp: is_irqcontrol_cap_def ep_related_cap_def)
done

lemma seL4_IssueSGISignal_helper:
assumes unify: "irq_cap = SGISignalCap (ucast irq) (ucast targets) \<and>
target_index = offset node_index root_size \<and>
root_index = offset croot root_size \<and>
control_index = offset control_cap root_size \<and>
target_ptr = (cap_object root_cap, target_index) \<and>
control_ptr = (cap_object root_cap, control_index) \<and>
root_ptr = (cap_object root_cap, root_index) \<and>
root_tcb = Tcb t"
shows
"\<lbrace>\<guillemotleft>root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
cap_object root_cap \<mapsto>f CNode (empty_cnode root_size) \<and>*
(root_tcb_id, tcb_cspace_slot) \<mapsto>c root_cap \<and>* control_ptr \<mapsto>c c_cap \<and>*
target_ptr \<mapsto>c target_cap \<and>* root_ptr \<mapsto>c root_cap \<and>* R\<guillemotright> and
K (\<not> ep_related_cap c_cap \<and> one_lvl_lookup root_cap word_bits root_size \<and>
one_lvl_lookup root_cap (unat node_depth) root_size \<and>
guard_equal root_cap node_index (unat node_depth) \<and>
guard_equal root_cap croot word_bits \<and>
guard_equal root_cap control_cap word_bits \<and>
guard_equal root_cap node_index word_bits \<and>
unat node_depth \<le> word_bits \<and> 0 < unat node_depth \<and>
is_irqcontrol_cap c_cap \<and> is_cnode_cap root_cap \<and> is_cnode_cap root_cap)\<rbrace>
seL4_IssueSGISignal control_cap irq targets croot node_index node_depth
\<lbrace>\<lambda>fail. \<guillemotleft>root_tcb_id \<mapsto>f root_tcb \<and>*
(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
\<comment> \<open>Root CNode\<close>
cap_object root_cap \<mapsto>f CNode (empty_cnode root_size) \<and>*
\<comment> \<open>Cap to the root CNode\<close>
(root_tcb_id, tcb_cspace_slot) \<mapsto>c root_cap \<and>*
control_ptr \<mapsto>c c_cap \<and>* target_ptr \<mapsto>c irq_cap \<and>*
root_ptr \<mapsto>c root_cap \<and>* R\<guillemotright>\<rbrace>"
apply (simp add: seL4_IssueSGISignal_def sep_state_projection2_def)
apply (wp do_kernel_op_pull_back)
apply (rule call_kernel_with_intent_allow_error_helper[where
check = True and
Perror = \<top> and
intent_op = "IrqControlIntent
(ArchIrqControlIssueIrqHandlerIntent
(ARMIssueSGISignalIntent irq targets node_index node_depth))" and
tcb = t and
intent_cptr = control_cap and
intent_extra = "[croot]", simplified])
apply clarsimp
apply (rule set_cap_wp[sep_wand_wp])
apply (rule mark_tcb_intent_error_sep_inv)
apply (wp corrupt_ipc_buffer_sep_inv)+
apply (rule_tac P = "iv = InvokeIrqControl
(ArchIssueIrqHandler
(ARMIssueSGISignal (ucast irq) (ucast targets) control_ptr
(cap_object root_cap,
offset node_index root_size)))"
in hoare_gen_asmEx)
apply (clarsimp simp: unify)
apply (wp invoke_irq_control_issue_sgi_wp[sep_wand_wp])
apply (wp set_cap_wp[sep_wand_wp])
apply (rule_tac P = "c=IrqControlCap" in hoare_gen_asmEx, simp)
apply (simp add: decode_invocation_def, wp)
apply (rule_tac P = "irq_control_intent =
ArchIrqControlIssueIrqHandlerIntent
(ARMIssueSGISignalIntent irq targets node_index node_depth)"
in hoare_gen_asmE, simp)
apply (wp decode_irq_control_issue_sgi_rv[where root_cap = root_cap and
root_ptr = root_ptr and
xs = "[]" and r = root_size, simplified])
apply (simp add: throw_opt_def get_irq_control_intent_def)
apply wp
apply (rule lookup_extra_caps_once_wp[where cap'=root_cap and r=root_size, simplified user_pointer_at_def])
apply (rule lookup_cap_and_slot_rvu[where cap'=c_cap and r=root_size, simplified user_pointer_at_def])
apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift update_thread_intent_update)
apply clarsimp
apply (rule conjI, fastforce)+
apply sep_solve
apply (intro impI conjI allI; clarsimp)
apply (intro impI conjI allI; clarsimp simp: unify)
apply sep_solve
apply sep_cancel+
apply (intro impI conjI allI; sep_solve)
apply fastforce
apply (metis is_cnode_cap_not_memory_cap not_memory_cap_reset_asid')
apply fastforce
apply (clarsimp simp: user_pointer_at_def Let_def)
apply sep_solve
apply (drule (1) reset_cap_asid_control, clarsimp simp: is_irqcontrol_cap_def)
apply (clarsimp simp: user_pointer_at_def Let_def)
apply sep_solve
apply (drule reset_cap_asid_ep_related_cap)
apply clarsimp
apply (clarsimp simp: user_pointer_at_def Let_def unify)
apply sep_solve
apply (clarsimp simp: unify)
apply sep_solve
done

lemma seL4_IssueSGISignal_Get:
"\<lbrace>\<guillemotleft>root_tcb_id \<mapsto>f root_tcb \<and>*
(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>*
cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>*
(cnode_id, control_index) \<mapsto>c IrqControlCap \<and>*
(cnode_id, root_index) \<mapsto>c cnode_cap \<and>*
(cnode_id, target_index) \<mapsto>c target_cap \<and>* R\<guillemotright>
and K (is_tcb root_tcb \<and>
is_cnode_cap cnode_cap \<and>
is_cnode_cap cnode_cap \<and>
cnode_id = cap_object cnode_cap \<and>
target_index = offset node_index root_size \<and>
root_index = offset croot root_size \<and>
control_index = offset control_cap root_size \<and>
one_lvl_lookup cnode_cap word_bits root_size \<and>
one_lvl_lookup cnode_cap (unat node_depth) root_size \<and>
guard_equal cnode_cap node_index (unat node_depth) \<and>
guard_equal cnode_cap croot word_bits \<and>
guard_equal cnode_cap control_cap word_bits \<and>
guard_equal cnode_cap node_index word_bits \<and>
unat node_depth \<le> word_bits \<and> 0 < unat node_depth)\<rbrace>
seL4_IssueSGISignal control_cap irq targets croot node_index node_depth
\<lbrace>\<lambda>fail.
\<guillemotleft>root_tcb_id \<mapsto>f root_tcb \<and>*
(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
\<comment> \<open>Cap to the root CNode\<close>
(root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>*
\<comment> \<open>Root CNode\<close>
cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>*
(cnode_id, control_index) \<mapsto>c IrqControlCap \<and>*
(cnode_id, root_index) \<mapsto>c cnode_cap \<and>*
(cnode_id, target_index) \<mapsto>c SGISignalCap (ucast irq) (ucast targets) \<and>* R\<guillemotright>\<rbrace>"
apply (rule hoare_gen_asm, elim conjE)
apply (sep_wp seL4_IssueSGISignal_helper [where t="obj_tcb root_tcb"])
apply fastforce
apply clarsimp
apply (rule conjI, sep_solve)
apply (clarsimp simp: is_irqcontrol_cap_def ep_related_cap_def)
done

lemma seL4_IRQHandler_SetEndpoint_wp_helper:
assumes unify: "irq_cap = IrqHandlerCap irq \<and>
offset endpoint_cptr root_size = irq_handler_slot \<and>
Expand Down
12 changes: 12 additions & 0 deletions proof/capDL-api/Kernel_DP.thy
Original file line number Diff line number Diff line change
Expand Up @@ -178,6 +178,18 @@ where
cdl_intent_extras = [croot],
cdl_intent_recv_slot = None\<rparr> True"

definition seL4_IssueSGISignal ::
"cdl_cptr \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> cdl_cptr \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> bool u_monad"
where
"seL4_IssueSGISignal control_cap irq targets croot node_index node_depth \<equiv>
do_kernel_op $ call_kernel_with_intent
\<lparr>cdl_intent_op = Some $ IrqControlIntent $ ArchIrqControlIssueIrqHandlerIntent $
ARMIssueSGISignalIntent irq targets node_index node_depth,
cdl_intent_error = False,
cdl_intent_cap = control_cap,
cdl_intent_extras = [croot],
cdl_intent_recv_slot = None\<rparr> True"

definition seL4_IRQHandler_SetEndpoint :: "cdl_cptr \<Rightarrow> cdl_cptr \<Rightarrow> bool u_monad"
where
"seL4_IRQHandler_SetEndpoint handler_cap endpoint_cap \<equiv>
Expand Down

0 comments on commit 5b40e6f

Please sign in to comment.