Invertibility as a type system

Prog.Invertible is a closure condition, decided by the schedule. Here it gets a syntax-directed judgment InvTyped, one rule per line, that is sound and complete for it (Prog.invTyped_iff). It annotates each variable v with a monotone Boolean formula Φ v over variables, read as "v is recoverable from any set of variables that satisfies Φ v". The supports of role typing are the special case where every formula is one conjunction.

• Prog: Φ v = v.
• Cond ys = o(xs): each y ∈ ys becomes y ∨ ⋀ Φ(xs) (condF).
• Spine ys = o(cs, ps) with a partial inverse: every formula substitutes c := c ∨ (⋀ ys ∧ ⋀ Φ(ps)) for c ∈ cs (spineF); without one, Φ is unchanged.
• Ret ret xs: each input's formula holds when the weights and xs are true.

Both updates are upd Φ tgt args for the line's recipe tgt ← o'(args). The invariant is that Φ v holds at A iff v is Known from A under the recipes of the lines so far (known_cons, eval_upd); it needs no linearity, acyclicity or scoping.

Role typing is an instance (Typed.sim, Prog.Typed.invTyped): its invariant Recov says Θ ∪ D(v) ⊨ Φ(v) (recov_iff_eval), so each support is a conjunction that implies the formula, and the live set adds what role typing needs beyond invertibility.

Monotone formulas

inductive RoleFlow.MF : Type

A monotone Boolean formula over variables.

• var (v : ℕ) : MF
• tt : MF
• and (φ ψ : MF) : MF
• or (φ ψ : MF) : MF

def RoleFlow.MF.eval (A : Set ℕ) : MF → Prop

φ holds when exactly the variables of A are true.

Equations

• RoleFlow.MF.eval A (RoleFlow.MF.var v) = (v ∈ A)
• RoleFlow.MF.eval A RoleFlow.MF.tt = True
• RoleFlow.MF.eval A (φ.and ψ) = (RoleFlow.MF.eval A φ ∧ RoleFlow.MF.eval A ψ)
• RoleFlow.MF.eval A (φ.or ψ) = (RoleFlow.MF.eval A φ ∨ RoleFlow.MF.eval A ψ)

def RoleFlow.MF.bind (σ : ℕ → MF) : MF → MF

Substitution of formulas for variables.

Equations

• RoleFlow.MF.bind σ (RoleFlow.MF.var v) = σ v
• RoleFlow.MF.bind σ RoleFlow.MF.tt = RoleFlow.MF.tt
• RoleFlow.MF.bind σ (φ.and ψ) = (RoleFlow.MF.bind σ φ).and (RoleFlow.MF.bind σ ψ)
• RoleFlow.MF.bind σ (φ.or ψ) = (RoleFlow.MF.bind σ φ).or (RoleFlow.MF.bind σ ψ)

def RoleFlow.MF.all : List MF → MF

The conjunction of a list.

Equations

• RoleFlow.MF.all [] = RoleFlow.MF.tt
• RoleFlow.MF.all (φ :: φs) = φ.and (RoleFlow.MF.all φs)

theorem RoleFlow.MF.eval_bind (A : Set ℕ) (σ : ℕ → MF) (φ : MF) : eval A (bind σ φ) ↔ eval {t : ℕ | eval A (σ t)} φ

theorem RoleFlow.MF.eval_all (A : Set ℕ) (φs : List MF) : eval A (all φs) ↔ ∀ φ ∈ φs, eval A φ

def RoleFlow.upd (Φ : ℕ → MF) (tgt args : List ℕ) : ℕ → MF

Firing the recipe tgt ← o'(args): each target t becomes t ∨ ⋀ Φ(args) in every formula.

Equations

• RoleFlow.upd Φ tgt args v = RoleFlow.MF.bind (fun (t : ℕ) => if t ∈ tgt then (RoleFlow.MF.var t).or (RoleFlow.MF.all (List.map Φ args)) else RoleFlow.MF.var t) (Φ v)

