From cd0a8f1abaccecc6c79280aa5dc3704048599a5d Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Sun, 25 Feb 2024 19:38:01 +0100
Subject: [PATCH] arm-hyp crefine: VCPUReg_VMPIDR updates

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 proof/crefine/ARM_HYP/ArchMove_C.thy   | 3 ++-
 proof/crefine/ARM_HYP/Retype_C.thy     | 9 +++++----
 proof/crefine/ARM_HYP/SR_lemmas_C.thy  | 1 +
 proof/crefine/ARM_HYP/Wellformed_C.thy | 7 ++++++-
 4 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/proof/crefine/ARM_HYP/ArchMove_C.thy b/proof/crefine/ARM_HYP/ArchMove_C.thy
index 530b503ebb..573715c6f8 100644
--- a/proof/crefine/ARM_HYP/ArchMove_C.thy
+++ b/proof/crefine/ARM_HYP/ArchMove_C.thy
@@ -457,8 +457,9 @@ 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 *)
 lemma fromEnum_maxBound_vcpureg_def:
-  "fromEnum (maxBound :: vcpureg) = 41"
+  "fromEnum (maxBound :: vcpureg) = 42"
   by (clarsimp simp: fromEnum_def maxBound_def enum_vcpureg)
 
 lemma unat_of_nat_mword_fromEnum_vcpureg[simp]:
diff --git a/proof/crefine/ARM_HYP/Retype_C.thy b/proof/crefine/ARM_HYP/Retype_C.thy
index 23030fcc21..9e6de1a1fb 100644
--- a/proof/crefine/ARM_HYP/Retype_C.thy
+++ b/proof/crefine/ARM_HYP/Retype_C.thy
@@ -5343,7 +5343,7 @@ lemma ptr_retyp_fromzeroVCPU:
   assumes cor: "caps_overlap_reserved' {p ..+ 2 ^ vcpu_bits} \<sigma>"
   assumes ptr0: "p \<noteq> 0"
   assumes kdr: "{p ..+ 2 ^ vcpu_bits} \<inter> kernel_data_refs = {}"
-  assumes subr: "{p ..+ 456} \<subseteq> {p ..+ 2 ^ vcpu_bits}"
+  assumes subr: "{p ..+ 464} \<subseteq> {p ..+ 2 ^ vcpu_bits}" (is "{_ ..+ ?vcpusz} \<subseteq> _")
   assumes act_bytes: "region_actually_is_bytes p (2 ^ vcpu_bits) \<sigma>'"
   assumes rep0: "heap_list (hrs_mem (t_hrs_' (globals \<sigma>'))) (2 ^ vcpu_bits) p = replicate (2 ^ vcpu_bits) 0"
   assumes "\<not> snd (placeNewObject p vcpu0 0 \<sigma>)"
@@ -5360,7 +5360,8 @@ 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"
 
-  have "size_of TYPE(vcpu_C) = 456" (is "_ = ?vcpusz")
+  (* sanity check for the value of ?vcpusz *)
+  have "size_of TYPE(vcpu_C) = ?vcpusz"
     by simp
 
   have ptr_al:
@@ -5574,7 +5575,7 @@ proof -
     apply (clarsimp simp: ko_vcpu_def vcpu0_def)
     apply (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def
                           cmachine_state_relation_def Let_def h_t_valid_clift_Some_iff)
-    apply (subgoal_tac "region_is_bytes p 456 \<sigma>'")
+    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])
@@ -5604,7 +5605,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..+456} \<subseteq> {regionBase..+2^vcpu_bits}")
+  apply (subgoal_tac "{regionBase..+464} \<subseteq> {regionBase..+2^vcpu_bits}")
    prefer 2
    apply clarsimp
    apply (drule intvlD, clarsimp)
diff --git a/proof/crefine/ARM_HYP/SR_lemmas_C.thy b/proof/crefine/ARM_HYP/SR_lemmas_C.thy
index 6a34b458be..0f0ca4caaa 100644
--- a/proof/crefine/ARM_HYP/SR_lemmas_C.thy
+++ b/proof/crefine/ARM_HYP/SR_lemmas_C.thy
@@ -2324,6 +2324,7 @@ lemmas seL4_VCPUReg_defs =
     seL4_VCPUReg_R10fiq_def
     seL4_VCPUReg_R11fiq_def
     seL4_VCPUReg_R12fiq_def
+    seL4_VCPUReg_VMPIDR_def
     seL4_VCPUReg_SPSRsvc_def
     seL4_VCPUReg_SPSRabt_def
     seL4_VCPUReg_SPSRund_def
diff --git a/proof/crefine/ARM_HYP/Wellformed_C.thy b/proof/crefine/ARM_HYP/Wellformed_C.thy
index 4a6b608e94..a09d0de707 100644
--- a/proof/crefine/ARM_HYP/Wellformed_C.thy
+++ b/proof/crefine/ARM_HYP/Wellformed_C.thy
@@ -42,8 +42,13 @@ abbreviation
   pt_Ptr :: "32 word \<Rightarrow> (pte_C[512]) ptr" where "pt_Ptr == Ptr"
 abbreviation
   pd_Ptr :: "32 word \<Rightarrow> (pde_C[2048]) ptr" where "pd_Ptr == Ptr"
+
+declare seL4_VCPUReg_Num_def[code]
+value_type num_vcpu_regs = seL4_VCPUReg_Num
+
 abbreviation
-  regs_C_Ptr :: "addr \<Rightarrow> (machine_word_len word[42]) ptr" where "regs_C_Ptr \<equiv> Ptr"
+  regs_C_Ptr :: "addr \<Rightarrow> (machine_word[num_vcpu_regs]) ptr" where"regs_C_Ptr \<equiv> Ptr"
+
 abbreviation
   vgic_lr_C_Ptr :: "addr \<Rightarrow> (virq_C[64]) ptr" where "vgic_lr_C_Ptr \<equiv> Ptr"
 abbreviation