Finite executions of dynamic concurrent processes

This file explains what it means to execute a Concurrent.ProcessOver for finitely many steps.

The important point is that one process step is itself a finite sequential interaction episode. So a finite concurrent execution is not just a list of atomic labels: at each residual state we record one complete sequential transcript of the current step, then continue from the residual process state selected by that transcript.

This file therefore provides two parallel views of finite execution:

• ProcessOver.Trace, the exact global execution history for any realized node context; and
• Step.Observed / ProcessOver.ObservedTrace, the local observations that one fixed party extracts from that history once the node context is projected into StepContext.

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

inductive Interaction.Concurrent.Step.Observed {Party : Type u} [DecidableEq Party] (me : Party) {spec : Spec} : Spec.Decoration (StepContext Party) spec → spec.Transcript → Type (max u (w + 1))

Observed me semantics tr is the exact typed sequence of local observations available to the fixed party me during one sequential step.

More concretely, suppose the current process step executes along transcript tr. At each visited node of that transcript, the step semantics determines what me is allowed to observe there, and Observed records exactly that piece of local information before continuing to the next node.

So Observed is the step-local projection of the global transcript: it forgets everything that me is not entitled to see, while preserving the exact local observation type at every node.

• done {Party : Type u} [DecidableEq Party] {me : Party} : Observed me PUnit.unit PUnit.unit

  The unique observed transcript of a completed sequential step.

• step {Party : Type u} [DecidableEq Party] {me : Party} {Moves : Type w} {rest : Moves → Spec} {node : NodeSemantics Party Moves} {semantics : (x : Moves) → Spec.Decoration (StepContext Party) (rest x)} {x : Moves} {tail : (rest x).Transcript} (obs : (node.views me).ObsType) (restObs : Observed me (semantics x) tail) : Observed me (have this := (node, semantics); this) (have this := ⟨x, tail⟩; this)

  Extend an observed transcript by the local observation available at the current node.

def Interaction.Concurrent.Step.Observed.length {Party : Type u} [DecidableEq Party] {me : Party} {spec : Spec} {semantics : Spec.Decoration (StepContext Party) spec} {tr : spec.Transcript} : Observed me semantics tr → ℕ

The number of visited nodes recorded by an observed sequential transcript.

def Interaction.Concurrent.Step.Observed.ofTranscript {Party : Type u} [DecidableEq Party] (me : Party) {spec : Spec} (semantics : Spec.Decoration (StepContext Party) spec) (tr : spec.Transcript) : Observed me semantics tr

ofTranscript me semantics tr is the canonical observed sequential transcript induced by the concrete global transcript tr.

It is obtained by replaying tr and, at each visited node, extracting the observation that the local view for me exposes there.

@[reducible, inline]

abbrev Interaction.Concurrent.Step.ObservedTranscript {Party : Type u} [DecidableEq Party] (me : Party) {P : Type v} (step : Step Party P) (tr : step.spec.Transcript) : Type (max u (u_1 + 1))

Observed me step tr is the sequence of local observations exposed to me while the step step executes along the transcript tr.

This is the most convenient step-level type when working with concrete process steps rather than raw decorations.

@[reducible, inline]

abbrev Interaction.Concurrent.Step.observe {Party : Type u} [DecidableEq Party] (me : Party) {P : Type v} (step : Step Party P) (tr : step.spec.Transcript) : ObservedTranscript me step tr

observe me step tr is the canonical observed sequential transcript induced by running step along tr.

@[reducible, inline]

abbrev Interaction.Concurrent.StepOver.ObservedTranscript {Γ : Spec.Node.Context} {Party : Type u} [DecidableEq Party] (me : Party) (resolve : Spec.Node.ContextHom Γ (StepContext Party)) {P : Type v} (step : StepOver Γ P) (tr : step.spec.Transcript) : Type (max u (w + 1))

ObservedTranscript me resolve step tr is the local observation sequence seen by me when the generic step step is interpreted through the context projection resolve : Γ → StepContext Party.

@[reducible, inline]

abbrev Interaction.Concurrent.StepOver.observe {Γ : Spec.Node.Context} {Party : Type u} [DecidableEq Party] (me : Party) (resolve : Spec.Node.ContextHom Γ (StepContext Party)) {P : Type v} (step : StepOver Γ P) (tr : step.spec.Transcript) : ObservedTranscript me resolve step tr

observe me resolve step tr is the canonical observed sequential transcript of step along tr, after projecting the generic step context into StepContext.

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

