From 2304dd7bb117f844daa8535732a44966620d1ad1 Mon Sep 17 00:00:00 2001
From: Michael George <mdgeorge@cs.cornell.edu>
Date: Fri, 17 Dec 2021 09:36:01 -0500
Subject: [PATCH] added script for checking token sanity

---
 certora/harnesses/ERC20PermitHarness.sol  |  5 +++++
 certora/harnesses/ERC20WrapperHarness.sol |  9 +++++++++
 certora/scripts/sanityTokens.sh           | 17 +++++++++++++++++
 3 files changed, 31 insertions(+)
 create mode 100644 certora/harnesses/ERC20PermitHarness.sol
 create mode 100644 certora/harnesses/ERC20WrapperHarness.sol
 create mode 100755 certora/scripts/sanityTokens.sh

diff --git a/certora/harnesses/ERC20PermitHarness.sol b/certora/harnesses/ERC20PermitHarness.sol
new file mode 100644
index 000000000..5b51788fa
--- /dev/null
+++ b/certora/harnesses/ERC20PermitHarness.sol
@@ -0,0 +1,5 @@
+import "../munged/token/ERC20/extensions/draft-ERC20Permit.sol";
+
+contract ERC20PermitHarness is ERC20Permit {
+}
+
diff --git a/certora/harnesses/ERC20WrapperHarness.sol b/certora/harnesses/ERC20WrapperHarness.sol
new file mode 100644
index 000000000..57a6c07be
--- /dev/null
+++ b/certora/harnesses/ERC20WrapperHarness.sol
@@ -0,0 +1,9 @@
+import "../munged/token/ERC20/extensions/ERC20Wrapper.sol";
+
+contract ERC20WrapperHarness is ERC20Wrapper {
+
+    constructor(IERC20 underlyingToken, string memory _name, string memory _symbol)
+        ERC20Wrapper(underlyingToken)
+    {}
+}
+
diff --git a/certora/scripts/sanityTokens.sh b/certora/scripts/sanityTokens.sh
new file mode 100755
index 000000000..10254c843
--- /dev/null
+++ b/certora/scripts/sanityTokens.sh
@@ -0,0 +1,17 @@
+#!/bin/bash
+
+make -C certora munged
+
+for f in certora/harnesses/{ERC20Votes,ERC20Wrapper,ERC20Permit}Harness.sol
+do
+    echo "Processing $f"
+    file=$(basename $f)
+    echo ${file%.*}
+    certoraRun certora/harnesses/$file \
+        --verify ${file%.*}:certora/specs/sanity.spec "$@" \
+        --solc solc8.2 --staging \
+        --optimistic_loop \
+        --msg "checking sanity on ${file%.*}" \
+        --settings -copyLoopUnroll=4 \
+        --send_only
+done