7.6.3.1. Shape And Broadcast🔗

NN.Examples.BugZoo.ShapeAndBroadcast source records one of TorchLean's core design choices: shapes belong in the object, not as an afterthought. The example uses a missing batch dimension and a reduce then broadcast pattern as its running examples. In NumPy style tensor libraries, a reduced vector can silently expand back across a matrix and still produce a plausible loss. In TorchLean, ordinary elementwise operations require the same shape, and explicit broadcasting carries Shape.CanBroadcastTo evidence.

The local contract is concrete: addSingletonBatch names the batch insertion, reduceRows names the reduction, and broadcastRowToMatrix names the expansion. The theorem broadcastRowToMatrix_firstRow shows the preferred style: if a dimension is added, removed, or reintroduced, the documentation and proof script can point at a term that did it.

The empirical motivation is tensor shape fault work such as SFData, plus numerical bug studies that found bad reductions and accidental broadcasting in real DL programs.

The contract shape is:

\operatorname{add} : \operatorname{Tensor}(\alpha,s)\to \operatorname{Tensor}(\alpha,s)\to \operatorname{Tensor}(\alpha,s)

and explicit broadcast operations carry evidence that the source shape can be broadcast to the target shape.

7.6.3.2. Stable Loss🔗

NN.Examples.BugZoo.StableLoss source is about losses that look mathematically harmless but fail numerically. The classic sketch is softmax followed by log: if a probability rounds to zero, the log path can produce infinities and downstream NaNs. TorchLean keeps two APIs separate. Logits should use crossEntropyLogitsSpec, which unfolds through logSoftmaxSpec; probability inputs use the clipped probability form crossEntropySpec.

The checked hooks are small. crossEntropyLogits_uses_logSoftmax says that the logits loss really takes the stable logits path. crossEntropyProbabilities_clips_before_log says that the probability path clamps before log. safeDivSpec_unfold gives division with domain assumptions an explicit node protected by epsilon rather than hiding it in an optimizer or backend.

This example is motivated by TensorFuzz, which targeted rare numerical failures, and by empirical studies of numerical bugs involving log, sqrt, division, exp, and reductions.

7.6.3.3. Ignored Labels🔗

NN.Examples.BugZoo.IgnoredLabelLoss source turns a corner case that is easy to dismiss into a reduction contract. PyTorch issue #75181 reported an ignore_index case where all labels were ignored and the result was nan.

TorchLean exposes the policy instead of copying every branch of a framework kernel. labelContribution false loss = 0 states that ignored labels contribute no scalar loss, and the example's helper for empty reductions names one policy for the all-ignored case. The bug appears when an empty active set reaches an unnamed backend reduction.

The policy is the definition:

\operatorname{labelContribution}(active,loss) = \begin{cases} loss, & active\\ 0, & \neg active \end{cases}

The all ignored case is then a declared reduction policy, not an accidental division by zero.

7.6.3.4. Autograd Domain🔗

NN.Examples.BugZoo.AutogradDomain source follows PyTorch's own autograd note about division by zero. If a graph computes x/0 and masks the bad value afterward, the forward result may look hidden while the backward graph still contains the undefined operation.

TorchLean's example names the difference between "divide first, mask later" and "safe divide, then mask." maskAfterSafeDiv records safedivSpec before the mask, and maskAfterSafeDiv_uses_epsilon_denominator unfolds to division by \mathrm{denominator}+\varepsilon. The contrast definition, unsafeDivThenMask, stays in the file so importers and reviewers can see the risky graph shape rather than treating every masked expression as safe.

7.6.3.5. Attention Mask🔗

NN.Examples.BugZoo.AttentionMask source is the catalog entry for causal mask semantics. Attention masks fail by polarity, layout, fake negative infinity, fully masked rows, and interactions with API flags. PyTorch has had relevant reports for MultiheadAttention, including is_causal=True being ignored when need_weights=True and fully masked heads producing NaNs when weights are requested.

