Executable introspection answer format and internal-cutoff checks

The register length Q and original-answer bound R are supplied constants. Introspect and Sample use pairCheck; Read uses tripleCheck Q R false; Hide uses tripleCheck Q Q true. Exact binary tuple re-encoding rejects all malformed delimiters, extra fields, and trailing bits. The bound on the original answer is checked here, independently of any outer tuple cutoff.

def MIPRE.Introspection.AnswerParser.pairBits (y a : Cost.BitStr) : Cost.BitStr

Equations

• MIPRE.Introspection.AnswerParser.pairBits y a = MIPRE.Introspection.AnswerParser.field y ++ MIPRE.Introspection.AnswerParser.field a

def MIPRE.Introspection.AnswerParser.tripleBits (y yp a : Cost.BitStr) : Cost.BitStr

Equations

• MIPRE.Introspection.AnswerParser.tripleBits y yp a = MIPRE.Introspection.AnswerParser.field y ++ (MIPRE.Introspection.AnswerParser.field yp ++ MIPRE.Introspection.AnswerParser.field a)

@[simp]

theorem MIPRE.Introspection.AnswerParser.pairBits_length (y a : Cost.BitStr) : List.length (pairBits y a) = 2 * (List.length y + List.length a + 2)

@[simp]

theorem MIPRE.Introspection.AnswerParser.tripleBits_length (y yp a : Cost.BitStr) : List.length (tripleBits y yp a) = 2 * (List.length y + List.length yp + List.length a + 3)

theorem MIPRE.Introspection.AnswerParser.pairBits_injective {y a z b : Cost.BitStr} (h : pairBits y a = pairBits z b) : y = z ∧ a = b

theorem MIPRE.Introspection.AnswerParser.tripleBits_injective {y yp a z zp b : Cost.BitStr} (h : tripleBits y yp a = tripleBits z zp b) : y = z ∧ yp = zp ∧ a = b

def MIPRE.Introspection.AnswerParser.pairParts (Q : ℕ) (bs : Cost.BitStr) : Cost.BitStr × Cost.BitStr

Equations

• MIPRE.Introspection.AnswerParser.pairParts Q bs = (MIPRE.Introspection.AnswerParser.payload (List.take (2 * Q + 2) bs), MIPRE.Introspection.AnswerParser.payload (List.drop (2 * Q + 2) bs))

def MIPRE.Introspection.AnswerParser.tripleParts (Q : ℕ) (bs : Cost.BitStr) : Cost.BitStr × Cost.BitStr × Cost.BitStr

Equations

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

@[simp]

theorem MIPRE.Introspection.AnswerParser.pairParts_pairBits (Q : ℕ) (y a : Cost.BitStr) (hy : List.length y = Q) : pairParts Q (pairBits y a) = (y, a)

@[simp]

theorem MIPRE.Introspection.AnswerParser.tripleParts_tripleBits (Q : ℕ) (y yp a : Cost.BitStr) (hy : List.length y = Q) (hyp : List.length yp = Q) : tripleParts Q (tripleBits y yp a) = (y, yp, a)

noncomputable def MIPRE.Introspection.AnswerParser.pairPartsProg (Q : ℕ) : Cost.PolyTimeFun Cost.BitStr (Cost.BitStr × Cost.BitStr)

Equations

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

@[simp]

theorem MIPRE.Introspection.AnswerParser.pairPartsProg_apply (Q : ℕ) (bs : Cost.BitStr) : (pairPartsProg Q).toFun bs = pairParts Q bs

noncomputable def MIPRE.Introspection.AnswerParser.triplePartsProg (Q : ℕ) : Cost.PolyTimeFun Cost.BitStr (Cost.BitStr × Cost.BitStr × Cost.BitStr)

Equations

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

@[simp]

theorem MIPRE.Introspection.AnswerParser.triplePartsProg_apply (Q : ℕ) (bs : Cost.BitStr) : (triplePartsProg Q).toFun bs = tripleParts Q bs

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

Equations

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

@[simp]

theorem MIPRE.Introspection.AnswerParser.pairBitsProg_apply (p : Cost.BitStr × Cost.BitStr) : pairBitsProg.toFun p = pairBits p.1 p.2

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

Equations

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

@[simp]

theorem MIPRE.Introspection.AnswerParser.tripleBitsProg_apply (p : Cost.BitStr × Cost.BitStr × Cost.BitStr) : tripleBitsProg.toFun p = tripleBits p.1 p.2.1 p.2.2

def MIPRE.Introspection.AnswerParser.pairValid (Q R : ℕ) (bs : Cost.BitStr) : Prop

Equations

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

def MIPRE.Introspection.AnswerParser.tripleValid (Q R : ℕ) (exactLast : Bool) (bs : Cost.BitStr) : Prop

Equations

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

@[instance_reducible]

