The auxiliary comparisons of the introspection processor, in polynomial time

The clauses of the auxiliary checks between two answers of the padded layout (AuxCons.lean: sampleCons, readCons, hideReadCons, hideNextCons, sameCons, sourceCons) are lists of constraints determined by a few readable data: the register length Q and the original cutoff R, the readable conditions (as Booleans), the input's split of its answer at the register, the coordinate sets of the hiding stages (as bit masks), the generators of a kernel, and the input's own constraints. This file builds each clause as a Cost.PolyTimeFun of those data, computed elsewhere, with Q, R and the split in unary:

• sampleConsF, readConsF on ((Q, R), (guard, source guard), sL);
• hideReadConsF on ((Q, R), guard);
• hideNextConsF on (Q, guard, (masks), generators);
• sameConsF on ((Q, R), (hide?, read?), (guard, source guard), sL), the kind of the label given by two Booleans (isHideT, isReadT) so that one program serves every label;
• sourceConsF on ((Q, R), ((sRa, sLa), (sRb, sLb)), the input's constraints);
• auxLenF, the length auxLen of a label's answers, for the swap (swapConsF);
• auxPairF, the assembly auxPair at a pair of labels from the consistency list and the two directed lists (dirAux), computed by the caller.

Each _spec lemma states that on the encodings of the semantic data the program outputs the semantic list.

The forms on a generic input

noncomputable def MIPRE.Tailored.Intro.guardOf {ι : Type} [Cost.SizedEncoding ι] (b : Cost.PolyTimeFun ι Bool) (d : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List Cost.BitStr)

guardCons b d.

Equations

• MIPRE.Tailored.Intro.guardOf b d = MIPRE.Tailored.Intro.guardConsF.comp (b.pair d)

@[simp]

theorem MIPRE.Tailored.Intro.guardOf_apply {ι : Type} [Cost.SizedEncoding ι] (b : Cost.PolyTimeFun ι Bool) (d : Cost.PolyTimeFun ι Cost.Unary) (a : ι) : (guardOf b d).toFun a = guardCons (b.toFun a) (List.length (d.toFun a))

noncomputable def MIPRE.Tailored.Intro.eqOf {ι : Type} [Cost.SizedEncoding ι] (la lb oa ob m : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List Cost.BitStr)

eqCons la lb oa ob m.

Equations

• MIPRE.Tailored.Intro.eqOf la lb oa ob m = MIPRE.Tailored.Intro.eqConsF.comp (((la.pair oa).pair (lb.pair ob)).pair m)

@[simp]

theorem MIPRE.Tailored.Intro.eqOf_apply {ι : Type} [Cost.SizedEncoding ι] (la lb oa ob m : Cost.PolyTimeFun ι Cost.Unary) (a : ι) : (eqOf la lb oa ob m).toFun a = eqCons (List.length (la.toFun a)) (List.length (lb.toFun a)) (List.length (oa.toFun a)) (List.length (ob.toFun a)) (List.length (m.toFun a))

noncomputable def MIPRE.Tailored.Intro.projEqOf {ι : Type} [Cost.SizedEncoding ι] (la lb oa ob : Cost.PolyTimeFun ι Cost.Unary) (m : Cost.PolyTimeFun ι Cost.BitStr) : Cost.PolyTimeFun ι (List Cost.BitStr)

projEqCons la lb oa ob S, the set given by its mask.

Equations

• MIPRE.Tailored.Intro.projEqOf la lb oa ob m = MIPRE.Tailored.Intro.projEqConsF.comp (((la.pair oa).pair (lb.pair ob)).pair m)

@[simp]

theorem MIPRE.Tailored.Intro.projEqOf_apply {ι : Type} [Cost.SizedEncoding ι] (la lb oa ob : Cost.PolyTimeFun ι Cost.Unary) (m : Cost.PolyTimeFun ι Cost.BitStr) (a : ι) : (projEqOf la lb oa ob m).toFun a = projEqConsF.toFun (lay (List.length (la.toFun a)) (List.length (oa.toFun a)) (List.length (lb.toFun a)) (List.length (ob.toFun a)), m.toFun a)

noncomputable def MIPRE.Tailored.Intro.dualOf {ι : Type} [Cost.SizedEncoding ι] (la lb oa ob : Cost.PolyTimeFun ι Cost.Unary) (m : Cost.PolyTimeFun ι Cost.BitStr) (gs : Cost.PolyTimeFun ι (List Cost.BitStr)) : Cost.PolyTimeFun ι (List Cost.BitStr)

dualCons la lb oa ob S gens, the set given by its mask, the generators by their bits.

Equations

• MIPRE.Tailored.Intro.dualOf la lb oa ob m gs = MIPRE.Tailored.Intro.dualConsF.comp (((la.pair oa).pair (lb.pair ob)).pair (m.pair gs))

@[simp]

theorem MIPRE.Tailored.Intro.dualOf_apply {ι : Type} [Cost.SizedEncoding ι] (la lb oa ob : Cost.PolyTimeFun ι Cost.Unary) (m : Cost.PolyTimeFun ι Cost.BitStr) (gs : Cost.PolyTimeFun ι (List Cost.BitStr)) (a : ι) : (dualOf la lb oa ob m gs).toFun a = dualConsF.toFun (lay (List.length (la.toFun a)) (List.length (oa.toFun a)) (List.length (lb.toFun a)) (List.length (ob.toFun a)), m.toFun a, gs.toFun a)

noncomputable def MIPRE.Tailored.Intro.srcEqOf {ι : Type} [Cost.SizedEncoding ι] (la lb oLa oLb : Cost.PolyTimeFun ι Cost.Unary) (g : Cost.PolyTimeFun ι Bool) (s : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List Cost.BitStr)

The input-answer equality srcEqCons: the guard g on la + lb bits, and the equality of the linear windows at oLa, oLb, of length s.

Equations

• MIPRE.Tailored.Intro.srcEqOf la lb oLa oLb g s = MIPRE.Tailored.Intro.catF (MIPRE.Tailored.Intro.guardOf g (MIPRE.Tailored.Intro.catF la lb)) (MIPRE.Tailored.Intro.eqOf la lb oLa oLb s)

@[simp]

theorem MIPRE.Tailored.Intro.srcEqOf_apply {ι : Type} [Cost.SizedEncoding ι] (la lb oLa oLb : Cost.PolyTimeFun ι Cost.Unary) (g : Cost.PolyTimeFun ι Bool) (s : Cost.PolyTimeFun ι Cost.Unary) (a : ι) : (srcEqOf la lb oLa oLb g s).toFun a = guardCons (g.toFun a) (List.length (la.toFun a) + List.length (lb.toFun a)) ++ eqCons (List.length (la.toFun a)) (List.length (lb.toFun a)) (List.length (oLa.toFun a)) (List.length (oLb.toFun a)) (List.length (s.toFun a))

noncomputable def MIPRE.Tailored.Intro.add3 {ι : Type} [Cost.SizedEncoding ι] (u v w : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

The sum of three unary numbers.

Equations

• MIPRE.Tailored.Intro.add3 u v w = MIPRE.Tailored.Intro.catF u (MIPRE.Tailored.Intro.catF v w)

@[simp]

theorem MIPRE.Tailored.Intro.length_add3 {ι : Type} [Cost.SizedEncoding ι] (u v w : Cost.PolyTimeFun ι Cost.Unary) (a : ι) : List.length ((add3 u v w).toFun a) = List.length (u.toFun a) + (List.length (v.toFun a) + List.length (w.toFun a))

The register and the cutoff

noncomputable def MIPRE.Tailored.Intro.uQR {ι : Type} [Cost.SizedEncoding ι] (Q R : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

Q + R.

Equations

• MIPRE.Tailored.Intro.uQR Q R = MIPRE.Tailored.Intro.catF Q R

noncomputable def MIPRE.Tailored.Intro.uQ2R {ι : Type} [Cost.SizedEncoding ι] (Q R : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

Q + 2R.

Equations

• MIPRE.Tailored.Intro.uQ2R Q R = MIPRE.Tailored.Intro.add3 Q R R

noncomputable def MIPRE.Tailored.Intro.u2QR {ι : Type} [Cost.SizedEncoding ι] (Q R : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

2Q + R.

Equations

• MIPRE.Tailored.Intro.u2QR Q R = MIPRE.Tailored.Intro.add3 Q Q R

noncomputable def MIPRE.Tailored.Intro.u2Q2R {ι : Type} [Cost.SizedEncoding ι] (Q R : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

2Q + 2R.

Equations

• MIPRE.Tailored.Intro.u2Q2R Q R = MIPRE.Tailored.Intro.catF (MIPRE.Tailored.Intro.catF Q Q) (MIPRE.Tailored.Intro.catF R R)

noncomputable def MIPRE.Tailored.Intro.u2Q {ι : Type} [Cost.SizedEncoding ι] (Q : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

2Q.

Equations

• MIPRE.Tailored.Intro.u2Q Q = MIPRE.Tailored.Intro.catF Q Q

noncomputable def MIPRE.Tailored.Intro.u3Q {ι : Type} [Cost.SizedEncoding ι] (Q : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

3Q.

Equations

• MIPRE.Tailored.Intro.u3Q Q = MIPRE.Tailored.Intro.add3 Q Q Q

@[simp]

theorem MIPRE.Tailored.Intro.length_uQR {ι : Type} [Cost.SizedEncoding ι] (Q R : Cost.PolyTimeFun ι Cost.Unary) (a : ι) : List.length ((uQR Q R).toFun a) = List.length (Q.toFun a) + List.length (R.toFun a)

@[simp]

theorem MIPRE.Tailored.Intro.length_uQ2R {ι : Type} [Cost.SizedEncoding ι] (Q R : Cost.PolyTimeFun ι Cost.Unary) (a : ι) : List.length ((uQ2R Q R).toFun a) = List.length (Q.toFun a) + 2 * List.length (R.toFun a)

@[simp]

theorem MIPRE.Tailored.Intro.length_u2QR {ι : Type} [Cost.SizedEncoding ι] (Q R : Cost.PolyTimeFun ι Cost.Unary) (a : ι) : List.length ((u2QR Q R).toFun a) = 2 * List.length (Q.toFun a) + List.length (R.toFun a)

@[simp]

theorem MIPRE.Tailored.Intro.length_u2Q2R {ι : Type} [Cost.SizedEncoding ι] (Q R : Cost.PolyTimeFun ι Cost.Unary) (a : ι) : List.length ((u2Q2R Q R).toFun a) = 2 * List.length (Q.toFun a) + 2 * List.length (R.toFun a)

@[simp]

theorem MIPRE.Tailored.Intro.length_u2Q {ι : Type} [Cost.SizedEncoding ι] (Q : Cost.PolyTimeFun ι Cost.Unary) (a : ι) : List.length ((u2Q Q).toFun a) = 2 * List.length (Q.toFun a)

@[simp]

theorem MIPRE.Tailored.Intro.length_u3Q {ι : Type} [Cost.SizedEncoding ι] (Q : Cost.PolyTimeFun ι Cost.Unary) (a : ι) : List.length ((u3Q Q).toFun a) = 3 * List.length (Q.toFun a)

noncomputable def MIPRE.Tailored.Intro.inQ {β : Type} [Cost.SizedEncoding β] : Cost.PolyTimeFun ((Cost.Unary × Cost.Unary) × β) Cost.Unary

The register length and the cutoff of an input ((Q, R), _).

Equations

• MIPRE.Tailored.Intro.inQ = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.Tailored.Intro.inR {β : Type} [Cost.SizedEncoding β] : Cost.PolyTimeFun ((Cost.Unary × Cost.Unary) × β) Cost.Unary

Equations

• MIPRE.Tailored.Intro.inR = MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.fst

@[simp]

theorem MIPRE.Tailored.Intro.inQ_apply {β : Type} [Cost.SizedEncoding β] (p : (Cost.Unary × Cost.Unary) × β) : inQ.toFun p = p.1.1

@[simp]

theorem MIPRE.Tailored.Intro.inR_apply {β : Type} [Cost.SizedEncoding β] (p : (Cost.Unary × Cost.Unary) × β) : inR.toFun p = p.1.2

Sampling and reading

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.PairIn : Type

The input of the sampling and reading comparisons: ((Q, R), (guard, source guard), sL).

Equations

• MIPRE.Tailored.Intro.PairIn = ((MIPRE.Cost.Unary × MIPRE.Cost.Unary) × (Bool × Bool) × MIPRE.Cost.Unary)

noncomputable def MIPRE.Tailored.Intro.sampleConsF : Cost.PolyTimeFun PairIn (List Cost.BitStr)

The sampling comparison sampleCons.

Equations

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

@[simp]

theorem MIPRE.Tailored.Intro.sampleConsF_apply (Q R : Cost.Unary) (g₁ g₂ : Bool) (s : Cost.Unary) : sampleConsF.toFun ((Q, R), (g₁, g₂), s) = guardCons g₁ (List.length Q + 2 * List.length R + (List.length Q + 2 * List.length R)) ++ (guardCons g₂ (List.length Q + 2 * List.length R + (List.length Q + 2 * List.length R)) ++ eqCons (List.length Q + 2 * List.length R) (List.length Q + 2 * List.length R) (List.length Q + List.length R) (List.length Q + List.length R) (List.length s))

theorem MIPRE.Tailored.Intro.sampleConsF_spec (Q R : ℕ) (sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (L : Bool → CL.CLFun CL.𝔽₂ (Fin Q) 7) (w : Bool) (aR bR : Cost.BitStr) : sampleConsF.toFun ((Cost.unary Q, Cost.unary R), (decide (CL.ofBits Q (win aR 0 Q) = (L w).eval (CL.ofBits Q (win bR 0 Q))), decide (sR (Introspection.AuxType.introspect, w) (win aR 0 Q) = sR (Introspection.AuxType.sample, w) (win bR 0 Q) ∧ sL (Introspection.AuxType.introspect, w) (win aR 0 Q) = sL (Introspection.AuxType.sample, w) (win bR 0 Q) ∧ win aR Q (sR (Introspection.AuxType.introspect, w) (win aR 0 Q)) = win bR Q (sR (Introspection.AuxType.sample, w) (win bR 0 Q)))), Cost.unary (sL (Introspection.AuxType.introspect, w) (win aR 0 Q))) = sampleCons Q R sR sL L w aR bR

The sampling comparison, on the encoded data.

noncomputable def MIPRE.Tailored.Intro.readConsF : Cost.PolyTimeFun PairIn (List Cost.BitStr)

The reading comparison readCons.

Equations

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

@[simp]

theorem MIPRE.Tailored.Intro.readConsF_apply (Q R : Cost.Unary) (g₁ g₂ : Bool) (s : Cost.Unary) : readConsF.toFun ((Q, R), (g₁, g₂), s) = guardCons g₁ (List.length Q + 2 * List.length R + (2 * List.length Q + 2 * List.length R)) ++ (guardCons g₂ (List.length Q + 2 * List.length R + (2 * List.length Q + 2 * List.length R)) ++ eqCons (List.length Q + 2 * List.length R) (2 * List.length Q + 2 * List.length R) (List.length Q + List.length R) (2 * List.length Q + List.length R) (List.length s))

theorem MIPRE.Tailored.Intro.readConsF_spec (Q R : ℕ) (sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (w : Bool) (aR bR : Cost.BitStr) : readConsF.toFun ((Cost.unary Q, Cost.unary R), (decide (win aR 0 Q = win bR 0 Q), decide (sR (Introspection.AuxType.introspect, w) (win aR 0 Q) = sR (Introspection.AuxType.read, w) (win bR 0 Q) ∧ sL (Introspection.AuxType.introspect, w) (win aR 0 Q) = sL (Introspection.AuxType.read, w) (win bR 0 Q) ∧ win aR Q (sR (Introspection.AuxType.introspect, w) (win aR 0 Q)) = win bR Q (sR (Introspection.AuxType.read, w) (win bR 0 Q)))), Cost.unary (sL (Introspection.AuxType.introspect, w) (win aR 0 Q))) = readCons Q R sR sL w aR bR

The reading comparison, on the encoded data.

Hiding

noncomputable def MIPRE.Tailored.Intro.hideReadConsF : Cost.PolyTimeFun ((Cost.Unary × Cost.Unary) × Bool) (List Cost.BitStr)

The comparison of the last Hide with Read hideReadCons, on ((Q, R), guard).

Equations

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

@[simp]

theorem MIPRE.Tailored.Intro.hideReadConsF_apply (Q R : Cost.Unary) (g : Bool) : hideReadConsF.toFun ((Q, R), g) = guardCons g (3 * List.length Q + (2 * List.length Q + 2 * List.length R)) ++ eqCons (3 * List.length Q) (2 * List.length Q + 2 * List.length R) (List.length Q) (List.length Q + List.length R) (List.length Q)

theorem MIPRE.Tailored.Intro.hideReadConsF_spec (Q R : ℕ) (L : Bool → CL.CLFun CL.𝔽₂ (Fin Q) 7) (w : Bool) (aR bR : Cost.BitStr) : hideReadConsF.toFun ((Cost.unary Q, Cost.unary R), decide ((L w).outputPrefix 6 (CL.ofBits Q (win aR 0 Q)) = (L w).outputPrefix 6 (CL.ofBits Q (win bR 0 Q)))) = hideReadCons Q R L w aR bR

The comparison of the last Hide with Read, on the encoded data.

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.HideIn : Type

The input of the comparison of consecutive Hide levels: Q, the guard, the masks of the prefix register of the next level, of that of the level after it (complemented by the program) and of the factor of the dual, and the bits of the kernel generators.

Equations

• MIPRE.Tailored.Intro.HideIn = (MIPRE.Cost.Unary × Bool × (MIPRE.Cost.BitStr × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr) × List MIPRE.Cost.BitStr)

noncomputable def MIPRE.Tailored.Intro.notMaskF : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

The complement of a mask.

Equations

• MIPRE.Tailored.Intro.notMaskF = ((MIPRE.Cost.PolyTimeFun.id Bool).ite (MIPRE.Cost.PolyTimeFun.const false) (MIPRE.Cost.PolyTimeFun.const true)).map

@[simp]

theorem MIPRE.Tailored.Intro.notMaskF_apply (m : Cost.BitStr) : notMaskF.toFun m = List.map not m

theorem MIPRE.Tailored.Intro.maskOf_compl {s : ℕ} (S : Finset (Fin s)) : maskOf Sᶜ = List.map not (maskOf S)

noncomputable def MIPRE.Tailored.Intro.hideNextConsF : Cost.PolyTimeFun HideIn (List Cost.BitStr)

The comparison of consecutive Hide levels hideNextCons.

Equations

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

theorem MIPRE.Tailored.Intro.hideNextConsF_spec (Q : ℕ) (L : Bool → CL.CLFun CL.𝔽₂ (Fin Q) 7) (kg : (S : Finset (Fin Q)) → CL.RegLinear CL.𝔽₂ S → List (Fin Q → CL.𝔽₂)) (w : Bool) (k : ℕ) (aR bR : Cost.BitStr) : hideNextConsF.toFun (Cost.unary Q, decide ((L w).outputPrefix k (CL.ofBits Q (win aR 0 Q)) = (L w).outputPrefix k (CL.ofBits Q (win bR 0 Q))), (maskOf (Introspection.CLChecks.prefixRegister (L w) (k + 1) (CL.ofBits Q (win bR 0 Q))), maskOf (Introspection.CLChecks.prefixRegister (L w) (k + 2) (CL.ofBits Q (win bR 0 Q))), maskOf ((L w).factorOfPrefix (k + 1) (CL.ofBits Q (win bR 0 Q)))), List.map CL.toBits (kg ((L w).factorOfPrefix (k + 1) (CL.ofBits Q (win bR 0 Q))) (Introspection.CLChecks.stageLinear (L w) (k + 1) (CL.ofBits Q (win bR 0 Q))))) = hideNextCons Q L kg w k aR bR

The comparison of consecutive Hide levels, on the encoded data.

Consistency at one label

def MIPRE.Tailored.Intro.isHideT : Introspection.AuxType 7 → Bool

Whether a label is a Hide label.

Equations

• MIPRE.Tailored.Intro.isHideT (MIPRE.Introspection.AuxType.hide k) = true
• MIPRE.Tailored.Intro.isHideT x✝ = false

def MIPRE.Tailored.Intro.isReadT : Introspection.AuxType 7 → Bool

Whether a label is the Read label.

Equations

• MIPRE.Tailored.Intro.isReadT MIPRE.Introspection.AuxType.read = true
• MIPRE.Tailored.Intro.isReadT x✝ = false

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.SameIn : Type

The input of the consistency comparison: ((Q, R), (hide?, read?), (guard, source guard), sL).

Equations

• MIPRE.Tailored.Intro.SameIn = ((MIPRE.Cost.Unary × MIPRE.Cost.Unary) × (Bool × Bool) × (Bool × Bool) × MIPRE.Cost.Unary)

noncomputable def MIPRE.Tailored.Intro.sG : Cost.PolyTimeFun SameIn Bool

The guard, the source guard and the split of the consistency comparison.

Equations

• MIPRE.Tailored.Intro.sG = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.Tailored.Intro.sG₂ : Cost.PolyTimeFun SameIn Bool

Equations

• MIPRE.Tailored.Intro.sG₂ = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.Tailored.Intro.sS : Cost.PolyTimeFun SameIn Cost.Unary

Equations

• MIPRE.Tailored.Intro.sS = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.Tailored.Intro.sameConsF : Cost.PolyTimeFun SameIn (List Cost.BitStr)

Consistency at one label sameCons, the kind of the label given by two Booleans.

Equations

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

theorem MIPRE.Tailored.Intro.sameConsF_spec (Q R : ℕ) (sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (t : Introspection.AuxType 7 × Bool) (aR bR : Cost.BitStr) : sameConsF.toFun ((Cost.unary Q, Cost.unary R), (isHideT t.1, isReadT t.1), (decide (win aR 0 Q = win bR 0 Q), decide (sR t (win aR 0 Q) = sR t (win bR 0 Q) ∧ sL t (win aR 0 Q) = sL t (win bR 0 Q) ∧ win aR Q (sR t (win aR 0 Q)) = win bR Q (sR t (win bR 0 Q)))), Cost.unary (sL t (win aR 0 Q))) = sameCons Q R sR sL t aR bR

Consistency at one label, on the encoded data.

The source game

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.SourceIn : Type

The input of the source comparison: ((Q, R), ((sRa, sLa), (sRb, sLb)), constraints).

Equations

• MIPRE.Tailored.Intro.SourceIn = ((MIPRE.Cost.Unary × MIPRE.Cost.Unary) × ((MIPRE.Cost.Unary × MIPRE.Cost.Unary) × MIPRE.Cost.Unary × MIPRE.Cost.Unary) × List MIPRE.Cost.BitStr)

noncomputable def MIPRE.Tailored.Intro.sourceConsF : Cost.PolyTimeFun SourceIn (List Cost.BitStr)

The source game's constraints sourceCons: the input's constraints, re-indexed.

Equations

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

@[simp]

theorem MIPRE.Tailored.Intro.sourceConsF_apply (Q R sRa sLa sRb sLb : Cost.Unary) (cs : List Cost.BitStr) : sourceConsF.toFun ((Q, R), ((sRa, sLa), sRb, sLb), cs) = List.map (reindex (List.length Q) (List.length R) (List.length sRa) (List.length sLa) (List.length sRb) (List.length sLb) (List.length Q + 2 * List.length R) (List.length Q + 2 * List.length R)) cs

theorem MIPRE.Tailored.Intro.sourceConsF_spec (Q R : ℕ) (sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (srcCons : Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → List Cost.BitStr) (aR bR : Cost.BitStr) : sourceConsF.toFun ((Cost.unary Q, Cost.unary R), ((Cost.unary (sR (Introspection.AuxType.introspect, false) (win aR 0 Q)), Cost.unary (sL (Introspection.AuxType.introspect, false) (win aR 0 Q))), Cost.unary (sR (Introspection.AuxType.introspect, true) (win bR 0 Q)), Cost.unary (sL (Introspection.AuxType.introspect, true) (win bR 0 Q))), srcCons (win aR 0 Q) (win bR 0 Q) (win aR Q (sR (Introspection.AuxType.introspect, false) (win aR 0 Q))) (win bR Q (sR (Introspection.AuxType.introspect, true) (win bR 0 Q)))) = sourceCons Q R sR sL srcCons aR bR

The source game's constraints, on the encoded data: the last input is the input's constraint list at the two registers and readable input answers.

The length of a label's answers

noncomputable def MIPRE.Tailored.Intro.auxLenF : Cost.PolyTimeFun ((Cost.Unary × Cost.Unary) × Bool × Bool) Cost.Unary

The length of a label's answers auxLen, on ((Q, R), (hide?, read?)).

Equations

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

theorem MIPRE.Tailored.Intro.auxLenF_spec (Q R : ℕ) (t : Introspection.AuxType 7) : auxLenF.toFun ((Cost.unary Q, Cost.unary R), isHideT t, isReadT t) = Cost.unary (auxLen Q R t)

A pair of auxiliary answers

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.PairAsmIn : Type

The input of the assembly at a pair of labels: ((guard, labels equal?), (la, lb), (same, directed, reverse directed)), the three lists already computed.

Equations

• MIPRE.Tailored.Intro.PairAsmIn = ((Bool × Bool) × (MIPRE.Cost.Unary × MIPRE.Cost.Unary) × List MIPRE.Cost.BitStr × List MIPRE.Cost.BitStr × List MIPRE.Cost.BitStr)

noncomputable def MIPRE.Tailored.Intro.auxPairF : Cost.PolyTimeFun PairAsmIn (List Cost.BitStr)

The constraints at a pair of auxiliary labels auxPair, from the consistency list and the two directed lists: when the guard holds, the consistency list when the labels agree, the directed list, and the reverse one swapped; otherwise the rejecting constraint.

Equations

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

@[simp]

theorem MIPRE.Tailored.Intro.auxPairF_apply (g e : Bool) (la lb : Cost.Unary) (same dir rev : List Cost.BitStr) : auxPairF.toFun ((g, e), (la, lb), same, dir, rev) = if g = true then (if e = true then same else []) ++ (dir ++ List.map (swapCon (List.length la) (List.length lb)) rev) else [rejectConstraint (List.length la + List.length lb)]

theorem MIPRE.Tailored.Intro.auxPairF_spec (Q R : ℕ) (sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (L : Bool → CL.CLFun CL.𝔽₂ (Fin Q) 7) (G : Introspection.AuxType 7 × Bool → Cost.BitStr → Prop) (kg : (S : Finset (Fin Q)) → CL.RegLinear CL.𝔽₂ S → List (Fin Q → CL.𝔽₂)) (srcCons : Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → List Cost.BitStr) (t u : Introspection.AuxType 7 × Bool) (aR bR : Cost.BitStr) : auxPairF.toFun ((decide (G t (win aR 0 Q) ∧ G u (win bR 0 Q)), decide (t = u)), (Cost.unary (auxLen Q R t.1), Cost.unary (auxLen Q R u.1)), sameCons Q R sR sL t aR bR, dirAux Q R sR sL L kg srcCons t u aR bR, dirAux Q R sR sL L kg srcCons u t bR aR) = auxPair Q R sR sL L G kg srcCons t u aR bR

The constraints at a pair of auxiliary labels, on the encoded data.