theory Dpolicy

lemma cap_auth_conferred_transform:
  "cap_auth_conferred cap = cdl_cap_auth_conferred (transform_cap cap)" apply (case_tac cap;
         clarsimp simp: cap_auth_conferred_def arch_cap_auth_conferred_def
                        cdl_cap_auth_conferred_def reply_cap_rights_to_auth_def) apply (rename_tac arch_cap) apply (case_tac arch_cap; clarsimp simp: is_page_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_auth_conferred cap = cdl_cap_auth_conferred (transform_cap cap) proof (prove)
goal (1 subgoal):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> (is_page_cap x12 \<longrightarrow> vspace_cap_rights_to_auth (acap_rights x12) = (case transform_cap (ArchObjectCap x12) of cdl_cap.NullCap \<Rightarrow> {} | cdl_cap.EndpointCap oref badge r \<Rightarrow> cap_rights_to_auth r True | cdl_cap.NotificationCap oref badge r \<Rightarrow> cap_rights_to_auth (r - {AllowGrant, AllowGrantReply}) False | cdl_cap.ReplyCap oref r \<Rightarrow> reply_cap_rights_to_auth False r | MasterReplyCap oref \<Rightarrow> UNIV | PendingSyncSendCap oref badge call grant grant_reply fault \<Rightarrow> {SyncSend} \<union> (if grant then {auth.Grant, Call} else {}) \<union> (if grant_reply then {Call} else {}) | PendingSyncRecvCap oref fault grant \<Rightarrow> (if fault then {} else {Receive}) \<union> (if grant then {auth.Grant} else {}) | PendingNtfnRecvCap oref \<Rightarrow> {Receive} | RestartCap \<Rightarrow> {} | RunningCap \<Rightarrow> {} | FrameCap dev oref r sz is_real asid \<Rightarrow> vspace_cap_rights_to_auth r | IOPortsCap worda set \<Rightarrow> {} | IOSpaceMasterCap \<Rightarrow> {} | IOSpaceCap worda \<Rightarrow> {} | IOPageTableCap worda \<Rightarrow> {} | BoundNotificationCap word \<Rightarrow> {Receive, Reset} | _ \<Rightarrow> {Control})) \<and> (\<not> is_page_cap x12 \<longrightarrow> {Control} = (case transform_cap (ArchObjectCap x12) of cdl_cap.NullCap \<Rightarrow> {} | cdl_cap.EndpointCap oref badge r \<Rightarrow> cap_rights_to_auth r True | cdl_cap.NotificationCap oref badge r \<Rightarrow> cap_rights_to_auth (r - {AllowGrant, AllowGrantReply}) False | cdl_cap.ReplyCap oref r \<Rightarrow> reply_cap_rights_to_auth False r | MasterReplyCap oref \<Rightarrow> UNIV | PendingSyncSendCap oref badge call grant grant_reply fault \<Rightarrow> {SyncSend} \<union> (if grant then {auth.Grant, Call} else {}) \<union> (if grant_reply then {Call} else {}) | PendingSyncRecvCap oref fault grant \<Rightarrow> (if fault then {} else {Receive}) \<union> (if grant then {auth.Grant} else {}) | PendingNtfnRecvCap oref \<Rightarrow> {Receive} | RestartCap \<Rightarrow> {} | RunningCap \<Rightarrow> {} | FrameCap dev oref r sz is_real asid \<Rightarrow> vspace_cap_rights_to_auth r | IOPortsCap worda set \<Rightarrow> {} | IOSpaceMasterCap \<Rightarrow> {} | IOSpaceCap worda \<Rightarrow> {} | IOPageTableCap worda \<Rightarrow> {} | BoundNotificationCap word \<Rightarrow> {Receive, Reset} | _ \<Rightarrow> {Control})) proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap. cap = ArchObjectCap arch_cap \<Longrightarrow> (is_page_cap arch_cap \<longrightarrow> vspace_cap_rights_to_auth (acap_rights arch_cap) = (case transform_cap (ArchObjectCap arch_cap) of cdl_cap.NullCap \<Rightarrow> {} | cdl_cap.EndpointCap oref badge r \<Rightarrow> cap_rights_to_auth r True | cdl_cap.NotificationCap oref badge r \<Rightarrow> cap_rights_to_auth (r - {AllowGrant, AllowGrantReply}) False | cdl_cap.ReplyCap oref r \<Rightarrow> reply_cap_rights_to_auth False r | MasterReplyCap oref \<Rightarrow> UNIV | PendingSyncSendCap oref badge call grant grant_reply fault \<Rightarrow> {SyncSend} \<union> (if grant then {auth.Grant, Call} else {}) \<union> (if grant_reply then {Call} else {}) | PendingSyncRecvCap oref fault grant \<Rightarrow> (if fault then {} else {Receive}) \<union> (if grant then {auth.Grant} else {}) | PendingNtfnRecvCap oref \<Rightarrow> {Receive} | RestartCap \<Rightarrow> {} | RunningCap \<Rightarrow> {} | FrameCap dev oref r sz is_real asid \<Rightarrow> vspace_cap_rights_to_auth r | IOPortsCap worda set \<Rightarrow> {} | IOSpaceMasterCap \<Rightarrow> {} | IOSpaceCap worda \<Rightarrow> {} | IOPageTableCap worda \<Rightarrow> {} | BoundNotificationCap word \<Rightarrow> {Receive, Reset} | _ \<Rightarrow> {Control})) \<and> (\<not> is_page_cap arch_cap \<longrightarrow> {Control} = (case transform_cap (ArchObjectCap arch_cap) of cdl_cap.NullCap \<Rightarrow> {} | cdl_cap.EndpointCap oref badge r \<Rightarrow> cap_rights_to_auth r True | cdl_cap.NotificationCap oref badge r \<Rightarrow> cap_rights_to_auth (r - {AllowGrant, AllowGrantReply}) False | cdl_cap.ReplyCap oref r \<Rightarrow> reply_cap_rights_to_auth False r | MasterReplyCap oref \<Rightarrow> UNIV | PendingSyncSendCap oref badge call grant grant_reply fault \<Rightarrow> {SyncSend} \<union> (if grant then {auth.Grant, Call} else {}) \<union> (if grant_reply then {Call} else {}) | PendingSyncRecvCap oref fault grant \<Rightarrow> (if fault then {} else {Receive}) \<union> (if grant then {auth.Grant} else {}) | PendingNtfnRecvCap oref \<Rightarrow> {Receive} | RestartCap \<Rightarrow> {} | RunningCap \<Rightarrow> {} | FrameCap dev oref r sz is_real asid \<Rightarrow> vspace_cap_rights_to_auth r | IOPortsCap worda set \<Rightarrow> {} | IOSpaceMasterCap \<Rightarrow> {} | IOSpaceCap worda \<Rightarrow> {} | IOPageTableCap worda \<Rightarrow> {} | BoundNotificationCap word \<Rightarrow> {Receive, Reset} | _ \<Rightarrow> {Control})) proof (prove)
goal:
No subgoals!