Verify safety of StrSearcher (Challenge 21) - #538

Open

jrey8343 wants to merge 32 commits into

model-checking:mainfrom

jrey8343:challenge-21-str-searcher

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 7, 2026

Commits on Feb 11, 2026

Commits on Feb 21, 2026

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

Commits on Apr 2, 2026

Commits on Aug 6, 2026

Relax TwoWaySearcher::new Kani bounds and remove unsafe from abstractions

jrey8343
and
claude
committed
941021c
Strengthen Ch21 harnesses: inductive invariant proofs with symbolic inputs

jrey8343
and
claude
committed
c0258c9

Commits on Aug 18, 2026

Commits on Aug 19, 2026

Add Challenge 20 harnesses verifying the real searcher code

jrey8343
and
claude
committed
5fd9a4a
Merge branch 'challenge-20-str-pattern' into challenge-21-str-searcher
jrey8343
committed
7bb749b
Verify real StrSearcher/TwoWaySearcher with inductive type invariant

jrey8343
and
claude
committed
89a87c0

Commits on Sep 2, 2026

Make Challenge 21 proofs haystack-unbounded and CI-fast

jrey8343
and
claude
committed
b8db0ba
Fix rustfmt alignment in type_invariant_two_way

jrey8343
and
claude
committed
9ea12d4
Retrigger CI (partition 2 runner setup flake)

jrey8343
and
claude
committed
9f8f480
Fit Challenge 21 harnesses in the autoharness job's 10-minute budget

jrey8343
and
claude
committed
aef3341
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
Merge branch 'challenge-20-str-pattern' into challenge-21-str-searcher
jrey8343
committed
3962403
Share the symbolic UTF-8 input model with str::iter::verify

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

jrey8343
and
claude
committed
7ebd1d4
Merge branch 'challenge-20-str-pattern' into challenge-21-str-searcher
jrey8343
committed
7fb05c4
Write next_match_back's width clause without an addition

jrey8343
and
claude
committed
2a548ca
Merge branch 'challenge-20-str-pattern' into challenge-21-str-searcher
jrey8343
committed
96604e8
Re-run CI after a runner shutdown killed the Kani List job

jrey8343
and
claude
committed
1ce17b2