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

3.8 KiB

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.