adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

ainvs+refine: update proofs for SetTLSBase (VER-807)

This commit is contained in:
Maksym Bortin 2017-12-13 16:03:41 +11:00 committed by Corey Lewis
parent 2b8a2ebfbe
commit 9d315cda20
12 changed files with 331 additions and 162 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
proof/invariant-abstract/ARM/ArchBCorres2_AI.thy
View File

@ -100,8 +100,9 @@ lemma decode_cnode_invocation[wp]: "bcorres (decode_cnode_invocation a b c d) (d
done
crunch (bcorres)bcorres[wp]:
decode_set_ipc_buffer,decode_set_space,decode_set_priority,decode_set_mcpriority,
decode_set_sched_params,decode_bind_notification,decode_unbind_notification truncate_state
decode_set_ipc_buffer, decode_set_space, decode_set_priority,
decode_set_mcpriority, decode_set_sched_params, decode_bind_notification,
decode_unbind_notification, decode_set_tls_base truncate_state
lemma decode_tcb_configure_bcorres[wp]: "bcorres (decode_tcb_configure b (cap.ThreadCap c) d e)
(decode_tcb_configure b (cap.ThreadCap c) d e)"

6
proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy
View File

@ -43,8 +43,10 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault
bool.splits list.splits thread_state.splits split_def catch_def sum.splits
Let_def wp: zipWithM_x_empty_fail)
crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
decode_set_priority, decode_set_mcpriority, decode_set_sched_params
crunch (empty_fail) empty_fail[wp]:
decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
decode_set_priority, decode_set_mcpriority, decode_set_sched_params,
decode_set_tls_base
(simp: cap.splits arch_cap.splits split_def)
lemma decode_tcb_invocation_empty_fail[wp]:

5
proof/invariant-abstract/ARM_HYP/ArchBCorres2_AI.thy
View File

@ -103,8 +103,9 @@ lemma decode_cnode_invocation[wp]: "bcorres (decode_cnode_invocation a b c d) (d
done
crunch (bcorres)bcorres[wp]:
decode_set_ipc_buffer,decode_set_space,decode_set_priority,decode_set_mcpriority,
decode_set_sched_params,decode_bind_notification,decode_unbind_notification truncate_state
decode_set_ipc_buffer, decode_set_space, decode_set_priority,
decode_set_mcpriority, decode_set_sched_params, decode_bind_notification,
decode_unbind_notification, decode_set_tls_base truncate_state
lemma decode_tcb_configure_bcorres[wp]: "bcorres (decode_tcb_configure b (cap.ThreadCap c) d e)
(decode_tcb_configure b (cap.ThreadCap c) d e)"

6
proof/invariant-abstract/ARM_HYP/ArchEmptyFail_AI.thy
View File

@ -43,8 +43,10 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault
bool.splits list.splits thread_state.splits split_def catch_def sum.splits
Let_def wp: zipWithM_x_empty_fail empty_fail_addressTranslateS1CPR)
crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
decode_set_priority, decode_set_mcpriority, decode_set_sched_params
crunch (empty_fail) empty_fail[wp]:
decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
decode_set_priority, decode_set_mcpriority, decode_set_sched_params,
decode_set_tls_base
(simp: cap.splits arch_cap.splits split_def)
crunch (empty_fail) empty_fail[wp]: decode_vcpu_invocation

16
proof/invariant-abstract/DetSchedSchedule_AI.thy
View File

@ -1922,12 +1922,18 @@ crunch it[wp]: suspend "\<lambda> s. P (idle_thread s)"
context DetSchedSchedule_AI begin
lemma invoke_tcb_valid_sched[wp]:
"\<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf ti\<rbrace> invoke_tcb ti \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
"\<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf ti\<rbrace>
invoke_tcb ti
\<lbrace>\<lambda>rv. valid_sched\<rbrace>"
apply (cases ti, simp_all only:)
apply (wp mapM_x_wp | simp | rule subset_refl | rule reschedule_preserves_valid_shed | clarsimp simp:invs_valid_objs invs_valid_global_refs idle_no_ex_cap | intro impI conjI)+
apply (rename_tac option)
apply (case_tac option)
apply (wp mapM_x_wp | simp | rule subset_refl | clarsimp simp:invs_valid_objs invs_valid_global_refs idle_no_ex_cap | intro impI conjI)+
apply (wp mapM_x_wp | simp | rule subset_refl | rule reschedule_preserves_valid_shed |
clarsimp simp:invs_valid_objs invs_valid_global_refs idle_no_ex_cap |
intro impI conjI)+
apply (rename_tac option)
apply (case_tac option)
apply (wp mapM_x_wp | simp | rule subset_refl |
clarsimp simp:invs_valid_objs invs_valid_global_refs idle_no_ex_cap |
rule reschedule_preserves_valid_shed | intro impI conjI)+
done
end

70
proof/invariant-abstract/Tcb_AI.thy
View File

