feat: M6 — Xtensa FPU emulator proven equal to S3 silicon

AGENTS.md

@@ -208,16 +208,26 @@ is the additive `emu-xt` feature behind the `xtn.q32` / `xtlpn.q32` filetest
 targets; it needs a cross-compiled builtins image
 (`scripts/build-builtins-xt.sh`, esp toolchain) and skips loudly without one.
 
-**Xtensa floating point is a separate, in-flight campaign (M6).** `lp-xt-inst`
-encodes the FP subset and `lp-xt-emu` executes it behind an explicit policy layer
-where every corner IEEE-754 does not fix is either cited to the ISA Reference
-Manual or `Unknown` — and **reading an `Unknown` panics** rather than guessing.
+**Xtensa floating point is proven equal to real ESP32-S3 silicon (M6, G2
+passed 2026-08-01).** `lp-xt-inst` encodes the FP subset and `lp-xt-emu`
+executes it behind an explicit policy layer where every corner IEEE-754 does
+not fix is either measured (cited to the ISA Reference Manual, silicon-
+confirmed, or silicon alone) or `Unknown` — and **reading an `Unknown`
+panics** rather than guessing. All 17 policy fields are now measured; the
+behavior contract, corner by corner with its proving vector family, is
+`docs/adr/2026-07-31-xtensa-fp-behavior-contract.md`.
 `cargo test -p lp-xt-emu --test fp_conformance` replays the whole 5 630-vector
-corpus with no board attached; `just fwtest-xt-fp-esp32s3 <port>` runs the same
-vectors on a desk S3 and `just fp-diff <capture>` classifies the answers. The
-predictions were committed before any hardware ran, so **a device disagreement is
-a finding to triage, never a reason to edit a golden**. Do not resolve a policy
-field without a citation naming a manual page or a dated desk session.
+corpus with no board attached and asserts **zero** `UNKNOWN` rows;
+`cargo test -p lp-xt-emu --test fp_silicon_replay` replays the campaign's own
+silicon captures (ROM sweeps, helper probes, the full family diff) with no
+board attached either — that pair is what makes "the emulator is trusted"
+something CI enforces on every commit. `just fwtest-xt-fp-esp32s3 <port>` runs
+the same vectors on a desk S3 and `just fp-diff <capture>` classifies the
+answers, for the rare case the contract itself needs re-checking. The
+predictions were committed before any hardware ran, so **a device
+disagreement is a finding to triage, never a reason to edit a golden**. Do
+not resolve a policy field without a citation naming a manual page or a dated
+desk session.
 
 > **`regalloc/` is shared by both ISAs, and rv32 passing does not prove it
 > correct.** Two defects landed there in 2026-07 that were correct on rv32 only

docs/defects/2026-07-31-mksadj-missing-from-fp-subset.md

@@ -0,0 +1,42 @@
+---
+status: fixed
+found: 2026-07-31      # how: M6 P6 hardware campaign (sequence transcription)
+fixed: this change
+area: lp-xt/lp-xt-inst
+class: incomplete-subset
+related:
+  - docs/adr/2026-07-31-xtensa-fp-behavior-contract.md
+---
+# `mksadj.s` was recorded as an unassigned slot, so the sqrt sequence could not decode
+
+**Symptom** — Transcribing the toolchain's real square-root sequence
+(`__ieee754_sqrtf`, esp-14.2.0 libm, read via `xtensa-esp32s3-elf-objdump`)
+for the M6 P6 campaign hit an instruction the P1 normative subset did not
+contain: `0xfa21c0`, which objdump disassembles as `mksadj.s f2, f1`. The
+emulator could not execute the sequence at all — every square root would have
+raised an unsupported-instruction trap at its 23rd instruction.
+
+**Root cause** — `lp-xt-inst`'s FP1 unary decode table carried a comment (and
+a test, `fp1_unassigned_slots_stay_unsupported`) asserting that selector
+`t = 0xC` "has no mnemonic in `xtensa-esp32s3-elf-objdump`". That was wrong:
+objdump assigns it `mksadj.s`, the square-root counterpart of `mkdadj.s`. The
+P1 probe list was assembled from the divide-sequence shape and never included
+a square-root sequence, so the gap survived P1's silicon session — presence
+was probed for 26 instructions and `mksadj.s` was not one of them.
+
+**Why it matters beyond the campaign** — M7's square-root lowering emits this
+sequence. Without the fix, `sqrt()` in any shader would have been
+un-emulatable, discovered only when M8's filetests first ran a sqrt on the
+`xtn` target.
+
+**Fix** — `MksadjS` added to `Inst::FpRr` (decode `t = 0xC`, encode, disasm,
+roundtrip, golden vector `0xc0 0x21 0xfa`); the emulator classifies it with
+the divide-step family and implements its measured semantics
+(`fp_rom::mksadj`: `A = ⌊(e − 127)/2⌋` split-encoded, class codes for
+zero/negative/inf/NaN, INVALID on negative or signalling input). The
+wrongly-asserting test now pins only `t = 0x2` as unassigned.
+
+**Signal** — an "unassigned per objdump" claim is only as good as the objdump
+invocation behind it; the claim had no golden pinning it to a real objdump
+run. The campaign's rule — transcribe real toolchain output, never enumerate
+from memory — is what caught it.

