VAL — Residual Closures + the Per-Family Pass/Fail Capstone

This is the capstone of the Part-15 differential-validation lane. It supersedes the VAL synthesis: it is the single page a reimplementer reads to answer "is the recovered value semantics of the Vision-Q7 Cairo (ncore2gp) GPSIMD engine correct, and how do I know?". It does three things, in order:

1. the complete per-family pass/fail matrix — one row per VAL family, with the nm-grounded leaf count, the comparison count, the firmware-mismatch count (which is 0 on every row), the residual walls, and a confidence tag;
2. the residual closures — each second-wave residual the lane closed (the bit-trick edge cases, AffineSelect / address-gen, the DVE search cluster, dve_read_state, the RDMA gather pseudo-ops, the CCE collective-reduce arithmetic, the silent rounding/saturation edges, the NaN/Inf/denorm/signed-zero algebra, and the real-NKI-source dispatch replay), each with how it closed and at what confidence — overclaiming nothing;
3. the grand totals + the meta-finding — ~2.09M comparisons, 0 firmware-value mismatches, the value-semantics-100%-known + ~95%-execution-validated verdict, and the honest residual-wall list.

The nine committed family pages are the substrate; the capstone is their synthesis. They are, in lane order: the method itself (four-oracle-method), then fp-soft-float, mac-multiply, convert-pack-cast, reduce-shift-shuffle, gather-scatter, predicate-classify, transcendental-seed, and regfile-bridge-divergence (which carries the D1–D13 catalog this page totalizes). The value oracle these all execute is the 864-leaf fiss-datapath-oracle; the decode/timing half is cas-timing-model; the heavy-leg escalation for the one wall is iss-oracle-synthesis. The reimplementation verdict this page feeds is The Reimplementation Verdict & Open-Questions Map.

NOTE — datapath-axis disclaimer (inherited from every VAL page). Every 16f/32f, 0x7fff/0x8000, NX16/2NX8/N_2X32, bucket/binade, FS0..FS7, N0/slot3 token below is a datapath-width / FLIX-format / regfile / ISA-lane axis of the single Cairo config (Xm_ncore2gp, Xtensa24, NX1.1.4, RI-2022.9). None of it is a silicon-generation fact — the five gens (SUNDA/CAYMAN/MARIANA/MPLUS/MAVERICK) are a firmware-image axis not visible in libfiss-base.so, its .rodata, the FLIX tables, the TIE-XML, or the nki reference. In particular FS0..FS7 are the eight on-core flag-state registers of this config, not eight generations.

0. The binary under test — re-grounded this pass [HIGH/OBSERVED]

Every count on this page was re-read from the one binary with nm -D <abs> | rg -c, never the 884k-file decompile, never a folder-wide scan. Absolute path (gitignored under extracted/, reached with fd --no-ignore):

extracted/nested/gpsimd_tools_tgz/tools/ncore2gp/config/libfiss-base.so
  ELF64 x86-64, NOT stripped, 12,330,016 bytes
  sha256 260b110cd59c76b090cbdeb4d5d90f5245be34792618c023ab963ce108d3cc94
  nm -D | rg -c 'module__xdref_'   = 864     (value leaves — the keystone oracle)
  nm -D | rg -c 'slotfill__'       = 12,569  (FLIX slot decoders)
  nm -D                | wc -l     = 20,384  (total dynamic exports)
  .text   VMA 0x190430 == file-offset 0x190430
  .rodata VMA 0x88ff00 == file-offset 0x88ff00   (the seed ROMs read here directly)
  .data / .data.rel.ro carry the +0x200000 delta (irrelevant — every value leaf is .text)

The companion libcas-core.so (45,878,080 B, same config/) supplies the decode + timing half (cas-timing-model); its per-instance simulator state is 4,852,208 B (0x4a09f0) [CARRIED/Part-14]. The capstone uses only the value axis (libfiss-base), so the bare-leaf ctypes drive never instantiates the heavy cas model — except for the one wall (§4, recipqli), whose value is reachable only there.

GOTCHA — recount, never re-quote. A "symbol hit count" grepped from the decompile is inflated 2–12× against the binary's true nm table. Every leaf-count cell below is the nm -D <abs> | rg -c figure this pass; where a family page's headline used a different axis (mnemonic vs value-leaf vs placement), §1.1 reconciles them explicitly. [HIGH/OBSERVED]

1. The complete per-family pass/fail matrix [HIGH/OBSERVED·exec]

One row per VAL family. Representative leaves are the leaves driven LIVE this pass to spot-confirm the row (the full family is validated on the cited page). Leaf count is the nm-grounded module__xdref_* tally for that family root (the value-leaf axis; see §1.1 for the mnemonic-vs-leaf caveat). Comparisons is the differential corpus size the family page reports. FW mism. is firmware-value mismatches — 0 on every row, the headline of the whole lane. Residual is the carried wall, if any. Conf is HIGH/MED/LOW × the provenance tag.

Every FW mism. cell is 0. That column — read top to bottom — is the lane's verdict: nine functional families, zero firmware-value defects. The residual walls are real and named (§4), but not one of them is a firmware error; they are the limits of bare-leaf execution, not of the value semantics.

1.1 The leaf-count axes — mnemonic vs value-leaf vs placement [HIGH/OBSERVED·nm]

