theory Example_Valid_StateH

lemma kh0H_simps[simp]:
  "kh0H (init_irq_node_ptr + (ucast (irq::10 word) << cte_level_bits)) =
                Some (KOCTE (CTE capability.NullCap Null_mdb))"
  "kh0H ntfn_ptr = Some (KONotification ntfnH)"
  "kh0H irq_cnode_ptr = Some (KOCTE irq_cte)"
  "kh0H Low_tcb_ptr = Some (KOTCB Low_tcbH)"
  "kh0H High_tcb_ptr = Some (KOTCB High_tcbH)"
  "kh0H idle_tcb_ptr = Some (KOTCB idle_tcbH)"
  "kh0H init_globals_frame = Some KOUserData"
  "length x = 10 \<Longrightarrow> kh0H (Low_cnode_ptr + of_bl x * 0x10) = Low_cte Low_cnode_ptr (Low_cnode_ptr + of_bl x * 0x10)"
  "length x = 10 \<Longrightarrow> kh0H (High_cnode_ptr + of_bl x * 0x10) = High_cte High_cnode_ptr (High_cnode_ptr + of_bl x * 0x10)"
  "length x = 10 \<Longrightarrow> kh0H (Silc_cnode_ptr + of_bl x * 0x10) = Silc_cte Silc_cnode_ptr (Silc_cnode_ptr + of_bl x * 0x10)"
  "kh0H (Low_pd_ptr + (ucast (y:: 12 word) << 2)) = Low_pdH Low_pd_ptr (Low_pd_ptr + (ucast (y:: 12 word) << 2))"
  "kh0H (High_pd_ptr + (ucast (y:: 12 word) << 2)) = High_pdH High_pd_ptr (High_pd_ptr + (ucast (y:: 12 word) << 2))"
  "kh0H (init_global_pd + (ucast (y:: 12 word) << 2)) = global_pdH' init_global_pd (init_global_pd + (ucast (y:: 12 word) << 2))"
  "kh0H (Low_pt_ptr + (ucast (z:: 8 word) << 2)) = Low_ptH Low_pt_ptr (Low_pt_ptr + (ucast (z:: 8 word) << 2))"
  "kh0H (High_pt_ptr + (ucast (z:: 8 word) << 2)) = High_ptH High_pt_ptr (High_pt_ptr + (ucast (z:: 8 word) << 2))" supply option.case_cong[cong] apply (clarsimp simp: kh0H_def option_update_range_def) apply fastforce apply (simp add:kh0H_def) apply (clarsimp simp: kh0H_def option_update_range_def kh0H_dom_distinct not_in_range_None)+ by ((clarsimp simp: kh0H_def option_update_range_def kh0H_dom_distinct kh0H_dom_distinct' not_in_range_None offs_in_range | simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD1] not_in_range_None | simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD2] not_in_range_None)+,
            rule conjI,
             clarsimp,
             drule not_disjointI,
               (erule offs_in_range | rule offs_in_range),
              (erule offs_in_range | rule offs_in_range),
             erule notE,
             rule kh0H_dom_sets_distinct,
            clarsimp split: option.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((kh0H (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)) = Some (KOCTE (CTE capability.NullCap (MDB 0 0 False False))) &&& kh0H ntfn_ptr = Some (KONotification ntfnH) &&& kh0H irq_cnode_ptr = Some (KOCTE irq_cte)) &&& (kh0H Low_tcb_ptr = Some (KOTCB Low_tcbH) &&& kh0H High_tcb_ptr = Some (KOTCB High_tcbH)) &&& kh0H idle_tcb_ptr = Some (KOTCB idle_tcbH) &&& kh0H init_globals_frame = Some KOUserData) &&& (((length x = 10 \<Longrightarrow> kh0H (Low_cnode_ptr + of_bl x * 0x10) = Low_cte Low_cnode_ptr (Low_cnode_ptr + of_bl x * 0x10)) &&& (length x = 10 \<Longrightarrow> kh0H (High_cnode_ptr + of_bl x * 0x10) = High_cte High_cnode_ptr (High_cnode_ptr + of_bl x * 0x10))) &&& (length x = 10 \<Longrightarrow> kh0H (Silc_cnode_ptr + of_bl x * 0x10) = Silc_cte Silc_cnode_ptr (Silc_cnode_ptr + of_bl x * 0x10)) &&& kh0H (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2)) = Low_pdH Low_pd_ptr (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2))) &&& (kh0H (High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2)) = High_pdH High_pd_ptr (High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2)) &&& kh0H (init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2)) = global_pdH' init_global_pd (init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2))) &&& kh0H (Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2)) = Low_ptH Low_pt_ptr (Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2)) &&& kh0H (High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2)) = High_ptH High_pt_ptr (High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2)) proof (prove)
