Define softmax semantics and implement a lowering to the correct sequence of named ops

For this, we need to lower it from multiple models and multiple frameworks and see "what they do". At least two potential options: `exp(arg)` and `exp(arg-mean)`, might be more. We need to pick one, provide reasoning, and then implement a lowering upstream.