Theory CIMP_lang

(*<*)
(*
 * 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_lang
imports
  CIMP_pred
  LTL
begin

(*>*)
section‹CIMP syntax and semantics \label{sec:cimp-syntax-semantics}›

text‹

We define a small sequential programming language with synchronous
message passing primitives for describing the individual
processes. This has the advantage over raw transition systems in that
it is programmer-readable, includes sequential composition, supports a
program logic and VCG (\S\ref{sec:cimp-vcg}), etc. These processes are
composed in parallel at the top-level.

CIMP is inspired by IMP, as presented by citet‹"Winskel:1993"› and citet‹"ConcreteSemantics:2014"›, and the classical process algebras CCS
citep‹"Milner:1980" and "Milner:1989"› and CSP
citep‹"Hoare:1985"›. Note that the algebraic
properties of this language have not been developed.

As we operate in a concurrent setting, we need to provide a small-step
semantics (\S\ref{sec:cimp-semantics}), which we give in the style of
\emph{structural operational semantics} (SOS) as popularised by citet‹"DBLP:journals/jlp/Plotkin04"›. The semantics of a
complete system (\S\ref{sec:cimp-system-steps}) is presently taken
simply to be the states reachable by interleaving the enabled steps of
the individual processes, subject to message passing rendezvous. We
leave a trace or branching semantics to future work.

This theory contains all the trusted definitions. The soundness of the other
theories supervenes upon this one.

›


subsection‹Syntax›

text‹

Programs are represented using an explicit (deep embedding) of their
syntax, as the semantics needs to track the progress of multiple
threads of control. Each (atomic) \emph{basic command}
(\S\ref{sec:cimp-decompose}) is annotated with a @{typ "'location"},
which we use in our assertions (\S\ref{sec:cimp-control-predicates}).
These locations need not be unique, though in practice they likely
will be.

Processes maintain \emph{local states} of type @{typ "'state"}. These
can be updated with arbitrary relations of @{typ "'state ⇒ 'state
set"} with ‹LocalOp›, and conditions of type @{typ "'s ⇒
bool"} are similarly shallowly embedded. This arrangement allows the
end-user to select their own level of atomicity.

The sequential composition operator and control constructs are
standard. We add the infinite looping construct ‹Loop› so we
can construct single-state reactive systems; this has implications for
fairness assertions.

›

type_synonym 's bexp = "'s ⇒ bool"

datatype ('answer, 'location, 'question, 'state) com
  = Request  "'location" "'state ⇒ 'question" "'answer ⇒ 'state ⇒ 'state set"        (‹⦃_⦄ Request _ _›  [0, 70, 70] 71)
  | Response "'location" "'question ⇒ 'state ⇒ ('state × 'answer) set"               (‹⦃_⦄ Response _›  [0, 70] 71)
  | LocalOp  "'location" "'state ⇒ 'state set"                                       (‹⦃_⦄ LocalOp _› [0, 70] 71)
  | Cond1    "'location" "'state bexp" "('answer, 'location, 'question, 'state) com" (‹⦃_⦄ IF _ THEN _ FI› [0, 0, 0] 71)
  | Cond2    "'location" "'state bexp" "('answer, 'location, 'question, 'state) com"
                           "('answer, 'location, 'question, 'state) com"             (‹⦃_⦄ IF _/ THEN _/ ELSE _/ FI›  [0, 0, 0, 0] 71)
  | Loop     "('answer, 'location, 'question, 'state) com"                           (‹LOOP DO _/ OD›  [0] 71)
  | While    "'location" "'state bexp" "('answer, 'location, 'question, 'state) com" (‹⦃_⦄ WHILE _/ DO _/ OD›  [0, 0, 0] 71)
  | Seq      "('answer, 'location, 'question, 'state) com"
              "('answer, 'location, 'question, 'state) com"                           (infixr ‹;;› 69)
  | Choose   "('answer, 'location, 'question, 'state) com"
              "('answer, 'location, 'question, 'state) com"                           (infixl ‹⊕› 68)

text‹

We provide a one-armed conditional as it is the common form and avoids
the need to discover a label for an internal ‹SKIP› and/or
trickier proofs about the VCG.

In contrast to classical process algebras, we have local state and
distinct request and response actions. These provide an interface to
Isabelle/HOL's datatypes that avoids the need for binding (ala the
$\pi$-calculus of citet‹"Milner:1989"›) or large
non-deterministic sums (ala CCS citep‹‹\S2.8› in
"Milner:1980"›). Intuitively the requester poses a @{typ "'question"} with
a ‹Request› command, which upon rendezvous with a
responder's ‹Response› command receives an @{typ
"'answer"}. The @{typ "'question"} is a deterministic function of the
requester's local state, whereas responses can be
non-deterministic. Note that CIMP does not provide a notion of
channel; these can be modelled by a judicious choice of @{typ
"'question"}.

