WIP: kani proofs

Signed-off-by: Babis Chalios <[email protected]>

Author: bchalios

src/vmm/src/arch/aarch64/mod.rs

@@ -215,8 +215,7 @@ pub fn load_kernel(
 #[cfg(kani)]
 mod verification {
     use crate::arch::aarch64::layout::{
-        DRAM_MEM_MAX_SIZE, DRAM_MEM_START, FIRST_ADDR_PAST_64BITS_MMIO, MMIO32_MEM_START,
-        MMIO64_MEM_START,
+        DRAM_MEM_MAX_SIZE, DRAM_MEM_START, FIRST_ADDR_PAST_64BITS_MMIO, MMIO64_MEM_START,
     };
     use crate::arch::arch_memory_regions;
 
@@ -275,7 +274,7 @@ mod verification {
         if regions.len() == 2 {
             kani::cover!();
 
-            assert_eq!(regions[0].0.0 + regions[0].1 as u64, MMIO32_MEM_START);
+            assert_eq!(regions[0].0.0 + regions[0].1 as u64, MMIO64_MEM_START);
             assert_eq!(regions[1].0.0, FIRST_ADDR_PAST_64BITS_MMIO);
         }
     }