[MRSolver] Changes to Mr. Solver to get zero_array working

[m-yac]

This PR gets an example of exponential explosion (exp_explosion_mr_solver.saw) and a Cryptol refinement proof of zero_array (arrays_mr_solver.saw) working with Mr. Solver.

The main changes needed to get these working were:

• Make refinement heterogeneous, specifically a function with argument type Vec n Bool can now refine a function with corresponding argument type Num (or vice versa) by introducing the former and substituting TCNum of bvToNat n of the former for the latter
• Define seqMapM in terms of multiFixM with a loop invariant (so that Mr. Solver can do co-induction on list comprehensions) and special-case it if its length argument is bvToNat of some bitvector (so that we can easily translate to SMT)
• Add monadification for ecUpdate and tweak the monadification of ecAt to better work with Mr. Solver
• Add a monadification macro for invariantHint to ensure an application of invariantHint remains top-level (i.e. so that invariantHint a cond comp monadifies to invariantHint (CompM a) cond comp and not comp >>= \x -> returnM a (invariantHint a cond x))
• Add a monadification macro for asserting and assuming (for the same reason as the above) and add special cases for them to Mr. Solver (for better error reporting)
• If there is an existing monadification macro for y, calling set_monadification x y will now add the same macro for x. This is needed so that in specPrims.saw, set_monadification "invariantHint" "Prelude.invariantHint" does the macro described above instead of just monadifying it to Prelude.invariantHint and stopping there - the same goes for assuming and asserting. (This could probably also be solved by recursing in monadifyTerm, but this seemed simpler.)
• Make bvNat w (bvToNat w' n) reduce to n in the SAW core simulator

[eddywestbrook]

Looks great, thanks Matt!