board: lane C state-checksum landed; fpu_cw experiment queued; event-posting lane
This commit is contained in:
parent
fdd0b72b7a
commit
9d385a7683
18 changed files with 1858 additions and 16 deletions
|
|
@ -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} -->
|
||||||
|
|
|
||||||
|
|
@ -77,3 +77,6 @@ Status flow: `backlog → in-progress → mapped → verified` (or `blocked`).
|
||||||
| 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) |
|
| 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
152
findings/subsystems/movefleet-position-rounding.md
Normal 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.
|
||||||
|
|
@ -438,7 +438,7 @@
|
||||||
"name": "Script_ScanToken",
|
"name": "Script_ScanToken",
|
||||||
"addr": "0x008cd1f0",
|
"addr": "0x008cd1f0",
|
||||||
"convention": "custom",
|
"convention": "custom",
|
||||||
"prototype": "/* EAX=cursor, ECX="edFlag, EDX=out; stack: end, outEnd, &len \u2014 internal, do not hook */",
|
"prototype": "/* EAX=cursor, ECX="edFlag, 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"
|
||||||
}
|
}
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -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
499
verify/results/compare/mf-after.json
Normal 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
24
verify/results/compare/mf-after.md
Normal 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
604
verify/results/compare/mf-before.json
Normal 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
37
verify/results/compare/mf-before.md
Normal 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
43
verify/results/shim/mf-after-shim.log
Normal 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
BIN
verify/results/shim/mf-after-turn2.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 165 KiB |
BIN
verify/results/shim/mf-after-turn7.png
Normal file
BIN
verify/results/shim/mf-after-turn7.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 165 KiB |
43
verify/results/shim/mf-before-shim.log
Normal file
43
verify/results/shim/mf-before-shim.log
Normal 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
BIN
verify/results/shim/mf-before-turn2.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 166 KiB |
BIN
verify/results/shim/mf-before-turn7.png
Normal file
BIN
verify/results/shim/mf-before-turn7.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 165 KiB |
BIN
verify/results/shim/mf-human-home-no-ships.png
Normal file
BIN
verify/results/shim/mf-human-home-no-ships.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 366 KiB |
188
verify/traces/mf-after-compare.jsonl
Normal file
188
verify/traces/mf-after-compare.jsonl
Normal file
File diff suppressed because one or more lines are too long
188
verify/traces/mf-before-compare.jsonl
Normal file
188
verify/traces/mf-before-compare.jsonl
Normal file
File diff suppressed because one or more lines are too long
Loading…
Add table
Reference in a new issue