Frontiers and residual concurrent interaction

This file gives the primary scheduler-facing execution view of Interaction.Concurrent.Spec.

The foundational concurrent syntax is structural: sequential nodes plus binary par. For execution, the important questions are instead:

• what events are currently enabled?
• and what residual interaction remains after choosing one of them?

Those questions are answered by:

• Front S — the type of currently enabled frontier events of S;
• residual — the residual concurrent spec after one frontier event.

The definition of Front is intentionally an inductive family, not a recursive alias into PEmpty and Sum. This keeps the scheduler-facing API close to the source syntax and preserves direct pattern matching and definitional computation for residual.

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

Front S is the type of currently enabled frontier events of the concurrent spec S.

Reading by cases:

• Front .done has no constructors, since no further events are enabled;
• Front (.node X rest) is a chosen move x : X;
• Front (.par left right) is an event from the left or right concurrent component.

The inductive-family presentation keeps the scheduler-facing interface definitionally close to the structural source syntax.

• move {Moves : Type u} {rest : Moves → Spec} (x : Moves) : Front (Spec.node Moves rest)

  A frontier event of an atomic node is simply one chosen move.

• left {left right : Spec} (event : Front left) : Front (left.par right)

  Lift a frontier event from the left component of a parallel spec.

• right {left right : Spec} (event : Front right) : Front (left.par right)

  Lift a frontier event from the right component of a parallel spec.

def Interaction.Concurrent.residual {S : Spec} : Front S → Spec

residual event is the residual concurrent spec after performing one frontier event event.

The equations are definitionally the expected ones:

• a move at an atomic node continues with that node's continuation;
• a left frontier event updates only the left component of a parallel node;
• a right frontier event updates only the right component.

This is the primary execution primitive for schedulers, adversaries, and traces.

theorem Interaction.Concurrent.isEmpty_of_not_live {S : Spec} : S.isLive = false → ∀ (a✝ : Front S), False

If a concurrent spec is not live, then its frontier type is empty.

This packages the structural fact that Spec.isLive exactly decides whether a concurrent spec still exposes enabled frontier events.

@[simp]

theorem Interaction.Concurrent.residual_move {Moves : Type u} {rest : Moves → Spec} (x : Moves) : residual (Front.move x) = rest x

@[simp]

theorem Interaction.Concurrent.residual_left {left right : Spec} (event : Front left) : residual event.left = (residual event).par right

@[simp]

theorem Interaction.Concurrent.residual_right {left right : Spec} (event : Front right) : residual event.right = left.par (residual event)