OAI/Analysis/MatrixSigning/Machines/BinaryAccumulator.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W03.BinaryAccumulator.nextAccumulator line 12
  2. def OAI.KS.W03.BinaryAccumulator.loop line 15
  3. theorem OAI.KS.W03.BinaryAccumulator.loop_value line 19
  4. def OAI.KS.W03.BinaryAccumulator.width line 27
  5. theorem OAI.KS.W03.BinaryAccumulator.next_width_le line 29
  6. theorem OAI.KS.W03.BinaryAccumulator.loop_length_le line 34
  7. def OAI.KS.W03.BinaryAccumulator.bodyTicks line 45
  8. theorem OAI.KS.W03.BinaryAccumulator.bodyTicks_le line 49
  9. def OAI.KS.W03.BinaryAccumulator.roundTicks line 55
  10. theorem OAI.KS.W03.BinaryAccumulator.roundTicks_le line 58
  11. def OAI.KS.W03.BinaryAccumulator.loopTicks line 64
  12. theorem OAI.KS.W03.BinaryAccumulator.loopTicks_le line 69
  13. theorem OAI.KS.W03.BinaryAccumulator.loop_zero_correct line 87
  14. theorem OAI.KS.W03.BinaryAccumulator.loop_zero_length_le line 91
  15. theorem OAI.KS.W03.BinaryAccumulator.loop_zero_ticks_le line 95
  16. theorem OAI.KS.W03.BinaryAccumulator.loop_trim_eq_multiply line 107