The auxiliary constraints of the introspection processor

Issue #281. At a pair of auxiliary labels t, u (fixed: the processor branches on the edge over the finite label alphabet) and two readable answers aR, bR, the constraints AuxCons.auxPair of Typed.consRaw as a Cost.PolyTimeFun on the environment and the two answers (DIn): the readable conditions at both registers (GP), the consistency list (sameP), and the directed lists of both orientations (dirP), assembled by auxPairF.

The data of each clause are read off the kernel's context (CLData) and the clocked runs of the input's programs (InputRuns); the stage data are correct under the prefix guards, which the readable conditions contain, so dirP_spec assumes them and auxPairP_spec does not.

Two answers in the environment

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.LpIntro.DIn : Type

The environment and two readable answers.

Equations

• MIPRE.Tailored.Intro.LpIntro.DIn = (MIPRE.Tailored.Intro.LpIntro.Env × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr)

noncomputable def MIPRE.Tailored.Intro.LpIntro.dE : Cost.PolyTimeFun DIn Env

Equations

• MIPRE.Tailored.Intro.LpIntro.dE = MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.Tailored.Intro.LpIntro.dA : Cost.PolyTimeFun DIn Cost.BitStr

Equations

• MIPRE.Tailored.Intro.LpIntro.dA = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Tailored.Intro.LpIntro.dB : Cost.PolyTimeFun DIn Cost.BitStr

Equations

• MIPRE.Tailored.Intro.LpIntro.dB = MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.dE_apply (d : DIn) : dE.toFun d = d.1

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.dA_apply (d : DIn) : dA.toFun d = d.2.1

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.dB_apply (d : DIn) : dB.toFun d = d.2.2

noncomputable def MIPRE.Tailored.Intro.LpIntro.swapD : Cost.PolyTimeFun DIn DIn

The answers swapped.

Equations

• MIPRE.Tailored.Intro.LpIntro.swapD = MIPRE.Tailored.Intro.LpIntro.dE.pair (MIPRE.Tailored.Intro.LpIntro.dB.pair MIPRE.Tailored.Intro.LpIntro.dA)

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.swapD_apply (e : Env) (a b : Cost.BitStr) : swapD.toFun (e, a, b) = (e, b, a)

noncomputable def MIPRE.Tailored.Intro.LpIntro.winF (a : Cost.PolyTimeFun DIn Cost.BitStr) (o m : Cost.PolyTimeFun DIn Cost.Unary) : Cost.PolyTimeFun DIn Cost.BitStr

The window win a o m, o and m in unary.

Equations

• MIPRE.Tailored.Intro.LpIntro.winF a o m = MIPRE.Tailored.Intro.takeOf (MIPRE.Tailored.Intro.dropOf a o) m

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.winF_apply (a : Cost.PolyTimeFun DIn Cost.BitStr) (o m : Cost.PolyTimeFun DIn Cost.Unary) (d : DIn) : (winF a o m).toFun d = win (a.toFun d) (List.length (o.toFun d)) (List.length (m.toFun d))

noncomputable def MIPRE.Tailored.Intro.LpIntro.regOf (a : Cost.PolyTimeFun DIn Cost.BitStr) : Cost.PolyTimeFun DIn Cost.BitStr

The register win a 0 Q of an answer.

Equations

• MIPRE.Tailored.Intro.LpIntro.regOf a = MIPRE.Tailored.Intro.takeOf a (MIPRE.Tailored.Intro.LpIntro.eQ.comp MIPRE.Tailored.Intro.LpIntro.dE)

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.regOf_apply (a : Cost.PolyTimeFun DIn Cost.BitStr) (d : DIn) : (regOf a).toFun d = win (a.toFun d) 0 (List.length d.1.2.2.2.2.1)

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Intro.LpIntro.ya : Cost.PolyTimeFun DIn Cost.BitStr

The two registers.

Equations

• MIPRE.Tailored.Intro.LpIntro.ya = MIPRE.Tailored.Intro.LpIntro.regOf MIPRE.Tailored.Intro.LpIntro.dA

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Intro.LpIntro.yb : Cost.PolyTimeFun DIn Cost.BitStr

Equations

• MIPRE.Tailored.Intro.LpIntro.yb = MIPRE.Tailored.Intro.LpIntro.regOf MIPRE.Tailored.Intro.LpIntro.dB

noncomputable def MIPRE.Tailored.Intro.LpIntro.atReg {X : Type} [Cost.SizedEncoding X] (F : Cost.PolyTimeFun RIn X) (y : Cost.PolyTimeFun DIn Cost.BitStr) : Cost.PolyTimeFun DIn X

