kings-crown/FVELER_Isabelle huggingface dataset:
theory VSpace_C

lemma ucast_asid_high_bits_is_shift:
  "asid \<le> mask asid_bits \<Longrightarrow> ucast (asid_high_bits_of asid) = (asid >> asid_low_bits)" apply (simp add: mask_def upper_bits_unset_is_l2p_32 [symmetric]) apply (simp add: asid_high_bits_of_def) apply (rule word_eqI) apply (simp add: word_size nth_shiftr nth_ucast asid_low_bits_def asid_bits_def word_bits_def) apply (erule_tac x="10+n" in allE) apply simp apply (case_tac "n < 7", simp)  (*asid_low_bits*)
   apply (clarsimp simp add: linorder_not_less) apply (frule test_bit_size) apply (simp add: word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid \<le> mask local.asid_bits \<Longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits proof (prove)
goal (1 subgoal):
 1. \<forall>n'\<ge>local.asid_bits. n' < word_bits \<longrightarrow> \<not> asid !! n' \<Longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits proof (prove)
goal (1 subgoal):
 1. \<forall>n'\<ge>local.asid_bits. n' < word_bits \<longrightarrow> \<not> asid !! n' \<Longrightarrow> UCAST(7 \<rightarrow> 32) (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = asid >> local.asid_low_bits proof (prove)
goal (1 subgoal):
 1. \<And>n. \<forall>n'\<ge>local.asid_bits. n' < word_bits \<longrightarrow> \<not> asid !! n' \<Longrightarrow> n < size (UCAST(7 \<rightarrow> 32) (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits))) \<longrightarrow> UCAST(7 \<rightarrow> 32) (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) !! n = (asid >> local.asid_low_bits) !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<forall>n'\<ge>17. n' < 32 \<longrightarrow> \<not> asid !! n' \<Longrightarrow> n < 32 \<longrightarrow> (n < 7 \<and> asid !! (10 + n)) = asid !! (10 + n) proof (prove)
goal (1 subgoal):
 1. \<And>n. 17 \<le> 10 + n \<longrightarrow> 10 + n < 32 \<longrightarrow> \<not> asid !! (10 + n) \<Longrightarrow> n < 32 \<longrightarrow> (n < 7 \<and> asid !! (10 + n)) = asid !! (10 + n) proof (prove)
goal (1 subgoal):
 1. \<And>n. 7 \<le> n \<longrightarrow> n < 22 \<longrightarrow> \<not> asid !! (10 + n) \<Longrightarrow> n < 32 \<longrightarrow> (n < 7 \<and> asid !! (10 + n)) = asid !! (10 + n) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>7 \<le> n \<longrightarrow> n < 22 \<longrightarrow> \<not> asid !! (10 + n); \<not> n < 7\<rbrakk> \<Longrightarrow> n < 32 \<longrightarrow> (n < 7 \<and> asid !! (10 + n)) = asid !! (10 + n) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>7 \<le> n \<longrightarrow> n < 22 \<longrightarrow> \<not> asid !! (10 + n); \<not> n < 7\<rbrakk> \<Longrightarrow> n < 32 \<longrightarrow> (n < 7 \<and> asid !! (10 + n)) = asid !! (10 + n) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < 32; asid !! (10 + n); 22 \<le> n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < 32; asid !! (10 + n); 22 \<le> n; 10 + n < size asid\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma cap_small_frame_cap_get_capFMappedASID_spec:
  "\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_small_frame_cap\<rbrace>
         Call cap_small_frame_cap_get_capFMappedASID_'proc
       \<lbrace>\<acute>ret__unsigned_long =
             (cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift \<^bsup>s\<^esup>cap) << asidLowBits)
               + (cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift \<^bsup>s\<^esup>cap))\<rbrace>" apply vcg apply (clarsimp simp: asidLowBits_def Kernel_C.asidLowBits_def word_sle_def
                        asid_low_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrace> Call cap_small_frame_cap_get_capFMappedASID_'proc \<lbrace>\<acute>ret__unsigned_long = (cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift \<^bsup>s\<^esup>cap) << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift \<^bsup>s\<^esup>cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<and> (\<forall>ret__unsigned. ret__unsigned = cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap) \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<and> (\<forall>ret__unsigned. ret__unsigned = cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap) \<longrightarrow> 0 \<le>s Kernel_C.asidLowBits \<and> Kernel_C.asidLowBits <s 0x20 \<and> UCAST(32 \<rightarrow> 32) ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap) << unat Kernel_C.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap)) = (cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap) << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap))) proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma cap_frame_cap_get_capFMappedASID_spec:
  "\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_frame_cap\<rbrace>
         Call cap_frame_cap_get_capFMappedASID_'proc
       \<lbrace>\<acute>ret__unsigned_long =
             (cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift \<^bsup>s\<^esup>cap) << asidLowBits)
               + (cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift \<^bsup>s\<^esup>cap))\<rbrace>" apply vcg apply (clarsimp simp: asidLowBits_def Kernel_C.asidLowBits_def word_sle_def
                        asid_low_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrace> Call cap_frame_cap_get_capFMappedASID_'proc \<lbrace>\<acute>ret__unsigned_long = (cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift \<^bsup>s\<^esup>cap) << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift \<^bsup>s\<^esup>cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<Longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<and> (\<forall>ret__unsigned. ret__unsigned = cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift cap) \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<and> (\<forall>ret__unsigned. ret__unsigned = cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift cap) \<longrightarrow> 0 \<le>s Kernel_C.asidLowBits \<and> Kernel_C.asidLowBits <s 0x20 \<and> UCAST(32 \<rightarrow> 32) ((cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift cap) << unat Kernel_C.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift cap)) = (cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift cap) << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift cap))) proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma generic_frame_cap_get_capFIsMapped_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_small_frame_cap \<or>
                cap_get_tag \<acute>cap = scast cap_frame_cap\<rbrace>
       Call generic_frame_cap_get_capFIsMapped_'proc
       \<lbrace>\<acute>ret__unsigned_long = (if generic_frame_cap_get_capFMappedASID_CL (cap_lift \<^bsup>s\<^esup>cap) \<noteq> 0 then 1 else 0)\<rbrace>" apply vcg apply (clarsimp simp: generic_frame_cap_get_capFMappedASID_CL_def if_distrib [where f=scast]
                  cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrace> Call generic_frame_cap_get_capFIsMapped_'proc \<lbrace>\<acute>ret__unsigned_long = (if generic_frame_cap_get_capFMappedASID_CL (cap_lift \<^bsup>s\<^esup>cap) \<noteq> 0 then 1 else 0)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<Longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap) \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) (if generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) \<noteq> SCAST(32 signed \<rightarrow> 32) 0 then 1 else 0) = (if generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) \<noteq> 0 then 1 else 0)) proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma clift_ptr_safe:
  "clift (h, x) ptr = Some a
  \<Longrightarrow> ptr_safe ptr x" by (erule lift_t_ptr_safe[where g = c_guard])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (h, x) ptr = Some a \<Longrightarrow> ptr_safe ptr x
