Theory Cyc_Check

section ‹Simple Cyclicity Checker›
theory Cyc_Check
imports "../DFS_Framework"
  CAVA_Automata.Digraph_Impl
  "../Misc/Impl_Rev_Array_Stack"
begin
text ‹
  This example presents a simple cyclicity checker: 
    Given a directed graph with start nodes, decide whether it's reachable 
    part is cyclic.

  The example tries to be a tutorial on using the DFS framework, 
  explaining every required step in detail.

  We define two versions of the algorithm, a partial correct one assuming 
  only a finitely branching graph, and a total correct one assuming finitely 
  many reachable nodes.
›

subsection ‹Framework Instantiation›
text ‹ Define a state, based on the DFS-state. 
  In our case, we just add a break-flag.
›
record 'v cycc_state = "'v state" +
  break :: bool

text ‹Some utility lemmas for the simplifier, to handle idiosyncrasies of
  the record package. ›
lemma break_more_cong: "state.more s = state.more s' ⟹ break s = break s'"
  by (cases s, cases s', simp)

lemma [simp]: "s⦇ state.more := ⦇ break = foo ⦈ ⦈ = s ⦇ break := foo ⦈"
  by (cases s) simp

text ‹
  Define the parameterization. We start at a default parameterization, where
  all operations default to skip, and just add the operations we are 
  interested in: Initially, the break flag is false, it is set if we 
  encounter a back-edge, and once set, the algorithm shall terminate immediately. ›
definition cycc_params :: "('v,unit cycc_state_ext) parameterization"
where "cycc_params ≡ dflt_parametrization state.more 
  (RETURN ⦇ break = False ⦈) ⦇
  on_back_edge := λ_ _ _. RETURN ⦇ break = True ⦈,
  is_break := break ⦈"
lemmas cycc_params_simp[simp] = 
  gen_parameterization.simps[mk_record_simp, OF cycc_params_def[simplified]]

interpretation cycc: param_DFS_defs where param=cycc_params for G .

text ‹We now can define our cyclicity checker. 
  The partially correct version asserts a finitely branching graph:›
definition "cyc_checker G ≡ do {
  ASSERT (fb_graph G);
  s ← cycc.it_dfs TYPE('a) G;
  RETURN (break s)
}"

text ‹The total correct variant asserts finitely many reachable nodes.›
definition "cyc_checkerT G ≡ do {
  ASSERT (graph G ∧ finite (graph_defs.reachable G));
  s ← cycc.it_dfsT TYPE('a) G;
  RETURN (break s)
}"


text ‹
  Next, we define a locale for the cyclicity checker's
  precondition and invariant, by specializing the ‹param_DFS› locale.›
locale cycc = param_DFS G cycc_params for G :: "('v, 'more) graph_rec_scheme"
begin
  text ‹We can easily show that our parametrization does not fail, thus we also
    get the DFS-locale, which gives us the correctness theorem for
    the DFS-scheme ›
  sublocale DFS G cycc_params
    apply unfold_locales
    apply (simp_all add: cycc_params_def)
    done

  thm it_dfs_correct  ― ‹Partial correctness›
  thm it_dfsT_correct ― ‹Total correctness if set of reachable states is finite› 
end

lemma cyccI: 
  assumes "fb_graph G" 
  shows "cycc G"
proof -
  interpret fb_graph G by fact
  show ?thesis by unfold_locales
qed

lemma cyccI': 
  assumes "graph G" 
  and FR: "finite (graph_defs.reachable G)"
  shows "cycc G"
proof -
  interpret graph G by fact
  from FR interpret fb_graph G by (rule fb_graphI_fr)
  show ?thesis by unfold_locales
qed


text ‹Next, we specialize the @{term DFS_invar} locale to our parameterization.
  This locale contains all proven invariants. When proving new invariants,
  this locale is available as assumption, thus allowing us to re-use already 
  proven invariants.
›
locale cycc_invar = DFS_invar where param = cycc_params + cycc

text ‹ The lemmas to establish invariants only provide the ‹DFS_invar› locale.
  This lemma is used to convert it into the ‹cycc_invar› locale.
›
lemma cycc_invar_eq[simp]:
  shows "DFS_invar G cycc_params s ⟷ cycc_invar G s" 
proof
  assume "DFS_invar G cycc_params s"
  interpret DFS_invar G cycc_params s by fact
  show "cycc_invar G s" by unfold_locales
next
  assume "cycc_invar G s"
  then interpret cycc_invar G s .
  show "DFS_invar G cycc_params s" by unfold_locales
qed

subsection ‹Correctness Proof›
text ‹ We now enter the ‹cycc_invar› locale, and show correctness of 
  our cyclicity checker.
›
context cycc_invar begin
  text ‹We show that we break if and only if there are back edges. 
    This is straightforward from our parameterization, and we can use the 
    @{thm [source] establish_invarI} rule provided by the DFS framework.

    We use this example to illustrate the general proof scheme:
    ›
  lemma (in cycc) i_brk_eq_back: "is_invar (λs. break s ⟷ back_edges s ≠ {})"
  proof (induct rule: establish_invarI)
  txt ‹The @{thm establish_invarI} rule is used with the induction method, and 
    yields cases›
  print_cases
    txt ‹Our parameterization has only hooked into initialization and back-edges,
      so only these two cases are non-trivial›
    case init thus ?case by (simp add: empty_state_def)
  next
    case (back_edge s s' u v)
    txt ‹For proving invariant preservation, we may assume that the invariant 
      holds on the previous state. Interpreting the invariant locale makes 
      available all invariants ever proved into this locale (i.e., the invariants 
      from all loaded libraries, and the ones you proved yourself.).
      ›
    then interpret cycc_invar G s by simp
    txt ‹However, here we do not need them:›
    from back_edge show ?case by simp
  qed (simp_all cong: break_more_cong)

  text ‹For technical reasons, invariants are proved in the basic locale, 
    and then transferred to the invariant locale:›  
  lemmas brk_eq_back = i_brk_eq_back[THEN make_invar_thm]

  text ‹The above lemma is simple enough to have a short apply-style proof:›
  lemma (in cycc) i_brk_eq_back_short_proof: 
    "is_invar (λs. break s ⟷ back_edges s ≠ {})"
    apply (induct rule: establish_invarI)
    apply (simp_all add: cond_def cong: break_more_cong)
    apply (simp add: empty_state_def)
    done

  text ‹Now, when we know that the break flag indicates back-edges,
    we can easily prove correctness, using a lemma from the invariant 
    library:›
  thm cycle_iff_back_edges
  lemma cycc_correct_aux: 
    assumes NC: "¬cond s"
    shows "break s ⟷ ¬acyclic (E ∩ reachable × UNIV)"
  proof (cases "break s", simp_all)
    assume "break s"
    with brk_eq_back have "back_edges s ≠ {}" by simp
    with cycle_iff_back_edges have "¬acyclic (edges s)" by simp
    with acyclic_subset[OF _ edges_ss_reachable_edges] 
    show "¬acyclic (E ∩ reachable × UNIV)" by blast
  next
    assume A: "¬break s"
    from A brk_eq_back have "back_edges s = {}" by simp
    with cycle_iff_back_edges have "acyclic (edges s)" by simp
    also from A nc_edges_covered[OF NC] have "edges s = E ∩ reachable × UNIV" 
      by simp
    finally show "acyclic (E ∩ reachable × UNIV)" .
  qed

  text ‹Again, we have a short two-line proof:›
  lemma cycc_correct_aux_short_proof:
    assumes NC: "¬cond s"
    shows "break s ⟷ ¬acyclic (E ∩ reachable × UNIV)"
    using nc_edges_covered[OF NC] brk_eq_back cycle_iff_back_edges 
    by (auto dest: acyclic_subset[OF _ edges_ss_reachable_edges])

    
end

text ‹Finally, we define a specification for cyclicity checking,
  and prove that our cyclicity checker satisfies the specification: ›
definition "cyc_checker_spec G ≡ do {
  ASSERT (fb_graph G);
  SPEC (λr. r ⟷ ¬acyclic (g_E G ∩ ((g_E G)⇧* `` g_V0 G) × UNIV))}"

theorem cyc_checker_correct: "cyc_checker G ≤ cyc_checker_spec G"
  unfolding cyc_checker_def cyc_checker_spec_def
proof (refine_vcg le_ASSERTI order_trans[OF DFS.it_dfs_correct], clarsimp_all)
  assume "fb_graph G"
  then interpret fb_graph G .
  interpret cycc by unfold_locales
  show "DFS G cycc_params" by unfold_locales
next
  fix s
  assume "cycc_invar G s"
  then interpret cycc_invar G s .
  assume "¬cycc.cond TYPE('b) G s"
  thus "break s = (¬ acyclic (g_E G ∩ cycc.reachable TYPE('b) G × UNIV))"
    by (rule cycc_correct_aux)
qed

text ‹The same for the total correct variant:›
definition "cyc_checkerT_spec G ≡ do {
  ASSERT (graph G ∧ finite (graph_defs.reachable G));
  SPEC (λr. r ⟷ ¬acyclic (g_E G ∩ ((g_E G)⇧* `` g_V0 G) × UNIV))}"

