Theory KMP

(* 
  Verified Knuth-Morris-Pratt String Search Algorithm in LLVM.
  Adapted from Fabian Hellauer, Peter Lammich: AFP/Knuth_Morris_Pratt by 
*)
theory KMP
  imports "../sepref/IICF/IICF"
    "HOL-Library.Sublist"
begin


declare len_greater_imp_nonempty[simp del] min_absorb2[simp]

section‹Specification›text_raw‹\label{sec:spec}›

subsection‹Sublist-predicate with a position check›

subsubsection‹Definition›

text ‹One could define›
definition "sublist_at' xs ys i ≡ take (length xs) (drop i ys) = xs"  

text‹However, this doesn't handle out-of-bound indexes uniformly:›
value[nbe] "sublist_at' [] [a] 5"
value[nbe] "sublist_at' [a] [a] 5"
value[nbe] "sublist_at' [] [] 5"

text‹Instead, we use a recursive definition:›
fun sublist_at :: "'a list ⇒ 'a list ⇒ nat ⇒ bool" where
  "sublist_at (x#xs) (y#ys) 0 ⟷ x=y ∧ sublist_at xs ys 0" |
  "sublist_at xs (y#ys) (Suc i) ⟷ sublist_at xs ys i" |
  "sublist_at [] ys 0 ⟷ True" |
  "sublist_at _ [] _ ⟷ False"

text‹In the relevant cases, both definitions agree:›
lemma "i ≤ length ys ⟹ sublist_at xs ys i ⟷ sublist_at' xs ys i"
  unfolding sublist_at'_def
  by (induction xs ys i rule: sublist_at.induct) auto

text‹However, the new definition has some reasonable properties:›
subsubsection‹Properties›
lemma sublist_lengths: "sublist_at xs ys i ⟹ i + length xs ≤ length ys"
  by (induction xs ys i rule: sublist_at.induct) auto

lemma Nil_is_sublist: "sublist_at ([] :: 'x list) ys i ⟷ i ≤ length ys"
  by (induction "[] :: 'x list" ys i rule: sublist_at.induct) auto

text‹Furthermore, we need:›
lemma sublist_step[intro]:
  "⟦i + length xs < length ys; sublist_at xs ys i; ys!(i + length xs) = x⟧ ⟹ sublist_at (xs@[x]) ys i"
  apply (induction xs ys i rule: sublist_at.induct)
      apply auto
  using sublist_at.elims(3) by fastforce

lemma all_positions_sublist:
"⟦i + length xs ≤ length ys; ∀jj<length xs. ys!(i+jj) = xs!jj⟧ ⟹ sublist_at xs ys i"
proof (induction xs rule: rev_induct)
  case Nil
  then show ?case by (simp add: Nil_is_sublist)
next
  case (snoc x xs)
  from ‹i + length (xs @ [x]) ≤ length ys› have "i + length xs ≤ length ys" by simp
  moreover have "∀jj<length xs. ys!(i + jj) = xs!jj"
    by (simp add: nth_append snoc.prems(2))
  ultimately have "sublist_at xs ys i"
    using snoc.IH by simp
  then show ?case
    using snoc.prems by auto
qed

lemma sublist_all_positions: "sublist_at xs ys i ⟹ ∀jj<length xs. ys!(i+jj) = xs!jj"
  by (induction xs ys i rule: sublist_at.induct) (auto simp: nth_Cons')

text‹It also connects well to theory @{theory "HOL-Library.Sublist"} (compare @{thm[source] sublist_def}):›
lemma sublist_at_altdef:
  "sublist_at xs ys i ⟷ (∃ps ss. ys = ps@xs@ss ∧ i = length ps)"
proof (induction xs ys i rule: sublist_at.induct)
  case (2 ss t ts i)
  show "sublist_at ss (t#ts) (Suc i) ⟷ (∃xs ys. t#ts = xs@ss@ys ∧ Suc i = length xs)"
    (is "?lhs ⟷ ?rhs")
  proof
    assume ?lhs
    then have "sublist_at ss ts i" by simp
    with "2.IH" obtain xs where "∃ys. ts = xs@ss@ys ∧ i = length xs" by auto
    then have "∃ys. t#ts = (t#xs)@ss@ys ∧ Suc i = length (t#xs)" by simp
    then show ?rhs by blast
  next
    assume ?rhs
    then obtain xs where "∃ys. t#ts = xs@ss@ys ∧ Suc i = length xs" by blast
    then have "∃ys. ts = (tl xs)@ss@ys ∧ i = length (tl xs)"
      by (metis hd_Cons_tl length_0_conv list.sel(3) nat.simps(3) size_Cons_lem_eq tl_append2)
    then have "∃xs ys. ts = xs@ss@ys ∧ i = length xs" by blast
    with "2.IH" show ?lhs by simp
  qed
qed auto

corollary sublist_iff_sublist_at: "Sublist.sublist xs ys ⟷ (∃i. sublist_at xs ys i)"
  by (simp add: sublist_at_altdef Sublist.sublist_def)

subsection‹Sublist-check algorithms›

text‹
  We use the Isabelle Refinement Framework to
  phrase the specification and the algorithm. 
›
text‹@{term s} for "searchword" / "searchlist", @{term t} for "text"›
definition "kmp_SPEC s t = SPEC (λ
  None ⇒ ∄i. sublist_at s t i |
  Some i ⇒ sublist_at s t i ∧ (∀ii<i. ¬sublist_at s t ii))"

lemma is_arg_min_id: "is_arg_min id P i ⟷ P i ∧ (∀ii<i. ¬P ii)"
  unfolding is_arg_min_def by auto

lemma kmp_result: "kmp_SPEC s t =
  RETURN (if sublist s t then Some (LEAST i. sublist_at s t i) else None)"
  unfolding kmp_SPEC_def sublist_iff_sublist_at
  apply (auto intro: LeastI dest: not_less_Least split: option.splits)
  by (meson LeastI nat_neq_iff not_less_Least)

corollary weak_kmp_SPEC: "kmp_SPEC s t ≤ SPEC (λpos. pos≠None ⟷ Sublist.sublist s t)"
  by (simp add: kmp_result)

lemmas kmp_SPEC_altdefs =
  kmp_SPEC_def[folded is_arg_min_id]
  kmp_SPEC_def[folded sublist_iff_sublist_at]
  kmp_result

section‹Naive algorithm›

text‹Since KMP is a direct advancement of the naive "test-all-starting-positions" approach, we provide it here for comparison:›

subsection‹Invariants›
definition "I_out_na s t ≡ λ(i,j,pos).
  (∀ii<i. ¬sublist_at s t ii) ∧
  (case pos of None ⇒ j = 0
    | Some p ⇒ p=i ∧ sublist_at s t i)"
definition "I_in_na s t i ≡ λ(j,pos).
  case pos of None ⇒ j < length s ∧ (∀jj<j. t!(i+jj) = s!(jj))
    | Some p ⇒ sublist_at s t i"

