From fc944c1bfeea06b4720af0bfeed2f7488eb2d31b Mon Sep 17 00:00:00 2001 From: Emily Boudreaux Date: Thu, 17 Sep 2026 09:35:59 -0400 Subject: [PATCH] Enforce floating arithmetic prerequisites for polynomial certificates --- .../POLYNOMIAL_ENTHALPY_ADMISSIBILITY_2026-09-17.md | 2 ++ .../interface/solver/enthalpy_admissibility.cppm | 11 +++++++++++ 2 files changed, 13 insertions(+) diff --git a/experiments/POLYNOMIAL_ENTHALPY_ADMISSIBILITY_2026-09-17.md b/experiments/POLYNOMIAL_ENTHALPY_ADMISSIBILITY_2026-09-17.md index ecda41e..8bb5762 100644 --- a/experiments/POLYNOMIAL_ENTHALPY_ADMISSIBILITY_2026-09-17.md +++ b/experiments/POLYNOMIAL_ENTHALPY_ADMISSIBILITY_2026-09-17.md @@ -19,3 +19,5 @@ Tests cover nodal-positive/interior-negative cubics, a positive polynomial with `PreparedStellarEnthalpyStrategy` resolves the enthalpy block from the compiled form type and captures the initial physical enthalpy as its anchor. Every full-state check denormalizes the state; pointwise positivity is not invariant under a general diagonal Riesz normalization. The strategy minimizes the full normalized linear-residual norm over the sufficient one-dimensional repair interval, verifies the actual normalized root candidate after rounding, and rejects a non-descent result. Unrelated blocks of the normalized correction are retained bit for bit. It does not prepare an operator or change an accepted state. A valid unaltered full candidate costs one Jacobian action for its true merit slope; an altered direction costs three actions (family model plus the actual rounded chosen direction). The anchor's certificate is cached only when coefficients agree exactly on every rank. A standalone extraction of the scalar/tensor certification engine was compiled with the system C++20 compiler and exercised before module integration. It certified a strictly positive quadratic with negative coarse coefficients and a three-dimensional zero-face bubble; it proved a negative pocket of depth 1e-10; it returned unresolved for an exact tangential zero. Production module compilation and MPI execution remain part of the integration campaign. + +Arithmetic requirements are enforced at compilation: `__FAST_MATH__` and a positive `__FINITE_MATH_ONLY__` are rejected, and static assertions require IEC 559 binary64 with subnormal support. Runtime floating-point modes must retain gradual underflow; the application must not enable flush-to-zero after construction. The existing Release build was inspected: `-O3 -g -DNDEBUG -std=c++23 -flto=thin -arch arm64`; no unsafe floating-point flags were present in the generated build commands. diff --git a/libmeanfield/interface/solver/enthalpy_admissibility.cppm b/libmeanfield/interface/solver/enthalpy_admissibility.cppm index a8ab6d7..09c63f7 100644 --- a/libmeanfield/interface/solver/enthalpy_admissibility.cppm +++ b/libmeanfield/interface/solver/enthalpy_admissibility.cppm @@ -15,6 +15,12 @@ module; #include #include +// Outward enclosure depends on ordinary floating-point operations. Optimizers +// that discard NaNs or reassociate expressions invalidate the certificate. +#if defined(__FAST_MATH__) || (defined(__FINITE_MATH_ONLY__) && __FINITE_MATH_ONLY__ > 0) +#error "Polynomial enthalpy certification does not support fast-math or finite-math-only compilation." +#endif + export module mean_field:solver.enthalpy_admissibility; export import :field.mfem; @@ -54,6 +60,11 @@ export namespace mean_field::solver { } namespace mean_field::solver::enthalpy_detail { + static_assert(std::numeric_limits::is_iec559 && std::numeric_limits::radix == 2 && + std::numeric_limits::digits == 53 && std::numeric_limits::max_exponent == 1024 && + std::numeric_limits::has_denorm == std::denorm_present, + "Polynomial enthalpy certification requires IEEE 754 binary64 with subnormal support."); + // Bounds concern the represented polynomial, not a tolerance-relaxed EOS. // Exact zero is retained algebraically so a prescribed zero trace does not // become an unresolved negative interval merely through outward rounding.