Finite prefixes and infinite runs of dynamic concurrent processes

This file extends finite executions in the two directions needed for semantic reasoning about ongoing concurrent behavior.

• ProcessOver.Prefix is the right notion of a finite initial segment of an execution. Unlike ProcessOver.Trace, it may stop at any residual process state, not only at a quiescent one.
• ProcessOver.Run is an infinite execution, represented by the residual process state at each time index together with the complete transcript chosen for the corresponding process step.

The closed-world Process API is recovered as a specialization of these generic definitions.

inductive Interaction.Concurrent.ProcessOver.Prefix {Γ : Spec.Node.Context} (process : ProcessOver Γ) : process.Proc → ℕ → Type (max u_1 w)

Prefix process p n is a finite prefix of length n of an execution starting from the residual process state p.

Unlike ProcessOver.Trace, a Prefix may stop at any residual state. This makes it the correct finite prefix object for later infinite-run semantics.

Each step constructor records one complete sequential transcript of the current process step and then continues with a shorter prefix of the induced residual state.

• nil {Γ : Spec.Node.Context} {process : ProcessOver Γ} {p : process.Proc} : process.Prefix p 0

  The empty execution prefix.

• step {Γ : Spec.Node.Context} {process : ProcessOver Γ} {p : process.Proc} {n : ℕ} (tr : (process.step p).spec.Transcript) : process.Prefix ((process.step p).next tr) n → process.Prefix p n.succ

  Extend a finite prefix by one complete process step transcript.

def Interaction.Concurrent.ProcessOver.Prefix.currentControllers {Γ : Spec.Node.Context} {Party : Type u} {process : ProcessOver Γ} (resolve : Spec.Node.ContextHom Γ (StepContext Party)) {p : process.Proc} {n : ℕ} : process.Prefix p n → List (Option Party)

The sequence of current controlling parties exposed by a finite prefix after projecting the generic context into StepContext.

def Interaction.Concurrent.ProcessOver.Prefix.controllerPaths {Γ : Spec.Node.Context} {Party : Type u} {process : ProcessOver Γ} (resolve : Spec.Node.ContextHom Γ (StepContext Party)) {p : process.Proc} {n : ℕ} : process.Prefix p n → List (List Party)

The sequence of full controller paths exposed by a finite prefix after projecting the generic context into StepContext.

def Interaction.Concurrent.ProcessOver.Prefix.events {Γ : Spec.Node.Context} {process : ProcessOver Γ} {Event : Type w₃} (eventMap : process.EventMap Event) {p : process.Proc} {n : ℕ} : process.Prefix p n → List Event

The stable event labels attached to the executed steps of a finite prefix.

def Interaction.Concurrent.ProcessOver.Prefix.tickets {Γ : Spec.Node.Context} {process : ProcessOver Γ} {Ticket : Type w₃} (ticketMap : process.Tickets Ticket) {p : process.Proc} {n : ℕ} : process.Prefix p n → List Ticket

The stable tickets attached to the executed steps of a finite prefix.

def Interaction.Concurrent.ProcessOver.Prefix.ofTrace {Γ : Spec.Node.Context} {process : ProcessOver Γ} {p : process.Proc} (trace : process.Trace p) : process.Prefix p trace.length

Forget the quiescence proof of a finite Trace and keep only its executed prefix.

@[simp]

theorem Interaction.Concurrent.ProcessOver.Prefix.currentControllers_nil {Γ : Spec.Node.Context} {Party : Type u} {process : ProcessOver Γ} (resolve : Spec.Node.ContextHom Γ (StepContext Party)) {p : process.Proc} : currentControllers resolve nil = []

@[simp]

theorem Interaction.Concurrent.ProcessOver.Prefix.controllerPaths_nil {Γ : Spec.Node.Context} {Party : Type u} {process : ProcessOver Γ} (resolve : Spec.Node.ContextHom Γ (StepContext Party)) {p : process.Proc} : controllerPaths resolve nil = []

@[simp]

theorem Interaction.Concurrent.ProcessOver.Prefix.events_nil {Γ : Spec.Node.Context} {process : ProcessOver Γ} {Event : Type w₃} (eventMap : process.EventMap Event) {p : process.Proc} : events eventMap nil = []

@[simp]

theorem Interaction.Concurrent.ProcessOver.Prefix.tickets_nil {Γ : Spec.Node.Context} {process : ProcessOver Γ} {Ticket : Type w₃} (ticketMap : process.Tickets Ticket) {p : process.Proc} : tickets ticketMap nil = []

