Verify safety of str iter functions (Challenge 22) - #557

Open

jrey8343 wants to merge 44 commits into

model-checking:mainfrom

jrey8343:challenge-22-str-iter

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

Make Ch22 str iter harnesses unbounded

jrey8343
and
claude
committed
80de244
Fix rustfmt and check_split_internal_get_end CI failures

jrey8343
and
claude
committed
ad3b155

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
Merge branch 'challenge-21-str-searcher' into challenge-22-str-iter
jrey8343
committed
66dcab1
Verify real str iter internals over the verified searchers

jrey8343
and
claude
committed
01296db

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
Merge branch 'challenge-21-str-searcher' into challenge-22-str-iter
jrey8343
committed
45ff80c
Share the symbolic UTF-8 input model with str::iter::verify

jrey8343
and
claude
committed
e8934ca
Merge branch 'challenge-21-str-searcher' into challenge-22-str-iter
jrey8343
committed
3e9acfc
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
Merge branch 'challenge-21-str-searcher' into challenge-22-str-iter
jrey8343
committed
092e5ca
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
Merge branch 'challenge-21-str-searcher' into challenge-22-str-iter
jrey8343
committed
e3035b7
Make the Challenge 22 proofs unbounded in string length and state

jrey8343
and
claude
committed
b46a6a9
Correct the measured figures in the Challenge 22 harness comments

jrey8343
and
claude
committed
56d8b2e