P3109 scaled blocks

Chapter 5 of the unapproved P3109 interim report 4.0.3 defines a nonempty sequence with one independently typed scale. Decoding multiplies exact closed rational observations, and projection normalizes each exact result before one destination projection. Zero and infinite result scales use the special rules of §5.4.2 rather than ordinary division.

A policy holds one saturation mode and one rounding mode for the whole block. Stochastic modes take one random word per lane, all of the same bit width. Reductions accumulate exact closed values in lane order and round only the final result. The generic elementwise operations cover exact rational closed operations. Transcendental functions need a separate evaluator, which this module does not install.

Reference: §§5.3–5.8 of https://github.com/P3109/Public/tree/34f5964d9bb2382b2665d15467fc3517b990b308.

structure FloatLib.Floats.Formats.P3109.Block (Scale Element : Type) (length : ℕ+) : Type

A nonempty block with independently typed scale and scalar elements.

• scale : Scale

  Shared scale, decoded through its own exact source interface.

• values : Vector Element ↑length

  Scalar element codes, one per lane.

inductive FloatLib.Floats.Formats.P3109.BlockRounding (length : ℕ+) : Type

A scalar rounding rule for the whole block, or same-width stochastic words, one per lane.

• scalar {length : ℕ+} (mode : RoundingMode) : BlockRounding length
• stochasticA {length : ℕ+} (width : ℕ) (words : Vector (BitVec width) ↑length) : BlockRounding length
• stochasticB {length : ℕ+} (width : ℕ) (words : Vector (BitVec width) ↑length) : BlockRounding length
• stochasticC {length : ℕ+} (width : ℕ) (words : Vector (BitVec width) ↑length) : BlockRounding length

structure FloatLib.Floats.Formats.P3109.BlockPolicy (length : ℕ+) : Type

Projection attributes shared by a block, with per-lane random words for stochastic modes.

• rounding : BlockRounding length

  Scalar rule or the report's sequence of stochastic random words.

• saturation : SaturationMode

  One saturation rule, shared by every element projection.

def FloatLib.Floats.Formats.P3109.BlockPolicy.at {length : ℕ+} (policy : BlockPolicy length) (lane : Fin ↑length) : ProjectionPolicy

Specialize the shared rounding attributes to one lane as prescribed by §5.3.

def FloatLib.Floats.Formats.P3109.Block.decode {length : ℕ+} {Scale ScaleExact Source SourceExact : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] (block : Block Scale Source length) : Vector (Numerics.NumericalValue ℚ) ↑length

Exact §5.4.1 decoding, including the closed rules for nonfinite scale or element codes.

def FloatLib.Floats.Formats.P3109.Block.signum : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Closed signum, with zero mapped to zero and either infinity to its sign.

def FloatLib.Floats.Formats.P3109.Block.normalize : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Exact §5.4.2 result normalization. NaN takes precedence over zero or infinite scales. A zero scale maps other inputs to zero, and an infinite scale maps them to a signed unit or zero.

def FloatLib.Floats.Formats.P3109.Block.project {length : ℕ+} {Scale ScaleExact Result : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] (destination : Arithmetic.Destination Result) (policy : BlockPolicy length) (scale : Scale) (values : Vector (Numerics.NumericalValue ℚ) ↑length) : Vector Result ↑length

Normalize exact lane results at the supplied scale, then project each lane once.

def FloatLib.Floats.Formats.P3109.Block.convertFrom {length : ℕ+} {Scale ScaleExact Source SourceExact Result : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] (destination : Arithmetic.Destination Result) (policy : BlockPolicy length) (block : Block Scale Source length) : Vector Result ↑length

§5.5.1 conversion out of a block, with independent scalar destination and lane attributes.

def FloatLib.Floats.Formats.P3109.Block.convertTo {length : ℕ+} {Scale ScaleExact Source SourceExact Result : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] (destination : Arithmetic.Destination Result) (policy : BlockPolicy length) (values : Vector Source ↑length) (scale : Scale) : Block Scale Result length

§5.5.2 conversion to a block whose result scale is given as an operand.

def FloatLib.Floats.Formats.P3109.Block.maxAbsFinite {length : ℕ+} (values : Vector (Numerics.NumericalValue ℚ) ↑length) : Numerics.NumericalValue ℚ

Maximum finite absolute value. All-NaN and all-infinite blocks follow closed extrema rules.

def FloatLib.Floats.Formats.P3109.Block.convertToMaxAbsFinite {length : ℕ+} {Scale ScaleExact Source SourceExact Result : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] (scaleDestination : Arithmetic.Destination Scale) (destination : Arithmetic.Destination Result) (scalePolicy : ProjectionPolicy) (policy : BlockPolicy length) (values : Vector Source ↑length) : Block Scale Result length

