CT: Improve generators sanity checks by not only checking variable clash but assignment clash as well.

[LuisPH3]

CT generators suffer from an anti-pattern, when two conflicting constraints check if the used variables are the same, but do not check if the already assigned values to the variable are the same.

So far the specification may not have produced assignments with this problem, but this is technically incorrect.

• Check all generators:
• Write unit tests for assignment variables clashes for each constraint in each generator.

Technically it is insufficient to just check for the same variable names. What you actually would have to check is whether the values assigned to those variables in the assignment are the same.

For instance, assume there are the following constraints:

Delegates($a), !Delegates($b)

In the current code, these could never cause a conflict, since $a and $b are distinct variables. However, for whatever reasons, the initial assignment could be

a -> Address(1), b -> Address(1)

which would get you

Delegates(Address(1)), !Delegates(Address(1))

which is unsatisfied. This, however, is not detected by this code.

You can see this in this unit test:

func TestDelegateConstraints_MissesConflictsIntroducedByAssignment(t *testing.T) {
	vA := Variable("a")
	vB := Variable("b")

	generator := NewAccountGenerator()
	generator.BindDelegationDesignator(vA, tosca.ColdAccess)
	generator.BindNoDelegationDesignator(vB)

	rnd := rand.New(0)
	assignment := Assignment{}
	_, err := generator.Generate(assignment, rnd, tosca.Address{})
	if err != nil {
		t.Fatalf("Unexpected error during account generation")
	}

	assignment[vA] = NewU256(1)
	assignment[vB] = NewU256(1)
	_, err = generator.Generate(assignment, rnd, tosca.Address{})
	if err == nil {
		t.Fatalf("expected %v to be unsatisfiable", generator)
	}
}

However, I do suspect that issues like this are hidden in many generators and situations like this are currently not showing up in our constraints. So I guess we can ignore this. However, technically this makes this constraint solver incorrect.

Originally posted by @HerbertJordan in #37 (comment)

[LuisPH3]

Attempt to fix this was done in: d80ac56
It was not enough: #37 (comment)

[LuisPH3]

Note: The existing attempt to fix this issue, in the accounts generator, uses the following lambda:

	areVariablesClashing := func(a, b Variable) bool {
		if a == b {
			return true
		}
		if aValue, isBoundA := assignment[a]; isBoundA {
			if bValue, isBoundB := assignment[b]; isBoundB {
				return aValue == bValue
			}
		}
		return false
	}

As commented here: #37 (comment), the generator should attempt to bind variables and prevent later clashes.
I am not 100% convinced about how this should work, as used addresses are stored in a map of already used addresses later down the execution of the algorithm.

I believe that this issue relates to all generators and variable types, not only the account generator. And a holistic approach could be followed in all generators, tests to be updated after the refactor.