[Lean Squad] feat(formal-verification): WrapBin proofs (20 theorems, latent C++ bug confirmed) + REPORT.md update (run 61)#59
Closed
github-actions[bot] wants to merge 1 commit 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>
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.
Summary
Tasks 5 (Proof Assistance) + 10 (Project Report) — Run 61
New:
WrapBin.lean(20 theorems, 0 sorry) — formal verification ofObstacleMath::wrap_bin. Updated:REPORT.md(314 theorems, 23 files).Key finding: Latent C++ truncation-mod bug confirmed
wrap_bin(bin, bin_count)computes(bin + bin_count) % bin_count. C++ truncation-toward-zero mod returns negative results for some negative inputs:Formally proved by
wrapBinCpp_bug_general: for anyn > 1,wrapBinCpp(-1, n) = -1.Current callers are safe (formally proved via
wrapBinOffset_valid).Two models
wrapBin%(Euclidean)wrapBinCppInt.tmod(C++ truncation)Key theorems (20, 0 sorry)
wrapBin_range,wrapBin_nonneg,wrapBin_lt_count: full range proofwrapBin_identity: identity on valid inputswrapBinCpp_bug_general: C++ returns -1 for input -1 when n > 1wrapBin_eq_wrapBinCpp_valid: models agree on non-negative inputswrapBinOffset_valid:get_offset_bin_indexcaller formally safeVerification