Bounded walks over lists, in the ambient model

The programs with which the wrapper decider of Halting/Wrapper.lean performs the paper's format checks: the questions must be bit strings of the sampler's length, the answers bit strings within the answer-length budget, and equal questions must carry equal answers. All of them walk their input under a budget, so that their cost is the budget times the size of the input — the shape T · (|input| + 1) of Decider.TimeBoundAt — rather than a power of it.

• Prog.bitWalkProg: on cons l u, walk l against the budget u (a list, typically a unary numeral), checking that each element passed is a bit; the result is nil on a non-bit element, and otherwise the pair of what remains of l and of u (Data.bitWalk). Both format checks read off it: |l| = |u| is the result cons nil nil, |l| ≤ |u| a result cons nil _.
• Prog.eqBitsProg: equality of two bit lists (Data.eqBits).
• Prog.normBinProg: the normalization Data.normBin of a parameter, by a walk recording the last bit seen (Data.canonWalk).

Every walk copies the remainder of the lists at each step, which is what the ambient model charges; the cost bounds are (budget + 1) · (S + c) for S the size of the input.

def MIPRE.Cost.Data.spine : Data → ℕ

The length of the right spine: the length of a list.

Equations

• MIPRE.Cost.Data.nil.spine = 0
• (a.cons r).spine = r.spine + 1

@[simp]

theorem MIPRE.Cost.Data.spine_nil : nil.spine = 0

@[simp]

theorem MIPRE.Cost.Data.spine_cons (a r : Data) : (a.cons r).spine = r.spine + 1

theorem MIPRE.Cost.Data.spine_ofNat (n : ℕ) : (ofNat n).spine = n

theorem MIPRE.Cost.Data.spine_le_size (d : Data) : d.spine ≤ d.size

def MIPRE.Cost.Data.bitOf : Data → Bool

The bit an element denotes: nil is false, anything else true.

Equations

• MIPRE.Cost.Data.nil.bitOf = false
• (a.cons r).bitOf = true

@[simp]

theorem MIPRE.Cost.Data.bitOf_ofBool (b : Bool) : (ofBool b).bitOf = b

def MIPRE.Cost.Data.bitWalk : Data → Data → Data

Walk l against the budget u, checking that every element passed is a bit: nil on a non-bit, otherwise the pair of the remainders.

Equations

• MIPRE.Cost.Data.nil.bitWalk x✝ = MIPRE.Cost.Data.nil.cons x✝
• (h.cons l').bitWalk MIPRE.Cost.Data.nil = (h.cons l').cons MIPRE.Cost.Data.nil
• (h.cons l').bitWalk (a.cons u') = if h.isBit = true then l'.bitWalk u' else MIPRE.Cost.Data.nil

theorem MIPRE.Cost.Data.bitWalk_encode (x : BitStr) (u : List Data) : (encode x).bitWalk (list u) = (encode (List.drop u.length x)).cons (list (List.drop (List.length x) u))

On a bit list and a list budget: the walk stops with the remainders.

def MIPRE.Cost.Data.eqBits : Data → Data → Bool

Equality of two bit lists, element by element.

Equations

• MIPRE.Cost.Data.nil.eqBits MIPRE.Cost.Data.nil = true
• (h₁.cons l₁).eqBits (h₂.cons l₂) = (h₁.bitOf == h₂.bitOf && l₁.eqBits l₂)
• x✝¹.eqBits x✝ = false

theorem MIPRE.Cost.Data.eqBits_ofNat (a b : ℕ) : (ofNat a).eqBits (ofNat b) = decide (a = b)

On unary numerals, eqBits is equality of the numbers: every element is nil, so the walk compares only the lengths.

theorem MIPRE.Cost.Data.eqBits_encode (x y : BitStr) : (encode x).eqBits (encode y) = (x == y)

def MIPRE.Cost.Data.canonWalk : Data → Bool → Bool

The walk of the normalization: last records whether the string so far is empty or ends in true.

Equations

