Skip to content

Commit 5443522

Browse files
kushalbabelkushalbabel
committed
Executable statements in the middle of data
1 parent ee2eb95 commit 5443522

File tree

3 files changed

+23
-22
lines changed

3 files changed

+23
-22
lines changed

‎find_mev.py

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,9 @@
55
from pathlib import Path
66

77
MAKER_DATA = """
8-
276203969674087029088707267242881295499809928317 opens vault 155042;
9-
276203969674087029088707267242881295499809928317 locks 9051654598458972160 collateral to vault 155042;
10-
276203969674087029088707267242881295499809928317 draws 800000000000000000000 debt from vault 155042;
8+
exec(276203969674087029088707267242881295499809928317 opens vault 155042);
9+
exec(276203969674087029088707267242881295499809928317 locks 9051654598458972160 collateral to vault 155042);
10+
exec(276203969674087029088707267242881295499809928317 draws 800000000000000000000 debt from vault 155042);
1111
"""
1212

1313

@@ -18,7 +18,7 @@
1818
0 in SAI gets 0;
1919
%s
2020
0 bites vault %s;
21-
=> ?X
21+
=> ?X
2222
</k>
2323
<S> ( (Uniswap in 0) |-> 0 (Uniswap in SAI) |-> 0 ) =>?S:Map </S>
2424
<M> .Set => ?_:Set </M>

‎maker.k

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -28,15 +28,15 @@ module MAKER
2828
// TODO : add stability fees (interest)
2929

3030
rule
31-
<k> exec(Address:ETHAddress opens vault Vault:ETHAddress) => .K </k>
31+
<k> exec(Address:ETHAddress opens vault Vault:ETHAddress) => .K ... </k>
3232
<V> V => V[(Vault) <- Address:ETHAddress] </V>
3333
<S> B => B[(Vault in 0) <- 0:Int][(Vault in SAI) <- 0:Int] </S>
3434
<B> ... .List => ListItem(Address opens vault Vault) </B>
3535
requires notBool((Vault in 0) in keys(B)) andBool notBool((Vault in SAI) in keys(B)) andBool notBool((Vault) in keys(V))
3636

3737

3838
rule
39-
<k> exec(Address:ETHAddress opens vault Vault:ETHAddress) => FAIL </k>
39+
<k> exec(Address:ETHAddress opens vault Vault:ETHAddress) => FAIL ... </k>
4040
<V> V </V>
4141
<S> B </S>
4242
<B> ... .List => ListItem(Address opens vault Vault) </B>
@@ -49,12 +49,12 @@ rule
4949
<k> exec(Address:ETHAddress locks Amount:Int collateral to vault Vault:ETHAddress) =>
5050
Address in 0 gets (0 -Int Amount) ~>
5151
Vault in 0 gets Amount
52-
</k>
52+
... </k>
5353
<V> ... Vault |-> Address ... </V>
5454
<B> ... .List => ListItem(Address locks Amount collateral to vault Vault) </B>
5555

5656
rule
57-
<k> exec(Address:ETHAddress locks Amount:Int collateral to vault Vault:ETHAddress) => FAIL </k>
57+
<k> exec(Address:ETHAddress locks Amount:Int collateral to vault Vault:ETHAddress) => FAIL ... </k>
5858
<V> V </V>
5959
<B> ... .List => ListItem(Address locks Amount collateral to vault Vault) </B>
6060
requires notBool( Vault in keys(V) )
@@ -66,15 +66,15 @@ rule
6666
<k> exec(Address:ETHAddress draws Amount:Int debt from vault Vault:ETHAddress) =>
6767
Address in SAI gets Amount ~>
6868
Vault in SAI gets Amount
69-
</k>
69+
... </k>
7070
<V> ... Vault |-> Address ... </V>
7171
<P> ... (0 , SAI) |-> Px ... </P>
7272
<S> ... (Vault in 0) |-> TotalCollateral (Vault in SAI) |-> TotalDebt ... </S>
7373
<B> ... .List => ListItem(Address draws Amount debt from vault Vault) </B>
7474
requires TotalCollateral *Int Px *Int 100 >=Int 150 *Int (TotalDebt +Int Amount)
7575

7676
rule
77-
<k> exec(Address:ETHAddress draws Amount:Int debt from vault Vault:ETHAddress) => FAIL </k>
77+
<k> exec(Address:ETHAddress draws Amount:Int debt from vault Vault:ETHAddress) => FAIL ... </k>
7878
<V> V </V>
7979
<P> P </P>
8080
<S> S </S>
@@ -83,7 +83,7 @@ rule
8383

8484

8585
rule
86-
<k> exec(Address:ETHAddress draws Amount:Int debt from vault Vault:ETHAddress) => FAIL </k>
86+
<k> exec(Address:ETHAddress draws Amount:Int debt from vault Vault:ETHAddress) => FAIL ... </k>
8787
<V> ... Vault |-> Address ... </V>
8888
<P> ... (0 , SAI) |-> Px ... </P>
8989
<S> ... (Vault in 0) |-> TotalCollateral (Vault in SAI) |-> TotalDebt ... </S>
@@ -97,7 +97,7 @@ rule
9797
<k> exec(Address:ETHAddress frees Amount:Int collateral from vault Vault:ETHAddress) =>
9898
Address in 0 gets Amount ~>
9999
Vault in 0 gets (0 -Int Amount)
100-
</k>
100+
... </k>
101101
<V> ... Vault |-> Address ... </V>
102102
<P> ... (0 , SAI) |-> Px ... </P>
103103
<S> ... (Vault in 0) |-> TotalCollateral (Vault in SAI) |-> TotalDebt ... </S>
@@ -107,7 +107,7 @@ rule
107107

