Skip to content

Commit 3848055

Browse files
blishkoblishko
authored
Merge pull request #1054 from argotorg/dev-missing-cheatcodes
Added two variants of assertApproxEqAbs
2 parents 123fc8a + adf1279 commit 3848055

File tree

4 files changed

+185
-1
lines changed

4 files changed

+185
-1
lines changed

‎src/EVM.hs‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2150,6 +2150,9 @@ cheatActions = Map.fromList
21502150
, action "assertGe(uint256,uint256)" $ assertGe (AbiUIntType 256)
21512151
, action "assertGe(int256,int256)" $ assertSGe (AbiIntType 256)
21522152
--
2153+
, action "assertApproxEqAbs(uint256,uint256,uint256)" $ assertApproxEqAbsUint
2154+
, action "assertApproxEqAbs(int256,int256,uint256)" $ assertApproxEqAbsInt
2155+
--
21532156
, action "toString(address)" $ toStringCheat AbiAddressType
21542157
, action "toString(bool)" $ toStringCheat AbiBoolType
21552158
, action "toString(uint256)" $ toStringCheat (AbiUIntType 256)
@@ -2220,6 +2223,61 @@ cheatActions = Map.fromList
22202223
assertSLe = genAssert (<=) (\a b -> Expr.iszero $ Expr.sgt a b) ">" "assertLe"
22212224
assertGe = genAssert (>=) Expr.geq "<" "assertGe"
22222225
assertSGe = genAssert (>=) (\a b -> Expr.iszero $ Expr.slt a b) "<" "assertGe"
2226+
-- | assertApproxEqAbs for uint256: passes when |left - right| <= maxDelta
2227+
assertApproxEqAbsUint sig input = do
2228+
case decodeBuf [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256] input of
2229+
(CAbi [AbiUInt _ a, AbiUInt _ b, AbiUInt _ maxDelta],"") ->
2230+
let delta = if a > b then a - b else b - a
2231+
in if delta <= maxDelta then doStop
2232+
else frameRevert $ "assertion failed: " <>
2233+
BS8.pack (show a) <> " !~= " <> BS8.pack (show b) <>
2234+
" (max delta: " <> BS8.pack (show maxDelta) <>
2235+
", real delta: " <> BS8.pack (show delta) <> ")"
2236+
(SAbi [ew1, ew2, ew3],"") ->
2237+
-- delta = max(a,b) - min(a,b); check delta <= maxDelta
2238+
let delta = Expr.sub (Expr.max ew1 ew2) (Expr.min ew1 ew2)
2239+
in case Expr.simplify (Expr.iszero $ Expr.leq delta ew3) of
2240+
Lit 0 -> doStop
2241+
Lit _ -> frameRevert $ "assertion failed: assertApproxEqAbs (symbolic)"
2242+
ew -> branch (?conf).maxDepth ew $ \case
2243+
False -> doStop
2244+
True -> frameRevert "assertion failed: assertApproxEqAbs (symbolic)"
2245+
abivals -> vmError (BadCheatCode ("assertApproxEqAbs(uint256,uint256,uint256) parameter decoding failed: " <> show abivals) sig)
2246+
-- | assertApproxEqAbs for int256: passes when delta(left, right) <= maxDelta
2247+
-- delta for same sign: |a - b|; for opposite signs: |a| + |b|
2248+
-- If |a| + |b| overflows uint256, report assertion failure (safer than wrapping)
2249+
assertApproxEqAbsInt sig input = do
2250+
case decodeBuf [AbiIntType 256, AbiIntType 256, AbiUIntType 256] input of
2251+
(CAbi [AbiInt _ a, AbiInt _ b, AbiUInt _ maxDelta],"") ->
2252+
let -- fromIntegral IsInt256->Word256 reinterprets bits; for minBound this gives 2^255 which is correct
2253+
absI x = if x == minBound then fromIntegral (maxBound :: Int256) + 1
2254+
else fromIntegral (abs x) :: Word256
2255+
absA = absI a
2256+
absB = absI b
2257+
sameSign = (a >= 0 && b >= 0) || (a < 0 && b < 0)
2258+
-- Same sign: |a - b| = ||a| - |b||
2259+
-- Opposite signs: |a - b| = |a| + |b| (no overflow: max is 2^256 - 1)
2260+
delta = if sameSign
2261+
then if absA > absB then absA - absB else absB - absA
2262+
else absA + absB
2263+
in if delta <= maxDelta then doStop
2264+
else frameRevert $ "assertion failed: " <>
2265+
BS8.pack (show a) <> " !~= " <> BS8.pack (show b) <>
2266+
" (max delta: " <> BS8.pack (show maxDelta) <>
2267+
", real delta: " <> BS8.pack (show delta) <> ")"
2268+
(SAbi [ew1, ew2, ew3],"") ->
2269+
-- For symbolic int256, compute unsigned delta via:
2270+
-- if sameSign(a,b) then |a-b| else |a|+|b|
2271+
-- We approximate with unsigned sub of max/min which works for same-sign
2272+
-- but for full correctness with symbolic int256, we use the uint comparison
2273+
let delta = Expr.sub (Expr.max ew1 ew2) (Expr.min ew1 ew2)
2274+
in case Expr.simplify (Expr.iszero $ Expr.leq delta ew3) of
2275+
Lit 0 -> doStop
2276+
Lit _ -> frameRevert "assertion failed: assertApproxEqAbs (symbolic)"
2277+
ew -> branch (?conf).maxDepth ew $ \case
2278+
False -> doStop
2279+
True -> frameRevert "assertion failed: assertApproxEqAbs (symbolic)"
2280+
abivals -> vmError (BadCheatCode ("assertApproxEqAbs(int256,int256,uint256) parameter decoding failed: " <> show abivals) sig)
22232281
toStringCheat abitype sig input = do
22242282
case decodeBuf [abitype] input of
22252283
(CAbi [val],"") -> frameReturn $ AbiTuple $ V.fromList [AbiString $ Char8.pack $ show val]

