Module fiat_crypto::secp256k1_dettman_64

Autogenerated: ‘src/ExtractionOCaml/dettman_multiplication’ –lang Rust –inline secp256k1_dettman 64 5 48 2 ‘2^256 - 4294968273’ mul square curve description: secp256k1_dettman machine_wordsize = 64 (from “64”) requested operations: mul, square n = 5 (from “5”) last_limb_width = 48 (from “48”) last_reduction = 2 (from “2”) s-c = 2^256 - [(1, 4294968273)] (from “2^256 - 4294968273”) inbounds_multiplier: None (from “”)

Computed values:

Functions

• fiat_secp256k1_dettman_mul
  The function fiat_secp256k1_dettman_mul multiplies two field elements.
• fiat_secp256k1_dettman_square
  The function fiat_secp256k1_dettman_square squares a field element.