OAI/Computability/DeterministicSum/WordArithmetic.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Signed word encoding, no-wrap bounds and modular arithmetic commands.

  1. lemma OAI.DeterministicThreeSum.wordModulus_pos line 10
  2. lemma OAI.DeterministicThreeSum.encodeWord_lt line 12
  3. lemma OAI.DeterministicThreeSum.encodeWord_add line 19
  4. lemma OAI.DeterministicThreeSum.encodeWord_eq_zero_iff line 29
  5. lemma OAI.DeterministicThreeSum.wordWidth_lower line 44
  6. lemma OAI.DeterministicThreeSum.cubic_sum_no_wrap line 57
  7. lemma OAI.DeterministicThreeSum.polynomial_sum_no_wrap line 67
  8. def OAI.DeterministicThreeSum.Structured.straight line 88
  9. def OAI.DeterministicThreeSum.Structured.execStraight line 92
  10. lemma OAI.DeterministicThreeSum.Structured.straight_correct line 96
  11. lemma OAI.DeterministicThreeSum.Structured.straight_writes line 104
  12. lemma OAI.DeterministicThreeSum.Structured.eval_add line 109
  13. lemma OAI.DeterministicThreeSum.Structured.eval_remainder line 116
  14. lemma OAI.DeterministicThreeSum.Structured.eval_indirect_load line 122
  15. lemma OAI.DeterministicThreeSum.Structured.eval_indirect_store line 128
  16. def OAI.DeterministicThreeSum.Structured.Modular.add line 138
  17. def OAI.DeterministicThreeSum.Structured.Modular.mul line 140
  18. def OAI.DeterministicThreeSum.Structured.Modular.sub line 142
  19. lemma OAI.DeterministicThreeSum.Structured.Modular.add_correct line 146
  20. lemma OAI.DeterministicThreeSum.Structured.Modular.mul_correct line 157
  21. lemma OAI.DeterministicThreeSum.Structured.Modular.sub_correct line 169
  22. lemma OAI.DeterministicThreeSum.Structured.Modular.cast_add line 183
  23. lemma OAI.DeterministicThreeSum.Structured.Modular.cast_mul line 185
  24. lemma OAI.DeterministicThreeSum.Structured.Modular.cast_sub line 187
  25. def OAI.DeterministicThreeSum.Structured.Modular.mac line 192
  26. lemma OAI.DeterministicThreeSum.Structured.Modular.mac_correct line 195