Skip to content

Commit

Permalink
Fix strings in Z3 and make RPS ask for hands
Browse files Browse the repository at this point in the history
  • Loading branch information
@jeapostrophe
jeapostrophe committed Jul 17, 2019
1 parent 10dddd2 commit 3b4c84b
Show file tree
Hide file tree
Showing 15 changed files with 2,168 additions and 1,720 deletions.
548 changes: 283 additions & 265 deletions examples/rps-auto/build/rps.bl
View file

Large diffs are not rendered by default.

250 changes: 133 additions & 117 deletions examples/rps-auto/build/rps.il
View file
Expand Up @@ -3,129 +3,145 @@
#:participants
(define-participant A
[0/wagerAmount : uint256]
[1/escrowAmount : uint256]
[2/handA : uint256])
(define-participant B
[3/handB : uint256])
[1/escrowAmount : uint256])
(define-participant B)

#:main
(@ A (define 4/PrimApp (PLE 0 2/handA)))
(@ A (define 5/PrimApp (PLT 2/handA 3)))
(@ A (define 6/PrimApp (IF_THEN_ELSE 4/PrimApp 5/PrimApp False)))
(@ A (assume! 6/PrimApp))
(@ B (define 7/PrimApp (PLE 0 3/handB)))
(@ B (define 8/PrimApp (PLT 3/handB 3)))
(@ B (define 9/PrimApp (IF_THEN_ELSE 7/PrimApp 8/PrimApp False)))
(@ B (assume! 9/PrimApp))
(@ A (define 10/PrimApp (RANDOM)))
(@ A (define 11/PrimApp (UINT256_TO_BYTES 10/PrimApp)))
(@ A (define 12/PrimApp (UINT256_TO_BYTES 2/handA)))
(@ A (define 13/PrimApp (BCAT 11/PrimApp 12/PrimApp)))
(@ A (define 14/PrimApp (DIGEST 13/PrimApp)))
(@ A (define 15/Declassify (declassify 0/wagerAmount)))
(@ A (define 16/Declassify (declassify 1/escrowAmount)))
(@ A (define 17/Declassify (declassify 14/PrimApp)))
(@ A (define 18/PrimApp (INTERACT "commits")))
(@ A (define 19/PrimApp (ADD 15/Declassify 16/Declassify)))
(@ A (define 2/PrimApp (INTERACT "getHand")))
(@ A (define 3/PrimApp (BYTES_EQ 2/PrimApp "ROCK")))
(@ A (define 4/PrimApp (BYTES_EQ 2/PrimApp "PAPER")))
(@ A (define 5/PrimApp (BYTES_EQ 2/PrimApp "SCISSORS")))
(@ A (define 6/PrimApp (IF_THEN_ELSE 4/PrimApp True 5/PrimApp)))
(@ A (define 7/PrimApp (IF_THEN_ELSE 3/PrimApp True 6/PrimApp)))
(@ A (assume! 7/PrimApp))
(@ A (define 8/PureIf (IF_THEN_ELSE 4/PrimApp 1 2)))
(@ A (define 9/PureIf (IF_THEN_ELSE 3/PrimApp 0 8/PureIf)))
(@ A (define 10/PrimApp (PLE 0 9/PureIf)))
(@ A (define 11/PrimApp (PLT 9/PureIf 3)))
(@ A (define 12/PrimApp (IF_THEN_ELSE 10/PrimApp 11/PrimApp False)))
(@ A (assert! 12/PrimApp))
(@ A (define 13/PrimApp (RANDOM)))
(@ A (define 14/PrimApp (UINT256_TO_BYTES 13/PrimApp)))
(@ A (define 15/PrimApp (UINT256_TO_BYTES 9/PureIf)))
(@ A (define 16/PrimApp (BCAT 14/PrimApp 15/PrimApp)))
(@ A (define 17/PrimApp (DIGEST 16/PrimApp)))
(@ A (define 18/Declassify (declassify 0/wagerAmount)))
(@ A (define 19/Declassify (declassify 1/escrowAmount)))
(@ A (define 20/Declassify (declassify 17/PrimApp)))
(@ A (define 21/PrimApp (INTERACT "commits")))
(@ A (define 22/PrimApp (ADD 18/Declassify 19/Declassify)))
(@ A
(publish! (15/Declassify 16/Declassify 17/Declassify))
(pay! (20, pay-amount) 19/PrimApp))
(@ CTC (define 21/PrimApp (ADD 15/Declassify 16/Declassify)))
(@ CTC (define 22/PrimApp (PEQ 20/pay-amount 21/PrimApp)))
(@ CTC (require! 22/PrimApp))
(publish! (18/Declassify 19/Declassify 20/Declassify))
(pay! (23, pay-amount) 22/PrimApp))
(@ CTC (define 24/PrimApp (ADD 18/Declassify 19/Declassify)))
(@ CTC (define 25/PrimApp (PEQ 23/pay-amount 24/PrimApp)))
(@ CTC (require! 25/PrimApp))
(return!)
(@ B (define 23/Declassify (declassify 3/handB)))
(@ B (define 24/PrimApp (INTERACT "accepts")))
(@ B (define 26/PrimApp (INTERACT "getHand")))
(@ B (define 27/PrimApp (BYTES_EQ 26/PrimApp "ROCK")))
(@ B (define 28/PrimApp (BYTES_EQ 26/PrimApp "PAPER")))
(@ B (define 29/PrimApp (BYTES_EQ 26/PrimApp "SCISSORS")))
(@ B (define 30/PrimApp (IF_THEN_ELSE 28/PrimApp True 29/PrimApp)))
(@ B (define 31/PrimApp (IF_THEN_ELSE 27/PrimApp True 30/PrimApp)))
(@ B (assume! 31/PrimApp))
(@ B (define 32/PureIf (IF_THEN_ELSE 28/PrimApp 1 2)))
(@ B (define 33/PureIf (IF_THEN_ELSE 27/PrimApp 0 32/PureIf)))
(@ B (define 34/PrimApp (PLE 0 33/PureIf)))
(@ B (define 35/PrimApp (PLT 33/PureIf 3)))
(@ B (define 36/PrimApp (IF_THEN_ELSE 34/PrimApp 35/PrimApp False)))
(@ B (assert! 36/PrimApp))
(@ B (define 37/Declassify (declassify 33/PureIf)))
(@ B (define 38/PrimApp (INTERACT "accepts")))
(@ B
(publish! (23/Declassify))
(pay! (25, pay-amount) 15/Declassify))
(@ CTC (define 26/PrimApp (PEQ 25/pay-amount 15/Declassify)))
(@ CTC (require! 26/PrimApp))
(@ CTC (define 27/PrimApp (PLE 0 23/Declassify)))
(@ CTC (define 28/PrimApp (PLT 23/Declassify 3)))
(@ CTC (define 29/PrimApp (IF_THEN_ELSE 27/PrimApp 28/PrimApp False)))
(@ CTC (require! 29/PrimApp))
(publish! (37/Declassify))
(pay! (39, pay-amount) 18/Declassify))
(@ CTC (define 40/PrimApp (PEQ 39/pay-amount 18/Declassify)))
(@ CTC (require! 40/PrimApp))
(@ CTC (define 41/PrimApp (PLE 0 37/Declassify)))
(@ CTC (define 42/PrimApp (PLT 37/Declassify 3)))
(@ CTC (define 43/PrimApp (IF_THEN_ELSE 41/PrimApp 42/PrimApp False)))
(@ CTC (require! 43/PrimApp))
(return!)
(@ A (define 30/Declassify (declassify 10/PrimApp)))
(@ A (define 31/Declassify (declassify 2/handA)))
(@ A (define 32/PrimApp (INTERACT "reveals")))
(@ A (define 44/Declassify (declassify 13/PrimApp)))
(@ A (define 45/Declassify (declassify 9/PureIf)))
(@ A (define 46/PrimApp (INTERACT "reveals")))
(@ A
(publish! (30/Declassify 31/Declassify))
(pay! (33, pay-amount) 0))
(@ CTC (define 34/PrimApp (PEQ 33/pay-amount 0)))
(@ CTC (require! 34/PrimApp))
(@ CTC (define 35/PrimApp (UINT256_TO_BYTES 30/Declassify)))
(@ CTC (define 36/PrimApp (UINT256_TO_BYTES 31/Declassify)))
(@ CTC (define 37/PrimApp (BCAT 35/PrimApp 36/PrimApp)))
(@ CTC (define 38/PrimApp (DIGEST 37/PrimApp)))
(@ CTC (define 39/PrimApp (PEQ 17/Declassify 38/PrimApp)))
(@ CTC (require! 39/PrimApp))
(@ CTC (define 40/PrimApp (PLE 0 31/Declassify)))
(@ CTC (define 41/PrimApp (PLT 31/Declassify 3)))
(@ CTC (define 42/PrimApp (IF_THEN_ELSE 40/PrimApp 41/PrimApp False)))
(@ CTC (require! 42/PrimApp))
(@ CTC (define 43/PrimApp (PLE 0 31/Declassify)))
(@ CTC (define 44/PrimApp (PLT 31/Declassify 3)))
(@ CTC (define 45/PrimApp (IF_THEN_ELSE 43/PrimApp 44/PrimApp False)))
(@ CTC (define 46/PrimApp (PLE 0 23/Declassify)))
(@ CTC (define 47/PrimApp (PLT 23/Declassify 3)))
(@ CTC (define 48/PrimApp (IF_THEN_ELSE 46/PrimApp 47/PrimApp False)))
(@ CTC (define 49/PrimApp (IF_THEN_ELSE 45/PrimApp 48/PrimApp False)))
(@ CTC (define 50/PrimApp (SUB 4 23/Declassify)))
(@ CTC (define 51/PrimApp (ADD 31/Declassify 50/PrimApp)))
(@ CTC (define 52/PrimApp (MOD 51/PrimApp 3)))
(@ CTC (define 53/PureIf (IF_THEN_ELSE 48/PrimApp 0 1)))
(@ CTC (define 54/PureIf (IF_THEN_ELSE 45/PrimApp 2 53/PureIf)))
(@ CTC (define 55/PureIf (IF_THEN_ELSE 49/PrimApp 52/PrimApp 54/PureIf)))
(@ CTC (define 56/PrimApp (PLE 0 55/PureIf)))
(@ CTC (define 57/PrimApp (PLT 55/PureIf 3)))
(@ CTC (define 58/PrimApp (IF_THEN_ELSE 56/PrimApp 57/PrimApp False)))
(@ CTC (assert! 58/PrimApp))
(@ CTC (define 59/PrimApp (PEQ 55/PureIf 2)))
(@ CTC (define 60/PrimApp (PLE 0 31/Declassify)))
(@ CTC (define 61/PrimApp (PLT 31/Declassify 3)))
(publish! (44/Declassify 45/Declassify))
(pay! (47, pay-amount) 0))
(@ CTC (define 48/PrimApp (PEQ 47/pay-amount 0)))
(@ CTC (require! 48/PrimApp))
(@ CTC (define 49/PrimApp (UINT256_TO_BYTES 44/Declassify)))
(@ CTC (define 50/PrimApp (UINT256_TO_BYTES 45/Declassify)))
(@ CTC (define 51/PrimApp (BCAT 49/PrimApp 50/PrimApp)))
(@ CTC (define 52/PrimApp (DIGEST 51/PrimApp)))
(@ CTC (define 53/PrimApp (PEQ 20/Declassify 52/PrimApp)))
(@ CTC (require! 53/PrimApp))
(@ CTC (define 54/PrimApp (PLE 0 45/Declassify)))
(@ CTC (define 55/PrimApp (PLT 45/Declassify 3)))
(@ CTC (define 56/PrimApp (IF_THEN_ELSE 54/PrimApp 55/PrimApp False)))
(@ CTC (require! 56/PrimApp))
(@ CTC (define 57/PrimApp (PLE 0 45/Declassify)))
(@ CTC (define 58/PrimApp (PLT 45/Declassify 3)))
(@ CTC (define 59/PrimApp (IF_THEN_ELSE 57/PrimApp 58/PrimApp False)))
(@ CTC (define 60/PrimApp (PLE 0 37/Declassify)))
(@ CTC (define 61/PrimApp (PLT 37/Declassify 3)))
(@ CTC (define 62/PrimApp (IF_THEN_ELSE 60/PrimApp 61/PrimApp False)))
(@ CTC (define 63/PrimApp (IF_THEN_ELSE 59/PrimApp False True)))
(@ CTC (define 64/PrimApp (IF_THEN_ELSE 63/PrimApp True 62/PrimApp)))
(@ CTC (assert! 64/PrimApp))
(@ CTC (define 65/PrimApp (PEQ 55/PureIf 0)))
(@ CTC (define 66/PrimApp (PLE 0 23/Declassify)))
(@ CTC (define 67/PrimApp (PLT 23/Declassify 3)))
(@ CTC (define 68/PrimApp (IF_THEN_ELSE 66/PrimApp 67/PrimApp False)))
(@ CTC (define 69/PrimApp (IF_THEN_ELSE 65/PrimApp False True)))
(@ CTC (define 70/PrimApp (IF_THEN_ELSE 69/PrimApp True 68/PrimApp)))
(@ CTC (assert! 70/PrimApp))
(@ CTC (define 71/PrimApp (PEQ 55/PureIf 2)))
(@ CTC (define 72/PrimApp (MUL 2 15/Declassify)))
(@ CTC (define 73/PrimApp (PEQ 55/PureIf 0)))
(@ CTC (define 74/PrimApp (MUL 2 15/Declassify)))
(@ CTC (define 75/PureIf (IF_THEN_ELSE 73/PrimApp 0 15/Declassify)))
(@ CTC (define 76/PureIf (IF_THEN_ELSE 73/PrimApp 74/PrimApp 15/Declassify)))
(@ CTC (define 77/PureIf (IF_THEN_ELSE 71/PrimApp 72/PrimApp 75/PureIf)))
(@ CTC (define 78/PureIf (IF_THEN_ELSE 71/PrimApp 0 76/PureIf)))
(@ CTC (define 79/PrimApp (ADD 16/Declassify 77/PureIf)))
(@ CTC (transfer! A 79/PrimApp))
(@ CTC (transfer! B 78/PureIf))
(@ CTC (define 63/PrimApp (IF_THEN_ELSE 59/PrimApp 62/PrimApp False)))
(@ CTC (define 64/PrimApp (SUB 4 37/Declassify)))
(@ CTC (define 65/PrimApp (ADD 45/Declassify 64/PrimApp)))
(@ CTC (define 66/PrimApp (MOD 65/PrimApp 3)))
(@ CTC (define 67/PureIf (IF_THEN_ELSE 62/PrimApp 0 1)))
(@ CTC (define 68/PureIf (IF_THEN_ELSE 59/PrimApp 2 67/PureIf)))
(@ CTC (define 69/PureIf (IF_THEN_ELSE 63/PrimApp 66/PrimApp 68/PureIf)))
(@ CTC (define 70/PrimApp (PLE 0 69/PureIf)))
(@ CTC (define 71/PrimApp (PLT 69/PureIf 3)))
(@ CTC (define 72/PrimApp (IF_THEN_ELSE 70/PrimApp 71/PrimApp False)))
(@ CTC (assert! 72/PrimApp))
(@ CTC (define 73/PrimApp (PEQ 69/PureIf 2)))
(@ CTC (define 74/PrimApp (PLE 0 45/Declassify)))
(@ CTC (define 75/PrimApp (PLT 45/Declassify 3)))
(@ CTC (define 76/PrimApp (IF_THEN_ELSE 74/PrimApp 75/PrimApp False)))
(@ CTC (define 77/PrimApp (IF_THEN_ELSE 73/PrimApp False True)))
(@ CTC (define 78/PrimApp (IF_THEN_ELSE 77/PrimApp True 76/PrimApp)))
(@ CTC (assert! 78/PrimApp))
(@ CTC (define 79/PrimApp (PEQ 69/PureIf 0)))
(@ CTC (define 80/PrimApp (PLE 0 37/Declassify)))
(@ CTC (define 81/PrimApp (PLT 37/Declassify 3)))
(@ CTC (define 82/PrimApp (IF_THEN_ELSE 80/PrimApp 81/PrimApp False)))
(@ CTC (define 83/PrimApp (IF_THEN_ELSE 79/PrimApp False True)))
(@ CTC (define 84/PrimApp (IF_THEN_ELSE 83/PrimApp True 82/PrimApp)))
(@ CTC (assert! 84/PrimApp))
(@ CTC (define 85/PrimApp (PEQ 69/PureIf 2)))
(@ CTC (define 86/PrimApp (MUL 2 18/Declassify)))
(@ CTC (define 87/PrimApp (PEQ 69/PureIf 0)))
(@ CTC (define 88/PrimApp (MUL 2 18/Declassify)))
(@ CTC (define 89/PureIf (IF_THEN_ELSE 87/PrimApp 0 18/Declassify)))
(@ CTC (define 90/PureIf (IF_THEN_ELSE 87/PrimApp 88/PrimApp 18/Declassify)))
(@ CTC (define 91/PureIf (IF_THEN_ELSE 85/PrimApp 86/PrimApp 89/PureIf)))
(@ CTC (define 92/PureIf (IF_THEN_ELSE 85/PrimApp 0 90/PureIf)))
(@ CTC (define 93/PrimApp (ADD 19/Declassify 91/PureIf)))
(@ CTC (transfer! A 93/PrimApp))
(@ CTC (transfer! B 92/PureIf))
(return!)
(@ CTC (define 80/PrimApp (PEQ 55/PureIf 2)))
(@ CTC (define 81/PrimApp (PEQ 31/Declassify 0)))
(@ CTC (define 82/PrimApp (IF_THEN_ELSE 81/PrimApp 80/PrimApp False)))
(@ CTC (possible? 82/PrimApp))
(@ CTC (define 83/PrimApp (PEQ 31/Declassify 1)))
(@ CTC (define 84/PrimApp (IF_THEN_ELSE 83/PrimApp 80/PrimApp False)))
(@ CTC (possible? 84/PrimApp))
(@ CTC (define 85/PrimApp (PEQ 31/Declassify 2)))
(@ CTC (define 86/PrimApp (IF_THEN_ELSE 85/PrimApp 80/PrimApp False)))
(@ CTC (possible? 86/PrimApp))
(@ CTC (define 87/PrimApp (PEQ 55/PureIf 0)))
(@ CTC (define 88/PrimApp (PEQ 23/Declassify 0)))
(@ CTC (define 89/PrimApp (IF_THEN_ELSE 88/PrimApp 87/PrimApp False)))
(@ CTC (possible? 89/PrimApp))
(@ CTC (define 90/PrimApp (PEQ 23/Declassify 1)))
(@ CTC (define 91/PrimApp (IF_THEN_ELSE 90/PrimApp 87/PrimApp False)))
(@ CTC (possible? 91/PrimApp))
(@ CTC (define 92/PrimApp (PEQ 23/Declassify 2)))
(@ CTC (define 93/PrimApp (IF_THEN_ELSE 92/PrimApp 87/PrimApp False)))
(@ CTC (possible? 93/PrimApp))
(@ CTC (define 94/PrimApp (INTERACT "outcome")))
55/PureIf
(@ CTC (define 94/PrimApp (PEQ 69/PureIf 2)))
(@ CTC (define 95/PrimApp (PEQ 45/Declassify 0)))
(@ CTC (define 96/PrimApp (IF_THEN_ELSE 95/PrimApp 94/PrimApp False)))
(@ CTC (possible? 96/PrimApp))
(@ CTC (define 97/PrimApp (PEQ 45/Declassify 1)))
(@ CTC (define 98/PrimApp (IF_THEN_ELSE 97/PrimApp 94/PrimApp False)))
(@ CTC (possible? 98/PrimApp))
(@ CTC (define 99/PrimApp (PEQ 45/Declassify 2)))
(@ CTC (define 100/PrimApp (IF_THEN_ELSE 99/PrimApp 94/PrimApp False)))
(@ CTC (possible? 100/PrimApp))
(@ CTC (define 101/PrimApp (PEQ 69/PureIf 0)))
(@ CTC (define 102/PrimApp (PEQ 37/Declassify 0)))
(@ CTC (define 103/PrimApp (IF_THEN_ELSE 102/PrimApp 101/PrimApp False)))
(@ CTC (possible? 103/PrimApp))
(@ CTC (define 104/PrimApp (PEQ 37/Declassify 1)))
(@ CTC (define 105/PrimApp (IF_THEN_ELSE 104/PrimApp 101/PrimApp False)))
(@ CTC (possible? 105/PrimApp))
(@ CTC (define 106/PrimApp (PEQ 37/Declassify 2)))
(@ CTC (define 107/PrimApp (IF_THEN_ELSE 106/PrimApp 101/PrimApp False)))
(@ CTC (possible? 107/PrimApp))
(@ CTC (define 108/PrimApp (INTERACT "outcome")))
69/PureIf

0 comments on commit 3b4c84b

Please sign in to comment.