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.
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
… Improved documentation
* Some small cleanup of EoL spaces * Revised confidential message/request receipt postconditions * Cleaned up some invariants and proofs with help of a small utility function --------- Co-authored-by: Klaas Pruiksma <klaas.pruiksma@sec.uni-stuttgart.de>
There was a problem hiding this comment.
As before, I think this looks good enough to merge and use --- there are of course always improvements to be made (e.g., I am currently working on making more of the library opaque to SMT), but this is functional in its current state.
The opinion of @TWal on the parse_and_pred function in particular would be welcome, but also generally on the whole library (I don't want to unilaterally merge it without input from the other working groups).
| val parse_and_pred: | ||
| #a:Type -> {| parseable_serializeable bytes a |} -> | ||
| (p:a -> Type0) -> (bytes -> Type0) | ||
| let parse_and_pred #a p = (fun b -> | ||
| match parse a b with | ||
| | None -> False | ||
| | Some x -> p x | ||
| ) |
There was a problem hiding this comment.
This feels to me like a generally good utility function, which we probably do want to have (and which could probably also be used more broadly) --- I also introduced it for that reason. That said, I see a few possible problems with it:
- This may not be the right place for it. It doesn't seem to fit in exactly with the other comparse glue, but it also feels strange to have this utils file with only a single function. Maybe this is less relevant if we have more useful functions of this form. Maybe also it belongs in the main Comparse repo (in a more general form, using an arbitrary
bytes_like), rather than here. - I'm not sure if the use of this will be bad for the SMT solver, in particular since it does often require a lambda to define the input predicate
p. My sense is that as long as we don't want to talk about equivalence of these predicates that shouldn't be too big of a problem, but I am far from an expert on the encoding used.
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