/
remote_state_reads.scilla
176 lines (149 loc) · 6.58 KB
/
remote_state_reads.scilla
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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
scilla_version 0
library RRLib
(* Tests various aspects of address types and remote state reads *)
type AddressADT =
| Address1 of ByStr20 with end
| Address2 of ByStr20 with contract field admin : ByStr20 with end end
contract RRContract (
(* Any address in use *)
cparam1: ByStr20 with end,
(* Any contract address *)
cparam2: ByStr20 with contract end,
(* Address with various fields *)
cparam3: ByStr20 with contract
field transactionCount : Uint32,
field admin : ByStr20 with end,
field owners : Map (ByStr20 with end) Bool,
field signatures : Map Uint32 (Map (ByStr20 with end) Bool),
field other_map : Map Uint128 (ByStr20 with end)
end)
field assign_test_1 : ByStr20 with end = cparam3
field assign_test_2 : ByStr20 with contract field transactionCount : Uint32 end = cparam3
field assign_test_3 : ByStr20 with contract field admin : ByStr20 with end end = cparam3
field assign_test_4 : ByStr20 with contract field admin : ByStr20 end = cparam3
field assign_test_5 : ByStr20 with contract field owners : Map ByStr20 Bool end = cparam3
field assign_test_6 : ByStr20 with contract field signatures : Map Uint32 (Map ByStr20 Bool) end = cparam3
field assign_test_7 : ByStr20 with contract field other_map : Map Uint128 ByStr20 end = cparam3
field assign_test_8 : AddressADT = Address1 cparam1
field assign_test_9 : List AddressADT = Nil {AddressADT}
field assign_test_10 : Map Uint128 (Map Uint128 AddressADT) = Emp Uint128 (Map Uint128 AddressADT)
field remote_reads_test_res_1_1 : Uint128 = Uint128 0 (* _balance of remote1 *)
field remote_reads_test_res_2_1 : Uint128 = Uint128 0 (* _balance of remote2 *)
field remote_reads_test_res_3_1 : Uint128 = Uint128 0 (* _balance of remote3 *)
field remote_reads_test_res_3_3 : Uint32 = Uint32 0 (* transactionCount of remote3 *)
field remote_reads_test_res_3_4 : ByStr20 with end = cparam3 (* admin of remote3 *)
field remote_reads_test_res_3_5 : Uint128 = Uint128 0 (* _balance of admin of remote3 *)
field remote_reads_test_res_3_6 : Map (ByStr20 with end) Bool = Emp (ByStr20 with end) Bool (* owners of remote3 *)
field remote_reads_test_res_3_7 : Bool = True (* exists of owners[key] in remote3 *)
field remote_reads_test_res_3_8 : Option Bool = let x = True in Some {Bool} x (* owners[key] in remote3 *)
field remote_reads_test_res_3_9 : Map Uint32 (Map (ByStr20 with end) Bool) = Emp Uint32 (Map (ByStr20 with end) Bool) (* signatures of remote3 *)
field remote_reads_test_res_3_10 : Bool = False (* exists of signatures[key] of remote3 *)
field remote_reads_test_res_3_11 : Option (Map (ByStr20 with end) Bool) = None {Map (ByStr20 with end) Bool} (* signatures[key] of remote3 *)
field remote_reads_test_res_3_12 : Bool = False (* exists signatures[key1][key2] of remote3 *)
field remote_reads_test_res_3_13 : Option Bool = None {Bool} (* signatures[key1][key2] of remote3 *)
field sender_balance_pre : Uint128 = Uint128 0
field sender_balance_mid : Uint128 = Uint128 0
field sender_balance_post : Uint128 = Uint128 0
transition RemoteReadsTest(
(* Any address in use *)
remote1: ByStr20 with end,
(* Any contract address *)
remote2: ByStr20 with contract end,
(* Address with various fields *)
remote3: ByStr20 with contract
field transactionCount : Uint32,
field admin : ByStr20 with end,
field owners : Map (ByStr20 with end) Bool,
field signatures : Map Uint32 (Map ByStr20 with end Bool)
end)
tmp_1_1 <-& remote1._balance;
remote_reads_test_res_1_1 := tmp_1_1;
tmp_2_1 <-& remote2._balance;
remote_reads_test_res_2_1 := tmp_2_1;
tmp_3_1 <-& remote3._balance;
remote_reads_test_res_3_1 := tmp_3_1;
tmp_3_3 <-& remote3.transactionCount;
remote_reads_test_res_3_3 := tmp_3_3;
tmp_3_4 <-& remote3.admin;
remote_reads_test_res_3_4 := tmp_3_4;
tmp_3_5 <-& tmp_3_4._balance;
remote_reads_test_res_3_5 := tmp_3_5;
tmp_3_6 <-& remote3.owners;
remote_reads_test_res_3_6 := tmp_3_6;
tmp_3_7 <-& exists remote3.owners[_sender];
remote_reads_test_res_3_7 := tmp_3_7;
tmp_3_8 <-& remote3.owners[_sender];
remote_reads_test_res_3_8 := tmp_3_8;
tmp_3_9 <-& remote3.signatures;
remote_reads_test_res_3_9 := tmp_3_9;
x = Uint32 0;
tmp_3_10 <-& exists remote3.signatures[x];
remote_reads_test_res_3_10 := tmp_3_10;
tmp_3_11 <-& remote3.signatures[x];
remote_reads_test_res_3_11 := tmp_3_11;
tmp_3_12 <-& exists remote3.signatures[x][_origin];
remote_reads_test_res_3_12 := tmp_3_12;
tmp_3_13 <-& remote3.signatures[x][_origin];
remote_reads_test_res_3_13 := tmp_3_13
end
(* Test the dynamic typecheck of ADT values *)
transition RemoteReadsADTTest(
list1 : List (ByStr20 with end),
list2 : List (ByStr20 with contract field f : Uint128 end),
list3 : List (ByStr20 with contract field g : AddressADT end),
pair1 : Pair (ByStr20 with end) AddressADT,
adt1 : AddressADT,
remote1: ByStr20 with contract field h : Map Uint128 AddressADT end)
end
(* Test that outgoing messages and events use ByStr20 for type info, and not the full address type
Also test that this is the case for EventInfo *)
transition OutgoingMsgTest()
msg = {_tag: "";
_recipient : _sender;
_amount : Uint128 0;
param : cparam3 };
msgs = let n = Nil {Message} in
Cons {Message} msg n;
send msgs;
e1 = { _eventname : "TestEvent";
info : cparam2 };
event e1;
e2 = { _eventname : "TestEvent";
info : cparam3 };
event e2
end
(* Test that exceptions use ByStr20 for type info, and not the full address type *)
transition ExceptionTest()
e = {_exception : "TestException";
value : cparam3 };
throw e
end
transition AssignTest()
x = Address2 cparam3;
assign_test_8 := x;
y = let n = Nil {AddressADT} in
Cons {AddressADT} x n;
assign_test_9 := y;
z = let n = Emp Uint128 (Map Uint128 AddressADT) in
let sub_n = Emp Uint128 AddressADT in
let sub_k = Uint128 0 in
let sub_res = builtin put sub_n sub_k x in
builtin put n sub_k sub_res;
assign_test_10 := z;
k1 = Uint128 1;
k2 = Uint128 42;
assign_test_10[k1][k2] := x
end
(* Check that sender balance is deducted on acceptance *)
transition SenderBalanceTest()
pre <-& _sender._balance;
sender_balance_pre := pre;
(* First accept should cause sender balance to decrease *)
accept;
mid <-& _sender._balance;
sender_balance_mid := mid;
(* Second accept should make no difference *)
accept;
post <-& _sender._balance;
sender_balance_post := post
end