OAI/Analysis/MatrixSigning/Encoding/PositiveWireSerializer.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W28.PositiveWireSerializer.dispatch line 12
  2. def OAI.KS.W28.PositiveWireSerializer.machine line 23
  3. def OAI.KS.W28.PositiveWireSerializer.cfg line 25
  4. def OAI.KS.W28.PositiveWireSerializer.wire line 28
  5. theorem OAI.KS.W28.PositiveWireSerializer.table_length line 30
  6. theorem OAI.KS.W28.PositiveWireSerializer.head_left line 33
  7. theorem OAI.KS.W28.PositiveWireSerializer.head_right line 38
  8. theorem OAI.KS.W28.PositiveWireSerializer.step_start line 44
  9. theorem OAI.KS.W28.PositiveWireSerializer.step_num_prefix line 53
  10. theorem OAI.KS.W28.PositiveWireSerializer.step_num_digit line 65
  11. theorem OAI.KS.W28.PositiveWireSerializer.step_num_done line 77
  12. theorem OAI.KS.W28.PositiveWireSerializer.step_den_prefix line 87
  13. theorem OAI.KS.W28.PositiveWireSerializer.step_den_digit line 99
  14. theorem OAI.KS.W28.PositiveWireSerializer.step_den_done line 110
  15. theorem OAI.KS.W28.PositiveWireSerializer.run_den line 120
  16. theorem OAI.KS.W28.PositiveWireSerializer.run_num line 149
  17. theorem OAI.KS.W28.PositiveWireSerializer.run_wire line 178
  18. theorem OAI.KS.W28.PositiveWireSerializer.wire_length line 192