subsection‹Algorithm›

(*Algorithm is common knowledge ⟶ remove citation here, move explanations to KMP below?*)
text‹The following definition is taken from Helmut Seidl's lecture on algorithms and data structures@{cite GAD} except that we
▪ output the identified position @{term ‹pos :: nat option›} instead of just @{const True}
▪ use @{term ‹pos :: nat option›} as break-flag to support the abort within the loops
▪ rewrite @{prop ‹i ≤ length t - length s›} in the first while-condition to @{prop ‹i + length s ≤ length t›} to avoid having to use @{typ int} for list indexes (or the additional precondition @{prop ‹length s ≤ length t›})
›

definition "naive_algorithm s t ≡ do {
  let i=0;
  let j=0;
  let pos=None;
  (_,_,pos) ← WHILEIT (I_out_na s t) (λ(i,_,pos). i + length s ≤ length t ∧ pos=None) (λ(i,j,pos). do {
    (_,pos) ← WHILEIT (I_in_na s t i) (λ(j,pos). t!(i+j) = s!j ∧ pos=None) (λ(j,_). do {
      let j=j+1;
      if j=length s then RETURN (j,Some i) else RETURN (j,None)
    }) (j,pos);
    if pos=None then do {
      let i = i + 1;
      let j = 0;
      RETURN (i,j,None)
    } else RETURN (i,j,Some i)
  }) (i,j,pos);

  RETURN pos
}"

subsection‹Correctness›

text‹The basic lemmas on @{const sublist_at} from the previous chapter together 
  with the Refinement Framework's verification condition generator / solver suffice:›

lemma "s ≠ [] ⟹ naive_algorithm s t ≤ kmp_SPEC s t"
  unfolding naive_algorithm_def kmp_SPEC_def I_out_na_def I_in_na_def
  apply (refine_vcg
    WHILEIT_rule[where R="measure (λ(i,_,pos). length t - i + (if pos = None then 1 else 0))"]
    WHILEIT_rule[where R="measure (λ(j,_::nat option). length s - j)"]
    )
                 apply (all ‹clarsimp;(auto; fail)?›)
  subgoal by (metis add_Suc_right all_positions_sublist less_antisym)
  subgoal using less_Suc_eq by blast
  subgoal by (metis less_SucE sublist_all_positions)
  subgoal by (auto split: option.splits) (metis sublist_lengths add_less_cancel_right leI le_less_trans)
  done

text‹Note that the precondition cannot be removed without an extra branch: If @{prop ‹s = []›}, the inner while-condition accesses out-of-bound memory. This will apply to KMP, too.›

section‹Knuth--Morris--Pratt algorithm›

text‹Just like our templates@{cite KMP77}@{cite GAD}, we first verify the main routine and discuss the computation of the auxiliary values @{term ‹𝔣 s›} only in a later section.›

subsection‹Preliminaries: Borders of lists›

definition "border xs ys ⟷ prefix xs ys ∧ suffix xs ys"
definition "strict_border xs ys ⟷ border xs ys ∧ length xs < length ys"
definition "intrinsic_border ls ≡ ARG_MAX length b. strict_border b ls"

subsubsection‹Properties›

interpretation border_order: order border strict_border
  by standard (auto simp: border_def suffix_def strict_border_def)
interpretation border_bot: order_bot Nil border strict_border
  by standard (simp add: border_def)

lemma borderE[elim]:
  fixes xs ys :: "'a list"
  assumes "border xs ys"
  obtains "prefix xs ys" and "suffix xs ys"
  using assms unfolding border_def by blast

lemma strict_borderE[elim]:
  fixes xs ys :: "'a list"
  assumes "strict_border xs ys"
  obtains "border xs ys" and "length xs < length ys"
  using assms unfolding strict_border_def by blast

lemma strict_border_simps[simp]:
  "strict_border xs [] ⟷ False"
  "strict_border [] (x # xs) ⟷ True"
  by (simp_all add: strict_border_def)

lemma strict_border_prefix: "strict_border xs ys ⟹ strict_prefix xs ys"
  and strict_border_suffix: "strict_border xs ys ⟹ strict_suffix xs ys"
  and strict_border_imp_nonempty: "strict_border xs ys ⟹ ys ≠ []"
  and strict_border_prefix_suffix: "strict_border xs ys ⟷ strict_prefix xs ys ∧ strict_suffix xs ys"
  by (auto simp: border_order.order.strict_iff_order border_def)

lemma border_length_le: "border xs ys ⟹ length xs ≤ length ys"
  unfolding border_def by (simp add: prefix_length_le)

lemma border_length_r_less (*rm*): "∀xs. strict_border xs ys ⟶ length xs < length ys"
  using strict_borderE by auto

lemma border_positions: "border xs ys ⟹ ∀i<length xs. ys!i = ys!(length ys - length xs + i)"
  unfolding border_def
  by (metis diff_add_inverse diff_add_inverse2 length_append not_add_less1 nth_append prefixE suffixE)

lemma all_positions_drop_length_take: "⟦i ≤ length w; i ≤ length x;
  ∀j<i. x ! j = w ! (length w + j - i)⟧
    ⟹ drop (length w - i) w = take i x"
  by (cases "i = length x") (auto intro: nth_equalityI)

lemma all_positions_suffix_take: "⟦i ≤ length w; i ≤ length x;
  ∀j<i. x ! j = w ! (length w + j - i)⟧
    ⟹ suffix (take i x) w"
  by (metis all_positions_drop_length_take suffix_drop)

lemma suffix_butlast: "suffix xs ys ⟹ suffix (butlast xs) (butlast ys)"
  unfolding suffix_def by (metis append_Nil2 butlast.simps(1) butlast_append)

lemma positions_border: "∀j<l. w!j = w!(length w - l + j) ⟹ border (take l w) w"
  by (cases "l < length w") (simp_all add: border_def all_positions_suffix_take take_is_prefix)

lemma positions_strict_border: "l < length w ⟹ ∀j<l. w!j = w!(length w - l + j) ⟹ strict_border (take l w) w"
  by (simp add: positions_border strict_border_def)

lemmas intrinsic_borderI = arg_max_natI[OF _ border_length_r_less, folded intrinsic_border_def]

lemmas intrinsic_borderI' = border_bot.bot.not_eq_extremum[THEN iffD1, THEN intrinsic_borderI]

lemmas intrinsic_border_max = arg_max_nat_le[OF _ border_length_r_less, folded intrinsic_border_def]

