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

Compare commits

base: alex:1b893e57c3faf5c5f7d6017bee5d1b3c4715a96b
Branches Tags
alex:main
...
compare: alex:9d385a7683a93451b8c42c140ea4bfd5374e3376
Branches Tags
alex:main

2 commits
1b893e57c3 ... 9d385a7683

Author SHA1 Message Date
alex
9d385a7683 board: lane C state-checksum landed; fpu_cw experiment queued; event-posting lane 2026-09-08 03:47:21 -04:00
alex
fdd0b72b7a state-checksum: whole-state diagnostic checksum harness (lane C) 
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.
 2026-09-08 03:46:34 -04:00
31 changed files with 3180 additions and 44 deletions
Show stats Expand all files Collapse all files

27
campaign/DASHBOARD.md
View file

@ -1,20 +1,20 @@
# SotS RE campaign — coverage dashboard # SotS RE campaign — coverage dashboard
Generated 2026-09-08 07:10 UTC · `sots-re` @ 6f81b04,2026-09-08 · `sots-engine` @ 45bdf7d,2026-09-08 (74 commits) · regenerate with `tools/dashboard.py` Generated 2026-09-08 07:47 UTC · `sots-re` @ fdd0b72,2026-09-08 · `sots-engine` @ 45bdf7d,2026-09-08 (74 commits) · regenerate with `tools/dashboard.py`
> **North star:** A functional reimplementation of the engine — behavior-equivalent, NOT byte-for-byte > **North star:** A functional reimplementation of the engine — behavior-equivalent, NOT byte-for-byte
## 1. Map coverage (campaign/board.md) ## 1. Map coverage (campaign/board.md)
72 targets · mapped-or-better **54/72** `[████████░░] 75%` · verified **35/72** `[█████░░░░░] 49%` 75 targets · mapped-or-better **55/75** `[███████░░░] 73%` · verified **36/75** `[█████░░░░░] 48%`
| Status | Count | % | | Status | Count | % |
|---|---:|---:| |---|---:|---:|
| verified | 35 | 49% | | verified | 36 | 48% |
| mapped | 19 | 26% | | mapped | 19 | 25% |
| in-progress | 3 | 4% | | in-progress | 3 | 4% |
| backlog | 14 | 19% | | backlog | 15 | 20% |
| blocked | 1 | 1% | | blocked | 2 | 3% |
| Type | verified | mapped | in-progress | backlog | blocked | total | | Type | verified | mapped | in-progress | backlog | blocked | total |
|---|---:|---:|---:|---:|---:|---:| |---|---:|---:|---:|---:|---:|---:|
@ -22,15 +22,16 @@ Generated 2026-09-08 07:10 UTC · `sots-re` @ 6f81b04,2026-09-08 · `sots-engine
| control-flow | 0 | 2 | 0 | 0 | 0 | 2 | | control-flow | 0 | 2 | 0 | 0 | 0 | 2 |
| subsystems | 2 | 7 | 1 | 3 | 1 | 14 | | subsystems | 2 | 7 | 1 | 3 | 1 | 14 |
| engine | 10 | 0 | 0 | 0 | 0 | 10 | | engine | 10 | 0 | 0 | 0 | 0 | 10 |
| verify | 7 | 2 | 1 | 8 | 0 | 18 | | verify | 8 | 2 | 0 | 9 | 0 | 19 |
| phase2 | 5 | 2 | 1 | 2 | 0 | 10 | | phase2 | 5 | 2 | 2 | 2 | 0 | 11 |
| meta | 6 | 4 | 0 | 1 | 0 | 11 | | meta | 6 | 4 | 0 | 1 | 0 | 11 |
| other | 0 | 0 | 0 | 0 | 1 | 1 |
## 2. Binary understanding ## 2. Binary understanding
- RTTI type descriptors: **1,924** (`Game::` 1,404, `Mars::` 194; serializable types 179) - RTTI type descriptors: **1,924** (`Game::` 1,404, `Mars::` 194; serializable types 179)
- Classes with recovered member layouts: **21** / 179 serializable types `[█░░░░░░░░░] 12%` — heuristic: distinct `Game::X`/`Mars::X` in `##`–`####` headings of `struct-recovery.md` + `schema-gaps-resolved.md` - Classes with recovered member layouts: **21** / 179 serializable types `[█░░░░░░░░░] 12%` — heuristic: distinct `Game::X`/`Mars::X` in `##`–`####` headings of `struct-recovery.md` + `schema-gaps-resolved.md`
- Functions: **41,411** (parsed from `01-fingerprint.md`); named/annotated in the **address contract** (`ghidra/addresses.json`, not Ghidra's full rename count): **380**, verified **373** `[██████████] 98%` - Functions: **41,411** (parsed from `01-fingerprint.md`); named/annotated in the **address contract** (`ghidra/addresses.json`, not Ghidra's full rename count): **386**, verified **379** `[██████████] 98%`
## 3. Data layer ## 3. Data layer
@ -95,10 +96,10 @@ Most recent open:
## 8. Delta since previous dashboard ## 8. Delta since previous dashboard
- verified targets: 33 → 35 (+2) · mapped-or-better: 51 → 54 (+3) - verified targets: 35 → 36 (+1) · mapped-or-better: 54 → 55 (+1)
- engine LOC: 29,095 → 29,095 (+0) · test files: 92 → 92 (+0) · checks: 2,942 → 2,942 (+0) - engine LOC: 29,095 → 29,095 (+0) · test files: 92 → 92 (+0) · checks: 2,942 → 2,942 (+0)
- addresses verified: 373 → 373 (+0) · recovered layouts: 21 → 21 (+0) · open questions: 27 → 27 (+0) - addresses verified: 373 → 379 (+6) · recovered layouts: 21 → 21 (+0) · open questions: 27 → 27 (+0)
--- ---
warnings: mars-rng.md: no oracle total row parsed; mars-stream.md: no oracle total row parsed; mars-vfs.md: no oracle total row parsed warnings: board.md: unknown types objects; mars-rng.md: no oracle total row parsed; mars-stream.md: no oracle total row parsed; mars-vfs.md: no oracle total row parsed
<!-- dashboard-metrics {"verified": 35, "mapped_plus": 54, "targets": 72, "loc": 29095, "tests": 92, "checks": 2942, "addr_verified": 373, "addr_total": 380, "layouts": 21, "open_q": 27} --> <!-- dashboard-metrics {"verified": 36, "mapped_plus": 55, "targets": 75, "loc": 29095, "tests": 92, "checks": 2942, "addr_verified": 379, "addr_total": 386, "layouts": 21, "open_q": 27} -->

5
campaign/board.md
View file

@ -74,6 +74,9 @@ 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 |
| fpu_cw sensitivity experiment | verify | backlog | — | 0% | 2026-09-08 | QUEUED FOR VM140 (lane M holds it). Lane C cannot tell whether any turn-pipeline value actually DEPENDS on x87 intermediate precision - every save on this host was made at fpu_cw=0x127f, so "the x64/SSE port must match bit-for-bit" is currently POLICY, not a measured requirement. Experiment: End Turn from ref-turn2.sav 3x with the shim forcing fpu_cw to 0x027f / 0x127f / 0x137f, then state_checksum the three autosaves. All equal => no double-rounding budget needed, closes STATE_CHECKSUM 3.5. Different => the diff IS the answer, naming every precision-sensitive field |
| Summary.Checksum algorithm | objects | blocked | — | 0% | 2026-09-08 | Lane C RULED OUT two candidates so nobody repeats them: NOT a byte sum over the inflated stream, NOT a sum over the int leaves. Each is consistent with the -16 re-save delta but leaves no constant residual across turns |
| event posting in ours | phase2 | in-progress | — | 0% | 2026-09-08 | Lane P: make ours actually post events so ProcessResearch's `side.events.after.v.next_id` 4->3 divergence closes. Converts harness-audit row 1 from known-defect to checked, and unbounds B2/B3 whose clean compares currently cover economy fields only |

152
findings/subsystems/movefleet-position-rounding.md Normal file
View file

