kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchVSpaceEntries_AI

lemma set_simple_ko_valid_pdpt_objs[wp]:
   "\<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
       set_simple_ko param_a param_b param_c \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>" unfolding set_simple_ko_def by (wpsimp wp: set_object_valid_pdpt[THEN hoare_set_object_weaken_pre] get_object_wp
           simp: a_type_def obj_valid_pdpt_def obj_at_def
          split: kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> set_simple_ko param_a param_b param_c \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> do obj <- get_object param_b;
assert (is_simple_type obj);
assert (partial_inv param_a obj \<noteq> None);
set_object param_b (param_a param_c)
od \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
theory ArchVSpaceEntries_AI

lemma preemption_point_valid_pdpt_objs[wp]:
  "\<lbrace>valid_pdpt_objs\<rbrace> preemption_point \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" by (wp preemption_point_inv | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> preemption_point \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
theory ArchVSpaceEntries_AI

lemma in_pte_rangeD:
  "x \<in> pte_range v y \<Longrightarrow> x && ~~ mask 4 = y && ~~ mask 4" by (case_tac v,simp_all split:if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> pte_range v y \<Longrightarrow> x && ~~ mask 4 = y && ~~ mask 4
theory ArchVSpaceEntries_AI

lemma in_pde_rangeD:
  "x \<in> pde_range v y \<Longrightarrow> x && ~~ mask 4 = y && ~~ mask 4" by (case_tac v,simp_all split:if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> pde_range v y \<Longrightarrow> x && ~~ mask 4 = y && ~~ mask 4
theory ArchVSpaceEntries_AI

lemma non_invalid_in_pde_range:
  "pde \<noteq> InvalidPDE
  \<Longrightarrow> x \<in> pde_range pde x" by (case_tac pde,simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pde \<noteq> InvalidPDE \<Longrightarrow> x \<in> pde_range pde x
theory ArchVSpaceEntries_AI

lemma non_invalid_in_pte_range:
  "pte \<noteq> InvalidPTE
  \<Longrightarrow> x \<in> pte_range pte x" by (case_tac pte,simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pte \<noteq> InvalidPTE \<Longrightarrow> x \<in> pte_range pte x
theory ArchVSpaceEntries_AI

lemma invoke_cnode_valid_pdpt_objs[wp]:
  "\<lbrace>valid_pdpt_objs and invs and valid_cnode_inv i\<rbrace> invoke_cnode i \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" apply (simp add: invoke_cnode_def) apply (rule hoare_pre) apply (wp get_cap_wp | wpc | simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invs and valid_cnode_inv i\<rbrace> invoke_cnode i \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 2. \<And>s. ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invs and valid_cnode_inv i) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ArchVSpaceEntries_AI

lemma invoke_domain_valid_pdpt_objs[wp]:
  "\<lbrace>valid_pdpt_objs\<rbrace> invoke_domain t d \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" by (simp add: invoke_domain_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> invoke_domain t d \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
theory ArchVSpaceEntries_AI

lemma retype_region_valid_pdpt[wp]:
  "\<lbrace>valid_pdpt_objs\<rbrace> retype_region ptr bits o_bits type dev \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" apply (simp add: retype_region_def split del: if_split) apply (wp | simp only: valid_pdpt_objs_trans_state trans_state_update[symmetric])+ apply (clarsimp simp: retype_addrs_fold foldr_upd_app_if ranI
                 elim!: ranE split: if_split_asm simp del:fun_upd_apply) apply (simp add: default_object_def default_arch_object_def
            split: Structures_A.kernel_object.splits
    Structures_A.apiobject_type.split aobject_type.split)+ apply (simp add:entries_align_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> retype_region ptr bits o_bits type dev \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> do y <- when (type \<noteq> Untyped) (do kh <- gets kheap;
y <- do_extended_op (retype_region_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<bits]) type);
modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<bits]) kh))
od);
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<bits])
od \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x \<Longrightarrow> (if type \<noteq> Untyped then \<lambda>s. \<forall>x\<in>ran (kheap (s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<bits]) (kheap s)\<rparr>)). obj_valid_pdpt x else (\<lambda>a. \<forall>x\<in>ran (kheap a). obj_valid_pdpt x)) s proof (prove)
goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; type \<noteq> Untyped; xa \<in> set (retype_addrs ptr type bits o_bits)\<rbrakk> \<Longrightarrow> obj_valid_pdpt (default_object type dev o_bits) proof (prove)
goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; type \<noteq> Untyped; xa \<in> set (retype_addrs ptr type bits o_bits)\<rbrakk> \<Longrightarrow> \<forall>x6. (x6 = PageTableObj \<longrightarrow> type = ArchObject PageTableObj \<longrightarrow> entries_align pte_range_sz (\<lambda>x. InvalidPTE)) \<and> (x6 = PageDirectoryObj \<longrightarrow> type = ArchObject PageDirectoryObj \<longrightarrow> entries_align pde_range_sz (\<lambda>x. InvalidPDE)) proof (prove)
goal:
No subgoals!
theory ArchVSpaceEntries_AI

