Skip to content

Commit

Permalink
feat(spec): WIP: Draft of Quint reset protocol (#174)
Browse files Browse the repository at this point in the history
* types for reset protocol spec

* normal flow of reset

* valset updates

* I need to debug, but we hit a reset condition and reset

* off 1

* added multiple registrations per L1 block

* more concrete on L1 acceptance ruls

* epoch in reset blocj (was height before)

* added TODOs

* changed towards staged/unstaged handling (rather than nextValset)

* comments and fixes

* transformed proofs into sets

* added a test with reset scenario

* small fixes before walkthrough

* moved test back for simplicity

* fixes during meeting

* reorganized test again

* Update specs/quint/specs/reset.qnt

Co-authored-by: Anca Zamfir <ancazamfir@users.noreply.github.com>

* renambed variables to match Matan's

* L1 height to time

* Update specs/quint/specs/reset.qnt

Co-authored-by: Anca Zamfir <ancazamfir@users.noreply.github.com>

* growing forkID propertyo

* types OK, need to debug

* EVE epochs fixed, I believe

* added comments after sync meeting with Daniel

* added invariant from PR discussion

* removed duplicate registrations

* fixed a bug in the heighest_staged

* invalid registration handling

* added previously deleted L2 blocks

* at most one rollback per forkID

* L1 block computation based on current staleness + noStaleWithProof

* cleanup

* added temporal block properties

* spellcheck

* spell

* added TODO

---------

Co-authored-by: Anca Zamfir <ancazamfir@users.noreply.github.com>
  • Loading branch information
josef-widder and ancazamfir authored Apr 25, 2024
1 parent a1a5c5f commit 67c8637
Show file tree
Hide file tree
Showing 2 changed files with 725 additions and 0 deletions.
Loading

0 comments on commit 67c8637

Please sign in to comment.