68 lines
4.2 KiB
Markdown
68 lines
4.2 KiB
Markdown
# Independent correction verification plan
|
|
|
|
Session `run-ee78b8773688ca09f8046e21`; actor `research-abi-correction-verifier`;
|
|
model `openai/gpt-5.6-sol`. This plan predates the verifier capture. It covers static
|
|
reproduction and does not authorize game, allocator, VM, Ghidra, or build-host execution.
|
|
|
|
## Required identities and positive execution
|
|
|
|
The assigned paired source manifests must rehash to engine
|
|
`ccd8e02083e8d2e2b3e97976ace2273c8f924dfc02a39e919004eaf3544c50fd` at HEAD
|
|
`7741d42fc5e4e761e6449bdaf0e4a61d00036a23` and RE
|
|
`6696fd5201e144843617cbf6d78b41b5287ad5dcc9fa1e8aaa861d52b64e72e8` at HEAD
|
|
`3bfde5a70d874a723e797a695bbd847fd82c0aa7`. The input must be 7,898,624-byte
|
|
`dumps/sots.exe` SHA-256 `970b7de729956a53094c7eb98aba4270aee98e2fed5daf0d39e290013c90c841`.
|
|
The instrument must be 373,888-byte `/usr/bin/objdump` SHA-256
|
|
`1eaaef2e7f57c4c7f69115c495e2466f5a8c8e5f3bc42221d092382f30f9d4cd`, GNU
|
|
objdump 2.38. Every command must return zero, emit nonempty stdout and empty stderr.
|
|
|
|
## Falsifiers
|
|
|
|
1. Any source, binary, tool, command boundary, byte count, or digest mismatch fails
|
|
reproduction; a decoded-looking listing does not override provenance failure.
|
|
2. Any write to `[EBP-0x20]` in get/create before the call at `0x00885413` falsifies the
|
|
corrected uninitialized-in-this-routine claim. Absence of a write does not prove a runtime
|
|
value, randomness, or allocator safety.
|
|
3. Failure of append to copy source `+4` to destination `+4`, or advancement of `_Mylast`
|
|
before nested copy returns, falsifies the claimed append ordering.
|
|
4. A final requested-turn store before temporary nested cleanup, or a returned pointer other
|
|
than `_Mylast-0x18`, falsifies the usable miss-path postcondition.
|
|
5. A nested-copy destination not initialized to three null pointers, allocation on its empty
|
|
branch, failure to expose a nonempty allocation/range-copy branch, or a stride other than
|
|
`0x74` falsifies the nested ownership interpretation.
|
|
6. A null nested-vector destructor path that destroys/frees, or a nonnull path lacking
|
|
per-element virtual destruction, `0x00924faa` free, and final three-pointer zeroing,
|
|
falsifies cleanup accounting.
|
|
7. Zero commands, unexpected skips, truncated terminal instructions, or fewer than all four
|
|
declared windows fails the package even if surviving hashes match.
|
|
|
|
## Required branch exposures and distinct states
|
|
|
|
* Get/create: empty outer vector; nonempty/no match; one match; duplicate matches selecting the
|
|
last; hit early return with no construction; and miss construction through cleanup/final store.
|
|
These are static control-flow states, not executed runtime fixtures.
|
|
* Outer append: spare-capacity external-source copy and full-capacity growth dispatch; the
|
|
source-inside-vector branch must be distinguished where the window exposes it. No allocation
|
|
failure is claimed executed.
|
|
* Nested copy: empty source (no allocation) versus nonempty source (allocation and `0x74`-stride
|
|
range copy), plus visible unwind edge without claiming a thrown execution.
|
|
* Nested destruction: null first pointer versus nonnull element loop/free, including final
|
|
pointer-zero state.
|
|
* Ordering: incoming transient scalar copy, nested copy completion, outer `_Mylast` advance,
|
|
temporary nested cleanup, requested-turn publication, then returned last element.
|
|
|
|
## Held-out challenge / ablation
|
|
|
|
In addition to byte-for-byte reproduction of the four handoff commands, capture each window with
|
|
its stop address widened by four bytes. Require every original stream's instruction rows to be an
|
|
exact prefix of the widened stream's rows and inspect the first added instruction. This challenges
|
|
the assumption that exact stop boundaries did not truncate a terminal instruction, the provenance
|
|
failure that invalidated earlier packages. Independently enumerate get/create stack-memory writes
|
|
through `0x00885413`; do not infer the answer from report prose.
|
|
|
|
## Acceptance limits
|
|
|
|
Success is an **independent static full compare** of four windows plus a static boundary ablation.
|
|
It is not original-game runtime comparison, integrated replay, live allocator safety, failure-path
|
|
execution, or independent replacement acceptance. Missing full/spare live fixtures, nonempty live
|
|
nested-copy state, transient observation, and induced unwind remain residuals.
|