arm cspec+crefine: update for iMX8+FPU

Signed-off-by: Rafal Kolanski <[email protected]>

proof/crefine/ARM/ADT_C.thy

@@ -118,36 +118,53 @@ end
 definition
   "register_to_H \<equiv> inv register_from_H"
 
+context state_rel begin
+
 definition
   to_user_context_C :: "user_context \<Rightarrow> user_context_C"
 where
-  "to_user_context_C uc \<equiv> user_context_C (FCP (\<lambda>r. uc (register_to_H (of_nat r))))"
-
-context kernel_m begin
-
-lemma ccontext_rel_to_C:
-  "ccontext_relation uc (to_user_context_C uc)"
-  apply (clarsimp simp: ccontext_relation_def to_user_context_C_def)
-  apply (rule arg_cong [where f=uc])
-  apply (simp add: register_to_H_def inv_def)
-  done
-
-end
+  "to_user_context_C uc \<equiv>
+    user_context_C (ARRAY r. user_regs uc (register_to_H (of_nat r)))
+                   (user_fpu_state_C ((ARRAY r. fpuRegs (fpu_state uc) (finite_index r)))
+                      (fpuExc (fpu_state uc)) (fpuScr (fpu_state uc)))"
 
 definition
   from_user_context_C :: "user_context_C \<Rightarrow> user_context"
 where
