sots-re/verify/results/research-completion-abi/run-16f8e9b6376b278c4870be09/report.md

64 lines
3.8 KiB
Markdown

# TurnEvents miss-path correction capture
This is a **fresh static measurement**, not live execution, allocator-safety evidence, independent
verification, or replacement acceptance. It implements the read-only analyst repair required by
Astra decision `d-b51f3f76803e852ed250846a`.
## Provenance and positive execution
`manifest.json` records four GNU objdump 2.38 invocations. Each returned zero, emitted nonempty
stdout and empty stderr. The freshly hashed inputs are:
* owner-supplied `dumps/sots.exe`: SHA-256
`970b7de729956a53094c7eb98aba4270aee98e2fed5daf0d39e290013c90c841`;
* `/usr/bin/objdump`: SHA-256
`1eaaef2e7f57c4c7f69115c495e2466f5a8c8e5f3bc42221d092382f30f9d4cd`;
* assigned engine source binding:
`ccd8e02083e8d2e2b3e97976ace2273c8f924dfc02a39e919004eaf3544c50fd`;
* assigned RE source binding:
`6696fd5201e144843617cbf6d78b41b5287ad5dcc9fa1e8aaa861d52b64e72e8`.
All four stdout hashes equal the corresponding records in the historical bridge manifest
`run-472955e277202c411388c66b/manifest.json`. This is same-tool/same-binary reproduction by the ABI
analyst, not the required independent-verifier reproduction.
## Recorded instruction facts
For valid containers and normally returning callees:
1. Complete get/create entry `0x00885380..0x0088544a` reserves stack space but does not initialize
`[EBP-0x20]`, the temporary `TurnEvents+4` / `EvTurn` word. The miss path writes the vptr at
`[EBP-0x24]`, nested-vector pointers at `-0x1c/-0x18/-0x14`, and EH state at `-4`.
2. Append's external-source branch at `0x00884d62..0x00884d73` loads source `+4`, stores it to
destination `+4`, then invokes nested-vector copy. It advances `_Mylast` at `0x00884d78`.
3. Nested copy `0x00779850` first zeros all three destination pointers. Its empty-source branch at
`0x007798b2` reaches the return without allocation; a nonempty source instead allocates and
range-copy-constructs `0x74`-byte `PlayerEvent` elements. The captured unwind edge calls
`0x00629580`; no throw was executed.
4. Get/create calls temporary nested-vector cleanup at `0x00885422`, then writes the requested turn
into the stored last element at `0x0088542d`, then returns `_Mylast-0x18` in EAX.
5. Cleanup `0x00629580` skips destruction/free for a null first pointer; otherwise it invokes each
`0x74`-stride element's virtual destructor, calls `0x00924faa` on the nested allocation, and in
either case zeros all three vector pointers.
## Corrected interpretation
**Decision:** describe the pre-append scalar only as an incoming stack word not initialized by this
routine. It is neither measured randomness nor necessarily nonzero. Do not encode a zero default or
attempt to reproduce an uninitialized read in clean-room code. The usable static postcondition is
that, after successful append and temporary cleanup, the stored new bucket contains the requested
turn and EAX identifies that bucket.
**Unexercised / unresolved:** full-capacity allocation at this call site, nonempty nested copy,
failure/unwind outcomes, transient observers/reentrancy, padding bytes and live CRT compatibility.
No event ID, event record, RNG, or other game state is written by get/create itself in the captured
normal path beyond outer container construction/pointers and the new bucket's fields.
## Independent falsifiers still required
The independent verifier should freshly hash the tool/binary and reproduce all four windows, then
check these distinct branches/states: existing duplicate turn buckets select the last match and do
not write; miss with spare versus full outer capacity; empty versus nonempty nested vector; and
cleanup-before-final-turn-store ordering. A future leased runtime fixture, if separately authorized,
can use distinct stack sentinels and spare/full capacity with neutral controls. Coherent parsing or
a final correct `EvTurn` alone cannot prove transient field semantics or allocator safety.