Add RebasingToken example

runtimeverification · Jan 7, 2025 · 75bda55 · 75bda55
1 parent e30bbe8
commit 75bda55
Showing 1 changed file with 23 additions and 0 deletions.
diff --git a/oz_erc20/test/RebasingToken.t.sol b/oz_erc20/test/RebasingToken.t.sol
@@ -0,0 +1,23 @@
+pragma solidity ^0.8.13;
+
+import {Test, console} from "forge-std/Test.sol";
+
+contract RebasingTokenTest is Test {
+    function check_balanceToRebasingCredits(uint256 rebasingCreditsPerToken, uint256 balance) public {
+        vm.assume(rebasingCreditsPerToken <= 1e27 && rebasingCreditsPerToken >= 1e18);
+        vm.assume(balance <= 1e25);
+
+        uint256 rebasingCredits = ((balance) * rebasingCreditsPerToken + 1e18 - 1) / 1e18;
+        uint256 actualBalance = (rebasingCredits * 1e18) / rebasingCreditsPerToken;
+        assert(actualBalance == balance);
+    }
+
+    function testFail_balanceToRebasingCredits(uint256 rebasingCreditsPerToken, uint256 balance) public {
+        vm.assume(rebasingCreditsPerToken <= 1e27); // && rebasingCreditsPerToken >= 1e18);
+        vm.assume(balance <= 1e25);
+
+        uint256 rebasingCredits = ((balance) * rebasingCreditsPerToken + 1e18 - 1) / 1e18;
+        uint256 actualBalance = (rebasingCredits * 1e18) / rebasingCreditsPerToken;
+        assert(actualBalance == balance);
+    }
+}