| -- 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 | |