theorem RoleFlow.eval_upd (Φ : ℕ → MF) (tgt args : List ℕ) (A : Set ℕ) (v : ℕ) : MF.eval A (upd Φ tgt args v) ↔ MF.eval (A ∪ {t : ℕ | t ∈ tgt ∧ ∀ w ∈ args, MF.eval A (Φ w)}) (Φ v)

Adding a recipe to Known

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

theorem RoleFlow.known_cons {S : Type} {Sg : Sig S} (r : XRecipe Sg) (R : List (XRecipe Sg)) (A : Set ℕ) (v : ℕ) : Known (r :: R) A v ↔ Known R (A ∪ {t : ℕ | t ∈ r.tgt ∧ ∀ w ∈ r.line.args, Known R A w}) v

One more recipe: r adds its targets to the base if its sources are known without it. A firing of r that needs its own targets adds nothing, since Known is a least fixpoint.

theorem RoleFlow.upd_known {S : Type} {Sg : Sig S} {Φ : ℕ → MF} {R : List (XRecipe Sg)} (hΦ : ∀ (A : Set ℕ) (v : ℕ), MF.eval A (Φ v) ↔ Known R A v) (r : XRecipe Sg) (A : Set ℕ) (v : ℕ) : MF.eval A (upd Φ r.tgt r.line.args v) ↔ Known (r :: R) A v

upd tracks Known when a recipe is added.

The judgment

def RoleFlow.condF {S : Type} {Sg : Sig S} (Φ : ℕ → MF) (l : Line Sg) (n : ℕ) : ℕ → MF

Cond: each result y becomes y ∨ ⋀ Φ(xs).

Equations

• RoleFlow.condF Φ l n = RoleFlow.upd Φ (l.ys n) l.args

def RoleFlow.spineF {S : Type} {Sg : Sig S} (Φ : ℕ → MF) (l : Line Sg) (k n : ℕ) : ℕ → MF

Spine, solving the first k arguments cs from the results ys and the parameters ps: every formula substitutes c := c ∨ (⋀ ys ∧ ⋀ Φ(ps)).

Equations

• RoleFlow.spineF Φ l k n = RoleFlow.upd Φ (List.take k l.args) (l.ys n ++ List.drop k l.args)

def RoleFlow.InvTyped {S : Type} (Sg : Sig S) (O : List S) (nw : ℕ) (I : List ℕ) : List S → (ℕ → MF) → List (Line Sg) → List ℕ → List Role → Prop

Γ; Φ ⊢ e : O with roles ρ, for the lines ls, the returned positions xs, nw weights and the inputs I: Ret, Cond, Spine (with a partial inverse) and a spine step without one, by recursion on the lines. Every rule checks the sorts of its line.

Equations

• One or more equations did not get rendered due to their size.
• RoleFlow.InvTyped Sg O nw I x✝² x✝¹ [] x✝ [] = (RoleFlow.Args x✝² x✝ O ∧ ∀ i ∈ I, RoleFlow.MF.eval ({w : ℕ | w < nw} ∪ ↑x✝.toFinset) (x✝¹ i))
• RoleFlow.InvTyped Sg O nw I x✝² x✝¹ (l :: ls) x✝ (RoleFlow.Role.cond :: ρ) = (RoleFlow.Args x✝² l.args l.as ∧ RoleFlow.InvTyped Sg O nw I (x✝² ++ l.bs) (RoleFlow.condF x✝¹ l x✝².length) ls x✝ ρ)
• RoleFlow.InvTyped Sg O nw I x✝⁴ x✝³ x✝² x✝¹ x✝ = False

theorem RoleFlow.invTyped_iff {S : Type} {Sg : Sig S} {O : List S} {nw : ℕ} {I xs : List ℕ} {Γ : List S} {Φ : ℕ → MF} {R₀ : List (XRecipe Sg)} {ls : List (Line Sg)} {ρ : List Role} : (∀ (A : Set ℕ) (v : ℕ), MF.eval A (Φ v) ↔ Known R₀ A v) → (InvTyped Sg O nw I Γ Φ ls xs ρ ↔ (LinesWF Γ ls ∧ Args (ctxAfter Γ ls) xs O) ∧ ρ.length = ls.length ∧ ∀ i ∈ I, Known (xrecs Γ.length ls ρ ++ R₀) ({w : ℕ | w < nw} ∪ ↑xs.toFinset) i)

