The Coverage Ledger

This is the completeness anchor of the whole guide — the single page the Reimplementation Verdict cites when it answers "how much of the Vision-Q7 'Cairo' (ncore2gp) GPSIMD engine is actually known, and at what confidence?" It is the long form behind the verdict's five headline fractions: a per-lane coverage assessment that, for each of the nineteen reverse-engineering lanes, states the coverage, splits it into what is OBSERVED (read or executed from a shipped binary), what is INFERRED (reasoned over OBSERVED bytes), and what is a genuine static-analysis WALL (a corpus / license / runtime boundary, not a knowledge gap), and pins the key deliverables to the owning synthesis page.

The verdict page is the navigable map; this is the accounting. Where the verdict states "~95% execution-validated," this page shows the per-lane denominators that roll up to it; where the verdict says "v5 header-OBSERVED + bounded-INFERRED," this page carries the exact OBSERVED/INFERRED seam per lane. Every headline number below was re-grounded against its owning synthesis page and, where cheap, re-read from the binary this pass (nm on the one file by absolute path — never a folder-wide scan).

Confidence tags follow the Confidence & Walls Model: OBSERVED = a byte/symbol/immediate read from the shipped binary (or a value computed by executing the shipped simulator); INFERRED = reasoned over OBSERVED facts; CARRIED = re-used at a cited report's confidence; each crossed with HIGH / MED / LOW. Callouts: QUIRK (counter-intuitive but real), GOTCHA (a reimplementation trap), CORRECTION (overturns a naive reading), NOTE (orienting context).

GOTCHA — count with nm, never a decompile grep. Every count cell on this page is the owning page's nm <abs> | rg -c figure, re-verified against the shipped binary where it is the keystone. A "symbol hit count" grepped from the 884k-file decompile inflates 2–12× against the binary's true .symtab/.dynsym table. The binary is the arbiter; the decompile is not. [HIGH/OBSERVED]

NOTE — what a "lane" is. A lane is one reverse-engineering axis with one owning capstone: ISA, ISS, VAL, HW, FW, IMG, GEN, ABI, RT, DMA, CCL, NCFW, NEFF, CC, STRUCT, CSR, ADDR, INT, SEC. They are not disjoint subsystems — VAL validates ISA's value leaves, ISS executes them, CC produces the opcodes FW dispatches — but each carries an independent coverage claim with its own binary witness, so they total honestly.

1. The headline fractions — each tied to its owning page

These four fractions are the completeness anchor. The verdict page quotes them; this page re-grounds each against the owning synthesis page and the binary where it is the keystone.

1.1 Value semantics — 100% (864/864) [HIGH/OBSERVED]

Every value-producing opcode of the GPSIMD datapath has its per-element function recovered. The denominator is the 864 module__xdref_ value leaves in libfiss-base.so; all 864 are enumerated and their semantics read from the bytes, and for all but the one recipqli wall (§3, VAL lane) executed in-process.

• Owning pages: VAL capstone §6.3 ("Value semantics: 100% known"); the ISA value-cover §5 (864/864 leaves); verdict A.2 ("864 / 864 = 100%").

• Binary re-verify this pass:

  nm -D libfiss-base.so | rg -c 'module__xdref_'   = 864
  nm    libfiss-base.so | rg -c 'module__xdref_'   = 864   (same in .symtab)
  

  Reproduces exactly. [HIGH/OBSERVED]

1.2 Execution-validated — ~95%, ~2.09M comparisons, 0 firmware bugs [HIGH/OBSERVED — the 0; MED — the ~95%]

The overwhelming majority of value-bearing leaves were driven LIVE against the shipped simulator and reproduced bit-exact, across 18 op families / ~2.09M in-process differential comparisons, with zero firmware value defects found — every one of the catalogued divergences (D1–D13) lived in the reference model, the analyst's lift, the python harness, or an inferred closed-form, never the firmware.

• Owning page: VAL capstone §3, §6 (the meta-finding + the grand totals); verdict A.2.

NOTE — why ~95% is MED on the fraction but HIGH on the fact. The fact that ~2.09M live comparisons over 18 families returned zero firmware value mismatches is [HIGH/OBSERVED] — it is what the binary returned when executed. The exact fraction (~95%) is MED: it is a census over a denominator the later VAL passes widened (from ~85–90% over 9 families to ~95% over 18). The VAL capstone is also honest that the 2.09M aggregate is ≈0.60M bottom-up summable + ~1.49M fp/MAC/4-leg remainder CARRIED — but the 0-mismatch count is summable and confirmed on every family. Encode "the value lane is the arbiter and found no firmware bug"; treat the percentage as a bounded estimate.

