OAI/Computability/FiniteCompiler/Validator.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Finite tape validation, scan reversal, and bounded cleanup.

  1. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Head line 15

    Source documentation

    The validator states I,J,J',N,V and its fresh machine handoff.

    inductive Head
  | initial | left | right | workspace | suffix | start
  deriving DecidableEq

/-- A cell includes every tag field, even unused ones. -/

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.cell

  2. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Cell line 20

    Source documentation

    A cell includes every tag field, even unused ones.

    abbrev Cell (S Γ : Type*) := Base S × Tag S Γ

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

  3. def OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.cell line 22
  4. structure OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Sector line 27

    Source documentation

    A headed sector in zipper notation. The left list is in reverse order, so its head is exactly the cell adjacent to the validator.

    structure Sector (S Γ : Type*) where
…
  5. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Step line 37

    Source documentation

    Literal internal equations compiler-validation, oriented as in the source. There is no entry from P and no transition from the machine back here.

    inductive Step {S Γ : Type*} (blank : Γ) : Sector S Γ → Sector S Γ → Prop
  | initial_workspace (l r : List (Cell S Γ)) (lb rb : Bool) :
      Step blank ⟨.initial, cell blank .workspace :: l, r, lb, rb⟩
        ⟨.initial, l, cell blank .workspace :: r, lb, rb⟩
  | initial_cut (l r : List (Cell S Γ)) (lb rb : Bool) :
      Step blank ⟨.initial, cell blank .cutC :: l, r, lb, rb⟩
        ⟨.left, l, cell blank .cutC :: r, lb, rb⟩
  | left_anchor (a : S) (l r : List (Cell S Γ)) (lb rb : Bool) :
      Step blank ⟨.left, cell blank (.anchor a) :: l, r, lb, rb⟩
        ⟨.left, l, cell blank (.anchor a) :: r, lb, rb⟩
  | left_boundary (r : List (Cell S Γ)) (rb : Bool) :
      Step blank ⟨.left, [], r, true, rb⟩ ⟨.right, [], r, true, rb⟩
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Cell, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.cell

  6. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.step_deterministic line 67
  7. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.step_leftUnique line 73

    Source documentation

    Validator reverse determinism, not asserted for machine phases.

    theorem step_leftUnique {S Γ : Type*} (blank : Γ) :
    Relator.LeftUnique (@Step S Γ blank) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Step

  8. def OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Entry line 79

    Source documentation

    An entry has clean D immediately right of its I head.

    def Entry {S Γ : Type*} (blank : Γ) (s : Sector S Γ) : Prop :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Sector

  9. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.entry_no_predecessor line 82
  10. def OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.skeleton line 89

    Source documentation

    Ordered cells and both flags are preserved by every internal validator step.

    def skeleton {S Γ : Type*} (s : Sector S Γ) :
    List (Cell S Γ) × Bool × Bool :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Cell

  11. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.step_skeleton line 93
  12. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.reaches_skeleton line 97
  13. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Anchors line 107

    Source documentation

    Exact clean-anchor language; dirty tags are not accepted.

    inductive Anchors : List (Cell S Γ) → Prop
  | nil : Anchors []
  | cons (a : S) {l} : Anchors l → Anchors (cell blank (.anchor a) :: l)

/-- The right suffix tested from N: clean workspace, D, then clean anchors. -/

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Cell, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.cell, OAI.FiniteAlgebraicEnvelopes.Compiler.clean

  14. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Tail line 112

    Source documentation

    The right suffix tested from N: clean workspace, D, then clean anchors.

    inductive Tail : List (Cell S Γ) → Prop
  | cut {l} : Anchors blank l → Tail (cell blank .cutD :: l)
  | work {l} : Tail l → Tail (cell blank .workspace :: l)

/-- The right suffix tested from J': anchors, C, workspace, D, anchors. -/

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Cell, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Anchors, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.cell

  15. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Body line 117

    Source documentation

    The right suffix tested from J': anchors, C, workspace, D, anchors.

    inductive Body : List (Cell S Γ) → Prop
  | cut {l} : Tail blank l → Body (cell blank .cutC :: l)
  | anchor (a : S) {l} : Body l → Body (cell blank (.anchor a) :: l)

