[Lean Squad] feat(fv): SlewRate convergence proofs + crc32_signature informal spec (run 74)#71
Open
github-actions[bot] wants to merge 1 commit 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>
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 74
Task 5: SlewRate Multi-Step Convergence Proofs
Adds the key liveness property of the rate limiter to
formal-verification/lean/FVSquad/SlewRate.lean: iteratingslewUpdatealways terminates attargetwithin a bounded number of steps.New definitions and theorems
slewIteratedefslewUpdateslewIterate_zero@[simp] theoremslewIterate_succtheoremslewIterate_steadytheoremslewUpdate_far_upprivate theoremslewUpdate_far_downprivate theoremslewIterate_converges_uptarget − current ≤ max_step × NslewIterate_converges_downcurrent − target ≤ max_step × NPlus 4
native_decidespot-checks:0→10in 4 steps at rate 3,10→0in 2 steps at rate 5, stability past convergence.Proof technique: induction on N,
by_caseson whether current is within one step of target. The "too far" case usesslewUpdate_far_up/downhelpers and acalcchain. Key fix: replaced Mathlib-onlyringwithomega(for linear steps) andsimp [Int.mul_add](for themax_step * ↑(n+1) − max_step = max_step * ↑nalgebra), keeping this a stdlib-only proof.Task 2: crc32_signature Informal Specification
New file
formal-verification/specs/crc32_informal.mdforcrc32_signatureinsrc/lib/crc/crc.c.Algorithm: CRC-32/ISO-HDLC (reflected polynomial
0xEDB88320), same family as used in Ethernet/gzip/PNG. Processed asList.foldl crc32Step acc bytes.Key properties specified:
crc32_signature(acc, 0, []) = acccrc32_signature(acc, a++b) = crc32_signature(crc32_signature(acc,a), b)— justifies UAVCAN bootloader's two-call chaining patternConcrete check value:
crc32_signature(0, 9, "123456789") = 0xCBF43926(REVENG check value for CRC-32/ISO-HDLC).Next step (Task 3): translate to Lean using same pattern as
Crc16Fold.lean.Verification Status
Files Changed
formal-verification/lean/FVSquad/SlewRate.lean— convergence section (+113 lines)formal-verification/specs/crc32_informal.md— new informal spec (+175 lines)formal-verification/TARGETS.md— updated SlewRate entry; added crc32 target [Lean Squad] feat(fv): interpolateNXY 3-pt spec (Task 4) + deadzone/expodz odd symmetry (Task 5) — run36 #35 at Phase 2