Networks of stateful processes and their semantics

This module defines networks (maps from process names to process terms), as well as their symbolic and concrete operational semantics.

Implementation notes

We leverage the fact that networks are functions to formulate the semantics without requiring a definition of parallel composition.

References

• F. Montesi, Introduction to Choreographies

Networks and their symbolic semantics

@[reducible, inline]

abbrev Cslib.StatefulProcesses.Network (Pid : Type u_1) (Var : Type u_2) (Val : Type u_3) (FunId : Type u_4) (SelLabel : Type u_5) (ProcName : Type u_6) : Type (max (max (max (max (max (max u_1 u_6) u_5) u_4) u_3) u_2) u_1)

A network maps process names to process terms.

Equations

• Cslib.StatefulProcesses.Network Pid Var Val FunId SelLabel ProcName = (Pid → Cslib.StatefulProcesses.Process Pid Var Val FunId SelLabel ProcName)

@[instance_reducible]

instance Cslib.StatefulProcesses.instZeroNetwork {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} : Zero (Network Pid Var Val FunId SelLabel ProcName)

The 0 ('zero') network, mapping all processes to the process term 0.

Equations

• Cslib.StatefulProcesses.instZeroNetwork = { zero := fun (x : Pid) => 0 }

inductive Cslib.StatefulProcesses.Network.TrLabel (Pid : Type u_1) (Var : Type u_2) (Val : Type u_3) (FunId : Type u_4) (SelLabel : Type u_5) : Type (max (max (max (max u_1 u_2) u_3) u_4) u_5)

Symbolic transition labels for networks.

• local {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} (p : Pid) (μ : Act Pid Var Val FunId SelLabel) : TrLabel Pid Var Val FunId SelLabel
• com {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} (p : Pid) (e : Mech.Expr Var Val FunId) (q : Pid) (x : Var) : TrLabel Pid Var Val FunId SelLabel
• sel {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} (p q : Pid) (l : SelLabel) : TrLabel Pid Var Val FunId SelLabel

inductive Cslib.StatefulProcesses.Network.Tr {Pid : Type u_1} [DecidableEq Pid] {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} : Network Pid Var Val FunId SelLabel ProcName → TrLabel Pid Var Val FunId SelLabel → Network Pid Var Val FunId SelLabel ProcName → Prop

Symbolic transition relation for networks.

