depthwise_close_mixed — the bf16-mixed DEPTHWISE convolution against exact ℝ #
The depthwise peer of FloatModel.conv_close_mixed, and — as
planning/archive/bf16_renderer.md §10.2 predicted — it is the same instantiation at a much smaller
fan-in, not a new result. A depthwise output is a dot product of length kH·kW: one channel,
no ic sum (depthwiseConv2d_eq_dw_dot). So it is dot_close_mixed_uniform at that fan-in, plus
one leaf rounding for the bf16 store and one accumulate rounding for the bias — three terms, one
per rounding the emit performs.
⭐ The fan-in shrinks from thousands to NINE and the bound barely moves, which is the whole
point of the §9.3 separation. At u_acc = 2⁻²⁴ / u_leaf = 2⁻⁸:
layer fan-in n fan-in term leaf term dwBr
depthwise 3×3 (every MNv2 block) 9 6.01e-07 7.83e-03 0.0078
R50 3×3, ic=512 (for contrast) 4608 2.77e-04 7.83e-03 0.0081
The fan-in term drops by 461× and dwBr moves by 3.5% — the fan-in rides the ACCUMULATE
precision, which stays fp32, while the flat leaf term is what actually costs. ▶ A depthwise layer
is not more accurate than a dense conv in bf16 in any way that matters; it is the same 0.8%.
⚠ Like conv_close_mixed, this bounds ONE layer against exact ℝ at an exactly-represented input.
Composition needs the error-modulus form — see ConvMixedComposeBridge for the conv version of
that argument, which transfers verbatim because FloatClose is precision- and layer-agnostic.
Channel ch's flattened filter as a plain Vec (kH·kW) — dwKernelMat's single column.
⚠⚠ dwWindow, dwKernelMat and depthwiseConv2d_eq_dense are REUSED from
DepthwiseFloatBridge, not rebuilt here. The first draft of this file defined its own
dwWindow with the identical type and meaning, and lake build LeanMlir refused the import
(environment already contains 'Proofs.dwWindow') — the same collision that had lake build LeanMlir broken for three commits over Proofs.convWindow. ▶ When a dw*/conv* helper
seems to be missing, grep before defining: on this evidence it usually already exists.
Equations
- Proofs.dwSlice W ch idx = Proofs.dwKernelMat W ch idx 0
Instances For
⭐ A depthwise output IS a dot product of length kH·kW — one channel, no ic sum.
depthwiseConv2d_eq_dense with dense unfolded; the depthwise peer of conv2d_eq_flat_dot,
and the reason §10.2's "expect it to be easier" was right.
Σ|kernel·window| over the receptive field — the magnitude the bound scales.
Equations
- Proofs.dwFanS W x ch hi wi = ∑ k : Fin (kH * kW), |Proofs.dwWindow kH kW x ch hi wi k * Proofs.dwSlice W ch k|
Instances For
The mixed-precision depthwise convolution, as the emitted graph computes it. Operands
rounded to the leaf precision L and accumulated at M, the accumulator then rounded to L
again — the bf16-typed result, i.e. the store — and only then the bias added at M.
⚠ The second L.rnd is not optional: BatchableOp.depthwiseBf16 must give the convolution a
bf16-typed result or XLA deletes the casts and cuDNN gets f32 parameters. Measured on a real
MNv2 layer (c=144, 56², fgc=144) — grouping buys no exemption from §9.2.
Equations
- M.depthwiseMixed L W b x ch hi wi = M.add (L.rnd (M.dotMixed L (Proofs.dwWindow kH kW x ch hi wi) (Proofs.dwSlice W ch))) (b ch)
Instances For
⭐⭐ Mixed-precision DEPTHWISE forward error. Three terms, one per rounding the emitted
graph performs: the dot (dwBr, fan-in kH·kW), the bf16 STORE of the accumulator (L.u),
and the f32 bias add (M.u). Structurally identical to conv_close_mixed; only the fan-in
differs, which is exactly what §10.2 predicted.