fiat

Imports

Imports #

"crypto/internal/fips140/subtle"
"errors"
"crypto/internal/fips140/subtle"
"errors"
"math/bits"
"crypto/internal/fips140/subtle"
"errors"
"math/bits"
_ "crypto/internal/fips140/check"
"math/bits"
"crypto/internal/fips140/subtle"
"errors"
"math/bits"

Constants & Variables

p224ElementLen const #

const p224ElementLen = 28

p256ElementLen const #

const p256ElementLen = 32

p384ElementLen const #

const p384ElementLen = 48

p521ElementLen const #

const p521ElementLen = 66

Type Aliases

p224Int1 type #

type p224Int1 int64

p224MontgomeryDomainFieldElement type #

The type p224MontgomeryDomainFieldElement is a field element in the Montgomery domain. Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

type p224MontgomeryDomainFieldElement [4]uint64

p224NonMontgomeryDomainFieldElement type #

The type p224NonMontgomeryDomainFieldElement is a field element NOT in the Montgomery domain. Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

type p224NonMontgomeryDomainFieldElement [4]uint64

p224Uint1 type #

type p224Uint1 uint64

p224UntypedFieldElement type #

type p224UntypedFieldElement [4]uint64

p256Int1 type #

type p256Int1 int64

p256MontgomeryDomainFieldElement type #

The type p256MontgomeryDomainFieldElement is a field element in the Montgomery domain. Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

type p256MontgomeryDomainFieldElement [4]uint64

p256NonMontgomeryDomainFieldElement type #

The type p256NonMontgomeryDomainFieldElement is a field element NOT in the Montgomery domain. Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

type p256NonMontgomeryDomainFieldElement [4]uint64

p256Uint1 type #

type p256Uint1 uint64

p256UntypedFieldElement type #

type p256UntypedFieldElement [4]uint64

p384Int1 type #

type p384Int1 int64

p384MontgomeryDomainFieldElement type #

The type p384MontgomeryDomainFieldElement is a field element in the Montgomery domain. Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

type p384MontgomeryDomainFieldElement [6]uint64

p384NonMontgomeryDomainFieldElement type #

The type p384NonMontgomeryDomainFieldElement is a field element NOT in the Montgomery domain. Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

type p384NonMontgomeryDomainFieldElement [6]uint64

p384Uint1 type #

type p384Uint1 uint64

p384UntypedFieldElement type #

type p384UntypedFieldElement [6]uint64

p521Int1 type #

type p521Int1 int64

p521MontgomeryDomainFieldElement type #

The type p521MontgomeryDomainFieldElement is a field element in the Montgomery domain. Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

type p521MontgomeryDomainFieldElement [9]uint64

p521NonMontgomeryDomainFieldElement type #

The type p521NonMontgomeryDomainFieldElement is a field element NOT in the Montgomery domain. Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

type p521NonMontgomeryDomainFieldElement [9]uint64

p521Uint1 type #

type p521Uint1 uint64

p521UntypedFieldElement type #

type p521UntypedFieldElement [9]uint64

Structs

P224Element struct #

P224Element is an integer modulo 2^224 - 2^96 + 1. The zero value is a valid zero element.

type P224Element struct {
x p224MontgomeryDomainFieldElement
}

P256Element struct #

P256Element is an integer modulo 2^256 - 2^224 + 2^192 + 2^96 - 1. The zero value is a valid zero element.

type P256Element struct {
x p256MontgomeryDomainFieldElement
}

P384Element struct #

P384Element is an integer modulo 2^384 - 2^128 - 2^96 + 2^32 - 1. The zero value is a valid zero element.

type P384Element struct {
x p384MontgomeryDomainFieldElement
}

P521Element struct #

P521Element is an integer modulo 2^521 - 1. The zero value is a valid zero element.

type P521Element struct {
x p521MontgomeryDomainFieldElement
}

Functions

Add method #

Add sets e = t1 + t2, and returns e.

func (e *P521Element) Add(t1 *P521Element, t2 *P521Element) *P521Element

Add method #

Add sets e = t1 + t2, and returns e.

func (e *P224Element) Add(t1 *P224Element, t2 *P224Element) *P224Element

Add method #

Add sets e = t1 + t2, and returns e.

func (e *P384Element) Add(t1 *P384Element, t2 *P384Element) *P384Element

Add method #

Add sets e = t1 + t2, and returns e.

func (e *P256Element) Add(t1 *P256Element, t2 *P256Element) *P256Element

