From 773af9fea751d12adeb1243eb6cb8fb31068b436 Mon Sep 17 00:00:00 2001 From: r4bbit <445106+0x-r4bbit@users.noreply.github.com> Date: Tue, 15 Oct 2024 12:07:18 +0200 Subject: [PATCH] refactor(certora): extract `allowedRequestStateChanges` rule into own file Closes #192 --- .github/workflows/ci.yml | 8 ++- certora/confs/StateChanges.conf | 23 ++++++ certora/specs/Marketplace.spec | 123 +------------------------------- certora/specs/StateChanges.spec | 42 +++++++++++ certora/specs/shared.spec | 40 +++++++++++ package.json | 5 +- 6 files changed, 117 insertions(+), 124 deletions(-) create mode 100644 certora/confs/StateChanges.conf create mode 100644 certora/specs/StateChanges.spec create mode 100644 certora/specs/shared.spec diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a3cd22e2..502864aa 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -70,10 +70,16 @@ jobs: run: npm install - name: Verify rules - run: npm run verify + run: | + pnpm ${{matrix.rule}} env: CERTORAKEY: ${{ secrets.CERTORAKEY }} strategy: fail-fast: false max-parallel: 16 + matrix: + rule: + - verify:marketplace + - verify:state_changes + diff --git a/certora/confs/StateChanges.conf b/certora/confs/StateChanges.conf new file mode 100644 index 00000000..11c55363 --- /dev/null +++ b/certora/confs/StateChanges.conf @@ -0,0 +1,23 @@ +{ + "files": [ + "certora/harness/MarketplaceHarness.sol", + "contracts/Marketplace.sol", + "contracts/Groth16Verifier.sol", + "certora/helpers/ERC20A.sol", + ], + "parametric_contracts": ["MarketplaceHarness"], + "link" : [ + "MarketplaceHarness:_token=ERC20A", + "MarketplaceHarness:_verifier=Groth16Verifier" + ], + "msg": "Verifying StateChanges", + "rule_sanity": "basic", + "verify": "MarketplaceHarness:certora/specs/StateChanges.spec", + "optimistic_loop": true, + "loop_iter": "3", + "optimistic_hashing": true, + "hashing_length_bound": "512", +} + + + diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec index 9e00376b..3eb10955 100644 --- a/certora/specs/Marketplace.spec +++ b/certora/specs/Marketplace.spec @@ -1,3 +1,5 @@ +import "./shared.spec"; + using ERC20A as Token; methods { @@ -108,16 +110,6 @@ hook Sstore _slots[KEY Marketplace.SlotId slotId].state Marketplace.SlotState ne } } -ghost mapping(MarketplaceHarness.SlotId => MarketplaceHarness.RequestId) slotIdToRequestId; - -hook Sload Marketplace.RequestId defaultValue _slots[KEY MarketplaceHarness.SlotId SlotId].requestId { - require slotIdToRequestId[SlotId] == defaultValue; -} - -hook Sstore _slots[KEY MarketplaceHarness.SlotId SlotId].requestId Marketplace.RequestId defaultValue { - slotIdToRequestId[SlotId] = defaultValue; -} - ghost mapping(MarketplaceHarness.RequestId => uint256) slotsFilledGhost; hook Sload uint256 defaultValue _requestContexts[KEY MarketplaceHarness.RequestId RequestId].slotsFilled { @@ -142,22 +134,6 @@ hook Sstore _requestContexts[KEY MarketplaceHarness.RequestId RequestId].endsAt | Helper functions | --------------------------------------------*/ -function ensureValidRequestId(Marketplace.RequestId requestId) { - // Without this, the prover will find counter examples with `requestId == 0`, - // which are unlikely in practice as `requestId` is a hash from a request object. - // However, `requestId == 0` enforces `SlotState.Free` in the `fillSlot` function regardless, - // which ultimately results in counter examples where we have a state change - // RequestState.Finished -> RequestState.Started, which is forbidden. - // - // COUNTER EXAMPLE: https://prover.certora.com/output/6199/81939b2b12d74a5cae5e84ceadb901c0?anonymousKey=a4ad6268598a1077ecfce75493b0c0f9bc3b17a0 - // - // The `require` below is a hack to ensure we exclude such cases as the code - // reverts in `requestIsKnown()` modifier (simply `require requestId != 0` isn't - // sufficient here) - // require requestId == to_bytes32(0) => currentContract._requests[requestId].client == 0; - require requestId != to_bytes32(0) && currentContract._requests[requestId].client != 0; -} - function canCancelRequest(method f) returns bool { return f.selector == sig:withdrawFunds(Marketplace.RequestId).selector; } @@ -228,13 +204,6 @@ invariant failedRequestAlwaysEnded(env e, Marketplace.RequestId requestId) currentContract.requestState(e, requestId) == Marketplace.RequestState.Failed => endsAtGhost[requestId] < lastBlockTimestampGhost; -// STATUS - verified -// finished slot always has finished request -// https://prover.certora.com/output/6199/3371ee4f80354ac9b05b1c84c53b6154?anonymousKey=eab83785acb61ccd31ed0c9d5a2e9e2b24099156 -invariant finishedSlotAlwaysHasFinishedRequest(env e, Marketplace.SlotId slotId) - currentContract.slotState(e, slotId) == Marketplace.SlotState.Finished => - currentContract.requestState(e, slotIdToRequestId[slotId]) == Marketplace.RequestState.Finished; - // STATUS - verified // paid slot always has finished or cancelled request // https://prover.certora.com/output/6199/d0e165ed5d594f9fb477602af06cfeb1?anonymousKey=01ffaad46027786c38d78e5a41c03ce002032200 @@ -246,12 +215,6 @@ invariant paidSlotAlwaysHasFinishedOrCancelledRequest(env e, Marketplace.SlotId } } -// STATUS - verified -// cancelled slot always belongs to cancelled request -// https://prover.certora.com/output/6199/80d5dc73d406436db166071e277283f1?anonymousKey=d5d175960dc40f72e22ba8e31c6904a488277e57 -invariant cancelledSlotAlwaysHasCancelledRequest(env e, Marketplace.SlotId slotId) - currentContract.slotState(e, slotId) == Marketplace.SlotState.Cancelled => - currentContract.requestState(e, slotIdToRequestId[slotId]) == Marketplace.RequestState.Cancelled; /*-------------------------------------------- | Properties | @@ -301,45 +264,6 @@ rule slotIsFailedOrFreeIfRequestHasFailed(env e, method f) { } -rule allowedRequestStateChanges(env e, method f) { - calldataarg args; - Marketplace.SlotId slotId; - - Marketplace.RequestId requestId = slotIdToRequestId[slotId]; - - // needed, otherwise it finds counter examples where - // `SlotState.Cancelled` and `RequestState.New` - requireInvariant cancelledSlotAlwaysHasCancelledRequest(e, slotId); - // needed, otherwise it finds counter example where - // `SlotState.Finished` and `RequestState.New` - requireInvariant finishedSlotAlwaysHasFinishedRequest(e, slotId); - - ensureValidRequestId(requestId); - - Marketplace.RequestState requestStateBefore = currentContract.requestState(e, requestId); - - // we need to check for `freeSlot(slotId)` here to ensure it's being called with - // the slotId we're interested in and not any other slotId (that may not pass the - // required invariants) - if (f.selector == sig:freeSlot(Marketplace.SlotId).selector || f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector) { - freeSlot(e, slotId); - } else { - f(e, args); - } - Marketplace.RequestState requestStateAfter = currentContract.requestState(e, requestId); - - // RequestState.New -> RequestState.Started - assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Started => requestStateBefore == Marketplace.RequestState.New; - - // RequestState.Started -> RequestState.Finished - assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Finished => requestStateBefore == Marketplace.RequestState.Started; - - // RequestState.Started -> RequestState.Failed - assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Failed => requestStateBefore == Marketplace.RequestState.Started; - - // RequestState.New -> RequestState.Cancelled - assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Cancelled => requestStateBefore == Marketplace.RequestState.New; -} rule functionsCausingRequestStateChanges(env e, method f) { calldataarg args; @@ -378,31 +302,6 @@ rule functionsCausingSlotStateChanges(env e, method f) { // SlotState.Free -> SlotState.Filled assert slotStateBefore != Marketplace.SlotState.Filled && slotStateAfter == Marketplace.SlotState.Filled => canFillSlot(f); -} - -rule allowedSlotStateChanges(env e, method f) { - calldataarg args; - Marketplace.SlotId slotId; - - slotAttributesAreConsistent(e, slotId); - - Marketplace.Slot slot = currentContract.slots(e, slotId); - Marketplace.SlotState slotStateBefore = currentContract.slotState(e, slotId); - f(e, args); - Marketplace.SlotState slotStateAfter = currentContract.slotState(e, slotId); - - // Cannot change from Paid - assert slotStateBefore == Marketplace.SlotState.Paid => slotStateAfter == Marketplace.SlotState.Paid; - - // SlotState.Cancelled -> SlotState.Cancelled || SlotState.Failed || Finished || Paid - assert slotStateBefore == Marketplace.SlotState.Cancelled => ( - slotStateAfter == Marketplace.SlotState.Cancelled || - slotStateAfter == Marketplace.SlotState.Failed || - slotStateAfter == Marketplace.SlotState.Finished || - slotStateAfter == Marketplace.SlotState.Paid - ); - - // SlotState.Filled only from Free assert slotStateBefore != Marketplace.SlotState.Filled && slotStateAfter == Marketplace.SlotState.Filled => slotStateBefore == Marketplace.SlotState.Free; } @@ -460,21 +359,3 @@ rule slotStateChangesOnlyOncePerFunctionCall(env e, method f) { assert slotStateChangesCountAfter <= slotStateChangesCountBefore + 1; } - -rule slotCanBeFreedAndPaidOnce { - env e; - Marketplace.SlotId slotId; - address rewardRecipient; - address collateralRecipient; - - Marketplace.SlotState slotStateBefore = currentContract.slotState(e, slotId); - require slotStateBefore != Marketplace.SlotState.Paid; - freeSlot(e, slotId, rewardRecipient, collateralRecipient); - - Marketplace.SlotState slotStateAfter = currentContract.slotState(e, slotId); - require slotStateAfter == Marketplace.SlotState.Paid; - - freeSlot@withrevert(e, slotId, rewardRecipient, collateralRecipient); - - assert lastReverted; -} diff --git a/certora/specs/StateChanges.spec b/certora/specs/StateChanges.spec new file mode 100644 index 00000000..82cb5d97 --- /dev/null +++ b/certora/specs/StateChanges.spec @@ -0,0 +1,42 @@ +import "./shared.spec"; + +rule allowedRequestStateChanges(env e, method f) { + calldataarg args; + Marketplace.SlotId slotId; + + Marketplace.RequestId requestId = slotIdToRequestId[slotId]; + + // needed, otherwise it finds counter examples where + // `SlotState.Cancelled` and `RequestState.New` + requireInvariant cancelledSlotAlwaysHasCancelledRequest(e, slotId); + // needed, otherwise it finds counter example where + // `SlotState.Finished` and `RequestState.New` + requireInvariant finishedSlotAlwaysHasFinishedRequest(e, slotId); + + ensureValidRequestId(requestId); + + Marketplace.RequestState requestStateBefore = currentContract.requestState(e, requestId); + + // we need to check for `freeSlot(slotId)` here to ensure it's being called with + // the slotId we're interested in and not any other slotId (that may not pass the + // required invariants) + if (f.selector == sig:freeSlot(Marketplace.SlotId).selector || f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector) { + freeSlot(e, slotId); + } else { + f(e, args); + } + Marketplace.RequestState requestStateAfter = currentContract.requestState(e, requestId); + + // RequestState.New -> RequestState.Started + assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Started => requestStateBefore == Marketplace.RequestState.New; + + // RequestState.Started -> RequestState.Finished + assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Finished => requestStateBefore == Marketplace.RequestState.Started; + + // RequestState.Started -> RequestState.Failed + assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Failed => requestStateBefore == Marketplace.RequestState.Started; + + // RequestState.New -> RequestState.Cancelled + assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Cancelled => requestStateBefore == Marketplace.RequestState.New; +} + diff --git a/certora/specs/shared.spec b/certora/specs/shared.spec new file mode 100644 index 00000000..b8249fd4 --- /dev/null +++ b/certora/specs/shared.spec @@ -0,0 +1,40 @@ +ghost mapping(MarketplaceHarness.SlotId => MarketplaceHarness.RequestId) slotIdToRequestId; + +hook Sload Marketplace.RequestId defaultValue _slots[KEY MarketplaceHarness.SlotId SlotId].requestId { + require slotIdToRequestId[SlotId] == defaultValue; +} + +hook Sstore _slots[KEY MarketplaceHarness.SlotId SlotId].requestId Marketplace.RequestId defaultValue { + slotIdToRequestId[SlotId] = defaultValue; +} + +function ensureValidRequestId(Marketplace.RequestId requestId) { + // Without this, the prover will find counter examples with `requestId == 0`, + // which are unlikely in practice as `requestId` is a hash from a request object. + // However, `requestId == 0` enforces `SlotState.Free` in the `fillSlot` function regardless, + // which ultimately results in counter examples where we have a state change + // RequestState.Finished -> RequestState.Started, which is forbidden. + // + // COUNTER EXAMPLE: https://prover.certora.com/output/6199/81939b2b12d74a5cae5e84ceadb901c0?anonymousKey=a4ad6268598a1077ecfce75493b0c0f9bc3b17a0 + // + // The `require` below is a hack to ensure we exclude such cases as the code + // reverts in `requestIsKnown()` modifier (simply `require requestId != 0` isn't + // sufficient here) + // require requestId == to_bytes32(0) => currentContract._requests[requestId].client == 0; + require requestId != to_bytes32(0) && currentContract._requests[requestId].client != 0; +} + +// STATUS - verified +// cancelled slot always belongs to cancelled request +// https://prover.certora.com/output/6199/80d5dc73d406436db166071e277283f1?anonymousKey=d5d175960dc40f72e22ba8e31c6904a488277e57 +invariant cancelledSlotAlwaysHasCancelledRequest(env e, Marketplace.SlotId slotId) + currentContract.slotState(e, slotId) == Marketplace.SlotState.Cancelled => + currentContract.requestState(e, slotIdToRequestId[slotId]) == Marketplace.RequestState.Cancelled; + +// STATUS - verified +// finished slot always has finished request +// https://prover.certora.com/output/6199/3371ee4f80354ac9b05b1c84c53b6154?anonymousKey=eab83785acb61ccd31ed0c9d5a2e9e2b24099156 +invariant finishedSlotAlwaysHasFinishedRequest(env e, Marketplace.SlotId slotId) + currentContract.slotState(e, slotId) == Marketplace.SlotState.Finished => + currentContract.requestState(e, slotIdToRequestId[slotId]) == Marketplace.RequestState.Finished; + diff --git a/package.json b/package.json index cee79744..494ff55c 100644 --- a/package.json +++ b/package.json @@ -10,8 +10,9 @@ "format:check": "prettier --check contracts/**/*.sol test/**/*.js", "lint": "solhint contracts/**.sol", "deploy": "hardhat deploy", - "verify": "npm run verify:marketplace", - "verify:marketplace": "certoraRun certora/confs/Marketplace.conf" + "verify": "npm run verify:marketplace && npm run verify:state_changes", + "verify:marketplace": "certoraRun certora/confs/Marketplace.conf", + "verify:state_changes": "certoraRun certora/confs/StateChanges.conf" }, "devDependencies": { "@nomiclabs/hardhat-ethers": "^2.2.1",