From 0b39274ed5d0305b58001a4d2ad2240849e49be3 Mon Sep 17 00:00:00 2001 From: r4bbit <445106+0x-r4bbit@users.noreply.github.com> Date: Tue, 15 Oct 2024 12:12:59 +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 | 80 +-------------------------------- certora/specs/StateChanges.spec | 42 +++++++++++++++++ certora/specs/shared.spec | 40 +++++++++++++++++ package.json | 5 ++- 6 files changed, 117 insertions(+), 81 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 a3cd22e..a2eb0c4 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: | + npm run ${{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 0000000..11c5536 --- /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 9e00376..59e31ee 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; diff --git a/certora/specs/StateChanges.spec b/certora/specs/StateChanges.spec new file mode 100644 index 0000000..82cb5d9 --- /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 0000000..b8249fd --- /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 cee7974..494ff55 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",