Skip to content

Commit 99f0c62

Browse files
kushalbabelkushalbabel
committed
Maker : Fail only when necessary
1 parent d00c39b commit 99f0c62

File tree

1 file changed

+96
-17
lines changed

1 file changed

+96
-17
lines changed

‎maker.k‎

Lines changed: 96 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -34,14 +34,34 @@ rule
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

37+
38+
rule
39+
<k> exec(Address:ETHAddress opens vault Vault:ETHAddress) => FAIL </k>
40+
<V> V </V>
41+
<S> B </S>
42+
<B> ... .List => ListItem(Address opens vault Vault) </B>
43+
requires ((Vault in 0) in keys(B)) orBool((Vault in SAI) in keys(B)) orBool ((Vault) in keys(V))
44+
45+
46+
47+
3748
rule
3849
<k> exec(Address:ETHAddress locks Amount:Int collateral to vault Vault:ETHAddress) =>
3950
Address in 0 gets (0 -Int Amount) ~>
4051
Vault in 0 gets Amount
4152
</k>
4253
<V> ... Vault |-> Address ... </V>
4354
<B> ... .List => ListItem(Address locks Amount collateral to vault Vault) </B>
44-
55+
56+
rule
57+
<k> exec(Address:ETHAddress locks Amount:Int collateral to vault Vault:ETHAddress) => FAIL </k>
58+
<V> V </V>
59+
<B> ... .List => ListItem(Address locks Amount collateral to vault Vault) </B>
60+
requires notBool( Vault in keys(V) )
61+
62+
63+
64+
4565
rule
4666
<k> exec(Address:ETHAddress draws Amount:Int debt from vault Vault:ETHAddress) =>
4767
Address in SAI gets Amount ~>
@@ -53,6 +73,26 @@ rule
5373
<B> ... .List => ListItem(Address draws Amount debt from vault Vault) </B>
5474
requires TotalCollateral *Int Px *Int 100 >=Int 150 *Int (TotalDebt +Int Amount)
5575

76+
rule
77+
<k> exec(Address:ETHAddress draws Amount:Int debt from vault Vault:ETHAddress) => FAIL </k>
78+
<V> V </V>
79+
<P> P </P>
80+
<S> S </S>
81+
<B> ... .List => ListItem(Address draws Amount debt from vault Vault) </B>
82+
requires notBool ( (Vault in keys(V)) andBool ( (0 , SAI) in keys(P) ) andBool ((Vault in 0) in keys(S)) andBool ((Vault in SAI) in keys(S)) )
83+
84+
85+
rule
86+
<k> exec(Address:ETHAddress draws Amount:Int debt from vault Vault:ETHAddress) => FAIL </k>
87+
<V> ... Vault |-> Address ... </V>
88+
<P> ... (0 , SAI) |-> Px ... </P>
89+
<S> ... (Vault in 0) |-> TotalCollateral (Vault in SAI) |-> TotalDebt ... </S>
90+
<B> ... .List => ListItem(Address draws Amount debt from vault Vault) </B>
91+
requires notBool(TotalCollateral *Int Px *Int 100 >=Int 150 *Int (TotalDebt +Int Amount))
92+
93+
94+
95+
5696
rule
5797
<k> exec(Address:ETHAddress frees Amount:Int collateral from vault Vault:ETHAddress) =>
5898
Address in 0 gets Amount ~>
@@ -64,6 +104,28 @@ rule
64104
<B> ... .List => ListItem(Address frees Amount collateral from vault Vault) </B>
65105
requires (TotalCollateral -Int Amount) *Int Px *Int 100 >=Int 150 *Int TotalDebt
66106

107+
108+
rule
109+
<k> exec(Address:ETHAddress frees Amount:Int collateral from vault Vault:ETHAddress) => FAIL
110+
</k>
111+
<V> V </V>
112+
<P> P </P>
113+
<S> S </S>
114+
<B> ... .List => ListItem(Address frees Amount collateral from vault Vault) </B>
115+
requires notBool ( (Vault in keys(V)) andBool ( (0 , SAI) in keys(P) ) andBool ((Vault in 0) in keys(S)) andBool ((Vault in SAI) in keys(S)) )
116+
117+
rule
118+
<k> exec(Address:ETHAddress frees Amount:Int collateral from vault Vault:ETHAddress) => FAIL
119+
</k>
120+
<V> ... Vault |-> Address ... </V>
121+
<P> ... (0 , SAI) |-> Px ... </P>
122+
<S> ... (Vault in 0) |-> TotalCollateral (Vault in SAI) |-> TotalDebt ... </S>
123+
<B> ... .List => ListItem(Address frees Amount collateral from vault Vault) </B>
124+
requires notBool((TotalCollateral -Int Amount) *Int Px *Int 100 >=Int 150 *Int TotalDebt)
125+
126+
127+
128+
67129
rule
68130
<k> exec(Address:ETHAddress wipes Amount:Int debt from vault Vault:ETHAddress) =>
69131
Address in SAI gets (0 -Int Amount) ~>
@@ -74,6 +136,23 @@ rule
74136
<B> ... .List => ListItem(Address wipes Amount debt from vault Vault) </B>
75137
requires (TotalDebt >=Int Amount)
76138

