Skip to content

Commit

Permalink
Fix wrong constraint assertSendCVIfNotCommitAndYesPrimary
Browse files Browse the repository at this point in the history
  • Loading branch information
@vncoelho
vncoelho committed Jun 19, 2020
1 parent 66f2264 commit 33c02cd
Show file tree
Hide file tree
Showing 4 changed files with 304 additions and 44 deletions.
86 changes: 43 additions & 43 deletions dbft2.0/dbft2.0_Byz_Liveness.mod
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,15 +43,15 @@ var RecvCV{T,R,R,V}, binary;
var totalBlockRelayed, integer, >= 0;
var lastRelayedBlock, integer, >= 0;
var numberOfRounds, integer, >= 0;
var prepReqSendPerNodeAndView{R,V}, integer, >= 0;
var prepRespSendPerNodeAndView{R,V}, integer, >= 0;
var commitSendPerNodeAndView{R,V}, integer, >= 0;
var changeViewSendPerNodeAndView{R,V}, integer, >= 0;
var prepReqRecvPerNodeAndView{R,V}, integer, >= 0;
var prepRespRecvPerNodeAndView{R,V}, integer, >= 0;
#var prepReqSendPerNodeAndView{R,V}, integer, >= 0;
#var prepRespSendPerNodeAndView{R,V}, integer, >= 0;
#var commitSendPerNodeAndView{R,V}, integer, >= 0;
#var changeViewSendPerNodeAndView{R,V}, integer, >= 0;
#var prepReqRecvPerNodeAndView{R,V}, integer, >= 0;
#var prepRespRecvPerNodeAndView{R,V}, integer, >= 0;
var changeViewRecvPerNodeAndView{R,V}, integer, >= 0;
var commitRecvPerNodeAndView{R,V}, integer, >= 0;
var blockRelayPerNodeAndView{R,V}, integer, >= 0;
#var commitRecvPerNodeAndView{R,V}, integer, >= 0;
#var blockRelayPerNodeAndView{R,V}, integer, >= 0;
/* ==================== */
/* AUXILIARY VARIABLES */
/* =================== */
Expand Down Expand Up @@ -80,13 +80,13 @@ initializeBlockRelay{i in R, v in V}: BlockRelay[1, i, v] = 0;
# Consensus should start on the first round
consensusShouldStart: sum{i in R} Primary[i,1] = 1;
singlePrimaryEveryView{v in V}: sum{i in R} Primary[i,v] <= 1;
primaryOnlyOnce{i in R}: sum{v in V} Primary[i,v] <= 1;
primaryOO{i in R}: sum{v in V} Primary[i,v] <= 1;
/* Ensure circular behavior, if previous Primary not found and conclusions not done we can not move on.
Primary should had fault, at least*/
avoidJumpingViews{v in V: v>1}: sum{i in R} Primary[i,v]*(v-1) <= sum{v2 in V:v2<v} sum{i in R} Primary[i,v2];
/* You should proof you have certificates to be the Primary,
proof the changeviews message records of previous view*/
nextPrimaryOnlyIfEnoughCV{i in R, v in V: v>1}: Primary[i,v] <= changeViewRecvPerNodeAndView[i,v-1]/M;
nextPrimaryOnlyIfEnoughCV{i in R, v in V: v>1}: Primary[i,v] <= (1/M) * changeViewRecvPerNodeAndView[i,v-1];
/* ==================== */
/* Primary constraints */
/* ==================== */
Expand All @@ -99,10 +99,10 @@ nextPrimaryOnlyIfEnoughCV{i in R, v in V: v>1}: Primary[i,v] <= changeViewRecvPe
# PrepRequest Received instantaneously when Self Sended (SS)
# Only Recv if it was sended before, otherwise it is infeasible
# --------- General comments -------------
prepReqOnlyOnceAndSentOptionally{i in R, v in V}: sum{t in T: t>1} SendPrepReq[t,i,v] <= Primary[i,v];
prepReqOOIfPrimary{i in R, v in V}: sum{t in T: t>1} SendPrepReq[t,i,v] <= Primary[i,v];
prepReqReceivedSS{t in T, i in R, v in V: t>1}: RecvPrepReq[t,i,i,v] = SendPrepReq[t,i,v];
prepReqReceived{t in T, i in R, j in R, v in V: t>1 and j!=i}: RecvPrepReq[t,i,j,v] <= sum{t2 in T: t2<t and t2>1} SendPrepReq[t2,j,v];
prepReqReceivedOnlyOnce{i in R, j in R, v in V}: sum{t in T: t>1} RecvPrepReq[t,i,j,v] <= 1;
rcvdPrepReqOO{i in R, j in R, v in V}: sum{t in T: t>1} RecvPrepReq[t,i,j,v] <= 1;
prepResReceivedAlongWithPrepReq{t in T, i in R, j in R, v in V: t>1}: RecvPrepResp[t,i,j,v] >= RecvPrepReq[t,i,j,v];
/* ==================== */
/* Prepare Request (PrepReq) constraints */
Expand All @@ -111,43 +111,43 @@ prepResReceivedAlongWithPrepReq{t in T, i in R, j in R, v in V: t>1}: RecvPrepRe
/* ==================== */
/* Prepare Response (PreRes) constraints */
/* ==================== */
sendPrepResonseOnlyOnce{i in R, v in V}: sum{t in T: t>1} SendPrepRes[t,i,v] <= 1;
sendPrepResOO{i in R, v in V}: sum{t in T: t>1} SendPrepRes[t,i,v] <= 1;
prepRespSendOptionally{t in T, i in R, v in V: t>1}: SendPrepRes[t,i,v] <= sum{t2 in T:t2<=t} sum{j in R} RecvPrepReq[t2,i,j,v];
prepRespReceivedSS{t in T, i in R, v in V: t>1}: RecvPrepResp[t,i,i,v] = SendPrepRes[t,i,v];
prepRespReceived{t in T, i in R, j in R, v in V: t>1 and j!=i}: RecvPrepResp[t,i,j,v] <= sum{t2 in T: t2<t and t2>1} SendPrepRes[t2,j,v];
receivedPrepResponseOnlyOnce{i in R, j in R, v in V}: sum{t in T: t>1} RecvPrepResp[t,i,j,v] <= 1;
rcvdPrepResOO{i in R, j in R, v in V}: sum{t in T: t>1} RecvPrepResp[t,i,j,v] <= 1;
/* ==================== */
/* Prepare Response (PreRes) constraints */
/* ==================== */

