From a868173e616261f827c9beb542536e6ae7721dda Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 15 May 2020 23:35:44 +0200 Subject: [PATCH 01/34] adapted fastsync for apalache --- docs/spec/fastsync/verification/MC_1_1_5.tla | 13 + .../verification/fastsync_apalache.tla | 740 ++++++++++++++++++ 2 files changed, 753 insertions(+) create mode 100644 docs/spec/fastsync/verification/MC_1_1_5.tla create mode 100644 docs/spec/fastsync/verification/fastsync_apalache.tla diff --git a/docs/spec/fastsync/verification/MC_1_1_5.tla b/docs/spec/fastsync/verification/MC_1_1_5.tla new file mode 100644 index 000000000..38e7f0128 --- /dev/null +++ b/docs/spec/fastsync/verification/MC_1_1_5.tla @@ -0,0 +1,13 @@ +------------------------------- MODULE MC_1_1_5 ------------------------------------ + +CORRECT == {"c1"} +FAULTY == {"f2"} +MAX_HEIGHT == 5 +PEER_MAX_REQUESTS == 2 +TARGET_PENDING == 3 + +VARIABLES + state, blockPool, peersState, turn, inMsg, outMsg + +INSTANCE fastsync_apalache +======================================================================================== diff --git a/docs/spec/fastsync/verification/fastsync_apalache.tla b/docs/spec/fastsync/verification/fastsync_apalache.tla new file mode 100644 index 000000000..5afa6f37a --- /dev/null +++ b/docs/spec/fastsync/verification/fastsync_apalache.tla @@ -0,0 +1,740 @@ +----------------------------- MODULE fastsync_apalache ----------------------------- +(* + In this document we give the high level specification of the fast sync + protocol as implemented here: + https://github.com/tendermint/tendermint/tree/master/blockchain/v2. + +We assume a system in which one node is trying to sync with the blockchain +(replicated state machine) by downloading blocks from the set of full nodes +(we call them peers) that are block providers, and executing transactions +(part of the block) against the application. + +Peers can be faulty, and we don't make any assumption about the rate of correct/faulty +nodes in the node peerset (i.e., they can all be faulty). Correct peers are part +of the replicated state machine, i.e., they manage blockchain and execute +transactions against the same deterministic application. We don't make any +assumptions about the behavior of faulty processes. Processes (client and peers) +communicate by message passing. + + In this specification, we model this system with two parties: + - the node (state machine) that is doing fastsync and + - the environment with which node interacts. + +The environment consists of the set of (correct and faulty) peers with +which node interacts as part of fast sync protocol, but also contains some +aspects (adding/removing peers, timeout mechanism) that are part of the node +local environment (could be seen as part of the runtime in which node +executes). + +As part of the fast sync protocol a node and the peers exchange the following messages: + +- StatusRequest +- StatusResponse +- BlockRequest +- BlockResponse +- NoBlockResponse. + +A node is periodically issuing StatusRequests to query peers for their current height (to decide what +blocks to ask from what peers). Based on StatusResponses (that are sent by peers), the node queries +blocks for some height(s) by sending peers BlockRequest messages. A peer provides a requested block by +BlockResponse message. If a peer does not want to provide a requested block, then it sends NoBlockResponse message. +In addition to those messages, a node in this spec receives additional input messages (events): + +- AddPeer +- RemovePeer +- SyncTimeout. + +These are the control messages that are provided to the node by its execution enviornment. AddPeer +is for the case when a connection is established with a peer; similarly RemovePeer is for the case +a connection with the peer is terminated. Finally SyncTimeout is used to model a timeout trigger. + +We assume that fast sync protocol starts when connections with some number of peers +are established. Therefore, peer set is initialised with non-empty set of peer ids. Note however +that node does not know initially the peer heights. +*) + +EXTENDS Integers, FiniteSets, Sequences + +(* Type definitions for Apalache *) +a <: b == a \* type annotation + +PIDT == STRING \* type of process ids +AsPidSet(a) == a <: {PIDT} + +\* LastCommit type +LCT == [blockId |-> Int, enoughVotingPower |-> BOOLEAN] + +\* Block type +BT == [height |-> Int, lastCommit |-> LCT, wellFormed |-> BOOLEAN] + +\* ControlMessage type +CMT == [type |-> STRING, peerId |-> PIDT] \* type of control messages + +\* InMsg type +IMT == [type |-> STRING, peerId |-> PIDT, height |-> Int, block |-> BT] +AsInMsg(m) == m <: IMT +AsInMsgSet(S) == S <: {IMT} + +\* OutMsg type +OMT == [type |-> STRING, peerId |-> PIDT, height |-> Int] +AsOutMsg(m) == m <: OMT +AsOutMsgSet(S) == S <: {OMT} + +BPT == [height |-> Int, peerIds |-> {PIDT}, peerHeights |-> [PIDT -> Int], + blockStore |-> [Int -> BT], receivedBlocks |-> [Int -> PIDT], + pendingBlocks |-> [Int -> PIDT], syncedBlocks |-> Int, syncHeight |-> Int] + +AsBlockPool(bp) == bp <: BPT + +(* End of type definitions *) + +CONSTANTS MAX_HEIGHT, + CORRECT, \* set of correct peers + FAULTY, \* set of faulty peers + TARGET_PENDING, \* maximum number of pending requests + downloaded blocks that are not yet processed + PEER_MAX_REQUESTS \* maximum number of pending requests per peer + +ASSUME CORRECT \intersect FAULTY = {} +ASSUME TARGET_PENDING > 0 +ASSUME PEER_MAX_REQUESTS > 0 + + +\* the set of potential heights +Heights == 1..MAX_HEIGHT + +\* simplifies execute blocks logic. Used only in block store. +HeightsPlus == 1..MAX_HEIGHT+1 + +\* a special value for an undefined height +NilHeight == 0 + +\* the set of all peer ids the node can receive a message from +AllPeerIds == CORRECT \union FAULTY + +\* the set of potential blocks ids. For simplification, correct blocks are equal to block height. +BlockIds == Heights \union {NilHeight} + +LastCommits == [blockId: BlockIds, enoughVotingPower: BOOLEAN] + +\* Correct last commit have enough voting power, i.e., +2/3 of the voting power of +\* the corresponding validator set (enoughVotingPower = TRUE) that signs blockId. +\* BlockId defines correct previous block (in the implementation it is the hash of the block). +\* For simplicity, we model blockId as the height of the previous block. +CorrectLastCommit(h) == [blockId |-> h-1, enoughVotingPower |-> TRUE] + +NilCommit == [blockId |-> 0, enoughVotingPower |-> TRUE] + +Blocks == [height: Heights, lastCommit: LastCommits, wellFormed: BOOLEAN] + +\*BlocksWithNil == [height: Heights, lastCommit: LastCommits, wellFormed: BOOLEAN] + +\* correct node will create always valid blocks, i.e., wellFormed = true and lastCommit is correct. +CorrectBlock(h) == [height |-> h, lastCommit |-> CorrectLastCommit(h), wellFormed |-> TRUE] + +NilBlock == [height |-> 0, lastCommit |-> NilCommit, wellFormed |-> TRUE] + +\* a special value for an undefined peer +NilPeer == "Nil" \* we have changed it to STRING for apalache efficiency + +\* control the state of the syncing node +States == { "running", "finished"} + +NoMsg == [type |-> "None"] + +\* the variables of the node running fastsync +VARIABLES + state, \* running or finished + (* + blockPool [ + height, \* current height we are trying to sync. Last block executed is height - 1 + peerIds, \* set of peers node is connected to + peerHeights, \* map of peer ids to its (stated) height + blockStore, \* map of heights to (received) blocks + receivedBlocks, \* map of heights to peer that has sent us the block (stored in blockStore) + pendingBlocks, \* map of heights to peer to which block request has been sent + syncHeight, \* height at the point syncTimeout was triggered last time + syncedBlocks \* number of blocks synced since last syncTimeout. If it is 0 when the next timeout occurs, then protocol terminates. + ] + *) + blockPool + + +\* the variables of the peers providing blocks +VARIABLES + (* + peersState [ + peerHeights, \* track peer heights + statusRequested, \* boolean set to true when StatusRequest is received. Models periodic sending of StatusRequests. + blocksRequested \* set of BlockRequests received that are not answered yet + ] + *) + peersState + + + \* the variables for the network and scheduler + VARIABLES + turn, \* who is taking the turn: "Peers" or "Node" + inMsg, \* a node receives message by this variable + outMsg \* a node sends a message by this variable + + +(* the variables of the node *) +nvars == <> + +\* Control messages +ControlMsgs == + [type: {"addPeer"}, peerId: AllPeerIds] + \union + [type: {"removePeer"}, peerId: AllPeerIds] + \union + [type: {"syncTimeout"}] + +\* All messages (and events) received by a node +InMsgs == + {NoMsg} + \union + [type: {"blockResponse"}, peerId: AllPeerIds, block: Blocks] + \union + [type: {"noBlockResponse"}, peerId: AllPeerIds, height: Heights] + \union + [type: {"statusResponse"}, peerId: AllPeerIds, height: Heights] + \union + ControlMsgs + +\* Messages sent by a node and received by peers (environment in our case) +OutMsgs == + {NoMsg} + \union + [type: {"statusRequest"}] \* StatusRequest is broadcast to the set of connected peers. + \union + [type: {"blockRequest"}, peerId: AllPeerIds, height: Heights] + + +(********************************** NODE ***********************************) + +InitNode == + \E pIds \in SUBSET AllPeerIds: \* set of peers node established initial connections with + /\ pIds /= AsPidSet({}) \* apalache better checks non-emptiness than subtracts from SUBSET + /\ blockPool = AsBlockPool([ + height |-> 1, + peerIds |-> pIds, + peerHeights |-> [p \in AllPeerIds |-> NilHeight], \* no peer height is known + blockStore |-> [h \in Heights |-> NilBlock], + receivedBlocks |-> [h \in Heights |-> NilPeer], + pendingBlocks |-> [h \in Heights |-> NilPeer], + syncedBlocks |-> -1, + syncHeight |-> 1 + ]) + /\ state = "running" + +\* Remove faulty peers. +\* Returns new block pool. +\* See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L222 +RemovePeers(rmPeers, bPool) == + LET keepPeers == bPool.peerIds \ rmPeers IN + LET pHeights == + [p \in AllPeerIds |-> IF p \in rmPeers THEN NilHeight ELSE bPool.peerHeights[p]] IN + + LET failedRequests == + {h \in Heights: /\ h >= bPool.height + /\ \/ bPool.pendingBlocks[h] \in rmPeers + \/ bPool.receivedBlocks[h] \in rmPeers} IN + LET pBlocks == + [h \in Heights |-> IF h \in failedRequests THEN NilPeer ELSE bPool.pendingBlocks[h]] IN + LET rBlocks == + [h \in Heights |-> IF h \in failedRequests THEN NilPeer ELSE bPool.receivedBlocks[h]] IN + LET bStore == + [h \in Heights |-> IF h \in failedRequests THEN NilBlock ELSE bPool.blockStore[h]] IN + + IF keepPeers /= bPool.peerIds + THEN [bPool EXCEPT + !.peerIds = keepPeers, + !.peerHeights = pHeights, + !.pendingBlocks = pBlocks, + !.receivedBlocks = rBlocks, + !.blockStore = bStore + ] + ELSE bPool + +\* Add a peer. +\* see https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L198 +AddPeer(peer, bPool) == + [bPool EXCEPT !.peerIds = bPool.peerIds \union {peer}] + + +(* +Handle StatusResponse message. +If valid status response, update peerHeights. +If invalid (height is smaller than the current), then remove peer. +Returns new block pool. +See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L667 +*) +HandleStatusResponse(msg, bPool) == + LET peerHeight == bPool.peerHeights[msg.peerId] IN + + IF /\ msg.peerId \in bPool.peerIds + /\ msg.height >= peerHeight + THEN \* a correct response + LET pHeights == [bPool.peerHeights EXCEPT ![msg.peerId] = msg.height] IN + [bPool EXCEPT !.peerHeights = pHeights] + ELSE RemovePeers({msg.peerId}, bPool) \* the peer has sent us message with smaller height or peer is not in our peer list + + +(* +Handle BlockResponse message. +If valid block response, update blockStore, pendingBlocks and receivedBlocks. +If invalid (unsolicited response or malformed block), then remove peer. +Returns new block pool. +See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L522 +*) +HandleBlockResponse(msg, bPool) == + LET h == msg.block.height IN + + IF /\ msg.peerId \in bPool.peerIds + /\ bPool.blockStore[h] = NilBlock + /\ bPool.pendingBlocks[h] = msg.peerId + /\ msg.block.wellFormed + THEN + [bPool EXCEPT + !.blockStore = [bPool.blockStore EXCEPT ![h] = msg.block], + !.receivedBlocks = [bPool.receivedBlocks EXCEPT![h] = msg.peerId], + !.pendingBlocks = [bPool.pendingBlocks EXCEPT![h] = NilPeer] + ] + ELSE RemovePeers({msg.peerId}, bPool) + + HandleNoBlockResponse(msg, bPool) == + RemovePeers({msg.peerId}, bPool) + + +\* Compute max peer height. +\* See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L440 +MaxPeerHeight(bPool) == + IF bPool.peerIds = AsPidSet({}) + THEN 0 \* no peers, just return 0 + ELSE LET Hts == {bPool.peerHeights[p] : p \in bPool.peerIds} IN + CHOOSE max \in Hts: \A h \in Hts: h <= max + +(* Returns next height for which request should be sent. + Returns NilHeight in case there is no height for which request can be sent. + See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L454 *) +FindNextRequestHeight(bPool) == + LET S == {i \in Heights: + /\ i >= bPool.height + /\ i <= MaxPeerHeight(bPool) + /\ bPool.blockStore[i] = NilBlock + /\ bPool.pendingBlocks[i] = NilPeer} IN + IF S = {} <: {Int} + THEN NilHeight + ELSE + CHOOSE min \in S: \A h \in S: h >= min + +\* Returns number of pending requests for a given peer. +NumOfPendingRequests(bPool, peer) == + LET peerPendingRequests == + {h \in Heights: + /\ h >= bPool.height + /\ bPool.pendingBlocks[h] = peer + } + IN + Cardinality(peerPendingRequests) + +(* Returns peer that can serve block for a given height. + Returns NilPeer in case there are no such peer. + See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L477 *) +FindPeerToServe(bPool, h) == + LET peersThatCanServe == { p \in bPool.peerIds: + /\ bPool.peerHeights[p] >= h + /\ NumOfPendingRequests(bPool, p) < PEER_MAX_REQUESTS } IN + + LET pendingBlocks == + {i \in Heights: + /\ i >= bPool.height + /\ \/ bPool.pendingBlocks[i] /= NilPeer + \/ bPool.blockStore[i] /= NilBlock + } IN + + IF \/ peersThatCanServe = {} <: {PIDT} + \/ Cardinality(pendingBlocks) >= TARGET_PENDING + THEN NilPeer + \* pick a peer that can serve request for height h that has minimum number of pending requests + ELSE CHOOSE p \in peersThatCanServe: \A q \in peersThatCanServe: + /\ NumOfPendingRequests(bPool, p) <= NumOfPendingRequests(bPool, q) + + +\* Make a request for a block (if possible) and return a request message and block poool. +CreateRequest(bPool) == + LET nextHeight == FindNextRequestHeight(bPool) IN + + IF nextHeight = NilHeight THEN [msg |-> AsOutMsg(NoMsg), pool |-> bPool] + ELSE + LET peer == FindPeerToServe(bPool, nextHeight) IN + IF peer = NilPeer THEN [msg |-> AsOutMsg(NoMsg), pool |-> bPool] + ELSE + LET m == [type |-> "blockRequest", peerId |-> peer, height |-> nextHeight] IN + LET newPool == [bPool EXCEPT + !.pendingBlocks = [bPool.pendingBlocks EXCEPT ![nextHeight] = peer] + ] IN + [msg |-> m, pool |-> newPool] + + +\* Returns node state, i.e., defines termination condition. +\* See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L432 +ComputeNextState(bPool) == + IF bPool.syncedBlocks = 0 \* corresponds to the syncTimeout in case no progress has been made for a period of time. + THEN "finished" + ELSE IF /\ bPool.height > 1 + /\ bPool.height >= MaxPeerHeight(bPool) \* see https://github.com/tendermint/tendermint/blob/61057a8b0af2beadee106e47c4616b279e83c920/blockchain/v2/scheduler.go#L566 + THEN "finished" + ELSE "running" + +(* Verify if commit is for the given block id and if commit has enough voting power. + See https://github.com/tendermint/tendermint/blob/61057a8b0af2beadee106e47c4616b279e83c920/blockchain/v2/processor_context.go#L12 *) +VerifyCommit(block, lastCommit) == + /\ lastCommit.enoughVotingPower + /\ lastCommit.blockId = block.height + + +(* Tries to execute next block in the pool, i.e., defines block validation logic. + Returns new block pool (peers that has send invalid blocks are removed). + See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/processor.go#L135 *) +ExecuteBlocks(bPool) == + LET bStore == bPool.blockStore IN + LET block1 == bStore[bPool.height] IN + LET block2 == bStore[bPool.height+1] IN + + IF block1 = NilBlock \/ block2 = NilBlock \* we don't have two next consecutive blocks + THEN bPool + ELSE IF bPool.height > 1 /\ ~VerifyCommit(block1, block2.lastCommit) + THEN RemovePeers({bPool.receivedBlocks[block1.height], bPool.receivedBlocks[block2.height]}, bPool) + ELSE \* all good, execute block at position height + [bPool EXCEPT !.height = bPool.height + 1] + + +\* Defines logic for pruning peers. +\* See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L613 +TryPrunePeer(bPool, suspectedSet, isTimedOut) == + (* -----------------------------------------------------------------------------------------------------------------------*) + (* Corresponds to function prunablePeers in scheduler.go file. Note that this function only checks if block has been *) + (* received from a peer during peerTimeout period. *) + (* Note that in case no request has been scheduled to a correct peer, or a request has been scheduled *) + (* recently, so the peer hasn't responded yet, a peer will be removed as no block is received within peerTimeout. *) + (* In case of faulty peers, we don't have any guarantee that they will respond. *) + (* Therefore, we model this with nondeterministic behavior as it could lead to peer removal, for both correct and faulty. *) + (* See scheduler.go *) + (* https://github.com/tendermint/tendermint/blob/4298bbcc4e25be78e3c4f21979d6aa01aede6e87/blockchain/v2/scheduler.go#L335 *) + LET toRemovePeers == bPool.peerIds \intersect suspectedSet IN + + (* + Corresponds to logic for pruning a peer that is responsible for delivering block for the next height. + The pruning logic for the next height is based on the time when a BlockRequest is sent. Therefore, if a request is sent + to a correct peer for the next height (blockPool.height), it should never be removed by this check as we assume that + correct peers respond timely and reliably. However, if a request is sent to a faulty peer then we + might get response on time or not, which is modelled with nondeterministic isTimedOut flag. + See scheduler.go + https://github.com/tendermint/tendermint/blob/4298bbcc4e25be78e3c4f21979d6aa01aede6e87/blockchain/v2/scheduler.go#L617 + *) + LET nextHeightPeer == bPool.pendingBlocks[bPool.height] IN + LET prunablePeers == + IF /\ nextHeightPeer /= NilPeer + /\ nextHeightPeer \in FAULTY + /\ isTimedOut + THEN toRemovePeers \union {nextHeightPeer} + ELSE toRemovePeers + IN + RemovePeers(prunablePeers, bPool) + + +\* Handle SyncTimeout. It models if progress has been made (height has increased) since the last SyncTimeout event. +HandleSyncTimeout(bPool) == + [bPool EXCEPT + !.syncedBlocks = bPool.height - bPool.syncHeight, + !.syncHeight = bPool.height + ] + +HandleResponse(msg, bPool) == + IF msg.type = "blockResponse" THEN + HandleBlockResponse(msg, bPool) + ELSE IF msg.type = "noBlockResponse" THEN + HandleNoBlockResponse(msg, bPool) + ELSE IF msg.type = "statusResponse" THEN + HandleStatusResponse(msg, bPool) + ELSE IF msg.type = "addPeer" THEN + AddPeer(msg.peerId, bPool) + ELSE IF msg.type = "removePeer" THEN + RemovePeers({msg.peerId}, bPool) + ELSE IF msg.type = "syncTimeout" THEN + HandleSyncTimeout(bPool) + ELSE + bPool + + +(* + At every node step we executed the following steps (atomically): + 1) input message is consumed and the corresponding handler is called, + 2) pruning logic is called + 3) block execution is triggered (we try to execute block at next height) + 4) a request to a peer is made (if possible) and + 5) we decide if termination condition is satisifed so we stop. +*) +NodeStep == + \E suspectedSet \in SUBSET AllPeerIds: \* suspectedSet is a nondeterministic set of peers + \E isTimedOut \in BOOLEAN: + LET bPool == HandleResponse(inMsg, blockPool) IN + LET bp == TryPrunePeer(bPool, suspectedSet, isTimedOut) IN + LET nbPool == ExecuteBlocks(bp) IN + LET msgAndPool == CreateRequest(nbPool) IN + LET nstate == ComputeNextState(msgAndPool.pool) IN + + /\ state' = nstate + /\ blockPool' = msgAndPool.pool + /\ outMsg' = msgAndPool.msg + /\ inMsg' = AsInMsg(NoMsg) + + +\* If node is running, then in every step we try to create blockRequest. +\* In addition, input message (if exists) is consumed and processed. +NextNode == + \/ /\ state = "running" + /\ NodeStep + + \/ /\ state = "finished" + /\ UNCHANGED <> + + +(********************************** Peers ***********************************) + +InitPeers == + \E pHeights \in [AllPeerIds -> Heights]: + peersState = [ + peerHeights |-> pHeights, + statusRequested |-> FALSE, + blocksRequested |-> AsOutMsgSet({}) + ] + +HandleStatusRequest(msg, pState) == + [pState EXCEPT + !.statusRequested = TRUE + ] + +HandleBlockRequest(msg, pState) == + [pState EXCEPT + !.blocksRequested = pState.blocksRequested \union AsOutMsgSet({msg}) + ] + +HandleRequest(msg, pState) == + IF msg = AsOutMsg(NoMsg) + THEN pState + ELSE IF msg.type = "statusRequest" + THEN HandleStatusRequest(msg, pState) + ELSE HandleBlockRequest(msg, pState) + +CreateStatusResponse(peer, pState, anyHeight) == + LET m == + IF peer \in CORRECT + THEN AsInMsg([type |-> "statusResponse", peerId |-> peer, height |-> pState.peerHeights[peer]]) + ELSE AsInMsg([type |-> "statusResponse", peerId |-> peer, height |-> anyHeight]) IN + + [msg |-> m, peers |-> pState] + +CreateBlockResponse(msg, pState, arbitraryBlock) == + LET m == + IF msg.peerId \in CORRECT + THEN AsInMsg([type |-> "blockResponse", peerId |-> msg.peerId, block |-> CorrectBlock(msg.height)]) + ELSE AsInMsg([type |-> "blockResponse", peerId |-> msg.peerId, block |-> arbitraryBlock]) IN + LET npState == + [pState EXCEPT + !.blocksRequested = pState.blocksRequested \ {msg} + ] IN + [msg |-> m, peers |-> npState] + +GrowBlockchain(pState) == + \E p \in CORRECT: + /\ pState.peerHeights[p] < MAX_HEIGHT + /\ peersState' = [pState EXCEPT !.peerHeights[p] = @ + 1] + /\ inMsg' = AsInMsg(NoMsg) + + +SendStatusResponseMessage(pState) == + /\ \E arbitraryHeight \in Heights: + \E peer \in AllPeerIds: + LET msgAndPeers == CreateStatusResponse(peer, pState, arbitraryHeight) IN + /\ peersState' = msgAndPeers.peers + /\ inMsg' = msgAndPeers.msg + + +SendAddPeerMessage == + \E peer \in AllPeerIds: + /\ inMsg' = AsInMsg([type |-> "addPeer", peerId |-> peer]) + /\ UNCHANGED peersState + +SendRemovePeerMessage == + \E peer \in AllPeerIds: + /\ inMsg' = AsInMsg([type |-> "removePeer", peerId |-> peer]) + /\ UNCHANGED peersState + +SendSyncTimeoutMessage == + /\ inMsg' = AsInMsg([type |-> "syncTimeout"]) + /\ UNCHANGED peersState + + +SendControlMessage == + \/ SendAddPeerMessage + \/ SendRemovePeerMessage + \/ SendSyncTimeoutMessage + + +SendBlockResponseMessage(pState) == + \/ /\ pState.blocksRequested /= AsOutMsgSet({}) + /\ \E msg \in pState.blocksRequested: + \E block \in Blocks: + LET msgAndPeers == CreateBlockResponse(msg, pState, block) IN + /\ peersState' = msgAndPeers.peers + /\ inMsg' = msgAndPeers.msg + + + \/ /\ peersState' = pState + /\ inMsg' \in AsInMsgSet([type: {"blockResponse"}, peerId: FAULTY, block: Blocks]) + + SendNoBlockResponseMessage(pState) == + /\ peersState' = pState + /\ inMsg' \in AsInMsgSet([type: {"noBlockResponse"}, peerId: FAULTY, height: Heights]) + + +SendResponseMessage(pState) == + \/ SendBlockResponseMessage(pState) + \/ SendNoBlockResponseMessage(pState) + \/ SendStatusResponseMessage(pState) + + +NextEnvStep(pState) == + \/ SendResponseMessage(pState) + \/ GrowBlockchain(pState) + \/ SendControlMessage + + +\* Peers consume a message and update it's local state. It then makes a single step, i.e., it sends at most single message. +\* Message sent could be either a response to a request or faulty message (sent by faulty processes). +NextPeers == + LET pState == HandleRequest(outMsg, peersState) IN + + \/ /\ outMsg' = AsOutMsg(NoMsg) + /\ NextEnvStep(pState) + + +\* the composition of the node, the peers, the network and scheduler +Init == + /\ InitNode + /\ InitPeers + /\ turn = "Peers" + /\ inMsg = AsInMsg(NoMsg) + /\ outMsg = AsOutMsg([type |-> "statusRequest"]) + +Next == + IF turn = "Peers" + THEN + /\ NextPeers + /\ turn' = "Node" + /\ UNCHANGED nvars + ELSE + /\ NextNode + /\ turn' = "Peers" + /\ UNCHANGED peersState + + + +FlipTurn == + turn' = ( + IF turn = "Peers" THEN + "Node" + ELSE + "Peers" + ) + + +\* Compute max peer height. Used as a helper operator in properties. +MaxCorrectPeerHeight(bPool) == + LET correctPeers == {p \in bPool.peerIds: p \in CORRECT} IN + IF correctPeers = {} + THEN 0 \* no peers, just return 0 + ELSE LET Hts == {bPool.peerHeights[p] : p \in correctPeers} IN + CHOOSE max \in Hts: \A h \in Hts: h <= max + +\* properties to check +TypeOK == + /\ state \in States + /\ inMsg \in InMsgs + /\ outMsg \in OutMsgs + /\ turn \in {"Peers", "Node"} + /\ peersState \in [ + peerHeights: [AllPeerIds -> Heights \union {NilHeight}], + statusRequested: BOOLEAN, + blocksRequested: + SUBSET + [type: {"blockRequest"}, peerId: AllPeerIds, height: Heights] + + ] + + /\ blockPool \in [ + height: Heights, + peerIds: SUBSET AllPeerIds, + peerHeights: [AllPeerIds -> Heights \union {NilHeight}], + blockStore: [Heights -> Blocks \union {NilBlock}], + receivedBlocks: [Heights -> AllPeerIds \union {NilPeer}], + pendingBlocks: [Heights -> AllPeerIds \union {NilPeer}], + syncedBlocks: Heights \union {NilHeight, -1}, + syncHeight: Heights + ] + +\* TODO: align with the English spec. Add reference to it +Correctness1 == state = "finished" => + blockPool.height >= MaxCorrectPeerHeight(blockPool) + +\* TODO: align with the English spec. Add reference to it +Correctness2 == + \A p \in CORRECT: + \/ p \notin blockPool.peerIds + \/ [] (state = "finished" => blockPool.height >= blockPool.peerHeights[p] - 1) + +Correctness3 == + \A p \in CORRECT: + \/ p \notin blockPool.peerIds + \/ blockPool.syncedBlocks <= 0 \* timeout + \/ [] (state = "finished" => blockPool.height >= blockPool.peerHeights[p] - 1) + +Correctness3AsInv == + \A p \in CORRECT: + \/ p \notin blockPool.peerIds + \/ blockPool.syncedBlocks <= 0 \* timeout + \/ (state = "finished" => blockPool.height >= blockPool.peerHeights[p] - 1) + +\* TODO: align with the English spec. Add reference to it +\* FIXME: uncomment when the Apalache issue is fixed: +\* https://github.com/konnov/apalache/issues/145 +\*Termination == WF_turn(FlipTurn) => <>(state = "finished") + +\* a few simple properties that trigger counterexamples + +\* Shows execution in which peer set is empty +PeerSetIsNeverEmpty == blockPool.peerIds /= {} + +\* Shows execution in which state = "finished" and MaxPeerHeight is not equal to 1 +StateNotFinished == + state /= "finished" \/ MaxPeerHeight(blockPool) = 1 + +BlockPoolInvariant == + \A h \in Heights: + \* waiting for a block to arrive + \/ /\ blockPool.receivedBlocks[h] = NilPeer + /\ blockPool.blockStore[h] = NilBlock + \* valid block is received and is present in the store + \/ /\ blockPool.receivedBlocks[h] /= NilPeer + /\ blockPool.blockStore[h] /= NilBlock + /\ blockPool.pendingBlocks[h] = NilPeer + +============================================================================= + +\*============================================================================= +\* Modification History +\* Last modified Fri May 15 15:38:28 CEST 2020 by igor +\* Last modified Thu Apr 16 16:57:22 CEST 2020 by zarkomilosevic +\* Created Tue Feb 04 10:36:18 CET 2020 by zarkomilosevic From 2fbe722c8942aa114cd5f60b7f2291daafe0393d Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 18 May 2020 17:59:56 +0200 Subject: [PATCH 02/34] bugfix for CorrectBlocks --- .../verification/fastsync_apalache.tla | 59 +++++++++++++++---- 1 file changed, 46 insertions(+), 13 deletions(-) diff --git a/docs/spec/fastsync/verification/fastsync_apalache.tla b/docs/spec/fastsync/verification/fastsync_apalache.tla index 5afa6f37a..1f4642b32 100644 --- a/docs/spec/fastsync/verification/fastsync_apalache.tla +++ b/docs/spec/fastsync/verification/fastsync_apalache.tla @@ -108,6 +108,9 @@ HeightsPlus == 1..MAX_HEIGHT+1 \* a special value for an undefined height NilHeight == 0 +\* the height of the genesis block +GenesisHeight == 1 + \* the set of all peer ids the node can receive a message from AllPeerIds == CORRECT \union FAULTY @@ -216,14 +219,16 @@ InitNode == \E pIds \in SUBSET AllPeerIds: \* set of peers node established initial connections with /\ pIds /= AsPidSet({}) \* apalache better checks non-emptiness than subtracts from SUBSET /\ blockPool = AsBlockPool([ - height |-> 1, + height |-> GenesisHeight + 1, \* the genesis block is at height 1 + syncHeight |-> GenesisHeight + 1, \* and we are synchronized to it peerIds |-> pIds, peerHeights |-> [p \in AllPeerIds |-> NilHeight], \* no peer height is known - blockStore |-> [h \in Heights |-> NilBlock], + blockStore |-> + [h \in Heights |-> + IF h > GenesisHeight THEN NilBlock ELSE CorrectBlock(1)], receivedBlocks |-> [h \in Heights |-> NilPeer], pendingBlocks |-> [h \in Heights |-> NilPeer], - syncedBlocks |-> -1, - syncHeight |-> 1 + syncedBlocks |-> -1 ]) /\ state = "running" @@ -402,12 +407,16 @@ ExecuteBlocks(bPool) == LET block1 == bStore[bPool.height] IN LET block2 == bStore[bPool.height+1] IN - IF block1 = NilBlock \/ block2 = NilBlock \* we don't have two next consecutive blocks - THEN bPool - ELSE IF bPool.height > 1 /\ ~VerifyCommit(block1, block2.lastCommit) - THEN RemovePeers({bPool.receivedBlocks[block1.height], bPool.receivedBlocks[block2.height]}, bPool) - ELSE \* all good, execute block at position height - [bPool EXCEPT !.height = bPool.height + 1] + IF block1 = NilBlock \/ block2 = NilBlock + THEN bPool \* we don't have two next consecutive blocks + ELSE IF bPool.height = GenesisHeight + 1 /\ ~VerifyCommit(bStore[GenesisHeight], block1.lastCommit) + THEN \* corner case: the block right after genesis is corrupted, evict it + RemovePeers({bPool.receivedBlocks[GenesisHeight + 1]}, bPool) + ELSE IF ~VerifyCommit(block1, block2.lastCommit) + THEN \* remove the peers of block1 and block2, as they are considered faulty + RemovePeers({bPool.receivedBlocks[block1.height], bPool.receivedBlocks[block2.height]}, bPool) + ELSE \* all good, execute block at position height + [bPool EXCEPT !.height = bPool.height + 1] \* Defines logic for pruning peers. @@ -654,7 +663,7 @@ FlipTurn == \* Compute max peer height. Used as a helper operator in properties. MaxCorrectPeerHeight(bPool) == LET correctPeers == {p \in bPool.peerIds: p \in CORRECT} IN - IF correctPeers = {} + IF correctPeers = AsPidSet({}) THEN 0 \* no peers, just return 0 ELSE LET Hts == {bPool.peerHeights[p] : p \in correctPeers} IN CHOOSE max \in Hts: \A h \in Hts: h <= max @@ -695,6 +704,11 @@ Correctness2 == \/ p \notin blockPool.peerIds \/ [] (state = "finished" => blockPool.height >= blockPool.peerHeights[p] - 1) +Correctness2AsInv == + \A p \in CORRECT: + \/ p \notin blockPool.peerIds + \/ (state = "finished" => blockPool.height >= blockPool.peerHeights[p] - 1) + Correctness3 == \A p \in CORRECT: \/ p \notin blockPool.peerIds @@ -715,12 +729,31 @@ Correctness3AsInv == \* a few simple properties that trigger counterexamples \* Shows execution in which peer set is empty -PeerSetIsNeverEmpty == blockPool.peerIds /= {} +PeerSetIsNeverEmpty == blockPool.peerIds /= AsPidSet({}) \* Shows execution in which state = "finished" and MaxPeerHeight is not equal to 1 StateNotFinished == state /= "finished" \/ MaxPeerHeight(blockPool) = 1 +\* A false expectation that the protocol only finishes with the blocks +\* from the processes that had not been suspected in being faulty +SyncFromCorrectInv == + \/ state /= "finished" + \/ \A h \in 1..blockPool.height: + blockPool.receivedBlocks[h] \in blockPool.peerIds \union {NilPeer} + +\* All synchronized blocks are well-formed and have sufficiently many votes +CorrectBlocksInv == + \/ state /= "finished" + \/ \A h \in 1..(blockPool.height - 1): + LET block == blockPool.blockStore[h] IN + block.wellFormed /\ block.lastCommit.enoughVotingPower + +\* A false expectation that a correct process is never removed from the set of peer ids. +\* A correct process may reply too late and then gets evicted. +CorrectNeverSuspectedInv == + CORRECT \subseteq blockPool.peerIds + BlockPoolInvariant == \A h \in Heights: \* waiting for a block to arrive @@ -735,6 +768,6 @@ BlockPoolInvariant == \*============================================================================= \* Modification History -\* Last modified Fri May 15 15:38:28 CEST 2020 by igor +\* Last modified Mon May 18 16:08:46 CEST 2020 by igor \* Last modified Thu Apr 16 16:57:22 CEST 2020 by zarkomilosevic \* Created Tue Feb 04 10:36:18 CET 2020 by zarkomilosevic From 3b3d42314be86139fc8e7b1e82b32f952b968d0b Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Tue, 19 May 2020 12:14:18 +0200 Subject: [PATCH 03/34] the minimalistic model of blockchain for fastsync --- docs/spec/fastsync/verification/Tinychain.tla | 99 +++++++++++++++++++ 1 file changed, 99 insertions(+) create mode 100644 docs/spec/fastsync/verification/Tinychain.tla diff --git a/docs/spec/fastsync/verification/Tinychain.tla b/docs/spec/fastsync/verification/Tinychain.tla new file mode 100644 index 000000000..b46d35111 --- /dev/null +++ b/docs/spec/fastsync/verification/Tinychain.tla @@ -0,0 +1,99 @@ +-------------------------- MODULE Tinychain ---------------------------------- +(* A very abstract model of Tendermint blockchain. Its only purpose is to highlight + the relation between validator sets, next validator sets, and last commits. + *) + +EXTENDS Sequences, Integers + +------------------------- MODULE ApalacheTypes ----------------------------------- +\* type annotation +a <: b == a + +\* the type of validator sets, e.g., STRING +VST == STRING + +\* LastCommit type. +\* It contains the id of the committed block +\* and the set of the validators who have committed the block +LCT == [blockId |-> Int, commiters |-> VST] + +\* Block type. +\* A block contains its height, validator set, next validator set, and last commit +BT == [height |-> Int, VS |-> VST, NextVS |-> VST, lastCommit |-> LCT] + +SeqOfBT(s) == s <: Seq(BT) +================================================================================== + +INSTANCE ApalacheTypes + +CONSTANTS + (* + A set of abstract values, each value representing a set of validators. + For the purposes of this specification, they can be any values, + e.g., "s1", "s2", etc. + *) + VALIDATOR_SETS, + (* The maximal height, up to which the blockchain may grow *) + MAX_HEIGHT + +VARIABLES + (* The blockchain as a sequence of blocks *) + chain + +\* Initially, the blockchain contains one trusted block +Init == + \E vs \in VALIDATOR_SETS: + \* the last commit in the trusted block is somewhat weird + LET lastCommit == [blockId |-> 0, commiters |-> vs] IN + chain = SeqOfBT(<< + [height |-> 1, VS |-> vs, NextVS |-> vs, lastCommit |-> lastCommit + ]>>) + +\* Add one more block to the blockchain +AdvanceChain == + \E NextVS \in VALIDATOR_SETS: + LET last == chain[Len(chain)] + lastCommit == [blockId |-> last.height, commiters |-> last.VS] + newBlock == [height |-> last.height + 1, + VS |-> last.NextVS, + NextVS |-> NextVS, + lastCommit |-> lastCommit] + IN + chain' = Append(chain, newBlock) + +\* The blockchain may grow up to the maximum and then stutter +Next == + \/ Len(chain) < MAX_HEIGHT /\ AdvanceChain + \/ Len(chain) >= MAX_HEIGHT /\ UNCHANGED chain + +\* The basic properties of blocks in the blockchain: +\* They should pass the validity check and they may verify the next block. + +\* Is a block valid against the next validator set (of the previous block) +IsValid(block, nextVS) == + \* simply check that the validator set is propagated correctly. + \* (the implementation tests hashes and the application state) + block.VS = nextVS + +\* Does the block verify the commit (of the next block) +DoesVerify(block, commit) == + \* the commits are signed by the block validators + /\ commit.commiters = block.VS + \* the block id in the commit matches the block height + \* (the implementation has more extensive tests) + /\ commit.blockId = block.height + + +\* Basic invariants + +\* every block has the validator set that is chosen by its predecessor +ValidBlockInv == + \A h \in 2..Len(chain): + IsValid(chain[h], chain[h - 1].NextVS) + +\* last commit of every block is signed by the validators of the predecessor +VerifiedBlockInv == + \A h \in 2..Len(chain): + DoesVerify(chain[h - 1], chain[h].lastCommit) + +================================================================================== From b6a140f3a830df048f5ce6cfb00dfcc1ab3f18ab Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Tue, 19 May 2020 21:17:04 +0200 Subject: [PATCH 04/34] fixed safety --- docs/spec/fastsync/verification/MC_1_1_4.tla | 15 ++ docs/spec/fastsync/verification/MC_1_2_5.tla | 15 ++ .../{MC_1_1_5.tla => MC_1_3_5.tla} | 10 +- docs/spec/fastsync/verification/Tinychain.tla | 52 ++++-- .../verification/fastsync_apalache.tla | 157 +++++++++--------- 5 files changed, 148 insertions(+), 101 deletions(-) create mode 100644 docs/spec/fastsync/verification/MC_1_1_4.tla create mode 100644 docs/spec/fastsync/verification/MC_1_2_5.tla rename docs/spec/fastsync/verification/{MC_1_1_5.tla => MC_1_3_5.tla} (52%) diff --git a/docs/spec/fastsync/verification/MC_1_1_4.tla b/docs/spec/fastsync/verification/MC_1_1_4.tla new file mode 100644 index 000000000..9797fabfc --- /dev/null +++ b/docs/spec/fastsync/verification/MC_1_1_4.tla @@ -0,0 +1,15 @@ +--------------------------- MODULE MC_1_1_4 ------------------------------------ + +VALIDATOR_SETS == {"vs1", "vs2"} +NIL_VS == "NilVS" +CORRECT == {"c1"} +FAULTY == {"f2"} +MAX_HEIGHT == 4 +PEER_MAX_REQUESTS == 2 +TARGET_PENDING == 3 + +VARIABLES + state, blockPool, peersState, chain, turn, inMsg, outMsg + +INSTANCE fastsync_apalache +================================================================================ diff --git a/docs/spec/fastsync/verification/MC_1_2_5.tla b/docs/spec/fastsync/verification/MC_1_2_5.tla new file mode 100644 index 000000000..1bd335082 --- /dev/null +++ b/docs/spec/fastsync/verification/MC_1_2_5.tla @@ -0,0 +1,15 @@ +-------------------------- MODULE MC_1_2_5 ------------------------------------ + +VALIDATOR_SETS == {"vs1", "vs2"} +NIL_VS == "NilVS" +CORRECT == {"c1"} +FAULTY == {"f2", "f3"} +MAX_HEIGHT == 5 +PEER_MAX_REQUESTS == 2 +TARGET_PENDING == 3 + +VARIABLES + state, blockPool, peersState, chain, turn, inMsg, outMsg + +INSTANCE fastsync_apalache +=============================================================================== diff --git a/docs/spec/fastsync/verification/MC_1_1_5.tla b/docs/spec/fastsync/verification/MC_1_3_5.tla similarity index 52% rename from docs/spec/fastsync/verification/MC_1_1_5.tla rename to docs/spec/fastsync/verification/MC_1_3_5.tla index 38e7f0128..81dadb470 100644 --- a/docs/spec/fastsync/verification/MC_1_1_5.tla +++ b/docs/spec/fastsync/verification/MC_1_3_5.tla @@ -1,13 +1,15 @@ -------------------------------- MODULE MC_1_1_5 ------------------------------------ +------------------------------- MODULE MC_1_3_5 ------------------------------------ -CORRECT == {"c1"} -FAULTY == {"f2"} MAX_HEIGHT == 5 +VALIDATOR_SETS == {"vs1", "vs2"} +NIL_VS == "NilVS" +CORRECT == {"c1"} +FAULTY == {"f2", "f3", "f4"} PEER_MAX_REQUESTS == 2 TARGET_PENDING == 3 VARIABLES - state, blockPool, peersState, turn, inMsg, outMsg + state, blockPool, peersState, chain, turn, inMsg, outMsg INSTANCE fastsync_apalache ======================================================================================== diff --git a/docs/spec/fastsync/verification/Tinychain.tla b/docs/spec/fastsync/verification/Tinychain.tla index b46d35111..bfd2bdf3b 100644 --- a/docs/spec/fastsync/verification/Tinychain.tla +++ b/docs/spec/fastsync/verification/Tinychain.tla @@ -5,7 +5,6 @@ EXTENDS Sequences, Integers -------------------------- MODULE ApalacheTypes ----------------------------------- \* type annotation a <: b == a @@ -14,17 +13,17 @@ VST == STRING \* LastCommit type. \* It contains the id of the committed block -\* and the set of the validators who have committed the block +\* and the set of the validators who have committed the block. +\* In the implementation, blockId is the hash of the previous block, which cannot be forged LCT == [blockId |-> Int, commiters |-> VST] \* Block type. \* A block contains its height, validator set, next validator set, and last commit -BT == [height |-> Int, VS |-> VST, NextVS |-> VST, lastCommit |-> LCT] +BT == [hash |-> Int, wellFormed |-> BOOLEAN, + VS |-> VST, NextVS |-> VST, lastCommit |-> LCT] SeqOfBT(s) == s <: Seq(BT) -================================================================================== -INSTANCE ApalacheTypes CONSTANTS (* @@ -33,55 +32,72 @@ CONSTANTS e.g., "s1", "s2", etc. *) VALIDATOR_SETS, + (* a nil validator set that is outside of VALIDATOR_SETS *) + NIL_VS, (* The maximal height, up to which the blockchain may grow *) MAX_HEIGHT VARIABLES (* The blockchain as a sequence of blocks *) chain + +Heights == 1..MAX_HEIGHT + +\* the set of block identifiers, simply the heights extended with 0 +BlockIds == 0..MAX_HEIGHT + +\* the set of all possible commits +Commits == [blockId: BlockIds, commiters: VALIDATOR_SETS] + +\* the set of all possible blocks, not necessarily valid ones +Blocks == + [hash: Heights, wellFormed: BOOLEAN, + VS: VALIDATOR_SETS, NextVS: VALIDATOR_SETS, lastCommit: Commits] \* Initially, the blockchain contains one trusted block -Init == +ChainInit == \E vs \in VALIDATOR_SETS: \* the last commit in the trusted block is somewhat weird LET lastCommit == [blockId |-> 0, commiters |-> vs] IN chain = SeqOfBT(<< - [height |-> 1, VS |-> vs, NextVS |-> vs, lastCommit |-> lastCommit + [hash |-> 1, wellFormed |-> TRUE, + VS |-> vs, NextVS |-> vs, lastCommit |-> lastCommit ]>>) \* Add one more block to the blockchain AdvanceChain == \E NextVS \in VALIDATOR_SETS: LET last == chain[Len(chain)] - lastCommit == [blockId |-> last.height, commiters |-> last.VS] - newBlock == [height |-> last.height + 1, + lastCommit == [blockId |-> last.hash, commiters |-> last.VS] + newBlock == [hash |-> last.hash + 1, VS |-> last.NextVS, NextVS |-> NextVS, - lastCommit |-> lastCommit] + lastCommit |-> lastCommit, + wellFormed |-> TRUE] IN chain' = Append(chain, newBlock) \* The blockchain may grow up to the maximum and then stutter -Next == +ChainNext == \/ Len(chain) < MAX_HEIGHT /\ AdvanceChain \/ Len(chain) >= MAX_HEIGHT /\ UNCHANGED chain \* The basic properties of blocks in the blockchain: \* They should pass the validity check and they may verify the next block. -\* Is a block valid against the next validator set (of the previous block) -IsValid(block, nextVS) == +\* Does the block pass the consistency check against the next validators of the previous block +IsMatchingValidators(block, nextVS) == \* simply check that the validator set is propagated correctly. \* (the implementation tests hashes and the application state) block.VS = nextVS \* Does the block verify the commit (of the next block) -DoesVerify(block, commit) == +PossibleCommit(block, commit) == \* the commits are signed by the block validators /\ commit.commiters = block.VS - \* the block id in the commit matches the block height + \* the block id in the commit matches the block hash \* (the implementation has more extensive tests) - /\ commit.blockId = block.height + /\ commit.blockId = block.hash \* Basic invariants @@ -89,11 +105,11 @@ DoesVerify(block, commit) == \* every block has the validator set that is chosen by its predecessor ValidBlockInv == \A h \in 2..Len(chain): - IsValid(chain[h], chain[h - 1].NextVS) + IsMatchingValidators(chain[h], chain[h - 1].NextVS) \* last commit of every block is signed by the validators of the predecessor VerifiedBlockInv == \A h \in 2..Len(chain): - DoesVerify(chain[h - 1], chain[h].lastCommit) + PossibleCommit(chain[h - 1], chain[h].lastCommit) ================================================================================== diff --git a/docs/spec/fastsync/verification/fastsync_apalache.tla b/docs/spec/fastsync/verification/fastsync_apalache.tla index 1f4642b32..e18bfeff3 100644 --- a/docs/spec/fastsync/verification/fastsync_apalache.tla +++ b/docs/spec/fastsync/verification/fastsync_apalache.tla @@ -55,40 +55,10 @@ that node does not know initially the peer heights. EXTENDS Integers, FiniteSets, Sequences -(* Type definitions for Apalache *) -a <: b == a \* type annotation - -PIDT == STRING \* type of process ids -AsPidSet(a) == a <: {PIDT} - -\* LastCommit type -LCT == [blockId |-> Int, enoughVotingPower |-> BOOLEAN] - -\* Block type -BT == [height |-> Int, lastCommit |-> LCT, wellFormed |-> BOOLEAN] - -\* ControlMessage type -CMT == [type |-> STRING, peerId |-> PIDT] \* type of control messages - -\* InMsg type -IMT == [type |-> STRING, peerId |-> PIDT, height |-> Int, block |-> BT] -AsInMsg(m) == m <: IMT -AsInMsgSet(S) == S <: {IMT} - -\* OutMsg type -OMT == [type |-> STRING, peerId |-> PIDT, height |-> Int] -AsOutMsg(m) == m <: OMT -AsOutMsgSet(S) == S <: {OMT} - -BPT == [height |-> Int, peerIds |-> {PIDT}, peerHeights |-> [PIDT -> Int], - blockStore |-> [Int -> BT], receivedBlocks |-> [Int -> PIDT], - pendingBlocks |-> [Int -> PIDT], syncedBlocks |-> Int, syncHeight |-> Int] -AsBlockPool(bp) == bp <: BPT - -(* End of type definitions *) - -CONSTANTS MAX_HEIGHT, +CONSTANTS MAX_HEIGHT, \* the maximal height of blockchain + VALIDATOR_SETS, \* abstract set of validators + NIL_VS, \* a nil validator set CORRECT, \* set of correct peers FAULTY, \* set of faulty peers TARGET_PENDING, \* maximum number of pending requests + downloaded blocks that are not yet processed @@ -98,9 +68,11 @@ ASSUME CORRECT \intersect FAULTY = {} ASSUME TARGET_PENDING > 0 ASSUME PEER_MAX_REQUESTS > 0 - -\* the set of potential heights -Heights == 1..MAX_HEIGHT +\* the blockchain, see Tinychain +VARIABLE chain + +\* introduce tiny chain as the source of blocks for the correct nodes +INSTANCE Tinychain \* simplifies execute blocks logic. Used only in block store. HeightsPlus == 1..MAX_HEIGHT+1 @@ -114,27 +86,21 @@ GenesisHeight == 1 \* the set of all peer ids the node can receive a message from AllPeerIds == CORRECT \union FAULTY -\* the set of potential blocks ids. For simplification, correct blocks are equal to block height. -BlockIds == Heights \union {NilHeight} - -LastCommits == [blockId: BlockIds, enoughVotingPower: BOOLEAN] - \* Correct last commit have enough voting power, i.e., +2/3 of the voting power of \* the corresponding validator set (enoughVotingPower = TRUE) that signs blockId. \* BlockId defines correct previous block (in the implementation it is the hash of the block). \* For simplicity, we model blockId as the height of the previous block. -CorrectLastCommit(h) == [blockId |-> h-1, enoughVotingPower |-> TRUE] - -NilCommit == [blockId |-> 0, enoughVotingPower |-> TRUE] +CorrectLastCommit(h) == chain[h].lastCommit -Blocks == [height: Heights, lastCommit: LastCommits, wellFormed: BOOLEAN] +NilCommit == [blockId |-> 0, commiters |-> NIL_VS] \*BlocksWithNil == [height: Heights, lastCommit: LastCommits, wellFormed: BOOLEAN] -\* correct node will create always valid blocks, i.e., wellFormed = true and lastCommit is correct. -CorrectBlock(h) == [height |-> h, lastCommit |-> CorrectLastCommit(h), wellFormed |-> TRUE] +\* correct node always supplies the blocks from the blockchain +CorrectBlock(h) == chain[h] -NilBlock == [height |-> 0, lastCommit |-> NilCommit, wellFormed |-> TRUE] +NilBlock == + [hash |-> 0, wellFormed |-> FALSE, lastCommit |-> NilCommit, VS |-> NIL_VS, NextVS |-> NIL_VS] \* a special value for an undefined peer NilPeer == "Nil" \* we have changed it to STRING for apalache efficiency @@ -172,10 +138,9 @@ VARIABLES ] *) peersState - \* the variables for the network and scheduler - VARIABLES +VARIABLES turn, \* who is taking the turn: "Peers" or "Node" inMsg, \* a node receives message by this variable outMsg \* a node sends a message by this variable @@ -184,6 +149,29 @@ VARIABLES (* the variables of the node *) nvars == <> +(* Type definitions for Apalache *) +PIDT == STRING \* type of process ids +AsPidSet(a) == a <: {PIDT} + +\* ControlMessage type +CMT == [type |-> STRING, peerId |-> PIDT] \* type of control messages + +\* InMsg type +IMT == [type |-> STRING, peerId |-> PIDT, height |-> Int, block |-> BT] +AsInMsg(m) == m <: IMT +AsInMsgSet(S) == S <: {IMT} + +\* OutMsg type +OMT == [type |-> STRING, peerId |-> PIDT, height |-> Int] +AsOutMsg(m) == m <: OMT +AsOutMsgSet(S) == S <: {OMT} + +BPT == [height |-> Int, peerIds |-> {PIDT}, peerHeights |-> [PIDT -> Int], + blockStore |-> [Int -> BT], receivedBlocks |-> [Int -> PIDT], + pendingBlocks |-> [Int -> PIDT], syncedBlocks |-> Int, syncHeight |-> Int] + +AsBlockPool(bp) == bp <: BPT + \* Control messages ControlMsgs == [type: {"addPeer"}, peerId: AllPeerIds] @@ -225,7 +213,7 @@ InitNode == peerHeights |-> [p \in AllPeerIds |-> NilHeight], \* no peer height is known blockStore |-> [h \in Heights |-> - IF h > GenesisHeight THEN NilBlock ELSE CorrectBlock(1)], + IF h > GenesisHeight THEN NilBlock ELSE chain[1]], receivedBlocks |-> [h \in Heights |-> NilPeer], pendingBlocks |-> [h \in Heights |-> NilPeer], syncedBlocks |-> -1 @@ -293,7 +281,7 @@ Returns new block pool. See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L522 *) HandleBlockResponse(msg, bPool) == - LET h == msg.block.height IN + LET h == msg.height IN IF /\ msg.peerId \in bPool.peerIds /\ bPool.blockStore[h] = NilBlock @@ -395,26 +383,27 @@ ComputeNextState(bPool) == (* Verify if commit is for the given block id and if commit has enough voting power. See https://github.com/tendermint/tendermint/blob/61057a8b0af2beadee106e47c4616b279e83c920/blockchain/v2/processor_context.go#L12 *) VerifyCommit(block, lastCommit) == - /\ lastCommit.enoughVotingPower - /\ lastCommit.blockId = block.height - + PossibleCommit(block, lastCommit) (* Tries to execute next block in the pool, i.e., defines block validation logic. Returns new block pool (peers that has send invalid blocks are removed). See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/processor.go#L135 *) ExecuteBlocks(bPool) == LET bStore == bPool.blockStore IN + LET block0 == bStore[bPool.height - 1] IN LET block1 == bStore[bPool.height] IN LET block2 == bStore[bPool.height+1] IN IF block1 = NilBlock \/ block2 = NilBlock THEN bPool \* we don't have two next consecutive blocks - ELSE IF bPool.height = GenesisHeight + 1 /\ ~VerifyCommit(bStore[GenesisHeight], block1.lastCommit) - THEN \* corner case: the block right after genesis is corrupted, evict it - RemovePeers({bPool.receivedBlocks[GenesisHeight + 1]}, bPool) + ELSE IF ~IsMatchingValidators(block1, block0.NextVS) \* the implementation stores NextVS in its state, not using block0 + \* \/ ~VerifyCommit(block0, block1.lastCommit) \* WE NEED THIS AT LEAST FOR THE TRUSTED BLOCK + THEN \* the block does not have the expected validator set + RemovePeers({bPool.receivedBlocks[bPool.height]}, bPool) ELSE IF ~VerifyCommit(block1, block2.lastCommit) + \*\/ ~IsMatchingValidators(block2, block1.NextVS) \* we need this check too THEN \* remove the peers of block1 and block2, as they are considered faulty - RemovePeers({bPool.receivedBlocks[block1.height], bPool.receivedBlocks[block2.height]}, bPool) + RemovePeers({bPool.receivedBlocks[bPool.height], bPool.receivedBlocks[bPool.height + 1]}, bPool) ELSE \* all good, execute block at position height [bPool EXCEPT !.height = bPool.height + 1] @@ -556,13 +545,12 @@ CreateBlockResponse(msg, pState, arbitraryBlock) == ] IN [msg |-> m, peers |-> npState] -GrowBlockchain(pState) == +GrowPeerHeight(pState) == \E p \in CORRECT: - /\ pState.peerHeights[p] < MAX_HEIGHT + /\ pState.peerHeights[p] < Len(chain) /\ peersState' = [pState EXCEPT !.peerHeights[p] = @ + 1] /\ inMsg' = AsInMsg(NoMsg) - SendStatusResponseMessage(pState) == /\ \E arbitraryHeight \in Heights: \E peer \in AllPeerIds: @@ -591,12 +579,19 @@ SendControlMessage == \/ SendRemovePeerMessage \/ SendSyncTimeoutMessage +\* An extremely important property of block hashes (blockId): +\* If a commit is correct, then the previous block in the block store must be also correct. +\* The same applies to the other direction. +UnforgeableBlockId(height, block) == + block.hash = chain[height].hash => block = chain[height] + SendBlockResponseMessage(pState) == \/ /\ pState.blocksRequested /= AsOutMsgSet({}) /\ \E msg \in pState.blocksRequested: \E block \in Blocks: LET msgAndPeers == CreateBlockResponse(msg, pState, block) IN + /\ UnforgeableBlockId(msg.height, block) /\ peersState' = msgAndPeers.peers /\ inMsg' = msgAndPeers.msg @@ -604,7 +599,7 @@ SendBlockResponseMessage(pState) == \/ /\ peersState' = pState /\ inMsg' \in AsInMsgSet([type: {"blockResponse"}, peerId: FAULTY, block: Blocks]) - SendNoBlockResponseMessage(pState) == +SendNoBlockResponseMessage(pState) == /\ peersState' = pState /\ inMsg' \in AsInMsgSet([type: {"noBlockResponse"}, peerId: FAULTY, height: Heights]) @@ -617,7 +612,7 @@ SendResponseMessage(pState) == NextEnvStep(pState) == \/ SendResponseMessage(pState) - \/ GrowBlockchain(pState) + \/ GrowPeerHeight(pState) \/ SendControlMessage @@ -626,12 +621,13 @@ NextEnvStep(pState) == NextPeers == LET pState == HandleRequest(outMsg, peersState) IN - \/ /\ outMsg' = AsOutMsg(NoMsg) - /\ NextEnvStep(pState) + /\ outMsg' = AsOutMsg(NoMsg) + /\ NextEnvStep(pState) \* the composition of the node, the peers, the network and scheduler Init == + /\ ChainInit \* init the blockchain /\ InitNode /\ InitPeers /\ turn = "Peers" @@ -639,15 +635,19 @@ Init == /\ outMsg = AsOutMsg([type |-> "statusRequest"]) Next == - IF turn = "Peers" - THEN - /\ NextPeers - /\ turn' = "Node" - /\ UNCHANGED nvars - ELSE - /\ NextNode - /\ turn' = "Peers" - /\ UNCHANGED peersState + IF Len(chain) < MAX_HEIGHT + \* fast-forward the blockchain to MAX_HEIGHT + THEN ChainNext /\ UNCHANGED <> + \* run fastsync + ELSE IF turn = "Peers" + THEN + /\ NextPeers + /\ turn' = "Node" + /\ UNCHANGED <> + ELSE + /\ NextNode + /\ turn' = "Peers" + /\ UNCHANGED <> @@ -742,12 +742,11 @@ SyncFromCorrectInv == \/ \A h \in 1..blockPool.height: blockPool.receivedBlocks[h] \in blockPool.peerIds \union {NilPeer} -\* All synchronized blocks are well-formed and have sufficiently many votes +\* All synchronized blocks are exactly like in the blockchain CorrectBlocksInv == \/ state /= "finished" \/ \A h \in 1..(blockPool.height - 1): - LET block == blockPool.blockStore[h] IN - block.wellFormed /\ block.lastCommit.enoughVotingPower + blockPool.blockStore[h] = chain[h] \* A false expectation that a correct process is never removed from the set of peer ids. \* A correct process may reply too late and then gets evicted. @@ -768,6 +767,6 @@ BlockPoolInvariant == \*============================================================================= \* Modification History -\* Last modified Mon May 18 16:08:46 CEST 2020 by igor +\* Last modified Tue May 19 20:21:15 CEST 2020 by igor \* Last modified Thu Apr 16 16:57:22 CEST 2020 by zarkomilosevic \* Created Tue Feb 04 10:36:18 CET 2020 by zarkomilosevic From 28969660f66822c0081a3d662971c7d83bb5c998 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Tue, 19 May 2020 21:43:09 +0200 Subject: [PATCH 05/34] introduced height again --- docs/spec/fastsync/verification/Tinychain.tla | 9 +++++---- .../fastsync/verification/fastsync_apalache.tla | 17 +++++++++-------- 2 files changed, 14 insertions(+), 12 deletions(-) diff --git a/docs/spec/fastsync/verification/Tinychain.tla b/docs/spec/fastsync/verification/Tinychain.tla index bfd2bdf3b..8d06c34fe 100644 --- a/docs/spec/fastsync/verification/Tinychain.tla +++ b/docs/spec/fastsync/verification/Tinychain.tla @@ -19,7 +19,7 @@ LCT == [blockId |-> Int, commiters |-> VST] \* Block type. \* A block contains its height, validator set, next validator set, and last commit -BT == [hash |-> Int, wellFormed |-> BOOLEAN, +BT == [height |-> Int, hash |-> Int, wellFormed |-> BOOLEAN, VS |-> VST, NextVS |-> VST, lastCommit |-> LCT] SeqOfBT(s) == s <: Seq(BT) @@ -51,7 +51,7 @@ Commits == [blockId: BlockIds, commiters: VALIDATOR_SETS] \* the set of all possible blocks, not necessarily valid ones Blocks == - [hash: Heights, wellFormed: BOOLEAN, + [height: Heights, hash: Heights, wellFormed: BOOLEAN, VS: VALIDATOR_SETS, NextVS: VALIDATOR_SETS, lastCommit: Commits] \* Initially, the blockchain contains one trusted block @@ -60,7 +60,7 @@ ChainInit == \* the last commit in the trusted block is somewhat weird LET lastCommit == [blockId |-> 0, commiters |-> vs] IN chain = SeqOfBT(<< - [hash |-> 1, wellFormed |-> TRUE, + [height |-> 1, hash |-> 1, wellFormed |-> TRUE, VS |-> vs, NextVS |-> vs, lastCommit |-> lastCommit ]>>) @@ -69,7 +69,8 @@ AdvanceChain == \E NextVS \in VALIDATOR_SETS: LET last == chain[Len(chain)] lastCommit == [blockId |-> last.hash, commiters |-> last.VS] - newBlock == [hash |-> last.hash + 1, + newBlock == [height |-> last.height + 1, + hash |-> last.hash + 1, VS |-> last.NextVS, NextVS |-> NextVS, lastCommit |-> lastCommit, diff --git a/docs/spec/fastsync/verification/fastsync_apalache.tla b/docs/spec/fastsync/verification/fastsync_apalache.tla index e18bfeff3..6440b7d46 100644 --- a/docs/spec/fastsync/verification/fastsync_apalache.tla +++ b/docs/spec/fastsync/verification/fastsync_apalache.tla @@ -100,7 +100,8 @@ NilCommit == [blockId |-> 0, commiters |-> NIL_VS] CorrectBlock(h) == chain[h] NilBlock == - [hash |-> 0, wellFormed |-> FALSE, lastCommit |-> NilCommit, VS |-> NIL_VS, NextVS |-> NIL_VS] + [height |-> 0, hash |-> 0, wellFormed |-> FALSE, + lastCommit |-> NilCommit, VS |-> NIL_VS, NextVS |-> NIL_VS] \* a special value for an undefined peer NilPeer == "Nil" \* we have changed it to STRING for apalache efficiency @@ -281,7 +282,7 @@ Returns new block pool. See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L522 *) HandleBlockResponse(msg, bPool) == - LET h == msg.height IN + LET h == msg.block.height IN IF /\ msg.peerId \in bPool.peerIds /\ bPool.blockStore[h] = NilBlock @@ -695,27 +696,27 @@ TypeOK == ] \* TODO: align with the English spec. Add reference to it -Correctness1 == state = "finished" => +Sync1 == state = "finished" => blockPool.height >= MaxCorrectPeerHeight(blockPool) \* TODO: align with the English spec. Add reference to it -Correctness2 == +Sync2 == \A p \in CORRECT: \/ p \notin blockPool.peerIds \/ [] (state = "finished" => blockPool.height >= blockPool.peerHeights[p] - 1) -Correctness2AsInv == +Sync2AsInv == \A p \in CORRECT: \/ p \notin blockPool.peerIds \/ (state = "finished" => blockPool.height >= blockPool.peerHeights[p] - 1) -Correctness3 == +Sync3 == \A p \in CORRECT: \/ p \notin blockPool.peerIds \/ blockPool.syncedBlocks <= 0 \* timeout \/ [] (state = "finished" => blockPool.height >= blockPool.peerHeights[p] - 1) -Correctness3AsInv == +Sync3AsInv == \A p \in CORRECT: \/ p \notin blockPool.peerIds \/ blockPool.syncedBlocks <= 0 \* timeout @@ -767,6 +768,6 @@ BlockPoolInvariant == \*============================================================================= \* Modification History -\* Last modified Tue May 19 20:21:15 CEST 2020 by igor +\* Last modified Tue May 19 21:29:52 CEST 2020 by igor \* Last modified Thu Apr 16 16:57:22 CEST 2020 by zarkomilosevic \* Created Tue Feb 04 10:36:18 CET 2020 by zarkomilosevic From 07e802cdf31d813692d8223f506cb452e71677c6 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 21 May 2020 13:20:52 +0200 Subject: [PATCH 06/34] fixed CorrectBlocks --- .../verification/fastsync_apalache.tla | 36 +++++++++++++------ 1 file changed, 26 insertions(+), 10 deletions(-) diff --git a/docs/spec/fastsync/verification/fastsync_apalache.tla b/docs/spec/fastsync/verification/fastsync_apalache.tla index 6440b7d46..19c267c87 100644 --- a/docs/spec/fastsync/verification/fastsync_apalache.tla +++ b/docs/spec/fastsync/verification/fastsync_apalache.tla @@ -206,6 +206,7 @@ OutMsgs == InitNode == \E pIds \in SUBSET AllPeerIds: \* set of peers node established initial connections with + /\ pIds \subseteq CORRECT /\ pIds /= AsPidSet({}) \* apalache better checks non-emptiness than subtracts from SUBSET /\ blockPool = AsBlockPool([ height |-> GenesisHeight + 1, \* the genesis block is at height 1 @@ -398,7 +399,7 @@ ExecuteBlocks(bPool) == IF block1 = NilBlock \/ block2 = NilBlock THEN bPool \* we don't have two next consecutive blocks ELSE IF ~IsMatchingValidators(block1, block0.NextVS) \* the implementation stores NextVS in its state, not using block0 - \* \/ ~VerifyCommit(block0, block1.lastCommit) \* WE NEED THIS AT LEAST FOR THE TRUSTED BLOCK + \/ ~VerifyCommit(block0, block1.lastCommit) \* WE NEED THIS AT LEAST FOR THE TRUSTED BLOCK THEN \* the block does not have the expected validator set RemovePeers({bPool.receivedBlocks[bPool.height]}, bPool) ELSE IF ~VerifyCommit(block1, block2.lastCommit) @@ -586,19 +587,34 @@ SendControlMessage == UnforgeableBlockId(height, block) == block.hash = chain[height].hash => block = chain[height] +\* a faulty peer cannot forge the validators signatures and thus cannot produce a fork +NoFork(height, block) == + LET refBlock == chain[height] IN + block.hash /= refBlock.hash => block.VS /= refBlock.VS + +\* can be block produced by a faulty peer +IsBlockByFaulty(height, block) == + /\ block.height = height + /\ UnforgeableBlockId(height, block) + /\ NoFork(height, block) SendBlockResponseMessage(pState) == + \* a response to a requested block: either by a correct, or by a faulty peer \/ /\ pState.blocksRequested /= AsOutMsgSet({}) /\ \E msg \in pState.blocksRequested: \E block \in Blocks: - LET msgAndPeers == CreateBlockResponse(msg, pState, block) IN - /\ UnforgeableBlockId(msg.height, block) - /\ peersState' = msgAndPeers.peers - /\ inMsg' = msgAndPeers.msg - - - \/ /\ peersState' = pState - /\ inMsg' \in AsInMsgSet([type: {"blockResponse"}, peerId: FAULTY, block: Blocks]) + /\ IsBlockByFaulty(msg.height, block) + /\ LET msgAndPeers == CreateBlockResponse(msg, pState, block) IN + /\ peersState' = msgAndPeers.peers + /\ inMsg' = msgAndPeers.msg + + \* a faulty peer can always send an unsolicited block + \/ \E peerId \in FAULTY: + \E block \in Blocks: + /\ IsBlockByFaulty(block.height, block) + /\ peersState' = pState + /\ inMsg' = AsInMsg([type |-> "blockResponse", + peerId |-> peerId, block |-> block]) SendNoBlockResponseMessage(pState) == /\ peersState' = pState @@ -768,6 +784,6 @@ BlockPoolInvariant == \*============================================================================= \* Modification History -\* Last modified Tue May 19 21:29:52 CEST 2020 by igor +\* Last modified Wed May 20 10:42:38 CEST 2020 by igor \* Last modified Thu Apr 16 16:57:22 CEST 2020 by zarkomilosevic \* Created Tue Feb 04 10:36:18 CET 2020 by zarkomilosevic From 1289aa04249e7f8709c413b61793274b646c36e9 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 25 May 2020 16:48:57 +0200 Subject: [PATCH 07/34] simplified the blockchain spec --- docs/spec/fastsync/verification/Tinychain.tla | 94 ++++++++----------- .../verification/fastsync_apalache.tla | 41 ++++---- 2 files changed, 55 insertions(+), 80 deletions(-) diff --git a/docs/spec/fastsync/verification/Tinychain.tla b/docs/spec/fastsync/verification/Tinychain.tla index 8d06c34fe..268aa250b 100644 --- a/docs/spec/fastsync/verification/Tinychain.tla +++ b/docs/spec/fastsync/verification/Tinychain.tla @@ -3,7 +3,7 @@ the relation between validator sets, next validator sets, and last commits. *) -EXTENDS Sequences, Integers +EXTENDS Integers \* type annotation a <: b == a @@ -12,19 +12,20 @@ a <: b == a VST == STRING \* LastCommit type. -\* It contains the id of the committed block -\* and the set of the validators who have committed the block. -\* In the implementation, blockId is the hash of the previous block, which cannot be forged -LCT == [blockId |-> Int, commiters |-> VST] +\* It contains: +\* 1) the flag of whether the block id equals to the hash of the previous block, and +\* 2) the set of the validators who have committed the block. +\* In the implementation, blockId is the hash of the previous block, which cannot be forged. +\* We abstract block id into whether it equals to the hash of the previous block or not. +LCT == [blockIdEqRef |-> BOOLEAN, committers |-> VST] \* Block type. -\* A block contains its height, validator set, next validator set, and last commit -BT == [height |-> Int, hash |-> Int, wellFormed |-> BOOLEAN, +\* A block contains its height, validator set, next validator set, and last commit. +\* Moreover, it contains the flag that tells us whether the block equals to the one +\* on the reference chain (this is an abstraction of hash). +BT == [height |-> Int, hashEqRef |-> BOOLEAN, wellFormed |-> BOOLEAN, VS |-> VST, NextVS |-> VST, lastCommit |-> LCT] -SeqOfBT(s) == s <: Seq(BT) - - CONSTANTS (* A set of abstract values, each value representing a set of validators. @@ -36,54 +37,34 @@ CONSTANTS NIL_VS, (* The maximal height, up to which the blockchain may grow *) MAX_HEIGHT - -VARIABLES - (* The blockchain as a sequence of blocks *) - chain Heights == 1..MAX_HEIGHT -\* the set of block identifiers, simply the heights extended with 0 -BlockIds == 0..MAX_HEIGHT - \* the set of all possible commits -Commits == [blockId: BlockIds, commiters: VALIDATOR_SETS] +Commits == [blockIdEqRef: BOOLEAN, committers: VALIDATOR_SETS] \* the set of all possible blocks, not necessarily valid ones Blocks == - [height: Heights, hash: Heights, wellFormed: BOOLEAN, + [height: Heights, hashEqRef: BOOLEAN, wellFormed: BOOLEAN, VS: VALIDATOR_SETS, NextVS: VALIDATOR_SETS, lastCommit: Commits] -\* Initially, the blockchain contains one trusted block -ChainInit == - \E vs \in VALIDATOR_SETS: - \* the last commit in the trusted block is somewhat weird - LET lastCommit == [blockId |-> 0, commiters |-> vs] IN - chain = SeqOfBT(<< - [height |-> 1, hash |-> 1, wellFormed |-> TRUE, - VS |-> vs, NextVS |-> vs, lastCommit |-> lastCommit - ]>>) - -\* Add one more block to the blockchain -AdvanceChain == - \E NextVS \in VALIDATOR_SETS: - LET last == chain[Len(chain)] - lastCommit == [blockId |-> last.hash, commiters |-> last.VS] - newBlock == [height |-> last.height + 1, - hash |-> last.hash + 1, - VS |-> last.NextVS, - NextVS |-> NextVS, - lastCommit |-> lastCommit, - wellFormed |-> TRUE] - IN - chain' = Append(chain, newBlock) - -\* The blockchain may grow up to the maximum and then stutter -ChainNext == - \/ Len(chain) < MAX_HEIGHT /\ AdvanceChain - \/ Len(chain) >= MAX_HEIGHT /\ UNCHANGED chain +\* Does the chain contain a sound sequence of blocks that could be produced by +\* a 2/3 of faulty validators. This operator can be used to initialise the chain! +IsCorrectChain(chain) == + /\ chain \in [1..MAX_HEIGHT -> Blocks] + /\ \A h \in 1..MAX_HEIGHT: + LET b == chain[h] IN + /\ b.height = h \* the height is correct + /\ b.wellFormed \* the block structure is OK + /\ b.hashEqRef \* the hash equals to that of the reference block (itself!) + /\ b.lastCommit.blockIdEqRef \* the hash in the last commit is OK + /\ h > 1 => + LET p == chain[h - 1] IN + /\ b.VS = p.NextVS \* the validators propagate from the previous block + /\ b.lastCommit.committers = p.VS \* and they are the committers -\* The basic properties of blocks in the blockchain: + +\* The basic properties of blocks on the blockchain: \* They should pass the validity check and they may verify the next block. \* Does the block pass the consistency check against the next validators of the previous block @@ -95,22 +76,21 @@ IsMatchingValidators(block, nextVS) == \* Does the block verify the commit (of the next block) PossibleCommit(block, commit) == \* the commits are signed by the block validators - /\ commit.commiters = block.VS - \* the block id in the commit matches the block hash - \* (the implementation has more extensive tests) - /\ commit.blockId = block.hash - + /\ commit.committers = block.VS + \* The block id in the commit matches the block hash (abstract comparison). + \* (The implementation has extensive tests for that.) + /\ commit.blockIdEqRef = block.hashEqRef \* Basic invariants \* every block has the validator set that is chosen by its predecessor -ValidBlockInv == - \A h \in 2..Len(chain): +ValidBlockInv(chain) == + \A h \in 2..MAX_HEIGHT: IsMatchingValidators(chain[h], chain[h - 1].NextVS) \* last commit of every block is signed by the validators of the predecessor -VerifiedBlockInv == - \A h \in 2..Len(chain): +VerifiedBlockInv(chain) == + \A h \in 2..MAX_HEIGHT: PossibleCommit(chain[h - 1], chain[h].lastCommit) ================================================================================== diff --git a/docs/spec/fastsync/verification/fastsync_apalache.tla b/docs/spec/fastsync/verification/fastsync_apalache.tla index 19c267c87..d3bebbd0e 100644 --- a/docs/spec/fastsync/verification/fastsync_apalache.tla +++ b/docs/spec/fastsync/verification/fastsync_apalache.tla @@ -89,10 +89,11 @@ AllPeerIds == CORRECT \union FAULTY \* Correct last commit have enough voting power, i.e., +2/3 of the voting power of \* the corresponding validator set (enoughVotingPower = TRUE) that signs blockId. \* BlockId defines correct previous block (in the implementation it is the hash of the block). -\* For simplicity, we model blockId as the height of the previous block. +\* Instead of blockId, we encode blockIdEqRef, which is true, if the block id is equal +\* to the hash of the previous block, see Tinychain. CorrectLastCommit(h) == chain[h].lastCommit -NilCommit == [blockId |-> 0, commiters |-> NIL_VS] +NilCommit == [blockIdEqRef |-> FALSE, committers |-> NIL_VS] \*BlocksWithNil == [height: Heights, lastCommit: LastCommits, wellFormed: BOOLEAN] @@ -100,7 +101,7 @@ NilCommit == [blockId |-> 0, commiters |-> NIL_VS] CorrectBlock(h) == chain[h] NilBlock == - [height |-> 0, hash |-> 0, wellFormed |-> FALSE, + [height |-> 0, hashEqRef |-> FALSE, wellFormed |-> FALSE, lastCommit |-> NilCommit, VS |-> NIL_VS, NextVS |-> NIL_VS] \* a special value for an undefined peer @@ -549,7 +550,7 @@ CreateBlockResponse(msg, pState, arbitraryBlock) == GrowPeerHeight(pState) == \E p \in CORRECT: - /\ pState.peerHeights[p] < Len(chain) + /\ pState.peerHeights[p] < MAX_HEIGHT /\ peersState' = [pState EXCEPT !.peerHeights[p] = @ + 1] /\ inMsg' = AsInMsg(NoMsg) @@ -585,12 +586,12 @@ SendControlMessage == \* If a commit is correct, then the previous block in the block store must be also correct. \* The same applies to the other direction. UnforgeableBlockId(height, block) == - block.hash = chain[height].hash => block = chain[height] + block.hashEqRef => block = chain[height] \* a faulty peer cannot forge the validators signatures and thus cannot produce a fork NoFork(height, block) == LET refBlock == chain[height] IN - block.hash /= refBlock.hash => block.VS /= refBlock.VS + ~block.hashEqRef => block.VS /= refBlock.VS \* can be block produced by a faulty peer IsBlockByFaulty(height, block) == @@ -644,7 +645,7 @@ NextPeers == \* the composition of the node, the peers, the network and scheduler Init == - /\ ChainInit \* init the blockchain + /\ IsCorrectChain(chain) \* initialize the blockchain /\ InitNode /\ InitPeers /\ turn = "Peers" @@ -652,29 +653,23 @@ Init == /\ outMsg = AsOutMsg([type |-> "statusRequest"]) Next == - IF Len(chain) < MAX_HEIGHT - \* fast-forward the blockchain to MAX_HEIGHT - THEN ChainNext /\ UNCHANGED <> - \* run fastsync - ELSE IF turn = "Peers" - THEN - /\ NextPeers - /\ turn' = "Node" - /\ UNCHANGED <> - ELSE - /\ NextNode - /\ turn' = "Peers" - /\ UNCHANGED <> - + IF turn = "Peers" + THEN + /\ NextPeers + /\ turn' = "Node" + /\ UNCHANGED <> + ELSE + /\ NextNode + /\ turn' = "Peers" + /\ UNCHANGED <> FlipTurn == - turn' = ( + turn' = IF turn = "Peers" THEN "Node" ELSE "Peers" - ) \* Compute max peer height. Used as a helper operator in properties. From 074d2c5980802913fcb293ff2c22111be7020742 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 25 May 2020 19:48:55 +0200 Subject: [PATCH 08/34] decreasing the search space, to give TLC a chance --- docs/spec/fastsync/verification/MC_1_0_4.tla | 17 +++++++++++++++++ docs/spec/fastsync/verification/MC_2_0_4.tla | 17 +++++++++++++++++ docs/spec/fastsync/verification/Tinychain.tla | 10 ++++++---- .../fastsync/verification/fastsync_apalache.tla | 17 ++++++++++------- 4 files changed, 50 insertions(+), 11 deletions(-) create mode 100644 docs/spec/fastsync/verification/MC_1_0_4.tla create mode 100644 docs/spec/fastsync/verification/MC_2_0_4.tla diff --git a/docs/spec/fastsync/verification/MC_1_0_4.tla b/docs/spec/fastsync/verification/MC_1_0_4.tla new file mode 100644 index 000000000..b4ab71228 --- /dev/null +++ b/docs/spec/fastsync/verification/MC_1_0_4.tla @@ -0,0 +1,17 @@ +--------------------------- MODULE MC_1_0_4 ------------------------------------ + +\*a <: b == a \* type annotation + +VALIDATOR_SETS == {"vs1", "vs2"} +NIL_VS == "NilVS" +CORRECT == {"c1"} +FAULTY == {"f2"} \ {"f2"} +MAX_HEIGHT == 4 +PEER_MAX_REQUESTS == 2 +TARGET_PENDING == 3 + +VARIABLES + state, blockPool, peersState, chain, turn, inMsg, outMsg + +INSTANCE fastsync_apalache +================================================================================ diff --git a/docs/spec/fastsync/verification/MC_2_0_4.tla b/docs/spec/fastsync/verification/MC_2_0_4.tla new file mode 100644 index 000000000..b39dcd608 --- /dev/null +++ b/docs/spec/fastsync/verification/MC_2_0_4.tla @@ -0,0 +1,17 @@ +--------------------------- MODULE MC_2_0_4 ------------------------------------ + +a <: b == a \* type annotation + +VALIDATOR_SETS == {"vs1", "vs2"} +NIL_VS == "NilVS" +CORRECT == {"c1", "c2"} +FAULTY == {} <: {STRING} +MAX_HEIGHT == 4 +PEER_MAX_REQUESTS == 2 +TARGET_PENDING == 3 + +VARIABLES + state, blockPool, peersState, chain, turn, inMsg, outMsg + +INSTANCE fastsync_apalache +================================================================================ diff --git a/docs/spec/fastsync/verification/Tinychain.tla b/docs/spec/fastsync/verification/Tinychain.tla index 268aa250b..7a0b66ab4 100644 --- a/docs/spec/fastsync/verification/Tinychain.tla +++ b/docs/spec/fastsync/verification/Tinychain.tla @@ -51,13 +51,15 @@ Blocks == \* Does the chain contain a sound sequence of blocks that could be produced by \* a 2/3 of faulty validators. This operator can be used to initialise the chain! IsCorrectChain(chain) == - /\ chain \in [1..MAX_HEIGHT -> Blocks] + \* restrict the structure of the blocks, to decrease the TLC search space + LET OkCommits == [blockIdEqRef: {TRUE}, committers: VALIDATOR_SETS] + OkBlocks == [height: Heights, hashEqRef: {TRUE}, wellFormed: {TRUE}, + VS: VALIDATOR_SETS, NextVS: VALIDATOR_SETS, lastCommit: OkCommits] + IN + /\ chain \in [1..MAX_HEIGHT -> OkBlocks] /\ \A h \in 1..MAX_HEIGHT: LET b == chain[h] IN /\ b.height = h \* the height is correct - /\ b.wellFormed \* the block structure is OK - /\ b.hashEqRef \* the hash equals to that of the reference block (itself!) - /\ b.lastCommit.blockIdEqRef \* the hash in the last commit is OK /\ h > 1 => LET p == chain[h - 1] IN /\ b.VS = p.NextVS \* the validators propagate from the previous block diff --git a/docs/spec/fastsync/verification/fastsync_apalache.tla b/docs/spec/fastsync/verification/fastsync_apalache.tla index d3bebbd0e..2276c9c97 100644 --- a/docs/spec/fastsync/verification/fastsync_apalache.tla +++ b/docs/spec/fastsync/verification/fastsync_apalache.tla @@ -58,7 +58,7 @@ EXTENDS Integers, FiniteSets, Sequences CONSTANTS MAX_HEIGHT, \* the maximal height of blockchain VALIDATOR_SETS, \* abstract set of validators - NIL_VS, \* a nil validator set + NIL_VS, \* a nil validator set CORRECT, \* set of correct peers FAULTY, \* set of faulty peers TARGET_PENDING, \* maximum number of pending requests + downloaded blocks that are not yet processed @@ -584,11 +584,10 @@ SendControlMessage == \* An extremely important property of block hashes (blockId): \* If a commit is correct, then the previous block in the block store must be also correct. -\* The same applies to the other direction. UnforgeableBlockId(height, block) == block.hashEqRef => block = chain[height] -\* a faulty peer cannot forge the validators signatures and thus cannot produce a fork +\* A faulty peer cannot forge the validators signatures and thus cannot produce a fork. NoFork(height, block) == LET refBlock == chain[height] IN ~block.hashEqRef => block.VS /= refBlock.VS @@ -707,8 +706,12 @@ TypeOK == ] \* TODO: align with the English spec. Add reference to it -Sync1 == state = "finished" => - blockPool.height >= MaxCorrectPeerHeight(blockPool) +Sync1 == + [](state = "finished" => + blockPool.height >= MaxCorrectPeerHeight(blockPool)) + +Sync1AsInv == + state = "finished" => blockPool.height >= MaxCorrectPeerHeight(blockPool) \* TODO: align with the English spec. Add reference to it Sync2 == @@ -736,7 +739,7 @@ Sync3AsInv == \* TODO: align with the English spec. Add reference to it \* FIXME: uncomment when the Apalache issue is fixed: \* https://github.com/konnov/apalache/issues/145 -\*Termination == WF_turn(FlipTurn) => <>(state = "finished") +Termination == WF_turn(FlipTurn) => <>(state = "finished") \* a few simple properties that trigger counterexamples @@ -779,6 +782,6 @@ BlockPoolInvariant == \*============================================================================= \* Modification History -\* Last modified Wed May 20 10:42:38 CEST 2020 by igor +\* Last modified Mon May 25 19:48:46 CEST 2020 by igor \* Last modified Thu Apr 16 16:57:22 CEST 2020 by zarkomilosevic \* Created Tue Feb 04 10:36:18 CET 2020 by zarkomilosevic From 1137a8376f06d28cdf1f184f376d2c29924fa673 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 25 May 2020 22:56:19 +0200 Subject: [PATCH 09/34] added Termination2 --- .../verification/fastsync_apalache.tla | 21 ++++++++++--------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/docs/spec/fastsync/verification/fastsync_apalache.tla b/docs/spec/fastsync/verification/fastsync_apalache.tla index 2276c9c97..400ea9a77 100644 --- a/docs/spec/fastsync/verification/fastsync_apalache.tla +++ b/docs/spec/fastsync/verification/fastsync_apalache.tla @@ -564,17 +564,14 @@ SendStatusResponseMessage(pState) == SendAddPeerMessage == \E peer \in AllPeerIds: - /\ inMsg' = AsInMsg([type |-> "addPeer", peerId |-> peer]) - /\ UNCHANGED peersState + inMsg' = AsInMsg([type |-> "addPeer", peerId |-> peer]) SendRemovePeerMessage == \E peer \in AllPeerIds: - /\ inMsg' = AsInMsg([type |-> "removePeer", peerId |-> peer]) - /\ UNCHANGED peersState + inMsg' = AsInMsg([type |-> "removePeer", peerId |-> peer]) SendSyncTimeoutMessage == - /\ inMsg' = AsInMsg([type |-> "syncTimeout"]) - /\ UNCHANGED peersState + inMsg' = AsInMsg([type |-> "syncTimeout"]) SendControlMessage == @@ -630,7 +627,7 @@ SendResponseMessage(pState) == NextEnvStep(pState) == \/ SendResponseMessage(pState) \/ GrowPeerHeight(pState) - \/ SendControlMessage + \/ SendControlMessage /\ peersState' = pState \* Peers consume a message and update it's local state. It then makes a single step, i.e., it sends at most single message. @@ -737,10 +734,14 @@ Sync3AsInv == \/ (state = "finished" => blockPool.height >= blockPool.peerHeights[p] - 1) \* TODO: align with the English spec. Add reference to it -\* FIXME: uncomment when the Apalache issue is fixed: -\* https://github.com/konnov/apalache/issues/145 +\* This property is violated, as we do not track precisely timeouts Termination == WF_turn(FlipTurn) => <>(state = "finished") +\* This property holds true +Termination2 == (WF_turn(FlipTurn) + /\ <>[](inMsg.type \notin {"statusResponse", "addPeer", "removePeer"})) + => <>(state = "finished") + \* a few simple properties that trigger counterexamples \* Shows execution in which peer set is empty @@ -782,6 +783,6 @@ BlockPoolInvariant == \*============================================================================= \* Modification History -\* Last modified Mon May 25 19:48:46 CEST 2020 by igor +\* Last modified Mon May 25 21:03:53 CEST 2020 by igor \* Last modified Thu Apr 16 16:57:22 CEST 2020 by zarkomilosevic \* Created Tue Feb 04 10:36:18 CET 2020 by zarkomilosevic From 853b74052ad95ee095cee0bd97c0f8af30d57043 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Tue, 26 May 2020 13:42:01 +0200 Subject: [PATCH 10/34] a few fixes --- .../verification/fastsync_apalache.tla | 39 ++++++++++++------- 1 file changed, 24 insertions(+), 15 deletions(-) diff --git a/docs/spec/fastsync/verification/fastsync_apalache.tla b/docs/spec/fastsync/verification/fastsync_apalache.tla index 400ea9a77..d9b726fba 100644 --- a/docs/spec/fastsync/verification/fastsync_apalache.tla +++ b/docs/spec/fastsync/verification/fastsync_apalache.tla @@ -81,7 +81,7 @@ HeightsPlus == 1..MAX_HEIGHT+1 NilHeight == 0 \* the height of the genesis block -GenesisHeight == 1 +TrustedHeight == 1 \* the set of all peer ids the node can receive a message from AllPeerIds == CORRECT \union FAULTY @@ -176,31 +176,31 @@ AsBlockPool(bp) == bp <: BPT \* Control messages ControlMsgs == - [type: {"addPeer"}, peerId: AllPeerIds] + AsInMsgSet([type: {"addPeer"}, peerId: AllPeerIds]) \union - [type: {"removePeer"}, peerId: AllPeerIds] + AsInMsgSet([type: {"removePeer"}, peerId: AllPeerIds]) \union - [type: {"syncTimeout"}] + AsInMsgSet([type: {"syncTimeout"}]) \* All messages (and events) received by a node InMsgs == - {NoMsg} + AsInMsgSet({NoMsg}) \union - [type: {"blockResponse"}, peerId: AllPeerIds, block: Blocks] + AsInMsgSet([type: {"blockResponse"}, peerId: AllPeerIds, block: Blocks]) \union - [type: {"noBlockResponse"}, peerId: AllPeerIds, height: Heights] + AsInMsgSet([type: {"noBlockResponse"}, peerId: AllPeerIds, height: Heights]) \union - [type: {"statusResponse"}, peerId: AllPeerIds, height: Heights] + AsInMsgSet([type: {"statusResponse"}, peerId: AllPeerIds, height: Heights]) \union ControlMsgs \* Messages sent by a node and received by peers (environment in our case) OutMsgs == - {NoMsg} + AsOutMsgSet({NoMsg}) \union - [type: {"statusRequest"}] \* StatusRequest is broadcast to the set of connected peers. + AsOutMsgSet([type: {"statusRequest"}]) \* StatusRequest is broadcast to the set of connected peers. \union - [type: {"blockRequest"}, peerId: AllPeerIds, height: Heights] + AsOutMsgSet([type: {"blockRequest"}, peerId: AllPeerIds, height: Heights]) (********************************** NODE ***********************************) @@ -210,13 +210,13 @@ InitNode == /\ pIds \subseteq CORRECT /\ pIds /= AsPidSet({}) \* apalache better checks non-emptiness than subtracts from SUBSET /\ blockPool = AsBlockPool([ - height |-> GenesisHeight + 1, \* the genesis block is at height 1 - syncHeight |-> GenesisHeight + 1, \* and we are synchronized to it + height |-> TrustedHeight + 1, \* the genesis block is at height 1 + syncHeight |-> TrustedHeight + 1, \* and we are synchronized to it peerIds |-> pIds, peerHeights |-> [p \in AllPeerIds |-> NilHeight], \* no peer height is known blockStore |-> [h \in Heights |-> - IF h > GenesisHeight THEN NilBlock ELSE chain[1]], + IF h > TrustedHeight THEN NilBlock ELSE chain[1]], receivedBlocks |-> [h \in Heights |-> NilPeer], pendingBlocks |-> [h \in Heights |-> NilPeer], syncedBlocks |-> -1 @@ -690,7 +690,6 @@ TypeOK == [type: {"blockRequest"}, peerId: AllPeerIds, height: Heights] ] - /\ blockPool \in [ height: Heights, peerIds: SUBSET AllPeerIds, @@ -702,6 +701,16 @@ TypeOK == syncHeight: Heights ] + (* + \* the constraints that would be better handled by apalache? + /\ \E PH \in [AllPeerIds -> Heights \union {NilHeight}]: + \E BR \in SUBSET [type: {"blockRequest"}, peerId: AllPeerIds, height: Heights]: + \E sr \in BOOLEAN: + peersState = [ peerHeights |-> PH, + statusRequested |-> sr, + blocksRequested |-> BR ] + *) + \* TODO: align with the English spec. Add reference to it Sync1 == [](state = "finished" => From 09c00be3add86746a23d7e8318d0fb8fc4155b76 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 27 May 2020 20:55:40 +0200 Subject: [PATCH 11/34] a better way of using the abstract hashes --- docs/spec/fastsync/verification/fastsync_apalache.tla | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/docs/spec/fastsync/verification/fastsync_apalache.tla b/docs/spec/fastsync/verification/fastsync_apalache.tla index d9b726fba..972ba59a1 100644 --- a/docs/spec/fastsync/verification/fastsync_apalache.tla +++ b/docs/spec/fastsync/verification/fastsync_apalache.tla @@ -584,12 +584,13 @@ SendControlMessage == UnforgeableBlockId(height, block) == block.hashEqRef => block = chain[height] -\* A faulty peer cannot forge the validators signatures and thus cannot produce a fork. +\* A faulty peer cannot forge enough of the validators signatures. +\* A more precise rule should have checked that the commiters have over 2/3 of the VS's voting power. NoFork(height, block) == - LET refBlock == chain[height] IN - ~block.hashEqRef => block.VS /= refBlock.VS + (height > 1 /\ block.lastCommit.committers = chain[height - 1].VS) + => block.lastCommit.blockIdEqRef -\* can be block produced by a faulty peer +\* Can be block produced by a faulty peer IsBlockByFaulty(height, block) == /\ block.height = height /\ UnforgeableBlockId(height, block) @@ -792,6 +793,6 @@ BlockPoolInvariant == \*============================================================================= \* Modification History -\* Last modified Mon May 25 21:03:53 CEST 2020 by igor +\* Last modified Wed May 27 19:15:23 CEST 2020 by igor \* Last modified Thu Apr 16 16:57:22 CEST 2020 by zarkomilosevic \* Created Tue Feb 04 10:36:18 CET 2020 by zarkomilosevic From c8bb4eb13cee3527925061f3951f7b7ec9eb8efd Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 27 May 2020 23:28:36 +0200 Subject: [PATCH 12/34] configuration files for the repeatable experiments --- docs/spec/fastsync/verification/001bmc-apalache.csv | 7 +++++++ docs/spec/fastsync/verification/002tlc-tlc.csv | 9 +++++++++ .../spec/fastsync/verification/MC-CorrectBlocksInv.cfg | 10 ++++++++++ .../verification/MC-CorrectNeverSuspectedInv.cfg | 10 ++++++++++ docs/spec/fastsync/verification/MC-Sync1AsInv.cfg | 10 ++++++++++ docs/spec/fastsync/verification/MC-Sync2AsInv.cfg | 10 ++++++++++ docs/spec/fastsync/verification/MC-Sync3AsInv.cfg | 10 ++++++++++ .../fastsync/verification/MC-SyncFromCorrectInv.cfg | 10 ++++++++++ docs/spec/fastsync/verification/MC-Termination.cfg | 10 ++++++++++ docs/spec/fastsync/verification/MC-Termination2.cfg | 10 ++++++++++ docs/spec/fastsync/verification/bfs.csv | 5 +++++ 11 files changed, 101 insertions(+) create mode 100644 docs/spec/fastsync/verification/001bmc-apalache.csv create mode 100644 docs/spec/fastsync/verification/002tlc-tlc.csv create mode 100644 docs/spec/fastsync/verification/MC-CorrectBlocksInv.cfg create mode 100644 docs/spec/fastsync/verification/MC-CorrectNeverSuspectedInv.cfg create mode 100644 docs/spec/fastsync/verification/MC-Sync1AsInv.cfg create mode 100644 docs/spec/fastsync/verification/MC-Sync2AsInv.cfg create mode 100644 docs/spec/fastsync/verification/MC-Sync3AsInv.cfg create mode 100644 docs/spec/fastsync/verification/MC-SyncFromCorrectInv.cfg create mode 100644 docs/spec/fastsync/verification/MC-Termination.cfg create mode 100644 docs/spec/fastsync/verification/MC-Termination2.cfg create mode 100644 docs/spec/fastsync/verification/bfs.csv diff --git a/docs/spec/fastsync/verification/001bmc-apalache.csv b/docs/spec/fastsync/verification/001bmc-apalache.csv new file mode 100644 index 000000000..72901715c --- /dev/null +++ b/docs/spec/fastsync/verification/001bmc-apalache.csv @@ -0,0 +1,7 @@ +no,filename,tool,timeout,init,inv,next,args +1,MC_1_1_4.tla,apalache,2h,,Sync1AsInv,,--length=20 +2,MC_1_1_4.tla,apalache,2h,,Sync2AsInv,,--length=20 +3,MC_1_1_4.tla,apalache,2h,,Sync3AsInv,,--length=20 +6,MC_1_1_4.tla,apalache,2h,,CorrectBlocksInv,,--length=20 +7,MC_1_1_4.tla,apalache,2h,,SyncFromCorrectInv,,--length=20 +8,MC_1_1_4.tla,apalache,2h,,CorrectNeverSuspectedInv,,--length=20 diff --git a/docs/spec/fastsync/verification/002tlc-tlc.csv b/docs/spec/fastsync/verification/002tlc-tlc.csv new file mode 100644 index 000000000..ea20b3c00 --- /dev/null +++ b/docs/spec/fastsync/verification/002tlc-tlc.csv @@ -0,0 +1,9 @@ +no,filename,tool,timeout,init,inv,next,args +1,MC_1_1_4.tla,tlc,4h,,,,-workers 4 -config MC-Sync1AsInv.cfg +2,MC_1_1_4.tla,tlc,4h,,,,-workers 4 -config MC-Sync2AsInv.cfg +3,MC_1_1_4.tla,tlc,4h,,,,-workers 4 -config MC-Sync3AsInv.cfg +4,MC_1_1_4.tla,tlc,4h,,Termination,,-workers 4 -config MC-Termination.cfg +5,MC_1_1_4.tla,tlc,4h,,Termination2,,-workers 4 -config MC-Termination2.cfg +6,MC_1_1_4.tla,tlc,4h,,,,-workers 4 -config MC-CorrectBlocksInv.cfg +7,MC_1_1_4.tla,tlc,4h,,,,-workers 4 -config MC-SyncFromCorrectInv.cfg +8,MC_1_1_4.tla,tlc,4h,,,,-workers 4 -config MC-CorrectNeverSuspectedInv.cfg diff --git a/docs/spec/fastsync/verification/MC-CorrectBlocksInv.cfg b/docs/spec/fastsync/verification/MC-CorrectBlocksInv.cfg new file mode 100644 index 000000000..3e80ef165 --- /dev/null +++ b/docs/spec/fastsync/verification/MC-CorrectBlocksInv.cfg @@ -0,0 +1,10 @@ +\* INIT definition +INIT +Init +\* NEXT definition +NEXT +Next +\* INVARIANT definition +INVARIANT +CorrectBlocksInv +\* Generated on Wed May 27 18:45:18 CEST 2020 diff --git a/docs/spec/fastsync/verification/MC-CorrectNeverSuspectedInv.cfg b/docs/spec/fastsync/verification/MC-CorrectNeverSuspectedInv.cfg new file mode 100644 index 000000000..8a4606a86 --- /dev/null +++ b/docs/spec/fastsync/verification/MC-CorrectNeverSuspectedInv.cfg @@ -0,0 +1,10 @@ +\* INIT definition +INIT +Init +\* NEXT definition +NEXT +Next +\* INVARIANT definition +INVARIANT +CorrectNeverSuspectedInv +\* Generated on Wed May 27 18:45:18 CEST 2020 diff --git a/docs/spec/fastsync/verification/MC-Sync1AsInv.cfg b/docs/spec/fastsync/verification/MC-Sync1AsInv.cfg new file mode 100644 index 000000000..b557fb8b1 --- /dev/null +++ b/docs/spec/fastsync/verification/MC-Sync1AsInv.cfg @@ -0,0 +1,10 @@ +\* INIT definition +INIT +Init +\* NEXT definition +NEXT +Next +\* INVARIANT definition +INVARIANT +Sync1AsInv +\* Generated on Wed May 27 18:45:18 CEST 2020 diff --git a/docs/spec/fastsync/verification/MC-Sync2AsInv.cfg b/docs/spec/fastsync/verification/MC-Sync2AsInv.cfg new file mode 100644 index 000000000..3308dc805 --- /dev/null +++ b/docs/spec/fastsync/verification/MC-Sync2AsInv.cfg @@ -0,0 +1,10 @@ +\* INIT definition +INIT +Init +\* NEXT definition +NEXT +Next +\* INVARIANT definition +INVARIANT +Sync2AsInv +\* Generated on Wed May 27 18:45:18 CEST 2020 diff --git a/docs/spec/fastsync/verification/MC-Sync3AsInv.cfg b/docs/spec/fastsync/verification/MC-Sync3AsInv.cfg new file mode 100644 index 000000000..e2d3db6e4 --- /dev/null +++ b/docs/spec/fastsync/verification/MC-Sync3AsInv.cfg @@ -0,0 +1,10 @@ +\* INIT definition +INIT +Init +\* NEXT definition +NEXT +Next +\* INVARIANT definition +INVARIANT +Sync3AsInv +\* Generated on Wed May 27 18:45:18 CEST 2020 diff --git a/docs/spec/fastsync/verification/MC-SyncFromCorrectInv.cfg b/docs/spec/fastsync/verification/MC-SyncFromCorrectInv.cfg new file mode 100644 index 000000000..b17317633 --- /dev/null +++ b/docs/spec/fastsync/verification/MC-SyncFromCorrectInv.cfg @@ -0,0 +1,10 @@ +\* INIT definition +INIT +Init +\* NEXT definition +NEXT +Next +\* INVARIANT definition +INVARIANT +SyncFromCorrectInv +\* Generated on Wed May 27 18:45:18 CEST 2020 diff --git a/docs/spec/fastsync/verification/MC-Termination.cfg b/docs/spec/fastsync/verification/MC-Termination.cfg new file mode 100644 index 000000000..0d5705205 --- /dev/null +++ b/docs/spec/fastsync/verification/MC-Termination.cfg @@ -0,0 +1,10 @@ +\* INIT definition +INIT +Init +\* NEXT definition +NEXT +Next +\* INVARIANT definition +INVARIANT +Termination +\* Generated on Wed May 27 18:45:18 CEST 2020 diff --git a/docs/spec/fastsync/verification/MC-Termination2.cfg b/docs/spec/fastsync/verification/MC-Termination2.cfg new file mode 100644 index 000000000..33d83aaa5 --- /dev/null +++ b/docs/spec/fastsync/verification/MC-Termination2.cfg @@ -0,0 +1,10 @@ +\* INIT definition +INIT +Init +\* NEXT definition +NEXT +Next +\* INVARIANT definition +INVARIANT +Termination2 +\* Generated on Wed May 27 18:45:18 CEST 2020 diff --git a/docs/spec/fastsync/verification/bfs.csv b/docs/spec/fastsync/verification/bfs.csv new file mode 100644 index 000000000..fdd8b27a2 --- /dev/null +++ b/docs/spec/fastsync/verification/bfs.csv @@ -0,0 +1,5 @@ +step,total_sec,nanosec_adjustment +0,1,455000000 +1,4,823000000 +2,8,938000000 +3,13,694000000 From 5b4073b0fb5f47ee67fb4afef71924045568bbe2 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 28 May 2020 08:40:52 +0200 Subject: [PATCH 13/34] INVARIANT -> PROPERTY --- docs/spec/fastsync/verification/MC-Termination.cfg | 4 ++-- docs/spec/fastsync/verification/MC-Termination2.cfg | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/spec/fastsync/verification/MC-Termination.cfg b/docs/spec/fastsync/verification/MC-Termination.cfg index 0d5705205..00e8236e7 100644 --- a/docs/spec/fastsync/verification/MC-Termination.cfg +++ b/docs/spec/fastsync/verification/MC-Termination.cfg @@ -4,7 +4,7 @@ Init \* NEXT definition NEXT Next -\* INVARIANT definition -INVARIANT +\* PROPERTY definition +PROPERTY Termination \* Generated on Wed May 27 18:45:18 CEST 2020 diff --git a/docs/spec/fastsync/verification/MC-Termination2.cfg b/docs/spec/fastsync/verification/MC-Termination2.cfg index 33d83aaa5..7fee4c447 100644 --- a/docs/spec/fastsync/verification/MC-Termination2.cfg +++ b/docs/spec/fastsync/verification/MC-Termination2.cfg @@ -4,7 +4,7 @@ Init \* NEXT definition NEXT Next -\* INVARIANT definition -INVARIANT +\* PROPERTY definition +PROPERTY Termination2 \* Generated on Wed May 27 18:45:18 CEST 2020 From ec8be58250d43da597f4fe37d04d3fdcc78dd3ea Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 28 May 2020 08:43:16 +0200 Subject: [PATCH 14/34] increased apalache timeout --- docs/spec/fastsync/verification/001bmc-apalache.csv | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/docs/spec/fastsync/verification/001bmc-apalache.csv b/docs/spec/fastsync/verification/001bmc-apalache.csv index 72901715c..d3efff9e1 100644 --- a/docs/spec/fastsync/verification/001bmc-apalache.csv +++ b/docs/spec/fastsync/verification/001bmc-apalache.csv @@ -1,7 +1,7 @@ no,filename,tool,timeout,init,inv,next,args -1,MC_1_1_4.tla,apalache,2h,,Sync1AsInv,,--length=20 -2,MC_1_1_4.tla,apalache,2h,,Sync2AsInv,,--length=20 -3,MC_1_1_4.tla,apalache,2h,,Sync3AsInv,,--length=20 -6,MC_1_1_4.tla,apalache,2h,,CorrectBlocksInv,,--length=20 -7,MC_1_1_4.tla,apalache,2h,,SyncFromCorrectInv,,--length=20 -8,MC_1_1_4.tla,apalache,2h,,CorrectNeverSuspectedInv,,--length=20 +1,MC_1_1_4.tla,apalache,4h,,Sync1AsInv,,--length=20 +2,MC_1_1_4.tla,apalache,4h,,Sync2AsInv,,--length=20 +3,MC_1_1_4.tla,apalache,4h,,Sync3AsInv,,--length=20 +6,MC_1_1_4.tla,apalache,4h,,CorrectBlocksInv,,--length=20 +7,MC_1_1_4.tla,apalache,4h,,SyncFromCorrectInv,,--length=20 +8,MC_1_1_4.tla,apalache,4h,,CorrectNeverSuspectedInv,,--length=20 From cee09ed1670dfc255fc6e5e2f4d6d0c613cb005d Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 28 May 2020 14:47:27 +0200 Subject: [PATCH 15/34] doubled the timeouts for apalache and tlc --- .../fastsync/verification/001bmc-apalache.csv | 10 +++++----- docs/spec/fastsync/verification/002tlc-tlc.csv | 16 ++++++++-------- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/docs/spec/fastsync/verification/001bmc-apalache.csv b/docs/spec/fastsync/verification/001bmc-apalache.csv index d3efff9e1..a50c6f4c5 100644 --- a/docs/spec/fastsync/verification/001bmc-apalache.csv +++ b/docs/spec/fastsync/verification/001bmc-apalache.csv @@ -1,7 +1,7 @@ no,filename,tool,timeout,init,inv,next,args -1,MC_1_1_4.tla,apalache,4h,,Sync1AsInv,,--length=20 -2,MC_1_1_4.tla,apalache,4h,,Sync2AsInv,,--length=20 +1,MC_1_1_4.tla,apalache,1h,,Sync1AsInv,,--length=20 +2,MC_1_1_4.tla,apalache,1h,,Sync2AsInv,,--length=20 3,MC_1_1_4.tla,apalache,4h,,Sync3AsInv,,--length=20 -6,MC_1_1_4.tla,apalache,4h,,CorrectBlocksInv,,--length=20 -7,MC_1_1_4.tla,apalache,4h,,SyncFromCorrectInv,,--length=20 -8,MC_1_1_4.tla,apalache,4h,,CorrectNeverSuspectedInv,,--length=20 +6,MC_1_1_4.tla,apalache,8h,,CorrectBlocksInv,,--length=20 +7,MC_1_1_4.tla,apalache,1h,,SyncFromCorrectInv,,--length=20 +8,MC_1_1_4.tla,apalache,1h,,CorrectNeverSuspectedInv,,--length=20 diff --git a/docs/spec/fastsync/verification/002tlc-tlc.csv b/docs/spec/fastsync/verification/002tlc-tlc.csv index ea20b3c00..3245a97ed 100644 --- a/docs/spec/fastsync/verification/002tlc-tlc.csv +++ b/docs/spec/fastsync/verification/002tlc-tlc.csv @@ -1,9 +1,9 @@ no,filename,tool,timeout,init,inv,next,args -1,MC_1_1_4.tla,tlc,4h,,,,-workers 4 -config MC-Sync1AsInv.cfg -2,MC_1_1_4.tla,tlc,4h,,,,-workers 4 -config MC-Sync2AsInv.cfg -3,MC_1_1_4.tla,tlc,4h,,,,-workers 4 -config MC-Sync3AsInv.cfg -4,MC_1_1_4.tla,tlc,4h,,Termination,,-workers 4 -config MC-Termination.cfg -5,MC_1_1_4.tla,tlc,4h,,Termination2,,-workers 4 -config MC-Termination2.cfg -6,MC_1_1_4.tla,tlc,4h,,,,-workers 4 -config MC-CorrectBlocksInv.cfg -7,MC_1_1_4.tla,tlc,4h,,,,-workers 4 -config MC-SyncFromCorrectInv.cfg -8,MC_1_1_4.tla,tlc,4h,,,,-workers 4 -config MC-CorrectNeverSuspectedInv.cfg +1,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-Sync1AsInv.cfg +2,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-Sync2AsInv.cfg +3,MC_1_1_4.tla,tlc,8h,,,,-workers 4 -config MC-Sync3AsInv.cfg +4,MC_1_1_4.tla,tlc,8h,,Termination,,-workers 4 -config MC-Termination.cfg +5,MC_1_1_4.tla,tlc,8h,,Termination2,,-workers 4 -config MC-Termination2.cfg +6,MC_1_1_4.tla,tlc,8h,,,,-workers 4 -config MC-CorrectBlocksInv.cfg +7,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-SyncFromCorrectInv.cfg +8,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-CorrectNeverSuspectedInv.cfg From 204a2bd67d01140dabcad6c0d9276fc2e48bcdb9 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 28 May 2020 14:47:49 +0200 Subject: [PATCH 16/34] formatting --- docs/spec/fastsync/verification/fastsync_apalache.tla | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/docs/spec/fastsync/verification/fastsync_apalache.tla b/docs/spec/fastsync/verification/fastsync_apalache.tla index 972ba59a1..da1ca2e1e 100644 --- a/docs/spec/fastsync/verification/fastsync_apalache.tla +++ b/docs/spec/fastsync/verification/fastsync_apalache.tla @@ -748,9 +748,10 @@ Sync3AsInv == Termination == WF_turn(FlipTurn) => <>(state = "finished") \* This property holds true -Termination2 == (WF_turn(FlipTurn) - /\ <>[](inMsg.type \notin {"statusResponse", "addPeer", "removePeer"})) - => <>(state = "finished") +Termination2 == + (WF_turn(FlipTurn) + /\ <>[](inMsg.type \notin {"statusResponse", "addPeer", "removePeer"})) + => <>(state = "finished") \* a few simple properties that trigger counterexamples @@ -793,6 +794,6 @@ BlockPoolInvariant == \*============================================================================= \* Modification History -\* Last modified Wed May 27 19:15:23 CEST 2020 by igor +\* Last modified Thu May 28 10:55:04 CEST 2020 by igor \* Last modified Thu Apr 16 16:57:22 CEST 2020 by zarkomilosevic \* Created Tue Feb 04 10:36:18 CET 2020 by zarkomilosevic From b97d83b1703709ce16bdd9c96d591464862e0423 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 28 May 2020 23:21:16 +0200 Subject: [PATCH 17/34] new timeouts for the experiments --- docs/spec/fastsync/verification/001bmc-apalache.csv | 2 +- docs/spec/fastsync/verification/002tlc-tlc.csv | 8 ++++---- docs/spec/fastsync/verification/bfs.csv | 5 ----- 3 files changed, 5 insertions(+), 10 deletions(-) delete mode 100644 docs/spec/fastsync/verification/bfs.csv diff --git a/docs/spec/fastsync/verification/001bmc-apalache.csv b/docs/spec/fastsync/verification/001bmc-apalache.csv index a50c6f4c5..370cc4b96 100644 --- a/docs/spec/fastsync/verification/001bmc-apalache.csv +++ b/docs/spec/fastsync/verification/001bmc-apalache.csv @@ -2,6 +2,6 @@ no,filename,tool,timeout,init,inv,next,args 1,MC_1_1_4.tla,apalache,1h,,Sync1AsInv,,--length=20 2,MC_1_1_4.tla,apalache,1h,,Sync2AsInv,,--length=20 3,MC_1_1_4.tla,apalache,4h,,Sync3AsInv,,--length=20 -6,MC_1_1_4.tla,apalache,8h,,CorrectBlocksInv,,--length=20 +6,MC_1_1_4.tla,apalache,8h,,CorrectBlocksInv,,--length=16 7,MC_1_1_4.tla,apalache,1h,,SyncFromCorrectInv,,--length=20 8,MC_1_1_4.tla,apalache,1h,,CorrectNeverSuspectedInv,,--length=20 diff --git a/docs/spec/fastsync/verification/002tlc-tlc.csv b/docs/spec/fastsync/verification/002tlc-tlc.csv index 3245a97ed..f6deabff4 100644 --- a/docs/spec/fastsync/verification/002tlc-tlc.csv +++ b/docs/spec/fastsync/verification/002tlc-tlc.csv @@ -1,9 +1,9 @@ no,filename,tool,timeout,init,inv,next,args 1,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-Sync1AsInv.cfg 2,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-Sync2AsInv.cfg -3,MC_1_1_4.tla,tlc,8h,,,,-workers 4 -config MC-Sync3AsInv.cfg -4,MC_1_1_4.tla,tlc,8h,,Termination,,-workers 4 -config MC-Termination.cfg -5,MC_1_1_4.tla,tlc,8h,,Termination2,,-workers 4 -config MC-Termination2.cfg -6,MC_1_1_4.tla,tlc,8h,,,,-workers 4 -config MC-CorrectBlocksInv.cfg +3,MC_1_1_4.tla,tlc,3h,,,,-workers 4 -config MC-Sync3AsInv.cfg +4,MC_1_1_4.tla,tlc,2h,,Termination,,-workers 4 -config MC-Termination.cfg +5,MC_1_1_4.tla,tlc,3h,,Termination2,,-workers 4 -config MC-Termination2.cfg +6,MC_1_1_4.tla,tlc,3h,,,,-workers 4 -config MC-CorrectBlocksInv.cfg 7,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-SyncFromCorrectInv.cfg 8,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-CorrectNeverSuspectedInv.cfg diff --git a/docs/spec/fastsync/verification/bfs.csv b/docs/spec/fastsync/verification/bfs.csv deleted file mode 100644 index fdd8b27a2..000000000 --- a/docs/spec/fastsync/verification/bfs.csv +++ /dev/null @@ -1,5 +0,0 @@ -step,total_sec,nanosec_adjustment -0,1,455000000 -1,4,823000000 -2,8,938000000 -3,13,694000000 From 1993777613189ef54597ada7bc6998cccf87dba9 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 29 May 2020 11:15:00 +0200 Subject: [PATCH 18/34] fixed termination after the example by tlc --- docs/spec/fastsync/verification/002tlc-tlc.csv | 2 +- ...-Termination2.cfg => MC-TerminationByTO.cfg} | 2 +- .../fastsync/verification/fastsync_apalache.tla | 17 +++++++++-------- 3 files changed, 11 insertions(+), 10 deletions(-) rename docs/spec/fastsync/verification/{MC-Termination2.cfg => MC-TerminationByTO.cfg} (89%) diff --git a/docs/spec/fastsync/verification/002tlc-tlc.csv b/docs/spec/fastsync/verification/002tlc-tlc.csv index f6deabff4..740242d56 100644 --- a/docs/spec/fastsync/verification/002tlc-tlc.csv +++ b/docs/spec/fastsync/verification/002tlc-tlc.csv @@ -3,7 +3,7 @@ no,filename,tool,timeout,init,inv,next,args 2,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-Sync2AsInv.cfg 3,MC_1_1_4.tla,tlc,3h,,,,-workers 4 -config MC-Sync3AsInv.cfg 4,MC_1_1_4.tla,tlc,2h,,Termination,,-workers 4 -config MC-Termination.cfg -5,MC_1_1_4.tla,tlc,3h,,Termination2,,-workers 4 -config MC-Termination2.cfg +5,MC_1_1_4.tla,tlc,3h,,TerminationByTO,,-workers 4 -config MC-TerminationByTO.cfg 6,MC_1_1_4.tla,tlc,3h,,,,-workers 4 -config MC-CorrectBlocksInv.cfg 7,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-SyncFromCorrectInv.cfg 8,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-CorrectNeverSuspectedInv.cfg diff --git a/docs/spec/fastsync/verification/MC-Termination2.cfg b/docs/spec/fastsync/verification/MC-TerminationByTO.cfg similarity index 89% rename from docs/spec/fastsync/verification/MC-Termination2.cfg rename to docs/spec/fastsync/verification/MC-TerminationByTO.cfg index 7fee4c447..3a871ccf9 100644 --- a/docs/spec/fastsync/verification/MC-Termination2.cfg +++ b/docs/spec/fastsync/verification/MC-TerminationByTO.cfg @@ -6,5 +6,5 @@ NEXT Next \* PROPERTY definition PROPERTY -Termination2 +TerminationByTO \* Generated on Wed May 27 18:45:18 CEST 2020 diff --git a/docs/spec/fastsync/verification/fastsync_apalache.tla b/docs/spec/fastsync/verification/fastsync_apalache.tla index da1ca2e1e..fcc71f8c1 100644 --- a/docs/spec/fastsync/verification/fastsync_apalache.tla +++ b/docs/spec/fastsync/verification/fastsync_apalache.tla @@ -743,15 +743,16 @@ Sync3AsInv == \/ blockPool.syncedBlocks <= 0 \* timeout \/ (state = "finished" => blockPool.height >= blockPool.peerHeights[p] - 1) -\* TODO: align with the English spec. Add reference to it -\* This property is violated, as we do not track precisely timeouts +\* This property is violated, as the faulty peers may produce infinitely many responses Termination == WF_turn(FlipTurn) => <>(state = "finished") -\* This property holds true -Termination2 == - (WF_turn(FlipTurn) - /\ <>[](inMsg.type \notin {"statusResponse", "addPeer", "removePeer"})) - => <>(state = "finished") +\* The only provable termination is by timeout: +\* If eventually there is a timeout, then the protocol terminates +TerminationByTOPre == + WF_turn(FlipTurn) /\ <>(inMsg.type = "syncTimeout") + +TerminationByTO == + TerminationByTOPre => <>(state = "finished") \* a few simple properties that trigger counterexamples @@ -794,6 +795,6 @@ BlockPoolInvariant == \*============================================================================= \* Modification History -\* Last modified Thu May 28 10:55:04 CEST 2020 by igor +\* Last modified Fri May 29 11:13:29 CEST 2020 by igor \* Last modified Thu Apr 16 16:57:22 CEST 2020 by zarkomilosevic \* Created Tue Feb 04 10:36:18 CET 2020 by zarkomilosevic From 3dfa3e84d0a194eb1e1e0cdb42de8e48f0263c51 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 29 May 2020 19:23:34 +0200 Subject: [PATCH 19/34] comment on hash abstraction --- .../fastsync/verification/MC-TerminationCorr.cfg | 10 ++++++++++ docs/spec/fastsync/verification/Tinychain.tla | 12 ++++++++++++ 2 files changed, 22 insertions(+) create mode 100644 docs/spec/fastsync/verification/MC-TerminationCorr.cfg diff --git a/docs/spec/fastsync/verification/MC-TerminationCorr.cfg b/docs/spec/fastsync/verification/MC-TerminationCorr.cfg new file mode 100644 index 000000000..bea493637 --- /dev/null +++ b/docs/spec/fastsync/verification/MC-TerminationCorr.cfg @@ -0,0 +1,10 @@ +\* INIT definition +INIT +Init +\* NEXT definition +NEXT +Next +\* PROPERTY definition +PROPERTY +TerminationCorr +\* Generated on Wed May 27 18:45:18 CEST 2020 diff --git a/docs/spec/fastsync/verification/Tinychain.tla b/docs/spec/fastsync/verification/Tinychain.tla index 7a0b66ab4..b8a212996 100644 --- a/docs/spec/fastsync/verification/Tinychain.tla +++ b/docs/spec/fastsync/verification/Tinychain.tla @@ -81,7 +81,19 @@ PossibleCommit(block, commit) == /\ commit.committers = block.VS \* The block id in the commit matches the block hash (abstract comparison). \* (The implementation has extensive tests for that.) + \* this is an abstraction of: commit.blockId = hash(block) + \* + \* These are possible scenarios on the concrete hashes: + \* + \* scenario 1: commit.blockId = 10 /\ hash(block) = 10 /\ hash(ref) = 10 + \* scenario 2: commit.blockId = 20 /\ hash(block) = 20 /\ block.VS /= ref.VS + \* scenario 3: commit.blockId = 50 /\ hash(block) = 100 + \* scenario 4: commit.blockId = 10 /\ hash(block) = 100 + \* scenario 5: commit.blockId = 100 /\ hash(block) = 10 /\ commit.blockIdEqRef = block.hashEqRef + \* the following test would be cheating, as we do not have access to the + \* reference chain: + \* /\ commit.blockIdEqRef \* Basic invariants From dabf5706be2665a41ad8661f65f2ca7b4b536da9 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 29 May 2020 19:23:47 +0200 Subject: [PATCH 20/34] TerminationCorr --- .../spec/fastsync/verification/002tlc-tlc.csv | 1 + .../verification/fastsync_apalache.tla | 20 +++++++++++++++++-- 2 files changed, 19 insertions(+), 2 deletions(-) diff --git a/docs/spec/fastsync/verification/002tlc-tlc.csv b/docs/spec/fastsync/verification/002tlc-tlc.csv index 740242d56..9fb3a439d 100644 --- a/docs/spec/fastsync/verification/002tlc-tlc.csv +++ b/docs/spec/fastsync/verification/002tlc-tlc.csv @@ -4,6 +4,7 @@ no,filename,tool,timeout,init,inv,next,args 3,MC_1_1_4.tla,tlc,3h,,,,-workers 4 -config MC-Sync3AsInv.cfg 4,MC_1_1_4.tla,tlc,2h,,Termination,,-workers 4 -config MC-Termination.cfg 5,MC_1_1_4.tla,tlc,3h,,TerminationByTO,,-workers 4 -config MC-TerminationByTO.cfg +5,MC_1_1_4.tla,tlc,3h,,TerminationCorr,,-workers 4 -config MC-TerminationCorr.cfg 6,MC_1_1_4.tla,tlc,3h,,,,-workers 4 -config MC-CorrectBlocksInv.cfg 7,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-SyncFromCorrectInv.cfg 8,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-CorrectNeverSuspectedInv.cfg diff --git a/docs/spec/fastsync/verification/fastsync_apalache.tla b/docs/spec/fastsync/verification/fastsync_apalache.tla index fcc71f8c1..83eb61737 100644 --- a/docs/spec/fastsync/verification/fastsync_apalache.tla +++ b/docs/spec/fastsync/verification/fastsync_apalache.tla @@ -749,11 +749,27 @@ Termination == WF_turn(FlipTurn) => <>(state = "finished") \* The only provable termination is by timeout: \* If eventually there is a timeout, then the protocol terminates TerminationByTOPre == - WF_turn(FlipTurn) /\ <>(inMsg.type = "syncTimeout") + /\ WF_turn(FlipTurn) + /\ <>(inMsg.type = "syncTimeout" + /\ blockPool.height <= blockPool.syncHeight) TerminationByTO == TerminationByTOPre => <>(state = "finished") +\* The termination property when we only have correct peers +CorrBlockResponse == + \A h \in Heights: + [](outMsg.type = "blockRequest" /\ outMsg.height = h + => <>(inMsg.type = "blockResponse" /\ inMsg.block.height = h)) + +TerminationCorrPre == + /\ FAULTY = AsPidSet({}) + /\ WF_turn(FlipTurn) + /\ CorrBlockResponse + +TerminationCorr == + TerminationCorrPre => <>(state = "finished") + \* a few simple properties that trigger counterexamples \* Shows execution in which peer set is empty @@ -795,6 +811,6 @@ BlockPoolInvariant == \*============================================================================= \* Modification History -\* Last modified Fri May 29 11:13:29 CEST 2020 by igor +\* Last modified Fri May 29 19:18:37 CEST 2020 by igor \* Last modified Thu Apr 16 16:57:22 CEST 2020 by zarkomilosevic \* Created Tue Feb 04 10:36:18 CET 2020 by zarkomilosevic From 13b71708db24184dbc880f801a5f2d69ba844a6b Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 29 May 2020 20:42:35 +0200 Subject: [PATCH 21/34] added comments on the properties --- .../verification/fastsync_apalache.tla | 55 +++++++++++-------- 1 file changed, 31 insertions(+), 24 deletions(-) diff --git a/docs/spec/fastsync/verification/fastsync_apalache.tla b/docs/spec/fastsync/verification/fastsync_apalache.tla index 83eb61737..4737f48ec 100644 --- a/docs/spec/fastsync/verification/fastsync_apalache.tla +++ b/docs/spec/fastsync/verification/fastsync_apalache.tla @@ -712,7 +712,7 @@ TypeOK == blocksRequested |-> BR ] *) -\* TODO: align with the English spec. Add reference to it +(* Incorrect synchronization: The last block may be never received *) Sync1 == [](state = "finished" => blockPool.height >= MaxCorrectPeerHeight(blockPool)) @@ -720,7 +720,7 @@ Sync1 == Sync1AsInv == state = "finished" => blockPool.height >= MaxCorrectPeerHeight(blockPool) -\* TODO: align with the English spec. Add reference to it +(* Incorrect synchronization, as there may be a timeout *) Sync2 == \A p \in CORRECT: \/ p \notin blockPool.peerIds @@ -731,6 +731,7 @@ Sync2AsInv == \/ p \notin blockPool.peerIds \/ (state = "finished" => blockPool.height >= blockPool.peerHeights[p] - 1) +(* Correct synchronization *) Sync3 == \A p \in CORRECT: \/ p \notin blockPool.peerIds @@ -743,41 +744,43 @@ Sync3AsInv == \/ blockPool.syncedBlocks <= 0 \* timeout \/ (state = "finished" => blockPool.height >= blockPool.peerHeights[p] - 1) +(* Naive termination *) \* This property is violated, as the faulty peers may produce infinitely many responses -Termination == WF_turn(FlipTurn) => <>(state = "finished") +Termination == + WF_turn(FlipTurn) => <>(state = "finished") -\* The only provable termination is by timeout: -\* If eventually there is a timeout, then the protocol terminates +(* Termination by timeout: the protocol terminates, if there is a timeout *) +\* the precondition: fair flip turn and eventual timeout when no new blocks were synchronized TerminationByTOPre == /\ WF_turn(FlipTurn) - /\ <>(inMsg.type = "syncTimeout" - /\ blockPool.height <= blockPool.syncHeight) + /\ <>(inMsg.type = "syncTimeout" /\ blockPool.height <= blockPool.syncHeight) TerminationByTO == TerminationByTOPre => <>(state = "finished") -\* The termination property when we only have correct peers +(* The termination property when we only have correct peers *) +\* as correct peers may spam the node with addPeer, removePeer, and statusResponse, +\* we have to enforce eventual response (there are no queues in our spec) CorrBlockResponse == \A h \in Heights: [](outMsg.type = "blockRequest" /\ outMsg.height = h => <>(inMsg.type = "blockResponse" /\ inMsg.block.height = h)) +\* a precondition for termination in presence of only correct processes TerminationCorrPre == /\ FAULTY = AsPidSet({}) /\ WF_turn(FlipTurn) /\ CorrBlockResponse - + +\* termination when there are only correct processes TerminationCorr == TerminationCorrPre => <>(state = "finished") -\* a few simple properties that trigger counterexamples - -\* Shows execution in which peer set is empty -PeerSetIsNeverEmpty == blockPool.peerIds /= AsPidSet({}) - -\* Shows execution in which state = "finished" and MaxPeerHeight is not equal to 1 -StateNotFinished == - state /= "finished" \/ MaxPeerHeight(blockPool) = 1 +\* All synchronized blocks (but the last one) are exactly like in the reference chain +CorrectBlocksInv == + \/ state /= "finished" + \/ \A h \in 1..(blockPool.height - 1): + blockPool.blockStore[h] = chain[h] \* A false expectation that the protocol only finishes with the blocks \* from the processes that had not been suspected in being faulty @@ -786,12 +789,6 @@ SyncFromCorrectInv == \/ \A h \in 1..blockPool.height: blockPool.receivedBlocks[h] \in blockPool.peerIds \union {NilPeer} -\* All synchronized blocks are exactly like in the blockchain -CorrectBlocksInv == - \/ state /= "finished" - \/ \A h \in 1..(blockPool.height - 1): - blockPool.blockStore[h] = chain[h] - \* A false expectation that a correct process is never removed from the set of peer ids. \* A correct process may reply too late and then gets evicted. CorrectNeverSuspectedInv == @@ -807,10 +804,20 @@ BlockPoolInvariant == /\ blockPool.blockStore[h] /= NilBlock /\ blockPool.pendingBlocks[h] = NilPeer +(* a few simple properties that trigger counterexamples *) + +\* Shows execution in which peer set is empty +PeerSetIsNeverEmpty == blockPool.peerIds /= AsPidSet({}) + +\* Shows execution in which state = "finished" and MaxPeerHeight is not equal to 1 +StateNotFinished == + state /= "finished" \/ MaxPeerHeight(blockPool) = 1 + + ============================================================================= \*============================================================================= \* Modification History -\* Last modified Fri May 29 19:18:37 CEST 2020 by igor +\* Last modified Fri May 29 20:41:53 CEST 2020 by igor \* Last modified Thu Apr 16 16:57:22 CEST 2020 by zarkomilosevic \* Created Tue Feb 04 10:36:18 CET 2020 by zarkomilosevic From dc0ab21dc38d1edb187dee855b8458374c4fad0f Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Sat, 30 May 2020 10:32:42 +0200 Subject: [PATCH 22/34] increase tlc timeout to 12 hrs --- docs/spec/fastsync/verification/002tlc-tlc.csv | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/docs/spec/fastsync/verification/002tlc-tlc.csv b/docs/spec/fastsync/verification/002tlc-tlc.csv index 9fb3a439d..20691e7ee 100644 --- a/docs/spec/fastsync/verification/002tlc-tlc.csv +++ b/docs/spec/fastsync/verification/002tlc-tlc.csv @@ -1,10 +1,9 @@ no,filename,tool,timeout,init,inv,next,args 1,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-Sync1AsInv.cfg 2,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-Sync2AsInv.cfg -3,MC_1_1_4.tla,tlc,3h,,,,-workers 4 -config MC-Sync3AsInv.cfg +3,MC_1_1_4.tla,tlc,12h,,,,-workers 4 -config MC-Sync3AsInv.cfg 4,MC_1_1_4.tla,tlc,2h,,Termination,,-workers 4 -config MC-Termination.cfg -5,MC_1_1_4.tla,tlc,3h,,TerminationByTO,,-workers 4 -config MC-TerminationByTO.cfg -5,MC_1_1_4.tla,tlc,3h,,TerminationCorr,,-workers 4 -config MC-TerminationCorr.cfg -6,MC_1_1_4.tla,tlc,3h,,,,-workers 4 -config MC-CorrectBlocksInv.cfg +5,MC_1_1_4.tla,tlc,12h,,TerminationByTO,,-workers 4 -config MC-TerminationByTO.cfg +6,MC_1_1_4.tla,tlc,12h,,,,-workers 4 -config MC-CorrectBlocksInv.cfg 7,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-SyncFromCorrectInv.cfg 8,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-CorrectNeverSuspectedInv.cfg From 28484cea3860442dbe4b5638199a79d066878e6a Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 1 Jun 2020 11:31:16 +0200 Subject: [PATCH 23/34] increased tlc timeout to 24h --- docs/spec/fastsync/verification/002tlc-tlc.csv | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/spec/fastsync/verification/002tlc-tlc.csv b/docs/spec/fastsync/verification/002tlc-tlc.csv index 20691e7ee..2e5429d48 100644 --- a/docs/spec/fastsync/verification/002tlc-tlc.csv +++ b/docs/spec/fastsync/verification/002tlc-tlc.csv @@ -1,9 +1,9 @@ no,filename,tool,timeout,init,inv,next,args 1,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-Sync1AsInv.cfg 2,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-Sync2AsInv.cfg -3,MC_1_1_4.tla,tlc,12h,,,,-workers 4 -config MC-Sync3AsInv.cfg +3,MC_1_1_4.tla,tlc,24h,,,,-workers 4 -config MC-Sync3AsInv.cfg 4,MC_1_1_4.tla,tlc,2h,,Termination,,-workers 4 -config MC-Termination.cfg -5,MC_1_1_4.tla,tlc,12h,,TerminationByTO,,-workers 4 -config MC-TerminationByTO.cfg -6,MC_1_1_4.tla,tlc,12h,,,,-workers 4 -config MC-CorrectBlocksInv.cfg +5,MC_1_1_4.tla,tlc,24h,,TerminationByTO,,-workers 4 -config MC-TerminationByTO.cfg +6,MC_1_1_4.tla,tlc,24h,,,,-workers 4 -config MC-CorrectBlocksInv.cfg 7,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-SyncFromCorrectInv.cfg 8,MC_1_1_4.tla,tlc,1h,,,,-workers 4 -config MC-CorrectNeverSuspectedInv.cfg From 4310960fd20d209d7c4de1cfbae5569b44ac0849 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 20 Jul 2020 14:43:30 +0200 Subject: [PATCH 24/34] simplifying block execution + comments --- .../verification/fastsync_apalache.tla | 47 ++++++++++--------- 1 file changed, 26 insertions(+), 21 deletions(-) diff --git a/docs/spec/fastsync/verification/fastsync_apalache.tla b/docs/spec/fastsync/verification/fastsync_apalache.tla index 4737f48ec..74fdd73dd 100644 --- a/docs/spec/fastsync/verification/fastsync_apalache.tla +++ b/docs/spec/fastsync/verification/fastsync_apalache.tla @@ -105,7 +105,7 @@ NilBlock == lastCommit |-> NilCommit, VS |-> NIL_VS, NextVS |-> NIL_VS] \* a special value for an undefined peer -NilPeer == "Nil" \* we have changed it to STRING for apalache efficiency +NilPeer == "Nil" \* STRING for apalache efficiency \* control the state of the syncing node States == { "running", "finished"} @@ -151,9 +151,12 @@ VARIABLES (* the variables of the node *) nvars == <> -(* Type definitions for Apalache *) -PIDT == STRING \* type of process ids -AsPidSet(a) == a <: {PIDT} +(*************** Type definitions for Apalache (model checker) **********************) +AsIntSet(S) == S <: {Int} + +\* type of process ids +PIDT == STRING +AsPidSet(S) == S <: {PIDT} \* ControlMessage type CMT == [type |-> STRING, peerId |-> PIDT] \* type of control messages @@ -168,12 +171,15 @@ OMT == [type |-> STRING, peerId |-> PIDT, height |-> Int] AsOutMsg(m) == m <: OMT AsOutMsgSet(S) == S <: {OMT} +\* block pool type BPT == [height |-> Int, peerIds |-> {PIDT}, peerHeights |-> [PIDT -> Int], blockStore |-> [Int -> BT], receivedBlocks |-> [Int -> PIDT], pendingBlocks |-> [Int -> PIDT], syncedBlocks |-> Int, syncHeight |-> Int] AsBlockPool(bp) == bp <: BPT +(******************** Sets of messages ********************************) + \* Control messages ControlMsgs == AsInMsgSet([type: {"addPeer"}, peerId: AllPeerIds]) @@ -319,7 +325,7 @@ FindNextRequestHeight(bPool) == /\ i <= MaxPeerHeight(bPool) /\ bPool.blockStore[i] = NilBlock /\ bPool.pendingBlocks[i] = NilPeer} IN - IF S = {} <: {Int} + IF S = AsIntSet({}) THEN NilHeight ELSE CHOOSE min \in S: \A h \in S: h >= min @@ -349,7 +355,7 @@ FindPeerToServe(bPool, h) == \/ bPool.blockStore[i] /= NilBlock } IN - IF \/ peersThatCanServe = {} <: {PIDT} + IF \/ peersThatCanServe = AsPidSet({}) \/ Cardinality(pendingBlocks) >= TARGET_PENDING THEN NilPeer \* pick a peer that can serve request for height h that has minimum number of pending requests @@ -399,14 +405,24 @@ ExecuteBlocks(bPool) == IF block1 = NilBlock \/ block2 = NilBlock THEN bPool \* we don't have two next consecutive blocks - ELSE IF ~IsMatchingValidators(block1, block0.NextVS) \* the implementation stores NextVS in its state, not using block0 - \/ ~VerifyCommit(block0, block1.lastCommit) \* WE NEED THIS AT LEAST FOR THE TRUSTED BLOCK + + ELSE IF ~IsMatchingValidators(block1, block0.NextVS) + \* Check that block1.VS = block0.Next. + \* Otherwise, CorrectBlocksInv fails. + \* In the implementation NextVS is part of the application state, + \* so a mismatch can be found without access to block0.NextVS. + \*\/ ~VerifyCommit(block0, block1.lastCommit) + \* Verify commit of block1 based on block0. If we omit this check, + \* the property XXX breaks. THEN \* the block does not have the expected validator set RemovePeers({bPool.receivedBlocks[bPool.height]}, bPool) ELSE IF ~VerifyCommit(block1, block2.lastCommit) + \* Verify commit of block2 based on block1. \*\/ ~IsMatchingValidators(block2, block1.NextVS) \* we need this check too THEN \* remove the peers of block1 and block2, as they are considered faulty - RemovePeers({bPool.receivedBlocks[bPool.height], bPool.receivedBlocks[bPool.height + 1]}, bPool) + RemovePeers({bPool.receivedBlocks[bPool.height], + bPool.receivedBlocks[bPool.height + 1]}, + bPool) ELSE \* all good, execute block at position height [bPool EXCEPT !.height = bPool.height + 1] @@ -629,13 +645,13 @@ NextEnvStep(pState) == \/ SendResponseMessage(pState) \/ GrowPeerHeight(pState) \/ SendControlMessage /\ peersState' = pState + \* note that we propagate pState that was missing in the previous version \* Peers consume a message and update it's local state. It then makes a single step, i.e., it sends at most single message. \* Message sent could be either a response to a request or faulty message (sent by faulty processes). NextPeers == LET pState == HandleRequest(outMsg, peersState) IN - /\ outMsg' = AsOutMsg(NoMsg) /\ NextEnvStep(pState) @@ -668,7 +684,6 @@ FlipTurn == ELSE "Peers" - \* Compute max peer height. Used as a helper operator in properties. MaxCorrectPeerHeight(bPool) == LET correctPeers == {p \in bPool.peerIds: p \in CORRECT} IN @@ -702,16 +717,6 @@ TypeOK == syncHeight: Heights ] - (* - \* the constraints that would be better handled by apalache? - /\ \E PH \in [AllPeerIds -> Heights \union {NilHeight}]: - \E BR \in SUBSET [type: {"blockRequest"}, peerId: AllPeerIds, height: Heights]: - \E sr \in BOOLEAN: - peersState = [ peerHeights |-> PH, - statusRequested |-> sr, - blocksRequested |-> BR ] - *) - (* Incorrect synchronization: The last block may be never received *) Sync1 == [](state = "finished" => From b471edd57547030b8bcd4e9f6d527b6410e744cf Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 20 Jul 2020 20:40:25 +0200 Subject: [PATCH 25/34] the experiments with 2 faulty processes --- docs/spec/fastsync/verification/001bmc-apalache.csv | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/docs/spec/fastsync/verification/001bmc-apalache.csv b/docs/spec/fastsync/verification/001bmc-apalache.csv index 370cc4b96..e83c4c96f 100644 --- a/docs/spec/fastsync/verification/001bmc-apalache.csv +++ b/docs/spec/fastsync/verification/001bmc-apalache.csv @@ -2,6 +2,12 @@ no,filename,tool,timeout,init,inv,next,args 1,MC_1_1_4.tla,apalache,1h,,Sync1AsInv,,--length=20 2,MC_1_1_4.tla,apalache,1h,,Sync2AsInv,,--length=20 3,MC_1_1_4.tla,apalache,4h,,Sync3AsInv,,--length=20 -6,MC_1_1_4.tla,apalache,8h,,CorrectBlocksInv,,--length=16 -7,MC_1_1_4.tla,apalache,1h,,SyncFromCorrectInv,,--length=20 -8,MC_1_1_4.tla,apalache,1h,,CorrectNeverSuspectedInv,,--length=20 +4,MC_1_1_4.tla,apalache,8h,,CorrectBlocksInv,,--length=16 +5,MC_1_1_4.tla,apalache,1h,,SyncFromCorrectInv,,--length=20 +6,MC_1_1_4.tla,apalache,1h,,CorrectNeverSuspectedInv,,--length=20 +7,MC_1_2_4.tla,apalache,1h,,Sync1AsInv,,--length=20 +8,MC_1_2_4.tla,apalache,1h,,Sync2AsInv,,--length=20 +9,MC_1_2_4.tla,apalache,4h,,Sync3AsInv,,--length=20 +10,MC_1_2_4.tla,apalache,8h,,CorrectBlocksInv,,--length=16 +11,MC_1_2_4.tla,apalache,1h,,SyncFromCorrectInv,,--length=20 +12,MC_1_2_4.tla,apalache,1h,,CorrectNeverSuspectedInv,,--length=20 From 420bef45c3a3f82505a312a048a10dcc626e6848 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 20 Jul 2020 20:40:58 +0200 Subject: [PATCH 26/34] a model for 2 faulty processes --- docs/spec/fastsync/verification/MC_1_2_4.tla | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 docs/spec/fastsync/verification/MC_1_2_4.tla diff --git a/docs/spec/fastsync/verification/MC_1_2_4.tla b/docs/spec/fastsync/verification/MC_1_2_4.tla new file mode 100644 index 000000000..8e9dc2cc9 --- /dev/null +++ b/docs/spec/fastsync/verification/MC_1_2_4.tla @@ -0,0 +1,15 @@ +-------------------------- MODULE MC_1_2_4 ------------------------------------ + +VALIDATOR_SETS == {"vs1", "vs2"} +NIL_VS == "NilVS" +CORRECT == {"c1"} +FAULTY == {"f2", "f3"} +MAX_HEIGHT == 4 +PEER_MAX_REQUESTS == 2 +TARGET_PENDING == 3 + +VARIABLES + state, blockPool, peersState, chain, turn, inMsg, outMsg + +INSTANCE fastsync_apalache +=============================================================================== From 6a064b1a3deea15b03537cd7e6227e139e9f7098 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Tue, 21 Jul 2020 13:57:03 +0200 Subject: [PATCH 27/34] cleaning up the spec a bit --- .../fastsync/verification/fastsync_apalache.tla | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/docs/spec/fastsync/verification/fastsync_apalache.tla b/docs/spec/fastsync/verification/fastsync_apalache.tla index 74fdd73dd..51dd54e57 100644 --- a/docs/spec/fastsync/verification/fastsync_apalache.tla +++ b/docs/spec/fastsync/verification/fastsync_apalache.tla @@ -52,7 +52,7 @@ We assume that fast sync protocol starts when connections with some number of pe are established. Therefore, peer set is initialised with non-empty set of peer ids. Note however that node does not know initially the peer heights. *) - + EXTENDS Integers, FiniteSets, Sequences @@ -74,9 +74,6 @@ VARIABLE chain \* introduce tiny chain as the source of blocks for the correct nodes INSTANCE Tinychain -\* simplifies execute blocks logic. Used only in block store. -HeightsPlus == 1..MAX_HEIGHT+1 - \* a special value for an undefined height NilHeight == 0 @@ -95,8 +92,6 @@ CorrectLastCommit(h) == chain[h].lastCommit NilCommit == [blockIdEqRef |-> FALSE, committers |-> NIL_VS] -\*BlocksWithNil == [height: Heights, lastCommit: LastCommits, wellFormed: BOOLEAN] - \* correct node always supplies the blocks from the blockchain CorrectBlock(h) == chain[h] @@ -400,8 +395,10 @@ VerifyCommit(block, lastCommit) == ExecuteBlocks(bPool) == LET bStore == bPool.blockStore IN LET block0 == bStore[bPool.height - 1] IN + \* blockPool is initialized with height = TrustedHeight + 1, + \* so bStore[bPool.height - 1] is well defined LET block1 == bStore[bPool.height] IN - LET block2 == bStore[bPool.height+1] IN + LET block2 == bStore[bPool.height + 1] IN IF block1 = NilBlock \/ block2 = NilBlock THEN bPool \* we don't have two next consecutive blocks @@ -411,14 +408,11 @@ ExecuteBlocks(bPool) == \* Otherwise, CorrectBlocksInv fails. \* In the implementation NextVS is part of the application state, \* so a mismatch can be found without access to block0.NextVS. - \*\/ ~VerifyCommit(block0, block1.lastCommit) - \* Verify commit of block1 based on block0. If we omit this check, - \* the property XXX breaks. THEN \* the block does not have the expected validator set RemovePeers({bPool.receivedBlocks[bPool.height]}, bPool) ELSE IF ~VerifyCommit(block1, block2.lastCommit) \* Verify commit of block2 based on block1. - \*\/ ~IsMatchingValidators(block2, block1.NextVS) \* we need this check too + \* Interestingly, we do not have to call IsMatchingValidators. THEN \* remove the peers of block1 and block2, as they are considered faulty RemovePeers({bPool.receivedBlocks[bPool.height], bPool.receivedBlocks[bPool.height + 1]}, From bf535f8e5f0a45dd9eeee0a95ba730c9fc745626 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Tue, 21 Jul 2020 13:59:30 +0200 Subject: [PATCH 28/34] updates from verification/fastsync_apalache.tla after model checking --- docs/spec/fastsync/fastsync.tla | 378 +++++++++++++++++++++----------- 1 file changed, 254 insertions(+), 124 deletions(-) diff --git a/docs/spec/fastsync/fastsync.tla b/docs/spec/fastsync/fastsync.tla index 28268e9e6..51dd54e57 100644 --- a/docs/spec/fastsync/fastsync.tla +++ b/docs/spec/fastsync/fastsync.tla @@ -1,4 +1,4 @@ ------------------------------ MODULE fastsync ----------------------------- +----------------------------- MODULE fastsync_apalache ----------------------------- (* In this document we give the high level specification of the fast sync protocol as implemented here: @@ -52,10 +52,13 @@ We assume that fast sync protocol starts when connections with some number of pe are established. Therefore, peer set is initialised with non-empty set of peer ids. Note however that node does not know initially the peer heights. *) - + EXTENDS Integers, FiniteSets, Sequences -CONSTANTS MAX_HEIGHT, + +CONSTANTS MAX_HEIGHT, \* the maximal height of blockchain + VALIDATOR_SETS, \* abstract set of validators + NIL_VS, \* a nil validator set CORRECT, \* set of correct peers FAULTY, \* set of faulty peers TARGET_PENDING, \* maximum number of pending requests + downloaded blocks that are not yet processed @@ -65,43 +68,39 @@ ASSUME CORRECT \intersect FAULTY = {} ASSUME TARGET_PENDING > 0 ASSUME PEER_MAX_REQUESTS > 0 - -\* the set of potential heights -Heights == 1..MAX_HEIGHT - -\* simplifies execute blocks logic. Used only in block store. -HeightsPlus == 1..MAX_HEIGHT+1 +\* the blockchain, see Tinychain +VARIABLE chain + +\* introduce tiny chain as the source of blocks for the correct nodes +INSTANCE Tinychain \* a special value for an undefined height NilHeight == 0 +\* the height of the genesis block +TrustedHeight == 1 + \* the set of all peer ids the node can receive a message from AllPeerIds == CORRECT \union FAULTY -\* the set of potential blocks ids. For simplification, correct blocks are equal to block height. -BlockIds == Heights \union {NilHeight} - -LastCommits == [blockId: BlockIds, enoughVotingPower: BOOLEAN] - \* Correct last commit have enough voting power, i.e., +2/3 of the voting power of \* the corresponding validator set (enoughVotingPower = TRUE) that signs blockId. \* BlockId defines correct previous block (in the implementation it is the hash of the block). -\* For simplicity, we model blockId as the height of the previous block. -CorrectLastCommit(h) == [blockId |-> h-1, enoughVotingPower |-> TRUE] - -NilCommit == [blockId |-> 0, enoughVotingPower |-> TRUE] +\* Instead of blockId, we encode blockIdEqRef, which is true, if the block id is equal +\* to the hash of the previous block, see Tinychain. +CorrectLastCommit(h) == chain[h].lastCommit -Blocks == [height: Heights, lastCommit: LastCommits, wellFormed: BOOLEAN] +NilCommit == [blockIdEqRef |-> FALSE, committers |-> NIL_VS] -\*BlocksWithNil == [height: Heights, lastCommit: LastCommits, wellFormed: BOOLEAN] +\* correct node always supplies the blocks from the blockchain +CorrectBlock(h) == chain[h] -\* correct node will create always valid blocks, i.e., wellFormed = true and lastCommit is correct. -CorrectBlock(h) == [height |-> h, lastCommit |-> CorrectLastCommit(h), wellFormed |-> TRUE] - -NilBlock == [height |-> 0, lastCommit |-> NilCommit, wellFormed |-> TRUE] +NilBlock == + [height |-> 0, hashEqRef |-> FALSE, wellFormed |-> FALSE, + lastCommit |-> NilCommit, VS |-> NIL_VS, NextVS |-> NIL_VS] \* a special value for an undefined peer -NilPeer == 0 +NilPeer == "Nil" \* STRING for apalache efficiency \* control the state of the syncing node States == { "running", "finished"} @@ -136,10 +135,9 @@ VARIABLES ] *) peersState - \* the variables for the network and scheduler - VARIABLES +VARIABLES turn, \* who is taking the turn: "Peers" or "Node" inMsg, \* a node receives message by this variable outMsg \* a node sends a message by this variable @@ -148,49 +146,82 @@ VARIABLES (* the variables of the node *) nvars == <> +(*************** Type definitions for Apalache (model checker) **********************) +AsIntSet(S) == S <: {Int} + +\* type of process ids +PIDT == STRING +AsPidSet(S) == S <: {PIDT} + +\* ControlMessage type +CMT == [type |-> STRING, peerId |-> PIDT] \* type of control messages + +\* InMsg type +IMT == [type |-> STRING, peerId |-> PIDT, height |-> Int, block |-> BT] +AsInMsg(m) == m <: IMT +AsInMsgSet(S) == S <: {IMT} + +\* OutMsg type +OMT == [type |-> STRING, peerId |-> PIDT, height |-> Int] +AsOutMsg(m) == m <: OMT +AsOutMsgSet(S) == S <: {OMT} + +\* block pool type +BPT == [height |-> Int, peerIds |-> {PIDT}, peerHeights |-> [PIDT -> Int], + blockStore |-> [Int -> BT], receivedBlocks |-> [Int -> PIDT], + pendingBlocks |-> [Int -> PIDT], syncedBlocks |-> Int, syncHeight |-> Int] + +AsBlockPool(bp) == bp <: BPT + +(******************** Sets of messages ********************************) + \* Control messages ControlMsgs == - [type: {"addPeer"}, peerId: AllPeerIds] + AsInMsgSet([type: {"addPeer"}, peerId: AllPeerIds]) \union - [type: {"removePeer"}, peerId: AllPeerIds] + AsInMsgSet([type: {"removePeer"}, peerId: AllPeerIds]) \union - [type: {"syncTimeout"}] + AsInMsgSet([type: {"syncTimeout"}]) \* All messages (and events) received by a node InMsgs == - {NoMsg} + AsInMsgSet({NoMsg}) \union - [type: {"blockResponse"}, peerId: AllPeerIds, block: Blocks] + AsInMsgSet([type: {"blockResponse"}, peerId: AllPeerIds, block: Blocks]) \union - [type: {"noBlockResponse"}, peerId: AllPeerIds, height: Heights] + AsInMsgSet([type: {"noBlockResponse"}, peerId: AllPeerIds, height: Heights]) \union - [type: {"statusResponse"}, peerId: AllPeerIds, height: Heights] + AsInMsgSet([type: {"statusResponse"}, peerId: AllPeerIds, height: Heights]) \union ControlMsgs \* Messages sent by a node and received by peers (environment in our case) OutMsgs == - {NoMsg} + AsOutMsgSet({NoMsg}) \union - [type: {"statusRequest"}] \* StatusRequest is broadcast to the set of connected peers. + AsOutMsgSet([type: {"statusRequest"}]) \* StatusRequest is broadcast to the set of connected peers. \union - [type: {"blockRequest"}, peerId: AllPeerIds, height: Heights] + AsOutMsgSet([type: {"blockRequest"}, peerId: AllPeerIds, height: Heights]) (********************************** NODE ***********************************) InitNode == - \E pIds \in SUBSET AllPeerIds \ {{}}: \* set of peers node established initial connections with - /\ blockPool = [ - height |-> 1, + \E pIds \in SUBSET AllPeerIds: \* set of peers node established initial connections with + /\ pIds \subseteq CORRECT + /\ pIds /= AsPidSet({}) \* apalache better checks non-emptiness than subtracts from SUBSET + /\ blockPool = AsBlockPool([ + height |-> TrustedHeight + 1, \* the genesis block is at height 1 + syncHeight |-> TrustedHeight + 1, \* and we are synchronized to it peerIds |-> pIds, peerHeights |-> [p \in AllPeerIds |-> NilHeight], \* no peer height is known - blockStore |-> [h \in Heights |-> NilBlock], + blockStore |-> + [h \in Heights |-> + IF h > TrustedHeight THEN NilBlock ELSE chain[1]], receivedBlocks |-> [h \in Heights |-> NilPeer], pendingBlocks |-> [h \in Heights |-> NilPeer], - syncedBlocks |-> -1, - syncHeight |-> 1 - ] + syncedBlocks |-> -1 + ]) /\ state = "running" \* Remove faulty peers. @@ -275,7 +306,7 @@ HandleBlockResponse(msg, bPool) == \* Compute max peer height. \* See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L440 MaxPeerHeight(bPool) == - IF bPool.peerIds = {} + IF bPool.peerIds = AsPidSet({}) THEN 0 \* no peers, just return 0 ELSE LET Hts == {bPool.peerHeights[p] : p \in bPool.peerIds} IN CHOOSE max \in Hts: \A h \in Hts: h <= max @@ -289,7 +320,7 @@ FindNextRequestHeight(bPool) == /\ i <= MaxPeerHeight(bPool) /\ bPool.blockStore[i] = NilBlock /\ bPool.pendingBlocks[i] = NilPeer} IN - IF S = {} + IF S = AsIntSet({}) THEN NilHeight ELSE CHOOSE min \in S: \A h \in S: h >= min @@ -319,7 +350,7 @@ FindPeerToServe(bPool, h) == \/ bPool.blockStore[i] /= NilBlock } IN - IF \/ peersThatCanServe = {} + IF \/ peersThatCanServe = AsPidSet({}) \/ Cardinality(pendingBlocks) >= TARGET_PENDING THEN NilPeer \* pick a peer that can serve request for height h that has minimum number of pending requests @@ -331,10 +362,10 @@ FindPeerToServe(bPool, h) == CreateRequest(bPool) == LET nextHeight == FindNextRequestHeight(bPool) IN - IF nextHeight = NilHeight THEN [msg |-> NoMsg, pool |-> bPool] + IF nextHeight = NilHeight THEN [msg |-> AsOutMsg(NoMsg), pool |-> bPool] ELSE LET peer == FindPeerToServe(bPool, nextHeight) IN - IF peer = NilPeer THEN [msg |-> NoMsg, pool |-> bPool] + IF peer = NilPeer THEN [msg |-> AsOutMsg(NoMsg), pool |-> bPool] ELSE LET m == [type |-> "blockRequest", peerId |-> peer, height |-> nextHeight] IN LET newPool == [bPool EXCEPT @@ -356,24 +387,38 @@ ComputeNextState(bPool) == (* Verify if commit is for the given block id and if commit has enough voting power. See https://github.com/tendermint/tendermint/blob/61057a8b0af2beadee106e47c4616b279e83c920/blockchain/v2/processor_context.go#L12 *) VerifyCommit(block, lastCommit) == - /\ lastCommit.enoughVotingPower - /\ lastCommit.blockId = block.height - + PossibleCommit(block, lastCommit) (* Tries to execute next block in the pool, i.e., defines block validation logic. Returns new block pool (peers that has send invalid blocks are removed). See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/processor.go#L135 *) ExecuteBlocks(bPool) == LET bStore == bPool.blockStore IN + LET block0 == bStore[bPool.height - 1] IN + \* blockPool is initialized with height = TrustedHeight + 1, + \* so bStore[bPool.height - 1] is well defined LET block1 == bStore[bPool.height] IN - LET block2 == bStore[bPool.height+1] IN - - IF block1 = NilBlock \/ block2 = NilBlock \* we don't have two next consecutive blocks - THEN bPool - ELSE IF bPool.height > 1 /\ ~VerifyCommit(block1, block2.lastCommit) - THEN RemovePeers({bPool.receivedBlocks[block1.height], bPool.receivedBlocks[block2.height]}, bPool) - ELSE \* all good, execute block at position height - [bPool EXCEPT !.height = bPool.height + 1] + LET block2 == bStore[bPool.height + 1] IN + + IF block1 = NilBlock \/ block2 = NilBlock + THEN bPool \* we don't have two next consecutive blocks + + ELSE IF ~IsMatchingValidators(block1, block0.NextVS) + \* Check that block1.VS = block0.Next. + \* Otherwise, CorrectBlocksInv fails. + \* In the implementation NextVS is part of the application state, + \* so a mismatch can be found without access to block0.NextVS. + THEN \* the block does not have the expected validator set + RemovePeers({bPool.receivedBlocks[bPool.height]}, bPool) + ELSE IF ~VerifyCommit(block1, block2.lastCommit) + \* Verify commit of block2 based on block1. + \* Interestingly, we do not have to call IsMatchingValidators. + THEN \* remove the peers of block1 and block2, as they are considered faulty + RemovePeers({bPool.receivedBlocks[bPool.height], + bPool.receivedBlocks[bPool.height + 1]}, + bPool) + ELSE \* all good, execute block at position height + [bPool EXCEPT !.height = bPool.height + 1] \* Defines logic for pruning peers. @@ -454,7 +499,7 @@ NodeStep == /\ state' = nstate /\ blockPool' = msgAndPool.pool /\ outMsg' = msgAndPool.msg - /\ inMsg' = NoMsg + /\ inMsg' = AsInMsg(NoMsg) \* If node is running, then in every step we try to create blockRequest. @@ -474,7 +519,7 @@ InitPeers == peersState = [ peerHeights |-> pHeights, statusRequested |-> FALSE, - blocksRequested |-> {} + blocksRequested |-> AsOutMsgSet({}) ] HandleStatusRequest(msg, pState) == @@ -484,11 +529,11 @@ HandleStatusRequest(msg, pState) == HandleBlockRequest(msg, pState) == [pState EXCEPT - !.blocksRequested = pState.blocksRequested \union {msg} + !.blocksRequested = pState.blocksRequested \union AsOutMsgSet({msg}) ] HandleRequest(msg, pState) == - IF msg = NoMsg + IF msg = AsOutMsg(NoMsg) THEN pState ELSE IF msg.type = "statusRequest" THEN HandleStatusRequest(msg, pState) @@ -497,28 +542,27 @@ HandleRequest(msg, pState) == CreateStatusResponse(peer, pState, anyHeight) == LET m == IF peer \in CORRECT - THEN [type |-> "statusResponse", peerId |-> peer, height |-> pState.peerHeights[peer]] - ELSE [type |-> "statusResponse", peerId |-> peer, height |-> anyHeight] IN + THEN AsInMsg([type |-> "statusResponse", peerId |-> peer, height |-> pState.peerHeights[peer]]) + ELSE AsInMsg([type |-> "statusResponse", peerId |-> peer, height |-> anyHeight]) IN [msg |-> m, peers |-> pState] CreateBlockResponse(msg, pState, arbitraryBlock) == LET m == IF msg.peerId \in CORRECT - THEN [type |-> "blockResponse", peerId |-> msg.peerId, block |-> CorrectBlock(msg.height)] - ELSE [type |-> "blockResponse", peerId |-> msg.peerId, block |-> arbitraryBlock] IN + THEN AsInMsg([type |-> "blockResponse", peerId |-> msg.peerId, block |-> CorrectBlock(msg.height)]) + ELSE AsInMsg([type |-> "blockResponse", peerId |-> msg.peerId, block |-> arbitraryBlock]) IN LET npState == [pState EXCEPT !.blocksRequested = pState.blocksRequested \ {msg} ] IN [msg |-> m, peers |-> npState] -GrowBlockchain(pState) == +GrowPeerHeight(pState) == \E p \in CORRECT: /\ pState.peerHeights[p] < MAX_HEIGHT /\ peersState' = [pState EXCEPT !.peerHeights[p] = @ + 1] - /\ inMsg' = NoMsg - + /\ inMsg' = AsInMsg(NoMsg) SendStatusResponseMessage(pState) == /\ \E arbitraryHeight \in Heights: @@ -530,17 +574,14 @@ SendStatusResponseMessage(pState) == SendAddPeerMessage == \E peer \in AllPeerIds: - /\ inMsg' = [type |-> "addPeer", peerId |-> peer] - /\ UNCHANGED peersState + inMsg' = AsInMsg([type |-> "addPeer", peerId |-> peer]) SendRemovePeerMessage == \E peer \in AllPeerIds: - /\ inMsg' = [type |-> "removePeer", peerId |-> peer] - /\ UNCHANGED peersState + inMsg' = AsInMsg([type |-> "removePeer", peerId |-> peer]) SendSyncTimeoutMessage == - /\ inMsg' = [type |-> "syncTimeout"] - /\ UNCHANGED peersState + inMsg' = AsInMsg([type |-> "syncTimeout"]) SendControlMessage == @@ -548,22 +589,44 @@ SendControlMessage == \/ SendRemovePeerMessage \/ SendSyncTimeoutMessage +\* An extremely important property of block hashes (blockId): +\* If a commit is correct, then the previous block in the block store must be also correct. +UnforgeableBlockId(height, block) == + block.hashEqRef => block = chain[height] + +\* A faulty peer cannot forge enough of the validators signatures. +\* A more precise rule should have checked that the commiters have over 2/3 of the VS's voting power. +NoFork(height, block) == + (height > 1 /\ block.lastCommit.committers = chain[height - 1].VS) + => block.lastCommit.blockIdEqRef + +\* Can be block produced by a faulty peer +IsBlockByFaulty(height, block) == + /\ block.height = height + /\ UnforgeableBlockId(height, block) + /\ NoFork(height, block) SendBlockResponseMessage(pState) == - \/ /\ pState.blocksRequested /= {} + \* a response to a requested block: either by a correct, or by a faulty peer + \/ /\ pState.blocksRequested /= AsOutMsgSet({}) /\ \E msg \in pState.blocksRequested: \E block \in Blocks: - LET msgAndPeers == CreateBlockResponse(msg, pState, block) IN - /\ peersState' = msgAndPeers.peers - /\ inMsg' = msgAndPeers.msg - - - \/ /\ peersState' = pState - /\ inMsg' \in [type: {"blockResponse"}, peerId: FAULTY, block: Blocks] + /\ IsBlockByFaulty(msg.height, block) + /\ LET msgAndPeers == CreateBlockResponse(msg, pState, block) IN + /\ peersState' = msgAndPeers.peers + /\ inMsg' = msgAndPeers.msg + + \* a faulty peer can always send an unsolicited block + \/ \E peerId \in FAULTY: + \E block \in Blocks: + /\ IsBlockByFaulty(block.height, block) + /\ peersState' = pState + /\ inMsg' = AsInMsg([type |-> "blockResponse", + peerId |-> peerId, block |-> block]) - SendNoBlockResponseMessage(pState) == +SendNoBlockResponseMessage(pState) == /\ peersState' = pState - /\ inMsg' \in [type: {"noBlockResponse"}, peerId: FAULTY, height: Heights] + /\ inMsg' \in AsInMsgSet([type: {"noBlockResponse"}, peerId: FAULTY, height: Heights]) SendResponseMessage(pState) == @@ -574,53 +637,51 @@ SendResponseMessage(pState) == NextEnvStep(pState) == \/ SendResponseMessage(pState) - \/ GrowBlockchain(pState) - \/ SendControlMessage + \/ GrowPeerHeight(pState) + \/ SendControlMessage /\ peersState' = pState + \* note that we propagate pState that was missing in the previous version \* Peers consume a message and update it's local state. It then makes a single step, i.e., it sends at most single message. \* Message sent could be either a response to a request or faulty message (sent by faulty processes). NextPeers == LET pState == HandleRequest(outMsg, peersState) IN - - \/ /\ outMsg' = NoMsg - /\ NextEnvStep(pState) + /\ outMsg' = AsOutMsg(NoMsg) + /\ NextEnvStep(pState) \* the composition of the node, the peers, the network and scheduler Init == + /\ IsCorrectChain(chain) \* initialize the blockchain /\ InitNode /\ InitPeers /\ turn = "Peers" - /\ inMsg = NoMsg - /\ outMsg = [type |-> "statusRequest"] + /\ inMsg = AsInMsg(NoMsg) + /\ outMsg = AsOutMsg([type |-> "statusRequest"]) Next == - IF turn = "Peers" - THEN - /\ NextPeers - /\ turn' = "Node" - /\ UNCHANGED nvars - ELSE - /\ NextNode - /\ turn' = "Peers" - /\ UNCHANGED peersState - + IF turn = "Peers" + THEN + /\ NextPeers + /\ turn' = "Node" + /\ UNCHANGED <> + ELSE + /\ NextNode + /\ turn' = "Peers" + /\ UNCHANGED <> FlipTurn == - turn' = ( + turn' = IF turn = "Peers" THEN "Node" ELSE "Peers" - ) - \* Compute max peer height. Used as a helper operator in properties. MaxCorrectPeerHeight(bPool) == LET correctPeers == {p \in bPool.peerIds: p \in CORRECT} IN - IF correctPeers = {} + IF correctPeers = AsPidSet({}) THEN 0 \* no peers, just return 0 ELSE LET Hts == {bPool.peerHeights[p] : p \in correctPeers} IN CHOOSE max \in Hts: \A h \in Hts: h <= max @@ -639,7 +700,6 @@ TypeOK == [type: {"blockRequest"}, peerId: AllPeerIds, height: Heights] ] - /\ blockPool \in [ height: Heights, peerIds: SUBSET AllPeerIds, @@ -651,27 +711,87 @@ TypeOK == syncHeight: Heights ] -\* TODO: align with the English spec. Add reference to it -Correctness1 == state = "finished" => - blockPool.height >= MaxCorrectPeerHeight(blockPool) +(* Incorrect synchronization: The last block may be never received *) +Sync1 == + [](state = "finished" => + blockPool.height >= MaxCorrectPeerHeight(blockPool)) -\* TODO: align with the English spec. Add reference to it -Correctness2 == +Sync1AsInv == + state = "finished" => blockPool.height >= MaxCorrectPeerHeight(blockPool) + +(* Incorrect synchronization, as there may be a timeout *) +Sync2 == \A p \in CORRECT: \/ p \notin blockPool.peerIds \/ [] (state = "finished" => blockPool.height >= blockPool.peerHeights[p] - 1) -\* TODO: align with the English spec. Add reference to it -Termination == WF_turn(FlipTurn) => <>(state = "finished") - -\* a few simple properties that trigger counterexamples +Sync2AsInv == + \A p \in CORRECT: + \/ p \notin blockPool.peerIds + \/ (state = "finished" => blockPool.height >= blockPool.peerHeights[p] - 1) -\* Shows execution in which peer set is empty -PeerSetIsNeverEmpty == blockPool.peerIds /= {} +(* Correct synchronization *) +Sync3 == + \A p \in CORRECT: + \/ p \notin blockPool.peerIds + \/ blockPool.syncedBlocks <= 0 \* timeout + \/ [] (state = "finished" => blockPool.height >= blockPool.peerHeights[p] - 1) -\* Shows execution in which state = "finished" and MaxPeerHeight is not equal to 1 -StateNotFinished == - state /= "finished" \/ MaxPeerHeight(blockPool) = 1 +Sync3AsInv == + \A p \in CORRECT: + \/ p \notin blockPool.peerIds + \/ blockPool.syncedBlocks <= 0 \* timeout + \/ (state = "finished" => blockPool.height >= blockPool.peerHeights[p] - 1) + +(* Naive termination *) +\* This property is violated, as the faulty peers may produce infinitely many responses +Termination == + WF_turn(FlipTurn) => <>(state = "finished") + +(* Termination by timeout: the protocol terminates, if there is a timeout *) +\* the precondition: fair flip turn and eventual timeout when no new blocks were synchronized +TerminationByTOPre == + /\ WF_turn(FlipTurn) + /\ <>(inMsg.type = "syncTimeout" /\ blockPool.height <= blockPool.syncHeight) + +TerminationByTO == + TerminationByTOPre => <>(state = "finished") + +(* The termination property when we only have correct peers *) +\* as correct peers may spam the node with addPeer, removePeer, and statusResponse, +\* we have to enforce eventual response (there are no queues in our spec) +CorrBlockResponse == + \A h \in Heights: + [](outMsg.type = "blockRequest" /\ outMsg.height = h + => <>(inMsg.type = "blockResponse" /\ inMsg.block.height = h)) + +\* a precondition for termination in presence of only correct processes +TerminationCorrPre == + /\ FAULTY = AsPidSet({}) + /\ WF_turn(FlipTurn) + /\ CorrBlockResponse + +\* termination when there are only correct processes +TerminationCorr == + TerminationCorrPre => <>(state = "finished") + +\* All synchronized blocks (but the last one) are exactly like in the reference chain +CorrectBlocksInv == + \/ state /= "finished" + \/ \A h \in 1..(blockPool.height - 1): + blockPool.blockStore[h] = chain[h] + +\* A false expectation that the protocol only finishes with the blocks +\* from the processes that had not been suspected in being faulty +SyncFromCorrectInv == + \/ state /= "finished" + \/ \A h \in 1..blockPool.height: + blockPool.receivedBlocks[h] \in blockPool.peerIds \union {NilPeer} + +\* A false expectation that a correct process is never removed from the set of peer ids. +\* A correct process may reply too late and then gets evicted. +CorrectNeverSuspectedInv == + CORRECT \subseteq blockPool.peerIds BlockPoolInvariant == \A h \in Heights: @@ -683,10 +803,20 @@ BlockPoolInvariant == /\ blockPool.blockStore[h] /= NilBlock /\ blockPool.pendingBlocks[h] = NilPeer +(* a few simple properties that trigger counterexamples *) + +\* Shows execution in which peer set is empty +PeerSetIsNeverEmpty == blockPool.peerIds /= AsPidSet({}) + +\* Shows execution in which state = "finished" and MaxPeerHeight is not equal to 1 +StateNotFinished == + state /= "finished" \/ MaxPeerHeight(blockPool) = 1 + + ============================================================================= \*============================================================================= \* Modification History +\* Last modified Fri May 29 20:41:53 CEST 2020 by igor \* Last modified Thu Apr 16 16:57:22 CEST 2020 by zarkomilosevic -\* Last modified Thu Apr 09 12:53:53 CEST 2020 by igor \* Created Tue Feb 04 10:36:18 CET 2020 by zarkomilosevic From 1a431cbae2e8532867b25ef0675c36a6b8bdba73 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Tue, 21 Jul 2020 15:34:26 +0200 Subject: [PATCH 29/34] copied Tinychain.tla from verification --- docs/spec/fastsync/Tinychain.tla | 110 +++++++++++++++++++++++++++++++ 1 file changed, 110 insertions(+) create mode 100644 docs/spec/fastsync/Tinychain.tla diff --git a/docs/spec/fastsync/Tinychain.tla b/docs/spec/fastsync/Tinychain.tla new file mode 100644 index 000000000..b8a212996 --- /dev/null +++ b/docs/spec/fastsync/Tinychain.tla @@ -0,0 +1,110 @@ +-------------------------- MODULE Tinychain ---------------------------------- +(* A very abstract model of Tendermint blockchain. Its only purpose is to highlight + the relation between validator sets, next validator sets, and last commits. + *) + +EXTENDS Integers + +\* type annotation +a <: b == a + +\* the type of validator sets, e.g., STRING +VST == STRING + +\* LastCommit type. +\* It contains: +\* 1) the flag of whether the block id equals to the hash of the previous block, and +\* 2) the set of the validators who have committed the block. +\* In the implementation, blockId is the hash of the previous block, which cannot be forged. +\* We abstract block id into whether it equals to the hash of the previous block or not. +LCT == [blockIdEqRef |-> BOOLEAN, committers |-> VST] + +\* Block type. +\* A block contains its height, validator set, next validator set, and last commit. +\* Moreover, it contains the flag that tells us whether the block equals to the one +\* on the reference chain (this is an abstraction of hash). +BT == [height |-> Int, hashEqRef |-> BOOLEAN, wellFormed |-> BOOLEAN, + VS |-> VST, NextVS |-> VST, lastCommit |-> LCT] + +CONSTANTS + (* + A set of abstract values, each value representing a set of validators. + For the purposes of this specification, they can be any values, + e.g., "s1", "s2", etc. + *) + VALIDATOR_SETS, + (* a nil validator set that is outside of VALIDATOR_SETS *) + NIL_VS, + (* The maximal height, up to which the blockchain may grow *) + MAX_HEIGHT + +Heights == 1..MAX_HEIGHT + +\* the set of all possible commits +Commits == [blockIdEqRef: BOOLEAN, committers: VALIDATOR_SETS] + +\* the set of all possible blocks, not necessarily valid ones +Blocks == + [height: Heights, hashEqRef: BOOLEAN, wellFormed: BOOLEAN, + VS: VALIDATOR_SETS, NextVS: VALIDATOR_SETS, lastCommit: Commits] + +\* Does the chain contain a sound sequence of blocks that could be produced by +\* a 2/3 of faulty validators. This operator can be used to initialise the chain! +IsCorrectChain(chain) == + \* restrict the structure of the blocks, to decrease the TLC search space + LET OkCommits == [blockIdEqRef: {TRUE}, committers: VALIDATOR_SETS] + OkBlocks == [height: Heights, hashEqRef: {TRUE}, wellFormed: {TRUE}, + VS: VALIDATOR_SETS, NextVS: VALIDATOR_SETS, lastCommit: OkCommits] + IN + /\ chain \in [1..MAX_HEIGHT -> OkBlocks] + /\ \A h \in 1..MAX_HEIGHT: + LET b == chain[h] IN + /\ b.height = h \* the height is correct + /\ h > 1 => + LET p == chain[h - 1] IN + /\ b.VS = p.NextVS \* the validators propagate from the previous block + /\ b.lastCommit.committers = p.VS \* and they are the committers + + +\* The basic properties of blocks on the blockchain: +\* They should pass the validity check and they may verify the next block. + +\* Does the block pass the consistency check against the next validators of the previous block +IsMatchingValidators(block, nextVS) == + \* simply check that the validator set is propagated correctly. + \* (the implementation tests hashes and the application state) + block.VS = nextVS + +\* Does the block verify the commit (of the next block) +PossibleCommit(block, commit) == + \* the commits are signed by the block validators + /\ commit.committers = block.VS + \* The block id in the commit matches the block hash (abstract comparison). + \* (The implementation has extensive tests for that.) + \* this is an abstraction of: commit.blockId = hash(block) + \* + \* These are possible scenarios on the concrete hashes: + \* + \* scenario 1: commit.blockId = 10 /\ hash(block) = 10 /\ hash(ref) = 10 + \* scenario 2: commit.blockId = 20 /\ hash(block) = 20 /\ block.VS /= ref.VS + \* scenario 3: commit.blockId = 50 /\ hash(block) = 100 + \* scenario 4: commit.blockId = 10 /\ hash(block) = 100 + \* scenario 5: commit.blockId = 100 /\ hash(block) = 10 + /\ commit.blockIdEqRef = block.hashEqRef + \* the following test would be cheating, as we do not have access to the + \* reference chain: + \* /\ commit.blockIdEqRef + +\* Basic invariants + +\* every block has the validator set that is chosen by its predecessor +ValidBlockInv(chain) == + \A h \in 2..MAX_HEIGHT: + IsMatchingValidators(chain[h], chain[h - 1].NextVS) + +\* last commit of every block is signed by the validators of the predecessor +VerifiedBlockInv(chain) == + \A h \in 2..MAX_HEIGHT: + PossibleCommit(chain[h - 1], chain[h].lastCommit) + +================================================================================== From 2ee8b8bee2d0d76bd16e4a1be6c6f73a086aadc8 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Tue, 28 Jul 2020 15:16:38 +0200 Subject: [PATCH 30/34] updated the spec name --- docs/spec/fastsync/fastsync.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/spec/fastsync/fastsync.tla b/docs/spec/fastsync/fastsync.tla index 51dd54e57..1aad6b553 100644 --- a/docs/spec/fastsync/fastsync.tla +++ b/docs/spec/fastsync/fastsync.tla @@ -1,4 +1,4 @@ ------------------------------ MODULE fastsync_apalache ----------------------------- +----------------------------- MODULE fastsync ----------------------------- (* In this document we give the high level specification of the fast sync protocol as implemented here: From 67ae7c3a253aad67f9ed45f820dac6983609a068 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 7 Aug 2020 11:57:49 +0200 Subject: [PATCH 31/34] Update docs/spec/fastsync/Tinychain.tla Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> --- docs/spec/fastsync/Tinychain.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/spec/fastsync/Tinychain.tla b/docs/spec/fastsync/Tinychain.tla index b8a212996..adc541efd 100644 --- a/docs/spec/fastsync/Tinychain.tla +++ b/docs/spec/fastsync/Tinychain.tla @@ -21,7 +21,7 @@ LCT == [blockIdEqRef |-> BOOLEAN, committers |-> VST] \* Block type. \* A block contains its height, validator set, next validator set, and last commit. -\* Moreover, it contains the flag that tells us whether the block equals to the one +\* Moreover, it contains the flag that tells us whether the block is equal to the one \* on the reference chain (this is an abstraction of hash). BT == [height |-> Int, hashEqRef |-> BOOLEAN, wellFormed |-> BOOLEAN, VS |-> VST, NextVS |-> VST, lastCommit |-> LCT] From 28e877bafca1d6c6fb3825fa90a961912833c014 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 7 Aug 2020 11:58:24 +0200 Subject: [PATCH 32/34] Update docs/spec/fastsync/fastsync.tla Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> --- docs/spec/fastsync/fastsync.tla | 2 ++ 1 file changed, 2 insertions(+) diff --git a/docs/spec/fastsync/fastsync.tla b/docs/spec/fastsync/fastsync.tla index 1aad6b553..b03bf08d6 100644 --- a/docs/spec/fastsync/fastsync.tla +++ b/docs/spec/fastsync/fastsync.tla @@ -595,6 +595,8 @@ UnforgeableBlockId(height, block) == block.hashEqRef => block = chain[height] \* A faulty peer cannot forge enough of the validators signatures. +\* In other words: If a commit contains enough signatures from the validators (in reality 2/3, in the model all), +\* then the blockID points to the block on the chain, encoded as block.lastCommit.blockIdEqRef being true \* A more precise rule should have checked that the commiters have over 2/3 of the VS's voting power. NoFork(height, block) == (height > 1 /\ block.lastCommit.committers = chain[height - 1].VS) From 52eec6f2e3a6f18a027bfd3f437a27603bddcf25 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 7 Aug 2020 11:58:35 +0200 Subject: [PATCH 33/34] Update docs/spec/fastsync/fastsync.tla Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> --- docs/spec/fastsync/fastsync.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/spec/fastsync/fastsync.tla b/docs/spec/fastsync/fastsync.tla index b03bf08d6..e2649997a 100644 --- a/docs/spec/fastsync/fastsync.tla +++ b/docs/spec/fastsync/fastsync.tla @@ -602,7 +602,7 @@ NoFork(height, block) == (height > 1 /\ block.lastCommit.committers = chain[height - 1].VS) => block.lastCommit.blockIdEqRef -\* Can be block produced by a faulty peer +\* Can be block produced by a faulty peer, assuming it cannot generate forks (basic assumption of the protocol) IsBlockByFaulty(height, block) == /\ block.height = height /\ UnforgeableBlockId(height, block) From 057c81fcb72273e76b1eea3fa14ea44f94ca1698 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 7 Aug 2020 16:15:21 +0200 Subject: [PATCH 34/34] addressing Josef's comments --- docs/spec/fastsync/Tinychain.tla | 7 +++++-- docs/spec/fastsync/fastsync.tla | 5 +++-- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/docs/spec/fastsync/Tinychain.tla b/docs/spec/fastsync/Tinychain.tla index adc541efd..26200c4f6 100644 --- a/docs/spec/fastsync/Tinychain.tla +++ b/docs/spec/fastsync/Tinychain.tla @@ -40,16 +40,19 @@ CONSTANTS Heights == 1..MAX_HEIGHT -\* the set of all possible commits +\* the set of all potential commits Commits == [blockIdEqRef: BOOLEAN, committers: VALIDATOR_SETS] -\* the set of all possible blocks, not necessarily valid ones +\* the set of all potential blocks, not necessarily coming from the blockchain Blocks == [height: Heights, hashEqRef: BOOLEAN, wellFormed: BOOLEAN, VS: VALIDATOR_SETS, NextVS: VALIDATOR_SETS, lastCommit: Commits] \* Does the chain contain a sound sequence of blocks that could be produced by \* a 2/3 of faulty validators. This operator can be used to initialise the chain! +\* Since we are abstracting validator sets with VALIDATOR_SETS, which are +\* 2/3 quorums, we just compare committers to those sets. In a more detailed +\* specification, one would write the \subseteq operator instead of equality. IsCorrectChain(chain) == \* restrict the structure of the blocks, to decrease the TLC search space LET OkCommits == [blockIdEqRef: {TRUE}, committers: VALIDATOR_SETS] diff --git a/docs/spec/fastsync/fastsync.tla b/docs/spec/fastsync/fastsync.tla index e2649997a..e1b7b812b 100644 --- a/docs/spec/fastsync/fastsync.tla +++ b/docs/spec/fastsync/fastsync.tla @@ -208,7 +208,7 @@ OutMsgs == InitNode == \E pIds \in SUBSET AllPeerIds: \* set of peers node established initial connections with - /\ pIds \subseteq CORRECT + /\ pIds \subseteq CORRECT \* this line is not necessary /\ pIds /= AsPidSet({}) \* apalache better checks non-emptiness than subtracts from SUBSET /\ blockPool = AsBlockPool([ height |-> TrustedHeight + 1, \* the genesis block is at height 1 @@ -590,7 +590,8 @@ SendControlMessage == \/ SendSyncTimeoutMessage \* An extremely important property of block hashes (blockId): -\* If a commit is correct, then the previous block in the block store must be also correct. +\* If the block hash coincides with the hash of the reference block, +\* then the blocks should be equal. UnforgeableBlockId(height, block) == block.hashEqRef => block = chain[height]