Pure semantics of GraphSpec DAGs #

This module interprets typed DAG terms and blocks in TorchLean.TensorPack environments and proves that evaluation respects renaming, substitution, inlining, and block composition.

source

def NN.GraphSpec.DAG.Env.tget {α : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {s : Spec.Shape} :

TorchLean.TensorPack α Γ → Var Γ s → TorchLean.Tensor α s

Typed environment lookup for pure tensors.

Instances For

source

@[simp]

theorem NN.GraphSpec.DAG.Env.tget_ofFin {α : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} (env : TorchLean.TensorPack α Γ) (i : Fin Γ.length) :

tget env (Var.ofFin i) = env.get i

Looking up a programmatically selected variable agrees with typed-list lookup.

source

@[simp]

theorem NN.GraphSpec.DAG.Env.tget_append_weakenRight {α : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {s t : Spec.Shape} (env : TorchLean.TensorPack α Γ) (value : TorchLean.Tensor α t) (i : Var Γ s) :

tget (env.append (TorchLean.TensorPack.cons value TorchLean.TensorPack.nil)) i.weakenRight = tget env i

Appending a value does not change the meaning of an existing variable.

source

@[simp]

theorem NN.GraphSpec.DAG.Env.tget_append_inLeft {α : Type} [TorchLean.Storage α] {Γ Δ : List Spec.Shape} {s : Spec.Shape} (left : TorchLean.TensorPack α Γ) (right : TorchLean.TensorPack α Δ) (v : Var Γ s) :

tget (left.append right) (Var.inLeft Δ v) = tget left v

Looking up a variable embedded from the left reads the original left environment.

source

@[simp]

theorem NN.GraphSpec.DAG.Env.tget_append_inRight {α : Type} [TorchLean.Storage α] {Γ Δ : List Spec.Shape} {s : Spec.Shape} (left : TorchLean.TensorPack α Γ) (right : TorchLean.TensorPack α Δ) (v : Var Δ s) :

tget (left.append right) (Var.inRight Γ v) = tget right v

Looking up a variable embedded from the right reads the appended right environment.

source

@[simp]

theorem NN.GraphSpec.DAG.Env.tget_append_last {α : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {s : Spec.Shape} (env : TorchLean.TensorPack α Γ) (value : TorchLean.Tensor α s) :

tget (env.append (TorchLean.TensorPack.cons value TorchLean.TensorPack.nil)) (Var.last Γ) = value

Looking up the final variable returns the value most recently appended to an environment.

Spec interpreter #

source

def NN.GraphSpec.DAG.Term.evalArgs {Γ ins : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Γ) :

Args Γ ins → TorchLean.TensorPack α ins

Evaluate a typed argument list by evaluating each component term under the same environment.

Instances For

source

def NN.GraphSpec.DAG.Term.eval {Γ : List Spec.Shape} {τ : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Γ) :

Term Γ τ → TorchLean.Tensor α τ

Pure evaluation of a DAG term.

This is the “math-first” semantics: we interpret a term as a pure function on tensors. No monads, no mutation, no autograd tape, just the Spec definitions of primitives.

The key runtime discipline is the environment discipline:

var reads from env,
op evaluates its arguments and feeds them to the primitive’s specFwd,
let1 evaluates the bound term once and extends env for the body.

Instances For

source

@[simp]

theorem NN.GraphSpec.DAG.Term.eval_op {Γ ins : List Spec.Shape} {τ : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Γ) (primitive : PrimOp ins τ) (args : Args Γ ins) :

eval env (op primitive args) = primitive.specFwd (evalArgs env args)

Evaluating an operation node first evaluates its typed arguments, then applies the primitive's pure semantics.

source

@[simp]

theorem NN.GraphSpec.DAG.Term.eval_cast {Γ : List Spec.Shape} {σ τ : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Γ) (term : Term Γ σ) (h : σ = τ) :

eval env (term.cast h) = h ▸ eval env term

Evaluating an output-shape cast transports the value along the same shape equality.

Semantics of variable renaming #

source

def NN.GraphSpec.DAG.Env.RenamingSound {α : Type} [TorchLean.Storage α] {Γ Δ : List Spec.Shape} (envΓ : TorchLean.TensorPack α Γ) (envΔ : TorchLean.TensorPack α Δ) (ρ : {s : Spec.Shape} → Var Γ s → Var Δ s) :

Prop

A variable renaming preserves an environment when every renamed lookup has the same value.

Instances For

source

theorem NN.GraphSpec.DAG.Env.RenamingSound.lift_right {α : Type} [TorchLean.Storage α] {Γ Δ : List Spec.Shape} {t : Spec.Shape} {envΓ : TorchLean.TensorPack α Γ} {envΔ : TorchLean.TensorPack α Δ} {ρ : {s : Spec.Shape} → Var Γ s → Var Δ s} (hρ : RenamingSound envΓ envΔ fun {s : Spec.Shape} => ρ) (value : TorchLean.Tensor α t) :

RenamingSound (envΓ.append (TorchLean.TensorPack.cons value TorchLean.TensorPack.nil)) (envΔ.append (TorchLean.TensorPack.cons value TorchLean.TensorPack.nil)) fun {s : Spec.Shape} => Var.liftRight fun {s : Spec.Shape} => ρ

A sound renaming remains sound when the same value is appended to both environments.

source

theorem NN.GraphSpec.DAG.Term.evalArgs_rename {Γ Δ ins : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (envΓ : TorchLean.TensorPack α Γ) (envΔ : TorchLean.TensorPack α Δ) (ρ : {s : Spec.Shape} → Var Γ s → Var Δ s) (hρ : Env.RenamingSound envΓ envΔ fun {s : Spec.Shape} => ρ) (args : Args Γ ins) :

evalArgs envΔ (Args.rename (fun {t : Spec.Shape} => ρ) args) = evalArgs envΓ args

Pure evaluation commutes with a sound renaming of an operation's arguments.

source

theorem NN.GraphSpec.DAG.Term.eval_rename {Γ Δ : List Spec.Shape} {s : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (envΓ : TorchLean.TensorPack α Γ) (envΔ : TorchLean.TensorPack α Δ) (ρ : {t : Spec.Shape} → Var Γ t → Var Δ t) (hρ : Env.RenamingSound envΓ envΔ fun {s : Spec.Shape} => ρ) (term : Term Γ s) :

eval envΔ (rename (fun {t : Spec.Shape} => ρ) term) = eval envΓ term

Pure evaluation commutes with any variable renaming that preserves environment lookup.

source

@[simp]

theorem NN.GraphSpec.DAG.Term.evalArgs_rename_inLeft {Γ Δ ins : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (left : TorchLean.TensorPack α Γ) (right : TorchLean.TensorPack α Δ) (args : Args Γ ins) :

evalArgs (left.append right) (Args.rename (fun {t : Spec.Shape} => Var.inLeft Δ) args) = evalArgs left args

Renaming arguments into the left side of an appended environment preserves their values.

source

@[simp]

theorem NN.GraphSpec.DAG.Term.evalArgs_rename_inRight {Γ Δ ins : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (left : TorchLean.TensorPack α Γ) (right : TorchLean.TensorPack α Δ) (args : Args Δ ins) :

evalArgs (left.append right) (Args.rename (fun {t : Spec.Shape} => Var.inRight Γ) args) = evalArgs right args

Renaming arguments into the right side of an appended environment preserves their values.

source

@[simp]

theorem NN.GraphSpec.DAG.Term.eval_rename_inLeft {Γ Δ : List Spec.Shape} {s : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (left : TorchLean.TensorPack α Γ) (right : TorchLean.TensorPack α Δ) (term : Term Γ s) :

eval (left.append right) (rename (fun {t : Spec.Shape} => Var.inLeft Δ) term) = eval left term

Renaming a term into the left side of an appended environment preserves its value.

source

@[simp]

theorem NN.GraphSpec.DAG.Term.eval_weakenAppend {Γ Δ : List Spec.Shape} {s : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (left : TorchLean.TensorPack α Γ) (right : TorchLean.TensorPack α Δ) (term : Term Γ s) :

eval (left.append right) (weakenAppend Δ term) = eval left term

Appending an arbitrary typed environment does not change a weakened term's value.

source

@[simp]

theorem NN.GraphSpec.DAG.Term.eval_rename_inRight {Γ Δ : List Spec.Shape} {s : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (left : TorchLean.TensorPack α Γ) (right : TorchLean.TensorPack α Δ) (term : Term Δ s) :

eval (left.append right) (rename (fun {t : Spec.Shape} => Var.inRight Γ) term) = eval right term

Renaming a term into the right side of an appended environment preserves its value.

source

@[simp]

theorem NN.GraphSpec.DAG.Term.eval_weakenRight {Γ : List Spec.Shape} {s t : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Γ) (value : TorchLean.Tensor α t) (term : Term Γ s) :

eval (env.append (TorchLean.TensorPack.cons value TorchLean.TensorPack.nil)) term.weakenRight = eval env term

Appending an unrelated value does not change a term's pure meaning.

source

@[simp]

theorem NN.GraphSpec.DAG.Term.eval_var_last_append {Γ : List Spec.Shape} {t : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Γ) (value : TorchLean.Tensor α t) :

eval (env.append (TorchLean.TensorPack.cons value TorchLean.TensorPack.nil)) (var (Var.last Γ)) = value

The final variable in an extended environment denotes the value that was just appended.

source

def NN.GraphSpec.DAG.Env.SubstitutionSound {α : Type} [TorchLean.Storage α] [Context α] {Γ Δ : List Spec.Shape} (envΓ : TorchLean.TensorPack α Γ) (envΔ : TorchLean.TensorPack α Δ) (σ : Substitution Γ Δ) :

Prop

A term substitution represents an environment when every assigned term evaluates to the value stored at the corresponding source variable.

Instances For

source

theorem NN.GraphSpec.DAG.Env.SubstitutionSound.lift_right {α : Type} [TorchLean.Storage α] [Context α] {Γ Δ : List Spec.Shape} {t : Spec.Shape} {envΓ : TorchLean.TensorPack α Γ} {envΔ : TorchLean.TensorPack α Δ} {σ : Substitution Γ Δ} (hσ : SubstitutionSound envΓ envΔ fun {s : Spec.Shape} => σ) (value : TorchLean.Tensor α t) :

SubstitutionSound (envΓ.append (TorchLean.TensorPack.cons value TorchLean.TensorPack.nil)) (envΔ.append (TorchLean.TensorPack.cons value TorchLean.TensorPack.nil)) fun {s : Spec.Shape} => Substitution.liftRight fun {s : Spec.Shape} => σ

A sound substitution remains sound across the value introduced by a let binding.

source

theorem NN.GraphSpec.DAG.Term.evalArgs_substitute {Γ Δ inputs : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (envΓ : TorchLean.TensorPack α Γ) (envΔ : TorchLean.TensorPack α Δ) (σ : Substitution Γ Δ) (hσ : Env.SubstitutionSound envΓ envΔ fun {s : Spec.Shape} => σ) (args : Args Γ inputs) :

evalArgs envΔ (Args.substitute (fun {s : Spec.Shape} => σ) args) = evalArgs envΓ args

Pure evaluation commutes with a sound substitution of operation arguments.

source

theorem NN.GraphSpec.DAG.Term.eval_substitute {Γ Δ : List Spec.Shape} {s : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (envΓ : TorchLean.TensorPack α Γ) (envΔ : TorchLean.TensorPack α Δ) (σ : Substitution Γ Δ) (hσ : Env.SubstitutionSound envΓ envΔ fun {s : Spec.Shape} => σ) (term : Term Γ s) :

eval envΔ (substitute (fun {s : Spec.Shape} => σ) term) = eval envΓ term

Pure evaluation commutes with any term substitution representing the source environment.

source

@[simp]

theorem NN.GraphSpec.DAG.Term.eval_get {Γ Δ : List Spec.Shape} {s : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Δ) (args : Args Δ Γ) (v : Var Γ s) :

eval env (args.get v) = Env.tget (evalArgs env args) v

Evaluating an argument selected by a typed variable agrees with lookup in the evaluated argument environment.

source

theorem NN.GraphSpec.DAG.Term.eval_instantiate {Γ Δ : List Spec.Shape} {s : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Δ) (args : Args Δ Γ) (term : Term Γ s) :

eval env (instantiate args term) = eval (evalArgs env args) term

Pure evaluation of an inlined term equals evaluation of the original term under the supplied argument values.

source

theorem NN.GraphSpec.DAG.Term.evalArgs_append {Γ left right : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Γ) (leftArgs : Args Γ left) (rightArgs : Args Γ right) :

evalArgs env (leftArgs.append rightArgs) = (evalArgs env leftArgs).append (evalArgs env rightArgs)

Evaluating concatenated graph arguments concatenates their tensor values in the same order.

source

theorem NN.GraphSpec.DAG.Term.evalArgs_splitAppend {Γ left right : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Γ) (args : Args Γ (left ++ right)) :

have argumentParts := args.splitAppend; have valueParts := (evalArgs env args).split; (evalArgs env argumentParts.1, evalArgs env argumentParts.2) = valueParts

Evaluating a statically split argument list agrees with splitting its evaluated values.

source

theorem NN.GraphSpec.DAG.Term.evalArgs_splitAppend_fst {Γ left right : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Γ) (args : Args Γ (left ++ right)) :

evalArgs env args.splitAppend.1 = (evalArgs env args).split.1

Evaluating the left part of a typed argument split returns the corresponding value prefix.

source

theorem NN.GraphSpec.DAG.Term.evalArgs_splitAppend_snd {Γ left right : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Γ) (args : Args Γ (left ++ right)) :

evalArgs env args.splitAppend.2 = (evalArgs env args).split.2

Evaluating the right part of a typed argument split returns the corresponding value suffix.

source

@[simp]

theorem NN.GraphSpec.DAG.Term.eval_weakenLeft {Γ : List Spec.Shape} {s t : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Γ) (value : TorchLean.Tensor α t) (term : Term Γ s) :

eval (TorchLean.TensorPack.cons value env) term.weakenLeft = eval env term

Prepending an unrelated value does not change a term's pure meaning.

source

@[simp]

theorem NN.GraphSpec.DAG.Term.evalArgs_weakenLeft {Γ ins : List Spec.Shape} {t : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Γ) (value : TorchLean.Tensor α t) (args : Args Γ ins) :

evalArgs (TorchLean.TensorPack.cons value env) args.weakenLeft = evalArgs env args

Prepending an unrelated value does not change a typed argument list's pure meaning.

source

@[simp]

theorem NN.GraphSpec.DAG.Term.evalArgs_vars {Γ : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Γ) :

evalArgs env (Args.vars Γ) = env

Evaluating all variables of an environment returns that environment in order.

source

def NN.GraphSpec.DAG.Block.castOutputs {Γ outputs outputs' : List Spec.Shape} (h : outputs = outputs') :

Block Γ outputs → Block Γ outputs'

Reinterpret a block's result list along an equality of output shapes.

Instances For

source

def NN.GraphSpec.DAG.Block.eval {Γ outs : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Γ) :

Block Γ outs → TorchLean.TensorPack α outs

Evaluate a multi-output block, preserving sharing introduced by let1.

Instances For

source

@[simp]

theorem NN.GraphSpec.DAG.Block.eval_castOutputs {Γ outputs outputs' : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Γ) (h : outputs = outputs') (block : Block Γ outputs) :

eval env (castOutputs h block) = h ▸ eval env block

Casting a block's output shapes casts its evaluated typed result by the same equality.

source

theorem NN.GraphSpec.DAG.Block.eval_substitute {Γ Δ outs : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (envΓ : TorchLean.TensorPack α Γ) (envΔ : TorchLean.TensorPack α Δ) (σ : Substitution Γ Δ) (hσ : Env.SubstitutionSound envΓ envΔ fun {s : Spec.Shape} => σ) (block : Block Γ outs) :

eval envΔ (substitute (fun {s : Spec.Shape} => σ) block) = eval envΓ block

Substituting terms into a block preserves its pure multi-output semantics whenever the substitution denotes the original environment.

source

theorem NN.GraphSpec.DAG.Block.eval_instantiate {Γ Δ outs : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Δ) (args : Args Δ Γ) (block : Block Γ outs) :

eval env (instantiate args block) = eval (Term.evalArgs env args) block

Evaluating an inlined block is the same as evaluating its original body under the supplied typed argument values.

source

theorem NN.GraphSpec.DAG.Block.eval_andThenWithRenaming {Γ middle outputs : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (envΓ : TorchLean.TensorPack α Γ) (second : Block (Γ ++ middle) outputs) {Δ : List Spec.Shape} (first : Block Δ middle) (envΔ : TorchLean.TensorPack α Δ) (ρ : {s : Spec.Shape} → Var Γ s → Var Δ s) :

(Env.RenamingSound envΓ envΔ fun {s : Spec.Shape} => ρ) → eval envΔ (andThenWithRenaming (fun {s : Spec.Shape} => ρ) first second) = eval (envΓ.append (eval envΔ first)) second

Pure evaluation of block composition is ordinary typed environment extension.

source

theorem NN.GraphSpec.DAG.Block.eval_andThen {Γ middle outputs : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (env : TorchLean.TensorPack α Γ) (first : Block Γ middle) (second : Block (Γ ++ middle) outputs) :

eval env (first.andThen second) = eval (env.append (eval env first)) second

Composing two blocks evaluates the first once and appends its typed outputs for the second.

TorchLean API

NN.GraphSpec.DAG.Semantics

Pure semantics of GraphSpec DAGs #

Spec interpreter #

Semantics of variable renaming #