rt spec+proof: restrict reply grant rights

In MCS configurations, a server's ability to grant capabilities when
replying to a call were previously determined entirely by the grant
right on the reply capability the server supplied when calling
`receiveIPC`. If the server had sufficient untyped memory, it could
create arbitrary reply capabilities, giving itself the ability to grant
to its clients. Consequently, the only way to restrict a server's
ability to grant to its clients was to avoid giving it untyped memory.
This would break the expected authority confinement property.

Contrast this with non-MCS configurations, where the grant rights on a
server's receive endpoint control the server's ability to grant
capabilities when replying to calls. This makes it much easier to
restrict a server's ability to grant when replying.

This commit makes MCS configurations behave more like non-MCS
configurations: In order to grant capabilities when replying to a call,
a server must have a grant right on the receive endpoint capability
when it calls `receiveIPC`.

This commit also removes the grant right from reply caps, as following the
previous change this right has no clear use case.

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

proof/crefine/RISCV64/CSpace_C.thy

@@ -30,9 +30,6 @@ lemma maskCapRights_cap_cases:
                         (\<lambda>_. capNtfnCanReceive c \<and> capAllowRead R)
                         (capNtfnCanSend_update
                           (\<lambda>_. capNtfnCanSend c \<and> capAllowWrite R) c))
-  | ReplyCap _ _ \<Rightarrow>
-    return (capReplyCanGrant_update
-             (\<lambda>_. capReplyCanGrant c \<and> capAllowGrant R) c)
   | _ \<Rightarrow> return c)"
   apply (simp add: maskCapRights_def Let_def split del: if_split)
   apply (cases c; simp add: isCap_simps split del: if_split)
@@ -63,10 +60,9 @@ lemma maskVMRights_spec:
     \<acute>ret__unsigned_long && mask 2 = \<acute>ret__unsigned_long \<and>
     \<acute>ret__unsigned_long \<noteq> 0 \<rbrace>"
   apply vcg
-  apply (clarsimp simp: vmrights_defs vmrights_to_H_def maskVMRights_def mask_def
-                        cap_rights_to_H_def to_bool_def
-                  split: bool.split)
-  done
+  by (clarsimp simp: vmrights_defs vmrights_to_H_def maskVMRights_def mask_def
+                     cap_rights_to_H_def to_bool_def
+              split: bool.split)
 
 lemma frame_cap_rights [simp]:
   "cap_get_tag cap = scast cap_frame_cap
@@ -134,15 +130,6 @@ lemma to_bool_ntfn_cap_bf:
   apply simp
   done
 
-lemma to_bool_reply_cap_bf:
-  "cap_lift c = Some (Cap_reply_cap cap)
-   \<Longrightarrow> to_bool (capReplyCanGrant_CL cap) = to_bool_bf (capReplyCanGrant_CL cap)"
-  apply (simp add: cap_lift_def Let_def split: if_split_asm)
-  apply (subst to_bool_bf_to_bool_mask,
-         clarsimp simp: cap_lift_thread_cap mask_def word_bw_assocs)+
-  apply simp
-  done
-
 lemma to_bool_ep_cap_bf:
   "cap_lift c = Some (Cap_endpoint_cap cap) \<Longrightarrow>
   to_bool (capCanSend_CL cap) = to_bool_bf (capCanSend_CL cap) \<and>
@@ -291,17 +278,6 @@ lemma maskCapRights_ccorres [corres]:
         apply (rule conseqPre)
          apply vcg
         apply (simp add: cap_get_tag_isCap isCap_simps return_def)
-        apply clarsimp
-        apply (unfold ccap_relation_def)[1]
-        apply (simp add: cap_reply_cap_lift [THEN iffD1])
-        apply (clarsimp simp: cap_to_H_def)
-        apply (simp add: map_option_case split: option.splits)
-        apply (clarsimp simp add: cap_to_H_def Let_def
-                        split: cap_CL.splits if_split_asm)
-        apply (simp add: cap_reply_cap_lift_def)
-        apply (simp add: ccap_rights_relation_def cap_rights_to_H_def
-                         to_bool_reply_cap_bf
-                         to_bool_mask_to_bool_bf[simplified] to_bool_cap_rights_bf)
        apply (simp add: Collect_const_mem)
        apply csymbr
        apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const)

