Scheduler and control ownership for concurrent interaction

This file adds an explicit control layer on top of the concurrent source syntax.

The key distinction is:

• at an atomic node, some party controls the payload move itself;
• at a parallel par left right, some party may control the scheduling choice of which currently live side fires next.

So a full frontier event may be controlled by several parties in sequence: a scheduler may first choose a live branch of par, and then a downstream node owner may choose the payload move of the selected atomic node.

The purpose of this file is to represent that control structure directly and definitionally.

Main definitions:

• Control Party S — structural control metadata for the concurrent spec S;
• Control.residual — transport control metadata across one scheduled frontier event;
• Control.isLive — whether a control tree still exposes enabled frontier events;
• Control.scheduler? — the party who currently has a genuine scheduling choice between two live concurrent components, if any;
• Control.current? — the party who currently controls the next decision, whether that is a scheduler choice or an atomic payload choice;
• Control.controllers — the full control path of a concrete frontier event.

This is intentionally a control/ownership layer only. It does not yet prescribe how those parties compute their choices or how local endpoint programs should be assembled from that ownership data.

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

Control Party S records who controls the next decision at each structural position of the concurrent spec S.

Constructors mirror the concurrent syntax:

• done — there are no further decisions to control;
• node owner cont — at an atomic node, owner controls the move payload, and cont x records the residual control tree after choosing x;
• par scheduler left right — at a parallel node, scheduler controls the choice between the two concurrently live components left and right.

This is not a local-view or observation object. It records only control.

• done {Party : Type u} : Control Party Spec.done

  Control tree for a terminated concurrent spec.

• node {Party Moves : Type u} {rest : Moves → Spec} (owner : Party) (cont : (x : Moves) → Control Party (rest x)) : Control Party (Spec.node Moves rest)

  Control tree for an atomic node: owner controls the move payload, and the continuation records residual control after that move.

• par {Party : Type u} {left right : Spec} (scheduler : Party) (leftControl : Control Party left) (rightControl : Control Party right) : Control Party (left.par right)

  Control tree for a parallel spec: scheduler controls the choice of which live side fires next while both sides remain live.

def Interaction.Concurrent.Control.residual {Party : Type u} {S : Spec} : Control Party S → (event : Front S) → Control Party (Concurrent.residual event)

residual control event is the control tree remaining after scheduling the frontier event event.

This mirrors the residual concurrent spec structurally:

• atomic node control follows the chosen payload branch;
• parallel control updates only the side from which the event came.

def Interaction.Concurrent.Control.isLive {Party : Type u} {S : Spec} : Control Party S → Bool

isLive control decides whether the control tree control still exposes any enabled frontier event.

This is the control-side analogue of asking whether the indexed frontier type is empty:

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

def Interaction.Concurrent.Control.scheduler? {Party : Type u} {S : Spec} : Control Party S → Option Party

scheduler? control returns the party who currently has a genuine scheduling choice between two live concurrent components.

This returns:

• some scheduler at a par node exactly when both sides are live;
• none otherwise.

So this records frontier scheduling ownership, not payload ownership.

def Interaction.Concurrent.Control.current? {Party : Type u} {S : Spec} : Control Party S → Option Party

current? control returns the party who currently controls the next decision.

This may be:

• a scheduler at a par node when both sides are live;
• otherwise, the controlling party of the unique live side;
• or the owner of an atomic node.

So current? collapses scheduler choice and payload choice into the one party who is currently in control of progress.

def Interaction.Concurrent.Control.controllers {Party : Type u} {S : Spec} : Control Party S → (event : Front S) → List Party

controllers control event is the full control path of the concrete frontier event event.

For an atomic node, this is the singleton list containing the node owner. For a parallel node:

• if the opposite side is also live, the scheduler is prepended;
• if the chosen side is the only live side, the scheduler does not appear, because there is no genuine scheduling choice to make.

This distinction matters after residual steps such as .par .done right, where control should immediately collapse to the right subtree rather than crediting a vacuous scheduler choice.

@[simp]

theorem Interaction.Concurrent.Control.isLive_done {Party : Type u} : done.isLive = false

@[simp]

theorem Interaction.Concurrent.Control.isLive_node {Party Moves : Type u} {rest : Moves → Spec} (owner : Party) (cont : (x : Moves) → Control Party (rest x)) : (node owner cont).isLive = true

@[simp]

theorem Interaction.Concurrent.Control.scheduler?_node {Party Moves : Type u} {rest : Moves → Spec} (owner : Party) (cont : (x : Moves) → Control Party (rest x)) : (node owner cont).scheduler? = none

@[simp]

theorem Interaction.Concurrent.Control.current?_node {Party Moves : Type u} {rest : Moves → Spec} (owner : Party) (cont : (x : Moves) → Control Party (rest x)) : (node owner cont).current? = some owner

@[simp]

theorem Interaction.Concurrent.Control.controllers_move {Party Moves : Type u} {rest : Moves → Spec} (owner : Party) (cont : (x : Moves) → Control Party (rest x)) (x : Moves) : (node owner cont).controllers (Front.move x) = [owner]