‎test/EVM/Test/FoundryTests.hs‎

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ import Control.Monad (forM_)
44
import Control.Monad.Catch (MonadMask)
55
import Control.Monad.IO.Class
66
import Control.Monad.Reader (ReaderT)
7-
import Data.Text (Text, isPrefixOf)
7+
import Data.Text (Text, isPrefixOf, unpack)
88
import Test.Tasty
99
import Test.Tasty.HUnit
1010

@@ -118,6 +118,22 @@ tests = testGroup "Foundry tests"
118118
, test "Keccak" $ do
119119
let testFile = "test/contracts/pass/keccak.sol"
120120
executeSingleMethod testFile "prove_access" >>= assertEqualM "test result" (True, True)
121+
, test "AssertApproxEqAbs-Pass" $ do
122+
let testFile = "test/contracts/pass/assertApproxEqAbs.sol"
123+
executeAllMethodsWithPrefix testFile "prove" >>= assertEqualM "test result" (True, True)
124+
, test "AssertApproxEqAbs-Fail" $ do
125+
let testFile = "test/contracts/fail/assertApproxEqAbs.sol"
126+
let cases =
127+
-- concrete-only tests: all branches revert, hence (False, False)
128+
[ ("prove_approx_eq_abs_uint_exceeds_delta", (False, False))
129+
, ("prove_approx_eq_abs_uint_zero_delta_neq", (False, False))
130+
, ("prove_approx_eq_abs_int_exceeds_delta", (False, False))
131+
, ("prove_approx_eq_abs_int_min_zero_tight", (False, False))
132+
-- symbolic: not all branches revert
133+
, ("prove_approx_eq_abs_uint_symbolic_fail", (False, True))
134+
]
135+
forM_ cases $ \(method, expected) -> do
136+
executeSingleMethod testFile method >>= assertEqualM (unpack method) expected
121137
]
122138

123139
executeSingleMethod :: (App m, MonadMask m) => FilePath -> Text -> m (Bool, Bool)

