Documentation

MIPRE.Foundations.Introspection.SeededLineProg

Uniform programs for the seeded axis and diagonal stages #

The field width, selector width, seed and vector data are all inputs of fixed programs. Indices stay binary. The bounded vector scan masks the selected direction or axis coordinate, and the diagonal stage invokes the actual Shoup line-representative program. Malformed inputs still halt in polynomial time.

noncomputable def MIPRE.Introspection.SeededLineProgram.indexedRows :

Cost.PolyTimeFun (List Cost.BitStr) (List (ℕ × Cost.BitStr))

Equations

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

Instances For

theorem MIPRE.Introspection.SeededLineProgram.indexedRows_apply (l : List Cost.BitStr) :

indexedRows.toFun l = (List.range' 0 l.length).zip l

noncomputable def MIPRE.Introspection.SeededLineProgram.maskBeforeStep :

Cost.PolyTimeFun ((ℕ × Cost.BitStr) × Cost.Unary × ℕ) Cost.BitStr

Equations

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

Instances For

noncomputable def MIPRE.Introspection.SeededLineProgram.maskBeforeProg :

Cost.PolyTimeFun (Cost.Unary × ℕ × List Cost.BitStr) (List Cost.BitStr)

Zero all coordinates strictly before the supplied binary index.

Equations

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

Instances For

theorem MIPRE.Introspection.SeededLineProgram.maskBeforeProg_apply (k : Cost.Unary) (i : ℕ) (v : List Cost.BitStr) :

maskBeforeProg.toFun (k, i, v) = List.map (fun (p : ℕ × Cost.BitStr) => if i ≤ p.1 then p.2 else SAT.shoupZeroProg.toFun k) ((List.range' 0 v.length).zip v)

theorem MIPRE.Introspection.SeededLineProgram.maskBeforeProg_correct (k : ℕ) (hk : 1 ≤ k) {n : ℕ} (i : ℕ) (v : Fin n → (SAT.shoupBinField k hk).carrier) :

maskBeforeProg.toFun (Cost.unary k, i, (SAT.shoupBinField k hk).vecBits v) = (SAT.shoupBinField k hk).vecBits fun (j : Fin n) => if ↑j < i then 0 else v j

noncomputable def MIPRE.Introspection.SeededLineProgram.zeroCoordinateStep :

Cost.PolyTimeFun ((ℕ × Cost.BitStr) × Cost.Unary × ℕ) Cost.BitStr

Equations

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

Instances For

noncomputable def MIPRE.Introspection.SeededLineProgram.zeroCoordinateProg :

Cost.PolyTimeFun (Cost.Unary × ℕ × List Cost.BitStr) (List Cost.BitStr)

Zero only the selected axis coordinate.

Equations

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

Instances For

theorem MIPRE.Introspection.SeededLineProgram.zeroCoordinateProg_apply (k : Cost.Unary) (i : ℕ) (v : List Cost.BitStr) :

zeroCoordinateProg.toFun (k, i, v) = List.map (fun (p : ℕ × Cost.BitStr) => if i = p.1 then SAT.shoupZeroProg.toFun k else p.2) ((List.range' 0 v.length).zip v)

theorem MIPRE.Introspection.SeededLineProgram.zeroCoordinateProg_correct (k : ℕ) (hk : 1 ≤ k) {n : ℕ} (i : Fin n) (v : Fin n → (SAT.shoupBinField k hk).carrier) :

zeroCoordinateProg.toFun (Cost.unary k, ↑i, (SAT.shoupBinField k hk).vecBits v) = (SAT.shoupBinField k hk).vecBits fun (j : Fin n) => if j = i then 0 else v j

noncomputable def MIPRE.Introspection.SeededLineProgram.axisRepresentativeProg :

Cost.PolyTimeFun ((Cost.Unary × Cost.Unary × Cost.BitStr) × List Cost.BitStr) (List Cost.BitStr)

Raw input contains the unary field and selector widths, followed by the canonical seed and the point vector.

Equations

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

Instances For

theorem MIPRE.Introspection.SeededLineProgram.axisRepresentativeProg_correct (k : ℕ) (hk : 1 ≤ k) (j : ℕ) (hj : j ≤ k) (s : (SAT.shoupBinField k hk).carrier) (u : Fin (2 ^ j) → (SAT.shoupBinField k hk).carrier) :

axisRepresentativeProg.toFun ((Cost.unary k, Cost.unary j, (SAT.shoupBinField k hk).toBits s), (SAT.shoupBinField k hk).vecBits u) = (SAT.shoupBinField k hk).vecBits fun (i : Fin (2 ^ j)) => if i = SeedProgram.selector (SAT.shoupBinField k hk) j hj s then 0 else u i

noncomputable def MIPRE.Introspection.SeededLineProgram.selectedDirectionProg :

Cost.PolyTimeFun ((Cost.Unary × Cost.Unary × Cost.BitStr) × List Cost.BitStr) (List Cost.BitStr)

Equations

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

Instances For

theorem MIPRE.Introspection.SeededLineProgram.selectedDirectionProg_correct (k : ℕ) (hk : 1 ≤ k) (j : ℕ) (hj : j ≤ k) (s : (SAT.shoupBinField k hk).carrier) (v : Fin (2 ^ j) → (SAT.shoupBinField k hk).carrier) :

selectedDirectionProg.toFun ((Cost.unary k, Cost.unary j, (SAT.shoupBinField k hk).toBits s), (SAT.shoupBinField k hk).vecBits v) = (SAT.shoupBinField k hk).vecBits fun (i : Fin (2 ^ j)) => if i < SeedProgram.selector (SAT.shoupBinField k hk) j hj s then 0 else v i

noncomputable def MIPRE.Introspection.SeededLineProgram.diagonalRepresentativeProg :

Cost.PolyTimeFun ((Cost.Unary × Cost.Unary × Cost.BitStr) × List Cost.BitStr × List Cost.BitStr) (List Cost.BitStr × List Cost.BitStr)

The actual diagonal stage returns the canonical point and selected direction, preserving the seed in the caller's first-stage register.

Equations

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

Instances For

theorem MIPRE.Introspection.SeededLineProgram.diagonalRepresentativeProg_correct (k : ℕ) (hk : 1 ≤ k) (j : ℕ) (hj : j ≤ k) (s : (SAT.shoupBinField k hk).carrier) (u v : Fin (2 ^ j) → (SAT.shoupBinField k hk).carrier) :

have v' := fun (i : Fin (2 ^ j)) => if i < SeedProgram.selector (SAT.shoupBinField k hk) j hj s then 0 else v i; diagonalRepresentativeProg.toFun ((Cost.unary k, Cost.unary j, (SAT.shoupBinField k hk).toBits s), (SAT.shoupBinField k hk).vecBits u, (SAT.shoupBinField k hk).vecBits v) = ((SAT.shoupBinField k hk).vecBits (LineProgram.representative u v'), (SAT.shoupBinField k hk).vecBits v')

theorem MIPRE.Introspection.SeededLineProgram.axisRepresentativeProg_runs (x : (Cost.Unary × Cost.Unary × Cost.BitStr) × List Cost.BitStr) :

∃ r ≤ Polynomial.eval (Cost.esize x) axisRepresentativeProg.timeBound, axisRepresentativeProg.code.Runs (Cost.encode x) (Cost.encode (axisRepresentativeProg.toFun x)) r