Ports.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Port-wise contracts on uniform families of invocations. Hidden stacks are also binary; they start and finish empty.

def OAI.Fifths.Store.extra line 16
theorem OAI.Fifths.Store.ok_extra line 19

theorem OAI.Fifths.Store.pad_eq line 25

Source documentation

Conditions for identifying a padded port file.

theorem pad_eq (e : K ↪ L) (d : L → List Bool)
    {s : Store J K} {t : Store J L}
    (h : s.ro = t.ro)
    (g : ∀ k, s.st k = t.st (e k))
    (o : ∀ y, (¬ ∃ k, e k = y) → d y = t.st y) :
    s.pad e d = t := by
…

Mentions: OAI.Fifths.Store

def OAI.Fifths.SM.more line 46
Source documentation
Enlarge a machine's collection of hidden stacks.
```
noncomputable def more (e : K ↪ U) (M : SM X J (L ⊕ K) Y) : SM X J (L ⊕ U) Y :=
…
```
Mentions: OAI.Fifths.SM
theorem OAI.Fifths.SM.exec_more line 49
def OAI.Fifths.Works line 68
Source documentation
Uniform relation on port stacks. Context X,J,L,Y are finite in uses that witness computation in the main theorem.
```
def Works {X J I L Y : Type} (x : I → Inputs X J) (S : I → ℕ)
    (a b : I → Store J L) (y : I → Y) : Prop :=
…
```
Mentions: OAI.Fifths.Inputs, OAI.Fifths.Store
def OAI.Fifths.FitsStore line 74
Source documentation
Space for the contents of the port file itself (not input positions).
```
def FitsStore {I J L : Type} (S : I → ℕ) (s : I → Store J L) : Prop :=
…
```
Mentions: OAI.Fifths.Store
theorem OAI.Fifths.Works.source line 82
theorem OAI.Fifths.Works.target line 86
theorem OAI.Fifths.Works.pull line 90
theorem OAI.Fifths.Works.up line 96
theorem OAI.Fifths.Works.direct line 103
theorem OAI.Fifths.Works.addPorts line 119

theorem OAI.Fifths.Works.hide line 156

Source documentation

Hide port stacks used in scratch fashion.

theorem hide (U : Type) [Fintype U]
    (r : Works x S (fun i => (a i).extra U) (fun i => (b i).extra U) y) :
    Works x S a b y := by
…

Mentions: OAI.Fifths.Works

theorem OAI.Fifths.Works.seq line 174
theorem OAI.Fifths.Works.branch line 190