From 03cc32aa32e1f61d3b6b7b8e0daeac01bf7ae5ab Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 16:34:06 +0000
Subject: [PATCH 01/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 47b96e0e..e54a87a9 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -12,3 +12,19 @@ test:
   after_script:
     - docker-compose -f docker-compose.test.yml run contracts-env npm run ci:clean
     - docker-compose -f docker-compose.test.yml down
+
+certora-test:
+  stage: test
+  image: openjdk:13
+  before_script:
+    - echo "export PATH=$PATH:~/.local/bin" >> $BASH_ENV
+    - sudo apt-get update || sudo apt-get update
+    - sudo apt-get install -y software-properties-common
+    - sudo apt-get install python3-pip
+    - pip3 install certora-cli-beta==0.4.1
+    - wget https://github.com/ethereum/solidity/releases/download/v0.6.8/solc-static-linux
+    - chmod +x solc-static-linux
+    - sudo mv solc-static-linux /usr/bin/solc
+  script:
+    - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken. spec --settings -assumeUnwindCond --cache StableDebtToken --staging
+

From 944f6624c89fba6ad54562d504ded62dec7163a3 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 16:42:58 +0000
Subject: [PATCH 02/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index e54a87a9..79e179a5 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -17,7 +17,7 @@ certora-test:
   stage: test
   image: openjdk:13
   before_script:
-    - echo "export PATH=$PATH:~/.local/bin" >> $BASH_ENV
+    - echo "export PATH=$PATH:~/.local/bin"
     - sudo apt-get update || sudo apt-get update
     - sudo apt-get install -y software-properties-common
     - sudo apt-get install python3-pip

From 6e943c8c6e54300973cbd439204308d4a7e60be2 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 16:45:27 +0000
Subject: [PATCH 03/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 79e179a5..190ff1c4 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -18,6 +18,7 @@ certora-test:
   image: openjdk:13
   before_script:
     - echo "export PATH=$PATH:~/.local/bin"
+    - whereis sudo
     - sudo apt-get update || sudo apt-get update
     - sudo apt-get install -y software-properties-common
     - sudo apt-get install python3-pip

From dd37825032ec175ef907ac32a52e2b2077d8f689 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 16:57:39 +0000
Subject: [PATCH 04/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 190ff1c4..0732484f 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -15,7 +15,7 @@ test:
 
 certora-test:
   stage: test
-  image: openjdk:13
+  image: openjdk:15-jdk - linux; amd64
   before_script:
     - echo "export PATH=$PATH:~/.local/bin"
     - whereis sudo

From 21df2d69224c04293ac4772a82201f4a913da89e Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 17:00:59 +0000
Subject: [PATCH 05/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 0732484f..56558772 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -15,7 +15,7 @@ test:
 
 certora-test:
   stage: test
-  image: openjdk:15-jdk - linux; amd64
+  image: openjdk:15-jdk
   before_script:
     - echo "export PATH=$PATH:~/.local/bin"
     - whereis sudo

From 11ed9c396e799783a7022404eaef1f76065b8c19 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 17:09:58 +0000
Subject: [PATCH 06/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 56558772..2872f074 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -15,7 +15,9 @@ test:
 
 certora-test:
   stage: test
-  image: openjdk:15-jdk
+  image: openjdk:15.0-jdk-buster
+  tags:
+    - linux
   before_script:
     - echo "export PATH=$PATH:~/.local/bin"
     - whereis sudo

From 5ab98dc4a87a574ab79b9b87b69cae530481e6cf Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 17:21:46 +0000
Subject: [PATCH 07/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 2872f074..4052dd2b 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -15,19 +15,18 @@ test:
 
 certora-test:
   stage: test
-  image: openjdk:15.0-jdk-buster
+  image: openjdk:15.0-jdk
   tags:
     - linux
   before_script:
     - echo "export PATH=$PATH:~/.local/bin"
-    - whereis sudo
-    - sudo apt-get update || sudo apt-get update
-    - sudo apt-get install -y software-properties-common
-    - sudo apt-get install python3-pip
+    - apt-get update || sudo apt-get update
+    - apt-get install -y software-properties-common
+    - apt-get install python3-pip
     - pip3 install certora-cli-beta==0.4.1
     - wget https://github.com/ethereum/solidity/releases/download/v0.6.8/solc-static-linux
     - chmod +x solc-static-linux
-    - sudo mv solc-static-linux /usr/bin/solc
+    - mv solc-static-linux /usr/bin/solc
   script:
     - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken. spec --settings -assumeUnwindCond --cache StableDebtToken --staging
 

From 4e478aa8ac8d2bb33027b353eb7f931021f9e389 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 17:27:16 +0000
Subject: [PATCH 08/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 4052dd2b..47c6056d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -19,6 +19,8 @@ certora-test:
   tags:
     - linux
   before_script:
+    - wget http://security.ubuntu.com/ubuntu/pool/main/a/apt/apt_2.1.11_amd64.deb -O apt.deb
+    - pkexec dpkg -i apt.deb
     - echo "export PATH=$PATH:~/.local/bin"
     - apt-get update || sudo apt-get update
     - apt-get install -y software-properties-common

From a27cb91a488794c6dc665ee74aa00fc8f377ba7e Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 17:31:07 +0000
Subject: [PATCH 09/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 47c6056d..8aebb51f 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -15,20 +15,17 @@ test:
 
 certora-test:
   stage: test
-  image: openjdk:15.0-jdk
   tags:
     - linux
   before_script:
-    - wget http://security.ubuntu.com/ubuntu/pool/main/a/apt/apt_2.1.11_amd64.deb -O apt.deb
-    - pkexec dpkg -i apt.deb
     - echo "export PATH=$PATH:~/.local/bin"
-    - apt-get update || sudo apt-get update
-    - apt-get install -y software-properties-common
-    - apt-get install python3-pip
+    - sudo apt-get update || sudo apt-get update
+    - sudo apt-get install -y software-properties-common
+    - sudo apt-get install python3-pip
     - pip3 install certora-cli-beta==0.4.1
     - wget https://github.com/ethereum/solidity/releases/download/v0.6.8/solc-static-linux
     - chmod +x solc-static-linux
-    - mv solc-static-linux /usr/bin/solc
+    - sudo mv solc-static-linux /usr/bin/solc
   script:
     - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken. spec --settings -assumeUnwindCond --cache StableDebtToken --staging
 

From 14961cac8c698b6ffc6a32388916a555892e08b5 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 17:34:00 +0000
Subject: [PATCH 10/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 8aebb51f..023c44cd 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -15,8 +15,7 @@ test:
 
 certora-test:
   stage: test
-  tags:
-    - linux
+  image: ubuntu:18.04
   before_script:
     - echo "export PATH=$PATH:~/.local/bin"
     - sudo apt-get update || sudo apt-get update

From 651412e7213466d2640fdf36603a3c1acf7cbef8 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 18:01:52 +0000
Subject: [PATCH 11/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 023c44cd..0571952d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -15,16 +15,17 @@ test:
 
 certora-test:
   stage: test
+  variables:
+    - PATH: "$PATH:~/.local/bin"
   image: ubuntu:18.04
   before_script:
-    - echo "export PATH=$PATH:~/.local/bin"
-    - sudo apt-get update || sudo apt-get update
-    - sudo apt-get install -y software-properties-common
-    - sudo apt-get install python3-pip
+    - apt-get update || apt-get update
+    - apt-get install -y software-properties-common
+    - apt-get install python3-pip
     - pip3 install certora-cli-beta==0.4.1
     - wget https://github.com/ethereum/solidity/releases/download/v0.6.8/solc-static-linux
     - chmod +x solc-static-linux
-    - sudo mv solc-static-linux /usr/bin/solc
+    - mv solc-static-linux /usr/bin/solc
   script:
     - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken. spec --settings -assumeUnwindCond --cache StableDebtToken --staging
 

From 64d7da37e7e6dcbd8686514f1a0604a743a3247c Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 18:02:54 +0000
Subject: [PATCH 12/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 0571952d..36702a0e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -15,8 +15,6 @@ test:
 
 certora-test:
   stage: test
-  variables:
-    - PATH: "$PATH:~/.local/bin"
   image: ubuntu:18.04
   before_script:
     - apt-get update || apt-get update

From 3c0d73eb0c4e1ec2010f634662856b5c20cc93bf Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 18:05:29 +0000
Subject: [PATCH 13/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 36702a0e..2cfa3518 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -15,7 +15,7 @@ test:
 
 certora-test:
   stage: test
-  image: ubuntu:18.04
+  image: openjdk:15-jdk
   before_script:
     - apt-get update || apt-get update
     - apt-get install -y software-properties-common

From ec454f0862d0f261b39c80f96291e03488157992 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 18:07:48 +0000
Subject: [PATCH 14/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 2cfa3518..eebb1df3 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -15,11 +15,10 @@ test:
 
 certora-test:
   stage: test
-  image: openjdk:15-jdk
+  image: python:latest
   before_script:
     - apt-get update || apt-get update
     - apt-get install -y software-properties-common
-    - apt-get install python3-pip
     - pip3 install certora-cli-beta==0.4.1
     - wget https://github.com/ethereum/solidity/releases/download/v0.6.8/solc-static-linux
     - chmod +x solc-static-linux

From aefe0e041f05a3f24552ab5c94a74e41064acccb Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 18:17:31 +0000
Subject: [PATCH 15/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index eebb1df3..3cec3d74 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -17,6 +17,7 @@ certora-test:
   stage: test
   image: python:latest
   before_script:
+    - echo "export PATH=$PATH:~/.local/bin" >> $BASH_ENV
     - apt-get update || apt-get update
     - apt-get install -y software-properties-common
     - pip3 install certora-cli-beta==0.4.1
@@ -24,5 +25,5 @@ certora-test:
     - chmod +x solc-static-linux
     - mv solc-static-linux /usr/bin/solc
   script:
-    - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken. spec --settings -assumeUnwindCond --cache StableDebtToken --staging
+    - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken spec --settings -assumeUnwindCond --cache StableDebtToken --staging
 

From b903f8dc63a9ddef31e9fcc8c3714f36721f90a9 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 18:19:25 +0000
Subject: [PATCH 16/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 3cec3d74..15756d57 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -17,7 +17,7 @@ certora-test:
   stage: test
   image: python:latest
   before_script:
-    - echo "export PATH=$PATH:~/.local/bin" >> $BASH_ENV
+    - echo "export PATH=$PATH:~/.local/bin" >> "$BASH_ENV"
     - apt-get update || apt-get update
     - apt-get install -y software-properties-common
     - pip3 install certora-cli-beta==0.4.1

From 515360d4903a4904bc2f184a4fcc4885471a6985 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 18:22:38 +0000
Subject: [PATCH 17/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 15756d57..5cbc9d32 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -17,7 +17,7 @@ certora-test:
   stage: test
   image: python:latest
   before_script:
-    - echo "export PATH=$PATH:~/.local/bin" >> "$BASH_ENV"
+    - echo export PATH=$PATH:~/.local/bin
     - apt-get update || apt-get update
     - apt-get install -y software-properties-common
     - pip3 install certora-cli-beta==0.4.1

From 388f8cb7bbc96b5792470624085de6705032f214 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 18:29:17 +0000
Subject: [PATCH 18/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 5cbc9d32..25e82c9c 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -20,6 +20,7 @@ certora-test:
     - echo export PATH=$PATH:~/.local/bin
     - apt-get update || apt-get update
     - apt-get install -y software-properties-common
+    - apt-get install openjdk-13-jdk
     - pip3 install certora-cli-beta==0.4.1
     - wget https://github.com/ethereum/solidity/releases/download/v0.6.8/solc-static-linux
     - chmod +x solc-static-linux

From cd1603b949c67fdade1a7e207f3abd023bae7be7 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 18:41:50 +0000
Subject: [PATCH 19/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 25e82c9c..4589a204 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -17,10 +17,15 @@ certora-test:
   stage: test
   image: python:latest
   before_script:
-    - echo export PATH=$PATH:~/.local/bin
+    - export PATH=$PATH:~/.local/bin
     - apt-get update || apt-get update
     - apt-get install -y software-properties-common
-    - apt-get install openjdk-13-jdk
+    - apt-get install curl
+    - curl -O https://download.java.net/java/GA/jdk13/5b8a42f3905b406298b72d750b6919f6/33/GPL/openjdk-13_linux-x64_bin.tar.gz
+    - tar xvf openjdk-13_linux-x64_bin.tar.gz
+    - mv jdk-13 ~/usr/lib/
+    - export JAVA_HOME=~/usr/lib/jdk-13
+    - export PATH=$PATH:$JAVA_HOME/bin
     - pip3 install certora-cli-beta==0.4.1
     - wget https://github.com/ethereum/solidity/releases/download/v0.6.8/solc-static-linux
     - chmod +x solc-static-linux

From 851041a915a6f4dd1abd99d235446fb502d24a1d Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 18:55:06 +0000
Subject: [PATCH 20/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 4589a204..1878ff6e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -23,8 +23,8 @@ certora-test:
     - apt-get install curl
     - curl -O https://download.java.net/java/GA/jdk13/5b8a42f3905b406298b72d750b6919f6/33/GPL/openjdk-13_linux-x64_bin.tar.gz
     - tar xvf openjdk-13_linux-x64_bin.tar.gz
-    - mv jdk-13 ~/usr/lib/
-    - export JAVA_HOME=~/usr/lib/jdk-13
+    - mkdir --parents ~/java; mv jdk-13 $_
+    - export JAVA_HOME=~/java/jdk-13
     - export PATH=$PATH:$JAVA_HOME/bin
     - pip3 install certora-cli-beta==0.4.1
     - wget https://github.com/ethereum/solidity/releases/download/v0.6.8/solc-static-linux

From 5ea03d441809438c267c348cdbfbd441a0bb0ee1 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 18:58:10 +0000
Subject: [PATCH 21/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1878ff6e..b2c12dc2 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -26,6 +26,7 @@ certora-test:
     - mkdir --parents ~/java; mv jdk-13 $_
     - export JAVA_HOME=~/java/jdk-13
     - export PATH=$PATH:$JAVA_HOME/bin
+    - whereis java
     - pip3 install certora-cli-beta==0.4.1
     - wget https://github.com/ethereum/solidity/releases/download/v0.6.8/solc-static-linux
     - chmod +x solc-static-linux

From cec1befb29361b1982a3a3048fd61fa7a3f21400 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 19:02:27 +0000
Subject: [PATCH 22/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b2c12dc2..1f627835 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -32,5 +32,5 @@ certora-test:
     - chmod +x solc-static-linux
     - mv solc-static-linux /usr/bin/solc
   script:
-    - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken spec --settings -assumeUnwindCond --cache StableDebtToken --staging
+    - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond --cache StableDebtToken --staging
 

From 7eb2382140f8f416144440db40db1b0f8e292755 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 19:11:47 +0000
Subject: [PATCH 23/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1f627835..af833279 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -20,17 +20,11 @@ certora-test:
     - export PATH=$PATH:~/.local/bin
     - apt-get update || apt-get update
     - apt-get install -y software-properties-common
-    - apt-get install curl
-    - curl -O https://download.java.net/java/GA/jdk13/5b8a42f3905b406298b72d750b6919f6/33/GPL/openjdk-13_linux-x64_bin.tar.gz
-    - tar xvf openjdk-13_linux-x64_bin.tar.gz
-    - mkdir --parents ~/java; mv jdk-13 $_
-    - export JAVA_HOME=~/java/jdk-13
-    - export PATH=$PATH:$JAVA_HOME/bin
-    - whereis java
     - pip3 install certora-cli-beta==0.4.1
     - wget https://github.com/ethereum/solidity/releases/download/v0.6.8/solc-static-linux
     - chmod +x solc-static-linux
     - mv solc-static-linux /usr/bin/solc
+    - export PATH=$PATH:/usr/bin/solc/solc-static-linux
   script:
     - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond --cache StableDebtToken --staging
 

From e71c23afa48a213d46c4c3cd38a91360343eb251 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 19:17:24 +0000
Subject: [PATCH 24/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index af833279..10958d2f 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -26,5 +26,5 @@ certora-test:
     - mv solc-static-linux /usr/bin/solc
     - export PATH=$PATH:/usr/bin/solc/solc-static-linux
   script:
-    - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond --cache StableDebtToken --staging
+    - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond --cache StableDebtToken --staging
 

From dce89a81a23c1d58f0b5a530453274ffb15ede8c Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 1 Nov 2020 19:43:24 +0000
Subject: [PATCH 25/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 10958d2f..bb16d272 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -17,7 +17,6 @@ certora-test:
   stage: test
   image: python:latest
   before_script:
-    - export PATH=$PATH:~/.local/bin
     - apt-get update || apt-get update
     - apt-get install -y software-properties-common
     - pip3 install certora-cli-beta==0.4.1
@@ -27,4 +26,6 @@ certora-test:
     - export PATH=$PATH:/usr/bin/solc/solc-static-linux
   script:
     - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond --cache StableDebtToken --staging
+    - certoraRun specs/harness/UserConfigurationHarness.sol --verify UserConfigurationHarness:specs/UserConfiguration.spec --settings -useBitVectorTheory --staging
+    - certoraRun contracts/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -assumeUnwindCond,-useNonLinearArithmetic --cache VariableDebtToken --staging
 

From e0be3a316339e36ac055d8a494f420d96682da41 Mon Sep 17 00:00:00 2001
From: pistiner <59415933+orpistiner@users.noreply.github.com>
Date: Thu, 12 Nov 2020 10:35:40 +0200
Subject: [PATCH 26/38] Changes in harness of VariableDebtToken

---
 specs/harness/LendingPoolHarnessForVariableDebtToken.sol | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol
index a6ffb6f2..7ecde340 100644
--- a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol
+++ b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol
@@ -24,9 +24,9 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
   ) external override {
     originalPool.deposit(asset, amount, onBehalfOf, referralCode);
   }
-
-  function withdraw(address asset, uint256 amount) external override {
-    originalPool.withdraw(asset, amount);
+	
+   function withdraw(address reserve, uint256 amount, address to) external override {
+	originalPool.withdraw(reserve, amount, to);
   }
 
   function getBorrowAllowance(

From 5ad4182508b4abdd3f10e4b8e4e3ba8456736716 Mon Sep 17 00:00:00 2001
From: pistiner <59415933+orpistiner@users.noreply.github.com>
Date: Thu, 12 Nov 2020 10:54:47 +0200
Subject: [PATCH 27/38] Changes in /LendingPoolHarnessForVariableDebtToken

---
 ...LendingPoolHarnessForVariableDebtToken.sol | 48 +++++++++----------
 1 file changed, 24 insertions(+), 24 deletions(-)

diff --git a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol
index f5ea9be1..a042e026 100644
--- a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol
+++ b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol
@@ -20,61 +20,61 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
   LendingPool private originalPool;
 
   function deposit(
-    address asset,
+    address reserve,
     uint256 amount,
     address onBehalfOf,
     uint16 referralCode
   ) external override {
-    originalPool.deposit(asset, amount, onBehalfOf, referralCode);
+    originalPool.deposit(reserve, amount, onBehalfOf, referralCode);
   }
 
   function withdraw(
-    address asset,
+    address reserve,
     uint256 amount,
     address to
   ) external override {
-    originalPool.withdraw(asset, amount, to);
+    originalPool.withdraw(reserve, amount, to);
   }
 
   function borrow(
-    address asset,
+    address reserve,
     uint256 amount,
     uint256 interestRateMode,
     uint16 referralCode,
     address onBehalfOf
   ) external override {
-    originalPool.borrow(asset, amount, interestRateMode, referralCode, onBehalfOf);
+    originalPool.borrow(reserve, amount, interestRateMode, referralCode, onBehalfOf);
   }
 
   function repay(
-    address asset,
+    address reserve,
     uint256 amount,
     uint256 rateMode,
     address onBehalfOf
   ) external override {
-    originalPool.repay(asset, amount, rateMode, onBehalfOf);
+    originalPool.repay(reserve, amount, rateMode, onBehalfOf);
   }
 
-  function swapBorrowRateMode(address asset, uint256 rateMode) external override {
-    originalPool.swapBorrowRateMode(asset, rateMode);
+  function swapBorrowRateMode(address reserve, uint256 rateMode) external override {
+    originalPool.swapBorrowRateMode(reserve, rateMode);
   }
 
-  function rebalanceStableBorrowRate(address asset, address user) external override {
-    originalPool.rebalanceStableBorrowRate(asset, user);
+  function rebalanceStableBorrowRate(address reserve, address user) external override {
+    originalPool.rebalanceStableBorrowRate(reserve, user);
   }
 
-  function setUserUseReserveAsCollateral(address asset, bool useAsCollateral) external override {
-    originalPool.setUserUseReserveAsCollateral(asset, useAsCollateral);
+  function setUserUseReserveAsCollateral(address reserve, bool useAsCollateral) external override {
+    originalPool.setUserUseReserveAsCollateral(reserve, useAsCollateral);
   }
 
   function liquidationCall(
     address collateral,
-    address asset,
+    address reserve,
     address user,
     uint256 purchaseAmount,
     bool receiveAToken
   ) external override {
-    originalPool.liquidationCall(collateral, asset, user, purchaseAmount, receiveAToken);
+    originalPool.liquidationCall(collateral, reserve, user, purchaseAmount, receiveAToken);
   }
 
   function getReservesList() external override view returns (address[] memory) {
@@ -116,14 +116,14 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
   }
 
   function initReserve(
-    address asset,
+    address reserve,
     address aTokenAddress,
     address stableDebtAddress,
     address variableDebtAddress,
     address interestRateStrategyAddress
   ) external override {
     originalPool.initReserve(
-      asset,
+      reserve,
       aTokenAddress,
       stableDebtAddress,
       variableDebtAddress,
@@ -131,24 +131,24 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
     );
   }
 
-  function setReserveInterestRateStrategyAddress(address asset, address rateStrategyAddress)
+  function setReserveInterestRateStrategyAddress(address reserve, address rateStrategyAddress)
     external
     override
   {
-    originalPool.setReserveInterestRateStrategyAddress(asset, rateStrategyAddress);
+    originalPool.setReserveInterestRateStrategyAddress(reserve, rateStrategyAddress);
   }
 
-  function setConfiguration(address asset, uint256 configuration) external override {
-    originalPool.setConfiguration(asset, configuration);
+  function setConfiguration(address reserve, uint256 configuration) external override {
+    originalPool.setConfiguration(reserve, configuration);
   }
 
-  function getConfiguration(address asset)
+  function getConfiguration(address reserve)
     external
     override
     view
     returns (ReserveConfiguration.Map memory)
   {
-    return originalPool.getConfiguration(asset);
+    return originalPool.getConfiguration(reserve);
   }
 
   mapping(uint256 => uint256) private reserveNormalizedIncome;

From dd0e3064e3efdcbaa0a08cc6b4b89d90ed5a7619 Mon Sep 17 00:00:00 2001
From: pistiner <59415933+orpistiner@users.noreply.github.com>
Date: Sun, 22 Nov 2020 22:20:43 +0200
Subject: [PATCH 28/38] Updates to the VariableDebtToken spec

---
 specs/VariableDebtToken.spec                  | 113 +++++++++---------
 ...LendingPoolHarnessForVariableDebtToken.sol |  62 +++++-----
 2 files changed, 88 insertions(+), 87 deletions(-)

diff --git a/specs/VariableDebtToken.spec b/specs/VariableDebtToken.spec
index 73e7e39c..eb19d1b4 100644
--- a/specs/VariableDebtToken.spec
+++ b/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";
+}
\ No newline at end of file
diff --git a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol
index a042e026..6f6ea7e1 100644
--- a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol
+++ b/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];

From 219d765f970135079fab6129ab89106c01ea4f19 Mon Sep 17 00:00:00 2001
From: pistiner <59415933+orpistiner@users.noreply.github.com>
Date: Sun, 22 Nov 2020 22:39:06 +0200
Subject: [PATCH 29/38] Updated running script of VariableDebtToken

---
 runVariableTokenCLI.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/runVariableTokenCLI.sh b/runVariableTokenCLI.sh
index 483e152e..cd037a7c 100644
--- a/runVariableTokenCLI.sh
+++ b/runVariableTokenCLI.sh
@@ -1 +1 @@
-certoraRun contracts/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --solc solc6.8 --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -assumeUnwindCond,-useNonLinearArithmetic --cache VariableDebtToken --staging
\ No newline at end of file
+certoraRun contracts/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --solc solc6.12 --solc_args '--optimize' --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -b=4,-assumeUnwindCond,-useNonLinearArithmetic --staging
\ No newline at end of file

From fa0d49e280eb36dd7a924f940ca44bdf119a1120 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 22 Nov 2020 20:43:01 +0000
Subject: [PATCH 30/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index bb16d272..ac8117d7 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -20,12 +20,12 @@ certora-test:
     - apt-get update || apt-get update
     - apt-get install -y software-properties-common
     - pip3 install certora-cli-beta==0.4.1
-    - wget https://github.com/ethereum/solidity/releases/download/v0.6.8/solc-static-linux
+    - wget https://github.com/ethereum/solidity/releases/download/v0.6.12/solc-static-linux
     - chmod +x solc-static-linux
     - mv solc-static-linux /usr/bin/solc
     - export PATH=$PATH:/usr/bin/solc/solc-static-linux
   script:
     - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond --cache StableDebtToken --staging
     - certoraRun specs/harness/UserConfigurationHarness.sol --verify UserConfigurationHarness:specs/UserConfiguration.spec --settings -useBitVectorTheory --staging
-    - certoraRun contracts/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -assumeUnwindCond,-useNonLinearArithmetic --cache VariableDebtToken --staging
+    - certoraRun contracts/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --solc_args '--optimize' --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -assumeUnwindCond,-useNonLinearArithmetic,-b=4 --cache VariableDebtToken --staging
 

From f90e53293d7a9fabc985527280aa08bc84657133 Mon Sep 17 00:00:00 2001
From: pistiner <59415933+orpistiner@users.noreply.github.com>
Date: Sun, 22 Nov 2020 23:19:56 +0200
Subject: [PATCH 31/38] Updated StableDebtToken spec

---
 runStableTokenCLI.sh       |  2 +-
 specs/StableDebtToken.spec | 84 ++++++++++++++++++++------------------
 2 files changed, 45 insertions(+), 41 deletions(-)

diff --git a/runStableTokenCLI.sh b/runStableTokenCLI.sh
index 8903f2f9..f9d852b3 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 --cache StableDebtToken --staging master
\ No newline at end of file
+certoraRun.py specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.12 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --cache StableDebtToken --staging
\ No newline at end of file
diff --git a/specs/StableDebtToken.spec b/specs/StableDebtToken.spec
index 0d6e0c5d..16fed3bb 100644
--- a/specs/StableDebtToken.spec
+++ b/specs/StableDebtToken.spec
@@ -14,82 +14,85 @@ rule integrityTimeStamp(address user, method f) {
 /**
 TotalSupply is the sum of all users’ balances
 	
-totalSupply(t) = Σaddress u. balanceOf(u,t)
+totalSupply(t) = Σaddress u. balanceOf(u,t).
 
-Check that each possible opertaion changes the balance of at most one user
+Checks that each possible operation changes the balance of at most one user.
 */
-rule balanceOfChange(address a, address b, method f )
+rule balanceOfChange(address a, address b, method f)
 {
 	env e;
 	require a!=b;
 	require sinvoke getIncentivesController(e) == 0;
-	uint256 balanceABefore = sinvoke balanceOf(e,a);
-	uint256 balanceBBefore = sinvoke balanceOf(e,b);
+	uint256 balanceABefore = sinvoke balanceOf(e, a);
+	uint256 balanceBBefore = sinvoke balanceOf(e, b);
 	 
 	calldataarg arg;
 	sinvoke f(e, arg); 
 
-	uint256 balanceAAfter = sinvoke balanceOf(e,a);
-	uint256 balanceBAfter = sinvoke balanceOf(e,b);
+	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 change to total supply is coherent with the changes to balance
+Checks that the change to total supply is coherent with the change to balance due to an operation
+(which is not burn).
 */
 rule integirtyBalanceOfTotalSupply(address a, method f )
 {
 	env e;
 	require sinvoke getIncentivesController(e) == 0;
-	uint256 balanceABefore = sinvoke balanceOf(e,a);
+	uint256 balanceABefore = sinvoke balanceOf(e, a);
 	uint256 totalSupplyBefore = sinvoke totalSupply(e);
 	 
 	calldataarg arg;
 	sinvoke f(e, arg); 
-	require (f.selector != burn(address,uint256).selector );
-	uint256 balanceAAfter = sinvoke balanceOf(e,a);
+	require (f.selector != burn(address, uint256).selector);
+	uint256 balanceAAfter = sinvoke balanceOf(e, a);
 	uint256 totalSupplyAfter = sinvoke totalSupply(e);
 
-	assert  (balanceAAfter != balanceABefore  => ( balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+	assert  (balanceAAfter != balanceABefore  => (balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
 }
 
-/* Burn behaves differently and due to accumulation errors might have less total supply than the balance
+/**
+Burn behaves differently and due to accumulation errors might have less total supply than the balance.
 */
 rule integirtyBalanceOfTotalSupplyOnBurn(address a, method f)
 {
 	env e;
 	require sinvoke getIncentivesController(e) == 0;
-	uint256 balanceABefore = sinvoke balanceOf(e,a);
+	uint256 balanceABefore = sinvoke balanceOf(e, a);
 	uint256 totalSupplyBefore = sinvoke totalSupply(e);
 	 
 	uint256 x;
 	sinvoke burn(e, a, x); 
-	uint256 balanceAAfter = sinvoke balanceOf(e,a);
+	uint256 balanceAAfter = sinvoke balanceOf(e, a);
 	uint256 totalSupplyAfter = sinvoke totalSupply(e);
 	if (totalSupplyBefore > x)
-		assert  (balanceAAfter != balanceABefore  => ( balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+		assert (balanceAAfter != balanceABefore  => (balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
 	else
-		assert  (totalSupplyAfter == 0 );
+		assert (totalSupplyAfter == 0);
 }
 
 /**
-Mint inceases the balanceOf user a as expected
+Mint increases the balanceOf user a as expected.
 */
 rule integrityMint(address a, uint256 x) {
 	env e;
+	address delegatedUser;
 	require sinvoke getIncentivesController(e) == 0;
 	uint256 index;
 	uint256 balancebefore = sinvoke balanceOf(e,a);
-	sinvoke mint(e,a,x,index);
+	sinvoke mint(e, delegatedUser, a, x, index);
 	
 	uint256 balanceAfter = sinvoke balanceOf(e,a);
 	assert balanceAfter == balancebefore+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
+Mint is additive, namely it 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,
@@ -97,18 +100,19 @@ and therefore it is currently excluded from the CI.
 */
 rule additiveMint(address a, uint256 x, uint256 y) {
 	env e;
+	address delegatedUser;
 	require sinvoke getIncentivesController(e) == 0;
-	require getUserStableRate(e,a) == 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);
+	sinvoke mint(e, delegatedUser, a, x, index);
+	sinvoke mint(e, delegatedUser, a, y, index);
+	uint256 balanceScenario1 = sinvoke balanceOf(e, a);
 	
 	uint256 t = x + y;
-	sinvoke mint(e,a, t ,index) at initialStorage;
+	sinvoke mint(e, delegatedUser, a, t ,index) at initialStorage;
 	
-	uint256 balanceScenario2 = sinvoke balanceOf(e,a);
+	uint256 balanceScenario2 = sinvoke balanceOf(e, a);
 	assert balanceScenario1 == balanceScenario2, "mint is not additive";
 }
 
@@ -116,10 +120,10 @@ rule integrityBurn(address a, uint256 x) {
 	env e;
 	require sinvoke getIncentivesController(e) == 0;
 	uint256 index;
-	uint256 balancebefore = sinvoke balanceOf(e,a);
+	uint256 balancebefore = sinvoke balanceOf(e, a);
 	sinvoke burn(e,a,x);
 	
-	uint256 balanceAfter = sinvoke balanceOf(e,a);
+	uint256 balanceAfter = sinvoke balanceOf(e, a);
 	assert balanceAfter == balancebefore - x;
 }
 
@@ -139,17 +143,17 @@ rule additiveBurn(address a, uint256 x,  uint256 y) {
 
 
 /**
-mint and burn are inverse operations
-Thus, totalSupply is back to initial state
-BalanceOf user is back to initial state */
+Mint and burn are inverse operations.
+Therefore, both totalSupply and BalanceOf user are back to the initial state.
+*/
 rule inverseMintBurn(address a, uint256 x) {
 	env e;
+	address delegatedUser;
 	require sinvoke getIncentivesController(e) == 0;
 	uint256 index;
-	uint256 balancebefore = sinvoke balanceOf(e,a);
-	sinvoke mint(e,a,x,index);
-	sinvoke burn(e,a,x);
-	uint256 balanceAfter = sinvoke balanceOf(e,a);
-	assert balancebefore == balanceAfter, "burn is not inverse of mint";
-}
-
+	uint256 balancebefore = sinvoke balanceOf(e, a);
+	sinvoke mint(e, delegatedUser, a, x, index);
+	sinvoke burn(e, a, x);
+	uint256 balanceAfter = sinvoke balanceOf(e, a);
+	assert balancebefore == balanceAfter, "burn is not the inverse of mint";
+}
\ No newline at end of file

From 87d23c65ea2b4b21bf24ef74eca0a1773edf97dd Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Sun, 22 Nov 2020 21:24:26 +0000
Subject: [PATCH 32/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index ac8117d7..7b3a0163 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -25,7 +25,7 @@ certora-test:
     - mv solc-static-linux /usr/bin/solc
     - export PATH=$PATH:/usr/bin/solc/solc-static-linux
   script:
-    - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond --cache StableDebtToken --staging
+    - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --cache StableDebtToken --staging
     - certoraRun specs/harness/UserConfigurationHarness.sol --verify UserConfigurationHarness:specs/UserConfiguration.spec --settings -useBitVectorTheory --staging
     - certoraRun contracts/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --solc_args '--optimize' --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -assumeUnwindCond,-useNonLinearArithmetic,-b=4 --cache VariableDebtToken --staging
 

From 296f1046ad8717bf9eea5f076109f11450387ee1 Mon Sep 17 00:00:00 2001
From: pistiner <59415933+orpistiner@users.noreply.github.com>
Date: Mon, 23 Nov 2020 19:25:47 +0200
Subject: [PATCH 33/38] Updated integirtyBalanceOfTotalSupplyOnBurn rule for
 StableDebtToken.

---
 runStableTokenCLI.sh                     |  2 +-
 specs/StableDebtToken.spec               | 41 +++++++++++++++++++-----
 specs/harness/StableDebtTokenHarness.sol | 10 +++++-
 3 files changed, 43 insertions(+), 10 deletions(-)

diff --git a/runStableTokenCLI.sh b/runStableTokenCLI.sh
index f9d852b3..653eaff1 100644
--- a/runStableTokenCLI.sh
+++ b/runStableTokenCLI.sh
@@ -1 +1 @@
-certoraRun.py specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.12 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --cache StableDebtToken --staging
\ No newline at end of file
+certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.12 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --staging
\ No newline at end of file
diff --git a/specs/StableDebtToken.spec b/specs/StableDebtToken.spec
index 16fed3bb..a486d335 100644
--- a/specs/StableDebtToken.spec
+++ b/specs/StableDebtToken.spec
@@ -36,7 +36,7 @@ rule balanceOfChange(address a, address b, method f)
 }
 
 /**
-Checks that the change to total supply is coherent with the change to balance due to an operation
+Checks that the change to total supply is coherent with the change to user balance due to an operation
 (which is not burn).
 */
 rule integirtyBalanceOfTotalSupply(address a, method f )
@@ -55,24 +55,49 @@ rule integirtyBalanceOfTotalSupply(address a, method f )
 	assert  (balanceAAfter != balanceABefore  => (balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
 }
 
+
 /**
-Burn behaves differently and due to accumulation errors might have less total supply than the balance.
+Checks that the change to total supply is coherent with the change to user balance due to a burn operation.
 */
-rule integirtyBalanceOfTotalSupplyOnBurn(address a, method f)
+rule integirtyBalanceOfTotalSupplyOnBurn(address a, uint256 x)
 {
 	env e;
 	require sinvoke getIncentivesController(e) == 0;
+	
 	uint256 balanceABefore = sinvoke balanceOf(e, a);
+	
 	uint256 totalSupplyBefore = sinvoke totalSupply(e);
-	 
-	uint256 x;
+	uint256 averageStableRateBefore = sinvoke getAverageStableRate(e);
+	uint256 debtSupplyBefore = sinvoke rayWadMul(e, averageStableRateBefore, totalSupplyBefore);
+	
+	uint256 stableRateA = sinvoke getUserStableRate(e, a);
+	uint256 repaidDebtA = sinvoke rayWadMul(e, stableRateA, x);
+	
+	
 	sinvoke burn(e, a, x); 
 	uint256 balanceAAfter = sinvoke balanceOf(e, a);
 	uint256 totalSupplyAfter = sinvoke totalSupply(e);
-	if (totalSupplyBefore > x)
-		assert (balanceAAfter != balanceABefore  => (balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
-	else
+
+	if(totalSupplyBefore > x) {
+	    /* The amount being burned (x) is smaller than the total supply */
+		if(repaidDebtA >= debtSupplyBefore) {
+			/*
+			The user debt being repaid is at least the debt supply.
+			The total supply becomes 0.
+			*/
+			assert(totalSupplyAfter == 0);
+		}
+		else {
+			assert(balanceAAfter != balanceABefore  =>
+			(balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+		}
+	}
+	else {
+	/* The amount being burned (x) is at least the total supply.
+	   The total supply becomes 0.
+	*/
 		assert (totalSupplyAfter == 0);
+	}
 }
 
 /**
diff --git a/specs/harness/StableDebtTokenHarness.sol b/specs/harness/StableDebtTokenHarness.sol
index 69a9aa8a..6a8323ca 100644
--- a/specs/harness/StableDebtTokenHarness.sol
+++ b/specs/harness/StableDebtTokenHarness.sol
@@ -11,7 +11,11 @@ contract StableDebtTokenHarness is StableDebtToken {
     string memory symbol,
     address incentivesController
   ) public StableDebtToken(pool, underlyingAsset, name, symbol, incentivesController) {}
-
+	
+	
+   /**
+   Simplification: The user accumulates no interest (the balance increase is always 0).
+   **/
   function balanceOf(address account) public override view returns (uint256) {
     return IncentivizedERC20.balanceOf(account);
   }
@@ -23,4 +27,8 @@ contract StableDebtTokenHarness is StableDebtToken {
   function getIncentivesController() public view returns (address) {
     return address(_incentivesController);
   }
+  
+  function rayWadMul(uint256 aRay, uint256 bWad) external view returns(uint256) {
+	return aRay.rayMul(bWad.wadToRay());
+  }
 }

From 66bb895cec00398286caf27f21a2d243d3d4173c Mon Sep 17 00:00:00 2001
From: pistiner <59415933+orpistiner@users.noreply.github.com>
Date: Tue, 24 Nov 2020 14:53:09 +0200
Subject: [PATCH 34/38] Updated running script of UserConfiguration library.

---
 runUserConfigCLI.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/runUserConfigCLI.sh b/runUserConfigCLI.sh
index f3ddbacc..776c032e 100644
--- a/runUserConfigCLI.sh
+++ b/runUserConfigCLI.sh
@@ -1 +1 @@
-certoraRun specs/harness/UserConfigurationHarness.sol  --solc solc6.8 --verify UserConfigurationHarness:specs/UserConfiguration.spec --settings -useBitVectorTheory --staging master
+certoraRun specs/harness/UserConfigurationHarness.sol  --solc solc6.12 --verify UserConfigurationHarness:specs/UserConfiguration.spec --solc_args '--optimize' --settings -useBitVectorTheory --staging

From 6dc710fd455d98817da6395ca1010d274dc6dbcd Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Tue, 24 Nov 2020 13:02:57 +0000
Subject: [PATCH 35/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 7b3a0163..e0f229d0 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -26,6 +26,6 @@ certora-test:
     - export PATH=$PATH:/usr/bin/solc/solc-static-linux
   script:
     - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --cache StableDebtToken --staging
-    - certoraRun specs/harness/UserConfigurationHarness.sol --verify UserConfigurationHarness:specs/UserConfiguration.spec --settings -useBitVectorTheory --staging
+    - certoraRun specs/harness/UserConfigurationHarness.sol --verify UserConfigurationHarness:specs/UserConfiguration.spec --solc_args '--optimize' --settings -useBitVectorTheory --staging
     - certoraRun contracts/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --solc_args '--optimize' --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -assumeUnwindCond,-useNonLinearArithmetic,-b=4 --cache VariableDebtToken --staging
 

From bb52ba0659554b2eccdf60097d699f1b4b318bcd Mon Sep 17 00:00:00 2001
From: pistiner <59415933+orpistiner@users.noreply.github.com>
Date: Tue, 24 Nov 2020 15:46:09 +0200
Subject: [PATCH 36/38] Updated import paths

---
 runVariableTokenCLI.sh                                   | 2 +-
 specs/harness/LendingPoolHarnessForVariableDebtToken.sol | 8 ++++----
 specs/harness/StableDebtTokenHarness.sol                 | 4 ++--
 specs/harness/UserConfigurationHarness.sol               | 2 +-
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/runVariableTokenCLI.sh b/runVariableTokenCLI.sh
index cd037a7c..5d549a8b 100644
--- a/runVariableTokenCLI.sh
+++ b/runVariableTokenCLI.sh
@@ -1 +1 @@
-certoraRun contracts/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --solc solc6.12 --solc_args '--optimize' --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -b=4,-assumeUnwindCond,-useNonLinearArithmetic --staging
\ No newline at end of file
+certoraRun contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --solc solc6.12 --solc_args '--optimize' --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -b=4,-assumeUnwindCond,-useNonLinearArithmetic --staging
\ No newline at end of file
diff --git a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol
index e6c0ff0b..5b14a5de 100644
--- a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol
+++ b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol
@@ -3,11 +3,11 @@ pragma experimental ABIEncoderV2;
 
 import {
 ReserveConfiguration
-} from '../../contracts/libraries/configuration/ReserveConfiguration.sol';
-import {UserConfiguration} from '../../contracts/libraries/configuration/UserConfiguration.sol';
-import {ReserveLogic} from '../../contracts/libraries/logic/ReserveLogic.sol';
+} from '../../contracts/protocol/libraries/configuration/ReserveConfiguration.sol';
+import {UserConfiguration} from '../../contracts/protocol/libraries/configuration/UserConfiguration.sol';
+import {ReserveLogic} from '../../contracts/protocol/libraries/logic/ReserveLogic.sol';
 import {ILendingPool} from '../../contracts/interfaces/ILendingPool.sol';
-import {LendingPool} from '../../contracts/lendingpool/LendingPool.sol';
+import {LendingPool} from '../../contracts/protocol/lendingpool/LendingPool.sol';
 import {
 ILendingPoolAddressesProvider
 } from '../../contracts/interfaces/ILendingPoolAddressesProvider.sol';
diff --git a/specs/harness/StableDebtTokenHarness.sol b/specs/harness/StableDebtTokenHarness.sol
index 6a8323ca..1218e0d9 100644
--- a/specs/harness/StableDebtTokenHarness.sol
+++ b/specs/harness/StableDebtTokenHarness.sol
@@ -1,7 +1,7 @@
 pragma solidity 0.6.12;
 
-import {StableDebtToken} from '../../contracts/tokenization/StableDebtToken.sol';
-import {IncentivizedERC20} from '../../contracts/tokenization/IncentivizedERC20.sol';
+import {StableDebtToken} from '../../contracts/protocol/tokenization/StableDebtToken.sol';
+import {IncentivizedERC20} from '../../contracts/protocol/tokenization/IncentivizedERC20.sol';
 
 contract StableDebtTokenHarness is StableDebtToken {
   constructor(
diff --git a/specs/harness/UserConfigurationHarness.sol b/specs/harness/UserConfigurationHarness.sol
index 0780c222..1ebd6e34 100644
--- a/specs/harness/UserConfigurationHarness.sol
+++ b/specs/harness/UserConfigurationHarness.sol
@@ -1,7 +1,7 @@
 pragma solidity 0.6.12;
 pragma experimental ABIEncoderV2;
 
-import {UserConfiguration} from '../../contracts/libraries/configuration/UserConfiguration.sol';
+import {UserConfiguration} from '../../contracts/protocol/libraries/configuration/UserConfiguration.sol';
 
 /*
 A wrapper contract for calling functions from the library UserConfiguration.

From 42954bca141b013df10ea7028dbf0ad23e795129 Mon Sep 17 00:00:00 2001
From: pistiner <or@certora.com>
Date: Tue, 24 Nov 2020 13:48:09 +0000
Subject: [PATCH 37/38] Update .gitlab-ci.yml

---
 .gitlab-ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index cd66ae5b..a722497e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -39,5 +39,5 @@ certora-test:
   script:
     - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --cache StableDebtToken --staging
     - certoraRun specs/harness/UserConfigurationHarness.sol --verify UserConfigurationHarness:specs/UserConfiguration.spec --solc_args '--optimize' --settings -useBitVectorTheory --staging
-    - certoraRun contracts/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --solc_args '--optimize' --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -assumeUnwindCond,-useNonLinearArithmetic,-b=4 --cache VariableDebtToken --staging
+    - certoraRun contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --solc_args '--optimize' --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -assumeUnwindCond,-useNonLinearArithmetic,-b=4 --cache VariableDebtToken --staging
 

From 7c53ad84fa5109b26f488582d6561c9365d4cc1b Mon Sep 17 00:00:00 2001
From: pistiner <59415933+orpistiner@users.noreply.github.com>
Date: Tue, 24 Nov 2020 16:08:23 +0200
Subject: [PATCH 38/38] fixed syntax error

---
 specs/harness/LendingPoolHarnessForVariableDebtToken.sol | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol
index 5b14a5de..cb699e39 100644
--- a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol
+++ b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol
@@ -101,11 +101,11 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
 
   function getUserAccountData(address user)
     external
-    override
     view
+    override
     returns (
       uint256 totalCollateralETH,
-      uint256 totalBorrowsETH,
+      uint256 totalDebtETH,
       uint256 availableBorrowsETH,
       uint256 currentLiquidationThreshold,
       uint256 ltv,