OAI/Analysis/MatrixSigning/Encoding/FramedArrayReplacement.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W11.FramedArrayRewrite.skipPorts line 14
  2. def OAI.KS.W11.FramedArrayRewrite.skipProgram line 20
  3. def OAI.KS.W11.FramedArrayRewrite.reverseNew line 23
  4. def OAI.KS.W11.FramedArrayRewrite.insertNew line 24
  5. def OAI.KS.W11.FramedArrayRewrite.restorePrefix line 25
  6. def OAI.KS.W11.FramedArrayRewrite.insertAndRestore line 26
  7. def OAI.KS.W11.FramedArrayRewrite.finishProgram line 27
  8. def OAI.KS.W11.FramedArrayRewrite.replaceTailProgram line 28
  9. def OAI.KS.W11.FramedArrayRewrite.program line 30
  10. theorem OAI.KS.W11.FramedArrayRewrite.program_states line 32
  11. theorem OAI.KS.W11.FramedArrayRewrite.program_input line 33
  12. theorem OAI.KS.W11.FramedArrayRewrite.program_output line 34
  13. theorem OAI.KS.W11.FramedArrayRewrite.program_table_length line 36
  14. theorem OAI.KS.W11.FramedArrayRewrite.run_prefix line 44
  15. theorem OAI.KS.W11.FramedArrayRewrite.run_skip line 55
  16. theorem OAI.KS.W11.FramedArrayRewrite.run_reverseNew line 77
  17. theorem OAI.KS.W11.FramedArrayRewrite.run_insertNew line 90
  18. theorem OAI.KS.W11.FramedArrayRewrite.run_restorePrefix line 103
  19. theorem OAI.KS.W11.FramedArrayRewrite.run_finish line 116
  20. theorem OAI.KS.W11.FramedArrayRewrite.run_replaceTail line 144
  21. def OAI.KS.W11.FramedArrayRewrite.replaceFuel line 159
  22. theorem OAI.KS.W11.FramedArrayRewrite.run_replace_prefix line 163
  23. theorem OAI.KS.W11.FramedArrayRewrite.replaceFuel_linear line 192
  24. theorem OAI.KS.W11.FramedArrayRewrite.run_replace line 200
  25. theorem OAI.KS.W11.FramedArrayRewrite.replacement_linear_time line 229