lemma detype_valid_pdpt[elim!]:
  "valid_pdpt_objs s \<Longrightarrow> valid_pdpt_objs (detype S s)" by (auto simp add: detype_def ran_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x \<Longrightarrow> \<forall>x\<in>ran (kheap (detype S s)). obj_valid_pdpt x
theory ArchVSpaceEntries_AI

lemma delete_objects_valid_pdpt:
  "\<lbrace>valid_pdpt_objs\<rbrace> delete_objects ptr bits \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" by (rule delete_objects_reduct) (wp detype_valid_pdpt)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> delete_objects ptr bits \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
theory ArchVSpaceEntries_AI

lemma pte_range_interD:
 "pte_range pte p \<inter> pte_range pte' p' \<noteq> {}
  \<Longrightarrow> pte \<noteq> InvalidPTE \<and> pte' \<noteq> InvalidPTE
      \<and> p && ~~ mask 4 = p' && ~~ mask 4" apply (drule int_not_emptyD) apply (case_tac pte,simp_all split:if_splits) apply (case_tac pte',simp_all split:if_splits) apply clarsimp apply (case_tac pte',simp_all split:if_splits) apply (case_tac pte', simp_all split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pte_range pte p \<inter> pte_range pte' p' \<noteq> {} \<Longrightarrow> pte \<noteq> InvalidPTE \<and> pte' \<noteq> InvalidPTE \<and> p && ~~ mask 4 = p' && ~~ mask 4 proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> pte_range pte p \<and> x \<in> pte_range pte' p' \<Longrightarrow> pte \<noteq> InvalidPTE \<and> pte' \<noteq> InvalidPTE \<and> p && ~~ mask 4 = p' && ~~ mask 4 proof (prove)
goal (3 subgoals):
 1. \<And>x21 x22 x23. \<lbrakk>pte = LargePagePTE x21 x22 x23; is_aligned p 4; \<exists>x. x && ~~ mask 4 = p \<and> x \<in> pte_range pte' p'\<rbrakk> \<Longrightarrow> pte' \<noteq> InvalidPTE \<and> p = p' && ~~ mask 4
 2. \<And>x21 x22 x23. \<lbrakk>pte = LargePagePTE x21 x22 x23; \<not> is_aligned p 4; p \<in> pte_range pte' p'\<rbrakk> \<Longrightarrow> pte' \<noteq> InvalidPTE \<and> p && ~~ mask 4 = p' && ~~ mask 4
 3. \<And>x31 x32 x33. \<lbrakk>p \<in> pte_range pte' p'; pte = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> pte' \<noteq> InvalidPTE \<and> p && ~~ mask 4 = p' && ~~ mask 4 proof (prove)
goal (3 subgoals):
 1. \<And>x21 x22 x23 x21a x22a x23a. \<lbrakk>pte' = LargePagePTE x21a x22a x23a; pte = LargePagePTE x21 x22 x23; is_aligned p 4; is_aligned p' 4; \<exists>x. x && ~~ mask 4 = p \<and> x && ~~ mask 4 = p'\<rbrakk> \<Longrightarrow> p = p'
 2. \<And>x21 x22 x23. \<lbrakk>pte = LargePagePTE x21 x22 x23; \<not> is_aligned p 4; p \<in> pte_range pte' p'\<rbrakk> \<Longrightarrow> pte' \<noteq> InvalidPTE \<and> p && ~~ mask 4 = p' && ~~ mask 4
 3. \<And>x31 x32 x33. \<lbrakk>p \<in> pte_range pte' p'; pte = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> pte' \<noteq> InvalidPTE \<and> p && ~~ mask 4 = p' && ~~ mask 4 proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23. \<lbrakk>pte = LargePagePTE x21 x22 x23; \<not> is_aligned p 4; p \<in> pte_range pte' p'\<rbrakk> \<Longrightarrow> pte' \<noteq> InvalidPTE \<and> p && ~~ mask 4 = p' && ~~ mask 4
 2. \<And>x31 x32 x33. \<lbrakk>p \<in> pte_range pte' p'; pte = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> pte' \<noteq> InvalidPTE \<and> p && ~~ mask 4 = p' && ~~ mask 4 proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33. \<lbrakk>p \<in> pte_range pte' p'; pte = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> pte' \<noteq> InvalidPTE \<and> p && ~~ mask 4 = p' && ~~ mask 4 proof (prove)
goal:
No subgoals!
theory ArchVSpaceEntries_AI

lemma pte_range_sz_le:
  "(pte_range_sz pte) \<le> 4" by (case_tac pte,simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pte_range_sz pte \<le> 4
theory ArchVSpaceEntries_AI

lemma pde_range_sz_le:
  "(pde_range_sz pde) \<le> 4" by (case_tac pde,simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pde_range_sz pde \<le> 4
theory ArchVSpaceEntries_AI

lemma mask_pd_bits_shift_ucast_align[simp]:
  "is_aligned (ucast (p && mask pd_bits >> 2)::12 word) 4 =
   is_aligned ((p::word32) >> 2) 4" by (clarsimp simp: is_aligned_mask mask_def pd_bits) word_bitwise

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) 4 = is_aligned (p >> 2) 4
theory ArchVSpaceEntries_AI

lemma mask_pt_bits_shift_ucast_align[simp]:
  "is_aligned (ucast (p && mask pt_bits >> 2)::word8) 4 =
   is_aligned ((p::word32) >> 2) 4" by (clarsimp simp: is_aligned_mask mask_def pt_bits_def pageBits_def)
     word_bitwise

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) 4 = is_aligned (p >> 2) 4
theory ArchVSpaceEntries_AI

lemma ucast_pt_index:
  "\<lbrakk>is_aligned (p::word32) 6\<rbrakk>
   \<Longrightarrow> ucast ((pa && mask 4) + (ucast (p && mask pt_bits >> 2)::8 word))
   =  ucast (pa && mask 4) + (p && mask pt_bits >> 2)" apply (simp add:is_aligned_mask mask_def pt_bits_def pageBits_def) apply word_bitwise apply (auto simp: carry_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p 6 \<Longrightarrow> UCAST(8 \<rightarrow> 32) ((pa && mask 4) + UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) = UCAST(8 \<rightarrow> 32) (pa && mask 4) + (p && mask pt_bits >> 2) proof (prove)
goal (1 subgoal):
 1. p && 0x3F = 0 \<Longrightarrow> UCAST(8 \<rightarrow> 32) ((pa && 0xF) + UCAST(32 \<rightarrow> 8) (p && 0x3FF >> 2)) = UCAST(8 \<rightarrow> 32) (pa && 0xF) + (p && 0x3FF >> 2) proof (prove)
goal (1 subgoal):
 1. \<not> p !! 0 \<and> \<not> p !! 1 \<and> \<not> p !! 2 \<and> \<not> p !! 3 \<and> \<not> p !! 4 \<and> \<not> p !! 5 \<Longrightarrow> p !! 9 \<longrightarrow> p !! 8 \<longrightarrow> p !! 7 \<longrightarrow> p !! 6 \<longrightarrow> \<not> carry (pa !! 3) (p !! 5) (carry (pa !! 2) (p !! 4) (carry (pa !! 1) (p !! 3) (pa !! 0 \<and> p !! 2))) proof (prove)
goal:
No subgoals!
theory ArchVSpaceEntries_AI

lemma ucast_pd_index:
  "\<lbrakk>is_aligned (p::word32) 6\<rbrakk>
   \<Longrightarrow> ucast ((pa && mask 4) + (ucast (p && mask pd_bits >> 2)::12 word))
   =  ucast (pa && mask 4) + (p && mask pd_bits >> 2)" apply (simp add:is_aligned_mask mask_def pd_bits_def pageBits_def) apply word_bitwise apply (auto simp:carry_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p 6 \<Longrightarrow> UCAST(12 \<rightarrow> 32) ((pa && mask 4) + UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = UCAST(12 \<rightarrow> 32) (pa && mask 4) + (p && mask pd_bits >> 2) proof (prove)
goal (1 subgoal):
 1. p && 0x3F = 0 \<Longrightarrow> UCAST(12 \<rightarrow> 32) ((pa && 0xF) + UCAST(32 \<rightarrow> 12) (p && 0x3FFF >> 2)) = UCAST(12 \<rightarrow> 32) (pa && 0xF) + (p && 0x3FFF >> 2) proof (prove)
goal (1 subgoal):
 1. \<not> p !! 0 \<and> \<not> p !! 1 \<and> \<not> p !! 2 \<and> \<not> p !! 3 \<and> \<not> p !! 4 \<and> \<not> p !! 5 \<Longrightarrow> p !! 13 \<longrightarrow> p !! 12 \<longrightarrow> p !! 11 \<longrightarrow> p !! 10 \<longrightarrow> p !! 9 \<longrightarrow> p !! 8 \<longrightarrow> p !! 7 \<longrightarrow> p !! 6 \<longrightarrow> \<not> carry (pa !! 3) (p !! 5) (carry (pa !! 2) (p !! 4) (carry (pa !! 1) (p !! 3) (pa !! 0 \<and> p !! 2))) proof (prove)
goal:
No subgoals!
theory ArchVSpaceEntries_AI

lemma unat_ucast_12_32:
  "unat (ucast (x::(12 word))::word32) = unat x" apply (subst unat_ucast) apply (rule mod_less) apply (rule less_le_trans[OF unat_lt2p]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (UCAST(12 \<rightarrow> 32) x) = unat x proof (prove)
goal (1 subgoal):
 1. unat x mod 2 ^ LENGTH(32) = unat x proof (prove)
goal (1 subgoal):
 1. unat x < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. 2 ^ LENGTH(12) \<le> 2 ^ LENGTH(32) proof (prove)
goal:
No subgoals!
theory ArchVSpaceEntries_AI

lemma perform_page_directory_valid_pdpt[wp]:
  "\<lbrace>valid_pdpt_objs and valid_pdi pinv\<rbrace>
      perform_page_directory_invocation pinv \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" apply (simp add: perform_page_directory_invocation_def split_def) apply (rule hoare_pre) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_pdi pinv\<rbrace> perform_page_directory_invocation pinv \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_pdi pinv\<rbrace> case pinv of PageDirectoryFlush typ start end pstart pd asid \<Rightarrow> when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od | PageDirectoryNothing \<Rightarrow> return () \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case pinv of PageDirectoryFlush typ start end pstart pd asid \<Rightarrow> when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od | PageDirectoryNothing \<Rightarrow> return () \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 2. \<And>s. ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_pdi pinv) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ArchVSpaceEntries_AI

lemma mask_out_same_pt:
  "\<lbrakk>is_aligned p 6; x < 2 ^ 6 \<rbrakk> \<Longrightarrow> p + x && ~~ mask pt_bits = p && ~~ mask pt_bits" apply (subst mask_lower_twice[symmetric,where n = 6]) apply (simp add:pt_bits_def pageBits_def) apply (simp add:is_aligned_add_helper) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p 6; x < 2 ^ 6\<rbrakk> \<Longrightarrow> p + x && ~~ mask pt_bits = p && ~~ mask pt_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p 6; x < 2 ^ 6\<rbrakk> \<Longrightarrow> 6 \<le> pt_bits
 2. \<lbrakk>is_aligned p 6; x < 2 ^ 6\<rbrakk> \<Longrightarrow> (p + x && ~~ mask 6) && ~~ mask pt_bits = p && ~~ mask pt_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p 6; x < 2 ^ 6\<rbrakk> \<Longrightarrow> (p + x && ~~ mask 6) && ~~ mask pt_bits = p && ~~ mask pt_bits proof (prove)
goal:
No subgoals!
theory ArchVSpaceEntries_AI

lemma mask_out_same_pd:
  "\<lbrakk>is_aligned p 6; x < 2 ^ 6 \<rbrakk> \<Longrightarrow> p + x && ~~ mask pd_bits = p && ~~ mask pd_bits" apply (subst mask_lower_twice[symmetric,where n = 6]) apply (simp add:pd_bits_def pageBits_def) apply (simp add:is_aligned_add_helper) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p 6; x < 2 ^ 6\<rbrakk> \<Longrightarrow> p + x && ~~ mask pd_bits = p && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p 6; x < 2 ^ 6\<rbrakk> \<Longrightarrow> 6 \<le> pd_bits
 2. \<lbrakk>is_aligned p 6; x < 2 ^ 6\<rbrakk> \<Longrightarrow> (p + x && ~~ mask 6) && ~~ mask pd_bits = p && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p 6; x < 2 ^ 6\<rbrakk> \<Longrightarrow> (p + x && ~~ mask 6) && ~~ mask pd_bits = p && ~~ mask pd_bits proof (prove)
goal:
No subgoals!
theory ArchVSpaceEntries_AI

lemma invocation_duplicates_valid_exst_update[simp]:
  "invocation_duplicates_valid i (trans_state f s) = invocation_duplicates_valid i s" apply (clarsimp simp add: invocation_duplicates_valid_def pti_duplicates_valid_def page_inv_duplicates_valid_def page_inv_entries_safe_def split: sum.splits invocation.splits arch_invocation.splits kernel_object.splits page_table_invocation.splits page_invocation.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invocation_duplicates_valid i (trans_state f s) = invocation_duplicates_valid i s proof (prove)
goal:
No subgoals!
theory ArchAInvsPre

lemma kernel_mappings_slots_eq:
  "p \<in> kernel_mappings \<longleftrightarrow> ucast (p >> 20) \<in> kernel_mapping_slots" apply (simp add: kernel_mappings_def kernel_mapping_slots_def word_le_nat_alt
                   shiftr_20_unat_ucast unat_ucast_kernel_base_rshift) apply (fold word_le_nat_alt) apply (rule iffI) apply (simp add: le_shiftr) apply (simp add: kernel_base_def) apply word_bitwise done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p \<in> kernel_mappings) = (UCAST(32 \<rightarrow> 12) (p >> 20) \<in> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. (unat kernel_base \<le> unat p) = (unat (kernel_base >> 20) \<le> unat (p >> 20)) proof (prove)
goal (1 subgoal):
 1. (kernel_base \<le> p) = (kernel_base >> 20 \<le> p >> 20) proof (prove)
goal (2 subgoals):
 1. kernel_base \<le> p \<Longrightarrow> kernel_base >> 20 \<le> p >> 20
 2. kernel_base >> 20 \<le> p >> 20 \<Longrightarrow> kernel_base \<le> p proof (prove)
goal (1 subgoal):
 1. kernel_base >> 20 \<le> p >> 20 \<Longrightarrow> kernel_base \<le> p proof (prove)
goal (1 subgoal):
 1. 0xE00 \<le> p >> 20 \<Longrightarrow> 0xE0000000 \<le> p proof (prove)
goal:
No subgoals!
theory ArchAInvsPre

lemma valid_global_pd_mappingsE:
  "\<lbrakk>valid_global_vspace_mappings s;
    \<And>pd. \<lbrakk>kheap s (arm_global_pd (arch_state s)) =
             Some (ArchObj (PageDirectory pd));
           \<forall>x. valid_pd_kernel_mappings (arm_kernel_vspace (arch_state s)) s
                 (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" apply (clarsimp simp add: valid_global_vspace_mappings_def obj_at_def) apply (case_tac ko, simp_all add: valid_pd_kernel_mappings_def
                             split: arch_kernel_obj.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_global_vspace_mappings s; \<And>pd. \<lbrakk>kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); \<forall>x. valid_pd_kernel_mappings (arm_kernel_vspace (arch_state s)) s (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>\<And>pd. \<lbrakk>ko = ArchObj (PageDirectory pd); valid_pd_kernel_mappings (arm_kernel_vspace (arch_state s)) s (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> R; kheap s (arm_global_pd (arch_state s)) = Some ko; valid_pd_kernel_mappings (arm_kernel_vspace (arch_state s)) s ko\<rbrakk> \<Longrightarrow> R proof (prove)
goal:
No subgoals!