Theory CopyBuffer

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSP - A Shallow Embedding of CSP in  Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff, Lina Ye.
 *                   (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file       : Example of Copy Buffer
 *
 * Copyright (c) 2009 Université Paris-Sud, France
 * Copyright (c) 2025 Université Paris-Saclay, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************›
(*>*)

chapter‹ Annex: Running Example with Buffer over infinite Alphabet›

(*<*)
theory      CopyBuffer 
  imports   "HOL-CSP"
begin 
(*>*)

section‹ Defining the Copy-Buffer Example ›


datatype 'a channel = left 'a | right 'a | mid 'a | ack

definition SYN  :: "'a channel set"
  where     "SYN  ≡ range mid ∪ {ack}"

definition COPY :: "'a channel process"
  where     "COPY ≡ μ COPY. left❙?x → right❙!x → COPY"

definition SEND :: "'a channel process"
  where     "SEND ≡ μ SEND. left❙?x → mid❙!x → ack → SEND"

definition REC  :: "'a channel process"
  where     "REC  ≡ μ REC. mid❙?x → right❙!x → ack → REC"


definition SYSTEM :: "'a channel process"
  where     ‹SYSTEM ≡ SEND ⟦ SYN ⟧ REC \ SYN›

thm SYSTEM_def

section‹ The Standard Proof ›

subsection‹ Channels and Synchronization Sets›

text‹ First part: abstract properties for these events to SYN.
       This kind of stuff could be automated easily by some
       extra-syntax for channels and SYN-sets. ›

lemma simplification_lemmas [simp] :
  ‹range left ∩ SYN = {}›
  ‹range right ∩ SYN = {}›
  ‹ack ∈ SYN›
  ‹range mid ⊆ SYN›
  ‹mid x ∈ SYN›
  ‹right x ∉ SYN›
  ‹left x ∉ SYN›
  ‹inj mid›
  by (auto simp: SYN_def inj_on_def)

lemma "finite (SYN:: 'a channel set) ⟹ finite {(t::'a). True}"
  by (metis (no_types) SYN_def UNIV_def channel.inject(3) finite_Un finite_imageD inj_on_def)

subsection‹ Definitions by Recursors ›

text‹ Second part: Derive recursive process equations, which
       are easier to handle in proofs. This part IS actually
       automated if we could reuse the fixrec-syntax below. ›

lemma COPY_rec:
  "COPY = left❙?x → right❙!x → COPY"
  by(simp add: COPY_def,rule trans, rule fix_eq, simp)

lemma SEND_rec: 
  "SEND = left❙?x → mid❙!x → ack → SEND"
  by(simp add: SEND_def,rule trans, rule fix_eq, simp)

lemma REC_rec:
  "REC = mid❙?x → right❙!x → ack → REC"
  by(simp add: REC_def,rule trans, rule fix_eq, simp)


subsection‹ Various Samples of Refinement Proofs ›


(* ************************************************************************* *)
(* 	                                                    								     *)
(* Setup for rewriting							                                         *)
(* 									                                                        *)
(* ************************************************************************* *)

lemmas Sync_rules = read_Sync_read_subset_forced_read_same_chan
  read_Sync_read_left read_Sync_read_right
  write_Sync_read_left write_Sync_read_right
  read_Sync_write_left read_Sync_write_right
  write_Sync_write_subset
  write_Sync_read_subset read_Sync_write_subset

write0_Sync_write_right write0_Sync_write0

lemmas Hiding_rules = Hiding_read_disjoint Hiding_write_subset Hiding_write_disjoint
  Hiding_write0_non_disjoint Hiding_write0_disjoint

lemmas mono_rules = mono_read_FD mono_write_FD mono_write0_FD



text‹An example for a very explicit structured proof. 
     Slow-motion for presentations. Note that the proof makes
     no assumption over the structure of the content of the channel;
     it is truly polymorphic wrt. the channel type \<^typ>‹'α›.›

lemma impl_refines_spec' : "(COPY :: 'a channel process) ⊑⇩F⇩D SYSTEM"
  unfolding  SYSTEM_def COPY_def
proof (rule fix_ind)
  show "adm (λa. a ⊑⇩F⇩D (SEND ⟦SYN⟧ REC \\ SYN))" 
    by (simp add: cont2mono)
next 
  show "⊥ ⊑⇩F⇩D (SEND ⟦SYN⟧ REC \\ SYN)"
    by simp
