SOS Barrier Certificate

What goes wrong with a naive approach

The frame-budget problem has two interacting state variables — say, $x_1$ (smoothed frame-time error) and $x_2$ (integrator accumulation) — and an “admissible region” where the PI controller is provably safe, plus an “unsafe region” where degradation must fire regardless of what the controller says.

A hand-drawn boundary — say, an ellipse — is easy to code but either too loose (triggers degradation when the controller could recover) or too tight (fails to degrade when the integrator is about to wind up). The real admissible region is shaped by the plant dynamics and is decidedly nonlinear.

A principled solution treats the region as the sublevel set of a Lyapunov-style barrier function $B(x_1, x_2)$ that is:

• Positive on the safe side — $B(x) > 0$ when the state is recoverable.
• Non-positive on the unsafe side — $B(x) \le 0$ triggers degradation.
• Cheap to evaluate online — no iterative solver on the frame loop.

The last two constraints rule out generic NLP solvers and suggest polynomial barriers — they are fast to evaluate and their certification is a well-studied SDP problem called sum-of-squares optimization.

Mental model

Pick a polynomial form:

Set up the certification constraint in SOS form: $B$ is non-negative on the safe region and its Lie derivative along the plant dynamics is non-positive on the boundary. This is an SDP whose solution produces the coefficients $c_{ij}$.

Offline: solve once in Python. Online: evaluate a 28-term polynomial per frame. The B(x) > 0 check becomes a constant-time sign test.

The math

Barrier form

Degree-at-most-6 polynomial in two variables:

28 coefficients total (monomials $1, x_1, x_2, x_1^2, x_1 x_2, x_2^2, \ldots, x_1^6, x_1^5 x_2, \ldots, x_2^6$ with constraint $i + j \le 6$).

SOS formulation

Express $B$ and its Lie derivative $\dot{B} = \nabla B \cdot f(x)$ as sums of squares over a monomial basis $m(x)$:

The feasibility SDP is:

Solved offline with scripts/solve_sos_barrier.py (using picos or cvxpy with an SDP backend).

Online evaluation

Runtime evaluates the polynomial with Horner-style nesting:

// B(x1, x2) with coefficients c_ij from the SDP
let mut s = 0.0;
for &(i, j, c) in COEFFS {
    s += c * x1.powi(i) * x2.powi(j);
}
// s > 0  -> safe
// s <= 0 -> trigger degradation

No allocations, no branches, constant time.

Why polynomial barriers instead of MPC or reachability?

- Optimises an explicit horizon; needs a plant model and a QP solver.
- Runtime cost per frame: O(horizon · state) solve.
- No formal safety guarantee outside the horizon.

- Samples random trajectories to estimate reachable set.
- Probabilistic guarantee only; conservative.
- Not tractable inside the frame loop.

- Offline SDP certifies B(x) > 0 → state stays admissible.
- Online: O(28) polynomial eval. Constant time.
- Deterministic safety guarantee wherever the certificate is valid.

Rust interface

use ftui_runtime::sos_barrier::{SosBarrier, BARRIER_COEFFS};
 
let barrier = SosBarrier::new(&BARRIER_COEFFS);
 
let safe = barrier.evaluate(x1, x2) > 0.0;
if !safe {
    degradation.trigger("sos_barrier_breach");
}

BARRIER_COEFFS lives in crates/ftui-runtime/src/sos_barrier_coeffs.rs and is regenerated by:

python scripts/solve_sos_barrier.py --output crates/ftui-runtime/src/sos_barrier_coeffs.rs

Rerun whenever you change the plant model (PI gains, budget, or degradation tiers).

How to debug

Barrier values travel alongside degradation_event emissions. When the barrier flips sign, the reason field records sos_barrier_breach:

{"schema":"degradation_event","decision":"step_down",
 "reason":"sos_barrier_breach",
 "x1":0.62,"x2":-1.12,"barrier_value":-0.04,
 "level_before":"Full","level_after":"SimpleBorders"}

FTUI_EVIDENCE_SINK=/tmp/ftui.jsonl cargo run -p ftui-demo-showcase
 
# Visualise barrier sign across the run:
jq -c 'select(.schema=="degradation_event" and .reason=="sos_barrier_breach")
       | [.x1, .x2, .barrier_value]' /tmp/ftui.jsonl

Plotting the (x1, x2, sign(B)) cloud in a notebook gives a direct view of how close the controller is travelling to the certified boundary.

Pitfalls

Cross-references

• Control theory — the PI controller whose admissible region this barrier certifies.
• /operations/frame-budget — how the barrier interacts with conformal gating and degradation.
• scripts/solve_sos_barrier.py in the repository — the offline SDP that produces the coefficients.

Where next