lemma nonempty_is_arg_max_ib: "ys ≠ [] ⟹ is_arg_max length (λxs. strict_border xs ys) (intrinsic_border ys)"
  by (simp add: intrinsic_borderI' intrinsic_border_max is_arg_max_linorder)

lemma intrinsic_border_less: "w ≠ [] ⟹ length (intrinsic_border w) < length w"
  using intrinsic_borderI[of w] border_length_r_less intrinsic_borderI' by blast

lemma intrinsic_border_take_less: "j > 0 ⟹ w ≠ [] ⟹ length (intrinsic_border (take j w)) < length w"
  by (metis intrinsic_border_less length_take less_not_refl2 min_less_iff_conj take_eq_Nil)

subsubsection‹Examples›

lemma border_example: "{b. border b ''aabaabaa''} = {'''', ''a'', ''aa'', ''aabaa'', ''aabaabaa''}"
  (is "{b. border b ?l} = {?take0, ?take1, ?take2, ?take5, ?l}")
proof
  show "{?take0, ?take1, ?take2, ?take5, ?l} ⊆ {b. border b ?l}"
    by simp eval
  have "¬border ''aab'' ?l" "¬border ''aaba'' ?l" "¬border ''aabaab'' ?l" "¬border ''aabaaba'' ?l"
    by eval+
  moreover have "{b. border b ?l} ⊆ set (prefixes ?l)"
    using border_def in_set_prefixes by blast
  ultimately show "{b. border b ?l} ⊆ {?take0, ?take1, ?take2, ?take5, ?l}"
    by auto
qed

corollary strict_border_example: "{b. strict_border b ''aabaabaa''} = {'''', ''a'', ''aa'', ''aabaa''}"
  (is "?l = ?r")
proof
  have "?l ⊆ {b. border b ''aabaabaa''}"
    by auto
  also have "… = {'''', ''a'', ''aa'', ''aabaa'', ''aabaabaa''}"
    by (fact border_example)
  finally show "?l ⊆ ?r" by auto
  show "?r ⊆ ?l" by simp eval
qed

corollary "intrinsic_border ''aabaabaa'' = ''aabaa''"
proof - ― ‹We later obtain a fast algorithm for that.›
  have exhaust: "strict_border b ''aabaabaa'' ⟷ b ∈ {'''', ''a'', ''aa'', ''aabaa''}" for b
    using strict_border_example by auto
  then have
    "¬is_arg_max length (λb. strict_border b ''aabaabaa'') ''''"
    "¬is_arg_max length (λb. strict_border b ''aabaabaa'') ''a''"
    "¬is_arg_max length (λb. strict_border b ''aabaabaa'') ''aa''"
    "is_arg_max length (λb. strict_border b ''aabaabaa'') ''aabaa''"
    unfolding is_arg_max_linorder by auto
  moreover have "strict_border (intrinsic_border ''aabaabaa'') ''aabaabaa''"
    using intrinsic_borderI' by blast
  note this[unfolded exhaust]
  ultimately show ?thesis
    by simp (metis list.discI nonempty_is_arg_max_ib)
qed

subsection‹Main routine›

text‹The following is Seidl's "border"-table@{cite GAD} (values shifted by 1 so we don't need @{typ int}),
or equivalently, "f" from Knuth's, Morris' and Pratt's paper@{cite KMP77} (with indexes starting at 0).›
fun 𝔣 :: "'a list ⇒ nat ⇒ nat" where
  "𝔣 s 0 = 0" ― ‹This increments the compare position while @{prop ‹j=(0::nat)›}› |
  "𝔣 s j = length (intrinsic_border (take j s)) + 1"
text‹Note that we use their "next" only implicitly.›

subsubsection‹Invariants›
definition "I_outer s t ≡ λ(i,j,pos).
  (∀ii<i. ¬sublist_at s t ii) ∧
  (i≤length t) ∧
  (case pos of None ⇒ (∀jj<j. t!(i+jj) = s!(jj)) ∧ j < length s
    | Some p ⇒ p=i ∧ sublist_at s t i)"
text‹For the inner loop, we can reuse @{const I_in_na}.›

subsubsection‹Algorithm›
text‹First, we use the non-evaluable function @{const 𝔣} directly:›
definition "kmp s t ≡ do {
  ASSERT (s ≠ []);
  let i=0;
  let j=0;
  let pos=None;
  (_,_,pos) ← WHILEIT (I_outer s t) (λ(i,j,pos). i + length s ≤ length t ∧ pos=None) (λ(i,j,pos). do {
    ASSERT (i + length s ≤ length t);
    (j,pos) ← WHILEIT (I_in_na s t i) (λ(j,pos). t!(i+j) = s!j ∧ pos=None) (λ(j,pos). do {
      let j=j+1;
      if j=length s then RETURN (j,Some i) else RETURN (j,None)
    }) (j,pos);
    if pos=None then do {
      ASSERT (j < length s ∧ 𝔣 s j ≤ j);
      let i = i + (j - 𝔣 s j + 1);
      let j = max 0 (𝔣 s j - 1); ― ‹‹max› not necessary, but indicates that subtraction may actually underflow›
      RETURN (i,j,None)
    } else RETURN (i,j,Some i)
  }) (i,j,pos);

  RETURN pos
}"

subsubsection‹Correctness›
lemma 𝔣_eq_0_iff_j_eq_0[simp]: "𝔣 s j = 0 ⟷ j = 0"
  by (cases j) simp_all

lemma j_le_𝔣_le: "j ≤ length s ⟹ 𝔣 s j ≤ j"
  apply (cases j)
  apply simp_all
  by (metis Suc_leI intrinsic_border_less length_take list.size(3) min.absorb2 nat.simps(3) not_less)

lemma j_le_𝔣_le': "0 < j ⟹ j ≤ length s ⟹ 𝔣 s j - 1 < j"
  by (metis diff_less j_le_𝔣_le le_eq_less_or_eq less_imp_diff_less less_one)

lemma 𝔣_le: "s ≠ [] ⟹ 𝔣 s j - 1 < length s"
  by (cases j) (simp_all add: intrinsic_border_take_less)

(*
  Only needed for run-time analysis
*)
lemma "p576 et seq":
  assumes
    "j ≤ length s" and
    assignments:
    "i' = i + (j + 1 - 𝔣 s j)"
    "j' = max 0 (𝔣 s j - 1)"
  shows
    sum_no_decrease: "i' + j' ≥ i + j" and
    i_increase: "i' > i"
  using assignments by (simp_all add: j_le_𝔣_le[OF assms(1), THEN le_imp_less_Suc])

lemma reuse_matches: 
  assumes j_le: "j ≤ length s"
  and old_matches: "∀jj<j. t ! (i + jj) = s ! jj"
  shows "∀jj<𝔣 s j - 1. t ! (i + (j - 𝔣 s j + 1) + jj) = s ! jj"
    (is "∀jj<?j'. t ! (?i' + jj) = s ! jj")
