OAI/Computability/RationalHitting/SignedBinary.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

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

    Source documentation

    Replace the front variable-width record, consuming the replacement in 5.

    def replaceRecord : Program (Fin 8) :=
…

    Mentions: OAI.RationalHitting.StackLanguage.Program

  2. lemma OAI.RationalHitting.StackLanguage.eval_replaceRecord line 13
  3. def OAI.RationalHitting.StackLanguage.arrayWrite line 44

    Source documentation

    Indexed overwrite with no fixed cell width or numerical oracle.

    def arrayWrite : Program (Fin 8) := .seq scan (.seq replaceRecord restore)

    Mentions: OAI.RationalHitting.StackLanguage.Program, OAI.RationalHitting.StackLanguage.scan, OAI.RationalHitting.StackLanguage.replaceRecord, OAI.RationalHitting.StackLanguage.restore

  4. theorem OAI.RationalHitting.StackLanguage.eval_arrayWrite line 46
  5. def OAI.RationalHitting.StackLanguage.powerBody line 81

    Source documentation

    Repeated multiplication, preserving the binary base in register 8 and consuming a unary exponent in register 9. Used in the Taylor input matrices.

    def powerBody : Program (Fin 10) :=
…

    Mentions: OAI.RationalHitting.StackLanguage.Program

  6. def OAI.RationalHitting.StackLanguage.powerLoop line 84
  7. lemma OAI.RationalHitting.StackLanguage.eval_powerBody line 86
  8. lemma OAI.RationalHitting.StackLanguage.eval_powerLoop line 109
  9. def OAI.RationalHitting.StackLanguage.powerCore line 143
  10. theorem OAI.RationalHitting.StackLanguage.eval_powerCore line 147

    Source documentation

    A fixed finite power subroutine. Its exponent is unary and its output is canonical binary. No exponentiation instruction is supplied by the machine.

    theorem eval_powerCore (s : Store (Fin 10)) (hf : factorialScratch s) (h0 : s 0=[])
    (n : ℕ) (hn : (s 9).length=n) :
    ∃ t≤n*(250*(2+(n+1)*(s 8).length)^4+1)+3,
      Eval powerCore s (update (update s 0 (wordValue (s 8)^n).bits) 9 []) t := by
…

    Mentions: OAI.RationalHitting.StackLanguage.Store, OAI.RationalHitting.StackLanguage.factorialScratch, OAI.RationalHitting.StackLanguage.Eval, OAI.RationalHitting.StackLanguage.powerCore, OAI.RationalHitting.StackLanguage.wordValue

  11. lemma OAI.RationalHitting.StackLanguage.wordValue_complement line 173
  12. def OAI.RationalHitting.StackLanguage.flipReverse line 179
  13. lemma OAI.RationalHitting.StackLanguage.eval_flipReverse line 182
  14. def OAI.RationalHitting.StackLanguage.flipWord line 209
  15. lemma OAI.RationalHitting.StackLanguage.eval_flipWord line 211
  16. def OAI.RationalHitting.StackLanguage.absoluteWord line 223
  17. lemma OAI.RationalHitting.StackLanguage.absoluteWord_length line 227
  18. lemma OAI.RationalHitting.StackLanguage.absoluteWord_value line 234
  19. def OAI.RationalHitting.StackLanguage.absolutize line 250

    Source documentation

    Convert the modular subtraction result to an absolute magnitude according to its genuinely computed borrow bit.

    def absolutize : Program (Fin 5) :=
…

    Mentions: OAI.RationalHitting.StackLanguage.Program

  20. lemma OAI.RationalHitting.StackLanguage.eval_absolutize line 253
  21. def OAI.RationalHitting.StackLanguage.signedDifference line 291

    Source documentation

    Signed difference of arbitrary naturals, in canonical signed magnitude.

    def signedDifference : Program (Fin 5) := .seq subtract absolutize

    Mentions: OAI.RationalHitting.StackLanguage.Program, OAI.RationalHitting.StackLanguage.subtract, OAI.RationalHitting.StackLanguage.absolutize

  22. lemma OAI.RationalHitting.StackLanguage.eval_signedDifference line 293