kings-crown/FVELER_Isabelle huggingface dataset:
theory Invariants_H

lemma valid_arch_obj'_pspaceI:
  "valid_arch_obj' obj s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> valid_arch_obj' obj s'" apply (cases obj; simp) apply (rename_tac asidpool) apply (case_tac asidpool,
           auto simp: page_directory_at'_def intro: typ_at'_pspaceI[rotated])[1] apply (rename_tac pte) apply (case_tac pte; simp add: valid_mapping'_def) apply (rename_tac pde) apply (case_tac pde;
         auto simp: page_table_at'_def valid_mapping'_def
             intro: typ_at'_pspaceI[rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_arch_obj' obj s; ksPSpace s = ksPSpace s'\<rbrakk> \<Longrightarrow> valid_arch_obj' obj s' proof (prove)
goal (3 subgoals):
 1. \<And>x1. \<lbrakk>valid_asid_pool' x1 s; ksPSpace s = ksPSpace s'; obj = KOASIDPool x1\<rbrakk> \<Longrightarrow> valid_asid_pool' x1 s'
 2. \<And>x2. \<lbrakk>valid_pte' x2 s; ksPSpace s = ksPSpace s'; obj = KOPTE x2\<rbrakk> \<Longrightarrow> valid_pte' x2 s'
 3. \<And>x3. \<lbrakk>valid_pde' x3 s; ksPSpace s = ksPSpace s'; obj = KOPDE x3\<rbrakk> \<Longrightarrow> valid_pde' x3 s' proof (prove)
goal (3 subgoals):
 1. \<And>asidpool. \<lbrakk>valid_asid_pool' asidpool s; ksPSpace s = ksPSpace s'; obj = KOASIDPool asidpool\<rbrakk> \<Longrightarrow> valid_asid_pool' asidpool s'
 2. \<And>x2. \<lbrakk>valid_pte' x2 s; ksPSpace s = ksPSpace s'; obj = KOPTE x2\<rbrakk> \<Longrightarrow> valid_pte' x2 s'
 3. \<And>x3. \<lbrakk>valid_pde' x3 s; ksPSpace s = ksPSpace s'; obj = KOPDE x3\<rbrakk> \<Longrightarrow> valid_pde' x3 s' proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>valid_pte' x2 s; ksPSpace s = ksPSpace s'; obj = KOPTE x2\<rbrakk> \<Longrightarrow> valid_pte' x2 s'
 2. \<And>x3. \<lbrakk>valid_pde' x3 s; ksPSpace s = ksPSpace s'; obj = KOPDE x3\<rbrakk> \<Longrightarrow> valid_pde' x3 s' proof (prove)
goal (2 subgoals):
 1. \<And>pte. \<lbrakk>valid_pte' pte s; ksPSpace s = ksPSpace s'; obj = KOPTE pte\<rbrakk> \<Longrightarrow> valid_pte' pte s'
 2. \<And>x3. \<lbrakk>valid_pde' x3 s; ksPSpace s = ksPSpace s'; obj = KOPDE x3\<rbrakk> \<Longrightarrow> valid_pde' x3 s' proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>valid_pde' x3 s; ksPSpace s = ksPSpace s'; obj = KOPDE x3\<rbrakk> \<Longrightarrow> valid_pde' x3 s' proof (prove)
goal (1 subgoal):
 1. \<And>pde. \<lbrakk>valid_pde' pde s; ksPSpace s = ksPSpace s'; obj = KOPDE pde\<rbrakk> \<Longrightarrow> valid_pde' pde s' proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma valid_obj'_pspaceI:
  "valid_obj' obj s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> valid_obj' obj s'" unfolding valid_obj'_def by (cases obj)
     (auto simp: valid_ep'_def valid_ntfn'_def valid_tcb'_def valid_cte'_def
                 valid_tcb_state'_def valid_arch_obj'_pspaceI valid_bound_tcb'_def
                 valid_bound_ntfn'_def
           split: Structures_H.endpoint.splits Structures_H.notification.splits
                  Structures_H.thread_state.splits ntfn.splits option.splits
           intro: obj_at'_pspaceI valid_cap'_pspaceI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_obj' obj s; ksPSpace s = ksPSpace s'\<rbrakk> \<Longrightarrow> valid_obj' obj s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case obj of KOEndpoint endpoint \<Rightarrow> valid_ep' endpoint s | KONotification notification \<Rightarrow> valid_ntfn' notification s | KOKernelData \<Rightarrow> False | KOTCB tcb \<Rightarrow> valid_tcb' tcb s | KOCTE cte \<Rightarrow> valid_cte' cte s | KOArch arch_kernel_object \<Rightarrow> valid_arch_obj' arch_kernel_object s | _ \<Rightarrow> True; ksPSpace s = ksPSpace s'\<rbrakk> \<Longrightarrow> case obj of KOEndpoint endpoint \<Rightarrow> valid_ep' endpoint s' | KONotification notification \<Rightarrow> valid_ntfn' notification s' | KOKernelData \<Rightarrow> False | KOTCB tcb \<Rightarrow> valid_tcb' tcb s' | KOCTE cte \<Rightarrow> valid_cte' cte s' | KOArch arch_kernel_object \<Rightarrow> valid_arch_obj' arch_kernel_object s' | _ \<Rightarrow> True
theory Invariants_H

lemma pred_tcb_at'_pspaceI:
  "pred_tcb_at' proj P t s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> pred_tcb_at' proj P t s'" unfolding pred_tcb_at'_def by (fast intro: obj_at'_pspaceI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pred_tcb_at' proj P t s; ksPSpace s = ksPSpace s'\<rbrakk> \<Longrightarrow> pred_tcb_at' proj P t s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t s; ksPSpace s = ksPSpace s'\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t s'
theory Invariants_H

lemma valid_pspace':
  "valid_pspace' s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> valid_pspace' s'" by  (auto simp add: valid_pspace'_def valid_objs'_def pspace_aligned'_def
                     pspace_distinct'_def ps_clear_def no_0_obj'_def ko_wp_at'_def
                     typ_at'_def
           intro: valid_obj'_pspaceI valid_mdb'_pspaceI)

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

lemma valid_idle'_pspace_itI[elim]:
  "\<lbrakk> valid_idle' s; ksPSpace s = ksPSpace s'; ksIdleThread s = ksIdleThread s' \<rbrakk>
      \<Longrightarrow> valid_idle' s'" apply (clarsimp simp: valid_idle'_def ex_nonz_cap_to'_def) apply (erule obj_at'_pspaceI, assumption) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle' s; ksPSpace s = ksPSpace s'; ksIdleThread s = ksIdleThread s'\<rbrakk> \<Longrightarrow> valid_idle' s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s = ksPSpace s'; ksIdleThread s = idle_thread_ptr; obj_at' idle_tcb' idle_thread_ptr s; idle_thread_ptr = ksIdleThread s'\<rbrakk> \<Longrightarrow> obj_at' idle_tcb' idle_thread_ptr s' proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma obj_at'_weaken:
  assumes x: "obj_at' P t s"
  assumes y: "\<And>obj. P obj \<Longrightarrow> P' obj"
  shows "obj_at' P' t s" by (insert x, clarsimp simp: obj_at'_def y)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' P' t s
theory Invariants_H

lemma cte_wp_at_weakenE':
  "\<lbrakk>cte_wp_at' P t s; \<And>c. P c \<Longrightarrow> P' c\<rbrakk> \<Longrightarrow> cte_wp_at' P' t s" by (fastforce simp: cte_wp_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' P t s; \<And>c. P c \<Longrightarrow> P' c\<rbrakk> \<Longrightarrow> cte_wp_at' P' t s
theory Invariants_H

lemma pred_tcb'_weakenE:
  "\<lbrakk> pred_tcb_at' proj P t s; \<And>st. P st \<Longrightarrow> P' st \<rbrakk> \<Longrightarrow> pred_tcb_at' proj P' t s" apply (simp add: pred_tcb_at'_def) apply (erule obj_at'_weakenE) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pred_tcb_at' proj P t s; \<And>st. P st \<Longrightarrow> P' st\<rbrakk> \<Longrightarrow> pred_tcb_at' proj P' t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t s; \<And>st. P st \<Longrightarrow> P' st\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. P' (proj (tcb_to_itcb' ko))) t s proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<And>st. P st \<Longrightarrow> P' st; P (proj (tcb_to_itcb' k))\<rbrakk> \<Longrightarrow> P' (proj (tcb_to_itcb' k)) proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma lookupAround2_None1:
  "(fst (lookupAround2 x s) = None) = (\<forall>y \<le> x. s y = None)" apply (simp    add: lookupAround2_def Let_def split_def lookupAround_def
           split del: if_split
               split: option.split) apply safe apply (fastforce split: if_split_asm) apply (clarsimp simp: order_less_imp_le) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (fst (lookupAround2 x s) = None) = (\<forall>y\<le>x. s y = None) proof (prove)
goal (1 subgoal):
 1. (s x = None \<longrightarrow> ((if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = None) = (\<forall>y\<le>x. s y = None)) \<and> ((\<exists>x2. s x = Some x2) \<longrightarrow> (\<exists>y\<le>x. \<exists>ya. s y = Some ya)) proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>s x = None; (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = None; y \<le> x\<rbrakk> \<Longrightarrow> s y = None
 2. \<lbrakk>s x = None; \<forall>y\<le>x. s y = None\<rbrakk> \<Longrightarrow> (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = None
 3. \<And>x2. s x = Some x2 \<Longrightarrow> \<exists>y\<le>x. \<exists>ya. s y = Some ya proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s x = None; \<forall>y\<le>x. s y = None\<rbrakk> \<Longrightarrow> (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = None
 2. \<And>x2. s x = Some x2 \<Longrightarrow> \<exists>y\<le>x. \<exists>ya. s y = Some ya proof (prove)
goal (1 subgoal):
 1. \<And>x2. s x = Some x2 \<Longrightarrow> \<exists>y\<le>x. \<exists>ya. s y = Some ya proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma lookupAround2_None2:
  "(snd (lookupAround2 x s) = None) = (\<forall>y. x < y \<longrightarrow> s y = None)" apply (simp add: lookupAround2_def Let_def split_def del: maybe_def
               split: option.splits) apply (simp add: o_def map_option_is_None [where f=fst, unfolded map_option_case]) apply (simp add: lookupAround_def Let_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (snd (lookupAround2 x s) = None) = (\<forall>y>x. s y = None) proof (prove)
goal (1 subgoal):
 1. (maybe None (Some \<circ> fst) (snd (snd (lookupAround x s))) = None) = (\<forall>y>x. s y = None) proof (prove)
goal (1 subgoal):
 1. (snd (snd (lookupAround x s)) = None) = (\<forall>y>x. s y = None) proof (prove)
goal (1 subgoal):
 1. ((\<forall>xa. xa \<in> dom s \<longrightarrow> \<not> x < xa) \<longrightarrow> (\<forall>y>x. s y = None)) \<and> ((\<exists>xa. xa \<in> dom s \<and> x < xa) \<longrightarrow> (\<exists>y>x. \<exists>ya. s y = Some ya)) proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma in_alignCheck[simp]:
  "((v, s') \<in> fst (alignCheck x n s)) = (s' = s \<and> is_aligned x n)" by (simp add: alignCheck_def in_monad is_aligned_mask[symmetric]
                alignError_def conj_comms
          cong: conj_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v, s') \<in> fst (alignCheck x n s)) = (s' = s \<and> is_aligned x n)
theory Invariants_H

lemma tcb_ctes_clear:
  "\<lbrakk> tcb_cte_cases (y - x) = Some (getF, setF);
     is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s;
     ksPSpace s x = Some (KOTCB tcb) \<rbrakk>
     \<Longrightarrow> \<not> ksPSpace s y = Some (KOCTE cte)" apply clarsimp apply (erule(4) tcb_space_clear) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s; ksPSpace s x = Some (KOTCB tcb)\<rbrakk> \<Longrightarrow> ksPSpace s y \<noteq> Some (KOCTE cte) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some (KOCTE cte); x = y; getF = tcbCTable; setF = tcbCTable_update\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma cte_wp_atE' [consumes 1, case_names CTE TCB]:
  assumes cte: "cte_wp_at' P ptr s"
  and   r1: "\<And>cte.
    \<lbrakk> ksPSpace s ptr = Some (KOCTE cte); ps_clear ptr cte_level_bits s;
      is_aligned ptr cte_level_bits; P cte \<rbrakk> \<Longrightarrow> R"
  and   r2: "\<And> tcb ptr' getF setF.
  \<lbrakk> ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits;
     tcb_cte_cases (ptr - ptr') = Some (getF, setF); P (getF tcb) \<rbrakk> \<Longrightarrow> R"
  shows "R" by (rule disjE [OF iffD1 [OF cte_wp_at_cases' cte]])
     (auto intro: r1 r2 simp: cte_level_bits_def objBits_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R
theory Invariants_H

lemma cte_wp_at_tcbI':
  assumes "ksPSpace s ptr' = Some (KOTCB tcb)"
  assumes "is_aligned ptr' tcbBlockSizeBits"
  assumes "ps_clear ptr' tcbBlockSizeBits s"
  and     "tcb_cte_cases (ptr - ptr') = Some (getF, setF)"
  and     "P (getF tcb)"
  shows "cte_wp_at' P ptr s" using assms apply (simp add: cte_wp_at_cases') apply (rule disjI2, rule exI[where x="ptr - ptr'"]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' P ptr s proof (prove)
using this:
ksPSpace s ptr' = Some (KOTCB tcb)
is_aligned ptr' tcbBlockSizeBits
ps_clear ptr' tcbBlockSizeBits s
tcb_cte_cases (ptr - ptr') = Some (getF, setF)
P (getF tcb)

goal (1 subgoal):
 1. cte_wp_at' P ptr s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); is_aligned ptr' tcbBlockSizeBits; ps_clear ptr' tcbBlockSizeBits s; tcb_cte_cases (ptr - ptr') = Some (getF, setF); P (getF tcb)\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s ptr = Some (KOCTE cte) \<and> is_aligned ptr cte_level_bits \<and> P cte \<and> ps_clear ptr cteSizeBits s) \<or> (\<exists>n tcb. ksPSpace s (ptr - n) = Some (KOTCB tcb) \<and> is_aligned (ptr - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (ptr - n) tcbBlockSizeBits s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); is_aligned ptr' tcbBlockSizeBits; ps_clear ptr' tcbBlockSizeBits s; tcb_cte_cases (ptr - ptr') = Some (getF, setF); P (getF tcb)\<rbrakk> \<Longrightarrow> \<exists>tcb. ksPSpace s (ptr - (ptr - ptr')) = Some (KOTCB tcb) \<and> is_aligned (ptr - (ptr - ptr')) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases (ptr - ptr') = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (ptr - (ptr - ptr')) tcbBlockSizeBits s) proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma obj_at_ko_at':
  "obj_at' P p s \<Longrightarrow> \<exists>ko. ko_at' ko p s \<and> P ko" by (auto simp add: obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' P p s \<Longrightarrow> \<exists>ko. ko_at' ko p s \<and> P ko
theory Invariants_H

lemma obj_at_aligned':
  fixes P :: "('a :: pspace_storable) \<Rightarrow> bool"
  assumes oat: "obj_at' P p s"
  and    oab: "\<And>(v :: 'a) (v' :: 'a). objBits v = objBits v'"
  shows "is_aligned p (objBits (obj :: 'a))" using oat apply (clarsimp simp add: obj_at'_def) apply (clarsimp simp add: projectKO_def fail_def return_def
                            project_inject objBits_def[symmetric]
                     split: option.splits) apply (erule subst[OF oab]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p (objBits obj) proof (prove)
using this:
obj_at' P p s

goal (1 subgoal):
 1. is_aligned p (objBits obj) proof (prove)
goal (1 subgoal):
 1. \<And>ko obja. \<lbrakk>ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); fst (projectKO ko s) = {(obja, s)}; P obja; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> is_aligned p (objBits obj) proof (prove)
goal (1 subgoal):
 1. \<And>obja. \<lbrakk>P obja; ps_clear p (objBits obja) s; ksPSpace s p = Some (injectKO obja); is_aligned p (objBits obja)\<rbrakk> \<Longrightarrow> is_aligned p (objBits obj) proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma typ_at_lift_tcb':
  "\<lbrace>typ_at' TCBT p\<rbrace> f \<lbrace>\<lambda>_. typ_at' TCBT p\<rbrace> \<Longrightarrow> \<lbrace>tcb_at' p\<rbrace> f \<lbrace>\<lambda>_. tcb_at' p\<rbrace>" by (simp add: typ_at_tcb')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>typ_at' TCBT p\<rbrace> f \<lbrace>\<lambda>_. typ_at' TCBT p\<rbrace> \<Longrightarrow> \<lbrace>tcb_at' p\<rbrace> f \<lbrace>\<lambda>_. tcb_at' p\<rbrace>
theory Invariants_H

lemma typ_at_lift_ep':
  "\<lbrace>typ_at' EndpointT p\<rbrace> f \<lbrace>\<lambda>_. typ_at' EndpointT p\<rbrace> \<Longrightarrow> \<lbrace>ep_at' p\<rbrace> f \<lbrace>\<lambda>_. ep_at' p\<rbrace>" by (simp add: typ_at_ep)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>typ_at' EndpointT p\<rbrace> f \<lbrace>\<lambda>_. typ_at' EndpointT p\<rbrace> \<Longrightarrow> \<lbrace>ep_at' p\<rbrace> f \<lbrace>\<lambda>_. ep_at' p\<rbrace>
theory Invariants_H

lemma typ_at_lift_ntfn':
  "\<lbrace>typ_at' NotificationT p\<rbrace> f \<lbrace>\<lambda>_. typ_at' NotificationT p\<rbrace> \<Longrightarrow> \<lbrace>ntfn_at' p\<rbrace> f \<lbrace>\<lambda>_. ntfn_at' p\<rbrace>" by (simp add: typ_at_ntfn)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>typ_at' NotificationT p\<rbrace> f \<lbrace>\<lambda>_. typ_at' NotificationT p\<rbrace> \<Longrightarrow> \<lbrace>ntfn_at' p\<rbrace> f \<lbrace>\<lambda>_. ntfn_at' p\<rbrace>
theory Invariants_H

lemma typ_at_lift_cte':
  "\<lbrace>typ_at' CTET p\<rbrace> f \<lbrace>\<lambda>_. typ_at' CTET p\<rbrace> \<Longrightarrow> \<lbrace>real_cte_at' p\<rbrace> f \<lbrace>\<lambda>_. real_cte_at' p\<rbrace>" by (simp add: typ_at_cte)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>typ_at' CTET p\<rbrace> f \<lbrace>\<lambda>_. typ_at' CTET p\<rbrace> \<Longrightarrow> \<lbrace>real_cte_at' p\<rbrace> f \<lbrace>\<lambda>_. real_cte_at' p\<rbrace>
theory Invariants_H

lemma typ_at_lift_page_directory_at':
  assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>"
  shows      "\<lbrace>page_directory_at' p\<rbrace> f \<lbrace>\<lambda>rv. page_directory_at' p\<rbrace>" unfolding page_directory_at'_def All_less_Ball by (wp hoare_vcg_const_Ball_lift x)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>page_directory_at' p\<rbrace> f \<lbrace>\<lambda>rv. page_directory_at' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_aligned p pdBits \<and> (\<forall>y\<in>{..<2 ^ 12}. pde_at' (p + (y << 2)) s)\<rbrace> f \<lbrace>\<lambda>rv s. is_aligned p pdBits \<and> (\<forall>y\<in>{..<2 ^ 12}. pde_at' (p + (y << 2)) s)\<rbrace>
theory Invariants_H

lemma typ_at_lift_page_table_at':
  assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>"
  shows      "\<lbrace>page_table_at' p\<rbrace> f \<lbrace>\<lambda>rv. page_table_at' p\<rbrace>" unfolding page_table_at'_def All_less_Ball by (wp hoare_vcg_const_Ball_lift x)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>page_table_at' p\<rbrace> f \<lbrace>\<lambda>rv. page_table_at' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_aligned p ptBits \<and> (\<forall>y\<in>{..<2 ^ 8}. pte_at' (p + (y << 2)) s)\<rbrace> f \<lbrace>\<lambda>rv s. is_aligned p ptBits \<and> (\<forall>y\<in>{..<2 ^ 8}. pte_at' (p + (y << 2)) s)\<rbrace>
theory Invariants_H

lemma ko_wp_typ_at':
  "ko_wp_at' P p s \<Longrightarrow> \<exists>T. typ_at' T p s" by (clarsimp simp: typ_at'_def ko_wp_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_wp_at' P p s \<Longrightarrow> \<exists>T. typ_at' T p s
theory Invariants_H

lemma koType_obj_range':
  "koTypeOf k = koTypeOf k' \<Longrightarrow> obj_range' p k = obj_range' p k'" apply (rule ccontr) apply (simp add: obj_range'_def objBitsKO_def archObjSize_def
            split: kernel_object.splits arch_kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. koTypeOf k = koTypeOf k' \<Longrightarrow> obj_range' p k = obj_range' p k' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>koTypeOf k = koTypeOf k'; obj_range' p k \<noteq> obj_range' p k'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma typ_at_lift_asid_at':
  "(\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>_. typ_at' T p\<rbrace>) \<Longrightarrow> \<lbrace>asid_pool_at' p\<rbrace> f \<lbrace>\<lambda>_. asid_pool_at' p\<rbrace>" by assumption

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>_. typ_at' T p\<rbrace>) \<Longrightarrow> \<lbrace>asid_pool_at' p\<rbrace> f \<lbrace>\<lambda>_. asid_pool_at' p\<rbrace>
theory Invariants_H

lemma typ_at_lift_valid_irq_node':
  assumes P: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>"
  shows      "\<lbrace>valid_irq_node' p\<rbrace> f \<lbrace>\<lambda>_. valid_irq_node' p\<rbrace>" apply (simp add: valid_irq_node'_def) apply (wp hoare_vcg_all_lift P typ_at_lift_cte') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_node' p\<rbrace> f \<lbrace>\<lambda>_. valid_irq_node' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_aligned p (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (p + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s)\<rbrace> f \<lbrace>\<lambda>_ s. is_aligned p (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (p + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma valid_pde_lift':
  assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>"
  shows "\<lbrace>\<lambda>s. valid_pde' pde s\<rbrace> f \<lbrace>\<lambda>rv s. valid_pde' pde s\<rbrace>" by (cases pde) (simp add: valid_mapping'_def|wp x typ_at_lift_page_table_at')+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pde' pde\<rbrace> f \<lbrace>\<lambda>rv. valid_pde' pde\<rbrace>
theory Invariants_H

lemma valid_pte_lift':
  assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>"
  shows "\<lbrace>\<lambda>s. valid_pte' pte s\<rbrace> f \<lbrace>\<lambda>rv s. valid_pte' pte s\<rbrace>" by (cases pte) (simp add: valid_mapping'_def|wp x typ_at_lift_page_directory_at')+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pte' pte\<rbrace> f \<lbrace>\<lambda>rv. valid_pte' pte\<rbrace>
theory Invariants_H

lemma valid_asid_pool_lift':
  assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>"
  shows "\<lbrace>\<lambda>s. valid_asid_pool' ap s\<rbrace> f \<lbrace>\<lambda>rv s. valid_asid_pool' ap s\<rbrace>" by (cases ap) (simp|wp x typ_at_lift_page_directory_at' hoare_vcg_const_Ball_lift)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_pool' ap\<rbrace> f \<lbrace>\<lambda>rv. valid_asid_pool' ap\<rbrace>
theory Invariants_H

lemma valid_bound_tcb_lift:
  "(\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>_. typ_at' T p\<rbrace>) \<Longrightarrow>
  \<lbrace>valid_bound_tcb' tcb\<rbrace> f \<lbrace>\<lambda>_. valid_bound_tcb' tcb\<rbrace>" by (auto simp: valid_bound_tcb'_def valid_def typ_at_tcb'[symmetric] split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>_. typ_at' T p\<rbrace>) \<Longrightarrow> \<lbrace>valid_bound_tcb' tcb\<rbrace> f \<lbrace>\<lambda>_. valid_bound_tcb' tcb\<rbrace>
theory Invariants_H

lemma mdb_next_unfold:
  "s \<turnstile> c \<leadsto> c' = (\<exists>z. s c = Some z \<and> c' = mdbNext (cteMDBNode z))" by (auto simp add: mdb_next_rel_def mdb_next_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> c \<leadsto> c' = (\<exists>z. s c = Some z \<and> c' = mdbNext (cteMDBNode z))