rt haskell+riscv refine+crefine: prove schedContext_donate_ccorres

This includes a small change to the Haskell which rephrases schedContextDonate, while preserving semantics, in order to make the proof of the ccorres rule easier. Signed-off-by: Michael McInerney <[email protected]>
seL4 · Aug 8, 2024 · 83a161d · 83a161d
1 parent 32c0ecc
commit 83a161d
Show file tree

Hide file tree

Showing 9 changed files with 125 additions and 79 deletions.
diff --git a/proof/crefine/RISCV64/IpcCancel_C.thy b/proof/crefine/RISCV64/IpcCancel_C.thy
@@ -1877,7 +1877,7 @@ lemma rescheduleRequired_ccorres:
   "ccorres dc xfdc
      ((\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and no_0_obj'
       and pspace_aligned' and pspace_distinct')
-     UNIV []
+     UNIV hs
      rescheduleRequired (Call rescheduleRequired_'proc)"
   supply if_split[split del]
   apply cinit

diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy
@@ -5009,11 +5009,101 @@ lemma reply_push_ccorres:
      (replyPush callerPtr calleePtr replyPtr canDonate) (Call reply_push_'proc)"
 sorry (* FIXME RT: reply_push_ccorres *)
 
+(* Note that valid_objs' can be removed from the Haskell guard by asserting valid_objs' within
+   schedContextDonate *)
 lemma schedContext_donate_ccorres:
   "ccorres dc xfdc
-     \<top> (\<lbrace>\<acute>sc = Ptr callerPtr\<rbrace> \<inter> \<lbrace>\<acute>to = tcb_ptr_to_ctcb_ptr tcbPtr\<rbrace>) []
+     (sc_at' scPtr and tcb_at' tcbPtr and valid_objs' and no_0_obj'
+      and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and pspace_aligned' and pspace_distinct')
+     (\<lbrace>\<acute>sc = Ptr scPtr\<rbrace> \<inter> \<lbrace>\<acute>to = tcb_ptr_to_ctcb_ptr tcbPtr\<rbrace>) []
      (schedContextDonate scPtr tcbPtr) (Call schedContext_donate_'proc)"
-sorry (* FIXME RT: schedContext_donate_ccorres *)
+  (is "ccorres _ _ ?abs _ _ _ _")
+  apply (cinit lift: sc_' to_')
+   apply (rule ccorres_pre_getObject_sc, rename_tac sc)
+   apply (rule ccorres_move_c_guard_sc)
+   apply (rule_tac xf'=from_'
+               and val="option_to_ctcb_ptr (scTCB sc)"
+               and R="ko_at' sc scPtr"
+               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: csched_context_relation_def typ_heap_simps)
+     apply ceqv
+    apply (clarsimp simp: when_def)
+    apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow)
+        apply (rule_tac Q="no_0_obj' and ko_at' sc scPtr and valid_objs'"
+                    and Q'="\<lambda>s'. from_' s' = option_to_ctcb_ptr (scTCB sc)"
+                     in ccorres_cond_both')
+          apply (fastforce dest: tcb_at_not_NULL sc_ko_at_valid_objs_valid_sc'
+                           simp: option_to_ctcb_ptr_def valid_sched_context'_def
+                          split: option.splits)
+         apply (rule ccorres_rhs_assoc)+
+         apply (ctac add: tcbSchedDequeue_ccorres)
+           apply (ctac add: tcbReleaseRemove_ccorres)
+             apply (rule ccorres_move_c_guard_tcb)
+             apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow)
+                 apply (rule_tac R="{s'. from_' s' = option_to_ctcb_ptr (scTCB sc)}"
+                             and P'="valid_objs' and no_0_obj' and ko_at' sc scPtr"
+                              in threadSet_ccorres_lemma4[where P=\<top>])
+                  apply vcg
+                 subgoal
+                   by (fastforce intro!: rf_sr_tcb_update_no_queue_gen2
+                                   simp: typ_heap_simps' option_to_ctcb_ptr_def tcb_cte_cases_def
+                                         cteSizeBits_def ctcb_relation_def)
+                apply ceqv
+               apply (rule ccorres_pre_getCurThread)
+               apply (rule ccorres_pre_getSchedulerAction)
+               apply (rule_tac Q="\<lambda>s. action = ksSchedulerAction s \<and> cur = ksCurThread s
+                                      \<and> valid_objs' s \<and> no_0_obj' s \<and> ko_at' sc scPtr s"
+                           and Q'="\<lambda>s'. from_' s' = option_to_ctcb_ptr (scTCB sc)"
+                            in ccorres_cond_both')
+                 apply clarsimp
+                 apply (prop_tac "tcb_at' (the (scTCB sc)) s")
+                  apply (fastforce dest!: sc_ko_at_valid_objs_valid_sc'
+                                    simp: valid_sched_context'_def)
+                 subgoal
+                   by (force dest: tcb_at_not_NULL tcb_at_1
+                             simp: rf_sr_def cstate_relation_def Let_def option_to_ctcb_ptr_def
+                                   cscheduler_action_relation_def
+                            split: scheduler_action.splits)
+                apply (ctac add: rescheduleRequired_ccorres)
+               apply (rule ccorres_return_Skip)
+              apply (rule_tac Q'="\<lambda>_. ?abs and ko_at' sc scPtr" in hoare_post_imp)
+               apply clarsimp
+              apply wpsimp
+             apply vcg
+            apply wpsimp
+           apply (vcg exspec=tcbReleaseRemove_modifies)
+          apply wpsimp
+         apply (vcg exspec=tcbSchedDequeue_modifies)
+        apply (rule ccorres_return_Skip)
+       apply ceqv
+      apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow)
+          apply (rule updateSchedContext_ccorres_lemma2[where P=\<top>])
+            apply vcg
+           apply simp
+          apply (fastforce intro: rf_sr_sc_update_no_refill_buffer_update2
+                                  refill_buffer_relation_sc_no_refills_update
+                            simp: typ_heap_simps' csched_context_relation_def option_to_ctcb_ptr_def)
+         apply ceqv
+        apply (rule threadSet_ccorres_lemma2[where P=\<top>])
+         apply vcg
+        subgoal
+          by (fastforce intro!: rf_sr_tcb_update_no_queue_gen2
+                          simp: typ_heap_simps' tcb_cte_cases_def cteSizeBits_def ctcb_relation_def)
+       apply wpsimp
+      apply vcg
+     apply (wpsimp wp: hoare_drop_imps)
+    apply (vcg exspec=tcbSchedDequeue_modifies
+               exspec=tcbReleaseRemove_modifies
+               exspec=rescheduleRequired_modifies)
+   apply vcg
+  apply normalise_obj_at'
+  apply (frule (1) sc_ko_at_valid_objs_valid_sc')
+  apply (clarsimp simp: valid_sched_context'_def option_to_ctcb_ptr_def split: option.splits)
+  done
 
 lemma sendIPC_ccorres [corres]:
   "ccorres dc xfdc (invs' and st_tcb_at' simple' thread

diff --git a/proof/crefine/RISCV64/IsolatedThreadAction.thy b/proof/crefine/RISCV64/IsolatedThreadAction.thy
@@ -920,7 +920,7 @@ lemma tcbReleaseRemove_tcbPriority[wp]:
 
 lemma schedContextDonate_tcbPriority[wp]:
   "schedContextDonate scPtr tcbPtr \<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace>"
-  apply (simp add: schedContextDonate_def)
+  apply (simp add: schedContextDonate_def updateSchedContext_def)
   by (wpsimp wp: hoare_drop_imps)
 
 lemma asUser_obj_at_unchangedT:

diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy
@@ -6178,35 +6178,6 @@ lemma bindScReply_valid_idle':
   unfolding bindScReply_def
   by (wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_all_lift set_reply'.obj_at')
 
-lemma replyPush_valid_idle':
-  "\<lbrace>valid_idle'
-    and valid_pspace'
-    and (\<lambda>s. callerPtr \<noteq> ksIdleThread s)
-    and sym_heap_tcbSCs\<rbrace>
-   replyPush callerPtr calleePtr replyPtr canDonate
-   \<lbrace>\<lambda>_. valid_idle'\<rbrace>"
-  apply (simp only: replyPush_def)
-  supply if_split [split del]
-  apply wpsimp
-         apply (wpsimp wp: schedContextDonate_valid_idle' bindScReply_valid_idle')+
-       apply (wpsimp wp: hoare_vcg_if_lift2 hoare_vcg_imp_lift')
-      apply (wpsimp wp: hoare_vcg_if_lift2 hoare_vcg_imp_lift')
-     apply (wpsimp wp: threadGet_wp)+
-  apply (clarsimp simp: tcb_at'_ex_eq_all valid_pspace'_def)
-  apply (subgoal_tac "\<forall>kob. valid_reply' kob s \<longrightarrow> valid_reply' (replyTCB_update (\<lambda>_. Some callerPtr) kob) s")
-   apply (subgoal_tac "calleePtr \<noteq> idle_thread_ptr", simp)
-    apply (subgoal_tac "y \<noteq> idle_sc_ptr", simp)
-     apply (erule (3) not_idle_scTCB)
-     apply (frule (1) tcb_ko_at_valid_objs_valid_tcb')
-     apply (clarsimp simp: valid_tcb'_def)
-    apply (frule (2) not_idle_tcbSC[where p=callerPtr])
-      apply (clarsimp simp: valid_idle'_def)
-     apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def)
-    apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def)
-   apply (clarsimp simp: valid_idle'_def idle_tcb'_def obj_at'_real_def ko_wp_at'_def)
-  apply (clarsimp simp: valid_reply'_def)
-  done
-
 lemma replyPush_untyped_ranges_zero'[wp]:
   "replyPush callerPtr calleePtr replyPtr canDonate \<lbrace>untyped_ranges_zero'\<rbrace>"
   apply (clarsimp simp: untyped_ranges_zero_inv_null_filter_cteCaps_of)
@@ -6724,8 +6695,7 @@ lemma si_invs'_helper2:
         od)
   \<lbrace>\<lambda>b s. invs' s \<and> tcb_at' d s \<and> ex_nonz_cap_to' d s
          \<and> st_tcb_at' (Not \<circ> is_BlockedOnReply) d s\<rbrace>"
-  apply (wpsimp wp: ex_nonz_cap_to_pres' schedContextDonate_invs' replyPush_invs'
-                    replyPush_valid_idle' sts_invs_minor' schedContextDonate_valid_idle'
+  apply (wpsimp wp: ex_nonz_cap_to_pres' schedContextDonate_invs' replyPush_invs' sts_invs_minor'
                     replyPush_st_tcb_at'_not_caller sts_st_tcb' threadGet_wp)
   apply (frule_tac P'="(\<lambda>st'. \<forall>rptr. st' \<noteq> BlockedOnReply rptr)" in pred_tcb'_weakenE)
    apply (clarsimp simp: is_BlockedOnReply_def)

diff --git a/proof/refine/RISCV64/KHeap_R.thy b/proof/refine/RISCV64/KHeap_R.thy
@@ -4900,6 +4900,12 @@ lemma setSchedContext_scReplies_of:
   apply (erule back_subst[where P=P], rule ext)
   by (clarsimp simp: opt_map_def)
 
+lemma updateSchedContext_scReplies_of:
+  "(\<And>sc. scReply (f sc) = scReply sc) \<Longrightarrow> updateSchedContext scPtr f \<lbrace>\<lambda>s. P' (scReplies_of s)\<rbrace>"
+  apply (wpsimp simp: updateSchedContext_def wp: setSchedContext_scReplies_of)
+  apply (auto elim!: rsubst[where P=P'] simp: opt_map_def obj_at'_def)
+  done
+
 lemma getObject_tcb_wp:
   "\<lbrace>\<lambda>s. tcb_at' p s \<longrightarrow> (\<exists>t::tcb. ko_at' t p s \<and> Q t s)\<rbrace> getObject p \<lbrace>Q\<rbrace>"
   by (clarsimp simp: getObject_def valid_def in_monad

diff --git a/proof/refine/RISCV64/SchedContext_R.thy b/proof/refine/RISCV64/SchedContext_R.thy
@@ -584,6 +584,9 @@ crunch schedContextDonate
 global_interpretation schedContextDonate: typ_at_all_props' "schedContextDonate scPtr tcbPtr"
   by typ_at_props'
 
+global_interpretation updateSchedContext: typ_at_all_props' "updateSchedContext scPtr f"
+  by typ_at_props'
+
 crunch schedContextDonate
   for aligned'[wp]: "pspace_aligned'"
   and distinct'[wp]:"pspace_distinct'"
@@ -625,53 +628,36 @@ lemma tcbSchedContext_update_None_valid_objs'[wp]:
   apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def cteSizeBits_def)
   done
 
+lemma updateSchedContext_valid_objs'_stTCB_update_Just[wp]:
+  "\<lbrace>valid_objs' and sc_at' scPtr and tcb_at' tcbPtr\<rbrace>
+   updateSchedContext scPtr (scTCB_update (\<lambda>_. Just tcbPtr))
+   \<lbrace>\<lambda>_. valid_objs'\<rbrace>"
+  apply wpsimp
+  by (clarsimp simp: opt_pred_def opt_map_def valid_obj'_def
+                     valid_sched_context'_def valid_sched_context_size'_def
+                     objBits_def objBitsKO_def refillSize_def obj_at'_def
+              split: if_splits)
+
 lemma schedContextDonate_valid_objs':
   "\<lbrace>valid_objs' and tcb_at' tcbPtr
     and sym_heap_sched_pointers and valid_sched_pointers
     and pspace_aligned' and pspace_distinct' and pspace_bounded'\<rbrace>
    schedContextDonate scPtr tcbPtr
    \<lbrace>\<lambda>_. valid_objs'\<rbrace>"
   unfolding schedContextDonate_def
-  apply (wpsimp wp: hoare_vcg_all_lift hoare_drop_imps)
-  by (fastforce dest: sc_ko_at_valid_objs_valid_sc'
-                simp: valid_sched_context'_def valid_sched_context_size'_def
-                      sc_size_bounds_def objBits_def objBitsKO_def refillSize_def)
+  apply (wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_disj_lift)
+  by fastforce
 
 lemma schedContextDonate_list_refs_of_replies' [wp]:
   "schedContextDonate scPtr tcbPtr \<lbrace>\<lambda>s. P (list_refs_of_replies' s)\<rbrace>"
-  unfolding schedContextDonate_def
+  unfolding schedContextDonate_def updateSchedContext_def
   by (wpsimp simp: comp_def | rule hoare_strengthen_post[where Q'="\<lambda>_ s. P (list_refs_of_replies' s)"])+
 
-lemma schedContextDonate_valid_idle':
-  "\<lbrace>\<lambda>s. valid_idle' s \<and> tcbPtr \<noteq> idle_thread_ptr \<and>
-        obj_at' (\<lambda>sc. scTCB sc \<noteq> Some idle_thread_ptr) scPtr s\<rbrace>
-   schedContextDonate scPtr tcbPtr
-   \<lbrace>\<lambda>_. valid_idle'\<rbrace>"
-  apply (simp only: schedContextDonate_def)
-  apply (wp threadSet_idle' setSchedContext_valid_idle')
-       apply (rule_tac Q'="\<lambda>_ s. tcbPtr \<noteq> ksIdleThread s" in hoare_strengthen_post; wpsimp)
-      apply (rule_tac Q'="\<lambda>_ s. valid_idle' s \<and> scPtr \<noteq> idle_sc_ptr \<and> tcbPtr \<noteq> ksIdleThread s"
-                   in hoare_strengthen_post; wpsimp)
-         apply (wpsimp wp: threadSet_idle' hoare_drop_imps threadSet_idle')
-        apply (rule_tac Q'="\<lambda>_ s. valid_idle' s \<and> scPtr \<noteq> idle_sc_ptr \<and>
-                                 tcbPtr \<noteq> ksIdleThread s \<and> from \<noteq> ksIdleThread s"
-                     in hoare_strengthen_post)
-         apply wpsimp+
-  apply (auto simp: obj_at'_def valid_idle'_def)
-  done
-
 lemma schedContextDonate_bound_tcb_sc_at[wp]:
   "\<lbrace>\<top>\<rbrace> schedContextDonate scPtr tcbPtr \<lbrace>\<lambda>_. obj_at' (\<lambda>a. \<exists>y. scTCB a = Some y) scPtr\<rbrace>"
-   unfolding schedContextDonate_def
+   unfolding schedContextDonate_def updateSchedContext_def
    by (wpsimp wp: set_sc'.obj_at')
 
-lemma updateSchedContext_obj_at'[wp]:
-  "\<forall>sc'. objBits sc' = objBits (f' sc'::sched_context) \<Longrightarrow>
-   updateSchedContext scp f' \<lbrace>\<lambda>s. P (sc_at' p s)\<rbrace>"
-  apply (wpsimp simp: updateSchedContext_def wp: set_sc'.set_wp)
-  apply (clarsimp simp: obj_at'_def ps_clear_upd objBits_simps)
-  done
-
 (* corres rules for updateRefillHd / updateRefillTl *)
 
 (* using the abstract side size *)

diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy
@@ -106,9 +106,6 @@ global_interpretation refillNew: typ_at_all_props' "refillNew scPtr maxRefills b
 global_interpretation refillUpdate: typ_at_all_props' "refillUpdate  scPtr newPeriod newBudget newMaxRefills"
   by typ_at_props'
 
-global_interpretation updateSchedContext: typ_at_all_props' "updateSchedContext scPtr f"
-  by typ_at_props'
-
 context begin interpretation Arch . (*FIXME: arch_split*)
 
 lemma findM_awesome':
@@ -5255,7 +5252,7 @@ lemma schedContextDonate_if_live_then_nonz_cap':
         \<and> pspace_aligned' s \<and> pspace_distinct' s \<and>  pspace_bounded' s\<rbrace>
    schedContextDonate scPtr tcbPtr
    \<lbrace>\<lambda>_. if_live_then_nonz_cap'\<rbrace>"
-  unfolding schedContextDonate_def
+  unfolding schedContextDonate_def updateSchedContext_def
   by (wpsimp wp: threadSet_iflive'T setSchedContext_iflive' hoare_vcg_all_lift threadSet_cap_to'
            simp: conj_ac cong: conj_cong
       | wp hoare_drop_imps
@@ -5268,8 +5265,6 @@ crunch schedContextDonate
   (wp: crunch_wps threadSet_sched_pointers threadSet_valid_sched_pointers hoare_vcg_all_lift
    simp: crunch_simps)
 
-(* `obj_at' (\<lambda>x. scTCB x \<noteq> Some idle_thread_ptr) scPtr s` is
-   needed because sometimes sym_refs doesn't hold in its entirety here. *)
 lemma schedContextDonate_invs':
   "\<lbrace>\<lambda>s. invs' s \<and> bound_sc_tcb_at' ((=) None) tcbPtr s \<and>
         ex_nonz_cap_to' scPtr s \<and> ex_nonz_cap_to' tcbPtr s\<rbrace>
@@ -5369,7 +5364,7 @@ lemma schedContextDonate_corres:
                  apply (rule_tac r'=sched_act_relation in corres_split)
                     apply (rule getSchedulerAction_corres)
                    apply (rule corres_when)
-                    apply (case_tac rv; clarsimp simp: sched_act_relation_def sc_relation_def)
+                    apply (case_tac rv; fastforce simp: sched_act_relation_def sc_relation_def)
                    apply (rule rescheduleRequired_corres_weak)
                   apply wpsimp
                  apply wpsimp
@@ -5389,7 +5384,7 @@ lemma schedContextDonate_corres:
                             hoare_vcg_all_lift hoare_vcg_imp_lift')
          apply (wpsimp wp: hoare_vcg_all_lift)
         apply (rule corres_split
-                   [OF update_sc_no_reply_stack_update_ko_at'_corres
+                   [OF updateSchedContext_no_stack_update_corres
                          [where f'="scTCB_update (\<lambda>_. Some thread)"]])
               apply (clarsimp simp: sc_relation_def refillSize_def)
              apply clarsimp

diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy
@@ -2306,7 +2306,7 @@ lemma cteInsert_sane[wp]:
 
 crunch setExtraBadge, transferCaps, handleFaultReply, doIPCTransfer
   for sch_act_sane [wp]: sch_act_sane
-  (wp: crunch_wps simp: crunch_simps)
+  (wp: crunch_wps sch_act_sane_lift simp: crunch_simps)
 
 lemma handleHypervisorFault_corres:
   "corres dc (einvs and  st_tcb_at active thread and ex_nonz_cap_to thread

diff --git a/spec/haskell/src/SEL4/Object/SchedContext.lhs b/spec/haskell/src/SEL4/Object/SchedContext.lhs
@@ -664,10 +664,9 @@ This module uses the C preprocessor to select a target architecture.
 >         threadSet (\tcb -> tcb { tcbSchedContext = Nothing }) from
 >         cur <- getCurThread
 >         action <- getSchedulerAction
->         case action of
->             SwitchToThread candidate -> when (candidate == from || from == cur) rescheduleRequired
->             _ -> when (from == cur) rescheduleRequired
->     setSchedContext scPtr (sc { scTCB = Just tcbPtr })
+>         when (from == cur || action == SwitchToThread from)
+>             rescheduleRequired
+>     updateSchedContext scPtr (\sc -> sc { scTCB = Just tcbPtr })
 >     threadSet (\tcb -> tcb { tcbSchedContext = Just scPtr }) tcbPtr
 
 > invokeSchedControlConfigureFlags :: SchedControlInvocation -> Kernel ()