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

Jump to bottom

Add select_wp and alternative_wp to wp #661

Merged
merged 2 commits into from
Aug 9, 2023
Merged

Add select_wp and alternative_wp to wp #661

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
a3e8b33
lib/monads: add select_wp and alternative_wp to wp set for Nondet monad
corlewis Aug 1, 2023
2da36ce
proof+autocorres: update for select_wp and alternative_wp
corlewis Aug 1, 2023
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
7 changes: 6 additions & 1 deletion lib/Monads/nondet/Nondet_VCG.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -554,7 +554,7 @@ lemma alternativeE_R_wp:
unfolding validE_R_def
by (rule alternativeE_wp)

lemma alternative_R_wp:
lemma alternativeE_E_wp:
"\<lbrakk> \<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> g -,\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<sqinter> g -, \<lbrace>Q\<rbrace>"
unfolding validE_E_def
by (rule alternativeE_wp)
Expand Down Expand Up @@ -1009,6 +1009,11 @@ lemmas [wp] = hoare_vcg_prop
gets_the_wp
gets_map_wp'
liftE_wp
alternative_wp
alternativeE_R_wp
alternativeE_E_wp
alternativeE_wp
select_wp
select_f_wp
state_select_wp
condition_wp
Expand Down
3 changes: 2 additions & 1 deletion proof/access-control/ADT_AC.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,7 +95,8 @@ lemma do_user_op_respects:
apply (rule dmo_device_update_respects_Write)
apply (wpsimp wp: dmo_um_upd_machine_state
dmo_user_memory_update_respects_Write
hoare_vcg_all_lift hoare_vcg_imp_lift)+
hoare_vcg_all_lift hoare_vcg_imp_lift
wp_del: select_wp)+
apply (rule hoare_pre_cont)
apply (wpsimp wp: select_wp)+
Comment on lines -98 to 101
Copy link
Member Author

Choose a reason for hiding this comment

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

There's a few places like this where existing proofs made use of the fact that select_wp wasn't in the wp set and were broken by this change. I could probably restructure the proof to avoid this but for now I've just deleted select_wp wherever required for the original proofs to continue working.

Copy link
Member

Choose a reason for hiding this comment

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

It looks like you were right and this situation is the rare one, so this is fine by me.

Copy link
Member

Choose a reason for hiding this comment

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

I agree

