prodigy.analysis.lowerbounds.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. Both certificates are synthesised by linear programming over eventually geometric templates (prodigy.analysis.lowerbounds.synthesis) with automatically chosen or user-given template parameters.

Soundness does not depend on termination: for a lower certificate nu <= Phi_g(nu) with |nu| < inf we have [not guard] nu <= Post (lower induction), and for an upper certificate Phi_g(I) <= I we have Post <= [not guard] I (Park). The loop-free code after the loop is a positive linear operator and maps lower (upper) bounds to lower (upper) bounds.

class QueryBound(query, lower, upper)[source]¶

Bases: object

Parameters:

query (Query)
lower (object)
upper (object)

query: Query¶

lower: object¶

upper: object¶

to_json()[source]¶

Return type:: dict

class SandwichResult(problem, lower, upper, bounds, mass_bounds, time_total, plan=None, attempts=list(), per_query=dict())[source]¶

Bases: object

Parameters:

problem (LoopProblem)
lower (Certificate | None)
upper (Certificate | None)
bounds (List[QueryBound])
mass_bounds (tuple)
time_total (float)
plan (ParameterPlan | None)
attempts (List[dict])
per_query (dict)

problem: LoopProblem¶

lower: Certificate | None¶

upper: Certificate | None¶

bounds: List[QueryBound]¶

mass_bounds: tuple¶

time_total: float¶

plan: ParameterPlan | None = None¶

attempts: List[dict]¶

per_query: dict¶

to_json()[source]¶

Return type:: dict

synthesize_lower(problem, shapes, verbose=False, attempts=None)[source]¶

Parameters:

problem (LoopProblem)
shapes (Sequence[TemplateShape])
verbose (bool)
attempts (list | None)

Return type:

Certificate | None

upper_objective(lp, problem, objective)[source]¶

Parameters:

lp (TemplateLP)
problem (LoopProblem)
objective (str)

synthesize_upper(problem, shapes, objective='auto', verbose=False, attempts=None, stop_after_first=False)[source]¶

Parameters:

problem (LoopProblem)
shapes (Sequence[TemplateShape])
objective (str)
verbose (bool)
attempts (list | None)
stop_after_first (bool)

Return type:

Certificate | None

refine_upper_per_query(problem, upper, verbose=False)[source]¶

Re-solve the LP of the best upper certificate once per event A and not A of every ?Pr query, minimising U(A) (useful when the total exit mass of the upper certificate is infinite).

Parameters:

problem (LoopProblem)
upper (Certificate)
verbose (bool)

Return type:

Dict[tuple, Certificate]

query_bounds(problem, lower, upper, per_query=None)[source]¶

Bounds on the queries of the program from the two certificates (after the epilogue).

For an event A with L(A) <= Post(A) <= U(A) (and likewise for the complement) and |Post| <= |g|: Post(A) >= max(L(A), |L| - U(not A)) and Post(A) <= min(U(A), min(|U|, |g|) - L(not A)). Normalised probabilities Post(A) / |Post| are increasing in Post(A) and decreasing in Post(not A).

Parameters:

problem (LoopProblem)
lower (Certificate | None)
upper (Certificate | None)
per_query (Dict[tuple, Certificate] | None)

evt_sandwich(problem, lower_shapes=None, upper_shapes=None, size=1200, objective='auto', with_upper=True, verbose=True, per_query=None)[source]¶

Synthesise and verify lower and upper certificates and compute bounds for the queries.

Parameters:

problem (LoopProblem)
lower_shapes (Sequence[TemplateShape] | None)
upper_shapes (Sequence[TemplateShape] | None)
size (int)
objective (str)
with_upper (bool)
verbose (bool)
per_query (bool | None)

Return type:

SandwichResult

print_result(res, show_certificates=False)[source]¶

Parameters:

res (SandwichResult)
show_certificates (bool)

write_json(res, path)[source]¶

Parameters:

res (SandwichResult)
path (str)