Arithmetic modulo 2^255 - 19 on ten UInt64 limbs

An element is Σ hᵢ · 2^⌈25.5·i⌉: limbs alternate 26 and 25 bits, so a product of two limbs fits in 64 bits with room to sum ten of them. Every operation ends with carry, which leaves each limb below 2^26; operations accept any input in that bound. Values are not kept fully reduced: toNat is the represented number and toNat % p its canonical value. The limbs are separate structure fields rather than an array so that they stay unboxed.

structure Cryptlib.Primitives.NIKE.Field25519.Fe : Type

• h0 : UInt64
• h1 : UInt64
• h2 : UInt64
• h3 : UInt64
• h4 : UInt64
• h5 : UInt64
• h6 : UInt64
• h7 : UInt64
• h8 : UInt64
• h9 : UInt64

@[instance_reducible]

instance Cryptlib.Primitives.NIKE.Field25519.instInhabitedFe : Inhabited Fe

Equations

• Cryptlib.Primitives.NIKE.Field25519.instInhabitedFe = { default := Cryptlib.Primitives.NIKE.Field25519.instInhabitedFe.default }

def Cryptlib.Primitives.NIKE.Field25519.instReprFe.repr : Fe → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Cryptlib.Primitives.NIKE.Field25519.instReprFe : Repr Fe

Equations

• Cryptlib.Primitives.NIKE.Field25519.instReprFe = { reprPrec := Cryptlib.Primitives.NIKE.Field25519.instReprFe.repr }

def Cryptlib.Primitives.NIKE.Field25519.Fe.offsets : List ℕ

Bit offset of each limb.

Equations

• Cryptlib.Primitives.NIKE.Field25519.Fe.offsets = [0, 26, 51, 77, 102, 128, 153, 179, 204, 230]

def Cryptlib.Primitives.NIKE.Field25519.Fe.limbs (f : Fe) : List UInt64

Equations

• f.limbs = [f.h0, f.h1, f.h2, f.h3, f.h4, f.h5, f.h6, f.h7, f.h8, f.h9]

def Cryptlib.Primitives.NIKE.Field25519.Fe.toNat (f : Fe) : ℕ

The number the limbs represent.

Equations

• f.toNat = List.foldl (fun (acc : ℕ) (x : UInt64 × ℕ) => match x with | (l, o) => acc + l.toNat <<< o) 0 (f.limbs.zip Cryptlib.Primitives.NIKE.Field25519.Fe.offsets)

def Cryptlib.Primitives.NIKE.Field25519.Fe.ofNat (n : ℕ) : Fe

Split n < 2^256 into limbs; bits from 255 up are folded back in as multiples of 19.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.NIKE.Field25519.Fe.ofNat.carry' (h : Fe) : Fe

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.NIKE.Field25519.Fe.zero : Fe

Equations

• Cryptlib.Primitives.NIKE.Field25519.Fe.zero = { h0 := 0, h1 := 0, h2 := 0, h3 := 0, h4 := 0, h5 := 0, h6 := 0, h7 := 0, h8 := 0, h9 := 0 }

def Cryptlib.Primitives.NIKE.Field25519.Fe.one : Fe

Equations

• Cryptlib.Primitives.NIKE.Field25519.Fe.one = { h0 := 1, h1 := 0, h2 := 0, h3 := 0, h4 := 0, h5 := 0, h6 := 0, h7 := 0, h8 := 0, h9 := 0 }

def Cryptlib.Primitives.NIKE.Field25519.Fe.carry (h : Fe) : Fe

Bring every limb back under its width, folding the overflow of the top limb into the bottom one as a multiple of 19. Accepts limbs up to 2^62.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.NIKE.Field25519.Fe.add (f g : Fe) : Fe

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.NIKE.Field25519.Fe.sub (f g : Fe) : Fe

f - g as f + 2p - g, so no limb goes negative.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.NIKE.Field25519.Fe.mulSmall (f : Fe) (c : UInt64) : Fe

Multiplication by a constant below 2^30.

Equations

• f.mulSmall c = { h0 := f.h0 * c, h1 := f.h1 * c, h2 := f.h2 * c, h3 := f.h3 * c, h4 := f.h4 * c, h5 := f.h5 * c, h6 := f.h6 * c, h7 := f.h7 * c, h8 := f.h8 * c, h9 := f.h9 * c }.carry

def Cryptlib.Primitives.NIKE.Field25519.Fe.mul (f g : Fe) : Fe

hₖ = Σ_{i+j=k} c·fᵢgⱼ + Σ_{i+j=k+10} 19·c·fᵢgⱼ, where c = 2 when i and j are both odd: the offsets of two odd limbs sum to one more than the offset of their product's limb, and 2^255 ≡ 19.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.NIKE.Field25519.Fe.sq (f : Fe) : Fe

Equations

• f.sq = f.mul f

def Cryptlib.Primitives.NIKE.Field25519.Fe.sqN (f : Fe) : ℕ → Fe

f^(2^k).

Equations

• f.sqN 0 = f
• f.sqN k.succ = f.sq.sqN k

def Cryptlib.Primitives.NIKE.Field25519.Fe.invert (z : Fe) : Fe

f^(p-2), which is f⁻¹ for f ≠ 0 and 0 for f = 0, by the usual addition chain.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.NIKE.Field25519.Fe.cswap (swap : UInt64) (f g : Fe) : Fe × Fe

Swap f and g when swap is 1, without branching on it. swap must be 0 or 1.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.NIKE.Field25519.Fe.ofBytes (v : Vector UInt8 X25519Common.keySize) : Fe

Little-endian bytes with bit 255 masked, as RFC 7748 decodes a u-coordinate.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.NIKE.Field25519.Fe.toBytes (f : Fe) : Vector UInt8 X25519Common.keySize

The canonical little-endian encoding.

Equations

• f.toBytes = Vector.ofFn fun (i : Fin Cryptlib.Primitives.NIKE.X25519Common.keySize) => ((f.toNat % Cryptlib.Primitives.NIKE.X25519Common.p) >>> (8 * ↑i)).toUInt8