Root invocation of Aho's invariant-carrying scheduler

This file discharges the bookkeeping which is specific to the initial parse task. Initially no productive-event owner is in use, so the complete finite carrier is the free-owner pool. Once the mutual compressed runner is supplied, its plain projection is therefore an accepting bounded run.

def IndexedGrammar.Aho.initialIndexOwnerPool {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) : IndexOwnerPool (initialScheduleCursor parse)

Initially every productive-event owner is free.

Equations

• IndexedGrammar.Aho.initialIndexOwnerPool parse = { free := IndexedGrammar.Aho.genericOwnerRange g input, all_nodup := ⋯, all_perm := ⋯ }

@[simp]

theorem IndexedGrammar.Aho.initialIndexOwnerPool_free {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) : (initialIndexOwnerPool parse).free = genericOwnerRange g input

def IndexedGrammar.Aho.initialIndexTicketLedger {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) : IndexTicketLedger (initialScheduleCursor parse)

The root cursor has no persistent owners, so its logical ticket ledger is the unique empty live assignment.

Equations

• IndexedGrammar.Aho.initialIndexTicketLedger parse = IndexedGrammar.Aho.IndexTicketLedger.ofEmpty ⋯ ⋯

theorem IndexedGrammar.Aho.initialParkingBelow {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) : (initialIndexTicketLedger parse).ParkingBelow (ProductiveOwnerWindow.root parse)

The empty root ledger satisfies the strict window-addressed parking invariant.

def IndexedGrammar.Aho.initialTicketOwnerLedger {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) : IndexTicketLedger.SemanticScheduleOwnerLedger parse (ProductiveOwnerWindow.root parse) (initialIndexTicketLedger parse)

Productive-owner provenance on the root's empty logical projection.

Equations

• IndexedGrammar.Aho.initialTicketOwnerLedger parse = id (IndexedGrammar.Aho.ScheduleOwnerLedger.root parse)

def IndexedGrammar.Aho.initialTicketShadowLedger {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) : IndexTicketLedger.SemanticShadowOwnerLedger parse (ProductiveOwnerWindow.root parse) (initialIndexTicketLedger parse)

Shadow-owner provenance on the same empty root projection.

Equations

• IndexedGrammar.Aho.initialTicketShadowLedger parse = id (IndexedGrammar.Aho.ShadowOwnerLedger.root parse)

def IndexedGrammar.Aho.initialScheduleRunResources {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) : ScheduleRunResources parse [] (initialScheduleCursor parse)

The root task begins with the exact full productive-event credit and owns the whole input interval.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

theorem IndexedGrammar.Aho.completeScheduleRuns {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {stack : List g.flag} {w : List T} (parse : g.NFParse A stack w) : CompleteScheduleRuns parse

Ordinary protected/plain execution and copy-on-write overlay execution are constructed simultaneously by strong recursion on parse node count.

theorem IndexedGrammar.Aho.parseScheduled_of_completeScheduleRuns {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) (runs : CompleteScheduleRuns parse) : ParseScheduled parse

A completed mutual compressed-runner proof supplies the ownership-preserving root schedule.

theorem IndexedGrammar.Aho.complete_bounded_of_completeScheduleRuns {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) (runs : CompleteScheduleRuns parse) : BoundedReaches g input (21 * input.length) (initialConfig g) (finalConfig g input.length)

The invariant-carrying mutual runner implies the concrete 21|w| completeness theorem.

theorem IndexedGrammar.Aho.complete_bounded {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) : BoundedReaches g input (21 * input.length) (initialConfig g) (finalConfig g input.length)

Every normal-form parse has a uniform 21|w| bounded accepting run.