From 5cc6acce8612597bdcd43c8e217739770400c144 Mon Sep 17 00:00:00 2001
From: pistiner <59415933+orpistiner@users.noreply.github.com>
Date: Thu, 29 Oct 2020 23:19:11 +0200
Subject: [PATCH] Updates in the specification of StableDebtToken

---
 runStableTokenCLI.sh       |  2 +-
 specs/StableDebtToken.spec | 14 ++++++++++----
 2 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/runStableTokenCLI.sh b/runStableTokenCLI.sh
index 658c7663..8903f2f9 100644
--- a/runStableTokenCLI.sh
+++ b/runStableTokenCLI.sh
@@ -1 +1 @@
-certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-useNonLinearArithmetic --cache StableDebtToken --staging master
\ No newline at end of file
+certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond --cache StableDebtToken --staging master
\ No newline at end of file
diff --git a/specs/StableDebtToken.spec b/specs/StableDebtToken.spec
index 718dcb60..0d6e0c5d 100644
--- a/specs/StableDebtToken.spec
+++ b/specs/StableDebtToken.spec
@@ -90,19 +90,25 @@ rule integrityMint(address a, uint256 x) {
 /**
 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
+
+Note: We assume that the stable rate of the user is 0.
+The case where the rate is non-zero takes much more time to prove,
+and therefore it is currently excluded from the CI.
 */
 rule additiveMint(address a, uint256 x, uint256 y) {
 	env e;
 	require sinvoke getIncentivesController(e) == 0;
+	require getUserStableRate(e,a) == 0;
 	uint256 index;
 	storage initialStorage = lastStorage;
 	sinvoke mint(e,a,x,index);
 	sinvoke mint(e,a,y,index);
 	uint256 balanceScenario1 = sinvoke balanceOf(e,a);
-	uint t = x + y;
+	
+	uint256 t = x + y;
 	sinvoke mint(e,a, t ,index) at initialStorage;
-
-	uint256 balanceScenario2 = sinvoke  balanceOf(e,a);
+	
+	uint256 balanceScenario2 = sinvoke balanceOf(e,a);
 	assert balanceScenario1 == balanceScenario2, "mint is not additive";
 }
 
@@ -124,7 +130,7 @@ rule additiveBurn(address a, uint256 x,  uint256 y) {
 	sinvoke burn(e, a, x);
 	sinvoke burn(e, a, y);
 	uint256 balanceScenario1 = balanceOf(e, a);
-	uint t = x + y;
+	uint256 t = x + y;
 	sinvoke burn(e, a, t) at initialStorage;
 
 	uint256 balanceScenario2 = balanceOf(e, a);