Debug printing

This is a guideline on how to print to stdout/stderr for debugging in miTLS.

Turns out, even (especially!) when proving your code, you still need to print what the function is up to to debug it. The current practice is to use IO.debug_print_string: string -> Tot bool for this. But please be kind to apps or libraries that are linking to the mitls.$OBJ library: they are not expecting your prints to be filling up their stdout/stderr!

To avoid this, please guard your calls to IO.debug_print_string with a per-module flag whose default value is false. See src/tls/KeySchedule.fst's ks_debug flag, for instance.

Which function should I use for printing debug information?

We said above that "current practice is to use IO.debug_print_string". This works for now, but this function is unsound (does IO but pretends to be pure). It would be better to have a function in ST.