OAI/Computability/FiniteCompiler/Machines.lean

GitHub source file

115 declarations, 0 contain sorry, 0 declared as axioms

Stack, binary, TM2, and TM0 realizations of partial recursive programs.

  1. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.swap line 13
  2. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.swap_swap line 15
  3. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.swap_injective line 16
  4. abbrev OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.Symbol line 19
  5. abbrev OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.Store line 20
  6. inductive OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.Label line 21
  7. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.proj line 27
  8. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.store line 29
  9. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.proj_store line 30
  10. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.embedStacks line 32
  11. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.embedStacks_swap line 33
  12. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.embedStacks_update line 35
  13. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.stmt line 44
  14. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.cfg line 54
  15. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.stmt_correct line 58
  16. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.step_correct line 90
  17. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.reaches_correct line 101
  18. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.path_cases line 109

    Source documentation

    Until the original interpreter halts, the wrapper cannot escape its run sector. This is the divergence/soundness half, not only a terminating test.

     theorem path_cases {c : TM2.Cfg (fun _ : K' => Γ') Λ (Option Γ')}
    {z : TM2.Cfg (fun _ : K' => Symbol S) (Label S Λ) (Store S)}
    (h : TM2.Reaches W (cfg c) z) :
    (∃ d, TM2.Reaches M c d ∧ z = cfg d) ∨
    (∃ d, TM2.Reaches M c d ∧ d.l = none ∧ TM2.Reaches W (cfg d) z) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.Symbol, OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.Label, OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.Store, OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackLift.cfg

  19. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.BinaryCode.value line 136
  20. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.BinaryCode.value_pos line 142
  21. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.BinaryCode.value_num line 148
  22. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.BinaryCode.value_nat line 149
  23. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.BinaryCode.trNat_injective line 150
  24. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.BinaryCode.block line 154
  25. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.BinaryCode.delimiter_cancel line 156
  26. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.BinaryCode.block_cancel line 181
  27. abbrev OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.Stmt line 194
  28. abbrev OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.Config line 195
  29. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.tracks line 197
  30. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.tracks_main line 203
  31. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.tracks_rev line 205
  32. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.tracks_update_main line 207
  33. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.tracks_update_rev line 211
  34. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.postCfg line 215
  35. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.reject line 216
  36. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.finish line 217
  37. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.decoder line 222
  38. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.decoder_correct line 231
  39. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.decoder_block line 267
  40. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.pushList line 275
  41. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.pushList_correct line 280
  42. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.machine line 292
  43. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.preCfg line 306
  44. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.haltCfg line 307
  45. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.runCfg line 308
  46. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.pre_cons line 313
  47. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.pre_nil line 327
  48. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.numbers line 335
  49. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.trList_append line 338
  50. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.pre_complete line 344
  51. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.post_cons line 355
  52. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.post_nil line 372
  53. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.post_complete line 378
  54. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.baseCfg line 388
  55. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.lift_base_some line 392
  56. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.lift_base_none line 398
  57. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.eval_run line 405
  58. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.RawTM.eval_pre line 447
  59. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FiniteTM2.restrictStmt line 468
  60. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FiniteTM2.embedCfg line 479
  61. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FiniteTM2.embed_stepAux line 484
  62. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FiniteTM2.machine line 498
  63. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FiniteTM2.embed_step line 502
  64. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FiniteTM2.respects line 511
  65. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FiniteTM2.eval_embed line 526
  66. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FiniteTM2.initial line 532
  67. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FiniteTM2.embed_initial line 536
  68. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FiniteTM2.eval_initial line 540
  69. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.Numerical.exists_evaluator line 554
  70. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.Numerical.exists_finite_evaluator line 562
  71. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.eval_comp line 576
  72. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.fix_eval_fwd line 581
  73. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.prefix₂ line 590
  74. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.prefix₂_eval line 591
  75. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.binary_code line 594
  76. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.test line 602
  77. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.test_eval line 603
  78. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.one line 609
  79. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.one_eval line 610
  80. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.encodeStep line 612
  81. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.encoder line 615
  82. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.encodeStep_nil line 617
  83. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.encodeStep_cons line 621
  84. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.encode_loop line 628
  85. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.encoder_eval line 649
  86. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.decodeStep line 655
  87. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.decoder line 658
  88. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.decodeStep_zero line 659
  89. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.decodeStep_cons line 663
  90. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.decoder_eval line 671
  91. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.unary_code line 694
  92. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ListCode.exists_wordCode line 703
  93. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FiniteTM2.embedCfg_injective line 750
  94. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.part_map_injective line 763
  95. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.WordEvaluator.exists_code line 781
  96. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.WordEvaluator.exists_finite line 797
  97. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.WordEvaluator.bound line 817
  98. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.WordEvaluator.le_bound line 818
  99. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.WordEvaluator.exists_raw line 821
  100. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FiniteTM0.machine line 842
  101. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FiniteTM0.embed line 845
  102. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FiniteTM0.embed_injective line 848
  103. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FiniteTM0.embed_step line 857
  104. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FiniteTM0.respects line 865
  105. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FiniteTM0.eval_embed line 880
  106. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackTape.slice line 890
  107. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackTape.stackList line 891
  108. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackTape.tape line 892
  109. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackTape.tracks_proj line 896
  110. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackTape.trCfg line 902
  111. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackTape.stackList_unique line 907
  112. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackTape.trCfg_unique line 917
  113. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackTape.eval_tape line 926
  114. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.StackTape.eval_post line 949
  115. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.WordEvaluator.exists_tape line 964