# Reachability

Continuous-mode verification for the PWR_HYBRID_3 hybrid controller.

## Soundness status: APPROXIMATE

The current `reach_operation.m` result is **not a sound reach tube for
the physical plant**.  It is a sound over-approximation of the
*linearized* closed-loop system (A_cl = A - BK around x_op) under
bounded disturbance.  The linear model is itself an approximation of
the nonlinear plant (`../plant-model/pke_th_rhs.m`), and that
approximation error is not currently bounded or inflated into the tube.

Two paths to upgrade to a sound result:

1. **Nonlinear reach directly** — CORA `nonlinearSys`, JuliaReach
   `BlackBoxContinuousSystem`, or equivalent.  More expensive but the
   honest answer.
2. **Linear reach + Taylor-remainder inflation** — compute an upper
   bound on `||f_nl(x, u) - (A x + B u)||` over the reach set (via
   Hessian norm estimate on each component of `f_nl`) and inflate the
   linear tube by that bound.  Less expensive, still rigorous.

Both are thesis-blocking for any safety claim.  Deferred only until
the per-mode plumbing is solid; it is not a "nice to have".

The current 5-orders-of-margin buffer (reach envelope ~0.03 K against
a 5 K safety band) means linearization error would have to be huge to
invalidate the conclusion, but that is vibes, not a proof.

## Related open issues

- **Saturation semantics.** `ctrl_heatup.m` uses `sat(u, u_min, u_max)`.
  Saturation is formally a 3-mode piecewise-affine system.  For
  heatup reach this has to be handled as (a) hybrid locations, or
  (b) proven dormant via reach on `u_unsat`.  Not modeled in the
  current artifacts (operation-mode LQR saturation is dormant in
  practice but the proof is implicit).
- **Parametric uncertainty in α_f, α_c.**  Real plants have α drift
  with burnup (~20%), boron (α_c ranges 10×), xenon.  The
  feedback-linearization in `ctrl_heatup.m` assumes exact α; a robust
  treatment would make α an interval and propagate parametric reach.
  Currently idealized — flag in the chapter.

## What's here

**Per-mode only.** Following the compositionality argument in the thesis:
verify each continuous mode separately, let the DRC handle discrete
switching. Current focus: **operation mode** under LQR feedback.

## What's here

- `linearization_at_op.mat` — A, B, B_w and reference point, generated by
  `../plant-model/test_linearize.m`.
- `reach_linear.m` — box-zonotope propagation of the closed-loop linear
  model under bounded disturbance. Pure MATLAB, no external toolbox.
- `barrier_lyapunov.m` — Lyapunov-ellipsoid barrier certificate for the
  closed-loop linear system. Solves a Lyapunov equation, reports the
  smallest sub-level set containing the initial set and closed under
  the disturbance.
- `reach_operation.m` — end-to-end operation-mode reach: linearize at
  x_op, compute LQR gain, propagate zonotope reach set, check against
  the `t_avg_in_range` predicate.
- `figures/` — generated plots.

## Running

From MATLAB:

```matlab
cd reachability
reach_operation     % computes reach set + plots
barrier_lyapunov    % solves Lyapunov, reports invariant ellipsoid
```

## Tool choice

Currently using a hand-rolled zonotope reach because:
- Avoids a ~0.5 GB CORA install for a first-pass result.
- Linear reach with bounded disturbance has a clean analytic form
  (matrix exponential on the state, integral of e^(A(t-s))·B_w·w ds
  for the disturbance).
- Stays inside MATLAB, which is where the plant model lives.

If we need nonlinear reach (and we will, for non-LQR controllers or
larger reach sets where linearization error matters), the planned
options are CORA (MATLAB) or JuliaReach (port the plant to Julia).

## What this does NOT do yet

- Any sound reach tube (see top of this file).
- Nonlinear reach for the original P controller on operation.
- Heatup reach (ramped reference makes x* time-varying — needs
  trajectory-LQR or a different formulation, and the saturation
  semantics need to be made explicit).
- Shutdown, scram, initialization reach.
- Hybrid-system level verification (mode switching validity).
- Parametric robustness to α_f, α_c drift.