The transcript encoding inside the polynomial-time algebra

⚠️ Unreviewed by Bolton

An interactive verifier reads Complexity.Protocol.view, which carries the transcript through DataEncode.bitstringEncode. A machine walking the game tree therefore has to build that encoding as it extends the transcript, one message at a time.

The encoding is a parenthesized serialization, so it is a plain concatenation once the outer brackets are stripped: Complexity.encBody is the concatenation of the per-message encodings, and extending the transcript appends to it (Complexity.encBody_append). That is what makes the walk possible — nothing has to be re-encoded when a message is added or removed.

Main definitions

• Complexity.encBit, Complexity.encMsg, Complexity.encBody — the three layers
• Complexity.encStep — the scan computing a message's encoding

Main results

• Complexity.bitstringEncode_transcript — the encoding, spelled out
• Complexity.encBody_append — a new message is appended
• Complexity.encMsgFn_mem_FP — a message can be encoded in polynomial time

The three layers

def Complexity.encBit (b : Bool) : List Bool

The encoding of a single bit.

Equations

• Complexity.encBit b = if b = true then [false, false, true, true] else [false, true]

def Complexity.encMsg (v : List Bool) : List Bool

The encoding of one message.

Equations

• Complexity.encMsg v = false :: ((List.map Complexity.encBit v).flatten ++ [true])

def Complexity.encBody (τ : List (List Bool)) : List Bool

The concatenation of the messages' encodings — the body of a transcript's encoding.

Equations

• Complexity.encBody τ = (List.map Complexity.encMsg τ).flatten

theorem Complexity.encBit_eq (b : Bool) : (DataEncode.encode b).toBits = encBit b

theorem Complexity.encMsg_eq (v : List Bool) : (DataEncode.encode v).toBits = encMsg v

theorem Complexity.bitstringEncode_transcript (τ : List (List Bool)) : DataEncode.bitstringEncode τ = false :: (encBody τ ++ [true])

The transcript's encoding, spelled out.

@[simp]

theorem Complexity.encBody_nil : encBody [] = []

@[simp]

theorem Complexity.encBody_append (τ : List (List Bool)) (v : List Bool) : encBody (τ ++ [v]) = encBody τ ++ encMsg v

A new message is appended. Nothing already written has to change.

theorem Complexity.encBody_append_two (τ : List (List Bool)) (v a : List Bool) : encBody (τ ++ [v, a]) = encBody τ ++ encMsg v ++ encMsg a

theorem Complexity.encBit_length_le (b : Bool) : (encBit b).length ≤ 4

theorem Complexity.encMsg_length_le (v : List Bool) : (encMsg v).length ≤ 4 * v.length + 2

Encoding a message is polynomial-time

def Complexity.encStep : List Bool × List Bool → List Bool × List Bool

One step of the encoding scan: the bits emitted so far, and the message still to read.

Equations

• Complexity.encStep (acc, []) = (acc, [])
• Complexity.encStep (acc, b :: t) = (acc ++ Complexity.encBit b, t)

@[simp]

theorem Complexity.encStep_nil (acc : List Bool) : encStep (acc, []) = (acc, [])

theorem Complexity.encStep_cons (acc : List Bool) (b : Bool) (t : List Bool) : encStep (acc, b :: t) = (acc ++ encBit b, t)

theorem Complexity.encStep_iterate_run (acc v : List Bool) : encStep^[v.length] (acc, v) = (acc ++ (List.map encBit v).flatten, [])

The scan flattens the per-bit encodings.

theorem Complexity.encStep_iterate_length (acc v : List Bool) (n : ℕ) : (encStep^[n] (acc, v)).1.length + (encStep^[n] (acc, v)).2.length ≤ acc.length + 4 * v.length

The packed scan

def Complexity.encPack (acc rest : List Bool) : List Bool

The packed scan state.

Equations

• Complexity.encPack acc rest = Complexity.pair acc rest

@[simp]

theorem Complexity.encPack_length (acc rest : List Bool) : (encPack acc rest).length = 2 * acc.length + rest.length + 2

def Complexity.encStepP (z : List Bool) : List Bool

One step of the packed scan.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.encStepP_pack (acc rest : List Bool) : encStepP (encPack acc rest) = encPack (encStep (acc, rest)).1 (encStep (acc, rest)).2

theorem Complexity.encStepP_iterate (s : List Bool × List Bool) (n : ℕ) : encStepP^[n] (encPack s.1 s.2) = encPack (encStep^[n] s).1 (encStep^[n] s).2

theorem Complexity.encStepP_iterate_args (acc rest : List Bool) (n : ℕ) : encStepP^[n] (encPack acc rest) = encPack (encStep^[n] (acc, rest)).1 (encStep^[n] (acc, rest)).2

def Complexity.encFlat (v : List Bool) : List Bool

The flattened per-bit encodings, computed by the scan.

Equations

• Complexity.encFlat v = Complexity.pairFst (Complexity.encStepP^[v.length] (Complexity.encPack [] v))

theorem Complexity.encFlat_eq (v : List Bool) : encFlat v = (List.map encBit v).flatten

theorem Complexity.encMsg_eq_encFlat (v : List Bool) : encMsg v = false :: (encFlat v ++ [true])

theorem Complexity.encStepP_mem_FP : encStepP ∈ FP

theorem Complexity.encFlatFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => encFlat (a z)) ∈ FP

theorem Complexity.encMsgFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => encMsg (a z)) ∈ FP

Transcripts given as rounds

def Complexity.flatRounds : List (List Bool × List Bool) → List (List Bool)

A transcript, read off a list of rounds. This is the shape a stack holds: one frame per round, carrying the verifier's message and the prover's reply.

Equations

• Complexity.flatRounds [] = []
• Complexity.flatRounds (p :: ps) = p.1 :: p.2 :: Complexity.flatRounds ps

@[simp]

theorem Complexity.flatRounds_nil : flatRounds [] = []

@[simp]

theorem Complexity.flatRounds_cons (p : List Bool × List Bool) (ps : List (List Bool × List Bool)) : flatRounds (p :: ps) = p.1 :: p.2 :: flatRounds ps

@[simp]

theorem Complexity.flatRounds_length (ps : List (List Bool × List Bool)) : (flatRounds ps).length = 2 * ps.length

@[simp]

theorem Complexity.flatRounds_append (ps : List (List Bool × List Bool)) (v a : List Bool) : flatRounds (ps ++ [(v, a)]) = flatRounds ps ++ [v, a]

def Complexity.encBodyR (ps : List (List Bool × List Bool)) : List Bool

The body of the encoding of a transcript given as rounds.

Equations

• Complexity.encBodyR ps = Complexity.encBody (Complexity.flatRounds ps)

@[simp]

theorem Complexity.encBodyR_nil : encBodyR [] = []

@[simp]

theorem Complexity.encBodyR_append (ps : List (List Bool × List Bool)) (v a : List Bool) : encBodyR (ps ++ [(v, a)]) = encBodyR ps ++ encMsg v ++ encMsg a