Merge branch 'equivalence-patch' into 'master'

Equivalence patch

See merge request !12

cmd/vplogic/query.go

@@ -355,7 +355,7 @@ func queryEquivalence(
 	}
 	values := []*Value{}
 	for i := 0; i < len(query.Constants); i++ {
-		a, _ := valueResolveConstant(query.Constants[i], valPrincipalState)
+		a, _ := valueResolveConstantEqv(query.Constants[i], valPrincipalState)
 		values = append(values, a)
 	}
 	brokenEquivalence := false

cmd/vplogic/value.go

@@ -474,6 +474,14 @@ func valueResolveConstant(c *Constant, valPrincipalState *PrincipalState) (*Valu
 	return valPrincipalState.Assigned[i], i
 }
 
+func valueResolveConstantEqv(c *Constant, valPrincipalState *PrincipalState) (*Value, int) {
+	i := valueGetPrincipalStateIndexFromConstant(valPrincipalState, c)
+	if i < 0 {
+		return &Value{Kind: typesEnumConstant, Data: c}, i
+	}
+	return valPrincipalState.Assigned[i], i
+}
+
 func valueResolveValueInternalValuesFromKnowledgeMap(
 	a *Value, valKnowledgeMap *KnowledgeMap,
 ) (*Value, []*Value) {

examples/problematic.vp

+attacker[passive]
+
+principal Server[
+	generates x
+	generates y
+	gx = G^x
+	gy = G^y
+	gxy = gx^y
+	gyx = gy^x
+]
+
+queries[
+	equivalence? gxy, gyx
+]