Documentation

Complexitylib.RationalHitting.Internal.BinaryAddition

Rational hitting lists: binary addition #

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

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

source
theorem Complexity.RationalHitting.StackLanguage.wordValue_head_tail (l : List Bool) :
wordValue l = (if l.headD false = true then 1 else 0) + 2 * wordValue l.tail
source
def Complexity.RationalHitting.StackLanguage.addWord :
List Bool → List Bool → List Bool

Grade-school addition, scanning the second operand one bit at a time. The first operand is shifted after adding the incoming low bit.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.RationalHitting.StackLanguage.addWord_value (a b : List Bool) :
    wordValue (addWord a b) = wordValue a + wordValue b
    source
    theorem Complexity.RationalHitting.StackLanguage.incrementWord_tail_length (a : List Bool) :
    (incrementWord a).tail.length ≤ a.length
    source
    theorem Complexity.RationalHitting.StackLanguage.addWord_length (a b : List Bool) :
    (addWord a b).length ≤ a.length + b.length
    source
    def Complexity.RationalHitting.StackLanguage.emitLow {K : Type} (a out : K) :
    Program K

    Emits one least-significant bit, supplying zero for an exhausted operand.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Complexity.RationalHitting.StackLanguage.eval_emitLow {K : Type} [DecidableEq K] {a out : K} (hao : a ≠ out) (s : Store K) :
      Eval (emitLow a out) s (Function.update (Function.update s a (s a).tail) out ((s a).headD false :: s out)) 2
      source
      def Complexity.RationalHitting.StackLanguage.addSplit :
      List Bool → List Bool → List Bool × List Bool

      Output invariant for the single pass: a reversed low part is on out.

      Equations
      Instances For
        source
        theorem Complexity.RationalHitting.StackLanguage.addSplit_spec (a b : List Bool) :
        (addSplit a b).1 ++ (addSplit a b).2 = addWord a b
        source
        theorem Complexity.RationalHitting.StackLanguage.addSplit_first_length (a b : List Bool) :
        (addSplit a b).1.length = b.length
        source
        def Complexity.RationalHitting.StackLanguage.addBody {K : Type} (a b out tmp flag : K) :
        Program K

        Consume one addend bit, propagating its contribution to the accumulator.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.RationalHitting.StackLanguage.addLoop {K : Type} (a b out tmp flag : K) :
          Program K

          Repeat the addition step until the addend stack is empty.

          Equations
          Instances For
            source
            theorem Complexity.RationalHitting.StackLanguage.eval_addLoop {K : Type} [DecidableEq K] {a b out tmp flag : K} (hab : a ≠ b) (hao : a ≠ out) (hat : a ≠ tmp) (haf : a ≠ flag) (hbo : b ≠ out) (hbt : b ≠ tmp) (hbf : b ≠ flag) (hot : out ≠ tmp) (hof : out ≠ flag) (htf : tmp ≠ flag) (s : Store K) (ht : s tmp = []) (hf : s flag = []) :
            ∃ t ≤ (s b).length * (7 * (s a).length + 25) + 1, Eval (addLoop a b out tmp flag) s (Function.update (Function.update (Function.update s a (addSplit (s a) (s b)).2) b []) out ((addSplit (s a) (s b)).1.reverse ++ s out)) t
            source
            def Complexity.RationalHitting.StackLanguage.add {K : Type} (a b out tmp flag : K) :
            Program K

            Destructive binary addition. The second operand and all scratch words are cleared; the first register holds the exact sum.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Complexity.RationalHitting.StackLanguage.eval_add {K : Type} [DecidableEq K] {a b out tmp flag : K} (hab : a ≠ b) (hao : a ≠ out) (hat : a ≠ tmp) (haf : a ≠ flag) (hbo : b ≠ out) (hbt : b ≠ tmp) (hbf : b ≠ flag) (hot : out ≠ tmp) (hof : out ≠ flag) (htf : tmp ≠ flag) (s : Store K) :
              ∃ t ≤ (s b).length * (7 * (s a).length + 27) + 2 * (s out).length + 2 * (s tmp).length + 2 * (s flag).length + 9, Eval (add a b out tmp flag) s (Function.update (Function.update (Function.update (Function.update (Function.update s a (addWord (s a) (s b))) b []) out []) tmp []) flag []) t