Organise files and folders

Author: kushalbabel

.gitignore

@@ -1,5 +1,8 @@
+*.out
 *.swp
 mev-kompiled
 .kprove-*
 __pycache__
 *~
+*.pyc
+

bound_maker.k boundmaker.kbound_maker.k renamed to boundmaker.k

@@ -1,4 +1,4 @@
-module BOUND
+module BOUNDMAKER
     imports MEV
     rule <k>
             0 in 0 gets 0;
@@ -23,4 +23,4 @@ module BOUND
 	// orBool (notBool ((0 , SAI) in keys(?P)))
 	// (notBool(?X ==K .K) andBool notBool(?Y ==K .K)) orBool (?X ==K .K andBool ?Y ==K .K andBool ({?S[0 in SAI]}:>Int <=Int 0 )) 
 	// (	notBool(?X ==K DONE)) orBool
-endmodule
+endmodule

calc_mev.py

@@ -0,0 +1,42 @@
+import sys
+from subprocess import Popen, PIPE
+import re
+
+BLANK_SPEC = """module CALCBOUND
+    imports MEV
+    rule <k>
+            %s
+         => ?X
+     </k>
+    <S> ( (Uniswap in 0) |-> 0 (Uniswap in SAI) |-> 0 ) =>?Y0:Map </S>
+    <M> .Set => ?Y1:Set </M>
+    <B> .List => ?Y2:List </B>
+    <P> .Map => ?Y3:Map </P>
+    <V> .Map => ?Y4:Map </V>
+    ensures ( ({?Y0[0 in SAI]}:>Int <=Int 0) andBool ?X ==K DONE) orBool (?X ==K FAIL)
+endmodule
+"""
+
+def find_mev_cdp(program, outfile):
+    global BLANK_SPEC
+    output = ""
+    spec = BLANK_SPEC % (program)
+    open("output/calcbound.k", "w").write(spec)
+    print("Starting proof...")
+    sys.stdout.flush()
+    pipe = Popen("kprove -v --debug --default-claim-type all-path --z3-impl-timeout 500 output/calcbound.k", shell=True, stdout=PIPE, stderr=PIPE)
+    output = pipe.stdout.read() + pipe.stderr.read()
+    output = str(output, "utf-8")
+    print(output)
+    if "#True" not in output:
+        print("MEV FOUND!")
+        print("Writing MEV configuration to", outfile, "...")
+        open(outfile, "w").write(output)
+        return
+
+def main():
+    PROGRAM = open(sys.argv[1]).read()
+    find_mev_cdp(PROGRAM, "output/calcmev.out")
+
+if __name__ == '__main__':
+    main()

test_uniswap_maker.txt data/test_uniswap_maker.txttest_uniswap_maker.txt renamed to data/test_uniswap_maker.txt

@@ -0,0 +1,24 @@
+module CALCBOUND
+    imports MEV
+    rule <k>
+                        0 in 0 gets 0;
+            0 in SAI gets 0;
+1 in 0 gets 100000000;
+Uniswap in 0 gets 5;
+Uniswap in SAI gets 500;
+GetPrice 0 SAI;
+1 opens vault 2;
+1 locks 6 collateral to vault 2;
+1 draws 6 debt from vault 2;
+1 in 0 swaps 40 input for SAI fee 5;
+0 bites vault 2;
+
+         => ?X
+     </k>
+    <S> ( (Uniswap in 0) |-> 0 (Uniswap in SAI) |-> 0 ) =>?Y0:Map </S>
+    <M> .Set => ?Y1:Set </M>
+    <B> .List => ?Y2:List </B>
+    <P> .Map => ?Y3:Map </P>
+    <V> .Map => ?Y4:Map </V>
+    ensures ( ({?Y0[0 in SAI]}:>Int <=Int 0) andBool ?X ==K DONE) orBool (?X ==K FAIL)
+endmodule