theorem cyc_checkerT_correct: "cyc_checkerT G ≤ cyc_checkerT_spec G"
  unfolding cyc_checkerT_def cyc_checkerT_spec_def
proof (refine_vcg le_ASSERTI order_trans[OF DFS.it_dfsT_correct], clarsimp_all)
  assume "graph G" then interpret graph G .
  assume "finite (graph_defs.reachable G)" 
  then interpret fb_graph G by (rule fb_graphI_fr)
  interpret cycc by unfold_locales
  show "DFS G cycc_params" by unfold_locales
next
  fix s
  assume "cycc_invar G s"
  then interpret cycc_invar G s .
  assume "¬cycc.cond TYPE('b) G s"
  thus "break s = (¬ acyclic (g_E G ∩ cycc.reachable TYPE('b) G × UNIV))"
    by (rule cycc_correct_aux)
qed


subsection ‹Implementation›
text ‹
  The implementation has two aspects: Structural implementation and data implementation.
  The framework provides recursive and tail-recursive implementations, as well as a variety
  of data structures for the state.

  We will choose the ‹simple_state› implementation, which provides 
  a stack, an on-stack and a visited set, but no timing information.

  Note that it is common for state implementations to omit details from the
  very detailed abstract state. This means, that the algorithm's operations 
  must not access these details (e.g. timing). However, the algorithm's 
  correctness proofs may still use them.
