WIP: kani proofs

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

Author: bchalios

src/vmm/src/arch/mod.rs

@@ -147,6 +147,6 @@ fn arch_memory_regions_with_gap(
             Some((first_addr_past_gap, remaining))
         }
         // case2: region starts past the gap
-        Some(remaining) => Some((first_addr_past_gap.max(offset), remaining)),
+        Some(_) => Some((first_addr_past_gap.max(offset), size)),
     }
 }