Role typing (docs/roleflow.tex, sec:typing)

The judgement Typed Sg O Γ Λ D ls xs ρ has the output sorts O, the context Γ (its length is the next free position), the live set Λ and the supports D; ls are the remaining lines, xs the returned positions and ρ the roles. Every rule checks the sorts of its line, and Ret those of the returned variables, so a typing includes well-formedness (Typed.wf). The support D.getD v ∅ of v stands for its live ancestors: empty for a weight and {x} for an input; a conditioner's results get the union of its arguments' supports (condSupp), and a spine step replaces the consumed arguments in every support that meets them by its results and its parameters' supports (spineSupp).

The invariant Recov (every variable is recomputable from the weights and its support) is preserved from each rule's conclusion to its premise (Recov.init, Recov.cond, Recov.spine), for a fixed list R of recipes that contains those of the lines (xrecs). Typed.induction_recov threads Recov through a whole derivation.

Typed is defined by recursion on the lines, so it is decidable as it stands (decTyped, Prog.decTyped, for decidable equality of sorts). Nothing here uses measure theory.

The judgement

@[reducible, inline]

abbrev RoleFlow.spineLive {S : Type} {Sg : Sig S} (Λ : Finset ℕ) (l : Line Sg) (k n : ℕ) : Finset ℕ

The live set after a spine step at scope n solving the first k arguments: the consumed arguments leave, the results [n, n + |ys|) enter.

Equations

• RoleFlow.spineLive Λ l k n = Λ \ (List.take k l.args).toFinset ∪ Finset.Ico n (n + l.bs.length)

def RoleFlow.initSupp (nw n : ℕ) : List (Finset ℕ)

The supports at the start: none for a weight, itself for an input.

Equations

• RoleFlow.initSupp nw n = List.map (fun (v : ℕ) => if v < nw then ∅ else {v}) (List.range n)

def RoleFlow.condSupp {S : Type} {Sg : Sig S} (D : List (Finset ℕ)) (l : Line Sg) : List (Finset ℕ)

The supports after a conditioner: each result has the union of its arguments' supports.

Equations

• RoleFlow.condSupp D l = D ++ List.replicate l.bs.length (l.args.toFinset.biUnion fun (x : ℕ) => D.getD x ∅)

def RoleFlow.spineSupp {S : Type} {Sg : Sig S} (D : List (Finset ℕ)) (l : Line Sg) (k n : ℕ) : List (Finset ℕ)

The supports after a spine step at scope n solving the first k arguments: a support that meets the consumed arguments drops them and gains the results and the parameters' supports; each result supports itself.

Equations

• One or more equations did not get rendered due to their size.

def RoleFlow.Typed {S : Type} (Sg : Sig S) (O : List S) : List S → Finset ℕ → List (Finset ℕ) → List (Line Sg) → List ℕ → List Role → Prop

Γ; Λ; D ⊢ e : O with roles ρ, for the lines ls and the returned positions xs: the rules Ret, Cond and Spine, by recursion on the lines. Each rule also checks the sorts of its line, so a typing includes well-formedness (Typed.wf).

Equations

• One or more equations did not get rendered due to their size.
• RoleFlow.Typed Sg O x✝³ x✝² x✝¹ [] x✝ [] = (x✝.Nodup ∧ x✝.toFinset = x✝² ∧ RoleFlow.Args x✝³ x✝ O)
• RoleFlow.Typed Sg O x✝³ x✝² x✝¹ (l :: ls) x✝ (RoleFlow.Role.cond :: ρ) = (RoleFlow.Args x✝³ l.args l.as ∧ RoleFlow.Typed Sg O (x✝³ ++ l.bs) x✝² (RoleFlow.condSupp x✝¹ l) ls x✝ ρ)
• RoleFlow.Typed Sg O x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = False

@[implicit_reducible]

instance RoleFlow.decTyped {S : Type} {Sg : Sig S} [DecidableEq S] (O Γ : List S) (Λ : Finset ℕ) (D : List (Finset ℕ)) (ls : List (Line Sg)) (xs : List ℕ) (ρ : List Role) : Decidable (Typed Sg O Γ Λ D ls xs ρ)