structure Interaction.Concurrent.ProcessOver.Run {Γ : Spec.Node.Context} (process : ProcessOver Γ) : Type (max u_1 w)

Run process is an infinite execution of the dynamic process process.

It is represented by:

• state n, the residual process state after n complete process steps;
• transcript n, the concrete transcript chosen for step n;
• next_state, which states that the residual state stream follows the process continuation exactly.

This is a continuation-based infinite semantics: the run does not introduce a new operational state space of its own. It simply records how the residual process state evolves when one complete process step is chosen at each time.

• state : ℕ → process.Proc
• transcript (n : ℕ) : (process.step (self.state n)).spec.Transcript
• next_state (n : ℕ) : self.state n.succ = (process.step (self.state n)).next (self.transcript n)

def Interaction.Concurrent.ProcessOver.Run.initial {Γ : Spec.Node.Context} {process : ProcessOver Γ} (run : process.Run) : process.Proc

The initial residual process state of a run.

def Interaction.Concurrent.ProcessOver.Run.head {Γ : Spec.Node.Context} {process : ProcessOver Γ} (run : process.Run) : (process.step run.initial).spec.Transcript

The first complete process-step transcript of the run.

def Interaction.Concurrent.ProcessOver.Run.tail {Γ : Spec.Node.Context} {process : ProcessOver Γ} (run : process.Run) : process.Run

The tail of a run after its first process step.

theorem Interaction.Concurrent.ProcessOver.Run.tail_initial {Γ : Spec.Node.Context} {process : ProcessOver Γ} (run : process.Run) : run.tail.initial = (process.step run.initial).next run.head

The initial state of run.tail is exactly the residual state obtained by executing run.head.

def Interaction.Concurrent.ProcessOver.Run.take {Γ : Spec.Node.Context} {process : ProcessOver Γ} (run : process.Run) (n : ℕ) : process.Prefix run.initial n

take run n is the length-n finite execution prefix of the infinite run run.

def Interaction.Concurrent.ProcessOver.Run.currentController? {Γ : Spec.Node.Context} {Party : Type u} {process : ProcessOver Γ} (resolve : Spec.Node.ContextHom Γ (StepContext Party)) (run : process.Run) (n : ℕ) : Option Party

The current controlling party of step n of a run, if any, after projecting the generic context into StepContext.

def Interaction.Concurrent.ProcessOver.Run.currentControllersUpTo {Γ : Spec.Node.Context} {Party : Type u} {process : ProcessOver Γ} (resolve : Spec.Node.ContextHom Γ (StepContext Party)) (run : process.Run) : ℕ → List (Option Party)

The current controlling parties exposed along the first n executed steps of the run run.

def Interaction.Concurrent.ProcessOver.Run.controllerPath {Γ : Spec.Node.Context} {Party : Type u} {process : ProcessOver Γ} (resolve : Spec.Node.ContextHom Γ (StepContext Party)) (run : process.Run) (n : ℕ) : List Party

The full controller path recorded by step n of a run after projecting the generic context into StepContext.

def Interaction.Concurrent.ProcessOver.Run.controllerPathsUpTo {Γ : Spec.Node.Context} {Party : Type u} {process : ProcessOver Γ} (resolve : Spec.Node.ContextHom Γ (StepContext Party)) (run : process.Run) : ℕ → List (List Party)

The full controller paths exposed along the first n executed steps of the run run.

def Interaction.Concurrent.ProcessOver.Run.event {Γ : Spec.Node.Context} {process : ProcessOver Γ} {Event : Type w₃} (eventMap : process.EventMap Event) (run : process.Run) (n : ℕ) : Event

The stable event label attached to step n of a run.

def Interaction.Concurrent.ProcessOver.Run.eventsUpTo {Γ : Spec.Node.Context} {process : ProcessOver Γ} {Event : Type w₃} (eventMap : process.EventMap Event) (run : process.Run) : ℕ → List Event

The stable event labels attached to the first n executed steps of the run run.

def Interaction.Concurrent.ProcessOver.Run.ticket {Γ : Spec.Node.Context} {process : ProcessOver Γ} {Ticket : Type w₃} (ticketMap : process.Tickets Ticket) (run : process.Run) (n : ℕ) : Ticket

The stable ticket attached to step n of a run.

