securedrop-client#1617 Unify [Draft]Reply
objects
Read this gist in this order for maximum comprehensibility:
File | Description |
---|---|
README.md |
This readme |
Reply.mmd |
"Hand-drawn" state diagram for a proposed Reply state machine |
Reply.cfg |
TLA+ configuration for the Reply module modeling this state machine |
Reply.tla |
TLA+ specification |
Reply.tla.dot.png |
Graphviz rendering of Reply.tla , to check visually against Reply.mmd |
Reply.tla_liveness.dot.png |
Graphviz rendering of TLA+'s own proof of the Termination liveness property |
- Check recovery modes (e.g.,
DownloadFailed
→Downloaded
at the storage versus controller/GUI layers)- Recovery/retry logic is internal to the pending state represented by a given
ApiJob
implementation. Therefore, failure states are terminal.- Ideally these states would be captured definitively in the model-level state at the storage layer and then propagated up for the controller and GUI layers to filter and handle as they see fit.
- Recovery/retry logic is internal to the pending state represented by a given
- Add deletion
- Deletion can happen at any time!
- Actually, there is a hierarchy:
- Local deletion exits the "alive" state machine and transitions to "dead".
- Remote deletion supervenes on local deletion and transitions to "gone" (that is, actually deleted) whether exiting the "alive" or the "dead" state machine.
- Model states as sets and add invariants/properties
- TLA+'s real magic lies in explicating implicit state machines, where it's useful to be able to define invariants to test expected states.
- Since we already have an explicit state machine, however, and since all
Reply
s are independent, we can define properties directly, without modeling individualReply
's paths through the states (sets). - We can see this because
Reply.tla_liveness.dot.png
is identical (mod colors) toReply.tla.dot.png
: TLA+'s liveness proof of our state machine matches the state machine itself.
The Reply
object is subject to intersection of two independent processes in which client-side intent must be reflected regardless of server-side result:
- Even if a reply fails to send, is rejected, etc., it still exists and has a status.
- Star-related operations could be implemented in this way but need not be.
- Both local and remote deletion may happen at any time, and remote deletion supervenes on local deletion.
- All client-side operations on sources and conversations are subject to this property. Therefore all client-side objects—including their persistent representations and their GUI presentations—should consistently reflect these "alive" and "dead" states.
This model therefore turns out to be a refinement of a general pattern for processing commands, where:
- The Client sends document messages and command messages.
- The Server returns document messages and event messages.
- Both Client and Server are idempotent receivers.
These patterns would give the Client more resilience as an occasionally-connected application. That's out of the scope of this redesign effort, and it ought to depend on the findings of the current E2EE research effort.
@gonzalo-bulnes in https://gist.github.com/cfm/2ca373e7ac5e5397550d7db98289dc3d?permalink_comment_id=4434209#gistcomment-4434209:
Thanks! Fixed in
4802be8
.https://gist.github.com/cfm/2ca373e7ac5e5397550d7db98289dc3d?permalink_comment_id=4434211#gistcomment-4434211:
Not quite! Read—
—as a refinement of the default—
—with two possible
Init
states. SoSpec
begins at (either)Init
and then traverses all possible transitions ofstate
defined byNext
.https://gist.github.com/cfm/2ca373e7ac5e5397550d7db98289dc3d?permalink_comment_id=4434224#gistcomment-4434224:
Right; this is too abstract. For that I'd need to:
NewOutgoingReply
and aNewIncomingReply
through those sets; andNext week!
Isn't that two different models to prove two different things in two different components at two different layers? :-)