crefine: arm-hyp: add word lemma FIXMEs

Various potential improvements that became apparent during the word
lemma move.

proof/crefine/ARM_HYP/ADT_C.thy

@@ -352,6 +352,7 @@ lemma projectKO_opt_UserData [simp]:
   "projectKO_opt KOUserData = Some UserData"
   by (simp add: projectKO_opts_defs)
 
+(* FIXME: rewrite using ucast_ucast_mask_shift *)
 lemma ucast_ucast_mask_pageBits_shift:
   "ucast (ucast (p && mask pageBits >> 2) :: 10 word) = p && mask pageBits >> 2"
   apply (rule word_eqI)
@@ -362,6 +363,7 @@ definition
 "processMemory s \<equiv> (ksMachineState s) \<lparr>underlying_memory := option_to_0 \<circ> (user_mem' s)\<rparr>"
 
 
+(* FIXME: rewrite using unat_ucast_mask_shift *)
 lemma unat_ucast_mask_pageBits_shift:
   "unat (ucast (p && mask pageBits >> 2) :: 10 word) = unat ((p::word32) && mask pageBits >> 2)"
   apply (simp only: unat_ucast)
@@ -373,6 +375,7 @@ lemma unat_ucast_mask_pageBits_shift:
   apply (simp add: pageBits_def mask_def)
   done
 
+(* FIXME: rewrite using mask_shift_sum *)
 lemma mask_pageBits_shift_sum:
   "unat n = unat (p && mask 2) \<Longrightarrow>
   (p && ~~ mask pageBits) + (p && mask pageBits >> 2) * 4 + n = (p::word32)"

proof/crefine/ARM_HYP/Arch_C.thy