docs/defects/README.md

@@ -112,6 +112,12 @@ genuinely fits none of these, and define it here in one line.
   only falsifier, so the collision surfaces whenever a compiler first
   emits the stolen form — which is usually at some optimization
   threshold nothing in the suite crosses.
+- **`incomplete-subset`** — a normative instruction/opcode subset is
+  assembled by enumerating what an external tool (objdump, an
+  assembler) is believed to assign, and the enumeration silently omits
+  a member that tool actually does assign — so the gap survives
+  exactly as long as nothing exercises that one member. Real toolchain
+  output (a sequence transcription, not memory) is the only falsifier.
 
 ## Index
 
@@ -172,6 +178,7 @@ sentence (arguments in, returns out; registers and stack).
 | invented-encoding | 2026-07-31 | [zexth-encoding-steals-xori-128](2026-07-31-zexth-encoding-steals-xori-128.md) | fixed | lp-riscv-inst (encode/decode) + lp-riscv-emu (executor) |
 | invented-encoding | 2026-07-31 | [elf-loader-riscv-reloc-numbering](2026-07-31-elf-loader-riscv-reloc-numbering.md) | **open** | lp-riscv-elf (relocations) |
 | partial-knowledge-loss | 2026-07-31 | [elf-loader-drops-relocation-addends](2026-07-31-elf-loader-drops-relocation-addends.md) | fixed | lp-riscv-elf (relocations) |
+| incomplete-subset | 2026-07-31 | [mksadj-missing-from-fp-subset](2026-07-31-mksadj-missing-from-fp-subset.md) | fixed | lp-xt/lp-xt-inst (FP subset) |
 | split-source-of-truth | 2026-07-30 | [jit-sret-return-count-zero](2026-07-30-jit-sret-return-count-zero.md) | fixed | lpvm-native/rt_jit (module.rs) |
 | config-masked-defect | 2026-07-30 | [xtensa-call-argument-clobber](2026-07-30-xtensa-call-argument-clobber.md) | fixed | lpvm-native/regalloc (walk.rs) |
 | config-masked-defect | 2026-07-30 | [xtensa-sret-pointer-clobber](2026-07-30-xtensa-sret-pointer-clobber.md) | fixed | lpvm-native/regalloc (pool.rs) |

docs/design/float.md

@@ -74,17 +74,31 @@ the WebAssembly spec; RV32F's from the RISC-V F spec.
 
 - **Denormal (subnormal) handling.** A target may flush denormal inputs
   and/or outputs to zero. wasm and RV32F preserve denormals (their specs
-  require it); the ESP32-S3 FPU and typical GPUs flush. Unifying this would
-  mean per-op software fixup on the hot path — rejected. Consequence:
-  results are only portable down to `~1.2e-38` magnitude; below that, a
-  target may produce `0.0` where another produces a tiny nonzero value.
+  require it); typical GPUs flush. **Measured on the ESP32-S3 Xtensa FPU by
+  the M6 hardware conformance campaign: it does NOT flush — full IEEE
+  subnormal arithmetic, both directions (350/350 conformance vectors, every
+  flush-distinguishing row)** — see
+  `docs/adr/2026-07-31-xtensa-fp-behavior-contract.md` §4. So `xtn.f32` and
+  `interp.f32`/`wasm.f32` agree on denormals by construction; the divergence
+  this row warns about is a GPU-tier and future-target risk, not a
+  Xtensa/wasm one. Unifying denormal handling in software everywhere would
+  still mean per-op fixup on targets that do flush — rejected as a blanket
+  policy. Consequence: results are only portable down to `~1.2e-38`
+  magnitude on a target that flushes; below that, such a target may produce
+  `0.0` where another produces a tiny nonzero value.
 - **Expression contraction.** An emitter may (or may not) fuse `a*b + c`
   into a fused multiply-add with a single rounding. Shaders must not depend
