prodigy.analysis.loop_strategies

Loop strategies (registry)

A loop strategy tells the forward analysis how to deal with one while loop: unroll it a fixed number of times, check a user-provided invariant, synthesise an EVT invariant, and so on. Up to now the strategy and its parameters were asked for interactively inside WhileHandler.

This module makes strategies explicit data:

  • ParamSpec describes one parameter (type, label, legacy CLI prompt, default).

  • LoopStrategy describes one strategy (stable name, menu text, parameters, nominal soundness) and points to the function that runs it.

  • LoopTask is what a strategy receives: the loop, the incoming distribution and a way to read its parameters (from the session’s decisions, or interactively).

  • LoopOutcome is what a strategy returns: the outgoing distribution plus what is known about it (exact, lower bound with residual mass, upper bound, unknown) and a certificate that a front end can display or re-check.

Strategies are registered by name, so additional strategies (for example from the lower-bounds work) appear in the CLI menu, the JSON API and the web GUI without touching those front ends: call register_loop_strategy() at import time.

class Bound[source]

Bases: object

What is known about a distribution computed by (part of) an analysis.

The values are compared to the exact semantics of the program:

  • EXACT: equal to the exact semantics (certified).

  • LOWER: coefficient-wise below the exact semantics; the mass that is not accounted for is at most the recorded residual mass. No termination assumption.

  • UPPER: coefficient-wise above the exact semantics (Park’s lemma).

  • UNKNOWN: an approximation without a guaranteed direction, or a result whose side conditions could not be checked.

EXACT = 'exact'
LOWER = 'lower'
UPPER = 'upper'
UNKNOWN = 'unknown'
ALL = ('exact', 'lower', 'upper', 'unknown')
static combine(first, second)[source]

Kind of a composition of two analysis steps (sequential or parallel).

Parameters:
Return type:

str

class ParamSpec(name, kind, label, prompt='', default=None, help='', minimum=None, choices=(), alias_of=None, optional=False)[source]

Bases: object

One parameter of a loop strategy.

Parameters:
name: str

Key in LoopDecision.params.

kind: str

One of int, probability, pgcl (program source), expression (generating-function expression), file (path, CLI only), choice.

label: str

Short label for forms.

prompt: str = ''

Prompt used by the interactive CLI (kept identical to the historic prompts).

default: Any = None

Default used by non-interactive front ends when the parameter is missing.

help: str = ''

One-sentence explanation for forms and --help texts.

minimum: int | None = None

Lower bound for int parameters.

choices: Tuple[str, ...] = ()

Allowed values for choice parameters.

alias_of: str | None = None

If set, this parameter is an alternative way to provide alias_of (e.g. an invariant file instead of the invariant source).

optional: bool = False

Optional parameters are never asked for; if missing, default (or None) is used.

parse(raw)[source]
Parameters:

raw (Any)

Return type:

Any

to_json()[source]
Return type:

Dict[str, Any]

class LoopOutcome(distribution, error_prob, kind='unknown', residual=0, certificate=dict(), messages=list(), query_bounds=dict())[source]

Bases: object

Result of running a loop strategy once.

Parameters:
distribution: Distribution
error_prob: Distribution
kind: str = 'unknown'
residual: Any = 0

upper bound on the mass that is not accounted for, in the units of the incoming distribution (i.e. before any later normalisation).

Type:

For LOWER

certificate: Dict[str, Any]
messages: List[str]
query_bounds: Dict[Tuple[str, str], Tuple[Any, Any]]

Bounds that the strategy computed itself for the queries directly after the loop, as (kind, expression) -> (lower, upper) with kind "?Pr" or "?Ex" and None for an unknown side. They refer to the incoming distribution of the loop and tighten the intervals of exactly these queries (e.g. the upper bounds of an EVT super-invariant).

class LoopTask(instruction, prog_info, distribution, error_prob, config, analyzer, session, loop, decision, strategy, record=None)[source]

Bases: object

Everything a strategy needs to analyse one occurrence of a loop.

Parameters:
instruction: WhileInstr
prog_info: ProgramInfo
distribution: Distribution
error_prob: Distribution
config: ForwardAnalysisConfig
analyzer: Callable[[SkipInstr | AbortInstr | WhileInstr | IfInstr | AsgnInstr | ChoiceInstr | LoopInstr | TickInstr | ObserveInstr | QueryInstr | ProbabilityQueryInstr | ExpectationInstr | PlotInstr | PrintInstr | OptimizationQuery | Sequence[SkipInstr | AbortInstr | WhileInstr | IfInstr | AsgnInstr | ChoiceInstr | LoopInstr | TickInstr | ObserveInstr | QueryInstr | ProbabilityQueryInstr | ExpectationInstr | PlotInstr | PrintInstr | OptimizationQuery], ProgramInfo, Distribution, Distribution, ForwardAnalysisConfig], Tuple[Distribution, Distribution]]
session: AnalysisSession
loop: LoopInfo | None
decision: LoopDecision
strategy: LoopStrategy
record: Any = None

The session’s LoopRecord for this loop.

param(name)[source]

Value of parameter name: from the decision if present, otherwise from the session’s decision provider (asks on the terminal in the interactive CLI, uses the default or reports a missing decision elsewhere).

Parameters:

name (str)

Return type:

Any

progress(done, total, message='')[source]
Parameters:
Return type:

None

note(message)[source]
Parameters:

message (str)

Return type:

None

property interactive: bool
class LoopStrategy(name, title, menu_text, soundness, description, run, params=(), legacy_key=None, requires_unconditioned=False)[source]

Bases: object

A registered way of analysing a while loop.

Parameters:
name: str

Stable identifier used in JSON decisions and on the command line.

title: str

Short title for menus and forms.

menu_text: str

Text of the entry in the interactive CLI menu.

soundness: str

Nominal guarantee (see Bound); the actual outcome may be weaker, e.g. when a side condition cannot be checked.

description: str

A few sentences for help texts and the GUI.

run: Callable[[LoopTask], LoopOutcome]
params: Tuple[ParamSpec, ...] = ()
legacy_key: str | None = None

Number of the entry in the historic CLI menu ("1" … "6").

requires_unconditioned: bool = False

True if the strategy cannot handle observe statements before or inside the loop.

param(name)[source]
Parameters:

name (str)

Return type:

ParamSpec

to_json()[source]
Return type:

Dict[str, Any]

register_loop_strategy(strategy, *, replace=False)[source]

Makes strategy available to the CLI menu, the JSON API and the web GUI.

Parameters:
Return type:

LoopStrategy

loop_strategies()[source]

All registered strategies; the six historic ones first, in menu order.

Return type:

List[LoopStrategy]

get_loop_strategy(name)[source]
Parameters:

name (str)

Return type:

LoopStrategy