feat:Communication Layer #50
Conversation
There was a problem hiding this comment.
This looks overall good, my main question are:
- What is the use of the receiver predicates? I don't understand what goal they achieve, and the pre-conditions they appear in seem in general difficult to prove.
- I think we could require sender predicates to stay true when the trace grows, this would avoid using something like
forall tr'. tr <$ tr' ==> higher_pred tr' ...
fabian-hk
force-pushed
the
feature/communication-layer
branch
from
a9f3be2 to
d0682e8
Compare
fabian-hk
changed the base branch from
main
to
feature/add-key-to-crypto-preds
fabian-hk
force-pushed
the
feature/add-key-to-crypto-preds
branch
from
f2945e2 to
96c58c5
Compare
fabian-hk
force-pushed
the
feature/communication-layer
branch
from
129ea3a to
46081f2
Compare
fabian-hk
force-pushed
the
feature/communication-layer
branch
from
46081f2 to
e54cca9
Compare
fabian-hk
force-pushed
the
feature/communication-layer
branch
from
b3630b9 to
c2205c5
Compare
|
This PR is ready to be merged from my side. There will be improvements in the future, but I believe this is a solid basis. |
…of for receive_response function
…sponse; Updated pre-condition of send_response_proof
… additional label; Cleanup
…r a meaning full trace printing function; Com Layer trace printing functions
fabian-hk
force-pushed
the
feature/communication-layer
branch
from
3743479 to
7deb02c
Compare
There was a problem hiding this comment.
While I have a lot of comments, I think it's probably best to get this merged properly, and then I can turn the most relevant ones into issues for the future (since none seem really blocking to me, more things that we should keep in mind as we continue to use this library and see what additional functionality we want out of it). It would be nice if a few of the small changes were made, but these also seem not critical to me, and I think for the sake of ease of review, it would be better to get this merged, and then do a follow-up cleanup PR for any minor changes.
| // We explicitly do not use `event_triggered tr receiver | ||
| // (CommConfReceiveMsg receiver (serialize a payload))` as a | ||
| // post-condition here. The reason for the following form of the | ||
| // post-condition is that it allows us on the higher layer to assert a | ||
| // statement `b` contained in the `higher_layer_preds` that depends on | ||
| // some field `field1` of the payload in the following way: `b | ||
| // payload.field1 \/ is_publishable tr payload.field1`. | ||
| event_triggered tr sender (CommConfSendMsg sender receiver (serialize a payload)) |
There was a problem hiding this comment.
It's not entirely obvious to me why this is needed --- my intuition is that CommConfReceiveMsg existing implies a corresponding earlier CommConfSendMsg must exist (or that the payload is publishable), and so this would seem to me to be a slightly stronger guarantee with ReceiveMsg instead. Does that implication not actually hold, or is there some other technical problem?
There was a problem hiding this comment.
I think this is a technical issue but I did not further investigate it because this form worked for me.
src/lib/communication/DY.Lib.Communication.RequestResponse.Invariants.fst
Show resolved
Hide resolved
src/lib/communication/DY.Lib.Communication.RequestResponse.Invariants.fst
Outdated
Show resolved
Hide resolved
src/lib/communication/DY.Lib.Communication.RequestResponse.Invariants.fst
Outdated
Show resolved
Hide resolved
This PR is an early version of a communication layer. It is a draft PR because it is not yet ready to merge. Currently, the following functionality is implemented:
Note that these functions can and probably will change before this PR can be merged.
You can find minimal example protocols for these functions in this repository: https://github.com/fabian-hk/dolev-yao-star-communication-layer-examples/tree/main