address PR comments

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

proof/crefine/AARCH64/ADT_C.thy

@@ -671,7 +671,7 @@ lemma cready_queues_to_H_correct:
   apply (rename_tac d p)
   apply (drule_tac x=d in spec)
   apply (drule_tac x=p in spec)
-  apply (clarsimp simp: ksReadyQueues_asrt_def)
+  apply (clarsimp simp: ready_queue_relation_def ksReadyQueues_asrt_def)
   apply (drule_tac x=d in spec)
   apply (drule_tac x=p in spec)
   apply clarsimp
@@ -844,9 +844,8 @@ lemma cthread_state_rel_imp_eq:
   apply (cases y, simp_all add: ThreadState_defs)+
   done
 
-(* FIXME: choose better name for this lemma *)
-lemma ksPSpace_valid_objs_bound_objs_nonzero:
-  "\<lbrakk>no_0_obj' s; valid_objs' s; map_to_tcbs (ksPSpace s) p = Some tcb\<rbrakk>
+lemma map_to_tcbs_Some_refs_nonzero:
+  "\<lbrakk>map_to_tcbs (ksPSpace s) p = Some tcb; no_0_obj' s; valid_objs' s\<rbrakk>
    \<Longrightarrow> tcbBoundNotification tcb \<noteq> Some 0
        \<and> tcbSchedPrev tcb \<noteq> Some 0
        \<and> tcbSchedNext tcb \<noteq> Some 0"
@@ -888,15 +887,14 @@ lemma tcb_ptr_to_ctcb_ptr_inj:
   by (auto simp: tcb_ptr_to_ctcb_ptr_def ctcb_offset_def)
 
 lemma
+  assumes "pspace_aligned' as" "pspace_distinct' as" "valid_tcb' atcb as"
   shows tcb_at'_tcbBoundNotification:
-  "\<lbrakk>pspace_aligned' as; pspace_distinct' as; valid_tcb' atcb as\<rbrakk>
-   \<Longrightarrow> bound (tcbBoundNotification atcb) \<longrightarrow> ntfn_at' (the (tcbBoundNotification atcb)) as"
+    "bound (tcbBoundNotification atcb) \<longrightarrow> ntfn_at' (the (tcbBoundNotification atcb)) as"
   and tcb_at'_tcbSchedPrev:
-  "\<lbrakk>pspace_aligned' as; pspace_distinct' as; valid_tcb' atcb as\<rbrakk>
-   \<Longrightarrow> tcbSchedPrev atcb \<noteq> None \<longrightarrow> tcb_at' (the (tcbSchedPrev atcb)) as"
+    "tcbSchedPrev atcb \<noteq> None \<longrightarrow> tcb_at' (the (tcbSchedPrev atcb)) as"
   and tcb_at'_tcbSchedNext:
-  "\<lbrakk>pspace_aligned' as; pspace_distinct' as; valid_tcb' atcb as\<rbrakk>
-   \<Longrightarrow> tcbSchedNext atcb \<noteq> None \<longrightarrow> tcb_at' (the (tcbSchedNext atcb)) as"
+    "tcbSchedNext atcb \<noteq> None \<longrightarrow> tcb_at' (the (tcbSchedNext atcb)) as"
+  using assms
   by (clarsimp simp: valid_tcb'_def obj_at'_def)+
 
 lemma cpspace_tcb_relation_unique:
@@ -921,8 +919,8 @@ lemma cpspace_tcb_relation_unique:
    apply (rename_tac p x y)
    apply (cut_tac ctes)
    apply (drule_tac x=x in spec, drule_tac x=y in spec, erule impE, fastforce)
