OAI/Analysis/MatrixSigning/Encoding/ZeroArrayConstructor.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W11.ZeroArrayConstructor.«stacks» line 11
  2. theorem OAI.KS.W11.ZeroArrayConstructor.config_ext line 14
  3. def OAI.KS.W11.ZeroArrayConstructor.emitDispatch line 20
  4. def OAI.KS.W11.ZeroArrayConstructor.emitProgram line 27
  5. theorem OAI.KS.W11.ZeroArrayConstructor.emit_step line 30
  6. theorem OAI.KS.W11.ZeroArrayConstructor.emit_done line 43
  7. theorem OAI.KS.W11.ZeroArrayConstructor.run_emit_aux line 55
  8. theorem OAI.KS.W11.ZeroArrayConstructor.emit_spec line 84
  9. def OAI.KS.W11.ZeroArrayConstructor.zeroFrame line 92
  10. theorem OAI.KS.W11.ZeroArrayConstructor.zeroFrame_length line 93
  11. def OAI.KS.W11.ZeroArrayConstructor.zeroTape line 94
  12. def OAI.KS.W11.ZeroArrayConstructor.bodyProgram line 95
  13. theorem OAI.KS.W11.ZeroArrayConstructor.zeroTape_succ line 97
  14. theorem OAI.KS.W11.ZeroArrayConstructor.zeroTape_length line 100
  15. def OAI.KS.W11.ZeroArrayConstructor.guard line 107
  16. def OAI.KS.W11.ZeroArrayConstructor.loopProgram line 111
  17. def OAI.KS.W11.ZeroArrayConstructor.finishProgram line 112
  18. def OAI.KS.W11.ZeroArrayConstructor.program line 113
  19. theorem OAI.KS.W11.ZeroArrayConstructor.program_states line 115
  20. theorem OAI.KS.W11.ZeroArrayConstructor.program_states_numeric line 116
  21. theorem OAI.KS.W11.ZeroArrayConstructor.program_input line 117
  22. theorem OAI.KS.W11.ZeroArrayConstructor.program_output line 118
  23. theorem OAI.KS.W11.ZeroArrayConstructor.guard_nil line 120
  24. theorem OAI.KS.W11.ZeroArrayConstructor.guard_cons line 133
  25. theorem OAI.KS.W11.ZeroArrayConstructor.run_loop line 147
  26. theorem OAI.KS.W11.ZeroArrayConstructor.finish_spec line 176
  27. theorem OAI.KS.W11.ZeroArrayConstructor.zero_spec line 188
  28. theorem OAI.KS.W11.ZeroArrayConstructor.zero_spec_linear line 204