fp

package
v0.10.0 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Jan 27, 2024 License: GPL-3.0 Imports: 4 Imported by: 0

Documentation

Overview

Autogenerated: 'src/ExtractionOCaml/word_by_word_montgomery' --lang Go --no-wide-int --relax-primitive-carry-to-bitwidth 32,64 --cmovznz-by-mul --internal-static --package-case flatcase --public-function-case UpperCamelCase --private-function-case camelCase --public-type-case UpperCamelCase --private-type-case camelCase --no-prefix-fiat --doc-newline-in-typedef-bounds --doc-prepend-header 'Code generated by Fiat Cryptography. DO NOT EDIT.' --doc-text-before-function-name ” --doc-text-before-type-name ” --package-name secp256k1 ” 64 '2^256 - 2^32 - 977' mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp

curve description (via package name): secp256k1

machine_wordsize = 64 (from "64")

requested operations: mul, square, add, sub, opp, from_montgomery, to_montgomery, nonzero, selectznz, to_bytes, from_bytes, one, msat, divstep, divstep_precomp

m = 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f (from "2^256 - 2^32 - 977")

NOTE: In addition to the bounds specified above each function, all 

functions synthesized for this Montgomery arithmetic require the

input to be strictly less than the prime modulus (m), and also

require the input to be in the unique saturated representation.

All functions also ensure that these two properties are true of

return values.

Computed values: 

eval z = z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192)

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) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248)

twos_complement_eval z = let x1 := z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) in

                         if x1 & (2^256-1) < 2^255 then x1 & (2^256-1) else (x1 & (2^256-1)) - 2^256

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func Add 

func Add(out1 *MontgomeryDomainFieldElement, arg1 *MontgomeryDomainFieldElement, arg2 *MontgomeryDomainFieldElement)

Add adds two field elements in the Montgomery domain.

Preconditions: 

0 ≤ eval arg1 < m
0 ≤ eval arg2 < m

Postconditions: 

eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
0 ≤ eval out1 < m

func Divstep 

func Divstep(out1 *uint64, out2 *[5]uint64, out3 *[5]uint64, out4 *[4]uint64, out5 *[4]uint64, arg1 uint64, arg2 *[5]uint64, arg3 *[5]uint64, arg4 *[4]uint64, arg5 *[4]uint64)

Divstep computes a divstep.

Preconditions: 

0 ≤ eval arg4 < m
0 ≤ eval arg5 < m

Postconditions: 

out1 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then 1 - arg1 else 1 + arg1)
twos_complement_eval out2 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then twos_complement_eval arg3 else twos_complement_eval arg2)
twos_complement_eval out3 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then ⌊(twos_complement_eval arg3 - twos_complement_eval arg2) / 2⌋ else ⌊(twos_complement_eval arg3 + (twos_complement_eval arg3 mod 2) * twos_complement_eval arg2) / 2⌋)
eval (from_montgomery out4) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (2 * eval (from_montgomery arg5)) mod m else (2 * eval (from_montgomery arg4)) mod m)
eval (from_montgomery out5) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (eval (from_montgomery arg4) - eval (from_montgomery arg4)) mod m else (eval (from_montgomery arg5) + (twos_complement_eval arg3 mod 2) * eval (from_montgomery arg4)) mod m)
0 ≤ eval out5 < m
0 ≤ eval out5 < m
0 ≤ eval out2 < m
0 ≤ eval out3 < m

Input Bounds: 

arg1: [0x0 ~> 0xffffffffffffffff]
arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
arg4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
arg5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

Output Bounds: 

out1: [0x0 ~> 0xffffffffffffffff]
out2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
out3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
out4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
out5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

func DivstepPrecomp 

func DivstepPrecomp(out1 *[4]uint64)

DivstepPrecomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form).

Postconditions: 

eval (from_montgomery out1) = ⌊(m - 1) / 2⌋^(if ⌊log2 m⌋ + 1 < 46 then ⌊(49 * (⌊log2 m⌋ + 1) + 80) / 17⌋ else ⌊(49 * (⌊log2 m⌋ + 1) + 57) / 17⌋)
0 ≤ eval out1 < m

Output Bounds: 

out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

func FromBytes 

func FromBytes(out1 *[4]uint64, arg1 *[32]uint8)

FromBytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.

Preconditions: 

