Concurrent interaction specifications

This file introduces the minimal concurrent source syntax for the Interaction library.

The existing sequential Interaction.Spec is a continuation tree with one currently enabled move family at each node. The concurrent extension keeps that continuation-first shape and adds exactly one new constructor:

• par left right — both left and right are concurrently live.

The design is intentionally syntax-first and minimal. This file does not yet define:

• the currently enabled frontier of a concurrent spec;
• scheduler or adversary execution;
• independence or true-concurrency refinements;
• dynamic spawning;
• or multiparty local observations of concurrent events.

Those layers live in later modules such as Concurrent/Frontier and Concurrent/Trace.

The guiding idea is the same as in the sequential layer: the "state" of a concurrent interaction is its current residual continuation, not an external mutable store.

inductive Interaction.Concurrent.Spec : Type (u + 1)

A Concurrent.Spec describes the shape of a concurrent interaction as a continuation tree with binary structural parallelism.

Constructors:

• done — no further behavior.
• node Moves rest — one currently enabled atomic move family, just as in the sequential Interaction.Spec.
• par left right — both left and right are concurrently live.

This is intentionally only a source syntax for concurrency. It says that residual behavior can be built from sequential nodes and parallel composition, but it does not yet commit to any particular execution semantics or equivalence laws.

• done : Spec

  Terminal concurrent interaction: no further events are enabled.

• node (Moves : Type u) (rest : Moves → Spec) : Spec

  One atomic interaction node, exactly as in the sequential setting: a move x : Moves occurs, and the residual concurrent interaction is rest x.

• par (left right : Spec) : Spec

  Parallel composition of two concurrently live residual interactions.

def Interaction.Concurrent.Spec.isLive : Spec → Bool

isLive S decides whether the concurrent spec S still exposes any enabled frontier event.

This is the structural liveness test for the concurrent source syntax:

• done is not live;
• an atomic node is live;
• a parallel spec is live iff either side is live.

Unlike syntactic equality with .done, this detects quiescent residuals such as .par .done .done, which expose no frontier events even though they are not literally the terminal constructor.

def Interaction.Concurrent.Spec.ofSequential : Interaction.Spec → Spec

Embed a sequential Interaction.Spec into the concurrent syntax as the one-thread fragment with no use of par.

This is the basic bridge from the existing sequential library to the new concurrent source language.

@[simp]

theorem Interaction.Concurrent.Spec.ofSequential_done : ofSequential Interaction.Spec.done = done

@[simp]

theorem Interaction.Concurrent.Spec.ofSequential_node (Moves : Type u) (rest : Moves → Interaction.Spec) : ofSequential (Interaction.Spec.node Moves rest) = node Moves fun (x : Moves) => ofSequential (rest x)

@[simp]

theorem Interaction.Concurrent.Spec.isLive_done : done.isLive = false

@[simp]

theorem Interaction.Concurrent.Spec.isLive_node (Moves : Type u) (rest : Moves → Spec) : (node Moves rest).isLive = true

@[simp]

theorem Interaction.Concurrent.Spec.isLive_par (left right : Spec) : (left.par right).isLive = (left.isLive || right.isLive)