theory Retype_IF

lemma create_cap_reads_respects:
  "reads_respects aag l (K (is_subject aag (fst (fst slot))))
     (create_cap type bits untyped dev slot)" apply (rule gen_asm_ev) apply (simp add: create_cap_def split_def bind_assoc[symmetric]) apply (fold update_cdt_def) apply (simp add: bind_assoc create_cap_ext_def) apply (wp set_cap_reads_respects set_original_reads_respects
            update_cdt_list_reads_respects update_cdt_reads_respects
         | simp | fastforce simp: equiv_for_def split: option.splits)+ apply (intro impI conjI allI) 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 (is_subject aag (fst (fst slot)))) (create_cap type bits untyped dev slot) proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst (fst slot)) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (create_cap type bits untyped dev slot) proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst (fst slot)) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do y <- do y <- do dest_p <- gets (\<lambda>s. cdt s (fst slot));
y <- do cdt <- gets cdt;
set_cdt (cdt(fst slot \<mapsto> untyped))
od;
create_cap_ext untyped (fst slot) dest_p
od;
set_original (fst slot) True
od;
set_cap (default_cap type (snd slot) bits dev) (fst slot)
od) proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst (fst slot)) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do y <- do y <- do dest_p <- gets (\<lambda>s. cdt s (fst slot));
y <- update_cdt (\<lambda>cdt. cdt(fst slot \<mapsto> untyped));
create_cap_ext untyped (fst slot) dest_p
od;
set_original (fst slot) True
od;
set_cap (default_cap type (snd slot) bits dev) (fst slot)
od) proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst (fst slot)) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do x <- gets (\<lambda>s. cdt s (fst slot));
xa <- update_cdt (\<lambda>cdt. cdt(fst slot \<mapsto> untyped));
x <- update_cdt_list (\<lambda>list. case x of None \<Rightarrow> list | Some p \<Rightarrow> list(p := list_remove (list p) (fst slot)));
x <- update_cdt_list (\<lambda>list. list(untyped := fst slot # list untyped));
y <- set_original (fst slot) True;
set_cap (default_cap type (snd slot) bits dev) (fst slot)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. is_subject aag (fst (fst slot)) \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> cdt s (fst slot) = cdt t (fst 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. cdt(fst slot \<mapsto> untyped)) rv rv') \<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>list. case cdt s (fst slot) of None \<Rightarrow> list | Some p \<Rightarrow> list(p := list_remove (list p) (fst slot))) rv rv') \<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>list. list(untyped := fst slot # list untyped)) rv rv') proof (prove)
goal (4 subgoals):
 1. \<And>s sa t. \<lbrakk>is_subject aag (fst (fst slot)); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> cdt sa (fst slot) = cdt t (fst slot)
 2. \<And>s rv rv'. \<lbrakk>is_subject aag (fst (fst 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. cdt(fst slot \<mapsto> untyped)) rv rv'
 3. \<And>s rv rv'. \<lbrakk>is_subject aag (fst (fst 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>list. case cdt s (fst slot) of None \<Rightarrow> list | Some p \<Rightarrow> list(p := list_remove (list p) (fst slot))) rv rv'
 4. \<And>s rv rv'. \<lbrakk>is_subject aag (fst (fst 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>list. list(untyped := fst slot # list untyped)) rv rv'