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.