Restorable parking for copy-on-write overlays

An overlay may leave the protected base block at the parking ticket of the current productive window. This is the one situation in which the ordinary strict IndexTicketLedger.ParkingBelow invariant is deliberately weakened to ParkingAtOrBelow.

OverlayParking records the exact extra information needed to undo that weakening: either the strict bound already holds, or a specified live base owner carries the unique ticket at the current base. Reticketing that owner to a nonparking ticket then restores the strict bound. The development here is ghost-only and independent of the physical overlay layout.

structure IndexedGrammar.Aho.IndexTicketLedger.OverlayParking {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} {cursor : ScheduleCursor g input} (ledger : IndexTicketLedger cursor) (window : ProductiveOwnerWindow parse) (baseOwner : Fin (10 * input.length)) : Prop

The parking invariant carried by overlay mode.

All live parking slots are at or below the current window base. If the strict bound does not already hold, baseOwner is live and identifies the owner of the canonical parking ticket at that base. Duplicate-freedom of the ticket ledger makes this owner unique.

• atOrBelow : ledger.ParkingAtOrBelow window
• strict_or_parked : ledger.ParkingBelow window ∨ baseOwner ∈ cursor.indexOwners ∧ ledger.ticketOf baseOwner = window.parkingTicket

theorem IndexedGrammar.Aho.IndexTicketLedger.OverlayParking.swapTickets_nonparking {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} {cursor : ScheduleCursor g input} {ledger : IndexTicketLedger cursor} {window : ProductiveOwnerWindow parse} {baseOwner : Fin (10 * input.length)} (parking : ledger.OverlayParking window baseOwner) (left right : IndexTicket input) (hleft : ∀ (hinput : 0 < input.length), left ≠ IndexTicket.scratch hinput) (hright : ∀ (hinput : 0 < input.length), right ≠ IndexTicket.scratch hinput) (hleftNonparking : left.Nonparking) (hrightNonparking : right.Nonparking) : (ledger.swapTickets left right hleft hright).OverlayParking window baseOwner

Swapping two nonparking tickets preserves a restorable parking marker. In the parked branch the canonical parking ticket is fixed by the swap; in the strict branch this is the ordinary strict parking preservation theorem.

theorem IndexedGrammar.Aho.IndexTicketLedger.OverlayParking.ofBelow {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} {cursor : ScheduleCursor g input} {ledger : IndexTicketLedger cursor} {window : ProductiveOwnerWindow parse} (baseOwner : Fin (10 * input.length)) (hbelow : ledger.ParkingBelow window) : ledger.OverlayParking window baseOwner

A strict parking bound is already a restorable overlay parking invariant.

theorem IndexedGrammar.Aho.IndexTicketLedger.OverlayParking.ofParked {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} {cursor : ScheduleCursor g input} {ledger : IndexTicketLedger cursor} {window : ProductiveOwnerWindow parse} {baseOwner : Fin (10 * input.length)} (hbound : ledger.ParkingAtOrBelow window) (hlive : baseOwner ∈ cursor.indexOwners) (hticket : ledger.ticketOf baseOwner = window.parkingTicket) : ledger.OverlayParking window baseOwner

A live owner carrying the current canonical parking ticket supplies the parked branch of the invariant, provided the non-strict global parking bound is known.

theorem IndexedGrammar.Aho.IndexTicketLedger.OverlayParking.owner_eq_of_parked_ticket {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} {cursor : ScheduleCursor g input} {ledger : IndexTicketLedger cursor} {window : ProductiveOwnerWindow parse} {baseOwner candidate : Fin (10 * input.length)} (hlive : baseOwner ∈ cursor.indexOwners) (hbase : ledger.ticketOf baseOwner = window.parkingTicket) (hcandidate : candidate ∈ cursor.indexOwners) (hcandidateTicket : ledger.ticketOf candidate = window.parkingTicket) : candidate = baseOwner

In the parked branch, the designated base owner is the unique live owner carrying the current window parking ticket.

theorem IndexedGrammar.Aho.IndexTicketLedger.OverlayParking.transport {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} {old new : ScheduleCursor g input} {ledger : IndexTicketLedger old} {window : ProductiveOwnerWindow parse} {baseOwner : Fin (10 * input.length)} (parking : ledger.OverlayParking window baseOwner) (hindices : new.indexOwners.Perm old.indexOwners) : (ledger.transport hindices).OverlayParking window baseOwner

Transporting the cursor through a physical-owner permutation preserves restorable overlay parking.

