LanglibOwner-annotated compressed block layouts #
This module mirrors BlockLayout before scheduler annotations are erased. Each physical block
is represented by one ScheduleIndex, and the layout index records its persistent owner. This
makes owner alignment and duplicate-freedom available to the bounded runner while erasure remains
exactly the already-verified physical layout.
def
IndexedGrammar.Aho.ScheduleIndexFree
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(xs : List (ScheduleAtom g input))
:
A ghost segment contains no scheduler index atom.
Equations
- IndexedGrammar.Aho.ScheduleIndexFree xs = ∀ (idx : IndexedGrammar.Aho.ScheduleIndex g input), IndexedGrammar.Aho.ScheduleAtom.index idx ∉ xs
Instances For
def
IndexedGrammar.Aho.ScheduleDollarFree
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(xs : List (ScheduleAtom g input))
:
A ghost segment contains no scheduler $ atom.
Equations
Instances For
theorem
IndexedGrammar.Aho.ScheduleIndexFree.append
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{xs ys : List (ScheduleAtom g input)}
(hxs : ScheduleIndexFree xs)
(hys : ScheduleIndexFree ys)
:
ScheduleIndexFree (xs ++ ys)
theorem
IndexedGrammar.Aho.ScheduleIndexFree.erase
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{xs : List (ScheduleAtom g input)}
(hfree : ScheduleIndexFree xs)
:
Erasing an index-free ghost gap produces an index-free physical gap.
@[simp]
theorem
IndexedGrammar.Aho.ScheduleIndexFree.filterMap_indexOwner_eq_nil
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{xs : List (ScheduleAtom g input)}
(hfree : ScheduleIndexFree xs)
:
theorem
IndexedGrammar.Aho.ScheduleDollarFree.append
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{xs ys : List (ScheduleAtom g input)}
(hxs : ScheduleDollarFree xs)
(hys : ScheduleDollarFree ys)
:
ScheduleDollarFree (xs ++ ys)
theorem
IndexedGrammar.Aho.ScheduleDollarFree.erase
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{xs : List (ScheduleAtom g input)}
(hfree : ScheduleDollarFree xs)
:
Erasing a dollar-free ghost gap produces a dollar-free physical gap.
def
IndexedGrammar.Aho.ScheduleIndex.markUsed
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(idx : ScheduleIndex g input)
:
ScheduleIndex g input
Mark one scheduler index used without changing its denotation or persistent owner.
Equations
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ScheduleIndex.markUsed_flags
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(idx : ScheduleIndex g input)
:
@[simp]
theorem
IndexedGrammar.Aho.ScheduleIndex.markUsed_relation
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(idx : ScheduleIndex g input)
:
@[simp]
theorem
IndexedGrammar.Aho.ScheduleIndex.markUsed_mark
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(idx : ScheduleIndex g input)
:
@[simp]
theorem
IndexedGrammar.Aho.ScheduleIndex.markUsed_owner
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(idx : ScheduleIndex g input)
:
@[simp]
theorem
IndexedGrammar.Aho.ScheduleIndex.markUsed_idem
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(idx : ScheduleIndex g input)
:
@[simp]
theorem
IndexedGrammar.Aho.ScheduleIndex.markUsed_later
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(idx : ScheduleIndex g input)
:
inductive
IndexedGrammar.Aho.ScheduleBlockLayout
{T : Type}
(g : IndexedGrammar T)
[Fintype g.nt]
(input : List T)
:
A ghost compressed visible-stack layout, indexed by the persistent owner of every selected
block. Gaps may contain tasks, terminals, and close, but neither another index nor $.
- nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (tail : List (ScheduleAtom g input)) : ScheduleBlockLayout g input [] [] [] tail tail
- cons {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {flags : List g.flag} {blocks : List (List g.flag)} {owners : List (Fin (10 * input.length))} {beta tail tail' : List (ScheduleAtom g input)} (idx : ScheduleIndex g input) (block_ne : idx.flags ≠ []) (indexFree : ScheduleIndexFree beta) (dollarFree : ScheduleDollarFree beta) (later : flags ≠ [] → idx.mark.later = true) (fresh : idx.owner ∉ owners) (rest : ScheduleBlockLayout g input flags blocks owners tail tail') : ScheduleBlockLayout g input (idx.flags ++ flags) (idx.flags :: blocks) (idx.owner :: owners) (beta ++ ScheduleAtom.index idx :: tail) (beta ++ ScheduleAtom.index idx.markUsed :: tail')
Instances For
theorem
IndexedGrammar.Aho.ScheduleBlockLayout.owners_length
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{flags : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
{word used : List (ScheduleAtom g input)}
(layout : ScheduleBlockLayout g input flags blocks owners word used)
:
Owner and block indices always have the same length.
theorem
IndexedGrammar.Aho.ScheduleBlockLayout.owners_nodup
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{flags : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
{word used : List (ScheduleAtom g input)}
(layout : ScheduleBlockLayout g input flags blocks owners word used)
:
owners.Nodup
Selected block owners are pairwise distinct.
def
IndexedGrammar.Aho.ScheduleBlockLayout.blockOwnership
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{flags : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
{word used : List (ScheduleAtom g input)}
(layout : ScheduleBlockLayout g input flags blocks owners word used)
:
BlockOwnership (10 * input.length) blocks
A ghost layout directly supplies the generic persistent ownership carrier.
Equations
- layout.blockOwnership = { owners := owners, owners_length := ⋯, owners_nodup := ⋯ }
Instances For
theorem
IndexedGrammar.Aho.ScheduleBlockLayout.erase
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{flags : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
{word used : List (ScheduleAtom g input)}
(layout : ScheduleBlockLayout g input flags blocks owners word used)
:
BlockLayout g flags blocks (List.map ScheduleAtom.workSym word) (List.map ScheduleAtom.workSym used)
Erasing ghost annotations produces the corresponding physical compressed layout.
theorem
IndexedGrammar.Aho.ScheduleBlockLayout.flags_eq_flatten
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{flags : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
{word used : List (ScheduleAtom g input)}
(layout : ScheduleBlockLayout g input flags blocks owners word used)
:
The concrete visible prefix is exactly the flattening of the ghost block partition.
theorem
IndexedGrammar.Aho.ScheduleBlockLayout.idempotent
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{flags : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
{word used : List (ScheduleAtom g input)}
(layout : ScheduleBlockLayout g input flags blocks owners word used)
:
ScheduleBlockLayout g input flags blocks owners used used
Re-selecting an already used ghost layout leaves every atom and owner unchanged.
theorem
IndexedGrammar.Aho.ScheduleBlockLayout.prepend
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{flags : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
{word used : List (ScheduleAtom g input)}
(pref : List (ScheduleAtom g input))
(hindex : ScheduleIndexFree pref)
(hdollar : ScheduleDollarFree pref)
(layout : ScheduleBlockLayout g input flags blocks owners word used)
:
ScheduleBlockLayout g input flags blocks owners (pref ++ word) (pref ++ used)
Insert an index- and dollar-free ghost prefix before the first selected block.
theorem
IndexedGrammar.Aho.ScheduleBlockLayout.splitTake
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{flags : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
{word used : List (ScheduleAtom g input)}
(n : ℕ)
(layout : ScheduleBlockLayout g input flags blocks owners word used)
:
∃ (middle : List (ScheduleAtom g input)),
ScheduleBlockLayout g input (List.take n blocks).flatten (List.take n blocks) (List.take n owners) word middle ∧ ScheduleBlockLayout g input flags blocks owners middle used
Restrict a ghost layout to its first n whole blocks and aligned owners.
theorem
IndexedGrammar.Aho.ScheduleBlockLayout.exists_selectedPrefixes
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{flags : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
{word used : List (ScheduleAtom g input)}
(layout : ScheduleBlockLayout g input flags blocks owners word used)
:
∃ (selected : List (ScheduleAtom g input)) (selectedUsed : List (ScheduleAtom g input)) (tail :
List (ScheduleAtom g input)),
word = selected ++ tail ∧ used = selectedUsed ++ tail ∧ List.filterMap ScheduleAtom.indexOwner? selected = owners ∧ List.filterMap ScheduleAtom.indexOwner? selectedUsed = owners
The selected ghost prefixes expose their owner list exactly; the arbitrary common tail may contain additional unselected indices.
theorem
IndexedGrammar.Aho.ScheduleBlockLayout.frameOwners_eq
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{flags : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
{word used : List (ScheduleAtom g input)}
(layout : ScheduleBlockLayout g input flags blocks owners word used)
:
Marking selected indices preserves every owner carried by an open frame.
theorem
IndexedGrammar.Aho.ScheduleBlockLayout.taskOwners_eq
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{flags : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
{word used : List (ScheduleAtom g input)}
(layout : ScheduleBlockLayout g input flags blocks owners word used)
:
Marking selected indices preserves every pending-task/terminal owner.
theorem
IndexedGrammar.Aho.ScheduleBlockLayout.word_length_eq
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{flags : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
{word used : List (ScheduleAtom g input)}
(layout : ScheduleBlockLayout g input flags blocks owners word used)
:
Marking changes no physical or ghost word length.
theorem
IndexedGrammar.Aho.ScheduleBlockLayout.word_eq_used_of_flags_eq_nil
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{flags : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
{word used : List (ScheduleAtom g input)}
(layout : ScheduleBlockLayout g input flags blocks owners word used)
(hflags : flags = [])
:
With no represented concrete flags there are no selected indices, so input and marked output words are definitionally the same common tail.
theorem
IndexedGrammar.Aho.ScheduleBlockLayout.exists_indexOwnersSuffix
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{flags : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
{word used : List (ScheduleAtom g input)}
(layout : ScheduleBlockLayout g input flags blocks owners word used)
:
∃ (suffix : List (Fin (10 * input.length))),
List.filterMap ScheduleAtom.indexOwner? word = owners ++ suffix ∧ List.filterMap ScheduleAtom.indexOwner? used = owners ++ suffix
The selected-owner contribution is an exact prefix of the full index-owner list; the same unselected suffix occurs before and after marking.
theorem
IndexedGrammar.Aho.ScheduleBlockLayout.indexOwners_eq
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{flags : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
{word used : List (ScheduleAtom g input)}
(layout : ScheduleBlockLayout g input flags blocks owners word used)
:
Marking selected indices preserves the complete index-owner sequence.
@[simp]
theorem
IndexedGrammar.Aho.ScheduleCursor.taskOwners_mk
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(left : List (ScheduleAtom g input))
(focus : ScheduleAtom g input)
(right : List (ScheduleAtom g input))
:
{ left := left, focus := focus, right := right }.taskOwners = List.filterMap ScheduleAtom.taskOwner? left ++ List.filterMap ScheduleAtom.taskOwner? [focus] ++ List.filterMap ScheduleAtom.taskOwner? right
@[simp]
theorem
IndexedGrammar.Aho.ScheduleCursor.indexOwners_mk
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(left : List (ScheduleAtom g input))
(focus : ScheduleAtom g input)
(right : List (ScheduleAtom g input))
:
{ left := left, focus := focus, right := right }.indexOwners = List.filterMap ScheduleAtom.indexOwner? left ++ List.filterMap ScheduleAtom.indexOwner? [focus] ++ List.filterMap ScheduleAtom.indexOwner? right
@[simp]
theorem
IndexedGrammar.Aho.ScheduleCursor.frameOwners_mk
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(left : List (ScheduleAtom g input))
(focus : ScheduleAtom g input)
(right : List (ScheduleAtom g input))
:
{ left := left, focus := focus, right := right }.frameOwners = List.filterMap ScheduleAtom.closeOwner? left ++ List.filterMap ScheduleAtom.closeOwner? [focus] ++ List.filterMap ScheduleAtom.closeOwner? right
theorem
IndexedGrammar.Aho.ScheduleInvariant.of_ownerFields_eq
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(hinv : ScheduleInvariant old)
(htasks : new.taskOwners = old.taskOwners)
(hindices : new.indexOwners = old.indexOwners)
(hframes : new.frameOwners = old.frameOwners)
(hlength : new.word.length = old.word.length)
:
Transport the global invariant across a cursor change which preserves all three owner lists and total ghost-word length.
theorem
IndexedGrammar.Aho.ScheduleInvariant.replaceRight
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{flags : List g.flag}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
{word used : List (ScheduleAtom g input)}
(left : List (ScheduleAtom g input))
(focus : ScheduleAtom g input)
(layout : ScheduleBlockLayout g input flags blocks owners word used)
(hinv : ScheduleInvariant { left := left, focus := focus, right := word })
:
ScheduleInvariant { left := left, focus := focus, right := used }
Marking all selected blocks in the right segment preserves the complete scheduler invariant.