Flow.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

Compile bounded-stack algorithms whose steps may themselves be space-bounded computations. A Flow is just semantics, no computability in its definition; the compilation criterion requires a uniformly computable step on the packed code, in the same unit being bounded. The interpreted machine manipulates ONE GLOBAL word, outside the activation stack. To charge the stack we measure the sizes of suspended (continuation) frame codes.

inductive OAI.Fifths.FlowMove line 15
structure OAI.Fifths.Flow line 20
def OAI.Fifths.Flow.fee line 31
Source documentation
Cost to stack this frame in our fixed prefix encoding.
```
def fee (f : m.F) := 2*(m.packF f).size + 1
```

inductive OAI.Fifths.Flow.Executes line 37

Source documentation

Contract of one activation. B upper bounds the sum of fees of frames simultaneously suspended by (or under) this invocation. Current frame not included; uniformly small active frame will also be required.

inductive Executes : ℕ → m.G → m.F → m.G → Prop
  | done {B g f h} (step : m.act g f = (h,.finish)) :
    Executes B g f h
  | next {B g f h j w}
    (step : m.act g f = (h,.cont j))
    (after : Executes B h j w) :
    Executes B g f w
  | call {A B g f h j k u w}
    (step : m.act g f = (h,.call j k))
    (child : Executes A h j u)
    (bound : m.fee k + A ≤ B)
    (after : Executes B u k w) :
…

Mentions: OAI.Fifths.Flow.next

theorem OAI.Fifths.Flow.Executes.up line 52

inductive OAI.Fifths.Flow.Continues line 62

Source documentation

Reaches another frame at the same level, with any children finished. (For use proving Executes via a schedule of loops.)

inductive Continues : ℕ → m.G → m.F → m.G → m.F → Prop
  | stop {B g f} : Continues B g f g f
  | next {B g f h j w l}
    (step : m.act g f = (h,.cont j))
    (after : Continues B h j w l) :
    Continues B g f w l
  | call {A B g f h j k u w l}
    (step : m.act g f = (h,.call j k))
    (child : m.Executes A h j u)
    (bound : m.fee k + A ≤ B)
    (after : Continues B u k w l) :
    Continues B g f w l
…

Mentions: OAI.Fifths.Flow.next

theorem OAI.Fifths.Flow.Continues.trans line 77
theorem OAI.Fifths.Flow.Continues.then_exec line 84
def OAI.Fifths.Flow.packFs line 92
theorem OAI.Fifths.Flow.packFs_cons line 95
theorem OAI.Fifths.Flow.pack_ne line 99
abbrev OAI.Fifths.Flow.Cfg line 105
def OAI.Fifths.Flow.next line 106
def OAI.Fifths.Flow.path line 116
theorem OAI.Fifths.Flow.path_add line 120
structure OAI.Fifths.Flow.Segment line 126
Source documentation
Segment of n flow moves. Suspended-frame total at each nonfinal point bounded by B. Active frame exists at such points.
```
structure Segment (s t : m.Cfg) (n B : ℕ) : Prop where
…
```
theorem OAI.Fifths.Flow.Segment.mono line 133
theorem OAI.Fifths.Flow.Segment.trans line 135
theorem OAI.Fifths.Flow.Segment.one line 146
theorem OAI.Fifths.Flow.trajectory line 154
def OAI.Fifths.Flow.tag line 170
Source comment
Code for a move: a leading tag, plus zero-padded first and second frame encodings.
```
def tag : FlowMove m.F → ℕ
  | .finish => 0
  | .cont _ => 1
  | .call _ _ => 2
```
Mentions: OAI.Fifths.FlowMove
def OAI.Fifths.Flow.arg1 line 174
def OAI.Fifths.Flow.arg2 line 177
def OAI.Fifths.Flow.packMove line 180
def OAI.Fifths.Flow.input line 185
Source documentation
Inspect the current activation in the presence of immutable integer parameter cp.
```
def input (cp : ℕ) (g : m.G) (f : m.F) :=
…
```
def OAI.Fifths.Flow.code line 188
theorem OAI.Fifths.Flow.next_code line 191
abbrev OAI.Fifths.Flow.Points line 207
Source documentation
Local indexed hypothesis. Global pool and program counter may be any encoded state of the corresponding semantic type.
```
abbrev Points (M : I → Flow) := Σ i, (M i).G × (M i).F
```
Mentions: OAI.Fifths.Flow
def OAI.Fifths.Flow.uniform line 209

theorem OAI.Fifths.Flow.uniform_move line 215

Source comment

Apply the move over a nonempty stack, incorporating local step computation.

theorem uniform_move {M : I → Flow} (p : uniform M x S cp)
    {U : Type} (e : U → I) (g : ∀ i, (M (e i)).G)
    (f : ∀ i, (M (e i)).F) (l : ∀ i, List (M (e i)).F) (s : U → ℕ)
    (h : Comp (fun i => x (e i)) (fun i => S (e i)) s
      (fun i => (M (e i)).code (cp (e i)) (g i,f i :: l i))) :
    Comp (fun i => x (e i)) (fun i => S (e i)) s
      (fun i => (M (e i)).code (cp (e i)) ((M (e i)).next (g i,f i :: l i))) := by
…

Mentions: OAI.Fifths.Flow, OAI.Fifths.Flow.uniform, OAI.Fifths.Comp, OAI.Fifths.Flow.code, OAI.Fifths.Flow.next

theorem OAI.Fifths.Flow.uniform_result line 235