arm refine: update for iMX8+FPU

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

proof/refine/ARM/CNodeInv_R.thy

@@ -627,7 +627,7 @@ lemma prepareThreadDelete_ctes_of_thread:
   "\<lbrace>\<lambda>s. \<exists>node. ctes_of s x = Some (CTE (ThreadCap t) node)\<rbrace>
      prepareThreadDelete t
    \<lbrace>\<lambda>rv s. \<exists>node. ctes_of s x = Some (CTE (ThreadCap t) node)\<rbrace>"
-  by (wpsimp simp: prepareThreadDelete_def)
+  by (wpsimp simp: prepareThreadDelete_def fpuThreadDelete_def)
 
 lemma suspend_not_recursive_ctes:
   "\<lbrace>\<lambda>s. P (not_recursive_ctes s)\<rbrace>
@@ -655,9 +655,7 @@ lemma prepareThreadDelete_not_recursive_ctes:
   "\<lbrace>\<lambda>s. P (not_recursive_ctes s)\<rbrace>
      prepareThreadDelete t
    \<lbrace>\<lambda>rv s. P (not_recursive_ctes s)\<rbrace>"
-  apply (simp only: prepareThreadDelete_def cteCaps_of_def)
-  apply wp
-  done
+  by (wpsimp simp: prepareThreadDelete_def fpuThreadDelete_def not_recursive_ctes_def cteCaps_of_def)
 
 definition
   finaliseSlot_recset :: "((word32 \<times> bool \<times> kernel_state) \<times> (word32 \<times> bool \<times> kernel_state)) set"
@@ -5237,6 +5235,11 @@ lemma invalid_Thread_CNode:
   apply (clarsimp simp: obj_at'_def projectKOs)
   done
 
+(* FIXME MOVE *)
+lemma all_Not_False[simp]:
+  "All Not = False"
+  by blast
+
 lemma Final_notUntyped_capRange_disjoint:
   "\<lbrakk> isFinal cap sl (cteCaps_of s); cteCaps_of s sl' = Some cap';
       sl \<noteq> sl'; capUntypedPtr cap = capUntypedPtr cap'; capBits cap = capBits cap';
@@ -5251,22 +5254,12 @@ lemma Final_notUntyped_capRange_disjoint:
   apply (elim disjE isCapDs[elim_format])
    apply (clarsimp simp: valid_cap'_def
                          obj_at'_def projectKOs objBits_simps'
-                         typ_at'_def ko_wp_at'_def
+                         typ_at'_def ko_wp_at'_def 
+                         page_table_at'_def page_directory_at'_def
+                         sameObjectAs_def3 isCap_simps
                   split: capability.split_asm zombie_type.split_asm
-                         arch_capability.split_asm
-                  dest!: spec[where x=0])
-     apply (clarsimp simp: sameObjectAs_def3 isCap_simps)
-    apply (simp add: isCap_simps)
-   apply (simp add: isCap_simps)
-  apply (clarsimp simp: valid_cap'_def
-                        obj_at'_def projectKOs objBits_simps
-                        typ_at'_def ko_wp_at'_def
-                        page_table_at'_def page_directory_at'_def
-                 split: capability.split_asm zombie_type.split_asm
-                        arch_capability.split_asm
-                 dest!: spec[where x=0])
-    apply fastforce+
-  apply (clarsimp simp: isCap_simps sameObjectAs_def3)
+                         arch_capability.split_asm option.split_asm
+                  dest!: spec[where x=0])+
   done
 
 lemma capBits_capUntyped_capRange:
@@ -8779,6 +8772,7 @@ crunch irq_states' [wp]: finaliseCap valid_irq_states'
        no_irq_invalidateLocalTLB_ASID no_irq_setHardwareASID
        no_irq_set_current_pd no_irq_invalidateLocalTLB_VAASID
        no_irq_cleanByVA_PoU
+       no_irq_switchFpuOwner no_irq_nativeThreadUsingFPU
    simp: crunch_simps armv_contextSwitch_HWASID_def o_def setCurrentPD_to_abs)
 
 lemma finaliseSlot_IRQInactive':

proof/refine/ARM/Finalise_R.thy

@@ -2721,9 +2721,29 @@ lemma unbindMaybeNotification_tcb_at'[wp]:
   apply (wp gbn_wp' | wpc | simp)+
   done
 
+lemma dmo_nativeThreadUsingFPU_invs'[wp]:
+  "\<lbrace>invs'\<rbrace> doMachineOp (nativeThreadUsingFPU thread) \<lbrace>\<lambda>_. invs'\<rbrace>"
+  apply (wp dmo_invs' no_irq_nativeThreadUsingFPU no_irq)
+  apply clarsimp
+  apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = underlying_memory m p"
+         in use_valid[where P=P and Q="\<lambda>_. P" for P])
+    apply (simp add: nativeThreadUsingFPU_def machine_op_lift_def
+                     machine_rest_lift_def split_def | wp)+
+  done
+
+lemma dmo_switchFpuOwner_invs'[wp]:
+  "\<lbrace>invs'\<rbrace> doMachineOp (switchFpuOwner thread cpu) \<lbrace>\<lambda>_. invs'\<rbrace>"
+  apply (wp dmo_invs' no_irq_switchFpuOwner no_irq)
+  apply clarsimp
+  apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = underlying_memory m p"
+         in use_valid[where P=P and Q="\<lambda>_. P" for P])
+    apply (simp add: switchFpuOwner_def machine_op_lift_def
+                     machine_rest_lift_def split_def | wp)+
+  done
+
 crunch cte_wp_at'[wp]: prepareThreadDelete "cte_wp_at' P p"
 crunch valid_cap'[wp]: prepareThreadDelete "valid_cap' cap"
-crunch invs[wp]: prepareThreadDelete "invs'"
+crunch invs[wp]: prepareThreadDelete "invs'" (ignore: doMachineOp)
 
 end
 

proof/refine/ARM/Invariants_H.thy

@@ -2162,7 +2162,7 @@ lemma cte_wp_at_cases':
    apply (erule is_aligned_no_wrap')
     apply (simp add: word_bits_conv)
    apply (simp add: tcb_cte_cases_def split: if_split_asm)
-  apply (subgoal_tac "(p - n) + n \<le> (p - n) + 511")
+  apply (subgoal_tac "(p - n) + n \<le> (p - n) + 0x3FF")
    apply (simp add: field_simps)
   apply (rule word_plus_mono_right)
    apply (simp add: tcb_cte_cases_def split: if_split_asm)

proof/refine/ARM/IpcCancel_R.thy

@@ -1439,10 +1439,37 @@ lemma (in delete_one) suspend_corres:
   apply (clarsimp simp add: invs'_def valid_state'_def valid_queues_inQ_queues)
   done
 
+lemma no_fail_switchFpuOwner[wp]:
+  "no_fail \<top> (ARM.switchFpuOwner thread cpu)"
+  by (simp add: ARM.switchFpuOwner_def Arch.no_fail_machine_op_lift)
+
+lemma no_fail_nativeThreadUsingFPU[wp]:
+  "no_fail \<top> (ARM.nativeThreadUsingFPU thread)"
+  unfolding ARM.nativeThreadUsingFPU_def
+  by (wpsimp wp: no_fail_bind Arch.no_fail_machine_op_lift)
+
 lemma (in delete_one) prepareThreadDelete_corres:
   "corres dc (tcb_at t) (tcb_at' t)
         (prepare_thread_delete t) (ArchRetypeDecls_H.ARM_H.prepareThreadDelete t)"
-  by (simp add: ArchVSpace_A.ARM_A.prepare_thread_delete_def ArchRetype_H.ARM_H.prepareThreadDelete_def)
+ apply (simp add: ArchVSpace_A.ARM_A.prepare_thread_delete_def ArchRetype_H.ARM_H.prepareThreadDelete_def
+                   ArchVSpace_A.ARM_A.fpu_thread_delete_def ArchRetype_H.ARM_H.fpuThreadDelete_def
+                   ARM_H.fromPPtr_def)
+  apply (rule corres_guard_imp)
+    apply (rule corres_split[where r'="(=)"])
+       apply (rule corres_machine_op)
+       apply (rule corres_Id, rule refl, simp)
+       apply wpsimp
+      apply (rule corres_when)
+       apply clarsimp
+      apply wpsimp
+      apply (rule corres_machine_op)
+      apply (rule corres_Id, rule refl, simp)
+      apply wpsimp
+     apply clarsimp
+     apply wpsimp
+    apply wpsimp
+   apply auto
+  done
 
 lemma no_refs_simple_strg':
   "st_tcb_at' simple' t s' \<and> P {} \<longrightarrow> st_tcb_at' (\<lambda>st. P (tcb_st_refs_of' st)) t s'"
@@ -2668,6 +2695,8 @@ lemma suspend_unqueued:
     apply wp+
   done
 
+crunch unqueued: fpuThreadDelete "obj_at' (Not \<circ> tcbQueued) t"
+  (simp: comp_def)
 crunch unqueued: prepareThreadDelete "obj_at' (Not \<circ> tcbQueued) t"
 crunch inactive: prepareThreadDelete "st_tcb_at' ((=) Inactive) t'"
 crunch nonq: prepareThreadDelete " \<lambda>s. \<forall>d p. t' \<notin> set (ksReadyQueues s (d, p))"

proof/refine/ARM/KHeap_R.thy

@@ -608,8 +608,8 @@ lemma cte_wp_at_ctes_of:
    apply (simp add: field_simps)
   apply (clarsimp split: if_split_asm del: disjCI)
    apply (simp add: ps_clear_def3 field_simps)
-  apply (rule disjI2, rule exI[where x="p - (p && ~~ mask 9)"])
-  apply (clarsimp simp: ps_clear_def3[where na=9] is_aligned_mask
+  apply (rule disjI2, rule exI[where x="p - (p && ~~ mask tcb_bits)"])
+  apply (clarsimp simp: ps_clear_def3[where na=tcb_bits] is_aligned_mask
                         word_bw_assocs field_simps)
   done
 

proof/refine/ARM/Retype_R.thy

@@ -2422,7 +2422,7 @@ lemma other_objs_default_relation:
                         default_ep_def makeObject_endpoint default_notification_def
                         makeObject_notification default_ntfn_def
                         fault_rel_optionation_def
-                        initContext_def
+                        initContext_def newFPUState_def
                         arch_tcb_context_get_def atcbContextGet_def
                         default_arch_tcb_def newArchTCB_def
                         arch_tcb_relation_def

proof/refine/ARM/TcbAcc_R.thy

@@ -3213,6 +3213,18 @@ lemmas msgRegisters_unfold
          unfolded fromEnum_def enum_register, simplified,
          unfolded toEnum_def enum_register, simplified]
 
+lemma thread_get_registers:
+  "thread_get (arch_tcb_get_registers \<circ> tcb_arch) t = as_user t (gets user_regs)"
+  apply (simp add: thread_get_def as_user_def arch_tcb_get_registers_def
+                   arch_tcb_context_get_def arch_tcb_context_set_def)
+  apply (rule bind_cong [OF refl])
+  apply (clarsimp simp: gets_the_member)
+  apply (simp add: get_def the_run_state_def set_object_def get_object_def
+                   put_def bind_def return_def gets_def)
+  apply (drule get_tcb_SomeD)
+  apply (clarsimp simp: map_upd_triv select_f_def image_def return_def)
+  done
+
 lemma getMRs_corres:
   "corres (=) (tcb_at t)
               (tcb_at' t and case_option \<top> valid_ipc_buffer_ptr' buf)
@@ -3222,8 +3234,7 @@ lemma getMRs_corres:
     by (simp add: gets_def)
   have T: "corres (\<lambda>con regs. regs = map con msg_registers) (tcb_at t) (tcb_at' t)
      (thread_get (arch_tcb_get_registers o tcb_arch) t) (asUser t (mapM getRegister ARM_H.msgRegisters))"
-    unfolding arch_tcb_get_registers_def
-    apply (subst thread_get_as_user)
+    apply (subst thread_get_registers)
     apply (rule asUser_corres')
     apply (subst mapM_gets)
      apply (simp add: getRegister_def)
@@ -3302,14 +3313,37 @@ lemma storeWordUser_valid_ipc_buffer_ptr' [wp]:
   unfolding valid_ipc_buffer_ptr'_def2
   by (wp hoare_vcg_all_lift storeWordUser_typ_at')
 
+lemma thread_set_as_user_registers:
+  "thread_set (\<lambda>tcb. tcb \<lparr> tcb_arch := arch_tcb_set_registers (f (arch_tcb_get_registers (tcb_arch tcb)))
+                          (tcb_arch tcb) \<rparr>) t
+    = as_user t (modify (modify_registers f))"
+proof -
+  have P: "\<And>f. det (modify f)"
+    by (simp add: modify_def)
+  thus ?thesis
+    apply (simp add: as_user_def P thread_set_def)
+    apply (clarsimp simp: select_f_def simpler_modify_def bind_def image_def modify_registers_def
+                          arch_tcb_set_registers_def arch_tcb_get_registers_def
+                          arch_tcb_context_set_def arch_tcb_context_get_def)
+    done
+qed
+
+lemma UserContext_fold:
+  "UserContext (fpu_state s) (foldl (\<lambda>s (x, y). s(x := y)) (user_regs s) xs) =
+   foldl (\<lambda>s (r, v). UserContext (fpu_state s) ((user_regs s)(r := v))) s xs"
+  apply (induct xs arbitrary: s; simp)
+  apply (clarsimp split: prod.splits)
+  by (metis user_context.sel(1) user_context.sel(2))
+
 lemma setMRs_corres:
   assumes m: "mrs' = mrs"
   shows
   "corres (=) (tcb_at t and case_option \<top> in_user_frame buf)
               (tcb_at' t and case_option \<top> valid_ipc_buffer_ptr' buf)
               (set_mrs t buf mrs) (setMRs t buf mrs')"
 proof -
-  have setRegister_def2: "setRegister = (\<lambda>r v. modify (\<lambda>s. s ( r := v )))"
+  have setRegister_def2:
+    "setRegister = (\<lambda>r v.  modify (\<lambda>s. UserContext (fpu_state s) ((user_regs s)(r := v))))"
     by ((rule ext)+, simp add: setRegister_def)
 
   have S: "\<And>xs ys n m. m - n \<ge> length xs \<Longrightarrow> (zip xs (drop n (take m ys))) = zip xs (drop n ys)"
@@ -3323,34 +3357,33 @@ proof -
 
   show ?thesis using m
     unfolding setMRs_def set_mrs_def
-    apply (clarsimp simp: arch_tcb_set_registers_def arch_tcb_get_registers_def cong: option.case_cong split del: if_split)
+    apply (clarsimp  cong: option.case_cong split del: if_split)
     apply (subst bind_assoc[symmetric])
     apply (fold thread_set_def[simplified])
-    apply (subst thread_set_as_user[where f="\<lambda>context. \<lambda>reg.
-                      if reg \<in> set (take (length mrs) msg_registers)
-                      then mrs ! (the_index msg_registers reg) else context reg",simplified])
+    apply (subst thread_set_as_user_registers)
     apply (cases buf)
-     apply (clarsimp simp: msgRegisters_unfold setRegister_def2 zipWithM_x_Nil zipWithM_x_modify
+     apply (clarsimp simp: msgRegisters_unfold setRegister_def2 zipWithM_x_modify
                            take_min_len zip_take_triv2 min.commute)
      apply (rule corres_guard_imp)
-       apply (rule corres_split_nor[OF asUser_corres'])
+       apply (rule corres_split_nor [OF asUser_corres'])
           apply (rule corres_modify')
-           apply (fastforce simp: fold_fun_upd[symmetric] msgRegisters_unfold
+           apply (fastforce simp: fold_fun_upd[symmetric] msgRegisters_unfold UserContext_fold
+                                  modify_registers_def
                             cong: if_cong simp del: the_index.simps)
           apply ((wp |simp)+)[6]
     \<comment> \<open>buf = Some a\<close>
     using if_split[split del]
-    apply (clarsimp simp: msgRegisters_unfold setRegister_def2 zipWithM_x_Nil zipWithM_x_modify
+    apply (clarsimp simp: msgRegisters_unfold setRegister_def2 zipWithM_x_modify
                           take_min_len zip_take_triv2 min.commute
                           msgMaxLength_def msgLengthBits_def)
     apply (simp add: msg_max_length_def)
     apply (rule corres_guard_imp)
       apply (rule corres_split_nor[OF asUser_corres'])
          apply (rule corres_modify')
           apply (simp only: msgRegisters_unfold cong: if_cong)
-          apply (fastforce simp: fold_fun_upd[symmetric])
+          apply (fastforce simp: fold_fun_upd[symmetric] modify_registers_def UserContext_fold)
          apply clarsimp
-         apply (rule corres_split_nor)
+        apply (rule corres_split_nor)
            apply (rule_tac S="{((x, y), (x', y')). y = y' \<and> x' = (a + (of_nat x * 4)) \<and> x < unat max_ipc_words}"
                         in zipWithM_x_corres)
                apply (fastforce intro: storeWordUser_corres)