alex/sots-re
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

state-checksum: whole-state diagnostic checksum harness (lane C)

Browse source 
The complement to the per-function compare harness. Instead of "did this
function's declared outputs match", it asks "is the entire simulation state
still identical" -- so no region-declaration mistake can hide from it.

Coverage is PROVED, not declared: the digest tree is re-serialised and compared
byte-for-byte against the inflated save on every run. When that reconstruction
reproduces the stream, the whole file is a function of the digest's inputs. A
run that cannot account for the file says so and exits non-zero. This is the
direct answer to B4's three hooks that printed "0 diverged" over an empty
region set.

It localises. The root is the fold of a per-subsystem / per-object tree with
named objects, so the known load->re-save delta reports as exactly five leaves
-- /Summary/Checksum and four /Sim/players/Player[...]/Status 4->0 -- naming the
two Singularity players by id where the raw byte diff could only say "1st of
two". One real End Turn reports as 108 fully attributed differences.

Float-parity policy is explicit and strict by default (STATE_CHECKSUM.md 3):
raw IEEE-754 bits; a `canonical` policy for signed zero and NaN payloads only;
and deliberately NO tolerant hashing mode, because quantisation moves the cliff
rather than removing it and destroys the roll-up. Tolerance lives in the differ
as --ulps, applied after localisation. Corpus census: 0 NaN, 0 -0.0, 0
subnormals across 4,474 float leaves, so the strict default costs nothing today
and a test fails the day that changes.

Validated on the real saves (verify/results/state-checksum/): 10 files, 4
distinct contents, all STABLE + COVERED; chain record/verify works on the real
turn1-3 saves. The VM-driven replay loop is designed (section 5) but UNRUN.

Section 3.5 names the one question the host side cannot settle -- whether the
turn pipeline depends on x87 intermediate precision -- and the experiment that
would: force fpu_cw to 0x027f / 0x127f / 0x137f across End Turn and checksum
the three autosaves.

Also recorded: Summary.Checksum is NOT a byte sum over the inflated stream nor
a sum over the int leaves (both ruled out), so nobody repeats those two.

38 tests; sots-engine untouched, clean_room_check.sh OK.
This commit is contained in:
alex 2026-09-08 03:46:34 -04:00
parent 1b893e57c3
commit fdd0b72b7a
14 changed files with 1322 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
campaign/board.md
View file

@ -74,6 +74,6 @@ Status flow: `backlog → in-progress → mapped → verified` (or `blocked`).
| B1 replace double-run | verify | backlog | — | 0% | 2026-09-08 | ComputeBudget replace mode runs the original a second time to harvest budget slots; ComputeOutput repairs ships in orbit as a side effect, so this is a real per-turn double effect on objects no region covers. Needs a design fix (harvest without re-running, or declare+revert) | | B1 replace double-run | verify | backlog | — | 0% | 2026-09-08 | ComputeBudget replace mode runs the original a second time to harvest budget slots; ComputeOutput repairs ships in orbit as a side effect, so this is a real per-turn double effect on objects no region covers. Needs a design fix (harvest without re-running, or declare+revert) |
| ReVa MCP link drop (workaround) | meta | verified | high | 100% | 2026-09-08 | The ReVa MCP client link dropped mid-session while the CT111 server stayed healthy (systemd active, :8080 listening, valid key -> 200). `tools/reva_call.py <tool> '<json>'` calls the same server over plain HTTP (initialize -> notifications/initialized -> tools/call; replies are SSE with a leading `id:` line, initialize is plain JSON). Key is NEVER stored in the repo: $REVA_KEY, else ~/.claude.json, else ssh to the CT properties file. Use this whenever mcp__plugin_ReVa_ReVa__* is unavailable | | ReVa MCP link drop (workaround) | meta | verified | high | 100% | 2026-09-08 | The ReVa MCP client link dropped mid-session while the CT111 server stayed healthy (systemd active, :8080 listening, valid key -> 200). `tools/reva_call.py <tool> '<json>'` calls the same server over plain HTTP (initialize -> notifications/initialized -> tools/call; replies are SSE with a leading `id:` line, initialize is plain JSON). Key is NEVER stored in the repo: $REVA_KEY, else ~/.claude.json, else ssh to the CT properties file. Use this whenever mcp__plugin_ReVa_ReVa__* is unavailable |
| event posting API | subsystem | mapped | high | 90% | 2026-09-08 | RECOVERED (lane E, `findings/subsystems/events.md`). Container: `EventStorage` embedded at `ServerPlayer+0x29c` (0x1c), `EvNxID` at +0x14 = player+0x2b0 — exactly the guard's byte run. Nested `vector<TurnEvents{int EvTurn; vector<PlayerEvent>}>`, record 0x74 B, tags `EvEID EvDsc EvMsg EvImg EvLoc EvPos EvAct EvCID`; layout confirmed field-by-field against turn3-state.sav, which CONTAINS the overbudget record. Entry point `int __thiscall EventStorage::PostEvent(this, string BYVAL, string BYVAL, obj*, Vector3*, turn, const char* img, int act)` 0x008862b0 RET 0x4c — **161 call sites in 113 functions, the whole sim's event API**. B3 defect fully explained: 0x00587b97, in the completion-roll-FAILED branch under `!wasDone && nowDone && owner`. 3 note corrections (EvPos is FLT_MAX not inf; the save array is turn-bucketed not flat; TECHS_UNLOCKED has no parent clause). 56 entries in addresses.json; 11 prototypes + 13 labels + 12 comments + 2 structs written back to Ghidra. Engine: `sots-engine` branch `wip/events` a7348be, `src/game/events` + 112 checks, ctest 32/32. NOT YET WIRED INTO A HOOK — see `docs/E-events.md` for the proposed region/Coverage change | | event posting API | subsystem | mapped | high | 90% | 2026-09-08 | RECOVERED (lane E, `findings/subsystems/events.md`). Container: `EventStorage` embedded at `ServerPlayer+0x29c` (0x1c), `EvNxID` at +0x14 = player+0x2b0 — exactly the guard's byte run. Nested `vector<TurnEvents{int EvTurn; vector<PlayerEvent>}>`, record 0x74 B, tags `EvEID EvDsc EvMsg EvImg EvLoc EvPos EvAct EvCID`; layout confirmed field-by-field against turn3-state.sav, which CONTAINS the overbudget record. Entry point `int __thiscall EventStorage::PostEvent(this, string BYVAL, string BYVAL, obj*, Vector3*, turn, const char* img, int act)` 0x008862b0 RET 0x4c — **161 call sites in 113 functions, the whole sim's event API**. B3 defect fully explained: 0x00587b97, in the completion-roll-FAILED branch under `!wasDone && nowDone && owner`. 3 note corrections (EvPos is FLT_MAX not inf; the save array is turn-bucketed not flat; TECHS_UNLOCKED has no parent clause). 56 entries in addresses.json; 11 prototypes + 13 labels + 12 comments + 2 structs written back to Ghidra. Engine: `sots-engine` branch `wip/events` a7348be, `src/game/events` + 112 checks, ctest 32/32. NOT YET WIRED INTO A HOOK — see `docs/E-events.md` for the proposed region/Coverage change |
| state-checksum replay harness | verify | in-progress | — | 0% | 2026-09-08 | Lane C: whole-state per-turn checksum as the COMPLEMENT to per-function compares (no region-declaration mistake can hide from it). Diagnostic tree that localises WHICH object moved, explicit float-parity policy (float32 + fpu_cw 0x127f + fistp ties-to-even; matters for the future x64/SSE port). Replay loop designed but unrun - lane R holds VM140 | | state-checksum replay harness | verify | verified | high | 90% | 2026-09-08 | Lane C: `verify/state-checksum/` (tool, 38 tests, `STATE_CHECKSUM.md`, evidence in `verify/results/state-checksum/`). Whole-state digest tree; **coverage is PROVED by byte-for-byte re-serialisation**, not declared - the answer to empty-region-set green verdicts. Localises: the known load->re-save delta reports as exactly 5 named leaves (`/Sim/players/Player[496 "Singularity"]/Status: 4 -> 0`, `/Summary/Checksum`), and one real End Turn as 108 attributed diffs. All 10 saves STABLE + COVERED. Float policy = exact bits by default, `canonical` for -0.0/NaN only, **tolerance deliberately not a hashing mode** (it lives in `--ulps` on the differ); corpus has 0 NaN/-0.0/subnormals so canonical is a no-op today. Chain record/verify validated on the real turn1-3 saves. REMAINING 10%: the VM-driven replay loop is designed (§5) but UNRUN - needs the VM holder. Open question named in §3.5 with the experiment that settles it (force `fpu_cw` 0x027f/0x127f/0x137f across End Turn, checksum the three autosaves) |
| MoveFleet position ULP divergence | phase2 | in-progress | — | 0% | 2026-09-08 | Lane M. FIRST arithmetic divergence caught by BEHAVIOURAL compare rather than static reading: 8 of 45 calls differ by 1 ULP on a position component (worst 64 ULP at a near-zero result; absolute error ~1.2e-7 everywhere = half an ULP of the INPUTS) => one rounding too many/few in the position update. Step length and all ship ranges match. B4 saw only 1 moving call and it still matches 4 of 5 moves, which is exactly why 1-call coverage is not evidence. All 15 moving calls are the same straight-run waypoint type; types 2-5 never occurred | | MoveFleet position ULP divergence | phase2 | in-progress | — | 0% | 2026-09-08 | Lane M. FIRST arithmetic divergence caught by BEHAVIOURAL compare rather than static reading: 8 of 45 calls differ by 1 ULP on a position component (worst 64 ULP at a near-zero result; absolute error ~1.2e-7 everywhere = half an ULP of the INPUTS) => one rounding too many/few in the position update. Step length and all ship ranges match. B4 saw only 1 moving call and it still matches 4 of 5 moves, which is exactly why 1-call coverage is not evidence. All 15 moving calls are the same straight-run waypoint type; types 2-5 never occurred |
| ObservedTech append (undeclared) | verify | backlog | — | 0% | 2026-09-08 | Lane R's guards caught a vector<ObservedTech> append at `player+0x274` during SetResearched. It is SERIALIZED state and appears in NO coverage note anywhere - found only because guards localise rather than just flag a moved hash. Needs a declared region + a model in ours | | ObservedTech append (undeclared) | verify | backlog | — | 0% | 2026-09-08 | Lane R's guards caught a vector<ObservedTech> append at `player+0x274` during SetResearched. It is SERIALIZED state and appears in NO coverage note anywhere - found only because guards localise rather than just flag a moved hash. Needs a declared region + a model in ours |

74
verify/results/state-checksum/chain-turn1-3.json Normal file
View file

@ -0,0 +1,74 @@
{
"format": "sots-state-chain/1",
"policy": {
"floats": "bits",
"mask": "none",
"digest": "blake2b-128",
"readerFingerprint": "fe5a6f7cd4ae7910"
},
"turns": [
{
"name": "turn1-state.sav",
"turn": 1,
"root": "9bbcbd4945cd8319b65d7d7958772ee0",
"coverage": true,
"subsystems": {
"/Summary": "c601faf8435ca9dd13f0d76f790d6447",
"/CreateParams": "68913c619976ba5f4fa719a7126156aa",
"/Sim/RNG": "0a82080734aaa2d4f3e986036f147963",
"/Sim/Attrib": "cea50f5077af4e42ee02fbbe7b2f8ffd",
"/Sim/turnstats": "b3e7593a4742ebc40a97000159063905",
"/Sim/players": "5c843fefbf911315288f059986c5f7e5",
"/Sim/systems": "8391940f1bb84af6ad3260fdf4390892",
"/Sim/fleets": "db0c730bfa7e21b0b449c1bb66d7fbf7",
"/Sim/NdGr2": "7771763e19ec2652c8c11864ad8e4a10",
"/Sim/trdmgr": "a1139ab953664ab1543ff42faa59aba6",
"/Sim/spymgr": "99c457b5334248e71d063f948ebd7f0c",
"/Sim/SvSctOb": "f9e074a56abb0d1ce82432fa2e1d2215",
"/CDT": "a3f7780ee36905117987374012d1586d"
}
},
{
"name": "turn2-state.sav",
"turn": 2,
"root": "aa85fe76d412cdb3a0e7e52c8f0ca9e2",
"coverage": true,
"subsystems": {
"/Summary": "42b2094efe6e285a3eddc0518a842c69",
"/CreateParams": "68913c619976ba5f4fa719a7126156aa",
"/Sim/RNG": "e9625f2b86f93f8ccf84dcd1b1833d6a",
"/Sim/Attrib": "cea50f5077af4e42ee02fbbe7b2f8ffd",
"/Sim/turnstats": "c32bab57e99cdf797510872b170243f9",
"/Sim/players": "fa7f5ad40afed20848714e38cfd360fb",
"/Sim/systems": "1a36f0d18f0d8babfb3b48c0c273c3f4",
"/Sim/fleets": "666872a3ce06721807e0487e2801f0b7",
"/Sim/NdGr2": "7771763e19ec2652c8c11864ad8e4a10",
"/Sim/trdmgr": "a1139ab953664ab1543ff42faa59aba6",
"/Sim/spymgr": "99c457b5334248e71d063f948ebd7f0c",
"/Sim/SvSctOb": "6cd7196a38f53574292b3bde3ee424a8",
"/CDT": "a3f7780ee36905117987374012d1586d"
}
},
{
"name": "turn3-state.sav",
"turn": 3,
"root": "5ac4a24197e82de49f3077cd8dd25fad",
"coverage": true,
"subsystems": {
"/Summary": "b375baaf6aab9da5202f30fd4dc85104",
"/CreateParams": "68913c619976ba5f4fa719a7126156aa",
"/Sim/RNG": "0978fdf34ff7962f76c2de810dc93e0a",
"/Sim/Attrib": "cea50f5077af4e42ee02fbbe7b2f8ffd",
"/Sim/turnstats": "f067f6b95f21ed0ea0d9844a48caa78f",
"/Sim/players": "8a0bf16b7166f7e30b170284ad26ae36",
"/Sim/systems": "ef4caa2237b49b2384bc9ee7cd733a96",
"/Sim/fleets": "0f65b7f9ccb245f6ff105be5d1f69dd1",
"/Sim/NdGr2": "7771763e19ec2652c8c11864ad8e4a10",
"/Sim/trdmgr": "a1139ab953664ab1543ff42faa59aba6",
"/Sim/spymgr": "99c457b5334248e71d063f948ebd7f0c",
"/Sim/SvSctOb": "d30210dd844215010d68c7d013fa4da0",
"/CDT": "a3f7780ee36905117987374012d1586d"
}
}
]
}

9
verify/results/state-checksum/chain.txt Normal file
View file

@ -0,0 +1,9 @@
recorded 3 turns -> /home/alex/sots-re/verify/results/state-checksum/chain-turn1-3.json
turn 1 9bbcbd4945cd8319 cov-ok turn1-state.sav
turn 2 aa85fe76d412cdb3 cov-ok turn2-state.sav
turn 3 5ac4a24197e82de4 cov-ok turn3-state.sav
$ state_checksum.py --chain chain-turn1-3.json turn1 turn2 turn3
turn 1 MATCH 9bbcbd4945cd8319 turn1-state.sav
turn 2 MATCH aa85fe76d412cdb3 turn2-state.sav
turn 3 MATCH 5ac4a24197e82de4 turn3-state.sav

36
verify/results/state-checksum/float-census.txt Normal file
View file

@ -0,0 +1,36 @@
# float census -- classes that separate the 'bits' and 'canonical'
# policies are: negative zero, NaN. Classes an x87 -> SSE port is
# most likely to move are: subnormal, and anything near FLT_MAX.
turn1-state.sav: 1101 float leaves
576 ordinary e.g. /CreateParams/MapP/.[1]/.[1]/.[0]/.[0]
275 positive zero e.g. /Summary/Session/TMRS/TQTLE
192 exact integer e.g. /Summary/Session/TMRS/TCTL
58 FLT_MAX (0x7f7fffff) e.g. /Summary/Session/TMRS/TSTL
turn2-state.sav: 1116 float leaves
581 ordinary e.g. /CreateParams/MapP/.[1]/.[1]/.[0]/.[0]
279 positive zero e.g. /Summary/Session/TMRS/TQTLE
198 exact integer e.g. /Summary/Session/TMRS/TCTL
58 FLT_MAX (0x7f7fffff) e.g. /Summary/Session/TMRS/TSTL
turn3-state.sav: 1141 float leaves
599 ordinary e.g. /CreateParams/MapP/.[1]/.[1]/.[0]/.[0]
281 positive zero e.g. /Summary/Session/TMRS/TQTLE
203 exact integer e.g. /Summary/Session/TMRS/TCTL
58 FLT_MAX (0x7f7fffff) e.g. /Summary/Session/TMRS/TSTL
Autosave EndTurn - turn3.sav: 1116 float leaves
581 ordinary e.g. /CreateParams/MapP/.[1]/.[1]/.[0]/.[0]
279 positive zero e.g. /Summary/Session/TMRS/TQTLE
198 exact integer e.g. /Summary/Session/TMRS/TCTL
58 FLT_MAX (0x7f7fffff) e.g. /Summary/Session/TMRS/TSTL
all distinct saves combined:
2337 ordinary
1114 positive zero
791 exact integer
232 FLT_MAX (0x7f7fffff)
'canonical' would change 0 leaf/leaves across the corpus (a no-op today).
subnormals: 0 (each one is an x87/SSE parity risk)

13
verify/results/state-checksum/identical-roots.txt Normal file
View file

@ -0,0 +1,13 @@
reader fingerprint: fe5a6f7cd4ae7910
10 file(s), 4 distinct content(s)
sha256:978041acd168b56e 2 file(s) STABLE + COVERED
root 5ac4a24197e82de49f3077cd8dd25fad Autosave - turn3.sav, turn3-state.sav
sha256:a3f9dc4b49fc669c 2 file(s) STABLE + COVERED
root 9bbcbd4945cd8319b65d7d7958772ee0 Autosave EndTurn - turn2.sav, turn1-state.sav
sha256:ab4ac2d7e2977260 3 file(s) STABLE + COVERED
root aa85fe76d412cdb3a0e7e52c8f0ca9e2 Autosave - turn2.sav, Autosave Backup - turn2.sav, turn2-state.sav
sha256:bb4fd9ac89f41e3b 3 file(s) STABLE + COVERED
root a1448e6c1867fc53708810b3a2f9ec77 Autosave EndTurn - turn3.sav, MyGameverify1verify1.sav, verify1.sav
VERDICT: all stable and fully covered

20
verify/results/state-checksum/resave-localisation.txt Normal file
View file

@ -0,0 +1,20 @@
# determinism-oracle.md: loading a post-turn autosave and re-saving it
# changes Player.Status (4->0) on the four turn-participating players
# plus the derived Summary.Checksum. Nothing else.
$ state_checksum.py turn2-state.sav Autosave EndTurn - turn3.sav
A aa85fe76d412cdb3a0e7e52c8f0ca9e2 /home/alex/sots-re/verify/results/saves/turn2-state.sav
B a1448e6c1867fc53708810b3a2f9ec77 /tmp/saves/Autosave EndTurn - turn3.sav
policy: floats=bits mask=none reader=fe5a6f7cd4ae7910
DIVERGED: 5 leaf difference(s)
/Summary/Checksum: -1205790620 -> -1205790636
/Sim/players/Player[16 "re"]/Status: 4 -> 0
/Sim/players/Player[32 "Fane Lao"]/Status: 4 -> 0
/Sim/players/Player[496 "Singularity"]/Status: 4 -> 0
/Sim/players/Player[512 "Singularity"]/Status: 4 -> 0
$ state_checksum.py turn2-state.sav Autosave EndTurn - turn3.sav --mask resave
A a55e433687fff0e380de2caabf964a31 /home/alex/sots-re/verify/results/saves/turn2-state.sav
B a55e433687fff0e380de2caabf964a31 /tmp/saves/Autosave EndTurn - turn3.sav
policy: floats=bits mask=resave reader=fe5a6f7cd4ae7910 [masked: Checksumx1, Statusx8]
IDENTICAL

86
verify/results/state-checksum/roots.txt Normal file
View file

@ -0,0 +1,86 @@
# state_checksum roots -- 2026-09-08T07:42:52Z
--- sha256:a3f9dc4b49fc669c turn1-state.sav
file: /home/alex/sots-re/verify/results/saves/turn1-state.sav
root: 9bbcbd4945cd8319b65d7d7958772ee0
policy: floats=bits mask=none digest=blake2b-128 reader=fe5a6f7cd4ae7910
coverage: PROVED (591376 bytes rebuilt == inflated); 34355 leaves, 187545 value bytes
reader: 0 error, 0 warn
subsystems:
c601faf8435ca9dd /Summary 60 leaves 216 B
68913c619976ba5f /CreateParams 228 leaves 907 B
0a82080734aaa2d4 /Sim/RNG 1 leaves 2503 B
cea50f5077af4e42 /Sim/Attrib 1 leaves 4 B
b3e7593a4742ebc4 /Sim/turnstats 281 leaves 1156 B
5c843fefbf911315 /Sim/players 28902 leaves 160989 B
8391940f1bb84af6 /Sim/systems 2754 leaves 10482 B
db0c730bfa7e21b0 /Sim/fleets 513 leaves 1880 B
7771763e19ec2652 /Sim/NdGr2 475 leaves 1900 B
a1139ab953664ab1 /Sim/trdmgr 166 leaves 664 B
99c457b5334248e7 /Sim/spymgr 2 leaves 8 B
f9e074a56abb0d1c /Sim/SvSctOb 123 leaves 530 B
a3f7780ee3690511 /CDT 5 leaves 104 B
--- sha256:ab4ac2d7e2977260 turn2-state.sav
file: /home/alex/sots-re/verify/results/saves/turn2-state.sav
root: aa85fe76d412cdb3a0e7e52c8f0ca9e2
policy: floats=bits mask=none digest=blake2b-128 reader=fe5a6f7cd4ae7910
coverage: PROVED (603360 bytes rebuilt == inflated); 35031 leaves, 190807 value bytes
reader: 0 error, 0 warn
subsystems:
42b2094efe6e285a /Summary 60 leaves 216 B
68913c619976ba5f /CreateParams 228 leaves 907 B
e9625f2b86f93f8c /Sim/RNG 1 leaves 2503 B
cea50f5077af4e42 /Sim/Attrib 1 leaves 4 B
c32bab57e99cdf79 /Sim/turnstats 545 leaves 2244 B
fa7f5ad40afed208 /Sim/players 29230 leaves 162841 B
1a36f0d18f0d8bab /Sim/systems 2779 leaves 10582 B
666872a3ce067218 /Sim/fleets 561 leaves 2058 B
7771763e19ec2652 /Sim/NdGr2 475 leaves 1900 B
a1139ab953664ab1 /Sim/trdmgr 166 leaves 664 B
99c457b5334248e7 /Sim/spymgr 2 leaves 8 B
6cd7196a38f53574 /Sim/SvSctOb 130 leaves 558 B
a3f7780ee3690511 /CDT 5 leaves 104 B
--- sha256:978041acd168b56e turn3-state.sav
file: /home/alex/sots-re/verify/results/saves/turn3-state.sav
root: 5ac4a24197e82de49f3077cd8dd25fad
policy: floats=bits mask=none digest=blake2b-128 reader=fe5a6f7cd4ae7910
coverage: PROVED (609080 bytes rebuilt == inflated); 35394 leaves, 192486 value bytes
reader: 0 error, 0 warn
subsystems:
b375baaf6aab9da5 /Summary 60 leaves 216 B
68913c619976ba5f /CreateParams 228 leaves 907 B
0978fdf34ff7962f /Sim/RNG 1 leaves 2503 B
cea50f5077af4e42 /Sim/Attrib 1 leaves 4 B
f067f6b95f21ed0e /Sim/turnstats 809 leaves 3332 B
8a0bf16b7166f7e3 /Sim/players 29264 leaves 163187 B
ef4caa2237b49b23 /Sim/systems 2779 leaves 10582 B
0f65b7f9ccb245f6 /Sim/fleets 624 leaves 2295 B
7771763e19ec2652 /Sim/NdGr2 475 leaves 1900 B
a1139ab953664ab1 /Sim/trdmgr 166 leaves 664 B
99c457b5334248e7 /Sim/spymgr 2 leaves 8 B
d30210dd84421501 /Sim/SvSctOb 130 leaves 558 B
a3f7780ee3690511 /CDT 5 leaves 104 B
--- sha256:bb4fd9ac89f41e3b Autosave EndTurn - turn3.sav
file: /tmp/saves/Autosave EndTurn - turn3.sav
root: a1448e6c1867fc53708810b3a2f9ec77
policy: floats=bits mask=none digest=blake2b-128 reader=fe5a6f7cd4ae7910
coverage: PROVED (603360 bytes rebuilt == inflated); 35031 leaves, 190807 value bytes
reader: 0 error, 0 warn
subsystems:
8c7e33a33dc76b3d /Summary 60 leaves 216 B
68913c619976ba5f /CreateParams 228 leaves 907 B
e9625f2b86f93f8c /Sim/RNG 1 leaves 2503 B
cea50f5077af4e42 /Sim/Attrib 1 leaves 4 B
c32bab57e99cdf79 /Sim/turnstats 545 leaves 2244 B
3416ca2128671b1e /Sim/players 29230 leaves 162841 B
1a36f0d18f0d8bab /Sim/systems 2779 leaves 10582 B
666872a3ce067218 /Sim/fleets 561 leaves 2058 B
7771763e19ec2652 /Sim/NdGr2 475 leaves 1900 B
a1139ab953664ab1 /Sim/trdmgr 166 leaves 664 B
99c457b5334248e7 /Sim/spymgr 2 leaves 8 B
6cd7196a38f53574 /Sim/SvSctOb 130 leaves 558 B
a3f7780ee3690511 /CDT 5 leaves 104 B

