LanglibResource-pool surgery for Aho's compressed scheduler #
Fresh compressed blocks move one owner from the free suffix into the cursor's persistent-index owners. Erasing a private overlay block performs the inverse operation. These lemmas express both updates as permutations, keeping the duplicate-freedom proof independent of cursor syntax.
def
IndexedGrammar.Aho.ShadowOwnerLedger.ofGeneric
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{window : ProductiveOwnerWindow parse}
{cursor : ScheduleCursor g input}
(pool : IndexOwnerPool cursor)
(ledger : ScheduleOwnerLedger parse window cursor)
:
ShadowOwnerLedger parse window cursor
Build the shadow ledger canonically when the physical owner pool is wholly outside every semantic shadow window.
Equations
Instances For
structure
IndexedGrammar.Aho.ScheduleRunResources
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
(parse : g.NFParse A stack w)
(pre : List T)
(cursor : ScheduleCursor g input)
:
Resources carried by one mutually recursive runner call. charged counts productive
events of the active task already represented by persistent blocks. The remaining events fit
in the free-owner pool. task_locality reserves the interior of the active yield interval for
the child tasks introduced by its binary nodes.
- pool : IndexOwnerPool cursor
- tickets : IndexTicketLedger cursor
An injective logical ticket assignment for the generic physical owners.
- window : ProductiveOwnerWindow parse
- parkingAtOrBelow : self.tickets.ParkingAtOrBelow self.window
Parking tickets in ordinary resources never lie above the current root-relative productive-window base. Protected mode strengthens this to a strict bound, while an active copy-on-write overlay may occupy the base slot itself.
- ownerLedger : ScheduleOwnerLedger parse self.window cursor
- ticketOwnerLedger : IndexTicketLedger.SemanticScheduleOwnerLedger parse self.window self.tickets
Productive-event provenance, interpreted on the logical-ticket projection of
cursor. - ticket_active_eq : self.ticketOwnerLedger.active = self.tickets.semanticOwners self.ownerLedger.active
The projected active list is aligned with the physical active-owner list.
The full aligned shadow context. It may extend the primary active prefix with parked lower blocks which remain on the tape while a structural child runs only that prefix.
- ticketShadowOwners_nodup : self.ticketShadowOwners.Nodup
- ticketShadowLedger : IndexTicketLedger.SemanticShadowOwnerLedger parse self.window self.tickets
Shadow-start provenance on the same logical-ticket projection.
- ticket_shadow_active_eq : self.ticketShadowLedger.active = self.tickets.semanticOwners self.ticketShadowOwners
- ticketShadowLayout : IndexTicketLedger.ShadowTicketLayout parse self.window self.tickets self.ticketShadowBlocks self.ticketShadowOwners
- shadowLedger : ShadowOwnerLedger parse self.window cursor
- charged : ℕ
Instances For
def
IndexedGrammar.Aho.ScheduleRunResources.TicketShadowContextExtends
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{pre : List T}
{cursor : ScheduleCursor g input}
(resources : ScheduleRunResources parse pre cursor)
(blocks : List (List g.flag))
(owners : List (Fin (10 * input.length)))
:
The selected primary block context is a prefix of the full projected shadow context. The suffix is parked on the tape and remains visible to shadow-ticket freshness.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
IndexedGrammar.Aho.ScheduleRunResources.free_ne_nil_of_index_count_lt
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{pre : List T}
{cursor : ScheduleCursor g input}
(resources : ScheduleRunResources parse pre cursor)
(hcapacity : cursor.indexOwners.length < 6 * input.length)
:
An explicit strict index bound below the exhaustive 6|input| owner pool supplies a free
physical owner.
theorem
IndexedGrammar.Aho.ScheduleRunResources.active_subset_indexOwners
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{pre : List T}
{cursor : ScheduleCursor g input}
(resources : ScheduleRunResources parse pre cursor)
:
Every active owner is physically present among the cursor's persistent indices.
def
IndexedGrammar.Aho.ScheduleRunResources.genericShadowStartLayout
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{pre : List T}
{cursor : ScheduleCursor g input}
(resources : ScheduleRunResources parse pre cursor)
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
(hactive : resources.ownerLedger.active = owners)
(hlen : owners.length = blocks.length)
(hne : ∀ block ∈ blocks, block ≠ [])
:
ShadowStartLayout parse resources.window blocks owners
Pooled owners all lie beyond the semantic shadow window, so any block partition whose owners are active admits an all-outside shadow layout.
Equations
- ⋯ = ⋯
Instances For
def
IndexedGrammar.Aho.PlainScheduleRun
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{A : g.nt}
{stack : List g.flag}
{w : List T}
(parse : g.NFParse A stack w)
:
Resource-aware plain runner mode. Both endpoints are genuine invariant-carrying scheduler states, so every intermediate node of the result is automatically within the linear bound.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
IndexedGrammar.Aho.ProtectedScheduleRun
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{A : g.nt}
{stack : List g.flag}
{w : List T}
(parse : g.NFParse A stack w)
:
Resource-aware protected-block runner mode.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
IndexedGrammar.Aho.OrdinaryScheduleRuns
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{A : g.nt}
{stack : List g.flag}
{w : List T}
(parse : g.NFParse A stack w)
:
The two ordinary strict-entry runners used by the window-parking recursion.
Equations
Instances For
theorem
IndexedGrammar.Aho.IndexOwnerPool.head_fresh
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(pool : IndexOwnerPool cursor)
{owner : Fin (10 * input.length)}
{rest : List (Fin (10 * input.length))}
(hfree : pool.free = owner :: rest)
:
owner ∉ cursor.indexOwners
The head of a free-owner pool cannot already own a persistent index.
def
IndexedGrammar.Aho.IndexOwnerPool.allocate
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(pool : IndexOwnerPool old)
(owner : Fin (10 * input.length))
(rest : List (Fin (10 * input.length)))
(hfree : pool.free = owner :: rest)
(hindices : new.indexOwners.Perm (owner :: old.indexOwners))
:
IndexOwnerPool new
Allocate the head free owner after a cursor change which inserts exactly that owner.
Instances For
@[simp]
theorem
IndexedGrammar.Aho.IndexOwnerPool.allocate_free
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(pool : IndexOwnerPool old)
(owner : Fin (10 * input.length))
(rest : List (Fin (10 * input.length)))
(hfree : pool.free = owner :: rest)
(hindices : new.indexOwners.Perm (owner :: old.indexOwners))
:
def
IndexedGrammar.Aho.IndexOwnerPool.allocatePerm
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(pool : IndexOwnerPool old)
(owner : Fin (10 * input.length))
(rest : List (Fin (10 * input.length)))
(hfree : pool.free.Perm (owner :: rest))
(hindices : new.indexOwners.Perm (owner :: old.indexOwners))
:
IndexOwnerPool new
Allocate an explicitly selected free owner. Unlike allocate, the owner need not be the
head of the current free list; the remaining pool is supplied up to permutation.
Equations
- pool.allocatePerm owner rest hfree hindices = { free := rest, all_nodup := ⋯, all_perm := ⋯ }
Instances For
@[simp]
theorem
IndexedGrammar.Aho.IndexOwnerPool.allocatePerm_free
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(pool : IndexOwnerPool old)
(owner : Fin (10 * input.length))
(rest : List (Fin (10 * input.length)))
(hfree : pool.free.Perm (owner :: rest))
(hindices : new.indexOwners.Perm (owner :: old.indexOwners))
:
def
IndexedGrammar.Aho.IndexOwnerPool.allocateMember
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(pool : IndexOwnerPool old)
(owner : Fin (10 * input.length))
(hfree : owner ∈ pool.free)
(hindices : new.indexOwners.Perm (owner :: old.indexOwners))
:
IndexOwnerPool new
Allocate an arbitrary known member of the exhaustive free pool.
Equations
- pool.allocateMember owner hfree hindices = pool.allocatePerm owner (pool.free.erase owner) ⋯ hindices
Instances For
@[simp]
theorem
IndexedGrammar.Aho.IndexOwnerPool.allocateMember_free
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(pool : IndexOwnerPool old)
(owner : Fin (10 * input.length))
(hfree : owner ∈ pool.free)
(hindices : new.indexOwners.Perm (owner :: old.indexOwners))
:
def
IndexedGrammar.Aho.IndexOwnerPool.release
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(pool : IndexOwnerPool old)
(owner : Fin (10 * input.length))
(hindices : old.indexOwners.Perm (owner :: new.indexOwners))
:
IndexOwnerPool new
Return an erased owner to the free pool after the cursor removes exactly that index.
Equations
Instances For
@[simp]
theorem
IndexedGrammar.Aho.IndexOwnerPool.release_free
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(pool : IndexOwnerPool old)
(owner : Fin (10 * input.length))
(hindices : old.indexOwners.Perm (owner :: new.indexOwners))
:
def
IndexedGrammar.Aho.ScheduleRunResources.releaseOwned
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A B : g.nt}
{stack residualStack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{residual : g.NFParse B residualStack w}
{pre : List T}
{old new : ScheduleCursor g input}
(resources : ScheduleRunResources parse pre old)
(owner : Fin (10 * input.length))
(hindices : old.indexOwners.Perm (owner :: new.indexOwners))
(htasks : new.taskOwners = old.taskOwners)
(hproductive : residual.productiveCount = parse.productiveCount)
(ownerLedger : ScheduleOwnerLedger residual (resources.window.transport hproductive) new)
(ticketOwnerLedger :
IndexTicketLedger.SemanticScheduleOwnerLedger residual (resources.window.transport hproductive)
(resources.tickets.release owner hindices))
(ticket_active_eq :
ticketOwnerLedger.active = (resources.tickets.release owner hindices).semanticOwners ownerLedger.active)
(ticketShadowBlocks : List (List g.flag))
(ticketShadowOwners : List (Fin (10 * input.length)))
(ticketShadowOwners_subset : ticketShadowOwners ⊆ new.indexOwners)
(ticketShadowOwners_nodup : ticketShadowOwners.Nodup)
(ticketShadowLedger :
ShadowOwnerLedger residual (resources.window.transport hproductive)
(resources.tickets.release owner hindices).semanticCursor)
(ticket_shadow_active_eq :
ticketShadowLedger.active = (resources.tickets.release owner hindices).semanticOwners ticketShadowOwners)
(ticketShadowLayout :
IndexTicketLedger.ShadowTicketLayout residual (resources.window.transport hproductive)
(resources.tickets.release owner hindices) ticketShadowBlocks ticketShadowOwners)
(shadowLedger : ShadowOwnerLedger residual (resources.window.transport hproductive) new)
(shadow_active_eq : shadowLedger.active = ownerLedger.active)
(hcharged : 0 < resources.charged)
:
ScheduleRunResources residual pre new
Release a private overlay owner before running a same-yield residual parse. One charged owner becomes one free owner, so the productive-event credit is preserved exactly.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ScheduleRunResources.releaseOwned_charged
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A B : g.nt}
{stack residualStack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{residual : g.NFParse B residualStack w}
{pre : List T}
{old new : ScheduleCursor g input}
(resources : ScheduleRunResources parse pre old)
(owner : Fin (10 * input.length))
(hindices : old.indexOwners.Perm (owner :: new.indexOwners))
(htasks : new.taskOwners = old.taskOwners)
(hproductive : residual.productiveCount = parse.productiveCount)
(ownerLedger : ScheduleOwnerLedger residual (resources.window.transport hproductive) new)
(ticketOwnerLedger :
IndexTicketLedger.SemanticScheduleOwnerLedger residual (resources.window.transport hproductive)
(resources.tickets.release owner hindices))
(ticket_active_eq :
ticketOwnerLedger.active = (resources.tickets.release owner hindices).semanticOwners ownerLedger.active)
(ticketShadowBlocks : List (List g.flag))
(ticketShadowOwners : List (Fin (10 * input.length)))
(ticketShadowOwners_subset : ticketShadowOwners ⊆ new.indexOwners)
(ticketShadowOwners_nodup : ticketShadowOwners.Nodup)
(ticketShadowLedger :
IndexTicketLedger.SemanticShadowOwnerLedger residual (resources.window.transport hproductive)
(resources.tickets.release owner hindices))
(ticket_shadow_active_eq :
ticketShadowLedger.active = (resources.tickets.release owner hindices).semanticOwners ticketShadowOwners)
(ticketShadowLayout :
IndexTicketLedger.ShadowTicketLayout residual (resources.window.transport hproductive)
(resources.tickets.release owner hindices) ticketShadowBlocks ticketShadowOwners)
(shadowLedger : ShadowOwnerLedger residual (resources.window.transport hproductive) new)
(shadow_active_eq : shadowLedger.active = ownerLedger.active)
(hcharged : 0 < resources.charged)
:
(resources.releaseOwned owner hindices htasks hproductive ownerLedger ticketOwnerLedger ticket_active_eq
ticketShadowBlocks ticketShadowOwners ticketShadowOwners_subset ticketShadowOwners_nodup ticketShadowLedger
ticket_shadow_active_eq ticketShadowLayout shadowLedger shadow_active_eq hcharged).charged = resources.charged - 1
@[simp]
theorem
IndexedGrammar.Aho.ScheduleRunResources.releaseOwned_free
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A B : g.nt}
{stack residualStack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{residual : g.NFParse B residualStack w}
{pre : List T}
{old new : ScheduleCursor g input}
(resources : ScheduleRunResources parse pre old)
(owner : Fin (10 * input.length))
(hindices : old.indexOwners.Perm (owner :: new.indexOwners))
(htasks : new.taskOwners = old.taskOwners)
(hproductive : residual.productiveCount = parse.productiveCount)
(ownerLedger : ScheduleOwnerLedger residual (resources.window.transport hproductive) new)
(ticketOwnerLedger :
IndexTicketLedger.SemanticScheduleOwnerLedger residual (resources.window.transport hproductive)
(resources.tickets.release owner hindices))
(ticket_active_eq :
ticketOwnerLedger.active = (resources.tickets.release owner hindices).semanticOwners ownerLedger.active)
(ticketShadowBlocks : List (List g.flag))
(ticketShadowOwners : List (Fin (10 * input.length)))
(ticketShadowOwners_subset : ticketShadowOwners ⊆ new.indexOwners)
(ticketShadowOwners_nodup : ticketShadowOwners.Nodup)
(ticketShadowLedger :
IndexTicketLedger.SemanticShadowOwnerLedger residual (resources.window.transport hproductive)
(resources.tickets.release owner hindices))
(ticket_shadow_active_eq :
ticketShadowLedger.active = (resources.tickets.release owner hindices).semanticOwners ticketShadowOwners)
(ticketShadowLayout :
IndexTicketLedger.ShadowTicketLayout residual (resources.window.transport hproductive)
(resources.tickets.release owner hindices) ticketShadowBlocks ticketShadowOwners)
(shadowLedger : ShadowOwnerLedger residual (resources.window.transport hproductive) new)
(shadow_active_eq : shadowLedger.active = ownerLedger.active)
(hcharged : 0 < resources.charged)
:
(resources.releaseOwned owner hindices htasks hproductive ownerLedger ticketOwnerLedger ticket_active_eq
ticketShadowBlocks ticketShadowOwners ticketShadowOwners_subset ticketShadowOwners_nodup ticketShadowLedger
ticket_shadow_active_eq ticketShadowLayout shadowLedger shadow_active_eq hcharged).pool.free = owner :: resources.pool.free