Fix test0001 so that it actually verifies the Java MD5 implementation

[brianhuffman]

The integration test test0001 currently uses the old-style java verification commands to specify a Java MD5 implementation that we have. However, it currently omits a java_verify_tactic declaration, which means the proof is skipped (only symbolic simulation is performed). Adding the missing java_verify_tactic declaration causes the verification to fail, as symbolic simulation produces proof obligations of the form False.

The old java verification commands have been deprecated for some time, and are slated for removal (#1005). However, we would like to once again have a regression test that verifies the same Java MD5 implementation.

We need to complete a verification of the Java MD5 implementation using the new-style JVM verification commands, and replace the current non-proof in test0001 with the new proof script.

[brianhuffman]

Here's one data point about how exactly the proof might be broken: When the 16-byte input message to the algorithm is fixed to all 0, the contents of the output of the Java implementation are

[0x4a, 0xe7, 0x13, 0x36, 0xe4, 0x4b, 0xf9, 0xbf, 0x79, 0xd2, 0x75, 0x2e, 0x23, 0x48, 0x18, 0xa5]

But in the cryptol MD5 spec, the result of md5_ref zero is

[0x52, 0xe7, 0xc8, 0x6c, 0x27, 0xd2, 0x9f, 0xfd, 0x9e, 0x4b, 0xae, 0x74, 0xc4, 0x12, 0x18, 0xa5]

Strangely, it appears that they agree on a few entries, but most of them are different. It turns out that each byte is individually reversed.