kings-crown/FVELER_Isabelle huggingface dataset:
theory Arch_C

lemma array_assertion_abs_pte_16_mv_aligned:
  "\<forall>s s'. (s, s') \<in> rf_sr \<and> (page_table_at' (ptr_val ptPtr && ~~ mask ptBits) s)
        \<and> (n s' \<le> 16 \<and> (x s' \<noteq> k \<longrightarrow> is_aligned (ptr_val ptPtr) 6 \<and> n s' \<noteq> 0))
    \<longrightarrow> (x s' = k \<or> array_assertion (ptPtr :: pte_C ptr) (n s') (hrs_htd (t_hrs_' (globals s'))))" by (metis array_assertion_abs_pte_16)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> rf_sr \<and> page_table_at' (ptr_val ptPtr && ~~ mask ptBits) s \<and> n s' \<le> 16 \<and> (x s' \<noteq> k \<longrightarrow> is_aligned (ptr_val ptPtr) 6 \<and> n s' \<noteq> 0) \<longrightarrow> x s' = k \<or> array_assertion ptPtr (n s') (hrs_htd (t_hrs_' (globals s')))
theory Arch_C

lemma pde_align_ptBits:
  "\<lbrakk> ko_at' (ARM_H.PageTablePDE x xa xb) slot s ;valid_objs' s\<rbrakk>
  \<Longrightarrow> is_aligned (ptrFromPAddr x) ptBits" apply (drule ko_at_valid_objs') apply simp apply (simp add:projectKO_opts_defs injectKO_defs
    split:Structures_H.kernel_object.splits
    arch_kernel_object.splits)+ apply (simp add:valid_obj'_def) apply (rule is_aligned_ptrFromPAddr_n) apply simp apply (simp add:ptBits_def pageBits_def pteBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' (ARM_H.PageTablePDE x xa xb) slot s; valid_objs' s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) ptBits proof (prove)
goal (3 subgoals):
 1. valid_objs' s \<Longrightarrow> valid_objs' s
 2. \<And>ko. \<lbrakk>valid_objs' s; projectKO_opt ko = Some (ARM_H.PageTablePDE x xa xb)\<rbrakk> \<Longrightarrow> injectKOS (ARM_H.PageTablePDE x xa xb) = ko
 3. \<lbrakk>valid_objs' s; valid_obj' (injectKOS (ARM_H.PageTablePDE x xa xb)) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) ptBits proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrakk>valid_objs' s; projectKO_opt ko = Some (ARM_H.PageTablePDE x xa xb)\<rbrakk> \<Longrightarrow> injectKOS (ARM_H.PageTablePDE x xa xb) = ko
 2. \<lbrakk>valid_objs' s; valid_obj' (injectKOS (ARM_H.PageTablePDE x xa xb)) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) ptBits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs' s; valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) ptBits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs' s; is_aligned x ptBits\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) ptBits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs' s; is_aligned x ptBits\<rbrakk> \<Longrightarrow> is_aligned x ptBits
 2. \<lbrakk>valid_objs' s; is_aligned x ptBits\<rbrakk> \<Longrightarrow> ptBits \<le> 24 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs' s; is_aligned x ptBits\<rbrakk> \<Longrightarrow> ptBits \<le> 24 proof (prove)
goal:
No subgoals!
theory Arch_C

lemma mapM_x_storePDE_pde_mappings':
"\<lbrakk>valid_pde_slots'2 (Inr (a, b)) s; b \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>valid_pde_mappings'\<rbrace>
          mapM_x (\<lambda>b. storePDE b a) b \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>" apply (wp mapM_x_wp') apply (auto simp: valid_pde_slots'2_def valid_pde_mapping'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pde_slots'2 (Inr (a, b)) s; b \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>valid_pde_mappings'\<rbrace> mapM_x (\<lambda>b. storePDE b a) b \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x sa. \<lbrakk>valid_pde_slots'2 (Inr (a, b)) s; b \<noteq> []; x \<in> set b; valid_pde_mappings' sa\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and K (valid_pde_mapping' (x && mask pdBits) a)) sa
 2. \<And>sa. \<lbrakk>valid_pde_slots'2 (Inr (a, b)) s; b \<noteq> []; valid_pde_mappings' sa\<rbrakk> \<Longrightarrow> valid_pde_mappings' sa proof (prove)
goal:
No subgoals!
theory Arch_C

