theory CNode_AC

lemma decode_cnode_inv_authorised:
  "\<lbrace>pas_refined aag and invs and valid_cap cap
                    and K (\<forall>c \<in> {cap} \<union> set excaps. pas_cap_cur_auth aag c)\<rbrace>
   decode_cnode_invocation label args cap excaps
   \<lbrace>\<lambda>rv s. authorised_cnode_inv aag rv s\<rbrace>,-" apply (simp add: authorised_cnode_inv_def decode_cnode_invocation_def
                   split_def whenE_def unlessE_def set_eq_iff
             cong: if_cong Invocations_A.cnode_invocation.case_cong split del: if_split) apply (wpsimp wp: hoare_vcg_all_lift hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R lsfco_cte_at
         | wp (once) get_cap_cur_auth)+ apply (subgoal_tac "\<forall>n. n < length excaps
                          \<longrightarrow> (is_cnode_cap (excaps ! n)
                               \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! n). is_subject aag x))") apply (fastforce simp: invs_valid_objs is_cnode_into_is_subject) apply (intro allI impI is_cnode_into_is_subject; fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and valid_cap cap and K (Ball ({cap} \<union> set excaps) (pas_cap_cur_auth aag))\<rbrace> decode_cnode_invocation label args cap excaps \<lbrace>authorised_cnode_inv aag\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and valid_cap cap and (\<lambda>y. pas_cap_cur_auth aag cap \<and> Ball (set excaps) (pas_cap_cur_auth aag))\<rbrace> doE y <- if gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] then returnOk () else throwError IllegalOperation;
