Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

test(medusa): requester properties #57

Merged
merged 29 commits into from
Nov 28, 2024
Merged
Show file tree
Hide file tree
Changes from 19 commits
Commits
Show all changes
29 commits
Select commit Hold shift + click to select a range
730db68
test: property-id 1
0xJabberwock Nov 19, 2024
24f492c
test(medusa): property-id 2
0xJabberwock Nov 20, 2024
e45ff98
test(medusa): epoch manager handler
0xJabberwock Nov 20, 2024
149474b
test(medusa): remove _ghost_epochChainIds
0xJabberwock Nov 20, 2024
823c735
test(medusa): update ghost state in property function
0xJabberwock Nov 20, 2024
f13c8ff
test(medusa): properties md update
simon-something Nov 20, 2024
c0ffee6
refactor(medusa): sanity check in setup
simon-something Nov 21, 2024
c0ffeed
chore(medusa): lib deployement
simon-something Nov 21, 2024
28d711a
test(medusa): tweak ebo request creator handler
0xJabberwock Nov 21, 2024
28d58da
test(medusa): assertion failure reasons
0xJabberwock Nov 21, 2024
5fafe29
chore(medusa): refactor chainId handling
simon-something Nov 22, 2024
1e453c7
chore(medusa): rm epoch mgr handler
simon-something Nov 22, 2024
59b46aa
chore(medusa): bound min max
simon-something Nov 22, 2024
c19b12d
chore(medusa): rm useless bounds
simon-something Nov 22, 2024
b7da278
chore(medusa): redo constraint we needed
simon-something Nov 22, 2024
3e7ae3e
test(medusa): track chains added after setup
0xJabberwock Nov 22, 2024
8072e09
test(medusa): wrap ghost logic within try blocks
0xJabberwock Nov 25, 2024
1c33374
test(medusa): rewrite prop-1 to assert
0xJabberwock Nov 25, 2024
98303e6
test(medusa): remove handlers around setters
0xJabberwock Nov 25, 2024
ed0d9fc
test(medusa): comment out chain removal handler
0xJabberwock Nov 27, 2024
10a7a07
test(medusa): unwrap ghost logic from try blocks
0xJabberwock Nov 27, 2024
710c3d1
test(medusa): compliant properties
0xJabberwock Nov 27, 2024
bc114a9
test(medusa): correct prop-1
0xJabberwock Nov 27, 2024
3730d59
test(medusa): disputer properties (#58)
simon-something Nov 27, 2024
23dff81
test(medusa): fix compilation after merge
0xJabberwock Nov 27, 2024
049f6fe
test(medusa): aggregate properties 1 and 2
0xJabberwock Nov 27, 2024
c349092
test(medusa): update helper functions
0xJabberwock Nov 27, 2024
9498da3
Merge branch 'test/handler-cov' of github-wonderland:defi-wonderland/…
0xJabberwock Nov 27, 2024
70ae4f8
test(medusa): progress proposer properties
0xJabberwock Nov 28, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions medusa.json
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
"corpusDirectory": "test/invariants/corpus",
"coverageEnabled": true,
"targetContracts": ["FuzzTest"],
"predeployedContracts": {},
"predeployedContracts": { "ValidatorLib": "0xc0ffee" },
"targetContractsBalances": [],
"constructorArgs": {},
"deployerAddress": "0x30000",
Expand Down Expand Up @@ -76,7 +76,7 @@
"target": "test/invariants/FuzzTest.t.sol",
"solcVersion": "",
"exportDirectory": "",
"args": ["--compile-libraries=(ValidatorLib,0xf0)"]
"args": ["--compile-libraries=(ValidatorLib,0xc0ffee)"]
}
},
"logging": {
Expand Down
5 changes: 2 additions & 3 deletions test/invariants/FuzzTest.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ pragma solidity 0.8.26;
import {PropertyParent} from './properties/PropertyParent.t.sol';

contract FuzzTest is PropertyParent {
function test_debug() public {
this.property_sanityCheck();
}
//solhint-disable no-empty-blocks
function test_debug() public {}
}
106 changes: 59 additions & 47 deletions test/invariants/PROPERTIES.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,55 +12,23 @@ Prophet modules in use (some modified from the example repo):
- AccessControl: every external function is gated, for Horizon operators (ie `caller` is either msg.sender or msg.sender is authorized as
operator for `caller`)


- Requester
- Can always create a request
- only one chainId/epoch can be requested at a time (a tuple can have second request if finalized without answer)

- Proposer
- Can always send answer before the deadline if enough token to bound in Horizon staking contract AND if any previous response is disputed OR no response at all
- Can escalate MAX ESCALATION times
- Every escalation creates a new tying buffer for further escalation (even if past deadline)

- Disputer
- Can always dispute if before finalisation/during dispute window, if enough token to bound in Horizon staking and not previously disputed
- only first disputed response is escalated (others go to resolution)
- Can escalate MAX ESCALATION times
- every escalation creates a new tying buffer for further escalation (even if past deadline)

- Pledgers:
- can pledge on any active dispute or resolution, during tying buffer/before deadline, if it’s that side’s turn
- Can only pledge one pledge at a time (you can only surpass other team by one pledge at a time), first to tie then to out-pledge (always 2 ties by side)

- Protocol
- finalise only after deadline
- no possible way for a given actor to use another one’s bonded token (no bonding or pledging/claiming on behalf of someone else if not allowed in the Horison staking contract)
- bonded amount only accessible by one requestId
- disputeId and responseId can only be tied to a given requestId
- arbitrator: can always settled a dispute if not finalised (can be a no resolution)


- disputer

wins → his money + proposer bonded amt
loose loose all
no resolution his money (when no pledging or max escalation on both side or other resolution module logic if only dispute module)

- pledger
wins → their money + enemy
no resolution -> their money

**winning determined by *pledgers* (b, c)**

bonded dispute goes to resolution if: escalateDispute or tie

## Properties & Invariants

| Id | Properties | Type |
| --- | ---------- | ---- |
| | requester can always create a request | |
| | there can only be one active request per chainId/epoch at a time | |

| Id | Properties | Type | Tested |
| --- | ------------------------------------------------------------------------------------------------------------------------------------- | ---- | ------ |
| 1 | requester can always create a request | | [ ] |
| 2 | there can only be one active request per chainId/epoch at a time | | [ ] |
| 3 | a proposer can always propose an answer before the deadline, if no response has been submitted | | [ ] |
| 4 | a proposer can always propose an answer before the deadline, if previous response is disputted and has staked | | [ ] |
| 5 | a proposer or a disputer can escalate max MAX_ESCALATION times, each time creating a new tying buffer | | [ ] |
| 6 | a disputer can always dispute a response before the finalisation, if no previous dispute has been made | | [ ] |
| 7 | a disputer can only escalate the first disputed response | | [ ] |
| 8 | a pledger can only pledge for the correct side for an active dispure or resolution, during the tying buffer or before the deadline | | [ ] |
| 9 | an arbitrator can always settle a dispute if it has not been finalised yet | | [ ] |
| 10 | an answer can only be finalized after the deadline | | [ ] |
| 11 | bonded token can never be used on behalf of someone else, unless allowed by the Horizon staking contract | | [ ] |
| 12 | each bonded amount can only be tied to one requestId | | [ ] |
| 13 | each disputeId and responseId can only be tied to one requestId | | [ ] |

## Handler coverage

Expand Down Expand Up @@ -147,3 +115,47 @@ Oracle
| escalateDispute(Request,Response,Dispute) external | [] |
| resolveDispute(Request,Response,Dispute) external | [] |
| finalize(Request,Response) external | [] |




- Requester
- Can always create a request
- only one chainId/epoch can be requested at a time (a tuple can have second request if finalized without answer)

- Proposer
- Can always send answer before the deadline if enough token to bound in Horizon staking contract AND if any previous response is disputed OR no response at all
- Can escalate MAX ESCALATION times
- Every escalation creates a new tying buffer for further escalation (even if past deadline)

- Disputer
- Can always dispute if before finalisation/during dispute window, if enough token to bound in Horizon staking and not previously disputed
- only first disputed response is escalated (others go to resolution)
- Can escalate MAX ESCALATION times
- every escalation creates a new tying buffer for further escalation (even if past deadline)

- Pledgers:
- can pledge on any active dispute or resolution, during tying buffer/before deadline, if it’s that side’s turn
- Can only pledge one pledge at a time (you can only surpass other team by one pledge at a time), first to tie then to out-pledge (always 2 ties by side)

- Protocol
- finalise only after deadline
- no possible way for a given actor to use another one’s bonded token (no bonding or pledging/claiming on behalf of someone else if not allowed in the Horison staking contract)
- bonded amount only accessible by one requestId
- disputeId and responseId can only be tied to a given requestId
- arbitrator: can always settled a dispute if not finalised (can be a no resolution)


- disputer

wins → his money + proposer bonded amt
loose loose all
no resolution his money (when no pledging or max escalation on both side or other resolution module logic if only dispute module)

- pledger
wins → their money + enemy
no resolution -> their money

**winning determined by *pledgers* (b, c)**

bonded dispute goes to resolution if: escalateDispute or tie
108 changes: 103 additions & 5 deletions test/invariants/Setup.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ contract Setup is Utils {
IEpochManager internal epochManager;

// Constants
uint256 internal constant START_EPOCH = 1000;
uint256 internal immutable START_EPOCH = block.timestamp;
uint64 internal constant MIN_THAWING_PERIOD = 1 days;
uint128 internal constant INITIAL_MAX_USERS_TO_CHECK = 10;
uint32 internal constant MAX_VERIFIER_CUT = 1_000_000;
Expand All @@ -88,10 +88,12 @@ contract Setup is Utils {
uint256 internal constant TYING_BUFFER = 3 days;
uint256 internal constant DISPUTE_DISPUTE_WINDOW = 2 weeks;

string[] internal INITIAL_CHAINS = ['mainnet', 'optimism', 'arbitrum'];

constructor() {
// Deploy mock contracts
GRT = IERC20(address(new FuzzERC20()));
epochManager = IEpochManager(address(new MockEpochManager(START_EPOCH)));
epochManager = IEpochManager(address(new MockEpochManager()));
horizonStaking = IHorizonStaking(address(new MockHorizonStaking(GRT)));

// Deploy core contracts
Expand Down Expand Up @@ -157,12 +159,15 @@ contract Setup is Utils {
horizonAccountingExtension.approveModule(address(bondEscalationModule));

// Set up initial chain IDs
eboRequestCreator.addChain('mainnet');
eboRequestCreator.addChain('optimism');
eboRequestCreator.addChain('arbitrum');
for (uint256 i; i < INITIAL_CHAINS.length; i++) {
eboRequestCreator.addChain(INITIAL_CHAINS[i]);
}

// Set up initial module parameters
_setupModuleParameters();

// System health check
_sanityCheck();
}

function _setupModuleParameters() internal {
Expand Down Expand Up @@ -205,4 +210,97 @@ contract Setup is Utils {
// Set finality module
eboRequestCreator.setFinalityModuleData(address(eboFinalityModule));
}

/// @custom:property-id 0
/// @custom:property Check if eboRequestCreator has the correct properties, including the ones set after its initial deployment
function _sanityCheck() internal {
assertEq(address(eboRequestCreator.ORACLE()), address(oracle), 'prop-0: wrong oracle address');

assertEq(address(eboRequestCreator.ARBITRABLE()), address(arbitrable), 'prop-0: wrong arbitrable address');

assertEq(eboRequestCreator.START_EPOCH(), START_EPOCH, 'prop-0: wrong start epoch');

assertEq(address(eboRequestCreator.epochManager()), address(epochManager), 'prop-0: wrong epoch manager address');

IOracle.Request memory initialRequestStored = eboRequestCreator.getRequestData();

assertEq(
initialRequestStored.requestModule, address(eboRequestModule), 'prop-0: wrong request module in initialRequest'
);

assertEq(
initialRequestStored.responseModule,
address(bondedResponseModule),
'prop-0: wrong response module in initialRequest'
);

assertEq(
initialRequestStored.disputeModule, address(bondEscalationModule), 'prop-0: wrong disputeModule in initialRequest'
);

assertEq(
initialRequestStored.resolutionModule,
address(arbitratorModule),
'prop-0: wrong resolutionModule in initialRequest'
);

assertEq(
initialRequestStored.finalityModule, address(eboFinalityModule), 'prop-0: wrong finalityModule in initialRequest'
);

assertEq(initialRequestStored.requester, address(eboRequestCreator), 'prop-0: wrong requester in initialRequest');

assertEq(
initialRequestStored.requestModuleData,
abi.encode(
IEBORequestModule.RequestParameters({
epoch: START_EPOCH,
chainId: 'mainnet',
accountingExtension: IAccountingExtension(address(horizonAccountingExtension)),
paymentAmount: PAYMENT_AMOUNT
})
),
'prop-0: wrong requestModuleData in initialRequest'
);

assertEq(
initialRequestStored.responseModuleData,
abi.encode(
IBondedResponseModule.RequestParameters({
accountingExtension: IAccountingExtension(address(horizonAccountingExtension)),
bondToken: GRT,
bondSize: RESPONSE_BOND_SIZE,
deadline: RESPONSE_DEADLINE,
disputeWindow: RESPONSE_DISPUTE_WINDOW
})
),
'prop-0: wrong responseModuleData module data in initialRequest'
);

assertEq(
initialRequestStored.disputeModuleData,
abi.encode(
IBondEscalationModule.RequestParameters({
accountingExtension: IBondEscalationAccounting(address(horizonAccountingExtension)),
bondToken: GRT,
bondSize: DISPUTE_BOND_SIZE,
maxNumberOfEscalations: MAX_NB_ESCALATION,
bondEscalationDeadline: DISPUTE_DEADLINE,
tyingBuffer: TYING_BUFFER,
disputeWindow: DISPUTE_DISPUTE_WINDOW
})
),
'prop-0: wrong disputeModuleData in initialRequest'
);

assertEq(
initialRequestStored.resolutionModuleData,
abi.encode(IArbitratorModule.RequestParameters({arbitrator: address(councilArbitrator)})),
'prop-0: wrong resolutionModuleData in initialRequest'
);

assertEq(initialRequestStored.finalityModuleData, bytes(''), 'prop-0: wrong finality module data in initialRequest');

assertEq(initialRequestStored.nonce, 0, 'prop-0: wrong nonce in initialRequest');
}
}
28 changes: 10 additions & 18 deletions test/invariants/handlers/BaseHandler.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,11 @@ import {Actors} from '../helpers/Actors.t.sol';
contract BaseHandler is Setup, Actors {
// Track all created request IDs
bytes32[] internal _ghost_requests;
// Track all created request IDs per epoch and chainId
mapping(uint256 _epoch => mapping(string _chainId => bytes32[] _requestIds)) internal _ghost_requestsPerEpochChainId;

// Track the chainId->chain (reverse the hash)
mapping(bytes32 _hash => string _chain) internal _ghost_chainIdToChain;

// Track request details
mapping(bytes32 _requestId => IOracle.Request _data) internal _ghost_requestData;
Expand All @@ -24,33 +29,20 @@ contract BaseHandler is Setup, Actors {
// Track which requests came from EBORequestCreator
mapping(bytes32 _requestId => bool _isFromRequestCreator) internal _ghost_validRequests;

// Track chain IDs used per epoch to prevent duplicates
mapping(uint256 _epoch => mapping(string _chainId => bool _isRequested)) internal _ghost_epochChainIds;

// Track bonds and pledges
mapping(address _owner => mapping(bytes32 _requestId => uint256 _boundedAmount)) internal _ghost_bonds;
mapping(address _pledger => mapping(bytes32 _disputeId => uint256 _pledgedAmount)) internal _ghost_pledgesFor;
mapping(address _pledger => mapping(bytes32 _disputeId => uint256 _pledgedAmount)) internal _ghost_pledgesAgainst;

// Helper functions
function _boundEpoch(uint256 _epoch) internal view returns (uint256) {
return bound(_epoch, START_EPOCH, START_EPOCH + 1000);
}

function _boundAmount(uint256 _amount) internal pure returns (uint256) {
return bound(_amount, 1, 1_000_000e18);
}

function _boundBlockNumber(uint256 _blockNumber) internal view returns (uint256) {
return bound(_blockNumber, block.number - 1000, block.number);
}
function _getRandomChainId(uint256 _seed) internal view returns (string memory) {
bytes32[] memory chainIds = eboRequestCreator.getAllowedChainIds();
if (chainIds.length == 0) return '';

function _generateChainId(uint256 _seed) internal pure returns (string memory) {
string[3] memory chains = ['mainnet', 'optimism', 'arbitrum'];
return chains[_seed % 3];
return _ghost_chainIdToChain[chainIds[_seed % chainIds.length]];
}

function _getRandomRequest(uint256 _seed) internal view returns (bytes32) {
function _getRandomRequestId(uint256 _seed) internal view returns (bytes32) {
if (_ghost_requests.length == 0) return bytes32(0);
return _ghost_requests[_seed % _ghost_requests.length];
}
Expand Down
6 changes: 3 additions & 3 deletions test/invariants/handlers/HandlerBondEscalationModule.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ import {BaseHandler, IOracle} from './BaseHandler.t.sol';

contract HandlerBondEscalationModule is BaseHandler {
function handlePledgeForDispute(uint256 _requestSeed, uint256 _disputeIndex, uint256 _actorSeed) external {
bytes32 requestId = _getRandomRequest(_requestSeed);
bytes32 requestId = _getRandomRequestId(_requestSeed);
if (requestId == bytes32(0)) return;

IOracle.Dispute memory dispute = _getRandomDispute(requestId, _disputeIndex);
Expand All @@ -22,7 +22,7 @@ contract HandlerBondEscalationModule is BaseHandler {
}

function handlePledgeAgainstDispute(uint256 _requestSeed, uint256 _disputeIndex, uint256 _actorSeed) external {
bytes32 requestId = _getRandomRequest(_requestSeed);
bytes32 requestId = _getRandomRequestId(_requestSeed);
if (requestId == bytes32(0)) return;

IOracle.Dispute memory dispute = _getRandomDispute(requestId, _disputeIndex);
Expand All @@ -39,7 +39,7 @@ contract HandlerBondEscalationModule is BaseHandler {
}

function handleSettleBondEscalation(uint256 _requestSeed, uint256 _disputeIndex) external {
bytes32 requestId = _getRandomRequest(_requestSeed);
bytes32 requestId = _getRandomRequestId(_requestSeed);
if (requestId == bytes32(0)) return;

IOracle.Dispute memory dispute = _getRandomDispute(requestId, _disputeIndex);
Expand Down
2 changes: 1 addition & 1 deletion test/invariants/handlers/HandlerBondedResponseModule.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ import {BaseHandler, IOracle} from './BaseHandler.t.sol';

contract HandlerBondedResponseModule is BaseHandler {
function handleReleaseUnutilizedResponse(uint256 _requestSeed) external {
bytes32 requestId = _getRandomRequest(_requestSeed);
bytes32 requestId = _getRandomRequestId(_requestSeed);
if (requestId == bytes32(0)) return;

IOracle.Response memory response = _getRandomActiveResponse(requestId, _requestSeed);
Expand Down
2 changes: 1 addition & 1 deletion test/invariants/handlers/HandlerCouncilArbitrator.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ import {BaseHandler, IOracle} from './BaseHandler.t.sol';

contract HandlerCouncilArbitrator is BaseHandler {
function handleArbitrateDispute(uint256 _requestSeed, uint256 _disputeIndex, uint256 _statusSeed) external {
bytes32 requestId = _getRandomRequest(_requestSeed);
bytes32 requestId = _getRandomRequestId(_requestSeed);
if (requestId == bytes32(0)) return;

IOracle.Dispute memory dispute = _getRandomDispute(requestId, _disputeIndex);
Expand Down
Loading
Loading