goal (1 subgoal):
 1. ((kh0H (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)) = Some (KOCTE (CTE capability.NullCap (MDB 0 0 False False))) &&& kh0H ntfn_ptr = Some (KONotification ntfnH) &&& kh0H irq_cnode_ptr = Some (KOCTE irq_cte)) &&& (kh0H Low_tcb_ptr = Some (KOTCB Low_tcbH) &&& kh0H High_tcb_ptr = Some (KOTCB High_tcbH)) &&& kh0H idle_tcb_ptr = Some (KOTCB idle_tcbH) &&& kh0H init_globals_frame = Some KOUserData) &&& (((length x = 10 \<Longrightarrow> kh0H (Low_cnode_ptr + of_bl x * 0x10) = Low_cte Low_cnode_ptr (Low_cnode_ptr + of_bl x * 0x10)) &&& (length x = 10 \<Longrightarrow> kh0H (High_cnode_ptr + of_bl x * 0x10) = High_cte High_cnode_ptr (High_cnode_ptr + of_bl x * 0x10))) &&& (length x = 10 \<Longrightarrow> kh0H (Silc_cnode_ptr + of_bl x * 0x10) = Silc_cte Silc_cnode_ptr (Silc_cnode_ptr + of_bl x * 0x10)) &&& kh0H (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2)) = Low_pdH Low_pd_ptr (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2))) &&& (kh0H (High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2)) = High_pdH High_pd_ptr (High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2)) &&& kh0H (init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2)) = global_pdH' init_global_pd (init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2))) &&& kh0H (Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2)) = Low_ptH Low_pt_ptr (Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2)) &&& kh0H (High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2)) = High_ptH High_pt_ptr (High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2)) proof (prove)