/* ==================== */
/* Commit constraints */
/* ==================== */
sendCommitOnlyOnce{i in R, v in V}: sum{t in T: t>1} SendCommit[t,i,v] <= 1;
commitSentIfMPrepRespOptionally{t in T, i in R, v in V: t>1}: SendCommit[t,i,v] <= (sum{t2 in T: t2<=t} sum{j in R} RecvPrepResp[t2,i,j,v])/M;
sendCommitOO{i in R, v in V}: sum{t in T: t>1} SendCommit[t,i,v] <= 1;
commitSentIfMPrepRespOptionally{t in T, i in R, v in V: t>1}: SendCommit[t,i,v] <= (1/M) * sum{t2 in T: t2<=t} sum{j in R} RecvPrepResp[t2,i,j,v];
commitReceivedSS{t in T, i in R, v in V: t>1}: RecvCommit[t,i,i,v] = SendCommit[t,i,v];
commitReceived{t in T, i in R, j in R, v in V: t>1 and j!=i}: RecvCommit[t,i,j,v] <= sum{t2 in T: t2<t and t2>1} SendCommit[t2,j,v];
receivedCommitOnlyOnce{i in R, j in R, v in V}: sum{t in T: t>1} RecvCommit[t,i,j,v] <= 1;
rcvdCommitOO{i in R, j in R, v in V}: sum{t in T: t>1} RecvCommit[t,i,j,v] <= 1;
/* ==================== */
/* Commit constraints */
/* ==================== */

/* ==================== */
/* Change View (CV) constraints */
/* ==================== */
sendCVOnlyOncePerView{i in R, v in V}: sum{t in T: t>1} SendCV[t,i,v] <= 1;
receivedCVSS{t in T, i in R, v in V: t>1}: RecvCV[t,i,i,v] = SendCV[t,i,v];
receivedCV{t in T, i in R, j in R, v in V: t>1 and j!=i}: RecvCV[t,i,j,v] <= sum{t2 in T: t2<t and t2>1} SendCV[t2,j,v];
receivedCVOnlyOnce{i in R, j in R, v in V}: sum{t in T: t>1} RecvCV[t,i,j,v] <= 1;
sendCVOO{i in R, v in V}: sum{t in T: t>1} SendCV[t,i,v] <= 1;
cvReceivedSS{t in T, i in R, v in V: t>1}: RecvCV[t,i,i,v] = SendCV[t,i,v];
cvReceived{t in T, i in R, j in R, v in V: t>1 and j!=i}: RecvCV[t,i,j,v] <= sum{t2 in T: t2<t and t2>1} SendCV[t2,j,v];
rcvdCVOO{i in R, j in R, v in V}: sum{t in T: t>1} RecvCV[t,i,j,v] <= 1;
/* ==================== */
/* Change View (CV) constraints */
/* ==================== */

/* ==================== */
/* Block Relay constraints */
/* ==================== */
blockRelayOptionallyOnlyIfEnoughCommits{t in T, i in R, v in V: t>1}: BlockRelay[t, i, v] <= (sum{t2 in T: t2<=t} sum{j in R} RecvCommit[t2,i,j,v])/M;
blockRelayOnlyOncePerView{i in R, v in V}: sum{t in T} BlockRelay[t,i,v] <= 1;
blockRelayOptionallyOnlyIfEnoughCommits{t in T, i in R, v in V: t>1}: BlockRelay[t, i, v] <= (1/M) * sum{t2 in T: t2<=t} sum{j in R} RecvCommit[t2,i,j,v];
blockRelayOO{i in R, v in V}: sum{t in T: t>1} BlockRelay[t,i,v] <= 1;
blockRelayedOnlyIfNodeRelay{v in V}: blockRelayed[v] <= sum{t in T: t>1} sum{i in R} BlockRelay[t, i, v];
blockRelayedCounterForced{v in V}: blockRelayed[v]*N >= sum{t in T: t>1} sum{i in R} BlockRelay[t, i, v];
/* ==================== */
Expand Down Expand Up @@ -175,25 +175,25 @@ Byz can Relay (HOLD) and never arrive */
blockRelayLimitToOneForNonByz{i in R_OK}: sum{t in T: t>1} sum{v in V} BlockRelay[t,i,v] <= 1;

/* Force a Primary to exist if any honest knows change views - 2 acts as BIGNUM */
assertAtLeastOnePrimaryIfEnoughCV{i in R_OK, v in V: v>1}: (sum{ii in R} Primary[ii,v])*2 >= (changeViewRecvPerNodeAndView[i,v-1] - M + 1);
assertAtLeastOnePrimaryIfEnoughCV{i in R_OK, v in V: v>1}: (2 * sum{ii in R} Primary[ii,v]) >= changeViewRecvPerNodeAndView[i,v-1] - M + 1;

