The inverse program (docs/roleflow.tex, sec:inverse)

The schedule is a forward closure (fire) over the recipes of the lines (Prog.xrecs): starting from the weights and the outputs, it fires a recipe whose sources are all known, until none is left, and emits each fired recipe as a line of the inverse program. A renaming maps the variables of P to those of the inverse program. Firing keeps the renaming sort-preserving (Good) and, on a trace of P, the values of the inverse program equal to those of the trace (Agree), since the recipes hold (xrecs_holds). At the end the known set is closed under the recipes (fire_closed), so by Recov at Ret it contains every input (Typed.known_xrecs, prop:schedule).

Prog.inverse is the inverse program P†, a program of the same signature (Prog.inverse_wf). Concordance (Prog.inverse_sem, thm:conc): ⟦P†⟧_θ ∘ ⟦P⟧_θ = id. With the right law, ⟦P⟧_θ is bijective with inverse ⟦P†⟧_θ (Prog.bijective, Prog.sem_inverse, Prog.equiv), and ⟦P†⟧_θ pushes μ_O back to μ_I with the negated log-weight (Prog.inverse_density, thm:invdensity), which needs only the left law.

Concordance needs less than the typing: Prog.Invertible asks only that the schedule reaches every input, and the recipes hold under any roles. A program that is invertible but not typed (say ret x + b, x + b) gets a left inverse, without a density.

theorem RoleFlow.Typed.known_xrecs {S : Type} {Sg : Sig S} {nw : ℕ} {O Γ : List S} {Λ : Finset ℕ} {R : List (XRecipe Sg)} {D : List (Finset ℕ)} {ls : List (Line Sg)} {xs : List ℕ} {ρ : List Role} (hT : Typed Sg O Γ Λ D ls xs ρ) (hrec : Recov nw Γ.length Λ R D) (hX : ∀ x ∈ xrecs Γ.length ls ρ, x ∈ R) (v : ℕ) : v < Γ.length + (List.map (fun (l : Line Sg) => l.bs.length) ls).sum → Known R ({w : ℕ | w < nw} ∪ ↑xs.toFinset) v

Existence of the schedule, the recoverability half: under Recov, every variable, in scope or introduced by the lines, is known from the weights and the returned variables.

The forward closure

def RoleFlow.pickFirst {α : Type u_1} (p : α → Bool) : List α → Option (α × List α)

The first element of a list with a property, and the list without it.

Equations

• RoleFlow.pickFirst p [] = none
• RoleFlow.pickFirst p (a :: as) = if p a = true then some (a, as) else Option.map (fun (r : α × List α) => (r.1, a :: r.2)) (RoleFlow.pickFirst p as)

theorem RoleFlow.pickFirst_none {α : Type u_1} {p : α → Bool} {as : List α} (h : pickFirst p as = none) (a : α) : a ∈ as → p a = false

theorem RoleFlow.pickFirst_some {α : Type u_1} {p : α → Bool} {as bs : List α} {a : α} (h : pickFirst p as = some (a, bs)) : p a = true ∧ a ∈ as ∧ bs.length + 1 = as.length ∧ (∀ b ∈ bs, b ∈ as) ∧ ∀ b ∈ as, b = a ∨ b ∈ bs

def RoleFlow.renStep (tgt : List ℕ) (m : ℕ) (ren : ℕ → ℕ) (v : ℕ) : ℕ

The renaming after firing a recipe with targets tgt at the next free position m.

Equations

• RoleFlow.renStep tgt m ren v = if v ∈ tgt then m + List.idxOf v tgt else ren v

def RoleFlow.fire {S : Type} {Sg : Sig S} : ℕ → List (XRecipe Sg) → ℕ → (ℕ → ℕ) → Std.HashSet ℕ → List (Line Sg) × (ℕ → ℕ) × Std.HashSet ℕ

The schedule, as a forward closure: fire a recipe of X whose sources are all known, emit it as a line at the next free position m, and continue; ren renames the variables of P into the inverse program and K is the hash set of known variables.

Equations

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

theorem RoleFlow.fire_mono {S : Type} {Sg : Sig S} (f : ℕ) (X : List (XRecipe Sg)) (m : ℕ) (ren : ℕ → ℕ) (K : Std.HashSet ℕ) (v : ℕ) : v ∈ K → v ∈ (fire f X m ren K).2.2

