[Lean Squad] feat(formal-verification): Tasks 7+1 — Critique update + 3 new research targets (run 63)#61
Closed
github-actions[bot] wants to merge 3 commits intomainfrom
Conversation
…onfirmed) + REPORT.md update (run 61) Add WrapBin.lean: formal verification of ObstacleMath::wrap_bin from src/lib/collision_prevention/ObstacleMath.cpp. Key results: - 20 theorems, 0 sorry, verified by lake build with Lean 4.29.0 - Two models: wrapBin (Euclidean %, provably safe for all Int) and wrapBinCpp (Int.tmod, faithfully models C++ truncation-toward-zero semantics) - wrapBin_range / wrapBin_nonneg / wrapBin_lt_count: full range proof - wrapBinCpp_bug_general: formally proves C++ wrap_bin(-1, n) = -1 for n > 1 (negative index — latent bug confirmed by proof) - wrapBin_eq_wrapBinCpp_valid: both models agree on non-negative inputs - wrapBinOffset_valid: get_offset_bin_index call site is formally safe despite bug - tmod_neg1_gt1 (private): key lemma for the bug proof using Int.tmod match reduction Also add wrap_bin_informal.md informal spec (preconditions, postconditions, edge cases, examples table, C++ bug analysis). Update REPORT.md for run 61: - Status: 259 → 314 theorems, 123 → 141 examples, 6 → 9 sorry, 20 → 23 files - Add Layer 4 WrapBin, Layer 6 CommanderArming, Layer 8 Atmosphere sections - Add Bug 3 finding (wrap_bin latent C++ truncation bug) - Add runs 55-61 timeline entries - Update file inventory table with Atmosphere, CommanderArming, WrapBin rows Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
… + 3 sorry (run 62) Add formal verification of math::sqrt_linear from PX4 mathlib. ## New files - formal-verification/lean/FVSquad/SqrtLinear.lean: Lean 4 spec + implementation - formal-verification/specs/sqrt_linear_informal.md: informal specification ## Summary - 15 theorems total: 12 proved without sorry, 3 sorry (sqrt branch) - Tasks 3 (Formal Spec Writing) + 4 (Implementation Extraction) - Three-branch model: negative→0, sqrt branch (axiomatised), identity (x≥1→x) - All non-sqrt theorems proved: neg→0, ge_one→identity, monotone, idempotent - Sorry-guarded: sqrtLinear_zero, sqrtLinear_sqrt_nonneg, sqrtLinear_sqrt_lt_one (all require Real.sqrt from Mathlib) ## Verification lake build passed with Lean 4.29.0. 3 sorry in SqrtLinear.lean (all clearly documented as needing Mathlib Real.sqrt). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…ch targets (run 63) Task 7 (Proof Utility Critique): - Update CRITIQUE.md: Last Updated → 2026-04-23 - Overall Assessment: 338 total theorems (326 proved, 12 sorry), 24 files, 27 targets - Add WrapBin theorems to Proved Theorems Table (7 new rows; latent C++ bug highlighted) - Add SqrtLinear theorems to Proved Theorems Table (4 new rows; 3 sorry-guarded) - Update Known Sorry-Guarded Theorems: now 12 (6 WrapAngle + 3 Atmosphere + 3 SqrtLinear) - Add Positive Findings #19 (WrapBin latent C++ bug) and #20 (SqrtLinear branches) - Update Gaps and Recommendations: add items 10–12 for WrapBin fix, SqrtLinear sorry, get_lower_bound_angle - Update Paper Review: stale items now include Atmosphere, WrapBin, SqrtLinear (runs 49–62); bug count in abstract is stale (3 bugs not 2) Task 1 (Research & Target Identification): - Add 3 new targets to RESEARCH.md (run 63 section): - Target 28: ObstacleMath::get_lower_bound_angle (builds on WrapBin) - Target 29: crc16_signature fold/split CCITT (same structure as Crc16Fold) - Target 30: math::computeBrakingDistanceFromVelocity (safety: non-neg + monotone) - Update TARGETS.md: targets 25/26 status updated (proved/partial); new targets 28–30 added - Updated priority order for run 63 Also includes merged PR content: WrapBin.lean (20 thms), SqrtLinear.lean (15 thms) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This was referenced Apr 24, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
🔬 Lean Squad — automated formal verification, run 63.
Summary
This PR delivers two tasks:
CRITIQUE.mdto reflect the WrapBin and SqrtLinear additions from runs 61–62 (merging two open PRs into the baseline). Total: 338 theorems (326 proved, 12 sorry), 24 Lean files, 27 targets.RESEARCH.mdandTARGETS.md.Also includes the previously open (un-merged) PRs for WrapBin.lean and SqrtLinear.lean, merged cleanly into this branch.
Task 7: CRITIQUE.md updates
New entries
wrapBin_range,wrapBin_identity,wrapBin_one_above,wrapBinCpp_bug_general(🐛 latent C++ bug),wrapBin_eq_wrapBinCpp_valid,wrapBinOffset_validsqrtLinear_neg,sqrtLinear_ge_one,sqrtLinear_mono_ge_one,sqrtLinear_idempotent_ge_one, plus 3 sorry-guarded sqrt-branch theoremsUpdated sections
Task 1: New Research Targets
ObstacleMath::get_lower_bound_angleObstacleMath.cppcrc16_signaturefold/split (CCITT)crc.cList.foldl_appendproofmath::computeBrakingDistanceFromVelocityTrajMath.hppRationale: Target 29 is the most tractable (structurally identical to the already-proved
Crc16Fold.lean). Target 30 has direct flight safety relevance (braking distance underestimation → waypoint overshoot/collision). Target 28 is the natural continuation of the WrapBin work.No Lean build required
This PR contains only documentation updates (
CRITIQUE.md,RESEARCH.md,TARGETS.md) plus the merged-inWrapBin.leanandSqrtLinear.leanfrom prior open PRs. No new.leanfiles are added in this PR beyond what was previously submitted.