Relational quantization specifications

Quantization is not, in general, a function from one scalar to one stored code. A result may depend on a block scale, an exception policy, an entropy stream, a status accumulator, or a format-specific tie rule. Some specifications intentionally permit several results before an implementation fixes one.

Spec Context Exact Result is therefore the relation

Context → Exact → Result → Prop

used to specify these choices. Deterministic reference functions and executable kernels are ordinary functions proved to satisfy the relation.

This separation follows the distinction between representability and rounding used in generic floating-point libraries. In particular, Flocq defines format membership independently from rounding operators; see S. Boldo and G. Melquiond, “Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq,” ARITH 2011, DOI 10.1109/ARITH.2011.40.

@[reducible, inline]

abbrev FloatLib.Numerics.Quantization.Spec (Context : Type u) (Exact : Type v) (Result : Type w) : Type (max (max u v) w)

A context-indexed relation describing the permitted result of quantizing an exact input.

Context, Exact, and Result are deliberately arbitrary. For example, Context may contain a shared exponent or entropy state, while Result may be a code, a code/status pair, or an updated entropy state together with a code.

def FloatLib.Numerics.Quantization.Spec.Implements {Context : Type u} {Exact : Type v} {Result : Type w} (spec : Spec Context Exact Result) (run : Context → Exact → Result) : Prop

An implementation chooses a result permitted by the relational specification.

def FloatLib.Numerics.Quantization.Spec.Total {Context : Type u} {Exact : Type v} {Result : Type w} (spec : Spec Context Exact Result) : Prop

Every context and exact input has at least one permitted result.

def FloatLib.Numerics.Quantization.Spec.Deterministic {Context : Type u} {Exact : Type v} {Result : Type w} (spec : Spec Context Exact Result) : Prop

The relation permits at most one result for each context and exact input.

def FloatLib.Numerics.Quantization.Spec.ofFunction {Context : Type u} {Exact : Type v} {Result : Type w} (reference : Context → Exact → Result) : Spec Context Exact Result

A reference function viewed as a singleton-valued relational specification.

@[simp]

theorem FloatLib.Numerics.Quantization.Spec.implements_ofFunction {Context : Type u} {Exact : Type v} {Result : Type w} (reference : Context → Exact → Result) : (ofFunction reference).Implements reference

The reference function implements its singleton relational specification.

theorem FloatLib.Numerics.Quantization.Spec.total_ofFunction {Context : Type u} {Exact : Type v} {Result : Type w} (reference : Context → Exact → Result) : (ofFunction reference).Total

A singleton relational specification is total.

theorem FloatLib.Numerics.Quantization.Spec.deterministic_ofFunction {Context : Type u} {Exact : Type v} {Result : Type w} (reference : Context → Exact → Result) : (ofFunction reference).Deterministic

A singleton relational specification is deterministic.

def FloatLib.Numerics.Quantization.Spec.mapResult {Context : Type u} {Exact : Type v} {Result : Type w} {MappedResult : Type x} (spec : Spec Context Exact Result) (f : Result → MappedResult) : Spec Context Exact MappedResult

Map every permitted result through a pure post-processing function.

An output is permitted exactly when it is the image of a permitted source result. This is a proposition about the output; it adds no runtime wrapper.

theorem FloatLib.Numerics.Quantization.Spec.implements_mapResult {Context : Type u} {Exact : Type v} {Result : Type w} {MappedResult : Type x} (spec : Spec Context Exact Result) (f : Result → MappedResult) (run : Context → Exact → Result) (implements : spec.Implements run) : (spec.mapResult f).Implements fun (context : Context) (input : Exact) => f (run context input)

Post-processing a conforming implementation preserves conformance.

theorem FloatLib.Numerics.Quantization.Spec.total_mapResult {Context : Type u} {Exact : Type v} {Result : Type w} {MappedResult : Type x} (spec : Spec Context Exact Result) (f : Result → MappedResult) (total : spec.Total) : (spec.mapResult f).Total

Mapping the results of a total relation preserves totality.

theorem FloatLib.Numerics.Quantization.Spec.deterministic_mapResult {Context : Type u} {Exact : Type v} {Result : Type w} {MappedResult : Type x} (spec : Spec Context Exact Result) (f : Result → MappedResult) (deterministic : spec.Deterministic) : (spec.mapResult f).Deterministic

Mapping the unique result of a deterministic relation remains deterministic.

def FloatLib.Numerics.Quantization.Spec.represents {Context : Type u} {Exact : Type v} (system : NumericalSystem) (target : Context → Exact → system.Scalar) : Spec Context Exact system.Code

Relational specification saying that a result code represents the scalar selected by target.

This is the bridge from context-dependent rounding to the common NumericalSystem representability predicate.

theorem FloatLib.Numerics.Quantization.Spec.implements_represents_iff {Context : Type u} {Exact : Type v} (system : NumericalSystem) (target : Context → Exact → system.Scalar) (run : Context → Exact → system.Code) : (represents system target).Implements run ↔ ∀ (context : Context) (input : Exact), system.Represents (run context input) (target context input)

A code-valued kernel implements represents exactly when every result represents its target.