A register-level program at a computed register.

Equations

• MIPRE.Tailored.Intro.LpIntro.atReg F y = F.comp (MIPRE.Tailored.Intro.LpIntro.dE.pair y)

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.atReg_apply {X : Type} [Cost.SizedEncoding X] (F : Cost.PolyTimeFun RIn X) (y : Cost.PolyTimeFun DIn Cost.BitStr) (d : DIn) : (atReg F y).toFun d = F.toFun (d.1, y.toFun d)

noncomputable def MIPRE.Tailored.Intro.LpIntro.kAt {X : Type} [Cost.SizedEncoding X] (F : Cost.PolyTimeFun CLData.Input X) (w : Bool) (y : Cost.PolyTimeFun DIn Cost.BitStr) : Cost.PolyTimeFun DIn X

A kernel datum of role w at a computed register.

Equations

• MIPRE.Tailored.Intro.LpIntro.kAt F w y = F.comp (((MIPRE.Tailored.Intro.LpIntro.ctxP w).comp MIPRE.Tailored.Intro.LpIntro.dE).pair y)

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.kAt_apply {X : Type} [Cost.SizedEncoding X] (F : Cost.PolyTimeFun CLData.Input X) (w : Bool) (y : Cost.PolyTimeFun DIn Cost.BitStr) (d : DIn) : (kAt F w y).toFun d = F.toFun ((ctxP w).toFun d.1, y.toFun d)

noncomputable def MIPRE.Tailored.Intro.LpIntro.qr : Cost.PolyTimeFun DIn (Cost.Unary × Cost.Unary)

(Q, R).

Equations

• MIPRE.Tailored.Intro.LpIntro.qr = (MIPRE.Tailored.Intro.LpIntro.eQ.comp MIPRE.Tailored.Intro.LpIntro.dE).pair (MIPRE.Tailored.Intro.LpIntro.eR.comp MIPRE.Tailored.Intro.LpIntro.dE)

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.qr_apply (d : DIn) : qr.toFun d = (d.1.2.2.2.2.1, d.1.2.2.2.2.2)

noncomputable def MIPRE.Tailored.Intro.LpIntro.eqB (a b : Cost.PolyTimeFun DIn Cost.BitStr) : Cost.PolyTimeFun DIn Bool

Equality of two computed bit strings.

Equations

• MIPRE.Tailored.Intro.LpIntro.eqB a b = MIPRE.SAT.ArrayProg.eqBits.ap₂ a b

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.eqB_apply (a b : Cost.PolyTimeFun DIn Cost.BitStr) (d : DIn) : (eqB a b).toFun d = decide (a.toFun d = b.toFun d)

The clauses

noncomputable def MIPRE.Tailored.Intro.LpIntro.srcEqB (U : Cost.ClockedUniversalMachine) (t u : Introspection.AuxType 7 × Bool) : Cost.PolyTimeFun DIn Bool

The input-answer equality between label t at aR and label u at bR: equal splits and equal readable input answers.

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.sameP (U : Cost.ClockedUniversalMachine) (t : Introspection.AuxType 7 × Bool) : Cost.PolyTimeFun DIn (List Cost.BitStr)

Consistency at the label t: sameCons.

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.sampleP (U : Cost.ClockedUniversalMachine) (w : Bool) : Cost.PolyTimeFun DIn (List Cost.BitStr)

The sampling comparison: sampleCons.

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.readP (U : Cost.ClockedUniversalMachine) (w : Bool) : Cost.PolyTimeFun DIn (List Cost.BitStr)

The reading comparison: readCons.

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.hideReadP (U : Cost.ClockedUniversalMachine) (w : Bool) : Cost.PolyTimeFun DIn (List Cost.BitStr)

The last Hide against Read: hideReadCons.

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.hideNextP (U : Cost.ClockedUniversalMachine) (w : Bool) (k : ℕ) : Cost.PolyTimeFun DIn (List Cost.BitStr)