The example connects the runtime convention to the math. Lean's real numbers do not contain literal negative infinity, so the file first uses EReal to state the exact fact \exp(-\infty)=0. TorchLean's ordinary attention spec then uses the equivalent hard masked softmax numerator. The theorem trueInfinityMask_future_attention_weight_zero says that strict future positions receive exactly zero attention mass under the causal mask. That property is the one needed when reasoning about autoregressive output causality.

The spec also makes fully blocked rows total: if every mask entry in a row is false, the complete weight row is zero. This is distinct from first forming a vector of negative infinities and then applying an implementation whose normalization may produce NaN on that row.

In formula form:

j>i \quad\Longrightarrow\quad \operatorname{attentionWeight}_{causal}(i,j)=0

This example also points back to the original transformer paper, Attention Is All You Need.

7.6.3.6. Compiler Boundary🔗

NN.Examples.BugZoo.CompilerBoundary source is the wrong-code example. It is about optimized graphs that run, return tensors, and are nevertheless not the same computation as the source graph. NNSmith found compiler bugs across TVM, TensorRT, ONNXRuntime, and PyTorch, FreeFuzz found framework/API bugs by mining real snippets, and a recent PyTorch compiler correctness study focuses directly on silent torch.compile wrong outputs.

The local object is the SemanticBoundary structure. It has a source evaluator, a target evaluator, an implementation relation, and a preservation field. This compact shape is the reusable claim behind heavier IR compiler correctness theorems: accepted target code must agree with the source semantics on every input. A runtime check can make us more confident, but it is not the same kind of artifact as a semantic boundary.

The reusable statement is:

\operatorname{implements}(source,target) \quad\Longrightarrow\quad \forall x,\; target(x)=source(x)

7.6.3.7. Float Boundary🔗

NN.Examples.BugZoo.FloatBoundary source is where we refuse to let proofs over real numbers silently masquerade as float32 deployment guarantees. Floating point verification attacks show why that matters: a property proved over reals can be invalidated by finite precision, exceptional values, fused operations, denorm behavior, or changed reduction order. The example cites Jia and Rinard's warning paper.

TorchLean's answer is explicit modeling. IEEE32Exec is the executable bit level float32 model. Runtime Float32 primitives are not transparent to the Lean kernel, so the theorem runtimeFloat32_add_rewrites_to_ieee32 requires the named assumption RuntimeFloat32FiniteMatchesIEEE32Exec, together with finite-input and finite-result hypotheses. We built that friction on purpose. If a proof uses the float32 model, the boundary says where runtime conformance entered.

The boundary is therefore visible in the theorem shape:

\operatorname{RuntimeFloat32FiniteMatchesIEEE32Exec} \quad\Longrightarrow\quad \operatorname{runtimeAdd}(x,y) = \operatorname{IEEE32Exec.add}(x,y)

7.6.3.8. Normalization State🔗

NN.Examples.BugZoo.NormalizationState source covers BatchNorm style bugs where the formula or state is wrong but the layer still emits a tensor. CRADLE reported a BatchNorm epsilon placement issue across backends, while LEMON found BatchNormalization moving stat bugs and BatchNorm layers that produce NaNs.

The example splits the concern in two. First, normalizeCore_scalar_uses_variance_plus_epsilon shows that TorchLean's scalar normalization puts epsilon inside the variance term before square root. Second, RunningStats packages inference time mean and variance as explicit inputs. Train/eval mode bugs are often state bugs. If running statistics are ambient mutable framework state, the proof cannot see them. If they are arguments to batchNormEvalWithStats, the state boundary is visible.

7.6.3.9. LayerNorm Degenerate Axis🔗

NN.Examples.BugZoo.LayerNormDegenerateAxis source records a related but different normalization bug family. LayerNorm can receive an axis with one element or a constant slice. The tensor output still has the expected shape, but the variance term is zero and the implementation's epsilon convention determines whether the result is finite and meaningful.

TorchLean's contract is to expose the denominator policy instead of burying it in a fused kernel. The invariant is small:

\operatorname{denom}=\sqrt{\operatorname{variance}+\epsilon}

