Add >=0 constraints to quot_round_zero and rem_round_zero

[Timmmm]

The type declarations for those division operators are missing >0 and >=0 constraints.

See https://github.com/riscv/sail-riscv/pull/552/files#r1768223964

[Alasdair]

I had a go at doing this. It should be possible, but there are a few places where we will need to add explicit asserts for divisors, even if it looks somewhat obvious:

  if EMUL_pow < 0 then nf / (2 ^ (0 - EMUL_pow)) <= 8

This is never division by zero, but it requires reasoning about non-linear arithmetic to prove it which the SMT solver can't do.

[Timmmm]

Hmm isn't the output of 2 ^ always greater than zero? That does feel obvious...

[Alasdair]

Yes, but in practice the SMT solver just gives up whenever it sees 2 ^ n and n isn't bounded. I have a fallback routine that replaces 2 ^ with an arbitrary function that is equivalent up to 2 ^ 64 so I can check any problem that is unsatisfiable for such a function must be unsatisfiable in general, and I could improve that fallback to handle this case but it doesn't work without an explicit assert right now.

[Alasdair]

That does mean the other solution is to really understand the vector spec and add tight bounds to every variable.