Add bitvector fallbacks to more nat ops in the simulator

[m-yac]

Currently, the primitives for subNat, equalNat, and ltNat convert their arguments to bitvectors and perform the corresponding bitvector operation if their arguments are not both concrete Naturals.

This PR adds similar bitvector fallbacks to all the remaining natural number operations except expNat (because there is no corresponding bitvector exp function at the moment) and natCase. To do this we generalize the behavior of subNat, equalNat, and ltNat into the functions binNatOp and binNatToNatOp.

Fixes #1558

[robdockins]

As far as I can tell from just looking at the implementation, this seems like a good improvement.

This is a pretty tricky area of the codebase; if we can find a way to add some tests for these behaviors, that would be great.

[m-yac]

Good idea! Looks like we haven't actually been running the saw-core test suite in the CI since we mirated the repo (yikes!), so I got that typechecking again, added it to the CI, and added two tests for each of the primitives I changed. I actually found a bug in my implementation of succOp while making the tests, so I'm very glad you made the suggestion!

@robdockins Let me know if this looks good now or if you think more tests are needed. I didn't cover every case for each operator, but since they're all implemented using unaryNatOp/binNatOp, the tests all together should have good coverage.

[RyanGlScott]

Thanks for fixing the saw-core test suite, @m-yac! Make sure to put "fixes #1558" in the commit message so that we can finally close that one :)