sots-re/verify/results/research-completion-abi-independent/verification-plan-run-7d85d45cb2196e07025e5096.md

41 lines
2.7 KiB
Markdown

# Verification plan — run-7d85d45cb2196e07025e5096
Scope classification: independent static reproduction plus archived-state inspection. This quantum
will not execute the original game, allocator, constructors/destructors, an independent replacement,
or integrated replay. It therefore cannot establish live allocator safety or replacement acceptance.
## Preconditions and falsifiers fixed before experiments
Fail or pause affected interpretation if any assigned worktree HEAD/common Git directory differs
from the contract baseline, either source binding differs from the evidence records, the binary or
tool identity differs, any required command has nonzero exit/empty stdout/nonempty stderr, any
declared window is skipped/truncated without an explicit paired boundary, evidence hashes are stale,
or direct save coverage does not rebuild every inflated byte.
Semantic falsifiers are: collapse of ObservedTech `0x2c` and PlayerEvent `0x74` element strides;
raw transfer rather than deep assignment of string state; fewer than three independently guarded
long-string releases in PlayerEvent destruction; description omission from duplicate equality;
`0x7f7fffff` words; or event/RNG claims available only from counters rather than direct archived
tree leaves. A contradiction is a surprise, not a passing residual.
## Required exposures and distinct states
Static windows must expose both narrow/truncated and minimally widened return boundaries; plain
`ret` as a negative control; `0x2c` versus `0x74` stepping; inline versus heap string selection;
three destructor capacity checks and delete calls; equal versus differing description branch;
ordered-equal versus unordered coordinate branch; and constructor default loads plus direct image
bytes. Required runtime states remain empty/short/long string, spare/full capacity, new/existing
tech, duplicate/nonduplicate and description-only-different event, finite/NaN coordinate,
empty/nonempty nested vector, normal/unwind destruction, and prune/get-or-create boundaries. Raw
branch exposure is not reported as live execution of those states.
Archived-state checks require strict zero-resync parsing, direct `EvNxID`, bucket elements and event
fields, exact whole-save byte rebuild, and the actual `/Sim/RNG` leaf byte count/digest independently
of reported counters.
## Held-out challenge
Challenge objdump-dependent terminal-byte interpretation by parsing the PE section table directly
and mapping selected virtual addresses to file offsets. Compare direct bytes for all seven repaired
`ret imm16` boundaries, the plain-ret control, and constructor defaults. Also run a negative control
at one byte before the plain `ret` to ensure boundary inclusion is not generalized from `ret imm16`.