Composing two-party protocols

Role-aware composition of strategies and counterparts along Spec.append, Spec.replicate, and Spec.stateChain. Each combinator dispatches on the role at each node (sending or receiving) to compose the two-party strategies correctly.

For binary composition, compWithRoles and Counterpart.append use Transcript.liftAppend for the output type (factored form). The flat variants (compWithRolesFlat, Counterpart.appendFlat) take a single output family on the combined transcript.

class Interaction.Spec.LawfulCommMonad (m : Type u → Type u) [Monad m] extends LawfulMonad m : Prop

A lawful monad whose independent effects may be swapped.

This is the exact extra structure needed for the sequential-composition execution theorems once both sides may perform effects after a sender move is observed: the composed prover may prepare suffix state before the counterpart finishes its sender-side observation, so proving the usual factorization law requires commuting those independent effects.

• map_const {α β : Type u} : Functor.mapConst = Functor.map ∘ Function.const β
• id_map {α : Type u} (x : m α) : id <$> x = x
• comp_map {α β γ : Type u} (g : α → β) (h : β → γ) (x : m α) : (h ∘ g) <$> x = h <$> g <$> x
• seqLeft_eq {α β : Type u} (x : m α) (y : m β) : x <* y = Function.const β <$> x <*> y
• seqRight_eq {α β : Type u} (x : m α) (y : m β) : x *> y = Function.const α id <$> x <*> y
• pure_seq {α β : Type u} (g : α → β) (x : m α) : pure g <*> x = g <$> x
• map_pure {α β : Type u} (g : α → β) (x : α) : g <$> pure x = pure (g x)
• seq_pure {α β : Type u} (g : m (α → β)) (x : α) : g <*> pure x = (fun (h : α → β) => h x) <$> g
• seq_assoc {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)) : h <*> (g <*> x) = Function.comp <$> h <*> g <*> x
• bind_pure_comp {α β : Type u} (f : α → β) (x : m α) : (do let a ← x pure (f a)) = f <$> x
• bind_map {α β : Type u} (f : m (α → β)) (x : m α) : (do let x_1 ← f x_1 <$> x) = f <*> x
• pure_bind {α β : Type u} (x : α) (f : α → m β) : pure x >>= f = f x
• bind_assoc {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ) : x >>= f >>= g = x >>= fun (x : α) => f x >>= g
• bind_comm {α β γ : Type u} (ma : m α) (mb : m β) (k : α → β → m γ) : (do let a ← ma let b ← mb k a b) = do let b ← mb let a ← ma k a b

def Interaction.Spec.Strategy.compWithRoles {m : Type u → Type u} [Monad m] {s₁ : Spec} {s₂ : s₁.Transcript → Spec} {r₁ : RoleDecoration s₁} {r₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁)} {Mid : s₁.Transcript → Type u} {F : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u} (strat₁ : withRoles m s₁ r₁ Mid) (f : (tr₁ : s₁.Transcript) → Mid tr₁ → m (withRoles m (s₂ tr₁) (r₂ tr₁) (F tr₁))) : m (withRoles m (s₁.append s₂) (Decoration.append r₁ r₂) (Transcript.liftAppend s₁ s₂ F))

Compose role-aware strategies along Spec.append with a two-argument output family lifted through Transcript.liftAppend. The continuation receives the first phase's output and produces a second-phase strategy.

def Interaction.Spec.Strategy.compWithRolesFlat {m : Type u → Type u} [Monad m] {s₁ : Spec} {s₂ : s₁.Transcript → Spec} {r₁ : RoleDecoration s₁} {r₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁)} {Mid : s₁.Transcript → Type u} {Output : (s₁.append s₂).Transcript → Type u} (strat₁ : withRoles m s₁ r₁ Mid) (f : (tr₁ : s₁.Transcript) → Mid tr₁ → m (withRoles m (s₂ tr₁) (r₂ tr₁) fun (tr₂ : (s₂ tr₁).Transcript) => Output (Transcript.append s₁ s₂ tr₁ tr₂))) : m (withRoles m (s₁.append s₂) (Decoration.append r₁ r₂) Output)

Compose role-aware strategies along Spec.append with a single output family on the combined transcript. The continuation indexes via Transcript.append.

