Skip to content

[certora] try fix loss factor #1027

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
lilCertora wants to merge 15 commits into from
+38 −19
Closed

[certora] try fix loss factor #1027

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
6b0cf92
try fix loss factor
lilCertora Jun 24, 2026
a90fdf8
Update LossFactor.conf
lilCertora Jun 24, 2026
68340ef
Merge branch 'main' into certora/fixLossFactor
lilCertora Jun 24, 2026
71075ed
linter
lilCertora Jun 24, 2026
454ca8d
linter
lilCertora Jun 24, 2026
392af59
try fix role
lilCertora Jun 24, 2026
682e4e5
Merge branch 'main' into certora/fixLossFactor
lilCertora Jun 24, 2026
16ea633
takeAMountsLibInvertibility fix
lilCertora Jun 24, 2026
dec6c2b
linter
lilCertora Jun 24, 2026
9742b8b
lossFactor fix
lilCertora Jun 24, 2026
52d36f5
try fix splitdoesnot
lilCertora Jun 25, 2026
12d4f24
try reentrancy fix
lilCertora Jun 25, 2026
ee82cd1
Update LossFactor.conf
lilCertora Jun 25, 2026
debc7d6
Merge branch 'main' into certora/fixLossFactor
lilCertora Jun 25, 2026
ac5f7f5
try fix splitDoesNot..
lilCertora Jun 25, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 6 additions & 3 deletions certora/confs/LossFactor.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,18 +7,21 @@
"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,
"prover_args": [
"-splitParallel true",
"-destructiveOptimizations twostage",
"-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"
"liquidateLossFactorDoesNotRevert",
"onlyLiquidateChangesMarketLossFactor"
],
"msg": "Loss Factor"
}
16 changes: 14 additions & 2 deletions certora/confs/Reentrancy.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
8 changes: 5 additions & 3 deletions certora/confs/Role.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
}
12 changes: 5 additions & 7 deletions certora/confs/SplitDoesNotPunishMakerOrFavorTaker.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,15 +11,13 @@
"loop_iter": 2,
"optimistic_hashing": true,
"hashing_length_bound": 1024,
"smt_timeout": 7200,
"smt_timeout": 1800,
"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"
],
"msg": "Split Does Not Punish Maker Or Favor Taker"
}
12 changes: 8 additions & 4 deletions certora/confs/TakeAmountsLibInvertibility.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,10 +13,14 @@
"optimistic_loop": true,
"loop_iter": 2,
"prover_args": [
"-destructiveOptimizations twostage",
"-splitParallel true",
"-splitParallelInitialDepth 4",
"-splitParallelTimelimit 7200"
"-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"
}
Loading