feat: enable via-IR

QGarchery · QGarchery · commit 7d2dcb8fba1d · 2023-10-19T10:56:00.000+02:00
diff --git a/certora/configuration/AccrueInterest.conf b/certora/configuration/AccrueInterest.conf
@@ -3,6 +3,8 @@
         "certora/harness/MorphoHarness.sol"
     ],
     "verify": "MorphoHarness:certora/specs/AccrueInterest.spec",
+    "solc_via_ir": true,
+    "solc_optimize": "4294967295",
     "prover_args": [
         "-smt_hashingScheme plaininjectivity",
         "-mediumTimeout 30"
diff --git a/certora/configuration/ConsistentState.conf b/certora/configuration/ConsistentState.conf
@@ -3,5 +3,7 @@
         "certora/harness/MorphoHarness.sol"
     ],
     "verify": "MorphoHarness:certora/specs/ConsistentState.spec",
+    "solc_via_ir": true,
+    "solc_optimize": "4294967295",
     "msg": "Morpho Blue Consistent State"
 }
diff --git a/certora/configuration/ExactMath.conf b/certora/configuration/ExactMath.conf
@@ -3,6 +3,8 @@
         "certora/harness/MorphoHarness.sol"
     ],
     "verify": "MorphoHarness:certora/specs/ExactMath.spec",
+    "solc_via_ir": true,
+    "solc_optimize": "4294967295",
     "prover_args": [
         "-smt_hashingScheme plaininjectivity",
         "-mediumTimeout 30"
diff --git a/certora/configuration/ExitLiquidity.conf b/certora/configuration/ExitLiquidity.conf
@@ -3,5 +3,7 @@
         "certora/harness/MorphoHarness.sol"
     ],
     "verify": "MorphoHarness:certora/specs/ExitLiquidity.spec",
+    "solc_via_ir": true,
+    "solc_optimize": "4294967295",
     "msg": "Morpho Blue Exit Liquidity"
 }
diff --git a/certora/configuration/Health.conf b/certora/configuration/Health.conf
@@ -4,6 +4,8 @@
         "src/mocks/OracleMock.sol"
     ],
     "verify": "MorphoHarness:certora/specs/Health.spec",
+    "solc_via_ir": true,
+    "solc_optimize": "4294967295",
     "prover_args": [
         "-smt_hashingScheme plaininjectivity"
     ],
diff --git a/certora/configuration/LibSummary.conf b/certora/configuration/LibSummary.conf
@@ -3,5 +3,7 @@
         "certora/harness/MorphoHarness.sol"
     ],
     "verify": "MorphoHarness:certora/specs/LibSummary.spec",
+    "solc_via_ir": true,
+    "solc_optimize": "4294967295",
     "msg": "Morpho Blue Lib Summary"
 }
diff --git a/certora/configuration/Liveness.conf b/certora/configuration/Liveness.conf
@@ -3,5 +3,7 @@
         "certora/harness/MorphoInternalAccess.sol"
     ],
     "verify": "MorphoInternalAccess:certora/specs/Liveness.spec",
+    "solc_via_ir": true,
+    "solc_optimize": "4294967295",
     "msg": "Morpho Blue Liveness"
 }
diff --git a/certora/configuration/RatioMath.conf b/certora/configuration/RatioMath.conf
@@ -3,6 +3,8 @@
         "certora/harness/MorphoHarness.sol"
     ],
     "verify": "MorphoHarness:certora/specs/RatioMath.spec",
+    "solc_via_ir": true,
+    "solc_optimize": "4294967295",
     "prover_args": [
         "-smt_hashingScheme plaininjectivity"
     ],
diff --git a/certora/configuration/Reentrancy.conf b/certora/configuration/Reentrancy.conf
@@ -3,6 +3,8 @@
         "certora/harness/MorphoHarness.sol"
     ],
     "verify": "MorphoHarness:certora/specs/Reentrancy.spec",
+    "solc_via_ir": true,
+    "solc_optimize": "4294967295",
     "prover_args": [
         "-enableStorageSplitting false"
     ],
diff --git a/certora/configuration/Reverts.conf b/certora/configuration/Reverts.conf
@@ -3,5 +3,7 @@
         "certora/harness/MorphoHarness.sol"
     ],
     "verify": "MorphoHarness:certora/specs/Reverts.spec",
+    "solc_via_ir": true,
+    "solc_optimize": "4294967295",
     "msg": "Morpho Blue Reverts"
 }
diff --git a/certora/configuration/Transfer.conf b/certora/configuration/Transfer.conf
@@ -6,5 +6,7 @@
         "certora/dispatch/ERC20NoRevert.sol"
     ],
     "verify": "TransferHarness:certora/specs/Transfer.spec",
+    "solc_via_ir": true,
+    "solc_optimize": "4294967295",
     "msg": "Morpho Blue Transfer"
 }

Original file line number	Diff line number	Diff line change
`@@ -3,5 +3,7 @@`
`3`	`3`	`"certora/harness/MorphoHarness.sol"`
`4`	`4`	`],`
`5`	`5`	`"verify": "MorphoHarness:certora/specs/ConsistentState.spec",`
	`6`	`+ "solc_via_ir": true,`
	`7`	`+ "solc_optimize": "4294967295",`
`6`	`8`	`"msg": "Morpho Blue Consistent State"`
`7`	`9`	`}`
Original file line number	Diff line number	Diff line change
`@@ -3,5 +3,7 @@`
`3`	`3`	`"certora/harness/MorphoInternalAccess.sol"`
`4`	`4`	`],`
`5`	`5`	`"verify": "MorphoInternalAccess:certora/specs/Liveness.spec",`
	`6`	`+ "solc_via_ir": true,`
	`7`	`+ "solc_optimize": "4294967295",`
`6`	`8`	`"msg": "Morpho Blue Liveness"`
`7`	`9`	`}`
Original file line number	Diff line number	Diff line change
`@@ -6,5 +6,7 @@`
`6`	`6`	`"certora/dispatch/ERC20NoRevert.sol"`
`7`	`7`	`],`
`8`	`8`	`"verify": "TransferHarness:certora/specs/Transfer.spec",`
	`9`	`+ "solc_via_ir": true,`
	`10`	`+ "solc_optimize": "4294967295",`
`9`	`11`	`"msg": "Morpho Blue Transfer"`
`10`	`12`	`}`