Skip to content

Verify safety of StrSearcher (Challenge 21) #538

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jrey8343 wants to merge 32 commits into
base: main
Choose a base branch
from
Open

Verify safety of StrSearcher (Challenge 21) #538

Changes from all commits
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
bdb88ae
Verify safety of char-related Searcher methods (Challenge 20)
jrey8343 Feb 6, 2026
fd5215c
Fix CI: remove loop invariants that cause CBMC assigns check interfer…
jrey8343 Feb 6, 2026
8189681
Verify safety of StrSearcher substring search methods (Challenge 21)
jrey8343 Feb 7, 2026
3ae3b61
Apply rustfmt to fix formatting issues
jrey8343 Feb 7, 2026
323b602
Fix comment indentation to match upstream rustfmt config
jrey8343 Feb 7, 2026
94c2de4
Apply upstream rustfmt formatting via check_rustc.sh --bless
jrey8343 Feb 7, 2026
b51df2c
Abstract next_match/next_match_back with #[cfg(kani)] nondeterministi…
jrey8343 Feb 11, 2026
b2ec02c
Abstract next_match/next_match_back with #[cfg(kani)] nondeterministi…
jrey8343 Feb 11, 2026
d763699
Fix arithmetic overflow in next_match/next_match_back Kani abstractions
jrey8343 Feb 21, 2026
d50b119
Fix arithmetic overflow in next_match/next_match_back Kani abstractions
jrey8343 Feb 21, 2026
4a9c0fc
Add UTF-8 boundary constraints, fix overflow, and improve docs
jrey8343 Apr 2, 2026
bdcbda1
Add UTF-8 char boundary constraints and fix overflow in Kani abstract…
jrey8343 Apr 2, 2026
941021c
Relax TwoWaySearcher::new Kani bounds and remove unsafe from abstract…
jrey8343 Aug 6, 2026
c0258c9
Strengthen Ch21 harnesses: inductive invariant proofs with symbolic i…
jrey8343 Aug 6, 2026
8e64315
Remove #[cfg(kani)] searcher abstractions; restore upstream pattern.rs
jrey8343 Aug 18, 2026
3c85fa3
Merge remote-tracking branch 'origin/main' into challenge-20-str-pattern
jrey8343 Aug 18, 2026
5fd9a4a
Add Challenge 20 harnesses verifying the real searcher code
jrey8343 Aug 19, 2026
7bb749b
Merge branch 'challenge-20-str-pattern' into challenge-21-str-searcher
jrey8343 Aug 19, 2026
89a87c0
Verify real StrSearcher/TwoWaySearcher with inductive type invariant
jrey8343 Aug 19, 2026
b8db0ba
Make Challenge 21 proofs haystack-unbounded and CI-fast
jrey8343 Sep 2, 2026
9ea12d4
Fix rustfmt alignment in type_invariant_two_way
jrey8343 Sep 2, 2026
9f8f480
Retrigger CI (partition 2 runner setup flake)
jrey8343 Sep 2, 2026
aef3341
Fit Challenge 21 harnesses in the autoharness job's 10-minute budget
jrey8343 Sep 2, 2026
347777d
Document the Challenge 20 haystack bound as an accepted limitation
jrey8343 Sep 2, 2026
2c5b3e7
Add the Searcher contract to CharSearcher::next_match/next_match_back
jrey8343 Sep 13, 2026
3962403
Merge branch 'challenge-20-str-pattern' into challenge-21-str-searcher
jrey8343 Sep 13, 2026
e8934ca
Share the symbolic UTF-8 input model with str::iter::verify
jrey8343 Sep 13, 2026
7ebd1d4
State the CharSearcher needle clause of C byte-wise
jrey8343 Sep 13, 2026
7fb05c4
Merge branch 'challenge-20-str-pattern' into challenge-21-str-searcher
jrey8343 Sep 13, 2026
2a548ca
Write next_match_back's width clause without an addition
jrey8343 Sep 13, 2026
96604e8
Merge branch 'challenge-20-str-pattern' into challenge-21-str-searcher
jrey8343 Sep 13, 2026
1ce17b2
Re-run CI after a runner shutdown killed the Kani List job
jrey8343 Sep 13, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Loading
Loading