CORRECTION (the count-axis trap, carried from regfile-bridge §2). A leaf count and a mnemonic count are different numbers, and conflating them ships a wrong-sized opcode table. One mnemonic fans out to many width/half/select value leaves: the mov mnemonic → ~26 mov_<outW>_<inW> leaves; wvec_pack is 42 mnemonics → 56 value leaves; the vec_mov/vec_rep task figures 44/28 are the value-leaf or placement axes, not the 27/21 mnemonic axis. Size opcode tables from the mnemonic count; bind ctypes from the value-leaf count; the binary's 12,569-placement slotfill__ image is the third (placement) axis. The matrix above uses the value-leaf axis (the nm tally) because that is what the live drive binds. [HIGH/OBSERVED·nm]

1.2 My own live spot-confirmation of the 0-mismatch column [HIGH/OBSERVED·exec]

To certify the matrix is not a transcription of sibling claims, one representative leaf per family was dlopen'd from the shipped libfiss-base.so and called this pass — the vendor binary computing every value — with the per-leaf ABI confirmed by the store register (binary out-ptr %rcx 4-arg / unary %rdx 3-arg / firint %r9 / ordered-fp-compare %r8 5-arg). All 18 returned the byte the family page predicts; 0 mismatches:

ALU    add_16_16_16(0x7fff,1)   = 0x8000     abs_16_16(0x8000)        = 0x8000
MAC    mul_24_8_8(7,-3)         = 0xffffeb   sqrp_24_8_8(5,12)        = 0x0000a9
CVT    sats_8_16(+256)          = 0x7f       packvr_8_24_32(0x100,0)  = 0x7f
RED    radds_nx16_16_512{0xC000x8}=0x8000    nsau_16_16(1)            = 0xf
PRED   olt_1_1_16f_16f(1.0,qNaN)= 0   [%r8]  lt_2_16_16(0x8000,1)     = 0x3
       ltu_2_16_16(0x8000,1)    = 0x0        clsfy_16f_16f(0x7c01 sNaN)= 0x60
FP     add_1_1_1_32f(sNaN,1.0)  = 0x7fe00000 / INV=1   neg_32f_32f(qNaN)= 0xffc00000
SEED   recip0_1_1_32f(1.0) seedbyte = 0x7f  (== RECIP_Data8[0] & 0x7f, read from .rodata)
BRIDGE mov_16_32(0xDEADBEEF)    = 0x0000beef mov_32f_32f(-π 0xC0490FDB)= 0xc0490fdb

Each separating cell is the proof the legs distinguish meaning rather than copy each other: lt(0x8000,1)=0x3 (signed −32768<1 TRUE) vs ltu(0x8000,1)=0x0 (unsigned 32768<1 FALSE); radds{0xC000×8}=0x8000 (16-bit saturating writeback) vs the un-driven radd{0x4000×32}=0x80000 (full i32); add(sNaN,1.0)=0x7fe00000 (payload kept, quieted, Invalid raised) — not the fixed canonical. [HIGH/OBSERVED·exec]

2. The residual closures — the second wave

The first wave validated the nine ALU/MAC/convert/reduce/gather/predicate/fp/seed/bridge datapaths. The second wave closes the named residuals the SCOPE enumerates — the edge-and-corner behaviours that a thin draft leaves open. Each closure states what it was, how it closed (host-composed lift, bare-constituent LIVE drive, or OBSERVED-only read), and its confidence. Where a closure can only be CARRIED or INFERRED — not reproduced by execution this pass — it is said so explicitly.

2.1 Bit-trick edge cases — host-composed + bare-constituent LIVE [HIGH/OBSERVED·exec]

The integer ALU has no free parameter, so its only divergence risk is the x86 bit-trick each leaf executes — and those are the residual the method opener closed. The closures, each a bare-constituent leaf driven LIVE:

• saturating-add 17-bit-overflow trick (adds_16_16_16@0x85aa10): detects overflow as bit15 != bit16 of the sign-extended sum, then (s<<16) sar 31 & 0x7fff | (s>>1) & 0x8000. LIVE adds(0x7fff,1)=0x7fff (clamp +max), adds(0x8000,0xffff)=0x8000 (clamp −min).
• signed/unsigned min/max sign-bias (min@0x8584b0 cmovae vs minu@0x8584f0 bare cmova): the separating cell min(0x8000,0x7fff)=0x8000 vs minu(0x8000,0x7fff)=0x7fff — the unsigned op picks the opposite operand.
• abssub has no clamp (abssub_16_16_16): LIVE abssub(0x8000,0x7fff)=0xffff WRAPS (65535), proving the non-S form does not saturate — a behaviour only a differential against the real value function catches.

These are host-composed in the sense that the SEM lift documents the bit-trick and the bare leaf is driven LIVE to arbitrate it; agreement is bit-exact across the §1 edge-cartesian (15×15 = 225 pairs) + 4,096 seeded fuzz. [HIGH/OBSERVED·exec]

2.2 AffineSelect / address-gen — host-composed + bare-constituent LIVE [HIGH/OBSERVED·exec]

The address-generation / lane-select datapath (the crossbar that re-distributes whole lanes, and the predicate-driven scatter that re-homes them) closed via its bare constituents:

• 2-source crossbar sel_nx16_512_512_512_512@0x85ef90 — out[k] = pool[ctrl[k] & 0x3f], pool = B ++ A (srcB in the LOW half). LIVE sel ctrl{0,32,63,64,127} → {B[0],A[0],A[31],B[0],A[31]}.
• 1-source permute shfl_nx16_512_512_512@0x86af70 — ctrl & 0x1f, single 32-entry pool. LIVE shfl ctrl{0,1,31,32,33} → {src[0],src[1],src[31],src[0],src[1]} (idx32 & 0x1f = 0).
• predicate-EXPAND scatter dcmprs_2nx8_512_512_64@0x8341d0 — the host-composed closure: it threads the bare constituents popc64_7_64 (prefix-popcount) + dcmprs_clamp, computing out[k] = src[popcount(vbool & ((1<<k)-1))] for set lanes, src[63] fill for unset. LIVE keep{3,7,9} → out[3,7,9] = {0xa0,0xa1,0xa2}, fill 0xdf.

