410f980832
Ran the queued VM140 verification of docs/P-events-wiring.md §4 with main dd38117
unchanged, cross-built on CT111 as eventlive-dd38117-20260908T0916Z and staged to
C:\SOTS\shimdist-v.
First End Turn on shim.cfg.recapb3 unchanged: 3 calls, 3 compared, 0 divergent,
tracecmp exit 0. Every field lane P forecast for call 0 read as predicted, including
turn=3, events_turn_bucket_exists=true, events_dedup_risk=0, next_id 3->4 on both
sides and observed_techs.bytes unchanged on all three calls.
Five End Turns: exit 1 with two divergent calls instead of three, both short by
exactly one id (7/6 and 12/11) — the unmodelled EVENT_TECHS_UNLOCKED, at the size
lane P said it would be.
sizeof(Game::ObservedTech) measured live at 44 on both completion calls
(observed_techs.bytes 440->484 and 484->528), confirming a static pin behaviourally.
That confirmation was written into the RE repo's addresses.json and has already
reached the generated header on main, so this branch carries docs only.
One deviation from lane R: rng diverged on call 9 because the completed tech had
research_roll_pending set, so the OnTechResearched callback drew one word ours does
not. That is a declared out-of-scope boundary, and it means lane R's "RNG 15/15" was
workload luck rather than a property of the hook.
Also closed the Zuul double roll behaviourally on a species-5 save made for the
purpose: 8 calls, 0 divergent, and all four species-5 researching calls advance the
generator by two with ours matching bit-for-bit.
clean_room_check.sh OK; host ctest 33/33. Run as separate commands.
163 lines
8.7 KiB
Markdown
163 lines
8.7 KiB
Markdown
# V — the live verification of lane P's event posting
|
||
|
||
Lane P wrote a prediction into `docs/P-events-wiring.md` §4 **before** any of this ran, and it
|
||
is the strongest kind of evidence this project can produce: a numeric forecast of a live run,
|
||
written down first, then checked. This lane ran it.
|
||
|
||
**The prediction held, field for field, on both runs.** Nothing below is an adjustment to the
|
||
model; the only new information is a workload effect (§4) and a measurement lane P asked for
|
||
(§3).
|
||
|
||
* Build: `eventlive-dd38117-20260908T0916Z` — main `dd38117` unchanged, cross-built on CT111
|
||
(`/srv/re-lab/build/sots-engine-v`, exports byte-identical to the real `binkw32.dll`),
|
||
staged `C:\SOTS\shimdist-v` on VM140.
|
||
* Recipe: `shim.cfg.recapb3` **unchanged**, `ref-turn2.sav` → Launch → End Turn, then four more
|
||
End Turns in the same session (turn 2 → turn 7).
|
||
* `tools/clean_room_check.sh` — **OK**. Host `ctest` — **33/33 passed**. Run as separate
|
||
commands, before and after the one-line regeneration of the address header.
|
||
* The End-Turn oracle held: `(Autosave EndTurn).sav` = `bb4fd9ac89f41e3b…`, `(Autosave).sav` =
|
||
`978041acd168b56e…`, the same two hashes lane R recorded. The events wiring does not perturb
|
||
the game.
|
||
|
||
---
|
||
|
||
## 1. First End Turn — prediction vs. outcome
|
||
|
||
**Predicted: 3 calls, 3 compared, 0 divergent, `tracecmp` exit 0. Observed: exactly that.**
|
||
|
||
| field (call 0) | lane P predicted | observed | |
|
||
|---|---|---|---|
|
||
| `turn` | 3 | 3 | ✓ |
|
||
| `events_turn_bucket_exists` | true | true | ✓ |
|
||
| `events_next_id_in` | 3 | 3 | ✓ |
|
||
| `events_in_turn_bucket` | 1 | 1 | ✓ |
|
||
| `events_dedup_risk` | 0 | 0 | ✓ |
|
||
| `events_scan_truncated` | absent | absent | ✓ |
|
||
| `events.next_id` | 3 → 4, both sides | 3 → 4, no divergence | ✓ |
|
||
| `events.turns` / `turns_bytes` | 2 / 0x30, unchanged | 2 / 48, unchanged | ✓ |
|
||
| `node[144].progress` | 2879 → 5768 | 2879 → 5768 | ✓ |
|
||
| `node[144].flag` | 1 → 2 | 1 → 2 | ✓ |
|
||
| `rng` | identical | `left` 432→431, `next_index` 192→193, `mt` hash identical | ✓ |
|
||
| `observed_techs.bytes` | unchanged on all 3 calls | 440 / 880 / 880, unchanged | ✓ |
|
||
| calls 1 and 2 | `EvNxID = 0`, scratch header untouched | 0 → 0, `turns_bytes` 0 | ✓ |
|
||
|
||
The alloc on call 0 was `{tech 144, 2889}`, species 2, `fpu_cw = 0x127f` — lane R's call 0
|
||
exactly. The one field that made lane R's run exit 1 is now clean, and it is clean for the
|
||
stated reason: the scan found a turn-3 bucket already holding one event, nothing in it could
|
||
collide with what we post (`events_dedup_risk = 0`), so the count model is exact for that call
|
||
rather than a lower bound.
|
||
|
||
Report: `verify/results/compare/eventlive-b3-t1.md` in the RE repo; trace
|
||
`verify/traces/eventlive-b3-t1.jsonl`.
|
||
|
||
## 2. Five End Turns — the residual is the predicted size
|
||
|
||
**Predicted: still exit 1, two divergent calls instead of three, each off by exactly 1.
|
||
Observed: exit 1, 15 calls, 15 compared, 2 divergent.**
|
||
|
||
| call | lane P predicted `next_id` orig → ours | observed | |
|
||
|---|---|---|---|
|
||
| 0 | 4 / **4** | 4 / 4, not divergent | ✓ |
|
||
| 3 | 7 / **6** | 7 / **6** | ✓ |
|
||
| 6 | 8 / 8 | 8 / 8 | ✓ |
|
||
| 9 | 12 / **11** | 12 / **11** | ✓ |
|
||
| 12 | 14 / 14 | 14 / 14 | ✓ |
|
||
| all others | 0 / 0 | 0 / 0 | ✓ |
|
||
|
||
Both residuals are `EVENT_TECHS_UNLOCKED`, exactly as §3 of `P-events-wiring.md` predicted and
|
||
for the reason it gave: the unlock cascade is an input `ours` is handed as *"no list"*, not an
|
||
empty one. A zero-divergence result here would have meant something was masking a known-missing
|
||
event; it did not happen.
|
||
|
||
The two divergent calls still carry their `SetResearched` fields (`cost_rp`/`state`/
|
||
`turn_available` on the unlocked children, `order`/`turn_researched` on the completed node),
|
||
which B3 declared out of scope in advance. Nothing new there.
|
||
|
||
**§4.3 also held.** `player+0x274/0x278/0x27c` no longer appear as undeclared guard spans; the
|
||
vector shows up in the diff as `observed_techs.bytes` instead. Undeclared spans dropped from 13
|
||
in 2 calls (lane R) to 10 in 2 calls, and the conversion is visible call by call.
|
||
|
||
## 3. `sizeof(Game::ObservedTech)` — 44, measured live
|
||
|
||
Lane P's §4.4 measurement, taken on both completion calls:
|
||
|
||
| call | `observed_techs.bytes` orig | delta |
|
||
|---|---|---|
|
||
| 3 | 440 → 484 | **+44** |
|
||
| 9 | 484 → 528 | **+44** |
|
||
|
||
`sizeof(Game::ObservedTech) = 0x2c (44)` — an independent **behavioural** confirmation of a
|
||
purely static result. Lane X pinned it three ways off the instruction stream and lane S mapped
|
||
every field from the serializer; the running game now agrees. The two non-researching players'
|
||
vectors measured 880 = 20 × 44 on every call and never moved. `addresses.json` carries the live
|
||
confirmation on both `ObservedTech_sizeof` and `ServerPlayer_off_ObservedTechs`.
|
||
|
||
Note for whoever wires the append: `RecordObservedTech` de-duplicates by tech name, so a
|
||
re-observation appends nothing. "No delta" is not a contradiction until you have checked
|
||
whether the tech was already observed.
|
||
|
||
## 4. The one thing that differed from lane R's run — and why it is not a defect
|
||
|
||
`rng` diverged on call 9: the original ended at `left` 374 / `next_index` 250, `ours` at
|
||
375 / 249. **The original drew one word that `ours` did not.**
|
||
|
||
That is the `RollResearchEvent` draw inside `OnTechResearched` — the same one word, at the same
|
||
two generator positions, that lane R measured from inside the `OnTechResearched` hook
|
||
(`left` 375 → 374, `next_index` 249 → 250) when `IND_TRKSTL` completed with
|
||
`research_roll_pending` set. B3 declared `SetResearched` and its owner callback out of scope,
|
||
and `P-events-wiring.md` §3 says in as many words that the callback "consumes one extra RNG
|
||
word". So this is a declared boundary showing itself, not a model failure.
|
||
|
||
What it *does* correct is a reading of lane R's result. **"RNG matched 15 of 15" was workload
|
||
luck, not a property of the hook.** Lane R's five-turn session never completed a tech that had
|
||
a pending research roll on this call; mine did, because from turn 4 the AI picks a different
|
||
target (lane R's own trap #2). The honest statement is: `ProcessResearch`'s `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 — until whichever lane takes `SetResearched`
|
||
models the callback.
|
||
|
||
The two guard spans that are new in this run relative to lane R's are `player+0x196` and
|
||
`player+0x3b4`, and both are already-named fields seen from the caller: `+0x3b4` is
|
||
`ServerPlayer_off_ResearchRollPending`, and `+0x196` is byte 2 of the design-option mask B at
|
||
`ServerPlayer_off_TechMaskA + 4` (lane R saw it from inside `OnTechResearched` as
|
||
`b` 64 → 2097216, i.e. `0x40 → 0x200040`).
|
||
|
||
## 5. Zuul double roll — closed, on a save this lane made
|
||
|
||
The board's `Zuul double-roll (behavioural)` row was blocked purely on a workload: no save in
|
||
`verify/` has a species-5 player, so `if (owner == Species::Zuul) r.roll = min(r.roll,
|
||
rng.NextFloat())` was disassembly plus host tests only. The check it asked for was one live
|
||
compare where `left` drops by 2 instead of 1.
|
||
|
||
A custom game was created on the VM with **only Zuul in the Available Species pool**, both
|
||
players therefore Zuul, and four End Turns run under the same `shim.cfg.recapb3` compare
|
||
config:
|
||
|
||
**8 calls, 8 compared, 0 divergent, `tracecmp` exit 0.** Four of the eight are researching
|
||
calls with `species = 5`, and every one of them advances the generator by **two**:
|
||
|
||
| call | turn | alloc | `left` | `next_index` |
|
||
|---|---|---|---|---|
|
||
| 0 | 2 | {144, 982} | 540 → **538** | 84 → **86** |
|
||
| 2 | 3 | {144, 960} | 522 → **520** | 102 → **104** |
|
||
| 4 | 4 | {144, 1417} | 504 → **502** | 120 → **122** |
|
||
| 6 | 5 | {144, 1372} | 485 → **483** | 139 → **141** |
|
||
|
||
(The four interleaved calls are the second Zuul player with a zero allocation: no draw,
|
||
`left` unchanged, and they compare clean too.)
|
||
|
||
`ours` reproduced the post-state of the generator bit-for-bit on all four — the `mt` block hash,
|
||
`left` and `next_index` all identical — so the double roll is now **behaviourally verified**,
|
||
not just implemented. The save is in the RE repo as
|
||
`verify/results/saves/zuul-turn5-species5.sav` and on the VM as
|
||
`C:\SOTS\SavedGames\zuul-turn5.sav`.
|
||
|
||
## 6. Still owed
|
||
|
||
* `EVENT_TECHS_UNLOCKED` — the residual, now measured twice at exactly 1. It belongs with
|
||
`SetResearched`, because computing it means running the unlock cascade.
|
||
* The `OnTechResearched` RNG draw, §4 — same owner, same reason.
|
||
* `TechTree::GetProgressRatio` (0x0057e950): the COMPLETE/UNDERBUDGET split is still analogy.
|
||
* Not reached by this lane: expense sliders / a debtor / a research-aid treaty (the eight
|
||
always-zero `ComputeBudget` slots), a temperance sweep, a plague, `PruneOldTurns`, and
|
||
replace mode on any hook.
|