merge lane V: live event verification - advance prediction held field for field; sizeof(ObservedTech)=44 confirmed behaviourally
This commit is contained in:
alex
commit
517e1f2e52
1 changed files with 163 additions and 0 deletions
163
docs/V-eventlive.md
Normal file
163
docs/V-eventlive.md
Normal file
|
|
@ -0,0 +1,163 @@
|
||||||
|
# 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.
|
||||||
Loading…
Add table
Reference in a new issue