kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchAcc_R

lemma getObject_PDE_corres' :
  "corres (pde_relation_aligned (p >> 2)) (pde_at p)
     (pspace_aligned' and pspace_distinct')
     (get_pde p) (getObject p)" apply (rule stronger_corres_guard_imp,
         rule getObject_PDE_corres) apply auto[1] apply clarsimp apply (rule aligned_distinct_relation_pde_atI') apply (simp add:state_relation_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (pde_relation_aligned (p >> 2)) (pde_at p) (pspace_aligned' and pspace_distinct') (get_pde p) (getObject p) proof (prove)
goal (3 subgoals):
 1. p = p
 2. \<And>s s'. \<lbrakk>pde_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pde_at p s
 3. \<And>s s'. \<lbrakk>pde_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>pde_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pde_at p s
 2. \<And>s s'. \<lbrakk>pde_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>pde_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>pde_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pde_at p (?s8 s s')
 2. \<And>s s'. \<lbrakk>pde_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pspace_relation (kheap (?s8 s s')) (ksPSpace s')
 3. \<And>s s'. \<lbrakk>pde_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pspace_aligned' s'
 4. \<And>s s'. \<lbrakk>pde_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pspace_distinct' s' proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma pte_relation_aligned_simp:
  "pte_relation_aligned (ucast (p && mask pt_bits >> 2)::word8) pde pde' =
   pte_relation_aligned ((p::word32) >> 2) pde pde'" by (clarsimp simp: pte_relation_aligned_def
              split: ARM_H.pte.splits if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pte_relation_aligned (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) pde pde' = pte_relation_aligned (p >> 2) pde pde'
theory ArchAcc_R

lemma getObject_PTE_corres':
  "corres (pte_relation_aligned (p >> 2)) (pte_at p)
     (pspace_aligned' and pspace_distinct')
     (get_pte p) (getObject p)" apply (rule stronger_corres_guard_imp,
         rule getObject_PTE_corres) apply auto[1] apply clarsimp apply (rule aligned_distinct_relation_pte_atI') apply (simp add:state_relation_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (pte_relation_aligned (p >> 2)) (pte_at p) (pspace_aligned' and pspace_distinct') (get_pte p) (getObject p) proof (prove)
goal (3 subgoals):
 1. p = p
 2. \<And>s s'. \<lbrakk>pte_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pte_at p s
 3. \<And>s s'. \<lbrakk>pte_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>pte_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pte_at p s
 2. \<And>s s'. \<lbrakk>pte_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>pte_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>pte_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pte_at p (?s8 s s')
 2. \<And>s s'. \<lbrakk>pte_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pspace_relation (kheap (?s8 s s')) (ksPSpace s')
 3. \<And>s s'. \<lbrakk>pte_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pspace_aligned' s'
 4. \<And>s s'. \<lbrakk>pte_at p s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pspace_distinct' s' proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma get_master_pte_corres':
  "corres pte_relation' (pte_at p)
     ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
      pspace_aligned' and pspace_distinct')
     (get_master_pte p) (getObject p)" apply (rule stronger_corres_guard_imp,
         rule get_master_pte_corres) apply auto done

