Skip to content

[TS Calls][Research] Capture stopped-path frontiers for article experiments #373

Description

@CaelmBleidd

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.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions