Decorations and dependent decorations (Over)

Spec.Decoration Γ spec is concrete nodewise metadata attached to a fixed protocol tree spec, where Γ : Spec.Node.Context is the realized family of node-local information. If a node of spec has move space X, then a decoration provides one value of type Γ X at that node, and recursively decorates every continuation subtree.

This is the basic way to say "the same protocol tree, but with extra data at each node". Typical examples include:

• RoleDecoration, recording who controls a node;
• monad decorations, recording which monad a local action uses at a node;
• oracle decorations, recording what oracle interface is available there.

A context may be written directly, or obtained from a telescope Spec.Node.Schema via Spec.Node.Schema.toContext.

Decoration.Over is the dependent (displayed) variant: its fibers may depend on the context value drawn from an existing decoration.

Naming note: Decoration.Over is nested because it is literally a decoration over a fixed base decoration value. By contrast, ShapeOver and InteractionOver keep the suffix form because they are the primary generalized syntax and semantics layers, not dependent objects over a fixed base Shape or Interaction.

Functorial map / map_id / map_comp for both layers are in this file. Composition along Spec.append is in VCVio.Interaction.Basic.Append.

Because decorations are concrete tree data, they are covariant in node-local contexts: a context morphism Γ → Δ induces a map from decorations by Γ to decorations by Δ. The schema-facing API in Decoration.Schema packages that same idea for realized contexts presented by schemas via Spec.Node.Schema.SchemaMap.

This file also contains the bridge between the semantic and staged views of node metadata: decorating a tree by an extended context Γ.extend A is equivalent to giving a base decoration by Γ together with one dependent Decoration.Over A layer on top of it.

In particular, if a schema is built as (Spec.Node.Schema.singleton Γ).extend A, then Decoration.equivOver A spec is exactly the statement that a decoration of that schema's realized context is the same as a base decoration by Γ plus one displayed layer over it.

The file concludes by lifting this one-step bridge recursively to arbitrary schemas: Spec.Decoration.Schema.View is the staged telescope view of a decoration by S.toContext, and Spec.Decoration.Schema.equivView identifies that staged view with an ordinary decoration of the realized context.

Polynomial substrate (DecoratedSpec)

Just as Spec is PFunctor.FreeM Spec.basePFunctor PUnit, the bundle (spec, Decoration Γ spec) is PFunctor.FreeM (Γ.toPFunctor) PUnit:

DecoratedSpec Γ := PFunctor.FreeM (Γ.toPFunctor) PUnit

Γ.toPFunctor is the polynomial whose positions are Σ X : Type u, Γ X and whose child family is Sigma.fst. A free term over this polynomial is literally a tree where every internal node carries both a move space X and a Γ-value, with continuations indexed by the move type.

Forgetting the Γ-component on positions yields a polynomial lens Γ.toPFunctor → Spec.basePFunctor, whose lift to free monads is the shape-forgetful map DecoratedSpec.shape : DecoratedSpec Γ → Spec. The fiber of shape over a fixed spec : Spec is exactly Decoration Γ spec, formalized as decoratedSpecEquiv : DecoratedSpec Γ ≃ Σ spec, Decoration Γ spec.

This makes precise the slogan "a Γ-decorated spec is the same data as a spec together with a Γ-decoration on it". Downstream code can use either view: the Spec-indexed Decoration family is convenient for talking about decorations over a fixed protocol, while DecoratedSpec is the right object when shape and metadata vary together (e.g. for the polynomial coalgebraic semantics of ProcessOver).

def Interaction.Spec.Decoration (Γ : Node.Context) : Spec → Type (max u v)

Decoration Γ spec is concrete nodewise metadata on the fixed protocol tree spec, for a realized node context Γ.

If a node of spec has move space X, then the decoration stores one value of type Γ X at that node, and recursively stores decorations on every subtree.

This is different from Spec.SyntaxOver:

