Shared-scale block model

A block code represents lanes rational values with one binary exponent and one integer significand per lane. Quantization is contextual because the shared exponent is supplied by the caller rather than inferred by the universal format.

The organization follows the Open Compute Project microscaling model while remaining independent of a particular element width or scale-selection policy.

Reference

• Open Compute Project, OCP Microscaling Formats (MX) Specification, Version 1.0 (2023): https://www.opencompute.org/documents/ocp-microscaling-formats-mx-v1-0-spec-final-pdf.

structure FloatLib.Floats.Formats.Block.SharedScaleCode (lanes : ℕ) : Type

Runtime storage for a block of integer significands with one shared binary exponent.

• exponent : ℤ

  Shared power-of-two exponent.

• significands : Vector ℤ lanes

  Per-lane integer significands.

def FloatLib.Floats.Formats.Block.instDecidableEqSharedScaleCode.decEq {lanes✝ : ℕ} (x✝ x✝¹ : SharedScaleCode lanes✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.Block.instDecidableEqSharedScaleCode {lanes✝ : ℕ} : DecidableEq (SharedScaleCode lanes✝)

def FloatLib.Floats.Formats.Block.instReprSharedScaleCode.repr {lanes✝ : ℕ} : SharedScaleCode lanes✝ → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.Block.instReprSharedScaleCode {lanes✝ : ℕ} : Repr (SharedScaleCode lanes✝)

inductive FloatLib.Floats.Formats.Block.SharedScale (lanes : ℕ) : Type

Type-level identity of an unbounded shared-scale block with lanes entries.

• format {lanes : ℕ} : SharedScale lanes

@[instance_reducible]

instance FloatLib.Floats.Formats.Block.instEncodedFormatSharedScale (lanes : ℕ) : Numerics.EncodedFormat (SharedScale lanes)

@[inline]

def FloatLib.Floats.Formats.Block.scale (exponent : ℤ) : ℚ

Exact rational multiplier selected by a shared binary exponent.

@[inline]

def FloatLib.Floats.Formats.Block.decode {lanes : ℕ} (code : SharedScaleCode lanes) : Vector ℚ lanes

Decode every lane using the one scale stored in the block.

@[instance_reducible]

instance FloatLib.Floats.Formats.Block.instFormatSemanticsSharedScale (lanes : ℕ) : Numerics.FormatSemantics (SharedScale lanes)

def FloatLib.Floats.Formats.Block.exactSemantics (lanes : ℕ) : Numerics.ExactSemantics (Numerics.formatSystem (SharedScale lanes))

Exact block observation retaining the selected scale and stored significands.

Forgetting this observation decodes the rational vector; it discards the choice of representation.

@[instance_reducible]

instance FloatLib.Floats.Formats.Block.instHasExactSemanticsSharedScale (lanes : ℕ) : Numerics.HasExactSemantics (SharedScale lanes)

def FloatLib.Floats.Formats.Block.QuantizesAt {lanes : ℕ} (exponent : ℤ) (input : Vector ℚ lanes) (result : SharedScaleCode lanes) : Prop

Quantization at a caller-selected scale: retain the exponent and round each scaled lane to the nearest integer, with ties to even.