Verified operation lowering

Executable tensor programs, planning data, and correctness theorems relating lowered operations to their independent coordinate semantics.