Examples: multiparty endpoints with local views

This file contains examples showing how the native multiparty endpoint types compute definitionally in the broadcast, directed, and profile-based communication models introduced in the new Interaction.Multiparty layer.

Besides the basic broadcast and directed examples, the later sections focus on adversarial semantics. They show that the current sequential Interaction.Spec framework can already model, in a definitionally transparent way:

• public-transcript adversarial choices;
• directed delivery with hidden outsiders;
• metadata leakage without full payload leakage;
• adversarial choices among dropping, delivering, and duplicating messages; and
• adaptive adversarial power where earlier choices change later local views.

The examples are written using pattern-matching resolvers rather than equality tests. This is deliberate: for concrete finite party types, it keeps the local endpoint types definitionally transparent.

inductive Interaction.Multiparty.ThreeParty : Type u

• prover : ThreeParty
• verifier : ThreeParty
• extractor : ThreeParty

@[implicit_reducible]

instance Interaction.Multiparty.instDecidableEqThreeParty : DecidableEq ThreeParty

def Interaction.Multiparty.ThreeParty.resolveBroadcastFor (me : ThreeParty) (owner : ThreeParty) {X : Type u} : LocalView X

resolveBroadcastFor me owner is the local-view projection of the broadcast model to the fixed participant me.

At nodes owned by me, the result is LocalView.active. At all other nodes, the result is LocalView.observe.

This definition is written by pattern matching, rather than by equality tests, so that endpoint types reduce definitionally in examples.

def Interaction.Multiparty.ThreeParty.resolveDirectedFor (me : ThreeParty) (src : ThreeParty) (dst : ThreeParty) {X : Type u} : LocalView X

resolveDirectedFor me src dst is the local-view projection of the directed model to the fixed participant me.

It returns:

• active when me is the node's source party;
• observe when me is the node's designated destination party;
• hidden otherwise.

As in the broadcast model, this resolver is defined by pattern matching, so that local endpoint types unfold definitionally.

inductive Interaction.Multiparty.ScheduleParty : Type u

• adversary : ScheduleParty
• recipient : ScheduleParty
• auditor : ScheduleParty
• outsider : ScheduleParty

@[implicit_reducible]

instance Interaction.Multiparty.instDecidableEqScheduleParty : DecidableEq ScheduleParty

inductive Interaction.Multiparty.DeliveryParty : Type u

DeliveryParty is a small network with one active adversary, two possible recipients, one auditor, and one completely uninformed outsider.

• adversary : DeliveryParty
• bob : DeliveryParty
• carol : DeliveryParty
• auditor : DeliveryParty
• outsider : DeliveryParty

@[implicit_reducible]

instance Interaction.Multiparty.instDecidableEqDeliveryParty : DecidableEq DeliveryParty

inductive Interaction.Multiparty.DeliverySummary : Type u

The public scheduling summary of a network action.

This forgets message payloads and records only who, if anyone, received a delivery.

• none : DeliverySummary
• bob : DeliverySummary
• carol : DeliverySummary
• both : DeliverySummary

@[implicit_reducible]

instance Interaction.Multiparty.instDecidableEqDeliverySummary : DecidableEq DeliverySummary

inductive Interaction.Multiparty.NetworkAction (Msg : Type u) : Type u

Possible one-step powers of a scheduling adversary for a single pending message.

The adversary may:

• drop the message entirely;
• deliver it only to Bob;
• deliver it only to Carol; or
• duplicate it and deliver to both Bob and Carol.

• drop {Msg : Type u} : NetworkAction Msg
• deliverBob {Msg : Type u} (msg : Msg) : NetworkAction Msg
• deliverCarol {Msg : Type u} (msg : Msg) : NetworkAction Msg
• duplicate {Msg : Type u} (msg : Msg) : NetworkAction Msg

@[implicit_reducible]

instance Interaction.Multiparty.instDecidableEqNetworkAction {Msg✝ : Type u_1} [DecidableEq Msg✝] : DecidableEq (NetworkAction Msg✝)

def Interaction.Multiparty.instDecidableEqNetworkAction.decEq {Msg✝ : Type u_1} [DecidableEq Msg✝] (x✝ x✝¹ : NetworkAction Msg✝) : Decidable (x✝ = x✝¹)

inductive Interaction.Multiparty.CorruptionParty : Type u

Parties in a tiny adaptive-corruption example.

The adversary first chooses whom to corrupt, and then gains active control over the next move that emerges from the corrupted side.

• adversary : CorruptionParty
• alice : CorruptionParty
• bob : CorruptionParty
• monitor : CorruptionParty

@[implicit_reducible]

instance Interaction.Multiparty.instDecidableEqCorruptionParty : DecidableEq CorruptionParty

inductive Interaction.Multiparty.CorruptionTarget : Type u

The honest party corrupted by the adversary.

• alice : CorruptionTarget
• bob : CorruptionTarget

@[implicit_reducible]

instance Interaction.Multiparty.instDecidableEqCorruptionTarget : DecidableEq CorruptionTarget