Library
ff-ieee-754
Modules
19
Total LOC
3,390
Used by
none in bundle
Deps
cubical-0.9
A stroke-only plate reads from the dimensioned binary word at top through the circular exact decoder to the representable-value and rounding scales below. Shape and line weight, independent of color, distinguish the left-hand zero, subnormal, normal, infinity, and NaN fan; the normal boundary, finite-to-infinity transition, lower and upper candidates, five rounding detents, tininess probe, and five exception traces remain visible.
IEEE 754 encoding, exact decoding, and rounding technical plate

ff-IEEE-754

repository URL pending

Scope

ff-ieee-754 formalizes binary IEEE 754 encodings and their mathematical meanings in safe cubical Agda. Its format layer describes parameterized binary interchange formats, their sign, exponent, and trailing-significand fields, and the corresponding bit-vector operations. Classification and representation modules distinguish zeros, subnormals, normals, infinities, and quiet or signaling NaNs while recording evidence about their bit patterns. Exact and finite-decoding modules relate encodings to signed rational values and connect the implemented decoder with declarative decoding specifications. Range, representability, rational-order, and rounding modules develop the finite value bounds and the selection rules needed to state rounding behavior and exception outcomes.

Most important results

The library provides an exact decoder from binary encodings to semantic IEEE values and proves that its output satisfies a case-by-case decoding specification. It proves the soundness of exponent and full-value classification, linking computed classes to structural evidence about the encoded fields. It establishes representability and ordering facts for landmark values including the least positive subnormal, the normal boundary, and the maximum finite magnitude across the standard binary formats. Its rounding specification covers exact results, nearest-even and nearest-away choices, directed rounding, overflow to infinity, tininess, and the associated exception flags.

Library modules

19 checked modules

Select a module to inspect its generated Agda source view.

Skip to content

Agda libraries

ff-IEEE-754

Cubical Agda foundations for IEEE-754 binary representation, decoding, finite-value semantics, and rounding specifications.

Library
ff-ieee-754
Modules
19
Total LOC
3390
Dependencies
cubical-0.9
IEEE 754 encoding, exact decoding, and rounding technical plateA stroke-only plate reads from the dimensioned binary word at top through the circular exact decoder to the representable-value and rounding scales below. Shape and line weight, independent of color, distinguish the left-hand zero, subnormal, normal, infinity, and NaN fan; the normal boundary, finite-to-infinity transition, lower and upper candidates, five rounding detents, tininess probe, and five exception traces remain visible.
A stroke-only plate reads from the dimensioned binary word at top through the circular exact decoder to the representable-value and rounding scales below. Shape and line weight, independent of color, distinguish the left-hand zero, subnormal, normal, infinity, and NaN fan; the normal boundary, finite-to-infinity transition, lower and upper candidates, five rounding detents, tininess probe, and five exception traces remain visible.
OverviewModulesArticle

Scope

ff-ieee-754 formalizes binary IEEE 754 encodings and their mathematical meanings in safe cubical Agda. Its format layer describes parameterized binary interchange formats, their sign, exponent, and trailing-significand fields, and the corresponding bit-vector operations. Classification and representation modules distinguish zeros, subnormals, normals, infinities, and quiet or signaling NaNs while recording evidence about their bit patterns. Exact and finite-decoding modules relate encodings to signed rational values and connect the implemented decoder with declarative decoding specifications. Range, representability, rational-order, and rounding modules develop the finite value bounds and the selection rules needed to state rounding behavior and exception outcomes.

Most important results

The library provides an exact decoder from binary encodings to semantic IEEE values and proves that its output satisfies a case-by-case decoding specification. It proves the soundness of exponent and full-value classification, linking computed classes to structural evidence about the encoded fields. It establishes representability and ordering facts for landmark values including the least positive subnormal, the normal boundary, and the maximum finite magnitude across the standard binary formats. Its rounding specification covers exact results, nearest-even and nearest-away choices, directed rounding, overflow to infinity, tininess, and the associated exception flags.

Source browser

Modules

Read the full library article

ff-IEEE-754 is a Cubical Agda formalization of IEEE-754 binary interchange representation and decoding.

The current milestone is a checked foundation, not a full arithmetic implementation. It establishes representation, classification, exact rational decoding, textbook finite-value bridges, representability, endpoint ranges, and relation-level vocabulary for future rounding and exception-flag specifications.

Current Scope

The library covers:

  • binary16, binary32, binary64, and binary128 format parameters;
  • bit-level binary encodings over Cubical.Data.Vec;
  • sign, exponent, significand, zero, subnormal, normal, infinity, and NaN classification;
  • rounding-direction and exception-flag vocabularies;
  • MSB-first bit-vector interpretation and exponent bias constants;
  • exact rational decoding for zero, subnormal, and normal encodings;
  • finite decoded values with sign separated from nonnegative rational magnitude;
  • textbook finite-value formulas for subnormals and normals;
  • soundness, completeness, and uniqueness of decodeValue relative to decode specs;
  • endpoint definitions for least subnormal, greatest subnormal, least normal, and greatest finite normal magnitudes;
  • positive-subnormal interval theorems;
  • a rounding-relation skeleton for exact rational inputs, candidate encodings, directed modes, nearest-mode hooks, tininess, overflow, and derived flags;
  • checked binary16 examples for zero, one, infinity, quiet NaN, and bridge corollaries.

Claim Discipline

The honest public claim is:

Mechanically checked representation and decoding correctness for IEEE-754
binary interchange encodings, including a textbook finite-value bridge and
a finite representability layer, plus checked relation-level vocabulary for
future rounding and exception-flag specifications.

Do not present this page as full IEEE-754 conformance or complete arithmetic. That work is intentionally listed as future milestones: concrete rounding, operation specs, flag behavior, NaN propagation, signed zero behavior, and full finite range theorems.

How It Fits

ff-IEEE-754 is useful precisely because it makes the checked boundary visible: representation and decoding correctness now, future arithmetic and conformance only after more proof work.

Floating point is a place where ordinary software hides precision under familiar syntax. A number looks like a number, but the actual artifact is a binary interchange encoding with a sign bit, exponent field, significand field, reserved representations, rounding rules, and exception behavior.

ff-IEEE-754 begins at that boundary. It connects bit-level encodings to exact rational decoding, finite-value specifications, textbook equations, representability, endpoint ranges, and rounding vocabulary.

The honest public claim is representation and decoding correctness for IEEE-754 binary interchange encodings, plus a textbook finite-value bridge, finite representability work, endpoint-range foundations, and relation-level vocabulary for future rounding and flags.

The library does not claim full IEEE-754 conformance or complete arithmetic. That visible boundary is part of the value: formalization shows exactly where the checked line currently is and what remains to be proved.

Browse modulesOpen generated Agda sources

Cabinet index

Explore Formal Foundry

Book a meeting Explore libraries

Trusted systems. Mathematical proofs.

Search the archive

Find a page

Type to search the published content.