diff --git a/proof/refine/RISCV64/Tcb_R.thy b/proof/refine/RISCV64/Tcb_R.thy index d0632ef6e..d1714323e 100644 --- a/proof/refine/RISCV64/Tcb_R.thy +++ b/proof/refine/RISCV64/Tcb_R.thy @@ -14,6 +14,18 @@ begin context begin interpretation Arch . (*FIXME: arch_split*) +(* FIXME RISCV: move to Invariants_H *) +lemma invs_valid_queues'_strg: + "invs' s \ valid_queues' s" + by (clarsimp simp: invs'_def valid_state'_def) + +(* FIXME RISCV: move to Invariants_H *) +lemmas invs_valid_queues'[elim!] = invs_valid_queues'_strg[rule_format] + +(* FIXME RISCV: move to Invariants_H *) +lemma einvs_valid_etcbs: "einvs s \ valid_etcbs s" + by (clarsimp simp: valid_sched_def) + lemma setNextPCs_corres: "corres dc (tcb_at t and invs) (tcb_at' t and invs') (as_user t (setNextPC v)) (asUser t (setNextPC v))" @@ -106,8 +118,7 @@ lemma activate_invs': \ st_tcb_at' (\st. st = state) thread s \ thread = ksCurThread s \ (runnable' state \ idle' state)" in hoare_seq_ext) - apply (case_tac x, simp_all add: isTS_defs hoare_pre_cont - split del: if_splits cong: if_cong) + apply (case_tac x; simp add: isTS_defs split del: if_split cong: if_cong) apply (wp) apply (clarsimp simp: ct_in_state'_def) apply (rule_tac Q="\rv. invs' and ct_idle'" in hoare_post_imp, simp) @@ -131,9 +142,6 @@ lemma activate_invs': pred_disj_def) done -crunch nosch[wp]: activateIdleThread "\s. P (ksSchedulerAction s)" - (ignore: setNextPC) - declare not_psubset_eq[dest!] lemma setThreadState_runnable_simp: @@ -174,12 +182,9 @@ lemma idle_tsr: "thread_state_relation ts ts' \ idle' ts' = idle ts" by (case_tac ts, auto) -crunch cur [wp]: cancelIPC cur_tcb' +crunch cur [wp]: cancelIPC, setupReplyMaster cur_tcb' (wp: crunch_wps simp: crunch_simps o_def) -crunch cur [wp]: setupReplyMaster cur_tcb' - (wp: crunch_wps simp: crunch_simps) - lemma setCTE_weak_sch_act_wf[wp]: "\\s. weak_sch_act_wf (ksSchedulerAction s) s\ setCTE c cte @@ -312,18 +317,6 @@ lemma readreg_corres: apply (clarsimp simp: invs'_def valid_state'_def dest!: global'_no_ex_cap) done -crunch sch_act_simple [wp]: asUser "sch_act_simple" - (rule: sch_act_simple_lift) - -lemma invs_valid_queues': - "invs' s \ valid_queues' s" - by (clarsimp simp: invs'_def valid_state'_def) - -declare invs_valid_queues'[rule_format, elim!] - -lemma einvs_valid_etcbs: "einvs s \ valid_etcbs s" - by (clarsimp simp: valid_sched_def) - lemma arch_post_modify_registers_corres: "corres dc (tcb_at t) (tcb_at' t and tcb_at' ct) (arch_post_modify_registers ct t) @@ -394,9 +387,6 @@ lemma suspend_ResumeCurrentThread_imp_notct[wp]: \\rv s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\" by (wpsimp simp: suspend_def) -crunches ThreadDecls_H.suspend - for it'[wp]: "\s. P (ksIdleThread s)" - lemma copyreg_corres: "corres (intr \ (=)) (einvs and simple_sched_action and tcb_at dest and tcb_at src and ex_nonz_cap_to src and @@ -482,8 +472,7 @@ proof - apply (wp suspend_nonz_cap_to_tcb static_imp_wp | simp add: if_apply_def2)+ apply (fastforce simp: invs_def valid_state_def valid_pspace_def dest!: idle_no_ex_cap) - apply (fastforce simp: invs'_def valid_state'_def dest!: global'_no_ex_cap) - done + by (fastforce simp: invs'_def valid_state'_def dest!: global'_no_ex_cap) qed lemma readreg_invs': @@ -494,13 +483,13 @@ lemma readreg_invs': | clarsimp simp: invs'_def valid_state'_def dest!: global'_no_ex_cap)+ -crunch invs'[wp]: getSanitiseRegisterInfo invs' +crunches getSanitiseRegisterInfo + for invs'[wp]: invs' + and ex_nonz_cap_to'[wp]: "ex_nonz_cap_to' d" + and it'[wp]: "\s. P (ksIdleThread s)" + and tcb_at'[wp]: "tcb_at' t" (ignore: getObject setObject) -crunch ex_nonz_cap_to'[wp]: getSanitiseRegisterInfo "ex_nonz_cap_to' d" -crunch it'[wp]: getSanitiseRegisterInfo "\s. P (ksIdleThread s)" -crunch tcb_at'[wp]: getSanitiseRegisterInfo "tcb_at' a" - lemma writereg_invs': "\invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest\ invokeTCB (tcbinvocation.WriteRegisters dest resume values arch) @@ -554,10 +543,10 @@ lemma threadSet_valid_queues'_no_state: apply (wp setObject_ko_wp_at | simp add: objBits_simps')+ apply (wp getObject_tcb_wp updateObject_default_inv | simp split del: if_split)+ - apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs + apply (clarsimp simp: obj_at'_def ko_wp_at'_def objBits_simps addToQs_def split del: if_split cong: if_cong) - apply (fastforce simp: projectKOs inQ_def split: if_split_asm) + apply (fastforce simp: inQ_def split: if_split_asm) done lemma gts_isRunnable_corres: @@ -841,7 +830,7 @@ lemma check_cap_at_corres_weak: defs assertDerived_def: "assertDerived src cap f \ - do stateAssert (\s. cte_wp_at' (is_derived' (ctes_of s) src cap o cteCap) src s) []; f od" + do stateAssert (\s. cte_wp_at' (is_derived' (ctes_of s) src cap o cteCap) src s) []; f od" lemma checked_insert_corres: "cap_relation new_cap newCap \ @@ -972,9 +961,7 @@ lemma isValidVTableRootD: lemma assertDerived_wp: "\P and (\s. cte_wp_at' (is_derived' (ctes_of s) slot cap o cteCap) slot s)\ f \Q\ \ \P\ assertDerived slot cap f \Q\" - apply (simp add: assertDerived_def) - apply wpsimp - done + unfolding assertDerived_def by wpsimp lemma setMCPriority_invs': "\invs' and tcb_at' t and K (prio \ maxPriority)\ setMCPriority t prio \\rv. invs'\" @@ -1011,9 +998,11 @@ lemma setMCPriority_valid_objs'[wp]: crunch sch_act_simple[wp]: setMCPriority sch_act_simple (wp: ssa_sch_act_simple crunch_wps rule: sch_act_simple_lift simp: crunch_simps) -(* For some reason, when this was embedded in a larger expression clarsimp wouldn't remove it. Adding it as a simp rule does *) +(* For some reason, when this was embedded in a larger expression clarsimp wouldn't remove it. + Adding it as a simp rule does *) lemma inQ_tc_corres_helper: - "(\d p. (\tcb. tcbQueued tcb \ tcbPriority tcb = p \ tcbDomain tcb = d \ (tcbQueued tcb \ tcbDomain tcb \ d)) \ a \ set (ksReadyQueues s (d, p))) = True" + "(\d p. (\tcb. tcbQueued tcb \ tcbPriority tcb = p \ tcbDomain tcb = d \ + (tcbQueued tcb \ tcbDomain tcb \ d)) \ a \ set (ksReadyQueues s (d, p)))" by clarsimp abbreviation "valid_option_prio \ case_option True (\(p, auth). p \ maxPriority)" @@ -1044,52 +1033,19 @@ lemma thread_set_ipc_weak_valid_sched_action: get_tcb_def obj_at_kh_def obj_at_def is_etcb_at'_def valid_sched_def valid_sched_action_def) done -(* FIXME RISCV remove *) -lemma thread_set_ipc_etcbs: - "\ einvs \ - thread_set (tcb_ipc_buffer_update f) a - \\_. valid_etcbs\" - apply (rule hoare_pre) - apply (simp add: thread_set_def) - apply (wp set_object_wp) - apply (simp | intro impI | elim exE conjE)+ - apply (frule get_tcb_SomeD) - apply (erule ssubst) - apply (clarsimp simp add: weak_valid_sched_action_def valid_etcbs_2_def st_tcb_at_kh_def - get_tcb_def obj_at_kh_def obj_at_def is_etcb_at'_def valid_sched_def valid_sched_action_def) - apply (erule_tac x=a in allE)+ - apply (clarsimp simp: is_tcb_def) - done - -(* FIXME RISCV remove *) -lemma threadcontrol_corres_helper1: - "\ einvs and simple_sched_action\ - thread_set (tcb_ipc_buffer_update f) a - \\x. weak_valid_sched_action and valid_etcbs\" - apply (rule hoare_pre) - apply (simp add: thread_set_def) - apply (wp set_object_wp) - apply (simp | intro impI | elim exE conjE)+ - apply (frule get_tcb_SomeD) - apply (erule ssubst) - apply (clarsimp simp add: weak_valid_sched_action_def valid_etcbs_2_def st_tcb_at_kh_def - get_tcb_def obj_at_kh_def obj_at_def is_etcb_at'_def valid_sched_def valid_sched_action_def) - apply (erule_tac x=a in allE)+ - apply (clarsimp simp: is_tcb_def) - done - lemma threadcontrol_corres_helper2: - "is_aligned a msg_align_bits \ \invs' and tcb_at' t\ - threadSet (tcbIPCBuffer_update (\_. a)) t - \\x s. Invariants_H.valid_queues s \ valid_queues' s\" + "is_aligned a msg_align_bits \ + \invs' and tcb_at' t\ + threadSet (tcbIPCBuffer_update (\_. a)) t + \\x s. Invariants_H.valid_queues s \ valid_queues' s\" by (wp threadSet_invs_trivial | strengthen invs_valid_queues' invs_queues invs_weak_sch_act_wf | clarsimp simp: inQ_def )+ lemma threadcontrol_corres_helper3: "\ einvs and simple_sched_action\ - check_cap_at aaa (ab, ba) (check_cap_at (cap.ThreadCap a) slot (cap_insert aaa (ab, ba) (a, tcb_cnode_index 4))) - \\x. weak_valid_sched_action and valid_etcbs \" + check_cap_at cap p (check_cap_at (cap.ThreadCap cap') slot (cap_insert cap p (t, tcb_cnode_index 4))) + \\x. weak_valid_sched_action and valid_etcbs \" apply (rule hoare_pre) apply (wp check_cap_inv | simp add:)+ by (clarsimp simp add: weak_valid_sched_action_def valid_etcbs_2_def st_tcb_at_kh_def @@ -1487,8 +1443,7 @@ proof - apply (clarsimp simp: inQ_def) apply (clarsimp simp: obj_at_def is_tcb) apply (rule cte_wp_at_tcbI, simp, fastforce, simp) - apply (clarsimp simp: cte_map_def tcb_cnode_index_def obj_at'_def - projectKOs objBits_simps) + apply (clarsimp simp: cte_map_def tcb_cnode_index_def obj_at'_def objBits_simps) apply (erule(2) cte_wp_at_tcbI', fastforce simp: objBits_defs cte_level_bits_def, simp) done have U: "getThreadCSpaceRoot a = return (cte_map (a, tcb_cnode_index 0))" @@ -1661,7 +1616,7 @@ crunch cap_to'[wp]: setPriority, setMCPriority "ex_nonz_cap_to' a" (simp: crunch_simps) lemma cteInsert_sa_simple[wp]: - "\sch_act_simple\ cteInsert newCap srcSlot destSlot \\_. sch_act_simple\" + "cteInsert newCap srcSlot destSlot \sch_act_simple\" by (simp add: sch_act_simple_def, wp) lemma isReplyCapD: @@ -1891,21 +1846,21 @@ lemma bindNotification_invs': | clarsimp dest!: global'_no_ex_cap simp: cteCaps_of_def)+ apply (clarsimp simp: valid_pspace'_def) apply (cases "tcbptr = ntfnptr") - apply (clarsimp dest!: pred_tcb_at' simp: obj_at'_def projectKOs) + apply (clarsimp dest!: pred_tcb_at' simp: obj_at'_def) apply (clarsimp simp: pred_tcb_at' conj_comms o_def) apply (subst delta_sym_refs, assumption) - apply (fastforce simp: ntfn_q_refs_of'_def obj_at'_def projectKOs + apply (fastforce simp: ntfn_q_refs_of'_def obj_at'_def dest!: symreftype_inverse' split: ntfn.splits if_split_asm) apply (clarsimp split: if_split_asm) apply (fastforce simp: tcb_st_refs_of'_def dest!: bound_tcb_at_state_refs_ofD' split: if_split_asm thread_state.splits) - apply (fastforce simp: obj_at'_def projectKOs state_refs_of'_def + apply (fastforce simp: obj_at'_def state_refs_of'_def dest!: symreftype_inverse') apply (clarsimp simp: valid_pspace'_def) apply (frule_tac P="\k. k=ntfn" in obj_at_valid_objs', simp) - apply (clarsimp simp: valid_obj'_def projectKOs valid_ntfn'_def obj_at'_def + apply (clarsimp simp: valid_obj'_def valid_ntfn'_def obj_at'_def dest!: pred_tcb_at' split: ntfn.splits) done @@ -2096,8 +2051,7 @@ lemma decode_set_priority_corres: apply (rule corres_returnOkTT) apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2)) apply wpsimp+ - apply (corressimp simp: valid_cap_def valid_cap'_def)+ - done + by (corressimp simp: valid_cap_def valid_cap'_def)+ lemma decode_set_mcpriority_corres: "\ cap_relation cap cap'; is_thread_cap cap; @@ -2115,8 +2069,7 @@ lemma decode_set_mcpriority_corres: apply (rule corres_returnOkTT) apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2)) apply wpsimp+ - apply (corressimp simp: valid_cap_def valid_cap'_def)+ - done + by (corressimp simp: valid_cap_def valid_cap'_def)+ lemma valid_objs'_maxPriority': "\s t. \ valid_objs' s; tcb_at' t s \ \ obj_at' (\tcb. tcbMCP tcb \ maxPriority) t s" @@ -2140,9 +2093,6 @@ lemma getMCP_wp: "\\s. \mcp. mcpriority_tcb_at' ((=) mcp apply (clarsimp simp: pred_tcb_at'_def obj_at'_def) done -crunch inv: checkPrio "P" - (simp: crunch_simps) - lemma checkPrio_wp: "\ \s. mcpriority_tcb_at' (\mcp. prio \ ucast mcp) auth s \ P s \ checkPrio prio auth @@ -2162,12 +2112,13 @@ lemma checkPrio_lt_ct_weak: apply (clarsimp simp: pred_tcb_at'_def obj_at'_def) by (rule le_ucast_ucast_le) simp +crunch inv: checkPrio "P" + lemma decodeSetPriority_wf[wp]: "\invs' and tcb_at' t and ex_nonz_cap_to' t \ decodeSetPriority args (ThreadCap t) extras \tcb_inv_wf'\,-" unfolding decodeSetPriority_def - apply (rule hoare_pre) - apply (wp checkPrio_lt_ct_weak | wpc | simp | wp (once) checkPrio_inv)+ + apply (wpsimp wp: checkPrio_lt_ct_weak | wp (once) checkPrio_inv)+ apply (clarsimp simp: maxPriority_def numPriorities_def) apply (cut_tac max_word_max[where 'a=8, unfolded max_word_def]) apply simp @@ -2408,8 +2359,7 @@ lemma decode_set_space_corres: apply (unfold unlessE_whenE) apply (rule corres_whenE) apply (case_tac vroot_cap', simp_all add: - is_valid_vtable_root_def isValidVTableRoot_def - RISCV64_H.isValidVTableRoot_def)[1] + is_valid_vtable_root_def isValidVTableRoot_def)[1] apply (rename_tac arch_cap) apply (clarsimp, case_tac arch_cap, simp_all)[1] apply (simp split: option.split) @@ -2581,7 +2531,7 @@ lemma lsft_real_cte: lemma tcb_real_cte_32: "\ real_cte_at' (t + 2^cteSizeBits) s; tcb_at' t s \ \ False" - by (clarsimp simp: obj_at'_def projectKOs objBitsKO_def ps_clear_32) + by (clarsimp simp: obj_at'_def objBitsKO_def ps_clear_32) lemma corres_splitEE': assumes y: "\x y x' y'. r' (x, y) (x', y') @@ -2701,7 +2651,7 @@ lemma decode_tcb_inv_corres: done crunch inv[wp]: decodeTCBInvocation P -(simp: crunch_simps) + (simp: crunch_simps) lemma real_cte_at_not_tcb_at': "real_cte_at' x s \ \ tcb_at' x s"