crefine: remove unused lemmas; resolve AARCH64 FIXMEs

Resolve obvious FIXMEs in AARCH64 proofs:

- questions that have resolved themselves
- lemmas that are unused (some on all architectures)
- trivial lemma moves
- some FIXME updates for easier grep later

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

proof/crefine/AARCH64/ADT_C.thy

@@ -161,17 +161,6 @@ where
   "getContext_C thread \<equiv>
    \<lambda>s. from_user_context_C (tcbContext_C (the (clift (t_hrs_' (globals s)) (Ptr &(thread\<rightarrow>[''tcbArch_C''])))))"
 
-(* FIXME AARCH64 move, this is very specific and rather ugly, is it possible to generalise? *)
-lemma size_64_less_64:
-  "size (r::64) < (64::nat)"
-  apply (induct r rule: bit0.plus_induct, simp)
-  apply (frule bit0.Suc_size)
-  apply (case_tac "x = 64 - 1"; clarsimp)
-  apply (prop_tac "size x \<noteq> size (64 - 1 :: 64)")
-   apply (subst bit0.size_inj, simp)
-  apply simp
-  done
-
 lemma from_user_context_C:
   "ccontext_relation uc uc' \<Longrightarrow> from_user_context_C uc' = uc"
   unfolding ccontext_relation_def cregs_relation_def
@@ -944,9 +933,6 @@ lemma option_to_ctcb_ptr_inj:
   apply (erule is_aligned_no_overflow_0; simp)
   done
 
-(* FIXME AARCH64 this is bad news, we need the alignment constraints to use option_to_ctcb_ptr_inj,
-   and we used to be able to say that if there's a non-null tcb pointer in a vcpu, then it's aligned,
-   but on AARCH64 we don't have anything like that in vcpu validity, so we are stuck *)
 lemma cpspace_vcpu_relation_unique:
   assumes "cpspace_vcpu_relation ah ch" "cpspace_vcpu_relation ah' ch"
   assumes "\<forall>x \<in> ran (map_to_vcpus ah). is_aligned_opt (vcpuTCBPtr x) tcbBlockSizeBits"
@@ -1064,19 +1050,6 @@ lemma cpspace_asidpool_relation_unique:
    apply (clarsimp simp: non_dom_eval_eq)
   apply force
   done
-(* FIXME AARCH64 old proof for reference, remove if not needed after rest of ADT_H is fixed
-   apply clarsimp
-   apply (case_tac "i \<le> mask asid_low_bits", simp)
-    apply (drule sym[where s="option_to_ptr _"], simp)
-    apply (simp add: option_to_ptr_def option_to_0_def ran_def split: option.splits)
-   apply clarsimp
-   apply (drule_tac c=i in contra_subsetD, simp)+
-   apply (clarsimp simp: non_dom_eval_eq)
-  apply clarsimp
-  apply (rule ccontr)
-  apply clarsimp
-  apply blast
-  done *)
 
 lemma cpspace_user_data_relation_unique:
   "\<lbrakk>cmap_relation (heap_to_user_data ah bh) (clift ch) Ptr cuser_user_data_relation;
@@ -1308,12 +1281,6 @@ lemma ksPSpace_eq_imp_valid_tcb'_eq:
                  valid_tcb'_def valid_tcb_state'_def valid_bound_ntfn'_def valid_arch_tcb'_def
           split: thread_state.splits option.splits)
 
-(* FIXME AARCH64 we don't have valid_vcpu' on AARCH64
-lemma ksPSpace_eq_imp_valid_vcpu'_eq:
-  assumes ksPSpace: "ksPSpace s' = ksPSpace s"
-  shows "valid_vcpu' vcpu s' = valid_vcpu' vcpu s"
-  by (auto simp: valid_vcpu'_def ksPSpace_eq_imp_typ_at'_eq[OF ksPSpace] split: option.splits) *)
-
 lemma ksPSpace_eq_imp_valid_objs'_eq:
   assumes ksPSpace: "ksPSpace s' = ksPSpace s"
   shows "valid_objs' s' = valid_objs' s"

proof/crefine/AARCH64/ArchMove_C.thy

@@ -462,9 +462,6 @@ crunch ko_at'[wp]: readVCPUReg "\<lambda>s. P (ko_at' a p s)"
 
 crunch obj_at'[wp]: readVCPUReg "\<lambda>s. P (obj_at' a p s)"
 
-(* FIXME AARCH64 this might not be needed, but currently proved version doesn't have the P
-crunch pred_tcb_at'[wp]: readVCPUReg "\<lambda>s. P (pred_tcb_at' a b p s)"  *)
-
 crunch ksCurThread[wp]: readVCPUReg "\<lambda>s. P (ksCurThread s)"
 
 (* schematic_goal leads to Suc (Suc ..) form only *)

proof/crefine/AARCH64/Arch_C.thy

@@ -745,7 +745,6 @@ lemma ccap_relation_VSpaceCap_IsMapped:
   apply (simp add: to_bool_def)
   done
 
-(* FIXME AARCH64 do we also want VSRootPT_T/cap_vspace_cap_lift? *)
 lemma ccap_relation_PageTableCap_BasePtr:
   "\<lbrakk> ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap p NormalPT_T m)) ccap \<rbrakk>
    \<Longrightarrow> capPTBasePtr_CL (cap_page_table_cap_lift ccap) = p"
@@ -754,7 +753,6 @@ lemma ccap_relation_PageTableCap_BasePtr:
   apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_splits)
   done
 
-(* FIXME AARCH64 do we also want VSRootPT_T/cap_vspace_cap_lift? *)
 lemma ccap_relation_PageTableCap_MappedASID:
   "\<lbrakk> ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap p NormalPT_T (Some (a,b))))
                    ccap \<rbrakk>
@@ -888,7 +886,7 @@ lemma slotcap_in_mem_VSpace:
   apply (simp add: cap_get_tag_isCap_ArchObject2)
   done
 
-lemma pptrUserTop_val: (* FIXME AARCH64: need value spelled out for C code *)
+lemma pptrUserTop_val: (* FIXME AARCH64: need value spelled out for C code, make schematic *)
   "pptrUserTop = 0xFFFFFFFFFFF"
   by (simp add: pptrUserTop_def mask_def Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)
 
@@ -898,11 +896,6 @@ lemma ccap_relation_vspace_base: (* FIXME AARCH64: move up if needed in VSpace_R
   by (frule cap_get_tag_isCap_unfolded_H_cap)
      (clarsimp simp: cap_vspace_cap_lift ccap_relation_def cap_to_H_def split: if_splits)
 
-(* The magic 4 comes out of the bitfield generator *)
-lemma ThreadState_Restart_mask[simp]: (* FIXME AARCH64: move far up *)
-  "(scast ThreadState_Restart::machine_word) && mask 4 = scast ThreadState_Restart"
-  by (simp add: ThreadState_Restart_def mask_def)
-
 lemma Restart_valid[simp]:
   "valid_tcb_state' Restart s"
   by (simp add: valid_tcb_state'_def)
@@ -1297,11 +1290,6 @@ definition
                             (pde_range_C.length_C pde_ran))
           \<and> 1 \<le> pde_range_C.length_C pde_ran"
 
-(* FIXME AARCH64 do we want an analogue for AARCH64?
-definition
- "vm_attribs_relation attr attr' \<equiv>
-       riscvExecuteNever_CL (vm_attributes_lift attr') = from_bool (riscvExecuteNever attr)" *)
-
 lemma framesize_from_H_eqs:
   "(framesize_from_H vsz = scast Kernel_C.ARMSmallPage) = (vsz = ARMSmallPage)"
   "(framesize_from_H vsz = scast Kernel_C.ARMLargePage) = (vsz = ARMLargePage)"
@@ -1348,7 +1336,7 @@ 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 up *)
+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)
@@ -1415,24 +1403,6 @@ lemma performPageInvocationMap_ccorres:
                          ccap_relation_FrameCap_MappedAddress)
   done
 
-lemma vaddr_segment_nonsense3_folded: (* FIXME AARCH64: remove if unused, also in RISCV64 and X64 *)
-  "is_aligned (p :: machine_word) pageBits \<Longrightarrow>
-   (p + ((vaddr >> pageBits) && mask ((pt_bits pt_t) - word_size_bits) << word_size_bits) &&
-     ~~ mask (pt_bits pt_t)) = p"
-  apply (rule is_aligned_add_helper[THEN conjunct2])
-   apply (simp add: bit_simps mask_def)+
-   (* FIXME AARCH64 abstraction violation *)
-   apply (simp add: Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)
-  (* FIXME AARCH64 consider cleanup *)
-  apply (cases pt_t; clarsimp simp: bit_simps mask_def split: if_splits)
-   apply (simp_all add: shiftl_less_t2n[where m=12 and n=3, simplified,
-                                        OF and_mask_less'[where n=9, unfolded mask_def, simplified]])
-  apply clarsimp
-  apply (rule shiftl_less_t2n[where m=13, simplified]; simp)
-  apply (rule and_mask_less'[where n=10, simplified mask_def, simplified])
-  apply simp
-  done
-
 lemma performPageGetAddress_ccorres:
   "ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and (\<lambda>s. ksCurThread s = thread) and ct_in_state' ((=) Restart))
@@ -1556,18 +1526,6 @@ lemma slotcap_in_mem_valid:
   apply (erule(1) ctes_of_valid')
   done
 
-lemma unat_less_iff64: (* FIXME AARCH64: remove if unused *)
-  "\<lbrakk>unat (a::machine_word) = b;c < 2^word_bits\<rbrakk>
-   \<Longrightarrow> (a < of_nat c) = (b < c)"
-  apply (rule iffI)
-    apply (drule unat_less_helper)
-    apply simp
-  apply (simp add:unat64_eq_of_nat)
-  apply (rule of_nat_mono_maybe)
-   apply (simp add:word_bits_def)
-  apply simp
-  done
-
 lemma injection_handler_if_returnOk:
   "injection_handler Inl (if a then b else returnOk c)
   = (if a then (injection_handler Inl b) else returnOk c)"
@@ -1580,11 +1538,6 @@ lemma injection_handler_if_returnOk:
 lemma pbfs_less: "pageBitsForSize sz < 31"
   by (case_tac sz,simp_all add: bit_simps)
 
-definition
-  to_option :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a option" (* FIXME AARCH64: remove if unused, also in X64 and RISCV64 *)
-where
-  "to_option f x \<equiv> if f x then Some x else None"
-
 lemma cte_wp_at_eq_gsMaxObjectSize:
   "cte_wp_at' ((=) cap o cteCap) slot s
     \<Longrightarrow> valid_global_refs' s
@@ -1673,8 +1626,7 @@ lemma ccap_relation_FrameCap_IsMapped:
   apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_splits)
   done
 
-(* FIXME AARCH64: move *)
-lemma and_1_0_not_bit_0:
+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

proof/crefine/AARCH64/CSpace_C.thy

@@ -1902,8 +1902,7 @@ lemma clearUntypedFreeIndex_noop_ccorres:
   apply simp
   done
 
-(* FIXME AARCH64 move *)
-lemma mask_shiftl_le_mask:
+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)

proof/crefine/AARCH64/Finalise_C.thy

@@ -1118,7 +1118,7 @@ lemma deleteASIDPool_ccorres:
              apply (rule ccorres_move_c_guard_ap)
              apply (rule_tac ccorres_symb_exec_r2)
                apply csymbr
-               apply (rule ccorres_guard_imp) (* FIXME AARCH64: csymbr messes up C precond *)
+               apply (rule ccorres_guard_imp)
                  apply (rule_tac R="\<lambda>_. True" and
                                  R'="\<lbrace>(inv asidpool.ASIDPool poolKO (of_nat n) \<noteq> None) \<longleftrightarrow>
                                       (asid_map_get_tag \<acute>asid_map = scast asid_map_asid_map_vspace)\<rbrace> \<inter>
@@ -1131,7 +1131,6 @@ lemma deleteASIDPool_ccorres:
                  apply (rule ccorres_return_Skip)
                 apply clarsimp
                 apply assumption
-               (* FIXME AARCH64: repairing broken csymbr C precond matching *)
                apply (clarsimp split: if_split simp: upto_enum_word simp del: upt.simps)
                apply (drule CollectD, assumption)
               apply clarsimp
@@ -1905,9 +1904,6 @@ lemma Zombie_new_spec:
   apply (simp add: word_add_less_mono1[where k=1 and j="0x3F", simplified])
   done
 
-(* FIXME AARCH64 move? retire? revisit *)
-lemmas upcast_ucast_id = More_Word.ucast_up_inj
-
 lemma ccap_relation_IRQHandler_mask:
   "\<lbrakk> ccap_relation acap ccap; isIRQHandlerCap acap \<rbrakk>
     \<Longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift ccap) && mask 9
@@ -2618,7 +2614,7 @@ lemma Arch_finaliseCap_ccorres:
                        F="\<lambda>asid'. asid' = asid" and
                        R=\<top> and
                        R'=UNIV
-                       in ccorres_symb_exec_r_abstract_UNIV) (* FIXME AARCH64: csymbr fails *)
+                       in ccorres_symb_exec_r_abstract_UNIV)
           apply vcg
           apply (clarsimp simp: ccap_relation_def map_option_Some_eq2 dest!: cap_to_H_VSCap)
           apply (clarsimp simp: cap_vspace_cap_lift_def cap_vspace_cap_lift)
@@ -2655,7 +2651,7 @@ lemma Arch_finaliseCap_ccorres:
                       F="\<lambda>asid'. asid' = asid" and
                       R=\<top> and
                       R'=UNIV
-                      in ccorres_symb_exec_r_abstract_UNIV) (* FIXME AARCH64: csymbr fails *)
+                      in ccorres_symb_exec_r_abstract_UNIV)
          apply vcg
          apply (clarsimp simp: ccap_relation_def map_option_Some_eq2 dest!: cap_to_H_PTCap)
          apply (clarsimp simp: cap_page_table_cap_lift_def cap_page_table_cap_lift)

