Protocol Specifications for (Oracle) Reductions

This file defines the ProtocolSpec type, which is used to specify the protocol between the prover and the verifier.

structure ProtocolSpec (n : ℕ) : Type 1

A protocol specification for an interactive protocol with n steps consists of:

• A vector of directions dir for each step, which is either .P_to_V (the prover sends a message to the verifier) or .V_to_P (the verifier sends a challenge to the prover).
• A vector of types «Type» for each step, which is the type of the message or challenge sent in that step.

• dir : Fin n → Direction

  The direction of each message in the protocol.

• Type : Fin n → Type

  The type of each message in the protocol.

theorem ProtocolSpec.ext_iff {n : ℕ} {x y : ProtocolSpec n} : x = y ↔ x.dir = y.dir ∧ x.Type = y.Type

theorem ProtocolSpec.ext {n : ℕ} {x y : ProtocolSpec n} (dir : x.dir = y.dir) («Type» : x.Type = y.Type) : x = y

def instInhabitedProtocolSpec.default {a✝ : ℕ} : ProtocolSpec a✝

@[implicit_reducible]

instance instInhabitedProtocolSpec {a✝ : ℕ} : Inhabited (ProtocolSpec a✝)

@[reducible]

def ProtocolSpec.empty : ProtocolSpec 0

The empty protocol specification, with no messages or challenges, written as !p[].

def ProtocolSpec.«term!p[]» : Lean.ParserDescr

The empty protocol specification, with no messages or challenges, written as !p[].

@[reducible]

def ProtocolSpec.MessageIdx {n : ℕ} (pSpec : ProtocolSpec n) : Type

Subtype of Fin n for the indices corresponding to messages in a protocol specification

@[reducible]

def ProtocolSpec.ChallengeIdx {n : ℕ} (pSpec : ProtocolSpec n) : Type

Subtype of Fin n for the indices corresponding to challenges in a protocol specification

@[implicit_reducible]

instance ProtocolSpec.instCoeHeadMessageIdxFin {n : ℕ} {pSpec : ProtocolSpec n} : CoeHead pSpec.MessageIdx (Fin n)

@[implicit_reducible]

instance ProtocolSpec.instCoeHeadChallengeIdxFin {n : ℕ} {pSpec : ProtocolSpec n} : CoeHead pSpec.ChallengeIdx (Fin n)

