forked from crytic/properties
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathABDKMath64x64PropertyTests.sol
1851 lines (1488 loc) · 59.5 KB
/
ABDKMath64x64PropertyTests.sol
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
// SPDX-License-Identifier: AGPL-3.0-or-later
pragma solidity ^0.8.0;
import "./abdk-libraries-solidity/ABDKMath64x64.sol";
contract CryticABDKMath64x64Properties {
/* ================================================================
64x64 fixed-point constants used for testing specific values.
This assumes that ABDK library's fromInt(x) works as expected.
================================================================ */
int128 internal ZERO_FP = ABDKMath64x64.fromInt(0);
int128 internal ONE_FP = ABDKMath64x64.fromInt(1);
int128 internal MINUS_ONE_FP = ABDKMath64x64.fromInt(-1);
int128 internal TWO_FP = ABDKMath64x64.fromInt(2);
int128 internal THREE_FP = ABDKMath64x64.fromInt(3);
int128 internal EIGHT_FP = ABDKMath64x64.fromInt(8);
int128 internal THOUSAND_FP = ABDKMath64x64.fromInt(1000);
int128 internal MINUS_SIXTY_FOUR_FP = ABDKMath64x64.fromInt(-64);
int128 internal EPSILON = 1;
int128 internal ONE_TENTH_FP =
ABDKMath64x64.div(ABDKMath64x64.fromInt(1), ABDKMath64x64.fromInt(10));
/* ================================================================
Constants used for precision loss calculations
================================================================ */
uint256 internal REQUIRED_SIGNIFICANT_BITS = 10;
/* ================================================================
Integer representations maximum values.
These constants are used for testing edge cases or limits for
possible values.
================================================================ */
int128 private constant MIN_64x64 = -0x80000000000000000000000000000000;
int128 private constant MAX_64x64 = 0x7FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF;
int256 private constant MAX_256 =
0x7FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF;
int256 private constant MIN_256 =
-0x8000000000000000000000000000000000000000000000000000000000000000;
uint256 private constant MAX_U256 =
0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF;
/* ================================================================
Events used for debugging or showing information.
================================================================ */
event Value(string reason, int128 val);
event LogErr(bytes error);
/* ================================================================
Helper functions.
================================================================ */
// These functions allows to compare a and b for equality, discarding
// the last precision_bits bits.
// An absolute value function is implemented inline in order to not use
// the implementation from the library under test.
function equal_within_precision(
int128 a,
int128 b,
uint256 precision_bits
) public pure returns (bool) {
int128 max = (a > b) ? a : b;
int128 min = (a > b) ? b : a;
int128 r = (max - min) >> precision_bits;
return (r == 0);
}
function equal_within_precision_u(
uint256 a,
uint256 b,
uint256 precision_bits
) public pure returns (bool) {
uint256 max = (a > b) ? a : b;
uint256 min = (a > b) ? b : a;
uint256 r = (max - min) >> precision_bits;
return (r == 0);
}
// This function determines if the relative error between a and b is less
// than error_percent % (expressed as a 64x64 value)
// Uses functions from the library under test!
function equal_within_tolerance(
int128 a,
int128 b,
int128 error_percent
) public pure returns (bool) {
int128 tol_value = abs(mul(a, div(error_percent, fromUInt(100))));
return (abs(sub(b, a)) <= tol_value);
}
// Check that there are remaining significant digits after a multiplication
// Uses functions from the library under test!
function significant_digits_lost_in_mult(
int128 a,
int128 b
) public pure returns (bool) {
int128 x = a >= 0 ? a : -a;
int128 y = b >= 0 ? b : -b;
int128 lx = toInt(log_2(x));
int128 ly = toInt(log_2(y));
return (lx + ly - 1 <= -64);
}
// Return how many significant bits will remain after multiplying a and b
// Uses functions from the library under test!
function significant_bits_after_mult(
int128 a,
int128 b
) public pure returns (uint256) {
int128 x = a >= 0 ? a : -a;
int128 y = b >= 0 ? b : -b;
int128 lx = toInt(log_2(x));
int128 ly = toInt(log_2(y));
int256 prec = lx + ly - 1;
if (prec < -64) return 0;
else return (64 + uint256(prec));
}
// Return the i most significant bits from |n|. If n has less than i significant bits, return |n|
// Uses functions from the library under test!
function most_significant_bits(
int128 n,
uint256 i
) public pure returns (uint256) {
// Create a mask consisting of i bits set to 1
uint256 mask = (2 ** i) - 1;
// Get the position of the MSB set to 1 of n
uint256 pos = uint64(toInt(log_2(n)) + 64 + 1);
// Get the positive value of n
uint256 value = (n > 0) ? uint128(n) : uint128(-n);
// Shift the mask to match the rightmost 1-set bit
if (pos > i) {
mask <<= (pos - i);
}
return (value & mask);
}
// Returns true if the n most significant bits of a and b are almost equal
// Uses functions from the library under test!
function equal_most_significant_bits_within_precision(
int128 a,
int128 b,
uint256 bits
) public pure returns (bool) {
// Get the number of bits in a and b
// Since log(x) returns in the interval [-64, 63), add 64 to be in the interval [0, 127)
uint256 a_bits = uint256(int256(toInt(log_2(a)) + 64));
uint256 b_bits = uint256(int256(toInt(log_2(b)) + 64));
// a and b lengths may differ in 1 bit, so the shift should take into account the longest
uint256 shift_bits = (a_bits > b_bits)
? (a_bits - bits)
: (b_bits - bits);
// Get the _bits_ most significant bits of a and b
uint256 a_msb = most_significant_bits(a, bits) >> shift_bits;
uint256 b_msb = most_significant_bits(b, bits) >> shift_bits;
// See if they are equal within 1 bit precision
// This could be modified to get the precision as a parameter to the function
return equal_within_precision_u(a_msb, b_msb, 1);
}
/* ================================================================
Library wrappers.
These functions allow calling the ABDKMath64x64 library.
================================================================ */
function debug(string calldata x, int128 y) public {
emit Value(x, ABDKMath64x64.toInt(y));
}
function fromInt(int256 x) public pure returns (int128) {
return ABDKMath64x64.fromInt(x);
}
function toInt(int128 x) public pure returns (int64) {
return ABDKMath64x64.toInt(x);
}
function fromUInt(uint256 x) public pure returns (int128) {
return ABDKMath64x64.fromUInt(x);
}
function toUInt(int128 x) public pure returns (uint64) {
return ABDKMath64x64.toUInt(x);
}
function add(int128 x, int128 y) public pure returns (int128) {
return ABDKMath64x64.add(x, y);
}
function sub(int128 x, int128 y) public pure returns (int128) {
return ABDKMath64x64.sub(x, y);
}
function mul(int128 x, int128 y) public pure returns (int128) {
return ABDKMath64x64.mul(x, y);
}
function mulu(int128 x, uint256 y) public pure returns (uint256) {
return ABDKMath64x64.mulu(x, y);
}
function div(int128 x, int128 y) public pure returns (int128) {
return ABDKMath64x64.div(x, y);
}
function neg(int128 x) public pure returns (int128) {
return ABDKMath64x64.neg(x);
}
function abs(int128 x) public pure returns (int128) {
return ABDKMath64x64.abs(x);
}
function inv(int128 x) public pure returns (int128) {
return ABDKMath64x64.inv(x);
}
function avg(int128 x, int128 y) public pure returns (int128) {
return ABDKMath64x64.avg(x, y);
}
function gavg(int128 x, int128 y) public pure returns (int128) {
return ABDKMath64x64.gavg(x, y);
}
function pow(int128 x, uint256 y) public pure returns (int128) {
return ABDKMath64x64.pow(x, y);
}
function sqrt(int128 x) public pure returns (int128) {
return ABDKMath64x64.sqrt(x);
}
function log_2(int128 x) public pure returns (int128) {
return ABDKMath64x64.log_2(x);
}
function ln(int128 x) public pure returns (int128) {
return ABDKMath64x64.ln(x);
}
function exp_2(int128 x) public pure returns (int128) {
return ABDKMath64x64.exp_2(x);
}
function exp(int128 x) public pure returns (int128) {
return ABDKMath64x64.exp(x);
}
/* ================================================================
Start of tests
================================================================ */
/* ================================================================
TESTS FOR FUNCTION add()
================================================================ */
/* ================================================================
Tests for arithmetic properties.
These should make sure that the implemented function complies
with math rules and expected behaviour.
================================================================ */
// Test for commutative property
// x + y == y + x
function add_test_commutative(int128 x, int128 y) public pure {
int128 x_y = add(x, y);
int128 y_x = add(y, x);
assert(x_y == y_x);
}
// Test for associative property
// (x + y) + z == x + (y + z)
function add_test_associative(int128 x, int128 y, int128 z) public pure {
int128 x_y = add(x, y);
int128 y_z = add(y, z);
int128 xy_z = add(x_y, z);
int128 x_yz = add(x, y_z);
assert(xy_z == x_yz);
}
// Test for identity operation
// x + 0 == x (equivalent to x + (-x) == 0)
function add_test_identity(int128 x) public view {
int128 x_0 = add(x, ZERO_FP);
assert(x_0 == x);
assert(add(x, neg(x)) == ZERO_FP);
}
// Test that the result increases or decreases depending
// on the value to be added
function add_test_values(int128 x, int128 y) public view {
int128 x_y = add(x, y);
if (y >= ZERO_FP) {
assert(x_y >= x);
} else {
assert(x_y < x);
}
}
/* ================================================================
Tests for overflow and edge cases.
These should make sure that the function reverts on overflow and
behaves correctly on edge cases
================================================================ */
// The result of the addition must be between the maximum
// and minimum allowed values for 64x64
function add_test_range(int128 x, int128 y) public view {
int128 result;
try this.add(x, y) {
result = this.add(x, y);
assert(result <= MAX_64x64 && result >= MIN_64x64);
} catch {
// If it reverts, just ignore
}
}
// Adding zero to the maximum value shouldn't revert, as it is valid
// Moreover, the result must be MAX_64x64
function add_test_maximum_value() public view {
int128 result;
try this.add(MAX_64x64, ZERO_FP) {
// Expected behaviour, does not revert
result = this.add(MAX_64x64, ZERO_FP);
assert(result == MAX_64x64);
} catch {
assert(false);
}
}
// Adding one to the maximum value should revert, as it is out of range
function add_test_maximum_value_plus_one() public view {
try this.add(MAX_64x64, ONE_FP) {
assert(false);
} catch {
// Expected behaviour, reverts
}
}
// Adding zero to the minimum value shouldn't revert, as it is valid
// Moreover, the result must be MIN_64x64
function add_test_minimum_value() public view {
int128 result;
try this.add(MIN_64x64, ZERO_FP) {
// Expected behaviour, does not revert
result = this.add(MIN_64x64, ZERO_FP);
assert(result == MIN_64x64);
} catch {
assert(false);
}
}
// Adding minus one to the minimum value should revert, as it is out of range
function add_test_minimum_value_plus_negative_one() public view {
try this.add(MIN_64x64, MINUS_ONE_FP) {
assert(false);
} catch {
// Expected behaviour, reverts
}
}
/* ================================================================
TESTS FOR FUNCTION sub()
================================================================ */
/* ================================================================
Tests for arithmetic properties.
These should make sure that the implemented function complies
with math rules and expected behaviour.
================================================================ */
// Test equivalence to addition
// x - y == x + (-y)
function sub_test_equivalence_to_addition(int128 x, int128 y) public pure {
int128 minus_y = neg(y);
int128 addition = add(x, minus_y);
int128 subtraction = sub(x, y);
assert(addition == subtraction);
}
// Test for non-commutative property
// x - y == -(y - x)
function sub_test_non_commutative(int128 x, int128 y) public pure {
int128 x_y = sub(x, y);
int128 y_x = sub(y, x);
assert(x_y == neg(y_x));
}
// Test for identity operation
// x - 0 == x (equivalent to x - x == 0)
function sub_test_identity(int128 x) public view {
int128 x_0 = sub(x, ZERO_FP);
assert(x_0 == x);
assert(sub(x, x) == ZERO_FP);
}
// Test for neutrality over addition and subtraction
// (x - y) + y == (x + y) - y == x
function sub_test_neutrality(int128 x, int128 y) public pure {
int128 x_minus_y = sub(x, y);
int128 x_plus_y = add(x, y);
int128 x_minus_y_plus_y = add(x_minus_y, y);
int128 x_plus_y_minus_y = sub(x_plus_y, y);
assert(x_minus_y_plus_y == x_plus_y_minus_y);
assert(x_minus_y_plus_y == x);
}
// Test that the result increases or decreases depending
// on the value to be subtracted
function sub_test_values(int128 x, int128 y) public view {
int128 x_y = sub(x, y);
if (y >= ZERO_FP) {
assert(x_y <= x);
} else {
assert(x_y > x);
}
}
/* ================================================================
Tests for overflow and edge cases.
These will make sure that the function reverts on overflow and
behaves correctly on edge cases
================================================================ */
// The result of the subtraction must be between the maximum
// and minimum allowed values for 64x64
function sub_test_range(int128 x, int128 y) public view {
int128 result;
try this.sub(x, y) {
result = this.sub(x, y);
assert(result <= MAX_64x64 && result >= MIN_64x64);
} catch {
// If it reverts, just ignore
}
}
// Subtracting zero from the maximum value shouldn't revert, as it is valid
// Moreover, the result must be MAX_64x64
function sub_test_maximum_value() public view {
int128 result;
try this.sub(MAX_64x64, ZERO_FP) {
// Expected behaviour, does not revert
result = this.sub(MAX_64x64, ZERO_FP);
assert(result == MAX_64x64);
} catch {
assert(false);
}
}
// Subtracting minus one from the maximum value should revert,
// as it is out of range
function sub_test_maximum_value_minus_neg_one() public view {
try this.sub(MAX_64x64, MINUS_ONE_FP) {
assert(false);
} catch {
// Expected behaviour, reverts
}
}
// Subtracting zero from the minimum value shouldn't revert, as it is valid
// Moreover, the result must be MIN_64x64
function sub_test_minimum_value() public view {
int128 result;
try this.sub(MIN_64x64, ZERO_FP) {
// Expected behaviour, does not revert
result = this.sub(MIN_64x64, ZERO_FP);
assert(result == MIN_64x64);
} catch {
assert(false);
}
}
// Subtracting one from the minimum value should revert, as it is out of range
function sub_test_minimum_value_minus_one() public view {
try this.sub(MIN_64x64, ONE_FP) {
assert(false);
} catch {
// Expected behaviour, reverts
}
}
/* ================================================================
TESTS FOR FUNCTION mul()
================================================================ */
/* ================================================================
Tests for arithmetic properties.
These should make sure that the implemented function complies
with math rules and expected behaviour.
================================================================ */
// Test for commutative property
// x * y == y * x
function mul_test_commutative(int128 x, int128 y) public pure {
int128 x_y = mul(x, y);
int128 y_x = mul(y, x);
assert(x_y == y_x);
}
// Test for associative property
// (x * y) * z == x * (y * z)
function mul_test_associative(int128 x, int128 y, int128 z) public view {
int128 x_y = mul(x, y);
int128 y_z = mul(y, z);
int128 xy_z = mul(x_y, z);
int128 x_yz = mul(x, y_z);
// Failure if all significant digits are lost
require(significant_bits_after_mult(x, y) > REQUIRED_SIGNIFICANT_BITS);
require(significant_bits_after_mult(y, z) > REQUIRED_SIGNIFICANT_BITS);
require(
significant_bits_after_mult(x_y, z) > REQUIRED_SIGNIFICANT_BITS
);
require(
significant_bits_after_mult(x, y_z) > REQUIRED_SIGNIFICANT_BITS
);
assert(equal_within_tolerance(xy_z, x_yz, ONE_TENTH_FP));
}
// Test for distributive property
// x * (y + z) == x * y + x * z
function mul_test_distributive(int128 x, int128 y, int128 z) public view {
int128 y_plus_z = add(y, z);
int128 x_times_y_plus_z = mul(x, y_plus_z);
int128 x_times_y = mul(x, y);
int128 x_times_z = mul(x, z);
// Failure if all significant digits are lost
require(significant_bits_after_mult(x, y) > REQUIRED_SIGNIFICANT_BITS);
require(significant_bits_after_mult(x, z) > REQUIRED_SIGNIFICANT_BITS);
require(
significant_bits_after_mult(x, y_plus_z) > REQUIRED_SIGNIFICANT_BITS
);
assert(
equal_within_tolerance(
add(x_times_y, x_times_z),
x_times_y_plus_z,
ONE_TENTH_FP
)
);
}
// Test for identity operation
// x * 1 == x (also check that x * 0 == 0)
function mul_test_identity(int128 x) public view {
int128 x_1 = mul(x, ONE_FP);
int128 x_0 = mul(x, ZERO_FP);
assert(x_0 == ZERO_FP);
assert(x_1 == x);
}
// Test that the result increases or decreases depending
// on the value to be added
function mul_test_values(int128 x, int128 y) public view {
require(x != ZERO_FP && y != ZERO_FP);
int128 x_y = mul(x, y);
require(significant_digits_lost_in_mult(x, y) == false);
if (x >= ZERO_FP) {
if (y >= ONE_FP) {
assert(x_y >= x);
} else {
assert(x_y <= x);
}
} else {
if (y >= ONE_FP) {
assert(x_y <= x);
} else {
assert(x_y >= x);
}
}
}
/* ================================================================
Tests for overflow and edge cases.
These will make sure that the function reverts on overflow and
behaves correctly on edge cases
================================================================ */
// The result of the multiplication must be between the maximum
// and minimum allowed values for 64x64
function mul_test_range(int128 x, int128 y) public view {
int128 result;
try this.mul(x, y) {
result = this.mul(x, y);
assert(result <= MAX_64x64 && result >= MIN_64x64);
} catch {
// If it reverts, just ignore
}
}
// Multiplying the maximum value times one shouldn't revert, as it is valid
// Moreover, the result must be MAX_64x64
function mul_test_maximum_value() public view {
int128 result;
try this.mul(MAX_64x64, ONE_FP) {
// Expected behaviour, does not revert
result = this.mul(MAX_64x64, ONE_FP);
assert(result == MAX_64x64);
} catch {
assert(false);
}
}
// Multiplying the minimum value times one shouldn't revert, as it is valid
// Moreover, the result must be MIN_64x64
function mul_test_minimum_value() public view {
int128 result;
try this.mul(MIN_64x64, ONE_FP) {
// Expected behaviour, does not revert
result = this.mul(MIN_64x64, ONE_FP);
assert(result == MIN_64x64);
} catch {
assert(false);
}
}
/* ================================================================
TESTS FOR FUNCTION div()
================================================================ */
/* ================================================================
Tests for arithmetic properties.
These should make sure that the implemented function complies
with math rules and expected behaviour.
================================================================ */
// Test for identity property
// x / 1 == x (equivalent to x / x == 1)
// Moreover, x/x should not revert unless x == 0
function div_test_division_identity(int128 x) public view {
int128 div_1 = div(x, ONE_FP);
assert(x == div_1);
int128 div_x;
try this.div(x, x) {
// This should always equal one
div_x = div(x, x);
assert(div_x == ONE_FP);
} catch {
// The only allowed case to revert is if x == 0
assert(x == ZERO_FP);
}
}
// Test for negative divisor
// x / -y == -(x / y)
function div_test_negative_divisor(int128 x, int128 y) public view {
require(y < ZERO_FP);
int128 x_y = div(x, y);
int128 x_minus_y = div(x, neg(y));
assert(x_y == neg(x_minus_y));
}
// Test for division with 0 as numerator
// 0 / x = 0
function div_test_division_num_zero(int128 x) public view {
require(x != ZERO_FP);
int128 div_0 = div(ZERO_FP, x);
assert(ZERO_FP == div_0);
}
// Test that the absolute value of the result increases or
// decreases depending on the denominator's absolute value
function div_test_values(int128 x, int128 y) public view {
require(y != ZERO_FP);
int128 x_y = abs(div(x, y));
if (abs(y) >= ONE_FP) {
assert(x_y <= abs(x));
} else {
assert(x_y >= abs(x));
}
}
/* ================================================================
Tests for overflow and edge cases.
These will make sure that the function reverts on overflow and
behaves correctly on edge cases
================================================================ */
// Test for division by zero
function div_test_div_by_zero(int128 x) public view {
try this.div(x, ZERO_FP) {
// Unexpected, this should revert
assert(false);
} catch {
// Expected revert
}
}
// Test for division by a large value, the result should be less than one
function div_test_maximum_denominator(int128 x) public view {
int128 div_large = div(x, MAX_64x64);
assert(abs(div_large) <= ONE_FP);
}
// Test for division of a large value
// This should revert if |x| < 1 as it would return a value higher than max
function div_test_maximum_numerator(int128 x) public view {
int128 div_large;
try this.div(MAX_64x64, x) {
// If it didn't revert, then |x| >= 1
div_large = div(MAX_64x64, x);
assert(abs(x) >= ONE_FP);
} catch {
// Expected revert as result is higher than max
}
}
// Test for values in range
function div_test_range(int128 x, int128 y) public view {
int128 result;
try this.div(x, y) {
// If it returns a value, it must be in range
result = div(x, y);
assert(result <= MAX_64x64 && result >= MIN_64x64);
} catch {
// Otherwise, it should revert
}
}
/* ================================================================
TESTS FOR FUNCTION neg()
================================================================ */
/* ================================================================
Tests for mathematical properties.
These should make sure that the implemented function complies
with math rules and expected behaviour.
================================================================ */
// Test for the double negation
// -(-x) == x
function neg_test_double_negation(int128 x) public pure {
int128 double_neg = neg(neg(x));
assert(x == double_neg);
}
// Test for the identity operation
// x + (-x) == 0
function neg_test_identity(int128 x) public view {
int128 neg_x = neg(x);
assert(add(x, neg_x) == ZERO_FP);
}
/* ================================================================
Tests for overflow and edge cases.
These will make sure that the function reverts on overflow and
behaves correctly on edge cases
================================================================ */
// Test for the zero-case
// -0 == 0
function neg_test_zero() public view {
int128 neg_x = neg(ZERO_FP);
assert(neg_x == ZERO_FP);
}
// Test for the maximum value case
// Since this is implementation-dependant, we will actually test with MAX_64x64-EPS
function neg_test_maximum() public view {
try this.neg(sub(MAX_64x64, EPSILON)) {
// Expected behaviour, does not revert
} catch {
assert(false);
}
}
// Test for the minimum value case
// Since this is implementation-dependant, we will actually test with MIN_64x64+EPS
function neg_test_minimum() public view {
try this.neg(add(MIN_64x64, EPSILON)) {
// Expected behaviour, does not revert
} catch {
assert(false);
}
}
/* ================================================================
TESTS FOR FUNCTION abs()
================================================================ */
/* ================================================================
Tests for mathematical properties.
These should make sure that the implemented function complies
with math rules and expected behaviour.
================================================================ */
// Test that the absolute value is always positive
function abs_test_positive(int128 x) public view {
int128 abs_x = abs(x);
assert(abs_x >= ZERO_FP);
}
// Test that the absolute value of a number equals the
// absolute value of the negative of the same number
function abs_test_negative(int128 x) public pure {
int128 abs_x = abs(x);
int128 abs_minus_x = abs(neg(x));
assert(abs_x == abs_minus_x);
}
// Test the multiplicativeness property
// | x * y | == |x| * |y|
function abs_test_multiplicativeness(int128 x, int128 y) public pure {
int128 abs_x = abs(x);
int128 abs_y = abs(y);
int128 abs_xy = abs(mul(x, y));
int128 abs_x_abs_y = mul(abs_x, abs_y);
// Failure if all significant digits are lost
require(significant_digits_lost_in_mult(abs_x, abs_y) == false);
// Assume a tolerance of two bits of precision
assert(equal_within_precision(abs_xy, abs_x_abs_y, 2));
}
// Test the subadditivity property
// | x + y | <= |x| + |y|
function abs_test_subadditivity(int128 x, int128 y) public pure {
int128 abs_x = abs(x);
int128 abs_y = abs(y);
int128 abs_xy = abs(add(x, y));
assert(abs_xy <= add(abs_x, abs_y));
}
/* ================================================================
Tests for overflow and edge cases.
These will make sure that the function reverts on overflow and
behaves correctly on edge cases
================================================================ */
// Test the zero-case | 0 | = 0
function abs_test_zero() public view {
int128 abs_zero;
try this.abs(ZERO_FP) {
// If it doesn't revert, the value must be zero
abs_zero = this.abs(ZERO_FP);
assert(abs_zero == ZERO_FP);
} catch {
// Unexpected, the function must not revert here
assert(false);
}
}
// Test the maximum value
function abs_test_maximum() public view {
int128 abs_max;
try this.abs(MAX_64x64) {
// If it doesn't revert, the value must be MAX_64x64
abs_max = this.abs(MAX_64x64);
assert(abs_max == MAX_64x64);
} catch {}
}
// Test the minimum value
function abs_test_minimum() public view {
int128 abs_min;
try this.abs(MIN_64x64) {
// If it doesn't revert, the value must be the negative of MIN_64x64
abs_min = this.abs(MIN_64x64);
assert(abs_min == neg(MIN_64x64));
} catch {}
}
/* ================================================================
TESTS FOR FUNCTION inv()
================================================================ */
/* ================================================================
Tests for mathematical properties.
These should make sure that the implemented function complies
with math rules and expected behaviour.
================================================================ */
// Test that the inverse of the inverse is close enough to the
// original number
function inv_test_double_inverse(int128 x) public view {
require(x != ZERO_FP);
int128 double_inv_x = inv(inv(x));
// The maximum loss of precision will be 2 * log2(x) bits rounded up
uint256 loss = 2 * toUInt(log_2(x)) + 2;
assert(equal_within_precision(x, double_inv_x, loss));
}
// Test equivalence with division
function inv_test_division(int128 x) public view {
require(x != ZERO_FP);
int128 inv_x = inv(x);
int128 div_1_x = div(ONE_FP, x);
assert(inv_x == div_1_x);
}
// Test the anticommutativity of the division
// x / y == 1 / (y / x)
function inv_test_division_noncommutativity(
int128 x,
int128 y
) public view {
require(x != ZERO_FP && y != ZERO_FP);
int128 x_y = div(x, y);
int128 y_x = div(y, x);
require(
significant_bits_after_mult(x, inv(y)) > REQUIRED_SIGNIFICANT_BITS
);
require(
significant_bits_after_mult(y, inv(x)) > REQUIRED_SIGNIFICANT_BITS
);
assert(equal_within_tolerance(x_y, inv(y_x), ONE_TENTH_FP));
}
// Test the multiplication of inverses
// 1/(x * y) == 1/x * 1/y
function inv_test_multiplication(int128 x, int128 y) public view {
require(x != ZERO_FP && y != ZERO_FP);
int128 inv_x = inv(x);
int128 inv_y = inv(y);
int128 inv_x_times_inv_y = mul(inv_x, inv_y);
int128 x_y = mul(x, y);
int128 inv_x_y = inv(x_y);
require(significant_bits_after_mult(x, y) > REQUIRED_SIGNIFICANT_BITS);
require(
significant_bits_after_mult(inv_x, inv_y) >
REQUIRED_SIGNIFICANT_BITS
);