proof/crefine/AARCH64/IpcCancel_C.thy

@@ -144,7 +144,7 @@ lemma tcbEPDequeue_spec:
    apply simp
   apply (frule c_guard_clift)
   apply (simp add: typ_heap_simps')
-  apply (intro allI conjI impI) (* FIXME AARCH64 different number of goals, not sure why *)
+  apply (intro allI conjI impI)
                apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff)
               apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff
                               cong: if_weak_cong)

proof/crefine/AARCH64/Machine_C.thy

@@ -62,7 +62,7 @@ assumes maskInterrupt_ccorres:
            (doMachineOp (maskInterrupt m irq))
            (Call maskInterrupt_'proc)"
 
-(* FIXME AARCH64 this is a simplification until complete FPU handling is added at a future date *)
+(* This is a simplification until complete FPU handling is added at a future date *)
 assumes fpuThreadDelete_ccorres:
   "ccorres dc xfdc (tcb_at' thread) (\<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs
      (fpuThreadDelete thread)
@@ -265,14 +265,6 @@ assumes vcpu_hw_write_reg_ccorres:
            (doMachineOp (writeVCPUHardwareReg r v))
            (Call vcpu_hw_write_reg_'proc)"
 
-(* FIXME AARCH64 these were RISCV64 machine op ccorres assumptions, remove after we have new ones
-assumes hwASIDFlush_ccorres:
-  "ccorres dc xfdc \<top> (\<lbrace>\<acute>asid___unsigned_long = asid\<rbrace>) []
-           (doMachineOp (AARCH64.hwASIDFlush asid))
-           (Call hwASIDFlush_'proc)"
-
-*)
-
 (* The following are fastpath specific assumptions.
    We might want to move them somewhere else. *)
 

proof/crefine/AARCH64/Recycle_C.thy

@@ -571,59 +571,6 @@ lemma page_table_at_rf_sr_dom_s:
   apply (auto simp add: intvl_def shiftl_t2n pte_bits_def word_size_bits_def)[1]
   done
 
-(* FIXME AARCH64 this currently doesn't make sense, update when going through Arch_C so that it's at
-   least useful
-   clearMemory corresponds to clearMemory on the Haskell side, and that contains a cleanCacheRange_RAM
-lemma clearMemory_setObject_PTE_ccorres:
-  "ccorres dc xfdc (page_table_at' pt_t ptr
-                and (\<lambda>s. 2 ^ (ptBits pt_t) \<le> gsMaxObjectSize s)
-                and (\<lambda>_. is_aligned ptr (ptBits pt_t) \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr))
-            (UNIV \<inter> {s. ptr___ptr_to_unsigned_long_' s = Ptr ptr} \<inter> {s. bits_' s = of_nat (ptBits pt_t)}) []
-       (do mapM_x (\<lambda>a. setObject a AARCH64_H.InvalidPTE)
-                        [ptr , ptr + 2 ^ objBits AARCH64_H.InvalidPTE .e. ptr + 2 ^ (ptBits pt_t) - 1];
-           cleanCacheRange_RAM ???
-        od)
-       (Call clearMemory_'proc)"
-  apply (rule ccorres_gen_asm)+
-  apply (cinit' lift: ptr___ptr_to_unsigned_long_' bits_')
-   apply (rule ccorres_Guard_Seq)
-
-
-   apply (rule_tac P="page_table_at' pt_t ptr and (\<lambda>s. 2 ^ (ptBits pt_t) \<le> gsMaxObjectSize s)"
-               in ccorres_from_vcg_nofail[where P'=UNIV])
-   apply (rule allI, rule conseqPre, vcg)
-   apply clarsimp
-   apply (subst ghost_assertion_size_logic[unfolded o_def])
-     apply (simp add: bit_simps)
-    apply assumption
-   apply (clarsimp simp: replicateHider_def[symmetric] bit_simps)
-   apply (frule is_aligned_no_overflow', simp)
-   apply (intro conjI)
-      apply (erule is_aligned_weaken, simp)
-     apply (clarsimp simp: is_aligned_def)
-    using page_table_at_rf_sr_dom_s
-    apply (simp add: bit_simps)
-   apply (clarsimp simp add: bit_simps
-                      cong: StateSpace.state.fold_congs globals.fold_congs)
-   apply (simp add: upto_enum_step_def objBits_simps bit_simps add.commute[where b=ptr]
-                    linorder_not_less[symmetric] archObjSize_def
-                    upto_enum_word split_def)
-  apply (erule mapM_x_store_memset_ccorres_assist
-                      [unfolded split_def, OF _ _ _ _ _ _ subset_refl],
-         simp_all add: shiftl_t2n hd_map objBits_simps archObjSize_def bit_simps)[1]
-   apply (rule cmap_relationE1, erule rf_sr_cpte_relation, erule ko_at_projectKO_opt)
-   apply (subst coerce_memset_to_heap_update_pte)
-   apply (clarsimp simp: rf_sr_def Let_def cstate_relation_def typ_heap_simps)
-   apply (rule conjI)
-    apply (simp add: cpspace_relation_def typ_heap_simps update_pte_map_tos
-                     update_pte_map_to_ptes carray_map_relation_upd_triv)
-    apply (rule cmap_relation_updI, simp_all)[1]
-    apply (simp add: cpte_relation_def Let_def pte_lift_def)
-   apply (simp add: carch_state_relation_def cmachine_state_relation_def
-                    update_pte_map_tos)
-  apply simp
-  done *)
-
 lemma ccorres_make_xfdc:
   "ccorresG rf_sr \<Gamma> r xf P P' h a c \<Longrightarrow> ccorresG rf_sr \<Gamma> dc xfdc P P' h a c"
   apply (erule ccorres_rel_imp)

proof/crefine/AARCH64/Retype_C.thy

@@ -35,14 +35,6 @@ lemma sle_positive: "\<lbrakk> b < 0x8000000000000000; (a :: machine_word) \<le>
   apply (clarsimp simp:word_le_def)
   done
 
-lemma sless_positive: "\<lbrakk> b < 0x8000000000000000; (a :: machine_word) < b \<rbrakk> \<Longrightarrow> a <s b"
-  apply (clarsimp simp: word_sless_def)
-  apply (rule conjI)
-   apply (erule sle_positive)
-   apply simp
-  apply simp
-  done
-
 lemma zero_le_sint: "\<lbrakk> 0 \<le> (a :: machine_word); a < 0x8000000000000000 \<rbrakk> \<Longrightarrow> 0 \<le> sint a"
   apply (subst sint_eq_uint)
    apply (simp add:unat_less_helper)
@@ -51,7 +43,6 @@ lemma zero_le_sint: "\<lbrakk> 0 \<le> (a :: machine_word); a < 0x80000000000000
 
 context begin interpretation Arch . (*FIXME: arch_split*)
 
-(* FIXME AARCH64 we have multiple page table index sizes *)
 lemma map_option_byte_to_word_heap:
   assumes disj: "\<And>(off :: 9 word) x. x<8 \<Longrightarrow> p + ucast off * 8 + x \<notin> S " (*9=page table index*)
   shows "byte_to_word_heap (\<lambda>x. if x \<in> S then 0 else mem x) p
@@ -5844,8 +5835,6 @@ lemma updatePTType_ccorres:
   apply (clarsimp simp: cvariable_array_map_relation_def split: if_splits)
   done
 
-(* FIXME AARCH64 multiple issues in vspace objects, possibly missing ghost state updates, and
-   page table ghost state in state relation *)
 lemma Arch_createObject_ccorres:
   assumes t: "toAPIType newType = None"
   shows "ccorres (\<lambda>a b. ccap_relation (ArchObjectCap a) b) ret__struct_cap_C_'
@@ -5856,7 +5845,6 @@ lemma Arch_createObject_ccorres:
      (Call Arch_createObject_'proc)"
 proof -
   note if_cong[cong]
-  (* FIXME AARCH64 note sign_extend_canonical_address[simp] *)
 
   show ?thesis
     apply (clarsimp simp: createObject_c_preconds_def