Role inference (docs/roleflow.tex, sec:infer)

Inference is a single backward pass (backward): starting from the returned variables N, a line is a spine step if one of its results is in N, and then its consumed arguments are added to N; otherwise it is a conditioner. Prog.infer runs the pass and checks the result.

Inference is exact (Prog.infer_iff): it finds the roles of every typing, so typings are unique (Prog.Typed.unique). The reason (backward_typed) is that at every node of a derivation the needed set below the scope is exactly the live set: a live variable is either returned or consumed by exactly one later spine step, and a conditioner's results are never live. Nothing here uses measure theory.

def RoleFlow.backward {S : Type} {Sg : Sig S} : ℕ → List (Line Sg) → Finset ℕ → List Role × Finset ℕ

The backward pass over the lines ls at scope n, from the needed set N₀ at the end: the roles, and the needed set at the start. A line is a spine step if one of its results is needed and it has a semi-inverse, and a conditioner otherwise. A needed result of a conditioner is never live, so the typing then fails.

Equations

• One or more equations did not get rendered due to their size.
• RoleFlow.backward x✝¹ [] x✝ = ([], x✝)

def RoleFlow.Prog.infer {S : Type} {Sg : Sig S} [DecidableEq S] (P : Prog Sg) : Option (List Role)

Infer the roles of a program: the backward pass, confirmed by deciding the typing.

Equations

• P.infer = if P.Typed (RoleFlow.backward P.ctx₀.length P.lines P.ret.toFinset).1 then some (RoleFlow.backward P.ctx₀.length P.lines P.ret.toFinset).1 else none

theorem RoleFlow.backward_typed {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 ρ) (hΛ : ∀ v ∈ Λ, v < Γ.length) : (backward Γ.length ls xs.toFinset).1 = ρ ∧ ∀ v < Γ.length, v ∈ (backward Γ.length ls xs.toFinset).2 ↔ v ∈ Λ

The backward pass finds the roles of a derivation, and below the scope its needed set is the live set.

theorem RoleFlow.Prog.infer_iff {S : Type} {Sg : Sig S} [DecidableEq S] (P : Prog Sg) (ρ : List Role) : P.infer = some ρ ↔ P.Typed ρ

Inference is exact (prop:infer).

theorem RoleFlow.Prog.Typed.unique {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ₁ ρ₂ : List Role} (h₁ : P.Typed ρ₁) (h₂ : P.Typed ρ₂) : ρ₁ = ρ₂

A program has at most one typing.