Update quint spec #1333
Update quint spec #1333
Conversation
| import defs.* from "../defs" | ||
| import option.* from "../option" | ||
| import replica( | ||
| N = 6, |
There was a problem hiding this comment.
I purposely removed these changes because they were never used anywhere (and just duplicate info that was already captured in CORRECT/FAULTY).
There was a problem hiding this comment.
They are different. N and F are protocol parameters; they should not be derived from CORRECT/FAULTY in formal verification code. For example, if we do not use faulty replicas in the configuration at all, is F = 0? That is why all files were initially named nNfFbB (e.g., n6f1b0.qnt): F- the maximum number of faulty nodes when the protocol still works, B was the real number of faulty replicas in the configuration. The same with N: what if I want to test that the protocol works for three replicas without faulty? then N = 3 and F = 0. L and Q will not be computed incorrectly for that case if CORRECT/FAULT are used.
pipeline/minimmit/quint/replica.qnt
Outdated
| L + Q > N + F, | ||
|
|
||
| 2*F + 1 <= L, | ||
| L <= N - 3*F, |
There was a problem hiding this comment.
Might be nice to have comments for all of these why they are necessary. I couldn't understand why this one is necessary (?)
There was a problem hiding this comment.
These two were the main points of our discussions. But it just follows from inequation if we introduce L from [ 2F+1, N-3F]:
(5*F+1 <= N) => (2*F + 3*F + 1<= N) => (2*F + 1 <= N - 3*F)
if N=5*F+1 then 2*F+1=L=N-3*F
pipeline/minimmit/quint/replica.qnt
Outdated
|
|
||
| 4*F + 1 <= Q, | ||
| Q <= N - F, | ||
| Q > L |
There was a problem hiding this comment.
Q >= L technically I think. For example for N=1, Q=L=1
There was a problem hiding this comment.
Correct, but we actually do not need this. I removed it.
pipeline/minimmit/quint/replica.qnt
Outdated
| L <= N - 3*F, | ||
|
|
||
| 4*F + 1 <= Q, | ||
| Q <= N - F, |
There was a problem hiding this comment.
I think you need to keep this invariant, right? Otherwise Q=N could be valid, which would prevent finalization from occurring? Or is Q = N - F and F = 2F+1 hardcoded somewhere?
There was a problem hiding this comment.
Yes, they are in the same file -
monorepo/pipeline/minimmit/quint/replica.qnt
Lines 22 to 23 in d737738
pipeline/minimmit/quint/replica.qnt
Outdated
| 4*F + 1 <= Q, | ||
| Q <= N - F, | ||
| Q > L | ||
| 2*L <= (N - F) + 1, // Liveness guard, prevents equivocation stall. |
There was a problem hiding this comment.
Nit: 2*L <= Q + 1 perhaps?
Codecov Report✅ All modified and coverable lines are covered by tests. @@ Coverage Diff @@
## main #1333 +/- ##
==========================================
- Coverage 91.37% 91.32% -0.06%
==========================================
Files 251 265 +14
Lines 63583 66018 +2435
==========================================
+ Hits 58097 60288 +2191
- Misses 5486 5730 +244 see 52 files with indirect coverage changes Continue to review full report in Codecov by Sentry.
🚀 New features to boost your workflow:
|
This PR updates the spec in quint