Jochen Hoenicke
7c2e9e68fc
Fix compile problem in one mutation
2025-08-01 18:14:20 +02:00
Jochen Hoenicke
4dff946866
New mutation for extendLock
2025-08-01 18:10:33 +02:00
Jochen Hoenicke
ff6b69caed
Added mutations to config file
2025-08-01 17:33:35 +02:00
zanderbyte-certora
6c96ce84de
add the rest mutations
2025-07-31 11:07:39 +03:00
zanderbyte-certora
2220c6659b
next period logic bug
2025-07-30 13:10:03 +03:00
zanderbyte-certora
8cdf17987a
remove holder restriction
2025-07-30 13:08:08 +03:00
zanderbyte-certora
e21324f3ff
add modifier bypass mutations
2025-07-30 12:03:51 +03:00
zanderbyte-certora
a3992bc0c0
add encoding and calculation mutations
2025-07-30 11:52:01 +03:00
zanderbyte-certora
d2ca1ae5b1
add more mutations
2025-07-29 20:09:27 +03:00
zanderbyte-certora
a63fcd9b56
Add mutation 001: accumulateFlows off-by-one
2025-07-29 10:48:59 +03:00
Jochen Hoenicke
c6b4e5e5b5
Added a README file
2025-07-18 17:35:07 +02:00
Jochen Hoenicke
dee68bd53b
Added multi_assert_check to avoid timeout
2025-07-18 15:50:00 +02:00
Jochen Hoenicke
191b9b65b7
Minor comment changes
2025-07-17 12:58:48 +02:00
Jochen Hoenicke
0f09197806
Fix rules and clean ups.
...
Set expectedFunds to 0 if it would be negative.
Prove some more auxiliary invariants.
Explain requires.
Clean-up plus comments.
2025-07-17 12:58:48 +02:00
Aleksander Kryukov
d99499b1cf
check in the latest code
2025-07-17 12:58:48 +02:00
Aleksander Kryukov
2e675d31ed
flowEnd as definition
2025-07-17 12:58:48 +02:00
Aleksander Kryukov
7ca5c8eb77
updated solvency for review
2025-07-17 12:58:48 +02:00
Aleksander Kryukov
a217a0476d
hook check in
2025-07-17 12:58:48 +02:00
Aleksander Kryukov
3350ab70dc
finished Codex's invariants and more spec cleaning
2025-07-17 12:58:48 +02:00
Aleksander Kryukov
965ae4df1e
spec cleaning
2025-07-17 12:58:48 +02:00
Aleksander Kryukov
17ebb6909d
tmp save
2025-07-17 12:58:48 +02:00
Aleksander Kryukov
3b5bd3d4fc
bug finding invariants
2025-07-17 12:58:48 +02:00
Aleksander Kryukov
2a46f53a0c
started implementing solvency
2025-07-17 12:58:48 +02:00
Aleksander Kryukov
980ca16766
adding CVLStatus to use in quantifiers
2025-07-17 12:58:48 +02:00
Aleksander Kryukov
6aed0bb07a
attempt to use sum ghost
2025-07-17 12:58:48 +02:00
Aleksander Kryukov
2f458d90ce
try to hook on _funds. fixed required
2025-07-17 12:58:48 +02:00
Mark Spanbroek
e4348de891
certora: update state changes spec now that we have vault
2025-06-11 16:31:58 +02:00
Mark Spanbroek
51862f67e9
certora: remove check on ERC20 token
...
No need to test the token itself
2025-06-11 16:31:58 +02:00
Mark Spanbroek
2d21d65624
certora: update marketplace spec now that we have vault
...
- changes to marketplace constructor
- we no longer have _marketplaceTotals
- timestamps have their own type now
- freeSlot no longer takes payout addresses
- slot state 'Paid' no longer exists
- freeSlot can be invoked more than once now
- a failed request no longer ends immediately
2025-06-11 16:31:58 +02:00
Mark Spanbroek
52cf22789c
proofs: use Timestamp instead of uint64
2025-06-11 16:31:56 +02:00
Mark Spanbroek
9826f31788
update solidity to version 0.8.28
2025-03-04 09:33:20 +01:00
Adam Uhlíř
c00152e621
perf: optimizing parameters sizing ( #207 )
...
* perf: optimizing parameters sizing
* chore: feedback
Co-authored-by: markspanbroek <mark@spanbroek.net>
* style: formatting
* perf: more optimizations
* chore: fixes
* chore: fix certora spec
* chore: more fixes for certora spec
* chore: more and more fixes for certora spec
* fix: ends type
* test(certora): timestamp conversion
* test(certora): timestamp conversion again
* test(certora): timestamp conversion revert to assert_uint64
* test(certora): timestamp with mathint
* test(certora): timestamp back with uint64 with require
* Add missing configuration
* Fix previous merge
* Update StorageRequested to use int64 for expiry
* requestDurationLimit => uint64
---------
Co-authored-by: markspanbroek <mark@spanbroek.net>
Co-authored-by: Arnaud <arnaud@status.im>
Co-authored-by: Eric <5089238+emizzle@users.noreply.github.com>
2025-02-20 16:54:41 +11:00
Adam Uhlíř
dfab6102e7
feat: repair reward ( #193 )
2024-12-12 18:39:42 +01:00
r4bbit
0b39274ed5
refactor(certora): extract allowedRequestStateChanges rule into own
...
file
Closes #192
2024-10-21 15:36:29 +02:00
Andrea Franz
2a1bef5255
chore(certora): verify slots transitions and that a slot can be paid only once
2024-10-15 11:06:46 +02:00
Adam Uhlíř
7e6187d4b1
feat: hosts payed by actual time hosting a slot ( #160 )
...
Co-authored-by: Eric <5089238+emizzle@users.noreply.github.com>
Co-authored-by: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
2024-10-08 09:38:19 +02:00
Andrea Franz
3a074abd20
chore(certora): verify possible slot state transitions
2024-09-30 12:53:06 +02:00
r4bbit
bba8736132
refactor(certora): use ghost variables for requestContext and slots
...
Instead of having additional harness code in `MarketplaceHarness` to
access fields in `requestContext` and `slots` objects, this introduces
dedicated ghost variables that keep track of the field changes and let
us read the values from there.
Prover run: https://prover.certora.com/output/6199/8343693dfc3f4ca38435f5aa10fa2345?anonymousKey=db5eaee6c688651132d1671919fb73544affa269
Closes #165
2024-08-28 10:51:42 +02:00
r4bbit
38caabeee3
fix(certora): remove incorrect requirment in
...
`paidSlotAlwaysHasCancelledOrFinishedRequest`
The mentioned invariant uses a `preserved` block with a `require
SlotState == Paid`, which essentially excludes all cases where
`SlotState != Paid`.
This was incorrectly applied. Removing that requirement causes the
prover to find a counter example where it starts with `RequestState == Started`
and `SlotState == Cancelled`.
This ultimately results in `SlotState == PAID` while `RequestState`
stays `Started`.
Counter example link: https://prover.certora.com/output/6199/a38c9bd665d544dabcffd07335c05420?anonymousKey=119a850a4d1d65ccbe8f95298615592835801d2b
A slot that is `Cancelled` however, can never belong to a request that
is `Started`. So requiring the invariant that
`cancelledSlotAlwaysHasCancelledRequest` fixes this and the rule is
passing.
Passing rule: https://prover.certora.com/output/6199/d0e165ed5d594f9fb477602af06cfeb1?anonymousKey=01ffaad46027786c38d78e5a41c03ce002032200
Closes #164
2024-08-28 07:56:32 +02:00
r4bbit
6d319c76b9
fix(certora): make vacuous rule pass
...
The rule `slotIsFailedOrFreeIfRequestHasFailed` currently has violations
as it is vacuous for some functions in the `Marketplace` contract.
The rule being vacuous means that the function on which the rule is
tested either doesn't have a case where the required conditions work (it
reverts), or, in this case, where any given function doesn't have a case
where it reaches the required state change.
There's various functions where this applies because the rule requires
that the request being tested is first any state that is `!= Failed`,
then for any function `f`, when `f` is executed, the required state of
the request is `Failed`.
Prover run that confirms this: https://prover.certora.com/output/6199/82ed96aac5014cb9a7485fc3752fb399?anonymousKey=28c97adbbe14ead331dc8e4b8ed05e94528075a3
There's two options to go about this:
1. Either filter out all functions from the rule where the rule is
vacuous (this is dangerous because we'd exclude those functions
entirely from the rule)
2. Or, rewrite the rule such that the requirements are relaxed
This commit implements option 2.
Instead of requiring that the starting request state has to be `!=
Failed`, we simply assert that **if** it **was** not `Failed` and then
**is** `Failed`, the corresponding slot is either failed or free.
Prover run that passes: https://prover.certora.com/output/6199/16fa074bd23146e59c21964c98bbb3e0?anonymousKey=229d721cf35873bed5eae67696eed803ce75fd18
2024-08-27 15:08:52 +02:00
r4bbit
3a6249e886
fix(certora): make rule for allowed request state changes work again
2024-08-23 14:01:43 +02:00
r4bbit
7dc26ccc47
chore(certora): add rule that cancelled requests stay cancelled and finished requests stay finished
2024-08-23 14:01:43 +02:00
r4bbit
09ca8481fb
fix(certora): fix rule that describes allowed request state changes
...
This broke due to a newly introduced signature for `fillSlot()`
2024-08-23 14:01:43 +02:00
r4bbit
faeb808d41
fix(certora): fix invariant that requests are started when slots filled
2024-08-23 14:01:43 +02:00
r4bbit
7c542e72b6
chore(certora); add rule to verify slot is failed or free when request
...
has failed
2024-08-23 14:01:43 +02:00
r4bbit
7dc5566cd9
chore(certora): add invariant that cancelled slots always belong to cancelled requests
2024-08-23 14:01:43 +02:00
r4bbit
0acb522fe7
chore(certora): add invariant that paid slots always have a finished or cancelled request
2024-08-23 14:01:43 +02:00
r4bbit
a1229b5af3
chore(certora): introduce invariant that finished slots always belong to finished requests
2024-08-23 14:01:43 +02:00
r4bbit
5b5a3c9e2e
chore(certora): introduce invariant that failed requests are always ended
2024-08-23 14:01:43 +02:00
r4bbit
7ce7a5dda0
chore(certora): add invariant that cancelled requests are always expired
2024-08-23 14:01:43 +02:00