Bytes method #

Bytes returns the 66-byte big-endian encoding of e.

func (e *P521Element) Bytes() []byte

Bytes method #

Bytes returns the 28-byte big-endian encoding of e.

func (e *P224Element) Bytes() []byte

Bytes method #

Bytes returns the 32-byte big-endian encoding of e.

func (e *P256Element) Bytes() []byte

Bytes method #

Bytes returns the 48-byte big-endian encoding of e.

func (e *P384Element) Bytes() []byte

Equal method #

Equal returns 1 if e == t, and zero otherwise.

func (e *P384Element) Equal(t *P384Element) int

Equal method #

Equal returns 1 if e == t, and zero otherwise.

func (e *P224Element) Equal(t *P224Element) int

Equal method #

Equal returns 1 if e == t, and zero otherwise.

func (e *P521Element) Equal(t *P521Element) int

Equal method #

Equal returns 1 if e == t, and zero otherwise.

func (e *P256Element) Equal(t *P256Element) int

Invert method #

Invert sets e = 1/x, and returns e. If x == 0, Invert returns e = 0.

func (e *P521Element) Invert(x *P521Element) *P521Element

Invert method #

Invert sets e = 1/x, and returns e. If x == 0, Invert returns e = 0.

func (e *P224Element) Invert(x *P224Element) *P224Element

Invert method #

Invert sets e = 1/x, and returns e. If x == 0, Invert returns e = 0.

func (e *P384Element) Invert(x *P384Element) *P384Element

Invert method #

Invert sets e = 1/x, and returns e. If x == 0, Invert returns e = 0.

func (e *P256Element) Invert(x *P256Element) *P256Element

IsZero method #

IsZero returns 1 if e == 0, and zero otherwise.

func (e *P224Element) IsZero() int

IsZero method #

IsZero returns 1 if e == 0, and zero otherwise.

func (e *P256Element) IsZero() int

IsZero method #

IsZero returns 1 if e == 0, and zero otherwise.

func (e *P384Element) IsZero() int

IsZero method #

IsZero returns 1 if e == 0, and zero otherwise.

func (e *P521Element) IsZero() int

Mul method #

Mul sets e = t1 * t2, and returns e.

func (e *P224Element) Mul(t1 *P224Element, t2 *P224Element) *P224Element

Mul method #

Mul sets e = t1 * t2, and returns e.

func (e *P256Element) Mul(t1 *P256Element, t2 *P256Element) *P256Element

Mul method #

Mul sets e = t1 * t2, and returns e.

func (e *P521Element) Mul(t1 *P521Element, t2 *P521Element) *P521Element

Mul method #

Mul sets e = t1 * t2, and returns e.

func (e *P384Element) Mul(t1 *P384Element, t2 *P384Element) *P384Element

One method #

One sets e = 1, and returns e.

func (e *P224Element) One() *P224Element

One method #

One sets e = 1, and returns e.

func (e *P256Element) One() *P256Element

One method #

One sets e = 1, and returns e.

func (e *P521Element) One() *P521Element

One method #

One sets e = 1, and returns e.

func (e *P384Element) One() *P384Element

Select method #

Select sets v to a if cond == 1, and to b if cond == 0.

func (v *P384Element) Select(a *P384Element, b *P384Element, cond int) *P384Element

Select method #

Select sets v to a if cond == 1, and to b if cond == 0.

func (v *P256Element) Select(a *P256Element, b *P256Element, cond int) *P256Element

Select method #

Select sets v to a if cond == 1, and to b if cond == 0.

func (v *P521Element) Select(a *P521Element, b *P521Element, cond int) *P521Element

Select method #

Select sets v to a if cond == 1, and to b if cond == 0.

func (v *P224Element) Select(a *P224Element, b *P224Element, cond int) *P224Element

Set method #

Set sets e = t, and returns e.

func (e *P256Element) Set(t *P256Element) *P256Element

Set method #

Set sets e = t, and returns e.

func (e *P224Element) Set(t *P224Element) *P224Element

Set method #

Set sets e = t, and returns e.

func (e *P521Element) Set(t *P521Element) *P521Element

Set method #

Set sets e = t, and returns e.

func (e *P384Element) Set(t *P384Element) *P384Element

SetBytes method #

SetBytes sets e = v, where v is a big-endian 28-byte encoding, and returns e. If v is not 28 bytes or it encodes a value higher than 2^224 - 2^96 + 1, SetBytes returns nil and an error, and e is unchanged.

