kani: Upgrade to 0.53.0

The kani::ensures attribute now requires a closure instead of just an
expression.

Signed-off-by: Patrick Roy <[email protected]>

Author: roypat

src/vmm/src/rate_limiter/mod.rs

@@ -28,7 +28,7 @@ const NANOSEC_IN_ONE_MILLISEC: u64 = 1_000_000;
 // Euclid's two-thousand-year-old algorithm for finding the greatest common divisor.
 #[cfg_attr(kani, kani::requires(x > 0 && y > 0))]
 #[cfg_attr(kani, kani::ensures(
-    result != 0
+    |&result| result != 0
         && x % result == 0
         && y % result == 0
 ))]

tests/integration_tests/test_kani.py

@@ -24,11 +24,12 @@ def test_kani(results_dir):
     """
     Test all Kani proof harnesses.
     """
-    # --enable-stubbing is required to enable the stubbing feature
+    # -Z stubbing is required to enable the stubbing feature
+    # -Z function-contracts is required to enable the function contracts feature
     # --restrict-vtable is required for some virtio queue proofs, which go out of memory otherwise
     # -j enables kani harnesses to be verified in parallel (required to keep CI time low)
     # --output-format terse is required by -j
-    # --enable-unstable is needed for each of the above
+    # --enable-unstable is needed to enable `-Z` flags
     _, stdout, _ = utils.check_output(
         "cargo kani --enable-unstable -Z stubbing -Z function-contracts --restrict-vtable -j --output-format terse"
     )