theory CNode_IF

lemma cap_move_reads_respects:
  notes split_paired_All[simp del]
  shows
  "reads_respects aag l (K (is_subject aag (fst src_slot) \<and> is_subject aag (fst dest_slot)))
                  (cap_move new_cap src_slot dest_slot)" unfolding cap_move_def apply (subst gets_apply) apply (simp add: bind_assoc[symmetric]) apply (fold update_cdt_def) apply (simp add: bind_assoc cap_move_ext_def) apply (rule gen_asm_ev) apply (elim conjE) apply (wp set_original_reads_respects gets_apply_ev update_cdt_reads_respects
            set_cap_reads_respects update_cdt_list_reads_respects
         | simp split del: if_split | fastforce simp: equiv_for_def split: option.splits)+ apply (intro impI conjI allI) apply (fastforce simp: reads_equiv_def2 equiv_for_def
                   elim: states_equiv_forE_is_original_cap states_equiv_forE_cdt
                   dest: aag_can_read_self
                  split: option.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (fst src_slot) \<and> is_subject aag (fst dest_slot))) (cap_move new_cap src_slot dest_slot) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (fst src_slot) \<and> is_subject aag (fst dest_slot))) (do set_cap new_cap dest_slot;
set_cap NullCap src_slot;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
cdt <- gets cdt;
parent <- return $ cdt src_slot;
cdt' <- return $ cdt(dest_slot := parent, src_slot := None);
set_cdt (\<lambda>r. if cdt' r = Some src_slot then Some dest_slot else cdt' r);
do_extended_op (cap_move_ext src_slot dest_slot src_p dest_p);
is_original <- gets is_original_cap;
set_original dest_slot (is_original src_slot);
set_original src_slot False
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (fst src_slot) \<and> is_subject aag (fst dest_slot))) (do set_cap new_cap dest_slot;
set_cap NullCap src_slot;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
cdt <- gets cdt;
parent <- return $ cdt src_slot;
cdt' <- return $ cdt(dest_slot := parent, src_slot := None);
set_cdt (\<lambda>r. if cdt' r = Some src_slot then Some dest_slot else cdt' r);
do_extended_op (cap_move_ext src_slot dest_slot src_p dest_p);
a <- gets_apply is_original_cap src_slot;
set_original dest_slot a;
set_original src_slot False
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. is_subject aag (fst src_slot) \<and> is_subject aag (fst dest_slot)) (do y <- do y <- do src_p <- do y <- do y <- set_cap new_cap dest_slot;
set_cap NullCap src_slot
od;
gets (\<lambda>s. cdt s src_slot)
od;
dest_p <- gets (\<lambda>s. cdt s dest_slot);
y <- do cdt <- gets cdt;
set_cdt (\<lambda>r. if (if r = src_slot then None else (cdt(dest_slot := cdt src_slot)) r) = Some src_slot then Some dest_slot else (cdt(dest_slot := cdt src_slot, src_slot := None)) r)
od;
cap_move_ext src_slot dest_slot src_p dest_p
od;
gets_apply is_original_cap src_slot
od >>= set_original dest_slot;
set_original src_slot False
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. is_subject aag (fst src_slot) \<and> is_subject aag (fst dest_slot)) (do y <- do y <- do src_p <- do y <- do y <- set_cap new_cap dest_slot;
set_cap NullCap src_slot
od;
gets (\<lambda>s. cdt s src_slot)
od;
dest_p <- gets (\<lambda>s. cdt s dest_slot);
y <- update_cdt (\<lambda>cdt r. if (if r = src_slot then None else (cdt(dest_slot := cdt src_slot)) r) = Some src_slot then Some dest_slot else (cdt(dest_slot := cdt src_slot, src_slot := None)) r);
cap_move_ext src_slot dest_slot src_p dest_p
od;
gets_apply is_original_cap src_slot
od >>= set_original dest_slot;
set_original src_slot False
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. is_subject aag (fst src_slot) \<and> is_subject aag (fst dest_slot)) (do x <- set_cap new_cap dest_slot;
x <- set_cap NullCap src_slot;
x <- gets (\<lambda>s. cdt s src_slot);
xa <- gets (\<lambda>s. cdt s dest_slot);
xb <- update_cdt (\<lambda>cdt r. if (if r = src_slot then None else (cdt(dest_slot := cdt src_slot)) r) = Some src_slot then Some dest_slot else (cdt(dest_slot := cdt src_slot, src_slot := None)) r);
xa <- update_cdt_list (\<lambda>list. case xa of None \<Rightarrow> list | Some p \<Rightarrow> list(p := list_remove (list p) dest_slot));
x <- if src_slot = dest_slot then return () else do update_cdt_list (\<lambda>list. case x of None \<Rightarrow> list | Some p \<Rightarrow> list(p := list_replace (list p) src_slot dest_slot));
update_cdt_list (\<lambda>list. list(src_slot := [], dest_slot := list src_slot @ list dest_slot))
od;
x <- gets_apply is_original_cap src_slot;
y <- set_original dest_slot x;
set_original src_slot False
od) proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst src_slot) \<and> is_subject aag (fst dest_slot) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do x <- set_cap new_cap dest_slot;
x <- set_cap NullCap src_slot;
x <- gets (\<lambda>s. cdt s src_slot);
xa <- gets (\<lambda>s. cdt s dest_slot);
xb <- update_cdt (\<lambda>cdt r. if (if r = src_slot then None else (cdt(dest_slot := cdt src_slot)) r) = Some src_slot then Some dest_slot else (cdt(dest_slot := cdt src_slot, src_slot := None)) r);
xa <- update_cdt_list (\<lambda>list. case xa of None \<Rightarrow> list | Some p \<Rightarrow> list(p := list_remove (list p) dest_slot));
x <- if src_slot = dest_slot then return () else do update_cdt_list (\<lambda>list. case x of None \<Rightarrow> list | Some p \<Rightarrow> list(p := list_replace (list p) src_slot dest_slot));
update_cdt_list (\<lambda>list. list(src_slot := [], dest_slot := list src_slot @ list dest_slot))
od;
x <- gets_apply is_original_cap src_slot;
y <- set_original dest_slot x;
set_original src_slot False
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag (fst src_slot); is_subject aag (fst dest_slot)\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do x <- set_cap new_cap dest_slot;
x <- set_cap NullCap src_slot;
x <- gets (\<lambda>s. cdt s src_slot);
xa <- gets (\<lambda>s. cdt s dest_slot);
xb <- update_cdt (\<lambda>cdt r. if (if r = src_slot then None else (cdt(dest_slot := cdt src_slot)) r) = Some src_slot then Some dest_slot else (cdt(dest_slot := cdt src_slot, src_slot := None)) r);
xa <- update_cdt_list (\<lambda>list. case xa of None \<Rightarrow> list | Some p \<Rightarrow> list(p := list_remove (list p) dest_slot));
x <- if src_slot = dest_slot then return () else do update_cdt_list (\<lambda>list. case x of None \<Rightarrow> list | Some p \<Rightarrow> list(p := list_replace (list p) src_slot dest_slot));
update_cdt_list (\<lambda>list. list(src_slot := [], dest_slot := list src_slot @ list dest_slot))
od;
x <- gets_apply is_original_cap src_slot;
y <- set_original dest_slot x;
set_original src_slot False
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag (fst src_slot); is_subject aag (fst dest_slot)\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> cdt s src_slot = cdt t src_slot) \<and> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> cdt s dest_slot = cdt t dest_slot) \<and> (\<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>cdt r. if (if r = src_slot then None else (cdt(dest_slot := cdt src_slot)) r) = Some src_slot then Some dest_slot else (cdt(dest_slot := cdt src_slot, src_slot := None)) r) rv rv') \<and> (\<forall>rv rv'. equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>a. a) rv rv' \<longrightarrow> equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>list. case cdt s dest_slot of None \<Rightarrow> list | Some p \<Rightarrow> \<lambda>a. if a = p then list_remove (list p) dest_slot else list a) rv rv') \<and> (src_slot \<noteq> dest_slot \<longrightarrow> (\<forall>rv rv'. equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>a. a) rv rv' \<longrightarrow> equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>list. case cdt s src_slot of None \<Rightarrow> list | Some p \<Rightarrow> \<lambda>a. if a = p then list_replace (list p) src_slot dest_slot else list a) rv rv') \<and> (\<forall>rv rv'. equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>a. a) rv rv' \<longrightarrow> equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>list a. if a = dest_slot then list src_slot @ list dest_slot else if a = src_slot then [] else list a) rv rv')) \<and> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> is_original_cap s src_slot = is_original_cap t src_slot) proof (prove)
goal (7 subgoals):
 1. \<And>s sa t. \<lbrakk>is_subject aag (fst src_slot); is_subject aag (fst dest_slot); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> cdt sa src_slot = cdt t src_slot
 2. \<And>s sa t. \<lbrakk>is_subject aag (fst src_slot); is_subject aag (fst dest_slot); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> cdt sa dest_slot = cdt t dest_slot
 3. \<And>s rv rv'. \<lbrakk>is_subject aag (fst src_slot); is_subject aag (fst dest_slot); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>cdt r. if (if r = src_slot then None else (cdt(dest_slot := cdt src_slot)) r) = Some src_slot then Some dest_slot else (cdt(dest_slot := cdt src_slot, src_slot := None)) r) rv rv'
 4. \<And>s rv rv'. \<lbrakk>is_subject aag (fst src_slot); is_subject aag (fst dest_slot); equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>a. a) rv rv'\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>list. case cdt s dest_slot of None \<Rightarrow> list | Some p \<Rightarrow> \<lambda>a. if a = p then list_remove (list p) dest_slot else list a) rv rv'
 5. \<And>s rv rv'. \<lbrakk>is_subject aag (fst src_slot); is_subject aag (fst dest_slot); src_slot \<noteq> dest_slot; equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>a. a) rv rv'\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>list. case cdt s src_slot of None \<Rightarrow> list | Some p \<Rightarrow> \<lambda>a. if a = p then list_replace (list p) src_slot dest_slot else list a) rv rv'
 6. \<And>s rv rv'. \<lbrakk>is_subject aag (fst src_slot); is_subject aag (fst dest_slot); src_slot \<noteq> dest_slot; equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>a. a) rv rv'\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>list a. if a = dest_slot then list src_slot @ list dest_slot else if a = src_slot then [] else list a) rv rv'
 7. \<And>s sa t. \<lbrakk>is_subject aag (fst src_slot); is_subject aag (fst dest_slot); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa src_slot = is_original_cap t src_slot proof (prove)
goal:
No subgoals!