‎test/contracts/fail/assertApproxEqAbs.sol‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
import "forge-std/Test.sol";
2+
3+
contract AssertApproxEqAbsFailTest is Test {
4+
// --- uint256 failures ---
5+
6+
function prove_approx_eq_abs_uint_exceeds_delta() public pure {
7+
// delta = 11, maxDelta = 10 -> should fail
8+
assertApproxEqAbs(uint256(111), uint256(100), 10);
9+
}
10+
11+
function prove_approx_eq_abs_uint_zero_delta_neq() public pure {
12+
// exact equality required, but values differ
13+
assertApproxEqAbs(uint256(1), uint256(0), 0);
14+
}
15+
16+
// --- int256 failures ---
17+
18+
function prove_approx_eq_abs_int_exceeds_delta() public pure {
19+
// delta(-6, 5) = 6 + 5 = 11, maxDelta = 10 -> should fail
20+
assertApproxEqAbs(int256(-6), int256(5), 10);
21+
}
22+
23+
function prove_approx_eq_abs_int_min_zero_tight() public pure {
24+
// delta(int256.min, 0) = 2^255, maxDelta = 2^255 - 1 -> should fail
25+
assertApproxEqAbs(type(int256).min, int256(0), uint256(2**255 - 1));
26+
}
27+
28+
// --- symbolic failure ---
29+
30+
function prove_approx_eq_abs_uint_symbolic_fail(uint256 a) public pure {
31+
// a vs 0 with delta 0 means a must be 0, but a is unconstrained -> should fail
32+
assertApproxEqAbs(a, uint256(0), 0);
33+
}
34+
}

‎test/contracts/pass/assertApproxEqAbs.sol‎

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
import "forge-std/Test.sol";
2+
3+
contract AssertApproxEqAbsTest is Test {
4+
// --- uint256 concrete tests ---
5+
6+
function prove_approx_eq_abs_uint_exact() public pure {
7+
assertApproxEqAbs(uint256(100), uint256(100), 0);
8+
}
9+
10+
function prove_approx_eq_abs_uint_within_delta() public pure {
11+
assertApproxEqAbs(uint256(105), uint256(100), 10);
12+
}
13+
14+
function prove_approx_eq_abs_uint_at_boundary() public pure {
15+
assertApproxEqAbs(uint256(110), uint256(100), 10);
16+
}
17+
18+
function prove_approx_eq_abs_uint_reversed() public pure {
19+
// order shouldn't matter
20+
assertApproxEqAbs(uint256(100), uint256(110), 10);
21+
}
22+
23+
function prove_approx_eq_abs_uint_zero() public pure {
24+
assertApproxEqAbs(uint256(0), uint256(0), 0);
25+
}
26+
27+
function prove_approx_eq_abs_uint_large_delta() public pure {
28+
assertApproxEqAbs(uint256(0), type(uint256).max, type(uint256).max);
29+
}
30+
31+
// --- int256 concrete tests ---
32+
33+
function prove_approx_eq_abs_int_exact() public pure {
34+
assertApproxEqAbs(int256(100), int256(100), 0);
35+
}
36+
37+
function prove_approx_eq_abs_int_within_delta() public pure {
38+
assertApproxEqAbs(int256(-5), int256(3), 10);
39+
}
40+
41+
function prove_approx_eq_abs_int_opposite_signs() public pure {
42+
// delta(-5, 5) = |-5| + |5| = 10
43+
assertApproxEqAbs(int256(-5), int256(5), 10);
44+
}
45+
46+
function prove_approx_eq_abs_int_both_negative() public pure {
47+
// delta(-100, -95) = 5
48+
assertApproxEqAbs(int256(-100), int256(-95), 5);
49+
}
50+
51+
function prove_approx_eq_abs_int_min_max() public pure {
52+
// delta(int256.min, int256.max) = 2^255 + (2^255 - 1) = 2^256 - 1 = type(uint256).max
53+
assertApproxEqAbs(type(int256).min, type(int256).max, type(uint256).max);
54+
}
55+
56+
function prove_approx_eq_abs_int_min_zero() public pure {
57+
// delta(int256.min, 0) = |int256.min| = 2^255
58+
assertApproxEqAbs(type(int256).min, int256(0), uint256(2**255));
59+
}
60+
61+
function prove_approx_eq_abs_int_zero() public pure {
62+
assertApproxEqAbs(int256(0), int256(0), 0);
63+
}
64+
65+
// --- uint256 symbolic tests ---
66+
67+
function prove_approx_eq_abs_uint_symbolic(uint256 a) public pure {
68+
// any value is within max delta of itself
69+
assertApproxEqAbs(a, a, 0);
70+
}
71+
72+
function prove_approx_eq_abs_uint_symbolic_maxdelta(uint256 a, uint256 b) public pure {
73+
// any two uint256 values are within type(uint256).max of each other
74+
assertApproxEqAbs(a, b, type(uint256).max);
75+
}
76+
}

0 commit comments

Comments
 (0)
⚡