controlled variables secure update check should use new gamma for updated controlled variables

[ailrst]

https://github.com/UQ-PAC/bil-to-boogie-translator/blob/7ad7a203b0c945786a84ce0fe2edac6c25bc792a/src/main/scala/translating/IRToBoogie.scala#L606

Here, controlled variables check should use the new gamma, since we want to check that the new classification after updating the control variables is sufficient to store the new values. This only makes a difference $y$ is controlled by $y$, which is not allowed in the logic, but relying on that is less conceptually clear and correct. See eqn 9

[l-kent]

I don't really see the point in changing this. Since x and y must be separate variables, this doesn't make a difference, as you say.

For example, this would just change the output from:

Gamma_x_old := (gamma_load32(Gamma_mem, $x_addr) || L(mem, $x_addr));
mem, Gamma_mem := memory_store32_le(mem, bvadd64(R8, 60bv64), 0bv32), gamma_store32(Gamma_mem, bvadd64(R8, 60bv64), true);
assert ((bvadd64(R8, 60bv64) == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old));

to:

L_x_old := L(mem, $x_addr);
mem, Gamma_mem := memory_store32_le(mem, bvadd64(R8, 60bv64), 0bv32), gamma_store32(Gamma_mem, bvadd64(R8, 60bv64), true);
assert ((bvadd64(R8, 60bv64) == $z_addr) ==> (L(mem, $x_addr) ==> (L_x_old || gamma_load32(Gamma_mem, $x_addr)));