Langlib

Langlib.Grammars.Indexed.NormalForm.Aho.Scheduler.Runners.Overlay.Layout

Branch-local compressed-index overlays #

A protected compressed block may be shared by a pending sibling and therefore cannot be updated in place. A branch which pushes above that shared suffix instead keeps a overlay, adjacent copy-on-write prefix. The head of this prefix is the mutable compressed accumulator; temporary event-boundary blocks may be consed above it and popped again without forgetting that the lower head is still overlay.

This file is deliberately ghost-only. An overlay index erases to the existing WorkSym.index, so all operations are already certified by livePushFresh, livePushCompress, the adjacent pop-and-erase moves, and eraseIndex. The only missing datum in the runner is which adjacent lower indices remain branch-local.

Computed overlay words and ledgers #

source
def IndexedGrammar.Aho.ScheduleOverlay.blocks {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (overlay : List (ScheduleIndex g input)) :
List (List g.flag)

Concrete flag blocks carried by the overlay overlay, nearest block first.

Equations
Instances For
    source
    def IndexedGrammar.Aho.ScheduleOverlay.flags {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (overlay : List (ScheduleIndex g input)) (baseSuffix : List g.flag) :
    List g.flag

    The complete visible flag prefix after placing an overlay above a protected suffix.

    Equations
    Instances For
      source
      def IndexedGrammar.Aho.ScheduleOverlay.owners {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (overlay : List (ScheduleIndex g input)) (baseSuffix : List (Fin (10 * input.length))) :
      List (Fin (10 * input.length))

      Persistent owners of the overlay followed by those of the protected suffix.

      Equations
      Instances For
        source
        def IndexedGrammar.Aho.ScheduleOverlay.word {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (overlay : List (ScheduleIndex g input)) (baseSuffix : List (ScheduleAtom g input)) :
        List (ScheduleAtom g input)

        Physical scheduler word with every overlay overlay block adjacent to the active task.

        Equations
        Instances For
          source
          def IndexedGrammar.Aho.ScheduleOverlay.used {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (overlay : List (ScheduleIndex g input)) (baseSuffix : List (ScheduleAtom g input)) :
          List (ScheduleAtom g input)

          Endpoint word after every overlay block and every protected block has been marked used.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem IndexedGrammar.Aho.ScheduleOverlay.blocks_nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} :
            blocks [] = []
            source
            @[simp]
            theorem IndexedGrammar.Aho.ScheduleOverlay.blocks_cons {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (idx : ScheduleIndex g input) (overlay : List (ScheduleIndex g input)) :
            blocks (idx :: overlay) = idx.flags :: blocks overlay
            source
            @[simp]
            theorem IndexedGrammar.Aho.ScheduleOverlay.flags_nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (baseSuffix : List g.flag) :
            flags [] baseSuffix = baseSuffix
            source
            @[simp]
            theorem IndexedGrammar.Aho.ScheduleOverlay.flags_cons {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (idx : ScheduleIndex g input) (overlay : List (ScheduleIndex g input)) (baseSuffix : List g.flag) :
            flags (idx :: overlay) baseSuffix = idx.flags ++ flags overlay baseSuffix
            source
            @[simp]
            theorem IndexedGrammar.Aho.ScheduleOverlay.owners_nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (baseSuffix : List (Fin (10 * input.length))) :
            owners [] baseSuffix = baseSuffix
            source
            @[simp]
            theorem IndexedGrammar.Aho.ScheduleOverlay.owners_cons {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (idx : ScheduleIndex g input) (overlay : List (ScheduleIndex g input)) (baseSuffix : List (Fin (10 * input.length))) :
            owners (idx :: overlay) baseSuffix = idx.owner :: owners overlay baseSuffix
            source
            @[simp]
            theorem IndexedGrammar.Aho.ScheduleOverlay.word_nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (baseSuffix : List (ScheduleAtom g input)) :
            word [] baseSuffix = baseSuffix
            source
            @[simp]
            theorem IndexedGrammar.Aho.ScheduleOverlay.word_cons {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (idx : ScheduleIndex g input) (overlay : List (ScheduleIndex g input)) (baseSuffix : List (ScheduleAtom g input)) :
            word (idx :: overlay) baseSuffix = ScheduleAtom.index idx :: word overlay baseSuffix
            source
            @[simp]
            theorem IndexedGrammar.Aho.ScheduleOverlay.used_nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (baseSuffix : List (ScheduleAtom g input)) :
            used [] baseSuffix = baseSuffix
            source
            @[simp]
            theorem IndexedGrammar.Aho.ScheduleOverlay.used_cons {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (idx : ScheduleIndex g input) (overlay : List (ScheduleIndex g input)) (baseSuffix : List (ScheduleAtom g input)) :
            used (idx :: overlay) baseSuffix = ScheduleAtom.index idx.markUsed :: used overlay baseSuffix
            source
            @[simp]
            theorem IndexedGrammar.Aho.ScheduleOverlay.blocks_length {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (overlay : List (ScheduleIndex g input)) :
            (blocks overlay).length = overlay.length
            source
            @[simp]
            theorem IndexedGrammar.Aho.ScheduleOverlay.privateOwners_length {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (overlay : List (ScheduleIndex g input)) :
            (List.map ScheduleIndex.owner overlay).length = overlay.length

            Adjacent overlay certificate #

            source
            inductive IndexedGrammar.Aho.AdjacentOverlayLayout {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {protectedFlags : List g.flag} {protectedBlocks : List (List g.flag)} {protectedOwners : List (Fin (10 * input.length))} {protectedWord protectedUsed : List (ScheduleAtom g input)} (base : ScheduleBlockLayout g input protectedFlags protectedBlocks protectedOwners protectedWord protectedUsed) :
            List (ScheduleIndex g input) → Prop

            An adjacent overlay index prefix layered over an already certified protected layout.

            The certificate is indexed only by the list of overlay ScheduleIndex records. All other objects are computed by ScheduleOverlay, which makes consing a fresh block, replacing the mutable head, and popping a temporary head exact operations rather than transports between existential layouts.

            Instances For
              source
              def IndexedGrammar.Aho.AdjacentOverlayLayout.empty {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {protectedFlags : List g.flag} {protectedBlocks : List (List g.flag)} {protectedOwners : List (Fin (10 * input.length))} {protectedWord protectedUsed : List (ScheduleAtom g input)} (base : ScheduleBlockLayout g input protectedFlags protectedBlocks protectedOwners protectedWord protectedUsed) :
              AdjacentOverlayLayout base []

              The empty overlay prefix is the protected layout itself.

              Equations
              • ⋯ = ⋯
              Instances For
                source
                def IndexedGrammar.Aho.AdjacentOverlayLayout.singleton {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {protectedFlags : List g.flag} {protectedBlocks : List (List g.flag)} {protectedOwners : List (Fin (10 * input.length))} {protectedWord protectedUsed : List (ScheduleAtom g input)} (base : ScheduleBlockLayout g input protectedFlags protectedBlocks protectedOwners protectedWord protectedUsed) (idx : ScheduleIndex g input) (block_ne : idx.flags ≠ []) (later : protectedFlags ≠ [] → idx.mark.later = true) (fresh : idx.owner ∉ protectedOwners) :
                AdjacentOverlayLayout base [idx]

                Put one mutable overlay block above a protected suffix.

                Equations
                • ⋯ = ⋯
                Instances For
                  source
                  def IndexedGrammar.Aho.AdjacentOverlayLayout.push {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {protectedFlags : List g.flag} {protectedBlocks : List (List g.flag)} {protectedOwners : List (Fin (10 * input.length))} {protectedWord protectedUsed : List (ScheduleAtom g input)} {base : ScheduleBlockLayout g input protectedFlags protectedBlocks protectedOwners protectedWord protectedUsed} {overlay : List (ScheduleIndex g input)} (layout : AdjacentOverlayLayout base overlay) (idx : ScheduleIndex g input) (block_ne : idx.flags ≠ []) (later : ScheduleOverlay.flags overlay protectedFlags ≠ [] → idx.mark.later = true) (fresh : idx.owner ∉ ScheduleOverlay.owners overlay protectedOwners) :
                  AdjacentOverlayLayout base (idx :: overlay)

                  Cons a new overlay event-boundary block above an existing overlay.

                  Equations
                  • ⋯ = ⋯
                  Instances For
                    source
                    theorem IndexedGrammar.Aho.AdjacentOverlayLayout.tail {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {protectedFlags : List g.flag} {protectedBlocks : List (List g.flag)} {protectedOwners : List (Fin (10 * input.length))} {protectedWord protectedUsed : List (ScheduleAtom g input)} {base : ScheduleBlockLayout g input protectedFlags protectedBlocks protectedOwners protectedWord protectedUsed} {head : ScheduleIndex g input} {overlay : List (ScheduleIndex g input)} (layout : AdjacentOverlayLayout base (head :: overlay)) :
                    AdjacentOverlayLayout base overlay

                    Pop the adjacent overlay head while retaining the lower copy-on-write classification.

                    source
                    theorem IndexedGrammar.Aho.AdjacentOverlayLayout.head_block_ne {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {protectedFlags : List g.flag} {protectedBlocks : List (List g.flag)} {protectedOwners : List (Fin (10 * input.length))} {protectedWord protectedUsed : List (ScheduleAtom g input)} {base : ScheduleBlockLayout g input protectedFlags protectedBlocks protectedOwners protectedWord protectedUsed} {head : ScheduleIndex g input} {overlay : List (ScheduleIndex g input)} (layout : AdjacentOverlayLayout base (head :: overlay)) :
                    head.flags ≠ []
                    source
                    theorem IndexedGrammar.Aho.AdjacentOverlayLayout.head_later {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {protectedFlags : List g.flag} {protectedBlocks : List (List g.flag)} {protectedOwners : List (Fin (10 * input.length))} {protectedWord protectedUsed : List (ScheduleAtom g input)} {base : ScheduleBlockLayout g input protectedFlags protectedBlocks protectedOwners protectedWord protectedUsed} {head : ScheduleIndex g input} {overlay : List (ScheduleIndex g input)} (layout : AdjacentOverlayLayout base (head :: overlay)) (hlower : ScheduleOverlay.flags overlay protectedFlags ≠ []) :
                    head.mark.later = true
                    source
                    theorem IndexedGrammar.Aho.AdjacentOverlayLayout.head_fresh {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {protectedFlags : List g.flag} {protectedBlocks : List (List g.flag)} {protectedOwners : List (Fin (10 * input.length))} {protectedWord protectedUsed : List (ScheduleAtom g input)} {base : ScheduleBlockLayout g input protectedFlags protectedBlocks protectedOwners protectedWord protectedUsed} {head : ScheduleIndex g input} {overlay : List (ScheduleIndex g input)} (layout : AdjacentOverlayLayout base (head :: overlay)) :
                    head.owner ∉ ScheduleOverlay.owners overlay protectedOwners
                    source
                    theorem IndexedGrammar.Aho.AdjacentOverlayLayout.flags_length_pos {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {protectedFlags : List g.flag} {protectedBlocks : List (List g.flag)} {protectedOwners : List (Fin (10 * input.length))} {protectedWord protectedUsed : List (ScheduleAtom g input)} {base : ScheduleBlockLayout g input protectedFlags protectedBlocks protectedOwners protectedWord protectedUsed} {head : ScheduleIndex g input} {overlay : List (ScheduleIndex g input)} (layout : AdjacentOverlayLayout base (head :: overlay)) :
                    0 < (ScheduleOverlay.flags (head :: overlay) protectedFlags).length

                    A nonempty overlay supplies the live-focus premise used by every overlay runner state.

                    source
                    theorem IndexedGrammar.Aho.AdjacentOverlayLayout.replaceHead {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {protectedFlags : List g.flag} {protectedBlocks : List (List g.flag)} {protectedOwners : List (Fin (10 * input.length))} {protectedWord protectedUsed : List (ScheduleAtom g input)} {base : ScheduleBlockLayout g input protectedFlags protectedBlocks protectedOwners protectedWord protectedUsed} {head replacement : ScheduleIndex g input} {overlay : List (ScheduleIndex g input)} (layout : AdjacentOverlayLayout base (head :: overlay)) (block_ne : replacement.flags ≠ []) (owner_eq : replacement.owner = head.owner) (later_eq : replacement.mark.later = head.mark.later) :
                    AdjacentOverlayLayout base (replacement :: overlay)

                    Replace only the mutable head. This is the ghost counterpart of livePushCompress. The lower overlay stack and the shared protected base are unchanged.

                    source
                    theorem IndexedGrammar.Aho.AdjacentOverlayLayout.toProtected {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {protectedFlags : List g.flag} {protectedBlocks : List (List g.flag)} {protectedOwners : List (Fin (10 * input.length))} {protectedWord protectedUsed : List (ScheduleAtom g input)} {base : ScheduleBlockLayout g input protectedFlags protectedBlocks protectedOwners protectedWord protectedUsed} {overlay : List (ScheduleIndex g input)} (layout : AdjacentOverlayLayout base overlay) :
                    ScheduleBlockLayout g input (ScheduleOverlay.flags overlay protectedFlags) (ScheduleOverlay.blocks overlay ++ protectedBlocks) (ScheduleOverlay.owners overlay protectedOwners) (ScheduleOverlay.word overlay protectedWord) (ScheduleOverlay.used overlay protectedUsed)

                    Forget copy-on-write status and seal every overlay block into the ordinary protected layout. This is used exactly when a binary fork starts sharing the overlay between its children.

                    source
                    theorem IndexedGrammar.Aho.AdjacentOverlayLayout.owners_nodup {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {protectedFlags : List g.flag} {protectedBlocks : List (List g.flag)} {protectedOwners : List (Fin (10 * input.length))} {protectedWord protectedUsed : List (ScheduleAtom g input)} {base : ScheduleBlockLayout g input protectedFlags protectedBlocks protectedOwners protectedWord protectedUsed} {overlay : List (ScheduleIndex g input)} (layout : AdjacentOverlayLayout base overlay) :
                    (ScheduleOverlay.owners overlay protectedOwners).Nodup

                    All overlay and protected owners are duplicate-free.

                    source
                    theorem IndexedGrammar.Aho.AdjacentOverlayLayout.private_owners_nodup {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {protectedFlags : List g.flag} {protectedBlocks : List (List g.flag)} {protectedOwners : List (Fin (10 * input.length))} {protectedWord protectedUsed : List (ScheduleAtom g input)} {base : ScheduleBlockLayout g input protectedFlags protectedBlocks protectedOwners protectedWord protectedUsed} {overlay : List (ScheduleIndex g input)} (layout : AdjacentOverlayLayout base overlay) :
                    (List.map ScheduleIndex.owner overlay).Nodup

                    Overlay owners are duplicate-free independently of the protected suffix.

                    source
                    theorem IndexedGrammar.Aho.AdjacentOverlayLayout.private_disjoint_protected {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {protectedFlags : List g.flag} {protectedBlocks : List (List g.flag)} {protectedOwners : List (Fin (10 * input.length))} {protectedWord protectedUsed : List (ScheduleAtom g input)} {base : ScheduleBlockLayout g input protectedFlags protectedBlocks protectedOwners protectedWord protectedUsed} {overlay : List (ScheduleIndex g input)} (layout : AdjacentOverlayLayout base overlay) :
                    (List.map ScheduleIndex.owner overlay).Disjoint protectedOwners

                    No branch-local owner aliases an owner in the shared protected suffix.

                    source
                    theorem IndexedGrammar.Aho.AdjacentOverlayLayout.blocks_nonempty {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {protectedFlags : List g.flag} {protectedBlocks : List (List g.flag)} {protectedOwners : List (Fin (10 * input.length))} {protectedWord protectedUsed : List (ScheduleAtom g input)} {base : ScheduleBlockLayout g input protectedFlags protectedBlocks protectedOwners protectedWord protectedUsed} {overlay : List (ScheduleIndex g input)} (layout : AdjacentOverlayLayout base overlay) (block : List g.flag) :
                    block ∈ ScheduleOverlay.blocks overlay ++ protectedBlocks → block ≠ []

                    Every block in the sealed overlay/protected layout is nonempty.

                    source
                    theorem IndexedGrammar.Aho.AdjacentOverlayLayout.flags_eq_flatten {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {protectedFlags : List g.flag} {protectedBlocks : List (List g.flag)} {protectedOwners : List (Fin (10 * input.length))} {protectedWord protectedUsed : List (ScheduleAtom g input)} {base : ScheduleBlockLayout g input protectedFlags protectedBlocks protectedOwners protectedWord protectedUsed} {overlay : List (ScheduleIndex g input)} (layout : AdjacentOverlayLayout base overlay) :
                    ScheduleOverlay.flags overlay protectedFlags = (ScheduleOverlay.blocks overlay ++ protectedBlocks).flatten

                    The complete visible prefix is exactly the flattening of the sealed block list.

                    source
                    theorem IndexedGrammar.Aho.AdjacentOverlayLayout.owners_length {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {protectedFlags : List g.flag} {protectedBlocks : List (List g.flag)} {protectedOwners : List (Fin (10 * input.length))} {protectedWord protectedUsed : List (ScheduleAtom g input)} {base : ScheduleBlockLayout g input protectedFlags protectedBlocks protectedOwners protectedWord protectedUsed} {overlay : List (ScheduleIndex g input)} (layout : AdjacentOverlayLayout base overlay) :
                    (ScheduleOverlay.owners overlay protectedOwners).length = (ScheduleOverlay.blocks overlay ++ protectedBlocks).length

                    Sealing preserves the exact block/owner alignment required by the protected runner.