[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Amjad Ali <amjad.hamdi.ali@xxxxxxxxx>*Date*: Thu, 10 Nov 2022 04:36:55 -0800 (PST)*References*: <a54e1db7-6807-4de1-bfdf-d7fe738a5ba8n@googlegroups.com> <C80DC618-2D06-4746-8C89-4951E2A78E92@gmail.com>

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_andOn 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:

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

PROOF<1>1

TAKEf,g \in bv4<1>2

TAKEi \in 0..3<1>3

ASSUMEAND4[f,g][i]PROVEf[i] /\ g[i]<1>4

CASEi = 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.

**Follow-Ups**:**Re: [tlaplus] How can I prove AND function on 4 bit value in TLAPS***From:*Stephan Merz

**References**:**[tlaplus] How can I prove AND function on 4 bit value in TLAPS***From:*Amjad Ali

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

- Prev by Date:
**Re: [tlaplus] How to add an auxiliary variable but not increase the state space?** - Next by Date:
**Re: [tlaplus] How can I prove AND function on 4 bit value in TLAPS** - Previous by thread:
**Re: [tlaplus] How can I prove AND function on 4 bit value in TLAPS** - Next by thread:
**Re: [tlaplus] How can I prove AND function on 4 bit value in TLAPS** - Index(es):