Prop349: See if we can simplify using Arti model

In Lisbon, I talked with @mikeperry about prop349, and made a suggestion that we could simplify some of the circuit state machines by using a modal "request/response" idea. The idea is that some message types put a circuit into a state where it is expecting a single response. These state machines cannot overlap in time: Only one request can be sent at once, so only one response can ever be correct.

Examples of requests that put a circuit into a given state are:

EXTEND
ESTABLISH_INTRO
ESTABLISH_RENDEZVOUS
INTRODUCE1
RENDEZVOUS1

(If we cannot make this simplification, that's also important to know: it's very closely related to how arti behaves today.)

Next steps here might be for a few of us to sit down in a video chat and walk through the arti source code to look at how messages are validated right now.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information