Module fiat_crypto::secp256k1_dettman_32

Autogenerated: ‘src/ExtractionOCaml/dettman_multiplication’ –lang Rust –inline secp256k1_dettman 32 10 22 6 ‘2^256 - 4294968273’ mul square curve description: secp256k1_dettman machine_wordsize = 32 (from “32”) requested operations: mul, square n = 10 (from “10”) last_limb_width = 22 (from “22”) last_reduction = 6 (from “6”) 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.