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

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

 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 NASSUME NNat == N \in NatBVN == [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 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 == 0b0010In 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+unsubscribe@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/C80DC618-2D06-4746-8C89-4951E2A78E92%40gmail.com.

• Follow-Ups: