4. Semantics and Graphs🔗

Verification needs a definition of what a model computes for every input covered by the claim. The specification layer gives that mathematical function. GraphSpec 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. The added structure lets an interpreter execute the program and lets 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. A node array makes imported structure and local transformations explicit. The useful relationship is a theorem that evaluating the translated representation preserves the specified function. That is what lets a later bound on a graph refer back to the model from which it was built.