Stateful Processes

The language of Stateful Processes (SP for short), a process calculus where processes communicate via message passing [Mon23]. Stateful processes or similar languages are typically used to model implementations of choreographic programs (concurrent and/or distributed protocols), but they are also designed to be used as abstract representations that can be later compiled to executable mainstream languages.

Limitations

The current formalisation does not cover process polymorphism (procedures do not take process parameters) nor general recursion (this is the tail-recursive fragment of Stateful Processes). For recursion, only the syntax is currently implemented. Its semantics will follow a similar approach to that for CCS.

Implementation notes

This development follows the presentation in [Mon23], with one difference: we adopt a modular approach to the definition of operational semantics, by first defining a symbolic semantics from which a concrete semantics is then derived by adding stores (process memory). This approach is described in [AMMQ26].

References

• M. Acclavio, G. Manara, F. Montesi, X. Qin, Choreographic Programming: a Semantic Approach
• F. Montesi, Introduction to Choreographies

Syntax of process terms

inductive Cslib.StatefulProcesses.Prefix (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)

Prefixes.

• assign {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} (x : Var) (e : Mech.Expr Var Val FunId) : Prefix Pid Var Val FunId SelLabel

  Assign to x the result of evaluating e.

• sendValue {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) : Prefix Pid Var Val FunId SelLabel

  Send to p the result of evaluating e.

• recvValue {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} (p : Pid) (x : Var) : Prefix Pid Var Val FunId SelLabel

  Receive a value from p and store it in x.

• sendLabel {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} (p : Pid) (l : SelLabel) : Prefix Pid Var Val FunId SelLabel

  Send to p the label l.

inductive Cslib.StatefulProcesses.Process (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)

Processes.

• nil {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} : Process Pid Var Val FunId SelLabel ProcName

  The terminated process.

• pre {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} (prf : Prefix Pid Var Val FunId SelLabel) (pr : Process Pid Var Val FunId SelLabel ProcName) : Process Pid Var Val FunId SelLabel ProcName

  Execute the prefix prf and proceed as the continuation pr.

• recvLabel {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} (p : Pid) (branches : List (SelLabel × Process Pid Var Val FunId SelLabel ProcName)) : Process Pid Var Val FunId SelLabel ProcName

  Branching process: receives a selection label and continues accordingly.

• cond {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} (e : Mech.Expr Var Val FunId) (pr₁ pr₂ : Process Pid Var Val FunId SelLabel ProcName) : Process Pid Var Val FunId SelLabel ProcName

  Conditional: evaluate e to choose between pr₁ and pr₂.

• call {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} (proc : ProcName) (ps : List Pid) : Process Pid Var Val FunId SelLabel ProcName

  Call the procedure proc.

@[instance_reducible]

