Emit JSON simplification logs with -l SimplifyJson

[geo2a]

Summary of changes

This PR enables the -l SimplifyJson log option in kore-rpc-booster and booster-dev. This option enables structured (as JSON) logging of equation application/failures to apply an equation.

These feature is a reincarnation of the log-*-simplifications request parameter. It has become evident that bundling the logs into the response is a bad idea, as they tend to be very heavy-weight. In this iteration, we change two things:

• logs do not contains the states anymore, but only the rule unique IDs and the failure reason (if failed)
• logs are written to a file, rather then collected in-memory and returned in the response

Log format

the logs follow the format of the Simplification constructor of the LogEntry datatype from kore-rpc-types. This allows us to shovel both Booster's and Kore's equation application data into the same format that. Here are three examples of a log entries:

Failure in Booster: {"tag":"simplification","result":{"tag":"failure","reason":"RuleNotPreservingDefinedness","rule-id":"d0c635862a74b433473f8d45be9da2608b68fbdcf820aff3a421795196e6070b"},"origin":"booster"}
Success in Booster: [SimplifyJson] {"tag":"simplification","result":{"tag":"success","rule-id":"f310443b160236f56d095576a7500c11d1e98ee7af349b0bbf7a34b5e444d300"},"origin":"booster"}
Success in Kore: {"tag":"simplification","result":{"tag":"success","rule-id":"24f1c49206508c64e029253c37c243d97ca8b3aaea2e4d938380c89870b81955"},"origin":"kore-rpc"}

Note: we do not have a way to get the failures from Kore at that point.

Output to file or stderr

Both kore-rpc-booster and booster-dev now support a new CLI option, --log-file FILENAME. This option only has effect of -l SimplifyJson is supplied too. If both are present, the simplification logs will be written to FILENAME, otherwise they will end-up in stderr.

Note: when written to stderr, the logs are prefixed with [SimplifyJson] to distinguish them from log entries of other types. When writing to a file, this prefix is skipped.

Analysis of logs

These logs are intended for machine, rather direct human consumption. I'm working on a Python tool on top of pyk that would allow transforming these logs into a table. Something along the lines of:

|    9642 | simplification | kore-rpc | success  | BYTES-SIMPLIFICATION.bytes-concat-right-assoc-symb-l    | evm-semantics/lemmas/bytes-simplification.k:(33, 45, 33, 115)    |                              |
|    9643 | simplification | kore-rpc | success  | BYTES-SIMPLIFICATION.bytes-concat-empty-right           | evm-semantics/lemmas/bytes-simplification.k:(30, 38, 30, 65)     |                              |
|    9644 | simplification | booster  | success  |                                                         | None                                                             |                              |
|    9645 | simplification | booster  | success  |                                                         | None                                                             |                              |
|    9647 | simplification | booster  | success  |                                                         | None                                                             |                              |
|    9648 | simplification | booster  | success  | EVM.isPrecompiledAccount                                | kproj/evm-semantics/evm.md:(1340, 35, 1340, 145)                 |                              |
|    9705 | simplification | booster  | success  |                                                         | None                                                             |                              |
|   10074 | simplification | booster  | success  | EVM.isPrecompiledAccount                                | kproj/evm-semantics/evm.md:(1340, 35, 1340, 145)                 |                              |
|   10131 | simplification | booster  | success  |                                                         | None                                                             |                              |
|   10762 | simplification | kore-rpc | success  | UNKNOWN                                                 | kframework/builtin/domains.md:(1161, 8, 1161, 84)                |                              |
|   10763 | simplification | kore-rpc | success  | UNKNOWN                                                 | kframework/builtin/domains.md:(1156, 8, 1156, 55)                |                              |

the above entries as are an exert from a table produced from logs of a Kontrol proof. For proof-wide tables to be more useful, we may want to add request IDs.

[jberthold]

LGTM

[jberthold]

Maybe not a bad idea to optionally log to a file... (but we can use a redirect, the server does not have any important output).
At the moment, this option only affects the SimplifyJSON log level, so it should maybe have a more specific name:

Suggested change

	<*> optional
	( strOption
	( metavar "LOG_FILE"
	<> long "log-file"
	<> help
	"Log file to write the logs to"
	)
	)
	<*> optional
	( strOption
	( metavar "JSON_LOG_FILE"
	<> long "simplification-log-file"
	<> help
	"Log file for the JSON simplification logs"
	)
	)

IDK if it is possible to automatically imply -l SimplifyJSON when this option is present (absolutely not required in this PR!)

[geo2a]

I've renamed --log-file to --simplification-log-file.