From ab0aed0bbc2f360bf6ee46a6019918c88f6d836b Mon Sep 17 00:00:00 2001 From: Roman Date: Mon, 27 Oct 2025 13:31:46 +0800 Subject: [PATCH] test: Echidna contract with invariants - registerMembership - attemptExtensionRace - attemptErasureRace --- test/EchidnaTest.t.sol | 140 +++++++++++++++++++++-------------------- 1 file changed, 71 insertions(+), 69 deletions(-) diff --git a/test/EchidnaTest.t.sol b/test/EchidnaTest.t.sol index 53dda4d..be5acad 100644 --- a/test/EchidnaTest.t.sol +++ b/test/EchidnaTest.t.sol @@ -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,