goal (15 subgoals):
 1. \<forall>irqa. UCAST(10 \<rightarrow> 32) irqa << cte_level_bits \<noteq> UCAST(10 \<rightarrow> 32) irq << cte_level_bits \<Longrightarrow> (case Low_cte Low_cnode_ptr (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)) of None \<Rightarrow> case High_cte High_cnode_ptr (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)) of None \<Rightarrow> case Silc_cte Silc_cnode_ptr (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)) of None \<Rightarrow> case Low_pdH Low_pd_ptr (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)) of None \<Rightarrow> case High_pdH High_pd_ptr (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)) of None \<Rightarrow> case Low_ptH Low_pt_ptr (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)) of None \<Rightarrow> case High_ptH High_pt_ptr (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)) of None \<Rightarrow> case global_pdH' init_global_pd (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)) of None \<Rightarrow> None | Some x2 \<Rightarrow> Some x2 | Some x2 \<Rightarrow> Some x2 | Some x2 \<Rightarrow> Some x2 | Some x2 \<Rightarrow> Some x2 | Some x2 \<Rightarrow> Some x2 | Some x2 \<Rightarrow> Some x2 | Some x2 \<Rightarrow> Some x2 | Some x2 \<Rightarrow> Some x2) = Some (KOCTE (CTE capability.NullCap (MDB 0 0 False False)))
 2. kh0H ntfn_ptr = Some (KONotification ntfnH)
 3. kh0H irq_cnode_ptr = Some (KOCTE irq_cte)
 4. kh0H Low_tcb_ptr = Some (KOTCB Low_tcbH)
 5. kh0H High_tcb_ptr = Some (KOTCB High_tcbH)
 6. kh0H idle_tcb_ptr = Some (KOTCB idle_tcbH)
 7. kh0H init_globals_frame = Some KOUserData
 8. length x = 10 \<Longrightarrow> kh0H (Low_cnode_ptr + of_bl x * 0x10) = Low_cte Low_cnode_ptr (Low_cnode_ptr + of_bl x * 0x10)
 9. length x = 10 \<Longrightarrow> kh0H (High_cnode_ptr + of_bl x * 0x10) = High_cte High_cnode_ptr (High_cnode_ptr + of_bl x * 0x10)
 10. length x = 10 \<Longrightarrow> kh0H (Silc_cnode_ptr + of_bl x * 0x10) = Silc_cte Silc_cnode_ptr (Silc_cnode_ptr + of_bl x * 0x10)
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. kh0H ntfn_ptr = Some (KONotification ntfnH)
 2. kh0H irq_cnode_ptr = Some (KOCTE irq_cte)
 3. kh0H Low_tcb_ptr = Some (KOTCB Low_tcbH)
 4. kh0H High_tcb_ptr = Some (KOTCB High_tcbH)
 5. kh0H idle_tcb_ptr = Some (KOTCB idle_tcbH)
 6. kh0H init_globals_frame = Some KOUserData
 7. length x = 10 \<Longrightarrow> kh0H (Low_cnode_ptr + of_bl x * 0x10) = Low_cte Low_cnode_ptr (Low_cnode_ptr + of_bl x * 0x10)
 8. length x = 10 \<Longrightarrow> kh0H (High_cnode_ptr + of_bl x * 0x10) = High_cte High_cnode_ptr (High_cnode_ptr + of_bl x * 0x10)
 9. length x = 10 \<Longrightarrow> kh0H (Silc_cnode_ptr + of_bl x * 0x10) = Silc_cte Silc_cnode_ptr (Silc_cnode_ptr + of_bl x * 0x10)
 10. kh0H (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2)) = Low_pdH Low_pd_ptr (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2))
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. option_update_range (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (KOCTE (CTE capability.NullCap (MDB 0 0 False False))) else None) (option_update_range (Low_cte Low_cnode_ptr) (option_update_range (High_cte High_cnode_ptr) (option_update_range (Silc_cte Silc_cnode_ptr) (option_update_range [ntfn_ptr \<mapsto> KONotification ntfnH] (option_update_range [irq_cnode_ptr \<mapsto> KOCTE irq_cte] (option_update_range (Low_pdH Low_pd_ptr) (option_update_range (High_pdH High_pd_ptr) (option_update_range (Low_ptH Low_pt_ptr) (option_update_range (High_ptH High_pt_ptr) (option_update_range [Low_tcb_ptr \<mapsto> KOTCB Low_tcbH] (option_update_range [High_tcb_ptr \<mapsto> KOTCB High_tcbH] (option_update_range [idle_tcb_ptr \<mapsto> KOTCB idle_tcbH] (option_update_range (global_pdH' init_global_pd) (option_update_range [init_globals_frame \<mapsto> KOUserData] (\<lambda>x. None))))))))))))))) ntfn_ptr = Some (KONotification ntfnH)
 2. kh0H irq_cnode_ptr = Some (KOCTE irq_cte)
 3. kh0H Low_tcb_ptr = Some (KOTCB Low_tcbH)
 4. kh0H High_tcb_ptr = Some (KOTCB High_tcbH)
 5. kh0H idle_tcb_ptr = Some (KOTCB idle_tcbH)
 6. kh0H init_globals_frame = Some KOUserData
 7. length x = 10 \<Longrightarrow> kh0H (Low_cnode_ptr + of_bl x * 0x10) = Low_cte Low_cnode_ptr (Low_cnode_ptr + of_bl x * 0x10)
 8. length x = 10 \<Longrightarrow> kh0H (High_cnode_ptr + of_bl x * 0x10) = High_cte High_cnode_ptr (High_cnode_ptr + of_bl x * 0x10)
 9. length x = 10 \<Longrightarrow> kh0H (Silc_cnode_ptr + of_bl x * 0x10) = Silc_cte Silc_cnode_ptr (Silc_cnode_ptr + of_bl x * 0x10)
 10. kh0H (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2)) = Low_pdH Low_pd_ptr (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2))
A total of 14 subgoals... proof (prove)
goal (8 subgoals):
 1. length x = 10 \<Longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> init_globals_frame \<and> (Low_cnode_ptr + of_bl x * 0x10 \<noteq> init_globals_frame \<longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> idle_tcb_ptr \<and> (Low_cnode_ptr + of_bl x * 0x10 \<noteq> idle_tcb_ptr \<longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> High_tcb_ptr \<and> (Low_cnode_ptr + of_bl x * 0x10 \<noteq> High_tcb_ptr \<longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> Low_tcb_ptr \<and> (Low_cnode_ptr + of_bl x * 0x10 \<noteq> Low_tcb_ptr \<longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> irq_cnode_ptr \<and> (Low_cnode_ptr + of_bl x * 0x10 \<noteq> irq_cnode_ptr \<longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> ntfn_ptr \<and> (Low_cnode_ptr + of_bl x * 0x10 \<noteq> ntfn_ptr \<longrightarrow> ((\<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = Low_cnode_ptr + of_bl x * 0x10) \<longrightarrow> Some (KOCTE (CTE capability.NullCap (MDB 0 0 False False))) = Low_cte Low_cnode_ptr (Low_cnode_ptr + of_bl x * 0x10)) \<and> ((\<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> Low_cnode_ptr + of_bl x * 0x10) \<longrightarrow> (case Low_cte Low_cnode_ptr (Low_cnode_ptr + of_bl x * 0x10) of None \<Rightarrow> case High_cte High_cnode_ptr (Low_cnode_ptr + of_bl x * 0x10) of None \<Rightarrow> case Silc_cte Silc_cnode_ptr (Low_cnode_ptr + of_bl x * 0x10) of None \<Rightarrow> case Low_pdH Low_pd_ptr (Low_cnode_ptr + of_bl x * 0x10) of None \<Rightarrow> case High_pdH High_pd_ptr (Low_cnode_ptr + of_bl x * 0x10) of None \<Rightarrow> case Low_ptH Low_pt_ptr (Low_cnode_ptr + of_bl x * 0x10) of None \<Rightarrow> case High_ptH High_pt_ptr (Low_cnode_ptr + of_bl x * 0x10) of None \<Rightarrow> case global_pdH' init_global_pd (Low_cnode_ptr + of_bl x * 0x10) of None \<Rightarrow> None | Some x2 \<Rightarrow> Some x2 | Some x2 \<Rightarrow> Some x2 | Some x2 \<Rightarrow> Some x2 | Some x2 \<Rightarrow> Some x2 | Some x2 \<Rightarrow> Some x2 | Some x2 \<Rightarrow> Some x2 | Some x2 \<Rightarrow> Some x2 | Some x2 \<Rightarrow> Some x2) = Low_cte Low_cnode_ptr (Low_cnode_ptr + of_bl x * 0x10))))))))
 2. length x = 10 \<Longrightarrow> kh0H (High_cnode_ptr + of_bl x * 0x10) = High_cte High_cnode_ptr (High_cnode_ptr + of_bl x * 0x10)
 3. length x = 10 \<Longrightarrow> kh0H (Silc_cnode_ptr + of_bl x * 0x10) = Silc_cte Silc_cnode_ptr (Silc_cnode_ptr + of_bl x * 0x10)
 4. kh0H (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2)) = Low_pdH Low_pd_ptr (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2))
 5. kh0H (High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2)) = High_pdH High_pd_ptr (High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2))
 6. kh0H (init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2)) = global_pdH' init_global_pd (init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2))
 7. kh0H (Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2)) = Low_ptH Low_pt_ptr (Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2))
 8. kh0H (High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2)) = High_ptH High_pt_ptr (High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2))