Parsing.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Superstring.BitCode.Ports line 8
Source documentation
A pair of public bit-stack ports and a private register bank.
```
abbrev Ports (K : Type) := Bool ⊕ K
```
def OAI.Superstring.BitCode.inputPort line 10
def OAI.Superstring.BitCode.outputPort line 11
def OAI.Superstring.BitCode.portStore line 13
def OAI.Superstring.BitCode.pairStore line 16
theorem OAI.Superstring.BitCode.portStore_input line 18
theorem OAI.Superstring.BitCode.portStore_output line 20
theorem OAI.Superstring.BitCode.portStore_private line 22
theorem OAI.Superstring.BitCode.update_input line 25
theorem OAI.Superstring.BitCode.update_output line 32
theorem OAI.Superstring.BitCode.update_private line 39
def OAI.Superstring.BitCode.Block.readBit line 47
Source documentation
Move exactly one bit, leaving the suffix and the old output accumulator in place. Empty input is a no-op, but valid parser calls always supply the bit.
```
def readBit {K : Type} (i o : K) : Block K := .branch i .skip
…
```
Mentions: OAI.Superstring.BitCode.Block
theorem OAI.Superstring.BitCode.Block.readBit_exec line 50
theorem OAI.Superstring.BitCode.Block.Exec.ports line 65
Source documentation
Lift a two-port clean routine while leaving an arbitrary disjoint private bank untouched. Public input/output ports are deliberately shared.
```
theorem Exec.ports {K L : Type} [DecidableEq K] [DecidableEq L]
    {b : Block (Ports K)} {x y x' y' : List Bool} {n : ℕ}
    (h : b.Exec (pairStore x y) (pairStore x' y') n)
    (f : K → L) (hf : Function.Injective f) (z : Store L) (hz : ∀ k, z (f k) = []) :
    (b.rename (Sum.map id f)).Exec (portStore x y z) (portStore x' y' z) n := by
…
```
Mentions: OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.Ports, OAI.Superstring.BitCode.pairStore, OAI.Superstring.BitCode.Store, OAI.Superstring.BitCode.Block.Exec, OAI.Superstring.BitCode.portStore
def OAI.Superstring.BitCode.Parses line 89
Source documentation
A linear-time prefix scanner for an explicit encoding. It consumes exactly one encoded value, pushes its reversal onto an accumulator, and restores every private stack to empty, independently of the untouched input suffix.
```
def Parses {α : Type} (e : α → List Bool) : Prop :=
…
```
theorem OAI.Superstring.BitCode.Parses.bit line 96
theorem OAI.Superstring.BitCode.Parses.const line 104
Source documentation
A fixed code word is a prefix encoding of a unit value.
```
theorem const (w : List Bool) : Parses (fun _ : Unit => w) := by
…
```
Mentions: OAI.Superstring.BitCode.Parses
theorem OAI.Superstring.BitCode.Parses.prod line 124
Source documentation
Consecutive self-delimiting values can be parsed in succession without scanning or copying the remaining suffix.
```
theorem prod {α β : Type} {ea : α → List Bool} {eb : β → List Bool}
    (ha : Parses ea) (hb : Parses eb) : Parses (fun p : α × β => ea p.1 ++ eb p.2) := by
…
```
Mentions: OAI.Superstring.BitCode.Parses
def OAI.Superstring.BitCode.listCode line 148
theorem OAI.Superstring.BitCode.Parses.list line 157
Source documentation
Lists of a linearly parsable self-delimiting type are themselves linearly parsable. Exactly one fixed-size private flag is added, not an infinite alphabet or uncharged whole-value operation.
```
theorem list {α : Type} {e : α → List Bool} (hp : Parses e) : Parses (listCode e) := by
…
```
Mentions: OAI.Superstring.BitCode.Parses, OAI.Superstring.BitCode.listCode
theorem OAI.Superstring.BitCode.pairStore_input line 226
theorem OAI.Superstring.BitCode.pairStore_output line 233
def OAI.Superstring.BitCode.Block.pushWord line 243
Source documentation
Write a fixed finite bit word, in the correct order.
```
def pushWord {K : Type} (i : K) : List Bool → Block K
  | [] => .skip
  | b :: bs => .seq (pushWord i bs) (.push i b)
```
Mentions: OAI.Superstring.BitCode.Block
theorem OAI.Superstring.BitCode.Block.pushWord_exec line 247
theorem OAI.Superstring.BitCode.RunsInPolyTime.const line 260
theorem OAI.Superstring.BitCode.RunsInPolyTime.reverseEncoding line 280
theorem OAI.Superstring.BitCode.RunsInPolyTime.fst line 290
Source documentation
First projection from two consecutive self-delimiting values.
```
theorem fst {α β : Type} {ea : α → List Bool} (eb : β → List Bool) (hp : Parses ea) :
    RunsInPolyTime (fun p : α × β => ea p.1 ++ eb p.2) ea Prod.fst := by
…
```
Mentions: OAI.Superstring.BitCode.Parses, OAI.Superstring.BitCode.RunsInPolyTime
theorem OAI.Superstring.BitCode.RunsInPolyTime.snd line 307
Source documentation
Second projection consumes just the first value; it does not copy or re-parse the tail. Accumulated garbage is explicitly erased by of_observed.
```
theorem snd {α β : Type} {ea : α → List Bool} (eb : β → List Bool) (hp : Parses ea) :
    RunsInPolyTime (fun p : α × β => ea p.1 ++ eb p.2) eb Prod.snd := by
…
```
Mentions: OAI.Superstring.BitCode.Parses, OAI.Superstring.BitCode.RunsInPolyTime
theorem OAI.Superstring.BitCode.RunsInPolyTime.cons line 319

theorem OAI.Superstring.BitCode.Block.move_exec line 340

Source documentation

Destructive linear concatenation, preserving every unrelated register.

theorem move_exec (i j scratch : K) (hij : i ≠ j) (hit : i ≠ scratch) (hjt : j ≠ scratch)
    (s : Store K) (ht : s scratch = []) :
    (move i j scratch).Exec s
      (Function.update (Function.update s i []) j (s i ++ s j)) (8 * (s i).length + 2) := by
…

Mentions: OAI.Superstring.BitCode.Store, OAI.Superstring.BitCode.Block.move, OAI.Superstring.BitCode.Block.Exec