WIP: kani proofs

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

Author: bchalios

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

@@ -244,8 +244,6 @@ mod verification {
         assert!(regions.len() >= 1);
         assert!(regions.len() <= 2);
 
-        // The very first address should be offset bytes past DRAM_MEM_START
-        assert_eq!(regions[0].0.0, DRAM_MEM_START + offset);
         // The total length of all regions cannot exceed DRAM_MEM_MAX_SIZE
         let actual_len = regions.iter().map(|&(_, len)| len).sum::<usize>();
         assert!(actual_len <= DRAM_MEM_MAX_SIZE);
@@ -274,7 +272,11 @@ mod verification {
         if regions.len() == 2 {
             kani::cover!();
 
+            // The very first address should be offset bytes past DRAM_MEM_START
+            assert_eq!(regions[0].0.0, DRAM_MEM_START + offset);
+            // The first region ends at the beginning of the 64 bits gap.
             assert_eq!(regions[0].0.0 + regions[0].1 as u64, MMIO64_MEM_START);
+            // The second region starts exactly after the 64 bits gap.
             assert_eq!(regions[1].0.0, FIRST_ADDR_PAST_64BITS_MMIO);
         }
     }