The front end is complete (module FrontComplete)

If some swap of P (SwapLine) is typed, swapArgs P is typed with the same roles (swapArgs_complete); with Prog.infer_iff, inference after the front end is exact up to swaps (infer_swapArgs_iff).

Fix the typed swap and its roles. Its recipes recs, one per line, are equations of the search (RecsOK.sub): the forward form of a conditioner, the solved or swapped solved form of a spine step. The search fires only recipes: every other equation of a line has a back edge to the line's recipe (line_back_cond, line_back_spine), reading a variable whose recipe reads one of its results, so it cannot fire while the known set is closed under the recipes (only_A). The search stops at a fixpoint (fwdKnown_terminal), where everything the recipes derive from the weights and the returned variables is known (fix_forward); that is every variable (Typed.known_xrecs), so every recipe has fired (fwdKnown_exact). Hence the swapped forms that fired are exactly the swapped spine steps of the typed swap, and the swaps swapArgs makes differ from it only on conditioners, whose argument order the typing ignores (typed_congr). The typing supplies unique binders and results outside the weights and the returned variables (recs_ok).

The search itself is Search; this module supplies its hypotheses for the lines.

theorem RoleFlow.swapIf_bs {S : Type} {Sg : Sig S} [Swap Sg] {s : Bool} {l : Line Sg} : (swapIf s l).bs = l.bs

theorem RoleFlow.swapIf_ys {S : Type} {Sg : Sig S} [Swap Sg] {s : Bool} {l : Line Sg} {n : ℕ} : (swapIf s l).ys n = l.ys n

theorem RoleFlow.kOf_swapIf {S : Type} {Sg : Sig S} [Swap Sg] {s : Bool} {l : Line Sg} : kOf (swapIf s l) = kOf l

theorem RoleFlow.mem_swapIf_args {S : Type} {Sg : Sig S} [Swap Sg] {s : Bool} {l : Line Sg} {x : ℕ} : x ∈ (swapIf s l).args ↔ x ∈ l.args

theorem RoleFlow.length_swapIf_args {S : Type} {Sg : Sig S} [Swap Sg] {s : Bool} {l : Line Sg} : (swapIf s l).args.length = l.args.length

theorem RoleFlow.swapIf_of_not {S : Type} {Sg : Sig S} [Swap Sg] {s : Bool} {l : Line Sg} (h : ¬(Swap.swappable l.op = true ∧ l.args.length = 2)) : swapIf s l = l

theorem RoleFlow.swapIf_args_add {S : Type} {Sg : Sig S} [Swap Sg] {s : Bool} {l : Line Sg} {a b : ℕ} (hA : Swap.swappable l.op = true) (hab : l.args = [a, b]) : (swapIf s l).args = if s = true then [b, a] else [a, b]

theorem RoleFlow.kOf_add {S : Type} {Sg : Sig S} [Swap Sg] {l : Line Sg} (h : Swap.swappable l.op = true) : kOf l = some 1

theorem RoleFlow.kOf_spec {S : Type} {Sg : Sig S} {l : Line Sg} {k : ℕ} (h : kOf l = some k) : ∃ (si : SemiInv Sg.Op l.as l.bs), Sg.inv l.op = some si ∧ si.k = k

theorem RoleFlow.kOf_of_inv {S : Type} {Sg : Sig S} {l : Line Sg} {si : SemiInv Sg.Op l.as l.bs} (h : Sg.inv l.op = some si) : kOf l = some si.k

theorem RoleFlow.kOf_pos {S : Type} {Sg : Sig S} {l : Line Sg} {k : ℕ} (h : kOf l = some k) : 1 ≤ k ∧ k ≤ l.as.length

theorem RoleFlow.ys_ne {S : Type} {Sg : Sig S} {l : Line Sg} {n : ℕ} : l.ys n ≠ []

theorem RoleFlow.be {e q : Search.Eqn} {u v : ℕ} (h₁ : u ∈ q.reads) (h₂ : v ∈ q.binds) (h₃ : u ∈ e.binds) (h₄ : v ∈ e.reads) : Search.BackEdge [e] q

def RoleFlow.lineRecipe {S : Type} {Sg : Sig S} [Swap Sg] (s : Bool) (i n : ℕ) (l : Line Sg) : Role → List Search.Eqn

The recipe of the line l, numbered i, at scope n, under a role, swapped if s: the forward form of a conditioner, the (swapped) solved form of a spine step.

Equations

• One or more equations did not get rendered due to their size.
• RoleFlow.lineRecipe s i n l RoleFlow.Role.cond = [{ binds := l.ys n, reads := l.args, line := i, swap := false }]

