Rational contracts for bounded fixed point

The bounded carrier denotes the subset of the unbounded fixed-point grid whose coefficients fit the signed storage width. This module defines the mathematical contract for three overflow policies:

• wrapping operations use centered reduction of the exact coefficient;
• checked operations are exact when the destination coefficient fits;
• saturating operations clamp the exact coefficient to the signed destination range.

The executable BitVec kernels live in Bounded.Core. Their refinement proofs are isolated in Semantics.Proof, keeping the contract reusable without importing the proof implementation.

def FloatLib.Floats.Formats.FixedPoint.Bounded.valueOfCoefficient (radix : Numerics.Radix) (fractionalDigits : ℕ) (value : ℤ) : ℚ

Rational value represented by an integer coefficient at one fixed scale.

def FloatLib.Floats.Formats.FixedPoint.Bounded.coefficientOf (radix : Numerics.Radix) (fractionalDigits : ℕ) (value : ℚ) : ℤ

Recover the nearest integer coefficient of a rational scalar at one fixed scale.

This is exact on every scalar represented by the bounded fixed-point system.

def FloatLib.Floats.Formats.FixedPoint.Bounded.wrapAddValue (radix : Numerics.Radix) (fractionalDigits width : ℕ) (left right : ℚ) : ℚ

Wrapping same-scale addition on scalar values.

def FloatLib.Floats.Formats.FixedPoint.Bounded.wrapSubValue (radix : Numerics.Radix) (fractionalDigits width : ℕ) (left right : ℚ) : ℚ

Wrapping same-scale subtraction on scalar values.

def FloatLib.Floats.Formats.FixedPoint.Bounded.wrapMulValue (radix : Numerics.Radix) (p q outWidth : ℕ) (left right : ℚ) : ℚ

Wrapping multiplication on scalar values at the composed output scale.

def FloatLib.Floats.Formats.FixedPoint.Bounded.saturatingAddValue (radix : Numerics.Radix) (fractionalDigits width : ℕ) (left right : ℚ) : ℚ

Saturating same-scale addition on scalar values.

def FloatLib.Floats.Formats.FixedPoint.Bounded.saturatingSubValue (radix : Numerics.Radix) (fractionalDigits width : ℕ) (left right : ℚ) : ℚ

Saturating same-scale subtraction on scalar values.

def FloatLib.Floats.Formats.FixedPoint.Bounded.saturatingMulValue (radix : Numerics.Radix) (p q outWidth : ℕ) (left right : ℚ) : ℚ

Saturating multiplication on scalar values at the composed output scale.

@[inline]

def FloatLib.Floats.Formats.FixedPoint.Bounded.toUnbounded {radix : Numerics.Radix} {fractionalDigits width : ℕ} (code : Code radix fractionalDigits width) : FixedPoint.Code radix fractionalDigits

Forgetting the coefficient bound yields the corresponding exact fixed-point code.

def FloatLib.Floats.Formats.FixedPoint.Bounded.numericalSystem (radix : Numerics.Radix) (fractionalDigits width : ℕ) : Numerics.NumericalSystem

Bounded fixed point interpreted as an exact rational numerical system.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.FixedPoint.Bounded.At (radix : Numerics.Radix) (fractionalDigits width : ℕ) (value : Numerics.NumericalValue ℚ) : Type

A bounded code with an erased proof of its complete denotation.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.FixedPoint.Bounded.AtFinite (radix : Numerics.Radix) (fractionalDigits width : ℕ) (value : ℚ) : Type

A bounded code with an erased proof of its exact rational value.