Executable configured shared-scale blocks

These operations expose complete storage, exact decoding, and contextual quantization at a caller-selected exponent.

The caller supplies the shared exponent, so different calibration strategies can use the same quantizer. Exponents and significands are unbounded integers; the vector type fixes the lane count.

@[inline]

def FloatLib.Floats.ExecFloat.SharedScale.ofCode {lanes : ℕ} (code : Formats.Block.SharedScaleCode lanes) : SharedScale lanes

Wrap a complete shared-scale block code without conversion.

@[inline]

def FloatLib.Floats.ExecFloat.SharedScale.toCode {lanes : ℕ} (value : SharedScale lanes) : Formats.Block.SharedScaleCode lanes

Recover the complete shared-scale block code without conversion.

@[inline]

def FloatLib.Floats.ExecFloat.SharedScale.ofComponents {lanes : ℕ} (exponent : ℤ) (significands : Vector ℤ lanes) : SharedScale lanes

Construct a block from one exponent and exactly lanes stored significands.

@[inline]

def FloatLib.Floats.ExecFloat.SharedScale.exponent {lanes : ℕ} (value : SharedScale lanes) : ℤ

Stored shared binary exponent.

@[inline]

def FloatLib.Floats.ExecFloat.SharedScale.significands {lanes : ℕ} (value : SharedScale lanes) : Vector ℤ lanes

Stored integer significands.

@[inline]

def FloatLib.Floats.ExecFloat.SharedScale.decode {lanes : ℕ} (value : SharedScale lanes) : Vector ℚ lanes

Decode every lane to its exact rational value.

@[inline]

def FloatLib.Floats.ExecFloat.SharedScale.quantizeAt {lanes : ℕ} (exponent : ℤ) (input : Vector ℚ lanes) : SharedScale lanes

Quantize every lane at an explicitly supplied shared exponent.