theorem RoleFlow.line_back_cond {S : Type} {Sg : Sig S} [Swap Sg] {l : Line Sg} {i n : ℕ} (hlen : ∀ (k : ℕ), kOf l = some k → k ≤ l.args.length) (q : Search.Eqn) : q ∈ lineEqns i n l → q = { binds := l.ys n, reads := l.args, line := i, swap := false } ∨ Search.BackEdge [{ binds := l.ys n, reads := l.args, line := i, swap := false }] q

A conditioner's other equations have back edges to its forward form.

theorem RoleFlow.line_back_spine {S : Type} {Sg : Sig S} [Swap Sg] {s : Bool} {l : Line Sg} {i n k : ℕ} (hk : kOf l = some k) (hlen : k ≤ l.args.length) : have e := { binds := List.take k (swapIf s l).args, reads := l.ys n ++ List.drop k (swapIf s l).args, line := i, swap := s && Swap.swappable l.op && l.args.length == 2 }; e ∈ lineEqns i n l ∧ ∀ q ∈ lineEqns i n l, q = e ∨ Search.BackEdge [e] q

A spine step's other equations have back edges to its (swapped) solved form.

theorem RoleFlow.swapLine_swapIf₂ {S : Type} {Sg : Sig S} [Swap Sg] (s t : Bool) (l : Line Sg) : SwapLine (swapIf s l) (swapIf t l)

The typing's recipes

def RoleFlow.recs {S : Type} {Sg : Sig S} [Swap Sg] (sw : ℕ → Bool) : ℕ → ℕ → List (Line Sg) → List Role → List Search.Eqn

The recipes of the lines numbered from i at scope n under the roles ρ, with the lines selected by sw swapped.

Equations

• RoleFlow.recs sw x✝¹ x✝ (l :: ls) (r :: ρ) = RoleFlow.lineRecipe (sw x✝¹) x✝¹ x✝ l r ++ RoleFlow.recs sw (x✝¹ + 1) (x✝ + l.bs.length) ls ρ
• RoleFlow.recs sw x✝³ x✝² x✝¹ x✝ = []

def RoleFlow.SwapAgree {S : Type} {Sg : Sig S} [Swap Sg] : List (Line Sg) → List (Line Sg) → List Role → Prop

Two line lists that agree on the spine steps and differ at most by a swap on conditioners.

Equations

• RoleFlow.SwapAgree (l₁ :: ls₁) (l₂ :: ls₂) (RoleFlow.Role.cond :: ρ) = (RoleFlow.SwapLine l₁ l₂ ∧ RoleFlow.SwapAgree ls₁ ls₂ ρ)
• RoleFlow.SwapAgree (l₁ :: ls₁) (l₂ :: ls₂) (RoleFlow.Role.spine :: ρ) = (l₁ = l₂ ∧ RoleFlow.SwapAgree ls₁ ls₂ ρ)
• RoleFlow.SwapAgree [] [] [] = True
• RoleFlow.SwapAgree x✝² x✝¹ x✝ = False

theorem RoleFlow.typed_congr {S : Type} {Sg : Sig S} [Swap Sg] {O Γ : List S} {Λ : Finset ℕ} {D : List (Finset ℕ)} {ls₁ ls₂ : List (Line Sg)} {xs : List ℕ} {ρ : List Role} (hT : Typed Sg O Γ Λ D ls₁ xs ρ) (ha : SwapAgree ls₁ ls₂ ρ) : Typed Sg O Γ Λ D ls₂ xs ρ

The typing ignores the argument order of conditioners.

structure RoleFlow.RecsOK {S : Type} {Sg : Sig S} [Swap Sg] (sw : ℕ → Bool) (nw i n : ℕ) (Λ : Finset ℕ) (ls : List (Line Sg)) (xs : List ℕ) (ρ : List Role) : Prop

What the typing of a swap gives about its recipes.

• uniq : Search.UniqB (recs sw i n ls ρ)
• binds (r : Search.Eqn) : r ∈ recs sw i n ls ρ → ∀ v ∈ r.binds, (v ∈ Λ ∨ n ≤ v) ∧ nw ≤ v ∧ v ∉ xs
• ne (r : Search.Eqn) : r ∈ recs sw i n ls ρ → r.binds ≠ []
• back (q : Search.Eqn) : q ∈ eqns i n ls → q ∈ recs sw i n ls ρ ∨ Search.BackEdge (recs sw i n ls ρ) q
• sub (r : Search.Eqn) : r ∈ recs sw i n ls ρ → r ∈ eqns i n ls
• line (r : Search.Eqn) : r ∈ recs sw i n ls ρ → i ≤ r.line
• agree (S : ℕ → Bool) : (∀ (j : ℕ), i ≤ j → (S j = true ↔ ∃ q ∈ recs sw i n ls ρ, q.swap = true ∧ q.line = j)) → SwapAgree (swapLines sw i ls) (swapLines S i ls) ρ

