File size: 759 Bytes
ef6eb55 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 | -- PAX IR DAG — PAX-IR module as verified Lean 4 DAG (Layer 2.1)
-- Ahmad Ali Parr · PAX Architecture
namespace PAX.IR_DAG
structure PAXFunction where
name : String
arity : ℕ
arch : String -- "sm_86" | "sm_90"
deriving Repr
structure Value where
id : ℕ
kind : String -- "reg" | "shared" | "global"
deriving Repr
/-- PAX-IR: functions + SSA data flow, no recursive kernels -/
structure PAXModuleDAG where
functions : List PAXFunction
callGraph : List (PAXFunction × PAXFunction)
dataFlow : List (Value × Value)
/-- Call graph acyclicity predicate (no recursive kernels) -/
def isAcyclic (dag : PAXModuleDAG) : Prop :=
∀ f : PAXFunction, ¬ (dag.callGraph.contains (f, f))
end PAX.IR_DAG
|