def Interaction.Spec.Strategy.splitPrefixWithRoles {m : Type u → Type u} [Functor m] {s₁ : Spec} {s₂ : s₁.Transcript → Spec} {r₁ : RoleDecoration s₁} {r₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁)} {Output : (s₁.append s₂).Transcript → Type u} : withRoles m (s₁.append s₂) (Decoration.append r₁ r₂) Output → withRoles m s₁ r₁ fun (tr₁ : s₁.Transcript) => withRoles m (s₂ tr₁) (r₂ tr₁) fun (tr₂ : (s₂ tr₁).Transcript) => Output (Transcript.append s₁ s₂ tr₁ tr₂)

Extract the first-phase role-aware strategy from a strategy on a composed interaction. At each first-phase transcript tr₁, the remainder is the second-phase strategy with output indexed by Transcript.append.

theorem Interaction.Spec.Strategy.compWithRolesFlat_splitPrefixWithRoles {m : Type u → Type u} [Monad m] [LawfulMonad m] {s₁ : Spec} {s₂ : s₁.Transcript → Spec} {r₁ : RoleDecoration s₁} {r₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁)} {Output : (s₁.append s₂).Transcript → Type u} (strat : withRoles m (s₁.append s₂) (Decoration.append r₁ r₂) Output) : (compWithRolesFlat (splitPrefixWithRoles strat) fun (x : s₁.Transcript) (strat₂ : withRoles m (s₂ x) (r₂ x) fun (tr₂ : (s₂ x).Transcript) => Output (Transcript.append s₁ s₂ x tr₂)) => pure strat₂) = pure strat

Recompose a role-aware strategy from its prefix decomposition.

theorem Interaction.Spec.Strategy.compWithRolesFlat_splitPrefixWithRoles.go {m : Type u → Type u} [Monad m] [LawfulMonad m] (s₁ : Spec) (r₁ : RoleDecoration s₁) {s₂ : s₁.Transcript → Spec} {r₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁)} {Output : (s₁.append s₂).Transcript → Type u} (strat : withRoles m (s₁.append s₂) (Decoration.append r₁ r₂) Output) : (compWithRolesFlat (splitPrefixWithRoles strat) fun (x : s₁.Transcript) (strat₂ : withRoles m (s₂ x) (r₂ x) fun (tr₂ : (s₂ x).Transcript) => Output (Transcript.append s₁ s₂ x tr₂)) => pure strat₂) = pure strat

def Interaction.Spec.Counterpart.append {m : Type u → Type u} [Monad m] {s₁ : Spec} {s₂ : s₁.Transcript → Spec} {r₁ : RoleDecoration s₁} {r₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁)} {Output₁ : s₁.Transcript → Type u} {F : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u} : Counterpart m s₁ r₁ Output₁ → ((tr₁ : s₁.Transcript) → Output₁ tr₁ → Counterpart m (s₂ tr₁) (r₂ tr₁) (F tr₁)) → Counterpart m (s₁.append s₂) (Decoration.append r₁ r₂) (Transcript.liftAppend s₁ s₂ F)

Compose counterparts along Spec.append with a two-argument output family lifted through Transcript.liftAppend. The continuation maps the first phase's output to a second-phase counterpart.

def Interaction.Spec.Counterpart.appendFlat {m : Type u → Type u} [Monad m] {s₁ : Spec} {s₂ : s₁.Transcript → Spec} {r₁ : RoleDecoration s₁} {r₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁)} {Output₁ : s₁.Transcript → Type u} {Output₂ : (s₁.append s₂).Transcript → Type u} : Counterpart m s₁ r₁ Output₁ → ((tr₁ : s₁.Transcript) → Output₁ tr₁ → Counterpart m (s₂ tr₁) (r₂ tr₁) fun (tr₂ : (s₂ tr₁).Transcript) => Output₂ (Transcript.append s₁ s₂ tr₁ tr₂)) → Counterpart m (s₁.append s₂) (Decoration.append r₁ r₂) Output₂

Compose counterparts along Spec.append with a single output family on the combined transcript. The continuation indexes via Transcript.append.

theorem Interaction.Spec.Counterpart.append_eq_appendFlat_mapOutput {m : Type u → Type u} [Monad m] [LawfulMonad m] {s₁ : Spec} {s₂ : s₁.Transcript → Spec} {r₁ : RoleDecoration s₁} {r₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁)} {Output₁ : s₁.Transcript → Type u} {F : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u} (c₁ : Counterpart m s₁ r₁ Output₁) (c₂ : (tr₁ : s₁.Transcript) → Output₁ tr₁ → Counterpart m (s₂ tr₁) (r₂ tr₁) (F tr₁)) : c₁.append c₂ = c₁.appendFlat fun (tr₁ : s₁.Transcript) (o : Output₁ tr₁) => mapOutput (fun (tr₂ : (s₂ tr₁).Transcript) (x : F tr₁ tr₂) => Transcript.packAppend s₁ s₂ F tr₁ tr₂ x) (c₂ tr₁ o)

