update after rebase and some small fixups

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

proof/crefine/RISCV64/IsolatedThreadAction.thy

@@ -1489,7 +1489,7 @@ crunch getSchedulable
 lemma setThreadState_rewrite_simple:
   "monadic_rewrite True True
      (\<lambda>s. ((runnable' st
-            \<and> ((\<lambda>sc. 0 < scRefillMax sc) |< (tcbs_of' s |> tcbSchedContext |> scs_of' s)) (ksCurThread s)
+            \<and> active_sc_tcb_at' (ksCurThread s) 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)
@@ -1507,7 +1507,7 @@ lemma setThreadState_rewrite_simple:
           apply (wpsimp simp: getCurThread_def
                           wp: hoare_vcg_disj_lift hoare_vcg_imp_lift' threadSet_tcbState_st_tcb_at')+
    apply (rule monadic_rewrite_refl)
-  apply (fastforce simp: schedulable'_def obj_at_simps  opt_map_def opt_pred_def
+  apply (fastforce simp: schedulable'_def obj_at_simps opt_map_def opt_pred_def active_sc_tcb_at'_def
                   split: option.splits if_splits)
   done
 

proof/invariant-abstract/KHeap_AI.thy

@@ -2219,11 +2219,6 @@ lemma assert_get_tcb_ko':
                      obj_at_def
                split: option.splits Structures_A.kernel_object.splits)
 
-(* FIXME RT: move to Lib *)
-lemma gets_the_sp:
-  "\<lbrace>Q\<rbrace> gets_the f \<lbrace>\<lambda>rv s. f s = Some rv \<and> Q s\<rbrace>"
-  by wpsimp
-
 lemma update_sched_context_obj_at_impossible:
   "\<lbrakk> \<And>np n. \<not> (P (SchedContext np n)) \<rbrakk> \<Longrightarrow>
        \<lbrace>\<lambda>s. Q (obj_at P p s)\<rbrace>

proof/refine/RISCV64/TcbAcc_R.thy

@@ -2234,7 +2234,7 @@ lemmas isRunnable_sp' =
   gets_the_sp[where f="readRunnable tcb_ptr" for tcb_ptr, simplified isRunnable_def[symmetric]]
 
 lemma isRunnable_sp:
-  "\<lbrace>Q\<rbrace> isRunnable t \<lbrace>\<lambda>rv s. (st_tcb_at' runnable' t s = rv) \<and> Q s\<rbrace>"
+  "\<lbrace>Q\<rbrace> isRunnable t \<lbrace>\<lambda>rv s. st_tcb_at' runnable' t s = rv \<and> Q s\<rbrace>"
   by wpsimp
 
 lemma no_ofail_readRunnable[wp]:
@@ -3046,13 +3046,6 @@ defs valid_tcbs'_asrt_def:
 
 declare valid_tcbs'_asrt_def[simp]
 
-(* FIXME RT: move to Lib *)
-lemma corres_gets_return_trivial:
-  "(\<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> f s = v)
-   \<Longrightarrow> corres_underlying sr nf nf' (=) P P' (gets f) (return v)"
-  unfolding corres_underlying_def gets_def get_def return_def bind_def
-  by clarsimp
-
 definition schedulable' :: "machine_word \<Rightarrow> kernel_state \<Rightarrow> bool" where
   "schedulable' tcbPtr s' \<equiv>
    (runnable' |< (tcbs_of' s' ||> tcbState)) tcbPtr
@@ -3080,15 +3073,6 @@ lemma isSchedulable_inv[wp]:
   "getSchedulable tcbPtr \<lbrace>P\<rbrace>"
   by (wpsimp wp: getSchedulable_wp)
 
-(* FIXME RT: move *)
-lemma ovalid_if_lift2:
-  "\<lblot>P\<rblot> f \<lblot>\<lambda>rv s. (Q rv s \<longrightarrow> X rv s) \<and> (\<not> Q rv s \<longrightarrow> Y rv s)\<rblot> \<Longrightarrow>
-   \<lblot>P\<rblot> f \<lblot>\<lambda>rv s. if Q rv s then X rv s else Y rv s\<rblot>"
-
-  "\<lblot>P\<rblot> f \<lblot>\<lambda>rv s. (Q' rv \<longrightarrow> X rv s) \<and> (\<not> Q' rv \<longrightarrow> Y rv s)\<rblot> \<Longrightarrow>
-   \<lblot>P\<rblot> f \<lblot>\<lambda>rv. if Q' rv then X rv else Y rv\<rblot>"
-  by (auto simp: ovalid_def split_def)
-
 lemma no_ofail_readSchedulable[wp]:
   "no_ofail (tcb_at' tcbPtr and valid_tcbs') (readSchedulable tcbPtr)"
   apply (clarsimp simp: readSchedulable_def readSchedContext_def ohaskell_state_assert_def)
@@ -3220,16 +3204,9 @@ lemma rescheduleRequired_corres_weak:
   apply (rule corres_symb_exec_l[OF _ thread_get_exs_valid thread_get_sp , rotated])
     apply (clarsimp simp: weaker_valid_sched_action_def vs_all_heap_simps obj_at_def is_tcb_def)
    apply (wpsimp simp: thread_get_def get_tcb_def weaker_valid_sched_action_def vs_all_heap_simps)
-  (* FIXME Michael: use new corres rule for assert_opt on the rhs *)
-  apply (rule corres_symb_exec_l[OF _ _ assert_opt_sp, rotated])
-    apply wpsimp
-    apply (clarsimp simp: obj_at_def schedulable_def opt_pred_def
-                          opt_map_def tcbs_of_kh_def
+  apply (rule corres_assert_opt_assume_lhs[rotated])
+    apply (clarsimp simp: obj_at_def schedulable_def opt_pred_def opt_map_def tcbs_of_kh_def
                    split: option.splits)
-   apply wpsimp
-   apply (clarsimp simp: obj_at_def schedulable_def opt_pred_def
-                         opt_map_def tcbs_of_kh_def
-                  split: option.splits)
 
   apply (rule corres_symb_exec_l[OF _ _ get_sc_refill_sufficient_sp, rotated])
     apply (rule get_sc_refill_sufficient_exs_valid)
@@ -3250,7 +3227,7 @@ lemma rescheduleRequired_corres_weak:
     apply (fastforce intro: valid_refills_nonempty_refills active_scs_validE
                       simp: obj_at_def vs_all_heap_simps schedulable_def2)
 
- apply (rule stronger_corres_guard_imp)
+  apply (rule stronger_corres_guard_imp)
     apply (rule corres_assert_assume_l)
     apply (rule tcbSchedEnqueue_corres)
     apply simp