@ -0,0 +1,152 @@
# `MoveFleet` position rounding — the precision sequence, read off the binary (lane M, 2026-09-08)
Lane R's guarded recapture found 8 of 45 live `StrategyServer::MoveFleet` calls diverging by
one ULP on a position component — the first arithmetic divergence the **behavioural** compare
caught on its own. This is the mechanism, read out of the instruction stream, and the live
before/after.
Ghidra work is written back: `Mars_Vec3_Normalize` @ `0x00422520`, `Mars_Vec3_Length` @
`0x004224b0`, `Mars_Vec3_LengthSquared` @ `0x004224f0` are named and prototyped with plate
comments, and two plate comments sit on the `MoveFleet` sites at `0x007da0f2` (the leg) and
`0x007da2ac` (the position update). Six new `ghidra/addresses.json` entries; header
regenerated with `tools/gen_addresses.py`.
## 1. `Mars_Vec3_Normalize` (`0x00422520`) — `float (Vec3* out, const Vec3* in)`, cdecl
123 callers. It normalises **and returns the length**, and it narrows to float32 **four**
separate times. Reading the FPU widths in order:
```
fld [in+4] fld [in] fld [in+8] ; y, x, z onto the x87 stack
fld st(1) fmulp st(2),st ; x*x
fld st(2) fmulp st(3),st ; y*y
fxch st(1) faddp st(2),st ; x*x + y*y
fmul st(0),st faddp st(1),st ; + z*z <- all still 53-bit
fstp DWORD PTR [ebp+0xc] ; (1) sumsq -> FLOAT32
fld DWORD PTR [ebp+0xc]
call 0x924f52 ; sqrt
fstp DWORD PTR [ebp+0xc] ; (2) len -> FLOAT32
fld DWORD PTR [ebp+0xc]
fld DWORD PTR ds:0x9e1ef8 ; eps = 0x34000000 = 2^-23
fcom ... test ah,0x41 ... jne <zero branch> ; !(len > eps) -> zero
fld st(0) fld1 fdivrp st(1),st ; 1.0 / len <- a RECIPROCAL
fstp DWORD PTR [ebp+0xc] ; (3) inv -> FLOAT32
fld [out] fld [ebp+0xc] fld st(0) fmulp st(2),st fxch st(1)
fstp DWORD PTR [out] ; (4) out.x -> FLOAT32
fld [out+4] fmul st,st(1) fstp DWORD PTR [out+4] ; out.y -> FLOAT32
fmul [out+8] fstp DWORD PTR [out+8] ; out.z -> FLOAT32
ret ; st0 = len (the float32 one)
```
so the contract is
```
sumsq = f32(x*x + y*y + z*z) products and adds in 53-bit, only the SUM stored
len = f32(sqrt(sumsq))
if (!(len > 2^-23)) { out = {0,0,0}; return; } <-- see the bug below
inv = f32(1.0 / len) a reciprocal, MULTIPLIED through, not three divides
out.c = f32(in.c * inv)
return len
```
**Original bug worth recording:** the zero branch at `0x004225a6` does `fldz`, three stores of
which the last one pops, and returns with an **empty x87 stack**. There is no return value, so
the caller's `fstp` for the distance underflows. Only reachable on a zero-length vector.
`Mars_Vec3_Length` (`0x004224b0`) is the same first half — `f32(sqrt(f32(sumsq)))` — and
`Mars_Vec3_LengthSquared` (`0x004224f0`) is `f32(sumsq)`. So **every** vector length in this
engine is float32-narrowed twice.
## 2. `MoveFleet`'s straight leg (`0x007da0f2`) and position update (`0x007da2ac`)
The leg:
```
edi = waypoint destination ; esi = fleet, ebx = &fleet.pos (fleet+0x18)
fld [edi+0x18] fsub [esi+0x18] fstp DWORD PTR [ebp+0x8] ; delta.x -> FLOAT32
fld [edi+0x4] fsub [ebx+0x4] fstp DWORD PTR [ebp-0x20] ; delta.y -> FLOAT32
fld [edi+0x8] fsub [ebx+0x8] fstp DWORD PTR [ebp-0x1c] ; delta.z -> FLOAT32
... copied into [ebp-0x38]/[ebp-0x34]/[ebp-0x30] ...
call 0x422520 ; Normalize(&v, &v), in place
fstp DWORD PTR [ebp-0x18] ; = the leg DISTANCE, never recomputed
```
so the delta a reimplementation normalises is `f32(dest.c - pos.c)`, **not** the exact
difference, and the distance and the direction come from the same single call.
The position update, on the `move != distance` branch:
```
fld [ebp-0x38] fmul st,st(1) fstp DWORD PTR [ebp+0x8] ; f32(dir.x * move)
fld [ebp-0x34] fmul st,st(1) fstp DWORD PTR [ebp-0x2c] ; f32(dir.y * move)
fmul [ebp-0x30] fstp DWORD PTR [ebp-0x30] ; f32(dir.z * move)
fld [ebp+0x8] fadd [ebx] fstp DWORD PTR [ebx] ; f32(pos.x + tmp)
fld [ebp-0x2c] fadd [ebx+4] fstp DWORD PTR [ebx+4]
fld [ebp-0x30] fadd [ebx+8] fstp DWORD PTR [ebx+8]
```
`move` is itself reloaded from a float32 slot (`[ebp-0x20]`). The sibling branch (`move ==
distance`, an **exact** float compare via `fucomp` + `test ah,0x44` + `jp`) copies the
destination's three words verbatim with `mov`, so an arrival never *steps* onto its
destination.
## 3. What `ours` was doing, and why the error looked the way it did
`sim::AdvanceAlongDirection` computed the exact double delta, a double sum of squares, a
double `sqrt`, and three double **divides**. Three of the five narrowings missing plus a
divide where the original multiplies by a rounded reciprocal. The position tail was already
right — which is precisely why the error was a *constant absolute* ~1.2e-7 rather than a
formula error: a direction wrong in its last float32 bit, scaled by a step of 2, is
2 x half-an-ULP-of-1 ~= 1.2e-7 wherever the fleet happens to be. The 64-ULP entry in lane R's
table is that same 1.2e-7 landing on a result near zero.
Which narrowing decides the answer is **not uniform** — worth knowing before anyone
"simplifies" it back:
| leg | exact delta + f32 len/inv/dir | f32 delta + f32 len, but a divide | all five |
|---|---|---|---|
| fleet 50, calls 42/79/116 | reproduces the **wrong** value | reproduces the original | reproduces the original |
| fleet 34, call 6 | reproduces the original | **neither** value | reproduces the original |
## 4. Offline confirmation before touching the game
Two of the run's fleets have a recoverable destination: an arrival copies the destination
verbatim, so `pos.after` on an arriving call **is** the waypoint destination. Fleet 34 arrives
on call 115 and fleet 50 on call 155, which gives exact float32 destinations for two fleets and
therefore eight fully determined legs (fleet 34 calls 6/41/78/115, fleet 50 calls 42/79/116/155)
— including all three of fleet 50's divergent calls and the 64-ULP one.
The five-narrowing model reproduces the **original** bit-for-bit on all eight, and the old
double model reproduces `ours` exactly on the three divergent ones. That settled the mechanism
before a single line was rebuilt.
## 5. Live before/after
Same VM, same save, same five End Turns, same `shim.cfg.recapmisc`, run twice by this lane:
| build | calls | compared | diverged | `tracecmp` exit |
|---|---|---|---|---|
| `recap-7584bad-20260908T0615Z` (control) | 45 | 45 | **8** | 1 |
| `mf-45bdf7d-dirty-20260908T0721Z` (fixed) | 45 | 45 | **0** | 0 |
The control run reproduced lane R's eight divergent `call_id`s exactly (42, 79, 80, 116, 118,
154, 156, 157), so this is a controlled before/after on one lane's own runs rather than a
comparison against someone else's report.
Artefacts: `verify/traces/mf-{before,after}-compare.jsonl`,
`verify/results/compare/mf-{before,after}.{json,md}`,
`verify/results/shim/mf-{before,after}-shim.log`.
## 6. Coverage — read this before quoting the zero
* **15 of the 45 calls move**; the other 30 are six waypointless fleets taking the early out.
* **All 15 moving calls are the same straight-run waypoint type.** Types 2 (node line),
3 (node route), 4 (gate teleport) and 5 (probabilistic jump) **never occurred**, so this
result says nothing about them and the generator never moved in this hook.
* The node-line step remains **knowingly wrong**: `NodeLineStep` / `BuildStutterSegments` are
written and unit-tested but not wired in; the hook steps every waypoint type as `speed x dt`.
* `sim::Distance` is deliberately left in double. It is now used only by the node-line /
stutter geometry, which on the evidence of `Mars_Vec3_Length` almost certainly needs the
same two narrowings — but with zero behavioural coverage on those paths there is nothing to
correct it against. Flagged at its declaration in the engine header.
* The two arrivals still compare clean and still mean nothing; no arrival machinery is declared.

52
ghidra/addresses.json
View file