\<comment> \<open>setObject_other_corres unfortunately doesn't work here\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres pte_relation' (pte_at p) ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') (get_master_pte p) (getObject p) proof (prove)
goal (3 subgoals):
 1. p = p
 2. \<And>s s'. \<lbrakk>pte_at p s; ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pte_at p s
 3. \<And>s s'. \<lbrakk>pte_at p s; ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pte_at' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') s' proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma storePDE_corres':
  "pde_relation_aligned (p >> 2) pde pde' \<Longrightarrow>
  corres dc
     (pde_at p and pspace_aligned and valid_etcbs) (pspace_aligned' and pspace_distinct')
     (store_pde p pde) (storePDE p pde')" apply (rule stronger_corres_guard_imp, rule storePDE_corres) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pde_relation_aligned (p >> 2) pde pde' \<Longrightarrow> corres dc (pde_at p and pspace_aligned and valid_etcbs) (pspace_aligned' and pspace_distinct') (store_pde p pde) (storePDE p pde') proof (prove)
goal (4 subgoals):
 1. pde_relation_aligned (p >> 2) pde pde' \<Longrightarrow> pde_relation_aligned (p >> 2) pde pde'
 2. pde_relation_aligned (p >> 2) pde pde' \<Longrightarrow> p = p
 3. \<And>s s'. \<lbrakk>pde_relation_aligned (p >> 2) pde pde'; (pde_at p and pspace_aligned and valid_etcbs) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at p and pspace_aligned and valid_etcbs) s
 4. \<And>s s'. \<lbrakk>pde_relation_aligned (p >> 2) pde pde'; (pde_at p and pspace_aligned and valid_etcbs) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma storePTE_corres':
  "pte_relation_aligned (p >> 2) pte pte' \<Longrightarrow>
  corres dc (pte_at p and pspace_aligned and valid_etcbs)
            (pspace_aligned' and pspace_distinct')
            (store_pte p pte) (storePTE p pte')" apply (rule stronger_corres_guard_imp, rule storePTE_corres) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pte_relation_aligned (p >> 2) pte pte' \<Longrightarrow> corres dc (pte_at p and pspace_aligned and valid_etcbs) (pspace_aligned' and pspace_distinct') (store_pte p pte) (storePTE p pte') proof (prove)
goal (4 subgoals):
 1. pte_relation_aligned (p >> 2) pte pte' \<Longrightarrow> pte_relation_aligned (p >> 2) pte pte'
 2. pte_relation_aligned (p >> 2) pte pte' \<Longrightarrow> p = p
 3. \<And>s s'. \<lbrakk>pte_relation_aligned (p >> 2) pte pte'; (pte_at p and pspace_aligned and valid_etcbs) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pte_at p and pspace_aligned and valid_etcbs) s
 4. \<And>s s'. \<lbrakk>pte_relation_aligned (p >> 2) pte pte'; (pte_at p and pspace_aligned and valid_etcbs) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma lookupPDSlot_corres [simp]:
  "lookupPDSlot pd vptr = lookup_pd_slot pd vptr" by (simp add: lookupPDSlot_def lookup_pd_slot_def pageBits_def ptBits_def pdeBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lookupPDSlot pd vptr = lookup_pd_slot pd vptr
theory ArchAcc_R

lemma pte_relation_must_pte:
  "pte_relation m (ArchObj (PageTable pt)) ko \<Longrightarrow> \<exists>pte. ko = (KOArch (KOPTE pte))" apply (case_tac ko) apply (simp_all add:pte_relation_def) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pte_relation m (ArchObj (PageTable pt)) ko \<Longrightarrow> \<exists>pte. ko = KOArch (KOPTE pte) proof (prove)
goal (8 subgoals):
 1. \<And>x1. \<lbrakk>pte_relation m (ArchObj (PageTable pt)) ko; ko = KOEndpoint x1\<rbrakk> \<Longrightarrow> \<exists>pte. ko = KOArch (KOPTE pte)
 2. \<And>x2. \<lbrakk>pte_relation m (ArchObj (PageTable pt)) ko; ko = KONotification x2\<rbrakk> \<Longrightarrow> \<exists>pte. ko = KOArch (KOPTE pte)
 3. \<lbrakk>pte_relation m (ArchObj (PageTable pt)) ko; ko = KOKernelData\<rbrakk> \<Longrightarrow> \<exists>pte. ko = KOArch (KOPTE pte)
 4. \<lbrakk>pte_relation m (ArchObj (PageTable pt)) ko; ko = KOUserData\<rbrakk> \<Longrightarrow> \<exists>pte. ko = KOArch (KOPTE pte)
 5. \<lbrakk>pte_relation m (ArchObj (PageTable pt)) ko; ko = KOUserDataDevice\<rbrakk> \<Longrightarrow> \<exists>pte. ko = KOArch (KOPTE pte)
 6. \<And>x6. \<lbrakk>pte_relation m (ArchObj (PageTable pt)) ko; ko = KOTCB x6\<rbrakk> \<Longrightarrow> \<exists>pte. ko = KOArch (KOPTE pte)
 7. \<And>x7. \<lbrakk>pte_relation m (ArchObj (PageTable pt)) ko; ko = KOCTE x7\<rbrakk> \<Longrightarrow> \<exists>pte. ko = KOArch (KOPTE pte)
 8. \<And>x8. \<lbrakk>pte_relation m (ArchObj (PageTable pt)) ko; ko = KOArch x8\<rbrakk> \<Longrightarrow> \<exists>pte. ko = KOArch (KOPTE pte) proof (prove)
goal (1 subgoal):
 1. \<And>x8. \<lbrakk>\<exists>pte. x8 = KOPTE pte \<and> pte_relation_aligned m (pt m) pte; ko = KOArch x8\<rbrakk> \<Longrightarrow> \<exists>pte. x8 = KOPTE pte proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma pde_relation_must_pde:
  "pde_relation m (ArchObj (PageDirectory pd)) ko \<Longrightarrow> \<exists>pde. ko = (KOArch (KOPDE pde))" apply (case_tac ko) apply (simp_all add:pde_relation_def) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pde_relation m (ArchObj (PageDirectory pd)) ko \<Longrightarrow> \<exists>pde. ko = KOArch (KOPDE pde) proof (prove)
goal (8 subgoals):
 1. \<And>x1. \<lbrakk>pde_relation m (ArchObj (PageDirectory pd)) ko; ko = KOEndpoint x1\<rbrakk> \<Longrightarrow> \<exists>pde. ko = KOArch (KOPDE pde)
 2. \<And>x2. \<lbrakk>pde_relation m (ArchObj (PageDirectory pd)) ko; ko = KONotification x2\<rbrakk> \<Longrightarrow> \<exists>pde. ko = KOArch (KOPDE pde)
 3. \<lbrakk>pde_relation m (ArchObj (PageDirectory pd)) ko; ko = KOKernelData\<rbrakk> \<Longrightarrow> \<exists>pde. ko = KOArch (KOPDE pde)
 4. \<lbrakk>pde_relation m (ArchObj (PageDirectory pd)) ko; ko = KOUserData\<rbrakk> \<Longrightarrow> \<exists>pde. ko = KOArch (KOPDE pde)
 5. \<lbrakk>pde_relation m (ArchObj (PageDirectory pd)) ko; ko = KOUserDataDevice\<rbrakk> \<Longrightarrow> \<exists>pde. ko = KOArch (KOPDE pde)
 6. \<And>x6. \<lbrakk>pde_relation m (ArchObj (PageDirectory pd)) ko; ko = KOTCB x6\<rbrakk> \<Longrightarrow> \<exists>pde. ko = KOArch (KOPDE pde)
 7. \<And>x7. \<lbrakk>pde_relation m (ArchObj (PageDirectory pd)) ko; ko = KOCTE x7\<rbrakk> \<Longrightarrow> \<exists>pde. ko = KOArch (KOPDE pde)
 8. \<And>x8. \<lbrakk>pde_relation m (ArchObj (PageDirectory pd)) ko; ko = KOArch x8\<rbrakk> \<Longrightarrow> \<exists>pde. ko = KOArch (KOPDE pde) proof (prove)
goal (1 subgoal):
 1. \<And>x8. \<lbrakk>\<exists>pde. x8 = KOPDE pde \<and> pde_relation_aligned m (pd m) pde; ko = KOArch x8\<rbrakk> \<Longrightarrow> \<exists>pde. x8 = KOPDE pde proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma getPDE_wp:
  "\<lbrace>\<lambda>s. \<forall>ko. ko_at' (ko::pde) p s \<longrightarrow> Q ko s\<rbrace> getObject p \<lbrace>Q\<rbrace>" by (clarsimp simp: getObject_def split_def loadObject_default_def
                     archObjSize_def in_magnitude_check pdeBits_def
                     projectKOs in_monad valid_def obj_at'_def objBits_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ko. ko_at' ko p s \<longrightarrow> Q ko s\<rbrace> getObject p \<lbrace>Q\<rbrace>
theory ArchAcc_R

lemma getPTE_wp:
  "\<lbrace>\<lambda>s. \<forall>ko. ko_at' (ko::pte) p s \<longrightarrow> Q ko s\<rbrace> getObject p \<lbrace>Q\<rbrace>" by (clarsimp simp: getObject_def split_def loadObject_default_def
                     archObjSize_def in_magnitude_check pteBits_def
                     projectKOs in_monad valid_def obj_at'_def objBits_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ko. ko_at' ko p s \<longrightarrow> Q ko s\<rbrace> getObject p \<lbrace>Q\<rbrace>
theory ArchAcc_R

lemma page_table_at_lift:
  "\<forall>s s'. (s, s') \<in> state_relation \<longrightarrow> (ptrFromPAddr ptr) = ptr' \<longrightarrow>
  (pspace_aligned s \<and> valid_pde (ARM_A.PageTablePDE ptr x z) s) \<longrightarrow>
  pspace_distinct' s' \<longrightarrow> page_table_at' ptr' s'" by (fastforce intro!: page_table_at_state_relation)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> state_relation \<longrightarrow> ptrFromPAddr ptr = ptr' \<longrightarrow> pspace_aligned s \<and> valid_pde (ARM_A.PageTablePDE ptr x z) s \<longrightarrow> pspace_distinct' s' \<longrightarrow> page_table_at' ptr' s'
theory ArchAcc_R

lemma setObject_asid_typ_at' [wp]:
  "\<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> setObject p' (v::asidpool) \<lbrace>\<lambda>_ s. P (typ_at' T p s)\<rbrace>" by (wp setObject_typ_at')

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

lemma getObject_pte_inv[wp]:
  "\<lbrace>P\<rbrace> getObject p \<lbrace>\<lambda>rv :: pte. P\<rbrace>" by (simp add: getObject_inv loadObject_default_inv)

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

lemma getObject_pde_inv[wp]:
  "\<lbrace>P\<rbrace> getObject p \<lbrace>\<lambda>rv :: pde. P\<rbrace>" by (simp add: getObject_inv loadObject_default_inv)

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

lemma arch_cap_rights_update:
  "acap_relation c c' \<Longrightarrow>
   cap_relation (cap.ArchObjectCap (acap_rights_update (acap_rights c \<inter> msk) c))
                 (Arch.maskCapRights (rights_mask_map msk) c')" apply (cases c, simp_all add: ARM_H.maskCapRights_def
                                acap_rights_update_def Let_def isCap_simps) apply (simp add: maskVMRights_def vmrights_map_def rights_mask_map_def
                   validate_vm_rights_def vm_read_write_def vm_read_only_def
                   vm_kernel_only_def ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. acap_relation c c' \<Longrightarrow> cap_relation (cap.ArchObjectCap (acap_rights_update (acap_rights c \<inter> msk) c)) (Arch.maskCapRights (rights_mask_map msk) c') proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 x34 x35. \<lbrakk>c' = arch_capability.PageCap x31 x32 (vmrights_map x33) x34 x35; c = arch_cap.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> maskVMRights (vmrights_map x33) (rights_mask_map msk) = vmrights_map (validate_vm_rights (x33 \<inter> msk)) proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma pte_relation'_Invalid_inv [simp]:
  "pte_relation' x ARM_H.pte.InvalidPTE = (x = ARM_A.pte.InvalidPTE)" by (cases x) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pte_relation' x ARM_H.InvalidPTE = (x = ARM_A.InvalidPTE)
theory ArchAcc_R

lemma asidHighBitsOf [simp]:
  "asidHighBitsOf asid = ucast (asid_high_bits_of asid)" apply (simp add: asidHighBitsOf_def asid_high_bits_of_def asidHighBits_def) apply word_eqI_solve done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asidHighBitsOf asid = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) proof (prove)
goal (1 subgoal):
 1. (asid >> local.asid_low_bits) && mask 7 = UCAST(7 \<rightarrow> 32) (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma page_directory_at_lift:
  "corres_inst_eq ptr ptr' \<Longrightarrow> \<forall>s s'. (s, s') \<in> state_relation \<longrightarrow> True \<longrightarrow>
  (pspace_aligned s \<and> page_directory_at ptr s) \<longrightarrow>
  pspace_distinct' s' \<longrightarrow> page_directory_at' ptr' s'" by (fastforce simp: corres_inst_eq_def intro!: page_directory_at_state_relation )

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_inst_eq ptr ptr' \<Longrightarrow> \<forall>s s'. (s, s') \<in> state_relation \<longrightarrow> True \<longrightarrow> pspace_aligned s \<and> typ_at (AArch APageDirectory) ptr s \<longrightarrow> pspace_distinct' s' \<longrightarrow> page_directory_at' ptr' s'
theory ArchAcc_R

lemma getASID_wp:
  "\<lbrace>\<lambda>s. \<forall>ko. ko_at' (ko::asidpool) p s \<longrightarrow> Q ko s\<rbrace> getObject p \<lbrace>Q\<rbrace>" by (clarsimp simp: getObject_def split_def loadObject_default_def
                     archObjSize_def in_magnitude_check pageBits_def
                     projectKOs in_monad valid_def obj_at'_def objBits_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ko. ko_at' ko p s \<longrightarrow> Q ko s\<rbrace> getObject p \<lbrace>Q\<rbrace>
theory ArchAcc_R

lemma find_pd_for_asid_corres':
  "corres (lfr \<oplus> (=)) (vspace_at_asid asid pd and valid_vspace_objs
                           and pspace_aligned and  K (0 < asid \<and> asid \<le> mask asidBits))
                       (pspace_aligned' and pspace_distinct' and no_0_obj')
                       (find_pd_for_asid asid) (findPDForASID asid)" apply (rule corres_guard_imp, rule find_pd_for_asid_corres) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (lfr \<oplus> (=)) (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits)) (pspace_aligned' and pspace_distinct' and no_0_obj') (find_pd_for_asid asid) (findPDForASID asid) proof (prove)
goal (3 subgoals):
 1. asid = asid
 2. \<And>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid ?pd4 s) and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits)) s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj') s proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma setObject_arch:
  assumes X: "\<And>p q n ko. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> updateObject val p q n ko \<lbrace>\<lambda>rv s. P (ksArchState s)\<rbrace>"
  shows "\<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setObject t val \<lbrace>\<lambda>rv s. P (ksArchState s)\<rbrace>" apply (simp add: setObject_def split_def) apply (wp X | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setObject t val \<lbrace>\<lambda>rv s. P (ksArchState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t ps));
obj' <- updateObject val (snd p) t (fst p) (snd (lookupAround2 t ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksArchState s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma setObject_ASID_arch [wp]:
  "\<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setObject p (v::asidpool) \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace>" apply (rule setObject_arch) apply (simp add: updateObject_default_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setObject p v \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> updateObject v p q n ko \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> do y <- assert (q = n);
_ <- projectKO p;
y <- alignCheck q (objBits v);
y <- magnitudeCheck q ko (objBits v);
return (KOArch (KOASIDPool v))
od \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko s. P (ksArchState s) \<Longrightarrow> q = n \<longrightarrow> P (ksArchState s) proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma setObject_PDE_arch [wp]:
  "\<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setObject p (v::pde) \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace>" apply (rule setObject_arch) apply (simp add: updateObject_default_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setObject p v \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> updateObject v p q n ko \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> do y <- assert (q = n);
_ <- projectKO p;
y <- alignCheck q (objBits v);
y <- magnitudeCheck q ko (objBits v);
return (KOArch (KOPDE v))
od \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko s. P (ksArchState s) \<Longrightarrow> q = n \<longrightarrow> P (ksArchState s) proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma setObject_PTE_arch [wp]:
  "\<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setObject p (v::pte) \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace>" apply (rule setObject_arch) apply (simp add: updateObject_default_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setObject p v \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> updateObject v p q n ko \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> do y <- assert (q = n);
_ <- projectKO p;
y <- alignCheck q (objBits v);
y <- magnitudeCheck q ko (objBits v);
return (KOArch (KOPTE v))
od \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko s. P (ksArchState s) \<Longrightarrow> q = n \<longrightarrow> P (ksArchState s) proof (prove)
goal:
No subgoals!
theory ArchAcc_R

lemma setObject_ASID_valid_arch [wp]:
  "\<lbrace>valid_arch_state'\<rbrace> setObject p (v::asidpool) \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>" by (rule valid_arch_state_lift'; wp)

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