kings-crown/FVELER_Isabelle huggingface dataset:
theory Untyped_R

lemma createNewCaps_idlethread_ranges[wp]:
  "\<lbrace>\<lambda>s. 0 < n \<and> range_cover ptr sz (APIType_capBits tp us) n
           \<and> ksIdleThread s \<notin> {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrace>
     createNewCaps tp ptr n us d
   \<lbrace>\<lambda>rv s. \<forall>cap\<in>set rv. ksIdleThread s \<notin> capRange cap\<rbrace>" apply (rule hoare_as_subst [OF createNewCaps_idlethread]) apply (rule hoare_assume_pre) apply (rule hoare_chain, rule createNewCaps_range_helper2) apply fastforce apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 0 < n \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> ksIdleThread s \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrace> createNewCaps tp ptr n us d \<lbrace>\<lambda>rv s. \<forall>cap\<in>set rv. ksIdleThread s \<notin> capRange cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrace>\<lambda>a. 0 < n \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> v \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrace> createNewCaps tp ptr n us d \<lbrace>\<lambda>a b. \<forall>cap\<in>set a. v \<notin> capRange cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>v s. 0 < n \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> v \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<Longrightarrow> \<lbrace>\<lambda>a. 0 < n \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> v \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrace> createNewCaps tp ptr n us d \<lbrace>\<lambda>a b. \<forall>cap\<in>set a. v \<notin> capRange cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>v s sa. \<lbrakk>0 < n \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> v \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; 0 < n \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> v \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> range_cover ptr (?sz26 v s) (APIType_capBits tp us) n \<and> 0 < n
 2. \<And>v s rv sa. \<lbrakk>0 < n \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> v \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<forall>cp\<in>set rv. capRange cp \<noteq> {} \<and> capRange cp \<subseteq> {ptr..(ptr && ~~ mask (?sz26 v s)) + 2 ^ ?sz26 v s - 1}\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. v \<notin> capRange cap proof (prove)
goal (1 subgoal):
 1. \<And>v s rv sa. \<lbrakk>0 < n \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> v \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<forall>cp\<in>set rv. capRange cp \<noteq> {} \<and> capRange cp \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. v \<notin> capRange cap proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma createNewCaps_ct_active':
  "\<lbrace>ct_active' and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and K (range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)\<rbrace>
    createNewCaps ty ptr n us d
   \<lbrace>\<lambda>_. ct_active'\<rbrace>" apply (simp add: ct_in_state'_def) apply (rule hoare_pre) apply wps apply (wp createNewCaps_pred_tcb_at'[where sz=sz]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_active' and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and K (range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>_. ct_active'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. st_tcb_at' active' (ksCurThread s) s) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and (\<lambda>y. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>_ s. st_tcb_at' active' (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>_ s. st_tcb_at' active' (ksCurThread s) s\<rbrace>
 2. \<And>s. ((\<lambda>s. st_tcb_at' active' (ksCurThread s) s) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and (\<lambda>y. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. st_tcb_at' active' (ksCurThread prev_s)\<rbrace>
 2. \<And>s. ((\<lambda>s. st_tcb_at' active' (ksCurThread s) s) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and (\<lambda>y. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)) s \<Longrightarrow> ?P3 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. st_tcb_at' active' (ksCurThread s) s) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and (\<lambda>y. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)) s \<Longrightarrow> st_tcb_at' active' (ksCurThread s) s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>tcb. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<forall>d. active' (itcbState (tcb_to_itcb' (tcbDomain_update (\<lambda>_. d) tcb))) = active' (itcbState (tcb_to_itcb' tcb)))) proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma invokeUntyped_invs'[wp]:
  "\<lbrace>invs' and valid_untyped_inv' ui and ct_active'\<rbrace>
     invokeUntyped ui
   \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (wp invokeUntyped_invs''[where Q=\<top>, simplified hoare_post_taut, simplified]) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and valid_untyped_inv' ui and ct_active'\<rbrace> invokeUntyped ui \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and valid_untyped_inv' ui and ct_active') s \<Longrightarrow> (invs' and valid_untyped_inv' ui and (\<lambda>s. (case ui of Invocations_H.untyped_invocation.Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'1 s) and ct_active') s proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma inv_untyp_tcb'[wp]:
  "\<lbrace>invs' and st_tcb_at' active' tptr
         and valid_untyped_inv' ui and ct_active'\<rbrace>
     invokeUntyped ui
   \<lbrace>\<lambda>rv. tcb_at' tptr\<rbrace>" apply (rule hoare_chain [OF inv_untyp_st_tcb_at'[where tptr=tptr and P="\<top>"]]) apply (clarsimp elim!: pred_tcb'_weakenE) apply fastforce apply (clarsimp simp: pred_tcb_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and st_tcb_at' active' tptr and valid_untyped_inv' ui and ct_active'\<rbrace> invokeUntyped ui \<lbrace>\<lambda>rv. tcb_at' tptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs' and st_tcb_at' active' tptr and valid_untyped_inv' ui and ct_active') s \<Longrightarrow> (invs' and st_tcb_at' ((\<lambda>_. True) and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) tptr and valid_untyped_inv' ui and ct_active') s
 2. \<And>rv s. st_tcb_at' (\<lambda>_. True) tptr s \<Longrightarrow> tcb_at' tptr s proof (prove)
goal (2 subgoals):
 1. \<And>s st. \<lbrakk>invs' s; active' st; valid_untyped_inv' ui s; ct_active' s\<rbrakk> \<Longrightarrow> Structures_H.thread_state.Inactive \<noteq> st \<and> Structures_H.thread_state.IdleThreadState \<noteq> st
 2. \<And>rv s. st_tcb_at' (\<lambda>_. True) tptr s \<Longrightarrow> tcb_at' tptr s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. st_tcb_at' (\<lambda>_. True) tptr s \<Longrightarrow> tcb_at' tptr s proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma resetUntypedCap_IRQInactive:
  "\<lbrace>valid_irq_states'\<rbrace>
    resetUntypedCap slot
  \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>"
  (is "\<lbrace>?P\<rbrace> resetUntypedCap slot \<lbrace>?Q\<rbrace>,\<lbrace>?E\<rbrace>") apply (simp add: resetUntypedCap_def) apply (rule hoare_pre) apply (wp mapME_x_inv_wp[where P=valid_irq_states' and E="?E", THEN hoare_post_impErr]
             doMachineOp_irq_states' preemptionPoint_inv hoare_drop_imps
     | simp add: no_irq_clearMemory if_apply_def2)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> resetUntypedCap slot \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> doE cap <- liftE (getSlotCap slot);
unlessE (capFreeIndex cap = 0) (doE y <- liftE (deleteObjects (capPtr cap) (capBlockSize cap));
if capIsDevice cap \<or> capBlockSize cap < resetChunkBits then withoutPreemption $ do unless (capIsDevice cap) $ doMachineOp $ clearMemory (PPtr (fromPPtr (capPtr cap))) (1 `~shiftL~` capBlockSize cap);
updateFreeIndex slot 0
od else forME_x (reverse [capPtr cap , capPtr cap + 1 `~shiftL~` resetChunkBits .e. getFreeRef (capPtr cap) (capFreeIndex cap) - 1]) (\<lambda>addr. doE withoutPreemption $ doMachineOp $ clearMemory (PPtr (fromPPtr addr)) (1 `~shiftL~` resetChunkBits);
withoutPreemption $ updateFreeIndex slot (getFreeIndex (capPtr cap) addr);
preemptionPoint
odE)
odE)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> doE cap <- liftE (getSlotCap slot);
unlessE (capFreeIndex cap = 0) (doE y <- liftE (deleteObjects (capPtr cap) (capBlockSize cap));
if capIsDevice cap \<or> capBlockSize cap < resetChunkBits then withoutPreemption $ do unless (capIsDevice cap) $ doMachineOp $ clearMemory (PPtr (fromPPtr (capPtr cap))) (1 `~shiftL~` capBlockSize cap);
updateFreeIndex slot 0
od else forME_x (reverse [capPtr cap , capPtr cap + 1 `~shiftL~` resetChunkBits .e. getFreeRef (capPtr cap) (capFreeIndex cap) - 1]) (\<lambda>addr. doE withoutPreemption $ doMachineOp $ clearMemory (PPtr (fromPPtr addr)) (1 `~shiftL~` resetChunkBits);
withoutPreemption $ updateFreeIndex slot (getFreeIndex (capPtr cap) addr);
preemptionPoint
odE)
odE)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>
 2. \<And>s. valid_irq_states' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma inv_untyped_IRQInactive:
  "\<lbrace>valid_irq_states'\<rbrace> invokeUntyped ui
  -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>" apply (simp add: invokeUntyped_def) apply (wpsimp wp: resetUntypedCap_IRQInactive) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> invokeUntyped ui -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> case ui of Invocations_H.untyped_invocation.Retype srcSlot reset base retypeBase newType userSize destSlots isDev \<Rightarrow> doE whenE reset $ resetUntypedCap srcSlot;
withoutPreemption $ do totalObjectSize <- return (length destSlots `~shiftL~` getObjectSize newType userSize);
inRange <- return (\<lambda>x. fromPPtr retypeBase \<le> x \<and> x \<le> fromPPtr retypeBase + fromIntegral totalObjectSize - 1);
stateAssert (\<lambda>s. \<not> cNodeOverlap (gsCNodes s) inRange) [];
stateAssert (\<lambda>s. \<not> archOverlap s inRange) [];
haskell_assert (canonicalAddressAssert retypeBase) [];
freeRef <- return (retypeBase + PPtr (fromIntegral totalObjectSize));
updateFreeIndex srcSlot (getFreeIndex base freeRef);
createNewObjects newType srcSlot destSlots retypeBase userSize isDev
od
odE -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal:
No subgoals!
theory Arch_R

lemma vp_strgs':
  "valid_pspace' s \<longrightarrow> pspace_distinct' s"
  "valid_pspace' s \<longrightarrow> pspace_aligned' s"
  "valid_pspace' s \<longrightarrow> valid_mdb' s" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pspace' s \<longrightarrow> pspace_distinct' s &&& valid_pspace' s \<longrightarrow> pspace_aligned' s &&& valid_pspace' s \<longrightarrow> valid_mdb' s
theory Arch_R

lemma descendants_of'_helper:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q (descendants_of' t (null_filter' (ctes_of s)))\<rbrace>
   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q (descendants_of' t (ctes_of s))\<rbrace>" apply (clarsimp simp:valid_def) apply (subst null_filter_descendants_of') prefer 2 apply fastforce apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q (descendants_of' t (null_filter' (ctes_of s)))\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q (descendants_of' t (ctes_of s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> Q (descendants_of' t (null_filter' (ctes_of s')))); P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> Q (descendants_of' t (ctes_of b)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> Q (descendants_of' t (null_filter' (ctes_of s')))); P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> null_filter' (ctes_of b) = null_filter' (?ys9 s a b)
 2. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> Q (descendants_of' t (null_filter' (ctes_of s')))); P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> Q (descendants_of' t (?ys9 s a b)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> Q (descendants_of' t (null_filter' (ctes_of s')))); P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> Q (descendants_of' t (?ys9 s a b))
 2. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> Q (descendants_of' t (null_filter' (ctes_of s')))); P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> null_filter' (ctes_of b) = null_filter' (?ys9 s a b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> Q (descendants_of' t (null_filter' (ctes_of s')))); P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> null_filter' (ctes_of b) = null_filter' (null_filter' (ctes_of b)) proof (prove)
goal:
No subgoals!
theory Arch_R

lemma set_cap_device_and_range_aligned:
  "is_aligned ptr sz \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace>
    set_cap
     (cap.UntypedCap dev ptr sz idx)
     aref
    \<lbrace>\<lambda>rv s.
        \<exists>slot.
           cte_wp_at
            (\<lambda>c. cap_is_device c = dev \<and>
                 up_aligned_area ptr sz \<subseteq> cap_range c)
            slot s\<rbrace>" apply (subst is_aligned_neg_mask_eq[symmetric]) apply simp apply (wp set_cap_device_and_range) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr sz \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> set_cap (cap.UntypedCap dev ptr sz idx) aref \<lbrace>\<lambda>rv s. \<exists>slot. cte_wp_at (\<lambda>c. cap_is_device c = dev \<and> up_aligned_area ptr sz \<subseteq> cap_range c) slot s\<rbrace> proof (prove)
goal (2 subgoals):
 1. is_aligned ptr sz \<Longrightarrow> is_aligned ptr ?n
 2. is_aligned ptr sz \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> set_cap (cap.UntypedCap dev (ptr && ~~ mask ?n) sz idx) aref \<lbrace>\<lambda>rv s. \<exists>slot. cte_wp_at (\<lambda>c. cap_is_device c = dev \<and> up_aligned_area ptr sz \<subseteq> cap_range c) slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned ptr sz \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> set_cap (cap.UntypedCap dev (ptr && ~~ mask sz) sz idx) aref \<lbrace>\<lambda>rv s. \<exists>slot. cte_wp_at (\<lambda>c. cap_is_device c = dev \<and> up_aligned_area ptr sz \<subseteq> cap_range c) slot s\<rbrace> proof (prove)
goal:
No subgoals!
theory Arch_R

lemma mask_vmrights_corres:
  "maskVMRights (vmrights_map R) (rightsFromWord d) =
  vmrights_map (mask_vm_rights R (data_to_rights d))" by (clarsimp simp: rightsFromWord_def data_to_rights_def
                     vmrights_map_def Let_def maskVMRights_def
                     mask_vm_rights_def nth_ucast
                     validate_vm_rights_def vm_read_write_def
                     vm_kernel_only_def vm_read_only_def
               split: bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. maskVMRights (vmrights_map R) (rightsFromWord d) = vmrights_map (mask_vm_rights R (data_to_rights d))
theory Arch_R

lemma vm_attributes_corres:
  "vmattributes_map (attribs_from_word w) = attribsFromWord w" by (clarsimp simp: attribsFromWord_def attribs_from_word_def
                     Let_def vmattributes_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vmattributes_map (attribs_from_word w) = attribsFromWord w
theory Arch_R

lemma checkVPAlignment_corres:
  "corres (ser \<oplus> dc) \<top> \<top>
          (check_vp_alignment sz w)
          (checkVPAlignment sz w)" apply (simp add: check_vp_alignment_def checkVPAlignment_def) apply (cases sz, simp_all add: corres_returnOk unlessE_whenE is_aligned_mask) apply ((rule corres_guard_imp, rule corres_whenE, rule refl, auto)[1])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (ser \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (check_vp_alignment sz w) (checkVPAlignment sz w) proof (prove)
goal (1 subgoal):
 1. corres (ser \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (unlessE (is_aligned w (pageBitsForSize sz)) (throwError ExceptionTypes_A.syscall_error.AlignmentError)) (unlessE (w && mask (pageBitsForSize sz) = 0) (throwError Fault_H.syscall_error.AlignmentError)) proof (prove)
goal (4 subgoals):
 1. sz = ARMSmallPage \<Longrightarrow> corres (ser \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (whenE (w && mask 12 \<noteq> 0) (throwError ExceptionTypes_A.syscall_error.AlignmentError)) (whenE (w && mask 12 \<noteq> 0) (throwError Fault_H.syscall_error.AlignmentError))
 2. sz = ARMLargePage \<Longrightarrow> corres (ser \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (whenE (w && mask 16 \<noteq> 0) (throwError ExceptionTypes_A.syscall_error.AlignmentError)) (whenE (w && mask 16 \<noteq> 0) (throwError Fault_H.syscall_error.AlignmentError))
 3. sz = ARMSection \<Longrightarrow> corres (ser \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (whenE (w && mask 20 \<noteq> 0) (throwError ExceptionTypes_A.syscall_error.AlignmentError)) (whenE (w && mask 20 \<noteq> 0) (throwError Fault_H.syscall_error.AlignmentError))
 4. sz = ARMSuperSection \<Longrightarrow> corres (ser \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (whenE (w && mask 24 \<noteq> 0) (throwError ExceptionTypes_A.syscall_error.AlignmentError)) (whenE (w && mask 24 \<noteq> 0) (throwError Fault_H.syscall_error.AlignmentError)) proof (prove)
goal:
No subgoals!
theory Arch_R

lemma checkVP_wpR [wp]:
  "\<lbrace>\<lambda>s. vmsz_aligned' w sz \<longrightarrow> P () s\<rbrace>
  checkVPAlignment sz w \<lbrace>P\<rbrace>, -" apply (simp add: checkVPAlignment_def unlessE_whenE cong: vmpage_size.case_cong) apply (rule hoare_pre) apply (wp whenE_wp|wpc)+ apply (simp add: is_aligned_mask vmsz_aligned'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vmsz_aligned' w sz \<longrightarrow> P () s\<rbrace> checkVPAlignment sz w \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vmsz_aligned' w sz \<longrightarrow> P () s\<rbrace> whenE (w && mask (pageBitsForSize sz) \<noteq> 0) (throwError Fault_H.syscall_error.AlignmentError) \<lbrace>P\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> whenE (w && mask (pageBitsForSize sz) \<noteq> 0) (throwError Fault_H.syscall_error.AlignmentError) \<lbrace>P\<rbrace>, -
 2. \<And>s. vmsz_aligned' w sz \<longrightarrow> P () s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. vmsz_aligned' w sz \<longrightarrow> P () s \<Longrightarrow> (if w && mask (pageBitsForSize sz) \<noteq> 0 then \<lambda>s. True \<and> True else P ()) s proof (prove)
goal:
No subgoals!
theory Arch_R

lemma asidHighBits [simp]:
  "asidHighBits = asid_high_bits" by (simp add: asidHighBits_def asid_high_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asidHighBits = local.asid_high_bits
theory Arch_R

lemma ARMMMU_improve_cases:
  "(if isPageDirectoryCap cap then P
    else if isPageTableCap cap then Q
    else if isPageCap cap then R
    else if isASIDControlCap cap then S
    else if isASIDPoolCap cap then T
    else undefined)
    =
   (if isPageDirectoryCap cap then P
    else if isPageTableCap cap then Q
    else if isPageCap cap then R
    else if isASIDControlCap cap then S
    else T)" by (cases cap, simp_all add: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if isPageDirectoryCap cap then P else if isPageTableCap cap then Q else if isPageCap cap then R else if isASIDControlCap cap then S else if isASIDPoolCap cap then T else undefined) = (if isPageDirectoryCap cap then P else if isPageTableCap cap then Q else if isPageCap cap then R else if isASIDControlCap cap then S else T)
theory Arch_R

lemma cap_relation_Untyped_eq:
  "cap_relation c (UntypedCap d p sz f) = (c = cap.UntypedCap d p sz f)" by (cases c) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation c (capability.UntypedCap d p sz f) = (c = cap.UntypedCap d p sz f)
theory Arch_R

lemma vmsz_aligned_less_kernel_base_eq:
  "\<lbrakk>ptr + 2 ^ pageBitsForSize vmpage_size - 1 < kernel_base;vmsz_aligned ptr vmpage_size\<rbrakk>
   \<Longrightarrow> ptr < kernel_base" apply (simp add:vmsz_aligned_def) apply (rule ccontr) apply (simp add:not_less) apply (drule(1) less_le_trans) apply (drule is_aligned_no_overflow) apply (simp add:not_less[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr + 2 ^ pageBitsForSize vmpage_size - 1 < kernel_base; vmsz_aligned ptr vmpage_size\<rbrakk> \<Longrightarrow> ptr < kernel_base proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr + 2 ^ pageBitsForSize vmpage_size - 1 < kernel_base; is_aligned ptr (pageBitsForSize vmpage_size)\<rbrakk> \<Longrightarrow> ptr < kernel_base proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr + 2 ^ pageBitsForSize vmpage_size - 1 < kernel_base; is_aligned ptr (pageBitsForSize vmpage_size); \<not> ptr < kernel_base\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr + 2 ^ pageBitsForSize vmpage_size - 1 < kernel_base; is_aligned ptr (pageBitsForSize vmpage_size); kernel_base \<le> ptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (pageBitsForSize vmpage_size); kernel_base \<le> ptr; ptr + 2 ^ pageBitsForSize vmpage_size - 1 < ptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kernel_base \<le> ptr; ptr + 2 ^ pageBitsForSize vmpage_size - 1 < ptr; ptr \<le> ptr + 2 ^ pageBitsForSize vmpage_size - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Arch_R

lemma select_ext_fap:
  "free_asid_pool_select p b \<in> S
  \<Longrightarrow> ((select_ext (\<lambda>_. free_asid_pool_select p b) S) :: (10 word) det_ext_monad)
   = return (free_asid_pool_select p b)" by (simp add: select_ext_def get_def gets_def bind_def assert_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. free_asid_pool_select p b \<in> S \<Longrightarrow> select_ext (\<lambda>_. free_asid_pool_select p b) S = return (free_asid_pool_select p b)