prodigy.analysis.lowerbounds¶

Modules

`egcalc`	Exact generating-function calculus over a fixed product denominator.
`explicit`	Explicit-state semantics of loop-free statements of the intermediate representation, on measures given as dicts `state tuple -> weight` (exact `fractions.Fraction` or `float`), and a sparse Kleene iteration for loops.
`ir`	Translation of pGCL programs (the AST of prodigy.pgcl) into the small intermediate representation used by the exact generating-function calculus of `prodigy.analysis.lowerbounds.egcalc`.
`parameters`	Automatic choice of template parameters (rates, periods, tail starts) for the LP synthesis of EVT sub- and superinvariants.
`problem`	A single-loop program split into the parts used by the lower-bound modes: the loop-free prefix (which determines the initial measure `g` of the loop), the loop, and the loop-free epilogue with its queries.
`sandwich`	Sandwich bounds for the output distribution of a loop: an exactly verified finite-mass EVT sub-invariant (lower induction) bounds the output distribution from below, an exactly verified EVT super-invariant (Park induction) from above.
`subinvariant`	Verification of user-provided EVT sub-invariants (lower induction).
`synthesis`	Synthesis of EVT (occupation) sub- and superinvariants with eventually geometric templates by linear programming, with exact rational certificates.