simplex-chat
Rfc/private groups
This is still quite rough and needs substantially more detail. Specifically, it also needs to cover contention and other membership alterations. I think it also needs to ensure that messages are delivered in reasonable ways as membership changes. However, I figured that sharing early and often is the best approach for something like this.
This also includes a TLA+ specification, which I find to be an enormously helpful tool for things like this. It mathematically models the system, which ensures that the description is perfectly precise, and then it can model check properties by running a complete simulation of all possible outcomes by a small model of the world. It can do proofs too, but that's likely more than needed here.
TLA+ specifications typically need to be quite abstract to be helpful, which is why many details that are important to SMP are ignored. If every detail is considered, then it becomes very challenging to both read and check. The right level of abstraction lets us zoom in specifically on the relevant part of the protocol being described. I plan to go back and add a lot more comments here so that it's easier to follow without too much TLA+ knowledge.
Hope this seems like a compelling proposal! I'll keep fleshing it out, and I'm looking forward to feedback.
@epoberezkin At this point, I think the guts of this RFC are here, and most of the edge cases are ironed out (contention, liveness). Be curious to get an early review as I continue to work on fleshing this out further. Cheers!