(*
 * Copyright 2014, General Dynamics C4 Systems
 *
 * SPDX-License-Identifier: GPL-2.0-only
 *)

theory ArchVSpaceEntries_AI
imports VSpaceEntries_AI
begin

context Arch begin global_naming ARM_HYP (*FIXME: arch_split*)

lemma a_type_pdD:
  "a_type ko = AArch APageDirectory \<Longrightarrow> \<exists>pd. ko = ArchObj (PageDirectory pd)"
  by (clarsimp)

primrec
  pde_range_sz :: "pde \<Rightarrow> nat"
where
    "pde_range_sz (InvalidPDE) = 0"
  | "pde_range_sz (SectionPDE ptr x y) = 0"
  | "pde_range_sz (SuperSectionPDE ptr x z) = 4"
  | "pde_range_sz (PageTablePDE ptr) = 0"

primrec
  pte_range_sz :: "pte \<Rightarrow> nat"
where
    "pte_range_sz (InvalidPTE) = 0"
  | "pte_range_sz (LargePagePTE ptr x y) = 4"
  | "pte_range_sz (SmallPagePTE ptr x y) = 0"

primrec
  pde_range :: "pde \<Rightarrow> 11 word \<Rightarrow> 11 word set"
where
    "pde_range (InvalidPDE) p = {}"
  | "pde_range (SectionPDE ptr x y) p = {p}"
  | "pde_range (SuperSectionPDE ptr x z) p =
     (if is_aligned p 4 then {x. x && ~~ mask 4 = p && ~~ mask 4} else {p})"
  | "pde_range (PageTablePDE ptr) p = {p}"

primrec
  pte_range :: "pte \<Rightarrow> 9 word \<Rightarrow> 9 word set"
where
    "pte_range (InvalidPTE) p = {}"
  | "pte_range (LargePagePTE ptr x y) p =
       (if is_aligned p 4 then {x. x && ~~ mask 4 = p && ~~ mask 4} else {p})"
  | "pte_range (SmallPagePTE ptr x y) p = {p}"

abbreviation "valid_pt_entries \<equiv> \<lambda>pt. valid_entries pte_range pt"

abbreviation "valid_pd_entries \<equiv> \<lambda>pd. valid_entries pde_range pd"

definition
  obj_valid_pdpt :: "kernel_object \<Rightarrow> bool"
where
 "obj_valid_pdpt obj \<equiv> case obj of
    ArchObj (PageTable pt) \<Rightarrow> valid_pt_entries pt \<and> entries_align pte_range_sz pt
  | ArchObj (PageDirectory pd) \<Rightarrow> valid_pd_entries pd \<and> entries_align pde_range_sz pd
  | _ \<Rightarrow> True"

lemmas obj_valid_pdpt_simps[simp]
    = obj_valid_pdpt_def
        [split_simps Structures_A.kernel_object.split
                     arch_kernel_obj.split]

abbreviation
  valid_pdpt_objs :: "'z state \<Rightarrow> bool"
where
 "valid_pdpt_objs s \<equiv> \<forall>x \<in> ran (kheap s). obj_valid_pdpt x"

lemma valid_pdpt_init[iff]:
  "valid_pdpt_objs init_A_st"
  by (auto simp: init_A_st_def init_kheap_def valid_entries_def entries_align_def
          elim!: ranE split: if_split_asm)

lemma set_object_valid_pdpt[wp]:
  "\<lbrace>valid_pdpt_objs and K (obj_valid_pdpt obj)\<rbrace>
      set_object ptr obj
   \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
  apply (simp add: set_object_def get_object_def, wp)
  apply (auto simp: fun_upd_def[symmetric] del: ballI elim: ball_ran_updI)
  done

crunch valid_pdpt_objs[wp]: cap_insert, cap_swap_for_delete,empty_slot "valid_pdpt_objs"
  (wp: crunch_wps simp: crunch_simps ignore:set_object)

crunches
  vcpu_save,vcpu_restore,vcpu_enable,get_vcpu,set_vcpu,vcpu_disable,vcpu_read_reg,
  read_vcpu_register,write_vcpu_register
  for valid_pdpt_objs[wp]: "valid_pdpt_objs"
  (wp: crunch_wps simp: crunch_simps ignore: set_object do_machine_op)

lemma vcpu_switch_valid_pdpt_objs[wp]:
  "\<lbrace>valid_pdpt_objs\<rbrace>
     vcpu_switch v
   \<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>"
  apply (simp add: vcpu_switch_def)
  apply (rule hoare_pre)
  apply (wp | wpc | clarsimp)+
  done

crunch valid_pdpt_objs[wp]: flush_page "valid_pdpt_objs"
  (wp: crunch_wps simp: crunch_simps ignore: set_object)

lemma add_3_eq_Suc'[simp]: "n + 3 = Suc (Suc (Suc n))" by simp

lemma shift_0x3C_set:
  "\<lbrakk> is_aligned p 7; 8 \<le> bits; bits < 32; len_of TYPE('a) = bits - 3 \<rbrakk> \<Longrightarrow>
   (\<lambda>x. ucast (x + p && mask bits >> 3) :: ('a :: len) word) ` set [0 :: word32 , 8 .e. 0x78]
        = {x. x && ~~ mask 4 = ucast (p && mask bits >> 3)}"
  apply (clarsimp simp: upto_enum_step_def word_shift_by_3 image_image)
  apply (subst image_cong[where N="{x. x < 2 ^ 4}"])
    apply (safe, simp_all)[1]
     apply (drule plus_one_helper2, simp_all)[1]
    apply (drule word_le_minus_one_leq, simp_all)[1]
   apply (rule_tac f="\<lambda>x. ucast (x && mask bits >> 3)" in arg_cong)
   apply (rule trans[OF add.commute is_aligned_add_or], assumption)
   apply (rule shiftl_less_t2n, simp_all)[1]
  apply safe
   apply (frule upper_bits_unset_is_l2p_32[THEN iffD2, rotated])
    apply (simp add: word_bits_conv)
   apply (rule word_eqI)
   apply (simp add: word_ops_nth_size word_size nth_ucast nth_shiftr
                    nth_shiftl neg_mask_test_bit
                    word_bits_conv)
   apply (safe, simp_all add: is_aligned_nth)[1]
  apply (rule_tac x="ucast x && mask 4" in image_eqI)
   apply (rule word_eqI[rule_format])
   apply (drule_tac x=n in word_eqD)
   apply (simp add: word_ops_nth_size word_size nth_ucast nth_shiftr
                    nth_shiftl)
   apply (safe, simp_all)
  apply (rule order_less_le_trans, rule and_mask_less_size)
   apply (simp_all add: word_size)
  done

lemma mapM_x_store_pte_updates:
  "\<forall>x \<in> set xs. f x && ~~ mask pt_bits = p \<Longrightarrow>
   \<lbrace>\<lambda>s. (\<not> page_table_at p s \<longrightarrow> Q s) \<and>
        (\<forall>pt. ko_at (ArchObj (PageTable pt)) p s
           \<longrightarrow> Q (s \<lparr> kheap := (kheap s) (p := Some (ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x.
         ucast (f x && mask pt_bits >> 3)) ` set xs then pte else pt y)))) \<rparr>))\<rbrace>
     mapM_x (\<lambda>x. store_pte (f x) pte) xs
   \<lbrace>\<lambda>_. Q\<rbrace>"
  apply (induct xs)
   apply (simp add: mapM_x_Nil)
   apply wp
   apply (clarsimp simp: obj_at_def fun_upd_idem)
  apply (simp add: mapM_x_Cons)
  apply (rule hoare_seq_ext, assumption)
  apply (thin_tac "valid P f Q" for P f Q)
  apply (simp add: store_pte_def set_pt_def set_object_def)
  apply (wp get_pt_wp get_object_wp)
  apply (clarsimp simp: obj_at_def a_type_simps)
  apply (erule rsubst[where P=Q])
  apply (rule abstract_state.fold_congs[OF refl refl])
  apply (rule ext, clarsimp simp add: vspace_bits_defs)
  apply (rule ext, clarsimp simp add: vspace_bits_defs)
  done

lemma valid_pt_entries_invalid[simp]:
  "valid_pt_entries (\<lambda>x. InvalidPTE)"
   by (simp add:valid_entries_def)

lemma valid_pd_entries_invalid[simp]:
  "valid_pd_entries (\<lambda>x. InvalidPDE)"
  by (simp add:valid_entries_def)

lemma entries_align_pte_update:
 "\<lbrakk>entries_align pte_range_sz pt;
  (\<forall>y. (P y) \<longrightarrow> is_aligned y (pte_range_sz pte))\<rbrakk>
  \<Longrightarrow> entries_align pte_range_sz (\<lambda>y. if (P y) then pte else pt y)"
  by (simp add:entries_align_def)

lemma entries_align_pde_update:
 "\<lbrakk>entries_align pde_range_sz pd;
  (\<forall>y. (P y) \<longrightarrow> is_aligned y (pde_range_sz pde))\<rbrakk>
  \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if (P y) then pde else pd y)"
  by (simp add:entries_align_def)

lemma valid_pdpt_objs_pdD:
  "\<lbrakk>valid_pdpt_objs s;
    kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory pd))\<rbrakk>
   \<Longrightarrow> valid_pd_entries pd \<and> entries_align pde_range_sz pd"
  by (fastforce simp:ran_def)

lemma valid_pdpt_objs_ptD:
  "\<lbrakk>valid_pdpt_objs s;
    kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable pt))\<rbrakk>
   \<Longrightarrow> valid_pt_entries pt \<and> entries_align pte_range_sz pt"
  by (fastforce simp:ran_def)

lemma mapM_x_store_invalid_pte_valid_pdpt:
  "\<lbrace>valid_pdpt_objs and K (is_aligned p 7) \<rbrace>
     mapM_x (\<lambda>x. store_pte (x + p) InvalidPTE) [0, 8 .e. 0x78]
   \<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>"
  apply (rule hoare_gen_asm)+
  apply (rule hoare_pre, rule_tac p="p && ~~ mask pt_bits" in mapM_x_store_pte_updates)
   apply clarsimp
   apply (rule mask_out_first_mask_some[where n=7])
    apply (drule_tac d=x in is_aligned_add_helper)
     apply (drule subsetD[OF upto_enum_step_subset])
     apply simp
     apply (erule order_le_less_trans, simp)
    apply (simp add: field_simps)
   apply (simp add: vspace_bits_defs)
  apply (clarsimp simp: ranI elim!: ranE split: if_split_asm)
  apply (intro conjI)
   apply (simp add: shift_0x3C_set vspace_bits_defs)
   apply (rule valid_entries_overwrite_groups
    [where S = "{x. x && ~~ mask 4 = ucast (p && mask 12 >> 3)}"])
      apply (fastforce simp add: obj_at_def ran_def)
     apply simp
    apply clarsimp
    apply (case_tac v)
      apply (simp split:if_splits)+
   apply (clarsimp)
   apply (case_tac v, simp_all split:if_splits)
    apply (intro conjI impI)
     apply (rule disjointI)
     apply (clarsimp)+
  apply (rule entries_align_pte_update)
   apply (clarsimp simp:obj_at_def)
   apply (drule(1) valid_pdpt_objs_ptD)
   apply simp
  apply (simp)
  done

lemma mapM_x_store_pde_updates:
  "\<forall>x \<in> set xs. f x && ~~ mask pd_bits = p \<Longrightarrow>
   \<lbrace>\<lambda>s. (\<not> page_directory_at p s \<longrightarrow> Q s) \<and>
        (\<forall>pd. ko_at (ArchObj (PageDirectory pd)) p s
           \<longrightarrow> Q (s \<lparr> kheap := (kheap s) (p := Some (ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x.
         ucast (f x && mask pd_bits >> 3)) ` set xs then pde else pd y)))) \<rparr>))\<rbrace>
     mapM_x (\<lambda>x. store_pde (f x) pde) xs
   \<lbrace>\<lambda>_. Q\<rbrace>"
  apply (induct xs)
   apply (simp add: mapM_x_Nil)
   apply wp
   apply (clarsimp simp: obj_at_def fun_upd_idem)
  apply (simp add: mapM_x_Cons)
  apply (rule hoare_seq_ext, assumption)
  apply (thin_tac "valid P f Q" for P f Q)
  apply (simp add: store_pde_def set_pd_def set_object_def)
  apply (wp get_pd_wp get_object_wp)
  apply (clarsimp simp: obj_at_def a_type_simps)
  apply (erule rsubst[where P=Q])
  apply (rule abstract_state.fold_congs[OF refl refl])
  apply (rule ext, clarsimp simp add: vspace_bits_defs)
  apply (rule ext, clarsimp simp add: vspace_bits_defs)
  done

