Repository navigation

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

Open

jrey8343 wants to merge 16 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 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
- Remove #[cfg(kani)] searcher abstractions; restore upstream pattern.rs
  
  jrey8343
  and
  claude
  committed
  8e64315
- Merge remote-tracking branch 'origin/main' into challenge-20-str-pattern
  jrey8343
  committed
  3c85fa3
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
Commits on Oct 7, 2026
- Merge remote-tracking branch 'origin/main' into challenge-20-str-pattern
  jrey8343
  committed
  58a19c1
- Drop the memchr stub: cfg(kani) memchr is memchr_naive since #628
  
  jrey8343
  and
  claude
  committed
  256ac0c
- Verify str iter functions (Challenge 22) over the Challenge 20 searcher contracts
  
  jrey8343
  and
  claude
  committed
  439dad2
- Retrigger CI: the macOS upstream_test runner died mid-step
  
  jrey8343
  and
  claude
  committed
  fc08a7f

Navigation Menu

Repository navigation

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

Verify safety of str iter functions (Challenge 22)#557
jrey8343 wants to merge 16 commits into
model-checking:mainfrom
jrey8343:challenge-22-str-iter

Commits on Feb 6, 2026

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

Fix CI: remove loop invariants that cause CBMC assigns check interference

Commits on Feb 11, 2026

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

Commits on Feb 21, 2026

Fix arithmetic overflow in next_match/next_match_back Kani abstractions

Commits on Apr 2, 2026

Add UTF-8 boundary constraints, fix overflow, and improve docs

Commits on Aug 18, 2026

Remove #[cfg(kani)] searcher abstractions; restore upstream pattern.rs

Merge remote-tracking branch 'origin/main' into challenge-20-str-pattern

Commits on Aug 19, 2026

Add Challenge 20 harnesses verifying the real searcher code

Commits on Sep 2, 2026

Document the Challenge 20 haystack bound as an accepted limitation

Commits on Sep 13, 2026

Add the Searcher contract to CharSearcher::next_match/next_match_back

State the CharSearcher needle clause of C byte-wise

Write next_match_back's width clause without an addition

Commits on Oct 7, 2026

Merge remote-tracking branch 'origin/main' into challenge-20-str-pattern

Drop the memchr stub: cfg(kani) memchr is memchr_naive since #628

Verify str iter functions (Challenge 22) over the Challenge 20 searcher contracts

Retrigger CI: the macOS upstream_test runner died mid-step