curve25519

Documentation

Overview

Code generated by Fiat Cryptography. DO NOT EDIT.

Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Go --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 curve25519 ” 32 '(auto)' '2^255 - 19' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax carry_scmul121666 carry_add carry_sub carry_opp

curve description (via package name): curve25519

machine_wordsize = 32 (from "32")

requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax, carry_scmul121666, carry_add, carry_sub, carry_opp

n = 10 (from "(auto)")

s-c = 2^255 - [(1, 19)] (from "2^255 - 19")

tight_bounds_multiplier = 1 (from "")

Computed values:

carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 0, 1]

eval z = z[0] + (z[1] << 26) + (z[2] << 51) + (z[3] << 77) + (z[4] << 102) + (z[5] << 128) + (z[6] << 153) + (z[7] << 179) + (z[8] << 204) + (z[9] << 230)

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)

balance = [0x7ffffda, 0x3fffffe, 0x7fffffe, 0x3fffffe, 0x7fffffe, 0x3fffffe, 0x7fffffe, 0x3fffffe, 0x7fffffe, 0x3fffffe]

Index

• func Add(out1 *LooseFieldElement, arg1 *TightFieldElement, arg2 *TightFieldElement)
• func Carry(out1 *TightFieldElement, arg1 *LooseFieldElement)
• func CarryAdd(out1 *TightFieldElement, arg1 *TightFieldElement, arg2 *TightFieldElement)
• func CarryMul(out1 *TightFieldElement, arg1 *LooseFieldElement, arg2 *LooseFieldElement)
• func CarryOpp(out1 *TightFieldElement, arg1 *TightFieldElement)
• func CarryScmul121666(out1 *TightFieldElement, arg1 *LooseFieldElement)
• func CarrySquare(out1 *TightFieldElement, arg1 *LooseFieldElement)
• func CarrySub(out1 *TightFieldElement, arg1 *TightFieldElement, arg2 *TightFieldElement)
• func FromBytes(out1 *TightFieldElement, arg1 *[32]uint8)
• func Opp(out1 *LooseFieldElement, arg1 *TightFieldElement)
• func Relax(out1 *LooseFieldElement, arg1 *TightFieldElement)
• func Selectznz(out1 *[10]uint32, arg1 uint1, arg2 *[10]uint32, arg3 *[10]uint32)
• func Sub(out1 *LooseFieldElement, arg1 *TightFieldElement, arg2 *TightFieldElement)
• func ToBytes(out1 *[32]uint8, arg1 *TightFieldElement)
• type LooseFieldElement
• type TightFieldElement

Functions

func Add

func Add(out1 *LooseFieldElement, arg1 *TightFieldElement, arg2 *TightFieldElement)

Add adds two field elements.

Postconditions:

eval out1 mod m = (eval arg1 + eval arg2) mod m

func Carry

func Carry(out1 *TightFieldElement, arg1 *LooseFieldElement)

Carry reduces a field element.

Postconditions:

eval out1 mod m = eval arg1 mod m

func CarryAdd

func CarryAdd(out1 *TightFieldElement, arg1 *TightFieldElement, arg2 *TightFieldElement)

CarryAdd adds two field elements.

Postconditions:

eval out1 mod m = (eval arg1 + eval arg2) mod m

func CarryMul

func CarryMul(out1 *TightFieldElement, arg1 *LooseFieldElement, arg2 *LooseFieldElement)

CarryMul multiplies two field elements and reduces the result.

Postconditions:

eval out1 mod m = (eval arg1 * eval arg2) mod m

func CarryOpp

func CarryOpp(out1 *TightFieldElement, arg1 *TightFieldElement)

CarryOpp negates a field element.

Postconditions:

eval out1 mod m = -eval arg1 mod m

func CarryScmul121666

func CarryScmul121666(out1 *TightFieldElement, arg1 *LooseFieldElement)

CarryScmul121666 multiplies a field element by 121666 and reduces the result.

Postconditions:

eval out1 mod m = (121666 * eval arg1) mod m

func CarrySquare

func CarrySquare(out1 *TightFieldElement, arg1 *LooseFieldElement)

CarrySquare squares a field element and reduces the result.

Postconditions:

eval out1 mod m = (eval arg1 * eval arg1) mod m

func CarrySub

func CarrySub(out1 *TightFieldElement, arg1 *TightFieldElement, arg2 *TightFieldElement)

CarrySub subtracts two field elements.

Postconditions:

eval out1 mod m = (eval arg1 - eval arg2) mod m

func FromBytes

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

FromBytes deserializes a field element from bytes in little-endian order.

Postconditions:

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

func Opp

func Opp(out1 *LooseFieldElement, arg1 *TightFieldElement)

Opp negates a field element.

Postconditions:

eval out1 mod m = -eval arg1 mod m

func Relax

func Relax(out1 *LooseFieldElement, arg1 *TightFieldElement)

Relax is the identity function converting from tight field elements to loose field elements.

Postconditions:

out1 = arg1

func Selectznz

func Selectznz(out1 *[10]uint32, arg1 uint1, arg2 *[10]uint32, arg3 *[10]uint32)

Selectznz is a multi-limb conditional select.

Postconditions:

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

Input Bounds:

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

Output Bounds:

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

func Sub

func Sub(out1 *LooseFieldElement, arg1 *TightFieldElement, arg2 *TightFieldElement)

Sub subtracts two field elements.

Postconditions:

eval out1 mod m = (eval arg1 - eval arg2) mod m

func ToBytes

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

ToBytes serializes a field element to bytes in little-endian order.

Postconditions:

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

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 ~> 0x7f]]

Types

type LooseFieldElement

type LooseFieldElement [10]uint32

LooseFieldElement is a field element with loose bounds.

Bounds:

[[0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000]]

type TightFieldElement

type TightFieldElement [10]uint32

TightFieldElement is a field element with tight bounds.

Bounds:

[[0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000]]