Counterpart.append equals appendFlat composed with mapOutput packAppend. This lets proofs that decompose an arbitrary strategy via splitPrefixWithRoles + appendFlat still work when Reduction.comp uses the non-flat append.

def Interaction.Spec.Counterpart.withMonads.append {s₁ : Spec} {s₂ : s₁.Transcript → Spec} {r₁ : RoleDecoration s₁} {r₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁)} {md₁ : s₁.MonadDecoration} {md₂ : (tr₁ : s₁.Transcript) → (s₂ tr₁).MonadDecoration} {Output₁ : s₁.Transcript → Type u} {F : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u} : withMonads s₁ r₁ md₁ Output₁ → ((tr₁ : s₁.Transcript) → Output₁ tr₁ → withMonads (s₂ tr₁) (r₂ tr₁) (md₂ tr₁) (F tr₁)) → withMonads (s₁.append s₂) (Decoration.append r₁ r₂) (Decoration.append md₁ md₂) (Transcript.liftAppend s₁ s₂ F)

Compose per-node-monad counterparts along Spec.append with a two-argument output family lifted through Transcript.liftAppend. At each node, the recursive composition is lifted through the node's BundledMonad via Functor.map.

theorem Interaction.Spec.Strategy.runWithRoles_compWithRolesFlat_appendFlat_pure {m : Type u → Type u} [Monad m] [LawfulMonad m] {s₁ : Spec} {s₂ : s₁.Transcript → Spec} {r₁ : RoleDecoration s₁} {r₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁)} {MidP MidC : s₁.Transcript → Type u} {OutputP OutputC : (s₁.append s₂).Transcript → Type u} (strat₁ : withRoles m s₁ r₁ MidP) (f : (tr₁ : s₁.Transcript) → MidP tr₁ → withRoles m (s₂ tr₁) (r₂ tr₁) fun (tr₂ : (s₂ tr₁).Transcript) => OutputP (Transcript.append s₁ s₂ tr₁ tr₂)) (cpt₁ : Counterpart m s₁ r₁ MidC) (cpt₂ : (tr₁ : s₁.Transcript) → MidC tr₁ → Counterpart m (s₂ tr₁) (r₂ tr₁) fun (tr₂ : (s₂ tr₁).Transcript) => OutputC (Transcript.append s₁ s₂ tr₁ tr₂)) : (do let strat ← compWithRolesFlat strat₁ fun (tr₁ : s₁.Transcript) (mid : MidP tr₁) => pure (f tr₁ mid) runWithRoles (s₁.append s₂) (Decoration.append r₁ r₂) strat (cpt₁.appendFlat cpt₂)) = do let __discr ← runWithRoles s₁ r₁ strat₁ cpt₁ match __discr with | ⟨tr₁, (mid, out₁)⟩ => do let __discr ← runWithRoles (s₂ tr₁) (r₂ tr₁) (f tr₁ mid) (cpt₂ tr₁ out₁) match __discr with | ⟨tr₂, (outP, outC)⟩ => pure ⟨Transcript.append s₁ s₂ tr₁ tr₂, (outP, outC)⟩

Executing a flat composed strategy/counterpart factors into first executing the prefix interaction and then executing the suffix continuation.

