Forward search over equations

An equation binds ← reads remembers its line and whether it is the swapped solved form of an add. Starting from a known set K₀, the search fires every equation whose reads are known and whose results are unknown, sweep after sweep, until nothing fires (fwdKnown). The search is exact for a list A of recipes (fwdKnown_exact): if every variable has at most one recipe, every equation of E is a recipe or has a back edge to one, and every result of A is derivable from K₀, then the fired equations are exactly A. Nothing here depends on the signature; the front end (Front, FrontComplete) supplies the equations of the lines and the swapped solved form of add.

structure RoleFlow.Search.Eqn : Type

An equation binds ← reads of the line line; swap marks the swapped solved form.

• binds : List ℕ
• reads : List ℕ
• line : ℕ
• swap : Bool

def RoleFlow.Search.fireStep (r : Std.HashSet ℕ × List Eqn) (q : Eqn) : Std.HashSet ℕ × List Eqn

Fire q if its reads are known and its results unknown.

Equations

• RoleFlow.Search.fireStep r q = if ((q.binds.all fun (x : ℕ) => !r.1.contains x) && q.reads.all r.1.contains) = true then (RoleFlow.insertAll r.1 q.binds, q :: r.2) else r

def RoleFlow.Search.sweep (E : List Eqn) (K : Std.HashSet ℕ) (F : List Eqn) : Std.HashSet ℕ × List Eqn

One sweep: fire, in order, every equation that can.

Equations

• RoleFlow.Search.sweep E K F = List.foldl RoleFlow.Search.fireStep (K, F) E

def RoleFlow.Search.fwdKnown (E : List Eqn) : ℕ → Std.HashSet ℕ → List Eqn → Std.HashSet ℕ × List Eqn

Sweep until nothing fires: the known set and the fired equations. Every equation binds something, so each fires at most once and E.length + 1 sweeps suffice.

Equations

• One or more equations did not get rendered due to their size.
• RoleFlow.Search.fwdKnown E 0 x✝¹ x✝ = (x✝¹, x✝)

def RoleFlow.Search.CanFire (K : Std.HashSet ℕ) (q : Eqn) : Prop

q can fire at K: its results are unknown and its reads known.

Equations

• RoleFlow.Search.CanFire K q = ((∀ v ∈ q.binds, v ∉ K) ∧ ∀ w ∈ q.reads, w ∈ K)

theorem RoleFlow.Search.canFire_iff {K : Std.HashSet ℕ} {q : Eqn} : ((q.binds.all fun (x : ℕ) => !K.contains x) && q.reads.all K.contains) = true ↔ CanFire K q

def RoleFlow.Search.Closed (A : List Eqn) (K : Std.HashSet ℕ) : Prop

The known set is closed under A: a known variable's recipe reads only known variables.

Equations

• RoleFlow.Search.Closed A K = ∀ u ∈ K, ∀ r ∈ A, u ∈ r.binds → ∀ w ∈ r.reads, w ∈ K

def RoleFlow.Search.BackEdge (A : List Eqn) (q : Eqn) : Prop

q reads a variable whose recipe reads one of q's results.

Equations

• RoleFlow.Search.BackEdge A q = ∃ u ∈ q.reads, ∃ v ∈ q.binds, ∃ r ∈ A, u ∈ r.binds ∧ v ∈ r.reads

def RoleFlow.Search.UniqB (A : List Eqn) : Prop

Every variable has at most one recipe.

Equations

• RoleFlow.Search.UniqB A = ∀ r₁ ∈ A, ∀ r₂ ∈ A, ∀ v ∈ r₁.binds, v ∈ r₂.binds → r₁ = r₂

def RoleFlow.Search.Terminal (E : List Eqn) (K : Std.HashSet ℕ) : Prop

Nothing in E can fire.

Equations

• RoleFlow.Search.Terminal E K = ∀ q ∈ E, ¬RoleFlow.Search.CanFire K q

theorem RoleFlow.Search.BackEdge.mono {e q : Eqn} {A : List Eqn} (h : BackEdge [e] q) (he : e ∈ A) : BackEdge A q

theorem RoleFlow.Search.BackEdge.mono' {A B : List Eqn} {q : Eqn} (h : BackEdge A q) (hAB : ∀ r ∈ A, r ∈ B) : BackEdge B q

structure RoleFlow.Search.Inv (A E : List Eqn) (K₀ K : Std.HashSet ℕ) (F : List Eqn) : Prop

The invariant of the search: the known set K is closed, the fired equations F are distinct recipes, and a variable is known iff it is a start variable or a result of F.