func (e *P224Element) SetBytes(v []byte) (*P224Element, error)

SetBytes method #

SetBytes sets e = v, where v is a big-endian 66-byte encoding, and returns e. If v is not 66 bytes or it encodes a value higher than 2^521 - 1, SetBytes returns nil and an error, and e is unchanged.

func (e *P521Element) SetBytes(v []byte) (*P521Element, error)

SetBytes method #

SetBytes sets e = v, where v is a big-endian 48-byte encoding, and returns e. If v is not 48 bytes or it encodes a value higher than 2^384 - 2^128 - 2^96 + 2^32 - 1, SetBytes returns nil and an error, and e is unchanged.

func (e *P384Element) SetBytes(v []byte) (*P384Element, error)

SetBytes method #

SetBytes sets e = v, where v is a big-endian 32-byte encoding, and returns e. If v is not 32 bytes or it encodes a value higher than 2^256 - 2^224 + 2^192 + 2^96 - 1, SetBytes returns nil and an error, and e is unchanged.

func (e *P256Element) SetBytes(v []byte) (*P256Element, error)

Square method #

Square sets e = t * t, and returns e.

func (e *P384Element) Square(t *P384Element) *P384Element

Square method #

Square sets e = t * t, and returns e.

func (e *P224Element) Square(t *P224Element) *P224Element

Square method #

Square sets e = t * t, and returns e.

func (e *P521Element) Square(t *P521Element) *P521Element

Square method #

Square sets e = t * t, and returns e.

func (e *P256Element) Square(t *P256Element) *P256Element

Sub method #

Sub sets e = t1 - t2, and returns e.

func (e *P224Element) Sub(t1 *P224Element, t2 *P224Element) *P224Element

Sub method #

Sub sets e = t1 - t2, and returns e.

func (e *P384Element) Sub(t1 *P384Element, t2 *P384Element) *P384Element

Sub method #

Sub sets e = t1 - t2, and returns e.

func (e *P256Element) Sub(t1 *P256Element, t2 *P256Element) *P256Element

Sub method #

Sub sets e = t1 - t2, and returns e.

func (e *P521Element) Sub(t1 *P521Element, t2 *P521Element) *P521Element

bytes method #

func (e *P256Element) bytes(out *[p256ElementLen]byte) []byte

bytes method #

func (e *P224Element) bytes(out *[p224ElementLen]byte) []byte

bytes method #

func (e *P384Element) bytes(out *[p384ElementLen]byte) []byte

bytes method #

func (e *P521Element) bytes(out *[p521ElementLen]byte) []byte

p224Add function #

p224Add 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 p224Add(out1 *p224MontgomeryDomainFieldElement, arg1 *p224MontgomeryDomainFieldElement, arg2 *p224MontgomeryDomainFieldElement)

p224CmovznzU64 function #

p224CmovznzU64 is a single-word conditional move. Postconditions: out1 = (if arg1 = 0 then arg2 else arg3) Input Bounds: arg1: [0x0 ~> 0x1] arg2: [0x0 ~> 0xffffffffffffffff] arg3: [0x0 ~> 0xffffffffffffffff] Output Bounds: out1: [0x0 ~> 0xffffffffffffffff]

func p224CmovznzU64(out1 *uint64, arg1 p224Uint1, arg2 uint64, arg3 uint64)

p224FromBytes function #

p224FromBytes 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]] Output Bounds: out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffff]]

func p224FromBytes(out1 *[4]uint64, arg1 *[28]uint8)

p224FromMontgomery function #

p224FromMontgomery 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 p224FromMontgomery(out1 *p224NonMontgomeryDomainFieldElement, arg1 *p224MontgomeryDomainFieldElement)

p224InvertEndianness function #

func p224InvertEndianness(v []byte)

p224Mul function #

p224Mul 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 p224Mul(out1 *p224MontgomeryDomainFieldElement, arg1 *p224MontgomeryDomainFieldElement, arg2 *p224MontgomeryDomainFieldElement)

p224Selectznz function #

p224Selectznz 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 p224Selectznz(out1 *[4]uint64, arg1 p224Uint1, arg2 *[4]uint64, arg3 *[4]uint64)

p224SetOne function #

p224SetOne returns the field element one in the Montgomery domain. Postconditions: eval (from_montgomery out1) mod m = 1 mod m 0 ≤ eval out1 < m

func p224SetOne(out1 *p224MontgomeryDomainFieldElement)