lemma setMRs_single:
  "setMRs thread buffer [val] = do
     _ \<leftarrow> asUser thread (setRegister register.R2 val);
     return 1
   od" apply (clarsimp simp: setMRs_def length_msgRegisters n_msgRegisters_def zipWithM_x_def zipWith_def
                 split: option.splits) apply (subst zip_commute, subst zip_singleton) apply (simp add: length_msgRegisters n_msgRegisters_def length_0_conv[symmetric]) apply (clarsimp simp: msgRegisters_unfold sequence_x_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. setMRs thread buffer [val] = do _ <- asUser thread (setRegister register.R2 val);
return 1
od proof (prove)
goal (1 subgoal):
 1. do y <- asUser thread (sequence_x (map2 setRegister TCB_H.msgRegisters [val]));
y <- sequence_x [];
return 1
od = do _ <- asUser thread (setRegister register.R2 val);
return 1
od proof (prove)
goal (2 subgoals):
 1. TCB_H.msgRegisters \<noteq> []
 2. do y <- asUser thread (sequence_x (map (\<lambda>(x, y). setRegister x y) (map (\<lambda>(x, y). (y, x)) [(val, TCB_H.msgRegisters ! 0)])));
y <- sequence_x [];
return 1
od = do _ <- asUser thread (setRegister register.R2 val);
return 1
od proof (prove)
goal (1 subgoal):
 1. do y <- asUser thread (sequence_x (map (\<lambda>(x, y). setRegister x y) (map (\<lambda>(x, y). (y, x)) [(val, TCB_H.msgRegisters ! 0)])));
y <- sequence_x [];
return 1
od = do _ <- asUser thread (setRegister register.R2 val);
return 1
od proof (prove)
goal:
No subgoals!
theory Arch_C

lemma vmsz_aligned_addrFromPPtr':
  "vmsz_aligned' (addrFromPPtr p) sz = vmsz_aligned' p sz" apply (simp add: vmsz_aligned'_def) apply (rule iffI) apply (simp add: addrFromPPtr_def is_aligned_mask) apply (prop_tac "pptrBaseOffset AND mask (pageBitsForSize sz) = 0") apply (rule mask_zero[OF is_aligned_weaken[OF pptrBaseOffset_aligned]], simp) apply (simp flip: mask_eqs(8)) apply (erule is_aligned_addrFromPPtr_n) apply (cases sz; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vmsz_aligned' (addrFromPPtr p) sz = vmsz_aligned' p sz proof (prove)
goal (1 subgoal):
 1. is_aligned (addrFromPPtr p) (pageBitsForSize sz) = is_aligned p (pageBitsForSize sz) proof (prove)
goal (2 subgoals):
 1. is_aligned (addrFromPPtr p) (pageBitsForSize sz) \<Longrightarrow> is_aligned p (pageBitsForSize sz)
 2. is_aligned p (pageBitsForSize sz) \<Longrightarrow> is_aligned (addrFromPPtr p) (pageBitsForSize sz) proof (prove)
goal (2 subgoals):
 1. p - pptrBaseOffset && mask (pageBitsForSize sz) = 0 \<Longrightarrow> p && mask (pageBitsForSize sz) = 0
 2. is_aligned p (pageBitsForSize sz) \<Longrightarrow> is_aligned (addrFromPPtr p) (pageBitsForSize sz) proof (prove)
goal (3 subgoals):
 1. p - pptrBaseOffset && mask (pageBitsForSize sz) = 0 \<Longrightarrow> pptrBaseOffset && mask (pageBitsForSize sz) = 0
 2. \<lbrakk>p - pptrBaseOffset && mask (pageBitsForSize sz) = 0; pptrBaseOffset && mask (pageBitsForSize sz) = 0\<rbrakk> \<Longrightarrow> p && mask (pageBitsForSize sz) = 0
 3. is_aligned p (pageBitsForSize sz) \<Longrightarrow> is_aligned (addrFromPPtr p) (pageBitsForSize sz) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p - pptrBaseOffset && mask (pageBitsForSize sz) = 0; pptrBaseOffset && mask (pageBitsForSize sz) = 0\<rbrakk> \<Longrightarrow> p && mask (pageBitsForSize sz) = 0
 2. is_aligned p (pageBitsForSize sz) \<Longrightarrow> is_aligned (addrFromPPtr p) (pageBitsForSize sz) proof (prove)
goal (1 subgoal):
 1. is_aligned p (pageBitsForSize sz) \<Longrightarrow> is_aligned (addrFromPPtr p) (pageBitsForSize sz) proof (prove)
goal (1 subgoal):
 1. pageBitsForSize sz \<le> 24 proof (prove)
goal:
No subgoals!
theory Arch_C

lemma gen_framesize_to_H_eq_from_H':
  "v < 4 \<Longrightarrow> (v' = gen_framesize_to_H v) = (framesize_from_H v' = v)" apply (simp add: gen_framesize_to_H_def framesize_from_H_eqs
            split: if_split) apply (clarsimp simp: framesize_from_H_eqs[symmetric] vm_page_size_defs) apply unat_arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. v < 4 \<Longrightarrow> (v' = gen_framesize_to_H v) = (framesize_from_H v' = v) proof (prove)
goal (1 subgoal):
 1. v < 4 \<Longrightarrow> v \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<longrightarrow> v \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage \<longrightarrow> v \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<longrightarrow> (v' = Wellformed_C.ARMSuperSection) = (framesize_from_H v' = v) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v < 4; v \<noteq> 2; v \<noteq> 1; v \<noteq> 0\<rbrakk> \<Longrightarrow> (framesize_from_H v' = 3) = (framesize_from_H v' = v) proof (prove)
goal:
No subgoals!
theory Arch_C

lemma gen_framesize_to_H_eq_from_H:
  assumes v: "v < 4" shows
  "(v' = gen_framesize_to_H v) = (framesize_from_H v' = v)"
  "(gen_framesize_to_H v = v') = (v = framesize_from_H v')" using gen_framesize_to_H_eq_from_H'[OF v, where v'=v'] by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (v' = gen_framesize_to_H v) = (framesize_from_H v' = v) &&& (gen_framesize_to_H v = v') = (v = framesize_from_H v') proof (prove)
using this:
(v' = gen_framesize_to_H v) = (framesize_from_H v' = v)

goal (1 subgoal):
 1. (v' = gen_framesize_to_H v) = (framesize_from_H v' = v) &&& (gen_framesize_to_H v = v') = (v = framesize_from_H v')
theory Arch_C

lemma shiftr_asid_low_bits_mask_asid_high_bits:
  "(asid :: word32) \<le> mask asid_bits
      \<Longrightarrow> (asid >> asid_low_bits) && mask asid_high_bits = asid >> asid_low_bits" apply (rule iffD2 [OF mask_eq_iff_w2p]) apply (simp add: asid_high_bits_def word_size) apply (rule shiftr_less_t2n) apply (simp add: asid_low_bits_def asid_high_bits_def mask_def) apply (simp add: asid_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid \<le> mask local.asid_bits \<Longrightarrow> (asid >> local.asid_low_bits) && mask local.asid_high_bits = asid >> local.asid_low_bits proof (prove)
goal (2 subgoals):
 1. asid \<le> mask local.asid_bits \<Longrightarrow> local.asid_high_bits < size (asid >> local.asid_low_bits)
 2. asid \<le> mask local.asid_bits \<Longrightarrow> asid >> local.asid_low_bits < 2 ^ local.asid_high_bits proof (prove)
goal (1 subgoal):
 1. asid \<le> mask local.asid_bits \<Longrightarrow> asid >> local.asid_low_bits < 2 ^ local.asid_high_bits proof (prove)
goal (1 subgoal):
 1. asid \<le> mask local.asid_bits \<Longrightarrow> asid < 2 ^ (local.asid_low_bits + local.asid_high_bits) proof (prove)
goal (1 subgoal):
 1. asid < 2 ^ local.asid_bits \<Longrightarrow> asid < 0x20000 proof (prove)
goal:
No subgoals!
theory Arch_C

lemma slotcap_in_mem_valid:
  "\<lbrakk> slotcap_in_mem cap slot (ctes_of s); valid_objs' s \<rbrakk>
            \<Longrightarrow> s \<turnstile>' cap" apply (clarsimp simp: slotcap_in_mem_def) apply (erule(1) ctes_of_valid') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slotcap_in_mem cap slot (ctes_of s); valid_objs' s\<rbrakk> \<Longrightarrow> valid_cap' cap s proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>valid_objs' s; ctes_of s slot = Some cte; cap = cteCap cte\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal:
No subgoals!
theory Arch_C

lemma ivc_label_flush_case:
  "label = ArchInvocationLabel arch_invocation_label.ARMPageUnify_Instruction \<or>
   label = ArchInvocationLabel arch_invocation_label.ARMPageCleanInvalidate_Data \<or>
   label = ArchInvocationLabel arch_invocation_label.ARMPageInvalidate_Data \<or>
   label = ArchInvocationLabel arch_invocation_label.ARMPageClean_Data
    \<Longrightarrow> (case label of
     ArchInvocationLabel arch_invocation_label.ARMPageMap \<Rightarrow> A
  |  ArchInvocationLabel arch_invocation_label.ARMPageUnmap \<Rightarrow> B
  |  ArchInvocationLabel arch_invocation_label.ARMPageUnify_Instruction \<Rightarrow> C
  |  ArchInvocationLabel arch_invocation_label.ARMPageCleanInvalidate_Data \<Rightarrow> C
  |  ArchInvocationLabel arch_invocation_label.ARMPageInvalidate_Data \<Rightarrow> C
  |  ArchInvocationLabel arch_invocation_label.ARMPageClean_Data \<Rightarrow> C
  |  ArchInvocationLabel arch_invocation_label.ARMPageGetAddress \<Rightarrow> D
  |  _  \<Rightarrow> E)
  = C" by (auto split: invocation_label.split arch_invocation_label.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. label = ArchInvocationLabel arch_invocation_label.ARMPageUnify_Instruction \<or> label = ArchInvocationLabel arch_invocation_label.ARMPageCleanInvalidate_Data \<or> label = ArchInvocationLabel arch_invocation_label.ARMPageInvalidate_Data \<or> label = ArchInvocationLabel arch_invocation_label.ARMPageClean_Data \<Longrightarrow> (case label of GenInvocationLabel gen_invocation_labels \<Rightarrow> E | ArchInvocationLabel arch_invocation_label.ARMPageMap \<Rightarrow> A | ArchInvocationLabel arch_invocation_label.ARMPageUnmap \<Rightarrow> B | ArchInvocationLabel arch_invocation_label.ARMPageClean_Data \<Rightarrow> C | ArchInvocationLabel arch_invocation_label.ARMPageInvalidate_Data \<Rightarrow> C | ArchInvocationLabel arch_invocation_label.ARMPageCleanInvalidate_Data \<Rightarrow> C | ArchInvocationLabel arch_invocation_label.ARMPageUnify_Instruction \<Rightarrow> C | ArchInvocationLabel arch_invocation_label.ARMPageGetAddress \<Rightarrow> D | ArchInvocationLabel _ \<Rightarrow> E) = C
theory Arch_C

lemma injection_handler_whenE:
  "injection_handler Inl (whenE a b) = (if a then injection_handler Inl b else returnOk ())" apply (subst injection_handler_returnOk[symmetric]) apply (clarsimp simp: whenE_def injection_handler_def cong: if_cong) apply (fastforce split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. injection_handler Inl (whenE a b) = (if a then injection_handler Inl b else returnOk ()) proof (prove)
goal (1 subgoal):
 1. injection_handler Inl (whenE a b) = (if a then injection_handler Inl b else injection_handler ?injector (returnOk ())) proof (prove)
goal (1 subgoal):
 1. ((if a then b else returnOk ()) <handle2> (\<lambda>ft. throwError (Inl ft))) = (if a then b <handle2> (\<lambda>ft. throwError (Inl ft)) else returnOk () <handle2> (\<lambda>ft. throwError (?injector ft))) proof (prove)
goal:
No subgoals!
theory Arch_C

lemma injection_handler_if_returnOk:
  "injection_handler Inl (if a then b else returnOk c)
  = (if a then (injection_handler Inl b) else returnOk c)" apply (clarsimp simp:whenE_def injection_handler_def) apply (clarsimp simp:injection_handler_def
    throwError_def return_def bind_def returnOk_def
    handleE'_def split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. injection_handler Inl (if a then b else returnOk c) = (if a then injection_handler Inl b else returnOk c) proof (prove)
goal (1 subgoal):
 1. ((if a then b else returnOk c) <handle2> (\<lambda>ft. throwError (Inl ft))) = (if a then injection_handler Inl b else returnOk c) proof (prove)
goal:
No subgoals!
theory Arch_C

lemma pbfs_less: "pageBitsForSize sz < 31" by (case_tac sz,simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pageBitsForSize sz < 31
theory Arch_C

lemma flushtype_relation_triv:
  "isPageFlushLabel (invocation_type label) \<or>
   isPDFlushLabel (invocation_type label)
  ==> flushtype_relation (labelToFlushType label) (ucast label)" by (clarsimp simp: labelToFlushType_def flushtype_relation_def
    invocation_eq_use_types ARM_H.isPageFlushLabel_def
    ARM_H.isPDFlushLabel_def
    split: flush_type.splits invocation_label.splits arch_invocation_label.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isPageFlushLabel (invocation_type label) \<or> isPDFlushLabel (invocation_type label) \<Longrightarrow> flushtype_relation (labelToFlushType label) (UCAST(32 \<rightarrow> 32 signed) label)
theory Arch_C

lemma pte_get_tag_alt:
  "pte_lift v = Some pteC
    \<Longrightarrow> pte_get_tag v = (case pteC of
            Pte_pte_small _ \<Rightarrow> scast pte_pte_small
          | Pte_pte_large _ \<Rightarrow> scast pte_pte_large)" by (auto simp add: pte_lift_def Let_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pte_lift v = Some pteC \<Longrightarrow> pte_get_tag v = (case pteC of Pte_pte_large x \<Rightarrow> SCAST(32 signed \<rightarrow> 32) pte_pte_large | Pte_pte_small x \<Rightarrow> SCAST(32 signed \<rightarrow> 32) pte_pte_small)
theory Arch_C

lemma resolve_ret_rel_None[simp]:
  "resolve_ret_rel None y = (valid_C y = scast false)" by (clarsimp simp: resolve_ret_rel_def to_option_def to_bool_def split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. resolve_ret_rel None y = (valid_C y = SCAST(32 signed \<rightarrow> 32) false)
theory Arch_C

lemma resolve_ret_rel_Some:
  "\<lbrakk>valid_C y = scast true;  frameSize_C y = framesize_from_H (fst x); snd x = frameBase_C y\<rbrakk>
   \<Longrightarrow> resolve_ret_rel (Some x) y" by (clarsimp simp: resolve_ret_rel_def to_option_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_C y = SCAST(32 signed \<rightarrow> 32) true; frameSize_C y = framesize_from_H (fst x); snd x = frameBase_C y\<rbrakk> \<Longrightarrow> resolve_ret_rel (Some x) y
theory Arch_C

lemma cte_wp_at_eq_gsMaxObjectSize:
  "cte_wp_at' ((=) cap o cteCap) slot s
    \<Longrightarrow> valid_global_refs' s
    \<Longrightarrow> 2 ^ capBits cap \<le> gsMaxObjectSize s" apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule(1) valid_global_refsD_with_objSize) apply (clarsimp simp: capMaster_eq_capBits_eq[OF capMasterCap_maskCapRights]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' ((=) cap \<circ> cteCap) slot s; valid_global_refs' s\<rbrakk> \<Longrightarrow> 2 ^ capBits cap \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>valid_global_refs' s; ctes_of s slot = Some cte; cap = cteCap cte\<rbrakk> \<Longrightarrow> 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>valid_global_refs' s; cap = cteCap cte; kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s \<subseteq> kernel_data_refs \<and> 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s proof (prove)
goal:
No subgoals!
theory Arch_C

lemma two_nat_power_pageBitsForSize_le:
  "(2 :: nat) ^ pageBits \<le> 2 ^ pageBitsForSize vsz" by (cases vsz, simp_all add: pageBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 ^ pageBits \<le> 2 ^ pageBitsForSize vsz
theory Arch_C

lemma throwError_invocationCatch:
  "throwError a >>= invocationCatch b c d e = throwError (Inl a)" by (simp add: invocationCatch_def throwError_bind)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. throwError a >>= invocationCatch b c d e = throwError (Inl a)
theory Arch_C

lemma asidHighBits_handy_convs:
  "sint Kernel_C.asidHighBits = 7"
  "Kernel_C.asidHighBits \<noteq> 0x20"
  "unat Kernel_C.asidHighBits = asid_high_bits" by (simp add: Kernel_C.asidHighBits_def
                asid_high_bits_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sint Kernel_C.asidHighBits = 7 &&& Kernel_C.asidHighBits \<noteq> 0x20 &&& unat Kernel_C.asidHighBits = local.asid_high_bits
theory Arch_C

lemma sts_Restart_ct_active [wp]:
  "\<lbrace>\<lambda>s. thread = ksCurThread s\<rbrace> setThreadState Restart thread \<lbrace>\<lambda>_. ct_active'\<rbrace>" apply (clarsimp simp: ct_in_state'_def) apply (rule hoare_lift_Pf2 [where f=ksCurThread]) apply (wp sts_st_tcb') apply (simp split: if_split) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. thread = ksCurThread s\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>_. ct_active'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. thread = ksCurThread s\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>_ s. st_tcb_at' active' (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. thread = x\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>_. st_tcb_at' active' x\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s. thread = x \<Longrightarrow> (if x = thread then K (active' Structures_H.thread_state.Restart) else st_tcb_at' active' x) s
 2. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Arch_C

lemma isPDFlush_fold:
 "(label = ArchInvocationLabel arch_invocation_label.ARMPDUnify_Instruction \<or>
 label =   ArchInvocationLabel arch_invocation_label.ARMPDCleanInvalidate_Data \<or>
 label =   ArchInvocationLabel arch_invocation_label.ARMPDInvalidate_Data \<or>
 label =   ArchInvocationLabel arch_invocation_label.ARMPDClean_Data) = isPDFlushLabel label" by (simp_all add:isPDFlushLabel_def split:invocation_label.splits arch_invocation_label.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (label = ArchInvocationLabel arch_invocation_label.ARMPDUnify_Instruction \<or> label = ArchInvocationLabel arch_invocation_label.ARMPDCleanInvalidate_Data \<or> label = ArchInvocationLabel arch_invocation_label.ARMPDInvalidate_Data \<or> label = ArchInvocationLabel arch_invocation_label.ARMPDClean_Data) = isPDFlushLabel label
theory Arch_C

lemma pageBase_spec:
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. \<acute>size___unsigned_long && mask 2 = \<acute>size___unsigned_long\<rbrace>
  Call pageBase_'proc
  \<lbrace> \<acute>ret__unsigned_long = \<^bsup>s\<^esup>vaddr && ~~ (2 ^ pageBitsForSize (gen_framesize_to_H \<^bsup>s\<^esup>size___unsigned_long) - 1)\<rbrace>" apply vcg apply (simp add:pageBitsForSize_def split:vmpage_size.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. \<acute>size___unsigned_long && mask 2 = \<acute>size___unsigned_long\<rbrace> Call pageBase_'proc \<lbrace>\<acute>ret__unsigned_long = \<^bsup>s\<^esup>vaddr && ~~ (2 ^ pageBitsForSize (gen_framesize_to_H \<^bsup>s\<^esup>size___unsigned_long) - 1)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>vaddr size___unsigned_long. size___unsigned_long && mask 2 = size___unsigned_long \<Longrightarrow> size___unsigned_long && mask 2 = size___unsigned_long \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = word_of_nat (pageBitsForSize (gen_framesize_to_H size___unsigned_long)) \<longrightarrow> word_of_nat (pageBitsForSize (gen_framesize_to_H size___unsigned_long)) < SCAST(32 signed \<rightarrow> 32) 0x20 \<and> vaddr && ~~ ((1 << unat (word_of_nat (pageBitsForSize (gen_framesize_to_H size___unsigned_long)))) - 1) = vaddr && ~~ (2 ^ pageBitsForSize (gen_framesize_to_H size___unsigned_long) - 1)) proof (prove)
goal:
No subgoals!
theory Arch_C

lemma framesize_from_H_mask2:
  "framesize_from_H a && mask 2 = framesize_from_H a" apply (rule less_mask_eq) apply (simp add:framesize_from_H_def
    split: vmpage_size.splits) apply (simp add:Kernel_C.ARMSmallPage_def
      Kernel_C.ARMLargePage_def
      Kernel_C.ARMSection_def
      Kernel_C.ARMSuperSection_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. framesize_from_H a && mask 2 = framesize_from_H a proof (prove)
goal (1 subgoal):
 1. framesize_from_H a < 2\<^sup>2 proof (prove)
goal (1 subgoal):
 1. (a = Wellformed_C.ARMSmallPage \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage < 4) \<and> (a = Wellformed_C.ARMLargePage \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage < 4) \<and> (a = Wellformed_C.ARMSection \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection < 4) \<and> (a = Wellformed_C.ARMSuperSection \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection < 4) proof (prove)
goal:
No subgoals!