108108
rule
109109
<k> exec(Address:ETHAddress frees Amount:Int collateral from vault Vault:ETHAddress) => FAIL
110-
</k>
110+
... </k>
111111
<V> V </V>
112112
<P> P </P>
113113
<S> S </S>
@@ -116,7 +116,7 @@ rule
116116

117117
rule
118118
<k> exec(Address:ETHAddress frees Amount:Int collateral from vault Vault:ETHAddress) => FAIL
119-
</k>
119+
... </k>
120120
<V> ... Vault |-> Address ... </V>
121121
<P> ... (0 , SAI) |-> Px ... </P>
122122
<S> ... (Vault in 0) |-> TotalCollateral (Vault in SAI) |-> TotalDebt ... </S>
@@ -130,21 +130,21 @@ rule
130130
<k> exec(Address:ETHAddress wipes Amount:Int debt from vault Vault:ETHAddress) =>
131131
Address in SAI gets (0 -Int Amount) ~>
132132
Vault in SAI gets (0 -Int Amount)
133-
</k>
133+
... </k>
134134
<V> ... Vault |-> Address ... </V>
135135
<S> ... (Vault in SAI) |-> TotalDebt ... </S>
136136
<B> ... .List => ListItem(Address wipes Amount debt from vault Vault) </B>
137137
requires (TotalDebt >=Int Amount)
138138

139139
rule
140-
<k> exec(Address:ETHAddress wipes Amount:Int debt from vault Vault:ETHAddress) => FAIL </k>
140+
<k> exec(Address:ETHAddress wipes Amount:Int debt from vault Vault:ETHAddress) => FAIL ... </k>
141141
<V> V </V>
142142
<S> S </S>
143143
<B> ... .List => ListItem(Address wipes Amount debt from vault Vault) </B>
144144
requires notBool((Vault in keys(V)) andBool ((Vault in SAI) in keys(S)))
145145

146146
rule
147-
<k> exec(Address:ETHAddress wipes Amount:Int debt from vault Vault:ETHAddress) => FAIL </k>
147+
<k> exec(Address:ETHAddress wipes Amount:Int debt from vault Vault:ETHAddress) => FAIL ... </k>
148148
<V> ... Vault |-> Address ... </V>
149149
<S> ... (Vault in SAI) |-> TotalDebt ... </S>
150150
<B> ... .List => ListItem(Address wipes Amount debt from vault Vault) </B>
@@ -159,21 +159,21 @@ rule
159159
Vault in 0 gets 0 -Int ((130 *Int TotalDebt) /Int (Px *Int 100)) ~> // 30% penalty
160160
Address in SAI gets TotalDebt ~>
161161
Address in 0 gets (0 -Int ((90 *Int TotalDebt) /Int (Px *Int 100)) ) //10% discount
162-
</k>
162+
... </k>
163163
<P> ... (0 , SAI) |-> Px ... </P>
164164
<S> ... (Vault in 0) |-> TotalCollateral (Vault in SAI) |-> TotalDebt ... </S>
165165
<B> ... .List => ListItem(Address bites vault Vault) </B>
166166
requires (TotalCollateral *Int Px *Int 100 <Int 150 *Int TotalDebt) andBool (Px >Int 0)
167167

168168
rule
169-
<k> exec(Address:ETHAddress bites vault Vault:ETHAddress) => FAIL </k>
169+
<k> exec(Address:ETHAddress bites vault Vault:ETHAddress) => FAIL ... </k>
170170
<P> P </P>
171171
<S> S </S>
172172
<B> ... .List => ListItem(Address bites vault Vault) </B>
173173
requires notBool ( ( (0 , SAI) in keys(P) ) andBool ((Vault in 0) in keys(S)) andBool ((Vault in SAI) in keys(S)))
174174

175175
rule
176-
<k> exec(Address:ETHAddress bites vault Vault:ETHAddress) => FAIL </k>
176+
<k> exec(Address:ETHAddress bites vault Vault:ETHAddress) => FAIL ... </k>
177177
<P> ... (0 , SAI) |-> Px ... </P>
178178
<S> ... (Vault in 0) |-> TotalCollateral (Vault in SAI) |-> TotalDebt ... </S>
179179
<B> ... .List => ListItem(Address bites vault Vault) </B>
@@ -183,12 +183,12 @@ rule
183183

184184

185185
rule
186-
<k> exec(Address:ETHAddress is given vault Vault:ETHAddress) => .K </k>
186+
<k> exec(Address:ETHAddress is given vault Vault:ETHAddress) => .K ... </k>
187187
<V> ... Vault |-> (_ => Address) ... </V>
188188
<B> ... .List => ListItem(Address is given vault Vault) </B>
189189

190190
rule
191-
<k> exec(Address:ETHAddress is given vault Vault:ETHAddress) => FAIL </k>
191+
<k> exec(Address:ETHAddress is given vault Vault:ETHAddress) => FAIL ... </k>
192192
<V> V </V>
193193
<B> ... .List => ListItem(Address is given vault Vault) </B>
194194
requires notBool(Vault in keys(V))

‎process_data.py

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ def get_price(cfg):
2020
def bootstrapped_data(f, cfg, rows):
2121
f.write("Uniswap in 0 gets {:.0f};\n".format(cfg['0']))
2222
f.write("Uniswap in SAI gets {:.0f};\n".format(cfg['SAI']))
23+
f.write("GetPrice SAI 0;\n")
2324
for row in rows:
2425
f.write(row)
2526

0 commit comments

Comments
 (0)