Dropout as NNModuleSpecs (deterministic spec variants)

PyTorch's dropout is stochastic during training and becomes identity during evaluation. In the spec layer we often want a deterministic, pure meaning that can be composed into models and used in proofs without introducing randomness.

This file wraps the deterministic dropout specs from NN/Spec/Layers/Dropout.lean as NNModuleSpecs so they can be used in SpecChain pipelines and carry export metadata.

Two variants are provided:

• DropoutInferenceModuleSpec p: evaluation-mode dropout, hence the identity map.
• DropoutMaskedModuleSpec p mask: a deterministic "training-style" dropout that takes the mask explicitly (useful when you want to model a particular dropout pattern).

def Spec.DropoutInferenceModuleSpec {α : Type} {s : Shape} (p : α) : ModSpec.NNModuleSpec α s s

Evaluation-mode dropout wrapper. The configured training probability is retained as module metadata, while the forward map is the identity.

def Spec.DropoutMaskedModuleSpec {α : Type} [Context α] {s : Shape} (p : α) (mask : Tensor Bool s) : ModSpec.NNModuleSpec α s s

Deterministic masked dropout wrapper (mask is captured as data).

This matches the usual training-time dropout structure with the mask made explicit instead of sampled. The forward uses the same scaling and epsilon-protection as dropoutMaskedSpec.