Function fiat_crypto::poly1305_32::fiat_poly1305_from_bytes

source ·

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

Expand description

The function fiat_poly1305_from_bytes deserializes a field element from bytes in little-endian order.

Postconditions: eval out1 mod m = bytes_eval arg1 mod m

Input Bounds: arg1: [[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]]