p224Square function #

p224Square 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 p224Square(out1 *p224MontgomeryDomainFieldElement, arg1 *p224MontgomeryDomainFieldElement)

p224Sub function #

p224Sub 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 p224Sub(out1 *p224MontgomeryDomainFieldElement, arg1 *p224MontgomeryDomainFieldElement, arg2 *p224MontgomeryDomainFieldElement)

p224ToBytes function #

p224ToBytes 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..27] Input Bounds: arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffff]] 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]]

func p224ToBytes(out1 *[28]uint8, arg1 *[4]uint64)

p224ToMontgomery function #

p224ToMontgomery 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

func p224ToMontgomery(out1 *p224MontgomeryDomainFieldElement, arg1 *p224NonMontgomeryDomainFieldElement)

p256Add function #

p256Add 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 p256Add(out1 *p256MontgomeryDomainFieldElement, arg1 *p256MontgomeryDomainFieldElement, arg2 *p256MontgomeryDomainFieldElement)

p256CmovznzU64 function #

p256CmovznzU64 is a single-word conditional move. Postconditions: out1 = (if arg1 = 0 then arg2 else arg3) Input Bounds: arg1: [0x0 ~> 0x1] arg2: [0x0 ~> 0xffffffffffffffff] arg3: [0x0 ~> 0xffffffffffffffff] Output Bounds: out1: [0x0 ~> 0xffffffffffffffff]

func p256CmovznzU64(out1 *uint64, arg1 p256Uint1, arg2 uint64, arg3 uint64)

p256FromBytes function #

p256FromBytes 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 p256FromBytes(out1 *[4]uint64, arg1 *[32]uint8)

p256FromMontgomery function #

p256FromMontgomery 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 p256FromMontgomery(out1 *p256NonMontgomeryDomainFieldElement, arg1 *p256MontgomeryDomainFieldElement)

p256InvertEndianness function #

func p256InvertEndianness(v []byte)

p256Mul function #

p256Mul 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 p256Mul(out1 *p256MontgomeryDomainFieldElement, arg1 *p256MontgomeryDomainFieldElement, arg2 *p256MontgomeryDomainFieldElement)

p256Selectznz function #

p256Selectznz 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 p256Selectznz(out1 *[4]uint64, arg1 p256Uint1, arg2 *[4]uint64, arg3 *[4]uint64)

p256SetOne function #

p256SetOne returns the field element one in the Montgomery domain. Postconditions: eval (from_montgomery out1) mod m = 1 mod m 0 ≤ eval out1 < m

func p256SetOne(out1 *p256MontgomeryDomainFieldElement)

p256Square function #

p256Square 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 p256Square(out1 *p256MontgomeryDomainFieldElement, arg1 *p256MontgomeryDomainFieldElement)

p256Sub function #

p256Sub 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 p256Sub(out1 *p256MontgomeryDomainFieldElement, arg1 *p256MontgomeryDomainFieldElement, arg2 *p256MontgomeryDomainFieldElement)

p256ToBytes function #

p256ToBytes 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 p256ToBytes(out1 *[32]uint8, arg1 *[4]uint64)

p256ToMontgomery function #

p256ToMontgomery 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

func p256ToMontgomery(out1 *p256MontgomeryDomainFieldElement, arg1 *p256NonMontgomeryDomainFieldElement)

p384Add function #

p384Add 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 p384Add(out1 *p384MontgomeryDomainFieldElement, arg1 *p384MontgomeryDomainFieldElement, arg2 *p384MontgomeryDomainFieldElement)

p384CmovznzU64 function #

p384CmovznzU64 is a single-word conditional move. Postconditions: out1 = (if arg1 = 0 then arg2 else arg3) Input Bounds: arg1: [0x0 ~> 0x1] arg2: [0x0 ~> 0xffffffffffffffff] arg3: [0x0 ~> 0xffffffffffffffff] Output Bounds: out1: [0x0 ~> 0xffffffffffffffff]

func p384CmovznzU64(out1 *uint64, arg1 p384Uint1, arg2 uint64, arg3 uint64)

p384FromBytes function #

p384FromBytes 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], [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], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

func p384FromBytes(out1 *[6]uint64, arg1 *[48]uint8)

p384FromMontgomery function #

p384FromMontgomery 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)^6) mod m 0 ≤ eval out1 < m

func p384FromMontgomery(out1 *p384NonMontgomeryDomainFieldElement, arg1 *p384MontgomeryDomainFieldElement)

