Skip to content

Commit 7e9b0f7

Browse files
committed
feat: enable via-IR
1 parent c98b4fb commit 7e9b0f7

10 files changed

+20
-0
lines changed

certora/scripts/verifyAccrueInterest.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,5 +8,7 @@ certoraRun \
88
certora/harness/MorphoHarness.sol \
99
--verify MorphoHarness:certora/specs/AccrueInterest.spec \
1010
--solc_allow_path src \
11+
--solc_via_ir \
12+
--solc_optimize 4294967295 \
1113
--msg "Morpho Blue Accrue Interest" \
1214
"$@"

certora/scripts/verifyConsistentState.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,5 +8,7 @@ certoraRun \
88
certora/harness/MorphoHarness.sol \
99
--verify MorphoHarness:certora/specs/ConsistentState.spec \
1010
--solc_allow_path src \
11+
--solc_via_ir \
12+
--solc_optimize 4294967295 \
1113
--msg "Morpho Blue Consistent State" \
1214
"$@"

certora/scripts/verifyExactMath.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,8 @@ certoraRun \
88
certora/harness/MorphoHarness.sol \
99
src/mocks/OracleMock.sol \
1010
--verify MorphoHarness:certora/specs/ExactMath.spec \
11+
--solc_via_ir \
12+
--solc_optimize 4294967295 \
1113
--prover_args '-smt_hashingScheme plaininjectivity' \
1214
--msg "Morpho Blue Exact Math" \
1315
"$@"

certora/scripts/verifyExitLiquidity.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,5 +8,7 @@ certoraRun \
88
certora/harness/MorphoHarness.sol \
99
--verify MorphoHarness:certora/specs/ExitLiquidity.spec \
1010
--solc_allow_path src \
11+
--solc_via_ir \
12+
--solc_optimize 4294967295 \
1113
--msg "Morpho Blue Exit Liquidity" \
1214
"$@"

certora/scripts/verifyHealth.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,8 @@ certoraRun \
88
certora/harness/MorphoHarness.sol \
99
certora/munged/mocks/OracleMock.sol \
1010
--verify MorphoHarness:certora/specs/Health.spec \
11+
--solc_via_ir \
12+
--solc_optimize 4294967295 \
1113
--prover_args '-smt_hashingScheme plaininjectivity' \
1214
--msg "Morpho Blue Health Check" \
1315
"$@"

certora/scripts/verifyLiveness.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,5 +8,7 @@ certoraRun \
88
certora/harness/MorphoInternalAccess.sol \
99
--verify MorphoInternalAccess:certora/specs/Liveness.spec \
1010
--solc_allow_path src \
11+
--solc_via_ir \
12+
--solc_optimize 4294967295 \
1113
--msg "Morpho Blue Liveness" \
1214
"$@"

certora/scripts/verifyRatioMath.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,8 @@ certoraRun \
88
certora/harness/MorphoHarness.sol \
99
--verify MorphoHarness:certora/specs/RatioMath.spec \
1010
--solc_allow_path src \
11+
--solc_via_ir \
12+
--solc_optimize 4294967295 \
1113
--prover_args '-smt_hashingScheme plaininjectivity' \
1214
--msg "Morpho Blue Ratio Math" \
1315
"$@"

certora/scripts/verifyReentrancy.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,8 @@ make -C certora munged
77
certoraRun \
88
certora/harness/MorphoHarness.sol \
99
--verify MorphoHarness:certora/specs/Reentrancy.spec \
10+
--solc_via_ir \
11+
--solc_optimize 4294967295 \
1012
--prover_args '-enableStorageSplitting false' \
1113
--msg "Morpho Blue Reentrancy" \
1214
"$@"

certora/scripts/verifyReverts.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,5 +7,7 @@ make -C certora munged
77
certoraRun \
88
certora/harness/MorphoHarness.sol \
99
--verify MorphoHarness:certora/specs/Reverts.spec \
10+
--solc_via_ir \
11+
--solc_optimize 4294967295 \
1012
--msg "Morpho Blue Reverts" \
1113
"$@"

certora/scripts/verifyTransfer.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,5 +10,7 @@ certoraRun \
1010
certora/dispatch/ERC20USDT.sol \
1111
certora/dispatch/ERC20NoRevert.sol \
1212
--verify TransferHarness:certora/specs/Transfer.spec \
13+
--solc_via_ir \
14+
--solc_optimize 4294967295 \
1315
--msg "Morpho Blue Transfer" \
1416
"$@"

0 commit comments

Comments
 (0)