build ineqs

examples/tests/conference_linear_small_withB.spec

@@ -2,7 +2,7 @@ Workflow
 
 forallmay x:X,p:P
     True -> Conf += (x,p)
-forall x:x,p:P
+forall x:X,p:P
     B(x,p) -> Assign += (x,p)
 forall x:X,p:P
     (Assign(x,p) ∧ O(x,p)) -> Report += (x,p)

examples/tests/conference_stubborn_withB.spec

+Workflow
+
+forallmay x:A,p:P
+    True → Conf += (x,p)
+forallmay x:A,p:P
+    B(x,p) → Assign += (x,p)
+forall x:A,p:P
+    (Assign(x,p) ∧ Oracle(x,p)) → Review += (x,p)
+loop {
+    forall xa:A,xb:A,p:P (Assign(xa,p) ∧ Review(xb,p)) → Read += (xa,xb,p)
+    forallmay x:A,p:P (Assign(x,p)) → Review += (x,p)
+}
+
+Declassify
+
+Oracle(x:A,p:P): ¬ Conf(xat:A,p:P)
+
+Target
+
+Read(xat:A, xbt:A, pt:P)

src/main/scala/de/tum/workflows/Encoding.scala

@@ -145,11 +145,11 @@ object Encoding extends LazyLogging {
       case Remove(_, f, tup)                    => And(Fun(f, tup), Exists(omitted toList, Neg(guard)))
     }
 