theorem Interaction.Spec.Strategy.runWithRoles_compWithRolesFlat_appendFlat_pure.go {m : Type u → Type u} [Monad m] [LawfulMonad m] (s₁ : Spec) (r₁ : RoleDecoration s₁) {MidP MidC : s₁.Transcript → Type u} {s₂ : s₁.Transcript → Spec} {r₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁)} {OutputP OutputC : (s₁.append s₂).Transcript → Type u} {β : Type u} (strat₁ : withRoles m s₁ r₁ MidP) (f : (tr₁ : s₁.Transcript) → MidP tr₁ → withRoles m (s₂ tr₁) (r₂ tr₁) fun (tr₂ : (s₂ tr₁).Transcript) => OutputP (Transcript.append s₁ s₂ tr₁ tr₂)) (cpt₁ : Counterpart m s₁ r₁ MidC) (cpt₂ : (tr₁ : s₁.Transcript) → MidC tr₁ → Counterpart m (s₂ tr₁) (r₂ tr₁) fun (tr₂ : (s₂ tr₁).Transcript) => OutputC (Transcript.append s₁ s₂ tr₁ tr₂)) (g : (tr : (s₁.append s₂).Transcript) × OutputP tr × OutputC tr → m β) : (have __do_jp := fun (r : (tr : (s₁.append s₂).Transcript) × OutputP tr × OutputC tr) => g r; do let strat ← compWithRolesFlat strat₁ fun (tr₁ : s₁.Transcript) (mid : MidP tr₁) => pure (f tr₁ mid) let y ← runWithRoles (s₁.append s₂) (Decoration.append r₁ r₂) strat (cpt₁.appendFlat cpt₂) __do_jp y) = do let r₁ ← runWithRoles s₁ r₁ strat₁ cpt₁ let r₂ ← runWithRoles (s₂ r₁.fst) (r₂ r₁.fst) (f r₁.fst r₁.snd.fst) (cpt₂ r₁.fst r₁.snd.snd) g ⟨Transcript.append s₁ s₂ r₁.fst r₂.fst, (r₂.snd.fst, r₂.snd.snd)⟩

theorem Interaction.Spec.Strategy.runWithRoles_compWithRolesFlat_appendFlat {m : Type u → Type u} [Monad m] [LawfulCommMonad m] {s₁ : Spec} {s₂ : s₁.Transcript → Spec} {r₁ : RoleDecoration s₁} {r₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁)} {MidP MidC : s₁.Transcript → Type u} {OutputP OutputC : (s₁.append s₂).Transcript → Type u} (strat₁ : withRoles m s₁ r₁ MidP) (f : (tr₁ : s₁.Transcript) → MidP tr₁ → m (withRoles m (s₂ tr₁) (r₂ tr₁) fun (tr₂ : (s₂ tr₁).Transcript) => OutputP (Transcript.append s₁ s₂ tr₁ tr₂))) (cpt₁ : Counterpart m s₁ r₁ MidC) (cpt₂ : (tr₁ : s₁.Transcript) → MidC tr₁ → Counterpart m (s₂ tr₁) (r₂ tr₁) fun (tr₂ : (s₂ tr₁).Transcript) => OutputC (Transcript.append s₁ s₂ tr₁ tr₂)) : (do let strat ← compWithRolesFlat strat₁ f runWithRoles (s₁.append s₂) (Decoration.append r₁ r₂) strat (cpt₁.appendFlat cpt₂)) = do let __discr ← runWithRoles s₁ r₁ strat₁ cpt₁ match __discr with | ⟨tr₁, (mid, out₁)⟩ => do let strat₂ ← f tr₁ mid let __discr ← runWithRoles (s₂ tr₁) (r₂ tr₁) strat₂ (cpt₂ tr₁ out₁) match __discr with | ⟨tr₂, (outP, outC)⟩ => pure ⟨Transcript.append s₁ s₂ tr₁ tr₂, (outP, outC)⟩

Executing a flat composed strategy/counterpart factors into first executing the prefix interaction and then executing the suffix continuation.

theorem Interaction.Spec.Strategy.runWithRoles_compWithRolesFlat_appendFlat.go {m : Type u → Type u} [Monad m] [LawfulCommMonad m] (s₁ : Spec) (r₁ : RoleDecoration s₁) {MidP MidC : s₁.Transcript → Type u} {s₂ : s₁.Transcript → Spec} {r₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁)} {OutputP OutputC : (s₁.append s₂).Transcript → Type u} {β : Type u} (strat₁ : withRoles m s₁ r₁ MidP) (f : (tr₁ : s₁.Transcript) → MidP tr₁ → m (withRoles m (s₂ tr₁) (r₂ tr₁) fun (tr₂ : (s₂ tr₁).Transcript) => OutputP (Transcript.append s₁ s₂ tr₁ tr₂))) (cpt₁ : Counterpart m s₁ r₁ MidC) (cpt₂ : (tr₁ : s₁.Transcript) → MidC tr₁ → Counterpart m (s₂ tr₁) (r₂ tr₁) fun (tr₂ : (s₂ tr₁).Transcript) => OutputC (Transcript.append s₁ s₂ tr₁ tr₂)) (g : (tr : (s₁.append s₂).Transcript) × OutputP tr × OutputC tr → m β) : (have __do_jp := fun (r : (tr : (s₁.append s₂).Transcript) × OutputP tr × OutputC tr) => g r; do let strat ← compWithRolesFlat strat₁ f let y ← runWithRoles (s₁.append s₂) (Decoration.append r₁ r₂) strat (cpt₁.appendFlat cpt₂) __do_jp y) = do let r₁ ← runWithRoles s₁ r₁ strat₁ cpt₁ let strat₂ ← f r₁.fst r₁.snd.fst let r₂ ← runWithRoles (s₂ r₁.fst) (r₂ r₁.fst) strat₂ (cpt₂ r₁.fst r₁.snd.snd) g ⟨Transcript.append s₁ s₂ r₁.fst r₂.fst, (r₂.snd.fst, r₂.snd.snd)⟩

