prodigy.analysis.lowerbounds.subinvariant

Verification of user-provided EVT sub-invariants (lower induction).

For a loop while (G) { B } with input distribution g and Phi_g(nu) = g + [[B]](<nu>_G):

if   nu >= 0,   nu <= Phi_g(nu)  (coefficient-wise)   and   |nu| = nu(1, ..., 1) < inf,
then <nu>_{not G} <= [[while (G) { B }]](g)   and   |[[loop]](g)| - |<nu>_{not G}| <= |Phi_g(nu)| - |nu|.

No termination assumption is needed. Phi_g(nu) is computed with Prodigy’s own forward semantics. The coefficient-wise sign conditions are decided exactly when the generating functions have product denominators prod_i (1 - r_i X_i^{p_i}) (finite positivity check); otherwise Prodigy’s positivity heuristics are used and the result may be inconclusive.

to_product_form(expr, variables)[source]

Write a rational generating function as P / prod_i (1 - r_i X_i^{p_i}) (at most one factor per variable, r_i >= 0), or return None if this is not possible.

Parameters:
Return type:

Tuple[Dict[Tuple[int, ...], Fraction], Denominator] | None

nonneg_by_construction(expr_str, variables)[source]

Sufficient criterion for non-negative coefficients: the expression is P / prod_i Q_i^k_i where P has non-negative coefficients and every Q_i = c_i - R_i has a constant c_i > 0 and R_i non-negative coefficients, as 1/(c - R) = sum_n R^n / c^(n+1). Covers denominators that are not products of univariate factors, e.g. x*y/(1 - 9/50*(x + y)).

Parameters:
Return type:

bool

decide_nonneg(expr_str, variables, config)[source]

Coefficient-wise nonnegativity: exact for product denominators, then a sufficient criterion for rational functions, otherwise Prodigy’s heuristics.

Parameters:
Return type:

Tuple[bool | None, str]

exact_mass(expr_str, variables)[source]
Parameters:
rational_mass(expr_str, variables)[source]

Total mass of a rational generating function with NONNEGATIVE coefficients, or None if the closed form is not rational. Let f(t) = F(t, ..., t) in lowest terms. By Pringsheim’s theorem, the radius of convergence of f is its smallest pole on the positive real axis; hence the mass sum of coefficients = lim_{t -> 1-} f(t) is infinite iff f has a pole in (0, 1], and equals f(1) otherwise. Evaluating the closed form at 1 directly is unsound: (1 + X)/(1 - 2X) = 1 + 3X + 6X^2 + ... evaluates to -2.

Parameters:
evt_subinvariant_verification(loop, prog_info, distribution, invariant, config, analyzer, details=None)[source]

Verify an EVT sub-invariant nu of finite mass and return the lower bound <nu>_{not G} on the output distribution of the loop (raises VerificationError if the conditions cannot be established).

details, if given, receives mass (|nu|), gap (|Phi(nu)| - |nu|, which bounds the mass that the lower bound misses), exit_mass and how non-negativity was established (nonneg_nu, nonneg_gap).

Parameters:
Return type:

Distribution