rt arm refine: add release_q_runnable_asrt to deleteObjects

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

proof/refine/ARM/Detype_R.thy

@@ -106,12 +106,17 @@ defs cNodePartialOverlap_def:
       \<or> (\<not> {p .. p + 2 ^ (cte_level_bits + n) - 1} \<subseteq> {p. inRange p}
         \<and> \<not> {p .. p + 2 ^ (cte_level_bits + n) - 1} \<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> {ptr .. ptr + 2 ^ bits - 1})) [];
@@ -145,6 +150,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);
@@ -887,19 +893,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/ARM/KHeap_R.thy

@@ -5089,6 +5089,19 @@ 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>
 
@@ -5121,6 +5134,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/ARM/PageTableDuplicates.thy

@@ -1323,19 +1323,16 @@ lemma valid_duplicates_deleteObjects_helper:
   done
 
 lemma deleteObjects_valid_duplicates'[wp]:
-  notes [simp del] =  atLeastAtMost_simps
+  notes [simp del] = atLeastAtMost_simps
   shows
-  "\<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
-      K (is_aligned ptr sz)
-   \<rbrace> deleteObjects ptr sz
-   \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
+  "\<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and K (is_aligned ptr sz)\<rbrace>
+   deleteObjects ptr sz
+   \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
   apply (rule hoare_gen_asm)
   apply (clarsimp simp: deleteObjects_def2)
-  apply (rule hoare_seq_ext_skip, wpsimp)
-  apply (rule hoare_seq_ext_skip, wpsimp)
-  apply (wp hoare_drop_imps|simp)+
-  apply clarsimp
-  apply (simp add:deletionIsSafe_def)
+  apply (intro hoare_seq_ext[OF _ stateAssert_sp])
+  apply (wpsimp wp: hoare_drop_imps)
+  apply (clarsimp simp: deletionIsSafe_def)
   apply (erule valid_duplicates_deleteObjects_helper)
    apply fastforce
   apply simp

proof/refine/ARM/TcbAcc_R.thy

@@ -4561,18 +4561,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'