Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Certora formally verified rewards checker #1656

Merged
merged 97 commits into from
Mar 15, 2024
Merged

Certora formally verified rewards checker #1656

merged 97 commits into from
Mar 15, 2024

Commits on Mar 20, 2023

  1. feat: verification of rewards, fresh start

    @QGarchery
    QGarchery committed Mar 20, 2023
    Configuration menu
    Copy the full SHA
    e9885c0 View commit details
    Browse the repository at this point in the history

Commits on Mar 21, 2023

  1. temp: prover error with axiom

    @QGarchery
    QGarchery committed Mar 21, 2023
    Configuration menu
    Copy the full SHA
    336fd3f View commit details
    Browse the repository at this point in the history

  2. temp: revert pover error with axiom 

    This reverts commit 336fd3f.
    @QGarchery
    QGarchery committed Mar 21, 2023
    Configuration menu
    Copy the full SHA
    8b49960 View commit details
    Browse the repository at this point in the history

  3. feat: ignore findAndClaimAt in the verification

    @QGarchery
    QGarchery committed Mar 21, 2023
    Configuration menu
    Copy the full SHA
    6ed55d1 View commit details
    Browse the repository at this point in the history

Commits on Mar 23, 2023

  1. feat: enforce hashing to non-address in merkle

    @QGarchery
    QGarchery committed Mar 23, 2023
    Configuration menu
    Copy the full SHA
    8759453 View commit details
    Browse the repository at this point in the history

  2. feat: factorizing invariants

    @QGarchery
    QGarchery committed Mar 23, 2023
    Configuration menu
    Copy the full SHA
    bbc96f0 View commit details
    Browse the repository at this point in the history

Commits on Apr 13, 2023

  1. feat: add isCreatedWellFormed as an axiom

    @QGarchery
    QGarchery committed Apr 13, 2023
    Configuration menu
    Copy the full SHA
    23d5e23 View commit details
    Browse the repository at this point in the history

Commits on Jun 21, 2023

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

    @Rubilmax @QGarchery
    Rubilmax authored and QGarchery committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    43b4858 View commit details
    Browse the repository at this point in the history

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

    Co-authored-by: MathisGD <[email protected]>
Signed-off-by: Romain Milon <[email protected]>
    @Rubilmax @MathisGD @QGarchery
    2 people authored and QGarchery committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    2a61fcd View commit details
    Browse the repository at this point in the history

  3. refactor(ci): use of OpenID connect

    @julien-devatom @QGarchery
    julien-devatom authored and QGarchery committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    390b4ee View commit details
    Browse the repository at this point in the history

  4. fix: removing useless lines

    @Tristan22400 @QGarchery
    Tristan22400 authored and QGarchery committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    ad356f8 View commit details
    Browse the repository at this point in the history

  5. fix: useless lines

    @Tristan22400 @QGarchery
    Tristan22400 authored and QGarchery committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    32f9f76 View commit details
    Browse the repository at this point in the history

  6. fix: indexes caching

    @MathisGD @QGarchery
    MathisGD authored and QGarchery committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    8953d04 View commit details
    Browse the repository at this point in the history

  7. test: remove indexes update skip

    @MathisGD @QGarchery
    MathisGD authored and QGarchery committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    d49daf1 View commit details
    Browse the repository at this point in the history

  8. fix(ci): update foundry action

    @julien-devatom @QGarchery
    julien-devatom authored and QGarchery committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    92f52c2 View commit details
    Browse the repository at this point in the history

  9. test: indexes caching (ma2)

    @MathisGD @QGarchery
    MathisGD authored and QGarchery committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    3662e72 View commit details
    Browse the repository at this point in the history

  10. docs: minor comments improvements

    @MathisGD @QGarchery
    MathisGD authored and QGarchery committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    8ef8205 View commit details
    Browse the repository at this point in the history

  11. fix: indexes caching

    @MathisGD @QGarchery
    MathisGD authored and QGarchery committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    fd7a798 View commit details
    Browse the repository at this point in the history

  12. test: index caching issue (mc core + lens)

    @MathisGD @QGarchery
    MathisGD authored and QGarchery committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    78abecd View commit details
    Browse the repository at this point in the history

  13. fix: indexes caching (mc lens)

    @MathisGD @QGarchery
    MathisGD authored and QGarchery committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    1904ac6 View commit details
    Browse the repository at this point in the history

  14. chore: migrate to CVL2

    @QGarchery
    QGarchery committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    2c174e0 View commit details
    Browse the repository at this point in the history

  15. refactor: move spec to specs

    @QGarchery
    QGarchery committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    4f704d6 View commit details
    Browse the repository at this point in the history

  16. fix: don't use grounding branch

    @QGarchery
    QGarchery committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    e222bf2 View commit details
    Browse the repository at this point in the history

