Large proof state gets split into multiple messages, causes JSON parsing errors that prevent dump state display

[klinvill]

I found that dumps failed to display proof states I expect to see in the UI after unfolding large proof states (normalizing with delta). Instead I just saw the dump function signature shown below.

It appears that the root cause of this problem is that a large proof state gets fragmented into multiple messages. When the extension then tries to parse these messages into JSON (at

fstar-vscode-assistant/server/src/server.ts

Line 831 in d454c0d

r = JSON.parse(data);

), the fragments are not valid JSON and the messages are ignored. I'm not sure if this fragmentation is because of something the F* executable does intentionally, or if it just happens to correspond to when output buffers are flushed.

I was able to reproduce this behavior with a large enough proof state. A minimal example is given below (note the many spaces in the strings).

module Test

let _ = assert(
    "Hello world                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      "
        ==
        "Goodbye!                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      "
        ) by (
        let open FStar.Tactics in
        dump "Current state:";
        smt ()
    )

Ideally I'd expect to see full proof states after dumps regardless of the size, but it may be desirable to still cap it to some large size to prevent potential resource starvation attacks or bugs.

[klinvill]

This could be tied to the buffer size OCaml uses when writing to channels: https://discuss.ocaml.org/t/when-does-printf-printf-flush/12057/3. However it seems to cut off at 8192 bytes, which might be a lower limit on the javascript side.

One potential solution would be to just wait for future messages if only a partial JSON message is received, but this may be highly-susceptible to race conditions and might bork up reading other messages. Although maybe it would be simple enough to check if the next received message can be interpreted as a standalone JSON message, and if so treat it as such, if not, try to append it to the stored incomplete JSON prefix and then try to interpret the combined result as a JSON message.

Another potential solution could be to implement/use some kind of reliable transmission protocol, similar to TCP, for sending messages so that fragmented messages can be reliably assembled. But this feels like a heavyweight solution for the (presumably) rare problem I'm running into.