[Halmos] Setup for verification and first invariants #675

QGarchery · 2024-04-02T15:35:45Z

Todo:

use test profile for Halmos
remove installation of setuptools when no longer necessary
~~look at certora timeout invariants~~ (all of them are timing out because of non linear math, which Halmos can't help with)
look at certora that could be quick win invariants

test/forge/HalmosTest.sol

Halmos: Few more basic rules

test/forge/HalmosTest.sol

feat: add Halmos test

7d7bfa9

QGarchery added the verif Modifies the formal verification label Apr 2, 2024

QGarchery self-assigned this Apr 2, 2024

QGarchery added 20 commits April 2, 2024 17:36

fix: add foundry to CI for Halmos

7aebf25

chore: no timeout on counterexample

6667451

chore: remove halmos-cheatcode

bb2f9af

chore: add back halmos-cheatcodes with https

b1445fa

fix: test fee

787e154

fix: use distinct args for dynamic types

725c9ee

chore: simpler setup

7a71b62

feat: pass all market params

8489407

feat: generalize token for flashLoan

49a1ca0

fix: svm create newFee

b6f96c7

feat: borrow less than supply and last updated invariant

3e546e5

fix: lastUpdate name

2b69597

Merge remote-tracking branch 'origin/main' into halmos/setup

0c94fc1

chore: specify python-version

72d70b2

chore: bump action setup python

ff1427a

chore: add setuptools

fd6adac

feat: symbolic LLTV

a71df2d

chore: remove setuptools

62fc02e

feat: check lltv smaller than WAD

6ef5c7a

refactor: use test profile for Halmos

c29c3bc

QGarchery marked this pull request as ready for review April 19, 2024 13:08

QGarchery changed the title ~~[Halmos] Setup for verification~~ [Halmos] Setup for verification and first invariants Apr 19, 2024

docs: add description of invariants

5a41d5d

QGarchery requested a review from MathisGD April 19, 2024 13:42

MathisGD reviewed Apr 22, 2024

View reviewed changes

test/forge/HalmosTest.sol Outdated Show resolved Hide resolved

MathisGD reviewed Apr 22, 2024

View reviewed changes

test/forge/HalmosTest.sol Outdated Show resolved Hide resolved

MathisGD and others added 8 commits April 22, 2024 12:26

test: halmost irm and ltv can't be disabled

1221cce

test: halmos nonce can't decrease

46c6f46

test: halmos fix nonceCannotDecrease

ba6386e

test: halmos add two little rules

a3bfab0

Merge pull request #677 from morpho-org/halmos/more-rules

95de5e5

Halmos: Few more basic rules

refactor: simplify setup

53f3e28

refactor: merge dispatch borrow-withdraw

4b96f6a

test: halmos document check_idToMarketParamsForCreatedMarketCannotChange

dc2c664

MathisGD reviewed Apr 22, 2024

View reviewed changes

test/forge/HalmosTest.sol Outdated Show resolved Hide resolved

MathisGD and others added 4 commits April 22, 2024 15:36

test: (halmos) fix check_nonceCannotDecrease

da3ebee

refactor: simplify setup, and generalize id

0bdca52

refactor: make id completely symbolic

0618762

refactor: move Halmos test to its own folder

5a79282

QGarchery requested a review from MathisGD April 23, 2024 08:56

MathisGD reviewed Apr 23, 2024

View reviewed changes

test/forge/HalmosTest.sol Outdated Show resolved Hide resolved

MathisGD approved these changes Apr 23, 2024

View reviewed changes

MerlinEgalite approved these changes Apr 23, 2024

View reviewed changes

MerlinEgalite merged commit d36719d into main Apr 23, 2024
16 checks passed

MerlinEgalite deleted the halmos/setup branch April 23, 2024 09:15

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Halmos] Setup for verification and first invariants #675

[Halmos] Setup for verification and first invariants #675

QGarchery commented Apr 2, 2024 •

edited

Loading

[Halmos] Setup for verification and first invariants #675

[Halmos] Setup for verification and first invariants #675

Conversation

QGarchery commented Apr 2, 2024 • edited Loading

QGarchery commented Apr 2, 2024 •

edited

Loading