next
  fix x :: "'a channel process"
  assume hyp : "x ⊑⇩F⇩D (SEND ⟦SYN⟧ REC \\ SYN)"
  show "(Λ x. left❙?xa → right❙!xa → x)⋅x ⊑⇩F⇩D (SEND ⟦SYN⟧ REC \\ SYN)"
    apply (subst SEND_rec, subst REC_rec)
    apply (simp add: cont_fun)
  proof - 
    have      "   left❙?x → mid❙!x → ack → SEND ⟦SYN⟧ mid❙?x → right❙!x → ack → REC \\ SYN 
                   =  left❙?x → (mid❙!x → ack → SEND ⟦SYN⟧ mid❙?x → right❙!x → ack → REC \\ SYN) " 
      (is "?lhs = _")
      by (simp add: Sync_rules Hiding_rules)
    also have " ... =  left❙?x → (mid❙!x → (ack → SEND ⟦SYN⟧ right❙!x → ack → REC) \\ SYN)"
      by (simp add: Sync_rules Hiding_rules)
    also have " ... = left❙?x → (ack → SEND ⟦SYN⟧ right❙!x → ack → REC) \\ SYN"
      by (simp add: Sync_rules Hiding_rules)
    also have " ... = left❙?x → right❙!x → (ack → SEND ⟦SYN⟧  ack → REC) \\ SYN"
      by (simp add: Sync_rules Hiding_rules )
    also  have " ...  = left❙?x → right❙!x → (SEND ⟦SYN⟧ REC \\ SYN)"  (is "_ = ?rhs")
      by (simp add: Sync_rules Hiding_rules) 
    finally have * :  "?lhs = ?rhs" .
    show "    left❙?xa → right❙!xa → x  ⊑⇩F⇩D ?lhs"
      by (simp only : "*" mono_read_FD mono_write_FD hyp)
  qed
qed



text‹An example for a highly automated proof.›
text‹Not too bad in automation considering what is inferred, but wouldn't scale for large examples. ›


lemma impl_refines_spec : "COPY ⊑⇩F⇩D SYSTEM"
  unfolding SYSTEM_def COPY_def
  apply(rule fix_ind, auto intro: le_FD_adm simp:  cont_fun monofunI)
  apply(subst SEND_rec, subst REC_rec)
  apply (simp add: Sync_rules Hiding_rules mono_read_FD mono_write_FD) (*  write0_Sync_write0 write_is_write0 *)
  oops


lemma spec_refines_impl : 
  assumes fin: "finite (SYN:: 'a channel set)"
  shows        "SYSTEM ⊑⇩F⇩D (COPY :: 'a channel process)"
  apply(simp add: SYSTEM_def SEND_def)
  apply(rule fix_ind, simp_all)
   apply (intro le_FD_adm)
    apply (simp add: fin)
   apply (simp add: cont2mono)
  apply (simp add: Sync_commute)
  apply (subst COPY_rec, subst REC_rec)
  apply (simp add: read_def write_def comp_def)
  apply (subst Mprefix_Sync_Mprefix_right) apply auto[2]
  apply (simp add: Sync_rules Hiding_rules comp_def)
  apply (subst Hiding_Mprefix_disjoint) apply auto[1]
  apply (intro mono_Mprefix_FD ballI)
  apply (subst Mprefix_Sync_Mprefix_subset) apply auto[2]
  apply (subst Hiding_Mprefix_non_disjoint) apply auto[1]
  apply simp
  apply (fold write0_def)
  by (simp add: Hiding_write0_disjoint Hiding_write0_non_disjoint Sync_commute mono_write0_FD write0_Sync_write0)



text‹ Note that this was actually proven for the
       Process ordering, not the refinement ordering. 
       But the former implies the latter.
       And due to anti-symmetry, equality follows
       for the case of finite alphabets \ldots ›