theorem RoleFlow.fire_closed {S : Type} {Sg : Sig S} (f : ℕ) (X : List (XRecipe Sg)) (m : ℕ) (ren : ℕ → ℕ) (K : Std.HashSet ℕ) : X.length ≤ f → ∀ x ∈ X, (∀ a ∈ x.line.args, a ∈ (fire f X m ren K).2.2) → ∀ t ∈ x.tgt, t ∈ (fire f X m ren K).2.2

After enough rounds, the known set is closed under the recipes.

theorem RoleFlow.known_fire {S : Type} {Sg : Sig S} {f : ℕ} {X : List (XRecipe Sg)} {m : ℕ} {ren : ℕ → ℕ} {K : Std.HashSet ℕ} (hf : X.length ≤ f) {B : Set ℕ} (hB : ∀ v ∈ B, v ∈ K) {v : ℕ} (hv : Known X B v) : v ∈ (fire f X m ren K).2.2

The inverse program's known set contains everything Known from its start.

theorem RoleFlow.fire_known {S : Type} {Sg : Sig S} {X₀ : List (XRecipe Sg)} {B : Set ℕ} (f : ℕ) (X : List (XRecipe Sg)) (m : ℕ) (ren : ℕ → ℕ) (K : Std.HashSet ℕ) : (∀ x ∈ X, x ∈ X₀) → (∀ v ∈ K, Known X₀ B v) → ∀ v ∈ (fire f X m ren K).2.2, Known X₀ B v

The converse of known_fire: everything the schedule adds is Known from its start.

Sorts and values along the schedule

