Solution
= Solution
Start with a one-cell, possibly unnormalized representation, then carry:
``
function MakeNum(t: integer): number
require t >= 0
new(result, 1)
result[0] := t
Normal(result)
return result
``
Before normalization its represented value is exactly `t`. <Carry normalization of a digit array> preserves that value and grows storage when needed. Zero returns a valid nonempty representation containing zero. A negative input is outside this nonnegative-number abstraction.