kings-crown/FVELER_Isabelle huggingface dataset:
theory Finalise_DR

lemma opt_object_asid_pool:
  "\<lbrakk> valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.ASIDPool fun)) \<rbrakk> \<Longrightarrow>
     cdl_objects (transform s) a = Some (cdl_object.AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents fun\<rparr>)" apply (frule asid_pool_at_rev) apply (frule(1) asid_pool_not_idle) apply (clarsimp simp: transform_objects_def transform_def not_idle_thread_def restrict_map_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s a = Some (ArchObj (ASIDPool fun))\<rbrakk> \<Longrightarrow> cdl_objects (transform s) a = Some (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents fun\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s a = Some (ArchObj (ASIDPool fun)); typ_at (AArch AASIDPool) a s\<rbrakk> \<Longrightarrow> cdl_objects (transform s) a = Some (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents fun\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s a = Some (ArchObj (ASIDPool fun)); typ_at (AArch AASIDPool) a s; not_idle_thread a s\<rbrakk> \<Longrightarrow> cdl_objects (transform s) a = Some (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents fun\<rparr>) proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma page_table_aligned:
  "\<lbrakk>pspace_aligned s;page_table_at oid s\<rbrakk> \<Longrightarrow>
         (oid && ~~ mask pt_bits) = oid" apply (clarsimp simp:pspace_aligned_def obj_at_def a_type_def) apply (clarsimp split:arch_kernel_obj.split_asm Structures_A.kernel_object.split_asm if_splits) apply (drule_tac x = oid in bspec) apply clarsimp apply (clarsimp simp:obj_bits_def arch_kobj_size_def pt_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned s; typ_at (AArch APageTable) oid s\<rbrakk> \<Longrightarrow> oid && ~~ mask pt_bits = oid proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>\<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); kheap s oid = Some ko; (case ko of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageTable\<rbrakk> \<Longrightarrow> oid && ~~ mask pt_bits = oid proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>\<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); kheap s oid = Some (ArchObj (arch_kernel_obj.PageTable x2))\<rbrakk> \<Longrightarrow> oid && ~~ mask pt_bits = oid proof (prove)
