Follow-up to #364. Part of #360. Optional research support for #385.
Goal
Capture stopped-state information only if an identified experiment requires data unavailable from existing unknown-call decision events.
Start condition
First name the consumer, the research question and the fields it cannot obtain by aggregating #364 events. Basic call counts, model decisions and stop-site frequencies do not justify a new snapshot API. If no concrete consumer needs a snapshot, leave this work deferred.
#364 provides decision callbacks only. It deliberately provides neither persistent path history nor stopped-frontier snapshots.
Scope
- Add opt-in capture orthogonal to the fallback setting only for the demonstrated consumer.
- Capture detached data rather than retaining live TsState/TsContext objects or allocation counters.
- Include the minimum stopping event, relevant signatures/statements and constraint status needed by that consumer.
- Add history or textual constraints only when explicitly required; do not serialize the entire engine state.
- Prefer experiment-owned aggregation/storage over changes to generic usvm-core primitives.
- Keep captured stopped states separate from completed execution states and generated tests.
- Define bounded retention and ownership with the consumer.
Definition of Done
- The consumer and required information are documented before implementation.
- Capture does not alter exploration decisions; observer failure isolation and detached ownership have focused tests.
- A stopped snapshot is never counted as a completed/replay-confirmed result.
- Deliver only the scoped research support in a separate PR when needed.
This issue does not block #365/#366, the census, or baseline evaluation in #385. It becomes a prerequisite only if the chosen measurement demonstrably requires it.
Follow-up to #364. Part of #360. Optional research support for #385.
Goal
Capture stopped-state information only if an identified experiment requires data unavailable from existing unknown-call decision events.
Start condition
First name the consumer, the research question and the fields it cannot obtain by aggregating #364 events. Basic call counts, model decisions and stop-site frequencies do not justify a new snapshot API. If no concrete consumer needs a snapshot, leave this work deferred.
#364 provides decision callbacks only. It deliberately provides neither persistent path history nor stopped-frontier snapshots.
Scope
Definition of Done
This issue does not block #365/#366, the census, or baseline evaluation in #385. It becomes a prerequisite only if the chosen measurement demonstrably requires it.