Closed jeapostrophe closed 5 years ago
The following patches violate the assertions on the listed lines
Line 54:
--- a/examples/rps-auto/rps/rps.ala +++ b/examples/rps-auto/rps/rps.ala @@ -37,7 +37,7 @@ participant B { main { @A assume! isHand(handA); - @B assume! isHand(handB); + // @B assume! isHand(handB); @A const commitA, saltA = precommit(handA); @A declassify! wagerAmount;
Line 61:
--- a/examples/rps-auto/rps/rps.ala +++ b/examples/rps-auto/rps/rps.ala @@ -55,6 +55,7 @@ main { return; @A declassify! saltA; + @A const handA = ROCK; @A declassify! handA; @A interact("reveals"); @A publish! saltA, handA w/ 0;
Line 62:
--- a/examples/rps-auto/rps/rps.ala +++ b/examples/rps-auto/rps/rps.ala @@ -36,7 +36,7 @@ participant B { uint256 handB } main { - @A assume! isHand(handA); + // @A assume! isHand(handA); @B assume! isHand(handB); @A const commitA, saltA = precommit(handA);
Line 64:
--- a/examples/rps-auto/rps/rps.ala +++ b/examples/rps-auto/rps/rps.ala @@ -6,7 +6,7 @@ enum isOutcome { B_WINS, DRAW, A_WINS }; function winner(handA, handB) : isOutcome { const validA = isHand(handA); const validB = isHand(handB); - if (validA && validB) { + if (true || (validA && validB)) { ((handA + (4 - handB)) % 3) } else if validA { A_WINS } @@ -59,7 +59,7 @@ main { @A interact("reveals"); @A publish! saltA, handA w/ 0; check_commit(commitA, saltA, handA); - require! isHand(handA); + // require! isHand(handA); const outcome = winner(handA, handB); assert! ((outcome == A_WINS) => isHand(handA)); assert! ((outcome == B_WINS) => isHand(handB));
Line 65:
--- a/examples/rps-auto/rps/rps.ala +++ b/examples/rps-auto/rps/rps.ala @@ -6,7 +6,7 @@ enum isOutcome { B_WINS, DRAW, A_WINS }; function winner(handA, handB) : isOutcome { const validA = isHand(handA); const validB = isHand(handB); - if (validA && validB) { + if (true || (validA && validB)) { ((handA + (4 - handB)) % 3) } else if validA { A_WINS } @@ -51,7 +51,7 @@ main { @B declassify! handB; @B interact("accepts"); @B publish! handB w/ wagerAmount; - require! isHand(handB); + // require! isHand(handB); return; @A declassify! saltA;
Line 77:
--- a/examples/rps-auto/rps/rps.ala +++ b/examples/rps-auto/rps/rps.ala @@ -13,7 +13,7 @@ function winner(handA, handB) : isOutcome { else if validB { B_WINS } else { - DRAW } } + DRAW }; A_WINS } function fair_if(handX, optionX, canWinX) { possible? ((handX == optionX) && canWinX) }
The A_WINS could be B_WINS or DRAW
A_WINS
B_WINS
DRAW
The following patches violate the assertions on the listed lines
Line 54:
Line 61:
Line 62:
Line 64:
Line 65:
Line 77:
The
A_WINS
could beB_WINS
orDRAW