diff --git a/docs/sbft-formal-model/README.md b/docs/sbft-formal-model/README.md index 23cb4a30c4..f3b31b1ef3 100644 --- a/docs/sbft-formal-model/README.md +++ b/docs/sbft-formal-model/README.md @@ -1,4 +1,5 @@ -# Project overview +## Project overview + The aim of this sub-project is to both document and to formally specify the concord-bft state machine replication (SMR) protocol. Given the distributed nature of the concord-bft protocol, unit tests offer limited means of establishing the desired state machine replication (SMR) safety properties. The main tool we use for proving correctness is an integration testing framework code-named [Apollo](https://github.com/vmware/concord-bft/tree/master/tests/apollo) which creates mini-blockchain deployments and exercises various runtime scenarios (including straight case, replica failures, network faults, as well as certain byzantine cases). @@ -7,7 +8,7 @@ Apollo does give us good confidence as to the correctness and fault tolerance of We use Dafny and first-order logic to model and prove the safety properties of the protocol's core state machine (liveness properties are out of scope for now). -# Dev instructions +## Dev instructions The Dafny model can be used as a document, for proving SBFT correctness properties, or as input for property-based tests of the implementation's core components. @@ -27,6 +28,7 @@ newgrp docker ``` ## Pull the image. + (This is the slow thing; it includes a couple GB of Ubuntu.) ```bash @@ -69,6 +71,28 @@ If everything is working, you should see something like: Dafny program verifier finished with 10 verified, 0 errors ``` -# Acknowledgements and references +## Acknowledgements and references Special thanks to [@jonhnet](https://github.com/jonhnet) for his help and support along the way. + +## Current status + +# We have completed the modeling of *replica.i.dfy* covering the following parts of the protocol: + +1. Slow Commit Path - the 2 phase commit path that requires collecting Prepared Certificate (2F+1 matching Prepares) and a Committed Certificate (2F+1 Commit messages). +2. View change - the mechanism that the system uses to replace the leader (Primary) in order to preserve livenes. +3. Sliding of the Working Window and Checkpointing - periodically the replicas exchange Checkpoint messages to reach agreement on the state. This also enables them to slide the Working Window of Sequence ID-s that can be considered for consensus in each replica. The checkpointing is crucial also for enabling replicas to catch up in case of long down time of a given replica. The Checkpoint represents a summary of the state (a hash in the implementation code and the entire state itself in the model) that can be used for correctness check when performing State Transfer. +4. State Transfer - the mechanism for replicas to help peers that have been disconnected for long enough to be unable to catch up because the system's Working Window has advanced beyond the particular replica's Working Window. This is a process that in the implementation code transfers portions of the state until catching up is completed in the behind replica. In the model we have the entire state in each Checkpoint message, therefore we can perform State Transfer once we collect quorum (2F+1) matching Checkpoint messages to the state in any of those messages (they have to be equal) if this state turns out to be more recent than our current state. We determine recentness based to the highest Sequence ID for which the system has reached consensus. + +# Modeling of malicious behavior in the system *faulty_replica.i.dfy*. + +To achieve validation in the presence of malicious behavior once we start writing the proof we needed a subset of the replicas (up to F) to act in a way that could try to corrupt the system. We achieve this by not restricting the F faulty replicas' actions in any specific way, thus allowing completely arbitrary behavior which can be considered as a super set of the Malicious behavior, which itself is a super set of the correct (honest) behavior that follows the protocol steps. + +# Message signatures checks support in *network.s.dfy*. + +In order for us to model signatures we have used the network to be a trusted arbitrary. It stores all the previously sent messages and can determine if a message really originated form a given host. The network rejects messages from hosts that try to impersonate another one. We also provide a mechanism to validate sub messages (some of the protocol messages are composite - carrying messages collected form peers in the model and hashes of those messages in the implementation code). + +# Progress on the proof. + +We have completed the proof that commit messages form honest senders agree in a given View, put otherwise, that consensus is reached in a View. This is a stepping stone for us to be able to prove consensus in the system is maintained even in the presence of multiple View Changes and at most F faulty replicas. The next milestone in proving UnCommitableAgreesWithPrepare. This predicate serves to bind the future and the past, showing that if an Hones Replica sends a Prepare message in a given View (effectively voting for a proposal from the primary for assigning a Client operation to a Sequence ID), it has performed all the necessary checks to validate that nothing else is commitable in prior views. +For the current state of the proof we have disabled sliding of the Working Window and Checkpointing in order to split the effort in smaller steps. \ No newline at end of file diff --git a/docs/sbft-formal-model/cluster_config.s.dfy b/docs/sbft-formal-model/cluster_config.s.dfy index 0ea42e862e..41fa93540d 100644 --- a/docs/sbft-formal-model/cluster_config.s.dfy +++ b/docs/sbft-formal-model/cluster_config.s.dfy @@ -14,6 +14,8 @@ include "network.s.dfy" module ClusterConfig { import opened HostIdentifiers + type ViewNum = nat + datatype Constants = Constants( maxByzantineFaultyReplicas:nat, numClients:nat, @@ -32,6 +34,12 @@ module ClusterConfig { N() + numClients } + function PrimaryForView(view:ViewNum) : nat + requires WF() + { + view % N() + } + function F() : nat requires WF() { diff --git a/docs/sbft-formal-model/library/Library.dfy b/docs/sbft-formal-model/library/Library.dfy index 87b2f8e599..d23d1d9ad4 100644 --- a/docs/sbft-formal-model/library/Library.dfy +++ b/docs/sbft-formal-model/library/Library.dfy @@ -1,4 +1,25 @@ module Library { + lemma MappedSetCardinality(p:set, f:(T)-->V, filtered:set) + requires forall t | t in p :: f.requires(t) + requires forall x, y | && x in p + && y in p + && f(x) == f(y) + :: x == y + //requires filtered == set t | t in p :: f(t) // TODO: bug in Dafny makes this un-triggerable. Uncomment when we find a workaround! + ensures |filtered| == |p| + { + assert filtered == set t | t in p :: f(t) by { + assume false; // TODO: temporary fix for triggering problem in Dafny. + } + if |p| != 0 { + var t0 :| t0 in p; + var sub_p := p - {t0}; + MappedSetCardinality(sub_p, f, set t | t in sub_p :: f(t)); + assert p == sub_p + {t0}; // Trigger extentionallity + assert (set t | t in p :: f(t)) == (set t | t in sub_p :: f(t)) + {f(t0)}; // Trigger extentionallity + } + } + function DropLast(theSeq: seq) : seq requires 0 < |theSeq| { diff --git a/docs/sbft-formal-model/messages.dfy b/docs/sbft-formal-model/messages.dfy index c6a919348c..8672dc60ad 100644 --- a/docs/sbft-formal-model/messages.dfy +++ b/docs/sbft-formal-model/messages.dfy @@ -11,14 +11,15 @@ include "network.s.dfy" include "library/Library.dfy" +include "cluster_config.s.dfy" module Messages { import Library import opened HostIdentifiers import Network + import opened ClusterConfig - type SequenceID = k:nat | 0 < k witness 1 - type ViewNum = nat + type SequenceID = nat datatype ClientOperation = ClientOperation(sender:HostId, timestamp:nat) @@ -40,26 +41,42 @@ module Messages { predicate WF() { (forall v | v in votes :: v.payload.Prepare?) } - predicate valid(quorumSize:nat) { + predicate validFull(clusterConfig:ClusterConfig.Constants, seqID:SequenceID) + requires clusterConfig.WF() + { + && |votes| >= clusterConfig.AgreementQuorum() + && WF() + && prototype().seqID == seqID + && (forall v | v in votes :: v.payload == prototype()) // messages have to be votes that match eachother by the prototype + && UniqueSenders(votes) + && (forall v | v in votes :: clusterConfig.IsReplica(v.sender)) + } + predicate valid(clusterConfig:ClusterConfig.Constants, seqID:SequenceID) + requires clusterConfig.WF() + { || empty() - || (&& |votes| == quorumSize - && WF() - && (forall v | v in votes :: v.payload == prototype()) // messages have to be votes that match eachother by the prototype - && UniqueSenders(votes)) + || validFull(clusterConfig, seqID) } predicate empty() { && |votes| == 0 } + predicate votesRespectView(view:ViewNum) + requires WF() + { + !empty() ==> prototype().view < view + } } datatype ViewChangeMsgsSelectedByPrimary = ViewChangeMsgsSelectedByPrimary(msgs:set>) { - predicate valid(view:ViewNum, quorumSize:nat) { + predicate valid(view:ViewNum, clusterConfig:ClusterConfig.Constants) + requires clusterConfig.WF() + { && |msgs| > 0 && (forall v | v in msgs :: && v.payload.ViewChangeMsg? - && v.payload.validViewChangeMsg(quorumSize) + && v.payload.validViewChangeMsg(clusterConfig) && v.payload.newView == view) // All the ViewChange messages have to be for the same View. && UniqueSenders(msgs) - && |msgs| == quorumSize //TODO: once proof is complete try with >= + && |msgs| == clusterConfig.AgreementQuorum() //TODO: once proof is complete try with >= } } @@ -71,12 +88,14 @@ module Messages { prot.payload } predicate valid(lastStableCheckpoint:SequenceID, quorumSize:nat) { - && |msgs| > 0 - && UniqueSenders(msgs) - && (forall m | m in msgs :: && m.payload.CheckpointMsg? - && m.payload == prototype() - && m.payload.seqIDReached == lastStableCheckpoint) - && |msgs| >= quorumSize + || (&& lastStableCheckpoint == 0 + && |msgs| == 0) + || (&& |msgs| > 0 + && UniqueSenders(msgs) + && (forall m | m in msgs :: && m.payload.CheckpointMsg? + && m.payload == prototype() + && m.payload.seqIDReached == lastStableCheckpoint) + && |msgs| >= quorumSize) } } @@ -87,7 +106,7 @@ module Messages { :: m1.sender != m2.sender) } - // Define your Message datatype here. + // Define your Message datatype here. // TODO: rename to payload. datatype Message = | PrePrepare(view:ViewNum, seqID:SequenceID, operationWrapper:OperationWrapper) | Prepare(view:ViewNum, seqID:SequenceID, operationWrapper:OperationWrapper) | Commit(view:ViewNum, seqID:SequenceID, operationWrapper:OperationWrapper) @@ -99,20 +118,51 @@ module Messages { | NewViewMsg(newView:ViewNum, vcMsgs:ViewChangeMsgsSelectedByPrimary) | CheckpointMsg(seqIDReached:SequenceID, committedClientOperations:CommittedClientOperations) { - predicate valid(quorumSize:nat) + predicate valid(clusterConfig:ClusterConfig.Constants) + requires clusterConfig.WF() { - && (ViewChangeMsg? ==> validViewChangeMsg(quorumSize)) - && (NewViewMsg? ==> validNewViewMsg(quorumSize)) + && (ViewChangeMsg? ==> validViewChangeMsg(clusterConfig)) + && (NewViewMsg? ==> validNewViewMsg(clusterConfig)) } - predicate validViewChangeMsg(quorumSize:nat) + predicate checked(clusterConfig:ClusterConfig.Constants, sigChecks:set>) + requires clusterConfig.WF() + { + && (ViewChangeMsg? ==> checkedViewChangeMsg(clusterConfig, sigChecks)) + && (NewViewMsg? ==> checkedNewViewMsg(clusterConfig, sigChecks)) + } + predicate validViewChangeMsg(clusterConfig:ClusterConfig.Constants) + requires clusterConfig.WF() + requires ViewChangeMsg? + { + && (forall seqID | seqID in certificates + :: && certificates[seqID].valid(clusterConfig, seqID) + && certificates[seqID].votesRespectView(newView)) + && proofForLastStable.valid(lastStableCheckpoint, clusterConfig.AgreementQuorum()) + } + predicate validNewViewMsg(clusterConfig:ClusterConfig.Constants) + requires clusterConfig.WF() + requires NewViewMsg? + { + && vcMsgs.valid(newView, clusterConfig) + && (forall replica | replica in sendersOf(vcMsgs.msgs) + :: clusterConfig.IsReplica(replica)) + } + predicate checkedViewChangeMsg(clusterConfig:ClusterConfig.Constants, sigChecks:set>) requires ViewChangeMsg? + requires clusterConfig.WF() { - proofForLastStable.valid(lastStableCheckpoint, quorumSize) + && valid(clusterConfig) + // Check Checkpoint msg-s signatures: + && proofForLastStable.msgs <= sigChecks + && (forall seqID | seqID in certificates + :: && certificates[seqID].votes <= sigChecks) } - predicate validNewViewMsg(quorumSize:nat) + predicate checkedNewViewMsg(clusterConfig:ClusterConfig.Constants, sigChecks:set>) requires NewViewMsg? + requires clusterConfig.WF() { - vcMsgs.valid(newView, quorumSize) + && valid(clusterConfig) + && vcMsgs.msgs <= sigChecks } predicate IsIntraViewMsg() { || PrePrepare? @@ -120,5 +170,12 @@ module Messages { || Commit? } } + predicate ValidNewViewMsg(clusterConfig:ClusterConfig.Constants, msg:Network.Message) + { + && clusterConfig.WF() + && msg.payload.NewViewMsg? + && msg.payload.valid(clusterConfig) + && clusterConfig.PrimaryForView(msg.payload.newView) == msg.sender + } // ToDo: ClientReply } diff --git a/docs/sbft-formal-model/proof.dfy b/docs/sbft-formal-model/proof.dfy index 081276d746..f35e926104 100644 --- a/docs/sbft-formal-model/proof.dfy +++ b/docs/sbft-formal-model/proof.dfy @@ -29,6 +29,8 @@ module Proof { import opened SafetySpec import opened Library + type Message = Network.Message + predicate IsHonestReplica(c:Constants, hostId:HostId) { && c.WF() @@ -44,10 +46,13 @@ module Proof { && var replicaConstants := c.hosts[replicaIdx].replicaConstants; && seqID in replicaVariables.workingWindow.getActiveSequenceIDs(replicaConstants) && replicaVariables.workingWindow.prePreparesRcvd[seqID].Some? - :: v.hosts[replicaIdx].replicaVariables.workingWindow.prePreparesRcvd[seqID].value in v.network.sentMsgs) + :: (&& var msg := v.hosts[replicaIdx].replicaVariables.workingWindow.prePreparesRcvd[seqID].value; + && msg in v.network.sentMsgs + && msg.payload.seqID == seqID)) // The key we stored matches what is in the msg + } - predicate RecordedPreparesRecvdCameFromNetwork(c:Constants, v:Variables, observer:HostId) + predicate RecordedPreparesRecvdCameFromNetworkForHost(c:Constants, v:Variables, observer:HostId) { && v.WF(c) && IsHonestReplica(c, observer) @@ -62,14 +67,14 @@ module Proof { && msg.payload.seqID == seqID)) // The key we stored matches what is in the msg } - predicate {:opaque} RecordedPreparesInAllHostsRecvdCameFromNetwork(c:Constants, v:Variables) { + predicate {:opaque} RecordedPreparesRecvdCameFromNetwork(c:Constants, v:Variables) { && v.WF(c) && (forall observer | && IsHonestReplica(c, observer) - :: RecordedPreparesRecvdCameFromNetwork(c, v, observer)) + :: RecordedPreparesRecvdCameFromNetworkForHost(c, v, observer)) } - predicate {:opaque} EveryCommitMsgIsSupportedByAQuorumOfPrepares(c:Constants, v:Variables) { + predicate {:opaque} EveryCommitMsgIsSupportedByAQuorumOfSentPrepares(c:Constants, v:Variables) { && v.WF(c) && (forall commitMsg | && commitMsg in v.network.sentMsgs && commitMsg.payload.Commit? @@ -78,6 +83,79 @@ module Proof { commitMsg.payload.seqID, commitMsg.payload.operationWrapper) ) } + predicate {:opaque} EveryCommitMsgIsSupportedByAQuorumOfRecordedPrepares(c:Constants, v:Variables) { + && v.WF(c) + && (forall commitMsg | && commitMsg in v.network.sentMsgs + && commitMsg.payload.Commit? + && IsHonestReplica(c, commitMsg.sender) + && var committer_c := c.hosts[commitMsg.sender].replicaConstants; + && var committer_v := v.hosts[commitMsg.sender].replicaVariables; + && committer_v.view == commitMsg.payload.view + && commitMsg.payload.seqID in committer_v.workingWindow.getActiveSequenceIDs(committer_c) + :: && var committer_c := c.hosts[commitMsg.sender].replicaConstants; + && var committer_v := v.hosts[commitMsg.sender].replicaVariables; + && |Replica.ExtractPreparesFromWorkingWindow(committer_c, committer_v, commitMsg.payload.seqID)| >= c.clusterConfig.AgreementQuorum()) + } + + predicate CertificateComportsWithCommit(c:Constants, certificate:Messages.PreparedCertificate, commitMsg:Message) { + && c.WF() + && commitMsg.payload.Commit? + && certificate.valid(c.clusterConfig, commitMsg.payload.seqID) + && !certificate.empty() + && certificate.prototype().view >= commitMsg.payload.view + && (certificate.prototype().view == commitMsg.payload.view + ==> certificate.prototype().operationWrapper == commitMsg.payload.operationWrapper) + } + + predicate {:opaque} EveryCommitMsgIsRememberedByItsSender(c:Constants, v:Variables) { //TODO: this does not cover Checkpointing + && v.WF(c) + && (forall commitMsg | && commitMsg in v.network.sentMsgs + && commitMsg.payload.Commit? + && IsHonestReplica(c, commitMsg.sender) + && var h_c := c.hosts[commitMsg.sender].replicaConstants; + && var h_v := v.hosts[commitMsg.sender].replicaVariables; + && commitMsg.payload.seqID in h_v.workingWindow.getActiveSequenceIDs(h_c) //TODO: remove when Checkpointing gets enabled + :: && var h_c := c.hosts[commitMsg.sender].replicaConstants; + && var h_v := v.hosts[commitMsg.sender].replicaVariables; + && var certificate := Replica.ExtractCertificateForSeqID(h_c, h_v, commitMsg.payload.seqID); + && CertificateComportsWithCommit(c, certificate, commitMsg) + ) + } + + predicate {:opaque} EveryCommitMsgIsRememberedByVCMsgs(c:Constants, v:Variables) { + && v.WF(c) + && (forall commitMsg, viewChangeMsg | + && commitMsg in v.network.sentMsgs + && viewChangeMsg in v.network.sentMsgs + && commitMsg.payload.Commit? + && viewChangeMsg.payload.ViewChangeMsg? + && viewChangeMsg.sender == commitMsg.sender + && IsHonestReplica(c, commitMsg.sender) + && commitMsg.payload.seqID > viewChangeMsg.payload.lastStableCheckpoint + && commitMsg.payload.view < viewChangeMsg.payload.newView + :: && commitMsg.payload.seqID in viewChangeMsg.payload.certificates + && var certificate := viewChangeMsg.payload.certificates[commitMsg.payload.seqID]; + && CertificateComportsWithCommit(c, certificate, commitMsg) + ) + } + + predicate {:opaque} ViewChangeMsgsFromHonestInNetworkAreValid(c:Constants, v:Variables) { + && v.WF(c) + && (forall viewChangeMsg | + && viewChangeMsg in v.network.sentMsgs + && viewChangeMsg.payload.ViewChangeMsg? + && var replicaIdx := viewChangeMsg.sender; + && IsHonestReplica(c, replicaIdx) + :: && var replicaIdx := viewChangeMsg.sender; + && viewChangeMsg.payload.checked(c.clusterConfig, v.network.sentMsgs)) + } + + predicate {:opaque} TemporarilyDisableCheckpointing(c:Constants, v:Variables) { + && v.WF(c) + && (forall replicaID | && IsHonestReplica(c, replicaID) + :: v.hosts[replicaID].replicaVariables.workingWindow.lastStableCheckpoint == 0) + } + // This predicate states that honest replicas accept the first PrePrepare they receive and vote // with a Prepare message only for it. The lock on Prepare is meant to highlight the fact that // even though a replica can send multiple times a Prepare message for a given Sequence ID for @@ -132,7 +210,8 @@ module Proof { && var prepareMap := v.hosts[replicaIdx].replicaVariables.workingWindow.preparesRcvd; && seqID in prepareMap && sender in prepareMap[seqID] - :: && v.hosts[replicaIdx].replicaVariables.workingWindow.preparesRcvd[seqID][sender].sender == sender + :: && c.clusterConfig.IsReplica(sender) + && v.hosts[replicaIdx].replicaVariables.workingWindow.preparesRcvd[seqID][sender].sender == sender ) } @@ -179,7 +258,7 @@ module Proof { && IsHonestReplica(c, msg.sender) :: && var replicaVariables := v.hosts[msg.sender].replicaVariables; && var replicaConstants := c.hosts[msg.sender].replicaConstants; - && msg.payload.seqID < replicaVariables.workingWindow.lastStableCheckpoint + replicaConstants.clusterConfig.workingWindowSize) + && msg.payload.seqID <= replicaVariables.workingWindow.lastStableCheckpoint + replicaConstants.clusterConfig.workingWindowSize) } predicate {:opaque} EverySentIntraViewMsgIsForAViewLessOrEqualToSenderView(c:Constants, v:Variables) { @@ -207,7 +286,7 @@ module Proof { && commitMsg.payload.operationWrapper == recordedPrePrepare.value.payload.operationWrapper) } - predicate {:opaque} EveryPrepareClientOpMatchesRecordedPrePrepare(c:Constants, v:Variables) { + predicate {:opaque} EveryPrepareMatchesRecordedPrePrepare(c:Constants, v:Variables) { && v.WF(c) && (forall prepareMsg | && prepareMsg in v.network.sentMsgs @@ -216,9 +295,10 @@ module Proof { && var replicaVariables := v.hosts[prepareMsg.sender].replicaVariables; && var replicaConstants := c.hosts[prepareMsg.sender].replicaConstants; && prepareMsg.payload.seqID in replicaVariables.workingWindow.getActiveSequenceIDs(replicaConstants) - && prepareMsg.payload.view == replicaVariables.view + && prepareMsg.payload.view == replicaVariables.view // There might be prepare messages for prior views that the sender no longer records. :: && var recordedPrePrepare := v.hosts[prepareMsg.sender].replicaVariables.workingWindow.prePreparesRcvd[prepareMsg.payload.seqID]; + && var replicaVariables := v.hosts[prepareMsg.sender].replicaVariables; && recordedPrePrepare.Some? && prepareMsg.payload.operationWrapper == recordedPrePrepare.value.payload.operationWrapper) } @@ -274,36 +354,57 @@ module Proof { // :: prePrepare1 == prePrepare2) // } - predicate {:opaque} AllReplicasLiteInv (c: Constants, v:Variables) { + predicate {:opaque} RecordedNewViewMsgsAreValid(c:Constants, v:Variables) { && v.WF(c) - && (forall replicaIdx | 0 <= replicaIdx < |c.hosts| && c.clusterConfig.IsHonestReplica(replicaIdx) - :: Replica.LiteInv(c.hosts[replicaIdx].replicaConstants, v.hosts[replicaIdx].replicaVariables)) + && (forall replicaIdx, newViewMsg | + && c.clusterConfig.IsHonestReplica(replicaIdx) + && var replicaVariables := v.hosts[replicaIdx].replicaVariables; + && newViewMsg in replicaVariables.newViewMsgsRecvd.msgs + :: && newViewMsg.payload.valid(c.clusterConfig) + && c.clusterConfig.PrimaryForView(newViewMsg.payload.newView) == newViewMsg.sender) } predicate Inv(c: Constants, v:Variables) { //&& PrePreparesCarrySameClientOpsForGivenSeqID(c, v) // Do not remove, lite invariant about internal honest Node invariants: - && AllReplicasLiteInv(c, v) + && v.WF(c) + && RecordedNewViewMsgsAreValid(c, v) && RecordedPreparesHaveValidSenderID(c, v) //&& SentPreparesMatchRecordedPrePrepareIfHostInSameView(c, v) && RecordedPrePreparesRecvdCameFromNetwork(c, v) - && RecordedPreparesInAllHostsRecvdCameFromNetwork(c, v) + && RecordedPreparesRecvdCameFromNetwork(c, v) + && RecordedPrePreparesMatchHostView(c, v) && RecordedPreparesMatchHostView(c, v) - && EveryCommitMsgIsSupportedByAQuorumOfPrepares(c, v) + && EveryCommitMsgIsSupportedByAQuorumOfSentPrepares(c, v) + && EveryCommitMsgIsSupportedByAQuorumOfRecordedPrepares(c, v) && RecordedPreparesClientOpsMatchPrePrepare(c, v) && RecordedCommitsClientOpsMatchPrePrepare(c, v) && EverySentIntraViewMsgIsInWorkingWindowOrBefore(c, v) && EverySentIntraViewMsgIsForAViewLessOrEqualToSenderView(c, v) - && EveryPrepareClientOpMatchesRecordedPrePrepare(c, v) + && EveryPrepareMatchesRecordedPrePrepare(c, v) && EveryCommitClientOpMatchesRecordedPrePrepare(c, v) && HonestReplicasLockOnPrepareForGivenView(c, v) && HonestReplicasLockOnCommitForGivenView(c, v) && CommitMsgsFromHonestSendersAgree(c, v) && RecordedCheckpointsRecvdCameFromNetwork(c, v) + && UnCommitableAgreesWithPrepare(c, v) + && UnCommitableAgreesWithRecordedPrePrepare(c, v)//Unfinished proof. + && HonestReplicasLeaveViewsBehind(c, v) + && RecordedNewViewMsgsAreChecked(c, v) + && RecordedViewChangeMsgsCameFromNetwork(c, v) + && OneViewChangeMessageFromReplicaPerView(c, v) + && SentViewChangesMsgsComportWithSentCommits(c, v)//Unfinished proof. This predicate is false. + && EveryCommitMsgIsRememberedByItsSender(c, v)//Unfinished proof. + && RecordedViewChangeMsgsAreValid(c, v) + && ViewChangeMsgsFromHonestInNetworkAreValid(c, v)//Unfinished proof. + && TemporarilyDisableCheckpointing(c, v) + // && NewViewMsgsReflectPriorCommitCertificates(c, v) + // && CommitCertificateEstablishesUncommitableInView(c, v) + // "AllPreparedCertsInWorkingWindowAreValid" } function sentPreparesForSeqID(c: Constants, v:Variables, view:nat, seqID:Messages.SequenceID, - operationWrapper:Messages.OperationWrapper) : set> + operationWrapper:Messages.OperationWrapper) : set requires v.WF(c) { set msg | && msg in v.network.sentMsgs @@ -323,7 +424,7 @@ module Proof { } lemma WlogCommitAgreement(c: Constants, v:Variables, v':Variables, step:Step, - msg1:Network.Message, msg2:Network.Message) + msg1:Message, msg2:Message) requires Inv(c, v) requires NextStep(c, v, v', step) requires msg1 in v'.network.sentMsgs @@ -338,11 +439,11 @@ module Proof { requires IsHonestReplica(c, msg2.sender) ensures msg1.payload.operationWrapper == msg2.payload.operationWrapper { - reveal_RecordedPreparesInAllHostsRecvdCameFromNetwork(); + reveal_RecordedPreparesRecvdCameFromNetwork(); reveal_RecordedPreparesMatchHostView(); reveal_RecordedPreparesClientOpsMatchPrePrepare(); reveal_HonestReplicasLockOnPrepareForGivenView(); - reveal_EveryCommitMsgIsSupportedByAQuorumOfPrepares(); + reveal_EveryCommitMsgIsSupportedByAQuorumOfSentPrepares(); var prepares1 := sentPreparesForSeqID(c, v, msg1.payload.view, msg1.payload.seqID, msg1.payload.operationWrapper); var senders1 := Messages.sendersOf(prepares1); @@ -463,12 +564,12 @@ module Proof { && Replica.NextStep(h_c, h_v, h_v', step.msgOps, h_step) } - lemma HonestPreservesAllReplicasLiteInv(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + lemma HonestPreservesRecordedNewViewMsgsAreValid(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) requires Inv(c, v) requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) - ensures AllReplicasLiteInv(c, v') + ensures RecordedNewViewMsgsAreValid(c, v') { - reveal_AllReplicasLiteInv(); + reveal_RecordedNewViewMsgsAreValid(); } lemma HonestPreservesRecordedPreparesHaveValidSenderID(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) @@ -499,12 +600,12 @@ module Proof { } } - lemma HonestPreservesRecordedPreparesInAllHostsRecvdCameFromNetwork(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + lemma HonestPreservesRecordedPreparesRecvdCameFromNetwork(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) requires Inv(c, v) requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) - ensures RecordedPreparesInAllHostsRecvdCameFromNetwork(c, v') + ensures RecordedPreparesRecvdCameFromNetwork(c, v') { - reveal_RecordedPreparesInAllHostsRecvdCameFromNetwork(); + reveal_RecordedPreparesRecvdCameFromNetwork(); if (h_step.AdvanceWorkingWindowStep?) { h_v.workingWindow.reveal_Shift(); @@ -527,13 +628,13 @@ module Proof { } } - lemma AlwaysPreservesEveryCommitMsgIsSupportedByAQuorumOfPrepares(c: Constants, v:Variables, v':Variables, step:Step) + lemma AlwaysPreservesEveryCommitMsgIsSupportedByAQuorumOfSentPrepares(c: Constants, v:Variables, v':Variables, step:Step) requires Inv(c, v) requires NextStep(c, v, v', step) - ensures EveryCommitMsgIsSupportedByAQuorumOfPrepares(c, v') + ensures EveryCommitMsgIsSupportedByAQuorumOfSentPrepares(c, v') { - reveal_EveryCommitMsgIsSupportedByAQuorumOfPrepares(); - // A proof of EveryCommitMsgIsSupportedByAQuorumOfPrepares, + reveal_EveryCommitMsgIsSupportedByAQuorumOfSentPrepares(); + // A proof of EveryCommitMsgIsSupportedByAQuorumOfSentPrepares, // by selecting an arbitrary commitMsg instance forall commitMsg | && commitMsg in v'.network.sentMsgs && commitMsg.payload.Commit? @@ -547,7 +648,7 @@ module Proof { commitMsg.payload.seqID, commitMsg.payload.operationWrapper)); Library.SubsetCardinality(senders, senders'); } else { // the commitMsg is being sent in the current step - reveal_RecordedPreparesInAllHostsRecvdCameFromNetwork(); + reveal_RecordedPreparesRecvdCameFromNetwork(); reveal_RecordedPreparesMatchHostView(); reveal_RecordedPreparesClientOpsMatchPrePrepare(); var prepares := sentPreparesForSeqID(c, v, commitMsg.payload.view, @@ -570,6 +671,70 @@ module Proof { } } + lemma HonestPreservesEveryCommitMsgIsSupportedByAQuorumOfRecordedPrepares(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + ensures EveryCommitMsgIsSupportedByAQuorumOfRecordedPrepares(c, v') + { + h_v.workingWindow.reveal_Shift(); + reveal_RecordedPreparesRecvdCameFromNetwork(); + reveal_EveryCommitMsgIsSupportedByAQuorumOfRecordedPrepares(); + reveal_TemporarilyDisableCheckpointing(); + reveal_EverySentIntraViewMsgIsForAViewLessOrEqualToSenderView(); + reveal_EverySentIntraViewMsgIsInWorkingWindowOrBefore(); + + if (h_step.SendCommitStep?) { + forall commitMsg | && commitMsg in v'.network.sentMsgs + && commitMsg.payload.Commit? + && IsHonestReplica(c, commitMsg.sender) + && var h_c := c.hosts[commitMsg.sender].replicaConstants; + && var h_v' := v'.hosts[commitMsg.sender].replicaVariables; + && h_v'.view == commitMsg.payload.view + && commitMsg.payload.seqID in h_v'.workingWindow.getActiveSequenceIDs(h_c) + ensures && var h_c := c.hosts[commitMsg.sender].replicaConstants; + && var h_v' := v'.hosts[commitMsg.sender].replicaVariables; + && |Replica.ExtractPreparesFromWorkingWindow(h_c, h_v', commitMsg.payload.seqID)| >= c.clusterConfig.AgreementQuorum() + { + var h_c := c.hosts[commitMsg.sender].replicaConstants; + var h_v' := v'.hosts[commitMsg.sender].replicaVariables; + if(commitMsg !in v.network.sentMsgs) { + CountPrepareMessages2(c, v, commitMsg.sender, h_c, h_v, h_step.seqID); + } + } + assert EveryCommitMsgIsSupportedByAQuorumOfRecordedPrepares(c, v'); + } else if(h_step.RecvPrepareStep?) { + var h_c := c.hosts[step.id].replicaConstants; + var h_v' := v'.hosts[step.id].replicaVariables; + forall commitMsg | && commitMsg in v'.network.sentMsgs + && commitMsg.payload.Commit? + && IsHonestReplica(c, commitMsg.sender) + && var committer_c := c.hosts[commitMsg.sender].replicaConstants; + && var committer_v' := v'.hosts[commitMsg.sender].replicaVariables; + && committer_v'.view == commitMsg.payload.view + && commitMsg.payload.seqID in committer_v'.workingWindow.getActiveSequenceIDs(h_c) + ensures && var committer_c := c.hosts[commitMsg.sender].replicaConstants; + && var committer_v' := v'.hosts[commitMsg.sender].replicaVariables; + && |Replica.ExtractPreparesFromWorkingWindow(committer_c, committer_v', commitMsg.payload.seqID)| >= c.clusterConfig.AgreementQuorum() + { + var seqID := commitMsg.payload.seqID; + var committer_c := c.hosts[commitMsg.sender].replicaConstants; + var committer_v := v.hosts[commitMsg.sender].replicaVariables; + var committer_v' := v'.hosts[commitMsg.sender].replicaVariables; + if(commitMsg.sender == step.id) { + forall p | p in Replica.ExtractPreparesFromWorkingWindow(committer_c, committer_v, seqID) + ensures p in Replica.ExtractPreparesFromWorkingWindow(committer_c, committer_v', seqID) { + assert p.sender in committer_v'.workingWindow.preparesRcvd[seqID]; // Trigger + } + Library.SubsetCardinality(Replica.ExtractPreparesFromWorkingWindow(committer_c, committer_v, seqID), + Replica.ExtractPreparesFromWorkingWindow(committer_c, committer_v', seqID)); + } + } + assert EveryCommitMsgIsSupportedByAQuorumOfRecordedPrepares(c, v'); + } else { + assert EveryCommitMsgIsSupportedByAQuorumOfRecordedPrepares(c, v'); + } + } + lemma HonestPreservesRecordedPreparesClientOpsMatchPrePrepare(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) requires Inv(c, v) requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) @@ -611,13 +776,61 @@ module Proof { } } - lemma HonestPreservesEveryPrepareClientOpMatchesRecordedPrePrepare(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + lemma CountPrepareMessagesInWorkingWindow(c:Constants, v:Variables, replicaId:HostId, seqID:Messages.SequenceID) + requires v.WF(c) + requires RecordedPreparesHaveValidSenderID(c, v) + requires IsHonestReplica(c, replicaId) + requires seqID in v.hosts[replicaId].replicaVariables.workingWindow.getActiveSequenceIDs(c.hosts[replicaId].replicaConstants) + ensures |v.hosts[replicaId].replicaVariables.workingWindow.preparesRcvd[seqID].Values| + == |v.hosts[replicaId].replicaVariables.workingWindow.preparesRcvd[seqID].Keys| + { + reveal_RecordedPreparesHaveValidSenderID(); + var proofSet := v.hosts[replicaId].replicaVariables.workingWindow.preparesRcvd[seqID]; + forall sender | sender in proofSet.Keys ensures proofSet[sender].sender == sender { + assert c.clusterConfig.IsReplica(sender); + } + CountPrepareMessages(proofSet); + // assert forall sender | && sender in v.hosts[replicaId].replicaVariables.workingWindow.preparesRcvd + // :: && c.clusterConfig.IsReplica(sender) + // && v.hosts[replicaId].replicaVariables.workingWindow.preparesRcvd[seqID][sender].sender == sender; + } + + lemma CountPrepareMessages2(c:Constants, v:Variables, replicaID:HostId, h_c:Replica.Constants, h_v:Replica.Variables, seqID:Messages.SequenceID) + requires v.WF(c) + requires IsHonestReplica(c, replicaID) + requires h_c == c.hosts[replicaID].replicaConstants + requires h_v == v.hosts[replicaID].replicaVariables + requires seqID in h_v.workingWindow.getActiveSequenceIDs(h_c) + requires RecordedPreparesHaveValidSenderID(c, v) + ensures |Replica.ExtractPreparesFromWorkingWindow(h_c, h_v, seqID)| == |h_v.workingWindow.preparesRcvd[seqID]| + { + var senders := h_v.workingWindow.preparesRcvd[seqID].Keys; + var f := sender requires sender in senders => h_v.workingWindow.preparesRcvd[seqID][sender]; + forall x, y | && x in senders + && y in senders + && f(x) == f(y) + ensures x == y { + reveal_RecordedPreparesHaveValidSenderID(); + assert c.clusterConfig.IsReplica(x); // Trigger + assert c.clusterConfig.IsReplica(y); // Trigger + } + var filtered := set x | x in senders :: f(x); + var filtered2 := set x | x in senders :: f(x); + assert filtered == filtered2; + + MappedSetCardinality(senders, f, filtered); // This is a Dafny triggering problem. + assert |senders| == |filtered|; + assert h_v.workingWindow.preparesRcvd[seqID].Keys == senders; + assert |h_v.workingWindow.preparesRcvd[seqID]| == |h_v.workingWindow.preparesRcvd[seqID].Keys|; + assert Replica.ExtractPreparesFromWorkingWindow(h_c, h_v, seqID) == filtered; + } + + lemma HonestPreservesEveryPrepareMatchesRecordedPrePrepare(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) requires Inv(c, v) requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) - ensures EveryPrepareClientOpMatchesRecordedPrePrepare(c, v') - + ensures EveryPrepareMatchesRecordedPrePrepare(c, v') { - reveal_EveryPrepareClientOpMatchesRecordedPrePrepare(); + reveal_EveryPrepareMatchesRecordedPrePrepare(); reveal_EverySentIntraViewMsgIsInWorkingWindowOrBefore(); reveal_EverySentIntraViewMsgIsForAViewLessOrEqualToSenderView(); h_v.workingWindow.reveal_Shift(); @@ -656,7 +869,7 @@ module Proof { ensures HonestReplicasLockOnPrepareForGivenView(c, v') { reveal_HonestReplicasLockOnPrepareForGivenView(); - reveal_EveryPrepareClientOpMatchesRecordedPrePrepare(); + reveal_EveryPrepareMatchesRecordedPrePrepare(); } lemma HonestPreservesHonestReplicasLockOnCommitForGivenView(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) @@ -709,6 +922,188 @@ module Proof { h_v.workingWindow.reveal_Shift(); } + datatype HonestInfo = HonestInfo(h_v:Replica.Variables, h_step:Replica.Step) | NotHonest() + + lemma TriviallyPreserveUnCommitableAgreesWithPrepare(c: Constants, v:Variables, v':Variables, step:Step, info:HonestInfo) + requires Inv(c, v) + requires match(info) { + case HonestInfo(h_v, h_step) => (&& HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + && !h_step.SendPrepareStep? + && !h_step.LeaveViewStep?) + case NotHonest() => (|| (NextStep(c, v, v', step) && c.clusterConfig.IsFaultyReplica(step.id)) + || (NextStep(c, v, v', step) && c.clusterConfig.IsClient(step.id))) + } + ensures UnCommitableAgreesWithPrepare(c, v') + { + reveal_UnCommitableAgreesWithPrepare(); + forall prepareMsg:Message, + priorView:nat, + priorOperationWrapper:Messages.OperationWrapper + | && prepareMsg.payload.Prepare? + && priorView < prepareMsg.payload.view + && c.clusterConfig.IsHonestReplica(prepareMsg.sender) + && priorOperationWrapper != prepareMsg.payload.operationWrapper + && prepareMsg in v'.network.sentMsgs + ensures UnCommitableInView(c, v', prepareMsg.payload.seqID, priorView, priorOperationWrapper) { + assert UnCommitableInView(c, v, prepareMsg.payload.seqID, priorView, priorOperationWrapper); + assert ReplicasThatCanCommitInView(c, v', prepareMsg.payload.seqID, priorView, priorOperationWrapper) + == ReplicasThatCanCommitInView(c, v, prepareMsg.payload.seqID, priorView, priorOperationWrapper); + // assert |ReplicasThatCanCommitInView(c, v', prepareMsg.payload.seqID, priorView, priorOperationWrapper)| + // == |ReplicasThatCanCommitInView(c, v, prepareMsg.payload.seqID, priorView, priorOperationWrapper)|; + } + } + + lemma TriviallyPreserveUnCommitableAgreesWithRecordedPrePrepare(c: Constants, v:Variables, v':Variables, step:Step, info:HonestInfo) + requires Inv(c, v) + requires match(info) { + case HonestInfo(h_v, h_step) => (&& HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + && !h_step.RecvPrePrepareStep? + && !h_step.LeaveViewStep? + && !h_step.SendPrePrepareStep?) + case NotHonest() => (|| (NextStep(c, v, v', step) && c.clusterConfig.IsFaultyReplica(step.id)) + || (NextStep(c, v, v', step) && c.clusterConfig.IsClient(step.id))) + } + ensures UnCommitableAgreesWithRecordedPrePrepare(c, v') + { + if info.HonestInfo? + { + info.h_v.workingWindow.reveal_Shift(); + } + reveal_UnCommitableAgreesWithRecordedPrePrepare(); + forall replicaIdx, seqID, priorView:nat, priorOperationWrapper:Messages.OperationWrapper | + && IsHonestReplica(c, replicaIdx) + && var replicaVariables := v'.hosts[replicaIdx].replicaVariables; + && var replicaConstants := c.hosts[replicaIdx].replicaConstants; + && seqID in replicaVariables.workingWindow.getActiveSequenceIDs(replicaConstants) + && replicaVariables.workingWindow.prePreparesRcvd[seqID].Some? + && var prePrepareMsg := replicaVariables.workingWindow.prePreparesRcvd[seqID].value; + && priorOperationWrapper != prePrepareMsg.payload.operationWrapper + && priorView < prePrepareMsg.payload.view + ensures && var prePrepareMsg := v'.hosts[replicaIdx].replicaVariables.workingWindow.prePreparesRcvd[seqID].value; + && UnCommitableInView(c, v', prePrepareMsg.payload.seqID, priorView, priorOperationWrapper) { + var prePrepareMsg := v'.hosts[replicaIdx].replicaVariables.workingWindow.prePreparesRcvd[seqID].value; + assert UnCommitableInView(c, v, prePrepareMsg.payload.seqID, priorView, priorOperationWrapper); + assert ReplicasThatCanCommitInView(c, v', prePrepareMsg.payload.seqID, priorView, priorOperationWrapper) + == ReplicasThatCanCommitInView(c, v, prePrepareMsg.payload.seqID, priorView, priorOperationWrapper); + } + } + + lemma HonestLeaveViewStepPreservesUnCommitableAgreesWithRecordedPrePrepare(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + requires h_step.LeaveViewStep? + ensures UnCommitableAgreesWithRecordedPrePrepare(c, v') + { + reveal_UnCommitableAgreesWithRecordedPrePrepare(); + forall replicaIdx, seqID, priorView:nat, priorOperationWrapper:Messages.OperationWrapper | + && IsHonestReplica(c, replicaIdx) + && var replicaVariables := v'.hosts[replicaIdx].replicaVariables; + && var replicaConstants := c.hosts[replicaIdx].replicaConstants; + && seqID in replicaVariables.workingWindow.getActiveSequenceIDs(replicaConstants) + && replicaVariables.workingWindow.prePreparesRcvd[seqID].Some? + && var prePrepareMsg := replicaVariables.workingWindow.prePreparesRcvd[seqID].value; + && priorOperationWrapper != prePrepareMsg.payload.operationWrapper + && priorView < prePrepareMsg.payload.view + ensures && var prePrepareMsg := v'.hosts[replicaIdx].replicaVariables.workingWindow.prePreparesRcvd[seqID].value; + && UnCommitableInView(c, v', prePrepareMsg.payload.seqID, priorView, priorOperationWrapper) { + var prePrepareMsg := v'.hosts[replicaIdx].replicaVariables.workingWindow.prePreparesRcvd[seqID].value; + assert UnCommitableInView(c, v, prePrepareMsg.payload.seqID, priorView, priorOperationWrapper); + Library.SubsetCardinality(ReplicasThatCanCommitInView(c, v', prePrepareMsg.payload.seqID, priorView, priorOperationWrapper), + ReplicasThatCanCommitInView(c, v, prePrepareMsg.payload.seqID, priorView, priorOperationWrapper)); + + } + } + + lemma HonestLeaveViewStepPreservesUnCommitableAgreesWithPrepare(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + requires h_step.LeaveViewStep? + ensures UnCommitableAgreesWithPrepare(c, v') + { + reveal_UnCommitableAgreesWithPrepare(); + forall prepareMsg:Message, + priorView:nat, + priorOperationWrapper:Messages.OperationWrapper + | && prepareMsg.payload.Prepare? + && priorView < prepareMsg.payload.view + && c.clusterConfig.IsHonestReplica(prepareMsg.sender) + && priorOperationWrapper != prepareMsg.payload.operationWrapper + && prepareMsg in v'.network.sentMsgs + ensures UnCommitableInView(c, v', prepareMsg.payload.seqID, priorView, priorOperationWrapper) { + assert UnCommitableInView(c, v, prepareMsg.payload.seqID, priorView, priorOperationWrapper); + // assert ReplicasThatCanCommitInView(c, v', prepareMsg.payload.seqID, priorView, priorOperationWrapper) + // <= ReplicasThatCanCommitInView(c, v, prepareMsg.payload.seqID, priorView, priorOperationWrapper); + // assert |ReplicasThatCanCommitInView(c, v', prepareMsg.payload.seqID, priorView, priorOperationWrapper)| + // <= |ReplicasThatCanCommitInView(c, v, prepareMsg.payload.seqID, priorView, priorOperationWrapper)|; + Library.SubsetCardinality(ReplicasThatCanCommitInView(c, v', prepareMsg.payload.seqID, priorView, priorOperationWrapper), + ReplicasThatCanCommitInView(c, v, prepareMsg.payload.seqID, priorView, priorOperationWrapper)); + } + } + + lemma HonestSendPrepareStepPreservesUnCommitableAgreesWithPrepare(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + requires h_step.SendPrepareStep? + ensures UnCommitableAgreesWithPrepare(c, v') + { + /// + // reveal_EveryCommitClientOpMatchesRecordedPrePrepare(); + // reveal_RecordedNewViewMsgsAreValid(); + // reveal_RecordedPreparesHaveValidSenderID(); + reveal_RecordedPrePreparesRecvdCameFromNetwork(); + // reveal_RecordedPreparesRecvdCameFromNetwork(); + // reveal_RecordedPreparesMatchHostView(); + // reveal_RecordedPreparesClientOpsMatchPrePrepare(); + // reveal_RecordedCommitsClientOpsMatchPrePrepare(); + // reveal_EverySentIntraViewMsgIsInWorkingWindowOrBefore(); + // reveal_EverySentIntraViewMsgIsForAViewLessOrEqualToSenderView(); + // reveal_EveryPrepareMatchesRecordedPrePrepare(); + // reveal_EveryCommitClientOpMatchesRecordedPrePrepare(); + // reveal_HonestReplicasLockOnPrepareForGivenView(); + // reveal_HonestReplicasLockOnCommitForGivenView(); + // reveal_CommitMsgsFromHonestSendersAgree(); + // reveal_RecordedCheckpointsRecvdCameFromNetwork(); + // reveal_HonestReplicasLockOnCommitForGivenView(); + // reveal_EveryCommitMsgIsSupportedByAQuorumOfSentPrepares(); + // h_v.workingWindow.reveal_Shift(); + reveal_UnCommitableAgreesWithRecordedPrePrepare(); + reveal_RecordedPrePreparesMatchHostView(); + /// + + reveal_UnCommitableAgreesWithPrepare(); + //TODO: minimise proof + forall prepareMsg:Message, + priorView:nat, + priorOperationWrapper:Messages.OperationWrapper + | && prepareMsg.payload.Prepare? + && priorView < prepareMsg.payload.view + && c.clusterConfig.IsHonestReplica(prepareMsg.sender) + && priorOperationWrapper != prepareMsg.payload.operationWrapper + && prepareMsg in v'.network.sentMsgs + ensures UnCommitableInView(c, v', prepareMsg.payload.seqID, priorView, priorOperationWrapper) { + if prepareMsg in v.network.sentMsgs { + assert UnCommitableInView(c, v, prepareMsg.payload.seqID, priorView, priorOperationWrapper); + assert ReplicasThatCanCommitInView(c, v', prepareMsg.payload.seqID, priorView, priorOperationWrapper) + == ReplicasThatCanCommitInView(c, v, prepareMsg.payload.seqID, priorView, priorOperationWrapper); + } else { + assert h_v.workingWindow.prePreparesRcvd[prepareMsg.payload.seqID].Some?; + var prePrepareMsg := h_v.workingWindow.prePreparesRcvd[prepareMsg.payload.seqID].value; + assert prePrepareMsg.payload.seqID == prepareMsg.payload.seqID; + assert UnCommitableInView(c, v, prePrepareMsg.payload.seqID, priorView, priorOperationWrapper); + assert UnCommitableInView(c, v, prepareMsg.payload.seqID, priorView, priorOperationWrapper); + assert ReplicasThatCanCommitInView(c, v', prepareMsg.payload.seqID, priorView, priorOperationWrapper) + == ReplicasThatCanCommitInView(c, v, prepareMsg.payload.seqID, priorView, priorOperationWrapper); + } + //END TODO + + // assert |ReplicasThatCanCommitInView(c, v', prepareMsg.payload.seqID, priorView, priorOperationWrapper)| + // == |ReplicasThatCanCommitInView(c, v, prepareMsg.payload.seqID, priorView, priorOperationWrapper)|; + // assert |ReplicasThatCanCommitInView(c, v, prepareMsg.payload.seqID, priorView, priorOperationWrapper)| < c.clusterConfig.AgreementQuorum(); + } + } + + /// End Of Case Splitting + lemma QuorumOfPreparesInNetworkMonotonic(c: Constants, v:Variables, v':Variables, step:Step) requires NextStep(c, v, v', step) ensures (forall view, seqID, clientOp | QuorumOfPreparesInNetwork(c, v, view, seqID, clientOp) @@ -723,6 +1118,1088 @@ module Proof { } } + predicate AgreementQuorumOfMessages(c:Constants, msgs:set) { + && c.WF() + && |msgs| >= c.clusterConfig.AgreementQuorum() + && Messages.UniqueSenders(msgs) + } + + predicate isCommitQuorum(c:Constants, + v:Variables, + view:nat, + seqID:Messages.SequenceID, + operationWrapper:Messages.OperationWrapper, + sentCommits:set) + requires v.WF(c) + { + && sentCommits <= v.network.sentMsgs + && AgreementQuorumOfMessages(c, sentCommits) + && (forall msg | msg in sentCommits + :: && msg.payload.Commit? + && msg.payload.view == view + && msg.payload.seqID == seqID + && msg.payload.operationWrapper == operationWrapper + && msg.sender in getAllReplicas(c)) + } + + lemma UniqueSendersCardinality(msgs:set) + requires Messages.UniqueSenders(msgs) + ensures |Messages.sendersOf(msgs)| == |msgs| + { + Messages.reveal_UniqueSenders(); + if |msgs| > 0 { + var m :| m in msgs; + var subMsgs := msgs - {m}; + UniqueSendersCardinality(subMsgs); + assert Messages.sendersOf(msgs) == Messages.sendersOf(subMsgs) + {m.sender}; + } + } + + predicate ReplicaSentCommit(c:Constants, + v:Variables, + seqID:Messages.SequenceID, + view:nat, + operationWrapper:Messages.OperationWrapper, + replica:HostIdentifiers.HostId) + requires v.WF(c) + { + && c.clusterConfig.IsHonestReplica(replica) + && Network.Message(replica, + Messages.Commit(view, + seqID, + operationWrapper)) in v.network.sentMsgs + } + + predicate ReplicasInViewOrLower(c:Constants, + v:Variables, + seqID:Messages.SequenceID, + view:nat, + operationWrapper:Messages.OperationWrapper, + replica:HostIdentifiers.HostId) + requires v.WF(c) + { + && c.clusterConfig.IsHonestReplica(replica) + && v.hosts[replica].replicaVariables.view <= view + } + + function ReplicasThatCanCommitInView(c:Constants, + v:Variables, + seqID:Messages.SequenceID, + view:nat, + operationWrapper:Messages.OperationWrapper) + : set + requires v.WF(c) + { + set replica | replica in getAllReplicas(c) && + (|| ReplicaSentCommit(c, v, seqID, view, operationWrapper, replica) + || ReplicasInViewOrLower(c, v, seqID, view, operationWrapper, replica) + || c.clusterConfig.IsFaultyReplica(replica)) + } + + predicate UnCommitableInView(c:Constants, + v:Variables, + seqID:Messages.SequenceID, + view:nat, + operationWrapper:Messages.OperationWrapper) { + && v.WF(c) + && |ReplicasThatCanCommitInView(c, v, seqID, view, operationWrapper)| < c.clusterConfig.AgreementQuorum() + } + + // UnCommitable agrees with Prepares. + predicate {:opaque} UnCommitableAgreesWithPrepare(c:Constants, v:Variables) { + && v.WF(c) + && (forall prepareMsg:Message, + priorView:nat, + priorOperationWrapper:Messages.OperationWrapper + | && prepareMsg.payload.Prepare? + && priorView < prepareMsg.payload.view + && c.clusterConfig.IsHonestReplica(prepareMsg.sender) + && priorOperationWrapper != prepareMsg.payload.operationWrapper + && prepareMsg in v.network.sentMsgs + :: UnCommitableInView(c, v, prepareMsg.payload.seqID, priorView, priorOperationWrapper)) + } + + predicate {:opaque} UnCommitableAgreesWithRecordedPrePrepare(c:Constants, v:Variables) { + && v.WF(c) + && (forall replicaIdx, seqID, priorView:nat, priorOperationWrapper:Messages.OperationWrapper | + && IsHonestReplica(c, replicaIdx) + && var replicaVariables := v.hosts[replicaIdx].replicaVariables; + && var replicaConstants := c.hosts[replicaIdx].replicaConstants; + && seqID in replicaVariables.workingWindow.getActiveSequenceIDs(replicaConstants) + && replicaVariables.workingWindow.prePreparesRcvd[seqID].Some? + && var prePrepareMsg := replicaVariables.workingWindow.prePreparesRcvd[seqID].value; + && priorOperationWrapper != prePrepareMsg.payload.operationWrapper + && priorView < prePrepareMsg.payload.view + :: && var prePrepareMsg := v.hosts[replicaIdx].replicaVariables.workingWindow.prePreparesRcvd[seqID].value; + && UnCommitableInView(c, v, prePrepareMsg.payload.seqID, priorView, priorOperationWrapper)) + } + + predicate {:opaque} HonestReplicasLeaveViewsBehind(c:Constants, v:Variables) { + && v.WF(c) + && (forall viewChangeMsg | && viewChangeMsg in v.network.sentMsgs + && viewChangeMsg.payload.ViewChangeMsg? + && IsHonestReplica(c, viewChangeMsg.sender) + :: && var replicaVariables := v.hosts[viewChangeMsg.sender].replicaVariables; + && replicaVariables.view >= viewChangeMsg.payload.newView) + } + + predicate {:opaque} RecordedNewViewMsgsAreChecked(c:Constants, v:Variables) { + && v.WF(c) + && (forall replicaIdx, newViewMsg | && IsHonestReplica(c, replicaIdx) + && var replicaVariables := v.hosts[replicaIdx].replicaVariables; + && newViewMsg in replicaVariables.newViewMsgsRecvd.msgs + :: && newViewMsg.payload.vcMsgs.msgs <= v.network.sentMsgs + && Messages.ValidNewViewMsg(c.clusterConfig, newViewMsg)) + } + + predicate {:opaque} RecordedPrePreparesMatchHostView(c:Constants, v:Variables) { + && v.WF(c) + && (forall observer, seqID, sender | + && IsHonestReplica(c, observer) + && c.clusterConfig.IsReplica(sender) + && var replicaVars := v.hosts[observer].replicaVariables; + && seqID in replicaVars.workingWindow.preparesRcvd + && replicaVars.workingWindow.prePreparesRcvd[seqID].Some? + :: && var replicaVars := v.hosts[observer].replicaVariables; + && replicaVars.view == replicaVars.workingWindow.prePreparesRcvd[seqID].value.payload.view) + } + + predicate {:opaque} RecordedViewChangeMsgsCameFromNetwork(c:Constants, v:Variables) { + && v.WF(c) + && (forall replicaIdx, viewChangeMsg | + && IsHonestReplica(c, replicaIdx) + && var replicaVariables := v.hosts[replicaIdx].replicaVariables; + && viewChangeMsg in replicaVariables.viewChangeMsgsRecvd.msgs + :: viewChangeMsg in v.network.sentMsgs) + } + + predicate {:opaque} OneViewChangeMessageFromReplicaPerView(c:Constants, v:Variables) { + && v.WF(c) + && (forall msg1, msg2 | + && msg1 in v.network.sentMsgs + && msg2 in v.network.sentMsgs + && msg1.sender == msg2.sender + && IsHonestReplica(c, msg1.sender) + && msg1.payload.ViewChangeMsg? + && msg2.payload.ViewChangeMsg? + && msg1.payload.newView == msg2.payload.newView + :: msg1 == msg2) + } + + predicate {:opaque} RecordedViewChangeMsgsAreValid(c:Constants, v:Variables) { + && v.WF(c) + && (forall replicaIdx, viewChangeMsg | + && IsHonestReplica(c, replicaIdx) + && var replicaVariables := v.hosts[replicaIdx].replicaVariables; + && viewChangeMsg in replicaVariables.viewChangeMsgsRecvd.msgs + :: && var replicaConstants := c.hosts[replicaIdx].replicaConstants; + && Replica.ValidViewChangeMsg(replicaConstants, + viewChangeMsg, + v.network.sentMsgs)) + } + + // This predicate is false and will be refactored to SentViewChangesMsgsComportWithUncommitableInView + predicate {:opaque} SentViewChangesMsgsComportWithSentCommits(c:Constants, v:Variables) { + && true + // && v.WF(c) + // && (forall viewChangeMsg, commitMsg | + // && viewChangeMsg in v.network.sentMsgs + // && commitMsg in v.network.sentMsgs + // && viewChangeMsg.payload.ViewChangeMsg? + // && commitMsg.payload.Commit? + // && commitMsg.payload.view <= viewChangeMsg.payload.newView + // && commitMsg.sender == viewChangeMsg.sender + // //TODO: add Shift consequences (this works only if no one advances the WW) + // && IsHonestReplica(c, viewChangeMsg.sender) + // :: && commitMsg.payload.seqID in viewChangeMsg.payload.certificates + // && var certificate := viewChangeMsg.payload.certificates[commitMsg.payload.seqID]; + // && certificate.valid(c.clusterConfig, commitMsg.payload.seqID) + // && !certificate.empty() + // && certificate.prototype().view >= commitMsg.payload.view + // // && (commitMsg.payload.view == viewChangeMsg.payload.newView) ==> + // // certificate.prototype().operationWrapper == commitMsg.payload.operationWrapper + // ) + } + //TODO: refactor + predicate {:opaque} SentViewChangesMsgsComportWithUncommitableInView(c:Constants, v:Variables) { + && true + // && v.WF(c) + // && (forall viewChangeMsg, + // seqID:Messages.SequenceID, + // view:nat, + // operationWrapper:Messages.OperationWrapper | + // && viewChangeMsg in v.network.sentMsgs + // && viewChangeMsg.payload.ViewChangeMsg? + // && IsHonestReplica(c, viewChangeMsg.sender) + // && view < viewChangeMsg.payload.newView + // && var certificate := viewChangeMsg.payload.certificates[seqID]; + // && !certificate.empty() + // && operationWrapper != certificate.prototype().operationWrapper + // :: && UnCommitableInView(c, v, seqID, view, operationWrapper)) + } + +//TODO: write a predicate Prepare matches Commit + lemma GetPrepareFromHonestSenderForCommit(c:Constants, v:Variables, commitMsg:Message) + returns (prepare:Message) + requires Inv(c, v) + requires commitMsg.payload.Commit? + requires commitMsg in v.network.sentMsgs + requires c.clusterConfig.IsHonestReplica(commitMsg.sender) + ensures prepare.payload.Prepare? + ensures c.clusterConfig.IsHonestReplica(prepare.sender) + ensures prepare in v.network.sentMsgs + ensures prepare.payload.view == commitMsg.payload.view + ensures prepare.payload.seqID == commitMsg.payload.seqID + ensures prepare.payload.operationWrapper == commitMsg.payload.operationWrapper + { + reveal_EveryCommitMsgIsSupportedByAQuorumOfSentPrepares(); + var prepares := sentPreparesForSeqID(c, v, commitMsg.payload.view, commitMsg.payload.seqID, commitMsg.payload.operationWrapper); + prepare := GetMsgFromHonestSender(c, prepares); + } + + function FaultyReplicas(c: Constants) : (faulty:set) + requires c.WF() + { + set sender | 0 <= sender < c.clusterConfig.N() && !IsHonestReplica(c, sender) + } + + lemma CountFaultyReplicas(c: Constants) + requires c.WF() + ensures |FaultyReplicas(c)| <= c.clusterConfig.F() + { + var count := 0; + var f := c.clusterConfig.F(); + var n := c.clusterConfig.N(); + while(count < n) + invariant count <= n + invariant |set sender | 0 <= sender < count && !IsHonestReplica(c, sender)| == if count <= f then count + else f + { + var oldSet := set sender | 0 <= sender < count && !IsHonestReplica(c, sender); + var newSet := set sender | 0 <= sender < count + 1 && !IsHonestReplica(c, sender); + if(count + 1 <= f) { + assert newSet == oldSet + {count}; + } else { + assert newSet == oldSet; + } + count := count + 1; + } + } + + lemma FindHonestNode(c: Constants, replicas:set) + returns (honest:HostIdentifiers.HostId) + requires c.WF() + requires |replicas| >= c.clusterConfig.ByzantineSafeQuorum() + requires replicas <= getAllReplicas(c) + ensures IsHonestReplica(c, honest) + ensures honest in replicas + { + var honestReplicas := replicas * HonestReplicas(c); + CountFaultyReplicas(c); + if(|honestReplicas| == 0) { + Library.SubsetCardinality(replicas, FaultyReplicas(c)); + assert false; //Proof by contradiction + } + + var result :| result in honestReplicas; + honest := result; + } + + lemma GetMsgFromHonestSender(c:Constants, quorum:set) + returns (message:Message) + requires c.WF() + requires |Messages.sendersOf(quorum)| >= c.clusterConfig.AgreementQuorum() + requires Messages.sendersOf(quorum) <= getAllReplicas(c) + ensures c.clusterConfig.IsHonestReplica(message.sender) + ensures message in quorum + { + var senders := Messages.sendersOf(quorum); + var honestSender := FindHonestNode(c, senders); + var honest :| honest in quorum && honest.sender == honestSender; + message := honest; + } + + lemma FindHonestCommitInQuorum(c:Constants, + v:Variables, + seqID:Messages.SequenceID, + view:nat, + commits:set, + operationWrapper:Messages.OperationWrapper) + returns (honestCommit:Message) + requires Inv(c, v) + requires isCommitQuorum(c, v, view, seqID, operationWrapper, commits) + ensures honestCommit in commits + ensures IsHonestReplica(c, honestCommit.sender) + { + var senders := Messages.sendersOf(commits); + UniqueSendersCardinality(commits); + var honestSender := FindHonestNode(c, senders); + var honest :| honest in commits && honest.sender == honestSender; + honestCommit := honest; + } + + lemma CommitQuorumAgree(c:Constants, v:Variables) + requires Inv(c, v) + ensures CommitQuorumsAgreeOnOperation(c, v) + { + forall seqID:Messages.SequenceID, + view1:nat, + view2:nat, + commits1:set, + commits2:set, + operationWrapper1:Messages.OperationWrapper, + operationWrapper2:Messages.OperationWrapper + | && isCommitQuorum(c, v, view1, seqID, operationWrapper1, commits1) + && isCommitQuorum(c, v, view2, seqID, operationWrapper2, commits2) + ensures (operationWrapper1 == operationWrapper2) { + if view1 == view2 { + // var honestCommit1 := FindHonestCommitInQuorum(); + var commit1 := FindHonestCommitInQuorum(c, v, seqID, view1, commits1, operationWrapper1); + var commit2 := FindHonestCommitInQuorum(c, v, seqID, view2, commits2, operationWrapper2); + assert commit1 in v.network.sentMsgs; // Trigger for CommitMsgsFromHonestSendersAgree + assert commit2 in v.network.sentMsgs; // Trigger for CommitMsgsFromHonestSendersAgree + reveal_CommitMsgsFromHonestSendersAgree(); + assert commit1.payload.operationWrapper == commit2.payload.operationWrapper; + assert operationWrapper1 == operationWrapper2; + } else if view1 < view2 { + CommitQuorumAgreeDifferentViews(c, v, seqID, view1, view2, commits1, commits2, operationWrapper1, operationWrapper2); + } else { + CommitQuorumAgreeDifferentViews(c, v, seqID, view2, view1, commits2, commits1, operationWrapper2, operationWrapper1); + } + } + } + + lemma CommitQuorumAgreeDifferentViews(c:Constants, v:Variables,seqID:Messages.SequenceID, + view1:nat, + view2:nat, + commits1:set, + commits2:set, + operationWrapper1:Messages.OperationWrapper, + operationWrapper2:Messages.OperationWrapper) + requires Inv(c, v) + requires isCommitQuorum(c, v, view1, seqID, operationWrapper1, commits1) + requires isCommitQuorum(c, v, view2, seqID, operationWrapper2, commits2) + requires view1 < view2 + ensures (operationWrapper1 == operationWrapper2) + { + reveal_UnCommitableAgreesWithPrepare(); + if operationWrapper1 != operationWrapper2 { + UniqueSendersCardinality(commits2); + var commit := GetMsgFromHonestSender(c, commits2); + var prepare := GetPrepareFromHonestSenderForCommit(c, v, commit); // This term instantiates UnCommitableAgreesWithPrepare + UniqueSendersCardinality(commits1); + Library.SubsetCardinality(Messages.sendersOf(commits1), ReplicasThatCanCommitInView(c, v, seqID, view1, operationWrapper1)); + assert !UnCommitableInView(c, v, seqID, view1, operationWrapper1); // We have proven both UnCommitableInView !UnCommitableInView + assert false; //proof by contradiction + } + } + + // Quorum of commits >= 2F+1 agree on all views + predicate CommitQuorumsAgreeOnOperation(c:Constants, v:Variables) { + && v.WF(c) + && (forall seqID:Messages.SequenceID, + view1:nat, + view2:nat, + commits1:set, + commits2:set, + operationWrapper1:Messages.OperationWrapper, + operationWrapper2:Messages.OperationWrapper + | && isCommitQuorum(c, v, view1, seqID, operationWrapper1, commits1) + && isCommitQuorum(c, v, view2, seqID, operationWrapper2, commits2) + :: operationWrapper1 == operationWrapper2) + } + + predicate HonestReplicasAgreeOnOperationsOrdering(c:Constants, v:Variables) { + && v.WF(c) + && (forall replica1:HostId, + replica2:HostId, + seqID:Messages.SequenceID | && IsHonestReplica(c, replica1) + && IsHonestReplica(c, replica2) + :: && var r1_c := c.hosts[replica1].replicaConstants; + && var r2_c := c.hosts[replica2].replicaConstants; + && var r1_v := v.hosts[replica1].replicaVariables; + && var r2_v := v.hosts[replica2].replicaVariables; + && (&& Replica.IsCommitted(r1_c, r1_v, seqID) + && Replica.IsCommitted(r2_c, r2_v, seqID)) ==> Replica.GetCommittedOperation(r1_c, r1_v, seqID) == Replica.GetCommittedOperation(r2_c, r2_v, seqID)) + + } + + lemma HonestPreservesRecordedPrePreparesMatchHostView(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + ensures RecordedPrePreparesMatchHostView(c, v') + { + h_v.workingWindow.reveal_Shift(); + reveal_RecordedPrePreparesMatchHostView(); + } + + lemma HonestPreservesUnCommitableAgreesWithPrepare(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + ensures UnCommitableAgreesWithPrepare(c, v') + { + if(h_step.LeaveViewStep?) { + HonestLeaveViewStepPreservesUnCommitableAgreesWithPrepare(c, v, v', step, h_v, h_step); + } else if(h_step.SendPrepareStep?) { + HonestSendPrepareStepPreservesUnCommitableAgreesWithPrepare(c, v, v', step, h_v, h_step); + } else { + TriviallyPreserveUnCommitableAgreesWithPrepare(c, v, v', step, HonestInfo(h_v, h_step)); + } + } + + lemma HonestPreservesHonestReplicasLeaveViewsBehind(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + ensures HonestReplicasLeaveViewsBehind(c, v') + { + reveal_HonestReplicasLeaveViewsBehind(); + } + + lemma HonestPreservesRecordedNewViewMsgsAreChecked(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + ensures RecordedNewViewMsgsAreChecked(c, v') + { + reveal_RecordedNewViewMsgsAreChecked(); + reveal_RecordedViewChangeMsgsCameFromNetwork(); + + forall replicaIdx, newViewMsg | && IsHonestReplica(c, replicaIdx) + && var replicaVariables' := v'.hosts[replicaIdx].replicaVariables; + && newViewMsg in replicaVariables'.newViewMsgsRecvd.msgs + ensures + && newViewMsg.payload.vcMsgs.msgs <= v'.network.sentMsgs + { + var replicaVariables := v.hosts[replicaIdx].replicaVariables; + if (newViewMsg in replicaVariables.newViewMsgsRecvd.msgs) { + assert newViewMsg.payload.vcMsgs.msgs <= v'.network.sentMsgs; + } else { + if (h_step.RecvNewViewMsgStep?) { + assert newViewMsg.payload.vcMsgs.msgs <= v'.network.sentMsgs; + } else if (h_step.SelectQuorumOfViewChangeMsgsStep?) { + assert newViewMsg.payload.vcMsgs.msgs <= v'.network.sentMsgs; + } else { + assert false; + } + } + } + } + + lemma HonestPreservesRecordedViewChangeMsgsCameFromNetwork(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + ensures RecordedViewChangeMsgsCameFromNetwork(c, v') + { + reveal_RecordedViewChangeMsgsCameFromNetwork(); + } + + lemma HonestPreservesOneViewChangeMessageFromReplicaPerView(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + ensures OneViewChangeMessageFromReplicaPerView(c, v') + { + reveal_HonestReplicasLeaveViewsBehind(); + reveal_ViewChangeMsgsFromHonestInNetworkAreValid(); + reveal_OneViewChangeMessageFromReplicaPerView(); + reveal_RecordedViewChangeMsgsCameFromNetwork(); + } + + lemma InvokeEveryCommitMsgIsRememberedByVCMsgs(c: Constants, v:Variables, commitMsg:Message, viewChangeMsg:Message) + requires EveryCommitMsgIsRememberedByVCMsgs(c, v) + requires commitMsg in v.network.sentMsgs + requires viewChangeMsg in v.network.sentMsgs + requires commitMsg.payload.Commit? + requires viewChangeMsg.payload.ViewChangeMsg? + requires viewChangeMsg.sender == commitMsg.sender + requires IsHonestReplica(c, commitMsg.sender) + requires commitMsg.payload.view < viewChangeMsg.payload.newView + ensures && commitMsg.payload.seqID in viewChangeMsg.payload.certificates + && var certificate := viewChangeMsg.payload.certificates[commitMsg.payload.seqID]; + && CertificateComportsWithCommit(c, certificate, commitMsg) + { + assume commitMsg.payload.seqID > viewChangeMsg.payload.lastStableCheckpoint; // Because of TemporarilyDisabledCheckpointing. Move as requires once it is introduced + reveal_EveryCommitMsgIsRememberedByVCMsgs(); + } + + lemma UnCommitableIfNoCertificates(c:Constants, + v:Variables, + replicaIdx:HostId, + seqID:Messages.SequenceID, + priorView:nat, + priorOperationWrapper:Messages.OperationWrapper, + newViewMsg:Message) + requires Inv(c, v) + requires IsHonestReplica(c, replicaIdx) + requires newViewMsg.payload.NewViewMsg? + requires priorView < newViewMsg.payload.newView + requires && var h_c := c.hosts[replicaIdx].replicaConstants; + && var h_v := v.hosts[replicaIdx].replicaVariables; + && |Replica.GetNewViewMsgsForCurrentView(h_c, h_v)| > 0 + && newViewMsg == Replica.GetNewViewMsgForCurrentView(h_c, h_v) + && newViewMsg in h_v.newViewMsgsRecvd.msgs + && Replica.CurrentNewViewMsg(h_c, h_v, newViewMsg) + && seqID in Replica.ExtractSeqIDsFromPrevView(h_c, h_v, newViewMsg) + && |Replica.getRelevantPrepareCertificates(h_c, seqID, newViewMsg)| == 0; + + ensures UnCommitableInView(c, v, seqID, priorView, priorOperationWrapper) + { + var h_c := c.hosts[replicaIdx].replicaConstants; + var h_v := v.hosts[replicaIdx].replicaVariables; + var relevantCerts := Replica.getRelevantPrepareCertificates(h_c, seqID, newViewMsg); + var newViewMsg := Replica.GetNewViewMsgForCurrentView(h_c, h_v); + var viewChangers := Messages.sendersOf(newViewMsg.payload.vcMsgs.msgs); + assert newViewMsg.payload.checked(c.clusterConfig, v.network.sentMsgs) by { + reveal_RecordedNewViewMsgsAreChecked(); + } + UniqueSendersCardinality(newViewMsg.payload.vcMsgs.msgs); + assert viewChangers <= getAllReplicas(c) by { + reveal_RecordedNewViewMsgsAreChecked(); + } + var troubleMakers := ReplicasThatCanCommitInView(c, v, seqID, priorView, priorOperationWrapper); + if |troubleMakers| >= c.clusterConfig.AgreementQuorum() { + var doubleAgent := FindQuorumIntersection(c, viewChangers, troubleMakers); + var vcMsg:Message :| && vcMsg in newViewMsg.payload.vcMsgs.msgs + && vcMsg.sender == doubleAgent; + assert IsHonestReplica(c, doubleAgent); + assert !ReplicasInViewOrLower(c, v, seqID, priorView, priorOperationWrapper, doubleAgent) by { + reveal_HonestReplicasLeaveViewsBehind(); + assert v.hosts[doubleAgent].replicaVariables.view >= vcMsg.payload.newView; + } + var sentCommit := Network.Message(doubleAgent, + Messages.Commit(priorView, + seqID, + priorOperationWrapper)); + assert sentCommit in v.network.sentMsgs; + assume seqID in vcMsg.payload.certificates; // Sliding of the WW is disabled for now. + var certificate := vcMsg.payload.certificates[seqID]; + assert CertificateComportsWithCommit(c, certificate, sentCommit) by { + assume false; // Left off on a timeout + //reveal_EveryCommitMsgIsRememberedByVCMsgs(); + assert sentCommit.payload.seqID in vcMsg.payload.certificates; + assert sentCommit.payload.seqID == seqID; + assert CertificateComportsWithCommit(c, certificate, sentCommit); + } + assert !certificate.empty(); + assert certificate in Replica.getRelevantPrepareCertificates(h_c, seqID, newViewMsg); + Library.SubsetCardinality({certificate}, Replica.getRelevantPrepareCertificates(h_c, seqID, newViewMsg)); + assert |{certificate}| == 1; + assert |Replica.getRelevantPrepareCertificates(h_c, seqID, newViewMsg)| > 0; + assert |Replica.getRelevantPrepareCertificates(h_c, seqID, newViewMsg)| == 0; + assert false; // Contradiction + } + assert UnCommitableInView(c, v, seqID, priorView, priorOperationWrapper); + } + + lemma UnCommitableIfSomeCertificates(c:Constants, + v:Variables, + replicaIdx:HostId, + seqID:Messages.SequenceID, + priorView:nat, + priorOperationWrapper:Messages.OperationWrapper, + newViewMsg:Message) + requires Inv(c, v) + requires IsHonestReplica(c, replicaIdx) + requires newViewMsg.payload.NewViewMsg? + requires priorView < newViewMsg.payload.newView + requires && var h_c := c.hosts[replicaIdx].replicaConstants; + && var h_v := v.hosts[replicaIdx].replicaVariables; + && newViewMsg in h_v.newViewMsgsRecvd.msgs + && Replica.CurrentNewViewMsg(h_c, h_v, newViewMsg) + && seqID in Replica.ExtractSeqIDsFromPrevView(h_c, h_v, newViewMsg) + && var relevantCerts := Replica.getRelevantPrepareCertificates(h_c, seqID, newViewMsg); + && |relevantCerts| > 0 + && Replica.HighestViewPrepareCertificate(relevantCerts).prototype().operationWrapper != priorOperationWrapper + ensures UnCommitableInView(c, v, seqID, priorView, priorOperationWrapper) + { + assume false; // TODO: Proof in progress. To be removed. + var h_c := c.hosts[replicaIdx].replicaConstants; + var h_v := v.hosts[replicaIdx].replicaVariables; + var relevantCerts := Replica.getRelevantPrepareCertificates(h_c, seqID, newViewMsg); + var highestViewCert := Replica.HighestViewPrepareCertificate(relevantCerts); + if highestViewCert.prototype().view == priorView { + // doubleAgent reasonong here. + } else if highestViewCert.prototype().view > priorView { + // From the highestViewCert take a prepare message from an honest replica. That honest replica has a NewViewMsg - use it to recurse. + } else if highestViewCert.prototype().view < priorView { + // doubleAgent reasonong here. + } + } + + lemma HonestRecvPrePrepareStepPreservesUnCommitableAgreesWithRecordedPrePrepare(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + requires h_step.RecvPrePrepareStep? + ensures UnCommitableAgreesWithRecordedPrePrepare(c, v') + { + reveal_UnCommitableAgreesWithRecordedPrePrepare(); + //reveal_RecordedNewViewMsgsAreValid(); Selectively reveal in assert by-s (causes triggering explosion) + forall replicaIdx, seqID, priorView:nat, priorOperationWrapper:Messages.OperationWrapper | + && IsHonestReplica(c, replicaIdx) + && var replicaVariables' := v'.hosts[replicaIdx].replicaVariables; + && var replicaConstants' := c.hosts[replicaIdx].replicaConstants; + && seqID in replicaVariables'.workingWindow.getActiveSequenceIDs(replicaConstants') + && replicaVariables'.workingWindow.prePreparesRcvd[seqID].Some? + && var prePrepareMsg := replicaVariables'.workingWindow.prePreparesRcvd[seqID].value; + && priorOperationWrapper != prePrepareMsg.payload.operationWrapper + && priorView < prePrepareMsg.payload.view + ensures && var prePrepareMsg := v'.hosts[replicaIdx].replicaVariables.workingWindow.prePreparesRcvd[seqID].value; + && UnCommitableInView(c, v', prePrepareMsg.payload.seqID, priorView, priorOperationWrapper) { + var replicaVariables := v.hosts[replicaIdx].replicaVariables; + var replicaVariables' := v'.hosts[replicaIdx].replicaVariables; + if replicaVariables.workingWindow.prePreparesRcvd[seqID].None? { // Interesting case is when we record a new PrePrepare. // The checks that the Replica does before recording // is sufficient to proove UnCommitableAgreesWithRecordedPrePrepare + var h_c := c.hosts[replicaIdx].replicaConstants; + var newViewMsgs := Replica.GetNewViewMsgsForCurrentView(h_c, h_v); + // Double check that we have everything we need for the var newViewMsgs + var prePrepareMsg := replicaVariables'.workingWindow.prePreparesRcvd[seqID].value; + assert prePrepareMsg.payload.seqID == seqID; + var newView := replicaVariables'.workingWindow.prePreparesRcvd[seqID].value.payload.view; // TODO: rename currentView + // Assert that newView == replicaVariables'.view + if |newViewMsgs| == 0 { + assert h_v.view == 0; + assert false;//This cannot happen because there is a priorView < prePrepareMsg's view. + } + var newViewMsg := Replica.GetNewViewMsgForCurrentView(h_c, h_v); + assert Replica.CurrentNewViewMsg(h_c, h_v, newViewMsg) by { + reveal_RecordedNewViewMsgsAreChecked(); + } + if seqID !in Replica.ExtractSeqIDsFromPrevView(h_c, h_v, newViewMsg) { + assume false; // Sliding of the WW is disabled for now. + } else if |Replica.getRelevantPrepareCertificates(h_c, seqID, newViewMsg)| == 0 { + UnCommitableIfNoCertificates(c, v, replicaIdx, seqID, priorView, priorOperationWrapper, newViewMsg); + } else { + UnCommitableIfSomeCertificates(c, v, replicaIdx, seqID, priorView, priorOperationWrapper, newViewMsg); + } + } else { + var prePrepareMsg := v.hosts[replicaIdx].replicaVariables.workingWindow.prePreparesRcvd[seqID].value; + var prePrepareMsg' := v'.hosts[replicaIdx].replicaVariables.workingWindow.prePreparesRcvd[seqID].value; + assert prePrepareMsg == prePrepareMsg'; + assert seqID == prePrepareMsg'.payload.seqID by { + reveal_RecordedPrePreparesRecvdCameFromNetwork(); + } + assert UnCommitableInView(c, v, prePrepareMsg.payload.seqID, priorView, priorOperationWrapper); + assert UnCommitableInView(c, v, seqID, priorView, priorOperationWrapper); + } + assert UnCommitableInView(c, v, seqID, priorView, priorOperationWrapper); + assert ReplicasThatCanCommitInView(c, v', seqID, priorView, priorOperationWrapper) // Carry the knowledge from v into v' + == ReplicasThatCanCommitInView(c, v, seqID, priorView, priorOperationWrapper); + } + } + + lemma HonestPreservesUnCommitableAgreesWithRecordedPrePrepare(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + ensures UnCommitableAgreesWithRecordedPrePrepare(c, v') + { + if(h_step.LeaveViewStep?) { + HonestLeaveViewStepPreservesUnCommitableAgreesWithRecordedPrePrepare(c, v, v', step, h_v, h_step); + } else if(h_step.RecvPrePrepareStep?) { + HonestRecvPrePrepareStepPreservesUnCommitableAgreesWithRecordedPrePrepare(c, v, v', step, h_v, h_step); + } else if(h_step.SendPrePrepareStep?) { + assume false; + } else { + TriviallyPreserveUnCommitableAgreesWithRecordedPrePrepare(c, v, v', step, HonestInfo(h_v, h_step)); + } + } + + lemma HonestPreservesSentViewChangesMsgsComportWithSentCommits(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + ensures SentViewChangesMsgsComportWithSentCommits(c, v') + { + reveal_SentViewChangesMsgsComportWithSentCommits(); + + reveal_EveryCommitClientOpMatchesRecordedPrePrepare(); + reveal_RecordedPreparesHaveValidSenderID(); + reveal_RecordedPrePreparesRecvdCameFromNetwork(); + reveal_RecordedPreparesMatchHostView(); + reveal_RecordedPreparesClientOpsMatchPrePrepare(); + reveal_RecordedCommitsClientOpsMatchPrePrepare(); + reveal_EverySentIntraViewMsgIsInWorkingWindowOrBefore(); + reveal_EverySentIntraViewMsgIsForAViewLessOrEqualToSenderView(); + reveal_EveryPrepareMatchesRecordedPrePrepare(); + reveal_EveryCommitClientOpMatchesRecordedPrePrepare(); + reveal_HonestReplicasLockOnPrepareForGivenView(); + reveal_HonestReplicasLockOnCommitForGivenView(); + reveal_CommitMsgsFromHonestSendersAgree(); + reveal_RecordedCheckpointsRecvdCameFromNetwork(); + reveal_HonestReplicasLockOnCommitForGivenView(); + reveal_EveryCommitMsgIsSupportedByAQuorumOfSentPrepares(); + h_v.workingWindow.reveal_Shift(); + } + + lemma HonestPreservesViewChangeMsgsFromHonestInNetworkAreValid(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + ensures ViewChangeMsgsFromHonestInNetworkAreValid(c, v') + { + assume false; // TODO: Proof in progress. To be removed. + reveal_ViewChangeMsgsFromHonestInNetworkAreValid(); + forall viewChangeMsg | + && viewChangeMsg in v'.network.sentMsgs + && viewChangeMsg.payload.ViewChangeMsg? + && var replicaIdx := viewChangeMsg.sender; + && IsHonestReplica(c, replicaIdx) + ensures && var replicaIdx := viewChangeMsg.sender; + && viewChangeMsg.payload.checked(c.clusterConfig, v'.network.sentMsgs) { + var h_c := c.hosts[step.id].replicaConstants; + var replicaIdx := viewChangeMsg.sender; + if viewChangeMsg !in v.network.sentMsgs { + assert h_step.LeaveViewStep? by { + reveal_RecordedViewChangeMsgsCameFromNetwork(); + } + reveal_EveryPrepareMatchesRecordedPrePrepare(); + reveal_TemporarilyDisableCheckpointing(); + var certificates := viewChangeMsg.payload.certificates; + forall seqID | seqID in certificates + ensures && certificates[seqID].valid(c.clusterConfig, seqID) + && certificates[seqID].votesRespectView(viewChangeMsg.payload.newView) + && certificates[seqID].votes <= v.network.sentMsgs { + var certificate := certificates[seqID]; + var workingWindowPreparesRecvd := Replica.ExtractPreparesFromWorkingWindow(h_c, h_v, seqID); + var viewChangeMsgPreparesRecvd := Replica.ExtractPreparesFromLatestViewChangeMsg(h_c, h_v, seqID); + if |workingWindowPreparesRecvd| >= h_c.clusterConfig.AgreementQuorum() + { + reveal_RecordedPreparesRecvdCameFromNetwork(); + assert certificates == Replica.ExtractCertificates(h_c, h_v); + assert certificate == Replica.ExtractCertificateForSeqID(h_c, h_v, seqID); + if !certificate.empty() { + var key :| && key in h_v.workingWindow.preparesRcvd[seqID] + && h_v.workingWindow.preparesRcvd[seqID][key].payload == certificate.prototype(); + + assert certificate.validFull(c.clusterConfig, seqID); + } + assert certificate.valid(c.clusterConfig, seqID); + assert certificate.votesRespectView(viewChangeMsg.payload.newView); + } + else if |viewChangeMsgPreparesRecvd| >= c.clusterConfig.AgreementQuorum() { + assume false; + assert certificate.valid(c.clusterConfig, seqID); + assert certificate.votesRespectView(viewChangeMsg.payload.newView); + assert certificate.votes <= v.network.sentMsgs; + } + else { + assert certificate.valid(c.clusterConfig, seqID); + assert certificate.votesRespectView(viewChangeMsg.payload.newView); + assert certificate.votes <= v.network.sentMsgs; + } + } + assert Replica.ExtractValidStableCheckpointProof(h_c, h_v).msgs == {} by { + // We need 2 Invariants: + // 1. All Checkpoint messages we record are in the netork. + // 2. Checkpint messages from honest senders precede its last stable variable. + // Since Checkpointing is disabled the honest senders have last stable == 0, + // therefore we cannot get a quorum of honest senders. + assume false; + } + assert h_v.workingWindow.lastStableCheckpoint == 0; + assert viewChangeMsg.payload.checked(c.clusterConfig, v'.network.sentMsgs); + } else { + assert viewChangeMsg.payload.checked(c.clusterConfig, v'.network.sentMsgs); + } + } + } + + lemma HonestPreservesEveryCommitMsgIsRememberedByItsSenderForCommitStep( + c:Constants, + v:Variables, + v':Variables, + step:Step, + stepper_v:Replica.Variables, + h_step:Replica.Step, + commitMsg:Message, + committer_c:Replica.Constants, + committer_v':Replica.Variables) returns (certificate:Messages.PreparedCertificate) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, stepper_v, h_step) + requires commitMsg in v'.network.sentMsgs + requires commitMsg.payload.Commit? + requires IsHonestReplica(c, commitMsg.sender) + requires committer_c == c.hosts[commitMsg.sender].replicaConstants + requires committer_v' == v'.hosts[commitMsg.sender].replicaVariables + requires commitMsg.payload.seqID in committer_v'.workingWindow.getActiveSequenceIDs(committer_c) + requires h_step.SendCommitStep? + ensures certificate == Replica.ExtractCertificateForSeqID(committer_c, committer_v', commitMsg.payload.seqID) + ensures certificate.valid(c.clusterConfig, commitMsg.payload.seqID) + ensures !certificate.empty() + ensures certificate.prototype().view >= commitMsg.payload.view + ensures (certificate.prototype().view == commitMsg.payload.view + ==> certificate.prototype().operationWrapper == commitMsg.payload.operationWrapper) + { + reveal_EveryCommitMsgIsRememberedByItsSender(); + reveal_TemporarilyDisableCheckpointing(); + reveal_RecordedViewChangeMsgsCameFromNetwork(); + reveal_OneViewChangeMessageFromReplicaPerView(); + + certificate := Replica.ExtractCertificateForSeqID(committer_c, committer_v', commitMsg.payload.seqID); + + // assert forall vcMsg + // :: Replica.IsRecordedViewChangeMsgForView(committer_c, committer_v', committer_v'.view, vcMsg) == + // Replica.IsRecordedViewChangeMsgForView(committer_c, stepper_v, stepper_v.view, vcMsg); + if(commitMsg !in v.network.sentMsgs) { + assert commitMsg.sender == step.id; // Committer and stepper are same in this branch + Messages.reveal_UniqueSenders(); + var seqID := commitMsg.payload.seqID; + var workingWindowPreparesRecvd := set key | key in stepper_v.workingWindow.preparesRcvd[seqID] // !!! TODO: We probably don't want the stepper here + :: stepper_v.workingWindow.preparesRcvd[seqID][key]; + reveal_RecordedPreparesHaveValidSenderID(); + reveal_RecordedPreparesRecvdCameFromNetwork(); + reveal_RecordedPreparesClientOpsMatchPrePrepare(); + reveal_RecordedPreparesMatchHostView(); + CountPrepareMessages(stepper_v.workingWindow.preparesRcvd[seqID]); + assert workingWindowPreparesRecvd == stepper_v.workingWindow.preparesRcvd[seqID].Values; // Extentionality + } + } + + // lemma FullQuorumOfPreparesEnsuresValidFullCertificate( + // c:Constants, + // v:Variables, + // h_c:Replica.Constants, + // h_v:Replica.Variables, + // seqID:Messages.SequenceID) + // requires v.WF(c) + // requires |Replica.ExtractCertificateForSeqID(h_c, h_v, seqID).votes| >= h_c.clusterConfig.AgreementQuorum() + // ensures Replica.ExtractCertificateForSeqID(h_c, h_v, seqID).validFull(h_c.clusterConfig, seqID) + // { + + // } + + lemma HonestPreservesEveryCommitMsgIsRememberedByItsSenderForRecvPrepareStep( + c:Constants, + v:Variables, + v':Variables, + step:Step, + stepper_v:Replica.Variables, + h_step:Replica.Step, + commitMsg:Message, + committer_c:Replica.Constants, + committer_v':Replica.Variables) returns (certificate:Messages.PreparedCertificate) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, stepper_v, h_step) + requires commitMsg in v'.network.sentMsgs + requires commitMsg.payload.Commit? + requires IsHonestReplica(c, commitMsg.sender) + requires committer_c == c.hosts[commitMsg.sender].replicaConstants + requires committer_v' == v'.hosts[commitMsg.sender].replicaVariables + requires commitMsg.payload.seqID in committer_v'.workingWindow.getActiveSequenceIDs(committer_c) + requires h_step.RecvPrepareStep? + ensures certificate == Replica.ExtractCertificateForSeqID(committer_c, committer_v', commitMsg.payload.seqID) + ensures certificate.valid(c.clusterConfig, commitMsg.payload.seqID) + ensures !certificate.empty() + ensures certificate.prototype().view >= commitMsg.payload.view + ensures (certificate.prototype().view == commitMsg.payload.view + ==> certificate.prototype().operationWrapper == commitMsg.payload.operationWrapper) + { + reveal_EveryCommitMsgIsRememberedByItsSender(); + reveal_TemporarilyDisableCheckpointing(); + reveal_RecordedViewChangeMsgsCameFromNetwork(); + reveal_OneViewChangeMessageFromReplicaPerView(); + reveal_RecordedPreparesMatchHostView(); + reveal_RecordedPreparesRecvdCameFromNetwork(); + reveal_RecordedPreparesClientOpsMatchPrePrepare(); + Messages.reveal_UniqueSenders(); + + var seqID := commitMsg.payload.seqID; + + assert EveryCommitMsgIsRememberedByItsSender(c, v); + + var committer_v := v.hosts[commitMsg.sender].replicaVariables; + + var oldCertificate := Replica.ExtractCertificateForSeqID(committer_c, committer_v, seqID); + certificate := Replica.ExtractCertificateForSeqID(committer_c, committer_v', seqID); + + if(commitMsg !in v.network.sentMsgs) { + assert false; + } + assert Replica.PrepareProofSetWF(committer_c, committer_v'.workingWindow.preparesRcvd[seqID]); + + if(step.id == commitMsg.sender) { + if(commitMsg.payload.view < committer_v.view) { + if(oldCertificate.votes != Replica.ExtractPreparesFromLatestViewChangeMsg(committer_c, committer_v, seqID)) { + forall prepare | prepare in Replica.ExtractPreparesFromWorkingWindow(committer_c, committer_v, seqID) + ensures prepare in Replica.ExtractPreparesFromWorkingWindow(committer_c, committer_v', seqID) { + assert committer_v.workingWindow.preparesRcvd[seqID][prepare.sender] == + committer_v'.workingWindow.preparesRcvd[seqID][prepare.sender]; //Trigger + } + SubsetCardinality(Replica.ExtractPreparesFromWorkingWindow(committer_c, committer_v, seqID), + Replica.ExtractPreparesFromWorkingWindow(committer_c, committer_v', seqID)); + } + assert certificate.valid(c.clusterConfig, seqID); + assert (certificate.prototype().view == commitMsg.payload.view + ==> certificate.prototype().operationWrapper == commitMsg.payload.operationWrapper); + } else { + assert commitMsg.payload.view == committer_v.view by { + reveal_EverySentIntraViewMsgIsForAViewLessOrEqualToSenderView(); + } + var oldPrepares := Replica.ExtractPreparesFromWorkingWindow(committer_c, committer_v, seqID); + var newPrepares := Replica.ExtractPreparesFromWorkingWindow(committer_c, committer_v', seqID); + if(|newPrepares| >= c.clusterConfig.AgreementQuorum()) { + assert certificate.validFull(c.clusterConfig, seqID); + if |oldPrepares| >= c.clusterConfig.AgreementQuorum() { + assert certificate.prototype().operationWrapper == commitMsg.payload.operationWrapper; + } else { + reveal_EveryCommitMsgIsSupportedByAQuorumOfRecordedPrepares(); + assert false; // Couldn't have sent a Commit + } + } else { + if (|oldPrepares| >= c.clusterConfig.AgreementQuorum()) { + forall p | p in oldPrepares ensures p in newPrepares { + assert committer_v'.workingWindow.preparesRcvd[seqID][p.sender] == p; // Trigger + } + SubsetCardinality(oldPrepares,newPrepares); + } + if |Replica.ExtractPreparesFromLatestViewChangeMsg(committer_c, committer_v, seqID)| >= c.clusterConfig.AgreementQuorum() { + var viewChangeMsg := Replica.GetViewChangeMsgForView(committer_c, committer_v.viewChangeMsgsRecvd, committer_v.view); + var viewChangeMsgVotes := viewChangeMsg.payload.certificates[seqID]; + assert viewChangeMsg.payload.newView == committer_v.view; + assert viewChangeMsg.payload.validViewChangeMsg(c.clusterConfig) by { + reveal_ViewChangeMsgsFromHonestInNetworkAreValid(); + } + assert viewChangeMsgVotes.prototype().view < committer_v.view; + + assert false; + } + assert oldCertificate.validFull(c.clusterConfig, seqID); + assert oldCertificate.votes == Replica.ExtractPreparesFromWorkingWindow(committer_c, committer_v, seqID); + assert certificate.validFull(c.clusterConfig, seqID); + assert certificate.prototype().operationWrapper == commitMsg.payload.operationWrapper; + } + assert certificate.valid(c.clusterConfig, seqID); + assert certificate.prototype().view == commitMsg.payload.view; + assert certificate.prototype().operationWrapper == commitMsg.payload.operationWrapper; + } + + } else { + assert oldCertificate.validFull(c.clusterConfig, seqID); + assert oldCertificate.votes <= certificate.votes; + assert certificate.validFull(c.clusterConfig, seqID); + assert certificate.valid(c.clusterConfig, seqID); + } + } + + lemma HonestPreservesEveryCommitMsgIsRememberedByItsSender(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + ensures EveryCommitMsgIsRememberedByItsSender(c, v') + { + reveal_EveryCommitMsgIsRememberedByItsSender(); + + forall commitMsg | && commitMsg in v'.network.sentMsgs + && commitMsg.payload.Commit? + && IsHonestReplica(c, commitMsg.sender) + && var h_c := c.hosts[commitMsg.sender].replicaConstants; + && var h_v' := v'.hosts[commitMsg.sender].replicaVariables; + && commitMsg.payload.seqID in h_v'.workingWindow.getActiveSequenceIDs(h_c) + ensures && var h_c := c.hosts[commitMsg.sender].replicaConstants; + && var h_v' := v'.hosts[commitMsg.sender].replicaVariables; + && var certificate := Replica.ExtractCertificateForSeqID(h_c, h_v', commitMsg.payload.seqID); + && certificate.valid(c.clusterConfig, commitMsg.payload.seqID) + && !certificate.empty() + && certificate.prototype().view >= commitMsg.payload.view + && (certificate.prototype().view == commitMsg.payload.view + ==> certificate.prototype().operationWrapper == commitMsg.payload.operationWrapper) + { + + /* + | SendPrePrepareStep(seqID:SequenceID) + | RecvPrePrepareStep() + | SendPrepareStep(seqID:SequenceID) + | RecvPrepareStep() + | SendCommitStep(seqID:SequenceID) + | RecvCommitStep() + | DoCommitStep(seqID:SequenceID) + | ExecuteStep(seqID:SequenceID) + | SendCheckpointStep(seqID:SequenceID) + | RecvCheckpointStep() + | AdvanceWorkingWindowStep(seqID:SequenceID, checkpointsQuorum:CheckpointsQuorum) + | PerformStateTransferStep(seqID:SequenceID, checkpointsQuorum:CheckpointsQuorum) + //| SendReplyToClient(seqID:SequenceID) + // TODO: uncomment those steps when we start working on the proof + | LeaveViewStep(newView:ViewNum) + | SendViewChangeMsgStep() + | RecvViewChangeMsgStep() + | SelectQuorumOfViewChangeMsgsStep(viewChangeMsgsSelectedByPrimary:ViewChangeMsgsSelectedByPrimary) + | SendNewViewMsgStep() + | RecvNewViewMsgStep() + */ + var h_c := c.hosts[step.id].replicaConstants; + var h_v' := v'.hosts[step.id].replicaVariables; + reveal_TemporarilyDisableCheckpointing(); + reveal_RecordedViewChangeMsgsCameFromNetwork(); + reveal_OneViewChangeMessageFromReplicaPerView(); + if(h_step.LeaveViewStep?) { + assume false; + } else if(h_step.SendCommitStep?) { + var res := HonestPreservesEveryCommitMsgIsRememberedByItsSenderForCommitStep( + c, + v, + v', + step, + h_v, + h_step, + commitMsg, + c.hosts[commitMsg.sender].replicaConstants, + v'.hosts[commitMsg.sender].replicaVariables); + } else if(h_step.RecvPrepareStep?) { + var res := HonestPreservesEveryCommitMsgIsRememberedByItsSenderForRecvPrepareStep( + c, + v, + v', + step, + h_v, + h_step, + commitMsg, + c.hosts[commitMsg.sender].replicaConstants, + v'.hosts[commitMsg.sender].replicaVariables); + } else if(h_step.PerformStateTransferStep?) { + assert forall vcMsg + :: Replica.IsRecordedViewChangeMsgForView(h_c, h_v'.viewChangeMsgsRecvd, h_v'.view, vcMsg) == + Replica.IsRecordedViewChangeMsgForView(h_c, h_v.viewChangeMsgsRecvd, h_v.view, vcMsg); + assume false; + } else if(h_step.AdvanceWorkingWindowStep?) { + assert forall vcMsg + :: Replica.IsRecordedViewChangeMsgForView(h_c, h_v'.viewChangeMsgsRecvd, h_v'.view, vcMsg) == + Replica.IsRecordedViewChangeMsgForView(h_c, h_v.viewChangeMsgsRecvd, h_v.view, vcMsg); + assume false; + } else if(h_step.RecvViewChangeMsgStep?) { + assume false; + } else { + assert forall vcMsg + :: Replica.IsRecordedViewChangeMsgForView(h_c, h_v'.viewChangeMsgsRecvd, h_v'.view, vcMsg) == + Replica.IsRecordedViewChangeMsgForView(h_c, h_v.viewChangeMsgsRecvd, h_v.view, vcMsg); + } + } + } + + lemma HonestPreservesRecordedViewChangeMsgsAreValid(c: Constants, v:Variables, v':Variables, step:Step, h_v:Replica.Variables, h_step:Replica.Step) + requires Inv(c, v) + requires HonestReplicaStepTaken(c, v, v', step, h_v, h_step) + ensures RecordedViewChangeMsgsAreValid(c, v') + { + reveal_RecordedViewChangeMsgsAreValid(); + reveal_TemporarilyDisableCheckpointing(); // Needed for LeaveViewStep + if (h_step.LeaveViewStep?) { + reveal_RecordedPreparesRecvdCameFromNetwork(); + reveal_RecordedPreparesMatchHostView(); + reveal_RecordedPreparesClientOpsMatchPrePrepare(); + reveal_TemporarilyDisableCheckpointing(); + + forall replicaIdx, viewChangeMsg | + && IsHonestReplica(c, replicaIdx) + && var replicaVariables' := v'.hosts[replicaIdx].replicaVariables; + && viewChangeMsg in replicaVariables'.viewChangeMsgsRecvd.msgs + ensures (&& var replicaConstants := c.hosts[replicaIdx].replicaConstants; + && Replica.ValidViewChangeMsg(replicaConstants, + viewChangeMsg, + v'.network.sentMsgs)) + { + if(viewChangeMsg !in v.hosts[replicaIdx].replicaVariables.viewChangeMsgsRecvd.msgs) { + Messages.reveal_UniqueSenders(); + assert viewChangeMsg.payload.lastStableCheckpoint == 0; + assume |viewChangeMsg.payload.proofForLastStable.msgs| == 0; // TODO: remove once we introduce Checkpointing reasoning + } + } + } + } + lemma InvariantNext(c: Constants, v:Variables, v':Variables) requires Inv(c, v) requires Next(c, v, v') @@ -735,22 +2212,35 @@ module Proof { var h_v' := v'.hosts[step.id].replicaVariables; var h_step :| Replica.NextStep(h_c, h_v, h_v', step.msgOps, h_step); assert HonestReplicaStepTaken(c, v, v', step, h_v, h_step); - HonestPreservesAllReplicasLiteInv(c, v, v', step, h_v, h_step); + HonestPreservesRecordedNewViewMsgsAreValid(c, v, v', step, h_v, h_step); HonestPreservesRecordedPreparesHaveValidSenderID(c, v, v', step, h_v, h_step); HonestPreservesRecordedPrePreparesRecvdCameFromNetwork(c, v, v', step, h_v, h_step); - HonestPreservesRecordedPreparesInAllHostsRecvdCameFromNetwork(c, v, v', step, h_v, h_step); + HonestPreservesRecordedPreparesRecvdCameFromNetwork(c, v, v', step, h_v, h_step); HonestPreservesRecordedPreparesMatchHostView(c, v, v', step, h_v, h_step); - AlwaysPreservesEveryCommitMsgIsSupportedByAQuorumOfPrepares(c, v, v', step); + AlwaysPreservesEveryCommitMsgIsSupportedByAQuorumOfSentPrepares(c, v, v', step); + HonestPreservesEveryCommitMsgIsSupportedByAQuorumOfRecordedPrepares(c, v, v', step, h_v, h_step); HonestPreservesRecordedPreparesClientOpsMatchPrePrepare(c, v, v', step, h_v, h_step); HonestPreservesRecordedCommitsClientOpsMatchPrePrepare(c, v, v', step, h_v, h_step); HonestPreservesEverySentIntraViewMsgIsInWorkingWindowOrBefore(c, v, v', step, h_v, h_step); HonestPreservesEverySentIntraViewMsgIsForAViewLessOrEqualToSenderView(c, v, v', step, h_v, h_step); - HonestPreservesEveryPrepareClientOpMatchesRecordedPrePrepare(c, v, v', step, h_v, h_step); + HonestPreservesEveryPrepareMatchesRecordedPrePrepare(c, v, v', step, h_v, h_step); HonestPreservesEveryCommitClientOpMatchesRecordedPrePrepare(c, v, v', step, h_v, h_step); HonestPreservesHonestReplicasLockOnPrepareForGivenView(c, v, v', step, h_v, h_step); HonestPreservesHonestReplicasLockOnCommitForGivenView(c, v, v', step, h_v, h_step); HonestPreservesCommitMsgsFromHonestSendersAgree(c, v, v', step, h_v, h_step); HonestPreservesRecordedCheckpointsRecvdCameFromNetwork(c, v, v', step, h_v, h_step); + HonestPreservesRecordedPrePreparesMatchHostView(c, v, v', step, h_v, h_step); + HonestPreservesUnCommitableAgreesWithRecordedPrePrepare(c, v, v', step, h_v, h_step); + HonestPreservesUnCommitableAgreesWithPrepare(c, v, v', step, h_v, h_step); + HonestPreservesHonestReplicasLeaveViewsBehind(c, v, v', step, h_v, h_step); + HonestPreservesRecordedNewViewMsgsAreChecked(c, v, v', step, h_v, h_step); + HonestPreservesRecordedViewChangeMsgsCameFromNetwork(c, v, v', step, h_v, h_step); + HonestPreservesSentViewChangesMsgsComportWithSentCommits(c, v, v', step, h_v, h_step); + HonestPreservesEveryCommitMsgIsRememberedByItsSender(c, v, v', step, h_v, h_step); + HonestPreservesViewChangeMsgsFromHonestInNetworkAreValid(c, v, v', step, h_v, h_step); + HonestPreservesRecordedViewChangeMsgsAreValid(c, v, v', step, h_v, h_step); + HonestPreservesOneViewChangeMessageFromReplicaPerView(c, v, v', step, h_v, h_step); + assume TemporarilyDisableCheckpointing(c, v'); } else { InvNextFaultyOrClient(c, v, v', step); } @@ -763,8 +2253,8 @@ module Proof { requires (c.clusterConfig.IsFaultyReplica(step.id) || c.clusterConfig.IsClient(step.id)) ensures Inv(c, v') { - assert AllReplicasLiteInv(c, v') by { - reveal_AllReplicasLiteInv(); + assert RecordedNewViewMsgsAreValid(c, v') by { + reveal_RecordedNewViewMsgsAreValid(); } assert RecordedPreparesHaveValidSenderID(c, v') by { reveal_RecordedPreparesHaveValidSenderID(); @@ -772,8 +2262,8 @@ module Proof { assert RecordedPrePreparesRecvdCameFromNetwork(c, v') by { reveal_RecordedPrePreparesRecvdCameFromNetwork(); } - assert RecordedPreparesInAllHostsRecvdCameFromNetwork(c, v') by { - reveal_RecordedPreparesInAllHostsRecvdCameFromNetwork(); + assert RecordedPreparesRecvdCameFromNetwork(c, v') by { + reveal_RecordedPreparesRecvdCameFromNetwork(); } assert RecordedPreparesMatchHostView(c, v') by { reveal_RecordedPreparesMatchHostView(); @@ -790,8 +2280,8 @@ module Proof { assert EverySentIntraViewMsgIsForAViewLessOrEqualToSenderView(c, v') by { reveal_EverySentIntraViewMsgIsForAViewLessOrEqualToSenderView(); } - assert EveryPrepareClientOpMatchesRecordedPrePrepare(c, v') by { - reveal_EveryPrepareClientOpMatchesRecordedPrePrepare(); + assert EveryPrepareMatchesRecordedPrePrepare(c, v') by { + reveal_EveryPrepareMatchesRecordedPrePrepare(); } assert EveryCommitClientOpMatchesRecordedPrePrepare(c, v') by { reveal_EveryCommitClientOpMatchesRecordedPrePrepare(); @@ -811,8 +2301,82 @@ module Proof { assert HonestReplicasLockOnCommitForGivenView(c, v') by { reveal_HonestReplicasLockOnCommitForGivenView(); } - assert EveryCommitMsgIsSupportedByAQuorumOfPrepares(c, v') by { - AlwaysPreservesEveryCommitMsgIsSupportedByAQuorumOfPrepares(c, v, v', step); + assert EveryCommitMsgIsSupportedByAQuorumOfSentPrepares(c, v') by { + AlwaysPreservesEveryCommitMsgIsSupportedByAQuorumOfSentPrepares(c, v, v', step); + } + assert EveryCommitMsgIsSupportedByAQuorumOfRecordedPrepares(c, v') by { + reveal_EveryCommitMsgIsSupportedByAQuorumOfRecordedPrepares(); + } + assert RecordedPrePreparesMatchHostView(c, v') by { + reveal_RecordedPrePreparesMatchHostView(); + } + assert UnCommitableAgreesWithRecordedPrePrepare(c, v') by { + TriviallyPreserveUnCommitableAgreesWithRecordedPrePrepare(c, v, v', step, NotHonest()); + } + assert UnCommitableAgreesWithPrepare(c, v') by { + TriviallyPreserveUnCommitableAgreesWithPrepare(c, v, v', step, NotHonest()); + } + assert HonestReplicasLeaveViewsBehind(c, v') by { + reveal_HonestReplicasLeaveViewsBehind(); + } + assert RecordedNewViewMsgsAreChecked(c, v') by { + reveal_RecordedNewViewMsgsAreChecked(); + } + assert RecordedViewChangeMsgsCameFromNetwork(c, v') by { + reveal_RecordedViewChangeMsgsCameFromNetwork(); + } + assert SentViewChangesMsgsComportWithSentCommits(c, v') by { + reveal_SentViewChangesMsgsComportWithSentCommits(); + } + assert EveryCommitMsgIsRememberedByItsSender(c, v') by { + reveal_EveryCommitMsgIsRememberedByItsSender(); + } + assert RecordedViewChangeMsgsAreValid(c, v') by { + reveal_RecordedViewChangeMsgsAreValid(); + } + assert ViewChangeMsgsFromHonestInNetworkAreValid(c, v') by { + reveal_ViewChangeMsgsFromHonestInNetworkAreValid(); + } + assert OneViewChangeMessageFromReplicaPerView(c, v') by { + reveal_OneViewChangeMessageFromReplicaPerView(); + } + assume TemporarilyDisableCheckpointing(c, v'); + } + + lemma InitEstablishesInv(c: Constants, v:Variables) + requires Init(c, v) + ensures Inv(c, v) + { + assert Inv(c, v) by { + reveal_RecordedNewViewMsgsAreValid(); + reveal_RecordedCommitsClientOpsMatchPrePrepare(); + reveal_EveryPrepareMatchesRecordedPrePrepare(); + reveal_EveryCommitClientOpMatchesRecordedPrePrepare(); + reveal_HonestReplicasLockOnCommitForGivenView(); + reveal_CommitMsgsFromHonestSendersAgree(); + reveal_RecordedPreparesHaveValidSenderID(); + reveal_RecordedPrePreparesRecvdCameFromNetwork(); + reveal_RecordedPreparesRecvdCameFromNetwork(); + reveal_RecordedPreparesMatchHostView(); + reveal_RecordedPreparesClientOpsMatchPrePrepare(); + reveal_EverySentIntraViewMsgIsInWorkingWindowOrBefore(); + reveal_EverySentIntraViewMsgIsForAViewLessOrEqualToSenderView(); + reveal_HonestReplicasLockOnPrepareForGivenView(); + reveal_RecordedCheckpointsRecvdCameFromNetwork(); + reveal_EveryCommitMsgIsSupportedByAQuorumOfSentPrepares(); + reveal_EveryCommitMsgIsSupportedByAQuorumOfRecordedPrepares(); + reveal_RecordedPrePreparesMatchHostView(); + reveal_UnCommitableAgreesWithPrepare(); + reveal_UnCommitableAgreesWithRecordedPrePrepare(); + reveal_HonestReplicasLeaveViewsBehind(); + reveal_RecordedNewViewMsgsAreChecked(); + reveal_RecordedViewChangeMsgsCameFromNetwork(); + reveal_SentViewChangesMsgsComportWithSentCommits(); + reveal_EveryCommitMsgIsRememberedByItsSender(); + reveal_RecordedViewChangeMsgsAreValid(); + reveal_ViewChangeMsgsFromHonestInNetworkAreValid(); + reveal_OneViewChangeMessageFromReplicaPerView(); + reveal_TemporarilyDisableCheckpointing(); } } @@ -822,27 +2386,10 @@ module Proof { //ensures Inv(c, v) ==> Safety(c, v) { if Init(c, v) { - assert Inv(c, v) by { - reveal_AllReplicasLiteInv(); - reveal_RecordedCommitsClientOpsMatchPrePrepare(); - reveal_EveryPrepareClientOpMatchesRecordedPrePrepare(); - reveal_EveryCommitClientOpMatchesRecordedPrePrepare(); - reveal_HonestReplicasLockOnCommitForGivenView(); - reveal_CommitMsgsFromHonestSendersAgree(); - reveal_RecordedPreparesHaveValidSenderID(); - reveal_RecordedPrePreparesRecvdCameFromNetwork(); - reveal_RecordedPreparesInAllHostsRecvdCameFromNetwork(); - reveal_RecordedPreparesMatchHostView(); - reveal_RecordedPreparesClientOpsMatchPrePrepare(); - reveal_EverySentIntraViewMsgIsInWorkingWindowOrBefore(); - reveal_EverySentIntraViewMsgIsForAViewLessOrEqualToSenderView(); - reveal_HonestReplicasLockOnPrepareForGivenView(); - reveal_RecordedCheckpointsRecvdCameFromNetwork(); - reveal_EveryCommitMsgIsSupportedByAQuorumOfPrepares(); - } + InitEstablishesInv(c, v); } if Inv(c, v) && Next(c, v, v') { InvariantNext(c, v, v'); } } -} //Module \ No newline at end of file +} //Module diff --git a/docs/sbft-formal-model/replica.i.dfy b/docs/sbft-formal-model/replica.i.dfy index d4c20a6731..9b7b948e81 100644 --- a/docs/sbft-formal-model/replica.i.dfy +++ b/docs/sbft-formal-model/replica.i.dfy @@ -18,7 +18,7 @@ module Replica { import opened HostIdentifiers import opened Messages import Network - import ClusterConfig + import opened ClusterConfig type PrepareProofSet = map> predicate PrepareProofSetWF(c:Constants, ps:PrepareProofSet) @@ -64,14 +64,14 @@ module Replica { predicate IsActiveSeqID(lastStableCheckpoint:SequenceID, seqID:SequenceID) { - && lastStableCheckpoint <= seqID < lastStableCheckpoint + clusterConfig.workingWindowSize + && lastStableCheckpoint < seqID <= lastStableCheckpoint + clusterConfig.workingWindowSize } function getActiveSequenceIDs(lastStableCheckpoint:SequenceID) : set requires WF() { set seqID:SequenceID | && IsActiveSeqID(lastStableCheckpoint, seqID) // This statement provides a trigger by naming the constraint - && lastStableCheckpoint <= seqID < lastStableCheckpoint + clusterConfig.workingWindowSize // This statement satisfies Dafny's finite set heuristics. + && lastStableCheckpoint < seqID <= lastStableCheckpoint + clusterConfig.workingWindowSize // This statement satisfies Dafny's finite set heuristics. } } @@ -163,16 +163,10 @@ module Replica { } } - function PrimaryForView(c:Constants, view:ViewNum) : nat - requires c.WF() - { - view % c.clusterConfig.N() - } - function CurrentPrimary(c:Constants, v:Variables) : nat requires v.WF(c) { - PrimaryForView(c, v.view) + c.clusterConfig.PrimaryForView(v.view) } predicate HaveSufficientVCMsgsToMoveTo(c:Constants, v:Variables, newView:ViewNum) @@ -214,15 +208,7 @@ module Replica { } function ExtractSeqIDsFromPrevView(c:Constants, v:Variables, newViewMsg:Network.Message) : set - requires c.WF() - requires v.WF(c) - requires newViewMsg.payload.NewViewMsg? - requires newViewMsg.payload.valid(c.clusterConfig.AgreementQuorum()) - requires newViewMsg in v.newViewMsgsRecvd.msgs - // readability: - requires newViewMsg.payload.newView == v.view - requires CurrentPrimary(c, v) == newViewMsg.sender - requires LiteInv(c, v) + requires CurrentNewViewMsg(c, v, newViewMsg) { // 1. Check Each VC Msg for correct proof for last stable SeqID. // 2. Check New View for containing only correct VC msgs. @@ -257,17 +243,24 @@ module Replica { else HighestStable(c, rest) } + function getRelevantPrepareCertificates(c:Constants, seqID:SequenceID, newViewMsg:Network.Message) : (set) + requires c.WF() + requires newViewMsg.payload.NewViewMsg? + requires newViewMsg.payload.valid(c.clusterConfig) + { + set viewChangeMsg, cert:PreparedCertificate | + && viewChangeMsg in newViewMsg.payload.vcMsgs.msgs + && seqID in viewChangeMsg.payload.certificates + && cert == viewChangeMsg.payload.certificates[seqID] + && cert.WF() + && !cert.empty() + :: cert + } + function CalculateRestrictionForSeqID(c:Constants, v:Variables, seqID:SequenceID, newViewMsg:Network.Message) - : Option - requires v.WF(c) - requires newViewMsg.payload.NewViewMsg? - requires newViewMsg.payload.vcMsgs.valid(v.view, c.clusterConfig.AgreementQuorum()) - requires newViewMsg in v.newViewMsgsRecvd.msgs - // readability: - requires newViewMsg.payload.newView == v.view - requires CurrentPrimary(c, v) == newViewMsg.sender + : Option // returns None if any operation is allowed + requires CurrentNewViewMsg(c, v, newViewMsg) requires seqID in v.workingWindow.getActiveSequenceIDs(c) - requires LiteInv(c, v) { // 1. Take the NewViewMsg for the current View. // 2. Go through all the ViewChangeMsg-s in the NewView and take the valid full @@ -279,13 +272,7 @@ module Replica { if seqID !in ExtractSeqIDsFromPrevView(c, v, newViewMsg) then None else - var relevantPrepareCertificates := set viewChangeMsg, cert | - && viewChangeMsg in newViewMsg.payload.vcMsgs.msgs - && seqID in viewChangeMsg.payload.certificates - && cert == viewChangeMsg.payload.certificates[seqID] - && cert.WF() - && !cert.empty() - :: cert; + var relevantPrepareCertificates := getRelevantPrepareCertificates(c, seqID, newViewMsg); if |relevantPrepareCertificates| == 0 then Some(Noop) @@ -309,32 +296,58 @@ module Replica { && v.WF(c) && msgOps.IsSend() && CurrentPrimary(c, v) == c.myId - && seqID in v.workingWindow.getActiveSequenceIDs(c) - && msgOps.send == Some(Network.Message(c.myId, - PrePrepare(v.view, - seqID, - v.workingWindow.prePreparesRcvd[seqID].value.payload.operationWrapper))) + && IsValidPrePrepare(c, v, msgOps.send.value) + && msgOps.send.value.payload.seqID == seqID && v.workingWindow.prePreparesRcvd[seqID].None? && v' == v.(workingWindow := v.workingWindow.(prePreparesRcvd := v.workingWindow.prePreparesRcvd[seqID := Some(msgOps.send.value)])) } - // Node local invariants that we need to satisfy dafny requires. This gets proven as part of the Distributed system invariants. - // That is why it can appear as enabling condition, but does not need to be translated to runtime checks to C++. - // For this to be safe it has to appear in the main invarinat in the proof. - predicate LiteInv(c:Constants, v:Variables) { + predicate CurrentNewViewMsg(c:Constants, + v:Variables, + newViewMsg:Network.Message) + { && v.WF(c) - && (forall newViewMsg | newViewMsg in v.newViewMsgsRecvd.msgs :: - && newViewMsg.payload.valid(c.clusterConfig.AgreementQuorum()) - && PrimaryForView(c, newViewMsg.payload.newView) == newViewMsg.sender) + && ValidNewViewMsg(c.clusterConfig, newViewMsg) + && |GetNewViewMsgsForCurrentView(c, v)| > 0 + && newViewMsg == GetNewViewMsgForCurrentView(c, v) + } + + predicate IsValidOperationWrapper(c:Constants, + v:Variables, + seqID:SequenceID, + newViewMsg:Network.Message, + operation:OperationWrapper) + requires CurrentNewViewMsg(c, v, newViewMsg) + requires seqID in v.workingWindow.getActiveSequenceIDs(c) + { + && var restriction := CalculateRestrictionForSeqID(c, + v, + seqID, + newViewMsg); + && restriction.Some? ==> restriction.value == operation + } + + function GetNewViewMsgsForCurrentView(c:Constants, v:Variables) : set> + requires v.WF(c) + { + set msg | && msg in v.newViewMsgsRecvd.msgs + && msg.payload.newView == v.view + } + + function GetNewViewMsgForCurrentView(c:Constants, v:Variables) : Network.Message + requires v.WF(c) + requires |GetNewViewMsgsForCurrentView(c, v)| > 0 + { + var newViewMsg :| newViewMsg in GetNewViewMsgsForCurrentView(c, v); + newViewMsg } // For clarity here we have extracted all preconditions that must hold for a Replica to accept a PrePrepare - predicate IsValidPrePrepareToAccept(c:Constants, v:Variables, msg:Network.Message) + predicate IsValidPrePrepare(c:Constants, v:Variables, msg:Network.Message) { && v.WF(c) - && LiteInv(c, v) && msg.payload.PrePrepare? && msg.payload.seqID in v.workingWindow.getActiveSequenceIDs(c) && c.clusterConfig.IsReplica(msg.sender) @@ -342,17 +355,14 @@ module Replica { && msg.payload.view == v.view && msg.sender == CurrentPrimary(c, v) && v.workingWindow.prePreparesRcvd[msg.payload.seqID].None? - && var newViewMsgs := set msg | && msg in v.newViewMsgsRecvd.msgs - && msg.payload.newView == v.view; + && var newViewMsgs := GetNewViewMsgsForCurrentView(c, v); && (if |newViewMsgs| == 0 then true else && |newViewMsgs| == 1 - && var newViewMsg :| newViewMsg in newViewMsgs; - && Some(msg.payload.operationWrapper) == CalculateRestrictionForSeqID(c, - v, - msg.payload.seqID, - newViewMsg)) - + && var newViewMsg := GetNewViewMsgForCurrentView(c, v); + && newViewMsg.payload.valid(c.clusterConfig) + && c.clusterConfig.PrimaryForView(newViewMsg.payload.newView) == newViewMsg.sender + && IsValidOperationWrapper(c, v, msg.payload.seqID, newViewMsg, msg.payload.operationWrapper)) } // Predicate that describes what is needed and how we mutate the state v into v' when RecvPrePrepare @@ -363,7 +373,7 @@ module Replica { && v.WF(c) && msgOps.IsRecv() && var msg := msgOps.recv.value; - && IsValidPrePrepareToAccept(c, v, msg) + && IsValidPrePrepare(c, v, msg) && v' == v.(workingWindow := v.workingWindow.(prePreparesRcvd := v.workingWindow.prePreparesRcvd[msg.payload.seqID := Some(msg)])) @@ -515,7 +525,7 @@ module Replica { predicate LeaveView(c:Constants, v:Variables, v':Variables, msgOps:Network.MessageOps, newView:ViewNum) { // TODO: Clear all Working Window after we leave a View. && v.WF(c) - && msgOps.NoSendRecv() + && msgOps.IsSend() // We can only leave a view we have collected at least 2F+1 View // Change messages for in viewChangeMsgsRecvd or View is 0. && (|| (HasCollectedProofMyViewIsAgreed(c, v) && newView == v.view + 1) @@ -524,14 +534,24 @@ module Replica { ViewChangeMsg( newView, v.workingWindow.lastStableCheckpoint, - CheckpointsQuorum(ExtractStableCheckpointProof(c, v)), - ExtractCertificatesFromWorkingWindow(c, v))); - // TODO: this should follow from the invariant and from the way we collect prepares. Might be put in LiteInv. + ExtractValidStableCheckpointProof(c, v), + ExtractCertificates(c, v))); + // TODO: this should follow from the invariant and from the way we collect prepares. // && (forall seqID :: seqID in vcMsg.payload.certificates ==> // (vcMsg.payload.certificates[seqID].valid(c.clusterConfig.AgreementQuorum()))) && v' == v.(view := newView) .(viewChangeMsgsRecvd := v.viewChangeMsgsRecvd.(msgs := v.viewChangeMsgsRecvd.msgs + {vcMsg})) .(workingWindow := v.workingWindow.EmptyWorkingWindow(c)) + && msgOps.send.value == vcMsg + } + + function ExtractValidStableCheckpointProof(c:Constants, v:Variables) : CheckpointsQuorum + requires v.WF(c) + { + var proof := ExtractStableCheckpointProof(c, v); + if |proof| >= c.clusterConfig.AgreementQuorum() + then CheckpointsQuorum(proof) + else CheckpointsQuorum({}) } function ExtractStableCheckpointProof(c:Constants, v:Variables) : set> @@ -544,7 +564,41 @@ module Replica { && msg.payload.committedClientOperations == stateUpToSeqID } - function ExtractCertificatesFromWorkingWindow(c:Constants, v:Variables) : map + predicate IsRecordedViewChangeMsgForView(c:Constants, viewChangeMsgsRecvd:ViewChangeMsgs, view:ViewNum, viewChangeMsg:Network.Message) + { + && c.WF() + && viewChangeMsg.payload.ViewChangeMsg? + && viewChangeMsg in viewChangeMsgsRecvd.msgs + && viewChangeMsg.payload.newView == view + && viewChangeMsg.sender == c.myId + } + + function GetViewChangeMsgForView(c:Constants, viewChangeMsgsRecvd:ViewChangeMsgs, view:ViewNum) : Network.Message + requires c.WF() + requires exists viewChangeMsg :: IsRecordedViewChangeMsgForView(c, viewChangeMsgsRecvd, view, viewChangeMsg) + { + var viewChangeMsg :| IsRecordedViewChangeMsgForView(c, viewChangeMsgsRecvd, view, viewChangeMsg); + viewChangeMsg + } + + function ExtractPreparesFromWorkingWindow(c:Constants, v:Variables, seqID:SequenceID) : set> + requires v.WF(c) + requires seqID in v.workingWindow.getActiveSequenceIDs(c) + { + set key | key in v.workingWindow.preparesRcvd[seqID] // This set comprehension is the same as calling .Values, + :: v.workingWindow.preparesRcvd[seqID][key] // but this way it is better for triggering in Dafny + } + + function ExtractPreparesFromLatestViewChangeMsg(c:Constants, v:Variables, seqID:SequenceID) : set> + { + if !exists vcMsg :: IsRecordedViewChangeMsgForView(c, v.viewChangeMsgsRecvd, v.view, vcMsg) + then {} + else if seqID !in GetViewChangeMsgForView(c, v.viewChangeMsgsRecvd, v.view).payload.certificates + then {} + else GetViewChangeMsgForView(c, v.viewChangeMsgsRecvd, v.view).payload.certificates[seqID].votes + } + + function ExtractCertificates(c:Constants, v:Variables) : map requires v.WF(c) { map seqID | seqID in v.workingWindow.getActiveSequenceIDs(c) :: ExtractCertificateForSeqID(c, v, seqID) @@ -554,10 +608,13 @@ module Replica { requires v.WF(c) requires seqID in v.workingWindow.getActiveSequenceIDs(c) { - var preparesRecvd := set msg | msg in v.workingWindow.preparesRcvd[seqID].Values && msg.payload.Prepare?; - if |preparesRecvd| < c.clusterConfig.AgreementQuorum() - then PreparedCertificate({}) - else PreparedCertificate(preparesRecvd) + var workingWindowPreparesRecvd := ExtractPreparesFromWorkingWindow(c, v, seqID); + var viewChangeMsgPreparesRecvd := ExtractPreparesFromLatestViewChangeMsg(c, v, seqID); + if |workingWindowPreparesRecvd| >= c.clusterConfig.AgreementQuorum() + then PreparedCertificate(workingWindowPreparesRecvd) + else if |viewChangeMsgPreparesRecvd| >= c.clusterConfig.AgreementQuorum() + then PreparedCertificate(viewChangeMsgPreparesRecvd) + else PreparedCertificate({}) } predicate SendViewChangeMsg(c:Constants, v:Variables, v':Variables, msgOps:Network.MessageOps) @@ -578,17 +635,18 @@ module Replica { msgOps:Network.MessageOps, viewChangeMsgsSelectedByPrimary:ViewChangeMsgsSelectedByPrimary) { && v.WF(c) - && msgOps.NoSendRecv() + && msgOps.IsSend() && CurrentPrimary(c, v) == c.myId && (forall msg | && msg in v.newViewMsgsRecvd.msgs && msg.sender == c.myId :: msg.payload.newView != v.view) // We can only select 1 set of VC msgs && (forall vcMsg | vcMsg in viewChangeMsgsSelectedByPrimary.msgs :: && vcMsg in v.viewChangeMsgsRecvd.msgs) - && viewChangeMsgsSelectedByPrimary.valid(v.view, c.clusterConfig.AgreementQuorum()) + && viewChangeMsgsSelectedByPrimary.valid(v.view, c.clusterConfig) && var newViewMsg := Network.Message(c.myId, NewViewMsg(v.view, viewChangeMsgsSelectedByPrimary)); && v' == v.(newViewMsgsRecvd := v.newViewMsgsRecvd.(msgs := v.newViewMsgsRecvd.msgs + {newViewMsg})) + && msgOps.send.value == newViewMsg } predicate SendNewViewMsg(c:Constants, v:Variables, v':Variables, msgOps:Network.MessageOps) @@ -603,20 +661,22 @@ module Replica { && v' == v } + predicate ValidViewChangeMsg(c:Constants, + msg:Network.Message, + networkMsgs:set>) + requires c.WF() + { + && msg.payload.ViewChangeMsg? + // Check validity and signatures for the Prepared Certificates: + && msg.payload.checked(c.clusterConfig, networkMsgs) + } + predicate RecvViewChangeMsg(c:Constants, v:Variables, v':Variables, msgOps:Network.MessageOps) { && v.WF(c) && msgOps.IsRecv() && var msg := msgOps.recv.value; - && msg.payload.ViewChangeMsg? - // Check Checkpoint msg-s signatures: - && var checkpointMsgs := set c | c in msg.payload.proofForLastStable.msgs; - && checkpointMsgs <= msgOps.signedMsgsToCheck - // Check Signatures for the Prepared Certificates: - && (forall seqID | seqID in msg.payload.certificates - :: && msg.payload.certificates[seqID].votes <= msgOps.signedMsgsToCheck - && msg.payload.certificates[seqID].valid(c.clusterConfig.AgreementQuorum())) - && msg.payload.valid(c.clusterConfig.AgreementQuorum()) + && ValidViewChangeMsg(c, msg, msgOps.signedMsgsToCheck) && v' == v.(viewChangeMsgsRecvd := v.viewChangeMsgsRecvd.(msgs := v.viewChangeMsgsRecvd.msgs + {msg})) } @@ -628,12 +688,11 @@ module Replica { && msg.payload.NewViewMsg? && CurrentPrimary(c, v) == msg.sender && msg.payload.newView == v.view - && msg.payload.vcMsgs.msgs <= msgOps.signedMsgsToCheck - // Check that all the PreparedCertificates are valid - && msg.payload.valid(c.clusterConfig.AgreementQuorum()) + // Check that all the PreparedCertificates are valid and the signatures are OK + && msg.payload.checked(c.clusterConfig, msgOps.signedMsgsToCheck) // We only allow the primary to select 1 set of View Change messages per view. && (forall storedMsg | storedMsg in v.newViewMsgsRecvd.msgs :: msg.payload.newView != storedMsg.payload.newView) - && v.workingWindow.lastStableCheckpoint == HighestStable(c, msg.payload.vcMsgs.msgs) + && v.workingWindow.lastStableCheckpoint == HighestStable(c, msg.payload.vcMsgs.msgs) //TODO: might be >= && v' == v.(newViewMsgsRecvd := v.newViewMsgsRecvd.(msgs := v.newViewMsgsRecvd.msgs + {msg})) } @@ -698,6 +757,21 @@ module Replica { .(committedClientOperations := checkpointsQuorum.prototype().committedClientOperations) } + // All Checkpoints recorded are in network + // msgs in Checkpoints Quorum are also in network + // Wahtever a replica has written down agrees with 2F+1 other + // Quorum of commits agree on all views + + predicate IsCommitted(c:Constants, v:Variables, seqID:SequenceID) { + && seqID in v.committedClientOperations + } + + function GetCommittedOperation(c:Constants, v:Variables, seqID:SequenceID) : OperationWrapper + requires IsCommitted(c, v, seqID) + { + v.committedClientOperations[seqID] + } + predicate Init(c:Constants, v:Variables) { && v.WF(c) && v.view == 0 @@ -710,6 +784,7 @@ module Replica { && v.newViewMsgsRecvd.msgs == {} && v.countExecutedSeqIDs == 0 && v.checkpointMsgsRecvd.msgs == {} + && v.workingWindow.lastStableCheckpoint == 0 } // Jay Normal Form - Dafny syntactic sugar, useful for selecting the next step