Primitives of the repeated sampler and decider

Three loops of the ambient model that the programs of thm:parallel-repetition share (planning/repetition-verifier.md, R3(a)–(b)):

• powBody: on the state (e, bl, bn, acc) — e a unary counter, bl and bn the bit lists of λ and n, acc a list — prepend |bl| + |bn| copies of nil to acc, e times (powLoop_runs). With acc = [] the result is the unary numeral e · (|λ| + |n|); with acc the numeral 1 it is the binary numeral 2^{e(|λ| + |n|)}, the repetition count k(n) and the parse length B(n) of MIPRE.Repetition; with acc the bits of s ≠ 0 it is 2^{e(|λ| + |n|)} · s, the dimension of the repeated sampler.
• dblBody: on (m, acc), m a unary counter and acc a unary numeral, double acc m times (dblLoop_runs): the unary numeral 2^m from the unary numeral m.
• takeBody and chunkBody: cut a list into pieces of s elements (Data.chunks), s given in unary (chunkLoop_runs): the blocks of a vector of 𝔽₂^{k s}.

def MIPRE.Cost.Data.toList : Data → List Data

The elements of a datum read as a list: every datum is a cons-chain ending in nil.

Equations

• MIPRE.Cost.Data.nil.toList = []
• (a.cons b).toList = a :: b.toList

@[simp]

theorem MIPRE.Cost.Data.list_toList (d : Data) : list d.toList = d

@[simp]

theorem MIPRE.Cost.Data.toList_list (l : List Data) : (list l).toList = l

theorem MIPRE.Cost.Data.size_list_append (l₁ l₂ : List Data) : (list (l₁ ++ l₂)).size + 1 = (list l₁).size + (list l₂).size

theorem MIPRE.Cost.Data.size_list_reverse (l : List Data) : (list l.reverse).size = (list l).size

theorem MIPRE.Cost.Data.size_list_take_le (s : ℕ) (l : List Data) : (list (List.take s l)).size ≤ (list l).size

theorem MIPRE.Cost.Data.size_list_drop_le (s : ℕ) (l : List Data) : (list (List.drop s l)).size ≤ (list l).size

theorem MIPRE.Cost.Data.length_le_size_list' (l : List Data) : l.length + 1 ≤ (list l).size

def MIPRE.Cost.Data.chunk {α : Type u_1} (s i : ℕ) (l : List α) : List α

The i-th piece of s elements of a list.

Equations

• MIPRE.Cost.Data.chunk s i l = List.take s (List.drop (i * s) l)

@[irreducible]

def MIPRE.Cost.Data.chunkPairs (s : ℕ) (hs : 0 < s) : List Data → List Data → List (List Data × List Data)

The pieces of s elements of two lists, in lockstep: as many as the first list has, the second one's possibly shorter or empty.

Equations

• MIPRE.Cost.Data.chunkPairs s hs [] x✝ = []
• MIPRE.Cost.Data.chunkPairs s hs (h :: l) x✝ = (List.take s (h :: l), List.take s x✝) :: MIPRE.Cost.Data.chunkPairs s hs (List.drop s (h :: l)) (List.drop s x✝)

theorem MIPRE.Cost.Data.chunkPairs_nil (s : ℕ) (hs : 0 < s) (y : List Data) : chunkPairs s hs [] y = []

theorem MIPRE.Cost.Data.chunkPairs_cons (s : ℕ) (hs : 0 < s) (h : Data) (l y : List Data) : chunkPairs s hs (h :: l) y = (List.take s (h :: l), List.take s y) :: chunkPairs s hs (List.drop s (h :: l)) (List.drop s y)

theorem MIPRE.Cost.Data.chunkPairs_of_ne_nil (s : ℕ) (hs : 0 < s) {l : List Data} (hl : l ≠ []) (y : List Data) : chunkPairs s hs l y = (List.take s l, List.take s y) :: chunkPairs s hs (List.drop s l) (List.drop s y)

