Documentation

VCVio.Interaction.TwoParty.Decoration

Role decorations and common role-based node contexts #

A RoleDecoration spec is a Spec.Decoration with fiber fun _ => Role: each internal node is labeled sender or receiver. This replaces a separate two-party interaction inductive while reusing all Spec infrastructure (Transcript, append, etc.).

This file also packages the most common role-based node contexts used by the two-party interaction layer:

Only the plain role layer is exposed as a schema here. The monadic extensions are exported as realized node contexts, because BundledMonad lives in a higher universe than Role, while Spec.Node.Schema currently uses one fixed universe for all staged fields.

These are the outward-facing schema/context names used by Strategy.withRolesAndMonads, Counterpart.withMonads, and the monadic execution layer.

source
@[reducible, inline]
abbrev Interaction.RoleContext :
Spec.Node.Context

The plain role-labeled node context.

Instances For
    source
    @[reducible, inline]
    abbrev Interaction.RoleSchema :
    Spec.Node.Schema RoleContext

    The singleton schema presenting RoleContext.

    Instances For
      source
      @[reducible, inline]
      abbrev Interaction.RoleMonadContext :
      Spec.Node.Context

      Role context extended by one bundled monad field.

      Instances For
        source
        @[reducible, inline]
        abbrev Interaction.RolePairedMonadContext :
        Spec.Node.Context

        Role context extended by a pair of bundled monads.

        Instances For
          source
          @[reducible, inline]
          abbrev Interaction.RolePairedMonadContext.fst :
          Spec.Node.ContextHom RolePairedMonadContext RoleMonadContext

          Forget the counterpart monad from a paired role/monad context.

          Instances For
            source
            @[reducible, inline]
            abbrev Interaction.RolePairedMonadContext.snd :
            Spec.Node.ContextHom RolePairedMonadContext RoleMonadContext

            Forget the focal monad from a paired role/monad context.

            Instances For
              source
              @[reducible, inline]
              abbrev Interaction.RoleDecoration :
              Spec → Type u_1

              Per-node sender/receiver assignment on a Spec.

              Instances For
                source
                def Interaction.Spec.Decoration.swap {spec : Spec} (roles : Decoration (fun (x : Type u_1) => Role) spec) :
                Decoration (fun (x : Type u_1) => Role) spec

                Swap sender ↔ receiver at each node.

                Because RoleDecoration is an abbrev of Decoration (fun _ => Role), dot notation on roles : RoleDecoration spec resolves this Spec.Decoration.swap.

                Instances For
                  source
                  def Interaction.RoleDecoration.monadsOver (spec : Spec) (roles : RoleDecoration spec) (md : spec.MonadDecoration) :
                  Spec.Decoration.Over (fun (x : Type u) (x_1 : Role) => BundledMonad) spec roles

                  View a plain monad decoration as one displayed layer over an existing role decoration.

                  Instances For
                    source
                    def Interaction.RoleDecoration.withMonads {spec : Spec} (roles : RoleDecoration spec) (md : spec.MonadDecoration) :
                    Spec.Decoration RoleMonadContext spec

                    Pack roles together with one bundled monad per node into RoleMonadContext.

                    Instances For
                      source
                      def Interaction.RoleDecoration.pairedMonadsOver (spec : Spec) (roles : RoleDecoration spec) (stratDeco cptDeco : spec.MonadDecoration) :
                      Spec.Decoration.Over (fun (x : Type u) (x_1 : Role) => BundledMonad × BundledMonad) spec roles

                      View a pair of monad decorations as one displayed layer over an existing role decoration.

                      Instances For
                        source
                        def Interaction.RoleDecoration.withPairedMonads {spec : Spec} (roles : RoleDecoration spec) (stratDeco cptDeco : spec.MonadDecoration) :
                        Spec.Decoration RolePairedMonadContext spec

                        Pack roles together with paired prover/counterpart monads into RolePairedMonadContext.

                        Instances For
                          source
                          @[simp]
                          theorem Interaction.RoleDecoration.withPairedMonads_map_fst {spec : Spec} {roles : RoleDecoration spec} {stratDeco cptDeco : spec.MonadDecoration} :
                          Spec.Decoration.map RolePairedMonadContext.fst spec (roles.withPairedMonads stratDeco cptDeco) = roles.withMonads stratDeco
                          source
                          @[simp]
                          theorem Interaction.RoleDecoration.withPairedMonads_map_snd {spec : Spec} {roles : RoleDecoration spec} {stratDeco cptDeco : spec.MonadDecoration} :
                          Spec.Decoration.map RolePairedMonadContext.snd spec (roles.withPairedMonads stratDeco cptDeco) = roles.withMonads cptDeco