OAI/Analysis/MatrixSigning/Arithmetic/BinaryAdder.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W01.BinaryAdder.sumBit line 11
  2. def OAI.KS.W01.BinaryAdder.carryBit line 13
  3. theorem OAI.KS.W01.BinaryAdder.fullAdder_identity line 15
  4. def OAI.KS.W01.BinaryAdder.carryState line 19
  5. def OAI.KS.W01.BinaryAdder.finishEntry line 21
  6. def OAI.KS.W01.BinaryAdder.addEntry line 24
  7. def OAI.KS.W01.BinaryAdder.dispatch line 27
  8. def OAI.KS.W01.BinaryAdder.machine line 34
  9. def OAI.KS.W01.BinaryAdder.cfg line 36
  10. theorem OAI.KS.W01.BinaryAdder.table_lookup line 39
  11. theorem OAI.KS.W01.BinaryAdder.step_left_cons line 55
  12. theorem OAI.KS.W01.BinaryAdder.step_right_cons line 74
  13. theorem OAI.KS.W01.BinaryAdder.step_done line 86
  14. def OAI.KS.W01.BinaryAdder.addBits line 97
  15. theorem OAI.KS.W01.BinaryAdder.addBits_correct line 107
  16. theorem OAI.KS.W01.BinaryAdder.addBits_length_le line 136
  17. theorem OAI.KS.W01.BinaryAdder.run_add line 161
  18. theorem OAI.KS.W01.BinaryAdder.run_correct line 213
  19. theorem OAI.KS.W01.BinaryAdder.run_encodedNat_correct line 226
  20. theorem OAI.KS.W01.BinaryAdder.transition_bound line 239
  21. theorem OAI.KS.W01.BinaryAdder.table_length line 242