Documentation

LeanMlir.Proofs.Nets.MobileNet.MobileNetV4Spec

MobileNetV4-Conv-M's block table #

UibSpec (one Universal Inverted Bottleneck row) and mnv4Blocks (the 21 rows of Conv-M), the one transcription of the net's layout. The renderer (MobileNetV4RenderB) folds over it to emit the artifacts, and the proof chain from MobileNetV4BackB0.lean on folds over it to state the net, so the proofs read the table without importing the renderer. Names are in Proofs.StableHLO, where the renderer first defined them.

References #

source
structure Proofs.StableHLO.UibSpec :
Type

One row of the MobileNetV4-Conv-M block table. h is the block's OUTPUT spatial size, so a stride2 block reads its input at 2h.

  • p : String

    parameter-name prefix: "1" … "21".

  • ic : Nat
  • oc : Nat
  • expand : Nat
  • preDWk : Nat

    pre-depthwise kernel, 0 = absent.

  • postDWk : Nat

    post-depthwise kernel, 0 = absent.

  • h : Nat
  • stride2 : Bool
Instances For
    source
    @[instance_reducible]
    instance Proofs.StableHLO.instInhabitedUibSpec :
    Inhabited UibSpec
    Equations
    source
    @[instance_reducible]
    instance Proofs.StableHLO.instDecidableEqUibSpec :
    DecidableEq UibSpec
    Equations
    source
    def Proofs.StableHLO.instDecidableEqUibSpec.decEq (x✝ x✝¹ : UibSpec) :
    Decidable (x✝ = x✝¹)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Proofs.StableHLO.mnv4Blocks :
      List UibSpec

      THE BLOCK TABLE — transcribed once, from jax/MainMobilenetV4.lean.

      Everything downstream folds over this list: the parameter signature, the BN stat slots, the forward chain, the backward chain and the running-statistic recomputes. Two readings of the layout that diverged would type-check alike (same ops, same channel counts, same types), so the rows are written once.

      Families in order (Conv-M): ExtraDW ×7, ConvNeXt, FFN, ConvNeXt, ExtraDW ×4, FFN, ConvNeXt, ExtraDW ×2, FFN ×2, ConvNeXt — 13 ExtraDW / 4 ConvNeXt / 4 FFN, and no IB row. Spatial ladder 56 → 28 → 14 → 7.

      Checked against timm 1.0.28 (mobilenetv4_conv_medium, walking model.blocks[1:4]): all 21 rows agree on (ic, oc, expand, preDWk, postDWk, h, stride2). The #guards in Proofs/Nets/MobileNet/MobileNetV4BackB0.lean pin that reading, one of them all 21 tuples written out literally; they are derived from timm rather than re-read off this table, or they would gate nothing. What the table cannot say — which depthwise carries a stride (the post-DW when both exist; every strided row has both, and a #guard in the renderer holds that), and that the pre-DW is BN only — is the renderer's, and scripts/parity/mnv4_timm_parity.py pins it against timm on shared weights.

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