Documentation

LeanMlir.Proofs.Nets.MobileNet.MobileNetV4FullBEval

MobileNetV4-Conv-M at inference — eval forward + graph + faithfulness, at every input side 32·f #

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 side 32·f. 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.

The artifacts are the zero-bias instance. Mnv4BWeightsEval carries a conv-bias field at every conv site (sb, be, bz, the slots' b, …), which den reads, while the graph spells each one as the %zb{c} zero operand. So the committed evals are the instance with every conv bias 0. At inference BatchNorm a conv bias does not cancel as it does under batch BN, so this is a restriction, not a reparametrisation.

@[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.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 side 32·f.

                  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' μ, σ², plus a conv-bias vector per conv site. Field names follow the render's SSA prefixes. The graph binds every conv bias to the %zb{c} zero operand, so the committed evals are the instance with every conv-bias field 0.

                    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 mnv4SkipGraphB_faithful with the body theorem, so the term stays linear in the depth.