Consecutive Hide levels k, k + 1: hideNextCons.

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.sourceP (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun DIn (List Cost.BitStr)

The source game's constraints: the input's processor at the two Introspect registers.

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.dirP (U : Cost.ClockedUniversalMachine) : Introspection.AuxType 7 × Bool → Introspection.AuxType 7 × Bool → Cost.PolyTimeFun DIn (List Cost.BitStr)

One orientation of the directed auxiliary checks: dirAux.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Tailored.Intro.LpIntro.dirP U (MIPRE.Introspection.AuxType.introspect, false) (MIPRE.Introspection.AuxType.introspect, true) = MIPRE.Tailored.Intro.LpIntro.sourceP U
• MIPRE.Tailored.Intro.LpIntro.dirP U x✝¹ x✝ = MIPRE.Cost.PolyTimeFun.const []

noncomputable def MIPRE.Tailored.Intro.LpIntro.auxLenU (t : Introspection.AuxType 7 × Bool) : Cost.PolyTimeFun DIn Cost.Unary

The length of a label's answers: auxLen.

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.auxPairP (U : Cost.ClockedUniversalMachine) (t u : Introspection.AuxType 7 × Bool) : Cost.PolyTimeFun DIn (List Cost.BitStr)

The constraints at a pair of auxiliary labels: auxPair.

Equations

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

Correctness

theorem MIPRE.Tailored.Intro.LpIntro.envT_Q (c lam n : ℕ) (T : TailoredVerifier 7) : (envT c lam n T).2.2.2.2.1 = Cost.unary (QQ c lam n)

theorem MIPRE.Tailored.Intro.LpIntro.envT_R (c lam n : ℕ) (T : TailoredVerifier 7) : (envT c lam n T).2.2.2.2.2 = Cost.unary ((2 ^ n) ^ lam)

theorem MIPRE.Tailored.Intro.LpIntro.length_win_Q {a : Cost.BitStr} {Q : ℕ} (h : Q ≤ List.length a) : List.length (win a 0 Q) = Q

theorem MIPRE.Tailored.Intro.LpIntro.srcEqB_envT (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hsamp : V.sampler.prog = T.sampler.prog) (hs : V.sampler.dim (2 ^ n) ≤ QQ c lam n) (t u : Introspection.AuxType 7 × Bool) (aR bR : Cost.BitStr) (ha : QQ c lam n ≤ List.length aR) (hb : QQ c lam n ≤ List.length bR) : (srcEqB U t u).toFun (envT c lam n T, aR, bR) = decide (srcSplitR T V hs t (win aR 0 (QQ c lam n)) = srcSplitR T V hs u (win bR 0 (QQ c lam n)) ∧ srcSplitL T V hs t (win aR 0 (QQ c lam n)) = srcSplitL T V hs u (win bR 0 (QQ c lam n)) ∧ win aR (QQ c lam n) (srcSplitR T V hs t (win aR 0 (QQ c lam n))) = win bR (QQ c lam n) (srcSplitR T V hs u (win bR 0 (QQ c lam n))))

theorem MIPRE.Tailored.Intro.LpIntro.sameP_spec (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hsamp : V.sampler.prog = T.sampler.prog) (hs : V.sampler.dim (2 ^ n) ≤ QQ c lam n) (t : Introspection.AuxType 7 × Bool) (aR bR : Cost.BitStr) (ha : QQ c lam n ≤ List.length aR) (hb : QQ c lam n ≤ List.length bR) : (sameP U t).toFun (envT c lam n T, aR, bR) = sameCons (QQ c lam n) ((2 ^ n) ^ lam) (srcSplitR T V hs) (srcSplitL T V hs) t aR bR

Consistency at a label.

theorem MIPRE.Tailored.Intro.LpIntro.toBits_inj {s : ℕ} {a b : Fin s → CL.𝔽₂} : CL.toBits a = CL.toBits b ↔ a = b

theorem MIPRE.Tailored.Intro.LpIntro.decide_eq_toBits {Q : ℕ} {y : Cost.BitStr} (hy : List.length y = Q) (X : Fin Q → CL.𝔽₂) : decide (y = CL.toBits X) = decide (CL.ofBits Q y = X)

theorem MIPRE.Tailored.Intro.LpIntro.regKerGens_toBits (Q : ℕ) (S : Finset (Fin Q)) (M : CL.RegLinear CL.𝔽₂ S) : List.map CL.toBits (regKerGens Q S M) = LowDegree.BinaryLinear.kernelGeneratorsProg.toFun (Cost.unary Q, LowDegree.BinaryLinear.matrixBits (LinearMap.toMatrix' M.toLinearMap))

The kernel generators of regKerGens, as bit strings, are the solver's output.

theorem MIPRE.Tailored.Intro.LpIntro.lenOf_le {T : TailoredVerifier 7} {lam m : ℕ} (hT : T.IsBounded lam) (hm : 2 ≤ m) (x : Cost.BitStr) (κ : Bool) : T.lenOf m x κ ≤ m ^ lam

A λ-bounded tailored verifier's lengths are at most m^λ.

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Intro.LpIntro.LL (V : Verifier 7) {n Q : ℕ} (hs : V.sampler.dim (2 ^ n) ≤ Q) : Bool → CL.CLFun CL.𝔽₂ (Fin Q) 7

The padded CL functions of the input.

Equations

• MIPRE.Tailored.Intro.LpIntro.LL V hs = MIPRE.Introspection.AuxiliaryDecision.padded V hs

theorem MIPRE.Tailored.Intro.LpIntro.kAt_envT {c lam n : ℕ} (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hsamp : V.sampler.prog = T.sampler.prog) {X : Type} [Cost.SizedEncoding X] (F : Cost.PolyTimeFun CLData.Input X) (w : Bool) (y : Cost.PolyTimeFun DIn Cost.BitStr) (aR bR : Cost.BitStr) : (kAt F w y).toFun (envT c lam n T, aR, bR) = F.toFun (CLData.context V lam n (QQ c lam n) w, y.toFun (envT c lam n T, aR, bR))

theorem MIPRE.Tailored.Intro.LpIntro.sampleP_spec (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hsamp : V.sampler.prog = T.sampler.prog) (hs : V.sampler.dim (2 ^ n) ≤ QQ c lam n) (w : Bool) (aR bR : Cost.BitStr) (ha : QQ c lam n ≤ List.length aR) (hb : QQ c lam n ≤ List.length bR) : (sampleP U w).toFun (envT c lam n T, aR, bR) = sampleCons (QQ c lam n) ((2 ^ n) ^ lam) (srcSplitR T V hs) (srcSplitL T V hs) (LL V hs) w aR bR

The sampling comparison.

theorem MIPRE.Tailored.Intro.LpIntro.readP_spec (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hsamp : V.sampler.prog = T.sampler.prog) (hs : V.sampler.dim (2 ^ n) ≤ QQ c lam n) (w : Bool) (aR bR : Cost.BitStr) (ha : QQ c lam n ≤ List.length aR) (hb : QQ c lam n ≤ List.length bR) : (readP U w).toFun (envT c lam n T, aR, bR) = readCons (QQ c lam n) ((2 ^ n) ^ lam) (srcSplitR T V hs) (srcSplitL T V hs) w aR bR

The reading comparison.

theorem MIPRE.Tailored.Intro.LpIntro.outputPrefix_at (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ QQ c lam n) (w : Bool) {k : ℕ} (hk : k ≤ 7) (y : Cost.BitStr) (hy : List.length y = QQ c lam n) (hg : CLData.Guard V hs w (k - 1) (CL.ofBits (QQ c lam n) y)) : (CLData.outputPrefix U k).toFun (CLData.context V lam n (QQ c lam n) w, y) = CL.toBits ((LL V hs w).outputPrefix k (CL.ofBits (QQ c lam n) y))

theorem MIPRE.Tailored.Intro.LpIntro.hideReadP_spec (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hsamp : V.sampler.prog = T.sampler.prog) (hs : V.sampler.dim (2 ^ n) ≤ QQ c lam n) (w : Bool) (aR bR : Cost.BitStr) (ha : QQ c lam n ≤ List.length aR) (hb : QQ c lam n ≤ List.length bR) (hga : CLData.Guard V hs w 6 (CL.ofBits (QQ c lam n) (win aR 0 (QQ c lam n)))) (hgb : CLData.Guard V hs w 6 (CL.ofBits (QQ c lam n) (win bR 0 (QQ c lam n)))) : (hideReadP U w).toFun (envT c lam n T, aR, bR) = hideReadCons (QQ c lam n) ((2 ^ n) ^ lam) (LL V hs) w aR bR

The last Hide against Read, under the prefix guards at level 6.

theorem MIPRE.Tailored.Intro.LpIntro.hideNextP_spec (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hsamp : V.sampler.prog = T.sampler.prog) (hs : V.sampler.dim (2 ^ n) ≤ QQ c lam n) (w : Bool) (k : ℕ) (hk : k + 1 < 7) (aR bR : Cost.BitStr) (ha : QQ c lam n ≤ List.length aR) (hb : QQ c lam n ≤ List.length bR) (hga : CLData.Guard V hs w k (CL.ofBits (QQ c lam n) (win aR 0 (QQ c lam n)))) (hgb : CLData.Guard V hs w (k + 1) (CL.ofBits (QQ c lam n) (win bR 0 (QQ c lam n)))) : (hideNextP U w k).toFun (envT c lam n T, aR, bR) = hideNextCons (QQ c lam n) (LL V hs) (regKerGens (QQ c lam n)) w k aR bR

Consecutive Hide levels, under the prefix guards at k and k + 1.

theorem MIPRE.Tailored.Intro.LpIntro.envT_clock (c lam n : ℕ) (T : TailoredVerifier 7) : (envT c lam n T).1 = Cost.unary (Introspection.ansBound 5 lam n)

theorem MIPRE.Tailored.Intro.LpIntro.envT_M (c lam n : ℕ) (T : TailoredVerifier 7) : (envT c lam n T).2.1 = InputRuns.clamp.toFun (T.progs, lam)

theorem MIPRE.Tailored.Intro.LpIntro.envT_idx (c lam n : ℕ) (T : TailoredVerifier 7) : (envT c lam n T).2.2.1 = 2 ^ n

theorem MIPRE.Tailored.Intro.LpIntro.length_win_split_le {lam n : ℕ} (T : TailoredVerifier 7) (hT : T.IsBounded lam) (hn : 1 ≤ n) (aR : Cost.BitStr) (o : ℕ) (q : Cost.BitStr) (κ : Bool) : List.length (win aR o (T.lenOf (2 ^ n) q κ)) ≤ (2 ^ n) ^ lam

theorem MIPRE.Tailored.Intro.LpIntro.sourceP_spec (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hsamp : V.sampler.prog = T.sampler.prog) (hs : V.sampler.dim (2 ^ n) ≤ QQ c lam n) (aR bR : Cost.BitStr) (ha : QQ c lam n ≤ List.length aR) (hb : QQ c lam n ≤ List.length bR) : (sourceP U).toFun (envT c lam n T, aR, bR) = sourceCons (QQ c lam n) ((2 ^ n) ^ lam) (srcSplitR T V hs) (srcSplitL T V hs) (Typed.srcCons (kk c lam n) (jj c lam n) T V hs) aR bR

The source game's constraints.

theorem MIPRE.Tailored.Intro.LpIntro.dirP_spec (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hsamp : V.sampler.prog = T.sampler.prog) (hs : V.sampler.dim (2 ^ n) ≤ QQ c lam n) (t u : Introspection.AuxType 7 × Bool) (aR bR : Cost.BitStr) (ha : QQ c lam n ≤ List.length aR) (hb : QQ c lam n ≤ List.length bR) (hGa : Typed.G (kk c lam n) (jj c lam n) ((2 ^ n) ^ lam) T V hs t (win aR 0 (QQ c lam n))) (hGb : Typed.G (kk c lam n) (jj c lam n) ((2 ^ n) ^ lam) T V hs u (win bR 0 (QQ c lam n))) : (dirP U t u).toFun (envT c lam n T, aR, bR) = dirAux (QQ c lam n) ((2 ^ n) ^ lam) (srcSplitR T V hs) (srcSplitL T V hs) (LL V hs) (regKerGens (QQ c lam n)) (Typed.srcCons (kk c lam n) (jj c lam n) T V hs) t u aR bR

One orientation of the directed checks, under the readable conditions at both registers.

theorem MIPRE.Tailored.Intro.LpIntro.auxLenU_envT {c lam n : ℕ} (T : TailoredVerifier 7) (t : Introspection.AuxType 7 × Bool) (aR bR : Cost.BitStr) : (auxLenU t).toFun (envT c lam n T, aR, bR) = Cost.unary (auxLen (QQ c lam n) ((2 ^ n) ^ lam) t.1)

theorem MIPRE.Tailored.Intro.LpIntro.auxPairP_spec (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hsamp : V.sampler.prog = T.sampler.prog) (hs : V.sampler.dim (2 ^ n) ≤ QQ c lam n) (t u : Introspection.AuxType 7 × Bool) (aR bR : Cost.BitStr) (ha : List.length aR = auxLenR (QQ c lam n) ((2 ^ n) ^ lam) t.1) (hb : List.length bR = auxLenR (QQ c lam n) ((2 ^ n) ^ lam) u.1) : (auxPairP U t u).toFun (envT c lam n T, aR, bR) = auxPair (QQ c lam n) ((2 ^ n) ^ lam) (srcSplitR T V hs) (srcSplitL T V hs) (LL V hs) (Typed.G (kk c lam n) (jj c lam n) ((2 ^ n) ^ lam) T V hs) (regKerGens (QQ c lam n)) (Typed.srcCons (kk c lam n) (jj c lam n) T V hs) t u aR bR

The constraints at a pair of auxiliary labels, for readable answers of the labels' readable lengths.