From e20871f42457423ecd1915858cbcd0de4f046176 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Tue, 8 Oct 2024 18:24:12 +0200 Subject: [PATCH 01/33] Start Blocksync --- specs/quint/specs/driver.qnt | 1 + specs/quint/specs/statemachineAsync.qnt | 7 +- specs/quint/specs/sync.qnt | 153 ++++++++++++++++++++++++ 3 files changed, 160 insertions(+), 1 deletion(-) create mode 100644 specs/quint/specs/sync.qnt diff --git a/specs/quint/specs/driver.qnt b/specs/quint/specs/driver.qnt index a15253327..f08a6ea28 100644 --- a/specs/quint/specs/driver.qnt +++ b/specs/quint/specs/driver.qnt @@ -407,6 +407,7 @@ module driver { incomingVotes: Set[Vote], incomingProposals: Set[Proposal], incomingCertificates: Set[Set[Vote]], + // TODO: add buffers for sync getValueRequests: Set[(Height, Round)], nextValueToPropose: Value, } diff --git a/specs/quint/specs/statemachineAsync.qnt b/specs/quint/specs/statemachineAsync.qnt index b25337fb8..bdfeac96d 100644 --- a/specs/quint/specs/statemachineAsync.qnt +++ b/specs/quint/specs/statemachineAsync.qnt @@ -17,6 +17,7 @@ module statemachineAsync { import types.* from "./types" +export types.* import driver.* from "./driver" export driver.* import consensus.* from "./consensus" @@ -54,6 +55,8 @@ var certBuffer : Address -> Set[Set[Vote]] var voteBuffer : Address -> Set[Vote] var _hist: { validator: Address, input: DriverInput, output: ConsensusOutput } + + action unchangedAll = all { system' = system, propBuffer' = propBuffer, @@ -212,7 +215,8 @@ action deliverCertificate(v: Address, c: Set[Vote]) : bool = all { voteBuffer' = voteBuffer, } -action deliverSomeCertificate(v: Address) : bool = any { +action deliverSomeCertificate(v: Address) : bool = all { + certBuffer.keys().size() > 0, nondet c = oneOf(certBuffer.get(v)) deliverCertificate(v, c) } @@ -241,4 +245,5 @@ action step = { } + } diff --git a/specs/quint/specs/sync.qnt b/specs/quint/specs/sync.qnt new file mode 100644 index 000000000..21f0e6ca1 --- /dev/null +++ b/specs/quint/specs/sync.qnt @@ -0,0 +1,153 @@ +// -*- mode: Bluespec; -*- + +module sync { + +import statemachineAsync( + validators = Set("v1", "v2", "v3", "v4"), + validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1), + Faulty = Set("v1"), + Values = Set("red", "blue"), + Rounds = Set(0, 1, 2, 3), + Heights = Set(0) // , 1, 2, 3) + ).* from "./statemachineAsync" + +type SyncStatusMsg = { + peer: Address, + base: Height, + top: Height +} + +type SyncStatus = { + base: Height, + top: Height +} + +type ReqType = + | SyncCertificate + | SyncBlock + +type RequestMsg = { + client: Address, + server: Address, + rtype: ReqType, + height: Height +} + +type SynchronizerOutput = + | SOCertificate(Set[Vote]) + | SOBlock(Value) + | SONoOutput + +type Option[a] = + | Some(a) + | None + +type Synchronizer = { + height: Height, + peers: Set[Address], // MVP: this is going to be the validator set for now + // so we use addresses. We might use peerID in the future + peerStatus: Address -> SyncStatus, + openRequests: Set[RequestMsg], + lastSyncedHeight: Height // done if greater than or equal to height +} + +pure def initSynchronizer(peers: Set[Address]) : Synchronizer = + { + height: -1, + peers: peers, + peerStatus: peers.mapBy(x => {base:-1, top:-1}), + openRequests: Set(), + lastSyncedHeight: -1, + } + +pure def syncNewHeight (s: Synchronizer, h: Height) : Synchronizer = + if (h <= s.height) s + else + s.with("height", h) + + +pure def syncStatus (s: NodeState) : SyncStatusMsg = +//TODO: Logic + { peer: s.es.cs.p , base: 5, top: 7 } + + + +// State machine + +var statusBuffer : Address -> Set[SyncStatusMsg] +var syncSystem: Address -> Synchronizer + + +pure def sendStatus(buffer: Address -> Set[SyncStatusMsg], sm: SyncStatusMsg): Address -> Set[SyncStatusMsg] = + buffer.keys().mapBy(x => { ...buffer.get(x).union(Set(sm)) }) + + + + +action syncInit = all { + init, + statusBuffer' = Correct.mapBy(v => Set()), +} + +action syncUnchangedAll = all { + statusBuffer' = statusBuffer +} + + +pure def syncClient (s: Synchronizer) : +{sync: Synchronizer, so: SynchronizerOutput, req: Option[RequestMsg]} = +// TODO logic + { + sync: s, + so: SONoOutput, + req: None + } + +pure def syncServer (s: Synchronizer, ns: NodeState) : +{sync: Synchronizer, block: Value, cert: Set[Set[Vote]]} = +// TODO logic +// check for requests and serve them +// coupling to node state unclear + { + sync: s, + block: Val("1"), + cert: Set() + } + +action syncStepServer(v) = all { + unchangedAll, + statusBuffer' = statusBuffer + +} + +action syncStepClient(v) = all { + // TODO call syncClient and deliver the SO to the node + unchangedAll, + statusBuffer' = statusBuffer +} + + +action syncStatusStep(v) = all { + val newStatus = system.get(v).syncStatus() + statusBuffer' = sendStatus(statusBuffer, newStatus), + unchangedAll +} + + +action stepWithBlockSync = any { + all { + step, + syncUnchangedAll + }, + nondet v = oneOf(Correct) + any { + //syncDeliverReq(v), + //syncDeliverResp(v), + syncStepServer(v), //looking for a request and sends responses + syncStepClient(v), // is checking if there are responses and check whether it need to requ + syncStatusStep(v), + //syncTimeout(v) + } +} + +} From 6f3c593a4faf1bca21ffbeec6500e9db5a31bbe9 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Tue, 8 Oct 2024 18:51:51 +0200 Subject: [PATCH 02/33] new Height enabled. needs to be tested --- specs/quint/specs/driver.qnt | 8 ++++---- specs/quint/specs/sync.qnt | 22 +++++++++++++++++++--- 2 files changed, 23 insertions(+), 7 deletions(-) diff --git a/specs/quint/specs/driver.qnt b/specs/quint/specs/driver.qnt index f08a6ea28..0f180ba7f 100644 --- a/specs/quint/specs/driver.qnt +++ b/specs/quint/specs/driver.qnt @@ -25,9 +25,9 @@ module driver { certificates: Set[Certificate], // we store Polkas and Commits we have seen } - pure def initDriver(v: Address, vs: ValidatorSet): DriverState = { - bk: initBookKeeper(0, vs), - cs: initConsensusState(v, 0), + pure def initDriver(v: Address, vs: ValidatorSet, h: Height): DriverState = { + bk: initBookKeeper(h, vs), + cs: initConsensusState(v, h), proposals: Set(), valset: vs, executedInputs: List(), @@ -413,7 +413,7 @@ module driver { } pure def initNode(v: Address, vs: Address -> Weight): NodeState = { - es: initDriver(v,vs), + es: initDriver(v, vs, 0), timeouts: Set(), incomingVotes: Set(), incomingProposals: Set(), diff --git a/specs/quint/specs/sync.qnt b/specs/quint/specs/sync.qnt index 21f0e6ca1..db497341f 100644 --- a/specs/quint/specs/sync.qnt +++ b/specs/quint/specs/sync.qnt @@ -49,6 +49,7 @@ type Synchronizer = { peerStatus: Address -> SyncStatus, openRequests: Set[RequestMsg], lastSyncedHeight: Height // done if greater than or equal to height + // we could add buffers for certificates and values } pure def initSynchronizer(peers: Set[Address]) : Synchronizer = @@ -74,15 +75,29 @@ pure def syncStatus (s: NodeState) : SyncStatusMsg = // State machine -var statusBuffer : Address -> Set[SyncStatusMsg] var syncSystem: Address -> Synchronizer +var statusBuffer : Address -> Set[SyncStatusMsg] +var syncValueBuffer : Address -> Set[Proposal] +var syncCertBuffer : Address -> Set[Set[Vote]] pure def sendStatus(buffer: Address -> Set[SyncStatusMsg], sm: SyncStatusMsg): Address -> Set[SyncStatusMsg] = buffer.keys().mapBy(x => { ...buffer.get(x).union(Set(sm)) }) - +action newHeightAction(v, valset, h) = all { + val ns = system.get(v).with("es", initDriver(v, valset, h)) + system' = system.put(v, ns), + syncSystem' = syncSystem.put(v, syncNewHeight(syncSystem.get(v), h)), + // rest unchanged + statusBuffer' = statusBuffer, + syncValueBuffer' = syncValueBuffer, + syncCertBuffer' = syncCertBuffer, + _hist' = _hist, + propBuffer' = propBuffer, + voteBuffer' = voteBuffer, + certBuffer' = certBuffer, +} action syncInit = all { init, @@ -115,7 +130,8 @@ pure def syncServer (s: Synchronizer, ns: NodeState) : } action syncStepServer(v) = all { - unchangedAll, + val result = syncServer(syncSystem.get(v), system.get(v)) // this is where the chains is passed + unchangedAll, statusBuffer' = statusBuffer } From 2dcaae42b046d42d46bb97989145f905ded43567 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Wed, 9 Oct 2024 18:14:52 +0200 Subject: [PATCH 03/33] blocksync fuctions done --- specs/quint/specs/driver.qnt | 4 + specs/quint/specs/sync.qnt | 274 ++++++++++++++++++++++++++++++----- 2 files changed, 242 insertions(+), 36 deletions(-) diff --git a/specs/quint/specs/driver.qnt b/specs/quint/specs/driver.qnt index 0f180ba7f..26a774e1e 100644 --- a/specs/quint/specs/driver.qnt +++ b/specs/quint/specs/driver.qnt @@ -408,6 +408,8 @@ module driver { incomingProposals: Set[Proposal], incomingCertificates: Set[Set[Vote]], // TODO: add buffers for sync + incomingSyncValues: Set[NonNilValue], + incomingSyncCertificates: Set[Set[Vote]], getValueRequests: Set[(Height, Round)], nextValueToPropose: Value, } @@ -418,6 +420,8 @@ module driver { incomingVotes: Set(), incomingProposals: Set(), incomingCertificates: Set(), + incomingSyncProposals: Set(), + incomingSyncCertificates: Set(), getValueRequests: Set(), nextValueToPropose: Nil, } diff --git a/specs/quint/specs/sync.qnt b/specs/quint/specs/sync.qnt index db497341f..e18c7c463 100644 --- a/specs/quint/specs/sync.qnt +++ b/specs/quint/specs/sync.qnt @@ -33,9 +33,23 @@ type RequestMsg = { height: Height } + +type Response = + | RespBlock(NonNilValue) + | RespCertificate(Set[Vote]) + +type ResponseMsg = { + client: Address, + server: Address, + height: Height, + response: Response, +} + + + type SynchronizerOutput = | SOCertificate(Set[Vote]) - | SOBlock(Value) + | SOBlock(NonNilValue) | SONoOutput type Option[a] = @@ -43,24 +57,44 @@ type Option[a] = | None type Synchronizer = { + id: Address, height: Height, peers: Set[Address], // MVP: this is going to be the validator set for now // so we use addresses. We might use peerID in the future peerStatus: Address -> SyncStatus, openRequests: Set[RequestMsg], - lastSyncedHeight: Height // done if greater than or equal to height + lastSyncedHeight: Height, // done if greater than or equal to height // we could add buffers for certificates and values + statusMsgs: Set[SyncStatusMsg], + responses: Set[ResponseMsg], } -pure def initSynchronizer(peers: Set[Address]) : Synchronizer = +type Server = { + inbuffer : Set[RequestMsg] +} + +pure def initSynchronizer(id: Address, peers: Set[Address]) : Synchronizer = { + id: id, height: -1, peers: peers, peerStatus: peers.mapBy(x => {base:-1, top:-1}), openRequests: Set(), lastSyncedHeight: -1, + statusMsgs: Set(), + responses: Set(), } +pure def updatePeerStatus (ps: Address -> SyncStatus, msgs: Set[SyncStatusMsg]) : Address -> SyncStatus = + 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 + ) + +pure def initServer = {inbuffer : Set()} + pure def syncNewHeight (s: Synchronizer, h: Height) : Synchronizer = if (h <= s.height) s else @@ -69,21 +103,28 @@ pure def syncNewHeight (s: Synchronizer, h: Height) : Synchronizer = pure def syncStatus (s: NodeState) : SyncStatusMsg = //TODO: Logic - { peer: s.es.cs.p , base: 5, top: 7 } +// TODO: perhaps we should add to height to the chain entries to capture non-zero bases + { peer: s.es.cs.p , base: 0, top: s.es.chain.length() - 1 } // State machine var syncSystem: Address -> Synchronizer +var serverSystem: Address -> Server var statusBuffer : Address -> Set[SyncStatusMsg] -var syncValueBuffer : Address -> Set[Proposal] -var syncCertBuffer : Address -> Set[Set[Vote]] +var syncResponseBuffer : Address -> Set[ResponseMsg] +var syncRequestBuffer : Address -> Set[RequestMsg] -pure def sendStatus(buffer: Address -> Set[SyncStatusMsg], sm: SyncStatusMsg): Address -> Set[SyncStatusMsg] = +pure def broadcastStatus(buffer: Address -> Set[SyncStatusMsg], sm: SyncStatusMsg): Address -> Set[SyncStatusMsg] = buffer.keys().mapBy(x => { ...buffer.get(x).union(Set(sm)) }) +/// put the response message in the boffer of the client +pure def sendResponse(buffer: Address -> Set[ResponseMsg], m: ResponseMsg): Address -> Set[ResponseMsg] = + buffer.put(m.client, { ...buffer.get(m.client).union(Set(m)) }) + + action newHeightAction(v, valset, h) = all { val ns = system.get(v).with("es", initDriver(v, valset, h)) @@ -91,8 +132,7 @@ action newHeightAction(v, valset, h) = all { syncSystem' = syncSystem.put(v, syncNewHeight(syncSystem.get(v), h)), // rest unchanged statusBuffer' = statusBuffer, - syncValueBuffer' = syncValueBuffer, - syncCertBuffer' = syncCertBuffer, + syncResponseBuffer' = syncResponseBuffer, _hist' = _hist, propBuffer' = propBuffer, voteBuffer' = voteBuffer, @@ -102,50 +142,212 @@ action newHeightAction(v, valset, h) = all { action syncInit = all { init, statusBuffer' = Correct.mapBy(v => Set()), + syncResponseBuffer' = Correct.mapBy(v => Set()), + syncRequestBuffer' = Correct.mapBy(v => Set()), + syncSystem' = Correct.mapBy(v => initSynchronizer(v, validators)), + serverSystem' = Correct.mapBy(v => initServer), } action syncUnchangedAll = all { - statusBuffer' = statusBuffer + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer, + syncSystem' = syncSystem, + serverSystem' = serverSystem, + syncRequestBuffer' = syncRequestBuffer, } -pure def syncClient (s: Synchronizer) : -{sync: Synchronizer, so: SynchronizerOutput, req: Option[RequestMsg]} = -// TODO logic - { - sync: s, - so: SONoOutput, - req: None - } +type ClientResult = { + sync: Synchronizer, + so: SynchronizerOutput, + req: Option[RequestMsg] +} -pure def syncServer (s: Synchronizer, ns: NodeState) : -{sync: Synchronizer, block: Value, cert: Set[Set[Vote]]} = -// TODO logic -// check for requests and serve them -// coupling to node state unclear - { + +// { +// height: Height, +// peers: Set[Address], // MVP: this is going to be the validator set for now +// // so we use addresses. We might use peerID in the future +// peerStatus: Address -> SyncStatus, +// openRequests: Set[RequestMsg], +// lastSyncedHeight: Height, // done if greater than or equal to height +// // we could add buffers for certificates and values +// statusMsgs: Set[SyncStatusMsg], +// responses: Set[ResponseMsg], +// } + +pure def syncClient (s: Synchronizer) : ClientResult = + val newPeerStates = updatePeerStatus(s.peerStatus, s.statusMsgs) + if (s.lastSyncedHeight >= s.height) + // nothing to do + { sync: {...s, peerStatus: newPeerStates}, + so: SONoOutput, + req: None} + else + // if there is a peer with a nice height, I am sending a request if I haven't done so before + // if received response + // if it is a certificate -> (check cerifcate) ask for the block from same peer + // -> give the certificate to consensus + // if i receive a block -> (check block) give the block to consensus + // -> nothing (newheight comes from outside) + val goodPeers = s.peers.filter(p => s.peerStatus.get(p).base <= s.height + and s.height < s.peerStatus.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.chooseSome(), + rtype: SyncCertificate, + height: s.height} + { sync: {...s, + peerStatus: newPeerStates, + 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. responses.size()> 0) + val resp = s.responses.chooseSome() // in the future there might be parallelization + val output = match resp.response { + // to be given to the context // TODO: checks for heights, validity + | RespBlock(value) => SOBlock(value) + | RespCertificate(cert) => SOCertificate(cert) + } + // TODO: refactor into handleBlock and handleCertificate + val request = match resp.response { + // if we received a certificate, we need to ask for a block + | RespCertificate(cert) => + val blockreq = { client: s.id, + server: goodPeers.chooseSome(), + rtype: SyncBlock, + height: s.height} + Some(blockreq) + | RespBlock(value) => None + } + val newOpen = match resp.response { + // if we received a certificate, we need to record the block request, otherwise, we are done + | RespCertificate(cert) => + match request { + | Some(blockreq) => Set(blockreq) + | None => Set() + } + | RespBlock(value) => Set() // If we have parallelization we need to remove one element + } + val newLast = match resp.response { + // if we received a certificate, we need to record the block request, otherwise, we are done + | RespCertificate(cert) => s.lastSyncedHeight + | RespBlock(value) => s.height // blockheight + } + { sync: {...s, + peerStatus: newPeerStates, + openRequests: newOpen, + lastSyncedHeight: newLast}, + so: output, + req: request} + else + // I don't have response + // this might be timeout logic + { sync: {...s, peerStatus: newPeerStates}, + so: SONoOutput, + req: None} + else + // no peers + { sync: {...s, peerStatus: newPeerStates}, + so: SONoOutput, + req: None} + + + +type ServerOutput = { + sync: Server, + msg: Option[ResponseMsg], +} + + + +pure def syncServer (s: Server, ns: NodeState) : ServerOutput = + if (s.inbuffer.size() > 0) + val m = s.inbuffer.chooseSome() // TODO: fix + val result = + if (m.height < ns.es.chain.length()) + match m.rtype { + | SyncCertificate => + val cm = { client: m.client, + server: m.server, + height: m.height, + response: RespCertificate(ns.es.chain[m.height].commit)} + Some(cm) + | SyncBlock => + val bl = { client: m.client, + server: m.server, + height: m.height, + response: RespBlock(ns.es.chain[m.height].decision)} + Some(bl) + } + else None + { sync: { ...s, inbuffer: s.inbuffer.exclude(Set(m))}, + msg: result} + else { sync: s, - block: Val("1"), - cert: Set() - } + msg: None} + -action syncStepServer(v) = all { - val result = syncServer(syncSystem.get(v), system.get(v)) // this is where the chains is passed - unchangedAll, - statusBuffer' = statusBuffer +action syncStepServer(v) = all { + val result = syncServer(serverSystem.get(v), system.get(v)) // this is where the chains is passed + all { + unchangedAll, + statusBuffer' = statusBuffer, + syncResponseBuffer' = match result.msg { + | Some(m) => syncResponseBuffer.sendResponse(m) // TODO: fix after broadcast + | None => syncResponseBuffer + }, + syncSystem' = syncSystem, + serverSystem' = serverSystem.put(v, result.sync), + syncRequestBuffer' = syncRequestBuffer, + } } + action syncStepClient(v) = all { - // TODO call syncClient and deliver the SO to the node - unchangedAll, - statusBuffer' = statusBuffer + val result = syncClient(syncSystem.get(v)) + all { + system' = match result.so { + // Put the sync output into the consensus engine + | SOCertificate(cert) => + system.put(v, {... system.get(v), + incomingSyncCertificates: + system.get(v).incomingCertificates.union(Set(cert))}) + | SOBlock(value) => + system.put(v, + {... system.get(v), + incomingSyncValues: system.get(v).incomingSyncValues.union(Set(value))}) + | SONoOutput => system + }, + propBuffer' = propBuffer, + voteBuffer' = voteBuffer, + certBuffer' = certBuffer, + _hist' = _hist, + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer, + syncSystem' = syncSystem.put(v, result.sync), + serverSystem' = serverSystem, + syncRequestBuffer' = match result.req { + | Some(m) => syncRequestBuffer.put(m.server, syncRequestBuffer.get(m.server).union(Set(m))) + | None => syncRequestBuffer + }, + } } action syncStatusStep(v) = all { val newStatus = system.get(v).syncStatus() - statusBuffer' = sendStatus(statusBuffer, newStatus), + statusBuffer' = broadcastStatus(statusBuffer, newStatus), + syncResponseBuffer' = syncResponseBuffer, + syncSystem' = syncSystem, + serverSystem' = serverSystem, + syncRequestBuffer' = syncRequestBuffer, unchangedAll } @@ -160,7 +362,7 @@ action stepWithBlockSync = any { //syncDeliverReq(v), //syncDeliverResp(v), syncStepServer(v), //looking for a request and sends responses - syncStepClient(v), // is checking if there are responses and check whether it need to requ + // syncStepClient(v), // is checking if there are responses and check whether it need to requ syncStatusStep(v), //syncTimeout(v) } From 0f0e8f7ed072619243e47b4896edcf2cdefd58d0 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Thu, 10 Oct 2024 11:55:01 +0200 Subject: [PATCH 04/33] it is moving --- specs/quint/specs/driver.qnt | 7 +- specs/quint/specs/statemachineAsync.qnt | 27 ++++- specs/quint/specs/sync.qnt | 151 ++++++++++++++++++------ 3 files changed, 147 insertions(+), 38 deletions(-) diff --git a/specs/quint/specs/driver.qnt b/specs/quint/specs/driver.qnt index 26a774e1e..be548ff6f 100644 --- a/specs/quint/specs/driver.qnt +++ b/specs/quint/specs/driver.qnt @@ -414,13 +414,13 @@ module driver { nextValueToPropose: Value, } - pure def initNode(v: Address, vs: Address -> Weight): NodeState = { - es: initDriver(v, vs, 0), + pure def initNode(v: Address, vs: Address -> Weight, height: Height): NodeState = { + es: initDriver(v, vs, height), timeouts: Set(), incomingVotes: Set(), incomingProposals: Set(), incomingCertificates: Set(), - incomingSyncProposals: Set(), + incomingSyncValues: Set(), incomingSyncCertificates: Set(), getValueRequests: Set(), nextValueToPropose: Nil, @@ -481,6 +481,7 @@ module driver { else if (state.incomingVotes != Set()) // pick vote, remove it from incoming // val vote = state.incomingVotes.chooseSome() + // TODO: only take votes for the current round. val vote = state.incomingVotes.fold(emptyVote, (sum, y) => y) val newstate = { ...state, incomingVotes: state.incomingVotes.exclude(Set(vote))} (newstate, VoteDInput(vote)) diff --git a/specs/quint/specs/statemachineAsync.qnt b/specs/quint/specs/statemachineAsync.qnt index bdfeac96d..6205013d3 100644 --- a/specs/quint/specs/statemachineAsync.qnt +++ b/specs/quint/specs/statemachineAsync.qnt @@ -72,13 +72,15 @@ val AgreementInv = tuples(Correct, Correct).forall(p => // Actions action init = all { - system' = Correct.mapBy(v => initNode(v, validatorSet)), + system' = Correct.mapBy(v => initNode(v, validatorSet, 0)), propBuffer' = Correct.mapBy(v => Set()), voteBuffer' = Correct.mapBy(v => Set()), certBuffer' = Correct.mapBy(v => Set()), _hist' = { validator: "INIT", input: NoDInput, output: NoConsensusOutput } } + + // Put the proposal into the buffers of all validators pure def sendProposal(buffer: Address -> Set[Proposal], prop: Proposal): Address -> Set[Proposal] = buffer.keys().mapBy(x => { buffer.get(x).union(Set(prop)) }) @@ -216,7 +218,7 @@ action deliverCertificate(v: Address, c: Set[Vote]) : bool = all { } action deliverSomeCertificate(v: Address) : bool = all { - certBuffer.keys().size() > 0, + certBuffer.get(v).size() > 0, nondet c = oneOf(certBuffer.get(v)) deliverCertificate(v, c) } @@ -246,4 +248,25 @@ action step = { +// retreat workaround + +action workaround(v, result) = all{ + system' = match result.so { + // Put the sync output into the consensus engine + | SOCertificate(cert) => + system.put(v, {... system.get(v), + incomingSyncCertificates: + system.get(v).incomingCertificates.union(Set(cert))}) + | SOBlock(value) => + system.put(v, + {... system.get(v), + incomingSyncValues: system.get(v).incomingSyncValues.union(Set(value))}) + | SONoOutput => system + }, + propBuffer' = propBuffer, + voteBuffer' = voteBuffer, + certBuffer' = certBuffer, + _hist' = _hist, +} + } diff --git a/specs/quint/specs/sync.qnt b/specs/quint/specs/sync.qnt index e18c7c463..c05850b47 100644 --- a/specs/quint/specs/sync.qnt +++ b/specs/quint/specs/sync.qnt @@ -33,6 +33,12 @@ type RequestMsg = { height: Height } +pure def emptyReqMsg = { + client: "", + server: "", + rtype: SyncCertificate, + height: -1 +} type Response = | RespBlock(NonNilValue) @@ -45,7 +51,12 @@ type ResponseMsg = { response: Response, } - +pure def emptyResponseMsg = { + client: "", + server: "", + height: -1, + response: RespBlock("none"), +} type SynchronizerOutput = | SOCertificate(Set[Vote]) @@ -125,6 +136,13 @@ pure def sendResponse(buffer: Address -> Set[ResponseMsg], m: ResponseMsg): Addr buffer.put(m.client, { ...buffer.get(m.client).union(Set(m)) }) +action syncInit = all { + statusBuffer' = Correct.mapBy(v => Set()), + syncResponseBuffer' = Correct.mapBy(v => Set()), + syncRequestBuffer' = Correct.mapBy(v => Set()), + syncSystem' = Correct.mapBy(v => initSynchronizer(v, validators)), + serverSystem' = Correct.mapBy(v => initServer), +} action newHeightAction(v, valset, h) = all { val ns = system.get(v).with("es", initDriver(v, valset, h)) @@ -133,19 +151,19 @@ action newHeightAction(v, valset, h) = all { // rest unchanged statusBuffer' = statusBuffer, syncResponseBuffer' = syncResponseBuffer, + serverSystem' = serverSystem, + syncRequestBuffer' = syncRequestBuffer, _hist' = _hist, propBuffer' = propBuffer, voteBuffer' = voteBuffer, certBuffer' = certBuffer, } -action syncInit = all { + + +action initAll = all { init, - statusBuffer' = Correct.mapBy(v => Set()), - syncResponseBuffer' = Correct.mapBy(v => Set()), - syncRequestBuffer' = Correct.mapBy(v => Set()), - syncSystem' = Correct.mapBy(v => initSynchronizer(v, validators)), - serverSystem' = Correct.mapBy(v => initServer), + syncInit } action syncUnchangedAll = all { @@ -190,13 +208,13 @@ pure def syncClient (s: Synchronizer) : ClientResult = // -> give the certificate to consensus // if i receive a block -> (check block) give the block to consensus // -> nothing (newheight comes from outside) - val goodPeers = s.peers.filter(p => s.peerStatus.get(p).base <= s.height - and s.height < s.peerStatus.get(p).top ) + val goodPeers = s.peers.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.chooseSome(), + server: goodPeers.fold("", (acc, i) => i), //chooseSome(), rtype: SyncCertificate, height: s.height} { sync: {...s, @@ -208,7 +226,7 @@ pure def syncClient (s: Synchronizer) : ClientResult = else // we issued a request before, let's see whether there is a response if (s. responses.size()> 0) - val resp = s.responses.chooseSome() // in the future there might be parallelization + val resp = s.responses.fold(emptyResponseMsg, (acc, i) => i) //chooseSome() // in the future there might be parallelization val output = match resp.response { // to be given to the context // TODO: checks for heights, validity | RespBlock(value) => SOBlock(value) @@ -219,7 +237,7 @@ pure def syncClient (s: Synchronizer) : ClientResult = // if we received a certificate, we need to ask for a block | RespCertificate(cert) => val blockreq = { client: s.id, - server: goodPeers.chooseSome(), + server: goodPeers.fold("", (acc, i) => i), // chooseSome(), rtype: SyncBlock, height: s.height} Some(blockreq) @@ -268,7 +286,7 @@ type ServerOutput = { pure def syncServer (s: Server, ns: NodeState) : ServerOutput = if (s.inbuffer.size() > 0) - val m = s.inbuffer.chooseSome() // TODO: fix + val m = s.inbuffer.fold(emptyReqMsg, (acc, i) => i) // chooseSome() // TODO: fix val result = if (m.height < ns.es.chain.length()) match m.rtype { @@ -313,22 +331,7 @@ action syncStepServer(v) = all { action syncStepClient(v) = all { val result = syncClient(syncSystem.get(v)) all { - system' = match result.so { - // Put the sync output into the consensus engine - | SOCertificate(cert) => - system.put(v, {... system.get(v), - incomingSyncCertificates: - system.get(v).incomingCertificates.union(Set(cert))}) - | SOBlock(value) => - system.put(v, - {... system.get(v), - incomingSyncValues: system.get(v).incomingSyncValues.union(Set(value))}) - | SONoOutput => system - }, - propBuffer' = propBuffer, - voteBuffer' = voteBuffer, - certBuffer' = certBuffer, - _hist' = _hist, + workaround(v, result), statusBuffer' = statusBuffer, syncResponseBuffer' = syncResponseBuffer, syncSystem' = syncSystem.put(v, result.sync), @@ -340,6 +343,30 @@ action syncStepClient(v) = all { } } +pure def setChain(s: DriverState, c: List[{decision: NonNilValue, commit: Set[Vote]}]): DriverState = + {... s, chain: c} + +action initHeight(h) = all { + val special = "v4" // TODO proper selection from correct set + val initsystem = Correct.mapBy(v => + // hack + if (v == special) initNode(v, validatorSet, 0) + else initNode(v, validatorSet, h)) + nondet decisionMap = 0.to(h-1).setOfMaps(Values).oneOf() + val list = range(0, h).foldl(List(), (acc, i) => acc.append(decisionMap.get(i))) + val chain = list.foldl(List(), (acc, i) => acc.append({decision: i, commit: Set()})) + all { + system' = initsystem.keys().mapBy(x => + // hack + if (x == special) initsystem.get(x) + else {... initsystem.get(x), es: setChain(initsystem.get(x).es, chain) }), + propBuffer' = Correct.mapBy(v => Set()), + voteBuffer' = Correct.mapBy(v => Set()), + certBuffer' = Correct.mapBy(v => Set()), + _hist' = { validator: "INIT", input: NoDInput, output: NoConsensusOutput }, + syncInit + } +} action syncStatusStep(v) = all { val newStatus = system.get(v).syncStatus() @@ -351,6 +378,47 @@ action syncStatusStep(v) = all { unchangedAll } +action syncDeliverReq(v) = all { + syncRequestBuffer.get(v).size() > 0, + nondet req = syncRequestBuffer.get(v).oneOf() + all { + syncRequestBuffer' = syncRequestBuffer.put(v, syncRequestBuffer.get(v).exclude(Set(req))), + serverSystem' = serverSystem.put(v, {... serverSystem.get(v), + inbuffer: serverSystem.get(v).inbuffer.union(Set(req))}), + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer, + syncSystem' = syncSystem, + unchangedAll + } +} + +action syncDeliverResp(v) = all { + syncResponseBuffer.get(v).size() > 0, + nondet resp = syncResponseBuffer.get(v).oneOf() + all { + syncSystem' = syncSystem.put(v, {... syncSystem.get(v), + responses: syncSystem.get(v).responses.union(Set(resp))}), + syncRequestBuffer' = syncRequestBuffer, + serverSystem' = serverSystem, + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer.put(v, syncResponseBuffer.get(v).exclude(Set(resp))), + unchangedAll + } +} + +action syncDeliverStatus(v) = all { + statusBuffer.get(v).size() > 0, + nondet status = statusBuffer.get(v).oneOf() + all { + syncSystem' = syncSystem.put(v, {... syncSystem.get(v), + statusMsgs: syncSystem.get(v).statusMsgs.union(Set(status))}), + syncRequestBuffer' = syncRequestBuffer, + serverSystem' = serverSystem, + statusBuffer' = statusBuffer.put(v, statusBuffer.get(v).exclude(Set(status))), + syncResponseBuffer' = syncResponseBuffer, + unchangedAll + } +} action stepWithBlockSync = any { all { @@ -359,13 +427,30 @@ action stepWithBlockSync = any { }, nondet v = oneOf(Correct) any { - //syncDeliverReq(v), - //syncDeliverResp(v), + syncDeliverReq(v), + syncDeliverResp(v), + syncDeliverStatus(v), syncStepServer(v), //looking for a request and sends responses - // syncStepClient(v), // is checking if there are responses and check whether it need to requ + syncStepClient(v), // is checking if there are responses and check whether it need to requ syncStatusStep(v), //syncTimeout(v) } } -} +run retreat = + initHeight(4) + .then(newHeightAction("v4", validatorSet, 0)) + .then( syncStatusStep("v2")) + .then(syncDeliverStatus("v4")) + .then(syncStepClient("v4")) // ask for certificate + .then(syncDeliverReq("v2")) + .then(syncStepServer("v2")) + .then(syncDeliverResp("v4")) + .then(syncStepClient("v4")) // ask for block + .then(syncDeliverReq("v2")) + .then(syncStepServer("v2")) + .then(syncDeliverResp("v4")) + .then(syncStepClient("v4")) + + +} \ No newline at end of file From 9b934ab2a81349b53e57550990621cf6c0597985 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Thu, 10 Oct 2024 13:07:08 +0200 Subject: [PATCH 05/33] Daniel told me to push --- specs/quint/specs/driver.qnt | 26 ++++++++++++++++--- specs/quint/specs/statemachineAsync.qnt | 3 ++- specs/quint/specs/sync.qnt | 33 +++++++++++++++++-------- 3 files changed, 47 insertions(+), 15 deletions(-) diff --git a/specs/quint/specs/driver.qnt b/specs/quint/specs/driver.qnt index be548ff6f..8312abb0d 100644 --- a/specs/quint/specs/driver.qnt +++ b/specs/quint/specs/driver.qnt @@ -21,7 +21,7 @@ module driver { pendingStepChange: Step, // NoStep if last consensus call did not change the step started: bool, voteKeeperOutput: VoteKeeperOutput, - chain: List[{decision: NonNilValue, commit: Set[Vote]}], + chain: List[{decision: Proposal, commit: Set[Vote]}], certificates: Set[Certificate], // we store Polkas and Commits we have seen } @@ -312,7 +312,12 @@ module driver { | _ => Set() // This cannot happen } val v = rv._2 - val dc = {decision: v, commit: commit} + val prop = es.proposals.filter(p => and { p.height == es.cs.height, + p.round == rv._1, + p.proposal == rv._2} + ).fold(emptyProposal, (acc, i) => i) //chooseSome(), + val dc = {decision: prop, commit: commit} + // TODO: store proposal in chain instead of value toDriverOutput({ ...es, chain: es.chain.append(dc) }, res, c) // take input out of pending inputs and then call consensus with that input @@ -408,7 +413,7 @@ module driver { incomingProposals: Set[Proposal], incomingCertificates: Set[Set[Vote]], // TODO: add buffers for sync - incomingSyncValues: Set[NonNilValue], + incomingSyncProposals: Set[Proposal], incomingSyncCertificates: Set[Set[Vote]], getValueRequests: Set[(Height, Round)], nextValueToPropose: Value, @@ -420,7 +425,7 @@ module driver { incomingVotes: Set(), incomingProposals: Set(), incomingCertificates: Set(), - incomingSyncValues: Set(), + incomingSyncProposals: Set(), incomingSyncCertificates: Set(), getValueRequests: Set(), nextValueToPropose: Nil, @@ -448,6 +453,19 @@ module driver { if (not(state.es.started)) (state, StartDInput) + else if (state.incomingSyncCertificates != Set()) + // val cert = state.incomingCertificates.chooseSome() + val cert = state.incomingSyncCertificates.fold (Set(), (sum, y) => y) + val newstate = { ...state, incomingSyncCertificates: state.incomingSyncCertificates.exclude(Set(cert))} + (newstate, CertificateDInput(cert)) + + else if (state.incomingSyncProposals != Set()) + // pick proposal, remove it from incoming + // val prop = state.incomingProposals.chooseSome() + val prop = state.incomingSyncProposals.fold (emptyProposal, (sum, y) => y) + val newstate = { ...state, incomingSyncProposals: state.incomingSyncProposals.exclude(Set(prop))} + (newstate, ProposalDInput(prop)) + // This is hard-coded right now. I remove the request when served // also this prevents the StepChangeDInput for the proposer of a new round else if (state.getValueRequests.contains((state.es.cs.height, state.es.cs.round))) diff --git a/specs/quint/specs/statemachineAsync.qnt b/specs/quint/specs/statemachineAsync.qnt index 6205013d3..198a823dc 100644 --- a/specs/quint/specs/statemachineAsync.qnt +++ b/specs/quint/specs/statemachineAsync.qnt @@ -260,7 +260,8 @@ action workaround(v, result) = all{ | SOBlock(value) => system.put(v, {... system.get(v), - incomingSyncValues: system.get(v).incomingSyncValues.union(Set(value))}) + incomingSyncProposals: system.get(v).incomingSyncProposals.union(Set(value))}) + | SONoOutput => system }, propBuffer' = propBuffer, diff --git a/specs/quint/specs/sync.qnt b/specs/quint/specs/sync.qnt index c05850b47..22a589618 100644 --- a/specs/quint/specs/sync.qnt +++ b/specs/quint/specs/sync.qnt @@ -41,7 +41,7 @@ pure def emptyReqMsg = { } type Response = - | RespBlock(NonNilValue) + | RespBlock(Proposal) | RespCertificate(Set[Vote]) type ResponseMsg = { @@ -55,12 +55,12 @@ pure def emptyResponseMsg = { client: "", server: "", height: -1, - response: RespBlock("none"), + response: RespBlock(emptyProposal), } type SynchronizerOutput = | SOCertificate(Set[Vote]) - | SOBlock(NonNilValue) + | SOBlock(Proposal) | SONoOutput type Option[a] = @@ -343,18 +343,25 @@ action syncStepClient(v) = all { } } -pure def setChain(s: DriverState, c: List[{decision: NonNilValue, commit: Set[Vote]}]): DriverState = +pure def setChain(s: DriverState, c: List[{decision: Proposal, commit: Set[Vote]}]): DriverState = {... s, chain: c} +pure def commitSet (h: Height, v: Value) : Set[Vote] = + Set("v1", "v2", "v3").map(n => mkVote(Precommit, n, h, 0, v)) + + + + action initHeight(h) = all { val special = "v4" // TODO proper selection from correct set val initsystem = Correct.mapBy(v => // hack if (v == special) initNode(v, validatorSet, 0) else initNode(v, validatorSet, h)) - nondet decisionMap = 0.to(h-1).setOfMaps(Values).oneOf() - val list = range(0, h).foldl(List(), (acc, i) => acc.append(decisionMap.get(i))) - val chain = list.foldl(List(), (acc, i) => acc.append({decision: i, commit: Set()})) + nondet decisionValMap = 0.to(h-1).setOfMaps(Values).oneOf() + val propMap = decisionValMap.keys().mapBy(i => mkProposal(noAddress, 0, 0, decisionValMap.get(i), 0)) + val list = range(0, h).foldl(List(), (acc, i) => acc.append(propMap.get(i))) + val chain = list.foldl(List(), (acc, i) => acc.append({decision: i, commit: commitSet(i.height, Val(i.proposal))})) all { system' = initsystem.keys().mapBy(x => // hack @@ -420,6 +427,11 @@ action syncDeliverStatus(v) = all { } } +action syncValStep(v) = all { + valStep(v), + syncUnchangedAll +} + action stepWithBlockSync = any { all { step, @@ -440,17 +452,18 @@ action stepWithBlockSync = any { run retreat = initHeight(4) .then(newHeightAction("v4", validatorSet, 0)) - .then( syncStatusStep("v2")) + .then(syncStatusStep("v2")) .then(syncDeliverStatus("v4")) .then(syncStepClient("v4")) // ask for certificate .then(syncDeliverReq("v2")) .then(syncStepServer("v2")) .then(syncDeliverResp("v4")) - .then(syncStepClient("v4")) // ask for block + .then(syncStepClient("v4")) // ask for block and give certificate to node + .expect(system.get("v4").incomingSyncCertificates.size() > 0) .then(syncDeliverReq("v2")) .then(syncStepServer("v2")) .then(syncDeliverResp("v4")) .then(syncStepClient("v4")) - + .expect(system.get("v4").incomingSyncProposals.size() > 0) } \ No newline at end of file From 5f62609004691507e3872affe27eae18c5c2883a Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Thu, 10 Oct 2024 15:40:46 +0200 Subject: [PATCH 06/33] syncing on the lucky path --- specs/quint/specs/sync.qnt | 14 +++++++++++--- specs/quint/specs/votekeeper.qnt | 2 +- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/specs/quint/specs/sync.qnt b/specs/quint/specs/sync.qnt index 22a589618..691d85dbb 100644 --- a/specs/quint/specs/sync.qnt +++ b/specs/quint/specs/sync.qnt @@ -346,12 +346,15 @@ action syncStepClient(v) = all { pure def setChain(s: DriverState, c: List[{decision: Proposal, commit: Set[Vote]}]): DriverState = {... s, chain: c} -pure def commitSet (h: Height, v: Value) : Set[Vote] = - Set("v1", "v2", "v3").map(n => mkVote(Precommit, n, h, 0, v)) +pure def commitSet (h: Height, v: Value) : Set[Vote] = + Set("v1", "v2", "v3").map(n => mkVote(Precommit, n, h, 0, v)) + +/// this sets up an initial state where v4 starts late, and v2 and v3 have reached +/// height h action initHeight(h) = all { val special = "v4" // TODO proper selection from correct set val initsystem = Correct.mapBy(v => @@ -359,7 +362,12 @@ action initHeight(h) = all { if (v == special) initNode(v, validatorSet, 0) else initNode(v, validatorSet, h)) nondet decisionValMap = 0.to(h-1).setOfMaps(Values).oneOf() - val propMap = decisionValMap.keys().mapBy(i => mkProposal(noAddress, 0, 0, decisionValMap.get(i), 0)) + val propMap = decisionValMap.keys().mapBy(i => + mkProposal( proposer(validatorSet, i,0), + i, + 0, + decisionValMap.get(i), + 0)) val list = range(0, h).foldl(List(), (acc, i) => acc.append(propMap.get(i))) val chain = list.foldl(List(), (acc, i) => acc.append({decision: i, commit: commitSet(i.height, Val(i.proposal))})) all { diff --git a/specs/quint/specs/votekeeper.qnt b/specs/quint/specs/votekeeper.qnt index 5353bb4ba..d5e251b5c 100644 --- a/specs/quint/specs/votekeeper.qnt +++ b/specs/quint/specs/votekeeper.qnt @@ -451,7 +451,7 @@ pure def applyCertificate(keeper: Bookkeeper, certificate: Set[Vote], currentRou val roundVotes = keeper.rounds.getOrElse(round, newRoundVotes(keeper.height, round, keeper.validatorSet.totalWeight())) // overwrite roundvotes with certificate val rvEv = roundVotesAndEvidenceFromCertificate(certificate, roundVotes, keeper.validatorSet) - val newRounds = keeper.rounds.set(certificate.certificateRound(), rvEv._1) + val newRounds = keeper.rounds.put(certificate.certificateRound(), rvEv._1) // compute the new bookkeeper state with evidence and updated roundvotes val newkeeper = keeper .with("evidence", keeper.evidence.union(rvEv._2)) From 0118eb3db936b3a369a83cf7f95a5b07d36ccde9 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Thu, 10 Oct 2024 16:15:54 +0200 Subject: [PATCH 07/33] syncing --- specs/quint/specs/driver.qnt | 13 ++++-- specs/quint/specs/sync.qnt | 84 ++++++++++++++++++++++-------------- 2 files changed, 60 insertions(+), 37 deletions(-) diff --git a/specs/quint/specs/driver.qnt b/specs/quint/specs/driver.qnt index 8312abb0d..512e9a8d9 100644 --- a/specs/quint/specs/driver.qnt +++ b/specs/quint/specs/driver.qnt @@ -11,6 +11,11 @@ module driver { // State // ************************************************************************* + type BlockStoreEntry = { + decision: Proposal, + commit: Set[Vote] + } + type DriverState = { bk: Bookkeeper, cs: ConsensusState, @@ -21,11 +26,11 @@ module driver { pendingStepChange: Step, // NoStep if last consensus call did not change the step started: bool, voteKeeperOutput: VoteKeeperOutput, - chain: List[{decision: Proposal, commit: Set[Vote]}], + chain: List[BlockStoreEntry], certificates: Set[Certificate], // we store Polkas and Commits we have seen } - pure def initDriver(v: Address, vs: ValidatorSet, h: Height): DriverState = { + pure def initDriver(v: Address, vs: ValidatorSet, h: Height, chain: List[BlockStoreEntry]): DriverState = { bk: initBookKeeper(h, vs), cs: initConsensusState(v, h), proposals: Set(), @@ -35,7 +40,7 @@ module driver { pendingStepChange: NoStep, started: false, voteKeeperOutput: NoVKOutput, - chain: List(), + chain: chain, certificates: Set(), } @@ -420,7 +425,7 @@ module driver { } pure def initNode(v: Address, vs: Address -> Weight, height: Height): NodeState = { - es: initDriver(v, vs, height), + es: initDriver(v, vs, height, List()), timeouts: Set(), incomingVotes: Set(), incomingProposals: Set(), diff --git a/specs/quint/specs/sync.qnt b/specs/quint/specs/sync.qnt index 691d85dbb..18e041c37 100644 --- a/specs/quint/specs/sync.qnt +++ b/specs/quint/specs/sync.qnt @@ -11,6 +11,10 @@ import statemachineAsync( Heights = Set(0) // , 1, 2, 3) ).* from "./statemachineAsync" +type Option[a] = + | Some(a) + | None + type SyncStatusMsg = { peer: Address, base: Height, @@ -63,10 +67,7 @@ type SynchronizerOutput = | SOBlock(Proposal) | SONoOutput -type Option[a] = - | Some(a) - | None - +/// The state of the synchronizer type Synchronizer = { id: Address, height: Height, @@ -74,19 +75,15 @@ type Synchronizer = { // so we use addresses. We might use peerID in the future peerStatus: Address -> SyncStatus, openRequests: Set[RequestMsg], - lastSyncedHeight: Height, // done if greater than or equal to height - // we could add buffers for certificates and values + lastSyncedHeight: Height, // "done" if greater than or equal to height + // TODO: we could add buffers for certificates and values + // inbuffers statusMsgs: Set[SyncStatusMsg], responses: Set[ResponseMsg], } -type Server = { - inbuffer : Set[RequestMsg] -} - pure def initSynchronizer(id: Address, peers: Set[Address]) : Synchronizer = - { - id: id, + { id: id, height: -1, peers: peers, peerStatus: peers.mapBy(x => {base:-1, top:-1}), @@ -96,6 +93,15 @@ pure def initSynchronizer(id: Address, peers: Set[Address]) : Synchronizer = responses: Set(), } +/// The server state are just incoming requests. The actual data used to respond +/// is from the NodeState +type Server = { + inbuffer : Set[RequestMsg] +} + +pure def initServer = {inbuffer : Set()} + +/// auxiliary function to iterate over the received status messages pure def updatePeerStatus (ps: Address -> SyncStatus, msgs: Set[SyncStatusMsg]) : Address -> SyncStatus = msgs.fold(ps, (newStatus , msg) => if (newStatus.get(msg.peer).top < msg.top) // TODO: think about base? @@ -104,29 +110,19 @@ pure def updatePeerStatus (ps: Address -> SyncStatus, msgs: Set[SyncStatusMsg]) newStatus ) -pure def initServer = {inbuffer : Set()} - +/// inform the synchronizer that consensus has entered height h pure def syncNewHeight (s: Synchronizer, h: Height) : Synchronizer = if (h <= s.height) s else s.with("height", h) - +/// look into the node state and generate a status message pure def syncStatus (s: NodeState) : SyncStatusMsg = -//TODO: Logic // TODO: perhaps we should add to height to the chain entries to capture non-zero bases { peer: s.es.cs.p , base: 0, top: s.es.chain.length() - 1 } -// State machine - -var syncSystem: Address -> Synchronizer -var serverSystem: Address -> Server - -var statusBuffer : Address -> Set[SyncStatusMsg] -var syncResponseBuffer : Address -> Set[ResponseMsg] -var syncRequestBuffer : Address -> Set[RequestMsg] pure def broadcastStatus(buffer: Address -> Set[SyncStatusMsg], sm: SyncStatusMsg): Address -> Set[SyncStatusMsg] = buffer.keys().mapBy(x => { ...buffer.get(x).union(Set(sm)) }) @@ -136,6 +132,17 @@ pure def sendResponse(buffer: Address -> Set[ResponseMsg], m: ResponseMsg): Addr buffer.put(m.client, { ...buffer.get(m.client).union(Set(m)) }) +// +// State machine +// + +var syncSystem: Address -> Synchronizer +var serverSystem: Address -> Server + +var statusBuffer : Address -> Set[SyncStatusMsg] +var syncResponseBuffer : Address -> Set[ResponseMsg] +var syncRequestBuffer : Address -> Set[RequestMsg] + action syncInit = all { statusBuffer' = Correct.mapBy(v => Set()), syncResponseBuffer' = Correct.mapBy(v => Set()), @@ -144,8 +151,11 @@ action syncInit = all { serverSystem' = Correct.mapBy(v => initServer), } +/// environment sends the node to the next height. +/// checks that we have all the previous blocks in the store. action newHeightAction(v, valset, h) = all { - val ns = system.get(v).with("es", initDriver(v, valset, h)) + system.get(v).es.chain.length() >= system.get(v).es.cs.height, + val ns = system.get(v).with("es", initDriver(v, valset, h, system.get(v).es.chain)) system' = system.put(v, ns), syncSystem' = syncSystem.put(v, syncNewHeight(syncSystem.get(v), h)), // rest unchanged @@ -159,8 +169,7 @@ action newHeightAction(v, valset, h) = all { certBuffer' = certBuffer, } - - +/// initialize consensus and synchronizer action initAll = all { init, syncInit @@ -453,13 +462,12 @@ action stepWithBlockSync = any { syncStepServer(v), //looking for a request and sends responses syncStepClient(v), // is checking if there are responses and check whether it need to requ syncStatusStep(v), - //syncTimeout(v) + //syncTimeout(v) // TODO: } } -run retreat = - initHeight(4) - .then(newHeightAction("v4", validatorSet, 0)) +run syncCycle(h) = + newHeightAction("v4", validatorSet, h) .then(syncStatusStep("v2")) .then(syncDeliverStatus("v4")) .then(syncStepClient("v4")) // ask for certificate @@ -467,11 +475,21 @@ run retreat = .then(syncStepServer("v2")) .then(syncDeliverResp("v4")) .then(syncStepClient("v4")) // ask for block and give certificate to node - .expect(system.get("v4").incomingSyncCertificates.size() > 0) + .expect(system.get("v4").incomingSyncCertificates.size() > h) .then(syncDeliverReq("v2")) .then(syncStepServer("v2")) .then(syncDeliverResp("v4")) .then(syncStepClient("v4")) - .expect(system.get("v4").incomingSyncProposals.size() > 0) + .expect(system.get("v4").incomingSyncProposals.size() > h) + .then(3.reps(_ => syncValStep("v4"))) + .expect(system.get("v4").es.chain.length() > 0) + +run retreat = + initHeight(4) + .then(syncCycle(0)) // TODO figure out iteration + // and now v4 has synced block 1! + + + } \ No newline at end of file From ca13638f4503d888f0132554021cce5da8cec79f Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Wed, 30 Oct 2024 12:25:03 +0100 Subject: [PATCH 08/33] moved definitions a bit around --- specs/quint/specs/sync.qnt | 213 +++++++++++++++++++++---------------- 1 file changed, 120 insertions(+), 93 deletions(-) diff --git a/specs/quint/specs/sync.qnt b/specs/quint/specs/sync.qnt index 18e041c37..2adc69ddb 100644 --- a/specs/quint/specs/sync.qnt +++ b/specs/quint/specs/sync.qnt @@ -67,6 +67,13 @@ type SynchronizerOutput = | SOBlock(Proposal) | SONoOutput + + +// **************************************************************************** +// Synchronizer (client side) +// **************************************************************************** + + /// The state of the synchronizer type Synchronizer = { id: Address, @@ -82,6 +89,11 @@ type Synchronizer = { responses: Set[ResponseMsg], } +// +// Synchronizer functions +// + +/// Initialize the synchronizer pure def initSynchronizer(id: Address, peers: Set[Address]) : Synchronizer = { id: id, height: -1, @@ -93,15 +105,7 @@ pure def initSynchronizer(id: Address, peers: Set[Address]) : Synchronizer = responses: Set(), } -/// The server state are just incoming requests. The actual data used to respond -/// is from the NodeState -type Server = { - inbuffer : Set[RequestMsg] -} - -pure def initServer = {inbuffer : Set()} - -/// auxiliary function to iterate over the received status messages +/// Auxiliary function to iterate over the received status messages pure def updatePeerStatus (ps: Address -> SyncStatus, msgs: Set[SyncStatusMsg]) : Address -> SyncStatus = msgs.fold(ps, (newStatus , msg) => if (newStatus.get(msg.peer).top < msg.top) // TODO: think about base? @@ -112,97 +116,19 @@ pure def updatePeerStatus (ps: Address -> SyncStatus, msgs: Set[SyncStatusMsg]) /// inform the synchronizer that consensus has entered height h pure def syncNewHeight (s: Synchronizer, h: Height) : Synchronizer = - if (h <= s.height) s + if (h <= s.height) + s else s.with("height", h) -/// look into the node state and generate a status message -pure def syncStatus (s: NodeState) : SyncStatusMsg = -// TODO: perhaps we should add to height to the chain entries to capture non-zero bases - { peer: s.es.cs.p , base: 0, top: s.es.chain.length() - 1 } - - - - -pure def broadcastStatus(buffer: Address -> Set[SyncStatusMsg], sm: SyncStatusMsg): Address -> Set[SyncStatusMsg] = - buffer.keys().mapBy(x => { ...buffer.get(x).union(Set(sm)) }) - -/// put the response message in the boffer of the client -pure def sendResponse(buffer: Address -> Set[ResponseMsg], m: ResponseMsg): Address -> Set[ResponseMsg] = - buffer.put(m.client, { ...buffer.get(m.client).union(Set(m)) }) - - -// -// State machine -// - -var syncSystem: Address -> Synchronizer -var serverSystem: Address -> Server - -var statusBuffer : Address -> Set[SyncStatusMsg] -var syncResponseBuffer : Address -> Set[ResponseMsg] -var syncRequestBuffer : Address -> Set[RequestMsg] - -action syncInit = all { - statusBuffer' = Correct.mapBy(v => Set()), - syncResponseBuffer' = Correct.mapBy(v => Set()), - syncRequestBuffer' = Correct.mapBy(v => Set()), - syncSystem' = Correct.mapBy(v => initSynchronizer(v, validators)), - serverSystem' = Correct.mapBy(v => initServer), -} - -/// environment sends the node to the next height. -/// checks that we have all the previous blocks in the store. -action newHeightAction(v, valset, h) = all { - system.get(v).es.chain.length() >= system.get(v).es.cs.height, - val ns = system.get(v).with("es", initDriver(v, valset, h, system.get(v).es.chain)) - system' = system.put(v, ns), - syncSystem' = syncSystem.put(v, syncNewHeight(syncSystem.get(v), h)), - // rest unchanged - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer, - serverSystem' = serverSystem, - syncRequestBuffer' = syncRequestBuffer, - _hist' = _hist, - propBuffer' = propBuffer, - voteBuffer' = voteBuffer, - certBuffer' = certBuffer, -} - -/// initialize consensus and synchronizer -action initAll = all { - init, - syncInit -} - -action syncUnchangedAll = all { - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer, - syncSystem' = syncSystem, - serverSystem' = serverSystem, - syncRequestBuffer' = syncRequestBuffer, -} - - +/// returned by the synchronizer: sync is the new state, so is the output towards +/// the consensus driver, req are messages sent towards peers/servers type ClientResult = { sync: Synchronizer, so: SynchronizerOutput, req: Option[RequestMsg] } - -// { -// height: Height, -// peers: Set[Address], // MVP: this is going to be the validator set for now -// // so we use addresses. We might use peerID in the future -// peerStatus: Address -> SyncStatus, -// openRequests: Set[RequestMsg], -// lastSyncedHeight: Height, // done if greater than or equal to height -// // we could add buffers for certificates and values -// statusMsgs: Set[SyncStatusMsg], -// responses: Set[ResponseMsg], -// } - pure def syncClient (s: Synchronizer) : ClientResult = val newPeerStates = updatePeerStatus(s.peerStatus, s.statusMsgs) if (s.lastSyncedHeight >= s.height) @@ -285,14 +211,35 @@ pure def syncClient (s: Synchronizer) : ClientResult = req: None} +// **************************************************************************** +// Server +// **************************************************************************** + +/// The server state are just incoming requests. The actual data used to respond +/// is from the NodeState +type Server = { + inbuffer : Set[RequestMsg] +} + +// +// Server functions +// + +pure def initServer = {inbuffer : Set()} + + +/// look into the node state and generate a status message +pure def syncStatus (s: NodeState) : SyncStatusMsg = +// TODO: perhaps we should add to height to the chain entries to capture non-zero bases + { peer: s.es.cs.p , base: 0, top: s.es.chain.length() - 1 } + +/// new server state and response messages to be sent type ServerOutput = { sync: Server, msg: Option[ResponseMsg], } - - pure def syncServer (s: Server, ns: NodeState) : ServerOutput = if (s.inbuffer.size() > 0) val m = s.inbuffer.fold(emptyReqMsg, (acc, i) => i) // chooseSome() // TODO: fix @@ -321,6 +268,86 @@ pure def syncServer (s: Server, ns: NodeState) : ServerOutput = + + + + +// +// State machine +// +// The statemachine is put on top of statemachineAsync, that is, we use its +// initialization and steps, and add the updates to the variables defined below +// + + + +// Variables + +var syncSystem: Address -> Synchronizer +var serverSystem: Address -> Server + +var statusBuffer : Address -> Set[SyncStatusMsg] +var syncResponseBuffer : Address -> Set[ResponseMsg] +var syncRequestBuffer : Address -> Set[RequestMsg] + +// Auxiliary functions for sending messages + +pure def broadcastStatus(buffer: Address -> Set[SyncStatusMsg], sm: SyncStatusMsg): Address -> Set[SyncStatusMsg] = + buffer.keys().mapBy(x => { ...buffer.get(x).union(Set(sm)) }) + +/// put the response message in the buffer of the client +pure def sendResponse(buffer: Address -> Set[ResponseMsg], m: ResponseMsg): Address -> Set[ResponseMsg] = + buffer.put(m.client, { ...buffer.get(m.client).union(Set(m)) }) + +// +// Actions +// + +/// initializing the variables of the sync part of the state machine +action syncInit = all { + statusBuffer' = Correct.mapBy(v => Set()), + syncResponseBuffer' = Correct.mapBy (v => Set()), + syncRequestBuffer' = Correct.mapBy(v => Set()), + syncSystem' = Correct.mapBy(v => initSynchronizer(v, validators)), + serverSystem' = Correct.mapBy(v => initServer), +} + +action syncUnchangedAll = all { + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer, + syncSystem' = syncSystem, + serverSystem' = serverSystem, + syncRequestBuffer' = syncRequestBuffer, +} + +/// initialize consensus and synchronizer +action initAll = all { + init, + syncInit +} + + +/// environment sends the node to the next height. +/// checks that we have all the previous blocks in the store. +action newHeightAction(v, valset, h) = all { + system.get(v).es.chain.length() >= system.get(v).es.cs.height, + val ns = system.get(v).with("es", initDriver(v, valset, h, system.get(v).es.chain)) + system' = system.put(v, ns), + syncSystem' = syncSystem.put(v, syncNewHeight(syncSystem.get(v), h)), + // rest unchanged + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer, + serverSystem' = serverSystem, + syncRequestBuffer' = syncRequestBuffer, + _hist' = _hist, + propBuffer' = propBuffer, + voteBuffer' = voteBuffer, + certBuffer' = certBuffer, +} + + + + action syncStepServer(v) = all { val result = syncServer(serverSystem.get(v), system.get(v)) // this is where the chains is passed all { From c575052ec65585edbd99004d15db7e6bebaecd87 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Thu, 31 Oct 2024 11:19:05 +0100 Subject: [PATCH 09/33] code cleanup --- specs/quint/specs/statemachineAsync.qnt | 20 +- specs/quint/specs/sync.qnt | 236 +++++++++++++----------- 2 files changed, 140 insertions(+), 116 deletions(-) diff --git a/specs/quint/specs/statemachineAsync.qnt b/specs/quint/specs/statemachineAsync.qnt index 198a823dc..d8c9febd2 100644 --- a/specs/quint/specs/statemachineAsync.qnt +++ b/specs/quint/specs/statemachineAsync.qnt @@ -246,17 +246,27 @@ action step = { } } +/// environment sends the node to the next height. +/// checks that we have all the previous blocks in the store. +action newHeightAction(v, valset, h) = all { + system.get(v).es.chain.length() >= system.get(v).es.cs.height, + val ns = system.get(v).with("es", initDriver(v, valset, h, system.get(v).es.chain)) + system' = system.put(v, ns), + _hist' = _hist, + propBuffer' = propBuffer, + voteBuffer' = voteBuffer, + certBuffer' = certBuffer, +} - -// retreat workaround - -action workaround(v, result) = all{ +/// retreat workaround. TODO: check with Gabriela about Quint flattening +/// the code should be situation in sync.qnt at action syncStepClient(v) +action putSyncOutputIntoNode(v, result) = all{ system' = match result.so { // Put the sync output into the consensus engine | SOCertificate(cert) => system.put(v, {... system.get(v), incomingSyncCertificates: - system.get(v).incomingCertificates.union(Set(cert))}) + system.get(v).incomingSyncCertificates.union(Set(cert))}) | SOBlock(value) => system.put(v, {... system.get(v), diff --git a/specs/quint/specs/sync.qnt b/specs/quint/specs/sync.qnt index 2adc69ddb..815d3a506 100644 --- a/specs/quint/specs/sync.qnt +++ b/specs/quint/specs/sync.qnt @@ -129,6 +129,29 @@ type ClientResult = { req: Option[RequestMsg] } +/// we have received a certifact. now we need to issue the corresponding block request +/// and generate a certificate output +pure def syncHandleCertificate (s: Synchronizer, cert: Set[Vote], newPeerStates: Address -> SyncStatus, peer: str ) : ClientResult = + val blockReq = { client: s.id, + server: peer, + rtype: SyncBlock, + height: s.height} + { sync: {...s, peerStatus: newPeerStates, + 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 +pure def syncHandleBlock (s: Synchronizer, p: Proposal, newPeerStates: Address -> SyncStatus ) : ClientResult = + { sync: {...s, peerStatus: newPeerStates, + openRequests: Set(), // If we have parallelization we need to remove one element, + lastSyncedHeight: s.height }, // blockheight, + so: SOBlock(p), + req: None} + +/// step of a client: +/// 1. update peer statuses, 2. if there is no open request, request something +/// 3. otherwise check whether we have a response and act accordingly pure def syncClient (s: Synchronizer) : ClientResult = val newPeerStates = updatePeerStatus(s.peerStatus, s.statusMsgs) if (s.lastSyncedHeight >= s.height) @@ -137,12 +160,6 @@ pure def syncClient (s: Synchronizer) : ClientResult = so: SONoOutput, req: None} else - // if there is a peer with a nice height, I am sending a request if I haven't done so before - // if received response - // if it is a certificate -> (check cerifcate) ask for the block from same peer - // -> give the certificate to consensus - // if i receive a block -> (check block) give the block to consensus - // -> nothing (newheight comes from outside) val goodPeers = s.peers.filter(p => newPeerStates.get(p).base <= s.height and s.height <= newPeerStates.get(p).top ) if (goodPeers.size() > 0) @@ -160,44 +177,12 @@ pure def syncClient (s: Synchronizer) : ClientResult = } else // we issued a request before, let's see whether there is a response - if (s. responses.size()> 0) + if (s.responses.size()> 0) val resp = s.responses.fold(emptyResponseMsg, (acc, i) => i) //chooseSome() // in the future there might be parallelization - val output = match resp.response { - // to be given to the context // TODO: checks for heights, validity - | RespBlock(value) => SOBlock(value) - | RespCertificate(cert) => SOCertificate(cert) + match resp.response { + | RespBlock(prop) => syncHandleBlock(s, prop, newPeerStates) + | RespCertificate(cert) => syncHandleCertificate(s,cert, newPeerStates, goodPeers.fold("", (s,x) => x)) } - // TODO: refactor into handleBlock and handleCertificate - val request = match resp.response { - // if we received a certificate, we need to ask for a block - | RespCertificate(cert) => - val blockreq = { client: s.id, - server: goodPeers.fold("", (acc, i) => i), // chooseSome(), - rtype: SyncBlock, - height: s.height} - Some(blockreq) - | RespBlock(value) => None - } - val newOpen = match resp.response { - // if we received a certificate, we need to record the block request, otherwise, we are done - | RespCertificate(cert) => - match request { - | Some(blockreq) => Set(blockreq) - | None => Set() - } - | RespBlock(value) => Set() // If we have parallelization we need to remove one element - } - val newLast = match resp.response { - // if we received a certificate, we need to record the block request, otherwise, we are done - | RespCertificate(cert) => s.lastSyncedHeight - | RespBlock(value) => s.height // blockheight - } - { sync: {...s, - peerStatus: newPeerStates, - openRequests: newOpen, - lastSyncedHeight: newLast}, - so: output, - req: request} else // I don't have response // this might be timeout logic @@ -305,19 +290,19 @@ pure def sendResponse(buffer: Address -> Set[ResponseMsg], m: ResponseMsg): Addr /// initializing the variables of the sync part of the state machine action syncInit = all { + syncSystem' = Correct.mapBy(v => initSynchronizer(v, validators)), + serverSystem' = Correct.mapBy(v => initServer), statusBuffer' = Correct.mapBy(v => Set()), syncResponseBuffer' = Correct.mapBy (v => Set()), syncRequestBuffer' = Correct.mapBy(v => Set()), - syncSystem' = Correct.mapBy(v => initSynchronizer(v, validators)), - serverSystem' = Correct.mapBy(v => initServer), } action syncUnchangedAll = all { + serverSystem' = serverSystem, + syncRequestBuffer' = syncRequestBuffer, statusBuffer' = statusBuffer, syncResponseBuffer' = syncResponseBuffer, syncSystem' = syncSystem, - serverSystem' = serverSystem, - syncRequestBuffer' = syncRequestBuffer, } /// initialize consensus and synchronizer @@ -326,28 +311,42 @@ action initAll = all { syncInit } +// +// Actions for the Environment to send a node to a new height +// /// environment sends the node to the next height. -/// checks that we have all the previous blocks in the store. -action newHeightAction(v, valset, h) = all { - system.get(v).es.chain.length() >= system.get(v).es.cs.height, - val ns = system.get(v).with("es", initDriver(v, valset, h, system.get(v).es.chain)) - system' = system.put(v, ns), +/// initializes synchronizer +action newHeightActionSync(v, valset, h) = all { syncSystem' = syncSystem.put(v, syncNewHeight(syncSystem.get(v), h)), - // rest unchanged statusBuffer' = statusBuffer, syncResponseBuffer' = syncResponseBuffer, serverSystem' = serverSystem, syncRequestBuffer' = syncRequestBuffer, - _hist' = _hist, - propBuffer' = propBuffer, - voteBuffer' = voteBuffer, - certBuffer' = certBuffer, } +/// environment sends the node to the next height. +action newHeightActionAll(v, valset, h) = all { + newHeightActionSync(v, valset, h), + newHeightAction(v, valset, h), +} +// +// Actions for process steps in the sync protocol +// +/// Server v announces its status +action syncStatusStep(v) = all { + val newStatus = system.get(v).syncStatus() + statusBuffer' = broadcastStatus(statusBuffer, newStatus), + syncResponseBuffer' = syncResponseBuffer, + syncSystem' = syncSystem, + serverSystem' = serverSystem, + syncRequestBuffer' = syncRequestBuffer, + unchangedAll +} +/// Server v takes a step (checking for requests and responding) action syncStepServer(v) = all { val result = syncServer(serverSystem.get(v), system.get(v)) // this is where the chains is passed all { @@ -363,11 +362,12 @@ action syncStepServer(v) = all { } } - +/// Client v takes a step action syncStepClient(v) = all { val result = syncClient(syncSystem.get(v)) all { - workaround(v, result), + putSyncOutputIntoNode(v, result), // the logic's code should be here, but due to Quint issues + // we need to keep it in stateMachineAsync for now statusBuffer' = statusBuffer, syncResponseBuffer' = syncResponseBuffer, syncSystem' = syncSystem.put(v, result.sync), @@ -379,56 +379,14 @@ action syncStepClient(v) = all { } } -pure def setChain(s: DriverState, c: List[{decision: Proposal, commit: Set[Vote]}]): DriverState = - {... s, chain: c} - - - - -pure def commitSet (h: Height, v: Value) : Set[Vote] = - Set("v1", "v2", "v3").map(n => mkVote(Precommit, n, h, 0, v)) -/// this sets up an initial state where v4 starts late, and v2 and v3 have reached -/// height h -action initHeight(h) = all { - val special = "v4" // TODO proper selection from correct set - val initsystem = Correct.mapBy(v => - // hack - if (v == special) initNode(v, validatorSet, 0) - else initNode(v, validatorSet, h)) - nondet decisionValMap = 0.to(h-1).setOfMaps(Values).oneOf() - val propMap = decisionValMap.keys().mapBy(i => - mkProposal( proposer(validatorSet, i,0), - i, - 0, - decisionValMap.get(i), - 0)) - val list = range(0, h).foldl(List(), (acc, i) => acc.append(propMap.get(i))) - val chain = list.foldl(List(), (acc, i) => acc.append({decision: i, commit: commitSet(i.height, Val(i.proposal))})) - all { - system' = initsystem.keys().mapBy(x => - // hack - if (x == special) initsystem.get(x) - else {... initsystem.get(x), es: setChain(initsystem.get(x).es, chain) }), - propBuffer' = Correct.mapBy(v => Set()), - voteBuffer' = Correct.mapBy(v => Set()), - certBuffer' = Correct.mapBy(v => Set()), - _hist' = { validator: "INIT", input: NoDInput, output: NoConsensusOutput }, - syncInit - } -} -action syncStatusStep(v) = all { - val newStatus = system.get(v).syncStatus() - statusBuffer' = broadcastStatus(statusBuffer, newStatus), - syncResponseBuffer' = syncResponseBuffer, - syncSystem' = syncSystem, - serverSystem' = serverSystem, - syncRequestBuffer' = syncRequestBuffer, - unchangedAll -} +// +// Actions for the environment to deliver messages in the sync protocol +// +/// deliver a request to server v action syncDeliverReq(v) = all { syncRequestBuffer.get(v).size() > 0, nondet req = syncRequestBuffer.get(v).oneOf() @@ -443,6 +401,7 @@ action syncDeliverReq(v) = all { } } +/// deliver a request to client v action syncDeliverResp(v) = all { syncResponseBuffer.get(v).size() > 0, nondet resp = syncResponseBuffer.get(v).oneOf() @@ -457,6 +416,7 @@ action syncDeliverResp(v) = all { } } +/// deliver a status message to client v action syncDeliverStatus(v) = all { statusBuffer.get(v).size() > 0, nondet status = statusBuffer.get(v).oneOf() @@ -471,11 +431,13 @@ action syncDeliverStatus(v) = all { } } +/// validator step in the system with sync protocol action syncValStep(v) = all { valStep(v), syncUnchangedAll } +/// main step function action stepWithBlockSync = any { all { step, @@ -493,8 +455,56 @@ action stepWithBlockSync = any { } } + + +// +// Interesting scenarios +// + +/// auxiliary function for initHeight +/// sets the chain +pure def setChain(s: DriverState, c: List[{decision: Proposal, commit: Set[Vote]}]): DriverState = + {... s, chain: c} + +/// auxiliary function for initHeight +/// constructs a commit certificate for a height and value +pure def commitSet (h: Height, v: Value) : Set[Vote] = + Set("v1", "v2", "v3").map(n => mkVote(Precommit, n, h, 0, v)) + +/// An action to set up an initial state with some nodes already decided up to height h +/// this sets up an initial state where v4 starts late, and v2 and v3 have reached +/// height h +action initHeight(h) = all { + val special = "v4" // TODO proper selection from correct set + val initsystem = Correct.mapBy(v => + // hack + if (v == special) initNode(v, validatorSet, 0) + else initNode(v, validatorSet, h)) + nondet decisionValMap = 0.to(h-1).setOfMaps(Values).oneOf() + val propMap = decisionValMap.keys().mapBy(i => + mkProposal( proposer(validatorSet, i,0), + i, + 0, + decisionValMap.get(i), + 0)) + val list = range(0, h).foldl(List(), (acc, i) => acc.append(propMap.get(i))) + val chain = list.foldl(List(), (acc, i) => acc.append({decision: i, commit: commitSet(i.height, Val(i.proposal))})) + all { + system' = initsystem.keys().mapBy(x => + // hack + if (x == special) initsystem.get(x) + else {... initsystem.get(x), es: setChain(initsystem.get(x).es, chain) }), + propBuffer' = Correct.mapBy(v => Set()), + voteBuffer' = Correct.mapBy(v => Set()), + certBuffer' = Correct.mapBy(v => Set()), + _hist' = { validator: "INIT", input: NoDInput, output: NoConsensusOutput }, + syncInit + } +} + +/// a simple scenario where v4 starts height h run syncCycle(h) = - newHeightAction("v4", validatorSet, h) + newHeightActionAll("v4", validatorSet, h) .then(syncStatusStep("v2")) .then(syncDeliverStatus("v4")) .then(syncStepClient("v4")) // ask for certificate @@ -502,19 +512,23 @@ run syncCycle(h) = .then(syncStepServer("v2")) .then(syncDeliverResp("v4")) .then(syncStepClient("v4")) // ask for block and give certificate to node - .expect(system.get("v4").incomingSyncCertificates.size() > h) + .expect(system.get("v4").incomingSyncCertificates.size() > 0) .then(syncDeliverReq("v2")) .then(syncStepServer("v2")) .then(syncDeliverResp("v4")) .then(syncStepClient("v4")) - .expect(system.get("v4").incomingSyncProposals.size() > h) + .expect(system.get("v4").incomingSyncProposals.size() > 0) .then(3.reps(_ => syncValStep("v4"))) - .expect(system.get("v4").es.chain.length() > 0) + .expect(system.get("v4").es.chain.length() > h) run retreat = - initHeight(4) - .then(syncCycle(0)) // TODO figure out iteration - // and now v4 has synced block 1! + nondet heightToReach = 1.to(7).oneOf() + initHeight( q::debug ("Height:", heightToReach)) + .then(heightToReach.reps(i => syncCycle(i))) + .expect(system.get("v4").es.chain == system.get("v2").es.chain) + .then(newHeightActionAll("v4", validatorSet, heightToReach)) + .expect(system.get("v4").es.cs.height == system.get("v2").es.cs.height) + // and now v4 has synced ! From 75b2c18d59a75c67615c5660fac8d9aa4851ffc4 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Thu, 31 Oct 2024 11:31:26 +0100 Subject: [PATCH 10/33] more cleanup --- specs/quint/specs/sync.qnt | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/specs/quint/specs/sync.qnt b/specs/quint/specs/sync.qnt index 815d3a506..e4e90efb7 100644 --- a/specs/quint/specs/sync.qnt +++ b/specs/quint/specs/sync.qnt @@ -131,20 +131,18 @@ type ClientResult = { /// we have received a certifact. now we need to issue the corresponding block request /// and generate a certificate output -pure def syncHandleCertificate (s: Synchronizer, cert: Set[Vote], newPeerStates: Address -> SyncStatus, peer: str ) : ClientResult = +pure def syncHandleCertificate (s: Synchronizer, cert: Set[Vote], peer: str ) : ClientResult = val blockReq = { client: s.id, server: peer, rtype: SyncBlock, height: s.height} - { sync: {...s, peerStatus: newPeerStates, - openRequests: Set(blockReq)}, // If we have parallelization we need to be more precise here + { 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 -pure def syncHandleBlock (s: Synchronizer, p: Proposal, newPeerStates: Address -> SyncStatus ) : ClientResult = - { sync: {...s, peerStatus: newPeerStates, - openRequests: Set(), // If we have parallelization we need to remove one element, +pure def syncHandleBlock (s: Synchronizer, 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} @@ -154,9 +152,10 @@ pure def syncHandleBlock (s: Synchronizer, p: Proposal, newPeerStates: Address - /// 3. otherwise check whether we have a response and act accordingly pure def syncClient (s: Synchronizer) : ClientResult = val newPeerStates = updatePeerStatus(s.peerStatus, s.statusMsgs) + val newS = { ...s, peerStatus: newPeerStates} if (s.lastSyncedHeight >= s.height) // nothing to do - { sync: {...s, peerStatus: newPeerStates}, + { sync: newS, so: SONoOutput, req: None} else @@ -169,9 +168,7 @@ pure def syncClient (s: Synchronizer) : ClientResult = server: goodPeers.fold("", (acc, i) => i), //chooseSome(), rtype: SyncCertificate, height: s.height} - { sync: {...s, - peerStatus: newPeerStates, - openRequests: s.openRequests.union(Set(req))}, + { sync: {... newS, openRequests: s.openRequests.union(Set(req))}, so: SONoOutput, req: Some(req) } @@ -179,19 +176,20 @@ pure def syncClient (s: Synchronizer) : ClientResult = // we issued a request before, let's see whether there is a response if (s.responses.size()> 0) val resp = s.responses.fold(emptyResponseMsg, (acc, i) => i) //chooseSome() // in the future there might be parallelization + match resp.response { - | RespBlock(prop) => syncHandleBlock(s, prop, newPeerStates) - | RespCertificate(cert) => syncHandleCertificate(s,cert, newPeerStates, goodPeers.fold("", (s,x) => x)) + | RespBlock(prop) => syncHandleBlock(newS, prop) + | RespCertificate(cert) => syncHandleCertificate(newS, cert, goodPeers.fold("", (s,x) => x)) } else // I don't have response // this might be timeout logic - { sync: {...s, peerStatus: newPeerStates}, + { sync: newS, so: SONoOutput, req: None} else // no peers - { sync: {...s, peerStatus: newPeerStates}, + { sync: newS, so: SONoOutput, req: None} From b889cd070969825c30cb44d8a0645949efcfb896 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Thu, 31 Oct 2024 11:50:29 +0100 Subject: [PATCH 11/33] polishing --- specs/quint/specs/statemachineAsync.qnt | 19 +++++++-------- specs/quint/specs/sync.qnt | 31 ++++++++++++++++--------- 2 files changed, 28 insertions(+), 22 deletions(-) diff --git a/specs/quint/specs/statemachineAsync.qnt b/specs/quint/specs/statemachineAsync.qnt index d8c9febd2..29397e851 100644 --- a/specs/quint/specs/statemachineAsync.qnt +++ b/specs/quint/specs/statemachineAsync.qnt @@ -260,18 +260,15 @@ action newHeightAction(v, valset, h) = all { /// retreat workaround. TODO: check with Gabriela about Quint flattening /// the code should be situation in sync.qnt at action syncStepClient(v) -action putSyncOutputIntoNode(v, result) = all{ - system' = match result.so { +action putSyncOutputIntoNode(v, syncOut) = all{ + system' = match syncOut { // Put the sync output into the consensus engine - | SOCertificate(cert) => - system.put(v, {... system.get(v), - incomingSyncCertificates: - system.get(v).incomingSyncCertificates.union(Set(cert))}) - | SOBlock(value) => - system.put(v, - {... system.get(v), - incomingSyncProposals: system.get(v).incomingSyncProposals.union(Set(value))}) - + | SOCertificate(cert) => system.put(v, {... system.get(v), + incomingSyncCertificates: + system.get(v).incomingSyncCertificates.union(Set(cert))}) + | SOBlock(prop) => system.put(v, {... system.get(v), + incomingSyncProposals: + system.get(v).incomingSyncProposals.union(Set(prop))}) | SONoOutput => system }, propBuffer' = propBuffer, diff --git a/specs/quint/specs/sync.qnt b/specs/quint/specs/sync.qnt index e4e90efb7..81da143d8 100644 --- a/specs/quint/specs/sync.qnt +++ b/specs/quint/specs/sync.qnt @@ -194,6 +194,8 @@ pure def syncClient (s: Synchronizer) : ClientResult = req: None} + + // **************************************************************************** // Server // **************************************************************************** @@ -255,8 +257,14 @@ pure def syncServer (s: Server, ns: NodeState) : ServerOutput = -// + +// **************************************************************************** // State machine +// **************************************************************************** + + + + // // The statemachine is put on top of statemachineAsync, that is, we use its // initialization and steps, and add the updates to the variables defined below @@ -273,6 +281,7 @@ var statusBuffer : Address -> Set[SyncStatusMsg] var syncResponseBuffer : Address -> Set[ResponseMsg] var syncRequestBuffer : Address -> Set[RequestMsg] + // Auxiliary functions for sending messages pure def broadcastStatus(buffer: Address -> Set[SyncStatusMsg], sm: SyncStatusMsg): Address -> Set[SyncStatusMsg] = @@ -348,15 +357,15 @@ action syncStatusStep(v) = all { action syncStepServer(v) = all { val result = syncServer(serverSystem.get(v), system.get(v)) // this is where the chains is passed all { - unchangedAll, - statusBuffer' = statusBuffer, + serverSystem' = serverSystem.put(v, result.sync), syncResponseBuffer' = match result.msg { | Some(m) => syncResponseBuffer.sendResponse(m) // TODO: fix after broadcast | None => syncResponseBuffer }, syncSystem' = syncSystem, - serverSystem' = serverSystem.put(v, result.sync), syncRequestBuffer' = syncRequestBuffer, + statusBuffer' = statusBuffer, + unchangedAll, } } @@ -364,16 +373,16 @@ action syncStepServer(v) = all { action syncStepClient(v) = all { val result = syncClient(syncSystem.get(v)) all { - putSyncOutputIntoNode(v, result), // the logic's code should be here, but due to Quint issues - // we need to keep it in stateMachineAsync for now - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer, syncSystem' = syncSystem.put(v, result.sync), - serverSystem' = serverSystem, syncRequestBuffer' = match result.req { | Some(m) => syncRequestBuffer.put(m.server, syncRequestBuffer.get(m.server).union(Set(m))) | None => syncRequestBuffer - }, + }, + putSyncOutputIntoNode(v, result.so), // the logic's code should be here, but due to Quint issues + // we need to keep it in stateMachineAsync for now + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer, + serverSystem' = serverSystem, } } @@ -520,7 +529,7 @@ run syncCycle(h) = .expect(system.get("v4").es.chain.length() > h) run retreat = - nondet heightToReach = 1.to(7).oneOf() + nondet heightToReach = 1.to(4).oneOf() initHeight( q::debug ("Height:", heightToReach)) .then(heightToReach.reps(i => syncCycle(i))) .expect(system.get("v4").es.chain == system.get("v2").es.chain) From 3f49d59ae8dd4ac36610a70417f7c877fbe6f6bf Mon Sep 17 00:00:00 2001 From: Daniel Date: Fri, 8 Nov 2024 11:49:53 +0100 Subject: [PATCH 12/33] fix(quint): fix test units with new driver's methods and types (#524) * quint: fix test unit with new driver's methods * quint: fix test units with new decision type * quint: test-all.sh script with optional params --- .../decideForPastRound/decideForPastRoundrun.qnt | 4 ++-- specs/quint/tests/multi-round/someMultiRoundRuns.qnt | 6 +++--- specs/quint/tests/state-machine/statemachineTest.qnt | 4 ++-- specs/quint/tests/test-all.sh | 11 +++++++++-- 4 files changed, 16 insertions(+), 9 deletions(-) diff --git a/specs/quint/tests/decideForPastRound/decideForPastRoundrun.qnt b/specs/quint/tests/decideForPastRound/decideForPastRoundrun.qnt index b461b742f..13ada2b62 100644 --- a/specs/quint/tests/decideForPastRound/decideForPastRoundrun.qnt +++ b/specs/quint/tests/decideForPastRound/decideForPastRoundrun.qnt @@ -49,7 +49,7 @@ run runToDecision = .then(ListTakeAStep(others.concat(List(testedVal)))) // at this point others have decided and testedVal is ready to go into next round. - .expect(otherSet.forall(x => system.get(x).es.chain[0].decision == "blue")) + .expect(otherSet.forall(x => system.get(x).es.chain[0].decision.proposal == "blue")) .expect(system.get(testedVal).es.chain == List()) .then(valStep(testedVal)) @@ -67,7 +67,7 @@ run runToDecision = .then(valStep(testedVal)) // now we are good. everyone has decided - .expect(Correct.forall(x => system.get(x).es.chain[0].decision == "blue")) + .expect(Correct.forall(x => system.get(x).es.chain[0].decision.proposal == "blue")) // moreover, testedVal has evidence .expect(Faulty.forall(f => diff --git a/specs/quint/tests/multi-round/someMultiRoundRuns.qnt b/specs/quint/tests/multi-round/someMultiRoundRuns.qnt index 65c8a490b..4a0dcead4 100644 --- a/specs/quint/tests/multi-round/someMultiRoundRuns.qnt +++ b/specs/quint/tests/multi-round/someMultiRoundRuns.qnt @@ -39,7 +39,7 @@ run AllButOneDecideInR1WhileSlowInR0 = { .then(ListDeliverAllVotes(Precommit, others, others, validatorSet, 0, 1, Val("green"))) .then(others.length().reps(_ => ListTakeAStep(correctList))) .then(all { - assert(SetFromList(others).forall(proc => system.get(proc).es.chain.head().decision == "green")), + assert(SetFromList(others).forall(proc => system.get(proc).es.chain.head().decision.proposal == "green")), unchangedAll }) } @@ -61,7 +61,7 @@ run DecideForFutureRoundRun = { }) .then(valStep(slow)) // it receives the final precommit and decides .then(all { - assert(validators.forall(proc => system.get(proc).es.chain.head().decision == "green")), + assert(validators.forall(proc => system.get(proc).es.chain.head().decision.proposal == "green")), unchangedAll }) } @@ -82,7 +82,7 @@ run DecideForFutureRoundPrecommitFirstRun = { }) .then(valStep(slow)) // receive proposal and decide .then(all { - assert(validators.forall(proc => system.get(proc).es.chain.head().decision == "green")), + assert(validators.forall(proc => system.get(proc).es.chain.head().decision.proposal == "green")), unchangedAll }) } diff --git a/specs/quint/tests/state-machine/statemachineTest.qnt b/specs/quint/tests/state-machine/statemachineTest.qnt index ae4ab96be..87561d3e1 100644 --- a/specs/quint/tests/state-machine/statemachineTest.qnt +++ b/specs/quint/tests/state-machine/statemachineTest.qnt @@ -26,7 +26,7 @@ var _hist: (str, DriverInput, ConsensusOutput) //var _histSimple: (str, str, str) action init = all { - system' = validators.mapBy(v => initNode(v, validatorSet)), + system' = validators.mapBy(v => initNode(v, validatorSet, 0)), _hist' = ("INIT", NoDInput, NoConsensusOutput) // _histSimple' = ("INIT", "", "") } @@ -173,7 +173,7 @@ run DecidingRunTest = }) .then(all{ // validator 3 decided on "a block" - assert(system.get("v3").es.chain.head().decision == "a block"), + assert(system.get("v3").es.chain.head().decision.proposal == "a block"), system' = system, _hist' = _hist }) diff --git a/specs/quint/tests/test-all.sh b/specs/quint/tests/test-all.sh index 96261c6a0..98547daa6 100755 --- a/specs/quint/tests/test-all.sh +++ b/specs/quint/tests/test-all.sh @@ -1,3 +1,10 @@ -#!/usr/bin/env bash +#!/bin/bash +# +# Accepts optional parameters to `quint`, e.g., `--max-samples 100`. -for x in */*Test.qnt; do quint test $x; done \ No newline at end of file +QUINT_PARAMS=$@ + +for TEST_FILE in */*Test.qnt +do + quint test $QUINT_PARAMS $TEST_FILE +done From 19d10d9fa9113de0b03bfa71ee5d75ef3b8d6626 Mon Sep 17 00:00:00 2001 From: Daniel Date: Mon, 11 Nov 2024 12:24:46 +0100 Subject: [PATCH 13/33] Apply suggestions from code review Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> --- specs/quint/specs/driver.qnt | 2 +- specs/quint/specs/sync.qnt | 8 +++++--- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/specs/quint/specs/driver.qnt b/specs/quint/specs/driver.qnt index 512e9a8d9..cfc9ca3fa 100644 --- a/specs/quint/specs/driver.qnt +++ b/specs/quint/specs/driver.qnt @@ -417,7 +417,7 @@ module driver { incomingVotes: Set[Vote], incomingProposals: Set[Proposal], incomingCertificates: Set[Set[Vote]], - // TODO: add buffers for sync + // buffers for sync protocol. We separate them from non-sync buffers to model that they have higher priority incomingSyncProposals: Set[Proposal], incomingSyncCertificates: Set[Set[Vote]], getValueRequests: Set[(Height, Round)], diff --git a/specs/quint/specs/sync.qnt b/specs/quint/specs/sync.qnt index 81da143d8..2402c8847 100644 --- a/specs/quint/specs/sync.qnt +++ b/specs/quint/specs/sync.qnt @@ -129,7 +129,7 @@ type ClientResult = { req: Option[RequestMsg] } -/// we have received a certifact. now we need to issue the corresponding block request +/// We have received a certificate. now we need to issue the corresponding block request /// and generate a certificate output pure def syncHandleCertificate (s: Synchronizer, cert: Set[Vote], peer: str ) : ClientResult = val blockReq = { client: s.id, @@ -394,6 +394,7 @@ action syncStepClient(v) = all { // /// deliver a request to server v +/// remove the request from the syncRequestBuffer and add it to the server's inbuffer. action syncDeliverReq(v) = all { syncRequestBuffer.get(v).size() > 0, nondet req = syncRequestBuffer.get(v).oneOf() @@ -408,7 +409,8 @@ action syncDeliverReq(v) = all { } } -/// deliver a request to client v +/// deliver a response to client v +/// remove the response from the syncResponseBuffer and add it to the client's responses buffer. action syncDeliverResp(v) = all { syncResponseBuffer.get(v).size() > 0, nondet resp = syncResponseBuffer.get(v).oneOf() @@ -444,7 +446,7 @@ action syncValStep(v) = all { syncUnchangedAll } -/// main step function +/// main step function: either a consensus state-machine step or a sync protocol step action stepWithBlockSync = any { all { step, From 1882dbb8653fdc32364423cc58243fedfc6bb1b0 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Fri, 8 Nov 2024 16:30:16 +0100 Subject: [PATCH 14/33] spec/quint: create a blocksync directory --- specs/quint/specs/{ => blocksync}/sync.qnt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) rename specs/quint/specs/{ => blocksync}/sync.qnt (99%) diff --git a/specs/quint/specs/sync.qnt b/specs/quint/specs/blocksync/sync.qnt similarity index 99% rename from specs/quint/specs/sync.qnt rename to specs/quint/specs/blocksync/sync.qnt index 2402c8847..78a02726b 100644 --- a/specs/quint/specs/sync.qnt +++ b/specs/quint/specs/blocksync/sync.qnt @@ -9,7 +9,7 @@ import statemachineAsync( Values = Set("red", "blue"), Rounds = Set(0, 1, 2, 3), Heights = Set(0) // , 1, 2, 3) - ).* from "./statemachineAsync" + ).* from "../statemachineAsync" type Option[a] = | Some(a) @@ -542,4 +542,4 @@ run retreat = -} \ No newline at end of file +} From 9a3e76eabf4fdd1aefe339321f5a60d5a6ed623e Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 11 Nov 2024 17:35:51 +0100 Subject: [PATCH 15/33] spec/quint: refactored spec into 4 files --- specs/quint/specs/blocksync/blocksync.qnt | 59 +++++ specs/quint/specs/blocksync/client.qnt | 132 ++++++++++++ specs/quint/specs/blocksync/server.qnt | 61 ++++++ specs/quint/specs/blocksync/sync.qnt | 251 +--------------------- 4 files changed, 257 insertions(+), 246 deletions(-) create mode 100644 specs/quint/specs/blocksync/blocksync.qnt create mode 100644 specs/quint/specs/blocksync/client.qnt create mode 100644 specs/quint/specs/blocksync/server.qnt diff --git a/specs/quint/specs/blocksync/blocksync.qnt b/specs/quint/specs/blocksync/blocksync.qnt new file mode 100644 index 000000000..2610e4c2d --- /dev/null +++ b/specs/quint/specs/blocksync/blocksync.qnt @@ -0,0 +1,59 @@ +// -*- mode: Bluespec; -*- + +module blocksync { + + import types.* from "../types" + export types.* + + type Option[a] = + | Some(a) + | None + + type SyncStatusMsg = { + peer: Address, + base: Height, + top: Height + } + + type SyncStatus = { + base: Height, + top: Height + } + + type ReqType = + | SyncCertificate + | SyncBlock + + type RequestMsg = { + client: Address, + server: Address, + rtype: ReqType, + height: Height + } + + pure def emptyReqMsg = { + client: "", + server: "", + rtype: SyncCertificate, + height: -1 + } + + type Response = + | RespBlock(Proposal) + | RespCertificate(Set[Vote]) + + type ResponseMsg = { + client: Address, + server: Address, + height: Height, + response: Response, + } + + pure def emptyResponseMsg = { + client: "", + server: "", + height: -1, + response: RespBlock(emptyProposal), + } + +} diff --git a/specs/quint/specs/blocksync/client.qnt b/specs/quint/specs/blocksync/client.qnt new file mode 100644 index 000000000..52cd92188 --- /dev/null +++ b/specs/quint/specs/blocksync/client.qnt @@ -0,0 +1,132 @@ +// -*- mode: Bluespec; -*- +// **************************************************************************** +// Synchronizer (client side) +// **************************************************************************** + +module client { + import blocksync.* from "./blocksync" + + /// The state of the synchronizer + type Synchronizer = { + id: Address, + height: Height, + peers: Set[Address], // MVP: this is going to be the validator set for now + // so we use addresses. We might use peerID in the future + peerStatus: Address -> SyncStatus, + openRequests: Set[RequestMsg], + lastSyncedHeight: Height, // "done" if greater than or equal to height + // TODO: we could add buffers for certificates and values + // inbuffers + statusMsgs: Set[SyncStatusMsg], + responses: Set[ResponseMsg], + } + + type SynchronizerOutput = + | SOCertificate(Set[Vote]) + | SOBlock(Proposal) + | SONoOutput + + // + // Synchronizer functions + // + + /// Initialize the synchronizer + pure def initSynchronizer(id: Address, peers: Set[Address]) : Synchronizer = + { id: id, + height: -1, + peers: peers, + peerStatus: peers.mapBy(x => {base:-1, top:-1}), + openRequests: Set(), + lastSyncedHeight: -1, + statusMsgs: Set(), + responses: Set(), + } + + /// Auxiliary function to iterate over the received status messages + pure def updatePeerStatus (ps: Address -> SyncStatus, msgs: Set[SyncStatusMsg]) : Address -> SyncStatus = + 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 + ) + + /// inform the synchronizer that consensus has entered height h + pure def syncNewHeight (s: Synchronizer, h: Height) : Synchronizer = + if (h <= s.height) + s + else + s.with("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 + type ClientResult = { + sync: Synchronizer, + so: SynchronizerOutput, + req: Option[RequestMsg] + } + + /// we have received a certifact. now we need to issue the corresponding block request + /// and generate a certificate output + pure def syncHandleCertificate (s: Synchronizer, 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)} + + /// we have received a block. now we need to generate a block output + pure def syncHandleBlock (s: Synchronizer, 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} + + /// step of a client: + /// 1. update peer statuses, 2. if there is no open request, request something + /// 3. otherwise check whether we have a response and act accordingly + pure def syncClient (s: Synchronizer) : ClientResult = + 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} + else + val goodPeers = s.peers.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: 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.responses.size()> 0) + val resp = s.responses.fold(emptyResponseMsg, (acc, i) => i) //chooseSome() // in the future there might be parallelization + + match resp.response { + | RespBlock(prop) => syncHandleBlock(newS, prop) + | RespCertificate(cert) => syncHandleCertificate(newS, cert, goodPeers.fold("", (s,x) => x)) + } + 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} +} diff --git a/specs/quint/specs/blocksync/server.qnt b/specs/quint/specs/blocksync/server.qnt new file mode 100644 index 000000000..231342edd --- /dev/null +++ b/specs/quint/specs/blocksync/server.qnt @@ -0,0 +1,61 @@ +// -*- mode: Bluespec; -*- +// **************************************************************************** +// Server +// **************************************************************************** + +module server { + import driver.* from "../driver" + import blocksync.* from "./blocksync" + + + + /// The server state are just incoming requests. The actual data used to respond + /// is from the NodeState + type Server = { + inbuffer : Set[RequestMsg] + } + + // + // Server functions + // + + pure def initServer = {inbuffer : Set()} + + + /// look into the node state and generate a status message + pure def syncStatus (s: NodeState) : SyncStatusMsg = + // TODO: perhaps we should add to height to the chain entries to capture non-zero bases + { peer: s.es.cs.p , base: 0, top: s.es.chain.length() - 1 } + + /// new server state and response messages to be sent + type ServerOutput = { + sync: Server, + msg: Option[ResponseMsg], + } + + pure def syncServer (s: Server, ns: NodeState) : ServerOutput = + if (s.inbuffer.size() > 0) + val m = s.inbuffer.fold(emptyReqMsg, (acc, i) => i) // chooseSome() // TODO: fix + val result = + if (m.height < ns.es.chain.length()) + match m.rtype { + | SyncCertificate => + val cm = { client: m.client, + server: m.server, + height: m.height, + response: RespCertificate(ns.es.chain[m.height].commit)} + Some(cm) + | SyncBlock => + val bl = { client: m.client, + server: m.server, + height: m.height, + response: RespBlock(ns.es.chain[m.height].decision)} + Some(bl) + } + else None + { sync: { ...s, inbuffer: s.inbuffer.exclude(Set(m))}, + msg: result} + else { + sync: s, + msg: None} +} diff --git a/specs/quint/specs/blocksync/sync.qnt b/specs/quint/specs/blocksync/sync.qnt index 78a02726b..29e138a42 100644 --- a/specs/quint/specs/blocksync/sync.qnt +++ b/specs/quint/specs/blocksync/sync.qnt @@ -1,6 +1,9 @@ // -*- mode: Bluespec; -*- module sync { + +// General definitions +import blocksync.* from "./blocksync" import statemachineAsync( validators = Set("v1", "v2", "v3", "v4"), @@ -11,252 +14,8 @@ import statemachineAsync( Heights = Set(0) // , 1, 2, 3) ).* from "../statemachineAsync" -type Option[a] = - | Some(a) - | None - -type SyncStatusMsg = { - peer: Address, - base: Height, - top: Height -} - -type SyncStatus = { - base: Height, - top: Height -} - -type ReqType = - | SyncCertificate - | SyncBlock - -type RequestMsg = { - client: Address, - server: Address, - rtype: ReqType, - height: Height -} - -pure def emptyReqMsg = { - client: "", - server: "", - rtype: SyncCertificate, - height: -1 -} - -type Response = - | RespBlock(Proposal) - | RespCertificate(Set[Vote]) - -type ResponseMsg = { - client: Address, - server: Address, - height: Height, - response: Response, -} - -pure def emptyResponseMsg = { - client: "", - server: "", - height: -1, - response: RespBlock(emptyProposal), -} - -type SynchronizerOutput = - | SOCertificate(Set[Vote]) - | SOBlock(Proposal) - | SONoOutput - - - -// **************************************************************************** -// Synchronizer (client side) -// **************************************************************************** - - -/// The state of the synchronizer -type Synchronizer = { - id: Address, - height: Height, - peers: Set[Address], // MVP: this is going to be the validator set for now - // so we use addresses. We might use peerID in the future - peerStatus: Address -> SyncStatus, - openRequests: Set[RequestMsg], - lastSyncedHeight: Height, // "done" if greater than or equal to height - // TODO: we could add buffers for certificates and values - // inbuffers - statusMsgs: Set[SyncStatusMsg], - responses: Set[ResponseMsg], -} - -// -// Synchronizer functions -// - -/// Initialize the synchronizer -pure def initSynchronizer(id: Address, peers: Set[Address]) : Synchronizer = - { id: id, - height: -1, - peers: peers, - peerStatus: peers.mapBy(x => {base:-1, top:-1}), - openRequests: Set(), - lastSyncedHeight: -1, - statusMsgs: Set(), - responses: Set(), - } - -/// Auxiliary function to iterate over the received status messages -pure def updatePeerStatus (ps: Address -> SyncStatus, msgs: Set[SyncStatusMsg]) : Address -> SyncStatus = - 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 - ) - -/// inform the synchronizer that consensus has entered height h -pure def syncNewHeight (s: Synchronizer, h: Height) : Synchronizer = - if (h <= s.height) - s - else - s.with("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 -type ClientResult = { - sync: Synchronizer, - so: SynchronizerOutput, - req: Option[RequestMsg] -} - -/// We have received a certificate. now we need to issue the corresponding block request -/// and generate a certificate output -pure def syncHandleCertificate (s: Synchronizer, 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)} - -/// we have received a block. now we need to generate a block output -pure def syncHandleBlock (s: Synchronizer, 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} - -/// step of a client: -/// 1. update peer statuses, 2. if there is no open request, request something -/// 3. otherwise check whether we have a response and act accordingly -pure def syncClient (s: Synchronizer) : ClientResult = - 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} - else - val goodPeers = s.peers.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: 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.responses.size()> 0) - val resp = s.responses.fold(emptyResponseMsg, (acc, i) => i) //chooseSome() // in the future there might be parallelization - - match resp.response { - | RespBlock(prop) => syncHandleBlock(newS, prop) - | RespCertificate(cert) => syncHandleCertificate(newS, cert, goodPeers.fold("", (s,x) => x)) - } - 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} - - - - -// **************************************************************************** -// Server -// **************************************************************************** - - -/// The server state are just incoming requests. The actual data used to respond -/// is from the NodeState -type Server = { - inbuffer : Set[RequestMsg] -} - -// -// Server functions -// - -pure def initServer = {inbuffer : Set()} - - -/// look into the node state and generate a status message -pure def syncStatus (s: NodeState) : SyncStatusMsg = -// TODO: perhaps we should add to height to the chain entries to capture non-zero bases - { peer: s.es.cs.p , base: 0, top: s.es.chain.length() - 1 } - -/// new server state and response messages to be sent -type ServerOutput = { - sync: Server, - msg: Option[ResponseMsg], -} - -pure def syncServer (s: Server, ns: NodeState) : ServerOutput = - if (s.inbuffer.size() > 0) - val m = s.inbuffer.fold(emptyReqMsg, (acc, i) => i) // chooseSome() // TODO: fix - val result = - if (m.height < ns.es.chain.length()) - match m.rtype { - | SyncCertificate => - val cm = { client: m.client, - server: m.server, - height: m.height, - response: RespCertificate(ns.es.chain[m.height].commit)} - Some(cm) - | SyncBlock => - val bl = { client: m.client, - server: m.server, - height: m.height, - response: RespBlock(ns.es.chain[m.height].decision)} - Some(bl) - } - else None - { sync: { ...s, inbuffer: s.inbuffer.exclude(Set(m))}, - msg: result} - else { - sync: s, - msg: None} - - - - - - - +import client.* from "./client" +import server.* from "./server" // **************************************************************************** // State machine From 30d418740d16fc6ffd8afb85338f4224ce3743f6 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 11 Nov 2024 17:36:33 +0100 Subject: [PATCH 16/33] spec/quint: spacing changes --- specs/quint/specs/blocksync/blocksync.qnt | 20 +- specs/quint/specs/blocksync/client.qnt | 42 +- specs/quint/specs/blocksync/server.qnt | 36 +- specs/quint/specs/blocksync/sync.qnt | 591 +++++++++++----------- 4 files changed, 342 insertions(+), 347 deletions(-) diff --git a/specs/quint/specs/blocksync/blocksync.qnt b/specs/quint/specs/blocksync/blocksync.qnt index 2610e4c2d..177a499b0 100644 --- a/specs/quint/specs/blocksync/blocksync.qnt +++ b/specs/quint/specs/blocksync/blocksync.qnt @@ -11,44 +11,44 @@ module blocksync { type SyncStatusMsg = { peer: Address, - base: Height, + base: Height, top: Height } - + type SyncStatus = { - base: Height, + base: Height, top: Height } - + type ReqType = | SyncCertificate | SyncBlock - + type RequestMsg = { client: Address, server: Address, rtype: ReqType, height: Height } - + pure def emptyReqMsg = { client: "", server: "", rtype: SyncCertificate, height: -1 } - - type Response = + + type Response = | RespBlock(Proposal) | RespCertificate(Set[Vote]) - + type ResponseMsg = { client: Address, server: Address, height: Height, response: Response, } - + pure def emptyResponseMsg = { client: "", server: "", diff --git a/specs/quint/specs/blocksync/client.qnt b/specs/quint/specs/blocksync/client.qnt index 52cd92188..c6af03093 100644 --- a/specs/quint/specs/blocksync/client.qnt +++ b/specs/quint/specs/blocksync/client.qnt @@ -21,15 +21,15 @@ module client { responses: Set[ResponseMsg], } - type SynchronizerOutput = + type SynchronizerOutput = | SOCertificate(Set[Vote]) | SOBlock(Proposal) | SONoOutput - + // // Synchronizer functions // - + /// Initialize the synchronizer pure def initSynchronizer(id: Address, peers: Set[Address]) : Synchronizer = { id: id, @@ -41,49 +41,49 @@ module client { statusMsgs: Set(), responses: Set(), } - + /// Auxiliary function to iterate over the received status messages pure def updatePeerStatus (ps: Address -> SyncStatus, msgs: Set[SyncStatusMsg]) : Address -> SyncStatus = - msgs.fold(ps, (newStatus , msg) => + 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 ) - + /// inform the synchronizer that consensus has entered height h pure def syncNewHeight (s: Synchronizer, h: Height) : Synchronizer = - if (h <= s.height) + if (h <= s.height) s else s.with("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 type ClientResult = { - sync: Synchronizer, - so: SynchronizerOutput, + sync: Synchronizer, + so: SynchronizerOutput, req: Option[RequestMsg] } - - /// we have received a certifact. now we need to issue the corresponding block request - /// and generate a certificate output + + /// We have received a certificate. now we need to issue the + /// corresponding block request and generate a certificate output. pure def syncHandleCertificate (s: Synchronizer, cert: Set[Vote], peer: str ) : ClientResult = val blockReq = { client: s.id, - server: peer, + 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 pure def syncHandleBlock (s: Synchronizer, 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} - + /// step of a client: /// 1. update peer statuses, 2. if there is no open request, request something /// 3. otherwise check whether we have a response and act accordingly @@ -96,10 +96,10 @@ module client { so: SONoOutput, req: None} else - val goodPeers = s.peers.filter(p => newPeerStates.get(p).base <= s.height + val goodPeers = s.peers.filter(p => newPeerStates.get(p).base <= s.height and s.height <= newPeerStates.get(p).top ) if (goodPeers.size() > 0) - if (s.openRequests.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(), @@ -113,13 +113,13 @@ module client { // we issued a request before, let's see whether there is a response if (s.responses.size()> 0) val resp = s.responses.fold(emptyResponseMsg, (acc, i) => i) //chooseSome() // in the future there might be parallelization - + match resp.response { | RespBlock(prop) => syncHandleBlock(newS, prop) | RespCertificate(cert) => syncHandleCertificate(newS, cert, goodPeers.fold("", (s,x) => x)) } - else - // I don't have response + else + // I don't have response // this might be timeout logic { sync: newS, so: SONoOutput, diff --git a/specs/quint/specs/blocksync/server.qnt b/specs/quint/specs/blocksync/server.qnt index 231342edd..29bf3775d 100644 --- a/specs/quint/specs/blocksync/server.qnt +++ b/specs/quint/specs/blocksync/server.qnt @@ -7,47 +7,47 @@ module server { import driver.* from "../driver" import blocksync.* from "./blocksync" - - + + /// The server state are just incoming requests. The actual data used to respond /// is from the NodeState type Server = { inbuffer : Set[RequestMsg] } - + // // Server functions // - + pure def initServer = {inbuffer : Set()} - - + + /// look into the node state and generate a status message pure def syncStatus (s: NodeState) : SyncStatusMsg = // TODO: perhaps we should add to height to the chain entries to capture non-zero bases { peer: s.es.cs.p , base: 0, top: s.es.chain.length() - 1 } - + /// new server state and response messages to be sent type ServerOutput = { - sync: Server, - msg: Option[ResponseMsg], + sync: Server, + msg: Option[ResponseMsg], } - + pure def syncServer (s: Server, ns: NodeState) : ServerOutput = - if (s.inbuffer.size() > 0) + if (s.inbuffer.size() > 0) val m = s.inbuffer.fold(emptyReqMsg, (acc, i) => i) // chooseSome() // TODO: fix val result = if (m.height < ns.es.chain.length()) match m.rtype { - | SyncCertificate => - val cm = { client: m.client, - server: m.server, + | SyncCertificate => + val cm = { client: m.client, + server: m.server, height: m.height, response: RespCertificate(ns.es.chain[m.height].commit)} Some(cm) - | SyncBlock => - val bl = { client: m.client, - server: m.server, + | SyncBlock => + val bl = { client: m.client, + server: m.server, height: m.height, response: RespBlock(ns.es.chain[m.height].decision)} Some(bl) @@ -58,4 +58,4 @@ module server { else { sync: s, msg: None} -} +} diff --git a/specs/quint/specs/blocksync/sync.qnt b/specs/quint/specs/blocksync/sync.qnt index 29e138a42..ce457ccdf 100644 --- a/specs/quint/specs/blocksync/sync.qnt +++ b/specs/quint/specs/blocksync/sync.qnt @@ -2,303 +2,298 @@ module sync { -// General definitions -import blocksync.* from "./blocksync" - -import statemachineAsync( - validators = Set("v1", "v2", "v3", "v4"), - validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1), - Faulty = Set("v1"), - Values = Set("red", "blue"), - Rounds = Set(0, 1, 2, 3), - Heights = Set(0) // , 1, 2, 3) - ).* from "../statemachineAsync" - -import client.* from "./client" -import server.* from "./server" - -// **************************************************************************** -// State machine -// **************************************************************************** - - - - -// -// The statemachine is put on top of statemachineAsync, that is, we use its -// initialization and steps, and add the updates to the variables defined below -// - - - -// Variables - -var syncSystem: Address -> Synchronizer -var serverSystem: Address -> Server - -var statusBuffer : Address -> Set[SyncStatusMsg] -var syncResponseBuffer : Address -> Set[ResponseMsg] -var syncRequestBuffer : Address -> Set[RequestMsg] - - -// Auxiliary functions for sending messages - -pure def broadcastStatus(buffer: Address -> Set[SyncStatusMsg], sm: SyncStatusMsg): Address -> Set[SyncStatusMsg] = - buffer.keys().mapBy(x => { ...buffer.get(x).union(Set(sm)) }) - -/// put the response message in the buffer of the client -pure def sendResponse(buffer: Address -> Set[ResponseMsg], m: ResponseMsg): Address -> Set[ResponseMsg] = - buffer.put(m.client, { ...buffer.get(m.client).union(Set(m)) }) - -// -// Actions -// - -/// initializing the variables of the sync part of the state machine -action syncInit = all { - syncSystem' = Correct.mapBy(v => initSynchronizer(v, validators)), - serverSystem' = Correct.mapBy(v => initServer), - statusBuffer' = Correct.mapBy(v => Set()), - syncResponseBuffer' = Correct.mapBy (v => Set()), - syncRequestBuffer' = Correct.mapBy(v => Set()), -} - -action syncUnchangedAll = all { - serverSystem' = serverSystem, - syncRequestBuffer' = syncRequestBuffer, - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer, - syncSystem' = syncSystem, -} - -/// initialize consensus and synchronizer -action initAll = all { - init, - syncInit -} - -// -// Actions for the Environment to send a node to a new height -// - -/// environment sends the node to the next height. -/// initializes synchronizer -action newHeightActionSync(v, valset, h) = all { - syncSystem' = syncSystem.put(v, syncNewHeight(syncSystem.get(v), h)), - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer, - serverSystem' = serverSystem, - syncRequestBuffer' = syncRequestBuffer, -} - -/// environment sends the node to the next height. -action newHeightActionAll(v, valset, h) = all { - newHeightActionSync(v, valset, h), - newHeightAction(v, valset, h), -} - -// -// Actions for process steps in the sync protocol -// - -/// Server v announces its status -action syncStatusStep(v) = all { - val newStatus = system.get(v).syncStatus() - statusBuffer' = broadcastStatus(statusBuffer, newStatus), - syncResponseBuffer' = syncResponseBuffer, - syncSystem' = syncSystem, - serverSystem' = serverSystem, - syncRequestBuffer' = syncRequestBuffer, - unchangedAll -} - -/// Server v takes a step (checking for requests and responding) -action syncStepServer(v) = all { - val result = syncServer(serverSystem.get(v), system.get(v)) // this is where the chains is passed - all { - serverSystem' = serverSystem.put(v, result.sync), - syncResponseBuffer' = match result.msg { - | Some(m) => syncResponseBuffer.sendResponse(m) // TODO: fix after broadcast - | None => syncResponseBuffer - }, - syncSystem' = syncSystem, - syncRequestBuffer' = syncRequestBuffer, - statusBuffer' = statusBuffer, - unchangedAll, - } -} - -/// Client v takes a step -action syncStepClient(v) = all { - val result = syncClient(syncSystem.get(v)) - all { - syncSystem' = syncSystem.put(v, result.sync), - syncRequestBuffer' = match result.req { - | Some(m) => syncRequestBuffer.put(m.server, syncRequestBuffer.get(m.server).union(Set(m))) - | None => syncRequestBuffer - }, - putSyncOutputIntoNode(v, result.so), // the logic's code should be here, but due to Quint issues - // we need to keep it in stateMachineAsync for now - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer, - serverSystem' = serverSystem, - } -} - - - - -// -// Actions for the environment to deliver messages in the sync protocol -// - -/// deliver a request to server v -/// remove the request from the syncRequestBuffer and add it to the server's inbuffer. -action syncDeliverReq(v) = all { - syncRequestBuffer.get(v).size() > 0, - nondet req = syncRequestBuffer.get(v).oneOf() - all { - syncRequestBuffer' = syncRequestBuffer.put(v, syncRequestBuffer.get(v).exclude(Set(req))), - serverSystem' = serverSystem.put(v, {... serverSystem.get(v), - inbuffer: serverSystem.get(v).inbuffer.union(Set(req))}), - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer, - syncSystem' = syncSystem, - unchangedAll - } -} - -/// deliver a response to client v -/// remove the response from the syncResponseBuffer and add it to the client's responses buffer. -action syncDeliverResp(v) = all { - syncResponseBuffer.get(v).size() > 0, - nondet resp = syncResponseBuffer.get(v).oneOf() - all { - syncSystem' = syncSystem.put(v, {... syncSystem.get(v), - responses: syncSystem.get(v).responses.union(Set(resp))}), - syncRequestBuffer' = syncRequestBuffer, - serverSystem' = serverSystem, - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer.put(v, syncResponseBuffer.get(v).exclude(Set(resp))), - unchangedAll - } -} - -/// deliver a status message to client v -action syncDeliverStatus(v) = all { - statusBuffer.get(v).size() > 0, - nondet status = statusBuffer.get(v).oneOf() - all { - syncSystem' = syncSystem.put(v, {... syncSystem.get(v), - statusMsgs: syncSystem.get(v).statusMsgs.union(Set(status))}), - syncRequestBuffer' = syncRequestBuffer, - serverSystem' = serverSystem, - statusBuffer' = statusBuffer.put(v, statusBuffer.get(v).exclude(Set(status))), - syncResponseBuffer' = syncResponseBuffer, - unchangedAll - } -} - -/// validator step in the system with sync protocol -action syncValStep(v) = all { - valStep(v), - syncUnchangedAll -} - -/// main step function: either a consensus state-machine step or a sync protocol step -action stepWithBlockSync = any { - all { - step, - syncUnchangedAll - }, - nondet v = oneOf(Correct) - any { - syncDeliverReq(v), - syncDeliverResp(v), - syncDeliverStatus(v), - syncStepServer(v), //looking for a request and sends responses - syncStepClient(v), // is checking if there are responses and check whether it need to requ - syncStatusStep(v), - //syncTimeout(v) // TODO: - } -} - - - -// -// Interesting scenarios -// - -/// auxiliary function for initHeight -/// sets the chain -pure def setChain(s: DriverState, c: List[{decision: Proposal, commit: Set[Vote]}]): DriverState = - {... s, chain: c} - -/// auxiliary function for initHeight -/// constructs a commit certificate for a height and value -pure def commitSet (h: Height, v: Value) : Set[Vote] = - Set("v1", "v2", "v3").map(n => mkVote(Precommit, n, h, 0, v)) - -/// An action to set up an initial state with some nodes already decided up to height h -/// this sets up an initial state where v4 starts late, and v2 and v3 have reached -/// height h -action initHeight(h) = all { - val special = "v4" // TODO proper selection from correct set - val initsystem = Correct.mapBy(v => - // hack - if (v == special) initNode(v, validatorSet, 0) - else initNode(v, validatorSet, h)) - nondet decisionValMap = 0.to(h-1).setOfMaps(Values).oneOf() - val propMap = decisionValMap.keys().mapBy(i => - mkProposal( proposer(validatorSet, i,0), - i, - 0, - decisionValMap.get(i), - 0)) - val list = range(0, h).foldl(List(), (acc, i) => acc.append(propMap.get(i))) - val chain = list.foldl(List(), (acc, i) => acc.append({decision: i, commit: commitSet(i.height, Val(i.proposal))})) - all { - system' = initsystem.keys().mapBy(x => - // hack - if (x == special) initsystem.get(x) - else {... initsystem.get(x), es: setChain(initsystem.get(x).es, chain) }), - propBuffer' = Correct.mapBy(v => Set()), - voteBuffer' = Correct.mapBy(v => Set()), - certBuffer' = Correct.mapBy(v => Set()), - _hist' = { validator: "INIT", input: NoDInput, output: NoConsensusOutput }, - syncInit - } -} - -/// a simple scenario where v4 starts height h -run syncCycle(h) = - newHeightActionAll("v4", validatorSet, h) - .then(syncStatusStep("v2")) - .then(syncDeliverStatus("v4")) - .then(syncStepClient("v4")) // ask for certificate - .then(syncDeliverReq("v2")) - .then(syncStepServer("v2")) - .then(syncDeliverResp("v4")) - .then(syncStepClient("v4")) // ask for block and give certificate to node - .expect(system.get("v4").incomingSyncCertificates.size() > 0) - .then(syncDeliverReq("v2")) - .then(syncStepServer("v2")) - .then(syncDeliverResp("v4")) - .then(syncStepClient("v4")) - .expect(system.get("v4").incomingSyncProposals.size() > 0) - .then(3.reps(_ => syncValStep("v4"))) - .expect(system.get("v4").es.chain.length() > h) - -run retreat = - nondet heightToReach = 1.to(4).oneOf() - initHeight( q::debug ("Height:", heightToReach)) - .then(heightToReach.reps(i => syncCycle(i))) - .expect(system.get("v4").es.chain == system.get("v2").es.chain) - .then(newHeightActionAll("v4", validatorSet, heightToReach)) - .expect(system.get("v4").es.cs.height == system.get("v2").es.cs.height) - // and now v4 has synced ! - - - + // General definitions + import blocksync.* from "./blocksync" + + import statemachineAsync( + validators = Set("v1", "v2", "v3", "v4"), + validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1), + Faulty = Set("v1"), + Values = Set("red", "blue"), + Rounds = Set(0, 1, 2, 3), + Heights = Set(0) // , 1, 2, 3) + ).* from "../statemachineAsync" + + import client.* from "./client" + import server.* from "./server" + + // **************************************************************************** + // State machine + // **************************************************************************** + // + // The statemachine is put on top of statemachineAsync, that is, we use its + // initialization and steps, and add the updates to the variables defined below + // + + // Variables + + var syncSystem: Address -> Synchronizer + var serverSystem: Address -> Server + + var statusBuffer : Address -> Set[SyncStatusMsg] + var syncResponseBuffer : Address -> Set[ResponseMsg] + var syncRequestBuffer : Address -> Set[RequestMsg] + + // **************************************************************************** + // State machine + // **************************************************************************** + + // Auxiliary functions for sending messages + + pure def broadcastStatus(buffer: Address -> Set[SyncStatusMsg], sm: SyncStatusMsg): Address -> Set[SyncStatusMsg] = + buffer.keys().mapBy(x => { ...buffer.get(x).union(Set(sm)) }) + + /// put the response message in the buffer of the client + pure def sendResponse(buffer: Address -> Set[ResponseMsg], m: ResponseMsg): Address -> Set[ResponseMsg] = + buffer.put(m.client, { ...buffer.get(m.client).union(Set(m)) }) + + // + // Actions + // + + /// initializing the variables of the sync part of the state machine + action syncInit = all { + syncSystem' = Correct.mapBy(v => initSynchronizer(v, validators)), + serverSystem' = Correct.mapBy(v => initServer), + statusBuffer' = Correct.mapBy(v => Set()), + syncResponseBuffer' = Correct.mapBy (v => Set()), + syncRequestBuffer' = Correct.mapBy(v => Set()), + } + + action syncUnchangedAll = all { + serverSystem' = serverSystem, + syncRequestBuffer' = syncRequestBuffer, + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer, + syncSystem' = syncSystem, + } + + /// initialize consensus and synchronizer + action initAll = all { + init, + syncInit + } + + // + // Actions for the Environment to send a node to a new height + // + + /// environment sends the node to the next height. + /// initializes synchronizer + action newHeightActionSync(v, valset, h) = all { + syncSystem' = syncSystem.put(v, syncNewHeight(syncSystem.get(v), h)), + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer, + serverSystem' = serverSystem, + syncRequestBuffer' = syncRequestBuffer, + } + + /// environment sends the node to the next height. + action newHeightActionAll(v, valset, h) = all { + newHeightActionSync(v, valset, h), + newHeightAction(v, valset, h), + } + + // + // Actions for process steps in the sync protocol + // + + /// Server v announces its status + action syncStatusStep(v) = all { + val newStatus = system.get(v).syncStatus() + statusBuffer' = broadcastStatus(statusBuffer, newStatus), + syncResponseBuffer' = syncResponseBuffer, + syncSystem' = syncSystem, + serverSystem' = serverSystem, + syncRequestBuffer' = syncRequestBuffer, + unchangedAll + } + + /// Server v takes a step (checking for requests and responding) + action syncStepServer(v) = all { + val result = syncServer(serverSystem.get(v), system.get(v)) // this is where the chains is passed + all { + serverSystem' = serverSystem.put(v, result.sync), + syncResponseBuffer' = match result.msg { + | Some(m) => syncResponseBuffer.sendResponse(m) // TODO: fix after broadcast + | None => syncResponseBuffer + }, + syncSystem' = syncSystem, + syncRequestBuffer' = syncRequestBuffer, + statusBuffer' = statusBuffer, + unchangedAll, + } + } + + /// Client v takes a step + action syncStepClient(v) = all { + val result = syncClient(syncSystem.get(v)) + all { + syncSystem' = syncSystem.put(v, result.sync), + syncRequestBuffer' = match result.req { + | Some(m) => syncRequestBuffer.put(m.server, syncRequestBuffer.get(m.server).union(Set(m))) + | None => syncRequestBuffer + }, + putSyncOutputIntoNode(v, result.so), // the logic's code should be here, but due to Quint issues + // we need to keep it in stateMachineAsync for now + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer, + serverSystem' = serverSystem, + } + } +>>>>>>> 8eadaf1 (spec/quint: spacing changes) + + + + + // + // Actions for the environment to deliver messages in the sync protocol + // + + /// deliver a request to server v + /// remove the request from the syncRequestBuffer and add it to the server's inbuffer. + action syncDeliverReq(v) = all { + syncRequestBuffer.get(v).size() > 0, + nondet req = syncRequestBuffer.get(v).oneOf() + all { + syncRequestBuffer' = syncRequestBuffer.put(v, syncRequestBuffer.get(v).exclude(Set(req))), + serverSystem' = serverSystem.put(v, {... serverSystem.get(v), + inbuffer: serverSystem.get(v).inbuffer.union(Set(req))}), + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer, + syncSystem' = syncSystem, + unchangedAll + } + } + + /// deliver a response to client v + /// remove the response from the syncResponseBuffer and add it to the client's responses buffer. + action syncDeliverResp(v) = all { + syncResponseBuffer.get(v).size() > 0, + nondet resp = syncResponseBuffer.get(v).oneOf() + all { + syncSystem' = syncSystem.put(v, {... syncSystem.get(v), + responses: syncSystem.get(v).responses.union(Set(resp))}), + syncRequestBuffer' = syncRequestBuffer, + serverSystem' = serverSystem, + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer.put(v, syncResponseBuffer.get(v).exclude(Set(resp))), + unchangedAll + } + } + + /// deliver a status message to client v + action syncDeliverStatus(v) = all { + statusBuffer.get(v).size() > 0, + nondet status = statusBuffer.get(v).oneOf() + all { + syncSystem' = syncSystem.put(v, {... syncSystem.get(v), + statusMsgs: syncSystem.get(v).statusMsgs.union(Set(status))}), + syncRequestBuffer' = syncRequestBuffer, + serverSystem' = serverSystem, + statusBuffer' = statusBuffer.put(v, statusBuffer.get(v).exclude(Set(status))), + syncResponseBuffer' = syncResponseBuffer, + unchangedAll + } + } + + /// validator step in the system with sync protocol + action syncValStep(v) = all { + valStep(v), + syncUnchangedAll + } + + /// main step function: either a consensus state-machine step or a sync protocol step + action stepWithBlockSync = any { + all { + step, + syncUnchangedAll + }, + nondet v = oneOf(Correct) + any { + syncDeliverReq(v), + syncDeliverResp(v), + syncDeliverStatus(v), + syncStepServer(v), //looking for a request and sends responses + syncStepClient(v), // is checking if there are responses and check whether it need to requ + syncStatusStep(v), + //syncTimeout(v) // TODO: + } + } + + + + // + // Interesting scenarios + // + + /// auxiliary function for initHeight + /// sets the chain + pure def setChain(s: DriverState, c: List[{decision: Proposal, commit: Set[Vote]}]): DriverState = + {... s, chain: c} + + /// auxiliary function for initHeight + /// constructs a commit certificate for a height and value + pure def commitSet (h: Height, v: Value) : Set[Vote] = + Set("v1", "v2", "v3").map(n => mkVote(Precommit, n, h, 0, v)) + + /// An action to set up an initial state with some nodes already decided up to height h + /// this sets up an initial state where v4 starts late, and v2 and v3 have reached + /// height h + action initHeight(h) = all { + val special = "v4" // TODO proper selection from correct set + val initsystem = Correct.mapBy(v => + // hack + if (v == special) initNode(v, validatorSet, 0) + else initNode(v, validatorSet, h)) + nondet decisionValMap = 0.to(h-1).setOfMaps(Values).oneOf() + val propMap = decisionValMap.keys().mapBy(i => + mkProposal( proposer(validatorSet, i,0), + i, + 0, + decisionValMap.get(i), + 0)) + val list = range(0, h).foldl(List(), (acc, i) => acc.append(propMap.get(i))) + val chain = list.foldl(List(), (acc, i) => acc.append({decision: i, commit: commitSet(i.height, Val(i.proposal))})) + all { + system' = initsystem.keys().mapBy(x => + // hack + if (x == special) initsystem.get(x) + else {... initsystem.get(x), es: setChain(initsystem.get(x).es, chain) }), + propBuffer' = Correct.mapBy(v => Set()), + voteBuffer' = Correct.mapBy(v => Set()), + certBuffer' = Correct.mapBy(v => Set()), + _hist' = { validator: "INIT", input: NoDInput, output: NoConsensusOutput }, + syncInit + } + } + + /// a simple scenario where v4 starts height h + run syncCycle(h) = + newHeightActionAll("v4", validatorSet, h) + .then(syncStatusStep("v2")) + .then(syncDeliverStatus("v4")) + .then(syncStepClient("v4")) // ask for certificate + .then(syncDeliverReq("v2")) + .then(syncStepServer("v2")) + .then(syncDeliverResp("v4")) + .then(syncStepClient("v4")) // ask for block and give certificate to node + .expect(system.get("v4").incomingSyncCertificates.size() > 0) + .then(syncDeliverReq("v2")) + .then(syncStepServer("v2")) + .then(syncDeliverResp("v4")) + .then(syncStepClient("v4")) + .expect(system.get("v4").incomingSyncProposals.size() > 0) + .then(3.reps(_ => syncValStep("v4"))) + .expect(system.get("v4").es.chain.length() > h) + + run retreat = + nondet heightToReach = 1.to(4).oneOf() + initHeight( q::debug ("Height:", heightToReach)) + .then(heightToReach.reps(i => syncCycle(i))) + .expect(system.get("v4").es.chain == system.get("v2").es.chain) + .then(newHeightActionAll("v4", validatorSet, heightToReach)) + .expect(system.get("v4").es.cs.height == system.get("v2").es.cs.height) + // and now v4 has synced ! } From 606b99dedbdab34aa3c759929c26af771fc8e23b Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 11 Nov 2024 12:44:01 +0100 Subject: [PATCH 17/33] spec/quint: spacing changes again --- specs/quint/specs/blocksync/server.qnt | 3 --- specs/quint/specs/blocksync/sync.qnt | 5 ----- 2 files changed, 8 deletions(-) diff --git a/specs/quint/specs/blocksync/server.qnt b/specs/quint/specs/blocksync/server.qnt index 29bf3775d..8632ab8dc 100644 --- a/specs/quint/specs/blocksync/server.qnt +++ b/specs/quint/specs/blocksync/server.qnt @@ -7,8 +7,6 @@ module server { import driver.* from "../driver" import blocksync.* from "./blocksync" - - /// The server state are just incoming requests. The actual data used to respond /// is from the NodeState type Server = { @@ -21,7 +19,6 @@ module server { pure def initServer = {inbuffer : Set()} - /// look into the node state and generate a status message pure def syncStatus (s: NodeState) : SyncStatusMsg = // TODO: perhaps we should add to height to the chain entries to capture non-zero bases diff --git a/specs/quint/specs/blocksync/sync.qnt b/specs/quint/specs/blocksync/sync.qnt index ce457ccdf..985953731 100644 --- a/specs/quint/specs/blocksync/sync.qnt +++ b/specs/quint/specs/blocksync/sync.qnt @@ -143,9 +143,6 @@ module sync { } >>>>>>> 8eadaf1 (spec/quint: spacing changes) - - - // // Actions for the environment to deliver messages in the sync protocol // @@ -221,8 +218,6 @@ module sync { } } - - // // Interesting scenarios // From 56a65a9608764712b58a0792587e6e9d12c5b795 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 11 Nov 2024 12:50:12 +0100 Subject: [PATCH 18/33] spec/quint: TODOs to render Server self-contained --- specs/quint/specs/blocksync/server.qnt | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/specs/quint/specs/blocksync/server.qnt b/specs/quint/specs/blocksync/server.qnt index 8632ab8dc..eb256f028 100644 --- a/specs/quint/specs/blocksync/server.qnt +++ b/specs/quint/specs/blocksync/server.qnt @@ -7,6 +7,10 @@ module server { import driver.* from "../driver" import blocksync.* from "./blocksync" + // TODO: this should be changed. The data from NodeState we rely on + // should be stored (copied) into the server state. In this way we get + // rid from the dependency on the driver, rendering the server + // self-contained and easier to test. /// The server state are just incoming requests. The actual data used to respond /// is from the NodeState type Server = { @@ -21,7 +25,9 @@ module server { /// look into the node state and generate a status message pure def syncStatus (s: NodeState) : SyncStatusMsg = - // TODO: perhaps we should add to height to the chain entries to capture non-zero bases + // TODO: perhaps we should add to height to the chain entries to capture non-zero bases + // TODO: s.es.cs.p is static, easy to keep in the Server + // TODO: the driver can maintain a copy of them `chain` { peer: s.es.cs.p , base: 0, top: s.es.chain.length() - 1 } /// new server state and response messages to be sent @@ -31,6 +37,7 @@ module server { } pure def syncServer (s: Server, ns: NodeState) : ServerOutput = + // TODO: the driver can maintain a copy of them `chain` if (s.inbuffer.size() > 0) val m = s.inbuffer.fold(emptyReqMsg, (acc, i) => i) // chooseSome() // TODO: fix val result = From d03d5fd3acfb9f1a033692390c3d7853f729db22 Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Mon, 11 Nov 2024 15:51:09 +0100 Subject: [PATCH 19/33] feat(spec): Blocksync (#462) * Start Blocksync * new Height enabled. needs to be tested * blocksync fuctions done * it is moving * Daniel told me to push * syncing on the lucky path * syncing * moved definitions a bit around * code cleanup * more cleanup * polishing * fix(quint): fix test units with new driver's methods and types (#524) * quint: fix test unit with new driver's methods * quint: fix test units with new decision type * quint: test-all.sh script with optional params * Apply suggestions from code review Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> --------- Co-authored-by: Daniel --- specs/quint/specs/sync.qnt | 545 +++++++++++++++++++++++++++++++++++++ 1 file changed, 545 insertions(+) create mode 100644 specs/quint/specs/sync.qnt diff --git a/specs/quint/specs/sync.qnt b/specs/quint/specs/sync.qnt new file mode 100644 index 000000000..2402c8847 --- /dev/null +++ b/specs/quint/specs/sync.qnt @@ -0,0 +1,545 @@ +// -*- mode: Bluespec; -*- + +module sync { + +import statemachineAsync( + validators = Set("v1", "v2", "v3", "v4"), + validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1), + Faulty = Set("v1"), + Values = Set("red", "blue"), + Rounds = Set(0, 1, 2, 3), + Heights = Set(0) // , 1, 2, 3) + ).* from "./statemachineAsync" + +type Option[a] = + | Some(a) + | None + +type SyncStatusMsg = { + peer: Address, + base: Height, + top: Height +} + +type SyncStatus = { + base: Height, + top: Height +} + +type ReqType = + | SyncCertificate + | SyncBlock + +type RequestMsg = { + client: Address, + server: Address, + rtype: ReqType, + height: Height +} + +pure def emptyReqMsg = { + client: "", + server: "", + rtype: SyncCertificate, + height: -1 +} + +type Response = + | RespBlock(Proposal) + | RespCertificate(Set[Vote]) + +type ResponseMsg = { + client: Address, + server: Address, + height: Height, + response: Response, +} + +pure def emptyResponseMsg = { + client: "", + server: "", + height: -1, + response: RespBlock(emptyProposal), +} + +type SynchronizerOutput = + | SOCertificate(Set[Vote]) + | SOBlock(Proposal) + | SONoOutput + + + +// **************************************************************************** +// Synchronizer (client side) +// **************************************************************************** + + +/// The state of the synchronizer +type Synchronizer = { + id: Address, + height: Height, + peers: Set[Address], // MVP: this is going to be the validator set for now + // so we use addresses. We might use peerID in the future + peerStatus: Address -> SyncStatus, + openRequests: Set[RequestMsg], + lastSyncedHeight: Height, // "done" if greater than or equal to height + // TODO: we could add buffers for certificates and values + // inbuffers + statusMsgs: Set[SyncStatusMsg], + responses: Set[ResponseMsg], +} + +// +// Synchronizer functions +// + +/// Initialize the synchronizer +pure def initSynchronizer(id: Address, peers: Set[Address]) : Synchronizer = + { id: id, + height: -1, + peers: peers, + peerStatus: peers.mapBy(x => {base:-1, top:-1}), + openRequests: Set(), + lastSyncedHeight: -1, + statusMsgs: Set(), + responses: Set(), + } + +/// Auxiliary function to iterate over the received status messages +pure def updatePeerStatus (ps: Address -> SyncStatus, msgs: Set[SyncStatusMsg]) : Address -> SyncStatus = + 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 + ) + +/// inform the synchronizer that consensus has entered height h +pure def syncNewHeight (s: Synchronizer, h: Height) : Synchronizer = + if (h <= s.height) + s + else + s.with("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 +type ClientResult = { + sync: Synchronizer, + so: SynchronizerOutput, + req: Option[RequestMsg] +} + +/// We have received a certificate. now we need to issue the corresponding block request +/// and generate a certificate output +pure def syncHandleCertificate (s: Synchronizer, 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)} + +/// we have received a block. now we need to generate a block output +pure def syncHandleBlock (s: Synchronizer, 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} + +/// step of a client: +/// 1. update peer statuses, 2. if there is no open request, request something +/// 3. otherwise check whether we have a response and act accordingly +pure def syncClient (s: Synchronizer) : ClientResult = + 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} + else + val goodPeers = s.peers.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: 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.responses.size()> 0) + val resp = s.responses.fold(emptyResponseMsg, (acc, i) => i) //chooseSome() // in the future there might be parallelization + + match resp.response { + | RespBlock(prop) => syncHandleBlock(newS, prop) + | RespCertificate(cert) => syncHandleCertificate(newS, cert, goodPeers.fold("", (s,x) => x)) + } + 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} + + + + +// **************************************************************************** +// Server +// **************************************************************************** + + +/// The server state are just incoming requests. The actual data used to respond +/// is from the NodeState +type Server = { + inbuffer : Set[RequestMsg] +} + +// +// Server functions +// + +pure def initServer = {inbuffer : Set()} + + +/// look into the node state and generate a status message +pure def syncStatus (s: NodeState) : SyncStatusMsg = +// TODO: perhaps we should add to height to the chain entries to capture non-zero bases + { peer: s.es.cs.p , base: 0, top: s.es.chain.length() - 1 } + +/// new server state and response messages to be sent +type ServerOutput = { + sync: Server, + msg: Option[ResponseMsg], +} + +pure def syncServer (s: Server, ns: NodeState) : ServerOutput = + if (s.inbuffer.size() > 0) + val m = s.inbuffer.fold(emptyReqMsg, (acc, i) => i) // chooseSome() // TODO: fix + val result = + if (m.height < ns.es.chain.length()) + match m.rtype { + | SyncCertificate => + val cm = { client: m.client, + server: m.server, + height: m.height, + response: RespCertificate(ns.es.chain[m.height].commit)} + Some(cm) + | SyncBlock => + val bl = { client: m.client, + server: m.server, + height: m.height, + response: RespBlock(ns.es.chain[m.height].decision)} + Some(bl) + } + else None + { sync: { ...s, inbuffer: s.inbuffer.exclude(Set(m))}, + msg: result} + else { + sync: s, + msg: None} + + + + + + + + +// **************************************************************************** +// State machine +// **************************************************************************** + + + + +// +// The statemachine is put on top of statemachineAsync, that is, we use its +// initialization and steps, and add the updates to the variables defined below +// + + + +// Variables + +var syncSystem: Address -> Synchronizer +var serverSystem: Address -> Server + +var statusBuffer : Address -> Set[SyncStatusMsg] +var syncResponseBuffer : Address -> Set[ResponseMsg] +var syncRequestBuffer : Address -> Set[RequestMsg] + + +// Auxiliary functions for sending messages + +pure def broadcastStatus(buffer: Address -> Set[SyncStatusMsg], sm: SyncStatusMsg): Address -> Set[SyncStatusMsg] = + buffer.keys().mapBy(x => { ...buffer.get(x).union(Set(sm)) }) + +/// put the response message in the buffer of the client +pure def sendResponse(buffer: Address -> Set[ResponseMsg], m: ResponseMsg): Address -> Set[ResponseMsg] = + buffer.put(m.client, { ...buffer.get(m.client).union(Set(m)) }) + +// +// Actions +// + +/// initializing the variables of the sync part of the state machine +action syncInit = all { + syncSystem' = Correct.mapBy(v => initSynchronizer(v, validators)), + serverSystem' = Correct.mapBy(v => initServer), + statusBuffer' = Correct.mapBy(v => Set()), + syncResponseBuffer' = Correct.mapBy (v => Set()), + syncRequestBuffer' = Correct.mapBy(v => Set()), +} + +action syncUnchangedAll = all { + serverSystem' = serverSystem, + syncRequestBuffer' = syncRequestBuffer, + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer, + syncSystem' = syncSystem, +} + +/// initialize consensus and synchronizer +action initAll = all { + init, + syncInit +} + +// +// Actions for the Environment to send a node to a new height +// + +/// environment sends the node to the next height. +/// initializes synchronizer +action newHeightActionSync(v, valset, h) = all { + syncSystem' = syncSystem.put(v, syncNewHeight(syncSystem.get(v), h)), + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer, + serverSystem' = serverSystem, + syncRequestBuffer' = syncRequestBuffer, +} + +/// environment sends the node to the next height. +action newHeightActionAll(v, valset, h) = all { + newHeightActionSync(v, valset, h), + newHeightAction(v, valset, h), +} + +// +// Actions for process steps in the sync protocol +// + +/// Server v announces its status +action syncStatusStep(v) = all { + val newStatus = system.get(v).syncStatus() + statusBuffer' = broadcastStatus(statusBuffer, newStatus), + syncResponseBuffer' = syncResponseBuffer, + syncSystem' = syncSystem, + serverSystem' = serverSystem, + syncRequestBuffer' = syncRequestBuffer, + unchangedAll +} + +/// Server v takes a step (checking for requests and responding) +action syncStepServer(v) = all { + val result = syncServer(serverSystem.get(v), system.get(v)) // this is where the chains is passed + all { + serverSystem' = serverSystem.put(v, result.sync), + syncResponseBuffer' = match result.msg { + | Some(m) => syncResponseBuffer.sendResponse(m) // TODO: fix after broadcast + | None => syncResponseBuffer + }, + syncSystem' = syncSystem, + syncRequestBuffer' = syncRequestBuffer, + statusBuffer' = statusBuffer, + unchangedAll, + } +} + +/// Client v takes a step +action syncStepClient(v) = all { + val result = syncClient(syncSystem.get(v)) + all { + syncSystem' = syncSystem.put(v, result.sync), + syncRequestBuffer' = match result.req { + | Some(m) => syncRequestBuffer.put(m.server, syncRequestBuffer.get(m.server).union(Set(m))) + | None => syncRequestBuffer + }, + putSyncOutputIntoNode(v, result.so), // the logic's code should be here, but due to Quint issues + // we need to keep it in stateMachineAsync for now + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer, + serverSystem' = serverSystem, + } +} + + + + +// +// Actions for the environment to deliver messages in the sync protocol +// + +/// deliver a request to server v +/// remove the request from the syncRequestBuffer and add it to the server's inbuffer. +action syncDeliverReq(v) = all { + syncRequestBuffer.get(v).size() > 0, + nondet req = syncRequestBuffer.get(v).oneOf() + all { + syncRequestBuffer' = syncRequestBuffer.put(v, syncRequestBuffer.get(v).exclude(Set(req))), + serverSystem' = serverSystem.put(v, {... serverSystem.get(v), + inbuffer: serverSystem.get(v).inbuffer.union(Set(req))}), + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer, + syncSystem' = syncSystem, + unchangedAll + } +} + +/// deliver a response to client v +/// remove the response from the syncResponseBuffer and add it to the client's responses buffer. +action syncDeliverResp(v) = all { + syncResponseBuffer.get(v).size() > 0, + nondet resp = syncResponseBuffer.get(v).oneOf() + all { + syncSystem' = syncSystem.put(v, {... syncSystem.get(v), + responses: syncSystem.get(v).responses.union(Set(resp))}), + syncRequestBuffer' = syncRequestBuffer, + serverSystem' = serverSystem, + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer.put(v, syncResponseBuffer.get(v).exclude(Set(resp))), + unchangedAll + } +} + +/// deliver a status message to client v +action syncDeliverStatus(v) = all { + statusBuffer.get(v).size() > 0, + nondet status = statusBuffer.get(v).oneOf() + all { + syncSystem' = syncSystem.put(v, {... syncSystem.get(v), + statusMsgs: syncSystem.get(v).statusMsgs.union(Set(status))}), + syncRequestBuffer' = syncRequestBuffer, + serverSystem' = serverSystem, + statusBuffer' = statusBuffer.put(v, statusBuffer.get(v).exclude(Set(status))), + syncResponseBuffer' = syncResponseBuffer, + unchangedAll + } +} + +/// validator step in the system with sync protocol +action syncValStep(v) = all { + valStep(v), + syncUnchangedAll +} + +/// main step function: either a consensus state-machine step or a sync protocol step +action stepWithBlockSync = any { + all { + step, + syncUnchangedAll + }, + nondet v = oneOf(Correct) + any { + syncDeliverReq(v), + syncDeliverResp(v), + syncDeliverStatus(v), + syncStepServer(v), //looking for a request and sends responses + syncStepClient(v), // is checking if there are responses and check whether it need to requ + syncStatusStep(v), + //syncTimeout(v) // TODO: + } +} + + + +// +// Interesting scenarios +// + +/// auxiliary function for initHeight +/// sets the chain +pure def setChain(s: DriverState, c: List[{decision: Proposal, commit: Set[Vote]}]): DriverState = + {... s, chain: c} + +/// auxiliary function for initHeight +/// constructs a commit certificate for a height and value +pure def commitSet (h: Height, v: Value) : Set[Vote] = + Set("v1", "v2", "v3").map(n => mkVote(Precommit, n, h, 0, v)) + +/// An action to set up an initial state with some nodes already decided up to height h +/// this sets up an initial state where v4 starts late, and v2 and v3 have reached +/// height h +action initHeight(h) = all { + val special = "v4" // TODO proper selection from correct set + val initsystem = Correct.mapBy(v => + // hack + if (v == special) initNode(v, validatorSet, 0) + else initNode(v, validatorSet, h)) + nondet decisionValMap = 0.to(h-1).setOfMaps(Values).oneOf() + val propMap = decisionValMap.keys().mapBy(i => + mkProposal( proposer(validatorSet, i,0), + i, + 0, + decisionValMap.get(i), + 0)) + val list = range(0, h).foldl(List(), (acc, i) => acc.append(propMap.get(i))) + val chain = list.foldl(List(), (acc, i) => acc.append({decision: i, commit: commitSet(i.height, Val(i.proposal))})) + all { + system' = initsystem.keys().mapBy(x => + // hack + if (x == special) initsystem.get(x) + else {... initsystem.get(x), es: setChain(initsystem.get(x).es, chain) }), + propBuffer' = Correct.mapBy(v => Set()), + voteBuffer' = Correct.mapBy(v => Set()), + certBuffer' = Correct.mapBy(v => Set()), + _hist' = { validator: "INIT", input: NoDInput, output: NoConsensusOutput }, + syncInit + } +} + +/// a simple scenario where v4 starts height h +run syncCycle(h) = + newHeightActionAll("v4", validatorSet, h) + .then(syncStatusStep("v2")) + .then(syncDeliverStatus("v4")) + .then(syncStepClient("v4")) // ask for certificate + .then(syncDeliverReq("v2")) + .then(syncStepServer("v2")) + .then(syncDeliverResp("v4")) + .then(syncStepClient("v4")) // ask for block and give certificate to node + .expect(system.get("v4").incomingSyncCertificates.size() > 0) + .then(syncDeliverReq("v2")) + .then(syncStepServer("v2")) + .then(syncDeliverResp("v4")) + .then(syncStepClient("v4")) + .expect(system.get("v4").incomingSyncProposals.size() > 0) + .then(3.reps(_ => syncValStep("v4"))) + .expect(system.get("v4").es.chain.length() > h) + +run retreat = + nondet heightToReach = 1.to(4).oneOf() + initHeight( q::debug ("Height:", heightToReach)) + .then(heightToReach.reps(i => syncCycle(i))) + .expect(system.get("v4").es.chain == system.get("v2").es.chain) + .then(newHeightActionAll("v4", validatorSet, heightToReach)) + .expect(system.get("v4").es.cs.height == system.get("v2").es.cs.height) + // and now v4 has synced ! + + + + +} \ No newline at end of file From e617e81f55d77d1f895eb0f729dfb2ee0128c5fc Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 11 Nov 2024 17:39:51 +0100 Subject: [PATCH 20/33] spec/quint: spacing changes again --- specs/quint/specs/blocksync/blocksync.qnt | 4 ++-- specs/quint/specs/blocksync/client.qnt | 3 +-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/specs/quint/specs/blocksync/blocksync.qnt b/specs/quint/specs/blocksync/blocksync.qnt index 177a499b0..a3196e075 100644 --- a/specs/quint/specs/blocksync/blocksync.qnt +++ b/specs/quint/specs/blocksync/blocksync.qnt @@ -11,12 +11,12 @@ module blocksync { type SyncStatusMsg = { peer: Address, - base: Height, + base: Height, top: Height } type SyncStatus = { - base: Height, + base: Height, top: Height } diff --git a/specs/quint/specs/blocksync/client.qnt b/specs/quint/specs/blocksync/client.qnt index c6af03093..f08b4309b 100644 --- a/specs/quint/specs/blocksync/client.qnt +++ b/specs/quint/specs/blocksync/client.qnt @@ -96,7 +96,7 @@ module client { so: SONoOutput, req: None} else - val goodPeers = s.peers.filter(p => newPeerStates.get(p).base <= s.height + val goodPeers = s.peers.filter(p => newPeerStates.get(p).base <= s.height and s.height <= newPeerStates.get(p).top ) if (goodPeers.size() > 0) if (s.openRequests.size() == 0) @@ -113,7 +113,6 @@ module client { // we issued a request before, let's see whether there is a response if (s.responses.size()> 0) val resp = s.responses.fold(emptyResponseMsg, (acc, i) => i) //chooseSome() // in the future there might be parallelization - match resp.response { | RespBlock(prop) => syncHandleBlock(newS, prop) | RespCertificate(cert) => syncHandleCertificate(newS, cert, goodPeers.fold("", (s,x) => x)) From a96f7cc71a4b713514332cf11a67ff073d5e4c05 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 11 Nov 2024 17:40:02 +0100 Subject: [PATCH 21/33] specs/quint: removed original sync.qnt --- specs/quint/specs/sync.qnt | 545 ------------------------------------- 1 file changed, 545 deletions(-) delete mode 100644 specs/quint/specs/sync.qnt diff --git a/specs/quint/specs/sync.qnt b/specs/quint/specs/sync.qnt deleted file mode 100644 index 2402c8847..000000000 --- a/specs/quint/specs/sync.qnt +++ /dev/null @@ -1,545 +0,0 @@ -// -*- mode: Bluespec; -*- - -module sync { - -import statemachineAsync( - validators = Set("v1", "v2", "v3", "v4"), - validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1), - Faulty = Set("v1"), - Values = Set("red", "blue"), - Rounds = Set(0, 1, 2, 3), - Heights = Set(0) // , 1, 2, 3) - ).* from "./statemachineAsync" - -type Option[a] = - | Some(a) - | None - -type SyncStatusMsg = { - peer: Address, - base: Height, - top: Height -} - -type SyncStatus = { - base: Height, - top: Height -} - -type ReqType = - | SyncCertificate - | SyncBlock - -type RequestMsg = { - client: Address, - server: Address, - rtype: ReqType, - height: Height -} - -pure def emptyReqMsg = { - client: "", - server: "", - rtype: SyncCertificate, - height: -1 -} - -type Response = - | RespBlock(Proposal) - | RespCertificate(Set[Vote]) - -type ResponseMsg = { - client: Address, - server: Address, - height: Height, - response: Response, -} - -pure def emptyResponseMsg = { - client: "", - server: "", - height: -1, - response: RespBlock(emptyProposal), -} - -type SynchronizerOutput = - | SOCertificate(Set[Vote]) - | SOBlock(Proposal) - | SONoOutput - - - -// **************************************************************************** -// Synchronizer (client side) -// **************************************************************************** - - -/// The state of the synchronizer -type Synchronizer = { - id: Address, - height: Height, - peers: Set[Address], // MVP: this is going to be the validator set for now - // so we use addresses. We might use peerID in the future - peerStatus: Address -> SyncStatus, - openRequests: Set[RequestMsg], - lastSyncedHeight: Height, // "done" if greater than or equal to height - // TODO: we could add buffers for certificates and values - // inbuffers - statusMsgs: Set[SyncStatusMsg], - responses: Set[ResponseMsg], -} - -// -// Synchronizer functions -// - -/// Initialize the synchronizer -pure def initSynchronizer(id: Address, peers: Set[Address]) : Synchronizer = - { id: id, - height: -1, - peers: peers, - peerStatus: peers.mapBy(x => {base:-1, top:-1}), - openRequests: Set(), - lastSyncedHeight: -1, - statusMsgs: Set(), - responses: Set(), - } - -/// Auxiliary function to iterate over the received status messages -pure def updatePeerStatus (ps: Address -> SyncStatus, msgs: Set[SyncStatusMsg]) : Address -> SyncStatus = - 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 - ) - -/// inform the synchronizer that consensus has entered height h -pure def syncNewHeight (s: Synchronizer, h: Height) : Synchronizer = - if (h <= s.height) - s - else - s.with("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 -type ClientResult = { - sync: Synchronizer, - so: SynchronizerOutput, - req: Option[RequestMsg] -} - -/// We have received a certificate. now we need to issue the corresponding block request -/// and generate a certificate output -pure def syncHandleCertificate (s: Synchronizer, 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)} - -/// we have received a block. now we need to generate a block output -pure def syncHandleBlock (s: Synchronizer, 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} - -/// step of a client: -/// 1. update peer statuses, 2. if there is no open request, request something -/// 3. otherwise check whether we have a response and act accordingly -pure def syncClient (s: Synchronizer) : ClientResult = - 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} - else - val goodPeers = s.peers.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: 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.responses.size()> 0) - val resp = s.responses.fold(emptyResponseMsg, (acc, i) => i) //chooseSome() // in the future there might be parallelization - - match resp.response { - | RespBlock(prop) => syncHandleBlock(newS, prop) - | RespCertificate(cert) => syncHandleCertificate(newS, cert, goodPeers.fold("", (s,x) => x)) - } - 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} - - - - -// **************************************************************************** -// Server -// **************************************************************************** - - -/// The server state are just incoming requests. The actual data used to respond -/// is from the NodeState -type Server = { - inbuffer : Set[RequestMsg] -} - -// -// Server functions -// - -pure def initServer = {inbuffer : Set()} - - -/// look into the node state and generate a status message -pure def syncStatus (s: NodeState) : SyncStatusMsg = -// TODO: perhaps we should add to height to the chain entries to capture non-zero bases - { peer: s.es.cs.p , base: 0, top: s.es.chain.length() - 1 } - -/// new server state and response messages to be sent -type ServerOutput = { - sync: Server, - msg: Option[ResponseMsg], -} - -pure def syncServer (s: Server, ns: NodeState) : ServerOutput = - if (s.inbuffer.size() > 0) - val m = s.inbuffer.fold(emptyReqMsg, (acc, i) => i) // chooseSome() // TODO: fix - val result = - if (m.height < ns.es.chain.length()) - match m.rtype { - | SyncCertificate => - val cm = { client: m.client, - server: m.server, - height: m.height, - response: RespCertificate(ns.es.chain[m.height].commit)} - Some(cm) - | SyncBlock => - val bl = { client: m.client, - server: m.server, - height: m.height, - response: RespBlock(ns.es.chain[m.height].decision)} - Some(bl) - } - else None - { sync: { ...s, inbuffer: s.inbuffer.exclude(Set(m))}, - msg: result} - else { - sync: s, - msg: None} - - - - - - - - -// **************************************************************************** -// State machine -// **************************************************************************** - - - - -// -// The statemachine is put on top of statemachineAsync, that is, we use its -// initialization and steps, and add the updates to the variables defined below -// - - - -// Variables - -var syncSystem: Address -> Synchronizer -var serverSystem: Address -> Server - -var statusBuffer : Address -> Set[SyncStatusMsg] -var syncResponseBuffer : Address -> Set[ResponseMsg] -var syncRequestBuffer : Address -> Set[RequestMsg] - - -// Auxiliary functions for sending messages - -pure def broadcastStatus(buffer: Address -> Set[SyncStatusMsg], sm: SyncStatusMsg): Address -> Set[SyncStatusMsg] = - buffer.keys().mapBy(x => { ...buffer.get(x).union(Set(sm)) }) - -/// put the response message in the buffer of the client -pure def sendResponse(buffer: Address -> Set[ResponseMsg], m: ResponseMsg): Address -> Set[ResponseMsg] = - buffer.put(m.client, { ...buffer.get(m.client).union(Set(m)) }) - -// -// Actions -// - -/// initializing the variables of the sync part of the state machine -action syncInit = all { - syncSystem' = Correct.mapBy(v => initSynchronizer(v, validators)), - serverSystem' = Correct.mapBy(v => initServer), - statusBuffer' = Correct.mapBy(v => Set()), - syncResponseBuffer' = Correct.mapBy (v => Set()), - syncRequestBuffer' = Correct.mapBy(v => Set()), -} - -action syncUnchangedAll = all { - serverSystem' = serverSystem, - syncRequestBuffer' = syncRequestBuffer, - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer, - syncSystem' = syncSystem, -} - -/// initialize consensus and synchronizer -action initAll = all { - init, - syncInit -} - -// -// Actions for the Environment to send a node to a new height -// - -/// environment sends the node to the next height. -/// initializes synchronizer -action newHeightActionSync(v, valset, h) = all { - syncSystem' = syncSystem.put(v, syncNewHeight(syncSystem.get(v), h)), - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer, - serverSystem' = serverSystem, - syncRequestBuffer' = syncRequestBuffer, -} - -/// environment sends the node to the next height. -action newHeightActionAll(v, valset, h) = all { - newHeightActionSync(v, valset, h), - newHeightAction(v, valset, h), -} - -// -// Actions for process steps in the sync protocol -// - -/// Server v announces its status -action syncStatusStep(v) = all { - val newStatus = system.get(v).syncStatus() - statusBuffer' = broadcastStatus(statusBuffer, newStatus), - syncResponseBuffer' = syncResponseBuffer, - syncSystem' = syncSystem, - serverSystem' = serverSystem, - syncRequestBuffer' = syncRequestBuffer, - unchangedAll -} - -/// Server v takes a step (checking for requests and responding) -action syncStepServer(v) = all { - val result = syncServer(serverSystem.get(v), system.get(v)) // this is where the chains is passed - all { - serverSystem' = serverSystem.put(v, result.sync), - syncResponseBuffer' = match result.msg { - | Some(m) => syncResponseBuffer.sendResponse(m) // TODO: fix after broadcast - | None => syncResponseBuffer - }, - syncSystem' = syncSystem, - syncRequestBuffer' = syncRequestBuffer, - statusBuffer' = statusBuffer, - unchangedAll, - } -} - -/// Client v takes a step -action syncStepClient(v) = all { - val result = syncClient(syncSystem.get(v)) - all { - syncSystem' = syncSystem.put(v, result.sync), - syncRequestBuffer' = match result.req { - | Some(m) => syncRequestBuffer.put(m.server, syncRequestBuffer.get(m.server).union(Set(m))) - | None => syncRequestBuffer - }, - putSyncOutputIntoNode(v, result.so), // the logic's code should be here, but due to Quint issues - // we need to keep it in stateMachineAsync for now - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer, - serverSystem' = serverSystem, - } -} - - - - -// -// Actions for the environment to deliver messages in the sync protocol -// - -/// deliver a request to server v -/// remove the request from the syncRequestBuffer and add it to the server's inbuffer. -action syncDeliverReq(v) = all { - syncRequestBuffer.get(v).size() > 0, - nondet req = syncRequestBuffer.get(v).oneOf() - all { - syncRequestBuffer' = syncRequestBuffer.put(v, syncRequestBuffer.get(v).exclude(Set(req))), - serverSystem' = serverSystem.put(v, {... serverSystem.get(v), - inbuffer: serverSystem.get(v).inbuffer.union(Set(req))}), - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer, - syncSystem' = syncSystem, - unchangedAll - } -} - -/// deliver a response to client v -/// remove the response from the syncResponseBuffer and add it to the client's responses buffer. -action syncDeliverResp(v) = all { - syncResponseBuffer.get(v).size() > 0, - nondet resp = syncResponseBuffer.get(v).oneOf() - all { - syncSystem' = syncSystem.put(v, {... syncSystem.get(v), - responses: syncSystem.get(v).responses.union(Set(resp))}), - syncRequestBuffer' = syncRequestBuffer, - serverSystem' = serverSystem, - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer.put(v, syncResponseBuffer.get(v).exclude(Set(resp))), - unchangedAll - } -} - -/// deliver a status message to client v -action syncDeliverStatus(v) = all { - statusBuffer.get(v).size() > 0, - nondet status = statusBuffer.get(v).oneOf() - all { - syncSystem' = syncSystem.put(v, {... syncSystem.get(v), - statusMsgs: syncSystem.get(v).statusMsgs.union(Set(status))}), - syncRequestBuffer' = syncRequestBuffer, - serverSystem' = serverSystem, - statusBuffer' = statusBuffer.put(v, statusBuffer.get(v).exclude(Set(status))), - syncResponseBuffer' = syncResponseBuffer, - unchangedAll - } -} - -/// validator step in the system with sync protocol -action syncValStep(v) = all { - valStep(v), - syncUnchangedAll -} - -/// main step function: either a consensus state-machine step or a sync protocol step -action stepWithBlockSync = any { - all { - step, - syncUnchangedAll - }, - nondet v = oneOf(Correct) - any { - syncDeliverReq(v), - syncDeliverResp(v), - syncDeliverStatus(v), - syncStepServer(v), //looking for a request and sends responses - syncStepClient(v), // is checking if there are responses and check whether it need to requ - syncStatusStep(v), - //syncTimeout(v) // TODO: - } -} - - - -// -// Interesting scenarios -// - -/// auxiliary function for initHeight -/// sets the chain -pure def setChain(s: DriverState, c: List[{decision: Proposal, commit: Set[Vote]}]): DriverState = - {... s, chain: c} - -/// auxiliary function for initHeight -/// constructs a commit certificate for a height and value -pure def commitSet (h: Height, v: Value) : Set[Vote] = - Set("v1", "v2", "v3").map(n => mkVote(Precommit, n, h, 0, v)) - -/// An action to set up an initial state with some nodes already decided up to height h -/// this sets up an initial state where v4 starts late, and v2 and v3 have reached -/// height h -action initHeight(h) = all { - val special = "v4" // TODO proper selection from correct set - val initsystem = Correct.mapBy(v => - // hack - if (v == special) initNode(v, validatorSet, 0) - else initNode(v, validatorSet, h)) - nondet decisionValMap = 0.to(h-1).setOfMaps(Values).oneOf() - val propMap = decisionValMap.keys().mapBy(i => - mkProposal( proposer(validatorSet, i,0), - i, - 0, - decisionValMap.get(i), - 0)) - val list = range(0, h).foldl(List(), (acc, i) => acc.append(propMap.get(i))) - val chain = list.foldl(List(), (acc, i) => acc.append({decision: i, commit: commitSet(i.height, Val(i.proposal))})) - all { - system' = initsystem.keys().mapBy(x => - // hack - if (x == special) initsystem.get(x) - else {... initsystem.get(x), es: setChain(initsystem.get(x).es, chain) }), - propBuffer' = Correct.mapBy(v => Set()), - voteBuffer' = Correct.mapBy(v => Set()), - certBuffer' = Correct.mapBy(v => Set()), - _hist' = { validator: "INIT", input: NoDInput, output: NoConsensusOutput }, - syncInit - } -} - -/// a simple scenario where v4 starts height h -run syncCycle(h) = - newHeightActionAll("v4", validatorSet, h) - .then(syncStatusStep("v2")) - .then(syncDeliverStatus("v4")) - .then(syncStepClient("v4")) // ask for certificate - .then(syncDeliverReq("v2")) - .then(syncStepServer("v2")) - .then(syncDeliverResp("v4")) - .then(syncStepClient("v4")) // ask for block and give certificate to node - .expect(system.get("v4").incomingSyncCertificates.size() > 0) - .then(syncDeliverReq("v2")) - .then(syncStepServer("v2")) - .then(syncDeliverResp("v4")) - .then(syncStepClient("v4")) - .expect(system.get("v4").incomingSyncProposals.size() > 0) - .then(3.reps(_ => syncValStep("v4"))) - .expect(system.get("v4").es.chain.length() > h) - -run retreat = - nondet heightToReach = 1.to(4).oneOf() - initHeight( q::debug ("Height:", heightToReach)) - .then(heightToReach.reps(i => syncCycle(i))) - .expect(system.get("v4").es.chain == system.get("v2").es.chain) - .then(newHeightActionAll("v4", validatorSet, heightToReach)) - .expect(system.get("v4").es.cs.height == system.get("v2").es.cs.height) - // and now v4 has synced ! - - - - -} \ No newline at end of file From bb9c380995c2f7a60822b92b06647f9a86cc6747 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 11 Nov 2024 17:44:36 +0100 Subject: [PATCH 22/33] spec/quint: fixing blocksync/sync.qnt module --- specs/quint/specs/blocksync/sync.qnt | 1 - 1 file changed, 1 deletion(-) diff --git a/specs/quint/specs/blocksync/sync.qnt b/specs/quint/specs/blocksync/sync.qnt index 985953731..7813f998e 100644 --- a/specs/quint/specs/blocksync/sync.qnt +++ b/specs/quint/specs/blocksync/sync.qnt @@ -141,7 +141,6 @@ module sync { serverSystem' = serverSystem, } } ->>>>>>> 8eadaf1 (spec/quint: spacing changes) // // Actions for the environment to deliver messages in the sync protocol From 390dbf15450a109bdb0e77bdc712e2663970948c Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 11 Nov 2024 17:50:10 +0100 Subject: [PATCH 23/33] spec/quint: sync Server has an id : Address --- specs/quint/specs/blocksync/server.qnt | 15 +++++++++------ specs/quint/specs/blocksync/sync.qnt | 4 ++-- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/specs/quint/specs/blocksync/server.qnt b/specs/quint/specs/blocksync/server.qnt index eb256f028..cbe4afd5e 100644 --- a/specs/quint/specs/blocksync/server.qnt +++ b/specs/quint/specs/blocksync/server.qnt @@ -14,6 +14,7 @@ module server { /// The server state are just incoming requests. The actual data used to respond /// is from the NodeState type Server = { + id: Address, inbuffer : Set[RequestMsg] } @@ -21,14 +22,16 @@ module server { // Server functions // - pure def initServer = {inbuffer : Set()} + pure def initServer(addr: Address) : Server = { + id: addr, + inbuffer : Set() + } /// look into the node state and generate a status message - pure def syncStatus (s: NodeState) : SyncStatusMsg = + pure def syncStatus (server: Server, s: NodeState) : SyncStatusMsg = // TODO: perhaps we should add to height to the chain entries to capture non-zero bases - // TODO: s.es.cs.p is static, easy to keep in the Server // TODO: the driver can maintain a copy of them `chain` - { peer: s.es.cs.p , base: 0, top: s.es.chain.length() - 1 } + { peer: server.id , base: 0, top: s.es.chain.length() - 1 } /// new server state and response messages to be sent type ServerOutput = { @@ -45,13 +48,13 @@ module server { match m.rtype { | SyncCertificate => val cm = { client: m.client, - server: m.server, + server: s.id, height: m.height, response: RespCertificate(ns.es.chain[m.height].commit)} Some(cm) | SyncBlock => val bl = { client: m.client, - server: m.server, + server: s.id, height: m.height, response: RespBlock(ns.es.chain[m.height].decision)} Some(bl) diff --git a/specs/quint/specs/blocksync/sync.qnt b/specs/quint/specs/blocksync/sync.qnt index 7813f998e..f3f518c73 100644 --- a/specs/quint/specs/blocksync/sync.qnt +++ b/specs/quint/specs/blocksync/sync.qnt @@ -54,7 +54,7 @@ module sync { /// initializing the variables of the sync part of the state machine action syncInit = all { syncSystem' = Correct.mapBy(v => initSynchronizer(v, validators)), - serverSystem' = Correct.mapBy(v => initServer), + serverSystem' = Correct.mapBy(v => initServer(v)), statusBuffer' = Correct.mapBy(v => Set()), syncResponseBuffer' = Correct.mapBy (v => Set()), syncRequestBuffer' = Correct.mapBy(v => Set()), @@ -100,7 +100,7 @@ module sync { /// Server v announces its status action syncStatusStep(v) = all { - val newStatus = system.get(v).syncStatus() + val newStatus = serverSystem.get(v).syncStatus(system.get(v)) statusBuffer' = broadcastStatus(statusBuffer, newStatus), syncResponseBuffer' = syncResponseBuffer, syncSystem' = syncSystem, From eaa90e76d94c4df962307c83deffe1d3e14b7965 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 11 Nov 2024 18:22:58 +0100 Subject: [PATCH 24/33] spec/quint: move BlockStoreEntry to types.qnt --- specs/quint/specs/driver.qnt | 5 ----- specs/quint/specs/types.qnt | 7 +++++++ 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/specs/quint/specs/driver.qnt b/specs/quint/specs/driver.qnt index cfc9ca3fa..893f9a231 100644 --- a/specs/quint/specs/driver.qnt +++ b/specs/quint/specs/driver.qnt @@ -11,11 +11,6 @@ module driver { // State // ************************************************************************* - type BlockStoreEntry = { - decision: Proposal, - commit: Set[Vote] - } - type DriverState = { bk: Bookkeeper, cs: ConsensusState, diff --git a/specs/quint/specs/types.qnt b/specs/quint/specs/types.qnt index ef711b7bf..a1103a5ea 100644 --- a/specs/quint/specs/types.qnt +++ b/specs/quint/specs/types.qnt @@ -21,6 +21,7 @@ module types { | Val(v) => v | Nil => "getVal error" // this should not happen } + pure def isValid(value: NonNilValue): bool = // for simulation, if the value is "invalid", so is the proposal // if this is to become "non-deterministic", we must push it @@ -84,4 +85,10 @@ module types { | Commit(Set[Vote]) + // Commited blocks store + type BlockStoreEntry = { + decision: Proposal, + commit: Set[Vote] + } + } From bee0d606dabe0b2cd77bbe8e103e48f42dc3ab4a Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 11 Nov 2024 18:40:06 +0100 Subject: [PATCH 25/33] specs/quint: blocksync Server keeps a chain copy --- specs/quint/specs/blocksync/server.qnt | 45 ++++++++++++++------------ specs/quint/specs/blocksync/sync.qnt | 22 ++++++++----- 2 files changed, 39 insertions(+), 28 deletions(-) diff --git a/specs/quint/specs/blocksync/server.qnt b/specs/quint/specs/blocksync/server.qnt index cbe4afd5e..da85472df 100644 --- a/specs/quint/specs/blocksync/server.qnt +++ b/specs/quint/specs/blocksync/server.qnt @@ -4,34 +4,39 @@ // **************************************************************************** module server { - import driver.* from "../driver" import blocksync.* from "./blocksync" - // TODO: this should be changed. The data from NodeState we rely on - // should be stored (copied) into the server state. In this way we get - // rid from the dependency on the driver, rendering the server - // self-contained and easier to test. - /// The server state are just incoming requests. The actual data used to respond - /// is from the NodeState type Server = { id: Address, + chain: List[BlockStoreEntry], + + // Incoming requests inbuffer : Set[RequestMsg] } - // - // Server functions - // - pure def initServer(addr: Address) : Server = { id: addr, + chain: List(), inbuffer : Set() } - /// look into the node state and generate a status message - pure def syncStatus (server: Server, s: NodeState) : SyncStatusMsg = + // + // Server functions + // + + // generate a status message + pure def syncStatus (server: Server) : SyncStatusMsg = // TODO: perhaps we should add to height to the chain entries to capture non-zero bases - // TODO: the driver can maintain a copy of them `chain` - { peer: server.id , base: 0, top: s.es.chain.length() - 1 } + { peer: server.id , base: 0, top: server.chain.length() - 1 } + + // update the server state from the node state + // at the moment this means updating the server's copy of the chain + pure def updateServer(s: Server, chain: List[BlockStoreEntry]) : Server = { + if (chain.length() > s.chain.length()) + { ...s, chain: chain } + else // FIXME: can it ever happen? + s + } /// new server state and response messages to be sent type ServerOutput = { @@ -39,24 +44,24 @@ module server { msg: Option[ResponseMsg], } - pure def syncServer (s: Server, ns: NodeState) : ServerOutput = - // TODO: the driver can maintain a copy of them `chain` + // main method: respond to incoming request, if any + pure def syncServer (s: Server) : ServerOutput = if (s.inbuffer.size() > 0) val m = s.inbuffer.fold(emptyReqMsg, (acc, i) => i) // chooseSome() // TODO: fix val result = - if (m.height < ns.es.chain.length()) + if (m.height < s.chain.length()) match m.rtype { | SyncCertificate => val cm = { client: m.client, server: s.id, height: m.height, - response: RespCertificate(ns.es.chain[m.height].commit)} + response: RespCertificate(s.chain[m.height].commit)} Some(cm) | SyncBlock => val bl = { client: m.client, server: s.id, height: m.height, - response: RespBlock(ns.es.chain[m.height].decision)} + response: RespBlock(s.chain[m.height].decision)} Some(bl) } else None diff --git a/specs/quint/specs/blocksync/sync.qnt b/specs/quint/specs/blocksync/sync.qnt index f3f518c73..25961c689 100644 --- a/specs/quint/specs/blocksync/sync.qnt +++ b/specs/quint/specs/blocksync/sync.qnt @@ -100,18 +100,24 @@ module sync { /// Server v announces its status action syncStatusStep(v) = all { - val newStatus = serverSystem.get(v).syncStatus(system.get(v)) - statusBuffer' = broadcastStatus(statusBuffer, newStatus), - syncResponseBuffer' = syncResponseBuffer, - syncSystem' = syncSystem, - serverSystem' = serverSystem, - syncRequestBuffer' = syncRequestBuffer, - unchangedAll + val chain = system.get(v).es.chain + val server = serverSystem.get(v).updateServer(chain) + val newStatus = server.syncStatus() + all { + serverSystem' = serverSystem.put(v, server), + statusBuffer' = broadcastStatus(statusBuffer, newStatus), + syncResponseBuffer' = syncResponseBuffer, + syncSystem' = syncSystem, + syncRequestBuffer' = syncRequestBuffer, + unchangedAll, + } } /// Server v takes a step (checking for requests and responding) action syncStepServer(v) = all { - val result = syncServer(serverSystem.get(v), system.get(v)) // this is where the chains is passed + val chain = system.get(v).es.chain + val server = serverSystem.get(v).updateServer(chain) + val result = server.syncServer() all { serverSystem' = serverSystem.put(v, result.sync), syncResponseBuffer' = match result.msg { From 96cdf25d457a1c3bf206211f739d6279ea87666b Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 11 Nov 2024 18:41:34 +0100 Subject: [PATCH 26/33] specs/quint: pleasing the linter --- specs/quint/specs/types.qnt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specs/quint/specs/types.qnt b/specs/quint/specs/types.qnt index a1103a5ea..b20bf57d1 100644 --- a/specs/quint/specs/types.qnt +++ b/specs/quint/specs/types.qnt @@ -85,7 +85,7 @@ module types { | Commit(Set[Vote]) - // Commited blocks store + // Committed blocks store type BlockStoreEntry = { decision: Proposal, commit: Set[Vote] From bc24ff1684b2c503b26d9a861d87cbb1869c4331 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Thu, 14 Nov 2024 10:36:03 +0100 Subject: [PATCH 27/33] spec/quint: updateServer is now an action --- specs/quint/specs/blocksync/server.qnt | 9 -------- specs/quint/specs/blocksync/sync.qnt | 32 +++++++++++++++++++++----- 2 files changed, 26 insertions(+), 15 deletions(-) diff --git a/specs/quint/specs/blocksync/server.qnt b/specs/quint/specs/blocksync/server.qnt index da85472df..97e6f3954 100644 --- a/specs/quint/specs/blocksync/server.qnt +++ b/specs/quint/specs/blocksync/server.qnt @@ -29,15 +29,6 @@ module server { // TODO: perhaps we should add to height to the chain entries to capture non-zero bases { peer: server.id , base: 0, top: server.chain.length() - 1 } - // update the server state from the node state - // at the moment this means updating the server's copy of the chain - pure def updateServer(s: Server, chain: List[BlockStoreEntry]) : Server = { - if (chain.length() > s.chain.length()) - { ...s, chain: chain } - else // FIXME: can it ever happen? - s - } - /// new server state and response messages to be sent type ServerOutput = { sync: Server, diff --git a/specs/quint/specs/blocksync/sync.qnt b/specs/quint/specs/blocksync/sync.qnt index 25961c689..ebb14c413 100644 --- a/specs/quint/specs/blocksync/sync.qnt +++ b/specs/quint/specs/blocksync/sync.qnt @@ -98,10 +98,26 @@ module sync { // Actions for process steps in the sync protocol // + // update the server state given the node blockchain content + action updateServer(v, chain) = all { + val s = serverSystem.get(v) + all { + // FIXME: how much we trust in the equality here? + chain != s.chain, + serverSystem' = serverSystem.put(v, { ...s, chain: chain }), + }, + all { // Nothing changes here + statusBuffer' = statusBuffer, + syncResponseBuffer' = syncResponseBuffer, + syncSystem' = syncSystem, + syncRequestBuffer' = syncRequestBuffer, + unchangedAll, + } + } + /// Server v announces its status action syncStatusStep(v) = all { - val chain = system.get(v).es.chain - val server = serverSystem.get(v).updateServer(chain) + val server = serverSystem.get(v) val newStatus = server.syncStatus() all { serverSystem' = serverSystem.put(v, server), @@ -115,8 +131,7 @@ module sync { /// Server v takes a step (checking for requests and responding) action syncStepServer(v) = all { - val chain = system.get(v).es.chain - val server = serverSystem.get(v).updateServer(chain) + val server = serverSystem.get(v) val result = server.syncServer() all { serverSystem' = serverSystem.put(v, result.sync), @@ -212,12 +227,14 @@ module sync { syncUnchangedAll }, nondet v = oneOf(Correct) + val chain = system.get(v).es.chain any { syncDeliverReq(v), syncDeliverResp(v), syncDeliverStatus(v), - syncStepServer(v), //looking for a request and sends responses - syncStepClient(v), // is checking if there are responses and check whether it need to requ + updateServer(v, chain), // update the server with the latest state of the chain + syncStepServer(v), // looking for a request and sends responses + syncStepClient(v), // is checking if there are responses and check whether it need to requ syncStatusStep(v), //syncTimeout(v) // TODO: } @@ -290,6 +307,9 @@ module sync { run retreat = nondet heightToReach = 1.to(4).oneOf() initHeight( q::debug ("Height:", heightToReach)) + // FIXME: I had to put it here, instead of syncCycle(h) + // This is not ideal, but it works. + .then(updateServer("v2", system.get("v2").es.chain)) .then(heightToReach.reps(i => syncCycle(i))) .expect(system.get("v4").es.chain == system.get("v2").es.chain) .then(newHeightActionAll("v4", validatorSet, heightToReach)) From 23c4c547f37ade70900de41548684a4ce2600c35 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Fri, 15 Nov 2024 11:30:24 +0100 Subject: [PATCH 28/33] spec/quint: move client actions to client.qnt --- specs/quint/specs/blocksync/client.qnt | 36 ++++++++++++++++++++++++++ specs/quint/specs/blocksync/sync.qnt | 25 +++++++----------- 2 files changed, 46 insertions(+), 15 deletions(-) diff --git a/specs/quint/specs/blocksync/client.qnt b/specs/quint/specs/blocksync/client.qnt index f08b4309b..2902130b5 100644 --- a/specs/quint/specs/blocksync/client.qnt +++ b/specs/quint/specs/blocksync/client.qnt @@ -128,4 +128,40 @@ module client { { sync: newS, so: SONoOutput, req: None} + + // Variables + + var syncSystem: Address -> Synchronizer + + action initClient(nodes) = all { + syncSystem' = nodes.mapBy(v => initSynchronizer(v, nodes.exclude(Set(v)))), + } + + action unchangedClient = all { + syncSystem' = syncSystem, + } + + // workaround to update the client state + action updateClient(node, client) = all { + syncSystem' = syncSystem.put(node, client) + } + + action newHeightClient(node, h) = all { + syncSystem' = syncSystem.put(node, syncNewHeight(syncSystem.get(node), h)), + } + + // deliver a status message to node + action deliverStatus(node, msg) = all { + val client = syncSystem.get(node) + syncSystem' = syncSystem.put(node, {... client, + statusMsgs: client.statusMsgs.union(Set(msg))}), + } + + // deliver a response message to node + action deliverResponse(node, msg) = all { + val client = syncSystem.get(node) + syncSystem' = syncSystem.put(node, {... client, + responses: client.responses.union(Set(msg))}), + } + } diff --git a/specs/quint/specs/blocksync/sync.qnt b/specs/quint/specs/blocksync/sync.qnt index ebb14c413..d516750c6 100644 --- a/specs/quint/specs/blocksync/sync.qnt +++ b/specs/quint/specs/blocksync/sync.qnt @@ -25,9 +25,6 @@ module sync { // initialization and steps, and add the updates to the variables defined below // - // Variables - - var syncSystem: Address -> Synchronizer var serverSystem: Address -> Server var statusBuffer : Address -> Set[SyncStatusMsg] @@ -53,7 +50,7 @@ module sync { /// initializing the variables of the sync part of the state machine action syncInit = all { - syncSystem' = Correct.mapBy(v => initSynchronizer(v, validators)), + initClient(validators), serverSystem' = Correct.mapBy(v => initServer(v)), statusBuffer' = Correct.mapBy(v => Set()), syncResponseBuffer' = Correct.mapBy (v => Set()), @@ -65,7 +62,7 @@ module sync { syncRequestBuffer' = syncRequestBuffer, statusBuffer' = statusBuffer, syncResponseBuffer' = syncResponseBuffer, - syncSystem' = syncSystem, + unchangedClient, } /// initialize consensus and synchronizer @@ -81,7 +78,7 @@ module sync { /// environment sends the node to the next height. /// initializes synchronizer action newHeightActionSync(v, valset, h) = all { - syncSystem' = syncSystem.put(v, syncNewHeight(syncSystem.get(v), h)), + newHeightClient(v, h), statusBuffer' = statusBuffer, syncResponseBuffer' = syncResponseBuffer, serverSystem' = serverSystem, @@ -109,7 +106,7 @@ module sync { all { // Nothing changes here statusBuffer' = statusBuffer, syncResponseBuffer' = syncResponseBuffer, - syncSystem' = syncSystem, + unchangedClient, syncRequestBuffer' = syncRequestBuffer, unchangedAll, } @@ -123,7 +120,7 @@ module sync { serverSystem' = serverSystem.put(v, server), statusBuffer' = broadcastStatus(statusBuffer, newStatus), syncResponseBuffer' = syncResponseBuffer, - syncSystem' = syncSystem, + unchangedClient, syncRequestBuffer' = syncRequestBuffer, unchangedAll, } @@ -139,7 +136,7 @@ module sync { | Some(m) => syncResponseBuffer.sendResponse(m) // TODO: fix after broadcast | None => syncResponseBuffer }, - syncSystem' = syncSystem, + unchangedClient, syncRequestBuffer' = syncRequestBuffer, statusBuffer' = statusBuffer, unchangedAll, @@ -150,7 +147,7 @@ module sync { action syncStepClient(v) = all { val result = syncClient(syncSystem.get(v)) all { - syncSystem' = syncSystem.put(v, result.sync), + updateClient(v, result.sync), syncRequestBuffer' = match result.req { | Some(m) => syncRequestBuffer.put(m.server, syncRequestBuffer.get(m.server).union(Set(m))) | None => syncRequestBuffer @@ -178,7 +175,7 @@ module sync { inbuffer: serverSystem.get(v).inbuffer.union(Set(req))}), statusBuffer' = statusBuffer, syncResponseBuffer' = syncResponseBuffer, - syncSystem' = syncSystem, + unchangedClient, unchangedAll } } @@ -189,8 +186,7 @@ module sync { syncResponseBuffer.get(v).size() > 0, nondet resp = syncResponseBuffer.get(v).oneOf() all { - syncSystem' = syncSystem.put(v, {... syncSystem.get(v), - responses: syncSystem.get(v).responses.union(Set(resp))}), + deliverResponse(v, resp), syncRequestBuffer' = syncRequestBuffer, serverSystem' = serverSystem, statusBuffer' = statusBuffer, @@ -204,8 +200,7 @@ module sync { statusBuffer.get(v).size() > 0, nondet status = statusBuffer.get(v).oneOf() all { - syncSystem' = syncSystem.put(v, {... syncSystem.get(v), - statusMsgs: syncSystem.get(v).statusMsgs.union(Set(status))}), + deliverStatus(v, status), syncRequestBuffer' = syncRequestBuffer, serverSystem' = serverSystem, statusBuffer' = statusBuffer.put(v, statusBuffer.get(v).exclude(Set(status))), From b967216dd32c2179f5397bef5f00be44ab7f3325 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Fri, 15 Nov 2024 11:43:42 +0100 Subject: [PATCH 29/33] spec/quint: rename sync client to bsync client --- specs/quint/specs/blocksync/blocksync.qnt | 4 +- specs/quint/specs/blocksync/client.qnt | 77 +++++++++++------------ specs/quint/specs/blocksync/server.qnt | 2 +- specs/quint/specs/blocksync/sync.qnt | 8 +-- 4 files changed, 45 insertions(+), 46 deletions(-) diff --git a/specs/quint/specs/blocksync/blocksync.qnt b/specs/quint/specs/blocksync/blocksync.qnt index a3196e075..9dc4243f1 100644 --- a/specs/quint/specs/blocksync/blocksync.qnt +++ b/specs/quint/specs/blocksync/blocksync.qnt @@ -9,13 +9,13 @@ module blocksync { | Some(a) | None - type SyncStatusMsg = { + type StatusMsg = { peer: Address, base: Height, top: Height } - type SyncStatus = { + type BlockRange = { base: Height, top: Height } diff --git a/specs/quint/specs/blocksync/client.qnt b/specs/quint/specs/blocksync/client.qnt index 2902130b5..d1f8806d7 100644 --- a/specs/quint/specs/blocksync/client.qnt +++ b/specs/quint/specs/blocksync/client.qnt @@ -1,49 +1,48 @@ // -*- mode: Bluespec; -*- -// **************************************************************************** -// Synchronizer (client side) -// **************************************************************************** +// +// Blocksync protocol: client side. -module client { +module bsync_client { import blocksync.* from "./blocksync" /// The state of the synchronizer - type Synchronizer = { + type BsyncClient = { id: Address, - height: Height, - peers: Set[Address], // MVP: this is going to be the validator set for now - // so we use addresses. We might use peerID in the future - peerStatus: Address -> SyncStatus, + + peerStatus: Address -> BlockRange, openRequests: Set[RequestMsg], + + height: Height, lastSyncedHeight: Height, // "done" if greater than or equal to height // TODO: we could add buffers for certificates and values // inbuffers - statusMsgs: Set[SyncStatusMsg], - responses: Set[ResponseMsg], + statusMsgs: Set[StatusMsg], + responseMsgs: Set[ResponseMsg], } - type SynchronizerOutput = + type BsyncClientOutput = | SOCertificate(Set[Vote]) | SOBlock(Proposal) | SONoOutput // - // Synchronizer functions + // BsyncClient functions // /// Initialize the synchronizer - pure def initSynchronizer(id: Address, peers: Set[Address]) : Synchronizer = - { id: id, - height: -1, - peers: peers, + pure def initBsyncClient(id: Address, peers: Set[Address]) : BsyncClient = + { + id: id, peerStatus: peers.mapBy(x => {base:-1, top:-1}), openRequests: Set(), + height: -1, lastSyncedHeight: -1, statusMsgs: Set(), - responses: Set(), + responseMsgs: Set(), } /// Auxiliary function to iterate over the received status messages - pure def updatePeerStatus (ps: Address -> SyncStatus, msgs: Set[SyncStatusMsg]) : Address -> SyncStatus = + 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}) @@ -52,7 +51,7 @@ module client { ) /// inform the synchronizer that consensus has entered height h - pure def syncNewHeight (s: Synchronizer, h: Height) : Synchronizer = + pure def syncNewHeight (s: BsyncClient, h: Height) : BsyncClient = if (h <= s.height) s else @@ -61,14 +60,14 @@ module client { /// returned by the synchronizer: sync is the new state, so is the output towards /// the consensus driver, req are messages sent towards peers/servers type ClientResult = { - sync: Synchronizer, - so: SynchronizerOutput, + sync: BsyncClient, + so: BsyncClientOutput, req: Option[RequestMsg] } /// We have received a certificate. now we need to issue the /// corresponding block request and generate a certificate output. - pure def syncHandleCertificate (s: Synchronizer, cert: Set[Vote], peer: str ) : ClientResult = + pure def syncHandleCertificate (s: BsyncClient, cert: Set[Vote], peer: str ) : ClientResult = val blockReq = { client: s.id, server: peer, rtype: SyncBlock, @@ -78,7 +77,7 @@ module client { req: Some(blockReq)} /// we have received a block. now we need to generate a block output - pure def syncHandleBlock (s: Synchronizer, p: Proposal) : ClientResult = + 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), @@ -87,7 +86,7 @@ module client { /// step of a client: /// 1. update peer statuses, 2. if there is no open request, request something /// 3. otherwise check whether we have a response and act accordingly - pure def syncClient (s: Synchronizer) : ClientResult = + pure def bsyncClient (s: BsyncClient) : ClientResult = val newPeerStates = updatePeerStatus(s.peerStatus, s.statusMsgs) val newS = { ...s, peerStatus: newPeerStates} if (s.lastSyncedHeight >= s.height) @@ -96,7 +95,7 @@ module client { so: SONoOutput, req: None} else - val goodPeers = s.peers.filter(p => newPeerStates.get(p).base <= s.height + 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) @@ -111,8 +110,8 @@ module client { } else // we issued a request before, let's see whether there is a response - if (s.responses.size()> 0) - val resp = s.responses.fold(emptyResponseMsg, (acc, i) => i) //chooseSome() // in the future there might be parallelization + if (s.responseMsgs.size()> 0) + val resp = s.responseMsgs.fold(emptyResponseMsg, (acc, i) => i) //chooseSome() // in the future there might be parallelization match resp.response { | RespBlock(prop) => syncHandleBlock(newS, prop) | RespCertificate(cert) => syncHandleCertificate(newS, cert, goodPeers.fold("", (s,x) => x)) @@ -129,39 +128,39 @@ module client { so: SONoOutput, req: None} - // Variables + // State machine - var syncSystem: Address -> Synchronizer + var bsyncClients: Address -> BsyncClient action initClient(nodes) = all { - syncSystem' = nodes.mapBy(v => initSynchronizer(v, nodes.exclude(Set(v)))), + bsyncClients' = nodes.mapBy(v => initBsyncClient(v, nodes.exclude(Set(v)))), } action unchangedClient = all { - syncSystem' = syncSystem, + bsyncClients' = bsyncClients, } // workaround to update the client state action updateClient(node, client) = all { - syncSystem' = syncSystem.put(node, client) + bsyncClients' = bsyncClients.put(node, client) } action newHeightClient(node, h) = all { - syncSystem' = syncSystem.put(node, syncNewHeight(syncSystem.get(node), h)), + bsyncClients' = bsyncClients.put(node, syncNewHeight(bsyncClients.get(node), h)), } // deliver a status message to node action deliverStatus(node, msg) = all { - val client = syncSystem.get(node) - syncSystem' = syncSystem.put(node, {... client, + val client = bsyncClients.get(node) + bsyncClients' = bsyncClients.put(node, {... client, statusMsgs: client.statusMsgs.union(Set(msg))}), } // deliver a response message to node action deliverResponse(node, msg) = all { - val client = syncSystem.get(node) - syncSystem' = syncSystem.put(node, {... client, - responses: client.responses.union(Set(msg))}), + val client = bsyncClients.get(node) + bsyncClients' = bsyncClients.put(node, {... client, + responseMsgs: client.responseMsgs.union(Set(msg))}), } } diff --git a/specs/quint/specs/blocksync/server.qnt b/specs/quint/specs/blocksync/server.qnt index 97e6f3954..ab6b9430b 100644 --- a/specs/quint/specs/blocksync/server.qnt +++ b/specs/quint/specs/blocksync/server.qnt @@ -25,7 +25,7 @@ module server { // // generate a status message - pure def syncStatus (server: Server) : SyncStatusMsg = + pure def syncStatus (server: Server) : StatusMsg = // TODO: perhaps we should add to height to the chain entries to capture non-zero bases { peer: server.id , base: 0, top: server.chain.length() - 1 } diff --git a/specs/quint/specs/blocksync/sync.qnt b/specs/quint/specs/blocksync/sync.qnt index d516750c6..4e93eba25 100644 --- a/specs/quint/specs/blocksync/sync.qnt +++ b/specs/quint/specs/blocksync/sync.qnt @@ -14,7 +14,7 @@ module sync { Heights = Set(0) // , 1, 2, 3) ).* from "../statemachineAsync" - import client.* from "./client" + import bsync_client.* from "./client" import server.* from "./server" // **************************************************************************** @@ -27,7 +27,7 @@ module sync { var serverSystem: Address -> Server - var statusBuffer : Address -> Set[SyncStatusMsg] + var statusBuffer : Address -> Set[StatusMsg] var syncResponseBuffer : Address -> Set[ResponseMsg] var syncRequestBuffer : Address -> Set[RequestMsg] @@ -37,7 +37,7 @@ module sync { // Auxiliary functions for sending messages - pure def broadcastStatus(buffer: Address -> Set[SyncStatusMsg], sm: SyncStatusMsg): Address -> Set[SyncStatusMsg] = + pure def broadcastStatus(buffer: Address -> Set[StatusMsg], sm: StatusMsg): Address -> Set[StatusMsg] = buffer.keys().mapBy(x => { ...buffer.get(x).union(Set(sm)) }) /// put the response message in the buffer of the client @@ -145,7 +145,7 @@ module sync { /// Client v takes a step action syncStepClient(v) = all { - val result = syncClient(syncSystem.get(v)) + val result = bsyncClient(bsyncClients.get(v)) all { updateClient(v, result.sync), syncRequestBuffer' = match result.req { From b7cbbca9b408b2ef22318771505fca54c5de7d19 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Fri, 15 Nov 2024 11:58:47 +0100 Subject: [PATCH 30/33] spec/quint: server to bsync_server, with its actions --- specs/quint/specs/blocksync/server.qnt | 49 ++++++++++++++++++-------- specs/quint/specs/blocksync/sync.qnt | 37 +++++++++---------- 2 files changed, 52 insertions(+), 34 deletions(-) diff --git a/specs/quint/specs/blocksync/server.qnt b/specs/quint/specs/blocksync/server.qnt index ab6b9430b..3e9fe69ba 100644 --- a/specs/quint/specs/blocksync/server.qnt +++ b/specs/quint/specs/blocksync/server.qnt @@ -1,29 +1,25 @@ // -*- mode: Bluespec; -*- -// **************************************************************************** -// Server -// **************************************************************************** +// +// Blocksync protocol: server side. -module server { +module bsync_server { import blocksync.* from "./blocksync" type Server = { id: Address, + chain: List[BlockStoreEntry], // Incoming requests - inbuffer : Set[RequestMsg] + requestMsgs: Set[RequestMsg] } - pure def initServer(addr: Address) : Server = { + pure def newServer(addr: Address) : Server = { id: addr, chain: List(), - inbuffer : Set() + requestMsgs: Set() } - // - // Server functions - // - // generate a status message pure def syncStatus (server: Server) : StatusMsg = // TODO: perhaps we should add to height to the chain entries to capture non-zero bases @@ -37,8 +33,8 @@ module server { // main method: respond to incoming request, if any pure def syncServer (s: Server) : ServerOutput = - if (s.inbuffer.size() > 0) - val m = s.inbuffer.fold(emptyReqMsg, (acc, i) => i) // chooseSome() // TODO: fix + if (s.requestMsgs.size() > 0) + val m = s.requestMsgs.fold(emptyReqMsg, (acc, i) => i) // chooseSome() // TODO: fix val result = if (m.height < s.chain.length()) match m.rtype { @@ -56,9 +52,34 @@ module server { Some(bl) } else None - { sync: { ...s, inbuffer: s.inbuffer.exclude(Set(m))}, + { sync: { ...s, requestMsgs: s.requestMsgs.exclude(Set(m))}, msg: result} else { sync: s, msg: None} + + // State machine + + var bsyncServers: Address -> Server + + action initServer(nodes) = all { + bsyncServers' = nodes.mapBy(v => newServer(v)), + } + + action unchangedServer = all { + bsyncServers' = bsyncServers, + } + + // workaround to update the server state + action updateServer(node, server) = all { + bsyncServers' = bsyncServers.put(node, server) + } + + // deliver a request message to node + action deliverRequest(node, msg) = all { + val server = bsyncServers.get(node) + bsyncServers' = bsyncServers.put(node, {... server, + requestMsgs: server.requestMsgs.union(Set(msg))}), + } + } diff --git a/specs/quint/specs/blocksync/sync.qnt b/specs/quint/specs/blocksync/sync.qnt index 4e93eba25..52e741742 100644 --- a/specs/quint/specs/blocksync/sync.qnt +++ b/specs/quint/specs/blocksync/sync.qnt @@ -15,7 +15,7 @@ module sync { ).* from "../statemachineAsync" import bsync_client.* from "./client" - import server.* from "./server" + import bsync_server.* from "./server" // **************************************************************************** // State machine @@ -25,8 +25,6 @@ module sync { // initialization and steps, and add the updates to the variables defined below // - var serverSystem: Address -> Server - var statusBuffer : Address -> Set[StatusMsg] var syncResponseBuffer : Address -> Set[ResponseMsg] var syncRequestBuffer : Address -> Set[RequestMsg] @@ -51,17 +49,17 @@ module sync { /// initializing the variables of the sync part of the state machine action syncInit = all { initClient(validators), - serverSystem' = Correct.mapBy(v => initServer(v)), + initServer(validators), statusBuffer' = Correct.mapBy(v => Set()), syncResponseBuffer' = Correct.mapBy (v => Set()), syncRequestBuffer' = Correct.mapBy(v => Set()), } action syncUnchangedAll = all { - serverSystem' = serverSystem, syncRequestBuffer' = syncRequestBuffer, statusBuffer' = statusBuffer, syncResponseBuffer' = syncResponseBuffer, + unchangedServer, unchangedClient, } @@ -81,8 +79,8 @@ module sync { newHeightClient(v, h), statusBuffer' = statusBuffer, syncResponseBuffer' = syncResponseBuffer, - serverSystem' = serverSystem, syncRequestBuffer' = syncRequestBuffer, + unchangedServer, } /// environment sends the node to the next height. @@ -96,12 +94,12 @@ module sync { // // update the server state given the node blockchain content - action updateServer(v, chain) = all { - val s = serverSystem.get(v) + action updateServerChain(v, chain) = all { + val s = bsyncServers.get(v) all { // FIXME: how much we trust in the equality here? chain != s.chain, - serverSystem' = serverSystem.put(v, { ...s, chain: chain }), + bsyncServers' = bsyncServers.put(v, { ...s, chain: chain }), }, all { // Nothing changes here statusBuffer' = statusBuffer, @@ -114,10 +112,10 @@ module sync { /// Server v announces its status action syncStatusStep(v) = all { - val server = serverSystem.get(v) + val server = bsyncServers.get(v) val newStatus = server.syncStatus() all { - serverSystem' = serverSystem.put(v, server), + updateServer(v, server), statusBuffer' = broadcastStatus(statusBuffer, newStatus), syncResponseBuffer' = syncResponseBuffer, unchangedClient, @@ -128,10 +126,10 @@ module sync { /// Server v takes a step (checking for requests and responding) action syncStepServer(v) = all { - val server = serverSystem.get(v) + val server = bsyncServers.get(v) val result = server.syncServer() all { - serverSystem' = serverSystem.put(v, result.sync), + updateServer(v, result.sync), syncResponseBuffer' = match result.msg { | Some(m) => syncResponseBuffer.sendResponse(m) // TODO: fix after broadcast | None => syncResponseBuffer @@ -156,7 +154,7 @@ module sync { // we need to keep it in stateMachineAsync for now statusBuffer' = statusBuffer, syncResponseBuffer' = syncResponseBuffer, - serverSystem' = serverSystem, + unchangedServer, } } @@ -171,8 +169,7 @@ module sync { nondet req = syncRequestBuffer.get(v).oneOf() all { syncRequestBuffer' = syncRequestBuffer.put(v, syncRequestBuffer.get(v).exclude(Set(req))), - serverSystem' = serverSystem.put(v, {... serverSystem.get(v), - inbuffer: serverSystem.get(v).inbuffer.union(Set(req))}), + deliverRequest(v, req), statusBuffer' = statusBuffer, syncResponseBuffer' = syncResponseBuffer, unchangedClient, @@ -188,9 +185,9 @@ module sync { all { deliverResponse(v, resp), syncRequestBuffer' = syncRequestBuffer, - serverSystem' = serverSystem, statusBuffer' = statusBuffer, syncResponseBuffer' = syncResponseBuffer.put(v, syncResponseBuffer.get(v).exclude(Set(resp))), + unchangedServer, unchangedAll } } @@ -202,9 +199,9 @@ module sync { all { deliverStatus(v, status), syncRequestBuffer' = syncRequestBuffer, - serverSystem' = serverSystem, statusBuffer' = statusBuffer.put(v, statusBuffer.get(v).exclude(Set(status))), syncResponseBuffer' = syncResponseBuffer, + unchangedServer, unchangedAll } } @@ -227,7 +224,7 @@ module sync { syncDeliverReq(v), syncDeliverResp(v), syncDeliverStatus(v), - updateServer(v, chain), // update the server with the latest state of the chain + updateServerChain(v, chain), // update the server with the latest state of the chain syncStepServer(v), // looking for a request and sends responses syncStepClient(v), // is checking if there are responses and check whether it need to requ syncStatusStep(v), @@ -304,7 +301,7 @@ module sync { initHeight( q::debug ("Height:", heightToReach)) // FIXME: I had to put it here, instead of syncCycle(h) // This is not ideal, but it works. - .then(updateServer("v2", system.get("v2").es.chain)) + .then(updateServerChain("v2", system.get("v2").es.chain)) .then(heightToReach.reps(i => syncCycle(i))) .expect(system.get("v4").es.chain == system.get("v2").es.chain) .then(newHeightActionAll("v4", validatorSet, heightToReach)) From 0eebb58b86e61df79e15497124492386b0a803d5 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Fri, 15 Nov 2024 12:42:52 +0100 Subject: [PATCH 31/33] spec/quint: moved buffers to blocksync.qnt --- specs/quint/specs/blocksync/blocksync.qnt | 29 +++++++ specs/quint/specs/blocksync/client.qnt | 26 +++++-- specs/quint/specs/blocksync/server.qnt | 13 +++- specs/quint/specs/blocksync/sync.qnt | 95 +++++++---------------- 4 files changed, 86 insertions(+), 77 deletions(-) diff --git a/specs/quint/specs/blocksync/blocksync.qnt b/specs/quint/specs/blocksync/blocksync.qnt index 9dc4243f1..534655400 100644 --- a/specs/quint/specs/blocksync/blocksync.qnt +++ b/specs/quint/specs/blocksync/blocksync.qnt @@ -56,4 +56,33 @@ module blocksync { response: RespBlock(emptyProposal), } + // ************* + // State machine + // ************* + + // Messages exchanged by nodes (clients and servers) + var statusBuffer : Address -> Set[StatusMsg] + var requestsBuffer : Address -> Set[RequestMsg] + var responsesBuffer : Address -> Set[ResponseMsg] + + // Auxiliary functions for sending messages + + pure def broadcastStatus(buffer: Address -> Set[StatusMsg], sm: StatusMsg): Address -> Set[StatusMsg] = + buffer.keys().mapBy(x => { ...buffer.get(x).union(Set(sm)) }) + + // put the response message in the buffer of the client + pure def sendResponse(buffer: Address -> Set[ResponseMsg], m: ResponseMsg): Address -> Set[ResponseMsg] = + buffer.put(m.client, { ...buffer.get(m.client).union(Set(m)) }) + + action initBsync(nodes) = all { + statusBuffer' = nodes.mapBy(v => Set()), + requestsBuffer' = nodes.mapBy(v => Set()), + responsesBuffer' = nodes.mapBy (v => Set()), + } + + action unchangedBsync = all { + statusBuffer' = statusBuffer, + requestsBuffer' = requestsBuffer, + responsesBuffer' = responsesBuffer, + } } diff --git a/specs/quint/specs/blocksync/client.qnt b/specs/quint/specs/blocksync/client.qnt index d1f8806d7..5a5361342 100644 --- a/specs/quint/specs/blocksync/client.qnt +++ b/specs/quint/specs/blocksync/client.qnt @@ -149,18 +149,32 @@ module bsync_client { bsyncClients' = bsyncClients.put(node, syncNewHeight(bsyncClients.get(node), h)), } - // deliver a status message to node - action deliverStatus(node, msg) = all { + // deliver a status message, from the statusBuffer, to node + action deliverStatus(node) = all { + statusBuffer.get(node).size() > 0, val client = bsyncClients.get(node) - bsyncClients' = bsyncClients.put(node, {... client, + nondet msg = statusBuffer.get(node).oneOf() + all { + bsyncClients' = bsyncClients.put(node, {... client, statusMsgs: client.statusMsgs.union(Set(msg))}), + statusBuffer' = statusBuffer.put(node, statusBuffer.get(node).exclude(Set(msg))), + requestsBuffer' = requestsBuffer, + responsesBuffer' = responsesBuffer, + } } - // deliver a response message to node - action deliverResponse(node, msg) = all { + // deliver a response message, from responsesBuffer, to node + action deliverResponse(node) = all { + responsesBuffer.get(node).size() > 0, val client = bsyncClients.get(node) - bsyncClients' = bsyncClients.put(node, {... client, + nondet msg = responsesBuffer.get(node).oneOf() + all { + bsyncClients' = bsyncClients.put(node, {... client, responseMsgs: client.responseMsgs.union(Set(msg))}), + requestsBuffer' = requestsBuffer, + responsesBuffer' = responsesBuffer.put(node, responsesBuffer.get(node).exclude(Set(msg))), + statusBuffer' = statusBuffer, + } } } diff --git a/specs/quint/specs/blocksync/server.qnt b/specs/quint/specs/blocksync/server.qnt index 3e9fe69ba..c1bbb7511 100644 --- a/specs/quint/specs/blocksync/server.qnt +++ b/specs/quint/specs/blocksync/server.qnt @@ -75,11 +75,18 @@ module bsync_server { bsyncServers' = bsyncServers.put(node, server) } - // deliver a request message to node - action deliverRequest(node, msg) = all { + // deliver a request message, from requestsBuffer, to node + action deliverRequest(node) = all { + requestsBuffer.get(node).size() > 0, val server = bsyncServers.get(node) - bsyncServers' = bsyncServers.put(node, {... server, + nondet msg = requestsBuffer.get(node).oneOf() + all { + bsyncServers' = bsyncServers.put(node, {... server, requestMsgs: server.requestMsgs.union(Set(msg))}), + statusBuffer' = statusBuffer, + requestsBuffer' = requestsBuffer.put(node, requestsBuffer.get(node).exclude(Set(msg))), + responsesBuffer' = responsesBuffer, + } } } diff --git a/specs/quint/specs/blocksync/sync.qnt b/specs/quint/specs/blocksync/sync.qnt index 52e741742..c1105d842 100644 --- a/specs/quint/specs/blocksync/sync.qnt +++ b/specs/quint/specs/blocksync/sync.qnt @@ -25,22 +25,11 @@ module sync { // initialization and steps, and add the updates to the variables defined below // - var statusBuffer : Address -> Set[StatusMsg] - var syncResponseBuffer : Address -> Set[ResponseMsg] - var syncRequestBuffer : Address -> Set[RequestMsg] // **************************************************************************** // State machine // **************************************************************************** - // Auxiliary functions for sending messages - - pure def broadcastStatus(buffer: Address -> Set[StatusMsg], sm: StatusMsg): Address -> Set[StatusMsg] = - buffer.keys().mapBy(x => { ...buffer.get(x).union(Set(sm)) }) - - /// put the response message in the buffer of the client - pure def sendResponse(buffer: Address -> Set[ResponseMsg], m: ResponseMsg): Address -> Set[ResponseMsg] = - buffer.put(m.client, { ...buffer.get(m.client).union(Set(m)) }) // // Actions @@ -50,17 +39,13 @@ module sync { action syncInit = all { initClient(validators), initServer(validators), - statusBuffer' = Correct.mapBy(v => Set()), - syncResponseBuffer' = Correct.mapBy (v => Set()), - syncRequestBuffer' = Correct.mapBy(v => Set()), + initBsync(validators), } action syncUnchangedAll = all { - syncRequestBuffer' = syncRequestBuffer, - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer, unchangedServer, unchangedClient, + unchangedBsync, } /// initialize consensus and synchronizer @@ -77,9 +62,7 @@ module sync { /// initializes synchronizer action newHeightActionSync(v, valset, h) = all { newHeightClient(v, h), - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer, - syncRequestBuffer' = syncRequestBuffer, + unchangedBsync, unchangedServer, } @@ -102,10 +85,8 @@ module sync { bsyncServers' = bsyncServers.put(v, { ...s, chain: chain }), }, all { // Nothing changes here - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer, unchangedClient, - syncRequestBuffer' = syncRequestBuffer, + unchangedBsync, unchangedAll, } } @@ -117,9 +98,9 @@ module sync { all { updateServer(v, server), statusBuffer' = broadcastStatus(statusBuffer, newStatus), - syncResponseBuffer' = syncResponseBuffer, + responsesBuffer' = responsesBuffer, unchangedClient, - syncRequestBuffer' = syncRequestBuffer, + requestsBuffer' = requestsBuffer, unchangedAll, } } @@ -130,12 +111,12 @@ module sync { val result = server.syncServer() all { updateServer(v, result.sync), - syncResponseBuffer' = match result.msg { - | Some(m) => syncResponseBuffer.sendResponse(m) // TODO: fix after broadcast - | None => syncResponseBuffer + responsesBuffer' = match result.msg { + | Some(m) => responsesBuffer.sendResponse(m) // TODO: fix after broadcast + | None => responsesBuffer }, unchangedClient, - syncRequestBuffer' = syncRequestBuffer, + requestsBuffer' = requestsBuffer, statusBuffer' = statusBuffer, unchangedAll, } @@ -146,14 +127,14 @@ module sync { val result = bsyncClient(bsyncClients.get(v)) all { updateClient(v, result.sync), - syncRequestBuffer' = match result.req { - | Some(m) => syncRequestBuffer.put(m.server, syncRequestBuffer.get(m.server).union(Set(m))) - | None => syncRequestBuffer + requestsBuffer' = match result.req { + | Some(m) => requestsBuffer.put(m.server, requestsBuffer.get(m.server).union(Set(m))) + | None => requestsBuffer }, putSyncOutputIntoNode(v, result.so), // the logic's code should be here, but due to Quint issues // we need to keep it in stateMachineAsync for now statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer, + responsesBuffer' = responsesBuffer, unchangedServer, } } @@ -162,49 +143,27 @@ module sync { // Actions for the environment to deliver messages in the sync protocol // - /// deliver a request to server v - /// remove the request from the syncRequestBuffer and add it to the server's inbuffer. + // deliver a status message to client v + action syncDeliverStatus(v) = all { + deliverStatus(v), + unchangedServer, + unchangedAll + } + + // deliver a request to server v action syncDeliverReq(v) = all { - syncRequestBuffer.get(v).size() > 0, - nondet req = syncRequestBuffer.get(v).oneOf() - all { - syncRequestBuffer' = syncRequestBuffer.put(v, syncRequestBuffer.get(v).exclude(Set(req))), - deliverRequest(v, req), - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer, + deliverRequest(v), unchangedClient, unchangedAll - } } - /// deliver a response to client v - /// remove the response from the syncResponseBuffer and add it to the client's responses buffer. + // deliver a response to client v action syncDeliverResp(v) = all { - syncResponseBuffer.get(v).size() > 0, - nondet resp = syncResponseBuffer.get(v).oneOf() - all { - deliverResponse(v, resp), - syncRequestBuffer' = syncRequestBuffer, - statusBuffer' = statusBuffer, - syncResponseBuffer' = syncResponseBuffer.put(v, syncResponseBuffer.get(v).exclude(Set(resp))), - unchangedServer, - unchangedAll - } + deliverResponse(v), + unchangedServer, + unchangedAll } - /// deliver a status message to client v - action syncDeliverStatus(v) = all { - statusBuffer.get(v).size() > 0, - nondet status = statusBuffer.get(v).oneOf() - all { - deliverStatus(v, status), - syncRequestBuffer' = syncRequestBuffer, - statusBuffer' = statusBuffer.put(v, statusBuffer.get(v).exclude(Set(status))), - syncResponseBuffer' = syncResponseBuffer, - unchangedServer, - unchangedAll - } - } /// validator step in the system with sync protocol action syncValStep(v) = all { From 8e5757e1916a5abbb22c8de1b68f51a01c5851fd Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Fri, 15 Nov 2024 13:14:52 +0100 Subject: [PATCH 32/33] quint/spec: refactoring of client and server methods --- specs/quint/specs/blocksync/blocksync.qnt | 2 +- specs/quint/specs/blocksync/client.qnt | 5 -- specs/quint/specs/blocksync/server.qnt | 45 ++++++++++-- specs/quint/specs/blocksync/sync.qnt | 88 ++++++++++------------- 4 files changed, 76 insertions(+), 64 deletions(-) diff --git a/specs/quint/specs/blocksync/blocksync.qnt b/specs/quint/specs/blocksync/blocksync.qnt index 534655400..0f4bae6ab 100644 --- a/specs/quint/specs/blocksync/blocksync.qnt +++ b/specs/quint/specs/blocksync/blocksync.qnt @@ -67,7 +67,7 @@ module blocksync { // Auxiliary functions for sending messages - pure def broadcastStatus(buffer: Address -> Set[StatusMsg], sm: StatusMsg): Address -> Set[StatusMsg] = + pure def broadcastStatusMsg(buffer: Address -> Set[StatusMsg], sm: StatusMsg): Address -> Set[StatusMsg] = buffer.keys().mapBy(x => { ...buffer.get(x).union(Set(sm)) }) // put the response message in the buffer of the client diff --git a/specs/quint/specs/blocksync/client.qnt b/specs/quint/specs/blocksync/client.qnt index 5a5361342..84215d511 100644 --- a/specs/quint/specs/blocksync/client.qnt +++ b/specs/quint/specs/blocksync/client.qnt @@ -140,11 +140,6 @@ module bsync_client { bsyncClients' = bsyncClients, } - // workaround to update the client state - action updateClient(node, client) = all { - bsyncClients' = bsyncClients.put(node, client) - } - action newHeightClient(node, h) = all { bsyncClients' = bsyncClients.put(node, syncNewHeight(bsyncClients.get(node), h)), } diff --git a/specs/quint/specs/blocksync/server.qnt b/specs/quint/specs/blocksync/server.qnt index c1bbb7511..5d6c359da 100644 --- a/specs/quint/specs/blocksync/server.qnt +++ b/specs/quint/specs/blocksync/server.qnt @@ -70,12 +70,7 @@ module bsync_server { bsyncServers' = bsyncServers, } - // workaround to update the server state - action updateServer(node, server) = all { - bsyncServers' = bsyncServers.put(node, server) - } - - // deliver a request message, from requestsBuffer, to node + // Deliver a request message, from requestsBuffer, to node action deliverRequest(node) = all { requestsBuffer.get(node).size() > 0, val server = bsyncServers.get(node) @@ -89,4 +84,42 @@ module bsync_server { } } + // Server at node broadcasts its blockchain status + action broadcastStatus(node) = all { + val server = bsyncServers.get(node) + val msg = server.syncStatus() + all { + bsyncServers' = bsyncServers.put(node, server), + statusBuffer' = broadcastStatusMsg(statusBuffer, msg), + requestsBuffer' = requestsBuffer, + responsesBuffer' = responsesBuffer, + } + } + + // Server at node takes a step (checking for requests and responding) + action stepServer(node) = all { + val server = bsyncServers.get(node) + val result = server.syncServer() + all { + bsyncServers' = bsyncServers.put(node, server), + statusBuffer' = statusBuffer, + requestsBuffer' = requestsBuffer, + responsesBuffer' = match result.msg { + | Some(m) => responsesBuffer.sendResponse(m) + | None => responsesBuffer + }, + } + } + + // Updates the server status, the latest available blockchain content. + // This action must be called by the component that knows the chain. + action updateServer(node, chain) = all { + val server = bsyncServers.get(node) + all { + chain != server.chain, + bsyncServers' = bsyncServers.put(node, { ...server, chain: chain }), + unchangedBsync, + } + } + } diff --git a/specs/quint/specs/blocksync/sync.qnt b/specs/quint/specs/blocksync/sync.qnt index c1105d842..14c49f6e5 100644 --- a/specs/quint/specs/blocksync/sync.qnt +++ b/specs/quint/specs/blocksync/sync.qnt @@ -25,16 +25,6 @@ module sync { // initialization and steps, and add the updates to the variables defined below // - - // **************************************************************************** - // State machine - // **************************************************************************** - - - // - // Actions - // - /// initializing the variables of the sync part of the state machine action syncInit = all { initClient(validators), @@ -76,71 +66,63 @@ module sync { // Actions for process steps in the sync protocol // - // update the server state given the node blockchain content - action updateServerChain(v, chain) = all { - val s = bsyncServers.get(v) + // Update server v from the consensus' blockchain + action syncUpdateServer(v) = all { + val chain = system.get(v).es.chain all { - // FIXME: how much we trust in the equality here? - chain != s.chain, - bsyncServers' = bsyncServers.put(v, { ...s, chain: chain }), - }, - all { // Nothing changes here + updateServer(v, chain), unchangedClient, - unchangedBsync, unchangedAll, } } - /// Server v announces its status + // Server v announces its status action syncStatusStep(v) = all { - val server = bsyncServers.get(v) - val newStatus = server.syncStatus() all { - updateServer(v, server), - statusBuffer' = broadcastStatus(statusBuffer, newStatus), - responsesBuffer' = responsesBuffer, + broadcastStatus(v), unchangedClient, - requestsBuffer' = requestsBuffer, unchangedAll, } } - /// Server v takes a step (checking for requests and responding) + // Server v takes a step (checking for requests and responding) action syncStepServer(v) = all { - val server = bsyncServers.get(v) - val result = server.syncServer() all { - updateServer(v, result.sync), - responsesBuffer' = match result.msg { - | Some(m) => responsesBuffer.sendResponse(m) // TODO: fix after broadcast - | None => responsesBuffer - }, + stepServer(v), unchangedClient, - requestsBuffer' = requestsBuffer, - statusBuffer' = statusBuffer, unchangedAll, } } - /// Client v takes a step + // Client v takes a step + // + // FIXME: here we need to apply the client output to the consensus + // state machine. Refactoring this method is much more complex. + // action syncStepClient(v) = all { val result = bsyncClient(bsyncClients.get(v)) all { - updateClient(v, result.sync), + // TODO: this block should be implmented in client.qnt + bsyncClients' = bsyncClients.put(v, result.sync), + statusBuffer' = statusBuffer, requestsBuffer' = match result.req { | Some(m) => requestsBuffer.put(m.server, requestsBuffer.get(m.server).union(Set(m))) | None => requestsBuffer }, - putSyncOutputIntoNode(v, result.so), // the logic's code should be here, but due to Quint issues - // we need to keep it in stateMachineAsync for now - statusBuffer' = statusBuffer, responsesBuffer' = responsesBuffer, + unchangedServer, + + // This is the part that interacts with the consensus state + // machine. Moreover, the logic's code should be here, but due + // to Quint issues we need to keep it in stateMachineAsync. + putSyncOutputIntoNode(v, result.so), } } // // Actions for the environment to deliver messages in the sync protocol + // Implemented by the blocksync server or client. // // deliver a status message to client v @@ -150,13 +132,6 @@ module sync { unchangedAll } - // deliver a request to server v - action syncDeliverReq(v) = all { - deliverRequest(v), - unchangedClient, - unchangedAll - } - // deliver a response to client v action syncDeliverResp(v) = all { deliverResponse(v), @@ -164,8 +139,18 @@ module sync { unchangedAll } + // deliver a request to server v + action syncDeliverReq(v) = all { + deliverRequest(v), + unchangedClient, + unchangedAll + } + + // + // Complex actions for a validator: consensus and blocksync + // - /// validator step in the system with sync protocol + // validator step in the system with sync protocol action syncValStep(v) = all { valStep(v), syncUnchangedAll @@ -178,12 +163,11 @@ module sync { syncUnchangedAll }, nondet v = oneOf(Correct) - val chain = system.get(v).es.chain any { syncDeliverReq(v), syncDeliverResp(v), syncDeliverStatus(v), - updateServerChain(v, chain), // update the server with the latest state of the chain + syncUpdateServer(v), // update the server with the latest state of the chain syncStepServer(v), // looking for a request and sends responses syncStepClient(v), // is checking if there are responses and check whether it need to requ syncStatusStep(v), @@ -260,7 +244,7 @@ module sync { initHeight( q::debug ("Height:", heightToReach)) // FIXME: I had to put it here, instead of syncCycle(h) // This is not ideal, but it works. - .then(updateServerChain("v2", system.get("v2").es.chain)) + .then(syncUpdateServer("v2")) .then(heightToReach.reps(i => syncCycle(i))) .expect(system.get("v4").es.chain == system.get("v2").es.chain) .then(newHeightActionAll("v4", validatorSet, heightToReach)) From 1e564b0af2eee4f4900da667fea49ef00c546c28 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Fri, 15 Nov 2024 13:19:24 +0100 Subject: [PATCH 33/33] spec/quint: pleasing the linter --- specs/quint/specs/blocksync/sync.qnt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specs/quint/specs/blocksync/sync.qnt b/specs/quint/specs/blocksync/sync.qnt index 14c49f6e5..3c64d9786 100644 --- a/specs/quint/specs/blocksync/sync.qnt +++ b/specs/quint/specs/blocksync/sync.qnt @@ -102,7 +102,7 @@ module sync { action syncStepClient(v) = all { val result = bsyncClient(bsyncClients.get(v)) all { - // TODO: this block should be implmented in client.qnt + // TODO: this block should be implemented in client.qnt bsyncClients' = bsyncClients.put(v, result.sync), statusBuffer' = statusBuffer, requestsBuffer' = match result.req {