-
Notifications
You must be signed in to change notification settings - Fork 0
/
ZkRollup.zok
50 lines (42 loc) · 1.21 KB
/
ZkRollup.zok
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
from ".\BabyJubJub.zok" import ECPoint
from ".\EdDSA.zok" import EdDSAVerify
const u32 TCNT = 10
const u32 ACNT = 2 * TCNT
struct Transaction {
field Value
field Nonce
ECPoint Receiver
ECPoint Sender
ECPoint R
field S
}
struct Account {
ECPoint Owner
field OldValue
field OldNonce
field NewValue
field NewNonce
}
def main(private Transaction[TCNT] T, Account[ACNT] A):
for u32 i in 0..TCNT do
bool empty = (T[i].Value == 0)
field[4] message = [T[i].Value, T[i].Nonce, T[i].Receiver.X, T[i].Receiver.Y]
bool correct = EdDSAVerify(T[i].Sender, message, T[i].R, T[i].S)
assert(empty || correct)
endfor
for u32 x in 0..ACNT do
field value = A[x].OldValue
field nonce = A[x].OldNonce
for u32 y in 0..TCNT do
bool nonEmpty = (T[y].Value != 0)
bool isSender = nonEmpty && (T[y].Sender == A[x].Owner)
bool isReceiver = nonEmpty && (T[y].Receiver == A[x].Owner)
bool canSend = (T[y].Nonce == nonce + 1) && (T[y].Value <= value)
assert(!isSender || canSend)
value = value + (isReceiver ? T[y].Value : 0)
value = value - (isSender ? T[y].Value : 0)
nonce = nonce + (isSender ? 1 : 0)
endfor
assert((A[x].NewValue == value) && (A[x].NewNonce == nonce))
endfor
return