From e87c4488836e811901130058e4d6fe66ba9f6b06 Mon Sep 17 00:00:00 2001
From: Corey Lewis <corey.lewis@unsw.edu.au>
Date: Mon, 31 Jan 2022 13:55:47 +1100
Subject: [PATCH] arm-hyp crefine: update for Exynos5

Signed-off-by: Corey Lewis <corey.lewis@unsw.edu.au>
---
 proof/crefine/ARM_HYP/StateRelation_C.thy | 2 +-
 proof/crefine/ARM_HYP/Syscall_C.thy       | 2 +-
 proof/crefine/ARM_HYP/VSpace_C.thy        | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/proof/crefine/ARM_HYP/StateRelation_C.thy b/proof/crefine/ARM_HYP/StateRelation_C.thy
index 085931cff3..83d8c0d9ac 100644
--- a/proof/crefine/ARM_HYP/StateRelation_C.thy
+++ b/proof/crefine/ARM_HYP/StateRelation_C.thy
@@ -631,7 +631,7 @@ fun
   | "irqstate_to_C irqstate.IRQReserved = scast Kernel_C.IRQReserved"
 
 definition
-  cinterrupt_relation :: "interrupt_state \<Rightarrow> 'a ptr \<Rightarrow> (word32[192]) \<Rightarrow> bool"
+  cinterrupt_relation :: "interrupt_state \<Rightarrow> 'a ptr \<Rightarrow> (word32[255]) \<Rightarrow> bool"
 where
   "cinterrupt_relation airqs cnode cirqs \<equiv>
      cnode = Ptr (intStateIRQNode airqs) \<and>
diff --git a/proof/crefine/ARM_HYP/Syscall_C.thy b/proof/crefine/ARM_HYP/Syscall_C.thy
index 142feb4946..febd5f827d 100644
--- a/proof/crefine/ARM_HYP/Syscall_C.thy
+++ b/proof/crefine/ARM_HYP/Syscall_C.thy
@@ -1612,7 +1612,7 @@ lemma ucast_maxIRQ_is_less:
   "SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ < UCAST(10 \<rightarrow> 32) irq \<Longrightarrow> scast Kernel_C.maxIRQ < irq"
   apply (clarsimp simp: scast_def Kernel_C.maxIRQ_def)
   apply (subgoal_tac "LENGTH(10) \<le> LENGTH(32)")
-  apply (drule less_ucast_ucast_less[where x= "0xBF" and y="irq"])
+  apply (drule less_ucast_ucast_less[where x= "0xFE" and y="irq"])
     by (simp)+
 
 lemma validIRQcastingLess:
diff --git a/proof/crefine/ARM_HYP/VSpace_C.thy b/proof/crefine/ARM_HYP/VSpace_C.thy
index 36160c1267..f4c98fd508 100644
--- a/proof/crefine/ARM_HYP/VSpace_C.thy
+++ b/proof/crefine/ARM_HYP/VSpace_C.thy
@@ -1851,7 +1851,7 @@ lemma isIRQActive_ccorres:
         (isIRQActive irq) (Call isIRQActive_'proc)"
   apply (cinit lift: irq_')
    apply (simp add: getIRQState_def getInterruptState_def)
-   apply (rule_tac P="irq \<le> ucast Kernel_C.maxIRQ \<and> unat irq < (192::nat)" in ccorres_gen_asm)
+   apply (rule_tac P="irq \<le> ucast Kernel_C.maxIRQ \<and> unat irq < (255::nat)" in ccorres_gen_asm)
    apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV])
    apply (rule allI, rule conseqPre, vcg)
    apply (clarsimp simp: simpler_gets_def word_sless_msb_less maxIRQ_def