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 19 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
19 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
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