We also provide a binary external choice operator @{term‹Choose›} (infix @{term‹(⊕)›}).
Internal choice can be recovered in combination with local operations
(see citet‹‹\S2.3› in "Milner:1980"›).

We abbreviate some common commands: ‹SKIP› is a local
operation that does nothing, and the floor brackets simplify
deterministic ‹LocalOp›s. We also adopt some syntax magic from
Makarius's ‹Hoare› and ‹Multiquote› theories in the Isabelle/HOL
distribution.

›

abbreviation SKIP_syn (‹⦃_⦄/ SKIP› [0] 71) where
  "⦃l⦄ SKIP ≡ ⦃l⦄ LocalOp (λs. {s})"

abbreviation (input) DetLocalOp :: "'location ⇒ ('state ⇒ 'state)
                                  ⇒ ('answer, 'location, 'question, 'state) com" (‹⦃_⦄ ⌊_⌋› [0, 0] 71) where
  "⦃l⦄ ⌊f⌋ ≡ ⦃l⦄ LocalOp (λs. {f s})"

syntax
  "_quote"        :: "'b ⇒ ('a ⇒ 'b)" (‹«_»› [0] 1000)
  "_antiquote"    :: "('a ⇒ 'b) ⇒ 'b" (‹´_› [1000] 1000)
  "_Assign"       :: "'location ⇒ idt ⇒ 'b ⇒ ('answer, 'location, 'question, 'state) com" (‹(⦃_⦄ ´_ :=/ _)› [0, 0, 70] 71)
  "_NonDetAssign" :: "'location ⇒ idt ⇒ 'b set ⇒ ('answer, 'location, 'question, 'state) com" (‹(⦃_⦄ ´_ :∈/ _)› [0, 0, 70] 71)

abbreviation (input) NonDetAssign :: "'location ⇒ (('val ⇒ 'val) ⇒ 'state ⇒ 'state) ⇒ ('state ⇒ 'val set)
                                   ⇒ ('answer, 'location, 'question, 'state) com" where
  "NonDetAssign l upd es ≡ ⦃l⦄ LocalOp (λs. { upd ⟨e⟩ s |e. e ∈ es s })"

translations
  "⦃l⦄ ´x := e" => "CONST DetLocalOp l «´(_update_name x (λ_. e))»"
  "⦃l⦄ ´x :∈ es" => "CONST NonDetAssign l (_update_name x) «es»"

parse_translation ‹
  let
    fun antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $
          (t as Const (@{syntax_const "_antiquote"}, _) $ _)) = skip_antiquote_tr i t
      | antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $ t) =
          antiquote_tr i t $ Bound i
      | antiquote_tr i (t $ u) = antiquote_tr i t $ antiquote_tr i u
      | antiquote_tr i (Abs (x, T, t)) = Abs (x, T, antiquote_tr (i + 1) t)
      | antiquote_tr _ a = a
    and skip_antiquote_tr i ((c as Const (@{syntax_const "_antiquote"}, _)) $ t) =
          c $ skip_antiquote_tr i t
      | skip_antiquote_tr i t = antiquote_tr i t;

    fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
      | quote_tr ts = raise TERM ("quote_tr", ts);
  in [(@{syntax_const "_quote"}, K quote_tr)] end
