1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
// CONTRACT: f16-conversion-v1.yaml
// HASH: sha256:f2a3b4c5d6e78901
// Generated by: pv probar --binding
// DO NOT EDIT — regenerate with `pv probar --binding`
use proptest::prelude::*;
/// Convert F16 bits to F32 bits via IEEE 754 bias trick (for normal f16).
/// f32_bits = (sign << 31) | ((exp_f16 + 112) << 23) | (mantissa << 13)
fn f16_to_f32_bits(h: u16) -> u32 {
let sign = ((h >> 15) & 1) as u32;
let exp = ((h >> 10) & 0x1F) as u32;
let mant = (h & 0x3FF) as u32;
if exp == 0 {
// Subnormal or zero — return signed zero for simplicity
sign << 31
} else if exp == 31 {
// Inf or NaN
(sign << 31) | (0xFF << 23) | (mant << 13)
} else {
// Normal: bias shift 127 - 15 = 112
(sign << 31) | ((exp + 112) << 23) | (mant << 13)
}
}
/// Convert F32 bits back to F16 bits (truncating mantissa).
fn f32_to_f16_bits(f: u32) -> u16 {
let sign = ((f >> 31) & 1) as u16;
let exp = ((f >> 23) & 0xFF) as i32;
let mant = f & 0x7F_FFFF; // keep as u32 — 23-bit mantissa
if exp == 0xFF {
// Inf or NaN
(sign << 15) | (0x1F << 10) | ((mant >> 13) as u16 & 0x3FF)
} else if exp < 113 {
// Too small for f16 normal — flush to zero
sign << 15
} else if exp > 142 {
// Too large for f16 — clamp to inf
(sign << 15) | (0x1F << 10)
} else {
// Normal range: reverse bias shift
let f16_exp = (exp - 112) as u16;
(sign << 15) | (f16_exp << 10) | ((mant >> 13) as u16 & 0x3FF)
}
}
proptest! {
/// Obligation: Bias trick correctness (equivalence)
/// Formal: f16_to_f32 via bit manipulation matches Rust f32 conversion
#[test]
fn prop_bias_trick(
exp in 1u16..31, // Normal exponents only
mant in 0u16..1024, // 10-bit mantissa
sign in 0u16..2
) {
let h = (sign << 15) | (exp << 10) | mant;
let f32_bits = f16_to_f32_bits(h);
let f32_val = f32::from_bits(f32_bits);
// Verify sign preservation
let expected_sign = if sign == 1 { -1.0f32 } else { 1.0f32 };
prop_assert!(
f32_val.signum() == expected_sign || f32_val == 0.0,
"sign mismatch: h=0x{:04X}, f32={}", h, f32_val
);
// Verify finite
prop_assert!(
f32_val.is_finite(),
"non-finite f32 from normal f16: h=0x{:04X}, f32={}", h, f32_val
);
}
/// Obligation: Roundtrip identity (invariant)
/// Formal: f32_to_f16(f16_to_f32(h)) == h for normal f16
#[test]
fn prop_roundtrip(
exp in 1u16..31, // Normal exponents only
mant in 0u16..1024,
sign in 0u16..2
) {
let h = (sign << 15) | (exp << 10) | mant;
let f32_bits = f16_to_f32_bits(h);
let roundtrip = f32_to_f16_bits(f32_bits);
prop_assert_eq!(
roundtrip, h,
"roundtrip failed: h=0x{:04X} -> f32=0x{:08X} -> h=0x{:04X}",
h, f32_bits, roundtrip
);
}
/// Obligation: Sign preservation (invariant)
/// Formal: sign(f16_to_f32(h)) == sign(h)
#[test]
fn prop_sign_preserved(
exp in 1u16..31,
mant in 0u16..1024
) {
// Positive
let h_pos = (0u16 << 15) | (exp << 10) | mant;
let f32_pos = f32::from_bits(f16_to_f32_bits(h_pos));
prop_assert!(
f32_pos > 0.0,
"positive f16=0x{:04X} produced non-positive f32={}", h_pos, f32_pos
);
// Negative
let h_neg = (1u16 << 15) | (exp << 10) | mant;
let f32_neg = f32::from_bits(f16_to_f32_bits(h_neg));
prop_assert!(
f32_neg < 0.0,
"negative f16=0x{:04X} produced non-negative f32={}", h_neg, f32_neg
);
}
/// Obligation: SIMD conversion equivalence (equivalence)
#[test]
#[ignore = "SIMD equivalence — trueno domain"]
fn prop_simd_equivalence(
_x in proptest::collection::vec(0u16..=0x7BFF, 1..32usize)
) {
// SIMD equivalence testing is trueno's responsibility
}
}