Eight-limb Montgomery arithmetic: runtime definitions (zero-import)

The runtime definitions of the eight-limb Montgomery arithmetic, split out of CompPoly.Fields.Montgomery.Native64x8 verbatim. All correctness statements about them live in that sibling module, which imports this one.

This module deliberately has zero imports: downstream consumers put it into precompileModules native-compilation lanes, and precompileModules compiles the entire import closure — so the runtime definitions must not pull in mathlib.

Word helpers

@[inline]

def Montgomery.Native64x8.mask : UInt64

Mask selecting the low 32 bits of a UInt64.

@[inline]

def Montgomery.Native64x8.adcLo (x y c : UInt64) : UInt64

Low limb of add-with-carry: (x + y + c) mod 2 ^ 32.

@[inline]

def Montgomery.Native64x8.adcCo (x y c : UInt64) : UInt64

Carry-out of add-with-carry: (x + y + c) / 2 ^ 32.

@[inline]

def Montgomery.Native64x8.sbbLo (x y b : UInt64) : UInt64

Low limb of subtract-with-borrow: (x - y - b) mod 2 ^ 32.

@[inline]

def Montgomery.Native64x8.sbbBo (x y b : UInt64) : UInt64

Borrow-out of subtract-with-borrow, read off the sign bit of the 64-bit difference.

@[inline]

def Montgomery.Native64x8.macLo (t x y c : UInt64) : UInt64

Low limb of multiply-accumulate: (t + x * y + c) mod 2 ^ 32.

@[inline]

def Montgomery.Native64x8.macHi (t x y c : UInt64) : UInt64

High word of multiply-accumulate: (t + x * y + c) / 2 ^ 32.

@[inline]

def Montgomery.Native64x8.montM (s negInv : UInt64) : UInt64

The Montgomery multiplier of a limb: (s * negInv) mod 2 ^ 32.

Eight-limb values

structure Montgomery.Native64x8.Limbs8 : Type

A 256-bit value as eight little-endian 32-bit limbs, each stored in a UInt64.

• l0 : UInt64

  Limb of weight 2 ^ 0.

• l1 : UInt64

  Limb of weight 2 ^ 32.

• l2 : UInt64

  Limb of weight 2 ^ 64.

• l3 : UInt64

  Limb of weight 2 ^ 96.

• l4 : UInt64

  Limb of weight 2 ^ 128.

• l5 : UInt64

  Limb of weight 2 ^ 160.

• l6 : UInt64

  Limb of weight 2 ^ 192.

• l7 : UInt64

  Limb of weight 2 ^ 224.

def Montgomery.Native64x8.instDecidableEqLimbs8.decEq (x✝ x✝¹ : Limbs8) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Montgomery.Native64x8.instDecidableEqLimbs8 : DecidableEq Limbs8

@[instance_reducible]

instance Montgomery.Native64x8.instReprLimbs8 : Repr Limbs8

def Montgomery.Native64x8.instReprLimbs8.repr : Limbs8 → Nat → Std.Format

@[instance_reducible]

instance Montgomery.Native64x8.instInhabitedLimbs8 : Inhabited Limbs8

def Montgomery.Native64x8.Limbs8.zero : Limbs8

The zero value.

def Montgomery.Native64x8.Limbs8.one : Limbs8

The value one.

@[inline]

def Montgomery.Native64x8.Limbs8.ofNat (n : Nat) : Limbs8

Split a natural number into eight 32-bit limbs, discarding bits above 2 ^ 256.

def Montgomery.Native64x8.Limbs8.toNat (x : Limbs8) : Nat

The natural number represented by the limbs: ∑ lᵢ * 2 ^ (32 * i).

def Montgomery.Native64x8.Limbs8.Bounded (x : Limbs8) : Prop

Every limb holds at most 32 significant bits.

@[instance_reducible]

instance Montgomery.Native64x8.Limbs8.instDecidableBounded (x : Limbs8) : Decidable x.Bounded

Limbwise addition and subtraction

@[inline]

