The stage programs of a copy of the PCP sampler

Piece AR-3d of planning/answer-reduction.md: polynomial-time functions answering the queries of one copy of the seeded test, on the three runs of k-bit blocks (MIPRE/Background/ AnswerReduction/Layout). A copy is described by its offset o, length sz = 2^jw, selector width jw and seed index c, all in unary (Desc), and a test type numbered 0, 1, 2.

The answers are first written as plain functions of the blocks (margL, linL, facL), with the field arithmetic done by the introspection stage programs (selectedDirectionProg, axisRepresentativeProg, lineRepresentativeProg); copyProg computes them.

@[reducible, inline]

abbrev MIPRE.AnswerReduction.StageProg.Desc : Type

A copy: offset, length, selector width and seed index, in unary.

Equations

• MIPRE.AnswerReduction.StageProg.Desc = (MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary)

@[reducible, inline]

abbrev MIPRE.AnswerReduction.StageProg.Blocks : Type

The three runs of blocks: point, direction, seeds.

Equations

• MIPRE.AnswerReduction.StageProg.Blocks = (List MIPRE.Cost.BitStr × List MIPRE.Cost.BitStr × List MIPRE.Cost.BitStr)

The answers, as functions of the blocks

def MIPRE.AnswerReduction.StageProg.zb (k : Cost.Unary) : Cost.BitStr

The zero field element.

Equations

• MIPRE.AnswerReduction.StageProg.zb k = List.map (fun (x : Unit) => false) k

def MIPRE.AnswerReduction.StageProg.zeroed (k : Cost.Unary) (l : List Cost.BitStr) : List Cost.BitStr

Every block replaced by zero.

Equations

• MIPRE.AnswerReduction.StageProg.zeroed k l = List.map (fun (x : MIPRE.Cost.BitStr) => MIPRE.AnswerReduction.StageProg.zb k) l

def MIPRE.AnswerReduction.StageProg.seedOf (d : Desc) (seeds : List Cost.BitStr) : Cost.BitStr

The copy's seed.

Equations

• MIPRE.AnswerReduction.StageProg.seedOf d seeds = (List.drop (List.length d.2.2.2) seeds).headD []

noncomputable def MIPRE.AnswerReduction.StageProg.selDirL (k : Cost.Unary) (d : Desc) (s : Cost.BitStr) (w : List Cost.BitStr) : List Cost.BitStr

The selected direction of a diagonal line.

Equations

• MIPRE.AnswerReduction.StageProg.selDirL k d s w = MIPRE.Introspection.SeededLineProgram.selectedDirectionProg.toFun ((k, d.2.2.1, s), w)

noncomputable def MIPRE.AnswerReduction.StageProg.ptMapL (k : Cost.Unary) (d : Desc) (τ : ℕ) (s : Cost.BitStr) (dir w : List Cost.BitStr) : List Cost.BitStr

The third stage's map of the point register.

Equations

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

def MIPRE.AnswerReduction.StageProg.seedOut (k : Cost.Unary) (d : Desc) (τ : ℕ) (s : Cost.BitStr) (seeds : List Cost.BitStr) : List Cost.BitStr

The seed run of the first stage.

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.dirOut (k : Cost.Unary) (d : Desc) (τ : ℕ) (s : Cost.BitStr) (dirs : List Cost.BitStr) : List Cost.BitStr

The direction run of the second stage.

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.ptOut (k : Cost.Unary) (d : Desc) (τ : ℕ) (s : Cost.BitStr) (dir pts : List Cost.BitStr) : List Cost.BitStr

The point run of the third stage.

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.margL (k : Cost.Unary) (d : Desc) (τ j : ℕ) (x : Blocks) : Blocks

The marginal at level j.

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.linL (k : Cost.Unary) (d : Desc) (τ j : ℕ) (u y : Blocks) : Blocks

The stage map at level j, from the prefix u, applied to y.

Equations

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

def MIPRE.AnswerReduction.StageProg.blk (k : Cost.Unary) (b : Bool) : Cost.BitStr

The block of k copies of a bit.

Equations

• MIPRE.AnswerReduction.StageProg.blk k b = List.map (fun (x : Unit) => b) k

def MIPRE.AnswerReduction.StageProg.facL (k : Cost.Unary) (d : Desc) (j : ℕ) (u : Blocks) : Blocks

The factor space at level j, as blocks of indicator bits.

Equations

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