p384InvertEndianness function #

func p384InvertEndianness(v []byte)

p384Mul function #

p384Mul 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 p384Mul(out1 *p384MontgomeryDomainFieldElement, arg1 *p384MontgomeryDomainFieldElement, arg2 *p384MontgomeryDomainFieldElement)

p384Selectznz function #

p384Selectznz 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], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] Output Bounds: out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

func p384Selectznz(out1 *[6]uint64, arg1 p384Uint1, arg2 *[6]uint64, arg3 *[6]uint64)

p384SetOne function #

p384SetOne returns the field element one in the Montgomery domain. Postconditions: eval (from_montgomery out1) mod m = 1 mod m 0 ≤ eval out1 < m

func p384SetOne(out1 *p384MontgomeryDomainFieldElement)

p384Square function #

p384Square 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 p384Square(out1 *p384MontgomeryDomainFieldElement, arg1 *p384MontgomeryDomainFieldElement)

p384Sub function #

p384Sub 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 p384Sub(out1 *p384MontgomeryDomainFieldElement, arg1 *p384MontgomeryDomainFieldElement, arg2 *p384MontgomeryDomainFieldElement)

p384ToBytes function #

p384ToBytes 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..47] Input Bounds: arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [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], [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 p384ToBytes(out1 *[48]uint8, arg1 *[6]uint64)

p384ToMontgomery function #

p384ToMontgomery 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

func p384ToMontgomery(out1 *p384MontgomeryDomainFieldElement, arg1 *p384NonMontgomeryDomainFieldElement)

p521Add function #

p521Add 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 p521Add(out1 *p521MontgomeryDomainFieldElement, arg1 *p521MontgomeryDomainFieldElement, arg2 *p521MontgomeryDomainFieldElement)

p521CmovznzU64 function #

p521CmovznzU64 is a single-word conditional move. Postconditions: out1 = (if arg1 = 0 then arg2 else arg3) Input Bounds: arg1: [0x0 ~> 0x1] arg2: [0x0 ~> 0xffffffffffffffff] arg3: [0x0 ~> 0xffffffffffffffff] Output Bounds: out1: [0x0 ~> 0xffffffffffffffff]

func p521CmovznzU64(out1 *uint64, arg1 p521Uint1, arg2 uint64, arg3 uint64)

p521FromBytes function #

p521FromBytes 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], [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], [0x0 ~> 0xff], [0x0 ~> 0x1]] Output Bounds: out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x1ff]]

func p521FromBytes(out1 *[9]uint64, arg1 *[66]uint8)

p521FromMontgomery function #

p521FromMontgomery 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)^9) mod m 0 ≤ eval out1 < m

func p521FromMontgomery(out1 *p521NonMontgomeryDomainFieldElement, arg1 *p521MontgomeryDomainFieldElement)

p521InvertEndianness function #

func p521InvertEndianness(v []byte)

p521Mul function #

p521Mul 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 p521Mul(out1 *p521MontgomeryDomainFieldElement, arg1 *p521MontgomeryDomainFieldElement, arg2 *p521MontgomeryDomainFieldElement)

p521Selectznz function #

p521Selectznz 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], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] Output Bounds: out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

func p521Selectznz(out1 *[9]uint64, arg1 p521Uint1, arg2 *[9]uint64, arg3 *[9]uint64)

p521SetOne function #

p521SetOne returns the field element one in the Montgomery domain. Postconditions: eval (from_montgomery out1) mod m = 1 mod m 0 ≤ eval out1 < m

func p521SetOne(out1 *p521MontgomeryDomainFieldElement)

p521Square function #

p521Square 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 p521Square(out1 *p521MontgomeryDomainFieldElement, arg1 *p521MontgomeryDomainFieldElement)

p521Sub function #

p521Sub 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 p521Sub(out1 *p521MontgomeryDomainFieldElement, arg1 *p521MontgomeryDomainFieldElement, arg2 *p521MontgomeryDomainFieldElement)

p521ToBytes function #

p521ToBytes 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..65] Input Bounds: arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x1ff]] 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], [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], [0x0 ~> 0xff], [0x0 ~> 0x1]]

func p521ToBytes(out1 *[66]uint8, arg1 *[9]uint64)

p521ToMontgomery function #

p521ToMontgomery 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

func p521ToMontgomery(out1 *p521MontgomeryDomainFieldElement, arg1 *p521NonMontgomeryDomainFieldElement)

Generated with Arrow