sots-re/verify/results/compare/unlock-b3-t1.md
Alex 5a3f986f38 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).
2026-09-08 06:57:37 -04:00

25 lines
3.7 KiB
Markdown

## 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