Skip to content

(old-2) Certora verification of the DLL #97

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
Closed
wants to merge 117 commits into from
Closed

(old-2) Certora verification of the DLL #97

wants to merge 117 commits into from

Conversation

@QGarchery
Copy link
Collaborator

@QGarchery QGarchery commented Dec 16, 2022

No description provided.

@QGarchery
feat: initial sanity test
48f833e
@QGarchery
fix: add DLL contract, prevent errors removing munged by accident
942c2bb
@QGarchery
feat: circular definitions
6ffb1bf
@QGarchery
feat: isForwardLinked in solidity
e4b5f1e
@QGarchery
feat: decreasingly sorted and linked to 0 invariants
6e62df0
@QGarchery
feat: length in the code, preserve remove check
883f4f1
@QGarchery
feat: prove zeroPrev preserved by remove
9c176cf
@QGarchery
refactor: invariants with tip not 0
c8e9c93
@QGarchery
feat: add definitions in the specification
4ca77d6
@QGarchery
feat: proof tailNextIsZero and linkedIsInDLL
59182f3
@QGarchery
feat: add hook to require invariant inside insertSorted
5a0eebc
@QGarchery
feat: ghost variable to track the element to insert in front of
6767673
@QGarchery
refactor: use public variable instead of hook
4ce152b
@QGarchery
feat: insertAfter
1a3684a
@QGarchery
feat: proved linkedIsInDLL
3a2cd60
@QGarchery
feat: proof of twoWayLinked
96c67bd
@QGarchery
feat: prove zeroIsNotLinked
9834960
@QGarchery
refactor: added isEmpty definition
beb0c50
@QGarchery
feat: proof of tailNextAndValue
a7f6218
@QGarchery
feat: proof of noPrevIsHead
26c4850
@QGarchery
feat: proof of neNextisTailPreservedInsertSorted
2bbea7d
@QGarchery
refactor: cleaning specification and removed constructor
7e160aa
@QGarchery
fix: length computation
5703773
@QGarchery
fix: temporary CVL error, revert munged makefile
6595504
@QGarchery
refactor: add munging for DLL with FIFO
682dba5
@QGarchery
feat: prove simple DLLisDecrSorted
b1a6b90
@QGarchery
feat: prove isForwardLinked preserved remove
4351413
@QGarchery
feat: finish forward link proof
3a6e1d3
@QGarchery
feat: bump number of loops from 3 to 7
efe0239
@QGarchery
feat: prove reachability of every element inside the list
f4c7a01
QGarchery and others added 19 commits December 16, 2022 20:15
@QGarchery
feat: memoize size in the 3-heap
ffb4b7a
@QGarchery
fix: fix condition to skip restoring the sorting
6a3119d
@QGarchery
fix: add computed to the size in remove
4fd6c41
@MathisGD @QGarchery
chore: use foundry.toml instead of Makefile
4900dea
@MathisGD @QGarchery
chore: add newline at the end of the file
fa9e49c
@MathisGD @QGarchery
chore: set solc version
0c1a298
@MathisGD @QGarchery
doc: update
1f87cd8
@Rubilmax @QGarchery
Make the CI fail when a test fails
86388ca
@MathisGD @QGarchery
test: heap invariant
b8c6faa
@MathisGD @QGarchery
test: refactor heap invariant testing
91c899c
@MathisGD @QGarchery
test: use ConcreteHeap contracts
464dcf9
@MathisGD @QGarchery
test: first invariants 3-heap
b3487c9
@MathisGD @QGarchery
test: refactor heap testing
c903dc3
@MathisGD @QGarchery
test: improve heap invariant testing
b8f4012
@MathisGD @QGarchery
test: reduce the depth for invariant testing
dbe6468
@MathisGD @QGarchery
test: modernize test dependancies
4c02c6d
@MathisGD @QGarchery
chore: rename test files
cf55387
@MathisGD @QGarchery
chore: remove old random test files
b8d586c
@MathisGD @QGarchery
chore: don't format deleted files in pre-commit
27d29bf
@QGarchery QGarchery mentioned this pull request Dec 16, 2022
Closed
@QGarchery QGarchery self-assigned this Dec 16, 2022
@QGarchery QGarchery mentioned this pull request Dec 19, 2022
Merged
@QGarchery QGarchery changed the title Certora verification of the DLL (old-2) Certora verification of the DLL Dec 19, 2022
@QGarchery QGarchery closed this Dec 19, 2022
@QGarchery
Copy link
Collaborator Author

QGarchery commented Dec 19, 2022

See #100 instead

@QGarchery QGarchery deleted the test/certora-2 branch May 30, 2024 21:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@MerlinEgalite MerlinEgalite Awaiting requested review from MerlinEgalite

@MathisGD MathisGD Awaiting requested review from MathisGD

Assignees

@QGarchery QGarchery

Labels

🧮 certora

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@QGarchery @MathisGD @Rubilmax