[Lean Squad] feat(fv): Tasks 5+1 — Crc32Sig (11 theorems, 0 sorry) + 3 new research targets (run 75)#72
Open
github-actions[bot] wants to merge 2 commits intomainfrom
Conversation
Task 5 (Proof Assistance): Add multi-step convergence theorems to SlewRate.lean. - slewIterate: N-step iterate of slewUpdate - slewIterate_steady: steady state is preserved under iteration - slewIterate_converges_up: starting ≤ target, N steps suffice when target - current ≤ max_step * N (proved 0-sorry) - slewIterate_converges_down: starting ≥ target, N steps suffice when current - target ≤ max_step * N (proved 0-sorry) - 4 native_decide spot-checks (0→10 in 4 steps, 10→0 in 2 steps, etc.) Key fix: replaced ring (Mathlib-only) with omega and simp [Int.mul_add] for the calc steps in the induction cases. Task 2 (Informal Spec Extraction): Write informal spec for crc32_signature. - specs/crc32_informal.md: purpose, preconditions, postconditions, edge cases, concrete examples (check value 0xCBF43926 for "123456789"), and formal properties suitable for Lean (fold/append, empty identity, determinism) - Identifies crc32_fold as highest-value target (justifies UAVCAN bootloader two-call chaining pattern) lake build: passed (31 jobs, Lean 4.29.0, 0 sorry) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…h targets (run 75) Task 5 (Proof Assistance): Add formal-verification/lean/FVSquad/Crc32Sig.lean - Models and proves properties of crc32_signature (CRC-32/ISO-HDLC, poly 0xEDB88320) - Used in UAVCAN bootloader for firmware-image integrity - 11 theorems: nil/singleton/cons/append/append3/init_zero/append_nil/two/split + 6 native_decide examples - Key result: crc32sig_append — fold/split streaming property (List.foldl_append) - Lean implementation model: crc32AddBit (1 bit step) + crc32Add (8-bit byte step) + crc32sig (fold) - Correspondence level: exact (UInt8/UInt32 modular arithmetic matches C uint8_t/uint32_t) - lake build: passed, Lean 4.29.0, 32 jobs, 0 sorry Task 1 (Research): Add 3 new research targets to TARGETS.md - Target 36: crc64_add_word (CRC-64-WE, src/lib/crc/crc.c) — fold/split with UInt64 - Target 37: math::isInRange (Limits.hpp:91) — pure boolean range predicate - Target 38: math::constrainFloatToInt16 (Limits.hpp:85) — float→int16 clamp safety Also: - CORRESPONDENCE.md updated: Crc32Sig section added (exact level), summary table row added - TARGETS.md: crc32_signature advanced to phase 5 ✅; crc16_signature updated to phase 5 ✅ > 🔄 Partial verification: `lake build` passed with Lean 4.29.0. 0 `sorry` remain. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
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
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 75
Task 5: CRC-32/ISO-HDLC Signature Formal Verification
Adds
formal-verification/lean/FVSquad/Crc32Sig.lean— formal proofs of thecrc32_signaturefunction insrc/lib/crc/crc.c(line 151), which the UAVCANbootloader uses to verify firmware-image integrity.
What is proved
The CRC-32/ISO-HDLC algorithm (reflected polynomial
0xEDB88320, LSBIT-first) ismodelled as a
List.foldlover bytes, enabling a clean algebraic proof of the keystreaming property.
crc32sig_nilcrc32sig init [] = init— empty buffer identitycrc32sig_singletoncrc32sig init [b] = crc32Add init bcrc32sig_conscrc32sig init (b::bs) = crc32sig (crc32Add init b) bscrc32sig_appendcrc32sig init (a ++ b) = crc32sig (crc32sig init a) bcrc32sig_append3crc32sig_init_zerocrc32sig_append_nil[]is a no-opcrc32sig_two[a, b]equals chained single-byte stepscrc32sig_splitcrc32sig_append(term-mode)native_decide/simpTotal: 11 theorems (9 named + term alias + 6 examples), 0
sorry.Correspondence level: exact
UInt8/UInt32carry the same modular-28/232 arithmetic as Cuint8_t/uint32_t.The
-(acc & 1)two's-complement mask is captured byif c &&& 1 != 0.The model is
List.foldl crc32Add init bytes— an exact algebraic description of theC
forloop.Key proof
One line — exactly the same proof structure as
Crc16SigandCrc16Fold.Task 1: New Research Targets
Three new FV candidates identified in
TARGETS.md:crc64_add_wordfold/splitsrc/lib/crc/crc.cmath::isInRangesrc/lib/mathlib/math/Limits.hpp:91(min≤val)&&(val≤max)math::constrainFloatToInt16src/lib/mathlib/math/Limits.hpp:85Files changed
formal-verification/lean/FVSquad/Crc32Sig.lean(new)formal-verification/lean/FVSquad.lean— addedimport FVSquad.Crc32Sigformal-verification/TARGETS.md— crc32 → phase 5, crc16 updated, 3 new targetsformal-verification/CORRESPONDENCE.md— Crc32Sig section added, summary table updatedVerification status