@ -438,7 +438,7 @@
"name": "Script_ScanToken", "name": "Script_ScanToken",
"addr": "0x008cd1f0", "addr": "0x008cd1f0",
"convention": "custom", "convention": "custom",
"prototype": "/* EAX=cursor, ECX=&quotedFlag, EDX=out; stack: end, outEnd, &len \u2014 internal, do not hook */", "prototype": "/* EAX=cursor, ECX=&quotedFlag, EDX=out; stack: end, outEnd, &len — internal, do not hook */",
"status": "verified", "status": "verified",
"source": "handoff/loader-prototypes.md#m3" "source": "handoff/loader-prototypes.md#m3"
}, },
@ -678,7 +678,7 @@
"name": "gobio_Buffer_Create", "name": "gobio_Buffer_Create",
"addr": "0x008d4c90", "addr": "0x008d4c90",
"convention": "custom", "convention": "custom",
"prototype": "/* size in EBX, IBuffer** out on stack \u2014 internal, do not hook */", "prototype": "/* size in EBX, IBuffer** out on stack — internal, do not hook */",
"status": "verified", "status": "verified",
"source": "handoff/loader-prototypes.md#m4" "source": "handoff/loader-prototypes.md#m4"
}, },
@ -3041,6 +3041,54 @@
"prototype": "double 0.0 -- the research completion draw is NextFloat()*(1.0-this)+this, so it is a plain NextFloat()", "prototype": "double 0.0 -- the research completion draw is NextFloat()*(1.0-this)+this, so it is a plain NextFloat()",
"status": "verified", "status": "verified",
"source": "E own disassembly pass 2026-09-08 (ReVa read-memory + capstone x86-32): EventStorage::PostEvent 0x008862b0, GetOrCreateTurnBucket 0x00885380, FindDuplicate 0x00825d40, PruneOldTurns 0x00879eb0, PlayerEvent ctor 0x0084ee30 / Serialize 0x00825970; layout cross-checked against verify/results/saves/turn3-state.sav. findings/subsystems/events.md" "source": "E own disassembly pass 2026-09-08 (ReVa read-memory + capstone x86-32): EventStorage::PostEvent 0x008862b0, GetOrCreateTurnBucket 0x00885380, FindDuplicate 0x00825d40, PruneOldTurns 0x00879eb0, PlayerEvent ctor 0x0084ee30 / Serialize 0x00825970; layout cross-checked against verify/results/saves/turn3-state.sav. findings/subsystems/events.md"
},
{
"name": "Mars_Vec3_Normalize",
"addr": "0x00422520",
"convention": "cdecl",
"prototype": "float (Vec3* out, const Vec3* in) /* normalises in-place-capable (MoveFleet passes the same pointer twice) and RETURNS THE LENGTH. FOUR float32 narrowings in this order: sumsq = float32(x*x+y*y+z*z) (products/adds stay in the x87 53-bit registers, only the sum is stored to a dword and reloaded); len = float32(sqrt(sumsq)); inv = float32(1.0/len) -- a RECIPROCAL, stored to a dword and reloaded, then MULTIPLIED through, NOT three divides; out.c = float32(in.c * inv). Zero branch: !(len > 2^-23, the float at 0x009e1ef8) => out = {0,0,0} and it returns with an EMPTY x87 stack, i.e. no return value at all (original bug, only reachable on a zero-length vector). 123 callers. */",
"status": "verified",
"source": "lane M own disassembly pass 2026-09-08 (ReVa read-memory + objdump -b binary -m i386); confirmed bit-for-bit against 8 live MoveFleet legs"
},
{
"name": "Mars_Vec3_Length",
"addr": "0x004224b0",
"convention": "cdecl",
"prototype": "float (const Vec3* v) /* float32(sqrt(float32(x*x+y*y+z*z))) -- the same two narrowings as the first half of Mars_Vec3_Normalize */",
"status": "verified",
"source": "lane M own disassembly pass 2026-09-08"
},
{
"name": "Mars_Vec3_LengthSquared",
"addr": "0x004224f0",
"convention": "cdecl",
"prototype": "float (const Vec3* v) /* float32(x*x+y*y+z*z), one narrowing on the sum */",
"status": "verified",
"source": "lane M own disassembly pass 2026-09-08"
},
{
"name": "Mars_Vec3_NormaliseEpsilon",
"addr": "0x009e1ef8",
"convention": "data",
"prototype": "const float = 0x34000000 = 2^-23 = 1.1920928955078125e-07 /* Mars_Vec3_Normalize zeroes the direction when !(len > this) */",
"status": "verified",
"source": "lane M own disassembly pass 2026-09-08"
},
{
"name": "StrategyServer_MoveFleet_straight_leg",
"addr": "0x007da0f2",
"convention": "site",
"prototype": "site inside StrategyServer::MoveFleet /* the straight-run leg. Each delta dest.c - fleet.pos.c is computed on the x87 stack and STORED BACK TO A FLOAT32 SLOT before Mars_Vec3_Normalize(&v, &v) is called on it in place; that single call returns the leg DISTANCE and leaves the float32 unit direction in the same slots. The distance is never recomputed. */",
"status": "verified",
"source": "lane M own disassembly pass 2026-09-08"
},
{
"name": "StrategyServer_MoveFleet_position_update",
"addr": "0x007da2ac",
"convention": "site",
"prototype": "site inside StrategyServer::MoveFleet /* the move != distance branch: exactly two roundings per component, tmp.c = float32(dir.c * move) then pos.c = float32(pos.c + tmp.c). `move` is reloaded from a float32 slot. The sibling branch (move == distance, an EXACT float compare) copies the destination's three words verbatim with mov, so an arrival never steps onto its destination. */",
"status": "verified",
"source": "lane M own disassembly pass 2026-09-08"
} }
] ]
} }

14
ghidra/generated/sots_addresses.h
View file

@ -1,5 +1,5 @@
// GENERATED — do not edit. Facts about Sword of the Stars.exe (GOG 1.8.1). // GENERATED — do not edit. Facts about Sword of the Stars.exe (GOG 1.8.1).
// Source: sots-re ghidra/addresses.json @ e0c3e64, generated 2026-09-08 by tools/gen_addresses.py // Source: sots-re ghidra/addresses.json @ 1b893e5, generated 2026-09-08 by tools/gen_addresses.py
// Runtime address = (uintptr_t)GetModuleHandle(NULL) + RVA (the exe is ASLR-relocated). // Runtime address = (uintptr_t)GetModuleHandle(NULL) + RVA (the exe is ASLR-relocated).
#pragma once #pragma once
#include <cstdint> #include <cstdint>
@ -767,5 +767,17 @@ constexpr uint32_t g_ptr_EVENTMSG_ADDICTION_TEMPERENCE = 0x006f0a94;
constexpr uint32_t g_dbl_ResearchUnderbudgetThreshold = 0x005e20c8; constexpr uint32_t g_dbl_ResearchUnderbudgetThreshold = 0x005e20c8;
// data double 0.0 -- the research completion draw is NextFloat()*(1.0-this)+this, so it is a plain NextFloat() [verified] // data double 0.0 -- the research completion draw is NextFloat()*(1.0-this)+this, so it is a plain NextFloat() [verified]
constexpr uint32_t g_dbl_ResearchRollBias = 0x005e1e68; constexpr uint32_t g_dbl_ResearchRollBias = 0x005e1e68;
// cdecl float (Vec3* out, const Vec3* in) /* normalises in-place-capable (MoveFleet passes the same pointer twice) and RETURNS THE LENGTH. FOUR float32 narrowings in this order: sumsq = float32(x*x+y*y+z*z) (products/adds stay in the x87 53-bit registers, only the sum is stored to a dword and reloaded); len = float32(sqrt(sumsq)); inv = float32(1.0/len) -- a RECIPROCAL, stored to a dword and reloaded, then MULTIPLIED through, NOT three divides; out.c = float32(in.c * inv). Zero branch: !(len > 2^-23, the float at 0x009e1ef8) => out = {0,0,0} and it returns with an EMPTY x87 stack, i.e. no return value at all (original bug, only reachable on a zero-length vector). 123 callers. */ [verified]
constexpr uint32_t Mars_Vec3_Normalize = 0x00022520;
// cdecl float (const Vec3* v) /* float32(sqrt(float32(x*x+y*y+z*z))) -- the same two narrowings as the first half of Mars_Vec3_Normalize */ [verified]
constexpr uint32_t Mars_Vec3_Length = 0x000224b0;
// cdecl float (const Vec3* v) /* float32(x*x+y*y+z*z), one narrowing on the sum */ [verified]
constexpr uint32_t Mars_Vec3_LengthSquared = 0x000224f0;
// data const float = 0x34000000 = 2^-23 = 1.1920928955078125e-07 /* Mars_Vec3_Normalize zeroes the direction when !(len > this) */ [verified]
constexpr uint32_t Mars_Vec3_NormaliseEpsilon = 0x005e1ef8;
// site site inside StrategyServer::MoveFleet /* the straight-run leg. Each delta dest.c - fleet.pos.c is computed on the x87 stack and STORED BACK TO A FLOAT32 SLOT before Mars_Vec3_Normalize(&v, &v) is called on it in place; that single call returns the leg DISTANCE and leaves the float32 unit direction in the same slots. The distance is never recomputed. */ [verified]
constexpr uint32_t StrategyServer_MoveFleet_straight_leg = 0x003da0f2;
// site site inside StrategyServer::MoveFleet /* the move != distance branch: exactly two roundings per component, tmp.c = float32(dir.c * move) then pos.c = float32(pos.c + tmp.c). `move` is reloaded from a float32 slot. The sibling branch (move == distance, an EXACT float compare) copies the destination's three words verbatim with mov, so an arrival never steps onto its destination. */ [verified]
constexpr uint32_t StrategyServer_MoveFleet_position_update = 0x003da2ac;
} // namespace sots::addr } // namespace sots::addr

499
verify/results/compare/mf-after.json Normal file
View file

