Rational hitting lists: binary subtract

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/BinarySubtract.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.mulAccWord : List Bool → List Bool → List Bool → List Bool

Shift-and-add on explicit little-endian words.

Equations

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

@[simp]

theorem Complexity.RationalHitting.StackLanguage.mulAccWord_value (a b c : List Bool) : wordValue (mulAccWord a b c) = wordValue c + wordValue a * wordValue b

theorem Complexity.RationalHitting.StackLanguage.mulAccWord_length (a b c : List Bool) : (mulAccWord a b c).length ≤ c.length + b.length * (a.length + b.length)

def Complexity.RationalHitting.StackLanguage.mulBody : Program (Fin 8)

Registers: 0 multiplicand, 1 multiplier, 2 accumulator, 3 copied addend, 4/5/6 addition scratch, 7 copy scratch.

Equations

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

def Complexity.RationalHitting.StackLanguage.mulLoop : Program (Fin 8)

Repeat the multiplication body over the multiplier bits.

Equations

• Complexity.RationalHitting.StackLanguage.mulLoop = Complexity.RationalHitting.StackLanguage.Program.loop 1 Complexity.RationalHitting.StackLanguage.mulBody

theorem Complexity.RationalHitting.StackLanguage.eval_mulLoop (s : Store (Fin 8)) (hf : ∀ (k : Fin 8), 3 ≤ ↑k → s k = []) (A C : ℕ) (hA : (s 0).length + (s 1).length ≤ A) (hC : (s 2).length + (s 1).length * ((s 0).length + (s 1).length) ≤ C) : ∃ t ≤ (s 1).length * (A * (7 * C + 34) + 23) + 1, Eval mulLoop s (Function.update (Function.update (Function.update s 0 (List.replicate (s 1).length false ++ s 0)) 1 []) 2 (mulAccWord (s 0) (s 1) (s 2))) t

def Complexity.RationalHitting.StackLanguage.multiply : Program (Fin 8)

The normalized multiplication instruction; the accumulator starts at zero. After execution register 2 is the canonical binary product.

Equations

• Complexity.RationalHitting.StackLanguage.multiply = Complexity.RationalHitting.StackLanguage.mulLoop.seq (Complexity.RationalHitting.StackLanguage.normalize 2 5 6)

theorem Complexity.RationalHitting.StackLanguage.eval_multiply (s : Store (Fin 8)) (hzero : s 2 = []) (hf : ∀ (k : Fin 8), 3 ≤ ↑k → s k = []) : have A := (s 0).length + (s 1).length; have C := (s 1).length * A; ∃ t ≤ (s 1).length * (A * (7 * C + 34) + 23) + 7 * C + 18, Eval multiply s (Function.update (Function.update (Function.update s 0 (List.replicate (s 1).length false ++ s 0)) 1 []) 2 (wordValue (s 0) * wordValue (s 1)).bits) t

theorem Complexity.RationalHitting.StackLanguage.wordValue_lt (l : List Bool) : wordValue l < 2 ^ l.length

theorem Complexity.RationalHitting.StackLanguage.product_bits_length (a b : List Bool) : (wordValue a * wordValue b).bits.length ≤ a.length + b.length

def Complexity.RationalHitting.StackLanguage.differenceBit (x y c : Bool) : Bool

Boolean full-subtractor gate.

Equations

• Complexity.RationalHitting.StackLanguage.differenceBit x y c = (x ^^ y ^^ c)

def Complexity.RationalHitting.StackLanguage.borrowBit (x y c : Bool) : Bool

The outgoing borrow bit for one full subtractor.

Equations

• Complexity.RationalHitting.StackLanguage.borrowBit x y c = (!x && (y || c) || y && c)

def Complexity.RationalHitting.StackLanguage.bitNat (x : Bool) : ℕ

Interpret a Boolean bit as zero or one.

Equations

• Complexity.RationalHitting.StackLanguage.bitNat x = if x = true then 1 else 0

@[simp]

theorem Complexity.RationalHitting.StackLanguage.bitNat_false : bitNat false = 0

theorem Complexity.RationalHitting.StackLanguage.wordValue_bit (x : Bool) (a : List Bool) : wordValue (x :: a) = bitNat x + 2 * wordValue a

@[simp]

theorem Complexity.RationalHitting.StackLanguage.wordValue_nil : wordValue [] = 0

theorem Complexity.RationalHitting.StackLanguage.digit_subtract (x y c : Bool) : bitNat x + 2 * bitNat (borrowBit x y c) = bitNat (differenceBit x y c) + bitNat y + bitNat c

@[irreducible]

def Complexity.RationalHitting.StackLanguage.subtractWord : List Bool → List Bool → Bool → List Bool × Bool

Fixed-width subtraction, returning the overflow borrow. Registers may have leading zeros. Width is exactly the larger input word length.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.subtractWord_length (a b : List Bool) (c : Bool) : (subtractWord a b c).1.length = max a.length b.length

theorem Complexity.RationalHitting.StackLanguage.subtractWord_value (a b : List Bool) (c : Bool) : wordValue a + 2 ^ max a.length b.length * bitNat (subtractWord a b c).2 = wordValue (subtractWord a b c).1 + wordValue b + bitNat c

theorem Complexity.RationalHitting.StackLanguage.subtractWord_borrow (a b : List Bool) : (subtractWord a b false).2 = true ↔ wordValue a < wordValue b

theorem Complexity.RationalHitting.StackLanguage.subtractWord_nonnegative {a b : List Bool} (h : wordValue b ≤ wordValue a) : (subtractWord a b false).2 = false ∧ wordValue (subtractWord a b false).1 = wordValue a - wordValue b

def Complexity.RationalHitting.StackLanguage.readBit {K : Type} (k : K) (f : Bool → Program K) : Program K

Branch on the head bit, treating an empty stack as false.

Equations

• Complexity.RationalHitting.StackLanguage.readBit k f = Complexity.RationalHitting.StackLanguage.Program.branch k (f false) (f false) (f true)

theorem Complexity.RationalHitting.StackLanguage.eval_readBit {K : Type} [DecidableEq K] (k : K) (f : Bool → Program K) (s v : Store K) (t : ℕ) (h : Eval (f ((s k).headD false)) s v t) : Eval (readBit k f) s v (1 + t)

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

Registers 0,1 input, 2 reverse output, 3 singleton borrow, 4 loop flag.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.eval_subtractDigit (s : Store (Fin 5)) (c : Bool) (hc : s 3 = [c]) : Eval subtractDigit s (Function.update (Function.update (Function.update (Function.update s 0 (s 0).tail) 1 (s 1).tail) 3 [borrowBit ((s 0).headD false) ((s 1).headD false) c]) 2 (differenceBit ((s 0).headD false) ((s 1).headD false) c :: s 2)) 12