/-- The reversed left side tested from I: workspace, C, then anchors. -/

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Cell, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Tail, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.cell

  16. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Left line 122

    Source documentation

    The reversed left side tested from I: workspace, C, then anchors.

    inductive Left : List (Cell S Γ) → Prop
  | cut {l} : Anchors blank l → Left (cell blank .cutC :: l)
  | work {l} : Left l → Left (cell blank .workspace :: l)

/-- Necessary future checks at each phase. Already-scanned cells need not be
    constrained: backwards propagation recovers exactly the checks made. -/

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Cell, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Anchors, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.cell

  17. def OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Ready line 128

    Source documentation

    Necessary future checks at each phase. Already-scanned cells need not be constrained: backwards propagation recovers exactly the checks made.

    def Ready (s : Sector S Γ) : Prop :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Sector

  18. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.ready_predecessor line 139
  19. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.reaches_ready line 176
  20. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.anchors_iff line 182
  21. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.left_iff line 196
  22. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.passing_entry line 217

    Source documentation

    Every entry which reaches handoff has the FULL clean form in the manuscript: both boundaries, all clean tags, anchors on each side, and one quota. In particular this is not a cleanliness assumption on the input.

    theorem passing_entry {a b : Sector S Γ} (ha : Entry blank a)
    (hab : ReflTransGen (Step blank) a b) (hb : b.head = .start) :
    ∃ (x y : List S) (s : ℕ), a =
      ⟨.initial, List.replicate s (cell blank .workspace) ++
        cell blank .cutC :: (x.map (fun c => cell blank (.anchor c))).reverse,
        cell blank .cutD :: y.map (fun c => cell blank (.anchor c)), true, true⟩ := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Entry, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.cell

  23. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.initial_workspaces line 238
  24. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.left_anchors line 251
  25. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.right_anchors line 262
  26. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.workspace_many line 273
  27. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.suffix_anchors line 286
  28. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.clean_entry_reaches line 299

    Source documentation

    Conversely every full clean entry passes the validator, with all cells left of the head at the handoff to the simulated program.

    theorem clean_entry_reaches (x y : List S) (s : ℕ) :
    ReflTransGen (Step blank)
      ⟨.initial, List.replicate s (cell blank .workspace) ++
        cell blank .cutC :: (x.map (fun a => cell blank (.anchor a))).reverse,
        cell blank .cutD :: y.map (fun a => cell blank (.anchor a)), true, true⟩
      ⟨.start, (y.map (fun a => cell blank (.anchor a))).reverse ++
        cell blank .cutD :: (List.replicate s (cell blank .workspace) ++
        cell blank .cutC :: (x.map (fun a => cell blank (.anchor a))).reverse),
        [], true, true⟩ := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.cell

  29. def OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.measure line 329

    Source documentation

    A strictly decreasing validator measure, valid for every dirty sector.

    def measure (s : Sector S Γ) : ℕ :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Sector

  30. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.measure_decreases line 339
  31. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.source_eq_of_reaches line 350

    Source documentation

    A source vertex cannot be reached from a different vertex.

    theorem source_eq_of_reaches {a b : α} (hb : ∀ c, ¬ r c b)
    (hab : ReflTransGen r a b) : a = b := by
…
  32. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.sources_unique_of_join line 357

    Source documentation

    In a reverse-deterministic graph, two sources reaching the same vertex agree.

    theorem sources_unique_of_join (hr : Relator.LeftUnique r) {a b c : α}
    (ha : ∀ x, ¬ r x a) (hb : ∀ x, ¬ r x b)
    (hac : ReflTransGen r a c) (hbc : ReflTransGen r b c) : a = b := by
