word_lib+crefine: move AARCH64 lemmas to Word_Lib

- move AARCH64 word lemmas to the holding area in Word_Lib
- generalise word_ctz_upcast_id and provide word_ctz_upcast_id_32_64

Signed-off-by: Gerwin Klein <[email protected]>

lib/Word_Lib/Word_Lemmas_64_Internal.thy

@@ -57,4 +57,13 @@ lemmas mask_64_id[simp] = mask_len_id[where 'a=64, folded word_bits_def]
 lemma neq_0_unat: "x \<noteq> 0 \<Longrightarrow> 0 < unat x" for x::machine_word
   by (simp add: unat_gt_0)
 
+(* The 32-bit version is occasionally needed on 64-bit platforms *)
+lemma word_rsplit_0_32:
+  "word_rsplit (0::32 word) = [0, 0, 0, (0::8 word)]"
+  by (simp add: word_rsplit_def bin_rsplit_def word_bits_def word_size_def Cons_replicate_eq)
+
+lemma word_ctz_upcast_id_32_64:
+  "x \<noteq> 0 \<Longrightarrow> word_ctz (UCAST(32 \<rightarrow> 64) x) = word_ctz x"
+  by (simp add: word_ctz_upcast_id is_up)
+
 end

lib/Word_Lib/Word_Lemmas_Internal.thy

@@ -745,4 +745,97 @@ lemma shiftr_anti_mono:
   apply (simp add: drop_bit_eq_div zdiv_mono2)
   done
 
+lemma mask_shift_neg_mask_eq:
+  "\<lbrakk> n' \<le> n; x \<le> mask (m+n') \<rbrakk> \<Longrightarrow> (x && ~~ mask n) && (mask m << n') = x && ~~ mask n"
+  by word_eqI_solve
+
+lemma from_bool_inj[simp]:
+  "(from_bool x = from_bool y) = (x = y)"
+  unfolding from_bool_def
+  by (auto split: bool.splits)
+
+lemma word_le_1_and_idem:
+  "w \<le> 1 \<Longrightarrow> w AND 1 = w" for w :: "_ word"
+  by (metis word_bw_same(1) word_le_1 word_log_esimps(7))
+
+lemma from_to_bool_le_1_idem:
+  "w \<le> 1 \<Longrightarrow> from_bool (to_bool w) = w"
+  apply (subst word_le_1_and_idem[symmetric], assumption)
+  apply (simp add: from_to_bool_last_bit)
+  apply (simp add: word_le_1_and_idem)
+  done
+
+lemma and_1_0_not_bit_0:
+  "(w && 1 = 0) = (\<not> (w::'a::len word) !! 0)"
+  using to_bool_and_1[simplified to_bool_def, where x=w]
+  by auto
+
+lemma unat_scast_up:
+  "\<lbrakk> LENGTH('a) \<le> LENGTH('b); 0 \<le> sint x \<rbrakk> \<Longrightarrow>unat (scast x::'b::len word) = unat x"
+  for x :: "'a :: len  word"
+  apply (simp flip: bit_last_iff not_less)
+  apply word_eqI
+  apply (clarsimp simp: min_def split: if_splits)
+  apply (rule conjI; clarsimp)
+   apply (drule test_bit_lenD)
+   apply clarsimp
+   apply (metis le_antisym nat_le_Suc_less_imp)
+  apply fastforce
+  done
+
+lemma unat_uint_less:
+  "unat x < nat i \<Longrightarrow> uint x < i" for x :: "'a :: len word"
+  by (simp add: zless_nat_eq_int_zless)
+
+lemma sint_ge_zero_uint:
+  "uint x < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> sint (x :: 'a :: len word) \<ge> 0"
+  by (simp add: sint_eq_uint_2pl word_2p_lem wsst_TYs(3))
+
+lemma sint_ge_zero_unat:
+  "unat x < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> sint (x :: 'a :: len word) \<ge> 0"
+  by (fastforce intro: sint_ge_zero_uint unat_uint_less simp: nat_power_eq)
+
+lemma mask_shiftl_le_mask:
+  "mask n << m \<le> (mask (n+m) :: 'a::len word)"
+  by (subst add.commute)
+     (rule leq_high_bits_shiftr_low_bits_leq_bits, simp)
+
+(* This is more useful for getting rid of a downcast *)
+lemma unat_ucast_unat_id:
+  "unat x < 2 ^ LENGTH('b) \<Longrightarrow> unat (UCAST('a::len \<rightarrow> 'b::len) x) = unat x"
+  by (simp add: unat_eq_of_nat)
+
+lemma ucast_up_preserves_gt0:
+  "\<lbrakk> 0 < x; LENGTH('a) < LENGTH('b) \<rbrakk> \<Longrightarrow> 0 < (ucast x :: 'b::len word)" for x :: "'a::len word"
+  by (metis ucast_0 ucast_less_ucast_weak)
+
+lemma ucast_up_preserves_not0:
+  "\<lbrakk> x \<noteq> 0; LENGTH('a) < LENGTH('b::len) \<rbrakk> \<Longrightarrow> (ucast x :: 'b::len word) \<noteq> 0"
+  for x :: "'a::len word"
+  by (metis ucast_0 ucast_ucast_id)
+
+lemma unat_le_fold:
+  "n < 2 ^ LENGTH('a) \<Longrightarrow> (unat x \<le> n) = (x \<le> of_nat n)" for x::"'a::len word"
+  by (simp add: word_le_nat_alt unat_of_nat_eq)
+
+lemma ucast_and_mask_drop:
+  "LENGTH('a) \<le> n \<Longrightarrow> (ucast w :: 'b::len word) && mask n = ucast w" for w::"'a::len word"
+  by word_eqI (fastforce dest: test_bit_lenD)
+
+lemma add_mask_ignore:
+  "x && mask n = 0 \<Longrightarrow> v + x && mask n = v && mask n"
+  by (metis add_0_right mask_eqs(2))
+
+lemma word_ctz_upcast_id:
+  "\<lbrakk> x \<noteq> 0; is_up (ucast::'a word \<Rightarrow>'b word) \<rbrakk> \<Longrightarrow>
+  word_ctz (ucast x :: 'b::len word) = word_ctz x" for x :: "'a::len word"
+  unfolding word_ctz_def
+  by (simp add: ucast_up_app[where n="LENGTH('b) - LENGTH('a)"]
+                source_size_def target_size_def is_up_def eq_zero_set_bl)
+
+lemma ucast_ucast_mask_id:
+  "\<lbrakk> LENGTH('b::len) < LENGTH('a); n = LENGTH('b) \<rbrakk> \<Longrightarrow>
+   UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) (x && mask n)) = x && mask n" for x :: "'a::len word"
+  by (simp add: ucast_ucast_len[OF eq_mask_less])
+
 end