• closed : Closed A K
• fa (q : Eqn) : q ∈ F → q ∈ A
• fe (q : Eqn) : q ∈ F → q ∈ E
• nd : F.Nodup
• src (v : ℕ) : v ∈ K → v ∈ K₀ ∨ ∃ q ∈ F, v ∈ q.binds
• fk (q : Eqn) : q ∈ F → ∀ v ∈ q.binds, v ∈ K
• k0 (v : ℕ) : v ∈ K₀ → v ∈ K

structure RoleFlow.Search.Hyp (A E : List Eqn) (K₀ : Std.HashSet ℕ) : Prop

The hypotheses the typing supplies.

• uniq : UniqB A
• back (q : Eqn) : q ∈ E → q ∈ A ∨ BackEdge A q
• sub (r : Eqn) : r ∈ A → r ∈ E
• out (r : Eqn) : r ∈ A → ∀ v ∈ r.binds, v ∉ K₀
• ne (r : Eqn) : r ∈ A → r.binds ≠ []

theorem RoleFlow.Search.inv_init {A E : List Eqn} {K₀ : Std.HashSet ℕ} (hd : ∀ r ∈ A, ∀ v ∈ r.binds, v ∉ K₀) : Inv A E K₀ K₀ []

theorem RoleFlow.Search.only_A {A : List Eqn} {K : Std.HashSet ℕ} {q : Eqn} (hC : Closed A K) (hq : q ∈ A ∨ BackEdge A q) (hf : CanFire K q) : q ∈ A

Only recipes fire: an equation with a back edge cannot fire at a closed known set.

theorem RoleFlow.Search.inv_fire {A E : List Eqn} {K₀ : Std.HashSet ℕ} (H : Hyp A E K₀) {K : Std.HashSet ℕ} {F : List Eqn} (hI : Inv A E K₀ K F) {q : Eqn} (hqE : q ∈ E) (hf : CanFire K q) : Inv A E K₀ (insertAll K q.binds) (q :: F)

theorem RoleFlow.Search.foldl_inv {A E : List Eqn} {K₀ : Std.HashSet ℕ} (H : Hyp A E K₀) (L : List Eqn) : (∀ q ∈ L, q ∈ E) → ∀ {K : Std.HashSet ℕ} {F : List Eqn}, Inv A E K₀ K F → have r := List.foldl fireStep (K, F) L; Inv A E K₀ r.1 r.2 ∧ F.length ≤ r.2.length ∧ (r.2.length = F.length → r.1 = K ∧ ∀ q ∈ L, ¬CanFire K q)

A sweep keeps the invariant, never loses fired equations, and if it fires nothing, nothing could fire.

theorem RoleFlow.Search.fwdKnown_inv {A E : List Eqn} {K₀ : Std.HashSet ℕ} (H : Hyp A E K₀) (fuel : ℕ) {K : Std.HashSet ℕ} {F : List Eqn} : Inv A E K₀ K F → have r := fwdKnown E fuel K F; Inv A E K₀ r.1 r.2 ∧ (Terminal E r.1 ∨ F.length + fuel ≤ r.2.length)

theorem RoleFlow.Search.fwdKnown_terminal {A E : List Eqn} {K₀ : Std.HashSet ℕ} (H : Hyp A E K₀) : have r := fwdKnown E (E.length + 1) K₀ []; Inv A E K₀ r.1 r.2 ∧ Terminal E r.1

The search stops at a fixpoint: the fired equations are distinct members of E.

theorem RoleFlow.Search.fix_forward {A E : List Eqn} {K₀ : Std.HashSet ℕ} (H : Hyp A E K₀) {K : Std.HashSet ℕ} {F : List Eqn} (hI : Inv A E K₀ K F) (hT : Terminal E K) (r : Eqn) : r ∈ A → (∀ w ∈ r.reads, w ∈ K) → ∀ v ∈ r.binds, v ∈ K

At a fixpoint the known set is closed under firing A forwards.

theorem RoleFlow.Search.fix_fires_all {A E : List Eqn} {K₀ : Std.HashSet ℕ} (H : Hyp A E K₀) {K : Std.HashSet ℕ} {F : List Eqn} (hI : Inv A E K₀ K F) {r : Eqn} (hr : r ∈ A) (hk : ∀ v ∈ r.binds, v ∈ K) : r ∈ F

Every recipe of A fires once its results are known.

theorem RoleFlow.Search.fwdKnown_exact {A E : List Eqn} {K₀ : Std.HashSet ℕ} (H : Hyp A E K₀) (hW : ∀ (S : Set ℕ), (∀ v ∈ K₀, v ∈ S) → (∀ r ∈ A, (∀ w ∈ r.reads, w ∈ S) → ∀ v ∈ r.binds, v ∈ S) → ∀ r ∈ A, ∀ v ∈ r.binds, v ∈ S) (q : Eqn) : q ∈ (fwdKnown E (E.length + 1) K₀ []).2 ↔ q ∈ A

The search fires exactly A, given that every result of A lies in every set that contains K₀ and is closed under A.