Equations

• One or more equations did not get rendered due to their size.
• RoleFlow.decTyped O x✝³ x✝² x✝¹ [] x✝ [] = RoleFlow.decTyped._aux_1 O x✝³ x✝² x✝¹ x✝
• RoleFlow.decTyped O x✝³ x✝² x✝¹ [] x✝ (head :: tail) = isFalse ⋯
• RoleFlow.decTyped O x✝³ x✝² x✝¹ (head :: tail) x✝ [] = isFalse ⋯

theorem RoleFlow.Typed.wf {S : Type} {Sg : Sig S} {O Γ : List S} {Λ : Finset ℕ} {D : List (Finset ℕ)} {ls : List (Line Sg)} {xs : List ℕ} {ρ : List Role} : Typed Sg O Γ Λ D ls xs ρ → LinesWF Γ ls ∧ Args (ctxAfter Γ ls) xs O

A typing includes well-formedness.

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

⊢ P : ρ: P is typed from its inputs.

Equations

• P.Typed ρ = RoleFlow.Typed Sg P.outs P.ctx₀ P.inputs (RoleFlow.initSupp P.nw P.ctx₀.length) P.lines P.ret ρ

@[implicit_reducible]

instance RoleFlow.Prog.decTyped {S : Type} {Sg : Sig S} [DecidableEq S] (P : Prog Sg) (ρ : List Role) : Decidable (P.Typed ρ)

Equations

• P.decTyped ρ = RoleFlow.decTyped P.outs P.ctx₀ P.inputs (RoleFlow.initSupp P.nw P.ctx₀.length) P.lines P.ret ρ

theorem RoleFlow.Prog.Typed.wf {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} (h : P.Typed ρ) : P.WF

Recoverability

def RoleFlow.Recov {S : Type} {Sg : Sig S} (nw n : ℕ) (Λ : Finset ℕ) (R : List (XRecipe Sg)) (D : List (Finset ℕ)) : Prop

Recov: there are n supports, and every variable in scope is recomputable from the weights and its support, which is live.

Equations

• RoleFlow.Recov nw n Λ R D = (D.length = n ∧ ∀ v < n, D.getD v ∅ ⊆ Λ ∧ RoleFlow.Known R ({w : ℕ | w < nw} ∪ ↑(D.getD v ∅)) v)

theorem RoleFlow.Recov.init {S : Type} {Sg : Sig S} (nw n : ℕ) (R : List (XRecipe Sg)) : Recov nw n (Finset.Ico nw n) R (initSupp nw n)

At the start, with the inputs live.

theorem RoleFlow.Prog.recov_init {S : Type} {Sg : Sig S} (P : Prog Sg) (R : List (XRecipe Sg)) : Recov P.nw P.ctx₀.length P.inputs R (initSupp P.nw P.ctx₀.length)

theorem RoleFlow.Recov.cond {S : Type} {Sg : Sig S} {nw n : ℕ} {Λ : Finset ℕ} {R : List (XRecipe Sg)} {D : List (Finset ℕ)} {l : Line Sg} (hR : Recov nw n Λ R D) (hargs : ∀ x ∈ l.args, x < n) (hr : { line := l, tgt := l.ys n } ∈ R) : Recov nw (n + l.bs.length) Λ R (condSupp D l)

Cond preserves Recov: the new variables are settled by their own equation.

theorem RoleFlow.Recov.spine {S : Type} {Sg : Sig S} {nw n : ℕ} {Λ : Finset ℕ} {R : List (XRecipe Sg)} {D : List (Finset ℕ)} {l : Line Sg} {si : SemiInv Sg.Op l.as l.bs} (hR : Recov nw n Λ R D) (hargs : ∀ x ∈ l.args, x < n) (hacyc : ∀ p ∈ List.drop si.k l.args, ∀ c ∈ List.take si.k l.args, c ∉ D.getD p ∅) (hr : { 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 } ∈ R) : Recov nw (n + l.bs.length) (spineLive Λ l si.k n) R (spineSupp D l si.k n)

