Verification rules for program lowering

Import this module explicitly when proving a lowering preserves semantics. The generic verify tactic stays independent of the IR correctness development.

The graph rule needs both successful lowering and NoRawLog. The einsum rule compares an already checked plan with its tensor semantics. Neither rule certifies the parser, native compilation, or an external kernel; those require separate evidence.