0 ≤ bytes_eval arg1 < m

Postconditions: 

eval out1 mod m = bytes_eval arg1 mod m
0 ≤ eval out1 < 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 ~> 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]]

Output Bounds: 

out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

func FromMontgomery 

func FromMontgomery(out1 *NonMontgomeryDomainFieldElement, arg1 *MontgomeryDomainFieldElement)

FromMontgomery translates a field element out of the Montgomery domain.

Preconditions: 

0 ≤ eval arg1 < m

Postconditions: 

eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m
0 ≤ eval out1 < m

func K256FpNew 

func K256FpNew() *native.Field

func Msat 

func Msat(out1 *[5]uint64)

Msat returns the saturated representation of the prime modulus.

Postconditions: 

twos_complement_eval out1 = m
0 ≤ eval out1 < m

Output Bounds: 

out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

func Mul 

func Mul(out1 *MontgomeryDomainFieldElement, arg1 *MontgomeryDomainFieldElement, arg2 *MontgomeryDomainFieldElement)

Mul multiplies two field elements in the Montgomery domain.

Preconditions: 

0 ≤ eval arg1 < m
0 ≤ eval arg2 < m

Postconditions: 

eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m
0 ≤ eval out1 < m

func Nonzero 

func Nonzero(out1 *uint64, arg1 *[4]uint64)

Nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.

Preconditions: 

0 ≤ eval arg1 < m

Postconditions: 

out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0

Input Bounds: 

arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

Output Bounds: 

out1: [0x0 ~> 0xffffffffffffffff]

func Opp 

func Opp(out1 *MontgomeryDomainFieldElement, arg1 *MontgomeryDomainFieldElement)

Opp negates a field element in the Montgomery domain.

Preconditions: 

0 ≤ eval arg1 < m

Postconditions: 

eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m
0 ≤ eval out1 < m

func Selectznz 

func Selectznz(out1 *[4]uint64, arg1 uint1, arg2 *[4]uint64, arg3 *[4]uint64)

Selectznz is a multi-limb conditional select.

Postconditions: 

eval out1 = (if arg1 = 0 then eval arg2 else eval arg3)

Input Bounds: 

arg1: [0x0 ~> 0x1]
arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

Output Bounds: 

out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

func SetOne 

func SetOne(out1 *MontgomeryDomainFieldElement)

SetOne returns the field element one in the Montgomery domain.

Postconditions: 

eval (from_montgomery out1) mod m = 1 mod m
0 ≤ eval out1 < m

func Square 

func Square(out1 *MontgomeryDomainFieldElement, arg1 *MontgomeryDomainFieldElement)

Square squares a field element in the Montgomery domain.

Preconditions: 

0 ≤ eval arg1 < m

Postconditions: 

eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
0 ≤ eval out1 < m

func Sub 

func Sub(out1 *MontgomeryDomainFieldElement, arg1 *MontgomeryDomainFieldElement, arg2 *MontgomeryDomainFieldElement)

Sub subtracts two field elements in the Montgomery domain.

Preconditions: 

0 ≤ eval arg1 < m
0 ≤ eval arg2 < m

Postconditions: 

eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
0 ≤ eval out1 < m

func ToBytes 

func ToBytes(out1 *[32]uint8, arg1 *[4]uint64)

ToBytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.

Preconditions: 

0 ≤ eval arg1 < m

Postconditions: 

out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31]

Input Bounds: 

arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

Output Bounds: 

out1: [[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 ~> 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]]

func ToMontgomery 

func ToMontgomery(out1 *MontgomeryDomainFieldElement, arg1 *NonMontgomeryDomainFieldElement)

ToMontgomery translates a field element into the Montgomery domain.

Preconditions: 

0 ≤ eval arg1 < m

Postconditions: 

eval (from_montgomery out1) mod m = eval arg1 mod m
0 ≤ eval out1 < m

Types

type MontgomeryDomainFieldElement 

type MontgomeryDomainFieldElement [4]uint64

MontgomeryDomainFieldElement is a field element in the Montgomery domain.

Bounds: 

[[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

type NonMontgomeryDomainFieldElement 

type NonMontgomeryDomainFieldElement [4]uint64

NonMontgomeryDomainFieldElement is a field element NOT in the Montgomery domain.

Bounds: 

[[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.