Backend selection soundness

The production planner selects registered capsules according to availability and policy. These proofs concern selection of declared contracts. They do not establish native kernel eligibility, numerical correctness, or the behavior of foreign implementations.

theorem NN.Backend.chooseCapsuleFor_sound {policy : KernelPolicy} {op : BackendOp} {registry : Array KernelCapsule} {selected : KernelCapsule} (hselected : chooseCapsuleFor? policy op registry = some selected) : selected ∈ registry ∧ selected.op = op ∧ KernelCapsule.admissible policy selected = true

A successful choice is registered, implements the requested operation, and is admissible.

theorem NN.Backend.chooseCapsuleFor_only_provider {policy : KernelPolicy} {op : BackendOp} {registry : Array KernelCapsule} {selected : KernelCapsule} {provider : Provider} (honly : policy.provider = ProviderPreference.only provider) (hselected : chooseCapsuleFor? policy op registry = some selected) : selected.provider = provider

An exclusive provider request never selects a capsule from another provider.

theorem NN.Backend.chooseCapsuleFor_prefer_fallback_iff {policy : KernelPolicy} {availability : Availability} {registry : Array KernelCapsule} {op : BackendOp} {preferred : Provider} {selected : KernelCapsule} (hprefer : policy.provider = ProviderPreference.prefer preferred) (hselected : chooseCapsuleFor? policy op (availability.filterCapsules registry) = some selected) : selected.provider ≠ preferred ↔ ¬∃ capsule ∈ registry, availability.admitsCapsule capsule = true ∧ capsule.op = op ∧ KernelCapsule.admissible policy capsule = true ∧ capsule.provider = preferred

A successful choice leaves the preferred provider exactly when no available, admissible candidate of that provider implements the requested operation.

theorem NN.Backend.planOp_sound {policy : KernelPolicy} {registry : Array KernelCapsule} {op : BackendOp} {kernel : PlannedKernel} (hplan : planOp policy registry op = Except.ok kernel) : kernel.op = op ∧ kernel.capsule ∈ registry ∧ kernel.capsule.op = kernel.op ∧ KernelCapsule.admissible policy kernel.capsule = true

Planning one operation preserves its tag and selects a registered, admissible capsule.

theorem NN.Backend.planOps_sound {policy : KernelPolicy} {registry : Array KernelCapsule} {ops : Array BackendOp} {plan : KernelPlan} (hplan : planOps policy registry ops = Except.ok plan) : Array.map (fun (x : PlannedKernel) => x.op) plan.kernels = ops ∧ ∀ kernel ∈ plan.kernels, kernel.capsule ∈ registry ∧ kernel.capsule.op = kernel.op ∧ KernelCapsule.admissible policy kernel.capsule = true

Successful planning preserves operation order and multiplicity, and each selected capsule is registered, implements its planned operation, and is admissible under the requested policy.

theorem NN.Backend.BackendProfile.planOps_sound {profile : BackendProfile} {ops : Array BackendOp} {plan : KernelPlan} (hplan : profile.planOps ops = Except.ok plan) : Array.map (fun (x : PlannedKernel) => x.op) plan.kernels = ops ∧ ∀ kernel ∈ plan.kernels, kernel.capsule ∈ profile.registry ∧ kernel.capsule.op = kernel.op ∧ profile.availability.admitsCapsule kernel.capsule = true ∧ KernelCapsule.admissible profile.policy kernel.capsule = true

A successful profile plan preserves the requests and selects only registered, available, operation-matching capsules admissible under the profile policy.