test(medusa): requester properties #57
Conversation
| /// @custom:property-id 2 | ||
| /// @custom:property There can only be one active request per chainId/epoch at a time | ||
| function property_onlyOneActiveRequest(uint256 _requestIdSeed) external { |
There was a problem hiding this comment.
As of now, bear in mind that prop-1 already takes into account active requests, so it asserts what prop-2 does as well – necessarily, as it is a reversion reason of the function call. Should we keep a separate prop-2 then?
There was a problem hiding this comment.
no, totally fine to test multiple properties in the same function (what we did so far is then keep naming based on the first property, but could be a more generic one, like property_createRequest), have all custom natspec included and a one line comment with the id before the relevant assert
/// @custom:property-id 1
/// @custom:property ...
/// @custom:property-id 2
/// @custom:property ...
/// @custom:property-id 3
/// @custom:property ...
function property_test() external {
(...)
try ...
// property 1
assertEq...
// property 2
...
catch
// property 3
assert ...|
|
||
| assertLte(activeRequests, 1, 'prop-2: same chainId/epoch active requests'); |
There was a problem hiding this comment.
Related assertions between prop-1 and prop-2 aren't exactly equal because the former updates ghost state after asserting, and the latter counts on already updated ghost state. So, in presence of and within try blocks, should the ghost state be updated before or after asserting?
There was a problem hiding this comment.
that's why having explicit Hoare logic would help I think (I mentioned it somewhere, but too late to refactor it everywhere, perhaps) -> the assertion(s) is/are the post-condition(s), ghost is just an extra-help to track state between calls (ie "propagate" the state change of the assertion, in other word, they are the pre-conditions of another test), imo, post-condition shouldn't rely on having the statement updating a ghost variable.
short version: after
# 🤖 Linear Closes GRT-XXX --------- Co-authored-by: drgorillamd <83670532+drgorillamd@users.noreply.github.com>
…EBO-core into test/property-ebo-request-creator
0xJabberwock
changed the title
🤖 Linear
Closes GRT-XXX