def Interaction.Concurrent.ProcessOver.Run.ticketsUpTo {Γ : Spec.Node.Context} {process : ProcessOver Γ} {Ticket : Type w₃} (ticketMap : process.Tickets Ticket) (run : process.Run) : ℕ → List Ticket

The stable tickets attached to the first n executed steps of the run run.

def Interaction.Concurrent.ProcessOver.Run.RelUpTo {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {left : ProcessOver Γ} {right : ProcessOver Δ} (rel : left.TranscriptRel right) (leftRun : left.Run) (rightRun : right.Run) : ℕ → Prop

RelUpTo rel left right n states that the first n executed steps of the runs left and right match step-by-step according to rel.

def Interaction.Concurrent.ProcessOver.Run.Rel {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {left : ProcessOver Γ} {right : ProcessOver Δ} (rel : left.TranscriptRel right) (leftRun : left.Run) (rightRun : right.Run) : Prop

Rel rel left right states that every finite prefix of the runs left and right matches according to rel.

theorem Interaction.Concurrent.ProcessOver.Run.relUpTo_of_pointwise {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {left : ProcessOver Γ} {right : ProcessOver Δ} (rel : left.TranscriptRel right) (leftRun : left.Run) (rightRun : right.Run) (hrel : ∀ (n : ℕ), rel (leftRun.transcript n) (rightRun.transcript n)) (n : ℕ) : RelUpTo (fun {pL : left.Proc} {pR : right.Proc} => rel) leftRun rightRun n

Pointwise step matching implies prefix matching of the first n steps.

theorem Interaction.Concurrent.ProcessOver.Run.rel_of_pointwise {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {left : ProcessOver Γ} {right : ProcessOver Δ} (rel : left.TranscriptRel right) (leftRun : left.Run) (rightRun : right.Run) (hrel : ∀ (n : ℕ), rel (leftRun.transcript n) (rightRun.transcript n)) : Rel (fun {pL : left.Proc} {pR : right.Proc} => rel) leftRun rightRun

Pointwise step matching implies full run matching.

@[simp]

theorem Interaction.Concurrent.ProcessOver.Run.take_zero {Γ : Spec.Node.Context} {process : ProcessOver Γ} (run : process.Run) : run.take 0 = Prefix.nil

@[simp]

theorem Interaction.Concurrent.ProcessOver.Run.take_succ {Γ : Spec.Node.Context} {process : ProcessOver Γ} (run : process.Run) (n : ℕ) : run.take (n + 1) = Prefix.step run.head (⋯ ▸ run.tail.take n)

@[simp]

theorem Interaction.Concurrent.ProcessOver.Run.currentControllersUpTo_zero {Γ : Spec.Node.Context} {Party : Type u} {process : ProcessOver Γ} (resolve : Spec.Node.ContextHom Γ (StepContext Party)) (run : process.Run) : currentControllersUpTo resolve run 0 = []

@[simp]

theorem Interaction.Concurrent.ProcessOver.Run.controllerPathsUpTo_zero {Γ : Spec.Node.Context} {Party : Type u} {process : ProcessOver Γ} (resolve : Spec.Node.ContextHom Γ (StepContext Party)) (run : process.Run) : controllerPathsUpTo resolve run 0 = []

@[simp]

theorem Interaction.Concurrent.ProcessOver.Run.eventsUpTo_zero {Γ : Spec.Node.Context} {process : ProcessOver Γ} {Event : Type w₃} (eventMap : process.EventMap Event) (run : process.Run) : eventsUpTo eventMap run 0 = []

@[simp]

theorem Interaction.Concurrent.ProcessOver.Run.ticketsUpTo_zero {Γ : Spec.Node.Context} {process : ProcessOver Γ} {Ticket : Type w₃} (ticketMap : process.Tickets Ticket) (run : process.Run) : ticketsUpTo ticketMap run 0 = []

@[simp]

theorem Interaction.Concurrent.ProcessOver.Run.currentControllersUpTo_succ {Γ : Spec.Node.Context} {Party : Type u} {process : ProcessOver Γ} (resolve : Spec.Node.ContextHom Γ (StepContext Party)) (run : process.Run) (n : ℕ) : currentControllersUpTo resolve run (n + 1) = currentController? resolve run 0 :: currentControllersUpTo resolve run.tail n

@[simp]

theorem Interaction.Concurrent.ProcessOver.Run.controllerPathsUpTo_succ {Γ : Spec.Node.Context} {Party : Type u} {process : ProcessOver Γ} (resolve : Spec.Node.ContextHom Γ (StepContext Party)) (run : process.Run) (n : ℕ) : controllerPathsUpTo resolve run (n + 1) = controllerPath resolve run 0 :: controllerPathsUpTo resolve run.tail n

@[simp]

theorem Interaction.Concurrent.ProcessOver.Run.eventsUpTo_succ {Γ : Spec.Node.Context} {process : ProcessOver Γ} {Event : Type w₃} (eventMap : process.EventMap Event) (run : process.Run) (n : ℕ) : eventsUpTo eventMap run (n + 1) = event eventMap run 0 :: eventsUpTo eventMap run.tail n

@[simp]

theorem Interaction.Concurrent.ProcessOver.Run.ticketsUpTo_succ {Γ : Spec.Node.Context} {process : ProcessOver Γ} {Ticket : Type w₃} (ticketMap : process.Tickets Ticket) (run : process.Run) (n : ℕ) : ticketsUpTo ticketMap run (n + 1) = ticket ticketMap run 0 :: ticketsUpTo ticketMap run.tail n

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Prefix {Party : Type u} (process : Process Party) : process.Proc → ℕ → Type (max u_1 u_2)

The closed-world specialization of ProcessOver.Prefix.

def Interaction.Concurrent.Process.Prefix.currentControllers {Party : Type u} {process : Process Party} {p : process.Proc} {n : ℕ} : process.Prefix p n → List (Option Party)

The sequence of current controlling parties exposed by a finite closed-world prefix.

def Interaction.Concurrent.Process.Prefix.controllerPaths {Party : Type u} {process : Process Party} {p : process.Proc} {n : ℕ} : process.Prefix p n → List (List Party)

The sequence of full controller paths exposed by a finite closed-world prefix.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Prefix.events {Party : Type u} {process : Process Party} {Event : Type w₃} (eventMap : process.EventMap Event) {p : process.Proc} {n : ℕ} : process.Prefix p n → List Event

The stable event labels attached to the executed steps of a finite closed-world prefix.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Prefix.tickets {Party : Type u} {process : Process Party} {Ticket : Type w₃} (ticketMap : process.Tickets Ticket) {p : process.Proc} {n : ℕ} : process.Prefix p n → List Ticket

The stable tickets attached to the executed steps of a finite closed-world prefix.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Prefix.ofTrace {Party : Type u} {process : Process Party} {p : process.Proc} (trace : process.Trace p) : process.Prefix p trace.length

Forget the quiescence proof of a finite closed-world trace and keep only its executed prefix.

@[simp]

theorem Interaction.Concurrent.Process.Prefix.currentControllers_nil {Party : Type u} {process : Process Party} {p : process.Proc} : currentControllers ProcessOver.Prefix.nil = []

@[simp]

theorem Interaction.Concurrent.Process.Prefix.controllerPaths_nil {Party : Type u} {process : Process Party} {p : process.Proc} : controllerPaths ProcessOver.Prefix.nil = []

@[simp]

theorem Interaction.Concurrent.Process.Prefix.events_nil {Party : Type u} {process : Process Party} {Event : Type w₃} (eventMap : process.EventMap Event) {p : process.Proc} : events eventMap ProcessOver.Prefix.nil = []

@[simp]

theorem Interaction.Concurrent.Process.Prefix.tickets_nil {Party : Type u} {process : Process Party} {Ticket : Type w₃} (ticketMap : process.Tickets Ticket) {p : process.Proc} : tickets ticketMap ProcessOver.Prefix.nil = []

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run {Party : Type u} (process : Process Party) : Type (max u_1 u_2)

The closed-world specialization of ProcessOver.Run.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run.initial {Party : Type u} {process : Process Party} (run : process.Run) : process.Proc

The initial residual process state of a closed-world run.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run.head {Party : Type u} {process : Process Party} (run : process.Run) : (process.step run.initial).spec.Transcript

The first complete process-step transcript of a closed-world run.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run.tail {Party : Type u} {process : Process Party} (run : process.Run) : process.Run

The tail of a closed-world run after its first process step.

theorem Interaction.Concurrent.Process.Run.tail_initial {Party : Type u} {process : Process Party} (run : process.Run) : run.tail.initial = (process.step run.initial).next run.head

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run.take {Party : Type u} {process : Process Party} (run : process.Run) (n : ℕ) : process.Prefix run.initial n

The length-n finite prefix of a closed-world run.

def Interaction.Concurrent.Process.Run.currentController? {Party : Type u} {process : Process Party} (run : process.Run) (n : ℕ) : Option Party

The current controlling party of step n of a closed-world run, if any.

def Interaction.Concurrent.Process.Run.currentControllersUpTo {Party : Type u} {process : Process Party} (run : process.Run) : ℕ → List (Option Party)

The current controlling parties exposed along the first n executed steps of a closed-world run.

def Interaction.Concurrent.Process.Run.controllerPath {Party : Type u} {process : Process Party} (run : process.Run) (n : ℕ) : List Party

The full controller path recorded by step n of a closed-world run.

def Interaction.Concurrent.Process.Run.controllerPathsUpTo {Party : Type u} {process : Process Party} (run : process.Run) : ℕ → List (List Party)

The full controller paths exposed along the first n executed steps of a closed-world run.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run.event {Party : Type u} {process : Process Party} {Event : Type w₃} (eventMap : process.EventMap Event) (run : process.Run) (n : ℕ) : Event

The stable event label attached to step n of a closed-world run.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run.eventsUpTo {Party : Type u} {process : Process Party} {Event : Type w₃} (eventMap : process.EventMap Event) (run : process.Run) : ℕ → List Event

The stable event labels attached to the first n executed steps of a closed-world run.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run.ticket {Party : Type u} {process : Process Party} {Ticket : Type w₃} (ticketMap : process.Tickets Ticket) (run : process.Run) (n : ℕ) : Ticket

The stable ticket attached to step n of a closed-world run.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run.ticketsUpTo {Party : Type u} {process : Process Party} {Ticket : Type w₃} (ticketMap : process.Tickets Ticket) (run : process.Run) : ℕ → List Ticket

The stable tickets attached to the first n executed steps of a closed-world run.

@[simp]

theorem Interaction.Concurrent.Process.Run.take_zero {Party : Type u} {process : Process Party} (run : process.Run) : run.take 0 = ProcessOver.Prefix.nil

@[simp]

theorem Interaction.Concurrent.Process.Run.take_succ {Party : Type u} {process : Process Party} (run : process.Run) (n : ℕ) : run.take (n + 1) = ProcessOver.Prefix.step run.head (⋯ ▸ run.tail.take n)

@[simp]

theorem Interaction.Concurrent.Process.Run.currentControllersUpTo_zero {Party : Type u} {process : Process Party} (run : process.Run) : run.currentControllersUpTo 0 = []

@[simp]

theorem Interaction.Concurrent.Process.Run.controllerPathsUpTo_zero {Party : Type u} {process : Process Party} (run : process.Run) : run.controllerPathsUpTo 0 = []

@[simp]

theorem Interaction.Concurrent.Process.Run.eventsUpTo_zero {Party : Type u} {process : Process Party} {Event : Type w₃} (eventMap : process.EventMap Event) (run : process.Run) : eventsUpTo eventMap run 0 = []

@[simp]

theorem Interaction.Concurrent.Process.Run.ticketsUpTo_zero {Party : Type u} {process : Process Party} {Ticket : Type w₃} (ticketMap : process.Tickets Ticket) (run : process.Run) : ticketsUpTo ticketMap run 0 = []

@[simp]

theorem Interaction.Concurrent.Process.Run.currentControllersUpTo_succ {Party : Type u} {process : Process Party} (run : process.Run) (n : ℕ) : run.currentControllersUpTo (n + 1) = run.currentController? 0 :: run.tail.currentControllersUpTo n

@[simp]

theorem Interaction.Concurrent.Process.Run.controllerPathsUpTo_succ {Party : Type u} {process : Process Party} (run : process.Run) (n : ℕ) : run.controllerPathsUpTo (n + 1) = run.controllerPath 0 :: run.tail.controllerPathsUpTo n

@[simp]

theorem Interaction.Concurrent.Process.Run.eventsUpTo_succ {Party : Type u} {process : Process Party} {Event : Type w₃} (eventMap : process.EventMap Event) (run : process.Run) (n : ℕ) : eventsUpTo eventMap run (n + 1) = event eventMap run 0 :: eventsUpTo eventMap run.tail n

@[simp]

theorem Interaction.Concurrent.Process.Run.ticketsUpTo_succ {Party : Type u} {process : Process Party} {Ticket : Type w₃} (ticketMap : process.Tickets Ticket) (run : process.Run) (n : ℕ) : ticketsUpTo ticketMap run (n + 1) = ticket ticketMap run 0 :: ticketsUpTo ticketMap run.tail n