theory Interrupt_DR

lemma cap_delete_one_original:
  "slot \<noteq> slot' \<Longrightarrow> \<lbrace>\<lambda>s. is_original_cap s slot\<rbrace> cap_delete_one slot'
            \<lbrace>\<lambda>r s. is_original_cap s slot\<rbrace>" apply (clarsimp simp:cap_delete_one_def unless_def) apply (wp when_wp) apply (clarsimp simp:empty_slot_def) apply wp apply (clarsimp simp:set_cdt_def) apply (wp dxo_wp_weak | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slot \<noteq> slot' \<Longrightarrow> \<lbrace>\<lambda>s. is_original_cap s slot\<rbrace> cap_delete_one slot' \<lbrace>\<lambda>r s. is_original_cap s slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. slot \<noteq> slot' \<Longrightarrow> \<lbrace>\<lambda>s. is_original_cap s slot\<rbrace> do cap <- CSpaceAcc_A.get_cap slot';
when (cap \<noteq> cap.NullCap) (do final <- IpcCancel_A.is_final_cap cap;
y <- IpcCancel_A.fast_finalise cap final;
IpcCancel_A.empty_slot slot' cap.NullCap
od)
od \<lbrace>\<lambda>r s. is_original_cap s slot\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>cap final y. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B4 cap final y\<rbrace> IpcCancel_A.empty_slot slot' cap.NullCap \<lbrace>\<lambda>r s. is_original_cap s slot\<rbrace>
 2. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B4 cap final\<rbrace>
 3. \<And>cap. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B3 cap\<rbrace>
 4. slot \<noteq> slot' \<Longrightarrow> \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q2 cap else (\<lambda>s. is_original_cap s slot)\<rbrace>
 5. \<And>s. \<lbrakk>slot \<noteq> slot'; is_original_cap s slot\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B4 cap final ()\<rbrace> do cap <- CSpaceAcc_A.get_cap slot';
if cap = cap.NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot');
cdt <- gets cdt;
parent <- return $ cdt slot';
set_cdt ((\<lambda>p. if cdt p = Some slot' then parent else cdt p)(slot' := None));
do_extended_op (empty_slot_ext slot' slot_p);
set_original slot' False;
CSpaceAcc_A.set_cap cap.NullCap slot';
post_cap_deletion cap.NullCap
od
od \<lbrace>\<lambda>r s. is_original_cap s slot\<rbrace>
 2. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B4 cap final\<rbrace>
 3. \<And>cap. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B3 cap\<rbrace>
 4. slot \<noteq> slot' \<Longrightarrow> \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q2 cap else (\<lambda>s. is_original_cap s slot)\<rbrace>
 5. \<And>s. \<lbrakk>slot \<noteq> slot'; is_original_cap s slot\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (13 subgoals):
 1. \<And>cap final capa x xa xb xc xd xe xf. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B23 cap final capa x xa xb xc xd xe xf\<rbrace> post_cap_deletion cap.NullCap \<lbrace>\<lambda>r s. is_original_cap s slot\<rbrace>
 2. \<And>cap final capa x xa xb xc xd xe. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B21 cap final capa x xa xb xc xd xe\<rbrace> CSpaceAcc_A.set_cap cap.NullCap slot' \<lbrace>?B23 cap final capa x xa xb xc xd xe\<rbrace>
 3. \<And>cap final capa x xa xb xc xd. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B19 cap final capa x xa xb xc xd\<rbrace> set_original slot' False \<lbrace>?B21 cap final capa x xa xb xc xd\<rbrace>
 4. \<And>cap final capa x xa xb xc. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B17 cap final capa x xa xb xc\<rbrace> do_extended_op (empty_slot_ext slot' x) \<lbrace>?B19 cap final capa x xa xb xc\<rbrace>
 5. \<And>cap final capa x xa xb. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap final capa x xa xb\<rbrace> set_cdt ((\<lambda>p. if xa p = Some slot' then xb else xa p)(slot' := None)) \<lbrace>?B17 cap final capa x xa xb\<rbrace>
 6. \<And>cap final capa x xa. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B15 cap final capa x xa\<rbrace> return $ xa slot' \<lbrace>?B16 cap final capa x xa\<rbrace>
 7. \<And>cap final capa x. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B14 cap final capa x\<rbrace> gets cdt \<lbrace>?B15 cap final capa x\<rbrace>
 8. \<And>cap final capa. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap final capa\<rbrace> gets (\<lambda>s. cdt s slot') \<lbrace>?B14 cap final capa\<rbrace>
 9. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B4 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> is_original_cap s slot) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> ?R12 cap final capa s)\<rbrace>
 10. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B4 cap final\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>cap final capa x xa xb. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B23 cap final capa x xa xb () () () ()\<rbrace> return () \<lbrace>\<lambda>r s. is_original_cap s slot\<rbrace>
 2. \<And>cap final capa x xa xb xc xd xe. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B21 cap final capa x xa xb xc xd xe\<rbrace> CSpaceAcc_A.set_cap cap.NullCap slot' \<lbrace>?B23 cap final capa x xa xb xc xd xe\<rbrace>
 3. \<And>cap final capa x xa xb xc xd. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B19 cap final capa x xa xb xc xd\<rbrace> set_original slot' False \<lbrace>?B21 cap final capa x xa xb xc xd\<rbrace>
 4. \<And>cap final capa x xa xb xc. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B17 cap final capa x xa xb xc\<rbrace> do_extended_op (empty_slot_ext slot' x) \<lbrace>?B19 cap final capa x xa xb xc\<rbrace>
 5. \<And>cap final capa x xa xb. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap final capa x xa xb\<rbrace> set_cdt ((\<lambda>p. if xa p = Some slot' then xb else xa p)(slot' := None)) \<lbrace>?B17 cap final capa x xa xb\<rbrace>
 6. \<And>cap final capa x xa. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B15 cap final capa x xa\<rbrace> return $ xa slot' \<lbrace>?B16 cap final capa x xa\<rbrace>
 7. \<And>cap final capa x. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B14 cap final capa x\<rbrace> gets cdt \<lbrace>?B15 cap final capa x\<rbrace>
 8. \<And>cap final capa. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap final capa\<rbrace> gets (\<lambda>s. cdt s slot') \<lbrace>?B14 cap final capa\<rbrace>
 9. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B4 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> is_original_cap s slot) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> ?R12 cap final capa s)\<rbrace>
 10. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B4 cap final\<rbrace>
A total of 13 subgoals... proof (prove)
goal:
No subgoals!