Recipes (docs/roleflow.tex, sec:typing, sec:inverse)

A recipe is executable (XRecipe): the line that computes its targets from its arguments. The recipes of lines under roles (xrecs) are one per conditioner, its own line, and one per spine step, the line of its semi-inverse, from the results and the parameters to the consumed arguments. Known R B is the least set containing B and closed under firing recipes of R.

Every recipe holds on every trace (xrecs_holds), conditioners by the trace and spine steps by the left law. The typing (Recov), the density theorem and the schedule all use these recipes and this one fact.

def RoleFlow.Line.ys {S : Type} {Sg : Sig S} (l : Line Sg) (n : ℕ) : List ℕ

The results of a line at scope n.

Equations

• l.ys n = List.range' n l.bs.length

theorem RoleFlow.Line.mem_ys {S : Type} {Sg : Sig S} {l : Line Sg} {n v : ℕ} : v ∈ l.ys n ↔ n ≤ v ∧ v < n + l.bs.length

structure RoleFlow.XRecipe {S : Type} (Sg : Sig S) : Type

An executable recipe tgt ← o(args): the line that computes the targets tgt from its arguments.

• line : Line Sg
• tgt : List ℕ

def RoleFlow.xrecs {S : Type} {Sg : Sig S} : ℕ → List (Line Sg) → List Role → List (XRecipe Sg)

The executable recipes of lines under roles at scope n, in the order of the lines.

Equations

• One or more equations did not get rendered due to their size.
• RoleFlow.xrecs x✝ (l :: ls) (RoleFlow.Role.cond :: ρ) = { line := l, tgt := l.ys x✝ } :: RoleFlow.xrecs (x✝ + l.bs.length) ls ρ
• RoleFlow.xrecs x✝² x✝¹ x✝ = []

theorem RoleFlow.xrecs_cond {S : Type} {Sg : Sig S} (n : ℕ) (l : Line Sg) (ls : List (Line Sg)) (ρ : List Role) : xrecs n (l :: ls) (Role.cond :: ρ) = { line := l, tgt := l.ys n } :: xrecs (n + l.bs.length) ls ρ

theorem RoleFlow.xrecs_spine {S : Type} {Sg : Sig S} (n : ℕ) (l : Line Sg) (ls : List (Line Sg)) (ρ : List Role) {si : SemiInv Sg.Op l.as l.bs} (hsi : Sg.inv l.op = some si) : xrecs n (l :: ls) (Role.spine :: ρ) = { line := { as := l.bs ++ si.ps, bs := si.cs, op := si.op, args := l.ys n ++ List.drop si.k l.args }, tgt := List.take si.k l.args } :: xrecs (n + l.bs.length) ls ρ

theorem RoleFlow.mem_xrecs {S : Type} {Sg : Sig S} {n : ℕ} {l : Line Sg} {ls : List (Line Sg)} {ρ : List Role} {x : XRecipe Sg} (h : x ∈ xrecs n (l :: ls) ρ) : x ∈ xrecs (n + l.bs.length) ls ρ.tail ∨ x = { line := l, tgt := l.ys n } ∨ ∃ (si : SemiInv Sg.Op l.as l.bs), Sg.inv l.op = some si ∧ x = { line := { as := l.bs ++ si.ps, bs := si.cs, op := si.op, args := l.ys n ++ List.drop si.k l.args }, tgt := List.take si.k l.args }

Membership inversion: an executable recipe of l :: ls is one of the remaining lines, the line's own (a conditioner) or that of its semi-inverse (a spine step).

theorem RoleFlow.xrecs_wf {S : Type} {Sg : Sig S} {Γ : List S} {ls : List (Line Sg)} (h : LinesWF Γ ls) (ρ : List Role) {n : ℕ} (hn : Γ.length = n) (x : XRecipe Sg) : x ∈ xrecs n ls ρ → Args (ctxAfter Γ ls) x.line.args x.line.as ∧ Args (ctxAfter Γ ls) x.tgt x.line.bs

The executable recipes are well formed in the context after the lines.

def RoleFlow.Prog.xrecs {S : Type} {Sg : Sig S} (P : Prog Sg) (ρ : List Role) : List (XRecipe Sg)

The executable recipes of P under the roles ρ.

Equations

• P.xrecs ρ = RoleFlow.xrecs P.ctx₀.length P.lines ρ

theorem RoleFlow.Prog.wf_xrecs {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} (h : P.WF) (x : XRecipe Sg) : x ∈ P.xrecs ρ → Args P.ctx x.line.args x.line.as ∧ Args P.ctx x.tgt x.line.bs

Recomputability

inductive RoleFlow.Known {S : Type} {Sg : Sig S} (R : List (XRecipe Sg)) (B : Set ℕ) : ℕ → Prop

Known R B: the least set containing B and closed under firing recipes of R.

• base {S : Type} {Sg : Sig S} {R : List (XRecipe Sg)} {B : Set ℕ} {v : ℕ} : v ∈ B → Known R B v
• fire {S : Type} {Sg : Sig S} {R : List (XRecipe Sg)} {B : Set ℕ} {r : XRecipe Sg} {v : ℕ} : r ∈ R → (∀ w ∈ r.line.args, Known R B w) → v ∈ r.tgt → Known R B v

theorem RoleFlow.Known.trans {S : Type} {Sg : Sig S} {R : List (XRecipe Sg)} {B B' : Set ℕ} (hB : ∀ w ∈ B', Known R B w) {v : ℕ} (h : Known R B' v) : Known R B v

Known values may serve as the base.

theorem RoleFlow.Known.mono {S : Type} {Sg : Sig S} {R : List (XRecipe Sg)} {B B' : Set ℕ} (hB : B ⊆ B') {v : ℕ} (h : Known R B v) : Known R B' v

The recipes hold

theorem RoleFlow.xrecs_holds {S : Type} {Sg : Sig S} [Sorts S] (M : Model Sg) {Γ : List S} {ls : List (Line Sg)} (h : LinesWF Γ ls) (ρ : List Role) {n : ℕ} (hn : Γ.length = n) (v : Val Γ) (x : XRecipe Sg) : x ∈ xrecs n ls ρ → ∀ (h₁ : Args (ctxAfter Γ ls) x.line.args x.line.as) (h₂ : Args (ctxAfter Γ ls) x.tgt x.line.bs), M.sem x.line.op ((trace M ls h v).pick x.line.args h₁) = (trace M ls h v).pick x.tgt h₂

Every executable recipe holds on every trace: conditioners by the trace, spine steps by the left law.