OAI/Analysis/MatrixSigning/Machines/FixedStackMachine.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.KS.W01.FixedStack.Instruction line 11
  2. def OAI.KS.W01.FixedStack.Instruction.action line 15
  3. def OAI.KS.W01.FixedStack.Instruction.halt line 18
  4. structure OAI.KS.W01.FixedStack.Machine line 21
  5. theorem OAI.KS.W01.FixedStack.Machine.stackCount_pos line 29
  6. theorem OAI.KS.W01.FixedStack.Machine.states_pos line 32
  7. def OAI.KS.W01.FixedStack.haltMachine line 35
  8. structure OAI.KS.W01.FixedStack.Config line 37
  9. def OAI.KS.W01.FixedStack.headsCode line 41
  10. def OAI.KS.W01.FixedStack.decodeHeads line 45
  11. theorem OAI.KS.W01.FixedStack.headsCode_lt line 49
  12. theorem OAI.KS.W01.FixedStack.decodeHeads_headsCode line 58
  13. def OAI.KS.W01.FixedStack.observedHeads line 75
  14. def OAI.KS.W01.FixedStack.headFin line 78
  15. def OAI.KS.W01.FixedStack.coinFin line 81
  16. def OAI.KS.W01.FixedStack.tableIndex line 83
  17. theorem OAI.KS.W01.FixedStack.tableIndex_val line 87
  18. def OAI.KS.W01.FixedStack.Machine.step line 93
  19. def OAI.KS.W01.FixedStack.Machine.init line 102
  20. def OAI.KS.W01.FixedStack.Machine.run line 105
  21. def OAI.KS.W01.FixedStack.Machine.output line 110
  22. def OAI.KS.W01.FixedStack.Machine.runSeed line 113
  23. def OAI.KS.W01.FixedStack.Machine.HaltsWithin line 116
  24. def OAI.KS.W01.FixedStack.Machine.successCount line 119
  25. def OAI.KS.W01.FixedStack.Machine.SucceedsTwoThirds line 125
  26. def OAI.KS.W01.FixedStack.Machine.PolynomialTime line 129
  27. def OAI.KS.W01.FixedStack.RandomizedPolynomialSpec line 133
  28. theorem OAI.KS.W01.FixedStack.Machine.step_halted line 139
  29. theorem OAI.KS.W01.FixedStack.Machine.run_halted line 142
  30. theorem OAI.KS.W01.FixedStack.Machine.run_append line 148
  31. theorem OAI.KS.W01.FixedStack.Machine.step_stack_length_le line 154
  32. theorem OAI.KS.W01.FixedStack.Machine.run_stack_length_le line 162
  33. def OAI.KS.W01.FixedStack.decodeDispatch line 173
  34. def OAI.KS.W01.FixedStack.compile line 180
  35. theorem OAI.KS.W01.FixedStack.compile_table_length line 184
  36. theorem OAI.KS.W01.FixedStack.decodeDispatch_tableIndex line 189
  37. theorem OAI.KS.W01.FixedStack.lookup_compile line 197
  38. theorem OAI.KS.W01.FixedStack.step_compile line 207
  39. def OAI.KS.W01.FixedStack.liftInstruction line 218
  40. theorem OAI.KS.W01.FixedStack.liftInstruction_on_port line 224
  41. theorem OAI.KS.W01.FixedStack.liftInstruction_off_port line 230
  42. def OAI.KS.W01.FixedStack.project line 235
  43. def OAI.KS.W01.FixedStack.selectedCode line 238
  44. def OAI.KS.W01.FixedStack.liftDispatch line 241
  45. def OAI.KS.W01.FixedStack.lift3 line 247
  46. theorem OAI.KS.W01.FixedStack.lift3_step line 250
  47. theorem OAI.KS.W01.FixedStack.lift3_project_step line 261
  48. theorem OAI.KS.W01.FixedStack.lift3_step_preserves_other line 275
  49. theorem OAI.KS.W01.FixedStack.lift3_project_run line 288
  50. theorem OAI.KS.W01.FixedStack.lift3_run_preserves_other line 298
  51. theorem OAI.KS.W01.FixedStack.lift3_project_init line 308
  52. theorem OAI.KS.W01.FixedStack.lift3_output_eq line 318
  53. theorem OAI.KS.W01.FixedStack.lift3_runSeed_state line 325
  54. theorem OAI.KS.W01.FixedStack.lift3_haltsWithin_iff line 333
  55. theorem OAI.KS.W01.FixedStack.lift3_successCount_eq line 343
  56. theorem OAI.KS.W01.FixedStack.lift3_succeedsTwoThirds_iff line 355
  57. def OAI.KS.W01.FixedStack.embed3 line 362
  58. def OAI.KS.W01.FixedStack.ofThree line 364
  59. theorem OAI.KS.W01.FixedStack.project_ofThree line 366
  60. theorem OAI.KS.W01.FixedStack.ofThree_project line 369
  61. theorem OAI.KS.W01.FixedStack.embed3_run line 372
  62. theorem OAI.KS.W01.FixedStack.embed3_output_eq line 379
  63. theorem OAI.KS.W01.FixedStack.embed3_haltsWithin_iff line 382