goal (2 subgoals):
 1. \<And>x2. kheap s oid = Some (ArchObj (arch_kernel_obj.PageTable x2)) \<Longrightarrow> oid \<in> dom (kheap s)
 2. \<And>x2. \<lbrakk>kheap s oid = Some (ArchObj (arch_kernel_obj.PageTable x2)); is_aligned oid (obj_bits (the (kheap s oid)))\<rbrakk> \<Longrightarrow> oid && ~~ mask pt_bits = oid proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>kheap s oid = Some (ArchObj (arch_kernel_obj.PageTable x2)); is_aligned oid (obj_bits (the (kheap s oid)))\<rbrakk> \<Longrightarrow> oid && ~~ mask pt_bits = oid proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma invalidateLocalTLB_VAASID_underlying_memory[wp]:
  "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateLocalTLB_VAASID word \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" by (clarsimp simp: invalidateLocalTLB_VAASID_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateLocalTLB_VAASID word \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
theory Finalise_DR

lemma flush_table_exec:
  "\<lbrakk>dcorres dc R (Q rv) h (g rv); \<lbrace>P\<rbrace> flush_table aa a b word \<lbrace>Q\<rbrace>\<rbrakk>\<Longrightarrow>dcorres dc R P h ((flush_table aa a b word) >>= g)" apply (rule corres_dummy_return_pl) apply (rule corres_guard_imp) apply (rule corres_split[OF dcorres_flush_table]) apply (simp|wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dcorres dc R (Q rv) h (g rv); \<lbrace>P\<rbrace> flush_table aa a b word \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> dcorres dc R P h (flush_table aa a b word >>= g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dcorres dc R (Q rv) h (g rv); \<lbrace>P\<rbrace> flush_table aa a b word \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> dcorres dc R P (do return ?b;
h
od) (flush_table aa a b word >>= g) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>dcorres dc R (Q rv) h (g rv); \<lbrace>P\<rbrace> flush_table aa a b word \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> dcorres dc ?Q2 ?Q'2 (do return ?b;
h
od) (flush_table aa a b word >>= g)
 2. \<And>s. \<lbrakk>dcorres dc R (Q rv) h (g rv); \<lbrace>P\<rbrace> flush_table aa a b word \<lbrace>Q\<rbrace>; R s\<rbrakk> \<Longrightarrow> ?Q2 s
 3. \<And>s. \<lbrakk>dcorres dc R (Q rv) h (g rv); \<lbrace>P\<rbrace> flush_table aa a b word \<lbrace>Q\<rbrace>; P s\<rbrakk> \<Longrightarrow> ?Q'2 s proof (prove)
goal (5 subgoals):
 1. \<And>rva rv'. \<lbrakk>dcorres dc R (Q rv) h (g rv); \<lbrace>P\<rbrace> flush_table aa a b word \<lbrace>Q\<rbrace>; dc rva rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R6 rva) (?R'6 rv') (K_bind h rva) (g rv')
 2. \<lbrakk>dcorres dc R (Q rv) h (g rv); \<lbrace>P\<rbrace> flush_table aa a b word \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> return ?b \<lbrace>?R6\<rbrace>
 3. \<lbrakk>dcorres dc R (Q rv) h (g rv); \<lbrace>P\<rbrace> flush_table aa a b word \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6\<rbrace> flush_table aa a b word \<lbrace>?R'6\<rbrace>
 4. \<And>s. \<lbrakk>dcorres dc R (Q rv) h (g rv); \<lbrace>P\<rbrace> flush_table aa a b word \<lbrace>Q\<rbrace>; R s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. \<lbrakk>dcorres dc R (Q rv) h (g rv); \<lbrace>P\<rbrace> flush_table aa a b word \<lbrace>Q\<rbrace>; P s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma transform_cap_not_new_invented:
  "transform_cap z \<noteq> cdl_cap.PageTableCap word Fake asid" by (auto simp:transform_cap_def split:arch_cap.splits cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_cap z \<noteq> cdl_cap.PageTableCap word Fake asid
theory Finalise_DR

lemma page_table_not_idle:
  "\<lbrakk>valid_idle s;page_table_at a s\<rbrakk> \<Longrightarrow> not_idle_thread a s" apply (clarsimp simp:obj_at_def valid_idle_def pred_tcb_at_def) apply (clarsimp simp: not_idle_thread_def split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; typ_at (AArch APageTable) a s\<rbrakk> \<Longrightarrow> not_idle_thread a s proof (prove)
goal (1 subgoal):
 1. \<And>pt tcb. \<lbrakk>idle_thread s = idle_thread_ptr; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable pt)); kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb)\<rbrakk> \<Longrightarrow> not_idle_thread a s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma page_directory_not_idle:
  "\<lbrakk>valid_idle s;page_directory_at a s\<rbrakk> \<Longrightarrow> not_idle_thread a s" apply (clarsimp simp:obj_at_def valid_idle_def pred_tcb_at_def) apply (clarsimp simp: not_idle_thread_def split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; typ_at (AArch APageDirectory) a s\<rbrakk> \<Longrightarrow> not_idle_thread a s proof (prove)
goal (1 subgoal):
 1. \<And>pd tcb. \<lbrakk>idle_thread s = idle_thread_ptr; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb)\<rbrakk> \<Longrightarrow> not_idle_thread a s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma page_table_at_rev:
  "\<lbrakk>kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun))\<rbrakk> \<Longrightarrow> page_table_at a s" apply (clarsimp simp:obj_at_def valid_idle_def pred_tcb_at_def) apply (clarsimp simp:a_type_def split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun)) \<Longrightarrow> typ_at (AArch APageTable) a s proof (prove)
goal (1 subgoal):
 1. kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun)) \<Longrightarrow> a_type (ArchObj (arch_kernel_obj.PageTable fun)) = AArch APageTable proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma page_directory_at_rev:
  "\<lbrakk>kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun))\<rbrakk> \<Longrightarrow> page_directory_at a s" apply (clarsimp simp:obj_at_def valid_idle_def st_tcb_at_def) apply (clarsimp simp:a_type_def split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)) \<Longrightarrow> typ_at (AArch APageDirectory) a s proof (prove)
goal (1 subgoal):
 1. kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)) \<Longrightarrow> a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = AArch APageDirectory proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma mask_pd_bits_less':
  "uint ((ptr::word32) && mask pd_bits >> (2::nat)) < (4096::int)" apply (clarsimp simp:pd_bits_def pageBits_def) using shiftr_less_t2n'[where m = 12 and x ="(ptr && mask 14)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]] apply (clarsimp simp:mask_twice) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uint (ptr && mask pd_bits >> 2) < 4096 proof (prove)
goal (1 subgoal):
 1. uint (ptr && mask 14 >> 2) < 4096 proof (prove)
using this:
uint (ptr && mask 14 >> 2) < uint 0x1000

