lane U: the unlock cascade, implemented and live-verified
Reads: TechTree::PrereqsMet 0x0057d8e0 (AND of ORs; zero groups TRUE, an empty group FALSE), the prerequisite layout at TechDef+0x88/+0x98, the tail collector 0x00587cc3, and the head of OnTechResearched (RecordObservedTech unconditional; the research-event roll gated on ResT == def && ResearchRollPending). Live: 35 compared calls over three workloads, 0 divergences, tracecmp exit 0, End-Turn oracle hashes unchanged. The EVENT_TECHS_UNLOCKED residual lane P predicted and lane V measured is closed by running the cascade, not by posting on completion. 12 new addresses in ghidra/addresses.d/lane-u.json (header 615 -> 627).
This commit is contained in:
parent
ae00053e04
commit
5a3f986f38
15 changed files with 2892 additions and 7 deletions
|
|
@ -59,8 +59,8 @@ Status flow: `backlog → in-progress → mapped → verified` (or `blocked`).
|
|||
| P2-B3 ProcessResearch (behavioral, RNG) | phase2 | mapped | high | 85% | 2026-09-08 | LIVE, PARTIAL PASS: 15 calls compared, 13 zero-divergence; RNG post-state matched 14/15 incl. every roll (validates MT19937 + draw mapping + odds together). 2 divergences are the declared SetResearched boundary. ORACLE FAILS by exactly one item across 40,300: an unposted EVENT_RESEARCH_OVERBUDGET - compare was blind because the event list was never a declared region. fpu_cw=0x127f => 53-bit double, x87 question SETTLED. No Zuul in the save: double roll still disassembly-only . RECAPTURED WITH GUARDS 2026-09-08 (lane R): the oracle gap is now a COMPARE DIVERGENCE - `side.events.after.v.next_id orig=4 ours=3` on call 0, its only divergent field, with node[144] progress 2879->5768 and flag 1->2 both reproduced and the single RNG draw identical. 15 calls over 5 turns: 3 diverged, **RNG 15/15** (better than the original 14/15 - no tech-effect draw in this session). Guards on the two completion calls map SetResearched: ConMod[0..2]/OutMod/PopMod, ResTNm, TechTree+0x20 order counter, and the undeclared otch vector | . **LANE V 2026-09-08 (build `eventlive-dd38117-20260908T0916Z`): the events divergence is CLOSED on the reference turn** - 3 calls, 3 compared, **0 diverged, exit 0**. Over 5 turns 15 calls / **2** diverged (was 3), both short by exactly 1 `next_id` = the unmodelled `EVENT_TECHS_UNLOCKED`. **CORRECTION to lane R's 'RNG 15/15': that was WORKLOAD LUCK, not a property.** On lane V's call 9 the completed tech had `research_roll_pending` set, so the original drew one word `ours` did not (`left` 374 vs 375, `next_index` 250 vs 249) - the `OnTechResearched` callback draw, a DECLARED out-of-scope boundary (P-events-wiring §3 says so in as many words). Honest statement: the `rng` region reproduces bit-for-bit on every call that does not complete a roll-triggering tech, and is short by exactly one draw on every call that does. Also live: `sizeof(ObservedTech)` = **44**, measured twice (`observed_techs.bytes` 440->484 and 484->528). Zuul double roll now CLOSED on a species-5 save lane V made - see its own row
|
||||
| RNG signatures (Ghidra) | meta | verified | high | 100% | 2026-09-08 | Seed/Twist/NextFloat/NextInt verified; draw = y/(2^32-1); NextInt [0,n] inclusive; lazy twist; left@+0x9c4. RUNTIME CONFIRMED: fpu_cw=0x127f (53-bit double, round-nearest) - our next_float model is right, float_from_pc24 is an unused contingency |
|
||||
| engine: game/effects | engine | verified | high | 100% | 2026-09-08 | merged: TechId enum (196 slots @10000+i), 44 ids with typed strategic effects, species flag bits, ApplyTechEffect; 254 checks |
|
||||
| VM140 exclusivity (lab rule) | meta | verified | high | 100% | 2026-09-08 | one agent at a time. Holder: **U-unlock** (V-eventlive released 2026-09-08 05:52 local; F-fpucw before it, M-movefleet before that). QUEUE: empty. VM left at the MAIN MENU, `hooks=trace`, build `recap-7584bad-20260908T0615Z` restored from `C:\SOTS\shimdist-recap` (that dist also carries `shim.cfg.recap{trace,b3,b1,misc}`). Lane M also left `C:\SOTS\shimdist-mf` + `C:\SOTS\ui\mf{deploy,release}.ps1` in place - harmless, and a working template for the next lane. Windows Update DISABLED/paused on the VM. Non-holders build /srv/re-lab/build/sots-engine-<lane>, stage dist-<lane>, deploy C:\SOTS\shimdist-<lane>. GOTCHA (lane R): after `schtasks /Run /TN SOTS` the main menu can take >60 s - SCREENSHOT AND VERIFY before clicking, or the click path lands in Credits. GOTCHA (lane M): drive the load dialog ONE rui.ps1 CALL PER CLICK with a screenshot between - a single chained cmd.txt loses sync and silently ends up somewhere else. And the Load Game dialog does NOT pre-select Single Player on a fresh launch: the documented path really is Load Game (512,536) -> Single Player (512,290) -> OK (551,523) -> row -> OK (682,624) -> Launch (511,663). ref-turn2 row is at (400,436) GOTCHA (lane F, confirms lane R): the >60 s startup is REAL and cost a whole wasted run — do not sleep-and-click, **verify the main menu from a screenshot** (`verify/fpu-cw/` run scripts poll a screenshot until the Load Game / Exit buttons are bright red; 3 probes ≈ 25 s was typical). TIP (lane F): reset `SavedGames\` to a fixed file set before every run — the Load dialog row positions depend on how many files are listed, so a constant set means the click path never has to be re-derived (with the 4-file set ref-turn2 sits at (400,348), not (400,436)). PowerShell over SSH mangles quoting badly: send snippets base64 as `powershell -EncodedCommand`, or use `-ExecutionPolicy Bypass -File`. Lane F left `C:\SOTS\shimdist-fpu` + `C:\SOTS\ui\f{deploy,grab,fpu}.ps1` + `C:\SOTS\ui\preF\` (the pre-lane-F SavedGames snapshot, restored) in place. VM RESTORED: recap build `recap-7584bad-20260908T0615Z`, `hooks=trace`, SavedGames back to the 7-file pre-F set, main menu verified by screenshot. GOTCHA (lane V, third confirmation): the >60 s startup is REAL - the Kerberos intro was still on screen at t+30 s and the main menu appeared at ~t+70 s. GOTCHA (lane V): `type <text>` via the click helper did **NOT** register in the game's text fields this session (neither the Create Game name nor the Save Game file name took SendKeys); the workaround is to accept the default name and **rename the `.sav` on disk** - the Load dialog lists files by FILENAME. SAVEDGAMES IS NOW **8 FILES**: the pre-existing 7 plus `zuul-turn5.sav` (a species-5 save, see the Zuul row). Row positions are UNCHANGED for existing lanes because `zuul-turn5` sorts last: **ref-turn2 is still (400,436)**, zuul-turn5 is the new row 8 at (400,465), rows 29 px apart from y=262 - verified by screenshot `verify/results/shim/eventlive/load-dialog-8files.png`. The three autosaves now belong to the Zuul game. Lane V left `C:\SOTS\shimdist-v` + `C:\SOTS\ui\v{deploy,release,click}.ps1`. VM RESTORED: recap build `recap-7584bad-20260908T0615Z`, `hooks=trace`, main menu verified by screenshot. |
|
||||
| Zuul double-roll (behavioural) | verify | verified | high | 100% | 2026-09-08 | **CLOSED by lane V 2026-09-08.** No species-5 save existed, so lane V MADE one on VM140: a custom game with only Zuul left in the Available Species pool (both players Zuul), 4 End Turns under `shim.cfg.recapb3`. **8 calls, 8 compared, 0 diverged, exit 0.** All four researching calls have `species=5` and the generator advances by TWO, not one: `left` 540->538 / 522->520 / 504->502 / 485->483, `next_index` +2 each, `mt` hash unchanged; `ours` reproduced every post-state bit-for-bit. Save `verify/results/saves/zuul-turn5-species5.sav` (48559ab5b719b332, 59,131 B, turn 5, homeworld Gallandro) and on the VM as `C:\SOTS\SavedGames\zuul-turn5.sav`. NOT yet exercised by it: a Zuul tech COMPLETION (node 144 was at ~4,700 of 5,000 after 5 turns - one more End Turn gets there), so `SetResearched` and the Zuul boarding-pod grant are still untouched. Report `findings/subsystems/eventlive-verification.md` §5 |
|
||||
| VM140 exclusivity (lab rule) | meta | verified | high | 100% | 2026-09-08 | one agent at a time. Holder: **FREE** (U-unlock released 2026-09-08 06:55 local; V-eventlive before it; F-fpucw before it, M-movefleet before that). QUEUE: empty. VM left at the MAIN MENU, `hooks=trace`, build `recap-7584bad-20260908T0615Z` restored from `C:\SOTS\shimdist-recap` (that dist also carries `shim.cfg.recap{trace,b3,b1,misc}`). Lane M also left `C:\SOTS\shimdist-mf` + `C:\SOTS\ui\mf{deploy,release}.ps1` in place - harmless, and a working template for the next lane. Windows Update DISABLED/paused on the VM. Non-holders build /srv/re-lab/build/sots-engine-<lane>, stage dist-<lane>, deploy C:\SOTS\shimdist-<lane>. GOTCHA (lane R): after `schtasks /Run /TN SOTS` the main menu can take >60 s - SCREENSHOT AND VERIFY before clicking, or the click path lands in Credits. GOTCHA (lane M): drive the load dialog ONE rui.ps1 CALL PER CLICK with a screenshot between - a single chained cmd.txt loses sync and silently ends up somewhere else. And the Load Game dialog does NOT pre-select Single Player on a fresh launch: the documented path really is Load Game (512,536) -> Single Player (512,290) -> OK (551,523) -> row -> OK (682,624) -> Launch (511,663). ref-turn2 row is at (400,436) GOTCHA (lane F, confirms lane R): the >60 s startup is REAL and cost a whole wasted run — do not sleep-and-click, **verify the main menu from a screenshot** (`verify/fpu-cw/` run scripts poll a screenshot until the Load Game / Exit buttons are bright red; 3 probes ≈ 25 s was typical). TIP (lane F): reset `SavedGames\` to a fixed file set before every run — the Load dialog row positions depend on how many files are listed, so a constant set means the click path never has to be re-derived (with the 4-file set ref-turn2 sits at (400,348), not (400,436)). PowerShell over SSH mangles quoting badly: send snippets base64 as `powershell -EncodedCommand`, or use `-ExecutionPolicy Bypass -File`. Lane F left `C:\SOTS\shimdist-fpu` + `C:\SOTS\ui\f{deploy,grab,fpu}.ps1` + `C:\SOTS\ui\preF\` (the pre-lane-F SavedGames snapshot, restored) in place. VM RESTORED: recap build `recap-7584bad-20260908T0615Z`, `hooks=trace`, SavedGames back to the 7-file pre-F set, main menu verified by screenshot. GOTCHA (lane V, third confirmation): the >60 s startup is REAL - the Kerberos intro was still on screen at t+30 s and the main menu appeared at ~t+70 s. GOTCHA (lane V): `type <text>` via the click helper did **NOT** register in the game's text fields this session (neither the Create Game name nor the Save Game file name took SendKeys); the workaround is to accept the default name and **rename the `.sav` on disk** - the Load dialog lists files by FILENAME. SAVEDGAMES IS NOW **8 FILES**: the pre-existing 7 plus `zuul-turn5.sav` (a species-5 save, see the Zuul row). Row positions are UNCHANGED for existing lanes because `zuul-turn5` sorts last: **ref-turn2 is still (400,436)**, zuul-turn5 is the new row 8 at (400,465), rows 29 px apart from y=262 - verified by screenshot `verify/results/shim/eventlive/load-dialog-8files.png`. The three autosaves now belong to the Zuul game. Lane V left `C:\SOTS\shimdist-v` + `C:\SOTS\ui\v{deploy,release,click}.ps1`. VM RESTORED: recap build `recap-7584bad-20260908T0615Z`, `hooks=trace`, main menu verified by screenshot. LANE U (2026-09-08): left `C:\SOTS\shimdist-u` + `C:\SOTS\ui\u{deploy,release}.ps1` in place. SavedGames is STILL 8 FILES (the three autosaves now belong to the Zuul game at turn 15) - **ref-turn2 is still (400,436)**, zuul-turn5 still (400,465). A QEMU-level screenshot (feed `screendump /tmp/vm140.ppm` to `qm monitor 140` on spicy, then scp the .ppm) is more reliable than the click helper's `shot` action and does not need the game window. FOURTH confirmation of the >60 s startup: the Kerberos intro was still on screen at t+45 s, the main menu at ~t+85 s. VM RESTORED: recap build `recap-7584bad-20260908T0615Z`, `hooks=trace`, main menu verified by screenshot. |
|
||||
| Zuul double-roll (behavioural) | verify | verified | high | 100% | 2026-09-08 | **CLOSED by lane V 2026-09-08.** No species-5 save existed, so lane V MADE one on VM140: a custom game with only Zuul left in the Available Species pool (both players Zuul), 4 End Turns under `shim.cfg.recapb3`. **8 calls, 8 compared, 0 diverged, exit 0.** All four researching calls have `species=5` and the generator advances by TWO, not one: `left` 540->538 / 522->520 / 504->502 / 485->483, `next_index` +2 each, `mt` hash unchanged; `ours` reproduced every post-state bit-for-bit. Save `verify/results/saves/zuul-turn5-species5.sav` (48559ab5b719b332, 59,131 B, turn 5, homeworld Gallandro) and on the VM as `C:\SOTS\SavedGames\zuul-turn5.sav`. NOT yet exercised by it: a Zuul tech COMPLETION (node 144 was at ~4,700 of 5,000 after 5 turns - one more End Turn gets there), so `SetResearched` and the Zuul boarding-pod grant are still untouched. Report `findings/subsystems/eventlive-verification.md` §5 **EXTENDED by lane U 2026-09-08: the double roll and the COMPLETION PATH together.** `zuul-turn5` + 10 more End Turns (turn 5 -> 15) under the same config: **20 calls, 20 compared, 0 diverged, exit 0**, with TWO Zuul completions. Call 2 (turn 7, alloc {144,1376}) advances the generator by two (`left` 449->447, `next_index` 175->177) AND runs the unlock cascade in the same call - node 144 -> state 4 / order 21 / turn_researched 7, nodes 132 and 136 -> state 2 with cost_rp 10000 / 16000 and turn_available 7, `next_id` 10->12, `observed_techs` 396->440. Note the ZUUL tree unlocks only 132 and 136 from tech 144 where the HUMAN tree also unlocks 142, so this is an independent instance of the cascade, not a repeat. Trace `verify/traces/unlock-b3-zuul.jsonl.gz` |
|
||||
| budget tail coverage (expenses/aid/debt) | verify | backlog | — | 0% | 2026-09-08 | 8 ComputeBudget slots were always 0 in ref-turn2 (no sliders, no aid, no debt, no handicap). Need a save with expense sliders, a debtor and a research-aid treaty to exercise ExpenseTotal + the aid/bonus tail . CONFIRMED AND WORSE 2026-09-08 (lane R, 4284 calls): **13 of 22 slots are 0 on every call** - tradeIncome, shipCarriedPop, secondaryManager, bonusIncome, systemIncomeNeg, debtInterest, construction, expenses, researchMoneyGiven, savingsGiven, tra, researchPointsGiven, trp |
|
||||
| hook GetDifficultyMods | meta | backlog | — | 0% | 2026-09-08 | B1 derived the two difficulty rows from trace values (AI maintenance divisor 3, research x1.5) instead of snapshotting them; hook it properly so they stop being constants |
|
||||
| section-loader compare crash | verify | backlog | — | 0% | 2026-09-08 | SectionDictionary compare crashes the engine while the identical weapon path succeeds -> fault is in re-running LoadSection, not the manifest reader. Next boundary: hook LoadSection itself. docs/M2.md has 3 ranked leads |
|
||||
|
|
@ -69,7 +69,7 @@ Status flow: `backlog → in-progress → mapped → verified` (or `blocked`).
|
|||
| RollResearchEvent draw (behavioural) | verify | verified | high | 100% | 2026-09-08 | **CLOSED by lane R.** On turn 6 (`IND_TRKSTL`, tech 10094) `research_roll_pending` was true going in; the original drew exactly one word (rng `left` 375->374, `next_index` 249->250) and cleared the flag, and `ours` reproduced both bit-for-bit on the scratch generator. 0 divergences on that call. Needs 5 End Turns from ref-turn2 to reach - the reference turn has no completion at all | . RE-OBSERVED by lane V from the CALLER side 2026-09-08: on the B3 hook's own call 9 the same draw shows as an `rng` divergence (`left` 374 vs 375) plus guard spans `player+0x3b4` (`ResErrRoll`) and `player+0x196` (byte 2 of design mask B at `+0x194`). Still NO save that starts with `research_roll_pending` true - the flag has only ever been seen set and cleared inside one turn
|
||||
| golden-trace recapture (post-guards) | verify | verified | high | 100% | 2026-09-08 | DONE on the live game, build `recap-7584bad-20260908T0615Z` (NO source change needed - the audit's machinery did all of it). **B3 ProcessResearch: the defect is VISIBLE** - `side.events.after.v.next_id orig=4 ours=3`, one divergent call of 3 on the reference turn and its ONLY divergent field; bit-for-bit the `EvNxID 4->3` that previously needed a 609 KB save diff. Over 5 turns 15 calls / 3 diverged, **RNG matched 15/15**, and the two completion calls miss TWO event ids each. **B1 ComputeBudget: verdict held** - 4284 compared, 0 diverged, exit 0, `budget_object` guard caught 0 undeclared writes (Budget+0x64 never changed value). **MoveFleet: 8 of 45 diverge by 1 ULP of position** (new; see its own row). First guarded captures for OnTechResearched (2 calls), ServerSystem::ProcessTurn (140 calls) and MoveFleet (45). Guards mapped SetResearched live (ConMod[0..2], OutMod, PopMod, ResTNm, TechTree+0x20 order counter) and found an UNDECLARED `vector<ObservedTech> otch` append at player+0x274. Oracle held on every run's first End Turn. Report `findings/subsystems/golden-trace-recapture.md`; engine `docs/R-recapture.md`; traces `verify/traces/recap-*`, reports `verify/results/compare/recap-*`. sots-engine branch `wip/recapture` e50d5e5 (merged with main 82ef52f; ctest 32/32, clean-room OK) |
|
||||
| MoveFleet position rounding (1 ULP) | verify | verified | high | 100% | 2026-09-08 | **CLOSED by lane M.** Mechanism read off the instruction stream, not fitted: the engine's `Mars_Vec3_Normalize` (0x00422520, 123 callers) narrows to float32 FOUR times - `sumsq = f32(x*x+y*y+z*z)` (products/adds stay in 53-bit regs, only the SUM is stored), `len = f32(sqrt(sumsq))`, `inv = f32(1.0/len)` a RECIPROCAL that is MULTIPLIED through rather than three divides, and `dir.c = f32(delta.c*inv)`; and MoveFleet stores each `dest.c - pos.c` BACK TO A FLOAT32 SLOT before calling it, and takes the leg distance from that same call's return value. `ours` did all of it in double. The position tail (`f32(pos + f32(dir*move))`) was already right, which is exactly why the error was a constant ABSOLUTE ~1.2e-7. Confirmed OFFLINE first (an arrival copies the destination verbatim, so calls 115/155 hand you fleet 34's and fleet 50's exact float32 destinations = 8 fully determined legs; the 5-narrowing model reproduces the ORIGINAL bit-for-bit on all 8, the old double model reproduces `ours` on the 3 divergent ones), then LIVE: control run 8/45 diverged exit 1, fixed run **0/45 diverged exit 0**, with identical args, identical pos.before and identical ORIGINAL pos.after on all 45 calls. Report `findings/subsystems/movefleet-position-rounding.md`, engine `docs/M-movefleet.md`, branch `wip/movefleet` 2aa8cba |
|
||||
| undeclared ObservedTech append | verify | mapped | high | 60% | 2026-09-08 | NEW (lane R). A tech completion grows `vector<ObservedTech> otch` at ServerPlayer+0x274 (all three vector words move = a realloc). Seen as an undeclared write by BOTH the ProcessResearch `player` guard and the OnTechResearched `player` guard. It is serialized ServerPlayer state and it is in NO coverage note anywhere - a third list append in the same neighbourhood as the event list. B3's replace oracle never saw it because turn 1 of ref-turn2 has no completion | **APPEND SITE NOW NAMED (lane X): `RecordObservedTech` 0x007ba1a0, called from OnTechResearched; stride 0x2c.** Still needs a declared region + a model in ours. . PARTLY ADDRESSED (lane P + lane V 2026-09-08): it IS now a declared **Result** region (`observed_techs`, ServerPlayer+0x274), so it has left the guards' undeclared list and appears in the diff instead - lane V measured the span growing by exactly 44 on both completion calls (440->484, 484->528) and `ours` short by that 44 each time. STILL OPEN: `ours` does not append, so the region diverges on every completion. The element and the append site are fully pinned (lane X/S: sizeof 0x2c, RecordObservedTech 0x007ba1a0, DE-DUPLICATES BY TECH NAME), so what is left is modelling it - and that belongs with whoever takes SetResearched
|
||||
| undeclared ObservedTech append | verify | verified | high | 90% | 2026-09-08 | NEW (lane R). A tech completion grows `vector<ObservedTech> otch` at ServerPlayer+0x274 (all three vector words move = a realloc). Seen as an undeclared write by BOTH the ProcessResearch `player` guard and the OnTechResearched `player` guard. It is serialized ServerPlayer state and it is in NO coverage note anywhere - a third list append in the same neighbourhood as the event list. B3's replace oracle never saw it because turn 1 of ref-turn2 has no completion **MODELLED AND LIVE-VERIFIED by lane U 2026-09-08.** `ours` now models the append DECISION - it scans the owner's otch element NAMES pre-call (the original appends during the call, so a scan taken afterwards would find the tech present and "agree" with a count it never computed) and reproduces `RecordObservedTech`'s de-duplication by name, then moves the SCRATCH header's byte span by one 0x2c element per append. `observed_techs.bytes` now matches on every call in all three runs (440->484, 484->528 on the five-turn; 396->440, 440->484 on the Zuul). STILL NOT MODELLED: the element's own fields (turn_first/turn_last/detected/name/with) - no region can see them | **APPEND SITE NOW NAMED (lane X): `RecordObservedTech` 0x007ba1a0, called from OnTechResearched; stride 0x2c.** Still needs a declared region + a model in ours. . PARTLY ADDRESSED (lane P + lane V 2026-09-08): it IS now a declared **Result** region (`observed_techs`, ServerPlayer+0x274), so it has left the guards' undeclared list and appears in the diff instead - lane V measured the span growing by exactly 44 on both completion calls (440->484, 484->528) and `ours` short by that 44 each time. STILL OPEN: `ours` does not append, so the region diverges on every completion. The element and the append site are fully pinned (lane X/S: sizeof 0x2c, RecordObservedTech 0x007ba1a0, DE-DUPLICATES BY TECH NAME), so what is left is modelling it - and that belongs with whoever takes SetResearched
|
||||
| unnamed offsets from guard hits | verify | backlog | — | 0% | 2026-09-08 | NEW (lane R). Three spans the guards report every run and no addresses.json entry names: **ServerSystem+0xd8 (1 B)** and **ServerSystem+0x238 (4 B)** - written by the AI home system on every colony turn, alongside the fleet-vector growth; **StarFleet+0xdc (1 B)** - written on every moving MoveFleet call, just past Speed (FPsp2 @0xd8). Cheap wins for the contract |
|
||||
| waypoint types 2-5 have no coverage | verify | backlog | — | 0% | 2026-09-08 | NEW (lane M, promoted from a coverage line to its own row because it is now the biggest gap in `MoveFleet`). Types 2 (node line), 3 (node route), 4 (gate teleport) and 5 (probabilistic jump) have NEVER fired in any capture, and the node-line step is WRONG BY CONSTRUCTION - `sim::NodeLineStep` and `sim::BuildStutterSegments` are written and host-tested but are NOT wired into the hook, which steps every waypoint type as `speed x dt`. **`ref-turn2` structurally cannot exercise them**: lane M held the VM and tried. The only mover in that save is the AI, which travels straight runs; the player that would travel a node line has `DE 00 CR 00 DN 00` at its home system (screenshot `verify/results/shim/mf-human-home-no-ships.png`), so Move/Manage Fleets are greyed out on every turn. Needs a ship built over several turns, or - much cheaper - a PURPOSE-BUILT SAVE with a fleet already in orbit next to a node line. Same save would unblock the gate-traffic and probabilistic-jump rows. Also owed on that path: `sim::Distance` is still plain double, and `Mars_Vec3_Length` (0x004224b0) says every vector length in the engine is float32-narrowed twice, so the stutter geometry is probably 1 ULP out the same way the position update was - deliberately left alone by lane M because there is no behavioural evidence to correct it against |
|
||||
| ref-turn2 has no tech completion | meta | verified | high | 100% | 2026-09-08 | TRAP for anyone writing a workload (lane R). The documented one-End-Turn recipe produces **zero** `OnTechResearched` calls - an empty log that still passes. It takes 5 End Turns (to turn 7) to reach a completion. Also: only the FIRST End Turn is reproducible - it hashed to the oracle on all four runs and its research calls reproduce docs/B3.md exactly, but from turn 4 the AI picks a different research target than B3 recorded while the point totals stay nearly identical. Treat anything past turn 1 as *a* run, not *the* run |
|
||||
|
|
@ -78,14 +78,14 @@ Status flow: `backlog → in-progress → mapped → verified` (or `blocked`).
|
|||
| event posting API | subsystem | mapped | high | 90% | 2026-09-08 | RECOVERED (lane E, `findings/subsystems/events.md`). Container: `EventStorage` embedded at `ServerPlayer+0x29c` (0x1c), `EvNxID` at +0x14 = player+0x2b0 — exactly the guard's byte run. Nested `vector<TurnEvents{int EvTurn; vector<PlayerEvent>}>`, record 0x74 B, tags `EvEID EvDsc EvMsg EvImg EvLoc EvPos EvAct EvCID`; layout confirmed field-by-field against turn3-state.sav, which CONTAINS the overbudget record. Entry point `int __thiscall EventStorage::PostEvent(this, string BYVAL, string BYVAL, obj*, Vector3*, turn, const char* img, int act)` 0x008862b0 RET 0x4c — **161 call sites in 113 functions, the whole sim's event API**. B3 defect fully explained: 0x00587b97, in the completion-roll-FAILED branch under `!wasDone && nowDone && owner`. 3 note corrections (EvPos is FLT_MAX not inf; the save array is turn-bucketed not flat; TECHS_UNLOCKED has no parent clause). 56 entries in addresses.json; 11 prototypes + 13 labels + 12 comments + 2 structs written back to Ghidra. Engine: `sots-engine` branch `wip/events` a7348be, `src/game/events` + 112 checks, ctest 32/32. NOT YET WIRED INTO A HOOK — see `docs/E-events.md` for the proposed region/Coverage change |
|
||||
| state-checksum replay harness | verify | 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) **§3.5 CLOSED 2026-09-08 by lane F** (see the fpu_cw row): measured, not assumed — 53-bit == 64-bit, so `floats=bits` costs the SSE port nothing; 24-bit and round-up each name one witness. The tool localised both to single leaves out of 35,394, with coverage PROVED on all 8 new saves. |
|
||||
| MoveFleet position ULP divergence | phase2 | verified | high | 100% | 2026-09-08 | **DONE (lane M).** First arithmetic divergence caught by BEHAVIOURAL compare rather than static reading, and it is fixed by matching the original's precision sequence rather than by fitting numbers - see the `MoveFleet position rounding (1 ULP)` row for the mechanism. Live 8 -> 0 on the same 45 calls, control run included so the before/after is this lane's own measurement. **COVERAGE IS UNCHANGED AND STILL THIN**: 15 of 45 calls move and all 15 are the same straight-run waypoint type. Waypoint types 2-5 were ATTEMPTED and could NOT be reached - the only player that would travel a node line has `DE 00 CR 00 DN 00` at its home system on this save, so its Move/Manage Fleets buttons are greyed out every turn and there is literally nothing to send along the node lines the map draws. Reaching them needs a ship BUILT over several turns, or (cheaper) a purpose-built save that starts with a fleet in orbit beside a node line. The node-line step is still wrong by construction: NodeLineStep/BuildStutterSegments exist and are unit-tested but are not wired into the hook |
|
||||
| ObservedTech append (undeclared) | verify | mapped | high | 60% | 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 | . PARTLY ADDRESSED (lane P + lane V 2026-09-08): it IS now a declared **Result** region (`observed_techs`, ServerPlayer+0x274), so it has left the guards' undeclared list and appears in the diff instead - lane V measured the span growing by exactly 44 on both completion calls (440->484, 484->528) and `ours` short by that 44 each time. STILL OPEN: `ours` does not append, so the region diverges on every completion. The element and the append site are fully pinned (lane X/S: sizeof 0x2c, RecordObservedTech 0x007ba1a0, DE-DUPLICATES BY TECH NAME), so what is left is modelling it - and that belongs with whoever takes SetResearched
|
||||
| ObservedTech append (undeclared) | verify | verified | high | 90% | 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 **MODELLED AND LIVE-VERIFIED by lane U 2026-09-08.** `ours` now models the append DECISION - it scans the owner's otch element NAMES pre-call (the original appends during the call, so a scan taken afterwards would find the tech present and "agree" with a count it never computed) and reproduces `RecordObservedTech`'s de-duplication by name, then moves the SCRATCH header's byte span by one 0x2c element per append. `observed_techs.bytes` now matches on every call in all three runs (440->484, 484->528 on the five-turn; 396->440, 440->484 on the Zuul). STILL NOT MODELLED: the element's own fields (turn_first/turn_last/detected/name/with) - no region can see them | . PARTLY ADDRESSED (lane P + lane V 2026-09-08): it IS now a declared **Result** region (`observed_techs`, ServerPlayer+0x274), so it has left the guards' undeclared list and appears in the diff instead - lane V measured the span growing by exactly 44 on both completion calls (440->484, 484->528) and `ours` short by that 44 each time. STILL OPEN: `ours` does not append, so the region diverges on every completion. The element and the append site are fully pinned (lane X/S: sizeof 0x2c, RecordObservedTech 0x007ba1a0, DE-DUPLICATES BY TECH NAME), so what is left is modelling it - and that belongs with whoever takes SetResearched
|
||||
| fpu_cw sensitivity experiment | verify | verified | high | 100% | 2026-09-08 | **DONE (lane F): 53-bit vs 64-bit x87 makes NO difference — the SSE port has no double-rounding budget to preserve, `STATE_CHECKSUM.md` §3.5 CLOSED.** 7 End Turns from ref-turn2, 6 control words, whole-state checksum on each. stock / 0x027f / 0x127f / **0x137f (64-bit)** all give `978041ac…` identical across all 35,394 leaves. Two settings DO move state, each reproduced on a repeat run: **0x007f (true 24-bit)** -> `/Sim/systems/Sys[112 "Gamma Cephei"]/Pop2/PopG/PopC 540000000->540000002` (+derived Summary/Checksum); **0x1a7f (53-bit, round-UP)** -> `/Sim/fleets/Flt[34 "Beta Fleet"]/Pos/.[0]` and `/Pos/.[2]`, 1 ULP each. So the port must hold intermediates at 53 bits (never compute a chain in `float`) and use round-to-nearest — both SSE defaults, now measured. **THE BRIEFED TRIPLE WAS UNDER-POWERED: 0x027f is 53-bit (differs from 0x127f only in bit 12, infinity control, ignored since the 387) and 0x137f is 64-bit, not a rounding change** — run as written, all three come back identical and would have 'proved' something false. PC=bits 8-9, RC=bits 10-11. Setting PROVEN to hold: read-back at each force + 38 in-pipeline hook samples per run spanning turn phases 4/6/8, all at the forced value (`verify/results/fpu-cw/cw-census.txt`). `Mars::Application::Run` calls `_controlfp(0x50000,0x3070300)` at 0x0089f606 EVERY FRAME = 0x127f, so forcing at EndTurn is wiped before BeginProcessTurn; BeginProcessTurn is the point that works. TRAP: under 24-bit the CRT's own %g rendering degrades, so trace TEXT is not a comparison surface — use `verify/fpu-cw/trace_bitdiff.py`. findings/subsystems/fpu-precision-sensitivity.md |
|
||||
| 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 |
|
||||
| LAB RULE: no `git add -A` in sots-re while lanes run | meta | verified | high | 100% | 2026-09-08 | MY error, caught by lane M: an integrator `git add -A` in the SHARED `sots-re` clone swept a running lane's in-progress files into commit 9d385a7 mid-run (remainder landed in f5b37c2). Nothing was lost, but authorship and atomicity were. RULE: while any lane is live, the integrator stages sots-re by explicit PATH only (`git add campaign/board.md campaign/DASHBOARD.md`), never `-A`. Lanes own their own subtrees. sots-engine is unaffected - lanes work in per-lane worktrees there, which is exactly why that repo has not had this problem . HAPPENED AGAIN 2026-09-08 (lane V): lane D's commit d7ea0a0 swept lane V's in-flight `ghidra/addresses.json` edit (the ObservedTech LIVE CONFIRMATION prose) into it. No harm this time - the content was correct and is now on main - but it is the same failure mode a third time, and it means a lane can find its own work already committed under another lane's message. Check `git log -- <path>` before assuming your edit is still unstaged. |
|
||||
| MoveFleet waypoint types 2-5 | verify | backlog | — | 0% | 2026-09-08 | Still ZERO behavioural coverage after lane M. Not for lack of trying: the only mover in ref-turn2 is the AI (straight runs only), and the player that would travel a node line has DE/CR/DN all 00 at its home system, so Move/Manage Fleets are greyed out every turn - there is nothing to send along the node lines the map draws. Needs a ship built over several turns or a purpose-built save. The type-2 node-line step is still WRONG BY CONSTRUCTION (B4). Also: sim::Distance deliberately left in double (only stutter geometry uses it); Mars_Vec3_Length says it is probably 1 ULP out the same way, but there is zero behavioural evidence to correct it against - do not "fix" it blind |
|
||||
| P2-P event posting in ours | phase2 | verified | high | 95% | 2026-09-08 | HOST-VERIFIED, VM RUN QUEUED (lane F holds VM140). next_id reaches 4 in a host reproduction of recap-b3 call 0, fixture rebuilt from raw bytes at the real 0x1c/0x18/0x74 strides and cross-checked against turn3-state.sav with lane C's state_checksum --tree. Count-only (lane E option a): ours never calls the game's PostEvent and REPLACE MODE WRITES NOTHING - a bumped EvNxID with no record behind it would corrupt the very save the oracle hashes. Three design points: the event scan is taken in describe_args BEFORE the original (taken after, ours would dedup against the original's own posts and agree for the wrong reason); dedup risk is MEASURED and reported as events_dedup_risk, not assumed; KeylessEventText resolves keys to "%s" so the shim carries no prose. VERIFIED from the instruction stream: SetResearched 0x00581e10 calls owner vft+0x10 with (flags>>2)&1 and ProcessResearch passes flags=2, so silent=false and the completion event IS posted - previously only inferable from "EvNxID moved by two". ctest 33/33, shim cross-builds on CT111 (lane P could only syntax-check) | . **LIVE-VERIFIED AGAINST AN ADVANCE PREDICTION (lane V 2026-09-08, build `eventlive-dd38117-20260908T0916Z`, main dd38117 unchanged).** Lane P wrote the expected numbers into `docs/P-events-wiring.md` §4 BEFORE the run; every one held. First End Turn: **3 calls, 3 compared, 0 diverged, exit 0** (was 1 diverged) with `turn=3`, `events_turn_bucket_exists=true`, `events_next_id_in=3`, `events_in_turn_bucket=1`, `events_dedup_risk=0`, no `events_scan_truncated`, `next_id` 3->4 both sides, `turns`/`turns_bytes` 2/48 unchanged, node[144] 2879->5768 + flag 1->2, rng identical. Five End Turns: exit 1 with **2 divergent calls instead of 3**, each short by EXACTLY 1 (`next_id` orig 7 ours 6, orig 12 ours 11) = the unmodelled `EVENT_TECHS_UNLOCKED`, exactly as forecast - 0 divergences there would have been suspicious, not good. §4.3 conversion held too: `player+0x274/0x278/0x27c` left the guard's undeclared list (13 spans in 2 calls -> 10) and appear in the diff as `observed_techs.bytes`. End-Turn oracle byte-identical to lane R's. clean_room_check OK, ctest 33/33 (separate commands). Report `findings/subsystems/eventlive-verification.md`; engine `docs/V-eventlive.md`; traces `verify/traces/eventlive-b3-*`, reports `verify/results/compare/eventlive-b3-*`
|
||||
| EVENT_TECHS_UNLOCKED not posted (predicted residual) | verify | backlog | — | 0% | 2026-09-08 | Lane P FLAGGED RATHER THAN GUESSED. Trigger IS pinned (SetResearched's sweep sets state=2 + stamps turnAvailable sticky at -1; tail loop collects state==2 && turnAvailable==currentTurn) but evaluating it needs the unlock cascade ours deliberately does not run. The driver takes the unlock list as an INPUT and is handed nullptr ("no list") - deliberately distinct from an empty list ("computed, empty"). PREDICTED RESIDUAL: next_id short by exactly 1 on every completion call. Posting it "whenever something completed" would score on this save and be WRONG the first time a completion unlocks nothing - the exact false-pass shape this project keeps catching |
|
||||
| EVENT_TECHS_UNLOCKED / the unlock cascade | verify | verified | high | 100% | 2026-09-08 | Lane P FLAGGED RATHER THAN GUESSED. Trigger IS pinned (SetResearched's sweep sets state=2 + stamps turnAvailable sticky at -1; tail loop collects state==2 && turnAvailable==currentTurn) but evaluating it needs the unlock cascade ours deliberately does not run. The driver takes the unlock list as an INPUT and is handed nullptr ("no list") - deliberately distinct from an empty list ("computed, empty"). PREDICTED RESIDUAL: next_id short by exactly 1 on every completion call. Posting it "whenever something completed" would score on this save and be WRONG the first time a completion unlocks nothing - the exact false-pass shape this project keeps catching **CLOSED by lane U 2026-09-08 — by running the cascade, not by posting on completion.** `sots-engine src/game/sim/techgraph.{h,cpp}` implements `PrereqsMet` (0x0057d8e0, AND of ORs; zero groups = TRUE, an EMPTY group = FALSE), `SetResearched` (0x00581e10: stamps, child-cost sweep with a SIGNED min against an INT_MAX sentinel, sticky `turnAvailable`, zero-cost recursion) and the tail collector (0x00587cc3). Wired into the B3 hook in COMPARE MODE ONLY, over the scratch node copies. LIVE: **first End Turn 3/3/0 exit 0; five-turn 15/15/0 exit 0; Zuul 20/20/0 exit 0** — all 22 of lane V's divergent fields gone, `next_id` reaching 7 and 12, and the End-Turn oracle hashes UNCHANGED (`bb4fd9ac…` / `978041ac…`). The unlock list is still an INPUT and still `nullptr` when it could not be computed, so lane P's distinction survives. `findings/subsystems/unlock-cascade.md`; engine `docs/U-unlock.md` (§4 = the advance prediction, §5 = the outcome) |
|
||||
| sizeof(ObservedTech) unpinned | objects | verified | high | 100% | 2026-09-08 | **PINNED (lane X).** `sizeof(Game::ObservedTech) = 0x2c (44)` -- three independent proofs: the magic divide `0x2e8ba2e9 sar 3` (= /44, exact) at 0x0087239f, `imul reg,reg,0x2c` at 0x0087243a / 0x007b735b, and the search stride `add edi,0x2c` at 0x007ba257. **Append site = `RecordObservedTech+0xdf` (0x007ba27f): `lea ecx,[player+0x274]; call vector_ObservedTech_push_back 0x007b7320`** -- a de-duplicating append, direct callee of OnTechResearched 0x00891790; the realloc through 0x007b5820 is why all three vector words move. Element FULLY MAPPED (lane S, from ObservedTech::Write 0x00817cf0 / Read 0x00817c40): +0x00 vptr 0x00a2439c (RTTI `.?AVObservedTech@Game@@`), +0x04 uint16 `otnF`, +0x06 uint16 `otnL`, +0x08 **bool** `odet` (1 byte), +0x0c std::string `otch` (**0x1c**, so +0x24 is its _Alval, NOT a field), +0x28 int `owith` -- 0x2c exactly, nothing unaccounted. Same shape as Game::ObservedWeapon (Write 0x00817bc0, tag `owep`). Built the general tool the row asked for: `tools/x86disp.py`, an x86 displacement xref scanner (100% code coverage, 0.17% desync). `findings/subsystems/observedtech-append.md` | . **CONFIRMED LIVE (lane V 2026-09-08)**: on the running game the `observed_techs` Result region grew by **exactly 44 bytes** on each of the two tech-completion calls of the 5-End-Turn run (440->484, 484->528), and both non-researching players' vectors measured 880 = 20 x 44 and never moved. Behavioural confirmation of a purely static pin
|
||||
| lea-displacement xref scanner | meta | verified | high | 100% | 2026-09-08 | `tools/x86disp.py` -- fixes the systemic blind spot that Ghidra does not index ModRM displacements. Full x86-32 length decoder swept from Ghidra's 41,089 function starts: 2,174,504 instructions, 612,166 displacement sites, **100.0% code coverage, 70 desyncs (0.17%), zero unknown opcodes**. Validated against ground truth before use (re-finds `lea eax,[ecx+0x29c]` in GetEventStorage, both OnTechResearched +0x29c sites, and one NEW ProcessTurn site). HONEST LIMITS: it is a **recall** tool, not an oracle -- class-level precision at 0x274 is ~13% by function (99 sites / 45 functions, ~6 real), i.e. a 900x search-space cut that still needs one call-graph check. The naive byte scan it replaces is not wrong so much as **blind**: it misses 80/99 real sites at 0x274 and 13,784/14,611 at disp8 0x14. `cohort` ranking must never be used as a hard filter -- it would have discarded the correct ObservedTech answer. Works off a gitignored local cache in `dumps/`, so it does not hammer CT111 |
|
||||
| lea-displacement xref scanner | meta | verified | high | 100% | 2026-09-08 | `tools/x86disp.py` - full x86-32 length decoder swept from 41,089 Ghidra function starts: 2,174,504 instructions, 612,166 disp sites, 0 unknown opcodes, 100.0% code coverage, 0.17% desyncs. VALIDATED against ground truth before any new claim (rediscovers GetEventStorage's lea ecx+0x29c, EvNxID +0x2b0; positive control: given 50 known ServerPlayer offsets, FUN_0087fac0 scores 50/50 = the serializer, nothing close). BUILD GOTCHA: clipping sweeps at fva+Ghidra sizeInBytes lost 11% of functions to mid-instruction truncation; sweeping to the NEXT function start took coverage 89% -> 100%. HONEST LIMIT: the win is RECALL not precision - naive lea-only scan MISSES 80 of 99 real 0x274 sites; class-level precision ~13% by function. Value = search space 41,411 -> 45 (~900x), then disambiguate by call graph |
|
||||
|
|
@ -107,7 +107,7 @@ Status flow: `backlog → in-progress → mapped → verified` (or `blocked`).
|
|||
| addresses.json fragment dir (structural fix) | meta | verified | high | 100% | 2026-09-08 | Three cross-lane sweeps today all traced to ONE shared file. `ghidra/addresses.d/<lane>.json` fragments are now merged by gen_addresses.py after addresses.json, in sorted order; a DUPLICATE NAME ACROSS FILES IS A HARD ERROR (exit 1), never last-wins, because two lanes disagreeing about an address is precisely what must not be papered over. Self-tested both ways (duplicate exit=1, clean exit=0). Integrator folds fragments back into addresses.json once a lane merges. This replaces the "stage by path" rule with a design that does not depend on remembering it |
|
||||
| P2-P event posting LIVE-VERIFIED | phase2 | verified | high | 95% | 2026-09-08 | ADVANCE PREDICTION HELD FIELD FOR FIELD. Lane P wrote the expected result into docs/P-events-wiring.md 4 BEFORE the run; lane V tested it. First End Turn: 3 calls, 3 compared, 0 divergent, tracecmp exit 0 - turn=3, bucket_exists=true, next_id_in=3, in_turn_bucket=1, dedup_risk=0, no scan_truncated, next_id 3->4 both sides, node[144] and rng as forecast, observed_techs.bytes unchanged on all three. Five-turn: exit 1, 2 divergent calls (was 3), each short by EXACTLY 1 (orig 7/ours 6, orig 12/ours 11) = the deliberately unmodelled EVENT_TECHS_UNLOCKED. player+0x274/0x278/0x27c LEFT the guards' undeclared list (13 spans -> 10) and now show as `observed_techs`. STRENGTHENED BY LUCK RUNNING OUT: this was NOT lane R's run - from turn 4 the AI picked different techs - and the predicted id totals landed anyway. End-Turn oracle matched lane R's hashes byte for byte |
|
||||
| sizeof(ObservedTech)=44 CONFIRMED LIVE | objects | verified | high | 100% | 2026-09-08 | observed_techs.bytes grew by EXACTLY 44 on both completion calls (440->484, 484->528); non-researching players measured 880 = 20 x 44 and never moved. Independent BEHAVIOURAL confirmation of a purely static pin (lane X's three proofs + lane D's magic-divide inversion). Static and dynamic now agree on this struct from four directions |
|
||||
| CORRECTION: lane R's "RNG matched 15/15" was workload luck | verify | verified | high | 100% | 2026-09-08 | Lane V found rng diverges on call 9 (orig left 374/next_index 250, ours 375/249) = the RollResearchEvent draw in OnTechResearched, a boundary B3 and P-events-wiring 3 both declared out of scope. HONEST STATEMENT: ProcessResearch's rng matches on every call that does NOT complete a roll-triggering tech, and is short by one draw on every call that DOES. Lane R's 15/15 was a property of that workload, not of the model - exactly the kind of claim that survives only until the workload changes. The two "new" guard spans (player+0x196, player+0x3b4) are already-named fields (design-mask B, ResErrRoll) seen from the caller |
|
||||
| CORRECTION: lane R's "RNG matched 15/15" was workload luck | verify | verified | high | 100% | 2026-09-08 | Lane V found rng diverges on call 9 (orig left 374/next_index 250, ours 375/249) = the RollResearchEvent draw in OnTechResearched, a boundary B3 and P-events-wiring 3 both declared out of scope. HONEST STATEMENT: ProcessResearch's rng matches on every call that does NOT complete a roll-triggering tech, and is short by one draw on every call that DOES. Lane R's 15/15 was a property of that workload, not of the model - exactly the kind of claim that survives only until the workload changes. The two "new" guard spans (player+0x196, player+0x3b4) are already-named fields (design-mask B, ResErrRoll) seen from the caller **EXPLAINED by lane U 2026-09-08, and it is stronger than "workload luck".** The draw is now MODELLED (`ServerPlayer::OnTechResearched` head: `if (ResT == def) { if (ResearchRollPending) RollResearchEvent(); pending=0; ResT=0; }`, one unconditional NextFloat), its two inputs are read PRE-CALL and reported in every record (`research_target`, `roll_pending_in`), and `region:rng` compared clean on all 35 of lane U's calls. BUT `roll_draws` was **0 on every one of them**: `ResearchRollPending` is normally consumed by `ServerPlayer::ProcessTurn` BEFORE ProcessResearch runs, because that call site fires once the progress ratio crosses its threshold - i.e. exactly the turns approaching completion. In lane U's Zuul run `roll_pending_in` is true for turns 8-12 and flips FALSE on turn 13, the turn before the tech completes on turn 14. So lane V's call-9 draw was the RARE case (a tech jumping from below the threshold to complete in one turn). Three sessions, three answers: 0 / 1 / 0. **The branch is inside the compare but has never been seen to fire** - needs a purpose-built save |
|
||||
| Zuul double roll (behavioural) | verify | verified | high | 100% | 2026-09-08 | CLOSED by lane V. No species-5 save existed so it MADE one: custom game, only Zuul in the Available Species pool, 4 End Turns. 8 calls, 8 compared, 0 divergent, exit 0; all four species=5 researching calls advance the generator by TWO (left 540->538, 522->520, 504->502, 485->483) and ours reproduced every post-state bit-for-bit. Was disassembly-only since 2026-09-08 morning. Save: verify/results/saves/zuul-turn5-species5.sav (and zuul-turn5.sav on the VM). Does not yet contain a Zuul COMPLETION - one more End Turn gets there |
|
||||
| VM click helper: `type` does not register | meta | verified | high | 100% | 2026-09-08 | The click helper's `type` action does not reach the game's text fields. WORKAROUND: accept the default name and rename the .sav afterwards. Costs a save-naming step in every workload-building lane |
|
||||
| wire-schema channel (engine) | engine | verified | high | 95% | 2026-09-08 | Lane G REJECTED the brief's premise for good reason. objects/layouts.json is a MEMORY-layout projection and was the wrong input: serializers.py's build() sorts fields by off_abs (89 of 386 classes have offset order != WRITE order) and merges duplicate offsets into alt_tags - which is exactly the JewelsOfTheCrown double-tag trap. Lab.layout() already computed true disk order internally and it was being thrown away. New `tools/streams.py` is a SECOND projection keeping order and repeats and DROPPING EVERY MEMORY FACT (no off/size/sizeof/gaps/strides) - so the original's ABI never enters our runtime types, which was the design constraint. Offsets still have their home as `offset` entries in addresses.json for the shim, which legitimately needs them. gen_stream_schema.py -> include/generated/sots_stream_schema.h (386 classes, 2,042 items). SUBTLETY: the on-disk primitive is NOT layouts.json's `kind` - it comes from the stream vftable slot/helper, and a member held as int16/int8 is written by WriteInt and is FOUR BYTES ON THE WIRE |
|
||||
|
|
@ -115,3 +115,7 @@ Status flow: `backlog → in-progress → mapped → verified` (or `blocked`).
|
|||
| NAMED coverage 38% -> 97% | engine | verified | high | 100% | 2026-09-08 | All four real saves round-tripped byte-identically BEFORE and AFTER - and lane G refused to call that a coverage claim, because `ar.any` bodies round-trip trivially by copying bytes nobody understands. New CoverageArchive separates items a FIELD NAMES from items a Node merely CARRIES: turn1/2/3 37.9/38.8/39.4% -> 97.1/97.2/97.2%; zuul-turn5 42.5% -> 97.6%. Ratchet at 95%. Newly typed: TechTree (both NumTechs sections), Events (3 nesting levels), ShipRecs, sprjs, civr, comms, spy2, spymgr, aid, Ojvs, AIEnf, FNG, trdmgr, Des section/gun-bank tree. STILL OPAQUE, honestly: CD custom data (744 items - TurnCommands_v5 is a NO-ORDERS snapshot, needs a save with issued orders), SvSctOb (147, eight EncObj variants), DOpts (94, read_elem lacks a std::string branch), spies2 (56, count 0 everywhere), RNG (2, correctly opaque) |
|
||||
| FOUR reader defects invisible to round-trip | verify | verified | high | 100% | 2026-09-08 | Present in BOTH readers, none catchable by a round-trip test. (1) SystemParams field 1 is a STRING, not an int - it is the empty string in every save, four zero bytes, byte-identical to int 0; it round-tripped BY LUCK and a named planet would have desynced both parsers. (2) ObservedTech/ObservedWeapon `odet` is a BOOL not an int (lane D's own golden table already said so); byte-safe only because a 4-char tag makes bool and int items both 12 bytes. (3) SpeciesRatios::nv and (4) ShipRecords::srbd are COUNTS, not fields. Lane G deliberately did NOT patch save_reader.py: every fix is byte-neutral on available saves, and quietly editing the oracle mid-campaign is worse than recording the divergence. THE ENGINE IS NOW THE CORRECTED REFERENCE; the Python oracle carries a logged open item |
|
||||
| RULE: interface stub -> look for the *Impl | objects | verified | high | 100% | 2026-09-08 | `trdmgr` RESOLVED, correcting the earlier "ServerTradeManager has no serializer" finding: the no-op Read/Write is real but THE CALL IS VIRTUAL - ServerTradeManagerImpl has the actual serializer. Same shape resolves IServerSpyManager -> ServerSpyManager. GENERAL RULE: when an interface's serializer is the inherited stub, look for the concrete *Impl. (Game::ShipDesign::Write genuinely still makes no stream call - but ShipDesignDef::Section IS recovered, so most of Des is typeable anyway) |
|
||||
| B3 hook: the completion path is now inside the compare | phase2 | verified | high | 95% | 2026-09-08 | NEW (lane U 2026-09-08). `Game::TechTree::ProcessResearch` in compare mode now reproduces not only what the function itself writes but the whole `SetResearched` completion path: the turn/order stamps, the child-cost sweep, the availability sweep, the newly-available collector that decides EVENT_TECHS_UNLOCKED, the de-duplicating ObservedTech append and the one RNG word RollResearchEvent draws. **35 compared calls across three workloads, 0 divergences, tracecmp exit 0 on all three.** FOUR pre-call reads make it work and each is a trap that reads back a PLAUSIBLE wrong answer if taken after the original: TechTree+0x20 (order counter, post-incremented -> every `order` off by one), ServerPlayer+0x294 (`ResT`, zeroed by the callback -> the extra RNG draw never modelled), +0x3b4 (pending roll, cleared in the same block), and the otch element names (already appended -> the dedup check 'agrees' with a count it never computed). All four are reported as ARGUMENTS so a run is auditable without trusting `ours`. COMPARE MODE ONLY: in replace mode applying half of OnTechResearched (the append and the roll, but not the ~90 tech-effect field writes) would leave the player in a state no code path produces |
|
||||
| CLEAN-RESULT DISCIPLINE: how a 0-divergence run was kept honest | meta | verified | high | 100% | 2026-09-08 | NEW (lane U). A clean result was EXPECTED here, which is exactly when a hook that silently models nothing slips through. Three things made that hard to hide and all three fired: (1) the 'did nothing' answer is KNOWN - it is `INT_MAX / 0 / -1`, precisely what lane V's report shows - so there is no null model that passes; (2) the collector ran on all 35 calls, not just the 4 completions, and had to come back EMPTY on the 31 quiet ones - an over-collecting transcription would have pushed `next_id` TOO HIGH and made those calls newly divergent; (3) the shim log prints per-call counters (`completions= unlocked= otch_appends= roll_draws= failures= depth= name_unreadable=`), so a clean compare with zeros on a completion call would have been visible as a clean compare of nothing. Reusable pattern for any lane whose expected outcome is 'no divergence' |
|
||||
| Prereq semantics come from the CODE, not the tech files | subsystem | verified | high | 100% | 2026-09-08 | NEW (lane U). `TechTree::PrereqsMet` 0x0057d8e0 (whole function): a prerequisite set is an **AND over groups, each group an OR over techs**, held as a flat entry array at `TechDef+0x88` (stride 8, `TechDef*` at +0) plus a vector of `{int start; int count}` groups at `TechDef+0x98/+0x9c` (stride 8). A tech satisfies its group only when its node exists IN THIS TREE and is state 4. TWO EDGE CASES THE DATA FILES DO NOT SUGGEST: **zero groups -> TRUE** (a tech with no `requires` is gated only by its parent edge), and **a group with zero entries -> FALSE, failing the whole test** (the inner loop cannot break, so the outer one exits with that group uncounted) - a 'vacuously true empty OR' reading gets this exactly backwards. Also `TechDef+0xb0`: a byte that excludes a node from the availability sweep entirely; named `TechDef_off_NoAutoAvailable` for what it DOES - the tech-file keyword `unlock_explicitly` matches the behaviour but ParseTech 0x0058b050 shows no reference to 0xb0, so the link is a HYPOTHESIS. `findings/subsystems/unlock-cascade.md` |
|
||||
| per-lane addresses.d fragment (second use) | meta | verified | high | 100% | 2026-09-08 | Lane U wrote `ghidra/addresses.d/lane-u.json` (12 entries; header 615 -> 627) rather than touching the shared `addresses.json`, and staged every sots-re change by explicit path. No sweep, no lost authorship. Duplicate-name detection did its job: `TechDef_off_Name` had to be checked against the shared file before being added |
|
||||
|
|
|
|||
|
|
@ -150,3 +150,27 @@ What is **not** known, and was looked for:
|
|||
region reports the vector's byte span, and one completion appends one element, so the delta on a
|
||||
completion call names `sizeof(ObservedTech)` directly. See `sots-engine docs/P-events-wiring.md`
|
||||
§4.4.
|
||||
|
||||
---
|
||||
|
||||
## 6. Continued by lane U (2026-09-08) — `findings/subsystems/unlock-cascade.md`
|
||||
|
||||
This note stopped at the two functions the sweeps *call*. Lane U read them and implemented the
|
||||
cascade, closing the `EVENT_TECHS_UNLOCKED` residual this note predicted:
|
||||
|
||||
* **`PrereqsMet` (0x0057d8e0)** is an AND over groups, each group an OR over techs, held at
|
||||
`TechDef+0x88` (flat entries, stride 8) and `TechDef+0x98/+0x9c` (`{start, count}` groups,
|
||||
stride 8). Zero groups is TRUE; a group with **zero entries is FALSE and fails the whole test**.
|
||||
* **`def+0xb0`**, the byte §4 left unresolved, is named `TechDef_off_NoAutoAvailable` for what it
|
||||
does. Its write site is still not read; the `unlock_explicitly` tech-file keyword is a
|
||||
hypothesis, not a fact.
|
||||
* The **tail collector** (0x00587cc3) runs once, after the per-node loop *and* after the decay
|
||||
sweep, gated on `tree->owner != 0`; the state test is on the self-resolved node, the turn test
|
||||
on the iterated one.
|
||||
* **`OnTechResearched`'s head**: `RecordObservedTech` is the FIRST statement and unconditional;
|
||||
the research-event roll is `if (ResT == def) { if (ResearchRollPending) RollResearchEvent();
|
||||
pending = 0; ResT = 0; }`.
|
||||
|
||||
Live result: the cascade running inside `ours` gives **0 divergences on 35 compared calls across
|
||||
three workloads**, `tracecmp` exit 0, End-Turn oracle hashes unchanged. §5 of the lane U note has
|
||||
the numbers; `sots-engine docs/U-unlock.md` §4 is the advance prediction and §5 the outcome.
|
||||
|
|
|
|||
226
findings/subsystems/unlock-cascade.md
Normal file
226
findings/subsystems/unlock-cascade.md
Normal file
|
|
@ -0,0 +1,226 @@
|
|||
# The tech unlock cascade — the code, and the live verification (lane U, 2026-09-08)
|
||||
|
||||
Lane P read `TechTree::SetResearched` (0x00581e10) and wrote
|
||||
`findings/subsystems/setresearched-cascade.md`, which settled the `silent` flag and sketched both
|
||||
sweeps. It stopped short of the two functions the sweeps *call*, and it deliberately did not post
|
||||
`EVENT_TECHS_UNLOCKED` — it handed the pass driver a `nullptr` unlock list and predicted a
|
||||
residual of exactly 1 on `next_id` per completion. Lane V measured that residual live, twice,
|
||||
exactly.
|
||||
|
||||
This note (a) finishes the instruction-level read — `PrereqsMet`, the prerequisite structure, the
|
||||
tail collector, and the head of `OnTechResearched` — and (b) records the live verification of the
|
||||
whole thing running inside `ours`.
|
||||
|
||||
**Result: the residual is gone. 0 divergences on all three workloads, `tracecmp` exit 0, and the
|
||||
End-Turn oracle hashes unchanged.** Engine side: `sots-engine docs/U-unlock.md`,
|
||||
`src/game/sim/techgraph.{h,cpp}`.
|
||||
|
||||
---
|
||||
|
||||
## 1. `TechTree::PrereqsMet` — 0x0057d8e0
|
||||
|
||||
`bool __thiscall PrereqsMet(TechTree* this, TechPrereqs* p /* = def + 0x88 */)`, 148 bytes,
|
||||
whole function read. Both `SetResearched` call sites pass `def + 0x88`.
|
||||
|
||||
```c
|
||||
satisfied = 0;
|
||||
total = (p->groups._Mylast - p->groups._Myfirst) >> 3; // p+0x14, p+0x10, stride 8
|
||||
for (g = p->groups._Myfirst; satisfied < total; g += 2) {
|
||||
i = g[0]; // start index into the flat entry array
|
||||
end = g[1] + i; // + count
|
||||
if (i < end) {
|
||||
e = (int*)(p->entries + i * 8); // p+0x00, stride 8
|
||||
do {
|
||||
if (e[0] != NULL &&
|
||||
(n = this->nodes[ ((int*)e[0])[0] ]) != NULL &&
|
||||
n->state == 4) break; // this group is satisfied
|
||||
i++; e += 2;
|
||||
} while (i < end);
|
||||
}
|
||||
if (i == end) break; // group NOT satisfied -> leave it uncounted
|
||||
satisfied++;
|
||||
}
|
||||
return satisfied == total;
|
||||
```
|
||||
|
||||
So a prerequisite set is **an AND over groups, each group an OR over techs**, and a tech counts
|
||||
only when its node exists in *this* tree and is in state 4.
|
||||
|
||||
Two edge cases are the code's, not a simplification, and both are easy to get backwards:
|
||||
|
||||
* **Zero groups → true.** `0 == 0`. A tech with no `requires` line is gated only by its parent
|
||||
edge.
|
||||
* **A group with zero entries → false, and the whole test fails.** The inner loop cannot run, so
|
||||
`i == end` immediately and the outer loop breaks with that group uncounted. A "vacuously true"
|
||||
reading of an empty OR gets this exactly wrong.
|
||||
|
||||
### The structure at `TechDef + 0x88`
|
||||
|
||||
Two MSVC vectors back to back:
|
||||
|
||||
| offset (from `def`) | what |
|
||||
|---|---|
|
||||
| `+0x88` | `vector<TechPrereqEntry>` — only its `_Myfirst` is read; the groups carry the bounds |
|
||||
| `+0x98` / `+0x9c` | `vector<TechPrereqGroup>` `_Myfirst` / `_Mylast` |
|
||||
|
||||
`TechPrereqEntry` is 8 bytes, `TechDef*` at +0x00 (the second word is never read here).
|
||||
`TechPrereqGroup` is 8 bytes, `{int start; int count}` indexing the entry array.
|
||||
|
||||
## 2. The tail collector — 0x00587cc3, inside `ProcessResearch`
|
||||
|
||||
Runs **once**, after the per-node allocation loop *and* after the decay sweep, and only when
|
||||
`tree->owner != 0`:
|
||||
|
||||
```c
|
||||
turn = ModCount;
|
||||
for (i = 0; i < nodes.size(); i++) {
|
||||
n = nodes[i];
|
||||
if (n && n->def && (p = nodes[ n->def->techId ]) != NULL &&
|
||||
p->state == 2 && n->turnAvailable == turn) collect(n);
|
||||
}
|
||||
if (!collected.empty()) PostEvent(EVENT_TECHS_UNLOCKED, ...);
|
||||
```
|
||||
|
||||
Note the asymmetry: the **state** test is on the self-resolved node `p`, the **turn** test on the
|
||||
iterated node `n`. This confirms lane E's read in `events.md` §3.4 and adds the `owner` gate and
|
||||
the "after the decay sweep" ordering.
|
||||
|
||||
## 3. The head of `ServerPlayer::OnTechResearched` — 0x00891790
|
||||
|
||||
The two statements before the `!silent` event post, and the only two parts of the callback the B3
|
||||
hook's regions can see:
|
||||
|
||||
```c
|
||||
RecordObservedTech(...); // FIRST statement, UNCONDITIONAL
|
||||
if (this->ResT /*+0x294*/ == def) {
|
||||
if (this->ResearchRollPending /*+0x3b4*/) RollResearchEvent(this); // exactly one NextFloat
|
||||
this->ResearchRollPending = 0;
|
||||
this->ResT = 0;
|
||||
}
|
||||
```
|
||||
|
||||
* `RecordObservedTech` (0x007ba1a0, lane X) de-duplicates by tech name, so "the vector did not
|
||||
grow" is a real outcome. Its unconditionality was not previously written down.
|
||||
* `RollResearchEvent` (0x0088df20) is
|
||||
`odds = ResearchEventOdds(this, this->ResT); roll = rand01(); if (roll < odds) FUN_00889d60(this);`
|
||||
— **one draw, unconditional**, and the branch behind it is normally dead (odds are 0 outside the
|
||||
plague and AI-rebellion families). Clearing `ResT` is what makes a *second* completion in the
|
||||
same pass draw nothing.
|
||||
|
||||
## 4. `TechDef + 0xb0` — named, not explained
|
||||
|
||||
The byte that makes the availability sweep `continue`. A node carrying it can still be completed
|
||||
by an explicit `SetResearched`, and sweep 1 still lowers its cost and raises its state — but
|
||||
nothing ever moves it to state 2, so it never stamps `turnAvailable` and can never raise
|
||||
`EVENT_TECHS_UNLOCKED`.
|
||||
|
||||
`addresses.d/lane-u.json` names it **`TechDef_off_NoAutoAvailable`** for what it does. The
|
||||
tech-file keyword `unlock_explicitly` (parsed by `sots-engine src/game/data/techtree.cpp:152`)
|
||||
matches the behaviour exactly and is the obvious candidate, but `MasterTechTree::ParseTech`
|
||||
(0x0058b050) shows no reference to 0xb0 in its decompilation, so **the link is a hypothesis, not a
|
||||
fact**. Nothing depends on it: the byte is read from the live def either way.
|
||||
|
||||
---
|
||||
|
||||
## 5. Live verification
|
||||
|
||||
Build `unlock-405ba41-20260908T1026Z`, cross-built on CT111, staged `C:\SOTS\shimdist-u`, recipe
|
||||
`shim.cfg.recapb3` unchanged. The prediction was written into `sots-engine docs/U-unlock.md` §4
|
||||
**before** the build was staged; §5 there is the field-by-field comparison.
|
||||
|
||||
| run | calls | compared | diverged | exit |
|
||||
|---|---|---|---|---|
|
||||
| first End Turn, `ref-turn2` | 3 | 3 | **0** | 0 |
|
||||
| five-turn continuation, turn 2 → 7 | 15 | 15 | **0** | 0 |
|
||||
| Zuul, `zuul-turn5`, turn 5 → 15 | 20 | 20 | **0** | 0 |
|
||||
|
||||
Reports `verify/results/compare/unlock-b3-{t1,t1-5,zuul}.{md,json}`; traces
|
||||
`verify/traces/unlock-b3-*`; shim log `verify/results/shim/unlock-shim.log`.
|
||||
|
||||
**The End-Turn oracle held.** `(Autosave EndTurn).sav` = `bb4fd9ac89f41e3b…`, `(Autosave).sav` =
|
||||
`978041acd168b56e…` — the same two hashes lane R and lane V recorded. Checked first, because a
|
||||
clean compare from a build that moved the game would be worthless.
|
||||
|
||||
### 5.1 What the five-turn run actually did
|
||||
|
||||
All 22 divergent fields lane V recorded are gone. Call 3 reproduced lane V's numbers exactly
|
||||
(node 144 completes with `order` 22 / `turn_researched` 4; nodes 132/136/142 go 0 → 2 with
|
||||
`cost_rp` 10000/16000/8000 and `turn_available` 4; `next_id` 5 → 7; `observed_techs` 440 → 484).
|
||||
|
||||
**Call 9 was a different completion from lane V's**, and that is the stronger evidence. From turn 5
|
||||
the AI picked a different target — lane R's documented trap #2. Lane V's call 9 completed tech 142
|
||||
and unlocked one node; this run completed **tech 9** (`order` 23, `turn_researched` 6) and unlocked
|
||||
**three**: node 3 at 13000, node 12 at 35000, node 18 at 4000, all `turn_available` 6. Those three
|
||||
costs appear in no earlier report and were predicted by no one. The model reproduced them with
|
||||
zero divergences on a case it had never seen — so it cannot be scoring by having memorised lane V's
|
||||
run. Call 12 then allocates to node 18, the tech the cascade had just unlocked.
|
||||
|
||||
### 5.2 The check against a compare that compares nothing
|
||||
|
||||
A clean result was *expected* here, which is exactly when a hook that silently models nothing
|
||||
slips through. Three things make that hard to hide, and all three fired:
|
||||
|
||||
1. The expected values are non-trivial and the "did nothing" answer is known: it is
|
||||
`INT_MAX / 0 / −1`, which is precisely what lane V's report shows. There is no null model that
|
||||
passes.
|
||||
2. The collector ran on all 35 calls, not just the four completions. On the 31 quiet calls it had
|
||||
to come back **empty**; an over-collecting transcription would have pushed `next_id` *too high*
|
||||
and made those calls newly divergent. It did not.
|
||||
3. The shim log prints per-call counters. `completions=1 unlocked=3 otch_appends=1` on the
|
||||
completion calls and all-zero elsewhere — a clean compare with zeros on a completion call would
|
||||
have been visible as a clean compare of nothing.
|
||||
|
||||
### 5.3 The Zuul completion — double roll and cascade together
|
||||
|
||||
Lane V's `zuul-turn5.sav` was one End Turn short of a completion; this run took ten.
|
||||
**20 calls, 0 divergences, two Zuul completions.** Call 2 (turn 7, species 5, alloc {144, 1376}):
|
||||
the generator advances by **two** (`left` 449 → 447, `next_index` 175 → 177 — the species-5 double
|
||||
roll) *and* the completion cascade runs, in the same call, and `ours` reproduces the post-state bit
|
||||
for bit. The Zuul tree unlocks only 132 and 136 from tech 144 where the Human tree also unlocks
|
||||
142, so this is an independent instance of the cascade rather than a repeat.
|
||||
|
||||
### 5.4 The `RollResearchEvent` draw — implemented, inside the compare, NOT exercised
|
||||
|
||||
`roll_draws` was **0 on all 35 compared calls**. The reason is a real finding, visible in the
|
||||
trace: `ResearchRollPending` is normally consumed by `ServerPlayer::ProcessTurn` *before*
|
||||
`ProcessResearch` runs, because that call site fires when the progress ratio crosses a threshold —
|
||||
which is exactly the turns approaching completion. In the Zuul run `roll_pending_in` is `true` on
|
||||
the funded call for turns 8–12 and flips to **false** on turn 13, the turn before the tech
|
||||
completes on turn 14.
|
||||
|
||||
So lane V's call-9 extra draw was the *rare* case (a tech that jumped from below the threshold to
|
||||
complete in one turn), not the normal one — which also explains lane R's "RNG matched 15 of 15".
|
||||
Three sessions, three answers: 0, 1, 0.
|
||||
|
||||
What is established: the draw is modelled at the right point in the stream, its two inputs are read
|
||||
**pre-call** and reported in every record (`research_target`, `roll_pending_in`), and `region:rng`
|
||||
compared clean on all 35 calls, so `ours` is not drawing a word the original does not. What is
|
||||
**not** established: that the branch has been seen to fire. The boundary is inside the compare; the
|
||||
compare has not yet had the chance to test it. It needs a save where a funded tech is below the
|
||||
ProcessTurn threshold and completes in one turn.
|
||||
|
||||
### 5.5 Guards
|
||||
|
||||
Undeclared writes: **9 in 2 calls** (five-turn), **8 in 2 calls** (Zuul). The span list differs
|
||||
from lane V's by the workload, not the code: `player+0x3b4` is gone because the pending-roll byte
|
||||
was already 0 when the completing call ran, and `+0x196` (design-option mask B) is replaced by
|
||||
`+0x130` (`PopMod`) because a different tech completed. Both are `OnTechResearched` tech-effect
|
||||
writes, both declared unmodelled. `tree_header+0x20` is still undeclared and still expected:
|
||||
`ours` seeds the order counter pre-call and advances its own copy; it does not model the live word.
|
||||
|
||||
Coverage verdict `partial`, 8 unmodelled notes (was 6).
|
||||
|
||||
---
|
||||
|
||||
## 6. Still owed
|
||||
|
||||
* A workload that fires the `RollResearchEvent` draw (§5.4).
|
||||
* `TechTree::GetProgressRatio` (0x0057e950) — the COMPLETE/UNDERBUDGET split remains analogy. It
|
||||
is count-neutral, so no compare can see it.
|
||||
* `def+0xb0`'s write site (§4).
|
||||
* `FUN_00889d60`, the branch behind the research-event roll; the temperance sweep;
|
||||
`EventStorage::PruneOldTurns`; replace mode on this hook. All untouched.
|
||||
* The `ObservedTech` element's own fields — `ours` decides the append, it does not build the
|
||||
element.
|
||||
* `FUN_00585ef0`, the refresh helper `SetResearched` runs when `flags & 8`. No research-path call
|
||||
site sets that bit, so it is unmodelled by call-site, not by omission.
|
||||
100
ghidra/addresses.d/lane-u.json
Normal file
100
ghidra/addresses.d/lane-u.json
Normal file
|
|
@ -0,0 +1,100 @@
|
|||
{
|
||||
"entries": [
|
||||
{
|
||||
"name": "TechTree_PrereqsMet",
|
||||
"addr": "0x0057d8e0",
|
||||
"convention": "thiscall",
|
||||
"prototype": "bool (TechTree* this, TechPrereqs* prereqs /* = TechDef + 0x88 */) // RET 4. An AND over groups, each group an OR over techs: a group is satisfied by any listed tech whose node exists in this->nodes AND whose state (+0x14) is 4. Zero groups -> TRUE (the function returns satisfied==total with both 0); a group with ZERO entries -> FALSE and the whole test fails, because the inner loop cannot break and the outer one then exits with that group uncounted. Reads only. Called from SetResearched twice: the unforced completion gate on the argument def, and the availability sweep on each node's self-resolved def",
|
||||
"status": "verified",
|
||||
"source": "findings/subsystems/unlock-cascade.md (lane U 2026-09-08, get-decompilation 0x0057d8e0, whole function 148 B / 36 lines)"
|
||||
},
|
||||
{
|
||||
"name": "TechDef_off_Prereqs",
|
||||
"offset": "0x88",
|
||||
"convention": "field",
|
||||
"prototype": "TechPrereqs prereqs -- the block TechTree::PrereqsMet is called on. Two MSVC vectors back to back: the flat entry array at +0x00 and the group array at +0x10. SetResearched passes `def + 0x88` at both call sites",
|
||||
"status": "verified",
|
||||
"source": "findings/subsystems/unlock-cascade.md (lane U 2026-09-08, 0x00581e10 + 0x0057d8e0)"
|
||||
},
|
||||
{
|
||||
"name": "TechPrereqs_off_Entries",
|
||||
"offset": "0x0",
|
||||
"convention": "field",
|
||||
"prototype": "std::vector<TechPrereqEntry> at TechPrereqs+0x00; only its _Myfirst is read (`*param_2`), because the groups carry the bounds. Element stride 8, the entry's TechDef* at +0x00; the second word is never read by PrereqsMet",
|
||||
"status": "verified",
|
||||
"source": "findings/subsystems/unlock-cascade.md (lane U 2026-09-08, 0x0057d8e0: piVar3 = (int*)(*param_2 + iVar5*8), piVar3 += 2 per step)"
|
||||
},
|
||||
{
|
||||
"name": "TechPrereqs_off_Groups",
|
||||
"offset": "0x10",
|
||||
"convention": "field",
|
||||
"prototype": "std::vector<TechPrereqGroup> at TechPrereqs+0x10 (_Myfirst +0x10, _Mylast +0x14). Group count = (last - first) >> 3. Each group is {int start; int count} indexing the entry array: the OR-set is entries[start .. start+count)",
|
||||
"status": "verified",
|
||||
"source": "findings/subsystems/unlock-cascade.md (lane U 2026-09-08, 0x0057d8e0: iVar2 = param_2[5] - param_2[4] >> 3; iVar6 = piVar4[1] + iVar5)"
|
||||
},
|
||||
{
|
||||
"name": "TechPrereqs_entry_stride",
|
||||
"offset": "0x8",
|
||||
"convention": "field",
|
||||
"prototype": "sizeof(TechPrereqEntry) -- the flat prerequisite entry, {TechDef* def; int unread}",
|
||||
"status": "verified",
|
||||
"source": "findings/subsystems/unlock-cascade.md (lane U 2026-09-08, 0x0057d8e0)"
|
||||
},
|
||||
{
|
||||
"name": "TechPrereqs_group_stride",
|
||||
"offset": "0x8",
|
||||
"convention": "field",
|
||||
"prototype": "sizeof(TechPrereqGroup) -- {int start; int count} into the entry array",
|
||||
"status": "verified",
|
||||
"source": "findings/subsystems/unlock-cascade.md (lane U 2026-09-08, 0x0057d8e0)"
|
||||
},
|
||||
{
|
||||
"name": "TechDef_off_NoAutoAvailable",
|
||||
"offset": "0xb0",
|
||||
"convention": "field",
|
||||
"prototype": "BYTE. Non-zero excludes the node from SetResearched's availability sweep entirely (`if ((char)def[0x2c] != 0) continue`, i.e. def+0xb0) -- it can still be completed by an explicit SetResearched and its cost/state are still lowered by the parent-edge sweep, but nothing ever moves it to state 2 and it never stamps turnAvailable, so it can never raise EVENT_TECHS_UNLOCKED. THE WRITE SITE WAS NOT READ: the name records what the byte does, not where it comes from. The tech-file keyword `unlock_explicitly` is the obvious candidate and matches the behaviour exactly, but MasterTechTree::ParseTech 0x0058b050 shows no reference to 0xb0 in its decompilation, so the link is a hypothesis and not a fact",
|
||||
"status": "verified",
|
||||
"source": "findings/subsystems/unlock-cascade.md (lane U 2026-09-08, 0x00581e10 line 67)"
|
||||
},
|
||||
{
|
||||
"name": "TechDef_off_Name",
|
||||
"offset": "0x40",
|
||||
"convention": "field",
|
||||
"prototype": "std::string name (0x1c bytes, _Mysize at +0x50, _Myres at +0x54: >= 0x10 selects the heap pointer). The substitution for every research event's %s, and the key RecordObservedTech de-duplicates the observed-tech vector on",
|
||||
"status": "verified",
|
||||
"source": "findings/subsystems/events.md 3.1 (def+0x40, _Myres at def+0x54, read at 0x00587a1d); re-used by lane U for the observed-tech dedup"
|
||||
},
|
||||
{
|
||||
"name": "TechTree_SetResearched_flag_Refresh",
|
||||
"offset": "0x8",
|
||||
"convention": "constant",
|
||||
"prototype": "flags bit 3 of SetResearched(def, flags): after the call, and after each recursive call from the availability sweep, run the refresh helper 0x00585ef0. Also enables the `node slot is NULL` re-lookup path at the head of the function (0x00580e30). No research-path call site sets it -- ProcessResearch passes 2 -- so neither behaviour is modelled",
|
||||
"status": "verified",
|
||||
"source": "findings/subsystems/unlock-cascade.md (lane U 2026-09-08, 0x00581e10 lines 24-26, 74-77)"
|
||||
},
|
||||
{
|
||||
"name": "TechTree_ProcessResearch_TechsUnlockedCollector",
|
||||
"addr": "0x00587cc3",
|
||||
"convention": "site",
|
||||
"prototype": "site inside TechTree::ProcessResearch: the tail loop that collects the newly available nodes for EVENT_TECHS_UNLOCKED. Runs only when tree->owner != 0, after the per-node loop AND after the decay sweep. Collects every node n with n != NULL, n->def != NULL, p = tree->nodes[n->def->techId] != NULL, p->state (+0x14) == 2, and n->turnAvailable (+0x20) == the owner's ModCount. Posts once if the collected vector is non-empty. NOTE the asymmetry: the state test is on the SELF-RESOLVED node p, the turn test on the iterated node n",
|
||||
"status": "verified",
|
||||
"source": "findings/subsystems/unlock-cascade.md (lane U 2026-09-08, get-decompilation 0x005876c0 lines 294-309)"
|
||||
},
|
||||
{
|
||||
"name": "ServerPlayer_OnTechResearched_RecordObservedTech",
|
||||
"addr": "0x00891790",
|
||||
"convention": "site",
|
||||
"prototype": "site at the very head of ServerPlayer::OnTechResearched: RecordObservedTech is the FIRST statement, called unconditionally on every completion -- before the ResT/roll block and before the !silent event post. It de-duplicates by tech name, so the observed-tech vector grows by one 0x2c element per completion of a tech not already observed and by nothing otherwise",
|
||||
"status": "verified",
|
||||
"source": "findings/subsystems/unlock-cascade.md (lane U 2026-09-08, decompilation of 0x00891790 line 78)"
|
||||
},
|
||||
{
|
||||
"name": "ServerPlayer_OnTechResearched_ResearchRollBlock",
|
||||
"addr": "0x00891790",
|
||||
"convention": "site",
|
||||
"prototype": "site in ServerPlayer::OnTechResearched, second statement: `if (this->ResT(+0x294) == def) { if (this->ResearchRollPending(+0x3b4)) RollResearchEvent(this); this->ResearchRollPending = 0; this->ResT = 0; }`. RollResearchEvent (0x0088df20) draws EXACTLY ONE NextFloat unconditionally and then enters 0x00889d60 only when roll < ResearchEventOdds -- the odds are 0 for every tech outside the plague and AI-rebellion families, so that branch is normally dead. This is the one extra RNG word a completion consumes, and clearing ResT means a second completion in the same pass consumes none",
|
||||
"status": "verified",
|
||||
"source": "findings/subsystems/unlock-cascade.md (lane U 2026-09-08, decompilation of 0x00891790 lines 79-85, 0x0088df20, 0x00889d60)"
|
||||
}
|
||||
]
|
||||
}
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
// GENERATED — do not edit. Facts about Sword of the Stars.exe (GOG 1.8.1).
|
||||
// Source: sots-re ghidra/addresses.json @ 795aa47, generated 2026-09-08 by tools/gen_addresses.py
|
||||
// Source: sots-re ghidra/addresses.json @ ae00053, generated 2026-09-08 by tools/gen_addresses.py
|
||||
// Runtime address = (uintptr_t)GetModuleHandle(NULL) + RVA (the exe is ASLR-relocated).
|
||||
#pragma once
|
||||
#include <cstdint>
|
||||
|
|
@ -1237,5 +1237,29 @@ constexpr uint32_t Game_StarSystem_OutputRates_Write = 0x00345190;
|
|||
constexpr uint32_t Game_StarSystem_OutputRates_Read = 0x003472a0;
|
||||
// layout sizeof(Game::StarSystem::OutputRates) -- enumeration meets embedding [verified]
|
||||
constexpr uint32_t sizeof_Game_StarSystem_OutputRates = 0x0000001c;
|
||||
// thiscall bool (TechTree* this, TechPrereqs* prereqs /* = TechDef + 0x88 */) // RET 4. An AND over groups, each group an OR over techs: a group is satisfied by any listed tech whose node exists in this->nodes AND whose state (+0x14) is 4. Zero groups -> TRUE (the function returns satisfied==total with both 0); a group with ZERO entries -> FALSE and the whole test fails, because the inner loop cannot break and the outer one then exits with that group uncounted. Reads only. Called from SetResearched twice: the unforced completion gate on the argument def, and the availability sweep on each node's self-resolved def [verified]
|
||||
constexpr uint32_t TechTree_PrereqsMet = 0x0017d8e0;
|
||||
// field TechPrereqs prereqs -- the block TechTree::PrereqsMet is called on. Two MSVC vectors back to back: the flat entry array at +0x00 and the group array at +0x10. SetResearched passes `def + 0x88` at both call sites [verified]
|
||||
constexpr uint32_t TechDef_off_Prereqs = 0x00000088;
|
||||
// field std::vector<TechPrereqEntry> at TechPrereqs+0x00; only its _Myfirst is read (`*param_2`), because the groups carry the bounds. Element stride 8, the entry's TechDef* at +0x00; the second word is never read by PrereqsMet [verified]
|
||||
constexpr uint32_t TechPrereqs_off_Entries = 0x00000000;
|
||||
// field std::vector<TechPrereqGroup> at TechPrereqs+0x10 (_Myfirst +0x10, _Mylast +0x14). Group count = (last - first) >> 3. Each group is {int start; int count} indexing the entry array: the OR-set is entries[start .. start+count) [verified]
|
||||
constexpr uint32_t TechPrereqs_off_Groups = 0x00000010;
|
||||
// field sizeof(TechPrereqEntry) -- the flat prerequisite entry, {TechDef* def; int unread} [verified]
|
||||
constexpr uint32_t TechPrereqs_entry_stride = 0x00000008;
|
||||
// field sizeof(TechPrereqGroup) -- {int start; int count} into the entry array [verified]
|
||||
constexpr uint32_t TechPrereqs_group_stride = 0x00000008;
|
||||
// field BYTE. Non-zero excludes the node from SetResearched's availability sweep entirely (`if ((char)def[0x2c] != 0) continue`, i.e. def+0xb0) -- it can still be completed by an explicit SetResearched and its cost/state are still lowered by the parent-edge sweep, but nothing ever moves it to state 2 and it never stamps turnAvailable, so it can never raise EVENT_TECHS_UNLOCKED. THE WRITE SITE WAS NOT READ: the name records what the byte does, not where it comes from. The tech-file keyword `unlock_explicitly` is the obvious candidate and matches the behaviour exactly, but MasterTechTree::ParseTech 0x0058b050 shows no reference to 0xb0 in its decompilation, so the link is a hypothesis and not a fact [verified]
|
||||
constexpr uint32_t TechDef_off_NoAutoAvailable = 0x000000b0;
|
||||
// field std::string name (0x1c bytes, _Mysize at +0x50, _Myres at +0x54: >= 0x10 selects the heap pointer). The substitution for every research event's %s, and the key RecordObservedTech de-duplicates the observed-tech vector on [verified]
|
||||
constexpr uint32_t TechDef_off_Name = 0x00000040;
|
||||
// constant flags bit 3 of SetResearched(def, flags): after the call, and after each recursive call from the availability sweep, run the refresh helper 0x00585ef0. Also enables the `node slot is NULL` re-lookup path at the head of the function (0x00580e30). No research-path call site sets it -- ProcessResearch passes 2 -- so neither behaviour is modelled [verified]
|
||||
constexpr uint32_t TechTree_SetResearched_flag_Refresh = 0x00000008;
|
||||
// site site inside TechTree::ProcessResearch: the tail loop that collects the newly available nodes for EVENT_TECHS_UNLOCKED. Runs only when tree->owner != 0, after the per-node loop AND after the decay sweep. Collects every node n with n != NULL, n->def != NULL, p = tree->nodes[n->def->techId] != NULL, p->state (+0x14) == 2, and n->turnAvailable (+0x20) == the owner's ModCount. Posts once if the collected vector is non-empty. NOTE the asymmetry: the state test is on the SELF-RESOLVED node p, the turn test on the iterated node n [verified]
|
||||
constexpr uint32_t TechTree_ProcessResearch_TechsUnlockedCollector = 0x00187cc3;
|
||||
// site site at the very head of ServerPlayer::OnTechResearched: RecordObservedTech is the FIRST statement, called unconditionally on every completion -- before the ResT/roll block and before the !silent event post. It de-duplicates by tech name, so the observed-tech vector grows by one 0x2c element per completion of a tech not already observed and by nothing otherwise [verified]
|
||||
constexpr uint32_t ServerPlayer_OnTechResearched_RecordObservedTech = 0x00491790;
|
||||
// site site in ServerPlayer::OnTechResearched, second statement: `if (this->ResT(+0x294) == def) { if (this->ResearchRollPending(+0x3b4)) RollResearchEvent(this); this->ResearchRollPending = 0; this->ResT = 0; }`. RollResearchEvent (0x0088df20) draws EXACTLY ONE NextFloat unconditionally and then enters 0x00889d60 only when roll < ResearchEventOdds -- the odds are 0 for every tech outside the plague and AI-rebellion families, so that branch is normally dead. This is the one extra RNG word a completion consumes, and clearing ResT means a second completion in the same pass consumes none [verified]
|
||||
constexpr uint32_t ServerPlayer_OnTechResearched_ResearchRollBlock = 0x00491790;
|
||||
|
||||
} // namespace sots::addr
|
||||
|
|
|
|||
795
verify/results/compare/unlock-b3-t1-5.json
Normal file
795
verify/results/compare/unlock-b3-t1-5.json
Normal file
|
|
@ -0,0 +1,795 @@
|
|||
{
|
||||
"coverage_contradicted": [],
|
||||
"coverage_unstated": [],
|
||||
"format": 1,
|
||||
"hooks": {
|
||||
"Game::TechTree::ProcessResearch": {
|
||||
"calls": 15,
|
||||
"compared": 15,
|
||||
"coverage": {
|
||||
"checked_regions": [
|
||||
"events",
|
||||
"node[0]",
|
||||
"node[105]",
|
||||
"node[106]",
|
||||
"node[107]",
|
||||
"node[108]",
|
||||
"node[109]",
|
||||
"node[10]",
|
||||
"node[110]",
|
||||
"node[111]",
|
||||
"node[112]",
|
||||
"node[113]",
|
||||
"node[114]",
|
||||
"node[115]",
|
||||
"node[116]",
|
||||
"node[117]",
|
||||
"node[118]",
|
||||
"node[119]",
|
||||
"node[11]",
|
||||
"node[120]",
|
||||
"node[121]",
|
||||
"node[122]",
|
||||
"node[123]",
|
||||
"node[124]",
|
||||
"node[125]",
|
||||
"node[126]",
|
||||
"node[127]",
|
||||
"node[128]",
|
||||
"node[129]",
|
||||
"node[12]",
|
||||
"node[130]",
|
||||
"node[131]",
|
||||
"node[132]",
|
||||
"node[133]",
|
||||
"node[134]",
|
||||
"node[135]",
|
||||
"node[136]",
|
||||
"node[137]",
|
||||
"node[138]",
|
||||
"node[139]",
|
||||
"node[13]",
|
||||
"node[140]",
|
||||
"node[141]",
|
||||
"node[142]",
|
||||
"node[143]",
|
||||
"node[144]",
|
||||
"node[145]",
|
||||
"node[146]",
|
||||
"node[147]",
|
||||
"node[148]",
|
||||
"node[149]",
|
||||
"node[14]",
|
||||
"node[151]",
|
||||
"node[152]",
|
||||
"node[153]",
|
||||
"node[154]",
|
||||
"node[155]",
|
||||
"node[156]",
|
||||
"node[157]",
|
||||
"node[158]",
|
||||
"node[159]",
|
||||
"node[15]",
|
||||
"node[160]",
|
||||
"node[161]",
|
||||
"node[162]",
|
||||
"node[163]",
|
||||
"node[164]",
|
||||
"node[165]",
|
||||
"node[166]",
|
||||
"node[167]",
|
||||
"node[168]",
|
||||
"node[169]",
|
||||
"node[16]",
|
||||
"node[170]",
|
||||
"node[171]",
|
||||
"node[172]",
|
||||
"node[173]",
|
||||
"node[174]",
|
||||
"node[175]",
|
||||
"node[177]",
|
||||
"node[178]",
|
||||
"node[179]",
|
||||
"node[17]",
|
||||
"node[180]",
|
||||
"node[181]",
|
||||
"node[182]",
|
||||
"node[183]",
|
||||
"node[184]",
|
||||
"node[185]",
|
||||
"node[186]",
|
||||
"node[187]",
|
||||
"node[188]",
|
||||
"node[189]",
|
||||
"node[18]",
|
||||
"node[190]",
|
||||
"node[191]",
|
||||
"node[192]",
|
||||
"node[193]",
|
||||
"node[194]",
|
||||
"node[195]",
|
||||
"node[196]",
|
||||
"node[197]",
|
||||
"node[198]",
|
||||
"node[199]",
|
||||
"node[19]",
|
||||
"node[1]",
|
||||
"node[200]",
|
||||
"node[201]",
|
||||
"node[202]",
|
||||
"node[203]",
|
||||
"node[204]",
|
||||
"node[205]",
|
||||
"node[206]",
|
||||
"node[207]",
|
||||
"node[208]",
|
||||
"node[209]",
|
||||
"node[20]",
|
||||
"node[210]",
|
||||
"node[211]",
|
||||
"node[212]",
|
||||
"node[213]",
|
||||
"node[214]",
|
||||
"node[215]",
|
||||
"node[216]",
|
||||
"node[217]",
|
||||
"node[218]",
|
||||
"node[219]",
|
||||
"node[21]",
|
||||
"node[220]",
|
||||
"node[221]",
|
||||
"node[222]",
|
||||
"node[223]",
|
||||
"node[224]",
|
||||
"node[225]",
|
||||
"node[226]",
|
||||
"node[227]",
|
||||
"node[228]",
|
||||
"node[229]",
|
||||
"node[22]",
|
||||
"node[230]",
|
||||
"node[231]",
|
||||
"node[232]",
|
||||
"node[233]",
|
||||
"node[234]",
|
||||
"node[235]",
|
||||
"node[236]",
|
||||
"node[237]",
|
||||
"node[238]",
|
||||
"node[239]",
|
||||
"node[23]",
|
||||
"node[240]",
|
||||
"node[241]",
|
||||
"node[242]",
|
||||
"node[243]",
|
||||
"node[244]",
|
||||
"node[245]",
|
||||
"node[246]",
|
||||
"node[247]",
|
||||
"node[248]",
|
||||
"node[249]",
|
||||
"node[24]",
|
||||
"node[250]",
|
||||
"node[251]",
|
||||
"node[252]",
|
||||
"node[253]",
|
||||
"node[254]",
|
||||
"node[255]",
|
||||
"node[256]",
|
||||
"node[257]",
|
||||
"node[258]",
|
||||
"node[259]",
|
||||
"node[25]",
|
||||
"node[260]",
|
||||
"node[261]",
|
||||
"node[262]",
|
||||
"node[263]",
|
||||
"node[264]",
|
||||
"node[265]",
|
||||
"node[266]",
|
||||
"node[267]",
|
||||
"node[268]",
|
||||
"node[269]",
|
||||
"node[26]",
|
||||
"node[270]",
|
||||
"node[271]",
|
||||
"node[272]",
|
||||
"node[273]",
|
||||
"node[274]",
|
||||
"node[275]",
|
||||
"node[276]",
|
||||
"node[277]",
|
||||
"node[278]",
|
||||
"node[279]",
|
||||
"node[27]",
|
||||
"node[280]",
|
||||
"node[281]",
|
||||
"node[282]",
|
||||
"node[283]",
|
||||
"node[284]",
|
||||
"node[285]",
|
||||
"node[286]",
|
||||
"node[287]",
|
||||
"node[288]",
|
||||
"node[289]",
|
||||
"node[28]",
|
||||
"node[290]",
|
||||
"node[291]",
|
||||
"node[292]",
|
||||
"node[29]",
|
||||
"node[2]",
|
||||
"node[30]",
|
||||
"node[31]",
|
||||
"node[32]",
|
||||
"node[33]",
|
||||
"node[34]",
|
||||
"node[35]",
|
||||
"node[36]",
|
||||
"node[37]",
|
||||
"node[38]",
|
||||
"node[39]",
|
||||
"node[3]",
|
||||
"node[40]",
|
||||
"node[41]",
|
||||
"node[42]",
|
||||
"node[43]",
|
||||
"node[44]",
|
||||
"node[45]",
|
||||
"node[46]",
|
||||
"node[47]",
|
||||
"node[48]",
|
||||
"node[49]",
|
||||
"node[4]",
|
||||
"node[50]",
|
||||
"node[51]",
|
||||
"node[52]",
|
||||
"node[53]",
|
||||
"node[54]",
|
||||
"node[55]",
|
||||
"node[56]",
|
||||
"node[57]",
|
||||
"node[58]",
|
||||
"node[5]",
|
||||
"node[60]",
|
||||
"node[61]",
|
||||
"node[62]",
|
||||
"node[63]",
|
||||
"node[64]",
|
||||
"node[65]",
|
||||
"node[66]",
|
||||
"node[67]",
|
||||
"node[68]",
|
||||
"node[69]",
|
||||
"node[6]",
|
||||
"node[70]",
|
||||
"node[72]",
|
||||
"node[74]",
|
||||
"node[77]",
|
||||
"node[78]",
|
||||
"node[7]",
|
||||
"node[80]",
|
||||
"node[81]",
|
||||
"node[85]",
|
||||
"node[86]",
|
||||
"node[87]",
|
||||
"node[88]",
|
||||
"node[89]",
|
||||
"node[8]",
|
||||
"node[90]",
|
||||
"node[91]",
|
||||
"node[92]",
|
||||
"node[94]",
|
||||
"node[98]",
|
||||
"node[99]",
|
||||
"node[9]",
|
||||
"observed_techs",
|
||||
"overbudget",
|
||||
"rng"
|
||||
],
|
||||
"guarded_calls": 15,
|
||||
"guards": [
|
||||
"player",
|
||||
"tree_header"
|
||||
],
|
||||
"spans": {
|
||||
"compare": [
|
||||
"player+0x10c:3",
|
||||
"player+0x110:3",
|
||||
"player+0x114:3",
|
||||
"player+0x124:3",
|
||||
"player+0x294:4",
|
||||
"tree_header+0x20:1",
|
||||
"player+0x130:3"
|
||||
]
|
||||
},
|
||||
"state": "partial",
|
||||
"undeclared_calls": 2,
|
||||
"undeclared_writes": 9,
|
||||
"unmodelled": [
|
||||
{
|
||||
"mitigation": "region:events",
|
||||
"risk": "medium",
|
||||
"what": "posts EVENT_RESEARCH_OVERBUDGET on the owner's EventStorage: ours reproduces the decision and the id sequence, so region:events compares next_id, but the composed EvDsc/EvMsg text is not reproduced and no region can see it",
|
||||
"why": "text comes from the game's string table, which the engine must not carry; ours posts into its own EventStorage and writes only the counts into the scratch copy, so no live byte moves and replace mode posts nothing at all"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:events",
|
||||
"risk": "low",
|
||||
"what": "composes EVENT_TECHS_UNLOCKED's message from the unlocked techs' names",
|
||||
"why": "the trigger and the list are modelled (SetResearched's availability sweep plus the tail collector, both read off the instruction stream), so region:events compares next_id; the names come from the game's string table, so the message is composed from node indices instead and is not the game's text"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:player, guard:tree_header",
|
||||
"risk": "high",
|
||||
"what": "TechTree::SetResearched in REPLACE mode: nothing of it runs",
|
||||
"why": "the cascade is compare-mode only. In replace mode every pointer is live game memory, and applying half of OnTechResearched -- the observed-tech append and the research-event roll, but not the tech-effect field writes -- would leave the player in a state no code path produces. A replace run therefore still leaves the completed node unstamped and no tech unlocked"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:player",
|
||||
"risk": "high",
|
||||
"what": "ServerPlayer::OnTechResearched's tech effects: the ~90 hard-coded ServerPlayer field writes, the plague-cure masks, the design-option bitmasks and the species tech flags",
|
||||
"why": "B2's milestone. `ours` models only the two parts of the callback this hook's regions can see -- the observed-tech append and the one RNG word RollResearchEvent draws -- and the rest is what the player guard reports"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:rng",
|
||||
"risk": "medium",
|
||||
"what": "the research-event branch RollResearchEvent takes when its roll beats the odds (0x00889d60: the plague and AI-rebellion event paths)",
|
||||
"why": "the one NextFloat is drawn unconditionally and is modelled; the branch behind it is entered only for the plague and AI-rebellion tech families, whose odds are 0 everywhere else. If it is ever entered, region:rng is the check -- it would consume draws ours does not"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:observed_techs",
|
||||
"risk": "medium",
|
||||
"what": "constructs the ObservedTech element it appends to ServerPlayer+0x274",
|
||||
"why": "`ours` models the append DECISION -- RecordObservedTech de-duplicates by tech name, so it decides whether the vector grows -- and moves the scratch header's byte span by one 0x2c element per append. The element's own fields (turn_first, turn_last, detected, the name string, `with`) are not built, and no region can see them"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:tree_header",
|
||||
"risk": "low",
|
||||
"what": "the tree's completion-order counter (TechTree+0x20) is read pre-call, not modelled as a region",
|
||||
"why": "the per-node `order` word IS compared, and it is stamped from a counter `ours` seeds from the pre-call read and advances itself; the counter's own final value is only seen by the tree_header guard"
|
||||
},
|
||||
{
|
||||
"mitigation": "",
|
||||
"risk": "low",
|
||||
"what": "writes a completion line to the game log",
|
||||
"why": "log text is not simulation state"
|
||||
}
|
||||
],
|
||||
"verdict": "partial",
|
||||
"why": ""
|
||||
},
|
||||
"diffs": [],
|
||||
"diverged": 0,
|
||||
"diverged_call_ids": [],
|
||||
"errors": 0,
|
||||
"modes": {
|
||||
"compare": 15
|
||||
}
|
||||
}
|
||||
},
|
||||
"inputs": [
|
||||
"/tmp/claude-1000/-home-alex/ec8e34f8-af37-4ef2-a309-ed6a15293097/scratchpad/u-b3-t1-5.jsonl"
|
||||
],
|
||||
"invalid": [],
|
||||
"kind": "report",
|
||||
"meta": [
|
||||
{
|
||||
"build": "unlock-405ba41-20260908T1026Z",
|
||||
"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",
|
||||
"risk": "medium",
|
||||
"what": "posts EVENT_RESEARCH_OVERBUDGET on the owner's EventStorage: ours reproduces the decision and the id sequence, so region:events compares next_id, but the composed EvDsc/EvMsg text is not reproduced and no region can see it",
|
||||
"why": "text comes from the game's string table, which the engine must not carry; ours posts into its own EventStorage and writes only the counts into the scratch copy, so no live byte moves and replace mode posts nothing at all"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:events",
|
||||
"risk": "low",
|
||||
"what": "composes EVENT_TECHS_UNLOCKED's message from the unlocked techs' names",
|
||||
"why": "the trigger and the list are modelled (SetResearched's availability sweep plus the tail collector, both read off the instruction stream), so region:events compares next_id; the names come from the game's string table, so the message is composed from node indices instead and is not the game's text"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:player, guard:tree_header",
|
||||
"risk": "high",
|
||||
"what": "TechTree::SetResearched in REPLACE mode: nothing of it runs",
|
||||
"why": "the cascade is compare-mode only. In replace mode every pointer is live game memory, and applying half of OnTechResearched -- the observed-tech append and the research-event roll, but not the tech-effect field writes -- would leave the player in a state no code path produces. A replace run therefore still leaves the completed node unstamped and no tech unlocked"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:player",
|
||||
"risk": "high",
|
||||
"what": "ServerPlayer::OnTechResearched's tech effects: the ~90 hard-coded ServerPlayer field writes, the plague-cure masks, the design-option bitmasks and the species tech flags",
|
||||
"why": "B2's milestone. `ours` models only the two parts of the callback this hook's regions can see -- the observed-tech append and the one RNG word RollResearchEvent draws -- and the rest is what the player guard reports"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:rng",
|
||||
"risk": "medium",
|
||||
"what": "the research-event branch RollResearchEvent takes when its roll beats the odds (0x00889d60: the plague and AI-rebellion event paths)",
|
||||
"why": "the one NextFloat is drawn unconditionally and is modelled; the branch behind it is entered only for the plague and AI-rebellion tech families, whose odds are 0 everywhere else. If it is ever entered, region:rng is the check -- it would consume draws ours does not"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:observed_techs",
|
||||
"risk": "medium",
|
||||
"what": "constructs the ObservedTech element it appends to ServerPlayer+0x274",
|
||||
"why": "`ours` models the append DECISION -- RecordObservedTech de-duplicates by tech name, so it decides whether the vector grows -- and moves the scratch header's byte span by one 0x2c element per append. The element's own fields (turn_first, turn_last, detected, the name string, `with`) are not built, and no region can see them"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:tree_header",
|
||||
"risk": "low",
|
||||
"what": "the tree's completion-order counter (TechTree+0x20) is read pre-call, not modelled as a region",
|
||||
"why": "the per-node `order` word IS compared, and it is stamped from a counter `ours` seeds from the pre-call read and advances itself; the counter's own final value is only seen by the tree_header guard"
|
||||
},
|
||||
{
|
||||
"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-08T10:30:02Z"
|
||||
}
|
||||
],
|
||||
"totals": {
|
||||
"calls": 15,
|
||||
"compared": 15,
|
||||
"coverage_contradicted": 0,
|
||||
"coverage_unstated": 0,
|
||||
"diverged": 0,
|
||||
"guarded_calls": 15,
|
||||
"invalid_records": 0,
|
||||
"undeclared_calls": 2,
|
||||
"undeclared_writes": 9
|
||||
},
|
||||
"warnings": []
|
||||
}
|
||||
26
verify/results/compare/unlock-b3-t1-5.md
Normal file
26
verify/results/compare/unlock-b3-t1-5.md
Normal file
|
|
@ -0,0 +1,26 @@
|
|||
## tracecmp report: u-b3-t1-5.jsonl
|
||||
|
||||
- build: unlock-405ba41-20260908T1026Z started: 2026-09-08T10:30:02Z inline_max: 256
|
||||
- calls: 15 compared: 15 diverged: 0 invalid records: 0 warnings: 0
|
||||
- coverage: 15 guarded call(s), 9 undeclared write(s) in 2 call(s); 0 hook(s) unstated, 0 contradicted
|
||||
|
||||
| hook | calls | modes | compared | diverged | errors |
|
||||
|---|---|---|---|---|---|
|
||||
| Game::TechTree::ProcessResearch | 15 | compare:15 | 15 | 0 | 0 |
|
||||
|
||||
### coverage
|
||||
|
||||
| hook | verdict | compared regions | guards | undeclared writes | unmodelled |
|
||||
|---|---|---|---|---|---|
|
||||
| Game::TechTree::ProcessResearch | partial | events, node[0], node[105], node[106], node[107], node[108], +271 | player, tree_header | 9 in 2 call(s) | 8 |
|
||||
|
||||
#### Game::TechTree::ProcessResearch — not checked by this run
|
||||
- (medium) posts EVENT_RESEARCH_OVERBUDGET on the owner's EventStorage: ours reproduces the decision and the id sequence, so region:events compares next_id, but the composed EvDsc/EvMsg text is not reproduced and no region can see it — text comes from the game's string table, which the engine must not carry; ours posts into its own EventStorage and writes only the counts into the scratch copy, so no live byte moves and replace mode posts nothing at all [region:events]
|
||||
- (low) composes EVENT_TECHS_UNLOCKED's message from the unlocked techs' names — the trigger and the list are modelled (SetResearched's availability sweep plus the tail collector, both read off the instruction stream), so region:events compares next_id; the names come from the game's string table, so the message is composed from node indices instead and is not the game's text [region:events]
|
||||
- (high) TechTree::SetResearched in REPLACE mode: nothing of it runs — the cascade is compare-mode only. In replace mode every pointer is live game memory, and applying half of OnTechResearched -- the observed-tech append and the research-event roll, but not the tech-effect field writes -- would leave the player in a state no code path produces. A replace run therefore still leaves the completed node unstamped and no tech unlocked [guard:player, guard:tree_header]
|
||||
- (high) ServerPlayer::OnTechResearched's tech effects: the ~90 hard-coded ServerPlayer field writes, the plague-cure masks, the design-option bitmasks and the species tech flags — B2's milestone. `ours` models only the two parts of the callback this hook's regions can see -- the observed-tech append and the one RNG word RollResearchEvent draws -- and the rest is what the player guard reports [guard:player]
|
||||
- (medium) the research-event branch RollResearchEvent takes when its roll beats the odds (0x00889d60: the plague and AI-rebellion event paths) — the one NextFloat is drawn unconditionally and is modelled; the branch behind it is entered only for the plague and AI-rebellion tech families, whose odds are 0 everywhere else. If it is ever entered, region:rng is the check -- it would consume draws ours does not [region:rng]
|
||||
- (medium) constructs the ObservedTech element it appends to ServerPlayer+0x274 — `ours` models the append DECISION -- RecordObservedTech de-duplicates by tech name, so it decides whether the vector grows -- and moves the scratch header's byte span by one 0x2c element per append. The element's own fields (turn_first, turn_last, detected, the name string, `with`) are not built, and no region can see them [region:observed_techs]
|
||||
- (low) the tree's completion-order counter (TechTree+0x20) is read pre-call, not modelled as a region — the per-node `order` word IS compared, and it is stamped from a counter `ours` seeds from the pre-call read and advances itself; the counter's own final value is only seen by the tree_header guard [guard:tree_header]
|
||||
- (low) writes a completion line to the game log — log text is not simulation state
|
||||
- guard hits in compare mode: player+0x10c:3, player+0x110:3, player+0x114:3, player+0x124:3, player+0x294:4, tree_header+0x20:1, player+0x130:3
|
||||
787
verify/results/compare/unlock-b3-t1.json
Normal file
787
verify/results/compare/unlock-b3-t1.json
Normal file
|
|
@ -0,0 +1,787 @@
|
|||
{
|
||||
"coverage_contradicted": [],
|
||||
"coverage_unstated": [],
|
||||
"format": 1,
|
||||
"hooks": {
|
||||
"Game::TechTree::ProcessResearch": {
|
||||
"calls": 3,
|
||||
"compared": 3,
|
||||
"coverage": {
|
||||
"checked_regions": [
|
||||
"events",
|
||||
"node[0]",
|
||||
"node[105]",
|
||||
"node[106]",
|
||||
"node[107]",
|
||||
"node[108]",
|
||||
"node[109]",
|
||||
"node[10]",
|
||||
"node[110]",
|
||||
"node[111]",
|
||||
"node[112]",
|
||||
"node[113]",
|
||||
"node[114]",
|
||||
"node[115]",
|
||||
"node[116]",
|
||||
"node[117]",
|
||||
"node[118]",
|
||||
"node[119]",
|
||||
"node[11]",
|
||||
"node[120]",
|
||||
"node[121]",
|
||||
"node[122]",
|
||||
"node[123]",
|
||||
"node[124]",
|
||||
"node[125]",
|
||||
"node[126]",
|
||||
"node[127]",
|
||||
"node[128]",
|
||||
"node[129]",
|
||||
"node[12]",
|
||||
"node[130]",
|
||||
"node[131]",
|
||||
"node[132]",
|
||||
"node[133]",
|
||||
"node[134]",
|
||||
"node[135]",
|
||||
"node[136]",
|
||||
"node[137]",
|
||||
"node[138]",
|
||||
"node[139]",
|
||||
"node[13]",
|
||||
"node[140]",
|
||||
"node[141]",
|
||||
"node[142]",
|
||||
"node[143]",
|
||||
"node[144]",
|
||||
"node[145]",
|
||||
"node[146]",
|
||||
"node[147]",
|
||||
"node[148]",
|
||||
"node[149]",
|
||||
"node[14]",
|
||||
"node[151]",
|
||||
"node[152]",
|
||||
"node[153]",
|
||||
"node[154]",
|
||||
"node[155]",
|
||||
"node[156]",
|
||||
"node[157]",
|
||||
"node[158]",
|
||||
"node[159]",
|
||||
"node[15]",
|
||||
"node[160]",
|
||||
"node[161]",
|
||||
"node[162]",
|
||||
"node[163]",
|
||||
"node[164]",
|
||||
"node[165]",
|
||||
"node[166]",
|
||||
"node[167]",
|
||||
"node[168]",
|
||||
"node[169]",
|
||||
"node[16]",
|
||||
"node[170]",
|
||||
"node[171]",
|
||||
"node[172]",
|
||||
"node[173]",
|
||||
"node[174]",
|
||||
"node[175]",
|
||||
"node[177]",
|
||||
"node[178]",
|
||||
"node[179]",
|
||||
"node[17]",
|
||||
"node[180]",
|
||||
"node[181]",
|
||||
"node[182]",
|
||||
"node[183]",
|
||||
"node[184]",
|
||||
"node[185]",
|
||||
"node[186]",
|
||||
"node[187]",
|
||||
"node[188]",
|
||||
"node[189]",
|
||||
"node[18]",
|
||||
"node[190]",
|
||||
"node[191]",
|
||||
"node[192]",
|
||||
"node[193]",
|
||||
"node[194]",
|
||||
"node[195]",
|
||||
"node[196]",
|
||||
"node[197]",
|
||||
"node[198]",
|
||||
"node[199]",
|
||||
"node[19]",
|
||||
"node[1]",
|
||||
"node[200]",
|
||||
"node[201]",
|
||||
"node[202]",
|
||||
"node[203]",
|
||||
"node[204]",
|
||||
"node[205]",
|
||||
"node[206]",
|
||||
"node[207]",
|
||||
"node[208]",
|
||||
"node[209]",
|
||||
"node[20]",
|
||||
"node[210]",
|
||||
"node[211]",
|
||||
"node[212]",
|
||||
"node[213]",
|
||||
"node[214]",
|
||||
"node[215]",
|
||||
"node[216]",
|
||||
"node[217]",
|
||||
"node[218]",
|
||||
"node[219]",
|
||||
"node[21]",
|
||||
"node[220]",
|
||||
"node[221]",
|
||||
"node[222]",
|
||||
"node[223]",
|
||||
"node[224]",
|
||||
"node[225]",
|
||||
"node[226]",
|
||||
"node[227]",
|
||||
"node[228]",
|
||||
"node[229]",
|
||||
"node[22]",
|
||||
"node[230]",
|
||||
"node[231]",
|
||||
"node[232]",
|
||||
"node[233]",
|
||||
"node[234]",
|
||||
"node[235]",
|
||||
"node[236]",
|
||||
"node[237]",
|
||||
"node[238]",
|
||||
"node[239]",
|
||||
"node[23]",
|
||||
"node[240]",
|
||||
"node[241]",
|
||||
"node[242]",
|
||||
"node[243]",
|
||||
"node[244]",
|
||||
"node[245]",
|
||||
"node[246]",
|
||||
"node[247]",
|
||||
"node[248]",
|
||||
"node[249]",
|
||||
"node[24]",
|
||||
"node[250]",
|
||||
"node[251]",
|
||||
"node[252]",
|
||||
"node[253]",
|
||||
"node[254]",
|
||||
"node[255]",
|
||||
"node[256]",
|
||||
"node[257]",
|
||||
"node[258]",
|
||||
"node[259]",
|
||||
"node[25]",
|
||||
"node[260]",
|
||||
"node[261]",
|
||||
"node[262]",
|
||||
"node[263]",
|
||||
"node[264]",
|
||||
"node[265]",
|
||||
"node[266]",
|
||||
"node[267]",
|
||||
"node[268]",
|
||||
"node[269]",
|
||||
"node[26]",
|
||||
"node[270]",
|
||||
"node[271]",
|
||||
"node[272]",
|
||||
"node[273]",
|
||||
"node[274]",
|
||||
"node[275]",
|
||||
"node[276]",
|
||||
"node[277]",
|
||||
"node[278]",
|
||||
"node[279]",
|
||||
"node[27]",
|
||||
"node[280]",
|
||||
"node[281]",
|
||||
"node[282]",
|
||||
"node[283]",
|
||||
"node[284]",
|
||||
"node[285]",
|
||||
"node[286]",
|
||||
"node[287]",
|
||||
"node[288]",
|
||||
"node[289]",
|
||||
"node[28]",
|
||||
"node[290]",
|
||||
"node[291]",
|
||||
"node[292]",
|
||||
"node[29]",
|
||||
"node[2]",
|
||||
"node[30]",
|
||||
"node[31]",
|
||||
"node[32]",
|
||||
"node[33]",
|
||||
"node[34]",
|
||||
"node[35]",
|
||||
"node[36]",
|
||||
"node[37]",
|
||||
"node[38]",
|
||||
"node[39]",
|
||||
"node[3]",
|
||||
"node[40]",
|
||||
"node[41]",
|
||||
"node[42]",
|
||||
"node[43]",
|
||||
"node[44]",
|
||||
"node[45]",
|
||||
"node[46]",
|
||||
"node[47]",
|
||||
"node[48]",
|
||||
"node[49]",
|
||||
"node[4]",
|
||||
"node[50]",
|
||||
"node[51]",
|
||||
"node[52]",
|
||||
"node[53]",
|
||||
"node[54]",
|
||||
"node[55]",
|
||||
"node[56]",
|
||||
"node[57]",
|
||||
"node[58]",
|
||||
"node[5]",
|
||||
"node[60]",
|
||||
"node[61]",
|
||||
"node[62]",
|
||||
"node[63]",
|
||||
"node[64]",
|
||||
"node[65]",
|
||||
"node[66]",
|
||||
"node[67]",
|
||||
"node[68]",
|
||||
"node[69]",
|
||||
"node[6]",
|
||||
"node[70]",
|
||||
"node[72]",
|
||||
"node[74]",
|
||||
"node[77]",
|
||||
"node[78]",
|
||||
"node[7]",
|
||||
"node[80]",
|
||||
"node[81]",
|
||||
"node[85]",
|
||||
"node[86]",
|
||||
"node[87]",
|
||||
"node[88]",
|
||||
"node[89]",
|
||||
"node[8]",
|
||||
"node[90]",
|
||||
"node[91]",
|
||||
"node[92]",
|
||||
"node[94]",
|
||||
"node[98]",
|
||||
"node[99]",
|
||||
"node[9]",
|
||||
"observed_techs",
|
||||
"overbudget",
|
||||
"rng"
|
||||
],
|
||||
"guarded_calls": 3,
|
||||
"guards": [
|
||||
"player",
|
||||
"tree_header"
|
||||
],
|
||||
"spans": {
|
||||
"compare": []
|
||||
},
|
||||
"state": "partial",
|
||||
"undeclared_calls": 0,
|
||||
"undeclared_writes": 0,
|
||||
"unmodelled": [
|
||||
{
|
||||
"mitigation": "region:events",
|
||||
"risk": "medium",
|
||||
"what": "posts EVENT_RESEARCH_OVERBUDGET on the owner's EventStorage: ours reproduces the decision and the id sequence, so region:events compares next_id, but the composed EvDsc/EvMsg text is not reproduced and no region can see it",
|
||||
"why": "text comes from the game's string table, which the engine must not carry; ours posts into its own EventStorage and writes only the counts into the scratch copy, so no live byte moves and replace mode posts nothing at all"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:events",
|
||||
"risk": "low",
|
||||
"what": "composes EVENT_TECHS_UNLOCKED's message from the unlocked techs' names",
|
||||
"why": "the trigger and the list are modelled (SetResearched's availability sweep plus the tail collector, both read off the instruction stream), so region:events compares next_id; the names come from the game's string table, so the message is composed from node indices instead and is not the game's text"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:player, guard:tree_header",
|
||||
"risk": "high",
|
||||
"what": "TechTree::SetResearched in REPLACE mode: nothing of it runs",
|
||||
"why": "the cascade is compare-mode only. In replace mode every pointer is live game memory, and applying half of OnTechResearched -- the observed-tech append and the research-event roll, but not the tech-effect field writes -- would leave the player in a state no code path produces. A replace run therefore still leaves the completed node unstamped and no tech unlocked"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:player",
|
||||
"risk": "high",
|
||||
"what": "ServerPlayer::OnTechResearched's tech effects: the ~90 hard-coded ServerPlayer field writes, the plague-cure masks, the design-option bitmasks and the species tech flags",
|
||||
"why": "B2's milestone. `ours` models only the two parts of the callback this hook's regions can see -- the observed-tech append and the one RNG word RollResearchEvent draws -- and the rest is what the player guard reports"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:rng",
|
||||
"risk": "medium",
|
||||
"what": "the research-event branch RollResearchEvent takes when its roll beats the odds (0x00889d60: the plague and AI-rebellion event paths)",
|
||||
"why": "the one NextFloat is drawn unconditionally and is modelled; the branch behind it is entered only for the plague and AI-rebellion tech families, whose odds are 0 everywhere else. If it is ever entered, region:rng is the check -- it would consume draws ours does not"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:observed_techs",
|
||||
"risk": "medium",
|
||||
"what": "constructs the ObservedTech element it appends to ServerPlayer+0x274",
|
||||
"why": "`ours` models the append DECISION -- RecordObservedTech de-duplicates by tech name, so it decides whether the vector grows -- and moves the scratch header's byte span by one 0x2c element per append. The element's own fields (turn_first, turn_last, detected, the name string, `with`) are not built, and no region can see them"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:tree_header",
|
||||
"risk": "low",
|
||||
"what": "the tree's completion-order counter (TechTree+0x20) is read pre-call, not modelled as a region",
|
||||
"why": "the per-node `order` word IS compared, and it is stamped from a counter `ours` seeds from the pre-call read and advances itself; the counter's own final value is only seen by the tree_header guard"
|
||||
},
|
||||
{
|
||||
"mitigation": "",
|
||||
"risk": "low",
|
||||
"what": "writes a completion line to the game log",
|
||||
"why": "log text is not simulation state"
|
||||
}
|
||||
],
|
||||
"verdict": "partial",
|
||||
"why": ""
|
||||
},
|
||||
"diffs": [],
|
||||
"diverged": 0,
|
||||
"diverged_call_ids": [],
|
||||
"errors": 0,
|
||||
"modes": {
|
||||
"compare": 3
|
||||
}
|
||||
}
|
||||
},
|
||||
"inputs": [
|
||||
"/tmp/claude-1000/-home-alex/ec8e34f8-af37-4ef2-a309-ed6a15293097/scratchpad/u-b3-t1.jsonl"
|
||||
],
|
||||
"invalid": [],
|
||||
"kind": "report",
|
||||
"meta": [
|
||||
{
|
||||
"build": "unlock-405ba41-20260908T1026Z",
|
||||
"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",
|
||||
"risk": "medium",
|
||||
"what": "posts EVENT_RESEARCH_OVERBUDGET on the owner's EventStorage: ours reproduces the decision and the id sequence, so region:events compares next_id, but the composed EvDsc/EvMsg text is not reproduced and no region can see it",
|
||||
"why": "text comes from the game's string table, which the engine must not carry; ours posts into its own EventStorage and writes only the counts into the scratch copy, so no live byte moves and replace mode posts nothing at all"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:events",
|
||||
"risk": "low",
|
||||
"what": "composes EVENT_TECHS_UNLOCKED's message from the unlocked techs' names",
|
||||
"why": "the trigger and the list are modelled (SetResearched's availability sweep plus the tail collector, both read off the instruction stream), so region:events compares next_id; the names come from the game's string table, so the message is composed from node indices instead and is not the game's text"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:player, guard:tree_header",
|
||||
"risk": "high",
|
||||
"what": "TechTree::SetResearched in REPLACE mode: nothing of it runs",
|
||||
"why": "the cascade is compare-mode only. In replace mode every pointer is live game memory, and applying half of OnTechResearched -- the observed-tech append and the research-event roll, but not the tech-effect field writes -- would leave the player in a state no code path produces. A replace run therefore still leaves the completed node unstamped and no tech unlocked"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:player",
|
||||
"risk": "high",
|
||||
"what": "ServerPlayer::OnTechResearched's tech effects: the ~90 hard-coded ServerPlayer field writes, the plague-cure masks, the design-option bitmasks and the species tech flags",
|
||||
"why": "B2's milestone. `ours` models only the two parts of the callback this hook's regions can see -- the observed-tech append and the one RNG word RollResearchEvent draws -- and the rest is what the player guard reports"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:rng",
|
||||
"risk": "medium",
|
||||
"what": "the research-event branch RollResearchEvent takes when its roll beats the odds (0x00889d60: the plague and AI-rebellion event paths)",
|
||||
"why": "the one NextFloat is drawn unconditionally and is modelled; the branch behind it is entered only for the plague and AI-rebellion tech families, whose odds are 0 everywhere else. If it is ever entered, region:rng is the check -- it would consume draws ours does not"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:observed_techs",
|
||||
"risk": "medium",
|
||||
"what": "constructs the ObservedTech element it appends to ServerPlayer+0x274",
|
||||
"why": "`ours` models the append DECISION -- RecordObservedTech de-duplicates by tech name, so it decides whether the vector grows -- and moves the scratch header's byte span by one 0x2c element per append. The element's own fields (turn_first, turn_last, detected, the name string, `with`) are not built, and no region can see them"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:tree_header",
|
||||
"risk": "low",
|
||||
"what": "the tree's completion-order counter (TechTree+0x20) is read pre-call, not modelled as a region",
|
||||
"why": "the per-node `order` word IS compared, and it is stamped from a counter `ours` seeds from the pre-call read and advances itself; the counter's own final value is only seen by the tree_header guard"
|
||||
},
|
||||
{
|
||||
"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-08T10:30:02Z"
|
||||
}
|
||||
],
|
||||
"totals": {
|
||||
"calls": 3,
|
||||
"compared": 3,
|
||||
"coverage_contradicted": 0,
|
||||
"coverage_unstated": 0,
|
||||
"diverged": 0,
|
||||
"guarded_calls": 3,
|
||||
"invalid_records": 0,
|
||||
"undeclared_calls": 0,
|
||||
"undeclared_writes": 0
|
||||
},
|
||||
"warnings": []
|
||||
}
|
||||
25
verify/results/compare/unlock-b3-t1.md
Normal file
25
verify/results/compare/unlock-b3-t1.md
Normal file
|
|
@ -0,0 +1,25 @@
|
|||
## tracecmp report: u-b3-t1.jsonl
|
||||
|
||||
- build: unlock-405ba41-20260908T1026Z started: 2026-09-08T10:30:02Z inline_max: 256
|
||||
- calls: 3 compared: 3 diverged: 0 invalid records: 0 warnings: 0
|
||||
- coverage: 3 guarded call(s), 0 undeclared write(s) in 0 call(s); 0 hook(s) unstated, 0 contradicted
|
||||
|
||||
| hook | calls | modes | compared | diverged | errors |
|
||||
|---|---|---|---|---|---|
|
||||
| Game::TechTree::ProcessResearch | 3 | compare:3 | 3 | 0 | 0 |
|
||||
|
||||
### coverage
|
||||
|
||||
| hook | verdict | compared regions | guards | undeclared writes | unmodelled |
|
||||
|---|---|---|---|---|---|
|
||||
| Game::TechTree::ProcessResearch | partial | events, node[0], node[105], node[106], node[107], node[108], +271 | player, tree_header | 0 | 8 |
|
||||
|
||||
#### Game::TechTree::ProcessResearch — not checked by this run
|
||||
- (medium) posts EVENT_RESEARCH_OVERBUDGET on the owner's EventStorage: ours reproduces the decision and the id sequence, so region:events compares next_id, but the composed EvDsc/EvMsg text is not reproduced and no region can see it — text comes from the game's string table, which the engine must not carry; ours posts into its own EventStorage and writes only the counts into the scratch copy, so no live byte moves and replace mode posts nothing at all [region:events]
|
||||
- (low) composes EVENT_TECHS_UNLOCKED's message from the unlocked techs' names — the trigger and the list are modelled (SetResearched's availability sweep plus the tail collector, both read off the instruction stream), so region:events compares next_id; the names come from the game's string table, so the message is composed from node indices instead and is not the game's text [region:events]
|
||||
- (high) TechTree::SetResearched in REPLACE mode: nothing of it runs — the cascade is compare-mode only. In replace mode every pointer is live game memory, and applying half of OnTechResearched -- the observed-tech append and the research-event roll, but not the tech-effect field writes -- would leave the player in a state no code path produces. A replace run therefore still leaves the completed node unstamped and no tech unlocked [guard:player, guard:tree_header]
|
||||
- (high) ServerPlayer::OnTechResearched's tech effects: the ~90 hard-coded ServerPlayer field writes, the plague-cure masks, the design-option bitmasks and the species tech flags — B2's milestone. `ours` models only the two parts of the callback this hook's regions can see -- the observed-tech append and the one RNG word RollResearchEvent draws -- and the rest is what the player guard reports [guard:player]
|
||||
- (medium) the research-event branch RollResearchEvent takes when its roll beats the odds (0x00889d60: the plague and AI-rebellion event paths) — the one NextFloat is drawn unconditionally and is modelled; the branch behind it is entered only for the plague and AI-rebellion tech families, whose odds are 0 everywhere else. If it is ever entered, region:rng is the check -- it would consume draws ours does not [region:rng]
|
||||
- (medium) constructs the ObservedTech element it appends to ServerPlayer+0x274 — `ours` models the append DECISION -- RecordObservedTech de-duplicates by tech name, so it decides whether the vector grows -- and moves the scratch header's byte span by one 0x2c element per append. The element's own fields (turn_first, turn_last, detected, the name string, `with`) are not built, and no region can see them [region:observed_techs]
|
||||
- (low) the tree's completion-order counter (TechTree+0x20) is read pre-call, not modelled as a region — the per-node `order` word IS compared, and it is stamped from a counter `ours` seeds from the pre-call read and advances itself; the counter's own final value is only seen by the tree_header guard [guard:tree_header]
|
||||
- (low) writes a completion line to the game log — log text is not simulation state
|
||||
754
verify/results/compare/unlock-b3-zuul.json
Normal file
754
verify/results/compare/unlock-b3-zuul.json
Normal file
|
|
@ -0,0 +1,754 @@
|
|||
{
|
||||
"coverage_contradicted": [],
|
||||
"coverage_unstated": [],
|
||||
"format": 1,
|
||||
"hooks": {
|
||||
"Game::TechTree::ProcessResearch": {
|
||||
"calls": 20,
|
||||
"compared": 20,
|
||||
"coverage": {
|
||||
"checked_regions": [
|
||||
"events",
|
||||
"node[0]",
|
||||
"node[106]",
|
||||
"node[107]",
|
||||
"node[108]",
|
||||
"node[109]",
|
||||
"node[10]",
|
||||
"node[110]",
|
||||
"node[111]",
|
||||
"node[112]",
|
||||
"node[113]",
|
||||
"node[114]",
|
||||
"node[115]",
|
||||
"node[116]",
|
||||
"node[117]",
|
||||
"node[118]",
|
||||
"node[119]",
|
||||
"node[120]",
|
||||
"node[121]",
|
||||
"node[122]",
|
||||
"node[123]",
|
||||
"node[124]",
|
||||
"node[125]",
|
||||
"node[126]",
|
||||
"node[129]",
|
||||
"node[130]",
|
||||
"node[131]",
|
||||
"node[132]",
|
||||
"node[133]",
|
||||
"node[134]",
|
||||
"node[135]",
|
||||
"node[136]",
|
||||
"node[137]",
|
||||
"node[138]",
|
||||
"node[139]",
|
||||
"node[140]",
|
||||
"node[141]",
|
||||
"node[143]",
|
||||
"node[144]",
|
||||
"node[145]",
|
||||
"node[146]",
|
||||
"node[147]",
|
||||
"node[148]",
|
||||
"node[149]",
|
||||
"node[14]",
|
||||
"node[151]",
|
||||
"node[152]",
|
||||
"node[153]",
|
||||
"node[154]",
|
||||
"node[155]",
|
||||
"node[156]",
|
||||
"node[157]",
|
||||
"node[158]",
|
||||
"node[159]",
|
||||
"node[160]",
|
||||
"node[161]",
|
||||
"node[162]",
|
||||
"node[163]",
|
||||
"node[164]",
|
||||
"node[165]",
|
||||
"node[166]",
|
||||
"node[167]",
|
||||
"node[168]",
|
||||
"node[169]",
|
||||
"node[170]",
|
||||
"node[171]",
|
||||
"node[172]",
|
||||
"node[173]",
|
||||
"node[174]",
|
||||
"node[175]",
|
||||
"node[176]",
|
||||
"node[177]",
|
||||
"node[178]",
|
||||
"node[179]",
|
||||
"node[180]",
|
||||
"node[181]",
|
||||
"node[182]",
|
||||
"node[183]",
|
||||
"node[184]",
|
||||
"node[185]",
|
||||
"node[186]",
|
||||
"node[187]",
|
||||
"node[188]",
|
||||
"node[189]",
|
||||
"node[18]",
|
||||
"node[190]",
|
||||
"node[191]",
|
||||
"node[192]",
|
||||
"node[193]",
|
||||
"node[194]",
|
||||
"node[195]",
|
||||
"node[196]",
|
||||
"node[197]",
|
||||
"node[198]",
|
||||
"node[199]",
|
||||
"node[19]",
|
||||
"node[200]",
|
||||
"node[201]",
|
||||
"node[202]",
|
||||
"node[203]",
|
||||
"node[204]",
|
||||
"node[205]",
|
||||
"node[206]",
|
||||
"node[207]",
|
||||
"node[208]",
|
||||
"node[209]",
|
||||
"node[210]",
|
||||
"node[211]",
|
||||
"node[212]",
|
||||
"node[213]",
|
||||
"node[214]",
|
||||
"node[215]",
|
||||
"node[216]",
|
||||
"node[218]",
|
||||
"node[219]",
|
||||
"node[21]",
|
||||
"node[220]",
|
||||
"node[221]",
|
||||
"node[222]",
|
||||
"node[223]",
|
||||
"node[224]",
|
||||
"node[225]",
|
||||
"node[226]",
|
||||
"node[227]",
|
||||
"node[228]",
|
||||
"node[229]",
|
||||
"node[22]",
|
||||
"node[230]",
|
||||
"node[231]",
|
||||
"node[232]",
|
||||
"node[233]",
|
||||
"node[234]",
|
||||
"node[235]",
|
||||
"node[236]",
|
||||
"node[237]",
|
||||
"node[238]",
|
||||
"node[239]",
|
||||
"node[23]",
|
||||
"node[240]",
|
||||
"node[241]",
|
||||
"node[242]",
|
||||
"node[243]",
|
||||
"node[244]",
|
||||
"node[245]",
|
||||
"node[246]",
|
||||
"node[247]",
|
||||
"node[248]",
|
||||
"node[24]",
|
||||
"node[259]",
|
||||
"node[25]",
|
||||
"node[260]",
|
||||
"node[261]",
|
||||
"node[262]",
|
||||
"node[263]",
|
||||
"node[264]",
|
||||
"node[26]",
|
||||
"node[270]",
|
||||
"node[271]",
|
||||
"node[272]",
|
||||
"node[273]",
|
||||
"node[274]",
|
||||
"node[275]",
|
||||
"node[276]",
|
||||
"node[27]",
|
||||
"node[282]",
|
||||
"node[283]",
|
||||
"node[284]",
|
||||
"node[285]",
|
||||
"node[286]",
|
||||
"node[287]",
|
||||
"node[288]",
|
||||
"node[289]",
|
||||
"node[28]",
|
||||
"node[290]",
|
||||
"node[291]",
|
||||
"node[292]",
|
||||
"node[29]",
|
||||
"node[30]",
|
||||
"node[31]",
|
||||
"node[32]",
|
||||
"node[33]",
|
||||
"node[34]",
|
||||
"node[35]",
|
||||
"node[36]",
|
||||
"node[37]",
|
||||
"node[38]",
|
||||
"node[39]",
|
||||
"node[3]",
|
||||
"node[41]",
|
||||
"node[42]",
|
||||
"node[43]",
|
||||
"node[44]",
|
||||
"node[45]",
|
||||
"node[46]",
|
||||
"node[47]",
|
||||
"node[48]",
|
||||
"node[49]",
|
||||
"node[50]",
|
||||
"node[51]",
|
||||
"node[52]",
|
||||
"node[53]",
|
||||
"node[54]",
|
||||
"node[55]",
|
||||
"node[56]",
|
||||
"node[57]",
|
||||
"node[58]",
|
||||
"node[61]",
|
||||
"node[62]",
|
||||
"node[63]",
|
||||
"node[64]",
|
||||
"node[65]",
|
||||
"node[66]",
|
||||
"node[67]",
|
||||
"node[68]",
|
||||
"node[69]",
|
||||
"node[6]",
|
||||
"node[70]",
|
||||
"node[72]",
|
||||
"node[74]",
|
||||
"node[80]",
|
||||
"node[81]",
|
||||
"node[85]",
|
||||
"node[89]",
|
||||
"node[8]",
|
||||
"node[90]",
|
||||
"node[91]",
|
||||
"node[92]",
|
||||
"node[93]",
|
||||
"node[94]",
|
||||
"node[95]",
|
||||
"node[96]",
|
||||
"node[98]",
|
||||
"node[99]",
|
||||
"node[9]",
|
||||
"observed_techs",
|
||||
"overbudget",
|
||||
"rng"
|
||||
],
|
||||
"guarded_calls": 20,
|
||||
"guards": [
|
||||
"player",
|
||||
"tree_header"
|
||||
],
|
||||
"spans": {
|
||||
"compare": [
|
||||
"player+0x10c:3",
|
||||
"player+0x110:3",
|
||||
"player+0x114:3",
|
||||
"player+0x124:3",
|
||||
"player+0x294:4",
|
||||
"tree_header+0x20:1"
|
||||
]
|
||||
},
|
||||
"state": "partial",
|
||||
"undeclared_calls": 2,
|
||||
"undeclared_writes": 8,
|
||||
"unmodelled": [
|
||||
{
|
||||
"mitigation": "region:events",
|
||||
"risk": "medium",
|
||||
"what": "posts EVENT_RESEARCH_OVERBUDGET on the owner's EventStorage: ours reproduces the decision and the id sequence, so region:events compares next_id, but the composed EvDsc/EvMsg text is not reproduced and no region can see it",
|
||||
"why": "text comes from the game's string table, which the engine must not carry; ours posts into its own EventStorage and writes only the counts into the scratch copy, so no live byte moves and replace mode posts nothing at all"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:events",
|
||||
"risk": "low",
|
||||
"what": "composes EVENT_TECHS_UNLOCKED's message from the unlocked techs' names",
|
||||
"why": "the trigger and the list are modelled (SetResearched's availability sweep plus the tail collector, both read off the instruction stream), so region:events compares next_id; the names come from the game's string table, so the message is composed from node indices instead and is not the game's text"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:player, guard:tree_header",
|
||||
"risk": "high",
|
||||
"what": "TechTree::SetResearched in REPLACE mode: nothing of it runs",
|
||||
"why": "the cascade is compare-mode only. In replace mode every pointer is live game memory, and applying half of OnTechResearched -- the observed-tech append and the research-event roll, but not the tech-effect field writes -- would leave the player in a state no code path produces. A replace run therefore still leaves the completed node unstamped and no tech unlocked"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:player",
|
||||
"risk": "high",
|
||||
"what": "ServerPlayer::OnTechResearched's tech effects: the ~90 hard-coded ServerPlayer field writes, the plague-cure masks, the design-option bitmasks and the species tech flags",
|
||||
"why": "B2's milestone. `ours` models only the two parts of the callback this hook's regions can see -- the observed-tech append and the one RNG word RollResearchEvent draws -- and the rest is what the player guard reports"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:rng",
|
||||
"risk": "medium",
|
||||
"what": "the research-event branch RollResearchEvent takes when its roll beats the odds (0x00889d60: the plague and AI-rebellion event paths)",
|
||||
"why": "the one NextFloat is drawn unconditionally and is modelled; the branch behind it is entered only for the plague and AI-rebellion tech families, whose odds are 0 everywhere else. If it is ever entered, region:rng is the check -- it would consume draws ours does not"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:observed_techs",
|
||||
"risk": "medium",
|
||||
"what": "constructs the ObservedTech element it appends to ServerPlayer+0x274",
|
||||
"why": "`ours` models the append DECISION -- RecordObservedTech de-duplicates by tech name, so it decides whether the vector grows -- and moves the scratch header's byte span by one 0x2c element per append. The element's own fields (turn_first, turn_last, detected, the name string, `with`) are not built, and no region can see them"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:tree_header",
|
||||
"risk": "low",
|
||||
"what": "the tree's completion-order counter (TechTree+0x20) is read pre-call, not modelled as a region",
|
||||
"why": "the per-node `order` word IS compared, and it is stamped from a counter `ours` seeds from the pre-call read and advances itself; the counter's own final value is only seen by the tree_header guard"
|
||||
},
|
||||
{
|
||||
"mitigation": "",
|
||||
"risk": "low",
|
||||
"what": "writes a completion line to the game log",
|
||||
"why": "log text is not simulation state"
|
||||
}
|
||||
],
|
||||
"verdict": "partial",
|
||||
"why": ""
|
||||
},
|
||||
"diffs": [],
|
||||
"diverged": 0,
|
||||
"diverged_call_ids": [],
|
||||
"errors": 0,
|
||||
"modes": {
|
||||
"compare": 20
|
||||
}
|
||||
}
|
||||
},
|
||||
"inputs": [
|
||||
"/tmp/claude-1000/-home-alex/ec8e34f8-af37-4ef2-a309-ed6a15293097/scratchpad/u-b3-zuul2.jsonl"
|
||||
],
|
||||
"invalid": [],
|
||||
"kind": "report",
|
||||
"meta": [
|
||||
{
|
||||
"build": "unlock-405ba41-20260908T1026Z",
|
||||
"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",
|
||||
"risk": "medium",
|
||||
"what": "posts EVENT_RESEARCH_OVERBUDGET on the owner's EventStorage: ours reproduces the decision and the id sequence, so region:events compares next_id, but the composed EvDsc/EvMsg text is not reproduced and no region can see it",
|
||||
"why": "text comes from the game's string table, which the engine must not carry; ours posts into its own EventStorage and writes only the counts into the scratch copy, so no live byte moves and replace mode posts nothing at all"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:events",
|
||||
"risk": "low",
|
||||
"what": "composes EVENT_TECHS_UNLOCKED's message from the unlocked techs' names",
|
||||
"why": "the trigger and the list are modelled (SetResearched's availability sweep plus the tail collector, both read off the instruction stream), so region:events compares next_id; the names come from the game's string table, so the message is composed from node indices instead and is not the game's text"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:player, guard:tree_header",
|
||||
"risk": "high",
|
||||
"what": "TechTree::SetResearched in REPLACE mode: nothing of it runs",
|
||||
"why": "the cascade is compare-mode only. In replace mode every pointer is live game memory, and applying half of OnTechResearched -- the observed-tech append and the research-event roll, but not the tech-effect field writes -- would leave the player in a state no code path produces. A replace run therefore still leaves the completed node unstamped and no tech unlocked"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:player",
|
||||
"risk": "high",
|
||||
"what": "ServerPlayer::OnTechResearched's tech effects: the ~90 hard-coded ServerPlayer field writes, the plague-cure masks, the design-option bitmasks and the species tech flags",
|
||||
"why": "B2's milestone. `ours` models only the two parts of the callback this hook's regions can see -- the observed-tech append and the one RNG word RollResearchEvent draws -- and the rest is what the player guard reports"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:rng",
|
||||
"risk": "medium",
|
||||
"what": "the research-event branch RollResearchEvent takes when its roll beats the odds (0x00889d60: the plague and AI-rebellion event paths)",
|
||||
"why": "the one NextFloat is drawn unconditionally and is modelled; the branch behind it is entered only for the plague and AI-rebellion tech families, whose odds are 0 everywhere else. If it is ever entered, region:rng is the check -- it would consume draws ours does not"
|
||||
},
|
||||
{
|
||||
"mitigation": "region:observed_techs",
|
||||
"risk": "medium",
|
||||
"what": "constructs the ObservedTech element it appends to ServerPlayer+0x274",
|
||||
"why": "`ours` models the append DECISION -- RecordObservedTech de-duplicates by tech name, so it decides whether the vector grows -- and moves the scratch header's byte span by one 0x2c element per append. The element's own fields (turn_first, turn_last, detected, the name string, `with`) are not built, and no region can see them"
|
||||
},
|
||||
{
|
||||
"mitigation": "guard:tree_header",
|
||||
"risk": "low",
|
||||
"what": "the tree's completion-order counter (TechTree+0x20) is read pre-call, not modelled as a region",
|
||||
"why": "the per-node `order` word IS compared, and it is stamped from a counter `ours` seeds from the pre-call read and advances itself; the counter's own final value is only seen by the tree_header guard"
|
||||
},
|
||||
{
|
||||
"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-08T10:40:32Z"
|
||||
}
|
||||
],
|
||||
"totals": {
|
||||
"calls": 20,
|
||||
"compared": 20,
|
||||
"coverage_contradicted": 0,
|
||||
"coverage_unstated": 0,
|
||||
"diverged": 0,
|
||||
"guarded_calls": 20,
|
||||
"invalid_records": 0,
|
||||
"undeclared_calls": 2,
|
||||
"undeclared_writes": 8
|
||||
},
|
||||
"warnings": []
|
||||
}
|
||||
26
verify/results/compare/unlock-b3-zuul.md
Normal file
26
verify/results/compare/unlock-b3-zuul.md
Normal file
|
|
@ -0,0 +1,26 @@
|
|||
## tracecmp report: u-b3-zuul2.jsonl
|
||||
|
||||
- build: unlock-405ba41-20260908T1026Z started: 2026-09-08T10:40:32Z inline_max: 256
|
||||
- calls: 20 compared: 20 diverged: 0 invalid records: 0 warnings: 0
|
||||
- coverage: 20 guarded call(s), 8 undeclared write(s) in 2 call(s); 0 hook(s) unstated, 0 contradicted
|
||||
|
||||
| hook | calls | modes | compared | diverged | errors |
|
||||
|---|---|---|---|---|---|
|
||||
| Game::TechTree::ProcessResearch | 20 | compare:20 | 20 | 0 | 0 |
|
||||
|
||||
### coverage
|
||||
|
||||
| hook | verdict | compared regions | guards | undeclared writes | unmodelled |
|
||||
|---|---|---|---|---|---|
|
||||
| Game::TechTree::ProcessResearch | partial | events, node[0], node[106], node[107], node[108], node[109], +231 | player, tree_header | 8 in 2 call(s) | 8 |
|
||||
|
||||
#### Game::TechTree::ProcessResearch — not checked by this run
|
||||
- (medium) posts EVENT_RESEARCH_OVERBUDGET on the owner's EventStorage: ours reproduces the decision and the id sequence, so region:events compares next_id, but the composed EvDsc/EvMsg text is not reproduced and no region can see it — text comes from the game's string table, which the engine must not carry; ours posts into its own EventStorage and writes only the counts into the scratch copy, so no live byte moves and replace mode posts nothing at all [region:events]
|
||||
- (low) composes EVENT_TECHS_UNLOCKED's message from the unlocked techs' names — the trigger and the list are modelled (SetResearched's availability sweep plus the tail collector, both read off the instruction stream), so region:events compares next_id; the names come from the game's string table, so the message is composed from node indices instead and is not the game's text [region:events]
|
||||
- (high) TechTree::SetResearched in REPLACE mode: nothing of it runs — the cascade is compare-mode only. In replace mode every pointer is live game memory, and applying half of OnTechResearched -- the observed-tech append and the research-event roll, but not the tech-effect field writes -- would leave the player in a state no code path produces. A replace run therefore still leaves the completed node unstamped and no tech unlocked [guard:player, guard:tree_header]
|
||||
- (high) ServerPlayer::OnTechResearched's tech effects: the ~90 hard-coded ServerPlayer field writes, the plague-cure masks, the design-option bitmasks and the species tech flags — B2's milestone. `ours` models only the two parts of the callback this hook's regions can see -- the observed-tech append and the one RNG word RollResearchEvent draws -- and the rest is what the player guard reports [guard:player]
|
||||
- (medium) the research-event branch RollResearchEvent takes when its roll beats the odds (0x00889d60: the plague and AI-rebellion event paths) — the one NextFloat is drawn unconditionally and is modelled; the branch behind it is entered only for the plague and AI-rebellion tech families, whose odds are 0 everywhere else. If it is ever entered, region:rng is the check -- it would consume draws ours does not [region:rng]
|
||||
- (medium) constructs the ObservedTech element it appends to ServerPlayer+0x274 — `ours` models the append DECISION -- RecordObservedTech de-duplicates by tech name, so it decides whether the vector grows -- and moves the scratch header's byte span by one 0x2c element per append. The element's own fields (turn_first, turn_last, detected, the name string, `with`) are not built, and no region can see them [region:observed_techs]
|
||||
- (low) the tree's completion-order counter (TechTree+0x20) is read pre-call, not modelled as a region — the per-node `order` word IS compared, and it is stamped from a counter `ours` seeds from the pre-call read and advances itself; the counter's own final value is only seen by the tree_header guard [guard:tree_header]
|
||||
- (low) writes a completion line to the game log — log text is not simulation state
|
||||
- guard hits in compare mode: player+0x10c:3, player+0x110:3, player+0x114:3, player+0x124:3, player+0x294:4, tree_header+0x20:1
|
||||
94
verify/results/shim/unlock-shim.log
Normal file
94
verify/results/shim/unlock-shim.log
Normal file
|
|
@ -0,0 +1,94 @@
|
|||
06:30:02.121 [tid 6384] ==== sots-engine shim (binkw32 proxy) build unlock-405ba41-20260908T1026Z ====
|
||||
06:30:02.121 [tid 6384] exe: C:\SOTS\Sword of the Stars.exe
|
||||
06:30:02.121 [tid 6384] exe base=0x00e80000 (link-time image base 0x00400000, ASLR delta +11010048) pid=7268 shim=69530000
|
||||
06:30:02.121 [tid 6384] addresses: Source: sots-re ghidra/addresses.json @ 545c715, generated 2026-09-08 by tools/gen_addresses.py
|
||||
06:30:02.121 [tid 6384] config: hooks=trace
|
||||
06:30:02.121 [tid 6384] config: hook.Shim::SelfTest::Fill=off
|
||||
06:30:02.121 [tid 6384] config: hook.Mars::GlobalConsts::LoadFile=off
|
||||
06:30:02.121 [tid 6384] config: hook.Game::WeaponDictionary::Init=off
|
||||
06:30:02.121 [tid 6384] config: hook.Game::SectionDictionary::SectionDictionary=off
|
||||
06:30:02.121 [tid 6384] config: hook.Game::ServerPlayer::ComputeBudget=off
|
||||
06:30:02.121 [tid 6384] config: hook.Game::ServerPlayer::OnTechResearched=off
|
||||
06:30:02.121 [tid 6384] config: hook.Game::ServerSystem::ProcessTurn=off
|
||||
06:30:02.121 [tid 6384] config: hook.Game::StrategyServer::MoveFleet=off
|
||||
06:30:02.121 [tid 6384] config: hook.Game::StrategyServer::ProcessFleetMovement=off
|
||||
06:30:02.121 [tid 6384] config: hook.Game::TechTree::ProcessResearch=compare
|
||||
06:30:02.121 [tid 6384] config: trace.path=C:\SOTS\shim.trace.jsonl
|
||||
06:30:02.121 [tid 6384] config: trace.inline_max=256
|
||||
06:30:02.121 [tid 6384] config: trace.flush=always
|
||||
06:30:02.183 [tid 6384] trace: C:\SOTS\shim.trace.jsonl (default mode trace, inline_max 256, flush always)
|
||||
06:30:02.183 [tid 6384] hook: Mars_Application_Initialize rva=0x004a0e50 -> va=01320e50
|
||||
06:30:02.183 [tid 6384] hook: MH_Initialize -> MH_OK
|
||||
06:30:02.183 [tid 6384] hook: MH_CreateHook -> MH_OK (trampoline=017e0fe0)
|
||||
06:30:02.199 [tid 6384] hook: MH_EnableHook -> MH_OK
|
||||
06:30:02.199 [tid 6384] cfg: GlobalConsts hook ready (scale constant 0.017453292519943295)
|
||||
06:30:02.199 [tid 6384] hook: Mars::GlobalConsts::LoadFile rva=0x004b73c0 mode=off (not installed)
|
||||
06:30:02.199 [tid 6384] dict: dictionaries hook ready (crt new=6adc232b delete=6adc0174)
|
||||
06:30:02.199 [tid 6384] hook: Game::WeaponDictionary::Init rva=0x0019a4c0 mode=off (not installed)
|
||||
06:30:02.199 [tid 6384] hook: Game::SectionDictionary::SectionDictionary rva=0x00176f40 mode=off (not installed)
|
||||
06:30:02.199 [tid 6384] research: ProcessResearch hook ready (Cost=00ffda00, node=0x34, rng=0x9cc, fpu_cw=0x027f)
|
||||
06:30:02.199 [tid 6384] hook: Game::TechTree::ProcessResearch rva=0x001876c0 -> va=010076c0 MH_CreateHook -> MH_OK (trampoline=017e0fc0)
|
||||
06:30:02.215 [tid 6384] hook: Game::TechTree::ProcessResearch MH_EnableHook -> MH_OK mode=compare
|
||||
06:30:02.215 [tid 6384] techfx: OnTechResearched hook ready (regions=15, gate=0/0, fpu_cw=0x027f)
|
||||
06:30:02.215 [tid 6384] hook: Game::ServerPlayer::OnTechResearched rva=0x00491790 mode=off (not installed)
|
||||
06:30:02.215 [tid 6384] hook: Game::ServerPlayer::ComputeBudget rva=0x00463030 mode=off (not installed)
|
||||
06:30:02.215 [tid 6384] hook: Game::ServerSystem::ProcessTurn rva=0x003598e0 mode=off (not installed)
|
||||
06:30:02.215 [tid 6384] hook: Game::StrategyServer::MoveFleet rva=0x003d9ee0 mode=off (not installed)
|
||||
06:30:02.215 [tid 6384] hook: Game::StrategyServer::ProcessFleetMovement rva=0x003da9a0 mode=off (not installed)
|
||||
06:30:02.215 [tid 6384] fpu: module init, entry cw=0x027f 53bit-double/nearest; force=off value=0x0000 sample_ticks=on
|
||||
06:30:02.215 [tid 6384] fpu: StrategyClient::EndTurn rva=0x00383be0 -> va=01203be0 MH_CreateHook -> MH_OK (trampoline=017e0fa0)
|
||||
06:30:02.230 [tid 6384] fpu: StrategyClient::EndTurn MH_EnableHook -> MH_OK
|
||||
06:30:02.230 [tid 6384] fpu: StrategyServer::BeginProcessTurn rva=0x003d98e0 -> va=012598e0 MH_CreateHook -> MH_OK (trampoline=017e0f80)
|
||||
06:30:02.246 [tid 6384] fpu: StrategyServer::BeginProcessTurn MH_EnableHook -> MH_OK
|
||||
06:30:02.246 [tid 6384] fpu: StrategyServer::ProcessTurn rva=0x003dc6c0 -> va=0125c6c0 MH_CreateHook -> MH_OK (trampoline=017e0f60)
|
||||
06:30:02.262 [tid 6384] fpu: StrategyServer::ProcessTurn MH_EnableHook -> MH_OK
|
||||
06:30:02.262 [tid 6384] fpu: DemoApp::OnTick rva=0x0049a640 -> va=0131a640 MH_CreateHook -> MH_OK (trampoline=017e0f40)
|
||||
06:30:02.262 [tid 6384] fpu: DemoApp::OnTick MH_EnableHook -> MH_OK
|
||||
06:30:02.262 [tid 6384] selftest: Shim::SelfTest::Fill mode=off checksum=075ef0c3 records=0
|
||||
06:30:02.277 [tid 6384] Application::Initialize called (this=03b38128)
|
||||
06:30:03.027 [tid 6384] fpu: TICK BASELINE at OnTick (this=03b38128): cw=0x127f 53bit-double/nearest
|
||||
06:35:03.077 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=0e92ee08): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:35:06.155 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=351dd610): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:35:06.186 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=351dc038): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:35:06.218 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=351e0908): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:35:07.171 [tid 6384] fpu: sample at StrategyServer::BeginProcessTurn (this=0e966350): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:35:07.171 [tid 6384] fpu: sample at StrategyServer::ProcessTurn (this=0e966350): cw=0x127f 53bit-double/nearest
|
||||
06:35:07.186 [tid 6384] research: cascade ok=1 completions=0 unlocked=0 otch_appends=0 roll_draws=0 failures=0 depth=0 name_unreadable=0
|
||||
06:35:07.202 [tid 6384] research: cascade ok=1 completions=0 unlocked=0 otch_appends=0 roll_draws=0 failures=0 depth=0 name_unreadable=0
|
||||
06:35:07.233 [tid 6384] research: cascade ok=1 completions=0 unlocked=0 otch_appends=0 roll_draws=0 failures=0 depth=0 name_unreadable=0
|
||||
06:36:33.764 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=0e92ee08): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:36:36.811 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=351dd610): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:36:36.843 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=351dc038): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:36:36.858 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=351e0908): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:36:37.827 [tid 6384] fpu: sample at StrategyServer::BeginProcessTurn (this=0e966350): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:36:37.827 [tid 6384] fpu: sample at StrategyServer::ProcessTurn (this=0e966350): cw=0x127f 53bit-double/nearest
|
||||
06:36:37.843 [tid 6384] research: cascade ok=1 completions=1 unlocked=3 otch_appends=1 roll_draws=0 failures=0 depth=0 name_unreadable=0
|
||||
06:36:37.874 [tid 6384] research: cascade ok=1 completions=0 unlocked=0 otch_appends=0 roll_draws=0 failures=0 depth=0 name_unreadable=0
|
||||
06:36:37.889 [tid 6384] research: cascade ok=1 completions=0 unlocked=0 otch_appends=0 roll_draws=0 failures=0 depth=0 name_unreadable=0
|
||||
06:37:03.343 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=0e92ee08): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:37:06.421 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=351dd610): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:37:06.436 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=351dc038): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:37:06.468 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=351e0908): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:37:07.421 [tid 6384] fpu: sample at StrategyServer::BeginProcessTurn (this=0e966350): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:37:07.421 [tid 6384] fpu: sample at StrategyServer::ProcessTurn (this=0e966350): cw=0x127f 53bit-double/nearest
|
||||
06:37:07.436 [tid 6384] research: cascade ok=1 completions=0 unlocked=0 otch_appends=0 roll_draws=0 failures=0 depth=0 name_unreadable=0
|
||||
06:37:07.468 [tid 6384] research: cascade ok=1 completions=0 unlocked=0 otch_appends=0 roll_draws=0 failures=0 depth=0 name_unreadable=0
|
||||
06:37:07.483 [tid 6384] research: cascade ok=1 completions=0 unlocked=0 otch_appends=0 roll_draws=0 failures=0 depth=0 name_unreadable=0
|
||||
06:37:32.858 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=0e92ee08): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:37:35.921 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=351dd610): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:37:35.936 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=351dc038): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:37:35.968 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=351e0908): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:37:36.936 [tid 6384] fpu: sample at StrategyServer::BeginProcessTurn (this=0e966350): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:37:36.936 [tid 6384] fpu: sample at StrategyServer::ProcessTurn (this=0e966350): cw=0x127f 53bit-double/nearest
|
||||
06:37:36.952 [tid 6384] research: cascade ok=1 completions=1 unlocked=3 otch_appends=1 roll_draws=0 failures=0 depth=0 name_unreadable=0
|
||||
06:37:36.983 [tid 6384] research: cascade ok=1 completions=0 unlocked=0 otch_appends=0 roll_draws=0 failures=0 depth=0 name_unreadable=0
|
||||
06:37:36.999 [tid 6384] research: cascade ok=1 completions=0 unlocked=0 otch_appends=0 roll_draws=0 failures=0 depth=0 name_unreadable=0
|
||||
06:38:02.624 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=0e92ee08): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:38:05.686 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=351dd610): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:38:05.702 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=351dc038): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:38:05.733 [tid 6384] fpu: sample at StrategyClient::EndTurn (this=351e0908): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:38:06.686 [tid 6384] fpu: sample at StrategyServer::BeginProcessTurn (this=0e966350): cw=0x127f 53bit-double/nearest [no fpu.force configured]
|
||||
06:38:06.686 [tid 6384] fpu: sample at StrategyServer::ProcessTurn (this=0e966350): cw=0x127f 53bit-double/nearest
|
||||
06:38:06.702 [tid 6384] research: cascade ok=1 completions=0 unlocked=0 otch_appends=0 roll_draws=0 failures=0 depth=0 name_unreadable=0
|
||||
06:38:06.733 [tid 6384] research: cascade ok=1 completions=0 unlocked=0 otch_appends=0 roll_draws=0 failures=0 depth=0 name_unreadable=0
|
||||
06:38:06.749 [tid 6384] research: cascade ok=1 completions=0 unlocked=0 otch_appends=0 roll_draws=0 failures=0 depth=0 name_unreadable=0
|
||||
BIN
verify/traces/unlock-b3-t1-5.jsonl.gz
Normal file
BIN
verify/traces/unlock-b3-t1-5.jsonl.gz
Normal file
Binary file not shown.
BIN
verify/traces/unlock-b3-t1.jsonl.gz
Normal file
BIN
verify/traces/unlock-b3-t1.jsonl.gz
Normal file
Binary file not shown.
BIN
verify/traces/unlock-b3-zuul.jsonl.gz
Normal file
BIN
verify/traces/unlock-b3-zuul.jsonl.gz
Normal file
Binary file not shown.
Loading…
Add table
Reference in a new issue