Repository navigation
t27b: std.math.pow of an f32 calls a t27 port of Zig's pow.zig, and gf16.t27 passes (Closes #7823) - #8167
Conversation
…f16.t27 passes (Closes #7823) libm.t27 ports std/math/pow.zig for f32 with its frexp and ldexp; libm_plan.t27 plans std.math.pow, whose first operand names the float type. The conformance spec holds the port to Zig's pow bit for bit. With it, specs/numeric/gf16.t27 passes under t27b, 201 of 201 tests: the last step of #7746. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
AGENTS.md takes master's remainder line and adds this PR's entry, re-measured with wc -l on the merge; the ledger takes master's rows and this PR's two. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
Held. Owner rule, restated 2026-10-09 (translated): "t27b must be generated entirely from .t27 specs -- this is the rule!!" AGENTS.md ("t27b is written in t27") already says the hand-written debt only shrinks. This PR adds a net +12 hand-written lines under Rework before merge. In this same PR, port at least 12 lines of the existing hand-written Rust in Prove the port changed nothing with a signed lane receipt. |
…loses #7823) Owner rule 2026-10-09: t27b is generated from .t27 specs, and a PR's hand-written lines under cli/t27b/ are net <= 0. This PR needs no glue: #7819's operand typing lowers std.math.pow already. Its one hand-written addition, a 12-line test in tests/tail.rs, is dropped; conformance/libm_powf.t27 and libm_plan.t27's std_math_pow_of_an_f32_calls_its_port hold the same cases in t27. With no line count moving, AGENTS.md is master's. The ledger takes master's rows and this PR's two. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
Reworked for the owner rule: this PR now changes nothing under |
PR DashboardGenerated at: 2026-10-09 15:04:10 UTC
Summary
Seal Status
|
Closes #7823. With this PR, t27b passes
specs/numeric/gf16.t27, the numeric SSOT of law L6, which is what #7746 asks (see #7746). Part of #6063 (t27b coverage), item C10 of #6488. This is the last PR of #7746's split, after #7791 (#7818), #7819 (#7863) and #7822 (#7918), all merged. It builds on #7923 (#7925) too, which addsstd.math.inf,std.math.log1pand the base-estd.math.logto the same plan.What
t27b now lowers
std.math.pow(f32, x, y)to a call of a t27 port inspecs/tri/t27b/libm.t27:std/math/pow.zig, generic and instantiated at f32. It is not compiler_rt. It comes with the helpers pow uses:frexpandldexp(frexp.zigandldexp.zig) andisOddInteger. It is built on t27b: f32 @floor, @ceil, @round, @trunc and @rem from libm.t27 (compiler_rt floorf, ceilf, roundf, truncf, fmodf) #7819'struncf, t27b: f32 @log, @log2 and @log10 from libm.t27 (compiler_rt logf, log2f, log10f) #7822'slogf, and libm.t27'sexpf.std.math.powjoinsspecs/tri/t27b/libm_plan.t27as builtin 16, after t27b: std.math.inf, std.math.log (base e), std.math.log1p and an f64 @round from libm_plan.t27 (weber_tuning, formats) #7923's three, with three operands. Likestd.math.nanandstd.math.inf, its first operand names its float type, and the other two take that type, as Zig's parametersx: T, y: Tgive it to a literal.operand(POW)is 0, so the glue passesxandy.has_f64now stops atstd.math.log, so an f64 pow is refused.exp,log,frexpandldexpof an f64) is not ported.cli/t27b/(owner rule 2026-10-09: t27b is generated from .t27 specs, and a PR's hand-written lines there are net <= 0). t27b: f32 @floor, @ceil, @round, @trunc and @rem from libm.t27 (compiler_rt floorf, ceilf, roundf, truncf, fmodf) #7819's glue already lowers the operands after the first with the type the plan names, sostd.math.pow(f32, x, 3.0)lowers its literal as an f32. An earlier version of this PR added a 12-line test totests/tail.rs. It is dropped:libm_plan.t27'sstd_math_pow_of_an_f32_calls_its_portandconformance/libm_powf.t27hold the same cases in t27, the literal operands and the f64 refusal included.specs/numeric/gf16.t27passes under t27b: 201 of 201 tests, 465 runtime asserts, 103 invariants held. These are the reference's verdicts:t27c test-reportgives 201/201, with 5 vacuous.What the reference does
Measured on the t27c lab (zig 0.16.0, x86_64 Debug), with Zig probes:
std.math.pow(f32, x, y)is std's generic pow, compiled into the test. In order, it:std.math.nan(f32), 0x7FC00000; y = 1 gives x; then a zero x by the oddness of y, and the infinities;@sqrtfor y = 0.5, and1 / @sqrtfor y = -0.5;exp(y * log(|x|))when the integer part of y is at least 2^31;exp(yf * log(x))for the fraction of y, square-and-multiply onfrexp(x)for its integer part, and oneldexpat the end, which rounds a subnormal result once, ties to even.pow(2, 0.5)is 0x3FB504F3,pow(1.5, 3.3)is 0x4073F05D,pow(2, 127.5)is 0x7F3504F3, andpow(1.0001, 100000)is 0x46ABEB14;pow(2, -149)is the least subnormal, andpow(2, -150)is a tie that goes to 0;pow(3, -80)is 0x0049AB74.std.math.pow(f32, ..)Zig folds at compile time gives the run-time bits, on a 49-point grid.std.math.ldexpof a zero with n > 0 is not a zero.ldexp(-0.0, 40)is 0x88000000. pow never passes a zero toldexp: a1 is a product of significands andexpresults. So pow never shows it. The port does what Zig does, and no test pins it.Decisions, including every float edge case
std.math.nan(f32), 0x7FC00000, on every platform.@sqrtof a negative x has the platform's bits. The port and Zig make it with the same operation on the same machine, so the sweeps agree on x86_64 and on aarch64.Specs
specs/tri/t27b/conformance/libm_powf.t27(new) brings the port in withuse tri::t27b::libm;.exp(y * log(x))path), and powers that over- and underflow;ldexpon its own, against Zig'sstd.math.ldexp. pow gives it only a normal a1, so this test asks the subnormal operands and the ties.t27c test-report--check(aarch64, qemu)conformance/libm_powf.t27(new)libm_plan.t27libm.t27specs/numeric/gf16.t27specs/ml/loss/kl_divergence.t27The three t27b specs are sealed (
t27c seal --save, then--verify: all hashes MATCH).Mutants
Each mutant ran on a copy, under both
t27c test-reportand t27b (qemu).powf,frexp,ldexp,isOddInteger,trunc,clz32libm_plan.t27rowsThe first run killed 20 of the 29. Three tests were then added: the subnormal x, the 2^31 boundary, and
ldexpon its own. The rerun killed:frexp's subnormal exponent and its subnormal shift;clz32starting one bit down;ldexp's subnormal result at< 0.The four survivors under both are equivalent:
y == 1short cut. The general path gives x back exactly: a1 = x1, ae = xe, andldexp(x1, xe)is x.ldexpgives the same infinity or zero.<= 0.5. x1 is 0.5 only when x is a power of two, where every product is exact.ldexp's underflow bound at 24 instead of 23. The rounding path gives 0 there too, because 1.m * 2^-151 is below half the least subnormal.One more survives under t27b only: pow without its NaN for a negative x with a fraction of y.
logf's NaN then carries through. On x86_64 that NaN is 0xFFC00000, and the reference kills the mutant. On aarch64 it is 0x7FC00000, which is the bitsnanfreturns, so the mutant gives the same bits there.Lines (
git diff --numstat --no-renames origin/master...HEAD)gen/rust/tri/t27b/libm_plan.rst27c gen-rust, not hand-editedspecs/tri/t27b/conformance/libm_powf.t27specs/tri/t27b/libm.t27specs/tri/t27b/libm_plan.t27.trinity/seals/*.json(3)t27c seal --save(t27c 0.5.2)docs/reports/t27b_expectations.jsonHand-written lines under
cli/t27b/: net 0. This PR changes no file there (src + tests: +0 / -0).AGENTS.md is master's, because no
wc -lcount moves.Gates
On the t27c lab, on this PR's tree:
cargo test --release -p t27b, on master 8415b2c with this PR: 137 passed, 0 failed on x86_64; 157 passed, 0 failed on aarch64 under qemu.check_assertionless_spec_tests.py: ok.check_seal_coverage.py: OK.dupe_scan.py --likefinds nothing inlibm.t27,libm_plan.t27orlibm_powf.t27that is written elsewhere. The full scan's six errors are master's (ends_block,get_last_blockand four more groups); master alone gives the same six.t27c gen-rustof the plan reproduces the committed file.check_budget()andcheck_all()from master'sown_language.c: exit 0.Ledger
Two rows move:
specs/numeric/gf16.t27goes from blocked (ExprCall(std.*)) to pass.specs/tri/t27b/conformance/libm_powf.t27is new, and passes.On master 8415b2c's ledger, pass rows go 1117 -> 1119, not_pass rows go 21 -> 20, and
max_not_passgoes 21 -> 20.Evidence: signed lane receipts (#7686)
Head 593e9d7 (this PR on master a97cb9e) against base a97cb9e, its merge base.
t27c corpus-receipt compare BASE HEAD --challenge-head <mine>, run on the t27b lab from/work/t27with/work/t27c-master:Exit 3, IMPROVED_ONLY.
cargo test --release -p t27b(aarch64)specs/numeric/gf16.t27: blocked (ExprCall(std.*)) in the base, pass in the head. It runs 201 tests with 465 runtime asserts, with the reference's verdict on every test.conformance/libm_powf.t27is new, and passes: 6 tests, 238 asserts.Commits after 593e9d7. These are merges of master, and one commit that drops the 12-line
tests/tail.rstest for the owner rule above. That test's file is not an input of any lane. On the last merge (master 8415b2c), the lab gives:cargo test: 137 passed on x86_64 and 157 on aarch64, 0 failed;gf16.t27201/201,libm_powf.t276/6,libm_plan.t2712/12 andlibm.t2721/21;gen-rust gaps
None new.
🤖 Generated with Claude Code