Commits on Jul 12, 2023

  1. chore: remove prover args

    @QGarchery
    QGarchery committed Jul 12, 2023
    Configuration menu
    Copy the full SHA
    dfc13de View commit details
    Browse the repository at this point in the history

Commits on Nov 30, 2023

  1. refactor: remove munging and move to prover v5

    @QGarchery
    QGarchery committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    578b906 View commit details
    Browse the repository at this point in the history

  2. refactor: remove initialized

    @QGarchery
    QGarchery committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    3b2df7c View commit details
    Browse the repository at this point in the history

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

    @QGarchery
    QGarchery committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    4435355 View commit details
    Browse the repository at this point in the history

  4. chore: remove unused applyHarness.patch

    @QGarchery
    QGarchery committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    8f41cc3 View commit details
    Browse the repository at this point in the history

  5. docs: small improvement of the description

    @QGarchery
    QGarchery committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    d7bbb51 View commit details
    Browse the repository at this point in the history

  6. refactor: update Certora gitignore

    @QGarchery
    QGarchery committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    f885174 View commit details
    Browse the repository at this point in the history

  7. fix: remove unused initialized declaration

    @QGarchery
    QGarchery committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    b030060 View commit details
    Browse the repository at this point in the history

  8. feat: harness rewards distributor

    @QGarchery
    QGarchery committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    477b3c1 View commit details
    Browse the repository at this point in the history

  9. feat: add claimCorrectnessZero rule

    @QGarchery
    QGarchery committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    060f2d5 View commit details
    Browse the repository at this point in the history

  10. feat: add rule correctness one and refactor token

    @QGarchery
    QGarchery committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    7275655 View commit details
    Browse the repository at this point in the history

Commits on Dec 1, 2023

  1. fix: correct hashing of leaves

    @QGarchery
    QGarchery committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    81bc8ce View commit details
    Browse the repository at this point in the history

  2. feat: link MORPHO

    @QGarchery
    QGarchery committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    9c0b000 View commit details
    Browse the repository at this point in the history

  3. feat: add Certora CI

    @QGarchery
    QGarchery committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    a21f7eb View commit details
    Browse the repository at this point in the history

  4. fix: solc binary name for Certora

    @QGarchery
    QGarchery committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    2d4a5fa View commit details
    Browse the repository at this point in the history

  5. fix: install yarn dependencies

    @QGarchery
    QGarchery committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    5ba2124 View commit details
    Browse the repository at this point in the history

Commits on Dec 5, 2023

  1. refactor: remove draft of completeness

    @QGarchery
    QGarchery committed Dec 5, 2023
    Configuration menu
    Copy the full SHA
    bfebc38 View commit details
    Browse the repository at this point in the history

  2. fix: add created to fullyCreatedWellFormed

    @QGarchery
    QGarchery committed Dec 5, 2023
    Configuration menu
    Copy the full SHA
    51af34b View commit details
    Browse the repository at this point in the history

  3. fix: typos in created

    @QGarchery
    QGarchery committed Dec 5, 2023
    Configuration menu
    Copy the full SHA
    d7106d6 View commit details
    Browse the repository at this point in the history

  4. feat: hardcode recursion depth

    @QGarchery
    QGarchery committed Dec 5, 2023
    Configuration menu
    Copy the full SHA
    5de2c8a View commit details
    Browse the repository at this point in the history

