pyfcstm.verify

Public API for verification algorithms, metadata, and inspect gating.

The top-level package exports the core raw verification algorithms so callers do not need to know the internal pyfcstm.verify.algorithms module layout. Use this module as the stable import surface for raw verification entry points, algorithm metadata, and inspect eligibility helpers.

Module map:

Area

Public entry

Purpose

Raw algorithms

dead_guard(), effect_no_op_under_guard(), transition_shadowed_by_predecessor()

Run one precise verification check and return AlgorithmResult.

Registry

REGISTRY

Store VerifyAlgorithmMeta for every implemented or planned verification algorithm.

Inspect gating

eligible_for_inspect(), iter_inspect_eligible()

Decide which raw algorithms may be used by automatic inspect workflows.

Inspect execution

InspectRunResult, run_inspect_algorithms()

Execute inspect-eligible algorithms and preserve normalized raw results for later diagnostics conversion.

Taxonomy

VerifyAlgorithmMeta and the Literal aliases

Describe algorithm complexity, theory, scope, and fallback risk.

Internal encoding

pyfcstm.verify.encoding

Shared FCSTM-to-SMT encoding helpers used by algorithm implementations; callers normally should not import this package directly.

Examples:

>>> from pyfcstm.verify import REGISTRY, dead_guard
>>> # The public top-level algorithm is the same callable registered here.
>>> REGISTRY["dead_guard"].impl is dead_guard
True

__all__

pyfcstm.verify.__all__ = ['CALL_COUNT_SCALING_ORDER', 'COMPLEXITY_TIER_ORDER', 'REGISTRY', 'AlgorithmResult', 'CallCountScaling', 'Closedness', 'ComplexityTier', 'FallbackUnknownRisk', 'FormulaSizeScaling', 'InspectAccessForbiddenError', 'InspectRunResult', 'SMTLogic', 'ResultKind', 'VerificationScope', 'VerifyAlgorithmMeta', 'composite_init_guards_incomplete', 'dead_guard', 'effect_contradicts_guard', 'effect_no_op_under_guard', 'enter_postcondition_implies_during_precondition', 'eligible_for_inspect', 'forced_guard_unsat_under_init', 'guard_tautology', 'iter_inspect_eligible', 'run_inspect_algorithms', 'transition_shadowed_by_predecessor']

Built-in mutable sequence.

If no argument is given, the constructor creates a new empty list. The argument must be an iterable if specified.