From e5920be891c877986732e9cf0a2e609468cab5c6 Mon Sep 17 00:00:00 2001
From: sunbreak1211 <sunbreak1211@proton.me>
Date: Tue, 19 Mar 2024 10:45:00 -0300
Subject: [PATCH] Fix Certora Specs

---
 Makefile            |  3 ++-
 certora/D3MHub.conf | 60 +++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 62 insertions(+), 1 deletion(-)
 create mode 100644 certora/D3MHub.conf

diff --git a/Makefile b/Makefile
index 532060d4..8287c606 100644
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,6 @@
+PATH := ~/.solc-select/artifacts/solc-0.8.14:~/.solc-select/artifacts/solc-0.5.12:$(PATH)
 all         :; FOUNDRY_OPTIMIZER=true FOUNDRY_OPTIMIZER_RUNS=200 forge build --use solc:0.8.14
 clean       :; forge clean
-certora-hub :; PATH=~/.solc-select/artifacts/solc-0.8.14:~/.solc-select/artifacts/solc-0.5.12:~/.solc-select/artifacts:${PATH} certoraRun --solc_map D3MHub=solc-0.8.14,Vat=solc-0.5.12,DaiJoin=solc-0.5.12,Dai=solc-0.5.12,End=solc-0.5.12,D3MTestPlan=solc-0.8.14,D3MTestPool=solc-0.8.14,TokenMock=solc-0.8.14 --optimize_map D3MHub=200,Vat=0,DaiJoin=0,Dai=0,End=0,D3MTestPlan=200,D3MTestPool=200,TokenMock=200 --rule_sanity basic src/D3MHub.sol certora/dss/Vat.sol certora/dss/DaiJoin.sol certora/dss/Dai.sol certora/dss/End.sol certora/d3m/D3MTestPlan.sol certora/d3m/D3MTestPool.sol src/tests/mocks/TokenMock.sol --link D3MHub:vat=Vat D3MHub:daiJoin=DaiJoin D3MHub:end=End DaiJoin:vat=Vat DaiJoin:dai=Dai End:vat=Vat D3MTestPlan:dai=Dai D3MTestPool:hub=D3MHub D3MTestPool:vat=Vat D3MTestPool:dai=Dai D3MTestPool:share=TokenMock --structLink D3MHub:pool=D3MTestPool D3MHub:plan=D3MTestPlan --verify D3MHub:certora/D3MHub.spec --settings -mediumTimeout=1200,-solver=z3,-adaptiveSolverConfig=false,-smt_nonLinearArithmetic=true$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)$(if $(multi), --multi_assert_check,)
+certora-hub :; PATH=${PATH} certoraRun certora/D3MHub.conf$(if $(rule), --rule $(rule),)
 deploy      :; ./deploy.sh config="$(config)"
 deploy-core :; ./deploy-core.sh
diff --git a/certora/D3MHub.conf b/certora/D3MHub.conf
new file mode 100644
index 00000000..a5b4554b
--- /dev/null
+++ b/certora/D3MHub.conf
@@ -0,0 +1,60 @@
+{
+    "files": [
+        "src/D3MHub.sol",
+        "certora/dss/Vat.sol",
+        "certora/dss/DaiJoin.sol",
+        "certora/dss/Dai.sol",
+        "certora/dss/End.sol",
+        "certora/d3m/D3MTestPlan.sol",
+        "certora/d3m/D3MTestPool.sol",
+        "src/tests/mocks/TokenMock.sol"
+    ],
+    "link": [
+        "D3MHub:vat=Vat",
+        "D3MHub:daiJoin=DaiJoin",
+        "D3MHub:end=End",
+        "DaiJoin:vat=Vat",
+        "DaiJoin:dai=Dai",
+        "End:vat=Vat",
+        "D3MTestPlan:dai=Dai",
+        "D3MTestPool:hub=D3MHub",
+        "D3MTestPool:vat=Vat",
+        "D3MTestPool:dai=Dai",
+        "D3MTestPool:share=TokenMock"
+    ],
+    "struct_link": [
+        "D3MHub:pool=D3MTestPool",
+        "D3MHub:plan=D3MTestPlan"
+    ],
+    "rule_sanity": "basic",
+    "solc_map": {
+        "D3MHub": "solc-0.8.14",
+        "Vat": "solc-0.5.12",
+        "DaiJoin": "solc-0.5.12",
+        "Dai": "solc-0.5.12",
+        "End": "solc-0.5.12",
+        "D3MTestPlan": "solc-0.8.14",
+        "D3MTestPool": "solc-0.8.14",
+        "TokenMock": "solc-0.8.14"
+    },
+    "solc_optimize_map": {
+        "D3MHub": "200",
+        "Vat": "0",
+        "DaiJoin": "0",
+        "Dai": "0",
+        "End": "0",
+        "D3MTestPlan": "200",
+        "D3MTestPool": "200",
+        "TokenMock": "200"
+    },
+    "verify": "D3MHub:certora/D3MHub.spec",
+    "prover_args": [
+        "-mediumTimeout 1200",
+        "-solver z3",
+        "-adaptiveSolverConfig false",
+        "-smt_nonLinearArithmetic true",
+        "-enableSolidityBasedInlining true"
+    ],
+    "multi_assert_check": true,
+    "wait_for_results": "all"
+}