›


subsection‹Process semantics \label{sec:cimp-semantics} ›

text‹

Here we define the semantics of a single process's program. We begin
by defining the type of externally-visible behaviour:

›

datatype ('answer, 'question) seq_label
  = sl_Internal (‹τ›)
  | sl_Send 'question 'answer (‹«_, _»›)
  | sl_Receive 'question 'answer (‹»_, _«›)

text‹

We define a \emph{labelled transition system} (an LTS) using an
execution-stack style of semantics that avoids special treatment of
the ‹SKIP›s introduced by a traditional small step
semantics (such as citet‹‹Chapter~14› in
"Winskel:1993"›) when a basic command is executed. This was suggested
by Thomas Sewell; citet‹"PittsAM:opespe"› gave a
semantics to an ML-like language using this approach.

We record the location of the command that was executed to support
fairness constraints.

›

type_synonym ('answer, 'location, 'question, 'state) local_state
  = "('answer, 'location, 'question, 'state) com list × 'location option × 'state"

inductive
  small_step :: "('answer, 'location, 'question, 'state) local_state
               ⇒ ('answer, 'question) seq_label
               ⇒ ('answer, 'location, 'question, 'state) local_state ⇒ bool" (‹_ →⇘_⇙ _› [55, 0, 56] 55)
where
  "⟦ α = action s; s' ∈ val β s ⟧ ⟹ (⦃l⦄ Request action val # cs, _, s) →⇘«α, β»⇙ (cs, Some l, s')"
| "(s', β) ∈ action α s ⟹ (⦃l⦄ Response action # cs, _, s) →⇘»α, β«⇙ (cs, Some l, s')"

| "s' ∈ R s ⟹ (⦃l⦄ LocalOp R # cs, _, s) →⇘τ⇙ (cs, Some l, s')"

| "b s ⟹ (⦃l⦄ IF b THEN c FI # cs, _, s) →⇘τ⇙ (c # cs, Some l, s)"
| "¬b s ⟹ (⦃l⦄ IF b THEN c FI # cs, _, s) →⇘τ⇙ (cs, Some l, s)"

| "b s ⟹ (⦃l⦄ IF b THEN c1 ELSE c2 FI # cs, _, s) →⇘τ⇙ (c1 # cs, Some l, s)"
| "¬b s ⟹ (⦃l⦄ IF b THEN c1 ELSE c2 FI # cs, _, s) →⇘τ⇙ (c2 # cs, Some l, s)"

| "(c # LOOP DO c OD # cs, s) →⇘α⇙ (cs', s') ⟹ (LOOP DO c OD # cs, s) →⇘α⇙ (cs', s')"

| "b s ⟹ (⦃l⦄ WHILE b DO c OD # cs, _, s) →⇘τ⇙ (c # ⦃l⦄ WHILE b DO c OD # cs, Some l, s)"
| "¬ b s ⟹ (⦃l⦄ WHILE b DO c OD # cs, _, s) →⇘τ⇙ (cs, Some l, s)"

| "(c1 # c2 # cs, s) →⇘α⇙ (cs', s') ⟹ (c1;; c2 # cs, s) →⇘α⇙ (cs', s')"

| Choose1: "(c1 # cs, s) →⇘α⇙ (cs', s') ⟹ (c1 ⊕ c2 # cs, s) →⇘α⇙ (cs', s')"
| Choose2: "(c2 # cs, s) →⇘α⇙ (cs', s') ⟹ (c1 ⊕ c2 # cs, s) →⇘α⇙ (cs', s')"

text‹

The following projections operate on local states. These should not
appear to the end-user.

›