…
  33. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.entries_unique line 376
  34. def OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.baseSkeleton line 383

    Source documentation

    The machine may alter tags but never these ordered bases or outer flags.

    def baseSkeleton (s : Sector S Γ) : List (Base S) × Bool × Bool :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Base

  35. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.clean_anchors line 386
  36. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.clean_left line 392
  37. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.clean_tail line 398
  38. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.cutD_not_mem_left line 404
  39. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.passing_entries_unique line 411

    Source documentation

    Passing entries are determined by their invariant base sequence, with no injectivity hypothesis on the subsequent simulated-machine transitions.

    theorem passing_entries_unique {a b : Sector S Γ}
    (ha : Entry blank a) (hb : Entry blank b)
    (hra : Ready blank a) (hrb : Ready blank b)
    (hs : baseSkeleton a = baseSkeleton b) : a = b := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Entry, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Ready, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.baseSkeleton

  40. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.Cfg line 445
  41. def OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.Active line 449

    Source documentation

    Only the fresh handoff and machine configurations participate in simulation; in particular there is no return to I,J,J',N,V.

    def Active : Cfg S Γ M → Prop
  | .inl v => v.head = .start
  | .inr _ => True

/-- The internal graph consists of literal validator equations and simulator
    edges. These edges contain neither quota insertion nor exit to cleanup. -/

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.Cfg

  42. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.Step line 455

    Source documentation

    The internal graph consists of literal validator equations and simulator edges. These edges contain neither quota insertion nor exit to cleanup.

    inductive Step (r : Cfg S Γ M → Cfg S Γ M → Prop) :
    Cfg S Γ M → Cfg S Γ M → Prop
  | validator {v w} : Validator.Step blank v w → Step r (.inl v) (.inl w)
  | machine {a b} : Active a → Active b → r a b → Step r a b

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.Cfg, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.Active

  43. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.validator_not_start line 460
  44. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.deterministic line 464
  45. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.path_decomposition line 479

    Source documentation

    A path starting in the validator either stays there, or first reaches its fresh handoff. This explicitly excludes a dirty bypass of validation.

    theorem path_decomposition {r : Cfg S Γ M → Cfg S Γ M → Prop}
    {a : Sector S Γ} {b : Cfg S Γ M} (h : ReflTransGen (Step blank r) (.inl a) b) :
    (∃ v, b = .inl v ∧ ReflTransGen (Validator.Step blank) a v) ∨
    ∃ v, ReflTransGen (Validator.Step blank) a v ∧ v.head = .start := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.Cfg, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Step

  46. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.reaches_active line 492
  47. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.path_to_validator line 502

    Source documentation

    Pulling a path back from a non-handoff validator configuration never encounters a simulator edge.

    theorem path_to_validator {r : Cfg S Γ M → Cfg S Γ M → Prop}
    {a c : Cfg S Γ M} (h : ReflTransGen (Step blank r) a c)
    {b : Sector S Γ} (hc : c = .inl b) (hb : b.head ≠ .start) :
    ∃ v, a = .inl v ∧ ReflTransGen (Validator.Step blank) v b := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.Cfg, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Step

  48. def OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.baseSkeleton line 518
  49. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.step_bases line 522
  50. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.connected_bases line 532
  51. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.entries_unique line 544

    Source documentation

    Entry uniqueness survives arbitrary reverse branching in the simulated machine. This is source Lemma compiler-components on all dirty sectors.

    theorem entries_unique {r : Cfg S Γ M → Cfg S Γ M → Prop}
    (hdet : Relator.RightUnique r)
    (hbase : ∀ a b, r a b → baseSkeleton bases a = baseSkeleton bases b)
    {a b : Sector S Γ} (ha : Entry blank a) (hb : Entry blank b)
    (hab : EqvGen (Step blank r) (.inl a) (.inl b)) : a = b := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.Cfg, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.baseSkeleton, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Entry, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Extended.Step

  52. structure OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector line 579

    Source documentation

    A list zipper for the same finite-scan semantics. Left cells are nearest first. This representation permits induction on literal scan paths.

    structure Sector (Head Base Tag : Type*) where
…

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

  53. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.step line 589
  54. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step line 604
  55. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.deterministic line 606
  56. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.baseSkeleton line 610
  57. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.step_skeleton line 613