§5.5.3 select a scale by projecting the maximum finite magnitude, then normalize every lane.

def FloatLib.Floats.Formats.P3109.Block.sumExact {length : ℕ+} (values : Vector (Numerics.NumericalValue ℚ) ↑length) : Numerics.NumericalValue ℚ

Ordered exact closed sum, with a zero identity and no intermediate projections.

def FloatLib.Floats.Formats.P3109.Block.productExact {length : ℕ+} (values : Vector (Numerics.NumericalValue ℚ) ↑length) : Numerics.NumericalValue ℚ

Ordered exact closed product, with a one identity and no intermediate projections.

def FloatLib.Floats.Formats.P3109.Block.reduceAdd {length : ℕ+} {Scale ScaleExact Source SourceExact Result : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] (destination : Arithmetic.Destination Result) (policy : ProjectionPolicy) (block : Block Scale Source length) : Result

§5.6.1 sum every decoded lane and project the complete sum once.

def FloatLib.Floats.Formats.P3109.Block.reduceMultiply {length : ℕ+} {Scale ScaleExact Source SourceExact Result : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] (destination : Arithmetic.Destination Result) (policy : ProjectionPolicy) (block : Block Scale Source length) : Result

§5.6.1 multiply every decoded lane and project the complete product once.

def FloatLib.Floats.Formats.P3109.Block.dotExact {length : ℕ+} {Scale ScaleExact Source SourceExact : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] {RightScale RightScaleExact Right RightExact : Type} [ExecFloat.ExactDecoder RightScale RightScaleExact] [ExecFloat.ExactMap RightScaleExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] (left : Block Scale Source length) (right : Block RightScale Right length) : Numerics.NumericalValue ℚ

Exact §5.6.2 dot product of independently scaled blocks, including closed exceptional rules.

def FloatLib.Floats.Formats.P3109.Block.dotProduct {length : ℕ+} {Scale ScaleExact Source SourceExact Result : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] {RightScale RightScaleExact Right RightExact : Type} [ExecFloat.ExactDecoder RightScale RightScaleExact] [ExecFloat.ExactMap RightScaleExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] (destination : Arithmetic.Destination Result) (policy : ProjectionPolicy) (left : Block Scale Source length) (right : Block RightScale Right length) : Result

Project a complete block dot product once, with no rounded lane product or partial sum.

def FloatLib.Floats.Formats.P3109.Block.unary {length : ℕ+} {Scale ScaleExact Source SourceExact Result : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] {RightScale RightScaleExact : Type} [ExecFloat.ExactDecoder RightScale RightScaleExact] [ExecFloat.ExactMap RightScaleExact ℚ] (destination : Arithmetic.Destination Result) (policy : BlockPolicy length) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (block : Block Scale Source length) (resultScale : RightScale) : Block RightScale Result length

§5.7 unary elementwise operation, followed by normalization at a given result scale.

def FloatLib.Floats.Formats.P3109.Block.binary {length : ℕ+} {Scale ScaleExact Source SourceExact Result : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] {RightScale RightScaleExact Right RightExact : Type} [ExecFloat.ExactDecoder RightScale RightScaleExact] [ExecFloat.ExactMap RightScaleExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] {ResultScale ResultScaleExact : Type} [ExecFloat.ExactDecoder ResultScale ResultScaleExact] [ExecFloat.ExactMap ResultScaleExact ℚ] (destination : Arithmetic.Destination Result) (policy : BlockPolicy length) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : Block Scale Source length) (right : Block RightScale Right length) (resultScale : ResultScale) : Block ResultScale Result length

§5.7 binary elementwise operation on independent source scales and element formats.

def FloatLib.Floats.Formats.P3109.Block.ternary {length : ℕ+} {Scale ScaleExact Source SourceExact Result : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] {RightScale RightScaleExact Right RightExact : Type} [ExecFloat.ExactDecoder RightScale RightScaleExact] [ExecFloat.ExactMap RightScaleExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] {ResultScale ResultScaleExact : Type} [ExecFloat.ExactDecoder ResultScale ResultScaleExact] [ExecFloat.ExactMap ResultScaleExact ℚ] {ThirdScale ThirdScaleExact Third ThirdExact : Type} [ExecFloat.ExactDecoder ThirdScale ThirdScaleExact] [ExecFloat.ExactMap ThirdScaleExact ℚ] [ExecFloat.ExactDecoder Third ThirdExact] [ExecFloat.ExactMap ThirdExact ℚ] (destination : Arithmetic.Destination Result) (policy : BlockPolicy length) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : Block Scale Source length) (right : Block RightScale Right length) (third : Block ThirdScale Third length) (resultScale : ResultScale) : Block ResultScale Result length

§5.7 ternary elementwise operation, retaining the full exact expression until projection.