The first hiding edge's constraints as polynomial-time programs

PauliHide.pauliHideCons and pauliHideConsRev are lists of register forms ∑ wᵣ ((Π a)ᵣ + xᵣ) = 0, for w the masked generators proj S z and the unit vectors off S, with Π a the kernel's register of the Pauli answer and x a register of the Hide answer. This file computes them by programs (Cost.PolyTimeFun), from the kernel's parameter triple, the mask of S = P.factorOfPrefix 0 0 and the generators' bits; the mask and the generators are inputs, computed elsewhere from the sampler.

The coefficient of a Hide bit is a coordinate of w. The coefficient of the Pauli bit i of block bb is ∑_s C i s · w (bb, s), with C i s the s-th self-dual coordinate of the i-th canonical (Shoup) basis element bsh i (dot_pauliXProj_unitV): Π expands each field element of the answer in the self-dual basis. So with the rows C i · computed once (ctxProg, by the kernel's basis conversion BasisProgram.toSelfDualRowsProg on the identity rows), the Pauli coefficients are those rows applied to each block of w (coefProg, coefProg_eq).

• toCon_hideCon, toCon_hideCon_seg: the constraint vector of a register form, position by position, and by segments of Q bits when the two registers sit at multiples of Q;
• hideChecks_toCon: hideChecks as such register forms;
• pauliHideProg_eq, pauliHideRevProg_eq: the programs compute the constraint lists, exactly, for every P and every list of generators.

Unit vectors

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.PauliHideProg.unitV {N : ℕ} (l : Fin N) : Fin N → ZMod 2

The unit vector at l, in the form LinCheck.toCon evaluates.

Equations

• MIPRE.Tailored.Intro.PauliHideProg.unitV l i = if l = i then 1 else 0

theorem MIPRE.Tailored.Intro.PauliHideProg.getv_unitV {N : ℕ} (l : Fin N) (p : ℕ) : (getv N p) (unitV l) = if p = ↑l then 1 else 0

theorem MIPRE.Tailored.Intro.PauliHideProg.block_iff {k i₀ bb bb₀ : ℕ} (hi : i₀ < k) : bb * k ≤ i₀ + k * bb₀ ∧ i₀ + k * bb₀ < bb * k + k ↔ bb = bb₀

The block reading of i·k bits: bb·k ≤ i₀ + k·bb₀ < bb·k + k exactly when bb = bb₀.

theorem MIPRE.Tailored.Intro.PauliHideProg.dot_regAt_unitV {N s : ℕ} (o : ℕ) (w : Fin s → ZMod 2) (l : Fin N) : ∑ r : Fin s, w r * (PauliHide.regAt N o s) (unitV l) r = if h : o ≤ ↑l ∧ ↑l < o + s then w ⟨↑l - o, ⋯⟩ else 0

The register coefficients of a register form.

theorem MIPRE.Tailored.Intro.PauliHideProg.seg_dite {Q : ℕ} (p σ a : ℕ) (t : Fin Q) (f : Fin Q → ZMod 2) (hp : p = ↑t + Q * σ) : (if h : a * Q ≤ p ∧ p < a * Q + Q then f ⟨p - a * Q, ⋯⟩ else 0) = if σ = a then f t else 0

A window at a·Q read at the position t + Q·σ of the σ-th segment.

noncomputable def MIPRE.Tailored.Intro.PauliHideProg.bsh (k : ℕ) (hk : 1 ≤ k) (i : Fin k) : (SAT.shoupBinField k hk).carrier

The i-th element of the canonical (Shoup polynomial) basis.

Equations

• MIPRE.Tailored.Intro.PauliHideProg.bsh k hk i = (MIPRE.SAT.shoupCoordinateEquiv k hk).symm (Pi.single i 1)

theorem MIPRE.Tailored.Intro.PauliHideProg.fldAt_unitV (k : ℕ) (hk : 1 ≤ k) {N : ℕ} (o : ℕ) (l : Fin N) : (fldAt k hk N o) (unitV l) = if h : o ≤ ↑l ∧ ↑l < o + k then bsh k hk ⟨↑l - o, ⋯⟩ else 0

noncomputable def MIPRE.Tailored.Intro.PauliHideProg.cm (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (i s : Fin k) : ZMod 2

The self-dual coordinates of the canonical basis: C i s.

Equations

• MIPRE.Tailored.Intro.PauliHideProg.cm k hk hodd i s = (MIPRE.SAT.shoupSelfDualNormalBasis k hk hodd).equivFun (MIPRE.Tailored.Intro.PauliHideProg.bsh k hk i) s

noncomputable def MIPRE.Tailored.Intro.PauliHideProg.coef (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (w : Fin (2 ^ 2 ^ j * k) → ZMod 2) : Fin (2 ^ 2 ^ j * k) → ZMod 2

The coefficients of the Pauli bits in ∑ wᵣ (Π a)ᵣ: at block bb, bit i, ∑_s C i s · w (bb, s).

Equations

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

theorem MIPRE.Tailored.Intro.PauliHideProg.dot_pauliXProj_unitV (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) {N : ℕ} (o : ℕ) (w : Fin (2 ^ 2 ^ j * k) → ZMod 2) (l : Fin N) : ∑ r : Fin (2 ^ 2 ^ j * k), w r * (PauliHide.pauliXProj k hk hodd j N o) (unitV l) r = if h : o ≤ ↑l ∧ ↑l < o + 2 ^ 2 ^ j * k then coef k hk hodd j w ⟨↑l - o, ⋯⟩ else 0

The Pauli coefficients of a register form.

noncomputable def MIPRE.Tailored.Intro.PauliHideProg.hideCon (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j N oP oR : ℕ) (w : Fin (2 ^ 2 ^ j * k) → ZMod 2) : LinCheck N

The register form ∑ wᵣ ((Π a)ᵣ + xᵣ), the Pauli register at oP, the other at oR.

Equations

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

theorem MIPRE.Tailored.Intro.PauliHideProg.toCon_hideCon (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j N oP oR : ℕ) (w : Fin (2 ^ 2 ^ j * k) → ZMod 2) : (hideCon k hk hodd j N oP oR w).toCon = (List.ofFn fun (l : Fin N) => LowDegree.BinaryLinear.bit ((if h : oP ≤ ↑l ∧ ↑l < oP + 2 ^ 2 ^ j * k then coef k hk hodd j w ⟨↑l - oP, ⋯⟩ else 0) + if h : oR ≤ ↑l ∧ ↑l < oR + 2 ^ 2 ^ j * k then w ⟨↑l - oR, ⋯⟩ else 0)) ++ [false]

The constraint vector of a register form, position by position.

theorem MIPRE.Tailored.Intro.PauliHideProg.toCon_hideCon_seg (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j a b : ℕ) (hab : a ≠ b) (w : Fin (2 ^ 2 ^ j * k) → ZMod 2) : (hideCon k hk hodd j (4 * (2 ^ 2 ^ j * k)) (a * (2 ^ 2 ^ j * k)) (b * (2 ^ 2 ^ j * k)) w).toCon = (List.ofFn fun (σ : Fin 4) => if ↑σ = a then CL.toBits (coef k hk hodd j w) else if ↑σ = b then CL.toBits w else List.replicate (2 ^ 2 ^ j * k) false).flatten ++ [false]

The constraint vector of a register form, by segments of Q bits: the Pauli register in segment a, the other in segment b.

The constraints of hideChecks as register forms

theorem MIPRE.Tailored.Intro.PauliHideProg.proj_eq_dotForm {s : ℕ} (i : Fin s) : LinearMap.proj i = PauliHide.dotForm (Pi.single i 1)

theorem MIPRE.Tailored.Intro.PauliHideProg.flatten_map_ite {α : Type u_1} {β : Type u_2} (l : List α) (p : α → Bool) (g : α → β) : (List.map (fun (x : α) => if p x = true then [] else [g x]) l).flatten = List.map g (List.filter (fun (x : α) => !p x) l)

theorem MIPRE.Tailored.Intro.PauliHideProg.hideChecks_toCon (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) {ℓ : ℕ} (P : CL.CLFun CL.𝔽₂ (Fin (2 ^ 2 ^ j * k)) ℓ) (gens : List (Fin (2 ^ 2 ^ j * k) → CL.𝔽₂)) (oP oH a b c : ℕ) (hoP : oP = a * (2 ^ 2 ^ j * k)) (hb' : oH + 2 ^ 2 ^ j * k = b * (2 ^ 2 ^ j * k)) (hc' : oH + 2 * (2 ^ 2 ^ j * k) = c * (2 ^ 2 ^ j * k)) : List.map LinCheck.toCon (PauliHide.hideChecks k hk hodd j (4 * (2 ^ 2 ^ j * k)) oP oH P gens) = List.map (fun (z : Fin (2 ^ 2 ^ j * k) → ZMod 2) => (hideCon k hk hodd j (4 * (2 ^ 2 ^ j * k)) (a * (2 ^ 2 ^ j * k)) (b * (2 ^ 2 ^ j * k)) ((CL.proj (P.factorOfPrefix 0 0)) z)).toCon) gens ++ List.map (fun (i : Fin (2 ^ 2 ^ j * k)) => (hideCon k hk hodd j (4 * (2 ^ 2 ^ j * k)) (a * (2 ^ 2 ^ j * k)) (c * (2 ^ 2 ^ j * k)) (Pi.single i 1)).toCon) (List.filter (fun (i : Fin (2 ^ 2 ^ j * k)) => decide (i ∉ P.factorOfPrefix 0 0)) (List.finRange (2 ^ 2 ^ j * k)))

hideChecks by segments: the register forms of hideChecks at offsets that are multiples of Q.

The programs

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.PauliHideProg.Ctx : Type

The data the coefficient programs share: the self-dual coordinate rows of the canonical basis, k and 2^j in unary.

Equations

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

noncomputable def MIPRE.Tailored.Intro.PauliHideProg.ctxProg : Cost.PolyTimeFun Introspection.PauliSamplerParameters.Parameters Ctx

The shared data, from the kernel's parameter triple.

Equations

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

noncomputable def MIPRE.Tailored.Intro.PauliHideProg.coefProg : Cost.PolyTimeFun (Cost.BitStr × Ctx) Cost.BitStr

The coefficients of the Pauli bits of a register form w: block by block, the coordinate rows applied to the block of w.

Equations

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

noncomputable def MIPRE.Tailored.Intro.PauliHideProg.zerosProg : Cost.PolyTimeFun (Cost.BitStr × Ctx) Cost.BitStr

Q zeros, Q the length of the register form.

Equations

• MIPRE.Tailored.Intro.PauliHideProg.zerosProg = MIPRE.Cost.PolyTimeFun.replicate.comp ((MIPRE.Cost.PolyTimeFun.length.comp MIPRE.Cost.PolyTimeFun.fst).pair (MIPRE.Cost.PolyTimeFun.const false))

noncomputable def MIPRE.Tailored.Intro.PauliHideProg.segProg (a b : ℕ) : Cost.PolyTimeFun (Cost.BitStr × Ctx) Cost.BitStr

The constraint of a register form: four segments of Q bits, the Pauli coefficients in segment a, the form in segment b, zeros elsewhere, then J's coefficient 0.

Equations

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

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.PauliHideProg.HideInput : Type

The input of the hiding programs: parameters, the mask of S, the generators.

Equations

• MIPRE.Tailored.Intro.PauliHideProg.HideInput = (MIPRE.Introspection.PauliSamplerParameters.Parameters × MIPRE.Cost.BitStr × List MIPRE.Cost.BitStr)

noncomputable def MIPRE.Tailored.Intro.PauliHideProg.genFamily (a b : ℕ) : Cost.PolyTimeFun HideInput (List Cost.BitStr)

The constraints of the generators.

Equations

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

noncomputable def MIPRE.Tailored.Intro.PauliHideProg.offFamily (a c : ℕ) : Cost.PolyTimeFun HideInput (List Cost.BitStr)

The constraints of the coordinates off the mask.

Equations

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

noncomputable def MIPRE.Tailored.Intro.PauliHideProg.pauliHideProg : Cost.PolyTimeFun HideInput (List Cost.BitStr)

The first hiding edge's constraints, Pauli answer first, as a program.

Equations

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

noncomputable def MIPRE.Tailored.Intro.PauliHideProg.pauliHideRevProg : Cost.PolyTimeFun HideInput (List Cost.BitStr)

The first hiding edge's constraints, Hide answer first, as a program.

Equations

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

Correctness of the programs

theorem MIPRE.Tailored.Intro.PauliHideProg.toBits_eq_vectorBits (k : ℕ) (hk : 1 ≤ k) (x : (SAT.shoupBinField k hk).carrier) : (SAT.shoupBinField k hk).toBits x = LowDegree.BinaryLinear.vectorBits ((SAT.shoupCoordinateEquiv k hk) x)

The canonical bits of a field element are its coordinate vector.

theorem MIPRE.Tailored.Intro.PauliHideProg.identityBits_eq (k : ℕ) (hk : 1 ≤ k) : LowDegree.BinaryLinear.identityBits k = (SAT.shoupBinField k hk).vecBits (bsh k hk)

noncomputable def MIPRE.Tailored.Intro.PauliHideProg.cRows (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) : List Cost.BitStr

The coordinate rows: row i is C i ·.

Equations

• MIPRE.Tailored.Intro.PauliHideProg.cRows k hk hodd = List.ofFn fun (i : Fin k) => MIPRE.CL.toBits fun (s : Fin k) => MIPRE.Tailored.Intro.PauliHideProg.cm k hk hodd i s

theorem MIPRE.Tailored.Intro.PauliHideProg.ctxProg_eq (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) : ctxProg.toFun (Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)) = (cRows k hk hodd, Cost.unary k, Cost.unary (2 ^ j))

theorem MIPRE.Tailored.Intro.PauliHideProg.toBits_blocks (k j : ℕ) (w : Fin (2 ^ 2 ^ j * k) → ZMod 2) : CL.toBits w = (List.ofFn fun (bb : Fin (2 ^ 2 ^ j)) => CL.toBits fun (s : Fin k) => w (finProdFinEquiv (bb, s))).flatten

theorem MIPRE.Tailored.Intro.PauliHideProg.coefProg_eq (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (w : Fin (2 ^ 2 ^ j * k) → ZMod 2) : coefProg.toFun (CL.toBits w, cRows k hk hodd, Cost.unary k, Cost.unary (2 ^ j)) = CL.toBits (coef k hk hodd j w)

theorem MIPRE.Tailored.Intro.PauliHideProg.segProg_eq (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j a b : ℕ) (w : Fin (2 ^ 2 ^ j * k) → ZMod 2) : (segProg a b).toFun (CL.toBits w, cRows k hk hodd, Cost.unary k, Cost.unary (2 ^ j)) = (List.ofFn fun (σ : Fin 4) => if ↑σ = a then CL.toBits (coef k hk hodd j w) else if ↑σ = b then CL.toBits w else List.replicate (2 ^ 2 ^ j * k) false).flatten ++ [false]

theorem MIPRE.Tailored.Intro.PauliHideProg.zip_indicator_identity (k j : ℕ) (S : Finset (Fin (2 ^ 2 ^ j * k))) : List.zip (CL.indicatorBits S) (LowDegree.BinaryLinear.identityBits (2 ^ 2 ^ j * k)) = List.map (fun (i : Fin (2 ^ 2 ^ j * k)) => (decide (i ∈ S), CL.toBits (Pi.single i 1))) (List.finRange (2 ^ 2 ^ j * k))

theorem MIPRE.Tailored.Intro.PauliHideProg.families_eq (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) {ℓ : ℕ} (P : CL.CLFun CL.𝔽₂ (Fin (2 ^ 2 ^ j * k)) ℓ) (gens : List (Fin (2 ^ 2 ^ j * k) → CL.𝔽₂)) (a b c : ℕ) (hab : a ≠ b) (hac : a ≠ c) : Cost.PolyTimeFun.append.toFun ((genFamily a b).toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), CL.indicatorBits (P.factorOfPrefix 0 0), List.map CL.toBits gens), (offFamily a c).toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), CL.indicatorBits (P.factorOfPrefix 0 0), List.map CL.toBits gens)) = List.map (fun (z : Fin (2 ^ 2 ^ j * k) → ZMod 2) => (hideCon k hk hodd j (4 * (2 ^ 2 ^ j * k)) (a * (2 ^ 2 ^ j * k)) (b * (2 ^ 2 ^ j * k)) ((CL.proj (P.factorOfPrefix 0 0)) z)).toCon) gens ++ List.map (fun (i : Fin (2 ^ 2 ^ j * k)) => (hideCon k hk hodd j (4 * (2 ^ 2 ^ j * k)) (a * (2 ^ 2 ^ j * k)) (c * (2 ^ 2 ^ j * k)) (Pi.single i 1)).toCon) (List.filter (fun (i : Fin (2 ^ 2 ^ j * k)) => decide (i ∉ P.factorOfPrefix 0 0)) (List.finRange (2 ^ 2 ^ j * k)))

theorem MIPRE.Tailored.Intro.PauliHideProg.pauliHideProg_eq (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) {ℓ : ℕ} (P : CL.CLFun CL.𝔽₂ (Fin (2 ^ 2 ^ j * k)) ℓ) (gens : List (Fin (2 ^ 2 ^ j * k) → CL.𝔽₂)) : pauliHideProg.toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), CL.indicatorBits (P.factorOfPrefix 0 0), List.map CL.toBits gens) = PauliHide.pauliHideCons k hk hodd j P gens

pauliHideProg computes pauliHideCons, from the kernel's parameter triple, the mask of the first factor S = P.factorOfPrefix 0 0 and the generators' bits.

theorem MIPRE.Tailored.Intro.PauliHideProg.pauliHideRevProg_eq (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) {ℓ : ℕ} (P : CL.CLFun CL.𝔽₂ (Fin (2 ^ 2 ^ j * k)) ℓ) (gens : List (Fin (2 ^ 2 ^ j * k) → CL.𝔽₂)) : pauliHideRevProg.toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), CL.indicatorBits (P.factorOfPrefix 0 0), List.map CL.toBits gens) = PauliHide.pauliHideConsRev k hk hodd j P gens

pauliHideRevProg computes pauliHideConsRev.