Exact Anytime Arbitrary-Opponent Certificate¶

Purpose and claim boundary¶

src.true_shield.adversarial implements the first theorem-facing certificate path. It is deliberately separate from TruePolicyTransitionShield and the learned WM/OM shield:

transitions come from the raw exact src.joint_graph.common.Graph;
the opponent is allowed to choose any joint opponent action represented by that graph at every state;
the certificate is per focal agent and per episode;
delta_cov = 0 only relative to the serialized exact graph, the matching environment contract, and the graph's declared reset support;
the certified statement starts at reset(). Any WM/OM pretraining prefix is outside its scope.

For a certified reset state and budget p, the checked Bellman invariant gives an eventual unsafe-reachability bound of at most p against arbitrary opponent actions in the finite kernel. This is not a claim about dynamics outside that abstraction or reset states absent from graph.start_keys.

For deterministic matrix games, the graph builder snapshots and steps the live environment, so the graph rows use the simulator transition implementation. The stochastic gridworld builders currently call separate pure successor functions. Their configuration is now bound and their rows are checked strictly, but a gridworld should be described as certified relative to the serialized graph until its successor function has an exhaustive equivalence audit or is shared directly with the simulator. In the retained paper suite, Bertrand and Chicken are therefore the primary simulator-bound cases; Pursuit-2 is useful as a boundary diagnostic rather than evidence of simulator equivalence.

Outer kernel¶

compile_exact_adversarial_outer_kernel(...) keeps one sparse row for each (s, a_i, a_-i). It never multiplies by an opponent policy and never uses the opp_prob or prob edge fields. The robust action backup is