• MIPRE.Cost.Data.nil.canonWalk x✝ = x✝
• (MIPRE.Cost.Data.nil.cons r).canonWalk x✝ = r.canonWalk false
• ((MIPRE.Cost.Data.nil.cons MIPRE.Cost.Data.nil).cons r).canonWalk x✝ = r.canonWalk true
• (a.cons a_1).canonWalk x✝ = false

theorem MIPRE.Cost.Data.canonWalk_iff (d : Data) (b : Bool) : d.canonWalk b = true ↔ ∃ (l : BitStr), d = encode l ∧ (l = [] → b = true) ∧ (l ≠ [] → List.getLast? l = some true)

theorem MIPRE.Cost.Data.canonWalk_eq_isCanonBin (d : Data) : d.canonWalk true = d.isCanonBin

The walk computes the normalization test.

def MIPRE.Cost.Prog.tacticCost_omega : Lean.ParserDescr

Close a cost bound after the run has been built: unfold the sizes of the small constants and let omega finish.

Equations

• MIPRE.Cost.Prog.tacticCost_omega = Lean.ParserDescr.node `MIPRE.Cost.Prog.tacticCost_omega 1024 (Lean.ParserDescr.nonReservedSymbol "cost_omega" false)

The bounded bit walk

def MIPRE.Cost.Prog.bitWalkBody : Prog

Body of bitWalkProg, on the state cons l u: stop with cons nil u if l is empty, with cons l nil if the budget is exhausted, with nil if the head of l is not a bit, and otherwise continue with the two tails.

Equations

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

def MIPRE.Cost.Prog.bitWalkProg : Prog

The bounded bit walk: on cons l u, compute bitWalk l u.

Equations

• MIPRE.Cost.Prog.bitWalkProg = MIPRE.Cost.Prog.bitWalkBody.loop

theorem MIPRE.Cost.Prog.bitWalkBody_wellScoped : WellScoped 1 bitWalkBody

theorem MIPRE.Cost.Prog.bitWalkProg_wellScoped : WellScoped 1 bitWalkProg

theorem MIPRE.Cost.Prog.bitWalkBody_lnil (u : Data) : ∃ t ≤ u.size + 20, Eval [Data.nil.cons u] bitWalkBody (Data.nil.cons (Data.nil.cons u)) t

theorem MIPRE.Cost.Prog.bitWalkBody_unil (h l' : Data) : ∃ t ≤ (h.cons l').size + 20, Eval [(h.cons l').cons Data.nil] bitWalkBody (Data.nil.cons ((h.cons l').cons Data.nil)) t

theorem MIPRE.Cost.Prog.bitWalkBody_step (h l' c u' : Data) (hb : h.isBit = true) : ∃ t ≤ l'.size + u'.size + 20, Eval [(h.cons l').cons (c.cons u')] bitWalkBody ((Data.nil.cons Data.nil).cons (l'.cons u')) t

theorem MIPRE.Cost.Prog.bitWalkBody_fail (h l' c u' : Data) (hb : h.isBit = false) : ∃ t ≤ 20, Eval [(h.cons l').cons (c.cons u')] bitWalkBody (Data.nil.cons Data.nil) t

theorem MIPRE.Cost.Prog.bitWalkProg_runs (l u : Data) (env : Env) (S : ℕ) (hS : l.size + u.size ≤ S) : ∃ t ≤ (u.spine + 1) * (S + 21), Eval (l.cons u :: env) bitWalkProg (l.bitWalk u) t

The bounded bit walk computes bitWalk l u, in time (|u| + 1) · (S + 21) for S dominating the sizes of l and u: linear in the input, times the budget.

Equality of bit lists

def MIPRE.Cost.Prog.eqBitsBody : Prog

Body of eqBitsProg, on the state cons l₁ l₂.

Equations

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

def MIPRE.Cost.Prog.eqBitsProg : Prog

Equality of two bit lists: on cons l₁ l₂, compute encode (eqBits l₁ l₂).

Equations

• MIPRE.Cost.Prog.eqBitsProg = MIPRE.Cost.Prog.eqBitsBody.loop

theorem MIPRE.Cost.Prog.eqBitsBody_wellScoped : WellScoped 1 eqBitsBody

theorem MIPRE.Cost.Prog.eqBitsProg_wellScoped : WellScoped 1 eqBitsProg

theorem MIPRE.Cost.Prog.eqBitsBody_nil_nil : ∃ t ≤ 20, Eval [Data.nil.cons Data.nil] eqBitsBody (Data.nil.cons (encode true)) t

theorem MIPRE.Cost.Prog.eqBitsBody_nil_cons (h₂ l₂ : Data) : ∃ t ≤ 20, Eval [Data.nil.cons (h₂.cons l₂)] eqBitsBody (Data.nil.cons (encode false)) t

theorem MIPRE.Cost.Prog.eqBitsBody_cons_nil (h₁ l₁ : Data) : ∃ t ≤ 20, Eval [(h₁.cons l₁).cons Data.nil] eqBitsBody (Data.nil.cons (encode false)) t

theorem MIPRE.Cost.Prog.eqBitsBody_cons_cons (h₁ l₁ h₂ l₂ : Data) : ∃ t ≤ l₁.size + l₂.size + 20, Eval [(h₁.cons l₁).cons (h₂.cons l₂)] eqBitsBody (if h₁.bitOf = h₂.bitOf then (Data.nil.cons Data.nil).cons (l₁.cons l₂) else Data.nil.cons (encode false)) t

theorem MIPRE.Cost.Prog.eqBitsProg_runs (l₁ l₂ : Data) (env : Env) (S : ℕ) (hS : l₁.size + l₂.size ≤ S) : ∃ t ≤ (l₁.spine + 1) * (S + 21), Eval (l₁.cons l₂ :: env) eqBitsProg (encode (l₁.eqBits l₂)) t

eqBitsProg computes eqBits l₁ l₂, in time (|l₁| + 1) · (S + 21) for S dominating the sizes.

Normalization of the parameter

def MIPRE.Cost.Prog.canonBody : Prog

Body of the canonicity walk, on the state cons rest last.

Equations

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

def MIPRE.Cost.Prog.normBinProg : Prog

normBinProg on d computes normBin d: the input itself if it is a canonical binary numeral, nil otherwise.

Equations

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

theorem MIPRE.Cost.Prog.canonBody_wellScoped : WellScoped 1 canonBody

theorem MIPRE.Cost.Prog.normBinProg_wellScoped : WellScoped 1 normBinProg

theorem MIPRE.Cost.Prog.canonBody_nil (last : Data) : ∃ t ≤ last.size + 20, Eval [Data.nil.cons last] canonBody (Data.nil.cons last) t

theorem MIPRE.Cost.Prog.canonBody_step (h r last : Data) : ∃ t ≤ r.size + 20, Eval [(h.cons r).cons last] canonBody (match h with | Data.nil => (Data.nil.cons Data.nil).cons (r.cons Data.nil) | Data.nil.cons Data.nil => (Data.nil.cons Data.nil).cons (r.cons (Data.nil.cons Data.nil)) | x => Data.nil.cons Data.nil) t

theorem MIPRE.Cost.Prog.canonLoop_runs (d : Data) (last : Bool) (env : Env) (S : ℕ) (hS : d.size + 3 ≤ S) : ∃ t ≤ (d.spine + 1) * (S + 21), Eval (d.cons (encode last) :: env) canonBody.loop (encode (d.canonWalk last)) t

The canonicity loop computes canonWalk d last, in time (|d| + 1) · (S + 21).

theorem MIPRE.Cost.Prog.normBinProg_runs (d : Data) : ∃ t ≤ (d.spine + 2) * (d.size + 25) + 3 * d.size + 10, normBinProg.Runs d d.normBin t

normBinProg computes the normalization, in time (|d| + 2) · (|d| + 25) + 3 |d| + 10.