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] Liquidate buffer, with executable code #708

Closed
wants to merge 19 commits into from
Closed

[Certora] Liquidate buffer, with executable code #708

wants to merge 19 commits into from

Conversation

QGarchery
Copy link
Contributor

No description provided.

@QGarchery QGarchery self-assigned this Dec 9, 2024
@QGarchery QGarchery mentioned this pull request Dec 9, 2024
Closed
QGarchery and others added 17 commits December 10, 2024 12:30
@QGarchery
fix: repaid shares computation
712e6a2
@QGarchery
fix: stronger require
6b6a8c7
@QGarchery
chore: try medium timeout 20
914c244
@QGarchery
chore: one assert
47d7558
@QGarchery
feat: more summarization
9a6b160
@Bilogweb3 @QGarchery
Update README.md
2cb3597 
Signed-off-by: Bilog WEB3 <155262265+Bilogweb3@users.noreply.github.com>
@QGarchery
feat: add flashLoan input validation
7df7a63
@MathisGD @QGarchery
docs: improve wording of assumptions for liveness
1399ed2
@MathisGD @QGarchery
docs: wording
3fb8394
@MathisGD @QGarchery
chore: remove bytecode hash from compilation
0efe836
@MathisGD @QGarchery
chore: explicitly turn on the optimizer
4f9b5ea 
Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>
@adhusson @QGarchery
build: add evm_version
e88a9bf
@MathisGD @QGarchery
Update foundry.toml
02820d4 
Co-authored-by: Quentin Garchery <garchery.quentin@gmail.com>
Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>
@QGarchery
fix : rename harness to helpers
e2e9700
@QGarchery
fix: rename harness related paths
cfb7827
@QGarchery
chore: rename harness folder to helpers
c27a99d
@QGarchery
Merge branch 'main' into certora/exec-liquidate-buffer
eb75586
@QGarchery QGarchery changed the base branch from main to certora/liquidate-buffer January 16, 2025 13:09
@QGarchery QGarchery changed the base branch from certora/liquidate-buffer to main January 16, 2025 13:09
@QGarchery
Copy link
Contributor Author

It seems very difficult to make this verification go though. Here is an example of such run, but deviating a little bit from it seems to cause a timeout. Also this run requires some heavy modifications:

  • passing the LIF to the liquidate function
  • munging to not update the value of repaidAssets
  • munging to comment out _accrueInterest (even though it should be skipped given the assumptions)
  • munging to require that no bad debt is realized (even though it should be provable by the assumptions)

For these reasons, it seems prefereable to do #710

@QGarchery QGarchery closed this Jan 29, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@QGarchery QGarchery

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@QGarchery @Bilogweb3 @MathisGD @adhusson