kings-crown/FVELER_Isabelle huggingface dataset:
theory Schedule_C

lemma ceqv_remove_tail_Guard_Skip:
  "\<lbrakk> \<And>s. s \<in> G \<rbrakk> \<Longrightarrow> ceqv Gamma xf v s s' (a ;; Guard F G Skip) a" apply (rule ceqvI) apply (safe elim!: exec_Normal_elim_cases) apply (case_tac s'a, auto intro: exec.intros elim!: exec_Normal_elim_cases)[1] apply (case_tac s', auto intro: exec.intros elim!: exec_Normal_elim_cases)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. s \<in> G) \<Longrightarrow> ceqv Gamma xf v s s' (a;;
Guard F G SKIP) a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. s \<in> G; xf s = v\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>a;;
Guard F G SKIP,Normal s\<rangle> \<Rightarrow> s' = Gamma\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s'a. \<lbrakk>\<And>s. s \<in> G; v = xf s; Gamma\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'a; Gamma\<turnstile> \<langle>Guard F G SKIP,s'a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'
 2. \<lbrakk>\<And>s. s \<in> G; v = xf s; Gamma\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>a;;
Guard F G SKIP,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. s \<in> G; v = xf s; Gamma\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>a;;
Guard F G SKIP,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory Schedule_C

