Uniform executable line representatives

The program selects the first nonzero direction coordinate, divides the point coordinate by it, and subtracts that multiple of the direction. Selection, inversion, multiplication and the coordinate scan are actual ambient programs. The raw program is polynomial-time and total on every input; correctness is stated on canonical encodings in the constructed Shoup field.

def MIPRE.Introspection.LineProgram.firstPair {F : Type u_1} [Zero F] [DecidableEq F] (l : List (F × F)) : F × F

Equations

• MIPRE.Introspection.LineProgram.firstPair l = List.foldr (fun (a s : F × F) => if a.2 ≠ 0 then a else s) (0, 0) l

theorem MIPRE.Introspection.LineProgram.firstPair_getD {F : Type u_1} [Zero F] [DecidableEq F] (l : List (F × F)) (j : ℕ) (hj : (l.getD j (0, 0)).2 ≠ 0) (hprev : ∀ i < j, (l.getD i (0, 0)).2 = 0) : firstPair l = l.getD j (0, 0)

theorem MIPRE.Introspection.LineProgram.firstPair_ofFn {F : Type u_1} [Zero F] [DecidableEq F] {n : ℕ} (u v : Fin n → F) (hv : ∃ (j : Fin n), v j ≠ 0) : firstPair (List.ofFn fun (i : Fin n) => (u i, v i)) = (u (Fin.find (fun (j : Fin n) => v j ≠ 0) hv), v (Fin.find (fun (j : Fin n) => v j ≠ 0) hv))

def MIPRE.Introspection.LineProgram.coefficient {F : Type u_1} [Field F] [DecidableEq F] (l : List (F × F)) : F

Equations

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

def MIPRE.Introspection.LineProgram.representative {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} (u v : Fin n → F) : Fin n → F

Equations

• MIPRE.Introspection.LineProgram.representative u v = u - MIPRE.Introspection.LineProgram.coefficient (List.ofFn fun (i : Fin n) => (u i, v i)) • v

theorem MIPRE.Introspection.LineProgram.representative_nonzero {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} (u v : Fin n → F) (hv : ∃ (j : Fin n), v j ≠ 0) : representative u v = u - (u (Fin.find (fun (j : Fin n) => v j ≠ 0) hv) / v (Fin.find (fun (j : Fin n) => v j ≠ 0) hv)) • v

noncomputable def MIPRE.Introspection.LineProgram.selectPairStep : Cost.PolyTimeFun ((Cost.BitStr × Cost.BitStr) × Cost.BitStr × Cost.BitStr) (Cost.BitStr × Cost.BitStr)

Equations

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

noncomputable def MIPRE.Introspection.LineProgram.firstPairBitsProg : Cost.PolyTimeFun (List (Cost.BitStr × Cost.BitStr) × Cost.BitStr × Cost.BitStr) (Cost.BitStr × Cost.BitStr)

Equations

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

theorem MIPRE.Introspection.LineProgram.firstPairBitsProg_correct (k : ℕ) (hk : 1 ≤ k) (l : List ((SAT.shoupBinField k hk).carrier × (SAT.shoupBinField k hk).carrier)) : firstPairBitsProg.toFun (List.map (fun (p : (SAT.shoupBinField k hk).carrier × (SAT.shoupBinField k hk).carrier) => ((SAT.shoupBinField k hk).toBits p.1, (SAT.shoupBinField k hk).toBits p.2)) l, (SAT.shoupBinField k hk).toBits 0, (SAT.shoupBinField k hk).toBits 0) = ((SAT.shoupBinField k hk).toBits (firstPair l).1, (SAT.shoupBinField k hk).toBits (firstPair l).2)

noncomputable def MIPRE.Introspection.LineProgram.coefficientOfPairProg : Cost.PolyTimeFun (Cost.Unary × Cost.BitStr × Cost.BitStr) Cost.BitStr

Equations

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

theorem MIPRE.Introspection.LineProgram.coefficientOfPairProg_correct (k : ℕ) (hk : 1 ≤ k) (a c : (SAT.shoupBinField k hk).carrier) : coefficientOfPairProg.toFun (Cost.unary k, (SAT.shoupBinField k hk).toBits a, (SAT.shoupBinField k hk).toBits c) = (SAT.shoupBinField k hk).toBits (if c ≠ 0 then a * c⁻¹ else 0)

noncomputable def MIPRE.Introspection.LineProgram.coefficientBitsProg : Cost.PolyTimeFun (Cost.Unary × List (Cost.BitStr × Cost.BitStr)) Cost.BitStr

Select a pivot and compute its point/direction ratio; the all-zero direction has coefficient zero.

Equations

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

theorem MIPRE.Introspection.LineProgram.coefficientBitsProg_correct (k : ℕ) (hk : 1 ≤ k) (l : List ((SAT.shoupBinField k hk).carrier × (SAT.shoupBinField k hk).carrier)) : coefficientBitsProg.toFun (Cost.unary k, List.map (fun (p : (SAT.shoupBinField k hk).carrier × (SAT.shoupBinField k hk).carrier) => ((SAT.shoupBinField k hk).toBits p.1, (SAT.shoupBinField k hk).toBits p.2)) l) = (SAT.shoupBinField k hk).toBits (coefficient l)

noncomputable def MIPRE.Introspection.LineProgram.subtractStepProg : Cost.PolyTimeFun ((Cost.BitStr × Cost.BitStr) × Cost.Unary × Cost.BitStr) Cost.BitStr

Equations

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

noncomputable def MIPRE.Introspection.LineProgram.lineRepresentativeProg : Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr × List Cost.BitStr) (List Cost.BitStr)

One uniform program for arbitrary field widths and vector lengths.

Equations

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

theorem MIPRE.Introspection.LineProgram.lineRepresentativeProg_correct (k : ℕ) (hk : 1 ≤ k) {n : ℕ} (u v : Fin n → (SAT.shoupBinField k hk).carrier) : lineRepresentativeProg.toFun (Cost.unary k, (SAT.shoupBinField k hk).vecBits u, (SAT.shoupBinField k hk).vecBits v) = (SAT.shoupBinField k hk).vecBits (representative u v)

theorem MIPRE.Introspection.LineProgram.lineRepresentativeProg_runs (x : Cost.Unary × List Cost.BitStr × List Cost.BitStr) : ∃ r ≤ Polynomial.eval (Cost.esize x) lineRepresentativeProg.timeBound, lineRepresentativeProg.code.Runs (Cost.encode x) (Cost.encode (lineRepresentativeProg.toFun x)) r

The ambient program halts within one polynomial for every raw input, including malformed field elements and unequal vector lengths.

theorem MIPRE.Introspection.LineProgram.lineRepresentativeProg_time_le : ∃ (R : Polynomial ℕ), ∀ (k : ℕ) (hk : 1 ≤ k) (n : ℕ) (u v : Fin n → (SAT.shoupBinField k hk).carrier), ∃ r ≤ Polynomial.eval (n + k + 1) R, lineRepresentativeProg.code.Runs (Cost.encode (Cost.unary k, (SAT.shoupBinField k hk).vecBits u, (SAT.shoupBinField k hk).vecBits v)) (Cost.encode ((SAT.shoupBinField k hk).vecBits (representative u v))) r

The same program has one polynomial bound in field width plus vector length; the polynomial is independent of both parameters.