theory CNode_AC

lemma cap_move_respects[wp]:
  "\<lbrace>integrity aag X st and pas_refined aag
                       and K (is_subject aag (fst dest) \<and> is_subject aag (fst src))\<rbrace>
   cap_move cap src dest
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (clarsimp simp: cap_move_def) apply (wpsimp wp: get_cap_wp set_cap_integrity_autarch set_original_integrity_autarch
                     cap_move_ext_list_integ_lift[where Q="\<top>"] cap_move_list_integrity
               simp: set_cdt_def | blast)+ apply (rule wp_integrity_clean') apply (simp add: integrity_def integrity_cdt_def) apply (blast intro: cca_owned) apply (wpsimp wp: set_cap_integrity_autarch)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (is_subject aag (fst dest) \<and> is_subject aag (fst src))\<rbrace> cap_move cap src dest \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst dest) \<and> is_subject aag (fst src) \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag\<rbrace> cap_move cap src dest \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag (fst dest); is_subject aag (fst src)\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag\<rbrace> do y <- set_cap cap dest;
y <- set_cap NullCap src;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (if r = src then None else if r = dest then cdt src else cdt r) = Some src then Some dest else if r = src then None else if r = dest then cdt src else cdt r);
y <- cap_move_ext src dest src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original dest (is_original src);
set_original src False
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_subject aag (fst dest); is_subject aag (fst src)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 ()\<rbrace> set_cap NullCap src \<lbrace>\<lambda>ya s. integrity aag X st (s\<lparr>cdt := \<lambda>r. if (if r = src then None else if r = dest then cdt s src else cdt s r) = Some src then Some dest else if r = src then None else if r = dest then cdt s src else cdt s r\<rparr>)\<rbrace>
 2. \<lbrakk>is_subject aag (fst dest); is_subject aag (fst src)\<rbrakk> \<Longrightarrow> \<lbrace>?Q10\<rbrace> set_cap cap dest \<lbrace>?B11\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag (fst dest); is_subject aag (fst src); (integrity aag X st and pas_refined aag) s\<rbrakk> \<Longrightarrow> ?Q10 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag (fst dest); is_subject aag (fst src)\<rbrakk> \<Longrightarrow> integrity aag X s (s\<lparr>cdt := \<lambda>r. if (if r = src then None else if r = dest then cdt s src else cdt s r) = Some src then Some dest else if r = src then None else if r = dest then cdt s src else cdt s r\<rparr>)
 2. \<lbrakk>is_subject aag (fst dest); is_subject aag (fst src)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 ()\<rbrace> set_cap NullCap src \<lbrace>\<lambda>ya. integrity aag X st\<rbrace>
 3. \<lbrakk>is_subject aag (fst dest); is_subject aag (fst src)\<rbrakk> \<Longrightarrow> \<lbrace>?Q10\<rbrace> set_cap cap dest \<lbrace>?B11\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst dest); is_subject aag (fst src); (integrity aag X st and pas_refined aag) s\<rbrakk> \<Longrightarrow> ?Q10 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag (fst dest); is_subject aag (fst src)\<rbrakk> \<Longrightarrow> \<forall>a b. ((a, b) = dest \<longrightarrow> (dest = src \<longrightarrow> cdt s src = None \<or> cdt_change_allowed' aag src s) \<and> (dest \<noteq> src \<longrightarrow> (cdt s src = Some src \<longrightarrow> cdt s dest = Some dest \<or> cdt_change_allowed' aag dest s) \<and> (cdt s src \<noteq> Some src \<longrightarrow> cdt s dest = cdt s src \<or> cdt_change_allowed' aag dest s))) \<and> ((a, b) \<noteq> dest \<longrightarrow> ((a, b) = src \<longrightarrow> cdt s src = None \<or> cdt_change_allowed' aag src s) \<and> ((a, b) \<noteq> src \<longrightarrow> cdt s (a, b) = Some src \<longrightarrow> src = dest \<or> cdt_change_allowed' aag (a, b) s))
 2. \<lbrakk>is_subject aag (fst dest); is_subject aag (fst src)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 ()\<rbrace> set_cap NullCap src \<lbrace>\<lambda>ya. integrity aag X st\<rbrace>
 3. \<lbrakk>is_subject aag (fst dest); is_subject aag (fst src)\<rbrakk> \<Longrightarrow> \<lbrace>?Q10\<rbrace> set_cap cap dest \<lbrace>?B11\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst dest); is_subject aag (fst src); (integrity aag X st and pas_refined aag) s\<rbrakk> \<Longrightarrow> ?Q10 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_subject aag (fst dest); is_subject aag (fst src)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 ()\<rbrace> set_cap NullCap src \<lbrace>\<lambda>ya. integrity aag X st\<rbrace>
 2. \<lbrakk>is_subject aag (fst dest); is_subject aag (fst src)\<rbrakk> \<Longrightarrow> \<lbrace>?Q10\<rbrace> set_cap cap dest \<lbrace>?B11\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag (fst dest); is_subject aag (fst src); (integrity aag X st and pas_refined aag) s\<rbrakk> \<Longrightarrow> ?Q10 s proof (prove)
goal:
No subgoals!