From 28b8341e2f8380fddde1768a7bf51ad6614e52f1 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Wed, 16 Jul 2025 08:45:21 -0400 Subject: [PATCH 01/33] add ast to cfg walker for nki --- KLR/Compile/NKIDataflow.lean | 153 +++++++++++++++++++++++++++++++++++ 1 file changed, 153 insertions(+) create mode 100644 KLR/Compile/NKIDataflow.lean diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean new file mode 100644 index 00000000..eaaeb36f --- /dev/null +++ b/KLR/Compile/NKIDataflow.lean @@ -0,0 +1,153 @@ +import KLR.NKI.Basic + +open KLR.NKI + +abbrev ℕ := Nat + +inductive VarAction where + | Read (name : String) + | Write (name : String) (ty : Option Expr) + | None + +structure NKIWalker where + num_nodes : ℕ + last_node : ℕ + actions : ℕ → VarAction + edges : ℕ → ℕ → Bool + breaks : List ℕ + conts : List ℕ + rets : List ℕ + +def NKIWalker.init : NKIWalker := { + num_nodes := 1 + last_node := 0 + actions _ := VarAction.None + edges _ _ := false + breaks := [] + conts := [] + rets := [] +} + +def NKIWalker.processAction (walker : NKIWalker) (action : VarAction) : NKIWalker := + let N := walker.num_nodes + {walker with + num_nodes := N + 1 + last_node := N + actions n := if n = N then action else walker.actions n + edges A B := (A, B) = (walker.last_node, N) + ∨ (walker.edges A B) + } + +def NKIWalker.setLast (walker : NKIWalker) (last_node : ℕ) : NKIWalker := {walker with + last_node := last_node +} + +def NKIWalker.addEdge (walker : NKIWalker) (a b : ℕ) : NKIWalker := {walker with + edges A B := (A, B) = (a, b) ∨ walker.edges A B +} + +def NKIWalker.addBreak (walker : NKIWalker) : NKIWalker := {walker with + breaks := walker.breaks ++ [walker.last_node] +} + +def NKIWalker.clearBreaks (walker : NKIWalker) : NKIWalker := {walker with + breaks := [] +} + +def NKIWalker.addContinue (walker : NKIWalker): NKIWalker := {walker with + conts := walker.conts ++ [walker.last_node] +} + +def NKIWalker.clearConts (walker : NKIWalker) : NKIWalker := {walker with + conts := [] +} + +def NKIWalker.addReturn (walker : NKIWalker) : NKIWalker := {walker with + rets := walker.rets ++ [walker.last_node] +} + +/-mutual +def NKIWalker.processExpr (walker : NKIWalker) (expr : Expr) : Nat := + match h : expr.expr with + | Expr'.tuple x => (walker.processExprList x).sum + | _ => 0 + termination_by sizeOf expr + decreasing_by cases expr; simp at h; rw [h]; simp; omega +def NKIWalker.processExprList (walker : NKIWalker) (exprs : List Expr) : List Nat := + exprs.map walker.processExpr + termination_by sizeOf exprs +end-/ + +mutual +def NKIWalker.processExpr (walker : NKIWalker) (expr : Expr) : NKIWalker := + let ⟨expr, _⟩ := expr + match _ : expr with + | Expr'.value _ => walker + | Expr'.var (name : String) => walker.processAction (VarAction.Read name) + | Expr'.proj (expr : Expr) _ => walker.processExpr expr + | Expr'.tuple (elements : List Expr) => walker.processExprList elements + | Expr'.access (expr : Expr) _ => walker.processExpr expr + | Expr'.binOp _ left right => (walker.processExpr left).processExpr right + | Expr'.ifExp test body orelse => + let body_walker := ((walker.processExpr test).processExpr body) + let orelse_walker := ((body_walker.setLast walker.last_node).processExpr orelse) + let complete_walker := (orelse_walker.processAction VarAction.None) + complete_walker.addEdge body_walker.last_node complete_walker.last_node + | Expr'.call (f: Expr) (args: List Expr) (_ : List Keyword) => + (walker.processExpr f).processExprList args + termination_by sizeOf expr + decreasing_by + all_goals { + try {rename_i expr' _<;> rcases h' : (expr, expr') with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega} + try {rcases h' : expr with ⟨⟨⟩, ⟨⟩⟩ <;> simp_all <;> omega} + } + +def NKIWalker.processExprList (walker : NKIWalker) (exprs : List Expr) : NKIWalker := + exprs.foldl NKIWalker.processExpr walker + termination_by sizeOf exprs +end + +mutual +def NKIWalker.processStmt (walker : NKIWalker) (stmt : Stmt) : NKIWalker := + let ⟨stmt, _⟩ := stmt + match _ : stmt with + | Stmt'.expr (e : Expr) => walker.processExpr e + | Stmt'.assert (e : Expr) => walker.processExpr e + | Stmt'.ret (e : Expr) => (walker.processExpr e).addReturn + | Stmt'.assign (x : Expr) (ty : Option Expr) (e : Option Expr) => + let withx := (walker.processExpr x) + let withty := (match ty with | some ty => withx.processExpr ty | none => withx) + match e with | some e => withty.processExpr e | none => withty + | Stmt'.ifStm (e : Expr) (thn : List Stmt) (els : List Stmt) => + let then_walker := (walker.processExpr e).processStmtList thn + let else_walker := (then_walker.setLast walker.last_node).processStmtList els + let complete := else_walker.processAction VarAction.None + complete.addEdge then_walker.last_node complete.last_node + | Stmt'.forLoop (x : Expr) (iter: Expr) (body: List Stmt) => + let intro_walker := (walker.processExpr x).processExpr iter + let outer_breaks := intro_walker.breaks + let outer_conts := intro_walker.conts + let inner_walker := ((intro_walker.clearBreaks).clearConts).processAction VarAction.None + let enter_node := inner_walker.last_node + let inner_walked := inner_walker.processStmtList body + let nearly_complete := (inner_walked.addEdge inner_walked.last_node enter_node).setLast enter_node + let complete := nearly_complete.processAction VarAction.None + let exit_node := complete.last_node + let with_conts := complete.conts.foldl (fun walker cont ↦ walker.addEdge cont enter_node) complete + let with_breaks := complete.breaks.foldl (fun walker brk ↦ walker.addEdge brk exit_node) with_conts + {with_breaks with + conts := outer_conts + breaks := outer_breaks + } + | Stmt'.breakLoop => (walker.processAction VarAction.None).addBreak + | Stmt'.continueLoop => (walker.processAction VarAction.None).addContinue + termination_by sizeOf stmt + decreasing_by + try rcases h : (thn, stmt) with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega + try rcases h : (els, stmt) with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega + try rcases h : (body, stmt) with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega + +def NKIWalker.processStmtList (walker : NKIWalker) (stmts : List Stmt) : NKIWalker := + stmts.foldl NKIWalker.processStmt walker + termination_by sizeOf stmts +end From edb3ae82d2c0b94da9795b3f85ae9d167ec81d06 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Wed, 16 Jul 2025 08:57:12 -0400 Subject: [PATCH 02/33] add tiny bit more --- KLR/Compile/NKIDataflow.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index eaaeb36f..554bf891 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -151,3 +151,9 @@ def NKIWalker.processStmtList (walker : NKIWalker) (stmts : List Stmt) : NKIWalk stmts.foldl NKIWalker.processStmt walker termination_by sizeOf stmts end + +def NKIWalker.processFun (f : Fun) : NKIWalker := + let body_walker := (NKIWalker.init.processStmtList f.body).processAction VarAction.None + body_walker.rets.foldl (fun walker ret ↦ walker.addEdge ret body_walker.last_node) body_walker + +def NKIWalker.isClosed (walker : NKIWalker) := walker.breaks.isEmpty ∧ walker.conts.isEmpty From f749f8d2ce351ddf844c6b55091ec408e1e24451 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Wed, 16 Jul 2025 10:50:58 -0400 Subject: [PATCH 03/33] add tostrings --- KLR/Compile/NKIDataflow.lean | 83 ++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index 554bf891..a73e7571 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -9,6 +9,12 @@ inductive VarAction where | Write (name : String) (ty : Option Expr) | None +instance VarAction.toString : ToString VarAction where + toString := fun + | Read name => s!"Read({name})" + | Write name _ => s!"Write({name})" + | None => "None" + structure NKIWalker where num_nodes : ℕ last_node : ℕ @@ -18,6 +24,14 @@ structure NKIWalker where conts : List ℕ rets : List ℕ +instance NKIWalker.toString : ToString NKIWalker where + toString walker := + let row n := + let tgts := (List.range walker.num_nodes).filter (walker.edges n) + let num := if n = walker.last_node then s!"{n}[exit]" else s!"{n}" + s!"{num} {walker.actions n} ↦ {tgts}\n" + String.intercalate "\n" ((List.range walker.num_nodes).map row) + def NKIWalker.init : NKIWalker := { num_nodes := 1 last_node := 0 @@ -157,3 +171,72 @@ def NKIWalker.processFun (f : Fun) : NKIWalker := body_walker.rets.foldl (fun walker ret ↦ walker.addEdge ret body_walker.last_node) body_walker def NKIWalker.isClosed (walker : NKIWalker) := walker.breaks.isEmpty ∧ walker.conts.isEmpty + +def test_kernel : Kernel := { + entry := "test.test", + funs := [{ name := "test.test", + file := "unknown", + line := 1, + body := [{ stmt := KLR.NKI.Stmt'.assign + { expr := KLR.NKI.Expr'.var "x", + pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 2 } } + none + (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 2, column := 5, lineEnd := some 2, columnEnd := some 6 } }), + pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 6 } }, + { stmt := KLR.NKI.Stmt'.ifStm + { expr := KLR.NKI.Expr'.var "cond0", + pos := { line := 3, column := 4, lineEnd := some 3, columnEnd := some 9 } } + [{ stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "print", + pos := { line := 4, + column := 2, + lineEnd := some 4, + columnEnd := some 7 } } + [{ expr := KLR.NKI.Expr'.var "x", + pos := { line := 4, + column := 8, + lineEnd := some 4, + columnEnd := some 9 } }] + [], + pos := { line := 4, + column := 2, + lineEnd := some 4, + columnEnd := some 10 } }, + pos := { line := 4, column := 2, lineEnd := some 4, columnEnd := some 10 } }] + [{ stmt := KLR.NKI.Stmt'.assign + { expr := KLR.NKI.Expr'.var "y", + pos := { line := 6, + column := 2, + lineEnd := some 6, + columnEnd := some 3 } } + none + (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 6, + column := 6, + lineEnd := some 6, + columnEnd := some 7 } }), + pos := { line := 6, column := 2, lineEnd := some 6, columnEnd := some 7 } }], + pos := { line := 3, column := 1, lineEnd := some 6, columnEnd := some 7 } }, + { stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "print", + pos := { line := 7, + column := 1, + lineEnd := some 7, + columnEnd := some 6 } } + [{ expr := KLR.NKI.Expr'.var "y", + pos := { line := 7, + column := 7, + lineEnd := some 7, + columnEnd := some 8 } }] + [], + pos := { line := 7, column := 1, lineEnd := some 7, columnEnd := some 9 } }, + pos := { line := 7, column := 1, lineEnd := some 7, columnEnd := some 9 } }], + args := [] }], + args := [], + globals := [] } + + def 𝕏 := NKIWalker.processFun test_kernel.funs[0] + #eval 𝕏 From ca90e8b445a38c9b34c28f8addc2ca6761cc1d12 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Wed, 16 Jul 2025 11:39:54 -0400 Subject: [PATCH 04/33] add example --- KLR/Compile/NKIDataflow.lean | 112 +++++++++++++++++++++++++++++------ 1 file changed, 93 insertions(+), 19 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index a73e7571..e17dc8ee 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -1,9 +1,8 @@ import KLR.NKI.Basic +import KLR.Compile.Dataflow open KLR.NKI -abbrev ℕ := Nat - inductive VarAction where | Read (name : String) | Write (name : String) (ty : Option Expr) @@ -15,6 +14,11 @@ instance VarAction.toString : ToString VarAction where | Write name _ => s!"Write({name})" | None => "None" +def VarAction.var := fun + | Read name => some name + | Write name _ => some name + | None => none + structure NKIWalker where num_nodes : ℕ last_node : ℕ @@ -23,6 +27,7 @@ structure NKIWalker where breaks : List ℕ conts : List ℕ rets : List ℕ + vars : List String --list of varnames seen instance NKIWalker.toString : ToString NKIWalker where toString walker := @@ -30,7 +35,7 @@ instance NKIWalker.toString : ToString NKIWalker where let tgts := (List.range walker.num_nodes).filter (walker.edges n) let num := if n = walker.last_node then s!"{n}[exit]" else s!"{n}" s!"{num} {walker.actions n} ↦ {tgts}\n" - String.intercalate "\n" ((List.range walker.num_nodes).map row) + String.intercalate "\n" ((List.range walker.num_nodes).map row ++ ["vars: ", walker.vars.toString]) def NKIWalker.init : NKIWalker := { num_nodes := 1 @@ -40,6 +45,7 @@ def NKIWalker.init : NKIWalker := { breaks := [] conts := [] rets := [] + vars := [] } def NKIWalker.processAction (walker : NKIWalker) (action : VarAction) : NKIWalker := @@ -50,6 +56,9 @@ def NKIWalker.processAction (walker : NKIWalker) (action : VarAction) : NKIWalke actions n := if n = N then action else walker.actions n edges A B := (A, B) = (walker.last_node, N) ∨ (walker.edges A B) + vars := match action.var with + | some var => if var ∈ walker.vars then walker.vars else walker.vars.concat var + | none => walker.vars } def NKIWalker.setLast (walker : NKIWalker) (last_node : ℕ) : NKIWalker := {walker with @@ -128,10 +137,14 @@ def NKIWalker.processStmt (walker : NKIWalker) (stmt : Stmt) : NKIWalker := | Stmt'.expr (e : Expr) => walker.processExpr e | Stmt'.assert (e : Expr) => walker.processExpr e | Stmt'.ret (e : Expr) => (walker.processExpr e).addReturn - | Stmt'.assign (x : Expr) (ty : Option Expr) (e : Option Expr) => - let withx := (walker.processExpr x) - let withty := (match ty with | some ty => withx.processExpr ty | none => withx) - match e with | some e => withty.processExpr e | none => withty + | Stmt'.assign ⟨Expr'.var name, _⟩ (ty : Option Expr) (e : Option Expr) => + let withty := (match ty with | some ty => walker.processExpr ty | none => walker) + let withe := (match e with | some e => withty.processExpr e | none => withty) + withe.processAction (VarAction.Write name ty) + | Stmt'.assign _ (ty : Option Expr) (e : Option Expr) => + let withty := (match ty with | some ty => walker.processExpr ty | none => walker) + let withe := (match e with | some e => withty.processExpr e | none => withty) + withe.processAction (VarAction.Write "NONVAR" ty) | Stmt'.ifStm (e : Expr) (thn : List Stmt) (els : List Stmt) => let then_walker := (walker.processExpr e).processStmtList thn let else_walker := (then_walker.setLast walker.last_node).processStmtList els @@ -172,6 +185,17 @@ def NKIWalker.processFun (f : Fun) : NKIWalker := def NKIWalker.isClosed (walker : NKIWalker) := walker.breaks.isEmpty ∧ walker.conts.isEmpty + +/- +def test(): + x = 0 + if cond0: + print(x) + else: + y = 0 + print(y) + print(y) +-/ def test_kernel : Kernel := { entry := "test.test", funs := [{ name := "test.test", @@ -215,28 +239,78 @@ def test_kernel : Kernel := { (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), pos := { line := 6, column := 6, - lineEnd := some 6, - columnEnd := some 7 } }), - pos := { line := 6, column := 2, lineEnd := some 6, columnEnd := some 7 } }], - pos := { line := 3, column := 1, lineEnd := some 6, columnEnd := some 7 } }, + lineEnd := some 6, + columnEnd := some 7 } }), + pos := { line := 6, column := 2, lineEnd := some 6, columnEnd := some 7 } }, + { stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "print", + pos := { line := 7, + column := 2, + lineEnd := some 7, + columnEnd := some 7 } } + [{ expr := KLR.NKI.Expr'.var "y", + pos := { line := 7, + column := 8, + lineEnd := some 7, + columnEnd := some 9 } }] + [], + pos := { line := 7, + column := 2, + lineEnd := some 7, + columnEnd := some 10 } }, + pos := { line := 7, column := 2, lineEnd := some 7, columnEnd := some 10 } }], + pos := { line := 3, column := 1, lineEnd := some 7, columnEnd := some 10 } }, { stmt := KLR.NKI.Stmt'.expr { expr := KLR.NKI.Expr'.call { expr := KLR.NKI.Expr'.var "print", - pos := { line := 7, + pos := { line := 8, column := 1, - lineEnd := some 7, + lineEnd := some 8, columnEnd := some 6 } } [{ expr := KLR.NKI.Expr'.var "y", - pos := { line := 7, + pos := { line := 8, column := 7, - lineEnd := some 7, + lineEnd := some 8, columnEnd := some 8 } }] [], - pos := { line := 7, column := 1, lineEnd := some 7, columnEnd := some 9 } }, - pos := { line := 7, column := 1, lineEnd := some 7, columnEnd := some 9 } }], + pos := { line := 8, column := 1, lineEnd := some 8, columnEnd := some 9 } }, + pos := { line := 8, column := 1, lineEnd := some 8, columnEnd := some 9 } }], args := [] }], args := [], globals := [] } - def 𝕏 := NKIWalker.processFun test_kernel.funs[0] - #eval 𝕏 +def walker := NKIWalker.processFun test_kernel.funs[0] +#eval walker +def transitions (n k : ℕ) (pre : Bool) : Bool := + (n = 0) ∨ + if _ : k < walker.vars.length then + match walker.actions n with + | VarAction.Write name _ => ¬ (name = walker.vars[k]) ∧ pre + | _ => pre + else + pre + +instance : Preorder Bool where + le_refl := by trivial + le_trans := by trivial + +instance : HasBot Bool where + bot := false + +instance : ToString Bool where + toString := fun + | true => "_" + | false => "DEF" + + +def 𝕏 := Solution + (ρ:=Bool) + (le_supl:=by trivial) + (le_supr:=by trivial) + (num_nodes:=walker.num_nodes) + (num_keys:=walker.vars.length) + (edges:=walker.edges) + (transitions:=transitions) + +#eval 𝕏 From eb58e4df0a167b3654a6bb4ef9ad8fa5bd361976 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Wed, 16 Jul 2025 12:52:09 -0400 Subject: [PATCH 05/33] more work --- KLR/Compile/NKIDataflow.lean | 64 ++++++++++++++++++++++++++++++++++-- 1 file changed, 61 insertions(+), 3 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index e17dc8ee..c2a234d3 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -37,6 +37,7 @@ instance NKIWalker.toString : ToString NKIWalker where s!"{num} {walker.actions n} ↦ {tgts}\n" String.intercalate "\n" ((List.range walker.num_nodes).map row ++ ["vars: ", walker.vars.toString]) +@[simp] def NKIWalker.init : NKIWalker := { num_nodes := 1 last_node := 0 @@ -48,6 +49,7 @@ def NKIWalker.init : NKIWalker := { vars := [] } +@[simp] def NKIWalker.processAction (walker : NKIWalker) (action : VarAction) : NKIWalker := let N := walker.num_nodes {walker with @@ -61,18 +63,22 @@ def NKIWalker.processAction (walker : NKIWalker) (action : VarAction) : NKIWalke | none => walker.vars } +@[simp] def NKIWalker.setLast (walker : NKIWalker) (last_node : ℕ) : NKIWalker := {walker with last_node := last_node } +@[simp] def NKIWalker.addEdge (walker : NKIWalker) (a b : ℕ) : NKIWalker := {walker with edges A B := (A, B) = (a, b) ∨ walker.edges A B } +@[simp] def NKIWalker.addBreak (walker : NKIWalker) : NKIWalker := {walker with breaks := walker.breaks ++ [walker.last_node] } +@[simp] def NKIWalker.clearBreaks (walker : NKIWalker) : NKIWalker := {walker with breaks := [] } @@ -81,10 +87,12 @@ def NKIWalker.addContinue (walker : NKIWalker): NKIWalker := {walker with conts := walker.conts ++ [walker.last_node] } +@[simp] def NKIWalker.clearConts (walker : NKIWalker) : NKIWalker := {walker with conts := [] } +@[simp] def NKIWalker.addReturn (walker : NKIWalker) : NKIWalker := {walker with rets := walker.rets ++ [walker.last_node] } @@ -102,6 +110,7 @@ def NKIWalker.processExprList (walker : NKIWalker) (exprs : List Expr) : List Na end-/ mutual +@[simp] def NKIWalker.processExpr (walker : NKIWalker) (expr : Expr) : NKIWalker := let ⟨expr, _⟩ := expr match _ : expr with @@ -125,12 +134,14 @@ def NKIWalker.processExpr (walker : NKIWalker) (expr : Expr) : NKIWalker := try {rcases h' : expr with ⟨⟨⟩, ⟨⟩⟩ <;> simp_all <;> omega} } +@[simp] def NKIWalker.processExprList (walker : NKIWalker) (exprs : List Expr) : NKIWalker := exprs.foldl NKIWalker.processExpr walker termination_by sizeOf exprs end mutual +@[simp] def NKIWalker.processStmt (walker : NKIWalker) (stmt : Stmt) : NKIWalker := let ⟨stmt, _⟩ := stmt match _ : stmt with @@ -174,15 +185,18 @@ def NKIWalker.processStmt (walker : NKIWalker) (stmt : Stmt) : NKIWalker := try rcases h : (els, stmt) with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega try rcases h : (body, stmt) with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega +@[simp] def NKIWalker.processStmtList (walker : NKIWalker) (stmts : List Stmt) : NKIWalker := stmts.foldl NKIWalker.processStmt walker termination_by sizeOf stmts end +@[simp] def NKIWalker.processFun (f : Fun) : NKIWalker := let body_walker := (NKIWalker.init.processStmtList f.body).processAction VarAction.None body_walker.rets.foldl (fun walker ret ↦ walker.addEdge ret body_walker.last_node) body_walker +@[simp] def NKIWalker.isClosed (walker : NKIWalker) := walker.breaks.isEmpty ∧ walker.conts.isEmpty @@ -196,6 +210,7 @@ def test(): print(y) print(y) -/ +@[simp] def test_kernel : Kernel := { entry := "test.test", funs := [{ name := "test.test", @@ -282,6 +297,8 @@ def test_kernel : Kernel := { def walker := NKIWalker.processFun test_kernel.funs[0] #eval walker + +@[simp] def transitions (n k : ℕ) (pre : Bool) : Bool := (n = 0) ∨ if _ : k < walker.vars.length then @@ -304,13 +321,54 @@ instance : ToString Bool where | false => "DEF" -def 𝕏 := Solution +#eval walker.num_nodes +example : walker.num_nodes = 12 := by { + simp_all! +} + +@[simp] +def 𝕏 := (Solution (ρ:=Bool) (le_supl:=by trivial) (le_supr:=by trivial) (num_nodes:=walker.num_nodes) (num_keys:=walker.vars.length) (edges:=walker.edges) - (transitions:=transitions) + (transitions:=transitions)).get (by { + sorry + }) +#eval! 𝕏 + +theorem reads_valid + : ∀ n k, (hn: n < walker.num_nodes) → (hk: k < walker.vars.length) → + walker.actions n = VarAction.Read (walker.vars[k]) → 𝕏.vals n k hn hk := + fun n k hn hk h ↦ match n with + | 0 => sorry + | 1 => sorry + | 2 => sorry + | 3 => sorry + | 4 => sorry + | 5 => sorry + | 6 => sorry + | 7 => sorry + | 8 => sorry + | 9 => sorry + | 10 => sorry + | 11 => sorry + | n + 12 => sorry + + + + +structure Path where + nodes : List ℕ + nonempty : nodes ≠ [] + sound : ∀ i (_ : i < nodes.length - 1), walker.edges nodes[i] nodes[i+1] + +def Path.motive (path : Path) := + 𝕏.vals (path.nodes.getLast path.nonempty) -#eval 𝕏 + match walker.actions (path.nodes.getLast path.nonempty) with + | VarAction.Read name => + ∃ i, i < path.nodes.length - 1 ∧ walker.actions i = VarAction.Read name + | _ => True From 906e82affe00f31390caa5a159dca18bcf56f480 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Thu, 17 Jul 2025 12:09:40 -0400 Subject: [PATCH 06/33] work --- KLR/Compile/DFSimp.lean | 8 ++ KLR/Compile/Dataflow.lean | 31 +++++++- KLR/Compile/NKIDataflow.lean | 140 +++++++++++++++++++++++++++++++++-- 3 files changed, 171 insertions(+), 8 deletions(-) create mode 100644 KLR/Compile/DFSimp.lean diff --git a/KLR/Compile/DFSimp.lean b/KLR/Compile/DFSimp.lean new file mode 100644 index 00000000..a6b81e30 --- /dev/null +++ b/KLR/Compile/DFSimp.lean @@ -0,0 +1,8 @@ +import Lean +open Lean.Meta + +initialize + discard <| registerSimpAttr `df_simp "Dataflow definitions to be fed to simp" + +initialize + discard <| registerSimpAttr `nm_simp "Nodemap definitions to be fed to simp" diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index e9f85b5b..ae855dd0 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -96,6 +96,7 @@ 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 KLR.Compile.DFSimp -- sigh i shouldn't have to do this abbrev ℕ := Nat @@ -198,6 +199,7 @@ section Basics infix:100 "⊔" => Max.max + @[df_simp] def NodeMap.instBEq {α β : Type} [NodeMap α] [BEq β] : BEq ⟦α, β⟧ := { beq μ₀ μ₁ := μ₀ fold⟪true, (fun a prev => prev ∧ (μ₀◃a == μ₁◃a))⟫ } @@ -300,7 +302,6 @@ section Basics end Basics - /- The section `DataflowProblemSolver ` is parameterized on an instance of `DataflowProblem α β`. It builds on the definitions of maps `⟦α, β⟧` from `NodeMap α`, and on the transition functions @@ -313,20 +314,29 @@ end Basics the dataflow problem, and a `I' ν : Prop` - which captures that `ν` satisfies the dataflow problem. -/ section DataflowProblemSolver + variable {α β : Type} [BEq α] {DP: DataflowProblem α β} open DataflowProblem + @[df_simp] def ν₀ : ⟦α, (β × Bool)⟧ := ⟪↦(⊥, true)⟫ + @[df_simp] def ε (a₀ a₁ : Node α) : Bool := List.elem a₁ (σ◃a₀) + @[df_simp] def strip_bools (ν : ⟦α, (β × Bool)⟧) := ν map⟪fun (β, _)=>β⟫ + @[df_simp] def E (P : (Node α) → (Node α) → Prop) := ∀ (a₀ a₁) (_:ε a₀ a₁), P a₀ a₁ + @[df_simp] def R (ν₀ : ⟦α, (β × Bool)⟧) (ν₁ : ⟦α, β⟧) [LE β]: Prop := E (fun a₀ a₁ => (ν₀◃a₀).2 ∨ (τ◃a₀) ((ν₀◃a₀).1) ≤ (ν₁◃a₁)) + @[df_simp] def I (ν : ⟦α, (β × Bool)⟧) : Prop := R ν (strip_bools ν) + @[df_simp] def R' (ν₀ ν₁ : ⟦α, β⟧) : Prop := E (fun a₀ a₁ => (τ◃a₀) (ν₀◃a₀) ≤ ν₁◃a₁) + @[df_simp] def I' (ν : ⟦α, β⟧) : Prop := R' ν ν theorem base_case : @I α β _ DP ν₀ := by { @@ -337,17 +347,21 @@ section DataflowProblemSolver rw [NodeMap.of_const_get] } + @[df_simp] def δ (ν : ⟦α, (β × Bool)⟧) (a : Node α) : ⟦α, β⟧ := -- step of_func⟪(fun a' => if ε a a' then ((τ◃a) (ν◃a).1) else ⊥)⟫ + @[df_simp] def Δ₀ (ν : ⟦α, (β × Bool)⟧) : ⟦α, β⟧ := ν fold⟪ν map⟪(·.1)⟫, (fun a ν₀ => if (ν◃a).2 then ν₀ ⊔ (δ ν a) else ν₀)⟫ + @[df_simp] def Δ (ν : ⟦α, (β × Bool)⟧) : ⟦α, (β × Bool)⟧ := let ν' := Δ₀ ν of_func⟪fun a => let (β, β') := ((ν◃a).1, (ν'◃a)); (β', β != β')⟫ + @[df_simp] def is_fix (ν : ⟦α, (β × Bool)⟧) : Bool := ν map⟪fun x↦x.2⟫ == ⟪↦false⟫ @@ -529,6 +543,7 @@ section DataflowProblemSolver } } + -- don't want to unroll this automatically def DataflowProblem.solve_to_depth {α β : Type} (depth : ℕ) (DP : DataflowProblem α β) @@ -546,6 +561,7 @@ section DataflowProblemSolver else solve_to_depth depth' DP ν' h' + @[df_simp] def DataflowProblem.solve {α β : Type} [BEq α] (DP : DataflowProblem α β) : Option ((ν : ⟦α, β⟧) ×' I' ν) @@ -585,27 +601,35 @@ section FiniteDataflowProblemSolver le_supl (β₀ β₁ : β) : β₀ ≤ Max.max β₀ β₁ le_supr (β₀ β₁ : β) : β₁ ≤ Max.max β₀ β₁ + @[df_simp] def LtProp : NodeProp ℕ where node_prop n' := n' < n + @[df_simp] def NodeT := @Node ℕ (LtProp n) + @[df_simp] def node_to_fin (nd : NodeT n) : (Fin n) := {val := @nd.data, isLt := @nd.sound} + @[df_simp] def fin_to_node (fin : Fin n) : (NodeT n) := @Node.mk ℕ (LtProp n) fin.val fin.isLt + @[df_simp] def nodes : Vector (NodeT n) n := Vector.ofFn (fin_to_node n) + @[df_simp] def vector_fn {β : Type} (f : NodeT n → β) : Vector β n := Vector.ofFn (f ∘ (fin_to_node n)) + @[df_simp] def FiniteNodeProp : NodeProp ℕ := { node_prop n' := n' < n } + @[df_simp] def FiniteNodeMap : NodeMap ℕ := { FiniteNodeProp n with μ β := Vector β n @@ -697,6 +721,7 @@ section FiniteDataflowProblemSolver This is the end of the section because the returned instance provides the `DataflowProblem.solve` function. -/ + @[df_simp] def FiniteDataflowProblem {β : Type} [BEq β] [P:Preorder β] @@ -854,6 +879,7 @@ section InnerMapImpl it allows significant code reuse and defines dataflowproblems with `β` equal to a map type minimally. -/ + @[df_simp] def FNM : NodeMap ℕ := (FiniteNodeMap num_keys) /- @@ -866,6 +892,7 @@ section InnerMapImpl proven properties of `⟦⬝, ⬝⟧` types. None are very surprising. -/ + @[df_simp] def FSI {_:NodeMap ℕ}: FiniteSolverInput (⟦ℕ, ρ⟧) := { num_nodes := num_nodes edges := edges @@ -935,6 +962,7 @@ section InnerMapImpl `Node ℕ` instances (of each `NodeMap ℕ` class!). None of these proofs are surprising. -/ + @[df_simp] def Solution : Option (SolutionT ρ num_nodes num_keys edges transitions) := let NMK : NodeMap ℕ := FNM num_keys let DP : DataflowProblem ℕ ⟦ℕ, ρ⟧ := FiniteDataflowProblem num_nodes @@ -1424,4 +1452,5 @@ namespace UseDefImpl end UseDefImpl + -- thanks for reading! - Julia 💕 diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index c2a234d3..5f161f29 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -14,6 +14,7 @@ instance VarAction.toString : ToString VarAction where | Write name _ => s!"Write({name})" | None => "None" +@[simp] def VarAction.var := fun | Read name => some name | Write name _ => some name @@ -295,7 +296,27 @@ def test_kernel : Kernel := { args := [], globals := [] } -def walker := NKIWalker.processFun test_kernel.funs[0] +/- +def test(): + x = 0 + x +-/ +@[simp] +def test_kernel_min : Kernel := { + entry := "test.test", + funs := [{ name := "test.test", + file := "unknown", + line := 1, + body := [{ stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 2 } }, + pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 2 } }], + args := [] }], + args := [], + globals := [] } + +@[simp] +def walker := NKIWalker.processFun test_kernel_min.funs[0] #eval walker @[simp] @@ -322,23 +343,128 @@ instance : ToString Bool where #eval walker.num_nodes -example : walker.num_nodes = 12 := by { - simp_all! +example : walker.num_nodes = 2 := by { + simp +} + +#eval walker.vars.length +example : walker.vars.length = 0 := by { + simp } + +--attribute [df_simp] List.foldl +--attribute [df_simp] Vector.ofFn +--attribute [df_simp] Array.ofFn + +def 𝕐 : NKIWalker := ({ num_nodes := 1, last_node := 0, actions := fun x => VarAction.None, + edges := fun _ _ => false, breaks := [], conts := [], rets := [], + vars := [] } : NKIWalker).processStmtList + [{ + stmt := + Stmt'.assign + { expr := Expr'.var "x", + pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 2 } } + none + (some + { expr := Expr'.value (Value.int 0), + pos := { line := 2, column := 5, lineEnd := some 2, columnEnd := some 6 } }), + pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 6 } }, + { + stmt := + Stmt'.expr + { expr := Expr'.var "x", + pos := { line := 3, column := 1, lineEnd := some 3, columnEnd := some 2 } }, + pos := + { line := 3, column := 1, lineEnd := some 3, columnEnd := some 2 } }] + + +#eval 𝕐.num_nodes +example : 𝕐.num_nodes = 3:= by { + unfold 𝕐 + unfold NKIWalker.processStmtList + simp + +} + + @[simp] -def 𝕏 := (Solution +def 𝕏opt := (Solution (ρ:=Bool) (le_supl:=by trivial) (le_supr:=by trivial) (num_nodes:=walker.num_nodes) (num_keys:=walker.vars.length) (edges:=walker.edges) - (transitions:=transitions)).get (by { - sorry - }) + (transitions:=transitions)) + + +#eval 𝕏opt +#synth (BEq (ℕ × Bool)) + +--theorem optsimp {α} (a : α) : (Option.some a).isSome := by simp + +theorem 𝕏present : 𝕏opt.isSome := by { + unfold 𝕏opt + unfold Solution + unfold FiniteDataflowProblem + unfold DataflowProblem.solve + dsimp only [] + unfold DataflowProblem.solve_to_depth + dsimp only [] + unfold ν₀ + unfold Δ + unfold Δ₀ + unfold is_fix + dsimp only [NodeMap.fold] + + + + unfold NodeMap.of_func NodeMap.fold NodeMap.app_unary NodeMap.get + dsimp + + + + + + unfold FiniteNodeMap + + let FNM := (FiniteNodeMap walker.num_nodes) + let F [NodeMap ℕ] [BEq (⟦ℕ, Bool⟧ × Bool)]:= fun a => ( + ⟪↦(⊥, true)⟫ fold⟪⟪↦(⊥, true)⟫map⟪fun x => x.fst⟫,fun a ν₀ => + if (⟪↦(⊥, true)⟫◃a).snd = true then ν₀⊔δ ⟪↦(⊥, true)⟫ a else ν₀⟫◃a, + (⟪↦(⊥, true)⟫◃a).fst + != + ⟪↦(⊥, true)⟫fold⟪⟪↦(⊥, true)⟫map⟪fun x => x.fst⟫,fun a ν₀ => + if (⟪↦(⊥, true)⟫◃a).snd = true then ν₀⊔δ ⟪↦(⊥, true)⟫ a else ν₀⟫◃a) + rw [F] + +} + + + +def 𝕏 := 𝕏opt.get 𝕏present + + + /-(by { + unfold Option.isSome + simp [df_simp] + + repeat unfold DataflowProblem.solve_to_depth + + + + unfold Option.isSome.match_1 Option.casesOn Option.rec + + simp [df_simp] + + + + })-/ #eval! 𝕏 +example : 𝕏.vals 2 0 (by {simp}) (by {}) = false + theorem reads_valid : ∀ n k, (hn: n < walker.num_nodes) → (hk: k < walker.vars.length) → walker.actions n = VarAction.Read (walker.vars[k]) → 𝕏.vals n k hn hk := From 849807fcac193d028d864e38dbc2a6631e70d658 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Fri, 18 Jul 2025 12:15:08 -0400 Subject: [PATCH 07/33] Clean up NKIDataflow example --- .gitignore | 5 + KLR/Compile/DFSimp.lean | 8 -- KLR/Compile/Dataflow.lean | 25 ++++- KLR/Compile/NKIDataflow.lean | 200 ++++++----------------------------- 4 files changed, 55 insertions(+), 183 deletions(-) delete mode 100644 KLR/Compile/DFSimp.lean diff --git a/.gitignore b/.gitignore index 80f25a0f..06544383 100644 --- a/.gitignore +++ b/.gitignore @@ -8,3 +8,8 @@ __pycache__/ build/ dist/ klr.bin +KLR/gotest +KLR/test.py +.gitignore +KLR/Compile/test.lean +KLR/test.ast diff --git a/KLR/Compile/DFSimp.lean b/KLR/Compile/DFSimp.lean deleted file mode 100644 index a6b81e30..00000000 --- a/KLR/Compile/DFSimp.lean +++ /dev/null @@ -1,8 +0,0 @@ -import Lean -open Lean.Meta - -initialize - discard <| registerSimpAttr `df_simp "Dataflow definitions to be fed to simp" - -initialize - discard <| registerSimpAttr `nm_simp "Nodemap definitions to be fed to simp" diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index ae855dd0..6212c6be 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -246,6 +246,16 @@ section Basics } } + theorem NodeMap.of_const_map {α β γ: Type} [BEq β] [BEq γ] [LawfulBEq γ] [NodeMap α] + (b : β) (f : β → γ) : (NodeMap.const (α:=α) b) map⟪f⟫ == ⟪↦(f b)⟫ := by { + rw [beq_ext] + intro a + rw [of_map_get, of_const_get, of_const_get] + simp + } + + --theorem NodeMap.of_func_map {α β γ: Type} [BEq β] [NodeMap α] (μ : ⟦α, β⟧) f (stt : γ) : μ fold⟪stt, f⟫ + instance {α β : Type} [NodeMap α] [ToString α] [ToString β] : ToString ⟦α, β⟧ where toString μ := μ fold⟪"", (fun nd repr => repr ++ "\n{" ++ toString nd.data ++ ": " ++ toString (μ◃nd) ++ "}")⟫ @@ -835,23 +845,27 @@ section InnerMapImpl 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) + key_labels : ℕ → Option String --for debugging printing 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) + let entries := (List.range num_keys).filterMap -- all entries will map to some _ but this isn't a dependent map + (fun k => if hk: k < num_keys then + let pre := match 𝕊.key_labels k with | some s => s!"{s}:" | none => ""; + some (s!"{pre}{(𝕍 n k hn hk)}") + else none) String.intercalate " " entries - let lines := (List.range num_nodes).filterMap + let lines := (List.range num_nodes).filterMap -- all entries will map to some _ but this isn't a dependent map (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) + instance [ToString ρ] : ToString (SolutionT ρ num_nodes num_keys edges transitions) where + toString := SolutionT.toString ρ num_nodes num_keys edges transitions end SolutionImpl @@ -1014,6 +1028,7 @@ section InnerMapImpl some { vals := vals props := props + key_labels _ := none } end InnerMapImpl /- diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index 5f161f29..0a3aaea0 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -200,8 +200,8 @@ def NKIWalker.processFun (f : Fun) : NKIWalker := @[simp] def NKIWalker.isClosed (walker : NKIWalker) := walker.breaks.isEmpty ∧ walker.conts.isEmpty - /- +file test.py: def test(): x = 0 if cond0: @@ -210,6 +210,8 @@ def test(): y = 0 print(y) print(y) + +bash: `klr compile test.py` yields the following serialization of a NKI Kernel -/ @[simp] def test_kernel : Kernel := { @@ -297,29 +299,14 @@ def test_kernel : Kernel := { globals := [] } /- -def test(): - x = 0 - x + Perform the walk of the AST, converting it into a CFG -/ -@[simp] -def test_kernel_min : Kernel := { - entry := "test.test", - funs := [{ name := "test.test", - file := "unknown", - line := 1, - body := [{ stmt := KLR.NKI.Stmt'.expr - { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), - pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 2 } }, - pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 2 } }], - args := [] }], - args := [], - globals := [] } - -@[simp] -def walker := NKIWalker.processFun test_kernel_min.funs[0] +def walker := NKIWalker.processFun test_kernel.funs[0] #eval walker -@[simp] +/- + extract the transitions from the walker +-/ def transitions (n k : ℕ) (pre : Bool) : Bool := (n = 0) ∨ if _ : k < walker.vars.length then @@ -338,57 +325,13 @@ instance : HasBot Bool where instance : ToString Bool where toString := fun - | true => "_" - | false => "DEF" + | true => "❌" + | false => "✅" -#eval walker.num_nodes -example : walker.num_nodes = 2 := by { - simp -} - -#eval walker.vars.length -example : walker.vars.length = 0 := by { - simp -} - - ---attribute [df_simp] List.foldl ---attribute [df_simp] Vector.ofFn ---attribute [df_simp] Array.ofFn - -def 𝕐 : NKIWalker := ({ num_nodes := 1, last_node := 0, actions := fun x => VarAction.None, - edges := fun _ _ => false, breaks := [], conts := [], rets := [], - vars := [] } : NKIWalker).processStmtList - [{ - stmt := - Stmt'.assign - { expr := Expr'.var "x", - pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 2 } } - none - (some - { expr := Expr'.value (Value.int 0), - pos := { line := 2, column := 5, lineEnd := some 2, columnEnd := some 6 } }), - pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 6 } }, - { - stmt := - Stmt'.expr - { expr := Expr'.var "x", - pos := { line := 3, column := 1, lineEnd := some 3, columnEnd := some 2 } }, - pos := - { line := 3, column := 1, lineEnd := some 3, columnEnd := some 2 } }] - - -#eval 𝕐.num_nodes -example : 𝕐.num_nodes = 3:= by { - unfold 𝕐 - unfold NKIWalker.processStmtList - simp - -} - - -@[simp] +/- + perform dataflow analysis +-/ def 𝕏opt := (Solution (ρ:=Bool) (le_supl:=by trivial) @@ -396,105 +339,22 @@ def 𝕏opt := (Solution (num_nodes:=walker.num_nodes) (num_keys:=walker.vars.length) (edges:=walker.edges) - (transitions:=transitions)) - + (transitions:=transitions)).map (fun a ↦ {a with + key_labels k := walker.vars[k]? + }) #eval 𝕏opt -#synth (BEq (ℕ × Bool)) - ---theorem optsimp {α} (a : α) : (Option.some a).isSome := by simp - -theorem 𝕏present : 𝕏opt.isSome := by { - unfold 𝕏opt - unfold Solution - unfold FiniteDataflowProblem - unfold DataflowProblem.solve - dsimp only [] - unfold DataflowProblem.solve_to_depth - dsimp only [] - unfold ν₀ - unfold Δ - unfold Δ₀ - unfold is_fix - dsimp only [NodeMap.fold] - - - - unfold NodeMap.of_func NodeMap.fold NodeMap.app_unary NodeMap.get - dsimp - - - - - - unfold FiniteNodeMap - - let FNM := (FiniteNodeMap walker.num_nodes) - let F [NodeMap ℕ] [BEq (⟦ℕ, Bool⟧ × Bool)]:= fun a => ( - ⟪↦(⊥, true)⟫ fold⟪⟪↦(⊥, true)⟫map⟪fun x => x.fst⟫,fun a ν₀ => - if (⟪↦(⊥, true)⟫◃a).snd = true then ν₀⊔δ ⟪↦(⊥, true)⟫ a else ν₀⟫◃a, - (⟪↦(⊥, true)⟫◃a).fst - != - ⟪↦(⊥, true)⟫fold⟪⟪↦(⊥, true)⟫map⟪fun x => x.fst⟫,fun a ν₀ => - if (⟪↦(⊥, true)⟫◃a).snd = true then ν₀⊔δ ⟪↦(⊥, true)⟫ a else ν₀⟫◃a) - rw [F] - -} - - - -def 𝕏 := 𝕏opt.get 𝕏present - - - /-(by { - unfold Option.isSome - simp [df_simp] - - repeat unfold DataflowProblem.solve_to_depth - - - - unfold Option.isSome.match_1 Option.casesOn Option.rec - - simp [df_simp] - - - - })-/ -#eval! 𝕏 - -example : 𝕏.vals 2 0 (by {simp}) (by {}) = false - -theorem reads_valid - : ∀ n k, (hn: n < walker.num_nodes) → (hk: k < walker.vars.length) → - walker.actions n = VarAction.Read (walker.vars[k]) → 𝕏.vals n k hn hk := - fun n k hn hk h ↦ match n with - | 0 => sorry - | 1 => sorry - | 2 => sorry - | 3 => sorry - | 4 => sorry - | 5 => sorry - | 6 => sorry - | 7 => sorry - | 8 => sorry - | 9 => sorry - | 10 => sorry - | 11 => sorry - | n + 12 => sorry - - - - -structure Path where - nodes : List ℕ - nonempty : nodes ≠ [] - sound : ∀ i (_ : i < nodes.length - 1), walker.edges nodes[i] nodes[i+1] - -def Path.motive (path : Path) := - 𝕏.vals (path.nodes.getLast path.nonempty) - - match walker.actions (path.nodes.getLast path.nonempty) with - | VarAction.Read name => - ∃ i, i < path.nodes.length - 1 ∧ walker.actions i = VarAction.Read name - | _ => True +/- +Node 0: x:✅ cond0:✅ print:✅ y:✅ +Node 1: x:❌ cond0:❌ print:❌ y:❌ +Node 2: x:✅ cond0:❌ print:❌ y:❌ +Node 3: x:✅ cond0:❌ print:❌ y:❌ +Node 4: x:✅ cond0:❌ print:❌ y:❌ +Node 5: x:✅ cond0:❌ print:❌ y:❌ +Node 6: x:✅ cond0:❌ print:❌ y:✅ +Node 7: x:✅ cond0:❌ print:❌ y:✅ +Node 8: x:✅ cond0:❌ print:❌ y:❌ +Node 9: x:✅ cond0:❌ print:❌ y:❌ +Node 10: x:✅ cond0:❌ print:❌ y:❌ +Node 11: x:✅ cond0:❌ print:❌ y:❌ +-/ From 381cc46df03e4f8ddf2b5fe1140911270b72d5b8 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Fri, 18 Jul 2025 12:22:13 -0400 Subject: [PATCH 08/33] clean up add comments --- KLR/Compile/Dataflow.lean | 57 +++++++++++++++++------------------- KLR/Compile/NKIDataflow.lean | 13 ++++++++ 2 files changed, 40 insertions(+), 30 deletions(-) diff --git a/KLR/Compile/Dataflow.lean b/KLR/Compile/Dataflow.lean index 6212c6be..7d48ada8 100644 --- a/KLR/Compile/Dataflow.lean +++ b/KLR/Compile/Dataflow.lean @@ -96,7 +96,6 @@ 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 KLR.Compile.DFSimp -- sigh i shouldn't have to do this abbrev ℕ := Nat @@ -199,7 +198,7 @@ section Basics infix:100 "⊔" => Max.max - @[df_simp] + def NodeMap.instBEq {α β : Type} [NodeMap α] [BEq β] : BEq ⟦α, β⟧ := { beq μ₀ μ₁ := μ₀ fold⟪true, (fun a prev => prev ∧ (μ₀◃a == μ₁◃a))⟫ } @@ -254,8 +253,6 @@ section Basics simp } - --theorem NodeMap.of_func_map {α β γ: Type} [BEq β] [NodeMap α] (μ : ⟦α, β⟧) f (stt : γ) : μ fold⟪stt, f⟫ - instance {α β : Type} [NodeMap α] [ToString α] [ToString β] : ToString ⟦α, β⟧ where toString μ := μ fold⟪"", (fun nd repr => repr ++ "\n{" ++ toString nd.data ++ ": " ++ toString (μ◃nd) ++ "}")⟫ @@ -328,25 +325,25 @@ section DataflowProblemSolver variable {α β : Type} [BEq α] {DP: DataflowProblem α β} open DataflowProblem - @[df_simp] + def ν₀ : ⟦α, (β × Bool)⟧ := ⟪↦(⊥, true)⟫ - @[df_simp] + def ε (a₀ a₁ : Node α) : Bool := List.elem a₁ (σ◃a₀) - @[df_simp] + def strip_bools (ν : ⟦α, (β × Bool)⟧) := ν map⟪fun (β, _)=>β⟫ - @[df_simp] + def E (P : (Node α) → (Node α) → Prop) := ∀ (a₀ a₁) (_:ε a₀ a₁), P a₀ a₁ - @[df_simp] + def R (ν₀ : ⟦α, (β × Bool)⟧) (ν₁ : ⟦α, β⟧) [LE β]: Prop := E (fun a₀ a₁ => (ν₀◃a₀).2 ∨ (τ◃a₀) ((ν₀◃a₀).1) ≤ (ν₁◃a₁)) - @[df_simp] + def I (ν : ⟦α, (β × Bool)⟧) : Prop := R ν (strip_bools ν) - @[df_simp] + def R' (ν₀ ν₁ : ⟦α, β⟧) : Prop := E (fun a₀ a₁ => (τ◃a₀) (ν₀◃a₀) ≤ ν₁◃a₁) - @[df_simp] + def I' (ν : ⟦α, β⟧) : Prop := R' ν ν theorem base_case : @I α β _ DP ν₀ := by { @@ -357,21 +354,21 @@ section DataflowProblemSolver rw [NodeMap.of_const_get] } - @[df_simp] + def δ (ν : ⟦α, (β × Bool)⟧) (a : Node α) : ⟦α, β⟧ := -- step of_func⟪(fun a' => if ε a a' then ((τ◃a) (ν◃a).1) else ⊥)⟫ - @[df_simp] + def Δ₀ (ν : ⟦α, (β × Bool)⟧) : ⟦α, β⟧ := ν fold⟪ν map⟪(·.1)⟫, (fun a ν₀ => if (ν◃a).2 then ν₀ ⊔ (δ ν a) else ν₀)⟫ - @[df_simp] + def Δ (ν : ⟦α, (β × Bool)⟧) : ⟦α, (β × Bool)⟧ := let ν' := Δ₀ ν of_func⟪fun a => let (β, β') := ((ν◃a).1, (ν'◃a)); (β', β != β')⟫ - @[df_simp] + def is_fix (ν : ⟦α, (β × Bool)⟧) : Bool := ν map⟪fun x↦x.2⟫ == ⟪↦false⟫ @@ -571,7 +568,7 @@ section DataflowProblemSolver else solve_to_depth depth' DP ν' h' - @[df_simp] + def DataflowProblem.solve {α β : Type} [BEq α] (DP : DataflowProblem α β) : Option ((ν : ⟦α, β⟧) ×' I' ν) @@ -611,35 +608,35 @@ section FiniteDataflowProblemSolver le_supl (β₀ β₁ : β) : β₀ ≤ Max.max β₀ β₁ le_supr (β₀ β₁ : β) : β₁ ≤ Max.max β₀ β₁ - @[df_simp] + def LtProp : NodeProp ℕ where node_prop n' := n' < n - @[df_simp] + def NodeT := @Node ℕ (LtProp n) - @[df_simp] + def node_to_fin (nd : NodeT n) : (Fin n) := {val := @nd.data, isLt := @nd.sound} - @[df_simp] + def fin_to_node (fin : Fin n) : (NodeT n) := @Node.mk ℕ (LtProp n) fin.val fin.isLt - @[df_simp] + def nodes : Vector (NodeT n) n := Vector.ofFn (fin_to_node n) - @[df_simp] + def vector_fn {β : Type} (f : NodeT n → β) : Vector β n := Vector.ofFn (f ∘ (fin_to_node n)) - @[df_simp] + def FiniteNodeProp : NodeProp ℕ := { node_prop n' := n' < n } - @[df_simp] + def FiniteNodeMap : NodeMap ℕ := { FiniteNodeProp n with μ β := Vector β n @@ -731,7 +728,7 @@ section FiniteDataflowProblemSolver This is the end of the section because the returned instance provides the `DataflowProblem.solve` function. -/ - @[df_simp] + def FiniteDataflowProblem {β : Type} [BEq β] [P:Preorder β] @@ -893,7 +890,6 @@ section InnerMapImpl it allows significant code reuse and defines dataflowproblems with `β` equal to a map type minimally. -/ - @[df_simp] def FNM : NodeMap ℕ := (FiniteNodeMap num_keys) /- @@ -906,7 +902,6 @@ section InnerMapImpl proven properties of `⟦⬝, ⬝⟧` types. None are very surprising. -/ - @[df_simp] def FSI {_:NodeMap ℕ}: FiniteSolverInput (⟦ℕ, ρ⟧) := { num_nodes := num_nodes edges := edges @@ -976,7 +971,6 @@ section InnerMapImpl `Node ℕ` instances (of each `NodeMap ℕ` class!). None of these proofs are surprising. -/ - @[df_simp] def Solution : Option (SolutionT ρ num_nodes num_keys edges transitions) := let NMK : NodeMap ℕ := FNM num_keys let DP : DataflowProblem ℕ ⟦ℕ, ρ⟧ := FiniteDataflowProblem num_nodes @@ -1031,7 +1025,10 @@ section InnerMapImpl key_labels _ := none } end InnerMapImpl -/- + + +/- EXAMPLE + The section `ConcreteMapImpl` serves to illustrate an end-to-end usage of the dataflow solver defined above. In particular: diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index 0a3aaea0..e898061d 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -1,3 +1,16 @@ +/- +# NKI Dataflow + +This file uses the Dataflow solver (`InnerMapImpl.Solution`) from `Dataflow.lean` +to analyize NKI functions. + +For example, see `test_kernel` below, serialized NKI ASTs can be generated from `klr compile`, +converted to CFGs by the `NKIWalker` class below, +paired with definitions of variable well-definition corresponding to syntactic defs and uses, +and analyzed to get `𝕏opt : Option SolutionT`, which can be printed to view the liveness of +all variables at all program points `#eval 𝕏opt` +-/ + import KLR.NKI.Basic import KLR.Compile.Dataflow From 56201671ad4e8c051e3fdbbae4254458beba4931 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Fri, 18 Jul 2025 12:48:43 -0400 Subject: [PATCH 09/33] add sections --- KLR/Compile/NKIDataflow.lean | 700 ++++++++++++++++++----------------- 1 file changed, 356 insertions(+), 344 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index e898061d..96befea2 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -16,358 +16,370 @@ import KLR.Compile.Dataflow open KLR.NKI -inductive VarAction where - | Read (name : String) - | Write (name : String) (ty : Option Expr) - | None - -instance VarAction.toString : ToString VarAction where - toString := fun - | Read name => s!"Read({name})" - | Write name _ => s!"Write({name})" - | None => "None" - -@[simp] -def VarAction.var := fun - | Read name => some name - | Write name _ => some name - | None => none - -structure NKIWalker where - num_nodes : ℕ - last_node : ℕ - actions : ℕ → VarAction - edges : ℕ → ℕ → Bool - breaks : List ℕ - conts : List ℕ - rets : List ℕ - vars : List String --list of varnames seen - -instance NKIWalker.toString : ToString NKIWalker where - toString walker := - let row n := - let tgts := (List.range walker.num_nodes).filter (walker.edges n) - let num := if n = walker.last_node then s!"{n}[exit]" else s!"{n}" - s!"{num} {walker.actions n} ↦ {tgts}\n" - String.intercalate "\n" ((List.range walker.num_nodes).map row ++ ["vars: ", walker.vars.toString]) - -@[simp] -def NKIWalker.init : NKIWalker := { - num_nodes := 1 - last_node := 0 - actions _ := VarAction.None - edges _ _ := false - breaks := [] - conts := [] - rets := [] - vars := [] -} - -@[simp] -def NKIWalker.processAction (walker : NKIWalker) (action : VarAction) : NKIWalker := - let N := walker.num_nodes - {walker with - num_nodes := N + 1 - last_node := N - actions n := if n = N then action else walker.actions n - edges A B := (A, B) = (walker.last_node, N) - ∨ (walker.edges A B) - vars := match action.var with - | some var => if var ∈ walker.vars then walker.vars else walker.vars.concat var - | none => walker.vars +section DefVarAction + + inductive VarAction where + | Read (name : String) + | Write (name : String) (ty : Option Expr) + | None + + instance VarAction.toString : ToString VarAction where + toString := fun + | Read name => s!"Read({name})" + | Write name _ => s!"Write({name})" + | None => "None" + + @[simp] + def VarAction.var := fun + | Read name => some name + | Write name _ => some name + | None => none + +end DefVarAction + +section DefNKIWalker + + structure NKIWalker where + num_nodes : ℕ + last_node : ℕ + actions : ℕ → VarAction + edges : ℕ → ℕ → Bool + breaks : List ℕ + conts : List ℕ + rets : List ℕ + vars : List String --list of varnames seen + + instance NKIWalker.toString : ToString NKIWalker where + toString walker := + let row n := + let tgts := (List.range walker.num_nodes).filter (walker.edges n) + let num := if n = walker.last_node then s!"[{n} (exit)]" else s!"[{n}]" + s!"Node {num} : {walker.actions n} ↦ Nodes {tgts}\n" + String.intercalate "\n" ((List.range walker.num_nodes).map row ++ ["vars: ", walker.vars.toString]) + + @[simp] + def NKIWalker.init : NKIWalker := { + num_nodes := 1 + last_node := 0 + actions _ := VarAction.None + edges _ _ := false + breaks := [] + conts := [] + rets := [] + vars := [] } -@[simp] -def NKIWalker.setLast (walker : NKIWalker) (last_node : ℕ) : NKIWalker := {walker with - last_node := last_node -} - -@[simp] -def NKIWalker.addEdge (walker : NKIWalker) (a b : ℕ) : NKIWalker := {walker with - edges A B := (A, B) = (a, b) ∨ walker.edges A B -} - -@[simp] -def NKIWalker.addBreak (walker : NKIWalker) : NKIWalker := {walker with - breaks := walker.breaks ++ [walker.last_node] -} - -@[simp] -def NKIWalker.clearBreaks (walker : NKIWalker) : NKIWalker := {walker with - breaks := [] -} - -def NKIWalker.addContinue (walker : NKIWalker): NKIWalker := {walker with - conts := walker.conts ++ [walker.last_node] -} - -@[simp] -def NKIWalker.clearConts (walker : NKIWalker) : NKIWalker := {walker with - conts := [] -} - -@[simp] -def NKIWalker.addReturn (walker : NKIWalker) : NKIWalker := {walker with - rets := walker.rets ++ [walker.last_node] -} - -/-mutual -def NKIWalker.processExpr (walker : NKIWalker) (expr : Expr) : Nat := - match h : expr.expr with - | Expr'.tuple x => (walker.processExprList x).sum - | _ => 0 - termination_by sizeOf expr - decreasing_by cases expr; simp at h; rw [h]; simp; omega -def NKIWalker.processExprList (walker : NKIWalker) (exprs : List Expr) : List Nat := - exprs.map walker.processExpr - termination_by sizeOf exprs -end-/ - -mutual -@[simp] -def NKIWalker.processExpr (walker : NKIWalker) (expr : Expr) : NKIWalker := - let ⟨expr, _⟩ := expr - match _ : expr with - | Expr'.value _ => walker - | Expr'.var (name : String) => walker.processAction (VarAction.Read name) - | Expr'.proj (expr : Expr) _ => walker.processExpr expr - | Expr'.tuple (elements : List Expr) => walker.processExprList elements - | Expr'.access (expr : Expr) _ => walker.processExpr expr - | Expr'.binOp _ left right => (walker.processExpr left).processExpr right - | Expr'.ifExp test body orelse => - let body_walker := ((walker.processExpr test).processExpr body) - let orelse_walker := ((body_walker.setLast walker.last_node).processExpr orelse) - let complete_walker := (orelse_walker.processAction VarAction.None) - complete_walker.addEdge body_walker.last_node complete_walker.last_node - | Expr'.call (f: Expr) (args: List Expr) (_ : List Keyword) => - (walker.processExpr f).processExprList args - termination_by sizeOf expr - decreasing_by - all_goals { - try {rename_i expr' _<;> rcases h' : (expr, expr') with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega} - try {rcases h' : expr with ⟨⟨⟩, ⟨⟩⟩ <;> simp_all <;> omega} + @[simp] + def NKIWalker.processAction (walker : NKIWalker) (action : VarAction) : NKIWalker := + let N := walker.num_nodes + {walker with + num_nodes := N + 1 + last_node := N + actions n := if n = N then action else walker.actions n + edges A B := (A, B) = (walker.last_node, N) + ∨ (walker.edges A B) + vars := match action.var with + | some var => if var ∈ walker.vars then walker.vars else walker.vars.concat var + | none => walker.vars } -@[simp] -def NKIWalker.processExprList (walker : NKIWalker) (exprs : List Expr) : NKIWalker := - exprs.foldl NKIWalker.processExpr walker - termination_by sizeOf exprs -end - -mutual -@[simp] -def NKIWalker.processStmt (walker : NKIWalker) (stmt : Stmt) : NKIWalker := - let ⟨stmt, _⟩ := stmt - match _ : stmt with - | Stmt'.expr (e : Expr) => walker.processExpr e - | Stmt'.assert (e : Expr) => walker.processExpr e - | Stmt'.ret (e : Expr) => (walker.processExpr e).addReturn - | Stmt'.assign ⟨Expr'.var name, _⟩ (ty : Option Expr) (e : Option Expr) => - let withty := (match ty with | some ty => walker.processExpr ty | none => walker) - let withe := (match e with | some e => withty.processExpr e | none => withty) - withe.processAction (VarAction.Write name ty) - | Stmt'.assign _ (ty : Option Expr) (e : Option Expr) => - let withty := (match ty with | some ty => walker.processExpr ty | none => walker) - let withe := (match e with | some e => withty.processExpr e | none => withty) - withe.processAction (VarAction.Write "NONVAR" ty) - | Stmt'.ifStm (e : Expr) (thn : List Stmt) (els : List Stmt) => - let then_walker := (walker.processExpr e).processStmtList thn - let else_walker := (then_walker.setLast walker.last_node).processStmtList els - let complete := else_walker.processAction VarAction.None - complete.addEdge then_walker.last_node complete.last_node - | Stmt'.forLoop (x : Expr) (iter: Expr) (body: List Stmt) => - let intro_walker := (walker.processExpr x).processExpr iter - let outer_breaks := intro_walker.breaks - let outer_conts := intro_walker.conts - let inner_walker := ((intro_walker.clearBreaks).clearConts).processAction VarAction.None - let enter_node := inner_walker.last_node - let inner_walked := inner_walker.processStmtList body - let nearly_complete := (inner_walked.addEdge inner_walked.last_node enter_node).setLast enter_node - let complete := nearly_complete.processAction VarAction.None - let exit_node := complete.last_node - let with_conts := complete.conts.foldl (fun walker cont ↦ walker.addEdge cont enter_node) complete - let with_breaks := complete.breaks.foldl (fun walker brk ↦ walker.addEdge brk exit_node) with_conts - {with_breaks with - conts := outer_conts - breaks := outer_breaks - } - | Stmt'.breakLoop => (walker.processAction VarAction.None).addBreak - | Stmt'.continueLoop => (walker.processAction VarAction.None).addContinue - termination_by sizeOf stmt - decreasing_by - try rcases h : (thn, stmt) with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega - try rcases h : (els, stmt) with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega - try rcases h : (body, stmt) with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega - -@[simp] -def NKIWalker.processStmtList (walker : NKIWalker) (stmts : List Stmt) : NKIWalker := - stmts.foldl NKIWalker.processStmt walker - termination_by sizeOf stmts -end - -@[simp] -def NKIWalker.processFun (f : Fun) : NKIWalker := - let body_walker := (NKIWalker.init.processStmtList f.body).processAction VarAction.None - body_walker.rets.foldl (fun walker ret ↦ walker.addEdge ret body_walker.last_node) body_walker - -@[simp] -def NKIWalker.isClosed (walker : NKIWalker) := walker.breaks.isEmpty ∧ walker.conts.isEmpty - -/- -file test.py: -def test(): - x = 0 - if cond0: - print(x) - else: - y = 0 - print(y) - print(y) - -bash: `klr compile test.py` yields the following serialization of a NKI Kernel --/ -@[simp] -def test_kernel : Kernel := { - entry := "test.test", - funs := [{ name := "test.test", - file := "unknown", - line := 1, - body := [{ stmt := KLR.NKI.Stmt'.assign - { expr := KLR.NKI.Expr'.var "x", - pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 2 } } - none - (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), - pos := { line := 2, column := 5, lineEnd := some 2, columnEnd := some 6 } }), - pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 6 } }, - { stmt := KLR.NKI.Stmt'.ifStm - { expr := KLR.NKI.Expr'.var "cond0", - pos := { line := 3, column := 4, lineEnd := some 3, columnEnd := some 9 } } - [{ stmt := KLR.NKI.Stmt'.expr - { expr := KLR.NKI.Expr'.call - { expr := KLR.NKI.Expr'.var "print", - pos := { line := 4, - column := 2, - lineEnd := some 4, - columnEnd := some 7 } } - [{ expr := KLR.NKI.Expr'.var "x", - pos := { line := 4, - column := 8, - lineEnd := some 4, - columnEnd := some 9 } }] - [], - pos := { line := 4, - column := 2, - lineEnd := some 4, - columnEnd := some 10 } }, - pos := { line := 4, column := 2, lineEnd := some 4, columnEnd := some 10 } }] - [{ stmt := KLR.NKI.Stmt'.assign - { expr := KLR.NKI.Expr'.var "y", - pos := { line := 6, - column := 2, - lineEnd := some 6, - columnEnd := some 3 } } - none - (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), - pos := { line := 6, - column := 6, - lineEnd := some 6, - columnEnd := some 7 } }), - pos := { line := 6, column := 2, lineEnd := some 6, columnEnd := some 7 } }, - { stmt := KLR.NKI.Stmt'.expr - { expr := KLR.NKI.Expr'.call - { expr := KLR.NKI.Expr'.var "print", - pos := { line := 7, - column := 2, - lineEnd := some 7, - columnEnd := some 7 } } - [{ expr := KLR.NKI.Expr'.var "y", - pos := { line := 7, - column := 8, - lineEnd := some 7, - columnEnd := some 9 } }] - [], - pos := { line := 7, - column := 2, - lineEnd := some 7, - columnEnd := some 10 } }, - pos := { line := 7, column := 2, lineEnd := some 7, columnEnd := some 10 } }], - pos := { line := 3, column := 1, lineEnd := some 7, columnEnd := some 10 } }, - { stmt := KLR.NKI.Stmt'.expr - { expr := KLR.NKI.Expr'.call - { expr := KLR.NKI.Expr'.var "print", - pos := { line := 8, - column := 1, - lineEnd := some 8, - columnEnd := some 6 } } - [{ expr := KLR.NKI.Expr'.var "y", - pos := { line := 8, - column := 7, - lineEnd := some 8, - columnEnd := some 8 } }] - [], - pos := { line := 8, column := 1, lineEnd := some 8, columnEnd := some 9 } }, - pos := { line := 8, column := 1, lineEnd := some 8, columnEnd := some 9 } }], - args := [] }], - args := [], - globals := [] } + @[simp] + def NKIWalker.setLast (walker : NKIWalker) (last_node : ℕ) : NKIWalker := {walker with + last_node := last_node + } -/- - Perform the walk of the AST, converting it into a CFG --/ -def walker := NKIWalker.processFun test_kernel.funs[0] -#eval walker + @[simp] + def NKIWalker.addEdge (walker : NKIWalker) (a b : ℕ) : NKIWalker := {walker with + edges A B := (A, B) = (a, b) ∨ walker.edges A B + } -/- - extract the transitions from the walker --/ -def transitions (n k : ℕ) (pre : Bool) : Bool := - (n = 0) ∨ - if _ : k < walker.vars.length then - match walker.actions n with - | VarAction.Write name _ => ¬ (name = walker.vars[k]) ∧ pre - | _ => pre - else - pre + @[simp] + def NKIWalker.addBreak (walker : NKIWalker) : NKIWalker := {walker with + breaks := walker.breaks ++ [walker.last_node] + } -instance : Preorder Bool where - le_refl := by trivial - le_trans := by trivial + @[simp] + def NKIWalker.clearBreaks (walker : NKIWalker) : NKIWalker := {walker with + breaks := [] + } -instance : HasBot Bool where - bot := false + def NKIWalker.addContinue (walker : NKIWalker): NKIWalker := {walker with + conts := walker.conts ++ [walker.last_node] + } -instance : ToString Bool where - toString := fun - | true => "❌" - | false => "✅" + @[simp] + def NKIWalker.clearConts (walker : NKIWalker) : NKIWalker := {walker with + conts := [] + } + @[simp] + def NKIWalker.addReturn (walker : NKIWalker) : NKIWalker := {walker with + rets := walker.rets ++ [walker.last_node] + } -/- - perform dataflow analysis --/ -def 𝕏opt := (Solution - (ρ:=Bool) - (le_supl:=by trivial) - (le_supr:=by trivial) - (num_nodes:=walker.num_nodes) - (num_keys:=walker.vars.length) - (edges:=walker.edges) - (transitions:=transitions)).map (fun a ↦ {a with - key_labels k := walker.vars[k]? - }) - -#eval 𝕏opt -/- -Node 0: x:✅ cond0:✅ print:✅ y:✅ -Node 1: x:❌ cond0:❌ print:❌ y:❌ -Node 2: x:✅ cond0:❌ print:❌ y:❌ -Node 3: x:✅ cond0:❌ print:❌ y:❌ -Node 4: x:✅ cond0:❌ print:❌ y:❌ -Node 5: x:✅ cond0:❌ print:❌ y:❌ -Node 6: x:✅ cond0:❌ print:❌ y:✅ -Node 7: x:✅ cond0:❌ print:❌ y:✅ -Node 8: x:✅ cond0:❌ print:❌ y:❌ -Node 9: x:✅ cond0:❌ print:❌ y:❌ -Node 10: x:✅ cond0:❌ print:❌ y:❌ -Node 11: x:✅ cond0:❌ print:❌ y:❌ --/ + /-mutual + def NKIWalker.processExpr (walker : NKIWalker) (expr : Expr) : Nat := + match h : expr.expr with + | Expr'.tuple x => (walker.processExprList x).sum + | _ => 0 + termination_by sizeOf expr + decreasing_by cases expr; simp at h; rw [h]; simp; omega + def NKIWalker.processExprList (walker : NKIWalker) (exprs : List Expr) : List Nat := + exprs.map walker.processExpr + termination_by sizeOf exprs + end-/ + + mutual + @[simp] + def NKIWalker.processExpr (walker : NKIWalker) (expr : Expr) : NKIWalker := + let ⟨expr, _⟩ := expr + match _ : expr with + | Expr'.value _ => walker + | Expr'.var (name : String) => walker.processAction (VarAction.Read name) + | Expr'.proj (expr : Expr) _ => walker.processExpr expr + | Expr'.tuple (elements : List Expr) => walker.processExprList elements + | Expr'.access (expr : Expr) _ => walker.processExpr expr + | Expr'.binOp _ left right => (walker.processExpr left).processExpr right + | Expr'.ifExp test body orelse => + let body_walker := ((walker.processExpr test).processExpr body) + let orelse_walker := ((body_walker.setLast walker.last_node).processExpr orelse) + let complete_walker := (orelse_walker.processAction VarAction.None) + complete_walker.addEdge body_walker.last_node complete_walker.last_node + | Expr'.call (f: Expr) (args: List Expr) (_ : List Keyword) => + (walker.processExpr f).processExprList args + termination_by sizeOf expr + decreasing_by + all_goals { + try {rename_i expr' _<;> rcases h' : (expr, expr') with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega} + try {rcases h' : expr with ⟨⟨⟩, ⟨⟩⟩ <;> simp_all <;> omega} + } + + @[simp] + def NKIWalker.processExprList (walker : NKIWalker) (exprs : List Expr) : NKIWalker := + exprs.foldl NKIWalker.processExpr walker + termination_by sizeOf exprs + end + + mutual + @[simp] + def NKIWalker.processStmt (walker : NKIWalker) (stmt : Stmt) : NKIWalker := + let ⟨stmt, _⟩ := stmt + match _ : stmt with + | Stmt'.expr (e : Expr) => walker.processExpr e + | Stmt'.assert (e : Expr) => walker.processExpr e + | Stmt'.ret (e : Expr) => (walker.processExpr e).addReturn + | Stmt'.assign ⟨Expr'.var name, _⟩ (ty : Option Expr) (e : Option Expr) => + let withty := (match ty with | some ty => walker.processExpr ty | none => walker) + let withe := (match e with | some e => withty.processExpr e | none => withty) + withe.processAction (VarAction.Write name ty) + | Stmt'.assign _ (ty : Option Expr) (e : Option Expr) => + let withty := (match ty with | some ty => walker.processExpr ty | none => walker) + let withe := (match e with | some e => withty.processExpr e | none => withty) + withe.processAction (VarAction.Write "NONVAR" ty) + | Stmt'.ifStm (e : Expr) (thn : List Stmt) (els : List Stmt) => + let then_walker := (walker.processExpr e).processStmtList thn + let else_walker := (then_walker.setLast walker.last_node).processStmtList els + let complete := else_walker.processAction VarAction.None + complete.addEdge then_walker.last_node complete.last_node + | Stmt'.forLoop (x : Expr) (iter: Expr) (body: List Stmt) => + let intro_walker := (walker.processExpr x).processExpr iter + let outer_breaks := intro_walker.breaks + let outer_conts := intro_walker.conts + let inner_walker := ((intro_walker.clearBreaks).clearConts).processAction VarAction.None + let enter_node := inner_walker.last_node + let inner_walked := inner_walker.processStmtList body + let nearly_complete := (inner_walked.addEdge inner_walked.last_node enter_node).setLast enter_node + let complete := nearly_complete.processAction VarAction.None + let exit_node := complete.last_node + let with_conts := complete.conts.foldl (fun walker cont ↦ walker.addEdge cont enter_node) complete + let with_breaks := complete.breaks.foldl (fun walker brk ↦ walker.addEdge brk exit_node) with_conts + {with_breaks with + conts := outer_conts + breaks := outer_breaks + } + | Stmt'.breakLoop => (walker.processAction VarAction.None).addBreak + | Stmt'.continueLoop => (walker.processAction VarAction.None).addContinue + termination_by sizeOf stmt + decreasing_by + try rcases h : (thn, stmt) with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega + try rcases h : (els, stmt) with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega + try rcases h : (body, stmt) with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega + + @[simp] + def NKIWalker.processStmtList (walker : NKIWalker) (stmts : List Stmt) : NKIWalker := + stmts.foldl NKIWalker.processStmt walker + termination_by sizeOf stmts + end + + @[simp] + def NKIWalker.processFun (f : Fun) : NKIWalker := + let body_walker := (NKIWalker.init.processStmtList f.body).processAction VarAction.None + body_walker.rets.foldl (fun walker ret ↦ walker.addEdge ret body_walker.last_node) body_walker + + @[simp] + def NKIWalker.isClosed (walker : NKIWalker) := walker.breaks.isEmpty ∧ walker.conts.isEmpty + +end DefNKIWalker + +section Test + + /- + file test.py: + def test(): + x = 0 + if cond0: + print(x) + else: + y = 0 + print(y) + print(y) + + bash: `klr compile test.py` yields the following serialization of a NKI Kernel + -/ + @[simp] + def test_kernel : Kernel := { + entry := "test.test", + funs := [{ name := "test.test", + file := "unknown", + line := 1, + body := [{ stmt := KLR.NKI.Stmt'.assign + { expr := KLR.NKI.Expr'.var "x", + pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 2 } } + none + (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 2, column := 5, lineEnd := some 2, columnEnd := some 6 } }), + pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 6 } }, + { stmt := KLR.NKI.Stmt'.ifStm + { expr := KLR.NKI.Expr'.var "cond0", + pos := { line := 3, column := 4, lineEnd := some 3, columnEnd := some 9 } } + [{ stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "print", + pos := { line := 4, + column := 2, + lineEnd := some 4, + columnEnd := some 7 } } + [{ expr := KLR.NKI.Expr'.var "x", + pos := { line := 4, + column := 8, + lineEnd := some 4, + columnEnd := some 9 } }] + [], + pos := { line := 4, + column := 2, + lineEnd := some 4, + columnEnd := some 10 } }, + pos := { line := 4, column := 2, lineEnd := some 4, columnEnd := some 10 } }] + [{ stmt := KLR.NKI.Stmt'.assign + { expr := KLR.NKI.Expr'.var "y", + pos := { line := 6, + column := 2, + lineEnd := some 6, + columnEnd := some 3 } } + none + (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 6, + column := 6, + lineEnd := some 6, + columnEnd := some 7 } }), + pos := { line := 6, column := 2, lineEnd := some 6, columnEnd := some 7 } }, + { stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "print", + pos := { line := 7, + column := 2, + lineEnd := some 7, + columnEnd := some 7 } } + [{ expr := KLR.NKI.Expr'.var "y", + pos := { line := 7, + column := 8, + lineEnd := some 7, + columnEnd := some 9 } }] + [], + pos := { line := 7, + column := 2, + lineEnd := some 7, + columnEnd := some 10 } }, + pos := { line := 7, column := 2, lineEnd := some 7, columnEnd := some 10 } }], + pos := { line := 3, column := 1, lineEnd := some 7, columnEnd := some 10 } }, + { stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "print", + pos := { line := 8, + column := 1, + lineEnd := some 8, + columnEnd := some 6 } } + [{ expr := KLR.NKI.Expr'.var "y", + pos := { line := 8, + column := 7, + lineEnd := some 8, + columnEnd := some 8 } }] + [], + pos := { line := 8, column := 1, lineEnd := some 8, columnEnd := some 9 } }, + pos := { line := 8, column := 1, lineEnd := some 8, columnEnd := some 9 } }], + args := [] }], + args := [], + globals := [] } + + /- + Perform the walk of the AST, converting it into a CFG + -/ + def walker := NKIWalker.processFun test_kernel.funs[0] + #eval walker + + /- + extract the transitions from the walker + -/ + def transitions (n k : ℕ) (pre : Bool) : Bool := + (n = 0) ∨ + if _ : k < walker.vars.length then + match walker.actions n with + | VarAction.Write name _ => ¬ (name = walker.vars[k]) ∧ pre + | _ => pre + else + pre + + instance : Preorder Bool where + le_refl := by trivial + le_trans := by trivial + + instance : HasBot Bool where + bot := false + + instance : ToString Bool where + toString := fun + | true => "❌" + | false => "✅" + + + /- + perform dataflow analysis + -/ + def 𝕏opt := (Solution + (ρ:=Bool) + (le_supl:=by trivial) + (le_supr:=by trivial) + (num_nodes:=walker.num_nodes) + (num_keys:=walker.vars.length) + (edges:=walker.edges) + (transitions:=transitions)).map (fun a ↦ {a with + key_labels k := walker.vars[k]? + }) + + #eval 𝕏opt + /- + Node 0: x:✅ cond0:✅ print:✅ y:✅ + Node 1: x:❌ cond0:❌ print:❌ y:❌ + Node 2: x:✅ cond0:❌ print:❌ y:❌ + Node 3: x:✅ cond0:❌ print:❌ y:❌ + Node 4: x:✅ cond0:❌ print:❌ y:❌ + Node 5: x:✅ cond0:❌ print:❌ y:❌ + Node 6: x:✅ cond0:❌ print:❌ y:✅ + Node 7: x:✅ cond0:❌ print:❌ y:✅ + Node 8: x:✅ cond0:❌ print:❌ y:❌ + Node 9: x:✅ cond0:❌ print:❌ y:❌ + Node 10: x:✅ cond0:❌ print:❌ y:❌ + Node 11: x:✅ cond0:❌ print:❌ y:❌ + -/ + +end Test From 8f51c8da8f61ad34edff66f27edebb1614ba0d8d Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Fri, 18 Jul 2025 12:50:38 -0400 Subject: [PATCH 10/33] clean up --- KLR/Compile/NKIDataflow.lean | 48 +++++++++++++++++------------------- 1 file changed, 23 insertions(+), 25 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index 96befea2..a68b8ea3 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -29,7 +29,6 @@ section DefVarAction | Write name _ => s!"Write({name})" | None => "None" - @[simp] def VarAction.var := fun | Read name => some name | Write name _ => some name @@ -57,7 +56,6 @@ section DefNKIWalker s!"Node {num} : {walker.actions n} ↦ Nodes {tgts}\n" String.intercalate "\n" ((List.range walker.num_nodes).map row ++ ["vars: ", walker.vars.toString]) - @[simp] def NKIWalker.init : NKIWalker := { num_nodes := 1 last_node := 0 @@ -69,7 +67,7 @@ section DefNKIWalker vars := [] } - @[simp] + def NKIWalker.processAction (walker : NKIWalker) (action : VarAction) : NKIWalker := let N := walker.num_nodes {walker with @@ -83,22 +81,22 @@ section DefNKIWalker | none => walker.vars } - @[simp] + def NKIWalker.setLast (walker : NKIWalker) (last_node : ℕ) : NKIWalker := {walker with last_node := last_node } - @[simp] + def NKIWalker.addEdge (walker : NKIWalker) (a b : ℕ) : NKIWalker := {walker with edges A B := (A, B) = (a, b) ∨ walker.edges A B } - @[simp] + def NKIWalker.addBreak (walker : NKIWalker) : NKIWalker := {walker with breaks := walker.breaks ++ [walker.last_node] } - @[simp] + def NKIWalker.clearBreaks (walker : NKIWalker) : NKIWalker := {walker with breaks := [] } @@ -107,12 +105,12 @@ section DefNKIWalker conts := walker.conts ++ [walker.last_node] } - @[simp] + def NKIWalker.clearConts (walker : NKIWalker) : NKIWalker := {walker with conts := [] } - @[simp] + def NKIWalker.addReturn (walker : NKIWalker) : NKIWalker := {walker with rets := walker.rets ++ [walker.last_node] } @@ -130,7 +128,7 @@ section DefNKIWalker end-/ mutual - @[simp] + def NKIWalker.processExpr (walker : NKIWalker) (expr : Expr) : NKIWalker := let ⟨expr, _⟩ := expr match _ : expr with @@ -154,14 +152,14 @@ section DefNKIWalker try {rcases h' : expr with ⟨⟨⟩, ⟨⟩⟩ <;> simp_all <;> omega} } - @[simp] + def NKIWalker.processExprList (walker : NKIWalker) (exprs : List Expr) : NKIWalker := exprs.foldl NKIWalker.processExpr walker termination_by sizeOf exprs end mutual - @[simp] + def NKIWalker.processStmt (walker : NKIWalker) (stmt : Stmt) : NKIWalker := let ⟨stmt, _⟩ := stmt match _ : stmt with @@ -205,18 +203,18 @@ section DefNKIWalker try rcases h : (els, stmt) with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega try rcases h : (body, stmt) with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega - @[simp] + def NKIWalker.processStmtList (walker : NKIWalker) (stmts : List Stmt) : NKIWalker := stmts.foldl NKIWalker.processStmt walker termination_by sizeOf stmts end - @[simp] + def NKIWalker.processFun (f : Fun) : NKIWalker := let body_walker := (NKIWalker.init.processStmtList f.body).processAction VarAction.None body_walker.rets.foldl (fun walker ret ↦ walker.addEdge ret body_walker.last_node) body_walker - @[simp] + def NKIWalker.isClosed (walker : NKIWalker) := walker.breaks.isEmpty ∧ walker.conts.isEmpty end DefNKIWalker @@ -236,10 +234,10 @@ section Test bash: `klr compile test.py` yields the following serialization of a NKI Kernel -/ - @[simp] + def test_kernel : Kernel := { entry := "test.test", - funs := [{ name := "test.test", + funs := [{name := "test.test", file := "unknown", line := 1, body := [{ stmt := KLR.NKI.Stmt'.assign @@ -252,7 +250,7 @@ section Test { stmt := KLR.NKI.Stmt'.ifStm { expr := KLR.NKI.Expr'.var "cond0", pos := { line := 3, column := 4, lineEnd := some 3, columnEnd := some 9 } } - [{ stmt := KLR.NKI.Stmt'.expr + [{stmt := KLR.NKI.Stmt'.expr { expr := KLR.NKI.Expr'.call { expr := KLR.NKI.Expr'.var "print", pos := { line := 4, @@ -260,7 +258,7 @@ section Test lineEnd := some 4, columnEnd := some 7 } } [{ expr := KLR.NKI.Expr'.var "x", - pos := { line := 4, + pos := {line := 4, column := 8, lineEnd := some 4, columnEnd := some 9 } }] @@ -269,8 +267,8 @@ section Test column := 2, lineEnd := some 4, columnEnd := some 10 } }, - pos := { line := 4, column := 2, lineEnd := some 4, columnEnd := some 10 } }] - [{ stmt := KLR.NKI.Stmt'.assign + pos := {line := 4, column := 2, lineEnd := some 4, columnEnd := some 10 } }] + [{stmt := KLR.NKI.Stmt'.assign { expr := KLR.NKI.Expr'.var "y", pos := { line := 6, column := 2, @@ -291,7 +289,7 @@ section Test lineEnd := some 7, columnEnd := some 7 } } [{ expr := KLR.NKI.Expr'.var "y", - pos := { line := 7, + pos := {line := 7, column := 8, lineEnd := some 7, columnEnd := some 9 } }] @@ -305,12 +303,12 @@ section Test { stmt := KLR.NKI.Stmt'.expr { expr := KLR.NKI.Expr'.call { expr := KLR.NKI.Expr'.var "print", - pos := { line := 8, + pos := {line := 8, column := 1, lineEnd := some 8, columnEnd := some 6 } } - [{ expr := KLR.NKI.Expr'.var "y", - pos := { line := 8, + [{expr := KLR.NKI.Expr'.var "y", + pos := {line := 8, column := 7, lineEnd := some 8, columnEnd := some 8 } }] From 74c6ad98c76bc469a7d1fa586468eced6d3772d1 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Fri, 18 Jul 2025 14:45:06 -0400 Subject: [PATCH 11/33] yay. add correctness condition --- KLR/Compile/NKIDataflow.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index a68b8ea3..9c4bab3a 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -67,6 +67,20 @@ section DefNKIWalker vars := [] } + structure NKIWalker.Path (walker : NKIWalker) where + nodes : List ℕ -- head of `nodes` is end of path + + def NKIWalker.Path.writes (walker : NKIWalker) (path : NKIWalker.Path walker) (name : String) : Bool := + path.nodes.any (match walker.actions · with | VarAction.Write name' _ => name = name' | _ => false) + + def NKIWalker.Path.reads (walker : NKIWalker) (path : NKIWalker.Path walker) (name : String) : Bool := + match path with + | ⟨List.cons n _⟩ => match walker.actions n with | VarAction.Read name' => name = name' | _ => false + | _ => false + + -- proving (or failing to prove) this is the goal!! + def NKIWalker.sound (walker : NKIWalker) : Prop := + ∀ (path : walker.Path) (name : String), (path.reads walker name) → (path.writes walker name) def NKIWalker.processAction (walker : NKIWalker) (action : VarAction) : NKIWalker := let N := walker.num_nodes From 69696bc7178d752dea1ba33fb886e1d5f253b3e9 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Fri, 18 Jul 2025 20:45:23 -0400 Subject: [PATCH 12/33] Build out path structure --- KLR/Compile/NKIDataflow.lean | 73 ++++++++++++++++++++++++++++++++---- 1 file changed, 66 insertions(+), 7 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index 9c4bab3a..6b404d42 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -67,20 +67,33 @@ section DefNKIWalker vars := [] } + def NKIWalker.Node (walker : NKIWalker) : Type := Fin (walker.num_nodes) + + def NKIWalker.isPath (walker : NKIWalker) : List walker.Node → Prop := fun + | [] => True + | [n] => walker.edges 0 n.val + | n₁ :: n₀ :: tl => walker.isPath (n₀ :: tl) ∧ (walker.edges n₀.val n₁.val) + structure NKIWalker.Path (walker : NKIWalker) where - nodes : List ℕ -- head of `nodes` is end of path + nodes : List walker.Node + nodes_sound : walker.isPath nodes - def NKIWalker.Path.writes (walker : NKIWalker) (path : NKIWalker.Path walker) (name : String) : Bool := - path.nodes.any (match walker.actions · with | VarAction.Write name' _ => name = name' | _ => false) + def NKIWalker.Path.writes (walker : NKIWalker) (𝕡 : walker.Path) (name : String) : Bool := + 𝕡.nodes.any (fun n ↦ match walker.actions n.val with + | VarAction.Write name' _ => name = name' + | _ => false) - def NKIWalker.Path.reads (walker : NKIWalker) (path : NKIWalker.Path walker) (name : String) : Bool := - match path with - | ⟨List.cons n _⟩ => match walker.actions n with | VarAction.Read name' => name = name' | _ => false + def NKIWalker.Path.terminal_is (walker : NKIWalker) (𝕡 : walker.Path) (motive : walker.Node → Bool) : Bool := + match 𝕡.nodes with + | n :: _ => motive n | _ => false + def NKIWalker.Path.reads_terminal (walker : NKIWalker) (𝕡 : walker.Path) (name : String) : Bool := + 𝕡.terminal_is walker (fun ⟨n, _⟩ ↦ match walker.actions n with | VarAction.Read name' => name = name' | _ => false) + -- proving (or failing to prove) this is the goal!! def NKIWalker.sound (walker : NKIWalker) : Prop := - ∀ (path : walker.Path) (name : String), (path.reads walker name) → (path.writes walker name) + ∀ (𝕡 : walker.Path) (name : String), (𝕡.reads_terminal walker name) → (𝕡.writes walker name) def NKIWalker.processAction (walker : NKIWalker) (action : VarAction) : NKIWalker := let N := walker.num_nodes @@ -394,4 +407,50 @@ section Test Node 11: x:✅ cond0:❌ print:❌ y:❌ -/ + variable (h𝕏 : 𝕏opt.isSome) + + def 𝕏 := 𝕏opt.get h𝕏 + def ν := (𝕏 h𝕏).vals + def σ := (𝕏 h𝕏).props + def ℙ := walker.Path + + #check ν + #check σ + + def NKIWalker.Var : Type := Fin (walker.vars.length) + + def NKIWalker.Path.def_terminal (𝕡 : walker.Path) (v : NKIWalker.Var) : Bool := + let ⟨k, hk⟩ := v + 𝕡.terminal_is walker (fun ⟨n, hn⟩ ↦ ν h𝕏 n k hn hk) + + def ℍ : ∀ (𝕡 : ℙ) (v : NKIWalker.Var), + let ⟨k, hk⟩ := v + let kvar : String := walker.vars[k]'hk + (𝕡.def_terminal h𝕏 v) → (𝕡.writes walker kvar) + := by { + sorry + } + + def 𝕀 : ∀ (𝕡 : ℙ) (v : NKIWalker.Var), + let ⟨k, hk⟩ := v + let kvar : String := walker.vars[k]'hk + (𝕡.reads_terminal walker kvar) → (𝕡.def_terminal h𝕏 v) + := by { + sorry + } + + -- yay! + def 𝕁 : walker.sound := by { + sorry + } + + +/- + match 𝕡.nodes.head? with + | some hd => if hhd : hd < walker.num_nodes + then @ν h𝕏 hd k hhd hk → 𝕡.writes walker kvar + else False + | none => True + := sorry-/ + end Test From 711a50f65fafcca255b4a75ee764ccc1c0d282f0 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Fri, 18 Jul 2025 21:08:15 -0400 Subject: [PATCH 13/33] well-def checker reduced to two sorry's! --- KLR/Compile/NKIDataflow.lean | 48 +++++++++++++++++++++--------------- 1 file changed, 28 insertions(+), 20 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index 6b404d42..c7041c8d 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -68,6 +68,17 @@ section DefNKIWalker } def NKIWalker.Node (walker : NKIWalker) : Type := Fin (walker.num_nodes) + def NKIWalker.Var (walker : NKIWalker) : Type := Fin (walker.vars.length) + + def NKIWalker.reads (walker : NKIWalker) (n : walker.Node) (v : walker.Var) : Bool := + match walker.actions n.val with + | VarAction.Read name => name = walker.vars.get v + | _ => false + + def NKIWalker.writes (walker : NKIWalker) (n : walker.Node) (v : walker.Var) : Bool := + match walker.actions n.val with + | VarAction.Write name _ => name = walker.vars.get v + | _ => false def NKIWalker.isPath (walker : NKIWalker) : List walker.Node → Prop := fun | [] => True @@ -78,22 +89,20 @@ section DefNKIWalker nodes : List walker.Node nodes_sound : walker.isPath nodes - def NKIWalker.Path.writes (walker : NKIWalker) (𝕡 : walker.Path) (name : String) : Bool := - 𝕡.nodes.any (fun n ↦ match walker.actions n.val with - | VarAction.Write name' _ => name = name' - | _ => false) + def NKIWalker.Path.writes (walker : NKIWalker) (𝕡 : walker.Path) (v : walker.Var) : Bool := + 𝕡.nodes.any (walker.writes . v) def NKIWalker.Path.terminal_is (walker : NKIWalker) (𝕡 : walker.Path) (motive : walker.Node → Bool) : Bool := match 𝕡.nodes with | n :: _ => motive n | _ => false - def NKIWalker.Path.reads_terminal (walker : NKIWalker) (𝕡 : walker.Path) (name : String) : Bool := - 𝕡.terminal_is walker (fun ⟨n, _⟩ ↦ match walker.actions n with | VarAction.Read name' => name = name' | _ => false) + def NKIWalker.Path.reads_terminal (walker : NKIWalker) (𝕡 : walker.Path) (v : walker.Var) : Bool := + 𝕡.terminal_is walker (walker.reads . v) -- proving (or failing to prove) this is the goal!! def NKIWalker.sound (walker : NKIWalker) : Prop := - ∀ (𝕡 : walker.Path) (name : String), (𝕡.reads_terminal walker name) → (𝕡.writes walker name) + ∀ (𝕡 : walker.Path) v, (𝕡.reads_terminal walker v) → (𝕡.writes walker v) def NKIWalker.processAction (walker : NKIWalker) (action : VarAction) : NKIWalker := let N := walker.num_nodes @@ -417,31 +426,30 @@ section Test #check ν #check σ - def NKIWalker.Var : Type := Fin (walker.vars.length) - def NKIWalker.Path.def_terminal (𝕡 : walker.Path) (v : NKIWalker.Var) : Bool := + + def NKIWalker.Path.def_terminal (𝕡 : walker.Path) (v : walker.Var) : Bool := let ⟨k, hk⟩ := v 𝕡.terminal_is walker (fun ⟨n, hn⟩ ↦ ν h𝕏 n k hn hk) - def ℍ : ∀ (𝕡 : ℙ) (v : NKIWalker.Var), - let ⟨k, hk⟩ := v - let kvar : String := walker.vars[k]'hk - (𝕡.def_terminal h𝕏 v) → (𝕡.writes walker kvar) + def ℍ : ∀ (𝕡 : ℙ) v, (𝕡.def_terminal h𝕏 v) → (𝕡.writes walker v) := by { - sorry + sorry -- proof by induction on 𝕡, "the hard part" } - def 𝕀 : ∀ (𝕡 : ℙ) (v : NKIWalker.Var), - let ⟨k, hk⟩ := v - let kvar : String := walker.vars[k]'hk - (𝕡.reads_terminal walker kvar) → (𝕡.def_terminal h𝕏 v) + def 𝕀 : ∀ (𝕡 : ℙ) v, (𝕡.reads_terminal walker v) → (𝕡.def_terminal h𝕏 v) := by { - sorry + sorry -- proof by relying an an easily computable hypothesis (abstracted as a var to prove this goal) } -- yay! def 𝕁 : walker.sound := by { - sorry + unfold NKIWalker.sound + intro 𝕡 name reads + apply ℍ + apply 𝕀 + assumption + assumption } From 52d2fe6f4af03640027679a5dff63cc185715fc8 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Fri, 18 Jul 2025 22:42:07 -0400 Subject: [PATCH 14/33] remove comment --- KLR/Compile/NKIDataflow.lean | 9 --------- 1 file changed, 9 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index c7041c8d..81b9273a 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -452,13 +452,4 @@ section Test assumption } - -/- - match 𝕡.nodes.head? with - | some hd => if hhd : hd < walker.num_nodes - then @ν h𝕏 hd k hhd hk → 𝕡.writes walker kvar - else False - | none => True - := sorry-/ - end Test From 929a95db131989395ec5e972cbfd94c255376294 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Sat, 19 Jul 2025 16:32:25 -0400 Subject: [PATCH 15/33] progress on final proof --- KLR/Compile/NKIDataflow.lean | 98 ++++++++++++++++++++++++++++++------ 1 file changed, 84 insertions(+), 14 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index 81b9273a..20060e7f 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -40,6 +40,7 @@ section DefNKIWalker structure NKIWalker where num_nodes : ℕ + num_nodes_nonzero : num_nodes > 0 last_node : ℕ actions : ℕ → VarAction edges : ℕ → ℕ → Bool @@ -58,6 +59,7 @@ section DefNKIWalker def NKIWalker.init : NKIWalker := { num_nodes := 1 + num_nodes_nonzero := by trivial last_node := 0 actions _ := VarAction.None edges _ _ := false @@ -75,12 +77,13 @@ section DefNKIWalker | VarAction.Read name => name = walker.vars.get v | _ => false + @[simp] def NKIWalker.writes (walker : NKIWalker) (n : walker.Node) (v : walker.Var) : Bool := match walker.actions n.val with | VarAction.Write name _ => name = walker.vars.get v | _ => false - def NKIWalker.isPath (walker : NKIWalker) : List walker.Node → Prop := fun + def NKIWalker.isPath (walker : NKIWalker) : List walker.Node → Bool := fun | [] => True | [n] => walker.edges 0 n.val | n₁ :: n₀ :: tl => walker.isPath (n₀ :: tl) ∧ (walker.edges n₀.val n₁.val) @@ -89,25 +92,35 @@ section DefNKIWalker nodes : List walker.Node nodes_sound : walker.isPath nodes - def NKIWalker.Path.writes (walker : NKIWalker) (𝕡 : walker.Path) (v : walker.Var) : Bool := - 𝕡.nodes.any (walker.writes . v) + def NKIWalker.Path.unroll (walker : NKIWalker) (𝕡 : walker.Path) + : 𝕡.nodes.length ≥ 2 → + ∃ (n₁ n₀ : walker.Node) (tl : List walker.Node), + (walker.edges n₀.val n₁.val) ∧ (n₁ :: n₀ :: tl = 𝕡.nodes) ∧ (walker.isPath (n₀ :: tl)) := by { + sorry + } + + @[simp] + def NKIWalker.Path.writes_somewhere (walker : NKIWalker) (𝕡 : walker.Path) (v : walker.Var) : Bool := + 𝕡.nodes.tail.any (walker.writes . v) - def NKIWalker.Path.terminal_is (walker : NKIWalker) (𝕡 : walker.Path) (motive : walker.Node → Bool) : Bool := + @[simp] + def NKIWalker.Path.true_at_terminal (walker : NKIWalker) (𝕡 : walker.Path) (motive : walker.Node → Bool) : Bool := match 𝕡.nodes with | n :: _ => motive n | _ => false - def NKIWalker.Path.reads_terminal (walker : NKIWalker) (𝕡 : walker.Path) (v : walker.Var) : Bool := - 𝕡.terminal_is walker (walker.reads . v) + def NKIWalker.Path.reads_at_terminal (walker : NKIWalker) (𝕡 : walker.Path) (v : walker.Var) : Bool := + 𝕡.true_at_terminal walker (walker.reads . v) -- proving (or failing to prove) this is the goal!! def NKIWalker.sound (walker : NKIWalker) : Prop := - ∀ (𝕡 : walker.Path) v, (𝕡.reads_terminal walker v) → (𝕡.writes walker v) + ∀ (𝕡 : walker.Path) v, (𝕡.reads_at_terminal walker v) → (𝕡.writes_somewhere walker v) def NKIWalker.processAction (walker : NKIWalker) (action : VarAction) : NKIWalker := let N := walker.num_nodes {walker with num_nodes := N + 1 + num_nodes_nonzero := by simp last_node := N actions n := if n = N then action else walker.actions n edges A B := (A, B) = (walker.last_node, N) @@ -423,26 +436,83 @@ section Test def σ := (𝕏 h𝕏).props def ℙ := walker.Path + + #check 𝕏 #check ν #check σ + #check ℙ - - def NKIWalker.Path.def_terminal (𝕡 : walker.Path) (v : walker.Var) : Bool := + @[simp] + def NKIWalker.Path.var_def_at_terminal (𝕡 : walker.Path) (v : walker.Var) : Bool := let ⟨k, hk⟩ := v - 𝕡.terminal_is walker (fun ⟨n, hn⟩ ↦ ν h𝕏 n k hn hk) + 𝕡.true_at_terminal walker (fun ⟨n, hn⟩ ↦ ¬ ν h𝕏 n k hn hk) + + def NKIWalker.Path.not_def_at_entry (𝕡 : walker.Path) (v : walker.Var) : 𝕡.nodes.length < 2 → ¬ 𝕡.var_def_at_terminal h𝕏 v := + match h : 𝕡.nodes with + | [] => by { + intro + cases v + simp + rw [h] + } + | [⟨n, hn⟩] => by { + intro + cases v + rename_i k hk + simp + rw [h] + simp + have h_edge: walker.edges 0 n := by { + have h𝕡 := 𝕡.nodes_sound + unfold NKIWalker.isPath at h𝕡 + rw [h] at h𝕡 + simp at h𝕡 + assumption + } + let X := σ h𝕏 0 n k walker.num_nodes_nonzero hn hk h_edge + simp [transitions, LE.le, instLEOfPreorder, Preorder.toLE, instPreorderBool_compile, Bool.instLE] at X + assumption + } + | _ :: _ :: tl => by { + intro h + simp at h + omega + } - def ℍ : ∀ (𝕡 : ℙ) v, (𝕡.def_terminal h𝕏 v) → (𝕡.writes walker v) + --no def without a write + def ℍ : ∀ (𝕡 : ℙ) v, (𝕡.var_def_at_terminal h𝕏 v) → (𝕡.writes_somewhere walker v) := by { - sorry -- proof by induction on 𝕡, "the hard part" + intro 𝕡₁ v + cases 𝕡₁_def : 𝕡₁ + rename_i nodes₁ is_path₁ + cases v_def : v + rename_i k hk + induction nodes₁; simp + { + --inductive hypothesis case + rename_i n₁ tl₁ IndHyp + intro var_def_at₁ + by_cases non_entry : 𝕡₁.nodes.length ≥ 2; swap + { + have non_entry' : 𝕡₁.nodes.length < 2 := by omega + exfalso + apply (𝕡₁.not_def_at_entry h𝕏 v non_entry') + rw [𝕡₁_def, v_def] + assumption + } + let ⟨n₁', n₀, tl, ε, is_unroll, isPath⟩ := 𝕡₁.unroll walker non_entry + sorry + } } - def 𝕀 : ∀ (𝕡 : ℙ) v, (𝕡.reads_terminal walker v) → (𝕡.def_terminal h𝕏 v) + --no read without a def + def 𝕀 : ∀ (𝕡 : ℙ) v, (𝕡.reads_at_terminal walker v) → (𝕡.var_def_at_terminal h𝕏 v) := by { sorry -- proof by relying an an easily computable hypothesis (abstracted as a var to prove this goal) } - -- yay! + -- no read without a write :) def 𝕁 : walker.sound := by { unfold NKIWalker.sound intro 𝕡 name reads From 0ff118235bd052ee104176bdbe4eeb7408b81fa2 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Sat, 19 Jul 2025 17:15:07 -0400 Subject: [PATCH 16/33] make more progress --- KLR/Compile/NKIDataflow.lean | 42 ++++++++++++++++-------------------- 1 file changed, 18 insertions(+), 24 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index 20060e7f..f414288d 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -480,31 +480,25 @@ section Test omega } + def NKIWalker.Path.motive (𝕡 : walker.Path) (v : walker.Var) : Prop := 𝕡.var_def_at_terminal h𝕏 v → 𝕡.writes_somewhere walker v + + def length_motive n := ∀ (𝕡 : ℙ) v, 𝕡.nodes.length = n → (𝕡.motive h𝕏 v) + + def sound_at_zero : length_motive h𝕏 0 := sorry + def sound_at_one : length_motive h𝕏 1 := sorry + def sound_ind : ∀ n, length_motive h𝕏 n → length_motive h𝕏 (n + 2) := sorry + + def sound_everywhere : ∀ n, length_motive h𝕏 n := fun + | 0 => sound_at_zero h𝕏 + | 1 => sound_at_one h𝕏 + | n + 2 => sound_ind h𝕏 n (sound_everywhere n) + --no def without a write - def ℍ : ∀ (𝕡 : ℙ) v, (𝕡.var_def_at_terminal h𝕏 v) → (𝕡.writes_somewhere walker v) - := by { - intro 𝕡₁ v - cases 𝕡₁_def : 𝕡₁ - rename_i nodes₁ is_path₁ - cases v_def : v - rename_i k hk - induction nodes₁; simp - { - --inductive hypothesis case - rename_i n₁ tl₁ IndHyp - intro var_def_at₁ - by_cases non_entry : 𝕡₁.nodes.length ≥ 2; swap - { - have non_entry' : 𝕡₁.nodes.length < 2 := by omega - exfalso - apply (𝕡₁.not_def_at_entry h𝕏 v non_entry') - rw [𝕡₁_def, v_def] - assumption - } - let ⟨n₁', n₀, tl, ε, is_unroll, isPath⟩ := 𝕡₁.unroll walker non_entry - sorry - } - } + def ℍ : ∀ (𝕡 : ℙ) v, (𝕡.var_def_at_terminal h𝕏 v) → (𝕡.writes_somewhere walker v) := by { + intro 𝕡 v + apply sound_everywhere + rfl + } --no read without a def def 𝕀 : ∀ (𝕡 : ℙ) v, (𝕡.reads_at_terminal walker v) → (𝕡.var_def_at_terminal h𝕏 v) From c81dd4930b6e888e7809d98af670f4c270b9a826 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Sat, 19 Jul 2025 17:29:49 -0400 Subject: [PATCH 17/33] shrink holes --- KLR/Compile/NKIDataflow.lean | 26 +++++++++++++++++++------- 1 file changed, 19 insertions(+), 7 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index f414288d..d8cc0687 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -99,11 +99,9 @@ section DefNKIWalker sorry } - @[simp] def NKIWalker.Path.writes_somewhere (walker : NKIWalker) (𝕡 : walker.Path) (v : walker.Var) : Bool := 𝕡.nodes.tail.any (walker.writes . v) - @[simp] def NKIWalker.Path.true_at_terminal (walker : NKIWalker) (𝕡 : walker.Path) (motive : walker.Node → Bool) : Bool := match 𝕡.nodes with | n :: _ => motive n @@ -443,7 +441,6 @@ section Test #check ℙ - @[simp] def NKIWalker.Path.var_def_at_terminal (𝕡 : walker.Path) (v : walker.Var) : Bool := let ⟨k, hk⟩ := v 𝕡.true_at_terminal walker (fun ⟨n, hn⟩ ↦ ¬ ν h𝕏 n k hn hk) @@ -453,14 +450,14 @@ section Test | [] => by { intro cases v - simp + simp [NKIWalker.Path.var_def_at_terminal, NKIWalker.Path.true_at_terminal] rw [h] } | [⟨n, hn⟩] => by { intro cases v rename_i k hk - simp + simp [NKIWalker.Path.var_def_at_terminal, NKIWalker.Path.true_at_terminal] rw [h] simp have h_edge: walker.edges 0 n := by { @@ -480,12 +477,27 @@ section Test omega } + @[simp] def NKIWalker.Path.motive (𝕡 : walker.Path) (v : walker.Var) : Prop := 𝕡.var_def_at_terminal h𝕏 v → 𝕡.writes_somewhere walker v + @[simp] def length_motive n := ∀ (𝕡 : ℙ) v, 𝕡.nodes.length = n → (𝕡.motive h𝕏 v) - def sound_at_zero : length_motive h𝕏 0 := sorry - def sound_at_one : length_motive h𝕏 1 := sorry + def sound_at_zero : length_motive h𝕏 0 := by { + simp [NKIWalker.Path.var_def_at_terminal, NKIWalker.Path.true_at_terminal, NKIWalker.Path.writes_somewhere] + intro 𝕡 ⟨h, k⟩ is_zero + simp [is_zero] + } + + def sound_at_one : length_motive h𝕏 1 := by { + simp + intro 𝕡 v _ _ + exfalso + apply (𝕡.not_def_at_entry h𝕏 v) + omega + assumption + } + def sound_ind : ∀ n, length_motive h𝕏 n → length_motive h𝕏 (n + 2) := sorry def sound_everywhere : ∀ n, length_motive h𝕏 n := fun From a3fbf70bd3df9aafa0e8e507f03272db9d37937f Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Sat, 19 Jul 2025 18:31:14 -0400 Subject: [PATCH 18/33] progress --- KLR/Compile/NKIDataflow.lean | 90 +++++++++++++++++++++--------------- 1 file changed, 53 insertions(+), 37 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index d8cc0687..f2f2a796 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -102,17 +102,22 @@ section DefNKIWalker def NKIWalker.Path.writes_somewhere (walker : NKIWalker) (𝕡 : walker.Path) (v : walker.Var) : Bool := 𝕡.nodes.tail.any (walker.writes . v) - def NKIWalker.Path.true_at_terminal (walker : NKIWalker) (𝕡 : walker.Path) (motive : walker.Node → Bool) : Bool := + def NKIWalker.Path.writes_somewhere_lifts (walker : NKIWalker) (𝕡₀ 𝕡₁ : walker.Path) (v : walker.Var) + : 𝕡₁.nodes.tail = 𝕡₀.nodes → 𝕡₀.writes_somewhere walker v → 𝕡₁.writes_somewhere walker v := by { + sorry + } + + def NKIWalker.Path.true_at_terminus (walker : NKIWalker) (𝕡 : walker.Path) (motive : walker.Node → Bool) : Bool := match 𝕡.nodes with | n :: _ => motive n | _ => false - def NKIWalker.Path.reads_at_terminal (walker : NKIWalker) (𝕡 : walker.Path) (v : walker.Var) : Bool := - 𝕡.true_at_terminal walker (walker.reads . v) + def NKIWalker.Path.reads_at_terminus (walker : NKIWalker) (𝕡 : walker.Path) (v : walker.Var) : Bool := + 𝕡.true_at_terminus walker (walker.reads . v) -- proving (or failing to prove) this is the goal!! def NKIWalker.sound (walker : NKIWalker) : Prop := - ∀ (𝕡 : walker.Path) v, (𝕡.reads_at_terminal walker v) → (𝕡.writes_somewhere walker v) + ∀ (𝕡 : walker.Path) v, (𝕡.reads_at_terminus walker v) → (𝕡.writes_somewhere walker v) def NKIWalker.processAction (walker : NKIWalker) (action : VarAction) : NKIWalker := let N := walker.num_nodes @@ -429,11 +434,16 @@ section Test variable (h𝕏 : 𝕏opt.isSome) - def 𝕏 := 𝕏opt.get h𝕏 - def ν := (𝕏 h𝕏).vals - def σ := (𝕏 h𝕏).props - def ℙ := walker.Path + abbrev 𝕏 := 𝕏opt.get h𝕏 + abbrev ℙ := walker.Path + abbrev 𝕟 := walker.Node + abbrev 𝕍 := walker.Var + abbrev ν (n : 𝕟) (v : 𝕍) := (𝕏 h𝕏).vals n.val v.val n.isLt v.isLt + def σ (n₀ n₁ : 𝕟) (v : 𝕍) : transitions n₀.val v.val (ν h𝕏 n₀ v) ≤ ν h𝕏 n₁ v := by { + let X := (𝕏 h𝕏).props n₀.val n₁.val v.val n₀.isLt n₁.isLt v.isLt + sorry + } #check 𝕏 #check ν @@ -441,51 +451,38 @@ section Test #check ℙ - def NKIWalker.Path.var_def_at_terminal (𝕡 : walker.Path) (v : walker.Var) : Bool := - let ⟨k, hk⟩ := v - 𝕡.true_at_terminal walker (fun ⟨n, hn⟩ ↦ ¬ ν h𝕏 n k hn hk) + def NKIWalker.Path.var_def_at_terminus (𝕡 : ℙ) (v : 𝕍) : Bool := 𝕡.true_at_terminus walker (¬ν h𝕏 . v) - def NKIWalker.Path.not_def_at_entry (𝕡 : walker.Path) (v : walker.Var) : 𝕡.nodes.length < 2 → ¬ 𝕡.var_def_at_terminal h𝕏 v := + def NKIWalker.Path.not_def_at_entry (𝕡 : ℙ) (v : walker.Var) : 𝕡.nodes.length = 1 → ¬ 𝕡.var_def_at_terminus h𝕏 v := match h : 𝕡.nodes with - | [] => by { - intro - cases v - simp [NKIWalker.Path.var_def_at_terminal, NKIWalker.Path.true_at_terminal] - rw [h] - } - | [⟨n, hn⟩] => by { + | [n] => by { intro cases v rename_i k hk - simp [NKIWalker.Path.var_def_at_terminal, NKIWalker.Path.true_at_terminal] + simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.true_at_terminus] rw [h] simp - have h_edge: walker.edges 0 n := by { + have h_edge: walker.edges 0 n.val := by { have h𝕡 := 𝕡.nodes_sound unfold NKIWalker.isPath at h𝕡 rw [h] at h𝕡 simp at h𝕡 assumption } - let X := σ h𝕏 0 n k walker.num_nodes_nonzero hn hk h_edge - simp [transitions, LE.le, instLEOfPreorder, Preorder.toLE, instPreorderBool_compile, Bool.instLE] at X - assumption + apply σ h𝕏 ⟨0, walker.num_nodes_nonzero⟩ n ⟨k, hk⟩ h_edge + simp [transitions, LE.le, instLEOfPreorder, Preorder.toLE, instPreorderBool_compile, Bool.instLE] } - | _ :: _ :: tl => by { - intro h - simp at h - omega - } + | [] | _ :: _ :: _ => by simp @[simp] - def NKIWalker.Path.motive (𝕡 : walker.Path) (v : walker.Var) : Prop := 𝕡.var_def_at_terminal h𝕏 v → 𝕡.writes_somewhere walker v + def NKIWalker.Path.motive (𝕡 : ℙ) (v : walker.Var) : Prop := 𝕡.var_def_at_terminus h𝕏 v → 𝕡.writes_somewhere walker v @[simp] def length_motive n := ∀ (𝕡 : ℙ) v, 𝕡.nodes.length = n → (𝕡.motive h𝕏 v) def sound_at_zero : length_motive h𝕏 0 := by { - simp [NKIWalker.Path.var_def_at_terminal, NKIWalker.Path.true_at_terminal, NKIWalker.Path.writes_somewhere] - intro 𝕡 ⟨h, k⟩ is_zero + simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.true_at_terminus, NKIWalker.Path.writes_somewhere] + intro _ _ is_zero simp [is_zero] } @@ -494,26 +491,45 @@ section Test intro 𝕡 v _ _ exfalso apply (𝕡.not_def_at_entry h𝕏 v) - omega + assumption assumption } - def sound_ind : ∀ n, length_motive h𝕏 n → length_motive h𝕏 (n + 2) := sorry + def sound_ind : ∀ len, len ≥ 1 → length_motive h𝕏 len → length_motive h𝕏 (len + 1) := by { + unfold length_motive + intro len len_nonzero IndHyp 𝕡₁ v 𝕡₁_len ν₁ + cases 𝕡₁_def : 𝕡₁ + rename_i nodes₁ is_path₁ + let ⟨n₁, n₀, tl₀, ε, unroll, is_path₀⟩ := 𝕡₁.unroll walker (by omega) + simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.true_at_terminus, ←unroll] at ν₁ + let 𝕡₀ : ℙ := ⟨n₀ :: tl₀, is_path₀⟩ + cases ν₀ : ν h𝕏 n₀ v + { + -- v is defined at n₀ - the terminus of 𝕡₀, so writes somewhere by ind hypo, then lift + } + { + -- is not defined at n₀ -- the terminus of 𝕡₀, but is at n₁, the terminus of 𝕡₁ + -- since we have ε : edge from n₀ to n₁, σ n₀ n₀ + let X := σ h𝕏 n₀ n₁ v ε + simp [transitions, LE.le, instLEOfPreorder, Preorder.toLE, instPreorderBool_compile, Bool.instLE] at X + + } + } def sound_everywhere : ∀ n, length_motive h𝕏 n := fun | 0 => sound_at_zero h𝕏 | 1 => sound_at_one h𝕏 - | n + 2 => sound_ind h𝕏 n (sound_everywhere n) + | n + 2 => sound_ind h𝕏 (n + 1) (by omega) (sound_everywhere (n + 1)) --no def without a write - def ℍ : ∀ (𝕡 : ℙ) v, (𝕡.var_def_at_terminal h𝕏 v) → (𝕡.writes_somewhere walker v) := by { + def ℍ : ∀ (𝕡 : ℙ) v, (𝕡.var_def_at_terminus h𝕏 v) → (𝕡.writes_somewhere walker v) := by { intro 𝕡 v apply sound_everywhere rfl } --no read without a def - def 𝕀 : ∀ (𝕡 : ℙ) v, (𝕡.reads_at_terminal walker v) → (𝕡.var_def_at_terminal h𝕏 v) + def 𝕀 : ∀ (𝕡 : ℙ) v, (𝕡.reads_at_terminus walker v) → (𝕡.var_def_at_terminus h𝕏 v) := by { sorry -- proof by relying an an easily computable hypothesis (abstracted as a var to prove this goal) } From cf29a0532488db5e307a1035b65f7c910059c213 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Sat, 19 Jul 2025 18:45:53 -0400 Subject: [PATCH 19/33] fewer holes --- KLR/Compile/NKIDataflow.lean | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index f2f2a796..66141d00 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -438,11 +438,12 @@ section Test abbrev ℙ := walker.Path abbrev 𝕟 := walker.Node abbrev 𝕍 := walker.Var + abbrev 𝔼 (n₀ n₁ : walker.Node) := walker.edges n₀.val n₁.val abbrev ν (n : 𝕟) (v : 𝕍) := (𝕏 h𝕏).vals n.val v.val n.isLt v.isLt - def σ (n₀ n₁ : 𝕟) (v : 𝕍) : transitions n₀.val v.val (ν h𝕏 n₀ v) ≤ ν h𝕏 n₁ v := by { - let X := (𝕏 h𝕏).props n₀.val n₁.val v.val n₀.isLt n₁.isLt v.isLt - sorry + + abbrev σ (n₀ n₁ : 𝕟) (v : 𝕍) (𝔼n:𝔼 n₀ n₁): transitions n₀.val v.val (ν h𝕏 n₀ v) ≤ ν h𝕏 n₁ v := by { + apply (𝕏 h𝕏).props n₀.val n₁.val v.val n₀.isLt n₁.isLt v.isLt 𝔼n } #check 𝕏 @@ -510,9 +511,16 @@ section Test { -- is not defined at n₀ -- the terminus of 𝕡₀, but is at n₁, the terminus of 𝕡₁ -- since we have ε : edge from n₀ to n₁, σ n₀ n₀ - let X := σ h𝕏 n₀ n₁ v ε - simp [transitions, LE.le, instLEOfPreorder, Preorder.toLE, instPreorderBool_compile, Bool.instLE] at X - + let σ' := σ h𝕏 n₀ n₁ v ε + simp [transitions, LE.le, instLEOfPreorder, Preorder.toLE, instPreorderBool_compile, Bool.instLE, ν₀, ν₁] at σ' + let ⟨_, σ''⟩ := σ' + cases action_def : walker.actions n₀.val <;> rw [action_def] at σ'' <;> try simp at σ'' + rename_i _ name _ + simp [NKIWalker.Path.writes_somewhere] + simp [𝕡₁_def] at unroll + simp [←unroll, action_def] + apply Or.inl + assumption } } From bff7c092e95a56bc33254f49ec6371f5a5176021 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Sat, 19 Jul 2025 19:27:27 -0400 Subject: [PATCH 20/33] yay more holes closed --- KLR/Compile/NKIDataflow.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index 66141d00..80ecaebb 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -507,6 +507,14 @@ section Test cases ν₀ : ν h𝕏 n₀ v { -- v is defined at n₀ - the terminus of 𝕡₀, so writes somewhere by ind hypo, then lift + rw [←𝕡₁_def] + apply (NKIWalker.Path.writes_somewhere_lifts walker 𝕡₀ 𝕡₁ v); simp [←unroll, 𝕡₀] + apply IndHyp + simp [←unroll] at 𝕡₁_len + simp [𝕡₀] + assumption + simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.true_at_terminus, 𝕡₀] + assumption } { -- is not defined at n₀ -- the terminus of 𝕡₀, but is at n₁, the terminus of 𝕡₁ From c714db6e0bfd35d4a6027ffca342fc2a19a4bc58 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Sat, 19 Jul 2025 19:41:01 -0400 Subject: [PATCH 21/33] kill a sorry! --- KLR/Compile/NKIDataflow.lean | 33 ++++++++++++++++++++++++--------- 1 file changed, 24 insertions(+), 9 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index 80ecaebb..c3b39fd9 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -77,7 +77,6 @@ section DefNKIWalker | VarAction.Read name => name = walker.vars.get v | _ => false - @[simp] def NKIWalker.writes (walker : NKIWalker) (n : walker.Node) (v : walker.Var) : Bool := match walker.actions n.val with | VarAction.Write name _ => name = walker.vars.get v @@ -102,9 +101,24 @@ section DefNKIWalker def NKIWalker.Path.writes_somewhere (walker : NKIWalker) (𝕡 : walker.Path) (v : walker.Var) : Bool := 𝕡.nodes.tail.any (walker.writes . v) + -- easier to rewrite this than find it in the library lol + abbrev mem_lifts {α} (a : α) (ℓ : List α) : a ∈ ℓ.tail → a ∈ ℓ := by { + intro h + cases ℓ + contradiction + simp_all + } + def NKIWalker.Path.writes_somewhere_lifts (walker : NKIWalker) (𝕡₀ 𝕡₁ : walker.Path) (v : walker.Var) : 𝕡₁.nodes.tail = 𝕡₀.nodes → 𝕡₀.writes_somewhere walker v → 𝕡₁.writes_somewhere walker v := by { - sorry + simp [writes_somewhere] + intro unroll n₀ n₀_in n₀_writes + exists n₀ + apply And.intro + simp [unroll] + apply mem_lifts + assumption + assumption } def NKIWalker.Path.true_at_terminus (walker : NKIWalker) (𝕡 : walker.Path) (motive : walker.Node → Bool) : Bool := @@ -476,18 +490,19 @@ section Test | [] | _ :: _ :: _ => by simp @[simp] - def NKIWalker.Path.motive (𝕡 : ℙ) (v : walker.Var) : Prop := 𝕡.var_def_at_terminus h𝕏 v → 𝕡.writes_somewhere walker v + abbrev NKIWalker.Path.motive (𝕡 : ℙ) (v : walker.Var) : Prop + := 𝕡.var_def_at_terminus h𝕏 v → 𝕡.writes_somewhere walker v @[simp] - def length_motive n := ∀ (𝕡 : ℙ) v, 𝕡.nodes.length = n → (𝕡.motive h𝕏 v) + abbrev length_motive n := ∀ (𝕡 : ℙ) v, 𝕡.nodes.length = n → (𝕡.motive h𝕏 v) - def sound_at_zero : length_motive h𝕏 0 := by { + abbrev sound_at_zero : length_motive h𝕏 0 := by { simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.true_at_terminus, NKIWalker.Path.writes_somewhere] intro _ _ is_zero simp [is_zero] } - def sound_at_one : length_motive h𝕏 1 := by { + abbrev sound_at_one : length_motive h𝕏 1 := by { simp intro 𝕡 v _ _ exfalso @@ -496,7 +511,7 @@ section Test assumption } - def sound_ind : ∀ len, len ≥ 1 → length_motive h𝕏 len → length_motive h𝕏 (len + 1) := by { + abbrev sound_ind : ∀ len, len ≥ 1 → length_motive h𝕏 len → length_motive h𝕏 (len + 1) := by { unfold length_motive intro len len_nonzero IndHyp 𝕡₁ v 𝕡₁_len ν₁ cases 𝕡₁_def : 𝕡₁ @@ -526,13 +541,13 @@ section Test rename_i _ name _ simp [NKIWalker.Path.writes_somewhere] simp [𝕡₁_def] at unroll - simp [←unroll, action_def] + simp [←unroll, action_def, NKIWalker.writes] apply Or.inl assumption } } - def sound_everywhere : ∀ n, length_motive h𝕏 n := fun + abbrev sound_everywhere : ∀ n, length_motive h𝕏 n := fun | 0 => sound_at_zero h𝕏 | 1 => sound_at_one h𝕏 | n + 2 => sound_ind h𝕏 (n + 1) (by omega) (sound_everywhere (n + 1)) From 34a8f27523cbae89637bc07c310676d1ec2681dc Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Sat, 19 Jul 2025 20:46:57 -0400 Subject: [PATCH 22/33] omg wow pretty good! --- KLR/Compile/NKIDataflow.lean | 52 +++++++++++++++++++++++++++++------- 1 file changed, 42 insertions(+), 10 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index c3b39fd9..f21b9c80 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -82,21 +82,49 @@ section DefNKIWalker | VarAction.Write name _ => name = walker.vars.get v | _ => false - def NKIWalker.isPath (walker : NKIWalker) : List walker.Node → Bool := fun + def NKIWalker.is_path (walker : NKIWalker) : List walker.Node → Bool := fun | [] => True | [n] => walker.edges 0 n.val - | n₁ :: n₀ :: tl => walker.isPath (n₀ :: tl) ∧ (walker.edges n₀.val n₁.val) + | n₁ :: n₀ :: tl => walker.is_path (n₀ :: tl) ∧ (walker.edges n₀.val n₁.val) + + def NKIWalker.is_path_lowers (walker : NKIWalker) : + ∀ n ℓ, walker.is_path (n::ℓ) → walker.is_path ℓ := by { + intro n₁ ℓ₁ h + cases ℓ₁ with | nil => simp [is_path] | cons n₀ ℓ₀ + simp_all [is_path] + } structure NKIWalker.Path (walker : NKIWalker) where nodes : List walker.Node - nodes_sound : walker.isPath nodes + nodes_sound : walker.is_path nodes + + -- a path can always be unrolled into a shorter valid one, with proof of an edge across the unrolling def NKIWalker.Path.unroll (walker : NKIWalker) (𝕡 : walker.Path) : 𝕡.nodes.length ≥ 2 → ∃ (n₁ n₀ : walker.Node) (tl : List walker.Node), - (walker.edges n₀.val n₁.val) ∧ (n₁ :: n₀ :: tl = 𝕡.nodes) ∧ (walker.isPath (n₀ :: tl)) := by { - sorry - } + (walker.edges n₀.val n₁.val) ∧ (n₁ :: n₀ :: tl = 𝕡.nodes) ∧ (walker.is_path (n₀ :: tl)) := by { + intro not_tiny + rcases 𝕡_def : 𝕡.nodes + simp [𝕡_def] at not_tiny + rename_i n₁ tl₁ + rcases tl₁_def : tl₁ + simp [𝕡_def, tl₁_def] at not_tiny + rename_i n₀ tl₀ + exists n₁, n₀, tl₀ + apply And.intro + { + let sound := 𝕡.nodes_sound + simp [𝕡_def, tl₁_def, is_path] at sound + exact sound.right + } + { + simp [←tl₁_def] + apply walker.is_path_lowers n₁ tl₁ + rw [←𝕡_def] + apply 𝕡.nodes_sound + } + } def NKIWalker.Path.writes_somewhere (walker : NKIWalker) (𝕡 : walker.Path) (v : walker.Var) : Bool := 𝕡.nodes.tail.any (walker.writes . v) @@ -468,7 +496,7 @@ section Test def NKIWalker.Path.var_def_at_terminus (𝕡 : ℙ) (v : 𝕍) : Bool := 𝕡.true_at_terminus walker (¬ν h𝕏 . v) - def NKIWalker.Path.not_def_at_entry (𝕡 : ℙ) (v : walker.Var) : 𝕡.nodes.length = 1 → ¬ 𝕡.var_def_at_terminus h𝕏 v := + def NKIWalker.Path.not_def_at_entry (𝕡 : ℙ) (v : 𝕍) : 𝕡.nodes.length = 1 → ¬ 𝕡.var_def_at_terminus h𝕏 v := match h : 𝕡.nodes with | [n] => by { intro @@ -479,7 +507,7 @@ section Test simp have h_edge: walker.edges 0 n.val := by { have h𝕡 := 𝕡.nodes_sound - unfold NKIWalker.isPath at h𝕡 + unfold NKIWalker.is_path at h𝕡 rw [h] at h𝕡 simp at h𝕡 assumption @@ -490,7 +518,7 @@ section Test | [] | _ :: _ :: _ => by simp @[simp] - abbrev NKIWalker.Path.motive (𝕡 : ℙ) (v : walker.Var) : Prop + abbrev NKIWalker.Path.motive (𝕡 : ℙ) (v : 𝕍) : Prop := 𝕡.var_def_at_terminus h𝕏 v → 𝕡.writes_somewhere walker v @[simp] @@ -559,10 +587,14 @@ section Test rfl } + variable (is_safe : ∀ (n : 𝕟) (v : 𝕍), walker.reads n v → ¬ν h𝕏 n v) + --no read without a def def 𝕀 : ∀ (𝕡 : ℙ) v, (𝕡.reads_at_terminus walker v) → (𝕡.var_def_at_terminus h𝕏 v) := by { - sorry -- proof by relying an an easily computable hypothesis (abstracted as a var to prove this goal) + simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.reads_at_terminus, NKIWalker.Path.true_at_terminus] + intro 𝕡 v h + cases nodes_def : 𝕡.nodes with | nil | cons n ℓ <;> simp_all [nodes_def] } -- no read without a write :) From 1e2f62c642c75147470a17aebe2811da1de9330f Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Sat, 19 Jul 2025 23:11:33 -0400 Subject: [PATCH 23/33] no sorries, still having trouble wrapping it all up --- KLR/Compile/NKIDataflow.lean | 74 +++++++++++++++++++++++++++--------- 1 file changed, 55 insertions(+), 19 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index f21b9c80..4483f93f 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -493,8 +493,8 @@ section Test #check σ #check ℙ - - def NKIWalker.Path.var_def_at_terminus (𝕡 : ℙ) (v : 𝕍) : Bool := 𝕡.true_at_terminus walker (¬ν h𝕏 . v) + abbrev var_def (n : 𝕟) (v : 𝕍) : Bool := ¬ν h𝕏 n v + def NKIWalker.Path.var_def_at_terminus (𝕡 : ℙ) (v : 𝕍) : Bool := 𝕡.true_at_terminus walker (var_def h𝕏 . v) def NKIWalker.Path.not_def_at_entry (𝕡 : ℙ) (v : 𝕍) : 𝕡.nodes.length = 1 → ¬ 𝕡.var_def_at_terminus h𝕏 v := match h : 𝕡.nodes with @@ -580,31 +580,67 @@ section Test | 1 => sound_at_one h𝕏 | n + 2 => sound_ind h𝕏 (n + 1) (by omega) (sound_everywhere (n + 1)) - --no def without a write - def ℍ : ∀ (𝕡 : ℙ) v, (𝕡.var_def_at_terminus h𝕏 v) → (𝕡.writes_somewhere walker v) := by { + def no_def_without_a_write : ∀ (𝕡 : ℙ) v, (𝕡.var_def_at_terminus h𝕏 v) → (𝕡.writes_somewhere walker v) := by { intro 𝕡 v apply sound_everywhere rfl } - variable (is_safe : ∀ (n : 𝕟) (v : 𝕍), walker.reads n v → ¬ν h𝕏 n v) + abbrev is_safe_at (n : 𝕟) (v : 𝕍) : Prop := walker.reads n v → var_def h𝕏 n v - --no read without a def - def 𝕀 : ∀ (𝕡 : ℙ) v, (𝕡.reads_at_terminus walker v) → (𝕡.var_def_at_terminus h𝕏 v) - := by { - simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.reads_at_terminus, NKIWalker.Path.true_at_terminus] - intro 𝕡 v h - cases nodes_def : 𝕡.nodes with | nil | cons n ℓ <;> simp_all [nodes_def] - } + abbrev is_safe : Prop := ∀ (n : 𝕟) (v : 𝕍), is_safe_at h𝕏 n v - -- no read without a write :) - def 𝕁 : walker.sound := by { - unfold NKIWalker.sound - intro 𝕡 name reads - apply ℍ - apply 𝕀 - assumption + abbrev local_safety_decidable : ∀ n v, Decidable (is_safe_at h𝕏 n v) := by { + intro n v + unfold is_safe_at + cases reads? : walker.reads n v <;> + cases defs? : var_def h𝕏 n v <;> + simp [is_safe_at] <;> try {apply isTrue; trivial} + apply isFalse; trivial + } + + inductive Safety : Prop + | Unsafe : Safety + | Safe : is_safe h𝕏 → Safety + + abbrev forall_fin {n} (f : Fin n → Bool) : Bool := (Vector.ofFn f).all (.) + + abbrev forall_fin_sound (f : Fin n → Bool) : forall_fin f → (m : Fin n) → (f m) := by { + simp [forall_fin] + intro h m + apply h + } + + abbrev decide_safety : Safety h𝕏 := by { + let safe := forall_fin (fun n ↦ forall_fin (fun v ↦ decide (is_safe_at h𝕏 n v))) + by_cases safety : safe + swap; apply Safety.Unsafe -- if any reads occur where a var isnt def this will hit and fail + apply Safety.Safe + unfold is_safe + intro n v + have safety_at_n := forall_fin_sound _ safety n + have safety := (forall_fin_sound _ safety_at_n v) + apply of_decide_eq_true assumption } + section IfSafe + variable (safety : ∀ (n : 𝕟) (v : 𝕍), walker.reads n v → ¬ν h𝕏 n v) + + def no_read_without_a_def : ∀ (𝕡 : ℙ) v, (𝕡.reads_at_terminus walker v) → (𝕡.var_def_at_terminus h𝕏 v) + := by { + simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.reads_at_terminus, NKIWalker.Path.true_at_terminus] + intro 𝕡 v h + cases nodes_def : 𝕡.nodes with | nil | cons n ℓ <;> simp_all [nodes_def] + } + + def no_read_without_a_write : walker.sound := by { + unfold NKIWalker.sound + intro 𝕡 name reads + apply no_def_without_a_write + apply no_read_without_a_def + assumption + assumption + } + end IfSafe end Test From 2a503d39cb97a226adfe72a72e3f59ffdc8bebde Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Sat, 19 Jul 2025 23:50:47 -0400 Subject: [PATCH 24/33] wow mayb done? --- KLR/Compile/NKIDataflow.lean | 37 ++++++++++++++++++++++++++++++------ 1 file changed, 31 insertions(+), 6 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index 4483f93f..f979a7ec 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -599,9 +599,19 @@ section Test apply isFalse; trivial } - inductive Safety : Prop - | Unsafe : Safety - | Safe : is_safe h𝕏 → Safety + inductive Maybe P + | No : Maybe P + | Yes : P → Maybe P + + def Maybe.well? (s : Maybe P) := match s with + | No => false + | _ => true + + def decide_success : Maybe (𝕏opt.isSome) := by { + cases h : 𝕏opt with | none => apply Maybe.No | some => { + apply Maybe.Yes; simp + } + } abbrev forall_fin {n} (f : Fin n → Bool) : Bool := (Vector.ofFn f).all (.) @@ -611,11 +621,11 @@ section Test apply h } - abbrev decide_safety : Safety h𝕏 := by { + def decide_safety : Maybe (is_safe h𝕏) := by { let safe := forall_fin (fun n ↦ forall_fin (fun v ↦ decide (is_safe_at h𝕏 n v))) by_cases safety : safe - swap; apply Safety.Unsafe -- if any reads occur where a var isnt def this will hit and fail - apply Safety.Safe + swap; apply Maybe.No -- if any reads occur where a var isnt def this will hit and fail + apply Maybe.Yes unfold is_safe intro n v have safety_at_n := forall_fin_sound _ safety n @@ -643,4 +653,19 @@ section Test assumption } end IfSafe + + def decide_sound : Maybe (walker.sound) := by { + clear h𝕏 + cases decide_success with | No => apply Maybe.No | Yes success + cases (decide_safety success) with | No => apply Maybe.No | Yes safety + apply Maybe.Yes + apply no_read_without_a_write success + intro n v h + have specific_safety := safety n v h + simp [is_safe_at, var_def] at specific_safety + rw [specific_safety] + trivial + } + + #eval decide_sound.well? end Test From aa1856b3325c834c587513dce69e36d23661fc9a Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Sun, 20 Jul 2025 00:26:14 -0400 Subject: [PATCH 25/33] make testing clearer. looking great! --- KLR/Compile/DataflowTestKernels.lean | 220 +++++++++++++++++++++++++++ KLR/Compile/NKIDataflow.lean | 139 +++-------------- 2 files changed, 237 insertions(+), 122 deletions(-) create mode 100644 KLR/Compile/DataflowTestKernels.lean diff --git a/KLR/Compile/DataflowTestKernels.lean b/KLR/Compile/DataflowTestKernels.lean new file mode 100644 index 00000000..1cf7f16a --- /dev/null +++ b/KLR/Compile/DataflowTestKernels.lean @@ -0,0 +1,220 @@ +import KLR.NKI.Basic +open KLR.NKI + +class HasKernel where + kernel : Fun + repr : String + +def safe_kernel_1 : HasKernel where + repr := " + def test(): + x = 0 + c = 0 + p = 0 + if c: + p(x) + else: + y = 0 + p(y) + p(x) + " + kernel := { name := "test.test", + file := "unknown", + line := 1, + body := [{ stmt := KLR.NKI.Stmt'.assign + { expr := KLR.NKI.Expr'.var "x", + pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 2 } } + none + (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 2, column := 5, lineEnd := some 2, columnEnd := some 6 } }), + pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 6 } }, + { stmt := KLR.NKI.Stmt'.assign + { expr := KLR.NKI.Expr'.var "c", + pos := { line := 3, column := 1, lineEnd := some 3, columnEnd := some 2 } } + none + (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 3, column := 5, lineEnd := some 3, columnEnd := some 6 } }), + pos := { line := 3, column := 1, lineEnd := some 3, columnEnd := some 6 } }, + { stmt := KLR.NKI.Stmt'.assign + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 4, column := 1, lineEnd := some 4, columnEnd := some 2 } } + none + (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 4, column := 5, lineEnd := some 4, columnEnd := some 6 } }), + pos := { line := 4, column := 1, lineEnd := some 4, columnEnd := some 6 } }, + { stmt := KLR.NKI.Stmt'.ifStm + { expr := KLR.NKI.Expr'.var "c", + pos := { line := 5, column := 4, lineEnd := some 5, columnEnd := some 5 } } + [{ stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 6, + column := 2, + lineEnd := some 6, + columnEnd := some 3 } } + [{ expr := KLR.NKI.Expr'.var "x", + pos := { line := 6, + column := 4, + lineEnd := some 6, + columnEnd := some 5 } }] + [], + pos := { line := 6, + column := 2, + lineEnd := some 6, + columnEnd := some 6 } }, + pos := { line := 6, column := 2, lineEnd := some 6, columnEnd := some 6 } }] + [{ stmt := KLR.NKI.Stmt'.assign + { expr := KLR.NKI.Expr'.var "y", + pos := { line := 8, + column := 2, + lineEnd := some 8, + columnEnd := some 3 } } + none + (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 8, + column := 6, + lineEnd := some 8, + columnEnd := some 7 } }), + pos := { line := 8, column := 2, lineEnd := some 8, columnEnd := some 7 } }, + { stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 9, + column := 2, + lineEnd := some 9, + columnEnd := some 3 } } + [{ expr := KLR.NKI.Expr'.var "y", + pos := { line := 9, + column := 4, + lineEnd := some 9, + columnEnd := some 5 } }] + [], + pos := { line := 9, + column := 2, + lineEnd := some 9, + columnEnd := some 6 } }, + pos := { line := 9, column := 2, lineEnd := some 9, columnEnd := some 6 } }], + pos := { line := 5, column := 1, lineEnd := some 9, columnEnd := some 6 } }, + { stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 10, + column := 1, + lineEnd := some 10, + columnEnd := some 2 } } + [{ expr := KLR.NKI.Expr'.var "x", + pos := { line := 10, + column := 3, + lineEnd := some 10, + columnEnd := some 4 } }] + [], + pos := { line := 10, column := 1, lineEnd := some 10, columnEnd := some 5 } }, + pos := { line := 10, column := 1, lineEnd := some 10, columnEnd := some 5 } }], + args := [] } + +def unsafe_kernel_2 : HasKernel where + repr := " + def test(): + x = 0 + c = 0 + p = 0 + if c: + p(x) + else: + y = 0 + p(y) + p(y) + " + kernel := { name := "test.test", + file := "unknown", + line := 1, + body := [{ stmt := KLR.NKI.Stmt'.assign + { expr := KLR.NKI.Expr'.var "x", + pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 2 } } + none + (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 2, column := 5, lineEnd := some 2, columnEnd := some 6 } }), + pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 6 } }, + { stmt := KLR.NKI.Stmt'.assign + { expr := KLR.NKI.Expr'.var "c", + pos := { line := 3, column := 1, lineEnd := some 3, columnEnd := some 2 } } + none + (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 3, column := 5, lineEnd := some 3, columnEnd := some 6 } }), + pos := { line := 3, column := 1, lineEnd := some 3, columnEnd := some 6 } }, + { stmt := KLR.NKI.Stmt'.assign + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 4, column := 1, lineEnd := some 4, columnEnd := some 2 } } + none + (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 4, column := 5, lineEnd := some 4, columnEnd := some 6 } }), + pos := { line := 4, column := 1, lineEnd := some 4, columnEnd := some 6 } }, + { stmt := KLR.NKI.Stmt'.ifStm + { expr := KLR.NKI.Expr'.var "c", + pos := { line := 5, column := 4, lineEnd := some 5, columnEnd := some 5 } } + [{ stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 6, + column := 2, + lineEnd := some 6, + columnEnd := some 3 } } + [{ expr := KLR.NKI.Expr'.var "x", + pos := { line := 6, + column := 4, + lineEnd := some 6, + columnEnd := some 5 } }] + [], + pos := { line := 6, + column := 2, + lineEnd := some 6, + columnEnd := some 6 } }, + pos := { line := 6, column := 2, lineEnd := some 6, columnEnd := some 6 } }] + [{ stmt := KLR.NKI.Stmt'.assign + { expr := KLR.NKI.Expr'.var "y", + pos := { line := 8, + column := 2, + lineEnd := some 8, + columnEnd := some 3 } } + none + (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 8, + column := 6, + lineEnd := some 8, + columnEnd := some 7 } }), + pos := { line := 8, column := 2, lineEnd := some 8, columnEnd := some 7 } }, + { stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 9, + column := 2, + lineEnd := some 9, + columnEnd := some 3 } } + [{ expr := KLR.NKI.Expr'.var "y", + pos := { line := 9, + column := 4, + lineEnd := some 9, + columnEnd := some 5 } }] + [], + pos := { line := 9, + column := 2, + lineEnd := some 9, + columnEnd := some 6 } }, + pos := { line := 9, column := 2, lineEnd := some 9, columnEnd := some 6 } }], + pos := { line := 5, column := 1, lineEnd := some 9, columnEnd := some 6 } }, + { stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 10, + column := 1, + lineEnd := some 10, + columnEnd := some 2 } } + [{ expr := KLR.NKI.Expr'.var "y", + pos := { line := 10, + column := 3, + lineEnd := some 10, + columnEnd := some 4 } }] + [], + pos := { line := 10, column := 1, lineEnd := some 10, columnEnd := some 5 } }, + pos := { line := 10, column := 1, lineEnd := some 10, columnEnd := some 5 } }], + args := [] } diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index f979a7ec..beb474af 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -13,6 +13,7 @@ all variables at all program points `#eval 𝕏opt` import KLR.NKI.Basic import KLR.Compile.Dataflow +import KLR.Compile.DataflowTestKernels open KLR.NKI @@ -313,111 +314,15 @@ section DefNKIWalker end DefNKIWalker -section Test +section WithKernel + variable [HasKernel] - /- - file test.py: - def test(): - x = 0 - if cond0: - print(x) - else: - y = 0 - print(y) - print(y) - - bash: `klr compile test.py` yields the following serialization of a NKI Kernel - -/ - - def test_kernel : Kernel := { - entry := "test.test", - funs := [{name := "test.test", - file := "unknown", - line := 1, - body := [{ stmt := KLR.NKI.Stmt'.assign - { expr := KLR.NKI.Expr'.var "x", - pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 2 } } - none - (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), - pos := { line := 2, column := 5, lineEnd := some 2, columnEnd := some 6 } }), - pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 6 } }, - { stmt := KLR.NKI.Stmt'.ifStm - { expr := KLR.NKI.Expr'.var "cond0", - pos := { line := 3, column := 4, lineEnd := some 3, columnEnd := some 9 } } - [{stmt := KLR.NKI.Stmt'.expr - { expr := KLR.NKI.Expr'.call - { expr := KLR.NKI.Expr'.var "print", - pos := { line := 4, - column := 2, - lineEnd := some 4, - columnEnd := some 7 } } - [{ expr := KLR.NKI.Expr'.var "x", - pos := {line := 4, - column := 8, - lineEnd := some 4, - columnEnd := some 9 } }] - [], - pos := { line := 4, - column := 2, - lineEnd := some 4, - columnEnd := some 10 } }, - pos := {line := 4, column := 2, lineEnd := some 4, columnEnd := some 10 } }] - [{stmt := KLR.NKI.Stmt'.assign - { expr := KLR.NKI.Expr'.var "y", - pos := { line := 6, - column := 2, - lineEnd := some 6, - columnEnd := some 3 } } - none - (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), - pos := { line := 6, - column := 6, - lineEnd := some 6, - columnEnd := some 7 } }), - pos := { line := 6, column := 2, lineEnd := some 6, columnEnd := some 7 } }, - { stmt := KLR.NKI.Stmt'.expr - { expr := KLR.NKI.Expr'.call - { expr := KLR.NKI.Expr'.var "print", - pos := { line := 7, - column := 2, - lineEnd := some 7, - columnEnd := some 7 } } - [{ expr := KLR.NKI.Expr'.var "y", - pos := {line := 7, - column := 8, - lineEnd := some 7, - columnEnd := some 9 } }] - [], - pos := { line := 7, - column := 2, - lineEnd := some 7, - columnEnd := some 10 } }, - pos := { line := 7, column := 2, lineEnd := some 7, columnEnd := some 10 } }], - pos := { line := 3, column := 1, lineEnd := some 7, columnEnd := some 10 } }, - { stmt := KLR.NKI.Stmt'.expr - { expr := KLR.NKI.Expr'.call - { expr := KLR.NKI.Expr'.var "print", - pos := {line := 8, - column := 1, - lineEnd := some 8, - columnEnd := some 6 } } - [{expr := KLR.NKI.Expr'.var "y", - pos := {line := 8, - column := 7, - lineEnd := some 8, - columnEnd := some 8 } }] - [], - pos := { line := 8, column := 1, lineEnd := some 8, columnEnd := some 9 } }, - pos := { line := 8, column := 1, lineEnd := some 8, columnEnd := some 9 } }], - args := [] }], - args := [], - globals := [] } + abbrev 𝕂 := HasKernel.kernel /- Perform the walk of the AST, converting it into a CFG -/ - def walker := NKIWalker.processFun test_kernel.funs[0] - #eval walker + def walker [HasKernel] : NKIWalker := NKIWalker.processFun 𝕂 /- extract the transitions from the walker @@ -458,22 +363,6 @@ section Test key_labels k := walker.vars[k]? }) - #eval 𝕏opt - /- - Node 0: x:✅ cond0:✅ print:✅ y:✅ - Node 1: x:❌ cond0:❌ print:❌ y:❌ - Node 2: x:✅ cond0:❌ print:❌ y:❌ - Node 3: x:✅ cond0:❌ print:❌ y:❌ - Node 4: x:✅ cond0:❌ print:❌ y:❌ - Node 5: x:✅ cond0:❌ print:❌ y:❌ - Node 6: x:✅ cond0:❌ print:❌ y:✅ - Node 7: x:✅ cond0:❌ print:❌ y:✅ - Node 8: x:✅ cond0:❌ print:❌ y:❌ - Node 9: x:✅ cond0:❌ print:❌ y:❌ - Node 10: x:✅ cond0:❌ print:❌ y:❌ - Node 11: x:✅ cond0:❌ print:❌ y:❌ - -/ - variable (h𝕏 : 𝕏opt.isSome) abbrev 𝕏 := 𝕏opt.get h𝕏 @@ -488,10 +377,10 @@ section Test apply (𝕏 h𝕏).props n₀.val n₁.val v.val n₀.isLt n₁.isLt v.isLt 𝔼n } - #check 𝕏 - #check ν - #check σ - #check ℙ + --#check 𝕏 + --#check ν + --#check σ + --#check ℙ abbrev var_def (n : 𝕟) (v : 𝕍) : Bool := ¬ν h𝕏 n v def NKIWalker.Path.var_def_at_terminus (𝕡 : ℙ) (v : 𝕍) : Bool := 𝕡.true_at_terminus walker (var_def h𝕏 . v) @@ -666,6 +555,12 @@ section Test rw [specific_safety] trivial } +end WithKernel + +instance : HasKernel := safe_kernel_1 + +#eval decide_sound.well? + +instance : HasKernel := unsafe_kernel_2 - #eval decide_sound.well? -end Test +#eval decide_sound.well? From a2b98f2e65886efc378ad72b404cf54b10ef554a Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Mon, 21 Jul 2025 11:18:12 -0400 Subject: [PATCH 26/33] get example working --- KLR/Compile/DataflowTestKernels.lean | 54 ++++++++++++++++----- KLR/Compile/NKIDataflow.lean | 72 +++++++++++++++++++--------- 2 files changed, 90 insertions(+), 36 deletions(-) diff --git a/KLR/Compile/DataflowTestKernels.lean b/KLR/Compile/DataflowTestKernels.lean index 1cf7f16a..123079d1 100644 --- a/KLR/Compile/DataflowTestKernels.lean +++ b/KLR/Compile/DataflowTestKernels.lean @@ -1,23 +1,45 @@ import KLR.NKI.Basic open KLR.NKI +section TestKernels + class HasKernel where kernel : Fun - repr : String + kernel_str : String + +instance : ToString Pos where toString p := s!"{p.line}, {p.lineEnd}, {p.column}, {p.columnEnd}" + +def highlight_pos_set [HasKernel] (actions : List Pos) (s : String) : String := + let newlines : List Nat := (List.range s.length).filter (fun n ↦ s.toList[n]! = '\n') + + let findStart (pos : Pos) : List Nat := [newlines[pos.line - 1]! + pos.column + 1] + let findEnd (pos : Pos) : List Nat := match pos.lineEnd, pos.columnEnd with + | some l, some c => [newlines[l - 1]! + c + 1] + | _, _ => [] + let starts := actions.flatMap findStart + let ends := actions.flatMap findEnd + let out_str_at n : List Char := + let st := if n ∈ starts then ['⟦'] else [] + let ed := if n ∈ ends then ['⟧'] else [] + st ++ ed ++ [s.toList[n]!] + ⟨((List.range s.length).flatMap out_str_at)⟩ + +def kernel_highlighted_repr [HasKernel] (actions : List Pos) : String := + highlight_pos_set actions HasKernel.kernel_str + def safe_kernel_1 : HasKernel where - repr := " + kernel_str :=" def test(): - x = 0 - c = 0 - p = 0 - if c: - p(x) - else: - y = 0 - p(y) - p(x) - " + x = 0 + c = 0 + p = 0 + if c: + p(x) + else: + y = 0 + p(y) + p(x)" kernel := { name := "test.test", file := "unknown", line := 1, @@ -112,8 +134,11 @@ def safe_kernel_1 : HasKernel where pos := { line := 10, column := 1, lineEnd := some 10, columnEnd := some 5 } }], args := [] } + +#eval safe_kernel_1.kernel_str.toList[0] = '\n' + def unsafe_kernel_2 : HasKernel where - repr := " + kernel_str := " def test(): x = 0 c = 0 @@ -218,3 +243,6 @@ def unsafe_kernel_2 : HasKernel where pos := { line := 10, column := 1, lineEnd := some 10, columnEnd := some 5 } }, pos := { line := 10, column := 1, lineEnd := some 10, columnEnd := some 5 } }], args := [] } + + +end TestKernels diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index beb474af..b7ac98c5 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -20,20 +20,20 @@ open KLR.NKI section DefVarAction inductive VarAction where - | Read (name : String) - | Write (name : String) (ty : Option Expr) + | Read (name : String) (pos : Pos) + | Write (name : String) (ty : Option Expr) (pos : Pos) | None instance VarAction.toString : ToString VarAction where toString := fun - | Read name => s!"Read({name})" - | Write name _ => s!"Write({name})" - | None => "None" + | Read name pos => s!"Read({name} @ {pos.line}, {pos.column})" + | Write name _ pos => s!"Write({name} @ {pos.line}, {pos.column})" + | _ => "None" def VarAction.var := fun - | Read name => some name - | Write name _ => some name - | None => none + | Read name _ => some name + | Write name _ _ => some name + | _ => none end DefVarAction @@ -75,12 +75,12 @@ section DefNKIWalker def NKIWalker.reads (walker : NKIWalker) (n : walker.Node) (v : walker.Var) : Bool := match walker.actions n.val with - | VarAction.Read name => name = walker.vars.get v + | VarAction.Read name _ => name = walker.vars.get v | _ => false def NKIWalker.writes (walker : NKIWalker) (n : walker.Node) (v : walker.Var) : Bool := match walker.actions n.val with - | VarAction.Write name _ => name = walker.vars.get v + | VarAction.Write name _ _ => name = walker.vars.get v | _ => false def NKIWalker.is_path (walker : NKIWalker) : List walker.Node → Bool := fun @@ -225,10 +225,10 @@ section DefNKIWalker mutual def NKIWalker.processExpr (walker : NKIWalker) (expr : Expr) : NKIWalker := - let ⟨expr, _⟩ := expr + let ⟨expr, pos⟩ := expr match _ : expr with | Expr'.value _ => walker - | Expr'.var (name : String) => walker.processAction (VarAction.Read name) + | Expr'.var (name : String) => walker.processAction (VarAction.Read name pos) | Expr'.proj (expr : Expr) _ => walker.processExpr expr | Expr'.tuple (elements : List Expr) => walker.processExprList elements | Expr'.access (expr : Expr) _ => walker.processExpr expr @@ -256,7 +256,7 @@ section DefNKIWalker mutual def NKIWalker.processStmt (walker : NKIWalker) (stmt : Stmt) : NKIWalker := - let ⟨stmt, _⟩ := stmt + let ⟨stmt, pos⟩ := stmt match _ : stmt with | Stmt'.expr (e : Expr) => walker.processExpr e | Stmt'.assert (e : Expr) => walker.processExpr e @@ -264,11 +264,11 @@ section DefNKIWalker | Stmt'.assign ⟨Expr'.var name, _⟩ (ty : Option Expr) (e : Option Expr) => let withty := (match ty with | some ty => walker.processExpr ty | none => walker) let withe := (match e with | some e => withty.processExpr e | none => withty) - withe.processAction (VarAction.Write name ty) + withe.processAction (VarAction.Write name ty pos) | Stmt'.assign _ (ty : Option Expr) (e : Option Expr) => let withty := (match ty with | some ty => walker.processExpr ty | none => walker) let withe := (match e with | some e => withty.processExpr e | none => withty) - withe.processAction (VarAction.Write "NONVAR" ty) + withe.processAction (VarAction.Write "" ty pos) | Stmt'.ifStm (e : Expr) (thn : List Stmt) (els : List Stmt) => let then_walker := (walker.processExpr e).processStmtList thn let else_walker := (then_walker.setLast walker.last_node).processStmtList els @@ -331,7 +331,7 @@ section WithKernel (n = 0) ∨ if _ : k < walker.vars.length then match walker.actions n with - | VarAction.Write name _ => ¬ (name = walker.vars[k]) ∧ pre + | VarAction.Write name _ _ => ¬ (name = walker.vars[k]) ∧ pre | _ => pre else pre @@ -488,9 +488,16 @@ section WithKernel apply isFalse; trivial } - inductive Maybe P - | No : Maybe P + inductive Maybe (P : Prop) -- option type plus message option | Yes : P → Maybe P + | No : Maybe P + | NoBC : String → Maybe P --no because of message + + instance Maybe.toString : ToString (Maybe P) where + toString := fun + | Yes _ => s!"YES [SAFETY PROVEN]" + | No => "NO [SAFETY NOT PROVEN]" + | NoBC s => s!"NO [SAFETY NOT PROVEN] BECAUSE: {s}" def Maybe.well? (s : Maybe P) := match s with | No => false @@ -510,10 +517,24 @@ section WithKernel apply h } + abbrev 𝕀 (α) (a : α) := a + + def get_unsafe_reads : List VarAction := + (List.ofFn (fun n : 𝕟 ↦ (n, List.ofFn (𝕀 𝕍)))).flatMap (fun (n, vs) ↦ + if vs.any (fun v ↦ ¬ decide (is_safe_at h𝕏 n v)) then [walker.actions n.val] else []) + + def get_unsafe_pos : List Pos := + (get_unsafe_reads h𝕏).flatMap (fun | VarAction.Read _ pos => [pos] | _ => []) + + --def print_unsafe_reads : String := + --(get_unsafe_reads h𝕏).foldl + def decide_safety : Maybe (is_safe h𝕏) := by { let safe := forall_fin (fun n ↦ forall_fin (fun v ↦ decide (is_safe_at h𝕏 n v))) by_cases safety : safe - swap; apply Maybe.No -- if any reads occur where a var isnt def this will hit and fail + swap; + -- if any reads occur where a var isnt def this will hit and fail + apply Maybe.NoBC; apply kernel_highlighted_repr; apply get_unsafe_pos h𝕏 apply Maybe.Yes unfold is_safe intro n v @@ -545,8 +566,13 @@ section WithKernel def decide_sound : Maybe (walker.sound) := by { clear h𝕏 - cases decide_success with | No => apply Maybe.No | Yes success - cases (decide_safety success) with | No => apply Maybe.No | Yes safety + cases decide_success with + | No | NoBC _ => apply Maybe.No + | Yes success + cases (decide_safety success) with + | No => apply Maybe.No + | NoBC s => apply Maybe.NoBC s + | Yes safety apply Maybe.Yes apply no_read_without_a_write success intro n v h @@ -559,8 +585,8 @@ end WithKernel instance : HasKernel := safe_kernel_1 -#eval decide_sound.well? +#eval decide_sound instance : HasKernel := unsafe_kernel_2 -#eval decide_sound.well? +#eval decide_sound From 3322e6990e3803071b15bb97cf97e2687d679147 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Mon, 21 Jul 2025 11:36:59 -0400 Subject: [PATCH 27/33] tweak tests --- .gitignore | 2 + KLR/Compile/DataflowTestKernels.lean | 274 ++++++++++++++++++++++++++- KLR/Compile/NKIDataflow.lean | 6 +- 3 files changed, 277 insertions(+), 5 deletions(-) diff --git a/.gitignore b/.gitignore index 06544383..d647d149 100644 --- a/.gitignore +++ b/.gitignore @@ -13,3 +13,5 @@ KLR/test.py .gitignore KLR/Compile/test.lean KLR/test.ast +KLR/.DS_Store +.DS_Store diff --git a/KLR/Compile/DataflowTestKernels.lean b/KLR/Compile/DataflowTestKernels.lean index 123079d1..24ecd386 100644 --- a/KLR/Compile/DataflowTestKernels.lean +++ b/KLR/Compile/DataflowTestKernels.lean @@ -134,12 +134,9 @@ def safe_kernel_1 : HasKernel where pos := { line := 10, column := 1, lineEnd := some 10, columnEnd := some 5 } }], args := [] } - -#eval safe_kernel_1.kernel_str.toList[0] = '\n' - def unsafe_kernel_2 : HasKernel where kernel_str := " - def test(): +def test(): x = 0 c = 0 p = 0 @@ -245,4 +242,273 @@ def unsafe_kernel_2 : HasKernel where args := [] } +def unsafe_kernel_3 : HasKernel where + kernel_str := " +def test(): + x = 0 + c = 0 + p = 0 + if c: + p(x) + for z in x: + w = 0 + p(w) + p(z) + p(w) + p(z) + else: + y = 0 + p(x) + p(y) + p(x) + p(y) + p(z)" + kernel := {name := "test.test", + file := "unknown", + line := 1, + body := [{ stmt := KLR.NKI.Stmt'.assign + { expr := KLR.NKI.Expr'.var "x", + pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 2 } } + none + (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 2, column := 5, lineEnd := some 2, columnEnd := some 6 } }), + pos := { line := 2, column := 1, lineEnd := some 2, columnEnd := some 6 } }, + { stmt := KLR.NKI.Stmt'.assign + { expr := KLR.NKI.Expr'.var "c", + pos := { line := 3, column := 1, lineEnd := some 3, columnEnd := some 2 } } + none + (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 3, column := 5, lineEnd := some 3, columnEnd := some 6 } }), + pos := { line := 3, column := 1, lineEnd := some 3, columnEnd := some 6 } }, + { stmt := KLR.NKI.Stmt'.assign + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 4, column := 1, lineEnd := some 4, columnEnd := some 2 } } + none + (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 4, column := 5, lineEnd := some 4, columnEnd := some 6 } }), + pos := { line := 4, column := 1, lineEnd := some 4, columnEnd := some 6 } }, + { stmt := KLR.NKI.Stmt'.ifStm + { expr := KLR.NKI.Expr'.var "c", + pos := { line := 5, column := 4, lineEnd := some 5, columnEnd := some 5 } } + [{ stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 6, + column := 2, + lineEnd := some 6, + columnEnd := some 3 } } + [{ expr := KLR.NKI.Expr'.var "x", + pos := { line := 6, + column := 4, + lineEnd := some 6, + columnEnd := some 5 } }] + [], + pos := { line := 6, + column := 2, + lineEnd := some 6, + columnEnd := some 6 } }, + pos := { line := 6, column := 2, lineEnd := some 6, columnEnd := some 6 } }, + { stmt := KLR.NKI.Stmt'.forLoop + { expr := KLR.NKI.Expr'.var "z", + pos := { line := 7, + column := 6, + lineEnd := some 7, + columnEnd := some 7 } } + { expr := KLR.NKI.Expr'.var "x", + pos := { line := 7, + column := 11, + lineEnd := some 7, + columnEnd := some 12 } } + [{ stmt := KLR.NKI.Stmt'.assign + { expr := KLR.NKI.Expr'.var "w", + pos := { line := 8, + column := 3, + lineEnd := some 8, + columnEnd := some 4 } } + none + (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 8, + column := 7, + lineEnd := some 8, + columnEnd := some 8 } }), + pos := { line := 8, + column := 3, + lineEnd := some 8, + columnEnd := some 8 } }, + { stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 9, + column := 3, + lineEnd := some 9, + columnEnd := some 4 } } + [{ expr := KLR.NKI.Expr'.var "w", + pos := { line := 9, + column := 5, + lineEnd := some 9, + columnEnd := some 6 } }] + [], + pos := { line := 9, + column := 3, + lineEnd := some 9, + columnEnd := some 7 } }, + pos := { line := 9, + column := 3, + lineEnd := some 9, + columnEnd := some 7 } }, + { stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 10, + column := 3, + lineEnd := some 10, + columnEnd := some 4 } } + [{ expr := KLR.NKI.Expr'.var "z", + pos := { line := 10, + column := 5, + lineEnd := some 10, + columnEnd := some 6 } }] + [], + pos := { line := 10, + column := 3, + lineEnd := some 10, + columnEnd := some 7 } }, + pos := { line := 10, + column := 3, + lineEnd := some 10, + columnEnd := some 7 } }], + pos := { line := 7, column := 2, lineEnd := some 10, columnEnd := some 7 } }, + { stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 11, + column := 2, + lineEnd := some 11, + columnEnd := some 3 } } + [{ expr := KLR.NKI.Expr'.var "w", + pos := { line := 11, + column := 4, + lineEnd := some 11, + columnEnd := some 5 } }] + [], + pos := { line := 11, + column := 2, + lineEnd := some 11, + columnEnd := some 6 } }, + pos := { line := 11, column := 2, lineEnd := some 11, columnEnd := some 6 } }, + { stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 12, + column := 2, + lineEnd := some 12, + columnEnd := some 3 } } + [{ expr := KLR.NKI.Expr'.var "z", + pos := { line := 12, + column := 4, + lineEnd := some 12, + columnEnd := some 5 } }] + [], + pos := { line := 12, + column := 2, + lineEnd := some 12, + columnEnd := some 6 } }, + pos := { line := 12, column := 2, lineEnd := some 12, columnEnd := some 6 } }] + [{ stmt := KLR.NKI.Stmt'.assign + { expr := KLR.NKI.Expr'.var "y", + pos := { line := 14, + column := 2, + lineEnd := some 14, + columnEnd := some 3 } } + none + (some { expr := KLR.NKI.Expr'.value (KLR.NKI.Value.int 0), + pos := { line := 14, + column := 6, + lineEnd := some 14, + columnEnd := some 7 } }), + pos := { line := 14, column := 2, lineEnd := some 14, columnEnd := some 7 } }, + { stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 15, + column := 2, + lineEnd := some 15, + columnEnd := some 3 } } + [{ expr := KLR.NKI.Expr'.var "x", + pos := { line := 15, + column := 4, + lineEnd := some 15, + columnEnd := some 5 } }] + [], + pos := { line := 15, + column := 2, + lineEnd := some 15, + columnEnd := some 6 } }, + pos := { line := 15, column := 2, lineEnd := some 15, columnEnd := some 6 } }, + { stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 16, + column := 2, + lineEnd := some 16, + columnEnd := some 3 } } + [{ expr := KLR.NKI.Expr'.var "y", + pos := { line := 16, + column := 4, + lineEnd := some 16, + columnEnd := some 5 } }] + [], + pos := { line := 16, + column := 2, + lineEnd := some 16, + columnEnd := some 6 } }, + pos := { line := 16, column := 2, lineEnd := some 16, columnEnd := some 6 } }], + pos := { line := 5, column := 1, lineEnd := some 16, columnEnd := some 6 } }, + { stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 17, + column := 1, + lineEnd := some 17, + columnEnd := some 2 } } + [{ expr := KLR.NKI.Expr'.var "x", + pos := { line := 17, + column := 3, + lineEnd := some 17, + columnEnd := some 4 } }] + [], + pos := { line := 17, column := 1, lineEnd := some 17, columnEnd := some 5 } }, + pos := { line := 17, column := 1, lineEnd := some 17, columnEnd := some 5 } }, + { stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 18, + column := 1, + lineEnd := some 18, + columnEnd := some 2 } } + [{ expr := KLR.NKI.Expr'.var "y", + pos := { line := 18, + column := 3, + lineEnd := some 18, + columnEnd := some 4 } }] + [], + pos := { line := 18, column := 1, lineEnd := some 18, columnEnd := some 5 } }, + pos := { line := 18, column := 1, lineEnd := some 18, columnEnd := some 5 } }, + { stmt := KLR.NKI.Stmt'.expr + { expr := KLR.NKI.Expr'.call + { expr := KLR.NKI.Expr'.var "p", + pos := { line := 19, + column := 1, + lineEnd := some 19, + columnEnd := some 2 } } + [{ expr := KLR.NKI.Expr'.var "z", + pos := { line := 19, + column := 3, + lineEnd := some 19, + columnEnd := some 4 } }] + [], + pos := { line := 19, column := 1, lineEnd := some 19, columnEnd := some 5 } }, + pos := { line := 19, column := 1, lineEnd := some 19, columnEnd := some 5 } }], + args := [] } + end TestKernels diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index b7ac98c5..3f3d1460 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -583,10 +583,14 @@ section WithKernel } end WithKernel -instance : HasKernel := safe_kernel_1 +instance : HasKernel := safe_kernel_1 #eval decide_sound instance : HasKernel := unsafe_kernel_2 #eval decide_sound + +instance : HasKernel := unsafe_kernel_3 + +#eval decide_sound From 54a6ca570ff948a855b40b8e09e82c454495de98 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Mon, 21 Jul 2025 11:46:27 -0400 Subject: [PATCH 28/33] tweaks --- KLR/Compile/NKIDataflow.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index 3f3d1460..76b38759 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -275,12 +275,15 @@ section DefNKIWalker let complete := else_walker.processAction VarAction.None complete.addEdge then_walker.last_node complete.last_node | Stmt'.forLoop (x : Expr) (iter: Expr) (body: List Stmt) => - let intro_walker := (walker.processExpr x).processExpr iter + let intro_walker := walker.processExpr iter let outer_breaks := intro_walker.breaks let outer_conts := intro_walker.conts let inner_walker := ((intro_walker.clearBreaks).clearConts).processAction VarAction.None let enter_node := inner_walker.last_node - let inner_walked := inner_walker.processStmtList body + let inner_pre_walk := match x with + | ⟨Expr'.var name, pos⟩ => inner_walker.processAction (VarAction.Write name none pos) + | _ => inner_walker + let inner_walked := inner_pre_walk.processStmtList body let nearly_complete := (inner_walked.addEdge inner_walked.last_node enter_node).setLast enter_node let complete := nearly_complete.processAction VarAction.None let exit_node := complete.last_node From 67bfd0df852bb3a0b9ec25c97d5ee07c49941278 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Mon, 21 Jul 2025 11:53:46 -0400 Subject: [PATCH 29/33] tweaks - its pretty good abt to show it to paul --- KLR/Compile/DataflowTestKernels.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/KLR/Compile/DataflowTestKernels.lean b/KLR/Compile/DataflowTestKernels.lean index 24ecd386..f62f8294 100644 --- a/KLR/Compile/DataflowTestKernels.lean +++ b/KLR/Compile/DataflowTestKernels.lean @@ -3,6 +3,9 @@ open KLR.NKI section TestKernels +def start_highlight := "⦃!" --"◯" --"⇉" +def end_highlight := "⦄" --"◯" --"⇇" + class HasKernel where kernel : Fun kernel_str : String @@ -19,8 +22,8 @@ def highlight_pos_set [HasKernel] (actions : List Pos) (s : String) : String := let starts := actions.flatMap findStart let ends := actions.flatMap findEnd let out_str_at n : List Char := - let st := if n ∈ starts then ['⟦'] else [] - let ed := if n ∈ ends then ['⟧'] else [] + let st := if n ∈ starts then start_highlight.toList else [] + let ed := if n ∈ ends then end_highlight.toList else [] st ++ ed ++ [s.toList[n]!] ⟨((List.range s.length).flatMap out_str_at)⟩ From 9af11764c283a8b7a7fb24d832c488de95d8fbda Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Wed, 23 Jul 2025 10:03:20 -0400 Subject: [PATCH 30/33] bugfix --- KLR/Compile/NKIDataflow.lean | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index 76b38759..4064a3fc 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -59,9 +59,9 @@ section DefNKIWalker String.intercalate "\n" ((List.range walker.num_nodes).map row ++ ["vars: ", walker.vars.toString]) def NKIWalker.init : NKIWalker := { - num_nodes := 1 + num_nodes := 1 -- zero is always the first node num_nodes_nonzero := by trivial - last_node := 0 + last_node := 0 -- zero is always the first node actions _ := VarAction.None edges _ _ := false breaks := [] @@ -270,8 +270,9 @@ section DefNKIWalker let withe := (match e with | some e => withty.processExpr e | none => withty) withe.processAction (VarAction.Write "" ty pos) | Stmt'.ifStm (e : Expr) (thn : List Stmt) (els : List Stmt) => - let then_walker := (walker.processExpr e).processStmtList thn - let else_walker := (then_walker.setLast walker.last_node).processStmtList els + let cond_walker := walker.processExpr e + let then_walker := cond_walker.processStmtList thn + let else_walker := (then_walker.setLast cond_walker.last_node).processStmtList els let complete := else_walker.processAction VarAction.None complete.addEdge then_walker.last_node complete.last_node | Stmt'.forLoop (x : Expr) (iter: Expr) (body: List Stmt) => @@ -313,6 +314,18 @@ section DefNKIWalker body_walker.rets.foldl (fun walker ret ↦ walker.addEdge ret body_walker.last_node) body_walker + -- WIP + def NKIWalker.processCoFun (f : Fun) : NKIWalker := + let walker := processFun f + let invert n := walker.num_nodes - n - 1 + let invert_action := fun + | VarAction.Read name pos => VarAction.Write name none pos + | VarAction.Write name _ pos => VarAction.Read name pos + | VarAction.None => VarAction.None + {walker with + edges n₀ n₁ := walker.edges (invert n₁) (invert n₀) + actions n := invert_action (walker.actions (invert n))} + def NKIWalker.isClosed (walker : NKIWalker) := walker.breaks.isEmpty ∧ walker.conts.isEmpty end DefNKIWalker From c46f66a2cee3d49a2c0a72cf7c3be9064a12e858 Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Wed, 23 Jul 2025 10:25:21 -0400 Subject: [PATCH 31/33] refactor fake modules --- KLR/Compile/NKIDataflow.lean | 369 ++++++++++++++++++----------------- 1 file changed, 187 insertions(+), 182 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index 4064a3fc..ebeaaf07 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -331,7 +331,7 @@ section DefNKIWalker end DefNKIWalker section WithKernel - variable [HasKernel] + variable [HK : HasKernel] abbrev 𝕂 := HasKernel.kernel @@ -378,224 +378,229 @@ section WithKernel (transitions:=transitions)).map (fun a ↦ {a with key_labels k := walker.vars[k]? }) + class HasSuccess where + success : 𝕏opt.isSome + section WithSuccess + variable [HS : HasSuccess] - variable (h𝕏 : 𝕏opt.isSome) - abbrev 𝕏 := 𝕏opt.get h𝕏 - abbrev ℙ := walker.Path - abbrev 𝕟 := walker.Node - abbrev 𝕍 := walker.Var - abbrev 𝔼 (n₀ n₁ : walker.Node) := walker.edges n₀.val n₁.val + abbrev 𝕏 := 𝕏opt.get HasSuccess.success + abbrev ℙ := walker.Path + abbrev 𝕟 := walker.Node + abbrev 𝕍 := walker.Var + abbrev 𝔼 (n₀ n₁ : walker.Node) := walker.edges n₀.val n₁.val - abbrev ν (n : 𝕟) (v : 𝕍) := (𝕏 h𝕏).vals n.val v.val n.isLt v.isLt + abbrev ν (n : 𝕟) (v : 𝕍) := 𝕏.vals n.val v.val n.isLt v.isLt - abbrev σ (n₀ n₁ : 𝕟) (v : 𝕍) (𝔼n:𝔼 n₀ n₁): transitions n₀.val v.val (ν h𝕏 n₀ v) ≤ ν h𝕏 n₁ v := by { - apply (𝕏 h𝕏).props n₀.val n₁.val v.val n₀.isLt n₁.isLt v.isLt 𝔼n - } + abbrev σ (n₀ n₁ : 𝕟) (v : 𝕍) (𝔼n:𝔼 n₀ n₁): transitions n₀.val v.val (ν n₀ v) ≤ ν n₁ v := by { + apply 𝕏.props n₀.val n₁.val v.val n₀.isLt n₁.isLt v.isLt 𝔼n + } - --#check 𝕏 - --#check ν - --#check σ - --#check ℙ - - abbrev var_def (n : 𝕟) (v : 𝕍) : Bool := ¬ν h𝕏 n v - def NKIWalker.Path.var_def_at_terminus (𝕡 : ℙ) (v : 𝕍) : Bool := 𝕡.true_at_terminus walker (var_def h𝕏 . v) - - def NKIWalker.Path.not_def_at_entry (𝕡 : ℙ) (v : 𝕍) : 𝕡.nodes.length = 1 → ¬ 𝕡.var_def_at_terminus h𝕏 v := - match h : 𝕡.nodes with - | [n] => by { - intro - cases v - rename_i k hk - simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.true_at_terminus] - rw [h] - simp - have h_edge: walker.edges 0 n.val := by { - have h𝕡 := 𝕡.nodes_sound - unfold NKIWalker.is_path at h𝕡 - rw [h] at h𝕡 - simp at h𝕡 - assumption + --#check 𝕏 + --#check ν + --#check σ + --#check ℙ + + abbrev var_def (n : 𝕟) (v : 𝕍) : Bool := ν n v = false + def NKIWalker.Path.var_def_at_terminus (𝕡 : ℙ) (v : 𝕍) : Bool := 𝕡.true_at_terminus walker (var_def . v) + + def NKIWalker.Path.not_def_at_entry (𝕡 : ℙ) (v : 𝕍) : 𝕡.nodes.length = 1 → ¬ 𝕡.var_def_at_terminus v := + match h : 𝕡.nodes with + | [n] => by { + intro + cases v + rename_i k hk + simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.true_at_terminus] + rw [h] + simp + have h_edge: walker.edges 0 n.val := by { + have h𝕡 := 𝕡.nodes_sound + unfold NKIWalker.is_path at h𝕡 + rw [h] at h𝕡 + simp at h𝕡 + assumption + } + apply σ ⟨0, walker.num_nodes_nonzero⟩ n ⟨k, hk⟩ h_edge + simp [transitions, LE.le, instLEOfPreorder, Preorder.toLE, instPreorderBool_compile, Bool.instLE] } - apply σ h𝕏 ⟨0, walker.num_nodes_nonzero⟩ n ⟨k, hk⟩ h_edge - simp [transitions, LE.le, instLEOfPreorder, Preorder.toLE, instPreorderBool_compile, Bool.instLE] - } - | [] | _ :: _ :: _ => by simp + | [] | _ :: _ :: _ => by simp - @[simp] - abbrev NKIWalker.Path.motive (𝕡 : ℙ) (v : 𝕍) : Prop - := 𝕡.var_def_at_terminus h𝕏 v → 𝕡.writes_somewhere walker v + @[simp] + abbrev NKIWalker.Path.motive (𝕡 : ℙ) (v : 𝕍) : Prop + := 𝕡.var_def_at_terminus v → 𝕡.writes_somewhere walker v - @[simp] - abbrev length_motive n := ∀ (𝕡 : ℙ) v, 𝕡.nodes.length = n → (𝕡.motive h𝕏 v) + @[simp] + abbrev length_motive n := ∀ (𝕡 : ℙ) v, 𝕡.nodes.length = n → (𝕡.motive v) - abbrev sound_at_zero : length_motive h𝕏 0 := by { - simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.true_at_terminus, NKIWalker.Path.writes_somewhere] - intro _ _ is_zero - simp [is_zero] - } - - abbrev sound_at_one : length_motive h𝕏 1 := by { - simp - intro 𝕡 v _ _ - exfalso - apply (𝕡.not_def_at_entry h𝕏 v) - assumption - assumption - } + abbrev sound_at_zero : length_motive 0 := by { + simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.true_at_terminus, NKIWalker.Path.writes_somewhere] + intro _ _ is_zero + simp [is_zero] + } - abbrev sound_ind : ∀ len, len ≥ 1 → length_motive h𝕏 len → length_motive h𝕏 (len + 1) := by { - unfold length_motive - intro len len_nonzero IndHyp 𝕡₁ v 𝕡₁_len ν₁ - cases 𝕡₁_def : 𝕡₁ - rename_i nodes₁ is_path₁ - let ⟨n₁, n₀, tl₀, ε, unroll, is_path₀⟩ := 𝕡₁.unroll walker (by omega) - simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.true_at_terminus, ←unroll] at ν₁ - let 𝕡₀ : ℙ := ⟨n₀ :: tl₀, is_path₀⟩ - cases ν₀ : ν h𝕏 n₀ v - { - -- v is defined at n₀ - the terminus of 𝕡₀, so writes somewhere by ind hypo, then lift - rw [←𝕡₁_def] - apply (NKIWalker.Path.writes_somewhere_lifts walker 𝕡₀ 𝕡₁ v); simp [←unroll, 𝕡₀] - apply IndHyp - simp [←unroll] at 𝕡₁_len - simp [𝕡₀] + abbrev sound_at_one : length_motive 1 := by { + simp + intro 𝕡 v _ _ + exfalso + apply (𝕡.not_def_at_entry v) assumption - simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.true_at_terminus, 𝕡₀] assumption } - { - -- is not defined at n₀ -- the terminus of 𝕡₀, but is at n₁, the terminus of 𝕡₁ - -- since we have ε : edge from n₀ to n₁, σ n₀ n₀ - let σ' := σ h𝕏 n₀ n₁ v ε - simp [transitions, LE.le, instLEOfPreorder, Preorder.toLE, instPreorderBool_compile, Bool.instLE, ν₀, ν₁] at σ' - let ⟨_, σ''⟩ := σ' - cases action_def : walker.actions n₀.val <;> rw [action_def] at σ'' <;> try simp at σ'' - rename_i _ name _ - simp [NKIWalker.Path.writes_somewhere] - simp [𝕡₁_def] at unroll - simp [←unroll, action_def, NKIWalker.writes] - apply Or.inl - assumption - } - } - - abbrev sound_everywhere : ∀ n, length_motive h𝕏 n := fun - | 0 => sound_at_zero h𝕏 - | 1 => sound_at_one h𝕏 - | n + 2 => sound_ind h𝕏 (n + 1) (by omega) (sound_everywhere (n + 1)) - - def no_def_without_a_write : ∀ (𝕡 : ℙ) v, (𝕡.var_def_at_terminus h𝕏 v) → (𝕡.writes_somewhere walker v) := by { - intro 𝕡 v - apply sound_everywhere - rfl - } - - abbrev is_safe_at (n : 𝕟) (v : 𝕍) : Prop := walker.reads n v → var_def h𝕏 n v - abbrev is_safe : Prop := ∀ (n : 𝕟) (v : 𝕍), is_safe_at h𝕏 n v - - abbrev local_safety_decidable : ∀ n v, Decidable (is_safe_at h𝕏 n v) := by { - intro n v - unfold is_safe_at - cases reads? : walker.reads n v <;> - cases defs? : var_def h𝕏 n v <;> - simp [is_safe_at] <;> try {apply isTrue; trivial} - apply isFalse; trivial - } + abbrev sound_ind : ∀ len, len ≥ 1 → length_motive len → length_motive (len + 1) := by { + unfold length_motive + intro len len_nonzero IndHyp 𝕡₁ v 𝕡₁_len ν₁ + cases 𝕡₁_def : 𝕡₁ + rename_i nodes₁ is_path₁ + let ⟨n₁, n₀, tl₀, ε, unroll, is_path₀⟩ := 𝕡₁.unroll walker (by omega) + simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.true_at_terminus, ←unroll] at ν₁ + let 𝕡₀ : ℙ := ⟨n₀ :: tl₀, is_path₀⟩ + cases ν₀ : ν n₀ v + { + -- v is defined at n₀ - the terminus of 𝕡₀, so writes somewhere by ind hypo, then lift + rw [←𝕡₁_def] + apply (NKIWalker.Path.writes_somewhere_lifts walker 𝕡₀ 𝕡₁ v); simp [←unroll, 𝕡₀] + apply IndHyp + simp [←unroll] at 𝕡₁_len + simp [𝕡₀] + assumption + simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.true_at_terminus, 𝕡₀] + assumption + } + { + -- is not defined at n₀ -- the terminus of 𝕡₀, but is at n₁, the terminus of 𝕡₁ + -- since we have ε : edge from n₀ to n₁, σ n₀ n₀ + let σ' := σ n₀ n₁ v ε + simp [transitions, LE.le, instLEOfPreorder, Preorder.toLE, instPreorderBool_compile, Bool.instLE, ν₀, ν₁] at σ' + let ⟨_, σ''⟩ := σ' + cases action_def : walker.actions n₀.val <;> rw [action_def] at σ'' <;> try simp at σ'' + rename_i _ name _ + simp [NKIWalker.Path.writes_somewhere] + simp [𝕡₁_def] at unroll + simp [←unroll, action_def, NKIWalker.writes] + apply Or.inl + assumption + } + } - inductive Maybe (P : Prop) -- option type plus message option - | Yes : P → Maybe P - | No : Maybe P - | NoBC : String → Maybe P --no because of message + abbrev sound_everywhere : ∀ n, length_motive n := fun + | 0 => sound_at_zero + | 1 => sound_at_one + | n + 2 => sound_ind (n + 1) (by omega) (sound_everywhere (n + 1)) - instance Maybe.toString : ToString (Maybe P) where - toString := fun - | Yes _ => s!"YES [SAFETY PROVEN]" - | No => "NO [SAFETY NOT PROVEN]" - | NoBC s => s!"NO [SAFETY NOT PROVEN] BECAUSE: {s}" - - def Maybe.well? (s : Maybe P) := match s with - | No => false - | _ => true - - def decide_success : Maybe (𝕏opt.isSome) := by { - cases h : 𝕏opt with | none => apply Maybe.No | some => { - apply Maybe.Yes; simp - } - } + def no_def_without_a_write : ∀ (𝕡 : ℙ) v, (𝕡.var_def_at_terminus v) → (𝕡.writes_somewhere walker v) := by { + intro 𝕡 v + apply sound_everywhere + rfl + } - abbrev forall_fin {n} (f : Fin n → Bool) : Bool := (Vector.ofFn f).all (.) + abbrev is_safe_at (n : 𝕟) (v : 𝕍) : Prop := walker.reads n v → var_def n v - abbrev forall_fin_sound (f : Fin n → Bool) : forall_fin f → (m : Fin n) → (f m) := by { - simp [forall_fin] - intro h m - apply h - } + abbrev is_safe : Prop := ∀ (n : 𝕟) (v : 𝕍), is_safe_at n v - abbrev 𝕀 (α) (a : α) := a + abbrev local_safety_decidable : ∀ n v, Decidable (is_safe_at n v) := by { + intro n v + unfold is_safe_at + cases reads? : walker.reads n v <;> + cases defs? : var_def n v <;> + simp [is_safe_at] <;> try {apply isTrue; trivial} + apply isFalse; trivial + } - def get_unsafe_reads : List VarAction := - (List.ofFn (fun n : 𝕟 ↦ (n, List.ofFn (𝕀 𝕍)))).flatMap (fun (n, vs) ↦ - if vs.any (fun v ↦ ¬ decide (is_safe_at h𝕏 n v)) then [walker.actions n.val] else []) + inductive Maybe (P : Prop) -- option type plus message option + | Yes : P → Maybe P + | No : Maybe P + | NoBC : String → Maybe P --no because of message - def get_unsafe_pos : List Pos := - (get_unsafe_reads h𝕏).flatMap (fun | VarAction.Read _ pos => [pos] | _ => []) + instance Maybe.toString : ToString (Maybe P) where + toString := fun + | Yes _ => s!"YES [SAFETY PROVEN]" + | No => "NO [SAFETY NOT PROVEN]" + | NoBC s => s!"NO [SAFETY NOT PROVEN] BECAUSE: {s}" - --def print_unsafe_reads : String := - --(get_unsafe_reads h𝕏).foldl + def Maybe.well? (s : Maybe P) := match s with + | No => false + | _ => true - def decide_safety : Maybe (is_safe h𝕏) := by { - let safe := forall_fin (fun n ↦ forall_fin (fun v ↦ decide (is_safe_at h𝕏 n v))) - by_cases safety : safe - swap; - -- if any reads occur where a var isnt def this will hit and fail - apply Maybe.NoBC; apply kernel_highlighted_repr; apply get_unsafe_pos h𝕏 - apply Maybe.Yes - unfold is_safe - intro n v - have safety_at_n := forall_fin_sound _ safety n - have safety := (forall_fin_sound _ safety_at_n v) - apply of_decide_eq_true - assumption - } + def decide_success : Maybe (𝕏opt.isSome) := by { + cases h : 𝕏opt with | none => apply Maybe.No | some => { + apply Maybe.Yes; simp + } + } - section IfSafe - variable (safety : ∀ (n : 𝕟) (v : 𝕍), walker.reads n v → ¬ν h𝕏 n v) + abbrev forall_fin {n} (f : Fin n → Bool) : Bool := (Vector.ofFn f).all (.) - def no_read_without_a_def : ∀ (𝕡 : ℙ) v, (𝕡.reads_at_terminus walker v) → (𝕡.var_def_at_terminus h𝕏 v) - := by { - simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.reads_at_terminus, NKIWalker.Path.true_at_terminus] - intro 𝕡 v h - cases nodes_def : 𝕡.nodes with | nil | cons n ℓ <;> simp_all [nodes_def] - } + abbrev forall_fin_sound (f : Fin n → Bool) : forall_fin f → (m : Fin n) → (f m) := by { + simp [forall_fin] + intro h m + apply h + } - def no_read_without_a_write : walker.sound := by { - unfold NKIWalker.sound - intro 𝕡 name reads - apply no_def_without_a_write - apply no_read_without_a_def - assumption + abbrev 𝕀 (α) (a : α) := a + + def get_unsafe_reads : List VarAction := + (List.ofFn (fun n : 𝕟 ↦ (n, List.ofFn (𝕀 𝕍)))).flatMap (fun (n, vs) ↦ + if vs.any (fun v ↦ ¬ decide (is_safe_at n v)) then [walker.actions n.val] else []) + + def get_unsafe_pos : List Pos := + get_unsafe_reads.flatMap (fun | VarAction.Read _ pos => [pos] | _ => []) + + --def print_unsafe_reads : String := + --(get_unsafe_reads h𝕏).foldl + + def decide_safety : Maybe is_safe := by { + let safe := forall_fin (fun n ↦ forall_fin (fun v ↦ decide (is_safe_at n v))) + by_cases safety : safe + swap; + -- if any reads occur where a var isnt def this will hit and fail + apply Maybe.NoBC; apply kernel_highlighted_repr; apply get_unsafe_pos + apply Maybe.Yes + unfold is_safe + intro n v + have safety_at_n := forall_fin_sound _ safety n + have safety := (forall_fin_sound _ safety_at_n v) + apply of_decide_eq_true assumption } - end IfSafe + + class IsSafe where + safety : is_safe + section WithSafety + variable [IS : IsSafe] + + def no_read_without_a_def : ∀ (𝕡 : ℙ) v, (𝕡.reads_at_terminus walker v) → (𝕡.var_def_at_terminus v) + := by { + simp [NKIWalker.Path.var_def_at_terminus, NKIWalker.Path.reads_at_terminus, NKIWalker.Path.true_at_terminus] + intro 𝕡 v h + cases nodes_def : 𝕡.nodes with | nil | cons n ℓ <;> simp_all + let safety := IS.safety + simp [is_safe, is_safe_at] at safety + apply safety + assumption + } + + def no_read_without_a_write : walker.sound := by { + unfold NKIWalker.sound + intro 𝕡 name reads + apply no_def_without_a_write + apply no_read_without_a_def + assumption + } + end WithSafety + end WithSuccess def decide_sound : Maybe (walker.sound) := by { - clear h𝕏 cases decide_success with | No | NoBC _ => apply Maybe.No | Yes success - cases (decide_safety success) with + have HS : HasSuccess := ⟨success⟩ + cases decide_safety with | No => apply Maybe.No | NoBC s => apply Maybe.NoBC s | Yes safety + have IS : IsSafe := ⟨safety⟩ apply Maybe.Yes - apply no_read_without_a_write success - intro n v h - have specific_safety := safety n v h - simp [is_safe_at, var_def] at specific_safety - rw [specific_safety] - trivial + apply no_read_without_a_write } end WithKernel From 75685c268e206114fbfe1099082970997183b95c Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Wed, 23 Jul 2025 12:21:09 -0400 Subject: [PATCH 32/33] add comments --- KLR/Compile/DataflowTestKernels.lean | 7 ++++ KLR/Compile/NKIDataflow.lean | 63 ++++++++++++++++++++++++---- 2 files changed, 62 insertions(+), 8 deletions(-) diff --git a/KLR/Compile/DataflowTestKernels.lean b/KLR/Compile/DataflowTestKernels.lean index f62f8294..a42ee4b7 100644 --- a/KLR/Compile/DataflowTestKernels.lean +++ b/KLR/Compile/DataflowTestKernels.lean @@ -1,3 +1,10 @@ +/- + This file defines a `class HasKernel` that can provide an instance of a NKI kernel function + if present. it also defines a few instances of this class corresponding to different kernels. + `kernel_str : String` is an additional attribute of `HasKernel` that records the source-level + code for output sake. +-/ + import KLR.NKI.Basic open KLR.NKI diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index ebeaaf07..21025ce7 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -2,13 +2,60 @@ # NKI Dataflow This file uses the Dataflow solver (`InnerMapImpl.Solution`) from `Dataflow.lean` -to analyize NKI functions. - -For example, see `test_kernel` below, serialized NKI ASTs can be generated from `klr compile`, -converted to CFGs by the `NKIWalker` class below, -paired with definitions of variable well-definition corresponding to syntactic defs and uses, -and analyzed to get `𝕏opt : Option SolutionT`, which can be printed to view the liveness of -all variables at all program points `#eval 𝕏opt` +to analyize NKI functions (`HasKernel.kernel`) from `DataflowTestKernels.lean`. +the final output is the def `decide_safety` - it is built on a kernel, a succesful +dataflow solution, and a safety analysis of the kernel. This is all arranges as follows: + +`section DefVarAction` defines the `VarAction` inductive which describes the + semantically significant actions of NKI statements for the sake of our + analysis: namely, named reads and writes to variables. + +`section DefNKIWalker`defines the `NKIWalker` structure that can walk a + NKI AST to construct a walker instance that contains the entire CFG + structure of the kernel: + `def NKIWalker.processFun (f : Fun) : NKIWalker := ...` + +the remainder of the file is organized in a module/functor-like structure +of parameterization of sections on typeclasses. each of the below +sections takes an instance of a class that bundles an important computational +step, and performs computation on it leading to some dependent output. + +`class HasKernel where kernel : Fun` - defined in `DataflowTestKernels.lean`, wraps a `NKI.Fun` kernel function + +`section WithKernel [HasKernel]` - uses a kernel to construct an instance + of a dataflow problem, whose (option-wrapped) solution `𝕏opt` is the final + output + + `class HasSuccess where success : 𝕏opt.isSome` - makes available the result + that the dataflow analysis was succesful, i.e `𝕏opt ≠ none` + + `section WithSuccess [HasSuccess]` - uses a success result to finish defining + our desired semantic properties of paths, and checks source functions + to ensure that reads occur only in places the (succesful) dataflow + analysis deemed safe + + `class HasSafety where safety : is_safe` - makes availabe + the result that the syntactic safety chcking was succesful + + `section WithSafety [HasSafety]` - defines + `def no_read_without_a_write [HasKernel] [HasSuccess] [HasSafety] : walker.sound := ...` + which provides an instance `is_safe`: + `abbrev is_safe : Prop := ∀ (n : 𝕟) (v : 𝕍), walker.reads n v → var_def n v` + of soundness for this NKI program, conditional on + a nki program being avaiable (`HasKernel`), dataflow analysis succeeding (`HasSuccess`) + and syntactic safety checks succeeding (`HasSafety`). + + `def decide_sound [HasKernel]: Maybe (walker.sound) := ...` - + exists inside `WithKernel` (so instantiating depends on a kernel), + but outside `WithSuccess` and `WithSafety` because success and safety + are decided based on the kernel not releid upon as parameters. + +this provides the final workflow: + - provide a NKI kernel to analyze as an `instance : HasKernel` + - read `decide_sound [HasKernel]`, which will evalute all + success and safety checks and provide a result of success, + with propositional proof of desired path semantics, or a + failure with a message constructed from the NKI source -/ import KLR.NKI.Basic @@ -364,7 +411,6 @@ section WithKernel | true => "❌" | false => "✅" - /- perform dataflow analysis -/ @@ -378,6 +424,7 @@ section WithKernel (transitions:=transitions)).map (fun a ↦ {a with key_labels k := walker.vars[k]? }) + class HasSuccess where success : 𝕏opt.isSome section WithSuccess From 412e6174263a48d246dcef63c15152360513c1cc Mon Sep 17 00:00:00 2001 From: Julia Turcotti Date: Mon, 28 Jul 2025 10:58:17 -0400 Subject: [PATCH 33/33] tweaks --- KLR/Compile/NKIDataflow.lean | 25 ++----------------------- 1 file changed, 2 insertions(+), 23 deletions(-) diff --git a/KLR/Compile/NKIDataflow.lean b/KLR/Compile/NKIDataflow.lean index 21025ce7..75c63d16 100644 --- a/KLR/Compile/NKIDataflow.lean +++ b/KLR/Compile/NKIDataflow.lean @@ -256,22 +256,7 @@ section DefNKIWalker def NKIWalker.addReturn (walker : NKIWalker) : NKIWalker := {walker with rets := walker.rets ++ [walker.last_node] } - - /-mutual - def NKIWalker.processExpr (walker : NKIWalker) (expr : Expr) : Nat := - match h : expr.expr with - | Expr'.tuple x => (walker.processExprList x).sum - | _ => 0 - termination_by sizeOf expr - decreasing_by cases expr; simp at h; rw [h]; simp; omega - def NKIWalker.processExprList (walker : NKIWalker) (exprs : List Expr) : List Nat := - exprs.map walker.processExpr - termination_by sizeOf exprs - end-/ - - mutual - - def NKIWalker.processExpr (walker : NKIWalker) (expr : Expr) : NKIWalker := + mutual def NKIWalker.processExpr (walker : NKIWalker) (expr : Expr) : NKIWalker := let ⟨expr, pos⟩ := expr match _ : expr with | Expr'.value _ => walker @@ -293,16 +278,12 @@ section DefNKIWalker try {rename_i expr' _<;> rcases h' : (expr, expr') with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega} try {rcases h' : expr with ⟨⟨⟩, ⟨⟩⟩ <;> simp_all <;> omega} } - - def NKIWalker.processExprList (walker : NKIWalker) (exprs : List Expr) : NKIWalker := exprs.foldl NKIWalker.processExpr walker termination_by sizeOf exprs end - mutual - - def NKIWalker.processStmt (walker : NKIWalker) (stmt : Stmt) : NKIWalker := + mutual def NKIWalker.processStmt (walker : NKIWalker) (stmt : Stmt) : NKIWalker := let ⟨stmt, pos⟩ := stmt match _ : stmt with | Stmt'.expr (e : Expr) => walker.processExpr e @@ -348,8 +329,6 @@ section DefNKIWalker try rcases h : (thn, stmt) with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega try rcases h : (els, stmt) with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega try rcases h : (body, stmt) with ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩ <;> simp_all <;> omega - - def NKIWalker.processStmtList (walker : NKIWalker) (stmts : List Stmt) : NKIWalker := stmts.foldl NKIWalker.processStmt walker termination_by sizeOf stmts