y <- if length args < 2 then throwError TruncatedMessage else returnOk ();
dest_slot <- lookup_slot_for_cnode_op False cap (to_bl (args ! 0)) (data_to_nat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE y <- ensure_empty dest_slot;
src_slot <- lookup_slot_for_cnode_op True (excaps ! 0) (to_bl (drop 2 args ! 0)) (data_to_nat (drop 2 args ! Suc 0));
src_cap <- liftE (get_cap src_slot);
y <- if src_cap = NullCap then throwError (FailedLookup True (MissingCapability (data_to_nat (drop 2 args ! Suc 0)))) else returnOk ();
p <- case gen_invocation_type label of CNodeCopy \<Rightarrow> case snd (gen_invocation_type label, drop 2 (drop 2 args)) of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case snd (gen_invocation_type label, drop 2 (drop 2 args)) of [] \<Rightarrow> throwError TruncatedMessage | [rightsWord] \<Rightarrow> throwError TruncatedMessage | rightsWord # capData # xa \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | CNodeMove \<Rightarrow> returnOk (all_rights, None, True) | CNodeMutate \<Rightarrow> case snd (gen_invocation_type label, drop 2 (drop 2 args)) of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
new_cap <- (if snd (snd p) then returnOk else derive_cap src_slot) (case fst (snd p) of None \<Rightarrow> mask_cap (fst p) src_cap | Some w \<Rightarrow> update_cap_data (snd (snd p)) w (mask_cap (fst p) src_cap));
y <- if new_cap = NullCap then throwError IllegalOperation else returnOk ();
returnOk ((if snd (snd p) then MoveCall else InsertCall) new_cap src_slot dest_slot)
odE else if gen_invocation_type label = CNodeRevoke then returnOk (RevokeCall dest_slot) else if gen_invocation_type label = CNodeDelete then returnOk (DeleteCall dest_slot) else if gen_invocation_type label = CNodeSaveCaller then doE y <- ensure_empty dest_slot;
returnOk (SaveCall dest_slot)
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE (get_cap dest_slot);
y <- if has_cancel_send_rights cap then returnOk () else throwError IllegalOperation;
returnOk (CancelBadgedSendsCall cap)
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length args - 2 \<and> Suc 0 < length excaps then doE src_slot <- lookup_slot_for_cnode_op True (excaps ! Suc 0) (to_bl (drop 2 args ! 4)) (data_to_nat (drop 2 args ! 5));
pivot_slot <- lookup_slot_for_cnode_op True (excaps ! 0) (to_bl (drop 2 args ! Suc 0)) (data_to_nat (drop 2 args ! 2));
y <- if pivot_slot = src_slot \<or> pivot_slot = dest_slot then throwError IllegalOperation else returnOk ();
y <- if src_slot = dest_slot then returnOk () else ensure_empty dest_slot;
src_cap <- liftE (get_cap src_slot);
y <- if src_cap = NullCap then throwError (FailedLookup True (MissingCapability (data_to_nat (drop 2 args ! 5)))) else returnOk ();
pivot_cap <- liftE (get_cap pivot_slot);
y <- if pivot_cap = NullCap then throwError (FailedLookup False (MissingCapability (data_to_nat (drop 2 args ! 2)))) else returnOk ();
y <- if update_cap_data True (drop 2 args ! 3) src_cap = NullCap then throwError IllegalOperation else returnOk ();
y <- if update_cap_data True (drop 2 args ! 0) pivot_cap = NullCap then throwError IllegalOperation else returnOk ();
returnOk (RotateCall (update_cap_data True (drop 2 args ! 3) src_cap) (update_cap_data True (drop 2 args ! 0) pivot_cap) src_slot pivot_slot dest_slot)
odE else throwError TruncatedMessage
odE \<lbrace>\<lambda>rv s. case rv of InsertCall cap ptr ptr' \<Rightarrow> is_subject aag (fst ptr) \<and> is_subject aag (fst ptr') | MoveCall cap ptr ptr' \<Rightarrow> is_subject aag (fst ptr) \<and> is_subject aag (fst ptr') | RevokeCall ptr \<Rightarrow> is_subject aag (fst ptr) | DeleteCall ptr \<Rightarrow> is_subject aag (fst ptr) | RotateCall s_cap p_cap src pivot dest \<Rightarrow> is_subject aag (fst src) \<and> is_subject aag (fst pivot) \<and> is_subject aag (fst dest) | SaveCall ptr \<Rightarrow> is_subject aag (fst ptr) | CancelBadgedSendsCall x \<Rightarrow> pas_cap_cur_auth aag x\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pas_refined aag s; invs s; s \<turnstile> cap; pas_cap_cur_auth aag cap; Ball (set excaps) (pas_cap_cur_auth aag)\<rbrakk> \<Longrightarrow> (2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<longrightarrow> (gen_invocation_type label = CNodeCopy \<longrightarrow> (\<exists>x xa. drop 4 args = x # xa) \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeCopy \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> (\<forall>x xa. (drop 4 args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> length args < 2 \<longrightarrow> CNodeMint \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))) \<and> (drop 4 args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeMint \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))) \<and> (drop 4 args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> length args < 2 \<longrightarrow> CNodeMint \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))) \<and> (drop 4 args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeMint \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))))) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeMove \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> (\<exists>x xa. drop 4 args = x # xa) \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeMutate \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x)))) \<and> ((2 \<le> length args - 2 \<longrightarrow> excaps = [] \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]) \<longrightarrow> (gen_invocation_type label = CNodeRevoke \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeRevoke \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x)) \<and> (gen_invocation_type label \<noteq> CNodeRevoke \<longrightarrow> (gen_invocation_type label = CNodeDelete \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeDelete \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x)) \<and> (gen_invocation_type label \<noteq> CNodeDelete \<longrightarrow> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeSaveCaller \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x)) \<and> (gen_invocation_type label \<noteq> CNodeSaveCaller \<longrightarrow> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeCancelBadgedSends \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> valid_objs s \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))) \<and> (gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<longrightarrow> gen_invocation_type label = CNodeRotate \<and> 5 < length args - 2 \<and> Suc 0 < length excaps \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeRotate \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> (is_cnode_cap (excaps ! Suc 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! Suc 0). is_subject aag x)) \<and> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))))))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pas_refined aag s; invs s; s \<turnstile> cap; pas_cap_cur_auth aag cap; Ball (set excaps) (pas_cap_cur_auth aag); \<forall>n<length excaps. is_cnode_cap (excaps ! n) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! n). is_subject aag x)\<rbrakk> \<Longrightarrow> (2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<longrightarrow> (gen_invocation_type label = CNodeCopy \<longrightarrow> (\<exists>x xa. drop 4 args = x # xa) \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeCopy \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> (\<forall>x xa. (drop 4 args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> length args < 2 \<longrightarrow> CNodeMint \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))) \<and> (drop 4 args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeMint \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))) \<and> (drop 4 args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> length args < 2 \<longrightarrow> CNodeMint \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))) \<and> (drop 4 args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeMint \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))))) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeMove \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> (\<exists>x xa. drop 4 args = x # xa) \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeMutate \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x)))) \<and> ((2 \<le> length args - 2 \<longrightarrow> excaps = [] \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]) \<longrightarrow> (gen_invocation_type label = CNodeRevoke \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeRevoke \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x)) \<and> (gen_invocation_type label \<noteq> CNodeRevoke \<longrightarrow> (gen_invocation_type label = CNodeDelete \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeDelete \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x)) \<and> (gen_invocation_type label \<noteq> CNodeDelete \<longrightarrow> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeSaveCaller \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x)) \<and> (gen_invocation_type label \<noteq> CNodeSaveCaller \<longrightarrow> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeCancelBadgedSends \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> valid_objs s \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))) \<and> (gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<longrightarrow> gen_invocation_type label = CNodeRotate \<and> 5 < length args - 2 \<and> Suc 0 < length excaps \<longrightarrow> \<not> length args < 2 \<longrightarrow> CNodeRotate \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> (is_cnode_cap (excaps ! Suc 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! Suc 0). is_subject aag x)) \<and> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x)))))))
 2. \<And>s. \<lbrakk>pas_refined aag s; invs s; s \<turnstile> cap; pas_cap_cur_auth aag cap; Ball (set excaps) (pas_cap_cur_auth aag)\<rbrakk> \<Longrightarrow> \<forall>n<length excaps. is_cnode_cap (excaps ! n) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! n). is_subject aag x) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pas_refined aag s; invs s; s \<turnstile> cap; pas_cap_cur_auth aag cap; Ball (set excaps) (pas_cap_cur_auth aag)\<rbrakk> \<Longrightarrow> \<forall>n<length excaps. is_cnode_cap (excaps ! n) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! n). is_subject aag x) proof (prove)
goal:
No subgoals!