Rational hitting lists: binary division

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/BinaryDivision.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

def Complexity.RationalHitting.StackLanguage.subtractBody : Program (Fin 5)

Subtract the next pair of bits and update the borrow flag.

Equations

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

def Complexity.RationalHitting.StackLanguage.subtractLoop : Program (Fin 5)

Repeat subtraction while the control flag remains set.

Equations

• Complexity.RationalHitting.StackLanguage.subtractLoop = Complexity.RationalHitting.StackLanguage.Program.loop 4 Complexity.RationalHitting.StackLanguage.subtractBody

def Complexity.RationalHitting.StackLanguage.subStep (s : Store (Fin 5)) (c : Bool) : Store (Fin 5)

The register store after one bit-subtraction step.

Equations

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

def Complexity.RationalHitting.StackLanguage.subFinish (s : Store (Fin 5)) (c : Bool) : Store (Fin 5)

The final subtraction store, including output and borrow flag.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.eval_subtractLoop (s : Store (Fin 5)) (c : Bool) (hc : s 3 = [c]) (hf : s 4 = [true]) : ∃ t ≤ 15 * ((s 0).length + (s 1).length) + 7, Eval subtractLoop s (subFinish s c) t

def Complexity.RationalHitting.StackLanguage.subtract : Program (Fin 5)

Subtract and compare, destructively. Output register 2 has the little-endian fixed-width modular difference; singleton register 3 is exactly the comparison bit (true iff the first number was smaller).

Equations

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

theorem Complexity.RationalHitting.StackLanguage.eval_subtract (s : Store (Fin 5)) : ∃ t ≤ 17 * ((s 0).length + (s 1).length) + 2 * (s 2).length + 2 * (s 3).length + 2 * (s 4).length + 19, Eval subtract s (Function.update (Function.update (Function.update (Function.update (Function.update s 0 (subtractWord (s 0) (s 1) false).1) 1 []) 2 []) 3 [(subtractWord (s 0) (s 1) false).2]) 4 []) t

theorem Complexity.RationalHitting.StackLanguage.bitNat_le_one (x : Bool) : bitNat x ≤ 1

def Complexity.RationalHitting.StackLanguage.reduceWord (a b : List Bool) : List Bool × Bool

Subtract when possible, otherwise retain the normalized original word.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.normalize_length_of_lt (a : List Bool) (B : ℕ) (h : wordValue a < 2 ^ B) : (normalizeWord a).length ≤ B

theorem Complexity.RationalHitting.StackLanguage.reduceWord_spec (a b : List Bool) (_hb : 0 < wordValue b) (ha : wordValue a < 2 * wordValue b) : wordValue (reduceWord a b).1 < wordValue b ∧ wordValue (reduceWord a b).1 + bitNat (reduceWord a b).2 * wordValue b = wordValue a ∧ (reduceWord a b).1.length ≤ b.length

def Complexity.RationalHitting.StackLanguage.divideDigits (b : List Bool) : List Bool → List Bool → List Bool → List Bool × List Bool

Long division, scanning the original numerator most-significant-bit first. The quotient and remainder registers remain ordinary little-endian words.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RationalHitting.StackLanguage.divideDigits b [] x✝¹ x✝ = (x✝¹, x✝)

theorem Complexity.RationalHitting.StackLanguage.divideDigits_spec (b l r q : List Bool) (hb : 0 < wordValue b) (hr : wordValue r < wordValue b) : wordValue (divideDigits b l r q).1 < wordValue b ∧ wordValue (divideDigits b l r q).2 * wordValue b + wordValue (divideDigits b l r q).1 = (wordValue q * wordValue b + wordValue r) * 2 ^ l.length + wordValue l.reverse ∧ (divideDigits b l r q).2.length = q.length + l.length ∧ (divideDigits b l r q).1.length ≤ max r.length b.length

theorem Complexity.RationalHitting.StackLanguage.divideDigits_quotient_remainder (a b : List Bool) (hb : 0 < wordValue b) : wordValue (divideDigits b a.reverse [] []).1 = wordValue a % wordValue b ∧ wordValue (divideDigits b a.reverse [] []).2 = wordValue a / wordValue b

def Complexity.RationalHitting.StackLanguage.Program.rename {K L : Type} (f : K → L) : Program K → Program L

Rename every register occurring in a finite stack program.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RationalHitting.StackLanguage.Program.rename f Complexity.RationalHitting.StackLanguage.Program.skip = Complexity.RationalHitting.StackLanguage.Program.skip
• Complexity.RationalHitting.StackLanguage.Program.rename f (Complexity.RationalHitting.StackLanguage.Program.push k b) = Complexity.RationalHitting.StackLanguage.Program.push (f k) b
• Complexity.RationalHitting.StackLanguage.Program.rename f (Complexity.RationalHitting.StackLanguage.Program.drop k) = Complexity.RationalHitting.StackLanguage.Program.drop (f k)
• Complexity.RationalHitting.StackLanguage.Program.rename f (Complexity.RationalHitting.StackLanguage.Program.transfer a b) = Complexity.RationalHitting.StackLanguage.Program.transfer (f a) (f b)

theorem Complexity.RationalHitting.StackLanguage.extend_update_store {K L : Type} [DecidableEq K] [DecidableEq L] (f : K → L) (hf : Function.Injective f) (s : Store K) (S : Store L) (k : K) (w : List Bool) : Function.extend f (Function.update s k w) S = Function.update (Function.extend f s S) (f k) w

theorem Complexity.RationalHitting.StackLanguage.extend_transfer_store {K L : Type} [DecidableEq K] [DecidableEq L] (f : K → L) (hf : Function.Injective f) (s : Store K) (S : Store L) (a b : K) : Function.extend f (transfer a b s) S = transfer (f a) (f b) (Function.extend f s S)

theorem Complexity.RationalHitting.StackLanguage.Eval.rename {K L : Type} [DecidableEq K] [DecidableEq L] {p : Program K} {s v : Store K} {t : ℕ} (h : Eval p s v t) (f : K → L) (hf : Function.Injective f) (S : Store L) : Eval (Program.rename f p) (Function.extend f s S) (Function.extend f v S) t

Uniform register allocation: renaming injectively never changes time and preserves every register outside its finite image.

theorem Complexity.RationalHitting.StackLanguage.extend_pull_store {K L : Type} (f : K → L) (hf : Function.Injective f) (S : Store L) : Function.extend f (fun (k : K) => S (f k)) S = S

theorem Complexity.RationalHitting.StackLanguage.eval_rename_from {K L : Type} [DecidableEq K] [DecidableEq L] (f : K → L) (hf : Function.Injective f) (S : Store L) {p : Program K} {v : Store K} {t : ℕ} (h : Eval p (fun (k : K) => S (f k)) v t) : Eval (Program.rename f p) S (Function.extend f v S) t