• a decoration is data on a tree;
• syntax is a specification of local participant objects that consumes such data;
• Spec.ShapeOver is the functorial refinement of that syntax layer.

def Interaction.Spec.Decoration.map {Γ : Node.Context} {Δ : Node.Context} (f : Node.ContextHom Γ Δ) (spec : Spec) : Decoration Γ spec → Decoration Δ spec

Natural transformation between per-node decorations, applied recursively.

@[simp]

theorem Interaction.Spec.Decoration.map_id {Γ : Node.Context} (spec : Spec) (d : Decoration Γ spec) : map (Node.ContextHom.id Γ) spec d = d

theorem Interaction.Spec.Decoration.map_comp {Γ : Node.Context} {Δ : Node.Context} {Λ : Node.Context} (g : Node.ContextHom Δ Λ) (f : Node.ContextHom Γ Δ) (spec : Spec) (d : Decoration Γ spec) : map g spec (map f spec d) = map (g.comp f) spec d

def Interaction.Spec.Decoration.Over {Γ : Node.Context} (F : (X : Type u) → Γ X → Type w) (spec : Spec) : Decoration Γ spec → Type (max u w)

Dependent decoration over d : Decoration Γ spec: at each node, data in F X γ where γ is the context value from d, plus recursive decorations on subtrees.

def Interaction.Spec.Decoration.Over.map {Γ : Node.Context} {F G : (X : Type u) → Γ X → Type w} (f : (X : Type u) → (γ : Γ X) → F X γ → G X γ) (spec : Spec) (d : Decoration Γ spec) : Over F spec d → Over G spec d

Fiberwise map between dependent decoration families over the same base decoration.

@[simp]

theorem Interaction.Spec.Decoration.Over.map_id {Γ : Node.Context} {F : (X : Type u) → Γ X → Type w} (spec : Spec) (d : Decoration Γ spec) (r : Over F spec d) : map (fun (x : Type u) (x_1 : Γ x) (x_2 : F x x_1) => x_2) spec d r = r

theorem Interaction.Spec.Decoration.Over.map_comp {Γ : Node.Context} {F G H : (X : Type u) → Γ X → Type w} (g : (X : Type u) → (γ : Γ X) → G X γ → H X γ) (f : (X : Type u) → (γ : Γ X) → F X γ → G X γ) (spec : Spec) (d : Decoration Γ spec) (r : Over F spec d) : map g spec d (map f spec d r) = map (fun (X : Type u) (γ : Γ X) => g X γ ∘ f X γ) spec d r

def Interaction.Spec.Decoration.Over.mapBase {Γ : Node.Context} {Δ : Node.Context} {A : (X : Type u) → Γ X → Type w₂} {B : (X : Type u) → Δ X → Type w₂} (f : Node.ContextHom Γ Δ) (g : (X : Type u) → (γ : Γ X) → A X γ → B X (f X γ)) (spec : Spec) (d : Decoration Γ spec) : Over A spec d → Over B spec (Decoration.map f spec d)

Transport a dependent decoration across a map of base contexts.

Given:

• a base-context morphism f : Γ → Δ, and
• a fiberwise map g from A X γ to B X (f X γ),

this sends a displayed decoration over d : Decoration Γ spec to a displayed decoration over Decoration.map f spec d.

theorem Interaction.Spec.Decoration.Over.mapBase_id {Γ : Node.Context} {A : (X : Type u) → Γ X → Type w} (spec : Spec) (d : Decoration Γ spec) (r : Over A spec d) : mapBase (Node.ContextHom.id Γ) (fun (x : Type u) (x_1 : Γ x) (x_2 : A x x_1) => x_2) spec d r ≍ r

theorem Interaction.Spec.Decoration.Over.mapBase_comp {Γ : Node.Context} {Δ : Node.Context} {Λ : Node.Context} {A : (X : Type u) → Γ X → Type w₂} {B : (X : Type u) → Δ X → Type w₂} {C : (X : Type u) → Λ X → Type w₂} (f : Node.ContextHom Γ Δ) (g : Node.ContextHom Δ Λ) (fOver : (X : Type u) → (γ : Γ X) → A X γ → B X (f X γ)) (gOver : (X : Type u) → (δ : Δ X) → B X δ → C X (g X δ)) (spec : Spec) (d : Decoration Γ spec) (r : Over A spec d) : mapBase g gOver spec (Decoration.map f spec d) (mapBase f fOver spec d r) ≍ mapBase (g.comp f) (fun (X : Type u) (γ : Γ X) => gOver X (f X γ) ∘ fOver X γ) spec d r

def Interaction.Spec.Decoration.ofOver {Γ : Node.Context} (A : (X : Type u) → Γ X → Type w) (spec : Spec) (d : Decoration Γ spec) : Over A spec d → Decoration (Node.Context.extend Γ A) spec

Pack a base decoration and one dependent Over layer into a decoration of the extended context Γ.extend A.

This is the tree-level realization of a single schema extension step.

theorem Interaction.Spec.Decoration.map_ofOver {Γ : Node.Context} {Δ : Node.Context} {A : (X : Type u) → Γ X → Type w₂} {B : (X : Type u) → Δ X → Type w₂} (f : Node.ContextHom Γ Δ) (g : (X : Type u) → (γ : Γ X) → A X γ → B X (f X γ)) (spec : Spec) (d : Decoration Γ spec) (r : Over A spec d) : map (Node.Context.extendMap f g) spec (ofOver A spec d r) = ofOver B spec (map f spec d) (Over.mapBase f g spec d r)

def Interaction.Spec.Decoration.toOver {Γ : Node.Context} (A : (X : Type u) → Γ X → Type w) (spec : Spec) : Decoration (Node.Context.extend Γ A) spec → (d : Decoration Γ spec) × Over A spec d

Unpack a decoration of the extended context Γ.extend A into:

• its base decoration by Γ, and
• its displayed Decoration.Over A layer above that base.

This is the inverse structural view to Decoration.ofOver.

@[simp]

theorem Interaction.Spec.Decoration.toOver_ofOver {Γ : Node.Context} (A : (X : Type u) → Γ X → Type w) (spec : Spec) (d : Decoration Γ spec) (r : Over A spec d) : toOver A spec (ofOver A spec d r) = ⟨d, r⟩

@[simp]

theorem Interaction.Spec.Decoration.ofOver_toOver {Γ : Node.Context} (A : (X : Type u) → Γ X → Type w) (spec : Spec) (d : Decoration (Node.Context.extend Γ A) spec) : ofOver A spec (toOver A spec d).fst (toOver A spec d).snd = d

def Interaction.Spec.Decoration.equivOver {Γ : Node.Context} (A : (X : Type u) → Γ X → Type w) (spec : Spec) : Decoration (Node.Context.extend Γ A) spec ≃ (d : Decoration Γ spec) × Over A spec d

Equivalence between:

• decorating a tree by the extended context Γ.extend A, and
• decorating it by Γ together with one Decoration.Over A layer.

This is the main bridge from the semantic "single realized context" view to the staged schema/dependent-decoration view.

Concrete example: if a schema is built as (Spec.Node.Schema.singleton Tag).extend Data, then decorations of its realized context Node.Context.extend Tag Data are equivalent to pairs consisting of:

• tags : Decoration Tag spec, and
• datas : Decoration.Over Data spec tags.

Polynomial substrate DecoratedSpec

A DecoratedSpec Γ is the free term of the polynomial Γ.toPFunctor at the unit payload: a tree where every internal node carries both its move space X and a Γ-value of type Γ X, with continuations indexed by X.

This is the polynomial substrate that justifies the Spec-indexed family Decoration Γ spec: forgetting the Γ-component on positions yields a polynomial lens Γ.toPFunctor → Spec.basePFunctor whose lift to free monads gives DecoratedSpec.shape. The fiber of shape over a fixed spec is exactly Decoration Γ spec, witnessed by decoratedSpecEquiv.

