minor cleanup

proof/crefine/AARCH64/Fastpath_C.thy

@@ -262,7 +262,6 @@ lemma lookup_fp_ccorres':
       apply (cinitlift cap_' bits_')
       apply (rename_tac cbits ccap)
       apply (elim conjE)
-      (* FIXME AARCH64 64/0x40 is just a guess based on machine_word size *)
       apply (rule_tac F="capCNodePtr_CL (cap_cnode_cap_lift ccap)
                                = capCNodePtr acap
                           \<and> capCNodeGuardSize acap < 64
@@ -542,8 +541,7 @@ lemma ccorres_catch_bindE_symb_exec_l:
   apply clarsimp
   done
 
-(* FIXME AARCH64 wrong name, do we want this or armKSASIDTable? *)
-lemma vcpuSwitch_ksArchState[wp]:
+lemma vcpuSwitch_armKSVMIDTable[wp]:
   "vcpuSwitch v \<lbrace>\<lambda>s. P (armKSVMIDTable (ksArchState s))\<rbrace>"
   by (wpsimp simp: vcpuSwitch_def split_def modifyArchState_def)
 
@@ -2784,8 +2782,8 @@ proof -
        apply (rename_tac msginfo' cptr')
        apply (rule_tac P="msginfo' = msginfo \<and> cptr' = cptr" in ccorres_gen_asm)
        (* the call_ignore_cong in this proof is required to prevent corruption of arguments in
-          endpoint_ptr_mset_epQueue_tail_state_'proc so that eventually fastpath_dequeue_ccorres
-          can apply  *)
+          endpoint_ptr_mset_epQueue_tail_state_'proc so that eventually fastpath_enqueue_ccorres
+          can apply *)
        apply (simp cong: call_ignore_cong)
        apply (simp only:)
        apply (csymbr, csymbr)
@@ -3087,10 +3085,8 @@ proof -
                             apply (simp add: prio_and_dom_limit_helpers cong: call_ignore_cong)
                             apply (rule ccorres_move_c_guard_tcb)
                             apply (rule ccorres_pre_threadGet)
-                            apply simp (* FIXME AARCH64 we have to do this simp without the
-                              call_ignore_cong, otherwise isHighestPrio_ccorres doesn't work, but
-                              does that ruin later calls? this proof doesn't use fastpath_dequeue_ccorres,
-                              so maybe we don't need these congs at all? *)
+                            apply simp (* we have to do this simp without the call_ignore_cong,
+                                          otherwise isHighestPrio_ccorres's args won't get simplified *)
                             apply (ctac add: isHighestPrio_ccorres)
                               apply (rename_tac highest highest')
                               apply (simp add: to_bool_def cong: call_ignore_cong)
@@ -3173,8 +3169,6 @@ proof -
                                 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2)
                                 apply (rule_tac xf'=xfdc and r'=dc in ccorres_split_nothrow)
                                     apply (rule fastpath_enqueue_ccorres[simplified])
-(* FIXME AARCH64 investigate: can we get rid of the congs in call_ccorres if we use [simplified] on
-the one ccorres rule it affects? *)
                                     apply simp
                                    apply ceqv