instance Cslib.StatefulProcesses.instZeroProcess {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 (Process Pid Var Val FunId SelLabel ProcName)

Equations

• Cslib.StatefulProcesses.instZeroProcess = { zero := Cslib.StatefulProcesses.Process.nil }

def Cslib.StatefulProcesses.spPre.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.spPre : Category

Syntactic category for prefixes.

Equations

• Lean.Parser.Category.spPre = { }

def Cslib.StatefulProcesses.«spPre_≔_» : Lean.ParserDescr

Assign to x the result of evaluating e.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.StatefulProcesses.spPre_!_ : Lean.ParserDescr

Send to p the result of evaluating e.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.StatefulProcesses.spPre_?_ : Lean.ParserDescr

Receive a value from p and store it in x.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.StatefulProcesses.«spPre_⊕_» : Lean.ParserDescr

Send to p the label l.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.StatefulProcesses.«term`(SPpre|_)» : Lean.ParserDescr

Prefixes.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.spProc : Category

Syntactic category for processes.

Equations

• Lean.Parser.Category.spProc = { }

def Cslib.StatefulProcesses.spProc.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Cslib.StatefulProcesses.spProc_ : Lean.ParserDescr

The terminated process.

Equations

• Cslib.StatefulProcesses.spProc_ = Lean.ParserDescr.node `Cslib.StatefulProcesses.spProc_ 1022 (Lean.ParserDescr.const `num)

def Cslib.StatefulProcesses.«spProc_;_» : Lean.ParserDescr

Execute the prefix prf and proceed as the continuation pr.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.StatefulProcesses.«spProc_&_» : Lean.ParserDescr

Branching process: receives a selection label and continues accordingly.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.StatefulProcesses.spProcIf_Then_Else_ : Lean.ParserDescr

Conditional: evaluate e to choose between pr₁ and pr₂.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.StatefulProcesses.«term`(SP|_)» : Lean.ParserDescr

Processes.

Equations

• One or more equations did not get rendered due to their size.

Semantics

inductive Cslib.StatefulProcesses.Act (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)

Actions.

• assign {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} (x : Var) (e : Mech.Expr Var Val FunId) : Act Pid Var Val FunId SelLabel

  Assign to x the result of evaluating e.

• sendValue {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) : Act Pid Var Val FunId SelLabel

  Send to p the result of evaluating e.

• recvValue {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} (p : Pid) (x : Var) : Act Pid Var Val FunId SelLabel

  Receive a value from p and store it in variable x.

• sendLabel {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} (p : Pid) (l : SelLabel) : Act Pid Var Val FunId SelLabel

  Send to p the selection label l.

• recvLabel {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} (p : Pid) (l : SelLabel) : Act Pid Var Val FunId SelLabel

  Receive from p the selection label l.

• condThen {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} (e : Mech.Expr Var Val FunId) : Act Pid Var Val FunId SelLabel

  Choose the then-branch of a conditional guarded by e.

• condElse {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} (e : Mech.Expr Var Val FunId) : Act Pid Var Val FunId SelLabel

  Choose the else-branch of a conditional guarded by e.

def Cslib.StatefulProcesses.Act.isInternal {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} : Act Pid Var Val FunId SelLabel → Bool

An action is internal if it is not meant to interact with another process.

Equations

• (Cslib.StatefulProcesses.Act.assign x_1 e).isInternal = true
• (Cslib.StatefulProcesses.Act.condThen e).isInternal = true
• (Cslib.StatefulProcesses.Act.condElse e).isInternal = true
• x✝.isInternal = false

@[reducible, inline]

abbrev Cslib.StatefulProcesses.Prefix.toAct {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} : Prefix Pid Var Val FunId SelLabel → Act Pid Var Val FunId SelLabel

Transforms a Prefix into an Act.

Equations

• (Cslib.StatefulProcesses.Prefix.assign x_1 e).toAct = Cslib.StatefulProcesses.Act.assign x_1 e
• (Cslib.StatefulProcesses.Prefix.sendValue p e).toAct = Cslib.StatefulProcesses.Act.sendValue p e
• (Cslib.StatefulProcesses.Prefix.recvValue p x_1).toAct = Cslib.StatefulProcesses.Act.recvValue p x_1
• (Cslib.StatefulProcesses.Prefix.sendLabel p l).toAct = Cslib.StatefulProcesses.Act.sendLabel p l

inductive Cslib.StatefulProcesses.Process.Tr {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} : Process Pid Var Val FunId SelLabel ProcName → Act Pid Var Val FunId SelLabel → Process Pid Var Val FunId SelLabel ProcName → Prop

Symbolic transition relation for processes. Do not use this directly, use Process.lts instead.

• pre {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} {prf : Prefix Pid Var Val FunId SelLabel} {pr : Process Pid Var Val FunId SelLabel ProcName} : (Process.pre prf pr).Tr prf.toAct pr
• condThen {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} {e : Mech.Expr Var Val FunId} {pr₁ pr₂ : Process Pid Var Val FunId SelLabel ProcName} : (cond e pr₁ pr₂).Tr (Act.condThen e) pr₁
• condElse {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} {e : Mech.Expr Var Val FunId} {pr₁ pr₂ : Process Pid Var Val FunId SelLabel ProcName} : (cond e pr₁ pr₂).Tr (Act.condElse e) pr₂
• recvLabel {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} {branches : List (SelLabel × Process Pid Var Val FunId SelLabel ProcName)} {l : SelLabel} {pr : Process Pid Var Val FunId SelLabel ProcName} {p : Pid} (h : (l, pr) ∈ branches) : (Process.recvLabel p branches).Tr (Act.recvLabel p l) pr

def Cslib.StatefulProcesses.Process.lts {Pid : Type u_1} {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} {ProcName : Type u_6} : LTS (Process Pid Var Val FunId SelLabel ProcName) (Act Pid Var Val FunId SelLabel)

Symbolic LTS of processes.

Equations

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