From b5f35b08700572cb9b6fd1f47ef7c2f3a4623649 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Tue, 1 Jul 2025 12:32:29 -0400 Subject: [PATCH 01/22] Add initial code for Dataflow.lean --- KLR/Compile/Dataflow.lean | 678 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 678 insertions(+) create mode 100644 KLR/Compile/Dataflow.lean diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean new file mode 100644 index 00000000..173a7e0c --- /dev/null +++ b/KLR/Compile/Dataflow.lean @@ -0,0 +1,678 @@ +/- +# 💻 Dataflow Solver 🥳 + +This is a file, originally authored by Julia, performing semilattice-join fixpoint +search based dataflow analysis! +In other words, a graph is the carrier for a datum of type `β` at each node. +These data are expected to follow the constraint `τ(β) ≤ β'`, where `τ : β → β` is a +node-specific "transition function", `β'` is any succesor of `β` in the graph, and `≤` is +the semitlattice order. +A "solution" is a set of data over the graph carrier satisfying these constraints. +This file exists to compute such solutions. + +note: this file considers only _partial_ correctness. _total_ correctness, i.e. proving +(conditional) termination, has been considered out of scope. In practice, a 'fuel' parameter +to the search loop in `DataflowProblem.solve_to_depth` can be easily set above theoretical +upper bonds on search duration. 😊 + +## Workflow 🫡 + +To instantiate the solver in general, for graphs whose nodes are indexed by a type `α`, and +whose data are drawn from a type `β`, begin by providing an instance of `DataflowProblem α β`. + +```class DataflowProblem (α β : Type) ...``` + +(Note... this involves instantiating several typeclasses, including the most heavyeight: + `NodeMap α` - which provides the type `⟦α, β⟧` of maps from nodes `α` to data `β`) +(The Class NodeProp α, which provides the structure type `Node α`, fixes +`node_prop : α → Prop` that idenitifes the subset of the type `α` corresponding to +nodes in the graph.) + +Once a `dataflowProblem : DataflowProblem` is created, call `dataflowProblem.solve`. +``` +def DataflowProblem.solve {α β : Type} ... + (DP : DataflowProblem α β) + : Option ((ν : ⟦α, β⟧) ×' I' ν) +``` +This will perform a fuel-based terminating fixpoint search for a dataflow solution ✌️. +if one is found, then `dataflowProblem.solve = some ⟨ν, ν_sound⟩`, where `ν` is +the solution and `ν_sound : Prop` proves its a solution (see `def E` through + `def I'`) for structure of solution soundness theorems 🦾. + +## Finite Graph Workflow #️⃣🌎🔢 + +When `Node α` is a finite type of size `n`, `⟦α, β] = Vector β n` suffices. This +choice fixes a large amount of the "boilerplate" in `DataflowProblem`. The class +`FiniteSolverInput β` consists primarily of three fields: +``` +structure FiniteSolverInput (β : Type) ... + num_nodes : ℕ + edges : ℕ → ℕ → Bool + transitions : ℕ → β → β + ... +``` +`num_nodes` is the number of nodes in the graph. `edges` and `transitions` operate on +the on node numbers (`Nat`s less than `num_nodes`). `edges` is a boolean relation +indicating the edge relation, and `transitions` provides the transition functions +`β → β` per node. Finally, lightweight soundness conditions on these entries +(`transitions_sound` `le_sound` `le_supl` `le_supr`) must be proved. + +Once a `FiniteSolverInput` instance is defined, it can be passed to the function + `FiniteDataflowProblem` to create a corresponding `DataflowProblem` instance: + +``` +def FiniteDataflowProblem {β : Type} ... + (FSI : FiniteSolverInput β) + : DataflowProblem ℕ β +``` + +`DataflowProblem.solve` may then be called on this instance. +-/ + +class NodeProp (α : Type) where + node_prop : α → Prop + +--type for elements of α verified to meet NodeProp α +structure Node (α : Type) [NP : NodeProp α] where + data : α + sound : NP.node_prop data + +instance {α} [TSA : ToString α] [NodeProp α]: ToString (Node α) where + toString := (TSA.toString ·.data) + +instance {α} [BEq α] [NodeProp α]: BEq (Node α) where + beq a₀ a₁ := a₀.data == a₁.data + +--type of maps whose domain is a set A +class NodeMap (α : Type) extends NodeProp α where + μ (β : Type) : Type -- type of maps + const {β} : β → μ β -- empty instance + of_func {β} : (Node α → β) → μ β --instance from func + get {β} : (μ β) → Node α → β + fold {β γ} : (μ β) → ((Node α) → γ → γ) → γ → γ + app_unary {β γ} : (μ β) → (β → γ) → (μ γ) + app_binary {β₀ β₁ γ} : (μ β₀) → (μ β₁) → (β₀ → β₁ → γ) → (μ γ) + + const_get {β} (b : β) a : get (const b) a = b + of_func_get {β} (f : Node α → β) a : get (of_func f) a = f a + of_map_get {β γ} μ (f : β → γ) a : get (app_unary μ f) a = f (get μ a) + of_app_binary_get {β₀ β₁ γ} μ₀ μ₁ (f : β₀ → β₁ → γ) a + : get (app_binary μ₀ μ₁ f) a = f (get μ₀ a) (get μ₁ a) + + fold_ind {β γ} {ν : μ β} {γ₀ : γ} {acc : (Node α) → γ → γ} : + (P : γ → Prop) → + (P γ₀) → + (∀ a γ, P γ → P (acc a γ)) → + P (fold ν acc γ₀) + + fold_strong_ind {β γ} {ν : μ β} {γ₀ : γ} {acc : Node α → γ → γ} : + (P : Node α → γ → Prop) → + (∀ a γ₀, P a (acc a γ₀)) → + (∀ a γ₀ b, P a γ₀ → P a (acc b γ₀)) → + (∀ a, P a (fold ν acc γ₀)) + +notation μ "fold⟪" st "," acc "⟫" => NodeMap.fold μ acc st + +instance {α β : Type} [ToString α] [ToString β] [NM:NodeMap α] + : ToString (NM.μ β) where + toString μ := NM.fold μ (fun nd str => + str ++ "{" ++ (toString nd.data) ++ ":" + ++ (toString (NM.get μ nd)) ++ "}\n") "" + + +infix:90 "◃" => NodeMap.get + +def NodeMap.call_const (α : Type) {β : Type} (b : β) [NodeMap α] + := NodeMap.const (α:=α) b +notation "⟪" α "↦" b "⟫"=> NodeMap.call_const α b + +notation "⟦" α "," β "⟧" => NodeMap.μ α β + +notation μ "map⟪" f "⟫" => NodeMap.app_unary μ f + +notation "of_func⟪" f "⟫" => NodeMap.of_func f + +notation "map2⟪" μ₀ "," μ₁ "," f "⟫" => NodeMap.app_binary μ₀ μ₁ f + +def NodeMap.LE {α β : Type} [NodeMap α] [LE β] (μ₀ μ₁ : ⟦α, β⟧) := (a : Node α) → (μ₀◃a ≤ μ₁◃a) +infix:90 "⟪≤⟫" => NodeMap.LE +instance {α β : Type} [NodeMap α] [LT β] : LT ⟦α, β⟧ where + lt μ₀ μ₁ := (a : Node α) → (μ₀◃a < μ₁◃a) +def NodeMap.Max {α β : Type} [NodeMap α] [Max β] (μ₀ μ₁ : ⟦α , β⟧) := + map2⟪μ₀, μ₁, (Max.max · ·)⟫ +infix:90 "⟪⊔⟫" => NodeMap.Max +instance {α β : Type} [NodeMap α] [BEq β] : BEq ⟦α, β⟧ where + beq μ₀ μ₁ := μ₀ fold⟪true, (fun a prev => prev ∧ (μ₀◃a == μ₁◃a))⟫ +instance {α β : Type} [NodeMap α] [ToString α] [ToString β] : ToString ⟦α, β⟧ where + toString μ := μ fold⟪"", (fun nd repr => repr ++ + "\n{" ++ toString nd.data ++ ": " ++ toString (μ◃nd) ++ "}")⟫ + +class Preorder (α : Type) extends LE α, LT α where + le_refl : ∀ a : α, a ≤ a + le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c + lt := fun a b => a ≤ b ∧ ¬b ≤ a + lt_iff_le_not_ge : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl + +instance (α : Type) [Preorder α] : LE α where + le := LE.le + +class HasBot (α : Type) where + bot : α + +notation "⊥" => HasBot.bot + +-- instance of the dataflow problem +class DataflowProblem (α β : Type) extends NodeMap α, Max β, BEq β, Preorder β, HasBot β +where + τ : ⟦α, (β → β)⟧ -- transition functions + σ : ⟦α, (List (Node α))⟧ -- successor relation + + τ_sound (α₀ : Node α) (β₀ β₁ : β) : (β₀ == β₁) → (τ◃α₀) β₀ == (τ◃α₀) β₁ + le_sound (β₀ β₁ β₂ : β) : (β₀ == β₁) → (β₀ ≤ β₂) → (β₁ ≤ β₂) + + map_le_supl (ν₀ ν₁ ν₂ : ⟦α, β⟧) (h : ν₀ ⟪≤⟫ ν₁) : (ν₀ ⟪≤⟫ (ν₁ ⟪⊔⟫ ν₂)) + map_le_supr (ν₀ ν₁ ν₂ : ⟦α, β⟧) (h : ν₀ ⟪≤⟫ ν₂) : (ν₀ ⟪≤⟫ (ν₁ ⟪⊔⟫ ν₂)) + +section + variable {α β : Type} [BEq α] {DP: DataflowProblem α β} + open DataflowProblem + + def ν₀ : ⟦α, (β × Bool)⟧ := ⟪α↦(⊥, true)⟫ + + def ε (a₀ a₁ : Node α) : Bool := List.elem a₁ (σ◃a₀) + + def strip_bools (ν : ⟦α, (β × Bool)⟧) := ν map⟪fun (β, _)=>β⟫ + + def E (P : (Node α) → (Node α) → Prop) := ∀ (a₀ a₁) (_:ε a₀ a₁), P a₀ a₁ + def R (ν₀ : ⟦α, (β × Bool)⟧) (ν₁ : ⟦α, β⟧) [LE β]: Prop := E (fun a₀ a₁ => (ν₀◃a₀).2 ∨ (τ◃a₀) ((ν₀◃a₀).1) ≤ (ν₁◃a₁)) + def I (ν : ⟦α, (β × Bool)⟧) : Prop := R ν (strip_bools ν) + + def R' (ν₀ ν₁ : ⟦α, β⟧) : Prop := E (fun a₀ a₁ => (τ◃a₀) (ν₀◃a₀) ≤ ν₁◃a₁) + def I' (ν : ⟦α, β⟧) : Prop := R' ν ν + + theorem base_case : @I α β _ DP ν₀ := by { + unfold I R E + intro α₀ α₁ edge + left + unfold ν₀ NodeMap.call_const + rw [NodeMap.const_get] + } + + def δ (ν : ⟦α, (β × Bool)⟧) (a : Node α) : ⟦α, β⟧ := -- step + of_func⟪(fun a' => if ε a a' then ((τ◃a) (ν◃a).1) else ⊥)⟫ + + def Δ₀ (ν : ⟦α, (β × Bool)⟧) : ⟦α, β⟧ := + ν fold⟪ν map⟪(·.1)⟫, (fun a ν₀ => if (ν◃a).2 then ν₀ ⟪⊔⟫ (δ ν a) else ν₀)⟫ + + def Δ (ν : ⟦α, (β × Bool)⟧) : ⟦α, (β × Bool)⟧ := + let ν' := Δ₀ ν + of_func⟪fun a => let (β, β') := ((ν◃a).1, (ν'◃a)); (β', β != β')⟫ + + + def is_fix (ν : ⟦α, (β × Bool)⟧) : Bool := + ν fold⟪true, fun a prior => prior && !(ν◃a).2 ⟫ + + section + open Classical -- this can prolly be proven without contradiction or choice + omit [BEq α] in theorem is_fix_sound (ν : ⟦α, (β × Bool)⟧) + : is_fix ν → ∀ a, !(ν ◃ a).2 := by { + intro h a + apply byContradiction + intro pν + simp at pν + have h' : is_fix ν = false := by { + unfold is_fix + let acc := fun prior a ↦ prior && !(ν◃a).2 + let P := fun a b ↦ (ν◃a).2 = true → b = false + apply (NodeMap.fold_strong_ind P)<;>try unfold P + { + simp + } + { + simp + intros a b af att + rw [att] at af + contradiction + } + { + apply pν + } + } + rw [h] at h' + contradiction + } + end + + omit [BEq α] in theorem strip_bools_snd (ν : ⟦α, (β × Bool)⟧) (a : Node α) + : ( (strip_bools ν)◃a = (ν◃a).1) := by { + unfold strip_bools + rw [NodeMap.of_map_get] + } + + omit [BEq α] in theorem map_le_refl (ν : ⟦α, β⟧) : ν ⟪≤⟫ ν := by { + unfold NodeMap.LE + intros + apply Preorder.le_refl + } + + + theorem δlessΔ (ν : ⟦α, (β × Bool)⟧) (a₀ : Node α) (h: (ν ◃ a₀).2): δ ν a₀ ⟪≤⟫ Δ₀ ν := by { + let P a ν₀ := (ν◃a).2 = true → δ ν a ⟪≤⟫ ν₀ + apply (NodeMap.fold_strong_ind P)<;>try unfold P + { + intro a γ₀ ha + rw [ha] + simp + apply map_le_supr + apply map_le_refl + } + { + intro a γ₀ b ha ha' + have h' := (ha ha') + cases (ν◃b).2<;>simp + assumption + apply map_le_supl; assumption + + } + assumption + } + + theorem Δfpt (ν : ⟦α, (β × Bool)⟧) (a : Node α) (nb_eq:(Δ ν ◃ a).2 = false) + : (ν ◃ a).1 == (Δ ν ◃ a).1 := by { + unfold Δ + simp + rw [NodeMap.of_func_get] + simp + unfold Δ at nb_eq + simp at nb_eq + rw [NodeMap.of_func_get] at nb_eq + simp at nb_eq + unfold bne at nb_eq + cases h : (ν◃a).1 == Δ₀ ν◃a + { + rw [h] at nb_eq + contradiction + } + { + rfl + } + } + + theorem Δmono (ν : ⟦α, (β × Bool)⟧) : (strip_bools ν) ⟪≤⟫ Δ₀ ν := by { + let P ν' := (strip_bools ν) ⟪≤⟫ ν' + apply NodeMap.fold_ind + { + unfold NodeMap.LE + intro a + rw [NodeMap.of_map_get] + rw [strip_bools_snd] + apply Preorder.le_refl + } + { + intro a g h + cases (ν◃a).2<;> simp + assumption + apply map_le_supl + assumption + } + } + + theorem Δgrnd (ν : ⟦α, (β × Bool)⟧) : ∀ a, (Δ ν◃a).1 = (Δ₀ ν ◃ a) := by { + intro a + unfold Δ + simp + rw [NodeMap.of_func_get] + } + + + theorem Δlift (ν : ⟦α, (β × Bool)⟧) (a₀ a₁ : Node α) (edge : ε a₀ a₁) (h : I ν) + : (τ◃a₀) (ν◃a₀).1 ≤ (Δ ν ◃ a₁).1 := by { + cases b : (ν◃a₀).2 + { + have le_fst : (τ◃a₀) (ν◃a₀).1 ≤ (ν◃a₁).1 := by { + have h' := h a₀ a₁ edge + simp at h' + rw [b] at h' + simp at h' + rw [strip_bools_snd] at h' + assumption + } + have le_snd : (ν◃a₁).1 ≤ (Δ₀ ν ◃ a₁) := by { + have h':= Δmono ν a₁ + rw [strip_bools_snd] at h' + assumption + } + rewrite [Δgrnd] + exact (@Preorder.le_trans β _ _ _ _ le_fst le_snd) + } + { + have le_fst : (τ◃a₀) (ν◃a₀).1 ≤ (δ ν a₀)◃a₁ := by { + unfold δ + rw [NodeMap.of_func_get, edge] + apply Preorder.le_refl + } + have le_snd : (δ ν a₀)◃a₁ ≤ (Δ₀ ν ◃ a₁) := by { + apply δlessΔ + assumption + } + rewrite [Δgrnd] + exact (@Preorder.le_trans β _ _ _ _ le_fst le_snd) + } + } + + theorem Δpres (ν : ⟦α, (β × Bool)⟧) (h : I ν) : I (Δ ν) := by { + unfold I R E + intro a₀ a₁ edge + cases Δstat : (Δ ν◃a₀).2 + right; { + { + rw [strip_bools_snd] + have Δrel := Δlift ν a₀ a₁ edge h + + have Δfpa : (ν ◃ a₀).1 == (Δ ν ◃ a₀).1 := by { + have h' := Δfpt ν a₀ + rw [Δstat] at h' + simp at h' + assumption + } + have Δfpa_lift : (τ◃a₀) (ν ◃ a₀).1 == (τ◃a₀) (Δ ν ◃ a₀).1 := by { + apply τ_sound + exact Δfpa + } + apply le_sound (β₀:=(τ◃a₀) (ν◃a₀).1) <;> assumption + } + } + left; rfl + } + + theorem Δsol (ν : ⟦α, (β × Bool)⟧) (h₀ : I ν) (h₁ : is_fix ν = true) + : I' (strip_bools ν) := by { + unfold I' R' E + unfold I R E at h₀ + + intro a₀ a₁ edge + have h₀' := h₀ a₀ a₁ edge + have h₁' := (is_fix_sound ν h₁) a₀ + simp at h₀' + + cases h₂ : (ν◃a₀).2 + { + cases h₀' + { + rename_i h₃ + rw [h₃] at h₂ + contradiction + } + { + rw [strip_bools_snd] + assumption + } + } + { + rw [h₂] at h₁' + contradiction + } + } + + +abbrev ℕ := Nat + + +def DataflowProblem.solve_to_depth {α β : Type} + (depth : ℕ) + (DP : DataflowProblem α β) + [BEq α] + (ν : ⟦α, (β × Bool)⟧) + (h : I ν) + : Option ((ν : ⟦α, (β × Bool)⟧) ×' (I ν) ×' (is_fix ν) = true) := + match depth with + | 0 => none + | Nat.succ depth' => + let ν' := Δ ν + let h' := Δpres ν h + if fix : is_fix ν' then + some ⟨ν', h', fix⟩ + else + solve_to_depth depth' DP ν' h' + +def DataflowProblem.solve {α β : Type} [BEq α] + (DP : DataflowProblem α β) + : Option ((ν : ⟦α, β⟧) ×' I' ν) + + := (DP.solve_to_depth 1000 ν₀ base_case).map (fun ⟨ν, h, fix⟩ => + let ν' := strip_bools ν; ⟨ν', Δsol ν h fix⟩) + +section FiniteSolver + +variable (n : Nat) -- size of arrays + +infix:90 "⊔" => Max.max + +structure FiniteSolverInput (β : Type) + [BEq β] + [Preorder β] + [Max β] + [HasBot β] +where + num_nodes : ℕ + edges : ℕ → ℕ → Bool + transitions : ℕ → β → β + + transitions_sound n (β₀ β₁ : β) : (β₀ == β₁) → (transitions n) β₀ == (transitions n) β₁ + le_sound (β₀ β₁ β₂ : β) : (β₀ == β₁) → (β₀ ≤ β₂) → (β₁ ≤ β₂) + le_supl (β₀ β₁ : β) : β₀ ≤ β₀ ⊔ β₁ + le_supr (β₀ β₁ : β) : β₁ ≤ β₀ ⊔ β₁ + +def LtProp : NodeProp ℕ where + node_prop n' := n' < n + +def NodeT := @Node ℕ (LtProp n) + +def node_to_fin (nd : NodeT n) : (Fin n) + := {val := @nd.data, isLt := @nd.sound} + +def fin_to_node (fin : Fin n) : (NodeT n) + := @Node.mk ℕ (LtProp n) fin.val fin.isLt + +def nodes : Vector (NodeT n) n + := Vector.ofFn (fin_to_node n) + +def vector_fn {β : Type} (f : NodeT n → β) : Vector β n + := Vector.ofFn (f ∘ (fin_to_node n)) + +#check Vector.rec + +def FiniteDataflowProblem {β : Type} + [M: Max β] + [B: BEq β] + [Preorder β] + [HasBot β] + (FSI : FiniteSolverInput β) + : DataflowProblem ℕ β + := let NP : NodeProp ℕ := { + node_prop n' := n' < n + } ; {NP with + μ β := Vector β n + const β + := vector_fn n (fun _ => β) + of_func f + := vector_fn n f + get μ nd + := μ.get (node_to_fin n nd) + fold _ := (nodes n).toList.foldr + app_unary μ f := Vector.map f μ + app_binary μ₀ μ₁ f := + (nodes n).map (fun nd => f + (μ₀.get (node_to_fin n nd)) + (μ₁.get (node_to_fin n nd))) + + const_get := by { + intros + unfold vector_fn Vector.get + simp + } + of_func_get := by { + intros + unfold node_to_fin vector_fn Vector.get + simp + unfold fin_to_node + rfl + } + of_map_get := by { + intros + unfold Vector.map Vector.get + simp + } + of_app_binary_get := by { + intros β₀ β₁ γ μ₀ μ₁ f a + unfold Vector.map Vector.get node_to_fin nodes fin_to_node + simp + } + + τ := vector_fn n (FSI.transitions ·.data) + σ := vector_fn n (fun nd => + (nodes n).toList.filter (FSI.edges nd.data ·.data) + ) + + τ_sound := by { + intro α₀ β₀ β₁ beq + unfold vector_fn Vector.ofFn Vector.get fin_to_node node_to_fin + simp + apply FSI.transitions_sound + assumption + } + le_sound := FSI.le_sound + + map_le_supl := by { + unfold NodeMap.LE NodeMap.Max + intro ν₀ ν₁ ν₂ h a + unfold NodeMap.app_binary node_to_fin Vector.map Vector.get nodes fin_to_node + simp + apply Preorder.le_trans + {apply h} + {apply FSI.le_supl} + } + map_le_supr := by { + unfold NodeMap.LE NodeMap.Max + intro ν₀ ν₁ ν₂ h a + unfold NodeMap.app_binary node_to_fin Vector.map Vector.get nodes fin_to_node + simp + apply Preorder.le_trans + {apply h} + {apply FSI.le_supr} + } + + fold_ind := by { + intro β γ ν γ₀ acc P h₀ h₁ + induction ((nodes n).toList) + { + simp + assumption + } + { + rename_i hd tl Pfld + simp + apply h₁ + assumption + } + } + + + fold_strong_ind := by { + intro β γ ν γ₀ acc P h₀ h₁ + let Q (l : List (Node ℕ)) := ∀ nd ∈ l, P nd (List.foldr acc γ₀ l) + have h : Q (nodes n).toList := by { + induction (nodes n).toList<;>unfold Q; simp + { + rename_i hd tl Qtl + intro nd ndin + cases ndin + { + apply h₀ + } + { + simp + apply h₁ + apply Qtl + assumption + } + } + } + unfold Q at h + intro a + apply h + simp + unfold nodes Vector.ofFn + simp + cases a + rename_i d snd + exists Fin.mk d snd + } + } + /- + namespace Test_Preds + def num_nodes := 14 + + instance : ToString (Finset ℕ) where + toString fs := + let _ := LtProp num_nodes + (vector_fn num_nodes (·)).foldl (fun repr nd => + if nd.data ∈ fs then + repr ++ " " ++ toString nd.data + else + repr) "" + + instance {α : Type} [ToString α] : ToString (Option α) where + toString | none => "none" | some a => toString a + + def FSI + : FiniteSolverInput (Finset ℕ) := { + + num_nodes := num_nodes + + edges := fun + | 0 => (· ∈ []) + | 1 => (· ∈ [2]) + | 2 => (· ∈ [3, 4]) + | 3 => (· ∈ [5]) + | 4 => (· ∈ [7, 8]) + | 5 => (· ∈ [6, 9]) + | 6 => (· ∈ [3, 10]) + | 7 => (· ∈ [10]) + | 8 => (· ∈ []) + | 9 => (· ∈ []) + | 10 => (· ∈ [11, ]) + | 11 => (· ∈ [7, 13]) + | 12 => (· ∈ []) + | 13 => (· ∈ []) + | _ => fun _ => false + transitions n := + (insert n ·) + + + + bot := Finset.empty + + + + transitions_sound := by { + unfold BEq.beq instBEqOfDecidableEq + simp + } + le_sound := by { + unfold BEq.beq instBEqOfDecidableEq + simp + intro β₀ β₁ β₂ beq ble + rw [←beq] + assumption + } + le_supl := by simp + le_supr := by simp + } + + def xx := (FiniteDataflowProblem num_nodes FSI).solve.map ((·.1)) + #print xx + #eval! xx + end Test_Preds + -/ +end FiniteSolver From bd3a521e25a9329e069e870f0676ae2d59fa3979 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Tue, 1 Jul 2025 12:50:33 -0400 Subject: [PATCH 02/22] add more structure and comments to Dataflow.lean --- KLR/Compile/Dataflow.lean | 508 ++++++++++++++++++++------------------ 1 file changed, 270 insertions(+), 238 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 173a7e0c..82c8dc73 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -69,10 +69,22 @@ def FiniteDataflowProblem {β : Type} ... `DataflowProblem.solve` may then be called on this instance. -/ +abbrev ℕ := Nat + +section Basics + +/- + An instance `_ : NodeProp α` fixes a `node_prop : α → Prop` that + defines the set of nodes (note `Set α := α → Prop`) in the carrier + graph. +-/ class NodeProp (α : Type) where node_prop : α → Prop ---type for elements of α verified to meet NodeProp α +/- + With a `NodeProp α` in scope, `Node α` is the subtype of `a : α` that + can prove `node_prop a` (i.e., are indeed nodes in the carrier graph) +-/ structure Node (α : Type) [NP : NodeProp α] where data : α sound : NP.node_prop data @@ -83,7 +95,14 @@ instance {α} [TSA : ToString α] [NodeProp α]: ToString (Node α) where instance {α} [BEq α] [NodeProp α]: BEq (Node α) where beq a₀ a₁ := a₀.data == a₁.data ---type of maps whose domain is a set A +/- + In the context of a set of nodes `Node α` fixed by a `NodeProp α`, an + instance of `NodeMap α` is a constructor for map objects whose domain + is the nodes of the carrier graph and whose codomain is a datatype `β`. + + Several utilities, as well as soundness theorems on them including + two induction principles, are required as well. +-/ class NodeMap (α : Type) extends NodeProp α where μ (β : Type) : Type -- type of maps const {β} : β → μ β -- empty instance @@ -119,7 +138,6 @@ instance {α β : Type} [ToString α] [ToString β] [NM:NodeMap α] str ++ "{" ++ (toString nd.data) ++ ":" ++ (toString (NM.get μ nd)) ++ "}\n") "" - infix:90 "◃" => NodeMap.get def NodeMap.call_const (α : Type) {β : Type} (b : β) [NodeMap α] @@ -147,6 +165,8 @@ instance {α β : Type} [NodeMap α] [ToString α] [ToString β] : ToString ⟦ toString μ := μ fold⟪"", (fun nd repr => repr ++ "\n{" ++ toString nd.data ++ ": " ++ toString (μ◃nd) ++ "}")⟫ + +-- copied from Mathlib for utility class Preorder (α : Type) extends LE α, LT α where le_refl : ∀ a : α, a ≤ a le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c @@ -156,12 +176,21 @@ class Preorder (α : Type) extends LE α, LT α where instance (α : Type) [Preorder α] : LE α where le := LE.le +-- An instance `HasBot α` fixes a bottom element (`⊥`) of type `α`. class HasBot (α : Type) where bot : α notation "⊥" => HasBot.bot --- instance of the dataflow problem +/- + A `DataflowProblem α β` extends an map constructor `NodeMap α` with choices of + `τ : ⟦α, (β → β)⟧`, the node-indexed map of transition functions, and + `σ : ⟦α, (List (Node α))⟧`, the node-indexed map of succesor lists fixing + the graph topology. Two soundness theorems are requires relating the `≤` + relation `τ`, and the `==` relation on `β` (as provided by their respective + included typeclasses). The `⊔` and `≤` relations (on `⟦α, β⟧`), must also + be proven. +-/ class DataflowProblem (α β : Type) extends NodeMap α, Max β, BEq β, Preorder β, HasBot β where τ : ⟦α, (β → β)⟧ -- transition functions @@ -173,7 +202,12 @@ where map_le_supl (ν₀ ν₁ ν₂ : ⟦α, β⟧) (h : ν₀ ⟪≤⟫ ν₁) : (ν₀ ⟪≤⟫ (ν₁ ⟪⊔⟫ ν₂)) map_le_supr (ν₀ ν₁ ν₂ : ⟦α, β⟧) (h : ν₀ ⟪≤⟫ ν₂) : (ν₀ ⟪≤⟫ (ν₁ ⟪⊔⟫ ν₂)) -section +end Basics + +/- + +-/ +section DataflowProblemSolver variable {α β : Type} [BEq α] {DP: DataflowProblem α β} open DataflowProblem @@ -414,265 +448,263 @@ section } } + def DataflowProblem.solve_to_depth {α β : Type} + (depth : ℕ) + (DP : DataflowProblem α β) + [BEq α] + (ν : ⟦α, (β × Bool)⟧) + (h : I ν) + : Option ((ν : ⟦α, (β × Bool)⟧) ×' (I ν) ×' (is_fix ν) = true) := + match depth with + | 0 => none + | Nat.succ depth' => + let ν' := Δ ν + let h' := Δpres ν h + if fix : is_fix ν' then + some ⟨ν', h', fix⟩ + else + solve_to_depth depth' DP ν' h' -abbrev ℕ := Nat - - -def DataflowProblem.solve_to_depth {α β : Type} - (depth : ℕ) - (DP : DataflowProblem α β) - [BEq α] - (ν : ⟦α, (β × Bool)⟧) - (h : I ν) - : Option ((ν : ⟦α, (β × Bool)⟧) ×' (I ν) ×' (is_fix ν) = true) := - match depth with - | 0 => none - | Nat.succ depth' => - let ν' := Δ ν - let h' := Δpres ν h - if fix : is_fix ν' then - some ⟨ν', h', fix⟩ - else - solve_to_depth depth' DP ν' h' - -def DataflowProblem.solve {α β : Type} [BEq α] - (DP : DataflowProblem α β) - : Option ((ν : ⟦α, β⟧) ×' I' ν) - - := (DP.solve_to_depth 1000 ν₀ base_case).map (fun ⟨ν, h, fix⟩ => - let ν' := strip_bools ν; ⟨ν', Δsol ν h fix⟩) - -section FiniteSolver - -variable (n : Nat) -- size of arrays - -infix:90 "⊔" => Max.max - -structure FiniteSolverInput (β : Type) - [BEq β] - [Preorder β] - [Max β] - [HasBot β] -where - num_nodes : ℕ - edges : ℕ → ℕ → Bool - transitions : ℕ → β → β - - transitions_sound n (β₀ β₁ : β) : (β₀ == β₁) → (transitions n) β₀ == (transitions n) β₁ - le_sound (β₀ β₁ β₂ : β) : (β₀ == β₁) → (β₀ ≤ β₂) → (β₁ ≤ β₂) - le_supl (β₀ β₁ : β) : β₀ ≤ β₀ ⊔ β₁ - le_supr (β₀ β₁ : β) : β₁ ≤ β₀ ⊔ β₁ + def DataflowProblem.solve {α β : Type} [BEq α] + (DP : DataflowProblem α β) + : Option ((ν : ⟦α, β⟧) ×' I' ν) -def LtProp : NodeProp ℕ where - node_prop n' := n' < n + := (DP.solve_to_depth 1000 ν₀ base_case).map (fun ⟨ν, h, fix⟩ => + let ν' := strip_bools ν; ⟨ν', Δsol ν h fix⟩) -def NodeT := @Node ℕ (LtProp n) +end DataflowProblemSolver -def node_to_fin (nd : NodeT n) : (Fin n) - := {val := @nd.data, isLt := @nd.sound} +section FiniteDataflowProblemSolver -def fin_to_node (fin : Fin n) : (NodeT n) - := @Node.mk ℕ (LtProp n) fin.val fin.isLt + variable (n : Nat) -- size of arrays -def nodes : Vector (NodeT n) n - := Vector.ofFn (fin_to_node n) + infix:90 "⊔" => Max.max -def vector_fn {β : Type} (f : NodeT n → β) : Vector β n - := Vector.ofFn (f ∘ (fin_to_node n)) + structure FiniteSolverInput (β : Type) + [BEq β] + [Preorder β] + [Max β] + [HasBot β] + where + num_nodes : ℕ + edges : ℕ → ℕ → Bool + transitions : ℕ → β → β -#check Vector.rec + transitions_sound n (β₀ β₁ : β) : (β₀ == β₁) → (transitions n) β₀ == (transitions n) β₁ + le_sound (β₀ β₁ β₂ : β) : (β₀ == β₁) → (β₀ ≤ β₂) → (β₁ ≤ β₂) + le_supl (β₀ β₁ : β) : β₀ ≤ β₀ ⊔ β₁ + le_supr (β₀ β₁ : β) : β₁ ≤ β₀ ⊔ β₁ -def FiniteDataflowProblem {β : Type} - [M: Max β] - [B: BEq β] - [Preorder β] - [HasBot β] - (FSI : FiniteSolverInput β) - : DataflowProblem ℕ β - := let NP : NodeProp ℕ := { + def LtProp : NodeProp ℕ where node_prop n' := n' < n - } ; {NP with - μ β := Vector β n - const β - := vector_fn n (fun _ => β) - of_func f - := vector_fn n f - get μ nd - := μ.get (node_to_fin n nd) - fold _ := (nodes n).toList.foldr - app_unary μ f := Vector.map f μ - app_binary μ₀ μ₁ f := - (nodes n).map (fun nd => f - (μ₀.get (node_to_fin n nd)) - (μ₁.get (node_to_fin n nd))) - - const_get := by { - intros - unfold vector_fn Vector.get - simp - } - of_func_get := by { - intros - unfold node_to_fin vector_fn Vector.get - simp - unfold fin_to_node - rfl - } - of_map_get := by { - intros - unfold Vector.map Vector.get - simp - } - of_app_binary_get := by { - intros β₀ β₁ γ μ₀ μ₁ f a - unfold Vector.map Vector.get node_to_fin nodes fin_to_node - simp - } - - τ := vector_fn n (FSI.transitions ·.data) - σ := vector_fn n (fun nd => - (nodes n).toList.filter (FSI.edges nd.data ·.data) - ) - τ_sound := by { - intro α₀ β₀ β₁ beq - unfold vector_fn Vector.ofFn Vector.get fin_to_node node_to_fin - simp - apply FSI.transitions_sound - assumption - } - le_sound := FSI.le_sound + def NodeT := @Node ℕ (LtProp n) + + def node_to_fin (nd : NodeT n) : (Fin n) + := {val := @nd.data, isLt := @nd.sound} + + def fin_to_node (fin : Fin n) : (NodeT n) + := @Node.mk ℕ (LtProp n) fin.val fin.isLt + + def nodes : Vector (NodeT n) n + := Vector.ofFn (fin_to_node n) + + def vector_fn {β : Type} (f : NodeT n → β) : Vector β n + := Vector.ofFn (f ∘ (fin_to_node n)) + + #check Vector.rec + + def FiniteDataflowProblem {β : Type} + [M: Max β] + [B: BEq β] + [Preorder β] + [HasBot β] + (FSI : FiniteSolverInput β) + : DataflowProblem ℕ β + := let NP : NodeProp ℕ := { + node_prop n' := n' < n + } ; {NP with + μ β := Vector β n + const β + := vector_fn n (fun _ => β) + of_func f + := vector_fn n f + get μ nd + := μ.get (node_to_fin n nd) + fold _ := (nodes n).toList.foldr + app_unary μ f := Vector.map f μ + app_binary μ₀ μ₁ f := + (nodes n).map (fun nd => f + (μ₀.get (node_to_fin n nd)) + (μ₁.get (node_to_fin n nd))) + + const_get := by { + intros + unfold vector_fn Vector.get + simp + } + of_func_get := by { + intros + unfold node_to_fin vector_fn Vector.get + simp + unfold fin_to_node + rfl + } + of_map_get := by { + intros + unfold Vector.map Vector.get + simp + } + of_app_binary_get := by { + intros β₀ β₁ γ μ₀ μ₁ f a + unfold Vector.map Vector.get node_to_fin nodes fin_to_node + simp + } - map_le_supl := by { - unfold NodeMap.LE NodeMap.Max - intro ν₀ ν₁ ν₂ h a - unfold NodeMap.app_binary node_to_fin Vector.map Vector.get nodes fin_to_node - simp - apply Preorder.le_trans - {apply h} - {apply FSI.le_supl} - } - map_le_supr := by { - unfold NodeMap.LE NodeMap.Max - intro ν₀ ν₁ ν₂ h a - unfold NodeMap.app_binary node_to_fin Vector.map Vector.get nodes fin_to_node - simp - apply Preorder.le_trans - {apply h} - {apply FSI.le_supr} - } + τ := vector_fn n (FSI.transitions ·.data) + σ := vector_fn n (fun nd => + (nodes n).toList.filter (FSI.edges nd.data ·.data) + ) - fold_ind := by { - intro β γ ν γ₀ acc P h₀ h₁ - induction ((nodes n).toList) - { + τ_sound := by { + intro α₀ β₀ β₁ beq + unfold vector_fn Vector.ofFn Vector.get fin_to_node node_to_fin simp + apply FSI.transitions_sound assumption } - { - rename_i hd tl Pfld + le_sound := FSI.le_sound + + map_le_supl := by { + unfold NodeMap.LE NodeMap.Max + intro ν₀ ν₁ ν₂ h a + unfold NodeMap.app_binary node_to_fin Vector.map Vector.get nodes fin_to_node simp - apply h₁ - assumption + apply Preorder.le_trans + {apply h} + {apply FSI.le_supl} + } + map_le_supr := by { + unfold NodeMap.LE NodeMap.Max + intro ν₀ ν₁ ν₂ h a + unfold NodeMap.app_binary node_to_fin Vector.map Vector.get nodes fin_to_node + simp + apply Preorder.le_trans + {apply h} + {apply FSI.le_supr} } - } - - fold_strong_ind := by { - intro β γ ν γ₀ acc P h₀ h₁ - let Q (l : List (Node ℕ)) := ∀ nd ∈ l, P nd (List.foldr acc γ₀ l) - have h : Q (nodes n).toList := by { - induction (nodes n).toList<;>unfold Q; simp + fold_ind := by { + intro β γ ν γ₀ acc P h₀ h₁ + induction ((nodes n).toList) { - rename_i hd tl Qtl - intro nd ndin - cases ndin - { - apply h₀ - } - { - simp - apply h₁ - apply Qtl - assumption - } + simp + assumption + } + { + rename_i hd tl Pfld + simp + apply h₁ + assumption } } - unfold Q at h - intro a - apply h - simp - unfold nodes Vector.ofFn - simp - cases a - rename_i d snd - exists Fin.mk d snd - } - } - /- - namespace Test_Preds - def num_nodes := 14 - - instance : ToString (Finset ℕ) where - toString fs := - let _ := LtProp num_nodes - (vector_fn num_nodes (·)).foldl (fun repr nd => - if nd.data ∈ fs then - repr ++ " " ++ toString nd.data - else - repr) "" - - instance {α : Type} [ToString α] : ToString (Option α) where - toString | none => "none" | some a => toString a - - def FSI - : FiniteSolverInput (Finset ℕ) := { - - num_nodes := num_nodes - - edges := fun - | 0 => (· ∈ []) - | 1 => (· ∈ [2]) - | 2 => (· ∈ [3, 4]) - | 3 => (· ∈ [5]) - | 4 => (· ∈ [7, 8]) - | 5 => (· ∈ [6, 9]) - | 6 => (· ∈ [3, 10]) - | 7 => (· ∈ [10]) - | 8 => (· ∈ []) - | 9 => (· ∈ []) - | 10 => (· ∈ [11, ]) - | 11 => (· ∈ [7, 13]) - | 12 => (· ∈ []) - | 13 => (· ∈ []) - | _ => fun _ => false - transitions n := - (insert n ·) - - - bot := Finset.empty - - - transitions_sound := by { - unfold BEq.beq instBEqOfDecidableEq + fold_strong_ind := by { + intro β γ ν γ₀ acc P h₀ h₁ + let Q (l : List (Node ℕ)) := ∀ nd ∈ l, P nd (List.foldr acc γ₀ l) + have h : Q (nodes n).toList := by { + induction (nodes n).toList<;>unfold Q; simp + { + rename_i hd tl Qtl + intro nd ndin + cases ndin + { + apply h₀ + } + { + simp + apply h₁ + apply Qtl + assumption + } + } + } + unfold Q at h + intro a + apply h simp - } - le_sound := by { - unfold BEq.beq instBEqOfDecidableEq + unfold nodes Vector.ofFn simp - intro β₀ β₁ β₂ beq ble - rw [←beq] - assumption + cases a + rename_i d snd + exists Fin.mk d snd } - le_supl := by simp - le_supr := by simp } + /- + namespace Test_Preds + def num_nodes := 14 + + instance : ToString (Finset ℕ) where + toString fs := + let _ := LtProp num_nodes + (vector_fn num_nodes (·)).foldl (fun repr nd => + if nd.data ∈ fs then + repr ++ " " ++ toString nd.data + else + repr) "" + + instance {α : Type} [ToString α] : ToString (Option α) where + toString | none => "none" | some a => toString a + + def FSI + : FiniteSolverInput (Finset ℕ) := { + + num_nodes := num_nodes + + edges := fun + | 0 => (· ∈ []) + | 1 => (· ∈ [2]) + | 2 => (· ∈ [3, 4]) + | 3 => (· ∈ [5]) + | 4 => (· ∈ [7, 8]) + | 5 => (· ∈ [6, 9]) + | 6 => (· ∈ [3, 10]) + | 7 => (· ∈ [10]) + | 8 => (· ∈ []) + | 9 => (· ∈ []) + | 10 => (· ∈ [11, ]) + | 11 => (· ∈ [7, 13]) + | 12 => (· ∈ []) + | 13 => (· ∈ []) + | _ => fun _ => false + transitions n := + (insert n ·) + + + + bot := Finset.empty + + + + transitions_sound := by { + unfold BEq.beq instBEqOfDecidableEq + simp + } + le_sound := by { + unfold BEq.beq instBEqOfDecidableEq + simp + intro β₀ β₁ β₂ beq ble + rw [←beq] + assumption + } + le_supl := by simp + le_supr := by simp + } - def xx := (FiniteDataflowProblem num_nodes FSI).solve.map ((·.1)) - #print xx - #eval! xx - end Test_Preds - -/ -end FiniteSolver + def xx := (FiniteDataflowProblem num_nodes FSI).solve.map ((·.1)) + #print xx + #eval! xx + end Test_Preds + -/ +end FiniteDataflowProblemSolver From 0026234c0ce64ab37154e187c44cb1b660c690b1 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Tue, 1 Jul 2025 13:37:27 -0400 Subject: [PATCH 03/22] make more readable --- KLR/Compile/Dataflow.lean | 299 +++++++++++++++++++++----------------- 1 file changed, 169 insertions(+), 130 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 82c8dc73..1faddfd5 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -67,145 +67,172 @@ def FiniteDataflowProblem {β : Type} ... ``` `DataflowProblem.solve` may then be called on this instance. --/ -abbrev ℕ := Nat +## Code by `Section` -section Basics +`Section Basics`- defines basic `Node`, `NodeProp`, and `NodeMap `definitions. + Culminates in `DataflowProblem` definition relying on `NodeMap`s. -/- - An instance `_ : NodeProp α` fixes a `node_prop : α → Prop` that - defines the set of nodes (note `Set α := α → Prop`) in the carrier - graph. --/ -class NodeProp (α : Type) where - node_prop : α → Prop +`Section DataflowProblemSolver` - defines computations and logic on `DataflowProblem`s, + culminating in `DataflowProblem.solve` definition that provides a solution + to dataflow problems. -/- - With a `NodeProp α` in scope, `Node α` is the subtype of `a : α` that - can prove `node_prop a` (i.e., are indeed nodes in the carrier graph) +`Section FiniteDataflowProblemSolver` - simplies the process of constructing + `DataflowProblem`s by proviing the `FiniteSolverInput` class that uses + `ℕ` indexing for nodes, and can be transformed by `FiniteDataflowProblem` + to a `DataflowProblem`. -/ -structure Node (α : Type) [NP : NodeProp α] where - data : α - sound : NP.node_prop data -instance {α} [TSA : ToString α] [NodeProp α]: ToString (Node α) where - toString := (TSA.toString ·.data) - -instance {α} [BEq α] [NodeProp α]: BEq (Node α) where - beq a₀ a₁ := a₀.data == a₁.data +abbrev ℕ := Nat /- - In the context of a set of nodes `Node α` fixed by a `NodeProp α`, an - instance of `NodeMap α` is a constructor for map objects whose domain - is the nodes of the carrier graph and whose codomain is a datatype `β`. - - Several utilities, as well as soundness theorems on them including - two induction principles, are required as well. --/ -class NodeMap (α : Type) extends NodeProp α where - μ (β : Type) : Type -- type of maps - const {β} : β → μ β -- empty instance - of_func {β} : (Node α → β) → μ β --instance from func - get {β} : (μ β) → Node α → β - fold {β γ} : (μ β) → ((Node α) → γ → γ) → γ → γ - app_unary {β γ} : (μ β) → (β → γ) → (μ γ) - app_binary {β₀ β₁ γ} : (μ β₀) → (μ β₁) → (β₀ → β₁ → γ) → (μ γ) - - const_get {β} (b : β) a : get (const b) a = b - of_func_get {β} (f : Node α → β) a : get (of_func f) a = f a - of_map_get {β γ} μ (f : β → γ) a : get (app_unary μ f) a = f (get μ a) - of_app_binary_get {β₀ β₁ γ} μ₀ μ₁ (f : β₀ → β₁ → γ) a - : get (app_binary μ₀ μ₁ f) a = f (get μ₀ a) (get μ₁ a) - - fold_ind {β γ} {ν : μ β} {γ₀ : γ} {acc : (Node α) → γ → γ} : - (P : γ → Prop) → - (P γ₀) → - (∀ a γ, P γ → P (acc a γ)) → - P (fold ν acc γ₀) - - fold_strong_ind {β γ} {ν : μ β} {γ₀ : γ} {acc : Node α → γ → γ} : - (P : Node α → γ → Prop) → - (∀ a γ₀, P a (acc a γ₀)) → - (∀ a γ₀ b, P a γ₀ → P a (acc b γ₀)) → - (∀ a, P a (fold ν acc γ₀)) - -notation μ "fold⟪" st "," acc "⟫" => NodeMap.fold μ acc st - -instance {α β : Type} [ToString α] [ToString β] [NM:NodeMap α] - : ToString (NM.μ β) where - toString μ := NM.fold μ (fun nd str => - str ++ "{" ++ (toString nd.data) ++ ":" - ++ (toString (NM.get μ nd)) ++ "}\n") "" - -infix:90 "◃" => NodeMap.get - -def NodeMap.call_const (α : Type) {β : Type} (b : β) [NodeMap α] - := NodeMap.const (α:=α) b -notation "⟪" α "↦" b "⟫"=> NodeMap.call_const α b - -notation "⟦" α "," β "⟧" => NodeMap.μ α β - -notation μ "map⟪" f "⟫" => NodeMap.app_unary μ f - -notation "of_func⟪" f "⟫" => NodeMap.of_func f - -notation "map2⟪" μ₀ "," μ₁ "," f "⟫" => NodeMap.app_binary μ₀ μ₁ f - -def NodeMap.LE {α β : Type} [NodeMap α] [LE β] (μ₀ μ₁ : ⟦α, β⟧) := (a : Node α) → (μ₀◃a ≤ μ₁◃a) -infix:90 "⟪≤⟫" => NodeMap.LE -instance {α β : Type} [NodeMap α] [LT β] : LT ⟦α, β⟧ where - lt μ₀ μ₁ := (a : Node α) → (μ₀◃a < μ₁◃a) -def NodeMap.Max {α β : Type} [NodeMap α] [Max β] (μ₀ μ₁ : ⟦α , β⟧) := - map2⟪μ₀, μ₁, (Max.max · ·)⟫ -infix:90 "⟪⊔⟫" => NodeMap.Max -instance {α β : Type} [NodeMap α] [BEq β] : BEq ⟦α, β⟧ where - beq μ₀ μ₁ := μ₀ fold⟪true, (fun a prev => prev ∧ (μ₀◃a == μ₁◃a))⟫ -instance {α β : Type} [NodeMap α] [ToString α] [ToString β] : ToString ⟦α, β⟧ where - toString μ := μ fold⟪"", (fun nd repr => repr ++ - "\n{" ++ toString nd.data ++ ": " ++ toString (μ◃nd) ++ "}")⟫ - - --- copied from Mathlib for utility -class Preorder (α : Type) extends LE α, LT α where - le_refl : ∀ a : α, a ≤ a - le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c - lt := fun a b => a ≤ b ∧ ¬b ≤ a - lt_iff_le_not_ge : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl - -instance (α : Type) [Preorder α] : LE α where - le := LE.le - --- An instance `HasBot α` fixes a bottom element (`⊥`) of type `α`. -class HasBot (α : Type) where - bot : α - -notation "⊥" => HasBot.bot + The section `Basics` provides the basic typeclasses, structures, and + notations needed to define `DataflowProblem` - including maps, + map operations, and operations like `≤` and `⊔` -/ +section Basics -/- - A `DataflowProblem α β` extends an map constructor `NodeMap α` with choices of - `τ : ⟦α, (β → β)⟧`, the node-indexed map of transition functions, and - `σ : ⟦α, (List (Node α))⟧`, the node-indexed map of succesor lists fixing - the graph topology. Two soundness theorems are requires relating the `≤` - relation `τ`, and the `==` relation on `β` (as provided by their respective - included typeclasses). The `⊔` and `≤` relations (on `⟦α, β⟧`), must also - be proven. --/ -class DataflowProblem (α β : Type) extends NodeMap α, Max β, BEq β, Preorder β, HasBot β -where - τ : ⟦α, (β → β)⟧ -- transition functions - σ : ⟦α, (List (Node α))⟧ -- successor relation + /- + An instance `_ : NodeProp α` fixes a `node_prop : α → Prop` that + defines the set of nodes (note `Set α := α → Prop`) in the carrier + graph. + -/ + class NodeProp (α : Type) where + node_prop : α → Prop + + /- + With a `NodeProp α` in scope, `Node α` is the subtype of `a : α` that + can prove `node_prop a` (i.e., are indeed nodes in the carrier graph) + -/ + structure Node (α : Type) [NP : NodeProp α] where + data : α + sound : NP.node_prop data + + instance {α} [TSA : ToString α] [NodeProp α]: ToString (Node α) where + toString := (TSA.toString ·.data) + + instance {α} [BEq α] [NodeProp α]: BEq (Node α) where + beq a₀ a₁ := a₀.data == a₁.data + + /- + In the context of a set of nodes `Node α` fixed by a `NodeProp α`, an + instance of `NodeMap α` is a constructor for map objects whose domain + is the nodes of the carrier graph and whose codomain is a datatype `β`. + + Several utilities, as well as soundness theorems on them including + two induction principles, are required as well. + -/ + class NodeMap (α : Type) extends NodeProp α where + μ (β : Type) : Type -- type of maps + const {β} : β → μ β -- empty instance + of_func {β} : (Node α → β) → μ β --instance from func + get {β} : (μ β) → Node α → β + fold {β γ} : (μ β) → ((Node α) → γ → γ) → γ → γ + app_unary {β γ} : (μ β) → (β → γ) → (μ γ) + app_binary {β₀ β₁ γ} : (μ β₀) → (μ β₁) → (β₀ → β₁ → γ) → (μ γ) + + const_get {β} (b : β) a : get (const b) a = b + of_func_get {β} (f : Node α → β) a : get (of_func f) a = f a + of_map_get {β γ} μ (f : β → γ) a : get (app_unary μ f) a = f (get μ a) + of_app_binary_get {β₀ β₁ γ} μ₀ μ₁ (f : β₀ → β₁ → γ) a + : get (app_binary μ₀ μ₁ f) a = f (get μ₀ a) (get μ₁ a) + + fold_ind {β γ} {ν : μ β} {γ₀ : γ} {acc : (Node α) → γ → γ} : + (P : γ → Prop) → + (P γ₀) → + (∀ a γ, P γ → P (acc a γ)) → + P (fold ν acc γ₀) + + fold_strong_ind {β γ} {ν : μ β} {γ₀ : γ} {acc : Node α → γ → γ} : + (P : Node α → γ → Prop) → + (∀ a γ₀, P a (acc a γ₀)) → + (∀ a γ₀ b, P a γ₀ → P a (acc b γ₀)) → + (∀ a, P a (fold ν acc γ₀)) + + notation μ "fold⟪" st "," acc "⟫" => NodeMap.fold μ acc st + + instance {α β : Type} [ToString α] [ToString β] [NM:NodeMap α] + : ToString (NM.μ β) where + toString μ := NM.fold μ (fun nd str => + str ++ "{" ++ (toString nd.data) ++ ":" + ++ (toString (NM.get μ nd)) ++ "}\n") "" + + infix:90 "◃" => NodeMap.get + + def NodeMap.call_const (α : Type) {β : Type} (b : β) [NodeMap α] + := NodeMap.const (α:=α) b + notation "⟪" α "↦" b "⟫"=> NodeMap.call_const α b + + notation "⟦" α "," β "⟧" => NodeMap.μ α β + + notation μ "map⟪" f "⟫" => NodeMap.app_unary μ f + + notation "of_func⟪" f "⟫" => NodeMap.of_func f + + notation "map2⟪" μ₀ "," μ₁ "," f "⟫" => NodeMap.app_binary μ₀ μ₁ f + + def NodeMap.LE {α β : Type} [NodeMap α] [LE β] (μ₀ μ₁ : ⟦α, β⟧) := (a : Node α) → (μ₀◃a ≤ μ₁◃a) + infix:90 "⟪≤⟫" => NodeMap.LE + instance {α β : Type} [NodeMap α] [LT β] : LT ⟦α, β⟧ where + lt μ₀ μ₁ := (a : Node α) → (μ₀◃a < μ₁◃a) + def NodeMap.Max {α β : Type} [NodeMap α] [Max β] (μ₀ μ₁ : ⟦α , β⟧) := + map2⟪μ₀, μ₁, (Max.max · ·)⟫ + infix:90 "⟪⊔⟫" => NodeMap.Max + instance {α β : Type} [NodeMap α] [BEq β] : BEq ⟦α, β⟧ where + beq μ₀ μ₁ := μ₀ fold⟪true, (fun a prev => prev ∧ (μ₀◃a == μ₁◃a))⟫ + instance {α β : Type} [NodeMap α] [ToString α] [ToString β] : ToString ⟦α, β⟧ where + toString μ := μ fold⟪"", (fun nd repr => repr ++ + "\n{" ++ toString nd.data ++ ": " ++ toString (μ◃nd) ++ "}")⟫ + + + -- copied from Mathlib for utility + class Preorder (α : Type) extends LE α, LT α where + le_refl : ∀ a : α, a ≤ a + le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c + lt := fun a b => a ≤ b ∧ ¬b ≤ a + lt_iff_le_not_ge : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl + + instance (α : Type) [Preorder α] : LE α where + le := LE.le + + -- An instance `HasBot α` fixes a bottom element (`⊥`) of type `α`. + class HasBot (α : Type) where + bot : α + + notation "⊥" => HasBot.bot + + /- + A `DataflowProblem α β` extends an map constructor `NodeMap α` with choices of + `τ : ⟦α, (β → β)⟧`, the node-indexed map of transition functions, and + `σ : ⟦α, (List (Node α))⟧`, the node-indexed map of succesor lists fixing + the graph topology. Two soundness theorems are requires relating the `≤` + relation `τ`, and the `==` relation on `β` (as provided by their respective + included typeclasses). The `⊔` and `≤` relations (on `⟦α, β⟧`), must also + be proven. + -/ + class DataflowProblem (α β : Type) extends NodeMap α, Max β, BEq β, Preorder β, HasBot β + where + τ : ⟦α, (β → β)⟧ -- transition functions + σ : ⟦α, (List (Node α))⟧ -- successor relation - τ_sound (α₀ : Node α) (β₀ β₁ : β) : (β₀ == β₁) → (τ◃α₀) β₀ == (τ◃α₀) β₁ - le_sound (β₀ β₁ β₂ : β) : (β₀ == β₁) → (β₀ ≤ β₂) → (β₁ ≤ β₂) + τ_sound (α₀ : Node α) (β₀ β₁ : β) : (β₀ == β₁) → (τ◃α₀) β₀ == (τ◃α₀) β₁ + le_sound (β₀ β₁ β₂ : β) : (β₀ == β₁) → (β₀ ≤ β₂) → (β₁ ≤ β₂) - map_le_supl (ν₀ ν₁ ν₂ : ⟦α, β⟧) (h : ν₀ ⟪≤⟫ ν₁) : (ν₀ ⟪≤⟫ (ν₁ ⟪⊔⟫ ν₂)) - map_le_supr (ν₀ ν₁ ν₂ : ⟦α, β⟧) (h : ν₀ ⟪≤⟫ ν₂) : (ν₀ ⟪≤⟫ (ν₁ ⟪⊔⟫ ν₂)) + map_le_supl (ν₀ ν₁ ν₂ : ⟦α, β⟧) (h : ν₀ ⟪≤⟫ ν₁) : (ν₀ ⟪≤⟫ (ν₁ ⟪⊔⟫ ν₂)) + map_le_supr (ν₀ ν₁ ν₂ : ⟦α, β⟧) (h : ν₀ ⟪≤⟫ ν₂) : (ν₀ ⟪≤⟫ (ν₁ ⟪⊔⟫ ν₂)) end Basics -/- +/- + The section `DataflowProblemSolver ` is paramterized on an instance of `DataflowProblem α β`. + It builds on the definitions of maps `⟦α, β⟧` from `NodeMap α`, and on the transition functions + `τ ◃ a` and succesor lists `σ ◃ a` for each node `a : Node α` (`◃` used as notation for map get) + provided by the `DataflowProblem` to compute a series of utility values, functions, and soundness + theorems ultimately definiting `DataflowProblem.solve`. This `solve` function performs a fixpoint + search for a solution to this dataflow problem instance. Its return type :`Option ((ν : ⟦α, β⟧) ×' I' ν)`, + captures that the search may fail, as it iterates only for a maximm of `(depth : ℕ) := 1000` rounds. + The `some` case, on the other hand, provides `ν : ⟦α, β⟧` - the map from nodes to data `β` that solves + the dataflow problem, and a `I' ν : Prop` - which captures that `ν` satisfies the dataflow problem. -/ section DataflowProblemSolver variable {α β : Type} [BEq α] {DP: DataflowProblem α β} @@ -474,6 +501,17 @@ section DataflowProblemSolver end DataflowProblemSolver +/- + The section `FiniteDataflowProblemSolver` provides a structure type definition + `FiniteSolverInput β`, that can be easily instantiated with any graph over + `num_nodes : ℕ` nodes, with data of type `β`, as long as the edge relation and + transition functions can be described by numbered node index. To fully instantiate + a `FiniteSolverInput`, 4 simple soundness theorems relating largely the relations + on `β` must be proved. + `FiniteDataflowProblem ... FiniteSolverInput β → DataflowProblem ℕ β` is the + key function, lifting a `FiniteSolverInput` to `DataflowProblem` admitting the + solver function `sound`. +-/ section FiniteDataflowProblemSolver variable (n : Nat) -- size of arrays @@ -609,7 +647,6 @@ section FiniteDataflowProblemSolver } } - fold_strong_ind := by { intro β γ ν γ₀ acc P h₀ h₁ let Q (l : List (Node ℕ)) := ∀ nd ∈ l, P nd (List.foldr acc γ₀ l) @@ -641,8 +678,11 @@ section FiniteDataflowProblemSolver exists Fin.mk d snd } } - /- - namespace Test_Preds + +/- + This section is a test that relies on Mathlib, to be replaced with one + that does not as a TBD. +namespace Test_Preds def num_nodes := 14 instance : ToString (Finset ℕ) where @@ -705,6 +745,5 @@ section FiniteDataflowProblemSolver def xx := (FiniteDataflowProblem num_nodes FSI).solve.map ((·.1)) #print xx #eval! xx - end Test_Preds - -/ -end FiniteDataflowProblemSolver +end Test_Preds +-/ From b5ffe68d96df5643ed113f914ec19e02ee9ae030 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Wed, 2 Jul 2025 09:12:21 -0400 Subject: [PATCH 04/22] start working on RBMap impl --- KLR/Compile/Dataflow.lean | 69 ++++++++++++++++++++++++++++++++++++--- 1 file changed, 65 insertions(+), 4 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 1faddfd5..484ab0db 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -82,6 +82,7 @@ def FiniteDataflowProblem {β : Type} ... `ℕ` indexing for nodes, and can be transformed by `FiniteDataflowProblem` to a `DataflowProblem`. -/ +import Lean.Data.RBMap abbrev ℕ := Nat @@ -550,11 +551,9 @@ section FiniteDataflowProblemSolver def vector_fn {β : Type} (f : NodeT n → β) : Vector β n := Vector.ofFn (f ∘ (fin_to_node n)) - #check Vector.rec - def FiniteDataflowProblem {β : Type} - [M: Max β] - [B: BEq β] + [Max β] + [BEq β] [Preorder β] [HasBot β] (FSI : FiniteSolverInput β) @@ -679,6 +678,68 @@ section FiniteDataflowProblemSolver } } +section RBMapImpl + variable {γ ρ} {_:Ord γ} {_:BEq ρ} {_:Preorder ρ} {_:DecidableLE ρ} {_:Max ρ} + variable {Γ : List γ} + + def instBEq : BEq (Lean.RBMap γ ρ Ord.compare) := { + beq μ₀ μ₁ := Γ.all (fun g ↦ + match μ₀.find? g, μ₁.find? g with + | none, none => true + | none, some _ => false + | some _, none => false + | some r₀, some r₁ => r₀ == r₁) + } + + def instPreorder : Preorder (Lean.RBMap γ ρ Ord.compare) := { + le μ₀ μ₁ := Γ.all (fun g ↦ + match μ₀.find? g, μ₁.find? g with + | none, none => true + | none, some _ => true + | some _, none => false + | some r₀, some r₁ => r₀ ≤ r₁) + le_refl := by { + simp + intro μ₀ g hg + cases (Lean.RBMap.find? μ₀ g)<;> simp + apply Preorder.le_refl + } + le_trans := by { + simp + intro μ₀ μ₁ μ₂ le₀₁ le₁₂ g gΓ + let le₀₁ := le₀₁ g gΓ + let le₁₂ := le₁₂ g gΓ + cases h₀ : Lean.RBMap.find? μ₀ g <;> + cases h₁ : Lean.RBMap.find? μ₁ g<;> + cases h₂ : Lean.RBMap.find? μ₂ g <;> + simp<;> + rw [h₀, h₁] at le₀₁<;>simp at le₀₁<;> + rw [h₁, h₂] at le₁₂<;>simp at le₁₂ + rename_i r₀ r₁ r₂ + exact (Preorder.le_trans r₀ r₁ r₂ le₀₁ le₁₂) + } + } + + def instMax : Max (Lean.RBMap γ ρ Ord.compare) := { + max μ₀ μ₁ := μ₀.mergeBy (fun _ ↦ (·⊔·)) μ₁ + } + + def instH : HasBot (Lean.RBMap γ ρ Ord.compare) := { + bot := Lean.RBMap.empty + } + + def FSI : @FiniteSolverInput (Lean.RBMap γ ρ Ord.compare) + (instBEq (Γ:=Γ)) (instPreorder (Γ:=Γ)) instMax instH := { + num_nodes := sorry + edges := sorry + + } +end RBMapImpl + + + + + /- This section is a test that relies on Mathlib, to be replaced with one that does not as a TBD. From 110e5e056167f66761fb8b4650d984533368f45b Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Wed, 2 Jul 2025 13:37:58 -0400 Subject: [PATCH 05/22] Clean up code and work on a double map impl --- KLR/Compile/Dataflow.lean | 341 ++++++++++++++++++++++++++++---------- 1 file changed, 251 insertions(+), 90 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 484ab0db..c8ca54b7 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -159,9 +159,7 @@ section Basics infix:90 "◃" => NodeMap.get - def NodeMap.call_const (α : Type) {β : Type} (b : β) [NodeMap α] - := NodeMap.const (α:=α) b - notation "⟪" α "↦" b "⟫"=> NodeMap.call_const α b + notation "⟪" α "↦" b "⟫"=> NodeMap.const (α:=α) b notation "⟦" α "," β "⟧" => NodeMap.μ α β @@ -171,26 +169,26 @@ section Basics notation "map2⟪" μ₀ "," μ₁ "," f "⟫" => NodeMap.app_binary μ₀ μ₁ f - def NodeMap.LE {α β : Type} [NodeMap α] [LE β] (μ₀ μ₁ : ⟦α, β⟧) := (a : Node α) → (μ₀◃a ≤ μ₁◃a) - infix:90 "⟪≤⟫" => NodeMap.LE - instance {α β : Type} [NodeMap α] [LT β] : LT ⟦α, β⟧ where - lt μ₀ μ₁ := (a : Node α) → (μ₀◃a < μ₁◃a) - def NodeMap.Max {α β : Type} [NodeMap α] [Max β] (μ₀ μ₁ : ⟦α , β⟧) := - map2⟪μ₀, μ₁, (Max.max · ·)⟫ - infix:90 "⟪⊔⟫" => NodeMap.Max + instance {α β : Type} [NodeMap α] [LE β] : LE ⟦α, β⟧ where + le μ₀ μ₁ := (a : Node α) → (μ₀◃a ≤ μ₁◃a) + + instance {α β : Type} [NodeMap α] [Max β] : Max ⟦α, β⟧ where + max μ₀ μ₁ := map2⟪μ₀, μ₁, (Max.max · ·)⟫ + + infix:100 "⊔" => Max.max + + instance {α β : Type} [NodeMap α] [BEq β] : BEq ⟦α, β⟧ where beq μ₀ μ₁ := μ₀ fold⟪true, (fun a prev => prev ∧ (μ₀◃a == μ₁◃a))⟫ + instance {α β : Type} [NodeMap α] [ToString α] [ToString β] : ToString ⟦α, β⟧ where toString μ := μ fold⟪"", (fun nd repr => repr ++ "\n{" ++ toString nd.data ++ ": " ++ toString (μ◃nd) ++ "}")⟫ - -- copied from Mathlib for utility - class Preorder (α : Type) extends LE α, LT α where + class Preorder (α : Type) extends LE α where le_refl : ∀ a : α, a ≤ a le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c - lt := fun a b => a ≤ b ∧ ¬b ≤ a - lt_iff_le_not_ge : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl instance (α : Type) [Preorder α] : LE α where le := LE.le @@ -201,6 +199,28 @@ section Basics notation "⊥" => HasBot.bot + instance {α β : Type} [NodeMap α] [HasBot β] : HasBot ⟦α, β⟧ where + bot := NodeMap.const (α:=α) ⊥ + + instance {α β : Type} [NodeMap α] [Preorder β] : Preorder ⟦α , β⟧ := { + le := LE.le + le_refl := by { + unfold LE.le instLEμ + simp + intros + apply Preorder.le_refl + } + le_trans := by { + unfold LE.le instLEμ + simp + intros + rename_i a b c h₀ h₁ nd + apply (Preorder.le_trans (a◃nd) (b◃nd) (c◃nd)) + apply h₀ + apply h₁ + } + } + /- A `DataflowProblem α β` extends an map constructor `NodeMap α` with choices of `τ : ⟦α, (β → β)⟧`, the node-indexed map of transition functions, and @@ -218,8 +238,8 @@ section Basics τ_sound (α₀ : Node α) (β₀ β₁ : β) : (β₀ == β₁) → (τ◃α₀) β₀ == (τ◃α₀) β₁ le_sound (β₀ β₁ β₂ : β) : (β₀ == β₁) → (β₀ ≤ β₂) → (β₁ ≤ β₂) - map_le_supl (ν₀ ν₁ ν₂ : ⟦α, β⟧) (h : ν₀ ⟪≤⟫ ν₁) : (ν₀ ⟪≤⟫ (ν₁ ⟪⊔⟫ ν₂)) - map_le_supr (ν₀ ν₁ ν₂ : ⟦α, β⟧) (h : ν₀ ⟪≤⟫ ν₂) : (ν₀ ⟪≤⟫ (ν₁ ⟪⊔⟫ ν₂)) + map_le_supl (ν₀ ν₁ ν₂ : ⟦α, β⟧) (h : ν₀ ≤ ν₁) : (ν₀ ≤ (ν₁ ⊔ ν₂)) + map_le_supr (ν₀ ν₁ ν₂ : ⟦α, β⟧) (h : ν₀ ≤ ν₂) : (ν₀ ≤ (ν₁ ⊔ ν₂)) end Basics @@ -256,7 +276,7 @@ section DataflowProblemSolver unfold I R E intro α₀ α₁ edge left - unfold ν₀ NodeMap.call_const + unfold ν₀ rw [NodeMap.const_get] } @@ -264,7 +284,7 @@ section DataflowProblemSolver of_func⟪(fun a' => if ε a a' then ((τ◃a) (ν◃a).1) else ⊥)⟫ def Δ₀ (ν : ⟦α, (β × Bool)⟧) : ⟦α, β⟧ := - ν fold⟪ν map⟪(·.1)⟫, (fun a ν₀ => if (ν◃a).2 then ν₀ ⟪⊔⟫ (δ ν a) else ν₀)⟫ + ν fold⟪ν map⟪(·.1)⟫, (fun a ν₀ => if (ν◃a).2 then ν₀ ⊔ (δ ν a) else ν₀)⟫ def Δ (ν : ⟦α, (β × Bool)⟧) : ⟦α, (β × Bool)⟧ := let ν' := Δ₀ ν @@ -311,22 +331,15 @@ section DataflowProblemSolver rw [NodeMap.of_map_get] } - omit [BEq α] in theorem map_le_refl (ν : ⟦α, β⟧) : ν ⟪≤⟫ ν := by { - unfold NodeMap.LE - intros - apply Preorder.le_refl - } - - - theorem δlessΔ (ν : ⟦α, (β × Bool)⟧) (a₀ : Node α) (h: (ν ◃ a₀).2): δ ν a₀ ⟪≤⟫ Δ₀ ν := by { - let P a ν₀ := (ν◃a).2 = true → δ ν a ⟪≤⟫ ν₀ + theorem δlessΔ (ν : ⟦α, (β × Bool)⟧) (a₀ : Node α) (h: (ν ◃ a₀).2): δ ν a₀ ≤ Δ₀ ν := by { + let P a ν₀ := (ν◃a).2 = true → δ ν a ≤ ν₀ apply (NodeMap.fold_strong_ind P)<;>try unfold P { intro a γ₀ ha rw [ha] simp apply map_le_supr - apply map_le_refl + apply Preorder.le_refl } { intro a γ₀ b ha ha' @@ -360,11 +373,11 @@ section DataflowProblemSolver } } - theorem Δmono (ν : ⟦α, (β × Bool)⟧) : (strip_bools ν) ⟪≤⟫ Δ₀ ν := by { - let P ν' := (strip_bools ν) ⟪≤⟫ ν' + theorem Δmono (ν : ⟦α, (β × Bool)⟧) : (strip_bools ν) ≤ Δ₀ ν := by { + let P ν' := (strip_bools ν) ≤ ν' apply NodeMap.fold_ind { - unfold NodeMap.LE + unfold LE.le intro a rw [NodeMap.of_map_get] rw [strip_bools_snd] @@ -515,7 +528,7 @@ end DataflowProblemSolver -/ section FiniteDataflowProblemSolver - variable (n : Nat) -- size of arrays + variable (n : Nat) -- number of nodes infix:90 "⊔" => Max.max @@ -531,8 +544,8 @@ section FiniteDataflowProblemSolver transitions_sound n (β₀ β₁ : β) : (β₀ == β₁) → (transitions n) β₀ == (transitions n) β₁ le_sound (β₀ β₁ β₂ : β) : (β₀ == β₁) → (β₀ ≤ β₂) → (β₁ ≤ β₂) - le_supl (β₀ β₁ : β) : β₀ ≤ β₀ ⊔ β₁ - le_supr (β₀ β₁ : β) : β₁ ≤ β₀ ⊔ β₁ + le_supl (β₀ β₁ : β) : β₀ ≤ Max.max β₀ β₁ + le_supr (β₀ β₁ : β) : β₁ ≤ Max.max β₀ β₁ def LtProp : NodeProp ℕ where node_prop n' := n' < n @@ -551,16 +564,12 @@ section FiniteDataflowProblemSolver def vector_fn {β : Type} (f : NodeT n → β) : Vector β n := Vector.ofFn (f ∘ (fin_to_node n)) - def FiniteDataflowProblem {β : Type} - [Max β] - [BEq β] - [Preorder β] - [HasBot β] - (FSI : FiniteSolverInput β) - : DataflowProblem ℕ β - := let NP : NodeProp ℕ := { + def FiniteNodeProp : NodeProp ℕ := { node_prop n' := n' < n - } ; {NP with + } + + def FiniteNodeMap : NodeMap ℕ := { + FiniteNodeProp n with μ β := Vector β n const β := vector_fn n (fun _ => β) @@ -598,39 +607,6 @@ section FiniteDataflowProblemSolver simp } - τ := vector_fn n (FSI.transitions ·.data) - σ := vector_fn n (fun nd => - (nodes n).toList.filter (FSI.edges nd.data ·.data) - ) - - τ_sound := by { - intro α₀ β₀ β₁ beq - unfold vector_fn Vector.ofFn Vector.get fin_to_node node_to_fin - simp - apply FSI.transitions_sound - assumption - } - le_sound := FSI.le_sound - - map_le_supl := by { - unfold NodeMap.LE NodeMap.Max - intro ν₀ ν₁ ν₂ h a - unfold NodeMap.app_binary node_to_fin Vector.map Vector.get nodes fin_to_node - simp - apply Preorder.le_trans - {apply h} - {apply FSI.le_supl} - } - map_le_supr := by { - unfold NodeMap.LE NodeMap.Max - intro ν₀ ν₁ ν₂ h a - unfold NodeMap.app_binary node_to_fin Vector.map Vector.get nodes fin_to_node - simp - apply Preorder.le_trans - {apply h} - {apply FSI.le_supr} - } - fold_ind := by { intro β γ ν γ₀ acc P h₀ h₁ induction ((nodes n).toList) @@ -648,7 +624,7 @@ section FiniteDataflowProblemSolver fold_strong_ind := by { intro β γ ν γ₀ acc P h₀ h₁ - let Q (l : List (Node ℕ)) := ∀ nd ∈ l, P nd (List.foldr acc γ₀ l) + let Q l := ∀ nd ∈ l, P nd (List.foldr acc γ₀ l) have h : Q (nodes n).toList := by { induction (nodes n).toList<;>unfold Q; simp { @@ -676,22 +652,97 @@ section FiniteDataflowProblemSolver rename_i d snd exists Fin.mk d snd } + } + + def FiniteDataflowProblem {β : Type} + [BEq β] + [P:Preorder β] + [Max β] + [HasBot β] + (FSI : FiniteSolverInput β) + : DataflowProblem ℕ β + := let FNM := FiniteNodeMap n; + { + τ := vector_fn n (FSI.transitions ·.data) + σ := vector_fn n (fun nd => + (nodes n).toList.filter (FSI.edges nd.data ·.data) + ) + + τ_sound := by { + intro α₀ β₀ β₁ beq + unfold vector_fn Vector.ofFn NodeMap.get + unfold FNM FiniteNodeMap Vector.get fin_to_node node_to_fin + simp + apply FSI.transitions_sound + assumption + } + + le_sound := FSI.le_sound + + map_le_supl := by { + unfold LE.le instLEμ Max.max instMaxμ + simp + intro ν₀ ν₁ ν₂ h a + unfold NodeMap.app_binary NodeMap.get + unfold FNM FiniteNodeMap node_to_fin Vector.map Vector.get nodes fin_to_node + simp + apply Preorder.le_trans + {apply h} + {apply FSI.le_supl} + } + map_le_supr := by { + unfold LE.le instLEμ Max.max instMaxμ + intro ν₀ ν₁ ν₂ h a + unfold NodeMap.app_binary NodeMap.get FNM + unfold FiniteNodeMap node_to_fin Vector.map Vector.get nodes fin_to_node + simp + apply Preorder.le_trans + {apply h} + {apply FSI.le_supr} + } + } + +section InnerMapImpl + variable (ρ) [BEq ρ] [DecidableEq ρ] [Preorder ρ] [DecidableLE ρ] [Max ρ] [HasBot ρ] + variable (num_nodes num_keys : ℕ) + + def FNM : NodeMap ℕ := (FiniteNodeMap num_keys) + + def FSI : FiniteSolverInput ((FNM num_keys).μ ρ) := { + num_nodes := num_nodes + edges := sorry + transitions := sorry + + transitions_sound := sorry + le_sound := by { + + } + le_supl := by { + + } + le_supr := by { + } + } + +end InnerMapImpl section RBMapImpl - variable {γ ρ} {_:Ord γ} {_:BEq ρ} {_:Preorder ρ} {_:DecidableLE ρ} {_:Max ρ} - variable {Γ : List γ} + variable (γ ρ) [Ord γ] [DecidableEq ρ] [Preorder ρ] [DecidableLE ρ] [Max ρ] + variable (Γ : List γ) - def instBEq : BEq (Lean.RBMap γ ρ Ord.compare) := { + abbrev μ := (Lean.RBMap γ ρ Ord.compare) + + instance instBEq : BEq (μ γ ρ) := { beq μ₀ μ₁ := Γ.all (fun g ↦ match μ₀.find? g, μ₁.find? g with | none, none => true | none, some _ => false | some _, none => false - | some r₀, some r₁ => r₀ == r₁) + | some r₀, some r₁ => r₀ = r₁) } - def instPreorder : Preorder (Lean.RBMap γ ρ Ord.compare) := { + instance instPreorder : Preorder (μ γ ρ) := { le μ₀ μ₁ := Γ.all (fun g ↦ match μ₀.find? g, μ₁.find? g with | none, none => true @@ -720,20 +771,130 @@ section RBMapImpl } } - def instMax : Max (Lean.RBMap γ ρ Ord.compare) := { + instance instMax : Max (μ γ ρ) := { max μ₀ μ₁ := μ₀.mergeBy (fun _ ↦ (·⊔·)) μ₁ - } - - def instH : HasBot (Lean.RBMap γ ρ Ord.compare) := { + } + instance instHasBot : HasBot (μ γ ρ) := { bot := Lean.RBMap.empty } - def FSI : @FiniteSolverInput (Lean.RBMap γ ρ Ord.compare) - (instBEq (Γ:=Γ)) (instPreorder (Γ:=Γ)) instMax instH := { - num_nodes := sorry - edges := sorry + section Prove_find_join + variable (μ₀ μ₁ : μ γ ρ) (g : γ) + theorem supl_none : μ₀.find? g = none → (μ₀⊔μ₁).find? g = μ₁.find? g := by { + intro h + unfold Max.max instMax Lean.RBMap.mergeBy Lean.RBMap.fold + cases hμ₀ : μ₀ + rename_i nd₀ wf₀ + cases hμ₁ : μ₁ + rename_i nd₁ wf₁ + simp + unfold Lean.RBNode.fold + induction nd₁ <;> simp + { + unfold Lean.RBMap.find? + simp + have h' : Lean.RBNode.find compare nd₀ g = none := by { + unfold Lean.RBMap.find? at h + rw [hμ₀] at h + simp at h + exact h + } + rw [h'] + unfold Lean.RBNode.find + trivial + } + { + } } + theorem supr_none : μ₁.find? g = none → (μ₀⊔μ₁).find? g = μ₀.find? g := sorry + theorem sup_some : ∀ ρ₀ ρ₁, μ₀.find? g = some ρ₀ → μ₁.find? g = some ρ₁ → + (μ₀⊔μ₁).find? g = some (ρ₀ ⊔ ρ₁) := sorry + + theorem find_join : (μ₀ ⊔ μ₁).find? g = + match (μ₀.find? g, μ₁.find? g) with + | (none, none) => none + | (some ρ, none) + | (none, some ρ) => some ρ + | (some ρ₀, some ρ₁) => ρ₀ ⊔ ρ₁ := by { + cases h₀ : (Lean.RBMap.find? μ₀ g) <;> + cases h₁ : (Lean.RBMap.find? μ₁ g) <;> simp + { + rw [supl_none] <;> assumption + } + { + rw [supl_none] <;> assumption + } + { + rw [supr_none] <;> assumption + } + { + rename_i ρ₀ ρ₁ + rw [sup_some] <;> assumption + } + } + + end Prove_find_join + + variable (num_nodes : ℕ) + variable (le_supl : ∀ ρ₀ ρ₁ : ρ, ρ₀ ≤ ρ₀ ⊔ ρ₁) + variable (le_supr : ∀ ρ₀ ρ₁ : ρ, ρ₁ ≤ ρ₀ ⊔ ρ₁) + + def SolverInput : @FiniteSolverInput (μ γ ρ) + (instBEq γ ρ Γ) (instPreorder γ ρ Γ) (instMax γ ρ) (instHasBot γ ρ) + := { + num_nodes := num_nodes + edges := sorry + transitions := sorry + + transitions_sound := sorry + le_sound := by { + unfold LE.le BEq.beq instLEOfPreorder instBEq Preorder.toLE instPreorder + simp + intro μ₀ μ₁ μ₂ h₀₁ h₀₂ g gΓ + let h₀₁ := h₀₁ g gΓ + let h₀₂ := h₀₂ g gΓ + cases h₀ : (Lean.RBMap.find? μ₀ g) <;> + cases h₁ : (Lean.RBMap.find? μ₁ g) <;> + cases h₂ : (Lean.RBMap.find? μ₂ g) <;> + rw [h₀, h₁] at h₀₁ <;> simp at h₀₁ <;> + rw [h₀, h₂] at h₀₂ <;> simp at h₀₂ + simp + rename_i ρ₀ ρ₁ ρ₂ + rw [←h₀₁] + assumption + } + + le_supl := by { + unfold LE.le instLEOfPreorder Preorder.toLE instPreorder + simp + intro μ₀ μ₁ g gΓ + cases h₀ : Lean.RBMap.find? μ₀ g <;> + cases h₁ : (Lean.RBMap.find? μ₁ g) <;> + cases h₀₁ : Lean.RBMap.find? (μ₀⊔μ₁) g <;> simp <;> + rw [find_join, h₀, h₁] at h₀₁ <;> + simp at h₀₁ <;> rw [←h₀₁] + apply Preorder.le_refl + apply le_supl + } + + le_supr := by { + unfold LE.le instLEOfPreorder Preorder.toLE instPreorder + simp + intro μ₀ μ₁ g gΓ + cases h₀ : Lean.RBMap.find? μ₀ g <;> + cases h₁ : (Lean.RBMap.find? μ₁ g) <;> + cases h₀₁ : Lean.RBMap.find? (μ₀⊔μ₁) g <;> simp <;> + rw [find_join, h₀, h₁] at h₀₁ <;> + simp at h₀₁ <;> rw [←h₀₁] + apply Preorder.le_refl + apply le_supr + } + } + + def solution := (FiniteDataflowProblem num_nodes + (SolverInput γ ρ Γ num_nodes le_supl le_supr)).solve + end RBMapImpl From 33fc033fc5e28bcdc0251bb3291d2bfd458e0e6d Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Wed, 2 Jul 2025 15:43:01 -0400 Subject: [PATCH 06/22] Finish filling in InnerMapImpl --- KLR/Compile/Dataflow.lean | 400 +++++++++++--------------------------- 1 file changed, 115 insertions(+), 285 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index c8ca54b7..31b685cc 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -81,6 +81,8 @@ def FiniteDataflowProblem {β : Type} ... `DataflowProblem`s by proviing the `FiniteSolverInput` class that uses `ℕ` indexing for nodes, and can be transformed by `FiniteDataflowProblem` to a `DataflowProblem`. + +`Section InnerMapImpl` - description TBD -/ import Lean.Data.RBMap @@ -131,7 +133,7 @@ section Basics app_unary {β γ} : (μ β) → (β → γ) → (μ γ) app_binary {β₀ β₁ γ} : (μ β₀) → (μ β₁) → (β₀ → β₁ → γ) → (μ γ) - const_get {β} (b : β) a : get (const b) a = b + of_const_get {β} (b : β) a : get (const b) a = b of_func_get {β} (f : Node α → β) a : get (of_func f) a = f a of_map_get {β γ} μ (f : β → γ) a : get (app_unary μ f) a = f (get μ a) of_app_binary_get {β₀ β₁ γ} μ₀ μ₁ (f : β₀ → β₁ → γ) a @@ -159,7 +161,7 @@ section Basics infix:90 "◃" => NodeMap.get - notation "⟪" α "↦" b "⟫"=> NodeMap.const (α:=α) b + notation "⟪↦" b "⟫"=> NodeMap.const b notation "⟦" α "," β "⟧" => NodeMap.μ α β @@ -177,9 +179,51 @@ section Basics infix:100 "⊔" => Max.max - - instance {α β : Type} [NodeMap α] [BEq β] : BEq ⟦α, β⟧ where + def NodeMap.instBEq {α β : Type} [NodeMap α] [BEq β] : BEq ⟦α, β⟧ := { beq μ₀ μ₁ := μ₀ fold⟪true, (fun a prev => prev ∧ (μ₀◃a == μ₁◃a))⟫ + } + + instance {α β : Type} [NodeMap α] [BEq β] : BEq ⟦α, β⟧ := NodeMap.instBEq + + theorem NodeMap.beq_ext {α β : Type} [BEq β] [NodeMap α] (μ₀ μ₁ : ⟦α, β⟧) + : μ₀ == μ₁ ↔ (∀ a, μ₀◃a == μ₁◃a) := by { + constructor + { + intro hμeq a + cases heq : (μ₀◃a == μ₁◃a) + { + have hμneq : (μ₀ == μ₁) = false := by { + unfold BEq.beq instBEqμ instBEq + simp + let P := fun a b ↦ (μ₀◃a == μ₁◃a) = false → b = false + apply (NodeMap.fold_strong_ind P)<;>try unfold P<;>try simp + { + intro a' b' eqa' neqa' + rw [eqa'] at neqa' + contradiction + } + { + exact heq + } + } + rw [hμeq] at hμneq + trivial + } + {trivial} + } + { + intro h + unfold BEq.beq instBEqμ instBEq + simp + apply (NodeMap.fold_ind (P:=(fun b↦b=true))) + {trivial} + { + intro a b bt + rw [bt, h] + trivial + } + } + } instance {α β : Type} [NodeMap α] [ToString α] [ToString β] : ToString ⟦α, β⟧ where toString μ := μ fold⟪"", (fun nd repr => repr ++ @@ -259,7 +303,7 @@ section DataflowProblemSolver variable {α β : Type} [BEq α] {DP: DataflowProblem α β} open DataflowProblem - def ν₀ : ⟦α, (β × Bool)⟧ := ⟪α↦(⊥, true)⟫ + def ν₀ : ⟦α, (β × Bool)⟧ := ⟪↦(⊥, true)⟫ def ε (a₀ a₁ : Node α) : Bool := List.elem a₁ (σ◃a₀) @@ -277,7 +321,7 @@ section DataflowProblemSolver intro α₀ α₁ edge left unfold ν₀ - rw [NodeMap.const_get] + rw [NodeMap.of_const_get] } def δ (ν : ⟦α, (β × Bool)⟧) (a : Node α) : ⟦α, β⟧ := -- step @@ -292,38 +336,21 @@ section DataflowProblemSolver def is_fix (ν : ⟦α, (β × Bool)⟧) : Bool := - ν fold⟪true, fun a prior => prior && !(ν◃a).2 ⟫ + ν map⟪fun x↦x.2⟫ == ⟪↦false⟫ - section - open Classical -- this can prolly be proven without contradiction or choice - omit [BEq α] in theorem is_fix_sound (ν : ⟦α, (β × Bool)⟧) + omit [BEq α] in theorem is_fix_sound (ν : ⟦α, (β × Bool)⟧) : is_fix ν → ∀ a, !(ν ◃ a).2 := by { + unfold is_fix intro h a - apply byContradiction - intro pν - simp at pν - have h' : is_fix ν = false := by { - unfold is_fix - let acc := fun prior a ↦ prior && !(ν◃a).2 - let P := fun a b ↦ (ν◃a).2 = true → b = false - apply (NodeMap.fold_strong_ind P)<;>try unfold P - { - simp - } - { - simp - intros a b af att - rw [att] at af - contradiction - } - { - apply pν - } + have h' : (ν map⟪fun x => x.snd⟫)◃a == ⟪↦false⟫◃a := by { + apply (NodeMap.beq_ext (ν map⟪fun x => x.snd⟫) ⟪↦false⟫).mp + assumption } - rw [h] at h' - contradiction + simp at h' + rw [NodeMap.of_map_get, NodeMap.of_const_get] at h' + rw [h'] + trivial } - end omit [BEq α] in theorem strip_bools_snd (ν : ⟦α, (β × Bool)⟧) (a : Node α) : ( (strip_bools ν)◃a = (ν◃a).1) := by { @@ -530,8 +557,6 @@ section FiniteDataflowProblemSolver variable (n : Nat) -- number of nodes - infix:90 "⊔" => Max.max - structure FiniteSolverInput (β : Type) [BEq β] [Preorder β] @@ -584,7 +609,7 @@ section FiniteDataflowProblemSolver (μ₀.get (node_to_fin n nd)) (μ₁.get (node_to_fin n nd))) - const_get := by { + of_const_get := by { intros unfold vector_fn Vector.get simp @@ -702,270 +727,75 @@ section FiniteDataflowProblemSolver } } +/- + description TBD +-/ section InnerMapImpl - variable (ρ) [BEq ρ] [DecidableEq ρ] [Preorder ρ] [DecidableLE ρ] [Max ρ] [HasBot ρ] + variable (ρ : Type) [DecidableEq ρ] [Preorder ρ] [DecidableLE ρ] [Max ρ] [HasBot ρ] + variable (le_supl:∀ ρ₀ ρ₁ : ρ, ρ₀ ≤ ρ₀ ⊔ ρ₁) + variable (le_supr:∀ ρ₀ ρ₁ : ρ, ρ₁ ≤ ρ₀ ⊔ ρ₁) variable (num_nodes num_keys : ℕ) + variable (edges : ℕ → ℕ → Bool) + variable (transitions : ℕ → ℕ → ρ → ρ) def FNM : NodeMap ℕ := (FiniteNodeMap num_keys) - def FSI : FiniteSolverInput ((FNM num_keys).μ ρ) := { + def FSI {_:NodeMap ℕ}: FiniteSolverInput (⟦ℕ, ρ⟧) := { num_nodes := num_nodes - edges := sorry - transitions := sorry - - transitions_sound := sorry - le_sound := by { + edges := edges + transitions n β₀ := of_func⟪fun k ↦ transitions n k.data (β₀◃k)⟫ + transitions_sound := by { + intro a β₀ β₁ βq + apply (NodeMap.beq_ext _ _).mpr + intro a + rw [NodeMap.of_func_get] + rw [NodeMap.of_func_get] + have h : β₀◃a == β₁◃a := by { + apply (NodeMap.beq_ext β₀ β₁).mp + assumption + } + have h' : β₀◃a = β₁◃a := by { + unfold BEq.beq instBEqOfDecidableEq at h + simp at h + assumption + } + rw [h'] + apply BEq.refl } - le_supl := by { - - } - le_supr := by { + le_sound := by { + unfold LE.le instLEOfPreorder Preorder.toLE instPreorderμ instLEμ + simp + intro β₀ β₁ β₂ eq₀₁ le₀₂ α + have h : β₀◃α == β₁◃α := by { + apply (NodeMap.beq_ext _ _).mp + assumption + } + unfold BEq.beq instBEqOfDecidableEq at h + simp at h + rw [←h] + apply le₀₂ } - } - -end InnerMapImpl - -section RBMapImpl - variable (γ ρ) [Ord γ] [DecidableEq ρ] [Preorder ρ] [DecidableLE ρ] [Max ρ] - variable (Γ : List γ) - abbrev μ := (Lean.RBMap γ ρ Ord.compare) - - instance instBEq : BEq (μ γ ρ) := { - beq μ₀ μ₁ := Γ.all (fun g ↦ - match μ₀.find? g, μ₁.find? g with - | none, none => true - | none, some _ => false - | some _, none => false - | some r₀, some r₁ => r₀ = r₁) - } - - instance instPreorder : Preorder (μ γ ρ) := { - le μ₀ μ₁ := Γ.all (fun g ↦ - match μ₀.find? g, μ₁.find? g with - | none, none => true - | none, some _ => true - | some _, none => false - | some r₀, some r₁ => r₀ ≤ r₁) - le_refl := by { + le_supl := by { + unfold LE.le instLEOfPreorder Preorder.toLE instPreorderμ instLEμ simp - intro μ₀ g hg - cases (Lean.RBMap.find? μ₀ g)<;> simp - apply Preorder.le_refl - } - le_trans := by { + intro β₀ β₁ a + unfold Max.max instMaxμ simp - intro μ₀ μ₁ μ₂ le₀₁ le₁₂ g gΓ - let le₀₁ := le₀₁ g gΓ - let le₁₂ := le₁₂ g gΓ - cases h₀ : Lean.RBMap.find? μ₀ g <;> - cases h₁ : Lean.RBMap.find? μ₁ g<;> - cases h₂ : Lean.RBMap.find? μ₂ g <;> - simp<;> - rw [h₀, h₁] at le₀₁<;>simp at le₀₁<;> - rw [h₁, h₂] at le₁₂<;>simp at le₁₂ - rename_i r₀ r₁ r₂ - exact (Preorder.le_trans r₀ r₁ r₂ le₀₁ le₁₂) - } - } - - instance instMax : Max (μ γ ρ) := { - max μ₀ μ₁ := μ₀.mergeBy (fun _ ↦ (·⊔·)) μ₁ + rw [NodeMap.of_app_binary_get] + apply le_supl } - instance instHasBot : HasBot (μ γ ρ) := { - bot := Lean.RBMap.empty - } - section Prove_find_join - variable (μ₀ μ₁ : μ γ ρ) (g : γ) - theorem supl_none : μ₀.find? g = none → (μ₀⊔μ₁).find? g = μ₁.find? g := by { - intro h - unfold Max.max instMax Lean.RBMap.mergeBy Lean.RBMap.fold - cases hμ₀ : μ₀ - rename_i nd₀ wf₀ - cases hμ₁ : μ₁ - rename_i nd₁ wf₁ + le_supr := by { + unfold LE.le instLEOfPreorder Preorder.toLE instPreorderμ instLEμ simp - unfold Lean.RBNode.fold - induction nd₁ <;> simp - { - unfold Lean.RBMap.find? - simp - have h' : Lean.RBNode.find compare nd₀ g = none := by { - unfold Lean.RBMap.find? at h - rw [hμ₀] at h - simp at h - exact h - } - rw [h'] - unfold Lean.RBNode.find - trivial - } - { - - } + intro β₀ β₁ a + unfold Max.max instMaxμ + simp + rw [NodeMap.of_app_binary_get] + apply le_supr } - theorem supr_none : μ₁.find? g = none → (μ₀⊔μ₁).find? g = μ₀.find? g := sorry - theorem sup_some : ∀ ρ₀ ρ₁, μ₀.find? g = some ρ₀ → μ₁.find? g = some ρ₁ → - (μ₀⊔μ₁).find? g = some (ρ₀ ⊔ ρ₁) := sorry - - theorem find_join : (μ₀ ⊔ μ₁).find? g = - match (μ₀.find? g, μ₁.find? g) with - | (none, none) => none - | (some ρ, none) - | (none, some ρ) => some ρ - | (some ρ₀, some ρ₁) => ρ₀ ⊔ ρ₁ := by { - cases h₀ : (Lean.RBMap.find? μ₀ g) <;> - cases h₁ : (Lean.RBMap.find? μ₁ g) <;> simp - { - rw [supl_none] <;> assumption - } - { - rw [supl_none] <;> assumption - } - { - rw [supr_none] <;> assumption - } - { - rename_i ρ₀ ρ₁ - rw [sup_some] <;> assumption - } - } - - end Prove_find_join - - variable (num_nodes : ℕ) - variable (le_supl : ∀ ρ₀ ρ₁ : ρ, ρ₀ ≤ ρ₀ ⊔ ρ₁) - variable (le_supr : ∀ ρ₀ ρ₁ : ρ, ρ₁ ≤ ρ₀ ⊔ ρ₁) - - def SolverInput : @FiniteSolverInput (μ γ ρ) - (instBEq γ ρ Γ) (instPreorder γ ρ Γ) (instMax γ ρ) (instHasBot γ ρ) - := { - num_nodes := num_nodes - edges := sorry - transitions := sorry - - transitions_sound := sorry - le_sound := by { - unfold LE.le BEq.beq instLEOfPreorder instBEq Preorder.toLE instPreorder - simp - intro μ₀ μ₁ μ₂ h₀₁ h₀₂ g gΓ - let h₀₁ := h₀₁ g gΓ - let h₀₂ := h₀₂ g gΓ - cases h₀ : (Lean.RBMap.find? μ₀ g) <;> - cases h₁ : (Lean.RBMap.find? μ₁ g) <;> - cases h₂ : (Lean.RBMap.find? μ₂ g) <;> - rw [h₀, h₁] at h₀₁ <;> simp at h₀₁ <;> - rw [h₀, h₂] at h₀₂ <;> simp at h₀₂ - simp - rename_i ρ₀ ρ₁ ρ₂ - rw [←h₀₁] - assumption - } - - le_supl := by { - unfold LE.le instLEOfPreorder Preorder.toLE instPreorder - simp - intro μ₀ μ₁ g gΓ - cases h₀ : Lean.RBMap.find? μ₀ g <;> - cases h₁ : (Lean.RBMap.find? μ₁ g) <;> - cases h₀₁ : Lean.RBMap.find? (μ₀⊔μ₁) g <;> simp <;> - rw [find_join, h₀, h₁] at h₀₁ <;> - simp at h₀₁ <;> rw [←h₀₁] - apply Preorder.le_refl - apply le_supl - } - - le_supr := by { - unfold LE.le instLEOfPreorder Preorder.toLE instPreorder - simp - intro μ₀ μ₁ g gΓ - cases h₀ : Lean.RBMap.find? μ₀ g <;> - cases h₁ : (Lean.RBMap.find? μ₁ g) <;> - cases h₀₁ : Lean.RBMap.find? (μ₀⊔μ₁) g <;> simp <;> - rw [find_join, h₀, h₁] at h₀₁ <;> - simp at h₀₁ <;> rw [←h₀₁] - apply Preorder.le_refl - apply le_supr - } } - - def solution := (FiniteDataflowProblem num_nodes - (SolverInput γ ρ Γ num_nodes le_supl le_supr)).solve - -end RBMapImpl - - - - - -/- - This section is a test that relies on Mathlib, to be replaced with one - that does not as a TBD. -namespace Test_Preds - def num_nodes := 14 - - instance : ToString (Finset ℕ) where - toString fs := - let _ := LtProp num_nodes - (vector_fn num_nodes (·)).foldl (fun repr nd => - if nd.data ∈ fs then - repr ++ " " ++ toString nd.data - else - repr) "" - - instance {α : Type} [ToString α] : ToString (Option α) where - toString | none => "none" | some a => toString a - - def FSI - : FiniteSolverInput (Finset ℕ) := { - - num_nodes := num_nodes - - edges := fun - | 0 => (· ∈ []) - | 1 => (· ∈ [2]) - | 2 => (· ∈ [3, 4]) - | 3 => (· ∈ [5]) - | 4 => (· ∈ [7, 8]) - | 5 => (· ∈ [6, 9]) - | 6 => (· ∈ [3, 10]) - | 7 => (· ∈ [10]) - | 8 => (· ∈ []) - | 9 => (· ∈ []) - | 10 => (· ∈ [11, ]) - | 11 => (· ∈ [7, 13]) - | 12 => (· ∈ []) - | 13 => (· ∈ []) - | _ => fun _ => false - transitions n := - (insert n ·) - - - - bot := Finset.empty - - - - transitions_sound := by { - unfold BEq.beq instBEqOfDecidableEq - simp - } - le_sound := by { - unfold BEq.beq instBEqOfDecidableEq - simp - intro β₀ β₁ β₂ beq ble - rw [←beq] - assumption - } - le_supl := by simp - le_supr := by simp - } - - def xx := (FiniteDataflowProblem num_nodes FSI).solve.map ((·.1)) - #print xx - #eval! xx -end Test_Preds --/ +end InnerMapImpl From 3ceb81bc770bd21b31781c6fdd46b11bc5c8160a Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Wed, 2 Jul 2025 16:36:46 -0400 Subject: [PATCH 07/22] Add SolutionT output type to InnerMapImpl --- KLR/Compile/Dataflow.lean | 45 ++++++++++++++++++++++++++++++++------- 1 file changed, 37 insertions(+), 8 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 31b685cc..5db0a66a 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -151,6 +151,12 @@ section Basics (∀ a γ₀ b, P a γ₀ → P a (acc b γ₀)) → (∀ a, P a (fold ν acc γ₀)) + -- An instance `HasBot α` fixes a bottom element (`⊥`) of type `α`. + class HasBot (α : Type) where + bot : α + + notation "⊥" => HasBot.bot + notation μ "fold⟪" st "," acc "⟫" => NodeMap.fold μ acc st instance {α β : Type} [ToString α] [ToString β] [NM:NodeMap α] @@ -159,12 +165,13 @@ section Basics str ++ "{" ++ (toString nd.data) ++ ":" ++ (toString (NM.get μ nd)) ++ "}\n") "" + + notation "⟦" α "," β "⟧" => NodeMap.μ α β + infix:90 "◃" => NodeMap.get notation "⟪↦" b "⟫"=> NodeMap.const b - notation "⟦" α "," β "⟧" => NodeMap.μ α β - notation μ "map⟪" f "⟫" => NodeMap.app_unary μ f notation "of_func⟪" f "⟫" => NodeMap.of_func f @@ -237,12 +244,6 @@ section Basics instance (α : Type) [Preorder α] : LE α where le := LE.le - -- An instance `HasBot α` fixes a bottom element (`⊥`) of type `α`. - class HasBot (α : Type) where - bot : α - - notation "⊥" => HasBot.bot - instance {α β : Type} [NodeMap α] [HasBot β] : HasBot ⟦α, β⟧ where bot := NodeMap.const (α:=α) ⊥ @@ -737,6 +738,9 @@ section InnerMapImpl variable (num_nodes num_keys : ℕ) variable (edges : ℕ → ℕ → Bool) variable (transitions : ℕ → ℕ → ρ → ρ) + structure SolutionT where + vals : ℕ → ℕ → ρ + props (n m k : ℕ) : (edges n m) → transitions n k (vals n k) ≤ vals m k def FNM : NodeMap ℕ := (FiniteNodeMap num_keys) @@ -798,4 +802,29 @@ section InnerMapImpl apply le_supr } } + + def Solution : Option (SolutionT ρ edges transitions) := + let _ : NodeMap ℕ := FNM num_keys + let DP : DataflowProblem ℕ ⟦ℕ, ρ⟧ := FiniteDataflowProblem num_nodes + (FSI ρ le_supl le_supr num_nodes edges transitions) + match DP.solve with + | none => none + | some ⟨ν, h⟩ => + let vals n k : ρ := by { + by_cases h : n < num_nodes + { + let nν := ν.get ⟨n, h⟩ + by_cases h : k < num_keys + {exact nν.get ⟨k, h⟩} + exact ⊥ + } + exact ⊥ + } + let props n m k : (edges n m) → transitions n k (vals n k) ≤ vals m k := sorry + some { + vals := vals + props := props + } + + #check Solution end InnerMapImpl From 54116bb30907168fd845e6a478aeaf3421cd9093 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Wed, 2 Jul 2025 19:58:11 -0400 Subject: [PATCH 08/22] Finish InnerMapImpl --- KLR/Compile/Dataflow.lean | 59 +++++++++++++++++++++++++++++---------- 1 file changed, 45 insertions(+), 14 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 5db0a66a..688492e0 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -739,8 +739,9 @@ section InnerMapImpl variable (edges : ℕ → ℕ → Bool) variable (transitions : ℕ → ℕ → ρ → ρ) structure SolutionT where - vals : ℕ → ℕ → ρ - props (n m k : ℕ) : (edges n m) → transitions n k (vals n k) ≤ vals m k + vals (n k : ℕ) : (n < num_nodes) → (k < num_keys) → ρ + props (n m k : ℕ) : (hn : n < num_nodes) → (hm : m < num_nodes) → (hk : k < num_keys) → + (edges n m) → transitions n k (vals n k hn hk) ≤ (vals m k hm hk) def FNM : NodeMap ℕ := (FiniteNodeMap num_keys) @@ -803,24 +804,54 @@ section InnerMapImpl } } - def Solution : Option (SolutionT ρ edges transitions) := - let _ : NodeMap ℕ := FNM num_keys + def Solution : Option (SolutionT ρ num_nodes num_keys edges transitions) := + let NMK : NodeMap ℕ := FNM num_keys let DP : DataflowProblem ℕ ⟦ℕ, ρ⟧ := FiniteDataflowProblem num_nodes (FSI ρ le_supl le_supr num_nodes edges transitions) + let NMN := DP.toNodeMap match DP.solve with | none => none | some ⟨ν, h⟩ => - let vals n k : ρ := by { - by_cases h : n < num_nodes - { - let nν := ν.get ⟨n, h⟩ - by_cases h : k < num_keys - {exact nν.get ⟨k, h⟩} - exact ⊥ - } - exact ⊥ + let vals n k hn hk : ρ := (ν.get ⟨n, hn⟩).get ⟨k, hk⟩ + + let props n m k hn hm hk : (edges n m) → + transitions n k (vals n k hn hk) ≤ vals m k hm hk := by { + unfold I' R' E at h + intro e + let ndn : @Node ℕ NMN.toNodeProp := ⟨n, by { + unfold NodeProp.node_prop NodeMap.toNodeProp NMN DataflowProblem.toNodeMap DP FiniteDataflowProblem FiniteNodeMap FiniteNodeProp + simp + assumption + }⟩ + let ndm : @Node ℕ NMN.toNodeProp := ⟨m, by { + unfold NodeProp.node_prop NodeMap.toNodeProp NMN DataflowProblem.toNodeMap DP FiniteDataflowProblem FiniteNodeMap FiniteNodeProp + simp + assumption + }⟩ + let ndk : @Node ℕ NMK.toNodeProp := @Node.mk ℕ NMK.toNodeProp k (by { + unfold NodeProp.node_prop NodeMap.toNodeProp NMK FNM FiniteNodeMap FiniteNodeProp + simp + assumption + }) + have hε : ε ndn ndm := by { + unfold ε DataflowProblem.σ DP FiniteDataflowProblem FSI nodes vector_fn fin_to_node NodeMap.get FiniteNodeMap node_to_fin Vector.ofFn Vector.get + simp + exists ndm + constructor + exists ⟨m, hm⟩ + constructor + unfold BEq.beq instBEqNode + simp + unfold ndn ndm + simp + assumption + } + have h' := h ndn ndm hε ndk + simp at h' + unfold DataflowProblem.τ DP FiniteDataflowProblem FSI NodeMap.get NodeMap.of_func FiniteNodeMap vector_fn fin_to_node node_to_fin NMK Vector.ofFn Vector.get FNM FiniteNodeMap vector_fn Vector.ofFn node_to_fin fin_to_node Vector.get at h' + simp at h' + apply h' } - let props n m k : (edges n m) → transitions n k (vals n k) ≤ vals m k := sorry some { vals := vals props := props From aa311365335d4ff84ca73e07d95d89f27f5982e4 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Thu, 3 Jul 2025 10:27:23 -0400 Subject: [PATCH 09/22] finish code for impl test??? --- KLR/Compile/Dataflow.lean | 151 +++++++++++++++++++++++++++++++++++++- 1 file changed, 149 insertions(+), 2 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 688492e0..fe84ba67 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -856,6 +856,153 @@ section InnerMapImpl vals := vals props := props } - - #check Solution end InnerMapImpl + +section ConcreteMapImpl + section IsConstImpl + inductive ℂ : Type where + | maybe : ℂ -- key may or may not be set (top val) + | any : ℂ -- key has been set + | some : ℕ → ℂ -- key has been set to (ℕ) + | unreachable : ℂ -- there are no reaching paths that set this key (bot val) + deriving DecidableEq + + notation "𝕄" => ℂ.maybe + notation "𝔸" => ℂ.any + notation "𝕊" => ℂ.some + notation "𝕌" => ℂ.unreachable + + instance : DecidableEq ℂ := by { + unfold DecidableEq + intro a b + by_cases h: (a=b) + apply isTrue; assumption + apply isFalse; assumption + } + + instance : Max ℂ where + max := fun + | 𝕄, _ + | _, 𝕄 => 𝕄 -- properties of merging w top (maybe - 𝕄) (if either branch is 𝕄, merge in 𝕄) + | 𝕌, ℂ₀ + | ℂ₀, 𝕌 => ℂ₀ -- properties of merging w bot (unreachable - 𝕌) (if either branch is 𝕌, other is unaffected) + | 𝕊 a, 𝕊 b => if a = b then 𝕊 a else 𝔸 --two 𝕊 (some) branches either agree, or must be generalized to 𝔸 + |_, _ => 𝔸 -- case where one branch is 𝔸 (any) and the other is 𝕊 (some), merge is 𝔸 + + instance : HasBot ℂ where + bot := 𝕌 + + instance : Preorder ℂ where + le ℂ₀ ℂ₁ := ℂ₁ = ℂ₀ ⊔ ℂ₁ + le_refl := by { + intro ℂ₀ + cases ℂ₀<;> + unfold Max.max instMaxℂ<;> + simp + } + le_trans := by { + unfold Max.max instMaxℂ<;> + intro ℂ₀ ℂ₁ ℂ₂ r₀ r₁<;> + cases ℂ₀<;>cases ℂ₁<;>cases ℂ₂<;> + simp<;>simp at r₀<;>simp at r₁ + { + rename_i n₀ n₁ n₂ + by_cases h₀₁: (n₀ = n₁) = true <;> + simp at h₀₁ <;> + by_cases h₁₂: (n₁ = n₂) = true <;> + simp at h₁₂ <;> + by_cases h₀₂: (n₀ = n₂) = true <;> + simp at h₀₂ <;> + try {split at r₀<;> contradiction} <;> + try {split at r₁<;> contradiction} + {rw [h₀₂]; simp} + {rw [←h₀₁] at h₁₂; contradiction} + } + } + + instance : DecidableLE ℂ := by { + intro ℂ₀ ℂ₁ + unfold LE.le instLEOfPreorder Preorder.toLE instPreorderℂ + simp + by_cases h : (ℂ₁ = ℂ₀⊔ℂ₁) + apply isTrue; assumption + apply isFalse; assumption + } + + #synth DecidableEq ℂ + #synth Preorder ℂ + #synth DecidableLE ℂ + #synth Max ℂ + #synth HasBot ℂ + + theorem le_supl: ∀ ℂ₀ ℂ₁ : ℂ, ℂ₀ ≤ ℂ₀ ⊔ ℂ₁ := by { + intro ℂ₀ ℂ₁ + unfold LE.le instLEOfPreorder Preorder.toLE instPreorderℂ Max.max instMaxℂ + simp + cases ℂ₀ <;> cases ℂ₁ <;> simp + split <;> simp + } + theorem le_supr : ∀ ℂ₀ ℂ₁ : ℂ, ℂ₁ ≤ ℂ₀ ⊔ ℂ₁ := by { + intro ℂ₀ ℂ₁ + unfold LE.le instLEOfPreorder Preorder.toLE instPreorderℂ Max.max instMaxℂ + simp + cases h₀ : ℂ₀ <;> cases h₁ : ℂ₁ <;> simp + split <;> simp + { + rename_i n₀ n₁ eq + rw [eq] + simp + } + } + end IsConstImpl + + def num_nodes : ℕ := 17 + def num_keys : ℕ := 2 + + def edges : ℕ → ℕ → Bool := fun + | 0, 1 + | 0, 2 + | 1, 3 + | 2, 4 + | 2, 5 + | 2, 6 + | 3, 7 + | 4, 3 + | 4, 8 + | 5, 9 + | 6, 10 + | 7, 1 + | 7, 11 + | 8, 12 + | 9, 13 + | 10, 13 + | 11, 15 + | 12, 14 + | 13, 14 + | 14, 16 + | 15, 16 => true + | _, _ => false + + def transitions : ℕ → ℕ → ℂ → ℂ := fun + | 2, 0, _ => ℂ.some 5 + | 2, 1, _ => ℂ.some 2 + | 5, 0, _ => ℂ.some 1 + | 6, 0, _ => ℂ.some 1 + | 7, 1, _ => ℂ.some 4 + | 8, 0, _ => ℂ.some 3 + | 11, 0, _ => ℂ.some 9 + | 14, 0, _ => ℂ.some 7 + | _, _, ℂ₀ => ℂ₀ + + + def X := Solution + (ρ:=ℂ) + (le_supl:=le_supl) + (le_supr:=le_supr) + (num_nodes:=num_nodes) + (num_keys:=num_keys) + (edges:=edges) + (transitions:=transitions) + + #eval! (match X with | some _ => "some" | none => "none") +end ConcreteMapImpl From 76bd1c7c00bfbd95a9fa24dd3b689e4f3539c2f1 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Thu, 3 Jul 2025 13:40:17 -0400 Subject: [PATCH 10/22] Get ToString working for solutions! --- KLR/Compile/Dataflow.lean | 62 +++++++++++++++++++++++++++++++++++---- 1 file changed, 56 insertions(+), 6 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index fe84ba67..6357b74e 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -738,11 +738,31 @@ section InnerMapImpl variable (num_nodes num_keys : ℕ) variable (edges : ℕ → ℕ → Bool) variable (transitions : ℕ → ℕ → ρ → ρ) - structure SolutionT where - vals (n k : ℕ) : (n < num_nodes) → (k < num_keys) → ρ - props (n m k : ℕ) : (hn : n < num_nodes) → (hm : m < num_nodes) → (hk : k < num_keys) → - (edges n m) → transitions n k (vals n k hn hk) ≤ (vals m k hm hk) + section SolutionImpl + structure SolutionT where + vals (n k : ℕ) : (n < num_nodes) → (k < num_keys) → ρ + props (n m k : ℕ) : (hn : n < num_nodes) → (hm : m < num_nodes) → (hk : k < num_keys) → + (edges n m) → transitions n k (vals n k hn hk) ≤ (vals m k hm hk) + + def SolutionT.toString [ToString ρ] + (𝕊 : SolutionT ρ num_nodes num_keys edges transitions) + : String := + let 𝕍 := 𝕊.vals + let nd_to_string n (hn :n < num_nodes) : String := + let entries := (List.range num_keys).filterMap + (fun k => if hk: k < num_keys then some (ToString.toString (𝕍 n k hn hk)) else none) + String.intercalate " " entries + let lines := (List.range num_nodes).filterMap + (fun n => if hn: n < num_nodes then ( + let s := nd_to_string n hn; some (s!"Node {n}: {s}") + ) else none) + String.intercalate "\n" ([""] ++ lines ++ [""]) + + instance [ToString ρ] : ToString (SolutionT ρ num_nodes num_keys edges transitions) where + toString := (SolutionT.toString ρ num_nodes num_keys edges transitions) + + end SolutionImpl def FNM : NodeMap ℕ := (FiniteNodeMap num_keys) def FSI {_:NodeMap ℕ}: FiniteSolverInput (⟦ℕ, ρ⟧) := { @@ -872,6 +892,13 @@ section ConcreteMapImpl notation "𝕊" => ℂ.some notation "𝕌" => ℂ.unreachable + instance : ToString ℂ where + toString := fun + | 𝕄 => "𝕄" + | 𝔸 => "𝔸" + | 𝕊 n => s!"𝕊 {n}" + | 𝕌 => "𝕌" + instance : DecidableEq ℂ := by { unfold DecidableEq intro a b @@ -995,7 +1022,7 @@ section ConcreteMapImpl | _, _, ℂ₀ => ℂ₀ - def X := Solution + def 𝕏 := Solution (ρ:=ℂ) (le_supl:=le_supl) (le_supr:=le_supr) @@ -1004,5 +1031,28 @@ section ConcreteMapImpl (edges:=edges) (transitions:=transitions) - #eval! (match X with | some _ => "some" | none => "none") + #eval 𝕏 + /- Output: + + (some ( + Node 0: 𝕌 𝕌 + Node 1: 𝕊 5 𝕊 4 + Node 2: 𝕌 𝕌 + Node 3: 𝕊 5 𝔸 + Node 4: 𝕊 5 𝕊 2 + Node 5: 𝕊 5 𝕊 2 + Node 6: 𝕊 5 𝕊 2 + Node 7: 𝕊 5 𝔸 + Node 8: 𝕊 5 𝕊 2 + Node 9: 𝕊 1 𝕊 2 + Node 10: 𝕊 1 𝕊 2 + Node 11: 𝕊 5 𝕊 4 + Node 12: 𝕊 3 𝕊 2 + Node 13: 𝕊 1 𝕊 2 + Node 14: 𝔸 𝕊 2 + Node 15: 𝕊 9 𝕊 4 + Node 16: 𝔸 𝔸 + )) + + -/ end ConcreteMapImpl From d0ffd969bdd988c67f8fc6e001d04dbefbacb624 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Thu, 3 Jul 2025 20:06:35 -0400 Subject: [PATCH 11/22] minor tweaks --- KLR/Compile/Dataflow.lean | 33 +++++++++++++++++++-------------- 1 file changed, 19 insertions(+), 14 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 6357b74e..27130bd5 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -881,10 +881,10 @@ end InnerMapImpl section ConcreteMapImpl section IsConstImpl inductive ℂ : Type where - | maybe : ℂ -- key may or may not be set (top val) - | any : ℂ -- key has been set - | some : ℕ → ℂ -- key has been set to (ℕ) - | unreachable : ℂ -- there are no reaching paths that set this key (bot val) + | maybe : ℂ -- key at pos may or may not be set (top val) + | any : ℂ -- key at pos is set + | some : ℕ → ℂ -- key at pos is set to (ℕ) + | unreachable : ℂ -- false - key as pos is unreachable deriving DecidableEq notation "𝕄" => ℂ.maybe @@ -983,7 +983,7 @@ section ConcreteMapImpl } end IsConstImpl - def num_nodes : ℕ := 17 + def num_nodes : ℕ := 20 def num_keys : ℕ := 2 def edges : ℕ → ℕ → Bool := fun @@ -1007,10 +1007,13 @@ section ConcreteMapImpl | 12, 14 | 13, 14 | 14, 16 - | 15, 16 => true + | 15, 16 + | 17, 18 + | 18, 19 => true | _, _ => false def transitions : ℕ → ℕ → ℂ → ℂ := fun + | 0, _, _ => 𝕄 | 2, 0, _ => ℂ.some 5 | 2, 1, _ => ℂ.some 2 | 5, 0, _ => ℂ.some 1 @@ -1021,7 +1024,6 @@ section ConcreteMapImpl | 14, 0, _ => ℂ.some 7 | _, _, ℂ₀ => ℂ₀ - def 𝕏 := Solution (ρ:=ℂ) (le_supl:=le_supl) @@ -1032,26 +1034,29 @@ section ConcreteMapImpl (transitions:=transitions) #eval 𝕏 - /- Output: + /- Output: (i looked at it by hand and it looks right 😊) - (some ( + some ( Node 0: 𝕌 𝕌 - Node 1: 𝕊 5 𝕊 4 - Node 2: 𝕌 𝕌 - Node 3: 𝕊 5 𝔸 + Node 1: 𝕄 𝕄 + Node 2: 𝕄 𝕄 + Node 3: 𝕄 𝕄 Node 4: 𝕊 5 𝕊 2 Node 5: 𝕊 5 𝕊 2 Node 6: 𝕊 5 𝕊 2 - Node 7: 𝕊 5 𝔸 + Node 7: 𝕄 𝕄 Node 8: 𝕊 5 𝕊 2 Node 9: 𝕊 1 𝕊 2 Node 10: 𝕊 1 𝕊 2 - Node 11: 𝕊 5 𝕊 4 + Node 11: 𝕄 𝕊 4 Node 12: 𝕊 3 𝕊 2 Node 13: 𝕊 1 𝕊 2 Node 14: 𝔸 𝕊 2 Node 15: 𝕊 9 𝕊 4 Node 16: 𝔸 𝔸 + Node 17: 𝕌 𝕌 + Node 18: 𝕌 𝕌 + Node 19: 𝕌 𝕌 )) -/ From f081b716fdb62e22c1138698c5fa404d183ab594 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Thu, 3 Jul 2025 20:32:33 -0400 Subject: [PATCH 12/22] add more comments --- KLR/Compile/Dataflow.lean | 48 ++++++++++++++++++++++++++++++++++++--- 1 file changed, 45 insertions(+), 3 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 27130bd5..77a57aee 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -545,14 +545,14 @@ end DataflowProblemSolver /- The section `FiniteDataflowProblemSolver` provides a structure type definition - `FiniteSolverInput β`, that can be easily instantiated with any graph over + `FiniteSolverInput β`, that can be instantiated with any graph over `num_nodes : ℕ` nodes, with data of type `β`, as long as the edge relation and transition functions can be described by numbered node index. To fully instantiate a `FiniteSolverInput`, 4 simple soundness theorems relating largely the relations on `β` must be proved. `FiniteDataflowProblem ... FiniteSolverInput β → DataflowProblem ℕ β` is the key function, lifting a `FiniteSolverInput` to `DataflowProblem` admitting the - solver function `sound`. + solver function `DataflowProblem.solve`. -/ section FiniteDataflowProblemSolver @@ -727,9 +727,51 @@ section FiniteDataflowProblemSolver {apply FSI.le_supr} } } +end FiniteDataflowProblemSolver /- - description TBD + The section `InnerMapImpl` provides a further reification of the + `DataflowProblem`-generating pipeline built above. In particular, + It makes instantiating `FiniteSolverInput β` easy for datatypes `β` + that represent maps themselves from a finite set of keys to values. + + Motivation: + + To instantiate the above `FiniteSolverInput β` for types `β`, that have + boolean equality (`BEq β`), a compatible ordering relation + (`Preorder β`), a supremum wrt ord `Max β`), a bottom element wrt ord + (`HasBot β`), and appropriate congruences under equality, is easy. + + For example: `FiniteSolverInput ℕ` or even `List ℕ` or other structures + with sufficiently many library typeclass instances. + + However, for many dataflow analysis cases, the right datatype `β` is + itself a map type. for example `⟦ℕ, γ⟧` for an innter datatype `γ`. + `ℕ` here is chosen to accomodate mappings over any finite, numbered + set of keys. `γ` must provide all the structure requires of `β` itself, + however, it will ideally be a simple enough type that this is immediate. + Finite types will often suffice for `γ` (e.g. `Bool` for use/free), and + in other cases shallow inductive types like the `ℂ` for constancy of a + value (set to n:ℕ, set to some value, unknown). + mappings `β := ⟦ℕ, γ⟧` represents assignments of each of the `num_keys` + keys (e.g., variable names, mem locs, other identifiers) to data `γ`. + + To complete the `DataflowProblem` instance, the edge relation `edges` + must be provided, and the transitions `τ := transitions n k`. Here + `τ` is the transition function at node `n < num_nodes`, as it acts + on key `k < num_keys`. Notably, the "whole node" functions `⟦ℕ, γ⟧ → ⟦ℕ, γ⟧` + that can be derived by thus specifying the transitions are only those + that factor into components that each act on a single key. This is a + restriction of `InnerMapImpl`. + + `InnerMapImpl.SolutionT` is a type that provides a final assignment + of nodes to data `β`, and of indexed props establishing the + satisfaction of the dataflow constraints by these data. + + `InnerMapImpl.Solution` returns a `Option (SolutionT ...)`. This + represents the success vs timeout case. + + That's how this thing works! 💕 -/ section InnerMapImpl variable (ρ : Type) [DecidableEq ρ] [Preorder ρ] [DecidableLE ρ] [Max ρ] [HasBot ρ] From c6379f0055317e1806a223375d515c1a0c4b1969 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Thu, 3 Jul 2025 21:17:35 -0400 Subject: [PATCH 13/22] more comments --- KLR/Compile/Dataflow.lean | 62 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 77a57aee..8326817d 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -68,6 +68,9 @@ def FiniteDataflowProblem {β : Type} ... `DataflowProblem.solve` may then be called on this instance. +## Concrete example : constant propagation + + ## Code by `Section` `Section Basics`- defines basic `Node`, `NodeProp`, and `NodeMap `definitions. @@ -83,6 +86,8 @@ def FiniteDataflowProblem {β : Type} ... to a `DataflowProblem`. `Section InnerMapImpl` - description TBD + +`Section ConcreteMapImpl` - description TBD -/ import Lean.Data.RBMap @@ -680,6 +685,11 @@ section FiniteDataflowProblemSolver } } + /- + This takes a defined `FiniteSolverInpu β` and generates a `DataflowProblem ℕ β`. + This is the end of the section because the returned instance provides the + `DataflowProblem.solve` function. + -/ def FiniteDataflowProblem {β : Type} [BEq β] [P:Preorder β] @@ -781,6 +791,13 @@ section InnerMapImpl variable (edges : ℕ → ℕ → Bool) variable (transitions : ℕ → ℕ → ρ → ρ) + /- + `SolutionT` captures the type of information returned by this section's + computqtions to the caller. namely, it forgets internal data representation + and offers all indexing by raw `(ℕ → ⬝). + + It is returned by `Solution` below + -/ section SolutionImpl structure SolutionT where vals (n k : ℕ) : (n < num_nodes) → (k < num_keys) → ρ @@ -805,8 +822,43 @@ section InnerMapImpl toString := (SolutionT.toString ρ num_nodes num_keys edges transitions) end SolutionImpl + + /- + This is the `NodeMap ℕ` instance for INNER maps over num_keys + Outer maps over num_nodes have a separate `NodeMap ℕ` instance. + This is because these provide different types `Node ℕ`; both + are finite types, but of different size. + + confusion over this duality is resolved where necessary by + providing identifiers to contextual instances, as opposed + to relying on inference at the signature level. + + For example, FNM below captures the INNER map types, whereas + the outer type is inferred without its invocation. Later, + `Solution` binds identifiers (`NMN` and `NMK`) to each of the + (`n`-indexed and `k`-indexed) `NodeMap ℕ` instances. + + Later in `Solution`, nodes `Node ℕ` corresponding to indices + of each of the inner and outer maps are needed, and are obtained: + `ndk : @Node ℕ NMK.toNodeProp := @Node.mk ℕ NMK.toNodeProp k` + `ndn : @Node ℕ NMN.toNodeProp := @Node.mk ℕ NMN.toNodeProp n` + + Though dealing with dual instances of `NodeMap ℕ` is cumbersome, + it allows significant code reuse and defines dataflowproblems + with `β` equal to a map type minimally. + -/ def FNM : NodeMap ℕ := (FiniteNodeMap num_keys) + /- + Defining a `FiniteSolverInput ⟦ℕ, ρ⟧` requires + tweaking the `transitions` function to index on + `Node ℕ`s instead of `ℕ`s, and proving a small + handful of compatibility lemmas. They ultimately + rely on sufficient corresponding properties of + `ρ` through unrollings also dependent on above- + proven properties of `⟦⬝, ⬝⟧` types. None are + very surprising. + -/ def FSI {_:NodeMap ℕ}: FiniteSolverInput (⟦ℕ, ρ⟧) := { num_nodes := num_nodes edges := edges @@ -866,6 +918,16 @@ section InnerMapImpl } } + /- + `Solution` mainly functions to take the `FSI : FiniteSolverInput ⟦ℕ, ρ⟧` + from above, use `FiniteDataflowProblem` from above to construct a + `DataflowProblem ℕ ⟦ℕ, ρ⟧` (internally represented by a `⟦ℕ, ⟦ℕ, ρ⟧⟧` instance), + and map under the resultant `Option ((ν : ⟦ℕ, ⟦ℕ, ρ⟧⟧) ×' I' ν)` a transformation + to the `InnerMapImpl.SolutionT` type. This mapping requires folding + and unfolding many conversions between raw `ℕ` indices, and proof-carrying + `Node ℕ` instances (of each `NodeMap ℕ` class!). None of these proofs + are surprising. + -/ def Solution : Option (SolutionT ρ num_nodes num_keys edges transitions) := let NMK : NodeMap ℕ := FNM num_keys let DP : DataflowProblem ℕ ⟦ℕ, ρ⟧ := FiniteDataflowProblem num_nodes From 0a30d4c0ff0aa3b59db39b2212e24cb4c474b041 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Thu, 3 Jul 2025 21:53:31 -0400 Subject: [PATCH 14/22] Add final comments (for now) --- KLR/Compile/Dataflow.lean | 251 ++++++++++++++++++++++++++------------ 1 file changed, 170 insertions(+), 81 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 8326817d..953547a9 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -70,6 +70,7 @@ def FiniteDataflowProblem {β : Type} ... ## Concrete example : constant propagation +See comment on section `ConcreteMapImpl` below. ## Code by `Section` @@ -81,13 +82,19 @@ def FiniteDataflowProblem {β : Type} ... to dataflow problems. `Section FiniteDataflowProblemSolver` - simplies the process of constructing - `DataflowProblem`s by proviing the `FiniteSolverInput` class that uses + `DataflowProblem`s by providing the `FiniteSolverInput` class that uses `ℕ` indexing for nodes, and can be transformed by `FiniteDataflowProblem` to a `DataflowProblem`. -`Section InnerMapImpl` - description TBD +`Section InnerMapImpl` - Provides functions to construct `DataflowProblem ℕ β`s + from `β` that are themselves map types (`⟦⬝, ⬝⟧`). Also provides a solution + type `SolutionT` that is more usable to the caller by omitting reliance on + proof-carrying `Node ℕ` indices. -`Section ConcreteMapImpl` - description TBD +`Section ConcreteMapImpl` - Defines a datatype `ℂ` representing knowledge of + constancy, and initializes a `DataflowProblem ℕ ⟦ℕ, ℂ⟧` using the `InnerMapImpl` + utilities above. initialized with a concrete graph and transition funcset, + the solver is called - exercising the pipeline end-to-end. -/ import Lean.Data.RBMap @@ -295,7 +302,7 @@ end Basics /- - The section `DataflowProblemSolver ` is paramterized on an instance of `DataflowProblem α β`. + The section `DataflowProblemSolver ` is parameterized on an instance of `DataflowProblem α β`. It builds on the definitions of maps `⟦α, β⟧` from `NodeMap α`, and on the transition functions `τ ◃ a` and succesor lists `σ ◃ a` for each node `a : Node α` (`◃` used as notation for map get) provided by the `DataflowProblem` to compute a series of utility values, functions, and soundness @@ -981,8 +988,65 @@ section InnerMapImpl props := props } end InnerMapImpl - +/- + The section `ConcreteMapImpl` serves to illustrate an end-to-end usage + of the dataflow solver defined above. In particular: + + `ConcreteMapImpl` defines a datatype `ℂ` representing knowledge of + the constancy of a variable `k` at a location (i.e. what can be said about the + value of the variable in any program trace that reaches that program point): + | `𝕄` - "maybe"/⊤ - `k` may or may not be defined + | `𝔸` - "any" - `k` is defined + | `𝕊 (n : ℕ)` - "some `n`" - `k = n` + | `𝕌` - "unreachable" - this program point is not reachable. + A bundle of class instances are proven to give `ℂ` + necessary type-level structure. The interesting part of each: + `[ToString ℂ]` - trivial + `[DecidableEq ℂ]` - trivial + `[Max ℂ]` - this defines our lattice structure! + morally, values `ρ₀⊔ρ₁` here should always + represent the right entry to a block + given that its predecessors exits are + `ρ₀` and `ρ₁`. if you come up with a relation + that lacks associativity, everything here + will technically work but using the returned + proofs of dataflow constraint satisfaction + will be very difficult. + `[HasBot ℂ]` - choose a `⊥` for the `β`-lattice. theoretically, + this should satisfy `⊥ ≤ ⬝` (i.e. `⊥⊔ρ₀ = ρ₀⊔⊥ = ρ₀), + but the solver can still be run with an alternate value. + the tradeoff is that the returned fixpoint may not be + minimal. But this may be useful in some cases. + `[Preorder ℂ]` - This formally defines `ℂ₀ ≤ ℂ₁ := ℂ₁ = ℂ₀ ⊔ ℂ₁`. + This is a canonical definition. completing the + `Preorder` requires proving reflexivity and + transitivity. Since `ℂ` is a finite type, + these just come down to case matching and bookkeeping. + `[DecidableLE ℂ]` - trivial + `{le_supl} {le_supr}` - these establish compatability for the `≤` and `⊔` + instances provided above. Notably, these + compatabilities were the definition of `≤`, + so the proof reduces to unfolding. + + With this `ℂ` plus algebraic structure in hand, we need only to + concretely choose our graph and transitions to obtain all arguments + to `InnerMapImpl.Solution`. + + Details of constructing this graph are provided below, but it is easy + to see that there is little to no boilerplate in the definitions of + `num_nodes`, `num_keys`, `edges` and `transitions`. + + Fully instantiating our instances allows the `𝕏` below to be a + parameter-free `InnerMapImpl.SolutionT` type (which luckily + has a ToString instance defined in section). + + wooo!!! 🎉 +-/ section ConcreteMapImpl + /- + Section `IsConstImpl` defines the "constancy type" `ℂ`, and all + needed structure on `ℂ` to eventually construct a `DataflowProblem ℕ ⟦ℕ, ℂ⟧`. + -/ section IsConstImpl inductive ℂ : Type where | maybe : ℂ -- key at pos may or may not be set (top val) @@ -1000,7 +1064,7 @@ section ConcreteMapImpl toString := fun | 𝕄 => "𝕄" | 𝔸 => "𝔸" - | 𝕊 n => s!"𝕊 {n}" + | 𝕊 n => s!"(𝕊 {n})" | 𝕌 => "𝕌" instance : DecidableEq ℂ := by { @@ -1087,81 +1151,106 @@ section ConcreteMapImpl } end IsConstImpl - def num_nodes : ℕ := 20 - def num_keys : ℕ := 2 - - def edges : ℕ → ℕ → Bool := fun - | 0, 1 - | 0, 2 - | 1, 3 - | 2, 4 - | 2, 5 - | 2, 6 - | 3, 7 - | 4, 3 - | 4, 8 - | 5, 9 - | 6, 10 - | 7, 1 - | 7, 11 - | 8, 12 - | 9, 13 - | 10, 13 - | 11, 15 - | 12, 14 - | 13, 14 - | 14, 16 - | 15, 16 - | 17, 18 - | 18, 19 => true - | _, _ => false - - def transitions : ℕ → ℕ → ℂ → ℂ := fun - | 0, _, _ => 𝕄 - | 2, 0, _ => ℂ.some 5 - | 2, 1, _ => ℂ.some 2 - | 5, 0, _ => ℂ.some 1 - | 6, 0, _ => ℂ.some 1 - | 7, 1, _ => ℂ.some 4 - | 8, 0, _ => ℂ.some 3 - | 11, 0, _ => ℂ.some 9 - | 14, 0, _ => ℂ.some 7 - | _, _, ℂ₀ => ℂ₀ - - def 𝕏 := Solution - (ρ:=ℂ) - (le_supl:=le_supl) - (le_supr:=le_supr) - (num_nodes:=num_nodes) - (num_keys:=num_keys) - (edges:=edges) - (transitions:=transitions) - - #eval 𝕏 - /- Output: (i looked at it by hand and it looks right 😊) - - some ( - Node 0: 𝕌 𝕌 - Node 1: 𝕄 𝕄 - Node 2: 𝕄 𝕄 - Node 3: 𝕄 𝕄 - Node 4: 𝕊 5 𝕊 2 - Node 5: 𝕊 5 𝕊 2 - Node 6: 𝕊 5 𝕊 2 - Node 7: 𝕄 𝕄 - Node 8: 𝕊 5 𝕊 2 - Node 9: 𝕊 1 𝕊 2 - Node 10: 𝕊 1 𝕊 2 - Node 11: 𝕄 𝕊 4 - Node 12: 𝕊 3 𝕊 2 - Node 13: 𝕊 1 𝕊 2 - Node 14: 𝔸 𝕊 2 - Node 15: 𝕊 9 𝕊 4 - Node 16: 𝔸 𝔸 - Node 17: 𝕌 𝕌 - Node 18: 𝕌 𝕌 - Node 19: 𝕌 𝕌 - )) + /- + Section `GraphImpl` specifies the topology and transitions + of the graph that will be fed to `InnerMapImpl.Solution` + (and within that, `DataflowProblem`). + + `num_nodes : ℕ` is the number of nodes in the graph + `num_keys : ℕ` is the number of keys in our dataflow values `β := ⟦ℕ, ℂ⟧` + here, it corresponds to the number of variables being tracked (2) + `edges : ℕ → ℕ → Bool` defines the edge relation. entering in a relation + from hand/head/mind requires minimal effort. + `transitions : (n : ℕ) → (k : ℕ) → ℂ → ℂ` defines how inner dataflow values `ℂ` are + transformed at node `n` and key `k`. As noted in the `section InnerMapImpl` comment, + `ℕ → ℕ → ℂ → ℂ` does not generate all `⟦ℕ, ℂ⟧ → ⟦ℕ, ℂ⟧`, but even under the + restriction (outlined above), many common problems are expressable + -/ + section GraphImpl + def num_nodes : ℕ := 20 + def num_keys : ℕ := 2 + + def edges : ℕ → ℕ → Bool := fun + | 0, 1 + | 0, 2 + | 1, 3 + | 2, 4 + | 2, 5 + | 2, 6 + | 3, 7 + | 4, 3 + | 4, 8 + | 5, 9 + | 6, 10 + | 7, 1 + | 7, 11 + | 8, 12 + | 9, 13 + | 10, 13 + | 11, 15 + | 12, 14 + | 13, 14 + | 14, 16 + | 15, 16 + | 17, 18 + | 18, 19 => true + | _, _ => false + + def transitions : ℕ → ℕ → ℂ → ℂ := fun + | 0, _, _ => 𝕄 + | 2, 0, _ => ℂ.some 5 + | 2, 1, _ => ℂ.some 2 + | 5, 0, _ => ℂ.some 1 + | 6, 0, _ => ℂ.some 1 + | 7, 1, _ => ℂ.some 4 + | 8, 0, _ => ℂ.some 3 + | 11, 0, _ => ℂ.some 9 + | 14, 0, _ => ℂ.some 7 + | _, _, ℂ₀ => ℂ₀ + end GraphImpl + /- + Given all above instantiations, `InnerMapImpl.Solution` is finally + called and a solution value `𝕏` can be defined parameter-free. 🥳 -/ + section ConcreteSolution + def 𝕏 := Solution + (ρ:=ℂ) + (le_supl:=le_supl) + (le_supr:=le_supr) + (num_nodes:=num_nodes) + (num_keys:=num_keys) + (edges:=edges) + (transitions:=transitions) + + #eval 𝕏 + /- Output: (i looked at it by hand and it looks right 😊) + + some ( + Node 0: 𝕌 𝕌 + Node 1: 𝕄 𝕄 + Node 2: 𝕄 𝕄 + Node 3: 𝕄 𝕄 + Node 4: (𝕊 5) (𝕊 2) + Node 5: (𝕊 5) (𝕊 2) + Node 6: (𝕊 5) (𝕊 2) + Node 7: 𝕄 𝕄 + Node 8: (𝕊 5) (𝕊 2) + Node 9: (𝕊 1) (𝕊 2) + Node 10: (𝕊 1) (𝕊 2) + Node 11: 𝕄 (𝕊 4) + Node 12: (𝕊 3) (𝕊 2) + Node 13: (𝕊 1) (𝕊 2) + Node 14: 𝔸 (𝕊 2) + Node 15: (𝕊 9) (𝕊 4) + Node 16: 𝔸 𝔸 + Node 17: 𝕌 𝕌 + Node 18: 𝕌 𝕌 + Node 19: 𝕌 𝕌 + )) + + -/ + end ConcreteSolution end ConcreteMapImpl + +-- thanks for reading! - Julia 💕 From 6d2c0f62261f970d9620fc54ad58bf519ed22846 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Thu, 3 Jul 2025 22:09:07 -0400 Subject: [PATCH 15/22] remove unnecessary import --- KLR/Compile/Dataflow.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 953547a9..0850f6c8 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -96,8 +96,8 @@ See comment on section `ConcreteMapImpl` below. utilities above. initialized with a concrete graph and transition funcset, the solver is called - exercising the pipeline end-to-end. -/ -import Lean.Data.RBMap +-- sigh i shouldn't have to do this abbrev ℕ := Nat /- From c1607cf683dca0ff0381b5f19c2038941224e225 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Thu, 3 Jul 2025 22:12:16 -0400 Subject: [PATCH 16/22] nits --- KLR/Compile/Dataflow.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 0850f6c8..a0984e3f 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -1006,14 +1006,14 @@ end InnerMapImpl `[Max ℂ]` - this defines our lattice structure! morally, values `ρ₀⊔ρ₁` here should always represent the right entry to a block - given that its predecessors exits are + given that its predecessors' exits are `ρ₀` and `ρ₁`. if you come up with a relation that lacks associativity, everything here will technically work but using the returned proofs of dataflow constraint satisfaction will be very difficult. `[HasBot ℂ]` - choose a `⊥` for the `β`-lattice. theoretically, - this should satisfy `⊥ ≤ ⬝` (i.e. `⊥⊔ρ₀ = ρ₀⊔⊥ = ρ₀), + this should satisfy `⊥ ≤ ⬝` (i.e. `⊥⊔ρ₀ = ρ₀⊔⊥ = ρ₀`), but the solver can still be run with an alternate value. the tradeoff is that the returned fixpoint may not be minimal. But this may be useful in some cases. From 163eb770bbd144d9723cbe9ce2af3a7f256cd32e Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Thu, 3 Jul 2025 23:09:58 -0400 Subject: [PATCH 17/22] add speculation on modularity --- KLR/Compile/Dataflow.lean | 74 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 74 insertions(+) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index a0984e3f..1c02e941 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -1248,7 +1248,81 @@ section ConcreteMapImpl Node 18: 𝕌 𝕌 Node 19: 𝕌 𝕌 )) + -/ + /-====================================================== + HEY THIS IS IMPORTANT: + + SPECULATION ON USAGE OF `(𝕏 : SolutionT).props` OUTPUT VALUE + IN LARGER PROOFS + + ====================================================== + + of course, the point of this dataflow solver as a modular + component is to return not just the solution `ν` but propositional + satisfaction of the dataflow inequalities by the `ν`. + + The propositional components of `𝕏 : SolutionT` establish + that for any edge from nodes `n` to `m` `τ ν[n] ≤ ν[m]`. + + How is this useful? + + Call `β := ⟦ℕ, ℂ⟧` our abstract domain. + The instance definition provides transitions `τ : ℕ → β → β`. + + Choose a "concrete domain" `α` + with a "stepping relation" for each node `σ : ℕ → α → α`, + and a "simulation relation" `α₀ ∼ β₀ : Prop` + satisfying `∀ n, α₀ ∼ β₀ → (σₙ α₀) ∼ (τₙ β₀)` + and `β₀ ≤ β₁ → α₀ ∼ β₀ → α₀ ∼ β₁` + and `β₀ == β₁ → α₀ ∼ β₀ → α₀ ∼ β₁`. + + We must also choose a `⊥{α}` for `α`, + (corresponding to value at program entry) + that relates to the `⊥{β}` for `β` + satisfying `⊥{α} ∼ ⊥{β}`. + + For our above example, we can choose `α := ⟦ℕ, Option ℕ⟧` + (concrete program states) + and `α₀ ∼ β₀` lifting from a corresponding canonical + `(_:Option ℕ) ∼ (_:ℂ)` relation (e.g. `some n ∼ 𝕊 n`) + Once the associated properties are proven... + + We can now define "program states" `π := (α₀ : α) × (n : ℕ)` (interpreted + as the statement "execution has state `α` at entry to block `n`. + + We can now define "program stepping": + `π₀ ⊑ π₁ := (edge π₀.n π₁.n) ∧ (n:=π₀.n; τₙ) π₀.α₀ = π₁.α₀` + + We can now define a type for "paths" `ℓ` as a list of + `N` `α × ℕ` entries (corresponding to program states at unit times) + where `ℓ[0] = (⊥{α}, 0)` + (assuming 0 is the "entry block"), + and `∀ n < N - 1, l[n] ⊑ l[n+1]` (successive entries constitute valid steps) + + Now if `ν := 𝕏.vals` is a dataflow solution, + and `ℓₙ := (n, _) := ℓ; n` + and `ℓₐ := (_, α₀) := ℓ; α₀` + it is provable inductively from `𝕏.props` that: + `∀ ℓ, ℓₐ ∼ ν[ℓₙ]`. + + In the case of our concrete example, this means that we can prove + that any program state `αₙ` at node `n` reached through stepping + from the entry state is constrained by + `αₙ ∼ βₙ` for the abstract state `βₙ := ν[n]`. + For various values of `αₙ` and `βₙ`, + this could mean (for all keys `k`), + + `αₙ ∼ 𝕄` : no information + `αₙ ∼ 𝔸` : `k` is defined + `αₙ ∼ 𝕊 m` : `k` is defined and equal to `m` + `αₙ ∼ 𝕌` : impossible (which implies that `∄ ℓ, ℓₐ ∼ 𝕌)`, + i.e., no node `n` satisfying `ν[n] = 𝕌` will + ever be reached by a path + + These are powerful results, for which much + thought has gone into generating and + presenting conveniently. -/ end ConcreteSolution end ConcreteMapImpl From 6ab84e234629b6b107b19ef2843df38585d705ba Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Thu, 3 Jul 2025 23:18:56 -0400 Subject: [PATCH 18/22] tweak speculation section --- KLR/Compile/Dataflow.lean | 50 ++++++++++++++++++++++++--------------- 1 file changed, 31 insertions(+), 19 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 1c02e941..ce7c6a76 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -1251,6 +1251,7 @@ section ConcreteMapImpl -/ /-====================================================== + HEY THIS IS IMPORTANT: SPECULATION ON USAGE OF `(𝕏 : SolutionT).props` OUTPUT VALUE @@ -1258,7 +1259,13 @@ section ConcreteMapImpl ====================================================== - of course, the point of this dataflow solver as a modular + In particular... + + Reasoning about execution traces by bisimulation to the dataflow type! + + ====================================================== + + Of course, the point of this dataflow solver as a modular component is to return not just the solution `ν` but propositional satisfaction of the dataflow inequalities by the `ν`. @@ -1281,11 +1288,15 @@ section ConcreteMapImpl (corresponding to value at program entry) that relates to the `⊥{β}` for `β` satisfying `⊥{α} ∼ ⊥{β}`. + (but note that `α` need not have any lattice + structure for the bisimulation to be established) For our above example, we can choose `α := ⟦ℕ, Option ℕ⟧` (concrete program states) - and `α₀ ∼ β₀` lifting from a corresponding canonical - `(_:Option ℕ) ∼ (_:ℂ)` relation (e.g. `some n ∼ 𝕊 n`) + and `α₀ ∼ β₀` + `α₀` is the concrete/runtime time "refining" `β₀` + (lifted from a corresponding canonical refinement + `(_:Option ℕ) ∼ (_:ℂ)` relation (e.g. `some n ∼ 𝕊 n`)) Once the associated properties are proven... We can now define "program states" `π := (α₀ : α) × (n : ℕ)` (interpreted @@ -1294,35 +1305,36 @@ section ConcreteMapImpl We can now define "program stepping": `π₀ ⊑ π₁ := (edge π₀.n π₁.n) ∧ (n:=π₀.n; τₙ) π₀.α₀ = π₁.α₀` - We can now define a type for "paths" `ℓ` as a list of - `N` `α × ℕ` entries (corresponding to program states at unit times) - where `ℓ[0] = (⊥{α}, 0)` - (assuming 0 is the "entry block"), - and `∀ n < N - 1, l[n] ⊑ l[n+1]` (successive entries constitute valid steps) + We can now define a type for "traces" `𝕥` as a list of + `N` `α × ℕ` entries + (corresponding to program states at successive times) + where `𝕥[0] = (⊥{α}, 0)` + (sound entry to trace (assuming 0 is the "entry block")), + and `∀ n < N - 1, 𝕥[n] ⊑ 𝕥[n+1]` + (successive entries in trace constitute valid steps) Now if `ν := 𝕏.vals` is a dataflow solution, - and `ℓₙ := (n, _) := ℓ; n` - and `ℓₐ := (_, α₀) := ℓ; α₀` + and `𝕥ₙ := (n, _) := 𝕥; n` + and `𝕥ₐ := (_, α₀) := 𝕥; α₀` it is provable inductively from `𝕏.props` that: - `∀ ℓ, ℓₐ ∼ ν[ℓₙ]`. + `∀ 𝕥, 𝕥ₐ ∼ ν[𝕥ₙ]`. In the case of our concrete example, this means that we can prove - that any program state `αₙ` at node `n` reached through stepping - from the entry state is constrained by - `αₙ ∼ βₙ` for the abstract state `βₙ := ν[n]`. - For various values of `αₙ` and `βₙ`, + that any program state `αₙ` at node `n` reached in a trace satifies + `αₙ ∼ ν[n]` (the concrete state refines the abstract state) + For various values of `αₙ` and `ν[n]`, this could mean (for all keys `k`), `αₙ ∼ 𝕄` : no information `αₙ ∼ 𝔸` : `k` is defined `αₙ ∼ 𝕊 m` : `k` is defined and equal to `m` - `αₙ ∼ 𝕌` : impossible (which implies that `∄ ℓ, ℓₐ ∼ 𝕌)`, + `αₙ ∼ 𝕌` : impossible (which implies that `∄ 𝕥, 𝕥ₐ ∼ 𝕌)`, i.e., no node `n` satisfying `ν[n] = 𝕌` will ever be reached by a path - These are powerful results, for which much - thought has gone into generating and - presenting conveniently. + These are powerful results, hopefully + presented in sufficiently accessible + datatypes to yield modular use. -/ end ConcreteSolution end ConcreteMapImpl From f8a7b618556ce1ad2fd3a824c7e6b09971d7e45d Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Fri, 4 Jul 2025 19:39:30 -0400 Subject: [PATCH 19/22] wording tweaks --- KLR/Compile/Dataflow.lean | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index ce7c6a76..1c4ed761 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -1281,8 +1281,9 @@ section ConcreteMapImpl with a "stepping relation" for each node `σ : ℕ → α → α`, and a "simulation relation" `α₀ ∼ β₀ : Prop` satisfying `∀ n, α₀ ∼ β₀ → (σₙ α₀) ∼ (τₙ β₀)` + (simulation is preserved by applying respective stepping/transition functions) and `β₀ ≤ β₁ → α₀ ∼ β₀ → α₀ ∼ β₁` - and `β₀ == β₁ → α₀ ∼ β₀ → α₀ ∼ β₁`. + (simulation is weakened by weakening `β`). We must also choose a `⊥{α}` for `α`, (corresponding to value at program entry) @@ -1299,11 +1300,14 @@ section ConcreteMapImpl `(_:Option ℕ) ∼ (_:ℂ)` relation (e.g. `some n ∼ 𝕊 n`)) Once the associated properties are proven... - We can now define "program states" `π := (α₀ : α) × (n : ℕ)` (interpreted - as the statement "execution has state `α` at entry to block `n`. + We can now define "program states" `π := (a : α) × (n : ℕ)` (interpreted + as the statement "execution has entered node `n` with state `a`. We can now define "program stepping": `π₀ ⊑ π₁ := (edge π₀.n π₁.n) ∧ (n:=π₀.n; τₙ) π₀.α₀ = π₁.α₀` + (i.e., `π₀` steps to `π₁` if `n₀` has an edge to `n₁` + and applying the indexed transition `τ` for node `n₀` + to `α₀` yields `α₁`.) We can now define a type for "traces" `𝕥` as a list of `N` `α × ℕ` entries @@ -1311,7 +1315,17 @@ section ConcreteMapImpl where `𝕥[0] = (⊥{α}, 0)` (sound entry to trace (assuming 0 is the "entry block")), and `∀ n < N - 1, 𝕥[n] ⊑ 𝕥[n+1]` - (successive entries in trace constitute valid steps) + (successive entries in trace constitute valid steps). + + Traces `𝕥` are the type of program executions! (trying to + decide many properties of the type will thus be impossible + however, the 'bisimulation' between the inductive constructors + for `𝕥` (for a neatly dependently typed implementation of the datatype) + and the transitions in the abstract domain, along with dataflow + equations that provide a tractable description of all sound + abstract program paths. Since this type has finite description, + properties can be proven that then project onto corresponding + properties of concrete program execution.) Now if `ν := 𝕏.vals` is a dataflow solution, and `𝕥ₙ := (n, _) := 𝕥; n` From e2fe2459e900bc0db35a7de1c6df082ce1695db9 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Mon, 7 Jul 2025 12:22:55 -0400 Subject: [PATCH 20/22] remove unnecessary instance --- KLR/Compile/Dataflow.lean | 8 -------- 1 file changed, 8 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 1c4ed761..4bfeaf24 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -1067,14 +1067,6 @@ section ConcreteMapImpl | 𝕊 n => s!"(𝕊 {n})" | 𝕌 => "𝕌" - instance : DecidableEq ℂ := by { - unfold DecidableEq - intro a b - by_cases h: (a=b) - apply isTrue; assumption - apply isFalse; assumption - } - instance : Max ℂ where max := fun | 𝕄, _ From 19714568d5623bbc5dc888f50bf8ae2e267e849d Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Tue, 8 Jul 2025 15:28:08 -0400 Subject: [PATCH 21/22] start working on UseDefImpl --- KLR/Compile/Dataflow.lean | 41 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 4bfeaf24..7a4f2cad 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -1345,4 +1345,45 @@ section ConcreteMapImpl end ConcreteSolution end ConcreteMapImpl +section UseDefChains + variable (num_nodes num_keys : ℕ) + variable (start_node : ℕ) + variable (edges : ℕ → ℕ → Bool) + + inductive UseDef where + | Use : ℕ → UseDef + | Def : ℕ → UseDef + deriving DecidableEq + + def UseDef.isUse := fun + | UseDef.Use _ => true + | _ => false + + def UseDef.isDef := fun + | UseDef.Def _ => true + | _ => false + + variable (labels : ℕ → UseDef) + + structure trace (last : ℕ) where + path : List ℕ + start_sound : path[0]? = some start_node + last_sound : path.getLast? = some last + + def trace.lastDefOf {n} (t : trace start_node n) (k : ℕ) : Option ℕ := + let rec lastOf := fun + | List.nil => none + | List.cons n tail => + if labels n = UseDef.Def k then some n else lastOf tail + lastOf t.path + + def solution : Type := (use_defs : (n : ℕ) → (labels n).isUse → List ℕ) ×' + (∀ (x n last) + (h_last : (labels last).isUse) + (t : trace start_node last) + (_ : t.lastDefOf start_node labels x = some n), + n ∈ use_defs last h_last) +end UseDefChains + + -- thanks for reading! - Julia 💕 From 80896a0d6bedb7d3e42f26b49ba398732e10a622 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Wed, 9 Jul 2025 15:33:50 -0400 Subject: [PATCH 22/22] tweaks --- KLR/Compile/Dataflow.lean | 50 ++++++++++++++++++++++++++++++++++----- 1 file changed, 44 insertions(+), 6 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 7a4f2cad..e9f85b5b 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -1042,7 +1042,7 @@ end InnerMapImpl wooo!!! 🎉 -/ -section ConcreteMapImpl +namespace ConcreteMapImpl /- Section `IsConstImpl` defines the "constancy type" `ℂ`, and all needed structure on `ℂ` to eventually construct a `DataflowProblem ℕ ⟦ℕ, ℂ⟧`. @@ -1345,7 +1345,10 @@ section ConcreteMapImpl end ConcreteSolution end ConcreteMapImpl -section UseDefChains +/- + This section (WIP) computes use def chains +-/ +namespace UseDefImpl variable (num_nodes num_keys : ℕ) variable (start_node : ℕ) variable (edges : ℕ → ℕ → Bool) @@ -1368,9 +1371,10 @@ section UseDefChains structure trace (last : ℕ) where path : List ℕ start_sound : path[0]? = some start_node + path_sound : ∀ n (h : n < path.length - 1), edges path[n] path[n+1] last_sound : path.getLast? = some last - def trace.lastDefOf {n} (t : trace start_node n) (k : ℕ) : Option ℕ := + def trace.lastDefOf {n} (t : trace start_node edges n) (k : ℕ) : Option ℕ := let rec lastOf := fun | List.nil => none | List.cons n tail => @@ -1380,10 +1384,44 @@ section UseDefChains def solution : Type := (use_defs : (n : ℕ) → (labels n).isUse → List ℕ) ×' (∀ (x n last) (h_last : (labels last).isUse) - (t : trace start_node last) - (_ : t.lastDefOf start_node labels x = some n), + (t : trace start_node edges last) + (_ : t.lastDefOf start_node edges labels x = some n), n ∈ use_defs last h_last) -end UseDefChains + + + /- + This section defines an instance of dataflow used to compute the usedef relation + -/ + section DataflowInstance + abbrev ρ := Vector Bool num_nodes + + def ρ1 (n : ℕ) : Vector Bool num_nodes := Vector.ofFn (fun n' ↦ n = n'.val) + + instance : Preorder (ρ num_nodes) where + le_refl := sorry + le_trans := sorry + + instance : Max (ρ num_nodes) where + max := Vector.zipWith Bool.or + + instance : HasBot (ρ num_nodes) where + bot := Vector.replicate num_nodes False + + def 𝕏 := Solution + (ρ:=ρ num_nodes) + (le_supl:=sorry) + (le_supr:=sorry) + (num_nodes:=num_nodes) + (num_keys:=num_keys) + (edges:=edges) + (transitions:=fun n k ρ => + match labels n with + | UseDef.Def k' => if k = k' then ρ1 num_nodes n else ρ + | _ => ρ) + + + end DataflowInstance +end UseDefImpl -- thanks for reading! - Julia 💕