feat: enable via-IR

morpho-org · Sep 5, 2023 · bb19b22 · bb19b22
1 parent c98b4fb
commit bb19b22
Show file tree

Hide file tree

Showing 11 changed files with 22 additions and 0 deletions.
diff --git a/certora/scripts/verifyAccrueInterest.sh b/certora/scripts/verifyAccrueInterest.sh
@@ -8,5 +8,7 @@ certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/AccrueInterest.spec \
     --solc_allow_path src \
+    --solc_via_ir \
+    --solc_optimize 4294967295 \
     --msg "Morpho Blue Accrue Interest" \
     "$@"
diff --git a/certora/scripts/verifyConsistentState.sh b/certora/scripts/verifyConsistentState.sh
@@ -8,5 +8,7 @@ certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/ConsistentState.spec \
     --solc_allow_path src \
+    --solc_via_ir \
+    --solc_optimize 4294967295 \
     --msg "Morpho Blue Consistent State" \
     "$@"
diff --git a/certora/scripts/verifyExactMath.sh b/certora/scripts/verifyExactMath.sh
@@ -8,6 +8,8 @@ certoraRun \
     certora/harness/MorphoHarness.sol \
     src/mocks/OracleMock.sol \
     --verify MorphoHarness:certora/specs/ExactMath.spec \
+    --solc_via_ir \
+    --solc_optimize 4294967295 \
     --prover_args '-smt_hashingScheme plaininjectivity' \
     --msg "Morpho Blue Exact Math" \
     "$@"
diff --git a/certora/scripts/verifyExitLiquidity.sh b/certora/scripts/verifyExitLiquidity.sh
@@ -8,5 +8,7 @@ certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/ExitLiquidity.spec \
     --solc_allow_path src \
+    --solc_via_ir \
+    --solc_optimize 4294967295 \
     --msg "Morpho Blue Exit Liquidity" \
     "$@"
diff --git a/certora/scripts/verifyHealth.sh b/certora/scripts/verifyHealth.sh
@@ -8,6 +8,8 @@ certoraRun \
     certora/harness/MorphoHarness.sol \
     certora/munged/mocks/OracleMock.sol \
     --verify MorphoHarness:certora/specs/Health.spec \
+    --solc_via_ir \
+    --solc_optimize 4294967295 \
     --prover_args '-smt_hashingScheme plaininjectivity' \
     --msg "Morpho Blue Health Check" \
     "$@"
diff --git a/certora/scripts/verifyLibSummary.sh b/certora/scripts/verifyLibSummary.sh
@@ -7,5 +7,7 @@ make -C certora munged
 certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/LibSummary.spec \
+    --solc_via_ir \
+    --solc_optimize 4294967295 \
     --msg "Morpho Blue Lib Summary" \
     "$@"
diff --git a/certora/scripts/verifyLiveness.sh b/certora/scripts/verifyLiveness.sh
@@ -8,5 +8,7 @@ certoraRun \
     certora/harness/MorphoInternalAccess.sol \
     --verify MorphoInternalAccess:certora/specs/Liveness.spec \
     --solc_allow_path src \
+    --solc_via_ir \
+    --solc_optimize 4294967295 \
     --msg "Morpho Blue Liveness" \
     "$@"
diff --git a/certora/scripts/verifyRatioMath.sh b/certora/scripts/verifyRatioMath.sh
@@ -8,6 +8,8 @@ certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/RatioMath.spec \
     --solc_allow_path src \
+    --solc_via_ir \
+    --solc_optimize 4294967295 \
     --prover_args '-smt_hashingScheme plaininjectivity' \
     --msg "Morpho Blue Ratio Math" \
     "$@"
diff --git a/certora/scripts/verifyReentrancy.sh b/certora/scripts/verifyReentrancy.sh
@@ -7,6 +7,8 @@ make -C certora munged
 certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/Reentrancy.spec \
+    --solc_via_ir \
+    --solc_optimize 4294967295 \
     --prover_args '-enableStorageSplitting false' \
     --msg "Morpho Blue Reentrancy" \
     "$@"
diff --git a/certora/scripts/verifyReverts.sh b/certora/scripts/verifyReverts.sh
@@ -7,5 +7,7 @@ make -C certora munged
 certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/Reverts.spec \
+    --solc_via_ir \
+    --solc_optimize 4294967295 \
     --msg "Morpho Blue Reverts" \
     "$@"
diff --git a/certora/scripts/verifyTransfer.sh b/certora/scripts/verifyTransfer.sh
@@ -10,5 +10,7 @@ certoraRun \
     certora/dispatch/ERC20USDT.sol \
     certora/dispatch/ERC20NoRevert.sol \
     --verify TransferHarness:certora/specs/Transfer.spec \
+    --solc_via_ir \
+    --solc_optimize 4294967295 \
     --msg "Morpho Blue Transfer" \
     "$@"