Skip to content

Commit d50e424

Browse files
MathisGDMathisGD
authored
Merge pull request #106 from morpho-org/test/abs-certora
Add Certora verification for `abs` and `safeAbs`
2 parents 540207b + 82669d7 commit d50e424

8 files changed

+103
-59
lines changed

‎certora/scripts/verifyAll.sh

+1
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22

33
set -euxo pipefail
44

5+
certora/scripts/verifyBitvectorMath.sh $@
56
certora/scripts/verifyCompoundMath.sh $@
67
certora/scripts/verifyMath.sh $@
78
certora/scripts/verifyPercentageMath.sh $@

‎certora/scripts/verifyBitvectorMath.sh

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
#!/bin/bash
2+
3+
certoraRun \
4+
test/mocks/MathMock.sol \
5+
--verify MathMock:certora/specs/bitvectorMath.spec \
6+
--settings -useBitVectorTheory \
7+
--msg "Math" \
8+
$@

‎certora/scripts/verifyMath.sh

-3
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,5 @@
33
certoraRun \
44
test/mocks/MathMock.sol \
55
--verify MathMock:certora/specs/math.spec \
6-
--settings -useBitVectorTheory \
76
--msg "Math" \
87
$@
9-
10-

‎certora/specs/bitvectorMath.spec

+34
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
methods {
2+
function min(uint256, uint256) external returns (uint256) envfree;
3+
function max(uint256, uint256) external returns (uint256) envfree;
4+
}
5+
6+
/// min ///
7+
8+
rule minSafety(uint256 a, uint256 b) {
9+
uint res = min(a, b);
10+
11+
assert a <= b => res == a;
12+
assert a > b => res == b;
13+
}
14+
15+
rule minLiveness(uint256 a, uint256 b) {
16+
min@withrevert(a, b);
17+
18+
assert lastReverted <=> false;
19+
}
20+
21+
/// max ///
22+
23+
rule maxSafety(uint256 a, uint256 b) {
24+
uint res = max(a, b);
25+
26+
assert a >= b => res == a;
27+
assert a < b => res == b;
28+
}
29+
30+
rule maxLiveness(uint256 a, uint256 b) {
31+
max@withrevert(a, b);
32+
33+
assert lastReverted <=> false;
34+
}

‎certora/specs/compoundMath.spec

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
methods {
2-
function mul(uint256, uint256) external returns (uint256) envfree;
3-
function div(uint256, uint256) external returns (uint256) envfree;
2+
function mul(uint256, uint256) external returns (uint256) envfree;
3+
function div(uint256, uint256) external returns (uint256) envfree;
44
}
55

6-
definition WAD() returns uint = 10^18;
6+
definition WAD() returns uint = 10^18;
77
definition UINT_LIMIT() returns mathint = 2 ^ 255 * 2;
88

99
/// mul ///

‎certora/specs/math.spec

+24-20
Original file line numberDiff line numberDiff line change
@@ -1,41 +1,45 @@
1-
21
methods {
3-
function min(uint256, uint256) external returns (uint256) envfree;
4-
function max(uint256, uint256) external returns (uint256) envfree;
5-
function zeroFloorSub(uint256, uint256) external returns (uint256) envfree;
6-
function divUp(uint256, uint256) external returns (uint256) envfree;
2+
function abs(int256) external returns (int256) envfree;
3+
function safeAbs(int256) external returns (int256) envfree;
4+
function zeroFloorSub(uint256, uint256) external returns (uint256) envfree;
5+
function divUp(uint256, uint256) external returns (uint256) envfree;
76
}
87

9-
/// min ///
8+
definition MIN_INT256() returns int256 = -2^255;
9+
definition MAX_INT256() returns int256 = 2^255 - 1;
10+
11+
/// abs ///
1012

