kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchAcc_R

lemma setObject_PDE_valid_arch [wp]:
  "\<lbrace>valid_arch_state'\<rbrace> setObject p (v::pde) \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>" by (rule valid_arch_state_lift') (wp setObject_typ_at')+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state'\<rbrace> setObject p v \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>
theory ArchAcc_R

lemma setObject_PTE_valid_arch [wp]:
  "\<lbrace>valid_arch_state'\<rbrace> setObject p (v::pte) \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>" by (rule valid_arch_state_lift') (wp setObject_typ_at')+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state'\<rbrace> setObject p v \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>
theory ArchAcc_R

lemma setObject_PDE_ct [wp]:
  "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject p (e::pde) \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>" apply (simp add: setObject_def updateObject_default_def split_def) apply (wp updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject p e \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- do y <- assert (p = fst pa);
_ <- projectKO (snd pa);
y <- alignCheck p (objBits e);
y <- magnitudeCheck p (snd (lookupAround2 p ps)) (objBits e);
return (KOArch (KOPDE e))
od;
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma setObject_pte_ct [wp]:
  "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject p (e::pte) \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>" apply (simp add: setObject_def updateObject_default_def split_def) apply (wp updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject p e \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- do y <- assert (p = fst pa);
_ <- projectKO (snd pa);
y <- alignCheck p (objBits e);
y <- magnitudeCheck p (snd (lookupAround2 p ps)) (objBits e);
return (KOArch (KOPTE e))
od;
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma setObject_ASID_cur_tcb' [wp]:
  "\<lbrace>\<lambda>s. cur_tcb' s\<rbrace> setObject p (e::asidpool) \<lbrace>\<lambda>_ s. cur_tcb' s\<rbrace>" apply (simp add: cur_tcb'_def) apply (rule hoare_lift_Pf [where f=ksCurThread]) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> setObject p e \<lbrace>\<lambda>_. cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' (ksCurThread s) s\<rbrace> setObject p e \<lbrace>\<lambda>_ s. tcb_at' (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>tcb_at' x\<rbrace> setObject p e \<lbrace>\<lambda>_. tcb_at' x\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject p e \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma setObject_PDE_cur_tcb' [wp]:
  "\<lbrace>\<lambda>s. cur_tcb' s\<rbrace> setObject p (e::pde) \<lbrace>\<lambda>_ s. cur_tcb' s\<rbrace>" apply (simp add: cur_tcb'_def) apply (rule hoare_lift_Pf [where f=ksCurThread]) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> setObject p e \<lbrace>\<lambda>_. cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' (ksCurThread s) s\<rbrace> setObject p e \<lbrace>\<lambda>_ s. tcb_at' (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>tcb_at' x\<rbrace> setObject p e \<lbrace>\<lambda>_. tcb_at' x\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject p e \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma setObject_pte_cur_tcb' [wp]:
  "\<lbrace>\<lambda>s. cur_tcb' s\<rbrace> setObject p (e::pte) \<lbrace>\<lambda>_ s. cur_tcb' s\<rbrace>" apply (simp add: cur_tcb'_def) apply (rule hoare_lift_Pf [where f=ksCurThread]) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> setObject p e \<lbrace>\<lambda>_. cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' (ksCurThread s) s\<rbrace> setObject p e \<lbrace>\<lambda>_ s. tcb_at' (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>tcb_at' x\<rbrace> setObject p e \<lbrace>\<lambda>_. tcb_at' x\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject p e \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma page_directory_pde_at_lookupI':
  "page_directory_at' pd s \<Longrightarrow> pde_at' (lookup_pd_slot pd vptr) s" apply (simp add: lookup_pd_slot_def Let_def) apply (erule page_directory_pde_atI') apply (rule vptr_shiftr_le_2p) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. page_directory_at' pd s \<Longrightarrow> pde_at' (lookup_pd_slot pd vptr) s proof (prove)
goal (1 subgoal):
 1. page_directory_at' pd s \<Longrightarrow> pde_at' (pd + (vptr >> 20 << 2)) s proof (prove)
goal (1 subgoal):
 1. vptr >> 20 < 2 ^ pageBits proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma pt_bits_stuff:
  "pt_bits = ptBits"
  "ptBits < word_bits"
  "2 \<le> ptBits" by (simp add: pt_bits_def ptBits_def pageBits_def word_bits_def pteBits_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pt_bits = ptBits &&& ptBits < word_bits &&& 2 \<le> ptBits
theory ArchAcc_R

lemma page_table_pte_at_lookupI':
  "page_table_at' pt s \<Longrightarrow> pte_at' (lookup_pt_slot_no_fail pt vptr) s" apply (simp add: lookup_pt_slot_no_fail_def) apply (erule page_table_pte_atI') apply (rule vptr_shiftr_le_2pt[simplified pt_bits_stuff]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. page_table_at' pt s \<Longrightarrow> pte_at' (lookup_pt_slot_no_fail pt vptr) s proof (prove)
goal (1 subgoal):
 1. page_table_at' pt s \<Longrightarrow> pte_at' (pt + ((vptr >> 12) && 0xFF << 2)) s proof (prove)
goal (1 subgoal):
 1. (vptr >> 12) && 0xFF < 2 ^ (ptBits - 2) proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma storePTE_ctes [wp]:
  "\<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> storePTE p pte \<lbrace>\<lambda>_ s. P (ctes_of s)\<rbrace>" apply (rule ctes_of_from_cte_wp_at [where Q=\<top>, simplified]) apply (rule storePTE_cte_wp_at') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> storePTE p pte \<lbrace>\<lambda>_ s. P (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P P' pa. \<lbrace>\<lambda>s. P (cte_wp_at' P' pa s)\<rbrace> storePTE p pte \<lbrace>\<lambda>r s. P (cte_wp_at' P' pa s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma storePDE_ctes [wp]:
  "\<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> storePDE p pte \<lbrace>\<lambda>_ s. P (ctes_of s)\<rbrace>" apply (rule ctes_of_from_cte_wp_at [where Q=\<top>, simplified]) apply (rule storePDE_cte_wp_at') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> storePDE p pte \<lbrace>\<lambda>_ s. P (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P P' pa. \<lbrace>\<lambda>s. P (cte_wp_at' P' pa s)\<rbrace> storePDE p pte \<lbrace>\<lambda>r s. P (cte_wp_at' P' pa s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma setObject_ASID_cte_wp_at'[wp]:
  "\<lbrace>\<lambda>s. P (cte_wp_at' P' p s)\<rbrace>
     setObject ptr (asid::asidpool)
   \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>" apply (wp setObject_cte_wp_at2'[where Q="\<top>"]) apply (clarsimp simp: updateObject_default_def in_monad
                          projectKO_opts_defs projectKOs) apply (rule equals0I) apply (clarsimp simp: updateObject_default_def in_monad
                         projectKOs projectKO_opts_defs) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at' P' p s)\<rbrace> setObject ptr asid \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject asid (KOTCB tcb) ptr x n s); True; lookupAround2 ptr (ksPSpace s) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> \<exists>tcb'. t = (KOTCB tcb', s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb' = getF tcb)
 2. \<And>x n cte s. fst (updateObject asid (KOCTE cte) ptr x n s) = {}
 3. \<And>s. P (cte_wp_at' P' p s) \<Longrightarrow> P (cte_wp_at' P' p s) \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>x n cte s. fst (updateObject asid (KOCTE cte) ptr x n s) = {}
 2. \<And>s. P (cte_wp_at' P' p s) \<Longrightarrow> P (cte_wp_at' P' p s) \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>x n cte s y. y \<in> fst (updateObject asid (KOCTE cte) ptr x n s) \<Longrightarrow> False
 2. \<And>s. P (cte_wp_at' P' p s) \<Longrightarrow> P (cte_wp_at' P' p s) \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s. P (cte_wp_at' P' p s) \<Longrightarrow> P (cte_wp_at' P' p s) \<and> True proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma setObject_ASID_ctes_of'[wp]:
  "\<lbrace>\<lambda>s. P (ctes_of s)\<rbrace>
     setObject ptr (asid::asidpool)
   \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>" by (rule ctes_of_from_cte_wp_at [where Q=\<top>, simplified]) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> setObject ptr asid \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>
theory ArchAcc_R

lemma clearMemory_vms':
  "valid_machine_state' s \<Longrightarrow>
   \<forall>x\<in>fst (clearMemory ptr bits (ksMachineState s)).
      valid_machine_state' (s\<lparr>ksMachineState := snd x\<rparr>)" apply (clarsimp simp: valid_machine_state'_def
                        disj_commute[of "pointerInUserData p s" for p s]) apply (drule_tac x=p in spec, simp) apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = 0"
         in use_valid[where P=P and Q="\<lambda>_. P" for P], simp_all) apply (rule clearMemory_um_eq_0) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_machine_state' s \<Longrightarrow> \<forall>x\<in>fst (clearMemory ptr bits (ksMachineState s)). valid_machine_state' (s\<lparr>ksMachineState := snd x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>b p. \<lbrakk>\<forall>p. pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0 \<or> pointerInUserData p s; ((), b) \<in> fst (clearMemory ptr bits (ksMachineState s)); \<not> pointerInDeviceData p s; \<not> pointerInUserData p s\<rbrakk> \<Longrightarrow> underlying_memory b p = 0 proof (prove)
goal (1 subgoal):
 1. \<And>b p. \<lbrakk>((), b) \<in> fst (clearMemory ptr bits (ksMachineState s)); \<not> pointerInDeviceData p s; \<not> pointerInUserData p s; underlying_memory (ksMachineState s) p = 0\<rbrakk> \<Longrightarrow> underlying_memory b p = 0 proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<not> pointerInDeviceData p s; \<not> pointerInUserData p s; underlying_memory (ksMachineState s) p = 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>m'. underlying_memory m' p = 0\<rbrace> clearMemory ptr bits \<lbrace>\<lambda>_ m'. underlying_memory m' p = 0\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma capUntypedPtr_simps [simp]:
  "capUntypedPtr (ThreadCap r) = r"
  "capUntypedPtr (NotificationCap r badge a b) = r"
  "capUntypedPtr (EndpointCap r badge a b c d) = r"
  "capUntypedPtr (Zombie r bits n) = r"
  "capUntypedPtr (ArchObjectCap x) = Arch.capUntypedPtr x"
  "capUntypedPtr (UntypedCap d r n f) = r"
  "capUntypedPtr (CNodeCap r n g n2) = r"
  "capUntypedPtr (ReplyCap r m a) = r"
  "Arch.capUntypedPtr (ARM_H.ASIDPoolCap r asid) = r"
  "Arch.capUntypedPtr (ARM_H.PageCap d r rghts sz mapdata) = r"
  "Arch.capUntypedPtr (ARM_H.PageTableCap r mapdata2) = r"
  "Arch.capUntypedPtr (ARM_H.PageDirectoryCap r mapdata3) = r" by (auto simp: capUntypedPtr_def
                 ARM_H.capUntypedPtr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((global.capUntypedPtr (capability.ThreadCap r) = r &&& global.capUntypedPtr (capability.NotificationCap r badge a b) = r &&& global.capUntypedPtr (capability.EndpointCap r badge a b c d) = r) &&& global.capUntypedPtr (capability.Zombie r bits n) = r &&& global.capUntypedPtr (capability.ArchObjectCap x) = Arch.capUntypedPtr x &&& global.capUntypedPtr (capability.UntypedCap d r n f) = r) &&& (global.capUntypedPtr (capability.CNodeCap r n g n2) = r &&& global.capUntypedPtr (capability.ReplyCap r m a) = r &&& Arch.capUntypedPtr (arch_capability.ASIDPoolCap r asid) = r) &&& Arch.capUntypedPtr (arch_capability.PageCap d r rghts sz mapdata) = r &&& Arch.capUntypedPtr (arch_capability.PageTableCap r mapdata2) = r &&& Arch.capUntypedPtr (arch_capability.PageDirectoryCap r mapdata3) = r
theory CSpace_I

lemma rights_mask_map_UNIV [simp]:
  "rights_mask_map UNIV = allRights" by (simp add: rights_mask_map_def allRights_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rights_mask_map UNIV = allRights
theory CSpace_I

lemma maskCapRights_allRights [simp]:
  "maskCapRights allRights c = c" unfolding maskCapRights_def isCap_defs allRights_def
            ARM_H.maskCapRights_def maskVMRights_def by (cases c) (simp_all add: Let_def split: arch_capability.split vmrights.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.maskCapRights allRights c = c proof (prove)
goal (1 subgoal):
 1. (let ca = c; aoCap = capCap c in if case ca of capability.NullCap \<Rightarrow> True | _ \<Rightarrow> False then capability.NullCap else if case ca of capability.DomainCap \<Rightarrow> True | _ \<Rightarrow> False then capability.DomainCap else if case ca of capability.UntypedCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False then ca else if case ca of capability.EndpointCap v0 v1 v2 v3 v4 v5 \<Rightarrow> True | _ \<Rightarrow> False then capEPCanGrantReply_update (\<lambda>_. capEPCanGrantReply ca \<and> capAllowGrantReply (CapRights True True True True)) (capEPCanGrant_update (\<lambda>_. capEPCanGrant ca \<and> capAllowGrant (CapRights True True True True)) (capEPCanReceive_update (\<lambda>_. capEPCanReceive ca \<and> capAllowRead (CapRights True True True True)) (capEPCanSend_update (\<lambda>_. capEPCanSend ca \<and> capAllowWrite (CapRights True True True True)) ca))) else if case ca of capability.NotificationCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False then capNtfnCanReceive_update (\<lambda>_. capNtfnCanReceive ca \<and> capAllowRead (CapRights True True True True)) (capNtfnCanSend_update (\<lambda>_. capNtfnCanSend ca \<and> capAllowWrite (CapRights True True True True)) ca) else if case ca of capability.ReplyCap v0 v1 v2 \<Rightarrow> True | _ \<Rightarrow> False then capReplyCanGrant_update (\<lambda>_. capReplyCanGrant ca \<and> capAllowGrant (CapRights True True True True)) ca else if case ca of capability.CNodeCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False then ca else if case ca of capability.ThreadCap v0 \<Rightarrow> True | _ \<Rightarrow> False then ca else if case ca of capability.IRQControlCap \<Rightarrow> True | _ \<Rightarrow> False then ca else if case ca of capability.IRQHandlerCap v0 \<Rightarrow> True | _ \<Rightarrow> False then ca else if case ca of capability.ArchObjectCap v0 \<Rightarrow> True | _ \<Rightarrow> False then let c = aoCap in if case c of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False then capability.ArchObjectCap $ capVPRights_update (\<lambda>_. case (capVPRights c, capAllowRead (CapRights True True True True), capAllowWrite (CapRights True True True True)) of (VMNoAccess, x, xa) \<Rightarrow> VMNoAccess | (VMKernelOnly, b) \<Rightarrow> VMKernelOnly | (VMReadOnly, True, x) \<Rightarrow> VMReadOnly | (VMReadOnly, False, x) \<Rightarrow> VMKernelOnly | (VMReadWrite, True, True) \<Rightarrow> VMReadWrite | (VMReadWrite, True, False) \<Rightarrow> VMReadOnly | (VMReadWrite, False, ba) \<Rightarrow> VMKernelOnly) c else capability.ArchObjectCap c else if case ca of capability.Zombie v0 v1 v2 \<Rightarrow> True | _ \<Rightarrow> False then ca else undefined) = c
theory CSpace_I

lemma getCTE_inv [wp]: "\<lbrace>P\<rbrace> getCTE addr \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: getCTE_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getCTE addr \<lbrace>\<lambda>rv. P\<rbrace>
theory CSpace_I

lemma getNotification_inv [wp]:
  "\<lbrace>P\<rbrace> getNotification ptr \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: getNotification_def getObject_inv loadObject_default_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getNotification ptr \<lbrace>\<lambda>rv. P\<rbrace>
theory CSpace_I

lemma getSlotCap_inv [wp]: "\<lbrace>P\<rbrace> getSlotCap addr \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: getSlotCap_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getSlotCap addr \<lbrace>\<lambda>rv. P\<rbrace>
theory CSpace_I

lemma cap_case_CNodeCap:
  "(case cap of CNodeCap a b c d \<Rightarrow> P
         | _ \<Rightarrow> Q)
      = (if isCNodeCap cap then P else Q)" by (cases cap, simp_all add: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case cap of capability.CNodeCap a b c d \<Rightarrow> P | _ \<Rightarrow> Q) = (if isCNodeCap cap then P else Q)
theory CSpace_I

lemma rab_inv' [wp]:
  "\<lbrace>P\<rbrace> resolveAddressBits cap addr depth \<lbrace>\<lambda>rv. P\<rbrace>" by (rule validE_valid, rule use_specE', rule resolveAddressBits_inv_induct)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> CSpace_H.resolveAddressBits cap addr depth \<lbrace>\<lambda>rv. P\<rbrace>
theory CSpace_I

lemma updateObject_cte_inv:
  "\<lbrace>P\<rbrace> updateObject (cte :: cte) ko x y n \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: updateObject_cte) apply (cases ko, simp_all add: typeError_def unless_def
                      split del: if_split
                           cong: if_cong) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> updateObject cte ko x y n \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> case ko of KOTCB tcb \<Rightarrow> do alignCheck y (objBits tcb);
magnitudeCheck y n (objBits tcb);
if x - y = tcbVTableSlot << objBits undefined then return (KOTCB (tcbVTable_update (\<lambda>_. cte) tcb)) else if x - y = tcbCTableSlot << objBits undefined then return (KOTCB (tcbCTable_update (\<lambda>_. cte) tcb)) else if x - y = tcbReplySlot << objBits undefined then return (KOTCB (tcbReply_update (\<lambda>_. cte) tcb)) else if x - y = tcbCallerSlot << objBits undefined then return (KOTCB (tcbCaller_update (\<lambda>_. cte) tcb)) else if x - y = tcbIPCBufferSlot << objBits undefined then return (KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb)) else fail
od | KOCTE v3 \<Rightarrow> do unless (x = y) $ haskell_fail [];
alignCheck x (objBits cte);
magnitudeCheck x n (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] ko \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x6. ko = KOTCB x6 \<Longrightarrow> \<lbrace>P\<rbrace> do ya <- alignCheck y (objBits x6);
ya <- magnitudeCheck y n (objBits x6);
if x - y = tcbVTableSlot << objBits undefined then return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6)) else if x - y = tcbCTableSlot << objBits undefined then return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6)) else if x - y = tcbReplySlot << objBits undefined then return (KOTCB (tcbReply_update (\<lambda>_. cte) x6)) else if x - y = tcbCallerSlot << objBits undefined then return (KOTCB (tcbCaller_update (\<lambda>_. cte) x6)) else if x - y = tcbIPCBufferSlot << objBits undefined then return (KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) x6)) else fail
od \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>x7. ko = KOCTE x7 \<Longrightarrow> \<lbrace>P\<rbrace> do y <- when (x \<noteq> y) fail;
y <- alignCheck x (objBits cte);
y <- magnitudeCheck x n (objBits cte);
return (KOCTE cte)
od \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma mdb_next_update:
  "m (x \<mapsto> y) \<turnstile> a \<leadsto> b =
  (if a = x then mdbNext (cteMDBNode y) = b else m \<turnstile> a \<leadsto> b)" by (simp add: mdb_next_rel_def mdb_next_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m(x \<mapsto> y) \<turnstile> a \<leadsto> b = (if a = x then mdbNext (cteMDBNode y) = b else m \<turnstile> a \<leadsto> b)
theory CSpace_I

lemma neg_no_loopsI:
  "m \<turnstile> c \<leadsto>\<^sup>+ c \<Longrightarrow> \<not> no_loops m" unfolding no_loops_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> c \<leadsto>\<^sup>+ c \<Longrightarrow> \<not> no_loops m proof (prove)
goal (1 subgoal):
 1. m \<turnstile> c \<leadsto>\<^sup>+ c \<Longrightarrow> \<not> (\<forall>c. (c, c) \<notin> (mdb_next_rel m)\<^sup>+)
theory CSpace_I

lemma valid_dlistEp [elim?]:
  "\<lbrakk> valid_dlist m; m p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0;
     \<And>cte'. \<lbrakk> m (mdbPrev (cteMDBNode cte)) = Some cte';
              mdbNext (cteMDBNode cte') = p \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow>
  P" unfolding valid_dlist_def Let_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist m; m p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; \<And>cte'. \<lbrakk>m (mdbPrev (cteMDBNode cte)) = Some cte'; mdbNext (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p cte. m p = Some cte \<longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)); m p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; \<And>cte'. \<lbrakk>m (mdbPrev (cteMDBNode cte)) = Some cte'; mdbNext (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory CSpace_I

lemma valid_dlistEn [elim?]:
  "\<lbrakk> valid_dlist m; m p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0;
     \<And>cte'. \<lbrakk> m (mdbNext (cteMDBNode cte)) = Some cte';
              mdbPrev (cteMDBNode cte') = p \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow>
  P" unfolding valid_dlist_def Let_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist m; m p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; \<And>cte'. \<lbrakk>m (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p cte. m p = Some cte \<longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)); m p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; \<And>cte'. \<lbrakk>m (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P