lemma spec_equal_impl : 
  assumes fin:  "finite (SYN::('a channel)set)"
  shows         "SYSTEM = (COPY::'a channel process)"
  by (simp add: FD_antisym fin impl_refines_spec' spec_refines_impl)

subsection‹Deadlock Freeness Proof ›

text‹HOL-CSP can be used to prove deadlock-freeness of processes with infinite alphabet. In the
case of the @{term COPY} - process, this can be formulated as the following refinement problem:›

lemma DF_COPY : "(DF (range left ∪ range right)) ⊑⇩F⇩D COPY"
  apply(simp add:DF_def,rule fix_ind2)
proof -
  show "adm (λa. a ⊑⇩F⇩D COPY)"   by(rule le_FD_adm, simp_all add: monofunI)
next
  show "⊥ ⊑⇩F⇩D COPY" by fastforce
next
  have 1: "(⊓xa∈ (range left ∪ range right) → ⊥) ⊑⇩F⇩D (⊓xa∈ range left →  ⊥)"
    by (simp add: Mndetprefix_FD_subset)
  have 2: "(⊓xa∈ range left →  ⊥)  ⊑⇩F⇩D (left❙?x →  ⊥)" 
    unfolding read_def
    by (meson Mndetprefix_FD_Mprefix BOT_leFD mono_Mndetprefix_FD trans_FD)
  show "(Λ x. ⊓xa∈(range left ∪ range right) →  x)⋅⊥ ⊑⇩F⇩D COPY" 
    by simp (metis (mono_tags, lifting) 1 2 COPY_rec mono_read_FD BOT_leFD trans_FD)
next
  fix P::"'a channel process"
  assume  *: "P ⊑⇩F⇩D COPY" and ** : "(Λ x. ⊓xa∈(range left ∪ range right) →  x)⋅P ⊑⇩F⇩D COPY"
  have 1:"⊓xa∈ (range left ∪ range right) →  P ⊑⇩F⇩D ⊓xa∈ range right →  P"
    by (simp add: Mndetprefix_FD_subset)
  have 2:"⊓xa∈ range right →  P ⊑⇩F⇩D right❙!x →  P" for x
    apply (unfold write_def, rule trans_FD[OF Mndetprefix_FD_subset[of ‹{right x}› ‹range right›]])
    by (simp_all add: Mndetprefix_FD_Mprefix Mprefix_singl)
  from 1 2 have ab:"⊓xa∈ (range left ∪ range right) →  P ⊑⇩F⇩D right❙!x →  P" for x
    using trans_FD by blast
  hence 3:"left❙?x → ⊓xa∈ (range left ∪ range right) →  P ⊑⇩F⇩D left❙?x → right❙!x →  P"
    by (simp add: mono_read_FD)
  have 4:"⋀X. ⊓xa∈ (range left ∪ range right) → X ⊑⇩F⇩D ⊓xa∈ range left → X"
    by (rule Mndetprefix_FD_subset, simp, blast) 
  have 5:"⋀X. ⊓xa∈ range left → X ⊑⇩F⇩D left❙?x → X"
    by (unfold read_def, subst K_record_comp, fact Mndetprefix_FD_Mprefix)
  from 3 4[of "⊓xa∈ (range left ∪ range right) →  P"] 
    5  [of "⊓xa∈ (range left ∪ range right) →  P"] 
  have 6:"⊓xa∈ (range left ∪ range right) → 
                  ⊓xa∈ (range left ∪ range right) →  P ⊑⇩F⇩D left❙?x → right❙!x →  P"
    using trans_FD by blast
  from * ** have 7:"left❙?x → right❙!x → P ⊑⇩F⇩D left❙?x → right❙!x → COPY"
    by (simp add: mono_read_FD mono_write_FD)

  show "(Λ x. ⊓xa∈(range left ∪ range right) →  x)⋅
             ((Λ x. ⊓xa∈(range left ∪ range right) →  x)⋅P) ⊑⇩F⇩D COPY"
    by simp (metis (mono_tags, lifting) "6" "7" COPY_rec trans_FD)
qed

section‹ An Alternative Approach: Using the fixrec-Package ›

subsection‹ Channels and Synchronisation Sets ›

text‹ As before. ›

subsection‹ Process Definitions via fixrec-Package  ›

fixrec
  COPY' :: "'a channel process"
  and
  SEND' :: "'a channel process"
  and
  REC' :: "'a channel process"
  where
    COPY'_rec[simp del]:  "COPY' = left❙?x → right❙!x → COPY'"
  |  SEND'_rec[simp del]:  "SEND' = left❙?x → mid❙!x → ack → SEND'"
  |  REC'_rec[simp del] :  "REC'  = mid❙?x  → right❙!x → ack → REC'"

thm COPY'_rec
definition SYSTEM' :: "'a channel process"
  where     ‹SYSTEM' ≡ ((SEND' ⟦ SYN ⟧ REC') \ SYN)›

subsection‹ Another Refinement Proof on fixrec-infrastructure ›

text‹ Third part: No comes the proof by fixpoint induction. 
       Not too bad in automation considering what is inferred,
       but wouldn't scale for large examples. ›
thm COPY'_SEND'_REC'.induct
lemma impl_refines_spec'' : "(COPY'::'a channel process) ⊑⇩F⇩D SYSTEM'"
  apply (unfold SYSTEM'_def)
  apply (rule_tac P=‹λ a b c. a ⊑⇩F⇩D ((SEND' ⟦SYN⟧ REC') \ SYN)› in COPY'_SEND'_REC'.induct)
    apply (subst case_prod_beta')+
    apply (intro le_FD_adm, simp_all add: monofunI)
  apply (subst SEND'_rec, subst REC'_rec)
  by (simp add: Sync_rules Hiding_rules mono_read_FD mono_write_FD)

lemma spec_refines_impl' : 
  assumes fin:  "finite (SYN::'a channel set)"
  shows         "SYSTEM' ⊑⇩F⇩D (COPY'::'a channel process)"
proof(unfold SYSTEM'_def, rule_tac P=‹λ a b c. ((b ⟦SYN⟧ REC') \ SYN) ⊑⇩F⇩D COPY'› 
    in  COPY'_SEND'_REC'.induct, goal_cases)
  case 1
  have aa:‹adm (λ(a::'a channel process). ((a ⟦SYN⟧ REC') \ SYN) ⊑⇩F⇩D COPY')›
    apply (intro le_FD_adm)
    by (simp_all add: fin cont2mono)
  thus ?case using adm_subst[of "λ(a,b,c). b", simplified, OF aa] by (simp add: split_def)
next
  case 2
  then show ?case by (simp add: Sync_commute)
next
  case (3 a aa b)
  then show ?case 
    by (subst COPY'_rec, subst REC'_rec)
      (simp add: Sync_rules Hiding_rules mono_read_FD mono_write_FD)
qed

lemma spec_equal_impl' : 
  assumes fin:  "finite (SYN::('a channel)set)"
  shows         "SYSTEM' = (COPY'::'a channel process)"
  apply (rule FD_antisym)
   apply (rule spec_refines_impl'[OF fin])
  apply (rule impl_refines_spec'')
  done



subsection‹Proof-techniques over alphabets of processes:›

text‹An elementary proof technique to determine the alphabet ‹α(P)› of a process ‹P› (which is 
in general a true subset of the set of possible events ‹Σ›) is based on a noetherian induction
principle over the length of lists:›

lemma alphabet_of_COPY : ‹α(COPY::('α channel) process) = range left ∪ range right›
proof(intro equalityI)
  show "α(COPY::('α channel) process) ⊆ range left ∪ range right" 
  proof -
    have * : "size t ≤ n ⟹ t ∈ 𝒯 COPY ⟹ x ∉ range right ⟹ ev x ∈ set t ⟹ x ∈ range left"  
      for n::nat and x::‹'α channel› and t:: ‹'α channel trace›
      proof(induct n  arbitrary : x t)
        case 0
        then show ?case by simp 
      next
        case (Suc n)
        then show ?case
        proof -
          assume 1 : ‹t ∈ 𝒯 COPY›
          have  ** : ‹t ∈ 𝒯 (left❙?x → right❙!x → COPY)› by (metis COPY_rec Suc.prems(2))
          assume 2 : ‹x ∉ range right›
          assume 3 : ‹ev x ∈ set t›
          show       ‹x ∈ range left›
            apply(insert **) 
            apply(subst (asm) T_read_inj_on, meson channel.inject(1) injI)
            apply(auto) using 3 apply force
            apply(subst (asm) T_write, auto) 
            using 3 apply auto[1] 
            by (metis Suc.hyps Suc.prems(1) 2 3 Suc_leD Suc_le_mono event⇩p⇩t⇩i⇩c⇩k.inject(1) 
                      insertE length_Cons list.simps(15) range_eqI)
        qed
      qed
    show ?thesis
      unfolding events_of_def 
      using * by blast
  qed
next
  show "range left ∪ range right ⊆ α(COPY::('α channel) process)"
  proof - 
    have * : " ∃x∈𝒯 (COPY::('α channel) process). ev (left xa) ∈ set x" for xa
               apply(subst COPY_rec) 
               by (metis (mono_tags, lifting) Mprefix_projs(3) Nil_elem_T insert_iff 
                         list.simps(15) mem_Collect_eq rangeI  read_def)
    have **: " ∃x∈𝒯 (COPY::('α channel) process). ev (right xa) ∈ set x" for xa
               apply(subst COPY_rec) 
               apply(subst T_read_inj_on,meson channel.inject(1) injI)
               by (metis (mono_tags, lifting) T_write UNIV_I insert_iff 
                          is_processT1_TR list.simps(15) mem_Collect_eq)
   show ?thesis
     unfolding events_of_def using * ** by auto
  qed   
qed

text‹ A more advanced technique promising a higher degree of automation is requiring a 
restriction space  argument, which is not yet at our disposition here. ›

section‹More on CopyBuffer›

text‹The CopyBuffer is a running example in the HOL-CSP theory and will be reused as a demonstrator
in various contexts, be it in proofs or model-checking. With respect to the former, the reader is
referred to the session ▩‹CSP_RefTK› where specific support for deadlock and lifelock refinement
proofs is developed, such that goals of the form:

@{theory_text [indent=10,margin=70] 
‹corollary df_COPY: "deadlock_free COPY"
      and  lf_COPY: "lifelock_free COPY"›}

can be solved with a reasonable degree of automation.

With respect to model-checking, the reader is referred to the session  ▩‹FDR› where techniques for
finitised model-checking of HOL-CSP processes is introduced. 
›



(*<*)
end
(*>*)