BugZoo: floating-point trust boundaries

Floating point is not a cosmetic implementation detail. Robustness and equivalence proofs over real numbers can become unsound when the deployed network runs with finite precision, fused operations, different reduction order, denorm/flush behavior, or backend-specific kernels.

The key warning paper is:

• Jia and Rinard, “Exploiting Verified Neural Networks via Floating Point Numerical Error”, IEEE S&P Workshops 2020. https://doi.org/10.1109/SPW50608.2020.00058

Core Float32 arithmetic has a logical definition through Float32.Model. FloatLib connects that model to its configured software arithmetic. Its add/sub bridge requires finite operands; its square-root bridge covers every input after NaN canonicalization. Configured division has a total software-model refinement, which does not assert native Float32 division conformance.

Compiled CPU instructions and CUDA kernels still sit beyond that logical equality and require their own backend-conformance evidence.