rt spec+proof: consolidate ASpec and Haskell versions of isSchedulable

This rephrases the ASpec predicate schedulable in terms of projections,
removing the monadic function is_schedulable and the auxiliary function
is_schedulable_opt.

The Haskell function isSchedulable was replaced with a reader monad
function readSchedulable and its nondet state monad counterpart
getSchedulable. A new Refine level predicate schedulable' is stated
in terms of projections, replacing isSchedulable_bool.

The preconditions of some top-level Hoare triples were simplified.

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

proof/crefine/Move_C.thy

@@ -936,7 +936,7 @@ lemma sts_running_ksReadyQueuesL1Bitmap[wp]:
   unfolding setThreadState_def scheduleTCB_def rescheduleRequired_def
   apply wpsimp
          apply (rule hoare_pre_cont)
-        by (wpsimp wp: hoare_drop_imps isSchedulable_wp)+
+        by (wpsimp wp: hoare_drop_imps getSchedulable_wp)+
 
 lemma asUser_obj_at_not_queued[wp]:
   "\<lbrace>obj_at' (\<lambda>tcb. \<not> tcbQueued tcb) p\<rbrace> asUser t m \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. \<not> tcbQueued tcb) p\<rbrace>"

proof/crefine/RISCV64/Finalise_C.thy