Trace process p is a finite execution trace of the residual process state p.

Each step constructor records one whole sequential transcript for the current process step, then continues with the residual process selected by that transcript. The done constructor is available only when the current step has no complete transcripts at all, so a Trace represents a genuinely terminated finite execution.

ProcessOver.Trace is therefore the generic finite-history object for the dynamic concurrent core: one element per process step, where each element remembers the entire internal interaction episode that realized that step.

• done {Γ : Spec.Node.Context} {process : ProcessOver Γ} {p : process.Proc} : (∀ (a : (process.step p).spec.Transcript), False) → process.Trace p

  A finished execution of a residual process state whose current step has no complete transcripts.

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

  Execute one complete sequential step transcript and continue with the residual process state induced by that transcript.

def Interaction.Concurrent.ProcessOver.Trace.length {Γ : Spec.Node.Context} {process : ProcessOver Γ} {p : process.Proc} : process.Trace p → ℕ

The number of process steps recorded by a finite execution trace.

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

currentControllers resolve trace records the current controlling party of each executed process step after projecting the generic step context into StepContext.

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

controllerPaths resolve trace records the full controller path of each executed process step after projecting the generic step context into StepContext.

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

events eventMap trace records the external event label attached to each process step transcript by the stable event map eventMap.

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

tickets ticketMap trace records the stable tickets attached to each process step transcript by ticketMap.

@[simp]

theorem Interaction.Concurrent.ProcessOver.Trace.length_done {Γ : Spec.Node.Context} {process : ProcessOver Γ} {p : process.Proc} (h : ∀ (a : (process.step p).spec.Transcript), False) : (done h).length = 0

@[simp]

theorem Interaction.Concurrent.ProcessOver.Trace.length_step {Γ : Spec.Node.Context} {process : ProcessOver Γ} {p : process.Proc} (tr : (process.step p).spec.Transcript) (tail : process.Trace ((process.step p).next tr)) : (step tr tail).length = tail.length.succ

inductive Interaction.Concurrent.ProcessOver.ObservedTrace {Γ : Spec.Node.Context} {Party : Type u} [DecidableEq Party] (me : Party) (resolve : Spec.Node.ContextHom Γ (StepContext Party)) (process : ProcessOver Γ) {p : process.Proc} : process.Trace p → Type (max (max u u_1) (w + 1))

ObservedTrace me resolve process trace is the exact typed sequence of local observations available to me along the concrete process execution trace, after interpreting the generic node context through resolve.

• done {Γ : Spec.Node.Context} {Party : Type u} [DecidableEq Party] {me : Party} {resolve : Spec.Node.ContextHom Γ (StepContext Party)} {process : ProcessOver Γ} {p : process.Proc} {h : ∀ (a : (process.step p).spec.Transcript), False} : ObservedTrace me resolve process (Trace.done h)

  The unique observed trace of a finished quiescent execution.

• step {Γ : Spec.Node.Context} {Party : Type u} [DecidableEq Party] {me : Party} {resolve : Spec.Node.ContextHom Γ (StepContext Party)} {process : ProcessOver Γ} {p : process.Proc} {tr : (process.step p).spec.Transcript} {tail : process.Trace ((process.step p).next tr)} (obs : StepOver.ObservedTranscript me resolve (process.step p) tr) (rest : ObservedTrace me resolve process tail) : ObservedTrace me resolve process (Trace.step tr tail)

  Extend an observed trace by the observed sequential transcript of the current step.

def Interaction.Concurrent.ProcessOver.ObservedTrace.length {Γ : Spec.Node.Context} {Party : Type u} [DecidableEq Party] {me : Party} {resolve : Spec.Node.ContextHom Γ (StepContext Party)} {process : ProcessOver Γ} {p : process.Proc} {trace : process.Trace p} : ObservedTrace me resolve process trace → ℕ

The number of process steps recorded by an observed trace.

def Interaction.Concurrent.ProcessOver.ObservedTrace.ofTrace {Γ : Spec.Node.Context} {Party : Type u} [DecidableEq Party] (me : Party) (resolve : Spec.Node.ContextHom Γ (StepContext Party)) (process : ProcessOver Γ) {p : process.Proc} (trace : process.Trace p) : ObservedTrace me resolve process trace

ofTrace me resolve process trace is the canonical observed process trace induced by the concrete execution trace trace.

@[simp]