proof (cases "j>0")
  assume "j>0"
  have 𝔣_le: "𝔣 s j ≤ j"
    by (simp add: j_le j_le_𝔣_le)
  with old_matches have 1: "∀jj<?j'. t ! (?i' + jj) = s ! (j - 𝔣 s j + 1 + jj)"
    by (metis ab_semigroup_add_class.add.commute add.assoc diff_diff_cancel less_diff_conv)
  have [simp]: "length (take j s) = j" "length (intrinsic_border (take j s)) = ?j'"
    by (simp add: j_le) (metis ‹0 < j› diff_add_inverse2 𝔣.elims nat_neq_iff)
  then have "∀jj<?j'. take j s ! jj = take j s ! (j - (𝔣 s j - 1) + jj)"
    by (metis intrinsic_borderI' ‹0 < j› border_positions length_greater_0_conv strict_border_def)
  then have "∀jj<?j'. take j s ! jj = take j s ! (j - 𝔣 s j + 1 + jj)"
    by (simp add: 𝔣_le)
  then have 2: "∀jj<?j'. s ! (j - 𝔣 s j + 1 + jj) = s ! jj"
    using 𝔣_le by simp
  from 1 2 show ?thesis by simp
qed simp

theorem shift_safe:
  assumes
    "∀ii<i. ¬sublist_at s t ii"
    "t!(i+j) ≠ s!j" and
    [simp]: "j < length s" and
    matches: "∀jj<j. t!(i+jj) = s!jj"
  defines
    assignment: "i' ≡ i + (j - 𝔣 s j + 1)"
  shows
    "∀ii<i'. ¬sublist_at s t ii"
proof (standard, standard)
  fix ii
  assume "ii < i'"
  then consider ― ‹The position falls into one of three categories:›
    (old) "ii < i" |
    (current) "ii = i" |
    (skipped) "ii > i"
    by linarith
  then show "¬sublist_at s t ii"
  proof cases
    case old ― ‹Old position, use invariant.›
    with ‹∀ii<i. ¬sublist_at s t ii› show ?thesis by simp
  next
    case current ― ‹The mismatch occurred while testing this alignment.›
    with ‹t!(i+j) ≠ s!j› show ?thesis
      using sublist_all_positions[of s t i] by auto
  next
    case skipped ― ‹The skipped positions.›
    then have "0<j"
      using ‹ii < i'› assignment by linarith
    then have less_j[simp]: "j + i - ii < j" and le_s: "j + i - ii ≤ length s"
      using ‹ii < i'› assms(3) skipped by linarith+
    note 𝔣_le[simp] = j_le_𝔣_le[OF assms(3)[THEN less_imp_le]]
    have "0 < 𝔣 s j"
      using ‹0 < j› 𝔣_eq_0_iff_j_eq_0 neq0_conv by blast
    then have "j + i - ii > 𝔣 s j - 1"
      using ‹ii < i'› assignment 𝔣_le by linarith
    then have contradiction_goal: "j + i - ii > length (intrinsic_border (take j s))"
      by (metis 𝔣.elims ‹0 < j› add_diff_cancel_right' not_gr_zero)
    show ?thesis
    proof
      assume "sublist_at s t ii"
      note sublist_all_positions[OF this]
      with le_s have a: "∀jj < j+i-ii. t!(ii+jj) = s!jj"
        by simp
      have ff1: "¬ ii < i"
        by (metis not_less_iff_gr_or_eq skipped)
      then have "i + (ii - i + jj) = ii + jj" for jj
        by (metis add.assoc add_diff_inverse_nat)
      then have "¬ jj < j + i - ii ∨ t ! (ii + jj) = s ! (ii - i + jj)" if "ii - i + jj < j" for jj
        using that ff1 by (metis matches)
      then have "¬ jj < j + i - ii ∨ t ! (ii + jj) = s ! (ii - i + jj)" for jj
        using ff1 by auto
      with matches have "∀jj < j+i-ii. t!(ii+jj) = s!(ii-i+jj)" by metis
      then have "∀jj < j+i-ii. s!jj = s!(ii-i+jj)"
        using a by auto
      then have "∀jj < j+i-ii. (take j s)!jj = (take j s)!(ii-i+jj)"
        using ‹i<ii› by auto
      with positions_strict_border[of "j+i-ii" "take j s", simplified]
      have "strict_border (take (j+i-ii) s) (take j s)".
      note intrinsic_border_max[OF this]
      also note contradiction_goal
      also have "j+i-ii ≤ length s" by (fact le_s)
      ultimately
      show False by simp
    qed
  qed
qed

lemma kmp_correct: "s ≠ []
  ⟹ kmp s t ≤ kmp_SPEC s t"
  unfolding kmp_def kmp_SPEC_def I_outer_def I_in_na_def
  apply (refine_vcg
    WHILEIT_rule[where R="measure (λ(i,_,pos). length t - i + (if pos = None then 1 else 0))"]
    WHILEIT_rule[where R="measure (λ(j,_::nat option). length s - j)"]
    )
  apply (all ‹clarsimp;(auto; fail)?›)
  subgoal by (metis add_Suc_right all_positions_sublist less_antisym)
  subgoal using less_antisym by blast
  subgoal for i jout j using j_le_𝔣_le[of j s] by simp
  subgoal for i jout j using shift_safe[of i s t j] by fastforce
  subgoal for i jout j using reuse_matches[of j s t i] 𝔣_le by simp
  subgoal by (auto split: option.splits) (metis sublist_lengths add_less_cancel_right leI le_less_trans)
  done

subsubsection‹Storing the @{const 𝔣}-values›
text‹We refine the algorithm to compute the @{const 𝔣}-values only once at the start:›
definition compute_𝔣s_SPEC :: "'a list ⇒ nat list nres" where
  "compute_𝔣s_SPEC s ≡ SPEC (λ𝔣s. length 𝔣s = length s + 1 ∧ (∀j≤length s. 𝔣s!j = 𝔣 s j))"

definition "kmp1 s t ≡ do {
  ASSERT (s ≠ []);
  let i=0;
  let j=0;
  let pos=None;
  𝔣s ← compute_𝔣s_SPEC (butlast s); ― ‹At the last char, we abort instead.›
  ASSERT (length 𝔣s = length s);
  (_,_,pos) ← WHILEIT (I_outer s t) (λ(i,j,pos). i + length s ≤ length t ∧ pos=None) (λ(i,j,pos). do {
    ASSERT (i + length s ≤ length t);
    (j,pos) ← WHILEIT (I_in_na s t i) (λ(j,pos). t!(i+j) = s!j ∧ pos=None) (λ(j,pos). do {
      let j=j+1;
      if j=length s then RETURN (j,Some i) else RETURN (j,None)
    }) (j,pos);
    if pos=None then do {
      ASSERT (j < length 𝔣s ∧ 𝔣s!j ≤ j);
      let i = i + (j - 𝔣s!j + 1);
      let j = max 0 (𝔣s!j - 1); ― ‹‹max› not necessary›
      RETURN (i,j,None)
    } else RETURN (i,j,Some i)
  }) (i,j,pos);

  RETURN pos
}"

lemma 𝔣_butlast[simp]: "j < length s ⟹ 𝔣 (butlast s) j = 𝔣 s j"
  by (cases j) (simp_all add: take_butlast)

lemma kmp1_refine: "kmp1 s t ≤ kmp s t"
  apply (rule refine_IdD)
  unfolding kmp1_def kmp_def Let_def compute_𝔣s_SPEC_def nres_monad_laws
  apply (intro ASSERT_refine_right ASSERT_refine_left)
   apply simp
  apply (rule Refine_Basic.intro_spec_refine)
  apply refine_rcg
                apply refine_dref_type
                apply auto
  done

text‹Next, an algorithm that satisfies @{const compute_𝔣s_SPEC}:›
subsection‹Computing @{const 𝔣}›
subsubsection‹Invariants›

definition "I_out_cb s ≡ λ(𝔣s,i,j).
  length s + 1 = length 𝔣s ∧
  (∀jj<j. 𝔣s!jj = 𝔣 s jj) ∧
  𝔣s!(j-1) = i ∧
  0 < j"
definition "I_in_cb s j ≡ λi.
  if j=1 then i=0 ― ‹first iteration›
  else
    strict_border (take (i-1) s) (take (j-1) s) ∧
    𝔣 s j ≤ i + 1"

subsubsection‹Algorithm›

text‹Again, we follow Seidl@{cite GAD}, p.582. Apart from the +1-shift, we make another modification:
Instead of directly setting @{term ‹𝔣s!1›}, we let the first loop-iteration (if there is one) do that for us.
This allows us to remove the precondition @{prop ‹s ≠ []›}, as the index bounds are respected even in that corner case.›

definition compute_𝔣s :: "'a list ⇒ nat list nres" where
  "compute_𝔣s s = do {
  let 𝔣s=replicate (length s + 1) 0; ― ‹only the first 0 is needed›
  let i=0;
  let j=1;
  (𝔣s,_,_) ← WHILEIT (I_out_cb s) (λ(𝔣s,_,j). j < length 𝔣s) (λ(𝔣s,i,j). do {
    i ← WHILEIT (I_in_cb s j) (λi. i>0 ∧ s!(i-1) ≠ s!(j-1)) (λi. do {
      ASSERT (i-1 < length 𝔣s);
      let i=𝔣s!(i-1);
      RETURN i
    }) i;
    ASSERT (i < length 𝔣s);
    let i=i+1;
    ASSERT (j < length 𝔣s);
    let 𝔣s=𝔣s[j:=i];
    let j=j+1;
    RETURN (𝔣s,i,j)
  }) (𝔣s,i,j);
  
  RETURN 𝔣s
}"

