synth#1436: built the tracer they asked for, and it RETIRED the hypothesis both sides held (AFD-134)

[avrabe]

synth#1436 asked jess for one measurement and said why it could not be read statically. Built the instrument, took the measurement — and it retired the hypothesis both sides held.

"the QEMU run, watching which addresses the rotation's quaternion loads actually resolve to against the ones the attitude update stores. That decides it without reconstructing the dataflow."
"all 236 r11 accesses are register-offset, none constant-offset. So 'the update writes one field, the rotation reads another' cannot be settled by comparing offsets — the addresses are computed at runtime."

The result, which contradicts what jess proposed

The persistent quaternion is bit-identical between wasmtime and the lowered run — wasm offset 0xac18, at ticks 1, 2, 3, 15 and 16. Identified by value, not by guessing which slot it is: the address is whichever one the parked quaternion words were stored to.

That retires the lagged / stale-attitude reading. jess proposed it from the tick-16 numbers; synth adopted it ("The lagged-attitude reading is now mine too") and wrote it into the v0.80 plan. A stale attitude would appear at that offset. It does not. The attitude state agrees; only what is computed from it diverges. Retracted explicitly rather than quietly dropped, because it is in synth's plan on jess's evidence.

And a sharper signature than AFD-125 could give

Looking for the quaternion suggested a better instrument than the tracer: dump all 64 KiB of linear memory from both runtimes and diff it. The module is fused --memory shared and the image maps linmem at 0x20000000, so the same offset means the same thing on both sides.

Return area at tick 16, field by field:

qw qx qy qz	same, bit-exact
pos-n pos-e pos-d	DIFFER — arm positive, wasmtime negative, all three
vel-n vel-e vel-d	DIFFER — arm positive, wasmtime negative, all three
wx wy wz	same (gyro passthrough)
innovation	same

Six fields differ and all six disagree in sign — 1 in 64 under independent signs. The split is not arbitrary either: what agrees is exactly the quaternion, the gyro passthrough and the innovation; what differs is exactly the translational sub-vector, the part that depends on rotating the accelerometer by a quaternion that is itself bit-exact. AFD-125 saw four differing words at tick 1; at tick 16 it is all six, with a pattern four words could not have shown.

Over all 16,384 words: 744 masked (ARM still holds the harness's 0xdeadbeef paint where wasmtime zero-inits — three quarters of the raw differences, and counting them would be a vacuous positive), 11 ULP-close, 217 divergent, and zero omitted stores — no offset where ARM holds the paint and wasmtime wrote a value. So the lowering is not dropping stores; it computes different values. A clean elimination.

Stated as a hypothesis, not a conclusion: the sign pattern is measured; "therefore the sign of the rotation or the gravity subtraction is wrong in the lowering" is not. The magnitudes differ too, so it is not a pure inversion, and naming the instruction still needs synth's disassembly. jess has no function mapping for these pcs and will not guess one and present the guess as a measurement — AFD-127 was exactly that error.

And then the term itself — the sharpest result

What, quantitatively, is the translational divergence? A strapdown inertial update is v_nav += (R(q)·a_body + g_nav)·dt, where + g_nav is the gravity compensation: an accelerometer at rest reads specific force, +1 g upward, and the compensation cancels it so a stationary vehicle integrates ≈ zero velocity. Drop that addend and the vehicle appears to accelerate downward at g forever — vel-d(n) = n·g·dt.

Measured per tick, from the trace's writes to the return area's vel-d slot:

  vel-d(n) / (n·g·dt) = 1.0000 1.0000 1.0000 1.0000 1.0001 … 1.0002 1.0003   (n = 1..16)
  wasmtime:             vel-d(1) = 0,  vel-d(16) = -1.867e-08

Sixteen consecutive ticks tracking n·g·dt to three parts in ten thousand. Not a rounding difference, not a stale read, not an emulator artefact — one missing or zero-valued addend. The drift from 1.0000 to 1.0003 is the attitude moving slightly off identity, which is what should happen.

And it explains the sign pattern rather than sitting beside it: with gravity uncancelled the translational sub-vector is dominated by a term of definite sign, while wasmtime's are the small tilt residuals of the opposite sign.

A correction I made mid-measurement

My first reading was that ARM matched the physics and wasmtime did not: with an identity attitude, gravity on body z "should" land on the down axis, and ARM's vel-d is g·dt to 1 ulp while wasmtime's is 0. I was close to reporting that the divergence ran the opposite way round to how AFD-125 frames it.

It is wrong. g·dt is the physics of free fall, not of a compensated inertial update. For a vehicle at rest the right answer is ≈ zero — wasmtime's. The 1-ulp agreement with a closed form is not ARM being right; it is ARM integrating an uncompensated accelerometer, and the closed form it matches is the one for the defect. What caught it was asking which closed form, not whether it matched one.

Re-checkable from committed evidence

repro/synth-1436/veld-arm-16ticks.txt holds the sixteen measured words, so the fit re-runs in a second with no emulator and no 20 MB trace:

tools/cascade-differential/gravity-residual.py --arm-words repro/synth-1436/veld-arm-16ticks.txt

Both paths — committed words and extraction from the trace — were run and agree. The classifier has three outcomes (UNCOMPENSATED / COMPENSATED / NEITHER), and its self-test requires a half-n·g·dt series and a quadratic series to both come back NEITHER — which is what stops a classifier that always answers UNCOMPENSATED from passing the positive case the headline rests on. Gated in rivet-validate asserting exit 1 exactly: a 0 would mean the committed series stopped showing the defect, a 2 means it could not be read, which is not a pass.

Stated as a hypothesis, not a conclusion: wasmtime defines the semantics, so its behaviour is the module's, and the lowered run deviating from it localises the defect to the lowering rather than to relay's components or meld's fusion. But whether the addend is absent, zeroed, or landing on another axis — and which instruction — still needs synth's disassembly. This measures the symptom to three parts in ten thousand; it does not name the instruction.

What is shipped

• hardware/qemu/memtrace/ — the TCG plugin. QEMU 11.1.1 accepts -plugin and ships none, so this is the whole supply. Records <seq> <pc> <addr> <bytes> <R|W> <value>: the sequence number makes order recoverable, which is the question; the value makes the quaternion a lookup rather than an inference. build.sh compiles against the installed qemu's header — the API is not stable across versions (v7 changed the translate callback's signature) — and then proves the plugin loads and observes accesses before reporting a successful build.
• tools/cascade-differential/linmem-{capture.sh,differential.py} — one command for both dumps and the classified diff.
• tools/cascade-differential/gravity-residual.py — the per-tick fit against n·g·dt, runnable from the committed words.

