Compositional properties of typed tensor programs

Theorems here lift local operation rules through the existing typed interpreter. They use the same program, scalar families, payloads and evaluation functions as execution.

• run_induction carries a predicate on values and conversion flags through a successful run.
• run_rel carries a relation between two successful runs, allowing different interpreters, inputs and parameter payloads.
• eval_rel transfers pointwise node relations to the designated results in return order.

These rules remove the traversal argument from proofs about a tensor program. A numerical bound, permutation property or other relation still needs correct rules for its operations, including input and constant nodes. Successful execution is an explicit hypothesis; the rules do not prove that a program executes for every input or that an external backend implements its semantics.

theorem NN.IR.Interpreter.run_rel {left right : Interpreter} (program : Program) (leftPayload : left.Payload) (rightPayload : right.Payload) (leftArguments : Array left.Value) (rightArguments : Array right.Value) (relation : Array left.Value × FloatLib.Floats.ExecFloat.ConversionStatus → Array right.Value × FloatLib.Floats.ExecFloat.ConversionStatus → Prop) (initial : relation (#[], { }) (#[], { })) (step : ∀ node ∈ program.graph.nodes, ∀ (leftState : Array left.Value × FloatLib.Floats.ExecFloat.ConversionStatus) (rightState : Array right.Value × FloatLib.Floats.ExecFloat.ConversionStatus) (leftValue : left.Value) (rightValue : right.Value) (leftStatus rightStatus : FloatLib.Floats.ExecFloat.ConversionStatus), relation leftState rightState → left.evalNode program leftPayload leftArguments leftState.1 node = Except.ok (leftValue, leftStatus) → right.evalNode program rightPayload rightArguments rightState.1 node = Except.ok (rightValue, rightStatus) → relation (leftState.1.push leftValue, leftState.2.merge leftStatus) (rightState.1.push rightValue, rightState.2.merge rightStatus)) {leftValues : Array left.Value} {rightValues : Array right.Value} {leftFlags rightFlags : FloatLib.Floats.ExecFloat.ConversionStatus} (hl : left.run program leftPayload leftArguments = Except.ok (leftValues, leftFlags)) (hr : right.run program rightPayload rightArguments = Except.ok (rightValues, rightFlags)) : relation (leftValues, leftFlags) (rightValues, rightFlags)

A relation preserved by each operation holds between the completed value tables.

The interpreters may use different scalar representations, and their inputs and payloads may also differ. The local rule must cover those differences for input, constant and numerical nodes. The relation can describe the whole prefix and accumulated conversion flags, allowing bounds and exception conditions to depend on earlier results.

theorem NN.IR.Interpreter.run_induction (interpreter : Interpreter) (program : Program) (payload : interpreter.Payload) (arguments : Array interpreter.Value) (property : Array interpreter.Value × FloatLib.Floats.ExecFloat.ConversionStatus → Prop) (initial : property (#[], { })) (step : ∀ node ∈ program.graph.nodes, ∀ (state : Array interpreter.Value × FloatLib.Floats.ExecFloat.ConversionStatus) (value : interpreter.Value) (status : FloatLib.Floats.ExecFloat.ConversionStatus), property state → interpreter.evalNode program payload arguments state.1 node = Except.ok (value, status) → property (state.1.push value, state.2.merge status)) {values : Array interpreter.Value} {flags : FloatLib.Floats.ExecFloat.ConversionStatus} (h : interpreter.run program payload arguments = Except.ok (values, flags)) : property (values, flags)

Carry an invariant from the empty value table through every successful operation.

The predicate can express bounds on intermediate tensors or conditions on conversion flags. It is supplied by the proof, independently of the frontend or model architecture.

theorem NN.IR.Interpreter.eval_rel {left right : Interpreter} (program : Program) (leftPayload : left.Payload) (rightPayload : right.Payload) (leftArguments : Array left.Value) (rightArguments : Array right.Value) (relation : left.Value → right.Value → Prop) (step : ∀ node ∈ program.graph.nodes, ∀ (leftValues : Array left.Value) (rightValues : Array right.Value) (leftValue : left.Value) (rightValue : right.Value) (leftStatus rightStatus : FloatLib.Floats.ExecFloat.ConversionStatus), List.Forall₂ relation leftValues.toList rightValues.toList → left.evalNode program leftPayload leftArguments leftValues node = Except.ok (leftValue, leftStatus) → right.evalNode program rightPayload rightArguments rightValues node = Except.ok (rightValue, rightStatus) → relation leftValue rightValue) {leftOutputs : Array left.Value} {rightOutputs : Array right.Value} {leftFlags rightFlags : FloatLib.Floats.ExecFloat.ConversionStatus} (hl : left.eval program leftPayload leftArguments = Except.ok (leftOutputs, leftFlags)) (hr : right.eval program rightPayload rightArguments = Except.ok (rightOutputs, rightFlags)) : List.Forall₂ relation leftOutputs.toList rightOutputs.toList

Operation rules imply a relation between corresponding returned tensors.

This includes multiple arguments, repeated result nodes and any return order. The rules apply to the program's actual typed operations and payloads; no architecture specification is required.