Solution (source code)

= 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.