LanglibGhost sealing of a transient logical ticket #
An unaligned live head may temporarily use the distinguished transient ticket. At a depth-zero productive event the head can be reticketed, without a machine move, to the canonical shadow ticket at block start zero. The physical cursor, owner pool, and erased work configuration are unchanged.
This module packages the reusable lower-level part of that operation. Runner-specific code still rebuilds the two projected cursor ledgers, because its exact right-side decomposition and frame transport depend on the surrounding zipper shape.
def
IndexedGrammar.Aho.EventOwnedLayout.reownerHeadOutside
{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}
{block : List g.flag}
{blocks : List (List g.flag)}
{oldOwner newOwner : Fin (10 * input.length)}
{owners : List (Fin (10 * input.length))}
(layout : EventOwnedLayout parse window (block :: blocks) (oldOwner :: owners))
(houtside : OutsideProductiveWindow window newOwner)
:
EventOwnedLayout parse window (block :: blocks) (newOwner :: owners)
Replace the first owner by one outside the primary productive window. Every lower block classification is unchanged.
Equations
- layout.reownerHeadOutside houtside = { compatible := layout.compatible, owners_length := ⋯, endpoint_pos := ⋯, owner_at := ⋯ }
Instances For
theorem
IndexedGrammar.Aho.ShadowStartLayout.appendLeft
{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}
{blocks parkedBlocks : List (List g.flag)}
{owners parkedOwners : List (Fin (10 * input.length))}
(layout : ShadowStartLayout parse window (blocks ++ parkedBlocks) (owners ++ parkedOwners))
(hlen : owners.length = blocks.length)
:
ShadowStartLayout parse window blocks owners
Restrict a full shadow context to a known aligned prefix.
theorem
IndexedGrammar.Aho.ShadowStartLayout.pushFreshRotateHead
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]}
{rest : g.NFParse B (f :: stack) w}
{window : ProductiveOwnerWindow (NFParse.push hr hlhs hc hrhs rest)}
{block : List g.flag}
{blocks : List (List g.flag)}
{oldHead newHead : Fin (10 * input.length)}
{owners : List (Fin (10 * input.length))}
(layout : ShadowStartLayout (NFParse.push hr hlhs hc hrhs rest) window (block :: blocks) (oldHead :: owners))
(hone : 1 ∈ rest.eventDepths)
(hnew : OutsideShadowWindow window.pushChild newHead)
:
ShadowStartLayout rest window.pushChild ([f] :: block :: blocks)
(newHead :: window.pushChild.shadowEventOwner 1 hone :: owners)
Prepend a fresh singleton block after rotating the old first owner to child shadow depth one. All lower positive parent starts transport canonically one position deeper.
structure
IndexedGrammar.Aho.TicketHeadSeal
{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)
(head : Fin (10 * input.length))
(block : List g.flag)
(blocks : List (List g.flag))
(owners : List (Fin (10 * input.length)))
(hzero : 0 ∈ parse.eventDepths)
:
Result of sealing one transient active head.
- sealed : IndexTicketLedger cursor
- transient_fresh (hinput : 0 < input.length) : IndexTicket.transient hinput ∉ cursor.indexTickets self.sealed.ticketOf
- eventLayout : IndexTicketLedger.EventTicketLayout parse resources.window self.sealed (block :: blocks) (head :: owners)
- shadowLayout : IndexTicketLedger.ShadowTicketLayout parse resources.window self.sealed (block :: blocks) (head :: owners)
- fullShadowLayout : IndexTicketLedger.ShadowTicketLayout parse resources.window self.sealed resources.ticketShadowBlocks resources.ticketShadowOwners
Instances For
structure
IndexedGrammar.Aho.TicketHeadNormalization
{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)
(head : Fin (10 * input.length))
(block : List g.flag)
(blocks : List (List g.flag))
(owners : List (Fin (10 * input.length)))
:
A transient-normalized ticket view of the same physical cursor. The physical pool,
window, owner ledgers, and accounting data remain in the surrounding resources; this
package contains exactly the projected fields which may change when the head is sealed.
- tickets : IndexTicketLedger cursor
- parkingAtOrBelow : self.tickets.ParkingAtOrBelow resources.window
- ticketOwnerLedger : IndexTicketLedger.SemanticScheduleOwnerLedger parse resources.window self.tickets
- ticket_active_eq : self.ticketOwnerLedger.active = self.tickets.semanticOwners resources.ownerLedger.active
- ticketShadowLedger : IndexTicketLedger.SemanticShadowOwnerLedger parse resources.window self.tickets
- ticket_shadow_active_eq : self.ticketShadowLedger.active = self.tickets.semanticOwners resources.ticketShadowOwners
- eventLayout : IndexTicketLedger.EventTicketLayout parse resources.window self.tickets (block :: blocks) (head :: owners)
- shadowLayout : IndexTicketLedger.ShadowTicketLayout parse resources.window self.tickets (block :: blocks) (head :: owners)
- fullShadowLayout : IndexTicketLedger.ShadowTicketLayout parse resources.window self.tickets resources.ticketShadowBlocks resources.ticketShadowOwners
- head_shadow (hzero : 0 ∈ parse.eventDepths) : self.tickets.ticketOf head = resources.window.shadowEventTicket 0 hzero
- transient_fresh (hinput : 0 < input.length) : IndexTicket.transient hinput ∉ cursor.indexTickets self.tickets.ticketOf
Instances For
structure
IndexedGrammar.Aho.ActiveHeadTicketRestoration
{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}
(old : ScheduleRunResources parse pre cursor)
(head : Fin (10 * input.length))
(block : List g.flag)
(blocks : List (List g.flag))
(owners : List (Fin (10 * input.length)))
(target : IndexTicket input)
:
The complete ghost update obtained by restoring a parked active head to a fresh
nonparking ticket. Unlike TicketHeadNormalization, the restore ticket need not be the
canonical shadow at depth zero: its semantic owner may instead lie outside the residual
shadow window.
- tickets : IndexTicketLedger cursor
- parkingBelow : self.tickets.ParkingBelow old.window
- ticketOwnerLedger : IndexTicketLedger.SemanticScheduleOwnerLedger parse old.window self.tickets
- ticket_active_eq : self.ticketOwnerLedger.active = self.tickets.semanticOwners old.ownerLedger.active
- ticketShadowLedger : IndexTicketLedger.SemanticShadowOwnerLedger parse old.window self.tickets
- ticket_shadow_active_eq : self.ticketShadowLedger.active = self.tickets.semanticOwners old.ticketShadowOwners
- eventLayout : IndexTicketLedger.EventTicketLayout parse old.window self.tickets (block :: blocks) (head :: owners)
- shadowLayout : IndexTicketLedger.ShadowTicketLayout parse old.window self.tickets (block :: blocks) (head :: owners)
- fullShadowLayout : IndexTicketLedger.ShadowTicketLayout parse old.window self.tickets old.ticketShadowBlocks old.ticketShadowOwners
- transient_fresh (hinput : 0 < input.length) : IndexTicket.transient hinput ∉ cursor.indexTickets self.tickets.ticketOf
Instances For
def
IndexedGrammar.Aho.ActiveHeadTicketRestoration.resources
{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}
{old : ScheduleRunResources parse pre cursor}
{head : Fin (10 * input.length)}
{block : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
{target : IndexTicket input}
(restored : ActiveHeadTicketRestoration old head block blocks owners target)
:
ScheduleRunResources parse pre cursor
Reassemble the unchanged physical resource package around a restored ticket view.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
IndexedGrammar.Aho.TicketHeadNormalization.parkingBelow
{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}
{old : ScheduleRunResources parse pre cursor}
{head : Fin (10 * input.length)}
{block : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
(normal : TicketHeadNormalization old head block blocks owners)
(hzero : 0 ∈ parse.eventDepths)
(hbound : old.tickets.ParkingBelow old.window)
:
normal.tickets.ParkingBelow old.window
Normalizing a live head to its canonical shadow-zero ticket preserves the ordinary strict parking invariant. The normalized head is nonparking and every other live ticket is unchanged.
def
IndexedGrammar.Aho.TicketHeadNormalization.resources
{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}
{old : ScheduleRunResources parse pre cursor}
{head : Fin (10 * input.length)}
{block : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
(normal : TicketHeadNormalization old head block blocks owners)
:
ScheduleRunResources parse pre cursor
Reassemble a complete resource package after ghost-only head normalization.
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
IndexedGrammar.Aho.FreshPushHeadRotation
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]}
{rest : g.NFParse B (f :: stack) w}
{pre : List T}
{cursor : ScheduleCursor g input}
(resources : ScheduleRunResources (NFParse.push hr hlhs hc hrhs rest) pre cursor)
{head : Fin (10 * input.length)}
{block : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
(normal : TicketHeadNormalization resources head block blocks owners)
(hone : 1 ∈ rest.eventDepths)
:
Logical head alignment used immediately before a fresh unary push. The old first block will start at child depth one, while the newly allocated singleton receives the transient ticket.
- tickets : IndexTicketLedger cursor
- transient_fresh (hinput : 0 < input.length) : IndexTicket.transient hinput ∉ cursor.indexTickets self.tickets.ticketOf
Instances For
def
IndexedGrammar.Aho.ScheduleRunResources.restoreParkedActiveHead
{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)
{head : Fin (10 * input.length)}
{block : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
(hactive : resources.ownerLedger.active = head :: owners)
(hownersNodup : (head :: owners).Nodup)
(hcontext : resources.TicketShadowContextExtends (block :: blocks) (head :: owners))
(eventLayout :
IndexTicketLedger.EventTicketLayout parse resources.window resources.tickets (block :: blocks) (head :: owners))
(shadowLayout :
IndexTicketLedger.ShadowTicketLayout parse resources.window resources.tickets (block :: blocks) (head :: owners))
(hheadMem : head ∈ cursor.indexOwners)
(hheadFrameFresh : head ∉ cursor.frameOwners)
(hframeSubset : cursor.frameOwners ⊆ cursor.indexOwners)
(parking : resources.tickets.OverlayParking resources.window head)
(target : IndexTicket input)
(htargetFresh : target ∉ cursor.indexTickets resources.tickets.ticketOf)
(htargetNotScratch : ∀ (hinput : 0 < input.length), target ≠ IndexTicket.scratch hinput)
(htargetNotTransient : ∀ (hinput : 0 < input.length), target ≠ IndexTicket.transient hinput)
(htargetNonparking : target.Nonparking)
(htargetOutside : OutsideProductiveWindow resources.window target.semanticOwner)
(htargetShadow :
(∃ (hzero : 0 ∈ parse.eventDepths), target.semanticOwner = resources.window.shadowEventOwner 0 hzero) ∨ OutsideShadowWindow resources.window target.semanticOwner)
(htransientFree :
∀ (hinput : 0 < input.length), IndexTicket.transient hinput ∉ cursor.indexTickets resources.tickets.ticketOf)
:
ActiveHeadTicketRestoration resources head block blocks owners target
Reticket a parked first active block to a fresh nonparking ticket and rebuild every ticket-projected resource invariant over the unchanged physical cursor.
The restore ticket may denote either the residual depth-zero shadow owner or an owner outside the residual shadow window. Its primary interpretation must be outside the productive window; these are exactly the two layout facts needed at a singleton-overlay exit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
IndexedGrammar.Aho.ScheduleRunResources.sealTransientHead
{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)
(hinput : 0 < input.length)
{head : Fin (10 * input.length)}
{block : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
(hactive : resources.ownerLedger.active = head :: owners)
(hownersNodup : (head :: owners).Nodup)
(hcontext : resources.TicketShadowContextExtends (block :: blocks) (head :: owners))
(eventLayout :
IndexTicketLedger.EventTicketLayout parse resources.window resources.tickets (block :: blocks) (head :: owners))
(shadowLayout :
IndexTicketLedger.ShadowTicketLayout parse resources.window resources.tickets (block :: blocks) (head :: owners))
(hzero : 0 ∈ parse.eventDepths)
(hheadMem : head ∈ cursor.indexOwners)
(hfocus : List.filterMap ScheduleAtom.indexOwner? [cursor.focus] = [])
(hheadTarget : resources.tickets.ticketOf head ≠ resources.window.shadowEventTicket 0 hzero)
(htransientHead :
IndexTicket.transient hinput ∈ cursor.indexTickets resources.tickets.ticketOf →
resources.tickets.ticketOf head = IndexTicket.transient hinput)
:
TicketHeadSeal resources head block blocks owners hzero
Seal a transient logical head into the canonical shadow ticket at depth zero.
The active-list and focus hypotheses are precisely what lets the projected shadow ledger prove
whole-cursor freshness. hownersNodup is normally obtained from the surrounding
ScheduleBlockLayout; it is used only to show that reticketing the head leaves all lower owner
associations unchanged.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
IndexedGrammar.Aho.ScheduleRunResources.normalizeTransientHead
{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)
(hinput : 0 < input.length)
{head : Fin (10 * input.length)}
{block : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
(hactive : resources.ownerLedger.active = head :: owners)
(hownersNodup : (head :: owners).Nodup)
(hcontext : resources.TicketShadowContextExtends (block :: blocks) (head :: owners))
(eventLayout :
IndexTicketLedger.EventTicketLayout parse resources.window resources.tickets (block :: blocks) (head :: owners))
(hzero : 0 ∈ parse.eventDepths)
(hheadMem : head ∈ cursor.indexOwners)
(hfocus : List.filterMap ScheduleAtom.indexOwner? [cursor.focus] = [])
(hheadFrameFresh : head ∉ cursor.frameOwners)
(hframeSubset : cursor.frameOwners ⊆ cursor.indexOwners)
(htransientHead :
IndexTicket.transient hinput ∈ cursor.indexTickets resources.tickets.ticketOf →
resources.tickets.ticketOf head = IndexTicket.transient hinput)
:
TicketHeadNormalization resources head block blocks owners
Normalize the logical transient ticket at a compressed head. If the transient ticket is already absent this is the identity package; otherwise the head is sealed to shadow start zero and both projected cursor ledgers are rebuilt over the unchanged physical cursor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
IndexedGrammar.Aho.ScheduleRunResources.rotateHeadForFreshPush
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]}
{rest : g.NFParse B (f :: stack) w}
{pre : List T}
{cursor : ScheduleCursor g input}
(resources : ScheduleRunResources (NFParse.push hr hlhs hc hrhs rest) pre cursor)
{head : Fin (10 * input.length)}
{block : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
(normal : TicketHeadNormalization resources head block blocks owners)
(hinput : 0 < input.length)
(hone : 1 ∈ rest.eventDepths)
(hheadMem : head ∈ cursor.indexOwners)
(hfocus : List.filterMap ScheduleAtom.indexOwner? [cursor.focus] = [])
:
FreshPushHeadRotation resources normal hone
Move an already normalized parent head to the child depth-one shadow ticket. When the child has no depth-zero event this is the identity, because parent shadow zero transports to child shadow one. When depth zero is present, the child-one ticket is absent from the fully accounted parent shadow cursor and one ghost reticketing step performs the alignment.
Equations
- One or more equations did not get rendered due to their size.