feat: M6 — Xtensa FPU emulator proven equal to S3 silicon - #240
Merged
Conversation
The M6 P6 campaign transcribed the toolchain's real divide and square-root sequences (objdump of esp-14.2.0 libgcc/libm — output-as-fact, no source read) and found __ieee754_sqrtf uses mksadj.s, which lp-xt-inst wrongly listed as an unassigned FP1 slot. Decode/encode/disasm/roundtrip/golden added; the emulator classifies and refuses it like the other divide-step helpers until their semantics are measured. Plan: 2026-07-30-1745-f32-native-math/m6-xtensa-fpu-emulator (P6) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… sweeps, helper probes The harness now runs the toolchain's REAL divide and square-root sequences (transcribed from objdump of esp-14.2.0 libgcc __divsf3 / libm __ieee754_sqrtf — output-as-fact) instead of skipping the F5 pseudo-ops; sweeps the estimate ROMs over 15 (sign, exponent) planes including the denormal/inf/NaN classes, with a run cap so a non-step-function plane aborts loudly instead of drowning the capture; and gains a 'helpers' mode: const.s 0..15 plus characterization grids for nexp01/mksadj/mkdadj/addexp/addexpm/maddn/divn (madd.s runs the identical grid as the contrast row). The grids live in lp-xt-fp-vectors::helpers so both sides regenerate them, with their own pinned fingerprint. Host side: fp_capture parses TABLE/T/END-table sweeps (with the same truncation-and-count teardown discipline as the family rows), CONST rows, and the helpers fingerprint. Plan: 2026-07-30-1745-f32-native-math/m6-xtensa-fpu-emulator (P6) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… corner The P6 campaign's implementation half. Every FpPolicy field is now measured with a citation; the full 5630-vector corpus agrees with the desk S3 capture bit for bit — result AND FSR columns, zero divergence — and the captures are committed as boardless replay fixtures. - fp_rom.rs: the three estimate ROMs read off silicon (recip/div shared 128-entry, rsqrt/sqrt odd+even 64-entry; every run of all 60 RLE sweeps reproduces exactly, ~503M points verified exhaustively in release), plus the measured helper semantics: nexp01 (normalize-negate by parity), mksadj/mkdadj (split exponent encoders, floor-halving arithmetic and a result-class channel), addexp/addexpm (pure bit ops), and divn — the reassembly step: 8-bit sign-extended exponent excess decomposed as 8k+p, A = 32k_r + (k_t mod 32), class window at A-384, RNE with exact sticky, +2^(A-50) on exact cancellation. - float_math.rs: FCR.RM is HONORED (F1: 1944/1944 directed-mode rows match IEEE) — directed rounding implemented for add/sub/mul, refused loudly where unmeasured; denormals fully IEEE (no flush either direction); NaN rule last-operand-quieted with acc-first priority for the accumulate ops; utrunc.s negative wrap (RM FALSIFIED); round.s ties-to-even; FSR flags modeled throughout (RM's no-flags claim FALSIFIED). - Corpus: FSR is now a first-class predicted column; goldens promoted with full board provenance; the UNKNOWN guard flipped — zero UNKNOWN rows, and the negative control (corrupted row -> exactly one DIVERGE) proven. - fp_silicon_replay.rs: tables/helpers/families captures replayed on every test run, no board; divn probe agreement pinned at 1387/1536 with the off-envelope remainder documented for the queued round-2 probe grids. Plan: 2026-07-30-1745-f32-native-math/m6-xtensa-fpu-emulator (P6) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The ADR records the measured contract corner by corner — including the two RM falsifications (utrunc.s negatives, FSR flags) — with a Remains Unverified section that states the negative space. Draft: P7 finalizes it after G2. Defect entry for the mksadj.s instruction-model gap the campaign caught. Plan: 2026-07-30-1745-f32-native-math/m6-xtensa-fpu-emulator (P6) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Yona-Appletree
changed the base branch from
claude/f32-m6-p5-campaign-harness
to
main
August 1, 2026 05:45
…P6's stale docs P7 (M6's close-out): the ADR drafted in P6 is now Accepted (G2 passed 2026-08-01) — full header fields, the G2 ratification folded in, the two register/ABI corrections M7's early implementation surfaced (f15 reserved emitter scratch; `!=` maps to oeq.s+movf not ueq.s+movf), and an Alternatives-considered section in house style. docs/design/float.md's denormal row asserted the opposite of what the campaign measured (ESP32-S3 does NOT flush denormals — full IEEE); fixed, and pointed the NaN-bits/round-ties rows at the ADR now that Xtensa has a measured answer for each. lp-xt-emu/README.md, lp-xt-inst/README.md, lp-xt/README.md, lp-xt-fp-vectors/README.md, AGENTS.md, and the fp fixtures READMEs still described the FP work as unproven/in-flight (pre-campaign UNKNOWN counts, "not yet run on hardware", "no FPU executors") — updated to the measured, zero-divergence, G2-passed state, with fp_silicon_replay.rs documented for the first time. Closed a real coverage gap found in the sweep: `mksadj.s` (added by P6, docs/defects/2026-07-31-mksadj-missing-from-fp-subset.md) was never added to the objdiff mechanical-oracle corpus (fp_subset.S), so its encoding sat outside the mechanical check the rest of the subset gets. Added it; objdiff now reports 136/136 matched (was 134/134), zero mismatches. Plan: 2026-07-30-1745-f32-native-math/m6-xtensa-fpu-emulator (P7) Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…r wrapper Cleanup sweep (P7): docs/defects/2026-07-31-mksadj-missing-from-fp-subset.md was filed at fix time but never added to the registry index or given a class-vocabulary entry — added `incomplete-subset` (the class: an external tool's enumerated opcode assignment is wrong, and only the tool's own output falsifies it) and indexed the entry. lp-xt-fp-vectors' helpers::probe2::vector() was unused outside its own definition — the device harness and fp_silicon_replay.rs both call probe2::probe() directly — and its body stuffed a fake `op: HelperOp::DivnS` discriminant with a "placeholder, unused" comment. Removed; the now-unused `use super::HelperVector` import went with it. Plan: 2026-07-30-1745-f32-native-math/m6-xtensa-fpu-emulator (P7) Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…mance harness Small follow-up to the P7 doc pass: the `just fwtest-xt-fp-esp32s3` example block showed family/tables invocations but not `helpers`, even though the harness has supported it since P6 (divide-step helpers + probe2). Plan: 2026-07-30-1745-f32-native-math/m6-xtensa-fpu-emulator (P7) Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Yona-Appletree
changed the title
Yona-Appletree
marked this pull request as ready for review
August 1, 2026 15:09
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Plan: lp2025/2026-07-30-1745-f32-native-math
Path: /Users/yona/.photomancer/planning/lp2025/2026-07-30-1745-f32-native-math/m6-xtensa-fpu-emulator/plan.md (phases P6+P7 — M6 complete)
M6 is done.
lp-xt-emunow executes the Xtensa single-precision FP subsetand every corner of its numeric behavior is either fixed by IEEE-754 or
measured on the desk ESP32-S3, replayed with no board attached, forever.
G2 — PASSED 2026-08-01. Yona: "Yeah I did look at this, I do trust it.
G2 pass." All four leans accepted (emulator matches silicon everywhere on
the corpus incl. FSR; captured vectors sufficient as a regression oracle;
denormals recorded target-defined as full IEEE, no product decision needed;
non-default rounding modes stay refused). Full record in
m6-xtensa-fpu-emulator.md§"Review gate: G2 — PASSED 2026-08-01".P6 — the hardware campaign
mksadj.sadded to lp-xt-inst — the real sqrt sequence uses it; it was wrongly recorded as an unassigned slot (defect filed)lp-xt/lp-xt-emu/tests/fixtures/fp/captures/P7 — ADR, docs, cleanup, PR (this batch)
docs/adr/2026-07-31-xtensa-fp-behavior-contract.md): Status → Accepted, G2 ratification folded in with full header fields (Supersedes/Relates), an Alternatives considered section in house style, and the two register/ABI corrections M7's early implementation (PR feat: hardware float on the S3 — f32 VInsts and Xtensa lowering (M7 P1–P2) #241 P1–P4) surfaced —f15reserved as emitter float scratch (15/16 FRs allocatable, not 16), and!=maps tooeq.s + movf(notueq.s + movf, which is false on NaN)docs/design/float.md§4: the denormal row was asserting the opposite of the measured fact (said Xtensa flushes; it doesn't) — fixed, and the NaN-bits/round-ties rows now point at the ADR's measured answerlp-xt-emu/README.md,lp-xt-inst/README.md,lp-xt/README.md,lp-xt-fp-vectors/README.md,AGENTS.md, and the fp-fixtures READMEs — pre-campaign UNKNOWN counts, "not yet run on hardware", "no FPU executors" all updated to the zero-divergence, G2-passed state;fp_silicon_replay.rsdocumented for the first timemksadj.s(added by P6) was never added to theobjdiffmechanical-oracle corpus (fp_subset.S) — added, objdiff now 136/136 matched (was 134/134); removedlp-xt-fp-vectors's deadprobe2::vector()wrapper; indexed the mksadj defect indocs/defects/README.md(was filed but not indexed) and added theincomplete-subsetclass it neededtest_xt_fp_conformanceis inclippy-fw-esp32s3's per-feature loop, andfp_conformance.rs/fp_silicon_replay.rsrun under plaincargo test -p lp-xt-emu(lp-xt-emuis indefault-members— no feature gate to rot)2026-esp32s3-experiment, separate repo/commit): FINDINGS.md, fixtures/README.md, docs/BACKPORT.md updated to stop claiming FP is unproven repo-wideValidation
cargo test -p lp-xt-inst -p lp-xt-emu -p lp-xt-fp-vectors -p lp-emu-core -p lp-riscv-emuall green (0 failures) ·cargo test -p lp-xt-emu --test fp_conformance --test fp_silicon_replay: 0 UNKNOWN, 5 630/5 630 AGREE, 0 DIVERGE ·cargo test -p lp-xt-fp-vectors18/18 · objdifffp_subset.elf136/136 matched, 0 mismatches ·CI is the validation of record for this push — see checks below.
Resume notes for anyone reading this cold:
p6-campaign-results.mdfirst, thenthe ADR, then
fp_rom.rs's module docs.🤖 Generated with Claude Code