›

text ‹We extend the state template to add a break flag›
record 'v cycc_state_impl = "'v simple_state" +
  break :: bool

text ‹Definition of refinement relation: The break-flag is refined by identity.›
definition "cycc_erel ≡ { 
  (⦇ cycc_state_impl.break = b ⦈, ⦇ cycc_state.break = b⦈) | b. True }"
abbreviation "cycc_rel ≡ ⟨cycc_erel⟩simple_state_rel"

text ‹Implementation of the parameters›
definition cycc_params_impl 
  :: "('v,'v cycc_state_impl,unit cycc_state_impl_ext) gen_parameterization"
where "cycc_params_impl 
  ≡ dflt_parametrization simple_state.more (RETURN ⦇ break = False ⦈) ⦇
  on_back_edge := λu v s. RETURN ⦇ break = True ⦈,
  is_break := break ⦈"
lemmas cycc_params_impl_simp[simp,DFS_code_unfold] = 
  gen_parameterization.simps[mk_record_simp, OF cycc_params_impl_def[simplified]]

text ‹Note: In this simple case, the reformulation of the extension state and 
  parameterization is just redundant, However, in general the refinement will 
  also affect the parameterization.›

lemma break_impl: "(si,s)∈cycc_rel 
  ⟹ cycc_state_impl.break si = cycc_state.break s"
  by (cases si, cases s, simp add: simple_state_rel_def cycc_erel_def)

interpretation cycc_impl: simple_impl_defs G cycc_params_impl cycc_params 
  for G .

text ‹The above interpretation creates an iterative and a recursive implementation ›
term cycc_impl.tailrec_impl term cycc_impl.rec_impl
term cycc_impl.tailrec_implT ― ‹Note, for total correctness we currently only support tail-recursive implementations.›

text ‹We use both to derive a tail-recursive and a recursive cyclicity checker:›
definition [DFS_code_unfold]: "cyc_checker_impl G ≡ do {
  ASSERT (fb_graph G);
  s ← cycc_impl.tailrec_impl TYPE('a) G;
  RETURN (break s)
}"

definition [DFS_code_unfold]: "cyc_checker_rec_impl G ≡ do {
  ASSERT (fb_graph G);
  s ← cycc_impl.rec_impl TYPE('a) G;
  RETURN (break s)
}"

definition [DFS_code_unfold]: "cyc_checker_implT G ≡ do {
  ASSERT (graph G ∧ finite (graph_defs.reachable G));
  s ← cycc_impl.tailrec_implT TYPE('a) G;
  RETURN (break s)
}"