@@ -1304,7 +1304,8 @@ lemma threadSet_tcbInReleaseQueue_ccorres[corres]:
 lemma tcbReleaseRemove_ccorres:
   "ccorres dc xfdc valid_objs' \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr tcbPtr\<rbrace> []
      (tcbReleaseRemove tcbPtr) (Call tcbReleaseRemove_'proc)"
-  apply (cinit lift: tcb_' simp: inReleaseQueue_def when_def)
+  apply (cinit lift: tcb_'
+               simp: inReleaseQueue_def when_def readInReleaseQueue_def threadGet_def[symmetric])
    apply (rule ccorres_stateAssert)+
    apply (rule_tac r'="\<lambda>rv rv'. rv = to_bool rv'" and xf'="ret__unsigned_longlong_'"
                 in ccorres_split_nothrow)
@@ -1461,15 +1462,6 @@ lemma schedContext_cancelYieldTo_ccorres:
   apply (fastforce dest: typ_heap_simps' split: if_splits)
   done
 
-lemma threadSet_isSchedulable_bool:
-  "\<lbrakk>\<forall>tcb. tcbState tcb = tcbState (f tcb); \<forall>tcb. tcbInReleaseQueue tcb = tcbInReleaseQueue (f tcb);
-    \<forall>tcb. tcbSchedContext tcb = tcbSchedContext (f tcb)\<rbrakk>
-   \<Longrightarrow> threadSet f t \<lbrace>\<lambda>s. P (isSchedulable_bool t s)\<rbrace>"
-  apply (wpsimp wp: threadSet_wp)
-  apply (erule_tac P=P in back_subst)
-  by (fastforce simp: pred_map_simps isSchedulable_bool_def isScActive_def opt_map_def obj_at_simps
-               split: if_splits option.splits)
-
 lemma active_runnable':
   "active' state \<Longrightarrow> runnable' state"
   by fastforce

proof/crefine/RISCV64/Invoke_C.thy

@@ -81,17 +81,17 @@ lemma setDomain_ccorres:
      apply (rule_tac Q'="\<lambda>rv'. invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)
                               and tcb_at' t and (\<lambda>s. curThread = ksCurThread s)"
                   in hoare_strengthen_post)
-       apply (wpsimp wp: isSchedulable_wp)
+       apply (wpsimp wp: getSchedulable_wp)
       apply (fastforce simp: valid_pspace_valid_objs' weak_sch_act_wf_def
                       split: if_splits)
      apply (rule_tac Q'="\<lambda>_. invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)
                             and tcb_at' t and (\<lambda>s. curThread = ksCurThread s)"
                   in hoare_strengthen_post)
       apply (wpsimp wp: threadSet_tcbDomain_update_invs' hoare_vcg_imp_lift'
-                        threadSet_isSchedulable_bool)+
+                        threadSet_schedulable')+
     apply (simp add: guard_is_UNIV_def)
    apply (wpsimp wp: tcbSchedDequeue_not_queued hoare_vcg_all_lift hoare_vcg_imp_lift')
-  apply (fastforce simp: isSchedulable_bool_def pred_map_simps opt_map_def obj_at_simps)
+  apply fastforce
   done
 
 lemma decodeDomainInvocation_ccorres:

proof/crefine/RISCV64/IpcCancel_C.thy

@@ -420,29 +420,25 @@ lemma isStopped_ccorres [corres]:
     apply (simp add: ThreadState_defs)+
   done
 
-lemma isRunnable_ccorres [corres]:
+lemma isRunnable_ccorres[corres]:
   "ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_'
-  (tcb_at' thread) (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread})  []
-  (isRunnable thread) (Call isRunnable_'proc)"
-  apply (cinit lift: thread_' simp: getThreadState_def)
+    (tcb_at' thread) {s. thread_' s = tcb_ptr_to_ctcb_ptr thread} hs
+    (isRunnable thread) (Call isRunnable_'proc)"
+  apply (cinit lift: thread_' simp: readRunnable_def threadGet_def[symmetric] getThreadState_def)
    apply (rule ccorres_move_c_guard_tcb)
    apply (rule ccorres_pre_threadGet)
    apply (rule ccorres_symb_exec_r)
      apply (rule ccorres_cond_weak)
+      apply (fastforce intro: ccorres_return_C)
      apply (rule ccorres_return_C)
-        apply (simp)
-       apply (simp)
-      apply (simp)
-     apply (simp add: ccorres_cond_iffs)
-     apply (rule ccorres_return_C)
-       apply (simp)
-      apply (simp)
-     apply (simp)
-    apply (vcg)
+       apply simp
+      apply simp
+     apply simp
+    apply vcg
    apply (rule conseqPre)
-    apply (vcg)
-   apply (clarsimp)
-  apply (clarsimp)
+    apply vcg
+   apply clarsimp
+  apply clarsimp
   apply (clarsimp simp: typ_heap_simps ctcb_relation_thread_state_to_tsType
                  split: thread_state.splits)
        apply (simp add: ThreadState_defs)+
@@ -1777,25 +1773,29 @@ lemma tcb_at_1:
   apply (clarsimp simp add: is_aligned_def ctcb_size_bits_def)
   done
 
-crunch inReleaseQueue, isSchedulable
+crunch inReleaseQueue, getSchedulable
  for (empty_fail) empty_fail[wp]
 
 lemma isSchedulable_ccorres [corres]:
   "ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_'
      (tcb_at' tcbPtr and no_0_obj') \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr tcbPtr\<rbrace> []
-     (isSchedulable tcbPtr) (Call isSchedulable_'proc)"
+     (getSchedulable tcbPtr) (Call isSchedulable_'proc)"
   supply Collect_const[simp del]
          if_split[split del]
-  apply (cinit lift: thread_')
+  apply (cinit lift: thread_'
+               simp: readSchedulable_def isRunnable_def[symmetric] threadGet_def[symmetric]
+                     gets_the_if_distrib ohaskell_state_assert_def gets_the_ostate_assert)
+   apply (subst gets_the_obind scActive_def[symmetric] inReleaseQueue_def[symmetric]
+                fun_app_def Nondet_Reader_Option.gets_the_return)+
    apply (ctac add: isRunnable_ccorres)
      apply (rename_tac runnable)
      apply csymbr
-     apply (rule ccorres_pre_threadGet)
+     apply (rule ccorres_pre_threadGet, rename_tac scPtrOpt)
      apply clarsimp
      apply (rule_tac P="to_bool runnable" in ccorres_cases; clarsimp simp: to_bool_def)
       apply ccorres_rewrite
       apply (rule ccorres_move_c_guard_tcb)
-      apply (rule ccorres_stateAssert)
+      apply (rule ccorres_stateAssert[simplified HaskellLib_H.stateAssert_def])
       apply (rule_tac xf'=ret__int_'
                   and val="from_bool (scPtrOpt \<noteq> None)"
                   and R="\<lambda>s. obj_at' (\<lambda>tcb. tcbSchedContext tcb = scPtrOpt) tcbPtr s
@@ -1832,7 +1832,7 @@ lemma isSchedulable_ccorres [corres]:
           apply (rule ccorres_cond_true)
           apply (rule ccorres_rhs_assoc)
           apply (rule ccorres_move_c_guard_tcb)
-          apply (clarsimp simp: inReleaseQueue_def)
+          apply (clarsimp simp: inReleaseQueue_def readInReleaseQueue_def simp flip: threadGet_def)
           apply (rule_tac r'="\<lambda>rv rv'. rv = to_bool rv'" and xf'="ret__unsigned_longlong_'"
                        in ccorres_split_nothrow)
               apply (rule threadGet_vcg_corres)
@@ -1860,7 +1860,7 @@ lemma isSchedulable_ccorres [corres]:
      apply (rule ccorres_cond_seq)
      apply (rule ccorres_cond_false)
      apply ccorres_rewrite
-     apply (rule ccorres_stateAssert)
+     apply (rule ccorres_stateAssert[simplified HaskellLib_H.stateAssert_def])
      apply (rule ccorres_if_lhs)
       apply (fastforce intro: ccorres_return_C)
      apply clarsimp
@@ -1913,7 +1913,7 @@ lemma rescheduleRequired_ccorres:
              apply (clarsimp simp: to_bool_def split: if_split)
             apply (ctac add: tcbSchedEnqueue_ccorres)
            apply (rule ccorres_return_Skip)
-          apply (wpsimp wp: isSchedulable_wp)
+          apply (wpsimp wp: getSchedulable_wp)
          apply (vcg exspec=isSchedulable_modifies)
         apply (clarsimp simp: to_bool_def)
         apply (rule ccorres_cond_false)
@@ -2239,7 +2239,7 @@ lemma possibleSwitchTo_ccorres:
                 and xf'=ret__int_'
                 and P'="\<lbrace>\<acute>ret__int = from_bool (\<exists>scPtr. scOpt = Some scPtr)\<rbrace>"
                  in ccorres_split_nothrow)
-        apply (clarsimp simp: inReleaseQueue_def)
+        apply (clarsimp simp: inReleaseQueue_def readInReleaseQueue_def simp flip: threadGet_def)
         apply (rule threadGet_vcg_corres_P_P')
         apply (rule allI, rule conseqPre, vcg)
         apply clarsimp
@@ -2327,7 +2327,7 @@ lemma scheduleTCB_ccorres:
           apply (fastforce simp: to_bool_def)
          apply (ctac (no_vcg) add: rescheduleRequired_ccorres)
         apply (rule ccorres_return_Skip)
-       apply (wpsimp wp: isSchedulable_wp)
+       apply (wpsimp wp: getSchedulable_wp)
       apply ccorres_rewrite
       apply (rule ccorres_cond_false)
       apply (rule ccorres_symb_exec_l')
@@ -2423,7 +2423,7 @@ lemma scheduleTCB_ccorres_simple:
           apply (fastforce simp: to_bool_def)
          apply (ctac (no_vcg) add: rescheduleRequired_ccorres_simple)
         apply (rule ccorres_return_Skip)
-       apply (wpsimp wp: isSchedulable_wp)
+       apply (wpsimp wp: getSchedulable_wp)
       apply ccorres_rewrite
       apply (rule ccorres_cond_false)
       apply (rule ccorres_symb_exec_l')

proof/crefine/RISCV64/IsolatedThreadAction.thy

@@ -854,7 +854,8 @@ lemma oblivious_switchToThread_schact:
                    getCurThread_def setCurThread_def liftM_def
                    threadSet_def tcbSchedEnqueue_def unless_when asUser_def
                    getQueue_def setQueue_def storeWordUser_def setRegister_def
-                   pointerInUserData_def isRunnable_def isStopped_def threadGet_getObject
+                   pointerInUserData_def isRunnable_def readRunnable_def threadGet_def[symmetric]
+                   isStopped_def threadGet_getObject
                    getThreadState_def tcbSchedDequeue_def bitmap_fun_defs ready_qs_runnable_def
                    ready_or_release'_asrt_def ksReadyQueues_asrt_def)
   by (safe intro!: oblivious_bind oblivious_tcbQueueRemove
@@ -1482,13 +1483,14 @@ lemma lookupIPCBuffer_isolatable:
       apply (simp add: assert_isolatable thread_actions_isolatable_return | wp)+
   done
 
-crunch isSchedulable
+crunch getSchedulable
   for (empty_fail) empty_fail[wp]
 
 lemma setThreadState_rewrite_simple:
   "monadic_rewrite True True
-     (\<lambda>s. ((runnable' st \<and> pred_map (\<lambda>tcb. \<not> tcbInReleaseQueue tcb) (tcbs_of' s) (ksCurThread s)
-            \<and> pred_map (\<lambda>scPtr. isScActive scPtr s) (tcbSCs_of s) (ksCurThread s))
+     (\<lambda>s. ((runnable' st
+            \<and> ((\<lambda>sc. 0 < scRefillMax sc) |< (tcbs_of' s |> tcbSchedContext |> scs_of' s)) (ksCurThread s)
+            \<and> (Not \<circ> tcbInReleaseQueue |< tcbs_of' s) (ksCurThread s))
            \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> t \<noteq> ksCurThread s)
           \<and> tcb_at' t s)
      (setThreadState st t)
@@ -1497,18 +1499,17 @@ lemma setThreadState_rewrite_simple:
   apply (simp add: setThreadState_def scheduleTCB_def when_def)
   apply (monadic_rewrite_l monadic_rewrite_if_l_False
            \<open>wpsimp wp: hoare_vcg_disj_lift hoare_vcg_imp_lift' threadSet_tcbState_st_tcb_at'
-                       isSchedulable_wp threadSet_wp\<close>)
+                       getSchedulable_wp threadSet_wp\<close>)
    (* take the threadSet, drop everything until return () *)
    apply (rule monadic_rewrite_trans[OF monadic_rewrite_bind_tail])
      apply (rule monadic_rewrite_symb_exec_l_drop)+
            apply (rule monadic_rewrite_refl)
           apply (wpsimp simp: getCurThread_def
-                        wp: hoare_vcg_disj_lift hoare_vcg_imp_lift' threadSet_tcbState_st_tcb_at')+
+                          wp: hoare_vcg_disj_lift hoare_vcg_imp_lift' threadSet_tcbState_st_tcb_at')+
    apply (rule monadic_rewrite_refl)
-  apply (clarsimp simp: isSchedulable_bool_def pred_map_simps obj_at_simps vs_all_heap_simps
-                        opt_map_def isScActive_def
-                 split: option.splits if_splits)
-  by (metis Structures_H.kernel_object.distinct(75) map_upd_eqD1)
+  apply (fastforce simp: schedulable'_def obj_at_simps  opt_map_def opt_pred_def
+                  split: option.splits if_splits)
+  done
 
 end
 

proof/crefine/RISCV64/Refine_C.thy

@@ -1048,36 +1048,22 @@ lemma refinement2_both:
            simp add: sch_act_simple_def)
      apply (clarsimp simp: ex_abs_def full_invs_def)
      apply (intro conjI)
-             apply (frule_tac s=abstract_state in invs_sym_refs)
-             apply (frule_tac s'=haskell_state in state_refs_of_cross_eq)
-               apply fastforce
-              apply fastforce
-             apply force
-            apply clarsimp
-            apply (erule (1) ct_running_cross)
-             apply fastforce
-            apply fastforce
-           apply (rule ct_running_or_idle_cross; simp?; fastforce)
-          apply (prop_tac "cur_sc abstract_state = ksCurSc haskell_state",
-                 fastforce dest!: state_relationD)
-          apply (prop_tac "sc_at (cur_sc abstract_state) abstract_state")
-           apply (rule cur_sc_tcb_sc_at_cur_sc[OF invs_valid_objs invs_cur_sc_tcb]; simp)
-          apply (prop_tac "sc_at' (ksCurSc haskell_state) haskell_state")
-           apply (rule sc_at_cross[OF state_relation_pspace_relation invs_psp_aligned invs_distinct]; simp)
-          apply (prop_tac "is_active_sc' (ksCurSc haskell_state) haskell_state")
-           apply (rule is_active_sc'2_cross[OF _ invs_psp_aligned invs_distinct], simp+)
-         apply (clarsimp simp: invs'_def valid_pspace'_def)
-         apply (rule sym_refs_tcbSCs; simp?)
-         apply (clarsimp simp: invs_def valid_state_def valid_pspace_def state_refs_of_cross_eq)
-        apply (fastforce dest!: cur_sc_tcb_cross[simplified schact_is_rct_def]
-                          simp: invs_def valid_state_def valid_pspace_def)
-       apply (prop_tac "cur_tcb' haskell_state")
-        apply (rule cur_tcb_cross[OF invs_cur invs_psp_aligned invs_distinct]; simp?)
-       apply (frule_tac s=abstract_state and s'=haskell_state in ct_not_in_release_q_cross)
+         apply (frule_tac s=abstract_state in invs_sym_refs)
+         apply (frule_tac s'=haskell_state in state_refs_of_cross_eq)
+           apply fastforce
           apply fastforce
-         apply (clarsimp simp: cur_tcb'_def dest!: state_relationD)
-        apply fastforce
-       apply fastforce
+         apply clarsimp
+         apply (erule (1) ct_running_cross)
+          apply fastforce
+         apply fastforce
+        apply (rule ct_running_or_idle_cross; simp?; fastforce)
+       apply (frule curthread_relation)
+       apply clarsimp
+       apply (erule schedulable_schedulable'_eq[THEN iffD1], fastforce+)
+       apply (clarsimp simp: schedulable_def2)
+       apply (rule conjI)
+        apply (clarsimp simp: ct_in_state_def pred_tcb_at_def obj_at_def)
+       apply (force elim!: schact_is_rct_ct_active_sc)
       apply (frule_tac a=abstract_state in resume_cur_thread_cross; fastforce)
      apply (clarsimp simp: state_relation_def)
     apply (fastforce simp: ct_running'_C)

proof/crefine/RISCV64/Schedule_C.thy

@@ -105,7 +105,7 @@ lemma threadGet_exs_valid[wp]:
 
 lemma isRunnable_exs_valid[wp]:
   "tcb_at' t s \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable t \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>"
-  unfolding isRunnable_def getThreadState_def
+  apply (clarsimp simp: isRunnable_def readRunnable_def simp flip: threadGet_def)
   by (wpsimp wp: exs_getObject)
 
 (* FIXME: move *)
@@ -313,7 +313,7 @@ proof -
           apply assumption
          apply (rule conseqPre, vcg)
          apply clarsimp
-        apply (wpsimp wp: isSchedulable_wp)+
+        apply (wpsimp wp: getSchedulable_wp)+
        apply (clarsimp simp: Let_def guard_is_UNIV_def ctcb_queue_relation_def
                              option_to_ctcb_ptr_def cready_queues_index_to_C_def numPriorities_def
                              le_maxDomain_eq_less_numDomains unat_trans_ucast_helper queue_in_range

proof/crefine/RISCV64/Tcb_C.thy

@@ -1210,7 +1210,7 @@ crunch schedContextResume
 
 crunch schedContextResume
   for tcbDomain[wp]: "obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t"
-  (wp: isSchedulable_wp simp: crunch_simps)
+  (wp: getSchedulable_wp simp: crunch_simps)
 
 lemma schedContextResume_sch_act_wf[wp]:
   "schedContextResume scPtr \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"