instance MIPRE.Introspection.AnswerParser.instDecidablePairValid (Q R : ℕ) (bs : Cost.BitStr) : Decidable (pairValid Q R bs)

Equations

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

@[instance_reducible]

instance MIPRE.Introspection.AnswerParser.instDecidableTripleValid (Q R : ℕ) (exactLast : Bool) (bs : Cost.BitStr) : Decidable (tripleValid Q R exactLast bs)

Equations

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

theorem MIPRE.Introspection.AnswerParser.decide_and_if (p q : Prop) [Decidable p] [Decidable q] : (if p then decide q else false) = decide (p ∧ q)

noncomputable def MIPRE.Introspection.AnswerParser.pairCheck (Q R : ℕ) : Cost.PolyTimeFun Cost.BitStr Bool

Concrete format and internal original-answer-cutoff check for Introspect/Sample.

Equations

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

theorem MIPRE.Introspection.AnswerParser.pairCheck_apply (Q R : ℕ) (bs : Cost.BitStr) : (pairCheck Q R).toFun bs = decide (pairValid Q R bs)

noncomputable def MIPRE.Introspection.AnswerParser.tripleCheck (Q R : ℕ) (exactLast : Bool) : Cost.PolyTimeFun Cost.BitStr Bool

Concrete format check for Read (exactLast=false) or Hide (exactLast=true).

Equations

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

theorem MIPRE.Introspection.AnswerParser.tripleCheck_apply (Q R : ℕ) (exactLast : Bool) (bs : Cost.BitStr) : (tripleCheck Q R exactLast).toFun bs = decide (tripleValid Q R exactLast bs)

theorem MIPRE.Introspection.AnswerParser.pairCheck_iff (Q R : ℕ) (bs : Cost.BitStr) : (pairCheck Q R).toFun bs = true ↔ ∃ (y : Cost.BitStr) (a : Cost.BitStr), List.length y = Q ∧ List.length a ≤ R ∧ bs = pairBits y a

theorem MIPRE.Introspection.AnswerParser.tripleCheck_iff (Q R : ℕ) (exactLast : Bool) (bs : Cost.BitStr) : (tripleCheck Q R exactLast).toFun bs = true ↔ ∃ (y : Cost.BitStr) (yp : Cost.BitStr) (a : Cost.BitStr), List.length y = Q ∧ List.length yp = Q ∧ (if exactLast = true then List.length a = R else List.length a ≤ R) ∧ bs = tripleBits y yp a

theorem MIPRE.Introspection.AnswerParser.pairCheck_pairBits (Q R : ℕ) (y a : Cost.BitStr) : (pairCheck Q R).toFun (pairBits y a) = true ↔ List.length y = Q ∧ List.length a ≤ R

In particular, an encoded pair with a wrong register length or long a is rejected.

theorem MIPRE.Introspection.AnswerParser.tripleCheck_tripleBits (Q R : ℕ) (exactLast : Bool) (y yp a : Cost.BitStr) : (tripleCheck Q R exactLast).toFun (tripleBits y yp a) = true ↔ List.length y = Q ∧ List.length yp = Q ∧ if exactLast = true then List.length a = R else List.length a ≤ R

theorem MIPRE.Introspection.AnswerParser.pairBits_lt_outer (Q R : ℕ) (hQ : 4 ≤ Q) (hR : 3 * R ≤ Q) (y a : Cost.BitStr) (hy : List.length y = Q) (ha : List.length a ≤ R) : List.length (pairBits y a) < 8 * Q

The repaired strict 8Q outer cutoff contains every honest pair tuple.

theorem MIPRE.Introspection.AnswerParser.readBits_lt_outer (Q R : ℕ) (hQ : 4 ≤ Q) (hR : 3 * R ≤ Q) (y yp a : Cost.BitStr) (hy : List.length y = Q) (hyp : List.length yp = Q) (ha : List.length a ≤ R) : List.length (tripleBits y yp a) < 8 * Q

The repaired strict 8Q outer cutoff contains every honest Read tuple.

theorem MIPRE.Introspection.AnswerParser.hideBits_lt_outer (Q : ℕ) (hQ : 4 ≤ Q) (y yp x : Cost.BitStr) (hy : List.length y = Q) (hyp : List.length yp = Q) (hx : List.length x = Q) : List.length (tripleBits y yp x) < 8 * Q

The repaired strict 8Q outer cutoff contains every honest Hide tuple.

theorem MIPRE.Introspection.AnswerParser.pairCheck_original_cutoff (Q R : ℕ) (bs : Cost.BitStr) (h : (pairCheck Q R).toFun bs = true) : List.length (pairParts Q bs).2 ≤ R

theorem MIPRE.Introspection.AnswerParser.readCheck_original_cutoff (Q R : ℕ) (bs : Cost.BitStr) (h : (tripleCheck Q R false).toFun bs = true) : List.length (tripleParts Q bs).2.2 ≤ R