-   apply (frule ksPSpace_valid_objs_bound_objs_nonzero[OF vs])
-   apply (frule ksPSpace_valid_objs_bound_objs_nonzero[OF vs'])
+   apply (frule map_to_tcbs_Some_refs_nonzero[OF _ vs])
+   apply (frule map_to_tcbs_Some_refs_nonzero[OF _ vs'])
    apply (frule ksPSpace_valid_objs_atcbVCPUPtr_nonzero[OF vs])
    apply (frule ksPSpace_valid_objs_atcbVCPUPtr_nonzero[OF vs'])
    apply (rename_tac atcb atcb')
@@ -941,10 +939,10 @@ lemma cpspace_tcb_relation_unique:
    apply (rule tcb.expand)
    apply clarsimp
    apply (intro conjI)
-          apply (simp add: cthread_state_rel_imp_eq)
-         apply (simp add: cfault_rel_imp_eq)
-        apply (case_tac "tcbBoundNotification atcb'", case_tac "tcbBoundNotification atcb"; clarsimp)
-        apply (clarsimp split: option.splits)
+        apply (simp add: cthread_state_rel_imp_eq)
+       apply (simp add: cfault_rel_imp_eq)
+      apply (case_tac "tcbBoundNotification atcb'", case_tac "tcbBoundNotification atcb"; clarsimp)
+      apply (clarsimp split: option.splits)
      apply (case_tac "tcbSchedPrev atcb'"; case_tac "tcbSchedPrev atcb"; clarsimp)
        apply (force dest!: tcb_at_not_NULL)
       apply (force dest!: tcb_at_not_NULL)

proof/crefine/AARCH64/Fastpath_Equiv.thy

@@ -1085,6 +1085,7 @@ crunch tcbContext[wp]: possibleSwitchTo "obj_at' (\<lambda>tcb. P ( (atcbContext
 crunch only_cnode_caps[wp]: doFaultTransfer "\<lambda>s. P (only_cnode_caps (ctes_of s))"
   (wp: crunch_wps simp: crunch_simps)
 
+(* FIXME: monadic_rewrite_l does not work with stateAssert here *)
 lemma tcbSchedDequeue_rewrite_not_queued:
   "monadic_rewrite True False (tcb_at' t and obj_at' (Not \<circ> tcbQueued) t)
      (tcbSchedDequeue t) (return ())"

proof/crefine/AARCH64/Finalise_C.thy

@@ -29,7 +29,7 @@ lemmas ksReadyQueues_head_end_def = ksReadyQueues_head_end_2_def
 lemma ksReadyQueues_asrt_ksReadyQueues_head_end:
   "ksReadyQueues_asrt s \<Longrightarrow> ksReadyQueues_head_end s"
   by (fastforce dest: tcbQueueHead_iff_tcbQueueEnd
-                simp: ksReadyQueues_asrt_def ksReadyQueues_head_end_def)
+                simp: ready_queue_relation_def ksReadyQueues_asrt_def ksReadyQueues_head_end_def)
 
 lemma tcbSchedEnqueue_ksReadyQueues_head_end[wp]:
   "tcbSchedEnqueue tcbPtr \<lbrace>ksReadyQueues_head_end\<rbrace>"
@@ -64,7 +64,8 @@ lemmas ksReadyQueues_head_end_tcb_at'_def = ksReadyQueues_head_end_tcb_at'_2_def
 lemma ksReadyQueues_asrt_ksReadyQueues_head_end_tcb_at':
   "\<lbrakk>ksReadyQueues_asrt s; pspace_aligned' s; pspace_distinct' s\<rbrakk>
    \<Longrightarrow> ksReadyQueues_head_end_tcb_at' s"
-  apply (clarsimp simp: ksReadyQueues_asrt_def ksReadyQueues_head_end_tcb_at'_def)
+  apply (clarsimp simp: ready_queue_relation_def ksReadyQueues_asrt_def
+                        ksReadyQueues_head_end_tcb_at'_def)
   apply (drule_tac x=d in spec)
   apply (drule_tac x=p in spec)
   apply (clarsimp simp: list_queue_relation_def)

proof/crefine/AARCH64/IpcCancel_C.thy

@@ -979,7 +979,7 @@ proof -
     apply (clarsimp simp: valid_tcb'_def)
     apply (frule (1) obj_at_cslift_tcb)
     apply (rule conjI)
-     apply (clarsimp simp: ksReadyQueues_asrt_def)
+     apply (clarsimp simp: ready_queue_relation_def ksReadyQueues_asrt_def)
      apply (drule_tac x="tcbDomain tcb" in spec)
      apply (drule_tac x="tcbPriority tcb" in spec)
      apply clarsimp
@@ -1112,7 +1112,7 @@ proof -
     apply (clarsimp simp: valid_tcb'_def)
     apply (frule (1) obj_at_cslift_tcb)
     apply (rule conjI)
-     apply (clarsimp simp: ksReadyQueues_asrt_def)
+     apply (clarsimp simp: ready_queue_relation_def ksReadyQueues_asrt_def)
      apply (drule_tac x="tcbDomain tcb" in spec)
      apply (drule_tac x="tcbPriority tcb" in spec)
      apply clarsimp
@@ -1539,7 +1539,7 @@ proof -
       apply fastforce
      apply fastforce
     apply (rule conjI)
-     apply (clarsimp simp: ksReadyQueues_asrt_def)
+     apply (clarsimp simp: ready_queue_relation_def ksReadyQueues_asrt_def)
      apply (drule_tac x="tcbDomain tcb" in spec)
      apply (drule_tac x="tcbPriority tcb" in spec)
      apply clarsimp
@@ -2557,10 +2557,10 @@ lemma cancelIPC_ccorres_helper:
                         cpspace_relation_def update_ep_map_tos typ_heap_simps')
        apply (elim conjE)
        apply (intro conjI)
-       \<comment> \<open>tcb relation\<close>
+           \<comment> \<open>tcb relation\<close>
            apply (erule ctcb_relation_null_ep_ptrs)
            subgoal by (clarsimp simp: comp_def)
-       \<comment> \<open>ep relation\<close>
+          \<comment> \<open>ep relation\<close>
           apply (rule cpspace_relation_ep_update_ep, assumption+)
            subgoal by (simp add: cendpoint_relation_def Let_def EPState_Idle_def)
           subgoal by simp
@@ -2590,45 +2590,43 @@ lemma cancelIPC_ccorres_helper:
       apply (simp add: remove1_empty rf_sr_def cstate_relation_def Let_def
                        cpspace_relation_def update_ep_map_tos typ_heap_simps')
       apply (elim conjE)
-        apply (intro conjI)
-            \<comment> \<open>tcb relation\<close>
-            apply (erule ctcb_relation_null_ep_ptrs)
-            subgoal by (clarsimp simp: comp_def)
-           \<comment> \<open>ep relation\<close>
-           apply (rule cpspace_relation_ep_update_ep, assumption+)
-            apply (simp add: cendpoint_relation_def Let_def isSendEP_def isRecvEP_def split: endpoint.splits split del: if_split)
-            \<comment> \<open>recv case\<close>
-             apply (subgoal_tac "pspace_canonical' \<sigma>")
-              prefer 2
-              apply fastforce
-             apply (clarsimp
-                     simp: h_t_valid_clift_Some_iff ctcb_offset_defs mask_shiftl_decompose
-                           tcb_queue_relation'_next_mask tcb_queue_relation'_prev_mask
-                           tcb_queue_relation'_next_canonical tcb_queue_relation'_prev_canonical
-                     simp flip: canonical_bit_def make_canonical_def
-                     cong: tcb_queue_relation'_cong)
-             subgoal by (intro impI conjI; simp)
-            \<comment> \<open>send case\<close>
-            apply (subgoal_tac "pspace_canonical' \<sigma>")
-             prefer 2
-             apply fastforce
-           apply (clarsimp
-                    simp: h_t_valid_clift_Some_iff ctcb_offset_defs mask_shiftl_decompose
-                          tcb_queue_relation'_next_mask tcb_queue_relation'_prev_mask
-                          tcb_queue_relation'_next_canonical tcb_queue_relation'_prev_canonical
-                    simp flip: canonical_bit_def
-                    cong: tcb_queue_relation'_cong)
-           subgoal by (intro impI conjI; simp)
-          \<comment> \<open>send case\<close>
+      apply (intro conjI)
+          \<comment> \<open>tcb relation\<close>
+          apply (erule ctcb_relation_null_ep_ptrs)
+          subgoal by (clarsimp simp: comp_def)
+         \<comment> \<open>ep relation\<close>
+         apply (rule cpspace_relation_ep_update_ep, assumption+)
+          apply (simp add: cendpoint_relation_def Let_def isSendEP_def isRecvEP_def
+                    split: endpoint.splits split del: if_split)
+           \<comment> \<open>recv case\<close>
            apply (subgoal_tac "pspace_canonical' \<sigma>")
             prefer 2
             apply fastforce
-          apply (clarsimp
-                   simp: h_t_valid_clift_Some_iff ctcb_offset_defs
-                         tcb_queue_relation'_next_mask tcb_queue_relation'_prev_mask
-                          tcb_queue_relation'_next_canonical tcb_queue_relation'_prev_canonical
+           apply (clarsimp simp: h_t_valid_clift_Some_iff ctcb_offset_defs mask_shiftl_decompose
+                                 tcb_queue_relation'_next_mask tcb_queue_relation'_prev_mask
+                                 tcb_queue_relation'_next_canonical tcb_queue_relation'_prev_canonical
+                      simp flip: canonical_bit_def make_canonical_def
+                           cong: tcb_queue_relation'_cong)
+           subgoal by (intro impI conjI; simp)
+          \<comment> \<open>send case\<close>
+          apply (subgoal_tac "pspace_canonical' \<sigma>")
+           prefer 2
+           apply fastforce
+         apply (clarsimp simp: h_t_valid_clift_Some_iff ctcb_offset_defs mask_shiftl_decompose
+                               tcb_queue_relation'_next_mask tcb_queue_relation'_prev_mask
+                               tcb_queue_relation'_next_canonical tcb_queue_relation'_prev_canonical
+                    simp flip: canonical_bit_def
+                         cong: tcb_queue_relation'_cong)
+          subgoal by (intro impI conjI; simp)
+         \<comment> \<open>send case\<close>
+         apply (subgoal_tac "pspace_canonical' \<sigma>")
+          prefer 2
+          apply fastforce
+         apply (clarsimp simp: h_t_valid_clift_Some_iff ctcb_offset_defs
+                               tcb_queue_relation'_next_mask tcb_queue_relation'_prev_mask
+                               tcb_queue_relation'_next_canonical tcb_queue_relation'_prev_canonical
                     simp flip: canonical_bit_def
-                    cong: tcb_queue_relation'_cong)
+                         cong: tcb_queue_relation'_cong)
         \<comment> \<open>ntfn relation\<close>
         apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1])
         apply simp

proof/crefine/AARCH64/IsolatedThreadAction.thy

@@ -1585,7 +1585,8 @@ lemma switchToThread_rewrite:
        (do Arch.switchToThread t; setCurThread t od)"
   apply (simp add: switchToThread_def Thread_H.switchToThread_def)
   apply (monadic_rewrite_l tcbSchedDequeue_rewrite, simp)
-  apply (repeat_unless \<open>rule monadic_rewrite_refl\<close> monadic_rewrite_symb_exec_l)
+   (* strip LHS of getters and asserts until LHS and RHS are the same *)
+   apply (repeat_unless \<open>rule monadic_rewrite_refl\<close> monadic_rewrite_symb_exec_l)
       apply wpsimp+
   apply (clarsimp simp: comp_def)
   done

proof/crefine/AARCH64/Recycle_C.thy

@@ -1008,21 +1008,11 @@ lemma cancelBadgedSends_ccorres:
            apply (clarsimp simp: cscheduler_action_relation_def st_tcb_at'_def
                           split: scheduler_action.split_asm)
            apply (rename_tac word)
-           apply (frule_tac x=word in tcbSchedEnqueue_cslift_precond_discharge)
-              apply simp
-             subgoal by clarsimp
-             subgoal by clarsimp
-             subgoal by clarsimp
-            subgoal by clarsimp
+           apply (frule_tac x=word in tcbSchedEnqueue_cslift_precond_discharge; simp?)
            subgoal by clarsimp
-             subgoal by clarsimp
-
           apply clarsimp
           apply (rule conjI)
-           apply (frule(3) tcbSchedEnqueue_cslift_precond_discharge)
-              subgoal by clarsimp
-             apply clarsimp
-            subgoal by clarsimp
+           apply (frule tcbSchedEnqueue_cslift_precond_discharge; simp?)
            subgoal by clarsimp
           apply clarsimp
           apply (rule context_conjI)
@@ -1062,22 +1052,19 @@ lemma cancelBadgedSends_ccorres:
    apply (clarsimp split: if_split)
    apply (drule sym_refsD, clarsimp)
    apply (drule(1) bspec)+
-apply (frule ksReadyQueues_asrt_ksReadyQueues_head_end)
-apply (frule invs_pspace_aligned')
-apply (frule invs_pspace_distinct')
-apply (frule (2) ksReadyQueues_asrt_ksReadyQueues_head_end_tcb_at')
-
-apply (auto simp: obj_at'_def projectKOs state_refs_of'_def pred_tcb_at'_def tcb_bound_refs'_def
-
-              dest!: symreftype_inverse')[1]
-apply (frule ksReadyQueues_asrt_ksReadyQueues_head_end)
-apply (frule invs_pspace_aligned')
-apply (frule invs_pspace_distinct')
-apply (frule (2) ksReadyQueues_asrt_ksReadyQueues_head_end_tcb_at')
-
-apply safe
-done
-
+   apply (frule ksReadyQueues_asrt_ksReadyQueues_head_end)
+   apply (frule invs_pspace_aligned')
+   apply (frule invs_pspace_distinct')
+   apply (frule (2) ksReadyQueues_asrt_ksReadyQueues_head_end_tcb_at')
+   apply (fastforce simp: obj_at'_def projectKOs state_refs_of'_def pred_tcb_at'_def
+                          tcb_bound_refs'_def
+                   dest!: symreftype_inverse')
+  apply (frule ksReadyQueues_asrt_ksReadyQueues_head_end)
+  apply (frule invs_pspace_aligned')
+  apply (frule invs_pspace_distinct')
+  apply (frule (2) ksReadyQueues_asrt_ksReadyQueues_head_end_tcb_at')
+  apply fastforce
+  done
 
 lemma tcb_ptr_to_ctcb_ptr_force_fold:
   "x + 2 ^ ctcb_size_bits = ptr_val (tcb_ptr_to_ctcb_ptr x)"

proof/crefine/AARCH64/SR_lemmas_C.thy

@@ -413,8 +413,8 @@ lemma cmdbnode_relation_mdb_node_to_H [simp]:
 
 definition tcb_no_ctes_proj ::
   "tcb \<Rightarrow> Structures_H.thread_state \<times> machine_word \<times> machine_word \<times> arch_tcb \<times> bool \<times> word8
-   \<times> word8 \<times> word8 \<times> nat \<times> fault option \<times> machine_word option
-   \<times> machine_word option \<times> machine_word option"
+          \<times> word8 \<times> word8 \<times> nat \<times> fault option \<times> machine_word option
+          \<times> machine_word option \<times> machine_word option"
   where
   "tcb_no_ctes_proj t \<equiv>
      (tcbState t, tcbFaultHandler t, tcbIPCBuffer t, tcbArch t, tcbQueued t,

proof/crefine/AARCH64/Schedule_C.thy

@@ -102,11 +102,11 @@ lemma Arch_switchToThread_ccorres:
   apply (clarsimp simp: typ_heap_simps ctcb_relation_def carch_tcb_relation_def)
   done
 
-lemma all_invs_but_ct_idle_or_in_cur_domain'_pspace_aligned':
+lemma invs_no_cicd'_pspace_aligned':
   "all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> pspace_aligned' s"
   by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_pspace'_def)
 
-lemma all_invs_but_ct_idle_or_in_cur_domain'_pspace_distinct':
+lemma invs_no_cicd'_pspace_distinct':
   "all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> pspace_distinct' s"
   by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_pspace'_def)
 
@@ -145,8 +145,7 @@ lemma switchToThread_ccorres:
      apply (clarsimp simp: setCurThread_def simpler_modify_def rf_sr_def cstate_relation_def
                            Let_def carch_state_relation_def cmachine_state_relation_def)
     apply (wpsimp wp: Arch_switchToThread_invs_no_cicd' hoare_drop_imps
-           | strengthen all_invs_but_ct_idle_or_in_cur_domain'_pspace_aligned'
-                        all_invs_but_ct_idle_or_in_cur_domain'_pspace_distinct')+
+           | strengthen invs_no_cicd'_pspace_aligned' invs_no_cicd'_pspace_distinct')+
   done
 
 lemma activateThread_ccorres:
@@ -269,25 +268,6 @@ lemma ccorres_pre_getQueue:
    apply (simp add: maxDom_to_H maxPrio_to_H)+
   done
 
-(* FIXME: replace the version of this rule in Schedule_R with this more general version *)
-lemma lookupBitmapPriority_obj_at':
-  "\<lbrakk>ksReadyQueuesL1Bitmap s d \<noteq> 0; valid_bitmapQ s; bitmapQ_no_L1_orphans s;
-    ksReadyQueues_asrt s; ready_qs_runnable s; pspace_aligned' s; pspace_distinct' s\<rbrakk>
-   \<Longrightarrow> obj_at' (inQ d (lookupBitmapPriority d s)
-                and runnable' \<circ> tcbState)
-               (the (tcbQueueHead
-                     (ksReadyQueues s (d, lookupBitmapPriority d s)))) s"
-  apply (drule (2) bitmapQ_from_bitmap_lookup)
-  apply (simp add: valid_bitmapQ_bitmapQ_simp)
-  apply (clarsimp simp: ksReadyQueues_asrt_def tcbQueueEmpty_def)
-  apply (drule_tac x=d in spec)
-  apply (drule_tac x="lookupBitmapPriority d s" in spec)
-  apply clarsimp
-  apply (frule (3) obj_at'_tcbQueueHead_ksReadyQueues)
-  apply (fastforce simp: obj_at'_and ready_qs_runnable_def obj_at'_def st_tcb_at'_def inQ_def
-                         tcbQueueEmpty_def)
-  done
-
 lemma chooseThread_ccorres:
   "ccorres dc xfdc all_invs_but_ct_idle_or_in_cur_domain' UNIV []
      chooseThread (Call chooseThread_'proc)"
@@ -394,16 +374,16 @@ proof -
     apply (frule invs_no_cicd'_valid_bitmaps)
     apply (frule valid_bitmaps_bitmapQ_no_L1_orphans)
     apply (frule valid_bitmaps_valid_bitmapQ)
-    apply (clarsimp simp: ksReadyQueues_asrt_def cong: conj_cong)
+    apply (clarsimp simp: ready_queue_relation_def ksReadyQueues_asrt_def cong: conj_cong)
     apply (intro conjI impI)
          apply (fastforce intro: lookupBitmapPriority_le_maxPriority)
         apply (fastforce dest!: bitmapQ_from_bitmap_lookup valid_bitmapQ_bitmapQ_simp)
        apply (fastforce dest!: lookupBitmapPriority_obj_at'
-                         simp: ksReadyQueues_asrt_def st_tcb_at'_def obj_at'_def)
+                         simp: ready_queue_relation_def ksReadyQueues_asrt_def st_tcb_at'_def obj_at'_def)
       apply (fastforce dest: lookupBitmapPriority_le_maxPriority)
      apply (fastforce dest!: bitmapQ_from_bitmap_lookup valid_bitmapQ_bitmapQ_simp)
     apply (fastforce dest!: lookupBitmapPriority_obj_at'
-                      simp: ksReadyQueues_asrt_def st_tcb_at'_def obj_at'_def)
+                      simp: ready_queue_relation_def ksReadyQueues_asrt_def st_tcb_at'_def obj_at'_def)
     done
 qed