Small IPC lemmas

proof/crefine/RISCV64/Finalise_C.thy

@@ -238,12 +238,17 @@ lemma isRoundRobin_ccorres:
 
 lemma refill_ready_ccorres:
   "ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_'
-     (active_sc_at' scPtr and valid_objs') \<lbrace>\<acute>sc = Ptr scPtr\<rbrace> []
+     valid_objs' \<lbrace>\<acute>sc = Ptr scPtr\<rbrace> []
      (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'="\<lambda>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 (\<lambda>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))
      (\<lbrace>\<acute>sc = Ptr scPtr\<rbrace> \<inter> \<lbrace>\<acute>index = word_of_nat idx\<rbrace>) []
      (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') \<lbrace>\<acute>sc = Ptr scPtr\<rbrace> []
+     (valid_objs' and no_0_obj') \<lbrace>\<acute>sc = Ptr scPtr\<rbrace> []
      (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'="\<lambda>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]

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')
-     (\<lbrace>\<acute>sc = Ptr scPtr\<rbrace> \<inter> {s'. crefill_relation new (refill_' s')}) []
+     invs'
+     (\<lbrace>\<acute>sc = Ptr scPtr\<rbrace> \<inter> {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)

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
 

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 \<leftarrow> 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 (\<lambda>s. h_val (hrs_mem (t_hrs_' (globals s))) (ret__ptr_to_struct_refill_C_' s))
-     (active_sc_at' scPtr and valid_objs') (\<lbrace>\<acute>sc = Ptr scPtr\<rbrace>) []
+     valid_objs' (\<lbrace>\<acute>sc = Ptr scPtr\<rbrace>) []
      (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 \<leftarrow> 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 (\<lambda>s. h_val (hrs_mem (t_hrs_' (globals s))) (ret__ptr_to_struct_refill_C_' s))
-     (active_sc_at' scPtr and valid_objs') (\<lbrace>\<acute>sc = Ptr scPtr\<rbrace>) []
+     valid_objs' (\<lbrace>\<acute>sc = Ptr scPtr\<rbrace>) []
      (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') (\<lbrace>\<acute>sc = Ptr scPtr\<rbrace> \<inter> \<lbrace>\<acute>usage = usage\<rbrace>) []
+     (valid_objs' and no_0_obj') (\<lbrace>\<acute>sc = Ptr scPtr\<rbrace> \<inter> \<lbrace>\<acute>usage = usage\<rbrace>) []
      (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'="\<lambda>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'="\<lambda>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=\<top>
+                   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'="\<lbrace>h_val (hrs_mem \<acute>t_hrs) \<acute>ret__ptr_to_struct_refill_C = refill'\<rbrace>"
+                     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'="\<lbrace>h_val (hrs_mem \<acute>t_hrs) \<acute>ret__ptr_to_struct_refill_C = refill'\<rbrace>"
-                   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 (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_'
-     (active_sc_at' scPtr and valid_objs' and no_0_obj') (\<lbrace>\<acute>sc = Ptr scPtr\<rbrace> \<inter> \<lbrace>\<acute>usage = usage\<rbrace>) []
+     (valid_objs' and no_0_obj') (\<lbrace>\<acute>sc = Ptr scPtr\<rbrace> \<inter> \<lbrace>\<acute>usage = usage\<rbrace>) []
      (getRefillSufficient scPtr usage) (Call refill_sufficient_'proc)"
   apply (cinit simp: readRefillSufficient_def getRefillCapacity_def[symmetric])
    apply (ctac add: refill_capacity_ccorres)