/* We assume that honest nodes will perform an action within the simulation limits*/
assertSendPrepReqWithinSimLimit {i in R_OK, v in V}: sum{t in T: t>1} SendPrepReq[t,i,v] >= Primary[i,v];
assertSendPrepResWithinSimLimit {i in R_OK, v in V}: sum{t in T: t>1} SendPrepRes[t,i,v] >= sum{t in T: t>1} sum{j in R} RecvPrepReq[t,i,j,v];
assertSendCommitWithinSimLimit {i in R_OK, v in V}: (sum{t in T: t>1} SendCommit[t,i,v])*2 >= ((sum{t in T: t>1} sum{j in R} RecvPrepResp[t,i,j,v]) - M + 1);
assertBlockRelayWithinSimLimit {i in R_OK, v in V}: (sum{t in T: t>1} BlockRelay[t,i,v])*2 >= ((sum{t in T: t>1} sum{j in R} RecvCommit[t,i,j,v]) - M + 1);
assertSendPrepResWithinSimLimit {i in R_OK, v in V}: sum{t in T: t>1} SendPrepRes[t,i,v] >= sum{t in T: t>1} sum{j in R} RecvPrepReq[t,i,j,v];
assertSendCommitWithinSimLimit {i in R_OK, v in V}: (sum{t in T: t>1} 2*SendCommit[t,i,v]) >= (sum{t in T: t>1} sum{j in R} RecvPrepResp[t,i,j,v]) - M + 1;
assertBlockRelayWithinSimLimit {i in R_OK, v in V}: (sum{t in T: t>1} 2*BlockRelay[t,i,v]) >= (sum{t in T: t>1} sum{j in R} RecvCommit[t,i,j,v]) - M + 1;

/* We assume that honest nodes will only perform an action if view change was approved - no view jumps
- not tested if really needed */
sendPrepReqOnlyIfViewBeforeOk {i in R_OK, v in V: v>1}: sum{t in T: t>1} SendPrepReq[t,i,v] <= changeViewRecvPerNodeAndView[i,v-1]/M;
sendPrepResOnlyIfViewBeforeOk {i in R_OK, v in V: v>1}: sum{t in T: t>1} SendPrepRes[t,i,v] <= changeViewRecvPerNodeAndView[i,v-1]/M;
sendCommitOnlyIfViewBeforeOk {i in R_OK, v in V: v>1}: sum{t in T: t>1} SendCommit[t,i,v] <= changeViewRecvPerNodeAndView[i,v-1]/M;
sendCVNextViewOnlyIfViewBeforeOk {i in R_OK, v in V: v>1}: sum{t in T: t>1} SendCV[t,i,v] <= changeViewRecvPerNodeAndView[i,v-1]/M;
sendPrepReqOnlyIfViewBeforeOk {i in R_OK, v in V: v>1}: sum{t in T: t>1} SendPrepReq[t,i,v] <= (1/M) * changeViewRecvPerNodeAndView[i,v-1];
sendPrepResOnlyIfViewBeforeOk {i in R_OK, v in V: v>1}: sum{t in T: t>1} SendPrepRes[t,i,v] <= (1/M) * changeViewRecvPerNodeAndView[i,v-1];
sendCommitOnlyIfViewBeforeOk {i in R_OK, v in V: v>1}: sum{t in T: t>1} SendCommit[t,i,v] <= (1/M) * changeViewRecvPerNodeAndView[i,v-1];
sendCVNextViewOnlyIfViewBeforeOk {i in R_OK, v in V: v>1}: sum{t in T: t>1} SendCV[t,i,v] <= (1/M) * changeViewRecvPerNodeAndView[i,v-1];