def Interaction.Spec.DecoratedSpec (Γ : Node.Context) : Type (max (u + 1) v)

A Γ-decorated interaction spec, viewed polynomially.

This is the free monad on Γ.toPFunctor at the unit payload. Equivalently (by decoratedSpecEquiv), it bundles a tree shape spec : Spec together with a Decoration Γ spec on it.

def Interaction.Spec.DecoratedSpec.shape {Γ : Node.Context} : DecoratedSpec Γ → Spec

Forget the Γ-component on every position, leaving only the underlying tree shape. This is the lift to free monads of the polynomial lens Γ.toPFunctor → Spec.basePFunctor whose position map is Sigma.fst and whose child map is the identity.

def Interaction.Spec.DecoratedSpec.decoration {Γ : Node.Context} (ds : DecoratedSpec Γ) : Decoration Γ ds.shape

Read off the per-node Γ-decoration of a decorated spec, indexed by the spec's underlying shape. Together with shape, this exhibits the fiberwise structure of DecoratedSpec Γ over Spec.

def Interaction.Spec.DecoratedSpec.mk {Γ : Node.Context} (spec : Spec) : Decoration Γ spec → DecoratedSpec Γ

Pack a tree shape together with a Γ-decoration on it into a single decorated spec. Inverse to the pair (shape, decoration).

@[simp]

theorem Interaction.Spec.DecoratedSpec.shape_mk {Γ : Node.Context} (spec : Spec) (d : Decoration Γ spec) : (mk spec d).shape = spec

theorem Interaction.Spec.DecoratedSpec.decoration_mk {Γ : Node.Context} (spec : Spec) (d : Decoration Γ spec) : (mk spec d).decoration ≍ d

@[simp]

theorem Interaction.Spec.DecoratedSpec.mk_shape_decoration {Γ : Node.Context} (ds : DecoratedSpec Γ) : mk ds.shape ds.decoration = ds

def Interaction.Spec.decoratedSpecEquiv {Γ : Node.Context} : DecoratedSpec Γ ≃ (spec : Spec) × Decoration Γ spec

The polynomial substrate equivalence: a Γ-decorated spec is the same data as a tree shape together with a Γ-decoration on it.

This is the Spec-indexed fiberwise view of DecoratedSpec Γ. The forward direction takes (shape, decoration); the backward direction is mk.

@[reducible, inline]

abbrev Interaction.Spec.Decoration.Schema.map {Γ Δ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} (f : S.SchemaMap T) (spec : Spec) : Decoration S.toContext spec → Decoration T.toContext spec

Map decorations along a schema morphism.

This is just Decoration.map viewed through schema-level sources and targets.

@[simp]

theorem Interaction.Spec.Decoration.Schema.map_id {Γ : Node.Context} {S : Node.Schema Γ} (spec : Spec) (d : Decoration S.toContext spec) : map (Node.Schema.SchemaMap.id S) spec d = d

theorem Interaction.Spec.Decoration.Schema.map_comp {Γ Δ Λ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} {U : Node.Schema Λ} (g : T.SchemaMap U) (f : S.SchemaMap T) (spec : Spec) (d : Decoration S.toContext spec) : map g spec (map f spec d) = map (g.comp f) spec d

theorem Interaction.Spec.Decoration.Schema.map_ofOver {Γ Δ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} {A : (X : Type u) → Γ X → Type v} {B : (X : Type u) → Δ X → Type v} (f : S.SchemaMap T) (g : (X : Type u) → (γ : Γ X) → A X γ → B X (f X γ)) (spec : Spec) (d : Decoration Γ spec) (r : Over A spec d) : map (f.extend g) spec (ofOver A spec d r) = ofOver B spec (map f spec d) (Over.mapBase f g spec d r)

def Interaction.Spec.Decoration.Schema.telescope {Γ : Node.Context} (S : Node.Schema Γ) (spec : Spec) : (T : Type (max u v)) × (Decoration Γ spec ≃ T)