def MIPRE.AnswerReduction.StageProg.blocksOf (k m' : Cost.Unary) (z : Cost.BitStr) : Blocks

The runs of a bit string of 2m' + 6 blocks of k bits.

Equations

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

def MIPRE.AnswerReduction.StageProg.bitsOf (x : Blocks) : Cost.BitStr

The bits of three runs.

Equations

• MIPRE.AnswerReduction.StageProg.bitsOf x = (x.1 ++ x.2.1 ++ x.2.2).flatten

noncomputable def MIPRE.AnswerReduction.StageProg.copyAnswer (k : Cost.Unary) (d : Desc) (τ : ℕ) (m' : Cost.Unary) (kind j : ℕ) (u y : Cost.BitStr) : Cost.BitStr

The answer of a copy to a query of kind kind at level j with vectors u, y.

Equations

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

The programs

noncomputable def MIPRE.AnswerReduction.StageProg.placeP : Cost.PolyTimeFun (Cost.BitStr × Cost.Unary × List Cost.BitStr × List Cost.BitStr) (List Cost.BitStr)

Placing, as a program: (fill, o, w, l) ↦ placeL fill o w l.

Equations

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

@[simp]

theorem MIPRE.AnswerReduction.StageProg.placeP_apply (fill : Cost.BitStr) (o : Cost.Unary) (w l : List Cost.BitStr) : placeP.toFun (fill, o, w, l) = Pcp.placeL fill (List.length o) w l

noncomputable def MIPRE.AnswerReduction.StageProg.sliceP : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × List Cost.BitStr) (List Cost.BitStr)

Slicing, as a program: (o, sz, l) ↦ sliceL o sz l.

Equations

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

@[simp]

theorem MIPRE.AnswerReduction.StageProg.sliceP_apply (o sz : Cost.Unary) (l : List Cost.BitStr) : sliceP.toFun (o, sz, l) = Pcp.sliceL (List.length o) (List.length sz) l

@[reducible, inline]

abbrev MIPRE.AnswerReduction.StageProg.Input : Type

The input of a copy's program: (k, d, τ, m', kind, j, u, y).

Equations

• MIPRE.AnswerReduction.StageProg.Input = (MIPRE.Cost.Unary × MIPRE.AnswerReduction.StageProg.Desc × ℕ × MIPRE.Cost.Unary × ℕ × ℕ × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr)

noncomputable def MIPRE.AnswerReduction.StageProg.kI : Cost.PolyTimeFun Input Cost.Unary

Equations

• MIPRE.AnswerReduction.StageProg.kI = MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.AnswerReduction.StageProg.dI : Cost.PolyTimeFun Input Desc

Equations

• MIPRE.AnswerReduction.StageProg.dI = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.AnswerReduction.StageProg.τI : Cost.PolyTimeFun Input ℕ

Equations

• MIPRE.AnswerReduction.StageProg.τI = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.AnswerReduction.StageProg.mI : Cost.PolyTimeFun Input Cost.Unary

Equations

• MIPRE.AnswerReduction.StageProg.mI = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.AnswerReduction.StageProg.kindI : Cost.PolyTimeFun Input ℕ

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.jI : Cost.PolyTimeFun Input ℕ

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.uI : Cost.PolyTimeFun Input Cost.BitStr

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.yI : Cost.PolyTimeFun Input Cost.BitStr

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.oI : Cost.PolyTimeFun Input Cost.Unary

Equations

• MIPRE.AnswerReduction.StageProg.oI = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.AnswerReduction.StageProg.dI

noncomputable def MIPRE.AnswerReduction.StageProg.szI : Cost.PolyTimeFun Input Cost.Unary

Equations

• MIPRE.AnswerReduction.StageProg.szI = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.AnswerReduction.StageProg.dI)

noncomputable def MIPRE.AnswerReduction.StageProg.jwI : Cost.PolyTimeFun Input Cost.Unary

Equations

• MIPRE.AnswerReduction.StageProg.jwI = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.AnswerReduction.StageProg.dI))

noncomputable def MIPRE.AnswerReduction.StageProg.cI : Cost.PolyTimeFun Input Cost.Unary

Equations

• MIPRE.AnswerReduction.StageProg.cI = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.AnswerReduction.StageProg.dI))

noncomputable def MIPRE.AnswerReduction.StageProg.zbP : Cost.PolyTimeFun Input Cost.BitStr

Equations

