Use a single persistent solver connection for typechecking cryptol

[brianhuffman]

For testing purposes I recently tried running examples/ecdsa/ecdsa-crucible.saw using crucible_jvm_unsafe_assume_spec instead of crucible_jvm_verify throughout. I expected everything to run really fast, but it was not nearly as fast as I had hoped to see. Some specs took well over a second to process:

[14:43:20.749] Skipping verification of ec_twin_mul_init
[14:43:21.593] Time: 0.843762s

[14:43:21.594] Skipping verification of ec_twin_mul
[14:43:22.231] Time: 0.637015s

[14:43:22.235] Skipping verification of signHash
[14:43:23.920] Time: 1.685543s

[14:43:23.924] Skipping verification of verifySignature
[14:43:25.364] Time: 1.440212s

I was surprised to see these specs take so long because crucible_jvm_unsafe_assume_spec doesn't really do much, other than check to see that everything in the spec is type-correct and otherwise well-formed.

Using unsafe_assume_spec, the entire file takes a bit over 15 seconds to run. (For comparison, the file takes about 4:30 or so with all the symbolic simulation and proofs turned on.)

Profiling shows that crucible_jvm_unsafe_assume_spec takes up about half of the total runtime. Of that, practically all of it is taken up by running parseTypedTerm on the embedded cryptol syntax {{ }}. parseTypedTerm appears to be called several hundred times in total.

We should see what we can do to reduce the cost of running parseTypedTerm lots of times.

[brianhuffman]

The profiling output shows that within parseTypedTerm, the function loadTcPrelude takes up a fifth of the runtime and 2/3 of the memory allocation. We could probably speed this up a lot with some pre-processing, because currently it seems to be taking the raw String contents of CryptolTC.z3, stripping comments, parsing S-expressions, and then prettyprinting SMT output over and over.

[brianhuffman]

Instead of making the processing of CryptolTC.z3 faster, a much more promising solution would be to just process CryptolTC.z3 and send it to the solver once. Apparently the Cryptol library interface will need to be modified to support this (see GaloisInc/cryptol#996).

[brianhuffman]

PR GaloisInc/saw-core#197 adapts cryptol-saw-core to work with GaloisInc/cryptol#1128, which adds support for maintaining a single persistent connection to z3 for typechecking purposes instead of opening a separate connection each time a term is typechecked. As suggested in the comment thread for #197, we could take advantage of this by storing the solver instance inside the CryptolEnv.