goal (1 subgoal):
 1. uint (ptr && mask 14 >> 2) < 4096 proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma mask_pd_bits_less:
  "unat ((y::word32) && mask pd_bits >> 2) < 4096" apply (clarsimp simp:pd_bits_def pageBits_def simp del: nat_uint_eq) apply (unfold unat_def) apply (rule iffD2[OF nat_less_eq_zless[where z = 4096,simplified]]) apply (simp) using shiftr_less_t2n'[where m = 12 and x ="(y && mask 14)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]] apply (clarsimp simp:mask_twice) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (y && mask pd_bits >> 2) < 4096 proof (prove)
goal (1 subgoal):
 1. unat (y && mask 14 >> 2) < 4096 proof (prove)
goal (1 subgoal):
 1. nat (uint (y && mask 14 >> 2)) < 4096 proof (prove)
goal (2 subgoals):
 1. 0 \<le> uint (y && mask 14 >> 2)
 2. uint (y && mask 14 >> 2) < 4096 proof (prove)
goal (1 subgoal):
 1. uint (y && mask 14 >> 2) < 4096 proof (prove)
using this:
uint (y && mask 14 >> 2) < uint 0x1000

goal (1 subgoal):
 1. uint (y && mask 14 >> 2) < 4096 proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma mask_pt_bits_less:
  "unat ((y::word32) && mask pt_bits >> 2) < 256" apply (clarsimp simp:pt_bits_def pageBits_def) apply (unfold unat_def) apply (rule iffD2[OF nat_less_eq_zless[where z = 256,simplified]]) apply (simp) using shiftr_less_t2n'[where m = 8 and x ="(y && mask 10)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]] apply (clarsimp simp:mask_twice) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (y && mask pt_bits >> 2) < 256 proof (prove)
goal (1 subgoal):
 1. unat (y && mask 10 >> 2) < 256 proof (prove)
goal (1 subgoal):
 1. nat (uint (y && mask 10 >> 2)) < 256 proof (prove)
goal (2 subgoals):
 1. 0 \<le> uint (y && mask 10 >> 2)
 2. uint (y && mask 10 >> 2) < 256 proof (prove)
goal (1 subgoal):
 1. uint (y && mask 10 >> 2) < 256 proof (prove)
using this:
uint (y && mask 10 >> 2) < uint 0x100

