fp

package
v0.0.0-...-35ce414 Latest Latest
Warning

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

Go to latest
Published: Apr 28, 2023 License: Apache-2.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

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

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

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

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

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

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

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]]

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL