Structural conversion of sequential GraphSpec chains to DAG terms

This module embeds each sequential primitive as a DAG primitive and lowers composition to explicit SSA-style let bindings.

Lowering: sequential chain → DAG term

GraphSpec has two surface syntaxes:

• NN.GraphSpec.Core: a sequential DSL (Chain + >>>), ideal for pure pipelines.
• NN.GraphSpec.DAG.Core: a general SSA/A-normal-form term language, ideal for sharing/skip connections.

The DAG term language is GraphSpec’s “general graph” core: it is the representation that can express sharing and skip connections.

Chain exists because it is the clearest way to write pipelines, and it has its own direct Spec semantics (Interp.spec) and program translation (Chain.toProgram).

This lowering is still useful whenever you want to embed a sequential pipeline into the DAG world (e.g. to reuse DAG-only tooling, or to keep a single GraphSpec example surface that can export DAG models).

The declarations below provide a structural lowering:

• Chain.toDAGTerm produces a DAG.Term (ps ++ [σ]) τ, i.e. a DAG term whose environment starts with the parameter list ps and ends with the (single) data input σ. Notes:
• The lowering is purely structural: it introduces let1 binders between stages to make the sequential flow explicit in SSA form.
• Each sequential Primitive ps σ τ is embedded as a DAG primitive op with inputs ps ++ [σ]. This embedding is generic: any custom GraphSpec primitive automatically becomes usable in the DAG world.

Lowering internals

The definitions below (castTerm, toTerm, …) are adapters for the structural lowering. The principal entry point is Chain.toDAGTerm.

def NN.GraphSpec.LowerToDAG.castTerm {Γ : List Spec.Shape} {s t : Spec.Shape} (h : s = t) : DAG.Term Γ s → DAG.Term Γ t

Cast a DAG.Term across a proven equality of output shapes.

def NN.GraphSpec.LowerToDAG.castEnvTerm {Γ Γ' : List Spec.Shape} {τ : Spec.Shape} (h : Γ = Γ') : DAG.Term Γ τ → DAG.Term Γ' τ

Cast the environment of a DAG.Term across a proven equality of environments.

List.get lemmas (small, self-contained)

theorem NN.GraphSpec.LowerToDAG.get_append_left_nat {α : Type} (as bs : List α) (i : ℕ) (hi : i < as.length) : (as ++ bs).get ⟨i, ⋯⟩ = as.get ⟨i, hi⟩

List.get into as is unchanged by appending a right list (Nat-index form).

theorem NN.GraphSpec.LowerToDAG.get_append_right_offset_nat {α : Type} (as bs : List α) (j : ℕ) (hj : as.length + j < (as ++ bs).length) : (as ++ bs).get ⟨as.length + j, hj⟩ = bs.get ⟨j, ⋯⟩

List.get into the right list after appending, using an explicit offset as.length + j (Nat-index form).

theorem NN.GraphSpec.LowerToDAG.get_append_last {α : Type} (xs : List α) (x : α) : (xs ++ [x]).get ⟨xs.length, ⋯⟩ = x

List.get of the last element after appending a singleton list.

Primitive embedding: Primitive → DAG.PrimOp

def NN.GraphSpec.LowerToDAG.Primitive.toDAGPrimOp {ps : List Spec.Shape} {σ τ : Spec.Shape} (p : Primitive ps σ τ) : DAG.PrimOp (ps ++ [σ]) τ

Embed a sequential GraphSpec primitive as a DAG primitive op.

The resulting op has input shapes ps ++ [σ] (parameters followed by the data input).

Building well-typed DAG arguments for a primitive call

theorem NN.GraphSpec.LowerToDAG.get_succ {α : Type} (a : α) (as : List α) (i : Fin as.length) : (a :: as).get ⟨↑i + 1, ⋯⟩ = as.get i

def NN.GraphSpec.LowerToDAG.argsOfFn {Γ : List Spec.Shape} (ins : List Spec.Shape) : ((i : Fin ins.length) → DAG.Term Γ (ins.get i)) → DAG.Args Γ ins

Build a typed DAG.Args list from an index-based family of argument terms.

This is the bridge from “arguments as a function of Fin ins.length” to the inductive DAG.Args encoding used by DAG.Term.op.

def NN.GraphSpec.LowerToDAG.Args.append1 {Γ ps : List Spec.Shape} {σ : Spec.Shape} : DAG.Args Γ ps → DAG.Term Γ σ → DAG.Args Γ (ps ++ [σ])

Append one final term to a typed DAG argument list.

def NN.GraphSpec.LowerToDAG.mkParamTerm {pre ps post extra : List Spec.Shape} (i : Fin ps.length) : DAG.Term (pre ++ ps ++ post ++ extra) (ps.get i)

Reference the ith parameter block inside a larger environment layout.

The surrounding environment is split as pre ++ ps ++ post ++ extra; this helper returns the term that points at parameter i : Fin ps.length while keeping the full ambient environment explicit.

def NN.GraphSpec.LowerToDAG.primCall {pre ps post extra : List Spec.Shape} {σ τ : Spec.Shape} (p : Primitive ps σ τ) (x : DAG.Term (pre ++ ps ++ post ++ extra) σ) : DAG.Term (pre ++ ps ++ post ++ extra) τ

Lower a unary Primitive application into the DAG term language.

Parameters are read from the middle ps segment of the ambient environment, in the same order as the primitive's parameter ABI, and the final data input is supplied by x.

Chain lowering

def NN.GraphSpec.LowerToDAG.toTerm {pre ps post extra : List Spec.Shape} {σ τ : Spec.Shape} (g : Chain ps σ τ) (x : DAG.Term (pre ++ ps ++ post ++ extra) σ) : DAG.Term (pre ++ ps ++ post ++ extra) τ

Lower a sequential Chain to an SSA-style DAG.Term, with parameters read from the environment.

Public API

def NN.GraphSpec.LowerToDAG.Chain.toDAGTerm {ps : List Spec.Shape} {σ τ : Spec.Shape} (g : Chain ps σ τ) : DAG.Term (ps ++ [σ]) τ

Lower a sequential Chain to a DAG term with environment ps ++ [σ].