Input processing performed by defmax-nat.
Currently this validates the inputs lightly. It should be improved to do a more thorough validation.