From eba034612311cc66603f0dba2440916e01922a92 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 25 Feb 2024 19:38:01 +0100 Subject: [PATCH] arm-hyp crefine: VCPUReg_VMPIDR updates Signed-off-by: Gerwin Klein --- proof/crefine/ARM_HYP/ArchMove_C.thy | 3 ++- proof/crefine/ARM_HYP/Retype_C.thy | 8 ++++---- proof/crefine/ARM_HYP/SR_lemmas_C.thy | 1 + proof/crefine/ARM_HYP/Wellformed_C.thy | 2 +- 4 files changed, 8 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 "\s. P (pred_tcb_at' a b p s)" crunch ksCurThread[wp]: readVCPUReg "\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..9843456105 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} \" assumes ptr0: "p \ 0" assumes kdr: "{p ..+ 2 ^ vcpu_bits} \ kernel_data_refs = {}" - assumes subr: "{p ..+ 456} \ {p ..+ 2 ^ vcpu_bits}" + assumes subr: "{p ..+ 464} \ {p ..+ 2 ^ vcpu_bits}" (is "{_ ..+ ?vcpusz} \ _") assumes act_bytes: "region_actually_is_bytes p (2 ^ vcpu_bits) \'" assumes rep0: "heap_list (hrs_mem (t_hrs_' (globals \'))) (2 ^ vcpu_bits) p = replicate (2 ^ vcpu_bits) 0" assumes "\ snd (placeNewObject p vcpu0 0 \)" @@ -5360,7 +5360,7 @@ proof - let ?htdret = "(hrs_htd_update (ptr_retyp (vcpu_Ptr p)) (t_hrs_' (globals \')))" let ?zeros = "from_bytes (replicate (size_of TYPE(vcpu_C)) 0) :: vcpu_C" - have "size_of TYPE(vcpu_C) = 456" (is "_ = ?vcpusz") + have "size_of TYPE(vcpu_C) = ?vcpusz" by simp have ptr_al: @@ -5574,7 +5574,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 \'") + apply (subgoal_tac "region_is_bytes p 464 \'") prefer 2 apply (fastforce simp: region_actually_is_bytes[OF act_bytes] region_is_bytes_subset[OF _ subr]) @@ -5604,7 +5604,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} \ {regionBase..+2^vcpu_bits}") + apply (subgoal_tac "{regionBase..+464} \ {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..1d29bf2bc8 100644 --- a/proof/crefine/ARM_HYP/Wellformed_C.thy +++ b/proof/crefine/ARM_HYP/Wellformed_C.thy @@ -43,7 +43,7 @@ abbreviation abbreviation pd_Ptr :: "32 word \ (pde_C[2048]) ptr" where "pd_Ptr == Ptr" abbreviation - regs_C_Ptr :: "addr \ (machine_word_len word[42]) ptr" where "regs_C_Ptr \ Ptr" + regs_C_Ptr :: "addr \ (machine_word_len word[43]) ptr" where"regs_C_Ptr \ Ptr" abbreviation vgic_lr_C_Ptr :: "addr \ (virq_C[64]) ptr" where "vgic_lr_C_Ptr \ Ptr" abbreviation