Skip to content

Commit baaa75d

Browse files
committed
Improve send and receive request proofs
1 parent 00217a4 commit baaa75d

File tree

2 files changed

+220
-371
lines changed

2 files changed

+220
-371
lines changed

src/lib/communication/DY.Lib.Communication.Printing.fst

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -112,6 +112,12 @@ let com_core_event_to_string #a payload_to_string =
112112
sender receiver (payload_to_string payload))
113113
)))
114114

115+
val sender_authentication_to_string: sender_authentication -> string
116+
let sender_authentication_to_string sa =
117+
match sa with
118+
| Authenticated -> "Authenticated"
119+
| Unauthenticated -> "Unauthenticated"
120+
115121
val com_reqres_event_to_string:
116122
#a:Type0 -> {|comm_layer_reqres_config a|} ->
117123
(a -> string) ->
@@ -121,8 +127,8 @@ let com_reqres_event_to_string #a payload_to_string =
121127
let? cre = parse (communication_reqres_event a) b in
122128
match cre with
123129
| CommClientSendRequest authenticated client server request key -> (
124-
Some (Printf.sprintf "CommClientSendRequest authenticated = %b, client = %s, server = %s, request = (%s)"
125-
authenticated client server (payload_to_string request))
130+
Some (Printf.sprintf "CommClientSendRequest authenticated = %s, client = %s, server = %s, request = (%s)"
131+
(sender_authentication_to_string authenticated) client server (payload_to_string request))
126132
)
127133
| CommServerReceiveRequest client server request key -> (
128134
Some (Printf.sprintf "CommServerReceiveRequest client = %s, server = %s, request = (%s), key = %s"
@@ -132,9 +138,9 @@ let com_reqres_event_to_string #a payload_to_string =
132138
Some (Printf.sprintf "CommServerSendResponse client = %s, server = %s, request = %s, response = (%s), key = %s"
133139
(option_to_string (fun s -> s) client) server (payload_to_string request) (payload_to_string response) (bytes_to_string key))
134140
)
135-
| CommClientReceiveResponse authenticated client server request response key -> (
136-
Some (Printf.sprintf "CommClientReceiveResponse authenticated = %b, client = %s, server = %s, response = (%s), key = %s"
137-
authenticated client server (payload_to_string response) (bytes_to_string key))
141+
| CommClientReceiveResponse client response req_meta_data -> (
142+
Some (Printf.sprintf "CommClientReceiveResponse client = %s, response = (%s), req_meta_data"
143+
client (payload_to_string response))
138144
)
139145
)))
140146

0 commit comments

Comments
 (0)