Skip to content

Commit 4a01295

Browse files
perf(exp10f): record rejected f32 profile route
bd-2g7oyh.383 rejected-restored evidence. Baseline rch vmi1153651: FrankenLibC exp10f p50/mean 607.088/658.606 ns; host glibc p50/mean 478.732/489.702 ns. Candidate proof: piecewise f32+1ULP route passed core exp10f proof and ABI diff_exp10f_within_4_ulps on rch vmi1227854; golden sha256 d8f3d4e893d4683c0a3c0d304c1d548af679d2dbe28dd7bb7fb1f137c74ecdc2. Same-worker decision rch vmi1227854: current-head control p50/mean 258.638/262.987 ns vs candidate 288.310/295.374 ns, regressing p50 11.47% and mean 12.31%; Score 0.0, source restored.
1 parent 67ee00f commit 4a01295

1 file changed

Lines changed: 95 additions & 0 deletions

File tree

Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
# bd-2g7oyh.383 exp10f profile-band f32 route
2+
3+
Date: 2026-06-13
4+
Agent: BoldFalcon
5+
6+
## Target
7+
8+
`glibc_baseline_math/exp10f/` on `[0.5, 2.5)` from the open `bd-2g7oyh.383`
9+
tracker entry. The current implementation already has a f64 table/residual
10+
profile-band kernel, so the tested lever was a structurally different bounded
11+
f32 route:
12+
13+
- keep exact integer `powi` fast path unchanged
14+
- keep out-of-band f64 `exp2` fallback unchanged
15+
- use `libm::exp2f(x * LOG2_10)` in the profile band, with the minimum
16+
correction needed to satisfy the existing 4-ULP contract
17+
18+
## Baseline
19+
20+
Focused baseline before edits, remote rch, worker `vmi1153651`:
21+
22+
- command: `cargo bench -j 1 -p frankenlibc-bench --bench glibc_baseline_bench -- 'glibc_baseline_math/exp10f/' --noplot --sample-size 50 --warm-up-time 1 --measurement-time 3`
23+
- FrankenLibC Criterion: `[636.65 ns 674.25 ns 720.80 ns]`
24+
- FrankenLibC profile row: p50 `607.088 ns`, mean `658.606 ns`
25+
- host glibc Criterion: `[486.47 ns 500.65 ns 516.04 ns]`
26+
- host glibc profile row: p50 `478.732 ns`, mean `489.702 ns`
27+
28+
Same-worker control baseline for the candidate worker, remote rch, worker
29+
`vmi1227854`, clean worktree at `290c2258d`:
30+
31+
- FrankenLibC Criterion: `[262.07 ns 266.64 ns 271.47 ns]`
32+
- FrankenLibC profile row: p50 `258.638 ns`, mean `262.987 ns`
33+
- host glibc Criterion: `[314.44 ns 317.61 ns 320.92 ns]`
34+
- host glibc profile row: p50 `324.839 ns`, mean `324.552 ns`
35+
36+
## Candidate Proof
37+
38+
Raw f32 route failed the 4-ULP contract:
39+
40+
- `exp10f(2.4858856)=306.11557` vs glibc `306.11572`, `5 ULP`
41+
- golden candidate SHA: `3f78266e9d6c4bc648fd6b5001c44c6e315e7e542c3647a7bce48ac179677557`
42+
43+
One-ULP correction still failed:
44+
45+
- `exp10f(2.400743)=251.6187` vs glibc `251.61877`, `5 ULP`
46+
- golden candidate SHA: `c22b8f409c2d486889b8e2f5a2072f9fbf63374acebe15629a66e59e968339d1`
47+
48+
Two-ULP correction overshot:
49+
50+
- `exp10f(1.4659023)=29.234955` vs glibc `29.234945`, `5 ULP`
51+
- golden candidate SHA: `6e5787f5f66f8a9e0e6573a434b1b5afa517242dcc3138193ea13628948d74d2`
52+
53+
Piecewise candidate (`f32+1ULP` below `2.25`, f64 fallback at/above `2.25`)
54+
passed behavior proof:
55+
56+
- core filtered tests on rch `vmi1227854`: `4 passed`
57+
- worst profile-band ULP: `4` at `2.0885048`
58+
- fallback-bit preservation: passed
59+
- ABI/glibc differential: `diff_exp10f_within_4_ulps` passed on rch `vmi1227854`
60+
- golden SHA: `d8f3d4e893d4683c0a3c0d304c1d548af679d2dbe28dd7bb7fb1f137c74ecdc2`
61+
62+
Isomorphism notes:
63+
64+
- exact integer exponents are checked before the profile-band helper, unchanged
65+
- inputs outside `[0.5, 2.5]` use the pre-existing f64 fallback, unchanged
66+
- profile-band FP contract remains <=4 ULP vs glibc for finite f32 inputs
67+
- no ordering, tie-breaking, errno, RNG, or allocation behavior is involved
68+
69+
## Post Benchmark And Decision
70+
71+
Candidate post benchmark, remote rch, worker `vmi1227854`:
72+
73+
- FrankenLibC Criterion: `[252.49 ns 260.94 ns 270.89 ns]`
74+
- FrankenLibC profile row: p50 `288.310 ns`, mean `295.374 ns`
75+
- host glibc Criterion: `[322.44 ns 324.58 ns 327.07 ns]`
76+
- host glibc profile row: p50 `329.398 ns`, mean `337.350 ns`
77+
78+
Same-worker decision:
79+
80+
- control current-head FL p50/mean: `258.638/262.987 ns`
81+
- candidate FL p50/mean: `288.310/295.374 ns`
82+
- result: candidate regressed current-head p50 by `11.47%` and mean by `12.31%`
83+
- Score: `0.0` (`Impact 0 x Confidence 5 / Effort 2`)
84+
85+
Rejected and restored. `git diff -- crates/frankenlibc-core/src/math/float32.rs
86+
crates/frankenlibc-abi/tests/conformance_diff_math.rs` is empty after restore.
87+
88+
## Next Route
89+
90+
Do not retry scalar `exp2f(x * LOG2_10)` nudging in this band. The current f64
91+
table/residual kernel is already faster on the same worker. The next primitive
92+
should be a generated proof-carrying f32 table/minimax kernel with explicit
93+
Remez coefficients and a full error-sign map, or a fused shared exp10f/expf
94+
kernel that removes the remaining libm dependency without relying on post-hoc
95+
ULP nudges.

0 commit comments

Comments
 (0)