[MRSolver] Improved heterogenous interface, bug fixes for SHA512 example

[m-yac]

I don't recommend reviewing this PR all together, since it is really the sum of a number of independent changes (sorry about that!). Each commit should be self-contained and have an accurate description, the main changes being:

• 3c77374 introduce equality arguments as assumptions
• 7de0965 add MRVarCtx to avoid ambiguity about var ctx orderings (already reviewed by @eddywestbrook, with comments addressed in 997b050 address comments about MRVarCtx)
• f496f69 replace matchHet with findInjConvs (which had a few bugs, addressed in 37565f9 fix bugs in new InjConversion interface)

and the only other non-trivial changes being:

• 26d7690 fail more gracefully when natSize is undefined, improve panic traces
• 7d52a80 add genCryM/atCryM and tweak Prims to get split normalizing

[eddywestbrook]

You're right, this is a bit much to review all at once, but as you said I have reviewed the major pieces of this with you as you wrote them, so I'm pretty confident about these changes. Plus, MR Solver still passes all of our CI tests, which is also a good sign.