1.3 Encoding — a certified-perfect cover (1534/1607/12642) [HIGH/OBSERVED]

The shipped Vision-Q7 encoding is a certified-perfect, non-overlapping cover: 1534 / 1534 shipped mnemonics and 12569 / 12569 shipped placements, folded from the 1607 / 12642 pre-fold TIE-DB authoring superset (the +73 fold = 24 .W18 wide-branch macros + 6 virtualops + 43 no-body pseudo). The device-native objdump/as round-trips byte-exact over hundreds of thousands of bundles with zero disagreements.

• Owning page: the ISA coverage tally; the semantics coverage ledger; the formal ISA model.

• Binary re-verify this pass (libisa-core.so):

  nm libisa-core.so | rg -c 'Opcode_.*_Slot_.*_encode'                       = 12569  (placements)
  nm libisa-core.so | rg -o 'Opcode_(.+)_Slot_[A-Za-z0-9_]+_encode' | sort -u = 1534  (mnemonics)
  1534 + 73 = 1607      12569 + 73 = 12642   (the fold arithmetic — exact)
  

  Reproduces exactly. [HIGH/OBSERVED]

GOTCHA — pair the totals correctly. The only valid pairs are 1534 ↔ 12569 (shipped / runtime) and 1607 ↔ 12642 (pre-fold / authoring). Pairing 1534 with 12642, or 1607 with 12569, mixes the runtime fold with the authoring superset and manufactures a ±73 phantom. The shipped 1534 / 12569 is the denominator for anything a reimplementer builds (decoder, assembler, ISS). [HIGH/OBSERVED]

1.4 The net grade — ≥97% reimplementation-grade for v2–v4; header-OBSERVED + bounded-INFERRED for v5 [HIGH/INFERRED over the named denominators]

Folding the three closed axes (encoding · value semantics · execution-proof) with the firmware mechanism, the custom-op ABI, the host runtime spine, and the device dispatch, the consolidated grade is a byte-grounded, execution-validated reimplementation reference at ≥97% coverage for v2–v4 (SUNDA / CAYMAN / MARIANA / MARIANA_PLUS), and a header-OBSERVED + bounded-INFERRED reference for v5 (MAVERICK) and v1 (TONGA).

• Owning page: verdict A.2 net grade.

GOTCHA — v2–v4 is hard spec; v5/v1 is header-OBSERVED only. A reimplementer can target v2–v4 as a hard specification — their firmware images, config, and ABI are present and read directly, their value semantics closed by execution. v5 (MAVERICK) and v1 (TONGA) are publishable only as header-OBSERVED + bounded-INFERRED, interiors flagged on every use. The 1534/12569 encoding cover is the gen-invariant Cairo core (one libisa-core.so, no arch_id/coretype gate in its decode path), so the encoding tally holds across all shipped generations; the per-generation firmware/image residuals (v5 absent) are a separate axis. See §4 for the v5 walls. [HIGH/OBSERVED on gen-invariance of the encoding]

2. The per-lane coverage table

One row per lane. Coverage is the lane's own self-assessed completeness (the owning page's figure, in its own wording — many lanes report a structural cover with a flagged interior rather than a single percentage). OBSERVED / INFERRED / WALL are the three-way split per lane. Deliverables are the lane's key reimplementer artifacts. Owning page is the synthesis / capstone that holds the full accounting. Confidence is HIGH/MED/LOW × OBSERVED/INFERRED/CARRIED.

NOTE — "complete" means coverage of what the lane can recover from this corpus, with the residual named. No lane claims to have recovered an artifact that is not in the corpus; where a body is absent (the v5 NCFW image, the customer _cpuN.so, the host PWP coefficient content), the lane carries it as a WALL with its closability, not as a silent gap. The honest reading of every "complete" cell is "complete up to the named wall." [HIGH]

3. The OBSERVED / INFERRED / WALL discipline — what each lane's three columns mean

The split is not cosmetic — it is the whole point of the ledger. A reimplementer encodes the OBSERVED column as a hard requirement, treats the INFERRED column as a bounded estimate to re-confirm on hardware, and reads the WALL column as "do not fabricate past here — close it with the cited artifact."