def Montgomery.Native64x8.addLimbs (a b : Limbs8) : Limbs8

Limbwise add-with-carry, discarding the carry out of the top limb.

@[inline]

def Montgomery.Native64x8.subLimbs (a b : Limbs8) : Limbs8

Limbwise subtract-with-borrow.

@[inline]

def Montgomery.Native64x8.subBorrow (a b : Limbs8) : UInt64

Borrow out of the top limb of subLimbs.

Conditional subtraction and field operations

@[inline]

def Montgomery.Native64x8.condSub (q t : Limbs8) : Limbs8

Subtract the modulus once if the value is at least the modulus. The borrow chain decides the branch, so no comparison is needed.

@[inline]

def Montgomery.Native64x8.add (q a b : Limbs8) : Limbs8

Modular addition.

@[inline]

def Montgomery.Native64x8.sub (q a b : Limbs8) : Limbs8

Modular subtraction: on a borrow, the modulus is added back.

@[inline]

def Montgomery.Native64x8.neg (q a : Limbs8) : Limbs8

Modular negation.

CIOS multiplication

structure Montgomery.Native64x8.State9 : Type

The CIOS accumulator: eight limbs plus one head limb.

• t0 : UInt64

  Limb of weight 2 ^ 0.

• t1 : UInt64

  Limb of weight 2 ^ 32.

• t2 : UInt64

  Limb of weight 2 ^ 64.

• t3 : UInt64

  Limb of weight 2 ^ 96.

• t4 : UInt64

  Limb of weight 2 ^ 128.

• t5 : UInt64

  Limb of weight 2 ^ 160.

• t6 : UInt64

  Limb of weight 2 ^ 192.

• t7 : UInt64

  Limb of weight 2 ^ 224.

• t8 : UInt64

  Head limb of weight 2 ^ 256.

@[instance_reducible]

instance Montgomery.Native64x8.instDecidableEqState9 : DecidableEq State9

def Montgomery.Native64x8.instDecidableEqState9.decEq (x✝ x✝¹ : State9) : Decidable (x✝ = x✝¹)

def Montgomery.Native64x8.instReprState9.repr : State9 → Nat → Std.Format

@[instance_reducible]

instance Montgomery.Native64x8.instReprState9 : Repr State9

@[instance_reducible]

instance Montgomery.Native64x8.instInhabitedState9 : Inhabited State9

@[inline]

def Montgomery.Native64x8.State9.zero : State9

The zero accumulator.

@[inline]

def Montgomery.Native64x8.State9.toLimbs8 (t : State9) : Limbs8

The eight low limbs of the accumulator.

def Montgomery.Native64x8.State9.toNat (t : State9) : Nat

The natural number represented by the accumulator.

def Montgomery.Native64x8.State9.Bounded (t : State9) : Prop

Every limb of the accumulator holds at most 32 significant bits.

@[inline]

def Montgomery.Native64x8.mulAccum (a : Limbs8) (bi : UInt64) (t : State9) : State9

The multiply half of a CIOS round: accumulate a * bi into the accumulator. The carry out of the top limb is kept in the head limb, so no information is lost.

@[inline]

def Montgomery.Native64x8.mulReduce (q : Limbs8) (negInv : UInt64) (s : State9) : State9

The reduce half of a CIOS round: add the multiple montM s.t0 negInv of the modulus that cancels the low limb, then drop that limb. negInv has to be -q⁻¹ mod 2 ^ 32.

@[inline]

def Montgomery.Native64x8.mulRound (q : Limbs8) (negInv : UInt64) (a : Limbs8) (bi : UInt64) (t : State9) : State9

One CIOS outer round: accumulate a * bi into the accumulator, then reduce away one limb.

@[inline]

def Montgomery.Native64x8.mul (q : Limbs8) (negInv : UInt64) (a b : Limbs8) : Limbs8

CIOS Montgomery multiplication: eight rounds followed by one conditional subtraction.

@[inline]

def Montgomery.Native64x8.square (q : Limbs8) (negInv : UInt64) (a : Limbs8) : Limbs8

Montgomery squaring.