changeset 5:3917d9bb1e21

Proofexample
author Sigurd Meldgaard <stm@daimi.au.dk>
date Mon, 18 May 2009 09:54:38 +0200
parents 5f850f623c69
children 516288f9b647
files ideal_functionality.py pretty_print.py proofexample.thy secret_annotator.py secret_ifs.py test.py util.py
diffstat 7 files changed, 120 insertions(+), 72 deletions(-) [+]
line wrap: on
line diff
--- a/ideal_functionality.py	Thu Nov 13 12:55:15 2008 +0100
+++ b/ideal_functionality.py	Mon May 18 09:54:38 2009 +0200
@@ -6,6 +6,7 @@
 import secret_annotator
 import secret_ifs
 import compatibility_check
+import proof_burden
 
 
 def init_statements(node):
@@ -28,48 +29,16 @@
     source_str = inspect.getsource(f)
     source_ast = ast.parse(source_str) # Returns a module
     function_ast = source_ast.body[0] # We want only the function
+    #pretty_print.PrettyPrinter().visit(source_ast)
     init_statements(function_ast)
     # We don't want recursive applications of this decorator
     #function_ast.decorator_list.remove[0]
+    print "-"*80
     compatibility_check.CompatibilityChecker().visit(function_ast)
     secret_annotator.secret_analysis(function_ast)
     t = secret_ifs.TransformIfs().visit(function_ast)
-    pretty_print.PrettyPrinter().visit(t)
-
-
-"""
-def a(a, b, c):
-    a = 2
-    if c:
-        b = 2
-        while True:
-            d = 3
-            if a:
-                break
-            else:
-                pass
-            if b:
-                return
-            else:
-                pass
-    else:
-        print("hej")
-"""
-
-
-@ideal_functionality
-def fun(b, c):
-    d = b + 2
-    if d:
-        e = 2
-    a = 2
-    mark_secret(a)
-    if a:
-        e = 4
-    else:
-        e = 8
-    f = 3
-    if f:
-        e = 2
-    f = e + 4
-#flow_graph.to_dot()
+    t.decorator_list.pop()
+    proof_burden.proof_burden(t)
+    exec compile(ast.Module([t]), "<string>", "exec")
+    #pretty_print.PrettyPrinter().visit(t)
+    return eval(function_ast.name)
--- a/pretty_print.py	Thu Nov 13 12:55:15 2008 +0100
+++ b/pretty_print.py	Mon May 18 09:54:38 2009 +0200
@@ -95,6 +95,22 @@
     return ops[op.__class__]
 
 
+def slice_string(slice):
+    if(isinstance(slice, ast.Ellipsis)):
+        return "..."
+    elif(isinstance(slice, ast.Index)):
+        return expr_string(slice.value)
+    elif(isinstance(slice, ast.Slice)):
+        #TODO: handle null lower/upper
+        #TODO: handle steps
+        return "%s:%s" % \
+            (expr_string(slice.lower),
+             expr_string(slice.upper))
+    else:
+        #TODO: handle several slices
+        assert False
+
+
 def expr_string(exp, prec=1):
     """Returns a string representation of the expression.
     *prec* is the precedence of the surrounding of the expression,
@@ -176,6 +192,13 @@
     elif(isinstance(exp, dict)):
         print exp
         assert False, "Type error"
+    elif(isinstance(exp, ast.Subscript)):
+        my_precedence = 21
+        r = "%s[%s]" % \
+            (expr_string(exp.value, my_precedence), slice_string(exp.slice))
+    elif(isinstance(exp, ast.Str)):
+        my_precedence = 100
+        r = '"%s"' % exp.s
     else:
         assert False, "Not implemented of type %s" % type(exp)
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/proofexample.thy	Mon May 18 09:54:38 2009 +0200
@@ -0,0 +1,47 @@
+theory proofexample imports Main begin
+
+value "sorted [-1, 0, 0, 5::int]"
+
+lemma "[] \<noteq> [1::nat]"
+  apply (rule list.distinct)
+done
+
+lemma assumes ab: "A \<and> B"
+  shows "B \<and> A"
+using ab
+proof
+  assume "B" "A" thus ?thesis ..
+qed
+
+lemma assumes "A" shows "A"
+proof -
+  show "A" by (rule assms) 
+qed
+
+lemma sorted_mono[simp]:
+  assumes
+  "sorted (xs::int list)"
+  shows "mono (\<lambda> x . xs ! x)"
+proof
+
+
+qed
+(* Simulates: xst[mid] \<ge> 0 *)
+definition "simulator" :: "nat \<Rightarrow> nat \<Rightarrow> bool " where
+  "simulator result mid = (result \<le> mid)"
+
+lemma simulation_correct:
+  assumes "sorted xs"
+  "(xs ! result) = (0::int)"
+  "(xs ! (result - 1)) < 0 \<or> (result = 0)"
+  shows "(simulator result index) = ((xs ! index) \<ge> 0)"
+proof
+  have "mono (\<lambda> x . xs ! 
+  assume "simulator result index"
+  have "xs ! index \<ge> 0" sorry
+  
+qed
+
+
+end
+  
\ No newline at end of file
--- a/secret_annotator.py	Thu Nov 13 12:55:15 2008 +0100
+++ b/secret_annotator.py	Mon May 18 09:54:38 2009 +0200
@@ -8,6 +8,7 @@
     Returns True if the expression exp should be considered secret
     given that the variables in *secret_variables* are secret.
     """