@@ -1590,10 +1590,12 @@ lemma pte_sadness:
   apply (cases pte', cases pte, simp)
   done
 
+(* FIXME: move to Lib *)
 lemma hd_in_zip_set:
    "slots \<noteq> [] \<Longrightarrow> (hd slots, 0) \<in> set (zip slots [0.e.of_nat (length slots - Suc 0)::machine_word])"
    by (cases slots; simp add: upto_enum_word upto_0_to_n2 del: upt_Suc)
 
+(* FIXME: move to Lib *)
 lemma last_in_zip_set:
   "\<lbrakk> slots \<noteq> []; length js = length slots \<rbrakk> \<Longrightarrow> (last slots, last js) \<in> set (zip slots js)"
    apply (simp add: in_set_zip last_conv_nth)
@@ -1845,6 +1847,7 @@ lemma pde_align_ptBits:
   apply (simp add: table_bits_defs)
   done
 
+(* FIXME: consider generalising and moving to Word_Lemmas *)
 lemma vaddr_segment_nonsense3_folded:
   "is_aligned (p :: word32) pageBits \<Longrightarrow>
    (p + ((vaddr >> pageBits) && mask (pt_bits - pte_bits) << pte_bits) && ~~ mask pt_bits) = p"
@@ -1897,6 +1900,7 @@ lemma createMappingEntries_valid_pte_slots'2:
    apply (wp | simp add:valid_pte_slots'2_def)+
   done
 
+(* FIXME: rewrite using 'unat_shiftr_shiftl_mask_zero *)
 (* FIXME: move *)
 (* this one is specialised to a PDE for a supersection *)
 lemma vaddr_segment_nonsense6:
@@ -2711,6 +2715,7 @@ lemma framesize_from_H_eq_eq:
 
 lemmas framesize_from_H_eq_eqs = framesize_from_H_eq_eq trans [OF eq_commute framesize_from_H_eq_eq]
 
+(* FIXME: generalise, move to Word_Lib, and/or rewrite using 'shift_then_mask_eq_shift_low_bits' *)
 lemma shiftr_asid_low_bits_mask_asid_high_bits:
   "(asid :: word32) \<le> mask asid_bits
       \<Longrightarrow> (asid >> asid_low_bits) && mask asid_high_bits = asid >> asid_low_bits"
@@ -2721,6 +2726,7 @@ lemma shiftr_asid_low_bits_mask_asid_high_bits:
   apply (simp add: asid_bits_def)
   done
 
+(* FIXME: generalise, move to Word_Lib, and/or rewrite using 'leq_low_bits_iff_zero' *)
 lemma shiftr_asid_low_bits_mask_eq_0:
   "\<lbrakk> (asid :: word32) \<le> mask asid_bits; asid >> asid_low_bits = 0 \<rbrakk>
         \<Longrightarrow> (asid && mask asid_low_bits = 0) = (asid = 0)"
@@ -2779,7 +2785,7 @@ lemma ivc_label_flush_case:
   = D"
   by (auto split: invocation_label.split arch_invocation_label.split)
 
-
+(* FIXME: move to Lib *)
 lemma list_length_less:
   "(args = [] \<or> length args \<le> Suc 0) = (length args < 2)"
   by (case_tac args,simp_all)
@@ -2875,6 +2881,7 @@ lemma setVMRootForFlush_ccorres2:
   apply (auto simp: cap_get_tag_isCap_ArchObject2)
   done
 
+(* FIXME: move to Lib *)
 lemma at_least_2_args:
   "\<not>  length args < 2 \<Longrightarrow> \<exists>a b c. args = a#b#c"
   apply (case_tac args)
@@ -3855,6 +3862,8 @@ lemma maskCapRights_eq_Untyped [simp]:
   done
 
 
+(* FIXME: generalise, move to Word_Lib, and/or rewrite using
+   'leq_high_bits_shiftr_low_bits_leq_bits' *)
 lemma le_mask_asid_bits_helper:
   "x \<le> 2 ^ asid_high_bits - 1 \<Longrightarrow> (x::word32) << asid_low_bits \<le> mask asid_bits"
   apply (simp add: mask_def)
@@ -3976,6 +3985,7 @@ lemma framesize_from_H_mask2:
       Kernel_C.ARMSuperSection_def)+
   done
 
+(* FIXME: move to Lib *)
 lemma rel_option_alt_def:
   "rel_option f a b = (
       (a = None \<and>  b = None)

proof/crefine/ARM_HYP/CSpace_C.thy

@@ -157,6 +157,7 @@ lemma Arch_maskCapRights_ccorres [corres]:
    apply (cases arch_cap)
        by (fastforce simp add: cap_get_tag_isCap isCap_simps  simp del: not_ex omgwtfbbq)+
 
+(* FIXME: move to Wellformed_C (or move to_bool_bf out of Wellformed_C) *)
 lemma to_bool_mask_to_bool_bf:
   "to_bool (x && mask (Suc 0)) = to_bool_bf (x::word32)"
   apply (simp add: to_bool_bf_def to_bool_def)

proof/crefine/ARM_HYP/Invoke_C.thy

@@ -1785,6 +1785,7 @@ lemma name_seq_bound_helper:
   apply (rule ccontr, simp add: linorder_not_le)
   done
 
+(* FIXME: what's being proven here? it's a pure word lemma - should it go in Word_Lib? *)
 lemma reset_name_seq_bound_helper:
   fixes sz
   fixes v :: "('a :: len) word"

proof/crefine/ARM_HYP/Ipc_C.thy

@@ -3490,6 +3490,7 @@ definition
  "cfault_rel2 \<equiv> \<lambda>ft exnvar err. exnvar = (scast EXCEPTION_FAULT :: machine_word) \<and>
                    cfault_rel (Some ft) (errfault err) (errlookup_fault err)"
 
+(* FIXME: move to Lib *)
 lemma takeWhile_eq:
   "\<lbrakk> \<And>m. \<lbrakk> m < length ys \<rbrakk> \<Longrightarrow> P (xs ! m);
        length ys < length xs \<Longrightarrow> \<not> P (xs ! length ys);