goal (1 subgoal):
 1. uint (y && mask 10 >> 2) < 256 proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma below_kernel_base_int:
  "ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots
    \<Longrightarrow> kernel_pde_mask f (of_int (uint (y && mask pd_bits >> 2)))
    = f (of_int (uint (y && mask pd_bits >> 2)))" by (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def )

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST('a \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> kernel_pde_mask f (word_of_int (uint (y && mask pd_bits >> 2))) = f (word_of_int (uint (y && mask pd_bits >> 2)))
theory Finalise_DR

lemma opt_object_page_table:
  "\<lbrakk>valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun))\<rbrakk>
  \<Longrightarrow> cdl_objects (transform s) a =
        Some (cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents fun\<rparr>)" apply (frule page_table_at_rev) apply (frule(1) page_table_not_idle) apply (clarsimp simp: transform_objects_def transform_def not_idle_thread_def restrict_map_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun))\<rbrakk> \<Longrightarrow> cdl_objects (transform s) a = Some (cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents fun\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun)); typ_at (AArch APageTable) a s\<rbrakk> \<Longrightarrow> cdl_objects (transform s) a = Some (cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents fun\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun)); typ_at (AArch APageTable) a s; not_idle_thread a s\<rbrakk> \<Longrightarrow> cdl_objects (transform s) a = Some (cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents fun\<rparr>) proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma opt_object_page_directory:
  "\<lbrakk>valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun))\<rbrakk>
  \<Longrightarrow> cdl_objects (transform s) a =
        Some (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents fun\<rparr>)" apply (frule page_directory_at_rev) apply (frule(1) page_directory_not_idle) apply (clarsimp simp:transform_objects_def transform_def not_idle_thread_def restrict_map_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun))\<rbrakk> \<Longrightarrow> cdl_objects (transform s) a = Some (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents fun\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); typ_at (AArch APageDirectory) a s\<rbrakk> \<Longrightarrow> cdl_objects (transform s) a = Some (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents fun\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); typ_at (AArch APageDirectory) a s; not_idle_thread a s\<rbrakk> \<Longrightarrow> cdl_objects (transform s) a = Some (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents fun\<rparr>) proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma dcorres_lookup_pd_slot:
  "is_aligned pd 14
  \<Longrightarrow> (cdl_lookup_pd_slot pd vptr =  transform_pd_slot_ref (lookup_pd_slot pd vptr))" apply (clarsimp simp:cdl_lookup_pd_slot_def
     transform_pd_slot_ref_def lookup_pd_slot_def) by (simp add:vaddr_segment_nonsense vaddr_segment_nonsense2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd 14 \<Longrightarrow> cdl_lookup_pd_slot pd vptr = transform_pd_slot_ref (lookup_pd_slot pd vptr) proof (prove)
goal (1 subgoal):
 1. is_aligned pd 14 \<Longrightarrow> pd = pd + (vptr >> 20 << 2) && ~~ mask pd_bits \<and> vptr >> 20 = pd + (vptr >> 20 << 2) && mask pd_bits >> 2
theory Finalise_DR

lemma large_frame_range_helper:
  fixes t :: word32
  shows
  "t \<in> set [0 , 4 .e. 0x3C] \<Longrightarrow> t < 0x40" apply (clarsimp simp: upto_enum_step_def) apply (subgoal_tac "x < 0x10") apply (subst mult.commute) apply (subst shiftl_t2n[where n =2,simplified,symmetric]) apply (rule shiftl_less_t2n[where m = 6 and n =2,simplified]) apply simp+ apply (rule le_less_trans) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t \<in> set [0 , 4 .e. 0x3C] \<Longrightarrow> t < 0x40 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>t = x * 4; x \<le> 0xF\<rbrakk> \<Longrightarrow> x * 4 < 0x40 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>t = x * 4; x \<le> 0xF; x < 0x10\<rbrakk> \<Longrightarrow> x * 4 < 0x40
 2. \<And>x. \<lbrakk>t = x * 4; x \<le> 0xF\<rbrakk> \<Longrightarrow> x < 0x10 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>t = x * 4; x \<le> 0xF; x < 0x10\<rbrakk> \<Longrightarrow> 4 * x < 0x40
 2. \<And>x. \<lbrakk>t = x * 4; x \<le> 0xF\<rbrakk> \<Longrightarrow> x < 0x10 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>t = x * 4; x \<le> 0xF; x < 0x10\<rbrakk> \<Longrightarrow> x << 2 < 0x40
 2. \<And>x. \<lbrakk>t = x * 4; x \<le> 0xF\<rbrakk> \<Longrightarrow> x < 0x10 proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>t = x * 4; x \<le> 0xF; x < 0x10\<rbrakk> \<Longrightarrow> x < 0x10
 2. \<And>x. \<lbrakk>t = x * 4; x \<le> 0xF; x < 0x10\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 3. \<And>x. \<lbrakk>t = x * 4; x \<le> 0xF\<rbrakk> \<Longrightarrow> x < 0x10 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>t = x * 4; x \<le> 0xF\<rbrakk> \<Longrightarrow> x < 0x10 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>t = x * 4; x \<le> 0xF\<rbrakk> \<Longrightarrow> x \<le> ?y29 x
 2. \<And>x. \<lbrakk>t = x * 4; x \<le> 0xF\<rbrakk> \<Longrightarrow> ?y29 x < 0x10 proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma shiftl_inj_if:
  "\<lbrakk>(shiftl a n) = (shiftl b n); shiftr (shiftl a n) n = a; shiftr (shiftl b n) n = b\<rbrakk> \<Longrightarrow> a = b" apply (drule arg_cong[where f = "\<lambda>x. shiftr x n"]) apply (rule box_equals) defer apply (assumption)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a << n = b << n; a << n >> n = a; b << n >> n = b\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a << n >> n = a; b << n >> n = b; a << n >> n = b << n >> n\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a << n >> n = a; b << n >> n = b; a << n >> n = b << n >> n\<rbrakk> \<Longrightarrow> ?a2 = ?b2
 2. \<lbrakk>a << n >> n = a; b << n >> n = b; a << n >> n = b << n >> n\<rbrakk> \<Longrightarrow> ?a2 = a
 3. \<lbrakk>a << n >> n = a; b << n >> n = b; a << n >> n = b << n >> n\<rbrakk> \<Longrightarrow> ?b2 = b proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a << n >> n = a; b << n >> n = b; a << n >> n = b << n >> n\<rbrakk> \<Longrightarrow> ?a2 = a
 2. \<lbrakk>a << n >> n = a; b << n >> n = b; a << n >> n = b << n >> n\<rbrakk> \<Longrightarrow> ?b2 = b
 3. \<lbrakk>a << n >> n = a; b << n >> n = b; a << n >> n = b << n >> n\<rbrakk> \<Longrightarrow> ?a2 = ?b2 proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma ucast_inj_mask:
  "(ucast (x::'a::len word) :: 'b::len word) = (ucast (y::'a::len word) :: 'b::len word)
   \<Longrightarrow> x && mask LENGTH('b) = y && mask LENGTH('b)" by (metis ucast_ucast_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST('a \<rightarrow> 'b) x = UCAST('a \<rightarrow> 'b) y \<Longrightarrow> x && mask LENGTH('b) = y && mask LENGTH('b)
theory Finalise_DR

lemma split_word_noteq_on_mask:
  "(x \<noteq> y)  =  (x && mask k \<noteq> y && mask k \<or> x && ~~ mask k \<noteq> y && ~~ mask k)" apply (rule iffI) using split_word_eq_on_mask[symmetric] apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<noteq> y) = (x && mask k \<noteq> y && mask k \<or> x && ~~ mask k \<noteq> y && ~~ mask k) proof (prove)