• OBSERVED is a byte read from a shipped binary (nm/readelf/objdump) or a value the shipped simulator returned when executed in-process. The 864 value leaves, the 1534/12569 encoding tables, the 386 image getters, the 65/85 byte-exact CSR schemas, the tpb_t 39,320-byte layout — all OBSERVED. This is the bedrock.
• INFERRED is reasoned over OBSERVED bytes: the HW datapath wiring (RTL absent, so box-to-box topology is reasoned from the stage stamps), the arch_id 36 (from the coretype − 1 relation), the cross-process 70/30 GPU arbitration. INFERRED is honest reasoning, flagged so it is never mistaken for a byte-read.
• WALL is a genuine static-analysis boundary — closable-with-corpus (a fuller checkout), closable-with-license (a FlexNet key on the already-runnable ISS), closable-with-hardware (a runtime capture / device run), closable-with-static (a follow-on pass on the binary in hand), or fundamental (the thing does not exist in this subsystem). The taxonomy is the Confidence & Walls Model §3.

NOTE — the meta-finding the whole ledger rests on. Across all nineteen lanes and the ~2.09M VAL comparisons, not one open question is a missing datapath body, a missing opcode decode, or a missing value semantics. Every WALL is a corpus / license / runtime / scope boundary — a checkout, a key, a capture, or a follow-on pass away. The machine is recovered; what is walled is a runtime input, an absent generation's image, an out-of-config core, or a license-gated observable. [HIGH/INFERRED over the named denominators]

