Skip to content

Commit

Permalink
spec/quint: fix comments, types, identation
Browse files Browse the repository at this point in the history
  • Loading branch information
@cason
cason committed Nov 22, 2024
1 parent 7fcd210 commit ad64a86
Show file tree
Hide file tree
Showing 4 changed files with 73 additions and 76 deletions.
132 changes: 66 additions & 66 deletions specs/quint/specs/blocksync/blocksyncClient.qnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,19 +47,19 @@ module blocksyncClient {
/// Auxiliary function to iterate over the received status messages
pure def updatePeerStatus (ps: Address -> BlockRange, msgs: Set[StatusMsg]) : Address -> BlockRange =
msgs.fold(ps, (newStatus , msg) =>
if (newStatus.get(msg.peer).top < msg.top) // TODO: think about base?
newStatus.put(msg.peer, {base: msg.base, top: msg.top})
else
newStatus
if (newStatus.get(msg.peer).top < msg.top) // TODO: think about base?
newStatus.put(msg.peer, {base: msg.base, top: msg.top})
else
newStatus
)

/// inform the synchronizer that consensus has entered height h
pure def syncNewHeight (s: BsyncClient, h: Height) : BsyncClient =
if (h <= s.height)
s
s
else
{ ... s, height: h,
openRequests: s.openRequests.filter(req => req.height >= h)}
{ ... s, height: h,
openRequests: s.openRequests.filter(req => req.height >= h)}

/// returned by the synchronizer: sync is the new state, so is the output towards
/// the consensus driver, req are messages sent towards peers/servers
Expand All @@ -70,30 +70,30 @@ module blocksyncClient {
}

/// We have received a certificate. now we need to issue the
/// corresponding block request and generate a certificate output.
/// corresponding block request and generate a certificate output.
pure def syncHandleCertificate (s: BsyncClient, cert: Set[Vote], peer: str ) : ClientResult =
val blockReq = { client: s.id,
server: peer,
rtype: SyncBlock,
height: s.height}
{ sync: {...s, openRequests: Set(blockReq)}, // If we have parallelization we need to be more precise here
so: SOCertificate(cert),
req: Some(blockReq)}
val blockReq = {client: s.id,
server: peer,
rtype: SyncBlock,
height: s.height}
{ sync: {...s, openRequests: Set(blockReq)}, // If we have parallelization we need to be more precise here
so: SOCertificate(cert),
req: Some(blockReq)}

/// we have received a block. now we need to generate a block output
/// we have received a block. now we need to generate a block output
pure def syncHandleBlock (s: BsyncClient, p: Proposal) : ClientResult =
{ sync: {...s, openRequests: Set(), // If we have parallelization we need to remove one element,
lastSyncedHeight: s.height }, // blockheight,
so: SOBlock(p),
req: None}
{ sync: {...s, openRequests: Set(), // If we have parallelization we need to remove one element,
lastSyncedHeight: s.height }, // blockheight,
so: SOBlock(p),
req: None}

/// we have received a blockstore entry (block and certificate).
/// now we need to generate a block output
/// now we need to generate a block output
pure def syncHandleBlockStoreEntry (s: BsyncClient, b: BlockStoreEntry) : ClientResult =
{ sync: {...s, openRequests: Set(), // If we have parallelization we need to remove one element,
lastSyncedHeight: s.height }, // blockheight,
so: SOBlockStoreEntry(b),
req: None}
{ sync: {...s, openRequests: Set(), // If we have parallelization we need to remove one element,
lastSyncedHeight: s.height }, // blockheight,
so: SOBlockStoreEntry(b),
req: None}

/// step of a client:
/// 1. update peer statuses, 2. if there is no open request, request something
Expand All @@ -102,48 +102,48 @@ module blocksyncClient {
val newPeerStates = updatePeerStatus(s.peerStatus, s.statusMsgs)
val newS = { ...s, peerStatus: newPeerStates}
if (s.lastSyncedHeight >= s.height)
// nothing to do
{ sync: newS,
so: SONoOutput,
req: None}
// nothing to do
{ sync: newS,
so: SONoOutput,
req: None}
else
val goodPeers = s.peerStatus.keys().filter(p => newPeerStates.get(p).base <= s.height
and s.height <= newPeerStates.get(p).top )
if (goodPeers.size() > 0)
if (s.openRequests.size() == 0)
// we start the sync "round" by asking for a certificate
val req = { client: s.id,
server: goodPeers.fold("", (acc, i) => i), //chooseSome(),
rtype: if (fullEntries)
SyncBlockStoreEntry
else
SyncCertificate,
height: s.height}
{ sync: {... newS, openRequests: s.openRequests.union(Set(req))},
so: SONoOutput,
req: Some(req)
}
else
// we issued a request before, let's see whether there is a response
if (s.responseMsgs.size()> 0)
val resp = s.responseMsgs.fold(emptyResponseMsg, (acc, i) => i) //chooseSome() // in the future there might be parallelization
val ns = {... newS, responseMsgs: newS.responseMsgs.exclude(Set(resp))}
match resp.response {
| RespBlock(prop) => syncHandleBlock(newS, prop)
| RespCertificate(cert) => syncHandleCertificate(newS, cert, goodPeers.fold("", (s,x) => x))
| RespBlockStoreEntry(b) => syncHandleBlockStoreEntry(ns, b)
}
else
// I don't have response
// this might be timeout logic
{ sync: newS,
so: SONoOutput,
req: None}
else
// no peers
{ sync: newS,
so: SONoOutput,
req: None}
val goodPeers = s.peerStatus.keys().filter(p => newPeerStates.get(p).base <= s.height
and s.height <= newPeerStates.get(p).top )
if (goodPeers.size() > 0)
if (s.openRequests.size() == 0)
// we start the sync "round" by asking for a certificate
val req = { client: s.id,
server: goodPeers.fold("", (acc, i) => i), //chooseSome(),
rtype: if (fullEntries)
SyncBlockStoreEntry
else
SyncCertificate,
height: s.height}
{ sync: {... newS, openRequests: s.openRequests.union(Set(req))},
so: SONoOutput,
req: Some(req)
}
else
// we issued a request before, let's see whether there is a response
if (s.responseMsgs.size()> 0)
val resp = s.responseMsgs.fold(emptyResponseMsg, (acc, i) => i) //chooseSome() // in the future there might be parallelization
val ns = {... newS, responseMsgs: newS.responseMsgs.exclude(Set(resp))}
match resp.response {
| RespBlock(prop) => syncHandleBlock(newS, prop)
| RespCertificate(cert) => syncHandleCertificate(newS, cert, goodPeers.fold("", (s,x) => x))
| RespBlockStoreEntry(b) => syncHandleBlockStoreEntry(ns, b)
}
else
// I don't have response
// this might be timeout logic
{ sync: newS,
so: SONoOutput,
req: None}
else
// no peers
{ sync: newS,
so: SONoOutput,
req: None}

/// step of a client upon timeout: We send the same request to a different server
// FIXME: what to do if goodPeers is empty?
Expand Down
5 changes: 1 addition & 4 deletions specs/quint/specs/blocksync/bsyncStatemachine.qnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,15 +63,12 @@ module bsyncStatemachine {
)

/// Every request will eventually terminate.
/// We cannot verify it.
/// We cannot currently verify it with Apalache.
temporal terminationRequest =
bsyncClients.keys().forall(c =>
always (bsyncClients.get(c).openRequests.forall(req =>
eventually (not(bsyncClients.get(c).openRequests.contains(req))))))




//
// Actions
//
Expand Down
6 changes: 3 additions & 3 deletions specs/quint/specs/blocksync/bsyncWithConsensus.qnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,8 @@ module bsyncWithConsensus {
//
// With the default `init` action, it is unlikely to observe this scenario,
// even with 200 steps (around 30 minutes) execution:
// $ quint run --invariant anyClientOuputWitness bsyncWithConsensus.qnt
val anyClientOuputWitness = Correct.forall(p =>
// $ quint run --invariant anyClientOutputWitness bsyncWithConsensus.qnt
val anyClientOutputWitness = Correct.forall(p =>
system.get(p).incomingSyncCertificates == Set())

//
Expand Down Expand Up @@ -147,7 +147,7 @@ module bsyncWithConsensus {
.then(all{unchangedAll, syncDeliverResp("v4")})
.then(syncStepClient("v4", putSyncOutputIntoNode, false)) // ask for block and give certificate to node
.expect(system.get("v4").incomingSyncCertificates.size() > 0)
.expect(not(anyClientOuputWitness))
.expect(not(anyClientOutputWitness))
.then(all{unchangedAll, syncDeliverReq("v2")})
.then(all{unchangedAll, syncStepServer("v2")})
.then(all{unchangedAll, syncDeliverResp("v4")})
Expand Down
6 changes: 3 additions & 3 deletions specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,11 +27,11 @@ module bsyncWithMockedConsensus {
/// received a certificate, or a block, or both (a block store entry).
//
// Use the `initSetup` initialization to have faster runs:
// $ quint run --invariant anyClientOuputWitness bsyncWithMockedConsensus.qnt --init initSetup --seed=0x131cbef6acef78
// $ quint run --invariant anyClientOutputWitness bsyncWithMockedConsensus.qnt --init initSetup --seed=0x131cbef6acef78
//
// With the default `init` action more steps are required, e.g.:
// $ quint run --invariant anyClientOuputWitness bsyncWithMockedConsensus.qnt --max-steps 100 --seed=0x4e9afa1aeb815
val anyClientOuputWitness = Correct.forall(p =>
// $ quint run --invariant anyClientOutputWitness bsyncWithMockedConsensus.qnt --max-steps 100 --seed=0x4e9afa1aeb815
val anyClientOutputWitness = Correct.forall(p =>
outputs.get(p).length() > 0 implies
outputs.get(p).foldl(Set(), (s, x) => s.union(Set(x))).forall(so =>
so == SONoOutput)
Expand Down

0 comments on commit ad64a86

Please sign in to comment.