abbreviation cPGM :: "('answer, 'location, 'question, 'state) local_state ⇒ ('answer, 'location, 'question, 'state) com list" where
  "cPGM ≡ fst"

abbreviation cTKN :: "('answer, 'location, 'question, 'state) local_state ⇒ 'location option" where
  "cTKN s ≡ fst (snd s)"

abbreviation cLST :: "('answer, 'location, 'question, 'state) local_state ⇒ 'state" where
  "cLST s ≡ snd (snd s)"


subsection‹System steps \label{sec:cimp-system-steps}›

text‹

A global state maps process names to process' local states. One might
hope to allow processes to have distinct types of local state, but
there remains no good solution yet in a simply-typed setting; see
citet‹"DBLP:journals/entcs/SchirmerW09"›.

›

type_synonym ('answer, 'location, 'proc, 'question, 'state) global_state
  = "'proc ⇒ ('answer, 'location, 'question, 'state) local_state"

type_synonym ('proc, 'state) local_states
  = "'proc ⇒ 'state"

text‹

An execution step of the overall system is either any enabled internal
@{term "τ"} step of any process, or a communication rendezvous between
two processes. For the latter to occur, a @{const "Request"} action
must be enabled in process @{term "p1"}, and a @{const "Response"}
action in (distinct) process @{term "p2"}, where the request/response
labels @{term "α"} and @{term "β"} (semantically) match.

We also track global communication history here to support assertional
reasoning (see \S\ref{sec:cimp-invariants}).

›

type_synonym ('answer, 'question) event = "'question × 'answer"
type_synonym ('answer, 'question) history = "('answer, 'question) event list"

record ('answer, 'location, 'proc, 'question, 'state) system_state =
  GST :: "('answer, 'location, 'proc, 'question, 'state) global_state"
  HST :: "('answer, 'question) history"

inductive ―‹ This is a predicate of the current state, so the successor state comes first. ›
  system_step :: "'proc set
              ⇒ ('answer, 'location, 'proc, 'question, 'state) system_state
              ⇒ ('answer, 'location, 'proc, 'question, 'state) system_state
              ⇒ bool"
where
  LocalStep: "⟦ GST sh p →⇘τ⇙ ls'; GST sh' = (GST sh)(p := ls'); HST sh' = HST sh ⟧ ⟹ system_step {p} sh' sh"
| CommunicationStep: "⟦ GST sh p →⇘«α, β»⇙ ls1'; GST sh q →⇘»α, β«⇙ ls2'; p ≠ q;
                        GST sh' = (GST sh)(p := ls1', q := ls2'); HST sh' = HST sh @ [(α, β)] ⟧ ⟹ system_step {p, q} sh' sh"

text‹

In classical process algebras matching communication actions yield
‹τ› steps, which aids nested parallel composition
and the restriction operation citep‹‹\S2.2› in "Milner:1980"›. As CIMP does not provide either
we do not need to hide communication labels. In CCS/CSP it is not
clear how one reasons about the communication history, and it seems
that assertional reasoning about these languages is not well
developed.

›

text‹

We define predicates over communication histories and system states. These are uncurried to ease composition.

›

type_synonym ('answer, 'location, 'proc, 'question, 'state) state_pred
  = "('answer, 'location, 'proc, 'question, 'state) system_state ⇒ bool"

text‹

The ‹LST› operator (written as a postfix ‹↓›) projects
the local states of the processes from a typ‹('answer, 'location, 'proc, 'question, 'state) system_state›, i.e. it
discards control location information.

Conversely the ‹LSTP› operator lifts predicates over
local states into predicates over typ‹('answer, 'location, 'proc, 'question, 'state) system_state›.

Predicates that do not depend on control locations were termed @{emph
‹universal assertions›} by citet‹‹\S3.6› in "DBLP:journals/acta/LevinG81"›.

›

type_synonym ('proc, 'state) local_state_pred
  = "('proc, 'state) local_states ⇒ bool"

definition LST :: "('answer, 'location, 'proc, 'question, 'state) system_state
                 ⇒ ('proc, 'state) local_states" (‹_↓› [1000] 1000) where
  "s↓ = cLST ∘ GST s"

abbreviation (input) LSTP :: "('proc, 'state) local_state_pred
                            ⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred" where
  "LSTP P ≡ λs. P s↓"


subsection‹Control predicates \label{sec:cimp-control-predicates}›

text‹

Following citet‹"DBLP:journals/acta/Lamport80"›\footnote{citet‹"MannaPnueli:1995"› also develop a theory of locations. I think
Lamport attributes control predicates to Owicki in her PhD thesis
(under Gries). I did not find a treatment of procedures. citet‹"MannaPnueli:1991"› observe that a notation for
making assertions over sets of locations reduces clutter
significantly.}, we define the ‹at› predicate, which
holds of a process when control resides at that location. Due to
non-determinism processes can be ‹at› a set of locations;
it is more like ``a statement with this location is enabled'', which
incidentally handles non-unique locations. Lamport's language is
deterministic, so he doesn't have this problem. This also allows him
to develop a stronger theory about his control predicates.

›

type_synonym 'location label = "'location set"

primrec
  atC :: "('answer, 'location, 'question, 'state) com ⇒ 'location label"
where
  "atC (⦃l⦄ Request action val) = {l}"
| "atC (⦃l⦄ Response action) = {l}"
| "atC (⦃l⦄ LocalOp f) = {l}"
| "atC (⦃l⦄ IF _ THEN _ FI) = {l}"
| "atC (⦃l⦄ IF _ THEN _ ELSE _ FI) = {l}"
| "atC (⦃l⦄ WHILE _ DO _ OD) = {l}"
| "atC (LOOP DO c OD) = atC c"
| "atC (c1;; c2) = atC c1"
| "atC (c1 ⊕ c2) = atC c1 ∪ atC c2"

primrec atCs :: "('answer, 'location, 'question, 'state) com list ⇒ 'location label" where
  "atCs [] = {}"
| "atCs (c # _) = atC c"

text‹

We provide the following definitions to the end-user.

‹AT› maps process names to a predicate that is true of
locations where control for that process resides, and the abbreviation ‹at› provides a conventional
way to use it. The constant ‹atS› specifies that control for process ‹p› resides at one of
the given locations. This stands in for, and generalises, the ‹in› predicate of citet‹"DBLP:journals/acta/Lamport80"›.

›

definition AT :: "('answer, 'location, 'proc, 'question, 'state) system_state ⇒ 'proc ⇒ 'location label" where
  "AT s p = atCs (cPGM (GST s p))"

abbreviation at :: "'proc ⇒ 'location ⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred" where
  "at p l s ≡ l ∈ AT s p"

definition atS :: "'proc ⇒ 'location set ⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred" where
  "atS p ls s = (∃l∈ls. at p l s)"

(* FIXME rename, document, rules. Identifies a process's control state label precisely as one element of a set. *)
definition atLs :: "'proc ⇒ 'location label set ⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred" where
  "atLs p labels s = (AT s p ∈ labels)"

(* FIXME rename, document. Identifies a process's control state label precisely. Relate atL to at/atS, ex/ *)
abbreviation (input) atL :: "'proc ⇒ 'location label ⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred" where
  "atL p label ≡ atLs p {label}"

(* FIXME rename, document. Processes are at the given labels. *)
definition atPLs :: "('proc × 'location label) set ⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred" where
  "atPLs pls = (∀p label. ⟨(p, label) ∈ pls⟩ ⟶ atL p label)"

text‹

The constant ‹taken› provides a way of identifying which transition was taken. It is somewhat like
Lamport's ‹after›, but not quite due to the presence of non-determinism here. This does not work well
for invariants or preconditions.

›

definition taken :: "'proc ⇒ 'location ⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred" where
  "taken p l s ⟷ cTKN (GST s p) = Some l"

text‹

\label{sec:cimp-termination}

A process is terminated if it not at any control location.

›

abbreviation (input) terminated :: "'proc ⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred" where
  "terminated p ≡ atL p {}"

text‹

A complete system consists of one program per process, and a (global)
constraint on their initial local states. From these we can construct
the set of initial global states and all those reachable by system
steps (\S\ref{sec:cimp-system-steps}).

›

type_synonym ('answer, 'location, 'proc, 'question, 'state) programs
  = "'proc ⇒ ('answer, 'location, 'question, 'state) com"

record ('answer, 'location, 'proc, 'question, 'state) pre_system =
  PGMs :: "('answer, 'location, 'proc, 'question, 'state) programs"
  INIT :: "('proc, 'state) local_state_pred"

definition
  initial_state :: "('answer, 'location, 'proc, 'question, 'state, 'ext) pre_system_ext
                   ⇒ ('answer, 'location, 'proc, 'question, 'state) global_state
                   ⇒ bool"
where
  "initial_state sys s = ((∀p. cPGM (s p) = [PGMs sys p] ∧ cTKN (s p) = None) ∧ INIT sys (cLST ∘ s))"

text‹

We construct infinite runs of a system by allowing stuttering, i.e., arbitrary repetitions of states
following citet‹‹Chapter~8› in"Lamport:2002"›, by taking the reflexive
closure of the @{const system_step} relation. Therefore terminated
programs infinitely repeat their final state (but note our definition
of terminated processes in \S\ref{sec:cimp-termination}).

Some accounts define stuttering as the @{emph ‹finite›} repetition of states. With or without this constraint
‹prerun› contains @{emph ‹junk›} in the form of unfair runs, where particular processes do not progress.

›

definition
  system_step_reflclp :: "('answer, 'location, 'proc, 'question, 'state) system_state seq_pred"
where
  "system_step_reflclp σ ⟷ (λsh sh'. ∃pls. system_step pls sh' sh)== (σ 0) (σ 1)"

definition
  prerun :: "('answer, 'location, 'proc, 'question, 'state, 'ext) pre_system_ext
         ⇒ ('answer, 'location, 'proc, 'question, 'state) system_state seq_pred"
where
  "prerun sys = ((λσ. initial_state sys (GST (σ 0)) ∧ HST (σ 0) = []) ∧ □system_step_reflclp)"

definition ―‹ state-based invariants only ›
  prerun_valid :: "('answer, 'location, 'proc, 'question, 'state, 'ext) pre_system_ext
                   ⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred ⇒ bool" (‹_ ⊨pre _› [11, 0] 11) (* FIXME priorities *)
where
  "(sys ⊨pre φ) ⟷ (∀σ. prerun sys σ ⟶ (□⌈φ⌉) σ)"

text‹

A ‹run› of a system is a @{const ‹prerun›} that satisfies the ‹FAIR› requirement.
Typically this would include @{emph ‹weak fairness›} for every transition of every process.

›

record ('answer, 'location, 'proc, 'question, 'state) system =
  "('answer, 'location, 'proc, 'question, 'state) pre_system"
+ FAIR :: "('answer, 'location, 'proc, 'question, 'state) system_state seq_pred"

definition
  run :: "('answer, 'location, 'proc, 'question, 'state) system
       ⇒ ('answer, 'location, 'proc, 'question, 'state) system_state seq_pred"
where
  "run sys = (prerun sys ∧ FAIR sys)"

definition
  valid :: "('answer, 'location, 'proc, 'question, 'state) system
                   ⇒ ('answer, 'location, 'proc, 'question, 'state) system_state seq_pred ⇒ bool" (‹_ ⊨ _› [11, 0] 11) (* FIXME priorities *)
where
  "(sys ⊨ φ) ⟷ (∀σ. run sys σ ⟶ φ σ)"
(*<*)

end
(*>*)