Add sorted_ipc_queues invariant

lib/Lib.thy

@@ -2269,6 +2269,16 @@ lemma in_set_zip2:
   "(x, y) \<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys"
   by (erule in_set_zipE)
 
+lemma in_set_zipD:
+  "t \<in> set (zip xs ys) \<Longrightarrow> fst t \<in> set xs \<and> snd t \<in> set ys"
+  by (clarsimp simp add: set_zip)
+
+lemma set_map_fst_filter_zip:
+  "set (map fst (filter P (zip xs ys))) \<subseteq> set xs"
+  apply (induct xs, simp)
+  apply (case_tac ys; simp)
+  by (metis (mono_tags, lifting) image_Collect_subsetI insertI2 in_set_zipD)
+
 lemma map_zip_snd_take:
   "map (\<lambda>(x, y). f y) (zip xs ys) = map f (take (length xs) ys)"
   apply (subst map_zip_snd' [symmetric, where xs=xs and ys="take (length xs) ys"], simp)

lib/Monad_Lists.thy

@@ -512,6 +512,33 @@ lemma mapM_wp':
   apply simp
   done
 
+lemma mapM_gets_the_wp:
+  "\<lbrace>\<lambda>s. \<forall>vs. map (\<lambda>t. f t s) ts = map Some vs \<longrightarrow> P vs s\<rbrace>
+   mapM (gets_the \<circ> f) ts
+   \<lbrace>P\<rbrace>"
+  unfolding comp_def
+proof (induct ts arbitrary: P)
+  case Nil thus ?case by (wpsimp simp: mapM_Nil)
+next
+  case (Cons x xs) show ?case by (wpsimp simp: mapM_Cons wp: Cons)
+qed
+
+lemma mapM_gets_the_wp_nth:
+  "\<lbrace>\<lambda>s. \<forall>vs. (\<forall>i < length vs. f (ts ! i) s = Some (vs ! i)) \<longrightarrow> P vs s\<rbrace>
+   mapM (gets_the \<circ> f) ts
+   \<lbrace>P\<rbrace>"
+  apply (wpsimp wp: mapM_gets_the_wp)
+  by (simp add: map_equality_iff)
+
+lemma mapM_gets_the_sp:
+  "\<lbrace>P\<rbrace> mapM (gets_the \<circ> f) ts \<lbrace>\<lambda>rv s. P s \<and> map (\<lambda>t. f t s) ts = map Some rv\<rbrace>"
+  by (wpsimp wp: mapM_gets_the_wp simp: comp_def)
+
+lemma mapM_gets_the_sp_nth:
+  "\<lbrace>P\<rbrace> mapM (gets_the \<circ> f) ts \<lbrace>\<lambda>rv s. P s \<and> (\<forall>i < length rv. f (ts ! i) s = Some (rv ! i))\<rbrace>"
+  apply (wpsimp wp: mapM_gets_the_wp simp: comp_def)
+  by (simp add: map_equality_iff)
+
 lemma mapM_set:
   assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>"
   assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>"

lib/Monads/reader_option/Reader_Option_Monad.thy

@@ -29,7 +29,7 @@ definition opt_map :: "('s,'a) lookup \<Rightarrow> ('a \<Rightarrow> 'b option)
   "f |> g \<equiv> \<lambda>s. case f s of None \<Rightarrow> None | Some x \<Rightarrow> g x"
 
 abbreviation opt_map_Some :: "('s \<rightharpoonup> 'a) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 's \<rightharpoonup> 'b" (infixl "||>" 54) where
-  "f ||> g \<equiv> f |> (Some \<circ> g)"
+  "f ||> g \<equiv> f |> (\<lambda>s. Some (g s))"
 
 lemmas opt_map_Some_def = opt_map_def
 
@@ -118,7 +118,7 @@ lemma opt_map_Some_foldr_upd:
 
 lemmas opt_map_foldr_upd_simps = opt_map_foldr_upd opt_map_Some_foldr_upd
 
-lemma opt_map_Some_comp[simp]:
+lemma opt_map_Some_comp:
   "f ||> g ||> h = f ||> h o g"
   by (fastforce simp: opt_map_def split: option.split)
 
@@ -143,10 +143,6 @@ lemma opt_map_zero_r[simp]:
   "f |> Map.empty = Map.empty"
   by (fastforce simp: opt_map_def split: option.split)
 
-lemma opt_map_Some_eta_fold:
-  "f |> (\<lambda>x. Some (g x)) = f ||> g"
-  by (simp add: o_def)
-
 lemma case_opt_map_distrib:
   "(\<lambda>s. case_option None g (f s)) |> h = (\<lambda>s. case_option None (g |> h) (f s))"
   by (fastforce simp: opt_map_def split: option.splits)

proof/access-control/Syscall_AC.thy

@@ -976,7 +976,7 @@ crunch_ignore (add: cap_swap_ext cap_move_ext cap_insert_ext create_cap_ext set_
 
 lemma zet_zip_contrapos:
   "fst t \<notin> set xs  \<Longrightarrow> t \<notin> set (zip xs ys)"
-  by (auto simp: set_zip_helper)
+  by (auto simp: in_set_zipD)
 
 lemma ct_active_update[simp]:
   "ct_active (s\<lparr>cdt := b\<rparr>) = ct_active s"

proof/crefine/AARCH64/Retype_C.thy

@@ -7301,7 +7301,7 @@ lemma ccorres_typ_region_bytes_dummy:
   apply (simp add: hrs_htd_update gsCNodes_typ_region_bytes
                    cnodes_retype_have_size_mono[where T=S]
                    tcb_ctes_typ_region_bytes[OF _ _ invs_pspace_aligned']
-                   pte_typ_region_bytes o_def)
+                   pte_typ_region_bytes)
   (* True for either version of config_ARM_PA_SIZE_BITS_40 with corresponding max vm level change *)
   apply (simp add: cmap_array_typ_region_bytes_triv invs_pspace_aligned' bit_simps
                    objBitsT_simps word_bits_def zero_ranges_are_zero_typ_region_bytes
@@ -8005,7 +8005,7 @@ crunch placeNewDataObject
   for ksArchState[wp]: "\<lambda>s. P (ksArchState s)"
   (simp: crunch_simps)
 
-lemma createObject_cnodes_have_size_pt[unfolded o_def]:
+lemma createObject_cnodes_have_size_pt:
   "\<lbrace>\<lambda>s. is_aligned ptr (APIType_capBits newType userSize)
       \<and> cnodes_retype_have_size R (APIType_capBits newType userSize) (gsPTTypes (ksArchState s) ||> (\<lambda>pt_t. pt_bits pt_t - cte_level_bits))\<rbrace>
     createObject newType ptr userSize dev
@@ -8014,8 +8014,7 @@ lemma createObject_cnodes_have_size_pt[unfolded o_def]:
   apply (simp add: createObject_def)
   apply (rule hoare_pre)
    apply (wp mapM_x_wp' | wpc | simp add: createObjects_def AARCH64_H.createObject_def updatePTType_def)+
-  apply (cases newType, simp_all add: AARCH64_H.toAPIType_def o_def)
-   apply (rule conjI, clarsimp)+
+  apply (cases newType, simp_all add: AARCH64_H.toAPIType_def)
    apply clarsimp
   supply fun_upd_def[symmetric, simp del] fun_upd_apply[simp]
   apply (clarsimp simp: APIType_capBits_def cnodes_retype_have_size_def bit_simps cte_level_bits_def

proof/crefine/ARM_HYP/Arch_C.thy

@@ -2102,7 +2102,7 @@ lemma performPageInvocationMapPDE_ccorres:
           apply (simp add: typ_at_to_obj_at_arches[symmetric])
           apply ((wp mapM_x_storePDE_pde_mappings' mapM_x_wp' valid_pde_slots_lift2 | simp add: split_def)+)[2]
          apply (clarsimp simp: valid_pde_mapping'_def valid_pde_slots'2_def)
-         apply (drule set_zip_helper, clarsimp)
+         apply (drule in_set_zipD, clarsimp)
         apply clarsimp
         apply (simp add: typ_at_to_obj_at_arches)
         apply (frule bspec, erule hd_in_zip_set)

proof/crefine/RISCV64/IpcCancel_C.thy

@@ -164,7 +164,8 @@ lemma ntfn_ptr_set_queue_spec:
 
 lemma cancelSignal_ccorres_helper:
   "ccorres dc xfdc (invs' and (\<lambda>s. sym_refs (state_refs_of' s))
-                    and st_tcb_at' ((=) (BlockedOnNotification ntfn)) thread and ko_at' ntfn' ntfn)
+                    and st_tcb_at' ((=) (BlockedOnNotification ntfn)) thread and ko_at' ntfn' ntfn
+                    and K (distinct (ntfnQueue (ntfnObj ntfn'))))
         UNIV
         []
         (setNotification ntfn (ntfnObj_update
@@ -2472,7 +2473,7 @@ lemma cancelSignal_ccorres[corres]:
    apply (simp only: simp_list_case_return return_bind ccorres_seq_skip)
    apply (rule ccorres_stateAssert)+
    apply (rule ccorres_pre_getNotification)
-   apply (rule ccorres_assert)
+   apply (rule ccorres_assert2)+
    apply (rule ccorres_rhs_assoc2)+
    apply (ctac (no_vcg) add: cancelSignal_ccorres_helper)
      apply (ctac add: setThreadState_ccorres)
@@ -2552,11 +2553,11 @@ lemma ep_ptr_set_queue_spec:
   oops
 
 lemma valid_ep_blockedD:
-  "\<lbrakk> valid_ep' ep s; (isSendEP ep \<or> isRecvEP ep) \<rbrakk> \<Longrightarrow> (epQueue ep) \<noteq> [] \<and> (\<forall>t\<in>set (epQueue ep). tcb_at' t s) \<and> distinct (epQueue ep)"
+  "\<lbrakk> valid_ep' ep s; isSendEP ep \<or> isRecvEP ep \<rbrakk>
+   \<Longrightarrow> epQueue ep \<noteq> [] \<and> (\<forall>t\<in>set (epQueue ep). tcb_at' t s)"
   unfolding valid_ep'_def isSendEP_def isRecvEP_def
   by (clarsimp split: endpoint.splits)
 
-
 lemma ep_to_ep_queue:
   assumes ko: "ko_at' ep' ep s"
   and     waiting: "(isSendEP ep' \<or> isRecvEP ep')"
@@ -2742,7 +2743,7 @@ lemma cancelIPC_ccorres_helper:
   "ccorres dc xfdc (invs' and (\<lambda>s. sym_refs (state_refs_of' s)) and
          st_tcb_at' (\<lambda>st. (isBlockedOnSend st \<or> isBlockedOnReceive st)
                             \<and> blockingObject st = ep) thread
-        and ko_at' ep' ep)
+        and ko_at' ep' ep and K (distinct (epQueue ep')))
         {s. epptr_' s = Ptr ep}
         []
         (setEndpoint ep (if remove1 thread (epQueue ep') = [] then Structures_H.endpoint.IdleEP

proof/crefine/RISCV64/Ipc_C.thy

@@ -4467,21 +4467,22 @@ lemma ccorres_getCTE_cte_at:
   done
 
 lemma sendIPC_dequeue_ccorres_helper:
-  "ep_ptr = Ptr ep ==>
-  ccorres (\<lambda>rv rv'. rv' = tcb_ptr_to_ctcb_ptr dest) dest___ptr_to_struct_tcb_C_'
-           (invs' and (\<lambda>s. sym_refs (state_refs_of' s))
-                  and st_tcb_at' (\<lambda>st. isBlockedOnReceive st \<and>
-                                       blockingObject st = ep) dest
-                  and ko_at' (RecvEP (dest#rest)) ep) UNIV hs
-           (setEndpoint ep $ case rest of [] \<Rightarrow> Structures_H.IdleEP
-                                        | (a#list) \<Rightarrow> Structures_H.RecvEP rest)
-        (\<acute>queue :== CALL ep_ptr_get_queue(ep_ptr);;
-         \<acute>dest___ptr_to_struct_tcb_C :== head_C \<acute>queue;;
-         \<acute>queue :== CALL tcbEPDequeue(\<acute>dest___ptr_to_struct_tcb_C,\<acute>queue);;
-         CALL ep_ptr_set_queue(ep_ptr,\<acute>queue);;
-         IF head_C \<acute>queue = Ptr 0 THEN
-             CALL endpoint_ptr_set_state(ep_ptr,scast EPState_Idle)
-         FI)"
+  "ep_ptr = Ptr ep \<Longrightarrow>
+   ccorres (\<lambda>rv rv'. rv' = tcb_ptr_to_ctcb_ptr dest) dest___ptr_to_struct_tcb_C_'
+     (invs' and (\<lambda>s. sym_refs (state_refs_of' s))
+            and st_tcb_at' (\<lambda>st. isBlockedOnReceive st \<and> blockingObject st = ep) dest
+            and ko_at' (RecvEP (dest#rest)) ep
+            and K (distinct (dest # rest)))
+     UNIV hs
+     (setEndpoint ep $ case rest of [] \<Rightarrow> Structures_H.IdleEP
+                                  | (a#list) \<Rightarrow> Structures_H.RecvEP rest)
+     (\<acute>queue :== CALL ep_ptr_get_queue(ep_ptr);;
+      \<acute>dest___ptr_to_struct_tcb_C :== head_C \<acute>queue;;
+      \<acute>queue :== CALL tcbEPDequeue(\<acute>dest___ptr_to_struct_tcb_C,\<acute>queue);;
+      CALL ep_ptr_set_queue(ep_ptr,\<acute>queue);;
+      IF head_C \<acute>queue = Ptr 0 THEN
+          CALL endpoint_ptr_set_state(ep_ptr,scast EPState_Idle)
+      FI)"
   apply (rule ccorres_from_vcg)
   apply (rule allI)
   apply (rule conseqPre, vcg)
@@ -4503,6 +4504,7 @@ lemma sendIPC_dequeue_ccorres_helper:
    apply (rule_tac x=\<sigma> in exI)
    apply (intro conjI)
        apply assumption+
+     apply fastforce
     apply (drule (2) ep_to_ep_queue)
     apply (simp add: tcb_queue_relation'_def)
    apply (clarsimp simp: typ_heap_simps cendpoint_relation_def Let_def
@@ -4852,7 +4854,7 @@ lemma sendIPC_enqueue_ccorres_helper:
                 and ko_at' (ep::Structures_H.endpoint) epptr
                 and K ((ep = IdleEP \<and> queue = [thread]) \<or>
                        (\<exists>q. ep = SendEP q \<and> thread \<notin> set q \<and>
-                            queue = q @ [thread])))
+                            queue = q @ [thread] \<and> distinct q)))
            UNIV hs
            (setEndpoint epptr (Structures_H.endpoint.SendEP queue))
            (\<acute>queue :== CALL ep_ptr_get_queue(ep_Ptr epptr);;
@@ -5379,7 +5381,7 @@ lemma receiveIPC_enqueue_ccorres_helper:
                 and ko_at' (ep::Structures_H.endpoint) epptr
                 and K ((ep = IdleEP \<and> queue = [thread]) \<or>
                        (\<exists>q. ep = RecvEP q \<and> thread \<notin> set q \<and>
-                            queue = q @ [thread])))
+                            queue = q @ [thread] \<and> distinct q)))
            UNIV hs
            (setEndpoint epptr (Structures_H.endpoint.RecvEP queue))
            (\<acute>queue :== CALL ep_ptr_get_queue(ep_Ptr epptr);;
@@ -5522,7 +5524,9 @@ lemma receiveIPC_dequeue_ccorres_helper:
            (invs' and (\<lambda>s. sym_refs (state_refs_of' s))
                   and st_tcb_at' (\<lambda>st. isBlockedOnSend st \<and>
                                        blockingObject st = ep) sender
-                  and ko_at' (SendEP (sender#rest)) ep) UNIV hs
+                  and ko_at' (SendEP (sender # rest)) ep
+                  and K (distinct (sender # rest)))
+           UNIV hs
            (setEndpoint ep (case rest of [] \<Rightarrow> Structures_H.IdleEP
                                        | (a#list) \<Rightarrow> Structures_H.SendEP rest))
         (\<acute>queue :== CALL ep_ptr_get_queue(Ptr ep);;
@@ -5553,6 +5557,7 @@ lemma receiveIPC_dequeue_ccorres_helper:
    apply (rule_tac x=\<sigma> in exI)
    apply (intro conjI)
        apply assumption+
+     apply fastforce
     apply (drule (2) ep_to_ep_queue)
     apply (simp add: tcb_queue_relation'_def)
    apply (clarsimp simp: typ_heap_simps cendpoint_relation_def Let_def
@@ -6085,7 +6090,8 @@ lemma sendSignal_dequeue_ccorres_helper:
            (invs' and (\<lambda>s. sym_refs (state_refs_of' s))
                   and st_tcb_at' ((=) (BlockedOnNotification ntfn)) dest
                   and ko_at' nTFN ntfn
-                  and K (ntfnObj nTFN = WaitingNtfn (dest # rest))) UNIV hs
+                  and K (ntfnObj nTFN = WaitingNtfn (dest # rest)) and K (distinct (dest # rest)))
+           UNIV hs
            (setNotification ntfn $ ntfnObj_update (\<lambda>_. case rest of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn
                                         | (a#list) \<Rightarrow> Structures_H.ntfn.WaitingNtfn rest) nTFN)
         (\<acute>ntfn_queue :== CALL ntfn_ptr_get_queue(Ptr ntfn);;
@@ -6516,7 +6522,7 @@ lemma receiveSignal_enqueue_ccorres_helper:
                 and ko_at' (ntfn::Structures_H.notification) ntfnptr
                 and K ((ntfnObj ntfn = IdleNtfn \<and> queue = [thread]) \<or>
                        (\<exists>q. ntfnObj ntfn = WaitingNtfn q \<and> thread \<notin> set q \<and>
-                            queue = q @ [thread])))
+                            queue = q @ [thread] \<and> distinct q)))
            UNIV hs
            (setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.WaitingNtfn queue) ntfn)
            (\<acute>ntfn_queue :== CALL ntfn_ptr_get_queue(ntfn_Ptr ntfnptr);;

proof/crefine/RISCV64/Recycle_C.thy

@@ -934,6 +934,7 @@ lemma cancelBadgedSends_ccorres:
       apply (rule ccorres_return_Skip)
      apply (simp add: ccorres_cond_iffs)
      apply (rule ccorres_return_Skip)
+    apply (rule ccorres_assert2)
     apply (rename_tac list)
     apply (simp add: Collect_True Collect_False endpoint_state_defs
                      ccorres_cond_iffs
@@ -964,6 +965,7 @@ lemma cancelBadgedSends_ccorres:
           subgoal by simp
          apply (simp add: refill_buffer_relation_def image_def dom_def Let_def typ_heap_simps
                           update_ep_map_tos)
+        apply (thin_tac "distinct _")
         apply (rule ccorres_symb_exec_r)
           apply (rule_tac xs=list in filterM_voodoo)
           apply (rule_tac P="\<lambda>xs s. (\<forall>x \<in> set xs \<union> set list.

proof/crefine/RISCV64/SR_lemmas_C.thy

@@ -1212,8 +1212,7 @@ lemma ntfn_blocked_in_queueD:
 (* MOVE *)
 lemma valid_ntfn_isWaitingNtfnD:
   "\<lbrakk> valid_ntfn' ntfn s; isWaitingNtfn (ntfnObj ntfn) \<rbrakk>
-  \<Longrightarrow> (ntfnQueue (ntfnObj ntfn)) \<noteq> [] \<and> (\<forall>t\<in>set (ntfnQueue (ntfnObj ntfn)). tcb_at' t s)
-    \<and> distinct (ntfnQueue (ntfnObj ntfn))"
+  \<Longrightarrow> ntfnQueue (ntfnObj ntfn) \<noteq> [] \<and> (\<forall>t\<in>set (ntfnQueue (ntfnObj ntfn)). tcb_at' t s)"
   unfolding valid_ntfn'_def isWaitingNtfn_def
   by (clarsimp split: Structures_H.notification.splits ntfn.splits)
 

proof/invariant-abstract/ARM/ArchArch_AI.thy

@@ -192,7 +192,7 @@ lemmas perform_asid_pool_invocation_typ_ats [wp] =
 
 
 lemma perform_asid_control_invocation_tcb_at:
-  "\<lbrace>invs and valid_aci aci and st_tcb_at active p and
+  "\<lbrace>invs and valid_aci aci and tcb_at p and ex_nonz_cap_to p and
     K (\<forall>w a b c. aci = asid_control_invocation.MakePool w a b c \<longrightarrow> w \<noteq> p)\<rbrace>
   perform_asid_control_invocation aci
   \<lbrace>\<lambda>rv. tcb_at p\<rbrace>"
@@ -204,10 +204,6 @@ lemma perform_asid_control_invocation_tcb_at:
   apply (intro impI conjI)
     apply (clarsimp simp: retype_addrs_def obj_bits_api_def default_arch_object_def image_def ptr_add_def)
    apply (clarsimp simp: st_tcb_at_tcb_at)+
-  apply (frule st_tcb_ex_cap)
-    apply fastforce
-   apply (clarsimp split: Structures_A.thread_state.splits)
-   apply auto[1]
   apply (clarsimp simp: ex_nonz_cap_to_def valid_aci_def)
   apply (frule invs_untyped_children)
   apply (clarsimp simp:cte_wp_at_caps_of_state)
@@ -250,9 +246,10 @@ lemma invoke_arch_tcb:
     apply fastforce
    apply (clarsimp split: Structures_A.thread_state.splits)
    apply auto[1]
-  apply (clarsimp simp: ex_nonz_cap_to_def)
+  apply (frule st_tcb_at_tcb_at)
+  apply clarsimp
   apply (frule invs_untyped_children)
-  apply (clarsimp simp:cte_wp_at_caps_of_state)
+  apply (clarsimp simp: ex_nonz_cap_to_def cte_wp_at_caps_of_state)
   apply (erule_tac ptr="(aa,ba)" in untyped_children_in_mdbE[where P="\<lambda>c. t \<in> zobj_refs c" for t])
       apply (simp add: cte_wp_at_caps_of_state)+
      apply fastforce