From 4ffb2e763d45956aadcf37e56b5d38a4c9387408 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Wed, 18 Mar 2026 09:40:29 +0100 Subject: [PATCH 1/8] Spec for balance and lossIndex --- certora/confs/BalanceAfterSlashing.conf | 22 ++++ certora/specs/BalanceAfterSlashing.spec | 139 ++++++++++++++++++++++++ src/Midnight.sol | 4 + 3 files changed, 165 insertions(+) create mode 100644 certora/confs/BalanceAfterSlashing.conf create mode 100644 certora/specs/BalanceAfterSlashing.spec diff --git a/certora/confs/BalanceAfterSlashing.conf b/certora/confs/BalanceAfterSlashing.conf new file mode 100644 index 000000000..f2268d478 --- /dev/null +++ b/certora/confs/BalanceAfterSlashing.conf @@ -0,0 +1,22 @@ +{ + "files": [ + "src/Midnight.sol" + ], + "verify": "Midnight:certora/specs/BalanceAfterSlashing.spec", + "solc": "solc-0.8.31", + "solc_via_ir": true, + "solc_evm_version": "osaka", + "optimistic_loop": true, + "loop_iter": 2, + "optimistic_hashing": true, + "hashing_length_bound": 1024, + "rule_sanity": "basic", + "multi_assert_check": true, + "smt_timeout": 7200, + "prover_args": [ + "-s", + "[z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5}]", + "-splitParallel true" + ], + "msg": "Balance After Slashing" +} diff --git a/certora/specs/BalanceAfterSlashing.spec b/certora/specs/BalanceAfterSlashing.spec new file mode 100644 index 000000000..a25197c44 --- /dev/null +++ b/certora/specs/BalanceAfterSlashing.spec @@ -0,0 +1,139 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +methods { + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function balanceOf(bytes32 id, address user) external returns (int256) envfree; + function balanceOfAfterSlashing(bytes32 id, address user) external returns (int256) envfree; + function totalUnits(bytes32 id) external returns (uint256) envfree; + function userLossIndex(bytes32 id, address user) external returns (uint128) envfree; + function obligationLossIndex(bytes32) external returns (uint128) envfree; + + function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d); + function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => NONDET; + + // Summarize price oracle as NONDET (it is a view function) + function _.price() external => NONDET; + + // Summarize safeTransfer as NONDET for now (TODO: we could also model them as external) + function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; + function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; + + // Summarize internals irrelevant to balance tracking. + function toId(Midnight.Obligation) external returns (bytes32) => NONDET; + function IdLib.storeInCode(Midnight.Obligation memory) internal returns (address) => NONDET; + function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET; + function UtilsLib.msb(uint256) internal returns (uint256) => NONDET; + function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; + function TickLib.wExp(int256) internal returns (uint256) => NONDET; + function isHealthy(Midnight.Obligation memory, bytes32, address) internal returns (bool) => NONDET; + function tradingFee(bytes32, uint256) internal returns (uint256) => NONDET; + function signer(bytes32, Midnight.Signature memory) internal returns (address) => NONDET; +} + +function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + return require_uint256(a * b / d); +} + +/// GHOST balanceAfterSlashingWithPrecision /// + +// precision is an integer that is so large that no rounding error will ever occur. +// A possible value would be 2^128! (factorial). +// We do not restrict the value but only axiomatically say that it's greater 0 and a multiple of each ownerLossIndex. +persistent ghost mathint PRECISION { + axiom PRECISION > 0; +} + +// ghost mapping for PRECISION * balanceOf(id,user) / userLossIndex(id,user) +// PRECISION ensures that the division will be without rounding errors. +ghost mapping(bytes32 => mapping(address => mathint)) preciseBalanceDivIndex { + init_state axiom forall bytes32 id. forall address user. preciseBalanceDivIndex[id][user] == 0; + // this is necessary to help the prover. It's an obvious consequence, but the usum implementation does not reason about quantifiers. + init_state axiom forall bytes32 id. (usum address user. preciseBalanceDivIndex[id][user]) == 0; +} + +/// HELPER FUNCTIONS /// + +// Map index to 1-index, for easier math. +definition mapIndex(mathint index) returns mathint = 2^128 - 1 - index; + +definition cvlBalanceOf(bytes32 id, address owner) returns int256 = currentContract.position[id][owner].balance; +definition cvlUserLossIndex(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].lossIndex; + +/// HOOKS /// + +function updateBalanceDivIndex(bytes32 id, address owner, int256 newBalance, uint128 newIndex) { + mathint ownerLossIndex = mapIndex(newIndex); + require ownerLossIndex > 0 => PRECISION * newBalance % ownerLossIndex == 0, "PRECISION is 2^128!"; + preciseBalanceDivIndex[id][owner] = + newBalance <= 0 || ownerLossIndex == 0 ? 0 : PRECISION * newBalance / ownerLossIndex; +} + +function checkBalanceDivInvariant(bytes32 id, address owner) returns bool { + int256 balance = cvlBalanceOf(id,owner); + uint128 userIndex = cvlUserLossIndex(id,owner); + mathint mappedIndex = mapIndex(userIndex); + return balance <= 0 || mappedIndex == 0 + ? preciseBalanceDivIndex[id][owner] == 0 + : preciseBalanceDivIndex[id][owner] * mappedIndex == PRECISION * balance; +} + +hook Sstore position[KEY bytes32 id][KEY address owner].balance int256 newBalance (int256 oldBalance) { + updateBalanceDivIndex(id, owner, newBalance, cvlUserLossIndex(id, owner)); +} + +hook Sstore position[KEY bytes32 id][KEY address owner].lossIndex uint128 newIndex (uint128 oldIndex) { + updateBalanceDivIndex(id, owner, cvlBalanceOf(id, owner), newIndex); +} + +/// invariants /// +strong invariant preciseBalanceCorrect(bytes32 id, address owner) + checkBalanceDivInvariant(id, owner); + +strong invariant sumOfBalancesLeTotalUnits(bytes32 id) + (usum address owner. preciseBalanceDivIndex[id][owner]) * mapIndex(obligationLossIndex(id)) <= PRECISION * totalUnits(id) +{ + preserved slash(bytes32 slashid, address user) with (env e) { + } + + preserved withdraw(Midnight.Obligation obligation, uint256 obligationUnits, address onBehalf, address receiver) with (env e) { + requireInvariant preciseBalanceCorrect(id, onBehalf); + requireInvariant obligationLossIndexLeqUserLossIndex(id, onBehalf); + } + + preserved take( + uint256 obligationUnits, + address taker, + address takerCallback, + bytes takerCallbackData, + address receiverIfTakerIsSeller, + Midnight.Offer offer, + Midnight.Signature signature, + bytes32 root, + bytes32[] proof) with (env e) { + requireInvariant preciseBalanceCorrect(id, taker); + requireInvariant obligationLossIndexLeqUserLossIndex(id, taker); + requireInvariant preciseBalanceCorrect(id, offer.maker); + requireInvariant obligationLossIndexLeqUserLossIndex(id, offer.maker); + } + +} +// The obligation loss index cannot be larger than the user loss index. +// We only need that if userLossIndex is zero so is obligationLossIndex. +strong invariant obligationLossIndexLeqUserLossIndex(bytes32 id, address owner) + mapIndex(cvlUserLossIndex(id, owner)) == 0 => mapIndex(obligationLossIndex(id)) == 0; +// mapIndex(obligationLossIndex(id)) <= mapIndex(cvlUserLossIndex(id, owner)); + +strong invariant balanceOfAfterSlashing(bytes32 id, address owner) + cvlBalanceOf(id, owner) >= 0 && mapIndex(cvlUserLossIndex(id,owner)) != 0 => + (balanceOfAfterSlashing(id, owner) == preciseBalanceDivIndex[id][owner] * mapIndex(obligationLossIndex(id)) / PRECISION) +{ + preserved { + requireInvariant preciseBalanceCorrect(id, owner); + requireInvariant obligationLossIndexLeqUserLossIndex(id, owner); + } +} diff --git a/src/Midnight.sol b/src/Midnight.sol index a0d703c5f..7b60519d0 100644 --- a/src/Midnight.sol +++ b/src/Midnight.sol @@ -587,6 +587,10 @@ contract Midnight is IMidnight { return obligationState[id].created; } + function obligationLossIndex(bytes32 id) external view returns (uint128) { + return obligationState[id].lossIndex; + } + function withdrawable(bytes32 id) external view returns (uint256) { return obligationState[id].withdrawable; } From 0803e3483380791f1d6e84ee5221da17275b0674 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Thu, 19 Mar 2026 11:31:08 +0100 Subject: [PATCH 2/8] Updated to credit/debt. --- certora/specs/BalanceAfterSlashing.spec | 64 ++++++++++++------------- 1 file changed, 32 insertions(+), 32 deletions(-) diff --git a/certora/specs/BalanceAfterSlashing.spec b/certora/specs/BalanceAfterSlashing.spec index a25197c44..056e8b3f3 100644 --- a/certora/specs/BalanceAfterSlashing.spec +++ b/certora/specs/BalanceAfterSlashing.spec @@ -3,8 +3,8 @@ methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; - function balanceOf(bytes32 id, address user) external returns (int256) envfree; - function balanceOfAfterSlashing(bytes32 id, address user) external returns (int256) envfree; + function creditOf(bytes32 id, address user) external returns (uint256) envfree; + function creditAfterSlashing(bytes32 id, address user) external returns (uint256) envfree; function totalUnits(bytes32 id) external returns (uint256) envfree; function userLossIndex(bytes32 id, address user) external returns (uint128) envfree; function obligationLossIndex(bytes32) external returns (uint128) envfree; @@ -19,7 +19,7 @@ methods { function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; - // Summarize internals irrelevant to balance tracking. + // Summarize internals irrelevant to credit tracking. function toId(Midnight.Obligation) external returns (bytes32) => NONDET; function IdLib.storeInCode(Midnight.Obligation memory) internal returns (address) => NONDET; function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET; @@ -39,7 +39,7 @@ function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { return require_uint256(a * b / d); } -/// GHOST balanceAfterSlashingWithPrecision /// +/// GHOST creditAfterSlashingWithPrecision /// // precision is an integer that is so large that no rounding error will ever occur. // A possible value would be 2^128! (factorial). @@ -48,12 +48,12 @@ persistent ghost mathint PRECISION { axiom PRECISION > 0; } -// ghost mapping for PRECISION * balanceOf(id,user) / userLossIndex(id,user) +// ghost mapping for PRECISION * creditOf(id,user) / userLossIndex(id,user) // PRECISION ensures that the division will be without rounding errors. -ghost mapping(bytes32 => mapping(address => mathint)) preciseBalanceDivIndex { - init_state axiom forall bytes32 id. forall address user. preciseBalanceDivIndex[id][user] == 0; +ghost mapping(bytes32 => mapping(address => mathint)) preciseCreditDivIndex { + init_state axiom forall bytes32 id. forall address user. preciseCreditDivIndex[id][user] == 0; // this is necessary to help the prover. It's an obvious consequence, but the usum implementation does not reason about quantifiers. - init_state axiom forall bytes32 id. (usum address user. preciseBalanceDivIndex[id][user]) == 0; + init_state axiom forall bytes32 id. (usum address user. preciseCreditDivIndex[id][user]) == 0; } /// HELPER FUNCTIONS /// @@ -61,47 +61,47 @@ ghost mapping(bytes32 => mapping(address => mathint)) preciseBalanceDivIndex { // Map index to 1-index, for easier math. definition mapIndex(mathint index) returns mathint = 2^128 - 1 - index; -definition cvlBalanceOf(bytes32 id, address owner) returns int256 = currentContract.position[id][owner].balance; +definition cvlCreditOf(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].credit; definition cvlUserLossIndex(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].lossIndex; /// HOOKS /// -function updateBalanceDivIndex(bytes32 id, address owner, int256 newBalance, uint128 newIndex) { +function updateCreditDivIndex(bytes32 id, address owner, uint128 newCredit, uint128 newIndex) { mathint ownerLossIndex = mapIndex(newIndex); - require ownerLossIndex > 0 => PRECISION * newBalance % ownerLossIndex == 0, "PRECISION is 2^128!"; - preciseBalanceDivIndex[id][owner] = - newBalance <= 0 || ownerLossIndex == 0 ? 0 : PRECISION * newBalance / ownerLossIndex; + require ownerLossIndex > 0 => PRECISION * newCredit % ownerLossIndex == 0, "PRECISION is 2^128!"; + preciseCreditDivIndex[id][owner] = + ownerLossIndex == 0 ? 0 : PRECISION * newCredit / ownerLossIndex; } -function checkBalanceDivInvariant(bytes32 id, address owner) returns bool { - int256 balance = cvlBalanceOf(id,owner); +function checkCreditDivInvariant(bytes32 id, address owner) returns bool { + uint128 credit = cvlCreditOf(id,owner); uint128 userIndex = cvlUserLossIndex(id,owner); mathint mappedIndex = mapIndex(userIndex); - return balance <= 0 || mappedIndex == 0 - ? preciseBalanceDivIndex[id][owner] == 0 - : preciseBalanceDivIndex[id][owner] * mappedIndex == PRECISION * balance; + return mappedIndex == 0 + ? preciseCreditDivIndex[id][owner] == 0 + : preciseCreditDivIndex[id][owner] * mappedIndex == PRECISION * credit; } -hook Sstore position[KEY bytes32 id][KEY address owner].balance int256 newBalance (int256 oldBalance) { - updateBalanceDivIndex(id, owner, newBalance, cvlUserLossIndex(id, owner)); +hook Sstore position[KEY bytes32 id][KEY address owner].credit uint128 newCredit (uint128 oldCredit) { + updateCreditDivIndex(id, owner, newCredit, cvlUserLossIndex(id, owner)); } hook Sstore position[KEY bytes32 id][KEY address owner].lossIndex uint128 newIndex (uint128 oldIndex) { - updateBalanceDivIndex(id, owner, cvlBalanceOf(id, owner), newIndex); + updateCreditDivIndex(id, owner, cvlCreditOf(id, owner), newIndex); } /// invariants /// -strong invariant preciseBalanceCorrect(bytes32 id, address owner) - checkBalanceDivInvariant(id, owner); +strong invariant preciseCreditCorrect(bytes32 id, address owner) + checkCreditDivInvariant(id, owner); -strong invariant sumOfBalancesLeTotalUnits(bytes32 id) - (usum address owner. preciseBalanceDivIndex[id][owner]) * mapIndex(obligationLossIndex(id)) <= PRECISION * totalUnits(id) +strong invariant sumOfCreditsLeTotalUnits(bytes32 id) + (usum address owner. preciseCreditDivIndex[id][owner]) * mapIndex(obligationLossIndex(id)) <= PRECISION * totalUnits(id) { preserved slash(bytes32 slashid, address user) with (env e) { } preserved withdraw(Midnight.Obligation obligation, uint256 obligationUnits, address onBehalf, address receiver) with (env e) { - requireInvariant preciseBalanceCorrect(id, onBehalf); + requireInvariant preciseCreditCorrect(id, onBehalf); requireInvariant obligationLossIndexLeqUserLossIndex(id, onBehalf); } @@ -115,9 +115,9 @@ strong invariant sumOfBalancesLeTotalUnits(bytes32 id) Midnight.Signature signature, bytes32 root, bytes32[] proof) with (env e) { - requireInvariant preciseBalanceCorrect(id, taker); + requireInvariant preciseCreditCorrect(id, taker); requireInvariant obligationLossIndexLeqUserLossIndex(id, taker); - requireInvariant preciseBalanceCorrect(id, offer.maker); + requireInvariant preciseCreditCorrect(id, offer.maker); requireInvariant obligationLossIndexLeqUserLossIndex(id, offer.maker); } @@ -128,12 +128,12 @@ strong invariant obligationLossIndexLeqUserLossIndex(bytes32 id, address owner) mapIndex(cvlUserLossIndex(id, owner)) == 0 => mapIndex(obligationLossIndex(id)) == 0; // mapIndex(obligationLossIndex(id)) <= mapIndex(cvlUserLossIndex(id, owner)); -strong invariant balanceOfAfterSlashing(bytes32 id, address owner) - cvlBalanceOf(id, owner) >= 0 && mapIndex(cvlUserLossIndex(id,owner)) != 0 => - (balanceOfAfterSlashing(id, owner) == preciseBalanceDivIndex[id][owner] * mapIndex(obligationLossIndex(id)) / PRECISION) +strong invariant creditAfterSlashingValue(bytes32 id, address owner) + mapIndex(cvlUserLossIndex(id,owner)) != 0 => + (creditAfterSlashing(id, owner) == preciseCreditDivIndex[id][owner] * mapIndex(obligationLossIndex(id)) / PRECISION) { preserved { - requireInvariant preciseBalanceCorrect(id, owner); + requireInvariant preciseCreditCorrect(id, owner); requireInvariant obligationLossIndexLeqUserLossIndex(id, owner); } } From c60fa1ab8a8a7819c4273d06d575aff5f81b72ad Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Thu, 19 Mar 2026 11:40:04 +0100 Subject: [PATCH 3/8] Fix slash preserve block --- certora/specs/BalanceAfterSlashing.spec | 2 ++ 1 file changed, 2 insertions(+) diff --git a/certora/specs/BalanceAfterSlashing.spec b/certora/specs/BalanceAfterSlashing.spec index 056e8b3f3..38c04a938 100644 --- a/certora/specs/BalanceAfterSlashing.spec +++ b/certora/specs/BalanceAfterSlashing.spec @@ -98,6 +98,8 @@ strong invariant sumOfCreditsLeTotalUnits(bytes32 id) (usum address owner. preciseCreditDivIndex[id][owner]) * mapIndex(obligationLossIndex(id)) <= PRECISION * totalUnits(id) { preserved slash(bytes32 slashid, address user) with (env e) { + requireInvariant preciseCreditCorrect(id, user); + requireInvariant obligationLossIndexLeqUserLossIndex(id, user); } preserved withdraw(Midnight.Obligation obligation, uint256 obligationUnits, address onBehalf, address receiver) with (env e) { From c5c7928932ca8dc049b7e6e9435a088e5a8ae5ea Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 24 Mar 2026 22:17:40 +0100 Subject: [PATCH 4/8] Added preserved for liquidate --- certora/specs/BalanceAfterSlashing.spec | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/certora/specs/BalanceAfterSlashing.spec b/certora/specs/BalanceAfterSlashing.spec index 38c04a938..2811c33a1 100644 --- a/certora/specs/BalanceAfterSlashing.spec +++ b/certora/specs/BalanceAfterSlashing.spec @@ -107,6 +107,18 @@ strong invariant sumOfCreditsLeTotalUnits(bytes32 id) requireInvariant obligationLossIndexLeqUserLossIndex(id, onBehalf); } + preserved liquidate( + Midnight.Obligation obligation, + uint256 collateralIndex, + uint256 seizedAssets, + uint256 repaidUnits, + address borrower, + bytes data + ) with (env e) { + requireInvariant preciseCreditCorrect(id, borrower); + requireInvariant obligationLossIndexLeqUserLossIndex(id, borrower); + } + preserved take( uint256 obligationUnits, address taker, From 0b8a229cc117cb3a84fa059bf4590f6dfa30471f Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 7 Apr 2026 14:27:56 +0200 Subject: [PATCH 5/8] passive fee recipient update --- certora/confs/BalanceAfterSlashing.conf | 1 + certora/helpers/MidnightWrapper.sol | 6 +- certora/specs/BalanceAfterSlashing.spec | 92 +++++++++++++++++++++---- 3 files changed, 85 insertions(+), 14 deletions(-) diff --git a/certora/confs/BalanceAfterSlashing.conf b/certora/confs/BalanceAfterSlashing.conf index f2268d478..a9ca47b0c 100644 --- a/certora/confs/BalanceAfterSlashing.conf +++ b/certora/confs/BalanceAfterSlashing.conf @@ -1,5 +1,6 @@ { "files": [ + //"certora/helpers/MidnightWrapper.sol" "src/Midnight.sol" ], "verify": "Midnight:certora/specs/BalanceAfterSlashing.spec", diff --git a/certora/helpers/MidnightWrapper.sol b/certora/helpers/MidnightWrapper.sol index bfe549d3f..5c0196d31 100644 --- a/certora/helpers/MidnightWrapper.sol +++ b/certora/helpers/MidnightWrapper.sol @@ -6,7 +6,7 @@ import {Midnight} from "../../src/Midnight.sol"; import {Position, Collateral, Obligation} from "../../src/interfaces/IMidnight.sol"; import {IOracle} from "../../src/interfaces/IOracle.sol"; import {UtilsLib} from "../../src/libraries/UtilsLib.sol"; -import {ORACLE_PRICE_SCALE, WAD} from "../../src/libraries/ConstantsLib.sol"; +import {ORACLE_PRICE_SCALE, WAD, PASSIVE_FEE_RECIPIENT} from "../../src/libraries/ConstantsLib.sol"; contract MidnightWrapper is Midnight { using UtilsLib for uint256; @@ -27,4 +27,8 @@ contract MidnightWrapper is Midnight { } return maxDebt >= debt; } + + function getPassiveFeeRecipient() public pure returns (address) { + return PASSIVE_FEE_RECIPIENT; + } } diff --git a/certora/specs/BalanceAfterSlashing.spec b/certora/specs/BalanceAfterSlashing.spec index 2811c33a1..6038979bb 100644 --- a/certora/specs/BalanceAfterSlashing.spec +++ b/certora/specs/BalanceAfterSlashing.spec @@ -3,14 +3,16 @@ methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; + //function getPassiveFeeRecipient() external returns address envfree; + function creditOf(bytes32 id, address user) external returns (uint256) envfree; - function creditAfterSlashing(bytes32 id, address user) external returns (uint256) envfree; + function updatePositionView(Midnight.Obligation memory obligation, bytes32 id, address user) external returns (uint128, uint128, uint128); function totalUnits(bytes32 id) external returns (uint256) envfree; function userLossIndex(bytes32 id, address user) external returns (uint128) envfree; function obligationLossIndex(bytes32) external returns (uint128) envfree; - function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d); - function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => NONDET; + //function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d); + //function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => NONDET; // Summarize price oracle as NONDET (it is a view function) function _.price() external => NONDET; @@ -23,14 +25,16 @@ methods { function toId(Midnight.Obligation) external returns (bytes32) => NONDET; function IdLib.storeInCode(Midnight.Obligation memory) internal returns (address) => NONDET; function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET; - function UtilsLib.msb(uint256) internal returns (uint256) => NONDET; + function UtilsLib.msb(uint128) internal returns (uint256) => NONDET; function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; function TickLib.wExp(int256) internal returns (uint256) => NONDET; function isHealthy(Midnight.Obligation memory, bytes32, address) internal returns (bool) => NONDET; function tradingFee(bytes32, uint256) internal returns (uint256) => NONDET; - function signer(bytes32, Midnight.Signature memory) internal returns (address) => NONDET; + function Midnight.signer(bytes32, Midnight.Signature memory) internal returns (address) => NONDET; } +definition PASSIVE_FEE_RECIPIENT() returns address = 0x7e3dce7c19791d65d67ef7ce3c42d2b7fe6fecb1; //currentContract.getPassiveFeeRecipient(); + function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { bool overflow; if (overflow || d == 0) { @@ -56,6 +60,14 @@ ghost mapping(bytes32 => mapping(address => mathint)) preciseCreditDivIndex { init_state axiom forall bytes32 id. (usum address user. preciseCreditDivIndex[id][user]) == 0; } +ghost mapping(bytes32 => mapping(address => mathint)) pendingFeeMirror { + init_state axiom forall bytes32 id. forall address user. pendingFeeMirror[id][user] == 0; +} +ghost mapping(bytes32 => mapping(address => mathint)) lastAccrualMirror { + init_state axiom forall bytes32 id. forall address user. lastAccrualMirror[id][user] == 0; +} + + /// HELPER FUNCTIONS /// // Map index to 1-index, for easier math. @@ -90,6 +102,23 @@ hook Sstore position[KEY bytes32 id][KEY address owner].lossIndex uint128 newInd updateCreditDivIndex(id, owner, cvlCreditOf(id, owner), newIndex); } +hook Sload uint128 value position[KEY bytes32 id][KEY address owner].pendingFee +{ + require pendingFeeMirror[id][owner] == value, "ghost mirror"; +} +hook Sload uint128 value position[KEY bytes32 id][KEY address owner].lastAccrual +{ + require lastAccrualMirror[id][owner] == value, "ghost mirror"; +} +hook Sstore position[KEY bytes32 id][KEY address owner].pendingFee uint128 newPending (uint128 oldPending) +{ + pendingFeeMirror[id][owner] = newPending; +} +hook Sstore position[KEY bytes32 id][KEY address owner].lastAccrual uint128 newLast (uint128 oldLast) +{ + lastAccrualMirror[id][owner] = newLast; +} + /// invariants /// strong invariant preciseCreditCorrect(bytes32 id, address owner) checkCreditDivInvariant(id, owner); @@ -97,12 +126,16 @@ strong invariant preciseCreditCorrect(bytes32 id, address owner) strong invariant sumOfCreditsLeTotalUnits(bytes32 id) (usum address owner. preciseCreditDivIndex[id][owner]) * mapIndex(obligationLossIndex(id)) <= PRECISION * totalUnits(id) { - preserved slash(bytes32 slashid, address user) with (env e) { + preserved updatePosition(Midnight.Obligation obligation, address user) with (env e) { + //requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); requireInvariant preciseCreditCorrect(id, user); requireInvariant obligationLossIndexLeqUserLossIndex(id, user); } preserved withdraw(Midnight.Obligation obligation, uint256 obligationUnits, address onBehalf, address receiver) with (env e) { + //requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); requireInvariant preciseCreditCorrect(id, onBehalf); requireInvariant obligationLossIndexLeqUserLossIndex(id, onBehalf); } @@ -115,6 +148,8 @@ strong invariant sumOfCreditsLeTotalUnits(bytes32 id) address borrower, bytes data ) with (env e) { + //requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); requireInvariant preciseCreditCorrect(id, borrower); requireInvariant obligationLossIndexLeqUserLossIndex(id, borrower); } @@ -129,6 +164,8 @@ strong invariant sumOfCreditsLeTotalUnits(bytes32 id) Midnight.Signature signature, bytes32 root, bytes32[] proof) with (env e) { + //requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); requireInvariant preciseCreditCorrect(id, taker); requireInvariant obligationLossIndexLeqUserLossIndex(id, taker); requireInvariant preciseCreditCorrect(id, offer.maker); @@ -142,12 +179,41 @@ strong invariant obligationLossIndexLeqUserLossIndex(bytes32 id, address owner) mapIndex(cvlUserLossIndex(id, owner)) == 0 => mapIndex(obligationLossIndex(id)) == 0; // mapIndex(obligationLossIndex(id)) <= mapIndex(cvlUserLossIndex(id, owner)); -strong invariant creditAfterSlashingValue(bytes32 id, address owner) - mapIndex(cvlUserLossIndex(id,owner)) != 0 => - (creditAfterSlashing(id, owner) == preciseCreditDivIndex[id][owner] * mapIndex(obligationLossIndex(id)) / PRECISION) +rule updatePositionViewReflectedByIndex(env e, Midnight.Obligation obligation, bytes32 id, address owner) { - preserved { - requireInvariant preciseCreditCorrect(id, owner); - requireInvariant obligationLossIndexLeqUserLossIndex(id, owner); - } + requireInvariant preciseCreditCorrect(id, owner); + requireInvariant obligationLossIndexLeqUserLossIndex(id, owner); + + uint128 newCredit; + uint128 newPending; + uint128 fee; + + mathint preciseCreditBefore = preciseCreditDivIndex[id][owner] * mapIndex(obligationLossIndex(id)); + mathint pendingBefore = pendingFeeMirror[id][owner]; + mathint lastAccrualBefore = lastAccrualMirror[id][owner]; + + require e.block.timestamp >= lastAccrualBefore, "Time is increasing"; + + newCredit, newPending, fee = updatePositionView(e, obligation, id, owner); + + assert fee <= pendingBefore, "Cannot take more fee than pending"; + assert (newCredit + fee) * PRECISION <= preciseCreditBefore, "newCredit (with fees) is at most precise credit after slashing"; } + +rule updatePositionZero(env e, Midnight.Obligation obligation, bytes32 id, address owner) { + require currentContract.position[id][owner].credit == 0, "Assume no credit"; + + uint128 newCredit; + uint128 newPending; + uint128 fee; + newCredit, newPending, fee = updatePositionView(e, obligation, id, owner); + + assert newCredit == 0 && newPending == 0 && fee == 0; +} + + +invariant pendingFeeLessEqualThanCredit(bytes32 id, address user) + currentContract.position[id][user].pendingFee <= currentContract.position[id][user].credit; + +invariant pendingFeeLessThanCredit(bytes32 id, address user) + currentContract.position[id][user].pendingFee < currentContract.position[id][user].credit || currentContract.position[id][user].pendingFee == 0; From 243dc618ba05d5c799afef98b9d851f270687f6f Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 7 Apr 2026 15:13:07 +0200 Subject: [PATCH 6/8] fix invariant --- certora/specs/BalanceAfterSlashing.spec | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/certora/specs/BalanceAfterSlashing.spec b/certora/specs/BalanceAfterSlashing.spec index 6038979bb..d6d86cd2e 100644 --- a/certora/specs/BalanceAfterSlashing.spec +++ b/certora/specs/BalanceAfterSlashing.spec @@ -127,14 +127,14 @@ strong invariant sumOfCreditsLeTotalUnits(bytes32 id) (usum address owner. preciseCreditDivIndex[id][owner]) * mapIndex(obligationLossIndex(id)) <= PRECISION * totalUnits(id) { preserved updatePosition(Midnight.Obligation obligation, address user) with (env e) { - //requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); requireInvariant preciseCreditCorrect(id, user); requireInvariant obligationLossIndexLeqUserLossIndex(id, user); } preserved withdraw(Midnight.Obligation obligation, uint256 obligationUnits, address onBehalf, address receiver) with (env e) { - //requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); requireInvariant preciseCreditCorrect(id, onBehalf); requireInvariant obligationLossIndexLeqUserLossIndex(id, onBehalf); @@ -148,7 +148,7 @@ strong invariant sumOfCreditsLeTotalUnits(bytes32 id) address borrower, bytes data ) with (env e) { - //requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); requireInvariant preciseCreditCorrect(id, borrower); requireInvariant obligationLossIndexLeqUserLossIndex(id, borrower); @@ -174,10 +174,8 @@ strong invariant sumOfCreditsLeTotalUnits(bytes32 id) } // The obligation loss index cannot be larger than the user loss index. -// We only need that if userLossIndex is zero so is obligationLossIndex. strong invariant obligationLossIndexLeqUserLossIndex(bytes32 id, address owner) - mapIndex(cvlUserLossIndex(id, owner)) == 0 => mapIndex(obligationLossIndex(id)) == 0; -// mapIndex(obligationLossIndex(id)) <= mapIndex(cvlUserLossIndex(id, owner)); + mapIndex(obligationLossIndex(id)) <= mapIndex(cvlUserLossIndex(id, owner)); rule updatePositionViewReflectedByIndex(env e, Midnight.Obligation obligation, bytes32 id, address owner) { From 91e6abe11e14155375058abf7b2b4de2cad62615 Mon Sep 17 00:00:00 2001 From: lilCertora Date: Thu, 30 Apr 2026 09:34:34 +0200 Subject: [PATCH 7/8] update latest solidity + midnight version + comment last invariant + add hashOffer,isLeaf summaries --- certora/confs/BalanceAfterSlashing.conf | 2 +- certora/specs/BalanceAfterSlashing.spec | 138 +++++++++++------------- 2 files changed, 65 insertions(+), 75 deletions(-) diff --git a/certora/confs/BalanceAfterSlashing.conf b/certora/confs/BalanceAfterSlashing.conf index a9ca47b0c..2b0caf209 100644 --- a/certora/confs/BalanceAfterSlashing.conf +++ b/certora/confs/BalanceAfterSlashing.conf @@ -4,7 +4,7 @@ "src/Midnight.sol" ], "verify": "Midnight:certora/specs/BalanceAfterSlashing.spec", - "solc": "solc-0.8.31", + "solc": "solc-0.8.34", "solc_via_ir": true, "solc_evm_version": "osaka", "optimistic_loop": true, diff --git a/certora/specs/BalanceAfterSlashing.spec b/certora/specs/BalanceAfterSlashing.spec index d6d86cd2e..21e0e6996 100644 --- a/certora/specs/BalanceAfterSlashing.spec +++ b/certora/specs/BalanceAfterSlashing.spec @@ -8,6 +8,7 @@ methods { function creditOf(bytes32 id, address user) external returns (uint256) envfree; function updatePositionView(Midnight.Obligation memory obligation, bytes32 id, address user) external returns (uint128, uint128, uint128); function totalUnits(bytes32 id) external returns (uint256) envfree; + function continuousFeeCredit(bytes32 id) external returns (uint256) envfree; function userLossIndex(bytes32 id, address user) external returns (uint128) envfree; function obligationLossIndex(bytes32) external returns (uint128) envfree; @@ -17,20 +18,29 @@ methods { // Summarize price oracle as NONDET (it is a view function) function _.price() external => NONDET; - // Summarize safeTransfer as NONDET for now (TODO: we could also model them as external) - function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; - function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; - // Summarize internals irrelevant to credit tracking. function toId(Midnight.Obligation) external returns (bytes32) => NONDET; function IdLib.storeInCode(Midnight.Obligation memory) internal returns (address) => NONDET; + function UtilsLib.hashOffer(Midnight.Offer memory) internal returns (bytes32) => NONDET; function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET; function UtilsLib.msb(uint128) internal returns (uint256) => NONDET; function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; function TickLib.wExp(int256) internal returns (uint256) => NONDET; function isHealthy(Midnight.Obligation memory, bytes32, address) internal returns (bool) => NONDET; function tradingFee(bytes32, uint256) internal returns (uint256) => NONDET; - function Midnight.signer(bytes32, Midnight.Signature memory) internal returns (address) => NONDET; + + // Assume no reentrancy: callbacks, gates, and token transfers do not re-enter Midnight. + function _.onBuy(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET; + function _.onSell(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET; + function _.onRatify(Midnight.Offer, bytes32, bytes) external => NONDET; + function _.onLiquidate(bytes32, Midnight.Obligation, uint256, uint256, uint256, address, bytes) external => NONDET; + function _.canIncreaseCredit(address) external => NONDET; + function _.canIncreaseDebt(address) external => NONDET; + function _.canLiquidate(address) external => NONDET; + + // Summarize safeTransfer as NONDET for now (TODO: we could also model them as external) + function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; + function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; } definition PASSIVE_FEE_RECIPIENT() returns address = 0x7e3dce7c19791d65d67ef7ce3c42d2b7fe6fecb1; //currentContract.getPassiveFeeRecipient(); @@ -56,6 +66,7 @@ persistent ghost mathint PRECISION { // PRECISION ensures that the division will be without rounding errors. ghost mapping(bytes32 => mapping(address => mathint)) preciseCreditDivIndex { init_state axiom forall bytes32 id. forall address user. preciseCreditDivIndex[id][user] == 0; + // this is necessary to help the prover. It's an obvious consequence, but the usum implementation does not reason about quantifiers. init_state axiom forall bytes32 id. (usum address user. preciseCreditDivIndex[id][user]) == 0; } @@ -63,17 +74,18 @@ ghost mapping(bytes32 => mapping(address => mathint)) preciseCreditDivIndex { ghost mapping(bytes32 => mapping(address => mathint)) pendingFeeMirror { init_state axiom forall bytes32 id. forall address user. pendingFeeMirror[id][user] == 0; } + ghost mapping(bytes32 => mapping(address => mathint)) lastAccrualMirror { init_state axiom forall bytes32 id. forall address user. lastAccrualMirror[id][user] == 0; } - /// HELPER FUNCTIONS /// // Map index to 1-index, for easier math. -definition mapIndex(mathint index) returns mathint = 2^128 - 1 - index; +definition mapIndex(mathint index) returns mathint = 2 ^ 128 - 1 - index; definition cvlCreditOf(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].credit; + definition cvlUserLossIndex(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].lossIndex; /// HOOKS /// @@ -81,17 +93,14 @@ definition cvlUserLossIndex(bytes32 id, address owner) returns uint128 = current function updateCreditDivIndex(bytes32 id, address owner, uint128 newCredit, uint128 newIndex) { mathint ownerLossIndex = mapIndex(newIndex); require ownerLossIndex > 0 => PRECISION * newCredit % ownerLossIndex == 0, "PRECISION is 2^128!"; - preciseCreditDivIndex[id][owner] = - ownerLossIndex == 0 ? 0 : PRECISION * newCredit / ownerLossIndex; + preciseCreditDivIndex[id][owner] = ownerLossIndex == 0 ? 0 : PRECISION * newCredit / ownerLossIndex; } function checkCreditDivInvariant(bytes32 id, address owner) returns bool { - uint128 credit = cvlCreditOf(id,owner); - uint128 userIndex = cvlUserLossIndex(id,owner); + uint128 credit = cvlCreditOf(id, owner); + uint128 userIndex = cvlUserLossIndex(id, owner); mathint mappedIndex = mapIndex(userIndex); - return mappedIndex == 0 - ? preciseCreditDivIndex[id][owner] == 0 - : preciseCreditDivIndex[id][owner] * mappedIndex == PRECISION * credit; + return mappedIndex == 0 ? preciseCreditDivIndex[id][owner] == 0 : preciseCreditDivIndex[id][owner] * mappedIndex == PRECISION * credit; } hook Sstore position[KEY bytes32 id][KEY address owner].credit uint128 newCredit (uint128 oldCredit) { @@ -102,20 +111,19 @@ hook Sstore position[KEY bytes32 id][KEY address owner].lossIndex uint128 newInd updateCreditDivIndex(id, owner, cvlCreditOf(id, owner), newIndex); } -hook Sload uint128 value position[KEY bytes32 id][KEY address owner].pendingFee -{ +hook Sload uint128 value position[KEY bytes32 id][KEY address owner].pendingFee { require pendingFeeMirror[id][owner] == value, "ghost mirror"; } -hook Sload uint128 value position[KEY bytes32 id][KEY address owner].lastAccrual -{ + +hook Sload uint128 value position[KEY bytes32 id][KEY address owner].lastAccrual { require lastAccrualMirror[id][owner] == value, "ghost mirror"; } -hook Sstore position[KEY bytes32 id][KEY address owner].pendingFee uint128 newPending (uint128 oldPending) -{ + +hook Sstore position[KEY bytes32 id][KEY address owner].pendingFee uint128 newPending (uint128 oldPending) { pendingFeeMirror[id][owner] = newPending; } -hook Sstore position[KEY bytes32 id][KEY address owner].lastAccrual uint128 newLast (uint128 oldLast) -{ + +hook Sstore position[KEY bytes32 id][KEY address owner].lastAccrual uint128 newLast (uint128 oldLast) { lastAccrualMirror[id][owner] = newLast; } @@ -124,61 +132,44 @@ strong invariant preciseCreditCorrect(bytes32 id, address owner) checkCreditDivInvariant(id, owner); strong invariant sumOfCreditsLeTotalUnits(bytes32 id) - (usum address owner. preciseCreditDivIndex[id][owner]) * mapIndex(obligationLossIndex(id)) <= PRECISION * totalUnits(id) -{ - preserved updatePosition(Midnight.Obligation obligation, address user) with (env e) { - requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); - requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); - requireInvariant preciseCreditCorrect(id, user); - requireInvariant obligationLossIndexLeqUserLossIndex(id, user); - } - - preserved withdraw(Midnight.Obligation obligation, uint256 obligationUnits, address onBehalf, address receiver) with (env e) { - requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); - requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); - requireInvariant preciseCreditCorrect(id, onBehalf); - requireInvariant obligationLossIndexLeqUserLossIndex(id, onBehalf); + (usum address owner. preciseCreditDivIndex[id][owner]) * mapIndex(obligationLossIndex(id)) + PRECISION * continuousFeeCredit(id) <= PRECISION * totalUnits(id) + { + preserved updatePosition(Midnight.Obligation obligation, address user) with (env e) { + requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant preciseCreditCorrect(id, user); + requireInvariant obligationLossIndexLeqUserLossIndex(id, user); + } + + preserved withdraw(Midnight.Obligation obligation, uint256 obligationUnits, address onBehalf, address receiver) with (env e) { + requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant preciseCreditCorrect(id, onBehalf); + requireInvariant obligationLossIndexLeqUserLossIndex(id, onBehalf); + } + + preserved liquidate(Midnight.Obligation obligation, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) with (env e) { + requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant preciseCreditCorrect(id, borrower); + requireInvariant obligationLossIndexLeqUserLossIndex(id, borrower); + } + + preserved take(uint256 obligationUnits, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) with (env e) { + //requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant preciseCreditCorrect(id, taker); + requireInvariant obligationLossIndexLeqUserLossIndex(id, taker); + requireInvariant preciseCreditCorrect(id, offer.maker); + requireInvariant obligationLossIndexLeqUserLossIndex(id, offer.maker); + } } - preserved liquidate( - Midnight.Obligation obligation, - uint256 collateralIndex, - uint256 seizedAssets, - uint256 repaidUnits, - address borrower, - bytes data - ) with (env e) { - requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); - requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); - requireInvariant preciseCreditCorrect(id, borrower); - requireInvariant obligationLossIndexLeqUserLossIndex(id, borrower); - } - - preserved take( - uint256 obligationUnits, - address taker, - address takerCallback, - bytes takerCallbackData, - address receiverIfTakerIsSeller, - Midnight.Offer offer, - Midnight.Signature signature, - bytes32 root, - bytes32[] proof) with (env e) { - //requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); - requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); - requireInvariant preciseCreditCorrect(id, taker); - requireInvariant obligationLossIndexLeqUserLossIndex(id, taker); - requireInvariant preciseCreditCorrect(id, offer.maker); - requireInvariant obligationLossIndexLeqUserLossIndex(id, offer.maker); - } - -} // The obligation loss index cannot be larger than the user loss index. strong invariant obligationLossIndexLeqUserLossIndex(bytes32 id, address owner) mapIndex(obligationLossIndex(id)) <= mapIndex(cvlUserLossIndex(id, owner)); -rule updatePositionViewReflectedByIndex(env e, Midnight.Obligation obligation, bytes32 id, address owner) -{ +rule updatePositionViewReflectedByIndex(env e, Midnight.Obligation obligation, bytes32 id, address owner) { requireInvariant preciseCreditCorrect(id, owner); requireInvariant obligationLossIndexLeqUserLossIndex(id, owner); @@ -209,9 +200,8 @@ rule updatePositionZero(env e, Midnight.Obligation obligation, bytes32 id, addre assert newCredit == 0 && newPending == 0 && fee == 0; } - invariant pendingFeeLessEqualThanCredit(bytes32 id, address user) currentContract.position[id][user].pendingFee <= currentContract.position[id][user].credit; -invariant pendingFeeLessThanCredit(bytes32 id, address user) - currentContract.position[id][user].pendingFee < currentContract.position[id][user].credit || currentContract.position[id][user].pendingFee == 0; +//invariant pendingFeeLessThanCredit(bytes32 id, address user) +// currentContract.position[id][user].pendingFee < currentContract.position[id][user].credit || currentContract.position[id][user].pendingFee == 0; From b508cffb8989380ca6ef781c478f17520b5b0c0d Mon Sep 17 00:00:00 2001 From: lilCertora Date: Thu, 30 Apr 2026 16:23:50 +0200 Subject: [PATCH 8/8] update to latest version midnight + add hashOffer nondet --- certora/confs/BalanceAfterSlashing.conf | 11 +- certora/specs/BalanceAfterSlashing.spec | 139 +++++++++++++++--------- 2 files changed, 97 insertions(+), 53 deletions(-) diff --git a/certora/confs/BalanceAfterSlashing.conf b/certora/confs/BalanceAfterSlashing.conf index 2b0caf209..16de73e8e 100644 --- a/certora/confs/BalanceAfterSlashing.conf +++ b/certora/confs/BalanceAfterSlashing.conf @@ -1,9 +1,9 @@ { "files": [ - //"certora/helpers/MidnightWrapper.sol" "src/Midnight.sol" ], "verify": "Midnight:certora/specs/BalanceAfterSlashing.spec", + "parametric_contracts": ["Midnight"], "solc": "solc-0.8.34", "solc_via_ir": true, "solc_evm_version": "osaka", @@ -11,13 +11,16 @@ "loop_iter": 2, "optimistic_hashing": true, "hashing_length_bound": 1024, - "rule_sanity": "basic", "multi_assert_check": true, "smt_timeout": 7200, + "build_cache": true, "prover_args": [ + "-destructiveOptimizations twostage", + "-mediumTimeout 20", + "-depth 5", + "-splitParallel true", "-s", - "[z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5}]", - "-splitParallel true" + "[z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5}]" ], "msg": "Balance After Slashing" } diff --git a/certora/specs/BalanceAfterSlashing.spec b/certora/specs/BalanceAfterSlashing.spec index 21e0e6996..c65ccd5c0 100644 --- a/certora/specs/BalanceAfterSlashing.spec +++ b/certora/specs/BalanceAfterSlashing.spec @@ -3,22 +3,32 @@ methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; - //function getPassiveFeeRecipient() external returns address envfree; - function creditOf(bytes32 id, address user) external returns (uint256) envfree; - function updatePositionView(Midnight.Obligation memory obligation, bytes32 id, address user) external returns (uint128, uint128, uint128); function totalUnits(bytes32 id) external returns (uint256) envfree; function continuousFeeCredit(bytes32 id) external returns (uint256) envfree; function userLossIndex(bytes32 id, address user) external returns (uint128) envfree; function obligationLossIndex(bytes32) external returns (uint128) envfree; - //function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d); - //function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => NONDET; + // updatePositionView is used in two regular rules but is not envfree (uses block.timestamp). + // Mark optional to silence the spec syntax warning when verifying parametric/invariant rules + // that do not exercise it directly. Note: no `memory` location specifier — CVL rejects it + // on non-library external method declarations. + function updatePositionView(Midnight.Obligation, bytes32, address) external returns (uint128, uint128, uint128) optional; - // Summarize price oracle as NONDET (it is a view function) + /// PRICE / ORACLE /// function _.price() external => NONDET; - // Summarize internals irrelevant to credit tracking. + /// SAFE TRANSFERS /// + function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; + function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; + + /// MUL/DIV — function summaries that compute the exact value in mathint. + /// This preserves all arithmetic relationships (so updatePositionViewReflectedByIndex + /// still works) while removing the toUint128/cast overhead inlined around each call. + function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d); + function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivUp(x, y, d); + + /// MISC INTERNALS irrelevant to credit / loss-index tracking /// function toId(Midnight.Obligation) external returns (bytes32) => NONDET; function IdLib.storeInCode(Midnight.Obligation memory) internal returns (address) => NONDET; function UtilsLib.hashOffer(Midnight.Offer memory) internal returns (bytes32) => NONDET; @@ -29,22 +39,26 @@ methods { function isHealthy(Midnight.Obligation memory, bytes32, address) internal returns (bool) => NONDET; function tradingFee(bytes32, uint256) internal returns (uint256) => NONDET; - // Assume no reentrancy: callbacks, gates, and token transfers do not re-enter Midnight. + /// EXTERNAL CALLBACKS — collapse path explosion for strong invariants. /// function _.onBuy(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET; function _.onSell(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET; - function _.onRatify(Midnight.Offer, bytes32, bytes) external => NONDET; + function _.onRepay(bytes32, Midnight.Obligation, uint256, address, bytes) external => NONDET; function _.onLiquidate(bytes32, Midnight.Obligation, uint256, uint256, uint256, address, bytes) external => NONDET; + function _.onFlashLoan(address, uint256, bytes) external => NONDET; + function _.onRatify(Midnight.Offer, bytes32, bytes) external => NONDET; function _.canIncreaseCredit(address) external => NONDET; function _.canIncreaseDebt(address) external => NONDET; function _.canLiquidate(address) external => NONDET; - - // Summarize safeTransfer as NONDET for now (TODO: we could also model them as external) - function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; - function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; } -definition PASSIVE_FEE_RECIPIENT() returns address = 0x7e3dce7c19791d65d67ef7ce3c42d2b7fe6fecb1; //currentContract.getPassiveFeeRecipient(); +definition PASSIVE_FEE_RECIPIENT() returns address = 0x7e3dce7c19791d65d67ef7ce3c42d2b7fe6fecb1; +/// MULDIV FUNCTION SUMMARIES /// +// Compute the exact value in mathint and reject division-by-zero / overflow paths. +// The non-deterministic `overflow` flag is sound: when picked true the call reverts +// and the rule's assertion is not checked on that branch (mirroring real Solidity +// uint256 multiplication overflow). Mirrors the helper already in this spec file +// historically and matches the pattern used in Healthiness.spec. function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { bool overflow; if (overflow || d == 0) { @@ -53,17 +67,24 @@ function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { return require_uint256(a * b / d); } +function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + return require_uint256((a * b + (d - 1)) / d); +} + /// GHOST creditAfterSlashingWithPrecision /// -// precision is an integer that is so large that no rounding error will ever occur. -// A possible value would be 2^128! (factorial). -// We do not restrict the value but only axiomatically say that it's greater 0 and a multiple of each ownerLossIndex. +// PRECISION is a (large, abstract) integer that absorbs all rounding error. +// We do not pin its value, only that it's positive and that PRECISION * credit +// is an exact multiple of every userLossIndex we may write. persistent ghost mathint PRECISION { axiom PRECISION > 0; } -// ghost mapping for PRECISION * creditOf(id,user) / userLossIndex(id,user) -// PRECISION ensures that the division will be without rounding errors. +// Ghost mirror of PRECISION * creditOf(id,user) / userLossIndex(id,user), kept exact by the hooks. ghost mapping(bytes32 => mapping(address => mathint)) preciseCreditDivIndex { init_state axiom forall bytes32 id. forall address user. preciseCreditDivIndex[id][user] == 0; @@ -133,38 +154,58 @@ strong invariant preciseCreditCorrect(bytes32 id, address owner) strong invariant sumOfCreditsLeTotalUnits(bytes32 id) (usum address owner. preciseCreditDivIndex[id][owner]) * mapIndex(obligationLossIndex(id)) + PRECISION * continuousFeeCredit(id) <= PRECISION * totalUnits(id) - { - preserved updatePosition(Midnight.Obligation obligation, address user) with (env e) { - requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); - requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); - requireInvariant preciseCreditCorrect(id, user); - requireInvariant obligationLossIndexLeqUserLossIndex(id, user); - } - - preserved withdraw(Midnight.Obligation obligation, uint256 obligationUnits, address onBehalf, address receiver) with (env e) { - requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); - requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); - requireInvariant preciseCreditCorrect(id, onBehalf); - requireInvariant obligationLossIndexLeqUserLossIndex(id, onBehalf); - } - - preserved liquidate(Midnight.Obligation obligation, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) with (env e) { - requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); - requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); - requireInvariant preciseCreditCorrect(id, borrower); - requireInvariant obligationLossIndexLeqUserLossIndex(id, borrower); - } - - preserved take(uint256 obligationUnits, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) with (env e) { - //requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); - requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); - requireInvariant preciseCreditCorrect(id, taker); - requireInvariant obligationLossIndexLeqUserLossIndex(id, taker); - requireInvariant preciseCreditCorrect(id, offer.maker); - requireInvariant obligationLossIndexLeqUserLossIndex(id, offer.maker); - } +{ + preserved updatePosition(Midnight.Obligation obligation, address user) with (env e) { + requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant preciseCreditCorrect(id, user); + requireInvariant obligationLossIndexLeqUserLossIndex(id, user); + } + + preserved withdraw(Midnight.Obligation obligation, uint256 obligationUnits, address onBehalf, address receiver) with (env e) { + requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant preciseCreditCorrect(id, onBehalf); + requireInvariant obligationLossIndexLeqUserLossIndex(id, onBehalf); } + preserved liquidate( + Midnight.Obligation obligation, + uint256 collateralIndex, + uint256 seizedAssets, + uint256 repaidUnits, + address borrower, + address receiver, + address callback, + bytes data + ) with (env e) { + requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant preciseCreditCorrect(id, borrower); + requireInvariant obligationLossIndexLeqUserLossIndex(id, borrower); + } + + // NOTE: this preserved block was previously stale (used Midnight.Signature) and never + // matched, so requireInvariant hints were silently dropped on take(). Fixed signature. + preserved take( + uint256 obligationUnits, + address taker, + address takerCallback, + bytes takerCallbackData, + address receiverIfTakerIsSeller, + Midnight.Offer offer, + bytes ratifierData, + bytes32 root, + bytes32[] proof) with (env e) { + requireInvariant preciseCreditCorrect(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant obligationLossIndexLeqUserLossIndex(id, PASSIVE_FEE_RECIPIENT()); + requireInvariant preciseCreditCorrect(id, taker); + requireInvariant obligationLossIndexLeqUserLossIndex(id, taker); + requireInvariant preciseCreditCorrect(id, offer.maker); + requireInvariant obligationLossIndexLeqUserLossIndex(id, offer.maker); + } +} + // The obligation loss index cannot be larger than the user loss index. strong invariant obligationLossIndexLeqUserLossIndex(bytes32 id, address owner) mapIndex(obligationLossIndex(id)) <= mapIndex(cvlUserLossIndex(id, owner));