lemma switchToThread_ccorres':
  "ccorres dc xfdc
           (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t)
           (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>)
           hs
           (switchToThread t)
           (Call switchToThread_'proc)" apply (rule ccorres_guard_imp2) apply (ctac (no_vcg) add: switchToThread_ccorres) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>) hs (global.switchToThread t) (Call switchToThread_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q ?Q' hs (global.switchToThread t) (Call switchToThread_'proc)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) s; s' \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) s; s' \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>\<rbrakk> \<Longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) s \<and> s' \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_C

lemma ksDomSched_length_dom_relation[simp]:
  "\<lbrakk>cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule \<rbrakk> \<Longrightarrow> length (kernel_state.ksDomSchedule s) = unat (ksDomScheduleLength)" apply (auto simp: cstate_relation_def cdom_schedule_relation_def Let_def ksDomScheduleLength_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule \<Longrightarrow> length (kernel_state.ksDomSchedule s) = unat kernel_all_global_addresses.ksDomScheduleLength proof (prove)
goal:
No subgoals!
theory Schedule_C

lemma map_to_tcbs_upd:
  "map_to_tcbs ((ksPSpace s)(t \<mapsto> KOTCB tcb')) = (map_to_tcbs (ksPSpace s))(t \<mapsto> tcb')" apply (rule ext) apply (clarsimp simp: map_comp_def projectKOs split: option.splits if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_to_tcbs ((ksPSpace s)(t \<mapsto> KOTCB tcb')) = (map_to_tcbs (ksPSpace s))(t \<mapsto> tcb') proof (prove)
goal (1 subgoal):
 1. \<And>x. map_to_tcbs ((ksPSpace s)(t \<mapsto> KOTCB tcb')) x = ((map_to_tcbs (ksPSpace s))(t \<mapsto> tcb')) x proof (prove)
goal:
No subgoals!
theory Schedule_C

lemma cep_relations_drop_fun_upd:
  "\<lbrakk> f x = Some v; tcbEPNext_C v' = tcbEPNext_C v; tcbEPPrev_C v' = tcbEPPrev_C v \<rbrakk>
      \<Longrightarrow> cendpoint_relation (f (x \<mapsto> v')) = cendpoint_relation f"
  "\<lbrakk> f x = Some v; tcbEPNext_C v' = tcbEPNext_C v; tcbEPPrev_C v' = tcbEPPrev_C v \<rbrakk>
      \<Longrightarrow> cnotification_relation (f (x \<mapsto> v')) = cnotification_relation f" by (intro ext cendpoint_relation_upd_tcb_no_queues[where thread=x]
                cnotification_relation_upd_tcb_no_queues[where thread=x]
          | simp split: if_split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>f x = Some v; tcbEPNext_C v' = tcbEPNext_C v; tcbEPPrev_C v' = tcbEPPrev_C v\<rbrakk> \<Longrightarrow> cendpoint_relation (f(x \<mapsto> v')) = cendpoint_relation f) &&& (\<lbrakk>f x = Some v; tcbEPNext_C v' = tcbEPNext_C v; tcbEPPrev_C v' = tcbEPPrev_C v\<rbrakk> \<Longrightarrow> cnotification_relation (f(x \<mapsto> v')) = cnotification_relation f)
theory Arch_C

lemma cap_case_PageDirectoryCap2:
  "(case cap of ArchObjectCap (PageDirectoryCap pd mapdata)
                   \<Rightarrow> f pd mapdata | _ \<Rightarrow> g)
   = (if isArchObjectCap cap \<and> isPageDirectoryCap (capCap cap)
      then f (capPDBasePtr (capCap cap)) (capPDMappedASID (capCap cap))
      else g)" by (simp add: isCap_simps
         split: capability.split arch_capability.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd mapdata) \<Rightarrow> f pd mapdata | capability.ArchObjectCap _ \<Rightarrow> g | _ \<Rightarrow> g) = (if isArchObjectCap cap \<and> isPageDirectoryCap (capCap cap) then f (capPDBasePtr (capCap cap)) (capPDMappedASID (capCap cap)) else g)
theory Arch_C

lemma ap_eq_D:
  "x \<lparr>array_C := arr'\<rparr> = asid_pool_C.asid_pool_C arr \<Longrightarrow> arr' = arr" by (cases x) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. array_C_update (\<lambda>_. arr') x = asid_pool_C.asid_pool_C arr \<Longrightarrow> arr' = arr
theory Arch_C

lemma ghost_assertion_data_get_gs_clear_region:
  "gs_get_assn proc (gs_clear_region addr n gs) = gs_get_assn proc gs" by (clarsimp simp: ghost_assertion_data_get_def gs_clear_region_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gs_get_assn proc (gs_clear_region addr n gs) = gs_get_assn proc gs
theory Arch_C

lemma ghost_assertion_size_logic_flex:
  "unat (sz :: word32) \<le> gsMaxObjectSize s
    \<Longrightarrow> (s, \<sigma>') \<in> rf_sr
    \<Longrightarrow> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' (globals \<sigma>'))
        = gs_get_assn cap_get_capSizeBits_'proc gs
    \<Longrightarrow> gs_get_assn cap_get_capSizeBits_'proc gs = 0 \<or>
            sz \<le> gs_get_assn cap_get_capSizeBits_'proc gs" by (metis ghost_assertion_size_logic)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat sz \<le> gsMaxObjectSize s; (s, \<sigma>') \<in> rf_sr; gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' (globals \<sigma>')) = gs_get_assn cap_get_capSizeBits_'proc gs\<rbrakk> \<Longrightarrow> gs_get_assn cap_get_capSizeBits_'proc gs = 0 \<or> sz \<le> gs_get_assn cap_get_capSizeBits_'proc gs
theory Arch_C

lemma slotcap_in_mem_PageDirectory:
  "\<lbrakk> slotcap_in_mem cap slot (ctes_of s); (s, s') \<in> rf_sr \<rbrakk>
       \<Longrightarrow> \<exists>v. cslift s' (cte_Ptr slot) = Some v
           \<and> (cap_get_tag (cte_C.cap_C v) = scast cap_page_directory_cap)
              = (isArchObjectCap cap \<and> isPageDirectoryCap (capCap cap))
           \<and> (isArchObjectCap cap \<and> isPageDirectoryCap (capCap cap)
                  \<longrightarrow> ccap_relation cap (cte_C.cap_C v))" apply (clarsimp simp: slotcap_in_mem_def) apply (erule(1) cmap_relationE1[OF cmap_relation_cte]) apply (clarsimp dest!: ccte_relation_ccap_relation) apply (simp add: cap_get_tag_isCap_ArchObject2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slotcap_in_mem cap slot (ctes_of s); (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>v. cslift s' (cte_Ptr slot) = Some v \<and> (cap_get_tag (cte_C.cap_C v) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) = (isArchObjectCap cap \<and> isPageDirectoryCap (capCap cap)) \<and> (isArchObjectCap cap \<and> isPageDirectoryCap (capCap cap) \<longrightarrow> ccap_relation cap (cte_C.cap_C v)) proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s slot = Some cte; cap = cteCap cte\<rbrakk> \<Longrightarrow> \<exists>v. cslift s' (cte_Ptr slot) = Some v \<and> (cap_get_tag (cte_C.cap_C v) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) = (isArchObjectCap (cteCap cte) \<and> isPageDirectoryCap (capCap (cteCap cte))) \<and> (isArchObjectCap (cteCap cte) \<and> isPageDirectoryCap (capCap (cteCap cte)) \<longrightarrow> ccap_relation (cteCap cte) (cte_C.cap_C v)) proof (prove)
goal (1 subgoal):
 1. \<And>cte y'. \<lbrakk>ctes_of s slot = Some cte; cap = cteCap cte; ctes_of s slot = Some cte; ccte_relation cte y'; cslift s' (cte_Ptr slot) = Some y'\<rbrakk> \<Longrightarrow> \<exists>v. cslift s' (cte_Ptr slot) = Some v \<and> (cap_get_tag (cte_C.cap_C v) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) = (isArchObjectCap (cteCap cte) \<and> isPageDirectoryCap (capCap (cteCap cte))) \<and> (isArchObjectCap (cteCap cte) \<and> isPageDirectoryCap (capCap (cteCap cte)) \<longrightarrow> ccap_relation (cteCap cte) (cte_C.cap_C v)) proof (prove)
goal (1 subgoal):
 1. \<And>cte y'. \<lbrakk>cap = cteCap cte; ctes_of s slot = Some cte; cslift s' (cte_Ptr slot) = Some y'; ccap_relation (cteCap cte) (cte_C.cap_C y')\<rbrakk> \<Longrightarrow> (cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) = (isArchObjectCap (cteCap cte) \<and> isPageDirectoryCap (capCap (cteCap cte))) proof (prove)
goal:
No subgoals!
theory Arch_C

lemma checkVPAlignment_spec:
  "\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. \<acute>sz < 4\<rbrace> Call checkVPAlignment_'proc
          {t. ret__unsigned_long_' t = from_bool
               (vmsz_aligned' (w_' s) (gen_framesize_to_H (sz_' s)))}" apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: mask_eq_iff_w2p word_size) apply (rule conjI) apply (simp add: pageBitsForSize_def split: vmpage_size.split) apply (simp add: vmsz_aligned'_def is_aligned_mask mask_def
            split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. \<acute>sz < 4\<rbrace> Call checkVPAlignment_'proc \<lbrace>\<acute>ret__unsigned_long = from_bool (vmsz_aligned' \<^bsup>s\<^esup>w (gen_framesize_to_H \<^bsup>s\<^esup>sz))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. \<acute>sz < 4\<rbrace> \<subseteq> \<lbrace>\<acute>sz && mask 2 = \<acute>sz \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned_long = word_of_nat (pageBitsForSize (gen_framesize_to_H \<acute>sz)) \<longrightarrow> word_of_nat (pageBitsForSize (gen_framesize_to_H \<acute>sz)) < SCAST(32 signed \<rightarrow> 32) 0x20 \<and> SCAST(32 signed \<rightarrow> 32) (if \<acute>w && (1 << unat (word_of_nat (pageBitsForSize (gen_framesize_to_H \<acute>sz)))) - 1 = SCAST(32 signed \<rightarrow> 32) 0 then 1 else 0) = from_bool (vmsz_aligned' \<^bsup>s\<^esup>w (gen_framesize_to_H \<^bsup>s\<^esup>sz)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x t. \<lbrakk>sz_' x < 4; ret__unsigned_long_' t = word_of_nat (pageBitsForSize (gen_framesize_to_H (sz_' x)))\<rbrakk> \<Longrightarrow> word_of_nat (pageBitsForSize (gen_framesize_to_H (sz_' x))) < 0x20 \<and> (if w_' x && 2 ^ pageBitsForSize (gen_framesize_to_H (sz_' x)) - 1 = 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (vmsz_aligned' (w_' x) (gen_framesize_to_H (sz_' x))) proof (prove)
goal (2 subgoals):
 1. \<And>x t. \<lbrakk>sz_' x < 4; ret__unsigned_long_' t = word_of_nat (pageBitsForSize (gen_framesize_to_H (sz_' x)))\<rbrakk> \<Longrightarrow> word_of_nat (pageBitsForSize (gen_framesize_to_H (sz_' x))) < 0x20
 2. \<And>x t. \<lbrakk>sz_' x < 4; ret__unsigned_long_' t = word_of_nat (pageBitsForSize (gen_framesize_to_H (sz_' x)))\<rbrakk> \<Longrightarrow> (if w_' x && 2 ^ pageBitsForSize (gen_framesize_to_H (sz_' x)) - 1 = 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (vmsz_aligned' (w_' x) (gen_framesize_to_H (sz_' x))) proof (prove)
goal (1 subgoal):
 1. \<And>x t. \<lbrakk>sz_' x < 4; ret__unsigned_long_' t = word_of_nat (pageBitsForSize (gen_framesize_to_H (sz_' x)))\<rbrakk> \<Longrightarrow> (if w_' x && 2 ^ pageBitsForSize (gen_framesize_to_H (sz_' x)) - 1 = 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (vmsz_aligned' (w_' x) (gen_framesize_to_H (sz_' x))) proof (prove)
goal:
No subgoals!
theory Arch_C

lemma createSafeMappingEntries_fold:
  "(doE
     entries \<leftarrow> createMappingEntries ptr vaddr vsz vrights attr pd;
     _ \<leftarrow> ensureSafeMapping entries;
     f entries
   odE) = (createSafeMappingEntries ptr vaddr vsz vrights attr pd >>=E f)" by (simp add: createSafeMappingEntries_def bindE_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doE entries <- createMappingEntries ptr vaddr vsz vrights attr pd;
_ <- ensureSafeMapping entries;
f entries
odE = createSafeMappingEntries ptr vaddr vsz vrights attr pd >>=E f
theory Arch_C

lemma framesize_from_H_eqs:
  "(framesize_from_H vsz = scast Kernel_C.ARMSmallPage) = (vsz = ARMSmallPage)"
  "(framesize_from_H vsz = scast Kernel_C.ARMLargePage) = (vsz = ARMLargePage)"
  "(framesize_from_H vsz = scast Kernel_C.ARMSection) = (vsz = ARMSection)"
  "(framesize_from_H vsz = scast Kernel_C.ARMSuperSection) = (vsz = ARMSuperSection)" by (simp add: framesize_from_H_def vm_page_size_defs split: vmpage_size.split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((framesize_from_H vsz = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage) = (vsz = Wellformed_C.ARMSmallPage) &&& (framesize_from_H vsz = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage) = (vsz = Wellformed_C.ARMLargePage)) &&& (framesize_from_H vsz = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection) = (vsz = Wellformed_C.ARMSection) &&& (framesize_from_H vsz = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) = (vsz = Wellformed_C.ARMSuperSection)
theory Arch_C

lemma pde_get_tag_alt:
  "pde_lift v = Some pdeC
    \<Longrightarrow> pde_get_tag v = (case pdeC of Pde_pde_invalid _ \<Rightarrow> scast pde_pde_invalid
          | Pde_pde_coarse _ \<Rightarrow> scast pde_pde_coarse
          | Pde_pde_section _ \<Rightarrow> scast pde_pde_section
          | Pde_pde_reserved \<Rightarrow> scast pde_pde_reserved)" by (auto simp add: pde_lift_def Let_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pde_lift v = Some pdeC \<Longrightarrow> pde_get_tag v = (case pdeC of Pde_pde_invalid x \<Rightarrow> SCAST(32 signed \<rightarrow> 32) pde_pde_invalid | Pde_pde_coarse x \<Rightarrow> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse | Pde_pde_section x \<Rightarrow> SCAST(32 signed \<rightarrow> 32) pde_pde_section | Pde_pde_reserved \<Rightarrow> SCAST(32 signed \<rightarrow> 32) pde_pde_reserved)
theory Arch_C

lemma cpde_relation_pde_case:
  "cpde_relation pde cpde
     \<Longrightarrow> (case pde of InvalidPDE \<Rightarrow> P
             | PageTablePDE _ _ _ \<Rightarrow> Q
             | SectionPDE _ _ _ _ _ _ _ \<Rightarrow> R
             | SuperSectionPDE _ _ _ _ _ _ \<Rightarrow> S)
         = (if pde_get_tag cpde = scast pde_pde_invalid then P
            else if (pde_get_tag cpde = scast pde_pde_coarse)
                     \<or> (pde_get_tag cpde \<noteq> scast pde_pde_section) then Q
            else if size_CL (pde_pde_section_lift cpde) = 0
                 then R else S)" by (clarsimp simp: cpde_relation_def Let_def pde_get_tag_alt
                     pde_tag_defs pde_pde_section_lift_def
              split: ARM_H.pde.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cpde_relation pde cpde \<Longrightarrow> (case pde of ARM_H.InvalidPDE \<Rightarrow> P | ARM_H.PageTablePDE x xa xb \<Rightarrow> Q | ARM_H.SectionPDE x xa xb xc xd xe xf \<Rightarrow> R | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> S) = (if pde_get_tag cpde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid then P else if pde_get_tag cpde = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse \<or> pde_get_tag cpde \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_section then Q else if size_CL (pde_pde_section_lift cpde) = 0 then R else S)
theory Arch_C

lemma pde_pde_section_size_0_1:
  "pde_get_tag pde = scast pde_pde_section
     \<Longrightarrow> size_CL (pde_pde_section_lift pde) = 0
            \<or> size_CL (pde_pde_section_lift pde) = 1" apply (simp add: pde_pde_section_lift_def pde_lift_pde_section) apply (rule x_less_2_0_1) apply (rule order_le_less_trans, rule word_and_le1) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<Longrightarrow> size_CL (pde_pde_section_lift pde) = 0 \<or> size_CL (pde_pde_section_lift pde) = 1 proof (prove)
goal (1 subgoal):
 1. pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<Longrightarrow> (pde_C.words_C pde.[0] >> 18) && 1 = 0 \<or> (pde_C.words_C pde.[0] >> 18) && 1 = 1 proof (prove)
goal (1 subgoal):
 1. pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<Longrightarrow> (pde_C.words_C pde.[0] >> 18) && 1 < 2 proof (prove)
goal (1 subgoal):
 1. pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<Longrightarrow> 1 < 2 proof (prove)
goal:
No subgoals!
theory Arch_C

lemma pde_bits_from_cacheable_simps [simp]:
  "shared_bit_from_cacheable (from_bool b) = s_from_cacheable b"
  "tex_bits_from_cacheable (from_bool b) = tex_from_cacheable b"
  "iwb_from_cacheable (from_bool b) =  b_from_cacheable b" by (simp_all add: shared_bit_from_cacheable_def s_from_cacheable_def
                    tex_bits_from_cacheable_def tex_from_cacheable_def
                    iwb_from_cacheable_def b_from_cacheable_def
               split: bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. shared_bit_from_cacheable (from_bool b) = s_from_cacheable b &&& tex_bits_from_cacheable (from_bool b) = tex_from_cacheable b &&& iwb_from_cacheable (from_bool b) = b_from_cacheable b
theory Arch_C

lemma pte_case_isLargePagePTE:
  "(case pte of LargePagePTE _ _ _ _ _ \<Rightarrow> P | _ \<Rightarrow> Q)
       = (if isLargePagePTE pte then P else Q)" by (simp add: isLargePagePTE_def split: ARM_H.pte.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case pte of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> P | _ \<Rightarrow> Q) = (if isLargePagePTE pte then P else Q)
theory Arch_C

lemma pte_get_tag_exhaust:
  "pte_get_tag pte = 0 \<or> pte_get_tag pte = 1" apply (simp add: pte_get_tag_def) apply word_bitwise done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pte_get_tag pte = 0 \<or> pte_get_tag pte = 1 proof (prove)
goal (1 subgoal):
 1. (pte_C.words_C pte.[0] >> Suc 0) && 1 = 0 \<or> (pte_C.words_C pte.[0] >> Suc 0) && 1 = 1 proof (prove)
goal:
No subgoals!
theory Arch_C

lemma ptr_add_uint_of_nat [simp]:
  "a  +\<^sub>p uint (of_nat b :: word32) = a  +\<^sub>p (int b)" by (clarsimp simp: CTypesDefs.ptr_add_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a +\<^sub>p uint (word_of_nat b) = a +\<^sub>p int b
theory Arch_C

lemma valid_pte_slots_lift2:
  "\<lbrakk> \<And>pt. \<lbrace> page_table_at' pt \<rbrace> f \<lbrace> \<lambda>_. page_table_at' pt \<rbrace> \<rbrakk>
    \<Longrightarrow> \<lbrace> valid_pte_slots'2 slots \<rbrace> f \<lbrace> \<lambda>_. valid_pte_slots'2 slots \<rbrace>" apply (cases slots, simp_all add: valid_pte_slots'2_def hoare_post_taut) apply clarsimp apply (wp hoare_vcg_ex_lift hoare_vcg_conj_lift | assumption)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>pt. \<lbrace>page_table_at' pt\<rbrace> f \<lbrace>\<lambda>_. page_table_at' pt\<rbrace>) \<Longrightarrow> \<lbrace>valid_pte_slots'2 slots\<rbrace> f \<lbrace>\<lambda>_. valid_pte_slots'2 slots\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>pt. \<lbrace>page_table_at' pt\<rbrace> f \<lbrace>\<lambda>_. page_table_at' pt\<rbrace>; slots = Inl a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case a of (pte, xs) \<Rightarrow> \<exists>sz\<le>4. length xs = 2 ^ sz \<and> is_aligned (hd xs) (Suc (Suc sz)) \<and> page_table_at' (hd xs && ~~ mask ptBits) s \<and> (sz = 0 \<or> sz = 4)\<rbrace> f \<lbrace>\<lambda>_ s. case a of (pte, xs) \<Rightarrow> \<exists>sz\<le>4. length xs = 2 ^ sz \<and> is_aligned (hd xs) (Suc (Suc sz)) \<and> page_table_at' (hd xs && ~~ mask ptBits) s \<and> (sz = 0 \<or> sz = 4)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>pt. \<lbrace>page_table_at' pt\<rbrace> f \<lbrace>\<lambda>_. page_table_at' pt\<rbrace>; slots = Inl (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> page_table_at' (hd b && ~~ mask ptBits) s \<and> (sz = 0 \<or> sz = 4)\<rbrace> f \<lbrace>\<lambda>_ s. \<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> page_table_at' (hd b && ~~ mask ptBits) s \<and> (sz = 0 \<or> sz = 4)\<rbrace> proof (prove)
goal:
No subgoals!
theory Arch_C

lemma valid_pde_slots_lift2:
  "\<lbrakk> \<And>pd. \<lbrace> page_directory_at' pd \<rbrace> f \<lbrace> \<lambda>_. page_directory_at' pd \<rbrace> \<rbrakk>
    \<Longrightarrow> \<lbrace> valid_pde_slots'2 slots \<rbrace> f \<lbrace> \<lambda>_. valid_pde_slots'2 slots \<rbrace>" apply (cases slots, simp_all add: valid_pde_slots'2_def hoare_post_taut) apply clarsimp apply (wp hoare_vcg_ex_lift hoare_vcg_conj_lift | assumption)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>pd. \<lbrace>page_directory_at' pd\<rbrace> f \<lbrace>\<lambda>_. page_directory_at' pd\<rbrace>) \<Longrightarrow> \<lbrace>valid_pde_slots'2 slots\<rbrace> f \<lbrace>\<lambda>_. valid_pde_slots'2 slots\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>\<And>pd. \<lbrace>page_directory_at' pd\<rbrace> f \<lbrace>\<lambda>_. page_directory_at' pd\<rbrace>; slots = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case b of (pde, xs) \<Rightarrow> (\<forall>x\<in>set xs. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd xs && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length xs = 2 ^ sz \<and> is_aligned (hd xs) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace> f \<lbrace>\<lambda>_ s. case b of (pde, xs) \<Rightarrow> (\<forall>x\<in>set xs. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd xs && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length xs = 2 ^ sz \<and> is_aligned (hd xs) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>pd. \<lbrace>page_directory_at' pd\<rbrace> f \<lbrace>\<lambda>_. page_directory_at' pd\<rbrace>; slots = Inr (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace> f \<lbrace>\<lambda>_ s. (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace> proof (prove)
goal:
No subgoals!