+    non_compromising_functions = set(["len", "open", "result"])
     if(isinstance(exp, ast.BoolOp)):
         return (expr_secret(exp.values[0], secret_variables)
                  or expr_secret(exp.values[1], secret_variables))
@@ -26,13 +27,18 @@
     elif(isinstance(exp, ast.Num)):
         return False
     elif(isinstance(exp, ast.Call)):
-        if(not (isinstance(exp.func, ast.Name)
-           and eval(exp.func.id).secret)):
+        if(not isinstance(exp.func, ast.Name)):
             if(any([expr_secret(i, secret_variables) for i in exp.args])):
-                util.error("Call of non-secret value with secret argument",
+                util.error("Call of non-fixed function with secret argument",
                            exp)
-            else:
-                return False
+        if(exp.func.id in non_compromising_functions):
+            return False
+        func = eval(exp.func.id)
+        if(func.secret):
+            return True
+        elif(any([expr_secret(i, secret_variables) for i in exp.args])):
+            util.error("Call of non-secret\
+ function with secret argument", exp)
         else:
             return True # For now
     else:
@@ -62,16 +68,14 @@
         if(expr_secret(node.value, ins)):
             ins = ins | set([node.targets[0].id])
         else:
-            print "fr", ins
             ins = ins - set([node.targets[0].id])
-            print "efter", ins
     if(isinstance(node, ast.Expr) and
        isinstance(node.value, ast.Call) and
        isinstance(node.value.func, ast.Name) and
        node.value.func.id == "mark_secret"):
         # Todo - handle non-names...
         ins = ins | set([i.id for i in node.value.args])
-    return r
+    return ins
 
 
 def secret_analysis(function):
--- a/secret_ifs.py	Thu Nov 13 12:55:15 2008 +0100
+++ b/secret_ifs.py	Mon May 18 09:54:38 2009 +0200
@@ -62,8 +62,12 @@
     def reset(self):
         self.changed = False
 
+    def visit_While(self, node):
+        if(secret_annotator.expr_secret(node.test, node.in_values["secret"])):
+            error("While is not possible on a secret value", node)
+        return node
+
     def visit_If(self, node):
-        print "-"*80, node.in_values["secret"]
         if(secret_annotator.expr_secret(node.test, node.in_values["secret"])):
             self.changed = True
 
--- a/test.py	Thu Nov 13 12:55:15 2008 +0100
+++ b/test.py	Mon May 18 09:54:38 2009 +0200
@@ -1,30 +1,31 @@
-import flow
-
-
-def blah(f):
-    return f
-
-
-def test(x, y, z):
+from ideal_functionality import ideal_functionality
 
-    @blah
-    def inner(y):
-        print x+y
-        if(x):
-            k = 9
-        else:
-            k = 7
-            b = y
-        y = 2
-    x += 2
-    r = 3
-    return r
-
-#@flow
+#@proof_burden
+#@ideal_functionality
 def a(c):
+    precondition("c == 5")
     y = 4
+    a = open(c)
     if(c>c):
         pass
     else:
-        y = 5
         y = 3
+
+
+@ideal_functionality
+def auction(bids):
+    precondition("a >= b <=> bids[a] >= bids[b]")
+    precondition("0 >= bids[0]")
+    precondition("bids[len(bids)-1] >= 0")
+    low = 0
+    high = len(bids)
+    while(low < high):
+        invariant("bids[high] >= 0 && 0 >= bids[low]")
+        mid = (low + high) // 2
+        r = open(bids[mid] >= 0)
+        if r:
+            high = mid
+        else:
+            low = mid
+    result(mid)
+    return mid
--- a/util.py	Thu Nov 13 12:55:15 2008 +0100
+++ b/util.py	Mon May 18 09:54:38 2009 +0200
@@ -1,11 +1,11 @@
 """ Utilities for the static analysis tool
 """
 
-
 def error(msg, loc=None):
     """Print the error message.
     *loc* is an ast-node at the given location."""
     loc_tuple = (loc.lineno, loc.col_offset)
+    print ast.dump(loc)
     if loc:
         print "at %s" % (loc_tuple, ),
     print msg