Verify safety of char-related Searcher methods (Challenge 20) - #537

Open

jrey8343 wants to merge 12 commits into

model-checking:mainfrom

jrey8343:challenge-20-str-pattern

Commits on Feb 6, 2026

Verify safety of char-related Searcher methods (Challenge 20)
jrey8343
committed
bdb88ae
Fix CI: remove loop invariants that cause CBMC assigns check interference
jrey8343
committed
fd5215c

Commits on Feb 11, 2026

Abstract next_match/next_match_back with #[cfg(kani)] nondeterministic overapproximation
jrey8343
committed
b51df2c

Commits on Feb 21, 2026

Fix arithmetic overflow in next_match/next_match_back Kani abstractions
jrey8343
committed
d763699

Commits on Apr 2, 2026

Add UTF-8 boundary constraints, fix overflow, and improve docs
jrey8343
committed
4a9c0fc

Commits on Aug 18, 2026

Commits on Aug 19, 2026

Add Challenge 20 harnesses verifying the real searcher code

jrey8343
and
claude
committed
5fd9a4a

Commits on Sep 2, 2026

Document the Challenge 20 haystack bound as an accepted limitation

jrey8343
and
claude
committed
347777d

Commits on Sep 13, 2026

Add the Searcher contract to CharSearcher::next_match/next_match_back

jrey8343
and
claude
committed
2c5b3e7
State the CharSearcher needle clause of C byte-wise

jrey8343
and
claude
committed
7ebd1d4
Write next_match_back's width clause without an addition

jrey8343
and
claude
committed
2a548ca