Small IPC lemmas

proof/crefine/RISCV64/Ipc_C.thy

@@ -6302,9 +6302,63 @@ lemma schedContext_bindTCB_ccorres:
 
 lemma schedContext_bindNtfn_ccorres:
   "ccorres dc xfdc
-     \<top> (\<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr tcbPtr\<rbrace> \<inter> \<lbrace>\<acute>sc = Ptr scPtr\<rbrace>) []
-     (schedContextBindNtfn scPtr tcbPtr) (Call schedContext_bindNtfn_'proc)"
-sorry (* FIXME RT: schedContext_bindNtfn_ccorres *)
+     (invs' and sc_at' scPtr) (\<lbrace>\<acute>ntfn = Ptr ntfnPtr\<rbrace> \<inter> \<lbrace>\<acute>sc = Ptr scPtr\<rbrace>) []
+     (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="\<lambda>s. invs' s \<and> sym_refs (state_refs_of' s)
+                          \<and> sc_at' scPtr s \<and> 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="\<top>"])
+       apply vcg
+      apply fastforce
+     apply (clarsimp simp: typ_heap_simps)
+     apply (rule_tac sc'="scNotification_C_update (\<lambda>_. 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]

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 (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_sc ntfn = None) ntfnp))
+      and (obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_sc ntfn = None) ntfnp)
+      and (\<lambda>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)

proof/refine/RISCV64/Syscall_R.thy

@@ -882,7 +882,7 @@ lemma schedContextBindNtfn_invs':
   "\<lbrace>invs' and ex_nonz_cap_to' scPtr and ex_nonz_cap_to' ntfnPtr\<rbrace>
    schedContextBindNtfn scPtr ntfnPtr
    \<lbrace>\<lambda>_. invs'\<rbrace>"
-  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)

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