Update Minimmit spec #1456
Update Minimmit spec #1456
Conversation
|
@BrendanChou I created an issue listing differences between the spec and the paper. I believe it should be resolved in the paper, in the repo, or in both (partially). Otherwise, the paper and the repo's spec are significantly different, so it is unclear whether the paper theoretically justifies anything about the repo's spec. |
… into denis/quint-upd-2
pipeline/minimmit/quint/replica.qnt
Outdated
| pure def is_view_notarized(view: ViewNumber, certificates: Set[Certificate]): bool = or { | ||
| view == GENESIS_VIEW, | ||
| certificates.exists(v => v.kind == NotarizationKind and v.view == view), | ||
| // TODO verify this assumption |
There was a problem hiding this comment.
Prefer not to keep TODOs in here.
I don't think a finalization certificate must exist if view is only notarized?
There was a problem hiding this comment.
I removed TODO. It can be a case when a slow replica receives a finalization certificate first and then receives other messages. We discussed that with @BrendanChou and I also created an issue #1491
pipeline/minimmit/quint/replica.qnt
Outdated
| not(is_view_notarized(view, certificates)), | ||
| not(was_finalized) and now_finalized, | ||
|
|
||
| val was_finalized = is_view_finalized(view, certificates) or is_view_finalized_votes(view, store, block) |
There was a problem hiding this comment.
nit: prefer notarized before finalized
pipeline/minimmit/quint/replica.qnt
Outdated
| val was_finalized = is_view_finalized(view, certificates) or is_view_finalized_votes(view, store, block) | ||
| val was_notarized = is_view_notarized(view, certificates) or is_view_notarized_votes(view, store, block) | ||
|
|
||
| val now_finalized = is_view_finalized_votes(view, new_store, block) |
There was a problem hiding this comment.
nit: prefer notarized before finalized
pipeline/minimmit/quint/replica.qnt
Outdated
|
|
||
| or { | ||
| cert.kind == FinalizationKind and cert.signatures.size() >= L and not(is_view_finalized(cert.view, certificates)), | ||
| cert.kind == NotarizationKind and cert.signatures.size() >= M and not(is_view_notarized(cert.view, certificates)), |
There was a problem hiding this comment.
nit: notarized before finalized
Codecov Report✅ All modified and coverable lines are covered by tests. @@ Coverage Diff @@
## main #1456 +/- ##
==========================================
+ Coverage 91.70% 92.06% +0.35%
==========================================
Files 275 283 +8
Lines 69443 73182 +3739
==========================================
+ Hits 63685 67377 +3692
- Misses 5758 5805 +47 see 89 files with indirect coverage changes Continue to review full report in Codecov by Sentry.
🚀 New features to boost your workflow:
|
This PR updates the Quint spec of Minimmit