Semantics of P3109 blocks

Lane projection refines the report's exact normalization followed by destination projection. The special scale laws cover NaN precedence and zero and infinite result scales. Finite reductions keep the whole rational sum or product, with no intermediate rounding.

@[simp]

theorem FloatLib.Floats.Formats.P3109.BlockPolicy.at_stochasticA {length : ℕ+} (width : ℕ) (words : Vector (BitVec width) ↑length) (saturation : SaturationMode) (lane : Fin ↑length) : ({ rounding := BlockRounding.stochasticA width words, saturation := saturation }.at lane).rounding = RoundingMode.stochasticA { width := width, bits := words[↑lane] }

Each lane takes its own word from a block's stochastic rounding words.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Block.normalize_finite (scale value : ℚ) (hscale : scale ≠ 0) : normalize (Numerics.NumericalValue.finite scale) (Numerics.NumericalValue.finite value) = Numerics.NumericalValue.finite (value / scale)

A finite nonzero scale normalizes a finite value by exact division.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Block.normalize_exceptional (scale : Numerics.NumericalValue ℚ) (kind : Numerics.ExceptionalValue) : normalize scale (Numerics.NumericalValue.exceptional kind) = Arithmetic.nan

NaN inputs take precedence even when the result scale is zero.

theorem FloatLib.Floats.Formats.P3109.Block.normalize_zero (value : Numerics.NumericalValue ℚ) (hvalue : ∀ (kind : Numerics.ExceptionalValue), value ≠ Numerics.NumericalValue.exceptional kind) : normalize (Numerics.NumericalValue.finite 0) value = Numerics.NumericalValue.finite 0

A non-NaN input normalized at a zero scale becomes zero, including either infinity.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Block.normalize_infinite_finite (negative : Bool) (value : ℚ) : normalize (Numerics.NumericalValue.infinity negative) (Numerics.NumericalValue.finite value) = Numerics.NumericalValue.finite ((if negative = true then -1 else 1) * if value = 0 then 0 else if value < 0 then -1 else 1)

Infinite scales reduce a finite input to its sign and the scale's sign.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Block.sumExact_finite {length : ℕ+} (values : Vector ℚ ↑length) : sumExact (Vector.map Numerics.NumericalValue.finite values) = Numerics.NumericalValue.finite (List.foldl (fun (x1 x2 : ℚ) => x1 + x2) 0 values.toList)

Finite sum reduction is the exact rational sum with zero identity.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Block.productExact_finite {length : ℕ+} (values : Vector ℚ ↑length) : productExact (Vector.map Numerics.NumericalValue.finite values) = Numerics.NumericalValue.finite (List.foldl (fun (x1 x2 : ℚ) => x1 * x2) 1 values.toList)

Finite product reduction is the exact rational product with one identity.

theorem FloatLib.Floats.Formats.P3109.Block.decode_lane_finite {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) (lane : Fin ↑length) (scale value : ℚ) (hscale : Arithmetic.Mixed.decode block.scale = Numerics.NumericalValue.finite scale) (hvalue : Arithmetic.Mixed.decode block.values[↑lane] = Numerics.NumericalValue.finite value) : block.decode[↑lane] = Numerics.NumericalValue.finite (scale * value)

Decoding a finite lane multiplies the exact source scale and element.

theorem FloatLib.Floats.Formats.P3109.Block.decode_project_lane {length : ℕ+} {Scale ScaleExact : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] (format : Format) (policy : BlockPolicy length) (scale : Scale) (values : Vector (Numerics.NumericalValue ℚ) ↑length) (lane : Fin ↑length) : Format.SameDatum (project (Arithmetic.Destination.p3109 format) policy scale values)[↑lane].decode (format.projectRatValue (policy.at lane) (normalize (Arithmetic.Mixed.decode scale) values[↑lane]))

Every P3109 destination lane refines the exact normalized report projection.

theorem FloatLib.Floats.Formats.P3109.Block.decode_convertFrom_lane {length : ℕ+} {Scale ScaleExact Source SourceExact : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] (format : Format) (policy : BlockPolicy length) (block : Block Scale Source length) (lane : Fin ↑length) : Format.SameDatum (convertFrom (Arithmetic.Destination.p3109 format) policy block)[↑lane].decode (format.projectRatValue (policy.at lane) block.decode[↑lane])

Conversion out projects the decoded scaled datum of each lane once.

@[simp]

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

Conversion to a block keeps the given result scale unchanged.

theorem FloatLib.Floats.Formats.P3109.Block.decode_reduceAdd {length : ℕ+} {Scale ScaleExact Source SourceExact : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] (format : Format) (policy : ProjectionPolicy) (block : Block Scale Source length) : Format.SameDatum (reduceAdd (Arithmetic.Destination.p3109 format) policy block).decode (format.projectRatValue policy (sumExact block.decode))

P3109 sum reduction refines one projection of the complete exact sum.

theorem FloatLib.Floats.Formats.P3109.Block.decode_reduceMultiply {length : ℕ+} {Scale ScaleExact Source SourceExact : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] (format : Format) (policy : ProjectionPolicy) (block : Block Scale Source length) : Format.SameDatum (reduceMultiply (Arithmetic.Destination.p3109 format) policy block).decode (format.projectRatValue policy (productExact block.decode))

P3109 product reduction refines one projection of the complete exact product.

theorem FloatLib.Floats.Formats.P3109.Block.dotExact_finite {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) (x y : Vector ℚ ↑length) (hx : left.decode = Vector.map Numerics.NumericalValue.finite x) (hy : right.decode = Vector.map Numerics.NumericalValue.finite y) : left.dotExact right = Numerics.NumericalValue.finite (List.foldl (fun (x1 x2 : ℚ) => x1 + x2) 0 (Vector.ofFn fun (lane : Fin ↑length) => x[↑lane] * y[↑lane]).toList)

A finite dot product of independently scaled blocks is the rational sum of lane products.

theorem FloatLib.Floats.Formats.P3109.Block.decode_dotProduct {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 ℚ] (format : Format) (policy : ProjectionPolicy) (left : Block Scale Source length) (right : Block RightScale Right length) : Format.SameDatum (dotProduct (Arithmetic.Destination.p3109 format) policy left right).decode (format.projectRatValue policy (left.dotExact right))

A dot product of independently scaled blocks refines one projection of the exact dot product.