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

Update ARM AInvs for det_ext changes #844

Merged
merged 1 commit into from
Dec 19, 2024
Merged

Update ARM AInvs for det_ext changes #844

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
37 changes: 6 additions & 31 deletions proof/invariant-abstract/ARM/ArchBCorres2_AI.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,11 +15,11 @@ named_theorems BCorres2_AI_assms

crunch invoke_cnode
for (bcorres) bcorres[wp, BCorres2_AI_assms]: truncate_state
(simp: swp_def ignore: clearMemory without_preemption filterM ethread_set )
(simp: swp_def ignore: clearMemory without_preemption filterM)

crunch create_cap,init_arch_objects,retype_region,delete_objects
for (bcorres) bcorres[wp]: truncate_state
(ignore: freeMemory clearMemory retype_region_ext)
(ignore: freeMemory clearMemory)

crunch set_extra_badge,derive_cap
for (bcorres) bcorres[wp]: truncate_state (ignore: storeWord)
Expand All @@ -28,7 +28,7 @@ crunch invoke_untyped
for (bcorres) bcorres[wp]: truncate_state
(ignore: sequence_x)

crunch set_mcpriority,
crunch set_mcpriority, set_priority,
arch_get_sanitise_register_info, arch_post_modify_registers
for (bcorres) bcorres[wp, BCorres2_AI_assms]: truncate_state

Expand Down Expand Up @@ -74,10 +74,6 @@ lemma handle_arch_fault_reply_bcorres[wp,BCorres2_AI_assms]:
"bcorres ( handle_arch_fault_reply a b c d) (handle_arch_fault_reply a b c d)"
by (cases a; simp add: handle_arch_fault_reply_def; wp)

crunch
arch_switch_to_thread,arch_switch_to_idle_thread
for (bcorres) bcorres[wp, BCorres2_AI_assms]: truncate_state

end

interpretation BCorres2_AI?: BCorres2_AI
Expand All @@ -86,11 +82,9 @@ interpretation BCorres2_AI?: BCorres2_AI
case 1 show ?case by (unfold_locales; (fact BCorres2_AI_assms)?)
qed

lemmas schedule_bcorres[wp] = schedule_bcorres1[OF BCorres2_AI_axioms]

context Arch begin arch_global_naming

crunch send_ipc,send_signal,do_reply_transfer,arch_perform_invocation
crunch send_ipc,send_signal,do_reply_transfer,arch_perform_invocation,invoke_domain
for (bcorres) bcorres[wp]: truncate_state
(simp: gets_the_def swp_def ignore: freeMemory clearMemory loadWord cap_fault_on_failure
storeWord lookup_error_on_failure getRestartPC getRegister mapME)
Expand Down Expand Up @@ -148,10 +142,8 @@ lemma handle_vm_fault_bcorres[wp]: "bcorres (handle_vm_fault a b) (handle_vm_fau
lemma handle_reserved_irq_bcorres[wp]: "bcorres (handle_reserved_irq a) (handle_reserved_irq a)"
by (simp add: handle_reserved_irq_def; wp)

lemma handle_hypervisor_fault_bcorres[wp]: "bcorres (handle_hypervisor_fault a b) (handle_hypervisor_fault a b)"
apply (cases b)
apply (simp | wp)+
done
crunch handle_hypervisor_fault, timer_tick
for (bcorres) bcorres[wp]: truncate_state

lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)"
apply (cases e)
Expand All @@ -160,23 +152,6 @@ lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)"
| intro impI conjI allI | wp | wpc)+
done

crunch guarded_switch_to,switch_to_idle_thread
for (bcorres) bcorres[wp]: truncate_state (ignore: storeWord clearExMonitor)