/* Assert Non-byz to SendCV every round, if commit not achieved
After first round we need to ensure circular behavior in order to not force if round is not active */
assertSendCVIfNotSendCommitV1 {i in R_OK}: sum{t in T: t>1} SendCV[t,i,1] >= 1 - sum{t in T: t>1} SendCommit[t,i,1];
assertSendCVIfNotCommitAndYesPrimary{i in R_OK, v in V: v>1}: sum{t in T: t>1} SendCV[t,i,v] >= 1 - sum{t in T: t>1} SendCommit[t,i,v-1] - (1 - sum{ii in R} Primary[ii,v-1]);
assertSendCVIfNotCommitAndYesPrimary{i in R_OK, v in V: v>1}: sum{t in T: t>1} SendCV[t,i,v] >= 1 - sum{t in T: t>1} SendCommit[t,i,v] - (1 - sum{ii in R} Primary[ii,v-1]);
# The following four constraints may soon be excluded - Where used on old tests
#assertSendCVIfNotRecvPrepReqV1{i in R_OK}: sum{t in T: t>1} SendCV[t,i,1] >= (1 - sum{j in R} sum{t in T: t>1} RecvPrepReq[t,i,j,1]);
#assertSendCVIfNotEnoughPrepResV1{i in R_OK}: sum{t in T: t>1} SendCV[t,i,1]*2 >= (M - sum{j in R} sum{t in T: t>1} RecvPrepResp[t,i,j,1]);
Expand All @@ -207,10 +207,10 @@ noCommitIfCV {i in R_OK, v in V, t in T: t>1}: SendCommit[t,i,v] <= 1 - sum
/* LINKS Commit and LIMITS - analogous as the constrains for SendCV*/
noCVIfCommit {i in R_OK, v in V, t in T: t>1}: SendCV[t,i,v] <= 1 - sum{t2 in T: t2<=t and t2>1} SendCommit[t2,i,v];
/* LINKS BlockRelayed and LIMITS - analogous as the constrains for SendCV */
noBlockYesCV {i in R_OK, v in V, t in T: t>1}: SendCV[t,i,v] <= 1 - sum{t2 in T: t2<=t and t2>1} BlockRelay[t2,i,v];
noBlockYesPrepReq{i in R_OK, v in V, t in T: t>1}: SendPrepReq[t,i,v] <= 1 - sum{t2 in T: t2<=t and t2>1} BlockRelay[t2,i,v];
noBlockYesPrepRes{i in R_OK, v in V, t in T: t>1}: SendPrepRes[t,i,v] <= 1 - sum{t2 in T: t2<=t and t2>1} BlockRelay[t2,i,v];
noBlockYesCommit {i in R_OK, v in V, t in T: t>1}: SendCommit[t,i,v] <= 1 - sum{t2 in T: t2<=t and t2>1} BlockRelay[t2,i,v];
noBlockYesCV {i in R_OK, v in V, t in T: t>1}: SendCV[t,i,v] <= 1 - sum{t2 in T: t2<=t and t2>1} BlockRelay[t2,i,v];
/* LINKS BlockRelayed and LIMITS in past views */
noBlockOldViewsYesPrimary {i in R_OK, v in V: v>1}: Primary[i,v] <= 1 - sum{t in T: t>1} sum{v2 in V: v2<v} BlockRelay[t,i,v2];
noBlockOldViewsYesPrepReq {i in R_OK, v in V: v>1}: sum{t in T: t>1} SendPrepReq[t,i,v] <= 1 - sum{t in T: t>1} sum{v2 in V: v2<v} BlockRelay[t,i,v2];
Expand All @@ -230,14 +230,14 @@ noCommitOldViewsYesCV {i in R_OK, v in V: v>1}: sum{t in T: t>1} SendCV[t,i,
/* ==================== */
calcSumBlockRelayed: totalBlockRelayed = sum{v in V} blockRelayed[v];
calcTotalPrimaries: numberOfRounds = sum{i in R} sum{v in V} Primary[i,v];
calcPrepReqSendEveryNodeAndView{i in R, v in V}: prepReqSendPerNodeAndView[i,v] = sum{t in T} SendPrepReq[t,i,v]*t;
calcPrepRespSendEveryNodeAndView{i in R, v in V}: prepRespSendPerNodeAndView[i,v] = sum{t in T} SendPrepRes[t,i,v]*t;
calcCommitSendEveryNodeAndView{i in R, v in V}: commitSendPerNodeAndView[i,v] = sum{t in T} SendCommit[t,i,v]*t;
calcCVSendEveryNodeAndView{i in R, v in V}: changeViewSendPerNodeAndView[i,v] = sum{t in T} SendCV[t,i,v]*t;
calcBlockRelayEveryNodeAndView{i in R, v in V}: blockRelayPerNodeAndView[i,v] = sum{t in T} BlockRelay[t,i,v]*t;
calcPrepReqEveryNodeAndView{i in R, v in V}: prepReqRecvPerNodeAndView[i,v] = (sum{j in R} sum{t in T} RecvPrepReq[t,i,j,v]*t);
calcPrepResponseEveryNodeAndView{i in R, v in V}: prepRespRecvPerNodeAndView[i,v] = (sum{j in R} sum{t in T} RecvPrepResp[t,i,j,v]);
calcCommitEveryNodeAndView{i in R, v in V}: commitRecvPerNodeAndView[i,v] = (sum{j in R} sum{t in T} RecvCommit[t,i,j,v]);
#calcPrepReqSendEveryNodeAndView{i in R, v in V}: prepReqSendPerNodeAndView[i,v] = sum{t in T} SendPrepReq[t,i,v]*t;
#calcPrepRespSendEveryNodeAndView{i in R, v in V}: prepRespSendPerNodeAndView[i,v] = sum{t in T} SendPrepRes[t,i,v]*t;
#calcCommitSendEveryNodeAndView{i in R, v in V}: commitSendPerNodeAndView[i,v] = sum{t in T} SendCommit[t,i,v]*t;
#calcCVSendEveryNodeAndView{i in R, v in V}: changeViewSendPerNodeAndView[i,v] = sum{t in T} SendCV[t,i,v]*t;
#calcBlockRelayEveryNodeAndView{i in R, v in V}: blockRelayPerNodeAndView[i,v] = sum{t in T} BlockRelay[t,i,v]*t;
#calcPrepReqEveryNodeAndView{i in R, v in V}: prepReqRecvPerNodeAndView[i,v] = (sum{j in R} sum{t in T} RecvPrepReq[t,i,j,v]*t);
#calcPrepResponseEveryNodeAndView{i in R, v in V}: prepRespRecvPerNodeAndView[i,v] = (sum{j in R} sum{t in T} RecvPrepResp[t,i,j,v]);
#calcCommitEveryNodeAndView{i in R, v in V}: commitRecvPerNodeAndView[i,v] = (sum{j in R} sum{t in T} RecvCommit[t,i,j,v]);
calcChangeViewEveryNodeAndView{i in R, v in V}: changeViewRecvPerNodeAndView[i,v] = (sum{j in R} sum{t in T} RecvCV[t,i,j,v]);
/* Constraints for defining a lower limit for lastRelayedBlock variable
On Maximization problems it should be multiplied by *-1 if the goal is to minimize the time for relaying */
Expand All @@ -250,9 +250,9 @@ calcLastRelayedBlockMaxProblem{t in T, i in R, v in V}: lastRelayedBlock >= ((v-
/* OBJ FUNCTION */
/* ==================== */
#minimize obj: totalBlockRelayed;
minimize obj: totalBlockRelayed*1000 + numberOfRounds*100;
#minimize obj: totalBlockRelayed*1000 + numberOfRounds*100;
#maximize obj: totalBlockRelayed*1000 + lastRelayedBlock*-1;
#maximize obj: totalBlockRelayed*1000 + numberOfRounds*100;
maximize obj: totalBlockRelayed*1000 + numberOfRounds;
#maximize obj: totalBlockRelayed*100 + lastRelayedBlock + sum{i in R} sum{v in V} changeViewRecvPerNodeAndView[i,v];
/* ==================== */
/* OBJ FUNCTION */
Expand Down
2 changes: 1 addition & 1 deletion dbft2.0/dbft2.0_Byz_Liveness.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -419,7 +419,7 @@
for (i, v) in product(R_OK, V - {1}):
m += (
xsum(SendCV[t, i, v] for t in T - {1})
>= 1 - xsum(SendCommit[t, i, v - 1] for t in T - {1}) - (1 - xsum(Primary[ii, v - 1] for ii in R)),
>= 1 - xsum(SendCommit[t, i, v] for t in T - {1}) - (1 - xsum(Primary[ii, v - 1] for ii in R)),
"assertSendCVIfNotCommitAndYesPrimary(%s,%s)" % (i, v),
)

Expand Down
Loading

0 comments on commit 33c02cd

Please sign in to comment.