proof/crefine/AARCH64/ADT_C.thy

@@ -953,9 +953,7 @@ lemma cpspace_vcpu_relation_unique:
    apply (case_tac "64 \<le> r"; simp)
   apply (rule conjI)
    apply (rule ext, blast)
-  apply (rule conjI)
-   apply (rule ext, rename_tac vppi)
-   apply (rule from_bool_eqI, blast)
+  apply (rule conjI, blast)
   apply (case_tac vtimer, case_tac vtimer')
   apply clarsimp
   done

proof/crefine/AARCH64/Arch_C.thy

@@ -921,10 +921,6 @@ lemma capVSMappedASID_CL_masked[unfolded asid_bits_def, simplified]:
   apply (clarsimp simp: cap_lift_def Let_def asid_bits_def split: if_splits)
   done
 
-lemma mask_shift_neg_mask_eq: (* FIXME AARCH64: move to Word_Lib *)
-  "\<lbrakk> n' \<le> n; x \<le> mask (m+n') \<rbrakk> \<Longrightarrow> (x && ~~ mask n) && (mask m << n') = x && ~~ mask n"
-  by word_eqI_solve
-
 lemma pptrUserTop_le_canonical_val[unfolded canonical_bit_def, simplified]:
   "x \<le> pptrUserTop \<Longrightarrow> x \<le> mask (Suc canonical_bit)"
   by (simp add: pptrUserTop_def canonical_bit_def order_trans[OF _ mask_mono] split: if_split_asm)
@@ -1336,11 +1332,6 @@ lemma cpte_relation_pte_invalid_eq:
   "cpte_relation pte pte' \<Longrightarrow> (pte_lift pte' = Some Pte_pte_invalid) = (pte = InvalidPTE)"
   by (clarsimp simp: cpte_relation_def Let_def split: if_splits pte.splits)
 
-lemma from_bool_inj[simp]: (* FIXME AARCH64: move to Word_Lib *)
-  "(from_bool x = from_bool y) = (x = y)"
-  unfolding from_bool_def
-  by (auto split: bool.splits)
-
 lemma performPageInvocationMap_ccorres:
   "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
        (invs' and cte_at' slot and (\<lambda>s. 7 \<le> gsMaxObjectSize s)
@@ -1626,11 +1617,6 @@ lemma ccap_relation_FrameCap_IsMapped:
   apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_splits)
   done
 
-lemma and_1_0_not_bit_0: (* FIXME AARCH64: move to Word_Lib *)
-  "(w && 1 = 0) = (\<not> (w::'a::len word) !! 0)"
-  using to_bool_and_1[simplified to_bool_def, where x=w]
-  by auto
-
 lemma cte_wp_at'_frame_at':
   "\<lbrakk> cte_wp_at'
        ((=) (capability.ArchObjectCap (arch_capability.FrameCap p v1 sz d m)) \<circ> cteCap) slot s;
@@ -1764,30 +1750,6 @@ lemma isPageFlushLabel_disj:
   isPageFlushLabel label"
   by (auto simp: isPageFlushLabel_def split: invocation_label.split arch_invocation_label.split)
 
-lemma unat_scast_up: (* FIXME AARCH64: currently unused, move to Word_Lib *)
-  "\<lbrakk> LENGTH('a) \<le> LENGTH('b); 0 \<le> sint x \<rbrakk> \<Longrightarrow> unat (scast x::'b::len word) = unat x" for x :: "'a :: len  word"
-  apply (simp flip: bit_last_iff not_less)
-  apply (word_eqI)
-  apply (clarsimp simp: min_def split: if_splits)
-  apply (rule conjI; clarsimp)
-   apply (drule test_bit_lenD)
-   apply clarsimp
-   apply (metis le_antisym nat_le_Suc_less_imp)
-  apply fastforce
-  done
-
-lemma unat_uint_less: (* FIXME AARCH64: currently unused, move to Word_Lib *)
-  "unat x < nat i \<Longrightarrow> uint x < i" for x :: "'a :: len word"
-  by (simp add: zless_nat_eq_int_zless)
-
-lemma sint_ge_zero_uint: (* FIXME AARCH64: currently unused, move to Word_Lib *)
-  "uint x < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> sint (x :: 'a :: len word) \<ge> 0"
-  by (simp add: sint_eq_uint_2pl word_2p_lem wsst_TYs(3))
-
-lemma sint_ge_zero_unat: (* FIXME AARCH64: currently unused, move to Word_Lib *)
-  "unat x < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> sint (x :: 'a :: len word) \<ge> 0"
-  by (fastforce intro: sint_ge_zero_uint unat_uint_less simp: nat_power_eq)
-
 lemma flushtype_relation_triv:
   "isPageFlushLabel (invocation_type label) \<or> isVSpaceFlushLabel (invocation_type label)
    \<Longrightarrow> flushtype_relation (labelToFlushType label) label"

proof/crefine/AARCH64/CSpace_C.thy

@@ -1902,11 +1902,6 @@ lemma clearUntypedFreeIndex_noop_ccorres:
   apply simp
   done
 
-lemma mask_shiftl_le_mask: (* FIXME AARCH64 move to Word_Lib *)
-  "mask n << m \<le> (mask (n+m) :: 'a::len word)"
-  by (subst add.commute)
-     (rule leq_high_bits_shiftr_low_bits_leq_bits, simp)
-
 lemma canonical_address_mdbNext_CL:
   "canonical_address (mdbNext_CL (mdb_node_lift (cteMDBNode_C cte')))"
   apply (simp add: mdb_node_lift_def canonical_address_def canonical_address_of_def

proof/crefine/AARCH64/Finalise_C.thy

@@ -873,11 +873,6 @@ definition
                       ucast irq \<le> UCAST(32 signed \<rightarrow> irq_len) Kernel_C.maxIRQ)
        | None \<Rightarrow> cirq = ucast irqInvalid"
 
-(* FIXME AARCH64 move to word lib, this is more useful for getting rid of a downcast *)
-lemma unat_ucast_unat_id:
-  "\<lbrakk> unat x < 2^LENGTH('b)  \<rbrakk> \<Longrightarrow> unat (UCAST('a::len \<rightarrow> 'b::len) x) = unat x"
-  by (simp add: unat_eq_of_nat)
-
 lemma irq_opt_relation_Some_ucast:
   "\<lbrakk> x && mask (LENGTH(irq_len)) = x; ucast x \<noteq> irqInvalid;
      ucast x \<le> (scast Kernel_C.maxIRQ :: irq_len word) \<or> x \<le> (scast Kernel_C.maxIRQ :: machine_word) \<rbrakk>
@@ -1425,10 +1420,6 @@ lemmas lookupPTFromLevel_val_helpers =
   of_nat_ptTranslationBits_NormalPT_T_val
   of_nat_ptTranslationBits_VSRootPT_T_val
 
-lemma from_bool_inj[simp]: (* FIXME AARCH64: move to Word_Lib *)
-  "(from_bool x = from_bool y) = (x = y)"
-  by (simp add: from_bool_def split: bool.splits)
-
 lemma lookupPTFromLevel_ccorres[unfolded lookupPTFromLevel_val_helpers]:
   notes Collect_const[simp del] call_ignore_cong[cong]
   defines "idx i \<equiv> of_nat (ptBitsLeft maxPTLevel) - of_nat (ptTranslationBits NormalPT_T) * i"

proof/crefine/AARCH64/Recycle_C.thy

@@ -1089,11 +1089,6 @@ lemma access_ti_list_word8_array:
   apply (simp add: typ_info_word word_rsplit_0 word_rsplit_same replicateHider_def replicate_append_same)
   done
 
-(* FIXME AARCH64 move, original word_rsplit_0 assumes machine word *)
-lemma word_rsplit_0_32:
-  "word_rsplit (0::32 word) = [0, 0, 0, (0::8 word)]"
-  by (simp add: word_rsplit_def bin_rsplit_def word_bits_def word_size_def Cons_replicate_eq)
-
 lemma coerce_memset_to_heap_update:
   "heap_update_list x (replicateHider (size_of (TYPE (tcb_C))) 0)
       = heap_update (tcb_Ptr x)

proof/crefine/AARCH64/Syscall_C.thy

@@ -1700,24 +1700,6 @@ lemma vgicUpdateLR_ccorres_armHSCurVCPU:
   apply (clarsimp dest!: rf_sr_ksArchState_armHSCurVCPU simp: cur_vcpu_relation_def split: option.splits)
   done
 
-(* FIXME AARCH64 move to word lib *)
-lemma ucast_up_preserves_gt0:
-  "\<lbrakk> 0 < x; LENGTH('a) < LENGTH('b) \<rbrakk> \<Longrightarrow> 0 < (ucast x :: 'b::len word)"
-  for x :: "'a::len word"
-  by (metis ucast_0 ucast_less_ucast_weak)
-
-(* FIXME AARCH64 move to word lib *)
-lemma ucast_up_preserves_not0:
-  "\<lbrakk> x \<noteq> 0; LENGTH('a) < LENGTH('b::len) \<rbrakk> \<Longrightarrow> (ucast x :: 'b::len word) \<noteq> 0"
-  for x :: "'a::len word"
-  by (metis ucast_0 ucast_ucast_id)
-
-(* FIXME AARCH64 move to word lib *)
-lemma word_ctz_upcast_id:
-  "x \<noteq> 0 \<Longrightarrow> word_ctz (UCAST(32 \<rightarrow> 64) x) = word_ctz x"
-  unfolding word_ctz_def
-  by (simp add: ucast_up_app source_size_def target_size_def eq_zero_set_bl)
-
 (* folded calculation of eisr used in vgicMaintenance *)
 definition
   eisr_calc :: "32 word \<Rightarrow> 32 word \<Rightarrow> nat"
@@ -1901,7 +1883,7 @@ proof -
             apply (rule conseqPre, vcg)
 
 
-    subgoal by (clarsimp simp: ucast_up_preserves_not0 word_ctz_upcast_id scast_s64_int_ctz_eq
+    subgoal by (clarsimp simp: ucast_up_preserves_not0 word_ctz_upcast_id_32_64 scast_s64_int_ctz_eq
                                ctz_add_0x20_s64_int_eq sint_s64_ctz_ge_0
                                order.trans[OF sint_s64_ctz_le_32])
 

proof/crefine/AARCH64/VSpace_C.thy

@@ -526,10 +526,6 @@ lemma levelType_maxPTLevel[simp]: (* FIXME AARCH64: move *)
   "levelType maxPTLevel = VSRootPT_T"
   by (simp add: levelType_def)
 
-lemma unat_le_fold: (* FIXME AARCH64: move to Word_Lib *)
-  "n < 2 ^ LENGTH('a) \<Longrightarrow> (unat x \<le> n) = (x \<le> of_nat n)" for x::"'a::len word"
-  by (simp add: word_le_nat_alt unat_of_nat_eq)
-
 lemma pte_at_rf_sr: (* FIXME AARCH64: move *)
   "\<lbrakk>ko_at' pte p s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow>
    \<exists>pte'. cslift s' (pte_Ptr p) = Some pte' \<and> cpte_relation pte pte'"
@@ -1485,10 +1481,6 @@ lemma findFreeHWASID_ccorres:
   apply simp
   done
 
-lemma ucast_and_mask_drop: (* FIXME AARCH64: move to Word_Lib *)
-  "LENGTH('a) \<le> n \<Longrightarrow> (ucast w :: 'b::len word) && mask n = ucast w" for w::"'a::len word"
-  by word_eqI (fastforce dest: test_bit_lenD)
-
 lemma storeHWASID_ccorres:
   "ccorres dc xfdc \<top> (\<lbrace>\<acute>asid___unsigned_long = asid\<rbrace> \<inter> \<lbrace>\<acute>hw_asid = vmid\<rbrace>) []
            (storeVMID asid vmid) (Call storeHWASID_'proc)"
@@ -1709,10 +1701,6 @@ lemma setVMRoot_ccorres:
               elim!: ccap_relationE
               split: if_split_asm cap_CL.splits)
 
-lemma add_mask_ignore: (* FIXME AARCH64: move to WordLib *)
-  "x && mask n = 0 \<Longrightarrow> v + x && mask n = v && mask n"
-  by (metis arith_simps(50) mask_eqs(2))
-
 lemma pptrBaseOffset_cacheLineSize_aligned[simp]: (* FIXME AARCH64: move *)
   "pptrBaseOffset && mask cacheLineSize = 0"
   by (simp add: pptrBaseOffset_def paddrBase_def pptrBase_def cacheLineSize_def mask_def)
@@ -1911,11 +1899,6 @@ lemma casid_map_relation_vspace_tag:
    asid_map_get_tag casid_map = scast asid_map_asid_map_vspace"
   by (clarsimp simp: casid_map_relation_def asid_map_lift_def Let_def split: if_splits)
 
-lemma ucast_ucast_mask_id: (* FIXME AARCH64: move to Word_Lib *)
-  "\<lbrakk> LENGTH('b::len) < LENGTH('a); n = LENGTH('b) \<rbrakk> \<Longrightarrow>
-   UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) (x && mask n)) = x && mask n" for x :: "'a::len word"
-  by (simp add: ucast_ucast_len[OF eq_mask_less])
-
 lemma invalidateTLBByASIDVA_ccorres:
   "ccorres dc xfdc
            (valid_arch_state' and K (asid_wf asid))

proof/crefine/ARM_HYP/ADT_C.thy

@@ -1014,9 +1014,7 @@ lemma cpspace_vcpu_relation_unique:
    apply (case_tac "64 \<le> r"; simp)
   apply (rule conjI)
    apply (rule ext, blast)
-  apply (rule conjI)
-   apply (rule ext, rename_tac vppi)
-   apply (rule from_bool_eqI, blast)
+  apply (rule conjI, blast)
   apply (case_tac vtimer, case_tac vtimer')
   apply clarsimp
   done

proof/crefine/ARM_HYP/Ipc_C.thy

@@ -4074,7 +4074,6 @@ apply (ctac(no_vcg) add: Arch_getSanitiseRegisterInfo_ccorres)
                                        msg_align_bits sanitiseRegister_def
                              simp del: upt_rec_numeral cong: if_cong register.case_cong,
                         simp_all add: word_less_nat_alt unat_add_lem[THEN iffD1] unat_of_nat)[1]
-               apply (rule_tac x=rv in exI, auto)[1]
                 apply (clarsimp simp: n_syscallMessage_def n_msgRegisters_def
                                       msgRegisters_ccorres
                                       syscallMessage_ccorres

proof/crefine/Move_C.thy

@@ -1480,17 +1480,4 @@ lemma multiple_add_less_nat:
   apply simp
   done
 
-(* FIXME AARCH64 move to wherever we keep the from_bool/to_bool lemmas *)
-lemma word_le_1_and_idem:
-  "w \<le> 1 \<Longrightarrow> w AND 1 = w" for w :: "_ word"
-  by (metis word_bw_same(1) word_le_1 word_log_esimps(7))
-
-(* FIXME AARCH64 move to wherever we keep the from_bool/to_bool lemmas *)
-lemma from_to_bool_le_1_idem:
-  "w \<le> 1 \<Longrightarrow> from_bool (to_bool w) = w"
-  apply (subst word_le_1_and_idem[symmetric], assumption)
-  apply (simp add: from_to_bool_last_bit)
-  apply (simp add: word_le_1_and_idem)
-  done
-
 end

proof/crefine/RISCV64/Ipc_C.thy

@@ -3816,7 +3816,6 @@ lemma copyMRsFaultReply_ccorres_syscall:
                                        msg_align_bits sanitiseRegister_def
                              simp del: upt_rec_numeral cong: if_cong register.case_cong,
                         simp_all add: word_less_nat_alt unat_add_lem[THEN iffD1] unat_of_nat)[1]
-               apply (rule_tac x=rv in exI, auto)[1]
                 apply (clarsimp simp: n_syscallMessage_def n_msgRegisters_def
                                       msgRegisters_ccorres
                                       syscallMessage_ccorres

proof/crefine/X64/Ipc_C.thy

@@ -3828,7 +3828,6 @@ lemma copyMRsFaultReply_ccorres_syscall:
                                        msg_align_bits sanitiseRegister_def
                              simp del: upt_rec_numeral cong: if_cong register.case_cong,
                         simp_all add: word_less_nat_alt unat_add_lem[THEN iffD1] unat_of_nat)[1]
-               apply (rule_tac x=rv in exI, auto)[1]
                 apply (clarsimp simp: n_syscallMessage_def n_msgRegisters_def
                                       msgRegisters_ccorres
                                       syscallMessage_ccorres