name = "half"
description = "IEEE 754 binary16 (f16) and bfloat16 support — ETNA workload."
language = "rust"
crate = "half"
strategies = ["proptest", "quickcheck", "crabcheck", "hegel"]
base_commit = "bd25b96c3d6ca1133a15cccab6f281f9e1e8cea5"

[[tasks]]
mutations = ["max_min_nan_handling_a61f31b_1"]

[tasks.source]
repo = "https://github.com/VoidStarKat/half-rs"
commits = ["a61f31bace6b63c6d3336a3867b5617976b0653e"]
commit_subjects = ["Fix bug #126: handle NaNs correctly in min() and max()"]
summary = "`f16::max/min` relied on `other > self` to decide which argument to return; when `self` is NaN that comparison is unordered and returned NaN instead of the non-NaN operand, violating IEEE 754 min/max semantics."

[tasks.injection]
kind = "marauders"
files = ["src/binary16.rs"]
locations = [{ file = "src/binary16.rs" }]

[tasks.bug]
short_name = "max_min_nan_handling"
invariant = "For IEEE 754 max/min, if exactly one input is NaN the non-NaN argument must be returned; in particular `NaN.max(x)` must return `x`."
how_triggered = "The buggy body reads `if other > self && !other.is_nan() { other } else { self }`. When `self` is NaN, `other > self` is `false` (any comparison with NaN is unordered), so the code returns `self` (NaN) instead of `other`. The fixed body explicitly checks `self.is_nan()` first."

[[tasks.tasks]]
property = "F16MaxMinNan"
witnesses = [
  { test_fn = "witness_f16_max_min_nan_case_self_nan_max" },
  { test_fn = "witness_f16_max_min_nan_case_self_nan_min" },
  { test_fn = "witness_f16_max_min_nan_case_other_nan_max" },
  { test_fn = "witness_f16_max_min_nan_case_both_nan_max" },
  { test_fn = "witness_f16_max_min_nan_case_non_nan_max" },
]

[[tasks]]
mutations = ["partial_cmp_sign_magnitude_22b5bd6_1"]

[tasks.source]
repo = "https://github.com/VoidStarKat/half-rs"
commits = ["22b5bd6c086d4caf8651bf5b866241ba8ce67407"]
commit_subjects = ["fix comparisons and add some tests"]
summary = "The `PartialOrd`/`PartialEq` impls on `f16` compared raw `u16` bit patterns, which disagrees with IEEE 754 sign-magnitude ordering: `-0.0 != 0.0`, negative numbers compared by magnitude instead of value, and mixed signs ordered wrong."

[tasks.injection]
kind = "patch"
files = ["src/binary16.rs"]
locations = [{ file = "src/binary16.rs" }]
patch = "patches/partial_cmp_sign_magnitude_22b5bd6_1.patch"

[tasks.bug]
short_name = "partial_cmp_sign_magnitude"
invariant = "`f16` comparisons must agree with the equivalent `f32` comparison obtained by `f16::from_bits(x).to_f32().partial_cmp(&y.to_f32())`. Concretely: `-0.0 == 0.0`, `-1.0 > -2.0`, `1.0 > -0.0`."
how_triggered = "The buggy impls use raw `u16` comparison (e.g. `self.0 < other.0`). In sign-magnitude representation this yields the wrong answer whenever (a) both operands are negative (larger magnitude ⇒ larger u16 ⇒ judged greater, but should be smaller) or (b) one operand is `-0.0` vs `+0.0` (different bits ⇒ judged unequal, but should be equal)."

[[tasks.tasks]]
property = "F16OrdSignMagnitude"
witnesses = [
  { test_fn = "witness_f16_ord_sign_magnitude_case_neg_order" },
  { test_fn = "witness_f16_ord_sign_magnitude_case_neg_zero_eq" },
  { test_fn = "witness_f16_ord_sign_magnitude_case_mixed_sign" },
]

[[tasks]]
mutations = ["subnormal_conversion_18e6467_1"]

[tasks.source]
repo = "https://github.com/VoidStarKat/half-rs"
commits = ["18e6467b52f821d21a7179d1da5ac5aded63b3bd"]
commit_subjects = ["hopefully fix subnormals"]
summary = "The software fallback `to_f32_const` reused the normal-number mantissa shift for subnormals, so `f16→f32` subnormals came out off by a power of two; the fix reinstates the subnormal branch that computes `man << (14 + e)` using the mantissa's leading-zero count."

[tasks.injection]
kind = "patch"
files = ["src/binary16/arch.rs"]
locations = [{ file = "src/binary16/arch.rs" }]
patch = "patches/subnormal_conversion_18e6467_1.patch"

[tasks.bug]
short_name = "subnormal_conversion"
invariant = "Every f16 value is exactly representable in f32, so for a subnormal f16 (`exp==0, mant!=0`) the fallback conversion `to_f32_const()` must produce exactly `mant * 2^-24` (with sign)."
how_triggered = "The buggy fallback pre-computes `man = (half_man & 0x03FF) << 13` outside the subnormal branch and reuses that shift for subnormals. The correct subnormal path, restored by the fix, computes `man = (half_man << (14 + e)) & 0x7F_FFFF` where `e` is the leading-zero count; the reused normal shift leaves residual bits that shift the result out of place (off by a factor `(1 + 2^-10)` or similar). Because the property exercises `to_f32_const()` (the software fallback) directly, the bug is detected even on targets with hardware FP16 intrinsics."

[[tasks.tasks]]
property = "F16SubnormalRoundtrip"
witnesses = [
  { test_fn = "witness_f16_subnormal_roundtrip_case_min_positive_subnormal" },
  { test_fn = "witness_f16_subnormal_roundtrip_case_mid_subnormal" },
  { test_fn = "witness_f16_subnormal_roundtrip_case_neg_subnormal" },
]
