Reference · Algorithm guarantees

rainbow.algorithms.proofs.failure-probability-monitor

Algorithm guaranteessrc/rainbow/algorithms/proofs/failure_probability_monitor.clj2 definitions, 2 theorems

Runtime failure-probability monitoring over exact rationals (AHoF V64). An online estimator maintains a failure-probability estimate p; the monitor declares the system SAFE while p stays at or below a risk threshold tau, and raises an ALARM exactly when it does not: safe? p tau = decide (p <= tau) alarm? p tau = NOT (safe? p tau) (boolean negation via logic/if-data) over exact rationals. The alarm is the boolean complement of the safety test, so every observation either keeps the system safe or trips the alarm. Proved native and axiom-free: the safety decision and the alarm as its negation, each with an unfold theorem. The online importance-sampling update of p is executable; what is proved is the threshold decision and its complement. Requires audit/decide-nnrat-at-most, logic/if-data (both in the D63 checkpoint). Scope (measured by the kernel): this module has 2 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.failure-probability-monitor` prints this classification.

failmon/safe? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

failmon/alarm? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

failmon/safe-unfold :
  (p tau : ℚ≥0)
  → failmon/safe? p tau = audit/decide-nnrat-at-most p tau

failmon/alarm-unfold :
  (p tau : ℚ≥0)
  → failmon/alarm? p tau = logic/if-data data/Bool (failmon/safe? p tau = failmon/safe? p tau) (failmon/safe? p tau) data/false data/true