theorem Interaction.Spec.Strategy.runWithRoles_compWithRoles_append {m : Type u → Type u} [Monad m] [LawfulCommMonad m] {s₁ : Spec} {s₂ : s₁.Transcript → Spec} {r₁ : RoleDecoration s₁} {r₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁)} {MidP MidC : s₁.Transcript → Type u} {FP FC : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u} (strat₁ : withRoles m s₁ r₁ MidP) (f : (tr₁ : s₁.Transcript) → MidP tr₁ → m (withRoles m (s₂ tr₁) (r₂ tr₁) (FP tr₁))) (cpt₁ : Counterpart m s₁ r₁ MidC) (cpt₂ : (tr₁ : s₁.Transcript) → MidC tr₁ → Counterpart m (s₂ tr₁) (r₂ tr₁) (FC tr₁)) : (do let strat ← compWithRoles strat₁ f runWithRoles (s₁.append s₂) (Decoration.append r₁ r₂) strat (cpt₁.append cpt₂)) = do let __discr ← runWithRoles s₁ r₁ strat₁ cpt₁ match __discr with | ⟨tr₁, (mid, out₁)⟩ => do let strat₂ ← f tr₁ mid let __discr ← runWithRoles (s₂ tr₁) (r₂ tr₁) strat₂ (cpt₂ tr₁ out₁) match __discr with | ⟨tr₂, (outP, outC)⟩ => pure ⟨Transcript.append s₁ s₂ tr₁ tr₂, (Transcript.packAppend s₁ s₂ FP tr₁ tr₂ outP, Transcript.packAppend s₁ s₂ FC tr₁ tr₂ outC)⟩

Executing a factored composed strategy/counterpart (using compWithRoles and Counterpart.append) factors into first executing the prefix interaction and then executing the suffix continuation. Outputs are transported via packAppend.

theorem Interaction.Spec.Strategy.runWithRoles_compWithRoles_append.go {m : Type u → Type u} [Monad m] [LawfulCommMonad m] (s₁ : Spec) (r₁ : RoleDecoration s₁) {MidP MidC : s₁.Transcript → Type u} {s₂ : s₁.Transcript → Spec} {r₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁)} {FP FC : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u} {β : Type u} (strat₁ : withRoles m s₁ r₁ MidP) (f : (tr₁ : s₁.Transcript) → MidP tr₁ → m (withRoles m (s₂ tr₁) (r₂ tr₁) (FP tr₁))) (cpt₁ : Counterpart m s₁ r₁ MidC) (cpt₂ : (tr₁ : s₁.Transcript) → MidC tr₁ → Counterpart m (s₂ tr₁) (r₂ tr₁) (FC tr₁)) (g : (tr : (s₁.append s₂).Transcript) × Transcript.liftAppend s₁ s₂ FP tr × Transcript.liftAppend s₁ s₂ FC tr → m β) : (have __do_jp := fun (r : (tr : (s₁.append s₂).Transcript) × Transcript.liftAppend s₁ s₂ FP tr × Transcript.liftAppend s₁ s₂ FC tr) => g r; do let strat ← compWithRoles strat₁ f let y ← runWithRoles (s₁.append s₂) (Decoration.append r₁ r₂) strat (cpt₁.append cpt₂) __do_jp y) = do let r₁ ← runWithRoles s₁ r₁ strat₁ cpt₁ let strat₂ ← f r₁.fst r₁.snd.fst let r₂ ← runWithRoles (s₂ r₁.fst) (r₂ r₁.fst) strat₂ (cpt₂ r₁.fst r₁.snd.snd) g ⟨Transcript.append s₁ s₂ r₁.fst r₂.fst, (Transcript.packAppend s₁ s₂ FP r₁.fst r₂.fst r₂.snd.fst, Transcript.packAppend s₁ s₂ FC r₁.fst r₂.fst r₂.snd.snd)⟩