theorem IndexedGrammar.Aho.IndexTicketLedger.OverlayParking.transport_mono {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {A₁ A₂ : g.nt} {stack₁ stack₂ : List g.flag} {w₁ w₂ : List T} {parse₁ : g.NFParse A₁ stack₁ w₁} {parse₂ : g.NFParse A₂ stack₂ w₂} {old new : ScheduleCursor g input} {ledger : IndexTicketLedger old} {oldWindow : ProductiveOwnerWindow parse₁} {newWindow : ProductiveOwnerWindow parse₂} {baseOwner : Fin (10 * input.length)} (parking : ledger.OverlayParking oldWindow baseOwner) (hindices : new.indexOwners.Perm old.indexOwners) (hbase : oldWindow.base ≤ newWindow.base) : (ledger.transport hindices).OverlayParking newWindow baseOwner

Transporting the physical cursor while weakly increasing the productive-window base preserves restorable overlay parking. A strict base increase absorbs a parked current-base ticket into the ordinary strict bound; under equal bases the parked witness is unchanged.

theorem IndexedGrammar.Aho.IndexTicketLedger.ParkingAtOrBelow.change_nonparking {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} {cursor : ScheduleCursor g input} {ledger updated : IndexTicketLedger cursor} {window : ProductiveOwnerWindow parse} (parking : ledger.ParkingAtOrBelow window) (owner : Fin (10 * input.length)) (hownerNonparking : (updated.ticketOf owner).Nonparking) (hunchanged : ∀ candidate ∈ cursor.indexOwners, candidate ≠ owner → updated.ticketOf candidate = ledger.ticketOf candidate) : updated.ParkingAtOrBelow window

Replacing one live ticket by a nonparking ticket, while leaving every other live ticket unchanged, preserves the non-strict parking bound.

theorem IndexedGrammar.Aho.IndexTicketLedger.ParkingBelow.change_nonparking {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} {cursor : ScheduleCursor g input} {ledger updated : IndexTicketLedger cursor} {window : ProductiveOwnerWindow parse} (parking : ledger.ParkingBelow window) (owner : Fin (10 * input.length)) (hownerNonparking : (updated.ticketOf owner).Nonparking) (hunchanged : ∀ candidate ∈ cursor.indexOwners, candidate ≠ owner → updated.ticketOf candidate = ledger.ticketOf candidate) : updated.ParkingBelow window

Replacing one live ticket by a nonparking ticket, while leaving every other live ticket unchanged, preserves a strict parking bound. This abstract form is useful for ticket normalizations whose implementation is not literally IndexTicketLedger.reticket.

theorem IndexedGrammar.Aho.IndexTicketLedger.OverlayParking.change_nonparking {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} {cursor : ScheduleCursor g input} {ledger updated : IndexTicketLedger cursor} {window : ProductiveOwnerWindow parse} {baseOwner : Fin (10 * input.length)} (parking : ledger.OverlayParking window baseOwner) (owner : Fin (10 * input.length)) (hownerNonparking : (updated.ticketOf owner).Nonparking) (hunchanged : ∀ candidate ∈ cursor.indexOwners, candidate ≠ owner → updated.ticketOf candidate = ledger.ticketOf candidate) : updated.OverlayParking window baseOwner

Replacing one live ticket by a nonparking ticket, while leaving every other live ticket unchanged, preserves restorable overlay parking. If the changed owner was the parked base owner, the resulting invariant is strict; otherwise the parked witness remains unchanged.

theorem IndexedGrammar.Aho.IndexTicketLedger.OverlayParking.allocate_nonparking {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} {old new : ScheduleCursor g input} {ledger : IndexTicketLedger old} {window : ProductiveOwnerWindow parse} {baseOwner : Fin (10 * input.length)} (parking : ledger.OverlayParking window baseOwner) (owner : Fin (10 * input.length)) (ticket : IndexTicket input) (hownerFresh : owner ∉ old.indexOwners) (hticketFresh : ticket ∉ old.indexTickets ledger.ticketOf) (hticketNotScratch : ∀ (hinput : 0 < input.length), ticket ≠ IndexTicket.scratch hinput) (hindices : new.indexOwners.Perm (owner :: old.indexOwners)) (hnonparking : ticket.Nonparking) : (ledger.allocate owner ticket hownerFresh hticketFresh hticketNotScratch hindices).OverlayParking window baseOwner

Allocating a fresh owner at a nonparking ticket preserves restorable overlay parking. The designated parked owner, when present, was already live and hence is not the allocated owner.

theorem IndexedGrammar.Aho.IndexTicketLedger.OverlayParking.restore_of_base_reticket_nonparking {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} {cursor : ScheduleCursor g input} {ledger updated : IndexTicketLedger cursor} {window : ProductiveOwnerWindow parse} {baseOwner : Fin (10 * input.length)} (hbound : updated.ParkingAtOrBelow window) (hlive : baseOwner ∈ cursor.indexOwners) (holdBase : ledger.ticketOf baseOwner = window.parkingTicket) (hnewBase : (updated.ticketOf baseOwner).Nonparking) (hunchanged : ∀ candidate ∈ cursor.indexOwners, candidate ≠ baseOwner → updated.ticketOf candidate = ledger.ticketOf candidate) : updated.ParkingBelow window

Abstract restoration lemma. Suppose a parked base owner is reticketed to a nonparking target and every other live ticket is unchanged. Once the updated ledger still satisfies ParkingAtOrBelow, its bound is automatically strict.

This formulation deliberately does not depend on the implementation of reticket; it is the generic fact needed by any later overlay ticket surgery.

theorem IndexedGrammar.Aho.IndexTicketLedger.OverlayParking.reticket_base_nonparking_restores {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} {cursor : ScheduleCursor g input} {ledger : IndexTicketLedger cursor} {window : ProductiveOwnerWindow parse} {baseOwner : Fin (10 * input.length)} (parking : ledger.OverlayParking window baseOwner) (hlive : baseOwner ∈ cursor.indexOwners) (target : IndexTicket input) (htargetFresh : target ∉ cursor.indexTickets ledger.ticketOf) (htargetNotScratch : ∀ (hinput : 0 < input.length), target ≠ IndexTicket.scratch hinput) (hnonparking : target.Nonparking) : (ledger.reticket baseOwner target hlive htargetFresh htargetNotScratch).ParkingBelow window

Reticketing the designated base owner to a fresh nonparking target restores the strict parking bound. IndexTicketLedger.reticket supplies the required unchanged-tail property.

theorem IndexedGrammar.Aho.IndexTicketLedger.OverlayParking.reticket_nonparking {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} {cursor : ScheduleCursor g input} {ledger : IndexTicketLedger cursor} {window : ProductiveOwnerWindow parse} {baseOwner : Fin (10 * input.length)} (parking : ledger.OverlayParking window baseOwner) (owner : Fin (10 * input.length)) (target : IndexTicket input) (howner : owner ∈ cursor.indexOwners) (htargetFresh : target ∉ cursor.indexTickets ledger.ticketOf) (htargetNotScratch : ∀ (hinput : 0 < input.length), target ≠ IndexTicket.scratch hinput) (hnonparking : target.Nonparking) : (ledger.reticket owner target howner htargetFresh htargetNotScratch).OverlayParking window baseOwner

Reticketing any live owner to a fresh nonparking target preserves the restorable invariant. When the selected owner is the parked base owner, the result takes the strict branch; otherwise the parked witness is unchanged.

theorem IndexedGrammar.Aho.IndexTicketLedger.OverlayParking.release_ne {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} {old new : ScheduleCursor g input} {ledger : IndexTicketLedger old} {window : ProductiveOwnerWindow parse} {baseOwner : Fin (10 * input.length)} (parking : ledger.OverlayParking window baseOwner) (owner : Fin (10 * input.length)) (hindices : old.indexOwners.Perm (owner :: new.indexOwners)) (hne : owner ≠ baseOwner) : (ledger.release owner hindices).OverlayParking window baseOwner

Releasing an owner other than the designated base owner preserves restorable overlay parking. This is the operation used when an unrelated private overlay head is erased.

theorem IndexedGrammar.Aho.IndexTicketLedger.OverlayParking.release_base_restores {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} {old new : ScheduleCursor g input} {ledger : IndexTicketLedger old} {window : ProductiveOwnerWindow parse} {baseOwner : Fin (10 * input.length)} (parking : ledger.OverlayParking window baseOwner) (hindices : old.indexOwners.Perm (baseOwner :: new.indexOwners)) : (ledger.release baseOwner hindices).ParkingBelow window

Releasing the designated parked owner itself restores the strict parking bound. The released ticket is absent from the tail by duplicate-freedom, so no remaining owner can carry the current canonical parking ticket.

theorem IndexedGrammar.Aho.IndexTicketLedger.OverlayParking.release {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} {old new : ScheduleCursor g input} {ledger : IndexTicketLedger old} {window : ProductiveOwnerWindow parse} {baseOwner : Fin (10 * input.length)} (parking : ledger.OverlayParking window baseOwner) (owner : Fin (10 * input.length)) (hindices : old.indexOwners.Perm (owner :: new.indexOwners)) : (ledger.release owner hindices).OverlayParking window baseOwner

Releasing an arbitrary overlay owner preserves restorable parking. If it is the designated parked owner, the result moves to the strict branch; otherwise the witness remains live.