Ch32.2: Rabin-Karp algorithm (rolling hash + correctness)

[TankTechnology]

Scope

Section 32.2 (The Rabin-Karp algorithm).

What to formalize

• Rolling hash: h(s) = Σ s[i] · d^(m-i-1) mod q
• Hash update formula: O(1) shift of rolling hash
• Algorithm: compute pattern hash, slide window, compare hash then verify
• Correctness: finds all matches (hash collision → full string compare)
• Expected running time: O(n+m) + O((n-m+1)·m/q) spurious hits
• When q ≥ m: O(n+m) expected, O(n·m) worst-case

Mathlib support

Moderate — modular arithmetic from Ch31 reusable; list operations.

Dependencies

Can reuse modular arithmetic infrastructure from Ch31.

Difficulty

Medium — rolling hash arithmetic and expected-time analysis.