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

fix(spec): agreement for multiple heights #749

Merged
merged 1 commit into from
Jan 13, 2025
Merged

fix(spec): agreement for multiple heights #749

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
28 changes: 20 additions & 8 deletions specs/consensus/quint/statemachineAsync.qnt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ export driver.*
import consensus.* from "./consensus"
export consensus.*
import votekeeper.* from "./votekeeper"
import extraSpells.* from "./spells/extra"
josef-widder marked this conversation as resolved.
Show resolved Hide resolved

const validators: Set[Address]
const validatorSet: Address -> Weight
Expand Down Expand Up @@ -65,10 +66,13 @@ action unchangedAll = all {
_hist' = _hist
}

/// Any two processes agree in the consensus instances in which they both have already decided
val AgreementInv = tuples(Correct, Correct).forall(p =>
(system.get(p._1).es.chain != List() and system.get(p._2).es.chain != List())
implies
system.get(p._1).es.chain[0] == system.get(p._2).es.chain[0])
val numDecidedInstances = min( system.get(p._1).es.chain.length(),
system.get(p._2).es.chain.length())
to(0, numDecidedInstances-1).forall(i =>
system.get(p._1).es.chain[i] == system.get(p._2).es.chain[i])
)

// Actions
action init = all {
Expand Down Expand Up @@ -224,13 +228,21 @@ action deliverSomeCertificate(v: Address) : bool = all {
}


// deliver a message or a certiciate.
// deliver a message or a certificate.
// Take it from the network buffer of from the faulty set and put it into the incoming sets
action deliver(v: Address) : bool = any {
nondet prop = oneOf(propBuffer.get(v).union(AllFaultyProposals))
deliverProposal(v, prop),
nondet vote = oneOf(voteBuffer.get(v).union(AllFaultyVotes))
deliverVote(v, vote),
val props = propBuffer.get(v).union(AllFaultyProposals)
all{
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is a deliverSomeProposal action in this file, with the same issue: it does not test if there is a proposal buffer to deliver.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This method, however, does not delivery faulty proposals.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The method is used in:

  • ./tests/decideForPastRound/decideForPastRoundrun.qnt
  • tests/line42/line42run.qnt

props.size() > 0,
nondet prop = oneOf(props)
deliverProposal(v, prop),
},
val votes = voteBuffer.get(v).union(AllFaultyVotes)
all {
votes.size() > 0,
nondet vote = oneOf(votes)
deliverVote(v, vote),
},
deliverSomeCertificate(v), // we might do fault injection here. But faulty nodes cannot
// totally make up certificates. They cannot forge messages to look
// like being sent by correct nodes
Expand Down
Loading