lemma mapM_x_store_pde_valid_pdpt_objs:
  "\<lbrace>valid_pdpt_objs and K (is_aligned p 7)\<rbrace>
     mapM_x (\<lambda>x. store_pde (x + p) InvalidPDE) [0, 8 .e. 0x78]
   \<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>"
  apply (rule hoare_gen_asm)+
  apply (rule hoare_pre, rule_tac p="p && ~~ mask pd_bits" in mapM_x_store_pde_updates)
   apply clarsimp
   apply (rule mask_out_first_mask_some[where n=7])
    apply (drule_tac d=x in is_aligned_add_helper)
     apply (drule subsetD[OF upto_enum_step_subset])
     apply simp
     apply (erule order_le_less_trans, simp)
    apply (simp add: field_simps)
   apply (simp add: vspace_bits_defs)
  apply (clarsimp simp: ranI elim!: ranE split: if_split_asm)
  apply (simp add: shift_0x3C_set vspace_bits_defs)
  apply (rule conjI)
   apply (rule_tac valid_entries_overwrite_groups
    [where S = "{x. x && ~~ mask 4 = ucast (p && mask 14 >> 3)}"])
      apply (fastforce simp add: obj_at_def ran_def)
     apply fastforce
    apply clarsimp
    apply (case_tac v, simp_all split:if_splits)
    apply clarsimp
    apply (case_tac v, simp_all split:if_splits)
   apply (intro conjI impI allI)
   apply (rule disjointI)
   apply clarsimp
  apply (rule entries_align_pde_update)
   apply (clarsimp simp:obj_at_def)
   apply (drule valid_pdpt_objs_pdD)
    apply (simp add:pd_bits_def pageBits_def)
   apply simp
  apply simp
  done

lemma store_invalid_pde_valid_pdpt:
  "\<lbrace>valid_pdpt_objs and
    (\<lambda>s. \<forall>pd. ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s
      \<longrightarrow> pde = InvalidPDE)\<rbrace>
       store_pde p pde \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
  apply (simp add: store_pde_def set_pd_def, wp get_object_wp)
  apply (clarsimp simp: obj_at_def)
   apply (intro conjI)
   apply (rule valid_entries_overwrite_0, simp_all)
   apply (fastforce simp: ran_def)
  apply (simp add:fun_upd_def)
  apply (rule entries_align_pde_update)
   apply (drule(1) valid_pdpt_objs_pdD)
   apply simp
  apply simp
  done

lemma store_pde_non_master_valid_pdpt:
  "\<lbrace>valid_pdpt_objs and
        (\<lambda>s. \<forall>pd. ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s
        \<longrightarrow> (pde_range_sz (pd (ucast (p && mask pd_bits >> 3) && ~~ mask 4)) = 0
        \<and> pde_range_sz pde = 0))\<rbrace>
       store_pde p pde \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
  apply (simp add: store_pde_def set_pd_def, wp get_object_wp)
  apply (clarsimp simp: obj_at_def)
  apply (intro conjI)
   apply (rule valid_entries_overwrite_0)
    apply (fastforce simp:ran_def)
   apply (drule bspec)
    apply fastforce
   apply (rename_tac p')
   apply (case_tac "pd p'"; cases pde; clarsimp simp: vspace_bits_defs)
  apply (simp add:fun_upd_def)
  apply (rule entries_align_pde_update)
   apply (drule(1) valid_pdpt_objs_pdD,simp)
  apply simp
  done

lemma store_invalid_pte_valid_pdpt:
  "\<lbrace>valid_pdpt_objs and
        (\<lambda>s. \<forall>pt. ko_at (ArchObj (PageTable pt)) (p && ~~ mask pt_bits) s
        \<longrightarrow> pte = InvalidPTE)\<rbrace>
       store_pte p pte \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
  apply (simp add: store_pte_def set_pt_def, wp get_object_wp)
  apply (clarsimp simp: obj_at_def)
   apply (intro conjI)
   apply (rule valid_entries_overwrite_0, simp_all)
   apply (fastforce simp: ran_def)
  apply (simp add:fun_upd_def)
  apply (rule entries_align_pte_update)
   apply (drule (1) valid_pdpt_objs_ptD,simp)
  apply simp
  done

lemma store_pte_non_master_valid_pdpt:
  "\<lbrace>valid_pdpt_objs and
        (\<lambda>s. \<forall>pt. ko_at (ArchObj (PageTable pt)) (p && ~~ mask pt_bits) s
        \<longrightarrow> (pte_range_sz (pt (ucast (p && mask pt_bits >> 3) && ~~ mask 4)) = 0
        \<and> pte_range_sz pte = 0))\<rbrace>
       store_pte p pte \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
  apply (simp add: store_pte_def set_pt_def, wp get_object_wp)
  apply (clarsimp simp: obj_at_def)
  apply (intro conjI)
   apply (rule valid_entries_overwrite_0)
    apply (fastforce simp:ran_def)
   apply (drule bspec)
    apply fastforce
   apply (case_tac "pt pa")
     apply simp
    apply (case_tac pte,simp_all)
    apply (clarsimp simp: vspace_bits_defs)
   apply (case_tac pte,simp_all)
  apply (simp add:fun_upd_def)
  apply (rule entries_align_pte_update)
   apply (drule (1) valid_pdpt_objs_ptD,simp)
  apply simp
  done

lemma unmap_page_valid_pdpt[wp]:
  "\<lbrace>valid_pdpt_objs\<rbrace> unmap_page sz asid vptr pptr \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
  apply (simp add: unmap_page_def mapM_discarded
             cong: vmpage_size.case_cong)
  including no_pre apply wp
    prefer 2
    apply (rule valid_validE[OF find_pd_for_asid_inv])
  apply (rule hoare_pre)
   apply (wp get_object_wp get_pte_wp get_pde_wp lookup_pt_slot_inv_any
             store_invalid_pte_valid_pdpt
             store_invalid_pde_valid_pdpt
             mapM_x_store_invalid_pte_valid_pdpt mapM_x_store_pde_valid_pdpt_objs
                | simp add: mapM_x_map vspace_bits_defs largePagePTE_offsets_def superSectionPDE_offsets_def
                | wpc | simp add: check_mapping_pptr_def)+
  apply (simp add: fun_upd_def[symmetric] is_aligned_mask[symmetric])
  done

crunch valid_pdpt_objs[wp]: flush_table "valid_pdpt_objs"
  (wp: crunch_wps simp: crunch_simps)

lemma unmap_page_table_valid_pdpt_objs[wp]:
  "\<lbrace>valid_pdpt_objs\<rbrace> unmap_page_table asid vptr pt \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
  apply (simp add: unmap_page_table_def)
  including no_pre apply (wp get_object_wp store_invalid_pde_valid_pdpt | wpc)+
  apply (simp add: obj_at_def)
  apply (simp add: page_table_mapped_def)
  apply (wp get_pde_wp | wpc)+
  apply simp
  apply (rule hoare_post_impErr, rule valid_validE,
         rule find_pd_for_asid_inv, simp_all)
  done

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
  apply (subst option.disc_eq_case(2))
  apply (wpsimp wp: set_object_valid_pdpt[THEN hoare_set_object_weaken_pre]
                    get_object_wp
              simp: a_type_simps obj_at_def)
  apply (clarsimp simp: a_type_def
                 split: kernel_object.splits)
  done

crunch valid_pdpt_objs[wp]: finalise_cap, cap_swap_for_delete, empty_slot "valid_pdpt_objs"
  (wp: crunch_wps select_wp preemption_point_inv simp: crunch_simps unless_def ignore:set_object)

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)+

lemmas cap_revoke_preservation_valid_pdpt_objs = cap_revoke_preservation[OF _,
                                                          where E=valid_pdpt_objs,
                                                          simplified, THEN validE_valid]

lemmas rec_del_preservation_valid_pdpt_objs = rec_del_preservation[OF _ _ _ _,
                                                    where P=valid_pdpt_objs, simplified]

crunch valid_pdpt_objs[wp]: cap_delete, cap_revoke "valid_pdpt_objs"
  (rule: cap_revoke_preservation_valid_pdpt_objs)

crunch valid_pdpt_objs[wp]: invalidate_tlb_by_asid, page_table_mapped
   "valid_pdpt_objs"