subsubsection‹Correctness›
lemma take_length_ib[simp]:
  assumes "0 < j" "j ≤ length s"
    shows "take (length (intrinsic_border (take j s))) s = intrinsic_border (take j s)"
proof -
  from assms have "prefix (intrinsic_border (take j s)) (take j s)"
    by (metis intrinsic_borderI' border_def list.size(3) neq0_conv not_less strict_border_def take_eq_Nil)
  also have "prefix (take j s) s"
    by (simp add: ‹j ≤ length s› take_is_prefix)
  finally show ?thesis
    by (metis append_eq_conv_conj prefixE)
qed

lemma ib_singleton[simp]: "intrinsic_border [z] = []"
  by (metis intrinsic_border_less length_Cons length_greater_0_conv less_Suc0 list.size(3))

lemma border_butlast: "border xs ys ⟹ border (butlast xs) (butlast ys)"
  apply (auto simp: border_def)
   apply (metis butlast_append prefixE prefix_order.eq_refl prefix_prefix prefixeq_butlast)
  apply (metis Sublist.suffix_def append.right_neutral butlast.simps(1) butlast_append)
  done

corollary strict_border_butlast: "xs ≠ [] ⟹ strict_border xs ys ⟹ strict_border (butlast xs) (butlast ys)"
  unfolding strict_border_def by (simp add: border_butlast less_diff_conv)

lemma border_take_lengths: "i ≤ length s ⟹ border (take i s) (take j s) ⟹ i ≤ j"
  using border_length_le by fastforce

lemma border_step: "border xs ys ⟷ border (xs@[ys!length xs]) (ys@[ys!length xs])"
  apply (auto simp: border_def suffix_def)
  using append_one_prefix prefixE apply fastforce
  using append_prefixD apply blast
  done

corollary strict_border_step: "strict_border xs ys ⟷ strict_border (xs@[ys!length xs]) (ys@[ys!length xs])"
  unfolding strict_border_def using border_step by auto

lemma ib_butlast: "length w ≥ 2 ⟹ length (intrinsic_border w) ≤ length (intrinsic_border (butlast w)) + 1"
proof -
  assume "length w ≥ 2"
  then have "w ≠ []" by auto
  then have "strict_border (intrinsic_border w) w"
    by (fact intrinsic_borderI')
  with ‹2 ≤ length w› have "strict_border (butlast (intrinsic_border w)) (butlast w)"
    by (metis One_nat_def border_bot.bot.not_eq_extremum butlast.simps(1) len_greater_imp_nonempty length_butlast lessI less_le_trans numerals(2) strict_border_butlast zero_less_diff)
  then have "length (butlast (intrinsic_border w)) ≤ length (intrinsic_border (butlast w))"
    using intrinsic_border_max by blast
  then show ?thesis
    by simp
qed

lemma take_Suc0: 
  "l≠[] ⟹ take (Suc 0) l = [l!0]" 
  "0 < length l ⟹ take (Suc 0) l = [l!0]" 
  "Suc n ≤ length l ⟹ take (Suc 0) l = [l!0]" 
  by (cases l, auto)+


corollary 𝔣_Suc(*rm*): "Suc i ≤ length w ⟹ 𝔣 w (Suc i) ≤ 𝔣 w i + 1"
  apply (cases i)
  apply (simp_all add: take_Suc0)
  by (metis One_nat_def Suc_eq_plus1 Suc_to_right butlast_take diff_is_0_eq ib_butlast length_take min.absorb2 nat.simps(3) not_less_eq_eq numerals(2))

lemma 𝔣_step_bound(*rm*):
  assumes "j ≤ length w"
  shows "𝔣 w j ≤ 𝔣 w (j-1) + 1"
  using assms[THEN j_le_𝔣_le] 𝔣_Suc assms
  by (metis One_nat_def Suc_pred le_SucI not_gr_zero trans_le_add2)

lemma border_take_𝔣: "border (take (𝔣 s i - 1) s ) (take i s)"
  apply (cases i, simp_all)
  by (metis intrinsic_borderI' border_order.eq_iff border_order.less_imp_le border_positions nat.simps(3) nat_le_linear positions_border take_all take_eq_Nil take_length_ib zero_less_Suc)

corollary 𝔣_strict_borderI: "y = 𝔣 s (i-1) ⟹ strict_border (take (i-1) s) (take (j-1) s) ⟹ strict_border (take (y-1) s) (take (j-1) s)"
  using border_order.less_le_not_le border_order.order.trans border_take_𝔣 by blast

corollary strict_border_take_𝔣: "0 < i ⟹ i ≤ length s ⟹ strict_border (take (𝔣 s i - 1) s ) (take i s)"
  by (meson border_order.less_le_not_le border_take_𝔣 border_take_lengths j_le_𝔣_le' leD)

lemma 𝔣_is_max: "j ≤ length s ⟹ strict_border b (take j s) ⟹ 𝔣 s j ≥ length b + 1"
  by (metis 𝔣.elims add_le_cancel_right add_less_same_cancel2 border_length_r_less intrinsic_border_max length_take min_absorb2 not_add_less2)

theorem skipping_ok:
  assumes j_bounds[simp]: "1 < j" "j ≤ length s"
    and mismatch: "s!(i-1) ≠ s!(j-1)"
    and greater_checked: "𝔣 s j ≤ i + 1"
    and "strict_border (take (i-1) s) (take (j-1) s)"
  shows "𝔣 s j ≤ 𝔣 s (i-1) + 1"
proof (rule ccontr)
  assume "¬𝔣 s j ≤ 𝔣 s (i-1) + 1"
  then have i_bounds: "0 < i" "i ≤ length s"
    using greater_checked assms(5) take_Nil by fastforce+
  then have i_less_j: "i < j"
    using assms(5) border_length_r_less nz_le_conv_less by auto
  from ‹¬𝔣 s j ≤ 𝔣 s (i-1) + 1› greater_checked consider
    (tested) "𝔣 s j = i + 1" ― ‹This contradicts @{thm mismatch}› |
    (skipped) "𝔣 s (i-1) + 1 < 𝔣 s j" "𝔣 s j ≤ i"
      ― ‹This contradicts @{thm 𝔣_is_max[of "i-1" s]}›
    by linarith
  then show False
  proof cases
    case tested
    then have "𝔣 s j - 1 = i" by simp
    moreover note border_positions[OF border_take_𝔣[of s j, unfolded this]]
    ultimately have "take j s ! (i-1) = s!(j-1)" using i_bounds i_less_j by simp
    with ‹i < j› have "s!(i-1) = s!(j-1)"
      by (simp add: less_imp_diff_less)
    with mismatch show False..
  next
    case skipped
    let ?border = "take (i-1) s"
      ― ‹This border of @{term ‹take (j-1) s›} could not be extended to a border of @{term ‹take j s›} due to the mismatch.›
    let ?impossible = "take (𝔣 s j - 2) s"
      ― ‹A strict border longer than @{term ‹intrinsic_border ?border›}, a contradiction.›
    have "length (take j s) = j"
      by simp
    have "𝔣 s j - 2 < i - 1"
      using skipped by linarith
    then have less_s: "𝔣 s j - 2 < length s" "i - 1 < length s"
      using ‹i < j› j_bounds(2) by linarith+
    then have strict: "length ?impossible < length ?border"
      using ‹𝔣 s j - 2 < i - 1› by auto
    moreover {
      have "prefix ?impossible (take j s)"
        using prefix_length_prefix take_is_prefix
        by (metis (no_types, lifting) ‹length (take j s) = j› j_bounds(2) diff_le_self j_le_𝔣_le length_take less_s(1) min_simps(2) order_trans)
      moreover have "prefix ?border (take j s)"
        by (metis (no_types, lifting) ‹length (take j s) = j› diff_le_self i_less_j le_trans length_take less_or_eq_imp_le less_s(2) min_simps(2) prefix_length_prefix take_is_prefix)
      ultimately have "prefix ?impossible ?border"
        using strict less_imp_le_nat prefix_length_prefix by blast
    } moreover {
      have "suffix (take (𝔣 s j - 1) s) (take j s)" using border_take_𝔣
        by (auto simp: border_def)
      note suffix_butlast[OF this]
      then have "suffix ?impossible (take (j-1) s)"
        by (metis One_nat_def j_bounds(2) butlast_take diff_diff_left 𝔣_le len_greater_imp_nonempty less_or_eq_imp_le less_s(2) one_add_one)
      then have "suffix ?impossible (take (j-1) s)" "suffix ?border (take (j-1) s)"
        using assms(5) by auto
      from suffix_length_suffix[OF this strict[THEN less_imp_le]]
        have "suffix ?impossible ?border".
    }
    ultimately have "strict_border ?impossible ?border"
      unfolding strict_border_def[unfolded border_def] by blast
    note 𝔣_is_max[of "i-1" s, OF _ this]
    then have "length (take (𝔣 s j - 2) s) + 1 ≤ 𝔣 s (i-1)"
      using less_imp_le_nat less_s(2) by blast
    then have "𝔣 s j - 1 ≤ 𝔣 s (i-1)"
      by (simp add: less_s(1))
    then have "𝔣 s j ≤ 𝔣 s (i-1) + 1"
      using le_diff_conv by blast
    with skipped(1) show False
      by linarith
  qed
qed

lemma extend_border:
  assumes "j ≤ length s"
  assumes "s!(i-1) = s!(j-1)"
  assumes "strict_border (take (i-1) s) (take (j-1) s)"
  assumes "𝔣 s j ≤ i + 1"
  shows "𝔣 s j = i + 1"
proof -
  from assms(3) have pos_in_range: "i - 1 < length s " "length (take (i-1) s) = i - 1"
    using border_length_r_less min_less_iff_conj by auto
  with strict_border_step[THEN iffD1, OF assms(3)] have "strict_border (take (i-1) s @ [s!(i-1)]) (take (j-1) s @ [s!(i-1)])"
    by (metis assms(3) border_length_r_less length_take min_less_iff_conj nth_take)
  with pos_in_range have "strict_border (take i s) (take (j-1) s @ [s!(i-1)])"
    by (metis Suc_eq_plus1 Suc_pred add.left_neutral border_bot.bot.not_eq_extremum border_order.less_asym neq0_conv take_0 take_Suc_conv_app_nth)
  then have "strict_border (take i s) (take (j-1) s @ [s!(j-1)])"
    by (simp only: ‹s!(i-1) = s!(j-1)›)
  then have "strict_border (take i s) (take j s)"
    by (metis One_nat_def Suc_pred assms(1,3) diff_le_self less_le_trans neq0_conv nz_le_conv_less strict_border_imp_nonempty take_Suc_conv_app_nth take_eq_Nil)
  with 𝔣_is_max[OF assms(1) this] have "𝔣 s j ≥ i + 1"
    using Suc_leI by fastforce
  with ‹𝔣 s j ≤ i + 1› show ?thesis
    using le_antisym by presburger
qed

lemma compute_𝔣s_correct: "compute_𝔣s s ≤ compute_𝔣s_SPEC s"
  unfolding compute_𝔣s_SPEC_def compute_𝔣s_def I_out_cb_def I_in_cb_def
  apply (simp, refine_vcg
    WHILEIT_rule[where R="measure (λ(𝔣s,i,j). length s + 1 - j)"]
    WHILEIT_rule[where R="measure id"] ― ‹@{term ‹i::nat›} decreases with every iteration.›
    )
  apply (clarsimp_all, fold One_nat_def)
  subgoal for b j by (rule strict_border_take_𝔣, auto)
  subgoal by (metis Suc_eq_plus1 𝔣_step_bound less_Suc_eq_le)
  subgoal by fastforce
  subgoal
    by (metis (no_types, lifting) One_nat_def Suc_lessD Suc_pred border_length_r_less 𝔣_strict_borderI length_take less_Suc_eq less_Suc_eq_le min.absorb2)
  subgoal for b j i
    by (metis (no_types, lifting) One_nat_def Suc_diff_1 Suc_eq_plus1 Suc_leI border_take_lengths less_Suc_eq_le less_antisym skipping_ok strict_border_def)
  subgoal by (metis Suc_diff_1 border_take_lengths j_le_𝔣_le less_Suc_eq_le strict_border_def)
  subgoal by (metis Suc_eq_plus1 𝔣_le border_order.less_irrefl diff_Suc_1 extend_border less_SucI less_Suc_eq_le take_Nil zero_less_Suc)
  subgoal for b j i jj
    by (metis Suc_eq_plus1 Suc_eq_plus1_left add.right_neutral extend_border 𝔣_eq_0_iff_j_eq_0 j_le_𝔣_le le_zero_eq less_Suc_eq less_Suc_eq_le nth_list_update_eq nth_list_update_neq)
  subgoal by linarith
  done

subsubsection‹Index shift›
text‹To avoid inefficiencies, we refine @{const compute_𝔣s} to take @{term s}
instead of @{term ‹butlast s›} (it still only uses @{term ‹butlast s›}).›
definition compute_butlast_𝔣s :: "'a list ⇒ nat list nres" where
  "compute_butlast_𝔣s s = do {
  let 𝔣s=replicate (length s) 0;
  let i=0;
  let j=1;
  (𝔣s,_,_) ← WHILEIT (I_out_cb (butlast s)) (λ(b,i,j). j < length b) (λ(𝔣s,i,j). do {
    ASSERT (1≤j ∧ j < length 𝔣s);
    i ← WHILEIT (I_in_cb (butlast s) j) (λi. i>0 ∧ s!(i-1) ≠ s!(j-1)) (λi. do {
      ASSERT (1≤i ∧ i-1 < length 𝔣s);
      let i=𝔣s!(i-1);
      RETURN i
    }) i;
    ASSERT (length 𝔣s = length s);
    ASSERT (i < length 𝔣s);
    let i=i+1;
    ASSERT (j < length 𝔣s);
    let 𝔣s=𝔣s[j:=i];
    let j=j+1;
    RETURN (𝔣s,i,j)
  }) (𝔣s,i,j);
  
  RETURN 𝔣s
}"

lemma compute_𝔣s_inner_bounds: 
  assumes "I_out_cb s (𝔣s,ix,j)"
  assumes "j < length 𝔣s"
  assumes "I_in_cb s j i"
  shows "1≤j" "i-1 < length s" "j-1 < length s"
  using assms by (auto simp: I_out_cb_def I_in_cb_def split: if_splits)

lemma compute_butlast_𝔣s_refine[refine]:
  assumes "(s,s') ∈ br butlast ((≠) [])"
  shows "compute_butlast_𝔣s s ≤ ⇓ Id (compute_𝔣s_SPEC s')"
proof -
  have "compute_butlast_𝔣s s ≤ ⇓ Id (compute_𝔣s s')"
    unfolding compute_butlast_𝔣s_def compute_𝔣s_def 
    apply (refine_rcg)
              apply (refine_dref_type)
    using assms apply (clarsimp_all simp: in_br_conv)
     apply (metis Suc_pred length_greater_0_conv replicate_Suc)
     apply (simp add: I_out_cb_def)
     apply (metis One_nat_def compute_𝔣s_inner_bounds(2-) nth_butlast)
     apply (simp add: I_out_cb_def)
     done
     
  also note compute_𝔣s_correct
  finally show ?thesis by simp
qed

  


subsection‹Conflation›
text‹We replace @{const compute_𝔣s_SPEC} with @{const compute_butlast_𝔣s}›
definition "kmp2 s t ≡ do {
  ASSERT (s ≠ []);
  let i=0;
  let j=0;
  let pos=None;
  𝔣s ← compute_butlast_𝔣s s;
  ASSERT (length 𝔣s = length s);
  (_,_,pos) ← monadic_WHILEIT (I_outer s t) 
    (λ(i,j,pos). do { ASSERT(i≤length t); RETURN (i + length s ≤ length t ∧ pos=None)} ) 
    (λ(i,j,pos). do {
      ASSERT (i + length s ≤ length t ∧ pos=None);
      (j,pos) ← monadic_WHILEIT (I_in_na s t i) 
        (λ(j,pos). do { ASSERT(pos=None ⟶ i+j<length t ∧ j<length s); RETURN (pos=None ∧ t!(i+j) = s!j) }) 
        (λ(j,pos). do {
          ASSERT (j<length s);
          let j=j+1;
          if j=length s then RETURN (j,Some i) else RETURN (j,None)
        }) (j,pos);
      if pos=None then do {
        ASSERT (j < length 𝔣s ∧ 𝔣s!j ≤ j);
        let i = i + (j - 𝔣s!j + 1);
        let j = op_nat_sub_ovf (𝔣s!j) 1; ― ‹Explicitly select 0-saturating subtraction›
        RETURN (i,j,None)
      } else RETURN (i,j,Some i)
    }) (i,j,pos);

  RETURN pos
}"

text‹Using @{thm [source] compute_butlast_𝔣s_refine} (it has attribute @{attribute refine}), the proof is trivial:›
lemma kmp2_refine: "kmp2 s t ≤ kmp1 s t"
  apply (rule refine_IdD)
  unfolding kmp2_def kmp1_def
  apply refine_rcg
                  apply refine_dref_type
                  apply (auto simp: in_br_conv I_outer_def I_in_na_def split: option.splits)
  done

lemma kmp2_correct: "s ≠ []
  ⟹ kmp2 s t ≤ kmp_SPEC s t"
proof -
  assume "s ≠ []"
  have "kmp2 s t ≤ kmp1 s t" by (fact kmp2_refine)
  also have "... ≤ kmp s t" by (fact kmp1_refine)
  also have "... ≤ kmp_SPEC s t" by (fact kmp_correct[OF ‹s ≠ []›])
  finally show ?thesis.
qed

text‹For convenience, we also remove the precondition:›
definition "kmp3 s t ≡ do {
  if s=[] then RETURN (Some 0) else kmp2 s t
}"

lemma kmp3_correct: "kmp3 s t ≤ kmp_SPEC s t"
  unfolding kmp3_def by (simp add: kmp2_correct) (simp add: kmp_SPEC_def)

  
  
section ‹Refinement to Imperative/HOL›

(* TODO: Use monadic_WHILEIT also in compute_𝔣s *)
lemmas in_bounds_aux = compute_𝔣s_inner_bounds[of "butlast s" for s, simplified]

subsection ‹Setup›
text ‹We fix a 64 bit type for string positions,
  and an 8 bit type for string content (characters)
›

type_synonym size_t = 64
abbreviation "size_t_assn ≡ snat_assn' TYPE(size_t)"

abbreviation "char_assn ≡ word_assn' TYPE(8)"
  
text ‹A string is represented as array with length value›
abbreviation "string_assn ≡ larray_assn' TYPE(size_t) char_assn"  

text ‹Also the lookup table is represented as array with length value.›
(* TODO: Do we ever need length of lookup table?
  We do, but could easily change algorithm such that it does not lookup this length!
*)
abbreviation "tab_assn ≡ larray_assn' TYPE(size_t) size_t_assn"
(*abbreviation "tab_assn ≡ array_assn size_t_assn" *) 
  
subsection ‹Refinement of Lookup Table Computation›
sepref_def compute_butlast_𝔣s_impl is compute_butlast_𝔣s 
  :: "[λs. length s < max_snat LENGTH(size_t)]⇩a (string_assn)⇧k → tab_assn"
  unfolding compute_butlast_𝔣s_def
  apply (rewrite in "WHILEIT _ ⌑" short_circuit_conv)+
  supply [[goals_limit = 1]]
  apply (annot_snat_const "TYPE(size_t)")
  apply (rewrite larray.fold_replicate_init)
  supply in_bounds_aux[dest]
  apply sepref
  done
  
(*prepare_code_thms (LLVM) [llvm_code] compute_butlast_𝔣s_impl_def*)
(*declare compute_butlast_𝔣s_impl_def[llvm_code]*)

llvm_deps compute_butlast_𝔣s_impl
export_llvm compute_butlast_𝔣s_impl

(*declare compute_butlast_𝔣s_impl.refine[sepref_fr_rules]*)

sepref_register compute_𝔣s


subsection ‹Refinement of Main Algorithm›


abbreviation "result_assn ≡ snat_option_assn' TYPE(size_t)"
  
sepref_def kmp_impl is "uncurry kmp3" 
  :: "[λ(s,t). length s + length t < max_snat LENGTH(size_t) ]⇩a 
      (string_assn)⇧k *⇩a (string_assn)⇧k → result_assn"
  unfolding kmp3_def kmp2_def
  apply (rewrite in "RETURN ⌑" in "monadic_WHILEIT (I_in_na _ _ _) ⌑" short_circuit_conv)
  supply [[goals_limit = 3]]
  apply (annot_snat_const "TYPE(size_t)")
  
  apply sepref_dbg_keep
  done
  
definition [llvm_code,llvm_inline]: "kmp_impl' ap bp ≡ doM {
  a ← ll_load ap;
  b ← ll_load bp;
  kmp_impl a b
}"


