Updates to the VariableDebtToken spec

specs/VariableDebtToken.spec

@@ -1,15 +1,12 @@
 using LendingPoolHarnessForVariableDebtToken as POOL
-/**
-TotalSupply is the sum of all users’ balances
-	
-totalSupply(t) = Σaddress u. balanceOf(u,t)
 
-Check that each possible opertaion changes the balance of at most one user
+/**
+Checks that each possible opertaion changes the balance of at most one user.
 */
 rule balanceOfChange(address a, address b, method f)
 {
 	env e;
-	require a!=b ;
+	require a != b;
 	uint256 balanceABefore = sinvoke balanceOf(e, a);
 	uint256 balanceBBefore = sinvoke balanceOf(e, b);
 	 
@@ -19,14 +16,14 @@ rule balanceOfChange(address a, address b, method f)
 	uint256 balanceAAfter = sinvoke balanceOf(e, a);
 	uint256 balanceBAfter = sinvoke balanceOf(e, b);
 	
-	assert ( balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter );
+	assert (balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter);
 }
 
-/*
-Check that the changed to total supply is coherent with the changes to balance
+/**
+Checks that the change to total supply is coherent with the change to the balance due to an operation
+(which is neither a burn nor a mint).
 */
-
-rule integirtyBalanceOfTotalSupply(address a, method f )
+rule integirtyBalanceOfTotalSupply(address a, method f)
 {
 	env e;
 	
@@ -36,17 +33,17 @@ rule integirtyBalanceOfTotalSupply(address a, method f )
 	calldataarg arg;
 	sinvoke f(e, arg); 
 	require (f.selector != burn(address, uint256, uint256).selector  &&
-		f.selector != mint(address, uint256, uint256).selector ) ;
+		f.selector != mint(address, address, uint256, uint256).selector);
 	uint256 balanceAAfter = balanceOf(e, a);
 	uint256 totalSupplyAfter = totalSupply(e);
 
 	assert  (balanceAAfter != balanceABefore  => ( balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
 }
 
-/* Burn behaves deferently and due to accumulation errors might hace less total supply then the balance
+/**
+Checks that the change to total supply is coherent with the change to the balance due to a burn operation.
 */
-
-rule integirtyBalanceOfTotalSupplyOnBurn(address a, method f )
+rule integirtyBalanceOfTotalSupplyOnBurn(address a)
 {
 	env e;
 	
@@ -59,67 +56,75 @@ rule integirtyBalanceOfTotalSupplyOnBurn(address a, method f )
 	sinvoke burn(e, a, x, index); 
 	uint256 balanceAAfter = balanceOf(e, a);
 	uint256 totalSupplyAfter = totalSupply(e);
-	assert  (balanceAAfter != balanceABefore  => ( balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+	assert (balanceAAfter != balanceABefore  => (balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
 }
 
-rule integirtyBalanceOfTotalSupplyOnMint(address a, method f )
+/**
+Checks that the change to total supply is coherent with the change to the balance due to a mint operation.
+*/
+rule integirtyBalanceOfTotalSupplyOnMint(address u, address delegatedUser)
 {
 	env e;
 	
-	uint256 balanceABefore = balanceOf(e, a);
+	uint256 balanceUBefore = balanceOf(e, u);
 	uint256 totalSupplyBefore = totalSupply(e);
 	 
 	uint256 x;
 	address asset;
 	uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
-	sinvoke mint(e, a, x, index); 
-	uint256 balanceAAfter = balanceOf(e, a);
+	sinvoke mint(e, delegatedUser, u, x, index); 
+	uint256 balanceUAfter = balanceOf(e, u);
 	uint256 totalSupplyAfter = totalSupply(e);
-	assert  (balanceAAfter != balanceABefore  => ( balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+	assert (balanceUAfter != balanceUBefore  => (balanceUAfter - balanceUBefore  == totalSupplyAfter - totalSupplyBefore));
 }
 
 /**
-Minting an amount of x tokens for user u increases their balance by x, up to rounding errors. 
-{ b= balanceOf(u,t) } 
-mint(u,x,index) 
-{ balanceOf(u,t) = b + x }
+Minting an amount of x tokens for user u increases her balance by x, up to rounding errors. 
+{ b = balanceOf(u,t) } 
+mint(delegatedUser, u, x, index) 
+{ balanceOf(u,t) = b + x }.
 
+Also, if the minting is done by a user delegatedUser different than u, the balance of delegatedUser
+remains unchanged.
 */
-rule integrityMint(address a, uint256 x) {
+rule integrityMint(address u, address delegatedUser, uint256 x) {
 	env e;
 	address asset;
 	uint256 index = POOL.getReserveNormalizedVariableDebt(e,asset);
-	uint256 balancebefore = balanceOf(e, a);
-	sinvoke mint(e, a, x, index);
+	uint256 balanceUBefore = balanceOf(e, u);
+	uint256 balanceDelegatedUBefore = balanceOf(e, delegatedUser);
+	sinvoke mint(e, delegatedUser, u, x, index);
 	
-	uint256 balanceAfter = balanceOf(e, a);
-	assert balanceAfter == balancebefore+x;
+	uint256 balanceUAfter = balanceOf(e, u);
+	uint256 balanceDelegatedUAfter = balanceOf(e, delegatedUser);
+	
+	assert balanceUAfter == balanceUBefore + x && (u != delegatedUser => (balanceDelegatedUAfter == balanceDelegatedUBefore));
 }
 
 /**
-Mint is additive, can performed either all at once or gradually
-mint(u,x); mint(u,y) ~ mint(u,x+y) at the same timestamp
+Mint is additive, namely it can performed either all at once or gradually:
+mint(delegatedUser, u, x, index); mint(delegatedUser, u, y, index) ~ mint(delegatedUser, u, x+y, index) at the same timestamp.
 */
-rule additiveMint(address a, uint256 x, uint256 y) {
+rule additiveMint(address a, address delegatedUser, uint256 x, uint256 y) {
 	env e;
 	address asset;
 	uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
 	storage initialStorage = lastStorage;
-	sinvoke mint(e, a, x, index);
-	sinvoke mint(e, a, y, index);
+	sinvoke mint(e, delegatedUser, a, x, index);
+	sinvoke mint(e, delegatedUser, a, y, index);
 	uint256 balanceScenario1 = balanceOf(e, a);
-	uint t = x + y;
-	sinvoke mint(e, a, t ,index) at initialStorage;
+	uint256 t = x + y;
+	sinvoke mint(e, delegatedUser, a, t ,index) at initialStorage;
 
 	uint256 balanceScenario2 = balanceOf(e, a);
 	assert balanceScenario1 == balanceScenario2, "mint is not additive";
 }
 
 /** 
-Transfer of x amount of tokens from user u  where receiver is user u’
-{bu = balanceOf(u) } 
-	burn(u, u’, x)
-{balanceOf(u) = bu - x } 
+Burning an amount of x tokens for user u decreases her balance by x, up to rounding errors. 
+{ bu = balanceOf(u) } 
+	burn(u, x)
+{ balanceOf(u) = bu - x }.
 */
 rule integrityBurn(address a, uint256 x) {
 	env e;
@@ -132,9 +137,8 @@ rule integrityBurn(address a, uint256 x) {
 	assert balanceAfter == balancebefore - x;
 }
 /**
-Minting is additive, i.e., it can be performed either all at once or in steps.
-
-burn(u, u’, x); burn(u, u’, y) ~ burn(u, u’, x+y) 
+Minting is additive, i.e., it can be performed either all at once or in steps:
+burn(u, x); burn(u, y) ~ burn(u, x+y) at the same timestamp.
 */
 rule additiveBurn(address a, uint256 x,  uint256 y) {
 	env e;
@@ -144,7 +148,7 @@ rule additiveBurn(address a, uint256 x,  uint256 y) {
 	sinvoke burn(e, a, x, index);
 	sinvoke burn(e, a, y, index);
 	uint256 balanceScenario1 = balanceOf(e, a);
-	uint t = x + y;
+	uint256 t = x + y;
 	sinvoke burn(e, a, t ,index) at initialStorage;
 
 	uint256 balanceScenario2 = balanceOf(e, a);
@@ -152,22 +156,19 @@ rule additiveBurn(address a, uint256 x,  uint256 y) {
 }
 
 /**
-Minting and burning are inverse operations.
-
-{bu = balanceOf(u) } 
+Minting and burning are inverse operations:
+{ bu = balanceOf(u) } 
 mint(u,x); burn(u, u, x) 
-	{balanceOf(u) = bu } 
+{ balanceOf(u) = bu }.
 */
 rule inverseMintBurn(address a, uint256 x) {
 	env e;
 	address asset;
+	address delegatedUser;
 	uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
 	uint256 balancebefore = balanceOf(e, a);
-	sinvoke mint(e, a, x, index);
+	sinvoke mint(e, delegatedUser, a, x, index);
 	sinvoke burn(e, a, x, index);
-	uint256 balanceAfter =  balanceOf(e, a);
-	assert balancebefore == balanceAfter, "burn is not inverse of mint";
-}
-
-
-
+	uint256 balanceAfter = balanceOf(e, a);
+	assert balancebefore == balanceAfter, "burn is not the inverse of mint";
+}

specs/harness/LendingPoolHarnessForVariableDebtToken.sol

@@ -2,14 +2,14 @@ pragma solidity ^0.6.8;
 pragma experimental ABIEncoderV2;
 
 import {
-  ReserveConfiguration
+ReserveConfiguration
 } from '../../contracts/libraries/configuration/ReserveConfiguration.sol';
 import {UserConfiguration} from '../../contracts/libraries/configuration/UserConfiguration.sol';
 import {ReserveLogic} from '../../contracts/libraries/logic/ReserveLogic.sol';
 import {ILendingPool} from '../../contracts/interfaces/ILendingPool.sol';
 import {LendingPool} from '../../contracts/lendingpool/LendingPool.sol';
 import {
-  ILendingPoolAddressesProvider
+ILendingPoolAddressesProvider
 } from '../../contracts/interfaces/ILendingPoolAddressesProvider.sol';
 
 /*
@@ -82,35 +82,35 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
   }
 
   function getReserveData(address asset)
-    external
-    override
-    view
-    returns (ReserveLogic.ReserveData memory)
+  external
+  override
+  view
+  returns (ReserveLogic.ReserveData memory)
   {
     return originalPool.getReserveData(asset);
   }
 
   function getUserConfiguration(address user)
-    external
-    override
-    view
-    returns (UserConfiguration.Map memory)
+  external
+  override
+  view
+  returns (UserConfiguration.Map memory)
   {
     return originalPool.getUserConfiguration(user);
   }
 
   function getUserAccountData(address user)
-    external
-    override
-    view
-    returns (
-      uint256 totalCollateralETH,
-      uint256 totalBorrowsETH,
-      uint256 availableBorrowsETH,
-      uint256 currentLiquidationThreshold,
-      uint256 ltv,
-      uint256 healthFactor
-    )
+  external
+  override
+  view
+  returns (
+    uint256 totalCollateralETH,
+    uint256 totalBorrowsETH,
+    uint256 availableBorrowsETH,
+    uint256 currentLiquidationThreshold,
+    uint256 ltv,
+    uint256 healthFactor
+  )
   {
     return originalPool.getUserAccountData(user);
   }
@@ -132,8 +132,8 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
   }
 
   function setReserveInterestRateStrategyAddress(address reserve, address rateStrategyAddress)
-    external
-    override
+  external
+  override
   {
     originalPool.setReserveInterestRateStrategyAddress(reserve, rateStrategyAddress);
   }
@@ -143,10 +143,10 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
   }
 
   function getConfiguration(address reserve)
-    external
-    override
-    view
-    returns (ReserveConfiguration.Map memory)
+  external
+  override
+  view
+  returns (ReserveConfiguration.Map memory)
   {
     return originalPool.getConfiguration(reserve);
   }
@@ -161,10 +161,10 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
   mapping(uint256 => uint256) private reserveNormalizedVariableDebt;
 
   function getReserveNormalizedVariableDebt(address asset)
-    external
-    override
-    view
-    returns (uint256)
+  external
+  override
+  view
+  returns (uint256)
   {
     require(reserveNormalizedVariableDebt[block.timestamp] == 1e27);
     return reserveNormalizedVariableDebt[block.timestamp];