proof/crefine/RISCV64/Ipc_C.thy

@@ -283,14 +283,6 @@ lemma ccap_relation_ep_helpers:
                      cap_endpoint_cap_lift_def word_size
               elim!: ccap_relationE)
 
-(* FIXME move *)
-lemma ccap_relation_reply_helpers:
-  "\<lbrakk> ccap_relation cap cap'; cap_get_tag cap' = scast cap_reply_cap \<rbrakk> \<Longrightarrow>
-   capReplyCanGrant_CL (cap_reply_cap_lift cap') = from_bool (capReplyCanGrant cap)"
-  by (clarsimp simp: cap_lift_reply_cap cap_to_H_simps
-                     cap_reply_cap_lift_def word_size
-              elim!: ccap_relationE)
-
 (*FIXME: arch_split: C kernel names hidden by Haskell names *)
 (*FIXME: fupdate simplification issues for 2D arrays *)
 abbreviation "syscallMessageC \<equiv>  kernel_all_global_addresses.fault_messages.[unat MessageID_Syscall]"

proof/crefine/RISCV64/SR_lemmas_C.thy

@@ -253,8 +253,7 @@ lemma cap_get_tag_ReplyCap:
    assumes cr: "ccap_relation cap cap'"
    shows "(cap_get_tag cap' = scast cap_reply_cap) =
    (cap =
-       ReplyCap (capReplyPtr_CL (cap_reply_cap_lift cap'))
-                (to_bool (capReplyCanGrant_CL (cap_reply_cap_lift cap'))))"
+       ReplyCap (capReplyPtr_CL (cap_reply_cap_lift cap')))"
    using cr
    apply -
    apply (rule iffI)
@@ -1787,6 +1786,19 @@ lemma obj_at_cslift_sc:
   apply fastforce
   done
 
+lemma obj_at_cslift_reply:
+  fixes P :: "reply \<Rightarrow> bool"
+  shows "\<lbrakk>obj_at' P sc s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow>
+  \<exists>ko ko'. ko_at' ko sc s \<and> P ko \<and>
+        cslift s' (Ptr sc) = Some ko' \<and>
+        creply_relation ko ko'"
+  apply (frule obj_at_ko_at')
+  apply clarsimp
+  apply (frule cmap_relation_reply)
+  apply (drule (1) cmap_relation_ko_atD)
+  apply fastforce
+  done
+
 fun
   thread_state_to_tsType :: "thread_state \<Rightarrow> machine_word"
 where
@@ -1987,7 +1999,7 @@ lemma cap_get_tag_isCap_unfolded_H_cap:
   and "ccap_relation (capability.IRQHandlerCap v13) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_irq_handler_cap)"
   and "ccap_relation (capability.IRQControlCap) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_irq_control_cap)"
   and "ccap_relation (capability.Zombie v14 v15 v16) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_zombie_cap)"
-  and "ccap_relation (capability.ReplyCap v17 v18) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_reply_cap)"
+  and "ccap_relation (capability.ReplyCap v17) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_reply_cap)"
   and "ccap_relation (capability.UntypedCap v100 v19 v20 v20b) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_untyped_cap)"
   and "ccap_relation (capability.CNodeCap v21 v22 v23 v24) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_cnode_cap)"
   and "ccap_relation (capability.DomainCap) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_domain_cap)"

proof/crefine/RISCV64/StateRelation_C.thy

@@ -498,6 +498,7 @@ lemma refill_buffer_relation_size_eq:
 definition creply_relation :: "Structures_H.reply \<Rightarrow> reply_C \<Rightarrow> bool" where
   "creply_relation areply creply \<equiv>
        option_to_ptr (replyTCB areply) = replyTCB_C creply
+     \<and> from_bool (replyCanGrant areply) = canGrant_C creply
      \<and> option_to_ptr (replyPrev areply)
         = ((Ptr \<circ> callStackPtr_CL \<circ> call_stack_lift \<circ> replyPrev_C) creply :: reply_C ptr)
      \<and> isHead (replyNext areply) = to_bool ((isHead_CL \<circ> call_stack_lift \<circ> replyNext_C) creply)

proof/crefine/RISCV64/Syscall_C.thy

@@ -96,10 +96,9 @@ lemma performInvocation_Notification_ccorres:
 
 lemma performInvocation_Reply_ccorres:
   "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
-     (invs' and tcb_at' sender and reply_at' reply)
+     (invs' and tcb_at' sender and reply_at' reply and obj_at' (\<lambda>reply. replyCanGrant reply = grant) reply)
      (\<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr sender\<rbrace>
-      \<inter> \<lbrace>\<acute>reply = reply_Ptr reply\<rbrace>
-      \<inter> \<lbrace>\<acute>canGrant = from_bool grant\<rbrace>) []
+      \<inter> \<lbrace>\<acute>reply = reply_Ptr reply\<rbrace>) []
      (liftE (doReplyTransfer sender reply grant))
      (Call performInvocation_Reply_'proc)"
   apply cinit
@@ -109,7 +108,7 @@ lemma performInvocation_Reply_ccorres:
     apply wp
    apply simp
    apply (vcg exspec=doReplyTransfer_modifies)
-  apply (simp add: rf_sr_ksCurThread)
+  apply (fastforce dest: obj_at_cslift_reply simp: creply_relation_def typ_heap_simps)
   done
 
 lemma decodeInvocation_ccorres:

proof/crefine/RISCV64/Wellformed_C.thy

@@ -323,7 +323,7 @@ where
  | Cap_notification_cap ntfn \<Rightarrow>
     NotificationCap (capNtfnPtr_CL ntfn)(capNtfnBadge_CL ntfn)(to_bool(capNtfnCanSend_CL ntfn))
                      (to_bool(capNtfnCanReceive_CL ntfn))
- | Cap_reply_cap rc \<Rightarrow> ReplyCap (capReplyPtr_CL rc) (to_bool (capReplyCanGrant_CL rc))
+ | Cap_reply_cap rc \<Rightarrow> ReplyCap (capReplyPtr_CL rc)
  | Cap_sched_context_cap sc \<Rightarrow> SchedContextCap (capSCPtr_CL sc) (unat (capSCSizeBits_CL sc))
  | Cap_sched_control_cap sc \<Rightarrow> SchedControlCap
  | Cap_thread_cap tc \<Rightarrow>  ThreadCap(ctcb_ptr_to_tcb_ptr (Ptr (cap_thread_cap_CL.capTCBPtr_CL tc)))

proof/invariant-abstract/AInvs.thy

@@ -1017,7 +1017,8 @@ lemma receive_ipc_schact_is_rct_imp_ct_not_in_release_q:
   apply (wpsimp wp: complete_signal_schact_is_rct_imp_ct_not_in_release_q)
            apply ((wpsimp wp: hoare_vcg_imp_lift' thread_get_wp')+)[2]
          apply (wpsimp wp: thread_get_wp')
-                    apply (wpsimp wp: hoare_vcg_imp_lift')
+                     apply (wpsimp wp: hoare_vcg_imp_lift')
+                    apply wpsimp
                    apply wpsimp
                   apply (wpsimp wp: hoare_vcg_imp_lift')
                  apply (wpsimp wp: hoare_vcg_imp_lift')
@@ -1886,6 +1887,10 @@ lemma check_budget_restart_schact_is_rct_imp_ct_activatable[wp]:
   "check_budget_restart \<lbrace>\<lambda>s. schact_is_rct s \<longrightarrow> ct_in_state activatable s\<rbrace>"
   by (wpsimp simp: check_budget_restart_def)
 
+lemma update_reply_schact_is_rct_imp_ct_activatable[wp]:
+  "update_reply ptr f \<lbrace>\<lambda>s. schact_is_rct s \<longrightarrow> ct_in_state activatable s\<rbrace>"
+  by (wpsimp simp: update_reply_def set_object_def get_object_def obj_at_def pred_tcb_at_def ct_in_state_def)
+
 lemma receive_ipc_schact_is_rct_imp_ct_activatable[wp]:
   "receive_ipc thread cap is_blocking reply_cap
    \<lbrace>\<lambda>s :: det_state. schact_is_rct s \<longrightarrow> ct_in_state activatable s\<rbrace>"
@@ -1899,8 +1904,8 @@ lemma receive_ipc_schact_is_rct_imp_ct_activatable[wp]:
   apply (case_tac ep; clarsimp)
     apply (cases is_blocking; clarsimp)
      apply (rule bind_wp_fwd_skip, solves \<open>(wpsimp | wpsimp wp: hoare_vcg_imp_lift')+\<close>)+
-     apply (wpsimp wp: set_simple_ko_wp hoare_vcg_imp_lift')
-     apply (clarsimp simp: ct_in_state_def pred_tcb_at_def obj_at_def simple_obj_at_def)
+     apply (wpsimp wp: set_simple_ko_wp update_reply_wp update_sk_obj_ref_wp)
+     apply (fastforce simp: ct_in_state_def pred_tcb_at_def obj_at_def simple_obj_at_def)
     apply (wpsimp wp: set_simple_ko_wp hoare_vcg_imp_lift')
    apply (rule bind_wp_fwd_skip, solves \<open>(wpsimp | wpsimp wp: hoare_vcg_imp_lift')+\<close>)+
    apply (intro hoare_if)

proof/invariant-abstract/CSpaceInv_AI.thy

@@ -46,7 +46,7 @@ lemma is_valid_vtable_root_simps[simp]:
   "\<not> is_valid_vtable_root (CNodeCap cnode_ref sz guard)"
   "\<not> is_valid_vtable_root (EndpointCap ep_ref badge R)"
   "\<not> is_valid_vtable_root (NotificationCap ep_ref badge R)"
-  "\<not> is_valid_vtable_root (ReplyCap tcb_ref R)"
+  "\<not> is_valid_vtable_root (ReplyCap tcb_ref)"
   "\<not> is_valid_vtable_root (Zombie e f g)"
   "\<not> is_valid_vtable_root (NullCap)"
   "\<not> is_valid_vtable_root (DomainCap)"
@@ -365,7 +365,7 @@ where
  | cap.ThreadCap ref \<Rightarrow> cap.ThreadCap ref
  | cap.DomainCap \<Rightarrow> cap.DomainCap
  | cap.SchedContextCap ref n \<Rightarrow> cap.SchedContextCap ref n \<comment> \<open>?\<close>
- | cap.ReplyCap ref R \<Rightarrow> cap.ReplyCap ref UNIV
+ | cap.ReplyCap ref \<Rightarrow> cap.ReplyCap ref
  | cap.UntypedCap dev ref n f \<Rightarrow> cap.UntypedCap dev ref n 0
  | cap.ArchObjectCap acap \<Rightarrow> cap.ArchObjectCap (cap_master_arch_cap acap)
  | _ \<Rightarrow> cap"
@@ -398,8 +398,8 @@ lemma cap_master_cap_eqDs1:
      \<Longrightarrow> cap = cap.SchedContextCap ref n"
   "cap_master_cap cap = cap.SchedControlCap
      \<Longrightarrow> cap = cap.SchedControlCap"
-  "cap_master_cap cap = cap.ReplyCap ref rghts
-     \<Longrightarrow> rghts = UNIV \<and> (\<exists>rghts. cap = cap.ReplyCap ref rghts)"
+  "cap_master_cap cap = cap.ReplyCap ref
+     \<Longrightarrow> cap = cap.ReplyCap ref"
   by (clarsimp simp: cap_master_cap_def
               split: cap.split_asm)+
 
@@ -423,7 +423,7 @@ lemma cap_badge_simps [simp]:
  "cap_badge (cap.CNodeCap r bits guard)            = None"
  "cap_badge (cap.ThreadCap r)                      = None"
  "cap_badge (cap.DomainCap)                        = None"
- "cap_badge (cap.ReplyCap r rights)                = None"
+ "cap_badge (cap.ReplyCap r)                       = None"
  "cap_badge (cap.IRQControlCap)                    = None"
  "cap_badge (cap.SchedContextCap sc n)             = None"
  "cap_badge (cap.SchedControlCap)                  = None"
@@ -1250,37 +1250,6 @@ lemma set_cap_valid_pspace:
   apply (clarsimp elim!: cte_wp_at_weakenE | rule conjI)+
   done
 
-
-lemma set_object_idle [wp]:
-  "\<lbrace>valid_idle and
-     (\<lambda>s. \<exists>ko t t' sc n. ko_at ko p s \<and> (p \<noteq> idle_thread_ptr \<and> p \<noteq> idle_sc_ptr \<or>
-                   (ko = (TCB t) \<and> ko' = (TCB t') \<and>
-                    tcb_state t = tcb_state t' \<and>
-                    tcb_bound_notification t = tcb_bound_notification t' \<and>
-                    tcb_sched_context t = tcb_sched_context t' \<and>
-                    tcb_yield_to t = tcb_yield_to t' \<and>
-                    valid_arch_idle (tcb_iarch t')) \<or>
-                   (ko = (SchedContext sc n) \<and> ko' = (SchedContext sc n))))\<rbrace>
-   set_object p ko'
-   \<lbrace>\<lambda>rv. valid_idle\<rbrace>"
-  apply (wpsimp wp: set_object_wp_strong)
-  apply (auto simp: valid_idle_def pred_tcb_at_def obj_at_def)
-  done
-
-lemma set_object_fault_tcbs_valid_states[wp]:
-  "\<lbrace>\<lambda>s. fault_tcbs_valid_states s \<and>
-        (\<forall>t. ko' = TCB t
-             \<longrightarrow> (\<exists>t'. ko_at (TCB t') p s \<and>
-                       tcb_state t' = tcb_state t \<and>
-                       tcb_fault t' = tcb_fault t))\<rbrace>
-   set_object p ko'
-   \<lbrace>\<lambda>rv. fault_tcbs_valid_states\<rbrace>"
-  apply (wpsimp wp: set_object_wp_strong)
-  apply (clarsimp simp: fault_tcbs_valid_states_def pred_tcb_at_def obj_at_def)
-  apply (drule_tac x=p in spec)
-  apply clarsimp
-  done
-
 lemma set_cap_idle[wp]:
   "\<lbrace>\<lambda>s. valid_idle s\<rbrace>
    set_cap cap p

proof/invariant-abstract/CSpacePre_AI.thy

@@ -66,7 +66,7 @@ lemma masked_as_full_simps[simp]:
   "masked_as_full (cap.ArchObjectCap x) cap = (cap.ArchObjectCap x)"
   "masked_as_full (cap.CNodeCap r n g) cap = (cap.CNodeCap r n g)"
   "masked_as_full (cap.SchedContextCap r m) cap = (cap.SchedContextCap r m)"
-  "masked_as_full (cap.ReplyCap r R) cap = (cap.ReplyCap r R)"
+  "masked_as_full (cap.ReplyCap r) cap = (cap.ReplyCap r)"
   "masked_as_full cap.NullCap cap = cap.NullCap"
   "masked_as_full cap.DomainCap cap = cap.DomainCap"
   "masked_as_full (cap.ThreadCap r) cap = cap.ThreadCap r"
@@ -75,7 +75,7 @@ lemma masked_as_full_simps[simp]:
   "masked_as_full cap (cap.ArchObjectCap x) = cap"
   "masked_as_full cap (cap.CNodeCap r n g) = cap"
   "masked_as_full cap (cap.SchedContextCap r m) = cap"
-  "masked_as_full cap (cap.ReplyCap r R) = cap"
+  "masked_as_full cap (cap.ReplyCap r) = cap"
   "masked_as_full cap cap.NullCap = cap"
   "masked_as_full cap cap.DomainCap = cap"
   "masked_as_full cap (cap.ThreadCap r) = cap"

proof/invariant-abstract/CSpace_AI.thy

@@ -660,7 +660,7 @@ where
   | Structures_A.ThreadCap r \<Rightarrow> True
   | Structures_A.DomainCap \<Rightarrow> False
   | Structures_A.SchedContextCap r n \<Rightarrow> False
-  | Structures_A.ReplyCap r rights \<Rightarrow> False
+  | Structures_A.ReplyCap r \<Rightarrow> False
   | Structures_A.SchedControlCap \<Rightarrow> False
   | Structures_A.IRQControlCap \<Rightarrow> False
   | Structures_A.IRQHandlerCap irq \<Rightarrow> True
@@ -984,7 +984,7 @@ lemma cap_master_cap_simps:
   "cap_master_cap (cap.NullCap)           = cap.NullCap"
   "cap_master_cap (cap.DomainCap)         = cap.DomainCap"
   "cap_master_cap (cap.UntypedCap dev r n f)  = cap.UntypedCap dev r n 0"
-  "cap_master_cap (cap.ReplyCap r rights) = cap.ReplyCap r UNIV"
+  "cap_master_cap (cap.ReplyCap r)        = cap.ReplyCap r"
   "cap_master_cap (cap.IRQControlCap)     = cap.IRQControlCap"
   "cap_master_cap (cap.SchedContextCap r n) = cap.SchedContextCap r n"
   "cap_master_cap (cap.SchedControlCap)   = cap.SchedControlCap"
@@ -3056,15 +3056,6 @@ lemma non_arch_cap_asid_vptr_None:
   using assms by (cases cap; simp add: is_cap_simps cap_asid_def cap_asid_base_def cap_vptr_def)+
 end
 
-lemma weak_derived_Reply:
-  "weak_derived (cap.ReplyCap t R) c = (\<exists> R'. c = cap.ReplyCap t R')"
-  "weak_derived c (cap.ReplyCap t R) = (\<exists> R'. c = cap.ReplyCap t R')"
-  by (auto simp: weak_derived_def copy_of_def
-                 same_object_as_def is_cap_simps
-                 non_arch_cap_asid_vptr_None[simplified is_cap_simps]
-          split: if_split_asm cap.split_asm)
-
-
 lemmas (in CSpace_AI_weak_derived) weak_derived_replies =
   weak_derived_is_reply
   weak_derived_obj_ref_of

proof/invariant-abstract/DetSchedSchedule_AI.thy

@@ -7374,13 +7374,13 @@ lemma finalise_cap_cur_sc_chargeable:
                apply wpsimp
               apply wpsimp
              apply (wpsimp wp: cancel_all_ipc_cur_sc_chargeable split: if_split)
-             apply (wpsimp wp: cancel_all_signals_cur_sc_chargeable unbind_maybe_notification_invs split: if_split)
+            apply (wpsimp wp: cancel_all_signals_cur_sc_chargeable unbind_maybe_notification_invs split: if_split)
            apply (wpsimp wp: reply_remove_cur_sc_chargeable cancel_ipc_cur_sc_chargeable
                              gts_wp get_simple_ko_wp split: if_split)
-   apply (rename_tac r R s ntfn x st)
-   apply (subgoal_tac "st_tcb_at (ipc_queued_thread_state) x s")
-    apply (clarsimp simp: obj_at_kh_kheap_simps ct_in_state_kh_simp)
-   apply (intro conjI; intro allI impI; clarsimp simp: invs_def pred_map_simps)
+           apply (rename_tac r s ntfn x st)
+           apply (subgoal_tac "st_tcb_at (ipc_queued_thread_state) x s")
+            apply (clarsimp simp: obj_at_kh_kheap_simps ct_in_state_kh_simp)
+            apply (intro conjI; intro allI impI; clarsimp simp: invs_def pred_map_simps)
            apply (subgoal_tac "(r, TCBReply) \<in> state_refs_of s x")
             apply (clarsimp simp: pred_tcb_at_def obj_at_def state_refs_of_def get_refs_def2 tcb_st_refs_of_def
                                   pred_neg_def
@@ -15567,6 +15567,11 @@ crunch receive_ipc_preamble
   for released_if_bound[wp]: "released_if_bound_sc_tcb_at t"
   (ignore: thread_set update_sched_context wp: crunch_wps)
 
+lemma update_reply_valid_sched_pred[wp]:
+  "update_reply ptr f \<lbrace>valid_sched_pred_strong P\<rbrace>"
+  by (wpsimp wp: update_reply_wp
+           simp: fun_upd_def obj_at_kh_kheap_simps vs_all_heap_simps)
+
 (* Preconditions for the guts of receive_ipc, after the reply preamble *)
 abbreviation (input) receive_ipc_valid_sched_preconds ::
   "obj_ref \<Rightarrow> obj_ref \<Rightarrow> cap \<Rightarrow> obj_ref option \<Rightarrow> endpoint \<Rightarrow> ('state_ext state \<Rightarrow> bool) \<Rightarrow> 'state_ext state \<Rightarrow> bool"
@@ -15586,7 +15591,7 @@ abbreviation (input) receive_ipc_valid_sched_preconds ::
 lemma receive_ipc_blocked_valid_sched':
   assumes ep: "case ep of IdleEP \<Rightarrow> queue = [] | RecvEP q \<Rightarrow> queue = q | SendEP _ \<Rightarrow> False"
   shows "\<lbrace> receive_ipc_valid_sched_preconds t ep_ptr reply reply_opt ep invs \<rbrace>
-          receive_ipc_blocked is_blocking t ep_ptr reply_opt pl queue
+          receive_ipc_blocked is_blocking t ep_ptr ep_rights reply_opt pl queue
          \<lbrace> \<lambda>rv. valid_sched \<rbrace>"
   apply (cases reply_opt; clarsimp simp: receive_ipc_blocked_def)
    apply (wpsimp wp: set_thread_state_valid_sched)
@@ -15597,7 +15602,7 @@ lemma receive_ipc_blocked_valid_sched':
 
 lemma receive_ipc_idle_valid_sched:
   "\<lbrace> receive_ipc_valid_sched_preconds t ep_ptr reply reply_opt IdleEP invs \<rbrace>
-    receive_ipc_idle is_blocking t ep_ptr reply_opt pl
+    receive_ipc_idle is_blocking t ep_ptr ep_rights reply_opt pl
    \<lbrace> \<lambda>rv. valid_sched \<rbrace>"
   apply (rule hoare_weaken_pre, rule monadic_rewrite_refine_valid[where P''=\<top>])
   apply (rule monadic_rewrite_receive_ipc_idle)

proof/invariant-abstract/Detype_AI.thy

@@ -100,7 +100,7 @@ definition
   obj_reply_refs :: "cap \<Rightarrow> machine_word set"
 where
  "obj_reply_refs cap \<equiv> obj_refs cap \<union>
-   (case cap of cap.ReplyCap t R \<Rightarrow> {t} | _ \<Rightarrow> {})"
+   (case cap of cap.ReplyCap t \<Rightarrow> {t} | _ \<Rightarrow> {})"
 
 
 lemma ex_cte_cap_to_obj_ref_disj: