Add GIC v3 support for AArch64 platforms

proof/crefine/AARCH64/ADT_C.thy

@@ -624,7 +624,7 @@ lemma carch_state_to_H_correct:
    apply (simp add: ccur_vcpu_to_H_correct)
   apply (rule conjI)
   using valid[simplified valid_arch_state'_def]
-   apply (clarsimp simp: max_armKSGICVCPUNumListRegs_def unat_of_nat_eq)
+   apply (clarsimp simp: max_armKSGICVCPUNumListRegs_val unat_of_nat_eq)
   apply (simp add: pt_t)
   done
 
@@ -1017,7 +1017,7 @@ lemma cpspace_vcpu_relation_unique:
    apply clarsimp
    apply (rule ext)
    apply (rename_tac r)
-   apply (case_tac "64 \<le> r"; simp)
+   apply (case_tac "max_armKSGICVCPUNumListRegs \<le> r"; simp)
   apply (rule conjI)
    apply (rule ext, blast)
   apply (rule conjI, blast)

proof/crefine/AARCH64/Arch_C.thy

@@ -3686,7 +3686,7 @@ lemma invokeVCPUInjectIRQ_ccorres:
   notes Collect_const[simp del]
   shows
   "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
-       (invs' and vcpu_at' vcpuptr and K (idx < 64))
+       (invs' and vcpu_at' vcpuptr and K (idx < max_armKSGICVCPUNumListRegs))
        (UNIV \<inter> \<lbrace>\<acute>vcpu = Ptr vcpuptr \<rbrace>
              \<inter> \<lbrace>\<acute>index = of_nat idx \<rbrace>
              \<inter> \<lbrace> virq_to_H \<acute>virq = virq \<rbrace>)
@@ -3721,7 +3721,7 @@ lemma invokeVCPUInjectIRQ_ccorres:
      apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV])
      apply (rule allI, rule conseqPre, vcg, clarsimp simp: return_def)
     apply wpsimp+
-  apply (clarsimp simp: unat_of_nat_eq word_of_nat_less)
+  apply (clarsimp simp: unat_of_nat_eq word_of_nat_less max_armKSGICVCPUNumListRegs_val)
   apply (rule conjI)
    apply (clarsimp elim: typ_at'_no_0_objD invs_no_0_obj')
   apply (subst scast_eq_ucast; simp?)
@@ -3737,9 +3737,25 @@ lemma virq_virq_pending_EN_new_spec:
        \<lbrace> virqEOIIRQEN_' s = 1 \<longrightarrow> virq_to_H \<acute>ret__struct_virq_C = makeVIRQ (virqGroup_' s) (virqPriority_' s) (virqIRQ_' s) \<rbrace>"
   apply (hoare_rule HoarePartial.ProcNoRec1) (* force vcg to unfold non-recursive procedure *)
   apply vcg
-  apply (clarsimp simp: virq_to_H_def makeVIRQ_def virq_virq_pending_def)
+  (* unfold config to match up with bitfield gen shifts *)
+  apply (clarsimp simp: virq_to_H_def make_virq_def virq_virq_pending_def
+                        Kernel_Config.config_ARM_GIC_V3_def virq_type_shift_def
+                        eoiirqen_shift_def mask_def)
   by (simp add: bit.disj_commute  bit.disj_assoc bit.disj_ac)
 
+lemma virq_virq_active_eq_is_virq_active:
+  "(of_nat (virq_type virq) = (scast virq_virq_active :: machine_word)) = is_virq_active virq"
+  apply (simp add: is_virq_active_def virq_virq_active_def)
+  apply (rule iffI; clarsimp?)
+  apply (clarsimp simp: virq_type_def)
+  done
+
+lemma virq_get_tag_eq_of_nat_virq_type:
+  "virq_get_tag virq = of_nat (virq_type (virq_to_H virq))"
+  (* config unfolding to match bitfield shift in virq_get_tag with virq_type_shift in virq_type *)
+  by (simp add: virq_to_H_def virq_type_def virq_get_tag_def virq_type_shift_def mask_def
+                Kernel_Config.config_ARM_GIC_V3_def)
+
 lemma decodeVCPUInjectIRQ_ccorres:
   notes if_cong[cong] Collect_const[simp del]
   (* csymbr will use this instead now *)
@@ -3807,98 +3823,85 @@ lemma decodeVCPUInjectIRQ_ccorres:
      apply (clarsimp simp: rangeCheck_def not_le[symmetric]
                            liftE_liftM[symmetric] liftE_bindE_assoc)
 
-       (* symbolically execute the gets on LHS *)
-       apply (rule_tac ccorres_pre_gets_armKSGICVCPUNumListRegs_ksArchState,
-              rename_tac nregs)
-
-    apply (rule_tac P="nregs \<le> max_armKSGICVCPUNumListRegs" in ccorres_gen_asm)
-           apply (rule_tac P="nregs \<le> max_armKSGICVCPUNumListRegs"
-                           in ccorres_cross_over_guard_no_st)
-
-       (* unfortunately directly looking at \<acute>gic_vcpu_num_list_regs means we need to abstract the
-          IF condition, and because of 32/64-bit casting we need to know \<le> max_armKSGICVCPUNumListRegs *)
-       apply (rule_tac Q="\<lambda>s. valid_arch_state' s \<and> nregs = armKSGICVCPUNumListRegs (ksArchState s)"
-                   and Q'=UNIV
-                   and C'="{s. of_nat nregs \<le> (args ! 0 >> 32) && 0xFF}"
-                 in ccorres_rewrite_cond_sr_Seq)
-        apply (clarsimp simp: not_le[symmetric] word_le_nat_alt unat_of_nat_eq)
-        apply (simp add: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
-                         valid_arch_state'_def max_armKSGICVCPUNumListRegs_def
-                         unat_of_nat64' unat_of_nat32')
+     (* symbolically execute the gets on LHS *)
+     apply (rule_tac ccorres_pre_gets_armKSGICVCPUNumListRegs_ksArchState,
+            rename_tac nregs)
 
-       apply (rule ccorres_Cond_rhs_Seq)
-        apply (subgoal_tac "(of_nat nregs \<le> (args ! 0 >> 32) && 0xFF)")
-         prefer 2
-  subgoal by (simp add: word_le_nat_alt not_le)
+     apply (rule_tac P="nregs < max_armKSGICVCPUNumListRegs" in ccorres_gen_asm)
+     apply (rule_tac P="nregs < max_armKSGICVCPUNumListRegs" in ccorres_cross_over_guard_no_st)
 
-        apply (simp add: rangeCheck_def not_le[symmetric])
-        apply (simp add: throwError_bind invocationCatch_def
-                   cong: StateSpace.state.fold_congs globals.fold_congs)
+     (* unfortunately directly looking at \<acute>gic_vcpu_num_list_regs means we need to abstract the
+        IF condition, and because of 32/64-bit casting we need to know < max_armKSGICVCPUNumListRegs *)
+     apply (rule_tac Q="\<lambda>s. valid_arch_state' s \<and> nregs = armKSGICVCPUNumListRegs (ksArchState s)"
+                 and Q'=UNIV
+                 and C'="{s. of_nat nregs \<le> (args ! 0 >> 32) && 0xFF}"
+               in ccorres_rewrite_cond_sr_Seq)
+      apply (clarsimp simp: not_le[symmetric] word_le_nat_alt unat_of_nat_eq)
+      apply (simp add: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
+                       valid_arch_state'_def
+                       unat_of_nat64' unat_of_nat32')
+
+     apply (rule ccorres_Cond_rhs_Seq)
+      apply (prop_tac "(of_nat nregs \<le> (args ! 0 >> 32) && 0xFF)")
+       apply (simp add: word_le_nat_alt not_le)
+
+      apply (simp add: rangeCheck_def not_le[symmetric])
+      apply (simp add: throwError_bind invocationCatch_def
+                 cong: StateSpace.state.fold_congs globals.fold_congs)
 
     (* can't use syscall_error_throwError_ccorres_n, since one of the globals updates reads a global
        var itself: gic_vcpu_num_list_regs_', need to split off up to the first return_C else
        vcg barfs *)
-        apply (rule ccorres_split_throws)
-         apply (rule_tac P="\<lambda>s. valid_arch_state' s \<and> nregs = armKSGICVCPUNumListRegs (ksArchState s)"
-                     and P'="UNIV" in ccorres_from_vcg_throws)
-         apply (rule allI, rule conseqPre)
-          apply (vcg exspec=invokeVCPUInjectIRQ_modifies)
-         apply (clarsimp split: prod.splits
-                          simp: throwError_def return_def EXCEPTION_SYSCALL_ERROR_def
-                                EXCEPTION_NONE_def syscall_error_rel_def syscall_error_to_H_def
-                                syscall_error_type_defs)
-         apply (simp add: rf_sr_def cstate_relation_def Let_def carch_state_relation_def)
-        apply (simp add: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
-                         valid_arch_state'_def max_armKSGICVCPUNumListRegs_def
-                         unat_of_nat64' unat_of_nat32')
-        apply vcg
-
-       apply (subgoal_tac "\<not> (of_nat nregs \<le> (args ! 0 >> 32) && 0xFF)")
-        prefer 2
-  subgoal by (simp add: word_le_nat_alt not_le)
-       apply clarsimp
-       apply (rule ccorres_move_const_guard)
-       apply (rule ccorres_move_c_guard_vcpu)
-       apply (simp add: liftM_def)
-       apply (clarsimp simp: rangeCheck_def not_le[symmetric]
-                             liftE_liftM[symmetric] liftE_bindE_assoc)
-
-       apply (rule ccorres_pre_getObject_vcpu, rename_tac vcpu)
-       apply csymbr
-       apply (rule ccorres_abstract_cleanup)
-       apply (simp add: virq_virq_active_def)
-
-(* FIXME AARCH64 cleanup and re-indent needed in this lemma *)
+      apply (rule ccorres_split_throws)
+       apply (rule_tac P="\<lambda>s. valid_arch_state' s \<and> nregs = armKSGICVCPUNumListRegs (ksArchState s)"
+                   and P'="UNIV" in ccorres_from_vcg_throws)
+       apply (rule allI, rule conseqPre)
+        apply (vcg exspec=invokeVCPUInjectIRQ_modifies)
+       apply (clarsimp split: prod.splits
+                        simp: throwError_def return_def EXCEPTION_SYSCALL_ERROR_def
+                              EXCEPTION_NONE_def syscall_error_rel_def syscall_error_to_H_def
+                              syscall_error_type_defs)
+       apply (simp add: rf_sr_def cstate_relation_def Let_def carch_state_relation_def)
+      apply (simp add: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
+                       valid_arch_state'_def not_le
+                       unat_of_nat64' unat_of_nat32')
+      apply vcg
 
-(* FIXME AARCH64 magic numbers: 3 here is the mask in virq_get_virqType, 28 is the shift *)
-       apply (rule_tac
-                P="ret__unsigned_longlong =
-                     (vgicLR (vcpuVGIC vcpu) (unat ((args ! 0 >> 32) && 0xFF)) >> 28) && 3"
-                in ccorres_gen_asm2)
-       apply clarsimp
-       apply (rule ccorres_Cond_rhs_Seq)
-        apply (subgoal_tac "isVIRQActive (vgicLR (vcpuVGIC vcpu) (unat ((args ! 0 >> 32) && 0xFF)))")
-         prefer 2
-  subgoal
-           apply (clarsimp simp: isVIRQActive_def virq_type_def word_unat_eq_iff)
-           done
+     apply (prop_tac "\<not> (of_nat nregs \<le> (args ! 0 >> 32) && 0xFF)")
+      apply (simp add: word_le_nat_alt not_le)
+     apply clarsimp
+     apply (rule ccorres_move_const_guard)
+     apply (rule ccorres_move_c_guard_vcpu)
+     apply (simp add: liftM_def)
+     apply (clarsimp simp: rangeCheck_def not_le[symmetric]
+                           liftE_liftM[symmetric] liftE_bindE_assoc)
 
-        apply (simp add: rangeCheck_def not_le[symmetric])
-        apply (simp add: throwError_bind invocationCatch_def invocation_eq_use_types
-                   cong: StateSpace.state.fold_congs globals.fold_congs)
-        apply (rule syscall_error_throwError_ccorres_n)
-        apply (simp add: syscall_error_to_H_cases)
+     apply (rule ccorres_pre_getObject_vcpu, rename_tac vcpu)
+     apply csymbr
+     apply (rule ccorres_abstract_cleanup)
 
-       apply (subgoal_tac "\<not> isVIRQActive (vgicLR (vcpuVGIC vcpu) (unat ((args ! 0 >> 32) && 0xFF)))")
-               prefer 2
-  subgoal by (clarsimp simp: isVIRQActive_def virq_type_def word_unat_eq_iff)
+     apply (rule_tac P="ret__unsigned_longlong =
+                          of_nat (virq_type (vgicLR (vcpuVGIC vcpu)
+                                            (unat ((args ! 0 >> 32) && 0xFF))))"
+                     in ccorres_gen_asm2)
+     apply clarsimp
+     apply (rule ccorres_Cond_rhs_Seq)
+      apply (prop_tac "isVIRQActive (vgicLR (vcpuVGIC vcpu) (unat ((args ! 0 >> 32) && 0xFF)))")
+       apply (clarsimp simp add: virq_virq_active_eq_is_virq_active)
+      apply (simp add: rangeCheck_def not_le[symmetric])
+      apply (simp add: throwError_bind invocationCatch_def invocation_eq_use_types
+                 cong: StateSpace.state.fold_congs globals.fold_congs)
+      apply (rule syscall_error_throwError_ccorres_n)
+      apply (simp add: syscall_error_to_H_cases)
 
-       apply clarsimp
-       apply (simp add: returnOk_bind bindE_assoc
-                        performARMMMUInvocations performARMVCPUInvocation_def)
-       apply csymbr
-       apply (subst liftE_invokeVCPUInjectIRQ_empty_return)
-       apply clarsimp
+     apply (prop_tac "\<not>is_virq_active (vgicLR (vcpuVGIC vcpu) (unat ((args ! 0 >> 32) && 0xFF)))")
+      apply (clarsimp simp add: virq_virq_active_eq_is_virq_active)
+     apply clarsimp
+     apply (simp add: returnOk_bind bindE_assoc not_le
+                      performARMMMUInvocations performARMVCPUInvocation_def)
+     apply csymbr
+     apply (subst liftE_invokeVCPUInjectIRQ_empty_return)
+     apply clarsimp
 
      \<comment> \<open>we want the second alternative - nothing to return to user\<close>
      apply (ctac add: setThreadState_ccorres)
@@ -3923,40 +3926,26 @@ lemma decodeVCPUInjectIRQ_ccorres:
                         valid_tcb_state'_def ThreadState_defs mask_def)
 
   apply (frule invs_arch_state')
-  apply (clarsimp simp: valid_arch_state'_def max_armKSGICVCPUNumListRegs_def rf_sr_armKSGICVCPUNumListRegs)
-  apply (clarsimp simp: isCap_simps cap_get_tag_isCap capVCPUPtr_eq)
-  apply (clarsimp simp: sysargs_rel_to_n word_le_nat_alt linorder_not_less)
-  apply (clarsimp simp: valid_cap'_def)
-  apply (clarsimp simp: not_le word_le_nat_alt)
+  apply (clarsimp simp: valid_arch_state'_def max_armKSGICVCPUNumListRegs_val
+                        rf_sr_armKSGICVCPUNumListRegs isCap_simps cap_get_tag_isCap capVCPUPtr_eq
+                        sysargs_rel_to_n word_le_nat_alt linorder_not_less valid_cap'_def not_le)
 
-  apply (subgoal_tac "armKSGICVCPUNumListRegs (ksArchState s) < 2 ^ LENGTH(machine_word_len)")
-  prefer 2 subgoal by (erule order_le_less_trans; simp)
+  apply (prop_tac "armKSGICVCPUNumListRegs (ksArchState s) < 2 ^ LENGTH(machine_word_len)")
+   apply (erule order_less_trans; simp)
 
   apply (safe; clarsimp?)
-     apply (simp add: unat_eq_zero)
-    apply (subgoal_tac "armKSGICVCPUNumListRegs (ksArchState s) < 2 ^ LENGTH(machine_word_len)")
-     prefer 2 subgoal by (erule order_le_less_trans; simp)
-    apply (erule order_less_le_trans)
-    apply (simp add: unat_of_nat_eq)
-  apply (fastforce simp: sysargs_rel_to_n ct_in_state'_def st_tcb_at'_def comp_def
-                    elim: obj_at'_weakenE)
-  apply (fastforce simp: sysargs_rel_to_n ct_in_state'_def st_tcb_at'_def comp_def
-                    elim: obj_at'_weakenE)
-
-  apply (subgoal_tac "armKSGICVCPUNumListRegs (ksArchState s) < 2 ^ LENGTH(machine_word_len)")
-  prefer 2 subgoal by (erule order_le_less_trans; simp)
-  apply (erule order_less_le_trans)
+       apply (simp add: unat_eq_zero)
+      apply (erule order_less_le_trans)
+      apply (simp add: unat_of_nat_eq)
+     apply (fastforce simp: sysargs_rel_to_n ct_in_state'_def st_tcb_at'_def comp_def
+                      elim: obj_at'_weakenE)
+    apply (fastforce simp: sysargs_rel_to_n ct_in_state'_def st_tcb_at'_def comp_def
+                      elim: obj_at'_weakenE)
   apply (simp add: unat_of_nat_eq)
-  apply (clarsimp simp: typ_heap_simps')
-  apply (simp add: virq_get_tag_def mask_def shiftr_over_and_dist)
-  apply (simp add: cvcpu_relation_def cvgic_relation_def virq_to_H_def)
-  apply (clarsimp simp: cvcpu_relation_def cvgic_relation_def virq_get_tag_def
-                        shiftr_over_and_dist mask_def cvcpu_vppi_masked_relation_def)
-
-  apply (subgoal_tac "unat ((args ! 0 >> 32) && 0xFF) \<le> 63")
-   apply (rule sym)
-   apply simp
-  apply (fastforce simp: unat_of_nat_eq)
+  apply (clarsimp simp: typ_heap_simps' cvcpu_relation_def cvgic_relation_def)
+  apply (subgoal_tac "unat ((args ! 0 >> 32) && 0xFF) < max_armKSGICVCPUNumListRegs")
+   apply (simp add: virq_get_tag_eq_of_nat_virq_type)
+  apply (fastforce simp: unat_of_nat_eq max_armKSGICVCPUNumListRegs_val)
   done
 
 lemma decodeVCPUReadReg_ccorres:

proof/crefine/AARCH64/Invoke_C.thy

@@ -1804,7 +1804,7 @@ inline assembly, so we must appeal to the axiomatisation of inline assembly to s
 \<close>
 lemma preemptionPoint_hrs_htd:
   "\<forall>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call preemptionPoint_'proc \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>\<sigma>\<^esup>t_hrs\<rbrace>"
-  by (rule allI, rule conseqPre, vcg, clarsimp simp: asm_spec_enabled elim!: asm_specE)
+  by (rule allI, rule conseqPre, vcg exspec=isIRQPending_modifies, clarsimp simp: asm_spec_enabled elim!: asm_specE)
 
 lemma resetUntypedCap_ccorres:
   notes upt.simps[simp del] Collect_const[simp del] replicate_numeral[simp del]

proof/crefine/AARCH64/Retype_C.thy

@@ -5447,7 +5447,7 @@ lemma ptr_retyp_fromzeroVCPU:
   assumes cor: "caps_overlap_reserved' {p ..+ 2 ^ vcpuBits} \<sigma>"
   assumes ptr0: "p \<noteq> 0"
   assumes kdr: "{p ..+ 2 ^ vcpuBits} \<inter> kernel_data_refs = {}"
-  assumes subr: "{p ..+ 752} \<subseteq> {p ..+ 2 ^ vcpuBits}" (is "{_ ..+ ?vcpusz} \<subseteq> _")
+  assumes subr: "{p ..+ size_of TYPE(vcpu_C)} \<subseteq> {p ..+ 2 ^ vcpuBits}" (is "{_ ..+ ?vcpusz} \<subseteq> _")
   assumes act_bytes: "region_actually_is_bytes p (2 ^ vcpuBits) \<sigma>'"
   assumes rep0: "heap_list (hrs_mem (t_hrs_' (globals \<sigma>'))) (2 ^ vcpuBits) p = replicate (2 ^ vcpuBits) 0"
   assumes "\<not> snd (placeNewObject p vcpu0 0 \<sigma>)"
@@ -5464,10 +5464,6 @@ proof -
   let ?htdret = "(hrs_htd_update (ptr_retyp (vcpu_Ptr p)) (t_hrs_' (globals \<sigma>')))"
   let ?zeros = "from_bytes (replicate (size_of TYPE(vcpu_C)) 0) :: vcpu_C"
 
-  (* sanity check for the value of ?vcpusz *)
-  have "size_of TYPE(vcpu_C) = ?vcpusz"
-    by simp
-
   have ptr_al:
     "ptr_aligned (vcpu_Ptr p)" using al
     by (auto simp: align_of_def vcpuBits_def pageBits_def
@@ -5496,7 +5492,7 @@ proof -
     (is "?hl = ?rep0")
     using retyp_p' rep0
     apply (simp add: lift_t_if h_val_def)
-    apply (subst take_heap_list_le[where k="?vcpusz" and n="2^vcpuBits", symmetric])
+    apply (subst take_heap_list_le[where k="?vcpusz" and n="2^vcpuBits", simplified, symmetric])
      apply (simp add: vcpuBits_def)+
     done
 
@@ -5550,7 +5546,7 @@ proof -
      apply (case_tac r; clarsimp simp: index_foldr_update)
     apply (rule conjI, clarsimp)
      (* vgic_C array initialisation *)
-     apply (subst index_fold_update; clarsimp)
+     apply (subst index_fold_update; clarsimp simp: max_armKSGICVCPUNumListRegs_val)
     (* vppi array initialisation *)
     apply clarsimp
     apply (case_tac vppi; clarsimp)
@@ -5692,7 +5688,7 @@ proof -
     apply (subgoal_tac "region_is_bytes p ?vcpusz \<sigma>'")
      prefer 2
      apply (fastforce simp: region_actually_is_bytes[OF act_bytes]
-                            region_is_bytes_subset[OF _ subr])
+                            region_is_bytes_subset[OF _ subr, simplified])
     apply (simp add: projectKO_opt_retyp_other' objBitsKO_vcpu cl_vcpu
                      htd_safe[simplified] kernel_data_refs_domain_eq_rotate)
     apply (subst ptr_retyp_gen_one[symmetric])+
@@ -5719,7 +5715,7 @@ lemma placeNewObject_vcpu_fromzero_ccorres:
   apply (rule ccorres_from_vcg_nofail, clarsimp)
   apply (rule conseqPre, vcg)
   apply (clarsimp simp: rf_sr_htd_safe)
-  apply (subgoal_tac "{regionBase..+752} \<subseteq> {regionBase..+2^vcpuBits}")
+  apply (subgoal_tac "{regionBase..+size_of TYPE(vcpu_C)} \<subseteq> {regionBase..+2^vcpuBits}")
    prefer 2
    apply clarsimp
    apply (drule intvlD, clarsimp)

proof/crefine/AARCH64/StateRelation_C.thy

@@ -528,8 +528,8 @@ definition cvgic_relation :: "gicvcpuinterface \<Rightarrow> gicVCpuIface_C \<Ri
        gicVCpuIface_C.hcr_C cvgic = vgicHCR vgic
      \<and> gicVCpuIface_C.vmcr_C cvgic = vgicVMCR vgic
      \<and> gicVCpuIface_C.apr_C cvgic = vgicAPR vgic
-     \<and> (\<forall>i\<le>63. vgicLR vgic i = virq_to_H ((gicVCpuIface_C.lr_C cvgic).[i]))
-     \<and> (\<forall>i\<ge>64. vgicLR vgic i = 0)"
+     \<and> (\<forall>i<max_armKSGICVCPUNumListRegs. vgicLR vgic i = virq_to_H ((gicVCpuIface_C.lr_C cvgic).[i]))
+     \<and> (\<forall>i\<ge>max_armKSGICVCPUNumListRegs. vgicLR vgic i = 0)"
 
 definition cvcpu_relation :: "vcpu \<Rightarrow> vcpu_C \<Rightarrow> bool" where
   "cvcpu_relation vcpu cvcpu \<equiv>