-
Notifications
You must be signed in to change notification settings - Fork 4
/
Copy pathfreelance-highlevel.idr
284 lines (218 loc) · 12.6 KB
/
freelance-highlevel.idr
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
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
module Main
import Data.Fin
%default covering
--------------------------------------------------------------------------------
---- Std extensions
--------------------------------------------------------------------------------
lookupBy : (a -> b -> Bool) -> a -> List (b, v) -> Maybe v
lookupBy p e [] = Nothing
lookupBy p e ((l, r) :: xs) =
if p e l then
Just r
else
lookupBy p e xs
repeat : (n : Nat) -> List a -> List a
repeat Z _ = []
repeat (S n) x = x ++ repeat n x
--------------------------------------------------------------------------------
---- Arithmetic types
--------------------------------------------------------------------------------
data UintSeq : Nat -> Type where
UintSeqVoid : UintSeq Z
UintSeqLow : (bits : Nat) -> UintSeq bits -> UintSeq (S bits)
UintSeqHigh : (bits : Nat) -> UintSeq bits -> UintSeq (S bits)
using (n : Nat)
Eq (UintSeq n) where
(==) UintSeqVoid UintSeqVoid = True
(==) (UintSeqLow _ a) (UintSeqLow _ b) = a == b
(==) (UintSeqHigh _ _) (UintSeqLow _ _) = False
(==) (UintSeqLow _ _) (UintSeqHigh _ _) = False
(==) (UintSeqHigh _ a) (UintSeqHigh _ b) = a == b
Ord (UintSeq n) where
compare UintSeqVoid UintSeqVoid = EQ
compare (UintSeqLow _ a) (UintSeqLow _ b) = compare a b
compare (UintSeqHigh _ _) (UintSeqLow _ _) = GT
compare (UintSeqLow _ _) (UintSeqHigh _ _) = LT
compare (UintSeqHigh _ a) (UintSeqHigh _ b) = compare a b
seq_to_bits : (n : Nat) -> UintSeq n -> List Nat
seq_to_bits Z UintSeqVoid = Nil
seq_to_bits (S n) (UintSeqLow n low) = 0 :: (seq_to_bits n low)
seq_to_bits (S n) (UintSeqHigh n low) = 1 :: (seq_to_bits n low)
bits_to_seq : (a : List (Fin 2)) -> UintSeq (length a)
bits_to_seq Nil = UintSeqVoid
bits_to_seq (0 :: next) = UintSeqLow _ $ bits_to_seq next
bits_to_seq (1 :: next) = UintSeqHigh _ $ bits_to_seq next
bits_to_nat : List Nat -> Nat
bits_to_nat Nil = 0
bits_to_nat (v :: old) = (bits_to_nat old) * 2 + v
stn : (n : Nat) -> UintSeq n -> Nat
stn n v = bits_to_nat (reverse (seq_to_bits n v))
build_zero_uint_seq : (n : Nat) -> UintSeq n
build_zero_uint_seq Z = UintSeqVoid
build_zero_uint_seq (S k) = UintSeqLow _ (build_zero_uint_seq k)
build_high_uint_seq : (n : Nat) -> UintSeq n
build_high_uint_seq Z = UintSeqVoid
build_high_uint_seq (S k) = UintSeqHigh _ (build_high_uint_seq k)
--------------------------------------------------------------------------------
---- TON-specific types
--------------------------------------------------------------------------------
data Anycast : Type where
AnycastCreate : (depth : UintSeq 5) -> (pfx : UintSeq (stn 5 depth)) -> Anycast
data MessageAddr : Type where
MsgAddressIntStd : (Maybe Anycast) -> (workchain : UintSeq 8) -> (hash_part : UintSeq 256) -> MessageAddr
-- MsgAddressIntVar : (Maybe Anycast) -> (addr_len : UintSeq 9) -> (workchain : UintSeq 32) -> (hash_part : UintSeq (stn 9 addr_len)) -> MessageAddr
Eq MessageAddr where
(==) (MsgAddressIntStd Nothing wc1 hp1) (MsgAddressIntStd Nothing wc2 hp2) = (wc1 == wc2) && (hp1 == hp2)
(==) _ _ = False
data TxMessage : Type where
IntMsg : (bounce : Bool) -> (src : MessageAddr) -> (dest : MessageAddr) -> (coins : UintSeq 120) -> (init : Maybe ()) -> (body : JobMsgBody) -> TxMessage
ExtInMsg : (src : MessageAddr) -> (dest : MessageAddr) -> (init : Maybe ()) -> (body : List Nat) -> TxMessage
ExtOutMsg : (src : MessageAddr) -> (dest : MessageAddr) -> (init : Maybe ()) -> (body : List Nat) -> TxMessage
--------------------------------------------------------------------------------
---- High-level contracts representation
--------------------------------------------------------------------------------
mutual
data NextState : Type where
MkNextState : ContractState ncs => ncs -> NextState
interface ContractState cs where
to_code : cs -> (cs -> TxMessage -> (NextState, List TxMessage))
to_data : cs -> Type
data Contract : Type where
Uninit : (addr : MessageAddr) -> Contract
Init : ContractState cs => (addr : MessageAddr) -> (st : cs) -> (balance : Nat) -> Contract
run_tvm : NextState -> TxMessage -> (NextState, List TxMessage)
run_tvm (MkNextState wrapped_state) msg = (to_code wrapped_state) wrapped_state msg
build_bounce : TxMessage -> List TxMessage
build_bounce (IntMsg True src self coins _ body) = [IntMsg False self src coins Nothing $ Bounce body]
build_bounce _ = Nil
bounce_typical : ContractState cs => cs -> TxMessage -> (NextState, List TxMessage)
bounce_typical state msg = (MkNextState state, build_bounce msg)
----
-- ContractStorage = (List (MessageAddr, NextState))
lookup_contract : (List (MessageAddr, NextState)) -> MessageAddr -> Maybe NextState
lookup_contract contracts addr = lookupBy f () contracts where
f : () -> MessageAddr -> Bool
f _ some_addr = addr == some_addr
extract_contract : (List (MessageAddr, NextState)) -> MessageAddr -> (Maybe NextState, (List (MessageAddr, NextState)))
extract_contract Nil addr = (Nothing, Nil)
extract_contract (x::xs) addr = let (gaddr, v) = x in
if gaddr == addr then
(Just v, xs)
else
let (loaded, storage) = extract_contract xs addr in
(loaded, (gaddr,v) :: storage)
extract_dest : TxMessage -> MessageAddr
extract_dest (IntMsg _ _ dest _ _ _) = dest
extract_dest (ExtInMsg _ dest _ _) = dest
extract_dest (ExtOutMsg _ dest _ _) = dest
main_loop : List TxMessage -> List (MessageAddr, NextState) -> (List TxMessage, List (MessageAddr, NextState))
main_loop Nil contracts = (Nil, contracts)
main_loop (msg :: later) contracts = let (mb_contract, contracts_ext) = extract_contract contracts $ extract_dest msg in
case mb_contract of
Nothing => main_loop (later ++ (build_bounce msg)) contracts_ext
Just contract => let (upd_contract, send) = run_tvm contract msg in
(later ++ send, (extract_dest msg, upd_contract) :: contracts_ext)
--------------------------------------------------------------------------------
---- Job contract
--------------------------------------------------------------------------------
data PayProposal : Type where
ProposePay : (worker_lower : UintSeq 64) -> (worker_upper : UintSeq 64) -> PayProposal
data PaySignature : PayProposal -> Type where
SignPay : (proposal : PayProposal) -> (role : UintSeq 2) -> (sig : UintSeq 512) -> PaySignature proposal
check_distinct_roles : PaySignature -> PaySignature -> Bool
check_distinct_roles (SignPay _ r1 _) (SignPay _ r2 _) = (r1 != r2)
data JobMsgBody : Type where
JumLock : (offer : MessageAddr) -> JobMsgBody
JlmConfirm : (worker_addr : MessageAddr) -> (worker_desc : Type) -> (worker_key : UintSeq 256) -> JobMsgBody
JwmFinish : (sig_a : PaySignature) -> (sig_b: PaySignature) -> JobMsgBody
Bounce : JobMsgBody -> JobMsgBody
MsgRaw : List Nat -> JobMsgBody
data JobContractStateDestroyed : Type where
JcsDestroyed : JobContractStateDestroyed
ContractState JobContractStateDestroyed where
to_code _ = bounce_typical
to_data _ = believe_me ()
----
data JobContractDataUnlocked : Type where
JcdUnlocked : (poster : MessageAddr) -> (desc : Type) -> (value : UintSeq 120) -> (poster_key : UintSeq 256) -> JobContractDataUnlocked
data JobContractStateUnlocked : Type where
JcsUnlocked : (jccode : (JobContractStateUnlocked -> TxMessage -> (NextState, List TxMessage))) -> (jcdata : JobContractDataUnlocked) -> JobContractStateUnlocked
ContractState JobContractStateUnlocked where
to_code cur_state = let JcsUnlocked jccode jcdata = cur_state in
jccode
to_data cur_state = let JcsUnlocked jccode jcdata = cur_state in
believe_me jcdata
----
data JobContractDataLockedOn : Type where
JcdLockedOn : (poster : MessageAddr) -> (desc : Type) -> (value : UintSeq 120) -> (poster_key : UintSeq 256) -> (offer : MessageAddr) -> JobContractDataLockedOn
data JobContractStateLockedOn : Type where
JcsLockedOn : (jccode : (JobContractStateLockedOn -> TxMessage -> (NextState, List TxMessage))) -> (jcdata : JobContractDataLockedOn) -> JobContractStateLockedOn
ContractState JobContractStateLockedOn where
to_code cur_state = let JcsLockedOn jccode jcdata = cur_state in
jccode
to_data cur_state = let JcsLockedOn jccode jcdata = cur_state in
believe_me jcdata
----
data JobContractDataWorking : Type where
JcdWorking : (poster : MessageAddr) -> (desc : Type) -> (value : UintSeq 120) -> (poster_key : UintSeq 256) -> (worker_key : UintSeq 256) -> JobContractDataWorking
data JobContractStateWorking : Type where
JcsWorking : (jccode : (JobContractStateWorking -> TxMessage -> (NextState, List TxMessage))) -> (jcdata : JobContractDataWorking) -> JobContractStateWorking
ContractState JobContractStateWorking where
to_code cur_state = let JcsWorking jccode jcdata = cur_state in
jccode
to_data cur_state = let JcsWorking jccode jcdata = cur_state in
believe_me jcdata
----
job_working : JobContractStateWorking -> TxMessage -> (NextState, List TxMessage)
job_working state (IntMsg bounce src self coins _ body) = case believe_me $ to_data state of
(JcdWorking poster desc value poster_key worker_key) => case body of
Bounce _ => (MkNextState state, Nil)
JwmFinish worker poster_sig worker_sig => case True of -- TODO: check signatures
True => (MkNextState JcsDestroyed, [IntMsg False self worker value Nothing $ MsgRaw []])
False => (MkNextState state, build_bounce (IntMsg bounce src self coins Nothing body))
_ => (MkNextState state, build_bounce (IntMsg bounce src self coins Nothing body))
_ => (MkNextState state, Nil)
job_working state _ = (MkNextState state, Nil)
job_locked_on : JobContractStateLockedOn -> TxMessage -> (NextState, List TxMessage)
job_locked_on state (IntMsg bounce src self coins _ body) = case believe_me $ to_data state of
(JcdLockedOn poster desc value poster_key offer) => case body of
Bounce _ => (MkNextState state, Nil)
(JlmConfirm worker_key) => case offer == src of
True => ((MkNextState $ JcsWorking job_working $ believe_me $ JcdWorking poster desc value poster_key worker_key), Nil)
False => (MkNextState state, build_bounce (IntMsg bounce src self coins Nothing body))
_ => (MkNextState state, build_bounce (IntMsg bounce src self coins Nothing body))
_ => (MkNextState state, Nil)
job_locked_on state _ = (MkNextState state, Nil)
job_unlocked : JobContractStateUnlocked -> TxMessage -> (NextState, List TxMessage)
job_unlocked state (IntMsg bounce src self coins _ body) = case believe_me $ to_data state of
(JcdUnlocked poster desc value poster_key) => case body of
Bounce _ => (MkNextState state, Nil)
(JumUpdate new_desc new_value new_poster_key) => case poster == src of
True => ((MkNextState $ JcsUnlocked job_unlocked $ believe_me $ JcdUnlocked poster new_desc new_value new_poster_key), Nil)
False => (MkNextState state, build_bounce (IntMsg bounce src self coins Nothing body))
(JumLock offer) => case poster == src of
True => ((MkNextState $ JcsLockedOn job_locked_on $ believe_me $ JcdLockedOn poster desc value poster_key offer), Nil)
False => (MkNextState state, build_bounce (IntMsg bounce src self coins Nothing body))
_ => (MkNextState state, build_bounce (IntMsg bounce src self coins Nothing body))
_ => (MkNextState state, Nil)
job_unlocked state _ = (MkNextState state, Nil)
----
{-
check_invariant : NextState -> TxMessage -> Bool
check_invariant state msg = state == (fst $ run_tvm state msg)
build_ju : MessageAddr -> Type -> UintSeq 120 -> UintSeq 256 -> NextState
build_ju poster desc value poster_key = MkNextState $ JcsUnlocked job_unlocked $ believe_me $ JcdUnlocked poster desc value poster_key
theorem_ju_no_extin_processing : (cp : MessageAddr) -> (cd : Type) -> (cv : UintSeq 120) -> (cpk : UintSeq 256)
-> (ExtInMsg ma mb mc md) -> (check_invariant (build_ju cp cd cv cpk) $ ExtInMsg ma mb mc md) = True
theorem_ju_no_extin_processing _ _ _ _ _ = Refl
theorem_ju_invariant_nonposter : (poster : MessageAddr) -> (any : MessageAddr)
-> (cd : Type) -> (cv : UintSeq 120) -> (cpk : UintSeq 256)
-> (
-> Not (poster == any)
-> (check_invariant (build_ju poster cd cv cpk)
-}
----
main : IO ()
main = do putStrLn "Theorems proved"
putStrLn "Starting transactions loop"
putStrLn "Transactions loop finished"