getters return structs instead of tuples

certora/confs/BundlerRepayInvertibility.conf

@@ -15,10 +15,10 @@
   "solc_via_ir": true,
   "optimistic_loop": true,
   "loop_iter": 2,
+  "smt_timeout": 7200,
   "prover_args": [
-    "-depth 5",
-    "-mediumTimeout 60",
-    "-timeout 3600"
+    "-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}]"
   ],
   "msg": "Midnight Bundler Repay Invertibility"
 }

certora/helpers/MidnightWrapper.sol

@@ -15,16 +15,16 @@ contract MidnightWrapper is Midnight {
     /* This isHealthy function iterates over all collateralParams, it doesn't use the collateral bitmap. */
 
     function isHealthyNoBitmap(Market memory market, bytes32 id, address borrower) public view returns (bool) {
-        Position storage _position = position[id][borrower];
-        uint256 debt = _position.debt;
+        Position storage userPosition = _position[id][borrower];
+        uint256 debt = userPosition.debt;
         uint256 maxDebt;
         if (debt > 0) {
             uint256 len = market.collateralParams.length;
             for (uint256 i = len; i > 0;) {
                 i--;
                 CollateralParams memory collateralParam = market.collateralParams[i];
                 uint256 price = IOracle(collateralParam.oracle).price();
-                maxDebt += _position.collateral[i].mulDivDown(price, ORACLE_PRICE_SCALE)
+                maxDebt += userPosition.collateral[i].mulDivDown(price, ORACLE_PRICE_SCALE)
                     .mulDivDown(collateralParam.lltv, WAD);
             }
         }

certora/specs/BalanceEffects.spec

@@ -150,7 +150,7 @@ rule takeSellerEffects(env e, Midnight.Offer offer, bytes ratifierData, uint256
 
 /// REPAY ///
 
-/// Repay decreases onBehalf's debt by exactly units and only changes position[id][onBehalf].debt
+/// Repay decreases onBehalf's debt by exactly units and only changes _position[id][onBehalf].debt
 rule repayEffects(env e, Midnight.Market market, uint256 units, address onBehalf, address callback, bytes data, bytes32 anyId, address anyUser) {
     bytes32 id = toId(e, market);
 
@@ -168,7 +168,7 @@ rule repayEffects(env e, Midnight.Market market, uint256 units, address onBehalf
 /// LIQUIDATE ///
 
 /// Liquidate decreases the borrower's debt by at least repaidUnits,
-/// and only changes position[id][borrower].debt.
+/// and only changes _position[id][borrower].debt.
 rule liquidateEffects(env e, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data, bytes32 anyId, address anyUser, bool postMaturityMode) {
     bytes32 id = toId(e, market);
 
@@ -207,7 +207,7 @@ filtered {
 /// SUPPLY COLLATERAL ///
 
 /// supplyCollateral increases onBehalf's collateral by exactly assets,
-/// and only changes position[id][onBehalf].collateral[collateralIndex].
+/// and only changes _position[id][onBehalf].collateral[collateralIndex].
 rule supplyCollateralEffects(env e, Midnight.Market market, uint256 collateralIndex, uint256 assets, address onBehalf, bytes32 anyId, address anyUser, uint256 anyIndex) {
     bytes32 id = toId(e, market);
 
@@ -223,7 +223,7 @@ rule supplyCollateralEffects(env e, Midnight.Market market, uint256 collateralIn
 /// WITHDRAW COLLATERAL ///
 
 /// withdrawCollateral decreases onBehalf's collateral by exactly assets,
-/// and only changes position[id][onBehalf].collateral[collateralIndex].
+/// and only changes _position[id][onBehalf].collateral[collateralIndex].
 rule withdrawCollateralCollateralEffects(env e, Midnight.Market market, uint256 collateralIndex, uint256 assets, address onBehalf, address receiver, bytes32 anyId, address anyUser, uint256 anyIndex) {
     bytes32 id = toId(e, market);
 
@@ -239,7 +239,7 @@ rule withdrawCollateralCollateralEffects(env e, Midnight.Market market, uint256
 /// LIQUIDATE (COLLATERAL) ///
 
 /// liquidate decreases the borrower's collateral at collateralIndex by exactly seizedResult,
-/// and only changes position[id][borrower].collateral[collateralIndex].
+/// and only changes _position[id][borrower].collateral[collateralIndex].
 rule liquidateCollateralEffects(env e, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data, bytes32 anyId, address anyUser, uint256 anyIndex, bool postMaturityMode) {
     bytes32 id = toId(e, market);
 

certora/specs/CollateralBitmap.spec

@@ -38,12 +38,12 @@ persistent ghost summaryMulDivUp(uint256, uint256, uint256) returns uint256;
 
 // Check that a collateral bit is set exactly when there is collateral for that index.
 strong invariant nonZeroCollateralsAreActivated(bytes32 id, address user, uint256 collateralIndex)
-    collateralIndex < 128 => (collateral(id, user, collateralIndex) != 0 <=> summaryGetBit(currentContract.position[id][user].collateralBitmap, collateralIndex));
+    collateralIndex < 128 => (collateral(id, user, collateralIndex) != 0 <=> summaryGetBit(currentContract._position[id][user].collateralBitmap, collateralIndex));
 
 // Check that the number of activated collaterals never exceeds MAX_COLLATERALS_PER_BORROWER.
 // This bounds the while-loop iterations in isHealthy() and liquidate().
 strong invariant atMostMaxCollateralsBitsSet(bytes32 id, address user)
-    summaryCountBits(currentContract.position[id][user].collateralBitmap) <= Utils.maxCollateralsPerBorrower();
+    summaryCountBits(currentContract._position[id][user].collateralBitmap) <= Utils.maxCollateralsPerBorrower();
 
 // This shows that the real isHealthy returns true if and only if the isHealthy function
 // that does not use collateral bitmap returns true.  We also check that the latter function

certora/specs/LiquidationBoundedByLIF.spec

@@ -69,7 +69,7 @@ function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 {
 
 /// Proven in CollateralBitmap.spec; assumed here via requireInvariant (not re-proven in this spec).
 strong invariant nonZeroCollateralsAreActivated(bytes32 id, address user, uint256 collateralIndex)
-    collateralIndex < 128 => (collateral(id, user, collateralIndex) != 0 <=> summaryGetBit(currentContract.position[id][user].collateralBitmap, collateralIndex));
+    collateralIndex < 128 => (collateral(id, user, collateralIndex) != 0 <=> summaryGetBit(currentContract._position[id][user].collateralBitmap, collateralIndex));
 
 /// LIF BOUNDARIES ///
 

certora/specs/LossFactor.spec

@@ -37,24 +37,24 @@ function marketIsCreated(Midnight.Market market) returns (bool) {
 
 /// The market's lossFactor is only modified by liquidate.
 rule onlyLiquidateChangesMarketLossFactor(bytes32 id, method f, env e, calldataarg args) filtered { f -> !f.isView && f.selector != sig:liquidate(Midnight.Market, uint256, uint256, uint256, address, bool, address, address, bytes).selector } {
-    uint128 lossFactorBefore = currentContract.marketState[id].lossFactor;
+    uint128 lossFactorBefore = currentContract._marketState[id].lossFactor;
 
     f(e, args);
 
-    assert currentContract.marketState[id].lossFactor == lossFactorBefore;
+    assert currentContract._marketState[id].lossFactor == lossFactorBefore;
 }
 
 /// In liquidate, the market's lossFactor changes if and only if bad debt is realized (totalUnits decreases).
 rule lossFactorChangesIffBadDebt(env e, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data, bool postMaturityMode) {
     bytes32 id = summaryToId(market);
-    uint128 lossFactorBefore = currentContract.marketState[id].lossFactor;
+    uint128 lossFactorBefore = currentContract._marketState[id].lossFactor;
     uint256 totalUnitsBefore = totalUnits(id);
 
     require lossFactorBefore < max_uint128, "market lossFactor must not be saturated";
 
     liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data);
 
-    bool lossFactorChanged = currentContract.marketState[id].lossFactor != lossFactorBefore;
+    bool lossFactorChanged = currentContract._marketState[id].lossFactor != lossFactorBefore;
     bool badDebtOccurred = totalUnits(id) < totalUnitsBefore;
 
     assert lossFactorChanged <=> badDebtOccurred;
@@ -66,19 +66,19 @@ rule updatePositionSyncsLastLossFactor(env e, Midnight.Market market, address us
 
     updatePosition(e, market, user);
 
-    assert lastLossFactor(id, user) == currentContract.marketState[id].lossFactor;
+    assert lastLossFactor(id, user) == currentContract._marketState[id].lossFactor;
 }
 
 /// Assuming that the market is created, the loss factor computation in updatePosition does not revert.
 rule updatePositionDoesNotRevert(env e, Midnight.Market market, address user) {
     bytes32 id = summaryToId(market);
 
     require marketIsCreated(market), "market must be created";
-    require lastLossFactor(id, user) <= currentContract.marketState[id].lossFactor, "lastLossFactor bounded by market lossFactor, already proved in Midnight.spec";
+    require lastLossFactor(id, user) <= currentContract._marketState[id].lossFactor, "lastLossFactor bounded by market lossFactor, already proved in Midnight.spec";
     require pendingFee(id, user) <= credit(id, user), "pending fee bounded by credit, already proved in Midnight.spec";
-    require currentContract.position[id][user].lastAccrual <= e.block.timestamp, "lastAccrual <= block.timestamp by timestamp monotonicity";
+    require currentContract._position[id][user].lastAccrual <= e.block.timestamp, "lastAccrual <= block.timestamp by timestamp monotonicity";
     require e.block.timestamp < 2 ^ 128, "reasonable timestamp";
-    require currentContract.marketState[id].continuousFeeCredit + pendingFee(id, user) <= max_uint128, "Total credit should be bounded by 2^128 and an increase of continuous fee credit should corresponds to a similar decrease of credit";
+    require currentContract._marketState[id].continuousFeeCredit + pendingFee(id, user) <= max_uint128, "Total credit should be bounded by 2^128 and an increase of continuous fee credit should corresponds to a similar decrease of credit";
 
     require e.msg.value == 0, "Midnight is not payable";
     updatePosition@withrevert(e, market, user);
@@ -90,11 +90,11 @@ rule updatePositionDoesNotRevert(env e, Midnight.Market market, address user) {
 rule updatePositionViewDoesNotRevert(env e, Midnight.Market market, address user) {
     bytes32 id = summaryToId(market);
 
-    require lastLossFactor(id, user) <= currentContract.marketState[id].lossFactor, "lastLossFactor bounded by market lossFactor, already proved in Midnight.spec";
-    require pendingFee(id, user) <= creditOf(id, user), "pending fee bounded by credit, already proved in Midnight.spec";
-    require currentContract.position[id][user].lastAccrual <= e.block.timestamp, "lastAccrual <= block.timestamp by timestamp monotonicity";
+    require lastLossFactor(id, user) <= currentContract._marketState[id].lossFactor, "lastLossFactor bounded by market lossFactor, already proved in Midnight.spec";
+    require pendingFee(id, user) <= credit(id, user), "pending fee bounded by credit, already proved in Midnight.spec";
+    require currentContract._position[id][user].lastAccrual <= e.block.timestamp, "lastAccrual <= block.timestamp by timestamp monotonicity";
     require e.block.timestamp < 2 ^ 128, "reasonable timestamp";
-    require currentContract.marketState[id].continuousFeeCredit + pendingFee(id, user) <= max_uint128, "Total credit should be bounded by 2^128 and an increase of continuous fee credit should corresponds to a similar decrease of credit";
+    require currentContract._marketState[id].continuousFeeCredit + pendingFee(id, user) <= max_uint128, "Total credit should be bounded by 2^128 and an increase of continuous fee credit should corresponds to a similar decrease of credit";
 
     require e.msg.value == 0, "Midnight is not payable";
     updatePositionView@withrevert(e, market, id, user);
@@ -108,15 +108,15 @@ rule updatePositionIsIdempotent(env e, Midnight.Market market, address user) {
 
     require pendingFee(id, user) <= credit(id, user), "see pendingContinuousFeeBoundedByCredit in Midnight.spec";
     require e.block.timestamp < 2 ^ 128, "reasonable timestamp";
-    require currentContract.marketState[id].continuousFeeCredit + pendingFee(id, user) <= max_uint128, "see updatePositionDoesNotRevert";
+    require currentContract._marketState[id].continuousFeeCredit + pendingFee(id, user) <= max_uint128, "see updatePositionDoesNotRevert";
 
     // Snapshot the relevant position state after a first updatePosition.
     updatePosition(e, market, user);
     mathint creditAfterFirst = credit(id, user);
     mathint pendingFeeAfterFirst = pendingFee(id, user);
     uint128 lastLossFactorAfterFirst = lastLossFactor(id, user);
-    uint128 lastAccrualAfterFirst = currentContract.position[id][user].lastAccrual;
-    uint128 cfcAfterFirst = currentContract.marketState[id].continuousFeeCredit;
+    uint128 lastAccrualAfterFirst = currentContract._position[id][user].lastAccrual;
+    uint128 cfcAfterFirst = currentContract._marketState[id].continuousFeeCredit;
 
     uint128 newCredit;
     uint128 newPendingFee;
@@ -132,16 +132,16 @@ rule updatePositionIsIdempotent(env e, Midnight.Market market, address user) {
     assert credit(id, user) == creditAfterFirst;
     assert pendingFee(id, user) == pendingFeeAfterFirst;
     assert lastLossFactor(id, user) == lastLossFactorAfterFirst;
-    assert currentContract.position[id][user].lastAccrual == lastAccrualAfterFirst;
-    assert currentContract.marketState[id].continuousFeeCredit == cfcAfterFirst;
+    assert currentContract._position[id][user].lastAccrual == lastAccrualAfterFirst;
+    assert currentContract._marketState[id].continuousFeeCredit == cfcAfterFirst;
 }
 
 /// When the user's lastLossFactor is in sync with the market's lossFactor (and not saturated),
 /// updatePosition does not slash: credit and pendingFee only decrease by the accrued fee.
 rule updatePositionPreservesCreditWhenLossIndexCurrent(env e, Midnight.Market market, address user) {
     bytes32 id = summaryToId(market);
 
-    require lastLossFactor(id, user) == currentContract.marketState[id].lossFactor, "lastLossFactor synced with market";
+    require lastLossFactor(id, user) == currentContract._marketState[id].lossFactor, "lastLossFactor synced with market";
     require lastLossFactor(id, user) < max_uint128, "lossFactor not saturated";
     require pendingFee(id, user) <= credit(id, user), "see pendingContinuousFeeBoundedByCredit in Midnight.spec";
     require e.block.timestamp < 2 ^ 128, "reasonable timestamp";
@@ -166,11 +166,11 @@ rule updatePositionPreservesContinuousFeeCreditWhenLastAccrualIsUpToDate(env e,
     bytes32 id = summaryToId(market);
 
     require e.block.timestamp < 2 ^ 128, "reasonable timestamp";
-    require currentContract.position[id][user].lastAccrual == e.block.timestamp, "lastAccrual is up to date";
+    require currentContract._position[id][user].lastAccrual == e.block.timestamp, "lastAccrual is up to date";
 
-    uint128 continuousFeeCreditBefore = currentContract.marketState[id].continuousFeeCredit;
+    uint128 continuousFeeCreditBefore = currentContract._marketState[id].continuousFeeCredit;
     updatePosition(e, market, user);
-    uint128 continuousFeeCreditAfter = currentContract.marketState[id].continuousFeeCredit;
+    uint128 continuousFeeCreditAfter = currentContract._marketState[id].continuousFeeCredit;
 
     assert continuousFeeCreditAfter == continuousFeeCreditBefore;
 }
@@ -184,9 +184,9 @@ rule liquidateLossFactorDoesNotRevert(env e, Midnight.Market market, address bor
     require market.liquidatorGate == 0, "Assumption:no liquidator gate";
     require market.collateralParams.length > 0, "market has at least one collateral (enforced by touchMarket)";
     require !liquidationLocked(id, borrower), "liquidation not locked (transient storage is zero at transaction start)";
-    require currentContract.position[id][borrower].collateralBitmap == 0, "Assumption: no active collaterals: skip loop and maximize badDebt";
-    require currentContract.position[id][borrower].debt > 0, "borrower must have debt to enter badDebt > 0 block";
-    require currentContract.position[id][borrower].debt <= currentContract.marketState[id].totalUnits, "position debt bounded by totalUnits (see totalUnitsEqualsSumNegativeDebtPlusWithdrawable)";
+    require currentContract._position[id][borrower].collateralBitmap == 0, "Assumption: no active collaterals: skip loop and maximize badDebt";
+    require currentContract._position[id][borrower].debt > 0, "borrower must have debt to enter badDebt > 0 block";
+    require currentContract._position[id][borrower].debt <= currentContract._marketState[id].totalUnits, "position debt bounded by totalUnits (see totalUnitsEqualsSumNegativeDebtPlusWithdrawable)";
     require e.msg.value == 0, "Midnight is not payable";
 
     address zero = 0;

certora/specs/Midnight.spec

@@ -48,7 +48,7 @@ persistent ghost mapping(bytes32 => mathint) sumDebt {
     init_state axiom (forall bytes32 id. sumDebt[id] == 0);
 }
 
-hook Sstore position[KEY bytes32 id][KEY address owner].debt uint128 newDebt (uint128 oldDebt) {
+hook Sstore _position[KEY bytes32 id][KEY address owner].debt uint128 newDebt (uint128 oldDebt) {
     sumDebt[id] = sumDebt[id] - to_mathint(oldDebt) + to_mathint(newDebt);
 }
 
@@ -93,9 +93,9 @@ rule liquidateInputOutputConsistency(env e, Midnight.Market market, uint256 coll
 }
 
 rule marketLossFactorMonotonicallyIncreases(bytes32 id, method f, env e, calldataarg args) {
-    uint128 lossFactorBefore = currentContract.marketState[id].lossFactor;
+    uint128 lossFactorBefore = currentContract._marketState[id].lossFactor;
     f(e, args);
-    uint128 lossFactorAfter = currentContract.marketState[id].lossFactor;
+    uint128 lossFactorAfter = currentContract._marketState[id].lossFactor;
     assert lossFactorAfter >= lossFactorBefore;
 }
 
@@ -108,7 +108,7 @@ rule lastLossFactorMonotonicallyIncreases(bytes32 id, address user, method f, en
 }
 
 rule creditAndDebtCannotIncreaseWhenLossFactorIsMaxed(bytes32 id, address user, method f, env e, calldataarg args) {
-    require currentContract.marketState[id].lossFactor == max_uint128, "assume loss factor is maxed out";
+    require currentContract._marketState[id].lossFactor == max_uint128, "assume loss factor is maxed out";
     uint256 creditBefore = credit(id, user);
     uint256 debtBefore = debt(id, user);
 
@@ -127,7 +127,7 @@ strong invariant defaultContinuousFeeBoundedAll()
     forall address token. currentContract.defaultContinuousFee[token] <= MAX_CONTINUOUS_FEE();
 
 strong invariant continuousFeeBounded(bytes32 id)
-    currentContract.marketState[id].continuousFee <= MAX_CONTINUOUS_FEE()
+    currentContract._marketState[id].continuousFee <= MAX_CONTINUOUS_FEE()
     {
         preserved with (env e) {
             requireInvariant defaultContinuousFeeBoundedAll();
@@ -154,7 +154,7 @@ rule noRemainingContinuousFeeWithoutCredit(bytes32 id, address user) {
 }
 
 strong invariant lastLossFactorLeqMarketLossFactor(bytes32 id, address user)
-    lastLossFactor(id, user) <= currentContract.marketState[id].lossFactor;
+    lastLossFactor(id, user) <= currentContract._marketState[id].lossFactor;
 
 /// A user cannot have both credit and debt.
 strong invariant noCreditAndDebt(bytes32 id, address user)