OAI/Analysis/MatrixSigning/Encoding/FrameDecoder.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W29.FrameDecoder.config line 12
  2. def OAI.KS.W29.FrameDecoder.tagEntry line 15
  3. def OAI.KS.W29.FrameDecoder.dataEntry line 20
  4. def OAI.KS.W29.FrameDecoder.reverseEntry line 24
  5. def OAI.KS.W29.FrameDecoder.dispatch line 28
  6. def OAI.KS.W29.FrameDecoder.machine line 33
  7. theorem OAI.KS.W29.FrameDecoder.first_head line 35
  8. theorem OAI.KS.W29.FrameDecoder.third_head line 40
  9. theorem OAI.KS.W29.FrameDecoder.tag_false_step line 46
  10. theorem OAI.KS.W29.FrameDecoder.tag_true_step line 58
  11. theorem OAI.KS.W29.FrameDecoder.data_step line 70
  12. theorem OAI.KS.W29.FrameDecoder.reverse_step line 83
  13. theorem OAI.KS.W29.FrameDecoder.reverse_done line 96
  14. theorem OAI.KS.W29.FrameDecoder.run_read line 107
  15. theorem OAI.KS.W29.FrameDecoder.run_reverse line 137
  16. theorem OAI.KS.W29.FrameDecoder.run_frame line 161
  17. theorem OAI.KS.W29.FrameDecoder.haltsWithin line 183
  18. theorem OAI.KS.W29.FrameDecoder.output_eq line 190
  19. theorem OAI.KS.W29.FrameDecoder.preserved_suffix line 196
  20. theorem OAI.KS.W29.FrameDecoder.run_frame_of_length_ge line 202
  21. theorem OAI.KS.W29.FrameDecoder.haltsWithin_polynomialFuel line 213