Challenge 21 (partial): bounded Kani PROBE of shipped TwoWaySearcher::next_back short-period arms

[ivmat]

What this is

A single, bounded Kani harness (check_twoway_search_back_arm_covers) that drives the unmodified,
shipped TwoWaySearcher::next_back through the real public ReverseSearcher API and proves — within
an explicitly stated bound — per-step memory safety, functional soundness of every returned Match,
bounded completeness (no silently-missed match at the fixture), and reachability of all five backward
search-loop arms.

Honest status up front: this is a PROBE, not a solution to Challenge 21. It does not satisfy the
challenge's success criteria on its own. It is offered as a differentiated partial contribution with
its residuals named at the headline, not buried.

What is proved (within the bound)

Fixture: needle "abab" (fixed; short-period, non-degenerate on both critical factorizations),
HAY_LEN = 5 (fixed), haystack content symbolic over the 3-symbol representative alphabet {a,b,z},
#[kani::unwind(6)] (VM-confirmed, every unwinding assertion SUCCESS at this bound).

• Per-step safety: every returned step is in-bounds and exactly tiles against the previous step's
  start (adjacency/no-skip), re-derived from the source, not assumed.
• Soundness: every returned Match slice is byte-for-byte equal to the needle (not merely
  in-bounds).
• Bounded completeness: the observed match set equals an independently computed closed-form
  expected match set (Option<usize>; the two candidate positions 0 and 1 are mutually exclusive at this
  fixture) — a silently-missed real match fails an assert_eq! directly.
• 5-arm non-vacuity: five kani::covers witness that all five backward arms (byteset-skip,
  left-mismatch, memory_back-guarded fast-forward, match, terminal) genuinely fire within the bound.

Oracle is proven genuine (negative controls)

The soundness oracle was shown to catch a real defect at this exact fixture (HAY_LEN=5, needle
"abab"). The completeness (no-miss) oracle's design was validated the same way, but not at this exact
fixture size — disclosed honestly below rather than glossed over.

• Soundness: a mutant (match_pos = self.end - needle.len() + 1, an off-by-one in the Match arm)
  was run against this fixture and is VM-confirmed RED: the adjacency/slice-equality oracle catches
  it directly (3 of 5 cover properties satisfied, rc=1, FAILED).
• Completeness: a mutant (a Galil-rule overshoot in the right-part-mismatch fast-forward,
  self.end -= self.period → self.end -= self.period + 1) does not diverge from the correct
  algorithm at this exact HAY_LEN=5 fixture — confirmed by exhaustive offline enumeration over all 3^5
  haystacks (0 divergent cases; the mutation is provably undetectable at this fixture size). At the
  smallest fixture size that does discriminate it (HAY_LEN=6, otherwise the same harness design and the
  same no-miss oracle shape), the same one-line mutation is VM-confirmed RED (5 of 5 cover properties
  satisfied, rc=1, FAILED on the no-miss assertion). That HAY_LEN=6 harness is a control only — it is
  not part of this submission. It confirms the no-miss oracle design is discriminating, not that it
  fires on this exact submitted fixture's completeness axis, which remains an open, disclosed residual
  (this harness's HAY_LEN=5 fixture happens to be too small for this particular Galil-rule defect class
  to surface observably; a different defect or a larger fixture might not have this gap).

What is NOT proved (residuals — headline, not footnote)

• Any other needle or needle length (this harness is one fixed short-period needle).
• Multibyte / UTF-8 char-boundary safety (the fixture is ASCII-only by construction).
• The generic (symbolic-needle, arbitrary-length) next_back.
• The MatchOnly backward path (next_match_back / rfind, where use_early_reject() == false is
  genuinely different control flow) — the 5-arm reachability here is witnessed under the RejectAndMatch
  instantiation only.
• A generic next_back safety contract is future work: it needs a symbolic-bound quantified loop
  invariant that this pinned toolchain cannot discharge (see the corrected note below).

Alternative direction toward a generic contract (diagnostic — not a commitment)

The bounded probe is not the only conceivable contribution here; the natural next rung is a generic
next_back safety contract (symbolic needle, arbitrary length). The concrete blocker is specific and
worth stating for other contributors: a generic proof needs a symbolic-bound quantified loop
invariant — a forall-quantified "no match skipped in the region already scanned" invariant on the
two-way search loop, whose stride is data-dependent (needle.len(), self.period,
i - crit_pos + 1). [Corrected 2026-08-30] At this submission's pinned toolchain (Kani d4df833 / CBMC 6.8.0), a
forall-quantified predicate whose range is not a compile-time constant is not encoded by the default
SAT backend — the quantifier is silently dropped, and this affects a flat assertion just as much as one
inside a #[kani::loop_invariant]. A quantified loop invariant over a constant range does discharge.
A generic next_back contract needs the data-dependent case, which is therefore out of scope here. We
state this as an observed limitation of this pinned toolchain, not a proof of impossibility. (An
earlier revision of this paragraph attributed the limitation to the quantifier's position — flat
assertion vs. loop invariant; a controlled 2×2 measurement at this pin showed it tracks the bound kind
instead.)

We are not claiming that adding quantified-loop-invariant support to Kani would be sufficient to
land the generic contract. The harder, still-open question is whether the two-way skip lemmas —
byteset-skip, the crit_pos left-part shift, and the period/memory fast-forward each preserving "no
match in the skipped span" — are themselves tractable as bounded or contract-backed obligations. That
is a separate analysis. This note flags the capability gap so the frontier is visible; it is not a
promise of a tool change.

Reproduce

kani verify-std -Z unstable-options ./library \
  --harness check_twoway_search_back_arm_covers \
  --cbmc-args --object-bits 12

Verified at this branch's head with Kani 0.67.0 (d4df833) / CBMC 6.8.0 (the repo's pinned
toolchain): VERIFICATION:- SUCCESSFUL, 5 of 5 cover properties satisfied.
(Unwind is pinned in-source via #[kani::unwind(6)].)

Acceptance manifest

A machine-readable statement of exactly what these proofs establish and do not establish — one entry
per claim, with declared bounds, evidence, and assurance band, checked by a standalone validator — is
shipped as a real-world example in the format's own repo:
examples/verify-rust-std-pr664/acceptance.toml
(format). It records the submitted probe (graded A3:
a red mutation control plus explicit assumes narrowing what the result covers) and an explicit A0
gap entry for what this PR does not prove (the MatchOnly backward path; a generic symbolic-needle
contract). Restamped and re-verified at this branch's head (09a3d026f66).

---

Edited 2026-08-30: corrected the quantifier characterization under "Alternative direction" after a
controlled measurement at this PR's pinned toolchain, and added the acceptance-manifest section.

[feliperodri]

Reviewed as part of Challenge 21 triage. This is a sound, honest diagnostic probe (your own header labels it PROBE -- does NOT count toward Challenge-21 success criteria), and I agree with that framing: it drives the real StrSearcher::new + ReverseSearcher::next_back (no cfg(kani) body swap), the short-period facts are asserted not assumed, and the match/adjacency oracles are real with kani::cover reachability witnesses.

But as a Ch21 solution it's 1/6 functions (next_back RejectAndMatch arm only), single concrete needle "abab", HAY_LEN=5, unwind(6) — bounded, and it doesn't define/prove the type invariant the challenge asks for. Ch21's bar remains an unbounded proof completing within CI limits; the preferred solution there is #538 (real inductive TwoWaySearcher, whose inductive step currently times out). This probe doesn't advance that bar, so it's informational rather than a competing solution — thanks for the careful, clearly-scoped diagnostics.