From d4f0e5a38bf848718dbed7303e06f508134d43a5 Mon Sep 17 00:00:00 2001
From: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Date: Tue, 5 Dec 2023 13:23:58 +1100
Subject: [PATCH] arm-hyp crefine: update length to word_t for VCPU functions

Length argument for these functions was previously unsigned int, which
was fine for AArch32, but an implicit downcast on AArch64. Changing it
to word_t makes it unsigned long, thus requiring signature update in
ccorres proofs.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
---
 proof/crefine/ARM_HYP/Arch_C.thy | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/proof/crefine/ARM_HYP/Arch_C.thy b/proof/crefine/ARM_HYP/Arch_C.thy
index f651380021..5468bae776 100644
--- a/proof/crefine/ARM_HYP/Arch_C.thy
+++ b/proof/crefine/ARM_HYP/Arch_C.thy
@@ -4557,14 +4557,14 @@ lemma decodeVCPUWriteReg_ccorres:
        (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple
               and sysargs_rel args buffer
               and (valid_cap' (ArchObjectCap cp)) and K (isVCPUCap cp))
-       (UNIV \<inter> {s. unat (length_' s) = length args}
+       (UNIV \<inter> {s. unat (length___unsigned_long_' s) = length args}
              \<inter> {s. ccap_relation (ArchObjectCap cp) (cap_' s)}
              \<inter> {s. buffer_' s = option_to_ptr buffer}) hs
        (decodeVCPUWriteReg args cp
               >>= invocationCatch thread isBlocking isCall InvokeArchObject)
        (Call decodeVCPUWriteReg_'proc)"
   apply (rule ccorres_grab_asm)
-  apply (cinit' lift: length_' cap_' buffer_' simp: decodeVCPUWriteReg_def Let_def)
+  apply (cinit' lift: length___unsigned_long_' cap_' buffer_' simp: decodeVCPUWriteReg_def Let_def)
    apply (rule ccorres_Cond_rhs_Seq ; clarsimp)
     apply (rule_tac ccorres_gen_asm[where P="length args < 2"])
     apply clarsimp
@@ -4688,7 +4688,7 @@ lemma decodeVCPUInjectIRQ_ccorres:
               and sysargs_rel args buffer
               and (valid_cap' (ArchObjectCap cp))
               and K (isVCPUCap cp))
-       (UNIV \<inter> {s. unat (length_' s) = length args}
+       (UNIV \<inter> {s. unat (length___unsigned_long_' s) = length args}
              \<inter> {s. ccap_relation (ArchObjectCap cp) (cap_' s)}
              \<inter> {s. buffer_' s = option_to_ptr buffer}
              ) hs
@@ -4696,7 +4696,7 @@ lemma decodeVCPUInjectIRQ_ccorres:
               >>= invocationCatch thread isBlocking isCall InvokeArchObject)
        (Call decodeVCPUInjectIRQ_'proc)"
   apply (rule ccorres_grab_asm)
-  apply (cinit' lift: length_' cap_' buffer_'
+  apply (cinit' lift: length___unsigned_long_' cap_' buffer_'
                 simp: decodeVCPUInjectIRQ_def Let_def shiftL_nat )
    apply csymbr
    apply csymbr
@@ -4904,14 +4904,14 @@ lemma decodeVCPUReadReg_ccorres:
        (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple
               and sysargs_rel args buffer
               and (valid_cap' (ArchObjectCap cp)))
-       (UNIV \<inter> {s. unat (length_' s) = length args}
+       (UNIV \<inter> {s. unat (length___unsigned_long_' s) = length args}
              \<inter> {s. ccap_relation (ArchObjectCap cp) (cap_' s)}
              \<inter> {s. buffer_' s = option_to_ptr buffer}
              \<inter> \<lbrace>\<acute>call = from_bool isCall \<rbrace>) hs
        (decodeVCPUReadReg args cp
               >>= invocationCatch thread isBlocking isCall InvokeArchObject)
        (Call decodeVCPUReadReg_'proc)"
-  apply (cinit' lift: length_' cap_' buffer_' call_')
+  apply (cinit' lift: length___unsigned_long_' cap_' buffer_' call_')
    apply (clarsimp simp: decodeVCPUReadReg_def Let_def)
    apply (rule ccorres_Cond_rhs_Seq)
     apply (simp add: throwError_bind invocationCatch_def invocation_eq_use_types
@@ -5120,7 +5120,7 @@ lemma decodeVCPUAckVPPI_ccorres:
               and sysargs_rel args buffer
               and (valid_cap' (ArchObjectCap cp))
               and K (isVCPUCap cp))
-       (UNIV \<inter> {s. unat (length_' s) = length args}
+       (UNIV \<inter> {s. unat (length___unsigned_long_' s) = length args}
              \<inter> {s. ccap_relation (ArchObjectCap cp) (cap_' s)}
              \<inter> {s. buffer_' s = option_to_ptr buffer}
              ) hs
@@ -5142,7 +5142,7 @@ proof -
 
   show ?thesis
     apply (rule ccorres_grab_asm)
-    apply (cinit' lift: length_' cap_' buffer_')
+    apply (cinit' lift: length___unsigned_long_' cap_' buffer_')
      apply (clarsimp simp: decodeVCPUAckVPPI_def)
      apply (csymbr, rename_tac cp')
      apply csymbr
@@ -5241,7 +5241,7 @@ lemma decodeARMVCPUInvocation_ccorres:
               and (valid_cap' (ArchObjectCap cp)))
        (UNIV \<comment> \<open>whoever wrote the C code decided to name this arbitrarily differently from other functions\<close>
              \<inter> {s. label___unsigned_long_' s = label}
-             \<inter> {s. unat (length_' s) = length args}
+             \<inter> {s. unat (length___unsigned_long_' s) = length args}
              \<inter> {s. slot_' s = cte_Ptr slot}
              \<inter> {s. current_extra_caps_' (globals s) = extraCaps'}
              \<inter> {s. ccap_relation (ArchObjectCap cp) (cap_' s)}
@@ -5250,7 +5250,7 @@ lemma decodeARMVCPUInvocation_ccorres:
        (decodeARMVCPUInvocation label args cptr slot cp extraCaps
               >>= invocationCatch thread isBlocking isCall InvokeArchObject)
        (Call decodeARMVCPUInvocation_'proc)"
-  apply (cinit' lift: label___unsigned_long_' length_' slot_' current_extra_caps_'
+  apply (cinit' lift: label___unsigned_long_' length___unsigned_long_' slot_' current_extra_caps_'
                        cap_' buffer_' call_')
    apply (clarsimp simp: decodeARMVCPUInvocation_def)