Legal source calls implement the padded query interface

An attained padded prefix restricts to an attained source prefix. The common exponent-five clock therefore answers every source call used to construct the padded factor and matrix, including the runtime dimension call.

def MIPRE.Introspection.SourcePadding.Program.sourceFamily {ℓ : ℕ} (V : Verifier ℓ) (n : ℕ) (w : Bool) : CL.CLFun CL.𝔽₂ (Fin (V.sampler.dim (2 ^ n))) ℓ

Equations

• MIPRE.Introspection.SourcePadding.Program.sourceFamily V n w = V.sampler.cl (2 ^ n) (MIPRE.Player.ofBool w)

def MIPRE.Introspection.SourcePadding.Program.queryContext {ℓ : ℕ} (V : Verifier ℓ) (lam n : ℕ) (w : Bool) (j : ℕ) {Q : ℕ} (u : Fin Q → CL.𝔽₂) : AuxiliarySource.Context

Equations

• MIPRE.Introspection.SourcePadding.Program.queryContext V lam n w j u = (MIPRE.Cost.unary (MIPRE.Introspection.ansBound 5 lam n), V.sampler.prog, 2 ^ n, w, j + 1, MIPRE.CL.toBits u)

theorem MIPRE.Introspection.SourcePadding.Program.queryContext_dimension (U : Cost.ClockedUniversalMachine) {ℓ lam n : ℕ} (V : Verifier ℓ) (hV : V.IsBounded lam) (hn : 1 ≤ n) (w : Bool) (j : ℕ) {Q : ℕ} (u : Fin Q → CL.𝔽₂) : (dimension U).toFun (queryContext V lam n w j u) = V.sampler.dim (2 ^ n)

theorem MIPRE.Introspection.SourcePadding.Program.source_prefix_attained {ℓ n Q : ℕ} (V : Verifier ℓ) (hQ : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) (j : ℕ) (u : Fin Q → CL.𝔽₂) (hu : ∃ (x : Fin Q → CL.𝔽₂), u = (CL.CLFun.truncate j (depthFamily (AuxiliaryProgram.firstEmbedding hQ) (sourceFamily V n) w)).eval x) : ∃ (x : Fin (V.sampler.dim (2 ^ n)) → CL.𝔽₂), List.take (V.sampler.dim (2 ^ n)) (CL.toBits u) = CL.toBits ((CL.CLFun.truncate j (V.sampler.cl (2 ^ n) (Player.ofBool w))).eval x)

theorem MIPRE.Introspection.SourcePadding.Program.factorFromContext_legal (U : Cost.ClockedUniversalMachine) {ℓ lam n Q : ℕ} (V : Verifier ℓ) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hQ : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) (j : ℕ) (hj : j < ℓ) (hjR : (j + 1).size ≤ (2 ^ n) ^ lam) (u : Fin Q → CL.𝔽₂) (hu : ∃ (x : Fin Q → CL.𝔽₂), u = (CL.CLFun.truncate j (depthFamily (AuxiliaryProgram.firstEmbedding hQ) (sourceFamily V n) w)).eval x) : (factorFromContext U).toFun (queryContext V lam n w j u) = CL.indicatorBits ((depthFamily (AuxiliaryProgram.firstEmbedding hQ) (sourceFamily V n) w).factorOfPrefix j u)

theorem MIPRE.Introspection.SourcePadding.Program.linear_legal (U : Cost.ClockedUniversalMachine) {ℓ lam n Q : ℕ} (V : Verifier ℓ) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hQ : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) (j : ℕ) (hj : j < ℓ) (hjR : (j + 1).size ≤ (2 ^ n) ^ lam) (u y : Fin Q → CL.𝔽₂) (hu : ∃ (x : Fin Q → CL.𝔽₂), u = (CL.CLFun.truncate j (depthFamily (AuxiliaryProgram.firstEmbedding hQ) (sourceFamily V n) w)).eval x) : (linear U).toFun (CL.toBits y, Cost.unary (V.sampler.dim (2 ^ n)), queryContext V lam n w j u) = CL.toBits (((depthFamily (AuxiliaryProgram.firstEmbedding hQ) (sourceFamily V n) w).mapOfPrefix j u) y)

theorem MIPRE.Introspection.SourcePadding.Program.matrixFromContext_legal (U : Cost.ClockedUniversalMachine) {ℓ lam n Q : ℕ} (V : Verifier ℓ) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hQ : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) (j : ℕ) (hj : j < ℓ) (hjR : (j + 1).size ≤ (2 ^ n) ^ lam) (u : Fin Q → CL.𝔽₂) (hu : ∃ (x : Fin Q → CL.𝔽₂), u = (CL.CLFun.truncate j (depthFamily (AuxiliaryProgram.firstEmbedding hQ) (sourceFamily V n) w)).eval x) : (matrixFromContext U).toFun (queryContext V lam n w j u) = LowDegree.BinaryLinear.matrixBits (LinearMap.toMatrix' ((depthFamily (AuxiliaryProgram.firstEmbedding hQ) (sourceFamily V n) w).mapOfPrefix j u))