• MIPRE.AnswerReduction.StageProg.zbP = (MIPRE.Cost.PolyTimeFun.const false).map.comp MIPRE.AnswerReduction.StageProg.kI

noncomputable def MIPRE.AnswerReduction.StageProg.blkP (b : Bool) : Cost.PolyTimeFun Input Cost.BitStr

Equations

• MIPRE.AnswerReduction.StageProg.blkP b = (MIPRE.Cost.PolyTimeFun.const b).map.comp MIPRE.AnswerReduction.StageProg.kI

noncomputable def MIPRE.AnswerReduction.StageProg.zeroedP (l : Cost.PolyTimeFun Input (List Cost.BitStr)) : Cost.PolyTimeFun Input (List Cost.BitStr)

Equations

• MIPRE.AnswerReduction.StageProg.zeroedP l = MIPRE.Cost.PolyTimeFun.snd.mapWith.comp (l.pair MIPRE.AnswerReduction.StageProg.zbP)

noncomputable def MIPRE.AnswerReduction.StageProg.isτ (t : ℕ) : Cost.PolyTimeFun Input Bool

Equations

• MIPRE.AnswerReduction.StageProg.isτ t = MIPRE.SAT.ArrayProg.eqNat.ap₂ MIPRE.AnswerReduction.StageProg.τI (MIPRE.Cost.PolyTimeFun.const t)

noncomputable def MIPRE.AnswerReduction.StageProg.blocksP (z : Cost.PolyTimeFun Input Cost.BitStr) : Cost.PolyTimeFun Input Blocks

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.seedOfP (seeds : Cost.PolyTimeFun Input (List Cost.BitStr)) : Cost.PolyTimeFun Input Cost.BitStr

Equations

• MIPRE.AnswerReduction.StageProg.seedOfP seeds = (MIPRE.Cost.PolyTimeFun.headD []).comp (MIPRE.Cost.PolyTimeFun.drop.comp (seeds.pair MIPRE.AnswerReduction.StageProg.cI))

noncomputable def MIPRE.AnswerReduction.StageProg.selDirP (s : Cost.PolyTimeFun Input Cost.BitStr) (w : Cost.PolyTimeFun Input (List Cost.BitStr)) : Cost.PolyTimeFun Input (List Cost.BitStr)

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.ptMapP (s : Cost.PolyTimeFun Input Cost.BitStr) (dir w : Cost.PolyTimeFun Input (List Cost.BitStr)) : Cost.PolyTimeFun Input (List Cost.BitStr)

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.sliceI (l : Cost.PolyTimeFun Input (List Cost.BitStr)) : Cost.PolyTimeFun Input (List Cost.BitStr)

Equations

• MIPRE.AnswerReduction.StageProg.sliceI l = MIPRE.AnswerReduction.StageProg.sliceP.comp (MIPRE.AnswerReduction.StageProg.oI.pair (MIPRE.AnswerReduction.StageProg.szI.pair l))

noncomputable def MIPRE.AnswerReduction.StageProg.seedOutP (s : Cost.PolyTimeFun Input Cost.BitStr) (seeds : Cost.PolyTimeFun Input (List Cost.BitStr)) : Cost.PolyTimeFun Input (List Cost.BitStr)

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.dirOutP (s : Cost.PolyTimeFun Input Cost.BitStr) (dirs : Cost.PolyTimeFun Input (List Cost.BitStr)) : Cost.PolyTimeFun Input (List Cost.BitStr)

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.ptOutP (s : Cost.PolyTimeFun Input Cost.BitStr) (dir pts : Cost.PolyTimeFun Input (List Cost.BitStr)) : Cost.PolyTimeFun Input (List Cost.BitStr)

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.margP (x : Cost.PolyTimeFun Input Blocks) : Cost.PolyTimeFun Input Blocks

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.isJ (t : ℕ) : Cost.PolyTimeFun Input Bool

Equations

• MIPRE.AnswerReduction.StageProg.isJ t = MIPRE.SAT.ArrayProg.eqNat.ap₂ MIPRE.AnswerReduction.StageProg.jI (MIPRE.Cost.PolyTimeFun.const t)

noncomputable def MIPRE.AnswerReduction.StageProg.linP (u y : Cost.PolyTimeFun Input Blocks) : Cost.PolyTimeFun Input Blocks

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.constBlk (b : Bool) (l : Cost.PolyTimeFun Input (List Cost.BitStr)) : Cost.PolyTimeFun Input (List Cost.BitStr)

Equations

