LanglibTicketed shadow owners for Aho's compressed scheduler #
The primary owner bank records productive events at block endpoints. A temporarily unaligned head cannot use that bank, since it need not end at an event. Before such a head is buried under another block, it is sealed into a disjoint shadow bank. Its ticket is the productive event at the start of the block.
For an input of length n, productive owners occupy [0, 2n - 1), their shadows occupy
[2n - 1, 4n - 2), and the last two slots are the temporary scratch and transient owners.
This file contains only the owner arithmetic and semantic ledgers. It does not perform any
machine move.
First physical slot of the bank of productive-event shadows.
Equations
- IndexedGrammar.Aho.shadowOwnerOffset input = 2 * input.length - 1
Instances For
def
IndexedGrammar.Aho.ProductiveOwnerWindow.shadowEventOwner
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(d : ℕ)
(hd : d ∈ parse.eventDepths)
:
The shadow of a canonical event owner. The shadow has the same root-relative productive ticket, translated into the disjoint second bank.
Equations
- window.shadowEventOwner d hd = ⟨IndexedGrammar.Aho.shadowOwnerOffset input + ↑(window.eventOwner d hd), ⋯⟩
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.shadowEventOwner_val
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(d : ℕ)
(hd : d ∈ parse.eventDepths)
:
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.shadowEventOwner_injective
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
{d e : ℕ}
(hd : d ∈ parse.eventDepths)
(he : e ∈ parse.eventDepths)
:
window.shadowEventOwner d hd = window.shadowEventOwner e he → d = e
Shadowing preserves injectivity of productive event tickets.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.shadowEventOwner_congr
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{stack stack' : List g.flag}
{w w' : List T}
{parse : g.NFParse A stack w}
{parse' : g.NFParse B stack' w'}
(window : ProductiveOwnerWindow parse)
(window' : ProductiveOwnerWindow parse')
{d e : ℕ}
(hd : d ∈ parse.eventDepths)
(he : e ∈ parse'.eventDepths)
(howner : window.eventOwner d hd = window'.eventOwner e he)
:
Any equality of primary event owners lifts to the corresponding equality in the shadow bank. This is the generic bridge used by unary and binary parse transports.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.shadowEventOwner_pop_succ
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = some f}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none]}
{rest : g.NFParse B stack w}
(window : ProductiveOwnerWindow (NFParse.pop hr hlhs hc hrhs rest))
{d : ℕ}
(hd : d ∈ rest.eventDepths)
:
Shadow owners commute with the one-position event shift of a pop.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.shadowEventOwner_push
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]}
{rest : g.NFParse B (f :: stack) w}
(window : ProductiveOwnerWindow (NFParse.push hr hlhs hc hrhs rest))
{d : ℕ}
(hd : d ∈ (NFParse.push hr hlhs hc hrhs rest).eventDepths)
:
window.shadowEventOwner d hd = window.pushChild.shadowEventOwner (NFParse.pushEventPreimage rest.eventDepths d) ⋯
Shadow owners commute with the canonical preimage of a push event.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.shadowEventOwner_push_pos
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]}
{rest : g.NFParse B (f :: stack) w}
(window : ProductiveOwnerWindow (NFParse.push hr hlhs hc hrhs rest))
{d : ℕ}
(hdpos : 0 < d)
(hd : d + 1 ∈ rest.eventDepths)
:
Positive push events and their one-deeper child events have the same shadow owner.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.eventOwner_ne_shadowEventOwner
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
{d e : ℕ}
(hd : d ∈ parse.eventDepths)
(he : e ∈ parse.eventDepths)
:
Primary and shadow banks are physically disjoint.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.shadowEventOwner_ne_scratchOwner
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
{d : ℕ}
(hd : d ∈ parse.eventDepths)
(hinput : 0 < input.length)
:
A shadow owner is never the temporary scratch slot.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.shadowEventOwner_ne_transientOwner
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
{d : ℕ}
(hd : d ∈ parse.eventDepths)
(hinput : 0 < input.length)
:
A shadow owner is never the temporary collision slot.
def
IndexedGrammar.Aho.OutsideShadowWindow
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(owner : Fin (10 * input.length))
:
An owner does not use a shadow ticket belonging to the active productive window. Primary owners and the two temporary owners satisfy this automatically.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
IndexedGrammar.Aho.OutsideShadowWindow.shadowEventOwner_not_outside
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
{d : ℕ}
(hd : d ∈ parse.eventDepths)
:
¬OutsideShadowWindow window (window.shadowEventOwner d hd)
A local shadow event lies strictly inside its shadow-ticket window.
theorem
IndexedGrammar.Aho.OutsideShadowWindow.eventOwner
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
{d : ℕ}
(hd : d ∈ parse.eventDepths)
:
OutsideShadowWindow window (window.eventOwner d hd)
Every primary productive owner lies before the shadow bank.
theorem
IndexedGrammar.Aho.OutsideShadowWindow.scratchOwner
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(hinput : 0 < input.length)
:
OutsideShadowWindow window (ProductiveOwnerWindow.scratchOwner hinput)
The temporary scratch slot lies after every shadow window.
theorem
IndexedGrammar.Aho.OutsideShadowWindow.transientOwner
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(hinput : 0 < input.length)
:
OutsideShadowWindow window (ProductiveOwnerWindow.transientOwner hinput)
The temporary collision slot lies after every shadow window.
theorem
IndexedGrammar.Aho.OutsideShadowWindow.genericOwner
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
{owner : Fin (10 * input.length)}
(howner : owner ∈ genericOwnerRange g input)
:
OutsideShadowWindow window owner
Every reusable generic label lies beyond every shadow-owner window.
theorem
IndexedGrammar.Aho.OutsideShadowWindow.transport
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{stack stack' : List g.flag}
{w w' : List T}
{parse : g.NFParse A stack w}
{residual : g.NFParse B stack' w'}
(window : ProductiveOwnerWindow parse)
(hcount : residual.productiveCount = parse.productiveCount)
{owner : Fin (10 * input.length)}
(hout : OutsideShadowWindow window owner)
:
OutsideShadowWindow (window.transport hcount) owner
Equal-count transports preserve shadow-window exclusion.
theorem
IndexedGrammar.Aho.OutsideShadowWindow.binaryLeft
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
(window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right))
{owner : Fin (10 * input.length)}
(hout : OutsideShadowWindow window owner)
:
OutsideShadowWindow window.binaryLeft owner
Shadow tickets outside a binary parent window remain outside its left child.
theorem
IndexedGrammar.Aho.OutsideShadowWindow.binaryRight
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
(window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right))
{owner : Fin (10 * input.length)}
(hout : OutsideShadowWindow window owner)
:
OutsideShadowWindow window.binaryRight owner
Shadow tickets outside a binary parent window remain outside its right child.
theorem
IndexedGrammar.Aho.OutsideShadowWindow.binaryZero_left
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
(window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right))
(hzero : 0 ∈ (NFParse.binary hr hlhs hc hrhs left right).eventDepths)
:
OutsideShadowWindow window.binaryLeft (window.shadowEventOwner 0 hzero)
The binary root ticket is already outside the left child's shadow window.
theorem
IndexedGrammar.Aho.OutsideShadowWindow.binaryZero_right
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
(window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right))
(hzero : 0 ∈ (NFParse.binary hr hlhs hc hrhs left right).eventDepths)
:
OutsideShadowWindow window.binaryRight (window.shadowEventOwner 0 hzero)
The binary root ticket is already outside the right child's shadow window.
def
IndexedGrammar.Aho.blockStart
{T : Type}
{g : IndexedGrammar T}
(blocks : List (List g.flag))
(i : Fin blocks.length)
:
Concrete start position of block i. Unlike blockEndpoint, this excludes block i
itself.
Equations
- IndexedGrammar.Aho.blockStart blocks i = (List.take (↑i) blocks).flatten.length
Instances For
@[simp]
theorem
IndexedGrammar.Aho.blockStart_cons_zero
{T : Type}
{g : IndexedGrammar T}
(block : List g.flag)
(blocks : List (List g.flag))
:
@[simp]
theorem
IndexedGrammar.Aho.blockStart_cons_succ
{T : Type}
{g : IndexedGrammar T}
(block : List g.flag)
(blocks : List (List g.flag))
(i : Fin blocks.length)
:
structure
IndexedGrammar.Aho.ShadowStartLayout
{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)
(window : ProductiveOwnerWindow parse)
(blocks : List (List g.flag))
(owners : List (Fin (10 * input.length)))
:
Productive provenance for shadow-bank owners aligned with block starts. Non-shadow owners fall into the outside alternative automatically.
- owner_at (i : Fin blocks.length) : (∃ (hd : blockStart blocks i ∈ parse.eventDepths), blockOwnerAt owners ⋯ i = window.shadowEventOwner (blockStart blocks i) hd) ∨ OutsideShadowWindow window (blockOwnerAt owners ⋯ i)
Instances For
theorem
IndexedGrammar.Aho.ShadowStartLayout.nil
{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}
{window : ProductiveOwnerWindow parse}
:
ShadowStartLayout parse window [] []
The empty block partition has the empty shadow ledger.
theorem
IndexedGrammar.Aho.ShadowStartLayout.ofOutside
{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}
{window : ProductiveOwnerWindow parse}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
(hlen : owners.length = blocks.length)
(hne : ∀ block ∈ blocks, block ≠ [])
(hout : ∀ (i : Fin blocks.length), OutsideShadowWindow window (blockOwnerAt owners hlen i))
:
ShadowStartLayout parse window blocks owners
A layout all of whose owners are outside the active shadow window.
theorem
IndexedGrammar.Aho.ShadowStartLayout.transport
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A B : g.nt}
{stack stack' : List g.flag}
{w w' : List T}
{parse : g.NFParse A stack w}
{residual : g.NFParse B stack' w'}
{window : ProductiveOwnerWindow parse}
{residualWindow : ProductiveOwnerWindow residual}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
(layout : ShadowStartLayout parse window blocks owners)
(outside :
∀ (owner : Fin (10 * input.length)), OutsideShadowWindow window owner → OutsideShadowWindow residualWindow owner)
(ticket_shift :
∀ (i : Fin blocks.length) (hd : blockStart blocks i ∈ parse.eventDepths),
∃ (hd' : blockStart blocks i ∈ residual.eventDepths),
window.shadowEventOwner (blockStart blocks i) hd = residualWindow.shadowEventOwner (blockStart blocks i) hd')
:
ShadowStartLayout residual residualWindow blocks owners
Generic parse/window transport. Local shadow tickets are transported explicitly; owners already outside the old window must remain outside the new one.
theorem
IndexedGrammar.Aho.ShadowStartLayout.cons
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A B : g.nt}
{stack stack' : List g.flag}
{w w' : List T}
{parse : g.NFParse A stack w}
{nextParse : g.NFParse B stack' w'}
{window : ProductiveOwnerWindow parse}
{nextWindow : ProductiveOwnerWindow nextParse}
{block : List g.flag}
{blocks : List (List g.flag)}
{owner : Fin (10 * input.length)}
{owners : List (Fin (10 * input.length))}
(layout : ShadowStartLayout parse window blocks owners)
(block_ne : block ≠ [])
(head_owner :
(∃ (hd : 0 ∈ nextParse.eventDepths), owner = nextWindow.shadowEventOwner 0 hd) ∨ OutsideShadowWindow nextWindow owner)
(outside :
∀ (candidate : Fin (10 * input.length)),
OutsideShadowWindow window candidate → OutsideShadowWindow nextWindow candidate)
(ticket_shift :
∀ (i : Fin blocks.length) (hd : blockStart blocks i ∈ parse.eventDepths),
∃ (hd' : block.length + blockStart blocks i ∈ nextParse.eventDepths),
window.shadowEventOwner (blockStart blocks i) hd = nextWindow.shadowEventOwner (block.length + blockStart blocks i) hd')
:
ShadowStartLayout nextParse nextWindow (block :: blocks) (owner :: owners)
Prepend one block, shifting every old block start by its length.
theorem
IndexedGrammar.Aho.ShadowStartLayout.tail
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A B : g.nt}
{stack stack' : List g.flag}
{w w' : List T}
{parse : g.NFParse A stack w}
{residual : g.NFParse B stack' w'}
{window : ProductiveOwnerWindow parse}
{residualWindow : ProductiveOwnerWindow residual}
{block : List g.flag}
{blocks : List (List g.flag)}
{owner : Fin (10 * input.length)}
{owners : List (Fin (10 * input.length))}
(layout : ShadowStartLayout parse window (block :: blocks) (owner :: owners))
(outside :
∀ (candidate : Fin (10 * input.length)),
OutsideShadowWindow window candidate → OutsideShadowWindow residualWindow candidate)
(ticket_shift :
∀ (i : Fin blocks.length) (hd : block.length + blockStart blocks i ∈ parse.eventDepths),
∃ (hd' : blockStart blocks i ∈ residual.eventDepths),
window.shadowEventOwner (block.length + blockStart blocks i) hd = residualWindow.shadowEventOwner (blockStart blocks i) hd')
:
ShadowStartLayout residual residualWindow blocks owners
Remove the first block, shifting every remaining start back by its length.
theorem
IndexedGrammar.Aho.ShadowStartLayout.binaryLeft
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
{window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right)}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
(layout : ShadowStartLayout (NFParse.binary hr hlhs hc hrhs left right) window blocks owners)
:
ShadowStartLayout left window.binaryLeft blocks owners
Restrict a shadow-start layout to the left binary child. A ticket belonging to the binary root or the right subtree becomes outside the child's shadow window.
theorem
IndexedGrammar.Aho.ShadowStartLayout.binaryRight
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
{window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right)}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
(layout : ShadowStartLayout (NFParse.binary hr hlhs hc hrhs left right) window blocks owners)
:
ShadowStartLayout right window.binaryRight blocks owners
Restrict a shadow-start layout to the right binary child. A ticket belonging to the binary root or the left subtree becomes outside the child's shadow window.
theorem
IndexedGrammar.Aho.ShadowStartLayout.reownerHead
{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}
{window : ProductiveOwnerWindow parse}
{block : List g.flag}
{blocks : List (List g.flag)}
{oldOwner newOwner : Fin (10 * input.length)}
{owners : List (Fin (10 * input.length))}
(layout : ShadowStartLayout parse window (block :: blocks) (oldOwner :: owners))
(head_owner :
(∃ (hd : 0 ∈ parse.eventDepths), newOwner = window.shadowEventOwner 0 hd) ∨ OutsideShadowWindow window newOwner)
:
ShadowStartLayout parse window (block :: blocks) (newOwner :: owners)
Replace the owner of the first block while keeping all shadow-start classifications below it unchanged.
theorem
IndexedGrammar.Aho.ShadowStartLayout.shadowEventOwner_not_mem_owners
{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}
{window : ProductiveOwnerWindow parse}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
(layout : ShadowStartLayout parse window blocks owners)
{d : ℕ}
(hd : d ∈ parse.eventDepths)
(hdiff : ∀ (i : Fin blocks.length), d ≠ blockStart blocks i)
:
window.shadowEventOwner d hd ∉ owners
A local shadow event absent from every represented block start is absent from all selected owners.
theorem
IndexedGrammar.Aho.ShadowStartLayout.shadowEventOwner_zero_not_mem_tail
{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}
{window : ProductiveOwnerWindow parse}
{block : List g.flag}
{blocks : List (List g.flag)}
{owner : Fin (10 * input.length)}
{owners : List (Fin (10 * input.length))}
(layout : ShadowStartLayout parse window (block :: blocks) (owner :: owners))
(hzero : 0 ∈ parse.eventDepths)
:
window.shadowEventOwner 0 hzero ∉ owners
The shadow ticket at the start of the first block is fresh from every lower block owner. This is the active-layout fact used when a scratch head is sealed at a binary event.
theorem
IndexedGrammar.Aho.ShadowStartLayout.shadowEventOwner_zero_fresh_of_head_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}
{window : ProductiveOwnerWindow parse}
{block : List g.flag}
{blocks : List (List g.flag)}
{owner : Fin (10 * input.length)}
{owners : List (Fin (10 * input.length))}
(layout : ShadowStartLayout parse window (block :: blocks) (owner :: owners))
(hzero : 0 ∈ parse.eventDepths)
(hhead : window.shadowEventOwner 0 hzero ≠ owner)
:
window.shadowEventOwner 0 hzero ∉ owner :: owners
Replacing a non-shadow head by its depth-zero shadow yields a physically fresh owner as soon as the old head is known distinct from that shadow.
theorem
IndexedGrammar.Aho.ShadowStartLayout.shadowEventOwner_second_fresh
{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}
{window : ProductiveOwnerWindow parse}
{first second : List g.flag}
{blocks : List (List g.flag)}
{firstOwner secondOwner : Fin (10 * input.length)}
{owners : List (Fin (10 * input.length))}
(layout : ShadowStartLayout parse window (first :: second :: blocks) (firstOwner :: secondOwner :: owners))
(hstart : first.length ∈ parse.eventDepths)
(hfirst : window.shadowEventOwner first.length hstart ≠ firstOwner)
:
window.shadowEventOwner first.length hstart ∉ firstOwner :: owners
When the second block is sealed at the end of a newly prepended first block, its shadow ticket is fresh from the new head and from every block below it.
def
IndexedGrammar.Aho.ShadowOwnedFrame
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
(parse : g.NFParse A stack w)
(window : ProductiveOwnerWindow parse)
(owner : Fin (10 * input.length))
:
Every open-frame owner has no ticket in the active shadow window. Primary owners satisfy this automatically. A local shadow-start owner can enter an open frame only after descent through the productive event at its start, at which point that ticket belongs to an ancestor window and is outside the active child window.
Equations
- IndexedGrammar.Aho.ShadowOwnedFrame parse window owner = IndexedGrammar.Aho.OutsideShadowWindow window owner
Instances For
structure
IndexedGrammar.Aho.ShadowOwnedFrames
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
(parse : g.NFParse A stack w)
(window : ProductiveOwnerWindow parse)
(owners : List (Fin (10 * input.length)))
:
Shadow-ticket provenance for every open frame.
- owner_at (owner : Fin (10 * input.length)) : owner ∈ owners → ShadowOwnedFrame parse window owner
Instances For
theorem
IndexedGrammar.Aho.ShadowOwnedFrames.nil
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{window : ProductiveOwnerWindow parse}
:
ShadowOwnedFrames parse window []
theorem
IndexedGrammar.Aho.ShadowOwnedFrames.cons
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{window : ProductiveOwnerWindow parse}
{owner : Fin (10 * input.length)}
{owners : List (Fin (10 * input.length))}
(head : ShadowOwnedFrame parse window owner)
(tail : ShadowOwnedFrames parse window owners)
:
ShadowOwnedFrames parse window (owner :: owners)
theorem
IndexedGrammar.Aho.ShadowOwnedFrames.transport
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{stack stack' : List g.flag}
{w w' : List T}
{parse : g.NFParse A stack w}
{residual : g.NFParse B stack' w'}
{window : ProductiveOwnerWindow parse}
{residualWindow : ProductiveOwnerWindow residual}
{owners : List (Fin (10 * input.length))}
(frames : ShadowOwnedFrames parse window owners)
(shift :
∀ (owner : Fin (10 * input.length)),
ShadowOwnedFrame parse window owner → ShadowOwnedFrame residual residualWindow owner)
:
ShadowOwnedFrames residual residualWindow owners
theorem
IndexedGrammar.Aho.ShadowOwnedFrames.transportEqual
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{stack stack' : List g.flag}
{w w' : List T}
{parse : g.NFParse A stack w}
{residual : g.NFParse B stack' w'}
{window : ProductiveOwnerWindow parse}
{owners : List (Fin (10 * input.length))}
(frames : ShadowOwnedFrames parse window owners)
(hcount : residual.productiveCount = parse.productiveCount)
:
ShadowOwnedFrames residual (window.transport hcount) owners
Equal-count window transport preserves the outside-only frame invariant.
theorem
IndexedGrammar.Aho.ShadowOwnedFrames.binaryLeft
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
{window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right)}
{owners : List (Fin (10 * input.length))}
(frames : ShadowOwnedFrames (NFParse.binary hr hlhs hc hrhs left right) window owners)
:
ShadowOwnedFrames left window.binaryLeft owners
Parent frame tickets remain outside the left binary child shadow window.
theorem
IndexedGrammar.Aho.ShadowOwnedFrames.binaryRight
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
{window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right)}
{owners : List (Fin (10 * input.length))}
(frames : ShadowOwnedFrames (NFParse.binary hr hlhs hc hrhs left right) window owners)
:
ShadowOwnedFrames right window.binaryRight owners
Parent frame tickets remain outside the right binary child shadow window.
theorem
IndexedGrammar.Aho.ShadowOwnedFrames.perm
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{window : ProductiveOwnerWindow parse}
{owners owners' : List (Fin (10 * input.length))}
(frames : ShadowOwnedFrames parse window owners)
(hperm : owners'.Perm owners)
:
ShadowOwnedFrames parse window owners'
theorem
IndexedGrammar.Aho.ShadowOwnedFrames.shadowEventOwner_not_mem
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{window : ProductiveOwnerWindow parse}
{owners : List (Fin (10 * input.length))}
(frames : ShadowOwnedFrames parse window owners)
{d : ℕ}
(hd : d ∈ parse.eventDepths)
:
window.shadowEventOwner d hd ∉ owners
No local shadow event can be held by an open frame.
structure
IndexedGrammar.Aho.ShadowOwnerLedger
{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)
(window : ProductiveOwnerWindow parse)
(cursor : ScheduleCursor g input)
:
Cursor-level decomposition of shadow tickets. The active start layout is supplied by the runner because its block list is mode-specific.
- frames : ShadowOwnedFrames parse window cursor.frameOwners
- prefixLedger : PrefixFrameLedger cursor
Instances For
def
IndexedGrammar.Aho.ShadowOwnerLedger.root
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(parse : g.NFParse g.initial [] input)
:
ShadowOwnerLedger parse (ProductiveOwnerWindow.root parse) (initialScheduleCursor parse)
The canonical root cursor has an empty shadow ledger.
Equations
Instances For
theorem
IndexedGrammar.Aho.ShadowOwnerLedger.shadowEventOwner_not_mem_indexOwners
{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}
{window : ProductiveOwnerWindow parse}
{cursor : ScheduleCursor g input}
(ledger : ShadowOwnerLedger parse window cursor)
{blocks : List (List g.flag)}
(layout : ShadowStartLayout parse window blocks ledger.active)
(hfocus : List.filterMap ScheduleAtom.indexOwner? [cursor.focus] = [])
{d : ℕ}
(hd : d ∈ parse.eventDepths)
(hdiff : ∀ (i : Fin blocks.length), d ≠ blockStart blocks i)
:
window.shadowEventOwner d hd ∉ cursor.indexOwners
Whole-cursor shadow freshness. Active right-side owners are excluded by their block starts, the common suffix is outside the shadow window, and prefix indices are reduced to the explicit frame-freshness premise.
theorem
IndexedGrammar.Aho.ShadowOwnerLedger.shadowEventOwner_not_mem_indexOwners_of_active
{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}
{window : ProductiveOwnerWindow parse}
{cursor : ScheduleCursor g input}
(ledger : ShadowOwnerLedger parse window cursor)
(hfocus : List.filterMap ScheduleAtom.indexOwner? [cursor.focus] = [])
{d : ℕ}
(hd : d ∈ parse.eventDepths)
(hactiveFresh : window.shadowEventOwner d hd ∉ ledger.active)
:
window.shadowEventOwner d hd ∉ cursor.indexOwners
Whole-cursor shadow freshness from an explicit active-list freshness fact. Prefix frames and the unselected right suffix are discharged entirely by the shadow ledger.
def
IndexedGrammar.Aho.ShadowOwnerLedger.transport
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A B : g.nt}
{stack stack' : List g.flag}
{w w' : List T}
{parse : g.NFParse A stack w}
{residual : g.NFParse B stack' w'}
{window : ProductiveOwnerWindow parse}
{old new : ScheduleCursor g input}
(ledger : ShadowOwnerLedger parse window old)
(residualWindow : ProductiveOwnerWindow residual)
(hright : List.filterMap ScheduleAtom.indexOwner? new.right = ledger.active ++ ledger.outside)
(houtside : ∀ owner ∈ ledger.outside, OutsideShadowWindow residualWindow owner)
(hframes : ShadowOwnedFrames residual residualWindow new.frameOwners)
(hprefix : PrefixFrameLedger new)
:
ShadowOwnerLedger residual residualWindow new
Generic cursor reassembly after transporting the active parse/window.
Equations
- One or more equations did not get rendered due to their size.