sots-re/verify/results/research-completion-abi-correction-verifier/verification-plan-run-d6c4dc15e9f4d15155fee856.md

56 lines
4 KiB
Markdown

# Verification plan — run-d6c4dc15e9f4d15155fee856
Role `verifier`; actor `research-abi-correction-verifier`; requested model
`openai/gpt-5.6-sol`. This plan predates this session's disassembly and save-state experiments.
## Scope separation
The analyst package is a fresh **static capture**, not live allocator execution, original-assisted
execution, partial/full compare, independent replacement, or integrated replay. This verifier will
independently reproduce static instruction/byte facts and archived save values only. It will not
claim runtime allocator safety, event posting, replacement acceptance, or integrated-tree evidence.
## Falsifiers
1. Reject if contract/campaign validation fails, an open surprise exists, either paired worktree is
not at its pinned baseline/common repository, source binding differs from the handoff, or binary
or objdump identity differs. Dirty trees are acceptable only when their full source digests match.
2. Reject zero executions, nonzero command exits, empty required stdout, unexpected stderr/skips,
missing streams, reused output, or a manifest/session mismatch.
3. Require stop `0x00779a20` to be incomplete despite exit zero: raw bytes must show `74 10` while
decoded output at `0x00779a1f` shows only `74`. If counted as a complete stream, reject.
4. Require aligned stops `0x00779a21`, `0x00779a23`, and `0x00779a28` to add exactly complete
`74 10`, `8b cf`, and `e8 28 6a ff ff` rows. Any truncated terminal row or non-prefix change in
the shared decoded range rejects the boundary interpretation.
5. Independently hold out stop `0x00779913` for nested-copy authority. It must include complete
`ret 4` at `0x00779912` without entering the later routine; compare it with raw terminal bytes.
A bad terminal boundary or changed preceding rows falsifies the package's authority boundary.
6. Check key ABI claims directly: get/create and outer append end `ret 4`; nested destruction ends
`ret`; nested copy has normal `ret 4`, unwind cleanup, and deallocation paths; get/create has no
write to temporary `[ebp-0x20]` before append, copies source `+4`, cleans the temporary nested
vector, then stores requested turn to the stored element. Contradictory def/use evidence pauses.
7. Independently parse the archived save, not narrative counters. Require the named player/event
container elements, IDs, strings, exact `0x7f7fffff` position words, and empty player states to
match. Missing parse coverage or unexpected skips reject archived-value validation.
8. Check actual RNG evidence independently: static helper captures execute no game and therefore
expose no RNG state/draws. Any claim that unchanged/zero RNG was measured by these captures is a
failure. Archived W1 unchanged RNG remains historical and outside this static reproduction.
## Required branch exposures and distinct states
Static instruction exposure required now: existing last-match return versus miss; spare-capacity
append versus full-capacity growth edges; empty versus nonempty nested copy; null versus nonnull
nested destruction; normal return versus unwind cleanup; short/long string branch instructions;
known-bad truncated versus aligned boundary. Instruction exposure is not runtime execution.
Runtime states still unexercised and must remain explicit residuals: existing-last-match, miss with
spare/full outer capacity, empty/nonempty nested vectors owning short/long strings, deliberate
allocation failure/throw, duplicate/description-only-different events, and transient stack
sentinels. Archived save states are distinct from all of those and validate serialized values only.
## Planned reproduction
Create a fail-if-exists session directory owned by this verifier. Use an independent script, not the
analyst's hard-coded recipe, to bind source/input/tool identities, run the package windows and held-
out boundary, archive raw stdout/stderr, parse instruction rows and save values, and emit a manifest
whose failed predictions/residuals remain failures or limitations.