• MIPRE.AnswerReduction.StageProg.constBlk b l = MIPRE.Cost.PolyTimeFun.snd.mapWith.comp (l.pair (MIPRE.AnswerReduction.StageProg.blkP b))

noncomputable def MIPRE.AnswerReduction.StageProg.facP (u : Cost.PolyTimeFun Input Blocks) : Cost.PolyTimeFun Input Blocks

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.bitsP (x : Cost.PolyTimeFun Input Blocks) : Cost.PolyTimeFun Input Cost.BitStr

Equations

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

noncomputable def MIPRE.AnswerReduction.StageProg.isKind (t : ℕ) : Cost.PolyTimeFun Input Bool

Equations

• MIPRE.AnswerReduction.StageProg.isKind t = MIPRE.SAT.ArrayProg.eqNat.ap₂ MIPRE.AnswerReduction.StageProg.kindI (MIPRE.Cost.PolyTimeFun.const t)

noncomputable def MIPRE.AnswerReduction.StageProg.copyProg : Cost.PolyTimeFun Input Cost.BitStr

The program of a copy.

Equations

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

theorem MIPRE.AnswerReduction.StageProg.blocksP_apply (x : Input) (z : Cost.PolyTimeFun Input Cost.BitStr) : (blocksP z).toFun x = blocksOf (kI.toFun x) (mI.toFun x) (z.toFun x)

theorem MIPRE.AnswerReduction.StageProg.ptMapP_apply (x : Input) (s : Cost.PolyTimeFun Input Cost.BitStr) (dir w : Cost.PolyTimeFun Input (List Cost.BitStr)) : (ptMapP s dir w).toFun x = ptMapL (kI.toFun x) (dI.toFun x) (τI.toFun x) (s.toFun x) (dir.toFun x) (w.toFun x)

theorem MIPRE.AnswerReduction.StageProg.seedOutP_apply (x : Input) (s : Cost.PolyTimeFun Input Cost.BitStr) (seeds : Cost.PolyTimeFun Input (List Cost.BitStr)) : (seedOutP s seeds).toFun x = seedOut (kI.toFun x) (dI.toFun x) (τI.toFun x) (s.toFun x) (seeds.toFun x)

theorem MIPRE.AnswerReduction.StageProg.dirOutP_apply (x : Input) (s : Cost.PolyTimeFun Input Cost.BitStr) (dirs : Cost.PolyTimeFun Input (List Cost.BitStr)) : (dirOutP s dirs).toFun x = dirOut (kI.toFun x) (dI.toFun x) (τI.toFun x) (s.toFun x) (dirs.toFun x)

theorem MIPRE.AnswerReduction.StageProg.ptOutP_apply (x : Input) (s : Cost.PolyTimeFun Input Cost.BitStr) (dir pts : Cost.PolyTimeFun Input (List Cost.BitStr)) : (ptOutP s dir pts).toFun x = ptOut (kI.toFun x) (dI.toFun x) (τI.toFun x) (s.toFun x) (dir.toFun x) (pts.toFun x)

theorem MIPRE.AnswerReduction.StageProg.margP_apply (x : Input) (X : Cost.PolyTimeFun Input Blocks) : (margP X).toFun x = margL (kI.toFun x) (dI.toFun x) (τI.toFun x) (jI.toFun x) (X.toFun x)

theorem MIPRE.AnswerReduction.StageProg.linP_apply (x : Input) (U Y : Cost.PolyTimeFun Input Blocks) : (linP U Y).toFun x = linL (kI.toFun x) (dI.toFun x) (τI.toFun x) (jI.toFun x) (U.toFun x) (Y.toFun x)

theorem MIPRE.AnswerReduction.StageProg.facP_apply (x : Input) (U : Cost.PolyTimeFun Input Blocks) : (facP U).toFun x = facL (kI.toFun x) (dI.toFun x) (jI.toFun x) (U.toFun x)

theorem MIPRE.AnswerReduction.StageProg.bitsP_apply (x : Input) (X : Cost.PolyTimeFun Input Blocks) : (bitsP X).toFun x = bitsOf (X.toFun x)

theorem MIPRE.AnswerReduction.StageProg.copyProg_apply (k : Cost.Unary) (d : Desc) (τ : ℕ) (m' : Cost.Unary) (kind j : ℕ) (u y : Cost.BitStr) : copyProg.toFun (k, d, τ, m', kind, j, u, y) = copyAnswer k d τ m' kind j u y