Fixed assumption in 2^255-19 carry propagation

Fixed assumption in 2^255-19 carry propagation

Careful re-examination of the carry propagation code revealed that
SUPERCOP's invariants for fe_tobytes() were not respected: there is a
possibility that the inputs slightly outrange the set of input for which
SUPERCOP's original proof was intended.

This happens in invsqrt(), used for EdDSA verification And Elligator,
and the reverse map of Elligator.  X25519 is unaffected.

Note that we were unable to produce a set of input that actually
triggers this range overflow.  Moreover, careful mathematical analysis
(and tests with SAGE) showed that fe_tobytes() is actually much more
tolerant than SUPERCOP's proof let on.  As far as I can tell, this
slight overflow cannot trigger any observable bug.

Still, I figured it would be a good idea to abide those invariants
anyway, if only to facilitate future audits.  To this end, I made sure
the inputs of fe_tobytes() came directly from either multiplications
(which perform a carry propagation), or constants (where carry
propagation has been pre-computed).