lemma choose_switch_or_idle:
"((), s') \<in> fst (choose_thread s) \<Longrightarrow>
(\<exists>word. ((),s') \<in> fst (guarded_switch_to word s)) \<or>
((),s') \<in> fst (switch_to_idle_thread s)"
apply (simp add: choose_thread_def)
apply (clarsimp simp add: switch_to_idle_thread_def bind_def gets_def
arch_switch_to_idle_thread_def in_monad
return_def get_def modify_def put_def
get_thread_state_def
thread_get_def
split: if_split_asm)
apply force
done

end

end
142 changes: 34 additions & 108 deletions proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,118 +12,59 @@ context Arch begin arch_global_naming

named_theorems DetSchedAux_AI_assms

lemma set_pd_etcbs[wp]:
"set_pd p pd \<lbrace>\<lambda>s. P (etcbs_of s)\<rbrace>"
unfolding set_pd_def
apply (wpsimp wp: set_object_wp_strong)
by (auto elim!: rsubst[where P=P] simp: etcbs_of'_def obj_at_def a_type_def
split: kernel_object.splits)

crunch init_arch_objects
for exst[wp]: "\<lambda>s. P (exst s)"
and ct[wp]: "\<lambda>s. P (cur_thread s)"
and valid_etcbs[wp, DetSchedAux_AI_assms]: valid_etcbs
(wp: crunch_wps unless_wp valid_etcbs_lift)

crunch invoke_untyped
for ct[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (cur_thread s)"
(wp: crunch_wps dxo_wp_weak preemption_point_inv mapME_x_inv_wp
simp: crunch_simps do_machine_op_def detype_def mapM_x_defsym unless_def
ignore: freeMemory retype_region_ext)
crunch invoke_untyped
for ready_queues[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (ready_queues s)"
(wp: crunch_wps mapME_x_inv_wp preemption_point_inv'
simp: detype_def detype_ext_def crunch_simps
wrap_ext_det_ext_ext_def mapM_x_defsym
ignore: freeMemory)
crunch invoke_untyped
for scheduler_action[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (scheduler_action s)"
(wp: crunch_wps mapME_x_inv_wp preemption_point_inv'
simp: detype_def detype_ext_def crunch_simps
wrap_ext_det_ext_ext_def mapM_x_defsym
ignore: freeMemory)
crunch invoke_untyped
for cur_domain[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (cur_domain s)"
(wp: crunch_wps mapME_x_inv_wp preemption_point_inv'
simp: detype_def detype_ext_def crunch_simps
wrap_ext_det_ext_ext_def mapM_x_defsym
ignore: freeMemory)
crunch invoke_untyped
for idle_thread[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (idle_thread s)"
(wp: crunch_wps mapME_x_inv_wp preemption_point_inv dxo_wp_weak
simp: detype_def detype_ext_def crunch_simps
wrap_ext_det_ext_ext_def mapM_x_defsym
ignore: freeMemory retype_region_ext)
and etcbs_of[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (etcbs_of s)"
and ready_queues[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (ready_queues s)"
and idle_thread[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (idle_thread s)"
and schedact[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (scheduler_action s)"
and cur_domain[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (cur_domain s)"
(wp: crunch_wps)

lemma tcb_sched_action_valid_idle_etcb:
"\<lbrace>valid_idle_etcb\<rbrace>
tcb_sched_action foo thread
\<lbrace>\<lambda>_. valid_idle_etcb\<rbrace>"
apply (rule valid_idle_etcb_lift)
apply (simp add: tcb_sched_action_def set_tcb_queue_def)
apply (wp | simp)+
done

lemma delete_objects_etcb_at[wp, DetSchedAux_AI_assms]:
"\<lbrace>\<lambda>s::det_ext state. etcb_at P t s\<rbrace> delete_objects a b \<lbrace>\<lambda>r s. etcb_at P t s\<rbrace>"
apply (simp add: delete_objects_def)
apply (wp)
apply (simp add: detype_def detype_ext_def wrap_ext_det_ext_ext_def etcb_at_def|wp)+
done

crunch reset_untyped_cap
for etcb_at[wp]: "etcb_at P t"
(wp: preemption_point_inv' mapME_x_inv_wp crunch_wps
simp: unless_def)

crunch reset_untyped_cap
for valid_etcbs[wp]: "valid_etcbs"
(wp: preemption_point_inv' mapME_x_inv_wp crunch_wps
simp: unless_def)

lemma invoke_untyped_etcb_at [DetSchedAux_AI_assms]:
"\<lbrace>(\<lambda>s :: det_ext state. etcb_at P t s) and valid_etcbs\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. st_tcb_at (Not o inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>"
apply (cases ui)
apply (simp add: mapM_x_def[symmetric] invoke_untyped_def whenE_def
split del: if_split)
apply (wp retype_region_etcb_at mapM_x_wp'
create_cap_no_pred_tcb_at typ_at_pred_tcb_at_lift
hoare_convert_imp[OF create_cap_no_pred_tcb_at]
hoare_convert_imp[OF _ init_arch_objects_exst]
| simp
| (wp (once) hoare_drop_impE_E))+
done
crunch init_arch_objects
for valid_queues[wp]: valid_queues
and valid_sched_action[wp]: valid_sched_action
and valid_sched[wp]: valid_sched
(wp: valid_queues_lift valid_sched_action_lift valid_sched_lift)

lemma tcb_sched_action_valid_idle_etcb:
"tcb_sched_action foo thread \<lbrace>valid_idle_etcb\<rbrace>"
by (rule valid_idle_etcb_lift)
(wpsimp simp: tcb_sched_action_def set_tcb_queue_def)

crunch init_arch_objects
for valid_blocked[wp, DetSchedAux_AI_assms]: valid_blocked
(wp: valid_blocked_lift set_cap_typ_at)
(wp: valid_blocked_lift crunch_wps)

lemma perform_asid_control_etcb_at:"\<lbrace>(\<lambda>s. etcb_at P t s) and valid_etcbs\<rbrace>
perform_asid_control_invocation aci
\<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>"
lemma perform_asid_control_etcb_at:
"\<lbrace>etcb_at P t\<rbrace>
perform_asid_control_invocation aci
\<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>"
apply (simp add: perform_asid_control_invocation_def)
apply (rule hoare_pre)
apply (wp | wpc | simp)+
apply wpsimp
apply (wp hoare_imp_lift_something typ_at_pred_tcb_at_lift)[1]
apply (rule hoare_drop_imps)
apply (wp retype_region_etcb_at)+
apply simp
done

crunch perform_asid_control_invocation
for ct[wp]: "\<lambda>s. P (cur_thread s)"

crunch perform_asid_control_invocation
for idle_thread[wp]: "\<lambda>s. P (idle_thread s)"
and valid_blocked[wp]: valid_blocked
and schedact[wp]: "\<lambda>s. P (scheduler_action s)"
and ready_queues[wp]: "\<lambda>s. P (ready_queues s)"
and cur_domain[wp]: "\<lambda>s. P (cur_domain s)"
(wp: hoare_weak_lift_imp simp: detype_def)

crunch perform_asid_control_invocation
for valid_etcbs[wp]: valid_etcbs (wp: hoare_weak_lift_imp)

crunch perform_asid_control_invocation
for valid_blocked[wp]: valid_blocked (wp: hoare_weak_lift_imp)

crunch perform_asid_control_invocation
for schedact[wp]: "\<lambda>s :: det_ext state. P (scheduler_action s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory)

crunch perform_asid_control_invocation
for rqueues[wp]: "\<lambda>s :: det_ext state. P (ready_queues s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory)

crunch perform_asid_control_invocation
for cur_domain[wp]: "\<lambda>s :: det_ext state. P (cur_domain s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory)
for ct[wp]: "\<lambda>s. P (cur_thread s)"

lemma perform_asid_control_invocation_valid_sched:
"\<lbrace>ct_active and invs and valid_aci aci and valid_sched and valid_idle\<rbrace>
Expand All @@ -143,26 +84,11 @@ lemma perform_asid_control_invocation_valid_sched:
apply simp
done

crunch init_arch_objects
for valid_queues[wp]: valid_queues (wp: valid_queues_lift)

crunch init_arch_objects
for valid_sched_action[wp]: valid_sched_action (wp: valid_sched_action_lift)

crunch init_arch_objects
for valid_sched[wp]: valid_sched (wp: valid_sched_lift)

end

lemmas tcb_sched_action_valid_idle_etcb
= ARM.tcb_sched_action_valid_idle_etcb

global_interpretation DetSchedAux_AI_det_ext?: DetSchedAux_AI_det_ext
proof goal_cases
interpret Arch .
case 1 show ?case by (unfold_locales; (fact DetSchedAux_AI_assms)?)
qed

global_interpretation DetSchedAux_AI?: DetSchedAux_AI
proof goal_cases
interpret Arch .
Expand Down
19 changes: 12 additions & 7 deletions proof/invariant-abstract/ARM/ArchDetSchedDomainTime_AI.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,9 +20,10 @@ crunch
arch_activate_idle_thread, arch_switch_to_thread, arch_switch_to_idle_thread,
handle_arch_fault_reply,
arch_invoke_irq_control, handle_vm_fault, arch_get_sanitise_register_info,
prepare_thread_delete, handle_hypervisor_fault, make_arch_fault_msg,
prepare_thread_delete, handle_hypervisor_fault, make_arch_fault_msg, init_arch_objects,
arch_post_modify_registers, arch_post_cap_deletion, arch_invoke_irq_handler
for domain_list_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s. P (domain_list s)"
for domain_list_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s::det_state. P (domain_list s)"
(wp: crunch_wps)

crunch arch_finalise_cap
for domain_time_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s. P (domain_time s)"
Expand All @@ -34,7 +35,8 @@ crunch
arch_invoke_irq_control, handle_vm_fault, arch_get_sanitise_register_info,
prepare_thread_delete, handle_hypervisor_fault,
arch_post_modify_registers, arch_post_cap_deletion, arch_invoke_irq_handler
for domain_time_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s. P (domain_time s)"
for domain_time_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s::det_state. P (domain_time s)"
(wp: crunch_wps)
declare init_arch_objects_exst[DetSchedDomainTime_AI_assms]
make_arch_fault_msg_inv[DetSchedDomainTime_AI_assms]

Expand All @@ -55,11 +57,11 @@ crunch arch_mask_irq_signal
for domain_list_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s. P (domain_list s)"

crunch arch_perform_invocation
for domain_time_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s. P (domain_time s)"
for domain_time_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s::det_state. P (domain_time s)"
(wp: crunch_wps check_cap_inv)

crunch arch_perform_invocation
for domain_list_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s. P (domain_list s)"
for domain_list_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s::det_state. P (domain_list s)"
(wp: crunch_wps check_cap_inv)

lemma timer_tick_valid_domain_time:
Expand All @@ -68,18 +70,21 @@ lemma timer_tick_valid_domain_time:
\<lbrace>\<lambda>x s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>" (is "\<lbrace> ?dtnot0 \<rbrace> _ \<lbrace> _ \<rbrace>")
unfolding timer_tick_def
supply if_split[split del]
supply ethread_get_wp[wp del]
supply thread_get_wp[wp del]
supply if_apply_def2[simp]
apply (wpsimp
wp: reschedule_required_valid_domain_time hoare_vcg_const_imp_lift gts_wp
(* unless we hit dec_domain_time we know ?dtnot0 holds on the state, so clean up the
postcondition once we hit thread_set_time_slice *)
hoare_post_imp[where Q'="\<lambda>_. ?dtnot0" and Q="\<lambda>_ s. domain_time s = 0 \<longrightarrow> X s"
and f="thread_set_time_slice t ts" for X t ts]
hoare_drop_imp[where f="ethread_get t f" for t f])
hoare_drop_imp[where f="thread_get t f" for t f])
apply fastforce
done

crunch do_machine_op
for domain_time_sched[wp]: "\<lambda>s. P (domain_time s) (scheduler_action s)"

lemma handle_interrupt_valid_domain_time [DetSchedDomainTime_AI_assms]:
"\<lbrace>\<lambda>s :: det_ext state. 0 < domain_time s \<rbrace>
handle_interrupt i
Expand Down
Loading
Loading