@ -771,6 +771,7 @@ where
\<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) ntfnptr
and ex_nonz_cap_to ntfnptr
and bound_tcb_at (op = None) t) ))"
| "tcb_inv_wf (SetTLSBase t tls_base) = (tcb_at t and ex_nonz_cap_to t)"
end
@ -835,18 +836,19 @@ lemma (in Tcb_AI) tcbinv_invs:
invoke_tcb ti
\<lbrace>\<lambda>rv. invs\<rbrace>"
apply (case_tac ti, simp_all only:)
apply ((wp writereg_invs readreg_invs copyreg_invs tc_invs
| simp
| clarsimp simp: invs_def valid_state_def valid_pspace_def
dest!: idle_no_ex_cap
split: option.split
| rule conjI)+)[6]
apply (rename_tac option)
apply (case_tac option, simp_all)
apply (rule hoare_pre)
apply ((wp unbind_notification_invs get_simple_ko_wp | simp)+)[2]
apply (wp bind_notification_invs)
apply clarsimp
apply ((wp writereg_invs readreg_invs copyreg_invs tc_invs
| simp
| clarsimp simp: invs_def valid_state_def valid_pspace_def
dest!: idle_no_ex_cap
split: option.split
| rule conjI)+)[6]
apply (rename_tac option)
apply (case_tac option, simp_all)
apply (rule hoare_pre)
apply ((wp unbind_notification_invs get_simple_ko_wp | simp)+)[2]
apply (wp bind_notification_invs)
apply clarsimp
apply wpsimp
done
lemma inj_ucast: "\<lbrakk> uc = ucast; is_up uc \<rbrakk> \<Longrightarrow> inj uc"
@ -868,23 +870,31 @@ lemma decode_readreg_inv:
"\<lbrace>P\<rbrace> decode_read_registers args (cap.ThreadCap t) \<lbrace>\<lambda>rv. P\<rbrace>"
apply (rule hoare_pre)
apply (simp add: decode_read_registers_def whenE_def | rule conjI | clarsimp
| wp_once | wpcw)+
| wp_once | wpcw)+
done
lemma decode_writereg_inv:
"\<lbrace>P\<rbrace> decode_write_registers args (cap.ThreadCap t) \<lbrace>\<lambda>rv. P\<rbrace>"
apply (rule hoare_pre)
apply (simp add: decode_write_registers_def whenE_def
split del: if_split
| wp_once | wpcw)+
apply (simp add: decode_write_registers_def whenE_def
split del: if_split
| wp_once | wpcw)+
done
lemma decode_copyreg_inv:
"\<lbrace>P\<rbrace> decode_copy_registers args (cap.ThreadCap t) extras \<lbrace>\<lambda>rv. P\<rbrace>"
apply (rule hoare_pre)
apply (simp add: decode_copy_registers_def whenE_def
split del: if_split
| wp_once | wpcw)+
apply (simp add: decode_copy_registers_def whenE_def
split del: if_split
| wp_once | wpcw)+
done
lemma decode_set_tls_base_inv:
"\<lbrace>P\<rbrace> decode_set_tls_base args (cap.ThreadCap t) \<lbrace>\<lambda>rv. P\<rbrace>"
apply (rule hoare_pre)
apply (simp add: decode_set_tls_base_def whenE_def
split del: if_split
| wp_once | wpcw)+
done
lemma (in Tcb_AI) decode_readreg_wf:
@ -922,6 +932,15 @@ lemma (in Tcb_AI) decode_copyreg_wf:
apply (clarsimp simp: valid_cap_def[where c="cap.ThreadCap t" for t])
done
lemma (in Tcb_AI) decode_set_tls_base_wf:
"\<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace>
decode_set_tls_base args (cap.ThreadCap t)
\<lbrace>tcb_inv_wf\<rbrace>,-"
apply (simp add: decode_set_tls_base_def whenE_def
cong: list.case_cong split del: if_split)
apply wpsimp
done
declare alternativeE_wp[wp]
declare alternativeE_R_wp[wp]
@ -1201,18 +1220,20 @@ lemma decode_bind_notification_inv[wp]:
split_del: if_split)
lemma (in Tcb_AI) decode_tcb_inv_inv:
"\<lbrace>P::'state_ext state \<Rightarrow> bool\<rbrace> decode_tcb_invocation label args (cap.ThreadCap t) slot extras \<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: decode_tcb_invocation_def Let_def
"\<lbrace>P::'state_ext state \<Rightarrow> bool\<rbrace>
decode_tcb_invocation label args (cap.ThreadCap t) slot extras
\<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: decode_tcb_invocation_def Let_def decode_set_tls_base_def
cong: if_cong
split del: if_split)
apply (rule hoare_pre)
apply (wpc
| wp decode_readreg_inv decode_writereg_inv
decode_copyreg_inv decode_tcb_conf_inv)+
decode_copyreg_inv decode_tcb_conf_inv
decode_set_tls_base_inv)+
apply simp
done
lemma real_cte_at_not_tcb_at:
"real_cte_at (x, y) s \<Longrightarrow> \<not> tcb_at x s"
by (clarsimp simp: obj_at_def is_tcb is_cap_table)
@ -1258,7 +1279,8 @@ lemma decode_tcb_inv_wf:
apply wpc
apply (wp decode_tcb_conf_wf decode_readreg_wf
decode_writereg_wf decode_copyreg_wf
decode_bind_notification_wf decode_unbind_notification_wf decode_set_priority_wf)+
decode_bind_notification_wf decode_unbind_notification_wf
decode_set_priority_wf decode_set_tls_base_wf)+
apply (clarsimp simp: real_cte_at_cte)
apply (fastforce simp: real_cte_at_not_tcb_at)
done

5
proof/invariant-abstract/X64/ArchBCorres2_AI.thy
View File

