Expand description

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

Computed values: carry_chain = [0, 1, 2, 3, 4, 0, 1] eval z = z[0] + (z[1] << 26) + (z[2] << 52) + (z[3] << 78) + (z[4] << 104) 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 = [0x7fffff6, 0x7fffffe, 0x7fffffe, 0x7fffffe, 0x7fffffe]

Functions

Type Definitions