fp

package
v0.9.0-beta.0 Latest Latest
Warning

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

 Go to latest Published: Dec 18, 2023 License: GPL-3.0 Imports: 4 Imported by: 0

Documentation

Overview

Code generated by Fiat Cryptography. DO NOT EDIT.

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 p256 ” 64 '2^256 - 2^224 + 2^192 + 2^96 - 1' mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one

curve description (via package name): p256

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 = 0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff (from "2^256 - 2^224 + 2^192 + 2^96 - 1")

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

func P256FpNew() *native.Field

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.