diff --git a/certora/confs/SumOfCreditsAxiomatic.conf b/certora/confs/SumOfCreditsAxiomatic.conf new file mode 100644 index 000000000..89ccb797e --- /dev/null +++ b/certora/confs/SumOfCreditsAxiomatic.conf @@ -0,0 +1,23 @@ +{ + "files": [ + "src/Midnight.sol" + ], + "parametric_contracts": [ + "Midnight" + ], + "verify": "Midnight:certora/specs/SumOfCreditsAxiomatic.spec", + "solc": "solc-0.8.34", + "solc_via_ir": true, + "solc_evm_version": "osaka", + "optimistic_loop": true, + "loop_iter": 2, + "optimistic_hashing": true, + "hashing_length_bound": 1024, + "build_cache": true, + "prover_args": [ + "-destructiveOptimizations twostage -depth 2" + ], + "rule_sanity": "basic", + "smt_timeout": 7200, + "msg": "SumOfCredits" +} diff --git a/certora/confs/UpdatePositionView.conf b/certora/confs/UpdatePositionView.conf new file mode 100644 index 000000000..38dcc3f2c --- /dev/null +++ b/certora/confs/UpdatePositionView.conf @@ -0,0 +1,29 @@ +{ + "files": [ + "src/Midnight.sol" + ], + "verify": "Midnight:certora/specs/UpdatePositionView.spec", + "parametric_contracts": [ + "Midnight" + ], + "solc": "solc-0.8.34", + "solc_via_ir": true, + "solc_evm_version": "osaka", + "optimistic_loop": true, + "loop_iter": 2, + "optimistic_hashing": true, + "hashing_length_bound": 1024, + "multi_assert_check": true, + "build_cache": true, + "smt_timeout": 600, + "prover_args": [ + "-destructiveOptimizations twostage", + "-backendStrategy singleRace", + "-smt_useLIA false", + "-smt_useNIA true", + "-depth 0", + "-smt_skipDelayedSolvers false", + "-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}]" + ], + "msg": "Update Position View" +} diff --git a/certora/specs/SumOfCreditsAxiomatic.spec b/certora/specs/SumOfCreditsAxiomatic.spec new file mode 100644 index 000000000..6263a84a8 --- /dev/null +++ b/certora/specs/SumOfCreditsAxiomatic.spec @@ -0,0 +1,340 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +// + +import "MulDivAxioms.spec"; + +methods { + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function totalUnits(bytes32 id) external returns (uint128) envfree; + function continuousFeeCredit(bytes32 id) external returns (uint128) envfree; + function lossFactor(bytes32) external returns (uint128) envfree; + function lastLossFactor(bytes32 id, address user) external returns (uint128) envfree; + + /// SUMMARY OF updatePositionView -- see file header for soundness argument. /// + function Midnight.updatePositionView(Midnight.Market memory obligation, bytes32 id, address user) internal returns (uint128, uint128, uint128) with(env e) => summaryUpdatePositionView(e, id, user); + + /// PRICE / ORACLE /// + function _.price() external => NONDET; + + /// MUL/DIV — exact mathint summaries (still needed for the parts of + /// withdraw / take outside `updatePositionView`, e.g. the proportional + /// pendingFee adjustment and the take buyer-fee accrual). + 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 IdLib.toId(Midnight.Market memory) internal returns (bytes32) => NONDET; + function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET; + function touchMarket(Midnight.Market) external returns (bytes32) => NONDET; + function Midnight.touchMarket(Midnight.Market memory) internal returns (bytes32) => NONDET; + function UtilsLib.msb(uint128) internal returns (uint256) => NONDET; + function UtilsLib.countBits(uint128) internal returns (uint256) => NONDET; + function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; + function TickLib.wExp(int256) internal returns (uint256) => NONDET; + function UtilsLib.tGet(uint256, bytes32, address) internal returns (bool) => NONDET; + function UtilsLib.tExchange(uint256, bytes32, address, bool) internal returns (bool) => NONDET; + function isHealthy(Midnight.Market memory, bytes32, address) internal returns (bool) => NONDET; + function settlementFee(bytes32, uint256) internal returns (uint256) => NONDET; + + /// SAFE TRANSFERS /// + function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; + function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; + + /// EXTERNAL CALLBACKS — prevent havoc of ghosts and variables in callbacks. + function _.onBuy(bytes32, Midnight.Market, uint256, uint256, uint256, address, bytes) external => NONDET; + function _.onSell(bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes) external => NONDET; + function _.onLiquidate(address, bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes, uint256) external => NONDET; + function _.onFlashLoan(address, address[], uint256[], bytes) external => NONDET; + function _.onRepay(bytes32, Midnight.Market, uint256, address, bytes) external => NONDET; +} + +/// GHOSTS /// + +persistent ghost mathint PRECISION { + axiom PRECISION > 0; +} + +ghost mapping(bytes32 => mathint) sumPreciseCreditDivIndex { + init_state axiom forall bytes32 id. sumPreciseCreditDivIndex[id] == 0; + axiom forall bytes32 id. sumPreciseCreditDivIndex[id] >= 0; +} + +ghost mapping(bytes32 => mapping(address => mathint)) preciseCreditDivIndex { + init_state axiom forall bytes32 id. forall address user. preciseCreditDivIndex[id][user] == 0; + axiom forall bytes32 id. forall address user. preciseCreditDivIndex[id][user] >= 0; +} + +// Instead of using the builtin `*`, which requires unstable non-linear arithemetic, we +// use the uninterpreted function `multiply` and only instantiate those axioms we need for proving. +// `multiply(a, b)` IS the product `a * b` declared as an uninterpreted function. +persistent ghost multiply(mathint, mathint) returns mathint { + axiom forall mathint a. forall mathint b. (a > 0 && b > 0) => multiply(a, b) > 0; + axiom forall mathint a. multiply(a, 0) == 0; + axiom forall mathint b. multiply(0, b) == 0; +} + +// Distributivity axiom. +definition axiomDistributivity(mathint a, mathint b, mathint c) returns bool = multiply(a + b, c) == multiply(a, c) + multiply(b, c); + +// Symmetry axiom over associativity. +definition axiomAssocComm(mathint a, mathint b, mathint c) returns bool = multiply(multiply(a, b), c) == multiply(multiply(a, c), b); + +// Linear order axiom for multiplication with positive constants. +definition axiomLeMulPos(mathint a, mathint b, mathint c) returns bool = c > 0 => ((a <= b) <=> (multiply(a, c) <= multiply(b, c))); + +// The following is RoundsDown axiom stated using the `multiply` function. +definition axiomMathMulDivDownRoundsDownMultiply(mathint a, mathint b, mathint d) returns bool = a >= 0 && b >= 0 => multiply(mathMulDivDown(a, b, d), d) <= multiply(a, b); + +definition axiomMathMulDivDownRoundsDownMultiplySymm(mathint a, mathint b, mathint d) returns bool = a >= 0 && b >= 0 => multiply(d, mathMulDivDown(a, b, d)) <= multiply(b, a); + +function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { + if (d == 0 || a * b >= 2 ^ 256) { + revert(); + } + require axiomMathMulDivDownZeroA(b, d), "axiom"; + require axiomMathMulDivDownZeroB(a, d), "axiom"; + require axiomMathMulDivDownRoundsDownMultiply(a, b, d), "axiom"; + require axiomMathMulDivDownRoundsDownMultiplySymm(a, b, d), "axiom"; + return require_uint256(ghostMulDivDown(a, b, d)); +} + +function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (d == 0 || a * b + d - 1 >= 2 ^ 256) { + revert(); + } + return require_uint256(ghostMulDivUp(a, b, d)); +} + +/// HELPER DEFINITIONS /// + +definition mapFactor(mathint index) returns mathint = 2 ^ 128 - 1 - index; + +definition cvlCredit(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].credit; + +definition cvlLastLossFactor(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].lastLossFactor; + +definition cvlPendingFee(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].pendingFee; + +definition cvlLastAccrual(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].lastAccrual; + +// Body of the strong invariant. The aggregate product is routed through the +// uninterpreted `multiply` (== sumPreciseCreditDivIndex[id] * mapFactor(...)). +definition sumOfCreditsBody(bytes32 id) returns bool = multiply(sumPreciseCreditDivIndex[id], mapFactor(lossFactor(id))) <= multiply(totalUnits(id), PRECISION) - multiply(continuousFeeCredit(id), PRECISION); + +/// HOOKS /// + +function updateCreditDivIndex(bytes32 id, address owner, uint128 newCredit, uint128 newIndex) { + mathint ownerLossIndex = mapFactor(newIndex); + mathint oldCDI = preciseCreditDivIndex[id][owner]; + mathint value; + + // We require there is a value such that + // value * ownerLossIndex == newCredit * PRECISION. + // This is sound because we can assume PRECISION to be large enough to + // be divisible by ownerLossIndex. + require ownerLossIndex > 0 => multiply(value, ownerLossIndex) == multiply(newCredit, PRECISION), "PRECISION is divisible by ownerLossIndex"; + + mathint newCDI = (ownerLossIndex == 0 || newCredit == 0) ? 0 : value; + preciseCreditDivIndex[id][owner] = newCDI; + mathint oldSum = sumPreciseCreditDivIndex[id]; + sumPreciseCreditDivIndex[id] = oldSum + newCDI - oldCDI; + + // require distributivity axioms to help prover + mathint lossIndex = mapFactor(lossFactor(id)); + require axiomDistributivity(oldSum, newCDI, lossIndex), "axiom"; + require axiomDistributivity(oldSum + newCDI - oldCDI, oldCDI, lossIndex), "axiom"; +} + +function checkCreditDivInvariant(bytes32 id, address owner) returns bool { + uint128 credit = cvlCredit(id, owner); + uint128 userIndex = cvlLastLossFactor(id, owner); + mathint mappedIndex = mapFactor(userIndex); + + // Per-user invariant stays in REAL-product form: it is per-user (cheap) and + // the hook's division-exactness genuinely needs real arithmetic. Abstracting + // it to multiply weakened this ASSUMED invariant enough to make a + // fully-slashed store (mapFactor==0, credit!=0) reachable, breaking the hook + // assert. Only the AGGREGATE (sumOfCreditsBody) is abstracted. + return mappedIndex == 0 || credit == 0 ? preciseCreditDivIndex[id][owner] == 0 : multiply(preciseCreditDivIndex[id][owner], mappedIndex) == multiply(credit, PRECISION); +} + +hook Sstore position[KEY bytes32 id][KEY address owner].credit uint128 newCredit (uint128 oldCredit) { + updateCreditDivIndex(id, owner, newCredit, cvlLastLossFactor(id, owner)); + if (newCredit > oldCredit) { + require axiomDistributivity(oldCredit, newCredit - oldCredit, PRECISION), "axiom"; + } else { + require axiomDistributivity(newCredit, oldCredit - newCredit, PRECISION), "axiom"; + } +} + +hook Sstore position[KEY bytes32 id][KEY address owner].lastLossFactor uint128 newIndex (uint128 oldIndex) { + updateCreditDivIndex(id, owner, cvlCredit(id, owner), newIndex); +} + +hook Sstore marketState[KEY bytes32 id].totalUnits uint128 newTotal (uint128 oldTotal) { + if (newTotal > oldTotal) { + require axiomDistributivity(oldTotal, newTotal - oldTotal, PRECISION), "axiom"; + } else { + require axiomDistributivity(newTotal, oldTotal - newTotal, PRECISION), "axiom"; + } +} + +/// SUMMARY OF updatePositionView /// +// +// Returns nondet (newCredit, newPendingFee, fee) constrained by the inequalities +// proved by rule updatePositionViewReflectedByFactor in UpdatePositionView.spec +function summaryUpdatePositionView(env e, bytes32 id, address user) returns (uint128, uint128, uint128) { + uint128 oldCredit = cvlCredit(id, user); + uint128 oldPendingFee = cvlPendingFee(id, user); + uint128 oldLastAccrual = cvlLastAccrual(id, user); + + require to_mathint(e.block.timestamp) >= to_mathint(oldLastAccrual), "time is non-decreasing"; + + uint128 newCredit; + uint128 newPendingFee; + uint128 fee; + mathint preciseCreditBefore = multiply(preciseCreditDivIndex[id][user], mapFactor(lossFactor(id))); + + require newCredit <= oldCredit, "proved in UpdatePositionView"; + require newPendingFee <= oldPendingFee, "proved in UpdatePositionView"; + require fee <= oldPendingFee, "proved in UpdatePositionView"; + require multiply(newCredit + fee, PRECISION) <= preciseCreditBefore, "proved in UpdatePositionView"; + + require axiomDistributivity(newCredit, fee, PRECISION), "axiom"; + require mapFactor(lossFactor(id)) == 0 => (newCredit == 0 && fee == 0), "proved in UpdatePositionView"; + + // help solver to reason about fee and distributivity. + require axiomDistributivity(fee, continuousFeeCredit(id), PRECISION), "axiom"; + + return (newCredit, newPendingFee, fee); +} + +/// INVARIANTS /// + +strong invariant preciseCreditCorrect(bytes32 id, address owner) + checkCreditDivInvariant(id, owner); + +// Parametric coverage of the sum invariant for all methods EXCEPT withdraw and +// take, which are handled by their dedicated rules (sumOfCreditsLeTotalUnits_withdraw +// here, and the SumOfCreditsSummaryTake.spec split for take). +strong invariant sumOfCreditsLeTotalUnits(bytes32 id) + sumOfCreditsBody(id) + filtered { f -> f.selector != sig:take(Midnight.Offer, bytes, uint256, address, address, address, bytes).selector && f.selector != sig:liquidate(Midnight.Market, uint256, uint256, uint256, address, bool, address, address, bytes).selector } { + preserved claimContinuousFee(Midnight.Market market, uint256 amount, address receiver) with (env e) { + require axiomDistributivity(continuousFeeCredit(id) - amount, amount, PRECISION), "axiom"; + require axiomDistributivity(totalUnits(id) - amount, amount, PRECISION), "axiom"; + } + + preserved updatePosition(Midnight.Market market, address user) with (env e) { + requireInvariant preciseCreditCorrect(id, user); + require lastLossFactor(id, user) <= currentContract.marketState[id].lossFactor, "lastLossFactorLeqMarketLossFactor in Midnight"; + } + + preserved withdraw(Midnight.Market market, uint256 units, address onBehalf, address receiver) with (env e) { + requireInvariant preciseCreditCorrect(id, onBehalf); + require lastLossFactor(id, onBehalf) <= currentContract.marketState[id].lossFactor, "lastLossFactorLeqMarketLossFactor in Midnight"; + } + } + +rule sumOfCreditsLeTotalUnitsPreservedByLiquidate(bytes32 id, env e, Midnight.Market obligation, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data) { + require sumOfCreditsBody(id); + requireInvariant preciseCreditCorrect(id, borrower); + require lastLossFactor(id, borrower) <= currentContract.marketState[id].lossFactor, "lastLossFactorLeqMarketLossFactor in Midnight"; + + mathint sumPre = sumPreciseCreditDivIndex[id]; + mathint indexPre = mapFactor(lossFactor(id)); + mathint tuPre = totalUnits(id); + mathint cfPre = continuousFeeCredit(id); + + liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); + + // Liquidate never calls _updatePosition or touches any user's credit; `sum` is unchanged. + // Instead the lossFactor rescales: + // lossFactor = mapLossFactor(mulDivDown(mapFactor(lossFactor), totalUnits - badDebt, totalUnits)) + // continuousFeeCredit = mulDivDown(contnuousFeeCredit, mapFactor(new), mapFactor(old)) + // totalUnits = totalUnits - badDebt + + mathint indexPost = mapFactor(lossFactor(id)); + mathint tuPost = totalUnits(id); + mathint cfPost = continuousFeeCredit(id); + + // bad debt can be computed from the change of totalUnits. + mathint badDebt = tuPre - tuPost; + + // The proof requires several steps: + + // From mulDivDownRoundsDown for indexPost = indexPre.mulDivDown(tuPost, tuPre): + // tuPre * indexPost <= tuPost * indexPre + // From mulDivDownRoundsDown for cfPost = cfPre.mulDivDown(indexPost, indexPre): + // cfPost * indexPre <= cfPre * indexPost + + // Use the following distributivity rules: + require axiomDistributivity(cfPre, tuPre - cfPre, indexPost), "axiom"; + require axiomDistributivity(cfPost, tuPost - cfPost, indexPre), "axiom"; + require axiomDistributivity(tuPre - cfPre, cfPre, PRECISION), "axiom"; + require axiomDistributivity(tuPost - cfPost, cfPost, PRECISION), "axiom"; + + // this yields + // (tuPre - cfPre) * indexPost <= (tuPost - cfPost) * indexPre (A) + + // Then the main proof is: + // sumPre * indexPre <= (tuPre - cfPre) * PRECISION (sumOfCreditBody Pre) + // <=> { indexPost >= 0} + // sumPre * indexPre * indexPost <= (tuPre - cfPre) * PRECISION * indexPost + // <=> { 2x associative commutative } + // sumPre * indexPost * indexPre <= (tuPre - cfPre) * indexPost * PRECISION + // <=> { (A) multiplied with PRECISION >= 0 } + // sumPre * indexPost * indexPre <= (tuPost - cfPost) * indexPre * PRECISION + // <=> { associative, commutative } + // sumPre * indexPost * indexPre <= (tuPost - cfPost) * PRECISION * indexPre + // <=> { divide by indexPre >= 0} + // sumPre * indexPost <= (tuPost - cfPost) * PRECISION (sumOfCreditBody Post) + + // These are the axioms used in the proof above + require axiomLeMulPos(multiply(sumPre, indexPre), multiply(tuPre - cfPre, PRECISION), indexPost), "axiom"; + require axiomAssocComm(sumPre, indexPre, indexPost), "axiom"; + require axiomAssocComm(tuPre - cfPre, PRECISION, indexPost), "axiom"; + require axiomLeMulPos(multiply(tuPre - cfPre, indexPost), multiply(tuPost - cfPost, indexPre), PRECISION), "axiom"; + require axiomAssocComm(tuPost - cfPost, indexPre, PRECISION), "axiom"; + require axiomLeMulPos(multiply(sumPre, indexPost), multiply(tuPost - cfPost, PRECISION), indexPre), "axiom"; + + assert sumOfCreditsBody(id); +} + +rule sumOfCreditsLeTotalUnitsPreservedByTake(bytes32 id, env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) { + require sumOfCreditsBody(id); + + // Determine buyer and seller + address buyer = offer.buy ? offer.maker : taker; + address seller = offer.buy ? taker : offer.maker; + + requireInvariant preciseCreditCorrect(id, taker); + require lastLossFactor(id, taker) <= currentContract.marketState[id].lossFactor, "lastLossFactorLeqMarketLossFactor in Midnight"; + requireInvariant preciseCreditCorrect(id, offer.maker); + require lastLossFactor(id, offer.maker) <= currentContract.marketState[id].lossFactor, "lastLossFactorLeqMarketLossFactor in Midnight"; + + mathint tuPre = totalUnits(id); + mathint debtPre_b = currentContract.position[id][buyer].debt; + + take(e, offer, ratifierData, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData); + mathint tuPost = totalUnits(id); + + // Compute the buyer credit increase. Note that updatePosition does + // not touch debt, so we can use this formula from Midnight. + mathint buyerCreditIncrease = units > debtPre_b ? units - debtPre_b : 0; + + // We do not have the credit of seller after updatePosition before take, + // but we can compute sellerCreditDecrease from totalUnits change. + mathint sellerCreditDecrease = tuPre + buyerCreditIncrease - tuPost; + + // These distributivity axiom is needed because Midnight adds buyer and + // seller credit at the same time. + if (buyerCreditIncrease > sellerCreditDecrease) { + require axiomDistributivity(buyerCreditIncrease - sellerCreditDecrease, sellerCreditDecrease, PRECISION), "axiom"; + } else { + require axiomDistributivity(sellerCreditDecrease - buyerCreditIncrease, buyerCreditIncrease, PRECISION), "axiom"; + } + assert sumOfCreditsBody(id); +} diff --git a/certora/specs/UpdatePositionView.spec b/certora/specs/UpdatePositionView.spec new file mode 100644 index 000000000..120c69b6d --- /dev/null +++ b/certora/specs/UpdatePositionView.spec @@ -0,0 +1,151 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +methods { + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function lossFactor(bytes32) external returns (uint128) envfree; + function lastLossFactor(bytes32 id, address user) external returns (uint128) envfree; + + /// PRICE / ORACLE /// + function _.price() external => NONDET; + + /// 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. + 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-factor tracking /// + function IdLib.toId(Midnight.Market memory) internal returns (bytes32) => NONDET; + function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => 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.Market memory, bytes32, address) internal returns (bool) => NONDET; + function settlementFee(bytes32, uint256) internal returns (uint256) => NONDET; + + /// EXTERNAL CALLBACKS — collapse path explosion for strong invariants. /// + function _.onBuy(bytes32, Midnight.Market, uint256, uint256, uint256, address, bytes) external => NONDET; + function _.onSell(bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes) external => NONDET; + function _.onLiquidate(address, bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes, uint256) external => NONDET; + function _.onFlashLoan(address, address[], uint256[], bytes) external => NONDET; + function _.onRepay(bytes32, Midnight.Market, uint256, address, bytes) external => NONDET; +} + +/// MULDIV FUNCTION SUMMARIES /// +function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + 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); +} + +/// GHOSTS /// + +persistent ghost mathint PRECISION { + axiom PRECISION > 0; +} + +ghost mapping(bytes32 => mapping(address => mathint)) preciseCreditDivFactor { + init_state axiom forall bytes32 id. forall address user. preciseCreditDivFactor[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 factor to 1 - factor, for easier math. +definition mapFactor(mathint factor) returns mathint = 2 ^ 128 - 1 - factor; + +definition cvlCredit(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].credit; + +definition cvlLastLossFactor(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].lastLossFactor; + +/// HOOKS /// + +function updateCreditDivFactor(bytes32 id, address owner, uint128 newCredit, uint128 newFactor) { + mathint ownerLossFactor = mapFactor(newFactor); + require ownerLossFactor > 0 => PRECISION * newCredit % ownerLossFactor == 0, "PRECISION is 2^128!"; + preciseCreditDivFactor[id][owner] = ownerLossFactor == 0 ? 0 : PRECISION * newCredit / ownerLossFactor; +} + +function checkCreditDivInvariant(bytes32 id, address owner) returns bool { + uint128 credit = cvlCredit(id, owner); + uint128 userFactor = cvlLastLossFactor(id, owner); + mathint mappedFactor = mapFactor(userFactor); + return mappedFactor == 0 ? preciseCreditDivFactor[id][owner] == 0 : preciseCreditDivFactor[id][owner] * mappedFactor == PRECISION * credit; +} + +hook Sstore position[KEY bytes32 id][KEY address owner].credit uint128 newCredit (uint128 oldCredit) { + updateCreditDivFactor(id, owner, newCredit, cvlLastLossFactor(id, owner)); +} + +hook Sstore position[KEY bytes32 id][KEY address owner].lastLossFactor uint128 newFactor (uint128 oldFactor) { + updateCreditDivFactor(id, owner, cvlCredit(id, owner), newFactor); +} + +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 newPendingFee (uint128 oldPendingFee) { + pendingFeeMirror[id][owner] = newPendingFee; +} + +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); + +/// RULES /// + +rule updatePositionViewProperties(env e, Midnight.Market obligation, bytes32 id, address user) { + requireInvariant preciseCreditCorrect(id, user); + require lastLossFactor(id, user) <= currentContract.marketState[id].lossFactor, "lastLossFactorLeqMarketLossFactor in Midnight"; + + uint128 newCredit; + uint128 newPendingFee; + uint128 fee; + + uint128 oldCredit = cvlCredit(id, user); + mathint preciseCreditBefore = preciseCreditDivFactor[id][user] * mapFactor(lossFactor(id)); + mathint oldPendingFee = pendingFeeMirror[id][user]; + mathint oldLastAccrual = lastAccrualMirror[id][user]; + + require e.block.timestamp >= oldLastAccrual, "Time is increasing"; + + newCredit, newPendingFee, fee = updatePositionView(e, obligation, id, user); + + // These are the properties updatePositionView guarantees + + assert fee <= oldPendingFee, "Cannot take more fee than pending"; + assert (newCredit + fee) * PRECISION <= preciseCreditBefore, "newCredit (with fees) is at most precise credit after slashing"; + assert newCredit <= oldCredit, "slashing and fee accrual only decrease credit"; + assert newPendingFee <= oldPendingFee, "fee deduction only decreases pending"; + assert mapFactor(currentContract.marketState[id].lossFactor) == 0 => newCredit == 0 && fee == 0, "no credit/fee on total loss factor"; +}