-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.rsh v0.4
95 lines (83 loc) · 2.3 KB
/
index.rsh v0.4
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
/*
* This version features nested while loops. One for the players interaction,
* the other for the dealer. Player can hit as much as they like, Dealer must hit below 15
*/
'reach 0.1';
// this considers aces high
const cardValue = (x) => (x == 1 ? 11 : (x < 10 ? x : 10))
const Shared = {
...hasRandom,
seeTotal: Fun([UInt], Null),
getCard: Fun([], UInt),
startGame: Fun([], Tuple(UInt, UInt)),
};
export const main = Reach.App(() => {
const Player = Participant('Player', {
...Shared,
wager: UInt,
// Specify Alice's interact interface here
});
const Dealer = Participant('Dealer', {
...Shared,
autoCard: Fun([], UInt),
// Specify Bob's interact interface here
});
init();
Player.only(() => {
const wager = declassify(interact.wager);
const [cardA, cardB] = declassify(interact.startGame());
});
// The first one to publish deploys the contract
Player.publish(wager, cardA, cardB)
.pay(wager);
commit();
// The second one to publish always attaches
Dealer.pay(wager);
commit();
Dealer.only(() => {
const [dealerCardA, dealerCardB] = declassify(interact.startGame());
});
Dealer.publish(dealerCardA, dealerCardB);
// outer loop is the dealer
var [sumB, flag] = [(cardValue(dealerCardA)+cardValue(dealerCardB)),0];
invariant(balance() == 2 * wager);
while(flag == 0){
commit();
Dealer.publish();
var [sumA, flagB] = [(cardValue(cardA)+cardValue(cardB)), 0];
invariant(balance() == 2 * wager);
// inner loop is the player
while(flagB == 0){
commit();
Player.only(() => {
interact.seeTotal(sumA);
const next = declassify(interact.getCard());
});
Player.publish(next);
if(next > 0){
[sumA ,flagB] = [(cardValue(next)+sumA), 0];
continue;
} else {
[sumA, flagB] = [sumA, 1];
continue;
}
};
if((sumB) < 15){
Dealer.only(() => {
const dealerCard = declassify(interact.autoCard());
});
commit();
Dealer.publish(dealerCard);
[sumB, flag] = [((cardValue(dealerCard))+sumB), 1];
continue;
} else {
[sumB, flag] = [sumB, 1];
continue;
}
};
// we can only use cardA and cardB values after we publish here
transfer(2 * wager).to(Dealer);
//assert(flag == 1);
commit();
exit();
});