@ -0,0 +1,499 @@
{
"coverage_contradicted": [],
"coverage_unstated": [],
"format": 1,
"hooks": {
"Game::StrategyServer::MoveFleet": {
"calls": 45,
"compared": 45,
"coverage": {
"checked_regions": [
"pos",
"prev_pos",
"rng",
"ship[0].range",
"ship[1].range",
"ship[2].range",
"ship[3].range",
"ship[4].range",
"ship[5].range",
"ship[6].range",
"ship[7].range",
"ship[8].range",
"ship[9].range"
],
"guarded_calls": 45,
"guards": [
"fleet"
],
"spans": {
"compare": [
"fleet+0xa0:4",
"fleet+0xdc:1",
"fleet+0x10c:1",
"fleet+0xcc:1",
"fleet+0xdb:2",
"fleet+0xe0:26"
]
},
"state": "partial",
"undeclared_calls": 15,
"undeclared_writes": 42,
"unmodelled": [
{
"mitigation": "guard:fleet sees the fleet's own words; the event and the system do not",
"risk": "high",
"what": "on arrival: dispatches SEFleetArrived and runs one of three arrival handlers by destination kind (enter system / join fleet / stop at point)",
"why": "declared input boundary -- an arriving call is expected to differ in all of it, and none of it is declared, so the compare says nothing about arrivals"
},
{
"mitigation": "",
"risk": "high",
"what": "on departure: cancels every still-acting ship (with a log line each) and calls ServerSystem::FleetDeparts, which rewrites the system's ownership bits",
"why": "writes through pointers to ships and to the system"
},
{
"mitigation": "",
"risk": "medium",
"what": "the tanker top-up refuels other ships in the fleet",
"why": "the per-ship range regions would show it, but ours does not model it, so a fleet with a tanker diverges for a known reason"
},
{
"mitigation": "declared gap: docs/B4.md",
"risk": "medium",
"what": "a node-line waypoint's step comes from the stutter profile",
"why": "NodeLineStep / BuildStutterSegments are written and unit-tested but not wired in; the hook steps every waypoint type as speed x dt, so a node-line leg is knowingly mis-stepped and only its type is recorded"
},
{
"mitigation": "",
"risk": "medium",
"what": "a missed probabilistic jump scatters the fleet in a random direction",
"why": "the direction is a second draw whose mapping is not modelled; ours leaves the position alone and reports the scatter distance, so the generator region diverges by one word on a miss"
},
{
"mitigation": "",
"risk": "medium",
"what": "the route revalidation and the waypoint list itself",
"why": "declared input boundary; the waypoint vector is not a region"
}
],
"verdict": "partial",
"why": ""
},
"diffs": [],
"diverged": 0,
"diverged_call_ids": [],
"errors": 0,
"modes": {
"compare": 45
}
}
},
"inputs": [
"../../traces/mf-after-compare.jsonl"
],
"invalid": [],
"kind": "report",
"meta": [
{
"build": "mf-45bdf7d-dirty-20260908T0721Z",
"exe_sha256": "970b7de729956a53094c7eb98aba4270aee98e2fed5daf0d39e290013c90c841",
"format": 1,
"hooks": {
"Game::SectionDictionary::SectionDictionary": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "see docs/M2.md; compare mode for this hook is not safe to run",
"risk": "high",
"what": "LoadSection registers each section with the string table and the live TechTree, and may append to the dictionary's own vector",
"why": "M3 scope; ours delegates to the game's LoadSection after the original has already built all 885 definitions, so the second pass registers duplicates -- the leading hypothesis for this hook's compare-mode crash"
},
{
"mitigation": "",
"risk": "medium",
"what": "post-load validation pass over every definition's @-token against the string table",
"why": "runs after the loop and touches no declared region"
},
{
"mitigation": "",
"risk": "low",
"what": "allocates 885 SectionDef objects (0x3d8 bytes each) on the game heap",
"why": "they do not exist at hook entry; compared by index/species/id/token"
},
{
"mitigation": "guard:dict",
"risk": "low",
"what": "the word at dictionary+0x14",
"why": "not modelled; emitted as an ignored pointer"
},
{
"mitigation": "",
"risk": "medium",
"what": "the before-snapshot of the object is uninitialised heap",
"why": "the hook is on the constructor, so `before` is meaningless and only `after` carries information"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Game::ServerPlayer::ComputeBudget": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "declared input boundary; see budget_inputs.h",
"risk": "high",
"what": "slots 1, 2, 3, 4, 7 and 11 are produced by callees this milestone does not model (per-system output, trade, ship-carried population, a second manager, the build-queue spend)",
"why": "they are copied out of the original's own output and back into the same slots, so they match BY CONSTRUCTION and prove nothing"
},
{
"mitigation": "guard:budget_object does not reach the ships; unverified",
"risk": "high",
"what": "ServerSystem::ComputeOutput repairs damaged ships in orbit",
"why": "replace mode runs the original a second time on a scratch Budget to harvest the six unmodelled slots, so that repair happens TWICE per turn in replace mode and nothing in the trace would show it"
},
{
"mitigation": "",
"risk": "medium",
"what": "the difficulty-mods row from StrategyServer::GetDifficultyMods",
"why": "not reachable from a ServerPlayer, so the two relevant entries are fitted constants measured from the B1 trace rather than snapshotted inputs"
},
{
"mitigation": "",
"risk": "low",
"what": "the research-allocation vector's heap block",
"why": "only the element count is compared; the three words are heap pointers the default policy ignores"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Game::ServerPlayer::OnTechResearched": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "guard:player (EventStorage is inline at ServerPlayer+0x29c)",
"risk": "high",
"what": "posts EVENT_RESEARCH_COMPLETE / _UNDERBUDGET / _TEMPERANCE on the owner's EventStorage when !silent",
"why": "the same class of write as B3's defect, and this hook has no replace-mode oracle that could catch it: gotcha 4 in docs/B2.md says a changed save hash on a completion turn is expected and therefore not a finding"
},
{
"mitigation": "",
"risk": "high",
"what": "writes every owned system's AI flag (CCC_AIVrus / CCC_AISlv), re-evaluates the arcology civilian cap, cures addiction and clears plague across systems AND ships",
"why": "writes through pointers to other objects; compare mode must not touch live state, and no region reaches them"
},
{
"mitigation": "this is the extra draw B3 observed on a completion",
"risk": "high",
"what": "the pending plague-cure roll (ServerPlayer::RollResearchEvent)",
"why": "it draws exactly one word from the strategic generator unconditionally; running it in compare mode would consume real randomness. The two words it guards are still cleared and the record says whether it would have fired"
},
{
"mitigation": "",
"risk": "medium",
"what": "TechTree::SetResearched for the Zuul boarding-pod grant",
"why": "it would mutate the live tree, and it recurses"
},
{
"mitigation": "region:node_bore, declared only when the block already exists",
"risk": "medium",
"what": "allocates or frees the node-bore block at ServerPlayer+0x308",
"why": "ours has no allocator the game's runtime could free, so replace mode calls the game's own updater -- which means replace mode never exercises our node-bore selection at all"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Game::ServerSystem::ProcessTurn": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "guard:system",
"risk": "high",
"what": "the addiction sweep raises MoraleEvents, which are constructed and appended to the system's capped morale history",
"why": "the same class of write as B3's defect. sim::ProcessColonyTurn does compute the morale events (ColonyTurnResult), but the hook never emits them: DescribeMoraleEvents is dead code, so they are neither compared nor logged"
},
{
"mitigation": "guard:system covers the system object only, not the other objects",
"risk": "high",
"what": "every callee: the plague pass, imperial and civilian growth, the resource debit, in-orbit refuel, slaves, rebellion and the build queue",
"why": "declared input boundary -- ProcessTurn is a dispatcher and only the words it writes itself are modelled. The callees raise EVENT_SLAVES_DEAD, EVENT_SYSTEM_REBELLION_CONTINUES, the plague events and SEBuildCompleted, create ships and bump per-player ShipRecords counters"
},
{
"mitigation": "",
"risk": "medium",
"what": "ApplyInfraBonus / ApplyPopBonus read the owner's home-system id, and the build queue writes the owning ServerPlayer",
"why": "writes through a pointer to another object; no region reaches the player"
},
{
"mitigation": "",
"risk": "low",
"what": "ProcessRebellion is the pass's only RNG consumer and its draw count is data-dependent",
"why": "the generator IS a declared region, so a moved post-state is visible and names the system whose rebellion fired -- it is reported, not modelled"
},
{
"mitigation": "",
"risk": "medium",
"what": "replace mode is refused for this hook",
"why": "our side models the dispatcher's own writes and none of the callees, so a replace run would silently skip a colony's whole turn. There is therefore no oracle layer behind the compare for this hook"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Game::StrategyServer::MoveFleet": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "guard:fleet sees the fleet's own words; the event and the system do not",
"risk": "high",
"what": "on arrival: dispatches SEFleetArrived and runs one of three arrival handlers by destination kind (enter system / join fleet / stop at point)",
"why": "declared input boundary -- an arriving call is expected to differ in all of it, and none of it is declared, so the compare says nothing about arrivals"
},
{
"mitigation": "",
"risk": "high",
"what": "on departure: cancels every still-acting ship (with a log line each) and calls ServerSystem::FleetDeparts, which rewrites the system's ownership bits",
"why": "writes through pointers to ships and to the system"
},
{
"mitigation": "",
"risk": "medium",
"what": "the tanker top-up refuels other ships in the fleet",
"why": "the per-ship range regions would show it, but ours does not model it, so a fleet with a tanker diverges for a known reason"
},
{
"mitigation": "declared gap: docs/B4.md",
"risk": "medium",
"what": "a node-line waypoint's step comes from the stutter profile",
"why": "NodeLineStep / BuildStutterSegments are written and unit-tested but not wired in; the hook steps every waypoint type as speed x dt, so a node-line leg is knowingly mis-stepped and only its type is recorded"
},
{
"mitigation": "",
"risk": "medium",
"what": "a missed probabilistic jump scatters the fleet in a random direction",
"why": "the direction is a second draw whose mapping is not modelled; ours leaves the position alone and reports the scatter distance, so the generator region diverges by one word on a miss"
},
{
"mitigation": "",
"risk": "medium",
"what": "the route revalidation and the waypoint list itself",
"why": "declared input boundary; the waypoint vector is not a region"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Game::StrategyServer::ProcessFleetMovement": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "",
"risk": "high",
"what": "`ours` re-reads the LIVE fleet list after the original has run",
"why": "the gate-traffic total is computed by the original at the very end of the pass, so a pre-call snapshot would diverge for the wrong reason. It breaks the compare invariant that ours never touches live memory, and it makes this hook's verdict partly self-fulfilling: the input to our arithmetic is the original's own post-move state"
},
{
"mitigation": "",
"risk": "high",
"what": "drives MoveFleet up to five times per fleet",
"why": "every undeclared effect of MoveFleet happens inside this call too; the pass schedule is recorded in the arguments but never compared"
},
{
"mitigation": "",
"risk": "high",
"what": "writes FPdpos into every fleet and clears flags 0x2 and 0x100 on every fleet",
"why": "no region covers the fleets, only the players' gate-traffic words"
},
{
"mitigation": "",
"risk": "high",
"what": "OnFleetArrived posts EVENT_FLEET_ARRIVED",
"why": "the same class of write as B3's defect, and there is no replace mode for this hook, so nothing behind the compare could catch it either"
},
{
"mitigation": "",
"risk": "medium",
"what": "the original accumulates by player->index but writes back by the player's position in the server vector, into a fixed 32-int array with no bounds check",
"why": "a real latent bug in the original that our side reproduces only while index == position; the reference save never separates them"
},
{
"mitigation": "",
"risk": "medium",
"what": "PassSchedule() is never called by the hook, and FleetSummary::targetFleetId / relation are never filled",
"why": "the header claims ours predicts the call order for a trace to check; that prediction is not actually emitted"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Game::TechTree::ProcessResearch": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "region:events (EvNxID now diverges instead of passing silently)",
"risk": "high",
"what": "posts EVENT_RESEARCH_OVERBUDGET on the owner's EventStorage in the same branch that sets node.flag = 2",
"why": "the message text is composed from the tech name, so ours cannot synthesise it; it would have to be posted through the game's own event API. This is the defect that made a clean compare false: replace mode's autosave differed from the oracle by exactly this one event"
},
{
"mitigation": "region:events",
"risk": "medium",
"what": "posts EVENT_TECHS_UNLOCKED for nodes that became available this turn",
"why": "the trailing unlock loop makes no draw and writes no node, but it does build a names list and post an event"
},
{
"mitigation": "guard:player, guard:tree_header",
"risk": "high",
"what": "TechTree::SetResearched on completion: the turn/order stamps, the child unlock cascade, the recursive research of zero-cost children, and the owner's OnTechResearched callback",
"why": "its own milestone (B2); the callback writes live player state that compare mode must not touch, and it consumes one extra RNG word"
},
{
"mitigation": "guard:tree_header",
"risk": "medium",
"what": "bumps the tree's completion-order counter (TechTree+0x20)",
"why": "part of SetResearched; the per-node `order` word is compared but the counter it comes from was not a region"
},
{
"mitigation": "",
"risk": "low",
"what": "writes a completion line to the game log",
"why": "log text is not simulation state"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Game::WeaponDictionary::Init": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "suspected cause of the sibling section hook's compare crash (docs/M2.md)",
"risk": "high",
"what": "LoadWeapon -> WeaponDef::ParseScript registers each weapon's name with the string table and resolves `requires` against the live TechTree",
"why": "per-file parsing is M3 scope; ours delegates to the game's own LoadWeapon, so a compare run performs the registration a SECOND time and neither the string table nor the tech tree is a declared region"
},
{
"mitigation": "",
"risk": "low",
"what": "allocates 123 WeaponDef objects (0x278 bytes each) on the game heap",
"why": "the definitions do not exist when the hook is entered, so they cannot be a before-snapshot; the dictionary region compares them by id/name/path"
},
{
"mitigation": "guard:dict",
"risk": "low",
"what": "the word at dictionary+0x14",
"why": "not modelled; emitted as an opaque pointer, which the default policy ignores -- a change is visible in a trace but never a divergence"
},
{
"mitigation": "",
"risk": "low",
"what": "writes lines to the game log for a missing manifest",
"why": "log text is not simulation state"
},
{
"mitigation": "",
"risk": "low",
"what": "std::sort tie order for equal weapon names",
"why": "msvc_sort.h replays MSVC 2010's introsort, but the shipped data has no tied names, so the tie rule is unexercised rather than verified"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Mars::GlobalConsts::LoadFile": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "LoadAll's post-state would have to be hooked to see it",
"risk": "medium",
"what": "erases each consumed key from the caller's std::map",
"why": "the map is a LoadAll temporary; declaring a red-black tree as a region is not possible before the call. First-occurrence-wins is reproduced in game::config::apply instead, so the *effect* is modelled, the container is not"
},
{
"mitigation": "",
"risk": "low",
"what": "writes three kinds of line to the game log (unrecognised key, applied key, expected-but-not-found)",
"why": "log text is not part of the simulation state"
},
{
"mitigation": "",
"risk": "low",
"what": "opens the file through the VFS and allocates/releases a refcounted buffer",
"why": "ours performs the same two calls, so allocation behaviour matches by construction rather than by comparison"
},
{
"mitigation": "",
"risk": "low",
"what": "String slots assign through the engine's own std::string, leaking one heap block per long string in compare mode",
"why": "start-up only; documented in docs/M1.md"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Shim::SelfTest::Fill": {
"coverage": {
"state": "complete",
"unmodelled": [],
"why": "Fill writes buf[0..n) and nothing else; the whole range is a declared region"
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
}
},
"inline_max": 256,
"started": "2026-09-08T07:31:45Z"
}
],
"totals": {
"calls": 45,
"compared": 45,
"coverage_contradicted": 0,
"coverage_unstated": 0,
"diverged": 0,
"guarded_calls": 45,
"invalid_records": 0,
"undeclared_calls": 15,
"undeclared_writes": 42
},
"warnings": []
}

