Skip to content

Commit

Permalink
chore: separate helpers
Browse files Browse the repository at this point in the history
  • Loading branch information
@varunsrin
varunsrin committed Jul 26, 2023
1 parent fd29863 commit 7ddb82e
Showing 1 changed file with 51 additions and 60 deletions.
111 changes: 51 additions & 60 deletions test/IdRegistry/IdRegistry.symbolic.t.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@ import {IdRegistryHarness} from "../Utils.sol";
contract IdRegistrySymTest is SymTest, Test {
IdRegistryHarness idRegistry;
address trustedCaller;

address x;
address y;

Expand Down Expand Up @@ -37,44 +36,26 @@ contract IdRegistrySymTest is SymTest, Test {
y = svm.createAddress("y");
}

// Additional setup to cover various input states
function init() public {
if (svm.createBool("disableTrustedOnly?")) {
idRegistry.disableTrustedOnly();
}
if (svm.createBool("pauseRegistration?")) {
idRegistry.pauseRegistration();
}
}

// Verify the IdRegistry invariants
function check_invariant(bytes4 selector, address caller) public {
init();

// Consider two distinct addresses
function verifyInvariants(bytes4 selector, address caller) public {
_initState();
vm.assume(x != y);

// Record pre-state
uint256 oldIdX = idRegistry.idOf(x);
uint256 oldIdY = idRegistry.idOf(y);

uint256 oldIdCounter = idRegistry.getIdCounter();

bool oldPaused = idRegistry.paused();

// Execute an arbitrary tx to IdRegistry
vm.prank(caller);
(bool success,) = address(idRegistry).call(mk_calldata(selector));
(bool success,) = address(idRegistry).call(_calldataFor(selector));
vm.assume(success); // ignore reverting cases

// Record post-state
uint256 newIdX = idRegistry.idOf(x);
uint256 newIdY = idRegistry.idOf(y);

uint256 newIdCounter = idRegistry.getIdCounter();

// Verify invariant properties

// Ensure that there is no recovery address associated with fid 0.
assert(idRegistry.getRecoveryOf(0) == address(0));

Expand All @@ -94,35 +75,8 @@ contract IdRegistrySymTest is SymTest, Test {
}
}

function mk_calldata(bytes4 selector) internal returns (bytes memory) {
// Generate calldata based on the function selector
bytes memory args;
if (selector == idRegistry.registerFor.selector) {
args = abi.encode(
svm.createAddress("to"),
svm.createAddress("recovery"),
svm.createUint256("deadline"),
svm.createBytes(65, "sig")
);
} else if (selector == idRegistry.transfer.selector) {
args = abi.encode(svm.createAddress("to"), svm.createUint256("deadline"), svm.createBytes(65, "sig"));
} else if (selector == idRegistry.recover.selector) {
args = abi.encode(
svm.createAddress("from"),
svm.createAddress("to"),
svm.createUint256("deadline"),
svm.createBytes(65, "sig")
);
} else {
args = svm.createBytes(1024, "data");
}
return abi.encodePacked(selector, args);
}

function check_transfer(address caller, address to, address other) public {
init();

// Consider another address that is not involved
function verifyTransfer(address caller, address to, address other) public {
_initState();
vm.assume(other != caller && other != to);

// Record pre-state
Expand All @@ -139,8 +93,6 @@ contract IdRegistrySymTest is SymTest, Test {
uint256 newIdTo = idRegistry.idOf(to);
uint256 newIdOther = idRegistry.idOf(other);

// Verify correctness properties

// Ensure that the fid has been transferred from the `caller` to the `to`.
assert(newIdTo == oldIdCaller);
if (caller != to) {
Expand All @@ -152,17 +104,14 @@ contract IdRegistrySymTest is SymTest, Test {
assert(newIdOther == oldIdOther);
}

function check_recover(address caller, address from, address to, address other) public {
init();

// Consider other address that is not involved
function verifyRecovery(address caller, address from, address to, address other) public {
_initState();
vm.assume(other != from && other != to);

// Record pre-state
uint256 oldIdFrom = idRegistry.idOf(from);
uint256 oldIdTo = idRegistry.idOf(to);
uint256 oldIdOther = idRegistry.idOf(other);

address oldRecoveryFrom = idRegistry.getRecoveryOf(oldIdFrom);

// Execute recover with symbolic arguments
Expand All @@ -174,8 +123,6 @@ contract IdRegistrySymTest is SymTest, Test {
uint256 newIdTo = idRegistry.idOf(to);
uint256 newIdOther = idRegistry.idOf(other);

// Verify correctness properties

// Ensure that the caller is the recovery address
assert(caller == oldRecoveryFrom);

Expand All @@ -189,4 +136,48 @@ contract IdRegistrySymTest is SymTest, Test {
// Ensure that the other fids are not affected.
assert(newIdOther == oldIdOther);
}

/*//////////////////////////////////////////////////////////////
HELPERS
//////////////////////////////////////////////////////////////*/

/**
* @dev Initialize IdRegistry with symbolic arguments for state.
*/
function _initState() public {
if (svm.createBool("disableTrustedOnly?")) {
idRegistry.disableTrustedOnly();
}
if (svm.createBool("pauseRegistration?")) {
idRegistry.pauseRegistration();
}
}

/**
* @dev Generates valid calldata for a given function selector.
*/
function _calldataFor(bytes4 selector) internal returns (bytes memory) {
bytes memory args;
if (selector == idRegistry.registerFor.selector) {
args = abi.encode(
svm.createAddress("to"),
svm.createAddress("recovery"),
svm.createUint256("deadline"),
svm.createBytes(65, "sig")
);
} else if (selector == idRegistry.transfer.selector) {
args = abi.encode(svm.createAddress("to"), svm.createUint256("deadline"), svm.createBytes(65, "sig"));
} else if (selector == idRegistry.recover.selector) {
args = abi.encode(
svm.createAddress("from"),
svm.createAddress("to"),
svm.createUint256("deadline"),
svm.createBytes(65, "sig")
);
} else {
args = svm.createBytes(1024, "data");
}

return abi.encodePacked(selector, args);
}
}

0 comments on commit 7ddb82e

Please sign in to comment.