def RoleFlow.Good {S : Type} (Γ Γ' : List S) (ren : ℕ → ℕ) (K : Std.HashSet ℕ) : Prop

The renaming ren takes the known variables of Γ to positions of Γ' of the same sort.

Equations

• RoleFlow.Good Γ Γ' ren K = ∀ v ∈ K, v < Γ.length ∧ Γ'[ren v]? = Γ[v]?

theorem RoleFlow.Good.args {S : Type} {Γ Γ' : List S} {ren : ℕ → ℕ} {K : Std.HashSet ℕ} (hG : Good Γ Γ' ren K) {xs : List ℕ} {as : List S} (h : Args Γ xs as) (hK : ∀ x ∈ xs, x ∈ K) : Args Γ' (List.map ren xs) as

theorem RoleFlow.lt_of_good {S : Type} {Γ Γ' : List S} {ren : ℕ → ℕ} {K : Std.HashSet ℕ} (hG : Good Γ Γ' ren K) {v : ℕ} (hv : v ∈ K) : ren v < Γ'.length

theorem RoleFlow.Good.step {S : Type} {Γ Γ' : List S} {ren : ℕ → ℕ} {K : Std.HashSet ℕ} (hG : Good Γ Γ' ren K) {tgt : List ℕ} {bs : List S} (h : Args Γ tgt bs) : Good Γ (Γ' ++ bs) (renStep tgt Γ'.length ren) (insertAll K tgt)

def RoleFlow.Agree {S : Type} [Sorts S] {Γ Γ' : List S} (t : Val Γ) (u : Val Γ') (ren : ℕ → ℕ) (K : Std.HashSet ℕ) : Prop

On known variables, the value u of the inverse program agrees with the trace t.

Equations

• RoleFlow.Agree t u ren K = ∀ v ∈ K, ∀ (a : S) (h : Γ[v]? = some a) (h' : Γ'[ren v]? = some a), u.get (ren v) h' = t.get v h

theorem RoleFlow.Agree.pick {S : Type} [Sorts S] {Γ Γ' : List S} {t : Val Γ} {u : Val Γ'} {ren : ℕ → ℕ} {K : Std.HashSet ℕ} (hA : Agree t u ren K) {xs : List ℕ} {as : List S} (h : Args Γ xs as) (h' : Args Γ' (List.map ren xs) as) (hK : ∀ x ∈ xs, x ∈ K) : u.pick (List.map ren xs) h' = t.pick xs h

theorem RoleFlow.Agree.step {S : Type} [Sorts S] {Γ Γ' : List S} {t : Val Γ} {u : Val Γ'} {ren : ℕ → ℕ} {K : Std.HashSet ℕ} (hA : Agree t u ren K) (hG : Good Γ Γ' ren K) {tgt : List ℕ} {bs : List S} (h : Args Γ tgt bs) : Agree t (u.append (t.pick tgt h)) (renStep tgt Γ'.length ren) (insertAll K tgt)

theorem RoleFlow.fire_wf {S : Type} {Sg : Sig S} {Γ : List S} {X₀ : List (XRecipe Sg)} (hX : ∀ x ∈ X₀, Args Γ x.line.args x.line.as ∧ Args Γ x.tgt x.line.bs) (f : ℕ) (X : List (XRecipe Sg)) : (∀ x ∈ X, x ∈ X₀) → ∀ (Γ' : List S) (m : ℕ), Γ'.length = m → ∀ (ren : ℕ → ℕ) (K : Std.HashSet ℕ), Good Γ Γ' ren K → LinesWF Γ' (fire f X m ren K).1 ∧ Good Γ (ctxAfter Γ' (fire f X m ren K).1) (fire f X m ren K).2.1 (fire f X m ren K).2.2

The lines emitted by the schedule are well formed, and the renaming stays good.

theorem RoleFlow.fire_agree {S : Type} {Sg : Sig S} [Sorts S] (M : Model Sg) {Γ : List S} (t : Val Γ) {X₀ : List (XRecipe Sg)} (hX : ∀ x ∈ X₀, Args Γ x.line.args x.line.as ∧ Args Γ x.tgt x.line.bs) (hH : ∀ x ∈ X₀, ∀ (h₁ : Args Γ x.line.args x.line.as) (h₂ : Args Γ x.tgt x.line.bs), M.sem x.line.op (t.pick x.line.args h₁) = t.pick x.tgt h₂) (f : ℕ) (X : List (XRecipe Sg)) : (∀ x ∈ X, x ∈ X₀) → ∀ (Γ' : List S) (m : ℕ), Γ'.length = m → ∀ (ren : ℕ → ℕ) (K : Std.HashSet ℕ), Good Γ Γ' ren K → ∀ (hwf : LinesWF Γ' (fire f X m ren K).1) (u : Val Γ'), Agree t u ren K → Agree t (trace M (fire f X m ren K).1 hwf u) (fire f X m ren K).2.1 (fire f X m ren K).2.2

On a trace on which the recipes hold, the inverse program reproduces the trace on every known variable.

The inverse program

def RoleFlow.Prog.schedule {S : Type} {Sg : Sig S} (P : Prog Sg) (ρ : List Role) : List (Line Sg) × (ℕ → ℕ) × Std.HashSet ℕ

The schedule of P: the forward closure from the weights and the outputs. The outputs get the positions after the weights, so the renaming starts as renStep P.ret P.nw id.

Equations

• P.schedule ρ = RoleFlow.fire (P.xrecs ρ).length (P.xrecs ρ) (P.nw + P.outs.length) (RoleFlow.renStep P.ret P.nw id) (RoleFlow.insertAll (RoleFlow.insertAll ∅ (List.range P.nw)) P.ret)

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

The inverse program P† = (Θ, O, e†): it fires the schedule and returns the inputs.

Equations

• P.inverse ρ = { wts := P.wts, ins := P.outs, outs := P.ins, lines := (P.schedule ρ).1, ret := List.map (P.schedule ρ).2.1 (List.range' P.nw P.ins.length) }

theorem RoleFlow.Prog.length_ctx₀_le {S : Type} {Sg : Sig S} (P : Prog Sg) : P.ctx₀.length ≤ P.ctx.length

theorem RoleFlow.Prog.good_wts {S : Type} {Sg : Sig S} (P : Prog Sg) : Good P.ctx P.wts id (insertAll ∅ (List.range P.nw))

The weights are known at the start, at their own positions.

theorem RoleFlow.Prog.good_init {S : Type} {Sg : Sig S} {P : Prog Sg} (h : P.WF) : Good P.ctx (P.wts ++ P.outs) (renStep P.ret P.nw id) (insertAll (insertAll ∅ (List.range P.nw)) P.ret)

theorem RoleFlow.Prog.inputs_known {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} (hT : P.Typed ρ) (v : ℕ) : v < P.ctx₀.length → v ∈ (P.schedule ρ).2.2

theorem RoleFlow.Prog.args_inputs {S : Type} {Sg : Sig S} {P : Prog Sg} : Args P.ctx (List.range' P.nw P.ins.length) P.ins

theorem RoleFlow.Prog.inputs_mem {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} (hT : P.Typed ρ) (x : ℕ) : x ∈ List.range' P.nw P.ins.length → x ∈ (P.schedule ρ).2.2

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

P is invertible under the roles ρ: it is well formed and the schedule reaches every input. Decidable, and implied by the typing (Typed.invertible).

Equations

• P.Invertible ρ = (P.WF ∧ ∀ x ∈ List.range' P.nw P.ins.length, x ∈ (P.schedule ρ).2.2)

@[implicit_reducible]

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

Equations

• P.instDecidableInvertibleOfDecidableEq ρ = RoleFlow.Prog.instDecidableInvertibleOfDecidableEq._aux_1 P ρ

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

theorem RoleFlow.Prog.invertible_iff_known {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} : P.Invertible ρ ↔ P.WF ∧ ∀ x ∈ List.range' P.nw P.ins.length, Known (P.xrecs ρ) ({w : ℕ | w < P.nw} ∪ ↑P.ret.toFinset) x

Invertibility is Known: the schedule reaches exactly the variables that are Known from the weights and the returned variables (known_fire, fire_known).

theorem RoleFlow.Prog.Invertible.inverse_wf {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} (hI : P.Invertible ρ) : (P.inverse ρ).WF

The inverse program is well formed (a program over the same signature).

theorem RoleFlow.Prog.inverse_wf {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} (hT : P.Typed ρ) : (P.inverse ρ).WF

theorem RoleFlow.Prog.agree_wts {S : Type} {Sg : Sig S} {P : Prog Sg} [Sorts S] (M : Model Sg) (h : P.WF) (θ : Val P.wts) (x : Val P.ins) : Agree (tr M P h θ x) θ id (insertAll ∅ (List.range P.nw))

At the start, the weights of the inverse program agree with the trace.

theorem RoleFlow.Prog.Invertible.inverse_sem {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} [Sorts S] (M : Model Sg) (hI : P.Invertible ρ) (θ : Val P.wts) (x : Val P.ins) : sem M (P.inverse ρ) ⋯ θ (sem M P ⋯ θ x) = x

Concordance (thm:conc): the inverse program undoes the program.

theorem RoleFlow.Prog.inverse_sem {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} [Sorts S] (M : Model Sg) (hT : P.Typed ρ) (θ : Val P.wts) (x : Val P.ins) : sem M (P.inverse ρ) ⋯ θ (sem M P ⋯ θ x) = x

theorem RoleFlow.Prog.Invertible.measurable_inverse {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} [Sorts S] (M : Model Sg) (hI : P.Invertible ρ) (θ : Val P.wts) : Measurable (sem M (P.inverse ρ) ⋯ θ)

The inverse program is measurable at fixed weights.

theorem RoleFlow.Prog.measurable_inverse {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} [Sorts S] (M : Model Sg) (hT : P.Typed ρ) (θ : Val P.wts) : Measurable (sem M (P.inverse ρ) ⋯ θ)

theorem RoleFlow.Prog.inverse_density {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} [Sorts S] (M : Model Sg) (hT : P.Typed ρ) (θ : Val P.wts) : Cov (vol P.outs) (vol P.ins) (sem M (P.inverse ρ) ⋯ θ) fun (y : Val P.outs) => expw (-logw M P ⋯ ρ θ (sem M (P.inverse ρ) ⋯ θ y))

Density of the inverse (thm:invdensity): ⟦P†⟧_θ pushes μ_O back to μ_I with the negated log-weight at the recomputed inputs. Only the left law is used.

theorem RoleFlow.Prog.map_inverse {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} [Sorts S] (M : Model Sg) (hT : P.Typed ρ) (θ : Val P.wts) : MeasureTheory.Measure.map (sem M (P.inverse ρ) ⋯ θ) (vol P.outs) = (vol P.ins).withDensity fun (x : Val P.ins) => expw (logw M P ⋯ ρ θ x)

Model density (cor:modeldensity): e^{L_θ} is the density of (⟦P†⟧_θ)_* μ_O with respect to μ_I, by the density theorem and the left inverse. Here and not in Density.lean, since it mentions P†.

theorem RoleFlow.Prog.sem_inverse {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} [Sorts S] {M : Model Sg} (hM : M.RightLaw) (hT : P.Typed ρ) (θ : Val P.wts) (y : Val P.outs) : sem M P ⋯ θ (sem M (P.inverse ρ) ⋯ θ y) = y

With the right law, the inverse program is also a right inverse.

theorem RoleFlow.Prog.bijective {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} [Sorts S] {M : Model Sg} (hM : M.RightLaw) (hT : P.Typed ρ) (θ : Val P.wts) : Function.Bijective (sem M P ⋯ θ)

Bijectivity (thm:bij): with the right law, ⟦P⟧_θ is a bijection.

def RoleFlow.Prog.equiv {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} [Sorts S] {M : Model Sg} (hM : M.RightLaw) (hT : P.Typed ρ) (θ : Val P.wts) : Val P.ins ≃ᵐ Val P.outs

⟦P⟧_θ as a measurable equivalence, with inverse ⟦P†⟧_θ.

Equations

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