The function toBytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
Preconditions: 0 ≤ eval arg1 < m Postconditions: out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..47]
Input Bounds: arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] Output Bounds: out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
pub fn toBytes(out1: *[48]u8, arg1: [6]u64) voidpub fn toBytes(out1: *[48]u8, arg1: [6]u64) void {
@setRuntimeSafety(mode == .debug);
const x1 = (arg1[5]);
const x2 = (arg1[4]);
const x3 = (arg1[3]);
const x4 = (arg1[2]);
const x5 = (arg1[1]);
const x6 = (arg1[0]);
const x7 = @as(u8, @truncate((x6 & 0xff)));
const x8 = (x6 >> 8);
const x9 = @as(u8, @truncate((x8 & 0xff)));
const x10 = (x8 >> 8);
const x11 = @as(u8, @truncate((x10 & 0xff)));
const x12 = (x10 >> 8);
const x13 = @as(u8, @truncate((x12 & 0xff)));
const x14 = (x12 >> 8);
const x15 = @as(u8, @truncate((x14 & 0xff)));
const x16 = (x14 >> 8);
const x17 = @as(u8, @truncate((x16 & 0xff)));
const x18 = (x16 >> 8);
const x19 = @as(u8, @truncate((x18 & 0xff)));
const x20 = @as(u8, @truncate((x18 >> 8)));
const x21 = @as(u8, @truncate((x5 & 0xff)));
const x22 = (x5 >> 8);
const x23 = @as(u8, @truncate((x22 & 0xff)));
const x24 = (x22 >> 8);
const x25 = @as(u8, @truncate((x24 & 0xff)));
const x26 = (x24 >> 8);
const x27 = @as(u8, @truncate((x26 & 0xff)));
const x28 = (x26 >> 8);
const x29 = @as(u8, @truncate((x28 & 0xff)));
const x30 = (x28 >> 8);
const x31 = @as(u8, @truncate((x30 & 0xff)));
const x32 = (x30 >> 8);
const x33 = @as(u8, @truncate((x32 & 0xff)));
const x34 = @as(u8, @truncate((x32 >> 8)));
const x35 = @as(u8, @truncate((x4 & 0xff)));
const x36 = (x4 >> 8);
const x37 = @as(u8, @truncate((x36 & 0xff)));
const x38 = (x36 >> 8);
const x39 = @as(u8, @truncate((x38 & 0xff)));
const x40 = (x38 >> 8);
const x41 = @as(u8, @truncate((x40 & 0xff)));
const x42 = (x40 >> 8);
const x43 = @as(u8, @truncate((x42 & 0xff)));
const x44 = (x42 >> 8);
const x45 = @as(u8, @truncate((x44 & 0xff)));
const x46 = (x44 >> 8);
const x47 = @as(u8, @truncate((x46 & 0xff)));
const x48 = @as(u8, @truncate((x46 >> 8)));
const x49 = @as(u8, @truncate((x3 & 0xff)));
const x50 = (x3 >> 8);
const x51 = @as(u8, @truncate((x50 & 0xff)));
const x52 = (x50 >> 8);
const x53 = @as(u8, @truncate((x52 & 0xff)));
const x54 = (x52 >> 8);
const x55 = @as(u8, @truncate((x54 & 0xff)));
const x56 = (x54 >> 8);
const x57 = @as(u8, @truncate((x56 & 0xff)));
const x58 = (x56 >> 8);
const x59 = @as(u8, @truncate((x58 & 0xff)));
const x60 = (x58 >> 8);
const x61 = @as(u8, @truncate((x60 & 0xff)));
const x62 = @as(u8, @truncate((x60 >> 8)));
const x63 = @as(u8, @truncate((x2 & 0xff)));
const x64 = (x2 >> 8);
const x65 = @as(u8, @truncate((x64 & 0xff)));
const x66 = (x64 >> 8);
const x67 = @as(u8, @truncate((x66 & 0xff)));
const x68 = (x66 >> 8);
const x69 = @as(u8, @truncate((x68 & 0xff)));
const x70 = (x68 >> 8);
const x71 = @as(u8, @truncate((x70 & 0xff)));
const x72 = (x70 >> 8);
const x73 = @as(u8, @truncate((x72 & 0xff)));
const x74 = (x72 >> 8);
const x75 = @as(u8, @truncate((x74 & 0xff)));
const x76 = @as(u8, @truncate((x74 >> 8)));
const x77 = @as(u8, @truncate((x1 & 0xff)));
const x78 = (x1 >> 8);
const x79 = @as(u8, @truncate((x78 & 0xff)));
const x80 = (x78 >> 8);
const x81 = @as(u8, @truncate((x80 & 0xff)));
const x82 = (x80 >> 8);
const x83 = @as(u8, @truncate((x82 & 0xff)));
const x84 = (x82 >> 8);
const x85 = @as(u8, @truncate((x84 & 0xff)));
const x86 = (x84 >> 8);
const x87 = @as(u8, @truncate((x86 & 0xff)));
const x88 = (x86 >> 8);
const x89 = @as(u8, @truncate((x88 & 0xff)));
const x90 = @as(u8, @truncate((x88 >> 8)));
out1[0] = x7;
out1[1] = x9;
out1[2] = x11;
out1[3] = x13;
out1[4] = x15;
out1[5] = x17;
out1[6] = x19;
out1[7] = x20;
out1[8] = x21;
out1[9] = x23;
out1[10] = x25;
out1[11] = x27;
out1[12] = x29;
out1[13] = x31;
out1[14] = x33;
out1[15] = x34;
out1[16] = x35;
out1[17] = x37;
out1[18] = x39;
out1[19] = x41;
out1[20] = x43;
out1[21] = x45;
out1[22] = x47;
out1[23] = x48;
out1[24] = x49;
out1[25] = x51;
out1[26] = x53;
out1[27] = x55;
out1[28] = x57;
out1[29] = x59;
out1[30] = x61;
out1[31] = x62;
out1[32] = x63;
out1[33] = x65;
out1[34] = x67;
out1[35] = x69;
out1[36] = x71;
out1[37] = x73;
out1[38] = x75;
out1[39] = x76;
out1[40] = x77;
out1[41] = x79;
out1[42] = x81;
out1[43] = x83;
out1[44] = x85;
out1[45] = x87;
out1[46] = x89;
out1[47] = x90;
}