lemma mapM_x_copy_pde_updates:
  "\<lbrakk> \<forall>x \<in> set xs. f x && ~~ mask pd_bits = 0; is_aligned p pd_bits;
               is_aligned p' pd_bits \<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s. (\<not> page_directory_at p s \<longrightarrow> Q s) \<and> (\<not> page_directory_at p' s \<longrightarrow> Q s) \<and>
        (\<forall>pd pd'. ko_at (ArchObj (PageDirectory pd)) p s
                \<and> ko_at (ArchObj (PageDirectory pd')) p' s
           \<longrightarrow> Q (s \<lparr> kheap := (kheap s) (p' := Some (ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x.
         ucast (f x && mask pd_bits >> 3)) ` set xs then pd y else pd' y)))) \<rparr>))\<rbrace>
     mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs
   \<lbrace>\<lambda>_. Q\<rbrace>"
  including no_pre
  apply (induct xs)
   apply (simp add: mapM_x_Nil)
   apply wp
   apply (clarsimp simp: obj_at_def fun_upd_idem dest!: a_type_pdD)
  apply (simp add: mapM_x_Cons)
  apply wp
  apply (thin_tac "valid P f Q" for P f Q)
  apply (simp add: store_pde_def set_pd_def set_object_def
             cong: bind_cong split del: if_split)
  apply (wp get_object_wp get_pde_wp)
  apply (clarsimp simp: obj_at_def a_type_simps mask_out_add_aligned[symmetric]
             split del: if_split)
  apply (simp add: a_type_simps, safe)
   apply (erule rsubst[where P=Q])
   apply (rule abstract_state.fold_congs[OF refl refl])
   apply (rule ext, clarsimp)
   apply (rule ext, simp)
  apply (erule rsubst[where P=Q])
  apply (rule abstract_state.fold_congs[OF refl refl])
  apply (rule ext, clarsimp simp add: vspace_bits_defs)
  apply (rule ext, simp add: mask_add_aligned vspace_bits_defs)
  done

lemma copy_global_mappings_valid_pdpt_objs[wp]:
  "\<lbrace>valid_pdpt_objs and valid_arch_state and pspace_aligned
            and K (is_aligned p pd_bits)\<rbrace>
       copy_global_mappings p \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
  apply (rule hoare_gen_asm)
  apply (simp add: copy_global_mappings_def)
  apply wp
  apply auto
  done

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)

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)

lemma mapM_x_store_pte_valid_pdpt2:
  "\<lbrace>valid_pdpt_objs and K (is_aligned ptr pt_bits)\<rbrace>
     mapM_x (\<lambda>x. store_pte x InvalidPTE) [ptr, ptr + 8 .e. ptr + 2 ^ pt_bits - 1]
   \<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>"
  apply (rule hoare_gen_asm)+
  apply (rule mapM_x_wp')
  apply (simp add:store_pte_def set_pt_def)
  apply (wp get_pt_wp get_object_wp)
  apply (clarsimp simp: mask_in_range
    split:Structures_A.kernel_object.splits
    arch_kernel_obj.splits)
  apply (rule conjI)
   apply (rule valid_entries_overwrite_0)
    apply (fastforce simp:ran_def obj_at_def)
   apply simp
  apply (simp add:fun_upd_def obj_at_def)
  apply (rule entries_align_pte_update)
   apply (drule (1) valid_pdpt_objs_ptD,simp)
  apply simp
  done

lemma mapM_x_store_pde_valid_pdpt2:
  "\<lbrace>valid_pdpt_objs and K (is_aligned pd pd_bits)\<rbrace>
       mapM_x (\<lambda>x. store_pde ((x << 3) + pd) pde.InvalidPDE)
        [0.e.(kernel_base >> 20) - 1]
       \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
  apply (rule hoare_gen_asm)
  apply (rule mapM_x_wp')
  apply (simp add:store_pde_def set_pd_def)
  apply (wp get_pd_wp get_object_wp)
  apply (clarsimp simp: mask_in_range
    split:Structures_A.kernel_object.splits
    arch_kernel_obj.splits)
  apply (rule conjI)
   apply (rule valid_entries_overwrite_0)
    apply (fastforce simp:ran_def obj_at_def)
   apply simp
  apply (simp add:fun_upd_def obj_at_def)
  apply (rule entries_align_pde_update)
   apply (drule (1) valid_pdpt_objs_pdD,simp)
  apply simp
  done

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

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

crunch valid_pdpt_objs[wp]: cancel_badged_sends "valid_pdpt_objs"
  (simp: crunch_simps filterM_mapM wp: crunch_wps ignore: filterM)

crunch valid_pdpt_objs[wp]: cap_move, cap_insert "valid_pdpt_objs"

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

crunch valid_pdpt_objs[wp]: invoke_tcb "valid_pdpt_objs"
  (wp: check_cap_inv crunch_wps simp: crunch_simps
       ignore: check_cap_at)

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)+

crunch valid_pdpt_objs[wp]: set_extra_badge, transfer_caps_loop "valid_pdpt_objs"
  (rule: transfer_caps_loop_pres)

crunch valid_pdpt_objs[wp]: send_ipc, send_signal,
    do_reply_transfer, invoke_irq_control, invoke_irq_handler "valid_pdpt_objs"
  (wp: crunch_wps simp: crunch_simps
         ignore: clearMemory const_on_failure set_object)

lemma valid_pdpt_objs_trans_state[simp]: "valid_pdpt_objs (trans_state f s) = valid_pdpt_objs s"
  apply (simp add: obj_valid_pdpt_def)
  done

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

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

crunch valid_pdpt_objs[wp]: create_cap "valid_pdpt_objs"
  (ignore: clearMemory simp: crunch_simps unless_def)

lemma init_arch_objects_valid_pdpt:
  "\<lbrace>valid_pdpt_objs and pspace_aligned and valid_arch_state
           and K (\<exists>us sz. orefs = retype_addrs ptr type n us
               \<and> range_cover ptr sz (obj_bits_api type us) n)\<rbrace>
     init_arch_objects type ptr n obj_sz orefs
   \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
  apply (rule hoare_gen_asm)+
  apply (clarsimp simp: init_arch_objects_def
             split del: if_split)
  apply (rule hoare_pre)
   apply (wp | wpc)+
     apply (rule_tac Q="\<lambda>rv. valid_pdpt_objs and pspace_aligned and valid_arch_state"
                  in hoare_post_imp, simp)
     apply (rule mapM_x_wp')
     apply (rule hoare_pre, wp copy_global_mappings_valid_pdpt_objs)
     apply clarsimp
     apply (drule_tac sz=sz in retype_addrs_aligned)
        apply (simp add:range_cover_def)
       apply (drule range_cover.sz,simp add:word_bits_def)
      apply (simp add:range_cover_def)
     apply (clarsimp simp:obj_bits_api_def pd_bits_def pageBits_def
       arch_kobj_size_def default_arch_object_def range_cover_def)+
   apply wp
  apply simp
  done

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)

crunch valid_pdpt[wp]: reset_untyped_cap "valid_pdpt_objs"
  (wp: mapME_x_inv_wp crunch_wps simp: crunch_simps unless_def)

lemma invoke_untyped_valid_pdpt[wp]:
  "\<lbrace>valid_pdpt_objs and invs and ct_active
          and valid_untyped_inv ui\<rbrace>
       invoke_untyped ui
   \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
  apply (rule hoare_pre, rule invoke_untyped_Q)
      apply (wp init_arch_objects_valid_pdpt | simp)+
     apply (auto simp: post_retype_invs_def split: if_split_asm)[1]
    apply (wp | simp)+
  done

crunch valid_pdpt_objs[wp]: perform_asid_pool_invocation,
     perform_asid_control_invocation "valid_pdpt_objs"
  (ignore: delete_objects wp: delete_objects_valid_pdpt static_imp_wp)

abbreviation (input)
  "safe_pt_range \<equiv> \<lambda>slots s. obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt)
                                    \<and> (\<forall>x\<in>set (tl slots). pt (ucast (x && mask pt_bits >> 3))
                                      = pte.InvalidPTE))
                              (hd slots && ~~ mask pt_bits) s"

abbreviation (input)
  "safe_pd_range \<equiv> \<lambda>slots s. obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd)
                                    \<and> (\<forall>x\<in>set (tl slots). pd (ucast (x && mask pd_bits >> 3))
                                      = pde.InvalidPDE))
                              (hd slots && ~~ mask pd_bits) s"

definition
  "page_inv_entries_pre entries \<equiv>
   let slots = (case entries of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots)
   in (if \<exists>sl. slots = [sl]
    then case entries of
        Inl (pte, _) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt)
                     \<and> pt (ucast (hd slots && mask pt_bits >> 3) && ~~ mask 4) = pte
                     \<and> pte_range_sz pte = 0)
                 (hd slots && ~~ mask pt_bits)
            and K (pte_range_sz pte = 0)
      | Inr (pde, _) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd)
                     \<and> pd (ucast (head slots && mask pd_bits >> 3) && ~~ mask 4)
                            = pde \<and> pde_range_sz pde = 0)
                 (hd slots && ~~ mask pd_bits)
           and K (pde_range_sz pde = 0)
    else  (\<lambda>s. (\<exists>p. is_aligned p 7 \<and> slots = map (\<lambda>x. x + p) [0, 8 .e. 0x78])))
   and K (case entries of Inl (pte,slots) \<Rightarrow> pte \<noteq> InvalidPTE
     | Inr (pde,slots) \<Rightarrow> pde \<noteq> InvalidPDE)"

definition
  "page_inv_entries_safe entries \<equiv>
   let slots = (case entries of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots)
   in if \<exists>sl. slots = [sl]
    then case entries of
        Inl (pte, _) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt)
                     \<and> pt (ucast (hd slots && mask pt_bits >> 3) && ~~ mask 4) = pte
                     \<and> pte_range_sz pte = 0)
                 (hd slots && ~~ mask pt_bits)
            and K (pte_range_sz pte = 0)
      | Inr (pde, _) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd)
                     \<and> pd (ucast (head slots && mask pd_bits >> 3) && ~~ mask 4)
                            = pde \<and> pde_range_sz pde = 0)
                 (hd slots && ~~ mask pd_bits)
           and K (pde_range_sz pde = 0)
    else  (\<lambda>s. (\<exists>p. is_aligned p 7 \<and> slots = map (\<lambda>x. x + p) [0, 8 .e. 0x78]
                  \<and> (case entries of
                     Inl (pte, _) \<Rightarrow> safe_pt_range slots s
                   | Inr (pde, _) \<Rightarrow> safe_pd_range slots s
                     )))"

definition
  "page_inv_duplicates_valid iv \<equiv> case iv of
         PageMap asid cap ct_slot entries \<Rightarrow>
            page_inv_entries_safe entries
       | _ \<Rightarrow> \<top>"

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

lemma pde_range_interD:
 "pde_range pde p \<inter> pde_range pde' p' \<noteq> {}
  \<Longrightarrow> pde \<noteq> InvalidPDE \<and> pde' \<noteq> InvalidPDE
      \<and> p && ~~ mask 4 = p' && ~~ mask 4"
  apply (drule int_not_emptyD)
  apply (case_tac pde,simp_all split:if_splits)
     apply (case_tac pde',simp_all split:if_splits)
    apply (case_tac pde',simp_all split:if_splits)
   apply clarsimp
   apply (case_tac pde', simp_all split:if_splits)
  apply (case_tac pde', simp_all split:if_splits)
  done

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

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

(* BUG , revisit the following lemmas , moved from ArchAcc_R.thy *)
lemma mask_pd_bits_shift_ucast_align[simp]:
  "is_aligned (ucast (p && mask pd_bits >> 3)::11 word) 4 =
   is_aligned ((p::word32) >> 3) 4"
  by (clarsimp simp: is_aligned_mask mask_def vspace_bits_defs) word_bitwise

lemma mask_pt_bits_shift_ucast_align[simp]:
  "is_aligned (ucast (p && mask pt_bits >> 3)::9 word) 4 =
   is_aligned ((p::word32) >> 3) 4"
  by (clarsimp simp: is_aligned_mask mask_def vspace_bits_defs)
     word_bitwise

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

lemma unat_ucast_9_32:
  fixes x :: "9 word"
  shows "unat (ucast x :: word32) = unat x"
  unfolding ucast_def unat_def
  apply (subst int_word_uint)
  apply (subst mod_pos_pos_trivial)
    apply simp
   apply (rule lt2p_lem)
   apply simp
  apply simp
  done

lemma store_pte_valid_pdpt:
  "\<lbrace>valid_pdpt_objs and page_inv_entries_safe (Inl (pte, slots))\<rbrace>
       store_pte (hd slots) pte \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
  apply (rule hoare_name_pre_state)
  apply (clarsimp simp:page_inv_entries_safe_def split:if_splits)
   apply (clarsimp simp:store_pte_def set_pt_def)
   apply (wp get_pt_wp get_object_wp)
   apply (clarsimp simp:obj_at_def pte_bits_def
     split:pte.splits arch_kernel_obj.splits)
  apply (rule conjI)
    apply (drule(1) valid_pdpt_objs_ptD)
    apply (rule valid_entries_overwrite_0)
     apply simp
    apply (case_tac pte)
     apply simp+
    apply (case_tac "pta p",simp_all)
    apply clarsimp
   apply (simp add:fun_upd_def)
   apply (rule entries_align_pte_update)
    apply (drule (1) valid_pdpt_objs_ptD,simp)
   apply simp
  apply (simp add:hd_map_simp upto_enum_def upto_enum_step_def)
  apply (clarsimp simp:store_pte_def set_pt_def)
  apply (wp get_pt_wp get_object_wp)
  apply (clarsimp simp:obj_at_def pte_bits_def
     split:pte.splits arch_kernel_obj.splits)
  apply (drule(1) valid_pdpt_objs_ptD)
  apply (rule conjI)
   apply (rule valid_entries_overwrite_0)
    apply simp
   apply (rule ccontr)
   apply (drule pte_range_interD)
   apply clarsimp
   apply (simp add:ucast_neg_mask)
   apply (subst (asm) is_aligned_neg_mask_eq[where n = 4])
    apply (rule is_aligned_shiftr[OF is_aligned_andI1])
    apply simp
   apply (drule_tac x = "((p && ~~ mask pt_bits)  + ((ucast pa) << 3))" in bspec)
    apply (clarsimp simp: tl_map_simp upto_0_to_n2 image_def)
    apply (rule_tac x = "unat (((ucast pa)::word32) - (p && mask pt_bits >> 3))" in bexI)
     apply (simp add:ucast_nat_def shiftl_t2n mask_out_sub_mask)
     apply (subst shiftl_t2n[where n = 3,simplified field_simps,simplified,symmetric])
     apply (subst shiftr_shiftl1)
      apply simp+
     apply (subst is_aligned_neg_mask_eq)
      apply (erule is_aligned_andI1[OF is_aligned_weaken])
      apply simp
     apply simp
    apply simp
    apply (drule_tac s = "ucast (p && mask pt_bits >> 3)" in sym)
    apply (simp add:mask_out_sub_mask field_simps)
    apply (drule_tac f = "ucast::(9 word\<Rightarrow>word32)" in arg_cong)
    apply (simp add: ucast_pt_index[simplified pte_bits_def])
    apply (simp add:unat_ucast_9_32)
    apply (rule conjI)
     apply (subgoal_tac "unat (pa && mask 4)\<noteq> 0")
      apply simp
     apply (simp add:unat_gt_0)
    apply (rule unat_less_helper)
    apply (rule le_less_trans[OF word_and_le1])
    apply (simp add:mask_def)
   apply (simp add:field_simps neg_mask_add_mask)
   apply (thin_tac "ucast y = x" for y x)
   apply (subst (asm) less_mask_eq[where n = pt_bits])
    apply (rule shiftl_less_t2n)
     apply (simp add:vspace_bits_defs)
     apply word_bitwise
    apply (simp add:vspace_bits_defs)
   apply (subst (asm) shiftl_shiftr_id)
    apply simp
   apply (simp,word_bitwise)
   apply (simp add:ucast_ucast_id)
  apply (simp add:fun_upd_def entries_align_def)
  apply (rule is_aligned_weaken[OF _ pte_range_sz_le])
  apply (simp add:is_aligned_shiftr)
  done

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

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

lemma ucast_pd_index11:
  "\<lbrakk>is_aligned (p::word32) 7\<rbrakk>
   \<Longrightarrow> ucast ((pa && mask 4) + (ucast (p && mask 14 >> 3)::11 word))
   =  ucast (pa && mask 4) + (p && mask 14 >> 3)"
  apply (simp add:is_aligned_mask mask_def)
  apply word_bitwise
  apply (auto simp:carry_def)
  done

lemma store_pde_valid_pdpt:
  "\<lbrace>valid_pdpt_objs and page_inv_entries_safe (Inr (pde, slots))\<rbrace>
       store_pde (hd slots) pde \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
  apply (rule hoare_name_pre_state)
  apply (clarsimp simp:page_inv_entries_safe_def split:if_splits)
   apply (clarsimp simp:store_pde_def set_pd_def)
   apply (wp get_pd_wp get_object_wp)
   apply (clarsimp simp:obj_at_def pde_bits_def
     split:pde.splits arch_kernel_obj.splits)
   apply (drule(1) valid_pdpt_objs_pdD)
   apply (rule conjI)
    apply (rule valid_entries_overwrite_0)
     apply simp
    apply (case_tac pde,simp_all)
     apply (case_tac "pda p",simp_all)
     apply clarsimp
    apply (case_tac "pda p",simp_all)
    apply clarsimp
   apply (simp add:fun_upd_def)
   apply (rule entries_align_pde_update)
    apply simp+
  apply (simp add:hd_map_simp upto_enum_def upto_enum_step_def)
  apply (clarsimp simp:store_pde_def set_pd_def)
  apply (wp get_pd_wp get_object_wp)
  apply (clarsimp simp:obj_at_def pde_bits_def
     split:pde.splits arch_kernel_obj.splits)
  apply (drule(1) valid_pdpt_objs_pdD)
  apply (rule conjI)
   apply (rule valid_entries_overwrite_0)
    apply simp
   apply (rule ccontr)
   apply (drule pde_range_interD)
   apply clarsimp
   apply (simp add:ucast_neg_mask)
   apply (subst (asm) is_aligned_neg_mask_eq[where n = 4])
    apply (rule is_aligned_shiftr[OF is_aligned_andI1])
    apply simp
   apply (drule_tac x = "((p && ~~ mask pd_bits)  + ((ucast pa) << 3))" in bspec)
    apply (clarsimp simp: tl_map_simp upto_0_to_n2 image_def)
    apply (rule_tac x = "unat (((ucast pa)::word32) - (p && mask pd_bits >> 3))" in bexI)
     apply (simp add:ucast_nat_def shiftl_t2n mask_out_sub_mask)
     apply (subst shiftl_t2n[where n = 3,simplified field_simps,simplified,symmetric])
     apply (subst shiftr_shiftl1)
      apply simp+
     apply (subst is_aligned_neg_mask_eq)
      apply (erule is_aligned_andI1[OF is_aligned_weaken])
      apply simp
     apply simp
    apply simp
    apply (drule_tac s = "ucast (p && mask pd_bits >> 3)" in sym)
    apply (simp add:mask_out_sub_mask field_simps)
    apply (drule_tac f = "ucast::(11 word\<Rightarrow>word32)" in arg_cong)
    apply (simp add:ucast_pd_index[simplified pde_bits_def])
    apply (simp add:unat_ucast_11_32)
    apply (rule conjI)
     apply (subgoal_tac "unat (pa && mask 4)\<noteq> 0")
      apply simp
     apply (simp add:unat_gt_0)
    apply (rule unat_less_helper)
    apply (rule le_less_trans[OF word_and_le1])
    apply (simp add:mask_def)
   apply (simp add:field_simps neg_mask_add_mask)
   apply (thin_tac "ucast y = x" for y x)
   apply (subst (asm) less_mask_eq[where n = pd_bits])
    apply (rule shiftl_less_t2n)
     apply (simp add:vspace_bits_defs)
     apply word_bitwise
    apply (simp add:vspace_bits_defs)
   apply (subst (asm) shiftl_shiftr_id)
     apply simp
    apply (simp,word_bitwise)
   apply (simp add:ucast_ucast_id)
  apply (simp add:entries_align_def)
  apply (rule is_aligned_weaken[OF _ pde_range_sz_le])
  apply (simp add:is_aligned_shiftr)
  done

lemma set_cap_page_inv_entries_safe:
  "\<lbrace>page_inv_entries_safe x\<rbrace> set_cap y z \<lbrace>\<lambda>_. page_inv_entries_safe x\<rbrace>"
  apply (simp add:page_inv_entries_safe_def set_cap_def split_def
    get_object_def set_object_def)
  apply (wp | wpc)+
  apply (case_tac x)
  apply (auto simp:obj_at_def
    Let_def split:if_splits option.splits)
  done

crunch inv[wp]: pte_check_if_mapped, pde_check_if_mapped "\<lambda>s. P s"

lemma perform_page_valid_pdpt[wp]:
  "\<lbrace>valid_pdpt_objs and valid_page_inv pinv and page_inv_duplicates_valid pinv\<rbrace>
        perform_page_invocation pinv \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
  apply (simp add: perform_page_invocation_def page_inv_duplicates_valid_def)
  apply (cases pinv,
         simp_all add: mapM_discarded page_inv_entries_safe_def
            split: sum.split arch_cap.split option.split,
         safe intro!: hoare_gen_asm hoare_gen_asm[unfolded K_def],
         simp_all add: mapM_x_Nil mapM_x_Cons mapM_x_map)
            apply (wp store_pte_valid_pdpt store_pde_valid_pdpt get_master_pte_wp get_master_pde_wp
                      store_pte_non_master_valid_pdpt store_pde_non_master_valid_pdpt
                      mapM_x_wp'[OF store_invalid_pte_valid_pdpt
                        [where pte=pte.InvalidPTE, simplified]]
                      mapM_x_wp'[OF store_invalid_pde_valid_pdpt
                        [where pde=pde.InvalidPDE, simplified]]
                      set_cap_page_inv_entries_safe
                      hoare_vcg_imp_lift[OF set_cap_arch_obj_neg] hoare_vcg_all_lift
                 | clarsimp simp: cte_wp_at_weakenE[OF _ TrueI] obj_at_def
                                  pte_range_sz_def pde_range_sz_def swp_def valid_page_inv_def
                                  valid_slots_def page_inv_entries_safe_def pte_check_if_mapped_def
                                  pde_check_if_mapped_def
                           split: pte.splits pde.splits
                 | wp (once) hoare_drop_imps)+
  done

definition
  "pti_duplicates_valid iv \<equiv>
   case iv of PageTableMap cap ct_slot pde pd_slot
     \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd)
                     \<and> pd (ucast (pd_slot && mask pd_bits >> 3) && ~~ mask 4)
                            = pde \<and> pde_range_sz pde = 0)
                 (pd_slot && ~~ mask pd_bits)

           and K (pde_range_sz pde = 0)
  | _ \<Rightarrow> \<top>"

definition
  "invocation_duplicates_valid i \<equiv>
   case i of
     InvokeArchObject (InvokePage pinv) \<Rightarrow> page_inv_duplicates_valid pinv
   | InvokeArchObject (InvokePageTable pti) \<Rightarrow> pti_duplicates_valid pti
   | _ \<Rightarrow> \<top>"

lemma perform_page_table_valid_pdpt[wp]:
  "\<lbrace>valid_pdpt_objs and valid_pti pinv and pti_duplicates_valid pinv\<rbrace>
      perform_page_table_invocation pinv \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
  apply (simp add: perform_page_table_invocation_def split_def vspace_bits_defs
             cong: page_table_invocation.case_cong
                   option.case_cong cap.case_cong arch_cap.case_cong)
  apply (rule hoare_pre)
   apply (wp store_pde_non_master_valid_pdpt hoare_vcg_ex_lift
             set_cap_arch_obj mapM_x_store_pte_valid_pdpt2[simplified vspace_bits_defs, simplified]
              | wpc
              | simp add: swp_def
              | strengthen all_imp_ko_at_from_ex_strg)+
  apply (clarsimp simp: pti_duplicates_valid_def valid_pti_def)
  apply (auto simp: obj_at_def cte_wp_at_caps_of_state valid_cap_simps
                    cap_aligned_def vspace_bits_defs
            intro!: inj_onI)
  done

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

crunch valid_pdpt_objs[wp]: perform_vcpu_invocation "valid_pdpt_objs"
  (ignore: delete_objects wp: delete_objects_valid_pdpt static_imp_wp)

lemma perform_invocation_valid_pdpt[wp]:
  "\<lbrace>invs and ct_active and valid_invocation i and valid_pdpt_objs
           and invocation_duplicates_valid i\<rbrace>
      perform_invocation blocking call i
         \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
  apply (cases i, simp_all)
  apply (wp send_signal_interrupt_states | simp)+
  apply (simp add: arch_perform_invocation_def)
  apply (rule hoare_pre)
  apply (wp | wpc | simp)+
  apply (auto simp: valid_arch_inv_def invocation_duplicates_valid_def)
  done

lemma neg_mask_pt_7_4:
  "(ptr && mask pt_bits >> 3) && ~~ mask 4 =
   (ptr::word32) && ~~ mask 7 && mask pt_bits >> 3"
  by (word_eqI_solve simp: vspace_bits_defs)

lemma neg_mask_pd_7_4:
  "(ptr && mask pd_bits >> 3) && ~~ mask 4 =
   (ptr::word32) && ~~ mask 7 && mask pd_bits >> 3"
  by (word_eqI_solve simp: vspace_bits_defs)

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

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

lemma ensure_safe_mapping_ensures[wp]:
  "\<lbrace>valid_pdpt_objs and (case entries of (Inl (SmallPagePTE _ _ _, [_])) \<Rightarrow> \<top>
                  | (Inl (SmallPagePTE _ _ _, _)) \<Rightarrow> \<bottom>
                  | (Inl (LargePagePTE _ _ _, [])) \<Rightarrow> \<bottom>
                  | (Inr (SectionPDE _ _ _, [_])) \<Rightarrow> \<top>
                  | (Inr (SuperSectionPDE _ _ _, [])) \<Rightarrow> \<bottom>
                  | (Inr (SectionPDE _ _ _, _)) \<Rightarrow> \<bottom>
                  | _ \<Rightarrow> page_inv_entries_pre entries)\<rbrace>
     ensure_safe_mapping entries
   \<lbrace>\<lambda>rv. page_inv_entries_safe entries\<rbrace>,-"
  proof -
    have [simp]:
      "\<And>s a. page_inv_entries_pre (Inl (pte.InvalidPTE, a)) s \<Longrightarrow>
      page_inv_entries_safe (Inl (pte.InvalidPTE, a)) s"
      apply (clarsimp simp:page_inv_entries_pre_def page_inv_entries_safe_def
        split:if_splits)
      done
    have name_pre:
      "\<And>F P Q. (\<And>s. P s \<Longrightarrow> \<lbrace>(=) s \<rbrace> F \<lbrace>Q\<rbrace>, -) \<Longrightarrow> \<lbrace>P\<rbrace> F \<lbrace>Q\<rbrace>,-"
      apply (simp add:validE_R_def validE_def)
      apply (rule hoare_name_pre_state)
      apply assumption
      done
    have mask_neg_mask_order[simp]:
      "\<And>a m n. a && ~~ mask m && mask n = a && mask n && ~~ mask m"
       by (simp add:word_bw_comms word_bw_lcs)
    have align_entry_ptD:
      "\<And>pt m x xb xc. \<lbrakk>pt m = pte.LargePagePTE x xb xc; entries_align pte_range_sz pt\<rbrakk>
       \<Longrightarrow> is_aligned m 4"
      apply (simp add:entries_align_def)
      apply (drule_tac x = m in spec,simp)
      done
    have align_entry_pdD:
      "\<And>pd m x xb xc. \<lbrakk>pd m = pde.SuperSectionPDE x xb xc; entries_align pde_range_sz pd\<rbrakk>
       \<Longrightarrow> is_aligned m 4"
      apply (simp add:entries_align_def)
      apply (drule_tac x = m in spec,simp)
      done
    have pt_offset_bitwise[simp]:"\<And>a. (ucast ((a::word32) && mask pt_bits && ~~ mask 7  >> 3)::9 word)
      = (ucast (a  && mask pt_bits >> 3)::9 word) && ~~ mask 4"
    apply (simp add: vspace_bits_defs mask_def)
    apply word_bitwise
    done
    have pt_offset_bitwise_pt_bits[simp]:"\<And>a. (ucast ((a::word32) && mask pt_bits && ~~ mask 7  >> pte_bits)::9 word)
      = (ucast (a  && mask pt_bits >> 3)::9 word) && ~~ mask 4"
    by (simp add: pte_bits_def)
    have pd_offset_bitwise[simp]:"\<And>a. (ucast ((a::word32) && mask pd_bits && ~~ mask 7  >> 3)::11 word)
      = (ucast (a  && mask pd_bits >> 3)::11 word) && ~~ mask 4"
    apply (simp add: vspace_bits_defs mask_def)
    apply word_bitwise
    done
    have pd_offset_bitwise_pt_bits[simp]:"\<And>a. (ucast ((a::word32) && mask pd_bits && ~~ mask 7  >> pde_bits)::11 word)
      = (ucast (a  && mask pd_bits >> 3)::11 word) && ~~ mask 4"
    by (simp add: pde_bits_def)
    have mask_neq_0:
      "\<And>z zs xa p g. \<lbrakk>[0 :: word32, 8 .e. 0x78] = z # zs; xa \<in> set zs; is_aligned p 7; 7 \<le> g\<rbrakk>
         \<Longrightarrow> (p + xa && mask g >> 3) && mask 4 \<noteq> 0"
     apply (rule ccontr)
      apply (simp add:is_aligned_mask[symmetric])
       apply (drule is_aligned_shiftl[where n = 7 and m = 3,simplified])
      apply (subst (asm) shiftr_shiftl1)
       apply simp+
      apply (subst (asm) is_aligned_neg_mask_eq)
       apply (rule is_aligned_andI1)
       apply (erule aligned_add_aligned)
        apply (clarsimp simp :upto_enum_def upto_enum_step_def
         Fun.comp_def upto_0_to_n2 is_aligned_mult_triv2[where n = 3,simplified])
       apply simp
      apply (simp add:is_aligned_mask mask_twice
        pt_bits_def pageBits_def min_def)
      apply (subst (asm) is_aligned_mask[symmetric])
      apply (subst (asm) is_aligned_add_helper)
       apply simp
      apply (clarsimp simp :upto_enum_def upto_enum_step_def
         Fun.comp_def upto_0_to_n2)
      apply (subst shiftl_t2n
        [where n = 3,simplified field_simps,simplified,symmetric])+
      apply (rule shiftl_less_t2n[where m = 7,simplified])
       apply (rule word_of_nat_less)
       apply simp
      apply simp
     apply (clarsimp simp :upto_enum_def upto_enum_step_def
         Fun.comp_def upto_0_to_n2)
     apply (cut_tac x = "of_nat x" and n = 3 in word_power_nonzero_32)
         apply (simp add:word_of_nat_less word_bits_def of_nat_neq_0)+
     done
    have neq_pt_offset: "\<And>z zs xa (p::word32). \<lbrakk>[0 , 8 .e. 0x78] = z # zs;
        xa \<in> set zs;is_aligned p 7 \<rbrakk> \<Longrightarrow>
        ucast (p + xa && mask pt_bits >> 3) && ~~ mask 4 \<noteq> ((ucast (p + xa && mask pt_bits >> 3))::9 word)"
      apply (rule ccontr)
      apply (simp add:mask_out_sub_mask ucast_and_mask[symmetric])
      apply (drule arg_cong[where f = unat])
      apply (simp add:unat_ucast)
      apply (subst (asm) mod_less)
       apply (rule unat_less_helper)
       apply (rule le_less_trans[OF word_and_le1])
       apply (simp add:mask_def)
      apply (simp add:unat_eq_0)
      apply (drule(2) mask_neq_0[of _ _ _ _ pt_bits])
       apply (simp add:pt_bits_def pageBits_def)+
      done
    have neq_pd_offset: "\<And>z zs xa (p::word32). \<lbrakk>[0 , 8 .e. 0x78] = z # zs;
        xa \<in> set zs;is_aligned p 7 \<rbrakk> \<Longrightarrow>
        ucast (p + xa && mask pd_bits >> 3) && ~~ mask 4 \<noteq> ((ucast (p + xa && mask pd_bits >> 3)) :: 11 word)"
      apply (simp add:mask_out_sub_mask)
      apply (rule ccontr)
      apply (simp add:mask_out_sub_mask ucast_and_mask[symmetric])
      apply (drule arg_cong[where f = unat])
      apply (simp add:unat_ucast)
      apply (subst (asm) mod_less)
       apply (rule unat_less_helper)
       apply (rule le_less_trans[OF word_and_le1])
       apply (simp add:mask_def)
      apply (simp add:unat_eq_0)
      apply (drule(2) mask_neq_0[of _ _ _ _ pd_bits])
       apply (simp add:pd_bits_def pageBits_def)+
      done
    have invalid_pteI:
      "\<And>a pt x y z. \<lbrakk>valid_pt_entries pt; (a && ~~ mask 4) \<noteq> a;
       pt (a && ~~ mask 4) = pte.LargePagePTE x y z \<rbrakk>
       \<Longrightarrow> pt a = pte.InvalidPTE"
      apply (drule(1) valid_entriesD[rotated])
      apply (case_tac "pt a"; simp add:mask_lower_twice is_aligned_neg_mask split:if_splits)
      done
    have invalid_pdeI:
      "\<And>a pd x y z. \<lbrakk>valid_pd_entries pd; (a && ~~ mask 4) \<noteq> a;
       pd (a && ~~ mask 4) = pde.SuperSectionPDE x y z \<rbrakk>
       \<Longrightarrow> pd a = pde.InvalidPDE"
      apply (drule(1) valid_entriesD[rotated])
      apply (case_tac "pd a",
        simp_all add:mask_lower_twice is_aligned_neg_mask
        split:if_splits)
      done
    have inj[simp]:
      "\<And>p. is_aligned (p::word32) 7 \<Longrightarrow> inj_on (\<lambda>x. toEnum x * 8 + p) {Suc 0..<16}"
      apply (clarsimp simp:inj_on_def)
      apply (subst (asm) shiftl_t2n[where n = 3,simplified field_simps,simplified,symmetric])+
      apply (drule arg_cong[where f = "\<lambda>x. x >> 3"])
      apply (simp add:shiftl_shiftr_id word_of_nat_less)
      apply (simp add:of_nat_inj)
      done

  show ?thesis
  apply (rule name_pre)
  apply (case_tac entries)
   apply (case_tac a, case_tac aa)
     apply (simp add:page_inv_entries_pre_def page_inv_entries_safe_def
       | wp | intro conjI impI)+
     apply (simp split:list.splits add:page_inv_entries_pre_def)+
    apply (rename_tac obj_ref vm_attributes cap_rights slot slots)
    apply (elim conjE exE)
    apply (subst mapME_x_Cons)
    apply simp
    apply wp
     apply (rule_tac Q' = "\<lambda>r s. \<forall>x \<in> set slots. obj_at
                (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and>
                 pt (ucast (x && mask pt_bits >> 3)) = pte.InvalidPTE)
                (hd (slot # slots) && ~~ mask pt_bits) s" in hoare_post_imp_R)
      apply (wp mapME_x_accumulate_checks[where Q = "\<lambda>s. valid_pdpt_objs s"] )
          apply (wp get_master_pte_wp| wpc | simp)+
         apply clarsimp
         apply (frule_tac x = xa in mask_out_same_pt)
          apply (clarsimp simp:upto_enum_def upto_enum_step_def upto_0_to_n2)
          apply (subst shiftl_t2n[where n = 3,simplified field_simps,simplified,symmetric])
          apply (rule shiftl_less_t2n[where m = 7,simplified])
           apply (simp add:word_of_nat_less)
          apply simp
         apply (frule_tac x = z in mask_out_same_pt)
          apply (clarsimp simp:upto_enum_def upto_enum_step_def upto_0_to_n2)
         apply (clarsimp simp:field_simps obj_at_def
           split:pte.splits)
         apply (intro conjI impI)
             apply (clarsimp simp: pte_bits_def)
            apply (drule(1) valid_pdpt_objs_ptD)
            apply (clarsimp simp: bit.conj_assoc)
            apply (frule align_entry_ptD,simp)
            apply (clarsimp simp: is_aligned_neg_mask_eq[of _ 4] pte_bits_def)
           apply clarsimp
           apply (drule(1) valid_pdpt_objs_ptD,clarify)
           apply (erule(4) invalid_pteI[OF _ neq_pt_offset])
          apply (clarsimp simp: pte_bits_def)
         apply (clarsimp simp:  pte_bits_def)
         apply (drule(1) valid_pdpt_objs_ptD)
         apply (frule align_entry_ptD,simp)
         apply simp
        apply (wp hoare_drop_imps |wpc|simp)+
      apply (clarsimp simp:upto_enum_def upto_enum_step_def
        upto_0_to_n2 Fun.comp_def distinct_map)
     apply (intro exI conjI,fastforce+)
     apply (simp add:obj_at_def hd_map_simp
         upto_0_to_n2 upto_enum_def upto_enum_step_def)
     apply (frule_tac x = 1 in bspec,fastforce+)
    apply ((wp hoare_drop_imps |wpc|simp)+)[1]
   apply (simp add:page_inv_entries_pre_def page_inv_entries_safe_def
       | wp | intro conjI impI)+
    apply (simp split:list.splits add:page_inv_entries_pre_def mapME_singleton)
    apply (wp get_master_pte_wp |wpc | simp)+
    apply (clarsimp simp:obj_at_def split:pte.splits)
   apply (clarsimp simp:page_inv_entries_safe_def split:list.splits)
  apply (simp split:list.splits add:page_inv_entries_pre_def mapME_singleton)
  apply (case_tac b,case_tac a)
     apply ((simp add:page_inv_entries_pre_def page_inv_entries_safe_def
       | wp | intro conjI impI)+)[1]
    apply simp
    apply wp[1]
   apply (simp split:list.splits add:page_inv_entries_pre_def mapME_singleton)
   apply (wp get_master_pde_wp | wpc | simp)+
   apply (clarsimp simp:obj_at_def page_inv_entries_safe_def pde_bits_def
     split:pde.splits)
  apply (simp split:list.splits if_splits
    add:page_inv_entries_pre_def Let_def page_inv_entries_safe_def)
  apply (elim conjE exE)
  apply (subst mapME_x_Cons)
  apply simp
  apply wp
   apply (rule_tac Q' = "\<lambda>r s. \<forall>x \<in> set x22.
                                 obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and>
                                                   pd (ucast (x && mask pd_bits >> 3)) = InvalidPDE)
                               (x21 && ~~ mask pd_bits) s" in hoare_post_imp_R)
    apply (wp mapME_x_accumulate_checks[where Q = "\<lambda>s. valid_pdpt_objs s"] )
        apply (wp get_master_pde_wp| wpc | simp)+
       apply clarsimp
       apply (frule_tac x = xa in mask_out_same_pd)
        apply (clarsimp simp:upto_enum_def upto_enum_step_def upto_0_to_n2)
        apply (subst shiftl_t2n[where n = 3,simplified field_simps,simplified,symmetric])
        apply (rule shiftl_less_t2n[where m = 7,simplified])
         apply (simp add:word_of_nat_less)
        apply simp
       apply (frule_tac x = z in mask_out_same_pd)
        apply (clarsimp simp:upto_enum_def upto_enum_step_def upto_0_to_n2)
       apply (clarsimp simp: field_simps obj_at_def split: pde.splits)
       apply (drule(1) valid_pdpt_objs_pdD)
       apply (intro conjI impI; clarsimp simp: pde_bits_def)
          apply (frule align_entry_pdD,simp)
          apply (clarsimp simp: pde_bits_def)
         apply (frule(1) align_entry_pdD)
         apply simp
        apply (frule(1) align_entry_pdD)
        apply simp
       apply (frule(1) align_entry_pdD)
       apply (erule(4) invalid_pdeI[OF _ neq_pd_offset])
      apply (wp hoare_drop_imps |wpc|simp)+
    apply (clarsimp simp:upto_enum_def upto_enum_step_def upto_0_to_n2 Fun.comp_def distinct_map)
   apply (intro exI conjI,fastforce+)
   apply (simp add:obj_at_def hd_map_simp upto_0_to_n2 upto_enum_def upto_enum_step_def)
   apply (frule_tac x = 1 in bspec,fastforce+)
  apply (wp get_master_pde_wp | simp | wpc)+
  done
qed

lemma create_mapping_entries_safe[wp]:
  "\<lbrace>\<exists>\<rhd>pd and K (vmsz_aligned vptr sz) and K (is_aligned pd pd_bits)
          and K (vptr < kernel_base)
          and valid_vspace_objs and pspace_aligned and
          (\<exists>\<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits))\<rbrace>
      create_mapping_entries ptr vptr sz rights attrib pd
   \<lbrace>\<lambda>entries. case entries of (Inl (SmallPagePTE _ _ _, [_])) \<Rightarrow> \<top>
                  | (Inl (SmallPagePTE _ _ _, _)) \<Rightarrow> \<bottom>
                  | (Inl (LargePagePTE _ _ _, [])) \<Rightarrow> \<bottom>
                  | (Inr (SectionPDE _ _ _, [_])) \<Rightarrow> \<top>
                  | (Inr (SectionPDE _ _ _, _)) \<Rightarrow> \<bottom>
                  | (Inr (SuperSectionPDE _ _ _, [])) \<Rightarrow> \<bottom>
                  | _ \<Rightarrow> page_inv_entries_pre entries\<rbrace>,-"
  apply (cases sz, simp_all add: largePagePTE_offsets_def superSectionPDE_offsets_def)
     defer 2
     apply (wp | simp)+
   apply (simp split:list.split)
   apply (subgoal_tac "lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x78")
    apply (clarsimp simp:upto_enum_def not_less upto_enum_step_def vspace_bits_defs
      page_inv_entries_pre_def Let_def)
    apply (clarsimp simp:upto_enum_step_def upto_enum_def
                     map_eq_Cons_conv upt_eq_Cons_conv)
    apply (drule_tac x = "lookup_pd_slot pd vptr" in spec)
    apply (subst (asm) upto_0_to_n2)
     apply simp
    apply clarsimp
    apply (drule lookup_pd_slot_aligned_6)
     apply (simp add: vspace_bits_defs)
    apply simp
   apply clarsimp
   apply (erule is_aligned_no_wrap'[OF lookup_pd_slot_aligned_6])
    apply (simp add: vspace_bits_defs)
   apply simp
  apply (wp get_pde_wp | simp add:lookup_pt_slot_def | wpc)+
  apply (clarsimp simp:upto_enum_def upto_enum_step_def
    page_inv_entries_pre_def Let_def )
  apply (drule_tac ref = refa in valid_vspace_objsD)
    apply (simp add:obj_at_def)
   apply simp
  apply (simp add: vspace_bits_defs)
  apply (drule_tac x = "ucast (lookup_pd_slot pd vptr && mask pd_bits >> 3)"
    in spec)
  apply (simp add: vspace_bits_defs)
  apply (clarsimp simp:not_less[symmetric] split:list.splits)
  apply (clarsimp simp:page_inv_entries_pre_def
    Let_def upto_enum_step_def upto_enum_def)
  apply (subst (asm) upto_0_to_n2)
   apply simp
  apply (clarsimp simp:not_less[symmetric])
  apply (subgoal_tac
    "(\<exists>xa xb. pda (ucast (lookup_pd_slot pd vptr && mask pd_bits >> 3))
     = pde.PageTablePDE x)
     \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0x1FF << 3)) 7")
   apply (clarsimp simp: vspace_bits_defs)
   apply (rule_tac x="ptrFromPAddr x + ((vptr >> 12) && 0x1FF << 3)" in exI)
   apply (subst map_upt_append[where x=15 and y=16]; simp add: mask_def del: upt_rec_numeral)
   apply (subst upt_rec_numeral)
   apply (simp add: mask_def del: upt_rec_numeral)
  apply clarsimp
  apply (rule aligned_add_aligned)
    apply (erule(1) pt_aligned)
   apply (rule is_aligned_shiftl[OF is_aligned_andI1])
   apply (rule is_aligned_shiftr)
   apply (simp add:vmsz_aligned_def)
  apply simp
  done

lemma decode_mmu_invocation_valid_pdpt[wp]:
  "\<lbrace>invs and valid_cap (cap.ArchObjectCap cap) and valid_pdpt_objs \<rbrace>
     decode_mmu_invocation label args cap_index slot cap excaps
   \<lbrace>invocation_duplicates_valid o Invocations_A.InvokeArchObject\<rbrace>, -"
  proof -
    have bitwise:"\<And>a. (ucast (((a::word32) && ~~ mask 7) && mask 14 >> 3)::11 word)
      = (ucast (a  && mask 14 >> 3)::11 word) && ~~ mask 4"
      apply (simp add:mask_def)
      apply word_bitwise
      done
    have sz:
      "\<And>vmpage_size. \<lbrakk>args ! 0 + 2 ^ pageBitsForSize vmpage_size - 1 < kernel_base;
        vmsz_aligned (args ! 0) vmpage_size\<rbrakk>
       \<Longrightarrow> args ! 0 < kernel_base"
      apply (rule le_less_trans[OF is_aligned_no_overflow])
       apply (simp add:vmsz_aligned_def)
      apply simp
      done
  show ?thesis
    supply if_split[split del]
    apply (simp add: decode_mmu_invocation_def)
    \<comment> \<open>Handle the easy cases first (trivial because of the post-condition invocation_duplicates_valid)\<close>
    apply (cases "invocation_type label \<notin> {ArchInvocationLabel ARMPageTableMap,
                                           ArchInvocationLabel ARMPageMap}")
     apply (wpsimp simp: invocation_duplicates_valid_def page_inv_duplicates_valid_def
                         pti_duplicates_valid_def Let_def
                   cong: if_cong)
    \<comment> \<open>Handle the two interesting cases now\<close>
    apply (clarsimp; erule disjE; cases cap;
           simp add: isPDFlushLabel_def isPageFlushLabel_def throwError_R')
       \<comment> \<open>PageTableMap\<close>
       apply (wpsimp simp: Let_def get_master_pde_def
                       wp: get_pde_wp hoare_drop_imps hoare_vcg_if_lift_ER)
       apply (fastforce simp: invocation_duplicates_valid_def pti_duplicates_valid_def
                              mask_lower_twice bitwise obj_at_def vspace_bits_defs if_apply_def2
                      split: if_splits)
      apply wp
     \<comment> \<open>PageMap\<close>
     apply (rename_tac dev pg_ptr rights sz pg_map)
     apply (wpsimp simp: Let_def invocation_duplicates_valid_def page_inv_duplicates_valid_def
                     wp: ensure_safe_mapping_ensures[THEN hoare_post_imp_R]
                         check_vp_wpR hoare_vcg_if_lift_ER find_pd_for_asid_lookup_pd_wp)
     apply (fastforce simp: invs_psp_aligned page_directory_at_aligned_pd_bits word_not_le sz
                            valid_cap_def valid_arch_cap_def lookup_pd_slot_eq
                     split: if_splits)
    apply wp
    done
qed

lemma returnOk_lift :
  assumes P': "\<forall>s. P rv s"
  shows "\<lbrace>Q\<rbrace> (doE y \<leftarrow> f ; returnOk rv odE) \<lbrace>P\<rbrace>, -"
  by (wp,auto simp: returnOk_def return_def validE_R_def validE_def valid_def P')

lemma decode_vcpu_invocation_valid_pdpt[wp]:
  "\<lbrace>Q\<rbrace>
     decode_vcpu_invocation label args vcap excaps
   \<lbrace>invocation_duplicates_valid o Invocations_A.InvokeArchObject\<rbrace>, -"
  apply (simp add: decode_vcpu_invocation_def)
  apply (wpsimp simp: decode_vcpu_set_tcb_def
                      decode_vcpu_inject_irq_def decode_vcpu_read_register_def
                      decode_vcpu_write_register_def decode_vcpu_ack_vppi_def
                      if_apply_def2
    | simp add: invocation_duplicates_valid_def)+
  done

lemma arch_decode_invocation_valid_pdpt[wp]:
  notes find_pd_for_asid_inv[wp del]
  shows
  "\<lbrace>invs and valid_cap (cap.ArchObjectCap cap) and valid_pdpt_objs \<rbrace>
   arch_decode_invocation label args cap_index slot cap excaps
   \<lbrace>invocation_duplicates_valid o Invocations_A.InvokeArchObject\<rbrace>,-"
  proof -
  show ?thesis
    apply (simp add: arch_decode_invocation_def)
    apply (rule hoare_pre)
     apply (wp | wpc)+
    apply auto
    done
qed

lemma decode_invocation_valid_pdpt[wp]:
  "\<lbrace>invs and valid_cap cap and valid_pdpt_objs\<rbrace>
     decode_invocation label args cap_index slot cap excaps
   \<lbrace>invocation_duplicates_valid\<rbrace>,-"
  apply (simp add: decode_invocation_def split del: if_split)
  apply (rule hoare_pre)
   apply (wp | wpc
            | simp only: invocation_duplicates_valid_def o_def uncurry_def split_def
                         Invocations_A.invocation.simps)+
  apply clarsimp
  done

crunch valid_pdpt_objs[wp]: handle_fault, reply_from_kernel "valid_pdpt_objs"
  (simp: crunch_simps wp: crunch_wps)

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

lemma set_thread_state_duplicates_valid[wp]:
  "\<lbrace>invocation_duplicates_valid i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. invocation_duplicates_valid i\<rbrace>"
  apply (simp add: set_thread_state_def set_object_def get_object_def)
  apply (wp|simp)+
  apply (clarsimp simp: invocation_duplicates_valid_def pti_duplicates_valid_def
                        page_inv_duplicates_valid_def page_inv_entries_safe_def
                        Let_def
                 dest!: get_tcb_SomeD
                 split: Invocations_A.invocation.split arch_invocation.split_asm
                        page_table_invocation.split
                        page_invocation.split sum.split
                        )
  apply (auto simp add: obj_at_def page_inv_entries_safe_def)
  done

lemma handle_invocation_valid_pdpt[wp]:
  "\<lbrace>valid_pdpt_objs and invs and ct_active\<rbrace>
        handle_invocation calling blocking \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
  unfolding handle_invocation_def
  (* take long: *)
  by (wp syscall_valid set_thread_state_ct_st
               | simp add: split_def | wpc
               | wp (once) hoare_drop_imps)+
     (auto simp: ct_in_state_def elim: st_tcb_ex_cap)

crunch valid_pdpt[wp]: handle_event, activate_thread,switch_to_thread,
       switch_to_idle_thread "valid_pdpt_objs"
  (simp: crunch_simps wp: crunch_wps alternative_wp select_wp OR_choice_weak_wp select_ext_weak_wp
      ignore: without_preemption getActiveIRQ resetTimer ackInterrupt
              getFAR getDFSR getIFSR OR_choice set_scheduler_action
              clearExMonitor)

lemma schedule_valid_pdpt[wp]: "\<lbrace>valid_pdpt_objs\<rbrace> schedule :: (unit,unit) s_monad \<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>"
  apply (simp add: schedule_def allActiveTCBs_def)
  apply (wp alternative_wp select_wp)
  apply simp
  done

lemma call_kernel_valid_pdpt[wp]:
  "\<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s) and valid_pdpt_objs\<rbrace>
      (call_kernel e) :: (unit,unit) s_monad
   \<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>"
  apply (cases e, simp_all add: call_kernel_def)
      apply (rule hoare_pre)
       apply (wp | simp | wpc
                 | rule conjI | clarsimp simp: ct_in_state_def
                 | erule pred_tcb_weakenE
                 | wp (once) hoare_drop_imps)+
  done

end

end


text:
(*
Copyright 2018

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
theory spinlock_irqsave_lock_mem
  imports spinlock
begin

text \<open>Up to two locales per function in the binary.\<close>
locale spinlock_irqsave_lock_function = spinlock_context +
  fixes rsp\<^sub>0 rbp\<^sub>0 current_task tid a spinlock_irqsave_lock_ret :: \<open>64 word\<close>
    and v\<^sub>0 :: \<open>8 word\<close>
    and blocks :: \<open>(nat \<times> 64 word \<times> nat) set\<close>
  assumes seps: \<open>seps blocks\<close>
    and current_task: \<open>the (label_to_address assembly ''current_task'') = current_task\<close>
    and masters:
      \<open>master blocks (a, 1) 0\<close>
      \<open>master blocks (rsp\<^sub>0, 8) 1\<close>
      \<open>master blocks (rsp\<^sub>0-8, 8) 2\<close>
      \<open>master blocks (rsp\<^sub>0-16, 8) 3\<close>
      \<open>master blocks (rsp\<^sub>0-24, 8) 4\<close>
      \<open>master blocks (rsp\<^sub>0-25, Suc 0) 5\<close>
      \<open>master blocks (rsp\<^sub>0-48, 8) 6\<close>
      \<open>master blocks (current_task, 8) 7\<close>
      \<open>master blocks (tid, 4) 8\<close>
    and ret_address: \<open>outside spinlock_irqsave_lock_ret 743 925\<close> \<comment> \<open>Only works for non-recursive functions.\<close>
begin

text \<open>
  The Floyd invariant expresses for some locations properties that are invariably true.
  Simply expresses that a byte in the memory remains untouched.
\<close>
definition pp_\<Theta> :: \<open>_ \<Rightarrow> floyd_invar\<close> where
  \<open>pp_\<Theta> s \<equiv> [
    \<comment> \<open>precondition\<close>
    boffset+743 \<mapsto> \<lambda>\<sigma>. regs \<sigma> rsp = rsp\<^sub>0
      \<and> regs \<sigma> rbp = rbp\<^sub>0
      \<and> regs \<sigma> rdi = s
      \<and> \<sigma> \<turnstile> *[current_task,8] = tid
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0,8] = boffset+spinlock_irqsave_lock_ret
      \<and> \<sigma> \<turnstile> *[a,1] = v\<^sub>0,
    boffset+781 \<mapsto> \<lambda>\<sigma>. regs \<sigma> rsp = rsp\<^sub>0-56
      \<and> regs \<sigma> rbp = rsp\<^sub>0-8
      \<and> \<sigma> \<turnstile> *[current_task,8] = tid
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-48,8] = s
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-8,8] = rbp\<^sub>0
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0,8] = boffset+spinlock_irqsave_lock_ret
      \<and> \<sigma> \<turnstile> *[a,1] = v\<^sub>0,
    boffset+786 \<mapsto> \<lambda>\<sigma>. regs \<sigma> rsp = rsp\<^sub>0-56
      \<and> regs \<sigma> rbp = rsp\<^sub>0-8
      \<and> \<sigma> \<turnstile> *[current_task,8] = tid
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-48,8] = s
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-8,8] = rbp\<^sub>0
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0,8] = boffset+spinlock_irqsave_lock_ret
      \<and> \<sigma> \<turnstile> *[a,1] = v\<^sub>0,
    boffset+848 \<mapsto> \<lambda>\<sigma>. regs \<sigma> rsp = rsp\<^sub>0-56
      \<and> regs \<sigma> rbp = rsp\<^sub>0-8
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-48,8] = s
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-8,8] = rbp\<^sub>0
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0,8] = boffset+spinlock_irqsave_lock_ret
      \<and> \<sigma> \<turnstile> *[a,1] = v\<^sub>0,
    boffset+853 \<mapsto> \<lambda>\<sigma>. regs \<sigma> rsp = rsp\<^sub>0-56
      \<and> regs \<sigma> rbp = rsp\<^sub>0-8
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-48,8] = s
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-8,8] = rbp\<^sub>0
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0,8] = boffset+spinlock_irqsave_lock_ret
      \<and> \<sigma> \<turnstile> *[a,1] = v\<^sub>0,
    boffset+872 \<mapsto> \<lambda>\<sigma>. regs \<sigma> rsp = rsp\<^sub>0-56
      \<and> regs \<sigma> rbp = rsp\<^sub>0-8
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-48,8] = s
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-8,8] = rbp\<^sub>0
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0,8] = boffset+spinlock_irqsave_lock_ret
      \<and> \<sigma> \<turnstile> *[a,1] = v\<^sub>0,
    boffset+877 \<mapsto> \<lambda>\<sigma>. regs \<sigma> rsp = rsp\<^sub>0-56
      \<and> regs \<sigma> rbp = rsp\<^sub>0-8
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-48,8] = s
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-8,8] = rbp\<^sub>0
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0,8] = boffset+spinlock_irqsave_lock_ret
      \<and> \<sigma> \<turnstile> *[a,1] = v\<^sub>0,
    boffset+923 \<mapsto> \<lambda>\<sigma>. regs \<sigma> rsp = rsp\<^sub>0-56
      \<and> regs \<sigma> rbp = rsp\<^sub>0-8
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-8,8] = rbp\<^sub>0
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0,8] = boffset+spinlock_irqsave_lock_ret
      \<and> \<sigma> \<turnstile> *[a,1] = v\<^sub>0,
    \<comment> \<open>postcondition\<close>
    boffset+spinlock_irqsave_lock_ret \<mapsto> \<lambda>\<sigma>. \<sigma> \<turnstile> *[a,1] = v\<^sub>0
      \<and> regs \<sigma> rsp = rsp\<^sub>0+8
      \<and> regs \<sigma> rbp = rbp\<^sub>0
  ]\<close>

text \<open>Adding some rules to the simplifier to simplify proofs.\<close>
schematic_goal pp_\<Theta>_zero[simp]:
  \<open>pp_\<Theta> s boffset = ?x\<close>
  unfolding pp_\<Theta>_def
  by simp
schematic_goal pp_\<Theta>_numeral_l[simp]:
  \<open>pp_\<Theta> s (n + boffset) = ?x\<close>
  unfolding pp_\<Theta>_def
  by simp
schematic_goal pp_\<Theta>_numeral_r[simp]:
  \<open>pp_\<Theta> s (boffset + n) = ?x\<close>
  unfolding pp_\<Theta>_def
  by simp

end

locale spinlock_irqsave_lock_function_calls = spinlock_irqsave_lock_function +
  fixes irq_nested_disable atomic_int64_read atomic_int64_inc :: \<open>state \<Rightarrow> state\<close>
  assumes irq_nested_disable_def: \<open>exec_instr assembly semantics tasks_flag_annotation (Unary (IS_8088 Call) (Immediate (ImmLabel ''irq_nested_disable''))) 5 = irq_nested_disable\<close>
    and irq_nested_disable_incr: \<open>regs (irq_nested_disable \<sigma>) rip = regs \<sigma> rip + 5\<close>
    and irq_nested_disable781: \<open>the (pp_\<Theta> s (boffset+781)) \<sigma> \<Longrightarrow> the (pp_\<Theta> s (boffset+786)) (irq_nested_disable \<sigma>)\<close>
    and atomic_int64_read_def: \<open>exec_instr assembly semantics tasks_flag_annotation (Unary (IS_8088 Call) (Immediate (ImmLabel ''atomic_int64_read''))) 5 = atomic_int64_read\<close>
    and atomic_int64_read_incr: \<open>regs (atomic_int64_read \<sigma>) rip = regs \<sigma> rip + 5\<close>
    and atomic_int64_read872: \<open>the (pp_\<Theta> s (boffset+872)) \<sigma> \<Longrightarrow> the (pp_\<Theta> s (boffset+877)) (atomic_int64_read \<sigma>)\<close>
    and atomic_int64_inc_def: \<open>exec_instr assembly semantics tasks_flag_annotation (Unary (IS_8088 Call) (Immediate (ImmLabel ''atomic_int64_inc''))) 5 = atomic_int64_inc\<close>
    and atomic_int64_inc_incr: \<open>regs (atomic_int64_inc \<sigma>) rip = regs \<sigma> rip + 5\<close>
    and atomic_int64_inc848: \<open>the (pp_\<Theta> s (boffset+848)) \<sigma> \<Longrightarrow> the (pp_\<Theta> s (boffset+853)) (atomic_int64_inc \<sigma>)\<close>
begin

lemma rewrite_spinlock_irqsave_lock_mem:
  assumes
    \<open>master blocks (s + 16, 4) 9\<close>
    \<open>master blocks (s + 20, 4) 10\<close>
    \<open>master blocks (s + 24, Suc 0) 11\<close>
  shows \<open>is_std_invar spinlock_irqsave_lock_ret (floyd.invar spinlock_irqsave_lock_ret (pp_\<Theta> s))\<close>
proof -
  note masters = masters assms

  show ?thesis
    text \<open>Boilerplate code to start the VCG\<close>
    apply (rule floyd_invarI)
    apply (rewrite at \<open>floyd_vcs spinlock_irqsave_lock_ret \<hole> _\<close> pp_\<Theta>_def)
    apply (intro floyd_vcsI)

    text \<open>Subgoal for rip = boffset+743\<close>
    subgoal premises prems for \<sigma>
      text \<open>Insert relevant knowledge\<close>
      apply (insert prems seps ret_address current_task)
      text \<open>Apply VCG/symb.\ execution\<close>
      apply (restart_symbolic_execution?, (symbolic_execution masters: masters)+, (finish_symbolic_execution masters: masters)?)+
      done

    text \<open>Subgoal for rip = boffset+781\<close>
    subgoal premises prems for \<sigma>
      text \<open>Insert relevant knowledge\<close>
      apply (insert prems seps ret_address current_task)
      text \<open>Discharge function call\<close>
      apply (rule wps_rls)
      apply (simp (no_asm_simp) add: lookup_table_def instr_index_def entry_size_def)
      apply (rewrite_one_let' add: assembly_def)
      apply (rewrite_one_let' add: irq_nested_disable_def)
      apply (rule floyd_invarI'[of _ _ \<open>the (pp_\<Theta> s (boffset+786))\<close>])
       apply (simp add: irq_nested_disable_incr)
      using irq_nested_disable781
      apply simp
      done

    text \<open>Subgoal for rip = boffset+786\<close>
    subgoal premises prems for \<sigma>
    proof -
      have x: \<open>regs \<sigma> rbp = rsp\<^sub>0 - 8\<close>
        using prems
        by simp
      show ?thesis
        text \<open>Insert relevant knowledge\<close>
        apply (insert prems seps ret_address current_task)
        text \<open>Apply VCG/symb.\ execution\<close>
        apply ((restart_symbolic_execution add: x)?, (symbolic_execution add: x masters: masters)+, (finish_symbolic_execution add: x masters: masters)?)+
        done
    qed

    text \<open>Subgoal for rip = boffset+848\<close>
    subgoal premises prems for \<sigma>
      text \<open>Insert relevant knowledge\<close>
      apply (insert prems seps ret_address current_task)
      text \<open>Discharge function call\<close>
      apply (rule wps_rls)
      apply (simp (no_asm_simp) add: lookup_table_def instr_index_def entry_size_def)
      apply (rewrite_one_let' add: assembly_def)
      apply (rewrite_one_let' add: atomic_int64_inc_def)
      apply (rule floyd_invarI'[of _ _ \<open>the (pp_\<Theta> s (boffset+853))\<close>])
       apply (simp add: atomic_int64_inc_incr)
      using atomic_int64_inc848
      apply simp
      done

    text \<open>Subgoal for rip = boffset+853\<close>
    subgoal premises prems for \<sigma>
      text \<open>Insert relevant knowledge\<close>
      apply (insert prems seps ret_address current_task)
      text \<open>Apply VCG/symb.\ execution\<close>
      apply (restart_symbolic_execution?, (symbolic_execution masters: masters)+, (finish_symbolic_execution masters: masters)?)+
      done

    text \<open>Subgoal for rip = boffset+872\<close>
    subgoal premises prems for \<sigma>
      text \<open>Insert relevant knowledge\<close>
      apply (insert prems seps ret_address current_task)
      text \<open>Discharge function call\<close>
      apply (rule wps_rls)
      apply (simp (no_asm_simp) add: lookup_table_def instr_index_def entry_size_def)
      apply (rewrite_one_let' add: assembly_def)
      apply (rewrite_one_let' add: atomic_int64_read_def)
      apply (rule floyd_invarI'[of _ _ \<open>the (pp_\<Theta> s (boffset+877))\<close>])
       apply (simp add: atomic_int64_read_incr)
      using atomic_int64_read872
      apply simp
      done

    text \<open>Subgoal for rip = boffset+877\<close>
    subgoal premises prems for \<sigma>
    proof -
      have x: \<open>regs \<sigma> rbp = rsp\<^sub>0 - 8\<close>
        using prems
        by simp
      show ?thesis
        text \<open>Insert relevant knowledge\<close>
        apply (insert prems seps ret_address current_task)
        text \<open>Apply VCG/symb.\ execution\<close>
        apply ((restart_symbolic_execution add: x)?, (symbolic_execution add: x masters: masters)+, (finish_symbolic_execution add: x masters: masters)?)+
        done
    qed

    text \<open>Subgoal for rip = boffset+923\<close>
    subgoal premises prems for \<sigma>
      text \<open>Insert relevant knowledge\<close>
      apply (insert prems seps ret_address current_task)
      text \<open>Apply VCG/symb.\ execution\<close>
      apply (restart_symbolic_execution?, (symbolic_execution masters: masters)+, (finish_symbolic_execution masters: masters)?)+
      done

    text \<open>Trivial ending subgoal.\<close>
    subgoal
      by simp
    done
qed

end

end

author: ssrg-vt

repo: Luce-src

save_path: github-repos/isabelle/ssrg-vt-Luce-src


text:
(*  Title:   Tools/Code_Generator.thy
    Author:  Florian Haftmann, TU Muenchen
*)

section {* Loading the code generator and related modules *}

theory Code_Generator
imports Pure
keywords
  "print_codeproc" "code_thms" "code_deps" :: diag and
  "export_code" "code_identifier" "code_printing" "code_reserved"
    "code_monad" "code_reflect" :: thy_decl and
  "datatypes" "functions" "module_name" "file" "checking"
  "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
begin

ML_file "~~/src/Tools/cache_io.ML"
ML_file "~~/src/Tools/Code/code_preproc.ML"

attribute_setup code_preproc_trace = {*
  (Scan.lift (Args.$$$ "off" >> K Code_Preproc.trace_none)
  || (Scan.lift (Args.$$$ "only" |-- Args.colon |-- Scan.repeat1 Parse.term))
       >> Code_Preproc.trace_only_ext
  || Scan.succeed Code_Preproc.trace_all)
  >> (Thm.declaration_attribute o K)
*} "tracing of the code generator preprocessor"

ML_file "~~/src/Tools/Code/code_symbol.ML"
ML_file "~~/src/Tools/Code/code_thingol.ML"
ML_file "~~/src/Tools/Code/code_simp.ML"
ML_file "~~/src/Tools/Code/code_printer.ML"
ML_file "~~/src/Tools/Code/code_target.ML"
ML_file "~~/src/Tools/Code/code_namespace.ML"
ML_file "~~/src/Tools/Code/code_ml.ML"
ML_file "~~/src/Tools/Code/code_haskell.ML"
ML_file "~~/src/Tools/Code/code_scala.ML"

setup {*
  Code_Simp.setup
  #> Code_Target.setup
  #> Code_ML.setup
  #> Code_Haskell.setup
  #> Code_Scala.setup
*}

code_datatype "TYPE('a\<Colon>{})"

definition holds :: "prop" where
  "holds \<equiv> ((\<lambda>x::prop. x) \<equiv> (\<lambda>x. x))"

lemma holds: "PROP holds"
  by (unfold holds_def) (rule reflexive)

code_datatype holds

lemma implies_code [code]:
  "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
  "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
proof -
  show "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
  proof
    assume "PROP holds \<Longrightarrow> PROP P"
    then show "PROP P" using holds .
  next
    assume "PROP P"
    then show "PROP P" .
  qed
next
  show "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
    by rule (rule holds)+
qed

ML_file "~~/src/Tools/Code/code_runtime.ML"
ML_file "~~/src/Tools/nbe.ML"

hide_const (open) holds

end

author: Josh-Tilles

repo: isabelle


text:
(*  Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de
    License:     LGPL
*)

(*  Title:      Heap.thy
    Author:     Norbert Schirmer, TU Muenchen

Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen

This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.

This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)

theory Simpl_Heap
imports Main
begin

subsection "References"

definition "ref = (UNIV::nat set)"

typedef ref = ref by (simp add: ref_def)

code_datatype Abs_ref

lemma finite_nat_ex_max:
  assumes fin: "finite (N::nat set)"
  shows "\<exists>m. \<forall>n\<in>N. n < m"
using fin
proof (induct)
  case empty
  show ?case by auto
next
  case (insert k N)
  have "\<exists>m. \<forall>n\<in>N. n < m" by fact
  then obtain m where m_max: "\<forall>n\<in>N. n < m"..
  show "\<exists>m. \<forall>n\<in>insert k N. n < m"
  proof (rule exI [where x="Suc (max k m)"])
  qed (insert m_max, auto simp add: max_def)
qed

lemma infinite_nat: "\<not>finite (UNIV::nat set)"
proof
  assume fin: "finite (UNIV::nat set)"
  then obtain m::nat where "\<forall>n\<in>UNIV. n < m"
    by (rule finite_nat_ex_max [elim_format] ) auto
  moreover have "m\<in>UNIV"..
  ultimately show False by blast
qed

lemma infinite_ref [simp,intro]: "\<not>finite (UNIV::ref set)"
proof
  assume "finite (UNIV::ref set)"
  hence "finite (range Rep_ref)"
    by simp
  moreover
  have "range Rep_ref = ref"
  proof
    show "range Rep_ref \<subseteq> ref"
      by (simp add: ref_def)
  next
    show "ref \<subseteq> range Rep_ref"
    proof
      fix x
      assume x: "x \<in> ref"
      show "x \<in> range Rep_ref"
        by (rule Rep_ref_induct) (auto simp add: ref_def)
    qed
  qed
  ultimately have "finite ref"
    by simp
  thus False
    by (simp add: ref_def infinite_nat)
qed

consts Null :: ref

definition new :: "ref set \<Rightarrow> ref" where
  "new A = (SOME a. a \<notin> {Null} \<union> A)"

text \<open>
  Constant @{const "Null"} can be defined later on.  Conceptually
  @{const "Null"} and @{const "new"} are \<open>fixes\<close> of a locale
  with @{prop "finite A \<Longrightarrow> new A \<notin> A \<union> {Null}"}.  But since definitions
  relative to a locale do not yet work in Isabelle2005 we use this
  workaround to avoid lots of parameters in definitions.
\<close>

lemma new_notin [simp,intro]:
 "finite A \<Longrightarrow> new (A) \<notin> A"
  apply (unfold new_def)
  apply (rule someI2_ex)
  apply (fastforce intro: ex_new_if_finite)
  apply simp
  done

lemma new_not_Null [simp,intro]:
  "finite A \<Longrightarrow> new (A) \<noteq> Null"
  apply (unfold new_def)
  apply (rule someI2_ex)
  apply (fastforce intro: ex_new_if_finite)
  apply simp
done

end

author: LVPGroup

repo: TimSort

save_path: github-repos/isabelle/LVPGroup-TimSort