theorem MIPRE.Cost.Data.chunkPairs_eq_ofFn (s : ℕ) (hs : 0 < s) (k : ℕ) (l y : List Data) : l.length = k * s → chunkPairs s hs l y = List.ofFn fun (i : Fin k) => (chunk s (↑i) l, chunk s (↑i) y)

With the first list of length k · s, the pairs are the k pairs of pieces.

theorem MIPRE.Cost.Data.size_le_of_mem_chunkPairs (s : ℕ) (hs : 0 < s) (l y : List Data) (p : List Data × List Data) : p ∈ chunkPairs s hs l y → (list p.1).size ≤ (list l).size ∧ (list p.2).size ≤ (list y).size

Every piece is a piece of the list it came from: the sizes are bounded.

theorem Nat.bits_two_pow_mul (m : ℕ) {s : ℕ} (hs : s ≠ 0) : (2 ^ m * s).bits = List.replicate m false ++ s.bits

The binary digits of 2^m · s, for s ≠ 0: m zeros then those of s.

Prepending e · (|bl| + |bn|) copies of nil

def MIPRE.Cost.Prog.powBody : Prog

Body of the power walk: on the state cons u (cons bl (cons bn acc)), stop with acc if the counter u is empty, and otherwise walk bn then bl, prepending a nil to acc per element, and decrement u.

Equations

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

theorem MIPRE.Cost.Prog.powBody_wellScoped : WellScoped 1 powBody

def MIPRE.Cost.Prog.powState (e : ℕ) (bl bn acc : List Data) : Data

The state of the power walk.

Equations

• MIPRE.Cost.Prog.powState e bl bn acc = (MIPRE.Cost.Data.ofNat e).cons ((MIPRE.Cost.Data.list bl).cons ((MIPRE.Cost.Data.list bn).cons (MIPRE.Cost.Data.list acc)))

theorem MIPRE.Cost.Prog.powBody_stop (bl bn acc : List Data) : ∃ t ≤ (Data.list acc).size + 8, Eval [powState 0 bl bn acc] powBody (Data.nil.cons (Data.list acc)) t

theorem MIPRE.Cost.Prog.size_list_replicate_nil_append (m : ℕ) (acc : List Data) : (Data.list (List.replicate m Data.nil ++ acc)).size = 2 * m + (Data.list acc).size

The size of a list of m copies of nil in front of acc.

theorem MIPRE.Cost.Prog.powBody_step (e : ℕ) (bl bn acc : List Data) : ∃ t ≤ (bn.length + 1) * ((Data.list bl).size + (Data.list bn).size + (Data.list acc).size + 2 * bn.length + 13) + (bl.length + 1) * ((Data.list bl).size + (Data.list bn).size + (Data.list acc).size + 2 * bn.length + 2 * bl.length + 13) + 4 * ((Data.list bl).size + (Data.list bn).size + (Data.list acc).size + 2 * e + 2 * bn.length + 2 * bl.length) + 40, Eval [powState (e + 1) bl bn acc] powBody ((Data.nil.cons Data.nil).cons (powState e bl bn (List.replicate (bl.length + bn.length) Data.nil ++ acc))) t

One iteration of the power walk.

def MIPRE.Cost.Prog.powCost (e L sz : ℕ) : ℕ

The cost of the power walk with counter e on lists of total length L and total size Σ: (e + 1) rounds, each polynomial in the sizes.

Equations

• MIPRE.Cost.Prog.powCost e L sz = (e + 1) * (8 * (L + 1) * (sz + 2 * e * L + e + 14))

theorem MIPRE.Cost.Prog.powLoop_runs (e : ℕ) (bl bn acc : List Data) (env : Env) : ∃ t ≤ powCost e (bl.length + bn.length) ((Data.list bl).size + (Data.list bn).size + (Data.list acc).size), Eval (powState e bl bn acc :: env) powBody.loop (Data.list (List.replicate (e * (bl.length + bn.length)) Data.nil ++ acc)) t

The power walk: e rounds, each prepending |bl| + |bn| copies of nil.

