OAI/Computability/RationalHitting/BinarySubtract.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalHitting.StackLanguage.mulAccWord line 9

    Source documentation

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

    def mulAccWord : List Bool → List Bool → List Bool → List Bool
  | _a, [], c => c
  | a, false::b, c => mulAccWord (false::a) b c
  | a, true::b, c => mulAccWord (false::a) b (addWord c a)

    Mentions: OAI.RationalHitting.StackLanguage.addWord

  2. theorem OAI.RationalHitting.StackLanguage.mulAccWord_value line 14
  3. lemma OAI.RationalHitting.StackLanguage.mulAccWord_length line 20
  4. def OAI.RationalHitting.StackLanguage.mulBody line 38

    Source documentation

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

    def mulBody : Program (Fin 8) := .branch 1 .skip
…

    Mentions: OAI.RationalHitting.StackLanguage.Program

  5. def OAI.RationalHitting.StackLanguage.mulLoop line 42
  6. lemma OAI.RationalHitting.StackLanguage.eval_mulLoop line 44
  7. def OAI.RationalHitting.StackLanguage.multiply line 134

    Source documentation

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

    def multiply : Program (Fin 8) := .seq mulLoop (normalize 2 5 6)

    Mentions: OAI.RationalHitting.StackLanguage.Program, OAI.RationalHitting.StackLanguage.mulLoop, OAI.RationalHitting.StackLanguage.normalize

  8. lemma OAI.RationalHitting.StackLanguage.eval_multiply line 136
  9. lemma OAI.RationalHitting.StackLanguage.wordValue_lt line 164
  10. lemma OAI.RationalHitting.StackLanguage.product_bits_length line 169
  11. def OAI.RationalHitting.StackLanguage.differenceBit line 180

    Source documentation

    Boolean full-subtractor gate.

    def differenceBit (x y c : Bool) : Bool := (x ^^ y) ^^ c
  12. def OAI.RationalHitting.StackLanguage.borrowBit line 181
  13. def OAI.RationalHitting.StackLanguage.bitNat line 182
  14. lemma OAI.RationalHitting.StackLanguage.bitNat_false line 183
  15. lemma OAI.RationalHitting.StackLanguage.wordValue_bit line 184
  16. lemma OAI.RationalHitting.StackLanguage.wordValue_nil line 185
  17. lemma OAI.RationalHitting.StackLanguage.digit_subtract line 187
  18. def OAI.RationalHitting.StackLanguage.subtractWord line 194

    Source documentation

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

    def subtractWord : List Bool → List Bool → Bool → List Bool × Bool
  | [],[],c => ([],c)
  | x::a,b,c =>
    let u := subtractWord a b.tail (borrowBit x (b.headD false) c)
…

    Mentions: OAI.RationalHitting.StackLanguage.borrowBit

  19. lemma OAI.RationalHitting.StackLanguage.subtractWord_length line 203
  20. lemma OAI.RationalHitting.StackLanguage.subtractWord_value line 211
  21. lemma OAI.RationalHitting.StackLanguage.subtractWord_borrow line 229
  22. lemma OAI.RationalHitting.StackLanguage.subtractWord_nonnegative line 238
  23. def OAI.RationalHitting.StackLanguage.readBit line 251
  24. lemma OAI.RationalHitting.StackLanguage.eval_readBit line 252
  25. def OAI.RationalHitting.StackLanguage.subtractDigit line 262

    Source documentation

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

    def subtractDigit : Program (Fin 5) :=
…

    Mentions: OAI.RationalHitting.StackLanguage.Program

  26. lemma OAI.RationalHitting.StackLanguage.eval_subtractDigit line 267