Certora formally verified rewards checker #1656

QGarchery · 2023-03-20T17:24:30Z

Please look at the README for a description of this PR

This reverts commit 336fd3f.

Co-authored-by: MathisGD <[email protected]> Signed-off-by: Romain Milon <[email protected]>

QGarchery · 2024-03-06T10:50:11Z

A simple thing to add is a check in wellFormed().

Oh right, that's an oversight, we should definitely add that !

I was also wondering about proving something like all users can never claim more than the value in root, but that's not straightforward to do

That would be a nice property to prove, but I'm not sure either how to do it

certora/checker/Checker.sol

certora/helpers/MerkleTreeLib.sol

certora/specs/RewardsDistributor.spec

certora/helpers/MerkleTrees.sol

certora/specs/MerkleTrees.spec

certora/README.md

foundry.toml

certora/checker/Checker.sol

certora/helpers/MerkleTreeLib.sol

certora/helpers/MerkleTrees.sol

certora/checker/create_certificate.py

feat: verification of rewards, fresh start

e9885c0

QGarchery added the 🧮 certora label Mar 20, 2023

QGarchery self-assigned this Mar 20, 2023

QGarchery and others added 20 commits March 21, 2023 15:27

temp: prover error with axiom

336fd3f

temp: revert pover error with axiom

8b49960

This reverts commit 336fd3f.

feat: ignore findAndClaimAt in the verification

6ed55d1

feat: enforce hashing to non-address in merkle

8759453

feat: factorizing invariants

bbc96f0

feat: add isCreatedWellFormed as an axiom

23d5e23

ci(docs): move to foundry-docs-aws

43b4858

Update .github/workflows/ci-docs-autogen.yml

2a61fcd

Co-authored-by: MathisGD <[email protected]> Signed-off-by: Romain Milon <[email protected]>

refactor(ci): use of OpenID connect

390b4ee

fix: removing useless lines

ad356f8

fix: useless lines

32f9f76

fix: indexes caching

8953d04

test: remove indexes update skip

d49daf1

fix(ci): update foundry action

92f52c2

test: indexes caching (ma2)

3662e72

docs: minor comments improvements

8ef8205

fix: indexes caching

fd7a798

test: index caching issue (mc core + lens)

78abecd

fix: indexes caching (mc lens)

1904ac6

chore: migrate to CVL2

2c174e0

github-actions bot added ⚙️ ci 👻 aave-v2 🟢 compound 🧪 testing labels Jun 21, 2023

QGarchery added 3 commits June 21, 2023 14:12

refactor: move spec to specs

4f704d6

fix: don't use grounding branch

e222bf2

chore: remove prover args

dfc13de

QGarchery added 7 commits March 6, 2024 11:55

feat: check sum of values for internal nodes

9f51cb2

refactor: require well formed on the path only

1c33193

refactor: well formed path with a loop

9736d1c

refactor: require once in loop

aff7755

chore: increase loop iteration to 4

ed73f4b

chore: loop iter to 4 in merkle tree

527a8c6

Merge remote-tracking branch 'origin/main' into certora-rewards

adb56a4

MathisGD reviewed Mar 10, 2024

View reviewed changes

QGarchery added 11 commits March 11, 2024 11:13

refactor: remove unnecessary require invariant

3b0b13f

docs: add comments

48e40e8

refactor: variable renaming

823f623

refactor: use structs in merkle tree lib

38276f2

fix: new interface for node creation

f5daa10

feat: check increasing claim amounts

b6f4f2a

refactor: remove unnecessary root of the Merkle tree

07db98d

docs: example of list of proofs

ef54f35

refactor: checker is now based on the contract instead of the lib

223f718

feat: check update root storage change

0b41773

fix: update root is not envfree

8a3aed9

MathisGD reviewed Mar 12, 2024

View reviewed changes

QGarchery added 3 commits March 12, 2024 11:56

refactor: restrict read permission

0ffd207

docs: node is the root candidate

8ad06d2

refactor: clarify verification

226d508

MathisGD approved these changes Mar 12, 2024

View reviewed changes

Merge remote-tracking branch 'origin/main' into certora-rewards

821c8ec

QGarchery requested a review from MerlinEgalite March 15, 2024 17:10

MerlinEgalite approved these changes Mar 15, 2024

View reviewed changes

QGarchery merged commit fbb5b13 into main Mar 15, 2024
8 checks passed

QGarchery deleted the certora-rewards branch March 15, 2024 17:24

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Certora formally verified rewards checker #1656

Certora formally verified rewards checker #1656

QGarchery commented Mar 20, 2023 •

edited

Loading

QGarchery commented Mar 6, 2024

Certora formally verified rewards checker #1656

Certora formally verified rewards checker #1656

Conversation

QGarchery commented Mar 20, 2023 • edited Loading

QGarchery commented Mar 6, 2024

QGarchery commented Mar 20, 2023 •

edited

Loading