OAI/Analysis/MatrixSigning/Encoding/BinaryEncoding.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W01.frame line 9
  2. def OAI.KS.W01.unframe line 13
  3. theorem OAI.KS.W01.unframe_frame_append line 19
  4. theorem OAI.KS.W01.length_frame line 25
  5. def OAI.KS.W01.encodeNat line 31
  6. def OAI.KS.W01.readNat line 33
  7. theorem OAI.KS.W01.readNat_encode_append line 36
  8. def OAI.KS.W01.encodeInt line 40
  9. def OAI.KS.W01.readInt line 44
  10. theorem OAI.KS.W01.readInt_encode_append line 49
  11. def OAI.KS.W01.encodeRat line 53
  12. def OAI.KS.W01.readRat line 55
  13. theorem OAI.KS.W01.readRat_encode_append line 60
  14. abbrev OAI.KS.W01.RationalComplex line 64
  15. def OAI.KS.W01.encodeComplex line 66
  16. def OAI.KS.W01.readComplex line 68
  17. theorem OAI.KS.W01.readComplex_encode_append line 73
  18. def OAI.KS.W01.decodeComplex line 77
  19. theorem OAI.KS.W01.decodeComplex_encode line 81
  20. theorem OAI.KS.W01.encodeComplex_injective line 87
  21. def OAI.KS.W01.natPayloadLength line 92
  22. def OAI.KS.W01.intPayload line 94
  23. theorem OAI.KS.W01.length_encodeNat line 98
  24. theorem OAI.KS.W01.length_encodeInt line 102
  25. theorem OAI.KS.W01.length_encodeRat line 106
  26. theorem OAI.KS.W01.length_encodeComplex line 112
  27. theorem OAI.KS.W01.length_encodePosNum line 116
  28. theorem OAI.KS.W01.length_encodeNum line 120
  29. theorem OAI.KS.W01.natPayloadLength_eq_size line 126
  30. theorem OAI.KS.W01.natPayloadLength_le_iff line 130