Party.lean🔗

Tier 2 · definitions used by the computational proof 3 headline theorems depend on it 13 of 58 lines trusted trust banner B3, trusted in part source ↗

Read the definitions shown. Only the declarations that the headline statements use are shown, with the namespace, section, open and variable commands needed to read them. The collapsed runs are theorems, which Lean checks, and definitions that no headline statement uses.

Protocol parties and alternating epoch ownership

Trusted in part. The theorems of Computational/Theorems/ use every definition in this file except Party.senderOf: read them. Party.senderOf and the theorems here are checked by Lean. See Computational/docs/TRUSTED_BASE.md.

Defines the two participants (Party), partner swap (Party.other), and alternating epoch ownership (Party.sendsIn, Party.senderOf: A sends in odd epochs, B in even epochs) shared by the CKA and SM games (ACD19 §3.2.1, §4.1.1).

@[expose] public section

namespace CryptoGames

inductive PartyL30–34 ↗#

Two-party protocol participant (A or B).

inductive Party
  | A
  | B
  deriving DecidableEq, Repr

namespace Party

def otherL38–41 ↗#

Partner of a party (A ↔ B).

def other : Party → Party
  | A => B
  | B => A

4 declarations not shown (lines 43–46): theorems, which Lean checks, or definitions that no headline statement uses

CryptoGames.Party.other_A, CryptoGames.Party.other_B, CryptoGames.Party.other_other, CryptoGames.Party.other_ne

def sendsInL48–51 ↗#

Whether P sends in epoch t (A in odd epochs, B in even epochs).

def sendsIn : Party → ℕ → Bool
  | A, t => t % 2 == 1
  | B, t => t % 2 == 0

1 declaration not shown (lines 53–59): theorems, which Lean checks, or definitions that no headline statement uses

CryptoGames.Party.senderOf

end Party

end CryptoGames