Two failures of my own, kept because they are reusable

A flooding positive is as useless as a vacuous zero. The first predicate — find an address loaded with a value another address has moved on from — returned 54,251 events over 1,662 address pairs, including symmetric pairs (A→B and B→A). Cause: wasm's shadow stack lives in linear memory, so most of that traffic is frame slots recycling the same values every tick. That is "the predicate is not specific", not 1,662 defects, and it is reported that way.

A stated blind spot. Value-identity only works for distinctive values. Measured: 15,193 of 15,295 stored values go to ≤ 8 addresses; the only ones above 16 are deadbeef (1,792), 0 (987), 1.0 (62), -0.0 (56). So it cannot see a stale copy of the tick-1 quaternion, which is exactly the identity (1,0,0,0). Ticks 2..n are covered, and the tool prints the exclusion rather than letting a reader assume full coverage.

Gated in both directions

Both tools are classifiers, and a classifier nobody has watched mis-sort is a classifier nobody has checked. linmem-differential's self-test requires 1 ulp → ULP-CLOSE, a sign flip → DIVERGENT, the sign flip to stay divergent at an absurd --ulp threshold (otherwise the classification collapses to one bucket and "six of six differ in sign" would be an artefact of the tool), paint-vs-zero → masked, paint-vs-a-value → reported as an omitted store. analyse.py's requires an injected stale copy to be found, a one-variable control to be not found, a non-distinctive value to be reported as skipped rather than "none found", and the segmentation guard to refuse a wrong tick count.

Both run in rivet-validate — hardware-free and dependency-free on purpose, so they gate on every run rather than only where a bench exists.

linmem-capture.sh asserts its own precondition before reporting anything: the quaternion at 0xac18 must agree bit-for-bit on both sides, which four f32 words would not do by chance if the layouts did not correspond. If that ever fails it refuses, rather than diffing two unrelated layouts.

The traced run reproduces AFD-125/132's parked words exactly, so this is the same execution the silicon result was measured on.

Checks

rivet validate PASS (589 warnings). check-workflow, check-consumers, check-catalog, check-realm all green; build.sh green including its load-and-observe smoke; linmem-capture.sh runs end to end. .scratch/linmem is now declared in the consumers inventory — it was invisible to that gate's literal-path matcher, so the green was correct but the directory was unaccounted for.

Recorded as AFD-134.

🤖 Generated with Claude Code

https://claude.ai/code/session_017EKh2onUHpWSUiAEqWxfy2