theory CNodeInv_AI

lemma cap_move_irq_handlers[wp]:
  "\<lbrace>valid_irq_handlers and cte_wp_at ((=) cap.NullCap) ptr'
           and cte_wp_at (weak_derived cap) ptr\<rbrace>
     cap_move cap ptr ptr'
   \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace>" apply (simp add: valid_irq_handlers_def irq_issued_def) apply (rule hoare_pre) apply (rule hoare_use_eq [where f=interrupt_states, OF cap_move_interrupt_states]) apply (simp add: cap_move_def set_cdt_def) apply (wp | simp)+ apply (clarsimp simp: cte_wp_at_caps_of_state
                 elim!: ranE split: if_split_asm
                 dest!: weak_derived_cap_irqs) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers and cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr\<rbrace> cap_move cap ptr ptr' \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal) and cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr\<rbrace> cap_move cap ptr ptr' \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q11\<rbrace> cap_move cap ptr ptr' \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal\<rbrace>
 2. \<And>s. ((\<lambda>s. \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal) and cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr) s \<Longrightarrow> ?Q11 s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P14 f\<rbrace> cap_move cap ptr ptr' \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. f irq = IRQSignal\<rbrace>
 2. \<And>s. ((\<lambda>s. \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal) and cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr) s \<Longrightarrow> ?P14 (interrupt_states s) s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P14 f\<rbrace> do y <- set_cap cap ptr';
y <- set_cap NullCap ptr;
src_p <- gets (\<lambda>s. cdt s ptr);
dest_p <- gets (\<lambda>s. cdt s ptr');
cdt <- gets cdt;
y <- do s <- get;
put (s\<lparr>cdt := \<lambda>r. if (if r = ptr then None else if r = ptr' then cdt ptr else cdt r) = Some ptr then Some ptr' else if r = ptr then None else if r = ptr' then cdt ptr else cdt r\<rparr>)
od;
y <- do_extended_op (cap_move_ext ptr ptr' src_p dest_p);
is_original <- gets is_original_cap;
y <- set_original ptr' (is_original ptr);
set_original ptr False
od \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. f irq = IRQSignal\<rbrace>
 2. \<And>s. ((\<lambda>s. \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal) and cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr) s \<Longrightarrow> ?P14 (interrupt_states s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal) \<and> cte_wp_at ((=) NullCap) ptr' s \<and> cte_wp_at (weak_derived cap) ptr s \<Longrightarrow> \<forall>cap\<in>ran (\<lambda>a. if a = ptr then Some NullCap else if a = ptr' then Some cap else caps_of_state s a). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal proof (prove)
goal (2 subgoals):
 1. \<And>s a b irq capa. \<lbrakk>irq \<in> cap_irqs capa; \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal; caps_of_state s (a, b) = Some NullCap; caps_of_state s ptr = Some capa; cap_irqs cap = cap_irqs capa; (a, b) \<noteq> ptr; ptr' = (a, b)\<rbrakk> \<Longrightarrow> interrupt_states s irq = IRQSignal
 2. \<And>s capa a b irq capaa. \<lbrakk>irq \<in> cap_irqs capa; \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal; caps_of_state s ptr' = Some NullCap; caps_of_state s ptr = Some capaa; cap_irqs cap = cap_irqs capaa; (a, b) \<noteq> ptr; (a, b) \<noteq> ptr'; caps_of_state s (a, b) = Some capa\<rbrakk> \<Longrightarrow> interrupt_states s irq = IRQSignal proof (prove)
goal:
No subgoals!