Re: [tlaplus] How to prove my "compare" function on 4-bit binary numbers is correct?

Since you apply Boolean operations to the elements of your bit vectors, you want to change the co-domain from {0,1} to {TRUE, FALSE}. After that change, TLC can easily evaluate your formula. In my version below, I made xor and cmp_bv4 plain operators rather than definitions of functions (which you get with your version using square brackets). This should not make a difference, but I consider this style to be more idiomatic. (See also section 6.4 of Specifying Systems.) I also strengthened the assertion of your theorem to make it an equivalence and to assert equality of the two bit vectors.

BV4 == [0..3 -> {TRUE, FALSE}]

xor(b0, b1) == (b0 /\ ~ b1) \/ (~ b0 /\ b1)
cmp_bv4(bv0, bv1) ==
  /\ ~ xor(bv0[0], bv1[0])
  /\ ~ xor(bv0[1], bv1[1])
  /\ ~ xor(bv0[2], bv1[2])
  /\ ~ xor(bv0[3], bv1[3])

THEOREM CMP_CORRECT ==
  \A x,y \in BV4 : cmp_bv4(x,y) <=> x = y

Now, create a model in the Toolbox and click on "evaluate constant _expression_". Paste the assertion of the theorem, i.e., the formula

\A x,y \in BV4 : cmp_bv4(x,y) <=> x = y

into the "_expression_" field of the window and click on the green triangle. TLC will report that the _expression_ evaluates to TRUE.

Stephan

On 6 Nov 2022, at 06:57, Amjad Ali <amjad.hamdi.ali@xxxxxxxxx> wrote:

I want to prove cmp_bv4 for all 4-bit binary numbers is correct. As seen below, a binary value of 4 bits is represented as a set of functions with domain 0-3 and range 0 and 1. Then, an xor function with domain 0 and 1 that outputs 0 if the two inputs match (or 1 other, otherwise). Finally, cmp_bv4 takes in two 4-bit binary numbers and uses the xor function to determine if the values match. Why do this and not just use (=) ? In the machine I'm building, a comparator is not available and I need to build one from scratch.
<Screen Shot 2022-11-06 at 12.43.42 AM.png>

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bcd0ac97-be4f-4b5e-b91b-d347dde2cb61n%40googlegroups.com.
<Screen Shot 2022-11-06 at 12.43.42 AM.png>