fix everything: should now be consistent and correct

Start with machines.dot, which gives the override. Then traverse downwards
from wormhole.dot .

docs/code.dot

@@ -24,7 +24,7 @@ digraph {
         S2 -> P2_got_nameplates [label="got_nameplates"]
         P2_got_nameplates [shape="box" label="stash nameplates\nfor completion"]
         P2_got_nameplates -> S2
-        S2 -> P2_finish [label="<return>" color="orange" fontcolor="orange"]
+        S2 -> P2_finish [label="<hyphen>" color="orange" fontcolor="orange"]
         P2_finish [shape="box" label="lookup wordlist\nfor completion"]
         P2_finish -> S3
         S3 [label="S3: typing\ncode"]
@@ -33,7 +33,7 @@ digraph {
         P3_completion -> S3
 
         S3 -> P0_set_code [label="<return>"
-                                     color="orange" fontcolor="orange"]
+                           color="orange" fontcolor="orange"]
 
         S0 -> P0_allocate [label="allocate"]
         P0_allocate [shape="box" label="C.tx_allocate"]

docs/key.dot

@@ -13,7 +13,7 @@ digraph {
         S0 [label="S0: know\nnothing"]
         S0 -> P0_build [label="set_code"]
 
-        P0_build [shape="box" label="build_pake\nM.set_nameplate\nM.add_message(pake)"]
+        P0_build [shape="box" label="build_pake\nM.add_message(pake)"]
         P0_build -> S1
         S1 [label="S1: know\ncode"]
 
@@ -28,55 +28,16 @@ digraph {
         something similar, queueing inbound messages until it sees one for
         the phase it currently cares about.*/
 
-        S1 -> P_mood_scary [label="got_message(pake)\npake bad"]
+        S1 -> P_mood_scary [label="got_pake\npake bad"]
-        S1 -> P1_compute [label="got_message(pake)\npake good"]
+        P_mood_scary [shape="box" color="red" label="W.scared"]
-        S1 -> P1_queue_inbound [label="got_message(data)" style="dashed"]
+        P_mood_scary -> S3 [color="red"]
-        P1_queue_inbound [shape="box" style="dotted" label="queue"]
+        S3 [label="S3:\nscared" color="red"]
-        P1_queue_inbound -> S1 [style="dashed"]
+        S1 -> P1_compute [label="got_pake\npake good"]
-        S1 -> P1_queue_version [label="got_message(version)"]
+        #S1 -> P_mood_lonely [label="close"]
-        P1_queue_version [label="queue\nversion??"]
-        P1_queue_version -> S1
-        S1 -> P_mood_lonely [label="close"]
 
-        P1_compute [label="compute_key\nM.add_message(version)\nA.got_verifier" shape="box"]
+        P1_compute [label="compute_key\nM.add_message(version)\nW.got_verifier\nR.got_key" shape="box"]
         P1_compute -> S2
 
-        P_mood_scary [shape="box" label="M.close\nmood=scary"]
+        S2 [label="S2: know_key" color="green"]
-        P_mood_scary -> P_notify_failure
 
-        P_notify_failure [shape="box" label="(record failure)" color="red"]
-        P_notify_failure -> S_closing
-
-        S2 [label="S2: know_key\n(unverified)" color="orange"]
-        S2 -> P2_queue_inbound [label="got_message(data)" style="dashed"]
-        P2_queue_inbound [shape="box" style="dotted" label="queue"]
-        P2_queue_inbound -> S2
-        S2 -> P2_verified [label="got_message(version)\ngood"]
-        S2 -> P_mood_scary [label="got_message(version)\nbad"]
-        S2 -> P_mood_lonely [label="close"] /* more like impatient */
-
-        P2_verified [label="D.got_message(queued)\nA.received(msg)\nencrypt queued\nM.add_message(queued)"
-                      shape="box"]
-        P2_verified -> S3
-
-        S3 [label="S3: know_key\n(verified)" color="green"]
-        S3 -> P3_accept [label="got_message(data)"] /* probably phase */
-        S3 -> P_mood_happy [label="close"]
-        S3 -> P_notify_failure [label="scary"]
-
-        P3_accept [shape="box" label="decrypt\nR.got_message(good,bad)"]
-        P3_accept -> S3
-        P_mood_happy [shape="box" label="M.close\nmood=happy"]
-        P_mood_happy -> S_closing
-
-        P_mood_lonely [shape="box" label="M.close\nmood=lonely"]
-        P_mood_lonely -> S_closing
-
-        S_closing [label="closing"]
-        S_closing -> P_closed [label="closed"]
-        S_closing -> S_closing [label="got_message"]
-
-        P_closed [shape="box" label="A.closed"]
-        P_closed -> S_closed
-        S_closed [label="closed"]
 }

docs/machines.dot

@@ -4,29 +4,46 @@ digraph {
                   color="blue" fontcolor="blue"]
         Mailbox [shape="box" color="blue" fontcolor="blue"]
         Connection [label="Rendezvous\nConnector"
-                    shape="oval" color="blue" fontcolor="blue"]
+                    shape="box" color="blue" fontcolor="blue"]
-        websocket [shape="oval" color="blue" fontcolor="blue"]
+        websocket [color="blue" fontcolor="blue"]
+        Order [shape="box" label="Ordering" color="blue" fontcolor="blue"]
+        Key [shape="box" label="Key" color="blue" fontcolor="blue"]
+        Send [shape="box" label="Send" color="blue" fontcolor="blue"]
+        Receive [shape="box" label="Receive" color="blue" fontcolor="blue"]
         Code [shape="box" label="Code" color="blue" fontcolor="blue"]
         Nameplates [shape="box" label="Nameplate\nLister"
                     color="blue" fontcolor="blue"
                     ]
-        {rank=same; Nameplates Code}
 
         Connection -> websocket [color="blue"]
+        #Connection -> Order [color="blue"]
 
         App -> Wormhole [style="dashed" label="set_code\nsend\nclose\n(once)"]
-        App -> Wormhole [color="blue"]
+        #App -> Wormhole [color="blue"]
         Wormhole -> App [style="dashed" label="got_verifier\nreceived\nclosed\n(once)"]
 
-        Wormhole -> Connection [color="blue"]
+        #Wormhole -> Connection [color="blue"]
+
+        Wormhole -> Send [style="dashed" label="send"]
 
         Wormhole -> Mailbox [style="dashed"
-                             label="set_nameplate\nadd_message\nclose\n(once)"
+                             label="set_nameplate\nclose\n(once)"
-                             ]
-        Wormhole -> Mailbox [color="blue"]
-        Mailbox -> Wormhole [style="dashed"
-                             label="got_message\nclosed\n(once)"
                              ]
+        #Wormhole -> Mailbox [color="blue"]
+        Mailbox -> Wormhole [style="dashed" label="closed\n(once)"]
+        Mailbox -> Order [style="dashed" label="got_message (once)"]
+        Wormhole -> Key [style="dashed" label="set_code"]
+        Key -> Wormhole [style="dashed" label="got_verifier\nscared"]
+        Order -> Key [style="dashed" label="got_pake"]
+        Order -> Receive [style="dashed" label="got_message"]
+        #Wormhole -> Key [color="blue"]
+        Key -> Mailbox [style="dashed" label="add_message (pake)\nadd_message (version)"]
+        Receive -> Send [style="dashed" label="got_verified_key"]
+        Send -> Mailbox [style="dashed" label="add_message (phase)"]
+
+        Key -> Receive [style="dashed" label="got_key"]
+        Receive -> Wormhole [style="dashed"
+                             label="happy\nscared\ngot_message"]
 
         Mailbox -> Connection [style="dashed"
                                label="tx_claim\ntx_open\ntx_add\ntx_release\ntx_close\nstop"
@@ -41,7 +58,7 @@ digraph {
                                   label="tx_list"
                                   ]
 
-        Wormhole -> Code [color="blue"]
+        #Wormhole -> Code [color="blue"]
         Code -> Connection [style="dashed"
                             label="tx_allocate"
                             ]
@@ -50,10 +67,12 @@ digraph {
         Nameplates -> Code [style="dashed"
                             label="got_nameplates"
                             ]
-        Code -> Nameplates [color="blue"]
+        #Code -> Nameplates [color="blue"]
         Code -> Nameplates [style="dashed"
                             label="refresh_nameplates"
                             ]
+        Code -> Wormhole [style="dashed"
+                          label="set_code"]
         
         
 

docs/mailbox.dot

@@ -86,8 +86,9 @@ digraph {
         P3_process_ours -> S3B
         S3B -> P3_process_theirs [label="rx_message\n(theirs)"
                                       color="orange" fontcolor="orange"]
-        P3_process_theirs [shape="box" label="C.tx_release\nW.got_message"
+        P3_process_theirs [shape="box" color="orange"
-                              color="orange"]
+                           label="C.tx_release\nO.got_message if new\nrecord"
+                           ]
         /* pay attention to the race here: this process_message() will
         deliver msg_pake to the WormholeMachine, which will compute_key() and
         send(version), and we're in between S1A (where send gets
@@ -116,7 +117,7 @@ digraph {
         P4_process_ours [shape="box" label="dequeue"]
         P4_process_ours -> S4B
         S4B -> P4_process_theirs [label="rx_message\n(theirs)"]
-        P4_process_theirs [shape="box" label="W.got_message"]
+        P4_process_theirs [shape="box" label="O.got_message if new\nrecord"]
         P4_process_theirs -> S4B
 
         S4A -> S5A [label="(none)" style="invis"]
@@ -145,7 +146,7 @@ digraph {
         P5_process_ours [shape="box" label="dequeue"]
         P5_process_ours -> S5B
         S5B -> P5_process_theirs [label="rx_message\n(theirs)"]
-        P5_process_theirs [shape="box" label="W.got_message"]
+        P5_process_theirs [shape="box" label="O.got_message if new\nrecord"]
         P5_process_theirs -> S5B
 
         foo5 [label="" style="invis"]

docs/order.dot

@@ -0,0 +1,35 @@
+digraph {
+        start [label="Order\nMachine" style="dotted"]
+        /* our goal: deliver PAKE before anything else */
+
+        {rank=same; S0 P0_other}
+        {rank=same; S1 P1_other}
+
+        S0 [label="S0: no pake" color="orange"]
+        S1 [label="S1: yes pake" color="green"]
+        S0 -> P0_pake [label="got_pake"
+                       color="orange" fontcolor="orange"]
+        P0_pake [shape="box" color="orange"
+                 label="K.got_pake\ndrain queue:\n[R.got_message]"
+                 ]
+        P0_pake -> S1 [color="orange"]
+        S0 -> P0_other [label="got_version\ngot_phase" style="dotted"]
+        P0_other [shape="box" label="queue" style="dotted"]
+        P0_other -> S0 [style="dotted"]
+
+        S1 -> P1_other [label="got_version\ngot_phase"]
+        P1_other [shape="box" label="R.got_message"]
+        P1_other -> S1
+
+        
+        /* the Mailbox will deliver each message exactly once, but doesn't
+        guarantee ordering: if Alice starts the process, then disconnects,
+        then Bob starts (reading PAKE, sending both his PAKE and his VERSION
+        phase), then Alice will see both PAKE and VERSION on her next
+        connect, and might get the VERSION first.
+
+        The Wormhole will queue inbound messages that it isn't ready for. The
+        wormhole shim that lets applications do w.get(phase=) must do
+        something similar, queueing inbound messages until it sees one for
+        the phase it currently cares about.*/
+}

docs/receive.dot

@@ -10,40 +10,30 @@ digraph {
 
         start [label="Receive\nMachine" style="dotted"]
 
-        S0 [label="S0: unknown\ncode"]
+        S0 [label="S0:\nunknown key" color="orange"]
-        S0 -> P0_got_key [label="got_verified_key"]
+        S0 -> P0_got_key [label="got_key" color="orange"]
 
-        P0_got_key [shape="box" label="record key"]
+        P0_got_key [shape="box" label="record key" color="orange"]
-        P0_got_key -> S1
+        P0_got_key -> S1 [color="orange"]
 
-        S0 -> P_mood_lonely [label="close"]
+        S1 [label="S1:\nunverified key" color="orange"]
+        S1 -> P_mood_scary [label="got_message\n(bad)"]
+        S1 -> P1_accept_msg [label="got_message\n(good)" color="orange"]
+        P1_accept_msg [shape="box" label="S.got_verified_key\nW.happy\nW.got_message"
+                       color="orange"]
+        P1_accept_msg -> S2 [color="orange"]
 
-        S1 [label="S1: verified\nkey" color="green"]
+        S2 [label="S2:\nverified key" color="green"]
 
-        S1 -> P_mood_scary [label="got_message(bad)"]
+        S2 -> P2_accept_msg [label="got_message\n(good)" color="orange"]
-        S1 -> P1_accept_msg [label="got_message(good)"]
+        S2 -> P_mood_scary [label="got_message(bad)"]
-        S1 -> P_mood_happy [label="close"]
 
-        P1_accept_msg [label="A.received(msg)" shape="box"]
+        P2_accept_msg [label="W.got_message" shape="box" color="orange"]
-        P1_accept_msg -> S1
+        P2_accept_msg -> S2 [color="orange"]
 
-        P_mood_scary [shape="box" label="K.scary"]
+        P_mood_scary [shape="box" label="W.scared" color="red"]
-        P_mood_scary -> S_closed
+        P_mood_scary -> S3 [color="red"]
 
-        P_notify_failure [shape="box" label="(record failure)" color="red"]
+        S3 [label="S3:\nscared" color="red"]
-        P_notify_failure -> S_closing
+        S3 -> S3 [label="got_message"]
-
-        P_mood_happy [shape="box" label="M.close\nmood=happy"]
-        P_mood_happy -> S_closing
-
-        P_mood_lonely [shape="box" label="M.close\nmood=lonely"]
-        P_mood_lonely -> S_closing
-
-        S_closing [label="closing"]
-        S_closing -> P_closed [label="closed"]
-        S_closing -> S_closing [label="got_message"]
-
-        P_closed [shape="box" label="A.closed"]
-        P_closed -> S_closed
-        S_closed [label="closed"]
 }

docs/send.dot

@@ -1,11 +1,14 @@
 digraph {
         start [label="Send\nMachine" style="dotted"]
 
+        {rank=same; S0 P0_queue}
+        {rank=same; S1 P1_send}
+        
         S0 [label="S0: unknown\nkey"]
-        S0 -> P0_queue [label="send" style="dashed"]
+        S0 -> P0_queue [label="send" style="dotted"]
-        P0_queue [shape="box" label="queue" style="dashed"]
+        P0_queue [shape="box" label="queue" style="dotted"]
-        P0_queue -> S0 [style="dashed"]
+        P0_queue -> S0 [style="dotted"]
-        S0 -> P0_got_key [label="set_verified_key"]
+        S0 -> P0_got_key [label="got_verified_key"]
 
         P0_got_key [shape="box" label="drain queue:\n[encrypt\n M.add_message]"]
         P0_got_key -> S1

docs/wormhole.dot

@@ -10,80 +10,48 @@ digraph {
 
         start [label="Wormhole\nMachine" style="dotted"]
 
-        S0 [label="S0: know\nnothing"]
+        {rank=same; P0_code S0}
-        S0 -> P0_queue [label="send" style="dotted"]
+        P0_code [shape="box" style="dashed"
-        P0_queue [shape="box" style="dotted" label="queue"]
+                 label="Code.input\n or Code.allocate\n or Code.set"]
-        P0_queue -> S0 [style="dotted"]
+        P0_code -> S0
+        S0 [label="S0: empty"]
         S0 -> P0_build [label="set_code"]
 
-        P0_build [shape="box" label="build_pake\nM.set_nameplate\nM.add_message(pake)"]
+        P0_build [shape="box" label="M.set_nameplate\nK.set_code"]
         P0_build -> S1
-        S1 [label="S1: know\ncode"]
+        S1 [label="S1: lonely" color="orange"]
-        S1 -> P1_queue [label="send" style="dotted"]
-        P1_queue [shape="box" style="dotted" label="queue"]
-        P1_queue -> S1 [style="dotted"]
 
-        /* the Mailbox will deliver each message exactly once, but doesn't
+        S1 -> S2 [label="happy"]
-        guarantee ordering: if Alice starts the process, then disconnects,
-        then Bob starts (reading PAKE, sending both his PAKE and his VERSION
-        phase), then Alice will see both PAKE and VERSION on her next
-        connect, and might get the VERSION first.
 
-        The Wormhole will queue inbound messages that it isn't ready for. The
+        S1 -> P_close_scary [label="scared" color="red"]
-        wormhole shim that lets applications do w.get(phase=) must do
+        S1 -> P_close_lonely [label="close"]
-        something similar, queueing inbound messages until it sees one for
+        P_close_lonely [shape="box" label="M.close(lonely)"]
-        the phase it currently cares about.*/
+        P_close_lonely -> S_closing
 
-        S1 -> P_mood_scary [label="got_message(pake)\npake bad"]
+        P_close_scary [shape="box" label="M.close(scary)" color="red"]
-        S1 -> P1_compute [label="got_message(pake)\npake good"]
+        P_close_scary -> S_closing [color="red"]
-        S1 -> P1_queue_inbound [label="got_message(other)"]
-        P1_queue_inbound [shape="box" style="dotted" label="queue\ninbound"]
-        P1_queue_inbound -> S1
-        S1 -> P_mood_lonely [label="close"]
 
-        P1_compute [label="compute_key\nM.add_message(version)\nA.got_verifier\nschedule process inbound queue?" shape="box"]
+        S2 [label="S2: happy" color="green"]
-        P1_compute -> S2
+        S2 -> P2_close [label="close"]
+        P2_close [shape="box" label="M.close(happy)"]
+        P2_close -> S_closing
 
-        P_mood_scary [shape="box" label="M.close\nmood=scary"]
+        S2 -> P2_got_message [label="got_message"]
-        P_mood_scary -> P_notify_failure
+        P2_got_message [shape="box" label="A.received"]
-
+        P2_got_message -> S2
-        P_notify_failure [shape="box" label="(record failure)" color="red"]
-        P_notify_failure -> S_closing
-
-        S2 [label="S2: know_key\n(unverified)" color="orange"]
-        S2 -> P_queue3 [label="send" style="dotted"]
-        P_queue3 [shape="box" style="dotted" label="queue"]
-        P_queue3 -> S2 [style="dotted"]
-        S2 -> P_verify [label="got_message"] /* version or phase */
-        S2 -> P_mood_lonely [label="close"] /* more like impatient */
-
-        P_verify [label="verify(msg)" shape="box"]
-        P_verify -> P_accept_msg [label="(good)"]
-        P_verify -> P_mood_scary [label="(bad)"]
-
-        P_accept_msg [label="A.received(msg)\nencrypt queued\nM.add_message(queued)"
-                      shape="box"]
-        P_accept_msg -> S3
-
-        S3 [label="S3: know_key\n(verified)" color="green"]
-        S3 -> P_verify [label="got_message"] /* probably phase */
-        S3 -> P_mood_happy [label="close"]
-        S3 -> P_send [label="send"]
-
-        P_mood_happy [shape="box" label="M.close\nmood=happy"]
-        P_mood_happy -> S_closing
-
-        P_mood_lonely [shape="box" label="M.close\nmood=lonely"]
-        P_mood_lonely -> S_closing
-
-        P_send [shape="box" label="encrypt\nM.add_message(msg)"]
-        P_send -> S3
 
         S_closing [label="closing"]
         S_closing -> P_closed [label="closed"]
-        S_closing -> S_closing [label="got_message"]
+        S_closing -> S_closing [label="got_message\nhappy\nscared\nclose"]
 
-        P_closed [shape="box" label="A.closed"]
+        P_closed [shape="box" label="A.closed(reason)"]
         P_closed -> S_closed
         S_closed [label="closed"]
+
+        {rank=same; Other S_closed}
+        Other [shape="box" style="dashed"
+               label="send -> S.send\ngot_verifier -> A.got_verifier"
+               ]
+
+
 }