rt riscv refine: add release_q_runnable_asrt to deleteObjects

Signed-off-by: Michael McInerney <[email protected]>

proof/refine/RISCV64/Detype_R.thy

@@ -109,13 +109,17 @@ defs cNodePartialOverlap_def:
       \<or> (\<not> mask_range p (cte_level_bits + n) \<subseteq> {p. inRange p}
         \<and> \<not> mask_range p (cte_level_bits + n) \<subseteq> {p. \<not> inRange p}))"
 
+defs release_q_runnable_asrt_def:
+  "release_q_runnable_asrt \<equiv>
+     \<lambda>s. \<forall>p. p \<in> set (ksReleaseQueue s) \<longrightarrow> obj_at' (runnable' \<circ> tcbState) p s"
 
 (* FIXME: move *)
 lemma deleteObjects_def2:
   "is_aligned ptr bits \<Longrightarrow>
    deleteObjects ptr bits = do
      stateAssert sym_refs_asrt [];
      stateAssert valid_idle'_asrt [];
+     stateAssert release_q_runnable_asrt [];
      stateAssert (deletionIsSafe ptr bits) [];
      doMachineOp (freeMemory ptr bits);
      stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> mask_range ptr bits)) [];
@@ -149,6 +153,7 @@ lemma deleteObjects_def3:
    do
      stateAssert sym_refs_asrt [];
      stateAssert valid_idle'_asrt [];
+     stateAssert release_q_runnable_asrt [];
      assert (is_aligned ptr bits);
      stateAssert (deletionIsSafe ptr bits) [];
      doMachineOp (freeMemory ptr bits);
@@ -843,19 +848,16 @@ lemma deleteObjects_corres:
            \<and> s' \<turnstile>' (UntypedCap d base magnitude idx))
       (delete_objects base magnitude) (deleteObjects base magnitude)"
     (is "_ \<Longrightarrow> _ \<Longrightarrow> corres _ _ ?conc_guard _ _")
-  apply (rule corres_cross_over_guard
-                 [where Q="?conc_guard
-                           and (\<lambda>s'. \<forall>p. p \<in> set (ksReleaseQueue s')
-                                         \<longrightarrow> obj_at' (runnable' \<circ> tcbState) p s')"])
-   apply (simp add: pred_conj_def)
-   apply (erule ksReleaseQueue_runnable_thread_state; fastforce?)
   apply add_sym_refs
   apply add_valid_idle'
+  apply add_release_q_runnable
   apply (simp add: deleteObjects_def2)
   apply (rule corres_stateAssert_add_assertion[rotated])
    apply (clarsimp simp: sym_refs_asrt_def)
   apply (rule corres_stateAssert_add_assertion[rotated])
    apply (clarsimp simp: valid_idle'_asrt_def)
+  apply (rule corres_stateAssert_add_assertion[rotated])
+   apply (clarsimp simp: release_q_runnable_asrt_def)
   apply (rule corres_stateAssert_add_assertion)
    prefer 2
    apply clarsimp

proof/refine/RISCV64/KHeap_R.thy

@@ -5005,6 +5005,18 @@ lemma is_active_sc'2_cross:
                         active_sc_def opt_map_red StateRelation.is_active_sc'_def)
   done
 
+lemma release_q_runnable_cross:
+  "\<lbrakk>(s,s') \<in> state_relation; valid_release_q s; pspace_aligned s; pspace_distinct s\<rbrakk> \<Longrightarrow>
+   \<forall>p. p \<in> set (ksReleaseQueue s') \<longrightarrow> obj_at' (runnable' \<circ> tcbState) p s'"
+  apply (frule state_relation_release_queue_relation)
+  apply (clarsimp simp: valid_release_q_def obj_at'_def release_queue_relation_def)
+  apply (drule_tac x=p in bspec, blast)
+  apply (clarsimp simp: vs_all_heap_simps)
+  apply (frule_tac t=p in st_tcb_at_coerce_concrete[rotated, where P=runnable], simp, simp)
+   apply (clarsimp simp: pred_tcb_at_def obj_at_def)
+  apply (clarsimp simp: pred_tcb_at'_def obj_at'_def sts_rel_runnable)
+  done
+
 \<comment> \<open>Some methods to add invariants to the concrete guard of a corres proof. Often used for properties
     that are asserted to hold in the Haskell definition.\<close>
 
@@ -5037,6 +5049,13 @@ method add_ready_qs_runnable =
   (frule valid_sched_valid_ready_qs)?, (frule invs_psp_aligned)?, (frule invs_distinct)?,
   fastforce dest: ready_qs_runnable_cross
 
+method add_release_q_runnable =
+  rule_tac Q="\<lambda>s'. \<forall>p. p \<in> set (ksReleaseQueue s') \<longrightarrow> obj_at' (runnable' \<circ> tcbState) p s'"
+        in corres_cross_add_guard,
+  (simp only: pred_conj_def)?,
+  (frule valid_sched_valid_release_q)?, (frule invs_psp_aligned)?, (frule invs_distinct)?,
+  fastforce dest: release_q_runnable_cross
+
 method add_valid_replies for rptr uses simp =
   rule_tac Q="\<lambda>s. valid_replies'_sc_asrt rptr s" in corres_cross_add_guard,
   fastforce elim: valid_replies_sc_cross simp: simp

proof/refine/RISCV64/TcbAcc_R.thy

@@ -4565,18 +4565,6 @@ lemma tcbReleaseRemove_pred_tcb_at'[wp]:
 crunches tcbReleaseRemove
   for weak_sch_act_wf[wp]: "\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s"
 
-lemma ksReleaseQueue_runnable_thread_state:
-  "\<lbrakk>(s,s') \<in> state_relation; valid_release_q s; pspace_aligned s; pspace_distinct s\<rbrakk>
-   \<Longrightarrow>  \<forall>p. p \<in> set (ksReleaseQueue s') \<longrightarrow> obj_at' (runnable' \<circ> tcbState) p s'"
-  apply (frule state_relation_release_queue_relation)
-  apply (clarsimp simp: valid_release_q_def obj_at'_def release_queue_relation_def)
-  apply (drule_tac x=p in bspec, blast)
-  apply (clarsimp simp: vs_all_heap_simps)
-  apply (frule_tac t=p in st_tcb_at_coerce_concrete[rotated, where P=runnable], simp, simp)
-   apply (clarsimp simp: pred_tcb_at_def obj_at_def)
-  apply (clarsimp simp: pred_tcb_at'_def obj_at'_def sts_rel_runnable)
-  done
-
 lemma sts_st_tcb':
   "\<lbrace>if t = t' then K (P st) else st_tcb_at' P t\<rbrace>
   setThreadState st t'