OAI/Probability/Contingency/StackSafety.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

Stack Safety.

  1. theorem OAI.Contingency.BitModel.StackCode.mass_eq_zero_of_safe line 14
  2. theorem OAI.Contingency.BitModel.StackCode.safe_compile line 29
  3. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.beValue_snoc line 61
  4. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.beValue_bits_reverse line 67
  5. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.minimal_width line 74
  6. def OAI.Contingency.BitModel.StackCode.IntegerDraw.rawMaximum line 86
  7. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.rawMaximum_length line 88
  8. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.rawMaximum_value line 90
  9. def OAI.Contingency.BitModel.StackCode.IntegerDraw.integerWord line 92
  10. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.integerWord_value line 95
  11. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.integerWord_length line 99
  12. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.machine_safe line 102
  13. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.integer_sampler line 109
  14. def OAI.Contingency.BitModel.StackCode.BinarySubtract.outBit line 139
  15. def OAI.Contingency.BitModel.StackCode.BinarySubtract.nextBorrow line 140
  16. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.digit_identity line 142
  17. def OAI.Contingency.BitModel.StackCode.BinarySubtract.value line 146
  18. structure OAI.Contingency.BitModel.StackCode.BinarySubtract.Digit line 150
  19. def OAI.Contingency.BitModel.StackCode.BinarySubtract.output line 154
  20. def OAI.Contingency.BitModel.StackCode.BinarySubtract.borrow line 158
  21. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.output_length line 162
  22. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.value_lt line 167
  23. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.word_identity line 175
  24. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.subtract_correct line 186
  25. inductive OAI.Contingency.BitModel.StackCode.BinarySubtract.Q line 195
  26. def OAI.Contingency.BitModel.StackCode.BinarySubtract.label line 202
  27. def OAI.Contingency.BitModel.StackCode.BinarySubtract.code line 204
  28. def OAI.Contingency.BitModel.StackCode.BinarySubtract.program line 210
  29. def OAI.Contingency.BitModel.StackCode.BinarySubtract.config line 211
  30. def OAI.Contingency.BitModel.StackCode.BinarySubtract.digitMemory line 213
  31. def OAI.Contingency.BitModel.StackCode.BinarySubtract.wordMemory line 216
  32. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.one_step line 220
  33. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.first_step line 225
  34. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.second_step line 230
  35. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.third_step line 235
  36. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.three_steps line 241
  37. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.pass line 250
  38. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.step_independent line 278
  39. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.fold_independent line 287
  40. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.pass_any line 300
  41. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.wordMemory_stacks line 308
  42. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.finish line 326
  43. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.halt line 330
  44. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.finish_run line 334
  45. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.fold_compiled line 343
  46. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.tape_pass line 354
  47. def OAI.Contingency.BitModel.StackCode.BinaryAdd.nextCarry line 374
  48. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.digit_identity line 376
  49. def OAI.Contingency.BitModel.StackCode.BinaryAdd.output line 380
  50. def OAI.Contingency.BitModel.StackCode.BinaryAdd.carry line 384
  51. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.output_length line 388
  52. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.word_identity line 393
  53. inductive OAI.Contingency.BitModel.StackCode.BinaryAdd.Q line 404
  54. def OAI.Contingency.BitModel.StackCode.BinaryAdd.label line 412
  55. def OAI.Contingency.BitModel.StackCode.BinaryAdd.code line 414
  56. def OAI.Contingency.BitModel.StackCode.BinaryAdd.program line 421
  57. def OAI.Contingency.BitModel.StackCode.BinaryAdd.config line 422
  58. def OAI.Contingency.BitModel.StackCode.BinaryAdd.digitMemory line 424
  59. def OAI.Contingency.BitModel.StackCode.BinaryAdd.wordMemory line 427
  60. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.one_step line 431
  61. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.first_step line 436
  62. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.second_step line 441
  63. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.third_step line 446
  64. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.three_steps line 452
  65. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.pass line 461
  66. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.step_independent line 490
  67. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.fold_independent line 499
  68. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.pass_any line 512
  69. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.wordMemory_stacks line 520
  70. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.finish line 538
  71. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.final_carry line 542
  72. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.halt line 546
  73. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.finish_run line 550
  74. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.tape_pass line 561
  75. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.value_append_false line 580
  76. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.value_bits line 590
  77. def OAI.Contingency.BitModel.StackCode.BinarySubtract.bits line 600
  78. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.bits_length line 602
  79. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.bits_value line 608
  80. def OAI.Contingency.BitModel.StackCode.BinarySubtract.digits line 611
  81. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.digits_maps line 613
  82. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.borrow_iff line 628
  83. theorem OAI.Contingency.BitModel.StackCode.BinarySubtract.padded_subtraction line 645