Function fiat_crypto::poly1305_32::fiat_poly1305_to_bytes

source ·

pub fn fiat_poly1305_to_bytes(
    out1: &mut [u8; 17],
    arg1: &fiat_poly1305_tight_field_element
)

Expand description

The function fiat_poly1305_to_bytes serializes a field element to bytes in little-endian order.

Postconditions: out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..16]

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 ~> 0x3]]