Documentation

LeanMlir.Proofs.Nets.MobileNet.MobileNetV4FullBEval

MobileNetV4-Conv-M at inference — eval forward + graph + faithfulness, at any resolution #

The eval twin of MobileNetV4FullB.lean. That file states Conv-M at TRAINING BatchNorm (bnBatchLA) at 224×224; this one states the same 21-row table at INFERENCE BatchNorm — frozen running statistics at all 77 sites, one shared ε — and proves its typed SHlo graph denotes it (mnv4FwdGraphBFullEval_faithful). That is the graph of mnv4_fwd_eval.mlir, mnv4in_fwd_eval.mlir and mnv4in_fwd_eval_s256.mlir.

One statement, every input size. The net is stated at a binder f, the final feature side: the input is 32f, the stem out 16f, the fused stage 8f, and the three stride-2 rows take it to 4f, 2f, f. The committed evals are f = 7 (224) and f = 8 (256, timm's test size for mobilenetv4_conv_medium.e500_r224_in1k) — mnv4FwdChainB's own f. The ladder is written as nested doublings (2 * (2 * f), not 4 * f) so a strided row's input side is its output side's 2 * h by the types alone.

Why no CertLayer and no resolution groups. Nothing differentiates the eval forward, so the blocks are plain functions; and at a variable f den stays stuck, so the single rewrite chain that times out at the training file's literal resolutions is small here.

Families by dispatch, as the render does it. A row's two depthwise positions are ifs on s.preDWk / s.postDWk in the graph (mnv4PreDWGraphBEval, mnv4PostDWGraphBEval), exactly the ifs uibFwdSkipB / uibFwdStridedB branch on, so one body graph covers ExtraDW, ConvNeXt-like, FFN (and IB, which Conv-M does not use) and one theorem proves it. The table picks the family.

What it is tied to. %x + 233 parameters + 154 statistic slots = 388 inputs. The SSA names are the eval render's: each BN's statistics are %{site}mu / %{site}var with the site the render's mnv4Bn statP (stn, f0cn, u{p}qn, …, hn). FwdGraphTextTies checks every block, the stem, the fused stage and the head against the render at .eval, at both f = 7 and f = 8.

@[reducible]
noncomputable def Proofs.StableHLO.mnv4CbReluBEval (N : ℕ) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (γ β μ v : Vec oc) :
Vec (N * (ic * h * w)) → Vec (N * (oc * h * w))

Batched k×k conv (any stride-1 extent) → inference BN → relu.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[reducible]
    noncomputable def Proofs.StableHLO.mnv4CbReluSBEval (N : ℕ) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (γ β μ v : Vec oc) :
    Vec (N * (ic * (2 * h) * (2 * w))) → Vec (N * (oc * h * w))

    Batched stride-2 conv, SYMMETRIC padding (the stem and the fused stage) → inference BN → relu.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[reducible]
      noncomputable def Proofs.StableHLO.mnv4ProjBEval (N : ℕ) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (γ β μ v : Vec oc) :
      Vec (N * (ic * h * w)) → Vec (N * (oc * h * w))

      Batched 1×1 project → inference BN, no activation (the linear bottleneck).

      Equations
      Instances For
        @[reducible]
        noncomputable def Proofs.StableHLO.mnv4DWBEval (N : ℕ) {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (γ β μ v : Vec c) :
        Vec (N * (c * h * w)) → Vec (N * (c * h * w))

        Batched depthwise → inference BN, no activation (timm's dw_start, the pre-DW).

        Equations
        Instances For
          @[reducible]
          noncomputable def Proofs.StableHLO.mnv4DWReluBEval (N : ℕ) {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (γ β μ v : Vec c) :
          Vec (N * (c * h * w)) → Vec (N * (c * h * w))

          Batched depthwise → inference BN → relu (the stride-1 post-DW).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[reducible]
            noncomputable def Proofs.StableHLO.mnv4DWReluSBEval (N : ℕ) {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (γ β μ v : Vec c) :
            Vec (N * (c * (2 * h) * (2 * w))) → Vec (N * (c * h * w))

            Batched stride-2 depthwise, symmetric → inference BN → relu (the strided post-DW).

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

              One depthwise site at inference: kernel, bias, and the BN's γ, β plus its frozen μ, σ².

              Instances For

                A depthwise slot at inference: nothing at k = 0, a Mnv4DWEval otherwise — DWSlot's eval twin.

                Equations
                Instances For

                  The slot's parameters at any k: the stored ones at k > 0, a zero placeholder at k = 0 that the absent slot never reads.

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

                    One UIB block's inference parameters, typed by its table row — UibParams's eval twin: each BN carries its frozen μ, σ² and no ε (the net shares one). The row's h appears in no field, which is what lets one record serve every input size.

                    Instances For

                      Every MobileNetV4-Conv-M inference parameter, generic in the class count: the 233 parameters of Mnv4BWeights without its per-site εs, plus the 77 BN sites' μ, σ². Field names follow the render's SSA prefixes.

                      Instances For
                        noncomputable def Proofs.StableHLO.mnv4PreDWSlotEval (N h : ℕ) (ε : ℝ) {c : ℕ} (k : ℕ) (p : Mnv4DWEvalSlot c k) :
                        Vec (N * (c * h * h)) → Vec (N * (c * h * h))

                        The pre-DW slot at inference: identity at k = 0, depthwise → BN otherwise.

                        Equations
                        Instances For
                          noncomputable def Proofs.StableHLO.mnv4PostDWSlotEval (N h : ℕ) (ε : ℝ) {c : ℕ} (k : ℕ) (p : Mnv4DWEvalSlot c k) :
                          Vec (N * (c * h * h)) → Vec (N * (c * h * h))

                          The stride-1 post-DW slot at inference: identity at k = 0, depthwise → BN → relu otherwise.

                          Equations
                          Instances For
                            noncomputable def Proofs.StableHLO.mnv4BodyEval (N h : ℕ) (ε : ℝ) (s : UibSpec) (p : UibEvalParams s) :
                            Vec (N * (s.ic * h * h)) → Vec (N * (s.oc * h * h))

                            A stride-1 UIB body at inference, read off its row: pre-DW? → expand-BN-relu → post-DW? → project-BN, at side h. The skip is added by the caller.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              noncomputable def Proofs.StableHLO.mnv4StridedEval (N h : ℕ) (ε : ℝ) (s : UibSpec) (p : UibEvalParams s) :
                              Vec (N * (s.ic * (2 * h) * (2 * h))) → Vec (N * (s.oc * h * h))

                              A stride-2 UIB block at inference: the pre-DW slot and the expand at the input side 2h, the post-DW carrying the stride to h (timm's dw_mid), the project at h. No skip.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                noncomputable def Proofs.StableHLO.mnv4FusedBEval (N h : ℕ) (ε : ℝ) {ic mid oc kH kW : ℕ} (Wc : Kernel4 mid ic kH kW) (bc γc βc μc vc : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp γp βp μp vp : Vec oc) :
                                Vec (N * (ic * (2 * h) * (2 * h))) → Vec (N * (oc * h * h))

                                The fused stage at inference: stride-2 k×k conv-BN-relu, then the 1×1 project-BN.

                                Equations
                                Instances For
                                  noncomputable def Proofs.StableHLO.mnv4HeadBEval (N h : ℕ) (ε : ℝ) {c mid oc nCls : ℕ} (W1 : Kernel4 mid c 1 1) (b1 γ1 β1 μ1 v1 : Vec mid) (W2 : Kernel4 oc mid 1 1) (b2 γ2 β2 μ2 v2 : Vec oc) (Wd : Mat oc nCls) (bd : Vec nCls) :
                                  Vec (N * (c * h * h)) → Vec (N * nCls)

                                  The head at inference, timm's order: 1×1 conv-BN-relu at h, GAP, conv_head 1×1 conv-BN-relu on the pooled [N, mid, 1, 1], dense — with mnv4Head's two relabellings.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    noncomputable def Proofs.StableHLO.mobilenetv4ForwardBFullEval (N f : ℕ) (ε : ℝ) {nCls : ℕ} (w : Mnv4BWeightsEval nCls) (x : Vec (N * (3 * (2 * (2 * (2 * (2 * (2 * f))))) * (2 * (2 * (2 * (2 * (2 * f)))))))) :
                                    Vec (N * nCls)

                                    The inference MobileNetV4-Conv-M at final feature side f, N·(3·32f·32f) → N·nCls: stem, fused stage, the 21 table rows (the eighteen stride-1 ones under residual), head. Every BN reads frozen statistics, so the whole net is per-example: each stage is batchMap N of a per-example map or a pointwise map.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      def Proofs.StableHLO.mnv4BnGraphBEval (epsStr gName btName site : String) (N c h : ℕ) (ε : ℝ) (γ β μ v : Vec c) (e : SHlo (N * (c * h * h))) :
                                      SHlo (N * (c * h * h))

                                      One inference BN node, named as mnv4Bn names it at .eval: γ, β by their parameter names, μ, σ² as %{site}mu / %{site}var.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        def Proofs.StableHLO.mnv4PreDWGraphBEval (epsStr p : String) (N h : ℕ) (ε : ℝ) {c : ℕ} (k : ℕ) (q : Mnv4DWEvalSlot c k) (e : SHlo (N * (c * h * h))) :
                                        SHlo (N * (c * h * h))

                                        The pre-DW slot's graph: no tokens at k = 0, depthwise → BN otherwise — uibFwdSkipB's and uibFwdStridedB's if preDWk > 0.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          def Proofs.StableHLO.mnv4PostDWGraphBEval (epsStr p : String) (N h : ℕ) (ε : ℝ) {c : ℕ} (k : ℕ) (q : Mnv4DWEvalSlot c k) (e : SHlo (N * (c * h * h))) :
                                          SHlo (N * (c * h * h))

                                          The stride-1 post-DW slot's graph: no tokens at k = 0, depthwise → BN → relu otherwise.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            def Proofs.StableHLO.mnv4BodyGraphBEval (epsStr : String) (N h : ℕ) (ε : ℝ) (s : UibSpec) (p : UibEvalParams s) (e : SHlo (N * (s.ic * h * h))) :
                                            SHlo (N * (s.oc * h * h))

                                            A stride-1 UIB body's inference graph at side h, every name read off the row.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              def Proofs.StableHLO.mnv4StridedGraphBEval (epsStr : String) (N h : ℕ) (ε : ℝ) (s : UibSpec) (p : UibEvalParams s) (e : SHlo (N * (s.ic * (2 * h) * (2 * h)))) :
                                              SHlo (N * (s.oc * h * h))

                                              A stride-2 UIB block's inference graph: pre-DW slot and expand at 2h, the strided post-DW (.depthwiseStrided, symmetric) to h, project at h.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                def Proofs.StableHLO.mnv4StemGraphBEval (epsStr : String) (N h : ℕ) (ε : ℝ) {ic oc kH kW : ℕ} (Ws : Kernel4 oc ic kH kW) (bs γs βs μs vs : Vec oc) (e : SHlo (N * (ic * (2 * h) * (2 * h)))) :
                                                SHlo (N * (oc * h * h))

                                                Stem inference graph: 3×3/s2 symmetric conv → BN (stn) → relu. Generic in the widths, for the reason mnv4StemGraphB records.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  def Proofs.StableHLO.mnv4FusedGraphBEval (epsStr : String) (N h : ℕ) (ε : ℝ) {ic mid oc kH kW : ℕ} (Wc : Kernel4 mid ic kH kW) (bc γc βc μc vc : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp γp βp μp vp : Vec oc) (e : SHlo (N * (ic * (2 * h) * (2 * h)))) :
                                                  SHlo (N * (oc * h * h))

                                                  Fused-stage inference graph: 3×3/s2 conv → BN (f0cn) → relu → 1×1 project → BN (f0pn).

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    def Proofs.StableHLO.mnv4HeadGraphBEval (epsStr : String) (N h : ℕ) (ε : ℝ) {c mid oc nCls : ℕ} (W1 : Kernel4 mid c 1 1) (b1 γ1 β1 μ1 v1 : Vec mid) (W2 : Kernel4 oc mid 1 1) (b2 γ2 β2 μ2 v2 : Vec oc) (Wd : Mat oc nCls) (bd : Vec nCls) (e : SHlo (N * (c * h * h))) :
                                                    SHlo (N * nCls)

                                                    Head inference graph, mnv4HeadGraphB's tokens with the two BNs at frozen statistics (h1n, hn).

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      theorem Proofs.StableHLO.mnv4BodyGraphBEval_faithful (epsStr : String) (N h : ℕ) (ε : ℝ) (s : UibSpec) (p : UibEvalParams s) (e : SHlo (N * (s.ic * h * h))) :
                                                      den (mnv4BodyGraphBEval epsStr N h ε s p e) = mnv4BodyEval N h ε s p (den e)

                                                      The stride-1 UIB body graph denotes its inference forward — every family, one theorem.

                                                      theorem Proofs.StableHLO.mnv4StridedGraphBEval_faithful (epsStr : String) (N h : ℕ) (ε : ℝ) (s : UibSpec) (p : UibEvalParams s) (e : SHlo (N * (s.ic * (2 * h) * (2 * h)))) :
                                                      den (mnv4StridedGraphBEval epsStr N h ε s p e) = mnv4StridedEval N h ε s p (den e)

                                                      The stride-2 UIB block graph denotes its inference forward.

                                                      def Proofs.StableHLO.mnv4FwdGraphBFullEval (N f : ℕ) (epsStr : String) (ε : ℝ) {nCls : ℕ} (w : Mnv4BWeightsEval nCls) (e : SHlo (N * (3 * (2 * (2 * (2 * (2 * (2 * f))))) * (2 * (2 * (2 * (2 * (2 * f)))))))) :
                                                      SHlo (N * nCls)

                                                      The MobileNetV4-Conv-M inference forward graph at final feature side f, at mnv4FwdChainB's .eval tokens and names: mnv4_fwd_eval.mlir and mnv4in_fwd_eval.mlir at f = 7, mnv4in_fwd_eval_s256.mlir at f = 8.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        theorem Proofs.StableHLO.mnv4FwdGraphBFullEval_faithful (N f : ℕ) (epsStr : String) (ε : ℝ) {nCls : ℕ} (w : Mnv4BWeightsEval nCls) (e : SHlo (N * (3 * (2 * (2 * (2 * (2 * (2 * f))))) * (2 * (2 * (2 * (2 * (2 * f)))))))) :
                                                        den (mnv4FwdGraphBFullEval N f epsStr ε w e) = mobilenetv4ForwardBFullEval N f ε w (den e)

                                                        The MobileNetV4-Conv-M inference graph denotes the inference forward, at every final feature side f. One rewrite per stage, outside-in; the eighteen skip rows each go through mnv4SkipGraphBEval_faithful with the body theorem, so the term stays linear in the depth.