arm-hyp crefine: update for Exynos5

Signed-off-by: Corey Lewis <corey.lewis@unsw.edu.au>
seL4 · Jun 20, 2024 · 863f4aa · 863f4aa
1 parent 8329132
commit 863f4aa
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/proof/crefine/ARM_HYP/StateRelation_C.thy b/proof/crefine/ARM_HYP/StateRelation_C.thy
@@ -637,7 +637,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
@@ -1600,7 +1600,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
@@ -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