Implement self-contained test

[brianhuffman]

The cryptol-verifier package needs to have some self-contained tests that can be run independently from saw-script. They should include:

• Load, parse, and typecheck Cryptol.sawcore
• Translate several bits of Cryptol syntax to saw-core and typecheck the resulting terms

[robdockins]

The first part of this was implemented in 1c57ba7

[brianhuffman]

Furthermore we need to make sure that the github CI requires these tests to pass for all cryptol-verifier PRs.

[brianhuffman]

I extended the test program to load, translate, and typecheck the Cryptol prelude (Cryptol.cry), and I discovered the following type error:

Loaded Cryptol.sawcore!
Translated Cryptol.cry!
Type error when checking "sborrow"
Inferred type
  Cryptol.Num
Not a subtype of expected type
  Prelude.Nat
For term
  n

cryptol-verifier-tc-test: user error (internal type error)

[robdockins]

Whoops. Looks like proveProp directly applies the PSignedCmpWord instance, whereas it needs a shim instance similar to PCmpSeqBool

[brianhuffman]

#30 has a fix for this now, using a new function PCmpSeqBool.

[brianhuffman]

Other tests I think we need before we can close this ticket:

• In addition to Cryptol.cry we also need to load and type check the other built-in cryptol modules that contain declarations of primitives (Array.cry and Float.cry)
• We need to translate and check cryptol definitions to test all of Cryptol's implicit instance rules and subclass relationships. (Actually, such a test file should be added to the cryptol test suite; then we should use it again here.)

[robdockins]

To the second point, is this might be what you want:
https://github.com/GaloisInc/cryptol/blob/master/tests/regression/superclass.cry

[brianhuffman]

Yes, that looks perfect for testing superclass relationships. I should add a similar file with a definition for each class instance rule as well.

[brianhuffman]

Implemented in #30.