The one value-leaf wall worth naming up front (the VAL lane's only structural wall): the 3 recipqli soft-float QLI refine leaves (3/864 ≈ 0.35%) route their value-producing FMA through a host soft-float dispatch object (call *0x38(%rax)) a bare ctypes drive cannot populate — a fork-isolated probe SIGSEGVs on the NULL slot. Everything under the wall (the 6-bit segment index, the four QLI coefficient tables read bit-exact, the two-substage split, the device round-trip) is proven; only the soft-float FMA on top is gated. This is a driver gap, not a knowledge gap, reachable via the heavy-leg ISS. [wall HIGH/OBSERVED; refine interior CARRIED]

4. The v5 / MAVERICK walls — the OBSERVED/INFERRED seam, stated carefully

The v5 (MAVERICK) generation is the single largest INFERRED region in the guide, and the ledger states its seam precisely because several downstream pages cite it. The hard fact is that the v5 NCFW management-core image is FILE-ABSENT — there is no MAVERICK NCFW image of either kind in this corpus, and MAVERICK does not reuse the v4+ image.

The binary evidence (from the NCFW synthesis §3.2 and the IMG catalog, re-grounded this pass):

• the libncfw_get_image ladder compares only {0x05, 0x0c, 0x14, 0x1c} (SUNDA / CAYMAN / MARIANA / MARIANA_PLUS); a cmp $0x1c; ja … sends any arch_id > 0x1c — including 0x24 (= 36) — to return 2;
• the libncfw rodata closes at 0x918e4 with zero v5/maverick symbols and exactly four codename .c strings.

4.1 The ct37 OBSERVED vs arch_id 36 INFERRED split

NOTE — coretype 37 is OBSERVED; arch_id 36 is INFERRED. State both; pick neither silently. The two facts live on opposite sides of the OBSERVED/INFERRED line, and the SCOPE requires the seam be stated, not collapsed:

• coretype 37 (ct37) — OBSERVED. It is byte-read in the live get_ext_isa jump-table arm (case 37: base = maverick_libs) and in the internal-twin dispatch gate (cmp $0x25 = 37, 6 hits this pass). The IMG catalog and the GEN matrix both tag it [ct37 HIGH/OBSERVED].
• arch_id 36 (0x24) — INFERRED. It is not byte-read anywhere. It rests on the arch_id = coretype − 1 relation extrapolated from the four observed generations; there is no cmp $0x24 and no v5 NCFW image to confirm it. The GEN matrix escalates it to "doubly inferred" because a second cross-check — the NX_TOPSP = arch_id rule — actually fails for MAVERICK (the enum slot 36 is a MAVERICK_NX__REMOVED__ placeholder; the real MAVERICK_NX_TOPSP sits at index 54). Tag [arch_id 36 MED/INFERRED]; always carry the 36* asterisk.

The relation that ties them is coretype = arch_id + 1; it is that −1 relation — not any coretype stride — that extends the v5 arch_id to 36. (Do not assert a flat +8 coretype stride: the observed set {6, 13, 21, 29, 37} is +7 then +8, +8, +8.)

CORRECTION — there is an OPEN cross-page question on whether ct37 is fully OBSERVED, and this ledger does not silently resolve it. The IMG/GEN/CCL pages tag coretype 37 OBSERVED (a live jump-table arm and a cmp $0x25 gate). The NCFW page, which owns the v5 file-absence finding, reaches the same arch_id conclusion but frames the whole v5 region as "every v5/MAVERICK claim is INFERRED or ABSENT, never OBSERVED" — i.e. it does not separately re-assert ct37 as independently OBSERVED, because its own binary (libncfw.so) carries no v5 arm to read. Both are internally consistent (ct37 is OBSERVED in the IMG/GEN binaries, absent in the NCFW binary), but the pages differ on whether to call the v5 surface "header-OBSERVED" or "INFERRED-or-absent." The hard, non-negotiable fact all four pages agree on is the one stated at the top of §4: the v5 NCFW image is FILE-ABSENT. The appendix-internal standardization is now applied (Part-16 reconcile): the one appendix outlier — the device-firmware globals §1.5i CORRECTION that had flipped ct37 to INFERRED — was rewritten to OBSERVED (keeping its true v5-NCFW-image-absent point), so every appendix page now reads [ct37 HIGH/OBSERVED in the IMG/GEN getter binaries; arch_id 36 MED/INFERRED·doubly; v5 NCFW image FILE-ABSENT HIGH/OBSERVED-absence]. The residual cross-Part framing question — whether the NCFW synthesis page should re-assert ct37 OBSERVED or keep its "INFERRED-or-absent" framing (its own libncfw.so carries no v5 arm to read) — is the only piece left for the global cross-Part pass. [CORRECTION]

4.2 The other v5 interiors — INFERRED, per lane

Every lane that touches v5 carries the interior as INFERRED, never OBSERVED:

• GEN / IMG: MAVERICK image interiors are getter-/dispatch-OBSERVED only; the per-v5 device-code decode is a wall; Q7_CC_TOP collective firmware FILE-ABSENT.
• DMA: v5 interiors header-OBSERVED — PSUM_BUF_SZ = 0, no PSUM region; SBUF re-bases to 128 MiB (OBSERVED header values), runtime semantics INFERRED.
• ADDR: the MAVERICK pkl DB structure (323,198 records, 5 views) is OBSERVED; what a v5 address does in silicon is INFERRED; the byte-grounded behavioral reference is the CAYMAN flat YAML.
• STRUCT: NRTUCODE_CORE_MAVERICK_* exist only behind #if NRTUCODE_INTERNAL_NAMES; no byte-grounded Maverick struct interior is observable [LOW × INFERRED].
• CSR: no v5 register schema ships; maverick/address_map/ is per-die C headers + pkl/json mirror only; interior register layout INFERRED.
• INT: the Maverick nsm.json ships and is byte-identical to Cayman (OBSERVED-on-disk), but the v5-interior behaviour (13 per-IP-block INTCs, per-die 119-entry apex) is INFERRED.
• SEC: the pass_on_miss + master_prot invariants are frozen across SUNDA→CAYMAN→MARIANA, but the Maverick remapper geometry is CARRIED, not re-decoded.
• CC: the MXTENSOR_V2 handler body (the v5 MX interior) is header-OBSERVED only and FLIX-desynced → INFERRED; MAVERICK ships no MAVERICK_NX_POOL_DEBUG image.

GOTCHA — never fabricate a v5 byte. No v5 arch_id byte, no v5 collective firmware, no v5 silicon part-binding is ever asserted as fact. The encoding cover (§1.3) holds across v5 because it is gen-invariant; everything v5-firmware-internal is INFERRED or file-absent, flagged on every use. [HIGH/OBSERVED on the file-absence; the interiors INFERRED]

5. Adversarial self-verification — the five strongest claims, re-challenged this pass

Each claim re-challenged against its owning page and the binary before this page was written.

1. "Value semantics 100% (864/864)." Challenge: is 864 a decompile grep or a binary symbol count? Resolved: nm -D libfiss-base.so | rg -c 'module__xdref_' = 864 this pass (and the .symtab count is also 864); the VAL capstone §6.3 reads "Value semantics: 100% known" and the verdict A.2 "864 / 864 = 100%". Survives. [HIGH/OBSERVED]

2. "~95% execution-validated, ~2.09M comparisons, 0 firmware bugs." Challenge: is the 2.09M a round number, and is the 0 transcribed? Resolved: the VAL capstone §6.2 is explicit that 2.09M = ≈0.60M summable + ~1.49M fp/MAC/4-leg CARRIED, and that the 0-mismatch count is summable on every family (re-confirmed by 18 representative leaves dlopen'd and called). The ~95% is MED on the fraction, HIGH on the fact. Survives, honestly bounded. [HIGH/OBSERVED 0-bugs; MED ~95%; CARRIED 1.49M remainder]

3. "Certified-perfect cover 1534/1607/12642." Challenge: do the counts reproduce and pair correctly? Resolved: nm libisa-core.so gives 12569 placements and 1534 distinct mnemonics this pass; 1534 + 73 = 1607 and 12569 + 73 = 12642 (exact); the valid pairs are 1534 ↔ 12569 (shipped) and 1607 ↔ 12642 (pre-fold), never the cross-pair. Survives. [HIGH/OBSERVED]

4. "≥97% reimplementation-grade for v2–v4; v5 header-OBSERVED + bounded-INFERRED." Challenge: is the ≥97% defensible, and is v5 correctly bounded? Resolved: the verdict A.2 net grade states exactly "≥97% coverage for v2–v4" and "header-OBSERVED + bounded-INFERRED reference for v5 and v1"; every v5-touching lane in §4.2 carries the interior as INFERRED, and the v5 NCFW image is the file-absent hard fact. Survives. [HIGH/INFERRED over the named denominators]

5. "The per-lane walls are real boundaries, and the v5 seam is ct37-OBSERVED / arch_id-36-INFERRED." Challenge: is any wall actually a hidden knowledge gap, and is the v5 seam collapsed? Resolved: every WALL column entry maps to a closability tag in the Walls Model (corpus / license / hardware / static / fundamental) — none is a missing decode or value; and the v5 seam is stated as both facts with the open cross-page divergence flagged for Part-16 (§4.1 CORRECTION), not silently picked. Survives. [HIGH/OBSERVED on the walls; CORRECTION-flagged on the ct37 divergence]

All five survive re-challenge against the owning pages and the binary.

Single strongest CORRECTION: the coretype 37 / arch_id 36 v5 seam is not one fact but two on opposite sides of the OBSERVED/INFERRED line, and the pages diverge on how to label the v5 surface. coretype 37 is byte-OBSERVED in the IMG/GEN getter binaries (a live case 37 jump arm and a cmp $0x25 gate); arch_id 36 is INFERRED (doubly — it rests on coretype − 1 and the NX_TOPSP = arch_id cross-check fails for v5). The NCFW page, owning the v5 file-absence, frames the whole v5 region as "INFERRED-or-absent" because its own binary carries no v5 arm. The one hard fact all pages agree on is that the v5 NCFW image is FILE-ABSENT. This ledger states both halves and flags the labeling divergence for the Part-16 reconcile rather than resolving it silently.

6. Cross-references

This page is the completeness anchor; it cross-links the verdict it feeds, the two companion registers, and every lane's owning synthesis page.

The anchor and its companions:

• The Reimplementation Verdict & Open-Questions Map — the navigable verdict this ledger is the long-form accounting behind; it quotes the §1 headline fractions.
• The Confidence & Walls Model — the [CONF/PROV] tag system every cell uses and the named-wall closability taxonomy (§3).
• The Open-Questions Register (appendix/open-questions-register.md) — the per-residual why-unreachable / what-would-close-it, partitioned by closability; the companion register to this coverage accounting (referenced by title; lands in the sidebar when committed).

Per-lane owning synthesis pages (one per row of §2):

• ISA — coverage tally · semantics coverage ledger · formal ISA model
• ISS — oracle synthesis · semantic synthesis
• VAL — the per-family pass/fail capstone
• HW — microarch synthesis
• FW — opcode-catalog ledger
• IMG — firmware-image catalog
• GEN — master capability matrix
• ABI — ABI synthesis
• RT — runtime synthesis
• DMA — data-movement reference
• CCL — collective architecture synthesis
• NCFW — LX-ISA / naming / arch-id synthesis
• NEFF — format reference
• CC — dtype/engine fan-in synthesis
• STRUCT — struct-census overview · exec-state census
• CSR — notific/SDMA residual
• ADDR — unified SoC memory map
• INT — NSM flow unified
• SEC — security synthesis

No silicon-generation, gen-count, or codename is inferred as a hard fact anywhere on this page: v2–v4 (SUNDA / CAYMAN / MARIANA / MARIANA_PLUS) are byte-grounded and execution-validated; v5 (MAVERICK) and v1 (TONGA) are header-OBSERVED + bounded-INFERRED, with the v5 NCFW image stated as the file-absent hard fact and every v5 interior flagged INFERRED.