-    (Forall(s.tuple, Eq(Next(Fun(s.fun, s.tuple)), t)), s.fun)
+    (Forall(s.tuple, Equiv(Next(Fun(s.fun, s.tuple)), t)), s.fun)
   }
 
   def encodeStaying(target: Fun) = {
-    Forall(target.params, Eq(Next(target), target))
+    Forall(target.params, Equiv(Next(target), target))
   }
 
   def encodeSem(sig: Signature, g: Graph[Int, LDiEdge]) = {

src/main/scala/de/tum/workflows/Preconditions.scala

@@ -16,7 +16,7 @@ object Preconditions extends LazyLogging {
           stmt.tuple.head.typ == s.target.params.head.typ) yield {
       val fun = Fun(stmt.fun, stmt.tuple)
       // TODO
-      val guard = Neg(Eq(fun.in(T1), fun.in(T2)))
+      val guard = Neg(Equiv(fun.in(T1), fun.in(T2)))
       ForallBlock(stmt.tuple, List(Add(guard, INFNAME, List(stmt.tuple.head))))
     }
     b :: newsteps

src/main/scala/de/tum/workflows/foltl/FOLTL.scala

@@ -53,8 +53,8 @@ object FOLTL {
     // TODO: better line breaking
     lazy val pretty: String = {
       val remeq = this.everywhere {
-        case Eq(t1, t2) if FormulaFunctions.annotateOverwrite(t1, Properties.T1, Properties.T2) == t2 =>
-          Eq(t1, Fun("eq", List()))
+        case Equiv(t1, t2) if FormulaFunctions.annotateOverwrite(t1, Properties.T1, Properties.T2) == t2 =>
+          Equiv(t1, Fun("eq", List()))
       }
 
       val s = remeq.toString
@@ -102,7 +102,7 @@ object FOLTL {
     val Predicate = "([a-zA-Z0-9]+)(#([a-zA-Z0-9]+))?((_[a-zA-Z0-9]+#[a-zA-Z0-9]+)*)".r
 
     def getVars(s: String) = {
-      val split = s split ("_") 
+      val split = s split ("_")
       if (split.length > 1) {
         split.drop(1).map(str => {
           val Array(name, typ) = str.split("#")
@@ -302,16 +302,29 @@ object FOLTL {
     val make = And.apply
   }
 
-  case class Eq(t1: Formula, t2: Formula) extends BinOp {
+  case class Equiv(t1: Formula, t2: Formula) extends BinOp {
     val opname = "↔"
-    val make = Eq.apply
+    val make = Equiv.apply
   }
-  object Eq {
+  object Equiv {
     def make(terms: List[Formula]) = {
-      BinOp.makeL(Eq.apply, terms, True)
+      BinOp.makeL(Equiv.apply, terms, True)
     }
     def make(terms: Formula*) = {
-      BinOp.makeL(Eq.apply, terms, True)
+      BinOp.makeL(Equiv.apply, terms, True)
+    }
+  }
+
+  case class Equal(t1: Formula, t2: Formula) extends BinOp {
+    val opname = "="
+    val make = Equal.apply
+  }
+  object Equal {
+    def make(terms: List[Formula]) = {
+      BinOp.makeL(Equal.apply, terms, True)
+    }
+    def make(terms: Formula*) = {
+      BinOp.makeL(Equal.apply, terms, True)
     }
   }
 

src/main/scala/de/tum/workflows/foltl/FOTransformers.scala

@@ -114,8 +114,8 @@ object FOTransformers extends LazyLogging {
         logger.warn("Trying to generate inequalities for different sized vectors")
       }
       val ineqs = l1.zip(l2).filterNot(x => x._1 == x._2).map {
-        case (x, y) if x.name <= y.name => Neg(Eq(x,y))
-        case (x, y)  => Neg(Eq(y,x))
+        case (x, y) if x.name <= y.name => Neg(Equal(x,y))
+        case (x, y)  => Neg(Equal(y,x))
       }.toSet
       Or.make(ineqs.toList)
     }
@@ -136,7 +136,7 @@ object FOTransformers extends LazyLogging {
     val HNegativeargs = H.map(getNegativeBArguments)
 
     if (H.nonEmpty) {
-      logger.warn("BSFO SOQE: H is not empty, Ackermann not applicable")
+      logger.debug("BSFO SOQE: H is not empty, Ackermann not applicable")
     }
 
     val fE = And.make(E.map(c => Or.make(pruneBs(c))))
@@ -164,10 +164,7 @@ object FOTransformers extends LazyLogging {
 
     val freeparams = b.params.map(p => FormulaFunctions.generateName(p, bounds.toSet))
     val gkineq = for ((gk, gargs) <- gks.zip(Gargs); garg <- gargs) yield {
-      Or.make(gk
-        ,
-        ineq(garg, freeparams)
-      )
+      Or.make(gk, ineq(garg, freeparams))
     }
     val fsol:Formula = And.make(gkineq)
     val fsolq = FormulaFunctions.rewrapQuantifiers(quantifiers, fsol)

src/main/scala/de/tum/workflows/foltl/FormulaFunctions.scala

@@ -92,8 +92,8 @@ object FormulaFunctions extends LazyLogging {
       //      case Or(t1, Neg(t2)) if t1 == t2        => True
 
       // Equivalence
-      case Eq(t1, t2) if t1 == t2 => True
-      case Eq(v1:Var, v2:Var) if v1.name > v2.name => Eq(v2, v1)
+      case Equiv(t1, t2) if t1 == t2 => True
+      case Equiv(v1:Var, v2:Var) if v1.name > v2.name => Equiv(v2, v1)
 
       // Double Temporals
       case Finally(Finally(t)) => Finally(t)
@@ -174,7 +174,9 @@ object FormulaFunctions extends LazyLogging {
 
   def eliminateEq(f: Formula): Formula = {
     f everywhere {
-      case Eq(f1, f2) => {
+      // TODO: switch eq between funs to lra
+      case Equiv(v1:Var, v2:Var) => Equiv(v1,v2)
+      case Equiv(f1, f2) => {
         val e1 = eliminateEq(f1)
         val e2 = eliminateEq(f2)
         And(Implies(e1, e2), Implies(e2, e1))
@@ -345,7 +347,7 @@ object FormulaFunctions extends LazyLogging {
     f.everywhere({
       case ForallOtherThan(vars, otherthan, fp) => {
         val eqs = for (x <- vars; y <- otherthan) yield {
-          Neg(Eq(x, y))
+          Neg(Equiv(x, y))
         }
         Forall(vars, Implies(And.make(eqs), fp.removeOTQuantifiers()))
       }

src/main/scala/de/tum/workflows/foltl/Properties.scala

@@ -13,7 +13,7 @@ object Stubborn {
     And.make(for (c <- choices.toList if c.params.head.typ == agent.typ) yield {
       val f = c.updatedParams(0, agent)
     	Globally(
-    	  Forall(c.params.drop(1), Eq(f.in(T1), f.in(T2)))    
+    	  Forall(c.params.drop(1), Equiv(f.in(T1), f.in(T2)))
    		)
     })
   }
@@ -25,7 +25,7 @@ object Causal {
     
     val equalchoices = for (c <- inputs.toList if c.params.head.typ == agent.typ) yield {
       val newc = c.updatedParams(0, agent)
-      Forall(c.params.drop(1), Eq(newc.in(T1), newc.in(T2)))                    
+      Forall(c.params.drop(1), Equiv(newc.in(T1), newc.in(T2)))
     }
     
     val noutputs = outputs.filter(_.params.head.typ == agent.typ)
@@ -53,7 +53,7 @@ object Causal {
           variable
         }
         val newo = o.updatedParams(agent :: agents)
-        val t = Neg(Eq(newo.in(T1), newo.in(T2)))
+        val t = Neg(Equiv(newo.in(T1), newo.in(T2)))
         
         Noninterference.buildViolations(agents, t, others)
     }
@@ -99,7 +99,7 @@ object Noninterference extends LazyLogging {
     
     val decl = Declassification(spec)
     
-    val difference = Neg(Eq(spec.target.in(T1), spec.target.in(T2)))
+    val difference = Neg(Equiv(spec.target.in(T1), spec.target.in(T2)))
     val diff = buildViolations(spec.target.params.drop(1), difference, spec.causals)
     
     Exists(agent, And.make(samechoices, decl, Finally(Exists(spec.target.params.drop(1), diff))))
@@ -111,7 +111,7 @@ object Declassification extends {
     val sameoracles = for ((o,(p,t)) <- spec.declass) yield {
       val fun = Fun(o, None, p)
       // Forall fv(o). (t_T1 and t_t2) -> G (o_T1 <-> o_T2) 
-      Globally(Forall(p, Implies(Or(t.in(T1), t.in(T2)), Eq(fun.in(T1), fun.in(T2)))))
+      Globally(Forall(p, Implies(Or(t.in(T1), t.in(T2)), Equiv(fun.in(T1), fun.in(T2)))))
     }
     And.make(sameoracles.toList)
   }
@@ -139,7 +139,7 @@ object Properties {
     
     val decl = Declassification(spec)
     
-    val noninter = Exists(agents, And(decl, Finally(Neg(Eq(spec.target.in(T1), spec.target.in(T2))))))
+    val noninter = Exists(agents, And(decl, Finally(Neg(Equiv(spec.target.in(T1), spec.target.in(T2))))))
     
     // maybe add exists t1, t2. phi?
     And.make(cfg, sem.in(T1, equals), sem.in(T2, equals), noninter)

src/main/scala/de/tum/workflows/owltransformer/OwlTransformer.scala

@@ -73,7 +73,7 @@ object OwlTransformer extends LazyLogging {
         Conjunction.of(e1, e2)
       }
 
-      case Eq(f1, f2) => {
+      case Equiv(f1, f2) => {
         val e1 = transform(f1)
         val e2 = transform(f2)
         Biconditional.of(e1, e2).nnf()

src/main/scala/de/tum/workflows/toz3/InvariantGenerator.scala

@@ -12,7 +12,7 @@ object InvariantGenerator {
   
   def genEq(f: Fun, p: List[Var]) = {
     val newf = f.parallelRename(f.params, p)
-    Eq(newf.in(T1), newf.in(T2))
+    Equiv(newf.in(T1), newf.in(T2))
   }
 
 //  def invariantNoninterStubborn(spec: Spec) = {

src/main/scala/de/tum/workflows/toz3/Z3FOEncoding.scala

@@ -64,7 +64,14 @@ object Z3FOEncoding extends LazyLogging {
         ctx.mkAnd(e1, e2)
       }
 
-      case Eq(f1, f2) => {
+      case Equiv(f1, f2) => {
+        logger.warn("Sending equiv <-> to Z3")
+        val e1 = toBoolZ3(ctx, f1, var_ctx)
+        val e2 = toBoolZ3(ctx, f2, var_ctx)
+        ctx.mkEq(e1, e2)
+      }
+
+      case Equal(f1, f2) => {
         val e1 = toSortedZ3(ctx, f1, var_ctx)
         val e2 = toSortedZ3(ctx, f2, var_ctx)
         ctx.mkEq(e1, e2)
@@ -169,7 +176,13 @@ object Z3FOEncoding extends LazyLogging {
       case f2 if f2.isAnd() => And.make(f2.getArgs.map(mapback).toList)
       case f2 if f2.isOr() => Or.make(f2.getArgs.map(mapback).toList)
       case f2 if f2.isImplies() => Implies.make(f2.getArgs.map(mapback).toList)
-      case f2 if f2.isEq() => Eq.make(f2.getArgs.map(mapback).toList)
+      case f2 if f2.isEq() => {
+        if (f2.getArgs.head.isBool) {
+          Equiv.make(f2.getArgs.map(mapback).toList)
+        } else {
+          Equal.make(f2.getArgs.map(mapback).toList)
+        }
+      }
       case f2 if f2.isNot() => Neg(mapback(f2.getArgs().head))
       case f2 if f2.isTrue() => True
       case f2 if f2.isFalse() => False
@@ -189,6 +202,10 @@ object Z3FOEncoding extends LazyLogging {
           Forall(vars, inner)
         }
       }
+      case f2 if f2.isVar() || f2.isConst() => {
+        mapbackToVar(f2)
+      }
+      // Why is a a constant also isApp?
       case f2 if f2.isApp() => {
         val name = FunNameFromVar.unapply(f2.getFuncDecl().getName.toString)
         if (name.isEmpty) {
@@ -197,12 +214,7 @@ object Z3FOEncoding extends LazyLogging {
         val params = f2.getArgs().map(mapbackToVar).toList
         Fun(name.get._1, name.get._2, params)
       }
-      case f2 if f2.isVar() => {
-        mapbackToVar(f2)
-      }
-      case f2 if f2.isConst() => {
-        mapbackToVar(f2)
-      }
+
       case x => {
         logger.error(s"Error mapping expression back from Z3: Could not parse $x")
         Var("unknown")

src/main/scala/de/tum/workflows/toz3/Z3LTL.scala

@@ -195,7 +195,7 @@ object Z3LTL extends LazyLogging {
         ctx.mkAnd(e1, e2)
       }
 
-      case Eq(f1, f2) => {
+      case Equiv(f1, f2) => {
         val e1 = toZ3(ctx, f1, texpr, tvar, var_ctx)
         val e2 = toZ3(ctx, f2, texpr, tvar, var_ctx)
         ctx.mkEq(e1, e2)

src/main/scala/de/tum/workflows/toz3/Z3QFree.scala

@@ -170,7 +170,7 @@ object Z3QFree extends LazyLogging {
         ctx.mkAnd(e1, e2)
       }
 
-      case Eq(f1, f2) => {
+      case Equiv(f1, f2) => {
         val e1 = toZ3(ctx, f1)
         val e2 = toZ3(ctx, f2)
         ctx.mkEq(e1, e2)
@@ -249,11 +249,16 @@ object Z3QFree extends LazyLogging {
     }
   }
 
+  @deprecated
   def mapback(e: Expr): Formula = {
     e match {
       case f2 if f2.isAnd()   => And.make(f2.getArgs.map(mapback).toList)
       case f2 if f2.isOr()    => Or.make(f2.getArgs.map(mapback).toList)
-      case f2 if f2.isEq()    => Eq.make(f2.getArgs.map(mapback).toList)
+      case f2 if f2.isEq()    => if (f2.getArgs.head.isBool) {
+        Equiv.make(f2.getArgs.map(mapback).toList)
+      } else {
+        Equal.make(f2.getArgs.map(mapback).toList)
+      }
       case f2 if f2.isNot()   => Neg(mapback(f2.getArgs().head))
       case f2 if f2.isTrue()  => True
       case f2 if f2.isFalse() => False

src/test/scala/de/tum/workflows/tests/EncodingTest.scala

@@ -42,8 +42,8 @@ class EncodingTest extends FlatSpec {
     sanity should be(
       And.make(n0, Neg(n1), Globally(Neg(And(n0, n1)))))
 
-    val rstays = Forall(List("x", "s"), Eq(Next(Rxs), Rxs))
-    val ostays = Forall(List("s"), Eq(Next(Os), Os))
+    val rstays = Forall(List("x", "s"), Equiv(Next(Rxs), Rxs))
+    val ostays = Forall(List("s"), Equiv(Next(Os), Os))
 
     //    if O stays
     //    sem should be(
@@ -58,7 +58,7 @@ class EncodingTest extends FlatSpec {
       Globally(
         And(
           Implies(And(n0, Next(n1)),
-            Forall(List("x", "s"), Eq(Next(Rxs), Or(Rxs, And(Os, aux0xs))))),
+            Forall(List("x", "s"), Equiv(Next(Rxs), Or(Rxs, And(Os, aux0xs))))),
           Implies(And(n1, Next(n1)), rstays))))
 
     init should be(
@@ -73,7 +73,7 @@ class EncodingTest extends FlatSpec {
 
     stubness should be (
       Globally(
-        Forall(List("y"), Eq(auxa1.in(T1), auxa1.in(T2)))))
+        Forall(List("y"), Equiv(auxa1.in(T1), auxa1.in(T2)))))
   }
 
   "Noninterference encoding" should "work" in {
@@ -89,8 +89,8 @@ class EncodingTest extends FlatSpec {
 
     nonint should be(
       Exists(List("a"), And(
-        Globally(Forall("y", Eq(aux0ay.in("t1"), aux0ay.in("t2")))),
-        Finally(Exists("b", Neg(Eq(Rab.in("t1"), Rab.in("t2"))))))))
+        Globally(Forall("y", Equiv(aux0ay.in("t1"), aux0ay.in("t2")))),
+        Finally(Exists("b", Neg(Equiv(Rab.in("t1"), Rab.in("t2"))))))))
   }
 
   "Property encoding" should "work" in {
@@ -105,7 +105,7 @@ class EncodingTest extends FlatSpec {
     noninter should be (
       Exists("ax", And(
         Stubborn("ax", choices),
-        Finally(Exists("as", Neg(Eq(ce.in(T1), ce.in(T2))))))))
+        Finally(Exists("as", Neg(Equiv(ce.in(T1), ce.in(T2))))))))
 
     val s2 = Spec(w, Map(), Fun("R", List("ax", "as")), List())
     val prop = Properties.noninterStubborn(s2)

src/test/scala/de/tum/workflows/tests/FOLTLTest.scala

@@ -18,13 +18,13 @@ class FOLTLTest extends FlatSpec {
     val f = ForallOtherThan("x", List("y", "z"), Globally("x"))
     val res = f.removeOTQuantifiers()
     res should be(
-      Forall("x", Implies(And(Neg(Eq("x", "y")), Neg(Eq("x", "z"))), Globally("x")))
+      Forall("x", Implies(And(Neg(Equiv("x", "y")), Neg(Equiv("x", "z"))), Globally("x")))
     )
     
     val f2 = ForallOtherThan(List("x","y"), "z", Globally("x"))
     val res2 = f2.removeOTQuantifiers()
     res2 should be(
-      Forall(List("x","y"), Implies(And(Neg(Eq("x", "z")), Neg(Eq("y", "z"))), Globally("x")))
+      Forall(List("x","y"), Implies(And(Neg(Equiv("x", "z")), Neg(Equiv("y", "z"))), Globally("x")))
     )
   }
   

src/test/scala/de/tum/workflows/tests/InferenceTests.scala

@@ -26,7 +26,7 @@ class InferenceTests  extends FlatSpec {
     val yt = Var("yt","X")
     val pt = Var("pt","P")
 //    val rt = Var("rt","R")
-    val inv = Forall(List(pt, yt), genEq("Comm", List(xt, yt, pt)))
+    val inv = Forall(List(xt, pt, yt), genEq("Comm", List(xt, yt, pt)))
     assert(checkSafeStubborn(name, inv))
   }
 
@@ -40,4 +40,23 @@ class InferenceTests  extends FlatSpec {
     assert(checkSafeCausalElim(name, "", inv))
   }
 
+  it should "prove safe loopy stubborn stuff safe" in {
+    val name = "tests/conference_stubborn_withB"
+    val xat = Var("xat","A")
+    val xbt = Var("xbt","A")
+    val pt = Var("pt","P")
+    //    val rt = Var("rt","R")
+    val inv = Forall(List(xat, xbt, pt), genEq("Read", List(xat, xbt, pt)))
+    assert(checkSafeStubborn(name, "", inv))
+  }
+
+  ignore should "prove safe loopy causal stuff safe" in {
+    val name = "tests/conference_stubborn_withB"
+    val xat = Var("xat","A")
+    val xbt = Var("xbt","A")
+    val pt = Var("pt","P")
+    //    val rt = Var("rt","R")
+    val inv = Forall(List(xat, xbt, pt), genEq("Read", List(xat, xbt, pt)))
+    assert(checkSafeCausalElim(name, "", inv))
+  }
 }

src/test/scala/de/tum/workflows/tests/InvariantTest.scala

@@ -40,7 +40,7 @@ class InvariantTest extends FlatSpec {
 
     val spec = ExampleWorkflows.parseExample("tests/simpleChoiceNoOracle").get
 
-    val inv = Forall(List("a", "b"), Eq(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
+    val inv = Forall(List("a", "b"), Equiv(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
 
     val (safe, msg, time) = InvariantChecker.checkInvariantFPDot(spec, inv)
 
@@ -91,7 +91,7 @@ class InvariantTest extends FlatSpec {
   def genEq(name:String, params: List[Var]) = {
     val o1 = Fun(name, Some("t1"), params)
     val o2 = Fun(name, Some("t2"), params)
-    Eq(o1, o2)
+    Equiv(o1, o2)
   }
 //  
 //  it should "prove noninter invariants" in {

src/test/scala/de/tum/workflows/tests/OwlTest.scala

@@ -26,7 +26,7 @@ class OwlTest  extends FlatSpec with LazyLogging {
       (Next(Or(Var("x"), Var("y"))), "X(x | y)"),
       (And(Var("x"), Var("y")), "(x & y)"),
       (Globally(Finally(Var("y"))), "GF y"),
-      (Next(Finally(Eq(Var("y"), Var("z")))), "XF (y <-> z)")
+      (Next(Finally(Equiv(Var("y"), Var("z")))), "XF (y <-> z)")
     )
 
     for (t <- tests) {

src/test/scala/de/tum/workflows/tests/TestUtils.scala

@@ -35,6 +35,6 @@ object TestUtils {
   def genEq(name: String, params: List[Var]) = {
     val o1 = Fun(name, Some("t1"), params)
     val o2 = Fun(name, Some("t2"), params)
-    Eq(o1, o2)
+    Equiv(o1, o2)
   }
 }
\ No newline at end of file

src/test/scala/de/tum/workflows/tests/Z3BSFOTest.scala

@@ -33,7 +33,7 @@ class Z3BSFOTest extends FlatSpec with LazyLogging {
   }
 
   it should "check equalities" in {
-    val easyForm = Forall(List("x","y"), Eq("x", "y"))
+    val easyForm = Forall(List("x","y"), Equiv("x", "y"))
 
     val (s, solver) = Z3BSFO.checkAE(easyForm)
 
@@ -42,7 +42,7 @@ class Z3BSFOTest extends FlatSpec with LazyLogging {
   }
 
   it should "check disequalities" in {
-    val easyForm = Forall(List("x","y"), Neg(Eq("x", "y")))
+    val easyForm = Forall(List("x","y"), Neg(Equiv("x", "y")))
 
     val (s, solver) = Z3BSFO.checkAE(easyForm)
 

src/test/scala/de/tum/workflows/tests/Z3LTLQFreeTest.scala

@@ -73,7 +73,7 @@ import com.microsoft.z3.Status
   it should "simplify stuff" in {
     Z3QFree.simplifyQFree(And(Or(Fun("a", List()), Fun("b", List())), Fun("a", List()))) should be (Fun("a", List()))
   
-    val eq = Eq(Fun("A", List("x")), Fun("A", List("y")))
+    val eq = Equiv(Fun("A", List("x")), Fun("A", List("y")))
     Z3QFree.simplifyQFree(eq) 
     Z3QFree.simplifyQFree(False) should be (False)
   }