@[reducible, inline, specialize #[]]

def ProtocolSpec.Message {n : ℕ} (pSpec : ProtocolSpec n) (i : pSpec.MessageIdx) : Type

The type of the i-th message in a protocol specification.

This does not distinguish between messages received in full or as an oracle.

@[reducible, inline, specialize #[]]

def ProtocolSpec.Message' {n : ℕ} (pSpec : ProtocolSpec n) (i : Fin n) : pSpec.dir i = Direction.P_to_V → Type

Unbundled version of Message, which supplies the proof separately from the index.

@[reducible, inline, specialize #[]]

def ProtocolSpec.Challenge {n : ℕ} (pSpec : ProtocolSpec n) (i : pSpec.ChallengeIdx) : Type

The type of the i-th challenge in a protocol specification

@[reducible, inline, specialize #[]]

def ProtocolSpec.Challenge' {n : ℕ} (pSpec : ProtocolSpec n) (i : Fin n) : pSpec.dir i = Direction.V_to_P → Type

Unbundled version of Challenge, which supplies the proof separately from the index.

@[reducible, inline, specialize #[]]

def ProtocolSpec.Messages {n : ℕ} (pSpec : ProtocolSpec n) : Type

The type of all messages in a protocol specification. Uncurried version of Message.

@[reducible, inline, specialize #[]]

def ProtocolSpec.Messages' {n : ℕ} (pSpec : ProtocolSpec n) : Type

Unbundled version of Messages, which supplies the proof separately from the index.

@[reducible, inline, specialize #[]]

def ProtocolSpec.Challenges {n : ℕ} (pSpec : ProtocolSpec n) : Type

The type of all challenges in a protocol specification

@[reducible, inline, specialize #[]]

def ProtocolSpec.Challenges' {n : ℕ} (pSpec : ProtocolSpec n) : Type

Unbundled version of Challenges, which supplies the proof separately from the index.

@[reducible, inline, specialize #[]]

def ProtocolSpec.FullTranscript {n : ℕ} (pSpec : ProtocolSpec n) : Type

The (full)) transcript of an interactive protocol, which is a list of messages and challenges.

Note that this is definitionally equal to Transcript (Fin.last n) pSpec.

def ProtocolSpec.take {n : ℕ} (m : ℕ) (h : m ≤ n) (pSpec : ProtocolSpec n) : ProtocolSpec m

Take the first m ≤ n rounds of a ProtocolSpec n

def ProtocolSpec.rtake {n : ℕ} (m : ℕ) (h : m ≤ n) (pSpec : ProtocolSpec n) : ProtocolSpec m

Take the last m ≤ n rounds of a ProtocolSpec n

def ProtocolSpec.drop {n : ℕ} (m : ℕ) (h : m ≤ n) (pSpec : ProtocolSpec n) : ProtocolSpec (n - m)

Drop the first m ≤ n rounds of a ProtocolSpec n

def ProtocolSpec.rdrop {n : ℕ} (m : ℕ) (h : m ≤ n) (pSpec : ProtocolSpec n) : ProtocolSpec (n - m)

Drop the last m ≤ n rounds of a ProtocolSpec n

def ProtocolSpec.extract {n : ℕ} (start stop : ℕ) (h1 : start ≤ stop) (h2 : stop ≤ n) (pSpec : ProtocolSpec n) : ProtocolSpec (stop - start)

Extract the slice of the rounds of a ProtocolSpec n from start to stop - 1.

@[implicit_reducible]

instance ProtocolSpec.instSliceLTNatLe {n : ℕ} : SliceLT (ProtocolSpec n) ℕ (fun (x : ProtocolSpec n) (stop : ℕ) => stop ≤ n) fun (x : ProtocolSpec n) (stop : ℕ) (x_1 : stop ≤ n) => ProtocolSpec stop

@[implicit_reducible]

instance ProtocolSpec.instSliceGENatLeHSub {n : ℕ} : SliceGE (ProtocolSpec n) ℕ (fun (x : ProtocolSpec n) (start : ℕ) => start ≤ n) fun (x : ProtocolSpec n) (start : ℕ) (x_1 : start ≤ n) => ProtocolSpec (n - start)

@[implicit_reducible]

instance ProtocolSpec.instSliceNatAndLeHSub {n : ℕ} : Slice (ProtocolSpec n) ℕ ℕ (fun (x : ProtocolSpec n) (start stop : ℕ) => start ≤ stop ∧ stop ≤ n) fun (x : ProtocolSpec n) (start stop : ℕ) (x_1 : start ≤ stop ∧ stop ≤ n) => ProtocolSpec (stop - start)

@[simp]

theorem ProtocolSpec.take_dir {n m : ℕ} {h : m ≤ n} {pSpec : ProtocolSpec n} : pSpec⟦:m⟧.dir = pSpec.dir⟦:m⟧

@[simp]

theorem ProtocolSpec.take_Type {n m : ℕ} {h : m ≤ n} {pSpec : ProtocolSpec n} : pSpec⟦:m⟧.Type = pSpec.Type⟦:m⟧

@[simp]

theorem ProtocolSpec.drop_dir {n m : ℕ} {h : m ≤ n} {pSpec : ProtocolSpec n} : pSpec⟦m:⟧.dir = pSpec.dir⟦m:⟧

@[simp]

theorem ProtocolSpec.drop_Type {n m : ℕ} {h : m ≤ n} {pSpec : ProtocolSpec n} : pSpec⟦m:⟧.Type = pSpec.Type⟦m:⟧

@[simp]

theorem ProtocolSpec.extract_dir {n m start stop : ℕ} {h1 : start ≤ stop} {h2 : stop ≤ n} {pSpec : ProtocolSpec n} : pSpec⟦start:stop⟧.dir = pSpec.dir⟦start:stop⟧

@[simp]

theorem ProtocolSpec.extract_Type {n m start stop : ℕ} {h1 : start ≤ stop} {h2 : stop ≤ n} {pSpec : ProtocolSpec n} : pSpec⟦start:stop⟧.Type = pSpec.Type⟦start:stop⟧

@[reducible, inline]

abbrev ProtocolSpec.FullTranscript.take {n : ℕ} {pSpec : ProtocolSpec n} (m : ℕ) (h : m ≤ n) (transcript : pSpec.FullTranscript) : (ProtocolSpec.take m h pSpec).FullTranscript

Take the first m ≤ n rounds of a (full) transcript for a protocol specification pSpec

@[reducible, inline]

abbrev ProtocolSpec.FullTranscript.rtake {n : ℕ} {pSpec : ProtocolSpec n} (m : ℕ) (h : m ≤ n) (transcript : pSpec.FullTranscript) : (ProtocolSpec.rtake m h pSpec).FullTranscript

Take the last m ≤ n rounds of a (full) transcript for a protocol specification pSpec

@[reducible, inline]

abbrev ProtocolSpec.FullTranscript.drop {n : ℕ} {pSpec : ProtocolSpec n} (m : ℕ) (h : m ≤ n) (transcript : pSpec.FullTranscript) : (ProtocolSpec.drop m h pSpec).FullTranscript

@[reducible, inline]

abbrev ProtocolSpec.FullTranscript.rdrop {n : ℕ} {pSpec : ProtocolSpec n} (m : ℕ) (h : m ≤ n) (transcript : pSpec.FullTranscript) : (ProtocolSpec.rdrop m h pSpec).FullTranscript

@[reducible, inline]

abbrev ProtocolSpec.FullTranscript.extract {n : ℕ} {pSpec : ProtocolSpec n} (start stop : ℕ) (h1 : start ≤ stop) (h2 : stop ≤ n) (transcript : pSpec.FullTranscript) : (ProtocolSpec.extract start stop h1 h2 pSpec).FullTranscript

@[implicit_reducible]

instance ProtocolSpec.FullTranscript.instSliceLTNatLeSliceLT {n : ℕ} {pSpec : ProtocolSpec n} : SliceLT pSpec.FullTranscript ℕ (fun (x : pSpec.FullTranscript) (stop : ℕ) => stop ≤ n) fun (x : pSpec.FullTranscript) (stop : ℕ) (x_1 : stop ≤ n) => pSpec⟦:stop⟧.FullTranscript

@[implicit_reducible]

instance ProtocolSpec.FullTranscript.instSliceGENatLeSliceGEHSub {n : ℕ} {pSpec : ProtocolSpec n} : SliceGE pSpec.FullTranscript ℕ (fun (x : pSpec.FullTranscript) (start : ℕ) => start ≤ n) fun (x : pSpec.FullTranscript) (start : ℕ) (x_1 : start ≤ n) => pSpec⟦start:⟧.FullTranscript

@[implicit_reducible]

instance ProtocolSpec.FullTranscript.instSliceNatAndLeSliceHSub {n : ℕ} {pSpec : ProtocolSpec n} : Slice pSpec.FullTranscript ℕ ℕ (fun (x : pSpec.FullTranscript) (start stop : ℕ) => start ≤ stop ∧ stop ≤ n) fun (x : pSpec.FullTranscript) (start stop : ℕ) (x_1 : start ≤ stop ∧ stop ≤ n) => pSpec⟦start:stop⟧.FullTranscript

theorem ProtocolSpec.FullTranscript.take_eq_take {n m : ℕ} {h : m ≤ n} {pSpec : ProtocolSpec n} {transcript : pSpec.FullTranscript} : transcript⟦:m⟧ = take m h transcript

theorem ProtocolSpec.FullTranscript.rtake_eq_rtake {n m : ℕ} {h : m ≤ n} {pSpec : ProtocolSpec n} {transcript : pSpec.FullTranscript} : transcript⟦m:⟧ = drop m h transcript

theorem ProtocolSpec.FullTranscript.extract_eq_extract {n m start stop m✝ start✝ stop✝ : ℕ} {h1 : start✝ ≤ stop✝} {h2 : stop✝ ≤ n} {pSpec : ProtocolSpec n} {transcript : pSpec.FullTranscript} : transcript⟦start✝:stop✝⟧ = extract start✝ stop✝ h1 h2 transcript

@[reducible]

def ProtocolSpec.MessageIdxUpTo {n : ℕ} (k : Fin (n + 1)) (pSpec : ProtocolSpec n) : Type

Subtype of Fin k for the indices corresponding to messages in a protocol specification up to round k

theorem ProtocolSpec.MessageIdxUpTo.eq_MessageIdx {n : ℕ} {k : Fin (n + 1)} {pSpec : ProtocolSpec n} : MessageIdxUpTo k pSpec = { i : Fin ↑k // pSpec.dir (Fin.castLE ⋯ i) = Direction.P_to_V }

@[reducible]

def ProtocolSpec.ChallengeIdxUpTo {n : ℕ} (k : Fin (n + 1)) (pSpec : ProtocolSpec n) : Type

Subtype of Fin k for the indices corresponding to challenges in a protocol specification up to round k

@[reducible, inline, specialize #[]]

def ProtocolSpec.MessageUpTo {n : ℕ} (k : Fin (n + 1)) (pSpec : ProtocolSpec n) (i : MessageIdxUpTo k pSpec) : Type

The indexed family of messages from the prover up to round k.

@[reducible, inline, specialize #[]]

def ProtocolSpec.ChallengeUpTo {n : ℕ} (k : Fin (n + 1)) (pSpec : ProtocolSpec n) (i : ChallengeIdxUpTo k pSpec) : Type

The indexed family of challenges from the verifier up to round k.

@[reducible, inline, specialize #[]]

def ProtocolSpec.MessagesUpTo {n : ℕ} (k : Fin (n + 1)) (pSpec : ProtocolSpec n) : Type

The type of all messages from the prover up to round k.

@[reducible, inline, specialize #[]]

def ProtocolSpec.ChallengesUpTo {n : ℕ} (k : Fin (n + 1)) (pSpec : ProtocolSpec n) : Type

The type of all challenges from the verifier up to round k.

@[reducible, inline, specialize #[]]

def ProtocolSpec.Transcript {n : ℕ} (k : Fin (n + 1)) (pSpec : ProtocolSpec n) : Type

A (partial) transcript of a protocol specification, indexed by some k : Fin (n + 1), is a list of messages from the protocol for all indices i less than k.

This is defined as the full transcript of the protocol specification up to round k.

@[simp]

theorem ProtocolSpec.Transcript.def_eq {n : ℕ} {k : Fin (n + 1)} {pSpec : ProtocolSpec n} : (take ↑k ⋯ pSpec).FullTranscript = ((i : Fin ↑k) → pSpec.Type (Fin.castLE ⋯ i))

@[implicit_reducible]

instance ProtocolSpec.instUniqueOfNatNat : Unique (ProtocolSpec 0)

There is only one protocol specification with 0 messages (the empty one)

@[implicit_reducible]

instance ProtocolSpec.instVCVCompatibleChallengeEmpty (i : !p[].ChallengeIdx) : VCVCompatible (!p[].Challenge i)

@[implicit_reducible]

instance ProtocolSpec.instSampleableTypeChallengeEmpty (i : !p[].ChallengeIdx) : SampleableType (!p[].Challenge i)

@[implicit_reducible]

instance ProtocolSpec.instOracleInterfaceMessageEmpty (i : !p[].MessageIdx) : OracleInterface (!p[].Message i)

@[implicit_reducible]

instance ProtocolSpec.instVCVCompatibleChallengeDefaultOfNatNat (i : default.ChallengeIdx) : VCVCompatible (default.Challenge i)

@[implicit_reducible]

instance ProtocolSpec.instSampleableTypeChallengeDefaultOfNatNat (i : default.ChallengeIdx) : SampleableType (default.Challenge i)

@[implicit_reducible]

instance ProtocolSpec.instOracleInterfaceMessageDefaultOfNatNat (i : default.MessageIdx) : OracleInterface (default.Message i)

instance ProtocolSpec.instIsEmptyChallengeIdxMkVconsDirectionP_to_VVempty {Msg : Type} : IsEmpty { dir := !v[Direction.P_to_V], «Type» := !v[Msg] }.ChallengeIdx

@[implicit_reducible]

instance ProtocolSpec.instUniqueMessageIdxMkVconsDirectionP_to_VVempty {Msg : Type} : Unique { dir := !v[Direction.P_to_V], «Type» := !v[Msg] }.MessageIdx

@[implicit_reducible]

instance ProtocolSpec.instOracleInterfaceMessageMkVconsDirectionP_to_VVempty {Msg : Type} [inst : OracleInterface Msg] (i : { dir := !v[Direction.P_to_V], «Type» := !v[Msg] }.MessageIdx) : OracleInterface ({ dir := !v[Direction.P_to_V], «Type» := !v[Msg] }.Message i)

@[implicit_reducible]

instance ProtocolSpec.instVCVCompatibleChallengeMkVconsDirectionP_to_VVempty {Msg : Type} (i : { dir := !v[Direction.P_to_V], «Type» := !v[Msg] }.ChallengeIdx) : VCVCompatible ({ dir := !v[Direction.P_to_V], «Type» := !v[Msg] }.Challenge i)

@[implicit_reducible]

instance ProtocolSpec.instSampleableTypeChallengeMkVconsDirectionP_to_VVempty {Msg : Type} (i : { dir := !v[Direction.P_to_V], «Type» := !v[Msg] }.ChallengeIdx) : SampleableType ({ dir := !v[Direction.P_to_V], «Type» := !v[Msg] }.Challenge i)

instance ProtocolSpec.instIsEmptyMessageIdxMkVconsDirectionV_to_PVempty {Chal : Type} : IsEmpty { dir := !v[Direction.V_to_P], «Type» := !v[Chal] }.MessageIdx

@[implicit_reducible]

instance ProtocolSpec.instUniqueChallengeIdxMkVconsDirectionV_to_PVempty {Chal : Type} : Unique { dir := !v[Direction.V_to_P], «Type» := !v[Chal] }.ChallengeIdx

@[implicit_reducible]

instance ProtocolSpec.instOracleInterfaceMessageMkVconsDirectionV_to_PVempty {Chal : Type} (i : { dir := !v[Direction.V_to_P], «Type» := !v[Chal] }.MessageIdx) : OracleInterface ({ dir := !v[Direction.V_to_P], «Type» := !v[Chal] }.Message i)

@[implicit_reducible]

instance ProtocolSpec.instVCVCompatibleChallengeMkVconsDirectionV_to_PVempty {Chal : Type} [inst : VCVCompatible Chal] (i : { dir := !v[Direction.V_to_P], «Type» := !v[Chal] }.ChallengeIdx) : VCVCompatible ({ dir := !v[Direction.V_to_P], «Type» := !v[Chal] }.Challenge i)

@[implicit_reducible]

instance ProtocolSpec.instSampleableTypeChallengeMkVconsDirectionV_to_PVempty {Chal : Type} [inst : SampleableType Chal] (i : { dir := !v[Direction.V_to_P], «Type» := !v[Chal] }.ChallengeIdx) : SampleableType ({ dir := !v[Direction.V_to_P], «Type» := !v[Chal] }.Challenge i)

@[implicit_reducible]

instance ProtocolSpec.instFintypeMessageIdx {n : ℕ} {pSpec : ProtocolSpec n} : Fintype pSpec.MessageIdx

@[implicit_reducible]

instance ProtocolSpec.instFintypeChallengeIdx {n : ℕ} {pSpec : ProtocolSpec n} : Fintype pSpec.ChallengeIdx

@[implicit_reducible]

instance ProtocolSpec.instFintypeMessageIdxUpTo {n : ℕ} {pSpec : ProtocolSpec n} {k : Fin (n + 1)} : Fintype (MessageIdxUpTo k pSpec)

@[implicit_reducible]

instance ProtocolSpec.instFintypeChallengeIdxUpTo {n : ℕ} {pSpec : ProtocolSpec n} {k : Fin (n + 1)} : Fintype (ChallengeIdxUpTo k pSpec)

def ProtocolSpec.MessagesUpTo.take {n : ℕ} {pSpec : ProtocolSpec n} {k : Fin (n + 1)} (j : Fin (↑k + 1)) (messages : MessagesUpTo k pSpec) : MessagesUpTo (Fin.castLE ⋯ j) pSpec

For a tuple of messages up to round k, take the messages up to round j : Fin (k + 1)

def ProtocolSpec.Messages.take {n : ℕ} {pSpec : ProtocolSpec n} (j : Fin (n + 1)) (messages : pSpec.Messages) : MessagesUpTo j pSpec

Take the messages up to round j : Fin (n + 1)

def ProtocolSpec.ChallengesUpTo.take {n : ℕ} {pSpec : ProtocolSpec n} {k : Fin (n + 1)} (j : Fin (↑k + 1)) (challenges : ChallengesUpTo k pSpec) : ChallengesUpTo (Fin.castLE ⋯ j) pSpec

For a tuple of challenges up to round k, take the challenges up to round j : Fin (k + 1)

def ProtocolSpec.Challenges.take {n : ℕ} {pSpec : ProtocolSpec n} (j : Fin (n + 1)) (challenges : pSpec.Challenges) : ChallengesUpTo j pSpec

Take the challenges up to round j : Fin (n + 1)

@[implicit_reducible]

instance ProtocolSpec.MessagesUpTo.instUniqueDefaultOfNatNat {k : Fin 1} : Unique (MessagesUpTo k default)

There is only one transcript for the empty protocol, represented as default : ProtocolSpec 0

@[implicit_reducible]

instance ProtocolSpec.MessagesUpTo.instUniqueEmpty {k : Fin 1} : Unique (MessagesUpTo k !p[])

There is only one transcript for the empty protocol, represented as ![]

@[implicit_reducible]

instance ProtocolSpec.MessagesUpTo.instUniqueOfNatFinHAddNat {n : ℕ} {pSpec : ProtocolSpec n} : Unique (MessagesUpTo 0 pSpec)

There is only one transcript for any protocol specification with cutoff index 0

def ProtocolSpec.MessagesUpTo.concat' {n : ℕ} {pSpec : ProtocolSpec n} {k : Fin n} (messages : (i : Fin ↑k) → pSpec.dir (Fin.castLE ⋯ i) = Direction.P_to_V → pSpec.Type (Fin.castLE ⋯ i)) (msg : (h : pSpec.dir k = Direction.P_to_V) → pSpec.Message ⟨k, h⟩) (i : Fin (↑k + 1)) : pSpec.dir (Fin.castLE ⋯ i) = Direction.P_to_V → pSpec.Type (Fin.castLE ⋯ i)

def ProtocolSpec.MessagesUpTo.concat {n : ℕ} {pSpec : ProtocolSpec n} {k : Fin n} (messages : MessagesUpTo k.castSucc pSpec) (h : pSpec.dir k = Direction.P_to_V) (msg : pSpec.Message ⟨k, h⟩) : MessagesUpTo k.succ pSpec

Concatenate the k-th message to the end of the tuple of messages up to round k, assuming round k is a message round.

def ProtocolSpec.MessagesUpTo.extend {n : ℕ} {pSpec : ProtocolSpec n} {k : Fin n} (messages : MessagesUpTo k.castSucc pSpec) (h : pSpec.dir k = Direction.V_to_P) : MessagesUpTo k.succ pSpec

Extend the tuple of messages up to round k to up to round k + 1, assuming round k is a challenge round (so no message from the prover is sent).

@[implicit_reducible]

instance ProtocolSpec.MessagesUpTo.instDecidableEqOfMessage {n : ℕ} {pSpec : ProtocolSpec n} [inst : (i : pSpec.MessageIdx) → DecidableEq (pSpec.Message i)] {k : Fin (n + 1)} : DecidableEq (MessagesUpTo k pSpec)

@[implicit_reducible]

instance ProtocolSpec.ChallengesUpTo.instUniqueDefaultOfNatNat {k : Fin 1} : Unique (ChallengesUpTo k default)

There is only one transcript for the empty protocol, represented as default : ProtocolSpec 0

@[implicit_reducible]

instance ProtocolSpec.ChallengesUpTo.instUniqueEmpty {k : Fin 1} : Unique (ChallengesUpTo k !p[])

There is only one transcript for the empty protocol, represented as ![]

@[implicit_reducible]

instance ProtocolSpec.ChallengesUpTo.instUniqueOfNatFinHAddNat {n : ℕ} {pSpec : ProtocolSpec n} : Unique (ChallengesUpTo 0 pSpec)

There is only one transcript for any protocol specification with cutoff index 0

def ProtocolSpec.ChallengesUpTo.concat' {n : ℕ} {pSpec : ProtocolSpec n} {k : Fin n} (challenges : (i : Fin ↑k) → pSpec.dir (Fin.castLE ⋯ i) = Direction.V_to_P → pSpec.Type (Fin.castLE ⋯ i)) (chal : (h : pSpec.dir k = Direction.V_to_P) → pSpec.Challenge ⟨k, h⟩) (i : Fin (↑k + 1)) : pSpec.dir (Fin.castLE ⋯ i) = Direction.V_to_P → pSpec.Type (Fin.castLE ⋯ i)

def ProtocolSpec.ChallengesUpTo.concat {n : ℕ} {pSpec : ProtocolSpec n} {k : Fin n} (challenges : ChallengesUpTo k.castSucc pSpec) (h : pSpec.dir k = Direction.V_to_P) (chal : pSpec.Challenge ⟨k, h⟩) : ChallengesUpTo k.succ pSpec

Concatenate the k-th challenge to the end of the tuple of challenges up to round k, assuming round k is a challenge round.

def ProtocolSpec.ChallengesUpTo.extend {n : ℕ} {pSpec : ProtocolSpec n} {k : Fin n} (challenges : ChallengesUpTo k.castSucc pSpec) (h : pSpec.dir k = Direction.P_to_V) : ChallengesUpTo k.succ pSpec

Extend the tuple of challenges up to round k to up to round k + 1, assuming round k is a message round (so no challenge from the verifier is sent).

@[implicit_reducible]

instance ProtocolSpec.Transcript.instUniqueDefaultOfNatNat {k : Fin 1} : Unique (Transcript k default)

There is only one transcript for the empty protocol

@[implicit_reducible]

instance ProtocolSpec.Transcript.instUniqueEmpty {k : Fin 1} : Unique (Transcript k !p[])

There is only one transcript for the empty protocol, represented as ![]

@[implicit_reducible]

instance ProtocolSpec.Transcript.instUniqueOfNatFinHAddNat {n : ℕ} {pSpec : ProtocolSpec n} : Unique (Transcript 0 pSpec)

There is only one transcript for any protocol with cutoff index 0

@[reducible, inline]

abbrev ProtocolSpec.Transcript.concat {n : ℕ} {pSpec : ProtocolSpec n} {m : Fin n} (msg : pSpec.Type m) (T : Transcript m.castSucc pSpec) : Transcript m.succ pSpec

Concatenate a message to the end of a partial transcript. This is definitionally equivalent to Fin.snoc.

def ProtocolSpec.Transcript.toMessagesUpTo {n : ℕ} {pSpec : ProtocolSpec n} {k : Fin (n + 1)} (transcript : Transcript k pSpec) : MessagesUpTo k pSpec

Extract messages from a transcript up to round k

def ProtocolSpec.Transcript.toChallengesUpTo {n : ℕ} {pSpec : ProtocolSpec n} {k : Fin (n + 1)} (transcript : Transcript k pSpec) : ChallengesUpTo k pSpec

Extract challenges from a transcript up to round k

def ProtocolSpec.Transcript.toMessagesChallenges {n : ℕ} {pSpec : ProtocolSpec n} {k : Fin (n + 1)} (transcript : Transcript k pSpec) : MessagesUpTo k pSpec × ChallengesUpTo k pSpec

def ProtocolSpec.Transcript.ofMessagesChallenges {n : ℕ} {pSpec : ProtocolSpec n} {k : Fin (n + 1)} (messages : MessagesUpTo k pSpec) (challenges : ChallengesUpTo k pSpec) : Transcript k pSpec

def ProtocolSpec.Transcript.equivMessagesChallenges {n : ℕ} {pSpec : ProtocolSpec n} {k : Fin (n + 1)} : Transcript k pSpec ≃ MessagesUpTo k pSpec × ChallengesUpTo k pSpec

An equivalence between transcripts up to round k and the tuple of messages and challenges up to round k.

@[simp]

theorem ProtocolSpec.Transcript.equivMessagesChallenges_apply {n : ℕ} {pSpec : ProtocolSpec n} {k : Fin (n + 1)} (transcript : Transcript k pSpec) : equivMessagesChallenges transcript = transcript.toMessagesChallenges

@[simp]

theorem ProtocolSpec.Transcript.equivMessagesChallenges_symm_apply {n : ℕ} {pSpec : ProtocolSpec n} {k : Fin (n + 1)} (a✝ : MessagesUpTo k pSpec × ChallengesUpTo k pSpec) (i : Fin ↑k) : equivMessagesChallenges.symm a✝ i = Function.uncurry ofMessagesChallenges a✝ i

@[reducible, inline, specialize #[]]

def ProtocolSpec.FullTranscript.messages {n : ℕ} {pSpec : ProtocolSpec n} (transcript : pSpec.FullTranscript) (i : pSpec.MessageIdx) : pSpec.Type ↑i

@[reducible, inline, specialize #[]]

def ProtocolSpec.FullTranscript.challenges {n : ℕ} {pSpec : ProtocolSpec n} (transcript : pSpec.FullTranscript) (i : pSpec.ChallengeIdx) : pSpec.Type ↑i

@[implicit_reducible]

instance ProtocolSpec.FullTranscript.instUniqueDefaultOfNatNat : Unique default.FullTranscript

There is only one full transcript (the empty one) for an empty protocol

def ProtocolSpec.FullTranscript.toMessagesChallenges {n : ℕ} {pSpec : ProtocolSpec n} (transcript : pSpec.FullTranscript) : pSpec.Messages × pSpec.Challenges

Convert a full transcript to the tuple of messages and challenges

def ProtocolSpec.FullTranscript.ofMessagesChallenges {n : ℕ} {pSpec : ProtocolSpec n} (messages : pSpec.Messages) (challenges : pSpec.Challenges) : pSpec.FullTranscript

Convert the tuple of messages and challenges to a full transcript

def ProtocolSpec.FullTranscript.equivMessagesChallenges {n : ℕ} {pSpec : ProtocolSpec n} : pSpec.FullTranscript ≃ pSpec.Messages × pSpec.Challenges

An equivalence between full transcripts and the tuple of messages and challenges.

@[simp]

theorem ProtocolSpec.FullTranscript.equivMessagesChallenges_apply {n : ℕ} {pSpec : ProtocolSpec n} (transcript : Transcript (Fin.last n) pSpec) : equivMessagesChallenges transcript = transcript.toMessagesChallenges

@[simp]

theorem ProtocolSpec.FullTranscript.equivMessagesChallenges_symm_apply {n : ℕ} {pSpec : ProtocolSpec n} (a✝ : MessagesUpTo (Fin.last n) pSpec × ChallengesUpTo (Fin.last n) pSpec) (i : Fin ↑(Fin.last n)) : equivMessagesChallenges.symm a✝ i = Function.uncurry Transcript.ofMessagesChallenges a✝ i

class ProtocolSpec.OracleInterfaces {n : ℕ} (pSpec : ProtocolSpec n) : Type 1

The specification of whether each message in a protocol specification is available in full (None) or received as an oracle (Some (instOracleInterface (pSpec.Message i))).

This is defined as a type class for notational convenience.

• oracleInterfaces (i : pSpec.MessageIdx) : Option (OracleInterface (pSpec.Message i))

@[reducible, inline, specialize #[]]

def ProtocolSpec.OracleMessageIdx {n : ℕ} (pSpec : ProtocolSpec n) [inst : pSpec.OracleInterfaces] : Type

Subtype of pSpec.MessageIdx for messages that are received as oracles

@[implicit_reducible]

instance ProtocolSpec.instOracleInterfaceMessageValMessageIdxEqBoolIsSomeOracleInterfacesTrue {n : ℕ} (pSpec : ProtocolSpec n) [inst : pSpec.OracleInterfaces] {i : pSpec.OracleMessageIdx} : OracleInterface (pSpec.Message ↑i)

The oracle interface instances for messages that are received as oracles

@[reducible, inline, specialize #[]]

def ProtocolSpec.PlainMessageIdx {n : ℕ} (pSpec : ProtocolSpec n) [inst : pSpec.OracleInterfaces] : Type

Subtype of pSpec.MessageIdx for messages that are received in full

@[reducible, inline, specialize #[]]

def ProtocolSpec.PlainMessage {n : ℕ} (pSpec : ProtocolSpec n) [inst : pSpec.OracleInterfaces] (i : pSpec.PlainMessageIdx) : Type

The type of messages that are received in full

@[reducible, inline, specialize #[]]

def ProtocolSpec.OracleMessage {n : ℕ} (pSpec : ProtocolSpec n) [inst : pSpec.OracleInterfaces] (i : pSpec.OracleMessageIdx) : Type

The type of messages that are received as oracles

def ProtocolSpec.PlainMessages {n : ℕ} (pSpec : ProtocolSpec n) [pSpec.OracleInterfaces] : Type

def ProtocolSpec.OracleMessages {n : ℕ} (pSpec : ProtocolSpec n) [pSpec.OracleInterfaces] : Type

@[reducible, inline, specialize #[]]

instance ProtocolSpec.challengeOracleInterface {n : ℕ} {pSpec : ProtocolSpec n} (i : pSpec.ChallengeIdx) : OracleInterface (pSpec.Challenge i)

Turn each verifier's challenge into an oracle, where querying a unit type gives back the challenge.

This is the default instance for the challenge oracle interface. It may be overridden by challengeOracleInterface{SR/FS} for state-restoration and/or Fiat-Shamir.

def ProtocolSpec.challengeOracleInterface' {n : ℕ} {pSpec : ProtocolSpec n} : OracleInterface ((i : pSpec.ChallengeIdx) → pSpec.Challenge i)

@[reducible, inline, specialize #[]]

def ProtocolSpec.getChallenge {n : ℕ} (pSpec : ProtocolSpec n) (i : pSpec.ChallengeIdx) : OracleComp [pSpec.Challenge]ₒ (pSpec.Challenge i)

Query a verifier's challenge for a given challenge round i, given the default challenge oracle interface challengeOracleInterface.

This is the default version for getting challenges, where we query the default challengeOracleInterface, which accepts trivial input. In contrast, getChallenge{SR/FS} requires an input statement and prior messages up to that round.

def ProtocolSpec.challengeQueryImpl {n : ℕ} {pSpec : ProtocolSpec n} [(i : pSpec.ChallengeIdx) → SampleableType (pSpec.Challenge i)] : QueryImpl [pSpec.Challenge]ₒ ProbComp

Define the query implementation for the verifier's challenge in terms of ProbComp.

This is a randomness oracle: it simply calls the selectElem method inherited from the SampleableType instance on the challenge types.

@[reducible, inline, specialize #[]]

def ProtocolSpec.challengeOracleInterfaceSR {n : ℕ} (StmtIn : Type) (pSpec : ProtocolSpec n) (i : pSpec.ChallengeIdx) : OracleInterface (pSpec.Challenge i)

The oracle interface for state-restoration and (basic) Fiat-Shamir.

This is the version where we hash the input statement and the entire transcript up to the point of deriving a new challenge. To be precise:

• The domain of the oracle is Statement × pSpec.MessagesUpTo i.1.castSucc
• The range of the oracle is pSpec.Challenge i
• The oracle just returns the challenge

def ProtocolSpec.challengeOracleInterfaceFS {n : ℕ} (StmtIn : Type) (pSpec : ProtocolSpec n) (i : pSpec.ChallengeIdx) : OracleInterface (pSpec.Challenge i)

Alias of ProtocolSpec.challengeOracleInterfaceSR.

---

The oracle interface for state-restoration and (basic) Fiat-Shamir.

This is the version where we hash the input statement and the entire transcript up to the point of deriving a new challenge. To be precise:

• The domain of the oracle is Statement × pSpec.MessagesUpTo i.1.castSucc
• The range of the oracle is pSpec.Challenge i
• The oracle just returns the challenge

@[reducible, inline]

def ProtocolSpec.srChallengeOracle (Statement : Type) {n : ℕ} (pSpec : ProtocolSpec n) : OracleSpec ((i : pSpec.ChallengeIdx) × OracleInterface.Query (pSpec.Challenge i))

The oracle interface for Fiat-Shamir.

This is the (inefficient) version where we hash the input statement and the entire transcript up to the point of deriving a new challenge. To be precise:

• The domain of the oracle is Statement × pSpec.MessagesUpTo i.1.castSucc
• The range of the oracle is pSpec.Challenge i

Some variants of Fiat-Shamir takes in a salt each round. We assume that such salts are included in the input statement (i.e. we can always transform a given reduction into one where every round has a random salt).

def ProtocolSpec.fsChallengeOracle (Statement : Type) {n : ℕ} (pSpec : ProtocolSpec n) : OracleSpec ((i : pSpec.ChallengeIdx) × OracleInterface.Query (pSpec.Challenge i))

Alias of ProtocolSpec.srChallengeOracle.

---

The oracle interface for Fiat-Shamir.

This is the (inefficient) version where we hash the input statement and the entire transcript up to the point of deriving a new challenge. To be precise:

• The domain of the oracle is Statement × pSpec.MessagesUpTo i.1.castSucc
• The range of the oracle is pSpec.Challenge i

Some variants of Fiat-Shamir takes in a salt each round. We assume that such salts are included in the input statement (i.e. we can always transform a given reduction into one where every round has a random salt).

@[implicit_reducible]

instance ProtocolSpec.instDecidableEqSigmaChallengeIdxQueryChallengeSrChallengeOracleOfMessageOfDecidableEq {n : ℕ} {pSpec : ProtocolSpec n} {Statement : Type} [DecidableEq Statement] [(i : pSpec.MessageIdx) → DecidableEq (pSpec.Message i)] [(i : pSpec.ChallengeIdx) → DecidableEq (pSpec.Challenge i)] : (srChallengeOracle Statement pSpec).DecidableEq

Decidable equality for the state-restoration / (slow) Fiat-Shamir oracle

@[implicit_reducible]

instance ProtocolSpec.instFintypeSigmaChallengeIdxQueryChallengeSrChallengeOracleOfVCVCompatible {n : ℕ} {pSpec : ProtocolSpec n} {Statement : Type} [(i : pSpec.ChallengeIdx) → VCVCompatible (pSpec.Challenge i)] : (srChallengeOracle Statement pSpec).Fintype

@[implicit_reducible]

instance ProtocolSpec.instFintypeSigmaChallengeIdxQueryChallengeFsChallengeOracleOfVCVCompatible {n : ℕ} {pSpec : ProtocolSpec n} {Statement : Type} [(i : pSpec.ChallengeIdx) → VCVCompatible (pSpec.Challenge i)] : (fsChallengeOracle Statement pSpec).Fintype

@[reducible, inline, specialize #[]]

def ProtocolSpec.srChallengeQueryImpl {n : ℕ} {Statement : Type} {pSpec : ProtocolSpec n} [(i : pSpec.ChallengeIdx) → SampleableType (pSpec.Challenge i)] : QueryImpl (srChallengeOracle Statement pSpec) ProbComp

Define the query implementation for the state-restoration / (slow) Fiat-Shamir oracle (returns a challenge given messages up to that point) in terms of ProbComp.

This is a randomness oracle: it simply calls the selectElem method inherited from the SampleableType instance on the challenge types. We may then augment this with withCaching to obtain a function-like implementation (caches and replays previous queries).

For implementation with caching, we add withCaching.

For implementation where the whole function is sampled ahead of time, and we answer with that function, see srChallengeQueryImpl'.

@[reducible, inline, specialize #[]]

def ProtocolSpec.srChallengeQueryImpl' {n : ℕ} {Statement : Type} {pSpec : ProtocolSpec n} [(i : pSpec.ChallengeIdx) → SampleableType (pSpec.Challenge i)] : QueryImpl (srChallengeOracle Statement pSpec) (StateT (QueryImpl (srChallengeOracle Statement pSpec) Id) ProbComp)

Alternate version of query implementation that takes in a cached function f and returns the result and the updated function.

TODO: upstream this as a more general construction in VCVio

def ProtocolSpec.fsChallengeQueryImpl' {n : ℕ} {Statement : Type} {pSpec : ProtocolSpec n} [(i : pSpec.ChallengeIdx) → SampleableType (pSpec.Challenge i)] : QueryImpl (srChallengeOracle Statement pSpec) (StateT (QueryImpl (srChallengeOracle Statement pSpec) Id) ProbComp)

Alias of ProtocolSpec.srChallengeQueryImpl'.

---

Alternate version of query implementation that takes in a cached function f and returns the result and the updated function.

TODO: upstream this as a more general construction in VCVio

def ProtocolSpec.MessagesUpTo.deriveTranscriptSRAux {n : ℕ} {pSpec : ProtocolSpec n} {ι : Type} {oSpec : OracleSpec ι} {StmtIn : Type} (stmt : StmtIn) (k : Fin (n + 1)) (messages : MessagesUpTo k pSpec) (j : Fin (↑k + 1)) : OracleComp (oSpec + fsChallengeOracle StmtIn pSpec) (Transcript (Fin.castLE ⋯ j) pSpec)

Auxiliary function for deriving the transcript up to round k from the (full) messages, via querying the state-restoration / Fiat-Shamir oracle for the challenges.

This is used to define deriveTranscriptFS.

def ProtocolSpec.MessagesUpTo.deriveTranscriptSR {n : ℕ} {pSpec : ProtocolSpec n} {ι : Type} {oSpec : OracleSpec ι} {StmtIn : Type} (stmt : StmtIn) (k : Fin (n + 1)) (messages : MessagesUpTo k pSpec) : OracleComp (oSpec + fsChallengeOracle StmtIn pSpec) (Transcript k pSpec)

Derive the transcript up to round k from the (full) messages, via querying the state-restoration / Fiat-Shamir oracle for the challenges.

def ProtocolSpec.MessagesUpTo.deriveTranscriptFS {n : ℕ} {pSpec : ProtocolSpec n} {ι : Type} {oSpec : OracleSpec ι} {StmtIn : Type} (stmt : StmtIn) (k : Fin (n + 1)) (messages : MessagesUpTo k pSpec) : OracleComp (oSpec + fsChallengeOracle StmtIn pSpec) (Transcript k pSpec)

Alias of ProtocolSpec.MessagesUpTo.deriveTranscriptSR.

---

Derive the transcript up to round k from the (full) messages, via querying the state-restoration / Fiat-Shamir oracle for the challenges.

def ProtocolSpec.Messages.deriveTranscriptSR {n : ℕ} {pSpec : ProtocolSpec n} {ι : Type} {oSpec : OracleSpec ι} {StmtIn : Type} (stmt : StmtIn) (messages : pSpec.Messages) : OracleComp (oSpec + fsChallengeOracle StmtIn pSpec) pSpec.FullTranscript

Derive the transcript up to round k from the (full) messages, via querying the state-restoration / Fiat-Shamir oracle for the challenges.

def ProtocolSpec.Messages.deriveTranscriptFS {n : ℕ} {pSpec : ProtocolSpec n} {ι : Type} {oSpec : OracleSpec ι} {StmtIn : Type} (stmt : StmtIn) (messages : pSpec.Messages) : OracleComp (oSpec + fsChallengeOracle StmtIn pSpec) pSpec.FullTranscript

Alias of ProtocolSpec.Messages.deriveTranscriptSR.

---

Derive the transcript up to round k from the (full) messages, via querying the state-restoration / Fiat-Shamir oracle for the challenges.