139+
rule
140+
<k> exec(Address:ETHAddress wipes Amount:Int debt from vault Vault:ETHAddress) => FAIL </k>
141+
<V> V </V>
142+
<S> S </S>
143+
<B> ... .List => ListItem(Address wipes Amount debt from vault Vault) </B>
144+
requires notBool((Vault in keys(V)) andBool ((Vault in SAI) in keys(S)))
145+
146+
rule
147+
<k> exec(Address:ETHAddress wipes Amount:Int debt from vault Vault:ETHAddress) => FAIL </k>
148+
<V> ... Vault |-> Address ... </V>
149+
<S> ... (Vault in SAI) |-> TotalDebt ... </S>
150+
<B> ... .List => ListItem(Address wipes Amount debt from vault Vault) </B>
151+
requires notBool(TotalDebt >=Int Amount)
152+
153+
154+
155+
77156
rule
78157
<k> exec(Address:ETHAddress bites vault Vault:ETHAddress) =>
79158
Vault in SAI gets (0 -Int TotalDebt) ~>
@@ -87,32 +166,32 @@ rule
87166
requires (TotalCollateral *Int Px *Int 100 <Int 150 *Int TotalDebt) andBool (Px >Int 0)
88167

89168
rule
90-
<k> exec(_ bites vault _) => FAIL </k>
91-
<B> ... .List => ListItem(FAIL) </B>
92-
169+
<k> exec(Address:ETHAddress bites vault Vault:ETHAddress) => FAIL </k>
170+
<P> P </P>
171+
<S> S </S>
172+
<B> ... .List => ListItem(Address bites vault Vault) </B>
173+
requires notBool ( ( (0 , SAI) in keys(P) ) andBool ((Vault in 0) in keys(S)) andBool ((Vault in SAI) in keys(S)))
93174

94175
rule
95-
<k> exec(_ draws _ debt from vault _) => FAIL </k>
96-
<B> ... .List => ListItem(FAIL) </B>
176+
<k> exec(Address:ETHAddress bites vault Vault:ETHAddress) => FAIL </k>
177+
<P> ... (0 , SAI) |-> Px ... </P>
178+
<S> ... (Vault in 0) |-> TotalCollateral (Vault in SAI) |-> TotalDebt ... </S>
179+
<B> ... .List => ListItem(Address bites vault Vault) </B>
180+
requires notBool ((TotalCollateral *Int Px *Int 100 <Int 150 *Int TotalDebt) andBool (Px >Int 0))
97181

98-
rule
99-
<k> exec(_ locks _ collateral to vault _) => FAIL </k>
100-
<B> ... .List => ListItem(FAIL) </B>
101182

102183

103-
rule
104-
<k> exec(_ opens vault _) => FAIL </k>
105-
<B> ... .List => ListItem(FAIL) </B>
106184

107185
rule
108-
<k> exec(_ is given vault _) => FAIL </k>
109-
<B> ... .List => ListItem(FAIL) </B>
110-
186+
<k> exec(Address:ETHAddress is given vault Vault:ETHAddress) => .K </k>
187+
<V> ... Vault |-> (_ => Address) ... </V>
188+
<B> ... .List => ListItem(Address is given vault Vault) </B>
111189

112190
rule
113-
<k> exec(Address:ETHAddress is given vault Vault:ETHAddress) => .K </k>
114-
<V> ... Vault |-> (_ => Address) ... </V>
191+
<k> exec(Address:ETHAddress is given vault Vault:ETHAddress) => FAIL </k>
192+
<V> V </V>
115193
<B> ... .List => ListItem(Address is given vault Vault) </B>
194+
requires notBool(Vault in keys(V))
116195

117196
endmodule
118197

0 commit comments

Comments
 (0)