Skip to content

Nurit/fix sanity #184

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
nd-certora wants to merge 6 commits into
base: main
Choose a base branch
from
Open

Nurit/fix sanity #184

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
284e655
missing summary
nd-certora Jun 4, 2026
fb6c276
missing summaries
nd-certora Jun 9, 2026
ba7d517
cleanup, missing summary
nd-certora Jun 9, 2026
f6fa696
duplicate summary
nd-certora Jun 9, 2026
549bd7f
timeout settings
nd-certora Jun 9, 2026
3bd3629
timeout setting
nd-certora Jun 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions .github/workflows/certora-solvency.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions certora/solvency/confs/solvency/liquidationCall/lemma-COLasset.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
5 changes: 3 additions & 2 deletions certora/solvency/confs/solvency/liquidationCall/main-COLasset-totSUP0.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
4 changes: 3 additions & 1 deletion certora/solvency/confs/solvency/liquidationCall/main-COLasset.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
4 changes: 3 additions & 1 deletion certora/solvency/confs/solvency/liquidationCall/main-SAMEasset.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
12 changes: 11 additions & 1 deletion certora/solvency/specs/liquidationCall/lemma-COLasset-totSUP0.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -93,6 +103,7 @@ function configuration() {
/*=====================================================================================
Rule: same_indexes__liquidationCall
=====================================================================================*/

rule same_indexes__liquidationCall(env e) {
INSIDE_liquidationCall = false;
configuration();
Expand Down Expand Up @@ -120,4 +131,3 @@ rule same_indexes__liquidationCall(env e) {
assert __COL_liqIND_after == _COL_liqIND;
}


12 changes: 11 additions & 1 deletion certora/solvency/specs/liquidationCall/lemma-COLasset.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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_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) {
Expand Down
9 changes: 9 additions & 0 deletions certora/solvency/specs/liquidationCall/lemma-DBTasset.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}


Expand Down
9 changes: 9 additions & 0 deletions certora/solvency/specs/liquidationCall/lemma-SAMEasset.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}


Expand Down
11 changes: 11 additions & 0 deletions certora/solvency/specs/liquidationCall/main-COLasset-totSUP0.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
9 changes: 9 additions & 0 deletions certora/solvency/specs/liquidationCall/main-COLasset.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down
9 changes: 9 additions & 0 deletions certora/solvency/specs/liquidationCall/main-DBTasset.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
9 changes: 9 additions & 0 deletions certora/solvency/specs/liquidationCall/main-SAMEasset.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down