Support for W4 solvers

[weaversa]

We're trying to use cryptol-remote-api's safe command with a w4-based prover (such as W4_Z3) to prove some safety properties about functions containing unimplemented primitives (for example, in the SuiteB) module. Unfortunately, Python is complaining about an 'invalid param' when we try to pass one of the w4-based provers.

for example:

...
result = c.safe(expr=<any cryptol function>, solver=cryptol.solver.W4_Z3).result()
...

[pnwamk]

The initial implementation of the SMT solver-related server functionality focused on just the SBV backends.

Work to extend support to include all backends is being done here: https://github.com/galoisinc/cryptol/tree/rpc/w4-solvers

[pnwamk]

The server should now be able to handle both the SBV and What4 based solver backends: GaloisInc/cryptol#1224