theory CNode_IF

lemma cap_insert_reads_respects:
  notes split_paired_All[simp del]
  shows
  "reads_respects aag l (K (aag_can_read aag (fst src_slot) \<and> aag_can_read aag (fst dest_slot)))
                  (cap_insert new_cap src_slot dest_slot)" unfolding cap_insert_def apply (rule gen_asm_ev) apply (subst gets_apply) apply (simp only: cap_insert_ext_extended.dxo_eq) apply (simp only: cap_insert_ext_def) apply (wp set_original_reads_respects update_cdt_reads_respects set_cap_reads_respects
            gets_apply_ev update_cdt_list_reads_respects set_untyped_cap_as_full_reads_respects
            get_cap_wp get_cap_rev
         | simp split del: if_split
         | clarsimp simp: equiv_for_def split: option.splits)+ by (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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read aag (fst src_slot) \<and> aag_can_read aag (fst dest_slot))) (cap_insert new_cap src_slot dest_slot) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read aag (fst src_slot) \<and> aag_can_read aag (fst dest_slot))) (do src_cap <- get_cap src_slot;
dest_original <- return $ is_cap_revocable new_cap src_cap;
old_cap <- get_cap dest_slot;
assert (old_cap = NullCap);
set_untyped_cap_as_full src_cap new_cap src_slot;
set_cap new_cap dest_slot;
is_original <- gets is_original_cap;
src_parent <- return $ should_be_parent_of src_cap (is_original src_slot) new_cap dest_original;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
update_cdt (\<lambda>cdt. cdt(dest_slot := if src_parent then Some src_slot else cdt src_slot));
do_extended_op (cap_insert_ext src_parent src_slot dest_slot src_p dest_p);
set_original dest_slot dest_original
od) proof (prove)
goal (1 subgoal):
 1. aag_can_read aag (fst src_slot) \<and> aag_can_read aag (fst dest_slot) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do src_cap <- get_cap src_slot;
dest_original <- return $ is_cap_revocable new_cap src_cap;
old_cap <- get_cap dest_slot;
assert (old_cap = NullCap);
set_untyped_cap_as_full src_cap new_cap src_slot;
set_cap new_cap dest_slot;
is_original <- gets is_original_cap;
src_parent <- return $ should_be_parent_of src_cap (is_original src_slot) new_cap dest_original;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
update_cdt (\<lambda>cdt. cdt(dest_slot := if src_parent then Some src_slot else cdt src_slot));
do_extended_op (cap_insert_ext src_parent src_slot dest_slot src_p dest_p);
set_original dest_slot dest_original
od) proof (prove)
goal (1 subgoal):
 1. aag_can_read aag (fst src_slot) \<and> aag_can_read aag (fst dest_slot) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do src_cap <- get_cap src_slot;
dest_original <- return $ is_cap_revocable new_cap src_cap;
old_cap <- get_cap dest_slot;
assert (old_cap = NullCap);
set_untyped_cap_as_full src_cap new_cap src_slot;
set_cap new_cap dest_slot;
a <- gets_apply is_original_cap src_slot;
src_parent <- return $ should_be_parent_of src_cap a new_cap dest_original;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
update_cdt (\<lambda>cdt. cdt(dest_slot := if src_parent then Some src_slot else cdt src_slot));
do_extended_op (cap_insert_ext src_parent src_slot dest_slot src_p dest_p);
set_original dest_slot dest_original
od) proof (prove)
goal (1 subgoal):
 1. aag_can_read aag (fst src_slot) \<and> aag_can_read aag (fst dest_slot) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do src_cap <- get_cap src_slot;
dest_original <- return $ is_cap_revocable new_cap src_cap;
old_cap <- get_cap dest_slot;
assert (old_cap = NullCap);
set_untyped_cap_as_full src_cap new_cap src_slot;
set_cap new_cap dest_slot;
a <- gets_apply is_original_cap src_slot;
src_parent <- return $ should_be_parent_of src_cap a new_cap dest_original;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
update_cdt (\<lambda>cdt. cdt(dest_slot := if src_parent then Some src_slot else cdt src_slot));
cap_insert_ext src_parent src_slot dest_slot src_p dest_p;
set_original dest_slot dest_original
od) proof (prove)
goal (1 subgoal):
 1. aag_can_read aag (fst src_slot) \<and> aag_can_read aag (fst dest_slot) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do src_cap <- get_cap src_slot;
dest_original <- return $ is_cap_revocable new_cap src_cap;
old_cap <- get_cap dest_slot;
assert (old_cap = NullCap);
set_untyped_cap_as_full src_cap new_cap src_slot;
set_cap new_cap dest_slot;
a <- gets_apply is_original_cap src_slot;
src_parent <- return $ should_be_parent_of src_cap a new_cap dest_original;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
update_cdt (\<lambda>cdt. cdt(dest_slot := if src_parent then Some src_slot else cdt src_slot));
do update_cdt_list (\<lambda>list. case dest_p of None \<Rightarrow> list | Some p \<Rightarrow> list(p := list_remove (list p) dest_slot));
update_cdt_list (\<lambda>list. case src_p of None \<Rightarrow> list(src_slot := if src_parent then [dest_slot] @ list src_slot else list src_slot) | Some p \<Rightarrow> list(src_slot := if src_parent then [dest_slot] @ list src_slot else list src_slot, p := if src_parent \<and> p \<noteq> src_slot then list p else if src_slot \<noteq> dest_slot then list_insert_after (list p) src_slot dest_slot else dest_slot # list p))
od;
set_original dest_slot dest_original
od) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>aag_can_read aag (fst src_slot); aag_can_read aag (fst dest_slot); cte_wp_at ((=) cap) src_slot s; cte_wp_at ((=) capa) dest_slot s\<rbrakk> \<Longrightarrow> (\<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) \<and> (capa = NullCap \<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))