export_llvm 
  compute_butlast_𝔣s_impl
  kmp_impl' is "_ kmp(string*,string*)"
  defines ‹
    typedef struct {int64_t len; char *str;} string;
  ›
  file "code/kmp.ll"
  
export_llvm 
  kmp_impl' is "_ kmp(string*,string*)"
  defines ‹
    typedef struct {int64_t len; char *str;} string;
  ›
  file "../../regression/gencode/kmp.ll"

section ‹Overall Correctness Theorem›
    
lemma kmp3_correct':
  "(uncurry kmp3, uncurry kmp_SPEC) ∈ Id ×⇩r Id →⇩f ⟨Id⟩nres_rel"
  apply (intro frefI nres_relI; clarsimp)
  apply (fact kmp3_correct)
  done

lemmas kmp_impl_correct' = kmp_impl.refine[FCOMP kmp3_correct']

text ‹The following theorem relates the final Imperative HOL algorithm to its specification,
  using, beyond basic HOL concepts
    ▪ Hoare triples for LLVM;
    ▪ The assertion @{const larray_assn} to specify array-lists, which we use to represent the input strings of the algorithm;
    ▪ The @{const sublist_at} function that we defined in section \ref{sec:spec}.
  ›
  
theorem kmp_impl_correct:
  "llvm_htriple 
    (larray_assn id_assn s si ** larray_assn id_assn t ti ** ↑(length s + length t < max_snat 64))
    (kmp_impl si ti)
    (λi. larray_assn id_assn s si ** larray_assn id_assn t ti 
      ** ↑(if i=-1 then ∄i. sublist_at s t i 
          else i≥0 ∧ sublist_at s t (unat i) ∧ (∀ii<unat i. ¬ sublist_at s t ii)))
    "
