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 chf  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 chf  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 ξ12snoc
                       c1 IF (λs. length s > 0) THEN s23 ξ12(hd, tl) FI
                     OD"
| "ex_coms p3 = LOOP DO r23 ξ23snoc 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: "syspre 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
(*>*)