Dependent append of interaction specs

Given two interactions where the second may depend on the outcome of the first, Spec.append fuses them into a single interaction. The file provides the full algebra around this operation:

• Transcript operations: Transcript.append / split construct and decompose combined transcripts, while Transcript.liftAppend lifts a two-argument type family to a single-argument family on the combined transcript with definitional computation.
• Strategy composition: Strategy.comp (factored output via liftAppend) and Strategy.compFlat (flat output via Transcript.append).
• Decoration / refinement append and their naturality lemmas.

Structural combinators

def Interaction.Spec.append (s₁ : Spec) : (s₁.Transcript → Spec) → Spec

Sequential composition of interactions: run s₁ first, then continue with s₂ tr₁ where tr₁ records what happened in s₁.

def Interaction.Spec.Transcript.liftAppend (s₁ : Spec) (s₂ : s₁.Transcript → Spec) : ((tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) → (s₁.append s₂).Transcript → Type u

Lift a two-argument type family F tr₁ tr₂ (indexed by per-phase transcripts) to a single-argument family on the combined transcript of s₁.append s₂.

Crucially, liftAppend s₁ s₂ F (Transcript.append s₁ s₂ tr₁ tr₂) reduces definitionally to F tr₁ tr₂, which makes this the right combinator for stage-dependent composition. Without this property, every composition combinator would need explicit casts between the two-argument and single-argument views.

This combinator propagates up through the entire stack:

• Transcript.stateChainFamily uses it at each stage of a state chain
• Chain.outputFamily uses it at each round of a continuation chain
• Strategy.comp / Strategy.compWithRoles use it for the output type
• All security composition theorems factor through it

theorem Interaction.Spec.Transcript.liftAppend_congr (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (F G : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) : (∀ (tr₁ : s₁.Transcript) (tr₂ : (s₂ tr₁).Transcript), F tr₁ tr₂ = G tr₁ tr₂) → ∀ (tr : (s₁.append s₂).Transcript), liftAppend s₁ s₂ F tr = liftAppend s₁ s₂ G tr

liftAppend respects pointwise equality of the family F.

@[simp]

theorem Interaction.Spec.Transcript.liftAppend_const (α : Type u) (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (tr : (s₁.append s₂).Transcript) : liftAppend s₁ s₂ (fun (x : s₁.Transcript) (x_1 : (s₂ x).Transcript) => α) tr = α

A constant family is unaffected by liftAppend.

def Interaction.Spec.Transcript.append (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (tr₁ : s₁.Transcript) : (s₂ tr₁).Transcript → (s₁.append s₂).Transcript

Combine a first-phase transcript and a second-phase transcript into a transcript of the composed interaction s₁.append s₂.

@[simp]

theorem Interaction.Spec.Transcript.liftAppend_append (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (F : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (tr₁ : s₁.Transcript) (tr₂ : (s₂ tr₁).Transcript) : liftAppend s₁ s₂ F (append s₁ s₂ tr₁ tr₂) = F tr₁ tr₂

liftAppend on an appended transcript reduces to the original two-argument family.

def Interaction.Spec.Transcript.split (s₁ : Spec) (s₂ : s₁.Transcript → Spec) : (s₁.append s₂).Transcript → (tr₁ : s₁.Transcript) × (s₂ tr₁).Transcript

Decompose a transcript of s₁.append s₂ into the first-phase prefix and the second-phase continuation. Inverse of Transcript.append.

@[simp]

theorem Interaction.Spec.Transcript.split_append (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (tr₁ : s₁.Transcript) (tr₂ : (s₂ tr₁).Transcript) : split s₁ s₂ (append s₁ s₂ tr₁ tr₂) = ⟨tr₁, tr₂⟩

Splitting after appending recovers the original components.

@[simp]

theorem Interaction.Spec.Transcript.append_split (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (tr : (s₁.append s₂).Transcript) : match split s₁ s₂ tr with | ⟨tr₁, tr₂⟩ => append s₁ s₂ tr₁ tr₂ = tr

Appending the components produced by split recovers the original transcript.

theorem Interaction.Spec.Transcript.liftAppend_split (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (F : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (tr : (s₁.append s₂).Transcript) : match split s₁ s₂ tr with | ⟨tr₁, tr₂⟩ => liftAppend s₁ s₂ F tr = F tr₁ tr₂

liftAppend can be reconstructed from the transcript pieces returned by Transcript.split.

def Interaction.Spec.Transcript.unliftAppend (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (F : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (tr : (s₁.append s₂).Transcript) : liftAppend s₁ s₂ F tr → match split s₁ s₂ tr with | ⟨tr₁, tr₂⟩ => F tr₁ tr₂

Reinterpret a liftAppend value against the transcript pair recovered by split. Defined by structural recursion mirroring liftAppend/split, so no explicit cast appears in the definition.

def Interaction.Spec.Transcript.packAppend (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (F : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (tr₁ : s₁.Transcript) (tr₂ : (s₂ tr₁).Transcript) : F tr₁ tr₂ → liftAppend s₁ s₂ F (append s₁ s₂ tr₁ tr₂)

Transport a value of F tr₁ tr₂ to liftAppend s₁ s₂ F (append s₁ s₂ tr₁ tr₂). Defined by structural recursion mirroring liftAppend/append, so no explicit cast appears. This is the identity function in disguise — at each constructor step, liftAppend s₁ s₂ F (append s₁ s₂ tr₁ tr₂) reduces to F tr₁ tr₂.

def Interaction.Spec.Transcript.unpackAppend (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (F : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (tr₁ : s₁.Transcript) (tr₂ : (s₂ tr₁).Transcript) : liftAppend s₁ s₂ F (append s₁ s₂ tr₁ tr₂) → F tr₁ tr₂

Transport a liftAppend value back to the pair-indexed family. Inverse of packAppend.

@[simp]

theorem Interaction.Spec.Transcript.unpackAppend_packAppend (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (F : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (tr₁ : s₁.Transcript) (tr₂ : (s₂ tr₁).Transcript) (x : F tr₁ tr₂) : unpackAppend s₁ s₂ F tr₁ tr₂ (packAppend s₁ s₂ F tr₁ tr₂ x) = x

@[simp]

theorem Interaction.Spec.Transcript.packAppend_unpackAppend (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (F : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (tr₁ : s₁.Transcript) (tr₂ : (s₂ tr₁).Transcript) (x : liftAppend s₁ s₂ F (append s₁ s₂ tr₁ tr₂)) : packAppend s₁ s₂ F tr₁ tr₂ (unpackAppend s₁ s₂ F tr₁ tr₂ x) = x

def Interaction.Spec.Transcript.collapseAppend (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (F : (s₁.append s₂).Transcript → Type u) (tr : (s₁.append s₂).Transcript) : liftAppend s₁ s₂ (fun (tr₁ : s₁.Transcript) (tr₂ : (s₂ tr₁).Transcript) => F (append s₁ s₂ tr₁ tr₂)) tr → F tr

Collapse a liftAppend family indexed by append tr₁ tr₂ back to the fused transcript index. Defined by structural recursion, so no explicit cast appears.

@[simp]

theorem Interaction.Spec.Transcript.collapseAppend_append (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (F : (s₁.append s₂).Transcript → Type u) (tr₁ : s₁.Transcript) (tr₂ : (s₂ tr₁).Transcript) (x : liftAppend s₁ s₂ (fun (tr₁ : s₁.Transcript) (tr₂ : (s₂ tr₁).Transcript) => F (append s₁ s₂ tr₁ tr₂)) (append s₁ s₂ tr₁ tr₂)) : collapseAppend s₁ s₂ F (append s₁ s₂ tr₁ tr₂) x = cast ⋯ x

@[reducible, inline]

abbrev Interaction.Spec.Transcript.liftAppendFamily (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (F : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) : (s₁.append s₂).Transcript → Type u

Lift a family indexed by a split append transcript into a family indexed by the fused append transcript.

@[simp]

theorem Interaction.Spec.Transcript.liftAppendFamily_append (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (F : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (tr₁ : s₁.Transcript) (tr₂ : (s₂ tr₁).Transcript) : liftAppendFamily s₁ s₂ F (append s₁ s₂ tr₁ tr₂) = F tr₁ tr₂

def Interaction.Spec.Transcript.liftAppendProd (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (A B : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (tr : (s₁.append s₂).Transcript) : liftAppend s₁ s₂ (fun (tr₁ : s₁.Transcript) (tr₂ : (s₂ tr₁).Transcript) => A tr₁ tr₂ × B tr₁ tr₂) tr → liftAppend s₁ s₂ A tr × liftAppend s₁ s₂ B tr

Split a fused liftAppend value whose payload is a product into the product of the separately lifted payloads.

def Interaction.Spec.Transcript.liftAppendProdMk (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (A B : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (tr : (s₁.append s₂).Transcript) : liftAppend s₁ s₂ A tr × liftAppend s₁ s₂ B tr → liftAppend s₁ s₂ (fun (tr₁ : s₁.Transcript) (tr₂ : (s₂ tr₁).Transcript) => A tr₁ tr₂ × B tr₁ tr₂) tr

Inverse of liftAppendProd, fusing separately lifted payloads into a lifted product payload.

@[simp]

theorem Interaction.Spec.Transcript.liftAppendProdMk_liftAppendProd (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (A B : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (tr : (s₁.append s₂).Transcript) (x : liftAppend s₁ s₂ (fun (tr₁ : s₁.Transcript) (tr₂ : (s₂ tr₁).Transcript) => A tr₁ tr₂ × B tr₁ tr₂) tr) : liftAppendProdMk s₁ s₂ A B tr (liftAppendProd s₁ s₂ A B tr x) = x

@[simp]

theorem Interaction.Spec.Transcript.liftAppendProd_liftAppendProdMk (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (A B : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (tr : (s₁.append s₂).Transcript) (x : liftAppend s₁ s₂ A tr × liftAppend s₁ s₂ B tr) : liftAppendProd s₁ s₂ A B tr (liftAppendProdMk s₁ s₂ A B tr x) = x

@[simp]

theorem Interaction.Spec.Transcript.liftAppendProd_packAppend (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (A B : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (tr₁ : s₁.Transcript) (tr₂ : (s₂ tr₁).Transcript) (x : A tr₁ tr₂ × B tr₁ tr₂) : liftAppendProd s₁ s₂ A B (append s₁ s₂ tr₁ tr₂) (packAppend s₁ s₂ (fun (tr₁ : s₁.Transcript) (tr₂ : (s₂ tr₁).Transcript) => A tr₁ tr₂ × B tr₁ tr₂) tr₁ tr₂ x) = (packAppend s₁ s₂ A tr₁ tr₂ x.fst, packAppend s₁ s₂ B tr₁ tr₂ x.snd)

theorem Interaction.Spec.Transcript.rel_unliftAppend_append (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (F G : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (R : (tr₁ : s₁.Transcript) → (tr₂ : (s₂ tr₁).Transcript) → F tr₁ tr₂ → G tr₁ tr₂ → Prop) (tr₁ : s₁.Transcript) (tr₂ : (s₂ tr₁).Transcript) (x : F tr₁ tr₂) (y : G tr₁ tr₂) : let tr := append s₁ s₂ tr₁ tr₂; R (split s₁ s₂ tr).fst (split s₁ s₂ tr).snd (unliftAppend s₁ s₂ F tr (packAppend s₁ s₂ F tr₁ tr₂ x)) (unliftAppend s₁ s₂ G tr (packAppend s₁ s₂ G tr₁ tr₂ y)) = R tr₁ tr₂ x y

When tr = append tr₁ tr₂, the round-trip (packAppend then unliftAppend) recovers the original pair-indexed relation value.

def Interaction.Spec.Transcript.liftAppendRel (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (F G : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (R : (tr₁ : s₁.Transcript) → (tr₂ : (s₂ tr₁).Transcript) → F tr₁ tr₂ → G tr₁ tr₂ → Prop) (tr : (s₁.append s₂).Transcript) : liftAppend s₁ s₂ F tr → liftAppend s₁ s₂ G tr → Prop

Lift a binary relation on pair-indexed type families to the fused transcript of s₁.append s₂. Reduces definitionally when the transcript is Transcript.append s₁ s₂ tr₁ tr₂, making it the right combinator for stating composition theorems without visible casts.

theorem Interaction.Spec.Transcript.liftAppendRel_iff (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (F G : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (R : (tr₁ : s₁.Transcript) → (tr₂ : (s₂ tr₁).Transcript) → F tr₁ tr₂ → G tr₁ tr₂ → Prop) (tr : (s₁.append s₂).Transcript) (x : liftAppend s₁ s₂ F tr) (y : liftAppend s₁ s₂ G tr) : liftAppendRel s₁ s₂ F G R tr x y ↔ R (split s₁ s₂ tr).fst (split s₁ s₂ tr).snd (unliftAppend s₁ s₂ F tr x) (unliftAppend s₁ s₂ G tr y)

liftAppendRel is equivalent to applying R at the transcript pair recovered by split, via unliftAppend.

def Interaction.Spec.Transcript.liftAppendPred (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (F : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (P : (tr₁ : s₁.Transcript) → (tr₂ : (s₂ tr₁).Transcript) → F tr₁ tr₂ → Prop) (tr : (s₁.append s₂).Transcript) : liftAppend s₁ s₂ F tr → Prop

Lift a unary predicate on a pair-indexed type family to the fused transcript of s₁.append s₂. Reduces definitionally when the transcript is Transcript.append s₁ s₂ tr₁ tr₂.

theorem Interaction.Spec.Transcript.liftAppendPred_iff (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (F : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u) (P : (tr₁ : s₁.Transcript) → (tr₂ : (s₂ tr₁).Transcript) → F tr₁ tr₂ → Prop) (tr : (s₁.append s₂).Transcript) (x : liftAppend s₁ s₂ F tr) : liftAppendPred s₁ s₂ F P tr x ↔ P (split s₁ s₂ tr).fst (split s₁ s₂ tr).snd (unliftAppend s₁ s₂ F tr x)

liftAppendPred is equivalent to applying P at the transcript pair recovered by split, via unliftAppend.

theorem Interaction.Spec.append_done (s₂ : done.Transcript → Spec) : done.append s₂ = s₂ PUnit.unit

theorem Interaction.Spec.append_node (X : Type u) (rest : X → Spec) (s₂ : (node X rest).Transcript → Spec) : (node X rest).append s₂ = node X fun (x : X) => (rest x).append fun (p : (rest x).Transcript) => s₂ ⟨x, p⟩

def Interaction.Spec.Strategy.comp {m : Type u → Type u} [Monad m] (s₁ : Spec) (s₂ : s₁.Transcript → Spec) {Mid : s₁.Transcript → Type u} {F : (tr₁ : s₁.Transcript) → (s₂ tr₁).Transcript → Type u} : Strategy m s₁ Mid → ((tr₁ : s₁.Transcript) → Mid tr₁ → m (Strategy m (s₂ tr₁) (F tr₁))) → m (Strategy m (s₁.append s₂) (Transcript.liftAppend s₁ s₂ F))

Monadic composition of strategies along Spec.append.

The output type is given as a two-argument family F : Transcript s₁ → Transcript (s₂ tr₁) → Type u, lifted to the combined spec via Transcript.liftAppend. The continuation receives the first-phase strategy's output and produces a second-phase strategy whose output family is F tr₁.

This is the preferred composition form: liftAppend ensures the output type reduces definitionally when combined with Transcript.append, which is essential for dependent chain composition (see Strategy.stateChainComp).

def Interaction.Spec.Strategy.compFlat {m : Type u → Type u} [Monad m] (s₁ : Spec) (s₂ : s₁.Transcript → Spec) {Mid : s₁.Transcript → Type u} {Output : (s₁.append s₂).Transcript → Type u} : Strategy m s₁ Mid → ((tr₁ : s₁.Transcript) → Mid tr₁ → m (Strategy m (s₂ tr₁) fun (tr₂ : (s₂ tr₁).Transcript) => Output (Transcript.append s₁ s₂ tr₁ tr₂))) → m (Strategy m (s₁.append s₂) Output)

Monadic composition of strategies along Spec.append with a single output family Output on the combined transcript. The continuation indexes into Output via Transcript.append.

Use this when the output type is naturally expressed over the combined transcript rather than as a two-argument family (e.g., constant output types, or when working with Strategy.iterate). See also Strategy.comp.

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

Extract the first-phase 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.

def Interaction.Spec.Decoration.append {S : Type u → Type v} {s₁ : Spec} {s₂ : s₁.Transcript → Spec} (d₁ : Decoration S s₁) (d₂ : (tr₁ : s₁.Transcript) → Decoration S (s₂ tr₁)) : Decoration S (s₁.append s₂)

Concatenate per-node labels along Spec.append.

def Interaction.Spec.Decoration.Over.append {L : Type u → Type v} {F : (X : Type u) → L X → Type w} {s₁ : Spec} {s₂ : s₁.Transcript → Spec} {d₁ : Decoration L s₁} {d₂ : (tr₁ : s₁.Transcript) → Decoration L (s₂ tr₁)} (r₁ : Over F s₁ d₁) (r₂ : (tr₁ : s₁.Transcript) → Over F (s₂ tr₁) (d₂ tr₁)) : Over F (s₁.append s₂) (d₁.append d₂)

Concatenate dependent decoration layers along Spec.append, over appended base decorations.

theorem Interaction.Spec.Decoration.Over.map_append {L : Type u → Type v} {F G : (X : Type u) → L X → Type w} (η : (X : Type u) → (l : L X) → F X l → G X l) (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (d₁ : Decoration L s₁) (d₂ : (tr₁ : s₁.Transcript) → Decoration L (s₂ tr₁)) (r₁ : Over F s₁ d₁) (r₂ : (tr₁ : s₁.Transcript) → Over F (s₂ tr₁) (d₂ tr₁)) : map η (s₁.append s₂) (d₁.append d₂) (r₁.append r₂) = (map η s₁ d₁ r₁).append fun (tr₁ : s₁.Transcript) => map η (s₂ tr₁) (d₂ tr₁) (r₂ tr₁)

Decoration.Over.map commutes with Over.append.

theorem Interaction.Spec.Decoration.map_append {S : Type u → Type v} {T : Type u → Type w} (f : (X : Type u) → S X → T X) (s₁ : Spec) (s₂ : s₁.Transcript → Spec) (d₁ : Decoration S s₁) (d₂ : (tr₁ : s₁.Transcript) → Decoration S (s₂ tr₁)) : map f (s₁.append s₂) (d₁.append d₂) = (map f s₁ d₁).append fun (tr₁ : s₁.Transcript) => map f (s₂ tr₁) (d₂ tr₁)

Decoration.map commutes with Decoration.append.