From 6b0cf92155ad6ff82b8986ad86ec530a4ebcd9d7 Mon Sep 17 00:00:00 2001 From: lilCertora Date: Wed, 24 Jun 2026 18:47:02 +0200 Subject: [PATCH 01/12] try fix loss factor --- certora/confs/LossFactor.conf | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/certora/confs/LossFactor.conf b/certora/confs/LossFactor.conf index dd3277bc2..24b3ca6f6 100644 --- a/certora/confs/LossFactor.conf +++ b/certora/confs/LossFactor.conf @@ -13,12 +13,16 @@ "hashing_length_bound": 2048, "smt_timeout": 7200, "prover_args": [ - "-splitParallel true", - "-destructiveOptimizations twostage", + "-destructiveOptimizations twostage", + "-backendStrategy singleRace", + "-smt_useLIA false", + "-smt_useNIA true", + "-depth 0", "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" - ], + ], "split_rules": [ - "liquidateLossFactorDoesNotRevert" + "liquidateLossFactorDoesNotRevert", + "onlyLiquidateChangesMarketLossFactor" ], - "msg": "Loss Factor" + "msg": "Loss Factor 2222" } From a90fdf8961b9a42f916c6c4e37e1fe96e08e93b9 Mon Sep 17 00:00:00 2001 From: lilCertora Date: Wed, 24 Jun 2026 18:47:41 +0200 Subject: [PATCH 02/12] Update LossFactor.conf Signed-off-by: lilCertora --- certora/confs/LossFactor.conf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/confs/LossFactor.conf b/certora/confs/LossFactor.conf index 24b3ca6f6..0fcaea08d 100644 --- a/certora/confs/LossFactor.conf +++ b/certora/confs/LossFactor.conf @@ -24,5 +24,5 @@ "liquidateLossFactorDoesNotRevert", "onlyLiquidateChangesMarketLossFactor" ], - "msg": "Loss Factor 2222" + "msg": "Loss Factor" } From 71075ed4ee8abd488429f09887804b8876d574e5 Mon Sep 17 00:00:00 2001 From: lilCertora Date: Wed, 24 Jun 2026 18:51:15 +0200 Subject: [PATCH 03/12] linter --- certora/confs/LossFactor.conf | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/confs/LossFactor.conf b/certora/confs/LossFactor.conf index 0fcaea08d..d9c55f5b8 100644 --- a/certora/confs/LossFactor.conf +++ b/certora/confs/LossFactor.conf @@ -13,13 +13,13 @@ "hashing_length_bound": 2048, "smt_timeout": 7200, "prover_args": [ - "-destructiveOptimizations twostage", + "-destructiveOptimizations twostage", "-backendStrategy singleRace", "-smt_useLIA false", "-smt_useNIA true", "-depth 0", "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" - ], + ], "split_rules": [ "liquidateLossFactorDoesNotRevert", "onlyLiquidateChangesMarketLossFactor" From 454ca8d443bf97398a722adf260fb56ac8639939 Mon Sep 17 00:00:00 2001 From: lilCertora Date: Wed, 24 Jun 2026 18:53:46 +0200 Subject: [PATCH 04/12] linter --- certora/confs/LossFactor.conf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/confs/LossFactor.conf b/certora/confs/LossFactor.conf index d9c55f5b8..2dde27dd2 100644 --- a/certora/confs/LossFactor.conf +++ b/certora/confs/LossFactor.conf @@ -7,8 +7,8 @@ "solc": "solc-0.8.34", "solc_via_ir": true, "solc_evm_version": "osaka", - "optimistic_loop": true, "loop_iter": 2, + "optimistic_loop": true, "optimistic_hashing": true, "hashing_length_bound": 2048, "smt_timeout": 7200, From 392af5981e1449268a96840c05eb6d1cc0b884bc Mon Sep 17 00:00:00 2001 From: lilCertora Date: Wed, 24 Jun 2026 22:27:50 +0200 Subject: [PATCH 05/12] try fix role --- certora/confs/Role.conf | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/certora/confs/Role.conf b/certora/confs/Role.conf index af7014329..f9d175e6d 100644 --- a/certora/confs/Role.conf +++ b/certora/confs/Role.conf @@ -12,9 +12,11 @@ "optimistic_hashing": true, "hashing_length_bound": 2048, "prover_args": [ - "-s", - "[z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5}]", - "-splitParallel true" + "-destructiveOptimizations twostage", + "-mediumTimeout 20", + "-lowTimeout 20", + "-tinyTimeout 20", + "-depth 20" ], "msg": "Role Safety and Liveness" } From 16ea633f73798c70867776de642ad5c2ebbad712 Mon Sep 17 00:00:00 2001 From: lilCertora Date: Wed, 24 Jun 2026 22:35:32 +0200 Subject: [PATCH 06/12] takeAMountsLibInvertibility fix --- certora/confs/TakeAmountsLibInvertibility.conf | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/certora/confs/TakeAmountsLibInvertibility.conf b/certora/confs/TakeAmountsLibInvertibility.conf index 15507fa19..7512fdced 100644 --- a/certora/confs/TakeAmountsLibInvertibility.conf +++ b/certora/confs/TakeAmountsLibInvertibility.conf @@ -13,9 +13,14 @@ "optimistic_loop": true, "loop_iter": 2, "prover_args": [ - "-depth 5", - "-mediumTimeout 60", - "-timeout 3600" - ], + "-destructiveOptimizations", + "twostage", + "-s", + "[z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]", + "-splitParallel", + "true", + "-dontStopAtFirstSplitTimeout", + "true" + ], "msg": "Midnight TakeAmountsLib Invertibility" } From dec6c2bcc939ec848c3bed7d3f83695fd947e697 Mon Sep 17 00:00:00 2001 From: lilCertora Date: Wed, 24 Jun 2026 22:43:00 +0200 Subject: [PATCH 07/12] linter --- certora/confs/TakeAmountsLibInvertibility.conf | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/certora/confs/TakeAmountsLibInvertibility.conf b/certora/confs/TakeAmountsLibInvertibility.conf index 7512fdced..22e359e3c 100644 --- a/certora/confs/TakeAmountsLibInvertibility.conf +++ b/certora/confs/TakeAmountsLibInvertibility.conf @@ -13,14 +13,14 @@ "optimistic_loop": true, "loop_iter": 2, "prover_args": [ - "-destructiveOptimizations", - "twostage", - "-s", - "[z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]", - "-splitParallel", - "true", - "-dontStopAtFirstSplitTimeout", - "true" - ], + "-destructiveOptimizations", + "twostage", + "-s", + "[z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]", + "-splitParallel", + "true", + "-dontStopAtFirstSplitTimeout", + "true" + ], "msg": "Midnight TakeAmountsLib Invertibility" } From 9742b8bd87a5c302f1dde580a64a7f54de7b7feb Mon Sep 17 00:00:00 2001 From: lilCertora Date: Wed, 24 Jun 2026 22:56:33 +0200 Subject: [PATCH 08/12] lossFactor fix --- certora/confs/LossFactor.conf | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/certora/confs/LossFactor.conf b/certora/confs/LossFactor.conf index 2dde27dd2..55bae0f09 100644 --- a/certora/confs/LossFactor.conf +++ b/certora/confs/LossFactor.conf @@ -14,15 +14,14 @@ "smt_timeout": 7200, "prover_args": [ "-destructiveOptimizations twostage", - "-backendStrategy singleRace", - "-smt_useLIA false", - "-smt_useNIA true", - "-depth 0", + "-smt_initialSplitDepth 4", + "-depth 10", + "-mediumTimeout 2", "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" ], "split_rules": [ "liquidateLossFactorDoesNotRevert", "onlyLiquidateChangesMarketLossFactor" ], - "msg": "Loss Factor" + "msg": "Loss Factor RECHECK 3" } From 52d36f583c8b9811cf3144847098d90e602fd7b2 Mon Sep 17 00:00:00 2001 From: lilCertora Date: Thu, 25 Jun 2026 09:35:14 +0200 Subject: [PATCH 09/12] try fix splitdoesnot --- .../confs/SplitDoesNotPunishMakerOrFavorTaker.conf | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/certora/confs/SplitDoesNotPunishMakerOrFavorTaker.conf b/certora/confs/SplitDoesNotPunishMakerOrFavorTaker.conf index 2a3b952b4..56ffebc89 100644 --- a/certora/confs/SplitDoesNotPunishMakerOrFavorTaker.conf +++ b/certora/confs/SplitDoesNotPunishMakerOrFavorTaker.conf @@ -13,13 +13,12 @@ "hashing_length_bound": 1024, "smt_timeout": 7200, "prover_args": [ - "-depth 10", - "-mediumTimeout 60", - "-splitParallel true", - "-smt_initialSplitDepth 2", "-destructiveOptimizations twostage", - "-s", - "[z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},cvc5:def,bitwuzla:def]" + "-backendStrategy singleRace", + "-smt_useLIA false", + "-smt_useNIA true", + "-depth 0", + "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" ], "msg": "Split Does Not Punish Maker Or Favor Taker" } From 12d4f24c1945b215622d11268088c11648173308 Mon Sep 17 00:00:00 2001 From: lilCertora Date: Thu, 25 Jun 2026 10:05:17 +0200 Subject: [PATCH 10/12] try reentrancy fix --- certora/confs/Reentrancy.conf | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf index 1940cfb8d..2a8ce9aa1 100644 --- a/certora/confs/Reentrancy.conf +++ b/certora/confs/Reentrancy.conf @@ -3,8 +3,20 @@ "src/Midnight.sol" ], "prover_args": [ - "-enableStorageSplitting false", - "-destructiveOptimizations twostage" + "-enableStorageSplitting", + "false", + "-destructiveOptimizations", + "twostage", + "-oldSplitParallel", + "true", + "-dontStopAtFirstSplitTimeout", + "true", + "-splitParallelTimelimit", + "7000", + "-splitParallelInitialDepth", + "3", + "-numOfParallelSplits", + "7" ], "solc": "solc-0.8.34", "solc_via_ir": true, From ee82cd18f228299443b1f0df5fbaf7941fb97f63 Mon Sep 17 00:00:00 2001 From: lilCertora Date: Thu, 25 Jun 2026 10:28:29 +0200 Subject: [PATCH 11/12] Update LossFactor.conf Signed-off-by: lilCertora --- certora/confs/LossFactor.conf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/confs/LossFactor.conf b/certora/confs/LossFactor.conf index 55bae0f09..07d3d1932 100644 --- a/certora/confs/LossFactor.conf +++ b/certora/confs/LossFactor.conf @@ -23,5 +23,5 @@ "liquidateLossFactorDoesNotRevert", "onlyLiquidateChangesMarketLossFactor" ], - "msg": "Loss Factor RECHECK 3" + "msg": "Loss Factor" } From ac5f7f518c685274410de736ba87d8ed0e827dbe Mon Sep 17 00:00:00 2001 From: lilCertora Date: Thu, 25 Jun 2026 16:55:20 +0200 Subject: [PATCH 12/12] try fix splitDoesNot.. --- certora/confs/SplitDoesNotPunishMakerOrFavorTaker.conf | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/certora/confs/SplitDoesNotPunishMakerOrFavorTaker.conf b/certora/confs/SplitDoesNotPunishMakerOrFavorTaker.conf index 56ffebc89..c72bb0330 100644 --- a/certora/confs/SplitDoesNotPunishMakerOrFavorTaker.conf +++ b/certora/confs/SplitDoesNotPunishMakerOrFavorTaker.conf @@ -11,14 +11,13 @@ "loop_iter": 2, "optimistic_hashing": true, "hashing_length_bound": 1024, - "smt_timeout": 7200, + "smt_timeout": 1800, "prover_args": [ "-destructiveOptimizations twostage", "-backendStrategy singleRace", "-smt_useLIA false", "-smt_useNIA true", - "-depth 0", - "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" + "-depth 0" ], "msg": "Split Does Not Punish Maker Or Favor Taker" }