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

feat(spec): WIP: Draft of Quint reset protocol #174

Merged
merged 41 commits into from
Apr 25, 2024
Merged

feat(spec): WIP: Draft of Quint reset protocol #174

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
41 commits
Select commit Hold shift + click to select a range
cd13283
types for reset protocol spec
josef-widder Mar 21, 2024
b464fb4
normal flow of reset
josef-widder Mar 22, 2024
a0045ae
valset updates
josef-widder Mar 22, 2024
dee7df4
I need to debug, but we hit a reset condition and reset
josef-widder Mar 22, 2024
7bffc4b
off 1
josef-widder Mar 22, 2024
bd6e3fa
added multiple registrations per L1 block
josef-widder Mar 22, 2024
20aba2b
more concrete on L1 acceptance ruls
josef-widder Mar 22, 2024
6a2911c
epoch in reset blocj (was height before)
josef-widder Mar 26, 2024
b3627ef
added TODOs
josef-widder Mar 26, 2024
b81ba1a
changed towards staged/unstaged handling (rather than nextValset)
josef-widder Mar 27, 2024
f565144
comments and fixes
josef-widder Mar 27, 2024
14ef579
transformed proofs into sets
josef-widder Mar 29, 2024
f85f505
added a test with reset scenario
josef-widder Mar 29, 2024
e2e99a8
small fixes before walkthrough
josef-widder Apr 2, 2024
65a2981
moved test back for simplicity
josef-widder Apr 2, 2024
5e2baec
fixes during meeting
josef-widder Apr 2, 2024
f70094b
reorganized test again
josef-widder Apr 5, 2024
0e867ed
Update specs/quint/specs/reset.qnt
josef-widder Apr 17, 2024
767b795
renambed variables to match Matan's
josef-widder Apr 17, 2024
9fa2d74
Merge branch 'josef/resetQuint' of github.com:informalsystems/malachi…
josef-widder Apr 17, 2024
ad6969b
L1 height to time
josef-widder Apr 17, 2024
bcbbc07
Update specs/quint/specs/reset.qnt
josef-widder Apr 17, 2024
9ae5624
growing forkID propertyo
josef-widder Apr 17, 2024
4566539
Merge branch 'josef/resetQuint' of github.com:informalsystems/malachi…
josef-widder Apr 17, 2024
0bacc36
types OK, need to debug
josef-widder Apr 17, 2024
1ff3df2
EVE epochs fixed, I believe
josef-widder Apr 18, 2024
fb9a94e
added comments after sync meeting with Daniel
josef-widder Apr 18, 2024
375f6fe
added invariant from PR discussion
josef-widder Apr 19, 2024
48e83e7
removed duplicate registrations
josef-widder Apr 19, 2024
abeb9de
fixed a bug in the heighest_staged
josef-widder Apr 19, 2024
78dbb23
invalid registration handling
josef-widder Apr 22, 2024
3b5a6ab
added previously deleted L2 blocks
josef-widder Apr 22, 2024
e263679
at most one rollback per forkID
josef-widder Apr 22, 2024
dcb488d
L1 block computation based on current staleness + noStaleWithProof
josef-widder Apr 23, 2024
ba75cf4
cleanup
josef-widder Apr 23, 2024
a71ccb8
added temporal block properties
josef-widder Apr 24, 2024
8569a44
spellcheck
josef-widder Apr 24, 2024
1658027
spell
josef-widder Apr 24, 2024
dde304d
Merge branch 'main' into josef/resetQuint
josef-widder Apr 24, 2024
87502e8
added TODO
josef-widder Apr 24, 2024
5fb76fc
Merge branch 'josef/resetQuint' of github.com:informalsystems/malachi…
josef-widder Apr 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Loading
Loading