Continuation-style chains (Spec.Chain)

A Chain n is a self-contained recipe for an n-round protocol: at each level it carries the current round's Spec and a transcript-indexed continuation to the next level. There is no external state type, no Stage : Nat → Type, and no round index family.

Converting to a Spec via Chain.toSpec uses only Spec.append. State-machine constructions are derived: Chain.ofStateMachine builds a chain from (σ, step, next, s₀) and then forgets σ.

Main definitions

• Spec.Chain — depth-indexed telescope: round spec + continuation.
• Spec.Chain.toSpec — convert a chain into a concrete Spec.
• Chain.replicate — constant rounds (recovers Spec.replicate).
• Chain.ofStateMachine — build from a state machine (recovers Spec.stateChain).

Three composition mechanisms

Mechanism	State?	Transcript-dependent?	Use when
Spec.replicate	No	No	Uniform rounds (same spec, independent)
Spec.stateChain	Yes (Stage i)	Yes	State machine with explicit state type
Spec.Chain	No (baked in)	Yes	Continuation-style, no external state

Chain is the most fundamental: it requires no external state type, yet supports full transcript dependence. stateChain is a specialization (recovered by Chain.ofStateMachine), and replicate is a further specialization (recovered by Chain.replicate).

Toy examples

The GrowingMessages section builds a protocol whose message type grows at each step (Fin 1, Fin 2, …) without mentioning any state type.

def Interaction.Spec.Chain : ℕ → Type (u + 1)

A self-contained recipe for an n-round protocol. At each level, carries the current round's Spec and, for each possible transcript, the recipe for the remaining rounds. No external state type.

def Interaction.Spec.Chain.toSpec (n : ℕ) : Chain n → Spec

Convert a chain into a concrete Spec via iterated append.

@[simp]

theorem Interaction.Spec.Chain.toSpec_zero (c : Chain 0) : toSpec 0 c = done

theorem Interaction.Spec.Chain.toSpec_succ {n : ℕ} (spec : Spec) (cont : spec.Transcript → Chain n) : toSpec (n + 1) ⟨spec, cont⟩ = spec.append fun (tr : spec.Transcript) => toSpec n (cont tr)

Constructors

def Interaction.Spec.Chain.replicate (spec : Spec) (n : ℕ) : Chain n

Constant rounds: same spec every round, continuation ignores the transcript.

def Interaction.Spec.Chain.ofStateMachine {σ : Type u} (step : σ → Spec) (next : (s : σ) → (step s).Transcript → σ) (n : ℕ) : σ → Chain n

Build a chain from a state machine. The state σ is consumed during construction and does not appear in the resulting Chain.

Bridge to existing API

theorem Interaction.Spec.Chain.toSpec_replicate (spec : Spec) (n : ℕ) : toSpec n (replicate spec n) = spec.replicate n

Converting a replicate chain recovers Spec.replicate.

theorem Interaction.Spec.Chain.toSpec_ofStateMachine {σ : Type u} (step : σ → Spec) (next : (s : σ) → (step s).Transcript → σ) (n i : ℕ) (s : σ) : toSpec n (ofStateMachine step next n s) = stateChain (fun (x : ℕ) => σ) (fun (x : ℕ) => step) (fun (x : ℕ) => next) n i s

Converting a state-machine chain recovers Spec.stateChain with constant stage family and round index erased.

Transcript operations

def Interaction.Spec.Chain.splitTranscript (n : ℕ) (c : Chain (n + 1)) : (toSpec (n + 1) c).Transcript → (tr₁ : c.fst.Transcript) × (toSpec n (c.snd tr₁)).Transcript

Split a transcript of an (n+1)-round chain into the first round's transcript and the remainder.

def Interaction.Spec.Chain.appendTranscript (n : ℕ) (c : Chain (n + 1)) (tr₁ : c.fst.Transcript) (tr₂ : (toSpec n (c.snd tr₁)).Transcript) : (toSpec (n + 1) c).Transcript

Combine a first-round transcript with a remainder.

@[simp]

theorem Interaction.Spec.Chain.splitTranscript_appendTranscript (n : ℕ) (c : Chain (n + 1)) (tr₁ : c.fst.Transcript) (tr₂ : (toSpec n (c.snd tr₁)).Transcript) : splitTranscript n c (appendTranscript n c tr₁ tr₂) = ⟨tr₁, tr₂⟩

Strategy composition

def Interaction.Spec.Chain.outputFamily (Family : {n : ℕ} → Chain n → Type u) (n : ℕ) (c : Chain n) : (toSpec n c).Transcript → Type u

Output family for strategy composition along a chain. This is the intrinsic analog of Transcript.stateChainFamily: a family on the remaining chain is lifted to a family on transcripts of the flattened Spec.

def Interaction.Spec.Chain.strategyComp {m : Type u → Type u} [Monad m] {Family : {n : ℕ} → Chain n → Type u} (step : {n : ℕ} → (c : Chain (n + 1)) → Family c → m (Strategy m c.fst fun (tr : c.fst.Transcript) => Family (c.snd tr))) (n : ℕ) (c : Chain n) : Family c → m (Strategy m (toSpec n c) (outputFamily (fun {n : ℕ} => Family) n c))

Compose strategies along a chain with a transcript-dependent output family. The step function sees the current round spec packaged as the remaining chain, and returns the next family member indexed by the transcript of that round.

Toy example: growing message types

Toy example: genuine transcript-prefix dependence

Dependent strategy composition over the prefix-dependent example