The bit-query program

bitAtProg on (y, m) — a bit string and a binary index — returns the m-th bit of y, or the out-of-range marker ofNat 2: this is the answer a succinct description must give ([MNY, Definition 2.4]; bitQueryAnswer). It walks y while decrementing m in binary, testing for zero at each step, so its cost is (|y| + 1) · bitAtIter (size y) |m| with bitAtIter quadratic in |m| (each zero test and decrement copies the index). This is where the (|m| + 1) ^ 2 factor of the succinctness budget of IsSuccinctDesc comes from.

def MIPRE.Cost.bitQueryAnswer (x : BitStr) (m : ℕ) : Data

The answer a succinct description must give to the bit-query m about the string x: the m-th bit for m < |x|, and the out-of-range marker (the unary numeral 2) otherwise.

Equations

• MIPRE.Cost.bitQueryAnswer x m = if h : m < List.length x then MIPRE.Cost.encode (List.get x ⟨m, h⟩) else MIPRE.Cost.Data.ofNat 2

@[simp]

theorem MIPRE.Cost.bitQueryAnswer_nil (m : ℕ) : bitQueryAnswer [] m = Data.ofNat 2

@[simp]

theorem MIPRE.Cost.bitQueryAnswer_cons_zero (b : Bool) (x : BitStr) : bitQueryAnswer (b :: x) 0 = encode b

@[simp]

theorem MIPRE.Cost.bitQueryAnswer_cons_succ (b : Bool) (x : BitStr) (m : ℕ) : bitQueryAnswer (b :: x) (m + 1) = bitQueryAnswer x m

def MIPRE.Cost.Prog.zeroBound (L : ℕ) : ℕ

Cost of one zero test on a bit string of length L.

Equations

• MIPRE.Cost.Prog.zeroBound L = (L + 1) * (4 * L + 1 + 8)

def MIPRE.Cost.Prog.decBound (L : ℕ) : ℕ

Cost of one decrement on a bit string of length L.

Equations

• MIPRE.Cost.Prog.decBound L = (L + 2) * (10 * (6 * L + 4) + 60)

def MIPRE.Cost.Prog.bitAtIter (sy L : ℕ) : ℕ

Cost of one iteration of bitAtProg with a string of size at most sy and an index of L bits.

Equations

• MIPRE.Cost.Prog.bitAtIter sy L = sy + 8 * L + MIPRE.Cost.Prog.zeroBound L + MIPRE.Cost.Prog.decBound L + 20

theorem MIPRE.Cost.Prog.isZeroProg_runs' (mb : BitStr) (env : Env) : ∃ t ≤ zeroBound (List.length mb), Eval (encode mb :: env) isZeroProg (encode (List.any mb id)) t

theorem MIPRE.Cost.Prog.decProg_runs' (mb : BitStr) (h : List.any mb id = true) : ∃ (mb' : BitStr), ∃ t ≤ decBound (List.length mb), List.length mb' = List.length mb ∧ bitsVal mb' + 1 = bitsVal mb ∧ decProg.Runs (encode mb) (encode mb') t

def MIPRE.Cost.Prog.bitAtBody : Prog

Body of bitAtProg: on state cons y m, stop with ofNat 2 if y is exhausted; else test m for zero: if zero, stop with the head bit of y; otherwise continue with the tail of y and m - 1.

Equations

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

def MIPRE.Cost.Prog.bitAtProg : Prog

bitAtProg on cons (encode y) (encode m) computes bitQueryAnswer y m.

Equations

• MIPRE.Cost.Prog.bitAtProg = MIPRE.Cost.Prog.bitAtBody.loop

theorem MIPRE.Cost.Prog.bitAtBody_wellScoped : WellScoped 1 bitAtBody

theorem MIPRE.Cost.Prog.bitAtProg_wellScoped : WellScoped 1 bitAtProg

theorem MIPRE.Cost.Prog.bitAtBody_nil (mb : BitStr) : Eval [(encode []).cons (encode mb)] bitAtBody (Data.nil.cons (Data.ofNat 2)) 9

The body on an exhausted string: stop with the out-of-range marker.

theorem MIPRE.Cost.Prog.bitAtBody_zero (b : Bool) (ys mb : BitStr) (hz : List.any mb id = false) (tz : ℕ) (hzr : Eval [encode mb] isZeroProg (encode (List.any mb id)) tz) : Eval [(encode (b :: ys)).cons (encode mb)] bitAtBody (Data.nil.cons (encode b)) ((encode mb).size + tz + (encode b).size + 9)

The body when the index is zero: stop with the head bit.

theorem MIPRE.Cost.Prog.bitAtBody_succ (b : Bool) (ys mb mb' : BitStr) (hz : List.any mb id = true) (tz td : ℕ) (hzr : Eval [encode mb] isZeroProg (encode (List.any mb id)) tz) (hd : Eval [encode mb] decProg (encode mb') td) : Eval [(encode (b :: ys)).cons (encode mb)] bitAtBody ((Data.nil.cons Data.nil).cons ((encode ys).cons (encode mb'))) (2 * (encode mb).size + tz + td + (encode ys).size + 14)

The body when the index is nonzero: continue with the tail and the decremented index.

theorem MIPRE.Cost.Prog.bitAtLoop_runs (m : ℕ) (y mb : BitStr) (hmb : bitsVal mb = m) (env : Env) (sy L : ℕ) (hsy : (encode y).size ≤ sy) (hL : List.length mb = L) : ∃ t ≤ (List.length y + 1) * bitAtIter sy L, Eval ((encode y).cons (encode mb) :: env) bitAtProg (bitQueryAnswer y m) t

The loop of bitAtProg, by induction on the queried index.

theorem MIPRE.Cost.Prog.bitAtProg_runs (y : BitStr) (m : ℕ) : ∃ t ≤ (List.length y + 1) * bitAtIter (encode y).size m.size, bitAtProg.Runs ((encode y).cons (encode m)) (bitQueryAnswer y m) t

bitAtProg answers bit queries: on (encode y, encode m) it computes bitQueryAnswer y m, in time (|y| + 1) · bitAtIter (size y) (Nat.size m).

theorem MIPRE.Cost.Prog.bitAtIter_le (sy L : ℕ) : bitAtIter sy L ≤ (sy + 534) * (L + 1) ^ 2

bitAtIter is quadratic in the length of the index.