text ‹To show correctness of the implementation, we integrate the
  locale of the simple implementation into our cyclicity checker's locale:›
context cycc begin
  sublocale simple_impl G cycc_params cycc_params_impl cycc_erel 
    apply unfold_locales
    apply (intro fun_relI, clarsimp simp: simple_state_rel_def, parametricity) []
    apply (auto simp: cycc_erel_def break_impl simple_state_rel_def)
    done

  text ‹We get that our implementation refines the abstrct DFS algorithm.›  
  lemmas impl_refine = simple_tailrec_refine simple_rec_refine simple_tailrecT_refine

  text ‹Unfortunately, the combination of locales and abbreviations gets to its 
    limits here, so we state the above lemma a bit more readable:›
  lemma 
    "cycc_impl.tailrec_impl TYPE('more) G ≤ ⇓ cycc_rel it_dfs"
    "cycc_impl.rec_impl TYPE('more) G ≤ ⇓ cycc_rel it_dfs"
    "cycc_impl.tailrec_implT TYPE('more) G ≤ ⇓ cycc_rel it_dfsT"
    using impl_refine .

end

text ‹Finally, we get correctness of our cyclicity checker implementations›
lemma cyc_checker_impl_refine: "cyc_checker_impl G ≤ ⇓Id (cyc_checker G)"
  unfolding cyc_checker_impl_def cyc_checker_def
  apply (refine_vcg cycc.impl_refine)
  apply (simp_all add: break_impl cyccI)
  done
  
lemma cyc_checker_rec_impl_refine: 
  "cyc_checker_rec_impl G ≤ ⇓Id (cyc_checker G)"
  unfolding cyc_checker_rec_impl_def cyc_checker_def
  apply (refine_vcg cycc.impl_refine)
  apply (simp_all add: break_impl cyccI)
  done