115
verify/results/state-checksum/turn2-to-turn3.txt Normal file
View file

@ -0,0 +1,115 @@
# one real End Turn (turn 2 -> turn 3), every difference named
A aa85fe76d412cdb3a0e7e52c8f0ca9e2 /home/alex/sots-re/verify/results/saves/turn2-state.sav
B 5ac4a24197e82de49f3077cd8dd25fad /home/alex/sots-re/verify/results/saves/turn3-state.sav
policy: floats=bits mask=none reader=fe5a6f7cd4ae7910
DIVERGED: 108 leaf difference(s)
/Summary/Turn: 2 -> 3
/Summary/Checksum: -1205790620 -> -769976634
/Sim/NMnx: 109 -> 111
/Sim/FleetIDs[]: removed [1744], added [34, 1776] (7 -> 8 entries)
/Sim/ShipIDs[]: removed [], added [1760] (16 -> 17 entries)
/Sim/ModCount: 12 -> 24
/Sim/Frame: 2 -> 3
/Sim/RNG/.: '<raw 2503 B ef4d678696ed4c53>' -> '<raw 2503 B a80459bfd63a006b>'
/Sim/cmbtid: 2 -> 3
/Sim/turnstats/history/hist[0]/stats[2]: only-in-B
/Sim/turnstats/history/hist[1]/stats[2]: only-in-B
/Sim/turnstats/history/hist[2]/stats[2]: only-in-B
/Sim/turnstats/history/hist[3]/stats[2]: only-in-B
/Sim/turnstats/history/hist[4]/stats[2]: only-in-B
/Sim/turnstats/history/hist[5]/stats[2]: only-in-B
/Sim/turnstats/history/hist[6]/stats[2]: only-in-B
/Sim/turnstats/history/hist[7]/stats[2]: only-in-B
/Sim/players/Player[16 "re"]/Sav: 289688 -> 532369
/Sim/players/Player[16 "re"]/Events/EvNxID: 2 -> 3
/Sim/players/Player[16 "re"]/Events/Events/.[EvTurn=3]: only-in-B
/Sim/players/Player[16 "re"]/Events/Events/.[0]: 1 -> 2
/Sim/players/Player[16 "re"]/PvSav: 50000 -> 289688
/Sim/players/Player[16 "re"]/BnkPr: -789323 -> -791290
/Sim/players/Player[16 "re"]/BnkEl: -1594593 -> -1598566
/Sim/players/Player[32 "Fane Lao"]/TechTree/TResDone[106]: 2879 -> 5768
/Sim/players/Player[32 "Fane Lao"]/TechTree/Tbd[106]: 1 -> 2
/Sim/players/Player[32 "Fane Lao"]/Sav: 92651 -> 135486
/Sim/players/Player[32 "Fane Lao"]/Maint: 500 -> 1000
/Sim/players/Player[32 "Fane Lao"]/Events/EvNxID: 2 -> 4
/Sim/players/Player[32 "Fane Lao"]/Events/Events/.[EvTurn=3]: only-in-B
/Sim/players/Player[32 "Fane Lao"]/Events/Events/.[0]: 1 -> 2
/Sim/players/Player[32 "Fane Lao"]/FNG/FNGNum: 1 -> 3
/Sim/players/Player[32 "Fane Lao"]/PvSav: 38100 -> 80751
/Sim/players/Player[32 "Fane Lao"]/BnkPr: -898837 -> -901002
/Sim/players/Player[32 "Fane Lao"]/BnkEl: -1815833 -> -1820206
/Sim/players/Player[32 "Fane Lao"]/ShipRecs/srb[0]: 1 -> 2
/Sim/players/Player[32 "Fane Lao"]/ShipRecs/sri[0]: 1 -> 2
/Sim/players/Player[32 "Fane Lao"]/ShipRecs/srb[3]: 1 -> 2
/Sim/players/Player[32 "Fane Lao"]/ShipRecs/sri[3]: 1 -> 2
/Sim/players/Player[32 "Fane Lao"]/lboid: 1 -> 2
/Sim/players/Player[32 "Fane Lao"]/odes/.[1]/otnL: 2 -> 3
/Sim/players/Player[496 "Singularity"]/dipstats/.[1]/lastally: 2 -> 3
/Sim/players/Player[512 "Singularity"]/dipstats/.[1]/lastally: 2 -> 3
/Sim/players/Player[528 "Alien Menace"]/dipstats/.[1]/lastnap: 2 -> 3
/Sim/players/Player[528 "Alien Menace"]/dipstats/.[2]/lastnap: 2 -> 3
/Sim/players/Player[528 "Alien Menace"]/dipstats/.[3]/lastnap: 2 -> 3
/Sim/players/Player[544 "Peacekeeper Enforcer"]/dipstats/.[1]/lastnap: 2 -> 3
/Sim/players/Player[544 "Peacekeeper Enforcer"]/dipstats/.[2]/lastnap: 2 -> 3
/Sim/players/Player[544 "Peacekeeper Enforcer"]/dipstats/.[3]/lastnap: 2 -> 3
/Sim/players/Player[560 "Von Neumann"]/dipstats/.[1]/lastnap: 2 -> 3
/Sim/players/Player[560 "Von Neumann"]/dipstats/.[2]/lastnap: 2 -> 3
/Sim/players/Player[560 "Von Neumann"]/dipstats/.[3]/lastnap: 2 -> 3
/Sim/players/Player[576 "Independent Colony"]/Sav: 98871 -> 198730
/Sim/players/Player[576 "Independent Colony"]/PvSav: 0 -> 98871
/Sim/players/Player[576 "Independent Colony"]/dipstats/.[1]/lastnap: 2 -> 3
/Sim/players/Player[576 "Independent Colony"]/dipstats/.[2]/lastnap: 2 -> 3
/Sim/players/Player[576 "Independent Colony"]/dipstats/.[3]/lastnap: 2 -> 3
/Sim/systems/Sys[64 "Hyperion"]/ltis: 2 -> 3
/Sim/systems/Sys[64 "Hyperion"]/rcex: 65536 -> 0
/Sim/systems/Sys[64 "Hyperion"]/TShn: 2 -> 3
/Sim/systems/Sys[64 "Hyperion"]/ETS: 2 -> 3
/Sim/systems/Sys[112 "Gamma Cephei"]/Pop2/PopG/PopC: 520000000 -> 540000000
/Sim/systems/Sys[112 "Gamma Cephei"]/PvPop2/PopG/PopC: 500000000 -> 520000000
/Sim/systems/Sys[112 "Gamma Cephei"]/RepCur: 336360.0 -> 336840.0 [15360 ulp]
/Sim/systems/Sys[112 "Gamma Cephei"]/RepMax: 336360.0 -> 336840.0 [15360 ulp]
/Sim/systems/Sys[112 "Gamma Cephei"]/ntdev: 1 -> 2
/Sim/systems/Sys[112 "Gamma Cephei"]/ltis: 2 -> 3
/Sim/systems/Sys[112 "Gamma Cephei"]/TShn: 2 -> 3
/Sim/systems/Sys[112 "Gamma Cephei"]/ETS: 2 -> 3
/Sim/systems/Sys[224 "Spica"]/TShn: 2 -> 3
/Sim/systems/Sys[288 "Ke'Dolarra"]/Pop2/PopG/PopC: 520000000 -> 540000000
/Sim/systems/Sys[288 "Ke'Dolarra"]/PvPop2/PopG/PopC: 500000000 -> 520000000
/Sim/systems/Sys[288 "Ke'Dolarra"]/RepCur: 370000.0 -> 370520.0 [16640 ulp]
/Sim/systems/Sys[288 "Ke'Dolarra"]/RepMax: 370000.0 -> 370520.0 [16640 ulp]
/Sim/systems/Sys[288 "Ke'Dolarra"]/ntdev: 1 -> 2
/Sim/systems/Sys[288 "Ke'Dolarra"]/ltis: 2 -> 3
/Sim/systems/Sys[288 "Ke'Dolarra"]/DefF: 1744 -> 1776
/Sim/systems/Sys[288 "Ke'Dolarra"]/Flt: 1744 -> 1776
/Sim/systems/Sys[288 "Ke'Dolarra"]/TShn: 2 -> 3
/Sim/systems/Sys[288 "Ke'Dolarra"]/ETS: 2 -> 3
/Sim/systems/Sys[304 "Koa’Vo"]/ntdev: 1 -> 2
/Sim/systems/Sys[304 "Koa’Vo"]/ltis: 2 -> 3
/Sim/systems/Sys[304 "Koa’Vo"]/rcex: 268435456 -> 0
/Sim/systems/Sys[304 "Koa’Vo"]/TShn: 2 -> 3
/Sim/systems/Sys[304 "Koa’Vo"]/ETS: 2 -> 3
/Sim/systems/Sys[336 "Kaa’Vaalu"]/ltis: 2 -> 3
/Sim/systems/Sys[336 "Kaa’Vaalu"]/rcex: 65536 -> 0
/Sim/systems/Sys[336 "Kaa’Vaalu"]/TShn: 2 -> 3
/Sim/systems/Sys[336 "Kaa’Vaalu"]/ETS: 2 -> 3
/Sim/systems/Sys[400 "Markab"]/ltis: 2 -> 3
/Sim/systems/Sys[400 "Markab"]/rcex: 65536 -> 0
/Sim/systems/Sys[400 "Markab"]/TShn: 2 -> 3
/Sim/systems/Sys[400 "Markab"]/ETS: 2 -> 3
/Sim/systems/Sys[448 "Kea’Pono"]/ltis: 2 -> 3
/Sim/systems/Sys[448 "Kea’Pono"]/rcex: 65536 -> 0
/Sim/systems/Sys[448 "Kea’Pono"]/TShn[0]: 2 -> 3
/Sim/systems/Sys[448 "Kea’Pono"]/TShn[1]: 2 -> 3
/Sim/systems/Sys[448 "Kea’Pono"]/ETS: 2 -> 3
/Sim/systems/Sys[480 "Ko'Rorkor"]/ltis: 2 -> 3
/Sim/systems/Sys[480 "Ko'Rorkor"]/rcex: 65536 -> 0
/Sim/systems/Sys[480 "Ko'Rorkor"]/TShn: 2 -> 3
/Sim/systems/Sys[480 "Ko'Rorkor"]/ETS: 2 -> 3
/Sim/NumFlts: 7 -> 8
/Sim/fleets/Flt[1744 "Alpha Fleet"]: only-in-A
/Sim/fleets/Flt[34 "Beta Fleet"]: only-in-B
/Sim/fleets/Flt[1776 "Gamma Fleet"]: only-in-B
/Sim/SvSctOb/EncObj[5]/Hives/.[1]/NextQ: 31 -> 32
/Sim/SvSctOb/EncObj[5]/Hives/.[2]/NextQ: 29 -> 30
floats: 4 differ, 0 within 2 ULP

