Backend Contracts

Contract-carrying backend vocabulary for TorchLean runtimes.

The semantic graph and specs stay in Lean. LibTorch and reference operations enter through named capsules that record shape, layout, value, and VJP contracts, a reduction-order policy, and an explicit trust level. The planner consumes these capsules under a KernelPolicy, the contract check confirms that every selected contract rests on evidence the policy accepts, and the eager runtime binds the selected capsule to a handler with the same operation, provider, and device.