Uniform programs for queries to a padded source

Source width is input data. The full register width is read from the prefix. Source queries receive only the original prefix and vector coordinates; their answers are extended to the full register. The first factor consumes the unused suffix and all later factors leave it empty.

@[reducible, inline]

abbrev MIPRE.Introspection.SourcePadding.Program.QContext : Type

Equations

• MIPRE.Introspection.SourcePadding.Program.QContext = (MIPRE.Cost.Unary × MIPRE.Introspection.AuxiliarySource.Context)

noncomputable def MIPRE.Introspection.SourcePadding.Program.sourceWidth : Cost.PolyTimeFun QContext Cost.Unary

Equations

• MIPRE.Introspection.SourcePadding.Program.sourceWidth = MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.Introspection.SourcePadding.Program.fullWidth : Cost.PolyTimeFun QContext Cost.Unary

Equations

• MIPRE.Introspection.SourcePadding.Program.fullWidth = MIPRE.Cost.PolyTimeFun.length.comp (MIPRE.Introspection.AuxiliarySource.inputPrefix.comp MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.Introspection.SourcePadding.Program.suffixWidth : Cost.PolyTimeFun QContext Cost.Unary

Equations

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

noncomputable def MIPRE.Introspection.SourcePadding.Program.sourceContext : Cost.PolyTimeFun QContext AuxiliarySource.Context

Equations

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

theorem MIPRE.Introspection.SourcePadding.Program.sourceContext_apply (s b : Cost.Unary) (S : Cost.Prog) (n : ℕ) (w : Bool) (j : ℕ) (u : Cost.BitStr) : sourceContext.toFun (s, b, S, n, w, j, u) = (b, S, n, w, j, List.take (List.length s) u)

noncomputable def MIPRE.Introspection.SourcePadding.Program.linear (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun (Cost.BitStr × QContext) Cost.BitStr

Equations

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

theorem MIPRE.Introspection.SourcePadding.Program.linear_apply (U : Cost.ClockedUniversalMachine) (y : Cost.BitStr) (s : Cost.Unary) (ctx : AuxiliarySource.Context) : (linear U).toFun (y, s, ctx) = (AuxiliarySource.linear U).toFun (List.take (List.length s) y, sourceContext.toFun (s, ctx)) ++ List.replicate (List.length (AuxiliarySource.inputPrefix.toFun ctx) - List.length s) false

noncomputable def MIPRE.Introspection.SourcePadding.Program.factor (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun QContext Cost.BitStr

Equations

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

theorem MIPRE.Introspection.SourcePadding.Program.factor_apply (U : Cost.ClockedUniversalMachine) (s : Cost.Unary) (ctx : AuxiliarySource.Context) : (factor U).toFun (s, ctx) = (AuxiliarySource.factor U).toFun (sourceContext.toFun (s, ctx)) ++ List.replicate (List.length (AuxiliarySource.inputPrefix.toFun ctx) - List.length s) (decide (AuxiliarySource.level.toFun ctx = 1))

noncomputable def MIPRE.Introspection.SourcePadding.Program.matrix (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun QContext (List Cost.BitStr)

Equations

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

theorem MIPRE.Introspection.SourcePadding.Program.toBits_pull_first {s Q : ℕ} (h : s ≤ Q) (x : Fin Q → CL.𝔽₂) : CL.toBits (CL.pull (AuxiliaryProgram.firstEmbedding h) x) = List.take s (CL.toBits x)

theorem MIPRE.Introspection.SourcePadding.Program.linear_correct (U : Cost.ClockedUniversalMachine) {s Q : ℕ} (h : s ≤ Q) (ctx : AuxiliarySource.Context) (u y : Fin Q → CL.𝔽₂) (v : Fin s → CL.𝔽₂) (hu : AuxiliarySource.inputPrefix.toFun ctx = CL.toBits u) (hv : (AuxiliarySource.linear U).toFun (CL.toBits (CL.pull (AuxiliaryProgram.firstEmbedding h) y), sourceContext.toFun (Cost.unary s, ctx)) = CL.toBits v) : (linear U).toFun (CL.toBits y, Cost.unary s, ctx) = CL.toBits (CL.push (AuxiliaryProgram.firstEmbedding h) v)

theorem MIPRE.Introspection.SourcePadding.Program.indicatorBits_padding {s Q : ℕ} (h : s ≤ Q) (S : Finset (Fin s)) (first : Bool) : CL.indicatorBits (Finset.map (AuxiliaryProgram.firstEmbedding h) S ∪ if first = true then (Finset.map (AuxiliaryProgram.firstEmbedding h) Finset.univ)ᶜ else ∅) = CL.indicatorBits S ++ List.replicate (Q - s) first

theorem MIPRE.Introspection.SourcePadding.Program.factor_correct (U : Cost.ClockedUniversalMachine) {s Q ℓ : ℕ} (h : s ≤ Q) (L : Bool → CL.CLFun CL.𝔽₂ (Fin s) ℓ) (hℓ : 0 < ℓ) (w : Bool) (j : ℕ) (ctx : AuxiliarySource.Context) (u : Fin Q → CL.𝔽₂) (hu : AuxiliarySource.inputPrefix.toFun ctx = CL.toBits u) (hj : AuxiliarySource.level.toFun ctx = j + 1) (hf : (AuxiliarySource.factor U).toFun (sourceContext.toFun (Cost.unary s, ctx)) = CL.indicatorBits ((L w).factorOfPrefix j (CL.pull (AuxiliaryProgram.firstEmbedding h) u))) : (factor U).toFun (Cost.unary s, ctx) = CL.indicatorBits ((depthFamily (AuxiliaryProgram.firstEmbedding h) L w).factorOfPrefix j u)

theorem MIPRE.Introspection.SourcePadding.Program.matrix_correct (U : Cost.ClockedUniversalMachine) (ctx : QContext) {Q : ℕ} (L : (Fin Q → CL.𝔽₂) →ₗ[CL.𝔽₂] Fin Q → CL.𝔽₂) (hn : List.length (AuxiliarySource.inputPrefix.toFun ctx.2) = Q) (h : ∀ (x : Fin Q → CL.𝔽₂), (linear U).toFun (LowDegree.BinaryLinear.vectorBits x, ctx) = LowDegree.BinaryLinear.vectorBits (L x)) : (matrix U).toFun ctx = LowDegree.BinaryLinear.matrixBits (LinearMap.toMatrix' L)

noncomputable def MIPRE.Introspection.SourcePadding.Program.dimension (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun AuxiliarySource.Context ℕ

Read the source dimension with the already supplied source clock.

Equations

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

theorem MIPRE.Introspection.SourcePadding.Program.dimension_correct (U : Cost.ClockedUniversalMachine) (ctx : AuxiliarySource.Context) (s : ℕ) (h : Cost.clockedResult (AuxiliarySource.source.toFun ctx) (Cost.encode (AuxiliarySource.index.toFun ctx, CL.Sampler.Query.dimension)) (List.length (AuxiliarySource.budget.toFun ctx)) = (Cost.encode true).cons (Cost.encode s)) : (dimension U).toFun ctx = s

noncomputable def MIPRE.Introspection.SourcePadding.Program.adapt (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun AuxiliarySource.Context QContext

Cap the dimension by the actual full prefix length before creating unary data. Consequently arbitrary dimension-query results cannot cause large allocation.

Equations

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

theorem MIPRE.Introspection.SourcePadding.Program.adapt_correct (U : Cost.ClockedUniversalMachine) (ctx : AuxiliarySource.Context) (s : ℕ) (hs : s ≤ List.length (AuxiliarySource.inputPrefix.toFun ctx)) (hd : (dimension U).toFun ctx = s) : (adapt U).toFun ctx = (Cost.unary s, ctx)

noncomputable def MIPRE.Introspection.SourcePadding.Program.factorFromContext (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr

The original scan context is sufficient: width is queried at runtime.

Equations

• MIPRE.Introspection.SourcePadding.Program.factorFromContext U = (MIPRE.Introspection.SourcePadding.Program.factor U).comp (MIPRE.Introspection.SourcePadding.Program.adapt U)

noncomputable def MIPRE.Introspection.SourcePadding.Program.matrixFromContext (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)

Equations

• MIPRE.Introspection.SourcePadding.Program.matrixFromContext U = (MIPRE.Introspection.SourcePadding.Program.matrix U).comp (MIPRE.Introspection.SourcePadding.Program.adapt U)

theorem MIPRE.Introspection.SourcePadding.Program.factorFromContext_correct (U : Cost.ClockedUniversalMachine) (ctx : AuxiliarySource.Context) (s : ℕ) (hs : s ≤ List.length (AuxiliarySource.inputPrefix.toFun ctx)) (hd : (dimension U).toFun ctx = s) : (factorFromContext U).toFun ctx = (factor U).toFun (Cost.unary s, ctx)

theorem MIPRE.Introspection.SourcePadding.Program.matrixFromContext_correct (U : Cost.ClockedUniversalMachine) (ctx : AuxiliarySource.Context) (s : ℕ) (hs : s ≤ List.length (AuxiliarySource.inputPrefix.toFun ctx)) (hd : (dimension U).toFun ctx = s) : (matrixFromContext U).toFun ctx = (matrix U).toFun (Cost.unary s, ctx)