Theory CIMP_one_place_buffer

(*<*)
(*
 * Copyright 2015, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

theory CIMP_one_place_buffer
imports
  "../CIMP"
begin

(*>*)
section‹Example: a one-place buffer \label{sec:one_place_buffer}›

text‹

To demonstrate the CIMP reasoning infrastructure, we treat the trivial
one-place buffer example of \<^citet>‹‹\S3.3› in "DBLP:journals/toplas/LamportS84"›. Note that the
semantics for our language is different to \<^cite>‹"DBLP:journals/toplas/LamportS84" using "citeauthor"›'s, who
treated a historical variant of CSP (i.e., not the one in \<^cite>‹"Hoare:1985"›).

We introduce some syntax for fixed-topology (static channel-based)
scenarios.

›

abbreviation
  rcv_syn :: "'location ⇒ 'channel ⇒ ('val ⇒ 'state ⇒ 'state)
           ⇒ (unit, 'location, 'channel × 'val, 'state) com" ("⦃_⦄/ _▹_" [0,0,81] 81)
where
  "⦃l⦄ ch▹f ≡ ⦃l⦄ Response (λq s. if fst q = ch then {(f (snd q) s, ())} else {})"

abbreviation
  snd_syn :: "'location ⇒ 'channel ⇒ ('state ⇒ 'val)
          ⇒ (unit, 'location, 'channel × 'val, 'state) com" ("⦃_⦄/ _◃_" [0,0,81] 81)
where
  "⦃l⦄ ch◃f ≡ ⦃l⦄ Request (λs. (ch, f s)) (λans s. {s})"

text‹

These definitions largely follow \<^citet>‹"DBLP:journals/toplas/LamportS84"›. We have three processes
communicating over two channels. We enumerate program locations.

›

datatype ex_chname = ξ12 | ξ23
type_synonym ex_val = nat
type_synonym ex_ch = "ex_chname × ex_val"
datatype ex_loc = r12 | r23 | s23 | s12
datatype ex_proc = p1 | p2 | p3

type_synonym ex_pgm = "(unit, ex_loc, ex_ch, ex_val) com"
type_synonym ex_pred = "(unit, ex_loc, ex_proc, ex_ch, ex_val) state_pred"
type_synonym ex_state = "(unit, ex_loc, ex_proc, ex_ch, ex_val) system_state"
type_synonym ex_sys = "(unit, ex_loc, ex_proc, ex_ch, ex_val) system"
type_synonym ex_history = "(ex_ch × unit) list"

text‹

We further specialise these for our particular example.

›

primrec
  ex_coms :: "ex_proc ⇒ ex_pgm"
where
  "ex_coms p1 = ⦃s12⦄ ξ12◃id"
| "ex_coms p2 = LOOP DO ⦃r12⦄ ξ12▹(λv _. v) ;; ⦃s23⦄ ξ23◃id OD"
| "ex_coms p3 = ⦃r23⦄ ξ23▹(λv _. v)"

text‹

Each process starts with an arbitrary initial local state.

›

abbreviation ex_init :: "(ex_proc ⇒ ex_val) ⇒ bool" where
  "ex_init ≡ ⟨True⟩"

abbreviation sys :: ex_sys where
  "sys ≡ ⦇PGMs = ex_coms, INIT = ex_init, FAIR = ⟨True⟩⦈" (* FIXME add fairness hypotheses *)

text‹

The following adapts Kai Engelhardt's, from his notes titled
\emph{Proving an Asynchronous Message Passing Program Correct},
2011. The history variable tracks the causality of the system, which I
feel is missing in Lamport's treatment. We tack on Lamport's invariant
so we can establish ‹Etern_pred›.

›

abbreviation
  filter_on_channel :: "ex_chname ⇒ ex_state ⇒ ex_val list" ("⇂_" [100] 101)
where
  "⇂ch ≡ map (snd ∘ fst) ∘ filter ((=) ch ∘ fst ∘ fst) ∘ HST"

definition IL :: ex_pred where
  "IL = pred_conjoin [
       at p1 s12 ❙⟶ LIST_NULL ⇂ξ12
     , terminated p1 ❙⟶ ⇂ξ12 ❙= (λs. [s↓ p1])
     , at p2 r12 ❙⟶ ⇂ξ12 ❙= ⇂ξ23
     , at p2 s23 ❙⟶ ⇂ξ12 ❙= ⇂ξ23 ❙@ (λs. [s↓ p2]) ❙∧ (λs. s↓ p1 = s↓ p2)
     , at p3 r23 ❙⟶ LIST_NULL ⇂ξ23
     , terminated p3 ❙⟶ ⇂ξ23 ❙= (λs. [s↓ p2]) ❙∧ (λs. s↓ p1 = s↓ p3)
     ]"

text‹

If @{const p3} terminates, then it has @{const p1}'s value. This is
stronger than \<^cite>‹"DBLP:journals/toplas/LamportS84" using "citeauthor"›'s as we don't ask that the first
process has also terminated.

›

definition Etern_pred :: ex_pred where
  "Etern_pred = (terminated p3 ❙⟶ (λs. s↓ p1 = s↓ p3))"

text‹

Proofs from here down.

›

lemma correct_system:
  assumes "IL sh"
  shows "Etern_pred sh"
using assms unfolding Etern_pred_def IL_def by simp

lemma IL_p1: "ex_coms, p1, lconst {} ⊢ ⦃IL⦄ ⦃s12⦄ ξ12◃(λs. s)"
apply (rule vcg.intros)
apply (rename_tac p')
apply (case_tac p'; clarsimp simp: IL_def atLs_def)
done

lemma IL_p2: "ex_coms, p2, lconst {r12} ⊢ ⦃IL⦄ ⦃s23⦄ ξ23◃(λs. s)"
apply (rule vcg.intros)
apply (rename_tac p')
apply (case_tac p'; clarsimp simp: IL_def)
done

lemma IL: "sys ⊨⇘pre⇙ IL"
apply (rule VCG)
 apply (clarsimp simp: IL_def atLs_def dest!: initial_stateD)
apply (rename_tac p)
apply (case_tac p; clarsimp simp: IL_p1 IL_p2)
done

lemma IL_valid: "sys ⊨ □⌈IL⌉"
by (rule valid_prerun_lift[OF IL])

(*<*)

end
(*>*)