XOR operator for DHT based protocol verification

[Earnshaw]

Hello everyone:

I am now wirting a Spec to verfiy a DHT ( peer-to-peer distributed hash table)  protocol,  the key algorithm is based on an enhanced version of  Kademlia.

As we now, for such peer to peer network, the logic distance of two nodes

is computed as the exclusive or (XOR) of the two node IDs, taking the result as an unsigned integer number.

d(a,b)=a⊕b

but how can I build such ⊕ operator or function in TLA+?

Of course, in my spec I can replace the logic distance computation with  

d(a,b)=|a-b | ,   but this is not a ideal solution.

  

[Andrew Helwer]

I think you could do it as follows:

1. Write a function NatToBinary[n \in Nat] converting a natural number to a Seq(BOOLEAN)
2. Write a function XorBinary[a, b \in Seq(BOOLEAN)] XOR'ing two Seq(BOOLEAN) to a single Seq(BOOLEAN) (note that /= on each element is equivalent to XOR for this purpose)
3. Write a function BinaryToNat[b \in Seq(BOOLEAN)] converting a Seq(BOOLEAN) to a natural number

Then given two node IDs n and m, evaluate BinaryToNat[XorBinary[NatToBinary[n], NatToBinary[m]]].

Andrew

[Markus Kuppe]

On 12/2/21 2:12 AM, Earnshaw wrote:
> Hello everyone:
>
> I am now wirting a Spec to verfiy a DHT ( peer-to-peer distributed hash
> table)  protocol,  the key algorithm is based on an enhanced version of
> Kademlia.
>
> As we now, for such peer to peer network, the logic distance of two nodes

> is computed as the /exclusive or (XOR)
> <https://en.wikipedia.org/wiki/Exclusive_or>/ of the two node IDs,

> taking the result as an unsigned integer number

> <https://en.wikipedia.org/wiki/Integer>.

>
> d(a,b)=a⊕b
>
>
> but how can I build such ⊕ operator or function in TLA+?
>
> Of course, in my spec I can replace the logic distance computation with
> d(a,b)=|a-b | ,   but this is not a ideal solution.

https://github.com/tlaplus/CommunityModules/blob/master/modules/Bitwise.tla#L39-L51

[Siegfried Bublitz]

Hi,

what about this?

EXTENDS Integers, Sequences

\* The Hamming Distance between two vectors of equal length is the number
\* of components at which they differ.

RECURSIVE HamDist(_,_) \* define as prefix operator
HamDist(a,b) == IF Len(a) # Len (b) THEN -1 \* or some undefined value
                              ELSE IF a = <<>> THEN 0     \* this implies b = <<>>
                                         ELSE IF Head(a) = Head(b) THEN HamDist(Tail(a),Tail(b))
                                                    ELSE 1 + HamDist(Tail(a),Tail(b))


a (+) b == HamDist(a,b) \* define as infix operator        

Siegfried