From b8d82aa1d1ec68fd124f49e8b41b28a6eab94a63 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 7 Aug 2024 17:21:02 +0930 Subject: [PATCH 01/14] rt riscv refine: add cursc_relation Signed-off-by: Michael McInerney --- proof/refine/RISCV64/StateRelation.thy | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/proof/refine/RISCV64/StateRelation.thy b/proof/refine/RISCV64/StateRelation.thy index 722421cafa..9675327a31 100644 --- a/proof/refine/RISCV64/StateRelation.thy +++ b/proof/refine/RISCV64/StateRelation.thy @@ -708,6 +708,10 @@ lemma curthread_relation: "(a, b) \ state_relation \ ksCurThread b = cur_thread a" by (simp add: state_relation_def) +lemma cursc_relation: + "(a, b) \ state_relation \ ksCurSc b = cur_sc a" + by (simp add: state_relation_def) + lemma curdomain_relation[elim!]: "(s, s') \ state_relation \ cur_domain s = ksCurDomain s'" by (clarsimp simp: state_relation_def) From 6458c49e5ce459ab6e88f5e8f74a5bbb98cb8ade Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 7 Aug 2024 17:23:03 +0930 Subject: [PATCH 02/14] rt haskell+design+haskell translator: add readStateAssert Signed-off-by: Michael McInerney --- spec/design/skel/KernelStateData_H.thy | 2 +- spec/haskell/src/SEL4/Model/StateData.lhs | 5 +++++ tools/haskell-translator/lhs_pars.py | 1 + 3 files changed, 7 insertions(+), 1 deletion(-) diff --git a/spec/design/skel/KernelStateData_H.thy b/spec/design/skel/KernelStateData_H.thy index 40179a2dce..1a0a605fce 100644 --- a/spec/design/skel/KernelStateData_H.thy +++ b/spec/design/skel/KernelStateData_H.thy @@ -101,6 +101,6 @@ where od" #INCLUDE_HASKELL SEL4/Model/StateData.lhs decls_only ONLY capHasProperty sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt valid_tcbs'_asrt -#INCLUDE_HASKELL SEL4/Model/StateData.lhs NOT doMachineOp KernelState ReadyQueue ReleaseQueue ReaderM Kernel KernelR getsJust assert stateAssert funOfM condition whileLoop findM funArray newKernelState capHasProperty ifM whenM whileM andM orM sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt valid_tcbs'_asrt +#INCLUDE_HASKELL SEL4/Model/StateData.lhs NOT doMachineOp KernelState ReadyQueue ReleaseQueue ReaderM Kernel KernelR getsJust assert stateAssert readStateAssert funOfM condition whileLoop findM funArray newKernelState capHasProperty ifM whenM whileM andM orM sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt valid_tcbs'_asrt end diff --git a/spec/haskell/src/SEL4/Model/StateData.lhs b/spec/haskell/src/SEL4/Model/StateData.lhs index adc2e392c5..1183262787 100644 --- a/spec/haskell/src/SEL4/Model/StateData.lhs +++ b/spec/haskell/src/SEL4/Model/StateData.lhs @@ -388,6 +388,11 @@ The function "stateAssert" is similar to "assert", except that it reads the curr > stateAssert :: MonadFail m => MonadState s m => (s -> Bool) -> String -> m () > stateAssert f e = get >>= \s -> assert (f s) e +A version of "stateAssert" that can be used within functions that are in the reader monad + +> readStateAssert :: MonadFail m => MonadReader s m => (s -> Bool) -> String -> m () +> readStateAssert f e = ask >>= \s -> assert (f s) e + The "capHasProperty" function is used with "stateAssert". As explained above, it is "const True" here, but is strengthened to actually check the capability in the translation to Isabelle. > capHasProperty :: PPtr CTE -> (Capability -> Bool) -> KernelState -> Bool diff --git a/tools/haskell-translator/lhs_pars.py b/tools/haskell-translator/lhs_pars.py index 203237ddc6..208a811fc4 100644 --- a/tools/haskell-translator/lhs_pars.py +++ b/tools/haskell-translator/lhs_pars.py @@ -1930,6 +1930,7 @@ def split_on_unmatched_bracket(elts, n=None): option_m_map = { 'return': 'oreturn', 'assert': 'ohaskell_assert', + 'readStateAssert': 'ohaskell_state_assert', 'fail': 'ohaskell_fail', 'when': 'owhen', 'unless': 'ounless', From 4d274ae9ef35ca36c14d27c2a8deaa17a8e339a6 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 7 Aug 2024 17:31:28 +0930 Subject: [PATCH 03/14] rt haskell+design+proof: reduce use of active_sc_at' in CRefine This is achieved by asserting active_sc_at' in the appropriate places within the Haskell. Signed-off-by: Michael McInerney --- proof/crefine/RISCV64/Finalise_C.thy | 35 ++++--- proof/crefine/RISCV64/SchedContext_C.thy | 13 +-- proof/crefine/RISCV64/Schedule_C.thy | 1 + proof/crefine/RISCV64/SyscallArgs_C.thy | 95 +++++++++++-------- proof/crefine/RISCV64/Tcb_C.thy | 2 +- proof/refine/RISCV64/InterruptAcc_R.thy | 42 ++++---- proof/refine/RISCV64/Ipc_R.thy | 27 ++++-- proof/refine/RISCV64/KHeap_R.thy | 16 ++-- proof/refine/RISCV64/SchedContextInv_R.thy | 3 +- proof/refine/RISCV64/SchedContext_R.thy | 8 +- proof/refine/RISCV64/Schedule_R.thy | 88 +++++++++-------- proof/refine/RISCV64/Syscall_R.thy | 8 +- proof/refine/RISCV64/TcbAcc_R.thy | 5 + spec/design/skel/KernelStateData_H.thy | 4 +- spec/haskell/src/SEL4/Model/StateData.lhs | 5 + spec/haskell/src/SEL4/Object/SchedContext.lhs | 7 ++ 16 files changed, 216 insertions(+), 143 deletions(-) diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy index 5db0345fcc..3e6aab7bb0 100644 --- a/proof/crefine/RISCV64/Finalise_C.thy +++ b/proof/crefine/RISCV64/Finalise_C.thy @@ -238,12 +238,17 @@ lemma isRoundRobin_ccorres: lemma refill_ready_ccorres: "ccorres (\rv rv'. rv = to_bool rv') ret__unsigned_long_' - (active_sc_at' scPtr and valid_objs') \\sc = Ptr scPtr\ [] + valid_objs' \\sc = Ptr scPtr\ [] (refillReady scPtr) (Call refill_ready_'proc)" supply sched_context_C_size[simp del] refill_C_size[simp del] - apply (cinit lift: sc_' - simp: readRefillReady_def readCurTime_def gets_the_ogets - getRefillHead_def[symmetric] getCurTime_def[symmetric]) + unfolding refillReady_def readRefillReady_def gets_the_obind ohaskell_state_assert_def + gets_the_ostate_assert + apply (rule ccorres_symb_exec_l' + [OF _ _ stateAssert_sp[simplified HaskellLib_H.stateAssert_def]]; + (solves wpsimp)?) + apply (cinit' lift: sc_' + simp: readCurTime_def gets_the_ogets getRefillHead_def[symmetric] + getCurTime_def[symmetric]) apply (rule_tac xf'="\s. h_val (hrs_mem (t_hrs_' (globals s))) (ret__ptr_to_struct_refill_C_' s)" in ccorres_split_nothrow_call) apply (fastforce intro: refill_head_ccorres) @@ -350,13 +355,18 @@ lemmas updateSchedContext_ccorres_lemma2 = lemma refill_next_ccorres: "ccorres (\next next'. next = unat next') ret__unsigned_long_' - (active_sc_at' scPtr and valid_objs' and K (Suc idx < 2 ^ word_bits)) + (valid_objs' and K (Suc idx < 2 ^ word_bits)) (\\sc = Ptr scPtr\ \ \\index = word_of_nat idx\) [] (getRefillNext scPtr idx) (Call refill_next_'proc)" supply len_bit0[simp del] - apply (cinit lift: sc_' index_' - simp: readRefillNext_def refillNext_def readSchedContext_def getObject_def[symmetric] - getSchedContext_def[symmetric]) + unfolding getRefillNext_def readRefillNext_def gets_the_obind ohaskell_state_assert_def + gets_the_ostate_assert + apply (rule ccorres_symb_exec_l' + [OF _ _ stateAssert_sp[simplified HaskellLib_H.stateAssert_def]]; + (solves wpsimp)?) + apply (cinit' lift: sc_' index_' + simp: refillNext_def readSchedContext_def getObject_def[symmetric] + getSchedContext_def[symmetric]) apply (rule ccorres_pre_getObject_sc, rename_tac sc) apply (rule ccorres_move_c_guard_sc) apply (rule ccorres_return_C; clarsimp) @@ -386,10 +396,12 @@ lemma refill_next_ccorres: lemma refill_pop_head_ccorres: "ccorres crefill_relation ret__struct_refill_C_' - (active_sc_at' scPtr and valid_objs' and no_0_obj') \\sc = Ptr scPtr\ [] + (valid_objs' and no_0_obj') \\sc = Ptr scPtr\ [] (refillPopHead scPtr) (Call refill_pop_head_'proc)" supply sched_context_C_size[simp del] refill_C_size[simp del] - apply (cinit lift: sc_') + unfolding refillPopHead_def + apply (rule ccorres_symb_exec_l'[OF _ _ stateAssert_sp]; (solves wpsimp)?) + apply (cinit' lift: sc_') apply (rule ccorres_symb_exec_r) apply (rule_tac xf'="\s. h_val (hrs_mem (t_hrs_' (globals s))) (ret__ptr_to_struct_refill_C_' s)" in ccorres_split_nothrow_call) @@ -738,7 +750,8 @@ lemma refill_unblock_check_ccorres: apply clarsimp apply wpsimp apply (clarsimp simp: active_sc_at'_def) - apply (wpsimp wp: no_ofail_refillHeadOverlapping simp: runReaderT_def) + apply (wpsimp wp: no_ofail_refillHeadOverlapping + simp: runReaderT_def active_sc_at'_def) apply (wpsimp wp: updateRefillHd_valid_objs' mergeOverlappingRefills_valid_objs') apply (clarsimp simp: active_sc_at'_rewrite runReaderT_def) apply (fastforce dest: use_ovalid[OF refillHeadOverlapping_refillSize] diff --git a/proof/crefine/RISCV64/SchedContext_C.thy b/proof/crefine/RISCV64/SchedContext_C.thy index df06eaca2e..f22d70e554 100644 --- a/proof/crefine/RISCV64/SchedContext_C.thy +++ b/proof/crefine/RISCV64/SchedContext_C.thy @@ -20,15 +20,16 @@ crunch getRefillSize lemma refill_add_tail_ccorres: "ccorres dc xfdc - (active_sc_at' scPtr and invs') - (\\sc = Ptr scPtr\ \ {s'. crefill_relation new (refill_' s')}) [] + invs' + (\\sc = Ptr scPtr\ \ {s'. crefill_relation new (refill_' s')}) hs (refillAddTail scPtr new) (Call refill_add_tail_'proc)" supply sched_context_C_size[simp del] refill_C_size[simp del] len_bit0[simp del] - apply (simp add: refillAddTail_def) - apply (rule ccorres_symb_exec_l'[rotated, OF _ getRefillSize_sp]; wpsimp) - apply (rule ccorres_symb_exec_l'[rotated, OF _ get_sc_sp']; wpsimp?) - apply (rule ccorres_symb_exec_l'[rotated, OF _ assert_sp]; wpsimp) + unfolding refillAddTail_def K_bind_apply haskell_assert_def + apply (rule ccorres_symb_exec_l'[rotated, OF _ stateAssert_sp]; (solves wpsimp)?) + apply (rule ccorres_symb_exec_l'[rotated, OF _ getRefillSize_sp]; (solves wpsimp)?) + apply (rule ccorres_symb_exec_l'[rotated, OF _ get_sc_sp']; (solves wpsimp)?) + apply (rule ccorres_symb_exec_l'[rotated, OF _ assert_sp]; (solves wpsimp)?) apply (cinit' lift: sc_' refill_' simp: updateRefillIndex_def) apply (rule ccorres_move_c_guard_sc) diff --git a/proof/crefine/RISCV64/Schedule_C.thy b/proof/crefine/RISCV64/Schedule_C.thy index a312834f69..73ba8d6331 100644 --- a/proof/crefine/RISCV64/Schedule_C.thy +++ b/proof/crefine/RISCV64/Schedule_C.thy @@ -781,6 +781,7 @@ lemma no_ofail_releaseQNonEmptyAndReady: apply normalise_obj_at' apply (fastforce intro!: aligned'_distinct'_obj_at'I simp: active_sc_tcb_at'_def obj_at'_def opt_pred_def opt_map_def + active_sc_at'_def split: option.splits) done diff --git a/proof/crefine/RISCV64/SyscallArgs_C.thy b/proof/crefine/RISCV64/SyscallArgs_C.thy index 2c31dd5b9e..2562c6bcc8 100644 --- a/proof/crefine/RISCV64/SyscallArgs_C.thy +++ b/proof/crefine/RISCV64/SyscallArgs_C.thy @@ -339,20 +339,24 @@ lemma refill_index_ccorres: lemma readRefillHead_rewrite: "readRefillHead scPtr = do { + ostate_assert (active_sc_at' scPtr); sc \ readSchedContext scPtr; readRefillIndex scPtr (scRefillHead sc) }" - by (fastforce simp: readRefillHead_def refillHd_def readRefillIndex_def refillIndex_def obind_def + by (fastforce simp: readRefillHead_def refillHd_def readRefillIndex_def refillIndex_def + obind_def ohaskell_state_assert_def split: option.splits) lemma refill_head_ccorres: "ccorres crefill_relation (\s. h_val (hrs_mem (t_hrs_' (globals s))) (ret__ptr_to_struct_refill_C_' s)) - (active_sc_at' scPtr and valid_objs') (\\sc = Ptr scPtr\) [] + valid_objs' (\\sc = Ptr scPtr\) [] (getRefillHead scPtr) (Call refill_head_'proc)" apply (cinit' lift: sc_' simp: getRefillHead_def readRefillHead_rewrite readSchedContext_def + gets_the_ostate_assert getObject_def[symmetric] getSchedContext_def[symmetric]) + apply (rule ccorres_stateAssert[unfolded HaskellLib_H.stateAssert_def]) apply (rule ccorres_pre_getObject_sc) apply (rule ccorres_move_c_guard_sc) apply (rule ccorres_add_return2) @@ -380,20 +384,24 @@ lemma refill_head_ccorres: lemma readRefillTail_rewrite: "readRefillTail scPtr = do { + ostate_assert (active_sc_at' scPtr); sc \ readSchedContext scPtr; readRefillIndex scPtr (scRefillTail sc) }" by (fastforce simp: readRefillTail_def refillTl_def readRefillIndex_def refillIndex_def obind_def + ohaskell_state_assert_def split: option.splits) lemma refill_tail_ccorres: "ccorres crefill_relation (\s. h_val (hrs_mem (t_hrs_' (globals s))) (ret__ptr_to_struct_refill_C_' s)) - (active_sc_at' scPtr and valid_objs') (\\sc = Ptr scPtr\) [] + valid_objs' (\\sc = Ptr scPtr\) [] (getRefillTail scPtr) (Call refill_tail_'proc)" apply (cinit' lift: sc_' simp: getRefillTail_def readRefillTail_rewrite readSchedContext_def + gets_the_ostate_assert getObject_def[symmetric] getSchedContext_def[symmetric]) + apply (rule ccorres_stateAssert[unfolded HaskellLib_H.stateAssert_def]) apply (rule ccorres_pre_getObject_sc) apply (rule ccorres_move_c_guard_sc) apply (rule ccorres_add_return2) @@ -421,53 +429,62 @@ lemma refill_tail_ccorres: lemma refill_capacity_ccorres: "ccorres (=) ret__unsigned_longlong_' - (active_sc_at' scPtr and valid_objs' and no_0_obj') (\\sc = Ptr scPtr\ \ \\usage = usage\) [] + (valid_objs' and no_0_obj') (\\sc = Ptr scPtr\ \ \\usage = usage\) [] (getRefillCapacity scPtr usage) (Call refill_capacity_'proc)" apply (cinit lift: usage_') - apply (clarsimp simp: readRefillCapacity_def getRefillHead_def[symmetric] refillCapacity_def) - apply (clarsimp simp: if_distrib) - apply (rule_tac xf'="\s. h_val (hrs_mem (t_hrs_' (globals s))) (ret__ptr_to_struct_refill_C_' s)" - in ccorres_split_nothrow_call) - apply (rule ccorres_nohs) - apply (rule refill_head_ccorres) + apply (clarsimp simp: readRefillCapacity_def getRefillHead_def[symmetric] refillCapacity_def + ohaskell_state_assert_def gets_the_ostate_assert) + apply (rule ccorres_symb_exec_l[OF _ _ stateAssert_sp[unfolded HaskellLib_H.stateAssert_def]]) + apply (clarsimp simp: if_distrib) + apply (rule_tac xf'="\s. h_val (hrs_mem (t_hrs_' (globals s))) (ret__ptr_to_struct_refill_C_' s)" + in ccorres_split_nothrow_call) + apply (rule ccorres_nohs) + apply (rule refill_head_ccorres) + apply fastforce + apply (clarsimp simp: typ_heap_simps) + apply fastforce + apply ceqv + apply (rename_tac refill refill') + apply (rule ccorres_Guard_Seq) + apply (rule_tac val="rAmount refill" + and xf'=head_amount_' + and R=\ + and R'="{s'. cslift s' (ret__ptr_to_struct_refill_C_' s') = Some refill'}" + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply (clarsimp simp: crefill_relation_def typ_heap_simps') + apply ceqv + apply (rule ccorres_cond_seq) + apply ccorres_rewrite + apply (rule_tac R="sc_at' scPtr" + and R'="\h_val (hrs_mem \t_hrs) \ret__ptr_to_struct_refill_C = refill'\" + in ccorres_cond_strong) + apply (simp add: crefill_relation_def typ_heap_simps' clift_Some_eq_valid split: if_splits) + apply (rule ccorres_return_C) + apply fastforce apply fastforce - apply (clarsimp simp: typ_heap_simps) - apply fastforce - apply ceqv - apply (rename_tac refill refill') - apply (rule ccorres_Guard_Seq) - apply (rule_tac val="rAmount refill" - and xf'=head_amount_' - and R'="{s'. cslift s' (ret__ptr_to_struct_refill_C_' s') = Some refill'}" - in ccorres_symb_exec_r_known_rv) - apply (rule conseqPre, vcg) - apply (clarsimp simp: crefill_relation_def typ_heap_simps') - apply ceqv - apply (rule ccorres_cond_seq) - apply ccorres_rewrite - apply (rule_tac R="sc_at' scPtr" - and R'="\h_val (hrs_mem \t_hrs) \ret__ptr_to_struct_refill_C = refill'\" - in ccorres_cond_strong) - apply (simp add: crefill_relation_def typ_heap_simps' clift_Some_eq_valid split: if_splits) - apply (rule ccorres_return_C) apply fastforce - apply fastforce - apply fastforce - apply (rule ccorres_return_C) - apply (clarsimp simp: crefill_relation_def) - apply simp - apply simp + apply (rule ccorres_return_C) + apply (clarsimp simp: crefill_relation_def) + apply simp + apply simp + apply vcg + apply wpsimp + apply (clarsimp simp: active_sc_at'_rewrite) apply vcg apply wpsimp - apply vcg + apply wpsimp + apply (intro context_conjI) + apply (clarsimp simp: active_sc_at'_rewrite) apply (clarsimp simp: active_sc_at'_def) + apply (rename_tac new_s) apply (normalise_obj_at', rename_tac sc) - apply (frule rf_sr_refill_buffer_relation) + apply (frule_tac s=new_s in rf_sr_refill_buffer_relation) apply (frule (1) obj_at_cslift_sc) apply clarsimp apply (frule (1) sc_ko_at_valid_objs_valid_sc') apply (frule_tac n="scRefillHead sc" in h_t_valid_refill, fastforce+) - apply (clarsimp simp: valid_sched_context'_def) + apply (clarsimp simp: valid_sched_context'_def is_active_sc'_def opt_pred_def split: option.splits) apply (fastforce intro: ko_at'_not_NULL) apply (clarsimp simp: typ_heap_simps' csched_context_relation_def sc_ptr_to_crefill_ptr_def) apply (drule clift_Some_eq_valid[THEN iffD2]) @@ -476,7 +493,7 @@ lemma refill_capacity_ccorres: lemma refill_sufficient_ccorres: "ccorres (\rv rv'. rv = to_bool rv') ret__unsigned_long_' - (active_sc_at' scPtr and valid_objs' and no_0_obj') (\\sc = Ptr scPtr\ \ \\usage = usage\) [] + (valid_objs' and no_0_obj') (\\sc = Ptr scPtr\ \ \\usage = usage\) [] (getRefillSufficient scPtr usage) (Call refill_sufficient_'proc)" apply (cinit simp: readRefillSufficient_def getRefillCapacity_def[symmetric]) apply (ctac add: refill_capacity_ccorres) diff --git a/proof/crefine/RISCV64/Tcb_C.thy b/proof/crefine/RISCV64/Tcb_C.thy index ac68d104a2..805891a848 100644 --- a/proof/crefine/RISCV64/Tcb_C.thy +++ b/proof/crefine/RISCV64/Tcb_C.thy @@ -3599,7 +3599,7 @@ lemma isBlocked_ccorres: lemma sc_released_ccorres: "ccorres (\rv rv'. rv = to_bool rv') ret__unsigned_long_' - (active_sc_at' scPtr and valid_objs') {s. sc_' s = sched_context_Ptr scPtr} [] + valid_objs' {s. sc_' s = sched_context_Ptr scPtr} [] (scReleased scPtr) (Call sc_released_'proc)" apply (cinit lift: sc_' simp: readScReleased_def scActive_def[symmetric]) apply (ctac add: sc_active_ccorres) diff --git a/proof/refine/RISCV64/InterruptAcc_R.thy b/proof/refine/RISCV64/InterruptAcc_R.thy index ca8196b449..f87a1c1aca 100644 --- a/proof/refine/RISCV64/InterruptAcc_R.thy +++ b/proof/refine/RISCV64/InterruptAcc_R.thy @@ -146,17 +146,17 @@ lemma updateTimeStamp_corres[corres]: done lemma no_ofail_readRefillHead[wp]: - "no_ofail (sc_at' scPtr) (readRefillHead scPtr)" - unfolding readRefillHead_def readSchedContext_def - by (wpsimp wp_del: ovalid_readObject) + "no_ofail (active_sc_at' scPtr) (readRefillHead scPtr)" + unfolding readRefillHead_def readSchedContext_def ohaskell_state_assert_def + by (wpsimp wp_del: ovalid_readObject simp: active_sc_at'_def) lemma no_ofail_readRefillCapacity[wp]: - "no_ofail (sc_at' scPtr) (readRefillCapacity scPtr usage)" - unfolding readRefillCapacity_def - by wpsimp + "no_ofail (active_sc_at' scPtr) (readRefillCapacity scPtr usage)" + unfolding readRefillCapacity_def ohaskell_state_assert_def + by (wpsimp simp: active_sc_at'_def) lemma no_ofail_readRefillSufficient[wp]: - "no_ofail (sc_at' scPtr) (readRefillSufficient scPtr usage)" + "no_ofail (active_sc_at' scPtr) (readRefillSufficient scPtr usage)" unfolding readRefillSufficient_def by wpsimp @@ -167,13 +167,15 @@ lemma getRefillHead_corres: "sc_ptr = scPtr \ corres (\rv rv'. refill_map rv' = rv) (valid_objs and pspace_aligned and pspace_distinct - and is_active_sc sc_ptr and sc_refills_sc_at (\refills. refills \ []) sc_ptr) + and is_active_sc sc_ptr and sc_at sc_ptr and sc_refills_sc_at (\refills. refills \ []) sc_ptr) valid_objs' (get_refill_head sc_ptr) (getRefillHead scPtr)" + apply (add_active_sc_at' scPtr) apply (clarsimp simp: get_refill_head_def getRefillHead_def read_refill_head_def - readRefillHead_def getSchedContext_def[symmetric] - read_sched_context_get_sched_context - readSchedContext_def getObject_def[symmetric]) + readRefillHead_def read_sched_context_get_sched_context + readSchedContext_def ohaskell_state_assert_def gets_the_ostate_assert + simp flip: getSchedContext_def getObject_def) + apply (rule corres_stateAssert_ignore[simplified HaskellLib_H.stateAssert_def], simp) apply (rule stronger_corres_guard_imp) apply (rule corres_split[OF get_sc_corres]) apply (rule corres_assert_assume_l) @@ -194,12 +196,14 @@ lemma getRefillCapacity_corres: "sc_ptr = scPtr \ corres (=) (valid_objs and pspace_aligned and pspace_distinct - and is_active_sc sc_ptr and sc_refills_sc_at (\refills. refills \ []) sc_ptr) + and is_active_sc sc_ptr and sc_at sc_ptr and sc_refills_sc_at (\refills. refills \ []) sc_ptr) valid_objs' (get_sc_refill_capacity sc_ptr consumed) (getRefillCapacity scPtr consumed)" - apply (clarsimp simp: get_sc_refill_capacity_def getRefillCapacity_def read_sc_refill_capacity_def - readRefillCapacity_def get_refill_head_def[symmetric] - getRefillHead_def[symmetric]) + apply (add_active_sc_at' scPtr) + apply (clarsimp simp: getRefillCapacity_def get_sc_refill_capacity_def read_sc_refill_capacity_def + readRefillCapacity_def ohaskell_state_assert_def gets_the_ostate_assert + simp flip: get_refill_head_def getRefillHead_def) + apply (rule corres_stateAssert_ignore[simplified HaskellLib_H.stateAssert_def], simp) apply (rule corres_guard_imp) apply (rule corres_split[OF getRefillHead_corres]) apply simp @@ -211,13 +215,15 @@ lemma getRefillSufficient_corres: "sc_ptr = scPtr \ corres (=) (valid_objs and pspace_aligned and pspace_distinct - and is_active_sc sc_ptr and sc_refills_sc_at (\refills. refills \ []) sc_ptr) + and is_active_sc sc_ptr and sc_at sc_ptr and sc_refills_sc_at (\refills. refills \ []) sc_ptr) valid_objs' (get_sc_refill_sufficient sc_ptr consumed) (getRefillSufficient scPtr consumed)" - apply (clarsimp simp: get_sc_refill_sufficient_def getRefillSufficient_def + apply (add_active_sc_at' scPtr) + apply (clarsimp simp: get_sc_refill_sufficient_def getRefillSufficient_def bind_assoc read_sc_refill_sufficient_def readRefillSufficient_def refill_sufficient_def - readRefillCapacity_def + readRefillCapacity_def ohaskell_state_assert_def gets_the_ostate_assert get_refill_head_def[symmetric] getRefillHead_def[symmetric]) + apply (rule corres_stateAssert_ignore[simplified HaskellLib_H.stateAssert_def], simp) apply (rule corres_guard_imp) apply (rule corres_split[OF getRefillHead_corres]) apply simp diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy index 049f0e4c57..b343002b62 100644 --- a/proof/refine/RISCV64/Ipc_R.thy +++ b/proof/refine/RISCV64/Ipc_R.thy @@ -3330,7 +3330,7 @@ lemma tcb_release_enqueue_monadic_rewrite: lemma gets_the_readReadyTime_corres: "sc_ptr = scPtr \ corres (=) - (pspace_aligned and pspace_distinct and valid_objs and is_active_sc scPtr + (pspace_aligned and pspace_distinct and valid_objs and is_active_sc scPtr and sc_at sc_ptr and active_scs_valid) valid_objs' (gets_the (read_ready_time sc_ptr)) (gets_the (readReadyTime scPtr))" @@ -3368,8 +3368,10 @@ lemma getTCBReadyTime_corres: apply (rule corres_symb_exec_r_conj_ex_abs_forwards[OF _ assert_sp]) apply (rule corres_symb_exec_r_conj_ex_abs_forwards[OF _ scActive_sp]) apply (rule corres_symb_exec_r_conj_ex_abs_forwards[OF _ assert_sp]) - apply (corres corres: gets_the_readReadyTime_corres - simp: vs_all_heap_simps obj_at_kh_kheap_simps) + apply (corres corres: gets_the_readReadyTime_corres) + apply (fastforce intro: valid_sched_context_size_objsI + simp: vs_all_heap_simps obj_at_kh_kheap_simps is_sc_obj_def) + apply fastforce apply wpsimp apply wpsimp apply (clarsimp simp: ex_abs_def vs_all_heap_simps) @@ -7078,8 +7080,8 @@ lemma doReplyTransfer_corres: invs and valid_list and scheduler_act_not recvr and current_time_bounded and st_tcb_at active recvr and valid_ready_qs and ready_or_release" - and Q'="invs' and tcb_at' recvr and sc_at' (the scopt)" - and P'="invs' and sc_at' (the scopt') and tcb_at' recvr" + and Q'="invs' and tcb_at' recvr and active_sc_at' (the scopt')" + and P'="invs' and tcb_at' recvr" and P="valid_sched_action and tcb_at recvr and current_time_bounded and sc_tcb_sc_at (\a. a \ None) (the scopt) and active_sc_at (the scopt) and valid_refills (the scopt) and @@ -7181,7 +7183,8 @@ lemma doReplyTransfer_corres: apply (frule (1) valid_objs_ko_at, clarsimp simp: valid_obj_def) apply (clarsimp simp: obj_at_def) apply (frule (1) pspace_relation_absD[OF _ state_relation_pspace_relation]) - apply (clarsimp simp: other_obj_relation_def obj_at'_def sc_relation_def) + apply (clarsimp simp: other_obj_relation_def obj_at'_def + sc_relation_def active_sc_at'_rewrite) apply (clarsimp simp: invs_def valid_state_def valid_pspace_def invs'_def valid_pspace'_def) apply (frule (1) valid_objs_ko_at, clarsimp simp: valid_obj_def) apply (rename_tac sc' n) @@ -7199,8 +7202,9 @@ lemma doReplyTransfer_corres: apply (subst (asm) active_sc_at_equiv) apply (frule (1) active_scs_validE) apply (clarsimp simp: valid_refills_def2 obj_at_def) - apply (clarsimp simp: obj_at_def vs_all_heap_simps active_sc_def - sc_relation_def) + apply (fastforce intro: active_sc_at'_cross + simp: obj_at_def vs_all_heap_simps active_sc_def + sc_relation_def) apply wpsimp apply wpsimp apply (wpsimp wp: refillReady_wp) @@ -7214,6 +7218,12 @@ lemma doReplyTransfer_corres: | clarsimp split: Structures_A.kernel_object.splits)+)[1] apply simp apply clarsimp + apply (erule active_sc_at'_cross) + apply fastforce + apply fastforce + apply (fastforce simp: obj_at_kh_kheap_simps) + apply (fastforce simp: vs_all_heap_simps obj_at_kh_kheap_simps is_sc_obj_def + intro!: valid_sched_context_size_objsI) apply (wpsimp wp: thread_get_wp') apply (wpsimp wp: threadGet_wp) apply (wpsimp wp: gts_wp) @@ -7264,7 +7274,6 @@ lemma doReplyTransfer_corres: apply wpsimp apply (rule_tac Q'="\_. tcb_at' recvr and invs'" in hoare_strengthen_post[rotated]) apply (clarsimp simp: tcb_at'_ex_eq_all invs'_def valid_pspace'_def) - apply (frule (1) tcb_ko_at_valid_objs_valid_tcb', clarsimp simp: valid_tcb'_def) apply (wpsimp wp: sts_invs') apply (rule_tac Q'="\_. invs' and ex_nonz_cap_to' recvr and tcb_at' recvr and (st_tcb_at' (\st. st = Inactive) recvr)" diff --git a/proof/refine/RISCV64/KHeap_R.thy b/proof/refine/RISCV64/KHeap_R.thy index 08b9475127..82357abd01 100644 --- a/proof/refine/RISCV64/KHeap_R.thy +++ b/proof/refine/RISCV64/KHeap_R.thy @@ -4125,21 +4125,13 @@ lemma getObject_sc_wp: projectKOs obj_at'_def in_magnitude_check dest!: readObject_misc_ko_at') -lemma getRefillNext_getSchedContext: - "getRefillNext scPtr index = do sc \ getSchedContext scPtr; - return $ if index = scRefillMax sc - 1 then 0 else index + 1 - od" - apply (clarsimp simp: getRefillNext_def readRefillNext_def readSchedContext_def - getSchedContext_def getObject_def[symmetric] refillNext_def) - done - lemma getRefillNext_wp: "\\s. sc_at' scPtr s \ (\t. ko_at' t scPtr s \ P (refillNext t index) s)\ getRefillNext scPtr index \P\" - apply (simp add: getRefillNext_getSchedContext) + apply (simp add: getRefillNext_def readRefillNext_def readSchedContext_def + flip: getObject_def) apply (wpsimp wp: getObject_sc_wp) - apply (fastforce simp: obj_at'_def refillNext_def split: if_splits) done lemma readRefillSize_SomeD: @@ -5183,4 +5175,8 @@ method add_cur_tcb' = rule_tac Q'="\s'. cur_tcb' s'" in corres_cross_add_guard, fastforce intro!: cur_tcb_cross +method add_active_sc_at' for scPtr :: machine_word = + rule_tac Q'="\s'. active_sc_at' scPtr s'" in corres_cross_add_guard, + fastforce intro!: active_sc_at'_cross + end diff --git a/proof/refine/RISCV64/SchedContextInv_R.thy b/proof/refine/RISCV64/SchedContextInv_R.thy index 78865be38a..f74c55599b 100644 --- a/proof/refine/RISCV64/SchedContextInv_R.thy +++ b/proof/refine/RISCV64/SchedContextInv_R.thy @@ -1054,7 +1054,8 @@ lemma refillUpdate_corres: | wpsimp simp: updateRefillHd_def wp: updateSchedContext_wp)+)[1] apply (rule refillAddTail_corres[simplified dc_def]) - apply (clarsimp simp: refill_map_def) + apply (clarsimp simp: refill_map_def) + apply simp apply (wpsimp wp: get_refill_head_wp) apply (rule getRefillHead_wp) apply (rule_tac Q'="\_ s. sc_at sc_ptr s \ is_active_sc2 sc_ptr s diff --git a/proof/refine/RISCV64/SchedContext_R.thy b/proof/refine/RISCV64/SchedContext_R.thy index df9fc1b4eb..89c3d611a0 100644 --- a/proof/refine/RISCV64/SchedContext_R.thy +++ b/proof/refine/RISCV64/SchedContext_R.thy @@ -779,8 +779,8 @@ lemma updateRefillTl_corres: done lemma readRefillReady_no_ofail[wp]: - "no_ofail (sc_at' t) (readRefillReady t)" - unfolding readRefillReady_def + "no_ofail (active_sc_at' t) (readRefillReady t)" + unfolding readRefillReady_def ohaskell_state_assert_def apply (wpsimp wp: no_ofail_readCurTime) done @@ -793,9 +793,13 @@ lemma refillReady_corres: and valid_objs and pspace_aligned and pspace_distinct) (valid_objs' and valid_refills' scPtr) (get_sc_refill_ready sc_ptr) (refillReady scPtr)" + apply (add_active_sc_at' scPtr) apply (clarsimp simp: refill_ready_def refillReady_def get_sc_refill_ready_def read_sc_refill_ready_def readRefillReady_def readCurTime_def gets_the_ogets + ohaskell_state_assert_def gets_the_ostate_assert simp flip: get_refill_head_def getRefillHead_def getCurTime_def) + apply (rule corres_symb_exec_r[OF _ stateAssert_sp[unfolded HaskellLib_H.stateAssert_def]]; + (solves wpsimp)?) apply (corres corres: getRefillHead_corres getCurTime_corres simp: refill_map_def projection_rewrites) done diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy index 81d9ad5583..244056c324 100644 --- a/proof/refine/RISCV64/Schedule_R.thy +++ b/proof/refine/RISCV64/Schedule_R.thy @@ -2115,9 +2115,9 @@ lemma mergeOverlappingRefills_valid_objs': by (wpsimp wp: updateRefillHd_valid_objs') lemma no_ofail_readRefillNext[wp]: - "no_ofail (sc_at' scPtr) (readRefillNext scPtr index)" - unfolding readRefillNext_def readSchedContext_def - by (wpsimp wp_del: ovalid_readObject) + "no_ofail (active_sc_at' scPtr) (readRefillNext scPtr index)" + unfolding readRefillNext_def readSchedContext_def ohaskell_state_assert_def + by (wpsimp wp_del: ovalid_readObject simp: active_sc_at'_def) lemmas no_fail_getRefillNext[wp] = no_ofail_gets_the[OF no_ofail_readRefillNext, simplified getRefillNext_def[symmetric]] @@ -2147,9 +2147,10 @@ lemma readRefillNext_wp[wp]: by (wpsimp wp: set_sc'.readObject_wp) lemma no_ofail_refillHeadOverlapping: - "no_ofail (sc_at' scp) (refillHeadOverlapping scp)" + "no_ofail (active_sc_at' scp) (refillHeadOverlapping scp)" unfolding refillHeadOverlapping_def - by (wpsimp wp: no_ofail_readSchedContext) + apply (wpsimp wp: no_ofail_readSchedContext simp: active_sc_at'_def) + by (clarsimp simp: obj_at'_def) lemma readRefillIndex_wp[wp]: "\\s. \sc. ko_at' (sc :: sched_context) scp s \ Q (refillIndex idx sc) s\ @@ -2174,11 +2175,12 @@ lemma refillHeadOverlappingLoop_valid_objs': (is "\?pre\_ \_\") apply (clarsimp simp: refillHeadOverlappingLoop_def runReaderT_def) apply (wpsimp wp: valid_whileLoop[where I="\_. ?pre"] mergeOverlappingRefills_valid_objs') - apply (clarsimp simp: active_sc_at'_rewrite) apply (frule no_ofailD[OF no_ofail_refillHeadOverlapping]) apply (fastforce dest: use_ovalid[OF refillHeadOverlapping_refillSize] - intro: valid_objs'_valid_refills') - apply simp+ + intro: valid_objs'_valid_refills' + simp: active_sc_at'_rewrite) + apply (fastforce simp: active_sc_at'_def) + apply fastforce done lemma setRefillHd_valid_objs': @@ -3419,14 +3421,17 @@ crunch getRefillNext for inv[wp]: P lemma refillPopHead_corres: - "corres (\refill refill'. refill = refill_map refill') + "sc_ptr = scPtr \ + corres (\refill refill'. refill = refill_map refill') (\s. sc_at sc_ptr s \ pspace_aligned s \ pspace_distinct s \ sc_refills_sc_at (\refills. 1 < length refills) sc_ptr s \ valid_objs s \ is_active_sc sc_ptr s) (valid_objs' and valid_refills' sc_ptr) - (refill_pop_head sc_ptr) (refillPopHead sc_ptr)" + (refill_pop_head sc_ptr) (refillPopHead scPtr)" + apply (add_active_sc_at' scPtr) apply (rule corres_cross[where Q' = "sc_at' sc_ptr", OF sc_at'_cross_rel], fastforce) apply (clarsimp simp: refill_pop_head_def refillPopHead_def) + apply (rule corres_stateAssert_ignore, simp) apply (rule stronger_corres_guard_imp) apply (rule corres_split[OF getRefillHead_corres], simp) apply (rule corres_symb_exec_r'[OF _ _ hoare_eq_P[OF get_sc_inv']]) @@ -3461,18 +3466,20 @@ lemma refillPopHead_valid_refills'[wp]: refillNext_def) lemma refillHeadOverlapping_simp: - "\sc_at' sc_ptr s'; valid_refills' sc_ptr s'\ \ + "\active_sc_at' sc_ptr s'; valid_refills' sc_ptr s'\ \ refillHeadOverlapping sc_ptr s' = (scs_of' s' ||> (\sc'. Suc 0 < refillSize sc' \ rTime (scRefills sc' ! (if scRefillHead sc' = scRefillMax sc' - Suc 0 then 0 else Suc (scRefillHead sc'))) - \ rTime (refillHd sc') + rAmount (refillHd sc'))) sc_ptr" + \ rTime (refillHd sc') + rAmount (refillHd sc'))) sc_ptr" unfolding refillHeadOverlapping_def + apply (clarsimp simp: active_sc_at'_rewrite) apply (frule no_ofailD[OF no_ofail_readSchedContext]) apply (clarsimp simp: obind_def omonad_defs oliftM_def obj_at'_def readRefillNext_def readRefillSize_def refillIndex_def opt_map_red readSchedContext_def refillSize_def valid_refills'_def in_omonad refillNext_def readRefillHead_def readRefillIndex_def readRefillSingle_def + active_sc_at'_rewrite ostate_assert_def dest!: readObject_ko_at'_sc split: option.splits if_splits) apply fastforce done @@ -3492,10 +3499,10 @@ lemma refill_head_overlapping_simp: done lemma refillHeadOverlapping_corres_eq: - "\(s, s') \ state_relation; sc_at sc_ptr s; sc_at' sc_ptr s'; valid_refills' sc_ptr s'\ + "\(s, s') \ state_relation; sc_at sc_ptr s; active_sc_at' sc_ptr s'; valid_refills' sc_ptr s'\ \ refill_head_overlapping sc_ptr s = refillHeadOverlapping sc_ptr s'" apply (frule no_ofailD[OF no_ofail_refillHeadOverlapping]) - apply clarsimp + apply (clarsimp simp: active_sc_at'_rewrite) apply (drule (2) state_relation_sc_relation) apply (clarsimp simp: obj_at_simps is_sc_obj) apply (rename_tac b n sc sc') @@ -3504,6 +3511,7 @@ lemma refillHeadOverlapping_corres_eq: is_sc_obj sc_relation_def valid_refills'_def refillHd_def neq_Nil_lengthI tl_drop_1 hd_drop_conv_nth refills_map_def hd_map hd_wrap_slice wrap_slice_index refill_map_def opt_map_red opt_pred_def + active_sc_at'_rewrite split: if_split_asm) by linarith+ @@ -3572,7 +3580,7 @@ lemma mergeOverlappingRefills_corres: apply (clarsimp simp: sc_relation_def) apply (clarsimp simp: valid_refills'_def obj_at_simps is_sc_obj opt_map_red opt_pred_def) apply (rule corres_guard_imp) - apply (rule corres_split[OF refillPopHead_corres]) + apply (rule corres_split[OF refillPopHead_corres], simp) apply (rule corres_split[OF updateRefillHd_corres], simp) apply (clarsimp simp: refill_map_def)+ apply (rule updateRefillHd_corres, simp) @@ -3593,15 +3601,16 @@ lemma mergeOverlappingRefills_valid_refills'[wp]: by (wpsimp simp: updateRefillHd_def refillPopHead_def wp: updateSchedContext_wp getRefillNext_wp) lemma no_fail_getRefillHead[wp]: - "no_fail (sc_at' scPtr) (getRefillHead scPtr)" + "no_fail (active_sc_at' scPtr) (getRefillHead scPtr)" apply (wpsimp simp: getRefillHead_def) apply (erule no_ofailD[OF no_ofail_readRefillHead]) done lemma no_fail_refillPopHead[wp]: - "no_fail (sc_at' scPtr) (refillPopHead scPtr)" - by (wpsimp simp: refillPopHead_def obj_at'_def opt_map_def opt_pred_def objBits_simps - wp: getRefillNext_wp) + "no_fail (active_sc_at' scPtr) (refillPopHead scPtr)" + unfolding refillPopHead_def + apply (wpsimp wp: getRefillNext_wp no_fail_stateAssert) + by (clarsimp simp: active_sc_at'_rewrite obj_at'_def opt_map_def opt_pred_def objBits_simps) crunch mergeOverlappingRefills for (no_fail) no_fail[wp] @@ -3651,13 +3660,13 @@ lemma mergeOverlappingRefills_terminates: apply simp apply (rename_tac s) apply (wpsimp wp: mergeOverlappingRefills_length_decreasing mergeOverlappingRefills_valid_objs') - apply (clarsimp simp: active_sc_at'_rewrite) apply (frule_tac s=s in no_ofailD[OF no_ofail_refillHeadOverlapping]) apply clarsimp apply (frule use_ovalid[OF refillHeadOverlapping_refillSize]) - apply (fastforce dest: valid_objs'_valid_refills') + apply (fastforce intro!: valid_objs'_valid_refills' simp: active_sc_at'_rewrite) apply (fastforce dest: valid_objs'_valid_refills' - simp: opt_pred_def opt_map_def valid_refills'_def obj_at'_def) + simp: active_sc_at'_rewrite opt_pred_def opt_map_def valid_refills'_def + obj_at'_def) apply (rule refillSize_wf) done @@ -3684,19 +3693,19 @@ lemma refillHeadOverlappingLoop_corres: Q'="Q and (\s. ((\sc. 1 < refillSize sc) |< scs_of' s) sc_ptr)" for Q]) apply (rule corres_cross_add_abs_guard [where Q="(\s. ((\sc. 1 < length (sc_refills sc)) |< scs_of2 s) sc_ptr)"]) - apply (clarsimp simp: active_sc_at'_rewrite) - apply (drule (2) state_relation_sc_relation) + apply (drule state_relation_sc_relation) + apply fastforce + apply (clarsimp simp: active_sc_at'_rewrite) apply (clarsimp simp: obj_at_simps is_sc_obj valid_refills'_def sc_relation_def - opt_map_red opt_pred_def) + opt_map_red opt_pred_def active_sc_at'_rewrite) apply (corres corres: mergeOverlappingRefills_corres) apply fastforce - apply (clarsimp simp: active_sc_at'_rewrite) + apply clarsimp apply (frule no_ofailD[OF no_ofail_refillHeadOverlapping]) apply clarsimp apply (fastforce dest!: use_ovalid[OF refillHeadOverlapping_refillSize]) apply (wpsimp simp: is_active_sc_rewrite) apply (wpsimp wp: mergeOverlappingRefills_valid_objs') - apply (clarsimp simp: active_sc_at'_rewrite) apply (frule no_ofailD[OF no_ofail_refillHeadOverlapping]) apply (fastforce dest: use_ovalid[OF refillHeadOverlapping_refillSize] simp: active_sc_at'_rewrite opt_pred_def opt_map_def obj_at'_def) @@ -3829,13 +3838,15 @@ lemma no_fail_getRefillSize[wp]: done lemma refillAddTail_corres: - "new = refill_map new' \ + "\new = refill_map new'; sc_ptr = scPtr\ \ corres dc - (sc_at sc_ptr and pspace_aligned and pspace_distinct) + (is_active_sc sc_ptr and sc_at sc_ptr and pspace_aligned and pspace_distinct) (\s'. ((\sc'. refillSize sc' < scRefillMax sc' \ sc_valid_refills' sc') |< scs_of' s') sc_ptr) - (refill_add_tail sc_ptr new) (refillAddTail sc_ptr new')" + (refill_add_tail sc_ptr new) (refillAddTail scPtr new')" + apply (add_active_sc_at' sc_ptr) apply (rule corres_cross[where Q' = "sc_at' sc_ptr", OF sc_at'_cross_rel], fastforce) apply (clarsimp simp: refill_add_tail_def refillAddTail_def) + apply (rule corres_stateAssert_ignore, simp) apply (rule corres_symb_exec_r[OF _ getRefillSize_sp]) apply (rule corres_symb_exec_r[OF _ get_sc_sp'], rename_tac sc) apply (rule corres_symb_exec_r[OF _ assert_sp]) @@ -3898,10 +3909,11 @@ lemma maybeAddEmptyTail_corres: apply (clarsimp simp: obj_at_def is_sc_obj) apply (clarsimp simp: when_def) apply (rule corres_guard_imp) - apply (rule corres_split[OF getRefillHead_corres]) + apply (rule corres_split[OF getRefillHead_corres], simp) apply simp apply (rule refillAddTail_corres) - apply (clarsimp simp: refill_map_def) + apply (clarsimp simp: refill_map_def) + apply simp apply (wpsimp wp: get_refill_head_wp) apply (wpsimp wp: getRefillHead_wp) apply (clarsimp simp: is_active_sc_rewrite[symmetric] obj_at_def is_sc_obj_def) @@ -4228,6 +4240,7 @@ lemma scheduleUsed_corres: apply (corres corres: getRefillFull_corres) apply (rule corres_if_split; (solves simp)?) apply (corres corres: refillAddTail_corres) + apply (fastforce simp: is_active_sc_rewrite) apply (clarsimp simp: refill_map_def obj_at_simps opt_map_red opt_pred_def) apply (corres corres: updateRefillTl_corres simp: refill_map_def) done @@ -4338,7 +4351,7 @@ lemma handleOverrunLoopBody_corres: apply (fastforce simp: refill_map_def sc_relation_def) apply (clarsimp simp: opt_map_red opt_pred_def vs_all_heap_simps obj_at'_def Suc_lessI) apply (rule corres_guard_imp) - apply (rule corres_split[OF refillPopHead_corres]) + apply (rule corres_split[OF refillPopHead_corres], simp) apply (rule scheduleUsed_corres) apply simp apply (clarsimp simp: refill_map_def sc_relation_def) @@ -4349,15 +4362,6 @@ lemma handleOverrunLoopBody_corres: apply (clarsimp simp: obj_at_simps) done -lemma handle_overrun_loop_body_no_fail: - "no_fail (\s. sc_refills_sc_at (\refills. refills \ []) (cur_sc s) s) - (handle_overrun_loop_body usage)" - unfolding handle_overrun_loop_body_def - apply (wpsimp simp: refill_single_def refill_size_def get_refills_def update_refill_hd_def - wp: refill_pop_head_no_fail refill_pop_head_nonempty_refills) - apply (clarsimp simp: sc_at_pred_n_def obj_at_def Suc_lessI) - done - lemma updateRefillIndex_is_active_sc'[wp]: "updateRefillIndex scPtr f index \is_active_sc' scPtr'\" unfolding updateRefillIndex_def diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy index 4e125b6dc2..4e1c630024 100644 --- a/proof/refine/RISCV64/Syscall_R.thy +++ b/proof/refine/RISCV64/Syscall_R.thy @@ -2130,9 +2130,13 @@ lemma checkBudget_corres: (* called when ct_schedulable or in checkBudgetRestart apply simp apply (wpsimp wp: hoare_drop_imp)+ apply (clarsimp simp: invs_def valid_state_def valid_pspace_def) - apply (clarsimp simp: sc_refills_sc_at_def obj_at_def cur_sc_tcb_def sc_tcb_sc_at_def valid_sched_def) + apply (clarsimp simp: obj_at_def sc_tcb_sc_at_def valid_sched_def) + apply (rule conjI) + apply (fastforce intro!: valid_sched_context_size_objsI + simp: vs_all_heap_simps is_sc_obj_def) apply (drule (1) active_scs_validE[rotated]) - apply (clarsimp simp: valid_refills_def vs_all_heap_simps rr_valid_refills_def + apply (frule valid_refills_nonempty_refills) + apply (clarsimp simp: obj_at_kh_kheap_simps vs_all_heap_simps split: if_split_asm) apply clarsimp done diff --git a/proof/refine/RISCV64/TcbAcc_R.thy b/proof/refine/RISCV64/TcbAcc_R.thy index 9bd166d61d..1853eaac81 100644 --- a/proof/refine/RISCV64/TcbAcc_R.thy +++ b/proof/refine/RISCV64/TcbAcc_R.thy @@ -2737,6 +2737,11 @@ crunch inReleaseQueue defs sc_at'_asrt_def: "sc_at'_asrt \ \scPtr s. sc_at' scPtr s" +defs active_sc_at'_asrt_def: + "active_sc_at'_asrt \ \scPtr s. active_sc_at' scPtr s" + +declare active_sc_at'_asrt_def[simp] + lemma ko_at'_valid_tcbs'_valid_tcb': "\ko_at' ko ptr s; valid_tcbs' s\ \ valid_tcb' ko s" by (fastforce simp: valid_tcbs'_def obj_at'_def) diff --git a/spec/design/skel/KernelStateData_H.thy b/spec/design/skel/KernelStateData_H.thy index 1a0a605fce..44668092a4 100644 --- a/spec/design/skel/KernelStateData_H.thy +++ b/spec/design/skel/KernelStateData_H.thy @@ -100,7 +100,7 @@ where return r od" -#INCLUDE_HASKELL SEL4/Model/StateData.lhs decls_only ONLY capHasProperty sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt valid_tcbs'_asrt -#INCLUDE_HASKELL SEL4/Model/StateData.lhs NOT doMachineOp KernelState ReadyQueue ReleaseQueue ReaderM Kernel KernelR getsJust assert stateAssert readStateAssert funOfM condition whileLoop findM funArray newKernelState capHasProperty ifM whenM whileM andM orM sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt valid_tcbs'_asrt +#INCLUDE_HASKELL SEL4/Model/StateData.lhs decls_only ONLY capHasProperty sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt active_sc_at'_asrt valid_tcbs'_asrt +#INCLUDE_HASKELL SEL4/Model/StateData.lhs NOT doMachineOp KernelState ReadyQueue ReleaseQueue ReaderM Kernel KernelR getsJust assert stateAssert readStateAssert funOfM condition whileLoop findM funArray newKernelState capHasProperty ifM whenM whileM andM orM sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt active_sc_at'_asrt valid_tcbs'_asrt end diff --git a/spec/haskell/src/SEL4/Model/StateData.lhs b/spec/haskell/src/SEL4/Model/StateData.lhs index 1183262787..8c13f427fb 100644 --- a/spec/haskell/src/SEL4/Model/StateData.lhs +++ b/spec/haskell/src/SEL4/Model/StateData.lhs @@ -533,6 +533,11 @@ An assert that will say that there is a scheduling context at the given pointer > sc_at'_asrt :: PPtr SchedContext -> KernelState -> Bool > sc_at'_asrt _ _ = True +An assert that will say that there is an active scheduling context at the given pointer + +> active_sc_at'_asrt :: PPtr SchedContext -> KernelState -> Bool +> active_sc_at'_asrt _ _ = True + An assert that will say that valid_tcbs' holds > valid_tcbs'_asrt :: KernelState -> Bool diff --git a/spec/haskell/src/SEL4/Object/SchedContext.lhs b/spec/haskell/src/SEL4/Object/SchedContext.lhs index 776736ccc8..99ebd48d9e 100644 --- a/spec/haskell/src/SEL4/Object/SchedContext.lhs +++ b/spec/haskell/src/SEL4/Object/SchedContext.lhs @@ -104,6 +104,7 @@ This module uses the C preprocessor to select a target architecture. > readRefillHead :: PPtr SchedContext -> KernelR Refill > readRefillHead scPtr = do +> readStateAssert (active_sc_at'_asrt scPtr) "there is an active scheduling context at scPtr" > sc <- readSchedContext scPtr > return $ refillHd sc @@ -115,6 +116,7 @@ This module uses the C preprocessor to select a target architecture. > readRefillTail :: PPtr SchedContext -> KernelR Refill > readRefillTail scPtr = do +> readStateAssert (active_sc_at'_asrt scPtr) "there is an active scheduling context at scPtr" > sc <- readSchedContext scPtr > return $ refillTl sc @@ -197,6 +199,7 @@ This module uses the C preprocessor to select a target architecture. > readRefillNext :: PPtr SchedContext -> Int -> KernelR Int > readRefillNext scPtr index = do +> readStateAssert (active_sc_at'_asrt scPtr) "there is an active scheduling context at scPtr" > sc <- readSchedContext scPtr > return $ refillNext sc index @@ -220,6 +223,7 @@ This module uses the C preprocessor to select a target architecture. > readRefillCapacity :: PPtr SchedContext -> Ticks -> KernelR Ticks > readRefillCapacity scPtr usage = do +> readStateAssert (active_sc_at'_asrt scPtr) "there is an active scheduling context at scPtr" > head <- readRefillHead scPtr > return $ refillCapacity usage head @@ -239,6 +243,7 @@ This module uses the C preprocessor to select a target architecture. > refillPopHead :: PPtr SchedContext -> Kernel Refill > refillPopHead scPtr = do +> stateAssert (active_sc_at'_asrt scPtr) "there is an active scheduling context at scPtr" > head <- getRefillHead scPtr > sc <- getSchedContext scPtr > next <- getRefillNext scPtr (scRefillHead sc) @@ -247,6 +252,7 @@ This module uses the C preprocessor to select a target architecture. > refillAddTail :: PPtr SchedContext -> Refill -> Kernel () > refillAddTail scPtr refill = do +> stateAssert (active_sc_at'_asrt scPtr) "there is an active scheduling context at scPtr" > size <- getRefillSize scPtr > sc <- getSchedContext scPtr > assert (size < scRefillMax sc) "cannot add beyond queue size" @@ -275,6 +281,7 @@ This module uses the C preprocessor to select a target architecture. > readRefillReady :: PPtr SchedContext -> KernelR Bool > readRefillReady scPtr = do +> readStateAssert (active_sc_at'_asrt scPtr) "there is an active scheduling context at scPtr" > head <- readRefillHead scPtr > curTime <- readCurTime > return $ rTime head <= curTime From 1a6fb393c8a171e66682006208b56ed57f410842 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 7 Aug 2024 17:34:02 +0930 Subject: [PATCH 04/14] rt crefine: move tcbReleaseEnqueue_ccorres Moved, along with some associated lemmas, in order for these results to be available for postpone_ccorres. Signed-off-by: Michael McInerney --- proof/crefine/RISCV64/Ipc_C.thy | 337 ++++++++++++++++++++++++++++++++ proof/crefine/RISCV64/Tcb_C.thy | 337 -------------------------------- 2 files changed, 337 insertions(+), 337 deletions(-) diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy index 52392b3cc6..d4a540ab89 100644 --- a/proof/crefine/RISCV64/Ipc_C.thy +++ b/proof/crefine/RISCV64/Ipc_C.thy @@ -4315,6 +4315,343 @@ lemma doIPCTransfer_reply_or_replyslot: crunch handleFaultReply for ksCurDomain[wp]: "\s. P (ksCurDomain s)" +lemma tcbReadyTime_ccorres: + "ccorres (=) ret__unsigned_longlong_' + (tcb_at' tcbPtr and valid_objs' and no_0_obj') + \\tcb = tcb_ptr_to_ctcb_ptr tcbPtr\ hs + (getTCBReadyTime tcbPtr) (Call tcbReadyTime_'proc)" + supply sched_context_C_size[simp del] refill_C_size[simp del] + unfolding getTCBReadyTime_def readTCBReadyTime_def readReadyTime_def gets_the_ohaskell_assert + gets_the_obind threadGet_def[symmetric] + getRefillHead_def[symmetric] + apply (rule ccorres_symb_exec_l'[OF _ _ threadGet_sp]; (solves wpsimp)?) + apply (rule ccorres_symb_exec_l'[OF _ _ assert_sp]; (solves wpsimp)?) + unfolding Nondet_Reader_Option.gets_the_return return_bind fun_app_def scActive_def[symmetric] + apply (rule ccorres_symb_exec_l'[OF _ _ scActive_sp]; (solves wpsimp)?) + apply (rule ccorres_symb_exec_l'[OF _ _ assert_sp]; (solves wpsimp)?) + apply (cinit' lift: tcb_') + apply (rule ccorres_move_c_guard_tcb) + apply (rule_tac xf'="\s. h_val (hrs_mem (t_hrs_' (globals s))) (ret__ptr_to_struct_refill_C_' s)" + in ccorres_split_nothrow_call) + apply (rule refill_head_ccorres) + apply fastforce + apply (clarsimp simp: typ_heap_simps) + apply fastforce + apply ceqv + apply (rule ccorres_Guard) + apply (fastforce intro: ccorres_return_C) + apply wpsimp + apply vcg + apply normalise_obj_at' + apply (rename_tac scPtr sc) + apply (frule (1) tcb_ko_at_valid_objs_valid_tcb') + apply (rule context_conjI) + apply (frule (1) obj_at_cslift_tcb) + apply (clarsimp simp: typ_heap_simps ctcb_relation_def) + apply (prop_tac "sc_at' scPtr s") + apply (fastforce simp: valid_tcb'_def valid_bound_sc'_def active_sc_at'_def) + apply (frule (1) obj_at_cslift_sc) + apply normalise_obj_at' + apply (frule (1) sc_ko_at_valid_objs_valid_sc') + apply (frule rf_sr_refill_buffer_relation) + apply (frule_tac n="scRefillHead sc" in h_t_valid_refill, fastforce+) + apply (clarsimp simp: valid_sched_context'_def obj_at'_def active_sc_at'_def) + apply fastforce + apply (clarsimp simp: typ_heap_simps csched_context_relation_def sc_ptr_to_crefill_ptr_def + h_val_field_from_bytes' crefill_relation_def) + done + +lemma time_after_ccorres: + "ccorres (\rv rv'. rv = to_bool rv') ret__unsigned_long_' + (\s. \tcbPtr. tcbPtrOpt = Some tcbPtr \ (tcb_at' tcbPtr s \ valid_objs' s \ no_0_obj' s)) + (\\new_time = newTime\ \ \\tcb = option_to_ctcb_ptr tcbPtrOpt\) [] + (gets_the (timeAfter tcbPtrOpt newTime)) (Call time_after_'proc)" + (is "ccorres _ _ ?abs _ _ _ _") + supply Collect_const[simp del] + apply (cinit' lift: new_time_' tcb_' simp: timeAfter_def gets_the_if_distrib) + apply csymbr + apply (rule ccorres_cond_seq) + apply ccorres_rewrite + apply (rule ccorres_cond_both'[where Q="?abs" and Q'=\]) + apply (fastforce dest: tcb_at_not_NULL simp: option_to_ctcb_ptr_def split: option.splits) + apply (simp flip: getTCBReadyTime_def) + apply (rule ccorres_rhs_assoc) + apply (ctac add: tcbReadyTime_ccorres) + apply csymbr + apply (rule ccorres_return_C; fastforce) + apply wpsimp + apply vcg + apply (clarsimp simp: gets_the_ogets) + apply (rule ccorres_return_C; fastforce) + by (clarsimp simp: option_to_ctcb_ptr_def split: if_splits option.splits) + +lemma timeAfter_SomeTrueD: + "timeAfter tcbPtrOpt new_time s = Some True + \ \tcbPtr. tcbPtrOpt = Some tcbPtr \ tcb_at' tcbPtr s" + unfolding timeAfter_def readTCBReadyTime_def + by (clarsimp dest!: threadRead_SomeD split: if_splits) + +lemma no_ofail_readReadyTime[wp]: + "no_ofail (active_sc_at' scPtr) (readReadyTime scPtr)" + unfolding readReadyTime_def + by wpsimp + +lemma no_ofail_readTCBReadyTime: + "no_ofail (tcb_at' tcbPtr and active_sc_tcb_at' tcbPtr and valid_objs') (readTCBReadyTime tcbPtr)" + unfolding readTCBReadyTime_def + apply (wpsimp wp: ovalid_threadRead) + apply normalise_obj_at' + apply (frule (1) tcb_ko_at_valid_objs_valid_tcb') + apply (clarsimp simp: opt_pred_def opt_map_def valid_tcb'_def obj_at'_def active_sc_tcb_at'_def + active_sc_at'_def + split: option.splits) + done + +lemma no_ofail_timeAfter: + "no_ofail (\s. \tcbPtr. tcbPtrOpt = Some tcbPtr + \ (tcb_at' tcbPtr s \ active_sc_tcb_at' tcbPtr s \ valid_objs' s)) + (timeAfter tcbPtrOpt newTime)" + unfolding timeAfter_def + apply (wpsimp wp: no_ofail_readTCBReadyTime) + apply (fastforce split: if_splits) + done + +lemma find_time_after_ccorres: + "ccorres (\ptr ptr'. ptr' = option_to_ctcb_ptr ptr) ret__ptr_to_struct_tcb_C_' + ((ksReleaseQueue_asrt and valid_objs' and no_0_obj' and pspace_aligned' and pspace_distinct') + and (\s. \tcbPtr. tcbPtrOpt = Some tcbPtr \ (tcbInReleaseQueue |< tcbs_of' s) tcbPtr)) + (\\new_time = newTime\ \ \\tcb = option_to_ctcb_ptr tcbPtrOpt\) [] + (findTimeAfter tcbPtrOpt newTime) (Call find_time_after_'proc)" + (is "ccorres _ _ (?abs_inv and _) _ _ _ _") + supply sched_context_C_size[simp del] refill_C_size[simp del] + apply (cinit lift: new_time_' tcb_' + simp: runReaderT_def whileAnno_def tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt_def) + apply (rule ccorres_stateAssert) + apply (rule ccorres_symb_exec_r) + apply (rule ccorres_add_return2) + apply (rule ccorres_rhs_assoc2) + apply (rule ccorres_split_nothrow_novcg) + apply (rule_tac r=tcbPtrOpt + and rrel="\ptr ptr'. ptr' = option_to_ctcb_ptr ptr" + and xf=after_' + and cond_xf=ret__unsigned_long_' + and G="\r s. ?abs_inv s + \ (\tcbPtr. (tcbInReleaseQueue |< tcbs_of' s) tcbPtr + \ (tcb_at' tcbPtr s \ active_sc_tcb_at' tcbPtr s)) + \ (\ptr. r = Some ptr \ (tcbInReleaseQueue |< tcbs_of' s) ptr)" + and G'=UNIV + in ccorres_While') + prefer 2 + apply (rule ccorres_guard_imp) + apply (ctac add: time_after_ccorres) + apply fastforce + apply fastforce + apply (rule stronger_ccorres_guard_imp) + apply (rule ccorres_pre_getObject_tcb) + apply (rule ccorres_Guard) + apply (rule ccorres_return[where R=\]) + apply vcg + apply clarsimp + apply (erule CollectD) + apply fastforce + apply (clarsimp simp: typ_heap_simps) + apply (frule timeAfter_SomeTrueD) + apply (clarsimp simp: typ_heap_simps option_to_ctcb_ptr_def opt_pred_def opt_map_def + obj_at'_def ctcb_relation_def + split: option.splits) + apply (wpsimp wp: no_ofail_timeAfter) + apply (wpsimp wp: getTCB_wp) + apply (frule timeAfter_SomeTrueD) + apply (clarsimp simp: ksReleaseQueue_asrt_def list_queue_relation_def) + apply (fastforce dest!: heap_ls_next_in_list simp: opt_pred_def opt_map_def obj_at'_def + split: option.splits) + apply (rule conseqPre, vcg) + apply (fastforce dest: timeAfter_SomeTrueD intro: tcb_at_h_t_valid + simp: option_to_ctcb_ptr_def obj_at'_def) + apply (rule conseqPre, vcg) + apply (clarsimp simp: option_to_ctcb_ptr_def) + apply (case_tac r; clarsimp) + apply (rename_tac tcbPtr) + apply (drule_tac x=tcbPtr in spec) + apply normalise_obj_at' + apply (rename_tac tcb) + apply (frule (1) tcb_ko_at_valid_objs_valid_tcb') + apply (prop_tac "tcbSchedContext tcb \ None") + apply (clarsimp simp: obj_at'_def active_sc_tcb_at'_def opt_pred_def opt_map_def + split: option.splits) + apply clarsimp + apply (rename_tac scPtr) + apply (prop_tac "sc_at' scPtr s") + apply (clarsimp simp: valid_tcb'_def valid_bound_sc'_def obj_at'_def split: option.splits) + apply normalise_obj_at' + apply (rename_tac sc) + apply (frule (1) obj_at_cslift_tcb) + apply (frule (1) obj_at_cslift_sc) + apply normalise_obj_at' + apply (frule (1) sc_ko_at_valid_objs_valid_sc') + apply (frule rf_sr_refill_buffer_relation) + apply (frule_tac n="scRefillHead sc" and scPtr=scPtr in h_t_valid_refill; fastforce?) + apply (clarsimp simp: valid_sched_context'_def obj_at'_def in_omonad + active_sc_tcb_at'_def) + apply (rule conjI) + apply (clarsimp simp: typ_heap_simps) + apply (rule conjI) + apply (clarsimp simp: typ_heap_simps ctcb_relation_def) + apply (rule conjI) + apply (rule disjI2) + apply (rule_tac n="length (scRefills sc)" in array_assertion_shrink_right) + apply (rule sc_at_array_assertion') + apply fastforce + apply (clarsimp simp: typ_heap_simps ctcb_relation_def) + apply (metis ptr_val_def) + apply (clarsimp simp: valid_sched_context'_def MIN_REFILLS_def) + apply (clarsimp simp: valid_sched_context'_def typ_heap_simps csched_context_relation_def + ctcb_relation_def active_sc_tcb_at'_def opt_pred_def + opt_map_def obj_at'_def) + apply (clarsimp simp: typ_heap_simps csched_context_relation_def ctcb_relation_def + sc_ptr_to_crefill_ptr_def) + apply (metis ptr_val_def) + apply ceqv + apply (fastforce intro: ccorres_return_C) + apply wpsimp + apply (clarsimp simp: guard_is_UNIV_def) + apply vcg + apply (rule conseqPre, vcg) + apply clarsimp + apply clarsimp + done + +lemma tcbReleaseEnqueue_ccorres: + "ccorres dc xfdc + (valid_objs' and no_0_obj' and pspace_aligned' and pspace_distinct') + \\tcb = tcb_ptr_to_ctcb_ptr tcbPtr\ [] + (tcbReleaseEnqueue tcbPtr) (Call tcbReleaseEnqueue_'proc)" + apply (cinit lift: tcb_' simp: orM_def ifM_def) + apply (rule ccorres_stateAssert)+ + apply (rule ccorres_symb_exec_l) + apply (rule ccorres_assert2) + apply (thin_tac runnable) + apply (rule ccorres_pre_getObject_tcb) + apply (rule ccorres_assert2) + apply (ctac (no_vcg) add: tcbReadyTime_ccorres) + apply (rule_tac r'=ctcb_queue_relation and xf'=queue_' + in ccorres_split_nothrow[where P=\ and P'=UNIV]) + apply (rule ccorres_from_vcg) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: getReleaseQueue_def gets_def return_def get_def bind_def + rf_sr_def cstate_relation_def Let_def) + apply ceqv + apply (rename_tac aqueue cqueue) + apply (clarsimp simp: bind_assoc simp del: Collect_const) + apply (rule_tac xf'=ret__unsigned_long_' + and val="from_bool (tcbQueueEmpty aqueue)" + and R="\s. \ tcbQueueEmpty aqueue \ tcb_at' (the (tcbQueueHead aqueue)) s + \ (tcbQueueHead aqueue \ None \ tcbQueueEnd aqueue \ None)" + and R'="\\queue = cqueue\" + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply (fastforce dest: tcb_at_not_NULL + simp: ctcb_queue_relation_def option_to_ctcb_ptr_def tcbQueueEmpty_def) + apply ceqv + apply csymbr + apply (rule_tac r'="\rv rv'. rv = to_bool rv'" and xf'=ret__int_' + in ccorres_split_nothrow_novcg) + apply (rule ccorres_cond[where R=\]) + apply (fastforce simp: tcbQueueEmpty_def) + apply (rule ccorres_return_Skip') + apply (ctac (no_vcg) add: tcbReadyTime_ccorres) + apply (rule ccorres_return[where R=\ and R'=UNIV]) + apply (rule conseqPre, vcg) + apply (clarsimp split: if_splits) + apply wpsimp + apply ceqv + apply (clarsimp simp: if_to_top_of_bind) + apply (rule ccorres_cond_seq) + apply (rule_tac Q="\s. \head. tcbQueueHead aqueue = Some head \ tcb_at' head s" + in ccorres_cond_both'[where Q'=\, simplified]) + apply (clarsimp simp: to_bool_def split: if_splits) + apply (simp flip: bind_assoc) + apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow_novcg) + apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) + apply (rule ccorres_call_getter_setter_dc[where P'=UNIV]) + apply (rule ccorres_guard_imp[where Q=Q and A=Q for Q, simplified]) + apply (rule tcb_queue_prepend_ccorres) + apply fastforce + apply clarsimp + apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def + setReleaseQueue_def modify_def get_def put_def bind_def + carch_state_relation_def cmachine_state_relation_def) + apply fastforce + apply wpsimp + apply ceqv + apply (rule_tac P=\ and P'=UNIV in ccorres_from_vcg) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: setReprogramTimer_def rf_sr_def cstate_relation_def Let_def + modify_def get_def put_def bind_def carch_state_relation_def + cmachine_state_relation_def) + apply wpsimp + apply vcg + apply ceqv + apply (rule ccorres_move_c_guard_tcb) + apply ctac + apply wpsimp + apply (clarsimp simp: guard_is_UNIV_def) + apply (clarsimp simp: bind_assoc) + apply (rule ccorres_rhs_assoc)+ + apply (rule ccorres_assert2) + apply (ctac (no_vcg) add: tcbReadyTime_ccorres) + apply (simp add: if_to_top_of_bind) + apply (rule ccorres_cond_seq) + apply (rule_tac Q="\s. \head. tcbQueueHead aqueue = Some head \ tcb_at' head s" + in ccorres_cond_both'[where Q'=\, simplified]) + apply (fastforce split: if_splits) + apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) + apply (rule ccorres_call_getter_setter_dc[where P'=UNIV]) + apply (rule ccorres_guard_imp) + apply (rule tcb_queue_append_ccorres) + apply assumption + apply clarsimp + apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def + setReleaseQueue_def modify_def get_def put_def bind_def + carch_state_relation_def cmachine_state_relation_def) + apply fastforce + apply wpsimp + apply ceqv + apply ctac + apply wpsimp + apply vcg + apply (rule ccorres_rhs_assoc)+ + apply csymbr + apply (clarsimp simp: bind_assoc) + apply (drule Some_to_the) + apply clarsimp + apply (ctac (no_vcg) add: find_time_after_ccorres) + apply (rule ccorres_assert2) + apply (rule ccorres_stateAssert) + apply (ctac (no_vcg) add: tcb_queue_insert_ccorres) + apply ctac + apply wpsimp + apply (rule_tac Q'="\_. tcb_at' tcbPtr and valid_objs'" in hoare_post_imp) + apply (clarsimp simp: findTimeAfter_asrt_def) + apply wpsimp+ + apply (clarsimp simp: guard_is_UNIV_def ctcb_queue_relation_def + option_to_ctcb_ptr_def to_bool_def + split: option.splits) + apply vcg + apply wpsimp+ + apply assumption + apply vcg + apply wpsimp+ + apply (rule conjI) + apply (clarsimp simp: ksReleaseQueue_asrt_def) + apply (frule (3) obj_at'_tcbQueueHead_ksReleaseQueue) + apply (frule (3) obj_at'_tcbQueueEnd_ksReleaseQueue) + apply (frule tcbQueueHead_iff_tcbQueueEnd) + apply (fastforce simp: opt_pred_def opt_map_def obj_at'_def simp: tcbQueueEmpty_def) + apply (fastforce simp: ctcb_queue_relation_def option_to_ctcb_ptr_def tcbQueueEmpty_def + split: option.splits) + done + lemma postpone_ccorres: "ccorres dc xfdc \ \\sc = Ptr scPtr\ [] diff --git a/proof/crefine/RISCV64/Tcb_C.thy b/proof/crefine/RISCV64/Tcb_C.thy index 805891a848..5f5c75cf84 100644 --- a/proof/crefine/RISCV64/Tcb_C.thy +++ b/proof/crefine/RISCV64/Tcb_C.thy @@ -4842,343 +4842,6 @@ sorry (* FIXME RT: decodeTCBInvocation_ccorres apply clarsimp done *) -lemma tcbReadyTime_ccorres: - "ccorres (=) ret__unsigned_longlong_' - (tcb_at' tcbPtr and valid_objs' and no_0_obj') - \\tcb = tcb_ptr_to_ctcb_ptr tcbPtr\ hs - (getTCBReadyTime tcbPtr) (Call tcbReadyTime_'proc)" - supply sched_context_C_size[simp del] refill_C_size[simp del] - apply (clarsimp simp: getTCBReadyTime_def readTCBReadyTime_def readReadyTime_def - gets_the_ohaskell_assert - simp flip: threadGet_def getRefillHead_def scActive_def) - apply (rule ccorres_symb_exec_l'[OF _ _ threadGet_sp]; wpsimp?) - apply (rule ccorres_symb_exec_l'[OF _ _ assert_sp]; wpsimp) - apply (rule ccorres_symb_exec_l'[OF _ _ scActive_sp]; wpsimp) - apply (rule ccorres_symb_exec_l'[OF _ _ assert_sp]; wpsimp) - apply (cinit' lift: tcb_') - apply (rule ccorres_move_c_guard_tcb) - apply (rule_tac xf'="\s. h_val (hrs_mem (t_hrs_' (globals s))) (ret__ptr_to_struct_refill_C_' s)" - in ccorres_split_nothrow_call) - apply (rule refill_head_ccorres) - apply fastforce - apply (clarsimp simp: typ_heap_simps) - apply fastforce - apply ceqv - apply (rule ccorres_Guard) - apply (fastforce intro: ccorres_return_C) - apply wpsimp - apply vcg - apply normalise_obj_at' - apply (rename_tac scPtr sc) - apply (frule (1) tcb_ko_at_valid_objs_valid_tcb') - apply (rule context_conjI) - apply (clarsimp simp: active_sc_at'_def obj_at'_def valid_tcb'_def) - apply (frule (1) obj_at_cslift_tcb) - apply (rule context_conjI) - apply (clarsimp simp: typ_heap_simps ctcb_relation_def) - apply (prop_tac "sc_at' scPtr s") - apply (fastforce simp: valid_tcb'_def valid_bound_sc'_def active_sc_at'_def) - apply (frule (1) obj_at_cslift_sc) - apply normalise_obj_at' - apply (frule (1) sc_ko_at_valid_objs_valid_sc') - apply (frule rf_sr_refill_buffer_relation) - apply (frule_tac n="scRefillHead sc" in h_t_valid_refill, fastforce+) - apply (clarsimp simp: valid_sched_context'_def obj_at'_def active_sc_at'_def) - apply fastforce - apply (clarsimp simp: typ_heap_simps csched_context_relation_def sc_ptr_to_crefill_ptr_def - h_val_field_from_bytes' crefill_relation_def) - done - -lemma time_after_ccorres: - "ccorres (\rv rv'. rv = to_bool rv') ret__unsigned_long_' - (\s. \tcbPtr. tcbPtrOpt = Some tcbPtr \ (tcb_at' tcbPtr s \ valid_objs' s \ no_0_obj' s)) - (\\new_time = newTime\ \ \\tcb = option_to_ctcb_ptr tcbPtrOpt\) [] - (gets_the (timeAfter tcbPtrOpt newTime)) (Call time_after_'proc)" - (is "ccorres _ _ ?abs _ _ _ _") - supply Collect_const[simp del] - apply (cinit' lift: new_time_' tcb_' simp: timeAfter_def gets_the_if_distrib) - apply csymbr - apply (rule ccorres_cond_seq) - apply ccorres_rewrite - apply (rule ccorres_cond_both'[where Q="?abs" and Q'=\]) - apply (fastforce dest: tcb_at_not_NULL simp: option_to_ctcb_ptr_def split: option.splits) - apply (simp flip: getTCBReadyTime_def) - apply (rule ccorres_rhs_assoc) - apply (ctac add: tcbReadyTime_ccorres) - apply csymbr - apply (rule ccorres_return_C; fastforce) - apply wpsimp - apply vcg - apply (clarsimp simp: gets_the_ogets) - apply (rule ccorres_return_C; fastforce) - by (clarsimp simp: option_to_ctcb_ptr_def split: if_splits option.splits) - -lemma timeAfter_SomeTrueD: - "timeAfter tcbPtrOpt new_time s = Some True - \ \tcbPtr. tcbPtrOpt = Some tcbPtr \ tcb_at' tcbPtr s" - unfolding timeAfter_def readTCBReadyTime_def - by (clarsimp dest!: threadRead_SomeD split: if_splits) - -lemma no_ofail_readReadyTime[wp]: - "no_ofail (sc_at' scPtr) (readReadyTime scPtr)" - unfolding readReadyTime_def - by wpsimp - -lemma no_ofail_readTCBReadyTime: - "no_ofail (tcb_at' tcbPtr and active_sc_tcb_at' tcbPtr and valid_objs') (readTCBReadyTime tcbPtr)" - unfolding readTCBReadyTime_def - apply (wpsimp wp: ovalid_threadRead) - apply normalise_obj_at' - apply (frule (1) tcb_ko_at_valid_objs_valid_tcb') - apply (clarsimp simp: opt_pred_def opt_map_def valid_tcb'_def obj_at'_def active_sc_tcb_at'_def - split: option.splits) - done - -lemma no_ofail_timeAfter: - "no_ofail (\s. \tcbPtr. tcbPtrOpt = Some tcbPtr - \ (tcb_at' tcbPtr s \ active_sc_tcb_at' tcbPtr s \ valid_objs' s)) - (timeAfter tcbPtrOpt newTime)" - unfolding timeAfter_def - apply (wpsimp wp: no_ofail_readTCBReadyTime) - apply (fastforce split: if_splits) - done - -lemma find_time_after_ccorres: - "ccorres (\ptr ptr'. ptr' = option_to_ctcb_ptr ptr) ret__ptr_to_struct_tcb_C_' - ((ksReleaseQueue_asrt and valid_objs' and no_0_obj' and pspace_aligned' and pspace_distinct') - and (\s. \tcbPtr. tcbPtrOpt = Some tcbPtr \ (tcbInReleaseQueue |< tcbs_of' s) tcbPtr)) - (\\new_time = newTime\ \ \\tcb = option_to_ctcb_ptr tcbPtrOpt\) [] - (findTimeAfter tcbPtrOpt newTime) (Call find_time_after_'proc)" - (is "ccorres _ _ (?abs_inv and _) _ _ _ _") - supply sched_context_C_size[simp del] refill_C_size[simp del] - apply (cinit lift: new_time_' tcb_' - simp: runReaderT_def whileAnno_def tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt_def) - apply (rule ccorres_stateAssert) - apply (rule ccorres_symb_exec_r) - apply (rule ccorres_add_return2) - apply (rule ccorres_rhs_assoc2) - apply (rule ccorres_split_nothrow_novcg) - apply (rule_tac r=tcbPtrOpt - and rrel="\ptr ptr'. ptr' = option_to_ctcb_ptr ptr" - and xf=after_' - and cond_xf=ret__unsigned_long_' - and G="\r s. ?abs_inv s - \ (\tcbPtr. (tcbInReleaseQueue |< tcbs_of' s) tcbPtr - \ (tcb_at' tcbPtr s \ active_sc_tcb_at' tcbPtr s)) - \ (\ptr. r = Some ptr \ (tcbInReleaseQueue |< tcbs_of' s) ptr)" - and G'=UNIV - in ccorres_While') - prefer 2 - apply (rule ccorres_guard_imp) - apply (ctac add: time_after_ccorres) - apply fastforce - apply fastforce - apply (rule stronger_ccorres_guard_imp) - apply (rule ccorres_pre_getObject_tcb) - apply (rule ccorres_Guard) - apply (rule ccorres_return[where R=\]) - apply vcg - apply clarsimp - apply (erule CollectD) - apply fastforce - apply (clarsimp simp: typ_heap_simps) - apply (frule timeAfter_SomeTrueD) - apply (clarsimp simp: typ_heap_simps option_to_ctcb_ptr_def opt_pred_def opt_map_def - obj_at'_def ctcb_relation_def - split: option.splits) - apply (wpsimp wp: no_ofail_timeAfter) - apply (wpsimp wp: getTCB_wp) - apply (frule timeAfter_SomeTrueD) - apply (clarsimp simp: ksReleaseQueue_asrt_def list_queue_relation_def) - apply (fastforce dest!: heap_ls_next_in_list simp: opt_pred_def opt_map_def obj_at'_def - split: option.splits) - apply (rule conseqPre, vcg) - apply (fastforce dest: timeAfter_SomeTrueD intro: tcb_at_h_t_valid - simp: option_to_ctcb_ptr_def obj_at'_def) - apply (rule conseqPre, vcg) - apply (clarsimp simp: option_to_ctcb_ptr_def) - apply (case_tac r; clarsimp) - apply (rename_tac tcbPtr) - apply (drule_tac x=tcbPtr in spec) - apply normalise_obj_at' - apply (rename_tac tcb) - apply (frule (1) tcb_ko_at_valid_objs_valid_tcb') - apply (prop_tac "tcbSchedContext tcb \ None") - apply (clarsimp simp: obj_at'_def active_sc_tcb_at'_def opt_pred_def opt_map_def - split: option.splits) - apply clarsimp - apply (rename_tac scPtr) - apply (prop_tac "sc_at' scPtr s") - apply (clarsimp simp: valid_tcb'_def valid_bound_sc'_def obj_at'_def split: option.splits) - apply normalise_obj_at' - apply (rename_tac sc) - apply (frule (1) obj_at_cslift_tcb) - apply (frule (1) obj_at_cslift_sc) - apply normalise_obj_at' - apply (frule (1) sc_ko_at_valid_objs_valid_sc') - apply (frule rf_sr_refill_buffer_relation) - apply (frule_tac n="scRefillHead sc" and scPtr=scPtr in h_t_valid_refill; fastforce?) - apply (clarsimp simp: valid_sched_context'_def obj_at'_def in_omonad - active_sc_tcb_at'_def) - apply (rule conjI) - apply (clarsimp simp: typ_heap_simps) - apply (rule conjI) - apply (clarsimp simp: typ_heap_simps ctcb_relation_def) - apply (rule conjI) - apply (rule disjI2) - apply (rule_tac n="length (scRefills sc)" in array_assertion_shrink_right) - apply (rule sc_at_array_assertion') - apply fastforce - apply (clarsimp simp: typ_heap_simps ctcb_relation_def) - apply (metis ptr_val_def) - apply (clarsimp simp: valid_sched_context'_def MIN_REFILLS_def) - apply (clarsimp simp: valid_sched_context'_def typ_heap_simps csched_context_relation_def - ctcb_relation_def active_sc_tcb_at'_def opt_pred_def - opt_map_def obj_at'_def) - apply (clarsimp simp: typ_heap_simps csched_context_relation_def ctcb_relation_def - sc_ptr_to_crefill_ptr_def) - apply (metis ptr_val_def) - apply ceqv - apply (fastforce intro: ccorres_return_C) - apply wpsimp - apply (clarsimp simp: guard_is_UNIV_def) - apply vcg - apply (rule conseqPre, vcg) - apply clarsimp - apply clarsimp - done - -lemma tcbReleaseEnqueue_ccorres: - "ccorres dc xfdc - (valid_objs' and no_0_obj' and pspace_aligned' and pspace_distinct') - \\tcb = tcb_ptr_to_ctcb_ptr tcbPtr\ [] - (tcbReleaseEnqueue tcbPtr) (Call tcbReleaseEnqueue_'proc)" - apply (cinit lift: tcb_' simp: orM_def ifM_def) - apply (rule ccorres_stateAssert)+ - apply (rule ccorres_symb_exec_l) - apply (rule ccorres_assert2) - apply (thin_tac runnable) - apply (rule ccorres_pre_getObject_tcb) - apply (rule ccorres_assert2) - apply (ctac (no_vcg) add: tcbReadyTime_ccorres) - apply (rule_tac r'=ctcb_queue_relation and xf'=queue_' - in ccorres_split_nothrow[where P=\ and P'=UNIV]) - apply (rule ccorres_from_vcg) - apply (rule allI, rule conseqPre, vcg) - apply (clarsimp simp: getReleaseQueue_def gets_def return_def get_def bind_def - rf_sr_def cstate_relation_def Let_def) - apply ceqv - apply (rename_tac aqueue cqueue) - apply (clarsimp simp: bind_assoc simp del: Collect_const) - apply (rule_tac xf'=ret__unsigned_long_' - and val="from_bool (tcbQueueEmpty aqueue)" - and R="\s. \ tcbQueueEmpty aqueue \ tcb_at' (the (tcbQueueHead aqueue)) s - \ (tcbQueueHead aqueue \ None \ tcbQueueEnd aqueue \ None)" - and R'="\\queue = cqueue\" - in ccorres_symb_exec_r_known_rv) - apply (rule conseqPre, vcg) - apply (fastforce dest: tcb_at_not_NULL - simp: ctcb_queue_relation_def option_to_ctcb_ptr_def tcbQueueEmpty_def) - apply ceqv - apply csymbr - apply (rule_tac r'="\rv rv'. rv = to_bool rv'" and xf'=ret__int_' - in ccorres_split_nothrow_novcg) - apply (rule ccorres_cond[where R=\]) - apply (fastforce simp: tcbQueueEmpty_def) - apply (rule ccorres_return_Skip') - apply (ctac (no_vcg) add: tcbReadyTime_ccorres) - apply (rule ccorres_return[where R=\ and R'=UNIV]) - apply (rule conseqPre, vcg) - apply (clarsimp split: if_splits) - apply wpsimp - apply ceqv - apply (clarsimp simp: if_to_top_of_bind) - apply (rule ccorres_cond_seq) - apply (rule_tac Q="\s. \head. tcbQueueHead aqueue = Some head \ tcb_at' head s" - in ccorres_cond_both'[where Q'=\, simplified]) - apply (clarsimp simp: to_bool_def split: if_splits) - apply (simp flip: bind_assoc) - apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow_novcg) - apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) - apply (rule ccorres_call_getter_setter_dc[where P'=UNIV]) - apply (rule ccorres_guard_imp[where Q=Q and A=Q for Q, simplified]) - apply (rule tcb_queue_prepend_ccorres) - apply fastforce - apply clarsimp - apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def - setReleaseQueue_def modify_def get_def put_def bind_def - carch_state_relation_def cmachine_state_relation_def) - apply fastforce - apply wpsimp - apply ceqv - apply (rule_tac P=\ and P'=UNIV in ccorres_from_vcg) - apply (rule allI, rule conseqPre, vcg) - apply (clarsimp simp: setReprogramTimer_def rf_sr_def cstate_relation_def Let_def - modify_def get_def put_def bind_def carch_state_relation_def - cmachine_state_relation_def) - apply wpsimp - apply vcg - apply ceqv - apply (rule ccorres_move_c_guard_tcb) - apply ctac - apply wpsimp - apply (clarsimp simp: guard_is_UNIV_def) - apply (clarsimp simp: bind_assoc) - apply (rule ccorres_rhs_assoc)+ - apply (rule ccorres_assert2) - apply (ctac (no_vcg) add: tcbReadyTime_ccorres) - apply (simp add: if_to_top_of_bind) - apply (rule ccorres_cond_seq) - apply (rule_tac Q="\s. \head. tcbQueueHead aqueue = Some head \ tcb_at' head s" - in ccorres_cond_both'[where Q'=\, simplified]) - apply (fastforce split: if_splits) - apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) - apply (rule ccorres_call_getter_setter_dc[where P'=UNIV]) - apply (rule ccorres_guard_imp) - apply (rule tcb_queue_append_ccorres) - apply assumption - apply clarsimp - apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def - setReleaseQueue_def modify_def get_def put_def bind_def - carch_state_relation_def cmachine_state_relation_def) - apply fastforce - apply wpsimp - apply ceqv - apply ctac - apply wpsimp - apply vcg - apply (rule ccorres_rhs_assoc)+ - apply csymbr - apply (clarsimp simp: bind_assoc) - apply (drule Some_to_the) - apply clarsimp - apply (ctac (no_vcg) add: find_time_after_ccorres) - apply (rule ccorres_assert2) - apply (rule ccorres_stateAssert) - apply (ctac (no_vcg) add: tcb_queue_insert_ccorres) - apply ctac - apply wpsimp - apply (rule_tac Q'="\_. tcb_at' tcbPtr and valid_objs'" in hoare_post_imp) - apply (clarsimp simp: findTimeAfter_asrt_def) - apply wpsimp+ - apply (clarsimp simp: guard_is_UNIV_def ctcb_queue_relation_def - option_to_ctcb_ptr_def to_bool_def - split: option.splits) - apply vcg - apply wpsimp+ - apply assumption - apply vcg - apply wpsimp+ - apply (rule conjI) - apply (clarsimp simp: ksReleaseQueue_asrt_def) - apply (frule (3) obj_at'_tcbQueueHead_ksReleaseQueue) - apply (frule (3) obj_at'_tcbQueueEnd_ksReleaseQueue) - apply (frule tcbQueueHead_iff_tcbQueueEnd) - apply (fastforce simp: opt_pred_def opt_map_def obj_at'_def simp: tcbQueueEmpty_def) - apply (fastforce simp: ctcb_queue_relation_def option_to_ctcb_ptr_def tcbQueueEmpty_def - split: option.splits) - done - lemma decodeSetTimeoutEndpoint_ccorres: "ccorres dc xfdc \ From e6c78f573f03e6cf2abeed1ccc5c37087be28255 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 7 Aug 2024 17:36:51 +0930 Subject: [PATCH 05/14] rt riscv refine: speed up proof of commitTime_corres Signed-off-by: Michael McInerney --- proof/refine/RISCV64/Schedule_R.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy index 244056c324..8a6e0a4044 100644 --- a/proof/refine/RISCV64/Schedule_R.thy +++ b/proof/refine/RISCV64/Schedule_R.thy @@ -4731,7 +4731,7 @@ lemma commitTime_corres: commitTime" supply if_split[split del] apply (rule_tac Q'="\s'. sc_at' (ksCurSc s') s'" in corres_cross_add_guard) - apply (fastforce intro: sc_at_cross simp: state_relation_def) + apply (fastforce intro!: sc_at_cross dest: cursc_relation) apply (clarsimp simp: commit_time_def commitTime_def liftM_def) apply (rule corres_underlying_split[rotated 2, OF gets_sp getCurSc_sp]) apply (corresKsimp corres: getCurSc_corres) From ee7f1f5c550bcb28855f0da200f6a7bb9188979a Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 7 Aug 2024 17:38:18 +0930 Subject: [PATCH 06/14] rt crefine: prove postpone_ccorres Signed-off-by: Michael McInerney --- proof/crefine/RISCV64/Ipc_C.thy | 32 ++++++++++++++++++++++++++++++-- 1 file changed, 30 insertions(+), 2 deletions(-) diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy index d4a540ab89..56bcb1b4c3 100644 --- a/proof/crefine/RISCV64/Ipc_C.thy +++ b/proof/crefine/RISCV64/Ipc_C.thy @@ -4654,9 +4654,37 @@ lemma tcbReleaseEnqueue_ccorres: lemma postpone_ccorres: "ccorres dc xfdc - \ \\sc = Ptr scPtr\ [] + (valid_objs' and no_0_obj' and pspace_aligned' and pspace_distinct') + \\sc = Ptr scPtr\ [] (postpone scPtr) (Call postpone_'proc)" -sorry (* FIXME RT: postpone_ccorres *) + apply (cinit lift: sc_') + apply (rule ccorres_pre_getObject_sc) + apply clarsimp + apply (rename_tac sc) + apply (rule ccorres_assert2) + apply (rule ccorres_move_c_guard_sc) + apply (rule_tac val="option_to_ctcb_ptr (scTCB sc)" + and R="ko_at' sc scPtr" + and R'=UNIV + and xf'=tcb_' + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply (fastforce dest: obj_at_cslift_sc simp: typ_heap_simps csched_context_relation_def) + apply ceqv + apply (ctac (no_vcg) add: tcbSchedDequeue_ccorres) + apply (ctac (no_vcg) add: tcbReleaseEnqueue_ccorres) + apply (rule_tac P=\ and P'=UNIV in ccorres_from_vcg) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: setReprogramTimer_def rf_sr_def cstate_relation_def Let_def + modify_def get_def put_def bind_def carch_state_relation_def + cmachine_state_relation_def) + apply wpsimp + apply wpsimp + apply vcg + apply (rule conjI) + apply (fastforce dest: sc_ko_at_valid_objs_valid_sc' simp: valid_sched_context'_def) + apply (clarsimp simp: option_to_ctcb_ptr_def) + done lemma doReplyTransfer_ccorres[corres]: "ccorres dc xfdc From 6d71f599f329838af297ca37eca5c7b6da87c43e Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 7 Aug 2024 17:40:36 +0930 Subject: [PATCH 07/14] rt crefine: prove schedContext_resume_ccorres Signed-off-by: Michael McInerney --- proof/crefine/RISCV64/Ipc_C.thy | 65 ++++++++++++++++++++++++++++++++- 1 file changed, 63 insertions(+), 2 deletions(-) diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy index 56bcb1b4c3..d53fffaf8b 100644 --- a/proof/crefine/RISCV64/Ipc_C.thy +++ b/proof/crefine/RISCV64/Ipc_C.thy @@ -6018,9 +6018,70 @@ lemma receiveIPC_dequeue_ccorres_helper: lemmas ccorres_pre_getBoundNotification = ccorres_pre_threadGet[where f=tcbBoundNotification, folded getBoundNotification_def] lemma schedContext_resume_ccorres: - "ccorres dc xfdc \ \\sc = Ptr scPtr\ [] + "ccorres dc xfdc + (valid_objs' and no_0_obj' and pspace_aligned' and pspace_distinct') + \\sc = Ptr scPtr\ hs (schedContextResume scPtr) (Call schedContext_resume_'proc)" -sorry (* FIXME RT: schedContext_resume_ccorres *) + supply Collect_const[simp del] + apply (cinit lift: sc_') + apply (rule ccorres_pre_getObject_sc) + apply (clarsimp, rename_tac sc) + apply (rule ccorres_assert2) + apply (rule_tac xf'=ret__int_' + and val="from_bool True" + and R="ko_at' sc scPtr and valid_objs' and no_0_obj'" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg, clarsimp) + apply (frule (1) obj_at_cslift_sc) + apply (clarsimp split: if_splits) + apply ceqv + apply ccorres_rewrite + apply (rule ccorres_rhs_assoc) + apply (rule ccorres_move_c_guard_sc) + apply (ctac add: isSchedulable_corres) + apply csymbr + apply (clarsimp simp: when_def) + apply (rule ccorres_cond[where R=\]) + apply (clarsimp simp: to_bool_def) + apply (rule ccorres_rhs_assoc)+ + apply (ctac add: refill_ready_ccorres) + apply (clarsimp, rename_tac is_ready) + apply csymbr + apply (rule_tac P="to_bool is_ready" in ccorres_cases; clarsimp) + apply (rule ccorres_cond_seq) + apply (rule ccorres_cond_true) + apply (rule ccorres_rhs_assoc)+ + apply (ctac add: refill_sufficient_ccorres) + apply csymbr + apply (rule ccorres_cond[where R=\]) + apply (clarsimp simp: to_bool_def) + apply (ctac add: postpone_ccorres) + apply (rule ccorres_return_Skip) + apply wpsimp + apply (vcg exspec=refill_sufficient_modifies) + apply (rule ccorres_cond_seq) + apply (rule ccorres_cond_false) + apply ccorres_rewrite + apply (rule ccorres_cond_true) + apply (rule ccorres_symb_exec_l') + apply (ctac add: postpone_ccorres) + apply wpsimp+ + apply (vcg exspec=refill_ready_modifies) + apply (rule ccorres_return_Skip) + apply clarsimp + apply (rule_tac Q'="\_. valid_objs' and no_0_obj' and pspace_aligned' and pspace_distinct'" + in hoare_post_imp) + apply clarsimp + apply wpsimp + apply (vcg exspec=isSchedulable_modifies) + apply vcg + apply (rule conjI) + apply (fastforce dest: sc_ko_at_valid_objs_valid_sc' simp: valid_sched_context'_def) + apply (fastforce simp: typ_heap_simps csched_context_relation_def option_to_ctcb_ptr_def + to_bool_def) + done + lemma maybeDonateSchedContext_ccorres: "ccorres dc xfdc From ce90c1ccc13cbd31f5c5d9e55a011eb2cfe7b15d Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 7 Aug 2024 17:41:05 +0930 Subject: [PATCH 08/14] rt crefine: add obj_at_cslift_ntfn Signed-off-by: Michael McInerney --- proof/crefine/RISCV64/Ipc_C.thy | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy index d53fffaf8b..362181008b 100644 --- a/proof/crefine/RISCV64/Ipc_C.thy +++ b/proof/crefine/RISCV64/Ipc_C.thy @@ -6082,6 +6082,18 @@ lemma schedContext_resume_ccorres: to_bool_def) done +lemma obj_at_cslift_ntfn: + fixes P :: "notification \ bool" + shows "\obj_at' P ntfn s; (s, s') \ rf_sr\ \ + \ko ko'. ko_at' ko ntfn s \ P ko \ + cslift s' (Ptr ntfn) = Some ko' \ + cnotification_relation (cslift s') ko ko'" + apply (frule obj_at_ko_at') + apply clarsimp + apply (frule cmap_relation_ntfn) + apply (drule (1) cmap_relation_ko_atD) + apply fastforce + done lemma maybeDonateSchedContext_ccorres: "ccorres dc xfdc From fae09d169f8054666a2cfcbb3ec3419c15f47c6c Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 7 Aug 2024 17:44:44 +0930 Subject: [PATCH 09/14] rt crefine: prove maybeDonateSchedContext_ccorres Signed-off-by: Michael McInerney --- proof/crefine/RISCV64/Ipc_C.thy | 85 ++++++++++++++++++++++++++++++++- 1 file changed, 83 insertions(+), 2 deletions(-) diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy index 362181008b..e2575a8546 100644 --- a/proof/crefine/RISCV64/Ipc_C.thy +++ b/proof/crefine/RISCV64/Ipc_C.thy @@ -6097,9 +6097,90 @@ lemma obj_at_cslift_ntfn: lemma maybeDonateSchedContext_ccorres: "ccorres dc xfdc - \ (\\tcb = tcb_ptr_to_ctcb_ptr tcbPtr\ \ \\ntfnPtr = Ptr ntfnPtr\) [] + (tcb_at' tcbPtr and invs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)) + (\\tcb = tcb_ptr_to_ctcb_ptr tcbPtr\ \ \\ntfnPtr = Ptr ntfnPtr\) hs (maybeDonateSc tcbPtr ntfnPtr) (Call maybeDonateSchedContext_'proc)" -sorry (* FIXME RT: maybeDonateSchedContext_ccorres *) + supply Collect_const[simp del] + apply (cinit lift: tcb_' ntfnPtr_') + apply (rule ccorres_stateAssert) + apply (rule ccorres_pre_threadGet) + apply (rule ccorres_move_c_guard_tcb) + apply (clarsimp simp: when_def) + apply (rule_tac R="obj_at' (\tcb. scOpt = tcbSchedContext tcb) tcbPtr + and valid_objs' and no_0_obj'" + in ccorres_cond) + apply normalise_obj_at' + apply (rename_tac tcb) + apply (frule (1) obj_at_cslift_tcb) + apply (frule (1) tcb_ko_at_valid_objs_valid_tcb') + apply (case_tac "tcbSchedContext tcb"; + clarsimp simp: ctcb_relation_def typ_heap_simps valid_tcb'_def) + apply (clarsimp simp: liftM_def) + apply (rule ccorres_pre_getNotification) + apply (rename_tac ntfn) + apply (rule ccorres_rhs_assoc) + apply (rule ccorres_rhs_assoc) + apply (rule_tac xf'=sc_' + and val="option_to_ptr (ntfnSc ntfn)" + and R="ko_at' ntfn ntfnPtr" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply clarsimp + apply (erule cmap_relationE1 [OF cmap_relation_ntfn]) + apply (erule ko_at_projectKO_opt) + apply (clarsimp simp: typ_heap_simps cnotification_relation_def Let_def) + apply ceqv + apply csymbr + apply (simp add: case_option_If2) + apply (rule ccorres_cond_seq) + apply (rule_tac Q="ko_at' ntfn ntfnPtr and valid_objs' and no_0_obj'" and Q'=\ + in ccorres_cond_both') + apply clarsimp + apply (frule (1) ntfn_ko_at_valid_objs_valid_ntfn') + apply (clarsimp simp: option_to_ptr_def option_to_0_def valid_ntfn'_def + split: option.splits) + apply (simp add: liftM_def) + apply (rule ccorres_pre_getObject_sc) + apply (rule ccorres_move_c_guard_sc) + apply (rule_tac xf'=ret__int_' + and val="from_bool (scTCB rv = None)" + and R="ko_at' ntfn ntfnPtr and ko_at' rv (the (ntfnSc ntfn)) + and valid_objs' and no_0_obj'" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply normalise_obj_at' + apply (frule (1) sc_ko_at_valid_objs_valid_sc') + apply (frule (1) obj_at_cslift_sc) + apply (force dest!: tcb_at_not_NULL + simp: typ_heap_simps' option_to_ctcb_ptr_def csched_context_relation_def + valid_sched_context'_def from_bool_def + split: option.splits bool.splits) + apply ceqv + apply (rule ccorres_cond[where R=\]) + apply fastforce + apply (ctac add: schedContext_donate_ccorres) + apply (ctac add: schedContext_resume_ccorres) + apply clarsimp + apply (drule Some_to_the) + apply (wpsimp wp: schedContextDonate_valid_objs') + apply (vcg exspec=schedContext_donate_modifies) + apply (rule ccorres_return_Skip) + apply vcg + apply ccorres_rewrite + apply (rule ccorres_cond_false) + apply (rule ccorres_return_Skip) + apply vcg + apply (rule ccorres_return_Skip) + apply (clarsimp simp: from_bool_def) + apply (frule invs_valid_objs') + apply safe + apply (clarsimp simp: obj_at'_def) + apply (clarsimp simp: valid_ntfn'_def) + apply (fastforce dest: obj_at_cslift_ntfn simp: typ_heap_simps) + apply (clarsimp simp: option_to_ptr_def option_to_0_def split: option.splits) + done lemma schedContext_bindTCB_ccorres: "ccorres dc xfdc From d54d6585e20fad072f7870a6105f91b8af1c93ff Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 7 Aug 2024 17:46:32 +0930 Subject: [PATCH 10/14] rt haskell+riscv refine+crefine: prove schedContext_bindTCB_ccorres Signed-off-by: Michael McInerney --- proof/crefine/RISCV64/Ipc_C.thy | 116 +++++++++++++++++- proof/refine/RISCV64/Tcb_R.thy | 33 +++-- spec/haskell/src/SEL4/Object/SchedContext.lhs | 3 +- 3 files changed, 131 insertions(+), 21 deletions(-) diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy index e2575a8546..a1dc591bdf 100644 --- a/proof/crefine/RISCV64/Ipc_C.thy +++ b/proof/crefine/RISCV64/Ipc_C.thy @@ -6182,11 +6182,123 @@ lemma maybeDonateSchedContext_ccorres: apply (clarsimp simp: option_to_ptr_def option_to_0_def split: option.splits) done +crunch schedContextResume + for no_0_obj'[wp]: no_0_obj' + (simp: crunch_simps wp: crunch_wps) + lemma schedContext_bindTCB_ccorres: "ccorres dc xfdc - \ (\\tcb = tcb_ptr_to_ctcb_ptr tcbPtr\ \ \\sc = Ptr scPtr\) [] + (tcb_at' tcbPtr and sc_at' scPtr and valid_objs' and no_0_obj' + and pspace_aligned' and pspace_distinct' and pspace_bounded' + and (\s. weak_sch_act_wf (ksSchedulerAction s) s)) + (\\tcb = tcb_ptr_to_ctcb_ptr tcbPtr\ \ \\sc = Ptr scPtr\) hs (schedContextBindTCB scPtr tcbPtr) (Call schedContext_bindTCB_'proc)" -sorry (* FIXME RT: schedContext_bindTCB_ccorres *) + supply Collect_const[simp del] + apply (cinit lift: tcb_' sc_') + apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) + apply (rule ccorres_move_c_guard_tcb)+ + apply (rule_tac Q="\s tcb'. {s'. (s, s') \ rf_sr \ ko_at' tcb' tcbPtr s}" + in threadSet_ccorres_lemma3[where P=\ and P'=\, simplified]) + apply (rule conseqPre, vcg) + apply clarsimp + apply (frule (1) obj_at_cslift_tcb) + apply (fastforce elim!: rf_sr_tcb_update_no_queue_gen2 + simp: typ_heap_simps' ctcb_relation_def option_to_ctcb_ptr_def + tcb_cte_cases_def cteSizeBits_def) + apply clarsimp + apply ceqv + apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) + apply clarsimp + apply (rule updateSchedContext_ccorres_lemma2[where P="\"]) + apply vcg + apply fastforce + apply (clarsimp simp: typ_heap_simps) + apply (rule_tac sc'="scTcb_C_update (\_. tcb_ptr_to_ctcb_ptr tcbPtr) sc'" + in rf_sr_sc_update_no_refill_buffer_update2; + fastforce?) + apply (clarsimp simp: typ_heap_simps' packed_heap_update_collapse_hrs) + apply (clarsimp simp: csched_context_relation_def option_to_ctcb_ptr_def) + apply (fastforce intro: refill_buffer_relation_sc_no_refills_update) + apply ceqv + apply (clarsimp simp: ifCondRefillUnblockCheck_def bind_assoc) + apply (rule ccorres_pre_getObject_sc, rename_tac sc) + apply (rule ccorres_pre_getCurSc, rename_tac cur_sc) + apply (rule ccorres_rhs_assoc2) + apply (rule_tac val="from_bool (scSporadic sc)" + and xf'=ret__int_' + and R="ko_at' sc scPtr and no_0_obj'" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply clarsimp + apply (frule (1) obj_at_cslift_sc) + apply (clarsimp simp: typ_heap_simps csched_context_relation_def to_bool_def + split: if_splits) + apply ceqv + apply (rule ccorres_rhs_assoc2) + apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) + apply (clarsimp simp: when_def) + apply (rule_tac P="scSporadic sc" in ccorres_cases; clarsimp) + apply ccorres_rewrite + apply (rule ccorres_rhs_assoc)+ + apply (rule_tac xf'=ret__unsigned_long_' + and val="from_bool (0 < scRefillMax sc)" + and R="ko_at' sc scPtr and no_0_obj'" + and R'="UNIV" + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg, clarsimp) + apply (frule (1) obj_at_cslift_sc) + apply (clarsimp simp: typ_heap_simps csched_context_relation_def from_bool_def + word_less_nat_alt + split: if_splits bool.splits) + apply ceqv + apply simp + apply csymbr + apply (simp only: if_1_0_0 simp_thms) + apply (rule_tac R="\s. cur_sc = ksCurSc s" in ccorres_cond) + apply (fastforce dest: rf_sr_ksCurSC) + apply (ctac add: refill_unblock_check_ccorres) + apply (rule ccorres_return_Skip) + apply (vcg exspec=sc_active_modifies) + apply ccorres_rewrite + apply (rule ccorres_cond_false) + apply (rule ccorres_return_Skip) + apply ceqv + apply (ctac add: schedContext_resume_ccorres) + apply (ctac add: isSchedulable_ccorres) + apply (clarsimp simp: when_def) + apply (rule ccorres_cond[where R=\]) + apply (fastforce simp: to_bool_def) + apply (ctac add: tcbSchedEnqueue_ccorres) + apply (ctac add: rescheduleRequired_ccorres) + apply wpsimp + apply (vcg exspec=tcbSchedEnqueue_modifies) + apply (rule ccorres_return_Skip) + apply (wpsimp wp: isSchedulable_wp) + apply (vcg exspec=isSchedulable_modifies) + apply (rule_tac Q'="\_ s. valid_objs' s \ no_0_obj' s + \ pspace_aligned' s \ pspace_distinct' s + \ weak_sch_act_wf (ksSchedulerAction s) s \ tcb_at' tcbPtr s" + in hoare_post_imp) + apply fastforce + apply wpsimp + apply (vcg exspec=schedContext_resume_modifies) + apply (wpsimp wp: refillUnblockCheck_invs') + apply (vcg exspec=refill_unblock_check_modifies exspec=sc_sporadic_modifies + exspec=sc_active_modifies) + apply (vcg exspec=sc_sporadic_modifies) + apply (rule_tac Q'="\_ s. valid_objs' s \ no_0_obj' s + \ pspace_aligned' s \ pspace_distinct' s \ pspace_bounded' s + \ weak_sch_act_wf (ksSchedulerAction s) s \ tcb_at' tcbPtr s" + in hoare_post_imp) + apply (fastforce split: if_splits) + apply (wpsimp wp: updateSchedContext_valid_objs'_stTCB_update_Just[simplified] + wp_del: updateSchedContext_valid_objs') + apply vcg + apply wpsimp + apply vcg + apply clarsimp + done lemma schedContext_bindNtfn_ccorres: "ccorres dc xfdc diff --git a/proof/refine/RISCV64/Tcb_R.thy b/proof/refine/RISCV64/Tcb_R.thy index 9e9f282f04..6e2251d367 100644 --- a/proof/refine/RISCV64/Tcb_R.thy +++ b/proof/refine/RISCV64/Tcb_R.thy @@ -1846,13 +1846,12 @@ lemma schedContextBindTCB_corres: apply (simp only: sched_context_bind_tcb_def schedContextBindTCB_def) apply (rule stronger_corres_guard_imp) apply clarsimp - apply (rule corres_symb_exec_r'[where Q'=\]) apply (rule corres_split_nor) apply (clarsimp simp: set_tcb_obj_ref_thread_set sc_relation_def) apply (rule threadset_corres; clarsimp simp: tcb_relation_def inQ_def) apply (rule corres_split_nor) apply (rule_tac f'="scTCB_update (\_. Some t)" - in update_sc_no_reply_stack_update_ko_at'_corres; clarsimp?) + in updateSchedContext_no_stack_update_corres; clarsimp?) apply (clarsimp simp: sc_relation_def refillSize_def) apply (clarsimp simp: objBits_def objBitsKO_def) apply (rule corres_split[OF ifCondRefillUnblockCheck_corres]) @@ -1920,7 +1919,7 @@ lemma schedContextBindTCB_corres: update_sched_context_valid_objs_same valid_ioports_lift update_sched_context_iflive_update update_sched_context_refs_of_update update_sched_context_cur_sc_tcb_None update_sched_context_valid_idle - simp: invs'_def valid_pspace_def + simp: invs'_def valid_pspace_def updateSchedContext_def | rule hoare_vcg_conj_lift update_sched_context_wp)+)[2] apply (clarsimp simp: pred_conj_def) apply ((wp set_tcb_sched_context_valid_ready_qs @@ -1935,8 +1934,9 @@ lemma schedContextBindTCB_corres: threadSet_ct_idle_or_in_cur_domain' threadSet_cur threadSet_valid_replies' sym_heap_sched_pointers_lift threadSet_tcbSchedNexts_of threadSet_tcbSchedPrevs_of threadSet_valid_sched_pointers threadSet_tcbInReleaseQueue threadSet_tcbQueued + threadSet_cap_to | clarsimp simp: tcb_cte_cases_def cteCaps_of_def cteSizeBits_def - | rule hoare_vcg_conj_lift threadSet_wp refl)+ + | rule hoare_vcg_conj_lift hoare_vcg_all_lift hoare_vcg_imp_lift' refl)+ apply (clarsimp simp: invs_def valid_state_def valid_pspace_def valid_sched_def) apply (intro conjI impI allI; (solves clarsimp)?) apply (fastforce simp: valid_obj_def obj_at_def sc_at_ppred_def is_sc_obj_def) @@ -1960,17 +1960,16 @@ lemma schedContextBindTCB_corres: apply (subgoal_tac "ptr \ idle_sc_ptr") apply (clarsimp simp: invs'_def valid_pspace'_def pred_tcb_at'_def sc_at_ppred_def obj_at'_def) apply (intro conjI allI impI; (solves \clarsimp simp: inQ_def comp_def\)?) - apply (fastforce simp: valid_tcb'_def tcb_cte_cases_def obj_at'_def cteSizeBits_def) - subgoal - by (fastforce simp: valid_obj'_def valid_sched_context'_def tcb_cte_cases_def - cteSizeBits_def obj_at'_def refillSize_def) - apply (fastforce elim: valid_objs_sizeE'[OF valid_objs'_valid_objs_size'] - simp: objBits_def objBitsKO_def valid_obj_size'_def - valid_sched_context_size'_def) - apply (fastforce elim: ex_cap_to'_after_update simp: ko_wp_at'_def tcb_cte_cases_def cteSizeBits_def) - apply (fastforce elim: ex_cap_to'_after_update simp: ko_wp_at'_def tcb_cte_cases_def cteSizeBits_def) - apply (clarsimp simp: untyped_ranges_zero_inv_def cteCaps_of_def comp_def) - apply simp + apply (fastforce simp: valid_tcb'_def tcb_cte_cases_def obj_at'_def cteSizeBits_def) + subgoal + by (fastforce simp: valid_obj'_def valid_sched_context'_def tcb_cte_cases_def + cteSizeBits_def obj_at'_def refillSize_def) + apply (fastforce elim: valid_objs_sizeE'[OF valid_objs'_valid_objs_size'] + simp: objBits_def objBitsKO_def valid_obj_size'_def + valid_sched_context_size'_def) + apply (fastforce elim: ex_cap_to'_after_update + simp: ko_wp_at'_def tcb_cte_cases_def cteSizeBits_def) + apply (clarsimp simp: untyped_ranges_zero_inv_def cteCaps_of_def comp_def) apply (fastforce simp: invs'_def dest!: global'_sc_no_ex_cap) apply (clarsimp simp: state_relation_def invs_def valid_state_def valid_pspace_def) apply (subgoal_tac "tcb_at' t s'") @@ -2306,7 +2305,7 @@ lemma schedContextBindTCB_invs': bound_sc_tcb_at' (\sc. sc = None) tcbPtr s \ obj_at' (\sc. scTCB sc = None) scPtr s\ schedContextBindTCB scPtr tcbPtr \\_. invs'\" - apply (simp add: schedContextBindTCB_def) + apply (simp add: schedContextBindTCB_def updateSchedContext_def) apply (subst bind_assoc[symmetric, where m="threadSet _ _"]) apply (rule bind_wp)+ apply wpsimp @@ -2324,7 +2323,7 @@ lemma schedContextBindTCB_invs': valid_irq_handlers_lift'' hoare_vcg_const_imp_lift hoare_vcg_imp_lift' threadSet_valid_replies' threadSet_valid_sched_pointers threadSet_tcbInReleaseQueue sym_heap_sched_pointers_lift threadSet_tcbSchedNexts_of threadSet_tcbSchedPrevs_of - threadSet_tcbQueued + threadSet_tcbQueued hoare_vcg_all_lift hoare_vcg_imp_lift' | clarsimp simp: tcb_cte_cases_def cteCaps_of_def cteSizeBits_def)+ apply (clarsimp simp: invs'_def valid_pspace'_def valid_dom_schedule'_def) by (fastforce simp: pred_tcb_at'_def obj_at'_def diff --git a/spec/haskell/src/SEL4/Object/SchedContext.lhs b/spec/haskell/src/SEL4/Object/SchedContext.lhs index 99ebd48d9e..9c0b6a58b7 100644 --- a/spec/haskell/src/SEL4/Object/SchedContext.lhs +++ b/spec/haskell/src/SEL4/Object/SchedContext.lhs @@ -475,9 +475,8 @@ This module uses the C preprocessor to select a target architecture. > schedContextBindTCB :: PPtr SchedContext -> PPtr TCB -> Kernel () > schedContextBindTCB scPtr tcbPtr = do -> sc <- getSchedContext scPtr > threadSet (\tcb -> tcb { tcbSchedContext = Just scPtr }) tcbPtr -> setSchedContext scPtr $ sc { scTCB = Just tcbPtr } +> updateSchedContext scPtr (\sc -> sc { scTCB = Just tcbPtr }) > ifCondRefillUnblockCheck (Just scPtr) (Just True) (Just False) > schedContextResume scPtr > schedulable <- isSchedulable tcbPtr From edc205744943d4f2f53c7390cd6585c91e5d5c0c Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 7 Aug 2024 17:47:47 +0930 Subject: [PATCH 11/14] rt haskell+riscv refine+crefine: prove schedContext_bindNtfn_ccorres Signed-off-by: Michael McInerney --- proof/crefine/RISCV64/Ipc_C.thy | 60 ++++++++++++++++++- proof/refine/RISCV64/SchedContextInv_R.thy | 8 ++- proof/refine/RISCV64/Syscall_R.thy | 2 +- spec/haskell/src/SEL4/Object/SchedContext.lhs | 10 ++-- 4 files changed, 68 insertions(+), 12 deletions(-) diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy index a1dc591bdf..2943e1de1b 100644 --- a/proof/crefine/RISCV64/Ipc_C.thy +++ b/proof/crefine/RISCV64/Ipc_C.thy @@ -6302,9 +6302,63 @@ lemma schedContext_bindTCB_ccorres: lemma schedContext_bindNtfn_ccorres: "ccorres dc xfdc - \ (\\tcb = tcb_ptr_to_ctcb_ptr tcbPtr\ \ \\sc = Ptr scPtr\) [] - (schedContextBindNtfn scPtr tcbPtr) (Call schedContext_bindNtfn_'proc)" -sorry (* FIXME RT: schedContext_bindNtfn_ccorres *) + (invs' and sc_at' scPtr) (\\ntfn = Ptr ntfnPtr\ \ \\sc = Ptr scPtr\) [] + (schedContextBindNtfn scPtr ntfnPtr) (Call schedContext_bindNtfn_'proc)" + unfolding schedContextBindNtfn_def K_bind_apply + apply (rule ccorres_symb_exec_l'[OF _ _stateAssert_sp]; (solves wpsimp)?) + apply (rule ccorres_symb_exec_l'[OF _ _get_ntfn_sp']; (solves wpsimp)?) + apply (cinit' lift: ntfn_' sc_') + apply (rename_tac ntfn sc' ntfn') + apply (rule_tac P="\s. invs' s \ sym_refs (state_refs_of' s) + \ sc_at' scPtr s \ ko_at' ntfn ntfnPtr s" + and P'=UNIV + in ccorres_split_nothrow_novcg) + apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) + apply (rule allI, rule conseqPre, vcg) + apply clarsimp + apply (frule (1) obj_at_cslift_ntfn) + apply (frule invs_valid_objs') + apply (frule (1) ntfn_ko_at_valid_objs_valid_ntfn') + apply normalise_obj_at' + apply (rule conjI) + apply (erule h_t_valid_clift) + apply (clarsimp simp: setNotification_def split_def) + apply (rule bexI[OF _ setObject_eq]) + apply (simp add: rf_sr_def cstate_relation_def Let_def init_def + cpspace_relation_def update_ntfn_map_tos + csched_context_relation_def typ_heap_simps') + apply clarsimp + apply (intro conjI) + apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) + subgoal + by (fastforce intro!: obj_at'_is_canonical + simp: cnotification_relation_def Let_def + sign_extend_canonical_address + split: ntfn.splits) + apply fastforce + apply (simp add: refill_buffer_relation_def image_def dom_def Let_def typ_heap_simps + update_ntfn_map_tos) + apply (simp add: carch_state_relation_def) + apply (simp add: cmachine_state_relation_def) + apply (simp add: h_t_valid_clift_Some_iff) + apply (simp add: objBits_simps') + apply (simp add: objBits_simps) + apply assumption + apply ceqv + apply (rule updateSchedContext_ccorres_lemma2[where P="\"]) + apply vcg + apply fastforce + apply (clarsimp simp: typ_heap_simps) + apply (rule_tac sc'="scNotification_C_update (\_. Ptr ntfnPtr) sc'a" + in rf_sr_sc_update_no_refill_buffer_update2; + fastforce?) + apply (clarsimp simp: typ_heap_simps' packed_heap_update_collapse_hrs) + apply (clarsimp simp: csched_context_relation_def option_to_ctcb_ptr_def) + apply (fastforce intro: refill_buffer_relation_sc_no_refills_update) + apply wpsimp + apply (clarsimp simp: guard_is_UNIV_def) + apply (clarsimp simp: sym_refs_asrt_def) + done lemma completeSignal_ccorres: notes if_split[split del] diff --git a/proof/refine/RISCV64/SchedContextInv_R.thy b/proof/refine/RISCV64/SchedContextInv_R.thy index f74c55599b..cd70225c75 100644 --- a/proof/refine/RISCV64/SchedContextInv_R.thy +++ b/proof/refine/RISCV64/SchedContextInv_R.thy @@ -374,16 +374,18 @@ lemma decode_sc_ctrl_inv_corres: lemma schedContextBindNtfn_corres: "corres dc (valid_objs and sc_ntfn_sc_at ((=) None) scp - and (obj_at (\ko. \ntfn. ko = Notification ntfn \ ntfn_sc ntfn = None) ntfnp)) + and (obj_at (\ko. \ntfn. ko = Notification ntfn \ ntfn_sc ntfn = None) ntfnp) + and (\s. sym_refs (state_refs_of s)) and pspace_aligned and pspace_distinct) (ntfn_at' ntfnp and sc_at' scp) (sched_context_bind_ntfn scp ntfnp) (schedContextBindNtfn scp ntfnp)" + apply add_sym_refs unfolding sched_context_bind_ntfn_def schedContextBindNtfn_def + apply (rule corres_stateAssert_ignore, simp) apply (clarsimp simp: update_sk_obj_ref_def bind_assoc) apply (rule corres_guard_imp) apply (rule corres_split[OF getNotification_corres]) apply (rule corres_split[OF setNotification_corres]) apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits) - apply (fold updateSchedContext_def) apply (rule updateSchedContext_no_stack_update_corres) apply (clarsimp simp: sc_relation_def refillSize_def) apply (clarsimp simp: opt_map_red) @@ -770,7 +772,7 @@ lemma invokeSchedContext_corres: apply (rule corres_rel_imp) apply (rule schedContextBindNtfn_corres) apply simp - apply clarsimp + apply fastforce apply (clarsimp simp: obj_at'_def) apply (clarsimp split: cap.split capability.split; intro conjI impI allI; clarsimp) apply (rule corres_guard_imp) diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy index 4e1c630024..d11a200687 100644 --- a/proof/refine/RISCV64/Syscall_R.thy +++ b/proof/refine/RISCV64/Syscall_R.thy @@ -882,7 +882,7 @@ lemma schedContextBindNtfn_invs': "\invs' and ex_nonz_cap_to' scPtr and ex_nonz_cap_to' ntfnPtr\ schedContextBindNtfn scPtr ntfnPtr \\_. invs'\" - apply (clarsimp simp: schedContextBindNtfn_def) + apply (clarsimp simp: schedContextBindNtfn_def updateSchedContext_def) apply (wpsimp wp: setSchedContext_invs' setNotification_invs' hoare_vcg_imp_lift' hoare_vcg_all_lift getNotification_wp) apply (rule conjI) diff --git a/spec/haskell/src/SEL4/Object/SchedContext.lhs b/spec/haskell/src/SEL4/Object/SchedContext.lhs index 9c0b6a58b7..22efb17e4a 100644 --- a/spec/haskell/src/SEL4/Object/SchedContext.lhs +++ b/spec/haskell/src/SEL4/Object/SchedContext.lhs @@ -485,11 +485,11 @@ This module uses the C preprocessor to select a target architecture. > rescheduleRequired > schedContextBindNtfn :: PPtr SchedContext -> PPtr Notification -> Kernel () -> schedContextBindNtfn sc ntfn = do -> n <- getNotification ntfn -> setNotification ntfn (n { ntfnSc = Just sc }) -> s <- getSchedContext sc -> setSchedContext sc (s { scNtfn = Just ntfn }) +> schedContextBindNtfn scPtr ntfnPtr = do +> stateAssert sym_refs_asrt "Assert that `sym_refs (state_refs_of' s)` holds" +> ntfn <- getNotification ntfnPtr +> setNotification ntfnPtr (ntfn { ntfnSc = Just scPtr }) +> updateSchedContext scPtr (\sc -> sc { scNtfn = Just ntfnPtr }) > schedContextUnbindTCB :: PPtr SchedContext -> Kernel () > schedContextUnbindTCB scPtr = do From afa5a87cce2f99c8ae905ca6c1990b90540cdbc8 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 7 Aug 2024 17:48:25 +0930 Subject: [PATCH 12/14] rt haskell+riscv refine+crefine: prove maybeReturnSchedContext_ccorres Signed-off-by: Michael McInerney --- proof/crefine/RISCV64/Ipc_C.thy | 111 +++++++++++++++++- proof/refine/RISCV64/Ipc_R.thy | 31 ++--- spec/haskell/src/SEL4/Object/SchedContext.lhs | 3 +- 3 files changed, 118 insertions(+), 27 deletions(-) diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy index 2943e1de1b..e96a042195 100644 --- a/proof/crefine/RISCV64/Ipc_C.thy +++ b/proof/crefine/RISCV64/Ipc_C.thy @@ -6464,9 +6464,116 @@ lemma st_tcb_at'_ko_at': lemma maybeReturnSchedContext_ccorres: "ccorres dc xfdc - \ (\\ntfnPtr = Ptr ntfnPtr\ \ \\tcb = tcb_ptr_to_ctcb_ptr tcbPtr\) [] + (valid_objs' and no_0_obj' and pspace_aligned' and pspace_distinct' + and (\s. weak_sch_act_wf (ksSchedulerAction s) s) + and ntfn_at' ntfnPtr and tcb_at' tcbPtr) + (\\ntfnPtr = Ptr ntfnPtr\ \ \\tcb = tcb_ptr_to_ctcb_ptr tcbPtr\) hs (maybeReturnSc ntfnPtr tcbPtr) (Call maybeReturnSchedContext_'proc)" -sorry (* FIXME RT: maybeReturnSchedContext_ccorres *) + supply Collect_const[simp del] + unfolding maybeReturnSc_def K_bind_apply liftM_def nested_bind fun_app_def + apply (rule ccorres_symb_exec_l'[rotated, OF _ stateAssert_sp]; (solves wpsimp)?) + apply (rule ccorres_symb_exec_l'[rotated, OF _ get_ntfn_sp']; (solves wpsimp)?) + apply (rename_tac ntfn) + apply (rule ccorres_symb_exec_l'[rotated, OF _ threadGet_sp]; (solves wpsimp)?) + apply (cinit' lift: ntfnPtr_' tcb_') + apply (rule ccorres_rhs_assoc2) + apply (rule_tac xf'=sc_' + and val="option_to_ptr (ntfnSc ntfn)" + and R="ko_at' ntfn ntfnPtr" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply clarsimp + apply (frule (1) obj_at_cslift_ntfn) + apply (clarsimp simp: typ_heap_simps cnotification_relation_def Let_def) + apply ceqv + apply clarsimp + apply csymbr + apply (rule_tac P="ntfnSc ntfn \ None" in ccorres_cases) + apply (rule ccorres_cond_seq) + apply (rule ccorres_cond_true) + apply (rule ccorres_move_c_guard_tcb) + apply (rule_tac xf'=ret__int_' + and val="from_bool (ntfnSc ntfn = tscOpt)" + and R="ko_at' ntfn ntfnPtr and obj_at' (\tcb. tcbSchedContext tcb = tscOpt) tcbPtr + and valid_objs' and no_0_obj'" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply normalise_obj_at' + apply (rename_tac scPtr tcb) + apply (frule (1) obj_at_cslift_tcb) + apply (frule (1) ntfn_ko_at_valid_objs_valid_ntfn') + apply (prop_tac "sc_at' scPtr s") + apply (clarsimp simp: valid_ntfn'_def) + apply (frule (1) obj_at_cslift_sc) + apply clarsimp + apply (frule_tac p=scPtr in ko_at'_not_NULL) + apply fastforce + apply (clarsimp simp: ctcb_relation_def typ_heap_simps' from_bool_def + split: bool.splits) + apply (metis option_to_ptr_simps option_to_ptr_not_0) + apply ceqv + apply (simp add: when_def) + apply (rule ccorres_cond[where R=\]) + apply fastforce + apply (rule ccorres_rhs_assoc) + apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) + apply (rule ccorres_move_c_guard_tcb)+ + apply (rule_tac Q="\s tcb. {s'. (s, s') \ rf_sr \ ko_at' tcb tcbPtr s}" + in threadSet_ccorres_lemma3[where P=\ and P'=\, simplified]) + apply (rule conseqPre, vcg) + apply clarsimp + apply (frule (1) obj_at_cslift_tcb[where thread=tcbPtr]) + subgoal + by (fastforce elim!: rf_sr_tcb_update_no_queue_gen2 + simp: typ_heap_simps' ctcb_relation_def option_to_ctcb_ptr_def + tcb_cte_cases_def cteSizeBits_def) + apply clarsimp + apply ceqv + apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) + apply (rule ccorres_move_c_guard_sc) + apply (rule_tac P=\ in updateSchedContext_ccorres_lemma2) + apply vcg + apply fastforce + apply clarsimp + apply (rule_tac sc'="scTcb_C_update (\_. NULL) sc'" + in rf_sr_sc_update_no_refill_buffer_update2; + fastforce?) + apply (clarsimp simp: typ_heap_simps') + apply (clarsimp simp: csched_context_relation_def option_to_ctcb_ptr_def) + apply (fastforce intro: refill_buffer_relation_sc_no_refills_update) + apply ceqv + apply (rule ccorres_pre_getCurThread) + apply (clarsimp, rename_tac cur_thread scPtr) + apply (rule_tac Q="\s. cur_thread = ksCurThread s" and Q'="\" in ccorres_cond_both') + apply (fastforce dest: rf_sr_ksCurThread) + apply (ctac add: rescheduleRequired_ccorres) + apply (rule ccorres_return_Skip) + apply clarsimp + apply (drule Some_to_the) + apply (wpsimp wp: updateSchedContext_valid_objs' hoare_vcg_imp_lift') + apply vcg + apply (wpsimp wp: hoare_vcg_imp_lift') + apply (rule_tac Q'="\_. sc_at' (the (ntfnSc ntfn)) and valid_objs' and no_0_obj' + and pspace_aligned' and pspace_distinct'" + in hoare_post_imp) + apply (clarsimp simp: opt_pred_def opt_map_def valid_obj'_def valid_sched_context'_def + valid_sched_context_size'_def obj_at'_def refillSize_def + objBits_simps + split: option.splits if_splits) + apply wpsimp + apply vcg + apply (rule ccorres_return_Skip) + apply vcg + apply ccorres_rewrite + apply clarsimp + apply (rule ccorres_cond_false) + apply (rule ccorres_return_Skip) + apply (vcg exspec=notification_ptr_get_ntfnSchedContext_modifies) + apply normalise_obj_at' + apply (fastforce dest: ntfn_ko_at_valid_objs_valid_ntfn' simp: valid_ntfn'_def) + done lemma receiveIPC_ccorres[corres]: notes option.case_cong_weak[cong] diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy index b343002b62..01a34ba883 100644 --- a/proof/refine/RISCV64/Ipc_R.thy +++ b/proof/refine/RISCV64/Ipc_R.thy @@ -5086,10 +5086,8 @@ lemma maybeReturnSc_corres: apply (clarsimp simp: tcb_relation_def) apply (rule ball_tcb_cap_casesI; simp) apply (clarsimp simp: tcb_cte_cases_def cteSizeBits_def) - apply (rule_tac Q'="\" in corres_symb_exec_r') apply (rule corres_split) - apply (rule update_sc_no_reply_stack_update_ko_at'_corres - [where f'="scTCB_update (\_. None)"]) + apply (rule updateSchedContext_no_stack_update_corres) apply ((clarsimp simp: sc_relation_def refillSize_def objBits_def objBitsKO_def)+)[4] apply (rule corres_split[OF getCurThread_corres]) @@ -5105,16 +5103,9 @@ lemma maybeReturnSc_corres: apply (wpsimp wp: get_simple_ko_wp getNotification_wp)+ apply (rule valid_tcbs_valid_tcbE, simp, simp) apply (clarsimp simp: valid_tcb_def valid_bound_obj_def split: option.splits) - apply (rule cross_rel_srE [OF tcb_at'_cross_rel [where t=thread]]; simp) apply (rule cross_rel_srE [OF ntfn_at'_cross_rel [where t=ntfnPtr]], simp) - apply clarsimp - apply (subgoal_tac "\tcb. ko_at' (tcb :: tcb) thread s'", clarsimp) - apply (intro conjI) - apply clarsimp - apply (subgoal_tac "valid_tcb' tcb s'") - apply (clarsimp simp: valid_tcb'_def valid_bound_obj'_def split: option.splits) - apply (clarsimp simp: valid_tcbs'_def obj_at'_real_def ko_wp_at'_def) - apply (clarsimp simp: obj_at'_def) + apply (fastforce dest: ko_at'_valid_tcbs'_valid_tcb' + simp: valid_tcb'_def valid_bound_obj'_def split: option.splits) apply (clarsimp simp: sym_refs_asrt_def) done @@ -5141,7 +5132,7 @@ lemma maybeReturnSc_valid_objs'[wp]: "\valid_objs' and pspace_aligned' and pspace_distinct' and pspace_bounded'\ maybeReturnSc ntfnPtr tcbPtr \\_. valid_objs'\" - apply (clarsimp simp: maybeReturnSc_def) + apply (clarsimp simp: maybeReturnSc_def updateSchedContext_def) apply (wpsimp wp: threadSet_valid_objs' threadGet_wp getNotification_wp hoare_vcg_all_lift hoare_vcg_imp_lift' hoare_vcg_disj_lift) apply normalise_obj_at' @@ -5175,7 +5166,7 @@ lemma maybe_return_sc_weak_valid_sched_action: lemma maybeReturnSc_invs': "maybeReturnSc nptr tptr \invs'\" - apply (wpsimp wp: setSchedContext_invs' simp: maybeReturnSc_def) + apply (wpsimp wp: setSchedContext_invs' simp: maybeReturnSc_def updateSchedContext_def) apply (clarsimp simp add: invs'_def split del: if_split) apply (wp threadSet_valid_pspace'T threadSet_sch_actT_P[where P=False, simplified] threadSet_ctes_of threadSet_iflive'T threadSet_ifunsafe'T threadSet_idle'T @@ -6294,7 +6285,7 @@ lemma maybeReturnSc_sym_heap_tcbSCs[wp]: "\sym_heap_tcbSCs and valid_objs'\ maybeReturnSc y t \\_. sym_heap_tcbSCs\" - unfolding maybeReturnSc_def + unfolding maybeReturnSc_def updateSchedContext_def apply (simp add: liftM_def) apply (rule bind_wp[OF _ stateAssert_sp]) apply (rule bind_wp[OF _ get_ntfn_sp']) @@ -6310,14 +6301,8 @@ lemma maybeReturnSc_sym_heap_tcbSCs[wp]: lemma maybeReturnSc_sym_heap_scReplies[wp]: "maybeReturnSc y t \sym_heap_scReplies\" - unfolding maybeReturnSc_def - apply (simp add: liftM_def) - apply (rule bind_wp[OF _ stateAssert_sp]) - apply (rule bind_wp[OF _ get_ntfn_sp']) - apply (wpsimp wp: setSchedContext_scReplies_of | wps)+ - apply (wpsimp wp: threadGet_wp) - apply (clarsimp simp: tcb_at'_ex_eq_all) - apply (drule sym, simp) + unfolding maybeReturnSc_def updateSchedContext_def + apply (wpsimp wp: setSchedContext_scReplies_of threadGet_wp getNotification_wp | wps)+ apply (erule back_subst) apply (rule arg_cong2[where f=sym_heap, OF _ refl], rule ext) apply (clarsimp simp: pred_map_eq_def pred_map_def obj_at'_real_def ko_wp_at'_def opt_map_def) diff --git a/spec/haskell/src/SEL4/Object/SchedContext.lhs b/spec/haskell/src/SEL4/Object/SchedContext.lhs index 22efb17e4a..10ccd8ecbf 100644 --- a/spec/haskell/src/SEL4/Object/SchedContext.lhs +++ b/spec/haskell/src/SEL4/Object/SchedContext.lhs @@ -775,8 +775,7 @@ This module uses the C preprocessor to select a target architecture. > when (nscOpt == tscOpt && nscOpt /= Nothing) $ do > threadSet (\tcb -> tcb { tcbSchedContext = Nothing }) tcbPtr > scPtr <- return $ fromJust nscOpt -> sc <- getSchedContext scPtr -> setSchedContext scPtr (sc { scTCB = Nothing }) +> updateSchedContext scPtr (\sc -> sc { scTCB = Nothing }) > cur <- getCurThread > when (tcbPtr == cur) rescheduleRequired From c7875aa13a9619f05792f139aeccea92562891b7 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 7 Aug 2024 17:48:53 +0930 Subject: [PATCH 13/14] rt crefine: remove duplicate of sc_released_ccorres Signed-off-by: Michael McInerney --- proof/crefine/RISCV64/Schedule_C.thy | 20 -------------------- 1 file changed, 20 deletions(-) diff --git a/proof/crefine/RISCV64/Schedule_C.thy b/proof/crefine/RISCV64/Schedule_C.thy index 73ba8d6331..684165423f 100644 --- a/proof/crefine/RISCV64/Schedule_C.thy +++ b/proof/crefine/RISCV64/Schedule_C.thy @@ -593,26 +593,6 @@ lemma length_scRefills_bounded: apply (clarsimp simp: word_bits_def untypedBits_defs) done -lemma sc_released_ccorres: - "ccorres (\rv rv'. rv = to_bool rv') ret__unsigned_long_' - (active_sc_at' scPtr and valid_objs') \\sc = Ptr scPtr\ [] - (scReleased scPtr) (Call sc_released_'proc)" - apply (cinit simp: readScReleased_def scActive_def[symmetric] gets_the_if_distrib) - apply (ctac add: sc_active_ccorres) - apply (rule ccorres_cond[where R=\]) - apply (clarsimp simp: to_bool_def) - apply (simp flip: refillReady_def) - apply (rule ccorres_add_return2) - apply (ctac add: refill_ready_ccorres) - apply (fastforce intro: ccorres_return_C) - apply wpsimp - apply vcg - apply (fastforce intro: ccorres_return_C) - apply wpsimp - apply vcg - apply clarsimp - done - lemma switchSchedContext_ccorres: "ccorres dc xfdc \ UNIV [] switchSchedContext (Call switchSchedContext_'proc)" sorry (* FIXME RT: switchSchedContext_ccorres *) From acf0754f3205c1c8053ac23cdfc4e26b090685cf Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 7 Aug 2024 17:49:15 +0930 Subject: [PATCH 14/14] rt riscv refine: add sym_refs_asrt_def to global [simp] set Signed-off-by: Michael McInerney --- proof/refine/RISCV64/Detype_R.thy | 1 - proof/refine/RISCV64/Finalise_R.thy | 45 ++++++++++++--------------- proof/refine/RISCV64/Invariants_H.thy | 2 ++ proof/refine/RISCV64/Ipc_R.thy | 16 +++++----- proof/refine/RISCV64/Syscall_R.thy | 2 -- 5 files changed, 29 insertions(+), 37 deletions(-) diff --git a/proof/refine/RISCV64/Detype_R.thy b/proof/refine/RISCV64/Detype_R.thy index a59de5e3a4..7350de1f5a 100644 --- a/proof/refine/RISCV64/Detype_R.thy +++ b/proof/refine/RISCV64/Detype_R.thy @@ -1859,7 +1859,6 @@ lemma deleteObjects_sym_refs': apply clarsimp apply (frule(2) delete_locale.intro, simp_all)[1] apply (simp add: valid_idle'_asrt_def) - apply (simp add: sym_refs_asrt_def) apply (rule subst[rotated, where P="\s. sym_refs (state_refs_of' s)"], erule delete_locale.delete_sym_refs') apply (simp add: field_simps mask_def) diff --git a/proof/refine/RISCV64/Finalise_R.thy b/proof/refine/RISCV64/Finalise_R.thy index a341e510da..6da27392b7 100644 --- a/proof/refine/RISCV64/Finalise_R.thy +++ b/proof/refine/RISCV64/Finalise_R.thy @@ -4110,30 +4110,26 @@ lemma schedContextUnbindNtfn_corres: apply (rule corres_cross[where Q' = "sc_at' sc", OF sc_at'_cross_rel]) apply (simp add: invs_psp_aligned invs_distinct) apply add_sym_refs - apply (rule corres_stateAssert_implied[where P'=\, simplified]) - apply (simp add: get_sc_obj_ref_def) - apply (rule corres_guard_imp) - apply (rule corres_split[OF get_sc_corres]) - apply (rule corres_option_split) - apply (simp add: sc_relation_def) - apply (rule corres_return_trivial) - apply (simp add: update_sk_obj_ref_def bind_assoc) - apply (rule corres_split[OF getNotification_corres]) - apply (rule corres_split[OF setNotification_corres]) - apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits) - apply (rule_tac f'="scNtfn_update (\_. None)" - in update_sc_no_reply_stack_update_ko_at'_corres) - apply (clarsimp simp: sc_relation_def objBits_def objBitsKO_def refillSize_def)+ - apply wpsimp+ - apply (frule invs_valid_objs) - apply (frule (1) valid_objs_ko_at) - apply (clarsimp simp: invs_psp_aligned valid_obj_def valid_sched_context_def - split: option.splits) - apply (clarsimp split: option.splits) - apply (frule (1) scNtfn_sym_refsD[OF ko_at_obj_at', simplified]) - apply clarsimp+ - apply normalise_obj_at' - apply (clarsimp simp: sym_refs_asrt_def) + apply (rule corres_stateAssert_implied[where P'=\, simplified, rotated], simp) + apply (simp add: get_sc_obj_ref_def) + apply (rule corres_guard_imp) + apply (rule corres_split[OF get_sc_corres]) + apply (rule corres_option_split) + apply (simp add: sc_relation_def) + apply (rule corres_return_trivial) + apply (simp add: update_sk_obj_ref_def bind_assoc) + apply (rule corres_split[OF getNotification_corres]) + apply (rule corres_split[OF setNotification_corres]) + apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits) + apply (rule_tac f'="scNtfn_update (\_. None)" + in update_sc_no_reply_stack_update_ko_at'_corres) + apply (clarsimp simp: sc_relation_def objBits_def objBitsKO_def refillSize_def)+ + apply wpsimp+ + apply (frule invs_valid_objs) + apply (frule (1) valid_objs_ko_at) + apply (clarsimp simp: invs_psp_aligned valid_obj_def valid_sched_context_def + split: option.splits) + apply (fastforce dest: scNtfn_sym_refsD[OF ko_at_obj_at', simplified] split: option.splits) done lemma sched_context_maybe_unbind_ntfn_corres: @@ -4178,7 +4174,6 @@ lemma sched_context_maybe_unbind_ntfn_corres: apply (frule (1) ntfnSc_sym_refsD[OF ko_at_obj_at', simplified]) apply clarsimp+ apply normalise_obj_at' - apply (clarsimp simp: sym_refs_asrt_def) apply (wpsimp wp: get_simple_ko_wp getNotification_wp split: option.splits)+ done diff --git a/proof/refine/RISCV64/Invariants_H.thy b/proof/refine/RISCV64/Invariants_H.thy index 26e11faccc..2d97e1f2e8 100644 --- a/proof/refine/RISCV64/Invariants_H.thy +++ b/proof/refine/RISCV64/Invariants_H.thy @@ -374,6 +374,8 @@ definition state_refs_of' :: "kernel_state \ obj_ref \ r defs sym_refs_asrt_def: "sym_refs_asrt \ \s. sym_refs (state_refs_of' s)" +declare sym_refs_asrt_def[simp] + definition live_sc' :: "sched_context \ bool" where "live_sc' sc \ bound (scTCB sc) \ scTCB sc \ Some idle_thread_ptr \ bound (scYieldFrom sc) \ bound (scNtfn sc) \ scReply sc \ None" diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy index 01a34ba883..14fce7fc11 100644 --- a/proof/refine/RISCV64/Ipc_R.thy +++ b/proof/refine/RISCV64/Ipc_R.thy @@ -4309,7 +4309,6 @@ lemma sendSignal_corres: defer apply (wp get_simple_ko_ko_at get_ntfn_ko')+ apply (simp add: invs_valid_objs invs_valid_objs')+ - apply (clarsimp simp: sym_refs_asrt_def) apply add_sym_refs apply (case_tac "ntfn_obj ntfn"; simp) \ \IdleNtfn\ @@ -5181,14 +5180,13 @@ lemma maybeReturnSc_invs': apply (rule_tac x=tcb in exI) apply (clarsimp simp: invs'_def inQ_def comp_def eq_commute[where a="Some _"]) apply (intro conjI impI allI; clarsimp?) - apply (clarsimp simp: untyped_ranges_zero_inv_def cteCaps_of_def comp_def) - apply (clarsimp simp: valid_idle'_def obj_at'_def sym_refs_asrt_def) - apply (drule_tac ko="tcb" and p=tptr in sym_refs_ko_atD'[rotated]) - apply (fastforce simp: obj_at'_def) - apply (clarsimp simp: ko_wp_at'_def refs_of_rev') - apply (fastforce elim: if_live_then_nonz_capE' simp: ko_wp_at'_def live_sc'_def) - apply (fastforce simp: valid_pspace'_def valid_obj'_def valid_sched_context'_def refillSize_def) - apply (fastforce simp: valid_obj'_def valid_sched_context_size'_def objBits_def objBitsKO_def) + apply (clarsimp simp: untyped_ranges_zero_inv_def cteCaps_of_def comp_def) + apply (drule_tac ko="tcb" and p=tptr in sym_refs_ko_atD'[rotated]) + apply (fastforce simp: obj_at'_def) + apply (clarsimp simp: ko_wp_at'_def refs_of_rev') + apply (fastforce elim: if_live_then_nonz_capE' simp: ko_wp_at'_def live_sc'_def) + apply (fastforce simp: valid_pspace'_def valid_obj'_def valid_sched_context'_def refillSize_def) + apply (fastforce simp: valid_obj'_def valid_sched_context_size'_def objBits_def objBitsKO_def) done crunch doIPCTransfer diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy index d11a200687..5763d5238e 100644 --- a/proof/refine/RISCV64/Syscall_R.thy +++ b/proof/refine/RISCV64/Syscall_R.thy @@ -443,9 +443,7 @@ lemma performInvocation_corres: apply (rule corres_returnOkTT) apply simp apply wpsimp+ - apply (clarsimp simp: sym_refs_asrt_def) - apply (clarsimp simp: liftE_bindE) apply (rule corres_guard_imp) apply (rule corres_split[OF getCurThread_corres]) apply simp