theory Invoke_C

lemma hasCancelSendRights_spec:
  "\<forall>cap. \<Gamma> \<turnstile> \<lbrace> ccap_relation cap \<acute>cap \<rbrace>
             Call hasCancelSendRights_'proc
             \<lbrace> \<acute>ret__unsigned_long = from_bool (hasCancelSendRights cap) \<rbrace>" apply vcg apply (clarsimp simp: if_1_0_0) apply (rule conjI) apply clarsimp apply (drule sym, drule (1) cap_get_tag_to_H) apply (clarsimp simp: hasCancelSendRights_def to_bool_def
                   split: if_split bool.splits) apply (rule impI) apply (case_tac cap,
         auto simp: cap_get_tag_isCap_unfolded_H_cap cap_tag_defs hasCancelSendRights_def
              dest: cap_get_tag_isArchCap_unfolded_H_cap
              split: capability.splits bool.splits)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>cap. \<Gamma>\<turnstile> \<lbrace>ccap_relation cap \<acute>cap\<rbrace> Call hasCancelSendRights_'proc \<lbrace>\<acute>ret__unsigned_long = from_bool (hasCancelSendRights cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap capa. ccap_relation cap capa \<Longrightarrow> \<forall>ret__unsigned. ret__unsigned = cap_get_tag capa \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap = cap_get_tag capa \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capCanSend_CL (cap_endpoint_cap_lift capa) \<longrightarrow> ((if capCanSend_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capCanReceive_CL (cap_endpoint_cap_lift capa) \<longrightarrow> ((if capCanReceive_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capCanGrantReply_CL (cap_endpoint_cap_lift capa) \<longrightarrow> ((if capCanGrantReply_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capCanGrant_CL (cap_endpoint_cap_lift capa) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) (if capCanGrant_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then 1 else 0) = from_bool (hasCancelSendRights cap))) \<and> ((if capCanGrantReply_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0 = from_bool (hasCancelSendRights cap)))) \<and> ((if capCanReceive_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0 = from_bool (hasCancelSendRights cap)))) \<and> ((if capCanSend_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0 = from_bool (hasCancelSendRights cap)))) \<and> (SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<noteq> cap_get_tag capa \<longrightarrow> SCAST(32 signed \<rightarrow> 32) false = from_bool (hasCancelSendRights cap)) proof (prove)
goal (1 subgoal):
 1. \<And>cap capa. ccap_relation cap capa \<Longrightarrow> (SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap = cap_get_tag capa \<longrightarrow> (capCanSend_CL (cap_endpoint_cap_lift capa) \<noteq> 0 \<longrightarrow> (capCanReceive_CL (cap_endpoint_cap_lift capa) \<noteq> 0 \<longrightarrow> (capCanGrantReply_CL (cap_endpoint_cap_lift capa) \<noteq> 0 \<longrightarrow> (if capCanGrant_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (hasCancelSendRights cap)) \<and> (capCanGrantReply_CL (cap_endpoint_cap_lift capa) = 0 \<longrightarrow> from_bool (hasCancelSendRights cap) = 0)) \<and> (capCanReceive_CL (cap_endpoint_cap_lift capa) = 0 \<longrightarrow> from_bool (hasCancelSendRights cap) = 0)) \<and> (capCanSend_CL (cap_endpoint_cap_lift capa) = 0 \<longrightarrow> from_bool (hasCancelSendRights cap) = 0)) \<and> (SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<noteq> cap_get_tag capa \<longrightarrow> \<not> hasCancelSendRights cap) proof (prove)
goal (2 subgoals):
 1. \<And>cap capa. ccap_relation cap capa \<Longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap = cap_get_tag capa \<longrightarrow> (capCanSend_CL (cap_endpoint_cap_lift capa) \<noteq> 0 \<longrightarrow> (capCanReceive_CL (cap_endpoint_cap_lift capa) \<noteq> 0 \<longrightarrow> (capCanGrantReply_CL (cap_endpoint_cap_lift capa) \<noteq> 0 \<longrightarrow> (if capCanGrant_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (hasCancelSendRights cap)) \<and> (capCanGrantReply_CL (cap_endpoint_cap_lift capa) = 0 \<longrightarrow> from_bool (hasCancelSendRights cap) = 0)) \<and> (capCanReceive_CL (cap_endpoint_cap_lift capa) = 0 \<longrightarrow> from_bool (hasCancelSendRights cap) = 0)) \<and> (capCanSend_CL (cap_endpoint_cap_lift capa) = 0 \<longrightarrow> from_bool (hasCancelSendRights cap) = 0)
 2. \<And>cap capa. ccap_relation cap capa \<Longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<noteq> cap_get_tag capa \<longrightarrow> \<not> hasCancelSendRights cap proof (prove)
goal (2 subgoals):
 1. \<And>cap capa. \<lbrakk>ccap_relation cap capa; SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap = cap_get_tag capa\<rbrakk> \<Longrightarrow> (capCanSend_CL (cap_endpoint_cap_lift capa) \<noteq> 0 \<longrightarrow> (capCanReceive_CL (cap_endpoint_cap_lift capa) \<noteq> 0 \<longrightarrow> (capCanGrantReply_CL (cap_endpoint_cap_lift capa) \<noteq> 0 \<longrightarrow> (if capCanGrant_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (hasCancelSendRights cap)) \<and> (capCanGrantReply_CL (cap_endpoint_cap_lift capa) = 0 \<longrightarrow> from_bool (hasCancelSendRights cap) = 0)) \<and> (capCanReceive_CL (cap_endpoint_cap_lift capa) = 0 \<longrightarrow> from_bool (hasCancelSendRights cap) = 0)) \<and> (capCanSend_CL (cap_endpoint_cap_lift capa) = 0 \<longrightarrow> from_bool (hasCancelSendRights cap) = 0)
 2. \<And>cap capa. ccap_relation cap capa \<Longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<noteq> cap_get_tag capa \<longrightarrow> \<not> hasCancelSendRights cap proof (prove)
goal (2 subgoals):
 1. \<And>cap capa. \<lbrakk>cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))\<rbrakk> \<Longrightarrow> (capCanSend_CL (cap_endpoint_cap_lift capa) \<noteq> 0 \<longrightarrow> (capCanReceive_CL (cap_endpoint_cap_lift capa) \<noteq> 0 \<longrightarrow> (capCanGrantReply_CL (cap_endpoint_cap_lift capa) \<noteq> 0 \<longrightarrow> (if capCanGrant_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (hasCancelSendRights cap)) \<and> (capCanGrantReply_CL (cap_endpoint_cap_lift capa) = 0 \<longrightarrow> from_bool (hasCancelSendRights cap) = 0)) \<and> (capCanReceive_CL (cap_endpoint_cap_lift capa) = 0 \<longrightarrow> from_bool (hasCancelSendRights cap) = 0)) \<and> (capCanSend_CL (cap_endpoint_cap_lift capa) = 0 \<longrightarrow> from_bool (hasCancelSendRights cap) = 0)
 2. \<And>cap capa. ccap_relation cap capa \<Longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<noteq> cap_get_tag capa \<longrightarrow> \<not> hasCancelSendRights cap proof (prove)
goal (1 subgoal):
 1. \<And>cap capa. ccap_relation cap capa \<Longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<noteq> cap_get_tag capa \<longrightarrow> \<not> hasCancelSendRights cap proof (prove)
goal (1 subgoal):
 1. \<And>cap capa. \<lbrakk>ccap_relation cap capa; SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<noteq> cap_get_tag capa\<rbrakk> \<Longrightarrow> \<not> hasCancelSendRights cap proof (prove)
goal:
No subgoals!