4. Semantics and Graphs🔗

Verification needs a definition of what a model computes for every input covered by the claim. That mathematical function comes from the specification layer, and the operator table names each operator once, with the rule the tapes and the operator graph run for it. A sequential model records its architecture with shapes in the types, while the shared IR uses a node array that importers and verification passes can inspect.

For a linear layer, the specification can say directly that each output is a dot product plus a bias. A graph must also say where the input came from, which parameter entry supplies the weights, and which node receives the result. That added structure lets an interpreter execute the program and a verifier inspect intermediate values. It also creates facts that need checking: a parent index must name an available node, and the chosen weights must fit the declared dimensions.

These representations support different tasks. Shape-indexed composition makes incompatible layer interfaces difficult to express, while a node array spells out imported structure and local transformations. We prove that the lowered graph runs as the typed graph that lowering records (IR.lowerForward_eq_ok). No theorem relates that graph to the source model, so a bound on the graph applies to the model only if the recording is right.