Documentation

LeanMlir.Spec

Spec helpers: parameter layouts and counts (Layer.paramSlots, NetSpec.totalParams), feature queries the codegen gates helper emission on, architecture display, and validation.

def fpnDetectParamShapes (oc c3 c4 c5 A tower : Nat) :

Param shapes owned by a .fpnDetect layer, in the ONE canonical order that emitTrainStepSig, the optimizer, the grad-clip list, the backward's grad-binding, NetSpec.paramShapes and heInitLayer must all agree on:

Wn3 [oc,c3], Wn4 [oc,c4], Wn5 [oc,c5]           -- neck laterals
(W [oc,oc,3,3], b [oc]) × tower, per level P3 → P4 → P5
Wh3, Wh4, Wh5 [A·15, oc]                        -- head convs
bh3, bh4, bh5 [A·15]                            -- head biases, LAST

The biases MUST stay last: NetSpec.applyDetPriorBias installs the RetinaNet prior by splicing the final 3·A·15 floats of the buffer.

Defined here (rather than in the codegen) because SpecHelpers and MlirCodegen both need it and neither should own it — a mismatch between any two of these consumers is a silent parameter-aliasing bug, not a compile error.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def mbConvSeMid (blockIc : Nat) :

    Squeeze width of an .mbConv block's SE: a quarter of the block's input channels (timm's se_ratio taken over the block input, not the expanded width). Every parameter-layout writer and emitter reads it from here.

    Equations
    Instances For
      inductive ParamInit :

      How one parameter tensor is initialized. A random draw consumes one seed; a constant does not. zeroSeeded is zeros that still consume a seed — .timeCondAdd's weight, which starts as a no-op but keeps the seed stream every later layer draws from.

      Instances For
        structure ParamSlot :

        One trainable tensor of a layer: its shape, its initialization, and its name in the emitted MLIR signatures (W weight — also a LayerNorm's γ, b bias — also β, g / bt a conv's BN γ / β). A W opens a group: the group shares one index, %W3, %g3, %bt3. decay: whether the optimizer applies weight decay — matrices and kernels do; vectors (biases, norm scales) and positional embeddings do not.

        Instances For
          def slotsConvB (oc ic k : Nat) :
          Equations
          Instances For
            def slotsConvBn (oc ic k : Nat) :
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def slotsDense (fi fo : Nat) :
              Equations
              Instances For
                Equations
                Instances For

                  The one writer of a trainable layer's parameter layout — the tensors in signature order, each with its initialization. NetSpec.paramShapes (the packed [θ|m|v] blob), heInitLayer (the initial weights) and Layer.nParams (hence totalParams) all read it, so they cannot disagree. none for layers the codegen does not train (their count is nParamsUntrained). The MLIR signatures (MlirCodegen.fwdSigParts, emitTrainStepSig) render it too.

                  Equations
                  Instances For

                    The displayed parameter count of a layer the codegen does NOT train (Layer.paramSlots is none): the Bestiary's architectures, some counted approximately (.mambaBlock).

                    Equations
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Equations
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      Instances For
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          Equations
                                          Instances For
                                            Equations
                                            Instances For
                                              Equations
                                              Instances For
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

                                                  Output channels of a layer. Returns 0 for structural layers (pool, flatten, GAP).

                                                  Equations
                                                  Instances For

                                                    Input channels expected by a layer. Returns 0 for layers that accept any input.

                                                    Equations
                                                    Instances For

                                                      Validate that channel dimensions chain correctly through the spec. Returns none if valid, or some errorMessage describing the first mismatch.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For

                                                        Validate at build time. Use as: #eval mySpec.validate!

                                                        Equations
                                                        Instances For
                                                          inductive SummarySize :

                                                          Which quantity the summary's first line reports. Bestiary entries cover images, token streams, residue chains and raw audio, and a few (NeRF) have no meaningful input extent.

                                                          Instances For
                                                            @[instance_reducible]
                                                            Equations
                                                            @[instance_reducible]
                                                            Equations
                                                            inductive ParamUnit :

                                                            How params is abbreviated after the exact count. bare prints the count alone.

                                                            Instances For
                                                              @[instance_reducible]
                                                              Equations
                                                              Equations
                                                              Instances For
                                                                @[instance_reducible]
                                                                Equations

                                                                The shared Bestiary summary block, printed by every Bestiary/*.lean entry. The first line's label, the params abbreviation (unit) and an optional parenthetical on the validate : OK line (okNote) are the parts that vary.

                                                                The ── {name} ── and params<pad>: {n} lines are parsed, not decoration: tests/test_bestiary_params.py parses exactly those two shapes out of each binary's stdout to pin every variant against tests/bestiary_params.yml (the CI drift guard in .github/workflows/certs.yml). Keep both shapes if you touch this.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For