kings-crown/FVELER_Isabelle huggingface dataset:
theory ADT_H

lemma after_in_list_next_reachable:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "after_in_list (t p) slot = Some slot2 \<Longrightarrow> m' \<turnstile> (cte_map slot) \<leadsto>\<^sup>* (cte_map slot2)" apply (subgoal_tac "m slot = Some p") apply (rule next_sib_reachable) apply (simp add: next_sib_def)+ apply (drule after_in_list_in_list') apply (insert valid_list_2) apply (simp add: valid_list_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. after_in_list (t p) slot = Some slot2 \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto>\<^sup>* cte_map slot2 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>after_in_list (t p) slot = Some slot2; m slot = Some p\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto>\<^sup>* cte_map slot2
 2. after_in_list (t p) slot = Some slot2 \<Longrightarrow> m slot = Some p proof (prove)
goal (3 subgoals):
 1. \<lbrakk>after_in_list (t p) slot = Some slot2; m slot = Some p\<rbrakk> \<Longrightarrow> next_sib slot t m = Some slot2
 2. \<lbrakk>after_in_list (t p) slot = Some slot2; m slot = Some p\<rbrakk> \<Longrightarrow> m slot = Some ?p1
 3. after_in_list (t p) slot = Some slot2 \<Longrightarrow> m slot = Some p proof (prove)
goal (1 subgoal):
 1. after_in_list (t p) slot = Some slot2 \<Longrightarrow> m slot = Some p proof (prove)
goal (1 subgoal):
 1. slot \<in> set (t p) \<Longrightarrow> m slot = Some p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot \<in> set (t p); valid_list_2 t m\<rbrakk> \<Longrightarrow> m slot = Some p proof (prove)
goal:
No subgoals!
theory ADT_H

lemma sorted_lists:
   "psorted (t p)" apply (rule after_order_sorted) apply (rule after_in_list_next_reachable) apply simp apply (insert assms') apply (simp add: valid_list_def t_def del: split_paired_All) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. psorted (t p) proof (prove)
goal (2 subgoals):
 1. \<And>x y. after_in_list (t p) x = Some y \<Longrightarrow> m' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y
 2. distinct (t p) proof (prove)
goal (2 subgoals):
 1. \<And>x y. after_in_list (t p) x = Some y \<Longrightarrow> after_in_list (t (?p3 x y)) x = Some y
 2. distinct (t p) proof (prove)
goal (1 subgoal):
 1. distinct (t p) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned s; pspace_distinct s; pspace_aligned' s'; pspace_distinct' s'; valid_objs s; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> distinct (t p) proof (prove)
goal:
No subgoals!
theory ADT_H

lemma sort_cdt_list_correct:
  "sort_cdt_list m m' = t" apply (rule ext) apply (simp add: sort_cdt_list_def) apply (rule the1_equality) apply (rule ex1_sorted_cdt) apply (simp add: sorted_lists) apply (insert assms') apply (simp add: valid_list_def t_def m_def del: split_paired_All) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sort_cdt_list m m' = t proof (prove)
goal (1 subgoal):
 1. \<And>x. sort_cdt_list m m' x = t x proof (prove)
goal (1 subgoal):
 1. \<And>x. (THE xs. set xs = {c. m c = Some x} \<and> psorted xs \<and> distinct xs) = t x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>!xs. set xs = {c. m c = Some x} \<and> psorted xs \<and> distinct xs
 2. \<And>x. set (t x) = {c. m c = Some x} \<and> psorted (t x) \<and> distinct (t x) proof (prove)
goal (1 subgoal):
 1. \<And>x. set (t x) = {c. m c = Some x} \<and> psorted (t x) \<and> distinct (t x) proof (prove)
goal (1 subgoal):
 1. \<And>x. set (t x) = {c. m c = Some x} \<and> distinct (t x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pspace_aligned s; pspace_distinct s; pspace_aligned' s'; pspace_distinct' s'; valid_objs s; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> set (t x) = {c. m c = Some x} \<and> distinct (t x) proof (prove)
goal:
No subgoals!
theory ADT_H

lemma no_loops_sym_eq: "no_loops m \<Longrightarrow> m \<turnstile> a \<leadsto>\<^sup>* b \<Longrightarrow> m \<turnstile> b \<leadsto>\<^sup>* a \<Longrightarrow> a = b" apply (rule ccontr) apply (subgoal_tac "m \<turnstile> a \<leadsto>\<^sup>+ a") apply (simp add: no_loops_def) apply (simp add: rtrancl_eq_or_trancl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_loops m; m \<turnstile> a \<leadsto>\<^sup>* b; m \<turnstile> b \<leadsto>\<^sup>* a\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_loops m; m \<turnstile> a \<leadsto>\<^sup>* b; m \<turnstile> b \<leadsto>\<^sup>* a; a \<noteq> b\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_loops m; m \<turnstile> a \<leadsto>\<^sup>* b; m \<turnstile> b \<leadsto>\<^sup>* a; a \<noteq> b; m \<turnstile> a \<leadsto>\<^sup>+ a\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>no_loops m; m \<turnstile> a \<leadsto>\<^sup>* b; m \<turnstile> b \<leadsto>\<^sup>* a; a \<noteq> b\<rbrakk> \<Longrightarrow> m \<turnstile> a \<leadsto>\<^sup>+ a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_loops m; m \<turnstile> a \<leadsto>\<^sup>* b; m \<turnstile> b \<leadsto>\<^sup>* a; a \<noteq> b\<rbrakk> \<Longrightarrow> m \<turnstile> a \<leadsto>\<^sup>+ a proof (prove)
goal:
No subgoals!
theory ADT_H

lemma substring_next: "m \<turnstile> a \<leadsto>\<^sup>* b \<Longrightarrow> m \<turnstile> a \<leadsto>\<^sup>* c \<Longrightarrow> m \<turnstile> b \<leadsto>\<^sup>* c \<or> m \<turnstile> c \<leadsto>\<^sup>* b" apply (rule single_valued_confluent) apply (rule mdb_next_single_valued) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>* b; m \<turnstile> a \<leadsto>\<^sup>* c\<rbrakk> \<Longrightarrow> m \<turnstile> b \<leadsto>\<^sup>* c \<or> m \<turnstile> c \<leadsto>\<^sup>* b proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>* b; m \<turnstile> a \<leadsto>\<^sup>* c\<rbrakk> \<Longrightarrow> single_valued (mdb_next_rel m)
 2. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>* b; m \<turnstile> a \<leadsto>\<^sup>* c\<rbrakk> \<Longrightarrow> m \<turnstile> ?x \<leadsto>\<^sup>* b
 3. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>* b; m \<turnstile> a \<leadsto>\<^sup>* c\<rbrakk> \<Longrightarrow> m \<turnstile> ?x \<leadsto>\<^sup>* c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>* b; m \<turnstile> a \<leadsto>\<^sup>* c\<rbrakk> \<Longrightarrow> m \<turnstile> ?x \<leadsto>\<^sup>* b
 2. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>* b; m \<turnstile> a \<leadsto>\<^sup>* c\<rbrakk> \<Longrightarrow> m \<turnstile> ?x \<leadsto>\<^sup>* c proof (prove)
goal:
No subgoals!
theory ADT_H

lemma ancestor_comparable: "\<lbrakk>m \<turnstile> a \<rightarrow> x; m \<turnstile> a \<rightarrow> y\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>* y \<or> m \<turnstile> y \<leadsto>\<^sup>* x" apply (rule substring_next) apply (erule subtree_mdb_next[THEN trancl_into_rtrancl])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> a \<rightarrow> x; m \<turnstile> a \<rightarrow> y\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>* y \<or> m \<turnstile> y \<leadsto>\<^sup>* x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> a \<rightarrow> x; m \<turnstile> a \<rightarrow> y\<rbrakk> \<Longrightarrow> m \<turnstile> ?a \<leadsto>\<^sup>* x
 2. \<lbrakk>m \<turnstile> a \<rightarrow> x; m \<turnstile> a \<rightarrow> y\<rbrakk> \<Longrightarrow> m \<turnstile> ?a \<leadsto>\<^sup>* y proof (prove)
goal:
No subgoals!
theory ADT_H

lemma valid_mdb'_no_loops: "valid_mdb' s \<Longrightarrow> no_loops (ctes_of s)" apply (rule mdb_chain_0_no_loops) apply (simp add: valid_mdb'_def valid_mdb_ctes_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb' s \<Longrightarrow> no_loops (ctes_of s) proof (prove)
goal (2 subgoals):
 1. valid_mdb' s \<Longrightarrow> mdb_chain_0 (ctes_of s)
 2. valid_mdb' s \<Longrightarrow> no_0 (ctes_of s) proof (prove)
goal:
No subgoals!
theory ADT_H

lemma absInterruptIRQNode_correct:
  "interrupt_state_relation (interrupt_irq_node s) (interrupt_states s)
      (ksInterruptState s') \<Longrightarrow>
   absInterruptIRQNode (ksInterruptState s') = interrupt_irq_node s" by (rule ext) (clarsimp simp add: absInterruptIRQNode_def
                                     interrupt_state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s') \<Longrightarrow> absInterruptIRQNode (ksInterruptState s') = interrupt_irq_node s
theory ADT_H

lemma absInterruptStates_correct:
  "interrupt_state_relation (interrupt_irq_node s) (interrupt_states s)
      (ksInterruptState s') \<Longrightarrow>
   absInterruptStates (ksInterruptState s') = interrupt_states s" apply (rule ext) apply (clarsimp simp add: absInterruptStates_def IRQStateMap_def
         interrupt_state_relation_def irq_state_relation_def) apply (erule_tac x=x in allE)+ apply (clarsimp split: irq_state.splits irqstate.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s') \<Longrightarrow> absInterruptStates (ksInterruptState s') = interrupt_states s proof (prove)
goal (1 subgoal):
 1. \<And>x. interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s') \<Longrightarrow> absInterruptStates (ksInterruptState s') x = interrupt_states s x proof (prove)
goal (1 subgoal):
 1. \<And>x node irqs'. \<lbrakk>ksInterruptState s' = InterruptState node irqs'; \<forall>irq. interrupt_irq_node s irq = node + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits); \<forall>irq. case interrupt_states s irq of irq_state.IRQInactive \<Rightarrow> case irqs' irq of irqstate.IRQInactive \<Rightarrow> True | _ \<Rightarrow> False | irq_state.IRQSignal \<Rightarrow> case irqs' irq of irqstate.IRQSignal \<Rightarrow> True | _ \<Rightarrow> False | irq_state.IRQTimer \<Rightarrow> case irqs' irq of irqstate.IRQTimer \<Rightarrow> True | _ \<Rightarrow> False | irq_state.IRQReserved \<Rightarrow> False\<rbrakk> \<Longrightarrow> (case irqs' x of irqstate.IRQInactive \<Rightarrow> irq_state.IRQInactive | irqstate.IRQSignal \<Rightarrow> irq_state.IRQSignal | irqstate.IRQTimer \<Rightarrow> irq_state.IRQTimer | irqstate.IRQReserved \<Rightarrow> irq_state.IRQReserved) = interrupt_states s x proof (prove)
goal (1 subgoal):
 1. \<And>x node irqs'. \<lbrakk>ksInterruptState s' = InterruptState node irqs'; interrupt_irq_node s x = node + (UCAST(10 \<rightarrow> 32) x << cte_level_bits); case interrupt_states s x of irq_state.IRQInactive \<Rightarrow> case irqs' x of irqstate.IRQInactive \<Rightarrow> True | _ \<Rightarrow> False | irq_state.IRQSignal \<Rightarrow> case irqs' x of irqstate.IRQSignal \<Rightarrow> True | _ \<Rightarrow> False | irq_state.IRQTimer \<Rightarrow> case irqs' x of irqstate.IRQTimer \<Rightarrow> True | _ \<Rightarrow> False | irq_state.IRQReserved \<Rightarrow> False\<rbrakk> \<Longrightarrow> (case irqs' x of irqstate.IRQInactive \<Rightarrow> irq_state.IRQInactive | irqstate.IRQSignal \<Rightarrow> irq_state.IRQSignal | irqstate.IRQTimer \<Rightarrow> irq_state.IRQTimer | irqstate.IRQReserved \<Rightarrow> irq_state.IRQReserved) = interrupt_states s x proof (prove)
goal:
No subgoals!
theory ADT_H

lemma absArchState_correct:
assumes rel:
  "(s,s') \<in> state_relation"
shows
  "absArchState (ksArchState s') = arch_state s" apply (subgoal_tac "(arch_state s, ksArchState s') \<in> arch_state_relation") prefer 2 using rel apply (simp add: state_relation_def) apply (clarsimp simp add: arch_state_relation_def) by (clarsimp simp add: absArchState_def
             split: ARM_H.kernel_state.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. absArchState (ksArchState s') = arch_state s proof (prove)
goal (2 subgoals):
 1. (arch_state s, ksArchState s') \<in> arch_state_relation \<Longrightarrow> absArchState (ksArchState s') = arch_state s
 2. (arch_state s, ksArchState s') \<in> arch_state_relation proof (prove)
goal (2 subgoals):
 1. (arch_state s, ksArchState s') \<in> arch_state_relation
 2. (arch_state s, ksArchState s') \<in> arch_state_relation \<Longrightarrow> absArchState (ksArchState s') = arch_state s proof (prove)
using this:
(s, s') \<in> state_relation

goal (2 subgoals):
 1. (arch_state s, ksArchState s') \<in> arch_state_relation
 2. (arch_state s, ksArchState s') \<in> arch_state_relation \<Longrightarrow> absArchState (ksArchState s') = arch_state s proof (prove)
goal (1 subgoal):
 1. (arch_state s, ksArchState s') \<in> arch_state_relation \<Longrightarrow> absArchState (ksArchState s') = arch_state s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>asid_table s = armKSASIDTable (ksArchState s') \<circ> UCAST(7 \<rightarrow> 32); arm_global_pd (arch_state s) = armKSGlobalPD (ksArchState s'); arm_hwasid_table (arch_state s) = armKSHWASIDTable (ksArchState s'); arm_global_pts (arch_state s) = armKSGlobalPTs (ksArchState s'); arm_next_asid (arch_state s) = armKSNextASID (ksArchState s'); arm_asid_map (arch_state s) = armKSASIDMap (ksArchState s'); arm_kernel_vspace (arch_state s) = armKSKernelVSpace (ksArchState s')\<rbrakk> \<Longrightarrow> absArchState (ksArchState s') = arch_state s
theory ADT_H

lemma absSchedulerAction_correct:
  assumes act_rel: "sched_act_relation action action'"
  shows " absSchedulerAction action' = action" using act_rel by (cases action, simp_all add: absSchedulerAction_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. absSchedulerAction action' = action proof (prove)
using this:
sched_act_relation action action'

goal (1 subgoal):
 1. absSchedulerAction action' = action
theory ADT_H

lemma invs_valid_ioc[elim!]: "invs s \<Longrightarrow> valid_ioc s" by (clarsimp simp add: invs_def valid_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> valid_ioc s
theory ArchKernelInit_AI

lemma [simp]: "is_aligned (0x1000 :: word32) 9" by (simp add: is_aligned_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned 0x1000 9
theory ArchKernelInit_AI

lemma [simp]: "is_aligned (0x2000 :: word32) 9" by (simp add: is_aligned_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned 0x2000 9
theory ArchKernelInit_AI

lemma [simp]: "is_tcb (TCB t)" by (simp add: is_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_tcb (TCB t)
theory ArchKernelInit_AI

lemma [simp]: "ran (empty_cnode n) = {Structures_A.NullCap}" apply (auto simp: ran_def empty_cnode_def) apply (rule_tac x="replicate n False" in exI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ran (empty_cnode n) = {NullCap} proof (prove)
goal (1 subgoal):
 1. \<exists>a. length a = n proof (prove)
goal (1 subgoal):
 1. length (replicate n False) = n proof (prove)
goal:
No subgoals!
theory ArchKernelInit_AI

lemma empty_cnode_apply[simp]:
  "(empty_cnode n xs = Some cap) = (length xs = n \<and> cap = Structures_A.NullCap)" by (auto simp add: empty_cnode_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (empty_cnode n xs = Some cap) = (length xs = n \<and> cap = NullCap)
theory ArchKernelInit_AI

lemma valid_cs_size_empty[simp]:
  "valid_cs_size n (empty_cnode n) = (n < word_bits - cte_level_bits)" apply (simp add: valid_cs_size_def) apply (insert wf_empty_bits [of n]) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_cs_size n (empty_cnode n) = (n < word_bits - cte_level_bits) proof (prove)
goal (1 subgoal):
 1. (n < word_bits - cte_level_bits \<and> well_formed_cnode_n n (empty_cnode n)) = (n < word_bits - cte_level_bits) proof (prove)
goal (1 subgoal):
 1. well_formed_cnode_n n (empty_cnode n) \<Longrightarrow> (n < word_bits - cte_level_bits \<and> well_formed_cnode_n n (empty_cnode n)) = (n < word_bits - cte_level_bits) proof (prove)
goal:
No subgoals!
theory ArchKernelInit_AI

lemma init_cdt [simp]:
  "cdt init_A_st = init_cdt" by (simp add: state_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdt init_A_st = init_cdt
theory ArchKernelInit_AI

lemma mdp_parent_empty [simp]:
  "\<not>Map.empty \<Turnstile> x \<rightarrow> y" apply clarsimp apply (drule tranclD) apply (clarsimp simp: cdt_parent_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, y) \<notin> (cdt_parent_rel (\<lambda>x. None))\<^sup>+ proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. None) \<Turnstile> x \<rightarrow> y \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<exists>z. (\<lambda>x. None) \<Turnstile> x \<leadsto> z \<and> (\<lambda>x. None) \<Turnstile> z \<rightarrow>* y \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ArchKernelInit_AI

lemma descendants_empty [simp]:
  "descendants_of x Map.empty = {}" by (clarsimp simp: descendants_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of x (\<lambda>x. None) = {}
theory ArchKernelInit_AI

lemma reply_Null [simp]: "\<not>is_reply_cap NullCap" by (simp add: is_reply_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_reply_cap NullCap
theory ArchKernelInit_AI

lemma mask_pde_mapping_bits:
  "(mask 20 :: machine_word) = 2^pde_mapping_bits - 1" by (simp add: mask_def pde_mapping_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mask 20 = 2 ^ pde_mapping_bits - 1
theory ArchKernelInit_AI

lemma init_irq_ptrs_eq:
  "((ucast (irq :: irq) << cte_level_bits)
        = (ucast (irq' :: irq) << cte_level_bits :: word32))
      = (irq = irq')" apply safe apply (rule ccontr) apply (erule_tac bnd="ucast (max_word :: irq) + 1"
              in shift_distinct_helper[rotated 3],
         safe intro!: plus_one_helper2;
         simp add: ucast_le_ucast_10_32 up_ucast_inj_eq cte_level_bits_def minus_1_eq_mask
                   ucast_leq_mask;
         simp add: mask_eq_exp_minus_1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (UCAST(10 \<rightarrow> 32) irq << cte_level_bits = UCAST(10 \<rightarrow> 32) irq' << cte_level_bits) = (irq = irq') proof (prove)
goal (1 subgoal):
 1. UCAST(10 \<rightarrow> 32) irq << cte_level_bits = UCAST(10 \<rightarrow> 32) irq' << cte_level_bits \<Longrightarrow> irq = irq' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>UCAST(10 \<rightarrow> 32) irq << cte_level_bits = UCAST(10 \<rightarrow> 32) irq' << cte_level_bits; irq \<noteq> irq'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ArchKernelInit_AI

lemma pspace_aligned_init_A:
  "pspace_aligned init_A_st" apply (clarsimp simp: pspace_aligned_def state_defs wf_obj_bits [OF wf_empty_bits]
                        dom_if_Some cte_level_bits_def) apply (safe intro!: aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl],
           simp_all add: is_aligned_def word_bits_def kernel_base_def)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_aligned init_A_st proof (prove)
goal (1 subgoal):
 1. is_aligned (kernel_base + 0x60000) 14 \<and> is_aligned (kernel_base + 0x5000) 12 \<and> is_aligned (kernel_base + 0x1000) 9 \<and> (\<forall>x. (x = kernel_base + 0x1000 \<longrightarrow> (\<exists>irq. 0x7000 + (UCAST(10 \<rightarrow> 32) irq << 4) = 0) \<longrightarrow> is_aligned (kernel_base + 0x1000) 9) \<and> (x \<noteq> kernel_base + 0x1000 \<longrightarrow> (x = kernel_base + 0x5000 \<longrightarrow> (\<exists>irq. 0x3000 + (UCAST(10 \<rightarrow> 32) irq << 4) = 0) \<longrightarrow> is_aligned (kernel_base + 0x5000) 12) \<and> (x \<noteq> kernel_base + 0x5000 \<longrightarrow> (x = kernel_base + 0x60000 \<longrightarrow> (\<exists>irq. UCAST(10 \<rightarrow> 32) irq << 4 = 0x58000) \<longrightarrow> is_aligned (kernel_base + 0x60000) 14) \<and> (x \<noteq> kernel_base + 0x60000 \<longrightarrow> (\<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << 4) = x) \<longrightarrow> is_aligned x 4)))) proof (prove)
goal:
No subgoals!
theory ArchKernelInit_AI

lemma caps_of_state_init_A_st_Null:
  "caps_of_state (init_A_st::'z::state_ext state) x
     = (if cte_at x (init_A_st::'z::state_ext state) then Some cap.NullCap else None)" apply (subgoal_tac "\<not> cte_wp_at ((\<noteq>) cap.NullCap) x init_A_st") apply (auto simp add: cte_wp_at_caps_of_state)[1] apply (clarsimp, erule cte_wp_atE) apply (auto simp add: state_defs tcb_cap_cases_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state init_A_st x = (if cte_wp_at (\<lambda>_. True) x init_A_st then Some NullCap else None) proof (prove)
goal (2 subgoals):
 1. \<not> cte_wp_at ((\<noteq>) NullCap) x init_A_st \<Longrightarrow> caps_of_state init_A_st x = (if cte_wp_at (\<lambda>_. True) x init_A_st then Some NullCap else None)
 2. \<not> cte_wp_at ((\<noteq>) NullCap) x init_A_st proof (prove)
goal (1 subgoal):
 1. \<not> cte_wp_at ((\<noteq>) NullCap) x init_A_st proof (prove)
goal (2 subgoals):
 1. \<And>sz fun cte. \<lbrakk>kheap init_A_st (fst x) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd x) = Some cte; NullCap \<noteq> cte\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb getF setF restr. \<lbrakk>kheap init_A_st (fst x) = Some (TCB tcb); tcb_cap_cases (snd x) = Some (getF, setF, restr); NullCap \<noteq> getF tcb\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ArchKernelInit_AI

lemma cte_wp_at_init_A_st_Null:
  "cte_wp_at P p init_A_st \<Longrightarrow> P cap.NullCap" apply (subst(asm) cte_wp_at_caps_of_state) apply (simp add:caps_of_state_init_A_st_Null split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at P p init_A_st \<Longrightarrow> P NullCap proof (prove)
goal (1 subgoal):
 1. \<exists>cap. caps_of_state init_A_st p = Some cap \<and> P cap \<Longrightarrow> P NullCap proof (prove)
goal:
No subgoals!
theory ArchKernelInit_AI

lemma pspace_respects_device_region_init[simp]:
  "pspace_respects_device_region init_A_st" apply (clarsimp simp: pspace_respects_device_region_def init_A_st_def init_machine_state_def device_mem_def
                         in_device_frame_def obj_at_def init_kheap_def a_type_def) apply (rule ext) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_respects_device_region init_A_st proof (prove)
goal (1 subgoal):
 1. (\<lambda>p. if \<exists>sz. (\<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> p && ~~ mask (pageBitsForSize sz)) \<and> (\<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = p && ~~ mask (pageBitsForSize sz)) then Some p else None) = (\<lambda>x. None) proof (prove)
goal (1 subgoal):
 1. \<And>p. (if \<exists>sz. (\<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> p && ~~ mask (pageBitsForSize sz)) \<and> (\<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = p && ~~ mask (pageBitsForSize sz)) then Some p else None) = None proof (prove)
goal:
No subgoals!