|
| 1 | +import Init.Data.Rat.Basic |
| 2 | + |
| 3 | +/-! |
| 4 | +# PX4 `BlockLimitSym` — Formal Verification |
| 5 | +
|
| 6 | +🔬 *Lean Squad automated formal verification.* |
| 7 | +
|
| 8 | +This file models and proves correctness properties of PX4's symmetric |
| 9 | +clamp/saturation block `BlockLimitSym`: |
| 10 | +
|
| 11 | +- **C++ source**: `src/lib/controllib/BlockLimitSym.cpp` (lines 47–57) and |
| 12 | + `src/lib/controllib/BlockLimitSym.hpp` (lines 63–73) |
| 13 | +
|
| 14 | +## C++ Source |
| 15 | +
|
| 16 | +```cpp |
| 17 | +float BlockLimitSym::update(float input) |
| 18 | +{ |
| 19 | + if (input > getMax()) { |
| 20 | + input = _max.get(); |
| 21 | + } else if (input < -getMax()) { |
| 22 | + input = -getMax(); |
| 23 | + } |
| 24 | + return input; |
| 25 | +} |
| 26 | +``` |
| 27 | +
|
| 28 | +## Model |
| 29 | +
|
| 30 | +Over `Rat` (exact rational arithmetic), the pure functional model of `update` is: |
| 31 | +
|
| 32 | +``` |
| 33 | +limitSym(input, max) = |
| 34 | + if input > max then max |
| 35 | + if input < -max then -max |
| 36 | + otherwise input |
| 37 | +``` |
| 38 | +
|
| 39 | +**Abstracted away**: The `_max` parameter object, the `Block` hierarchy, and |
| 40 | +floating-point rounding. The Lean model captures the pure numeric behaviour. |
| 41 | +The C++ implementation assumes `max ≥ 0` (always the case in practice); |
| 42 | +several theorems require this hypothesis. |
| 43 | +
|
| 44 | +## Properties Proved (10 theorems, 0 sorry) |
| 45 | +
|
| 46 | +1. `limitSym_above` — input above max → output = max |
| 47 | +2. `limitSym_below` — input below −max → output = −max (requires max ≥ 0) |
| 48 | +3. `limitSym_in_range` — input in [−max, max] → output = input (pass-through) |
| 49 | +4. `limitSym_upper` — output ≤ max (requires max ≥ 0) |
| 50 | +5. `limitSym_lower` — −max ≤ output (requires max ≥ 0) |
| 51 | +6. `limitSym_range` — −max ≤ output ≤ max (combined, requires max ≥ 0) |
| 52 | +7. `limitSym_idempotent` — applying twice = applying once (requires max ≥ 0) |
| 53 | +8. `limitSym_zero` — limitSym 0 max = 0 when max ≥ 0 |
| 54 | +9. `limitSym_sym` — limitSym (−x) max = −(limitSym x max) (odd function, requires max ≥ 0) |
| 55 | +10. `limitSym_mono` — monotone in input (requires max ≥ 0) |
| 56 | +-/ |
| 57 | + |
| 58 | +namespace PX4.BlockLimitSym |
| 59 | + |
| 60 | +def limitSym (input max : Rat) : Rat := |
| 61 | + if input > max then max |
| 62 | + else if input < -max then -max |
| 63 | + else input |
| 64 | + |
| 65 | +theorem limitSym_above (input max : Rat) (h : input > max) : |
| 66 | + limitSym input max = max := by |
| 67 | + unfold limitSym; rw [if_pos h] |
| 68 | + |
| 69 | +theorem limitSym_below (input max : Rat) (hmax : 0 ≤ max) (h : input < -max) : |
| 70 | + limitSym input max = -max := by |
| 71 | + unfold limitSym |
| 72 | + rw [if_neg (Rat.not_lt.mpr (Rat.le_trans (Rat.le_of_lt h) |
| 73 | + (Rat.le_trans (Rat.neg_le_iff.mp hmax) hmax))), |
| 74 | + if_pos h] |
| 75 | + |
| 76 | +theorem limitSym_in_range (input max : Rat) (h1 : -max ≤ input) (h2 : input ≤ max) : |
| 77 | + limitSym input max = input := by |
| 78 | + unfold limitSym |
| 79 | + rw [if_neg (Rat.not_lt.mpr h2), if_neg (Rat.not_lt.mpr h1)] |
| 80 | + |
| 81 | +theorem limitSym_upper (input max : Rat) (hmax : 0 ≤ max) : limitSym input max ≤ max := by |
| 82 | + unfold limitSym |
| 83 | + by_cases h1 : input > max |
| 84 | + · rw [if_pos h1]; exact Rat.le_refl |
| 85 | + · by_cases h2 : input < -max |
| 86 | + · rw [if_neg h1, if_pos h2]; exact Rat.le_trans (Rat.neg_le_iff.mp hmax) hmax |
| 87 | + · rw [if_neg h1, if_neg h2]; exact Rat.not_lt.mp h1 |
| 88 | + |
| 89 | +theorem limitSym_lower (input max : Rat) (hmax : 0 ≤ max) : -max ≤ limitSym input max := by |
| 90 | + unfold limitSym |
| 91 | + by_cases h1 : input > max |
| 92 | + · rw [if_pos h1]; exact Rat.le_trans (Rat.neg_le_iff.mp hmax) hmax |
| 93 | + · by_cases h2 : input < -max |
| 94 | + · rw [if_neg h1, if_pos h2]; exact Rat.le_refl |
| 95 | + · rw [if_neg h1, if_neg h2]; exact Rat.not_lt.mp h2 |
| 96 | + |
| 97 | +theorem limitSym_range (input max : Rat) (hmax : 0 ≤ max) : |
| 98 | + -max ≤ limitSym input max ∧ limitSym input max ≤ max := |
| 99 | + ⟨limitSym_lower input max hmax, limitSym_upper input max hmax⟩ |
| 100 | + |
| 101 | +theorem limitSym_idempotent (input max : Rat) (hmax : 0 ≤ max) : |
| 102 | + limitSym (limitSym input max) max = limitSym input max := |
| 103 | + limitSym_in_range _ _ (limitSym_lower input max hmax) (limitSym_upper input max hmax) |
| 104 | + |
| 105 | +theorem limitSym_zero (max : Rat) (hmax : 0 ≤ max) : limitSym 0 max = 0 := |
| 106 | + limitSym_in_range 0 max (Rat.neg_le_iff.mp hmax) hmax |
| 107 | + |
| 108 | +/-- `limitSym` is an odd function: `limitSym (-x) max = -(limitSym x max)`. |
| 109 | +
|
| 110 | + The positive and negative saturation boundaries are symmetric about zero. -/ |
| 111 | +theorem limitSym_sym (x max : Rat) (hmax : 0 ≤ max) : |
| 112 | + limitSym (-x) max = -(limitSym x max) := by |
| 113 | + unfold limitSym |
| 114 | + by_cases h1 : x > max |
| 115 | + · have h2 : -x < -max := Rat.neg_lt_neg h1 |
| 116 | + have hno : ¬ (-x) > max := |
| 117 | + Rat.not_lt.mpr (Rat.le_trans (Rat.le_of_lt h2) |
| 118 | + (Rat.le_trans (Rat.neg_le_iff.mp hmax) hmax)) |
| 119 | + rw [if_pos h1, if_neg hno, if_pos h2] |
| 120 | + · by_cases h2 : x < -max |
| 121 | + · have h3 : max < -x := by |
| 122 | + have := Rat.neg_lt_neg h2 |
| 123 | + rw [show -(-max) = max from Rat.neg_neg max] at this; exact this |
| 124 | + rw [if_neg h1, if_pos h2, if_pos h3] |
| 125 | + exact (Rat.neg_neg max).symm |
| 126 | + · have hnx_hi : -x ≤ max := Rat.neg_le_iff.mpr (Rat.not_lt.mp h2) |
| 127 | + have hnx_lo : -max ≤ -x := Rat.neg_le_neg (Rat.not_lt.mp h1) |
| 128 | + rw [if_neg h1, if_neg h2, |
| 129 | + if_neg (Rat.not_lt.mpr hnx_hi), if_neg (Rat.not_lt.mpr hnx_lo)] |
| 130 | + |
| 131 | +/-- `limitSym` is monotone in its input. |
| 132 | +
|
| 133 | + Saturation is a non-decreasing operation: larger inputs produce outputs |
| 134 | + that are at least as large. -/ |
| 135 | +theorem limitSym_mono (a b max : Rat) (hmax : 0 ≤ max) (h : a ≤ b) : |
| 136 | + limitSym a max ≤ limitSym b max := by |
| 137 | + unfold limitSym |
| 138 | + by_cases ha1 : a > max |
| 139 | + · rw [if_pos ha1] |
| 140 | + by_cases hb1 : b > max |
| 141 | + · rw [if_pos hb1]; exact Rat.le_refl |
| 142 | + · exact absurd (Std.lt_of_lt_of_le ha1 h) hb1 |
| 143 | + · by_cases ha2 : a < -max |
| 144 | + · rw [if_neg ha1, if_pos ha2] |
| 145 | + by_cases hb1 : b > max |
| 146 | + · rw [if_pos hb1]; exact Rat.le_trans (Rat.neg_le_iff.mp hmax) hmax |
| 147 | + · by_cases hb2 : b < -max |
| 148 | + · rw [if_neg hb1, if_pos hb2]; exact Rat.le_refl |
| 149 | + · rw [if_neg hb1, if_neg hb2]; exact Rat.not_lt.mp hb2 |
| 150 | + · rw [if_neg ha1, if_neg ha2] |
| 151 | + by_cases hb1 : b > max |
| 152 | + · rw [if_pos hb1]; exact Rat.not_lt.mp ha1 |
| 153 | + · by_cases hb2 : b < -max |
| 154 | + · exact absurd (Std.lt_of_lt_of_le hb2 (Rat.not_lt.mp ha2)) (Rat.not_lt.mpr h) |
| 155 | + · rw [if_neg hb1, if_neg hb2]; exact h |
| 156 | + |
| 157 | +end PX4.BlockLimitSym |
0 commit comments