theorem RoleFlow.exists_cons_line {e : Search.Eqn} {A : List Search.Eqn} {j : ℕ} (he : e.line ≠ j) : (∃ q ∈ e :: A, q.swap = true ∧ q.line = j) ↔ ∃ q ∈ A, q.swap = true ∧ q.line = j

theorem RoleFlow.recs_ok {S : Type} {Sg : Sig S} [Swap Sg] (sw : ℕ → Bool) (nw : ℕ) (ls : List (Line Sg)) {i n : ℕ} {Λ : Finset ℕ} {D : List (Finset ℕ)} {xs : List ℕ} {ρ : List Role} {O Γ : List S} : Typed Sg O Γ Λ D (swapLines sw i ls) xs ρ → LinesWF Γ ls → Γ.length = n → (∀ v ∈ Λ, nw ≤ v ∧ v < n) → nw ≤ n → RecsOK sw nw i n Λ ls xs ρ

The recipes of a typed swap: unique binders, results live or later and outside the weights and the returned variables, back edges, and the swap flags.

Every result of the recipes is derivable

theorem RoleFlow.xrecs_recs {S : Type} {Sg : Sig S} [Swap Sg] (sw : ℕ → Bool) (ls : List (Line Sg)) {i n : ℕ} {ρ : List Role} (x : XRecipe Sg) : x ∈ xrecs n (swapLines sw i ls) ρ → ∃ a ∈ recs sw i n ls ρ, (∀ w ∈ a.reads, w ∈ x.line.args) ∧ ∀ v ∈ x.tgt, v ∈ a.binds

Each executable recipe of the swap is covered by a recipe of recs: it reads at most the recipe's arguments and computes at most its results.

theorem RoleFlow.recs_xrecs {S : Type} {Sg : Sig S} [Swap Sg] (sw : ℕ → Bool) (ls : List (Line Sg)) {i n : ℕ} {ρ : List Role} (a : Search.Eqn) : a ∈ recs sw i n ls ρ → ∃ x ∈ xrecs n (swapLines sw i ls) ρ, ∀ v ∈ a.binds, v ∈ x.tgt

Each recipe of recs computes results of an executable recipe of the swap.

Completeness

theorem RoleFlow.swapLines_congr {S : Type} {Sg : Sig S} [Swap Sg] {sw sw' : ℕ → Bool} {i : ℕ} (ls : List (Line Sg)) : (∀ (j : ℕ), i ≤ j → sw j = sw' j) → swapLines sw i ls = swapLines sw' i ls

theorem RoleFlow.swapLines_upd {S : Type} {Sg : Sig S} [Swap Sg] (b : Bool) (sw : ℕ → Bool) (i : ℕ) (l : Line Sg) {ls : List (Line Sg)} : swapLines (fun (j : ℕ) => if j = i then b else sw j) i (l :: ls) = swapIf b l :: swapLines sw (i + 1) ls

theorem RoleFlow.exists_swapLines {S : Type} {Sg : Sig S} [Swap Sg] {ls ls' : List (Line Sg)} (hs : List.Forall₂ SwapLine ls ls') (i : ℕ) : ∃ (sw : ℕ → Bool), swapLines sw i ls = ls'

Every swap is swapLines sw for some selection sw.

theorem RoleFlow.swapArgs_complete_sw {S : Type} {Sg : Sig S} [Swap Sg] {P : Prog Sg} {ρ : List Role} (sw : ℕ → Bool) (hT : (P.swap (swapLines sw 0 P.lines)).Typed ρ) : (swapArgs P).Typed ρ

Completeness for the swap selected by sw.

theorem RoleFlow.swapArgs_complete {S : Type} {Sg : Sig S} [Swap Sg] {P : Prog Sg} {ρ : List Role} {ls : List (Line Sg)} (hs : List.Forall₂ SwapLine P.lines ls) (hT : (P.swap ls).Typed ρ) : (swapArgs P).Typed ρ

The front end is complete: if some swap of P is typed, swapArgs P is typed with the same roles.

theorem RoleFlow.infer_swapArgs_iff {S : Type} {Sg : Sig S} [Swap Sg] [DecidableEq S] (P : Prog Sg) (ρ : List Role) : (swapArgs P).infer = some ρ ↔ ∃ (ls : List (Line Sg)), List.Forall₂ SwapLine P.lines ls ∧ (P.swap ls).Typed ρ

Inference after the front end is exact up to swaps.

theorem RoleFlow.swap_roles_unique {S : Type} {Sg : Sig S} [Swap Sg] {P : Prog Sg} {ls₁ ls₂ : List (Line Sg)} {ρ₁ ρ₂ : List Role} (hs₁ : List.Forall₂ SwapLine P.lines ls₁) (hT₁ : (P.swap ls₁).Typed ρ₁) (hs₂ : List.Forall₂ SwapLine P.lines ls₂) (hT₂ : (P.swap ls₂).Typed ρ₂) : ρ₁ = ρ₂

All typed swaps of a program have the same roles.