theory Ipc_AI

lemma setup_caller_cap_valid_arch [wp]:
  "\<lbrace>valid_arch_state\<rbrace> setup_caller_cap st rt grant \<lbrace>\<lambda>_. valid_arch_state\<rbrace>" apply (rule valid_arch_state_lift_aobj_at; wp?) unfolding setup_caller_cap_def cap_insert_def update_cdt_def set_cdt_def set_untyped_cap_as_full_def apply simp apply (intro conjI impI) apply (wpsimp wp: set_cap.aobj_at get_cap_wp hoare_drop_imps sts.aobj_at)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<rbrace> setup_caller_cap st rt grant \<lbrace>\<lambda>_. valid_arch_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P P' pd. arch_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> setup_caller_cap st rt grant \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P P' pd. arch_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> do set_thread_state st BlockedOnReply;
src_cap <- get_cap (st, tcb_cnode_index 2);
dest_original <- return $ is_cap_revocable (ReplyCap st False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) src_cap;
old_cap <- get_cap (rt, tcb_cnode_index 3);
assert (old_cap = NullCap);
if is_untyped_cap src_cap \<and> is_untyped_cap (ReplyCap st False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) \<and> obj_ref_of src_cap = obj_ref_of (ReplyCap st False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) \<and> cap_bits_untyped src_cap = cap_bits_untyped (ReplyCap st False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) then set_cap (max_free_index_update src_cap) (st, tcb_cnode_index 2) else return ();
set_cap (ReplyCap st False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (rt, tcb_cnode_index 3);
is_original <- gets is_original_cap;
src_parent <- return $ should_be_parent_of src_cap (is_original (st, tcb_cnode_index 2)) (ReplyCap st False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) dest_original;
src_p <- gets (\<lambda>s. cdt s (st, tcb_cnode_index 2));
dest_p <- gets (\<lambda>s. cdt s (rt, tcb_cnode_index 3));
do t <- gets cdt;
s <- get;
put $ s\<lparr>cdt := t((rt, tcb_cnode_index 3) := if src_parent then Some (st, tcb_cnode_index 2) else t (st, tcb_cnode_index 2))\<rparr>
od;
do_extended_op (cap_insert_ext src_parent (st, tcb_cnode_index 2) (rt, tcb_cnode_index 3) src_p dest_p);
set_original (rt, tcb_cnode_index 3) dest_original
od \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P P' pd. arch_obj_pred P' \<Longrightarrow> (grant \<longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> do y <- set_thread_state st BlockedOnReply;
src_cap <- get_cap (st, tcb_cnode_index 2);
old_cap <- get_cap (rt, tcb_cnode_index 3);
y <- assert (old_cap = NullCap);
y <- set_cap (ReplyCap st False {AllowGrant, AllowWrite}) (rt, tcb_cnode_index 3);
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s (st, tcb_cnode_index 2));
dest_p <- gets (\<lambda>s. cdt s (rt, tcb_cnode_index 3));
y <- do t <- gets cdt;
s <- get;
put (s\<lparr>cdt := t((rt, tcb_cnode_index 3) := if should_be_parent_of src_cap (is_original (st, tcb_cnode_index 2)) (ReplyCap st False {AllowGrant, AllowWrite}) (is_cap_revocable (ReplyCap st False {AllowGrant, AllowWrite}) src_cap) then Some (st, tcb_cnode_index 2) else t (st, tcb_cnode_index 2))\<rparr>)
od;
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original (st, tcb_cnode_index 2)) (ReplyCap st False {AllowGrant, AllowWrite}) (is_cap_revocable (ReplyCap st False {AllowGrant, AllowWrite}) src_cap)) (st, tcb_cnode_index 2) (rt, tcb_cnode_index 3) src_p dest_p);
set_original (rt, tcb_cnode_index 3) (is_cap_revocable (ReplyCap st False {AllowGrant, AllowWrite}) src_cap)
od \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace>) \<and> (\<not> grant \<longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> do y <- set_thread_state st BlockedOnReply;
src_cap <- get_cap (st, tcb_cnode_index 2);
old_cap <- get_cap (rt, tcb_cnode_index 3);
y <- assert (old_cap = NullCap);
y <- set_cap (ReplyCap st False {AllowWrite}) (rt, tcb_cnode_index 3);
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s (st, tcb_cnode_index 2));
dest_p <- gets (\<lambda>s. cdt s (rt, tcb_cnode_index 3));
y <- do t <- gets cdt;
s <- get;
put (s\<lparr>cdt := t((rt, tcb_cnode_index 3) := if should_be_parent_of src_cap (is_original (st, tcb_cnode_index 2)) (ReplyCap st False {AllowWrite}) (is_cap_revocable (ReplyCap st False {AllowWrite}) src_cap) then Some (st, tcb_cnode_index 2) else t (st, tcb_cnode_index 2))\<rparr>)
od;
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original (st, tcb_cnode_index 2)) (ReplyCap st False {AllowWrite}) (is_cap_revocable (ReplyCap st False {AllowWrite}) src_cap)) (st, tcb_cnode_index 2) (rt, tcb_cnode_index 3) src_p dest_p);
set_original (rt, tcb_cnode_index 3) (is_cap_revocable (ReplyCap st False {AllowWrite}) src_cap)
od \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<And>P P' pd. \<lbrakk>arch_obj_pred P'; grant\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> do y <- set_thread_state st BlockedOnReply;
src_cap <- get_cap (st, tcb_cnode_index 2);
old_cap <- get_cap (rt, tcb_cnode_index 3);
y <- assert (old_cap = NullCap);
y <- set_cap (ReplyCap st False {AllowGrant, AllowWrite}) (rt, tcb_cnode_index 3);
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s (st, tcb_cnode_index 2));
dest_p <- gets (\<lambda>s. cdt s (rt, tcb_cnode_index 3));
y <- do t <- gets cdt;
s <- get;
put (s\<lparr>cdt := t((rt, tcb_cnode_index 3) := if should_be_parent_of src_cap (is_original (st, tcb_cnode_index 2)) (ReplyCap st False {AllowGrant, AllowWrite}) (is_cap_revocable (ReplyCap st False {AllowGrant, AllowWrite}) src_cap) then Some (st, tcb_cnode_index 2) else t (st, tcb_cnode_index 2))\<rparr>)
od;
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original (st, tcb_cnode_index 2)) (ReplyCap st False {AllowGrant, AllowWrite}) (is_cap_revocable (ReplyCap st False {AllowGrant, AllowWrite}) src_cap)) (st, tcb_cnode_index 2) (rt, tcb_cnode_index 3) src_p dest_p);
set_original (rt, tcb_cnode_index 3) (is_cap_revocable (ReplyCap st False {AllowGrant, AllowWrite}) src_cap)
od \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace>
 2. \<And>P P' pd. \<lbrakk>arch_obj_pred P'; \<not> grant\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> do y <- set_thread_state st BlockedOnReply;
