Multi-session work bundle on a draft branch. Splits into a clean
sequence of commits later; pushed here so it isn't lost on a reboot.
Reach work
- code/scripts/reach/reach_scram_pj.jl: shutdown_margin halfspace
X_exit (replaces "n <= 1e-4 AND T_f bound" framing); per-step
envelope extraction added.
- code/scripts/reach/reach_scram_pj_fat.jl: per-step envelope
extraction added; shutdown_margin discharge logic mirrored from the
tight scram script. 3 probes (10/30/60s) all discharge from the
fat union polytope.
- code/scripts/reach/reach_scram_full_fat.jl (NEW): full nonlinear
PKE scram reach with fat entry. Hits the stiffness wall at
~1.5 s plant time as expected; saves NaN-tolerant per-step
envelopes. Demonstrates concretely why PJ is the right tool for
the longer-horizon proof.
- code/scripts/reach/reach_heatup_pj.jl: T_REF_START_C constant
(entry-conditioned ramp) replaces T_STANDBY-init that was making
the FL controller command cooling at t=0. Per-step extraction
already in place.
- code/configs/heatup/tight.toml: bumped maxsteps; probe horizon
parameterized.
Hot-standby SOS barrier
- code/scripts/barrier/barrier_sos_2d_shutdown.jl (NEW): mirrors the
operation SOS machinery on the hot-standby thermal projection.
Includes the eps-slack pattern (so feasibility doesn't silently
collapse to B == 0).
- code/scripts/barrier/barrier_sos_2d.jl: refactored to use the same
helper.
- code/src/sos_barrier.jl (NEW): solve_sos_barrier_2d helper module
factoring out the SOS construction; eps-slack with eps_cap=1.0 to
avoid unbounded primal.
Library
- code/src/pke_states.jl (NEW): single source of truth for canonical
initial-condition vectors per DRC mode (op, shutdown, heatup) keyed
off plant + predicates.
- code/scripts/sim/{main_mode_sweep,validate_pj}.jl, code/CLAUDE.md:
migrated to pke_states.
Predicates + invariants
- reachability/predicates.json: new shutdown_margin predicate (1%
dk/k tech-spec floor, expressed as alpha_f*T_f + alpha_c*T_c
halfspace). Used as scram X_exit.
Plot script
- code/scripts/plot/plot_reach_tubes.jl: plot_tubes_scram_pj() with
variant=:fat|:tight knob; plot_tubes_scram_full() for full-PKE
3-panel (T_c, T_f, rho); plot_tubes_heatup_pj() reads results/
not reachability/.
Journal + memory
- journal/entries/2026-04-27-shutdown-sos-and-scram-X_exit.tex (NEW):
long-form entry on the SOS hot-standby barrier and the scram X_exit
refactor.
- journal/journal.tex: input chain updated.
- claude_memory/ — three new session notes:
* 2026-04-27-scram-X_exit-shutdown-margin.md
* 2026-04-28-DICE-2026-conference-intel.md (people, sessions,
strategic notes for the May 12 talk)
* 2026-04-28-path1-sos-pj-sketch.md (sketch of nonlinear-SOS via
polynomial multiply-through; saved for an overnight session)
Docs
- docs/model_cheatsheet.md (NEW): one-page reference of state vector,
dynamics, constants, modes, predicates, sanity numbers — the talk
prep cheatsheet Dane asked for.
- docs/figures/reach_*_tubes.png: regenerated with the new mat data.
- presentations/prelim-presentation/outline.md: revised arc per the
April-28 review pass (cuts: Lyapunov-fails standalone slide,
operation-tube standalone slide, SOS standalone; adds: scopes-of-
control framing, scram on the headline result slide).
- app/predicate_explorer.jl: minor.
Hacker-Split: end-of-session scratch bundle
Scram PJ reach from the bounding-box union of:
- hot-standby box (mode_boundaries.q_shutdown)
- heatup-tight reach envelope (results/reach_heatup_pj_tight.mat)
- operation-LQR reach envelope (results/reach_operation_result.mat)
- LOCA operation envelope (results/reach_loca_operation.mat, 3s)
with precursor + temperature outliers clamped to physical bounds.
Results at probe horizons:
T=10s: 10890 sets in 480s wall — n ∈ [-8e-4, 0.047] T_c [231, 362]
T=30s: 16925 sets in 2892s wall — n ∈ [-4e-4, 0.021] T_c [229, 361]
T=60s: 23919 sets in 705s wall — n ∈ [-2e-4, 0.009] T_c [226, 359]
Monotone n decay, factor-of-5-per-minute even from the wide union.
This is the defensible scram-obligation version: starts from anywhere
the plant could plausibly be (including LOCA-perturbed operation
state), proves n decays. X_exit(scram)=n≤1e-4 still not reached in
60s — same T_max-vs-plant-decay mismatch previously flagged.
Fixed: missing Printf import that had failed the summary block on the
first run (results still computed correctly, just the final print
errored; the matwrite is after the print so the mat file wasn't
saved on that run).
Journal entry for 2026-04-21 extended with the fat-entry result +
the LOCA-reach 3s-horizon numerical-looseness apass. 38 pages.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Morning-review items 2 and 3.
Point 2 (scram X_entry expansion):
- reach_loca_operation.jl: LQR reach under Q_sg widened to
[0, 1.5*P_0] (steam-line break envelope) for 3 s horizon.
Longer horizons cause numerical blowup in the box-hull
reach propagator due to slow precursor modes amplifying
under large disturbance — documented in the script.
- reach_scram_pj_fat.jl: computes bounding-box union of
hot-standby + heatup-tight + operation + LOCA reach
envelopes, clamps obvious numerical outliers on precursors
and temperatures, builds a fat X_entry(scram), runs scram
PJ reach. Result pending (TMJets compiling).
Point 3 (heatup steam-dump Q_sg):
- configs/heatup/with_steam_dump.toml: Q_sg ∈ [0, 0.05·P_0]
as bounded parameter.
- reach_heatup_pj_sd.jl: 12-state RHS with x[10]=Q_sg (dx=0,
augmented bounded param) and x[11]=t. Running in
background.
Tight-entry heatup via the new TOML-config reach_heatup_pj.jl
reproduces the previous all-6-halfspaces-discharged result
(300s horizon, T_c envelope [281.05, 291.0]). Refactor
preserves semantics.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Architecture restructure from morning review:
1. code/scripts/ subdivided into sim/, reach/, barrier/, plot/.
Easier nav; `barrier/` is the natural place for SOS scale-up scripts.
2. Heatup PJ reach variants consolidated behind TOML configs.
reach_heatup_pj.jl now takes `--config path/to/config.toml`;
configs/heatup/baseline.toml (wide entry, from predicates.json) and
configs/heatup/tight.toml (narrow entry, reproduces all-6-halfspaces
discharged result). Old reach_heatup_pj_tight.jl and
reach_heatup_pj_tight_full.jl deleted (superseded).
3. Reach output .mat files moved from reachability/ to results/.
reachability/ now = specs + docs; results/ = ephemeral outputs
(gitignored *.mat). README added.
4. OVERNIGHT_NOTES.md archived to claude_memory/2026-04-20-21-overnight-
session-summary.md (date range in the filename makes the history clearer).
All include() / Pkg.activate() paths in scripts updated for the new
depth. Smoke tests pass (reach_operation.jl generates its .mat in
the new results/ location; sim_sanity.jl matches MATLAB).
Presentation outline for the 20-min prelim talk landed in
presentations/prelim-presentation/outline.md. 14-slide assertion-
evidence format targeting OT-informed cybersecurity audience. Each
slide: one declarative assertion + one figure. Outline includes
which figures already exist and which need to be created, timing
checkpoints, cybersecurity angle to emphasize, and Q&A prep.
New config configs/heatup/with_steam_dump.toml + its companion
scripts/reach/reach_heatup_pj_sd.jl (12-state RHS with Q_sg as an
augmented bounded parameter x[10] and time as x[11]). Kicks off
point 3 from morning review.
Next up: scram X_entry expansion (morning point 2) — LOCA scenario
+ union of mode reach envelopes.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Dane Sabo