kings-crown/FVELER_Isabelle huggingface dataset:
theory Invariants_AI

lemma valid_arch_cap_pspaceI:
  "\<lbrakk> valid_arch_cap acap s; kheap s = kheap s' \<rbrakk> \<Longrightarrow> valid_arch_cap acap s'" unfolding valid_arch_cap_def by (auto intro: obj_at_pspaceI split: arch_cap.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_arch_cap acap s; kheap s = kheap s'\<rbrakk> \<Longrightarrow> valid_arch_cap acap s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case acap of ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ASIDControlCap \<Rightarrow> True | PageCap dev r rghts sz mapdata \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base) | PageTableCap r mapdata \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | PageDirectoryCap r mapdata \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1); kheap s = kheap s'\<rbrakk> \<Longrightarrow> case acap of ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s' \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ASIDControlCap \<Rightarrow> True | PageCap dev r rghts sz mapdata \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s' else typ_at (AArch (AUserData sz)) r s') \<and> rghts \<in> valid_vm_rights \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base) | PageTableCap r mapdata \<Rightarrow> typ_at (AArch APageTable) r s' \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | PageDirectoryCap r mapdata \<Rightarrow> typ_at (AArch APageDirectory) r s' \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)
theory Invariants_AI

lemma valid_objs_pspaceI:
  "\<lbrakk> valid_objs s; kheap s = kheap s' \<rbrakk> \<Longrightarrow> valid_objs s'" unfolding valid_objs_def by (auto intro: valid_obj_pspaceI dest!: bspec [OF _ domI])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; kheap s = kheap s'\<rbrakk> \<Longrightarrow> valid_objs s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ptr\<in>dom $ kheap s. \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; kheap s = kheap s'\<rbrakk> \<Longrightarrow> \<forall>ptr\<in>dom $ kheap s'. \<exists>obj. kheap s' ptr = Some obj \<and> valid_obj ptr obj s'
theory Invariants_AI

lemma state_refs_of_pspaceI:
  "\<lbrakk> P (state_refs_of s); kheap s = kheap s' \<rbrakk> \<Longrightarrow> P (state_refs_of s')" unfolding state_refs_of_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P (state_refs_of s); kheap s = kheap s'\<rbrakk> \<Longrightarrow> P (state_refs_of s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P (\<lambda>x. case kheap s x of None \<Rightarrow> {} | Some ko \<Rightarrow> refs_of ko); kheap s = kheap s'\<rbrakk> \<Longrightarrow> P (\<lambda>x. case kheap s' x of None \<Rightarrow> {} | Some ko \<Rightarrow> refs_of ko)
theory Invariants_AI

lemma distinct_pspaceI:
  "pspace_distinct s \<Longrightarrow> kheap s = kheap s' \<Longrightarrow> pspace_distinct s'" by (simp add: pspace_distinct_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_distinct s; kheap s = kheap s'\<rbrakk> \<Longrightarrow> pspace_distinct s'
theory Invariants_AI

lemma iflive_pspaceI:
  "if_live_then_nonz_cap s \<Longrightarrow> kheap s = kheap s' \<Longrightarrow> if_live_then_nonz_cap s'" unfolding if_live_then_nonz_cap_def ex_nonz_cap_to_def by (fastforce simp: obj_at_def intro: cte_wp_at_pspaceI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>if_live_then_nonz_cap s; kheap s = kheap s'\<rbrakk> \<Longrightarrow> if_live_then_nonz_cap s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ptr. obj_at live ptr s \<longrightarrow> (\<exists>cref. cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) cref s); kheap s = kheap s'\<rbrakk> \<Longrightarrow> \<forall>ptr. obj_at live ptr s' \<longrightarrow> (\<exists>cref. cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) cref s')
theory Invariants_AI

lemma cte_wp_at_pspace:
  "kheap s = kheap s' \<Longrightarrow> cte_wp_at P p s = cte_wp_at P p s'" by (fastforce elim!: cte_wp_at_pspaceI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s = kheap s' \<Longrightarrow> cte_wp_at P p s = cte_wp_at P p s'
theory Invariants_AI

lemma caps_of_state_pspace:
  assumes x: "kheap s = kheap s'"
  shows      "caps_of_state s = caps_of_state s'" by (simp add: caps_of_state_cte_wp_at cte_wp_at_pspace [OF x] cong: if_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state s = caps_of_state s'
theory Invariants_AI

lemma ifunsafe_pspaceI:
  "if_unsafe_then_cap s \<Longrightarrow> kheap s = kheap s' \<Longrightarrow> interrupt_irq_node s = interrupt_irq_node s'
       \<Longrightarrow> if_unsafe_then_cap s'" unfolding if_unsafe_then_cap_def ex_cte_cap_wp_to_def apply (frule caps_of_state_pspace) by (auto simp: cte_wp_at_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>if_unsafe_then_cap s; kheap s = kheap s'; interrupt_irq_node s = interrupt_irq_node s'\<rbrakk> \<Longrightarrow> if_unsafe_then_cap s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>cref cap. caps_of_state s cref = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>crefa. cte_wp_at (\<lambda>c. appropriate_cte_cap cap c \<and> cref \<in> cte_refs c (interrupt_irq_node s)) crefa s); kheap s = kheap s'; interrupt_irq_node s = interrupt_irq_node s'\<rbrakk> \<Longrightarrow> \<forall>cref cap. caps_of_state s' cref = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>crefa. cte_wp_at (\<lambda>c. appropriate_cte_cap cap c \<and> cref \<in> cte_refs c (interrupt_irq_node s')) crefa s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>cref cap. caps_of_state s cref = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>crefa. cte_wp_at (\<lambda>c. appropriate_cte_cap cap c \<and> cref \<in> cte_refs c (interrupt_irq_node s)) crefa s); kheap s = kheap s'; interrupt_irq_node s = interrupt_irq_node s'; caps_of_state s = caps_of_state s'\<rbrakk> \<Longrightarrow> \<forall>cref cap. caps_of_state s' cref = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>crefa. cte_wp_at (\<lambda>c. appropriate_cte_cap cap c \<and> cref \<in> cte_refs c (interrupt_irq_node s')) crefa s')
theory Invariants_AI

lemma valid_idle_pspaceI:
  "valid_idle s \<Longrightarrow> \<lbrakk>kheap s = kheap s'; idle_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> valid_idle s'" unfolding valid_idle_def pred_tcb_at_def by (fastforce elim!: obj_at_pspaceI cte_wp_at_pspaceI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s = kheap s'; idle_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> valid_idle s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (case (itcb_state (tcb_to_itcb tcb), itcb_bound_notification (tcb_to_itcb tcb), itcb_arch (tcb_to_itcb tcb)) of (st, ntfn, arch) \<Rightarrow> idle st \<and> ntfn = None \<and> valid_arch_idle arch)) (idle_thread s) s \<and> idle_thread s = idle_thread_ptr; kheap s = kheap s'; idle_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (case (itcb_state (tcb_to_itcb tcb), itcb_bound_notification (tcb_to_itcb tcb), itcb_arch (tcb_to_itcb tcb)) of (st, ntfn, arch) \<Rightarrow> idle st \<and> ntfn = None \<and> valid_arch_idle arch)) (idle_thread s') s' \<and> idle_thread s' = idle_thread_ptr
theory Invariants_AI

lemma gen_obj_refs_Int:
  "(gen_obj_refs cap \<inter> gen_obj_refs cap' = {})
     = (obj_refs cap \<inter> obj_refs cap' = {}
            \<and> cap_irqs cap \<inter> cap_irqs cap' = {}
            \<and> arch_gen_refs cap \<inter> arch_gen_refs cap' = {})" by (simp add: gen_obj_refs_def Int_Un_distrib Int_Un_distrib2
                image_Int[symmetric] Int_image_empty)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (gen_obj_refs cap \<inter> gen_obj_refs cap' = {}) = (obj_refs cap \<inter> obj_refs cap' = {} \<and> cap_irqs cap \<inter> cap_irqs cap' = {} \<and> arch_gen_refs cap \<inter> arch_gen_refs cap' = {})
theory Invariants_AI

lemma is_final_cap'_def2:
  "is_final_cap' cap =
    (\<lambda>s. \<exists>cref. \<forall>cref'. cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c \<noteq> {}) cref' s
                  = (cref' = cref))" apply (rule ext) apply (auto simp: is_final_cap'_def cte_wp_at_def
                    set_eq_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_final_cap' cap = (\<lambda>s. \<exists>cref. \<forall>cref'. cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c \<noteq> {}) cref' s = (cref' = cref)) proof (prove)
goal (1 subgoal):
 1. \<And>s. is_final_cap' cap s = (\<exists>cref. \<forall>cref'. cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c \<noteq> {}) cref' s = (cref' = cref)) proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma zombies_final_pspaceI:
  assumes x: "zombies_final s"
      and y: "kheap s = kheap s'"
  shows      "zombies_final s'" using x unfolding zombies_final_def is_final_cap'_def2 by (simp only: cte_wp_at_pspace [OF y])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zombies_final s' proof (prove)
using this:
zombies_final s

goal (1 subgoal):
 1. zombies_final s' proof (prove)
using this:
\<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. \<exists>cref. \<forall>cref'. cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c \<noteq> {}) cref' s = (cref' = cref)) p s

goal (1 subgoal):
 1. \<forall>p. cte_wp_at is_zombie p s' \<longrightarrow> cte_wp_at (\<lambda>cap. \<exists>cref. \<forall>cref'. cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c \<noteq> {}) cref' s' = (cref' = cref)) p s'
theory Invariants_AI

lemma pspace_pspace_update:
  "kheap (kheap_update (\<lambda>a. ps) s) = ps" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap (s\<lparr>kheap := ps\<rparr>) = ps
theory Invariants_AI

lemma valid_pspace_eqI:
  "\<lbrakk> valid_pspace s; kheap s = kheap s' \<rbrakk> \<Longrightarrow> valid_pspace s'" unfolding valid_pspace_def by (auto simp: pspace_aligned_def
           intro: valid_objs_pspaceI state_refs_of_pspaceI state_hyp_refs_of_pspaceI
                  distinct_pspaceI iflive_pspaceI
                  ifunsafe_pspaceI zombies_final_pspaceI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace s; kheap s = kheap s'\<rbrakk> \<Longrightarrow> valid_pspace s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s))) s; kheap s = kheap s'\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s))) s'
theory Invariants_AI

lemma cte_wp_caps_of_lift:
  assumes c: "\<And>p P. cte_wp_at P p s = cte_wp_at P p s'"
  shows "caps_of_state s = caps_of_state s'" apply (rule ext) apply (case_tac "caps_of_state s' x") apply (rule classical) apply (clarsimp dest!: caps_of_state_cteD simp add: c) apply (simp add: cte_wp_at_caps_of_state) apply clarsimp apply (clarsimp dest!: caps_of_state_cteD simp add: c [symmetric]) apply (simp add: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state s = caps_of_state s' proof (prove)
goal (1 subgoal):
 1. \<And>x. caps_of_state s x = caps_of_state s' x proof (prove)
goal (2 subgoals):
 1. \<And>x. caps_of_state s' x = None \<Longrightarrow> caps_of_state s x = caps_of_state s' x
 2. \<And>x a. caps_of_state s' x = Some a \<Longrightarrow> caps_of_state s x = caps_of_state s' x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>caps_of_state s' x = None; caps_of_state s x \<noteq> caps_of_state s' x\<rbrakk> \<Longrightarrow> caps_of_state s x = caps_of_state s' x
 2. \<And>x a. caps_of_state s' x = Some a \<Longrightarrow> caps_of_state s x = caps_of_state s' x proof (prove)
goal (2 subgoals):
 1. \<And>a b y. \<lbrakk>caps_of_state s' (a, b) = None; cte_wp_at ((=) y) (a, b) s'\<rbrakk> \<Longrightarrow> caps_of_state s (a, b) = None
 2. \<And>x a. caps_of_state s' x = Some a \<Longrightarrow> caps_of_state s x = caps_of_state s' x proof (prove)
goal (1 subgoal):
 1. \<And>x a. caps_of_state s' x = Some a \<Longrightarrow> caps_of_state s x = caps_of_state s' x proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. caps_of_state s' (a, b) = Some aa \<Longrightarrow> caps_of_state s (a, b) = Some aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. cte_wp_at ((=) aa) (a, b) s \<Longrightarrow> caps_of_state s (a, b) = Some aa proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma ex_cte_cap_to_pres:
  assumes x: "\<And>P p. \<lbrace>cte_wp_at P p\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace>"
  assumes irq: "\<And>P. \<lbrace>\<lambda>s. P (interrupt_irq_node s)\<rbrace> f \<lbrace>\<lambda>rv s. P (interrupt_irq_node s)\<rbrace>"
  shows      "\<lbrace>ex_cte_cap_wp_to P p\<rbrace> f \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p\<rbrace>" by (simp add: ex_cte_cap_wp_to_def,
      wp hoare_vcg_ex_lift hoare_use_eq[where f=interrupt_irq_node, OF irq, OF x])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to P p\<rbrace> f \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p\<rbrace>
theory Invariants_AI

lemma set_object_at_obj1:
  "P obj \<Longrightarrow> \<lbrace> obj_at P p \<rbrace> set_object r obj \<lbrace> \<lambda>rv. obj_at P p \<rbrace>" by (clarsimp simp: valid_def in_monad obj_at_def set_object_def get_object_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P obj \<Longrightarrow> \<lbrace>obj_at P p\<rbrace> set_object r obj \<lbrace>\<lambda>rv. obj_at P p\<rbrace>
theory Invariants_AI

lemma set_object_at_obj2:
  "(\<And>ko. Q ko \<Longrightarrow> \<not>P ko) \<Longrightarrow>
  \<lbrace> obj_at P p and obj_at Q r \<rbrace> set_object r obj \<lbrace> \<lambda>rv. obj_at P p \<rbrace>" by (clarsimp simp: valid_def in_monad obj_at_def set_object_def get_object_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>ko. Q ko \<Longrightarrow> \<not> P ko) \<Longrightarrow> \<lbrace>obj_at P p and obj_at Q r\<rbrace> set_object r obj \<lbrace>\<lambda>rv. obj_at P p\<rbrace>
theory Invariants_AI

lemma test:
  "\<lbrace> ep_at p and tcb_at r \<rbrace> set_object r obj \<lbrace> \<lambda>rv. ep_at p \<rbrace>" apply (rule set_object_at_obj2) apply (clarsimp simp: is_obj_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ep_at p and tcb_at r\<rbrace> set_object r obj \<lbrace>\<lambda>rv. ep_at p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ko. is_tcb ko \<Longrightarrow> \<not> is_ep ko proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma valid_pspaceI [intro]:
  "\<lbrakk> valid_objs s; pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s);
     pspace_distinct s; if_live_then_nonz_cap s; zombies_final s \<rbrakk>
     \<Longrightarrow> valid_pspace s" unfolding valid_pspace_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s\<rbrakk> \<Longrightarrow> valid_pspace s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s))) s
theory Invariants_AI

lemma valid_pspaceE [elim?]:
  assumes vp: "valid_pspace s"
  and     rl: "\<lbrakk> valid_objs s; pspace_aligned s;
                 sym_refs (state_refs_of s);  sym_refs (state_hyp_refs_of s);
                 pspace_distinct s; if_live_then_nonz_cap s;
                 zombies_final s \<rbrakk> \<Longrightarrow> R"
  shows    R using vp unfolding valid_pspace_def by (auto intro: rl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R proof (prove)
using this:
valid_pspace s

goal (1 subgoal):
 1. R proof (prove)
using this:
(valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s))) s

goal (1 subgoal):
 1. R
theory Invariants_AI

lemma valid_objs_valid_cs [dest?]:
  assumes vp: "valid_objs s"
  and    ran: "CNode sz ct \<in> ran (kheap s)"
  shows  "valid_cs sz ct s" using vp ran unfolding valid_objs_def by (auto simp: valid_obj_def ran_def dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_cs sz ct s proof (prove)
using this:
valid_objs s
CNode sz ct \<in> ran (kheap s)

goal (1 subgoal):
 1. valid_cs sz ct s proof (prove)
using this:
\<forall>ptr\<in>dom $ kheap s. \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s
CNode sz ct \<in> ran (kheap s)

goal (1 subgoal):
 1. valid_cs sz ct s
theory Invariants_AI

lemma valid_pspace_valid_cs [dest?]:
  assumes vp: "valid_pspace s"
  and    ran: "CNode sz ct \<in> ran (kheap s)"
  shows  "valid_cs sz ct s" using vp by (rule valid_pspaceE)
     (simp add: valid_objs_valid_cs ran)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_cs sz ct s proof (prove)
using this:
valid_pspace s

goal (1 subgoal):
 1. valid_cs sz ct s
theory Invariants_AI

lemma valid_pspace_aligned:
  assumes vp: "valid_pspace s"
  and    lup: "kheap s addr = Some ko"
  shows  "is_aligned addr (obj_bits ko)" using vp apply (rule valid_pspaceE) apply (unfold pspace_aligned_def) apply (drule bspec [OF _ domI]) apply (rule lup) apply (simp add: lup) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned addr (obj_bits ko) proof (prove)
using this:
valid_pspace s

goal (1 subgoal):
 1. is_aligned addr (obj_bits ko) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s\<rbrakk> \<Longrightarrow> is_aligned addr (obj_bits ko) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; \<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s\<rbrakk> \<Longrightarrow> is_aligned addr (obj_bits ko) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s\<rbrakk> \<Longrightarrow> kheap s ?x2 = Some ?b2
 2. \<lbrakk>valid_objs s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; is_aligned ?x2 (obj_bits (the (kheap s ?x2)))\<rbrakk> \<Longrightarrow> is_aligned addr (obj_bits ko) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; is_aligned addr (obj_bits (the (kheap s addr)))\<rbrakk> \<Longrightarrow> is_aligned addr (obj_bits ko) proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma valid_pspace_valid_cs_size [intro?]:
  assumes ran: "CNode sz cs \<in> ran (kheap s)"
  and      vp: "valid_pspace s"
  shows  "valid_cs_size sz cs" using valid_pspace_valid_cs [OF vp ran] unfolding valid_cs_def ..

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_cs_size sz cs proof (prove)
using this:
valid_cs sz cs s

goal (1 subgoal):
 1. valid_cs_size sz cs proof (prove)
using this:
(\<forall>cap\<in>ran cs. s \<turnstile> cap) \<and> valid_cs_size sz cs

goal (1 subgoal):
 1. valid_cs_size sz cs
theory Invariants_AI

lemma valid_objs_valid_cs_size [intro?]:
  assumes ran: "CNode sz cs \<in> ran (kheap s)"
  and      vp: "valid_objs s"
  shows  "valid_cs_size sz cs" using valid_objs_valid_cs [OF vp ran] unfolding valid_cs_def ..

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_cs_size sz cs proof (prove)
using this:
valid_cs sz cs s

goal (1 subgoal):
 1. valid_cs_size sz cs proof (prove)
using this:
(\<forall>cap\<in>ran cs. s \<turnstile> cap) \<and> valid_cs_size sz cs

goal (1 subgoal):
 1. valid_cs_size sz cs
theory Invariants_AI

lemma valid_cs_size_objsI [intro?]:
  "\<lbrakk> valid_objs s; kheap s r = Some (CNode sz ps) \<rbrakk>
  \<Longrightarrow> valid_cs_size sz ps" by (drule ranI, erule valid_objs_valid_cs_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; kheap s r = Some (CNode sz ps)\<rbrakk> \<Longrightarrow> valid_cs_size sz ps
theory Invariants_AI

lemma valid_cs_sizeI [intro?]:
  "\<lbrakk> valid_pspace s; kheap s r = Some (CNode sz ps) \<rbrakk>
  \<Longrightarrow> valid_cs_size sz ps" by (drule ranI, erule valid_pspace_valid_cs_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace s; kheap s r = Some (CNode sz ps)\<rbrakk> \<Longrightarrow> valid_cs_size sz ps
theory Invariants_AI

lemma wf_cs_insert:
  "\<lbrakk> well_formed_cnode_n sz cs; cs ref \<noteq> None \<rbrakk> \<Longrightarrow> well_formed_cnode_n sz (cs (ref \<mapsto> val))" apply (clarsimp simp: well_formed_cnode_n_def) apply (subst insert_absorb, simp_all) apply (drule domI, fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_formed_cnode_n sz cs; cs ref \<noteq> None\<rbrakk> \<Longrightarrow> well_formed_cnode_n sz (cs(ref \<mapsto> val)) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>dom cs = {x. length x = sz}; cs ref = Some y\<rbrakk> \<Longrightarrow> insert ref {x. length x = sz} = {x. length x = sz} proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>dom cs = {x. length x = sz}; cs ref = Some y\<rbrakk> \<Longrightarrow> length ref = sz proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma obj_bits_CNode:
  "\<lbrakk> valid_cs_size sz ps; ps cref = Some cap \<rbrakk> \<Longrightarrow>
  obj_bits (CNode sz ps) = cte_level_bits + length cref" by (auto simp: valid_cs_size_def well_formed_cnode_n_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cs_size sz ps; ps cref = Some cap\<rbrakk> \<Longrightarrow> obj_bits (CNode sz ps) = cte_level_bits + length cref
theory Invariants_AI

lemma obj_bits_CNode':
  "\<lbrakk> valid_cs_size sz ps; cref \<in> dom ps \<rbrakk> \<Longrightarrow>
  obj_bits (CNode sz ps) = cte_level_bits + length cref" by (drule domD, erule exE, rule obj_bits_CNode)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cs_size sz ps; cref \<in> dom ps\<rbrakk> \<Longrightarrow> obj_bits (CNode sz ps) = cte_level_bits + length cref