fq

package
v0.0.0-...-62736aa Latest Latest
Warning

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

Go to latest
Published: Feb 3, 2023 License: Apache-2.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 fq ” 64 '2^256 - 2^224 + 2^192 - 89188191075325690597107910205041859247' mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one

curve description (via package name): fq

machine_wordsize = 64 (from "64")

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

m = 0xffffffff00000000ffffffffffffffffbce6faada7179e84f3b9cac2fc632551 (from "2^256 - 2^224 + 2^192 - 89188191075325690597107910205041859247")

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

func P256FqNew() *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

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