Shape Soundness #
Shape inference (Infer.nodeOutShape, Graph.checkShapes) and the reference semantics
(Graph.evalNodeRaw, Graph.denoteAll) are two matches over OpKind. This file proves that they
agree: on a graph accepted by checkShapes, the value the evaluator computes for every node already
has the shape inference assigns to it, so the declared-shape normalization performed by evalNode
never rejects a node.
The results are organized as one lemma per operator family, followed by an induction over the node
array that runs Graph.inferShapesFrom and Graph.denoteAllFrom in lockstep.
Except helpers #
Except.map succeeds exactly when its argument succeeds.
Binding an error propagates the error.
Every success value of an Except computation has shape s.
Instances For
Errors have no success value.
A success value tagged with s has shape s.
Binding preserves the shape invariant of the continuation.
A dependent conditional preserves the shape invariant of both branches.
A conditional preserves the shape invariant of both branches.
Decoder characterizations #
A successful expectShape certifies the stored shape tag.
A successful parent read is an in-bounds array lookup.
The unary inference decoder returns the sole parent shape.
The same-shape inference rule returns the first parent's shape.
Parent-shape correspondence #
parentShapes lists the shapes of the already evaluated values at a node's parent ids.
This is the interface between the shape table maintained by Graph.inferShapesFrom and the value
table maintained by Graph.denoteAllFrom: whenever the evaluator can read parent k, inference
saw exactly that parent's shape at position k.
Instances For
The unary parent shape read by inference is the shape of the value read by the evaluator.
The binary parent shapes read by inference are the shapes of the values read by the evaluator.
Operator families #
Each lemma below fixes one operator (or family) and shows that the raw evaluator value has the
inferred shape. The hypotheses are the same throughout: the parent-shape correspondence, a
successful inference, and a successful raw evaluation. permute, transpose, and conv are the
exception (see evalNodeRaw_shape_declared).
The eval-mode BatchNorm contract returns the parent shape.
Eval-mode BatchNorm preserves the shape of its input.
Leading-axis concat produces the declared leading extent over the shared tail.
Binary elementwise operations (add, sub, mulElem, maxElem, minElem).
Source nodes (input, const, randUniform, bernoulliMask): inference returns the shape the
evaluator tags its result with.
Unary shape-preserving operations that only read one parent at the declared shape.
topKMask: shape preserving, reading one parent at the declared shape.
log: like the other unary operations, plus the data-dependent positivity check.
softmax, hardMaskedSoftmax, and layernorm: shape preserving after their axis, mask, or
normalized-suffix validation.
Axis reductions (reduceSum, reduceMean) and the full reduction sum.
Pure shape operations (broadcastTo, reshape, flatten) tag their result with the shape
written in the operation.
linear and mseLoss: the evaluator tags its result with the declared shape, respectively the
scalar shape, and inference returns the same.
matmul: both passes decompose the operand shapes with OpContracts.matmulDims.
A scalar scale operand changes a contraction's arithmetic, not its output shape.
maxPool and avgPool: both passes plan the pooled suffix with OpContracts.planPool.
batchNormEval: the payload-backed evaluator preserves the parent shape, which is also what
the contract returns.
concat: the evaluator recomputes OpContracts.inferConcatOutShape on the parent values and
insists that it equals the declared shape, which is what it produces.
permute, transpose, and conv compare the shape they realize against the declared
outShape, so a successful raw evaluation has the declared shape. Relating that realized shape to
the inference rule (Shape.permute?, respectively the convolution contract) is not needed for
soundness because checkShapes separately forces the inferred shape to be the declared one.
slice: the evaluator checks the sliced shape against the declared one.
A successful pointwise evaluation read its first parent at the declared shape, and its value has that shape.
Pointwise operators: inference returns the shape of the first parent, which the evaluator reads at the declared shape, and the result has that shape too.
Node-level soundness of shape inference.
If inference assigns the declared shape to a node (as Graph.checkShapes requires) and the node's
parents carry the shapes inference saw, then the raw evaluator value already has the declared shape.
Graph-level soundness #
A successful denoteAll is a successful denoteAllFrom started at node 0.
The normalized value of a node has the declared shape.
Normalization is the identity on a value that already has the declared shape.
Every value produced by evalNode has the declared shape of its node.
A successful parent lookup returns one already inferred shape per parent id.
The shapes looked up by inference are the shapes of the corresponding evaluated values.
Evaluate nodes i, i+1, ... with evalNodeRaw, that is, without the per-node declared-shape
normalization performed by evalNode.
This is a proof-only reference evaluator: denoteAllRawFrom_eq_denoteAllFrom shows that on a
graph accepted by checkShapes it computes the same table as denoteAllFrom.
Instances For
denoteAll without the per-node declared-shape normalization.
Instances For
Lockstep induction: if shape inference accepts the nodes from i on, starting from a table of
inferred shapes that matches the evaluated prefix, then raw and normalized evaluation agree from
i on.
On a graph accepted by checkShapes, the per-node declared-shape normalization is redundant:
evaluating with evalNodeRaw and with evalNode produce the same result.
Values already in the table are untouched by evaluating further nodes.
Evaluation from i fills exactly the remaining nodes, each with its declared shape.
Successful evaluation produces exactly one value per node, each with its declared shape.
This needs no shape-inference hypothesis: evalNode checks each result's declared shape.
The stronger correspondence denoteAllRaw_eq_denoteAll shows that on a graph accepted by
checkShapes, these checks never change or reject a raw result.
Shape inference is sound for the reference semantics: if checkShapes accepts a graph and the
graph evaluates, every node value has the shape inference assigned to it, namely the declared
one.