Equality and binary-indexed array access as ambient programs

Formula variables and circuit wires are binary indices. Looking them up must not first expand the index to unary: a malformed index can be exponentially larger than its encoding. The programs here scan the supplied array and compare binary indices, so their bounds apply to malformed inputs as well.

def MIPRE.SAT.ArrayProg.eqStep (s : Cost.BitStr × Bool) (b : Bool) : Cost.BitStr × Bool

Equations

• MIPRE.SAT.ArrayProg.eqStep s b = match s.1 with | [] => ([], false) | a :: as => (as, s.2 && a == b)

def MIPRE.SAT.ArrayProg.finishEq (s : Cost.BitStr × Bool) : Bool

Equations

• MIPRE.SAT.ArrayProg.finishEq s = (s.2 && List.isEmpty s.1)

theorem MIPRE.SAT.ArrayProg.esize_bool_le (b : Bool) : Cost.esize b ≤ 3

theorem MIPRE.SAT.ArrayProg.fold_eqStep (a b : Cost.BitStr) (ok : Bool) : finishEq (List.foldl eqStep (a, ok) b) = (ok && decide (a = b))

noncomputable def MIPRE.SAT.ArrayProg.eqStepP : Cost.PolyTimeFun ((Cost.BitStr × Bool) × Bool) (Cost.BitStr × Bool)

Equations

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

theorem MIPRE.SAT.ArrayProg.fold_eqStep_size (bs a : Cost.BitStr) (ok : Bool) : Cost.esize (List.foldl eqStep (a, ok) bs) ≤ Cost.esize a + 4

noncomputable def MIPRE.SAT.ArrayProg.eqBits : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) Bool

Exact equality of bit strings, including their lengths.

Equations

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

@[simp]

theorem MIPRE.SAT.ArrayProg.eqBits_apply (p : Cost.BitStr × Cost.BitStr) : eqBits.toFun p = decide (p.1 = p.2)

noncomputable def MIPRE.SAT.ArrayProg.eqNat : Cost.PolyTimeFun (ℕ × ℕ) Bool

Equality of binary natural numbers, without unary expansion.

Equations

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

@[simp]

theorem MIPRE.SAT.ArrayProg.eqNat_apply (p : ℕ × ℕ) : eqNat.toFun p = decide (p.1 = p.2)

def MIPRE.SAT.ArrayProg.lookupStep {α : Type u_1} (s a : ℕ × α) : ℕ × α

Equations

• MIPRE.SAT.ArrayProg.lookupStep s a = (s.1, if a.1 = s.1 then a.2 else s.2)

noncomputable def MIPRE.SAT.ArrayProg.lookupStepP {α : Type u_1} [Cost.SizedEncoding α] : Cost.PolyTimeFun ((ℕ × α) × ℕ × α) (ℕ × α)

Equations

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

theorem MIPRE.SAT.ArrayProg.fold_lookupStep {α : Type u_1} (l : List (ℕ × α)) (k : ℕ) (d : α) : List.foldl lookupStep (k, d) l.reverse = (k, List.foldr (fun (a : ℕ × α) (acc : α) => if a.1 = k then a.2 else acc) d l)

theorem MIPRE.SAT.ArrayProg.indexed_lookup {α : Type u_1} (l : List α) (base t : ℕ) (d : α) : List.foldr (fun (a : ℕ × α) (acc : α) => if a.1 = base + t then a.2 else acc) d ((List.range' base l.length).zip l) = l.getD t d

noncomputable def MIPRE.SAT.ArrayProg.getD {α : Type u_1} [Cost.SizedEncoding α] (d : α) : Cost.PolyTimeFun (ℕ × List α) α

Read a binary-indexed array, returning the fixed default outside its bounds. The scan is bounded by the array length, independently of the magnitude of the index.

Equations

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

@[simp]

theorem MIPRE.SAT.ArrayProg.getD_apply {α : Type u_1} [Cost.SizedEncoding α] (d : α) (p : ℕ × List α) : (getD d).toFun p = p.2.getD p.1 d