R_beta(s, a_i) = max_{a_-i} sum_s' P(s' | s, a_i, a_-i) beta(s')
T beta(s)       = min_{a_i} R_beta(s, a_i).

Opponent tuples are segmented rows, not synthetic shield “levels”. A missing opponent tuple makes that focal action demand risk 1. Missing probability mass within a present row is also sent to the implicit unsafe sink. Negative or non-finite probabilities are rejected; mass above one is rejected beyond the small representation allowance.

Exact graph generation rejects negative, non-finite, and excess probability mass and never renormalizes a deficient successor distribution. The compiler sends any deficit to the implicit unsafe sink. The vectorized solver first computes the largest robust invariant safe set, then runs lower/upper reachability iteration. A build is rejected unless the lower/upper gap converges. The final float vector is closed upward against exact rational evaluations of the serialized decimal probabilities.

Independent validation¶

validate_exact_adversarial_certificate(...) uses a deliberately slow nested loop over raw graph edges rather than the vectorized compiler or synthesis risk routine. It checks:

graph, public-state encoding, unsafe-label, and environment-config hashes;
finite/non-negative probability rows and excess/missing mass handling;
complete focal/opponent action groups;
finite beta values in [0, 1] and beta=1 on unsafe states;
every stored exact action-risk fraction, action mask, row ID, and worst-case opponent witness;
the robust Bellman inequality T beta <= beta with Fraction arithmetic;
equality between the certificate reset support and graph.start_keys;
support membership and beta(reset) <= p_shield for every reset key.

Certificate NumPy arrays are copied and made read-only. The official runtime factory recomputes the environment contract and unsafe labels, revalidates the persisted certificate against the raw graph, and checks agent order and every Discrete action-space size before constructing the wrapper. Runtime state encoding accepts only exact finite binary values and compares the bits with the stored graph node after key lookup.

solver_converged and certificate_inductive are separate report fields. A non-converged or non-inductive artifact is rejected. An inductive artifact can still have status infeasible when its reset risk exceeds the requested budget; retaining that result is useful for negative controls.

Reset metadata distinguishes deterministic, exhaustively enumerated, sampled, and conditional supports. Feasible artifacts with incomplete or unknown reset support use certified_on_declared_reset_support; only a complete support uses the unqualified certified status. Both runtimes reject an undeclared reset.

Artifact and runtime contract¶

The opt-in notebook diagnostic writes:

exports/<family>/<environment>/true_shield/exact_anytime/
  certificate.pkl
  report.json

The report records status, scope, reset support and risks, p_total, p_shield, delta_cov, graph sizes/hashes, solver and validator versions, wall-clock diagnostic time, and training_environment_steps=0.

After the Bertrand, Chicken, and two-agent Pursuit reports exist, render the paper tables without manually copying fields:

uv run python scripts/summarize_exact_anytime_diagnostics.py \
  --exports-root exports \
  --require-complete

This writes anytime_certificate_results.tex, anytime_certificate_costs.tex, and a combined JSON provenance record beneath exports/reports/exact_anytime/. The certificate table reports audit status, worst declared-reset risk, and Bellman residual; the cost table reports graph size, cache state, graph time, synthesis-plus-audit time, solver iterations, and the zero RL-training-step count. It intentionally excludes the separate evaluation-only shield harness.

ExactAdversarialTransitionShield is the strict runtime consumer. It starts each episode at q=p_shield, admits an action only by exact rational comparison against the precomputed robust action risk, and then sets q_next=beta(next_state). There is no positive admissibility tolerance. An optional ActionScorer only ranks actions after the safety mask is fixed; it cannot make an unsafe action admissible. The wrapper refuses an infeasible certificate, an undeclared reset, or a reached state outside the graph. It also implements the trainer's action_mask(agent) and last_executed_actions contracts and streams decisions into EpisodeLog through record_shield_step(...).

Notebook switch and cost¶

Every standard environment experiment notebook exposes run_exact_anytime_diagnostic=False. Enabling it builds or reuses the exact graph, solves and validates the certificate, and writes the report. It does not initialize PPO, collect RL rollouts, or retrain a policy. On a cache hit the cost is certificate synthesis plus validation; on a miss, exact graph enumeration can dominate.

This is intentionally an offline audit first. Evaluation with a saved policy can use make_exact_anytime_shielded_env_factory(...); a full shielded PPO retraining condition should only be added if the offline certificate is feasible and the paper needs reward results under the strict shield.

evaluate_exact_anytime_policies(...) is the lean evaluation-only path for already reconstructed policy adapters. It performs no updates, exports one aggregate row per episode plus a summary, and retains no per-transition trace. The summary includes unsafe episodes, override rate, maximum runtime residual, minimum margin, return, steps, and evaluation time.

Environment routing¶

Environment	Reporting value	Guidance
Bertrand, Chicken	High, very cheap	Primary retained positive certificate table; tiny exact graphs and clear safety fallbacks.
Inspection	High, very cheap	Useful if the retired environment is restored; otherwise keep outside the active paper table.
Congestion	High	Useful if the retired environment is restored. Start with 2 agents; larger agent counts make exact joint graphs grow rapidly.
DPGG	Medium-high	Modest exact graph and useful additional matrix-game result; inspect whether the robust value is non-trivial.
Ice Duel	High diagnostic value, not yet a primary guarantee	Exercises multi-successor rows. Its stochastic game can expose an upper/lower value-iteration plateau; include it in a guarantee table only when the report is `certified`.
Pursuit	High as a negative control	Report infeasibility if arbitrary opponent motion defeats the reset budget; larger agent counts also stress graph memory.
Gathering	Conditional	Run only with reset support appropriate to the claim. The default exact builder samples starts; use complete start enumeration before claiming coverage over all resets.
Markov Stag Hunt	Conditional and expensive	The exact builder samples reset states and the reachable graph can be large. Treat it as an engineering audit until reset-support coverage is established.

Matrix games may produce mostly 0/1 certificates. The stochastic unit case in tests/test_true_shield.py supplies a checked non-trivial value and budget propagation path. Ice Duel is a useful next integration target, but is not a substitute unless its environment report actually converges and is certified.

The current lower/upper solver detects a numerical fixed-point stall and emits an invalid diagnostic rather than looping to vi_max_iterations. This occurs for stochastic games whose ordinary bounded value iteration needs end-component deflation. The retained coarse upper vector may be inductive, but solver_converged=false means it is rejected by the runtime and must not be reported as the theorem guarantee. A future Ice Duel certificate should add a formally checked deflation or strategy-iteration step, not weaken this gate.

Deliberate exclusions¶

This version does not assign statistical coverage to learned transitions. The existing shield_credible_* fields describe posterior opponent-level tails; they are not delta_cov. A later learned-model theorem path should reserve p_shield = p_total - delta_cov and attach a time-uniform transition coverage event without changing the exact certificate's meaning.