src_cap <- get_cap (st, tcb_cnode_index 2);
old_cap <- get_cap (rt, tcb_cnode_index 3);
y <- assert (old_cap = NullCap);
y <- set_cap (ReplyCap st False {AllowWrite}) (rt, tcb_cnode_index 3);
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s (st, tcb_cnode_index 2));
dest_p <- gets (\<lambda>s. cdt s (rt, tcb_cnode_index 3));
y <- do t <- gets cdt;
s <- get;
put (s\<lparr>cdt := t((rt, tcb_cnode_index 3) := if should_be_parent_of src_cap (is_original (st, tcb_cnode_index 2)) (ReplyCap st False {AllowWrite}) (is_cap_revocable (ReplyCap st False {AllowWrite}) src_cap) then Some (st, tcb_cnode_index 2) else t (st, tcb_cnode_index 2))\<rparr>)
od;
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original (st, tcb_cnode_index 2)) (ReplyCap st False {AllowWrite}) (is_cap_revocable (ReplyCap st False {AllowWrite}) src_cap)) (st, tcb_cnode_index 2) (rt, tcb_cnode_index 3) src_p dest_p);
set_original (rt, tcb_cnode_index 3) (is_cap_revocable (ReplyCap st False {AllowWrite}) src_cap)
od \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace> proof (prove)
goal:
No subgoals!