OAI/Analysis/MatrixSigning/Realization/RawRationalMachine.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.RawRationalMachine.state line 14
  2. def OAI.CurrentKS.RawRationalMachine.corePorts line 17
  3. def OAI.CurrentKS.RawRationalMachine.numPorts line 18
  4. def OAI.CurrentKS.RawRationalMachine.denPorts line 19
  5. def OAI.CurrentKS.RawRationalMachine.magnitudePorts line 20
  6. def OAI.CurrentKS.RawRationalMachine.readSign line 22
  7. def OAI.CurrentKS.RawRationalMachine.readNumerator line 23
  8. def OAI.CurrentKS.RawRationalMachine.readDenominator line 24
  9. def OAI.CurrentKS.RawRationalMachine.parse line 25
  10. def OAI.CurrentKS.RawRationalMachine.magnitude line 26
  11. def OAI.CurrentKS.RawRationalMachine.trim line 27
  12. def OAI.CurrentKS.RawRationalMachine.normalize line 28
  13. def OAI.CurrentKS.RawRationalMachine.serialize line 29
  14. def OAI.CurrentKS.RawRationalMachine.program line 30
  15. lemma OAI.CurrentKS.RawRationalMachine.entry_wire line 32
  16. lemma OAI.CurrentKS.RawRationalMachine.readSign_spec line 39
  17. lemma OAI.CurrentKS.RawRationalMachine.readNumerator_spec line 47
  18. lemma OAI.CurrentKS.RawRationalMachine.readDenominator_spec line 54
  19. lemma OAI.CurrentKS.RawRationalMachine.parse_spec line 61
  20. lemma OAI.CurrentKS.RawRationalMachine.magnitude_spec line 87
  21. lemma OAI.CurrentKS.RawRationalMachine.trim_spec line 96
  22. lemma OAI.CurrentKS.RawRationalMachine.magnitude_value line 104
  23. def OAI.CurrentKS.RawRationalMachine.magnitudeRecord line 110
  24. lemma OAI.CurrentKS.RawRationalMachine.magnitudeRecord_value line 114
  25. lemma OAI.CurrentKS.RawRationalMachine.state_core line 121
  26. lemma OAI.CurrentKS.RawRationalMachine.state_remaining line 125
  27. lemma OAI.CurrentKS.RawRationalMachine.normalize_spec line 134
  28. lemma OAI.CurrentKS.RawRationalMachine.serialize_spec line 153
  29. def OAI.CurrentKS.RawRationalMachine.ticks line 174
  30. theorem OAI.CurrentKS.RawRationalMachine.program_spec line 182