Improve crucible_jvm_verify performance

[atomb]

Ensure that the entire ECDSA proof can complete successfully, and in less than 2x the time taken by java_verify.

[brianhuffman]

Currently the crucible ECDSA proof is about 15x slower than the java_verify version, so we have a lot of work to do. It appears that there are slowdowns in both simulation and proving.

[brianhuffman]

Even when using crucible_jvm_unsafe_assume_spec to skip every subproof, the script takes more than 30 seconds to run; some subproofs take up to 1.5 seconds. (To be clear, this only involves processing the setup block; it does no symbolic simulation or proof.)

I believe the slowdown is due to calling the Cryptol parser and type checker so many times to process terms in Cryptol quotes {{ }}. This is due to the fact that we don't yet have any points_to command that can do a whole array at once, so we have to do things (rather expensively, it turns out) like this:

let jvm_array24_is ref x =
  do {
    for [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23]
      (\i -> jvm_elem_is ref i (jvm_term {{ x@(`i:[8]) }}));
    return ();
  };

I wonder if there might be some computation that is repeated for every set of cryptol quotes, which we might be able to cache and re-use.

[atomb]

We've made a bunch of improvements which should be sufficient for 0.3. I'm going to leave this open to track further improvements, though.

[brianhuffman]

In a branch, the ecdsa-crucible.saw runtime is down to about 5 minutes, compared to 3 for ecdsa.saw. So we are already within the 2x performance target. I'll close this ticket once the relevant changes are merged to master.

[brianhuffman]

As of #932, ecdsa-crucible.saw is part of the regression test suite, and runs suitably fast.