-  on the intermediate rounding of a multiply feeding an add.
+  on the intermediate rounding of a multiply feeding an add. Xtensa: the
+  `-O3` toolchain contracts on its own (`madd.s`), so contraction is not
+  even emitter-optional there — measured, xtensa-fp-behavior-contract ADR §7.
 - **NaN bit patterns.** Which NaN (payload, sign, quiet bit) an operation
   produces or propagates. "Is NaN" is portable; *which* NaN never is.
+  Xtensa: last NaN operand of `(fs, ft)` wins with the accumulator
+  outranking both for `madd.s`/`msub.s`, quiet bit forced, payload and sign
+  preserved; a generated NaN is `0x7FC00000` — measured, ADR §4.
 - **`round()` ties.** Halfway cases round to even or away from zero,
   per target — this is GLSL's own latitude, and hardware disagrees.
+  Xtensa's `round.s` ties to even — measured, ADR §4.
 
 ## 5. Unspecified
 

justfile

@@ -778,10 +778,13 @@ fwtest-loopback-esp32s3 port="":
 #   just fwtest-xt-fp-esp32s3 /dev/cu.usbmodemXXXX                 # everything
 #   just fwtest-xt-fp-esp32s3 /dev/cu.usbmodemXXXX signed_zero 50  # a smoke run
 #   just fwtest-xt-fp-esp32s3 /dev/cu.usbmodemXXXX tables          # estimate ROMs
+#   just fwtest-xt-fp-esp32s3 /dev/cu.usbmodemXXXX helpers         # divide-step probes
 #
 # `family` is an `lp-xt-fp-vectors` family name (rounding, nan_payload,
 # denormal, signed_zero, div_sqrt, convert), or `tables` for the estimate-table
-# sweep. `limit` caps each family; 0 runs all of it.
+# sweep, or `helpers` for the divide-step characterization grids (const.s and
+# the nexp01/mksadj/mkdadj/addexp/addexpm/maddn/divn probes). `limit` caps each
+# family or grid; 0 runs all of it.
 #
 # ORDERING RULE, same as fwtest-xt-jit-esp32s3 and for the same reason: the host
 # predictions in `lp-xt/lp-xt-emu/tests/fixtures/fp/` are committed FIRST, by
@@ -811,8 +814,8 @@ fwtest-xt-fp-esp32s3 port="" family="" limit="0":
     fi
     mode=families
     family="{{ family }}"
-    if [[ "$family" == "tables" ]]; then
-      mode=tables
+    if [[ "$family" == "tables" || "$family" == "helpers" ]]; then
+      mode="$family"
       family=""
     fi
     mkdir -p target/fp-capture
@@ -846,12 +849,14 @@ fwtest-xt-fp-esp32s3 port="" family="" limit="0":
     wait "$cap" 2>/dev/null || true
     echo "captured $(wc -l < "$out") lines to $out"
     # Only the family modes have predictions to diff against. The table sweep
-    # produces the estimate ROMs themselves — there is nothing to compare them
-    # to, which is the whole reason they have to be read off silicon.
+    # and the helper grids produce silicon-first data — there is nothing to
+    # compare them to, which is the whole reason they have to be read off
+    # silicon (the derived semantics are then held to the committed captures
+    # by boardless replay tests).
     if [[ "$mode" == "families" ]]; then
       just fp-diff "$out"
     else
-      echo "table sweep captured; P6 turns it into fp_policy::EstimateTables"
+      echo "$mode capture done; P6 turns it into fp_policy data + replay fixtures"
     fi
 
 # Diff an FP conformance capture against the committed host predictions.

lp-fw/fw-esp32s3/README.md

@@ -69,6 +69,7 @@ cargo test -p lpvm-native --features xt-corpus,emu-xt
 just fwtest-xt-fp-esp32s3 /dev/cu.usbmodemXXXX                 # the whole corpus
 just fwtest-xt-fp-esp32s3 /dev/cu.usbmodemXXXX signed_zero 50  # a smoke run
 just fwtest-xt-fp-esp32s3 /dev/cu.usbmodemXXXX tables          # estimate ROMs
+just fwtest-xt-fp-esp32s3 /dev/cu.usbmodemXXXX helpers         # divide-step helpers + probe2
 ```
 
 The M6 hardware campaign's rig. Runs `lp-xt-fp-vectors`' 5 630-vector corpus on