Theory CIMP_unbounded_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_unbounded_buffer
imports
  "../CIMP"
  "HOL-Library.Prefix_Order"
begin

abbreviation (input)
  Receive :: "'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 (input)
  Send :: "'location ⇒ 'channel ⇒ ('state ⇒ 'val) × ('state ⇒ 'state)
          ⇒ (unit, 'location, 'channel × 'val, 'state) com" (‹⦃_⦄/ _◃_› [0,0,81] 81)
where
  "⦃l⦄ ch◃f ≡ ⦃l⦄ Request (λs. (ch, fst f s)) (λans s. {snd f s})"

(*>*)
section‹Example: an unbounded buffer \label{sec:unbounded_buffer}›

text‹

This is more literally Kai Engelhardt's example from his notes titled
\emph{Proving an Asynchronous Message Passing Program Correct}, 2011.

›

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

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

text‹

The local state for the producer process contains all values produced; consider that ghost state.

›

abbreviation (input) snoc :: "'a ⇒ 'a list ⇒ 'a list" where "snoc x xs ≡ xs @ [x]"

primrec ex_coms :: "ex_proc ⇒ ex_pgm" where
  "ex_coms p1 = LOOP DO ⦃c1⦄ LocalOp (λxs. {snoc x xs |x. True}) ;; ⦃s12⦄ ξ12◃(last, id) OD"
| "ex_coms p2 = LOOP DO ⦃r12⦄ ξ12▹snoc
                      ⊕ ⦃c1⦄ IF (λs. length s > 0) THEN ⦃s23⦄ ξ12◃(hd, tl) FI
                     OD"
| "ex_coms p3 = LOOP DO ⦃r23⦄ ξ23▹snoc OD"

abbreviation ex_init :: "(ex_proc ⇒ ex_ls) ⇒ bool" where
  "ex_init s ≡ ∀p. s p = []"

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

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

definition I_pred :: ex_pred where
  "I_pred = pred_conjoin [
       at p1 c1 ❙⟶ ⇂ξ12 ❙= (λs. s↓ p1)
     , at p1 s12 ❙⟶ (λs. length (s↓ p1) > 0 ∧ butlast (s↓ p1) = (⇂ξ12) s)
     , ⇂ξ12 ❙≤ (λs. s↓ p1)
     , ⇂ξ12 ❙= ⇂ξ23 ❙@ (λs. s↓ p2)
     , at p2 s23 ❙⟶ (λs. length (s↓ p2) > 0)
     , (λs. s↓ p3) ❙= ⇂ξ23
     ]"

text‹

The local state of @{const "p3"} is some prefix of the local state of
@{const "p1"}.

›

definition Etern_pred :: ex_pred where
  "Etern_pred ≡ λs. s↓ p3 ≤ s↓ p1"

lemma correct_system:
  assumes "I_pred s"
  shows "Etern_pred s"
using assms unfolding Etern_pred_def I_pred_def less_eq_list_def prefix_def by clarsimp

lemma p1_c1[simplified, intro]:
  "ex_coms, p1, lconst {s12} ⊢ ⦃I_pred⦄ ⦃c1⦄ LocalOp (λxs. { snoc x xs |x. True })"
apply (rule vcg.intros)
apply (clarsimp simp: I_pred_def atS_def)
done

lemma p1_s12[simplified, intro]:
  "ex_coms, p1, lconst {c1} ⊢ ⦃I_pred⦄ ⦃s12⦄ ξ12◃(last, id)"
apply (rule vcg.intros)
apply (rename_tac p')
apply (case_tac p'; clarsimp)
apply (clarsimp simp: I_pred_def atS_def)
apply (metis Prefix_Order.prefix_snoc append.assoc append_butlast_last_id)
done

lemma p2_s23[simplified, intro]:
  "ex_coms, p2, lconst {c1, r12} ⊢ ⦃I_pred⦄ ⦃s23⦄ ξ12◃(hd, tl)"
apply (rule vcg.intros)
apply (rename_tac p')
apply (case_tac p'; clarsimp)
done

lemma p2_pi4[intro]:
  "ex_coms, p2, lcond {s23} {c1, r12} (λs. s ≠ []) ⊢ ⦃I_pred⦄ ⦃c1⦄ IF (λs. s ≠ []) THEN c' FI"
apply (rule vcg.intros)
apply (clarsimp simp: I_pred_def atS_def split: lcond_splits)
done

lemma I: "sys ⊨⇘pre⇙ I_pred"
apply (rule VCG)
 apply (clarsimp dest!: initial_stateD simp: I_pred_def atS_def)
apply (rename_tac p)
apply (case_tac p; auto)
done

lemma I_valid: "sys ⊨ □⌈I_pred⌉"
by (rule valid_prerun_lift[OF I])

(*<*)

end
(*>*)