FeToBytes function Null safety

void FeToBytes(
  1. Uint8List s,
  2. FieldElement h
)

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;
}