Fixed-limb product runtime #

Carry-preserving addition and full products operate over one, two, and four native limbs. The UInt256 carrier holds the full product of two UInt128 values, so the product needs no arbitrary-precision conversion.

Product.Proof shows that each returned value and carry reconstruct the natural-number sum or product.

source

structure FloatLib.Numerics.FixedWord.AddResult (α : Type u) :

Type u

A fixed-width addition result together with its unsigned carry.

value : α
Low fixed-width part of the sum.
carry : UInt64
Carry above the payload's highest bit, represented as a native word.

Instances For

source

def FloatLib.Numerics.FixedWord.instDecidableEqAddResult.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : AddResult α✝) :

Decidable (x✝ = x✝¹)

Instances For

source

@[instance_reducible]

instance FloatLib.Numerics.FixedWord.instDecidableEqAddResult {α✝ : Type u_1} [DecidableEq α✝] :

DecidableEq (AddResult α✝)

source

@[instance_reducible]

instance FloatLib.Numerics.FixedWord.instReprAddResult {α✝ : Type u_1} [Repr α✝] :

Repr (AddResult α✝)

source

def FloatLib.Numerics.FixedWord.instReprAddResult.repr {α✝ : Type u_1} [Repr α✝] :

AddResult α✝ → ℕ → Std.Format

Instances For

source

@[inline]

def FloatLib.Numerics.FixedWord.add64 (x y : UInt64) :

AddResult UInt64

Add two native words and retain the unsigned carry.

Instances For

source

@[inline]

def FloatLib.Numerics.FixedWord.addCarry64 (x y carry : UInt64) :

AddResult UInt64

Add two words and an incoming carry.

Instances For

source

@[inline]

def FloatLib.Numerics.FixedWord.add128 (x y : UInt128) :

AddResult UInt128

Add two two-word values.

Instances For

source

structure FloatLib.Numerics.FixedWord.UInt256 :

Type

A 256-bit unsigned value represented by four native 64-bit limbs.

limb3 : UInt64
Bits 192 through 255.
limb2 : UInt64
Bits 128 through 191.
limb1 : UInt64
Bits 64 through 127.
limb0 : UInt64
Bits 0 through 63.

Instances For

source

@[instance_reducible]

instance FloatLib.Numerics.FixedWord.instDecidableEqUInt256 :

DecidableEq UInt256

source

def FloatLib.Numerics.FixedWord.instDecidableEqUInt256.decEq (x✝ x✝¹ : UInt256) :

Decidable (x✝ = x✝¹)

Instances For

source

@[instance_reducible]

instance FloatLib.Numerics.FixedWord.instReprUInt256 :

Repr UInt256

source

def FloatLib.Numerics.FixedWord.instReprUInt256.repr :

UInt256 → ℕ → Std.Format

Instances For

source

@[inline]

def FloatLib.Numerics.FixedWord.UInt256.ofUInt128 (value : UInt128) :

UInt256

Embed a two-limb unsigned value in the low half of a four-limb carrier.

Instances For

source

@[inline]

def FloatLib.Numerics.FixedWord.UInt256.ofUInt128ShiftedLeft (value : UInt128) (shift : ℕ) :

UInt256

Embed a two-limb value after shifting it left by shift bits, for 64 < shift < 128.

The two-word kernels for formats of at most 128 bits align a fracWidth + 1-bit significand by fracWidth or fracWidth + 1 places, so division, fused multiply-add, and square root share this one word shuffle. toNat_ofUInt128ShiftedLeft gives its value under the stated shift bounds. Outside them the native shift counts wrap and the result is unspecified.

Instances For

source

@[inline]

def FloatLib.Numerics.FixedWord.UInt256.low128 (value : UInt256) :

UInt128

Return the low two limbs of a four-limb unsigned value.

Instances For

source

def FloatLib.Numerics.FixedWord.UInt256.toNat (value : UInt256) :

ℕ

Mathematical value of a four-limb unsigned integer.

Instances For

source

@[inline]

def FloatLib.Numerics.FixedWord.UInt256.log2 (value : UInt256) :

ℕ

Position of the most significant set bit, with zero mapped to zero.

Instances For

source

@[inline]

def FloatLib.Numerics.FixedWord.add256 (x y : UInt256) :

AddResult UInt256

Add two four-word values.

Instances For

source

@[inline]

def FloatLib.Numerics.FixedWord.mul128 (x y : UInt128) :

UInt256

Full 256-bit product of two two-limb values in native arithmetic.

Four mul64 products form the schoolbook product. Each output column is reduced with add64, and the resulting carry count is passed to the next column.

Instances For

Scalar-carry implementations #

AddResult UInt64 boxes its value field, and the generated code materializes the record behind the carry branch, so every add64 inside a larger kernel allocates. The definitions below repeat the same column arithmetic with every intermediate sum and carry as a native word. Each is definitionally equal to the definition it replaces, and @[csimp] installs it in compiled code.

source

@[inline]