and the degenerate case should be governed by the same explicit formula. That gives later kernels a reference behavior to match.

7.6.3.10. Constant Normalization Slice🔗

NN.Examples.BugZoo.ConstantNormalizationSlice source keeps the constant-slice case visible. A constant row or channel slice is not exotic; it appears in padding-heavy batches, masked tokens, uniform images, and clipped signals. If the normalization implementation accidentally assumes positive variance, a constant slice can produce a division by zero, NaN, or a backend-specific branch.

The contract is the same discipline used throughout BugZoo: name the slice, name the variance, and name the epsilon-protected normalization result. An optimized kernel can then be tested or proved against the reference object.

7.6.3.11. Batch Invariance🔗

NN.Examples.BugZoo.BatchInvariance source is about serving systems that change outputs depending on which other requests share a batch. This can come from dynamic batching, kernel selection, reduction order, and scheduling details even when user randomness is off. The catalog points at recent LLM serving discussions and studies: Thinking Machines on inference nondeterminism and an LLM inference engine bug study.

The checked reference semantics is mapBatch: apply the same function to each example independently to each row. The theorem mapBatch_select_eq_single says that selecting one row from the batched result equals evaluating that row alone. That theorem is the semantic target a runtime path should refine; any explicit float32 tolerance, reduction-order difference, or serving-system batching policy belongs in a separate runtime assumption.

7.6.3.12. KV Cache🔗

NN.Examples.BugZoo.KVCache source models cache accounting in autoregressive inference. LLM engines fail through shifted caches, wrong cache slots, config/shape mismatches, resource scheduling, and interaction with positions or tokenizers. The broader source trail is the LLM inference engine bug study.

The local contract is exact: a cache append operation preserves existing entries and puts the newly decoded key/value in the final slot. That sounds obvious, but it is the kind of invariant that becomes fragile when a serving system combines paged attention, batching, and mutable buffers. The BugZoo example says what the reference operation means before any external cache manager is trusted to implement it.

7.6.3.13. RoPE Position🔗

NN.Examples.BugZoo.RoPEPosition source pairs naturally with the KV cache example. Rotary position embeddings make position accounting part of the model's meaning. A decode position off by one can be hard to notice because the tensor shapes still line up and the model still produces tokens.

The file introduces PositionSchedule and appendNextPosition. The theorem appendNextPosition_last states that the newly appended token gets exactly the next sequence index. The schedule is explicit rather than derived from ambient mutable state. It follows the same design move as the normalization example: if the state affects semantics, it should appear in the object we inspect.

7.6.3.14. Tokenizer Boundary🔗

NN.Examples.BugZoo.TokenizerBoundary source marks the boundary before tensors even reach the model. Tokenizer/config mismatches can disagree about vocabulary size, padding, EOS, or special token IDs while the neural network code itself looks ordinary. The LLM inference engine bug study lists tokenizer/config bugs as a real serving class.

TorchLean's current contract is small but valuable: token IDs inside the typed fragment can be represented as Fin vocabSize. padId_in_vocab and tokenAt_in_vocab are almost tautological, which means token IDs outside the vocabulary are no longer a late runtime condition once data has crossed into this representation. The remaining producer step is the importer or tokenizer bridge that constructs those Fin values from external bytes.

7.6.3.15. Geometry 3D Projection🔗

NN.Examples.BugZoo.Geometry3DProjection source shows why BugZoo is not limited to language-model incidents. Vision and robotics pipelines often project 3D points to image coordinates with a camera matrix. The formula is familiar:

(u,v)=\left(\frac{x}{z},\frac{y}{z}\right)

up to intrinsics and coordinate conventions. The bug family is also familiar: depth is zero or has the wrong sign, coordinate frames are swapped, or the denominator convention is implicit. A tensor can still be emitted, but the geometry claim no longer matches the camera model.

The TorchLean response is to expose projection preconditions and the safe division boundary. A verified perception or control argument should not inherit an unspoken "all points have valid positive depth" assumption from preprocessing code.