OAI/Analysis/MatrixSigning/Arithmetic/SignedRationalSerializer.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KS.W01.SignedRationalSerializer.Registers line 15
  2. def OAI.KS.W01.SignedRationalSerializer.inputState line 17
  3. def OAI.KS.W01.SignedRationalSerializer.selectedState line 19
  4. def OAI.KS.W01.SignedRationalSerializer.oneState line 21
  5. def OAI.KS.W01.SignedRationalSerializer.decrementedState line 23
  6. def OAI.KS.W01.SignedRationalSerializer.reverseState line 25
  7. def OAI.KS.W01.SignedRationalSerializer.outputState line 27
  8. def OAI.KS.W01.SignedRationalSerializer.signedWire line 30
  9. def OAI.KS.W01.SignedRationalSerializer.rawWire line 32
  10. theorem OAI.KS.W01.SignedRationalSerializer.signedWire_length line 35
  11. def OAI.KS.W01.SignedRationalSerializer.positivePorts line 40
  12. def OAI.KS.W01.SignedRationalSerializer.negativePorts line 41
  13. def OAI.KS.W01.SignedRationalSerializer.subtractPorts line 42
  14. def OAI.KS.W01.SignedRationalSerializer.reversePorts line 43
  15. def OAI.KS.W01.SignedRationalSerializer.pushDispatch line 45
  16. def OAI.KS.W01.SignedRationalSerializer.pushOne line 47
  17. def OAI.KS.W01.SignedRationalSerializer.positiveBranch line 48
  18. def OAI.KS.W01.SignedRationalSerializer.negativeBranch line 49
  19. def OAI.KS.W01.SignedRationalSerializer.selector line 53
  20. def OAI.KS.W01.SignedRationalSerializer.program line 57
  21. theorem OAI.KS.W01.SignedRationalSerializer.stackCount line 59
  22. theorem OAI.KS.W01.SignedRationalSerializer.inputPort line 60
  23. theorem OAI.KS.W01.SignedRationalSerializer.outputPort line 61
  24. theorem OAI.KS.W01.SignedRationalSerializer.branch_table_length line 63
  25. theorem OAI.KS.W01.SignedRationalSerializer.table_length line 71
  26. theorem OAI.KS.W01.SignedRationalSerializer.selector_false line 75
  27. theorem OAI.KS.W01.SignedRationalSerializer.selector_true line 87
  28. theorem OAI.KS.W01.SignedRationalSerializer.pushOne_spec line 99
  29. theorem OAI.KS.W01.SignedRationalSerializer.positive_emit_spec line 117
  30. theorem OAI.KS.W01.SignedRationalSerializer.subtract_spec line 130
  31. theorem OAI.KS.W01.SignedRationalSerializer.negative_emit_spec line 144
  32. theorem OAI.KS.W01.SignedRationalSerializer.finish_spec line 160
  33. theorem OAI.KS.W01.SignedRationalSerializer.positive_spec line 171
  34. theorem OAI.KS.W01.SignedRationalSerializer.negative_spec line 179
  35. theorem OAI.KS.W01.SignedRationalSerializer.program_spec line 193
  36. theorem OAI.KS.W01.SignedRationalSerializer.rawWire_canonical line 221
  37. theorem OAI.KS.W01.SignedRationalSerializer.serializes_rational line 229