Spine preserves Recov: the consumed arguments are settled by the solved equation, whose sources are the new live variables and parameters, whose supports avoid them.

Recoverability along a derivation

theorem RoleFlow.Typed.induction_recov {S : Type} {Sg : Sig S} {nw : ℕ} {R : List (XRecipe Sg)} {O : List S} {motive : List S → Finset ℕ → List (Line Sg) → List ℕ → List Role → Prop} (ret : ∀ {Γ : List S} {Λ : Finset ℕ} {D : List (Finset ℕ)} {xs : List ℕ}, Recov nw Γ.length Λ R D → xs.Nodup → xs.toFinset = Λ → Args Γ xs O → motive Γ Λ [] xs []) (cond : ∀ {Γ : List S} {Λ : Finset ℕ} {D : List (Finset ℕ)} {l : Line Sg} {ls : List (Line Sg)} {xs : List ℕ} {ρ : List Role}, Recov nw Γ.length Λ R D → Args Γ l.args l.as → motive (Γ ++ l.bs) Λ ls xs ρ → motive Γ Λ (l :: ls) xs (Role.cond :: ρ)) (spine : ∀ {Γ : List S} {Λ : Finset ℕ} {D : List (Finset ℕ)} {l : Line Sg} {ls : List (Line Sg)} {xs : List ℕ} {ρ : List Role} (si : SemiInv Sg.Op l.as l.bs), Recov nw Γ.length Λ R D → Args Γ l.args l.as → Sg.inv l.op = some si → (List.take si.k l.args).Nodup → (∀ c ∈ List.take si.k l.args, c ∈ Λ) → (∀ p ∈ List.drop si.k l.args, ∀ c ∈ List.take si.k l.args, c ∉ D.getD p ∅) → motive (Γ ++ l.bs) (spineLive Λ l si.k Γ.length) ls xs ρ → motive Γ Λ (l :: ls) xs (Role.spine :: ρ)) {Γ : List S} {Λ : Finset ℕ} {D : List (Finset ℕ)} {ls : List (Line Sg)} {xs : List ℕ} {ρ : List Role} (hT : Typed Sg O Γ Λ D ls xs ρ) (hR : Recov nw Γ.length Λ R D) (hX : ∀ x ∈ xrecs Γ.length ls ρ, x ∈ R) : motive Γ Λ ls xs ρ

Recov along a derivation: induction on a typing in which every node may use Recov, given Recov at the root and recipes R that contain those of the lines.

Congruence and the returned variables

theorem RoleFlow.condSupp_congr {S : Type} {Sg : Sig S} {D : List (Finset ℕ)} {l l' : Line Sg} (hb : l'.bs.length = l.bs.length) (ha : ∀ (x : ℕ), x ∈ l'.args ↔ x ∈ l.args) : condSupp D l' = condSupp D l

theorem RoleFlow.typed_final {S : Type} {Sg : Sig S} {O Γ : List S} {Λ : Finset ℕ} {D : List (Finset ℕ)} {ls : List (Line Sg)} {xs : List ℕ} {ρ : List Role} (hT : Typed Sg O Γ Λ D ls xs ρ) (v : ℕ) : v ∈ xs → v ∈ Λ ∨ Γ.length ≤ v

The returned variables are live or introduced later.

Hash sets

def RoleFlow.insertAll (H : Std.HashSet ℕ) (xs : List ℕ) : Std.HashSet ℕ

Insert a list into a hash set.

Equations

• RoleFlow.insertAll H xs = List.foldl (fun (x1 : Std.HashSet ℕ) (x2 : ℕ) => x1.insert x2) H xs

theorem RoleFlow.mem_insertAll {H : Std.HashSet ℕ} {xs : List ℕ} {a : ℕ} : a ∈ insertAll H xs ↔ a ∈ xs ∨ a ∈ H