Commits on Dec 6, 2023

  1. refactor: simplify root tree

    @QGarchery
    QGarchery committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    6a8aaea View commit details
    Browse the repository at this point in the history

  2. refactor: internalize isEmpty

    @QGarchery
    QGarchery committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    f306d45 View commit details
    Browse the repository at this point in the history

  3. feat: remove summarization of SafeTransferLib

    @QGarchery
    QGarchery committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    2e4d40b View commit details
    Browse the repository at this point in the history

  4. refactor: add back prevRoot

    @QGarchery
    QGarchery committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    91b872b View commit details
    Browse the repository at this point in the history

  5. refactor: remove harness

    @QGarchery
    QGarchery committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    53dec17 View commit details
    Browse the repository at this point in the history

  6. feat: transferredTokens rule

    @QGarchery
    QGarchery committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    b83380a View commit details
    Browse the repository at this point in the history

  7. fix: workflow name RewardsDistributor

    @QGarchery
    QGarchery committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    b319816 View commit details
    Browse the repository at this point in the history

  8. fix: add required assumptions in noClaimAgain and transferredTokens

    @QGarchery
    QGarchery committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    482c728 View commit details
    Browse the repository at this point in the history

  9. fix: total supply requirement on solmate ERC20

    @QGarchery
    QGarchery committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    1ee4190 View commit details
    Browse the repository at this point in the history

  10. docs: add comments and improve readability

    @QGarchery
    QGarchery committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    8cca093 View commit details
    Browse the repository at this point in the history

  11. fix: typo in variable name

    @QGarchery
    QGarchery committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    51b56be View commit details
    Browse the repository at this point in the history

  12. feat: add production server flag to config

    @QGarchery
    QGarchery committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    6ae9d24 View commit details
    Browse the repository at this point in the history

  13. chore: add initial total supply to mocked Morpho token

    @QGarchery
    QGarchery committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    6d8cdec View commit details
    Browse the repository at this point in the history

  14. feat: fist checker prototype

    @QGarchery
    QGarchery committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    60be797 View commit details
    Browse the repository at this point in the history

Commits on Dec 7, 2023

  1. feat: full certificate generation and checker

    @QGarchery
    QGarchery committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    d45d7d5 View commit details
    Browse the repository at this point in the history

  2. chore: use project root directly

    @QGarchery
    QGarchery committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    d51e74c View commit details
    Browse the repository at this point in the history

  3. chore: clean leftover files

    @QGarchery
    QGarchery committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    9492c7f View commit details
    Browse the repository at this point in the history

  4. refactor: use relative import for submodule

    @QGarchery
    QGarchery committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    31688e7 View commit details
    Browse the repository at this point in the history

  5. refactor: profile to separate checker from other tests

    @QGarchery
    QGarchery committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    234500e View commit details
    Browse the repository at this point in the history

  6. Merge pull request #1668 from morpho-org/certora/rewards-checker 

    Certora rewards checker
    @QGarchery
    QGarchery authored Dec 7, 2023
    Configuration menu
    Copy the full SHA
    a9ea31f View commit details
    Browse the repository at this point in the history

  7. refactor: renaming and verifying totals

    @QGarchery
    QGarchery committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    2f409fc View commit details
    Browse the repository at this point in the history

Commits on Dec 8, 2023

  1. docs: add checker documentation

    @QGarchery
    QGarchery committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    2153ffa View commit details
    Browse the repository at this point in the history

  2. fix: value different from 0 in internal nodes

    @QGarchery
    QGarchery committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    e536b19 View commit details
    Browse the repository at this point in the history

  3. refactor: remove created field

    @QGarchery
    QGarchery committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    42dbc54 View commit details
    Browse the repository at this point in the history

  4. docs: add well-formed specification

    @QGarchery
    QGarchery committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    75ca684 View commit details
    Browse the repository at this point in the history

  5. fix: empty root check in checker

    @QGarchery
    QGarchery committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    7aba314 View commit details
    Browse the repository at this point in the history

Commits on Jan 5, 2024

  1. Merge branch 'fix/upgrade-tests' into certora-rewards

    @QGarchery
    QGarchery committed Jan 5, 2024
    Configuration menu
    Copy the full SHA
    652d15b View commit details
    Browse the repository at this point in the history

  2. feat: add an overview of the verification

    @QGarchery
    QGarchery committed Jan 5, 2024
    Configuration menu
    Copy the full SHA
    8b8097f View commit details
    Browse the repository at this point in the history