@ -101,7 +101,10 @@ lemma decode_cnode_invocation[wp]: "bcorres (decode_cnode_invocation a b c d) (d
apply (wp | wpc | simp add: split_def | intro impI conjI)+
done
crunch (bcorres)bcorres[wp]: decode_set_ipc_buffer,decode_set_space,decode_set_priority,decode_set_mcpriority,decode_set_sched_params,decode_bind_notification,decode_unbind_notification truncate_state
crunch (bcorres)bcorres[wp]:
decode_set_ipc_buffer, decode_set_space, decode_set_priority,
decode_set_mcpriority, decode_set_sched_params, decode_bind_notification,
decode_unbind_notification, decode_set_tls_base truncate_state
lemma decode_tcb_configure_bcorres[wp]: "bcorres (decode_tcb_configure b (cap.ThreadCap c) d e)
(decode_tcb_configure b (cap.ThreadCap c) d e)"

6
proof/invariant-abstract/X64/ArchEmptyFail_AI.thy
View File

@ -51,8 +51,10 @@ lemma port_in_empty_fail[simp, intro!]:
apply (simp add: port_in_def)
by (wp | simp add: ef)+
crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
decode_set_priority, decode_set_mcpriority, decode_set_sched_params
crunch (empty_fail) empty_fail[wp]:
decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
decode_set_priority, decode_set_mcpriority, decode_set_sched_params,
decode_set_tls_base
(simp: cap.splits arch_cap.splits split_def)
lemma decode_tcb_invocation_empty_fail[wp]:

12
proof/refine/ARM/Orphanage.thy
View File

