From 284e655adc87933e6cb0843d1630795c6718e32d Mon Sep 17 00:00:00 2001 From: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Date: Thu, 4 Jun 2026 13:52:14 +0300 Subject: [PATCH 1/6] missing summary --- .github/workflows/certora-solvency.yml | 4 ++-- .../lemma-COLasset-totSUP0.spec | 22 +++++++++++++++++++ .../main-COLasset-totSUP0.spec | 11 ++++++++++ 3 files changed, 35 insertions(+), 2 deletions(-) diff --git a/.github/workflows/certora-solvency.yml b/.github/workflows/certora-solvency.yml index 6f99e2621..255f6c048 100644 --- a/.github/workflows/certora-solvency.yml +++ b/.github/workflows/certora-solvency.yml @@ -58,8 +58,8 @@ jobs: certora/solvency/confs/solvency/liquidationCall/lemma-DBTasset.conf certora/solvency/confs/solvency/liquidationCall/main-DBTasset.conf certora/solvency/confs/solvency/liquidationCall/main-COLasset.conf - certora/solvency/confs/solvency/liquidationCall/lemma-COLasset.conf --rule_sanity "none" - certora/solvency/confs/solvency/liquidationCall/main-COLasset-totSUP0.conf --rule_sanity "none" + certora/solvency/confs/solvency/liquidationCall/lemma-COLasset.conf + certora/solvency/confs/solvency/liquidationCall/main-COLasset-totSUP0.conf certora/solvency/confs/solvency/liquidationCall/lemma-COLasset-totSUP0.conf certora/solvency/confs/solvency/liquidationCall/burnBadDebt-assetINloop.conf certora/solvency/confs/solvency/liquidationCall/burnBadDebt-assetNOTINloop.conf diff --git a/certora/solvency/specs/liquidationCall/lemma-COLasset-totSUP0.spec b/certora/solvency/specs/liquidationCall/lemma-COLasset-totSUP0.spec index 472453e0b..b9d7e34b2 100644 --- a/certora/solvency/specs/liquidationCall/lemma-COLasset-totSUP0.spec +++ b/certora/solvency/specs/liquidationCall/lemma-COLasset-totSUP0.spec @@ -26,6 +26,16 @@ methods { uint256 liquidationBonus ) internal returns (uint256,uint256,uint256) => _calculateAvailableCollateralToLiquidateCVL(); + + + function LiquidationLogic.get_userCollateralBalance() internal returns (uint256) => NONDET; + function LiquidationLogic.get_liquidationBonus() internal returns (uint256) => NONDET; + function LiquidationLogic.get_collateralAssetPrice() internal returns (uint256) => NONDET; + function LiquidationLogic.get_debtAssetPrice() internal returns (uint256) => NONDET; + function LiquidationLogic.get_collateralAssetUnit() internal returns (uint256) => NONDET; + function LiquidationLogic.get_debtAssetUnit() internal returns (uint256) => NONDET; + function LiquidationLogic.get_userReserveDebtInBaseCurrency() internal returns (uint256) => NONDET; + function LiquidationLogic.get_userReserveCollateralInBaseCurrency() internal returns (uint256) => NONDET; } function getNormalizedIncome_hook_CVL(uint256 ret_val, address aTokenAddress) { @@ -93,6 +103,7 @@ function configuration() { /*===================================================================================== Rule: same_indexes__liquidationCall =====================================================================================*/ + rule same_indexes__liquidationCall(env e) { INSIDE_liquidationCall = false; configuration(); @@ -121,3 +132,14 @@ rule same_indexes__liquidationCall(env e) { } + + +rule test() { + // THE FUNCTION CALL + configuration(); + + address user; uint256 debtToCover; bool receiveAToken; + env e; + liquidationCall(e, _COL_asset, _DBT_asset, user, debtToCover, receiveAToken); + assert false; +} diff --git a/certora/solvency/specs/liquidationCall/main-COLasset-totSUP0.spec b/certora/solvency/specs/liquidationCall/main-COLasset-totSUP0.spec index 54323c81a..a0a1360c3 100644 --- a/certora/solvency/specs/liquidationCall/main-COLasset-totSUP0.spec +++ b/certora/solvency/specs/liquidationCall/main-COLasset-totSUP0.spec @@ -40,6 +40,17 @@ methods { uint256 liquidationBonus ) internal returns (uint256,uint256,uint256) => _calculateAvailableCollateralToLiquidateCVL(); + + + + function LiquidationLogic.get_userCollateralBalance() internal returns (uint256) => NONDET; + function LiquidationLogic.get_liquidationBonus() internal returns (uint256) => NONDET; + function LiquidationLogic.get_collateralAssetPrice() internal returns (uint256) => NONDET; + function LiquidationLogic.get_debtAssetPrice() internal returns (uint256) => NONDET; + function LiquidationLogic.get_collateralAssetUnit() internal returns (uint256) => NONDET; + function LiquidationLogic.get_debtAssetUnit() internal returns (uint256) => NONDET; + function LiquidationLogic.get_userReserveDebtInBaseCurrency() internal returns (uint256) => NONDET; + function LiquidationLogic.get_userReserveCollateralInBaseCurrency() internal returns (uint256) => NONDET; } // This is immediately after the call to updateState for the COL token From fb6c2760634e17f4011af47374f9874defc032bb Mon Sep 17 00:00:00 2001 From: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Date: Tue, 9 Jun 2026 10:08:52 +0300 Subject: [PATCH 2/6] missing summaries --- .../solvency/specs/liquidationCall/lemma-DBTasset.spec | 9 +++++++++ .../solvency/specs/liquidationCall/lemma-SAMEasset.spec | 9 +++++++++ .../solvency/specs/liquidationCall/main-COLasset.spec | 9 +++++++++ .../solvency/specs/liquidationCall/main-DBTasset.spec | 9 +++++++++ .../solvency/specs/liquidationCall/main-SAMEasset.spec | 9 +++++++++ 5 files changed, 45 insertions(+) diff --git a/certora/solvency/specs/liquidationCall/lemma-DBTasset.spec b/certora/solvency/specs/liquidationCall/lemma-DBTasset.spec index 4c199e35f..18ef52d07 100644 --- a/certora/solvency/specs/liquidationCall/lemma-DBTasset.spec +++ b/certora/solvency/specs/liquidationCall/lemma-DBTasset.spec @@ -35,6 +35,15 @@ methods { function LiquidationLogic.HOOK_liquidation_after_burnBadDebt() internal with (env e) => HOOK_liquidation_after_burnBadDebt_CVL(e); + + function LiquidationLogic.get_userCollateralBalance() internal returns (uint256) => NONDET; + function LiquidationLogic.get_liquidationBonus() internal returns (uint256) => NONDET; + function LiquidationLogic.get_collateralAssetPrice() internal returns (uint256) => NONDET; + function LiquidationLogic.get_debtAssetPrice() internal returns (uint256) => NONDET; + function LiquidationLogic.get_collateralAssetUnit() internal returns (uint256) => NONDET; + function LiquidationLogic.get_debtAssetUnit() internal returns (uint256) => NONDET; + function LiquidationLogic.get_userReserveDebtInBaseCurrency() internal returns (uint256) => NONDET; + function LiquidationLogic.get_userReserveCollateralInBaseCurrency() internal returns (uint256) => NONDET; } diff --git a/certora/solvency/specs/liquidationCall/lemma-SAMEasset.spec b/certora/solvency/specs/liquidationCall/lemma-SAMEasset.spec index d38d2a256..bc2b42a42 100644 --- a/certora/solvency/specs/liquidationCall/lemma-SAMEasset.spec +++ b/certora/solvency/specs/liquidationCall/lemma-SAMEasset.spec @@ -35,6 +35,15 @@ methods { function LiquidationLogic.HOOK_liquidation_after_burnBadDebt() internal with (env e) => HOOK_liquidation_after_burnBadDebt_CVL(e); + + function LiquidationLogic.get_userCollateralBalance() internal returns (uint256) => NONDET; + function LiquidationLogic.get_liquidationBonus() internal returns (uint256) => NONDET; + function LiquidationLogic.get_collateralAssetPrice() internal returns (uint256) => NONDET; + function LiquidationLogic.get_debtAssetPrice() internal returns (uint256) => NONDET; + function LiquidationLogic.get_collateralAssetUnit() internal returns (uint256) => NONDET; + function LiquidationLogic.get_debtAssetUnit() internal returns (uint256) => NONDET; + function LiquidationLogic.get_userReserveDebtInBaseCurrency() internal returns (uint256) => NONDET; + function LiquidationLogic.get_userReserveCollateralInBaseCurrency() internal returns (uint256) => NONDET; } diff --git a/certora/solvency/specs/liquidationCall/main-COLasset.spec b/certora/solvency/specs/liquidationCall/main-COLasset.spec index 24619588a..401747a4f 100644 --- a/certora/solvency/specs/liquidationCall/main-COLasset.spec +++ b/certora/solvency/specs/liquidationCall/main-COLasset.spec @@ -77,6 +77,15 @@ methods { DataTypes.UserConfigurationMap storage userConfig, DataTypes.ExecuteLiquidationCallParams memory params ) internal with (env e) => _burnBadDebt_CVL(e); + + function LiquidationLogic.get_userCollateralBalance() internal returns (uint256) => NONDET; + function LiquidationLogic.get_liquidationBonus() internal returns (uint256) => NONDET; + function LiquidationLogic.get_collateralAssetPrice() internal returns (uint256) => NONDET; + function LiquidationLogic.get_debtAssetPrice() internal returns (uint256) => NONDET; + function LiquidationLogic.get_collateralAssetUnit() internal returns (uint256) => NONDET; + function LiquidationLogic.get_debtAssetUnit() internal returns (uint256) => NONDET; + function LiquidationLogic.get_userReserveDebtInBaseCurrency() internal returns (uint256) => NONDET; + function LiquidationLogic.get_userReserveCollateralInBaseCurrency() internal returns (uint256) => NONDET; } function _burnBadDebt_CVL(env e) { diff --git a/certora/solvency/specs/liquidationCall/main-DBTasset.spec b/certora/solvency/specs/liquidationCall/main-DBTasset.spec index abccc4321..96198e899 100644 --- a/certora/solvency/specs/liquidationCall/main-DBTasset.spec +++ b/certora/solvency/specs/liquidationCall/main-DBTasset.spec @@ -71,6 +71,15 @@ methods { DataTypes.UserConfigurationMap storage userConfig, DataTypes.ExecuteLiquidationCallParams memory params ) internal with (env e) => _burnBadDebt_CVL(e); + + function LiquidationLogic.get_userCollateralBalance() internal returns (uint256) => NONDET; + function LiquidationLogic.get_liquidationBonus() internal returns (uint256) => NONDET; + function LiquidationLogic.get_collateralAssetPrice() internal returns (uint256) => NONDET; + function LiquidationLogic.get_debtAssetPrice() internal returns (uint256) => NONDET; + function LiquidationLogic.get_collateralAssetUnit() internal returns (uint256) => NONDET; + function LiquidationLogic.get_debtAssetUnit() internal returns (uint256) => NONDET; + function LiquidationLogic.get_userReserveDebtInBaseCurrency() internal returns (uint256) => NONDET; + function LiquidationLogic.get_userReserveCollateralInBaseCurrency() internal returns (uint256) => NONDET; } function getNormalizedIncome_CVL() returns uint256 { diff --git a/certora/solvency/specs/liquidationCall/main-SAMEasset.spec b/certora/solvency/specs/liquidationCall/main-SAMEasset.spec index 5955ce7b2..2ad8df739 100644 --- a/certora/solvency/specs/liquidationCall/main-SAMEasset.spec +++ b/certora/solvency/specs/liquidationCall/main-SAMEasset.spec @@ -76,6 +76,15 @@ methods { DataTypes.UserConfigurationMap storage userConfig, DataTypes.ExecuteLiquidationCallParams memory params ) internal with (env e) => _burnBadDebt_CVL(e); + + function LiquidationLogic.get_userCollateralBalance() internal returns (uint256) => NONDET; + function LiquidationLogic.get_liquidationBonus() internal returns (uint256) => NONDET; + function LiquidationLogic.get_collateralAssetPrice() internal returns (uint256) => NONDET; + function LiquidationLogic.get_debtAssetPrice() internal returns (uint256) => NONDET; + function LiquidationLogic.get_collateralAssetUnit() internal returns (uint256) => NONDET; + function LiquidationLogic.get_debtAssetUnit() internal returns (uint256) => NONDET; + function LiquidationLogic.get_userReserveDebtInBaseCurrency() internal returns (uint256) => NONDET; + function LiquidationLogic.get_userReserveCollateralInBaseCurrency() internal returns (uint256) => NONDET; } function getNormalizedIncome_CVL() returns uint256 { From ba7d517e5b8e5b4185b077fdba4a1d6ba43cd8c1 Mon Sep 17 00:00:00 2001 From: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Date: Tue, 9 Jun 2026 11:09:48 +0300 Subject: [PATCH 3/6] cleanup, missing summary --- .../liquidationCall/lemma-COLasset-totSUP0.spec | 12 ------------ .../specs/liquidationCall/lemma-COLasset.spec | 12 +++++++++++- 2 files changed, 11 insertions(+), 13 deletions(-) diff --git a/certora/solvency/specs/liquidationCall/lemma-COLasset-totSUP0.spec b/certora/solvency/specs/liquidationCall/lemma-COLasset-totSUP0.spec index b9d7e34b2..f139b26ee 100644 --- a/certora/solvency/specs/liquidationCall/lemma-COLasset-totSUP0.spec +++ b/certora/solvency/specs/liquidationCall/lemma-COLasset-totSUP0.spec @@ -131,15 +131,3 @@ rule same_indexes__liquidationCall(env e) { assert __COL_liqIND_after == _COL_liqIND; } - - - -rule test() { - // THE FUNCTION CALL - configuration(); - - address user; uint256 debtToCover; bool receiveAToken; - env e; - liquidationCall(e, _COL_asset, _DBT_asset, user, debtToCover, receiveAToken); - assert false; -} diff --git a/certora/solvency/specs/liquidationCall/lemma-COLasset.spec b/certora/solvency/specs/liquidationCall/lemma-COLasset.spec index bb029ed24..674fa00c9 100644 --- a/certora/solvency/specs/liquidationCall/lemma-COLasset.spec +++ b/certora/solvency/specs/liquidationCall/lemma-COLasset.spec @@ -29,8 +29,18 @@ methods { internal => getNormalizedDebt_hook_CVL(ret_val, aTokenAddress); function ReserveLogic._updateIndexes_hook(DataTypes.ReserveData storage reserve, - DataTypes.ReserveCache memory reserveCache) + DataTypes.ReserveCache memory reserveCache) internal => _updateIndexes_hook_CVL(reserveCache); + + function LiquidationLogic.get_userCollateralBalance() internal returns (uint256) => NONDET; + function LiquidationLogic.get_liquidationBonus() internal returns (uint256) => NONDET; + function LiquidationLogic.get_collateralAssetPrice() internal returns (uint256) => NONDET; + function LiquidationLogic.get_debtAssetPrice() internal returns (uint256) => NONDET; + function LiquidationLogic.get_collateralAssetUnit() internal returns (uint256) => NONDET; + function LiquidationLogic.get_debtAssetUnit() internal returns (uint256) => NONDET; + function LiquidationLogic.get_userReserveDebtInBaseCurrency() internal returns (uint256) => NONDET; + function LiquidationLogic.get_userReserveCollateralInBaseCurrency() internal returns (uint256) => NONDET; + } function getNormalizedIncome_hook_CVL(uint256 ret_val, address aTokenAddress) { From f6fa696226230c1564bd99b827cc046103799a98 Mon Sep 17 00:00:00 2001 From: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Date: Tue, 9 Jun 2026 11:26:47 +0300 Subject: [PATCH 4/6] duplicate summary --- certora/solvency/specs/liquidationCall/lemma-COLasset.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/solvency/specs/liquidationCall/lemma-COLasset.spec b/certora/solvency/specs/liquidationCall/lemma-COLasset.spec index 674fa00c9..dd721bc87 100644 --- a/certora/solvency/specs/liquidationCall/lemma-COLasset.spec +++ b/certora/solvency/specs/liquidationCall/lemma-COLasset.spec @@ -32,7 +32,7 @@ methods { DataTypes.ReserveCache memory reserveCache) internal => _updateIndexes_hook_CVL(reserveCache); - function LiquidationLogic.get_userCollateralBalance() internal returns (uint256) => NONDET; + function LiquidationLogic.get_liquidationBonus() internal returns (uint256) => NONDET; function LiquidationLogic.get_collateralAssetPrice() internal returns (uint256) => NONDET; function LiquidationLogic.get_debtAssetPrice() internal returns (uint256) => NONDET; @@ -40,7 +40,7 @@ methods { function LiquidationLogic.get_debtAssetUnit() internal returns (uint256) => NONDET; function LiquidationLogic.get_userReserveDebtInBaseCurrency() internal returns (uint256) => NONDET; function LiquidationLogic.get_userReserveCollateralInBaseCurrency() internal returns (uint256) => NONDET; - + } function getNormalizedIncome_hook_CVL(uint256 ret_val, address aTokenAddress) { From 549bd7f7740001b2d12165f3dd7ac6c16592c110 Mon Sep 17 00:00:00 2001 From: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Date: Tue, 9 Jun 2026 18:15:13 +0300 Subject: [PATCH 5/6] timeout settings --- .../confs/solvency/liquidationCall/lemma-COLasset.conf | 4 ++-- .../solvency/liquidationCall/main-COLasset-totSUP0.conf | 5 +++-- .../confs/solvency/liquidationCall/main-SAMEasset.conf | 4 +++- 3 files changed, 8 insertions(+), 5 deletions(-) diff --git a/certora/solvency/confs/solvency/liquidationCall/lemma-COLasset.conf b/certora/solvency/confs/solvency/liquidationCall/lemma-COLasset.conf index 1a6346ff0..495c504b4 100644 --- a/certora/solvency/confs/solvency/liquidationCall/lemma-COLasset.conf +++ b/certora/solvency/confs/solvency/liquidationCall/lemma-COLasset.conf @@ -10,8 +10,8 @@ "msg": "SOLVENCY - LIQUIDATION-CALL - COLasset lemma", "optimistic_loop": true, "process": "emv", - "prover_args": ["-depth 0" -// " -split false" + "prover_args": [ + " -destructiveOptimizations twostage -backendStrategy singleRace -smt_useLIA false -smt_useNIA true -depth 0 -s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" ], "server": "prover", "smt_timeout": "8000", diff --git a/certora/solvency/confs/solvency/liquidationCall/main-COLasset-totSUP0.conf b/certora/solvency/confs/solvency/liquidationCall/main-COLasset-totSUP0.conf index c5f87ca6d..eb13072a9 100644 --- a/certora/solvency/confs/solvency/liquidationCall/main-COLasset-totSUP0.conf +++ b/certora/solvency/confs/solvency/liquidationCall/main-COLasset-totSUP0.conf @@ -7,8 +7,9 @@ "msg": "SOLVENCY - LIQUIDATION-CALL - COLasset case totDebt==0", "optimistic_loop": true, "process": "emv", -// "prover_args": ["-depth 0"], - "prover_args": ["-splitParallel true","-dontStopAtFirstSplitTimeout true"], + "prover_args": [ + " -destructiveOptimizations twostage -s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" + ], "server": "prover", "smt_timeout": "8000", "solc": "solc8.27", diff --git a/certora/solvency/confs/solvency/liquidationCall/main-SAMEasset.conf b/certora/solvency/confs/solvency/liquidationCall/main-SAMEasset.conf index f51e71e7f..1816cdae2 100644 --- a/certora/solvency/confs/solvency/liquidationCall/main-SAMEasset.conf +++ b/certora/solvency/confs/solvency/liquidationCall/main-SAMEasset.conf @@ -8,7 +8,9 @@ "msg": "SOLVENCY - LIQUIDATION-CALL - DBT==COL main property", "optimistic_loop": true, "process": "emv", -// "prover_args": [], + "prover_args": [ + " -destructiveOptimizations twostage -s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" + ], "server": "prover", "smt_timeout": "8000", "solc": "solc8.27", From 3bd36292cdddc2f4218ec586aff44aad96cf4fde Mon Sep 17 00:00:00 2001 From: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Date: Wed, 10 Jun 2026 19:54:56 +0300 Subject: [PATCH 6/6] timeout setting --- .../confs/solvency/liquidationCall/main-COLasset.conf | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/certora/solvency/confs/solvency/liquidationCall/main-COLasset.conf b/certora/solvency/confs/solvency/liquidationCall/main-COLasset.conf index e5f61f318..3fe5123f7 100644 --- a/certora/solvency/confs/solvency/liquidationCall/main-COLasset.conf +++ b/certora/solvency/confs/solvency/liquidationCall/main-COLasset.conf @@ -8,7 +8,9 @@ "msg": "SOLVENCY - LIQUIDATION-CALL - COLasset main", "optimistic_loop": true, "process": "emv", -// "prover_args": [" -split false" ], +"prover_args": [ + " -destructiveOptimizations twostage -backendStrategy singleRace -smt_useLIA false -smt_useNIA true -depth 0 -s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" + ], "server": "prover", "smt_timeout": "8000", "solc": "solc8.27",