theorem Interaction.Spec.RoleDecoration.swap_replicate {spec : Spec} (roles : RoleDecoration spec) (n : ℕ) : (Decoration.replicate roles n).swap = (Decoration.swap roles).replicate n

Role swapping commutes with replication.

def Interaction.Spec.Counterpart.iterate {m : Type u → Type u} [Monad m] {spec : Spec} {roles : RoleDecoration spec} {β : Type u} (n : ℕ) : (Fin n → β → Counterpart m spec roles fun (x : spec.Transcript) => β) → β → Counterpart m (spec.replicate n) (Decoration.replicate roles n) fun (x : (spec.replicate n).Transcript) => β

n-fold counterpart iteration on spec.replicate n, threading state β through each round.

def Interaction.Spec.Strategy.iterateWithRoles {m : Type u → Type u} [Monad m] {spec : Spec} {roles : RoleDecoration spec} {α : Type u} (n : ℕ) (step : Fin n → α → m (withRoles m spec roles fun (x : spec.Transcript) => α)) : α → m (withRoles m (spec.replicate n) (Decoration.replicate roles n) fun (x : (spec.replicate n).Transcript) => α)

n-fold role-aware strategy iteration on spec.replicate n, threading state α through each round.

def Interaction.Spec.Counterpart.stateChainComp {m : Type u → Type u} [Monad m] {Stage : ℕ → Type u} {spec : (i : ℕ) → Stage i → Spec} {advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)} {roles : (i : ℕ) → (s : Stage i) → RoleDecoration (spec i s)} {Family : (i : ℕ) → Stage i → Type u} (step : (i : ℕ) → (s : Stage i) → Family i s → Counterpart m (spec i s) (roles i s) fun (tr : (spec i s).Transcript) => Family (i + 1) (advance i s tr)) (n i : ℕ) (s : Stage i) : Family i s → Counterpart m (stateChain Stage spec advance n i s) (Decoration.stateChain roles n i s) (Transcript.stateChainFamily Family n i s)

Compose counterparts along a state chain with stage-dependent output. At each stage, the step transforms Family i s into a counterpart whose output is Family (i+1) (advance i s tr). The full state chain output is Transcript.stateChainFamily Family.

def Interaction.Spec.Strategy.stateChainCompWithRoles {m : Type u → Type u} [Monad m] {Stage : ℕ → Type u} {spec : (i : ℕ) → Stage i → Spec} {advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)} {roles : (i : ℕ) → (s : Stage i) → RoleDecoration (spec i s)} {Family : (i : ℕ) → Stage i → Type u} (step : (i : ℕ) → (s : Stage i) → Family i s → m (withRoles m (spec i s) (roles i s) fun (tr : (spec i s).Transcript) => Family (i + 1) (advance i s tr))) (n i : ℕ) (s : Stage i) : Family i s → m (withRoles m (stateChain Stage spec advance n i s) (Decoration.stateChain roles n i s) (Transcript.stateChainFamily Family n i s))

Compose role-aware strategies along a state chain with stage-dependent output. At each stage, the step transforms Family i s into a strategy whose output is Family (i+1) (advance i s tr). The full state chain output is Transcript.stateChainFamily Family.

def Interaction.Spec.Counterpart.withMonads.stateChainComp {Stage : ℕ → Type u} {spec : (i : ℕ) → Stage i → Spec} {advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)} {roles : (i : ℕ) → (s : Stage i) → RoleDecoration (spec i s)} {md : (i : ℕ) → (s : Stage i) → (spec i s).MonadDecoration} {Family : (i : ℕ) → Stage i → Type u} (step : (i : ℕ) → (s : Stage i) → Family i s → withMonads (spec i s) (roles i s) (md i s) fun (tr : (spec i s).Transcript) => Family (i + 1) (advance i s tr)) (n i : ℕ) (s : Stage i) : Family i s → withMonads (stateChain Stage spec advance n i s) (Decoration.stateChain roles n i s) (Decoration.stateChain md n i s) (Transcript.stateChainFamily Family n i s)

Compose per-node-monad counterparts along a state chain with stage-dependent output. At each stage, the step transforms Family i s into a counterpart whose output is Family (i+1) (advance i s tr). The full state chain output is Transcript.stateChainFamily Family.