goal (2 subgoals):
 1. x \<noteq> y \<Longrightarrow> x && mask k \<noteq> y && mask k \<or> x && ~~ mask k \<noteq> y && ~~ mask k
 2. x && mask k \<noteq> y && mask k \<or> x && ~~ mask k \<noteq> y && ~~ mask k \<Longrightarrow> x \<noteq> y proof (prove)
using this:
(?x && ?m = ?y && ?m \<and> ?x && ~~ ?m = ?y && ~~ ?m) = (?x = ?y)

goal (2 subgoals):
 1. x \<noteq> y \<Longrightarrow> x && mask k \<noteq> y && mask k \<or> x && ~~ mask k \<noteq> y && ~~ mask k
 2. x && mask k \<noteq> y && mask k \<or> x && ~~ mask k \<noteq> y && ~~ mask k \<Longrightarrow> x \<noteq> y proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma test_bits_mask:
  "\<lbrakk>x && mask l = y && mask l;na < size x; size x = size y\<rbrakk>
  \<Longrightarrow> na<l \<longrightarrow> x !! na = y !! na" apply (drule word_eqD) apply (auto simp:word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && mask l = y && mask l; na < size x; size x = size y\<rbrakk> \<Longrightarrow> na < l \<longrightarrow> x !! na = y !! na proof (prove)
goal (1 subgoal):
 1. \<lbrakk>na < size x; size x = size y; (x && mask l) !! ?x = (y && mask l) !! ?x\<rbrakk> \<Longrightarrow> na < l \<longrightarrow> x !! na = y !! na proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma aligned_in_step_up_to:
  "\<lbrakk>x\<in> set (map (\<lambda>x. x + ptr) [0 , (2^t) .e. up]); t < word_bits; is_aligned ptr t\<rbrakk>
  \<Longrightarrow> is_aligned x t" apply (clarsimp simp:upto_enum_step_def image_def) apply (rule aligned_add_aligned[where n = t]) apply (rule is_aligned_mult_triv2) apply (simp add:word_bits_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set (map (\<lambda>x. x + ptr) [0 , 2 ^ t .e. up]); t < word_bits; is_aligned ptr t\<rbrakk> \<Longrightarrow> is_aligned x t proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>t < word_bits; is_aligned ptr t; xa \<le> up div 2 ^ t; x = xa * 2 ^ t + ptr\<rbrakk> \<Longrightarrow> is_aligned (xa * 2 ^ t + ptr) t proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>t < word_bits; is_aligned ptr t; xa \<le> up div 2 ^ t; x = xa * 2 ^ t + ptr\<rbrakk> \<Longrightarrow> is_aligned (xa * 2 ^ t) t
 2. \<And>xa. \<lbrakk>t < word_bits; is_aligned ptr t; xa \<le> up div 2 ^ t; x = xa * 2 ^ t + ptr\<rbrakk> \<Longrightarrow> is_aligned ptr t
 3. \<And>xa. \<lbrakk>t < word_bits; is_aligned ptr t; xa \<le> up div 2 ^ t; x = xa * 2 ^ t + ptr\<rbrakk> \<Longrightarrow> t \<le> t proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>t < word_bits; is_aligned ptr t; xa \<le> up div 2 ^ t; x = xa * 2 ^ t + ptr\<rbrakk> \<Longrightarrow> is_aligned ptr t
 2. \<And>xa. \<lbrakk>t < word_bits; is_aligned ptr t; xa \<le> up div 2 ^ t; x = xa * 2 ^ t + ptr\<rbrakk> \<Longrightarrow> t \<le> t proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma mapM_Cons_split:
  "xs \<noteq> [] \<Longrightarrow> (mapM f xs) = (do y \<leftarrow> f (hd xs); ys \<leftarrow> mapM f (tl xs); return (y # ys) od)" by (clarsimp simp:neq_Nil_conv mapM_Cons)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> mapM f xs = do y <- f (hd xs);
ys <- mapM f (tl xs);
return (y # ys)
od