• local {Pid : Type u_1} [DecidableEq Pid] {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} {n : Network Pid Var Val FunId SelLabel ProcName} {μ : Act Pid Var Val FunId SelLabel} {prP : Process Pid Var Val FunId SelLabel ProcName} {n' : Network Pid Var Val FunId SelLabel ProcName} {p : Pid} (hμ : μ.isInternal = true) (htr : Process.lts.Tr (n p) μ prP) (hn' : n' = n[p := prP]) : n.Tr (TrLabel.local p μ) n'
• com {Pid : Type u_1} [DecidableEq Pid] {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} {n : Network Pid Var Val FunId SelLabel ProcName} {q : Pid} {e : Mech.Expr Var Val FunId} {prP : Process Pid Var Val FunId SelLabel ProcName} {p : Pid} {x : Var} {prQ : Process Pid Var Val FunId SelLabel ProcName} {n' : Network Pid Var Val FunId SelLabel ProcName} (hsend : Process.lts.Tr (n p) (Act.sendValue q e) prP) (hrecv : Process.lts.Tr (n q) (Act.recvValue p x) prQ) (hn' : n' = n[p := prP][q := prQ]) : n.Tr (TrLabel.com p e q x) n'
• sel {Pid : Type u_1} [DecidableEq Pid] {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} {n : Network Pid Var Val FunId SelLabel ProcName} {q : Pid} {l : SelLabel} {prP : Process Pid Var Val FunId SelLabel ProcName} {p : Pid} {prQ : Process Pid Var Val FunId SelLabel ProcName} {n' : Network Pid Var Val FunId SelLabel ProcName} (hsend : Process.lts.Tr (n p) (Act.sendLabel q l) prP) (hrecv : Process.lts.Tr (n q) (Act.recvLabel p l) prQ) (hn' : n' = n[p := prP][q := prQ]) : n.Tr (TrLabel.sel p q l) n'

def Cslib.StatefulProcesses.Network.lts {Pid : Type u_1} [DecidableEq Pid] {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} : LTS (Network Pid Var Val FunId SelLabel ProcName) (TrLabel Pid Var Val FunId SelLabel)

Symbolic LTS of networks.

Equations

• Cslib.StatefulProcesses.Network.lts = { Tr := Cslib.StatefulProcesses.Network.Tr }

Stores, evaluation, and concrete semantics of networks

structure Cslib.StatefulProcesses.Cfg (Pid : Type u_1) (Var : Type u_2) (Val : Type u_3) (FunId : Type u_4) (SelLabel : Type u_5) (ProcName : Type u_6) : Type (max (max (max (max (max u_1 u_2) u_3) u_4) u_5) u_6)

Configurations, consisting of a network and a global store.

• net : Network Pid Var Val FunId SelLabel ProcName

  The network of the configuration.

• store : Mech.GlobalStore Pid Var Val

  The global store of the configuration.

inductive Cslib.StatefulProcesses.Cfg.TrLabel (Pid : Sort u_1) (Val : Sort u_2) (SelLabel : Sort u_3) : Sort (max (max (max 1 u_1) u_2) u_3)

Transition labels for network configurations.

These labels model what can be observed from execution, and thus hide internal computational details.

• local {Pid : Sort u_1} {Val : Sort u_2} {SelLabel : Sort u_3} (p : Pid) : TrLabel Pid Val SelLabel
• com {Pid : Sort u_1} {Val : Sort u_2} {SelLabel : Sort u_3} (p q : Pid) (v : Val) : TrLabel Pid Val SelLabel
• sel {Pid : Sort u_1} {Val : Sort u_2} {SelLabel : Sort u_3} (p q : Pid) (l : SelLabel) : TrLabel Pid Val SelLabel

inductive Cslib.StatefulProcesses.Cfg.Tr {Pid : Type u_1} [DecidableEq Pid] {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} [DecidableEq Var] (isTrue : Val → Bool) (Eval : Mech.FunCallEval FunId Val) {SelLabel : Type u_5} {ProcName : Type u_6} : Cfg Pid Var Val FunId SelLabel ProcName → TrLabel Pid Val SelLabel → Cfg Pid Var Val FunId SelLabel ProcName → Prop

Transition relation for network configurations.

• assign {Pid : Type u_1} [DecidableEq Pid] {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} [DecidableEq Var] {isTrue : Val → Bool} {Eval : Mech.FunCallEval FunId Val} {p : Pid} {x : Var} {e : Mech.Expr Var Val FunId} {v : Val} {x✝ : Type u_5} {x✝¹ : Type u_6} {cfg cfg' : Cfg Pid Var Val FunId x✝ x✝¹} (htr : Network.lts.Tr cfg.net (Network.TrLabel.local p (Act.assign x e)) cfg'.net) (heval : Eval.EvalExpr (cfg.store p) e v) (hstore : cfg'.store = cfg.store[(p, x) := v]) : Tr isTrue Eval cfg (TrLabel.local p) cfg'
• condThen {Pid : Type u_1} [DecidableEq Pid] {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} [DecidableEq Var] {isTrue : Val → Bool} {Eval : Mech.FunCallEval FunId Val} {p : Pid} {e : Mech.Expr Var Val FunId} {v : Val} {x✝ : Type u_5} {x✝¹ : Type u_6} {cfg cfg' : Cfg Pid Var Val FunId x✝ x✝¹} (htr : Network.lts.Tr cfg.net (Network.TrLabel.local p (Act.condThen e)) cfg'.net) (heval : Eval.EvalExpr (cfg.store p) e v) (hguard : isTrue v = true) (hstore : cfg'.store = cfg.store) : Tr isTrue Eval cfg (TrLabel.local p) cfg'
• condElse {Pid : Type u_1} [DecidableEq Pid] {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} [DecidableEq Var] {isTrue : Val → Bool} {Eval : Mech.FunCallEval FunId Val} {p : Pid} {e : Mech.Expr Var Val FunId} {v : Val} {x✝ : Type u_5} {x✝¹ : Type u_6} {cfg cfg' : Cfg Pid Var Val FunId x✝ x✝¹} (htr : Network.lts.Tr cfg.net (Network.TrLabel.local p (Act.condElse e)) cfg'.net) (heval : Eval.EvalExpr (cfg.store p) e v) (hguard : ¬isTrue v = true) (hstore : cfg'.store = cfg.store) : Tr isTrue Eval cfg (TrLabel.local p) cfg'
• com {Pid : Type u_1} [DecidableEq Pid] {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} [DecidableEq Var] {isTrue : Val → Bool} {Eval : Mech.FunCallEval FunId Val} {p : Pid} {e : Mech.Expr Var Val FunId} {q : Pid} {x : Var} {v : Val} {x✝ : Type u_5} {x✝¹ : Type u_6} {cfg cfg' : Cfg Pid Var Val FunId x✝ x✝¹} (htr : Network.lts.Tr cfg.net (Network.TrLabel.com p e q x) cfg'.net) (heval : Eval.EvalExpr (cfg.store p) e v) (hstore : cfg'.store = cfg.store[(q, x) := v]) : Tr isTrue Eval cfg (TrLabel.com p q v) cfg'
• sel {Pid : Type u_1} [DecidableEq Pid] {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} [DecidableEq Var] {isTrue : Val → Bool} {Eval : Mech.FunCallEval FunId Val} {p q : Pid} {x✝ : Type u_5} {l : x✝} {x✝¹ : Type u_6} {cfg cfg' : Cfg Pid Var Val FunId x✝ x✝¹} (htr : Network.lts.Tr cfg.net (Network.TrLabel.sel p q l) cfg'.net) (hstore : cfg'.store = cfg.store) : Tr isTrue Eval cfg (TrLabel.sel p q l) cfg'

def Cslib.StatefulProcesses.Cfg.lts {Pid : Type u_1} [DecidableEq Pid] {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} [DecidableEq Var] (isTrue : Val → Bool) (Eval : Mech.FunCallEval FunId Val) : LTS (Cfg Pid Var Val FunId SelLabel ProcName) (TrLabel Pid Val SelLabel)

LTS of network configurations.

Equations

• Cslib.StatefulProcesses.Cfg.lts isTrue Eval = { Tr := Cslib.StatefulProcesses.Cfg.Tr isTrue Eval }