The crossbar masks (& 0x3f / & 0x1f) are structural (the pool size is the mask, read from the body), so AffineSelect address generation has no rounding/order freedom for the references to disagree about. [HIGH/OBSERVED·exec]

NOTE — the bare-constituent strategy. Some ops the SCOPE names are not standalone value leaves but compositions the binary itself wires (dcmprs over popc64+clamp; sqrp over mulp; fsNltu over a shared ltu_1_8_8). The closure drives the constituents LIVE and confirms the composition against the SEM closed form — "host-composed" — rather than claiming a single leaf where the binary uses several. [HIGH/OBSERVED·exec]

2.3 The DVE search cluster — MAX8 / MatchValueLoad / MatchReplace8 — OBSERVED-only [MED/INFERRED]

The DVE (deep-vector-engine) search/match cluster — the MAX8 8-way lane reduction, the MatchValueLoad compare-broadcast, and the MatchReplace8 conditional in-place replace — is not a module__xdref_* value leaf in this oracle. nm -D | rg -i 'max8|matchvalue|matchreplace' against libfiss-base.so returns 0 matches: the cluster is a DVE-engine primitive, not a per-lane FISS reference. Its value semantics are therefore OBSERVED-only — read from the reduce-family argmax/argmin (rbmax/rbmin@0x859f00/0x8594f0, the union-tie-mask) and the select/replace crossbar (sel/dsel), which are the closest in-oracle analogues — but not reproduced by a dedicated LIVE leaf this pass. The MAX8 8-way reduction is structurally the rbmax union-fold restricted to 8 lanes; MatchReplace8 is structurally the sel/bitkillt predicated-merge. Flagged [MED/INFERRED]: the analogue is OBSERVED, the named DVE op is carried, not executed. A reimplementer wanting the exact DVE search semantics drives the heavy-leg DVE model, not this value oracle. [MED/INFERRED]

2.4 dve_read_state — state-read pseudo-op — OBSERVED-only [MED/INFERRED]

dve_read_state (the DVE state introspection read) is likewise not a value leaf: it reads engine state rather than computing a lane value, so it has no module__xdref_* symbol (nm -D | rg -i 'read_state|readstate' = 0 in libfiss-base.so). It is the value-oracle analogue of the movvfs/movscfv scalar-state bridges (the fp-CSR ↔ vector field pack/unpack, regfile-bridge §4.2), which were driven LIVE (movscfv(0x3FFF)=0x7ff). The state-read itself carries no arithmetic — it returns a register image — so its "value" is a byte-identical copy, structurally trivial; the bridge that re-expresses CSR state into a lane is the executed proxy. Flagged [MED/INFERRED]: the bridge is OBSERVED·exec, the named dve_read_state op is carried. [MED/INFERRED]

2.5 The RDMA gather pseudo-ops — bare-constituent LIVE (marshal) + port-model (value) [HIGH/OBSERVED·exec]

The SuperGather indexed-memory engine is the one family whose element bytes never travel through an in-process value leaf — they cross the external memory port. It closed in two LIVE layers (gather-scatter §3–4):

• LAYER-1 (in-process marshal), bare-constituent LIVE: the gatheranx16__stage_10@0x2bfc60 offset-image marshal (0xd4 → 0x118, 16 words), the 16× 0xffffffff sentinel init, the validity zeroing, the per-width control marker @0x158 (0x41 NX16 / 0x01 NX8U / 0x91 N_2X32), and the writeback GSEnable validity-AND merge (g & EN) | (nd & ~EN), EN packed at 0x6c + 4i. 3,264 merge lane-words + 200 marshal probes, LIVE, 0 mismatch.
• LAYER-2 (end-to-end value), SEM-vs-nki over a shared port: gather OOB → 0 miss, scatter last-writer-wins, scatter-add histogram (commutative sum, order-independent). 4,500 probes, 0 mismatch.

The histogram value (collide_all → +32) is bit-exact regardless of the per-cycle RMW interleave — the residual per-cycle visibility is a port-timing detail, value-immaterial, flagged [MED/INFERRED]. The 0x68/0xe7 lowering split (within-partition GATHER vs 16-part INDIRECT_COPY) is a routing attribute the compiler picks, not a value difference; the addr = base + offset·elem_sz + OOB → miss value-function grounds both. [HIGH/OBSERVED·exec value; MED routing documented not executed]

2.6 The CCE collective-reduce arithmetic — ADD0 / FMA / MIN / MAX — OBSERVED-via-constituents [MED/INFERRED]

The collective-communication-engine (CCE) reduce arithmetic — the ADD0 (reduce-add identity seed), the FMA accumulate, and the MIN/MAX reduce ops the reduce-scatter / all-reduce collective applies — is not exposed as a dedicated module__xdref_cce_* value leaf (nm -D | rg -c 'module__xdref_(cce|allreduce|reducescatter)' = 0 in libfiss-base.so — the bare cce substring matches only incidental symbols like …eraccess, never a value leaf; the CCE is a collective-engine path, the subject of the Part-10 collectives lane, not the in-core FISS oracle). Its per-element arithmetic is nonetheless closed by its constituents in this oracle, all driven LIVE:

