test: Echidna contract with invariants

- registerMembership
- attemptExtensionRace
- attemptErasureRace
This commit is contained in:
Roman 2025-10-27 13:31:46 +08:00
parent 0be627965f
commit ab0aed0bbc
No known key found for this signature in database
GPG Key ID: 583BDF43C238B83E

View File

@ -6,13 +6,15 @@ import "../src/WakuRlnV2.sol";
import "./TestStableToken.sol";
import { ERC1967Proxy } from "@openzeppelin/contracts/proxy/ERC1967/ERC1967Proxy.sol";
// Echidna invariants for WakuRlnV2 multi-user erasure/reuse (run: echidna-test this.sol --contract EchidnaTest)
// Echidna invariants for WakuRlnV2 multi-user timestamp manipulation races
contract EchidnaTest {
WakuRlnV2 internal w;
TestStableToken internal token;
address internal tokenOwner = address(this);
uint32 internal totalRegisteredRate;
uint32 internal numUsers; // Set in fuzz
// Storage for multi-user registrations and their timestamps (to check races per user)
mapping(uint256 => uint256) internal registrationTimes; // idCommitment => registration timestamp
uint256[] internal registeredIds; // List of registered IDs for iteration in checks
constructor() {
address tokenImpl = address(new TestStableToken());
@ -29,75 +31,75 @@ contract EchidnaTest {
w = WakuRlnV2(proxyAddr);
}
function testEraseAndReuse(uint32 _numUsers, bool fullErase, uint32 rateLimit) public {
numUsers = _numUsers;
// Function to register a single membership; Echidna can call this multiple times with time advances between
function registerMembership(uint256 idCommitment, uint32 rateLimit) public {
(, uint256 price) = w.priceCalculator().calculate(rateLimit);
token.mint(address(this), price);
token.approve(address(w), price);
w.register(idCommitment, rateLimit, new uint256[](0));
// Multi-user registers
totalRegisteredRate = 0;
for (uint32 i = 1; i <= numUsers; i++) {
address user = address(uint160(i)); // Simple addresses
(, uint256 price) = w.priceCalculator().calculate(rateLimit);
token.mint(user, price);
// Simulate approval/register (Echidna can't prank, so direct call; assume sender)
token.approve(address(w), price);
w.register(i, rateLimit, new uint256[](0));
totalRegisteredRate += rateLimit;
}
require(w.currentTotalRateLimit() == totalRegisteredRate, "Registration invariant failed");
// Erasures (fuzz numErasures up to numUsers - 1)
uint32 numErasures = uint32(uint256(keccak256(abi.encodePacked(address(this)))) % (numUsers - 1)) + 1;
uint256[] memory eraseIds = new uint256[](numErasures);
bool[] memory erased = new bool[](numUsers + 1);
uint32 eraseCount = 0;
while (eraseCount < numErasures) {
uint32 eraseIdx = uint32(uint256(keccak256(abi.encodePacked(address(this), eraseCount))) % numUsers) + 1;
if (!erased[eraseIdx]) {
eraseIds[eraseCount] = eraseIdx;
erased[eraseIdx] = true;
eraseCount++;
}
}
uint32 eraser = uint32(uint256(keccak256(abi.encodePacked(address(this)))) % numUsers) + 1;
w.eraseMemberships(eraseIds, fullErase);
uint32 erasedRate = numErasures * rateLimit;
require(w.currentTotalRateLimit() == totalRegisteredRate - erasedRate, "Erasure invariant failed");
// Reuses
uint32 numReuses = numErasures;
for (uint32 i = 0; i < numReuses; i++) {
uint32 reuser = uint32(uint256(keccak256(abi.encodePacked(address(this), i + numUsers))) % numUsers) + 1;
address user = address(uint160(reuser));
(, uint256 price) = w.priceCalculator().calculate(rateLimit);
token.mint(user, price);
token.approve(address(w), price);
uint256 newId =
100 + uint256(keccak256(abi.encodePacked("new", reuser, address(this), i))) % (w.Q() - 1) + 1;
w.register(newId, rateLimit, new uint256[](0));
}
// Check proofs
for (uint32 i = 1; i <= numUsers; i++) {
bool isErased = erased[i];
uint256 checkId = isErased ? 0 : i;
if (checkId != 0) {
(, uint32 idx, uint256 commitment) = w.getMembershipInfo(checkId);
uint256[20] memory proof = w.getMerkleProof(idx);
require(_verifyMerkleProof(proof, w.root(), idx, commitment, 20), "Proof invalid");
}
}
require(w.nextFreeIndex() == numUsers, "Index growth invariant failed");
// Store registration time and add to list
registrationTimes[idCommitment] = block.timestamp;
registeredIds.push(idCommitment);
}
// Helper for proof verification
// Function to attempt extension on a random registered membership and assert based on current time
function attemptExtensionRace(uint256 index) public {
if (registeredIds.length == 0) return; // Skip if no registrations yet
uint256 focusId = registeredIds[index % registeredIds.length];
uint256 regTime = registrationTimes[focusId];
uint256 graceStart = regTime + uint256(w.activeDurationForNewMemberships());
uint256 graceEnd = graceStart + uint256(w.gracePeriodDurationForNewMemberships());
bool isInGrace = (block.timestamp >= graceStart && block.timestamp < graceEnd);
bool isExpired = (block.timestamp >= graceEnd);
uint256[] memory ids = new uint256[](1);
ids[0] = focusId;
bool success = false;
try w.extendMemberships(ids) {
success = true;
} catch { }
// Assertion: Extension should succeed only if in grace period
assert(success == isInGrace);
// Additional assertions: State consistency
assert(w.isInGracePeriod(focusId) == isInGrace);
assert(w.isExpired(focusId) == isExpired);
}
// Function to attempt erasure on a random registered membership and assert based on current time
function attemptErasureRace(uint256 index, bool fullErase) public {
if (registeredIds.length == 0) return; // Skip if no registrations yet
uint256 focusId = registeredIds[index % registeredIds.length];
uint256 regTime = registrationTimes[focusId];
uint256 activeEnd = regTime + uint256(w.activeDurationForNewMemberships());
uint256 graceEnd = activeEnd + uint256(w.gracePeriodDurationForNewMemberships());
bool isActive = (block.timestamp < activeEnd);
bool isExpired = (block.timestamp >= graceEnd);
uint256[] memory ids = new uint256[](1);
ids[0] = focusId;
bool success = false;
try w.eraseMemberships(ids, fullErase) {
success = true;
} catch { }
// Assertion: Erasure should succeed only if not active (i.e., in grace or expired)
assert(success == !isActive);
// Additional assertions: State consistency
assert(w.isExpired(focusId) == isExpired);
assert(!w.isInGracePeriod(focusId) == (isExpired || isActive));
}
// Helper for proof verification (if needed in future expansions)
function _verifyMerkleProof(
uint256[20] memory proof,
uint256 root,