[move-prover][prover-lab] Create a z3 vs cvc5 basic experiment, nuke Rust-Jupyter-Book dependency

[wrwg]

This PR enables to compare cvc5 with z3 in benchmarks over the whole Diem framework. This is achieved in 3 steps:

1. We remove all dependency from Jupyter Rust notebooks. These turned out to not reliably work. (It was in fact broken at head, but also before fragile and extremely slow.) Instead we provide a new prover-lab command plot which generates a .svg file (based on the same refactored plotting logic) which can be included in MD.

2. A new lab is created under lab/data/cvc. This lab is intended to benchmark cvc5 vs z3 (later also include vector theories). The output of this lab is found in this README markdown.

3. It turned out that some of the benchmarks lead cvc to not terminate and respect soft timeouts. To innoculate the in-process benchmark infra against such situations, we support now a 'hard timeout' option in the boogie backend. Only with this addition we can now run cvc against the full Diem framework benchmark suite. If cvc does not terminate, we mark the benchmark as error instead of
   aborting the benchmark run.

The older labs aren't yet updated to this new approach, which should be done in subsequent PRs.

Motivation

Fix bench-marking infrastructure.

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

NA

Related PRs

NA

[wrwg]

During review, the correct link to the README for the cvc lab, which includes the rendered SVG, is this: https://github.com/wrwg/diem/blob/bench/language/move-prover/lab/data/cvc/README.md

[ma2bd]

nice!

[ma2bd]

Here, structopt would make it easy for plot_svg to take a clean configuration structure (instead of a vector of unparsed arguments). Thanks to the "flatten" option of structopt, the configuration struct can even be equipped with its own reusable command-line parsing logic:
https://github.com/facebookincubator/smt2utils/blob/master/z3tracer/src/main.rs#L18
https://github.com/facebookincubator/smt2utils/blob/master/z3tracer/src/model.rs#L23
(^^ there is only one caveat due to a minor bug in cargo doc)

[wrwg]

Yeah, I'm still using clap, as structopt wasn't ready when I started doing this. Should switch this and other code to it in the future.

[wrwg]

/land

[github-actions]

Cluster Test Result

Test runner setup time spent 242 secs
Compatibility test results for land_6ba7b291 ==> land_b48c6336 (PR)
1. All instances running land_6ba7b291, generating some traffic on network
2. First full node land_6ba7b291 ==> land_b48c6336, to validate new full node to old validator node traffic
3. First Validator node land_6ba7b291 ==> land_b48c6336, to validate storage compatibility
4. First batch validators (14) land_6ba7b291 ==> land_b48c6336, to test consensus and traffic between old full nodes and new validator node
5. First batch full nodes (14) land_6ba7b291 ==> land_b48c6336
6. Second batch validators (15) land_6ba7b291 ==> land_b48c6336, to upgrade rest of the validators
7. Second batch of full nodes (15) land_6ba7b291 ==> land_b48c6336, to finish the network upgrade, time spent 712 secs
all up : 1033 TPS, 4394 ms latency, 4950 ms p99 latency, no expired txns, time spent 250 secs
Logs: http://kibana.ct-1-k8s-testnet.aws.hlw3truzy4ls.com/app/kibana#/discover?_g=(time:(from:'2021-07-13T21:17:31Z',to:'2021-07-13T21:40:24Z'))
Dashboard: http://grafana.ct-1-k8s-testnet.aws.hlw3truzy4ls.com/d/performance/performance?from=1626211051000&to=1626212424000
Validator 1 logs: http://kibana.ct-1-k8s-testnet.aws.hlw3truzy4ls.com/app/kibana#/discover?_g=(time:(from:'2021-07-13T21:17:31Z',to:'2021-07-13T21:40:24Z'))&_a=(columns:!(log),query:(language:kuery,query:'kubernetes.pod_name:"val-1"'),sort:!(!('@timestamp',desc)))

Repro cmd:

./scripts/cti --tag land_6ba7b291 --cluster-test-tag land_b48c6336 -E BATCH_SIZE=15 -E UPDATE_TO_TAG=land_b48c6336 --report report.json --suite land_blocking_compat

🎉 Land-blocking cluster test passed! 👌