Soundness and completeness of InvTyped, for any context: if Φ tracks Known under the recipes R₀ of the lines before, then the judgment holds iff the lines and returned variables are well formed, there is one role per line, and every input is Known from the weights and the returned variables.

Role typing as an instance

theorem RoleFlow.MF.eval_mono {A B : Set ℕ} (h : A ⊆ B) (φ : MF) : eval A φ → eval B φ

theorem RoleFlow.recov_iff_eval {S : Type} {Sg : Sig S} {nw n : ℕ} {Λ : Finset ℕ} {R : List (XRecipe Sg)} {D : List (Finset ℕ)} {Φ : ℕ → MF} (hΦ : ∀ (A : Set ℕ) (v : ℕ), MF.eval A (Φ v) ↔ Known R A v) : Recov nw n Λ R D ↔ D.length = n ∧ ∀ v < n, D.getD v ∅ ⊆ Λ ∧ MF.eval ({w : ℕ | w < nw} ∪ ↑(D.getD v ∅)) (Φ v)

Role typing's invariant is a conjunction below Φ: when Φ tracks Known, Recov says that every variable's formula holds at the weights and its support, which is live.

theorem RoleFlow.Recov.of_subset {S : Type} {Sg : Sig S} {nw n : ℕ} {Λ : Finset ℕ} {R R' : List (XRecipe Sg)} {D : List (Finset ℕ)} (hR' : ∀ r ∈ R, r ∈ R') (hR : Recov nw n Λ R D) : Recov nw n Λ R' D

theorem RoleFlow.Typed.sim {S : Type} {Sg : Sig S} {O : List S} {nw : ℕ} {I xs : List ℕ} {Γ : List S} {Λ : Finset ℕ} {D : List (Finset ℕ)} {ls : List (Line Sg)} {ρ : List Role} {Φ : ℕ → MF} {R₀ : List (XRecipe Sg)} : Typed Sg O Γ Λ D ls xs ρ → (∀ (A : Set ℕ) (v : ℕ), MF.eval A (Φ v) ↔ Known R₀ A v) → Recov nw Γ.length Λ R₀ D → (∀ i ∈ I, i < Γ.length) → InvTyped Sg O nw I Γ Φ ls xs ρ

Simulation: a role typing whose annotations satisfy Recov (equivalently Θ ∪ D(v) ⊨ Φ(v), recov_iff_eval) for the recipes R₀ of the lines before gives an invertibility typing line by line: Cond and Spine become I-Cond and I-Spine, Recov is preserved for the recipes so far, and at Ret the support of every input lies in the live set, the returned variables.

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

⊢^inv_ρ P: Prog starts every formula as its own variable.

Equations

• P.InvTyped ρ = RoleFlow.InvTyped Sg P.outs P.nw (List.range' P.nw P.ins.length) P.ctx₀ RoleFlow.MF.var P.lines P.ret ρ

theorem RoleFlow.Prog.known_nil {S : Type} {Sg : Sig S} (A : Set ℕ) (v : ℕ) : MF.eval A (MF.var v) ↔ Known [] A v

theorem RoleFlow.Prog.invTyped_iff {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} : P.InvTyped ρ ↔ P.Invertible ρ ∧ ρ.length = P.lines.length

The judgment characterizes invertibility: ⊢^inv_ρ P iff P is invertible under ρ and ρ has one role per line.

@[implicit_reducible]

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

Equations

• P.instDecidableInvTypedOfDecidableEq ρ = decidable_of_iff (P.Invertible ρ ∧ ρ.length = P.lines.length) ⋯

theorem RoleFlow.Prog.Typed.invTyped {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} (hT : P.Typed ρ) : P.InvTyped ρ

Role typing instantiates the invertibility judgment (Typed.sim from Prog).