577
verify/state-checksum/STATE_CHECKSUM.md Normal file
View file

@ -0,0 +1,577 @@
# Per-turn state checksum
Status: **validated on the real saves** (`verify/results/state-checksum/`). The replay loop in
§5 is **designed but not run** — it needs VM140, which lane R holds.
`state_checksum.py` computes a whole-state checksum of a `.sav` as a *tree* of per-subsystem
and per-object digests that roll up to one root, and diffs two such trees to name the object
that moved.
```
verify/state-checksum/
state_checksum.py the tool + library
float_census.py classifies every float leaf (evidence for §3)
stability_check.py identical bytes -> identical roots, coverage proved
run_validation.sh regenerates verify/results/state-checksum/
test_state_checksum.py 38 tests
```
---
## 1. Why a whole-state checksum, next to the per-function harness
Every verification the project has today is **per-function**: hook a routine, compare the
regions it declares, print a verdict. That verdict is bounded by the region declaration, and
region declarations have been wrong in both directions:
* B4 found three hooks that printed "0 diverged" while their region set was **empty**.
* The harness audit (`sots-engine/docs/harness-audit.md`) found **23 undeclared side effects**.
* B3's `TechTree::ProcessResearch` passed replace-mode by 40,300 items and was still wrong —
by one unposted `EVENT_RESEARCH_OVERBUDGET` that no declared region covered
(`findings/subsystems/events.md`).
Those are three different failures of the same kind: the verdict was green because the
evidence was narrow, not because the state matched. **Coverage is the evidence; the verdict is
not.**
A whole-state checksum is the complement. It never asks what a function declared. It asks
whether the entire simulation state is still identical, using the strongest oracle this project
has: End-Turn autosaves are **byte-identical across runs and across processes**
(`findings/subsystems/determinism-oracle.md`).
The two are not redundant. The per-function harness says *where in the code* a divergence
started; the state checksum says *that* one exists and *which object* it landed on, and no
region-declaration mistake can hide from it.
### 1.1 What makes this evidence rather than a comforting number
**Coverage is proved, not declared.** After building the digest tree, the tool re-serialises
the parse back into bytes and compares that with the inflated save, byte for byte
(`audit_coverage`, on by default). When the reconstruction reproduces the stream, the whole
file is a function of the digest's inputs — every tag, every value, every frame boundary — so
no state change can be invisible to it. This is the one property that a hand-maintained region
list can never have, and it is the direct answer to the empty-region-set failure: a
`state_checksum.py` run that could not account for the file says `coverage: FAILED at inflated
offset 0x…` and exits non-zero, instead of printing a clean root.
Observed on every save on this host:
```
coverage: PROVED (603360 bytes rebuilt == inflated); 35031 leaves, 190807 value bytes
```
**It localises.** The root is the fold of a tree, and objects carry names, so a divergence is
reported as `/Sim/players/Player[496 "Singularity"]/Status`, not "the hash moved". This is the
same principle that made the harness guards useful — name `player+0x2b0`, do not just say
something changed.
---
## 2. The digest tree
### 2.1 Shape
The tree follows the save's own frame nesting (`SAVE_FORMAT.md` §3), with two foldings applied
so that it reads as a subsystem tree rather than a flat item list:
| fold | what it does | why |
|---|---|---|
| **object tables** | a run of `(PlayerID, Player{})` sibling pairs becomes one `players` group whose children are `Player[16 "re"]`, `Player[32 "Fane Lao"]`, … | `Sim` has 259 flat children; without this there is no "players subsystem" to point at |
| **inline id lists** | `PlayerIDs` + n × `.` becomes one `PlayerIDs[]` node holding the values | one inserted id used to shift every following sibling and produce ~30 spurious "moves" per turn |
Both foldings preserve order and byte span exactly; nothing is dropped, so the reconstruction
audit still proves total coverage. The tables are `PAIR_GROUPS`, `NAME_FIELDS`, `ELEM_KEYS` and
`INLINE_ID_LISTS` at the top of the module.
### 2.2 Naming
* Object frames get their id **and** their in-file name: `Player[16 "re"]`, `Sys[112 "Gamma
Cephei"]`, `Flt[1744 "Alpha Fleet"]`, `Des[592 "Armor"]`. The id is folded into the object's
digest, so two objects with identical bodies and different ids do not collide. (The
determinism-oracle byte diff could only say "1st of two Singularity records"; the tree says
`Player[496 …]` and `Player[512 …]`.) `Ship` frames carry no name field on disk, so a ship is
labelled by id alone — `Ship[1728]`.
* NULL-named (`"."`) element frames are keyed by the first identifying child they carry:
`Events/.[EvTurn=3]`, `ords/.[ordID=…]`.
* A uniquely-named field gets no index at all (`/Sim/players/Player[16 "re"]/Status`).
* Where an index is unavoidable it is the ordinal **among same-named siblings**, so an
insertion elsewhere in the frame does not renumber everything after it.
### 2.3 Digest construction
`blake2b-128`, length-prefixed and domain-separated at every level:
```
leaf = H("leaf", tag, kind, value_key)
object = H("obj", H("id", id_tag, id_bytes), frame_digest)
frame = H("frame", tag, child_digest...)
group = H("group", group_name, member_digest...)
list = H("list", tag, count_bytes, element_key...)
root = H("save", float_policy, mask_preset, top_level_digest...)
```
Order is part of the state, so children are folded in file order. The float policy and the mask
preset are folded into the **root** so a strict root and a lenient root can never be compared by
accident.
Note what is *not* hashed: the human labels of §2.2. Digests consume the **on-disk tag** and the
id bytes; the `"re"` / `"Gamma Cephei"` part of a label is diagnostic metadata only. So improving
the naming tables never invalidates a recorded root — verified in practice when `Flt`'s name tag
was corrected from a guess to the on-disk `FtName` and every root stayed the same.
### 2.4 The digest depends on the reader, not only on the bytes
Each leaf hashes its **inferred kind** alongside its bytes, and that kind comes from
`save_reader.py`'s schema and its int/float classifier (`SAVE_FORMAT.md` §2). The same four
bytes typed `int` and typed `float` produce different digests. That is correct for comparing two
saves parsed by one reader, and dangerous for a chain recorded months earlier, so every run
prints and every chain records a `readerFingerprint` (blake2b-64 of `save_reader.py`), and
`verify_chain` says so loudly when it does not match:
```
!! chain was recorded under save_reader 3f1e…, this is fe5a6f7cd4ae7910
-- re-record before trusting a DIVERGE
```
It is deliberately *not* folded into the digest: a cosmetic reader edit should raise a warning,
not invalidate every recorded root.
### 2.5 Masking is opt-in and audited
Default is **no masking**, so the one known non-idempotent field set (§4) is *localised* rather
than absorbed. `--mask resave` applies the canonicalisation `determinism-oracle.md` prescribes.
Each rule is scoped to a path prefix, not just a tag name, and the run always reports what it hit:
```
policy: floats=bits mask=resave reader=fe5a6f7cd4ae7910 [masked: Checksumx1, Statusx8]
```
A mask that matches nothing prints `[mask matched NOTHING -- check the rule paths]`. A mask
nobody audits is a hiding place, and this project has already been bitten once by a comparison
that quietly covered nothing.
---
## 3. Float-parity policy
This is the subtle part, and it has to be settled now rather than at port time, because the
policy decides what a future x64/SSE standalone is *allowed* to differ by.
### 3.1 What the engine actually does
From `findings/subsystems/formula-gaps.md`:
* State is stored in **float32**. Literals in the code are float32 values widened to double
(`0.05000000074505806`), so the constants themselves are exactly representable as singles.
* `fnstcw` inside a hooked turn-pipeline call returns **`0x127f`**: precision control = 53-bit
(double), rounding = round-to-nearest-even. The FPU is *not* left in 24-bit single precision
by the D3D9 device. So an x87 intermediate rounds to **double** and the caller then narrows to
float32 — two roundings, not one.
* Integer rounding is `fistp`/`fild`, i.e. **ties-to-even**, not truncation and not C's
round-half-away-from-zero.
### 3.2 The save is a narrowing boundary
Everything the checksum sees is a 4-byte IEEE-754 single. Whatever precision the FPU carried
internally, the values that reach the save have already been narrowed to float32. That is a
useful property: the checksum compares state at exactly the level where an x87-vs-SSE
difference either survived the narrowing or vanished in it. It also means the checksum cannot
see a precision difference that got rounded away — which is the right behaviour, because a
difference that does not survive into state is not a state difference.
### 3.3 The policies
| policy | float leaf hashes | separates | default |
|---|---|---|---|
| `bits` | the raw 4 bytes, unchanged | everything, including `-0.0` vs `+0.0` and distinct NaN payloads | **yes** |
| `canonical` | raw bytes, with `-0.0 → +0.0` and every NaN → one quiet NaN (`0x7fc00000`) | everything except those two | no |
`canonical` also normalises a `bool` byte to 0/1. Nothing else is ever normalised.
**Why `bits` is the default.** It is the only policy under which "the roots match" means "the
state is identical". Everything else is a claim about which differences we have decided not to
care about, and this project's whole lesson is that such claims must be earned, stated, and
audited rather than assumed.
**What `bits` catches:** any state difference at all, down to one ULP of one float32 in one
object, plus every non-float change. **What it over-reports:** exactly two cases where a
value-equal result can carry different bits — signed zero and NaN payload. x87 `FLD`/`FSTP`
quiets a signalling NaN where SSE may not; a zero result can pick up a sign from a different
rounding path. `canonical` exists for precisely those two, and for nothing else.
**Corpus evidence** (`verify/results/state-checksum/float-census.txt`, 4 distinct saves,
4,474 float leaves):
```
2337 ordinary
1114 positive zero
791 exact integer
232 FLT_MAX (0x7f7fffff)
'canonical' would change 0 leaf/leaves across the corpus (a no-op today).
subnormals: 0 (each one is an x87/SSE parity risk)
```
No negative zero, no NaN, no infinity, no subnormals. So `canonical` is a **no-op below the
root** on everything we have — verified by a test that fails the day that stops being true. The
strict default therefore costs nothing today, and the lenient policy is available the moment a
save contains a case that needs it.
The 232 `FLT_MAX` leaves (58 per save) are worth flagging: `FLT_MAX` is `0x7f7fffff`, a finite
normal value, **not** infinity. `events.md` corrected `formula-gaps.md` on exactly this point
for the default `EvPos`. A checksum that treated "very large" as "infinite" would merge
distinct states; `bits` cannot, and a test pins it.
### 3.4 Why there is no tolerant hashing policy
A tolerant hash is a contradiction, and it is worth writing down rather than rediscovering:
1. **Quantisation moves the cliff, it does not remove it.** Round to *k* bits and two values one
ULP apart still hash differently whenever they straddle a bucket boundary, while two values
2^k ULPs apart inside one bucket hash the same. You get both false positives and false
negatives, with the boundaries in arbitrary places.
2. **It destroys the roll-up.** The point of the tree is that a differing parent digest lets you
descend to the object. Under quantisation a parent can differ while every child is
"close enough", and you cannot tell from digests alone.
3. **It makes the root uninterpretable.** "Roots match" would mean "match to within a tolerance
nobody recorded".
So the digest is always exact and **tolerance lives in the differ**. `--ulps N` classifies each
leaf difference *after* it has been localised:
```
$ state_checksum.py A B --ulps 2
DIVERGED: 3 leaf difference(s)
/Sim/players/Player[16 "re"]/IdealSuit: 11.106206893920898 -> 11.106207847595215 [1 ulp] <= 2 ULP
...
floats: 3 differ, 3 within 2 ULP
```
The root stays strict; a human or a CI rule decides whether "three leaves, all ≤ 1 ULP" is an
acceptable port artefact. That decision is then visible in the log, which is the whole point.
This mirrors the existing harness vocabulary (`verify/harness/compare/TRACE_FORMAT.md`, per-hook
`ftol`, default 0), rather than inventing a second one.
Real output, from the turn 2 → turn 3 transition (§4.3):
```
/Sim/systems/Sys[112 "Gamma Cephei"]/RepCur: 336360.0 -> 336840.0 [15360 ulp]
/Sim/systems/Sys[112 "Gamma Cephei"]/RepMax: 336360.0 -> 336840.0 [15360 ulp]
/Sim/systems/Sys[288 "Ke'Dolarra"]/RepCur: 370000.0 -> 370520.0 [16640 ulp]
/Sim/systems/Sys[288 "Ke'Dolarra"]/RepMax: 370000.0 -> 370520.0 [16640 ulp]
floats: 4 differ, 0 within 2 ULP
```
That is the mode working as intended: four float leaves moved, and the ULP column says at a
glance that all four are genuine simulation changes (tens of thousands of ULPs — resource pools
growing over a turn), not float-path noise. Had a port produced `[1 ulp]` on these instead, the
same line would say so and the judgement call would be an explicit one.
### 3.5 The x64/SSE budget, and the one thing this cannot settle
x87 with PC=53 rounds an intermediate to double and then to float32 — **double rounding**. SSE
`mulss`/`addss` rounds once, directly to float32. For a minority of inputs those differ by one
ULP, and one ULP in a float32 that feeds an `fistp` can cross a tie and change an integer.
OpenRCT2 hit exactly this: "replays on x64 and x86 platforms will generate different sprite
checksums" (`guides/re-windows-2000s-howto.md` §1.1).
Under the strict default, a port that changes the float path **will** be reported as diverged.
That is deliberate: it is a real state difference. The port's job is either to reproduce the
double rounding (compute in double, narrow explicitly at each store — which is what
`fpu_cw = 0x127f` makes the original do) or to accept a documented `--ulps` budget on a named
list of fields.
**What I cannot settle from the host side:** whether the turn pipeline's results depend on the
x87 intermediate precision at all. Every save on this host was produced with `fpu_cw = 0x127f`,
so the corpus is one point, not a curve. It is possible that every value in the turn pipeline
is computed in a way that gives the same float32 under 24-bit, 53-bit and 64-bit precision
control, in which case an SSE port has **no** double-rounding budget to spend and the strict
policy is free forever. It is equally possible that a handful of fields are precision-sensitive.
**The experiment that would settle it** (VM140, lane R):
> Load `ref-turn2.sav`, press End Turn, and capture `(Autosave).sav` three times, with the shim
> forcing `fpu_cw` to `0x027f` (24-bit), `0x127f` (53-bit, the baseline) and `0x137f` (64-bit)
> across the turn call. Then run
> `state_checksum.py baseline.sav variant.sav` on each pair.
>
> * All three roots equal → no turn-pipeline value depends on x87 intermediate precision. The
> strict policy costs the SSE port nothing, and §3.5 can be closed.
> * Roots differ → the diff *is* the answer: it names every precision-sensitive field, and that
> list becomes the port's work item and the only place a `--ulps` budget is ever justified.
>
> Cheap, because the oracle is already byte-identical and the tool already localises. It needs
> nothing from this lane; it needs a shim knob that sets the control word around the turn call
> and the existing End-Turn click path from §5.
Until that runs, "the checksum is exact and the port must match bit-for-bit" is a *policy*, not
a measured requirement. It is the right default either way — it fails loudly rather than
quietly — but it should not be described as validated.
---
## 4. What was validated, on which saves
Regenerate with `verify/state-checksum/run_validation.sh`; outputs land in
`verify/results/state-checksum/`. Saves are read from `$SOTS_SAVES_DIR` plus the in-repo
`verify/results/saves/`, and the script skips cleanly when neither has anything. No `.sav` is
copied into either repo.
The corpus on this host is 10 files with **4 distinct contents** (the four the determinism work
produced): `a3f9dc4b` turn-1 pre-turn, `ab4ac2d7` turn-2 post-turn, `bb4fd9ac` turn-2
pre-turn/manual (the loaded-and-re-saved form of `ab4ac2d7`), `978041ac` turn-3 post-turn.
### 4.1 Identical saves produce identical checksums, and every save is covered
```
reader fingerprint: fe5a6f7cd4ae7910
10 file(s), 4 distinct content(s)
sha256:978041acd168b56e 2 file(s) STABLE + COVERED
root 5ac4a24197e82de49f3077cd8dd25fad Autosave - turn3.sav, turn3-state.sav
sha256:a3f9dc4b49fc669c 2 file(s) STABLE + COVERED
root 9bbcbd4945cd8319b65d7d7958772ee0 Autosave EndTurn - turn2.sav, turn1-state.sav
sha256:ab4ac2d7e2977260 3 file(s) STABLE + COVERED
root aa85fe76d412cdb3a0e7e52c8f0ca9e2 Autosave - turn2.sav, Autosave Backup - turn2.sav, turn2-state.sav
sha256:bb4fd9ac89f41e3b 3 file(s) STABLE + COVERED
root a1448e6c1867fc53708810b3a2f9ec77 Autosave EndTurn - turn3.sav, MyGameverify1verify1.sav, verify1.sav
VERDICT: all stable and fully covered
```
"COVERED" is the byte-for-byte reconstruction (§1.1), so this is a stronger statement than
sha256 equality: the *parse* is deterministic and total, not just the bytes.
### 4.2 The known re-save difference is localised, not reported as a whole-state mismatch
This is the deliverable that matters. `determinism-oracle.md` established that loading a
post-turn autosave and re-saving it changes exactly five things. The tree names all five and
nothing else:
```
$ state_checksum.py turn2-state.sav "Autosave EndTurn - turn3.sav"
A aa85fe76d412cdb3a0e7e52c8f0ca9e2 verify/results/saves/turn2-state.sav
B a1448e6c1867fc53708810b3a2f9ec77 $SOTS_SAVES_DIR/Autosave EndTurn - turn3.sav
policy: floats=bits mask=none reader=fe5a6f7cd4ae7910
DIVERGED: 5 leaf difference(s)
/Summary/Checksum: -1205790620 -> -1205790636
/Sim/players/Player[16 "re"]/Status: 4 -> 0
/Sim/players/Player[32 "Fane Lao"]/Status: 4 -> 0
/Sim/players/Player[496 "Singularity"]/Status: 4 -> 0
/Sim/players/Player[512 "Singularity"]/Status: 4 -> 0
$ state_checksum.py turn2-state.sav "Autosave EndTurn - turn3.sav" --mask resave
A a55e433687fff0e380de2caabf964a31
B a55e433687fff0e380de2caabf964a31
policy: floats=bits mask=resave reader=fe5a6f7cd4ae7910 [masked: Checksumx1, Statusx8]
IDENTICAL
```
Two things to note. The tree distinguishes the two `Singularity` players by id (496 and 512)
where the raw byte diff could only say "1st of two Singularity records". And the masked run
reports `Statusx8` — it replaced all eight `Player.Status` fields, of which four were already 0;
that number is printed so the mask's reach is visible rather than assumed.
### 4.3 A real turn transition is fully attributed
One real End Turn (`verify/results/state-checksum/turn2-to-turn3.txt`), 108 leaf differences,
every one carrying a path:
```
/Summary/Turn: 2 -> 3
/Sim/FleetIDs[]: removed [1744], added [34, 1776] (7 -> 8 entries)
/Sim/ShipIDs[]: removed [], added [1760] (16 -> 17 entries)
/Sim/RNG/.: '<raw 2503 B ef4d678696ed4c53>' -> '<raw 2503 B a80459bfd63a006b>'
/Sim/players/Player[16 "re"]/Sav: 289688 -> 532369
/Sim/players/Player[16 "re"]/Events/EvNxID: 2 -> 3
/Sim/players/Player[16 "re"]/Events/Events/.[EvTurn=3]: only-in-B
/Sim/players/Player[32 "Fane Lao"]/TechTree/TResDone[106]: 2879 -> 5768
/Sim/players/Player[32 "Fane Lao"]/Maint: 500 -> 1000
/Sim/players/Player[496 "Singularity"]/dipstats/.[1]/lastally: 2 -> 3
...
```
That reads as a turn report: economy, research, the new fleet and ship ids, the advanced RNG
state, and the new event bucket at `EvTurn=3` — which is the turn-bucketed layout `events.md`
established, walked correctly by the tree.
Of the 108 differences, 93 are scalar value changes, 13 are structural (12 nodes only in the
turn-3 save, 1 only in turn 2), and 2 are id lists. **Only 4 are floats**, and all four are far
outside any plausible tolerance:
```
/Sim/systems/Sys[112 "Gamma Cephei"]/RepCur: 336360.0 -> 336840.0 [15360 ulp]
/Sim/systems/Sys[288 "Ke'Dolarra"]/RepMax: 370000.0 -> 370520.0 [16640 ulp]
floats: 4 differ, 0 within 2 ULP
```
Worth knowing before budgeting float-parity work: on a two-player 28-system turn the float state
barely moves, and what moves, moves a long way. Nothing in this corpus sits near a rounding
boundary, so §3's question is about paths this corpus does not yet exercise.
### 4.4 Chain record and verify
```
recorded 3 turns -> chain-turn1-3.json
turn 1 9bbcbd4945cd8319 cov-ok turn1-state.sav
turn 2 aa85fe76d412cdb3 cov-ok turn2-state.sav
turn 3 5ac4a24197e82de4 cov-ok turn3-state.sav
$ state_checksum.py --chain chain-turn1-3.json turn1 turn2 turn3
turn 1 MATCH 9bbcbd4945cd8319 turn1-state.sav
turn 2 MATCH aa85fe76d412cdb3 turn2-state.sav
turn 3 MATCH 5ac4a24197e82de4 turn3-state.sav
```
and, substituting a wrong save at turn 2, the desync-log behaviour — stop at the first divergent
turn, name the subsystems:
```
turn 1 MATCH 9bbcbd4945cd8319 turn1-state.sav
turn 2 DIVERGE a1448e6c1867fc53 != aa85fe76d412cdb3 MyGameverify1verify1.sav
subsystem /Summary: 42b2094efe6e285a -> 8c7e33a33dc76b3d
subsystem /Sim/players: fa7f5ad40afed208 -> 3416ca2128671b1e
```
The saves in this chain are the ones the game actually wrote across two End Turns, so the chain
*mechanics* are validated on real turn data. What is not validated is generating a fresh chain
from the VM — see §5.
### 4.5 Tests
38 tests, `uv run python3 -m unittest discover -s verify/state-checksum -t verify/state-checksum`.
All pass. With only the in-repo saves, two real-save tests skip (the `bb4fd9ac` re-save form is
not in the repo); with `SOTS_SAVES_DIR` pointed at the full corpus, **38 pass, 0 skipped**.
Two of the tests earn their keep by having caught real defects during development: the
sibling-index cascade in §2.1, and a `string` value's length prefix missing from the
reconstruction (which made the coverage audit fail loudly at offset `0x1c` instead of silently
under-covering — the audit working exactly as intended, on its author).
### 4.6 A negative result on `Summary.Checksum`
`determinism-oracle.md` observed that the top-level `Checksum` moves by exactly −16 when four
`Player.Status` ints go 4 → 0, and concluded it is additive and derived. Two candidate
derivations were tried here and **both are ruled out**: it is not a byte sum over the inflated
stream, and it is not a sum over the int leaves. Both are consistent with the −16 on the re-save
pair (both change by −16 there), but neither leaves a constant residual across turns 1/2/3, so
neither is the function.
Most likely it is an additive sum over some traversal of the *in-memory* state — a desync check
of the same family as this tool — which would explain why it tracks the four `Status` ints and
not the file. Unresolved, and it does not need resolving: it is derived, so it is masked or
localised, never trusted as evidence. Recorded here so nobody re-runs the same two experiments.
---
## 5. The replay loop — designed, NOT run
VM140 is held by one lane at a time under the lab exclusivity rule (`campaign/board.md`; holder
was R-recapture, is M-movefleet as of 2026-09-08). Nothing in this section has been executed by
this lane. It is written to be handed to whoever holds the VM.
### 5.1 The loop
```
record: verify:
seed.sav ──┐ seed.sav ──┐
│ load │ load
▼ ▼
[game: End Turn] ──> (Autosave).sav [game: End Turn] ──> (Autosave).sav
│ │ │ │
│ ▼ │ ▼
│ state_checksum root_N │ state_checksum root_N'
│ │ │ │
└── feed back ─────┘ └── feed back ─────┘
│ │
▼ ▼
chain.json (turn, root, compare: first N where
per-subsystem digests) root_N' != root_N is the
divergent turn; diff the
two saves to name the object
```
Per turn, on the host:
1. Push the current save to `C:\SOTS\SavedGames\` (`scp` to `re@192.168.10.139`).
2. Drive the UI: Load Game → Single Player → OK → pick row → OK → Launch → wait for the
strategy map → **End Turn** → wait for the new turn → Quit to Main Menu.
3. Pull `(Autosave).sav` and `(Autosave EndTurn).sav` back.
4. `state_checksum.py` the post-turn autosave; append `{turn, root, subsystems}` to the chain.
5. The post-turn autosave becomes the next iteration's input.
Comparison against a recorded chain is `state_checksum.py --chain chain.json S1 S2 …`, already
implemented and validated on the three real saves (§4.4). It stops at the **first** divergent
turn — the OpenRCT2 desync-log discipline: only the first divergence is diagnostic, everything
after it is downstream noise.
### 5.2 The one canonicalisation the loop needs
Step 5 feeds a **loaded post-turn autosave** back in. That is precisely the case
`determinism-oracle.md` flagged: `Player.Status` 4 → 0 and the derived `Summary.Checksum` move
on the round trip. So:
* compare **post-turn autosave against post-turn autosave** with `--mask none` (they are
byte-identical run to run; no canonicalisation is needed and none should be applied);
* use `--mask resave` **only** when comparing across a load boundary — a re-implementation's
output against a loaded autosave, or a pre-turn save against a post-turn one of the same turn.
The chain records which mask it was built under and `verify_chain` refuses to compare across
policies, so this cannot be got wrong silently.
### 5.3 What it needs from lane R's recipe
Everything below already exists in `findings/subsystems/running-the-game.md` and
`findings/subsystems/determinism-oracle.md`; this is the list of what the loop consumes, so the
VM holder can say which parts are still true.
| need | where it is today | note |
|---|---|---|
| launch the game non-interactively | `schtasks /Run /TN SOTS` (task created `/IT /RL HIGHEST`, runs `C:\SOTS\launch.cmd`) | nominally ~30 s to the main menu, but the board records it taking **>60 s**; screenshot and verify before the first click or the path lands in Credits. 3× `qm sendkey 140 esc` skips the Bink intros |
| click driver | task `SOTSUI` running `recipe/click_helper.ps1`, reading `C:\SOTS\ui\cmd.txt` (`click X Y \| move \| key \| type \| sleep ms \| fg`) | QEMU `mouse_move`/`mouse_button` do **not** register (no USB tablet); this is the only working path |
| the End-Turn click path | `determinism-oracle.md`: Load Game (512,536) → Single Player (512,290) → OK (551,523) → row → OK (682,624) → Launch (511,663) → ~30 s → **End Turn (100,714)** → ~5 s → menu (1000,714) → Quit to Main Menu (938,699) → OK (537,377) | 1024×768 windowed at 0,0; `display.cfg` must pin `windowed 1 / 1024 / 768` |
| where saves live | `C:\SOTS\SavedGames\`; End Turn writes `(Autosave EndTurn).sav` (pre-turn), `(Autosave).sav` (post-turn), rotates `(Autosave Backup).sav` | nothing is written on Load or on Launch |
| a clean Load dialog | move pre-existing autosaves aside, as `determinism-oracle.md` did with `pre-existing\` | the dialog lists by filename; a stale row shifts the row click |
| file transport | `scp` over `re@192.168.10.139` | the earlier work also used a `Z:\saves` share |
| failure triage | `ssh spicy 'echo "screendump /tmp/x.ppm" \| qm monitor 140'` + `convert` | the loop should screenshot on any step that times out, since a mis-click looks like a divergence |
| shim state | `binkw32.dll` proxy with `shim.cfg hooks=trace` was loaded during the determinism runs and did not perturb the bytes | the chain must record the shim build id; a `hooks=replace` run is a *different* chain, not a continuation |
Two hazards worth stating before anyone runs it:
* **Text fields ignore Backspace and Esc** (`running-the-game.md`), which is why the existing
save names are concatenated. The loop should never need to type, but if it does, it cannot
correct a typo.
* **A mis-click is indistinguishable from a divergence** at the checksum layer. The loop must
assert the expected turn number from the parsed save (`Summary.Turn`) before recording a root,
and screenshot when it does not match. Without that, the harness can report a confident
DIVERGE that is really a missed button — which would be exactly the same class of error this
whole tool exists to prevent. The board's >60 s main-menu gotcha is this hazard already
happening once; a blind click landed in Credits. Every wait in the loop must be a
*wait-for-condition*, never a fixed sleep.
### 5.4 What the loop would buy
The three-turn chain in §4.4 is real but tiny. A 50-turn chain from a fixed seed would be the
project's first *end-to-end* regression: any change to the shim, to a replaced function, or to
the standalone engine either reproduces 50 roots or names the turn and the object where it
stopped. That is the OpenRCT2 replay test, with a stronger oracle than they had (byte-identical
saves rather than reconstructed command streams) and a finer diagnostic (a named object rather
than a sprite-checksum delta).
---
## 6. Costs and limits
* **~6 s per save** on this host, dominated by `save_reader.py` (37k items). `--no-audit` saves
roughly a fifth of that and gives up the coverage proof; do not use it in a gate.
* **The digest is only as good as the parse.** The reconstruction audit closes the gap between
"the reader read something" and "the reader read everything", but a reader that mis-*types* a
field still produces a self-consistent, total, deterministic digest. That is why §2.4 records
the reader fingerprint.
* **Opaque frames** (`TechTree` body, `spy2`, `civr`, `comms`, `Ojvs`, `Attrib`, `sprjs`,
`SvSctOb`, `trdmgr`, `spymgr`, `CD`) are covered byte-for-byte but not *named* internally, so a
divergence inside one localises to the frame, not to a field. Improving that is schema work in
`save_reader.py`, not checksum work.
* **The corpus is one game**: 2 real players, 28 systems, 3 turns. Every claim in §3 and §4 is
bounded by that. In particular §4.3's "zero float leaves differ across a turn" is a fact about
this game, not about the engine.

96
verify/state-checksum/float_census.py Normal file
View file

@ -0,0 +1,96 @@
#!/usr/bin/env python3
"""float_census.py -- classify every float leaf in a set of saves.
This is the evidence behind the float-parity policy in STATE_CHECKSUM.md: it
says whether the corpus actually contains the values where a `bits` policy and
a `canonical` policy disagree (signed zero, NaN payloads), and whether it
contains the values where an x87 -> SSE port is most likely to drift
(subnormals, values at the edge of float32 range).
uv run python3 float_census.py SAVE...
"""
from __future__ import annotations
import collections
import math
import os
import struct
import sys
_HERE = os.path.dirname(os.path.abspath(__file__))
if _HERE not in sys.path:
sys.path.insert(0, _HERE)
import state_checksum as sc # noqa: E402
FLT_MIN_NORMAL = 1.1754943508222875e-38
FLT_MAX = 3.4028234663852886e38
def classify(raw: bytes) -> str:
(bits,) = struct.unpack("<I", raw)
(v,) = struct.unpack("<f", raw)
if bits == 0x80000000:
return "negative zero"
if v == 0.0:
return "positive zero"
if math.isnan(v):
return "NaN"
if math.isinf(v):
return "infinity"
if bits == 0x7F7FFFFF:
return "FLT_MAX (0x7f7fffff)"
if bits == 0xFF7FFFFF:
return "-FLT_MAX"
if abs(v) < FLT_MIN_NORMAL:
return "subnormal"
if v == int(v) and abs(v) < 2 ** 24:
return "exact integer"
return "ordinary"
def main(argv=None) -> int:
argv = list(sys.argv[1:] if argv is None else argv)
if not argv:
print("usage: float_census.py SAVE...", file=sys.stderr)
return 2
seen: set = set()
total = collections.Counter()
print("# float census -- classes that separate the 'bits' and 'canonical'")
print("# policies are: negative zero, NaN. Classes an x87 -> SSE port is")
print("# most likely to move are: subnormal, and anything near FLT_MAX.")
print()
for p in argv:
with open(p, "rb") as f:
data = f.read()
key = hash(data)
if key in seen:
continue
seen.add(key)
ck = sc.checksum_bytes(data, path=p, audit=False)
c = collections.Counter()
examples: dict = {}
for n in ck.root.walk():
if n.kind != "float":
continue
k = classify(n.raw)
c[k] += 1
examples.setdefault(k, n.path)
total += c
print(f"{os.path.basename(p)}: {sum(c.values())} float leaves")
for k, v in sorted(c.items(), key=lambda kv: -kv[1]):
print(f" {v:>6} {k:<24} e.g. {examples[k]}")
print()
print("all distinct saves combined:")
for k, v in sorted(total.items(), key=lambda kv: -kv[1]):
print(f" {v:>6} {k}")
print()
risky = total["negative zero"] + total["NaN"]
print(f"'canonical' would change {risky} leaf/leaves across the corpus "
f"({'a no-op today' if risky == 0 else 'NOT a no-op'}).")
print(f"subnormals: {total['subnormal']} (each one is an x87/SSE parity risk)")
return 0
if __name__ == "__main__":
sys.exit(main())

114
verify/state-checksum/run_validation.sh Executable file
View file

@ -0,0 +1,114 @@
#!/usr/bin/env bash
# Regenerate verify/results/state-checksum/ from the saves on this host.
#
# Saves are read from $SOTS_SAVES_DIR when set, plus the in-repo
# verify/results/saves/. No .sav is copied anywhere. Skips cleanly with a
# message when there is nothing to read.
#
# verify/state-checksum/run_validation.sh
#
# Each gate is run separately and its exit status reported; nothing is chained
# with && so that a failure cannot skip a later step.
set -u
HERE="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
VERIFY="$(dirname "$HERE")"
OUT="$VERIFY/results/state-checksum"
SC="uv run python3 $HERE/state_checksum.py"
mkdir -p "$OUT"
REPO_SAVES="$VERIFY/results/saves"
EXTRA="${SOTS_SAVES_DIR:-}"
if [ -n "$EXTRA" ] && [ ! -d "$EXTRA" ]; then
echo "note: \$SOTS_SAVES_DIR=$EXTRA is not a directory; ignoring"
EXTRA=""
fi
if [ -z "$EXTRA" ]; then
echo "note: \$SOTS_SAVES_DIR unset; using in-repo saves only"
fi
shopt -s nullglob
ALL=("$REPO_SAVES"/*.sav)
[ -n "$EXTRA" ] && ALL+=("$EXTRA"/*.sav)
if [ ${#ALL[@]} -eq 0 ]; then
echo "no saves available; nothing to validate"
exit 0
fi
rc=0
note() { echo "== $1 -> exit $2"; [ "$2" -eq 0 ] || rc=1; }
# 1. one root + subsystem digest set per distinct save content
{
echo "# state_checksum roots -- $(date -u +%Y-%m-%dT%H:%M:%SZ)"
echo
seen=""
for f in "${ALL[@]}"; do
h=$(sha256sum "$f" | cut -c1-16)
case " $seen " in *" $h "*) continue;; esac
seen="$seen $h"
echo "--- sha256:$h $(basename "$f")"
$SC "$f"
echo
done
} > "$OUT/roots.txt" 2>&1
note "roots" $?
# 2. identical bytes must give identical roots, and every save must be covered
uv run python3 "$HERE/stability_check.py" "${ALL[@]}" > "$OUT/identical-roots.txt" 2>&1
note "identical-roots" $?
# 3. the known load->re-save delta must LOCALISE, not read as a whole-state miss
A="$REPO_SAVES/turn2-state.sav"
B=""
for f in "${ALL[@]}"; do
[ "$(sha256sum "$f" | cut -c1-8)" = "bb4fd9ac" ] && B="$f" && break
done
if [ -n "$B" ] && [ -f "$A" ]; then
{
echo "# determinism-oracle.md: loading a post-turn autosave and re-saving it"
echo "# changes Player.Status (4->0) on the four turn-participating players"
echo "# plus the derived Summary.Checksum. Nothing else."
echo
echo "\$ state_checksum.py turn2-state.sav $(basename "$B")"
$SC "$A" "$B"
echo
echo "\$ state_checksum.py turn2-state.sav $(basename "$B") --mask resave"
$SC "$A" "$B" --mask resave
} > "$OUT/resave-localisation.txt" 2>&1
note "resave-localisation" 0
else
echo "== resave-localisation -> SKIPPED (the bb4fd9ac re-save form is not on this host)"
fi
# 4. a real turn transition, fully attributed
if [ -f "$REPO_SAVES/turn2-state.sav" ] && [ -f "$REPO_SAVES/turn3-state.sav" ]; then
{
echo "# one real End Turn (turn 2 -> turn 3), every difference named"
echo
$SC "$REPO_SAVES/turn2-state.sav" "$REPO_SAVES/turn3-state.sav" --ulps 2 --limit 500
} > "$OUT/turn2-to-turn3.txt" 2>&1
note "turn-transition" 0
fi
# 5. the recorded chain (host side of the replay loop; the VM side is unrun)
CH=("$REPO_SAVES/turn1-state.sav" "$REPO_SAVES/turn2-state.sav" "$REPO_SAVES/turn3-state.sav")
have=1
for f in "${CH[@]}"; do [ -f "$f" ] || have=0; done
if [ "$have" = 1 ]; then
$SC "${CH[@]}" --record-chain "$OUT/chain-turn1-3.json" > "$OUT/chain.txt" 2>&1
note "record-chain" $?
echo >> "$OUT/chain.txt"
echo "\$ state_checksum.py --chain chain-turn1-3.json turn1 turn2 turn3" >> "$OUT/chain.txt"
$SC --chain "$OUT/chain-turn1-3.json" "${CH[@]}" >> "$OUT/chain.txt" 2>&1
note "verify-chain" $?
fi
# 6. float census -- the evidence behind the float-parity policy
uv run python3 "$HERE/float_census.py" "${ALL[@]}" > "$OUT/float-census.txt" 2>&1
note "float-census" $?
echo
echo "wrote $OUT"
exit $rc

60
verify/state-checksum/stability_check.py Normal file
View file

@ -0,0 +1,60 @@
#!/usr/bin/env python3
"""stability_check.py -- byte-identical saves must produce identical roots.
Groups the given saves by file sha256 and checks that every file in a group
gets the same root digest, and that every file's coverage audit passes. This
is the direct machine check of the determinism-oracle claim, one level up from
sha256: it also proves the *parse* is deterministic, not just the bytes.
uv run python3 stability_check.py SAVE...
"""
from __future__ import annotations
import hashlib
import os
import sys
_HERE = os.path.dirname(os.path.abspath(__file__))
if _HERE not in sys.path:
sys.path.insert(0, _HERE)
import state_checksum as sc # noqa: E402
def main(argv=None) -> int:
argv = list(sys.argv[1:] if argv is None else argv)
if not argv:
print("usage: stability_check.py SAVE...", file=sys.stderr)
return 2
groups: dict = {}
for p in argv:
with open(p, "rb") as f:
groups.setdefault(hashlib.sha256(f.read()).hexdigest()[:16], []).append(p)
print(f"reader fingerprint: {sc.READER_FINGERPRINT}")
print(f"{len(argv)} file(s), {len(groups)} distinct content(s)")
print()
bad = 0
for h, paths in sorted(groups.items()):
roots: dict = {}
cov_fail = []
for p in paths:
ck = sc.checksum_save(p)
roots.setdefault(ck.digest, []).append(os.path.basename(p))
if not ck.coverage["ok"]:
cov_fail.append((os.path.basename(p), ck.coverage["firstDiff"]))
ok = len(roots) == 1 and not cov_fail
bad += not ok
print(f"sha256:{h} {len(paths)} file(s) "
f"{'STABLE + COVERED' if ok else 'PROBLEM'}")
for r, names in roots.items():
print(f" root {r} {', '.join(sorted(names))}")
for name, off in cov_fail:
print(f" !! coverage failed for {name} at inflated offset {off}")
print()
print("VERDICT:", "all stable and fully covered" if not bad
else f"{bad} group(s) unstable or uncovered")
return 1 if bad else 0
if __name__ == "__main__":
sys.exit(main())

50
verify/state-checksum/state_checksum.py
View file

@ -71,6 +71,26 @@ __all__ = [
DIGEST_BYTES = 16 # blake2b-128; 2**-64 collision floor at our object counts DIGEST_BYTES = 16 # blake2b-128; 2**-64 collision floor at our object counts
SHORT = 16 # hex chars shown in text output SHORT = 16 # hex chars shown in text output
def _reader_fingerprint() -> str:
"""Identity of the save_reader build the digests were computed under.
The digest hashes each leaf's *inferred kind* alongside its bytes, so it is
a function of (save bytes, reader schema) -- not of the bytes alone. That
is fine for comparing two saves parsed by one reader, and dangerous for a
chain recorded months ago. So it is recorded and checked, never assumed.
It is deliberately NOT folded into the digest: a cosmetic reader edit
should not invalidate every recorded root, it should raise a warning.
"""
try:
with open(sr.__file__, "rb") as f:
return hashlib.blake2b(f.read(), digest_size=8).hexdigest()
except OSError: # pragma: no cover
return "unknown"
READER_FINGERPRINT = _reader_fingerprint()
BEGIN = struct.pack("<I", 0xBEEFBEEF) BEGIN = struct.pack("<I", 0xBEEFBEEF)
END = struct.pack("<I", 0x41104110) END = struct.pack("<I", 0x41104110)
@ -141,12 +161,13 @@ PAIR_GROUPS = {
"ply": ("hist", "history"), "ply": ("hist", "history"),
} }
#: frame tag -> child tags to use as a human label, first match wins #: frame tag -> child tags to use as a human label, first match wins. Tags are
#: as spelled on disk (SAVE_FORMAT.md section 10); `Ship` carries no name field,
#: so a ship is labelled by its id alone.
NAME_FIELDS = { NAME_FIELDS = {
"Player": ("PlryName",), "Player": ("PlryName",),
"Sys": ("Name",), "Sys": ("Name",),
"Flt": ("FltNm", "Name", "FName"), "Flt": ("FtName",),
"Ship": ("ShpNm", "Name", "SName"),
"Des": ("DName",), "Des": ("DName",),
} }
@ -509,7 +530,8 @@ class SaveChecksum:
"file": self.path, "file": self.path,
"root": self.digest, "root": self.digest,
"policy": {"floats": self.policy, "mask": self.mask, "policy": {"floats": self.policy, "mask": self.mask,
"digest": f"blake2b-{DIGEST_BYTES * 8}"}, "digest": f"blake2b-{DIGEST_BYTES * 8}",
"readerFingerprint": READER_FINGERPRINT},
"coverage": self.coverage, "coverage": self.coverage,
"readerIssues": {lvl: self.res.count(lvl) for lvl in ("error", "warn", "info")}, "readerIssues": {lvl: self.res.count(lvl) for lvl in ("error", "warn", "info")},
"maskHits": self.mask_hits, "maskHits": self.mask_hits,
@ -647,12 +669,24 @@ def build_chain(files: list[str], **kw) -> dict:
return {"format": "sots-state-chain/1", return {"format": "sots-state-chain/1",
"policy": {"floats": kw.get("floats", "bits"), "policy": {"floats": kw.get("floats", "bits"),
"mask": kw.get("mask", "none"), "mask": kw.get("mask", "none"),
"digest": f"blake2b-{DIGEST_BYTES * 8}"}, "digest": f"blake2b-{DIGEST_BYTES * 8}",
"readerFingerprint": READER_FINGERPRINT},
"turns": entries} "turns": entries}
def verify_chain(chain: dict, files: list[str], **kw) -> tuple[bool, list[str]]: def verify_chain(chain: dict, files: list[str], **kw) -> tuple[bool, list[str]]:
msgs, ok = [], True msgs, ok = [], True
pol = chain.get("policy") or {}
for field, got in (("floats", kw.get("floats", "bits")),
("mask", kw.get("mask", "none"))):
if pol.get(field) not in (None, got):
msgs.append(f"!! chain was recorded with {field}={pol[field]!r}, "
f"verifying with {got!r} -- roots are not comparable")
ok = False
fp = pol.get("readerFingerprint")
if fp and fp != READER_FINGERPRINT:
msgs.append(f"!! chain was recorded under save_reader {fp}, this is "
f"{READER_FINGERPRINT} -- re-record before trusting a DIVERGE")
rec = chain["turns"] rec = chain["turns"]
if len(rec) != len(files): if len(rec) != len(files):
msgs.append(f"chain has {len(rec)} turns, {len(files)} saves given") msgs.append(f"chain has {len(rec)} turns, {len(files)} saves given")
@ -756,7 +790,8 @@ def main(argv=None) -> int:
"coverage: FAILED at inflated offset 0x%x" % (cov.get("firstDiff") or 0)) "coverage: FAILED at inflated offset 0x%x" % (cov.get("firstDiff") or 0))
print(f"file: {ck.path}") print(f"file: {ck.path}")
print(f"root: {ck.digest}") print(f"root: {ck.digest}")
print(f"policy: floats={ck.policy} mask={ck.mask} digest=blake2b-{DIGEST_BYTES * 8}" print(f"policy: floats={ck.policy} mask={ck.mask} "
f"digest=blake2b-{DIGEST_BYTES * 8} reader={READER_FINGERPRINT}"
f"{_mask_note(ck)}") f"{_mask_note(ck)}")
print(f"{covs}; {ck.root.leaves} leaves, {ck.root.value_bytes} value bytes") print(f"{covs}; {ck.root.leaves} leaves, {ck.root.value_bytes} value bytes")
print(f"reader: {ck.res.count('error')} error, {ck.res.count('warn')} warn") print(f"reader: {ck.res.count('error')} error, {ck.res.count('warn')} warn")
@ -787,7 +822,8 @@ def main(argv=None) -> int:
return 0 if a.digest == b.digest else 1 return 0 if a.digest == b.digest else 1
print(f"A {a.digest} {a.path}") print(f"A {a.digest} {a.path}")
print(f"B {b.digest} {b.path}") print(f"B {b.digest} {b.path}")
print(f"policy: floats={a.policy} mask={a.mask}{_mask_note(a)}") print(f"policy: floats={a.policy} mask={a.mask} reader={READER_FINGERPRINT}"
f"{_mask_note(a)}")
for ck, nm in ((a, "A"), (b, "B")): for ck, nm in ((a, "A"), (b, "B")):
if ck.coverage.get("ok") is False: if ck.coverage.get("ok") is False:
print(f"!! {nm}: coverage FAILED at 0x{ck.coverage.get('firstDiff') or 0:x} " print(f"!! {nm}: coverage FAILED at 0x{ck.coverage.get('firstDiff') or 0:x} "

98
verify/state-checksum/test_state_checksum.py
View file

@ -31,8 +31,15 @@ import state_checksum as sc # noqa: E402
# --- helpers ------------------------------------------------------------------ # --- helpers ------------------------------------------------------------------
def tiny(status_a=4, status_b=4, checksum=-1000, extra_ids=(), fval=1.5) -> bytes: def tiny(status_a=4, status_b=4, checksum=-1000, extra_ids=(),
"""A miniature save with the shapes the tool special-cases.""" fval_a=1.5, fval_b=2.5) -> bytes:
"""A miniature save with the shapes the tool special-cases.
The `Sim` prefix fields (`KeyPath`..`NMnx`) are emitted because the reader
types `PlayerIDs` positionally off the Sim shape; without them the tag is
guessed and a 4-byte int is indistinguishable from a 2-byte string at the
same item size (SAVE_FORMAT.md section 2).
"""
w = sw.SaveWriter("joint") w = sw.SaveWriter("joint")
w.begin("Summary") w.begin("Summary")
w.string("GameName", "T") w.string("GameName", "T")
@ -40,17 +47,21 @@ def tiny(status_a=4, status_b=4, checksum=-1000, extra_ids=(), fval=1.5) -> byte
w.int("Checksum", checksum) w.int("Checksum", checksum)
w.end() w.end()
w.begin("Sim") w.begin("Sim")
w.string("KeyPath", "")
w.int("NMSz", 16)
w.int("NMLc", 0)
w.int("NMnx", 109)
ids = (16, 32) + tuple(extra_ids) ids = (16, 32) + tuple(extra_ids)
w.int("PlayerIDs", len(ids)) w.int("PlayerIDs", len(ids))
for i in ids: for i in ids:
w.int(".", i) w.int(".", i)
w.int("NumPlrs", 2) w.int("NumPlrs", 2)
for pid, st in ((16, status_a), (32, status_b)): for pid, st, fv in ((16, status_a, fval_a), (32, status_b, fval_b)):
w.int("PlayerID", pid) w.int("PlayerID", pid)
w.begin("Player") w.begin("Player")
w.string("PlryName", f"p{pid}") w.string("PlryName", f"p{pid}")
w.int("Status", st) w.int("Status", st)
w.float("IdealSuit", fval) w.float("IdealSuit", fv)
w.end() w.end()
w.end() w.end()
return w.bytes() return w.bytes()
@ -66,6 +77,16 @@ def find_saves() -> list[str]:
REAL = find_saves() REAL = find_saves()
needs_saves = unittest.skipUnless(REAL, "no saves in $SOTS_SAVES_DIR or verify/results/saves") needs_saves = unittest.skipUnless(REAL, "no saves in $SOTS_SAVES_DIR or verify/results/saves")
_CACHE: dict = {}
def real_ck(path: str, **kw):
"""Memoised checksum_save -- a real save costs ~6 s to parse."""
key = (path, tuple(sorted(kw.items())))
if key not in _CACHE:
_CACHE[key] = sc.checksum_save(path, **kw)
return _CACHE[key]
# --- coverage: the property that makes the digest evidence -------------------- # --- coverage: the property that makes the digest evidence --------------------
@ -115,7 +136,7 @@ class DigestTest(unittest.TestCase):
base = sc.checksum_bytes(tiny()) base = sc.checksum_bytes(tiny())
seen = 0 seen = 0
for name, kw in (("status", dict(status_a=5)), ("checksum", dict(checksum=-1001)), for name, kw in (("status", dict(status_a=5)), ("checksum", dict(checksum=-1001)),
("float", dict(fval=1.5000001))): ("float", dict(fval_a=1.5000001))):
with self.subTest(name): with self.subTest(name):
other = sc.checksum_bytes(tiny(**kw)) other = sc.checksum_bytes(tiny(**kw))
self.assertNotEqual(base.digest, other.digest) self.assertNotEqual(base.digest, other.digest)
@ -123,14 +144,36 @@ class DigestTest(unittest.TestCase):
self.assertEqual(seen, 3) self.assertEqual(seen, 3)
def test_a_one_bit_float_change_moves_the_root(self): def test_a_one_bit_float_change_moves_the_root(self):
a = sc.checksum_bytes(tiny(fval=1.5)) a = sc.checksum_bytes(tiny(fval_a=1.5))
(bits,) = struct.unpack("<I", struct.pack("<f", 1.5)) (bits,) = struct.unpack("<I", struct.pack("<f", 1.5))
(nudged,) = struct.unpack("<f", struct.pack("<I", bits + 1)) (nudged,) = struct.unpack("<f", struct.pack("<I", bits + 1))
b = sc.checksum_bytes(tiny(fval=nudged)) b = sc.checksum_bytes(tiny(fval_a=nudged))
self.assertNotEqual(a.digest, b.digest) self.assertNotEqual(a.digest, b.digest)
d = sc.diff(a.root, b.root) d = sc.diff(a.root, b.root)
self.assertEqual(len(d), 1, [repr(e) for e in d])
self.assertTrue(d[0].path.endswith("/IdealSuit"))
def test_a_float_leaf_diff_carries_its_ulp_distance(self):
"""Built from reader nodes directly: the fixture's positional type
inference would otherwise decide whether the leaf is a float at all."""
def leaf(v):
raw = struct.pack("<f", v)
n = sr.Node("F", "float", v, 0, 12, raw=raw)
return sc._build(n, "/F", "F", "bits", (), {})
(bits,) = struct.unpack("<I", struct.pack("<f", 1.5))
(nudged,) = struct.unpack("<f", struct.pack("<I", bits + 3))
d = sc.diff(leaf(1.5), leaf(nudged))
self.assertEqual(len(d), 1) self.assertEqual(len(d), 1)
self.assertEqual(d[0].ulps, 1.0) self.assertEqual(d[0].ulps, 3.0)
def test_the_digest_depends_on_the_inferred_kind_not_only_the_bytes(self):
"""Documented caveat: same 4 bytes, different reader typing, different
digest. Hence READER_FINGERPRINT is recorded with every chain."""
raw = struct.pack("<f", 1.5)
as_f = sc._build(sr.Node("F", "float", 1.5, 0, 12, raw=raw), "/F", "F", "bits", (), {})
as_i = sc._build(sr.Node("F", "int", 1069547520, 0, 12, raw=raw), "/F", "F", "bits", (), {})
self.assertNotEqual(as_f.digest, as_i.digest)
self.assertNotEqual(sc.READER_FINGERPRINT, "unknown")
def test_policy_is_domain_separated_into_the_root(self): def test_policy_is_domain_separated_into_the_root(self):
"""A strict root and a lenient root must never be confusable.""" """A strict root and a lenient root must never be confusable."""
@ -291,8 +334,23 @@ class ChainTest(unittest.TestCase):
chain = sc.build_chain(files, floats="canonical", mask="resave") chain = sc.build_chain(files, floats="canonical", mask="resave")
self.assertEqual(chain["policy"]["floats"], "canonical") self.assertEqual(chain["policy"]["floats"], "canonical")
self.assertEqual(chain["policy"]["mask"], "resave") self.assertEqual(chain["policy"]["mask"], "resave")
self.assertEqual(chain["policy"]["readerFingerprint"], sc.READER_FINGERPRINT)
json.dumps(chain) # must stay serialisable json.dumps(chain) # must stay serialisable
def test_verifying_under_a_different_policy_is_refused(self):
files = [self._write(tiny())]
chain = sc.build_chain(files, floats="bits")
ok, msgs = sc.verify_chain(chain, files, floats="canonical")
self.assertFalse(ok)
self.assertTrue(any("not comparable" in m for m in msgs), msgs)
def test_a_stale_reader_fingerprint_is_called_out(self):
files = [self._write(tiny())]
chain = sc.build_chain(files)
chain["policy"]["readerFingerprint"] = "0" * 16
_, msgs = sc.verify_chain(chain, files)
self.assertTrue(any("save_reader" in m for m in msgs), msgs)
# --- real saves --------------------------------------------------------------- # --- real saves ---------------------------------------------------------------
@ -301,7 +359,7 @@ class RealSaveTest(unittest.TestCase):
def test_coverage_is_proved_on_every_available_save(self): def test_coverage_is_proved_on_every_available_save(self):
for p in REAL: for p in REAL:
with self.subTest(os.path.basename(p)): with self.subTest(os.path.basename(p)):
ck = sc.checksum_save(p) ck = real_ck(p)
self.assertTrue(ck.coverage["ok"], self.assertTrue(ck.coverage["ok"],
f"reconstruction diverged at {ck.coverage['firstDiff']}") f"reconstruction diverged at {ck.coverage['firstDiff']}")
self.assertEqual(ck.coverage["rebuiltBytes"], ck.coverage["inflatedBytes"]) self.assertEqual(ck.coverage["rebuiltBytes"], ck.coverage["inflatedBytes"])
@ -315,17 +373,17 @@ class RealSaveTest(unittest.TestCase):
for data, paths in by_hash.items(): for data, paths in by_hash.items():
if len(paths) < 2: if len(paths) < 2:
continue continue
digs = {sc.checksum_save(p).digest for p in paths} digs = {real_ck(p).digest for p in paths}
self.assertEqual(len(digs), 1, paths) self.assertEqual(len(digs), 1, paths)
def test_repeated_runs_are_stable(self): def test_repeated_runs_are_stable(self):
p = REAL[0] p = REAL[0]
self.assertEqual(sc.checksum_save(p).digest, sc.checksum_save(p).digest) self.assertEqual(real_ck(p).digest, real_ck(p).digest)
def test_reader_is_clean_on_every_save(self): def test_reader_is_clean_on_every_save(self):
for p in REAL: for p in REAL:
with self.subTest(os.path.basename(p)): with self.subTest(os.path.basename(p)):
ck = sc.checksum_save(p, audit=False) ck = real_ck(p, audit=False)
self.assertEqual(ck.res.count("error"), 0) self.assertEqual(ck.res.count("error"), 0)
self.assertEqual(ck.res.count("warn"), 0) self.assertEqual(ck.res.count("warn"), 0)
@ -335,8 +393,8 @@ class RealSaveTest(unittest.TestCase):
here rather than silently.""" here rather than silently."""
for p in REAL: for p in REAL:
with self.subTest(os.path.basename(p)): with self.subTest(os.path.basename(p)):
a = sc.checksum_save(p, audit=False, floats="bits") a = real_ck(p, audit=False, floats="bits")
b = sc.checksum_save(p, audit=False, floats="canonical") b = real_ck(p, audit=False, floats="canonical")
self.assertEqual(sc.diff(a.root, b.root), []) self.assertEqual(sc.diff(a.root, b.root), [])
def test_known_resave_delta_localises_to_five_named_leaves(self): def test_known_resave_delta_localises_to_five_named_leaves(self):
@ -348,7 +406,7 @@ class RealSaveTest(unittest.TestCase):
for b in REAL: for b in REAL:
if a >= b: if a >= b:
continue continue
ca, cb = sc.checksum_save(a, audit=False), sc.checksum_save(b, audit=False) ca, cb = real_ck(a, audit=False), real_ck(b, audit=False)
d = sc.diff(ca.root, cb.root) d = sc.diff(ca.root, cb.root)
if d and all(e.kind == "value" for e in d) and \ if d and all(e.kind == "value" for e in d) and \
{e.path.rsplit("/", 1)[-1] for e in d} == {"Status", "Checksum"}: {e.path.rsplit("/", 1)[-1] for e in d} == {"Status", "Checksum"}:
@ -372,10 +430,10 @@ class RealSaveTest(unittest.TestCase):
for b in REAL: for b in REAL:
if a >= b: if a >= b:
continue continue
if sc.checksum_save(a, audit=False, mask="resave").digest == \ if real_ck(a, audit=False, mask="resave").digest == \
sc.checksum_save(b, audit=False, mask="resave").digest and \ real_ck(b, audit=False, mask="resave").digest and \
sc.checksum_save(a, audit=False).digest != \ real_ck(a, audit=False).digest != \
sc.checksum_save(b, audit=False).digest: real_ck(b, audit=False).digest:
found = True found = True
if not found: if not found:
self.skipTest("no re-save pair among the available saves") self.skipTest("no re-save pair among the available saves")
@ -384,7 +442,7 @@ class RealSaveTest(unittest.TestCase):
def test_a_real_turn_transition_localises_to_named_objects(self): def test_a_real_turn_transition_localises_to_named_objects(self):
by_turn = {} by_turn = {}
for p in REAL: for p in REAL:
ck = sc.checksum_save(p, audit=False) ck = real_ck(p, audit=False)
t = (ck.res.typed.get("summary") or {}).get("Turn") t = (ck.res.typed.get("summary") or {}).get("Turn")
by_turn.setdefault(t, ck) by_turn.setdefault(t, ck)
if not {2, 3} <= set(by_turn): if not {2, 3} <= set(by_turn):