Re: [tlaplus] How can I prove AND function on 4 bit value in TLAPS

[Amjad Ali <amjad.hamdi.ali@xxxxxxxxx>]

It's weird how defining bv_and as an operator makes this much simpler. Why is this the case?

I have ANDN defined as a function and ANDN2 as an operator. They do the same thing but the proof fails on line <1>3 for ANDN . Under "Poorly Supported Tla Features" in the TLAPS Documentation page, it reads, "For records, the provers usually need to be told explicitly to use a fact of the form r.f = e even when they are given the fact r = [f |-> e, ...]." My guess is this poorly supported feature applies to functions as well because, in my case, the prover cannot see that:

                                PROVE   [i \in 0..N |-> f[i] /\ g[i]]  = [f_1, g_1 \in BVN |-> [i \in 0..N |-> f_1[i] /\ g_1[i]]] [f, g]

All it literally needs to do is apply the [f,g] to the function on the right side and see that it equals the left function.

BVN == [0..N -> {TRUE, FALSE}]

ANDN == [f,g \in BVN |-> [i \in 0..N |-> f[i] /\ g[i]]]

ANDN2(f,g) == [i \in 0..N |-> f[i] /\ g[i]]

THEOREM ANDN2_CORRECT==

    \A f,g \in BVN : \A i \in 0..N :

    ANDN2(f,g)[i] <=> f[i] /\ g[i]

PROOF

    <1>1 TAKE f,g \in BVN

    <1>2 TAKE i \in 0..N

    <1>3 ANDN2(f,g)[i] <=> f[i] /\ g[i]

        BY DEF BVN, ANDN2

    <1> QED BY <1>3

THEOREM ANDN_CORRECT==

    \A f,g \in BVN : \A i \in 0..N : 

    ANDN[f,g][i] <=> f[i] /\ g[i]

PROOF

    <1>1 TAKE f,g \in BVN

    <1>2 TAKE i \in 0..N

    <1>3 ANDN[f,g][i] <=> f[i] /\ g[i]                >>>>>>>>>>>>>>>>>>>> Fails Here

        BY DEF BVN, ANDN

    <1> QED BY <1>3

On Thursday, November 10, 2022 at 3:06:42 AM UTC-6 Stephan Merz wrote:

Before diving into subproofs, it is good practice to get the overall structure of the proof right: start by checking if you can prove the level-1 QED step from the preceding level-1 steps. In your case, since you are claiming an equivalence, you'll need both your step <1>3 and the reverse implication. Your step <1>4 should be one of several level-2 steps beneath step <1>3.

Below is how I would set up the proof, for bit vectors of arbitrary (but fixed) length. Note that the assumption that N is a natural number is not needed for this proof but will probably be useful elsewhere.

Stephan

–––

CONSTANT N
ASSUME NNat == N \in Nat

BVN == [1 .. N -> BOOLEAN]

bv_and(bv1, bv2) == [i \in 1 .. N |-> bv1[i] /\ bv2[i]]

THEOREM 
  ASSUME NEW bv1 \in BVN, NEW bv2 \in BVN, NEW i \in 1 .. N
  PROVE  bv_and(bv1, bv2)[i] <=> bv1[i] /\ bv2[i]
BY DEF BVN, bv_and

On 10 Nov 2022, at 04:58, Amjad Ali <amjad.h...@xxxxxxxxx> wrote:

I've defined a 4 bit value as such:

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

and a function that does an AND operation on two 4 bit values:

AND4 == [f,g \in bv4 |-> [i \in 0..3 |-> (i=0 /\ f[0] /\ g[0]) \/ 

                                                                (i=1 /\ f[1] /\ g[1]) \/

                                                                (i=2 /\ f[2] /\ g[2]) \/

                                                                (i=3 /\ f[3] /\ g[3])     ]]

This function should behave like any an AND operation in any assembly language. For example,  AND 0b1010, 0b0010 == 0b0010

In TLA+, a 4-bit binary number is represented in a form of a function. So, AND4 takes in. two functions and outputs a function.

It's pretty straight forward to see that AND4 would behave as it should, but how can I prove it for any given 4-bit. values.

I tried starting it. Please tell me if I'm on the right track:

THEOREM AND4_CORRECT==

    \A f,g \in bv4 : \A i \in 0..3 : AND4[f,g][i] <=> f[i] /\ g[i]

PROOF

    <1>1 TAKE f,g \in bv4

    <1>2 TAKE i \in 0..3

    <1>3 ASSUME AND4[f,g][i] PROVE f[i] /\ g[i]

    <1>4 CASE i = 0

        <2>1 f[0] /\ g[0]

            

        <2> QED

    

    <1> QED

--
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/a54e1db7-6807-4de1-bfdf-d7fe738a5ba8n%40googlegroups.com.

-- 
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/4e50b05c-19bb-4673-ba06-7933b41412cen%40googlegroups.com.