ADR-0014: Narrow exact-to-floating refinement contract¶

Status: accepted Date: 2026-08-29

Decision¶

The implemented refinement profiles are limited to NumPy and CPU PyTorch float64, frozen finite IEEE inputs/weights interpreted as exact dyadic rationals, and elementwise add, subtract, multiply, and direct divide. Pure sign observation, projective normalization, and typed decoding require specialized result validators and remain outside the advertised profile until those validators exist. It records payload bounds and status-preservation obligations separately.

Ambiguity, overflow, unsupported operations, and refusal are typed outcomes. Inputs and outputs separately record machine zero, subnormal, underflow-to-zero, and non-finite events without converting those events to exact bottom. Strict masked-gradient and surrogate-gradient metadata are different profiles; a surrogate claim must name its objective and boundary behavior. Transcendental trunks are refused rather than described as exact compilation.

Consequences¶

The bridge can support one bounded, tested correspondence statement. It does not generalize to arbitrary Python, Torch, ONNX, hardware, learned models, or compiler correctness.