LanglibInvariant-preserving scheduler moves #
The compressed runner changes the focused payload one elementary Aho move at a time. This module isolates the corresponding ownership arithmetic. The lemmas are deliberately phrased at cursor level: semantic runner modes may choose their own task constructors, and only need to prove the resulting owner equalities or freshness facts.
Generic owner insertion and deletion #
theorem
IndexedGrammar.Aho.ScheduleInvariant.insertTaskOwner
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(hinv : ScheduleInvariant old)
(owner : Fin input.length)
(hfresh : owner ∉ old.taskOwners)
(htasks : new.taskOwners.Perm (owner :: old.taskOwners))
(hindices : new.indexOwners = old.indexOwners)
(hframes : new.frameOwners = old.frameOwners)
(hlength : new.word.length = old.word.length + 1)
:
Insert one fresh task/terminal owner while adding exactly one ghost square.
theorem
IndexedGrammar.Aho.ScheduleInvariant.insertIndexOwner
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(hinv : ScheduleInvariant old)
(owner : Fin (10 * input.length))
(hfresh : owner ∉ old.indexOwners)
(hcapacity : old.indexOwners.length < 6 * input.length)
(htasks : new.taskOwners = old.taskOwners)
(hindices : new.indexOwners.Perm (owner :: old.indexOwners))
(hframes : new.frameOwners = old.frameOwners)
(hlength : new.word.length = old.word.length + 1)
:
Insert one fresh persistent-index owner while adding exactly one ghost square.
theorem
IndexedGrammar.Aho.ScheduleInvariant.removeTaskOwner
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(hinv : ScheduleInvariant old)
(owner : Fin input.length)
(htasks : old.taskOwners.Perm (owner :: new.taskOwners))
(hindices : new.indexOwners = old.indexOwners)
(hframes : new.frameOwners = old.frameOwners)
(hlength : old.word.length = new.word.length + 1)
:
Delete one task/terminal owner together with its unique ghost square.
theorem
IndexedGrammar.Aho.ScheduleInvariant.insertFrameOwner
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(hinv : ScheduleInvariant old)
(owner : Fin (10 * input.length))
(hfresh : owner ∉ old.frameOwners)
(htasks : new.taskOwners.Perm old.taskOwners)
(hindices : new.indexOwners = old.indexOwners)
(hframes : new.frameOwners.Perm (owner :: old.frameOwners))
(hownerIndex : owner ∈ new.indexOwners)
(hlength : new.word.length = old.word.length + 2)
:
Open one frame charged to an existing persistent index. The two new ghost squares are the
inner $ and its matching close.
theorem
IndexedGrammar.Aho.ScheduleInvariant.removeFrameOwner
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(hinv : ScheduleInvariant old)
(owner : Fin (10 * input.length))
(htasks : new.taskOwners = old.taskOwners)
(hindices : new.indexOwners = old.indexOwners)
(hframes : old.frameOwners.Perm (owner :: new.frameOwners))
(hlength : old.word.length = new.word.length + 2)
:
Close one frame and remove its $/close delimiter pair.
theorem
IndexedGrammar.Aho.ScheduleInvariant.removeIndexOwner
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(hinv : ScheduleInvariant old)
(owner : Fin (10 * input.length))
(hunframed : owner ∉ old.frameOwners)
(htasks : new.taskOwners = old.taskOwners)
(hindices : old.indexOwners.Perm (owner :: new.indexOwners))
(hframes : new.frameOwners = old.frameOwners)
(hlength : old.word.length = new.word.length + 1)
:
Remove one persistent index which is not charged by an open frame.
Focused plain-mode cursor changes #
theorem
IndexedGrammar.Aho.ScheduleInvariant.replaceTask_sameOwner
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(left right : List (ScheduleAtom g input))
(oldTask newTask : ScheduleTask g input)
(howner : newTask.owner = oldTask.owner)
(hinv : ScheduleInvariant { left := left, focus := ScheduleAtom.task oldTask, right := right })
:
ScheduleInvariant { left := left, focus := ScheduleAtom.task newTask, right := right }
Replace a focused task by another task with the same terminal owner.
theorem
IndexedGrammar.Aho.ScheduleInvariant.plainBinary
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(left right : List (ScheduleAtom g input))
(parent leftTask rightTask : ScheduleTask g input)
(hleftOwner : leftTask.owner = parent.owner)
(hrightFresh : rightTask.owner ∉ { left := left, focus := ScheduleAtom.task parent, right := right }.taskOwners)
(hinv : ScheduleInvariant { left := left, focus := ScheduleAtom.task parent, right := right })
:
ScheduleInvariant { left := left, focus := ScheduleAtom.task leftTask, right := ScheduleAtom.task rightTask :: right }
The plain binary move replaces one task by its two ordered children. The left child keeps the parent owner; freshness of the right child is the only new ownership obligation.
theorem
IndexedGrammar.Aho.ScheduleInvariant.plainPushSkip
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(left right : List (ScheduleAtom g input))
(parent child : ScheduleTask g input)
(howner : child.owner = parent.owner)
(hinv : ScheduleInvariant { left := left, focus := ScheduleAtom.task parent, right := right })
:
ScheduleInvariant { left := left, focus := ScheduleAtom.task child, right := right }
A plain push whose new flag is irrelevant only changes the task certificate.
theorem
IndexedGrammar.Aho.ScheduleInvariant.plainPushUse
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(left right : List (ScheduleAtom g input))
(parent child : ScheduleTask g input)
(idx : ScheduleIndex g input)
(htaskOwner : child.owner = parent.owner)
(hindexFresh : idx.owner ∉ { left := left, focus := ScheduleAtom.task parent, right := right }.indexOwners)
(hcapacity : { left := left, focus := ScheduleAtom.task parent, right := right }.indexOwners.length < 6 * input.length)
(hinv : ScheduleInvariant { left := left, focus := ScheduleAtom.task parent, right := right })
:
ScheduleInvariant { left := left, focus := ScheduleAtom.task child, right := ScheduleAtom.index idx :: right }
A plain push which starts a relevant block keeps the task owner and allocates one fresh persistent index immediately to its right.
theorem
IndexedGrammar.Aho.ScheduleInvariant.livePushCompress
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(left right : List (ScheduleAtom g input))
(parent child : ScheduleTask g input)
(oldIndex newIndex : ScheduleIndex g input)
(htaskOwner : child.owner = parent.owner)
(hindexOwner : newIndex.owner = oldIndex.owner)
(hinv :
ScheduleInvariant { left := left, focus := ScheduleAtom.task parent, right := ScheduleAtom.index oldIndex :: right })
:
ScheduleInvariant { left := left, focus := ScheduleAtom.task child, right := ScheduleAtom.index newIndex :: right }
Replace a focused live task and its adjacent represented block without changing either
persistent owner. This is the invariant part of livePushCompress.
theorem
IndexedGrammar.Aho.ScheduleInvariant.plainTerminal
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(left right : List (ScheduleAtom g input))
(task : ScheduleTask g input)
(a : T)
(hinv : ScheduleInvariant { left := left, focus := ScheduleAtom.task task, right := right })
:
ScheduleInvariant { left := left, focus := ScheduleAtom.terminal task.owner a, right := right }
Emitting the terminal of a plain leaf preserves its task owner exactly.
theorem
IndexedGrammar.Aho.ScheduleInvariant.matchTerminal
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(left : List (ScheduleAtom g input))
(owner : Fin input.length)
(a : T)
(next : ScheduleAtom g input)
(right : List (ScheduleAtom g input))
(hinv : ScheduleInvariant { left := left, focus := ScheduleAtom.terminal owner a, right := next :: right })
:
ScheduleInvariant { left := left, focus := next, right := right }
Matching an emitted terminal removes its owner and focuses the following square.
theorem
IndexedGrammar.Aho.ScheduleInvariant.finishTask
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(left : List (ScheduleAtom g input))
(task : ScheduleTask g input)
(next : ScheduleAtom g input)
(right : List (ScheduleAtom g input))
(hinv : ScheduleInvariant { left := left, focus := ScheduleAtom.task task, right := next :: right })
:
ScheduleInvariant { left := left, focus := next, right := right }
Remove a completed focused task payload and expose its continuation. Recursive runner endpoints use this owner-level inverse of task creation.
Pop-frame cursor changes #
theorem
IndexedGrammar.Aho.ScheduleInvariant.popErase
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(alpha tail : List (ScheduleAtom g input))
(task residual : ScheduleTask g input)
(idx : ScheduleIndex g input)
(htaskOwner : residual.owner = task.owner)
(hunframed :
idx.owner ∉
{ left := alpha ++ [ScheduleAtom.dollar], focus := ScheduleAtom.task task,
right := ScheduleAtom.index idx :: tail }.frameOwners)
(hinv :
ScheduleInvariant
{ left := alpha ++ [ScheduleAtom.dollar], focus := ScheduleAtom.task task,
right := ScheduleAtom.index idx :: tail })
:
ScheduleInvariant { left := alpha ++ [ScheduleAtom.dollar], focus := ScheduleAtom.task residual, right := tail }
Pop and immediately erase an adjacent compressed block. No frame is opened: the selected index is owned by the active call, so after applying its relation the residual task may reuse that owner.
theorem
IndexedGrammar.Aho.ScheduleInvariant.popFrame
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(alpha gap tail : List (ScheduleAtom g input))
(task residual : ScheduleTask g input)
(idx : ScheduleIndex g input)
(htaskOwner : residual.owner = task.owner)
(hframeFresh :
idx.owner ∉
{ left := alpha ++ [ScheduleAtom.dollar], focus := ScheduleAtom.task task,
right := gap ++ ScheduleAtom.index idx :: tail }.frameOwners)
(hinv :
ScheduleInvariant
{ left := alpha ++ [ScheduleAtom.dollar], focus := ScheduleAtom.task task,
right := gap ++ ScheduleAtom.index idx :: tail })
:
ScheduleInvariant
{ left := alpha ++ [ScheduleAtom.dollar] ++ gap ++ [ScheduleAtom.index idx.markUsed, ScheduleAtom.dollar],
focus := ScheduleAtom.task residual, right := ScheduleAtom.close idx.owner :: tail }
Consume a selected index, mark it used, and open the frame in which the residual task runs.
The task may cross arbitrary task payloads in gap; owner permutation, rather than syntactic
list equality, is therefore the appropriate invariant statement.
theorem
IndexedGrammar.Aho.ScheduleInvariant.returnFrame
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(alpha gap tail : List (ScheduleAtom g input))
(next : ScheduleAtom g input)
(owner : Fin (10 * input.length))
(hinv :
ScheduleInvariant
{ left := alpha ++ [ScheduleAtom.dollar, next] ++ gap ++ [ScheduleAtom.dollar], focus := ScheduleAtom.close owner,
right := tail })
:
ScheduleInvariant { left := alpha ++ [ScheduleAtom.dollar], focus := next, right := gap ++ tail }
Return from a completed pop frame. The saved square next and gap are restored outside
the frame while the matching close charge disappears.
theorem
IndexedGrammar.Aho.ScheduleInvariant.prepareReturnFrame
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(alpha gap tail : List (ScheduleAtom g input))
(next : ScheduleAtom g input)
(owner : Fin (10 * input.length))
(hfresh : owner ∉ { left := alpha ++ [ScheduleAtom.dollar], focus := next, right := gap ++ tail }.frameOwners)
(howned : owner ∈ { left := alpha ++ [ScheduleAtom.dollar], focus := next, right := gap ++ tail }.indexOwners)
(hinv : ScheduleInvariant { left := alpha ++ [ScheduleAtom.dollar], focus := next, right := gap ++ tail })
:
ScheduleInvariant
{ left := alpha ++ [ScheduleAtom.dollar, next] ++ gap ++ [ScheduleAtom.dollar], focus := ScheduleAtom.close owner,
right := tail }
Reconstruct the invariant expected immediately before returnFrame. This is the inverse
accounting move used to provide a recursive subrun with its required endpoint invariant.
theorem
IndexedGrammar.Aho.ScheduleInvariant.eraseIndex
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(alpha tail : List (ScheduleAtom g input))
(idx : ScheduleIndex g input)
(next : ScheduleAtom g input)
(hunframed :
idx.owner ∉
{ left := alpha ++ [ScheduleAtom.dollar], focus := ScheduleAtom.index idx, right := next :: tail }.frameOwners)
(hinv :
ScheduleInvariant { left := alpha ++ [ScheduleAtom.dollar], focus := ScheduleAtom.index idx, right := next :: tail })
:
ScheduleInvariant { left := alpha ++ [ScheduleAtom.dollar], focus := next, right := tail }
Erase an unframed used index and expose the square following it.