proof -
  have 1: "snat_option_assn' TYPE(size_t) a c = ↑(if c=-1 then a = None else a = Some (unat c) ∧ snat_invar c)" for a c
    unfolding snat.option_assn_def
    unfolding snat_rel_def pure_def snat.rel_def in_br_conv
    by (auto simp: pred_lift_extract_simps snat_eq_unat)
    
  note R = kmp_impl_correct'[THEN hfrefD, THEN hn_refineD, of "(s,t)" "(si,ti)", simplified]  
  note R = R[unfolded kmp_SPEC_def 1, simplified]       
  note [vcg_rules] = R

  show ?thesis    
   apply vcg' 
   done
   
qed
   
theorem kmp_impl'_correct:
  "llvm_htriple 
    (↿ll_pto si sip ** ↿ll_pto ti tip ** larray_assn id_assn s si ** larray_assn id_assn t ti ** ↑(length s + length t < max_snat 64))
    (kmp_impl' sip tip)
    (λi. ↿ll_pto si sip ** ↿ll_pto ti tip ** larray_assn id_assn s si ** larray_assn id_assn t ti 
      ** ↑(if i=-1 then ∄i. sublist_at s t i 
          else i≥0 ∧ sublist_at s t (unat i) ∧ (∀ii<unat i. ¬ sublist_at s t ii)))
    "
proof -
  interpret llvm_prim_setup .
    
  show ?thesis
    unfolding kmp_impl'_def
    supply [vcg_rules] = kmp_impl_correct
    by (vcg )
qed    

thm hnr_bind[of Γ m⇩i Γ⇩1 R⇩1 m f⇩i Γ⇩2 R⇩2 f R⇩x Γ' free]

thm kmp_impl_def


term ‹foo bar ⌦‹  @{d} } ››



end