theory Retype_R

lemma createObjects_no_cte_irq_handlers:
  assumes no_cte: "\<And>c. projectKO_opt val \<noteq> Some (c::cte)"
  assumes no_tcb: "\<And>t. projectKO_opt val \<noteq> Some (t::tcb)"
  shows
  "\<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and>
        pspace_no_overlap' ptr sz s \<and>
        range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and>
        valid_irq_handlers' s\<rbrace>
      createObjects ptr n val gbits
   \<lbrace>\<lambda>rv s.  valid_irq_handlers' s\<rbrace>" apply (simp add: valid_irq_handlers_cte_wp_at_form' createObjects_def irq_issued'_def) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift
             createObjects_orig_cte_wp_at2') apply (clarsimp simp: no_cte no_tcb split_def split: option.splits) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> valid_irq_handlers' s\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<and> (\<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal \<or> (\<forall>p. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) p s))\<rbrace> do y <- createObjects' ptr n val gbits;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>rv s. \<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal \<or> (\<forall>p. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<and> (\<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal \<or> (\<forall>p. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) p s)) \<Longrightarrow> \<forall>x. intStateIRQTable (ksInterruptState s) x = irqstate.IRQSignal \<or> (\<forall>xa. \<not> cte_wp_at' (\<lambda>a. cteCap a = capability.IRQHandlerCap x) xa s \<and> n \<noteq> 0 \<and> range_cover ptr (?sz10 x xa) (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some a \<Rightarrow> cteCap a = capability.IRQHandlerCap x) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some xa \<Rightarrow> ((\<lambda>a. cteCap a = capability.IRQHandlerCap x) \<circ> getF) xa)) \<and> pspace_no_overlap' ptr (?sz10 x xa) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; \<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal \<or> (\<forall>p. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) p s); projectKO_opt val = None; intStateIRQTable (ksInterruptState s) x \<noteq> irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<not> cte_wp_at' (\<lambda>a. cteCap a = capability.IRQHandlerCap x) xa s \<and> range_cover ptr (?sz10 x xa) (objBitsKO val + gbits) n \<and> pspace_no_overlap' ptr (?sz10 x xa) s proof (prove)
goal:
No subgoals!