FeToBytes function
FeToBytes marshals h to s. Preconditions: |h| bounded by 1.12^25,1.12^24,1.12^25,1.12^24,etc.
Write p=2^255-19; q=floor(h/p). Basic claim: q = floor(2^(-255)(h + 19 2^(-25)h9 + 2^(-1))).
Proof: Have |h|<=p so |q|<=1 so |19^2 2^(-255) q|<1/4. Also have |h-2^230 h9|<2^230 so |19 2^(-255)(h-2^230 h9)|<1/4.
Write y=2^(-1)-19^2 2^(-255)q-19 2^(-255)(h-2^230 h9). Then 0<y<1.
Write r=h-pq. Have 0<=r<=p-1=2^255-20. Thus 0<=r+19(2^-255)r<r+19(2^-255)2^255<=2^255-1.
Write x=r+19(2^-255)r+y. Then 0<x<2^255 so floor(2^(-255)x) = 0 so floor(q+2^(-255)x) = q.
Have q+2^(-255)x = 2^(-255)(h + 19 2^(-25) h9 + 2^(-1)) so floor(2^(-255)(h + 19 2^(-25) h9 + 2^(-1))) = q.
Implementation
void FeToBytes(Uint8List s, FieldElement h) {
var carry = List<int>.filled(10, 0);
var q = (19 * h[9] + (1 << 24)) >> 25;
q = (h[0] + q) >> 26;
q = (h[1] + q) >> 25;
q = (h[2] + q) >> 26;
q = (h[3] + q) >> 25;
q = (h[4] + q) >> 26;
q = (h[5] + q) >> 25;
q = (h[6] + q) >> 26;
q = (h[7] + q) >> 25;
q = (h[8] + q) >> 26;
q = (h[9] + q) >> 25;
// Goal: Output h-(2^255-19)q, which is between 0 and 2^255-20.
h[0] += 19 * q;
// Goal: Output h-2^255 q, which is between 0 and 2^255-20.
carry[0] = h[0] >> 26;
h[1] += carry[0];
h[0] -= carry[0] << 26;
carry[1] = h[1] >> 25;
h[2] += carry[1];
h[1] -= carry[1] << 25;
carry[2] = h[2] >> 26;
h[3] += carry[2];
h[2] -= carry[2] << 26;
carry[3] = h[3] >> 25;
h[4] += carry[3];
h[3] -= carry[3] << 25;
carry[4] = h[4] >> 26;
h[5] += carry[4];
h[4] -= carry[4] << 26;
carry[5] = h[5] >> 25;
h[6] += carry[5];
h[5] -= carry[5] << 25;
carry[6] = h[6] >> 26;
h[7] += carry[6];
h[6] -= carry[6] << 26;
carry[7] = h[7] >> 25;
h[8] += carry[7];
h[7] -= carry[7] << 25;
carry[8] = h[8] >> 26;
h[9] += carry[8];
h[8] -= carry[8] << 26;
carry[9] = h[9] >> 25;
h[9] -= carry[9] << 25;
// h10 = carry9
// Goal: Output h[0]+...+2^255 h10-2^255 q, which is between 0 and 2^255-20.
// Have h[0]+...+2^230 h[9] between 0 and 2^255-1;
// evidently 2^255 h10-2^255 q = 0.
// Goal: Output h[0]+...+2^230 h[9].
s[0] = h[0] >> 0;
s[1] = h[0] >> 8;
s[2] = h[0] >> 16;
s[3] = (h[0] >> 24) | (h[1] << 2);
s[4] = h[1] >> 6;
s[5] = h[1] >> 14;
s[6] = (h[1] >> 22) | (h[2] << 3);
s[7] = h[2] >> 5;
s[8] = h[2] >> 13;
s[9] = (h[2] >> 21) | (h[3] << 5);
s[10] = h[3] >> 3;
s[11] = h[3] >> 11;
s[12] = (h[3] >> 19) | (h[4] << 6);
s[13] = h[4] >> 2;
s[14] = h[4] >> 10;
s[15] = h[4] >> 18;
s[16] = h[5] >> 0;
s[17] = h[5] >> 8;
s[18] = h[5] >> 16;
s[19] = (h[5] >> 24) | (h[6] << 1);
s[20] = h[6] >> 7;
s[21] = h[6] >> 15;
s[22] = (h[6] >> 23) | (h[7] << 3);
s[23] = h[7] >> 5;
s[24] = h[7] >> 13;
s[25] = (h[7] >> 21) | (h[8] << 4);
s[26] = h[8] >> 4;
s[27] = h[8] >> 12;
s[28] = (h[8] >> 20) | (h[9] << 6);
s[29] = h[9] >> 2;
s[30] = h[9] >> 10;
s[31] = h[9] >> 18;
}