Commits on Feb 1, 2024

  1. refactor: remove unnecessary hash condition

    @QGarchery
    QGarchery committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    c792819 View commit details
    Browse the repository at this point in the history

Commits on Feb 2, 2024

  1. refactor: remove unnecessary packages

    @QGarchery
    QGarchery committed Feb 2, 2024
    Configuration menu
    Copy the full SHA
    f5e7dc1 View commit details
    Browse the repository at this point in the history

Commits on Mar 6, 2024

  1. feat: split no claim again rule

    @QGarchery
    QGarchery committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    ac2af4c View commit details
    Browse the repository at this point in the history

  2. feat: add claim twice rule

    @QGarchery
    QGarchery committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    48fb135 View commit details
    Browse the repository at this point in the history

  3. feat: check sum of values for internal nodes

    @QGarchery
    QGarchery committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    9f51cb2 View commit details
    Browse the repository at this point in the history

  4. refactor: require well formed on the path only

    @QGarchery
    QGarchery committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    1c33193 View commit details
    Browse the repository at this point in the history

  5. refactor: well formed path with a loop

    @QGarchery
    QGarchery committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    9736d1c View commit details
    Browse the repository at this point in the history

  6. refactor: require once in loop

    @QGarchery
    QGarchery committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    aff7755 View commit details
    Browse the repository at this point in the history

  7. chore: increase loop iteration to 4

    @QGarchery
    QGarchery committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    ed73f4b View commit details
    Browse the repository at this point in the history

  8. chore: loop iter to 4 in merkle tree

    @QGarchery
    QGarchery committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    527a8c6 View commit details
    Browse the repository at this point in the history

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

    @QGarchery
    QGarchery committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    adb56a4 View commit details
    Browse the repository at this point in the history

Commits on Mar 11, 2024

  1. refactor: remove unnecessary require invariant

    @QGarchery
    QGarchery committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    3b0b13f View commit details
    Browse the repository at this point in the history

  2. docs: add comments

    @QGarchery
    QGarchery committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    48e40e8 View commit details
    Browse the repository at this point in the history

  3. refactor: variable renaming

    @QGarchery
    QGarchery committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    823f623 View commit details
    Browse the repository at this point in the history

  4. refactor: use structs in merkle tree lib

    @QGarchery
    QGarchery committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    38276f2 View commit details
    Browse the repository at this point in the history

  5. fix: new interface for node creation

    @QGarchery
    QGarchery committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    f5daa10 View commit details
    Browse the repository at this point in the history

  6. feat: check increasing claim amounts

    @QGarchery
    QGarchery committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    b6f4f2a View commit details
    Browse the repository at this point in the history

  7. refactor: remove unnecessary root of the Merkle tree

    @QGarchery
    QGarchery committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    07db98d View commit details
    Browse the repository at this point in the history

  8. docs: example of list of proofs

    @QGarchery
    QGarchery committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    ef54f35 View commit details
    Browse the repository at this point in the history

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

    @QGarchery
    QGarchery committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    223f718 View commit details
    Browse the repository at this point in the history

  10. feat: check update root storage change

    @QGarchery
    QGarchery committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    0b41773 View commit details
    Browse the repository at this point in the history

  11. fix: update root is not envfree

    @QGarchery
    QGarchery committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    8a3aed9 View commit details
    Browse the repository at this point in the history

Commits on Mar 12, 2024

  1. refactor: restrict read permission

    @QGarchery
    QGarchery committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    0ffd207 View commit details
    Browse the repository at this point in the history

  2. docs: node is the root candidate

    @QGarchery
    QGarchery committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    8ad06d2 View commit details
    Browse the repository at this point in the history

  3. refactor: clarify verification

    @QGarchery
    QGarchery committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    226d508 View commit details
    Browse the repository at this point in the history

Commits on Mar 15, 2024

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

    @QGarchery
    QGarchery committed Mar 15, 2024
    Configuration menu
    Copy the full SHA
    821c8ec View commit details
    Browse the repository at this point in the history