Expand description
The coding operational safety barrier (PSP-9 system 12).
A narrow, useful barrier rather than a pretend solution to semantic
correctness: versioned policy channels h_j(x) ∈ [0, ∞) whose unsafe
boundary is 1, with h(x) = max_j h_j(x) and the exact deterministic
increment c_t = max(0, h(x') − h(x)). Correctness evidence — compiler
errors, test failures — stays in V and is never duplicated into h.
The old shortcut “deterministic transition, therefore c_c = 0” is
prohibited: read-only effects get c_t = 0 by measurement (no channel
moves), not by declaration.
Structs§
- Operational
Safety Barrier - The versioned channel set for the coding domain.