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

THEOREM NOT_XOR_EQ ==

\A x,y \in {TRUE, FALSE} : ~xor[x,y] => x=y

PROOF

<1> TAKE x,y \in {TRUE, FALSE}

<1>1 CASE x=FALSE /\ y=FALSE

<2>1 ~xor[x,y] = TRUE BY DEF xor

<2>2 QED BY <2>1

<1>2 x=FALSE /\ y=TRUE

<2>3 ~xor[x,y] = FALSE BY DEF xor

<2>4 QED BY <2>3

<1>3 x=TRUE /\ y=FALSE

<2>5 ~xor[x,y] = FALSE BY DEF xor

<2>6 QED BY <2>5

<1>4 x=TRUE /\ y=TRUE

<2>7 ~xor[x,y] = TRUE BY DEF xor

<2>8 QED BY <2>7

<1>5 QED BY <1>1, <1>2, <1>3, <1>4

On Sunday, November 6, 2022 at 2:36:04 AM UTC-6 Stephan Merz wrote:

Hello,

first of all, please do not send screen shots unless you want to illustrate some behavior of the GUI: TLA+ source is pure ASCII and can be copied and pasted into messages.

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.h...@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+u...@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>