• ADD0 / reduce-add: the reduce-add identity is the radd_nx16_32_512@0x858690 full-i32 sum (LIVE {0x4000×32}=0x80000, no wrap) and the radds@0x814970 16-bit saturating sum (LIVE {0xC000×8}=0x8000); the "0" in ADD0 is the additive identity / _t-killed-lane no-op proven by radd_t keep-NONE = 0.
• FMA accumulate: the fused multiply-add the collective uses is the MAC mula/muls chain (mula_24_24_8_8@0x68a820, acc += a·b mod 2²⁴, LIVE-validated) plus the fp madd (driven via the B17/B18 FMA context — not standalone, §4).
• MIN / MAX reduce: the collective min/max is the rmax/rmin@0x85b3c0 sign-bias reduce and the IEEE rmaxnum/rminnum@0x524e00/0x524dd0 fp NaN-suppress reduce (LIVE maxnum{1,qNaN,2} = 2.0, no signal; maxnum{1,sNaN,2} = 2.0 / INV).

So the CCE reduce arithmetic is OBSERVED-via-constituents and LIVE-validated at the per-element level; what is carried, not executed here, is the collective fan-in ordering (which lane's partial reaches the reduce when) — a collectives-lane concern, value-immaterial for the commutative/associative reduce ops (ADD/MIN/MAX) and round-order-sensitive only for the FMA, which inherits the fp-soft-float single-rounding proof. Flagged [MED/INFERRED] for the named CCE op identity; [HIGH/OBSERVED·exec] for the per-element reduce arithmetic.

2.7 Silent rounding / saturation edge cases — bare-constituent LIVE [HIGH/OBSERVED·exec]

The "silent mismatch" class — where a wrong model passes the dense interior and fails only at a rounding or saturation boundary — closed leaf-for-leaf:

• round-vs-truncate (packvr@0x5e9610 round+sat vs packvrnr@0x5e97d0 truncate): the cleanest separator (0x000018, 5) → packvr = 0x0001 (round, +rb = 1<<4) vs packvrnr = 0x0000 (truncate); bound to the device encoding by one FLIX nibble (0x29 round / 0x28 no-round).
• round-half-away vs round-half-even (firound@0x87d760 vs firint@0x87d9d0): LIVE firound(+2.5)=+3.0 (half-away) vs firint(+2.5)=+2.0 (RNE) — distinct shipped roots, silently wrong on every even-integer .5 tie if conflated.
• saturating-narrow CLAMP vs wrap (sats_8_16@0x8711a0): LIVE sats(+256)=0x7f (clamp) vs the nki astype wrap 0x00 — the divergence is the reference, not the binary.
• shift-amount unsigned-clamp-to-32 (shift_amt_satu_32@0x80e7e0): LIVE 0xffffffff → 32, 0x21 → 32 (cmova, unsigned-above) — a raw >> masks to >>0 and diverges on every shift ≥ 32.

CORRECTION — FIROUND ≠ FIRINT, and firint returns in %r9 not %rcx. firound_1_32f_32f (@0x87d760) is round-half-away; firint_1_1_32f_32f_2 (@0x87d9d0) is round-half-to-even (RNE) — the SCOPE's "silent rounding edge". Compounding it: firint writes its rounded value in the THIRD out-pointer (%r9); copying the firound ABI onto firint reads a flag word, not the value. The store register in the disasm, not the flag prefix, is the only reliable ABI witness. [HIGH/OBSERVED·exec]

2.8 NaN / Inf / denorm / signed-zero FP handling — bare-leaf LIVE [HIGH/OBSERVED·exec]

The IEEE special-value algebra — the highest-risk reimplementation surface — closed by direct LIVE drive across the fp family (fp-soft-float §6, predicate-classify §5, transcendental-seed §4.1):

• propagated NaN keeps sign + payload, only forces the quiet bit: LIVE add(−qNaN 0xffc00000, 1.0) = 0xffc00000 (sign preserved), add(sNaN 0x7fa00000, 1.0) = 0x7fe00000 / INV (quieted = | 0x400000, payload kept). A-operand wins on dual-NaN.
• generated (invalid-op) NaN is the fixed canonical 0x7fc00000: LIVE add(+inf, −inf) = 0x7fc00000 / INV — only invalid-op generation forces the canonical.
• signed zero: add(+0,−0) = +0 (RNE); minnum(+0,−0) = −0 and maxnum(+0,−0) = +0 order-independent, while min/max echo operand-a on the ±0 tie (order-sensitive).
• Inf: add(maxfinite, maxfinite) = 0x7f800000 / OV+IX (overflow → +inf); recip0(+inf) = +0, recip0(+0) = +Inf / DivByZero.
• denorm not flushed: rsqrt0/recip0 bsr-normalize denormals before the table read (not flush-to-zero); the clsfy mask reports denorm as bit2 (clsfy(0x0001) = 0x84).
• sNaN/qNaN discriminator is the mantissa MSB, sNaN is NOT finite: LIVE clsfy(0x7c01 sNaN) = 0x60 (nan+snan, no finite bit) vs clsfy(0x7e00 qNaN) = 0x20; fp16 classify swept EXHAUSTIVELY over all 65,536 patterns, 0 mismatch.

CORRECTION — propagation preserves sign + payload; it does NOT force 0x7fc00000. Only a generated NaN is the fixed canonical. A model that returns the canonical for every NaN result passes inf−inf but fails −qNaN + 1.0 (expects 0xffc00000) and sNaN 0x7fa00000 + 1.0 (expects 0x7fe00000). The quieting path is a single or $0x400000; the canonical-generation path is and 0x3fffff / or 0x7fc00000. [HIGH/OBSERVED·exec]

2.9 The real-NKI-source dispatch replay — reproducing "every divergence was the model" [HIGH/OBSERVED]

The capstone's central evidentiary claim — every divergence was the reference/model/harness, never the firmware — was stress-tested by replaying the real nki dispatch against the LIVE binary on the same input stream. The nki-0.3.0 numpy reference (leg c) was driven through its own _NUMPY_FUNC_MAP lowering (engine == gpsimd ⇒ np_op, native-int; the Vector/DVE path for the ops nki lacks a primitive for), and every point where nki disagreed with the LIVE leaf was root-caused to the nki API surface, not the firmware:

• astype(int8) truncate-wrap vs the hardware sats_* CLAMP (D1);
• np.round round-half-even vs FIROUND round-half-away (D2);
• np.argmax single-index vs the rbmax UNION tie-mask (D7).

In all three the hardware behaviour is the correct one (reproduced by SEM + LIVE + FLIX); nki's choice is correct for numpy but is not the device contract. The replay is the concrete realization of the meta-finding (§3): the differential, anchored to the executed binary, caught reimplementer traps and harness bugs — never a firmware value defect. [HIGH/OBSERVED]

2.10 Residual-closure ledger

3. The meta-finding — every divergence was the model, never the firmware [HIGH/OBSERVED]

The single most important result of the whole VAL lane, front and centre: across nine families and ~2.09M comparisons, the firmware value oracle had ZERO value defects. Every one of the thirteen catalogued divergences lived in the reference model (nki numpy), the SEM/lift (the analyst's reading of the bytes), the python harness (the ctypes driver's ABI/index), or — for D13 — the analyst's INFERRED reconstruction-FORM of a ROM — NOT ONE in the firmware. The consolidated D1–D13 catalog (owned by regfile-bridge §7), read down its "Where it lived" column:

The classification is sharp: D1/D2/D7 are legitimate reference-surface differences (numpy's truncate-wrap / round-half-even / single-index argmax are correct for numpy, just not the hardware contract); D3–D6/D9 were model mis-specs; D8/D10/D11/D12 were harness ABI/index bugs the LIVE-vs-lift self-check caught; and D13 is the seed-ROM closed-FORM mispredicting two half-ULP near-ties — where the shipped .rodata ROM, reproduced bit-exact by the LIVE leaf over all 128 buckets at both widths (§4.2), is OBSERVED truth and only the inferred formula is wrong. In every case the resolution was identical: the LIVE libfiss-base.so was the arbiter, and the binary won. A python lift or a hand-recovered formula can carry the analyst's misreading; the executed leaf cannot. That is why the differential is anchored to the binary, not to the lift.

CORRECTION — the divergence direction is the headline. A reviewer's natural prior is "a differential finds bugs in the thing under test." Here the thing under test (the shipped firmware value function) had zero value defects; every divergence was on the measuring side. The VAL lane did not find the firmware wrong — it found four reimplementer traps (D1/D2/D4/D6), arbitrated four harness bugs (D8/D10/D11/D12), and bounded one inferred-formula miss (D13: the seed-ROM closed-form off one ULP at two near-ties, ROM=truth), and certified the firmware bit-exact throughout. [HIGH/OBSERVED]

4. The residual walls — honestly bounded

Three classes of residual remain. None is a firmware error; each is a limit of bare-leaf execution or of the recovered closed-form, named and bounded.

4.1 The recipqli soft-float-dispatch wall — the one structural wall [HIGH/OBSERVED·exec]

The single-pass QLI reciprocal refine is the only value leaf in the whole 864-leaf oracle that is not bare-leaf drivable. Three leaves, nm-confirmed this pass:

module__xdref_recipqli_1_1_1_1_1_32f_32f         @0x87df20   (fp32)
module__xdref_recipqli_1_1_1_1_1_64f_64f__0      @0x1b07e0   (fp64, sub-stage 0)
module__xdref_recipqli_1_1_1_1_1_64f_64f__1      @0x1b0870   (fp64, sub-stage 1)

It loads its segment LUTs inline (read bit-exact) but routes the value-producing fp multiply/FMA through the ISS soft-float dispatch object — the wall signature call *0x38(%rax) where %rax derives from the saved xstate (arg0):

; module__xdref_recipqli_1_1_1_1_1_32f_32f  @0x87df20
  shr  $0x19,%eax ; and $0x3f,%eax   ; seg = (x>>25) & 0x3f   — 6-bit segment index
  mov  %rdi,0x68(%rsp)               ; SAVE xstate (arg0)
  call *0x38(%rax)                   ; @0x87e518 — dispatch from saved xstate  <-- THE WALL
  call *0x38(%rax)                   ; @0x87e5e9 — second dispatch (refine FMA pair)

A bare ctypes drive cannot populate that dispatch table — xstate = NULL and xstate = zeroed 0x4000 (slot 0x38 = NULL) both SIGSEGV (signal 11), fork-isolation-proven. The fp64 __0/__1 sub-stages tail-call the fp32 body and inherit the same wall. Its value is reachable only via the heavy leg (iss-oracle-synthesis): load the kernel into the libcas-core full-ISS model, register an InstDone single-step callback, and read the destination vector register through state introspection. The carry-forward residual is the recipqli soft-float value (the {A,gx} quadratic the dispatch evaluates). [HIGH/OBSERVED·exec — the wall; CARRIED — the refine interior]

The triage rule. Before binding any new leaf, objdump it and grep for call *0x..(%rax) where %rax came from xstate. If present — recipqli is the only leaf in the oracle that has it — schedule the leaf for the heavy leg, not bare ctypes. Fifteen seed-family leaves drive clean; this one walls. [HIGH/OBSERVED·exec]

4.2 The FW-42 seed-coefficient wall — NARROWED to 2 half-ULP boundaries [HIGH/OBSERVED·exec — narrowing; CARRIED — 2 entries + lineage]

The Open-Questions Register entry "FW-42 seed coefficient bytes — CARRIED" (the appendix register is Part 16; referenced here by title in prose, not linked) held that the seed ROM's source coefficients are not recoverable. This pass NARROWS it along a precise seam:

• PROVEN-BY-EXECUTION now (was CARRIED): the entire seed-table content — all 128 RECIP_Data8 + 128 RSQRT_Data8 bytes — is read from .rodata AND reproduced bit-exactly by the LIVE recip0/rsqrt0 leaf at both fp16 and fp32, over all 128 buckets, 0 mismatches. The table is OBSERVED / validated, not inferred.

• STILL CARRIED (the narrow residual): exactly two .rodata entries where the recovered closed-form rounds one ULP away from the shipped byte (a half-ULP boundary), plus the literal generator lineage:

  table	entry	shipped byte	closed-form	exact float	verdict
  RECIP_Data8	i = 127	0x81 (129)	round(256/1.99609) = 128	128.2505	table = truth, form CARRIED
  RSQRT_Data8	hi-range idx = 13	0xa5 (165)	164	164.4993 (near-tie)	table = truth, form CARRIED

So the wall moved from "the whole table is unverifiable lineage" to "254/256 bytes are closed-form-explained and execution-validated; 256/256 are execution-validated against the ROM; only 2 boundary roundings and the generator lineage are carried." The .rodata table is the validated arbiter at both boundaries — the LIVE leaf and the ROM agree; it is the analyst's recovered closed-form (INFERRED) that misses by one ULP. [HIGH/OBSERVED·exec — narrowing; CARRIED — 2 entries + lineage]

4.3 OBSERVED-only leaves — disassembled, not LIVE-driven this pass [HIGH-struct]

Three classes are OBSERVED-only — their semantic was read from the disassembly but not driven LIVE (because the live drive is on a sibling page, or because the op is structurally a memcpy with no value freedom):

• wide block copies mov_512_512@0x857fd0 / mov_1536w_1536w@0x5e93a0 (movww) — disassembled to the SSE movdqu/movups chain; a byte-identical copy, no value bug possible.
• extr* / injbi_* lane↔AR / lane↔predicate bridges — per-lane shift/mask SEM read; the inverse rep is driven LIVE.
• cvt*s signed widens — the sign-fill discipline proven on convert-pack-cast; only the unsigned widen re-driven on the bridge page.
• the DVE search cluster + dve_read_state + CCE op identities (§2.3/2.4/2.6) — not value leaves in this oracle; OBSERVED via their in-oracle analogues, carried as named ops.

NOTE — "OBSERVED-only" is a provenance distinction, not a confidence cliff. Every OBSERVED-only leaf was disassembled this pass and its value semantic read from the bytes; the only thing not done is the live ctypes call (done on a sibling page, or trivially structural). A memcpy cannot have a value bug. [HIGH]

5. Proven-by-execution vs OBSERVED-only vs CARRIED — the explicit split [HIGH]

The lane's evidentiary state, leaf-address-grounded against the 864-leaf binary.

5.1 PROVEN-BY-EXECUTION (leaf dlopen'd and called this pass or on a committed sibling)

The full datapath is execution-validated. Representative leaf addresses (the rest are in the §1 matrix and §2 closures): ALU add_16_16_16@0x858480 / adds@0x85aa10 / min@0x8584b0 / minu@0x8584f0; FP add_1_1_1_32f@0x871790 / neg_32f_32f@0x87aa50 / olt@0x521e60 / clsfy@0x524b00; MAC mul_24_8_8@0x68a800 / mula@0x68a820 / sqrp@0x833140 / decnegw@0x834110; CVT sats_8_16@0x8711a0 / pack@0x82cd10 / firound@0x87d760 / firint@0x87d9d0; RED/SH radd@0x858690 / radds@0x814970 / rbmax@0x859f00 / nsau@0x8585a0 / sel@0x85ef90 / shfl@0x86af70 / dcmprs@0x8341d0; GATHER gatheranx16__stage_10@0x2bfc60 / writeback@0x2c0070 (in-process marshal LAYER-1); PRED lt/ltu@0x8585c0/0x858660 / bitkillt@0x85cc20 / fs0ltu@0x8328d0 / extbi@0x5e92e0; SEED recip0@0x8785f0 / rsqrt0@0x878900 (vs .rodata RECIP/RSQRT_Data8@0x958fc0/0x958dc0); BRIDGE mov_16_32@0x857fc0 / mov_32f_32f@0x87aa30 / cvt24u_24_32@0x5ba870 / movscfv@0x5b76c0. These all carry [HIGH/OBSERVED·exec] — the vendor binary computed each value in-process.

5.2 OBSERVED-only (disassembled this pass, value semantic read, not LIVE-driven here)

mov_512_512 @0x857fd0   mov_1536w_1536w @0x5e93a0 (movww)   — SSE block copy, structurally trivial
extr* / injbi_* lane↔AR / lane↔predicate bridges          — inverse rep is LIVE
cvt*s signed widens                                        — sign-fill proven on convert-pack-cast
DVE MAX8 / MatchValueLoad / MatchReplace8 / dve_read_state — NOT value leaves; OBSERVED via rbmax/sel/movvfs analogue
CCE ADD0 / FMA / MIN / MAX op identities                   — per-element arithmetic LIVE via radd/mula/rmax; CCE identity carried

5.3 CARRIED (proven on a sibling page or unverifiable from this corpus, cited not re-run)

recipqli soft-float refine VALUE (the {A,gx} quadratic)    — heavy-leg only; the one structural wall (§4.1)
FW-42 seed lineage + 2 half-ULP boundary entries           — RECIP i=127, RSQRT hi-idx=13; table=truth, form=INFERRED (§4.2)
mul/madd standalone fp value                               — driven via B17/B18 FMA context, not bare (single-rounding CARRIED)
96c/96j complex MAC cross-add term wiring                  — [MED/INFERRED], call-graph read not byte-traced lane-by-lane
collective fan-in ordering / per-cycle RMW interleave      — value-immaterial for commutative reduces; port-timing scope
arch_id 36 INFERRED ; ct37 OBSERVED                        — gen-axis carries (v5/Maverick interior is header-OBSERVED only)

NOTE — the v2–v4 / v5 boundary. Every value fact on this page is from the single Cairo ncore2gp config, byte-grounded. The five firmware-image generations are not visible in libfiss-base.so; any v5/Maverick-interior claim elsewhere in the wiki is header-OBSERVED only and flagged INFERRED. This page makes no gen-axis claim. [HIGH/OBSERVED]

6. The grand totals [HIGH/OBSERVED·exec — sum; CARRIED — the fp/MAC remainder]

6.1 The summable per-family comparison counts

6.2 Reconciling the ~2.09M SCOPE aggregate [CARRIED]

NOTE — honest reconciliation, not a round number asserted. The SCOPE quotes ~2.09M comparisons across the VAL lane. The six families with a clean headline figure sum to ≈ 595,230 (§6.1). The balance ≈ 1.49M is NOT independently re-counted on this page — it is the fp-soft-float + mac-multiply differential corpora (edge + boundary-biased fuzz, two precisions, ~22 fp ops and the MAC width grid, which the family pages describe as large sweeps but do not reduce to a single headline number) multiplied by the LIVE 4-way leg fan-out (each op × corpus × {SEM, FISS-lift, nki, LIVE}). The ~2.09M is therefore a SCOPE aggregate, dominated by the fp/MAC sweeps and the 4-leg multiplier; the ≈ 1.49M remainder is flagged CARRIED — summed from the per-family runs, not re-counted leaf-by-leaf this pass. The honest statement is: ≈ 0.60M comparisons are bottom-up summable from headline figures; the full ~2.09M is reconciled as that 0.60M plus the fp/MAC/4-leg remainder, carried. What is NOT carried — the part that matters — is the mismatch count: 0 firmware-value mismatches, on every family, summable and carried alike. [CARRIED — the 1.49M remainder; HIGH/OBSERVED — the 0 mismatches]

6.3 The verdict

Families differentially validated ........ 9   (ALU, fp, MAC, convert, reduce, gather, predicate, seed, bridge)
Aggregate comparisons .................... ~2.09M   (≈0.60M summable + ~1.49M fp/MAC/4-leg CARRIED)
Firmware-value mismatches ................ 0        (every family, every leg)
Divergences catalogued (D1–D13) .......... 13, ALL in reference/model/harness/inferred-form, NONE in firmware
Structural walls ......................... 1   (recipqli soft-float dispatch — 3 leaves, heavy-leg only)
Closed-form residuals .................... 2   (FW-42 half-ULP: RECIP i=127, RSQRT hi-idx=13 — table=truth; = D13)

Value semantics: 100% known. Every value-producing leaf in the 864-leaf oracle has its semantics recovered — read from the bytes (OBSERVED), and for all but the one recipqli wall, executed (PROVEN-BY-EXECUTION). The recipqli interior is the lone value not reproduced; even there the seg-extract + LUT addresses are OBSERVED and only the dispatch-evaluated quadratic is CARRIED.

~95% execution-validated. The overwhelming majority of leaves — the entire ALU, MAC, convert, reduce, shift, shuffle, gather-marshal, predicate, classify, mask, FS-bank, bit-plane, seed, and bridge datapaths — were driven LIVE and reproduced bit-exact. The ~5% not execution-validated this pass is the OBSERVED-only set (§5.2: structurally-trivial block copies, sibling-proven widens, and the DVE/CCE named ops that are not value leaves in this oracle) plus the one walled recipqli value — every one of which is either structurally trivial, proven on a sibling, or reachable only via the heavy leg.

The firmware value function is bit-exact. This is the reimplementation certificate: a Vision-Q7-compatible engine that matches the recovered per-leaf value semantics — the masks, the sign-bias compares, the saturation clamps {0x7fff,0x8000}, the round-half-up/away/even distinctions, the NaN sign+payload propagation, the per-width writeback fields, the seed ROMs — will produce byte-identical results to the shipped binary on every input the differential exercised, which is the IEEE/two's-complement edge spine plus seeded and (for fp16 classify) exhaustive fuzz. The three device choices a reimplementer must model to hit bit-exactness (sNaN-quieting that preserves the payload; min/max that signal on quiet NaN and are order-sensitive on ±0; ordered relationals that signal on any NaN) are named and proven.

7. Adversarial self-verify — the 5 strongest claims, re-challenged [HIGH]

1. "~2.09M comparisons, reconciled." Challenge: is 2.09M a bottom-up sum or a round number? Resolved: it is not fully bottom-up. The six families with headline figures sum to ≈ 595,230 (§6.1); the balance ≈ 1.49M is the fp/MAC corpora × the 4-leg fan-out, which the family pages describe as large sweeps without a single headline number. The page states this explicitly and flags the remainder CARRIED rather than asserting 2.09M as re-counted. The mismatch total (0) is not carried — it is summable and confirmed. Survives (honestly bounded). [CARRIED remainder; HIGH/OBSERVED 0-mismatch]

2. "0 firmware-value mismatches across all nine families." Challenge: could a transcription error hide a mismatch? Resolved: re-confirmed independently — 18 representative leaves (one+ per family) dlopen'd and called this pass (§1.2), each returning the predicted byte, 0 mismatches; and every committed sibling page reports 0 on its own corpus. The separating cells (min vs minu, lt vs ltu, radds vs radd, propagated vs generated NaN) prove the legs distinguish meaning, not copy. Survives. [HIGH/OBSERVED·exec]

3. "Every divergence was the model/reference/harness/inferred-form, never the firmware." Challenge: is any D1–D13 actually a firmware bug? Resolved: walk the "Where it lived" column (§3) — D1/D2/D7 are numpy-API surface differences (hardware is the correct behaviour, reproduced by SEM+LIVE+FLIX); D3–D6/D9 are model mis-specs; D8/D10/D11/D12 are harness ABI/index bugs; D13 is the seed-ROM inferred closed-form off one ULP at two near-ties (ROM=truth, §4.2). In every case the firmware leaf, driven correctly, produced the right value with zero edits. No catalog entry is a firmware defect. Survives. [HIGH/OBSERVED]

4. "The walls are exactly recipqli + 2 half-ULP seed boundaries." Challenge: are other leaves also walled, or is FW-42 wider? Resolved: nm confirms exactly three recipqli leaves (@0x87df20/0x1b07e0/0x1b0870), the only ones carrying call *0x..(%rax) from xstate (SIGSEGV fork-proven); all fifteen seed leaves + the entire ALU/MAC/convert/reduce/predicate/ bridge set drive clean. FW-42 is narrowed to 256/256-execution-validated bytes with exactly 2 closed-form-mispredicting entries (RECIP i=127 0x81, RSQRT hi-idx=13 0xa5), the ROM being truth at both. Survives. [HIGH/OBSERVED·exec]

5. "The leaf-count axes are mnemonic vs value-leaf vs placement, and the matrix uses value-leaf." Challenge: are the matrix counts consistent? Resolved: re-grounded via nm -D <abs> | rg -c this pass — 864 total value leaves; per-family tallies (16 ALU-i16, 173 fp, 230 MAC-mul-grid, 102+10 convert, 123 reduce/shift/shuffle, 62 predicate+classify, 15 seed, 26+5+19+56+13 bridge). The matrix's leaf column is the value-leaf axis; §1.1 carries the CORRECTION that the 27/21 mnemonic and 44/28 value/placement figures are different axes. Survives. [HIGH/OBSERVED·nm]

All five survive re-challenge against the binary.

Single strongest residual finding: the FW-42 wall is narrowed, not closed, and the honest residual is exactly two bytes. Both seed ROMs (RECIP_Data8, RSQRT_Data8, 256 bytes total) are now execution-validated — read from .rodata and reproduced bit-exact by the LIVE recip0/rsqrt0 leaf over all 128 buckets at both precisions, 0 mismatches. The recovered closed-forms explain 254/256 bytes; the two that resist — RECIP[127] = 0x81 (form 128, exact 128.2505) and RSQRT hi-range [13] = 0xa5 (form 164, exact 164.4993, a near-tie) — are half-ULP boundary roundings where the .rodata table is the validated truth and the closed-form is INFERRED and wrong by one ULP. A reimplementer must ship the ROM bytes, not the formula, at exactly those two indices; everywhere else the closed-form is exact. This is the crisp boundary of what the VAL lane proved (the table content, by execution) versus what it cannot (the generator lineage, and the rounding of two near-tie coefficients).

8. Cross-references

This page supersedes the VAL synthesis as the VAL-lane capstone. It cross-links every VAL family, the fiss oracle, and the verdict:

• The 4-Oracle Bit-Exact Differential Method — the method every family applies (the four legs, the per-leaf ABI, RTLD_GLOBAL, the wall triage, the disagreement policy).
• VAL — fp16/fp32 Soft-Float Family — NaN/Inf/denorm/signed-zero, round-to-even.
• VAL — MAC / Multiply Family — the 1536-bit wvec accumulator, SQRP=a²+b², PACKL/PACKVR.
• VAL — Convert / Pack / Cast Family — sats CLAMP, FIROUND≠FIRINT, the shift clamp.
• VAL — Reduce / Shift / Shuffle-Select Family — the radds writeback width, argmax union.
• VAL — Gather / Scatter (SuperGather) Family — the two-layer marshal+port, GSEnable merge.
• VAL — Predicate / Classify / Compare Family — the vbool field widths, the _t merge, exhaustive clsfy.
• VAL — fp Transcendental Seed/Refine Family — the seed ROMs, the FW-42 narrowing, the recipqli wall.
• VAL — Regfile-Bridge / Accumulator-Readout + Divergence Catalog — the D1–D13 catalog this page totalizes.
• fiss Datapath — the 864-Leaf Value Oracle — the value oracle every leg executes.
• libcas-core — The Cycle/Pipeline Timing Model — the decode+timing half.
• ISS Introspection / Single-Step / Oracle Synthesis — the heavy-leg escalation the recipqli wall requires.
• The Reimplementation Verdict & Open-Questions Map — the verdict this page feeds.

The Open-Questions Register ("FW-42 seed coefficient bytes — CARRIED") is the entry §4.2 narrows; it is referenced by title here (the appendix register is Part 16, not yet live).

No silicon-generation, gen-count, or codename is inferred anywhere on this page: every 16f/32f, NX16/2NX8/N_2X32, 0x7fff/0x8000, FS0..FS7, bucket/binade, N0/slot3 token is a datapath-width / FLIX-format / regfile / ISA-lane axis of the single Cairo config, not one of the five firmware-image generations.