kmp_impl_correct preserves the pattern/text arrays and returns None exactly when no match exists, or Some i at the first matching offset. Useful for string/rope search and diff anchoring; it neither proves diff minimality nor correspondence to an arbitrary production search routine. The inspected theorem is functional correctness, not a formal runtime bound.
External evidence (contributor report)
source inspected
Proof assistant / theorem
Isabelle · kmp_impl_correct; kmp_impl_correct'
Commit / toolchain / license
80985fd56a4cb63a90176bf4bfe456eaff949bfd · Pinned AFP development snapshot; Imperative HOL, Sepref and separation-logic dependencies · BSD-2-Clause
Assumptions
Pattern and text arrays satisfy arl_assn id_assn.
The Hoare triple uses the Imperative-HOL heap semantics and separation-logic refinement framework.
Reproduction
isabelle build -D thys/Knuth_Morris_Pratt
Not run: the external proof assistant/toolchain is not installed in this workspace. Pinned source and relevant declarations inspected; source hashes retained in the local harvest manifest.
The dependent app type returns a tree whose index is the combined measure; split_tree packages its specification in a dependent result. RopeModule.v implements strings as measured chunks. Caveat: wrapper size lemmas are admitted and the sequence specialization declares an extra axiom. Treat this as qualified source evidence, not a fully audited or reproduced library.
5906d88f7096c6c6d421b81336fb344a4e2ec688 · Pinned v8.10.0 commit; package requires Coq >=8.10 and <8.11; OCaml · License not established from the inspected source snapshot
Assumptions
Measured monoid laws are explicit assumptions.
Split requires a nonempty tree and the specified measure predicate preconditions.
DependentSequence.v declares subsetT_eq_compat; FingerTree.v and FingerTreeModule.v contain admitted size lemmas.
Reproduction
Build the pinned v8.10.0 package with Coq 8.10 and its project configuration
Not run: the external proof assistant/toolchain is not installed in this workspace. Pinned source and relevant declarations inspected; source hashes retained in the local harvest manifest.
A complete external functional model for rope-like measured sequences: concatenation denotes list append; split preserves invariants and reconstructs contents at the predicate boundary; fold agrees with list fold. No formal logarithmic-time bound or refinement to a production rope library is claimed. The Hunchroom chunked-sequence model only extracts reference obligations.
80985fd56a4cb63a90176bf4bfe456eaff949bfd · Pinned AFP development snapshot; matching Isabelle development revision not established · BSD-2-Clause
Assumptions
Measured finger trees satisfy ft_invar and annotations form a monoid.
Split predicate is monotone; it fails on the initial measure and holds after the full tree measure.
Reproduction
isabelle build -D thys/Finger-Trees
Not run: the external proof assistant/toolchain is not installed in this workspace. Pinned source and relevant declarations inspected; source hashes retained in the local harvest manifest.