@ -1970,6 +1970,16 @@ lemma copyreg_no_orphans:
apply (fastforce simp: invs'_def valid_state'_def dest!: global'_no_ex_cap)
done
lemma settlsbase_no_orphans:
"\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
invokeTCB (tcbinvocation.SetTLSBase src dest)
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
unfolding invokeTCB_def performTransfer_def
apply simp
apply (wp hoare_vcg_if_lift static_imp_wp)
apply (wpsimp wp: hoare_vcg_imp_lift' mapM_x_wp' asUser_no_orphans)+
done
lemma almost_no_orphans_no_orphans:
"\<lbrakk> almost_no_orphans t s; \<not> is_active_tcb_ptr t s \<rbrakk> \<Longrightarrow> no_orphans s"
by (auto simp: almost_no_orphans_def no_orphans_def all_active_tcb_ptrs_def)
@ -2072,7 +2082,7 @@ lemma invokeTCB_no_orphans [wp]:
apply (rename_tac option)
apply (case_tac option)
apply ((wp | simp add: invokeTCB_def)+)[2]
apply (wp writereg_no_orphans readreg_no_orphans copyreg_no_orphans | clarsimp)+
apply (wp writereg_no_orphans readreg_no_orphans copyreg_no_orphans settlsbase_no_orphans | clarsimp)+
done
lemma invokeCNode_no_orphans [wp]:

120
proof/refine/ARM/Tcb_R.thy
View File

@ -1607,6 +1607,8 @@ where
= (x = tcbinvocation.Resume a)"
| "tcbinv_relation (tcb_invocation.NotificationControl t ntfnptr) x
= (x = tcbinvocation.NotificationControl t ntfnptr)"
| "tcbinv_relation (tcb_invocation.SetTLSBase ref w) x
= (x = tcbinvocation.SetTLSBase ref w)"
primrec
tcb_inv_wf' :: "tcbinvocation \<Rightarrow> kernel_state \<Rightarrow> bool"
@ -1644,6 +1646,8 @@ where
\<and> (\<forall>q. ntfnObj ko \<noteq> WaitingNtfn q)) ntfnptr
and ex_nonz_cap_to' ntfnptr
and bound_tcb_at' (op = None) t) )"
| "tcb_inv_wf' (tcbinvocation.SetTLSBase ref w)
= (tcb_at' ref and ex_nonz_cap_to' ref)"
lemma tcbinv_corres:
"tcbinv_relation ti ti' \<Longrightarrow>
@ -1652,42 +1656,53 @@ lemma tcbinv_corres:
(invs' and sch_act_simple and tcb_inv_wf' ti')
(invoke_tcb ti) (invokeTCB ti')"
apply (case_tac ti, simp_all only: tcbinv_relation.simps valid_tcb_invocation_def)
apply (rule corres_guard_imp [OF writereg_corres], simp+)[1]
apply (rule corres_guard_imp [OF readreg_corres], simp+)[1]
apply (rule corres_guard_imp [OF copyreg_corres], simp+)[1]
apply (clarsimp simp del: invoke_tcb.simps)
apply (rename_tac word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11)
apply (rule_tac F="is_aligned word 5" in corres_req)
apply (clarsimp simp add: is_aligned_weaken [OF tcb_aligned])
apply (rule corres_guard_imp [OF tc_corres], clarsimp+)
apply (clarsimp simp: is_cnode_or_valid_arch_def
split: option.split option.split_asm)
apply clarsimp
apply (auto split: option.split_asm simp: newroot_rel_def)[1]
apply (rule corres_guard_imp [OF writereg_corres], simp+)[1]
apply (rule corres_guard_imp [OF readreg_corres], simp+)[1]
apply (rule corres_guard_imp [OF copyreg_corres], simp+)[1]
apply (clarsimp simp del: invoke_tcb.simps)
apply (rename_tac word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11)
apply (rule_tac F="is_aligned word 5" in corres_req)
apply (clarsimp simp add: is_aligned_weaken [OF tcb_aligned])
apply (rule corres_guard_imp [OF tc_corres], clarsimp+)
apply (clarsimp simp: is_cnode_or_valid_arch_def
split: option.split option.split_asm)
apply clarsimp
apply (auto split: option.split_asm simp: newroot_rel_def)[1]
apply (simp add: invokeTCB_def liftM_def[symmetric]
o_def dc_def[symmetric])
apply (rule corres_guard_imp [OF suspend_corres], simp+)
apply (simp add: invokeTCB_def liftM_def[symmetric]
o_def dc_def[symmetric])
apply (rule corres_guard_imp [OF suspend_corres], simp+)
apply (simp add: invokeTCB_def liftM_def[symmetric]
o_def dc_def[symmetric])
apply (rule corres_guard_imp [OF restart_corres], simp+)
apply (simp add:invokeTCB_def)
apply (rename_tac option)
apply (case_tac option)
apply (rule corres_guard_imp [OF restart_corres], simp+)
apply (simp add:invokeTCB_def)
apply (rename_tac option)
apply (case_tac option)
apply simp
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ unbind_notification_corres])
apply (rule corres_trivial, simp)
apply wp+
apply (clarsimp)
apply clarsimp
apply simp
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ unbind_notification_corres])
apply (rule corres_split[OF _ bind_notification_corres])
apply (rule corres_trivial, simp)
apply wp+
apply (clarsimp)
apply clarsimp
apply simp
apply clarsimp
apply (clarsimp simp: obj_at_def is_ntfn)
apply (clarsimp simp: obj_at'_def projectKOs)
apply (simp add: invokeTCB_def tlsBaseRegister_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ bind_notification_corres])
apply (rule corres_trivial, simp)
apply wp+
apply clarsimp
apply (clarsimp simp: obj_at_def is_ntfn)
apply (clarsimp simp: obj_at'_def projectKOs)
apply (rule corres_split[OF _ TcbAcc_R.user_setreg_corres])
apply (rule corres_split[OF _ Bits_R.gct_corres])
apply (rule corres_split[OF _ Corres_UL.corres_when])
apply (rule corres_trivial, simp)
apply simp
apply (rule TcbAcc_R.rescheduleRequired_corres)
apply (wpsimp wp: hoare_drop_imp)+
apply (clarsimp simp: valid_sched_weak_strg einvs_valid_etcbs)
apply (clarsimp simp: Tcb_R.invs_valid_queues' Invariants_H.invs_queues)
done
lemma tcbBoundNotification_caps_safe[simp]:
@ -1770,22 +1785,29 @@ lemma tcbntfn_invs':
apply (wp unbindNotification_invs bindNotification_invs' | simp)+
done
lemma setTLSBase_invs'[wp]:
"\<lbrace>invs' and tcb_inv_wf' (tcbinvocation.SetTLSBase tcb tls_base)\<rbrace>
invokeTCB (tcbinvocation.SetTLSBase tcb tls_base)
\<lbrace>\<lambda>rv. invs'\<rbrace>"
by (wpsimp simp: invokeTCB_def)
lemma tcbinv_invs':
"\<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' ti\<rbrace>
invokeTCB ti
\<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (case_tac ti, simp_all only:)
apply (simp add: invokeTCB_def)
apply wp
apply (clarsimp simp: invs'_def valid_state'_def
dest!: global'_no_ex_cap)
apply (simp add: invokeTCB_def)
apply wp
apply (wp restart_invs')
apply (clarsimp simp: invs'_def valid_state'_def
dest!: global'_no_ex_cap)
apply (simp add: invokeTCB_def)
apply (wp restart_invs')
apply (clarsimp simp: invs'_def valid_state'_def
dest!: global'_no_ex_cap)
apply (wp tc_invs')
apply (clarsimp split: option.split dest!: isCapDs)
apply (wp writereg_invs' readreg_invs' copyreg_invs' tcbntfn_invs' | simp)+
dest!: global'_no_ex_cap)
apply (wp tc_invs')
apply (clarsimp split: option.split dest!: isCapDs)
apply (wp writereg_invs' readreg_invs' copyreg_invs' tcbntfn_invs'
| simp)+
done
crunch_ignore (add: setNextPC getRestartPC)
@ -2577,6 +2599,14 @@ lemma decode_unbind_notification_corres:
apply auto
done
lemma decode_set_tls_base_corres:
"corres (ser \<oplus> tcbinv_relation) (tcb_at t) (tcb_at' t)
(decode_set_tls_base w (cap.ThreadCap t))
(decodeSetTLSBase w (capability.ThreadCap t))"
apply (clarsimp simp: decode_set_tls_base_def decodeSetTLSBase_def returnOk_def
split: list.split)
by (rule sym, rule ucast_id)
lemma decode_tcb_inv_corres:
"\<lbrakk> c = Structures_A.ThreadCap t; cap_relation c c';
list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras';
@ -2603,7 +2633,8 @@ lemma decode_tcb_inv_corres:
corres_guard_imp[OF decode_set_ipc_corres]
corres_guard_imp[OF decode_set_space_corres]
corres_guard_imp[OF decode_bind_notification_corres]
corres_guard_imp[OF decode_unbind_notification_corres],
corres_guard_imp[OF decode_unbind_notification_corres]
corres_guard_imp[OF decode_set_tls_base_corres],
simp_all add: valid_cap_simps valid_cap_simps' invs_def valid_sched_def)
apply (auto simp: list_all2_map1 list_all2_map2
elim!: list_all2_mono)
@ -2645,6 +2676,14 @@ lemma decodeUnbindNotification_wf:
apply (auto simp: obj_at'_def pred_tcb_at'_def)
done
lemma decodeSetTLSBase_wf:
"\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace>
decodeSetTLSBase w (capability.ThreadCap t)
\<lbrace>tcb_inv_wf'\<rbrace>,-"
apply (simp add: decodeSetTLSBase_def
cong: list.case_cong)
by wpsimp
lemma decodeTCBInv_wf:
"\<lbrace>invs' and tcb_at' t and cte_at' slot and ex_nonz_cap_to' t
and (\<lambda>s. \<forall>x \<in> set extras. real_cte_at' (snd x) s
@ -2654,7 +2693,7 @@ lemma decodeTCBInv_wf:
apply (simp add: decodeTCBInvocation_def Let_def
cong: if_cong invocation_label.case_cong split del: if_split)
apply (rule hoare_pre)
apply (wpc, (wp decodeTCBConf_wf decodeReadReg_wf decodeWriteReg_wf
apply (wpc, (wp decodeTCBConf_wf decodeReadReg_wf decodeWriteReg_wf decodeSetTLSBase_wf
decodeCopyReg_wf decodeBindNotification_wf decodeUnbindNotification_wf)+)
apply (clarsimp simp: real_cte_at')
apply (fastforce simp: real_cte_at_not_tcb_at' objBits_defs)
@ -2711,6 +2750,7 @@ lemma invokeTCB_makes_simple':
apply ((wp restart_makes_simple' suspend_makes_simple'
mapM_x_wp'
| simp cong: if_cong)+)[5]
apply (wpsimp split: if_split)
apply (rule hoare_pre)
apply ((simp split del: if_split
| wp cteDelete_makes_simple' checkCap_inv [where P="st_tcb_at' simple' t"]

122
proof/refine/ARM_HYP/Tcb_R.thy
View File

@ -1598,6 +1598,8 @@ where
= (x = tcbinvocation.Resume a)"
| "tcbinv_relation (tcb_invocation.NotificationControl t ntfnptr) x
= (x = tcbinvocation.NotificationControl t ntfnptr)"
| "tcbinv_relation (tcb_invocation.SetTLSBase ref w) x
= (x = tcbinvocation.SetTLSBase ref w)"
primrec
tcb_inv_wf' :: "tcbinvocation \<Rightarrow> kernel_state \<Rightarrow> bool"
@ -1635,6 +1637,8 @@ where
\<and> (\<forall>q. ntfnObj ko \<noteq> WaitingNtfn q)) ntfnptr
and ex_nonz_cap_to' ntfnptr
and bound_tcb_at' (op = None) t) )"
| "tcb_inv_wf' (tcbinvocation.SetTLSBase ref w)
= (tcb_at' ref and ex_nonz_cap_to' ref)"
lemma tcbinv_corres:
"tcbinv_relation ti ti' \<Longrightarrow>
@ -1643,43 +1647,54 @@ lemma tcbinv_corres:
(invs' and sch_act_simple and tcb_inv_wf' ti')
(invoke_tcb ti) (invokeTCB ti')"
apply (case_tac ti, simp_all only: tcbinv_relation.simps valid_tcb_invocation_def)
apply (rule corres_guard_imp [OF writereg_corres], simp+)[1]
apply (rule corres_guard_imp [OF readreg_corres], simp+)[1]
apply (rule corres_guard_imp [OF copyreg_corres], simp+)[1]
apply (clarsimp simp del: invoke_tcb.simps)
apply (rename_tac word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11)
apply (rule_tac F="is_aligned word 5" in corres_req)
apply (clarsimp simp add: is_aligned_weaken [OF tcb_aligned])
apply (rule corres_guard_imp [OF tc_corres], clarsimp+)
subgoal
by (clarsimp simp: is_cnode_or_valid_arch_def
split: option.split option.split_asm)
apply clarsimp
apply (auto split: option.split_asm simp: newroot_rel_def)[1]
apply (rule corres_guard_imp [OF writereg_corres], simp+)[1]
apply (rule corres_guard_imp [OF readreg_corres], simp+)[1]
apply (rule corres_guard_imp [OF copyreg_corres], simp+)[1]
apply (clarsimp simp del: invoke_tcb.simps)
apply (rename_tac word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11)
apply (rule_tac F="is_aligned word 5" in corres_req)
apply (clarsimp simp add: is_aligned_weaken [OF tcb_aligned])
apply (rule corres_guard_imp [OF tc_corres], clarsimp+)
subgoal
by (clarsimp simp: is_cnode_or_valid_arch_def
split: option.split option.split_asm)
apply clarsimp
apply (auto split: option.split_asm simp: newroot_rel_def)[1]
apply (simp add: invokeTCB_def liftM_def[symmetric]
o_def dc_def[symmetric])
apply (rule corres_guard_imp [OF suspend_corres], simp+)
apply (simp add: invokeTCB_def liftM_def[symmetric]
o_def dc_def[symmetric])
apply (rule corres_guard_imp [OF suspend_corres], simp+)
apply (simp add: invokeTCB_def liftM_def[symmetric]
o_def dc_def[symmetric])
apply (rule corres_guard_imp [OF restart_corres], simp+)
apply (simp add:invokeTCB_def)
apply (rename_tac option)
apply (case_tac option)
apply (rule corres_guard_imp [OF restart_corres], simp+)
apply (simp add: invokeTCB_def)
apply (rename_tac option)
apply (case_tac option)
apply simp
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ unbind_notification_corres])
apply (rule corres_trivial, simp)
apply wp+
apply clarsimp
apply clarsimp
apply simp
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ unbind_notification_corres])
apply (rule corres_split[OF _ bind_notification_corres])
apply (rule corres_trivial, simp)
apply wp+
apply (clarsimp)
apply clarsimp
apply simp
apply clarsimp
apply (clarsimp simp: obj_at_def is_ntfn)
apply (clarsimp simp: obj_at'_def projectKOs)
apply (simp add: invokeTCB_def tlsBaseRegister_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ bind_notification_corres])
apply (rule corres_trivial, simp)
apply wp+
apply clarsimp
apply (clarsimp simp: obj_at_def is_ntfn)
apply (clarsimp simp: obj_at'_def projectKOs)
apply (rule corres_split[OF _ TcbAcc_R.user_setreg_corres])
apply (rule corres_split[OF _ Bits_R.gct_corres])
apply (rule corres_split[OF _ Corres_UL.corres_when])
apply (rule corres_trivial, simp)
apply simp
apply (rule TcbAcc_R.rescheduleRequired_corres)
apply (wpsimp wp: hoare_drop_imp)+
apply (clarsimp simp: valid_sched_weak_strg einvs_valid_etcbs)
apply (clarsimp simp: Tcb_R.invs_valid_queues' Invariants_H.invs_queues)
done
lemma tcbBoundNotification_caps_safe[simp]:
@ -1762,22 +1777,29 @@ lemma tcbntfn_invs':
apply (wp unbindNotification_invs bindNotification_invs' | simp)+
done
lemma setTLSBase_invs'[wp]:
"\<lbrace>invs' and tcb_inv_wf' (tcbinvocation.SetTLSBase tcb tls_base)\<rbrace>
invokeTCB (tcbinvocation.SetTLSBase tcb tls_base)
\<lbrace>\<lambda>rv. invs'\<rbrace>"
by (wpsimp simp: invokeTCB_def)
lemma tcbinv_invs':
"\<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' ti\<rbrace>
invokeTCB ti
\<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (case_tac ti, simp_all only:)
apply (simp add: invokeTCB_def)
apply wp
apply (clarsimp simp: invs'_def valid_state'_def
dest!: global'_no_ex_cap)
apply (simp add: invokeTCB_def)
apply wp
apply (wp restart_invs')
apply (clarsimp simp: invs'_def valid_state'_def
dest!: global'_no_ex_cap)
apply (simp add: invokeTCB_def)
apply (wp restart_invs')
apply (clarsimp simp: invs'_def valid_state'_def
dest!: global'_no_ex_cap)
apply (wp tc_invs')
apply (clarsimp split: option.split dest!: isCapDs)
apply (wp writereg_invs' readreg_invs' copyreg_invs' tcbntfn_invs' | simp)+
dest!: global'_no_ex_cap)
apply (wp tc_invs')
apply (clarsimp split: option.split dest!: isCapDs)
apply (wp writereg_invs' readreg_invs' copyreg_invs' tcbntfn_invs'
| simp)+
done
crunch_ignore (add: setNextPC getRestartPC)
@ -2569,6 +2591,14 @@ lemma decode_unbind_notification_corres:
apply auto
done
lemma decode_set_tls_base_corres:
"corres (ser \<oplus> tcbinv_relation) (tcb_at t) (tcb_at' t)
(decode_set_tls_base w (cap.ThreadCap t))
(decodeSetTLSBase w (capability.ThreadCap t))"
apply (clarsimp simp: decode_set_tls_base_def decodeSetTLSBase_def returnOk_def
split: list.split)
by (rule sym, rule ucast_id)
lemma decode_tcb_inv_corres:
"\<lbrakk> c = Structures_A.ThreadCap t; cap_relation c c';
list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras';
@ -2595,7 +2625,8 @@ lemma decode_tcb_inv_corres:
corres_guard_imp[OF decode_set_ipc_corres]
corres_guard_imp[OF decode_set_space_corres]
corres_guard_imp[OF decode_bind_notification_corres]
corres_guard_imp[OF decode_unbind_notification_corres],
corres_guard_imp[OF decode_unbind_notification_corres]
corres_guard_imp[OF decode_set_tls_base_corres],
simp_all add: valid_cap_simps valid_cap_simps' invs_def valid_sched_def)
apply (auto simp: list_all2_map1 list_all2_map2
elim!: list_all2_mono)
@ -2637,6 +2668,14 @@ lemma decodeUnbindNotification_wf:
apply (auto simp: obj_at'_def pred_tcb_at'_def)
done
lemma decodeSetTLSBase_wf:
"\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace>
decodeSetTLSBase w (capability.ThreadCap t)
\<lbrace>tcb_inv_wf'\<rbrace>,-"
apply (simp add: decodeSetTLSBase_def
cong: list.case_cong)
by wpsimp
lemma decodeTCBInv_wf:
"\<lbrace>invs' and tcb_at' t and cte_at' slot and ex_nonz_cap_to' t
and (\<lambda>s. \<forall>x \<in> set extras. real_cte_at' (snd x) s
@ -2646,7 +2685,7 @@ lemma decodeTCBInv_wf:
apply (simp add: decodeTCBInvocation_def Let_def
cong: if_cong invocation_label.case_cong split del: if_split)
apply (rule hoare_pre)
apply (wpc, (wp decodeTCBConf_wf decodeReadReg_wf decodeWriteReg_wf
apply (wpc, (wp decodeTCBConf_wf decodeReadReg_wf decodeWriteReg_wf decodeSetTLSBase_wf
decodeCopyReg_wf decodeBindNotification_wf decodeUnbindNotification_wf)+)
apply (clarsimp simp: real_cte_at')
apply (fastforce simp: real_cte_at_not_tcb_at' objBits_defs)
@ -2703,6 +2742,7 @@ lemma invokeTCB_makes_simple':
apply ((wp restart_makes_simple' suspend_makes_simple'
mapM_x_wp'
| simp cong: if_cong)+)[5]
apply (wpsimp split: if_split)
apply (rule hoare_pre)
apply ((simp split del: if_split
| wp cteDelete_makes_simple' checkCap_inv [where P="st_tcb_at' simple' t"]

120
proof/refine/X64/Tcb_R.thy
View File

@ -1638,6 +1638,8 @@ where
= (x = tcbinvocation.Resume a)"
| "tcbinv_relation (tcb_invocation.NotificationControl t ntfnptr) x
= (x = tcbinvocation.NotificationControl t ntfnptr)"
| "tcbinv_relation (tcb_invocation.SetTLSBase ref w) x
= (x = tcbinvocation.SetTLSBase ref w)"
primrec
tcb_inv_wf' :: "tcbinvocation \<Rightarrow> kernel_state \<Rightarrow> bool"
@ -1675,6 +1677,8 @@ where
\<and> (\<forall>q. ntfnObj ko \<noteq> WaitingNtfn q)) ntfnptr
and ex_nonz_cap_to' ntfnptr
and bound_tcb_at' (op = None) t) )"
| "tcb_inv_wf' (tcbinvocation.SetTLSBase ref w)
= (tcb_at' ref and ex_nonz_cap_to' ref)"
lemma tcbinv_corres:
"tcbinv_relation ti ti' \<Longrightarrow>
@ -1683,42 +1687,53 @@ lemma tcbinv_corres:
(invs' and sch_act_simple and tcb_inv_wf' ti')
(invoke_tcb ti) (invokeTCB ti')"
apply (case_tac ti, simp_all only: tcbinv_relation.simps valid_tcb_invocation_def)
apply (rule corres_guard_imp [OF writereg_corres], simp+)[1]
apply (rule corres_guard_imp [OF readreg_corres], simp+)[1]
apply (rule corres_guard_imp [OF copyreg_corres], simp+)[1]
apply (clarsimp simp del: invoke_tcb.simps)
apply (rename_tac word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11)
apply (rule_tac F="is_aligned word 5" in corres_req)
apply (clarsimp simp add: is_aligned_weaken [OF tcb_aligned])
apply (rule corres_guard_imp [OF tc_corres], clarsimp+)
apply (clarsimp simp: is_cnode_or_valid_arch_def
split: option.split option.split_asm)
apply clarsimp
apply (auto split: option.split_asm simp: newroot_rel_def)[1]
apply (rule corres_guard_imp [OF writereg_corres], simp+)[1]
apply (rule corres_guard_imp [OF readreg_corres], simp+)[1]
apply (rule corres_guard_imp [OF copyreg_corres], simp+)[1]
apply (clarsimp simp del: invoke_tcb.simps)
apply (rename_tac word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11)
apply (rule_tac F="is_aligned word 5" in corres_req)
apply (clarsimp simp add: is_aligned_weaken [OF tcb_aligned])
apply (rule corres_guard_imp [OF tc_corres], clarsimp+)
apply (clarsimp simp: is_cnode_or_valid_arch_def
split: option.split option.split_asm)
apply clarsimp
apply (auto split: option.split_asm simp: newroot_rel_def)[1]
apply (simp add: invokeTCB_def liftM_def[symmetric]
o_def dc_def[symmetric])
apply (rule corres_guard_imp [OF suspend_corres], simp+)
apply (simp add: invokeTCB_def liftM_def[symmetric]
o_def dc_def[symmetric])
apply (rule corres_guard_imp [OF suspend_corres], simp+)
apply (simp add: invokeTCB_def liftM_def[symmetric]
o_def dc_def[symmetric])
apply (rule corres_guard_imp [OF restart_corres], simp+)
apply (simp add:invokeTCB_def)
apply (rename_tac option)
apply (case_tac option)
apply (rule corres_guard_imp [OF restart_corres], simp+)
apply (simp add:invokeTCB_def)
apply (rename_tac option)
apply (case_tac option)
apply simp
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ unbind_notification_corres])
apply (rule corres_trivial, simp)
apply wp+
apply (clarsimp)
apply clarsimp
apply simp
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ unbind_notification_corres])
apply (rule corres_split[OF _ bind_notification_corres])
apply (rule corres_trivial, simp)
apply wp+
apply (clarsimp)
apply clarsimp
apply simp
apply clarsimp
apply (clarsimp simp: obj_at_def is_ntfn)
apply (clarsimp simp: obj_at'_def projectKOs)
apply (simp add: invokeTCB_def tlsBaseRegister_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ bind_notification_corres])
apply (rule corres_trivial, simp)
apply wp+
apply clarsimp
apply (clarsimp simp: obj_at_def is_ntfn)
apply (clarsimp simp: obj_at'_def projectKOs)
apply (rule corres_split[OF _ TcbAcc_R.user_setreg_corres])
apply (rule corres_split[OF _ Bits_R.gct_corres])
apply (rule corres_split[OF _ Corres_UL.corres_when])
apply (rule corres_trivial, simp)
apply simp
apply (rule TcbAcc_R.rescheduleRequired_corres)
apply (wpsimp wp: hoare_drop_imp)+
apply (clarsimp simp: valid_sched_weak_strg einvs_valid_etcbs)
apply (clarsimp simp: Tcb_R.invs_valid_queues' Invariants_H.invs_queues)
done
lemma tcbBoundNotification_caps_safe[simp]:
@ -1801,22 +1816,29 @@ lemma tcbntfn_invs':
apply (wp unbindNotification_invs bindNotification_invs' | simp)+
done
lemma setTLSBase_invs'[wp]:
"\<lbrace>invs' and tcb_inv_wf' (tcbinvocation.SetTLSBase tcb tls_base)\<rbrace>
invokeTCB (tcbinvocation.SetTLSBase tcb tls_base)
\<lbrace>\<lambda>rv. invs'\<rbrace>"
by (wpsimp simp: invokeTCB_def)
lemma tcbinv_invs':
"\<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' ti\<rbrace>
invokeTCB ti
\<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (case_tac ti, simp_all only:)
apply (simp add: invokeTCB_def)
apply wp
apply (clarsimp simp: invs'_def valid_state'_def
dest!: global'_no_ex_cap)
apply (simp add: invokeTCB_def)
apply wp
apply (wp restart_invs')
apply (clarsimp simp: invs'_def valid_state'_def
dest!: global'_no_ex_cap)
apply (simp add: invokeTCB_def)
apply (wp restart_invs')
apply (clarsimp simp: invs'_def valid_state'_def
dest!: global'_no_ex_cap)
apply (wp tc_invs')
apply (clarsimp split: option.split dest!: isCapDs)
apply (wp writereg_invs' readreg_invs' copyreg_invs' tcbntfn_invs' | simp)+
dest!: global'_no_ex_cap)
apply (wp tc_invs')
apply (clarsimp split: option.split dest!: isCapDs)
apply (wp writereg_invs' readreg_invs' copyreg_invs' tcbntfn_invs'
| simp)+
done
crunch_ignore (add: setNextPC getRestartPC)
@ -2608,6 +2630,14 @@ lemma decode_unbind_notification_corres:
apply auto
done
lemma decode_set_tls_base_corres:
"corres (ser \<oplus> tcbinv_relation) (tcb_at t) (tcb_at' t)
(decode_set_tls_base w (cap.ThreadCap t))
(decodeSetTLSBase w (capability.ThreadCap t))"
apply (clarsimp simp: decode_set_tls_base_def decodeSetTLSBase_def returnOk_def
split: list.split)
by (rule sym, rule ucast_id)
lemma decode_tcb_inv_corres:
"\<lbrakk> c = Structures_A.ThreadCap t; cap_relation c c';
list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras';
@ -2634,7 +2664,8 @@ lemma decode_tcb_inv_corres:
corres_guard_imp[OF decode_set_ipc_corres]
corres_guard_imp[OF decode_set_space_corres]
corres_guard_imp[OF decode_bind_notification_corres]
corres_guard_imp[OF decode_unbind_notification_corres],
corres_guard_imp[OF decode_unbind_notification_corres]
corres_guard_imp[OF decode_set_tls_base_corres],
simp_all add: valid_cap_simps valid_cap_simps' invs_def valid_sched_def)
apply (auto simp: list_all2_map1 list_all2_map2
elim!: list_all2_mono)
@ -2676,6 +2707,14 @@ lemma decodeUnbindNotification_wf:
apply (auto simp: obj_at'_def pred_tcb_at'_def)
done
lemma decodeSetTLSBase_wf:
"\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace>
decodeSetTLSBase w (capability.ThreadCap t)
\<lbrace>tcb_inv_wf'\<rbrace>,-"
apply (simp add: decodeSetTLSBase_def
cong: list.case_cong)
by wpsimp
lemma decodeTCBInv_wf:
"\<lbrace>invs' and tcb_at' t and cte_at' slot and ex_nonz_cap_to' t
and (\<lambda>s. \<forall>x \<in> set extras. real_cte_at' (snd x) s
@ -2685,7 +2724,7 @@ lemma decodeTCBInv_wf:
apply (simp add: decodeTCBInvocation_def Let_def
cong: if_cong invocation_label.case_cong split del: if_split)
apply (rule hoare_pre)
apply (wpc, (wp decodeTCBConf_wf decodeReadReg_wf decodeWriteReg_wf
apply (wpc, (wp decodeTCBConf_wf decodeReadReg_wf decodeWriteReg_wf decodeSetTLSBase_wf
decodeCopyReg_wf decodeBindNotification_wf decodeUnbindNotification_wf)+)
apply (clarsimp simp: real_cte_at')
apply (fastforce simp: real_cte_at_not_tcb_at' objBits_defs)
@ -2742,6 +2781,7 @@ lemma invokeTCB_makes_simple':
apply ((wp restart_makes_simple' suspend_makes_simple'
mapM_x_wp'
| simp cong: if_cong)+)[5]
apply (wpsimp split: if_split)
apply (rule hoare_pre)
apply ((simp split del: if_split
| wp cteDelete_makes_simple' checkCap_inv [where P="st_tcb_at' simple' t"]