diff --git a/specs/quint/specs/blocksync/blocksyncClientTest.qnt b/specs/quint/specs/blocksync/blocksyncClientTest.qnt new file mode 100644 index 000000000..e205f3cd0 --- /dev/null +++ b/specs/quint/specs/blocksync/blocksyncClientTest.qnt @@ -0,0 +1,228 @@ +// -*- mode: Bluespec; -*- +// +// Test unit for blocksync client-side protocol. + +module blocksyncClientTest { + + import blocksyncClient.* from "./blocksyncClient" + import blocksync.* from "./blocksync" + + val nodes = Set("v1", "v2", "v3") + val chain = List( + { decision: mkProposal("v3", 0, 0, "block1", -1), + commit: Set() + }, + { decision: mkProposal("v2", 1, 1, "block2", 0), + commit: Set() + } + ) + + var outputs: List[BsyncClientOutput] + + action init = all { + initClient(nodes), + initBsync(nodes), + outputs' = List(), + } + + action addOutput(v, so) = all { + outputs' = if (so == SONoOutput) outputs else outputs.append(so), + } + + action produceStatus(status) = all { + outputs' = outputs, + unchangedClient, + statusBuffer' = broadcastStatusMsg(statusBuffer, status), + requestsBuffer' = requestsBuffer, + responsesBuffer' = responsesBuffer, + } + + action produceResponse(resp) = all { + outputs' = outputs, + unchangedClient, + statusBuffer' = statusBuffer, + requestsBuffer' = requestsBuffer, + responsesBuffer' = sendResponse(responsesBuffer, resp), + } + + // Test clientLogic with "full == false" + run bsClientBasicTest = + init + + // Nothing happens until the height is set + .then(clientLogic("v1", addOutput, false)) + .expect(length(outputs) == 0) + .expect(bsyncClients.get("v1").lastSyncedHeight == -1) + .expect(requestsBuffer.keys().forall(x => requestsBuffer.get(x).size() == 0)) + .then(all { + newHeightClient("v1", 1), + outputs' = outputs, + unchangedBsync, + }) + // We don't react to new height immediately + .expect(length(outputs) == 0) + .expect(requestsBuffer.keys().forall(x => requestsBuffer.get(x).size() == 0)) + .expect(bsyncClients.get("v1").lastSyncedHeight == -1) + + // Nothing happens until status are received + .then(clientLogic("v1", addOutput, false)) + .expect(length(outputs) == 0) + .expect(requestsBuffer.keys().forall(x => requestsBuffer.get(x).size() == 0)) + .expect(bsyncClients.get("v1").lastSyncedHeight == -1) + + // We receive a status report from v3, but nothing for us + .then(produceStatus({ peer: "v3", base: 0, top: 0,})) + .then(all { + deliverStatus("v1"), + outputs' = outputs, + }) + // Nothing happens because the status is bad + .then(clientLogic("v1", addOutput, false)) + .expect(length(outputs) == 0) + .expect(requestsBuffer.keys().forall(x => requestsBuffer.get(x).size() == 0)) + .expect(bsyncClients.get("v1").lastSyncedHeight == -1) + + // We receive a status report from v2 + .then(produceStatus({ peer: "v2", base: 0, top: 1,})) + .then(all { + deliverStatus("v1"), + outputs' = outputs, + }) + // Then we send a certificate request to v2 + .then(clientLogic("v1", addOutput, false)) + .expect(length(outputs) == 0) + .expect(requestsBuffer.keys().forall(x => + if (x != "v2") requestsBuffer.get(x).size() == 0 + else requestsBuffer.get(x).size() == 1)) + .expect(requestsBuffer.get("v2").contains({ + client: "v1", + server: "v2", + rtype: SyncCertificate, + height: 1, + })) + .expect(bsyncClients.get("v1").lastSyncedHeight == -1) + + // The server replies with a certificate + .then(produceResponse({ + client: "v1", + server: "v2", + height: 1, + response: RespCertificate(chain[0].commit), + })) + .then(all { + deliverResponse("v1"), + outputs' = outputs, + }) + + // Then we: (i) produce a certificate output and + // (ii) send a block request to v2. + .then(clientLogic("v1", addOutput, false)) + .expect(length(outputs) == 1) + .expect(outputs[0] == SOCertificate(chain[0].commit)) + .expect(requestsBuffer.keys().forall(x => + if (x != "v2") requestsBuffer.get(x).size() == 0 + else requestsBuffer.get(x).size() == 2)) + .expect(requestsBuffer.get("v2").contains({ + client: "v1", + server: "v2", + rtype: SyncBlock, + height: 1, + })) + .expect(bsyncClients.get("v1").lastSyncedHeight == -1) + + // The server replies with a block + .then(produceResponse({ + client: "v1", + server: "v2", + height: 1, + response: RespBlock(chain[0].decision), + })) + .then(all { + deliverResponse("v1"), + outputs' = outputs, + }) + + .then(clientLogic("v1", addOutput, false)) + .expect(length(outputs) == 2) + .expect(outputs[1] == SOBlock(chain[0].decision)) + .expect(bsyncClients.get("v1").lastSyncedHeight == 1) + + // Test clientLogic with "full == true" + run bsClientBasicFastTest = + init + + // Nothing happens until the height is set + .then(clientLogic("v1", addOutput, true)) + .expect(length(outputs) == 0) + .expect(requestsBuffer.keys().forall(x => requestsBuffer.get(x).size() == 0)) + .then(all { + newHeightClient("v1", 1), + outputs' = outputs, + unchangedBsync, + }) + .expect(bsyncClients.get("v1").lastSyncedHeight == -1) + // We don't react to new height immediately + .expect(length(outputs) == 0) + .expect(requestsBuffer.keys().forall(x => requestsBuffer.get(x).size() == 0)) + + // Nothing happens until status are received + .then(clientLogic("v1", addOutput, true)) + .expect(length(outputs) == 0) + .expect(requestsBuffer.keys().forall(x => requestsBuffer.get(x).size() == 0)) + .expect(bsyncClients.get("v1").lastSyncedHeight == -1) + + // We receive a status report from v3, but nothing for us + .then(produceStatus({ peer: "v3", base: 0, top: 0,})) + .then(all { + deliverStatus("v1"), + outputs' = outputs, + }) + // Nothing happens because the status is bad + .then(clientLogic("v1", addOutput, true)) + .expect(length(outputs) == 0) + .expect(requestsBuffer.keys().forall(x => requestsBuffer.get(x).size() == 0)) + .expect(bsyncClients.get("v1").lastSyncedHeight == -1) + + // We receive a status report from v2 + .then(produceStatus({ peer: "v2", base: 0, top: 1,})) + .then(all { + deliverStatus("v1"), + outputs' = outputs, + }) + // Then we send a certificate request to v2 + .then(clientLogic("v1", addOutput, true)) + .expect(length(outputs) == 0) + .expect(bsyncClients.get("v1").lastSyncedHeight == -1) + .expect(requestsBuffer.keys().forall(x => + if (x != "v2") requestsBuffer.get(x).size() == 0 + else requestsBuffer.get(x).size() == 1)) + .expect(requestsBuffer.get("v2").contains({ + client: "v1", + server: "v2", + rtype: SyncBlockStoreEntry, + height: 1, + })) + + // The server replies with a certificate and block + .then(produceResponse({ + client: "v1", + server: "v2", + height: 1, + response: RespBlockStoreEntry(chain[0]), + })) + .then(all { + deliverResponse("v1"), + outputs' = outputs, + }) + .expect(bsyncClients.get("v1").lastSyncedHeight == -1) + + // Then we produce two outputs and no message + .then(clientLogic("v1", addOutput, true)) + .expect(length(outputs) == 1) + .expect(outputs[0] == SOBlockStoreEntry(chain[0])) + .expect(requestsBuffer.keys().forall(x => + if (x != "v2") requestsBuffer.get(x).size() == 0 + else requestsBuffer.get(x).size() == 1)) + .expect(bsyncClients.get("v1").lastSyncedHeight == 1) + +} diff --git a/specs/quint/specs/blocksync/blocksyncServer.qnt b/specs/quint/specs/blocksync/blocksyncServer.qnt index dcff19fda..bad7fb08e 100644 --- a/specs/quint/specs/blocksync/blocksyncServer.qnt +++ b/specs/quint/specs/blocksync/blocksyncServer.qnt @@ -29,7 +29,7 @@ module blocksyncServer { /// new server state and response messages to be sent type ServerOutput = { - sync: Server, + server: Server, msg: Option[ResponseMsg], } @@ -60,10 +60,10 @@ module blocksyncServer { Some(bs) } else None - { sync: { ...s, requestMsgs: s.requestMsgs.exclude(Set(m))}, + { server: { ...s, requestMsgs: s.requestMsgs.exclude(Set(m))}, msg: result} else { - sync: s, + server: s, msg: None} // @@ -115,7 +115,7 @@ module blocksyncServer { val server = bsyncServers.get(node) val result = server.syncServer() all { - bsyncServers' = bsyncServers.put(node, server), + bsyncServers' = bsyncServers.put(node, result.server), statusBuffer' = statusBuffer, requestsBuffer' = requestsBuffer, responsesBuffer' = match result.msg { diff --git a/specs/quint/specs/blocksync/blocksyncServerTest.qnt b/specs/quint/specs/blocksync/blocksyncServerTest.qnt new file mode 100644 index 000000000..09bf2dbaa --- /dev/null +++ b/specs/quint/specs/blocksync/blocksyncServerTest.qnt @@ -0,0 +1,154 @@ +// -*- mode: Bluespec; -*- + +module blocksyncServerTest { + + import blocksyncServer.* from "./blocksyncServer" + import blocksync.* from "./blocksync" + + val s = "v1" + val c = "v2" + + val chain = List( + { decision: mkProposal("v3", 0, 0, "block1", -1), + commit: Set() + }, + { decision: mkProposal("v2", 1, 1, "block2", 0), + commit: Set() + } + ) + + action sendRequestTo(v, req) = all { + statusBuffer' = statusBuffer, + requestsBuffer' = requestsBuffer.put(v, requestsBuffer.get(v).union(Set(req))), + responsesBuffer' = responsesBuffer, + unchangedServer, + } + + action clearResponses(client) = all { + statusBuffer' = statusBuffer, + requestsBuffer' = requestsBuffer, + responsesBuffer' = responsesBuffer.put(client, Set()), + unchangedServer, + } + + run fullDeliverRequest(client, server, rtype, height) = + sendRequestTo(server, { + client: client, + server: server, + rtype: rtype, + height: height, + }) + .then(deliverRequest(s)) + .then(stepServer(s)) + + // A server is created with no state. No responses should be produced. + // This run can be used as initialization for other tests. + run blocksyncServerInitTest = + all { + initServer(Set(s)), + initBsync(Set(s, c)), + } + + .then(broadcastStatus(s)) + // FIXME: I don't think there is a point on broadcast a status message + // here, since the blockchain is empty. + .expect(statusBuffer.get(c).contains({ + peer: s, + base: 0, + top: -1, + })) + + // Requests are all rejected + .then(fullDeliverRequest(c, s, SyncCertificate, 0)) + .then(fullDeliverRequest(c, s, SyncBlock, 0)) + .then(fullDeliverRequest(c, s, SyncBlockStoreEntry, 0)) + .expect(bsyncServers.get(s).requestMsgs.size() == 0) + .expect(responsesBuffer.get(c).size() == 0) + + // The server knows a chain with 1 element (height 0). + // It replies to request to height 0, but not for height 1. + run blocksyncServerSingleHeightTest = + blocksyncServerInitTest + + // Now the server knows height 0 + .then(updateServer(s, chain.slice(0, 1))) + + .then(broadcastStatus(s)) + .expect(statusBuffer.get(c).contains({ + peer: s, + base: 0, + top: 0, + })) + + .then(fullDeliverRequest(c, s, SyncCertificate, 0)) + .expect(responsesBuffer.get(c).contains({ + client: c, + server: s, + height: 0, + response: RespCertificate(chain[0].commit), + })) + + .then(fullDeliverRequest(c, s, SyncBlock, 0)) + .expect(responsesBuffer.get(c).contains({ + client: c, + server: s, + height: 0, + response: RespBlock(chain[0].decision), + })) + + .then(fullDeliverRequest(c, s, SyncBlockStoreEntry, 0)) + .expect(responsesBuffer.get(c).contains({ + client: c, + server: s, + height: 0, + response: RespBlockStoreEntry(chain[0]), + })) + + .then(clearResponses(c)) + + // Requests for height 2 are ignored + .then(fullDeliverRequest(c, s, SyncCertificate, 1)) + .then(fullDeliverRequest(c, s, SyncBlock, 1)) + .then(fullDeliverRequest(c, s, SyncBlockStoreEntry, 1)) + .expect(bsyncServers.get(s).requestMsgs.size() == 0) + .expect(responsesBuffer.get(c).size() == 0) + + // The server knows a chain with 2 elements (heights 0 and 1). + // It replies properly to requests to heights 0 and 1. + run blocksyncServerTwoHeightsTest = + blocksyncServerInitTest + + // Now the server knows heights 0 and 1 + .then(updateServer(s, chain.slice(0, 2))) + + .then(broadcastStatus(s)) + .expect(statusBuffer.get(c).contains({ + peer: s, + base: 0, + top: 1, + })) + + .then(fullDeliverRequest(c, s, SyncCertificate, 0)) + .expect(responsesBuffer.get(c).contains({ + client: c, + server: s, + height: 0, + response: RespCertificate(chain[0].commit), + })) + + .then(fullDeliverRequest(c, s, SyncBlock, 1)) + .expect(responsesBuffer.get(c).contains({ + client: c, + server: s, + height: 1, + response: RespBlock(chain[1].decision), + })) + + .then(fullDeliverRequest(c, s, SyncBlockStoreEntry, 0)) + .expect(responsesBuffer.get(c).contains({ + client: c, + server: s, + height: 0, + response: RespBlockStoreEntry(chain[0]), + })) +}