-  "from_user_context_C uc \<equiv> \<lambda>r. index (registers_C uc) (unat (register_from_H r))"
+  "from_user_context_C uc \<equiv>
+  UserContext (FPUState (Rep_array (fpregs_C (fpuState_C uc)))
+                        (fpexc_C (fpuState_C uc))
+                        (fpscr_C (fpuState_C uc)))
+              (\<lambda>r. (registers_C uc).[unat (register_from_H r)])"
+
+lemma (in kernel_m) ccontext_rel_to_C:
+  "ccontext_relation uc (to_user_context_C uc)"
+  unfolding ccontext_relation_def to_user_context_C_def cregs_relation_def fpu_relation_def
+  by (clarsimp simp: register_to_H_def inv_def split: fpu_state.splits)
 
 definition
   getContext_C :: "tcb_C ptr \<Rightarrow> cstate \<Rightarrow> user_context"
 where
   "getContext_C thread \<equiv>
    \<lambda>s. from_user_context_C (tcbContext_C (the (clift (t_hrs_' (globals s)) (Ptr &(thread\<rightarrow>[''tcbArch_C''])))))"
 
+lemma fpu_relation_Rep:
+  "fpu_relation fH fC \<Longrightarrow> Rep_array (fpregs_C fC) = fpuRegs fH"
+  unfolding fpu_relation_def index_def
+  apply (clarsimp split: fpu_state.splits)
+  apply (subst (asm) forall_finite_index[where 'a=fpu_regs, symmetric, simplified])
+  by auto
+
 lemma from_user_context_C:
   "ccontext_relation uc uc' \<Longrightarrow> from_user_context_C uc' = uc"
-  by (auto simp: ccontext_relation_def from_user_context_C_def)
+  unfolding ccontext_relation_def cregs_relation_def
+  apply clarsimp
+  apply (frule fpu_relation_Rep)
+  apply (cases uc)
+  apply (auto simp: from_user_context_C_def fpu_relation_def split: fpu_state.splits)
+  done
+
+end
 
 context kernel_m begin
 
@@ -688,9 +705,23 @@ lemma cpspace_cte_relation_unique:
 lemma inj_tcb_ptr_to_ctcb_ptr: "inj tcb_ptr_to_ctcb_ptr"
   by (simp add: inj_on_def tcb_ptr_to_ctcb_ptr_def)
 
+lemma cregs_relation_imp_eq:
+  "cregs_relation f x \<Longrightarrow> cregs_relation g x \<Longrightarrow> f=g"
+  by (auto simp: cregs_relation_def)
+
+lemma fpu_relation_imp_eq:
+  "fpu_relation f x \<Longrightarrow> fpu_relation g x \<Longrightarrow> f=g"
+  unfolding fpu_relation_def index_def
+  apply (clarsimp split: fpu_state.splits)
+  apply (subst (asm) forall_finite_index[where 'a=fpu_regs, symmetric, simplified])+
+  by auto
+
 lemma ccontext_relation_imp_eq:
   "ccontext_relation f x \<Longrightarrow> ccontext_relation g x \<Longrightarrow> f=g"
-  by (rule ext) (simp add: ccontext_relation_def)
+  unfolding ccontext_relation_def
+  apply (cases f, cases g)
+  apply (auto dest: fpu_relation_imp_eq cregs_relation_imp_eq)
+  done
 
 lemma carch_tcb_relation_imp_eq:
   "carch_tcb_relation f x \<Longrightarrow> carch_tcb_relation g x \<Longrightarrow> f = g"
@@ -724,7 +755,7 @@ lemma map_to_ctes_tcb_ctes:
    apply (frule_tac s1=s' in ps_clear_def3[THEN iffD1,rotated 2],
           assumption, simp add: objBits_simps')
    apply (drule (1) ps_clear_16)+
-   apply (simp add: is_aligned_add_helper[of _ 9 "0x10", simplified]
+   apply (simp add: is_aligned_add_helper[of _ 10 "0x10", simplified]
                     split_def objBits_simps')
   apply (rule conjI)
    apply (clarsimp simp: map_to_ctes_def Let_def fun_eq_iff)
@@ -734,7 +765,7 @@ lemma map_to_ctes_tcb_ctes:
    apply (frule_tac s1=s' in ps_clear_def3[THEN iffD1,rotated 2],
           assumption, simp add: objBits_simps')
    apply (drule (1) ps_clear_is_aligned_ctes_None(1))+
-   apply (simp add: is_aligned_add_helper[of _ 9 "0x20", simplified]
+   apply (simp add: is_aligned_add_helper[of _ 10 "0x20", simplified]
                     split_def objBits_simps')
   apply (rule conjI)
    apply (clarsimp simp: map_to_ctes_def Let_def fun_eq_iff)
@@ -744,7 +775,7 @@ lemma map_to_ctes_tcb_ctes:
    apply (frule_tac s1=s' in ps_clear_def3[THEN iffD1,rotated 2],
           assumption, simp add: objBits_simps')
    apply (drule (1) ps_clear_is_aligned_ctes_None(2))+
-   apply (simp add: is_aligned_add_helper[of _ 9 "0x30", simplified]
+   apply (simp add: is_aligned_add_helper[of _ 10 "0x30", simplified]
                     split_def objBits_simps')
   apply (clarsimp simp: map_to_ctes_def Let_def fun_eq_iff)
   apply (drule_tac x="p+0x40" in spec, simp add: objBitsKO_def)
@@ -753,7 +784,7 @@ lemma map_to_ctes_tcb_ctes:
   apply (frule_tac s1=s' in ps_clear_def3[THEN iffD1,rotated 2],
          assumption, simp add: objBits_simps')
   apply (drule (1) ps_clear_is_aligned_ctes_None(3))+
-  apply (simp add: is_aligned_add_helper[of _ 9 "0x40", simplified]
+  apply (simp add: is_aligned_add_helper[of _ 10 "0x40", simplified]
                    split_def objBits_simps')
   done
 
@@ -804,7 +835,7 @@ lemma cpspace_tcb_relation_unique:
    apply (frule ksPSpace_valid_objs_tcbBoundNotification_nonzero[OF vs])
    apply (frule ksPSpace_valid_objs_tcbBoundNotification_nonzero[OF vs'])
    apply (thin_tac "map_to_tcbs x y = Some z" for x y z)+
-   apply (case_tac x, case_tac y, case_tac "the (clift ch (tcb_Ptr (p+0x100)))")
+   apply (case_tac x, case_tac y, case_tac "the (clift ch (tcb_Ptr (p+0x200)))")
    apply (clarsimp simp: ctcb_relation_def ran_tcb_cte_cases)
    apply (clarsimp simp: option_to_ptr_def option_to_0_def split: option.splits)
    apply (auto simp: cfault_rel_imp_eq cthread_state_rel_imp_eq carch_tcb_relation_imp_eq

proof/crefine/ARM/ArchMove_C.thy

@@ -223,7 +223,9 @@ proof -
 qed
 
 lemma user_getreg_rv:
-  "\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb r)) t\<rbrace> asUser t (getRegister r) \<lbrace>\<lambda>rv s. P rv\<rbrace>"
+  "\<lbrace>obj_at' (\<lambda>tcb. P ((user_regs \<circ> atcbContextGet \<circ> tcbArch) tcb r)) t\<rbrace>
+   asUser t (getRegister r)
+   \<lbrace>\<lambda>rv s. P rv\<rbrace>"
   apply (simp add: asUser_def split_def)
   apply (wp threadGet_wp)
   apply (clarsimp simp: obj_at'_def projectKOs getRegister_def in_monad atcbContextGet_def)

proof/crefine/ARM/Arch_C.thy

@@ -1433,6 +1433,10 @@ lemma valid_pde_slots_lift2:
   apply (wp hoare_vcg_ex_lift hoare_vcg_conj_lift | assumption)+
   done
 
+lemma addrFromPPtr_mask_6:
+  "addrFromPPtr ptr && mask (6::nat) = ptr && mask (6::nat)"
+  by (rule addrFromPPtr_mask[where n=6, simplified])
+
 lemma pteCheckIfMapped_ccorres:
   "ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' \<top>
     (UNIV \<inter> {s. pte___ptr_to_struct_pte_C_' s = Ptr slot}) []
@@ -1596,7 +1600,7 @@ lemma performPageInvocationMapPTE_ccorres:
         apply (subst add_diff_eq [symmetric], subst is_aligned_no_wrap', assumption, fastforce)
         apply (simp add:addrFromPPtr_mask_5)
        apply (clarsimp simp:pte_range_relation_def ptr_add_def ptr_range_to_list_def
-                            addrFromPPtr_mask_5)
+                            addrFromPPtr_mask_6)
        apply (auto simp: valid_pte_slots'2_def upt_conv_Cons[where i=0])[1]
       apply (clarsimp simp: guard_is_UNIV_def hd_conv_nth last_conv_nth ucast_minus)
       apply (clarsimp simp: pte_range_relation_def ptr_range_to_list_def objBits_simps archObjSize_def)
@@ -1856,7 +1860,7 @@ lemma performPageInvocationMapPDE_ccorres:
         apply (subst is_aligned_no_wrap', assumption, fastforce)
         apply (simp add:addrFromPPtr_mask_5)
        apply (clarsimp simp: pde_range_relation_def ptr_range_to_list_def CTypesDefs.ptr_add_def
-                             valid_pde_slots'2_def addrFromPPtr_mask_5)
+                             valid_pde_slots'2_def addrFromPPtr_mask_6)
        apply (auto simp: upt_conv_Cons[where i=0])[1]
       apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem hd_conv_nth last_conv_nth)
       apply (clarsimp simp: pde_range_relation_def ptr_range_to_list_def pdeBits_def)
@@ -3141,7 +3145,7 @@ lemma decodeARMPageDirectoryInvocation_ccorres:
               apply (simp add:linorder_not_le)
               apply (erule word_less_sub_1)
              apply (simp add:mask_add_aligned mask_twice)
-            apply (subgoal_tac "5 \<le> pageBitsForSize a")
+            apply (subgoal_tac "6 \<le> pageBitsForSize a")
              apply (frule(1) is_aligned_weaken)
              apply (simp add:mask_add_aligned mask_twice)
              apply (erule order_trans[rotated])

proof/crefine/ARM/CLevityCatch.thy

@@ -62,7 +62,7 @@ declare empty_fail_doMachineOp [simp]
 lemma asUser_get_registers:
   "\<lbrace>tcb_at' target\<rbrace>
      asUser target (mapM getRegister xs)
-   \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. map ((atcbContextGet o tcbArch) tcb) xs = rv) target s\<rbrace>"
+   \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. map ((user_regs \<circ> atcbContextGet \<circ> tcbArch) tcb) xs = rv) target s\<rbrace>"
   apply (induct xs)
    apply (simp add: mapM_empty asUser_return)
    apply wp

proof/crefine/ARM/CSpace_C.thy

@@ -2554,15 +2554,15 @@ definition
     | Some (Cap_endpoint_cap c) \<Rightarrow> 4
     | Some (Cap_notification_cap c) \<Rightarrow> 4
     | Some (Cap_cnode_cap c) \<Rightarrow> unat (capCNodeRadix_CL c) + 4
-    | Some (Cap_thread_cap c) \<Rightarrow> 9
+    | Some (Cap_thread_cap c) \<Rightarrow> 10
     | Some (Cap_small_frame_cap c) \<Rightarrow> 12
     | Some (Cap_frame_cap c) \<Rightarrow> pageBitsForSize (gen_framesize_to_H $ generic_frame_cap_get_capFSize_CL cap)
     | Some (Cap_page_table_cap c) \<Rightarrow> 10
     | Some (Cap_page_directory_cap c) \<Rightarrow> 14
     | Some (Cap_asid_pool_cap c) \<Rightarrow> asidLowBits + 2
     | Some (Cap_zombie_cap c) \<Rightarrow>
         let type = cap_zombie_cap_CL.capZombieType_CL c in
-        if isZombieTCB_C type then 9 else unat (type && mask 5) + 4
+        if isZombieTCB_C type then 10 else unat (type && mask 5) + 4
     | _ \<Rightarrow> 0"
 
 lemma generic_frame_cap_size[simp]:

proof/crefine/ARM/Fastpath_C.thy

@@ -1574,7 +1574,7 @@ lemma ctes_of_Some_cte_wp_at:
   by (clarsimp simp: cte_wp_at_ctes_of)
 
 lemma user_getreg_wp:
-  "\<lbrace>\<lambda>s. tcb_at' t s \<and> (\<forall>rv. obj_at' (\<lambda>tcb. (atcbContextGet o tcbArch) tcb r = rv) t s \<longrightarrow> Q rv s)\<rbrace>
+  "\<lbrace>\<lambda>s. tcb_at' t s \<and> (\<forall>rv. obj_at' (\<lambda>tcb. (user_regs o atcbContextGet o tcbArch) tcb r = rv) t s \<longrightarrow> Q rv s)\<rbrace>
       asUser t (getRegister r) \<lbrace>Q\<rbrace>"
   apply (rule_tac Q="\<lambda>rv s. \<exists>rv'. rv' = rv \<and> Q rv' s" in hoare_post_imp)
    apply simp
@@ -1698,8 +1698,8 @@ lemma fastpath_call_ccorres:
   notes hoare_TrueI[simp]
   shows "ccorres dc xfdc
      (\<lambda>s. invs' s \<and> ct_in_state' ((=) Running) s
-                  \<and> obj_at' (\<lambda>tcb. (atcbContextGet o tcbArch) tcb ARM_H.capRegister = cptr
-                                 \<and>  (atcbContextGet o tcbArch) tcb ARM_H.msgInfoRegister = msginfo)
+                  \<and> obj_at' (\<lambda>tcb. (user_regs o atcbContextGet o tcbArch) tcb ARM_H.capRegister = cptr
+                                 \<and>  (user_regs o atcbContextGet o tcbArch) tcb ARM_H.msgInfoRegister = msginfo)
                         (ksCurThread s) s)
      (UNIV \<inter> {s. cptr_' s = cptr} \<inter> {s. msgInfo_' s = msginfo}) []
      (fastpaths SysCall) (Call fastpath_call_'proc)"
@@ -2514,8 +2514,8 @@ lemma fastpath_reply_recv_ccorres:
   notes hoare_TrueI[simp]
   shows "ccorres dc xfdc
        (\<lambda>s. invs' s \<and> ct_in_state' ((=) Running) s
-               \<and> obj_at' (\<lambda>tcb.  (atcbContextGet o tcbArch) tcb capRegister = cptr
-                              \<and>  (atcbContextGet o tcbArch) tcb msgInfoRegister = msginfo)
+               \<and> obj_at' (\<lambda>tcb.  (user_regs o atcbContextGet o tcbArch) tcb capRegister = cptr
+                              \<and>  (user_regs o atcbContextGet o tcbArch) tcb msgInfoRegister = msginfo)
                      (ksCurThread s) s)
        (UNIV \<inter> {s. cptr_' s = cptr} \<inter> {s. msgInfo_' s = msginfo}) []
        (fastpaths SysReplyRecv) (Call fastpath_reply_recv_'proc)"

proof/crefine/ARM/Fastpath_Equiv.thy

@@ -248,7 +248,7 @@ lemma ctes_of_Some_cte_wp_at:
   by (clarsimp simp: cte_wp_at_ctes_of)
 
 lemma user_getreg_wp:
-  "\<lbrace>\<lambda>s. tcb_at' t s \<and> (\<forall>rv. obj_at' (\<lambda>tcb. (atcbContextGet o tcbArch) tcb r = rv) t s \<longrightarrow> Q rv s)\<rbrace>
+  "\<lbrace>\<lambda>s. tcb_at' t s \<and> (\<forall>rv. obj_at' (\<lambda>tcb. (user_regs \<circ> atcbContextGet \<circ> tcbArch) tcb r = rv) t s \<longrightarrow> Q rv s)\<rbrace>
       asUser t (getRegister r) \<lbrace>Q\<rbrace>"
   apply (rule_tac Q="\<lambda>rv s. \<exists>rv'. rv' = rv \<and> Q rv' s" in hoare_post_imp)
    apply simp
@@ -1069,7 +1069,7 @@ lemma setEndpoint_setCTE_pivot[unfolded K_bind_def]:
                  setEndpoint_typ_at'[where T="koType TYPE(cte)", unfolded typ_at_to_obj_at']
                      | simp)+
       apply (rule_tac P="\<lambda>s. epat = ep_at' p s \<and> cteat = real_cte_at' slot s
-                           \<and> tcbat = (tcb_at' (slot && ~~ mask 9) and (%y. slot && mask 9 : dom tcb_cte_cases)) s"
+                           \<and> tcbat = (tcb_at' (slot && ~~ mask 10) and (%y. slot && mask 10 : dom tcb_cte_cases)) s"
                    in monadic_rewrite_pre_imp_eq)
       apply (simp add: setEndpoint_def setObject_modify_assert bind_assoc
                        exec_gets assert_def exec_modify
@@ -1159,7 +1159,7 @@ lemma set_setCTE[unfolded K_bind_def]:
    apply (rule monadic_rewrite_transverse, rule monadic_rewrite_add_gets,
           rule monadic_rewrite_bind_tail)
     apply (rule monadic_rewrite_trans,
-           rule_tac f="tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)"
+           rule_tac f="tcb_at' (p && ~~ mask 10) and K (p && mask 10 \<in> dom tcb_cte_cases)"
                   in monadic_rewrite_add_gets)
     apply (rule monadic_rewrite_transverse, rule monadic_rewrite_add_gets,
            rule monadic_rewrite_bind_tail)
@@ -1176,7 +1176,7 @@ lemma set_setCTE[unfolded K_bind_def]:
      apply (rule monadic_rewrite_bind_tail)+
        apply (rule_tac P="c = cteat \<and> t = tcbat
                            \<and> (tcbat \<longrightarrow>
-                                 (\<exists> getF setF. tcb_cte_cases (p && mask 9) = Some (getF, setF)
+                                 (\<exists> getF setF. tcb_cte_cases (p && mask 10) = Some (getF, setF)
                                         \<and> (\<forall> f g tcb. setF f (setF g tcb) = setF (f o g) tcb)))"
                    in monadic_rewrite_gen_asm)
        apply (rule monadic_rewrite_is_refl[OF ext])

proof/crefine/ARM/Finalise_C.thy

@@ -2003,13 +2003,32 @@ lemma ccap_relation_IRQHandler_mask:
   apply (simp add: c_valid_cap_def cap_irq_handler_cap_lift cl_valid_cap_def)
   done
 
-lemma prepare_thread_delete_ccorres:
-  "ccorres dc xfdc \<top> UNIV []
+lemma fpuThreadDelete_ccorres:
+  "ccorres dc xfdc
+     (invs' and tcb_at' thread)
+     (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) hs
+   (fpuThreadDelete thread) (Call fpuThreadDelete_'proc)"
+  supply Collect_const[simp del] dc_simp[simp del]
+  apply (cinit lift: thread_')
+   apply clarsimp
+   apply (ctac (no_vcg) add: nativeThreadUsingFPU_ccorres)
+    apply clarsimp
+    apply (rule ccorres_when[where R=\<top>])
+     apply fastforce
+    apply (ctac add: switchFpuOwner_ccorres)
+   apply wpsimp
+  apply fastforce
+  done
+
+lemma prepareThreadDelete_ccorres:
+  "ccorres dc xfdc
+     (invs' and tcb_at' thread)
+     (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) hs
    (prepareThreadDelete thread) (Call Arch_prepareThreadDelete_'proc)"
-  unfolding prepareThreadDelete_def
-  apply (rule ccorres_Call)
-  apply (rule Arch_prepareThreadDelete_impl[unfolded Arch_prepareThreadDelete_body_def])
-  apply (rule ccorres_return_Skip)
+  supply dc_simp[simp del]
+  apply (cinit lift: thread_', rename_tac cthread)
+   apply (ctac add: fpuThreadDelete_ccorres)
+  apply fastforce
   done
 
 lemma finaliseCap_ccorres:
@@ -2112,7 +2131,7 @@ lemma finaliseCap_ccorres:
     apply csymbr
     apply (ctac(no_vcg) add: unbindNotification_ccorres)
      apply (ctac(no_vcg) add: suspend_ccorres[OF cteDeleteOne_ccorres])
-     apply (ctac(no_vcg) add: prepare_thread_delete_ccorres)
+     apply (ctac(no_vcg) add: prepareThreadDelete_ccorres)
       apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV])
       apply (rule allI, rule conseqPre, vcg)
       apply (clarsimp simp: word_sle_def return_def)
@@ -2182,14 +2201,15 @@ lemma finaliseCap_ccorres:
    apply (simp add: guard_is_UNIV_def)
   apply (clarsimp simp: cap_get_tag_isCap word_sle_def Collect_const_mem)
   apply (intro impI conjI)
-             apply (clarsimp split: bool.splits)
-            apply (clarsimp split: bool.splits)
-           apply (clarsimp simp: valid_cap'_def isCap_simps)
+               apply (clarsimp split: bool.splits)
+              apply (clarsimp split: bool.splits)
+             apply (clarsimp simp: valid_cap'_def isCap_simps)
+            apply (clarsimp simp: isCap_simps capRange_def capAligned_def)
+           apply (clarsimp simp: isCap_simps valid_cap'_def)
           apply (clarsimp simp: isCap_simps capRange_def capAligned_def)
-         apply (clarsimp simp: isCap_simps valid_cap'_def)
-        apply (clarsimp simp: isCap_simps valid_cap'_def)
-       apply (clarsimp simp: isCap_simps valid_cap'_def)
-      apply (clarsimp simp: isCap_simps valid_cap'_def )
+         apply (clarsimp simp: isCap_simps valid_cap'_def )
+        apply clarsimp
+       apply (clarsimp simp: isCap_simps valid_cap'_def )
       apply (clarsimp simp: tcb_ptr_to_ctcb_ptr_def ccap_relation_def isCap_simps
                             c_valid_cap_def cap_thread_cap_lift_def cap_to_H_def
                             ctcb_ptr_to_tcb_ptr_def Let_def

proof/crefine/ARM/Interrupt_C.thy

@@ -371,7 +371,7 @@ lemma isIRQActive_ccorres:
         (isIRQActive irq) (Call isIRQActive_'proc)"
   apply (cinit lift: irq_')
    apply (simp add: getIRQState_def getInterruptState_def)
-   apply (rule_tac P="irq \<le> ucast Kernel_C.maxIRQ \<and> unat irq < (160::nat)" in ccorres_gen_asm)
+   apply (rule_tac P="irq \<le> ucast Kernel_C.maxIRQ \<and> unat irq < (161::nat)" in ccorres_gen_asm)
    apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV])
    apply (rule allI, rule conseqPre, vcg)
    apply (clarsimp simp: simpler_gets_def word_sless_msb_less maxIRQ_def

proof/crefine/ARM/Invoke_C.thy

@@ -1949,7 +1949,7 @@ lemma resetUntypedCap_ccorres:
              apply (simp add: is_aligned_def addr_card_def card_word)
              apply clarsimp
 
-            apply (rule conseqPre, vcg exspec=cleanCacheRange_RAM_preserves_bytes
+            apply (rule conseqPre, vcg exspec=cleanCacheRange_PoC_preserves_bytes exspec=cleanCacheRange_RAM_preserves_bytes
               exspec=preemptionPoint_modifies)
             apply (clarsimp simp: in_set_conv_nth isCap_simps
                                   length_upto_enum_step upto_enum_step_nth
@@ -1972,7 +1972,6 @@ lemma resetUntypedCap_ccorres:
                                   is_aligned_add_multI conj_comms
                                   region_actually_is_bytes_def)
             apply (simp add: Kernel_Config.resetChunkBits_def is_aligned_def)
-
            apply (rule hoare_pre)
             apply (wp updateFreeIndex_cte_wp_at updateFreeIndex_clear_invs'
                       updateFreeIndex_pspace_no_overlap'