Theory BFS

(*<*)
theory BFS
imports
  "Assume_Guarantee"
begin

(*>*)
section‹ Example: data refinement (search)\label{sec:ex-data_refinement} ›

text‹

We show a very simple example of data refinement: implementing sets with functional queues
for breadth-first search (BFS). The objective here is to transfer a simple correctness property
proven on the abstract level to the concrete level.

Observations:
 ▪ there is no concurrency in the BFS: this is just about data refinement
  ▪ however arbitrary interference is allowed
 ▪ the abstract level does not require the implementation of the pending set to make progress
 ▪ the concrete level does not require a representation invariant
 ▪ depth optimality is not shown

References:
 ▪ queue ADT: 🗏‹$ISABELLE_HOME/src/Doc/Codegen/Introduction.thy›
 ▪ BFS verification:
  ▪ J. C. Filliâtre 🌐‹http://toccata.lri.fr/gallery/vstte12_bfs.en.html›
  ▪ 🗏‹$AFP/Refine_Monadic/examples/Breadth_First_Search.thy›
  ▪ our model is quite different

›

setup ‹Sign.mandatory_path "pending"›

record ('a, 's) interface =
  init :: "('s, unit) prog"
  enq :: "'a ⇒ ('s, unit) prog"
  deq :: "('s, 'a option) prog"

type_synonym 'a abstract = "'a set"

definition abstract :: "('a, 'a pending.abstract × 's) pending.interface" where
  "abstract =
    ⦇ pending.interface.init = prog.write (map_prod ⟨{}⟩ id)
    , pending.interface.enq = λx. prog.write (map_prod (insert x) id)
    , pending.interface.deq = prog.action ({(None, s, s) |s. fst s = {}}
                                         ∪ {(Some x, (insert x X, s), (X, s)) |X s x. True})
    ⦈"

type_synonym 'a concrete = "'a list × 'a list" ―‹ a queue ›

fun cdeq_update :: "'a pending.concrete × 's ⇒ 'a option × 'a pending.concrete × 's" where
  "cdeq_update (([], []), s) = (None, (([], []), s))"
| "cdeq_update ((xs, []), s) = cdeq_update (([], rev xs), s)"
| "cdeq_update ((xs, y # ys), s) = (Some y, ((xs, ys), s))"

