Documentation

LeanMlir.Proofs.Codegen.EfficientNetRenderPCEval

EfficientNet-B0 — the inference (frozen-statistics) stages and block graphs #

The eval twin of EfficientNetRenderPC.lean: the batched stage abbreviations at frozen statistics (cbsBEval / stemBEval / dwbsBEval / dwbsSBEval / projBEval — seB is unchanged, it has no BN) and the five block graphs with their faithfulness (*GraphBEval_faithful). EfficientNetFullB0Eval chains them into the shipped sixteen-block eval forward.

⭐ At inference the batch decouples: frozen statistics are constants, so the eval BN is per-example — batchMap N (bnPerChannelEvalTensor3 oc h w ε γ β μ v), denOp's bnEval arm, read off by den_batchOp — and every stage is batchMap N of a per-example op or a pointwise map.

⚠ One ε for the whole net, as the render emits, where the training def carries a separate ε per site. The SSA names extend the training graph's (%sg/%sbt → %smu/%svar, %b1dg/%b1dbt → %b1dmu/%b1dvar, …); names are pretty-printing metadata and do not enter den. 3-axiom clean.

@[reducible]

noncomputable def Proofs.cbsBEval (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 conv → inference bn → swish (1×1 expand / generic stride-1 conv).

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def Proofs.stemBEval (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 strided (3×3 s2) stem conv → inference bn → swish (halves spatial). At the XLA-SAME phase, as stemB (EfficientNetRenderPC.lean) and the shipped efficientnet_fwd_eval.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible]

noncomputable def Proofs.dwbsBEval (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 (stride-1, k×k) → inference bn → swish.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible]

noncomputable def Proofs.dwbsSBEval (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 depthwise (stride-2 downsample, k×k) → inference bn → swish.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible]

noncomputable def Proofs.projBEval (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 project: 1×1 conv → inference bn (no swish — the linear bottleneck).

Equations

Proofs.projBEval N W b ε γ β μ v = Proofs.StableHLO.batchMap N (Proofs.bnPerChannelEvalTensor3 oc h w ε γ β μ v) ∘ Proofs.StableHLO.batchMap N (Proofs.flatConv W b)

Instances For

noncomputable def Proofs.mbNoExpFwdBEval (N : ℕ) {ic oc h w kHd kWd r : ℕ} (ε : ℝ) (Wd : DepthwiseKernel ic kHd kWd) (bd γd βd μd vd : Vec ic) (Wz₁ : Mat ic r) (bz₁ : Vec r) (Wz₂ : Mat r ic) (bz₂ : Vec ic) (Wp : Kernel4 oc ic 1 1) (bp γp βp μp vp : Vec oc) :

Vec (N * (ic * h * w)) → Vec (N * (oc * h * w))

MBConv1 (t=1, no expand) at inference: dw-bn-swish → SE → project-bn.

Equations

Proofs.mbNoExpFwdBEval N ε Wd bd γd βd μd vd Wz₁ bz₁ Wz₂ bz₂ Wp bp γp βp μp vp = Proofs.projBEval N Wp bp ε γp βp μp vp ∘ Proofs.seB N Wz₁ bz₁ Wz₂ bz₂ ∘ Proofs.dwbsBEval N Wd bd ε γd βd μd vd

Instances For

noncomputable def Proofs.mbStridedFwdBEval (N : ℕ) {ic mid oc h w kHd kWd r : ℕ} (ε : ℝ) (We : Kernel4 mid ic 1 1) (be γe βe μe ve : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd γd βd μd vd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp γp βp μp vp : Vec oc) :

Vec (N * (ic * (2 * h) * (2 * w))) → Vec (N * (oc * h * w))

MBConv6 with a stride-2 downsample at inference.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def Proofs.mbResidFwdBEval (N : ℕ) {c mid h w kHd kWd r : ℕ} (ε : ℝ) (We : Kernel4 mid c 1 1) (be γe βe μe ve : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd γd βd μd vd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 c mid 1 1) (bp γp βp μp vp : Vec c) :

Vec (N * (c * h * w)) → Vec (N * (c * h * w))

MBConv6 with an identity residual skip at inference.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def Proofs.headFwdBEval (N : ℕ) {c oc h w nC : ℕ} (ε : ℝ) (Wh : Kernel4 oc c 1 1) (bh γh βh μh vh : Vec oc) (Wfc : Mat oc nC) (bfc : Vec nC) :

Vec (N * (c * h * w)) → Vec (N * nC)

Head at inference: 1×1 conv-bn-swish → global-avg-pool → dense classifier.

Equations

One or more equations did not get rendered due to their size.

Instances For

def Proofs.StableHLO.stemGraphBEval (epsStr : String) {N ic oc h w : ℕ} (Ws : Kernel4 oc ic 3 3) (bs : Vec oc) (ε : ℝ) (γs βs μs vs : Vec oc) (e : SHlo (N * (ic * (2 * h) * (2 * w)))) :

SHlo (N * (oc * h * w))

Stem 3×3-s2 conv → inference bn → swish, batched.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Proofs.StableHLO.stemGraphBEval_faithful (epsStr : String) {N ic oc h w : ℕ} (Ws : Kernel4 oc ic 3 3) (bs : Vec oc) (ε : ℝ) (γs βs μs vs : Vec oc) (e : SHlo (N * (ic * (2 * h) * (2 * w)))) :

den (stemGraphBEval epsStr Ws bs ε γs βs μs vs e) = stemBEval N Ws bs ε γs βs μs vs (den e)

def Proofs.StableHLO.mbNoExpGraphBEval (p epsStr : String) {N ic oc h w kHd kWd r : ℕ} (ε : ℝ) (Wd : DepthwiseKernel ic kHd kWd) (bd γd βd μd vd : Vec ic) (Wz₁ : Mat ic r) (bz₁ : Vec r) (Wz₂ : Mat r ic) (bz₂ : Vec ic) (Wp : Kernel4 oc ic 1 1) (bp γp βp μp vp : Vec oc) (e : SHlo (N * (ic * h * w))) :

SHlo (N * (oc * h * w))

MBConv1 (no expand) at inference: dw-bn-swish → SE → project-bn, batched.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Proofs.StableHLO.mbNoExpGraphBEval_faithful (p epsStr : String) {N ic oc h w kHd kWd r : ℕ} (ε : ℝ) (Wd : DepthwiseKernel ic kHd kWd) (bd γd βd μd vd : Vec ic) (Wz₁ : Mat ic r) (bz₁ : Vec r) (Wz₂ : Mat r ic) (bz₂ : Vec ic) (Wp : Kernel4 oc ic 1 1) (bp γp βp μp vp : Vec oc) (e : SHlo (N * (ic * h * w))) :

den (mbNoExpGraphBEval p epsStr ε Wd bd γd βd μd vd Wz₁ bz₁ Wz₂ bz₂ Wp bp γp βp μp vp e) = mbNoExpFwdBEval N ε Wd bd γd βd μd vd Wz₁ bz₁ Wz₂ bz₂ Wp bp γp βp μp vp (den e)

def Proofs.StableHLO.mbStridedGraphBEval (p epsStr : String) {N ic mid oc h w kHd kWd r : ℕ} (ε : ℝ) (We : Kernel4 mid ic 1 1) (be γe βe μe ve : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd γd βd μd vd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp γp βp μp vp : Vec oc) (e : SHlo (N * (ic * (2 * h) * (2 * w)))) :

SHlo (N * (oc * h * w))

MBConv6 strided at inference: expand-bn-swish (at 2h×2w) → strided dw-bn-swish → SE → project-bn, batched.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Proofs.StableHLO.mbStridedGraphBEval_faithful (p epsStr : String) {N ic mid oc h w kHd kWd r : ℕ} (ε : ℝ) (We : Kernel4 mid ic 1 1) (be γe βe μe ve : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd γd βd μd vd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp γp βp μp vp : Vec oc) (e : SHlo (N * (ic * (2 * h) * (2 * w)))) :

den (mbStridedGraphBEval p epsStr ε We be γe βe μe ve Wd bd γd βd μd vd Wz₁ bz₁ Wz₂ bz₂ Wp bp γp βp μp vp e) = mbStridedFwdBEval N ε We be γe βe μe ve Wd bd γd βd μd vd Wz₁ bz₁ Wz₂ bz₂ Wp bp γp βp μp vp (den e)

def Proofs.StableHLO.mbResidGraphBEval (p epsStr : String) {N c mid h w kHd kWd r : ℕ} (ε : ℝ) (We : Kernel4 mid c 1 1) (be γe βe μe ve : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd γd βd μd vd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 c mid 1 1) (bp γp βp μp vp : Vec c) (e : SHlo (N * (c * h * w))) :

SHlo (N * (c * h * w))

MBConv6 with identity residual at inference: addV body skip.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Proofs.StableHLO.mbResidGraphBEval_faithful (p epsStr : String) {N c mid h w kHd kWd r : ℕ} (ε : ℝ) (We : Kernel4 mid c 1 1) (be γe βe μe ve : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd γd βd μd vd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 c mid 1 1) (bp γp βp μp vp : Vec c) (e : SHlo (N * (c * h * w))) :

den (mbResidGraphBEval p epsStr ε We be γe βe μe ve Wd bd γd βd μd vd Wz₁ bz₁ Wz₂ bz₂ Wp bp γp βp μp vp e) = mbResidFwdBEval N ε We be γe βe μe ve Wd bd γd βd μd vd Wz₁ bz₁ Wz₂ bz₂ Wp bp γp βp μp vp (den e)

def Proofs.StableHLO.headGraphBEval (epsStr : String) {N c oc h w nC : ℕ} (ε : ℝ) (Wh : Kernel4 oc c 1 1) (bh γh βh μh vh : Vec oc) (Wfc : Mat oc nC) (bfc : Vec nC) (e : SHlo (N * (c * h * w))) :

SHlo (N * nC)

Head at inference: 1×1 conv-bn-swish → GAP → dense, batched.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Proofs.StableHLO.headGraphBEval_faithful (epsStr : String) {N c oc h w nC : ℕ} (ε : ℝ) (Wh : Kernel4 oc c 1 1) (bh γh βh μh vh : Vec oc) (Wfc : Mat oc nC) (bfc : Vec nC) (e : SHlo (N * (c * h * w))) :

den (headGraphBEval epsStr ε Wh bh γh βh μh vh Wfc bfc e) = headFwdBEval N ε Wh bh γh βh μh vh Wfc bfc (den e)