Review all uses of unbounded numbers

[nc6]

We use Natural/Integer in various places in the spec, most likely for consistency with the formal spec. But this is a little annoying for implementation, where we'd like to make assumptions about the maximum size. Consider whether we can replace these with bounded types.