Decoration.Schema.telescope S spec packages the staged telescope view of decorations for schema S, together with an equivalence from ordinary decorations by the realized context S.toContext.

The resulting type is the recursively decomposed form of a decoration: each snoc in the schema contributes one more displayed Decoration.Over layer.

@[reducible, inline]

abbrev Interaction.Spec.Decoration.Schema.View {Γ : Node.Context} (S : Node.Schema Γ) (spec : Spec) : Type (max u v)

Decoration.Schema.View S spec is the staged telescope view carried by the recursive schema decomposition theorem Decoration.Schema.telescope.

@[reducible, inline]

abbrev Interaction.Spec.Decoration.Schema.unpack {Γ : Node.Context} (S : Node.Schema Γ) (spec : Spec) : Decoration Γ spec → View S spec

Unpack an ordinary decoration into the staged telescope view determined by a schema.

@[reducible, inline]

abbrev Interaction.Spec.Decoration.Schema.pack {Γ : Node.Context} (S : Node.Schema Γ) (spec : Spec) : View S spec → Decoration Γ spec

Pack a staged schema-decoration view back into an ordinary decoration of the realized context.

@[simp]

theorem Interaction.Spec.Decoration.Schema.pack_unpack {Γ : Node.Context} (S : Node.Schema Γ) (spec : Spec) (d : Decoration Γ spec) : pack S spec (unpack S spec d) = d

@[simp]

theorem Interaction.Spec.Decoration.Schema.unpack_pack {Γ : Node.Context} (S : Node.Schema Γ) (spec : Spec) (d : View S spec) : unpack S spec (pack S spec d) = d

@[reducible, inline]

abbrev Interaction.Spec.Decoration.Schema.mapView {Γ Δ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} (f : S.SchemaMap T) (spec : Spec) : View S spec → View T spec

Map the staged telescope view of decorations along a schema morphism.

This is the schema-view analogue of Decoration.Schema.map: pack the staged view into an ordinary decoration, map that decoration along the schema morphism, then unpack it into the staged view for the target schema.

@[simp]

theorem Interaction.Spec.Decoration.Schema.unpack_map {Γ Δ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} (f : S.SchemaMap T) (spec : Spec) (d : Decoration S.toContext spec) : unpack T spec (map f spec d) = mapView f spec (unpack S spec d)

@[simp]

theorem Interaction.Spec.Decoration.Schema.pack_mapView {Γ Δ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} (f : S.SchemaMap T) (spec : Spec) (d : View S spec) : pack T spec (mapView f spec d) = map f spec (pack S spec d)

@[simp]

theorem Interaction.Spec.Decoration.Schema.mapView_id {Γ : Node.Context} {S : Node.Schema Γ} (spec : Spec) (d : View S spec) : mapView (Node.Schema.SchemaMap.id S) spec d = d

theorem Interaction.Spec.Decoration.Schema.mapView_comp {Γ Δ Λ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} {U : Node.Schema Λ} (g : T.SchemaMap U) (f : S.SchemaMap T) (spec : Spec) (d : View S spec) : mapView g spec (mapView f spec d) = mapView (g.comp f) spec d

@[reducible, inline]

abbrev Interaction.Spec.Decoration.Schema.Prefix.map {Γ Δ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} (p : S.Prefix T) (spec : Spec) : Decoration T.toContext spec → Decoration S.toContext spec

Project decorations along a syntactic schema prefix.

This is the tree-level forgetting map induced by the schema morphism Node.Schema.Prefix.toSchemaMap.

@[reducible, inline]

abbrev Interaction.Spec.Decoration.Schema.equivView {Γ : Node.Context} (S : Node.Schema Γ) (spec : Spec) : Decoration Γ spec ≃ View S spec

Equivalence between an ordinary decoration by the realized context of S and its staged telescope view.

This is the recursive schema-level form of Decoration.equivOver.