Current local views of concurrent frontier events

This file combines the two structural concurrent layers:

• Concurrent.Control, which records who currently controls scheduling and payload choices;
• Concurrent.Profile, which records what each party can locally observe from concrete frontier events.

From those ingredients, it computes the current local view of the next frontier event for a fixed party.

This is the key conceptual bridge:

• if the fixed party currently controls the next decision, its current local view is active;
• otherwise, its current local view is the observation view induced by the current frontier profile.

At a par node, this means:

• when both sides are live, the scheduler's local view is active on the full frontier event type Front S;
• when only one side remains live, control collapses to that side's own current controller and local view.

So this file gives the first true "who chooses what next, and what does everyone else learn?" interface for the concurrent layer.

@[reducible, inline]

abbrev Interaction.Concurrent.Current.controller? {Party : Type u} {S : Spec} (control : Control Party S) : Option Party

The party currently controlling the next decision in the concurrent control tree. This is just Control.current?, re-exported here because the present module treats Control and Profile together as the current-step interface.

@[reducible, inline]

abbrev Interaction.Concurrent.Current.scheduler? {Party : Type u} {S : Spec} (control : Control Party S) : Option Party

The party currently controlling a genuine scheduling choice between two live concurrent components, when such a choice exists. This is just Control.scheduler?, re-exported here for the combined current-step interface.

def Interaction.Concurrent.Current.view {Party : Type u} [DecidableEq Party] (me : Party) {S : Spec} : Control Party S → Profile Party S → Multiparty.LocalView (Front S)

view me control profile is the current local view of the next frontier event for the fixed party me.

It is computed from both control and observation structure:

• at an atomic node, the owner recorded by control gets active, while every other party gets the frontier observation induced by profile;
• at a parallel node with two live sides, the scheduler recorded by control gets active on the full frontier event type, while every other party gets the profile-induced frontier observation;
• at a parallel node with exactly one live side, control collapses to that side's current local view and is then lifted back to the full frontier type without introducing a spurious branch tag from the dead side;
• at done, everyone is hidden.

This is the fundamental current-step local interface for the concurrent layer.

@[reducible, inline]

abbrev Interaction.Concurrent.Current.ObsType {Party : Type u} [DecidableEq Party] (me : Party) {S : Spec} (control : Control Party S) (profile : Profile Party S) : Type (u + 1)

ObsType me control profile is the type of the current local observation available to the fixed party me for the next frontier event.

This is just the observation type of Current.view me control profile.

def Interaction.Concurrent.Current.observe {Party : Type u} [DecidableEq Party] (me : Party) {S : Spec} (control : Control Party S) (profile : Profile Party S) (event : Front S) : ObsType me control profile

observe me control profile event is the current local observation exposed to the fixed party me by the concrete frontier event event.

If me is currently the active controller, this returns the full frontier event itself. Otherwise, it returns the profile-induced observation of that frontier event.

def Interaction.Concurrent.Current.residualView {Party : Type u} [DecidableEq Party] (me : Party) {S : Spec} (control : Control Party S) (profile : Profile Party S) (event : Front S) : Multiparty.LocalView (Front (residual event))

residualView me control profile event is the current local view of the fixed party me after scheduling the frontier event event.

This is defined by first transporting both control and profile through the event, then recomputing the current local view of the residual concurrent interaction.