Reference · Algorithm guarantees

rainbow.algorithms.proofs.odd-monitor

Algorithm guaranteessrc/rainbow/algorithms/proofs/odd_monitor.clj1 definitions, 1 theorems

Operational Design Domain (ODD) monitoring over exact rationals (AHoF V59). An ODD is a multi-dimensional operating envelope -- here a 2-D box [lo1,hi1] x [lo2,hi2]. The monitor accepts an operating point (x1, x2) exactly when it lies inside the box on BOTH dimensions, i.e. the four-way conjunction in-odd? = (lo1<=x1) AND (x1<=hi1) AND (lo2<=x2) AND (x2<=hi2) built as nested boolean ANDs (logic/if-data over Bool) of the exact-rational order decisions. A single out-of-range coordinate takes the point outside the ODD, which is exactly the runtime-monitor alarm condition. Proved native and axiom-free: the membership decision as the four-way conjunction, with its unfold theorem. Requires audit/decide-nnrat-at-most, logic/if-data (both in the D63 checkpoint). Scope (measured by the kernel): this module has 1 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.odd-monitor` prints this classification.

monitor/in-odd? :
  (x₁ x₂ x₃ x₄ x₅ x₆ : ℚ≥0)
  → data/Bool

monitor/in-odd-unfold :
  (lo1 hi1 x1 lo2 hi2 x2 : ℚ≥0)
  → monitor/in-odd? lo1 hi1 x1 lo2 hi2 x2 = logic/if-data data/Bool (data₁ = data₁) (data₁) (data) data/false
  where data := logic/if-data data/Bool (audit/decide-nnrat-at-most lo2 x2 = audit/decide-nnrat-at-most lo2 x2) (audit/decide-nnrat-at-most lo2 x2) (audit/decide-nnrat-at-most x2 hi2) data/false
  where data₁ := logic/if-data data/Bool (audit/decide-nnrat-at-most lo1 x1 = audit/decide-nnrat-at-most lo1 x1) (audit/decide-nnrat-at-most lo1 x1) (audit/decide-nnrat-at-most x1 hi1) data/false