Module poly1305_64

Autogenerated: ‘src/ExtractionOCaml/unsaturated_solinas’ –lang Rust –inline poly1305 64 3 ‘2^130 - 5’ carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax curve description: poly1305 machine_wordsize = 64 (from “64”) requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax n = 3 (from “3”) s-c = 2^130 - [(1, 5)] (from “2^130 - 5”) tight_bounds_multiplier = 1 (from “”)

Computed values: carry_chain = [0, 1, 2, 0, 1] eval z = z[0] + (z[1] << 44) + (z[2] << 87) bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) balance = [0x1ffffffffff6, 0xffffffffffe, 0xffffffffffe]

Structs

fiat_poly1305_loose_field_element

The type fiat_poly1305_loose_field_element is a field element with loose bounds. Bounds: [[0x0 ~> 0x300000000000], [0x0 ~> 0x180000000000], [0x0 ~> 0x180000000000]]

fiat_poly1305_tight_field_element

The type fiat_poly1305_tight_field_element is a field element with tight bounds. Bounds: [[0x0 ~> 0x100000000000], [0x0 ~> 0x80000000000], [0x0 ~> 0x80000000000]]

Functions

fiat_poly1305_add

The function fiat_poly1305_add adds two field elements.

fiat_poly1305_addcarryx_u43

The function fiat_poly1305_addcarryx_u43 is an addition with carry.

fiat_poly1305_addcarryx_u44

The function fiat_poly1305_addcarryx_u44 is an addition with carry.

fiat_poly1305_carry

The function fiat_poly1305_carry reduces a field element.

fiat_poly1305_carry_mul

The function fiat_poly1305_carry_mul multiplies two field elements and reduces the result.

fiat_poly1305_carry_square

The function fiat_poly1305_carry_square squares a field element and reduces the result.

fiat_poly1305_cmovznz_u64

The function fiat_poly1305_cmovznz_u64 is a single-word conditional move.

fiat_poly1305_from_bytes

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

fiat_poly1305_opp

The function fiat_poly1305_opp negates a field element.

fiat_poly1305_relax

The function fiat_poly1305_relax is the identity function converting from tight field elements to loose field elements.

fiat_poly1305_selectznz

The function fiat_poly1305_selectznz is a multi-limb conditional select.

fiat_poly1305_sub

The function fiat_poly1305_sub subtracts two field elements.

fiat_poly1305_subborrowx_u43

The function fiat_poly1305_subborrowx_u43 is a subtraction with borrow.

fiat_poly1305_subborrowx_u44

The function fiat_poly1305_subborrowx_u44 is a subtraction with borrow.

fiat_poly1305_to_bytes

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

Type Aliases

fiat_poly1305_i1

fiat_poly1305_i1 represents values of 1 bits, stored in one byte.

fiat_poly1305_i2

fiat_poly1305_i2 represents values of 2 bits, stored in one byte.

fiat_poly1305_u1

fiat_poly1305_u1 represents values of 1 bits, stored in one byte.

fiat_poly1305_u2

fiat_poly1305_u2 represents values of 2 bits, stored in one byte.