Mark Spanbroek
ad991304b1
certora: cleanup
2025-06-12 17:14:49 +02:00
Mark Spanbroek
0305965bd5
certora: update certora-cli to 7.29.3
...
Reason: Vault.conf parsing errors with old certora-cli
2025-06-12 17:03:00 +02:00
Mark Spanbroek
6d16b0c613
certora: run vault rules as part of the CI
2025-06-12 16:58:58 +02:00
Mark Spanbroek
cbe52b4934
certora: remove configuration that fixes solidity to solc8.28
...
Reason: makes certoraRun in the CI fail
2025-06-12 16:55:53 +02:00
Aleksander Kryukov
26e8fce9bb
finished Codex's invariants and more spec cleaning
2025-06-12 15:59:40 +02:00
Aleksander Kryukov
1742b1dae5
spec cleaning
2025-06-12 15:59:40 +02:00
Aleksander Kryukov
d0e4208854
tmp save
2025-06-12 15:59:40 +02:00
Aleksander Kryukov
25c8f11a06
bug finding invariants
2025-06-12 15:59:40 +02:00
Aleksander Kryukov
73ac5820a6
started implementing solvency
2025-06-12 15:59:40 +02:00
Aleksander Kryukov
3cda5a0ce0
adding CVLStatus to use in quantifiers
2025-06-12 15:59:40 +02:00
Aleksander Kryukov
c35b8b6d74
attempt to use sum ghost
2025-06-12 15:59:40 +02:00
Aleksander Kryukov
ae94d1ebf3
try to hook on _funds. fixed required
2025-06-12 15:59:40 +02:00
Mark Spanbroek
b5ab3869b9
marketplace: better tests for repair
...
Co-Authored-By: Adam Uhlíř <adam@uhlir.dev>
2025-06-12 15:50:09 +02:00
Mark Spanbroek
d7554ce0d2
marketplace: improve withdraw test
...
Co-Authored-By: Adam Uhlíř <adam@uhlir.dev>
2025-06-12 08:05:24 +02:00
Mark Spanbroek
4410941061
marketplace: add test for hosts that makes request fail
...
Co-Authored-By: Adam Uhlíř <adam@uhlir.dev>
2025-06-11 17:00:52 +02:00
Mark Spanbroek
cd8b6572f3
marketplace: fix test
...
Co-Authored-By: Adam Uhlíř <adam@uhlir.dev>
2025-06-11 17:00:24 +02:00
Mark Spanbroek
075d97e5da
marketplace: clarify why we flow & transfer funds before burning
...
Co-Authored-By: Adam Uhlíř <adam@uhlir.dev>
2025-06-11 16:31:58 +02:00
Mark Spanbroek
895e36fbba
marketplace: clarify why we flow funds from client to itself
...
Co-Authored-By: Adam Uhlíř <adam@uhlir.dev>
2025-06-11 16:31:58 +02:00
Mark Spanbroek
bdee8de9cc
marketplace: move collateralPerSlot() to Requests.sol
...
reason: the function only depends on the request, and it is similar
to the pricePerSlotPerSecond function
Co-Authored-By: Adam Uhlíř <adam@uhlir.dev>
2025-06-11 16:31:58 +02:00
Mark Spanbroek
1fb3d2130b
marketplace: cleanup
...
Co-Authored-By: Adam Uhlíř <adam@uhlir.dev>
2025-06-11 16:31:58 +02:00
Mark Spanbroek
724344cb5e
marketplace: allow slot payout for failed requests
...
reason: hosts are paid for the time that they hosted
the slot up until the time that the request failed
Co-Authored-By: Adam Uhlíř <adam@uhlir.dev>
2025-06-11 16:31:58 +02:00
Mark Spanbroek
2cd45214cf
marketplace: no longer expose forciblyFreeSlot in tests
...
reason: freeSlot() will call forciblyFreeSlot when contract is not
finished, so we can use that instead
2025-06-11 16:31:58 +02:00
Mark Spanbroek
47f3c1e36d
marketplace: keep request in myRequests when freeing slot
...
Because a client might still need to call withdraw()
2025-06-11 16:31:58 +02:00
Mark Spanbroek
9603025202
marketplace: simplify requestEnd()
2025-06-11 16:31:58 +02:00
Mark Spanbroek
7a566182d5
marketplace: re-instate currentCollateral()
...
So that a storage provider can know how much collateral is
returned when it calls freeSlot()
2025-06-11 16:31:58 +02:00
Mark Spanbroek
6971766b62
marketplace: cleanup tests
2025-06-11 16:31:58 +02:00
Mark Spanbroek
6bd4144714
marketplace: repair reward is paid out at the end
...
It is no longer a discount on the collateral, to
simplify reasoning about collateral in the sales
module of the codex node
2025-06-11 16:31:58 +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
468bc2e833
marketplace: remove 'Paid' state
...
This state is no longer necessary, vault ensures
that payouts happen only once. Hosts could bypass
this state anyway by withdrawing from the vault
directly.
2025-06-11 16:29:21 +02:00
Mark Spanbroek
5fb63c4939
marketplace: cleanup
2025-06-11 16:29:21 +02:00
Mark Spanbroek
06a9e417b2
marketplace: remove accounting that is now done by vault
2025-06-11 16:29:21 +02:00
Mark Spanbroek
e60ff36202
marketplace: formatting
2025-06-11 16:29:21 +02:00
Mark Spanbroek
17646f15b9
marketplace: designate validator rewards
...
so that they can no longer be transfered
within the vault
2025-06-11 16:29:21 +02:00
Mark Spanbroek
b6f5d65630
marketplace: transfer repair reward in vault
2025-06-11 16:29:21 +02:00
Mark Spanbroek
5c9910d29d
marketplace: optimize storage reads and writes
2025-06-11 16:29:21 +02:00
Mark Spanbroek
5e8031eda5
marketplace: remove accounting that is now done by vault
2025-06-11 16:29:21 +02:00
Mark Spanbroek
c626372d55
marketplace: burn tokens in vault when slashing
...
- move all collateral calculatons to separate library
2025-06-11 16:29:21 +02:00
Mark Spanbroek
3ea02914fa
marketplace: simplify withdrawing by client
...
- removes RequestCancelled event, which was not great anyway
because it is not emitted at the moment that the request is
cancelled
2025-06-11 16:29:21 +02:00
Mark Spanbroek
9570404fba
marketplace: remove accounting that is now done by vault
2025-06-11 16:29:21 +02:00
Mark Spanbroek
15c58e1a81
marketplace: remove fuzzing
...
replaced by formal verification with certora
2025-06-11 16:29:21 +02:00
Mark Spanbroek
761fbd4f84
marketplace: collateral is uint128
...
Vault stores balances as uint128
2025-06-11 16:29:21 +02:00
Mark Spanbroek
4f45856a5e
marketplace: use Timestamp, Duration and TokensPerSecond types
2025-06-11 16:29:19 +02:00
Mark Spanbroek
ccf91075bf
vault: move Timestamp and TokensPerSecond libraries one level up
2025-06-11 16:29:13 +02:00
Mark Spanbroek
0910c83428
marketplace: use vault in marketplace
2025-06-11 16:29:13 +02:00
Mark Spanbroek
6ebed47327
marketplace: remove support for changing payout addresses
2025-06-11 16:29:13 +02:00
Mark Spanbroek
aee61bdb45
marketplace: deploy vault and set it in the marketplace
2025-06-11 16:29:13 +02:00
Mark Spanbroek
341b303789
marketplace: use SafeERC20 for transfers
2025-06-11 16:29:11 +02:00