11-
rule minSafety(uint256 a, uint256 b) {
12-
uint res = min(a, b);
13+
rule absSafety(int256 a) {
14+
int256 res = abs(a);
1315

14-
assert a <= b => res == a;
15-
assert a > b => res == b;
16+
assert a >= 0 => res == a;
17+
assert a < 0 && a > MIN_INT256() => to_mathint(res) == -a;
18+
assert a == MIN_INT256() => res == MAX_INT256();
1619
}
1720

18-
rule minLiveness(uint256 a, uint256 b) {
19-
min@withrevert(a, b);
21+
rule absLiveness(int256 a) {
22+
abs@withrevert(a);
2023

2124
assert lastReverted <=> false;
2225
}
2326

24-
/// max ///
27+
/// safeAbs ///
2528

26-
rule maxSafety(uint256 a, uint256 b) {
27-
uint res = max(a, b);
29+
rule safeAbsSafety(int256 a) {
30+
int256 res = safeAbs(a);
2831

29-
assert a >= b => res == a;
30-
assert a < b => res == b;
32+
assert a >= 0 => res == a;
33+
assert a < 0 => to_mathint(res) == -a;
3134
}
3235

33-
rule maxLiveness(uint256 a, uint256 b) {
34-
max@withrevert(a, b);
36+
rule safeAbsLiveness(int256 a) {
37+
safeAbs@withrevert(a);
3538

36-
assert lastReverted <=> false;
39+
assert lastReverted <=> a == MIN_INT256();
3740
}
3841

42+
3943
/// zeroFloorSub ///
4044

4145
rule zeroFloorSubSafety(uint256 a, uint256 b) {

‎certora/specs/percentageMath.spec

+12-12
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,16 @@
11
methods {
2-
function percentAdd(uint256, uint256) external returns (uint256) envfree;
3-
function percentSub(uint256, uint256) external returns (uint256) envfree;
4-
function percentMul(uint256, uint256) external returns (uint256) envfree;
5-
function percentMulDown(uint256, uint256) external returns (uint256) envfree;
6-
function percentMulUp(uint256, uint256) external returns (uint256) envfree;
7-
function percentDiv(uint256, uint256) external returns (uint256) envfree;
8-
function percentDivDown(uint256, uint256) external returns (uint256) envfree;
9-
function percentDivUp(uint256, uint256) external returns (uint256) envfree;
10-
function weightedAvg(uint256, uint256, uint256) external returns (uint256) envfree;
11-
}
12-
13-
definition PERCENTAGE_FACTOR() returns uint = 10^4;
2+
function percentAdd(uint256, uint256) external returns (uint256) envfree;
3+
function percentSub(uint256, uint256) external returns (uint256) envfree;
4+
function percentMul(uint256, uint256) external returns (uint256) envfree;
5+
function percentMulDown(uint256, uint256) external returns (uint256) envfree;
6+
function percentMulUp(uint256, uint256) external returns (uint256) envfree;
7+
function percentDiv(uint256, uint256) external returns (uint256) envfree;
8+
function percentDivDown(uint256, uint256) external returns (uint256) envfree;
9+
function percentDivUp(uint256, uint256) external returns (uint256) envfree;
10+
function weightedAvg(uint256, uint256, uint256) external returns (uint256) envfree;
11+
}
12+
13+
definition PERCENTAGE_FACTOR() returns uint = 10^4;
1414
definition UINT_LIMIT() returns mathint = 2 ^ 255 * 2;
1515

1616
/// percentAdd ///

‎certora/specs/wadRayMath.spec

+21-21
Original file line numberDiff line numberDiff line change
@@ -1,25 +1,25 @@
11
methods {
2-
function wadMul(uint256, uint256) external returns (uint256) envfree;
3-
function wadMulDown(uint256, uint256) external returns (uint256) envfree;
4-
function wadMulUp(uint256, uint256) external returns (uint256) envfree;
5-
function wadDiv(uint256, uint256) external returns (uint256) envfree;
6-
function wadDivDown(uint256, uint256) external returns (uint256) envfree;
7-
function wadDivUp(uint256, uint256) external returns (uint256) envfree;
8-
function rayMul(uint256, uint256) external returns (uint256) envfree;
9-
function rayMulDown(uint256, uint256) external returns (uint256) envfree;
10-
function rayMulUp(uint256, uint256) external returns (uint256) envfree;
11-
function rayDiv(uint256, uint256) external returns (uint256) envfree;
12-
function rayDivDown(uint256, uint256) external returns (uint256) envfree;
13-
function rayDivUp(uint256, uint256) external returns (uint256) envfree;
14-
function rayToWad(uint256) external returns (uint256) envfree;
15-
function wadToRay(uint256) external returns (uint256) envfree;
16-
function wadWeightedAvg(uint256, uint256, uint256) external returns (uint256) envfree;
17-
function rayWeightedAvg(uint256, uint256, uint256) external returns (uint256) envfree;
18-
}
19-
20-
definition WAD() returns uint = 10^18;
21-
definition RAY() returns uint = 10^27;
22-
definition WADTORAY() returns uint = 10^9;
2+
function wadMul(uint256, uint256) external returns (uint256) envfree;
3+
function wadMulDown(uint256, uint256) external returns (uint256) envfree;
4+
function wadMulUp(uint256, uint256) external returns (uint256) envfree;
5+
function wadDiv(uint256, uint256) external returns (uint256) envfree;
6+
function wadDivDown(uint256, uint256) external returns (uint256) envfree;
7+
function wadDivUp(uint256, uint256) external returns (uint256) envfree;
8+
function rayMul(uint256, uint256) external returns (uint256) envfree;
9+
function rayMulDown(uint256, uint256) external returns (uint256) envfree;
10+
function rayMulUp(uint256, uint256) external returns (uint256) envfree;
11+
function rayDiv(uint256, uint256) external returns (uint256) envfree;
12+
function rayDivDown(uint256, uint256) external returns (uint256) envfree;
13+
function rayDivUp(uint256, uint256) external returns (uint256) envfree;
14+
function rayToWad(uint256) external returns (uint256) envfree;
15+
function wadToRay(uint256) external returns (uint256) envfree;
16+
function wadWeightedAvg(uint256, uint256, uint256) external returns (uint256) envfree;
17+
function rayWeightedAvg(uint256, uint256, uint256) external returns (uint256) envfree;
18+
}
19+
20+
definition WAD() returns uint = 10^18;
21+
definition RAY() returns uint = 10^27;
22+
definition WADTORAY() returns uint = 10^9;
2323
definition UINT_LIMIT() returns mathint = 2 ^ 255 * 2;
2424

2525
/// wadMul ///

0 commit comments

Comments
 (0)