theory VSpace_C

lemma ccorres_abstract_cleanup:
  "ccorres r xf G G' hs a c \<Longrightarrow>
   ccorres r xf G ({s. s \<in> S \<longrightarrow> s \<in> G'} \<inter> S) hs a c" by (fastforce intro: ccorres_guard_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf G G' hs a c \<Longrightarrow> ccorres r xf G ({s. s \<in> S \<longrightarrow> s \<in> G'} \<inter> S) hs a c
theory VSpace_C

lemma pde_case_isPageTablePDE:
  "(case pde of PageTablePDE a b c \<Rightarrow> fn a b c | _ \<Rightarrow> g)
    = (if isPageTablePDE pde then fn (pdeTable pde) (pdeParity pde) (pdeDomain pde) else g)" by (cases pde, simp_all add: isPageTablePDE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case pde of ARM_H.PageTablePDE a b c \<Rightarrow> fn a b c | _ \<Rightarrow> g) = (if isPageTablePDE pde then fn (pdeTable pde) (pdeParity pde) (pdeDomain pde) else g)
theory VSpace_C

lemma ptrFromPAddr_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
   Call ptrFromPAddr_'proc
   \<lbrace>\<acute>ret__ptr_to_void =  Ptr (ptrFromPAddr (paddr_' s))\<rbrace>" apply vcg apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call ptrFromPAddr_'proc \<lbrace>\<acute>ret__ptr_to_void = PTR(unit) (ptrFromPAddr \<^bsup>s\<^esup>paddr)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>paddr. \<forall>ret__unsigned_long. ret__unsigned_long = physBase \<longrightarrow> PTR(unit) (paddr + (UCAST(32 \<rightarrow> 32) 0xE0000000 - physBase)) = PTR(unit) (ptrFromPAddr paddr) proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma addrFromPPtr_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
   Call addrFromPPtr_'proc
   \<lbrace>\<acute>ret__unsigned_long = addrFromPPtr (ptr_val (pptr_' s))\<rbrace>" apply vcg apply (simp add: addrFromPPtr_def pptrBaseOffset_def pptrBase_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call addrFromPPtr_'proc \<lbrace>\<acute>ret__unsigned_long = addrFromPPtr (ptr_val \<^bsup>s\<^esup>pptr)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>pptr. \<forall>ret__unsigned_long. ret__unsigned_long = physBase \<longrightarrow> ptr_val pptr - (UCAST(32 \<rightarrow> 32) 0xE0000000 - physBase) = addrFromPPtr (ptr_val pptr) proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma addrFromKPPtr_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
   Call addrFromKPPtr_'proc
   \<lbrace>\<acute>ret__unsigned_long = addrFromKPPtr (ptr_val (pptr_' s))\<rbrace>" apply vcg apply (simp add: addrFromKPPtr_def kernelELFBaseOffset_def kernelELFPAddrBase_def
                   kernelELFBase_def pptrBase_def mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call addrFromKPPtr_'proc \<lbrace>\<acute>ret__unsigned_long = addrFromKPPtr (ptr_val \<^bsup>s\<^esup>pptr)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>pptr. \<forall>ret__unsigned_long. ret__unsigned_long = physBase \<longrightarrow> (\<forall>ret__unsigned_long. ret__unsigned_long = physBase \<longrightarrow> 0 \<le>s 0x16 \<and> 0x16 <s 0x20 \<and> ptr_val pptr - (UCAST(32 \<rightarrow> 32) 0xE0000000 + (physBase && (1 << unat 0x16) - 1) - physBase) = addrFromKPPtr (ptr_val pptr)) proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma invalidateTranslationASIDLocal_ccorres:
  "ccorres dc xfdc \<top> (\<lbrace>\<acute>hw_asid = hw_asid \<rbrace>) []
           (doMachineOp (invalidateLocalTLB_ASID hw_asid))
           (Call invalidateTranslationASIDLocal_'proc)" apply cinit' apply (ctac (no_vcg) add: invalidateLocalTLB_ASID_ccorres) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>hw_asid = hw_asid\<rbrace> [] (doMachineOp (invalidateLocalTLB_ASID hw_asid)) (Call invalidateTranslationASIDLocal_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q5 ?Q'5 [SKIP] (doMachineOp (invalidateLocalTLB_ASID hw_asid)) (CALL invalidateLocalTLB_ASID_'proc(\<acute>hw_asid))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>hw_asid = hw_asid\<rbrace>\<rbrakk> \<Longrightarrow> ?Q5 s \<and> s' \<in> ?Q'5 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>hw_asid = hw_asid\<rbrace>\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. hw_asid_'_update (\<lambda>_. hw_asid_' s) s \<in> \<lbrace>\<acute>hw_asid = hw_asid\<rbrace>} proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma invalidateTranslationASID_ccorres:
  "ccorres dc xfdc \<top> (\<lbrace>\<acute>hw_asid = hw_asid \<rbrace>) []
           (doMachineOp (invalidateLocalTLB_ASID hw_asid))
           (Call invalidateTranslationASID_'proc)" apply cinit' apply (ctac (no_vcg) add: invalidateTranslationASIDLocal_ccorres) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>hw_asid = hw_asid\<rbrace> [] (doMachineOp (invalidateLocalTLB_ASID hw_asid)) (Call invalidateTranslationASID_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q43 ?Q'43 [SKIP] (doMachineOp (invalidateLocalTLB_ASID hw_asid)) (CALL invalidateTranslationASIDLocal_'proc(\<acute>hw_asid))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>hw_asid = hw_asid\<rbrace>\<rbrakk> \<Longrightarrow> ?Q43 s \<and> s' \<in> ?Q'43 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>hw_asid = hw_asid\<rbrace>\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. hw_asid_'_update (\<lambda>_. hw_asid_' s) s \<in> \<lbrace>\<acute>hw_asid = hw_asid\<rbrace>} proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma rf_sr_armKSASIDTable_rel:
  "(s, s') \<in> rf_sr
    \<Longrightarrow> array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s))
                               (armKSHWASIDTable_' (globals s'))" by (clarsimp simp: rf_sr_def cstate_relation_def
                     Let_def carch_state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> rf_sr \<Longrightarrow> array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s'))
theory VSpace_C

lemma rf_sr_armKSNextASID:
  "(s, s') \<in> rf_sr \<Longrightarrow> armKSNextASID_' (globals s') = armKSNextASID (ksArchState s)" by (clarsimp simp: rf_sr_def cstate_relation_def
                     Let_def carch_state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> rf_sr \<Longrightarrow> armKSNextASID_' (globals s') = armKSNextASID (ksArchState s)
theory VSpace_C

lemma all_invs_but_ct_idle_or_in_cur_domain_valid_pde_mappings':
  "all_invs_but_ct_idle_or_in_cur_domain' s \<longrightarrow> valid_pde_mappings' s" by (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. all_invs_but_ct_idle_or_in_cur_domain' s \<longrightarrow> valid_pde_mappings' s
theory VSpace_C

lemma invs_valid_pde_mappings':
  "invs' s \<longrightarrow> valid_pde_mappings' s" by (clarsimp simp: invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<longrightarrow> valid_pde_mappings' s
theory VSpace_C

lemma ccorres_h_t_valid_armKSGlobalPD:
  "ccorres r xf P P' hs f (f' ;; g') \<Longrightarrow>
   ccorres r xf P P' hs f (Guard C_Guard {s'. s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr} f';; g')" apply (rule ccorres_guard_imp2) apply (rule ccorres_move_c_guards[where P = \<top>]) apply clarsimp apply assumption apply simp by (simp add:rf_sr_def cstate_relation_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf P P' hs f (f';;
g') \<Longrightarrow> ccorres r xf P P' hs f (Guard C_Guard {s'. s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr} f';;
g') proof (prove)
goal (2 subgoals):
 1. ccorres r xf P P' hs f (f';;
g') \<Longrightarrow> ccorres r xf ?Q ?Q' hs f (Guard C_Guard {s'. s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr} f';;
g')
 2. \<And>s s'. \<lbrakk>ccorres r xf P P' hs f (f';;
g'); (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (3 subgoals):
 1. ccorres r xf P P' hs f (f';;
g') \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<and> ?P'3 s' \<longrightarrow> s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr
 2. ccorres r xf P P' hs f (f';;
g') \<Longrightarrow> ccorres r xf ?A3 ?C'3 hs f (f';;
g')
 3. \<And>s s'. \<lbrakk>ccorres r xf P P' hs f (f';;
g'); (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> (?A3 and (\<lambda>_. True)) s \<and> s' \<in> ?C'3 \<inter> Collect ?P'3 proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>ccorres r xf P P' hs f (f';;
g'); (s, s') \<in> rf_sr; ?P'3 s'\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr
 2. ccorres r xf P P' hs f (f';;
g') \<Longrightarrow> ccorres r xf ?A3 ?C'3 hs f (f';;
g')
 3. \<And>s s'. \<lbrakk>ccorres r xf P P' hs f (f';;
g'); (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> (?A3 and (\<lambda>_. True)) s \<and> s' \<in> ?C'3 \<inter> Collect ?P'3 proof (prove)
goal (2 subgoals):
 1. ccorres r xf P P' hs f (f';;
g') \<Longrightarrow> ccorres r xf ?A3 ?C'3 hs f (f';;
g')
 2. \<And>s s'. \<lbrakk>ccorres r xf P P' hs f (f';;
g'); (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> (?A3 and (\<lambda>_. True)) s \<and> s' \<in> ?C'3 \<inter> {s'. s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>ccorres r xf P P' hs f (f';;
g'); (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> (P and (\<lambda>_. True)) s \<and> s' \<in> P' \<inter> {s'. s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr}
theory VSpace_C

lemma framesize_from_to_H:
  "gen_framesize_to_H (framesize_from_H sz) = sz" by (simp add: gen_framesize_to_H_def framesize_from_H_def
                Kernel_C.ARMSmallPage_def Kernel_C.ARMLargePage_def
                Kernel_C.ARMSection_def Kernel_C.ARMSuperSection_def
           split: if_split vmpage_size.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gen_framesize_to_H (framesize_from_H sz) = sz
theory VSpace_C

lemma dmo_flushtype_case:
  "(doMachineOp (case t of
    ARM_H.flush_type.Clean \<Rightarrow> f
  | ARM_H.flush_type.Invalidate \<Rightarrow> g
  | ARM_H.flush_type.CleanInvalidate \<Rightarrow> h
  | ARM_H.flush_type.Unify \<Rightarrow> i)) =
  (case t of
    ARM_H.flush_type.Clean \<Rightarrow> doMachineOp f
  | ARM_H.flush_type.Invalidate \<Rightarrow> doMachineOp g
  | ARM_H.flush_type.CleanInvalidate \<Rightarrow> doMachineOp h
  | ARM_H.flush_type.Unify \<Rightarrow> doMachineOp i)" by (case_tac "t", simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doMachineOp (case t of ARM_H.Clean \<Rightarrow> f | ARM_H.Invalidate \<Rightarrow> g | ARM_H.CleanInvalidate \<Rightarrow> h | ARM_H.Unify \<Rightarrow> i) = (case t of ARM_H.Clean \<Rightarrow> doMachineOp f | ARM_H.Invalidate \<Rightarrow> doMachineOp g | ARM_H.CleanInvalidate \<Rightarrow> doMachineOp h | ARM_H.Unify \<Rightarrow> doMachineOp i)
theory VSpace_C

lemma register_from_H_bound[simp]:
  "unat (register_from_H v) < 20" by (cases v, simp_all add: "StrictC'_register_defs")

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (register_from_H v) < 20
theory VSpace_C

lemma register_from_H_inj:
  "inj register_from_H" apply (rule inj_onI) apply (case_tac x) by (case_tac y, simp_all add: "StrictC'_register_defs")+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj register_from_H proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; register_from_H x = register_from_H y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (20 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; register_from_H x = register_from_H y; x = register.R0\<rbrakk> \<Longrightarrow> x = y
 2. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; register_from_H x = register_from_H y; x = register.R1\<rbrakk> \<Longrightarrow> x = y
 3. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; register_from_H x = register_from_H y; x = register.R2\<rbrakk> \<Longrightarrow> x = y
 4. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; register_from_H x = register_from_H y; x = register.R3\<rbrakk> \<Longrightarrow> x = y
 5. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; register_from_H x = register_from_H y; x = register.R4\<rbrakk> \<Longrightarrow> x = y
 6. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; register_from_H x = register_from_H y; x = register.R5\<rbrakk> \<Longrightarrow> x = y
 7. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; register_from_H x = register_from_H y; x = register.R6\<rbrakk> \<Longrightarrow> x = y
 8. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; register_from_H x = register_from_H y; x = register.R7\<rbrakk> \<Longrightarrow> x = y
 9. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; register_from_H x = register_from_H y; x = register.R8\<rbrakk> \<Longrightarrow> x = y
 10. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; register_from_H x = register_from_H y; x = register.R9\<rbrakk> \<Longrightarrow> x = y
A total of 20 subgoals...