[Certora] liquidation liveness

certora/confs/LiquidateLiveness.conf

@@ -0,0 +1,34 @@
+{
+  "files": [
+    "certora/helpers/Utils.sol",
+    "src/Midnight.sol"
+  ],
+  "verify": "Midnight:certora/specs/LiquidateLiveness.spec",
+  "solc": "solc-0.8.34",
+  "solc_via_ir": true,
+  "solc_evm_version": "osaka",
+  "optimistic_loop": true,
+  "loop_iter": 3,
+  "optimistic_hashing": true,
+  "hashing_length_bound": 2048,
+  "smt_timeout": 7200,
+  "prover_args": [
+    "-mediumTimeout 20",
+    "-lowTimeout 20",
+    "-tinyTimeout 20",
+    "-depth 20"
+  ],
+  "exclude_rule": [
+    "nonZeroCollateralsAreActivated"
+  ],
+  "split_rules": [
+    "unhealthyLltvFullLiquidatableForAnySafeAmount",
+    "unhealthyLowLltvLiquidatableForAnySafeAmount",
+    "postMaturityLiquidatableForAnySafeAmount",
+    "seizeUnhealthyLltvFullLiquidatableForAnySafeAmount",
+    "seizeUnhealthyLowLltvLiquidatableForAnySafeAmount",
+    "seizePostMaturityLiquidatableForAnySafeAmount",
+    "badDebtCanBeLiquidated"
+  ],
+  "msg": "Liquidate Liveness"
+}