Restorable parking for copy-on-write overlay execution

This module states the runner interface used to preserve branch-local compressed accumulators. It intentionally contains no constructor dispatch.

The nonempty adjacent list head :: overlayTail is private to the active branch. word begins the sibling-shared protected suffix. A successful run erases every private overlay token and leaves the protected suffix in its existing used form.

structure IndexedGrammar.Aho.OverlayRestoreData {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) (overlay : List (ScheduleIndex g input)) (baseBlocks : List (List g.flag)) (baseOwners : List (Fin (10 * input.length))) : Type

Restoration data carried only while a copy-on-write overlay is active.

restore is the nonparking ticket displaced when the protected base head was parked. It is reserved either by remaining absent from the live ticket image or by being carried by a private overlay index. Its semantic owner is tracked at a depth inside (or exactly at the lower boundary of) the private overlay prefix. This is the information needed to make it a valid residual depth-zero base ticket when the last private block is erased.

• marker : Fin (10 * input.length)
• base_head : ∃ (block : List g.flag) (tailBlocks : List (List g.flag)) (tailOwners : List (Fin (10 * input.length))), baseBlocks = block :: tailBlocks ∧ baseOwners = self.marker :: tailOwners
• parkingAtOrBelow : resources.tickets.ParkingAtOrBelow resources.window
• marker_live : self.marker ∈ cursor.indexOwners
• marker_ticket : resources.tickets.ticketOf self.marker = resources.window.parkingTicket
• restore : IndexTicket input
• restore_nonparking : self.restore.Nonparking
• restore_not_scratch (hinput : 0 < input.length) : self.restore ≠ IndexTicket.scratch hinput
• restore_not_transient (hinput : 0 < input.length) : self.restore ≠ IndexTicket.transient hinput
• restore_outside_primary : OutsideProductiveWindow resources.window self.restore.semanticOwner
• available : self.restore ∉ cursor.indexTickets resources.tickets.ticketOf ∨ ∃ idx ∈ overlay, resources.tickets.ticketOf idx.owner = self.restore
• depth : ℕ
• depth_le : self.depth ≤ (ScheduleOverlay.flags overlay []).length
• aligned : (∃ (hd : self.depth ∈ parse.eventDepths), self.restore.semanticOwner = resources.window.shadowEventOwner self.depth hd) ∨ OutsideShadowWindow resources.window self.restore.semanticOwner

inductive IndexedGrammar.Aho.OverlayParkingContext {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) (overlay : List (ScheduleIndex g input)) (baseBlocks : List (List g.flag)) (baseOwners : List (Fin (10 * input.length))) : Type

Parking state for an active overlay. Strict mode needs no restoration metadata. Attached mode records exactly how to restore the parked protected base before leaving overlay mode.

• strict {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} {overlay : List (ScheduleIndex g input)} {baseBlocks : List (List g.flag)} {baseOwners : List (Fin (10 * input.length))} (below : resources.tickets.ParkingBelow resources.window) : OverlayParkingContext resources overlay baseBlocks baseOwners
• attached {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} {overlay : List (ScheduleIndex g input)} {baseBlocks : List (List g.flag)} {baseOwners : List (Fin (10 * input.length))} (restore : OverlayRestoreData resources overlay baseBlocks baseOwners) : OverlayParkingContext resources overlay baseBlocks baseOwners

def IndexedGrammar.Aho.OverlayScheduleRun {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {stack : List g.flag} {w : List T} (parse : g.NFParse A stack w) : Prop

Resource-aware copy-on-write overlay execution.

The structural recursion intended for this interface is:

• livePushCompress replaces head through AdjacentOverlayLayout.replaceHead;
• livePushFresh conses a new private head through AdjacentOverlayLayout.push;
• adjacent atomic pop erases head and resumes at overlayTail via AdjacentOverlayLayout.tail;
• a binary fork seals the whole overlay with AdjacentOverlayLayout.toProtected, after which the already-certified protected runner may share it between both children.

Equations

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

def 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) : Prop

The sound mutual scheduler target. Ordinary and copy-on-write overlay execution are proved together by strong recursion on parse size.

Equations

• IndexedGrammar.Aho.CompleteScheduleRuns parse = (IndexedGrammar.Aho.OrdinaryScheduleRuns parse ∧ IndexedGrammar.Aho.OverlayScheduleRun parse)