Role-dependent strategies and counterparts

Spec.Strategy.withRoles is the prover / focal party: owned nodes are effectful move/continuation packages, while non-owned nodes respond to the other party's move. Spec.Counterpart is the dual type. withRolesAndMonads and runWithRolesAndMonads extend this with per-node BundledMonad data from MonadDecoration.

This module also contains the public-coin specialization needed for verifier-side Fiat-Shamir. The ordinary Counterpart type is the right shape for execution, but at receiver nodes it hides the continuation behind an opaque monadic sample. Spec.PublicCoinCounterpart refines that node shape to expose:

• sample : m X — how the next public challenge is chosen
• next : (x : X) → ... — how the rest of the verifier depends on that challenge

This makes transcript replay definable without changing the core two-party interaction model.

inductive Interaction.Spec.ParticipantBase : Type

• focal : ParticipantBase
• counterpart : ParticipantBase

@[implicit_reducible]

instance Interaction.Spec.instDecidableEqParticipantBase : DecidableEq ParticipantBase

structure Interaction.Spec.Participant : Type u

• tag : ParticipantBase
• lift : ULift PUnit

def Interaction.Spec.instDecidableEqParticipant.decEq (x✝ x✝¹ : Participant) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Interaction.Spec.instDecidableEqParticipant : DecidableEq Participant

def Interaction.Spec.Participant.focal : Participant

def Interaction.Spec.Participant.counterpart : Participant

def Interaction.Spec.pairedSyntax (m : Type u → Type u) : SyntaxOver Participant fun (x : Type u) => Role

def Interaction.Spec.pairedMonadicSyntax : SyntaxOver Participant RolePairedMonadContext

@[reducible, inline]

abbrev Interaction.Spec.Strategy.withRoles (m : Type u → Type u) (spec : Spec) (roles : RoleDecoration spec) (Output : spec.Transcript → Type u) : Type u

Focal strategy: Role.Action at each decorated node (choose vs. respond).

@[simp]

theorem Interaction.Spec.Strategy.withRoles_done {m : Type u → Type u} {Output : PUnit → Type u} : withRoles m done PUnit.unit Output = Output PUnit.unit

@[simp]

theorem Interaction.Spec.Strategy.withRoles_sender_eq {m : Type u → Type u} {X : Type u} {rest : X → Spec} {rRest : (x : X) → RoleDecoration (rest x)} {Output : (node X rest).Transcript → Type u} : withRoles m (node X rest) (Role.sender, rRest) Output = m ((x : X) × withRoles m (rest x) (rRest x) fun (tr : (rest x).Transcript) => Output ⟨x, tr⟩)

@[simp]

theorem Interaction.Spec.Strategy.withRoles_receiver_eq {m : Type u → Type u} {X : Type u} {rest : X → Spec} {rRest : (x : X) → RoleDecoration (rest x)} {Output : (node X rest).Transcript → Type u} : withRoles m (node X rest) (Role.receiver, rRest) Output = ((x : X) → m (withRoles m (rest x) (rRest x) fun (tr : (rest x).Transcript) => Output ⟨x, tr⟩))

@[reducible, inline]

abbrev Interaction.Spec.CounterpartFamily (Sender Receiver : (X : Type u) → (X → Type u) → Type u) (spec : Spec) (roles : RoleDecoration spec) (Output : spec.Transcript → Type u) : Type u

A generic counterpart family parameterized by separate sender- and receiver-side node representations.

Sender nodes model how the environment follows a move chosen by the focal party. Receiver nodes model how the environment chooses a move itself. Both ordinary Counterpart and replayable PublicCoinCounterpart are specializations of this single recursion.

def Interaction.Spec.CounterpartFamily.mapOutput (Sender Receiver : (X : Type u) → (X → Type u) → Type u) (mapSender : {X : Type u} → {A B : X → Type u} → ((x : X) → A x → B x) → Sender X A → Sender X B) (mapReceiver : {X : Type u} → {A B : X → Type u} → ((x : X) → A x → B x) → Receiver X A → Receiver X B) {spec : Spec} {roles : RoleDecoration spec} {A B : spec.Transcript → Type u} : ((tr : spec.Transcript) → A tr → B tr) → CounterpartFamily Sender Receiver spec roles A → CounterpartFamily Sender Receiver spec roles B

@[reducible, inline]

abbrev Interaction.Spec.Counterpart (m : Type u → Type u) (spec : Spec) (roles : RoleDecoration spec) (Output : spec.Transcript → Type u) : Type u

Counterpart / environment type with transcript-dependent output: dual actions at each node, producing Output ⟨⟩ at .done. For a no-output counterpart (the old behavior), use Counterpart m spec roles (fun _ => PUnit).

def Interaction.Spec.Counterpart.mapReceiver {m : Type u → Type u} [Functor m] {X : Type u} {A B : X → Type u} : ((x : X) → A x → B x) → m ((x : X) × A x) → m ((x : X) × B x)

Map a receiver-family output through a sender-owned sampled move.

def Interaction.Spec.Counterpart.mapSender {m : Type u → Type u} [Functor m] {X : Type u} {A B : X → Type u} : ((x : X) → A x → B x) → ((x : X) → m (A x)) → (x : X) → m (B x)

Map outputs through an effectful sender-side observation.

def Interaction.Spec.Strategy.mapOutputWithRoles {m : Type u → Type u} [Functor m] {spec : Spec} {roles : RoleDecoration spec} {A B : spec.Transcript → Type u} : ((tr : spec.Transcript) → A tr → B tr) → withRoles m spec roles A → withRoles m spec roles B

Functorial output map for role-dependent strategies.

@[simp]

theorem Interaction.Spec.Strategy.mapOutputWithRoles_id {m : Type u → Type u} [Functor m] [LawfulFunctor m] {spec : Spec} {roles : RoleDecoration spec} {A : spec.Transcript → Type u} (σ : withRoles m spec roles A) : mapOutputWithRoles (fun (x : spec.Transcript) (x_1 : A x) => x_1) σ = σ

Pointwise identity on outputs is the identity on role-dependent strategies.

def Interaction.Spec.Counterpart.mapOutput {m : Type u → Type u} [Functor m] {spec : Spec} {roles : RoleDecoration spec} {A B : spec.Transcript → Type u} : ((tr : spec.Transcript) → A tr → B tr) → Counterpart m spec roles A → Counterpart m spec roles B

Functorial output map for counterparts.

@[reducible, inline]

abbrev Interaction.Spec.PublicCoinCounterpart (m : Type u → Type u) (spec : Spec) (roles : RoleDecoration spec) (Output : spec.Transcript → Type u) : Type u

A verifier counterpart with replayable public-coin receiver nodes.

An ordinary Counterpart m represents a receiver node as an opaque monadic action returning both the sampled challenge and the continuation. That is the right shape for execution, but it is too weak for verifier-side Fiat-Shamir: given a prescribed challenge x, there is no way to recover the continuation for x unless that continuation is exposed separately.

PublicCoinCounterpart factors each receiver node into:

• sample : m X — how the verifier samples the next public challenge
• next : (x : X) → ... — how the rest of the verifier depends on that challenge

This is exactly the extra structure needed to replay a prescribed transcript through the verifier.

def Interaction.Spec.PublicCoinCounterpart.mapOutput {m : Type u → Type u} [Functor m] {spec : Spec} {roles : RoleDecoration spec} {A B : spec.Transcript → Type u} : ((tr : spec.Transcript) → A tr → B tr) → PublicCoinCounterpart m spec roles A → PublicCoinCounterpart m spec roles B

Functorial output map for public-coin counterparts. The challenge samplers are unchanged; only the terminal output carried by continuations is mapped.

def Interaction.Spec.PublicCoinCounterpart.toCounterpart {m : Type u → Type u} [Monad m] {spec : Spec} {roles : RoleDecoration spec} {Output : spec.Transcript → Type u} : PublicCoinCounterpart m spec roles Output → Counterpart m spec roles Output

Forget the public-coin factorization and recover the ordinary executable counterpart.

def Interaction.Spec.PublicCoinCounterpart.replay {m : Type u → Type u} [Monad m] {spec : Spec} {roles : RoleDecoration spec} {Output : spec.Transcript → Type u} : PublicCoinCounterpart m spec roles Output → (tr : spec.Transcript) → m (Output tr)

Replay a prescribed transcript through a public-coin counterpart. Sender messages are read from the transcript; receiver samplers are ignored and the stored continuation family is followed at the recorded challenge.

@[simp]

theorem Interaction.Spec.Counterpart.mapOutput_id {m : Type u → Type u} [Functor m] [LawfulFunctor m] {spec : Spec} {roles : RoleDecoration spec} {A : spec.Transcript → Type u} (c : Counterpart m spec roles A) : mapOutput (fun (x : spec.Transcript) (x_1 : A x) => x_1) c = c

Pointwise identity on outputs is the identity on counterparts.

def Interaction.Spec.Counterpart.liftId {m : Type u → Type u} [Monad m] {spec : Spec} {roles : RoleDecoration spec} {Output : spec.Transcript → Type u} : Counterpart Id spec roles Output → Counterpart m spec roles Output

Lift a deterministic counterpart (Counterpart Id) into any monad.

At sender nodes the observational branch structure is unchanged. At receiver nodes the chosen move and continuation are simply wrapped in pure. This is a generic utility for reusing deterministic environments inside monadic execution machinery such as runWithRoles.

def Interaction.Spec.Strategy.runWithRoles {m : Type u → Type u} [Monad m] (spec : Spec) (roles : RoleDecoration spec) {OutputP OutputC : spec.Transcript → Type u} : withRoles m spec roles OutputP → Counterpart m spec roles OutputC → m ((tr : spec.Transcript) × OutputP tr × OutputC tr)

Execute withRoles against a Counterpart, producing transcript, prover output, and counterpart output.

@[simp]

theorem Interaction.Spec.Strategy.runWithRoles_done {m : Type u → Type u} [Monad m] {OutputP OutputC : done.Transcript → Type u} (outP : OutputP PUnit.unit) (outC : OutputC PUnit.unit) : runWithRoles done PUnit.unit outP outC = pure ⟨PUnit.unit, (outP, outC)⟩

@[simp]

theorem Interaction.Spec.Strategy.runWithRoles_sender {m : Type u → Type u} [Monad m] {X : Type u} {rest : X → Spec} {rRest : (x : X) → RoleDecoration (rest x)} {OutputP OutputC : (node X rest).Transcript → Type u} (send : m ((x : X) × withRoles m (rest x) (rRest x) fun (tr : (rest x).Transcript) => OutputP ⟨x, tr⟩)) (dualFn : (x : X) → m (Counterpart m (rest x) (rRest x) fun (tr : (rest x).Transcript) => OutputC ⟨x, tr⟩)) : runWithRoles (node X rest) (Role.sender, rRest) send dualFn = do let __discr ← send match __discr with | ⟨x, next⟩ => do let dualNext ← dualFn x let __discr ← runWithRoles (rest x) (rRest x) next dualNext match __discr with | ⟨tail, (outP, outC)⟩ => pure ⟨⟨x, tail⟩, (outP, outC)⟩

@[simp]

theorem Interaction.Spec.Strategy.runWithRoles_receiver {m : Type u → Type u} [Monad m] {X : Type u} {rest : X → Spec} {rRest : (x : X) → RoleDecoration (rest x)} {OutputP OutputC : (node X rest).Transcript → Type u} (respond : (x : X) → m (withRoles m (rest x) (rRest x) fun (tr : (rest x).Transcript) => OutputP ⟨x, tr⟩)) (dualSample : m ((x : X) × Counterpart m (rest x) (rRest x) fun (tr : (rest x).Transcript) => OutputC ⟨x, tr⟩)) : runWithRoles (node X rest) (Role.receiver, rRest) respond dualSample = do let __discr ← dualSample match __discr with | ⟨x, dualRest⟩ => do let next ← respond x let __discr ← runWithRoles (rest x) (rRest x) next dualRest match __discr with | ⟨tail, (outP, outC)⟩ => pure ⟨⟨x, tail⟩, (outP, outC)⟩

theorem Interaction.Spec.Strategy.runWithRoles_mapOutputWithRoles_mapOutput {m : Type u → Type u} [Monad m] [LawfulMonad m] {spec : Spec} {roles : RoleDecoration spec} {OutputP OutputP' OutputC OutputC' : spec.Transcript → Type u} (fP : (tr : spec.Transcript) → OutputP tr → OutputP' tr) (fC : (tr : spec.Transcript) → OutputC tr → OutputC' tr) (strat : withRoles m spec roles OutputP) (cpt : Counterpart m spec roles OutputC) : runWithRoles spec roles (mapOutputWithRoles fP strat) (Counterpart.mapOutput fC cpt) = (fun (z : (tr : spec.Transcript) × OutputP tr × OutputC tr) => ⟨z.fst, (fP z.fst z.snd.fst, fC z.fst z.snd.snd)⟩) <$> runWithRoles spec roles strat cpt

Running runWithRoles after mapping both participant outputs is the same as running first and mapping the final triple.

theorem Interaction.Spec.Strategy.runWithRoles_mapOutputWithRoles_mapOutput.go {m : Type u → Type u} [Monad m] [LawfulMonad m] (spec : Spec) (roles : RoleDecoration spec) {OutputP OutputP' OutputC OutputC' : spec.Transcript → Type u} (fP : (tr : spec.Transcript) → OutputP tr → OutputP' tr) (fC : (tr : spec.Transcript) → OutputC tr → OutputC' tr) (strat : withRoles m spec roles OutputP) (cpt : Counterpart m spec roles OutputC) : runWithRoles spec roles (mapOutputWithRoles fP strat) (Counterpart.mapOutput fC cpt) = (fun (z : (tr : spec.Transcript) × OutputP tr × OutputC tr) => ⟨z.fst, (fP z.fst z.snd.fst, fC z.fst z.snd.snd)⟩) <$> runWithRoles spec roles strat cpt

@[reducible, inline]

abbrev Interaction.Spec.Strategy.withRolesAndMonads (spec : Spec) (roles : RoleDecoration spec) (md : spec.MonadDecoration) (Output : spec.Transcript → Type u) : Type u

withRoles using the monad attached at each node (from MonadDecoration). See Counterpart.withMonads for the dual.

@[reducible, inline]

abbrev Interaction.Spec.Counterpart.withMonads (spec : Spec) (roles : RoleDecoration spec) (md : spec.MonadDecoration) (Output : spec.Transcript → Type u) : Type u

Counterpart with per-node monads and transcript-dependent output.

This is the primary type for oracle verifiers: OracleCounterpart (in Oracle/Core.lean) is defined as Counterpart.withMonads with a MonadDecoration computed from the oracle decoration via toMonadDecoration. At sender nodes the monad is Id (pure observation); at receiver nodes it is OracleComp with the accumulated oracle access. All generic Counterpart.withMonads composition combinators (e.g., withMonads.append, withMonads.stateChainComp) therefore apply directly to oracle counterparts.

def Interaction.Spec.Counterpart.withMonads.mapOutput (spec : Spec) (roles : RoleDecoration spec) (md : spec.MonadDecoration) {Output₁ Output₂ : spec.Transcript → Type u} (f : (tr : spec.Transcript) → Output₁ tr → Output₂ tr) : withMonads spec roles md Output₁ → withMonads spec roles md Output₂

Map the transcript-indexed output of a monadic counterpart. This is the counterpart-side analog of Strategy.mapOutputWithRoles, specialized to Counterpart.withMonads.

@[simp]

theorem Interaction.Spec.Counterpart.withMonads.mapOutput_done {Output₁ Output₂ : PUnit → Type u} (md : PUnit) (f : (tr : PUnit) → Output₁ tr → Output₂ tr) (cpt : withMonads done PUnit.unit md Output₁) : mapOutput done PUnit.unit md f cpt = f PUnit.unit cpt

@[simp]

theorem Interaction.Spec.Counterpart.withMonads.mapOutput_sender_eq {X : Type u} {rest : X → Spec} {rRest : (x : X) → RoleDecoration (rest x)} {bm : BundledMonad} {mdRest : (x : X) → (rest x).MonadDecoration} {Output₁ Output₂ : (node X rest).Transcript → Type u} (f : (tr : (node X rest).Transcript) → Output₁ tr → Output₂ tr) (cpt : withMonads (node X rest) (Role.sender, rRest) (bm, mdRest) Output₁) : mapOutput (node X rest) (Role.sender, rRest) (bm, mdRest) f cpt = fun (x : X) => (mapOutput (rest x) (rRest x) (mdRest x) fun (tr : (rest x).Transcript) => f ⟨x, tr⟩) <$> cpt x

@[simp]

theorem Interaction.Spec.Counterpart.withMonads.mapOutput_receiver_eq {X : Type u} {rest : X → Spec} {rRest : (x : X) → RoleDecoration (rest x)} {bm : BundledMonad} {mdRest : (x : X) → (rest x).MonadDecoration} {Output₁ Output₂ : (node X rest).Transcript → Type u} (f : (tr : (node X rest).Transcript) → Output₁ tr → Output₂ tr) (cpt : withMonads (node X rest) (Role.receiver, rRest) (bm, mdRest) Output₁) : mapOutput (node X rest) (Role.receiver, rRest) (bm, mdRest) f cpt = (fun (xc : (x : X) × (fun (x : X) => Interaction.Spec.counterpartMonadicSyntax✝.Family PUnit.unit (rest x) ((fun (x : X) => Decoration.ofOver (fun (x : Type u) (x_1 : Role) => BundledMonad) (rest x) (rRest x) ((fun (x : X) => RoleDecoration.monadsOver (rest x) (rRest x) (mdRest x)) x)) x) fun (tr : (rest x).Transcript) => Output₁ ⟨x, tr⟩) x) => ⟨xc.fst, mapOutput (rest xc.fst) (rRest xc.fst) (mdRest xc.fst) (fun (tr : (rest xc.fst).Transcript) => f ⟨xc.fst, tr⟩) xc.snd⟩) <$> cpt

def Interaction.Spec.Strategy.runWithRolesAndMonads {m : Type u → Type u} [Monad m] (liftStrat liftCpt : (bm : BundledMonad) → {α : Type u} → bm.M α → m α) (spec : Spec) (roles : RoleDecoration spec) (stratDeco cptDeco : spec.MonadDecoration) {OutputP OutputC : spec.Transcript → Type u} : withRolesAndMonads spec roles stratDeco OutputP → Counterpart.withMonads spec roles cptDeco OutputC → m ((tr : spec.Transcript) × OutputP tr × OutputC tr)