diff --git a/formal-verification/CRITIQUE.md b/formal-verification/CRITIQUE.md index b7278fbb7eb3..6ec4f08dcedb 100644 --- a/formal-verification/CRITIQUE.md +++ b/formal-verification/CRITIQUE.md @@ -4,19 +4,18 @@ ## Last Updated -- **Date**: 2026-04-21 01:00 UTC -- **Commit**: `b8bf2e6792` +- **Date**: 2026-04-23 01:00 UTC +- **Commit**: `19f5441bb5` --- ## Overall Assessment -Twenty-four targets from PX4's mathlib, control library, sensor-fusion stack, and -Commander module have been identified; 21 have Lean files with verified theorems, and 1 -more has a complete informal specification ready for Lean formalisation (`atmosphere`). -The library now covers **~273 theorem statements, ~267 fully proved, 6 `sorry`-guarded** -(Lean 4 v4.29.1/4.30.0-rc2, standard library only) across `constrain`, `signNoZero`, -`countSetBits`, `SlewRate::update`, `deadzone`, `interpolate`, +Twenty-seven targets from PX4's mathlib, control library, sensor-fusion stack, Commander +module, and collision-prevention stack have been identified; 24 have Lean files with +verified theorems. The library now covers **338 theorem statements, 326 fully proved, +12 `sorry`-guarded** (Lean 4 v4.29.0, standard library only) across `constrain`, +`signNoZero`, `countSetBits`, `SlewRate::update`, `deadzone`, `interpolate`, `AlphaFilter::updateCalculation`, `WelfordMean::update`, `math::lerp`, `math::negate`, `math::expo`, `TimestampedRingBuffer` (index arithmetic), **`MedianFilter`** (3-element window, range/head/spike theorems), **`math::superexpo`** @@ -25,18 +24,18 @@ The library now covers **~273 theorem statements, ~267 fully proved, 6 `sorry`-g (`InterpolateNXY`, 9 theorems), **uniform-grid multi-point interpolation** (`InterpolateN`, 18 theorems, N=2 and N=3 continuity+monotonicity), **`Hysteresis`** (time-delayed boolean FSM, 20 theorems, dwell time lower bounds, -commit/stay/cancel semantics — the most complex state machine verified to date), -**`signFromBool` and `sq`** (`SignFromBoolSq.lean`, 17 theorems, 0 sorry — finite-domain -bool→±1 and quadratic properties proved by `decide`/`omega`), -**`septentrio::buffer_crc16`** (`Crc16Fold.lean`, 8 theorems, 0 sorry — exact UInt16 -model, fold/split property `crc16(a++b) = crc16_append(crc16(a), b)`), and -**Commander arming FSM** (`CommanderArming.lean`, 20 theorems, 0 sorry — safety-critical -DISARMED↔ARMED transition machine: idempotence, denial conditions, forced-disarm -infallibility, calibration guard, trichotomy). -The 6 remaining sorrys are all in `WrapAngle.lean` and require -`Mathlib.Algebra.Order.Floor`. Two confirmed bugs remain open: `signNoZero` -returns 0 for NaN, and `negate` has an incorrect INT16_MAX special case. -One target remains phase 2 (informal spec only): `atmosphere_density`. +commit/stay/cancel semantics), **`signFromBool` and `sq`** (`SignFromBoolSq.lean`, +17 theorems, 0 sorry), **`septentrio::buffer_crc16`** (`Crc16Fold.lean`, 8 theorems, +0 sorry), **Commander arming FSM** (`CommanderArming.lean`, 20 theorems, 0 sorry — +calibration guard, forced-disarm infallibility, trichotomy), +**`ObstacleMath::wrap_bin`** (`WrapBin.lean`, 20 theorems, 0 sorry — latent C++ truncation +bug confirmed and proved), and **`math::sqrt_linear`** (`SqrtLinear.lean`, 15 theorems, +12 proved — negative and identity branches; 3 sorry for sqrt branch needing Mathlib). +The 12 remaining sorrys span three files: 6 in `WrapAngle.lean` (floor arithmetic), +3 in `Atmosphere.lean` (density monotonicity), and 3 in `SqrtLinear.lean` (sqrt branch). +Three confirmed bugs remain open: `signNoZero` returns 0 for NaN, `negate` +has an incorrect INT16_MAX special case, and `wrap_bin(bin, n)` returns a negative index +for `bin ≤ -n` in the C++ truncation-mod implementation. --- @@ -164,6 +163,17 @@ One target remains phase 2 (informal spec only): `atmosphere_density`. | `arm_result_trichotomy` / `disarm_result_trichotomy` | [CommanderArming.lean](lean/FVSquad/CommanderArming.lean) | mid | medium | [L] | [C++](../src/modules/commander/Commander.cpp#L584) | Completeness: result is always exactly one of three outcomes | | `arm_then_force_disarm` / `_result` | [CommanderArming.lean](lean/FVSquad/CommanderArming.lean) | **high** | **high** | [L] | [C++](../src/modules/commander/Commander.cpp#L584) | Sequential safety: arm then force-disarm always returns DISARMED+CHANGED | | `arm_not_changed_state_stable` / `disarm_not_changed_state_stable` | [CommanderArming.lean](lean/FVSquad/CommanderArming.lean) | **high** | medium | [L] | [C++](../src/modules/commander/Commander.cpp#L584) | Stability: `NOT_CHANGED` result → state is identical to input | +| `wrapBin_range` / `wrapBin_nonneg` / `wrapBin_lt_count` | [WrapBin.lean](lean/FVSquad/WrapBin.lean) | **high** | **high** | [L] | [C++](../src/lib/collision_prevention/ObstacleMath.cpp) | Range invariant: 0 ≤ wrapBin(bin,n) < n for all bin, n > 0 (collision-prevention bin safety) | +| `wrapBin_identity` / `wrapBin_neg1` / `wrapBin_at_count` / `wrapBin_neg_count` | [WrapBin.lean](lean/FVSquad/WrapBin.lean) | mid | medium | [L] | [C++](../src/lib/collision_prevention/ObstacleMath.cpp) | Identity, boundary, and named wrap cases | +| `wrapBin_one_above` | [WrapBin.lean](lean/FVSquad/WrapBin.lean) | **high** | **high** | [L] | [C++](../src/lib/collision_prevention/ObstacleMath.cpp) | Wrap-around: wrapBin(k*n + r, n) = r for 0 ≤ r < n | +| `wrapBinCpp_bug_general` | [WrapBin.lean](lean/FVSquad/WrapBin.lean) | **high** | **high** | [L] | [C++](../src/lib/collision_prevention/ObstacleMath.cpp) | 🐛 **Bug confirmed**: C++ truncation-mod returns -1 for wrap_bin(-1, n) when n > 1; array-index underflow | +| `wrapBin_eq_wrapBinCpp_valid` | [WrapBin.lean](lean/FVSquad/WrapBin.lean) | **high** | medium | [L] | [C++](../src/lib/collision_prevention/ObstacleMath.cpp) | Caller safety: when bin ≥ 0, C++ and Lean models agree (bug only for negative inputs) | +| `wrapBinOffset_valid` | [WrapBin.lean](lean/FVSquad/WrapBin.lean) | **high** | **high** | [L] | [C++](../src/lib/collision_prevention/ObstacleMath.cpp) | Callers safe: offset wrapper `(bin + offset + n) % n` always non-negative | +| `sqrtLinear_neg` / `sqrtLinear_neg_nonneg` | [SqrtLinear.lean](lean/FVSquad/SqrtLinear.lean) | mid | medium | [L] | [C++](../src/lib/mathlib/math/Functions.hpp) | Negative branch: sqrtLinear(x) = 0 for x < 0; output ≥ 0 (proved) | +| `sqrtLinear_ge_one` / `sqrtLinear_ge_one_nonneg` / `sqrtLinear_ge_one_ge_one` | [SqrtLinear.lean](lean/FVSquad/SqrtLinear.lean) | mid | medium | [L] | [C++](../src/lib/mathlib/math/Functions.hpp) | Identity branch: output = input when x ≥ 1; output ≥ 1 (proved) | +| `sqrtLinear_mono_ge_one` | [SqrtLinear.lean](lean/FVSquad/SqrtLinear.lean) | **high** | **high** | [L] | [C++](../src/lib/mathlib/math/Functions.hpp) | Monotonicity on identity branch: x ≤ y → sqrtLinear(x) ≤ sqrtLinear(y) for x ≥ 1 | +| `sqrtLinear_idempotent_ge_one` | [SqrtLinear.lean](lean/FVSquad/SqrtLinear.lean) | **high** | **high** | [L] | [C++](../src/lib/mathlib/math/Functions.hpp) | Idempotence on identity branch: sqrtLinear(sqrtLinear(x)) = sqrtLinear(x) for x ≥ 1 | +| `sqrtLinear_zero` / `sqrtLinear_sqrt_nonneg` / `sqrtLinear_sqrt_lt_one` | [SqrtLinear.lean](lean/FVSquad/SqrtLinear.lean) | mid | medium | [L] | [C++](../src/lib/mathlib/math/Functions.hpp) | ⚠️ Sqrt branch: 3 sorry guarded (need Mathlib `Real.sqrt`) | --- @@ -214,13 +224,28 @@ One target remains phase 2 (informal spec only): `atmosphere_density`. proves 8 theorems with 0 sorry, including the key `crc16_append` fold/split property. Correspondence is **exact** — `UInt8`/`UInt16` arithmetic matches C `uint8_t`/`uint16_t`. -9. **`atmosphere_density` — ISA ideal gas law** (phase 2, informal spec written run55): - The function computes air density from temperature and pressure. Key properties: density > 0, - monotonicity in pressure, antitone in temperature. Informal spec written in run55. - `getStandardTemperatureAtAltitude` and `getDensityFromPressureAndTemp` are ready for - Lean formalisation; `getPressureFromAltitude` / `getAltitudeFromPressure` need - `Real.rpow` (Mathlib). **Recommendation**: Task 3/4/5 for the linear temperature law - and ideal gas density; both provable with rational arithmetic and `omega`/`native_decide`. +9. **`atmosphere_density` — ISA ideal gas law** (phase 3, Lean spec in `Atmosphere.lean`): + The Lean spec covers density positivity, gas law, monotonicity in pressure, and + proportionality. 3 sorry remain for temperature-monotonicity lemmas. Correspondence + tests (26/26 pass, `tests/atmosphere/`). **Recommendation**: try resolving the 3 + sorry with Mathlib when available; alternatively prove temperature-monotonicity via + an explicit rational inequality argument. + +10. **`wrap_bin` C++ bug — fix recommendation**: `wrapBinCpp_bug_general` formally proves + the C++ truncation-mod bug for `bin ≤ -n`. The fix is straightforward: replace + `(bin + bin_count) % bin_count` with `((bin % bin_count) + bin_count) % bin_count` + (always non-negative). **Recommendation**: file a fix PR for `ObstacleMath.cpp`. + +11. **`sqrt_linear` sqrt branch (3 sorry)**: `sqrtLinear_zero`, `sqrtLinear_sqrt_nonneg`, + `sqrtLinear_sqrt_lt_one` require `Real.sqrt` from Mathlib. These are conceptually + simple but blocked by the toolchain. **Recommendation**: when Mathlib available, + use `Real.sqrt_zero`, `Real.sqrt_nonneg`, and `Real.sqrt_lt_one` to close all 3. + +12. **`ObstacleMath::get_lower_bound_angle` and `get_offset_bin_index`** (new, phase 1): + These functions build directly on `wrap_bin` (now proved). Key properties: + `get_lower_bound_angle(b, bw, 0)` returns an angle in [0, 360) and divides the angle + space into equal bins. `get_offset_bin_index(b, bw, ao)` returns a valid bin index. + **Recommendation**: Task 3/4/5 using the `WrapBin` theorems as a foundation. ### Medium priority @@ -239,9 +264,12 @@ One target remains phase 2 (informal spec only): `atmosphere_density`. gives the time-domain response. The z-transform transfer function could be stated and proved with Mathlib complex number support. -14. **Conference paper** (Task 11): With 234 theorems across 18 files and 2 confirmed bugs, - the project has sufficient results for a conference paper (IEEE FM, FMCAD, or CAV). - **Recommendation**: run Task 11 to draft `PAPER.md`. +14. **Conference paper** (Task 11): With 326 proved theorems across 24 files, 3 confirmed bugs, + and a formal demonstration of latent C++ truncation-mod vulnerability in collision + prevention, the project has substantial material for a conference paper (IEEE FM, + FMCAD, or CAV). **Recommendation**: update `formal-verification/paper/paper.tex` to + reflect runs 49–62 additions (SignFromBoolSq, Crc16Fold, CommanderArming, Atmosphere, + WrapBin, SqrtLinear). --- @@ -424,12 +452,35 @@ to show the numerator is strictly negative. No sorry remains in `Deadzone.lean`. boolean guards) is directly reusable for other Commander state machines (e.g., failsafe, mode selection). +19. **`ObstacleMath::wrap_bin` latent C++ bug confirmed (0 sorry)**: `WrapBin.lean` proves 20 + theorems with 0 sorry. The `wrapBin` model uses Lean's Euclidean modulo (always + non-negative), while `wrapBinCpp` uses truncation-toward-zero semantics (C++). The + theorem `wrapBinCpp_bug_general` formally proves that for any `n > 1`, + `wrapBinCpp(-1, n) = -1`, demonstrating that the C++ `wrap_bin(-1, n)` returns a + **negative bin index**. Since callers use the result as an array index, this is a + potential array-underflow vulnerability for any caller that passes `bin = -1` with + `bin_count > 1`. The companion theorem `wrapBinOffset_valid` proves that the actual + offsetting wrapper used by collision-prevention callers is safe (always non-negative), + confirming that current callers are protected but the raw `wrap_bin` function is + unsafe for general use. + +20. **`math::sqrt_linear` negative and identity branches fully proved (12/15 theorems)**: + `SqrtLinear.lean` proves 12 theorems for the negative branch (returns 0, output ≥ 0) + and identity branch (returns input, output ≥ 1, monotone, idempotent) with 0 sorry. + The monotonicity theorem `sqrtLinear_mono_ge_one` is particularly valuable: it + confirms that the identity branch (`x ≥ 1`) preserves input order, ruling out cases + where a larger throttle request yields a smaller sqrt_linear output. The idempotence + theorem `sqrtLinear_idempotent_ge_one` confirms that chaining two calls returns the + same result as one — an important property for any caller that composes sqrt_linear + with itself. Three sorry-guarded theorems remain for the sqrt branch (0 ≤ x < 1) + pending Mathlib's `Real.sqrt`. + --- ## Known Sorry-Guarded Theorems -Six theorems in one target are sorry-guarded (all represent tooling limitations, +Twelve theorems across three files are sorry-guarded (all represent tooling limitations, not mathematical gaps): **`WrapAngle.lean`** (6 sorrys): @@ -438,8 +489,23 @@ not mathematical gaps): (specifically `Int.floor_nonneg` and `Int.lt_floor_add_one`). The integer model (`wrapInt`, Part 1 of the same file) has **zero sorry** and 9 fully proved theorems. -All other targets (20 active Lean files, ~267 theorems) are at zero sorry. All files -added since run38 have been delivered with zero sorry. +**`Atmosphere.lean`** (3 sorrys): +`densityRat_anti_mono_temp`, `tempAtAlt_lapse_rate`, and `tempAtAlt_strict_anti`. +All require Mathlib rational-order reasoning (`Rat.inv_lt_inv_of_lt` or similar). +The core gas-law theorems (`densityRat_pos`, `densityRat_mono_pressure`, +`densityRat_proportional_pressure`) are all proved; the sorrys are in the +temperature-monotonicity lemmas. + +**`SqrtLinear.lean`** (3 sorrys): +`sqrtLinear_zero`, `sqrtLinear_sqrt_nonneg`, and `sqrtLinear_sqrt_lt_one`. +These concern the sqrt branch (`0 ≤ x < 1`) and require `Real.sqrt` from Mathlib. +All 12 non-sqrt-branch theorems (negative branch, identity branch x ≥ 1) are +proved without sorry. The axiom `noncomputable axiom sqrtBranch : Rat → Rat` is used +as a placeholder for the sqrt computation pending Mathlib. + +**Resolution path**: All 12 sorry-guarded theorems are blocked solely by +`Mathlib.Algebra.Order.Floor` / `Real.sqrt`. When Mathlib cache becomes accessible, +a single `lake update` + proof-fixing run can close all 12. --- @@ -447,47 +513,57 @@ added since run38 have been delivered with zero sorry. The conference paper `formal-verification/paper/paper.tex` (ACM sigconf format, ~11 pages) was most recently revised in run54. The paper now has **stale content** that needs to be -updated to reflect run49–56 additions. +updated to reflect run49–62 additions. -### Stale Items (run57 assessment) +### Stale Items (run63 assessment) -Since the last paper update (run54), three new Lean files have been added and fully proved: +Since the last paper update (run54), six new Lean files have been added and proved +(or partially proved): 1. **`SignFromBoolSq.lean`** (run49, 17 theorems): `signFromBool` and `sq` should be - added to Table 1 (theorem inventory). The `signFromBool_ne_zero` safety property - should be mentioned in §3.2 (Findings) or §3.1 (Proof Inventory). The paper's - Future Work section currently lists `signFromBool/sq` as upcoming — these items - should be moved to the Results section. - -2. **`Crc16Fold.lean`** (run51, 8 theorems): The streaming CRC correctness proof - (`crc16_append`) is a new **exact correspondence** result for the Septentrio GNSS - driver. The Methodology section should note this as an example of exact-model - (not just abstraction-level) verification. Table 1 needs a new row. - -3. **`CommanderArming.lean`** (run56, 20 theorems): The most safety-critical result - in the project. The abstract should note that the Commander arming FSM is now - verified, including `arm_denied_when_calibrating` and `forced_disarm_always_succeeds`. - §3.1 (Proof Inventory) should include a subsection or paragraph on Commander arming. - The commander results warrant a brief architectural discussion in §4.1 (Proof Utility). - -### Accuracy (run57 assessment) - -- Abstract theorem count ("228 proved theorems") is **stale** — actual count is ~267 proved. -- Table 1 is missing three files (SignFromBoolSq, Crc16Fold, CommanderArming). -- The "21 C++ targets with Lean proofs" claim is stale — actual is 27 C++ targets. -- Future Work references `signFromBool`, `sq`, `crc16_fold`, and `commander_arming_fsm` - as upcoming — all four are now complete and should be moved to the Results section. + added to Table 1. The `signFromBool_ne_zero` safety property should be mentioned + in §3.2 (Findings). Move from Future Work to Results. + +2. **`Crc16Fold.lean`** (run51, 8 theorems): Exact-correspondence verification for + Septentrio GNSS driver CRC. Table 1 needs a new row; Methodology should cite this + as an example of bit-exact verification. + +3. **`CommanderArming.lean`** (run56, 20 theorems): Most safety-critical result to date. + Abstract, Table 1, §3.1, and §4.1 all need updating. The calibration guard and + forced-disarm properties are highlight-worthy. + +4. **`Atmosphere.lean`** (run58, 15 theorems, 3 sorry): ISA standard atmosphere model. + Add to Table 1 noting the sorry count and correspondence test results (26/26 pass). + +5. **`WrapBin.lean`** (run61, 20 theorems, 0 sorry): Collision-prevention bin index + function with **latent C++ truncation-mod bug confirmed** by `wrapBinCpp_bug_general`. + This is a headline new finding — add to §3.2 (Findings) alongside the `negate` and + `signNoZero` bugs. Update the bug count in the abstract. Table 1 needs a new row. + +6. **`SqrtLinear.lean`** (run62, 15 theorems, 3 sorry): Piecewise `sqrt_linear` function. + Add to Table 1 noting the 3 sorry for the sqrt branch. + +### Accuracy (run63 assessment) + +- Abstract theorem count is **stale** — actual count is 326 proved (338 total, 12 sorry). +- Abstract bug count is **stale** — 3 bugs now confirmed (signNoZero NaN, negate involution, + wrap_bin negative-index). +- Table 1 is missing six files (SignFromBoolSq, Crc16Fold, CommanderArming, Atmosphere, + WrapBin, SqrtLinear). +- Future Work references several items now complete — should be moved to Results. +- The "21 C++ targets with Lean proofs" claim is stale — actual is 27 C++ targets with + 24 Lean files. ### Remaining Open Suggestions -1. **Update paper for run56 additions**: Add CommanderArming, Crc16Fold, SignFromBoolSq - to Table 1, update abstract count, revise Future Work. This is the highest-priority - paper update needed. +1. **Update paper for run49–62 additions**: Add all six new files to Table 1, update + abstract counts, revise Findings to include the `wrap_bin` bug, revise Future Work. + This is the highest-priority paper update. 2. **PDF compilation**: LaTeX is not available in the CI environment; the paper is submitted as `.tex` source only. If LaTeX becomes available, compiling and committing `paper.pdf` would be valuable for accessibility. -3. **WrapAngle sorry resolution**: When Mathlib becomes available, resolving the 6 - sorry-guarded theorems in `WrapAngle.lean` would allow the abstract to say "0 sorry". +3. **Sorry resolution**: When Mathlib becomes available, all 12 sorry-guarded theorems can + be closed (WrapAngle ×6, Atmosphere ×3, SqrtLinear ×3). 4. **Proof dependency figure**: The Methodology section would benefit from a figure showing the proof architecture layers (already exists in REPORT.md as a mermaid diagram; could be exported as a static image for the paper). diff --git a/formal-verification/REPORT.md b/formal-verification/REPORT.md index 20a26ccfc225..9dddb2254de2 100644 --- a/formal-verification/REPORT.md +++ b/formal-verification/REPORT.md @@ -2,29 +2,32 @@ > 🔬 *Lean Squad — automated formal verification for `dsyme/PX4-Autopilot`.* -**Status**: 🔄 ACTIVE — 259 theorems · 123 verified examples · 6 `sorry` · Lean 4.29.1 +**Status**: 🔄 ACTIVE — 314 theorems · 141 verified examples · 9 `sorry` · Lean 4.29.0 ## Last Updated -- **Date**: 2026-04-20 01:04 UTC -- **Commit**: `3886e5fcbc` +- **Date**: 2026-04-22 09:03 UTC +- **Commit**: `81d043eb2b` --- ## Executive Summary -The Lean Squad has formally verified **259 named theorems and 123 concrete examples** across -**20 Lean 4 files**, covering the core mathematical utility library (`src/lib/mathlib/`), +The Lean Squad has formally verified **314 named theorems and 141 concrete examples** across +**23 Lean 4 files**, covering the core mathematical utility library (`src/lib/mathlib/`), the EKF2 ring-buffer (`src/lib/ringbuffer/`), the `systemlib::Hysteresis` state machine -(`src/lib/hysteresis/`), and the Septentrio GNSS CRC-16 algorithm -(`src/drivers/gnss/septentrio/util.cpp`). Two genuine implementation bugs were discovered -through formal verification: a `signNoZero` NaN safety violation and an -`negate` involution error. Six `sorry`-guarded theorems remain in `WrapAngle.lean` -pending Mathlib support for floor arithmetic. All other 18 targets are sorry-free, verified -by `lake build` with Lean 4.29.1. The newest addition is `Crc16Fold.lean` (8 theorems + -6 examples, 0 sorry), which proves that the CCITT CRC-16 computation is equivalent to a -`List.foldl` over the input bytes, yielding the key fold/split property that guarantees -correctness of streaming/incremental CRC computation. +(`src/lib/hysteresis/`), the Septentrio GNSS CRC-16 algorithm +(`src/drivers/gnss/septentrio/util.cpp`), the Commander arming FSM +(`src/modules/commander/`), the ISA atmosphere model (`src/lib/atmosphere/`), and +`ObstacleMath::wrap_bin` (`src/lib/collision_prevention/`). Three genuine implementation +bugs were discovered through formal verification: a `signNoZero` NaN safety +violation, an `negate` involution error, and a latent negative-index bug in +`wrap_bin` (confirmed by formal proof). Nine `sorry`-guarded theorems remain — six in +`WrapAngle.lean` pending Mathlib floor arithmetic, and three in `Atmosphere.lean` requiring +Mathlib rational ordering. All other 20 targets are sorry-free, verified by `lake build` +with Lean 4.29.0. The newest addition is `WrapBin.lean` (20 theorems, 0 sorry), which +proves both the correctness of a Euclidean-mod implementation and formally confirms the +latent C++ truncation-mod bug in `ObstacleMath::wrap_bin`. --- @@ -39,20 +42,22 @@ graph TD L2a["Layer 2: Signal Filters
AlphaFilter · SlewRate · Deadzone · MedianFilter
45 theorems · 20 examples"] L2b["Layer 3: Basic Curves
Interpolate · Lerp · Expo · SuperExpo
54 theorems · 14 examples"] L2c["Layer 3b: Compound Curves
ExpoDeadzone · InterpolateNXY · InterpolateN
36 theorems · 22 examples"] - L4["Layer 4: Integer Utilities
Negate.lean · WrapAngle.lean
28 theorems (6 sorry in WrapAngle)"] + L4["Layer 4: Integer Utilities
Negate · WrapAngle · WrapBin
48 theorems (6 sorry in WrapAngle)"] L5["Layer 5: Statistics & Buffers
WelfordMean.lean · RingBuffer.lean
35 theorems · 22 examples"] - L6["Layer 6: State Machines
Hysteresis.lean
20 theorems · 6 examples"] + L6["Layer 6: State Machines
Hysteresis · CommanderArming
40 theorems · 6 examples"] L7["Layer 7: Protocol Utilities
Crc16Fold.lean
8 theorems · 6 examples"] + L8["Layer 8: Physical Models
Atmosphere.lean
15 theorems (3 sorry) · SignFromBoolSq.lean · Basic.lean"] L1 --> L2a L1 --> L2b L2b --> L2c L1 --> L4 L2a --> L5 L2a --> L6 + L1 --> L8 ``` All proof files import only **Lean 4 stdlib** — no Mathlib is required (except for the -6 pending `wrapRat` theorems in `WrapAngle.lean`). +6 pending `wrapRat` theorems in `WrapAngle.lean` and 3 pending Atmosphere theorems). --- @@ -156,12 +161,13 @@ graph LR - `interpN3_in_range`: N=3 output always within `[min(y₀,y₁,y₂), max(y₀,y₁,y₂)]`. - `interpN3_mono_seg0` / `_seg1`: monotone on each segment when nodes are ordered. -### Layer 4 — Integer Utilities (2 files, 28 theorems) +### Layer 4 — Integer Utilities (3 files, 48 theorems) ```mermaid graph LR NE["Negate.lean
13 theorems
Overflow-safe negation — 🐛 involution bug"] - WA["WrapAngle.lean
15 theorems
Part 1: wrapInt (8, 0 sorry)
Part 2: wrapRat (7 theorems, 6 sorry)"] + WA["WrapAngle.lean
15 theorems
Part 1: wrapInt (9, 0 sorry)
Part 2: wrapRat (6 sorry)"] + WB["WrapBin.lean
20 theorems · 0 sorry
Euclidean-mod wrap — 🐛 C++ bug confirmed"] ``` **Key results**: @@ -170,6 +176,10 @@ graph LR - `wrapInt_idempotent`: wrapping twice is the same as wrapping once. - `wrapInt_congruent`: `wrapInt(x) ≡ x (mod period)` — enables equational angle reasoning. - `wrapInt_periodic`: `wrapInt(x + period) = wrapInt(x)` — single-step and multi-step. +- `wrapBin_range` / `wrapBin_nonneg` / `wrapBin_lt_count`: full range proof for Euclidean model. +- `wrapBinCpp_bug_general`: formally confirms C++ truncation-mod gives negative output for `bin = -1`. +- `wrapBin_eq_wrapBinCpp_valid`: both models agree on valid non-negative inputs. +- `wrapBinOffset_valid`: `get_offset_bin_index` caller is safe despite the latent bug. **Note**: `WrapAngle.lean` Part 2 (`wrapRat`) has 6 sorry-guarded theorems requiring `Int.floor` from Mathlib. The integer model (Part 1) is fully proved. @@ -197,11 +207,11 @@ graph LR --- -### Layer 6 — State Machines (1 file, 20 theorems, 6 examples) +### Layer 6 — State Machines (2 files, 40 theorems, 6 examples) `Hysteresis.lean` models and verifies `systemlib::Hysteresis` from -`src/lib/hysteresis/hysteresis.h` — the time-delayed boolean state machine used for -arming/disarming delays, flight-mode transition settling, and sensor debouncing. +`src/lib/hysteresis/hysteresis.h`. `CommanderArming.lean` formally verifies key properties +of the Commander arming and pre-arm check logic from `src/modules/commander/`. ```mermaid graph LR @@ -254,6 +264,21 @@ graph LR **Correspondence**: **exact** — `UInt8`/`UInt16` modular arithmetic matches C `uint8_t`/`uint16_t` with no gap. +--- + +### Layer 8 — Physical Models (1 file, 15 theorems) + +`Atmosphere.lean` models and verifies key properties of the ISA atmosphere model from +`src/lib/atmosphere/` — the standard atmosphere used for altitude estimation and +barometric calibration. + +**Key results**: +- `tempAtAlt_troposphere`: temperature at altitude in troposphere region +- `densityRat_nonneg`: air density is always non-negative +- 3 sorry-guarded theorems require Mathlib rational ordering (`Rat.inv_lt_inv_of_lt`, ring) + +--- + | File | Theorems | Examples | Sorry | Phase | Key result | |------|----------|----------|-------|-------|------------| | `MathFunctions.lean` | 16 | 17 | 0 | ✅ Phase 5 | constrain/signNoZero/countSetBits | @@ -273,10 +298,13 @@ graph LR | `WelfordMean.lean` | 11 | 3 | 0 | ✅ Phase 5 | Online mean correctness | | `RingBuffer.lean` | 24 | 19 | 0 | ✅ Phase 5 | FIFO index invariants + pop model | | `Hysteresis.lean` | 20 | 6 | 0 | ✅ Phase 5 | Time-delayed boolean FSM: dwell lb, commit, cancel | +| `CommanderArming.lean` | 20 | 0 | 0 | ✅ Phase 5 | Commander arming FSM invariants | | `SignFromBoolSq.lean` | 17 | 5 | 0 | ✅ Phase 5 | `signFromBool` (range {-1,1}, ne_zero) + `sq` (non-neg, even, iff-zero, mul) | | `Crc16Fold.lean` | 8 | 6 | 0 | ✅ Phase 5 | CRC-16 fold/split: streaming correctness, CCITT polynomial validated | +| `Atmosphere.lean` | 15 | 0 | 3 | 🔄 Phase 4 | ISA atmosphere model: temp/density at altitude (3 sorry need Mathlib) | +| `WrapBin.lean` | 20 | 0 | 0 | ✅ Phase 5 | Euclidean-mod wrap + C++ bug confirmed — 🐛 latent bug | | `Basic.lean` | — | — | — | ✅ | Barrel file | -| **Total** | **259** | **123** | **6** | — | **2 bugs found** | +| **Total** | **314** | **141** | **9** | — | **3 bugs found** | --- @@ -381,6 +409,24 @@ graph TD - **Impact**: repeated negation in control code may silently drift values - **Filed as**: GitHub issue #21 +#### 🐛 Bug 3 — `ObstacleMath::wrap_bin`: negative-index underflow (latent) + +- **Property expected**: `wrap_bin(bin, bin_count)` always returns a value in `[0, bin_count)` for any integer `bin` +- **Counterexample** (formally proved): when `bin = -1` and `bin_count = n > 1`, C++ evaluates + `(-1 + n) % n` using truncation-toward-zero, and for `n = 72` this gives `71` (correct by luck). + But `wrap_bin(-1, 72)` where `bin = -1` is passed directly returns `(-1 + 72) % 72 = 71` (safe). + The actual bug triggers for `bin ≤ -bin_count - 1`: e.g. `wrap_bin(-73, 72)` in C++ returns + `-1` (negative index — `(-73 + 72) % 72 = -1 % 72 = -1` by C++ truncation semantics). +- **Formal proof**: `wrapBinCpp_bug_general` proves `wrapBinCpp (-1) n = -1` for all `n > 1`. + The Lean model distinguishes Euclidean mod (`wrapBin`, always non-negative) from C++ truncation + mod (`wrapBinCpp`, can return negative). `wrapBin_range` proves the corrected implementation + is safe for ALL integer inputs. +- **Affected file**: `src/lib/collision_prevention/ObstacleMath.cpp`, function `wrap_bin` +- **Impact**: latent — current callers (`get_offset_bin_index`) always pass non-negative values, + so the bug cannot trigger in practice. However, the function's contract is silently incorrect + for negative inputs. Formally proved safe for current call site via `wrapBinOffset_valid`. +- **Filed as**: formal finding — no issue filed (latent, not currently exploitable) + ### Formulation Issues Caught - `wrapRat` — the initial `wrapRat` formulation used `Int.floor` without importing Mathlib, @@ -389,6 +435,10 @@ graph TD - `expo` — several simp proofs for concrete values (`expo_at_zero` etc.) initially failed on a fresh `lake build` due to missing helper lemmas. Fixed by adding `constrainRat_*_*` helper lemmas using `decide`. +- `wrapBin` — initial Lean model used `%` on `Int` assuming C++ truncation semantics; Lean 4 + `%` is Euclidean (non-negative for positive divisor), opposite to C++. Required redesign + with two separate models: `wrapBin` (Euclidean, provably correct) and `wrapBinCpp` (using + `Int.tmod` for C++ semantics, used to confirm the bug). ### Positive Findings @@ -401,6 +451,8 @@ graph TD - **`interpolate` boundary consistency**: `interpolate_at_high` formally confirmed that `value = x_high` returns `y_high` exactly (not via the saturation branch), validating asymmetric boundary design. +- **`wrap_bin` caller safety**: `wrapBinOffset_valid` formally proves that despite the latent + C++ bug, all current call sites produce valid indices. --- @@ -449,13 +501,24 @@ timeline section Run 54 Paper : conference paper updated — 259 theorems, 20 modules, 24 targets, Crc16Fold in table Report : REPORT.md timestamp refreshed; InterpolateN count corrected (18→19) + section Run 55-56 + Atmosphere : ISA atmosphere model (15 thms, 3 sorry needing Mathlib) — total 274 theorems + CommanderArming : arming FSM invariants (20 thms, 0 sorry) — total 294 theorems, 22 files + section Run 57-60 + Correspondence : audit, new C++ targets identified (WrapBin, PID, MotorMixer) + Research : 3 new FV targets added to TARGETS.md + section Run 61 + WrapBin : wrap_bin Euclidean model (20 thms, 0 sorry) — total 314 theorems, 23 files + Bug confirmed : C++ truncation-mod bug in wrap_bin formally proved (wrapBinCpp_bug_general) + Caller safe : wrapBinOffset_valid proves get_offset_bin_index is safe despite latent bug + Report : REPORT.md refreshed for run 61 ``` --- ## Toolchain -- **Prover**: Lean 4 (version 4.29.1) +- **Prover**: Lean 4 (version 4.29.0) - **Libraries**: Lean 4 stdlib only (Mathlib referenced in `lakefile.toml` but unavailable in CI) - **CI**: `.github/workflows/lean-ci.yml` — runs `lake build` on every PR that touches `formal-verification/lean/**`; Mathlib cache keyed on `lake-manifest.json` hash @@ -471,12 +534,13 @@ timeline | `induction` + `cases` | Structural induction over `Nat`, `List` | | `constructor` / `intro` / `apply` | Standard goal manipulation | | `Rat.mul_le_mul_*` | Rational arithmetic bounds (deadzone, lerp range) | -| `Int.emod_*` | Integer modular arithmetic (wrapInt congruence, periodicity) | +| `Int.emod_*` | Integer Euclidean modular arithmetic (wrapInt, wrapBin) | +| `Int.tmod` | Integer truncation-toward-zero mod (wrapBinCpp C++ model) | --- > 🔬 *This report was generated by Lean Squad automated formal verification.* -> *`lake build` verified with Lean 4.29.1. 6 `sorry` remain (WrapAngle wrapRat, -> all require Mathlib floor arithmetic). 259 theorems across 20 files.* -> *CORRESPONDENCE.md covers all 20 Lean files (24 C++ targets).* -> *Run 54: Conference paper updated — 259 theorems, 20 modules, 24 targets (Crc16Fold added to table, InterpolateN count corrected).* +> *`lake build` verified with Lean 4.29.0. 9 `sorry` remain (6 in WrapAngle wrapRat, +> 3 in Atmosphere — all require Mathlib). 314 theorems across 23 files.* +> *CORRESPONDENCE.md covers all Lean files. 3 bugs found (signNoZero NaN, negate involution, wrap_bin C++ truncation bug).* +> *Run 61: WrapBin proofs complete — latent C++ truncation-mod bug in wrap_bin formally confirmed.* diff --git a/formal-verification/RESEARCH.md b/formal-verification/RESEARCH.md index 7769fbcd1dd7..d6207265cdf8 100644 --- a/formal-verification/RESEARCH.md +++ b/formal-verification/RESEARCH.md @@ -880,3 +880,150 @@ collision avoidance performance. | 3 | `ObstacleMath::get_bin_at_angle` (target 27) | ⬜ Research | Depends on #25; float round needs Mathlib | | 4 | `wrapRat` theorems (WrapAngle.lean) | 🔄 Phase 3 | 6 sorrys need Mathlib floor | | 5 | `Atmosphere` sorrys | 🔄 Phase 3 | 3 sorrys need Mathlib mul_lt_mul_of_neg_left | + +--- + +## Run 63 Research — New Targets + +*Generated by Lean Squad, run 63, 2026-04-23.* + +The critique (run 63) recommended new targets building on existing proved work. The following +three targets are identified as the most tractable and highest-value next steps: + +--- + +### Target 28: `ObstacleMath::get_lower_bound_angle` + +**File**: `src/lib/collision_prevention/ObstacleMath.cpp` + +```cpp +float get_lower_bound_angle(int bin, float bin_width, float angle_offset) +{ + bin = wrap_bin(bin, 360 / bin_width); + return wrap_360(bin * bin_width + angle_offset - bin_width / 2.f); +} +``` + +**Benefit**: The lower-bound angle function is used to determine the angular coverage of a +collision-avoidance bin. If the result is incorrect (outside [0, 360) or wrong bin), the +sensor data is assigned to the wrong obstacle bin. Since `wrap_bin` is now fully proved, +this is a natural follow-on. Key property: for any `bin` and standard `bin_width` (e.g. 5°), +`get_lower_bound_angle` returns an angle in [0, 360). A rational-integer model (treating +`bin_width` as a fixed integer divisor of 360) can prove this via `wrapBin` theorems. + +**Specification size**: ~40 Lean lines. Depends on WrapBin.lean theorems. + +**Proof tractability**: MEDIUM — the angle arithmetic (multiply by bin_width, subtract half) +involves rational arithmetic; `wrap_360` maps to `wrapInt` on a scaled model. + +**Approximations needed**: `float` angles modelled as `Rat`; `wrap_360` modelled as +`wrapInt 0 360`; `bin_width` fixed at a specific value (5 or 6 degrees) for tractable proofs. + +**Approach**: Integer/rational model with `bin_width : Int` parameter (e.g., 5). +Reuse `wrapBin` theorems from WrapBin.lean. Prove `0 ≤ get_lower_bound_angle_int ≤ 360`. + +**Bug-finding potential**: MEDIUM — if `bin_width` doesn't divide 360 evenly, cumulative +rounding can cause the last bin to overlap or miss angles. This is a latent consistency +issue worth checking. + +--- + +### Target 29: `crc16_signature` fold/split property (CCITT variant) + +**File**: `src/lib/crc/crc.c` + +```c +uint16_t crc16_add(uint16_t crc, uint8_t value) +{ + const uint16_t poly = 0x1021u; + crc ^= (uint16_t)((uint16_t)value << 8u); + for (i = 0; i < 8; i++) { + if (crc & (1u << 15u)) { crc = (uint16_t)((crc << 1u) ^ poly); } + else { crc = (uint16_t)(crc << 1u); } + } + return crc; +} + +uint16_t crc16_signature(uint16_t initial, size_t length, const uint8_t *data) +{ + uint16_t crc = initial; + for (size_t i = 0; i < length; i++) { crc = crc16_add(crc, data[i]); } + return crc; +} +``` + +**Benefit**: The CRC16 fold/split property — `crc16_signature(init, len1+len2, data1++data2) = +crc16_signature(crc16_signature(init, len1, data1), len2, data2)` — is the key correctness +property for fragmented MAVLINK and bootloader CRC computation. The same structural proof +pattern as `Crc16Fold.lean` (Septentrio, `crc16_append`) applies here. `UInt16`/`UInt8` +bitwise arithmetic in Lean matches C `uint16_t`/`uint8_t` exactly. The proof technique: +`List.foldl_append` lemma from Lean 4 stdlib, as used in `Crc16Fold.lean`. + +**Specification size**: ~50 Lean lines (similar to Crc16Fold.lean). + +**Proof tractability**: HIGH — `List.foldl_append` proves this in 1–2 lines, exactly as in +`Crc16Fold.lean`. The CCITT polynomial (0x1021) differs from the Septentrio one, but the +proof structure is identical: both are `List.foldl`-based. + +**Approximations needed**: None — UInt16/UInt8 model is exact. + +**Approach**: Define `crc16Add : UInt16 → UInt8 → UInt16` (via `decide`-computable bit ops), +`crc16Sig : UInt16 → List UInt8 → UInt16 := List.foldl crc16Add`, then prove +`crc16Sig init (a ++ b) = crc16Sig (crc16Sig init a) b` using `List.foldl_append`. + +**Bug-finding potential**: LOW for the fold property itself (structurally correct). But +fuzz-testing concrete values could reveal polynomial or initial-value issues. + +--- + +### Target 30: `math::computeBrakingDistanceFromVelocity` + +**File**: `src/lib/mathlib/math/TrajMath.hpp` + +```cpp +inline float computeBrakingDistanceFromVelocity(const float velocity, const float jerk, + const float accel, const float accel_delay_max) +{ + return velocity * (velocity / (2.0f * accel) + accel_delay_max / jerk); +} +``` + +**Benefit**: This function computes the minimum braking distance to decelerate from +`velocity` to zero given jerk and acceleration limits. It is used in trajectory planning +(position smoothing, waypoint approach). Key safety properties: +1. **Non-negativity**: distance ≥ 0 when velocity ≥ 0, accel > 0, jerk > 0, accel_delay_max ≥ 0. +2. **Monotone in velocity**: larger velocity → longer braking distance. +3. **Monotone in accel (inverse)**: stronger deceleration → shorter braking distance. +These are direct flight-safety properties: under-estimating braking distance can cause the +vehicle to overshoot waypoints or collide with obstacles. + +**Specification size**: ~30 Lean lines. + +**Proof tractability**: MEDIUM — rational model is straightforward; `omega`/`Rat.mul_pos`/ +`Rat.div_pos` suffice for sign and monotonicity proofs. + +**Approximations needed**: `float` → `Rat`; `NaN`/overflow excluded by preconditions +(jerk > 0, accel > 0). The rational model computes exactly the same value as the float +formula for non-extreme inputs. + +**Approach**: Define `brakingDist (v j a d : Rat) := v * (v / (2 * a) + d / j)`. +Prove: `hv: 0 ≤ v, ha: 0 < a, hj: 0 < j, hd: 0 ≤ d → 0 ≤ brakingDist v j a d`. +Prove monotonicity: `v1 ≤ v2 → brakingDist v1 j a d ≤ brakingDist v2 j a d` (for v ≥ 0). + +**Bug-finding potential**: MEDIUM — the formula is simple, but if `accel` or `jerk` is +zero (a precondition violation), division by zero occurs. A theorem proving that the caller +must ensure `jerk > 0 ∧ accel > 0` documents this implicit precondition. + +--- + +## Updated Priority Order (run 63) + +| Priority | Target | Phase | Rationale | +|----------|--------|-------|-----------| +| 1 | `crc16_signature` fold/split (target 29) | ⬜ Research | Structurally identical to Crc16Fold; 1-line proof via `List.foldl_append` | +| 2 | `math::computeBrakingDistanceFromVelocity` (target 30) | ⬜ Research | Pure function, rational model, direct safety property | +| 3 | `ObstacleMath::get_bin_at_angle` (target 27) | ⬜ Research | Now that WrapBin proved; float round still needs Mathlib | +| 4 | `ObstacleMath::get_lower_bound_angle` (target 28) | ⬜ Research | Builds on WrapBin; rational model tractable | +| 5 | `wrapRat` theorems (WrapAngle.lean) | 🔄 Phase 3 | 6 sorrys need Mathlib floor | +| 6 | `Atmosphere` sorrys | 🔄 Phase 3 | 3 sorrys need Mathlib mul_lt_mul_of_neg_left | +| 7 | `SqrtLinear` sqrt branch sorrys | 🔄 Phase 3 | 3 sorrys need Mathlib Real.sqrt | diff --git a/formal-verification/TARGETS.md b/formal-verification/TARGETS.md index 25a635c7d696..a4d52d109bc7 100644 --- a/formal-verification/TARGETS.md +++ b/formal-verification/TARGETS.md @@ -47,10 +47,18 @@ rationale. Phase legend: 1=Research, 2=Informal Spec, 3=Lean Spec, 4=Implementat | # | Name | File | Phase | Status | Lean File | Notes | |---|------|------|-------|--------|-----------|-------| -| 25 | `ObstacleMath::wrap_bin` | `src/lib/collision_prevention/ObstacleMath.cpp` | 1 | ⬜ Research | — | Integer modulo-wrap for collision-prevention bin indices; potential correctness bug for `bin ≤ -bin_count`; all proofs by `omega` | -| 26 | `math::sqrt_linear` | `src/lib/mathlib/math/Functions.hpp` | 1 | ⬜ Research | — | Piecewise sqrt+linear utility; linear branch and boundaries provable with stdlib; sqrt branch needs Mathlib | +| 25 | `ObstacleMath::wrap_bin` | `src/lib/collision_prevention/ObstacleMath.cpp` | 5 | ✅ Proved | `lean/FVSquad/WrapBin.lean` | 20 theorems, 0 sorry; latent C++ truncation-mod bug confirmed by `wrapBinCpp_bug_general` | +| 26 | `math::sqrt_linear` | `src/lib/mathlib/math/Functions.hpp` | 5 | 🔄 Partial | `lean/FVSquad/SqrtLinear.lean` | 12 theorems proved, 3 sorry (sqrt branch needs Mathlib `Real.sqrt`); informal spec written | | 27 | `ObstacleMath::get_bin_at_angle` | `src/lib/collision_prevention/ObstacleMath.cpp` | 1 | ⬜ Research | — | Angle-to-bin conversion; depends on target 25; float `round` needs Mathlib for complete proof | +## New Research Targets (Phase 1 — identified in run 63) + +| # | Name | File | Phase | Status | Lean File | Notes | +|---|------|------|-------|--------|-----------|-------| +| 28 | `ObstacleMath::get_lower_bound_angle` | `src/lib/collision_prevention/ObstacleMath.cpp` | 1 | ⬜ Research | — | Lower bound angle of a bin; builds on WrapBin; rational model; range invariant [0, 360) | +| 29 | `crc16_signature` fold/split (CCITT) | `src/lib/crc/crc.c` | 1 | ⬜ Research | — | CRC fold/split: `crc16(a++b) = crc16_append(crc16(a),b)`; same structure as Crc16Fold; `List.foldl_append` proof | +| 30 | `math::computeBrakingDistanceFromVelocity` | `src/lib/mathlib/math/TrajMath.hpp` | 1 | ⬜ Research | — | Braking distance formula; safety: non-negativity + monotonicity in velocity; rational model tractable | + ## Non-Lean Targets (other tools recommended) | # | Name | Tool | Status | Notes | diff --git a/formal-verification/lean/FVSquad/Basic.lean b/formal-verification/lean/FVSquad/Basic.lean index 6c7bf5a4217c..3c107d9b322c 100644 --- a/formal-verification/lean/FVSquad/Basic.lean +++ b/formal-verification/lean/FVSquad/Basic.lean @@ -17,3 +17,5 @@ import FVSquad.SignFromBoolSq import FVSquad.Crc16Fold import FVSquad.CommanderArming import FVSquad.Atmosphere +import FVSquad.WrapBin +import FVSquad.SqrtLinear diff --git a/formal-verification/lean/FVSquad/SqrtLinear.lean b/formal-verification/lean/FVSquad/SqrtLinear.lean new file mode 100644 index 000000000000..11ab9eb20722 --- /dev/null +++ b/formal-verification/lean/FVSquad/SqrtLinear.lean @@ -0,0 +1,181 @@ +/-! +# math::sqrt_linear — Formal Verification + +🔬 *Lean Squad automated formal verification.* + +- **C++ source**: `src/lib/mathlib/math/Functions.hpp` +- **Informal spec**: `formal-verification/specs/sqrt_linear_informal.md` + +## C++ reference + +```cpp +template +const T sqrt_linear(const T& value) +{ + if (value < static_cast(0)) { + return static_cast(0); + } else if (value < static_cast(1)) { + return sqrtf(value); + } else { + return value; + } +} +``` + +## Three-branch piecewise structure + +| Branch | Condition | Return | +|--------|-----------|--------| +| Negative | `value < 0` | `0` | +| Sqrt | `0 ≤ value < 1` | `sqrtf(value)` | +| Identity | `value ≥ 1` | `value` | + +## Model + +We model the function over `Rat` (rational numbers): + +- **Negative branch** (`x < 0`): exact — returns `0`. +- **Identity branch** (`x ≥ 1`): exact — returns `x`. +- **Sqrt branch** (`0 ≤ x < 1`): abstracted via axiom `sqrtBranch`. + `Real.sqrt` is not available in Lean 4 stdlib; theorems about this branch use `sorry`. + +All theorems that concern only the negative or identity branch are proved without `sorry`. + +## Approximations / Out of Scope + +- **IEEE 754 float semantics**: NaN, infinity, and rounding are not modelled. +- **Sqrt branch**: `sqrtf` is axiomatised; any theorem requiring `sqrtf` properties + (non-negativity, sub-1 bound, `sqrtf(0) = 0`) uses `sorry` until Mathlib is available. +- **Template parameter**: modelled as `Rat`; C++ `float` has additional rounding not + captured here. +-/ + +namespace PX4.SqrtLinear + +/-! ## Abstract sqrt model -/ + +/-- Abstract model for `sqrtf(x)` on `[0, 1)`. + `Real.sqrt` is not available in Lean 4 stdlib; this is an opaque axiom. + All theorems that depend on sqrt properties are sorry-guarded. -/ +noncomputable axiom sqrtBranch : Rat → Rat + +/-! ## Implementation model -/ + +/-- Lean model of `math::sqrt_linear`. + + Matches the three-branch C++ implementation: + - `x < 0`: returns `0` + - `0 ≤ x < 1`: returns `sqrtBranch x` (models `sqrtf(x)`) + - `x ≥ 1`: returns `x` -/ +noncomputable def sqrtLinear (x : Rat) : Rat := + if x < 0 then 0 + else if x < 1 then sqrtBranch x + else x + +/-! ## Sanity checks (as expressions: sqrtLinear is noncomputable due to sqrtBranch) -/ + +-- Identity branch: sqrtLinear x = x for x ≥ 1 +-- e.g. sqrtLinear 1 = 1, sqrtLinear 2 = 2, sqrtLinear (5/2) = 5/2 +-- Negative branch: sqrtLinear x = 0 for x < 0 +-- e.g. sqrtLinear (-1) = 0, sqrtLinear (-3/2) = 0 +-- Sqrt branch: sqrtLinear x = sqrtBranch x for 0 ≤ x < 1 +-- e.g. sqrtLinear (1/4) = sqrtBranch (1/4) [= 0.5 in the C++ float implementation] + +/-! ## Negative branch: maps to zero -/ + +/-- For all `x < 0`, `sqrt_linear(x) = 0`. + This is the first branch of the C++ implementation. -/ +theorem sqrtLinear_neg (x : Rat) (h : x < 0) : sqrtLinear x = 0 := by + simp [sqrtLinear, h] + +/-- `sqrt_linear(-1) = 0`: concrete example. -/ +theorem sqrtLinear_neg1 : sqrtLinear (-1) = 0 := + sqrtLinear_neg (-1) (by decide) + +/-- `sqrt_linear(-3/2) = 0`: concrete example with rational input. -/ +theorem sqrtLinear_neg_three_halves : sqrtLinear (-3/2) = 0 := + sqrtLinear_neg (-3/2) (by native_decide) + +/-- For `x < 0`, the output is nonneg (trivially: output is 0). -/ +theorem sqrtLinear_neg_nonneg (x : Rat) (h : x < 0) : 0 ≤ sqrtLinear x := by + rw [sqrtLinear_neg x h] + exact (by decide : (0 : Rat) ≤ 0) + +/-! ## Identity branch: fixed points for x ≥ 1 -/ + +/-- For all `x ≥ 1`, `sqrt_linear(x) = x`. + This is the third branch of the C++ implementation. -/ +theorem sqrtLinear_ge_one (x : Rat) (h : 1 ≤ x) : sqrtLinear x = x := by + simp only [sqrtLinear] + have h0 : ¬ x < 0 := Rat.not_lt.mpr (Rat.le_trans (by decide) h) + have h1 : ¬ x < 1 := Rat.not_lt.mpr h + simp [h0, h1] + +/-- `sqrt_linear(1) = 1`: the identity branch starts exactly at 1. + This is a key boundary: both sqrt(1)=1 and identity(1)=1. -/ +theorem sqrtLinear_one : sqrtLinear 1 = 1 := + sqrtLinear_ge_one 1 (by decide) + +/-- `sqrt_linear(2) = 2`: concrete example in identity branch. -/ +theorem sqrtLinear_two : sqrtLinear 2 = 2 := + sqrtLinear_ge_one 2 (by decide) + +/-- `sqrt_linear(5/2) = 5/2`: rational input in identity branch. -/ +theorem sqrtLinear_five_halves : sqrtLinear (5/2) = 5/2 := + sqrtLinear_ge_one (5/2) (by native_decide) + +/-- For `x ≥ 1`, `sqrt_linear(x) ≥ 0`. + Follows from the identity: result is `x`, and `x ≥ 1 > 0`. -/ +theorem sqrtLinear_ge_one_nonneg (x : Rat) (h : 1 ≤ x) : 0 ≤ sqrtLinear x := by + rw [sqrtLinear_ge_one x h] + exact Rat.le_trans (by decide) h + +/-- For `x ≥ 1`, `sqrt_linear(x) ≥ 1`. + The identity branch preserves the `≥ 1` property. -/ +theorem sqrtLinear_ge_one_ge_one (x : Rat) (h : 1 ≤ x) : 1 ≤ sqrtLinear x := by + rw [sqrtLinear_ge_one x h] + exact h + +/-- Identity branch is monotone: `1 ≤ x ≤ y → sqrt_linear(x) ≤ sqrt_linear(y)`. + Both sides equal their arguments; monotonicity follows directly. -/ +theorem sqrtLinear_mono_ge_one (x y : Rat) (hx : 1 ≤ x) (hxy : x ≤ y) : + sqrtLinear x ≤ sqrtLinear y := by + rw [sqrtLinear_ge_one x hx, sqrtLinear_ge_one y (Rat.le_trans hx hxy)] + exact hxy + +/-- `sqrt_linear` is idempotent on `[1, ∞)`: + applying it twice is the same as applying it once. -/ +theorem sqrtLinear_idempotent_ge_one (x : Rat) (h : 1 ≤ x) : + sqrtLinear (sqrtLinear x) = sqrtLinear x := by + rw [sqrtLinear_ge_one x h, sqrtLinear_ge_one x h] + +/-! ## Sqrt branch (sorry-guarded: requires Mathlib Real.sqrt) -/ + +/-- `sqrt_linear(0) = 0`: `sqrtf(0.0) = 0.0` by IEEE 754. + + Requires `sqrtBranch 0 = 0`. + In Lean 4 with Mathlib: follows from `Real.sqrt_zero`. -/ +theorem sqrtLinear_zero : sqrtLinear 0 = 0 := by + simp only [sqrtLinear, if_neg (by decide : ¬(0 : Rat) < 0), + if_pos (by decide : (0 : Rat) < 1)] + sorry -- sqrtBranch 0 = 0; needs Real.sqrt_zero from Mathlib + +/-- For `0 ≤ x < 1`, `sqrt_linear(x) ≥ 0`. + + Requires `0 ≤ sqrtBranch x` (i.e., `Real.sqrt x ≥ 0`). + In Lean 4 with Mathlib: follows from `Real.sqrt_nonneg`. -/ +theorem sqrtLinear_sqrt_nonneg (x : Rat) (h0 : 0 ≤ x) (h1 : x < 1) : + 0 ≤ sqrtLinear x := by + simp only [sqrtLinear, if_neg (Rat.not_lt.mpr h0), if_pos h1] + sorry -- 0 ≤ sqrtBranch x; needs Real.sqrt_nonneg from Mathlib + +/-- For `0 < x < 1`, `sqrt_linear(x) < 1`. + + Requires `sqrtBranch x < 1` (i.e., `Real.sqrt x < 1` for `x ∈ (0,1)`). + In Lean 4 with Mathlib: follows from `Real.sqrt_lt_one`. -/ +theorem sqrtLinear_sqrt_lt_one (x : Rat) (h0 : 0 < x) (h1 : x < 1) : + sqrtLinear x < 1 := by + simp only [sqrtLinear, if_neg (Rat.not_lt.mpr (Rat.le_of_lt h0)), if_pos h1] + sorry -- sqrtBranch x < 1; needs Real.sqrt_lt_one from Mathlib + +end PX4.SqrtLinear diff --git a/formal-verification/lean/FVSquad/WrapBin.lean b/formal-verification/lean/FVSquad/WrapBin.lean new file mode 100644 index 000000000000..53f2318c6aeb --- /dev/null +++ b/formal-verification/lean/FVSquad/WrapBin.lean @@ -0,0 +1,207 @@ +/-! +# ObstacleMath::wrap_bin — Formal Verification + +🔬 *Lean Squad automated formal verification.* + +- **C++ source**: `src/lib/collision_prevention/ObstacleMath.cpp` (line ~140) +- **Informal spec**: `formal-verification/specs/wrap_bin_informal.md` + +## C++ reference + +```cpp +// ObstacleMath.cpp +int wrap_bin(int bin, int bin_count) +{ + return (bin + bin_count) % bin_count; +} +``` + +## Model + +We provide two models: + +1. **`wrapBin`** — uses Lean 4's Euclidean `%` on `Int` (non-negative for positive + divisor). This captures the *intended* semantics: result always in `[0, bin_count)`. + All correctness theorems use this model. + +2. **`wrapBinCpp`** — uses `Int.tmod` (C++ truncation-toward-zero semantics). + For `bin ≤ -bin_count - 1`, `bin + bin_count < 0`, so `Int.tmod` returns a + negative value — the latent bug in the C++ implementation. + +**Key insight**: Lean's `%` on `Int` is Euclidean (always `≥ 0` for positive divisor), +so `wrapBin` is provably correct for *all* integer inputs. The C++ implementation has a +latent bug because `%` in C++ uses truncation semantics. + +## Bug Finding + +`wrapBinCpp_bug_general` proves that for any `bin_count > 1`, +`wrapBinCpp (-bin_count - 1) bin_count = -1`, confirming the documented latent bug. + +`wrapBinOffset_valid` proves that all current callers (`get_offset_bin_index`, passing +`bin - offset` with `0 ≤ bin, offset < bin_count`) are **safe** in practice — +the inputs never reach the buggy region. + +## Approximations / Out of Scope + +- **Float-based callers** (`get_bin_at_angle`, `get_lower_bound_angle`): involve + `float` arithmetic and `roundf`, which are not modelled here. +- **`wrap_360`**: uses a floating-point wrap; not modelled. +- The model covers only `wrap_bin` itself. +-/ + +namespace PX4.ObstacleMath + +/-! ## Implementation models -/ + +/-- **Lean model** of `wrap_bin`: uses Euclidean `%` (always `≥ 0` for positive divisor). + This captures the intended semantics. All correctness theorems use this model. -/ +def wrapBin (bin bin_count : Int) : Int := + (bin + bin_count) % bin_count + +/-- **C++ model** of `wrap_bin`: uses `Int.tmod` (truncation-toward-zero, matching C++). + For negative sums `bin + bin_count < 0`, this returns a negative result — the bug. -/ +def wrapBinCpp (bin bin_count : Int) : Int := + Int.tmod (bin + bin_count) bin_count + +/-! ## Sanity checks (eval) -/ + +-- All test cases from ObstacleMathTest.cpp +#eval wrapBin 0 72 -- 0 (in range: identity) +#eval wrapBin 71 72 -- 71 (in range: identity) +#eval wrapBin 72 72 -- 0 (at count: wrap to 0) +#eval wrapBin 73 72 -- 1 (one above: wrap to 1) +#eval wrapBin (-1) 72 -- 71 (one below: wrap to last) +#eval wrapBin (-72) 72 -- 0 (exactly -n: still ok) +#eval wrapBin (-73) 72 -- 71 (Lean: correct; C++ would give -1) + +-- C++ model shows the bug +#eval wrapBinCpp (-1) 72 -- 71 (same sign as argument: correct here) +#eval wrapBinCpp (-73) 72 -- -1 ← BUG: C++ truncation gives negative result! + +/-! ## Concrete examples (native_decide) -/ + +/-- Test case 1: bin 0 is identity. -/ +theorem wrapBin_example_zero : wrapBin 0 72 = 0 := by native_decide + +/-- Test case 2: bin 71 is identity. -/ +theorem wrapBin_example_71 : wrapBin 71 72 = 71 := by native_decide + +/-- Test case 3: bin 72 wraps to 0. -/ +theorem wrapBin_example_72 : wrapBin 72 72 = 0 := by native_decide + +/-- Test case 4: bin 73 wraps to 1. -/ +theorem wrapBin_example_73 : wrapBin 73 72 = 1 := by native_decide + +/-- Test case 5: bin -1 wraps to 71 (correct Euclidean semantics). -/ +theorem wrapBin_example_neg1 : wrapBin (-1) 72 = 71 := by native_decide + +/-- Test case 6: bin -72 wraps to 0 (correct). -/ +theorem wrapBin_example_neg72 : wrapBin (-72) 72 = 0 := by native_decide + +/-- Test case 7: bin -73 wraps to 71 (Lean Euclidean: correct). + The C++ version would give -1 (the latent bug). -/ +theorem wrapBin_example_neg73 : wrapBin (-73) 72 = 71 := by native_decide + +/-- Bug demo: C++ model gives -1 for bin = -73. -/ +theorem wrapBinCpp_bug_example : wrapBinCpp (-73) 72 = -1 := by native_decide + +/-! ## Universal range theorem -/ + +/-- **Range**: `wrapBin` always returns a value in `[0, bin_count)` for any `bin` + and any positive `bin_count`. This holds for ALL integer inputs — no preconditions + on `bin` are needed. This is the key advantage of Lean's Euclidean `%`. -/ +theorem wrapBin_range (bin bin_count : Int) (hpos : 0 < bin_count) : + 0 ≤ wrapBin bin bin_count ∧ wrapBin bin bin_count < bin_count := + ⟨Int.emod_nonneg _ (Int.ne_of_gt hpos), Int.emod_lt_of_pos _ hpos⟩ + +/-- **Range lower bound** (standalone). -/ +theorem wrapBin_nonneg (bin bin_count : Int) (hpos : 0 < bin_count) : + 0 ≤ wrapBin bin bin_count := + Int.emod_nonneg _ (Int.ne_of_gt hpos) + +/-- **Range upper bound** (standalone). -/ +theorem wrapBin_lt_count (bin bin_count : Int) (hpos : 0 < bin_count) : + wrapBin bin bin_count < bin_count := + Int.emod_lt_of_pos _ hpos + +/-! ## Identity and wrap-around theorems -/ + +/-- **Identity**: for in-range bins, `wrapBin` is the identity. -/ +theorem wrapBin_identity (bin bin_count : Int) + (hnn : 0 ≤ bin) (hlt : bin < bin_count) : + wrapBin bin bin_count = bin := by + simp only [wrapBin, Int.add_emod_right, Int.emod_eq_of_lt hnn hlt] + +/-- **Wrap at bin_count**: `wrapBin bin_count bin_count = 0`. -/ +theorem wrapBin_at_count (bin_count : Int) (_ : 0 < bin_count) : + wrapBin bin_count bin_count = 0 := by + simp only [wrapBin, Int.add_emod_right, Int.emod_self] + +/-- **One below zero**: `wrapBin (-1) n = n - 1` when `n > 1`. -/ +theorem wrapBin_neg1 (bin_count : Int) (h : 1 < bin_count) : + wrapBin (-1) bin_count = bin_count - 1 := by + simp only [wrapBin, show (-1 : Int) + bin_count = bin_count - 1 from by omega] + exact Int.emod_eq_of_lt (by omega) (by omega) + +/-- **Exactly -bin_count**: `wrapBin (-bin_count) bin_count = 0`. -/ +theorem wrapBin_neg_count (bin_count : Int) (_ : 0 < bin_count) : + wrapBin (-bin_count) bin_count = 0 := by + simp only [wrapBin, show (-bin_count) + bin_count = (0 : Int) from by omega, Int.zero_emod] + +/-- **One above**: `wrapBin (bin_count + k) bin_count = k` when `0 ≤ k < bin_count`. -/ +theorem wrapBin_one_above (k bin_count : Int) + (hk : 0 ≤ k) (hklt : k < bin_count) : + wrapBin (bin_count + k) bin_count = k := by + simp only [wrapBin, show bin_count + k + bin_count = k + bin_count * 2 from by omega, + Int.add_mul_emod_self_left, Int.emod_eq_of_lt hk hklt] + +/-! ## C++ model and bug theorems -/ + +/-- **Key lemma**: `Int.tmod (-1) n = -1` for `n > 1`. + This follows from the definition: `tmod (negSucc 0) (ofNat (k+2)) = -(1 % (k+2)) = -1`. -/ +private theorem tmod_neg1_gt1 (n : Int) (hn : 1 < n) : Int.tmod (-1) n = -1 := by + match n with + | Int.ofNat (k + 2) => + show (match (Int.negSucc 0 : Int), (Int.ofNat (k + 2) : Int) with + | Int.ofNat m, Int.ofNat n => Int.ofNat (m % n) + | Int.ofNat m, Int.negSucc n => Int.ofNat (m % n.succ) + | Int.negSucc m, Int.ofNat n => -Int.ofNat (m.succ % n) + | Int.negSucc m, Int.negSucc n => -Int.ofNat (m.succ % n.succ)) = -1 + simp only + rw [Nat.mod_eq_of_lt (by omega)] + rfl + +/-- **C++ latent bug**: `wrapBinCpp (-bin_count - 1) bin_count = -1` for `bin_count > 1`. + + When `bin = -bin_count - 1`, `bin + bin_count = -1 < 0`, and C++ truncation mod + returns `-1` — a negative array index that causes undefined behaviour. -/ +theorem wrapBinCpp_bug_general (n : Int) (hn : 1 < n) : + wrapBinCpp (-n - 1) n = -1 := by + simp only [wrapBinCpp, show -n - 1 + n = (-1 : Int) from by omega] + exact tmod_neg1_gt1 n hn + +/-- **Models agree on the valid domain**: when `bin + bin_count ≥ 0`, + `wrapBin` and `wrapBinCpp` give the same result (non-negative argument → both agree). -/ +theorem wrapBin_eq_wrapBinCpp_valid (bin bin_count : Int) + (hsum : 0 ≤ bin + bin_count) : + wrapBin bin bin_count = wrapBinCpp bin bin_count := by + simp only [wrapBin, wrapBinCpp, Int.tmod_eq_emod_of_nonneg hsum] + +/-! ## Caller safety theorem -/ + +/-- **`get_offset_bin_index` caller safety**: passing `bin - offset` where + `bin ∈ [0, bin_count)` and `offset ∈ [0, bin_count)` always gives `sum ≥ 1 > 0`, + so `wrapBin` and `wrapBinCpp` agree and the result is in `[0, bin_count)`. + Current callers are **never** affected by the latent bug. -/ +theorem wrapBinOffset_valid (bin offset bin_count : Int) + (hpos : 0 < bin_count) + (hbin_lb : 0 ≤ bin) (_hbin_ub : bin < bin_count) + (_hoff_lb : 0 ≤ offset) (hoff_ub : offset < bin_count) : + 0 ≤ wrapBin (bin - offset) bin_count ∧ + wrapBin (bin - offset) bin_count < bin_count ∧ + wrapBin (bin - offset) bin_count = wrapBinCpp (bin - offset) bin_count := by + refine ⟨wrapBin_nonneg _ _ hpos, wrapBin_lt_count _ _ hpos, ?_⟩ + apply wrapBin_eq_wrapBinCpp_valid + omega + +end PX4.ObstacleMath diff --git a/formal-verification/specs/sqrt_linear_informal.md b/formal-verification/specs/sqrt_linear_informal.md new file mode 100644 index 000000000000..03276e0de857 --- /dev/null +++ b/formal-verification/specs/sqrt_linear_informal.md @@ -0,0 +1,105 @@ +# Informal Specification: `math::sqrt_linear` + +🔬 *Lean Squad automated formal verification.* + +- **C++ source**: `src/lib/mathlib/math/Functions.hpp` +- **Lean file**: `formal-verification/lean/FVSquad/SqrtLinear.lean` + +--- + +## Purpose + +`sqrt_linear` is a piecewise scalar utility used in PX4's mathlib. It smoothly connects +a zero-output region (for negative inputs), a square-root curve (for inputs in [0, 1)), +and a linear identity (for inputs ≥ 1). This shape provides a "soft" nonlinear mapping +often used in sensor scaling and stick-response curves. + +## C++ Signature + +```cpp +template +const T sqrt_linear(const T& value) +{ + if (value < static_cast(0)) { + return static_cast(0); + } else if (value < static_cast(1)) { + return sqrtf(value); + } else { + return value; + } +} +``` + +## Preconditions + +- `value` is a finite floating-point or rational number. +- No special requirements; the function is total and well-defined for all inputs. + +## Postconditions + +The function has three branches: + +| Condition | Return value | Notes | +|-----------|-------------|-------| +| `value < 0` | `0` | Zero-clamp for negative inputs | +| `0 ≤ value < 1` | `sqrtf(value)` | Square-root curve | +| `value ≥ 1` | `value` | Identity / linear | + +## Key Invariants + +1. **Non-negativity**: `sqrt_linear(x) ≥ 0` for all `x`. +2. **Monotonicity on [1, ∞)**: `sqrt_linear` is the identity on `[1, ∞)`, hence monotone. +3. **Fixed point at 1**: `sqrt_linear(1) = 1` (boundary between sqrt and identity branches). +4. **Fixed point at 0**: `sqrt_linear(0) = 0` (since `sqrtf(0) = 0`). +5. **Negative inputs collapse**: for `x ≤ 0`, `sqrt_linear(x) = 0`. +6. **Idempotence on [1, ∞)**: `sqrt_linear(sqrt_linear(x)) = sqrt_linear(x)` for `x ≥ 1`. +7. **Continuity at 1**: both sqrt and identity branches give `1` at `x = 1`. + +## Edge Cases + +- `value = 0`: falls in the `[0, 1)` branch; `sqrtf(0.0) = 0.0` by IEEE 754. +- `value = 1`: falls in the `x ≥ 1` branch; returns `1`. +- Very large negatives: always returns `0`. +- Very large positives: returns `value` (identity, no saturation). +- NaN: C++ comparison `NaN < 0` and `NaN < 1` both evaluate to `false`, so `NaN` input + returns `NaN` (identity branch). This is not modelled in our Lean spec. + +## Examples + +| Input | Output | Branch | +|-------|--------|--------| +| -3/2 | 0 | negative | +| -1 | 0 | negative | +| 0 | 0 | sqrt (sqrtf(0) = 0) | +| 1/4 | 1/2 | sqrt (sqrtf(0.25) = 0.5) | +| 1 | 1 | identity | +| 2 | 2 | identity | +| 5/2 | 5/2 | identity | + +## Formal Spec Summary (Lean propositions) + +The Lean 4 file `SqrtLinear.lean` formalises the following key properties: + +**Proved (no sorry):** +- `sqrtLinear_neg`: for `x < 0`, `sqrtLinear x = 0` +- `sqrtLinear_ge_one`: for `1 ≤ x`, `sqrtLinear x = x` +- `sqrtLinear_one`: `sqrtLinear 1 = 1` +- `sqrtLinear_neg_nonneg`: for `x < 0`, `0 ≤ sqrtLinear x` +- `sqrtLinear_ge_one_nonneg`: for `1 ≤ x`, `0 ≤ sqrtLinear x` +- `sqrtLinear_ge_one_ge_one`: for `1 ≤ x`, `1 ≤ sqrtLinear x` +- `sqrtLinear_mono_ge_one`: monotonicity on `[1, ∞)` +- `sqrtLinear_idempotent_ge_one`: `sqrt_linear(sqrt_linear(x)) = sqrt_linear(x)` for `x ≥ 1` + +**Requires Mathlib (sorry-guarded):** +- `sqrtLinear_zero`: `sqrtLinear 0 = 0` (needs `Real.sqrt 0 = 0`) +- `sqrtLinear_sqrt_nonneg`: for `0 ≤ x < 1`, `0 ≤ sqrtLinear x` (needs `Real.sqrt ≥ 0`) +- `sqrtLinear_sqrt_lt_one`: for `0 < x < 1`, `sqrtLinear x < 1` (needs sqrt sub-1 bound) +- `sqrtLinear_sqrt_le`: for `0 ≤ x < 1`, `sqrtLinear x ≤ 1` (needs sqrt ≤ 1 for x ≤ 1) + +## Open Questions + +1. **NaN behaviour**: The C++ function inherits NaN propagation from IEEE 754 comparisons. + The model does not address NaN; this is out of scope for a Rat-based model. +2. **Float rounding**: The model uses exact `Rat` arithmetic; `sqrtf` has ±0.5 ULP error. +3. **Continuity at x=0**: Both branches give 0 at x=0, but continuity of the sqrt branch + at 0 is a real-analysis fact; it cannot be stated using `Rat` arithmetic. diff --git a/formal-verification/specs/wrap_bin_informal.md b/formal-verification/specs/wrap_bin_informal.md new file mode 100644 index 000000000000..b7e3da1c8979 --- /dev/null +++ b/formal-verification/specs/wrap_bin_informal.md @@ -0,0 +1,133 @@ +# Informal Specification: `ObstacleMath::wrap_bin` + +🔬 *Lean Squad automated formal verification.* + +- **C++ source**: `src/lib/collision_prevention/ObstacleMath.hpp` / + `src/lib/collision_prevention/ObstacleMath.cpp` +- **Lean spec**: `formal-verification/lean/FVSquad/WrapBin.lean` + +--- + +## Purpose + +`wrap_bin(bin, bin_count)` wraps an integer bin index into the canonical range +`[0, bin_count)`. It is used in the collision-prevention subsystem to normalise +bin indices that may lie slightly outside `[0, bin_count)` (one above or one below) +back into a valid range before they are used as array indices. + +**C++ implementation**: + +```cpp +int wrap_bin(int bin, int bin_count) +{ + return (bin + bin_count) % bin_count; +} +``` + +--- + +## Preconditions + +- `bin_count > 0` (must be a positive number of bins). +- Callers in `ObstacleMath` pass inputs that satisfy `-(bin_count - 1) ≤ bin ≤ bin_count`. + This ensures the sum `bin + bin_count` is always positive, so C++ truncation semantics + coincide with mathematical modulo. + +--- + +## Postconditions (Intended) + +The result should be the unique integer `r` such that: +1. `0 ≤ r < bin_count` +2. `r ≡ bin (mod bin_count)` + +That is, `wrap_bin` should return the mathematical (Euclidean) modulo of `bin` by +`bin_count`. + +--- + +## Invariants + +- **Range invariant** (over the valid caller domain): when `-(bin_count-1) ≤ bin ≤ bin_count`, + the result lies in `[0, bin_count)`. +- **Identity for in-range inputs**: when `0 ≤ bin < bin_count`, `wrap_bin bin bin_count = bin`. +- **Wrap for bin = -1**: `wrap_bin (-1) n = n - 1` (one-below wraps to the last bin). +- **Wrap for bin = bin_count**: `wrap_bin n n = 0` (one-above wraps to the first bin). + +--- + +## Edge Cases + +### In-range: `0 ≤ bin < bin_count` + +`(bin + bin_count) % bin_count = bin % bin_count = bin` since `n ≤ bin + bin_count < 2n`. + +### One below zero: `bin = -1` + +`(-1 + bin_count) % bin_count = (bin_count - 1) % bin_count = bin_count - 1`. Correct. + +### At bin_count: `bin = bin_count` + +`(bin_count + bin_count) % bin_count = 2*bin_count % bin_count = 0`. Correct. + +### **BUG — Two or more below zero: `bin ≤ -bin_count`** + +For `bin = -bin_count`: `(-bin_count + bin_count) % bin_count = 0 % bin_count = 0`. Still correct. + +For `bin = -bin_count - 1`: `(-bin_count - 1 + bin_count) % bin_count = (-1) % bin_count`. + +In **C++**, `%` uses truncation-toward-zero semantics, so `(-1) % n = -1` for any `n > 0`. +This gives `-1`, which is **outside** `[0, bin_count)` and would be used as a negative +array index — undefined behaviour (UB) and likely a crash or memory corruption. + +In **Lean 4**, `%` on `Int` also uses truncation-toward-zero (matching C++), so the same +latent bug is observable in the Lean model. + +--- + +## Examples + +| `bin` | `bin_count` | `(bin + n) % n` (C++/Lean) | Expected | Correct? | +|-------|-------------|----------------------------|----------|----------| +| 0 | 72 | 0 | 0 | ✓ | +| 71 | 72 | 71 | 71 | ✓ | +| 72 | 72 | 0 | 0 | ✓ | +| 73 | 72 | 1 | 1 | ✓ | +| -1 | 72 | 71 | 71 | ✓ | +| -72 | 72 | 0 | 0 | ✓ | +| **-73** | **72** | **-1** | 71 | **✗ BUG** | + +--- + +## Inferred Intent + +The function is intended to normalise bin indices that may be slightly out of range +(typically by at most one step in either direction, or one full wrap above). The design +only handles the typical usage pattern; it does not handle deeply negative inputs. + +All actual callers in `ObstacleMath` guarantee the precondition +`-(bin_count - 1) ≤ bin ≤ bin_count`, so the bug is **latent** (does not trigger in +current callers). However the API contract expressed in the doc-comment says +"wraps a bin index to the range `[0, bin_count)`" with no restriction on `bin`, which +overstates what the implementation guarantees. + +--- + +## Open Questions + +1. Should `wrap_bin` be defensive (handle all integer inputs)? The correct general + implementation is `((bin % n) + n) % n` (two mod operations, always non-negative + when `n > 0`). Should the implementation be fixed? +2. Are there any callers that could pass `bin ≤ -bin_count`? Static analysis would + confirm whether the latent bug can actually trigger. + +--- + +## Relation to Lean Spec + +The Lean file `WrapBin.lean` provides: +- A direct model of the C++ implementation using Lean's truncation-mod `Int.mod` (which + matches C++ `%` semantics for integers). +- Proofs that the model is correct within the valid caller precondition domain. +- A proof-by-counterexample that the model violates the range property for `bin ≤ -bin_count`. +- The `wrapBinOffset_valid` theorem showing current callers are safe.