apply (simp add: restrict_map_def split: if_splits)
Expand Down
3 changes: 1 addition & 2 deletions proof/access-control/ARM/ArchArch_AC.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -826,8 +826,7 @@ lemma decode_arch_invocation_authorised:
apply (rule hoare_pre)
apply (simp add: split_def Let_def split del: if_split
cong: cap.case_cong arch_cap.case_cong if_cong option.case_cong)
apply (wp select_wp whenE_throwError_wp check_vp_wpR
find_pd_for_asid_authority2
apply (wp whenE_throwError_wp check_vp_wpR find_pd_for_asid_authority2
| wpc
| simp add: authorised_asid_control_inv_def authorised_page_inv_def
authorised_page_directory_inv_def
Expand Down
2 changes: 1 addition & 1 deletion proof/access-control/ARM/ArchCNode_AC.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ crunches set_cdt

crunches prepare_thread_delete, arch_finalise_cap
for cur_domain[CNode_AC_assms, wp]:"\<lambda>s. P (cur_domain s)"
(wp: crunch_wps select_wp hoare_vcg_if_lift2 simp: unless_def)
(wp: crunch_wps hoare_vcg_if_lift2 simp: unless_def)

lemma state_vrefs_tcb_upd[CNode_AC_assms]:
"tcb_at t s \<Longrightarrow> state_vrefs (s\<lparr>kheap := kheap s(t \<mapsto> TCB tcb)\<rparr>) = state_vrefs s"
Expand Down
4 changes: 2 additions & 2 deletions proof/access-control/CNode_AC.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1522,10 +1522,10 @@ lemma post_cap_deletion_cur_domain[wp]:
by (wpsimp simp: post_cap_deletion_def)

crunch cur_domain[wp]: cap_swap_for_delete, empty_slot "\<lambda>s. P (cur_domain s)"
(wp: crunch_wps select_wp hoare_vcg_if_lift2 simp: unless_def)
(wp: crunch_wps hoare_vcg_if_lift2 simp: unless_def)

crunch cur_domain[wp]: finalise_cap "\<lambda>s. P (cur_domain s)"
(wp: crunch_wps select_wp hoare_vcg_if_lift2 simp: unless_def)
(wp: crunch_wps hoare_vcg_if_lift2 simp: unless_def)

lemma rec_del_cur_domain[wp]:
"rec_del call \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace>"
Expand Down
6 changes: 3 additions & 3 deletions proof/access-control/DomainSepInv.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -439,7 +439,7 @@ lemma reply_cancel_ipc_domain_sep_inv[wp]:
reply_cancel_ipc t
\<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>"
apply (simp add: reply_cancel_ipc_def)
apply (wp select_wp)
apply wp
apply (rule hoare_strengthen_post[OF thread_set_tcb_fault_update_domain_sep_inv])
apply auto
done
Expand Down Expand Up @@ -553,7 +553,7 @@ lemma cap_revoke_domain_sep_inv':
apply (wp drop_spec_validE[OF valid_validE[OF preemption_point_domain_sep_inv]]
drop_spec_validE[OF valid_validE[OF cap_delete_domain_sep_inv]]
drop_spec_validE[OF assertE_wp] drop_spec_validE[OF returnOk_wp]
drop_spec_validE[OF liftE_wp] select_wp
drop_spec_validE[OF liftE_wp]
| simp | wp (once) hoare_drop_imps)+
done
qed
Expand Down Expand Up @@ -1181,7 +1181,7 @@ lemma handle_event_domain_sep_inv:
lemma schedule_domain_sep_inv:
"(schedule :: (unit,det_ext) s_monad) \<lbrace>domain_sep_inv irqs (st :: 'state_ext state)\<rbrace>"
apply (simp add: schedule_def allActiveTCBs_def)
apply (wp add: alternative_wp select_wp guarded_switch_to_lift hoare_drop_imps
apply (wp add: guarded_switch_to_lift hoare_drop_imps
del: ethread_get_wp
| wpc | clarsimp simp: get_thread_state_def thread_get_def trans_state_update'[symmetric]
schedule_choose_new_thread_def)+
Expand Down
8 changes: 4 additions & 4 deletions proof/access-control/Finalise_AC.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -347,7 +347,7 @@ lemma reply_cancel_ipc_pas_refined[wp]:
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: reply_cancel_ipc_def)
apply (wp add: select_wp wp_transferable del: wp_not_transferable)
apply (wp add: wp_transferable del: wp_not_transferable)
apply (rule hoare_strengthen_post[where Q="\<lambda>_. invs and tcb_at t and pas_refined aag"])
apply (wpsimp wp: hoare_wp_combs thread_set_tcb_fault_reset_invs thread_set_pas_refined)+
apply (frule(1) reply_cap_descends_from_master0)
Expand All @@ -368,7 +368,7 @@ crunches suspend
for pspace_aligned[wp]: "\<lambda>s :: det_ext state. pspace_aligned s"
and valid_vspace_objs[wp]: "\<lambda>s :: det_ext state. valid_vspace_objs s"
and valid_arch_state[wp]: "\<lambda>s :: det_ext state. valid_arch_state s"
(wp: dxo_wp_weak select_wp hoare_drop_imps simp: crunch_simps)
(wp: dxo_wp_weak hoare_drop_imps simp: crunch_simps)

crunch pas_refined[wp]: suspend "pas_refined aag"

Expand Down Expand Up @@ -528,7 +528,7 @@ lemma reply_cancel_ipc_respects[wp]:
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: reply_cancel_ipc_def)
apply (rule hoare_pre)
apply (wp add: select_wp wp_transferable del:wp_not_transferable)
apply (wp add: wp_transferable del:wp_not_transferable)
apply simp
apply (rule hoare_lift_Pf2[where f="cdt"])
apply (wpsimp wp: hoare_vcg_const_Ball_lift thread_set_integrity_autarch
Expand Down Expand Up @@ -1231,7 +1231,7 @@ proof (induct rule: cap_revoke.induct)
apply (subst cap_revoke.simps)
apply (unfold P_def)
apply (wp "1.hyps"[unfolded P_def], simp+)
apply (wp preemption_point_inv hoare_drop_imps select_wp
apply (wp preemption_point_inv hoare_drop_imps
rec_del_preserves_cte_zombie_null_insts[where P=Q]
| simp add: Q_Null Q_Zombie)+
done
Expand Down
2 changes: 1 addition & 1 deletion proof/access-control/Ipc_AC.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ lemma send_signal_caps_of_state[wp]:
done

crunch mdb[wp]: blocked_cancel_ipc, update_waiting_ntfn "\<lambda>s. P (cdt (s :: det_ext state))"
(wp: crunch_wps unless_wp select_wp dxo_wp_weak simp: crunch_simps)
(wp: crunch_wps unless_wp dxo_wp_weak simp: crunch_simps)

lemma cancel_ipc_receive_blocked_mdb:
"\<lbrace>\<lambda>s :: det_ext state. P (cdt s) \<and> st_tcb_at receive_blocked t s\<rbrace>
Expand Down
2 changes: 1 addition & 1 deletion proof/access-control/RISCV64/ArchCNode_AC.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,7 @@ crunches set_cdt

crunches prepare_thread_delete, arch_finalise_cap
for cur_domain[CNode_AC_assms, wp]:"\<lambda>s. P (cur_domain s)"
(wp: crunch_wps select_wp hoare_vcg_if_lift2 simp: unless_def)
(wp: crunch_wps hoare_vcg_if_lift2 simp: unless_def)

lemma state_vrefs_tcb_upd[CNode_AC_assms]:
"\<lbrakk> pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tcb_at t s \<rbrakk>
Expand Down
29 changes: 14 additions & 15 deletions proof/access-control/Syscall_AC.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -699,7 +699,7 @@ lemma handle_event_integrity:
handle_reply_respects handle_fault_integrity_autarch
handle_interrupt_integrity handle_vm_fault_integrity
handle_reply_pas_refined handle_vm_fault_valid_fault
handle_reply_valid_sched alternative_wp select_wp
handle_reply_valid_sched
hoare_vcg_conj_lift hoare_vcg_all_lift hoare_drop_imps
simp: domain_sep_inv_def
| rule dmo_wp hoare_vcg_E_elim
Expand Down Expand Up @@ -899,7 +899,7 @@ lemma schedule_integrity:
schedule
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: schedule_def)
apply (wpsimp wp: alternative_wp switch_to_thread_respects' select_wp guarded_switch_to_lift
apply (wpsimp wp: switch_to_thread_respects' guarded_switch_to_lift
switch_to_idle_thread_respects choose_thread_respects gts_wp hoare_drop_imps
set_scheduler_action_cnt_valid_sched append_thread_queued enqueue_thread_queued
tcb_sched_action_enqueue_valid_blocked_except tcb_sched_action_append_integrity'
Expand Down Expand Up @@ -949,14 +949,14 @@ crunch pas_refined[wp]: choose_thread "pas_refined aag"
lemma schedule_pas_refined:
"schedule \<lbrace>pas_refined aag\<rbrace>"
apply (simp add: schedule_def allActiveTCBs_def)
apply (wp add: alternative_wp guarded_switch_to_lift switch_to_thread_pas_refined select_wp
switch_to_idle_thread_pas_refined gts_wp
guarded_switch_to_lift switch_to_thread_respects_pasMayEditReadyQueues
choose_thread_respects_pasMayEditReadyQueues
next_domain_valid_sched next_domain_valid_queues gts_wp hoare_drop_imps
set_scheduler_action_cnt_valid_sched enqueue_thread_queued
tcb_sched_action_enqueue_valid_blocked_except
del: ethread_get_wp
apply (wp add: guarded_switch_to_lift switch_to_thread_pas_refined
switch_to_idle_thread_pas_refined gts_wp
guarded_switch_to_lift switch_to_thread_respects_pasMayEditReadyQueues
choose_thread_respects_pasMayEditReadyQueues
next_domain_valid_sched next_domain_valid_queues gts_wp hoare_drop_imps
set_scheduler_action_cnt_valid_sched enqueue_thread_queued
tcb_sched_action_enqueue_valid_blocked_except
del: ethread_get_wp
| wpc | simp add: schedule_choose_new_thread_def)+
done

Expand All @@ -983,7 +983,7 @@ lemma ct_active_update[simp]:
lemma set_cap_ct_active[wp]:
"set_cap ptr c \<lbrace>ct_active \<rbrace>"
apply (rule hoare_pre)
apply (wps | wpsimp wp: select_wp sts_st_tcb_at_cases thread_set_no_change_tcb_state
apply (wps | wpsimp wp: sts_st_tcb_at_cases thread_set_no_change_tcb_state
simp: crunch_simps ct_in_state_def)+
done

Expand Down Expand Up @@ -1034,7 +1034,7 @@ crunch ct_active[wp]: post_cap_deletion, empty_slot "\<lambda>s :: det_ext state
wp: crunch_wps filterM_preserved unless_wp)

crunch cur_thread[wp]: cap_swap_for_delete, finalise_cap "\<lambda>s :: det_ext state. P (cur_thread s)"
(wp: select_wp dxo_wp_weak crunch_wps simp: crunch_simps)
(wp: dxo_wp_weak crunch_wps simp: crunch_simps)

lemma rec_del_cur_thread[wp]:
"rec_del a \<lbrace>\<lambda>s :: det_ext state. P (cur_thread s)\<rbrace>"
Expand Down Expand Up @@ -1139,8 +1139,7 @@ lemma call_kernel_integrity':
apply (simp add: call_kernel_def)
apply (simp only: spec_valid_def)
apply (wpsimp wp: activate_thread_respects schedule_integrity_pasMayEditReadyQueues
handle_interrupt_integrity dmo_wp alternative_wp
select_wp handle_interrupt_pas_refined)
handle_interrupt_integrity dmo_wp handle_interrupt_pas_refined)
apply (clarsimp simp: if_fun_split)
apply (rule_tac Q="\<lambda>rv ms. (rv \<noteq> None \<longrightarrow> the rv \<notin> non_kernel_IRQs) \<and>
R True (domain_sep_inv (pasMaySendIrqs aag) st' s) rv ms"
Expand Down Expand Up @@ -1182,7 +1181,7 @@ lemma call_kernel_pas_refined:
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (simp add: call_kernel_def )
apply (wp activate_thread_pas_refined schedule_pas_refined handle_interrupt_pas_refined
do_machine_op_pas_refined dmo_wp alternative_wp select_wp hoare_drop_imps getActiveIRQ_inv
do_machine_op_pas_refined dmo_wp hoare_drop_imps getActiveIRQ_inv
| simp add: if_fun_split
| strengthen invs_psp_aligned invs_vspace_objs invs_arch_state)+
apply (wp he_invs handle_event_pas_refined)
Expand Down
2 changes: 1 addition & 1 deletion proof/bisim/Syscall_S.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -699,7 +699,7 @@ lemma schedule_separate_state [wp]:
"\<lbrace>separate_state\<rbrace> schedule :: (unit,unit) s_monad \<lbrace>\<lambda>_. separate_state\<rbrace>"
unfolding schedule_def switch_to_thread_def arch_switch_to_thread_def
switch_to_idle_thread_def arch_switch_to_idle_thread_def allActiveTCBs_def
by (wpsimp wp: select_inv separate_state_pres' alternative_wp
by (wpsimp wp: select_inv separate_state_pres'
simp: arch_activate_idle_thread_def |
strengthen imp_consequent)+

Expand Down
18 changes: 9 additions & 9 deletions proof/capDL-api/Arch_DP.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,9 +65,9 @@ lemma decode_page_map_intent_rv_20_24:
\<lbrace>\<lambda>r s. R r\<rbrace>, -"
apply (simp add: decode_invocation_def get_index_def get_page_intent_def throw_opt_def
cap_rights_def decode_page_invocation_def throw_on_none_def get_mapped_asid_def)
apply (wp alternativeE_wp select_wp | wpc)+
apply (wp | wpc)+
apply (rule validE_validE_R)
apply (wp alternativeE_wp)
apply wp
apply (simp add:cdl_page_mapping_entries_def split del:if_split | wp | wpc)+
apply auto
done
Expand All @@ -86,9 +86,9 @@ lemma decode_page_map_intent_rv_16_12:
get_page_intent_def throw_opt_def cap_rights_def
decode_page_invocation_def throw_on_none_def
get_mapped_asid_def)
apply (wp alternativeE_wp select_wp)
apply wp
apply (rule validE_validE_R)
apply (wp alternativeE_wp)
apply wp
apply (simp add:cdl_page_mapping_entries_def)
apply (wp cdl_lookup_pt_slot_rv | wpc | simp)+
apply auto
Expand Down Expand Up @@ -130,13 +130,13 @@ lemma invoke_page_table_wp:
done

crunch cdl_cur_thread[wp]: invoke_page "\<lambda>s. P (cdl_current_thread s)"
(wp: crunch_wps select_wp alternative_wp simp : swp_def )
(wp: crunch_wps simp: swp_def)

crunch cdl_cur_thread[wp]: invoke_page_table "\<lambda>s. P (cdl_current_thread s)"
(wp: crunch_wps select_wp alternative_wp simp : swp_def )
(wp: crunch_wps simp: swp_def)

crunch cdl_cur_domain[wp]: invoke_page_table, invoke_page "\<lambda>s. P (cdl_current_domain s)"
(wp: crunch_wps select_wp alternative_wp simp : swp_def unless_def)
(wp: crunch_wps simp: swp_def unless_def)

lemmas cap_asid_simps[simp] = cap_asid_def[split_simps cdl_cap.split]
lemmas cap_mapped_simps[simp] = cap_mapped_def[split_simps cdl_cap.split]
Expand All @@ -153,7 +153,7 @@ lemma decode_page_table_rv:
apply (simp add:decode_invocation_def get_page_table_intent_def
throw_opt_def decode_page_table_invocation_def)
apply (rule hoare_pre)
apply (wp alternativeE_wp throw_on_none_wp | wpc | simp)+
apply (wp throw_on_none_wp | wpc | simp)+
apply (clarsimp split:option.splits simp:get_index_def cap_object_def
cap_has_object_def get_mapped_asid_def)
done
Expand Down Expand Up @@ -564,7 +564,7 @@ lemma decode_invocation_asid_pool_assign:
decode_asid_pool_invocation_def get_index_def
throw_opt_def throw_on_none_def)
apply (rule validE_validE_R)
apply (wp alternativeE_wp select_wp)
apply wp
apply (clarsimp simp:cap_object_def cap_has_object_def)
done

Expand Down
2 changes: 1 addition & 1 deletion proof/capDL-api/CNode_DP.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ lemma invoke_cnode_insert_cdl_current_domain[wp]:
\<lbrace>\<lambda>_ s. P (cdl_current_domain s) \<rbrace>"
apply (simp add: invoke_cnode_def)
apply (rule hoare_pre)
apply (wp alternative_wp | wpc | clarsimp)+
apply (wp | wpc | clarsimp)+
done

lemma invoke_cnode_move_cdl_current_domain[wp]:
Expand Down
9 changes: 4 additions & 5 deletions proof/capDL-api/IRQ_DP.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,6 @@ lemma invoke_irq_handler_set_handler_wp:
invoke_irq_handler (SetIrqHandler irq cap slot)
\<lbrace>\<lambda>_. < irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R> \<rbrace>"
apply (clarsimp simp: invoke_irq_handler_def, wp)
apply (wp alternative_wp)
apply (wp sep_wp: insert_cap_child_wp insert_cap_sibling_wp)+
apply (sep_wp delete_cap_simple_format[where cap=cap'])+
apply (safe)
Expand All @@ -71,7 +70,7 @@ lemma decode_invocation_irq_ack_rv':
decode_irq_handler_invocation cap cap_ref caps (IrqHandlerAckIntent)
\<lbrace>P\<rbrace>, -"
apply (clarsimp simp: decode_irq_handler_invocation_def)
apply (wp alternativeE_R_wp)
apply wp
apply (clarsimp)
done

Expand All @@ -80,7 +79,7 @@ lemma decode_invocation_irq_clear_rv':
decode_irq_handler_invocation cap cap_ref caps (IrqHandlerClearIntent)
\<lbrace>P\<rbrace>, -"
apply (clarsimp simp: decode_irq_handler_invocation_def)
apply (wp alternativeE_R_wp)
apply wp
apply (clarsimp)
done

Expand All @@ -105,7 +104,7 @@ decode_irq_handler_invocation cap cap_ref caps (IrqHandlerSetEndpointIntent)
\<lbrace>P\<rbrace>, -"
apply (rule validE_R_gen_asm_conj)
apply (clarsimp simp: decode_irq_handler_invocation_def)
apply (wp alternativeE_R_wp | wpc)+
apply (wp | wpc)+
apply (clarsimp split: cdl_cap.splits, safe)
apply ((wp throw_on_none_rv)+, clarsimp simp: get_index_def)
apply simp
Expand All @@ -117,7 +116,7 @@ lemma decode_irq_control_issue_irq_rv:
<\<box> (r, (unat depth)) : root_cap index \<mapsto>u cap \<and>* R> s\<rbrace>
decode_irq_control_invocation target target_ref caps (IrqControlIssueIrqHandlerIntent irq index depth) \<lbrace>P\<rbrace>, -"
apply (clarsimp simp: decode_irq_control_invocation_def)
apply (wp alternativeE_R_wp lookup_slot_for_cnode_op_rvu'[where cap=cap and r=r] throw_on_none_rv)
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
Expand Down
Loading
Loading