Doubling a unary numeral

def MIPRE.Cost.Prog.dblBody : Prog

Body of the doubling loop: on the state cons u acc, stop with acc if the counter u is empty, and otherwise replace acc by acc ++ acc (reversal onto itself, acc being a list of nils) and decrement u.

Equations

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

theorem MIPRE.Cost.Prog.dblBody_wellScoped : WellScoped 1 dblBody

theorem MIPRE.Cost.Prog.dblBody_stop (a : ℕ) : ∃ t ≤ 2 * a + 8, Eval [(Data.ofNat 0).cons (Data.ofNat a)] dblBody (Data.nil.cons (Data.ofNat a)) t

theorem MIPRE.Cost.Prog.dblBody_step (m a : ℕ) : ∃ t ≤ (a + 1) * (4 * a + 14) + 10 * a + 2 * m + 30, Eval [(Data.ofNat (m + 1)).cons (Data.ofNat a)] dblBody ((Data.nil.cons Data.nil).cons ((Data.ofNat m).cons (Data.ofNat (2 * a)))) t

def MIPRE.Cost.Prog.dblCost (m a : ℕ) : ℕ

The cost of the doubling loop: m rounds from the numeral a, the last on 2^m a.

Equations

• MIPRE.Cost.Prog.dblCost m a = (m + 1) * ((2 ^ m * a + 1) * (4 * 2 ^ m * a + 14) + 10 * 2 ^ m * a + 2 * m + 32)

theorem MIPRE.Cost.Prog.dblLoop_runs (m a : ℕ) (env : Env) : ∃ t ≤ dblCost m a, Eval ((Data.ofNat m).cons (Data.ofNat a) :: env) dblBody.loop (Data.ofNat (2 ^ m * a)) t

The doubling loop: dblBody on (m, a) computes 2^m · a.

Taking a prefix of given unary length

def MIPRE.Cost.Prog.takeBody : Prog

Body of the take loop: on the state cons u (cons rem cur), stop with cons rem cur if the counter u is empty or rem is; otherwise move the head of rem onto cur and decrement.

Equations

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

theorem MIPRE.Cost.Prog.takeBody_wellScoped : WellScoped 1 takeBody

def MIPRE.Cost.Prog.takeState (c : ℕ) (rem cur : List Data) : Data

The state of the take loop.

Equations

• MIPRE.Cost.Prog.takeState c rem cur = (MIPRE.Cost.Data.ofNat c).cons ((MIPRE.Cost.Data.list rem).cons (MIPRE.Cost.Data.list cur))

theorem MIPRE.Cost.Prog.takeBody_stop_counter (rem cur : List Data) : ∃ t ≤ (Data.list rem).size + (Data.list cur).size + 8, Eval [takeState 0 rem cur] takeBody (Data.nil.cons ((Data.list rem).cons (Data.list cur))) t

theorem MIPRE.Cost.Prog.takeBody_stop_empty (c : ℕ) (cur : List Data) : ∃ t ≤ (Data.list cur).size + 2 * c + 12, Eval [takeState (c + 1) [] cur] takeBody (Data.nil.cons ((Data.list []).cons (Data.list cur))) t

theorem MIPRE.Cost.Prog.takeBody_step (c : ℕ) (h : Data) (rem cur : List Data) : ∃ t ≤ (Data.list rem).size + h.size + (Data.list cur).size + 2 * c + 18, Eval [takeState (c + 1) (h :: rem) cur] takeBody ((Data.nil.cons Data.nil).cons (takeState c rem (h :: cur))) t

theorem MIPRE.Cost.Prog.takeLoop_runs (c : ℕ) (rem cur : List Data) (env : Env) : ∃ t ≤ (c + 1) * ((Data.list rem).size + (Data.list cur).size + 2 * c + 20), Eval (takeState c rem cur :: env) takeBody.loop ((Data.list (List.drop c rem)).cons (Data.list ((List.take c rem).reverse ++ cur))) t

The take loop: c elements moved from rem onto cur, reversed.