theorem Interaction.Concurrent.ProcessOver.ObservedTrace.length_done {Γ : Spec.Node.Context} {Party : Type u} [DecidableEq Party] {me : Party} {resolve : Spec.Node.ContextHom Γ (StepContext Party)} {process : ProcessOver Γ} {p : process.Proc} {h : ∀ (a : (process.step p).spec.Transcript), False} : done.length = 0

@[simp]

theorem Interaction.Concurrent.ProcessOver.ObservedTrace.length_step {Γ : Spec.Node.Context} {Party : Type u} [DecidableEq Party] {me : Party} {resolve : Spec.Node.ContextHom Γ (StepContext Party)} {process : ProcessOver Γ} {p : process.Proc} {tr : (process.step p).spec.Transcript} {tail : process.Trace ((process.step p).next tr)} (obs : StepOver.ObservedTranscript me resolve (process.step p) tr) (rest : ObservedTrace me resolve process tail) : (step obs rest).length = rest.length.succ

theorem Interaction.Concurrent.ProcessOver.ObservedTrace.length_ofTrace {Γ : Spec.Node.Context} {Party : Type u} [DecidableEq Party] {me : Party} (resolve : Spec.Node.ContextHom Γ (StepContext Party)) (process : ProcessOver Γ) {p : process.Proc} (trace : process.Trace p) : (ofTrace me resolve process trace).length = trace.length

The canonical observed process trace has the same number of process steps as the underlying execution trace.

@[reducible, inline]

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

The closed-world specialization of ProcessOver.Trace.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Trace.length {Party : Type u} {process : Process Party} {p : process.Proc} : process.Trace p → ℕ

The number of process steps recorded by a finite closed-world execution trace.

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

The current controlling party of each executed step of a closed-world trace.

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

The full controller path of each executed step of a closed-world trace.

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[simp]

theorem Interaction.Concurrent.Process.Trace.length_done {Party : Type u} {process : Process Party} {p : process.Proc} (h : ∀ (a : (process.step p).spec.Transcript), False) : length (ProcessOver.Trace.done h) = 0

@[simp]

theorem Interaction.Concurrent.Process.Trace.length_step {Party : Type u} {process : Process Party} {p : process.Proc} (tr : (process.step p).spec.Transcript) (tail : process.Trace ((process.step p).next tr)) : length (ProcessOver.Trace.step tr tail) = tail.length.succ

@[reducible, inline]

abbrev Interaction.Concurrent.Process.ObservedTrace {Party : Type u} [DecidableEq Party] (me : Party) (process : Process Party) {p : process.Proc} : process.Trace p → Type (max (max u (u_2 + 1)) u_1)

The closed-world specialization of ProcessOver.ObservedTrace.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.ObservedTrace.length {Party : Type u} [DecidableEq Party] {me : Party} {process : Process Party} {p : process.Proc} {trace : process.Trace p} : ObservedTrace me process trace → ℕ

The number of process steps recorded by an observed closed-world trace.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.ObservedTrace.ofTrace {Party : Type u} [DecidableEq Party] (me : Party) (process : Process Party) {p : process.Proc} (trace : process.Trace p) : ObservedTrace me process trace

ofTrace me process trace is the canonical observed closed-world process trace induced by the concrete execution trace trace.

@[simp]

theorem Interaction.Concurrent.Process.ObservedTrace.length_done {Party : Type u} [DecidableEq Party] {me : Party} {process : Process Party} {p : process.Proc} {h : ∀ (a : (process.step p).spec.Transcript), False} : length ProcessOver.ObservedTrace.done = 0

@[simp]

theorem Interaction.Concurrent.Process.ObservedTrace.length_step {Party : Type u} [DecidableEq Party] {me : Party} {process : Process Party} {p : process.Proc} {tr : (process.step p).spec.Transcript} {tail : process.Trace ((process.step p).next tr)} (obs : StepOver.ObservedTranscript me (Spec.Node.ContextHom.id (StepContext Party)) (process.step p) tr) (rest : ObservedTrace me process tail) : length (ProcessOver.ObservedTrace.step obs rest) = rest.length.succ

theorem Interaction.Concurrent.Process.ObservedTrace.length_ofTrace {Party : Type u} [DecidableEq Party] {me : Party} (process : Process Party) {p : process.Proc} (trace : process.Trace p) : (ofTrace me process trace).length = trace.length

The canonical observed closed-world trace has the same number of process steps as the underlying execution trace.