Choreography

A choreography defines the collective behaviour of a system of communicating participants (processes) [Mon23].

Limitations

Some notable features not yet included:

• Recursion (only the syntax is implemented, but no semantics).
• General recursion (the current syntax supports only tail recursion).
• Choreographic choice (for barriers, first-come/first-served patterns, etc.).
• Asynchronous communication.

References

• F. Montesi, Introduction to Choreographies

Syntax of choreographies

inductive Cslib.Languages.Mech.Expr (Var : Type u_1) (Val : Type u_2) (FunId : Type u_3) : Type (max (max u_1 u_2) u_3)

Expressions for local computation.

• var {Var : Type u_1} {Val : Type u_2} {FunId : Type u_3} (x : Var) : Expr Var Val FunId

  Read variable x.

• val {Var : Type u_1} {Val : Type u_2} {FunId : Type u_3} (v : Val) : Expr Var Val FunId

  Value v.

• call {Var : Type u_1} {Val : Type u_2} {FunId : Type u_3} (f : FunId) (args : List (Expr Var Val FunId)) : Expr Var Val FunId

  Call function f with arguments args.

@[instance_reducible]

instance Cslib.Languages.Mech.instCoeExpr {Var : Type u_1} {Val : Type u_2} {FunId : Type u_3} : Coe Var (Expr Var Val FunId)

Utility instance to write variables directly as expressions.

Equations

• Cslib.Languages.Mech.instCoeExpr = { coe := fun (x : Var) => Cslib.Languages.Mech.Expr.var x }

@[instance_reducible]

instance Cslib.Languages.Mech.instCoeExpr_1 {Val : Type u_1} {Var : Type u_2} {FunId : Type u_3} : Coe Val (Expr Var Val FunId)

Utility instance to write values directly as expressions.

Equations

• Cslib.Languages.Mech.instCoeExpr_1 = { coe := fun (v : Val) => Cslib.Languages.Mech.Expr.val v }

inductive Cslib.Languages.Mech.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)

Choreographic prefix.

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

  p assigns x the value computed from e.

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

  p communicates the evaluation of e to q, which stores it in its variable x.

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

  p communicates the selection label (a static tag used to denote a choice) to q.

inductive Cslib.Languages.Mech.Choreography (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)

Choreographies.

• 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} : Choreography Pid Var Val FunId SelLabel ProcName

  The terminated choreography.

• 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) (c : Choreography Pid Var Val FunId SelLabel ProcName) : Choreography Pid Var Val FunId SelLabel ProcName

  Do prf and continue as c.

• 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} (p : Pid) (e : Expr Var Val FunId) (c₁ c₂ : Choreography Pid Var Val FunId SelLabel ProcName) : Choreography Pid Var Val FunId SelLabel ProcName

  Conditional: p evaluates e to choose between c₁ and c₂.

• 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) : Choreography Pid Var Val FunId SelLabel ProcName

  Call the procedure proc.

@[instance_reducible]

instance Cslib.Languages.Mech.instZeroChoreography {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 (Choreography Pid Var Val FunId SelLabel ProcName)

Equations

• Cslib.Languages.Mech.instZeroChoreography = { zero := Cslib.Languages.Mech.Choreography.nil }

def Lean.Parser.Category.mechPre : Category

Syntactic category for prefixes.

Equations

• Lean.Parser.Category.mechPre = { }

def Cslib.Languages.Mech.mechPre.quot : Lean.ParserDescr

Equations

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

def Cslib.Languages.Mech.«mechPre_._≔_» : Lean.ParserDescr

p assigns x the value computed from e.

Equations

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

def Cslib.Languages.Mech.«mechPre_._⮕_._» : Lean.ParserDescr

p communicates the evaluation of e to q, which stores it in its variable x.

Equations

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

def Cslib.Languages.Mech.«mechPre_⮕_[_]» : Lean.ParserDescr

p communicates the selection label (a static tag used to denote a choice) to q.

Equations

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

def Cslib.Languages.Mech.«term`(MechPre|_)» : Lean.ParserDescr

Choreographic prefix.

Equations

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

def Cslib.Languages.Mech.mechChor.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.mechChor : Category

Syntactic category for choreographies.

Equations

• Lean.Parser.Category.mechChor = { }

def Cslib.Languages.Mech.mechChor_ : Lean.ParserDescr

The terminated choreography.

Equations

• Cslib.Languages.Mech.mechChor_ = Lean.ParserDescr.node `Cslib.Languages.Mech.mechChor_ 1022 (Lean.ParserDescr.const `num)

def Cslib.Languages.Mech.«mechChor_;_» : Lean.ParserDescr

Do prf and continue as c.

Equations

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

def Cslib.Languages.Mech.«mechChorIf_._Then_Else_» : Lean.ParserDescr

Conditional: p evaluates e to choose between c₁ and c₂.

Equations

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

def Cslib.Languages.Mech.«term`(Mech|_)» : Lean.ParserDescr

Choreographies.

Equations

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

def Cslib.Languages.Mech.Prefix.pn {Pid : Type u_1} [DecidableEq Pid] {Var : Type u_2} {Val : Type u_3} {FunId : Type u_4} {SelLabel : Type u_5} : Prefix Pid Var Val FunId SelLabel → Finset Pid

Process names in a prefix.

Equations

• (Cslib.Languages.Mech.Prefix.assign p x_1 e).pn = {p}
• (Cslib.Languages.Mech.Prefix.com p e q x_1).pn = {p, q}
• (Cslib.Languages.Mech.Prefix.sel p q l).pn = {p, q}

def Cslib.Languages.Mech.Choreography.pn {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} : Choreography Pid Var Val FunId SelLabel ProcName → Finset Pid

Process names in a choreography.

Equations

• Cslib.Languages.Mech.Choreography.nil.pn = ∅
• (Cslib.Languages.Mech.Choreography.pre prf c).pn = prf.pn ∪ c.pn
• (Cslib.Languages.Mech.Choreography.cond p e c₁ c₂).pn = {p} ∪ c₁.pn ∪ c₂.pn
• (Cslib.Languages.Mech.Choreography.call proc args).pn = args.toFinset