Executable full-register Introspect/Read comparison

The binary register length and original answer cutoff are input data. All register fields have the full padded length. In particular the Read dual answer is not required to vanish outside the original source register: the same-depth padding puts those coordinates in the first zero-map factor. The program checks canonical tuple syntax, the separate original answer cutoff, and the strict outer cutoff before comparing the two relevant fields.

noncomputable def MIPRE.Introspection.AuxiliaryProgram.andCheck {α : Type u_1} [Cost.SizedEncoding α] (f g : Cost.PolyTimeFun α Bool) : Cost.PolyTimeFun α Bool

Equations

• MIPRE.Introspection.AuxiliaryProgram.andCheck f g = f.ite g (MIPRE.Cost.PolyTimeFun.const false)

theorem MIPRE.Introspection.AuxiliaryProgram.andCheck_iff {α : Type u_1} [Cost.SizedEncoding α] (f g : Cost.PolyTimeFun α Bool) (x : α) : (andCheck f g).toFun x = true ↔ f.toFun x = true ∧ g.toFun x = true

noncomputable def MIPRE.Introspection.AuxiliaryProgram.equal {α : Type u_1} [Cost.SizedEncoding α] {β : Type u_2} [Cost.SizedEncoding β] (f g : Cost.PolyTimeFun α β) : Cost.PolyTimeFun α Bool

Equations

• MIPRE.Introspection.AuxiliaryProgram.equal f g = MIPRE.Cost.PolyTimeFun.treeEq.ap₂ (MIPRE.CL.Detyping.Program.encoded.comp f) (MIPRE.CL.Detyping.Program.encoded.comp g)

theorem MIPRE.Introspection.AuxiliaryProgram.equal_iff {α : Type u_1} [Cost.SizedEncoding α] {β : Type u_2} [Cost.SizedEncoding β] (f g : Cost.PolyTimeFun α β) (x : α) : (equal f g).toFun x = true ↔ f.toFun x = g.toFun x

noncomputable def MIPRE.Introspection.AuxiliaryProgram.rightTriple : Cost.PolyTimeFun SourceCompiler.GuardInput (Cost.BitStr × Cost.BitStr × Cost.BitStr)

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryProgram.outerCheck : Cost.PolyTimeFun SourceCompiler.GuardInput Bool

Equations

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

theorem MIPRE.Introspection.AuxiliaryProgram.outerCheck_iff (x : SourceCompiler.GuardInput) : outerCheck.toFun x = true ↔ List.length (SourceCompiler.inputLeft.toFun x) < 8 * SourceCompiler.inputQ.toFun x ∧ List.length (SourceCompiler.inputRight.toFun x) < 8 * SourceCompiler.inputQ.toFun x

noncomputable def MIPRE.Introspection.AuxiliaryProgram.pairLeft : Cost.PolyTimeFun SourceCompiler.GuardInput Bool

Full-Q pair format, including the original answer cutoff.

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryProgram.pairRight : Cost.PolyTimeFun SourceCompiler.GuardInput Bool

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryProgram.readRight : Cost.PolyTimeFun SourceCompiler.GuardInput Bool

Full-Q Read format: there is deliberately no original-subspace test on the dual field.

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryProgram.readingCheck : Cost.PolyTimeFun SourceCompiler.GuardInput Bool

The actual Introspect/Read branch, with all bounds supplied in binary.

Equations

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

theorem MIPRE.Introspection.AuxiliaryProgram.readingCheck_iff (x : SourceCompiler.GuardInput) : readingCheck.toFun x = true ↔ List.length (SourceCompiler.inputLeft.toFun x) < 8 * SourceCompiler.inputQ.toFun x ∧ List.length (SourceCompiler.inputRight.toFun x) < 8 * SourceCompiler.inputQ.toFun x ∧ AnswerParser.pairValid (SourceCompiler.inputQ.toFun x) (SourceCompiler.inputR.toFun x) (SourceCompiler.inputLeft.toFun x) ∧ AnswerParser.tripleValid (SourceCompiler.inputQ.toFun x) (SourceCompiler.inputR.toFun x) false (SourceCompiler.inputRight.toFun x) ∧ (SourceCompiler.leftParts.toFun x).1 = (rightTriple.toFun x).1 ∧ (SourceCompiler.leftParts.toFun x).2 = (rightTriple.toFun x).2.2

theorem MIPRE.Introspection.AuxiliaryProgram.toBits_injective {Q : ℕ} : Function.Injective CL.toBits

theorem MIPRE.Introspection.AuxiliaryProgram.readingCheck_vectors {Q R : ℕ} (hQ : 4 ≤ Q) (hR : 3 * R ≤ Q) (n s : ℕ) (y z zp : Fin Q → CL.𝔽₂) (a b : Cost.BitStr) : readingCheck.toFun (n, Q, R, s, AnswerParser.pairBits (CL.toBits y) a, AnswerParser.tripleBits (CL.toBits z) (CL.toBits zp) b) = true ↔ List.length a ≤ R ∧ List.length b ≤ R ∧ CLChecks.reading (y, a) (z, zp, b)

Exact acceptance on full-register parsed answers, including arbitrary dual labels.

noncomputable def MIPRE.Introspection.AuxiliaryProgram.rawCheck (check : Cost.PolyTimeFun SourceCompiler.GuardInput Bool) : Cost.PolyTimeFun Cost.Data Bool

Reject arbitrary noncanonical input trees before running the supplied pure check.

Equations

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

@[simp]

theorem MIPRE.Introspection.AuxiliaryProgram.rawCheck_encode (check : Cost.PolyTimeFun SourceCompiler.GuardInput Bool) (x : SourceCompiler.GuardInput) : (rawCheck check).toFun (Cost.encode x) = check.toFun x

theorem MIPRE.Introspection.AuxiliaryProgram.rawCheck_haltsWithin (check : Cost.PolyTimeFun SourceCompiler.GuardInput Bool) (x : Cost.Data) : Cost.HaltsWithin (rawCheck check).code x (Polynomial.eval x.size (rawCheck check).timeBound)

Total runtime on every raw tree, independently of source-program termination.

theorem MIPRE.Introspection.AuxiliaryProgram.readingCheck_typed {PauliType : Type u_1} {PauliAnswer : Type u_2} {Q R ℓ : ℕ} (L : Bool → CL.CLFun CL.𝔽₂ (Fin Q) ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → Fin Q → CL.𝔽₂) (D : (Fin Q → CL.𝔽₂) → (Fin Q → CL.𝔽₂) → Cost.BitStr → Cost.BitStr → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (hQ : 4 ≤ Q) (hR : 3 * R ≤ Q) (n s : ℕ) (w : Bool) (y z zp : Fin Q → CL.𝔽₂) (a b : Cost.BitStr) : readingCheck.toFun (n, Q, R, s, AnswerParser.pairBits (CL.toBits y) a, AnswerParser.tripleBits (CL.toBits z) (CL.toBits zp) b) = true ↔ List.length a ≤ R ∧ List.length b ≤ R ∧ TypedPredicate.check L X Z projectPauli D DP (Sum.inr (AuxType.introspect, w)) (Sum.inr (AuxType.read, w)) (ParsedAnswer.pair y a) (ParsedAnswer.read z zp b) = true