lemma cyc_checker_implT_refine: "cyc_checker_implT G ≤ ⇓Id (cyc_checkerT G)"
  unfolding cyc_checker_implT_def cyc_checkerT_def
  apply (refine_vcg cycc.impl_refine)
  apply (simp_all add: break_impl cyccI')
  done


subsection ‹Synthesizing Executable Code›
text ‹
  Our algorithm's implementation is still abstract, as it uses abstract data 
  structures like sets and relations. In a last step, we use the Autoref tool
  to derive an implementation with efficient data structures.
›

text ‹Again, we derive our state implementation from the template provided by 
  the framework. The break-flag is implemented by a Boolean flag. 
  Note that, in general, the user-defined state extensions may be data-refined
  in this step.›
record ('si,'nsi,'psi)cycc_state_impl' = "('si,'nsi)simple_state_impl" +
  break_impl :: bool

text ‹We define the refinement relation for the state extension›
definition [to_relAPP]: "cycc_state_erel erel ≡ {
  (⦇break_impl = bi, … =  mi⦈,⦇break = b, … = m⦈) | bi mi b m.
    (bi,b)∈bool_rel ∧ (mi,m)∈erel}"

text ‹And register it with the Autoref tool:›
consts 
  i_cycc_state_ext :: "interface ⇒ interface"

lemmas [autoref_rel_intf] = REL_INTFI[of cycc_state_erel i_cycc_state_ext]


text ‹We show that the record operations on our extended state are parametric,
  and declare these facts to Autoref: ›
lemma [autoref_rules]:
  fixes ns_rel vis_rel erel
  defines "R ≡ ⟨ns_rel,vis_rel,⟨erel⟩cycc_state_erel⟩ss_impl_rel"
  shows 
    "(cycc_state_impl'_ext, cycc_state_impl_ext) ∈ bool_rel → erel → ⟨erel⟩cycc_state_erel"
    "(break_impl, cycc_state_impl.break) ∈ R → bool_rel"
  unfolding cycc_state_erel_def ss_impl_rel_def R_def
  by auto

text ‹Finally, we can synthesize an implementation for our cyclicity checker,
  using the standard Autoref-approach:›
schematic_goal cyc_checker_impl:
  defines "V ≡ Id :: ('v × 'v::hashable) set"
  assumes [unfolded V_def,autoref_rules]:
    "(Gi, G) ∈ ⟨Rm, V⟩g_impl_rel_ext"
  notes [unfolded V_def,autoref_tyrel] = 
    TYRELI[where R="⟨V⟩dflt_ahs_rel"]
    TYRELI[where R="⟨V ×⇩r ⟨V⟩list_set_rel⟩ras_rel"]
  shows "nres_of (?c::?'c dres) ≤⇓?R (cyc_checker_impl G)"
  unfolding DFS_code_unfold
  using [[autoref_trace_failed_id, goals_limit=1]]
  apply (autoref_monadic (trace))
  done
concrete_definition cyc_checker_code uses cyc_checker_impl
export_code cyc_checker_code checking SML

text ‹Combining the refinement steps yields a correctness 
  theorem for the cyclicity checker implementation:›
theorem cyc_checker_code_correct:
  assumes 1: "fb_graph G"
  assumes 2: "(Gi, G) ∈ ⟨Rm, Id⟩g_impl_rel_ext"
  assumes 4: "cyc_checker_code Gi = dRETURN x"
  shows "x ⟷ (¬acyclic (g_E G ∩ ((g_E G)⇧* `` g_V0 G) × UNIV))"
proof -
  note cyc_checker_code.refine[OF 2]
  also note cyc_checker_impl_refine
  also note cyc_checker_correct
  finally show ?thesis using 1 4
  unfolding cyc_checker_spec_def by auto
qed

text ‹We can repeat the same boilerplate for the recursive version of the algorithm:›
schematic_goal cyc_checker_rec_impl:
  defines "V ≡ Id :: ('v × 'v::hashable) set"
  assumes [unfolded V_def,autoref_rules]:
    "(Gi, G) ∈ ⟨Rm, V⟩g_impl_rel_ext"
  notes [unfolded V_def,autoref_tyrel] = 
    TYRELI[where R="⟨V⟩dflt_ahs_rel"]
    TYRELI[where R="⟨V ×⇩r ⟨V⟩list_set_rel⟩ras_rel"]
  shows "nres_of (?c::?'c dres) ≤⇓?R (cyc_checker_rec_impl G)"
  unfolding DFS_code_unfold
  using [[autoref_trace_failed_id, goals_limit=1]]
  apply (autoref_monadic (trace))
  done
concrete_definition cyc_checker_rec_code uses cyc_checker_rec_impl
prepare_code_thms cyc_checker_rec_code_def
export_code cyc_checker_rec_code checking SML

lemma cyc_checker_rec_code_correct:
  assumes 1: "fb_graph G"
  assumes 2: "(Gi, G) ∈ ⟨Rm, Id⟩g_impl_rel_ext"
  assumes 4: "cyc_checker_rec_code Gi = dRETURN x"
  shows "x ⟷ (¬acyclic (g_E G ∩ ((g_E G)⇧* `` g_V0 G) × UNIV))"
proof -
  note cyc_checker_rec_code.refine[OF 2]
  also note cyc_checker_rec_impl_refine
  also note cyc_checker_correct
  finally show ?thesis using 1 4 
  unfolding cyc_checker_spec_def by auto
qed

text ‹And, again, for the total correct version. 
  Note that we generate a plain implementation, not inside a monad:›
schematic_goal cyc_checker_implT:
  defines "V ≡ Id :: ('v × 'v::hashable) set"
  assumes [unfolded V_def,autoref_rules]:
    "(Gi, G) ∈ ⟨Rm, V⟩g_impl_rel_ext"
  notes [unfolded V_def,autoref_tyrel] = 
    TYRELI[where R="⟨V⟩dflt_ahs_rel"]
    TYRELI[where R="⟨V ×⇩r ⟨V⟩list_set_rel⟩ras_rel"]
  shows "RETURN (?c::?'c) ≤⇓?R (cyc_checker_implT G)"
  unfolding DFS_code_unfold
  using [[autoref_trace_failed_id, goals_limit=1]]
  apply (autoref_monadic (trace,plain))
  done
concrete_definition cyc_checker_codeT uses cyc_checker_implT
export_code cyc_checker_codeT checking SML

theorem cyc_checker_codeT_correct:
  assumes 1: "graph G" "finite (graph_defs.reachable G)"
  assumes 2: "(Gi, G) ∈ ⟨Rm, Id⟩g_impl_rel_ext"
  shows "cyc_checker_codeT Gi ⟷ (¬acyclic (g_E G ∩ ((g_E G)⇧* `` g_V0 G) × UNIV))"
proof -
  note cyc_checker_codeT.refine[OF 2]
  also note cyc_checker_implT_refine
  also note cyc_checkerT_correct
  finally show ?thesis using 1
  unfolding cyc_checkerT_spec_def by auto
qed
  
end