theory Ipc_AC

lemma remove_rights_cap_auth_conferred_subset:
  "x \<in> cap_auth_conferred (remove_rights R cap) \<Longrightarrow> x \<in> cap_auth_conferred cap" unfolding remove_rights_def cap_rights_update_def apply (clarsimp split: if_split_asm cap.splits bool.splits
                   simp: cap_auth_conferred_def
                         validate_vm_rights_def vm_read_only_def vm_kernel_only_def) apply (erule set_mp [OF cap_rights_to_auth_mono, rotated], clarsimp)+ apply (fastforce simp: cap_rights_to_auth_def reply_cap_rights_to_auth_def) apply (simp add: Diff_eq) apply (erule set_rev_mp[OF _ acap_auth_conferred_acap_rights_update]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> cap_auth_conferred (remove_rights R cap) \<Longrightarrow> x \<in> cap_auth_conferred cap proof (prove)
goal (1 subgoal):
 1. x \<in> cap_auth_conferred (case cap of EndpointCap oref badge cr \<Rightarrow> EndpointCap oref badge (cap_rights cap - R) | NotificationCap oref badge cr \<Rightarrow> NotificationCap oref badge (cap_rights cap - R - {AllowGrant, AllowGrantReply}) | ReplyCap t m cr \<Rightarrow> ReplyCap t m (cap_rights cap - R - {AllowRead, AllowGrantReply} \<union> {AllowWrite}) | ArchObjectCap acap \<Rightarrow> ArchObjectCap (acap_rights_update (cap_rights cap - R) acap) | _ \<Rightarrow> cap) \<Longrightarrow> x \<in> cap_auth_conferred cap proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 x33a. \<lbrakk>x \<in> cap_rights_to_auth (x33a - R) True; cap = EndpointCap x31 x32 x33a\<rbrakk> \<Longrightarrow> x \<in> cap_rights_to_auth x33a True
 2. \<And>x41 x42 x43a. \<lbrakk>x \<in> cap_rights_to_auth (x43a - R - {AllowGrant, AllowGrantReply}) False; cap = NotificationCap x41 x42 x43a\<rbrakk> \<Longrightarrow> x \<in> cap_rights_to_auth (x43a - {AllowGrant, AllowGrantReply}) False
 3. \<And>x51 x52 x53a. \<lbrakk>x \<in> reply_cap_rights_to_auth x52 (insert AllowWrite (x53a - R - {AllowRead, AllowGrantReply})); cap = ReplyCap x51 x52 x53a\<rbrakk> \<Longrightarrow> x \<in> reply_cap_rights_to_auth x52 x53a
 4. \<And>x12a. \<lbrakk>x \<in> arch_cap_auth_conferred (acap_rights_update (acap_rights x12a - R) x12a); cap = ArchObjectCap x12a\<rbrakk> \<Longrightarrow> x \<in> arch_cap_auth_conferred x12a proof (prove)
goal (2 subgoals):
 1. \<And>x51 x52 x53a. \<lbrakk>x \<in> reply_cap_rights_to_auth x52 (insert AllowWrite (x53a - R - {AllowRead, AllowGrantReply})); cap = ReplyCap x51 x52 x53a\<rbrakk> \<Longrightarrow> x \<in> reply_cap_rights_to_auth x52 x53a
 2. \<And>x12a. \<lbrakk>x \<in> arch_cap_auth_conferred (acap_rights_update (acap_rights x12a - R) x12a); cap = ArchObjectCap x12a\<rbrakk> \<Longrightarrow> x \<in> arch_cap_auth_conferred x12a proof (prove)
goal (1 subgoal):
 1. \<And>x12a. \<lbrakk>x \<in> arch_cap_auth_conferred (acap_rights_update (acap_rights x12a - R) x12a); cap = ArchObjectCap x12a\<rbrakk> \<Longrightarrow> x \<in> arch_cap_auth_conferred x12a proof (prove)
goal (1 subgoal):
 1. \<And>x12a. \<lbrakk>x \<in> arch_cap_auth_conferred (acap_rights_update (acap_rights x12a \<inter> - R) x12a); cap = ArchObjectCap x12a\<rbrakk> \<Longrightarrow> x \<in> arch_cap_auth_conferred x12a proof (prove)
goal:
No subgoals!