theory ArchBCorres2_AI

lemma decode_cnode_invocation[wp]: "bcorres (decode_cnode_invocation a b c d) (decode_cnode_invocation a b c d)" apply (simp add: decode_cnode_invocation_def) apply (wp | wpc | simp add: split_def | intro impI conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (decode_cnode_invocation a b c d) (decode_cnode_invocation a b c d) proof (prove)
goal (1 subgoal):
 1. bcorres (doE y <- unlessE (gen_invocation_type a \<in> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length b < 2) (throwError TruncatedMessage);
dest_slot <- lookup_slot_for_cnode_op False c (to_bl (b ! 0)) (unat (b ! Suc 0));
if 2 \<le> length b - 2 \<and> d \<noteq> [] \<and> gen_invocation_type a \<in> set [CNodeCopy .e. CNodeMutate] then doE y <- ensure_empty dest_slot;
src_slot <- lookup_slot_for_cnode_op True (d ! 0) (to_bl (drop 2 b ! 0)) (unat (drop 2 b ! Suc 0));
src_cap <- liftE (get_cap src_slot);
y <- whenE (src_cap = NullCap) (throwError (FailedLookup True (MissingCapability (unat (drop 2 b ! Suc 0)))));
(rights, cap_data, is_move) <- case gen_invocation_type a of CNodeCopy \<Rightarrow> case drop 2 (drop 2 b) of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case drop 2 (drop 2 b) 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 drop 2 (drop 2 b) of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
new_cap <- (if is_move then returnOk else derive_cap src_slot) (case cap_data of None \<Rightarrow> mask_cap rights src_cap | Some w \<Rightarrow> update_cap_data is_move w (mask_cap rights src_cap));
y <- whenE (new_cap = NullCap) (throwError IllegalOperation);
returnOk ((if is_move then MoveCall else InsertCall) new_cap src_slot dest_slot)
odE else if gen_invocation_type a = CNodeRevoke then returnOk (RevokeCall dest_slot) else if gen_invocation_type a = CNodeDelete then returnOk (DeleteCall dest_slot) else if gen_invocation_type a = CNodeSaveCaller then doE y <- ensure_empty dest_slot;
returnOk (SaveCall dest_slot)
odE else if gen_invocation_type a = CNodeCancelBadgedSends then doE cap <- liftE (get_cap dest_slot);
y <- unlessE (has_cancel_send_rights cap) (throwError IllegalOperation);
returnOk (CancelBadgedSendsCall cap)
odE else if gen_invocation_type a = CNodeRotate \<and> 5 < length b - 2 \<and> Suc 0 < length d then doE src_slot <- lookup_slot_for_cnode_op True (d ! Suc 0) (to_bl (drop 2 b ! 4)) (unat (drop 2 b ! 5));
pivot_slot <- lookup_slot_for_cnode_op True (d ! 0) (to_bl (drop 2 b ! Suc 0)) (unat (drop 2 b ! 2));
y <- whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) (throwError IllegalOperation);
y <- unlessE (src_slot = dest_slot) (ensure_empty dest_slot);
src_cap <- liftE (get_cap src_slot);
y <- whenE (src_cap = NullCap) (throwError (FailedLookup True (MissingCapability (unat (drop 2 b ! 5)))));
pivot_cap <- liftE (get_cap pivot_slot);
y <- whenE (pivot_cap = NullCap) (throwError (FailedLookup False (MissingCapability (unat (drop 2 b ! 2)))));
y <- whenE (update_cap_data True (drop 2 b ! 3) src_cap = NullCap) (throwError IllegalOperation);
y <- whenE (update_cap_data True (drop 2 b ! 0) pivot_cap = NullCap) (throwError IllegalOperation);
returnOk (RotateCall (update_cap_data True (drop 2 b ! 3) src_cap) (update_cap_data True (drop 2 b ! 0) pivot_cap) src_slot pivot_slot dest_slot)
odE else throwError TruncatedMessage
odE) (doE y <- unlessE (gen_invocation_type a \<in> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length b < 2) (throwError TruncatedMessage);
dest_slot <- lookup_slot_for_cnode_op False c (to_bl (b ! 0)) (unat (b ! Suc 0));
if 2 \<le> length b - 2 \<and> d \<noteq> [] \<and> gen_invocation_type a \<in> set [CNodeCopy .e. CNodeMutate] then doE y <- ensure_empty dest_slot;
src_slot <- lookup_slot_for_cnode_op True (d ! 0) (to_bl (drop 2 b ! 0)) (unat (drop 2 b ! Suc 0));
src_cap <- liftE (get_cap src_slot);
y <- whenE (src_cap = NullCap) (throwError (FailedLookup True (MissingCapability (unat (drop 2 b ! Suc 0)))));
(rights, cap_data, is_move) <- case gen_invocation_type a of CNodeCopy \<Rightarrow> case drop 2 (drop 2 b) of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case drop 2 (drop 2 b) 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 drop 2 (drop 2 b) of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
new_cap <- (if is_move then returnOk else derive_cap src_slot) (case cap_data of None \<Rightarrow> mask_cap rights src_cap | Some w \<Rightarrow> update_cap_data is_move w (mask_cap rights src_cap));
y <- whenE (new_cap = NullCap) (throwError IllegalOperation);
returnOk ((if is_move then MoveCall else InsertCall) new_cap src_slot dest_slot)
odE else if gen_invocation_type a = CNodeRevoke then returnOk (RevokeCall dest_slot) else if gen_invocation_type a = CNodeDelete then returnOk (DeleteCall dest_slot) else if gen_invocation_type a = CNodeSaveCaller then doE y <- ensure_empty dest_slot;
returnOk (SaveCall dest_slot)
odE else if gen_invocation_type a = CNodeCancelBadgedSends then doE cap <- liftE (get_cap dest_slot);
y <- unlessE (has_cancel_send_rights cap) (throwError IllegalOperation);
returnOk (CancelBadgedSendsCall cap)
odE else if gen_invocation_type a = CNodeRotate \<and> 5 < length b - 2 \<and> Suc 0 < length d then doE src_slot <- lookup_slot_for_cnode_op True (d ! Suc 0) (to_bl (drop 2 b ! 4)) (unat (drop 2 b ! 5));
pivot_slot <- lookup_slot_for_cnode_op True (d ! 0) (to_bl (drop 2 b ! Suc 0)) (unat (drop 2 b ! 2));
y <- whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) (throwError IllegalOperation);
y <- unlessE (src_slot = dest_slot) (ensure_empty dest_slot);
src_cap <- liftE (get_cap src_slot);
y <- whenE (src_cap = NullCap) (throwError (FailedLookup True (MissingCapability (unat (drop 2 b ! 5)))));
pivot_cap <- liftE (get_cap pivot_slot);
y <- whenE (pivot_cap = NullCap) (throwError (FailedLookup False (MissingCapability (unat (drop 2 b ! 2)))));
y <- whenE (update_cap_data True (drop 2 b ! 3) src_cap = NullCap) (throwError IllegalOperation);
y <- whenE (update_cap_data True (drop 2 b ! 0) pivot_cap = NullCap) (throwError IllegalOperation);
returnOk (RotateCall (update_cap_data True (drop 2 b ! 3) src_cap) (update_cap_data True (drop 2 b ! 0) pivot_cap) src_slot pivot_slot dest_slot)
odE else throwError TruncatedMessage
odE) proof (prove)
goal:
No subgoals!