A total clocked full-register sampling check

The program reads (level, role, n, Q, R, s, left, right) with binary parameters. Both answers contain Q-bit registers; only the Introspect register must vanish past s. The Sample seed is freely supported on the full register. The actual source marginal query receives its first s bits at index 2^n. A timeout or malformed source result rejects.

@[reducible, inline]

abbrev MIPRE.Introspection.AuxiliaryProgram.SamplingInput : Type

Equations

• MIPRE.Introspection.AuxiliaryProgram.SamplingInput = (ℕ × Bool × MIPRE.Introspection.SourceCompiler.GuardInput)

noncomputable def MIPRE.Introspection.AuxiliaryProgram.samplingLevel : Cost.PolyTimeFun SamplingInput ℕ

Equations

• MIPRE.Introspection.AuxiliaryProgram.samplingLevel = MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.Introspection.AuxiliaryProgram.samplingRole : Cost.PolyTimeFun SamplingInput Bool

Equations

• MIPRE.Introspection.AuxiliaryProgram.samplingRole = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Introspection.AuxiliaryProgram.samplingFields : Cost.PolyTimeFun SamplingInput SourceCompiler.GuardInput

Equations

• MIPRE.Introspection.AuxiliaryProgram.samplingFields = MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Introspection.AuxiliaryProgram.readRole : Cost.PolyTimeFun Cost.Data Bool

Equations

• MIPRE.Introspection.AuxiliaryProgram.readRole = MIPRE.Introspection.AuxiliaryProgram.equal (MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Data) (MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.encode true))

@[simp]

theorem MIPRE.Introspection.AuxiliaryProgram.readRole_encode (w : Bool) : readRole.toFun (Cost.encode w) = w

noncomputable def MIPRE.Introspection.AuxiliaryProgram.readSamplingInput : Cost.PolyTimeFun Cost.Data SamplingInput

Equations

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

@[simp]

theorem MIPRE.Introspection.AuxiliaryProgram.readSamplingInput_encode (x : SamplingInput) : readSamplingInput.toFun (Cost.encode x) = x

def MIPRE.Introspection.AuxiliaryProgram.SamplingReady (x : SamplingInput) : Prop

Equations

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

@[instance_reducible]

noncomputable instance MIPRE.Introspection.AuxiliaryProgram.instDecidableSamplingReady (x : SamplingInput) : Decidable (SamplingReady x)

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryProgram.samplingReady : Cost.PolyTimeFun SamplingInput Bool

Equations

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

theorem MIPRE.Introspection.AuxiliaryProgram.samplingReady_iff (x : SamplingInput) : samplingReady.toFun x = true ↔ SamplingReady x

def MIPRE.Introspection.AuxiliaryProgram.SamplingRawReady (x : Cost.Data) : Prop

Equations

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

@[instance_reducible]

noncomputable instance MIPRE.Introspection.AuxiliaryProgram.instDecidableSamplingRawReady (x : Cost.Data) : Decidable (SamplingRawReady x)

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryProgram.samplingCall : Cost.PolyTimeFun SamplingInput Cost.Data

The marginal query contains the original seed length, not the padded length.

Equations

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

theorem MIPRE.Introspection.AuxiliaryProgram.samplingCall_apply (x : SamplingInput) : samplingCall.toFun x = Cost.encode (SourceCompiler.inputIndex.toFun x.2.2, CL.Sampler.Query.marginal (Player.ofBool x.2.1) x.1 (List.take (SourceCompiler.inputDim.toFun x.2.2) (SourceCompiler.rightParts.toFun x.2.2).1))

noncomputable def MIPRE.Introspection.AuxiliaryProgram.samplingRoute : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

Equations

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

theorem MIPRE.Introspection.AuxiliaryProgram.samplingRoute_apply (x : Cost.Data) : samplingRoute.toFun x = if SamplingRawReady x then (true, (samplingCall.toFun (readSamplingInput.toFun x)).cons x) else (false, Cost.encode false)

noncomputable def MIPRE.Introspection.AuxiliaryProgram.samplingExpected : Cost.PolyTimeFun SamplingInput Cost.Data

Equations

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

theorem MIPRE.Introspection.AuxiliaryProgram.samplingExpected_apply (x : SamplingInput) : samplingExpected.toFun x = (Cost.encode true).cons (Cost.encode (List.take (SourceCompiler.inputDim.toFun x.2.2) (SourceCompiler.leftParts.toFun x.2.2).1))

noncomputable def MIPRE.Introspection.AuxiliaryProgram.samplingPost : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

Equations

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

theorem MIPRE.Introspection.AuxiliaryProgram.samplingPost_apply (x r : Cost.Data) : samplingPost.toFun (x, r) = Cost.encode (decide (r = samplingExpected.toFun (readSamplingInput.toFun x)))

noncomputable def MIPRE.Introspection.AuxiliaryProgram.samplingProg (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (S : Cost.Prog) : Cost.Prog

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryProgram.samplingResult (k lam : ℕ) (S : Cost.Prog) (x : SamplingInput) : Cost.Data

Equations

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

theorem MIPRE.Introspection.AuxiliaryProgram.samplingProg_run (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (S : Cost.Prog) (x : Cost.Data) : ∃ (t : ℕ), (samplingProg k lam U S).Runs x (if SamplingRawReady x then Cost.encode (decide (samplingResult k lam S (readSamplingInput.toFun x) = samplingExpected.toFun (readSamplingInput.toFun x))) else Cost.encode false) t

theorem MIPRE.Introspection.AuxiliaryProgram.samplingProg_accepts_iff (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (S : Cost.Prog) (x : Cost.Data) : (∃ (t : ℕ), (samplingProg k lam U S).Runs x (Cost.encode true) t) ↔ SamplingRawReady x ∧ samplingResult k lam S (readSamplingInput.toFun x) = samplingExpected.toFun (readSamplingInput.toFun x)