Shielding API¶

Compile one shield bundle, optionally over a certified ambiguity set.

joint_row_radius attaches a total-variation radius to each joint row of the transition graph, as produced by src.shield.ambiguity.counts_row_radius from an empirical count table. Radii are marginalised through each level's opponent policy before value iteration, so the shield certifies against a statistically valid kernel set rather than a point estimate.

Leaving it None is the default and reproduces the point-estimate bundle exactly. The radius must be centred on the same empirical kernel the confidence sequence was computed from; centring a coverage claim on a neural kernel would not follow from that sequence.

Return bundle with padded floor bounds and padding_radius = radius.

The floor bounds become the padded certificate at every floor, iterated from above until no state moves by tol; every iterate is a super-solution, so each state with budget at least its value keeps an admissible action. Radius 0 returns the bundle unchanged.

sup of E_P[values] over the TV ball of radius on support.

Moves at most radius of mass from the lowest-value support entries into a highest-value one (the same transport as tv_ball_sup).

_robust_egalitarian_fill with the padded inequality.

Raises every successor still below one by a common amount, as large as keeps max_l sup_{B_r(P_l)} E[W] <= budget, and repeats as entries reach one. The padded cost is non-decreasing in the common shift, so bisection finds it. Every accepted shift keeps the padded cost within budget exactly; eps only stops the loop early, which leaves W lower and so is always safe.

Project a proposed point on an action edge into every level constraint.

The returned distribution is (1-x) e_i + x e_j. Unlike masking the two endpoints separately, intersecting the level-wise intervals can retain a mixture whose endpoints violate different robust constraints.

Safely project learned raw budget logits along their proposed direction.

Max-min additive successor-budget fill under every level constraint.

Compute sound lower/upper bounds on the minimal probability of eventually reaching the unsafe set U.

Conservative modeling: any missing transition mass is sent to an absorbing unsafe sink (value 1), ensuring over-approximation for the upper bound.

Then both bounds are iterated monotonically until the sup-norm gap between them is within tol, or max_iter is reached.

row_radius optionally attaches a total-variation ambiguity set to each (state, action) row, turning the Bellman step into its robust counterpart:

acc_upper = sup_{P : TV(P, P_hat) <= eps} E_P[upper_q]
acc_lower = inf_{P : TV(P, P_hat) <= eps} E_P[lower_q]

The set lives on the row's certified support, which is the enumerated successors plus the unsafe sink only when the row genuinely carries missing mass; W_max is taken over that support and never hard-coded to one. robust_mode="exact" uses two-ended transport, "bound" the conservative closed form. row_radius=None is the default and reproduces the point-estimate iteration exactly.

Note that max_gap changes meaning once a radius is active. Without one, the two bounds converge to a common value and the gap is a numerical residual. With one, they are the fixed points of two different operators, so the gap is the certified interval width and does not close; iteration then stops when each bound stops moving.

Label graph nodes through a labelled environment's safety model.

Label graph nodes with an explicit environment safety abstraction.

Largest safe set W such that every state in W has at least one action whose full support stays inside W and has no missing transition mass.

These are the states from which the controller can stay safe almost surely, so their minimal reachability to unsafe is exactly zero. Every successor of mass above support_tol (default zero) is support; mass_tol only absorbs the floating-point deficit of a normalised row.

Return the pointwise tail-mass allowance for an OM observation count.

summable allocates a total error budget using 6 * delta / (pi^2 * (t + 1)^2). fixed retains the same pointwise allowance and therefore has no time-uniform infinite-horizon guarantee.

Resolve the largest monotone floor retaining 1 - credible_delta mass.

Compile (s, a_i, a_-i) rows without marginalizing opponents.

Synthesize and independently validate an exact arbitrary-opponent certificate.

Audit the artifact with a slow raw-edge implementation.

Time-uniform TV radius from Weissman's :math:L_1 bound.

Pr(||P_hat_n - P||_1 >= eps) <= (2^m - 2) exp(-n eps^2 / 2), inverted at the summable schedule and halved to convert :math:L_1 to total variation.

Time-uniform TV radius from per-category empirical-Bernstein deviations.

Each category gets an empirical-Bernstein bound at the summable schedule with the row budget split support_size ways; the per-category deviations are summed to bound :math:\lVert \hat P - P \rVert_1 and halved.

This is much tighter than :func:weissman_tv_radius on near-deterministic rows, where the empirical variance is close to zero — and near-deterministic rows are the common case in these environments.

Split a chosen coverage budget uniformly across state-action rows.

delta_cov = 0 is permitted and meaningful: it asks for a certificate that makes no probabilistic claim, so only structurally certain rows are certified and every other row is the whole simplex. On a graph whose rows all have singleton support this recovers the exact certificate at the full budget p_shield = p_total, which is what such a graph should use — spending coverage budget there lowers the deployed budget and buys nothing.

sup_{P in U} E_P[values] by exact two-ended transport.

O(k log k). Returns the nominal expectation when radius is zero.

Solve and report feasibility of the count-centred robust shield.

The deployed budget is p_shield = p_total - delta_cov: the coverage budget is paid once, up front, not per step. A negative remainder means the coverage budget alone exhausts the risk budget, which is infeasible by construction rather than by the dynamics.

Per-row TV between two compiled bundles over the same levels and actions.

Rows are matched by state key; a state missing from learned is skipped and counted. Also reports exact-support entries absent from the learned row, which no radius can cover.

min_{sigma in simplex} max_l sigma . costs[l, s, :] for every state s.

costs has shape (levels, states, actions). The minimax is a linear programme whose optimal vertices mix at most levels actions with the mixed actions' level costs tied, so enumerating pure actions, pairs tied on two levels and triples tied on three is exact for up to three levels. Each candidate is scored by its own worst level, so every returned value is attained by a feasible mixture.

Sound upper and lower iterates of the pure and the mixed robust operators.

Upper iterates start from one and lower iterates from zero, with unsafe states fixed at one and almost-surely-safe states at zero (a mixture is almost surely safe only if each of its actions is). Upper iterates are rounded outward and stay super-solutions, so they are inductive certificates; lower iterates stay sub-solutions, so they bound the least fixed points from below.

Upper bound on ||beta_pure - beta_mix||_inf, over states if given.

Next-state law of the focal action under the opponents' actual (independent) laws.

opponent_laws are the other agents' action distributions in agent order with the focal agent removed. Returns the successor law and the opponent probability mass whose joint row the graph does not contain (treated by callers as unsafe).

E_P[W] with W = 1 off the certificate's listed successors, and that off-list mass.