definition concrete :: "('a, 'a pending.concrete × 's) pending.interface" where
  "concrete =
    ⦇ pending.interface.init = prog.write (map_prod ⟨([], [])⟩ id)
    , pending.interface.enq = λx. prog.write (map_prod (map_prod ((#) x) id) id)
    , pending.interface.deq = prog.det_action pending.cdeq_update
    ⦈"

abbreviation absfn' :: "'a pending.concrete ⇒ 'a list" where ―‹ queue as a list ›
  "absfn' s ≡ snd s @ rev (fst s)"

definition absfn :: "'a pending.concrete ⇒ 'a pending.abstract" where
  "absfn s = set (pending.absfn' s)"

setup ‹Sign.mandatory_path "ag"›

lemma init:
  fixes Q :: "unit ⇒ 'a pending.abstract × 's ⇒ bool"
  fixes A :: "'s rel"
  assumes "stable (Id ×⇩R A) (Q ())"
  shows "prog.p2s (pending.init pending.abstract) ≤ ⦃λs. Q () ({}, snd s)⦄, Id ×⇩R A ⊢ UNIV ×⇩R Id, ⦃Q⦄"
using assms by (auto intro: ag.prog.action simp: pending.abstract_def stable_def monotone_def)

lemma enq:
  fixes x :: 'a
  fixes Q :: "unit ⇒ 'a pending.abstract × 's ⇒ bool"
  fixes A :: "'s rel"
  assumes "stable (Id ×⇩R A) (Q ())"
  shows "prog.p2s (pending.enq pending.abstract x) ≤ ⦃λs. Q () (insert x (fst s), snd s)⦄, Id ×⇩R A ⊢ UNIV ×⇩R Id, ⦃Q⦄"
using assms by (auto intro: ag.prog.action simp: pending.abstract_def stable_def monotone_def)

lemma deq:
  fixes Q :: "'a option ⇒ 'a pending.abstract × 's ⇒ bool"
  fixes A :: "'s rel"
  assumes "⋀v. stable (Id ×⇩R A) (Q v)"
  shows "prog.p2s (pending.deq pending.abstract) ≤ ⦃λs. if fst s = {} then Q None s else (∀x X. fst s = insert x X ⟶ Q (Some x) (X, snd s))⦄, Id ×⇩R A ⊢ UNIV ×⇩R Id, ⦃Q⦄"
unfolding pending.abstract_def pending.interface.simps
by (rule ag.prog.action)
   (use assms in ‹auto simp: stable_def monotone_def le_bool_def split: if_split_asm›)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "set"›

record ('a, 's) interface =
  init :: "('s, unit) prog"
  ins :: "'a ⇒ ('s, unit) prog"
  mem :: "'a ⇒ ('s, bool) prog"

type_synonym 'a abstract = "'a list" ―‹ model finite sets ›

definition abstract :: "('a, 's × 'a set.abstract × 't) set.interface" where
  "abstract =
    ⦇ set.interface.init = prog.write (map_prod id (map_prod ⟨[]⟩ id))
    , set.interface.ins = λx. prog.write (map_prod id (map_prod ((#) x) id))
    , set.interface.mem = λx. prog.read (λs. x ∈ set (fst (snd s)))
    ⦈"

setup ‹Sign.mandatory_path "ag"›

lemma init:
  fixes Q :: "unit ⇒ 's × 'a set.abstract × 't ⇒ bool"
  fixes A :: "'s rel"
  assumes "stable (A ×⇩R Id ×⇩R B) (Q ())"
  shows "prog.p2s (set.init set.abstract) ≤ ⦃λs. Q () (fst s, [], snd (snd s))⦄, A ×⇩R Id ×⇩R B ⊢ Id ×⇩R UNIV ×⇩R Id, ⦃Q⦄"
using assms by (auto intro: ag.prog.action simp: set.abstract_def stable_def monotone_def)

lemma ins:
  fixes x :: 'a
  fixes Q :: "unit ⇒ 's × 'a set.abstract × 't ⇒ bool"
  fixes A :: "'s rel"
  assumes "stable (A ×⇩R Id ×⇩R B) (Q ())"
  shows "prog.p2s (set.ins set.abstract x) ≤ ⦃λs. Q () (fst s, x # fst (snd s), snd (snd s))⦄, A ×⇩R Id ×⇩R B ⊢ Id ×⇩R UNIV ×⇩R Id, ⦃Q⦄"
using assms by (auto intro: ag.prog.action simp: set.abstract_def stable_def monotone_def)

lemma mem:
  fixes Q :: "bool ⇒ 's × 'a set.abstract × 't ⇒ bool"
  assumes "⋀v. stable (A ×⇩R Id ×⇩R B) (Q v)"
  shows "prog.p2s (set.mem set.abstract x) ≤ ⦃λs. Q (x ∈ set (fst (snd s))) s⦄, A ×⇩R Id ×⇩R B ⊢ Id ×⇩R UNIV ×⇩R Id, ⦃Q⦄"
using assms by (auto intro: ag.prog.action simp: set.abstract_def stable_def monotone_def)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

context
  fixes pending :: "('a, 'p × 'a set.abstract × 's) pending.interface"
  fixes f :: "'a ⇒ 'a list"
begin

definition loop :: "'a pred ⇒ ('p × 'a set.abstract × 's, 'a option) prog" where
  "loop p =
    prog.while (λ_.
      do { aopt ← pending.deq pending
         ; case aopt of
             None ⇒ prog.return (Inr None)
           | Some x ⇒
               if p x
               then prog.return (Inr (Some x))
               else do { prog.app (λy. do { b ← set.mem set.abstract y;
                                            prog.unlessM b (do { set.ins set.abstract y
                                                               ; pending.enq pending y }) })
                                  (f x)
                       ; prog.return (Inl ())
                       }
       }) ()"

definition main :: "'a pred ⇒ 'a ⇒ ('p × 'a set.abstract × 's, 'a option) prog" where
  "main p x =
    do {
      set.init set.abstract
    ; pending.init pending
    ; set.ins set.abstract x
    ; pending.enq pending x
    ; loop p
    }"

definition search :: "'a pred ⇒ 'a ⇒ ('s, 'a option) prog" where
  "search p x = prog.local (prog.local (main p x))"

end

abbreviation (input) "aloop ≡ loop pending.abstract"
abbreviation (input) "amain ≡ main pending.abstract"
abbreviation (input) "asearch ≡ search pending.abstract"
abbreviation (input) "bfs ≡ search pending.concrete"

lemma
  shows pending_g: "UNIV ×⇩R Id ⊆ UNIV ×⇩R UNIV ×⇩R Id"
    and set_g: "Id ×⇩R UNIV ×⇩R Id ⊆ UNIV ×⇩R UNIV ×⇩R Id"
by fastforce+

context
  fixes f :: "'a ⇒ 'a list"
  fixes P :: "'a pred"
  fixes x⇩0 :: "'a"
begin

abbreviation (input) step :: "'a rel" where
  "step ≡ {(x, y). y ∈ set (f x)}"

abbreviation (input) path :: "'a rel" where
  "path ≡ step⇧*"

definition aloop_invP :: "'a pending.abstract ⇒ 'a set.abstract ⇒ bool" where
  "aloop_invP q v ⟷
        q ⊆ set v
      ∧ set v ⊆ path `` {x⇩0}
      ∧ set v ∩ Collect P ⊆ q
      ∧ x⇩0 ∈ set v"

definition vclosureP :: "'a ⇒ 'a pending.abstract ⇒ 'a set.abstract ⇒ bool" where
  "vclosureP x q v ⟷ (x ∈ set v - q ⟶ step `` {x} ⊆ set v)"

definition search_postP :: "'a option ⇒ bool" where
  "search_postP rv = (case rv of
      None ⇒ finite (path `` {x⇩0}) ∧ (path `` {x⇩0} ∩ Collect P = {})
    | Some y ⇒ (x⇩0, y) ∈ path ∧ P y)"

abbreviation "aloop_inv s ≡ aloop_invP (fst s) (fst (snd s))"
abbreviation "vclosure x s ≡ vclosureP x (fst s) (fst (snd s))"
abbreviation "search_post rv ≡ ⟨search_postP rv⟩"

lemma vclosureP_closed:
  assumes "set v ⊆ path `` {x⇩0}"
  assumes "∀y. vclosureP y {} v"
  assumes "x⇩0 ∈ set v"
  shows "path `` {x⇩0} = set v"
proof -
  have "y ∈ set v" if "(x⇩0, y) ∈ path" for y
    using that assms(2,3) by induct (auto simp: vclosureP_def)
  with assms(1) show ?thesis
    by fast
qed

lemma vclosureP_app:
  assumes "∀y. x ≠ y ⟶ local.vclosureP y q v"
  assumes "set (f x) ⊆ set v"
  shows "vclosureP y q v"
using assms by (fastforce simp: vclosureP_def)

lemma vclosureP_init:
  shows "vclosureP x {x⇩0} [x⇩0]"
by (simp add: vclosureP_def)

lemma vclosureP_step:
  assumes "∀z. x ≠ z ⟶ vclosureP z q v"
  assumes "x ≠ z"
  shows "vclosureP z (insert y q) (y # v)"
using assms by (fastforce simp: vclosureP_def)

lemma vclosureP_dequeue:
  assumes "∀z. vclosureP z (insert x q) v"
  assumes "x ≠ z"
  shows "vclosureP z q v"
using assms by (fastforce simp: vclosureP_def)

lemma aloop_invPD:
  assumes "aloop_invP q v"
  assumes "x ∈ q"
  shows "(x⇩0, x) ∈ path"
using assms by (auto simp: aloop_invP_def)

lemma aloop_invP_init:
  shows "aloop_invP {x⇩0} [x⇩0]"
by (simp add: aloop_invP_def)

lemma aloop_invP_step:
  assumes "aloop_invP q v"
  assumes "(x⇩0, x) ∈ path"
  assumes "y ∈ set (f x) - set v"
  shows "aloop_invP (insert y q) (y # v)"
using assms by (auto simp: aloop_invP_def elim: rtrancl_into_rtrancl)

lemma aloop_invP_dequeue:
  assumes "aloop_invP (insert x q) v"
  assumes "¬ P x"
  shows "aloop_invP q v"
using assms by (auto simp: aloop_invP_def)

lemma search_postcond_None:
  assumes "aloop_invP {} v"
  assumes "∀y. vclosureP y {} v"
  shows "search_postP None"
using assms by (auto simp: search_postP_def aloop_invP_def dest: vclosureP_closed)

lemma search_postcond_Some:
  assumes "aloop_invP q v"
  assumes "x ∈ q"
  assumes "P x"
  shows "search_postP (Some x)"
using assms by (auto simp: search_postP_def aloop_invP_def)

lemmas stable_simps =
  prod.sel
  split_def
  sum.simps

lemma ag_aloop:
  shows "prog.p2s (aloop f P) ≤ ⦃aloop_inv ❙∧ (❙∀x. vclosure x)⦄, Id ×⇩R Id ×⇩R UNIV ⊢ UNIV ×⇩R UNIV ×⇩R Id, ⦃search_post⦄"
unfolding loop_def
apply (rule ag.prog.while[OF _ _ stable.Id_fst_fst_snd])
 apply (rule ag.prog.bind)
  apply (rule ag.prog.case_option)
   apply (rule ag.prog.return)
   apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
  apply (rule ag.prog.if)
   apply (rule ag.prog.return)
   apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
  apply (rule ag.prog.bind)
   apply (rule ag.prog.return)
   apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
  apply (rename_tac x)
  apply (rule_tac Q="λ_. aloop_inv ❙∧ (❙∀y. ⟨x ≠ y⟩ ❙⟶ vclosure y) ❙∧ (λs. set (f x) ⊆ set (fst (snd s)) ∧ (x⇩0, x) ∈ path)" in ag.post_imp)
   apply (force elim: vclosureP_app)
  apply (rule ag.prog.app)
   apply (rule ag.prog.bind)
    apply (rule ag.prog.if)
     apply (rule ag.prog.return)
     apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
    apply (rule ag.prog.bind)
     apply (rule ag.pre_g[OF pending.ag.enq pending_g])
     apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
    apply (rule ag.pre_g[OF set.ag.ins set_g])
    apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
   apply (rule ag.pre_pre[OF ag.pre_g[OF set.ag.mem set_g]])
    apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
   apply (force simp: aloop_invP_step vclosureP_step)
  apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
 apply (rule ag.pre_g[OF pending.ag.deq pending_g])
 apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
apply (auto elim: search_postcond_Some search_postcond_None aloop_invP_dequeue
                  aloop_invPD vclosureP_dequeue)
done

lemma ag_amain:
  shows "prog.p2s (amain f P x⇩0) ≤ ⦃⟨True⟩⦄, Id ×⇩R Id ×⇩R UNIV ⊢ UNIV ×⇩R UNIV ×⇩R Id, ⦃search_post⦄"
unfolding main_def
apply (rule ag.pre_pre)
 apply (rule ag.prog.bind)+
     apply (rule ag_aloop)
    apply (rule ag.post_imp[where Q="⟨λ(q, v, _). q = {x⇩0} ∧ v = [x⇩0]⟩"])
     apply (clarsimp simp: aloop_invP_init vclosureP_init; fail)
    apply (rule ag.pre_g[OF pending.ag.enq pending_g])
    apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
   apply (rule ag.pre_g[OF set.ag.ins set_g])
   apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
  apply (rule ag.pre_g[OF pending.ag.init pending_g])
  apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
 apply (rule ag.pre_g[OF set.ag.init set_g])
 apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
apply simp
done

lemma ag_asearch:
  shows "prog.p2s (asearch f P x⇩0 :: ('s, 'a option) prog) ≤ ⦃⟨True⟩⦄, UNIV ⊢ Id, ⦃search_post⦄"
unfolding search_def by (rule ag.prog.local ag_amain)+


paragraph‹ Refinement ›

abbreviation "A ≡ ag.assm (Id ×⇩R Id ×⇩R UNIV)"
abbreviation "absfn c ≡ prog.sinvmap (map_prod pending.absfn id) c"
abbreviation "p2s_absfn c ≡ prog.p2s (absfn c)"

―‹ visited set: reflexive ›
lemma ref_set_init:
  shows "prog.p2s (set.init set.abstract) ≤ ⦃λs. True⦄, A ⊩ p2s_absfn (set.init set.abstract), ⦃λv s. True⦄"
by (auto simp: set.abstract_def intro: rair.prog.action stable.intro)

lemma ref_set_ins:
  shows "prog.p2s (set.ins set.abstract x) ≤ ⦃λs. True⦄, A ⊩ p2s_absfn (set.ins set.abstract x), ⦃λv s. True⦄"
by (auto simp: set.abstract_def intro: rair.prog.action stable.intro)

lemma ref_set_mem:
  shows "prog.p2s (set.mem set.abstract x) ≤ ⦃λs. True⦄, A ⊩ p2s_absfn (set.mem set.abstract x), ⦃λv s. True⦄"
by (auto simp: set.abstract_def intro: rair.prog.action stable.intro)

―‹ queue ›
lemma ref_queue_init:
  shows "prog.p2s (pending.init pending.concrete) ≤ ⦃λs. True⦄, A ⊩ p2s_absfn (pending.init pending.abstract), ⦃λv s. True⦄"
by (auto simp: pending.abstract_def pending.concrete_def pending.absfn_def intro: rair.prog.action stable.intro)

lemma ref_queue_enq:
  shows "prog.p2s (pending.enq pending.concrete x) ≤ ⦃λs. True⦄, A ⊩ p2s_absfn (pending.enq pending.abstract x), ⦃λv s. True⦄"
by (auto simp: pending.abstract_def pending.concrete_def pending.absfn_def intro: rair.prog.action stable.intro)

lemma ref_queue_deq:
  shows "prog.p2s (pending.deq pending.concrete) ≤ ⦃λs. True⦄, A ⊩ p2s_absfn (pending.deq pending.abstract), ⦃λv s. True⦄"
by (auto simp: pending.abstract_def pending.concrete_def pending.absfn_def
        intro: rair.prog.action stable.intro elim!: pending.cdeq_update.elims[OF sym])

―‹ program ›
lemma ref_bfs_loop:
  shows "prog.p2s (loop pending.concrete f P) ≤ ⦃λs. True⦄, A ⊩ p2s_absfn (loop pending.abstract f P), ⦃λv s. True⦄"
apply (simp add: loop_def)
apply (rule rair.prog.while)
  apply (rule rair.prog.rev_bind)
   apply (rule ref_queue_deq)
  apply (rule refinement.pre_pre[OF rair.prog.case_option])
    apply (rule rair.prog.return)
    apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
   apply (rule rair.prog.if)
    apply (rule rair.prog.return)
    apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
   apply (rule rair.prog.rev_bind)
    apply (rule rair.prog.app)
     apply (rule rair.prog.rev_bind)
      apply (rule ref_set_mem)
     apply (rule refinement.pre_pre[OF rair.prog.if])
       apply (rule rair.prog.return)
       apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
      apply (rule rair.prog.rev_bind)
       apply (rule ref_set_ins)
      apply (rule ref_queue_enq)
     apply (simp; fail)
    apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
   apply (rule refinement.pre_pre[OF rair.prog.return])
    apply ((simp only: stable_simps)?; (rule stable.intro)+; fail)
   apply (auto intro: stable.intro split: option.split)
done

lemma ref_bfs_main:
  shows "prog.p2s (main pending.concrete f P x) ≤ ⦃⟨True⟩⦄, A ⊩ p2s_absfn (amain f P x), ⦃λv s. True⦄"
apply (simp add: main_def)
apply (rule rair.prog.rev_bind)
 apply (rule ref_set_init)
apply (rule rair.prog.rev_bind)
 apply (rule ref_queue_init)
apply (rule rair.prog.rev_bind)
 apply (rule ref_set_ins)
apply (rule rair.prog.rev_bind)
 apply (rule ref_queue_enq)
apply (rule ref_bfs_loop)
done

theorem ref_bfs:
  shows "bfs f P x ≤ asearch f P x"
unfolding search_def
apply (intro refinement.prog.leI refinement.prog.data[where sf=id])
apply (simp add: spec.invmap.id spec.localizeA.top)
apply (rule refinement.prog.data[where sf=pending.absfn])
apply (simp flip: prog.p2s.invmap)
apply (rule refinement.pre_a[OF ref_bfs_main])
apply (auto simp: spec.localizeA_def spec.invmap.rel
       simp flip: spec.rel.inf
           intro: spec.rel.mono)
done

theorem bfs_post_le:
  shows "prog.p2s (bfs f P x⇩0) ≤ spec.post (search_post)"
apply (strengthen ord_to_strengthen[OF ref_bfs])
apply (strengthen ord_to_strengthen(1)[OF ag_asearch])
apply (simp add: ag_def spec.rel.UNIV flip: Sigma_Un_distrib1)
done

end
(*<*)

end
(*>*)