add nonce to ping/pong, fix version field

Author: oxarbitrage

messages.tla

@@ -20,12 +20,14 @@ MakeVerack == [
     header |-> [ magic |-> 619259748, command |-> "verack" ]
 ]
 
-MakePing == [
-    header |-> [ magic |-> 619259748, command |-> "ping" ]
+MakePing(nonce) == [
+    header  |-> [ magic |-> 619259748, command |-> "ping" ],
+    payload |-> [ nonce |-> nonce ]
 ]
 
-MakePong == [
-    header |-> [ magic |-> 619259748, command |-> "pong" ]
+MakePong(nonce) == [
+    header  |-> [ magic |-> 619259748, command |-> "pong" ],
+    payload |-> [ nonce |-> nonce ]
 ]
 
 MakeInv(blocks) == [
@@ -50,7 +52,7 @@ MakeHeaders(blocks, timestamp) == [
     header  |-> [ magic |-> 619259748, command |-> "headers" ],
     payload |-> [
         count   |-> 1,
-        headers |-> << [ version |-> 70015, prev_block |-> Cardinality(blocks), merkle_root |-> 0, timestamp |-> timestamp, bits |-> 0, nonce |-> 0 ] >>
+        headers |-> << [ version |-> 170140, prev_block |-> Cardinality(blocks), merkle_root |-> 0, timestamp |-> timestamp, bits |-> 0, nonce |-> 0 ] >>
     ]
 ]
 

protocol.tla

@@ -45,17 +45,18 @@ PingMessage ==
     \E n \in InitialPeers:
         \E m \in OtherPeers[n]:
             /\ nodes[n].last_recv_at[m] <= clock - 3
-            /\ nodes' = [ nodes EXCEPT ![n].channels[m] = Append(@, MakePing) ]
+            /\ nodes' = [ nodes EXCEPT ![n].channels[m] = Append(@, MakePing(clock)) ]
             /\ UNCHANGED << clock >>
 
 PongMessage ==
     \E n \in InitialPeers:
         \E m \in OtherPeers[n]:
             /\ Len(nodes[n].channels[m]) > 0
             /\ nodes[n].channels[m][Len(nodes[n].channels[m])].header.command = "ping"
-            /\ nodes' = [ nodes EXCEPT
-                    ![n].channels[m]     = Append(@, MakePong),
-                    ![n].last_recv_at[m] = clock ]
+            /\ LET ping == nodes[n].channels[m][Len(nodes[n].channels[m])] IN
+                /\ nodes' = [ nodes EXCEPT
+                        ![n].channels[m]     = Append(@, MakePong(ping.payload.nonce)),
+                        ![n].last_recv_at[m] = clock ]
             /\ UNCHANGED << clock >>
 
 InvMessage ==