OAI/Computability/FiniteCompiler/Simulator.lean

GitHub source file

132 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Alphabet line 13

   Source documentation

   Finite work alphabet, including a literal code for every input letter and a distinct blank. The remaining symbols are rejected by output reading.

   structure Alphabet (S Γ : Type*) where
   …

2. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Move line 20
3. instance OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.(instance at line 24) line 24
4. structure OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Command line 26
5. structure OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Machine line 34

   Source documentation

   A deterministic left-ended one-tape machine. none is halt, recognized only while the head is at a workspace cell.

   structure Machine (Q Γ : Type*) where
   …

6. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Resume line 38
7. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Head line 44

   Source documentation

   Distinct phases make every scan's designated reading side unambiguous.

   inductive Head (S Q : Type*)
     | start
     | rewind : Resume S → Head S Q
     | scan : Resume S → Head S Q
     | run : Q → Head S Q
     | left : Q → Head S Q
     | finish | ok
     deriving DecidableEq, Fintype
   
   variable {S Γ Q : Type*}
   
   /-- The cell table is finite when the alphabets and state set are finite. All

   Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.rewind, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Resume, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.finish, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.cell, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table

8. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.cell line 57

   Source documentation

   The cell table is finite when the alphabets and state set are finite. All tests and assignments are precisely the source's scan expansion.

   def cell (A : Alphabet S Γ) (M : Machine Q Γ) [DecidableEq Γ]
       (q : Head S Q) (b : Base S) (t : Tag S Γ) :
       Option (Instruction (Head S Q) (Tag S Γ)) :=
   …

   Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Alphabet, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Machine, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Head, OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Instruction

9. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table line 100
10. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.run_outside line 114

    Source documentation

    No false acceptance results from an attempted simulation past a quota edge.

    theorem run_outside (A : Alphabet S Γ) (M : Machine Q Γ) [DecidableEq Γ]
        (q : Q) (b : Base S) (t : Tag S Γ) (hb : b ≠ .workspace) :
        (table A M).cell (.run q) b t = none := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Alphabet, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Machine, OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.cell

11. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.ok_terminal line 119
12. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.rewind line 129

    Source documentation

    Rewinding crosses all left cells unchanged and then changes phase at alpha. This lemma holds on dirty data as well as the intended clean simulation.

    theorem rewind (A : Alphabet S Γ) (M : Machine Q Γ) [DecidableEq Γ]
        (s : Resume S) (l r : List (Base S × Tag S Γ)) (rb : Bool) :
        Relation.ReflTransGen (Scan.Step (table A M))
          ⟨l,.rewind s,r,true,rb⟩ ⟨[],.scan s,l.reverse ++ r,true,rb⟩ := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Alphabet, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Machine, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Resume, OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table

13. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.finish line 142

    Source documentation

    Going to the right boundary also preserves every cell.

    theorem finish (A : Alphabet S Γ) (M : Machine Q Γ) [DecidableEq Γ]
        (l r : List (Base S × Tag S Γ)) (lb : Bool) :
        Relation.ReflTransGen (Scan.Step (table A M))
          ⟨l,.finish,r,lb,true⟩ ⟨r.reverse ++ l,.ok,[],lb,true⟩ := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Alphabet, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Machine, OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table

14. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.cross_right line 160
15. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells line 183
16. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.scan_update line 187

    Source documentation

    One complete find/update/rewind invocation acts on the first matching cell. No higher-level operation is used in the actual finite table.

    theorem scan_update (s s' : Resume S) (p r : Cells S Γ) (b : Base S) (t t' : Tag S Γ)
        (hp : ∀ c ∈ p, cell A M (.scan s) c.1 c.2 = some ⟨.scan s,c.2,true⟩)
        (hc : cell A M (.scan s) b t = some ⟨.rewind s',t',false⟩) :
        ReflTransGen (Scan.Step (table A M))
          ⟨[],.scan s,p ++ (b,t)::r,true,true⟩
          ⟨[],.scan s',p ++ (b,t')::r,true,true⟩ := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Resume, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.cell, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.rewind, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table

17. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.readAnchor line 204

    Source documentation

    Tags following the copy phase; unused full-tag fields remain literally clean, as required by the validator/simulator convention.

    def readAnchor (a : S) (read : Bool) : Base S × Tag S Γ :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag

18. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.filledWork line 207
19. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.bare line 210
20. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.body line 214

    Source documentation

    The whole tape during copying: read and unread anchor prefixes on either side of the reserved workspace, with a filled prefix followed by blanks.

    def body (xp xs yp ys w : List S) (n : ℕ) : Cells S Γ :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells

21. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Pass line 219
22. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pass_read line 222
23. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pass_input_bareC line 224
24. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pass_input_bareD line 225
25. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pass_input_bareW line 226
26. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pass_input_filled line 227
27. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pass_fill_anchor line 228
28. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pass_fill_bareC line 230
29. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pass_fill_filled line 231
30. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.copy_left_one line 235

    Source documentation

    A loaded input letter is transferred to the next free workspace cell, expanding the prefix and shrinking the finite quota by one.

    theorem copy_left_one (xp xs yp ys w : List S) (a : S) (n : ℕ) :
        ReflTransGen (Scan.Step (table A M))
          ⟨[],.scan .input,body A xp (a::xs) yp ys w (n+1),true,true⟩
          ⟨[],.scan .input,body A (xp++[a]) xs yp ys (w++[a]) n,true,true⟩ := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.body

31. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.copy_right_one line 265
32. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.copy_left line 300
33. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.copy_right line 311
34. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.copy_all line 323

    Source documentation

    Both anchor blocks are copied in their order, not in zipper order.

    theorem copy_all (x y : List S) (n : ℕ) :
        ReflTransGen (Scan.Step (table A M))
          ⟨[],.scan .input,body A [] x [] y [] (x.length+y.length+n),true,true⟩
          ⟨[],.scan .input,body A x [] y [] (x++y) n,true,true⟩ := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.body

35. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pass_spare_anchor line 332
36. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pass_spare_C line 334
37. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pass_spare_filled line 335
38. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pass_first_anchor line 336
39. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pass_first_C line 338
40. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.copy_enter_run line 343

    Source documentation

    The two final copy scans check a spare blank and position the machine at the first workspace cell. In particular the quota is not treated as tape that may silently grow during internal transitions.

    theorem copy_enter_run (x y w : List S) (n : ℕ) :
        ReflTransGen (Scan.Step (table A M))
          ⟨[],.scan .input,body A x [] y [] w (n+1),true,true⟩
          ⟨(x.map (readAnchor A · true) ++ [bare A .cutC]).reverse,.run M.initial,
            w.map (filledWork A) ++ List.replicate (n+1) (bare A .workspace) ++
              [bare A .cutD] ++ y.map (readAnchor A · true),true,true⟩ := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.body, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.readAnchor, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.bare, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.filledWork

41. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.start_copy line 397

    Source documentation

    The fresh post-validator handoff starts copying from the left boundary.

    theorem start_copy (cells : Cells S Γ) :
        ReflTransGen (Scan.Step (table A M))
          ⟨cells.reverse,.start,[],true,true⟩ ⟨[],.scan .input,cells,true,true⟩ := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table

42. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.copy_correct line 407

    Source documentation

    Literal correctness of the complete copy/init program with any sufficient finite quota. Every table operation is one of the listed compiled equations.

    theorem copy_correct (x y : List S) (n : ℕ) :
        ReflTransGen (Scan.Step (table A M))
          ⟨(body A [] x [] y [] (x.length+y.length+n+1)).reverse,.start,[],true,true⟩
          ⟨(x.map (readAnchor A · true) ++ [bare A .cutC]).reverse,.run M.initial,
            (x++y).map (filledWork A) ++ List.replicate (n+1) (bare A .workspace) ++
              [bare A .cutD] ++ y.map (readAnchor A · true),true,true⟩ := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.body, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.readAnchor, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.bare, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.filledWork

43. structure OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape line 426

    Source documentation

    A literal bounded workspace. The left list is in reverse tape order, and an empty right list is outside the supplied quota, not a fresh blank cell.

    structure Tape where
    …

44. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.writeWork line 432

    Source documentation

    Update only the simulated work track; all auxiliary tag fields are retained.

    def writeWork (t : Tag S Γ) (a : Γ) : Tag S Γ := { t with work := a }

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Tag

45. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.TapeStep line 436

    Source documentation

    The intended finite-quota operations of the finite compiler. These are defined from the given machine table, not postulated accepting transitions.

    inductive TapeStep (M : Machine Q Γ) : Tape (S := S) (Γ := Γ) (Q := Q) → Tape → Prop
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Machine, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

46. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.workCells line 446
47. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.runSector line 450

    Source documentation

    Workspace in its fixed surrounding anchor/cut sector. x is the cells before C in their ordinary order, y the cells following D.

    def runSector (A : Alphabet S Γ) (x y : Cells S Γ) (c : Tape (S := S) (Γ := Γ) (Q := Q)) :
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Alphabet, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

48. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.tapeStep_simulates line 460

    Source documentation

    Every bounded machine transition is implemented by one or two actual finite scan instructions. Both the stationary left edge and true left movement are proved, and no quota insertion occurs during simulation.

    theorem tapeStep_simulates (x y : Cells S Γ) {c d : Tape (S := S) (Γ := Γ) (Q := Q)}
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

49. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.tapeRun_simulates line 488

    Source documentation

    Simulation respects literal finite traces, without a running-time bound.

    theorem tapeRun_simulates (x y : Cells S Γ) {c d : Tape (S := S) (Γ := Γ) (Q := Q)}
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

50. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.quota_exhausted line 497

    Source documentation

    Exhaustion is stuck even if the machine's current state would be halting: a halt must be observed at an actual workspace cell.

    theorem quota_exhausted (x y : Cells S Γ) (q : Q) (l : List (Tag S Γ)) :
        Scan.step (table A M) (runSector A x y ⟨q,l,[]⟩) = none := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.runSector

51. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.halt_readout line 502

    Source documentation

    A genuine in-bounds halt triggers precisely the readout rewind.

    theorem halt_readout (x y : Cells S Γ) (q : Q) (l : List (Tag S Γ))
        (t : Tag S Γ) (r : List (Tag S Γ)) (h : M.transition q t.work = none) :
        ReflTransGen (Scan.Step (table A M))
          (runSector A x y ⟨q,l,t::r⟩)
          ⟨[],.scan .readout,
            x ++ [bare A .cutC] ++ workCells (l.reverse ++ t::r) ++ bare A .cutD :: y,
            true,true⟩ := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.runSector, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.bare, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.workCells

52. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.split_filterMap line 526

    Source documentation

    Locate a specified item of a projected list without discarding the cells skipped by the projection. This handles interleaved anchors and workspace.

    theorem split_filterMap {α β : Type*} (f : α → Option β) (l : List α)
        (p : List β) (b : β) (r : List β) (h : l.filterMap f = p ++ b::r) :
        ∃ l₁ a l₂, l = l₁ ++ a::l₂ ∧ l₁.filterMap f = p ∧
          f a = some b ∧ l₂.filterMap f = r := by
    …

53. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.workView line 549
54. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.anchorView line 554
55. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.workView_append line 559
56. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.anchorView_append line 561
57. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.readout_pass line 566
58. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.put_pass line 578
59. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.readout_one line 591

    Source documentation

    One output letter is read from the first unread workspace cell and written to the first unmarked anchor. The projected views certify both orders.

    theorem readout_one (cells : Cells S Γ) (done remaining : List Γ)
        (out : List S) (a : S) (g : Γ) (n : ℕ)
        (hw : workView cells = done.map (true,·) ++ (false,g)::remaining.map (false,·))
        (ha : anchorView cells = out.map some ++ none :: List.replicate n none)
        (hg : g ≠ A.blank) (hg' : A.output g = some a) :
        ∃ cells', ReflTransGen (Scan.Step (table A M))
          ⟨[],.scan .readout,cells,true,true⟩ ⟨[],.scan .readout,cells',true,true⟩ ∧
          workView cells' = (done ++ [g]).map (true,·) ++ remaining.map (false,·) ∧
          anchorView cells' = (out ++ [a]).map some ++ List.replicate n none := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.workView, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.anchorView, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table

60. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.readout_blank line 646

    Source documentation

    The first unread blank ends output. No cell is changed by the final sweep.

    theorem readout_blank (cells : Cells S Γ) (done : List Γ) (rest : List (Bool × Γ))
        (hw : workView cells = done.map (true,·) ++ (false,A.blank)::rest) :
        ReflTransGen (Scan.Step (table A M))
          ⟨[],.scan .readout,cells,true,true⟩ ⟨cells.reverse,.ok,[],true,true⟩ := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.workView, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table

61. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.input_ne_blank line 673
62. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.readout_complete line 682

    Source documentation

    Complete readout of a finite, blank-delimited returned string. The spare anchor count drops by exactly one for each letter, including when that letter's anchor is on the other side of the workspace.

    theorem readout_complete (out : List S) (cells : Cells S Γ) (done tail : List Γ)
        (old : List S) (n : ℕ)
        (hw : workView cells = done.map (true,·) ++
          (out.map A.input ++ A.blank::tail).map (false,·))
        (ha : anchorView cells = old.map some ++ List.replicate (out.length+n) none) :
        ∃ cells', ReflTransGen (Scan.Step (table A M))
          ⟨[],.scan .readout,cells,true,true⟩ ⟨cells'.reverse,.ok,[],true,true⟩ ∧
          anchorView cells' = (old ++ out).map some ++ List.replicate n none := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.workView, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.anchorView, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table

63. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Rejects line 718

    Source documentation

    Rejection here means the actual finite table has no forward accepting trace; it is stronger than merely failing a chosen simulation trace.

    def Rejects (v : Scan.Sector (Head S Q) (Base S) (Tag S Γ)) : Prop :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Head, OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag

64. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.terminal_of_none line 721
65. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.rejects_of_stuck line 727
66. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.rejects_before line 736
67. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.readout_no_unread line 746

    Source documentation

    No unread cell, in particular no blank delimiter, means that readout stops at omega without entering the finish phase.

    theorem readout_no_unread (cells : Cells S Γ) (done : List Γ)
        (h : workView cells = done.map (true,·)) :
        Rejects A M ⟨[],.scan .readout,cells,true,true⟩ := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.workView, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Rejects

68. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.put_no_anchor line 756

    Source documentation

    Filled anchors cannot be overwritten. Exhausting them rejects even if a workspace character was successfully decoded.

    theorem put_no_anchor (cells : Cells S Γ) (old : List S) (a : S)
        (h : anchorView cells = old.map some) :
        Rejects A M ⟨[],.scan (.put a),cells,true,true⟩ := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.anchorView, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Rejects

69. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.readout_invalid line 765

    Source documentation

    Metasymbols that are neither blank nor returned letters block output.

    theorem readout_invalid (cells : Cells S Γ) (done : List Γ) (g : Γ)
        (rest : List (Bool × Γ))
        (h : workView cells = done.map (true,·) ++ (false,g)::rest)
        (hg : g ≠ A.blank) (hdecode : A.output g = none) :
        Rejects A M ⟨[],.scan .readout,cells,true,true⟩ := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.workView, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Rejects

70. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.readout_no_anchor line 785

    Source documentation

    The first nonblank output symbol cannot succeed when all anchors are full.

    theorem readout_no_anchor (cells : Cells S Γ) (done : List Γ) (rest : List (Bool × Γ))
        (old : List S) (a : S) (g : Γ)
        (hw : workView cells = done.map (true,·) ++ (false,g)::rest)
        (ha : anchorView cells = old.map some)
        (hg : g ≠ A.blank) (hdecode : A.output g = some a) :
        Rejects A M ⟨[],.scan .readout,cells,true,true⟩ := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.workView, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.anchorView, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Rejects

71. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.readout_too_long line 809

    Source documentation

    Insufficient anchor quota is rejected without truncating the returned string or replacing it by an arbitrary shorter result.

    theorem readout_too_long (out : List S) (cells : Cells S Γ) (done tail : List Γ)
        (old : List S) (n : ℕ)
        (hw : workView cells = done.map (true,·) ++
          (out.map A.input ++ A.blank::tail).map (false,·))
        (ha : anchorView cells = old.map some ++ List.replicate n none)
        (hn : n < out.length) : Rejects A M ⟨[],.scan .readout,cells,true,true⟩ := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.workView, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.anchorView, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Rejects

72. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pad line 841

    Source documentation

    Appending untouched blank cells reserves quota without altering any already represented tape position.

    def pad (A : Alphabet S Γ) (c : Tape (S := S) (Γ := Γ) (Q := Q)) (n : ℕ) : Tape (S := S) (Γ := Γ) (Q := Q) :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Alphabet, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

73. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.UnboundedStep line 847

    Source documentation

    Unbounded left-ended tape semantics. A cell beyond the finite represented region is blank; it is materialized only when reached. No output fact or acceptance relation is built into these transition constructors.

    inductive UnboundedStep (A : Alphabet S Γ) (M : Machine Q Γ) :
        Tape (S := S) (Γ := Γ) (Q := Q) → Tape (S := S) (Γ := Γ) (Q := Q) → Prop
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Alphabet, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Machine, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

74. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.tapeStep_pad line 857

    Source documentation

    A bounded operation never inspects cells beyond its current head and is therefore preserved by appending arbitrary extra blank quota.

    theorem tapeStep_pad {c d : Tape (S := S) (Γ := Γ) (Q := Q)}
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

75. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.tapeRun_pad line 865
76. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.finite_quota line 874

    Source documentation

    Every finite unbounded trace uses a finite quota. The terminal padding can be prescribed in advance, in particular ensuring an explicit spare blank.

    theorem finite_quota {c d : Tape (S := S) (Γ := Γ) (Q := Q)}
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

77. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.tapeStep_tags line 892

    Source documentation

    A predicate on full tags insensitive to changes of the work symbol is an invariant of every bounded run, not just of a chosen clean execution.

    theorem tapeStep_tags (P : Tag S Γ → Prop)
        (hwrite : ∀ t a, P t → P (writeWork t a))
        {c d : Tape (S := S) (Γ := Γ) (Q := Q)} (h : TapeStep M c d)
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.writeWork, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.TapeStep

78. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.unboundedStep_tags line 920
79. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.unboundedRun_tags line 931
80. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.initialTape line 940

    Source documentation

    Initial finite representation after copying, before adding blank quota.

    def initialTape (w : List S) : Tape (S := S) (Γ := Γ) (Q := Q) :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

81. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Halted line 944

    Source documentation

    The halt test includes the implicit blank at the first unrepresented cell.

    def Halted (c : Tape (S := S) (Γ := Γ) (Q := Q)) : Prop :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

82. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Returns line 949

    Source documentation

    The returned string begins at position zero and is delimited by its first blank. Extra blanks may lie outside the finite represented portion.

    def Returns (c : Tape (S := S) (Γ := Γ) (Q := Q)) (out : List S) : Prop :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

83. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pad_left line 953
84. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pad_right line 956
85. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.halt_pad line 959
86. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.workView_workCells line 966
87. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.anchorView_workCells line 970
88. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.finalCells line 974

    Source documentation

    Full cell list at readout, with the copied anchors on either side.

    def finalCells (x y : List S) (c : Tape (S := S) (Γ := Γ) (Q := Q)) : Cells S Γ :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells

89. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.anchorView_readAnchors line 978
90. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.workView_readAnchors line 987
91. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.finalCells_anchors line 991
92. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.finalCells_work line 999
93. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.copy_correct_pad line 1017
94. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.halt_readout_pad line 1027
95. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.unread_pad line 1041
96. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.simulation_complete line 1054

    Source documentation

    Adequate quota for every genuinely halting, length-bounded output. This connects the actual copy/run/readout table, including empty inputs, without assuming a bound on the machine's running time or workspace beforehand.

    theorem simulation_complete (x y out : List S)
        (c : Tape (S := S) (Γ := Γ) (Q := Q))
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

97. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.haltSector line 1100

    Source documentation

    The first readout-rewind configuration, before any tape cell is moved.

    def haltSector (x y : Cells S Γ) (c : Tape (S := S) (Γ := Γ) (Q := Q)) :
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

98. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.run_step_cases line 1107

    Source documentation

    Exact classification of a simulator step made in a workspace run phase. The only intermediate phase is the deterministic half of a left move.

    theorem run_step_cases (x y : Cells S Γ)
        (c : Tape (S := S) (Γ := Γ) (Q := Q))
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

99. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.simulation_halt_sound line 1152

    Source documentation

    Arbitrary accepting paths, not just chosen forward simulations, must have exited the run phases through a genuine in-bounds machine halt.

    theorem simulation_halt_sound (x y : Cells S Γ)
        {c : Tape (S := S) (Γ := Γ) (Q := Q)}
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

100. structure OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.SemanticTape line 1189

     Source documentation

     Semantic one-sided tape: its right end is an infinite blank tail, not an extra halting edge. Auxiliary simulator tags do not enter this semantics.

     structure SemanticTape (Γ Q : Type*) where
     …

101. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.semanticStep line 1195

     Source documentation

     The literal machine command interpreted on an infinite right-hand tape.

     def semanticStep (M : Machine Q Γ) (c : SemanticTape Γ Q) : Option (SemanticTape Γ Q) :=
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Machine, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.SemanticTape

102. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.SemanticStep line 1204
103. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.interpret line 1207
104. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.replicate_append_const line 1211
105. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.interpret_pad line 1219
106. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.tapeStep_interpret line 1226

     Source documentation

     Each bounded transition is exactly one transition of the semantic machine.

     theorem tapeStep_interpret (A : Alphabet S Γ) (M : Machine Q Γ)
         {c d : Tape (S := S) (Γ := Γ) (Q := Q)} (h : TapeStep M c d) :
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Alphabet, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Machine, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.TapeStep

107. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.unboundedStep_interpret line 1233

     Source documentation

     Materializing an implicit blank never changes the semantic tape.

     theorem unboundedStep_interpret (A : Alphabet S Γ) (M : Machine Q Γ)
         {c d : Tape (S := S) (Γ := Γ) (Q := Q)} (h : UnboundedStep A M c d) :
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Alphabet, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Machine, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.UnboundedStep

108. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.tapeRun_interpret line 1245
109. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.unboundedRun_interpret line 1250
110. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.semantic_deterministic line 1255
111. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.halted_interpret line 1259
112. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.halted_quota_unique line 1269

     Source documentation

     Halts with different finite quotas represent the same semantic output. In particular a workspace edge can neither invent a halt nor alter one.

     theorem halted_quota_unique (A : Alphabet S Γ) (M : Machine Q Γ)
         {start c d : Tape (S := S) (Γ := Γ) (Q := Q)} (n : ℕ)
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Alphabet, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Machine, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

113. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.accepting_after line 1288

     Source documentation

     An accepting terminal cannot be bypassed by any other finite forward path.

     theorem accepting_after
         {v s w : Scan.Sector (Head S Q) (Base S) (Tag S Γ)}
         (hs : ReflTransGen (Scan.Step (table A M)) v s)
         (hw : ReflTransGen (Scan.Step (table A M)) v w) (hq : w.head = .ok) :
         ReflTransGen (Scan.Step (table A M)) s w := by
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Head, OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table

114. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.readout_sound line 1301

     Source documentation

     Soundness of the output scans, under the literal decoding convention of the compiled alphabet. Both the first blank and the anchor quota are forced; the result is not an arbitrary truncation of a workspace string.

     theorem readout_sound
         (hdecode : ∀ g a, A.output g = some a → g = A.input a)
         (remaining : List Γ) (cells : Cells S Γ) (done : List Γ) (old : List S) (n : ℕ)
         (hw : workView cells = done.map (true,·) ++ remaining.map (false,·))
         (ha : anchorView cells = old.map some ++ List.replicate n none)
         {v : Scan.Sector (Head S Q) (Base S) (Tag S Γ)}
         (hv : ReflTransGen (Scan.Step (table A M)) ⟨[],.scan .readout,cells,true,true⟩ v)
         (hq : v.head = .ok) :
         ∃ out tail result, remaining = out.map A.input ++ A.blank::tail ∧ out.length ≤ n ∧
           v = ⟨result.reverse,.ok,[],true,true⟩ ∧
           anchorView result = (old ++ out).map some ++ List.replicate (n-out.length) none := by
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.workView, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.anchorView, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Head, OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table

115. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.semanticContent line 1349

     Source documentation

     The whole semantic tape, read in physical order starting at cell zero.

     def semanticContent (c : SemanticTape Γ Q) : Stream' Γ :=
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.SemanticTape

116. def OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.SemanticReturns line 1353

     Source documentation

     Standard literal, first-blank-delimited machine output.

     def SemanticReturns (c : SemanticTape Γ Q) (w : List S) : Prop :=
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.SemanticTape

117. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.returns_interpret line 1356
118. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.input_injective line 1364
119. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.delimited_prefix_unique line 1371

     Source documentation

     The input alphabet excludes the delimiter, so two literal returned prefixes of the same infinite tape must be the same list, including empty output.

     theorem delimited_prefix_unique (x y : List S) (r s : Stream' Γ)
         (h : Stream'.appendStream' (x.map A.input) (Stream'.cons A.blank r) =
           Stream'.appendStream' (y.map A.input) (Stream'.cons A.blank s)) : x = y := by
     …

120. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.semanticReturns_unique line 1395
121. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.returned_quota_unique line 1404

     Source documentation

     The output of any bounded accepting computation agrees with the output of a genuine unbounded halt, whenever both are expressed in the literal input alphabet. This compares different quotas without comparing their padding.

     theorem returned_quota_unique (M : Machine Q Γ)
         {start c d : Tape (S := S) (Γ := Γ) (Q := Q)} (n : ℕ)
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Machine, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

122. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.haltSector_readout line 1421
123. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.tapeRun_tags line 1432
124. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.simulation_sound_sufficient line 1443

     Source documentation

     Exact soundness from the fresh validated handoff, with a positive spare workspace quota. Arbitrary successes are actual halts returning exactly the output marks that cleanup will retain.

     theorem simulation_sound_sufficient
         (hdecode : ∀ g a, A.output g = some a → g = A.input a)
         (x y : List S) (n : ℕ)
         {v : Scan.Sector (Head S Q) (Base S) (Tag S Γ)}
         (hv : ReflTransGen (Scan.Step (table A M))
           ⟨(body A [] x [] y [] (x.length+y.length+n+1)).reverse,.start,[],true,true⟩ v)
         (hq : v.head = .ok) :
         ∃ c out result,
           ReflTransGen (TapeStep M) (pad A (initialTape A M (x++y)) (n+1)) c ∧
           Halted A M c ∧ Returns A c out ∧ out.length ≤ x.length+y.length ∧
           v = ⟨result.reverse,.ok,[],true,true⟩ ∧
           anchorView result = out.map some ++ List.replicate (x.length+y.length-out.length) none := by
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Head, OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.body, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.TapeStep, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pad, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.initialTape, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Halted, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Returns, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.anchorView

125. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pass_fill_bareD line 1477
126. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pass_spare_D line 1478
127. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.scan_exhausted line 1480
128. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.fill_no_space line 1489
129. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.copy_no_space line 1497

     Source documentation

     Zero spare workspace is a genuine rejection even for empty input.

     theorem copy_no_space (xp xs yp ys w : List S) :
         Rejects A M ⟨[],.scan .input,body A xp xs yp ys w 0,true,true⟩ := by
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Rejects, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.body

130. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.copy_insufficient line 1549

     Source documentation

     A quota no larger than the unread input rejects: there must be space for every copied letter and also the spare blank tested before running.

     theorem copy_insufficient (xp xs yp ys w : List S) (n : ℕ)
         (hn : n ≤ xs.length+ys.length) :
         Rejects A M ⟨[],.scan .input,body A xp xs yp ys w n,true,true⟩ := by
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Rejects, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.body

131. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.simulation_insufficient line 1568

     Source documentation

     Insufficient quota cannot give an accepting computation from a clean post-validator handoff, including the zero-workspace and empty-input cases.

     theorem simulation_insufficient (x y : List S) (s : ℕ) (hs : s ≤ x.length+y.length) :
         Rejects A M ⟨(body A [] x [] y [] s).reverse,.start,[],true,true⟩ :=
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Rejects, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.body

132. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.simulation_sound line 1575

     Source documentation

     Soundness for every clean quota, without a promise that enough was inserted. All accepting paths return the genuine first-blank-delimited machine output, in input order and within the anchor length bound.

     theorem simulation_sound
         (hdecode : ∀ g a, A.output g = some a → g = A.input a)
         (x y : List S) (s : ℕ)
         {v : Scan.Sector (Head S Q) (Base S) (Tag S Γ)}
         (hv : ReflTransGen (Scan.Step (table A M))
           ⟨(body A [] x [] y [] s).reverse,.start,[],true,true⟩ v)
         (hq : v.head = .ok) :
         ∃ n c out result, s = x.length+y.length+n+1 ∧
           ReflTransGen (TapeStep M) (pad A (initialTape A M (x++y)) (n+1)) c ∧
           Halted A M c ∧ Returns A c out ∧ out.length ≤ x.length+y.length ∧
           v = ⟨result.reverse,.ok,[],true,true⟩ ∧
           anchorView result = out.map some ++ List.replicate (x.length+y.length-out.length) none := by
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Head, OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.body, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.TapeStep, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pad, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.initialTape, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Halted, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Returns, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.anchorView