Dafny latest proof progress WIP #3009
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
We completed the proof refactoring to improve verification times by manually guiding the automation on the last stable point where the proof passes correctly without timeouts. We are now transferring the latest progress in the proof to the now improved structure of the proof.
ReplicasThatSentCommit and ReplicasInViewOrLower predicates added for use in ReplicasThatCanCommitInView. Added predicates RecordedPrePreparesMatchHostView and UnCommitableAgreesWithRecordedPrePrepare to the global invariant.
* Addition to Inv predicate RecordedPrePreparesRecvdCameFromNetwork to retain the knowledge that the key we stored (seqID) is equal to the seqID in the msg. * Refactor TriviallyPreserveUnCommitableAgreesWithPrepare and * TriviallyPreserveUnCommitableAgreesWithRecordedPrePrepare to take as argument an option of either honest or not honest replica. * Necessary reveals for InitEstablishesInv extracted to separate lemma. * Lemmas for proving the additional predicates in the Inv added.
Added predicates HonestReplicasLeaveViewsBehind and RecordedNewViewMsgsContainSentVCMsgs to the global Invariant. Initial structuring for proving the Invarinat holds for HonestRecvPrePrepareStepPreservesUnCommitableAgreesWithRecordedPrePrepare.
When sending a PrePrepare, the Primary has to check if the SeqID is from a previous view and oblige the necessary restrictions if this is the case.
To avoid code duplication we extract the prerequisites for a NewViewMsg to be the one for the current View a replica is in to a separate predicate.
…nvariant. We need to retain the information that the recorded ViewChangeMsgs in the replicas came from the network. Minor fixes and structuring of the code by adding the necessary proofs for the newly added predicates in the global Invariant - HonestReplicasLeaveViewsBehind, RecordedNewViewMsgsContainSentVCMsgs and RecordedViewChangeMsgsCameFromNetwork.
* PreparedCertificate's valid method now takes a SeqID for whcich we check if the PreparedCertificate is valid. * LeaveView and SelectQuorumOfViewChangeMsgs send the newly created msgs right away. * On leaving a View we check for PreparedCertificates in both the Working Window and in the latest View Change msg we have generated.
* Predicate EveryCommitMsgIsRememberedByItsSender - temporary predicate states the honest replicas remember their Commit msgs. This will be revised Once Checkpoint and Shift are introduced to the proof. * RecordedViewChangeMsgsAreValid - predicate indicating that honest replicas validate a View Change msg before recording it, therefore all VC msgs an honest replica has recorded are valid. * SentViewChangesMsgsComportWithSentCommits - predicate indicating that honest replicas insert the prepared certificates they have collected into the View Change messages they have generated. * Cleanup of debugging code in the proof.
* SequenceID data type starts form 0, but we start committing from 1. This way we start with LastStableCkeckpoint at 0 and commit beyond it. * Fix for CheckpointsQuorum's valid predicate to take in consideration that for Sequence ID 0 we don't need agreement quorum of Checkpoint messages. * Added checked predicate for ViewChangeMsg and NewViewMsg which does all necessary checks including the signature checking, which is achieved on the call site by passing all the messages the network has stored. The call sites in replica.i.dfy have been revised. * Fix to set the lastStableCheckpoint == 0 in replica.i.dfy's Init predicate. * proof.dfy has been revised to take in consideration the above changes + hints on the lemmas that need to be completed.
* Move PrimaryForView to ClusterConfig. * Move functionality from checked that is not related to signature checks to valid predicate. * Remove LiteInv from replicas and move it into the global Inv but renamed to RecordedNewViewMsgsAreValid.
* Completed the verification of lemma HonestPreservesRecordedViewChangeMsgsAreValid. * Added triggering changes in replica.dfy in regard to the verification. * Refactoring in PreparedCertificate to collect all conditions for a valid check in 2 predicates - validFull() and empty().
Preparation for new lemma DoubleAgentDidNotCommit and Inv predicate CommitCertificateEstablishesUncommitableInView. Minor code cleanup.
…tsSenderForRecvPrepareStep. Refactoring in replica.i.dfy to improve triggering by dafny's heuristics.
… committer_v.view.
…derForRecvPrepareStep.
…roof in progress.
…cordedPrePrepare.
…reesWithRecordedPrePrepare. Minor cleanup: GetMsgFromHonestSender does not need Distributed system's variables.
RecordedNewViewMsgsContainSentVCMsgs changed to RecordedNewViewMsgsAreChecked. In this new predicate we check whether the contents of each recorded new view msg are correct according to the protocol (the VC msgs contained are valid and from different senders, etc). Temporary workaround in Library's MappedSetCardinality added to address Dafny's triggering problem.
…dedPrePrepare. We split the reasoning to first prove correctness wen moving to consecutive view.
…greesWithRecordedPrePrepare. We split the reasoning for proving HonestRecvPrePrepareStepPreservesUnCommitableAgreesWithRecordedPrePrepare in 2 cases (separate lemmas) for the case we have no Prepared Certificate for the Sequence ID of the PrePrepare and a case that has a set of Prepared Certificates that have to be considered. In replica.i.dfy we create a function to extract the relevant Prepared Certificate from a New View message for a given Sequence ID.
…pare lemma proof complete. Next steps proof UnCommitableIfNoCertificates and UnCommitableIfSomeCertificates since the above lemma relies on them being true. Refactors in Replica to provide deterministic definitions from chose operator.
teoparvanov
approved these changes
Jun 20, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Most recent progress on the proof for correctness of the BFT protocol. This is a WIP branch where we are proving the invariants in the presence of arbitrary number of View Changes with Checkpoint-ing and sliding of the Working Window disabled. More information in docs/sbft-formal-model/README.md
< describe automated and/or manual test scenarios >