vbpf / prevail / 28972716456

87%

push

github

Replace Boost.Multiprecision with a portable int128 (#1189 phase 1) (#1190)

Phase 1 of #1189 (hide Boost from prevail's public headers). num_big.hpp used
boost::multiprecision::int128_t/uint128_t on compilers without a native __int128
(MSVC), which leaked Boost.Multiprecision into the public ABI and forced MSVC
consumers of the installed library to have Boost.

Add a Boost-free 128-bit integer (arith/num_int128.hpp): two-limb unsigned/signed
types with two's-complement semantics matching __int128 exactly (wrap-around
add/sub/mul, truncation-toward-zero div/mod via binary long division, arithmetic
right shift, signed/unsigned compares, narrowing conversions), all constexpr.
GCC/Clang keep using native __int128; the fallback is used only where there is no
builtin. The __builtin_*_overflow paths are now gated on PREVAIL_HAS_NATIVE_INT128
rather than __GNUC__.

Validation:
- test_int128.cpp checks every operation against native __int128 as an oracle
  over a large value/shift matrix (407,992 assertions).
- Built the whole suite with -DPREVAIL_FORCE_CUSTOM_INT128 (custom type used
  throughout the verifier): results are bit-identical to the native build
  (1811 cases, 417,410 assertions, 0 real failures).
- The MSVC (build_windows) CI already compiles and runs this path on the real
  target.

Boost is still a dependency via bitset_domain (dynamic_bitset) and zone_domain/
adapt_sgraph (flat_map), so find_dependency(Boost) stays for now; those are the
remaining #1189 phases.

- num_int128.hpp: include <concepts> (std::integral) and <compare> (operator<=>
  result types) so the installed header compiles standalone rather than relying
  on transitive includes.
- test_int128.cpp: the signed oracle computed a+b / -a / a<<s etc. in signed
  __int128, which is UB on overflow (e.g. -INT128_MIN). Two's-complement add/
  sub/mul/negate/left-shift share the unsigned bit pattern, so compute those
  expectations in unsigned (ua/ub); signed >> and / % stay signed (well-... (continued)

103 of 105 new or added lines in 1 file covered. (98.1%)

9263 of 10695 relevant lines covered (86.61%)

6421158.68 hits per line