sots-re/verify/results/fpu-cw/run-1a7f/shim.trace.jsonl.gz
alex 849c5069fc lane F: x87 precision sensitivity measured; STATE_CHECKSUM 3.5 closed
Seven End Turns from ref-turn2.sav on VM140, six control words, whole-state
checksum on every post-turn autosave.

53-bit and 64-bit x87 give byte-identical state across all 35,394 leaves, so
an x64/SSE port computing in IEEE double has NO double-rounding budget to
preserve and floats=bits is free. Two settings do move state, each reproduced
on a repeat run:

  0x007f (24-bit)   Sys[112 "Gamma Cephei"]/Pop2/PopG/PopC 540000000 -> 540000002
  0x1a7f (round-up) Flt[34 "Beta Fleet"]/Pos/.[0] and /Pos/.[2], 1 ULP each

So the port must hold intermediates at 53 bits and use round-to-nearest --
both SSE defaults, now measured rather than assumed, each with a named
regression witness.

The briefed triple was under-powered: 0x027f is 53-bit (it differs from 0x127f
only in bit 12, infinity control, ignored since the 387) and 0x137f is 64-bit,
not a rounding change. Run as written all three come back identical, and that
would have "proved" something false on both axes that matter.

Evidence the forced word actually held: read-back at each force site plus 38
independent in-pipeline hook samples per run spanning turn phases 4, 6 and 8,
all reading the forced value. Mars::Application::Run calls
_controlfp(0x50000,0x3070300) at 0x0089f606 every frame, which is 0x127f, so
forcing at StrategyClient::EndTurn is wiped before the turn runs;
StrategyServer::BeginProcessTurn is the point that works.

Also re-confirms the End-Turn determinism oracle on engine cef889e:
bb4fd9ac... / 978041ac... unchanged.

New tools: verify/fpu-cw/cw_census.py, verify/fpu-cw/trace_bitdiff.py (the
latter exists because under a forced 24-bit word the CRT's own %g rendering
degrades, so trace text is not a valid comparison surface).
2026-09-08 05:07:53 -04:00

114 KiB