24
verify/results/compare/mf-after.md Normal file
View file

@ -0,0 +1,24 @@
## tracecmp report: mf-after-compare.jsonl
- build: mf-45bdf7d-dirty-20260908T0721Z started: 2026-09-08T07:31:45Z inline_max: 256
- calls: 45 compared: 45 diverged: 0 invalid records: 0 warnings: 0
- coverage: 45 guarded call(s), 42 undeclared write(s) in 15 call(s); 0 hook(s) unstated, 0 contradicted
| hook | calls | modes | compared | diverged | errors |
|---|---|---|---|---|---|
| Game::StrategyServer::MoveFleet | 45 | compare:45 | 45 | 0 | 0 |
### coverage
| hook | verdict | compared regions | guards | undeclared writes | unmodelled |
|---|---|---|---|---|---|
| Game::StrategyServer::MoveFleet | partial | pos, prev_pos, rng, ship[0].range, ship[1].range, ship[2].range, +7 | fleet | 42 in 15 call(s) | 6 |
#### Game::StrategyServer::MoveFleet — not checked by this run
- (high) on arrival: dispatches SEFleetArrived and runs one of three arrival handlers by destination kind (enter system / join fleet / stop at point) — declared input boundary -- an arriving call is expected to differ in all of it, and none of it is declared, so the compare says nothing about arrivals [guard:fleet sees the fleet's own words; the event and the system do not]
- (high) on departure: cancels every still-acting ship (with a log line each) and calls ServerSystem::FleetDeparts, which rewrites the system's ownership bits — writes through pointers to ships and to the system
- (medium) the tanker top-up refuels other ships in the fleet — the per-ship range regions would show it, but ours does not model it, so a fleet with a tanker diverges for a known reason
- (medium) a node-line waypoint's step comes from the stutter profile — NodeLineStep / BuildStutterSegments are written and unit-tested but not wired in; the hook steps every waypoint type as speed x dt, so a node-line leg is knowingly mis-stepped and only its type is recorded [declared gap: docs/B4.md]
- (medium) a missed probabilistic jump scatters the fleet in a random direction — the direction is a second draw whose mapping is not modelled; ours leaves the position alone and reports the scatter distance, so the generator region diverges by one word on a miss
- (medium) the route revalidation and the waypoint list itself — declared input boundary; the waypoint vector is not a region
- guard hits in compare mode: fleet+0xa0:4, fleet+0xdc:1, fleet+0x10c:1, fleet+0xcc:1, fleet+0xdb:2, fleet+0xe0:26

604
verify/results/compare/mf-before.json Normal file
View file

@ -0,0 +1,604 @@
{
"coverage_contradicted": [],
"coverage_unstated": [],
"format": 1,
"hooks": {
"Game::StrategyServer::MoveFleet": {
"calls": 45,
"compared": 45,
"coverage": {
"checked_regions": [
"pos",
"prev_pos",
"rng",
"ship[0].range",
"ship[1].range",
"ship[2].range",
"ship[3].range",
"ship[4].range",
"ship[5].range",
"ship[6].range",
"ship[7].range",
"ship[8].range",
"ship[9].range"
],
"guarded_calls": 45,
"guards": [
"fleet"
],
"spans": {
"compare": [
"fleet+0xa0:4",
"fleet+0xdc:1",
"fleet+0x10c:1",
"fleet+0xcc:1",
"fleet+0xdb:2",
"fleet+0xe0:26"
]
},
"state": "partial",
"undeclared_calls": 15,
"undeclared_writes": 42,
"unmodelled": [
{
"mitigation": "guard:fleet sees the fleet's own words; the event and the system do not",
"risk": "high",
"what": "on arrival: dispatches SEFleetArrived and runs one of three arrival handlers by destination kind (enter system / join fleet / stop at point)",
"why": "declared input boundary -- an arriving call is expected to differ in all of it, and none of it is declared, so the compare says nothing about arrivals"
},
{
"mitigation": "",
"risk": "high",
"what": "on departure: cancels every still-acting ship (with a log line each) and calls ServerSystem::FleetDeparts, which rewrites the system's ownership bits",
"why": "writes through pointers to ships and to the system"
},
{
"mitigation": "",
"risk": "medium",
"what": "the tanker top-up refuels other ships in the fleet",
"why": "the per-ship range regions would show it, but ours does not model it, so a fleet with a tanker diverges for a known reason"
},
{
"mitigation": "declared gap: docs/B4.md",
"risk": "medium",
"what": "a node-line waypoint's step comes from the stutter profile",
"why": "NodeLineStep / BuildStutterSegments are written and unit-tested but not wired in; the hook steps every waypoint type as speed x dt, so a node-line leg is knowingly mis-stepped and only its type is recorded"
},
{
"mitigation": "",
"risk": "medium",
"what": "a missed probabilistic jump scatters the fleet in a random direction",
"why": "the direction is a second draw whose mapping is not modelled; ours leaves the position alone and reports the scatter distance, so the generator region diverges by one word on a miss"
},
{
"mitigation": "",
"risk": "medium",
"what": "the route revalidation and the waypoint list itself",
"why": "declared input boundary; the waypoint vector is not a region"
}
],
"verdict": "partial",
"why": ""
},
"diffs": [
{
"call_id": 42,
"diff": [
{
"orig": {
"t": "f32",
"v": 3.1515913
},
"ours": {
"t": "f32",
"v": 3.15159106
},
"path": "side.pos.after.v.y",
"why": "exact"
}
],
"file": "mf-before-compare.jsonl",
"line": 44
},
{
"call_id": 79,
"diff": [
{
"orig": {
"t": "f32",
"v": 1.58417809
},
"ours": {
"t": "f32",
"v": 1.58417821
},
"path": "side.pos.after.v.y",
"why": "exact"
}
],
"file": "mf-before-compare.jsonl",
"line": 81
},
{
"call_id": 80,
"diff": [
{
"orig": {
"t": "f32",
"v": 4.21149492
},
"ours": {
"t": "f32",
"v": 4.21149445
},
"path": "side.pos.after.v.y",
"why": "exact"
}
],
"file": "mf-before-compare.jsonl",
"line": 82
},
{
"call_id": 116,
"diff": [
{
"orig": {
"t": "f32",
"v": 0.0167649984
},
"ours": {
"t": "f32",
"v": 0.0167651176
},
"path": "side.pos.after.v.y",
"why": "exact"
}
],
"file": "mf-before-compare.jsonl",
"line": 118
},
{
"call_id": 118,
"diff": [
{
"orig": {
"t": "f32",
"v": 3.14307928
},
"ours": {
"t": "f32",
"v": 3.14307904
},
"path": "side.pos.after.v.y",
"why": "exact"
}
],
"file": "mf-before-compare.jsonl",
"line": 120
}
],
"diverged": 8,
"diverged_call_ids": [
42,
79,
80,
116,
118,
154,
156,
157
],
"errors": 0,
"modes": {
"compare": 45
}
}
},
"inputs": [
"../../traces/mf-before-compare.jsonl"
],
"invalid": [],
"kind": "report",
"meta": [
{
"build": "recap-7584bad-20260908T0615Z",
"exe_sha256": "970b7de729956a53094c7eb98aba4270aee98e2fed5daf0d39e290013c90c841",
"format": 1,
"hooks": {
"Game::SectionDictionary::SectionDictionary": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "see docs/M2.md; compare mode for this hook is not safe to run",
"risk": "high",
"what": "LoadSection registers each section with the string table and the live TechTree, and may append to the dictionary's own vector",
"why": "M3 scope; ours delegates to the game's LoadSection after the original has already built all 885 definitions, so the second pass registers duplicates -- the leading hypothesis for this hook's compare-mode crash"
},
{
"mitigation": "",
"risk": "medium",
"what": "post-load validation pass over every definition's @-token against the string table",
"why": "runs after the loop and touches no declared region"
},
{
"mitigation": "",
"risk": "low",
"what": "allocates 885 SectionDef objects (0x3d8 bytes each) on the game heap",
"why": "they do not exist at hook entry; compared by index/species/id/token"
},
{
"mitigation": "guard:dict",
"risk": "low",
"what": "the word at dictionary+0x14",
"why": "not modelled; emitted as an ignored pointer"
},
{
"mitigation": "",
"risk": "medium",
"what": "the before-snapshot of the object is uninitialised heap",
"why": "the hook is on the constructor, so `before` is meaningless and only `after` carries information"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Game::ServerPlayer::ComputeBudget": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "declared input boundary; see budget_inputs.h",
"risk": "high",
"what": "slots 1, 2, 3, 4, 7 and 11 are produced by callees this milestone does not model (per-system output, trade, ship-carried population, a second manager, the build-queue spend)",
"why": "they are copied out of the original's own output and back into the same slots, so they match BY CONSTRUCTION and prove nothing"
},
{
"mitigation": "guard:budget_object does not reach the ships; unverified",
"risk": "high",
"what": "ServerSystem::ComputeOutput repairs damaged ships in orbit",
"why": "replace mode runs the original a second time on a scratch Budget to harvest the six unmodelled slots, so that repair happens TWICE per turn in replace mode and nothing in the trace would show it"
},
{
"mitigation": "",
"risk": "medium",
"what": "the difficulty-mods row from StrategyServer::GetDifficultyMods",
"why": "not reachable from a ServerPlayer, so the two relevant entries are fitted constants measured from the B1 trace rather than snapshotted inputs"
},
{
"mitigation": "",
"risk": "low",
"what": "the research-allocation vector's heap block",
"why": "only the element count is compared; the three words are heap pointers the default policy ignores"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Game::ServerPlayer::OnTechResearched": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "guard:player (EventStorage is inline at ServerPlayer+0x29c)",
"risk": "high",
"what": "posts EVENT_RESEARCH_COMPLETE / _UNDERBUDGET / _TEMPERANCE on the owner's EventStorage when !silent",
"why": "the same class of write as B3's defect, and this hook has no replace-mode oracle that could catch it: gotcha 4 in docs/B2.md says a changed save hash on a completion turn is expected and therefore not a finding"
},
{
"mitigation": "",
"risk": "high",
"what": "writes every owned system's AI flag (CCC_AIVrus / CCC_AISlv), re-evaluates the arcology civilian cap, cures addiction and clears plague across systems AND ships",
"why": "writes through pointers to other objects; compare mode must not touch live state, and no region reaches them"
},
{
"mitigation": "this is the extra draw B3 observed on a completion",
"risk": "high",
"what": "the pending plague-cure roll (ServerPlayer::RollResearchEvent)",
"why": "it draws exactly one word from the strategic generator unconditionally; running it in compare mode would consume real randomness. The two words it guards are still cleared and the record says whether it would have fired"
},
{
"mitigation": "",
"risk": "medium",
"what": "TechTree::SetResearched for the Zuul boarding-pod grant",
"why": "it would mutate the live tree, and it recurses"
},
{
"mitigation": "region:node_bore, declared only when the block already exists",
"risk": "medium",
"what": "allocates or frees the node-bore block at ServerPlayer+0x308",
"why": "ours has no allocator the game's runtime could free, so replace mode calls the game's own updater -- which means replace mode never exercises our node-bore selection at all"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Game::ServerSystem::ProcessTurn": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "guard:system",
"risk": "high",
"what": "the addiction sweep raises MoraleEvents, which are constructed and appended to the system's capped morale history",
"why": "the same class of write as B3's defect. sim::ProcessColonyTurn does compute the morale events (ColonyTurnResult), but the hook never emits them: DescribeMoraleEvents is dead code, so they are neither compared nor logged"
},
{
"mitigation": "guard:system covers the system object only, not the other objects",
"risk": "high",
"what": "every callee: the plague pass, imperial and civilian growth, the resource debit, in-orbit refuel, slaves, rebellion and the build queue",
"why": "declared input boundary -- ProcessTurn is a dispatcher and only the words it writes itself are modelled. The callees raise EVENT_SLAVES_DEAD, EVENT_SYSTEM_REBELLION_CONTINUES, the plague events and SEBuildCompleted, create ships and bump per-player ShipRecords counters"
},
{
"mitigation": "",
"risk": "medium",
"what": "ApplyInfraBonus / ApplyPopBonus read the owner's home-system id, and the build queue writes the owning ServerPlayer",
"why": "writes through a pointer to another object; no region reaches the player"
},
{
"mitigation": "",
"risk": "low",
"what": "ProcessRebellion is the pass's only RNG consumer and its draw count is data-dependent",
"why": "the generator IS a declared region, so a moved post-state is visible and names the system whose rebellion fired -- it is reported, not modelled"
},
{
"mitigation": "",
"risk": "medium",
"what": "replace mode is refused for this hook",
"why": "our side models the dispatcher's own writes and none of the callees, so a replace run would silently skip a colony's whole turn. There is therefore no oracle layer behind the compare for this hook"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Game::StrategyServer::MoveFleet": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "guard:fleet sees the fleet's own words; the event and the system do not",
"risk": "high",
"what": "on arrival: dispatches SEFleetArrived and runs one of three arrival handlers by destination kind (enter system / join fleet / stop at point)",
"why": "declared input boundary -- an arriving call is expected to differ in all of it, and none of it is declared, so the compare says nothing about arrivals"
},
{
"mitigation": "",
"risk": "high",
"what": "on departure: cancels every still-acting ship (with a log line each) and calls ServerSystem::FleetDeparts, which rewrites the system's ownership bits",
"why": "writes through pointers to ships and to the system"
},
{
"mitigation": "",
"risk": "medium",
"what": "the tanker top-up refuels other ships in the fleet",
"why": "the per-ship range regions would show it, but ours does not model it, so a fleet with a tanker diverges for a known reason"
},
{
"mitigation": "declared gap: docs/B4.md",
"risk": "medium",
"what": "a node-line waypoint's step comes from the stutter profile",
"why": "NodeLineStep / BuildStutterSegments are written and unit-tested but not wired in; the hook steps every waypoint type as speed x dt, so a node-line leg is knowingly mis-stepped and only its type is recorded"
},
{
"mitigation": "",
"risk": "medium",
"what": "a missed probabilistic jump scatters the fleet in a random direction",
"why": "the direction is a second draw whose mapping is not modelled; ours leaves the position alone and reports the scatter distance, so the generator region diverges by one word on a miss"
},
{
"mitigation": "",
"risk": "medium",
"what": "the route revalidation and the waypoint list itself",
"why": "declared input boundary; the waypoint vector is not a region"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Game::StrategyServer::ProcessFleetMovement": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "",
"risk": "high",
"what": "`ours` re-reads the LIVE fleet list after the original has run",
"why": "the gate-traffic total is computed by the original at the very end of the pass, so a pre-call snapshot would diverge for the wrong reason. It breaks the compare invariant that ours never touches live memory, and it makes this hook's verdict partly self-fulfilling: the input to our arithmetic is the original's own post-move state"
},
{
"mitigation": "",
"risk": "high",
"what": "drives MoveFleet up to five times per fleet",
"why": "every undeclared effect of MoveFleet happens inside this call too; the pass schedule is recorded in the arguments but never compared"
},
{
"mitigation": "",
"risk": "high",
"what": "writes FPdpos into every fleet and clears flags 0x2 and 0x100 on every fleet",
"why": "no region covers the fleets, only the players' gate-traffic words"
},
{
"mitigation": "",
"risk": "high",
"what": "OnFleetArrived posts EVENT_FLEET_ARRIVED",
"why": "the same class of write as B3's defect, and there is no replace mode for this hook, so nothing behind the compare could catch it either"
},
{
"mitigation": "",
"risk": "medium",
"what": "the original accumulates by player->index but writes back by the player's position in the server vector, into a fixed 32-int array with no bounds check",
"why": "a real latent bug in the original that our side reproduces only while index == position; the reference save never separates them"
},
{
"mitigation": "",
"risk": "medium",
"what": "PassSchedule() is never called by the hook, and FleetSummary::targetFleetId / relation are never filled",
"why": "the header claims ours predicts the call order for a trace to check; that prediction is not actually emitted"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Game::TechTree::ProcessResearch": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "region:events (EvNxID now diverges instead of passing silently)",
"risk": "high",
"what": "posts EVENT_RESEARCH_OVERBUDGET on the owner's EventStorage in the same branch that sets node.flag = 2",
"why": "the message text is composed from the tech name, so ours cannot synthesise it; it would have to be posted through the game's own event API. This is the defect that made a clean compare false: replace mode's autosave differed from the oracle by exactly this one event"
},
{
"mitigation": "region:events",
"risk": "medium",
"what": "posts EVENT_TECHS_UNLOCKED for nodes that became available this turn",
"why": "the trailing unlock loop makes no draw and writes no node, but it does build a names list and post an event"
},
{
"mitigation": "guard:player, guard:tree_header",
"risk": "high",
"what": "TechTree::SetResearched on completion: the turn/order stamps, the child unlock cascade, the recursive research of zero-cost children, and the owner's OnTechResearched callback",
"why": "its own milestone (B2); the callback writes live player state that compare mode must not touch, and it consumes one extra RNG word"
},
{
"mitigation": "guard:tree_header",
"risk": "medium",
"what": "bumps the tree's completion-order counter (TechTree+0x20)",
"why": "part of SetResearched; the per-node `order` word is compared but the counter it comes from was not a region"
},
{
"mitigation": "",
"risk": "low",
"what": "writes a completion line to the game log",
"why": "log text is not simulation state"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Game::WeaponDictionary::Init": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "suspected cause of the sibling section hook's compare crash (docs/M2.md)",
"risk": "high",
"what": "LoadWeapon -> WeaponDef::ParseScript registers each weapon's name with the string table and resolves `requires` against the live TechTree",
"why": "per-file parsing is M3 scope; ours delegates to the game's own LoadWeapon, so a compare run performs the registration a SECOND time and neither the string table nor the tech tree is a declared region"
},
{
"mitigation": "",
"risk": "low",
"what": "allocates 123 WeaponDef objects (0x278 bytes each) on the game heap",
"why": "the definitions do not exist when the hook is entered, so they cannot be a before-snapshot; the dictionary region compares them by id/name/path"
},
{
"mitigation": "guard:dict",
"risk": "low",
"what": "the word at dictionary+0x14",
"why": "not modelled; emitted as an opaque pointer, which the default policy ignores -- a change is visible in a trace but never a divergence"
},
{
"mitigation": "",
"risk": "low",
"what": "writes lines to the game log for a missing manifest",
"why": "log text is not simulation state"
},
{
"mitigation": "",
"risk": "low",
"what": "std::sort tie order for equal weapon names",
"why": "msvc_sort.h replays MSVC 2010's introsort, but the shipped data has no tied names, so the tie rule is unexercised rather than verified"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Mars::GlobalConsts::LoadFile": {
"coverage": {
"state": "partial",
"unmodelled": [
{
"mitigation": "LoadAll's post-state would have to be hooked to see it",
"risk": "medium",
"what": "erases each consumed key from the caller's std::map",
"why": "the map is a LoadAll temporary; declaring a red-black tree as a region is not possible before the call. First-occurrence-wins is reproduced in game::config::apply instead, so the *effect* is modelled, the container is not"
},
{
"mitigation": "",
"risk": "low",
"what": "writes three kinds of line to the game log (unrecognised key, applied key, expected-but-not-found)",
"why": "log text is not part of the simulation state"
},
{
"mitigation": "",
"risk": "low",
"what": "opens the file through the VFS and allocates/releases a refcounted buffer",
"why": "ours performs the same two calls, so allocation behaviour matches by construction rather than by comparison"
},
{
"mitigation": "",
"risk": "low",
"what": "String slots assign through the engine's own std::string, leaking one heap block per long string in compare mode",
"why": "start-up only; documented in docs/M1.md"
}
],
"why": ""
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
},
"Shim::SelfTest::Fill": {
"coverage": {
"state": "complete",
"unmodelled": [],
"why": "Fill writes buf[0..n) and nothing else; the whole range is a declared region"
},
"ftol": 0,
"ftol_kind": "abs",
"ptr": "ignore"
}
},
"inline_max": 256,
"started": "2026-09-08T07:22:42Z"
}
],
"totals": {
"calls": 45,
"compared": 45,
"coverage_contradicted": 0,
"coverage_unstated": 0,
"diverged": 8,
"guarded_calls": 45,
"invalid_records": 0,
"undeclared_calls": 15,
"undeclared_writes": 42
},
"warnings": []
}

37
verify/results/compare/mf-before.md Normal file
View file

@ -0,0 +1,37 @@
## tracecmp report: mf-before-compare.jsonl
- build: recap-7584bad-20260908T0615Z started: 2026-09-08T07:22:42Z inline_max: 256
- calls: 45 compared: 45 diverged: 8 invalid records: 0 warnings: 0
- coverage: 45 guarded call(s), 42 undeclared write(s) in 15 call(s); 0 hook(s) unstated, 0 contradicted
| hook | calls | modes | compared | diverged | errors |
|---|---|---|---|---|---|
| Game::StrategyServer::MoveFleet | 45 | compare:45 | 45 | 8 | 0 |
### coverage
| hook | verdict | compared regions | guards | undeclared writes | unmodelled |
|---|---|---|---|---|---|
| Game::StrategyServer::MoveFleet | partial | pos, prev_pos, rng, ship[0].range, ship[1].range, ship[2].range, +7 | fleet | 42 in 15 call(s) | 6 |
#### Game::StrategyServer::MoveFleet — not checked by this run
- (high) on arrival: dispatches SEFleetArrived and runs one of three arrival handlers by destination kind (enter system / join fleet / stop at point) — declared input boundary -- an arriving call is expected to differ in all of it, and none of it is declared, so the compare says nothing about arrivals [guard:fleet sees the fleet's own words; the event and the system do not]
- (high) on departure: cancels every still-acting ship (with a log line each) and calls ServerSystem::FleetDeparts, which rewrites the system's ownership bits — writes through pointers to ships and to the system
- (medium) the tanker top-up refuels other ships in the fleet — the per-ship range regions would show it, but ours does not model it, so a fleet with a tanker diverges for a known reason
- (medium) a node-line waypoint's step comes from the stutter profile — NodeLineStep / BuildStutterSegments are written and unit-tested but not wired in; the hook steps every waypoint type as speed x dt, so a node-line leg is knowingly mis-stepped and only its type is recorded [declared gap: docs/B4.md]
- (medium) a missed probabilistic jump scatters the fleet in a random direction — the direction is a second draw whose mapping is not modelled; ours leaves the position alone and reports the scatter distance, so the generator region diverges by one word on a miss
- (medium) the route revalidation and the waypoint list itself — declared input boundary; the waypoint vector is not a region
- guard hits in compare mode: fleet+0xa0:4, fleet+0xdc:1, fleet+0x10c:1, fleet+0xcc:1, fleet+0xdb:2, fleet+0xe0:26
### Game::StrategyServer::MoveFleet: first 5 of 8 divergent call(s)
- call_id 42 (mf-before-compare.jsonl:44)
side.pos.after.v.y [exact] orig={"t":"f32","v":3.1515913} ours={"t":"f32","v":3.15159106}
- call_id 79 (mf-before-compare.jsonl:81)
side.pos.after.v.y [exact] orig={"t":"f32","v":1.58417809} ours={"t":"f32","v":1.58417821}
- call_id 80 (mf-before-compare.jsonl:82)
side.pos.after.v.y [exact] orig={"t":"f32","v":4.21149492} ours={"t":"f32","v":4.21149445}
- call_id 116 (mf-before-compare.jsonl:118)
side.pos.after.v.y [exact] orig={"t":"f32","v":0.0167649984} ours={"t":"f32","v":0.0167651176}
- call_id 118 (mf-before-compare.jsonl:120)
side.pos.after.v.y [exact] orig={"t":"f32","v":3.14307928} ours={"t":"f32","v":3.14307904}
other divergent call_ids: [154, 156, 157]

43
verify/results/shim/mf-after-shim.log Normal file
View file

@ -0,0 +1,43 @@
03:31:44.723 [tid 2752] ==== sots-engine shim (binkw32 proxy) build mf-45bdf7d-dirty-20260908T0721Z ====
03:31:44.723 [tid 2752] exe: C:\SOTS\Sword of the Stars.exe
03:31:44.723 [tid 2752] exe base=0x00e80000 (link-time image base 0x00400000, ASLR delta +11010048) pid=800 shim=696b0000
03:31:44.723 [tid 2752] addresses: Source: sots-re ghidra/addresses.json @ e0c3e64, generated 2026-09-08 by tools/gen_addresses.py
03:31:44.723 [tid 2752] config: hooks=trace
03:31:44.723 [tid 2752] config: hook.Shim::SelfTest::Fill=off
03:31:44.723 [tid 2752] config: hook.Mars::GlobalConsts::LoadFile=off
03:31:44.723 [tid 2752] config: hook.Game::WeaponDictionary::Init=off
03:31:44.723 [tid 2752] config: hook.Game::SectionDictionary::SectionDictionary=off
03:31:44.723 [tid 2752] config: hook.Game::TechTree::ProcessResearch=off
03:31:44.723 [tid 2752] config: hook.Game::ServerPlayer::ComputeBudget=off
03:31:44.723 [tid 2752] config: hook.Game::StrategyServer::ProcessFleetMovement=off
03:31:44.723 [tid 2752] config: hook.Game::ServerPlayer::OnTechResearched=compare
03:31:44.723 [tid 2752] config: hook.Game::ServerSystem::ProcessTurn=compare
03:31:44.723 [tid 2752] config: hook.Game::StrategyServer::MoveFleet=compare
03:31:44.723 [tid 2752] config: trace.path=C:\SOTS\shim.trace.jsonl
03:31:44.723 [tid 2752] config: trace.inline_max=256
03:31:44.723 [tid 2752] config: trace.flush=always
03:31:45.114 [tid 2752] trace: C:\SOTS\shim.trace.jsonl (default mode trace, inline_max 256, flush always)
03:31:45.114 [tid 2752] hook: Mars_Application_Initialize rva=0x004a0e50 -> va=01320e50
03:31:45.114 [tid 2752] hook: MH_Initialize -> MH_OK
03:31:45.114 [tid 2752] hook: MH_CreateHook -> MH_OK (trampoline=01bd0fe0)
03:31:45.145 [tid 2752] hook: MH_EnableHook -> MH_OK
03:31:45.145 [tid 2752] cfg: GlobalConsts hook ready (scale constant 0.017453292519943295)
03:31:45.145 [tid 2752] hook: Mars::GlobalConsts::LoadFile rva=0x004b73c0 mode=off (not installed)
03:31:45.145 [tid 2752] dict: dictionaries hook ready (crt new=6adc232b delete=6adc0174)
03:31:45.145 [tid 2752] hook: Game::WeaponDictionary::Init rva=0x0019a4c0 mode=off (not installed)
03:31:45.145 [tid 2752] hook: Game::SectionDictionary::SectionDictionary rva=0x00176f40 mode=off (not installed)
03:31:45.145 [tid 2752] research: ProcessResearch hook ready (Cost=00ffda00, node=0x34, rng=0x9cc, fpu_cw=0x027f)
03:31:45.145 [tid 2752] hook: Game::TechTree::ProcessResearch rva=0x001876c0 mode=off (not installed)
03:31:45.145 [tid 2752] techfx: OnTechResearched hook ready (regions=15, gate=0/0, fpu_cw=0x027f)
03:31:45.145 [tid 2752] hook: Game::ServerPlayer::OnTechResearched rva=0x00491790 -> va=01311790 MH_CreateHook -> MH_OK (trampoline=01bd0fc0)
03:31:45.161 [tid 2752] hook: Game::ServerPlayer::OnTechResearched MH_EnableHook -> MH_OK mode=compare
03:31:45.161 [tid 2752] hook: Game::ServerPlayer::ComputeBudget rva=0x00463030 mode=off (not installed)
03:31:45.161 [tid 2752] hook: Game::ServerSystem::ProcessTurn rva=0x003598e0 -> va=011d98e0 MH_CreateHook -> MH_OK (trampoline=01bd0fa0)
03:31:45.177 [tid 2752] hook: Game::ServerSystem::ProcessTurn MH_EnableHook -> MH_OK mode=compare
03:31:45.177 [tid 2752] hook: Game::StrategyServer::MoveFleet rva=0x003d9ee0 -> va=01259ee0 MH_CreateHook -> MH_OK (trampoline=01bd0f80)
03:31:45.192 [tid 2752] hook: Game::StrategyServer::MoveFleet MH_EnableHook -> MH_OK mode=compare
03:31:45.192 [tid 2752] hook: Game::StrategyServer::ProcessFleetMovement rva=0x003da9a0 mode=off (not installed)
03:31:45.192 [tid 2752] selftest: Shim::SelfTest::Fill mode=off checksum=075ef0c3 records=0
03:31:45.255 [tid 2752] Application::Initialize called (this=03bc8128)
03:41:03.116 [tid 2752] techfx: ours mode=compare id=10001 granted=10197 plague=0x00 systems_ai=0 civcaps=0 temperance=0x00 bore_changed=0 bore_present=0 roll=0 value=-1
03:42:06.288 [tid 2752] techfx: ours mode=compare id=10094 granted=10197 plague=0x00 systems_ai=0 civcaps=0 temperance=0x00 bore_changed=0 bore_present=0 roll=1 value=0.316456825

BIN
verify/results/shim/mf-after-turn2.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 165 KiB

BIN
verify/results/shim/mf-after-turn7.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 165 KiB

43
verify/results/shim/mf-before-shim.log Normal file
View file

@ -0,0 +1,43 @@
03:22:42.435 [tid 3356] ==== sots-engine shim (binkw32 proxy) build recap-7584bad-20260908T0615Z ====
03:22:42.435 [tid 3356] exe: C:\SOTS\Sword of the Stars.exe
03:22:42.435 [tid 3356] exe base=0x00e80000 (link-time image base 0x00400000, ASLR delta +11010048) pid=2184 shim=696b0000
03:22:42.435 [tid 3356] addresses: Source: sots-re ghidra/addresses.json @ ff67ec0, generated 2026-09-08 by tools/gen_addresses.py
03:22:42.435 [tid 3356] config: hooks=trace
03:22:42.435 [tid 3356] config: hook.Shim::SelfTest::Fill=off
03:22:42.435 [tid 3356] config: hook.Mars::GlobalConsts::LoadFile=off
03:22:42.435 [tid 3356] config: hook.Game::WeaponDictionary::Init=off
03:22:42.435 [tid 3356] config: hook.Game::SectionDictionary::SectionDictionary=off
03:22:42.435 [tid 3356] config: hook.Game::TechTree::ProcessResearch=off
03:22:42.435 [tid 3356] config: hook.Game::ServerPlayer::ComputeBudget=off
03:22:42.435 [tid 3356] config: hook.Game::StrategyServer::ProcessFleetMovement=off
03:22:42.435 [tid 3356] config: hook.Game::ServerPlayer::OnTechResearched=compare
03:22:42.435 [tid 3356] config: hook.Game::ServerSystem::ProcessTurn=compare
03:22:42.435 [tid 3356] config: hook.Game::StrategyServer::MoveFleet=compare
03:22:42.435 [tid 3356] config: trace.path=C:\SOTS\shim.trace.jsonl
03:22:42.435 [tid 3356] config: trace.inline_max=256
03:22:42.435 [tid 3356] config: trace.flush=always
03:22:42.497 [tid 3356] trace: C:\SOTS\shim.trace.jsonl (default mode trace, inline_max 256, flush always)
03:22:42.497 [tid 3356] hook: Mars_Application_Initialize rva=0x004a0e50 -> va=01320e50
03:22:42.497 [tid 3356] hook: MH_Initialize -> MH_OK
03:22:42.497 [tid 3356] hook: MH_CreateHook -> MH_OK (trampoline=017d0fe0)
03:22:42.513 [tid 3356] hook: MH_EnableHook -> MH_OK
03:22:42.513 [tid 3356] cfg: GlobalConsts hook ready (scale constant 0.017453292519943295)
03:22:42.513 [tid 3356] hook: Mars::GlobalConsts::LoadFile rva=0x004b73c0 mode=off (not installed)
03:22:42.513 [tid 3356] dict: dictionaries hook ready (crt new=6adc232b delete=6adc0174)
03:22:42.513 [tid 3356] hook: Game::WeaponDictionary::Init rva=0x0019a4c0 mode=off (not installed)
03:22:42.513 [tid 3356] hook: Game::SectionDictionary::SectionDictionary rva=0x00176f40 mode=off (not installed)
03:22:42.513 [tid 3356] research: ProcessResearch hook ready (Cost=00ffda00, node=0x34, rng=0x9cc, fpu_cw=0x027f)
03:22:42.513 [tid 3356] hook: Game::TechTree::ProcessResearch rva=0x001876c0 mode=off (not installed)
03:22:42.513 [tid 3356] techfx: OnTechResearched hook ready (regions=15, gate=0/0, fpu_cw=0x027f)
03:22:42.513 [tid 3356] hook: Game::ServerPlayer::OnTechResearched rva=0x00491790 -> va=01311790 MH_CreateHook -> MH_OK (trampoline=017d0fc0)
03:22:42.528 [tid 3356] hook: Game::ServerPlayer::OnTechResearched MH_EnableHook -> MH_OK mode=compare
03:22:42.528 [tid 3356] hook: Game::ServerPlayer::ComputeBudget rva=0x00463030 mode=off (not installed)
03:22:42.528 [tid 3356] hook: Game::ServerSystem::ProcessTurn rva=0x003598e0 -> va=011d98e0 MH_CreateHook -> MH_OK (trampoline=017d0fa0)
03:22:42.544 [tid 3356] hook: Game::ServerSystem::ProcessTurn MH_EnableHook -> MH_OK mode=compare
03:22:42.544 [tid 3356] hook: Game::StrategyServer::MoveFleet rva=0x003d9ee0 -> va=01259ee0 MH_CreateHook -> MH_OK (trampoline=017d0f80)
03:22:42.560 [tid 3356] hook: Game::StrategyServer::MoveFleet MH_EnableHook -> MH_OK mode=compare
03:22:42.560 [tid 3356] hook: Game::StrategyServer::ProcessFleetMovement rva=0x003da9a0 mode=off (not installed)
03:22:42.560 [tid 3356] selftest: Shim::SelfTest::Fill mode=off checksum=075ef0c3 records=0
03:22:42.560 [tid 3356] Application::Initialize called (this=03b18128)
03:28:46.630 [tid 3356] techfx: ours mode=compare id=10001 granted=10197 plague=0x00 systems_ai=0 civcaps=0 temperance=0x00 bore_changed=0 bore_present=0 roll=0 value=-1
03:29:49.817 [tid 3356] techfx: ours mode=compare id=10094 granted=10197 plague=0x00 systems_ai=0 civcaps=0 temperance=0x00 bore_changed=0 bore_present=0 roll=1 value=0.316456825

BIN
verify/results/shim/mf-before-turn2.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 166 KiB

BIN
verify/results/shim/mf-before-turn7.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 165 KiB

BIN
verify/results/shim/mf-human-home-no-ships.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 366 KiB

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):

188
verify/traces/mf-after-compare.jsonl Normal file
View file

File diff suppressed because one or more lines are too long

188
verify/traces/mf-before-compare.jsonl Normal file
View file

File diff suppressed because one or more lines are too long