The paper's binary tuple encoding

These are binary strings inside answers, distinct from ambient Data encodings. Each payload bit b is written false,b; each field ends in true,false. The polynomial-time candidate reader is deliberately permissive. The answer parser checks exact re-encoding before using any candidate.

def MIPRE.Introspection.AnswerParser.doubleBits : Cost.BitStr → Cost.BitStr

Equations

• MIPRE.Introspection.AnswerParser.doubleBits [] = []
• MIPRE.Introspection.AnswerParser.doubleBits (b :: bs) = false :: b :: MIPRE.Introspection.AnswerParser.doubleBits bs

def MIPRE.Introspection.AnswerParser.field (bs : Cost.BitStr) : Cost.BitStr

Equations

• MIPRE.Introspection.AnswerParser.field bs = MIPRE.Introspection.AnswerParser.doubleBits bs ++ [true, false]

@[simp]

theorem MIPRE.Introspection.AnswerParser.doubleBits_length (bs : Cost.BitStr) : List.length (doubleBits bs) = 2 * List.length bs

@[simp]

theorem MIPRE.Introspection.AnswerParser.field_length (bs : Cost.BitStr) : List.length (field bs) = 2 * List.length bs + 2

theorem MIPRE.Introspection.AnswerParser.field_append_injective (a b c d : Cost.BitStr) (h : field a ++ c = field b ++ d) : a = b ∧ c = d

A field terminator distinguishes its endpoint from every encoded payload bit.

noncomputable def MIPRE.Introspection.AnswerParser.doubleStep : Cost.PolyTimeFun (Cost.BitStr × Bool) Cost.BitStr

Equations

• MIPRE.Introspection.AnswerParser.doubleStep = MIPRE.Cost.PolyTimeFun.snd.cons ((MIPRE.Cost.PolyTimeFun.const false).cons MIPRE.Cost.PolyTimeFun.fst)

theorem MIPRE.Introspection.AnswerParser.doubleStep_size (s : Cost.BitStr) (b : Bool) : Cost.esize (doubleStep.toFun (s, b)) ≤ Cost.esize s + Polynomial.eval (Cost.esize b) (Polynomial.C 6)

theorem MIPRE.Introspection.AnswerParser.double_fold (bs acc : Cost.BitStr) : List.reverse (List.foldl (fun (s : Cost.BitStr) (b : Bool) => doubleStep.toFun (s, b)) acc bs) = List.reverse acc ++ doubleBits bs

noncomputable def MIPRE.Introspection.AnswerParser.doubleProg : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

An actual ambient polynomial-time implementation of bit doubling.

Equations

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

@[simp]

theorem MIPRE.Introspection.AnswerParser.doubleProg_apply (bs : Cost.BitStr) : doubleProg.toFun bs = doubleBits bs

noncomputable def MIPRE.Introspection.AnswerParser.fieldProg : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

Equations

• MIPRE.Introspection.AnswerParser.fieldProg = MIPRE.Cost.PolyTimeFun.append.ap₂ MIPRE.Introspection.AnswerParser.doubleProg (MIPRE.Cost.PolyTimeFun.const [true, false])

@[simp]

theorem MIPRE.Introspection.AnswerParser.fieldProg_apply (bs : Cost.BitStr) : fieldProg.toFun bs = field bs

def MIPRE.Introspection.AnswerParser.readStepFun (s : Bool × Cost.BitStr) (b : Bool) : Bool × Cost.BitStr

Equations

• MIPRE.Introspection.AnswerParser.readStepFun s b = if s.1 = true then (false, b :: s.2) else (true, s.2)

noncomputable def MIPRE.Introspection.AnswerParser.readStep : Cost.PolyTimeFun ((Bool × Cost.BitStr) × Bool) (Bool × Cost.BitStr)

Equations

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

theorem MIPRE.Introspection.AnswerParser.readStep_apply (s : Bool × Cost.BitStr) (b : Bool) : readStep.toFun (s, b) = readStepFun s b

theorem MIPRE.Introspection.AnswerParser.readStep_size (s : Bool × Cost.BitStr) (b : Bool) : Cost.esize (readStep.toFun (s, b)) ≤ Cost.esize s + Polynomial.eval (Cost.esize b) (Polynomial.C 6)

def MIPRE.Introspection.AnswerParser.undouble (bs : Cost.BitStr) : Cost.BitStr

Read the second bit of each pair, discarding a trailing unmatched bit.

Equations

• MIPRE.Introspection.AnswerParser.undouble bs = List.reverse (List.foldl MIPRE.Introspection.AnswerParser.readStepFun (false, []) bs).2

theorem MIPRE.Introspection.AnswerParser.read_double_fold (bs acc : Cost.BitStr) : List.foldl readStepFun (false, acc) (doubleBits bs) = (false, List.reverse bs ++ acc)

@[simp]

theorem MIPRE.Introspection.AnswerParser.undouble_doubleBits (bs : Cost.BitStr) : undouble (doubleBits bs) = bs

noncomputable def MIPRE.Introspection.AnswerParser.undoubleProg : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

Equations

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

@[simp]

theorem MIPRE.Introspection.AnswerParser.undoubleProg_apply (bs : Cost.BitStr) : undoubleProg.toFun bs = undouble bs

def MIPRE.Introspection.AnswerParser.payload (bs : Cost.BitStr) : Cost.BitStr

Candidate payload obtained by removing the presumed last delimiter pair.

Equations

• MIPRE.Introspection.AnswerParser.payload bs = MIPRE.Introspection.AnswerParser.undouble (List.take (List.length bs - 2) bs)

noncomputable def MIPRE.Introspection.AnswerParser.payloadProg : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

Equations

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

@[simp]

theorem MIPRE.Introspection.AnswerParser.payloadProg_apply (bs : Cost.BitStr) : payloadProg.toFun bs = payload bs

@[simp]

theorem MIPRE.Introspection.AnswerParser.payload_field (bs : Cost.BitStr) : payload (field bs) = bs