theory CSpaceInv_AI

lemma cap_insert_irq_handlers[wp]:
  shows "\<lbrace>\<lambda>s. valid_irq_handlers s
      \<and> cte_wp_at (\<lambda>cap'. \<forall>irq \<in> cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s\<rbrace>
    cap_insert cap src dest
  \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace>" apply (simp add: cap_insert_def set_untyped_cap_as_full_def
                   update_cdt_def set_cdt_def set_original_def) apply (wp | simp split del: if_split)+ apply (wp set_cap_irq_handlers get_cap_wp)+ apply (clarsimp simp: is_cap_simps) apply (wp set_cap_cte_wp_at get_cap_wp)+ apply (clarsimp simp: cte_wp_at_caps_of_state valid_irq_handlers_def) apply (clarsimp simp: free_index_update_def
                 dest!: cap_irqs_must_be_irqhandler
                 split: cap.splits) apply (rename_tac irq irq') apply (case_tac "irq = irq'"; simp) apply (drule_tac x=cap in bspec; clarsimp simp: ranI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_irq_handlers s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_irq_handlers s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) src else return ();
y <- set_cap cap dest;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
y <- do t <- gets cdt;
s <- get;
put (s\<lparr>cdt := t(dest := if should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap) then Some src else t src)\<rparr>)
od;
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap)) src dest src_p dest_p);
r <- gets is_original_cap;
modify (is_original_cap_update (\<lambda>_. r(dest := is_cap_revocable cap src_cap)))
od \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>src_cap x. \<lbrace>?B4 src_cap x () ()\<rbrace> set_cap cap dest \<lbrace>\<lambda>yb. valid_irq_handlers\<rbrace>
 2. \<And>src_cap x y. \<lbrace>?B3 src_cap x y\<rbrace> if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) src else return () \<lbrace>?B4 src_cap x y\<rbrace>
 3. \<And>src_cap x. \<lbrace>?B2 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>?B3 src_cap x\<rbrace>
 4. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> get_cap dest \<lbrace>?B2 src_cap\<rbrace>
 5. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 6. \<And>s. valid_irq_handlers s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>src_cap x y. is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<Longrightarrow> \<lbrace>?P'40 src_cap x y\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) dest s\<rbrace>
 2. \<And>src_cap x y. \<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<Longrightarrow> \<lbrace>?R39 src_cap x y\<rbrace> return () \<lbrace>\<lambda>a b. valid_irq_handlers b \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq b) dest b\<rbrace>
 3. \<And>src_cap x. \<lbrace>?B2 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>\<lambda>y s. (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> (valid_irq_handlers s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs (max_free_index_update src_cap) - cap_irqs cap'. irq_issued irq s) src s) \<and> ?P'40 src_cap x y s) \<and> (\<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<longrightarrow> ?R39 src_cap x y s)\<rbrace>
 4. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> get_cap dest \<lbrace>?B2 src_cap\<rbrace>
 5. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 6. \<And>s. valid_irq_handlers s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>x dev f deva ra bitsa fa. cap = UntypedCap deva ra bitsa fa \<Longrightarrow> \<lbrace>?P'40 (UntypedCap dev ra bitsa f) x ()\<rbrace> set_cap (free_index_update (\<lambda>_. max_free_index bitsa) (UntypedCap dev ra bitsa f)) src \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>cap'. True) dest\<rbrace>
 2. \<And>src_cap x y. \<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<Longrightarrow> \<lbrace>?R39 src_cap x y\<rbrace> return () \<lbrace>\<lambda>a b. valid_irq_handlers b \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq b) dest b\<rbrace>
 3. \<And>src_cap x. \<lbrace>?B2 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>\<lambda>y s. (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> (valid_irq_handlers s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs (max_free_index_update src_cap) - cap_irqs cap'. irq_issued irq s) src s) \<and> ?P'40 src_cap x y s) \<and> (\<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<longrightarrow> ?R39 src_cap x y s)\<rbrace>
 4. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> get_cap dest \<lbrace>?B2 src_cap\<rbrace>
 5. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 6. \<And>s. valid_irq_handlers s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_handlers s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src s \<longrightarrow> (\<forall>capb. cte_wp_at ((=) capb) dest s \<longrightarrow> capb = NullCap \<longrightarrow> (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> (valid_irq_handlers s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs (max_free_index_update capa) - cap_irqs cap'. irq_issued irq s) src s) \<and> ((\<lambda>s. if dest = src then True else cte_wp_at (\<lambda>a. True) dest s) and cte_wp_at (\<lambda>_. True) src) s) \<and> (\<not> (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap) \<longrightarrow> valid_irq_handlers s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) dest s)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. irq_issued irq s; caps_of_state s src = Some capa; \<forall>irq\<in>cap_irqs cap - cap_irqs capa. irq_issued irq s; dest \<noteq> src; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> (\<forall>irq\<in>cap_irqs (max_free_index_update capa) - cap_irqs capa. irq_issued irq s)) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> (\<forall>irq\<in>cap_irqs cap. irq_issued irq s)) proof (prove)
goal (1 subgoal):
 1. \<And>s irq x10. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. irq_issued irq s; caps_of_state s src = Some (IRQHandlerCap x10); \<forall>irq\<in>{irq} - {x10}. irq_issued irq s; dest \<noteq> src; caps_of_state s dest = Some NullCap; cap = IRQHandlerCap irq\<rbrakk> \<Longrightarrow> irq_issued irq s proof (prove)
goal (1 subgoal):
 1. \<And>s irq irq'. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. irq_issued irq s; caps_of_state s src = Some (IRQHandlerCap irq'); \<forall>irq\<in>{irq} - {irq'}. irq_issued irq s; dest \<noteq> src; caps_of_state s dest = Some NullCap; cap = IRQHandlerCap irq\<rbrakk> \<Longrightarrow> irq_issued irq s proof (prove)
goal (1 subgoal):
 1. \<And>s irq irq'. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. irq_issued irq s; caps_of_state s src = Some (IRQHandlerCap irq'); dest \<noteq> src; caps_of_state s dest = Some NullCap; cap = IRQHandlerCap irq'; irq = irq'\<rbrakk> \<Longrightarrow> irq_issued irq' s proof (prove)
goal:
No subgoals!